I'm trying to write a custom induction rule for an inductive set. Unfortunately, when I try to apply it with induction rule: my_induct_rule, I get an extra, impossible to prove case. I have the following:
inductive iterate :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for f where
iter_refl [simp]: "iterate f a a"
| iter_step [elim]: "f a b ⟹ iterate f b c ⟹ iterate f a c"
theorem my_iterate_induct: "iterate f x y ⟹ (⋀a. P a a) ⟹
(⋀a b c. f a b ⟹ iterate f b c ⟹ P b c ⟹ P a c) ⟹ P x y"
by (induction x y rule: iterate.induct) simp_all
lemma iter_step_backwards: "iterate f a b ⟹ f b c ⟹ iterate f a c"
proof (induction a b rule: my_iterate_induct)
...
qed
Obviously the custom induction rule doesn't give me any new power (my real use case is more complicated) but that's kinda the point. my_iterate_induct is exactly the same as the autogenerated iterate.induct rule, as far as I can tell, but inside the proof block I have the following goals:
goal (3 subgoals):
1. iterate ?f a b
2. ⋀a. iterate f a a ⟹ f a c ⟹ iterate f a c
3. ⋀a b ca. ?f a b ⟹ iterate ?f b ca ⟹
(iterate f b ca ⟹ f ca c ⟹ iterate f b c) ⟹ iterate f a ca ⟹
f ca c ⟹ iterate f a c
Goal 1 seems to rise from some failure to unify ?f with the actual argument f, but if I ignore the fact that the f is fixed and try induction f a b rule: my_iterate_induct I just get Failed to apply proof method, as expected. How do I get the nice behaviour that the regular iterate.induct provides?
You need to declare your custom induction rule as ‘consuming’ one premise using the consumes attribute (see the Isabelle/Isar reference manual, §6.5.1):
theorem my_iterate_induct [consumes 1]: "iterate f x y ⟹ (⋀a. P a a) ⟹
(⋀a b c. f a b ⟹ iterate f b c ⟹ P b c ⟹ P a c) ⟹ P x y"
by (induction x y rule: iterate.induct) simp_all