4

在 Isabelle 中,有时会遇到重复子目标的情况。例如,想象以下证明脚本:

lemma "a ∧ a"
  apply (rule conjI)

有目标:

proof (prove): step 1

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

有没有办法就地消除重复的子目标,所以不需要重复证明?

4

3 回答 3

8

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

于 2013-03-25T05:43:39.710 回答
1

我遇到了类似的行为,作为应用于任何定理的方法的副作用subst,例如refl. 然后apply (subst refl)确实删除重复的子目标。

这不是一个错误,这是一个功能 ;-)。

于 2014-07-30T23:50:04.710 回答
1

添加到 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 *)
于 2020-08-31T20:46:34.120 回答