*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] finishing a proof*From*: Alexander Kogtenkov via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*Date*: Thu, 13 Oct 2016 14:40:41 +0300*Authentication-results*: f340.i.mail.ru; auth=pass smtp.auth=kwaxer@mail.ru smtp.mailfrom=kwaxer@mail.ru*In-reply-to*: <002401d22532$530fc2a0$f92f47e0$@uni-eszterhazy.hu>*References*: <002401d22532$530fc2a0$f92f47e0$@uni-eszterhazy.hu>*Reply-to*: Alexander Kogtenkov <kwaxer at mail.ru>

"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 >

**Follow-Ups**:**Re: [isabelle] finishing a proof***From:*Gergely Buday

**References**:**[isabelle] finishing a proof***From:*Gergely Buday

- Previous by Date: Re: [isabelle] finishing a proof
- Next by Date: Re: [isabelle] finishing a proof
- Previous by Thread: Re: [isabelle] finishing a proof
- Next by Thread: Re: [isabelle] finishing a proof
- Cl-isabelle-users October 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list