Re: [isabelle] Induction rules of the function package

Hi Andreas,

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 MHonArc.