1

イザベルのように目標があるときは、"∀x. P x"書くことができることを知っています

show "∀x. P x"
proof (rule allI)

しかし、目標がである場合"∀x>0. P x"、私にはそれができません。proof目標を単純化するために後で使用できる同様のルール/方法はありますか? という形の目標を持っているシチュエーションにも興味があります"∃x>0. P x"。

proof (rule something)スタイルを使用する Isar プルーフを探しています。

4

2 に答える 2

3

ユニバーサル量指定子

Lars の答えを拡張するには:∀x>0. P xは∀x. x > 0 ⟶ P x. 結果として、このようなステートメントを証明したい場合は、最初に で全称量指定子をallI取り除き、次に で含意を取り除く必要がありimpIます。次のようなことができます。

lemma "∀x>0. P x"
proof (rule allI, rule impI)

または、使用できなくなるまでintro適用するのとほぼ同じです。rule

lemma "∀x>0. P x"
proof (intro allI impI)

または、「安全」とsafe宣言されているすべての導入ルールを積極的に適用するを使用できます。allIimpI

lemma "∀x>0. P x"
proof safe

いずれにせよ、あなたの新しい証明状態は

proof (state)
goal (1 subgoal):
 1. ⋀x. 0 < x ⟹ P x

そして、次のように進めることができます：

lemma "∀x>0. P (x :: nat)"
proof safe
  fix x :: nat assume "x > 0"
  show "P x"

注釈を追加したことに注意してください。あなたのタイプがわからなかったPので、 を使用しnatました。Isar で変数を修正し、型が仮定から明確でない場合、新しい自由型変数が導入されたという警告が表示されますが、これは望んでいたものではありません。その警告が表示されたら、fix上記のように型注釈を追加する必要があります。

存在数量詞

存在量指定子の場合、技術的な理由によりsafeイントロ ルールが常に安全であるとは限らないため、機能しません。exIの典型的な証明パターンは次の∃x>0. P xようになります。

lemma "∃x>0. P (x :: nat)"
proof -
  have "42 > (0 :: nat)" by simp
  moreover have "P 42" sorry
  ultimately show ?thesis by blast
qed

またはもう少し明示的に：

lemma "∃x>0. P (x :: nat)"
proof -
  have "42 > 0 ∧ P 42" sorry
  thus ?thesis by (rule exI)
qed

実在の証人 (つまり、この例では 42) がobtainコマンドから取得した変数に依存しない場合は、より直接的に実行することもできます。

lemma "∃x>0. P (x :: nat)"
proof (intro exI conjI)

これにより、目標?x > 0とが残りますP ?x。?xは、任意に配置できるスキーマ変数であることに注意してください。したがって、次のように証明を完成させることができます。

lemma "∃x>0. P (x :: nat)"
proof (intro exI conjI)
  show "42 > (0::nat)" by simp
  show "P 42" sorry
qed

私が言ったように、あなたの実存証人が技術的な制限のためにあなたが得たいくつかの変数に依存している場合、これは機能しません. obtainその場合、私が言及した他の解決策にフォールバックする必要があります。

于 2016-11-24T07:27:53.343 に答える
1

以下は Isabelle2016-1-RC2 で機能します。

lemma "∀ x>0. P x"
  apply (rule allI)

一般にapply rule、デフォルトのイントロダクション ルールを選択する を使用することもできます。存在量指定子についても同じことが言えます。

于 2016-11-22T16:42:13.070 に答える