如何在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)確實刪除重複的子目標。

這不是一個錯誤，它是一個功能;-)。