如何在参数化归纳集上编写自定义归纳规则？

Question

我正在尝试为归纳集编写自定义归纳规则。不幸的是，当我尝试使用induction rule: my_induct_rule 应用它时，我得到了一个额外的、无法证明的案例。我有以下内容：

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

显然，自定义归纳规则并没有给我任何新的力量（我的实际用例更复杂），但这就是重点。 my_iterate_induct 与自动生成的 iterate.induct 规则完全相同，据我所知，但在证明块内我有以下目标：

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

目标 1 似乎是由于未能将 ?f 与实际参数 f 统一起来，但如果我忽略 f 是固定的事实并尝试induction f a b rule: my_iterate_induct，我只会得到Failed to apply proof method，正如预期的那样。如何获得常规 iterate.induct 提供的良好行为？

Answer 1

您需要使用consumes 属性将您的自定义归纳规则声明为“消耗”一个前提（请参阅 Isabelle/Isar 参考手册，第 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