3

Isabelle に次のコードがあるとします。

lemma"[| xs@zs = ys@xs ;[]@xs = []@[] |] => ys=zs" (*never mind the lemma body*)
apply simp
done

上記のコードでは、simp メソッドが補題を証明しています。単純化法がこの補題を証明するために必要な詳細な (書き換え/単純化) 手順を確認して印刷することに興味があります (そして、他のすべての証明方法についても同じことができる可能性があります)。これはどのように可能ですか？

JEdi​​tエディターでisabelle 2014を使用しています。

どうもありがとう

4

2 に答える 2

4

simp_trace単純化トレースは、属性またはsimp_trace_new次を指定することで有効にできます。

lemma "⟦xs @ zs = ys @ xs; [] @ xs = [] @ [] ⟧ ⟹ ys = zs"
  using [[simp_trace]]
  apply simp
done

カーソルがsimpステップの後に配置されている場合、出力ペインには書き換えトレースがインラインで表示されます (追加されたルール、適用されたルール、および書き換えられた用語のリストが表示されます)。

simp_trace_newトレースのよりコンパクトなバリアント (書き換えられたもの) を別のウィンドウで見ることができます (メッセージの強調表示された部分を押すと、トレース ペインがアクティブになります。トレース）。オプションを追加すると、 にmode=full似たより詳細な出力が生成されますsimp_traceが、より構造化された方法で生成されます。

lemma "⟦xs @ zs = ys @ xs; [] @ xs = [] @ [] ⟧ ⟹ ys = zs"
  using [[simp_trace_new mode=full]]
  apply simp
done

詳細については、Isabelle2014 のインストールにも含まれているIsabelle/Isar リファレンス マニュアルを参照してください。

于 2014-11-09T07:46:22.787 に答える
3

ファイルを 1 つまたは 2 つダウンロードしてよろしければ、l4.verifiedプロジェクトには、 Daniel Matichuk によって作成されたApply Traceというツールが含まれています。apply_traceこれにより、通常 を使用する場所であればどこでも使用できる新しいコマンドが提供されますapplyが、ステップで使用される定理が表示されます。

たとえば、次のように記述します。

lemma "⟦xs @ zs = ys @ xs; [] @ xs = [] @ [] ⟧ ⟹ ys = zs"
  apply_trace simp

生成:

used theorems:
  simp_thms(6): (?x = ?x) = True
  append_Nil: [] @ ?ys = ?ys
  append_Nil2: ?xs @ [] = ?xs

とは異なりsimp_trace、定理がどの順序で適用されたかはわかりません。ただし、すべてのメソッド ( simp、clarsimp、fastforce、autoなど) を操作simp_traceできますが、単純化に基づくメソッドでのみ機能します。

Apply_Trace_Cmd.thyそれを使用するには、ファイルとApply_Trace.thyインポートの両方を取得する必要がありますApply_Trace_Cmd。

于 2014-11-09T10:35:36.940 に答える