CODEWITHSUNDEEP
isabelle
corny
corny

Reputation: 7852

Drop a premise in a goal in apply style

let's assume I want to show the following lemma

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

I get the goal

1. A ⟹ B ⟹ C ⟹ D

However, I don't need B. How can I transfer my goal to something like

1. A ⟹ C ⟹ D

I don't want to alter the original lemma statement, just the current goal in apply style.

Upvotes: 6

Views: 405

Answers (2)

Makarius
Makarius

Reputation: 2204

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

Upvotes: 5

Manuel Eberl
Manuel Eberl

Reputation: 8258

What you want is apply (thin_tac B). However, the last time I did this, Peter Lammich shouted "Oh god, why are you doing this!" in disgust and rewrote my proof in order to get rid of the thin_tac. So using this tactic doesn't exactly seem to be encouraged anymore.

Upvotes: 6

Related Questions