[isabelle] Set induction and pair datatype



I have the following problem with set induction and pair datatypes,
illustrated in the pice of code below:

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

-- "Now do some very simple inductive proof, using trcl.induct"
consts T':: "(nat \<times> bool \<times> nat) set"
consts Prop':: "nat \<Rightarrow> bool"

lemma preserves': "(a,e,a')\<in>T' \<Longrightarrow> Prop' a
\<Longrightarrow> Prop' a'" sorry

lemma preserves_trcl': "(a,w,a')\<in>trcl T' \<Longrightarrow> Prop' a
\<Longrightarrow> Prop' a'"
  apply (induct rule: trcl.induct)
  apply (auto simp add: preserves')
done
-- "Ok, this works fine !"

-- "Now we want to do the same for states that are pairs: "
consts T:: "((nat \<times> nat) \<times> bool \<times> (nat \<times>
nat)) set"
consts Prop:: "nat \<Rightarrow> nat \<Rightarrow> bool"

lemma preserves: "((a,b),e,(a',b'))\<in>T \<Longrightarrow> Prop a b
\<Longrightarrow> Prop a' b'" sorry

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.