3

次のばかげた例を考えてみましょう

theory meta_all
imports Main
begin

lemma strict_subset: "⟦ A ⊂ B ⟧ ⟹ ∃a ∈ B. a ∉ A"
apply(blast)
done

lemma strict_subset2: "∀A B. A ⊂ B ⟶ (∃a ∈ B. a ∉ A)"
apply(blast)
done

lemma "¬ (∃A. A ⊂ A)"
apply(rule notI)
apply(erule exE)

次に、補題を使用してとの両方をstrict_subset置き換えたいと思います。それは実行されますが、既存の名前が に変更され、補題を導入する目的が完全に無効になります。AABAAa

apply(insert strict_subset [where A="A" and B="A"])

導出されたレンマを使用すると、strict_subset2すべてうまくいくので、私の推論は正しいと確信しています。

apply(insert strict_subset2)
apply(erule_tac x="A" in allE, erule_tac x="A" in allE)
apply(drule mp, assumption)
apply(erule bexE, erule notE, assumption)
done

end

要点は、ほとんどの標準補題は形式のものであり、形式のものstrict_subsetではなくstrict_subset2、Isabelle の作成者は私がstrict_subset2最初に自分自身を作成することを意図していない可能性があるということです。したがって、私は何か間違ったことをしているに違いありません.

名前が変更された理由を知りたいAですか？タイプが正確である限り、メタユニバーサル定量化が問題にならなかった例も見たことがあると思うので、それはタイピングシステムと関係があると思います。

Aもう1つの質問は、どうにかして名前の変更を防ぐことができるかどうかです。

もちろん、私はまだ Isabelle に慣れていないので、両方の質問が本当に正しい答えと無関係になる可能性は十分にあります。

PS。ここでもイザベルから素敵なシンボルを手に入れることはできますか?

4

3 に答える 3

3

これは、この実験の道が意味をなすかどうかという質問に着手することなく、単なる狭い技術的な答えです。

あなたの状況では

apply(insert strict_subset [where A="A" and B="A"])

問題のサブゴールはこれでした：

⋀A. A ⊂ A ⟹ False

ただし、ローカルにバインドされた（緑）Aは、サブゴールのいわゆる「パラメーター」であり、ゴールコンテキスト内に隠されていることを意味します。の使用は、証明の目標ではなく、証明のテキストstrict_subset [where A="A" and B="A"]のコンテキストを指します。したがって、異なる（無料、宣言されていない）が得られます。これは、証明者の出力の特別な強調表示によっても示されます。A

暗黙の目標コンテキストの下でダイビングし、いくつかのインスタンス化を行うことを可能にする（非常に古風な）戦術の特別なセットがあります。次に例を示します。

apply(cut_tac A = A and B = A in strict_subset)

これで、ゴール状態内にグリーンのインスタンスができましAたが、ルールの形式とこの奇妙な動作により、サブゴールに分割されすぎていますcut_tac。

基本的に、Isabelle/Isar証明方法には次のカテゴリがあることに注意してください。

  • 構造化されたIsarプルーフステップ：特にrule

  • 推論の方向性を示す弱く構造化されたステップ：erule、、drulefrule

  • パラメータを使用して暗黙の目標コンテキストを入力できる古いスタイルの戦術エミュレーション：rule_tac、、、erule_tacdrule_tacfrule_tac

PS：Isabelle/jEditからのUnicode出力をこのテキストエディタにコピーアンドペーストできます。

于 2013-03-12T22:19:38.603 に答える
1

apply (insert strict_subset)に変更する必要があると思いますapply (drule strict_subset)。その後、証明は までに終了できますapply simp。

(insert fooメソッドはfoo追加の仮定として追加し、それがもたらすメタ量指定子を完備しています。必要なのはdrule fooメソッドであり、含意に従って仮定の 1 つを弱めますfoo。)

于 2013-03-12T21:37:42.890 に答える
1

構造化された証明は、前述の命名の問題を回避し、単一ステップの推論を実行することもできます。

lemma  "¬ (∃A :: 'a set. A ⊂ A)"
proof
   assume "∃A :: 'a set. A ⊂ A"
   then obtain A :: "'a set" where "A ⊂ A" ..          (* by (rule exE) *)
   then have "∃a ∈ A. a ∉ A" by (rule strict_subset)
   then obtain a where "a ∉ A" "a ∈ A" ..              (* by (rule bexE) *)
   then show False ..                                  (* by (rule notE) *)
qed

..と同じby ruleです。using [[rule_trace]]証明ステップの前に (および find_theorems を)使用して、どのルールruleが使用されているかを把握できます。

この構造により、証明で何が起こっているかがさらに明確になります。もちろん、apply-style は間違いなくより探索的なタッチを持っています (これが、証明を見つけようとするときに私がしばしば好む理由です) が、構造化された証明はより多くの制御を提供します。

于 2013-03-29T09:04:22.637 に答える