*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Induction principle for datatypes*From*: çæç <wangsl at ios.ac.cn>*Date*: Fri, 29 Jan 2016 10:02:15 +0000*Accept-language*: zh-CN, en-US*In-reply-to*: <56AB0810.5050400@inf.ethz.ch>*References*: <1f03cf5c2c964e32bf9b96f33a3e20ac@EX01.ios.ac.cn> <56AB0810.5050400@inf.ethz.ch>*Thread-index*: AdFaSjukDY4fC2PaQh2sqagy3P5TRv//o8IA//8/UGA=*Thread-topic*: [isabelle] Induction principle for datatypes

Dear Andreas, Thanks. I am using Isabelle 2014. I just tried to use mutual recursion to my case and it works, while one problem is that I need to redefine many functions of the datatype. So I install Isabelle2015, and as you said, I find the induction hypothesis is strong enough. Best regards, Shuling Wang SKLCS, Institute of Software, Chinese Academy of Sciences > -----Original Message----- > From: Andreas Lochbihler [mailto:andreas.lochbihler at inf.ethz.ch] > Sent: Friday, January 29, 2016 2:35 PM > To: çæç; cl-isabelle-users at lists.cam.ac.uk > Subject: Re: [isabelle] Induction principle for datatypes > > Dear Shuling, > > What version of Isabelle are you using? > > As of Isabelle2015, the induction rule should produce the induction hypothesis > "!!x. x : > set list ==> PP x". If you are using an older version of Isabelle (or you have called > "datatype_compat comm" to get the old-style induction rule), the recursion > through list in the datatype definition is translated to a mutual recursion with a > specialised version of list. Thus, you'd have to state and prove a simultaneous > mutual induction statement, i.e., > > lemma "PP a" and "QQ as" > proof(induct a and as) > > In the inductive step for Cond, you then get QQ list as the induction hypothesis > for the arguments, i.e., QQ has to summarise the inductive statement for lists. > In general, QQ as = (\<forall>a\<in>set as. PP a) should work. > > 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 > >

**References**:**[isabelle] Induction principle for datatypes***From:*çæç

**Re: [isabelle] Induction principle for datatypes***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Induction principle for datatypes
- Next by Date: [isabelle] Funded Doctoral Positions in Computer Science in Austria (LogiCS)
- Previous by Thread: Re: [isabelle] Induction principle for datatypes
- Next by Thread: [isabelle] Funded Doctoral Positions in Computer Science in Austria (LogiCS)
- 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