Re: [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
> >



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