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" はタプルで、やや見苦しい構文になります。残念ながら isabelle は、私が のようなものを書くことを許可していませんfor "(a,b)"。

この帰納的述語に対して、より適切な導入規則と帰納規則を作成するにはどうすればよいでしょうか?

4

1 に答える 1

0

my_inductive_introsより美しいベースケースとデフォルトのステップケースを使用して、導入ルールの新しいセットを定義できます

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 1isabelle に最初のパラメーターを使用するように指示します。これを例で説明しましょう。

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. ?a
  3. ⋀x y. someP (?a, ?b) xy ⟹ my_inductive (?a, ?b) x ⟹ x ⟹ y

を使用[consumes 1]すると、目的の証明状態が得られます。

  1. パーバ
  2. ⋀x y. someP (a, b) xy ⟹ my_inductive (a, b) x ⟹ P abx ⟹ P aby

case_namesisar プルーフのケース名を設定します。したがって、上記の証明は で開始できます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 に答える