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.