search

data61 / PSL

Other
64 stars 9 forks source link

PSL, MiLkMaId, LiFtEr: arbitrary x and y #39

Open yutakang opened 6 years ago

yutakang commented 6 years ago

Currently, PSL does not create a version of induction method that uses the "and" keyword between two "arbitrary" variables.

This limits the power of PSL.

See, for example, this entry to the Isabelle mailing list.

yutakang commented 6 years ago

Probably, two variables should be separated when they appear in different meta-conjuncts.

yutakang commented 6 years ago

It is often better to apply mathematical induction on variables that appear in all (or multiple) meta-conjuncts in the goal, especially when using "rule: *.inducts".

--> a mutually recursive function definition with the primrec does not produce .inducts rules. Only the inductive keyword does so for mutually inductive function definitions.

--> See line 98 of thysLambdaMu/DeBruijn.thy.

yutakang commented 6 years ago

I think PSL does not even support "rule: *.inducts".