# [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)
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

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