Re: [isabelle] structured induction proofs using customized induction scheme
unfortunately, I am not able to reproduce your error, but here are some
more hints on using the induct method:
1. The generated induction rules for inductive predicates "consume" the
premise for the inductive predicate. By passing this fact to the induct
method, it normally selects the right induction rule automatically.
Moreover, you do not have to show the inductive predicate goal any more.
If you want the same effect for your custom induction rule, use the
attribute "consumes n" where n is the number of facts to consume, usually 1.
In your example:
lemma R_induct[consumes 1]: ...
fixes t1 t2
assumes "R t1 t2"
shows "lc t1 & lc t2"
proof (induct rule: R_induct)
If you combine this with the case_names attribute, use consumes first.
Consumed assumptions are not counted when providing names.
In your example:
lemma R_induct[consumes 1, case_names P1_T1 P1_T2 ...]
2. Usually, you do not have to instantiate the parameters that appear in
the conclusion. In particular, ?P1 in R_induct is automatically unified
with "%t1 t2. lc t1 & lc t2" in your example. If induct has trouble to
figure out the right instantiation, you can provide the arguments to P1
proof (induct t1 t2 rule: R_induct)
3. Your induction rule R_induct involves the free variable P2 that does
not occur in the conclusion nor in the consumed facts. This is usually
the cause for your error message "unbound schematic variable(s) in case 2".
Rather than manually instantiating P2 in the induction rule, the induct
method provides the "taking" specification:
proof (induct t1 t2
taking: "%t1 t2. (ALL x. Q x --> lc (op t1 x) & lc (op t2 x))"
You can find more documentation on the induct method in the
Isabelle/Isar Reference Manual, Sec. 6.6.
I hope this helps.
This archive was generated by a fusion of
Pipermail (Mailman edition) and