如何删除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世界.