[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)?
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and