[isabelle] Induction rules of the function package



Hi all,

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)?

A concrete example:

fun map where
  "map f [] = []"
| "map f (x # xs) = f x # map f xs"

produces the induction rule map.induct:
[| !!f. P f []; !!f x xs. P f xs ==> P f (x # xs) |] ==> P a0 a1

but I would much more like the following rule (which I currently derive by hand from the generated one):
[| P []; !!x xs. P xs ==> P (x # xs) |] ==> P a

Thanks,
Andreas





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.