Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Induction principle for datatypes


view this post on Zulip Email Gateway (Aug 22 2022 at 12:21):

From: 王淑灵 <wangsl@ios.ac.cn>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 12:21):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 12:21):

From: 王淑灵 <wangsl@ios.ac.cn>
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


Last updated: Mar 29 2024 at 01:04 UTC