Re: [isabelle] Set induction and pair datatype



Hi Peter,

if you look in the original TransitiveClosure theory of HOL, you also
find an extra rule for pairs.
However, you do not have to prove the induction rule by hand, but you
can have Isabelle generate it for you:

In TransitiveClosure.thy:
lemmas rtrancl_induct2 =
rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
consumes 1, case_names refl step]

So, your trcl_pair_induct could be written as
lemmas trcl_pair_induct =
trcl_induct[of "(xc1,xc2)" "xb" "(xa1,xa2)", split_format (complete),
consumes 1, case names empty cons]

Induction over inductive sets where the element to be in the set in the
premises is not of the most general form is always a problem because
induct discards everything like pairs, a fixed parameter and the like.

An alternative would be to reformulate the lemma you want to prove, but
this is very tedious if you have to do it multiple times.

lemma preserves_cl: "[| (c,w,c') : trcl T; c = (a, b); c' = (a', b') |]
     \<Longrightarrow> Prop a b \<Longrightarrow> Prop a' b'"


Regards,
Andreas


>>-- "Defining transitive closure of labeled transition system as
>>inductive set"
>>types ('c,'a) LTS = "('c \<times> 'a \<times> 'c) set"
>>
>>text {* Transitive closure of LTS *}
>>consts trcl :: "('c,'a) LTS \<Rightarrow> ('c,'a list) LTS"
>>
>>inductive "trcl t"
>>intros
>>  empty[simp]: "(c,[],c) \<in> trcl t"
>>  cons[simp]: "\<lbrakk> (c,a,c') \<in> t; (c',w,c'') \<in> trcl t
>>\<rbrakk> \<Longrightarrow> (c,a#w,c'') \<in> trcl t"
>>
>>
>>
>>lemma preserves_cl: "((a,b),w,(a',b'))\<in>trcl T \<Longrightarrow> Prop
>>a b \<Longrightarrow> Prop a' b'"
>>  apply (induct rule: trcl.induct)
>>  oops
>>  This did not get the induction correctly, there are the following
>>subgoals:
>>    1. \<And>c. Prop a b \<Longrightarrow> Prop a' b'
>>    2. \<And>aa c c' c'' w. \<lbrakk>(c, aa, c') \<in> T; (c', w, c'')
>>\<in> trcl T; Prop a b \<Longrightarrow> Prop a' b'; Prop a b\<rbrakk>
>>\<Longrightarrow> Prop a' b'
>>  the first one is obviously not provable
>>
>>What can I do about this ? Currently I'm working around by providing a
>>specialized induction rule for pairs:
>>lemma trcl_pair_induct[induct set]:
>>  "\<lbrakk>((xc1,xc2), xb, (xa1,xa2)) \<in> trcl t; \<And>c1 c2. P c1
>>c2 [] c1 c2; \<And>a c1 c2 c1' c2' c1'' c2'' w. \<lbrakk>((c1,c2), a,
>>(c1',c2')) \<in> t; ((c1',c2'), w, (c1'',c2'')) \<in> trcl t; P c1' c2'
>>w c1'' c2''\<rbrakk> \<Longrightarrow> P c1 c2 (a # w) c1'' c2''\<rbrakk>
>>  \<Longrightarrow> P xc1 xc2 xb xa1 xa2"
>>  using trcl.induct[of "(xc1,xc2)" xb "(xa1,xa2)" t "\<lambda>c w c'.
>>let (c1,c2)=c in let (c1',c2')=c' in P c1 c2 w c1' c2'"] by auto
>>
>>Is this the way to go, or is there another (nicer) possibility, i.e. one
>>generic scheme that can handle pairs, triples and so on
>>
>>Many thanks in advance, yours
>>Peter
>>  
>>
>  
>







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