Gergely Buday
2016-10-13 09:20:13 UTC
Hi,
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
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