1

假设我们有一些谓词

definition someP :: "('a × 'a) ⇒ 'a ⇒ 'a ⇒ bool"

和一个inductive结束它

inductive my_inductive :: "('a × 'a) ⇒ 'a ⇒ bool"
 for "a_b" where
 basecase: "fst a_b = a ⟹ my_inductive a_b a" |
 stepcase: "someP a_b x y ⟹ my_inductive a_b x ⟹ my_inductive a_b y"

第一个参数“a_b”的归纳是固定的。"a_b" 是一个元组，导致语法有些难看。不幸的是，伊莎贝尔不允许我写类似for "(a,b)".

如何为这个归纳谓词创建更好的介绍和归纳规则？

4

1 回答 1

0

my_inductive_intros我们可以用更漂亮的basecase和默认stepcase定义一组新的引入规则

lemma my_inductive_intro_1: "my_inductive (a, b) a"
  by (simp add: my_inductive.basecase)
lemmas my_inductive_intros = my_inductive_intro_1 my_inductive.stepcase

我们可以编写自己漂亮的归纳规则

lemma my_inductive_tuple_induct[consumes 1, case_names "basecase" "stepcase", induct pred: my_inductive]: 
 "my_inductive (a, b) x ⟹ 
 (P a) ⟹ (⋀x y. someP (a, b) x y ⟹ my_inductive (a, b) x ⟹ P x ⟹ P y) ⟹ P x"
 apply(rule my_inductive.induct[of "(a,b)"])
 apply(simp_all)
 done

consumes 1告诉 isabelle 使用第一个参数。让我们通过一个例子来说明这一点：

lemma "my_inductive (a,b) c ⟹ P a b c"
  proof(induction rule: my_inductive_tuple_induct)

没有[consumes 1]这个就是证明状态：

  1. my_inductive (?a, ?b) (my_inductive (a, b) c ⟶ P abc)
  2. ？一种
  3. ⋀xy。someP (?a, ?b) xy ⟹ my_inductive (?a, ?b) x ⟹ x ⟹ y

有了[consumes 1]，我们得到了想要的证明状态：

  1. 爸爸
  2. ⋀xy。someP (a, b) xy ⟹ my_inductive (a, b) x ⟹ P abx ⟹ P aby

case_names为 isar 证明设置案例名称。因此，上述证明可以从 开始case basecase。

induct pred告诉我们正在声明一个归纳规则。在某些情况下，proof(induction)现在仅仅写作可能就足以让 isabelle 自己找出来使用我们新的奇特归纳规则。

以下示例演示了设置

lemma
  assumes "my_inductive (a,b) c" shows "P a b c"
  using assms
proof (induction)
case basecase thus ?case using my_inductive_intros sorry
case (stepcase x y) thus ?case using my_inductive_intros sorry
qed
于 2013-04-24T07:30:58.683 回答