在应用样式中将目标放在目标中

Question

让我们假设我想要显示以下引理

lemma "? A; B; C ? ? D"

我得到了目标

1. A ? B ? C ? D

但是,我不需要B.我怎样才能将目标转移到类似的东西上

1. A ? C ? D

我不想改变原始lemma陈述,只是改变申请风格的当前目标.

Answer 1

你想要的是什么apply (thin_tac B).然而,上次我这样做时,彼得拉姆米奇喊道:"天啊,你为什么要这样做!" 厌恶并重写我的证据,以摆脱thin_tac.因此,使用这种策略似乎不再受到鼓励.

Answer 2

通常最好避免在目标状态下不需要的东西,而不是以后删除它.您制定证明问题的方式会影响您解决问题的方式.

这对于结构化证明尤其重要:您对那些应该参与证明的下一步的事实给予积极的反对,而不是消极地压制其中的一些.

像这样:

from `A` and `C` have D ...

告知哪些事实与证据相关已经是可读性的开始.

遵循该样式,您的初始问题将如下所示:

lemma
  assumes A and B and C 
  shows D
proof -
  from `A` and `C` show D sorry
qed

如果ABCD是大的命题,或者像这样减少详细程度:

lemma
  assumes a: A and b: B and c: C 
  shows D
proof -
  from a c show ?thesis sorry
qed