Re: [isabelle] Induction rules of the function package
the induction rules that the function package generates for a function
definitions are usually great. However, is always quantifies over all
parameters of the function, even if they are just passed through all
recursive calls. For some proofs, I would like not to have them
quantified. Is there an option to the function package to declare such
parameters to treat differently (like the for clause for inductive)?
Currently, there is no such option. In fact, a for-clause would not
solve the problem completely, since even if an argument arguments does
change in recursive calls, one would sometime like to see it
eliminated from the induction rule.
In suce a case, I usually project away the extra arguments manually
(using something like [where P="%x y. Q y", standard]), which is not
nice but works.
This archive was generated by a fusion of
Pipermail (Mailman edition) and