4

証明することに困惑している

A ==> B ==> C ==> B

イザベルで。明らかにあなたができる

apply simp

しかし、ルールを使用してこれをどのように証明できますか?

または、使用されているルールをダンプする方法はありsimpますか? ありがとう。

4

2 に答える 2

6

証明がどのように機能するかを本当に理解したい場合は、最初に面白い戦術と自動推論ツールの両方を忘れる必要があります。

A ==> B ==> C ==> BIsabelle/Pure の(この特別な接続詞を使用した)ステートメント==>はすぐに真になるため、Isabelle/Isar での証明は次のとおりです。

lemma "A ==> B ==> C ==> B" .

それだけです.(これは を省略しますby thisが、this実際にはここでは空です)。

少し空虚でない証明では、実際の Isabelle/HOL 結合子を使用するため、標準的な導入または削除手順で処理できます。たとえば、次のようにします。

lemma "A --> B --> C --> B"
proof
  show "B --> C --> B"
  proof
    assume b: B
    show "C --> B"
    proof
      show B by (rule b)
    qed
  qed
qed

しかし、それもそれほど興味深いものではありません。退屈な含意を構築し、それを最後まで分解します。

より興味深い Isabelle/Isar の証明を見つけるには、Web 検索を行うか、システムに付属のソースを調べてください。完全に恣意的な例を次に示します: Drinker。

マニュアルもたくさんありますが、実際には多すぎます。

于 2014-03-14T20:34:24.760 に答える
4

単純化トレースを有効にすることができます。Proof General では、Isabelle → Settings → Tracing → Trace Simplifier でこれを行うことができます。jEdit についてはわかりません。

EDIT：この場合、単純なトレースはあまり役に立ちsimpません。これを解決するために書き換えルールを使用しないため、代わりに、前提でA、B、およびCを「認識」し、このステートメントのコンテキストで可能であると結論付けます、A = True、B = True、およびC = Trueを書き換えてから、ゴールBをに書き換えてTrue完了です。

ただし、このようなステートメントを証明する「通常の」方法はassumption、前提に対して目標を一致させる方法を使用することBです。おそらくこれを使用して証明する方法ruleもありますが、それは不必要に複雑になります。assumptionこれは非常に基本的なfunctionassume_tacの単なるラッパーであるため、Isabelle で最も基本的な証明方法の 1 つと見なすことができます。だからただ書いてください。Thm.assumptionby assumption

于 2013-11-28T18:05:35.850 に答える