*To*: michel levy <michel.levy at imag.fr>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] elementary proofs*From*: Alfio Martini <alfio.martini at acm.org>*Date*: Sun, 27 Mar 2016 13:15:10 -0300*In-reply-to*: <56F80477.4080006@imag.fr>*References*: <56F711D4.8090403@imag.fr> <CAAPnxw3O2LCpeFstfmwHGnkEXVgiT_wrR9XzgwB3ffJZVHfniw@mail.gmail.com> <56F7B087.4070704@imag.fr> <CAAPnxw0b+YA1DMv18415WUqvMBa7eoXQNcLN9EuKokQYrfVa6A@mail.gmail.com> <56F80477.4080006@imag.fr>*Sender*: alfio.martini at gmail.com

Hi Michel, Here goes one way to do it: theorem "P â Q --> Q â P" proof (rule impI) assume 1: "P \/ Q" show "Q \/ P" proof (rule disjE[OF 1]) assume "P" then show "Q \/ P" by (rule disj2) next assume "Q" then show "Q \/ P" by (rule disjI1) qed qed Best On Sun, Mar 27, 2016 at 1:04 PM, michel levy <michel.levy at imag.fr> wrote: > On 27/03/2016 12:38, Alfio Martini wrote: > > > > Hi, > > > > It should be in the reference manual and in the programming and > > proving tutorial. > > > > Best > > > You're right. I find some examples in the tutorial prog-prove. > But I have still difficulties to understand how to prove (always with > the same style) P \/ Q --> Q \/ P. > I have tried this "proof" > > proof > assume 1: "P â Q" > show "Q â P" > proof (rule disjE) > assume "P" > show "Q â P" by (rule disjI2) > next > assume "Q" > show "Q â P" by (rule disjI1) > ------------- at this point I am lost. > qed > oops > > Can you help me how to solve this proof ? > > Sincerely yours > > PS : I am a beginner in my study of Isabelle, and because I am retired, > it's not easy to find a help. > > -- > email : michel.levy at imag.fr > http://membres-liglab.imag.fr/michel.levy > > -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) Associate Professor at Faculty of Informatics (PUCRS) www.inf.pucrs.br/alfio Av. Ipiranga, 6681 - PrÃdio 32 - Faculdade de InformÃtica 90619-900 -Porto Alegre - RS - Brasil

**References**:**[isabelle] elementary proofs***From:*michel levy

**Re: [isabelle] elementary proofs***From:*Alfio Martini

**Re: [isabelle] elementary proofs***From:*Alfio Martini

- Previous by Date: Re: [isabelle] elementary proofs
- Next by Date: [isabelle] Lemmas reuse
- Previous by Thread: Re: [isabelle] elementary proofs
- Next by Thread: [isabelle] Lemmas reuse
- Cl-isabelle-users March 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