*To*: çæç <wangsl at ios.ac.cn>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Induction principle for datatypes*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 29 Jan 2016 07:34:56 +0100*In-reply-to*: <1f03cf5c2c964e32bf9b96f33a3e20ac@EX01.ios.ac.cn>*References*: <1f03cf5c2c964e32bf9b96f33a3e20ac@EX01.ios.ac.cn>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

Dear Shuling, What version of Isabelle are you using?

lemma "PP a" and "QQ as" proof(induct a and as)

Hope this helps, Andreas On 29/01/16 05:04, çæç wrote:

Dear Isabelle list, I am defining a datatype which involves a list constructor, see the following code: datatype comm = skip | Seq comm comm | Cond "comm list" Notice that the length of the command list is not fixed. So this is why I use list here. Then I need to prove a property for the datatype: consts PP :: "comm => bool" lemma "PP a" To prove the above lemma, I apply âinductâ on ââaââ, and the following induction principle is produced by Isabelle, ââlist. PP (Cond list)â However, this is too weak to prove the fact. The induction hypothesis on the elements in the list are expected, which are, PP (fst a) and PP (Cond (snd a)) Is there any way I can solve the above problem, defining comm in another way, or using other stronger induction principles of Isabelle? I greatly appreciate your help. Thanks. Best regards, Shuling Wang SKLCS, Institute of Software, Chinese Academy of Sciences

**Follow-Ups**:

**References**:

- Previous by Date: [isabelle] Induction principle for datatypes
- Next by Date: Re: [isabelle] Induction principle for datatypes
- Previous by Thread: [isabelle] Induction principle for datatypes
- Next by Thread: Re: [isabelle] Induction principle for datatypes
- Cl-isabelle-users January 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list