Geek asks and answers

Throw a target in the app style

suppose I want to show the following lemma

lemma "⟦ A; B; C ⟧ ⟹ D"

I get the goal

1. A ⟹ B ⟹ C ⟹ D

However, I do not need B. How to transfer my goal to something like

1. A ⟹ C ⟹ D

I do not want to change the source statement lemma, only the current target in the application style.

+5
source share
2 answers

You want to apply (thin_tac B). However, the last time I did this, Peter Lammich shouted: "God, why are you doing this!" in disgust and rewrote my proof to get rid of the subtle. Thus, the use of this tactic no longer looks like a promotion.

+5
source

, . .

: , , , .

. :

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

, , .

, :

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

, , , A B C D - :

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

More articles:


All Articles