isabelle - 以应用风格删除目标中的前提

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

Normally it is better to avoid unwanted stuff in a goal state, instead of removing it later. The way you formulate a proof problem affects the way you solve it.

This is particularly important for structured proofs: you appeal positively to those facts that should participate in the next step of the proof, instead of suppressing some of them negatively.

E.g. like this:

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

Telling which facts are relevant to a proof is already a start for readability.

Following that style, your initial problem will look like this:

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

or like this with reduced verbosity, if A B C D are large propositions:

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