let's assume I want to show the following lemma <pre class="prettyprint"><code>lemma "⟦ A; B; C ⟧ ⟹ D" </code></pre> I get the goal <pre class="prettyprint"><code>1. A ⟹ B ⟹ C ⟹ D </code></pre> However, I don't need <code>B</code>. How can I transfer my goal to something like <pre class="prettyprint"><code>1. A ⟹ C ⟹ D </code></pre> I don't want to alter the original <code>lemma</code> statement, just the current goal in apply style.

Drop a premise in a goal in apply style

Tags:

isabelle

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.

960

asked Mar 09 '13 14:03

1 Answers

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.

108