isabelle - 如何删除 Isabelle 中的重复子目标？

Question

在 Isabelle 中，有时会遇到存在重复子目标的场景。例如，想象以下证明脚本:

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 世界。