Re: [isabelle] finishing a proof



"assume" is used to state what is used as a premise of a goal, and neither P nor Q are given, that's why the proof fails. So, instead of proving a fact relying on "assume" you can prove a fact relying on "if we assume...":

proof -
Âassume "P â (Q â R)"
Âthen have "Q â R" if p: P by (simp add: p)
Âthen have "R"ÂÂÂÂÂÂ if p: P and q: Q by (simp add: p q)
Âthen have "P â R" if q: Q by (simp add: q)
Âthen have "Q â (P â R)" by simp
Âthen show ?thesis by assumption
qed

Given that "simp" is too powerful and could be used to prove the original lemma right away, you can also use explicit rules:

proof -
 Âassume "P â (Q â R)"
 Âthen have "Q â R" if p: P using p by (rule mp)
 Âthen have "R" if p: P and q: Q using q by (rule mp) (insert p)
 Âthen have "P â R" if q: Q by (rule impI) (insert q)
ÂÂÂthen show "Q â (P â R)" by (rule impI)
qed

Alexander Kogtenkov


>"Gergely Buday" <buday.gergely at uni-eszterhazy.hu>:
>
>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
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.