# Re: [isabelle] structured induction proofs using customized induction scheme

Hi Bianca,

`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]: ...
lemma R_lc:
fixes t1 t2
assumes "R t1 t2"
shows "lc t1 & lc t2"
using assms
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
``explicitly:
`
...
using assms
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:
`
...
using assms
proof (induct t1 t2
taking: "%t1 t2. (ALL x. Q x --> lc (op t1 x) & lc (op t2 x))"
rule: R_induct)

`You can find more documentation on the induct method in the
``Isabelle/Isar Reference Manual, Sec. 6.6.
`
I hope this helps.
Regards,
Andreas

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