Re: [isabelle] elementary proofs

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

```

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