Gergely Buday

2016-10-13 09:20:13 UTC

Permalink

Hi,Raw Message

I would like to write a forward proof in Isar to have

P ⟶ (Q ⟶ R) ⟹ Q ⟶ (P ⟶ R)

by hand it can be done through two implication eliminations using P and Q as assumptions, and then re-introducing implications but in the reverse order.

I wrote the following to formalise this:

theory Logic

imports Main

begin

lemma "P ⟶ (Q ⟶ R) ⟹ Q ⟶ (P ⟶ R)"

proof -

assume premise : "P ⟶ (Q ⟶ R)"

assume p: "P"

have qr: "Q ⟶ R" by (simp add: p premise)

assume q: "Q"

have r: "R" by (simp add: q qr)

from this have "P ⟶ R" by (simp add: p)

from this have "Q ⟶ (P ⟶ R)" by (simp add: q)

thus "P ⟶ (Q ⟶ R) ⟹ Q ⟶ (P ⟶ R)" by assumption

Failed to refine any pending goal

Local statement fails to refine any pending goal

Failed attempt to solve goal by exported rule:

(P ⟶ Q ⟶ R) ⟹ (P) ⟹ (Q) ⟹ (P ⟶ Q ⟶ R) ⟹ Q ⟶ P ⟶ R

It fails at the last line, it is not really clear why. Can you give a clue?

- Gergely