isabelle - Isabelleで重複するサブゴールを削除するにはどうすればよいですか？

Question

イザベルでは、サブゴールが重複しているシナリオにたまに到達します。たとえば、次の証明スクリプトを想像してみてください。

lemma "a ∧ a"
  apply (rule conjI)

目標を持って：

proof (prove): step 1

goal (2 subgoals):
 1. a
 2. a    

重複するサブゴールをインプレースで排除する方法はありますか？そのため、証明を繰り返す必要はありませんか？

Answer 1

のMLレベルの戦術は、重複するサブゴールdistinct_subgoals_tacをPure/tactic.ML削除し、次のように使用できます。

lemma "a ∧ a"
  apply (rule conjI)
  apply (tactic {* distinct_subgoals_tac *})

去る：

proof (prove): step 2

goal (1 subgoal):
 1. a

残念ながら、MLの世界に立ち寄らなければ方法はないようです。

Answer 2

substたとえば、任意の定理に適用される方法の副作用と同様の動作に遭遇しましたrefl。次にapply (subst refl)、重複するサブゴールを実際に削除します。

これはバグではなく、機能です;-)。

Answer 3

davidgの答えに加えてtactic、何らかの理由で使用したくない場合はdistinct_subgoals_tac、メソッドに変換するのは簡単です。

method_setup distinct_subgoals =
  ‹Scan.succeed (K (SIMPLE_METHOD distinct_subgoals_tac))›

lemma P and P and P
  (* here there are three goals P *)
  apply distinct_subgoals
  (* now there is only one goal P *)