[isabelle] Induction principle for datatypes



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.