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.