*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 20:01:11 +0300*Authentication-results*: f221.i.mail.ru; auth=pass smtp.auth=kwaxer@mail.ru smtp.mailfrom=kwaxer@mail.ru*In-reply-to*: <006001d22550$870eef40$952ccdc0$@uni-eszterhazy.hu>*References*: <002401d22532$530fc2a0$f92f47e0$@uni-eszterhazy.hu> <1476358841.502079848@f340.i.mail.ru> <006001d22550$870eef40$952ccdc0$@uni-eszterhazy.hu>*Reply-to*: Alexander Kogtenkov <kwaxer at mail.ru>

The form "assumes-shows" separates facts, so if in the proof you want to rely on the facts from "assumes", you need to tell it by adding ÂÂ using assms proof - Then your version completes without an issue. (You can also use "pqr" instead of a general "assms" to refer to the particular fact.) Another variant is to replace "assume" with the fact itself. In this case "using assms" is not required: proof - Â Ânote pqr ÂÂÂ... Finally, you can just use "pqr" in the proof itself. Then neither "assume" nor "note" is required: lemma assumes pqr: "P â (Q â R)" shows "Q â (P â R)" proof - Âhave "Q â R" if p: P using pqr p by (rule mp) Âthen have "R" if p: P and q: Q using q by (rule mp) (insert p pqr) Âthen have "P â R" if q: Q by (rule impI) (insert q pqr) Âthen show "Q â (P â R)" by (rule impI) (insert pqr) qed Alexander Kogtenkov >"Gergely Buday" <buday.gergely at uni-eszterhazy.hu>: > >Alexander Kogtenkov wrote: > >> "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 > >Thanks. > >A question: > >if I write > >lemma assumes pqr: "P â (Q â R)" shows "Q â (P â R)" >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 have "Q â (P â R)" by (rule impI) > >I have > >have Q â P â R >proof (state) >this: >ÂÂQ â P â R > >goal (1 subgoal): >Â1. Q â P â R > >which I guess should be trivial to solve but it resisted any attempt. > >What is wrong here? > >- Gergely

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

**Re: [isabelle] finishing a proof***From:*Alexander Kogtenkov via Cl-isabelle-users

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

- Previous by Date: Re: [isabelle] New in the AFP: Intersecting Chords Theorem
- Next by Date: Re: [isabelle] New in the AFP: Intersecting Chords Theorem
- Previous by Thread: Re: [isabelle] finishing a proof
- Next by Thread: [isabelle] Foundations of Mathematics: Type Theory after Church's Simple Theory of Types (1940)
- 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