Re: [isabelle] Isabelle

Hi Mahmoud,

Yes, you can prove this theorem in a lot of detail using the proof language
Isar (see the
tutorial "Programming and Proving in Isabelle/HOL").

As an example, I attach a theory that shows the proof of one of the lemmas
you need to prove your theorem.
I use one of the several possible styles.


On Tue, Sep 30, 2014 at 9:15 AM, mahmoud abdelazim <m.abdelazim at>

> i am user of Isabelle and i am trying to proof a theorem for example :
>    theorem rev_rev [simp]: "rev(rev xs) = xs"
>    apply(induct_tac xs)
>    apply(auto)
>    done
> The steps of auto could be done using separate steps?
> The steps of induct_tac could be done using separate steps?
> please provide an example

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

Attachment: isarlistexample.thy
Description: Binary data

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