Isabelleの完全証明出力

Question

Isabelleが補題の証明を見つけられなかった場合、サブゴールに到達するために使用されたすべての証明方法によって行われたすべてを出力することは可能ですか？さらに進む？これは、彼らが正しい方向にそれらを指すのに役立つ、つかの間につかまった道が見えるのを助けるだろう。

（私はそれが面白い証拠いくつかの補題に行われた全ての基本推論を示し、完全な証拠のログを持って見つけるだろう完了の証明のためにも。）

Answer 1

この質問はthis oneに似て聞こえる、私は答えています数日前。その答えの一部もここに当てはまります。とにかく、この質問に具体的に答えるには：

本当にそうではありません。ほとんどの基本的な証明方法（ruleなど、intro、fact、cases、induct）は、彼らが行うことは比較的簡単で、失敗したときには、適用しようとした規則が目標/彼らが与えられた前提。 （または、彼らは最初の場所に適用するルールたかわからない）

おそらくblast、force、simp、およびautoのようなより自動戦術の多くを考えていました。それらのほとんどは、サブゴールを解決するか、まったく何もしないかのいずれかである（すべてblast、force、fastforce、fast、metis、meson、bestなど）です。したがって、どこに行き詰まっているのかを調べるのはちょっと難しいです。通常、人々はautoをこの種の探索に使用します：autoを適用し、残りのサブゴールを見て、それらを分解するためにどのような事実/もっと。

simpの状況は、auto未満であることを除いて同様です。 simpは、用語の書き換え、simprocsと呼ばれるカスタム書き換え手続き、ある種のソルバー（例えば線形算術のためのもの）、そしてスプリッターのような便利なもののいくつかを使ってifの式を取り除く単純化されたものです。 autoは基本的にsimpと古典的な推論を組み合わせたもので、simpよりはるかに強力ですが、あまり予測できません。 （時折、autoがあまりにも多く、それによってunprovableゴールに証明可能な目標を回すん）

いくつかのトレースツール（hereを説明されている、例えばシンプリトレースは、）があります。私は古典的な推論を辿る方法もあると思ったが、もはやそれを見つけることができない。おそらく私は間違っていた。いずれにしても、トレースツールは予期しない動作を説明するのに役立つことがありますが、ここで使用するものとは思われません。より良い方法は、これらのメソッドがどのような種類のものを試しているのかを理解することです。simpまたはautoがサブゴールを返すとき、あなたはそれらを見て、simpとautoが何をするのか、 （通常は何らかの欠落事実があるため）、修正してください。