5

ときどき<statement> solve_direct(通常は を介し​​て呼び出し<statement> tryます) は多数のライブラリ定理をリストし、「現在の目標は次の方法で直接解決できます: …」と述べています。

<theorem>を の検索結果の 1 つとすると、solve_directほとんどの場合、 を証明でき<statement> by (rule theorem)ます。

ただし、そのような証明が受け入れられない場合があり、その結果、「最初の証明方法を適用できませんでした」というエラー メッセージが表示されます。

によって見つかった定理を再利用するための一般的な別の手法はありsolve_directますか?

それとも個々の状況によるのでしょうか？最小限の例を作成して、この質問に添付することができます。

4

3 に答える 3

5

個人的には、私はただ使用する傾向があります：

apply (metis thm)

これは、ほとんどの場合、私に非常に一生懸命考えることを強いることなく機能します (ただし、トリッキーな解決策が必要な場合は、それでも失敗することがあります)。

通常は次のような方法も使用できます。

apply (rule thm)                 (* If "thm" has no premises. *)
apply (erule thm)                (* If "thm" has a single premise. *)
apply (erule thm, assumption+)   (* If "thm" has multiple premises. *)

答えが1つじゃないのはなぜ？答えは少し複雑です。

内部的に をsolve_direct呼び出しfind_theorems solves、次の処理を実行します。

fun etacn thm i = Seq.take (! tac_limit) o etac thm i;
(* ... *)
if Thm.no_prems thm then rtac thm 1 goal
else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;

rule thmこれは、ルールに前提がない場合、または次のような場合の ML コードです。

apply (erule thm, assumption+)

ルールに複数の前提がある場合。あなたの質問についてブライアンがコメントしたように、仮定に複雑なメタ論理結合がある場合、上記はまだ失敗する可能性があります（これはnorm_hhf_tac対処しますが、私が知る限りイザベルメソッドとして直接公開されていません）。

find_theorems必要に応じて、次のように、によって使用される戦術を直接公開する新しいメソッドを作成できます。

ML {*
  fun solve_direct_tac thm ctxt goal =
  if Thm.no_prems thm then rtac thm 1 goal
  else (etac thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
*}

method_setup solve =
  {* Attrib.thm >> (fn thm => fn ctxt =>
        SIMPLE_METHOD' (K (solve_direct_tac thm ctxt ))) *}
  "directly solve a rule"

これは、次のように使用できます。

lemma "⟦ a; b ⟧ ⟹ a ∧ b"
  by (solve conjI)

うまくいけばsolve_direct、あなたに投げかけられるものは何でも解決するはずです.

于 2013-08-30T00:12:48.450 に答える
1

solve_directの提案を使用する別の方法を で見つけましたby rule。など、ライブラリの特定の非常に基本的なルールHilbert_Choice.someI2が提案されている場合、コンテキスト内の事実の 1 つが実際には適用可能なルール自体であるように見えます。以下は、少なくとも2つの具体的な状況で機能しました（source）：

  1. 「ルールに似た」事実、その他の事実（もしあれば）、および目標を再検討する
  2. 必要に応じて、他のファクトを並べ替えます
  3. 証明をするusing <other_facts> ... by (rule <rule-like-fact>)
于 2013-09-11T11:45:27.990 に答える
0

factまたはを試すことができますrule_tac。私の記憶が正しければrule、他の事実が存在する場合に特定のルールを適用できないことがありますが、その理由は完全にはわかりません。その質問には、私よりもこれらのメソッドの実装の詳細に詳しい人が答える必要があります。

于 2013-08-29T13:38:41.593 に答える