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.