51 |
51 |
52 lemma rtran_closure_mem_type [TC]: |
52 lemma rtran_closure_mem_type [TC]: |
53 "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> rtran_closure_mem_fm(x,y,z) \<in> formula" |
53 "[| x \<in> nat; y \<in> nat; z \<in> nat |] ==> rtran_closure_mem_fm(x,y,z) \<in> formula" |
54 by (simp add: rtran_closure_mem_fm_def) |
54 by (simp add: rtran_closure_mem_fm_def) |
55 |
55 |
56 lemma arity_rtran_closure_mem_fm [simp]: |
|
57 "[| x \<in> nat; y \<in> nat; z \<in> nat |] |
|
58 ==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" |
|
59 by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac) |
|
60 |
|
61 lemma sats_rtran_closure_mem_fm [simp]: |
56 lemma sats_rtran_closure_mem_fm [simp]: |
62 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
57 "[| x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)|] |
63 ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <-> |
58 ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <-> |
64 rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))" |
59 rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))" |
65 by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def) |
60 by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def) |
101 |
96 |
102 lemma rtran_closure_type [TC]: |
97 lemma rtran_closure_type [TC]: |
103 "[| x \<in> nat; y \<in> nat |] ==> rtran_closure_fm(x,y) \<in> formula" |
98 "[| x \<in> nat; y \<in> nat |] ==> rtran_closure_fm(x,y) \<in> formula" |
104 by (simp add: rtran_closure_fm_def) |
99 by (simp add: rtran_closure_fm_def) |
105 |
100 |
106 lemma arity_rtran_closure_fm [simp]: |
|
107 "[| x \<in> nat; y \<in> nat |] |
|
108 ==> arity(rtran_closure_fm(x,y)) = succ(x) \<union> succ(y)" |
|
109 by (simp add: rtran_closure_fm_def succ_Un_distrib [symmetric] Un_ac) |
|
110 |
|
111 lemma sats_rtran_closure_fm [simp]: |
101 lemma sats_rtran_closure_fm [simp]: |
112 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
102 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
113 ==> sats(A, rtran_closure_fm(x,y), env) <-> |
103 ==> sats(A, rtran_closure_fm(x,y), env) <-> |
114 rtran_closure(**A, nth(x,env), nth(y,env))" |
104 rtran_closure(**A, nth(x,env), nth(y,env))" |
115 by (simp add: rtran_closure_fm_def rtran_closure_def) |
105 by (simp add: rtran_closure_fm_def rtran_closure_def) |
137 Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))" |
127 Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))" |
138 |
128 |
139 lemma tran_closure_type [TC]: |
129 lemma tran_closure_type [TC]: |
140 "[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula" |
130 "[| x \<in> nat; y \<in> nat |] ==> tran_closure_fm(x,y) \<in> formula" |
141 by (simp add: tran_closure_fm_def) |
131 by (simp add: tran_closure_fm_def) |
142 |
|
143 lemma arity_tran_closure_fm [simp]: |
|
144 "[| x \<in> nat; y \<in> nat |] |
|
145 ==> arity(tran_closure_fm(x,y)) = succ(x) \<union> succ(y)" |
|
146 by (simp add: tran_closure_fm_def succ_Un_distrib [symmetric] Un_ac) |
|
147 |
132 |
148 lemma sats_tran_closure_fm [simp]: |
133 lemma sats_tran_closure_fm [simp]: |
149 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
134 "[| x \<in> nat; y \<in> nat; env \<in> list(A)|] |
150 ==> sats(A, tran_closure_fm(x,y), env) <-> |
135 ==> sats(A, tran_closure_fm(x,y), env) <-> |
151 tran_closure(**A, nth(x,env), nth(y,env))" |
136 tran_closure(**A, nth(x,env), nth(y,env))" |