Re: [isabelle] elementary proofs
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])
then show "Q \/ P" by (rule disj2)
then show "Q \/ P" by (rule disjI1)
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"
> assume 1: "P â Q"
> show "Q â P"
> proof (rule disjE)
> assume "P"
> show "Q â P" by (rule disjI2)
> assume "Q"
> show "Q â P" by (rule disjI1)
> ------------- at this point I am lost.
> 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
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
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