*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Set induction and pair datatype*From*: Andreas Lochbihler <lochbihl at infosun.fim.uni-passau.de>*Date*: Thu, 13 Sep 2007 07:38:06 +0200*In-reply-to*: <mailman.3.1189566002.2562.cl-isabelle-users@lists.cam.ac.uk>*References*: <mailman.3.1189566002.2562.cl-isabelle-users@lists.cam.ac.uk>*Reply-to*: lochbihl at fim.uni-passau.de*User-agent*: Mozilla Thunderbird 1.0.8-1.1.fc4 (X11/20060501)

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 >> >> > >

- Previous by Date: [isabelle] Set induction and pair datatype
- Next by Date: [isabelle] small verification task
- Previous by Thread: [isabelle] Set induction and pair datatype
- Next by Thread: [isabelle] small verification task
- Cl-isabelle-users September 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list