在 Isabelle 中,有时会遇到重复子目标的情况。例如,想象以下证明脚本:
lemma "a ∧ a"
apply (rule conjI)
有目标:
proof (prove): step 1
goal (2 subgoals):
1. a
2. a
有没有办法就地消除重复的子目标,所以不需要重复证明?
在 Isabelle 中,有时会遇到重复子目标的情况。例如,想象以下证明脚本:
lemma "a ∧ a"
apply (rule conjI)
有目标:
proof (prove): step 1
goal (2 subgoals):
1. a
2. a
有没有办法就地消除重复的子目标,所以不需要重复证明?
distinct_subgoals_tac
删除重复子目标中的 ML 级别策略Pure/tactic.ML
,可按如下方式使用:
lemma "a ∧ a"
apply (rule conjI)
apply (tactic {* distinct_subgoals_tac *})
离开:
proof (prove): step 2
goal (1 subgoal):
1. a
不幸的是,似乎没有办法不进入 ML 世界。
我遇到了类似的行为,作为应用于任何定理的方法的副作用subst
,例如refl
. 然后apply (subst refl)
确实删除重复的子目标。
这不是一个错误,这是一个功能 ;-)。
添加到 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 *)