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.

Best!

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

> 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)
www.inf.pucrs.br/alfio
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.