author  paulson 
Fri, 16 Aug 2002 16:41:48 +0200  
changeset 13505  52a16cb7fefb 
parent 13496  6f0c57def6d5 
child 13506  acc18a5d2b1a 
permissions  rwrr 
13505  1 
(* Title: ZF/Constructible/L_axioms.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 2002 University of Cambridge 

5 
*) 

13429  6 

7 
header {* The ZF Axioms (Except Separation) in L *} 

13223  8 

13314  9 
theory L_axioms = Formula + Relative + Reflection + MetaExists: 
13223  10 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

11 
text {* The class L satisfies the premises of locale @{text M_triv_axioms} *} 
13223  12 

13 
lemma transL: "[ y\<in>x; L(x) ] ==> L(y)" 

13429  14 
apply (insert Transset_Lset) 
15 
apply (simp add: Transset_def L_def, blast) 

13223  16 
done 
17 

18 
lemma nonempty: "L(0)" 

13429  19 
apply (simp add: L_def) 
20 
apply (blast intro: zero_in_Lset) 

13223  21 
done 
22 

23 
lemma upair_ax: "upair_ax(L)" 

24 
apply (simp add: upair_ax_def upair_def, clarify) 

13429  25 
apply (rule_tac x="{x,y}" in rexI) 
26 
apply (simp_all add: doubleton_in_L) 

13223  27 
done 
28 

29 
lemma Union_ax: "Union_ax(L)" 

30 
apply (simp add: Union_ax_def big_union_def, clarify) 

13429  31 
apply (rule_tac x="Union(x)" in rexI) 
32 
apply (simp_all add: Union_in_L, auto) 

33 
apply (blast intro: transL) 

13223  34 
done 
35 

36 
lemma power_ax: "power_ax(L)" 

37 
apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify) 

13429  38 
apply (rule_tac x="{y \<in> Pow(x). L(y)}" in rexI) 
13299  39 
apply (simp_all add: LPow_in_L, auto) 
13429  40 
apply (blast intro: transL) 
13223  41 
done 
42 

43 
subsubsection{*For L to satisfy Replacement *} 

44 

45 
(*Can't move these to Formula unless the definition of univalent is moved 

46 
there too!*) 

47 

48 
lemma LReplace_in_Lset: 

13429  49 
"[X \<in> Lset(i); univalent(L,X,Q); Ord(i)] 
13223  50 
==> \<exists>j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Lset(j)" 
13429  51 
apply (rule_tac x="\<Union>y \<in> Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))" 
13223  52 
in exI) 
53 
apply simp 

13429  54 
apply clarify 
55 
apply (rule_tac a=x in UN_I) 

56 
apply (simp_all add: Replace_iff univalent_def) 

57 
apply (blast dest: transL L_I) 

13223  58 
done 
59 

13429  60 
lemma LReplace_in_L: 
61 
"[L(X); univalent(L,X,Q)] 

13223  62 
==> \<exists>Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Y" 
13429  63 
apply (drule L_D, clarify) 
13223  64 
apply (drule LReplace_in_Lset, assumption+) 
65 
apply (blast intro: L_I Lset_in_Lset_succ) 

66 
done 

67 

68 
lemma replacement: "replacement(L,P)" 

69 
apply (simp add: replacement_def, clarify) 

13429  70 
apply (frule LReplace_in_L, assumption+, clarify) 
71 
apply (rule_tac x=Y in rexI) 

72 
apply (simp_all add: Replace_iff univalent_def, blast) 

13223  73 
done 
74 

13363  75 
subsection{*Instantiating the locale @{text M_triv_axioms}*} 
76 
text{*No instances of Separation yet.*} 

13291  77 

78 
lemma Lset_mono_le: "mono_le_subset(Lset)" 

13429  79 
by (simp add: mono_le_subset_def le_imp_subset Lset_mono) 
13291  80 

81 
lemma Lset_cont: "cont_Ord(Lset)" 

13429  82 
by (simp add: cont_Ord_def Limit_Lset_eq OUnion_def Limit_is_Ord) 
13291  83 

13428  84 
lemmas Pair_in_Lset = Formula.Pair_in_LLimit 
13291  85 

13428  86 
lemmas L_nat = Ord_in_L [OF Ord_nat] 
13291  87 

13428  88 
theorem M_triv_axioms_L: "PROP M_triv_axioms(L)" 
89 
apply (rule M_triv_axioms.intro) 

90 
apply (erule (1) transL) 

91 
apply (rule nonempty) 

92 
apply (rule upair_ax) 

93 
apply (rule Union_ax) 

94 
apply (rule power_ax) 

95 
apply (rule replacement) 

96 
apply (rule L_nat) 

97 
done 

13291  98 

13429  99 
lemmas rall_abs = M_triv_axioms.rall_abs [OF M_triv_axioms_L] 
100 
and rex_abs = M_triv_axioms.rex_abs [OF M_triv_axioms_L] 

13428  101 
and ball_iff_equiv = M_triv_axioms.ball_iff_equiv [OF M_triv_axioms_L] 
102 
and M_equalityI = M_triv_axioms.M_equalityI [OF M_triv_axioms_L] 

13429  103 
and empty_abs = M_triv_axioms.empty_abs [OF M_triv_axioms_L] 
104 
and subset_abs = M_triv_axioms.subset_abs [OF M_triv_axioms_L] 

105 
and upair_abs = M_triv_axioms.upair_abs [OF M_triv_axioms_L] 

106 
and upair_in_M_iff = M_triv_axioms.upair_in_M_iff [OF M_triv_axioms_L] 

107 
and singleton_in_M_iff = M_triv_axioms.singleton_in_M_iff [OF M_triv_axioms_L] 

108 
and pair_abs = M_triv_axioms.pair_abs [OF M_triv_axioms_L] 

109 
and pair_in_M_iff = M_triv_axioms.pair_in_M_iff [OF M_triv_axioms_L] 

13428  110 
and pair_components_in_M = M_triv_axioms.pair_components_in_M [OF M_triv_axioms_L] 
13429  111 
and cartprod_abs = M_triv_axioms.cartprod_abs [OF M_triv_axioms_L] 
112 
and union_abs = M_triv_axioms.union_abs [OF M_triv_axioms_L] 

113 
and inter_abs = M_triv_axioms.inter_abs [OF M_triv_axioms_L] 

114 
and setdiff_abs = M_triv_axioms.setdiff_abs [OF M_triv_axioms_L] 

115 
and Union_abs = M_triv_axioms.Union_abs [OF M_triv_axioms_L] 

116 
and Union_closed = M_triv_axioms.Union_closed [OF M_triv_axioms_L] 

117 
and Un_closed = M_triv_axioms.Un_closed [OF M_triv_axioms_L] 

118 
and cons_closed = M_triv_axioms.cons_closed [OF M_triv_axioms_L] 

119 
and successor_abs = M_triv_axioms.successor_abs [OF M_triv_axioms_L] 

120 
and succ_in_M_iff = M_triv_axioms.succ_in_M_iff [OF M_triv_axioms_L] 

121 
and separation_closed = M_triv_axioms.separation_closed [OF M_triv_axioms_L] 

13428  122 
and strong_replacementI = M_triv_axioms.strong_replacementI [OF M_triv_axioms_L] 
13429  123 
and strong_replacement_closed = M_triv_axioms.strong_replacement_closed [OF M_triv_axioms_L] 
124 
and RepFun_closed = M_triv_axioms.RepFun_closed [OF M_triv_axioms_L] 

125 
and lam_closed = M_triv_axioms.lam_closed [OF M_triv_axioms_L] 

126 
and image_abs = M_triv_axioms.image_abs [OF M_triv_axioms_L] 

13428  127 
and powerset_Pow = M_triv_axioms.powerset_Pow [OF M_triv_axioms_L] 
128 
and powerset_imp_subset_Pow = M_triv_axioms.powerset_imp_subset_Pow [OF M_triv_axioms_L] 

13429  129 
and nat_into_M = M_triv_axioms.nat_into_M [OF M_triv_axioms_L] 
13428  130 
and nat_case_closed = M_triv_axioms.nat_case_closed [OF M_triv_axioms_L] 
13429  131 
and Inl_in_M_iff = M_triv_axioms.Inl_in_M_iff [OF M_triv_axioms_L] 
132 
and Inr_in_M_iff = M_triv_axioms.Inr_in_M_iff [OF M_triv_axioms_L] 

13428  133 
and lt_closed = M_triv_axioms.lt_closed [OF M_triv_axioms_L] 
13429  134 
and transitive_set_abs = M_triv_axioms.transitive_set_abs [OF M_triv_axioms_L] 
135 
and ordinal_abs = M_triv_axioms.ordinal_abs [OF M_triv_axioms_L] 

136 
and limit_ordinal_abs = M_triv_axioms.limit_ordinal_abs [OF M_triv_axioms_L] 

137 
and successor_ordinal_abs = M_triv_axioms.successor_ordinal_abs [OF M_triv_axioms_L] 

13428  138 
and finite_ordinal_abs = M_triv_axioms.finite_ordinal_abs [OF M_triv_axioms_L] 
13429  139 
and omega_abs = M_triv_axioms.omega_abs [OF M_triv_axioms_L] 
140 
and number1_abs = M_triv_axioms.number1_abs [OF M_triv_axioms_L] 

141 
and number2_abs = M_triv_axioms.number2_abs [OF M_triv_axioms_L] 

142 
and number3_abs = M_triv_axioms.number3_abs [OF M_triv_axioms_L] 

143 

144 
declare rall_abs [simp] 

145 
declare rex_abs [simp] 

146 
declare empty_abs [simp] 

147 
declare subset_abs [simp] 

148 
declare upair_abs [simp] 

149 
declare upair_in_M_iff [iff] 

150 
declare singleton_in_M_iff [iff] 

151 
declare pair_abs [simp] 

152 
declare pair_in_M_iff [iff] 

153 
declare cartprod_abs [simp] 

154 
declare union_abs [simp] 

155 
declare inter_abs [simp] 

156 
declare setdiff_abs [simp] 

157 
declare Union_abs [simp] 

158 
declare Union_closed [intro, simp] 

159 
declare Un_closed [intro, simp] 

160 
declare cons_closed [intro, simp] 

161 
declare successor_abs [simp] 

162 
declare succ_in_M_iff [iff] 

163 
declare separation_closed [intro, simp] 

164 
declare strong_replacementI 

165 
declare strong_replacement_closed [intro, simp] 

166 
declare RepFun_closed [intro, simp] 

167 
declare lam_closed [intro, simp] 

168 
declare image_abs [simp] 

169 
declare nat_into_M [intro] 

170 
declare Inl_in_M_iff [iff] 

171 
declare Inr_in_M_iff [iff] 

172 
declare transitive_set_abs [simp] 

173 
declare ordinal_abs [simp] 

174 
declare limit_ordinal_abs [simp] 

175 
declare successor_ordinal_abs [simp] 

176 
declare finite_ordinal_abs [simp] 

177 
declare omega_abs [simp] 

178 
declare number1_abs [simp] 

179 
declare number2_abs [simp] 

180 
declare number3_abs [simp] 

13291  181 

182 

183 
subsection{*Instantiation of the locale @{text reflection}*} 

184 

185 
text{*instances of locale constants*} 

186 
constdefs 

187 
L_F0 :: "[i=>o,i] => i" 

188 
"L_F0(P,y) == \<mu>b. (\<exists>z. L(z) \<and> P(<y,z>)) > (\<exists>z\<in>Lset(b). P(<y,z>))" 

189 

190 
L_FF :: "[i=>o,i] => i" 

191 
"L_FF(P) == \<lambda>a. \<Union>y\<in>Lset(a). L_F0(P,y)" 

192 

193 
L_ClEx :: "[i=>o,i] => o" 

194 
"L_ClEx(P) == \<lambda>a. Limit(a) \<and> normalize(L_FF(P),a) = a" 

195 

196 

13314  197 
text{*We must use the metaexistential quantifier; otherwise the reflection 
13429  198 
terms become enormous!*} 
13314  199 
constdefs 
200 
L_Reflects :: "[i=>o,[i,i]=>o] => prop" ("(3REFLECTS/ [_,/ _])") 

201 
"REFLECTS[P,Q] == (??Cl. Closed_Unbounded(Cl) & 

202 
(\<forall>a. Cl(a) > (\<forall>x \<in> Lset(a). P(x) <> Q(a,x))))" 

13291  203 

204 

13314  205 
theorem Triv_reflection: 
206 
"REFLECTS[P, \<lambda>a x. P(x)]" 

13429  207 
apply (simp add: L_Reflects_def) 
208 
apply (rule meta_exI) 

209 
apply (rule Closed_Unbounded_Ord) 

13314  210 
done 
211 

212 
theorem Not_reflection: 

213 
"REFLECTS[P,Q] ==> REFLECTS[\<lambda>x. ~P(x), \<lambda>a x. ~Q(a,x)]" 

13429  214 
apply (unfold L_Reflects_def) 
215 
apply (erule meta_exE) 

216 
apply (rule_tac x=Cl in meta_exI, simp) 

13314  217 
done 
218 

219 
theorem And_reflection: 

13429  220 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ] 
13314  221 
==> REFLECTS[\<lambda>x. P(x) \<and> P'(x), \<lambda>a x. Q(a,x) \<and> Q'(a,x)]" 
13429  222 
apply (unfold L_Reflects_def) 
223 
apply (elim meta_exE) 

224 
apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI) 

225 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  226 
done 
227 

228 
theorem Or_reflection: 

13429  229 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ] 
13314  230 
==> REFLECTS[\<lambda>x. P(x) \<or> P'(x), \<lambda>a x. Q(a,x) \<or> Q'(a,x)]" 
13429  231 
apply (unfold L_Reflects_def) 
232 
apply (elim meta_exE) 

233 
apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI) 

234 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  235 
done 
236 

237 
theorem Imp_reflection: 

13429  238 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ] 
13314  239 
==> REFLECTS[\<lambda>x. P(x) > P'(x), \<lambda>a x. Q(a,x) > Q'(a,x)]" 
13429  240 
apply (unfold L_Reflects_def) 
241 
apply (elim meta_exE) 

242 
apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI) 

243 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  244 
done 
245 

246 
theorem Iff_reflection: 

13429  247 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ] 
13314  248 
==> REFLECTS[\<lambda>x. P(x) <> P'(x), \<lambda>a x. Q(a,x) <> Q'(a,x)]" 
13429  249 
apply (unfold L_Reflects_def) 
250 
apply (elim meta_exE) 

251 
apply (rule_tac x="\<lambda>a. Cl(a) \<and> Cla(a)" in meta_exI) 

252 
apply (simp add: Closed_Unbounded_Int, blast) 

13314  253 
done 
254 

255 

13434  256 
lemma reflection_Lset: "reflection(Lset)" 
257 
apply (blast intro: reflection.intro Lset_mono_le Lset_cont Pair_in_Lset) + 

258 
done 

259 

13314  260 
theorem Ex_reflection: 
261 
"REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] 

262 
==> REFLECTS[\<lambda>x. \<exists>z. L(z) \<and> P(x,z), \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z)]" 

13429  263 
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) 
264 
apply (elim meta_exE) 

13314  265 
apply (rule meta_exI) 
13434  266 
apply (erule reflection.Ex_reflection [OF reflection_Lset]) 
13291  267 
done 
268 

13314  269 
theorem All_reflection: 
270 
"REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] 

13429  271 
==> REFLECTS[\<lambda>x. \<forall>z. L(z) > P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]" 
272 
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) 

273 
apply (elim meta_exE) 

13314  274 
apply (rule meta_exI) 
13434  275 
apply (erule reflection.All_reflection [OF reflection_Lset]) 
13291  276 
done 
277 

13314  278 
theorem Rex_reflection: 
279 
"REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] 

280 
==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z\<in>Lset(a). Q(a,x,z)]" 

13429  281 
apply (unfold rex_def) 
13314  282 
apply (intro And_reflection Ex_reflection, assumption) 
283 
done 

13291  284 

13314  285 
theorem Rall_reflection: 
286 
"REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] 

13429  287 
==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z\<in>Lset(a). Q(a,x,z)]" 
288 
apply (unfold rall_def) 

13314  289 
apply (intro Imp_reflection All_reflection, assumption) 
290 
done 

291 

13440  292 
text{*This version handles an alternative form of the bounded quantifier 
293 
in the second argument of @{text REFLECTS}.*} 

294 
theorem Rex_reflection': 

295 
"REFLECTS[ \<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] 

296 
==> REFLECTS[\<lambda>x. \<exists>z[L]. P(x,z), \<lambda>a x. \<exists>z[**Lset(a)]. Q(a,x,z)]" 

297 
apply (unfold setclass_def rex_def) 

298 
apply (erule Rex_reflection [unfolded rex_def Bex_def]) 

299 
done 

300 

301 
text{*As above.*} 

302 
theorem Rall_reflection': 

303 
"REFLECTS[\<lambda>x. P(fst(x),snd(x)), \<lambda>a x. Q(a,fst(x),snd(x))] 

304 
==> REFLECTS[\<lambda>x. \<forall>z[L]. P(x,z), \<lambda>a x. \<forall>z[**Lset(a)]. Q(a,x,z)]" 

305 
apply (unfold setclass_def rall_def) 

306 
apply (erule Rall_reflection [unfolded rall_def Ball_def]) 

307 
done 

308 

13429  309 
lemmas FOL_reflections = 
13314  310 
Triv_reflection Not_reflection And_reflection Or_reflection 
311 
Imp_reflection Iff_reflection Ex_reflection All_reflection 

13440  312 
Rex_reflection Rall_reflection Rex_reflection' Rall_reflection' 
13291  313 

314 
lemma ReflectsD: 

13429  315 
"[REFLECTS[P,Q]; Ord(i)] 
13291  316 
==> \<exists>j. i<j & (\<forall>x \<in> Lset(j). P(x) <> Q(j,x))" 
13429  317 
apply (unfold L_Reflects_def Closed_Unbounded_def) 
318 
apply (elim meta_exE, clarify) 

319 
apply (blast dest!: UnboundedD) 

13291  320 
done 
321 

322 
lemma ReflectsE: 

13314  323 
"[ REFLECTS[P,Q]; Ord(i); 
13291  324 
!!j. [i<j; \<forall>x \<in> Lset(j). P(x) <> Q(j,x)] ==> R ] 
325 
==> R" 

13429  326 
apply (drule ReflectsD, assumption, blast) 
13314  327 
done 
13291  328 

13428  329 
lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B" 
13291  330 
by blast 
331 

332 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

333 
subsection{*Internalized Formulas for some SetTheoretic Concepts*} 
13298  334 

13306  335 
lemmas setclass_simps = rall_setclass_is_ball rex_setclass_is_bex 
336 

337 
subsubsection{*Some numbers to help write de Bruijn indices*} 

338 

339 
syntax 

340 
"3" :: i ("3") 

341 
"4" :: i ("4") 

342 
"5" :: i ("5") 

343 
"6" :: i ("6") 

344 
"7" :: i ("7") 

345 
"8" :: i ("8") 

346 
"9" :: i ("9") 

347 

348 
translations 

349 
"3" == "succ(2)" 

350 
"4" == "succ(3)" 

351 
"5" == "succ(4)" 

352 
"6" == "succ(5)" 

353 
"7" == "succ(6)" 

354 
"8" == "succ(7)" 

355 
"9" == "succ(8)" 

356 

13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

357 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

358 
subsubsection{*The Empty Set, Internalized*} 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

359 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

360 
constdefs empty_fm :: "i=>i" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

361 
"empty_fm(x) == Forall(Neg(Member(0,succ(x))))" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

362 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

363 
lemma empty_type [TC]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

364 
"x \<in> nat ==> empty_fm(x) \<in> formula" 
13429  365 
by (simp add: empty_fm_def) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

366 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

367 
lemma arity_empty_fm [simp]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

368 
"x \<in> nat ==> arity(empty_fm(x)) = succ(x)" 
13429  369 
by (simp add: empty_fm_def succ_Un_distrib [symmetric] Un_ac) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

370 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

371 
lemma sats_empty_fm [simp]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

372 
"[ x \<in> nat; env \<in> list(A)] 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

373 
==> sats(A, empty_fm(x), env) <> empty(**A, nth(x,env))" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

374 
by (simp add: empty_fm_def empty_def) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

375 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

376 
lemma empty_iff_sats: 
13429  377 
"[ nth(i,env) = x; nth(j,env) = y; 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

378 
i \<in> nat; env \<in> list(A)] 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

379 
==> empty(**A, x) <> sats(A, empty_fm(i), env)" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

380 
by simp 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

381 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

382 
theorem empty_reflection: 
13429  383 
"REFLECTS[\<lambda>x. empty(L,f(x)), 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

384 
\<lambda>i x. empty(**Lset(i),f(x))]" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

385 
apply (simp only: empty_def setclass_simps) 
13429  386 
apply (intro FOL_reflections) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

387 
done 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

388 

13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset

389 
text{*Not used. But maybe useful?*} 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset

390 
lemma Transset_sats_empty_fm_eq_0: 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset

391 
"[ n \<in> nat; env \<in> list(A); Transset(A)] 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset

392 
==> sats(A, empty_fm(n), env) <> nth(n,env) = 0" 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset

393 
apply (simp add: empty_fm_def empty_def Transset_def, auto) 
13429  394 
apply (case_tac "n < length(env)") 
395 
apply (frule nth_type, assumption+, blast) 

396 
apply (simp_all add: not_lt_iff_le nth_eq_0) 

13385
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset

397 
done 
31df66ca0780
Expressing Lset and L without using length and arity; simplifies Separation
paulson
parents:
13363
diff
changeset

398 

13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

399 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

400 
subsubsection{*Unordered Pairs, Internalized*} 
13298  401 

402 
constdefs upair_fm :: "[i,i,i]=>i" 

13429  403 
"upair_fm(x,y,z) == 
404 
And(Member(x,z), 

13298  405 
And(Member(y,z), 
13429  406 
Forall(Implies(Member(0,succ(z)), 
13298  407 
Or(Equal(0,succ(x)), Equal(0,succ(y)))))))" 
408 

409 
lemma upair_type [TC]: 

410 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> upair_fm(x,y,z) \<in> formula" 

13429  411 
by (simp add: upair_fm_def) 
13298  412 

413 
lemma arity_upair_fm [simp]: 

13429  414 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13298  415 
==> arity(upair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  416 
by (simp add: upair_fm_def succ_Un_distrib [symmetric] Un_ac) 
13298  417 

418 
lemma sats_upair_fm [simp]: 

419 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  420 
==> sats(A, upair_fm(x,y,z), env) <> 
13298  421 
upair(**A, nth(x,env), nth(y,env), nth(z,env))" 
422 
by (simp add: upair_fm_def upair_def) 

423 

424 
lemma upair_iff_sats: 

13429  425 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13298  426 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
427 
==> upair(**A, x, y, z) <> sats(A, upair_fm(i,j,k), env)" 

428 
by (simp add: sats_upair_fm) 

429 

430 
text{*Useful? At least it refers to "real" unordered pairs*} 

431 
lemma sats_upair_fm2 [simp]: 

432 
"[ x \<in> nat; y \<in> nat; z < length(env); env \<in> list(A); Transset(A)] 

13429  433 
==> sats(A, upair_fm(x,y,z), env) <> 
13298  434 
nth(z,env) = {nth(x,env), nth(y,env)}" 
13429  435 
apply (frule lt_length_in_nat, assumption) 
436 
apply (simp add: upair_fm_def Transset_def, auto) 

437 
apply (blast intro: nth_type) 

13298  438 
done 
439 

13314  440 
theorem upair_reflection: 
13429  441 
"REFLECTS[\<lambda>x. upair(L,f(x),g(x),h(x)), 
442 
\<lambda>i x. upair(**Lset(i),f(x),g(x),h(x))]" 

13314  443 
apply (simp add: upair_def) 
13429  444 
apply (intro FOL_reflections) 
13314  445 
done 
13306  446 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

447 
subsubsection{*Ordered pairs, Internalized*} 
13298  448 

449 
constdefs pair_fm :: "[i,i,i]=>i" 

13429  450 
"pair_fm(x,y,z) == 
13298  451 
Exists(And(upair_fm(succ(x),succ(x),0), 
452 
Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0), 

453 
upair_fm(1,0,succ(succ(z)))))))" 

454 

455 
lemma pair_type [TC]: 

456 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> pair_fm(x,y,z) \<in> formula" 

13429  457 
by (simp add: pair_fm_def) 
13298  458 

459 
lemma arity_pair_fm [simp]: 

13429  460 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13298  461 
==> arity(pair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  462 
by (simp add: pair_fm_def succ_Un_distrib [symmetric] Un_ac) 
13298  463 

464 
lemma sats_pair_fm [simp]: 

465 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  466 
==> sats(A, pair_fm(x,y,z), env) <> 
13298  467 
pair(**A, nth(x,env), nth(y,env), nth(z,env))" 
468 
by (simp add: pair_fm_def pair_def) 

469 

470 
lemma pair_iff_sats: 

13429  471 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13298  472 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
473 
==> pair(**A, x, y, z) <> sats(A, pair_fm(i,j,k), env)" 

474 
by (simp add: sats_pair_fm) 

475 

13314  476 
theorem pair_reflection: 
13429  477 
"REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)), 
13314  478 
\<lambda>i x. pair(**Lset(i),f(x),g(x),h(x))]" 
479 
apply (simp only: pair_def setclass_simps) 

13429  480 
apply (intro FOL_reflections upair_reflection) 
13314  481 
done 
13306  482 

483 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

484 
subsubsection{*Binary Unions, Internalized*} 
13298  485 

13306  486 
constdefs union_fm :: "[i,i,i]=>i" 
13429  487 
"union_fm(x,y,z) == 
13306  488 
Forall(Iff(Member(0,succ(z)), 
489 
Or(Member(0,succ(x)),Member(0,succ(y)))))" 

490 

491 
lemma union_type [TC]: 

492 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> union_fm(x,y,z) \<in> formula" 

13429  493 
by (simp add: union_fm_def) 
13306  494 

495 
lemma arity_union_fm [simp]: 

13429  496 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13306  497 
==> arity(union_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  498 
by (simp add: union_fm_def succ_Un_distrib [symmetric] Un_ac) 
13298  499 

13306  500 
lemma sats_union_fm [simp]: 
501 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  502 
==> sats(A, union_fm(x,y,z), env) <> 
13306  503 
union(**A, nth(x,env), nth(y,env), nth(z,env))" 
504 
by (simp add: union_fm_def union_def) 

505 

506 
lemma union_iff_sats: 

13429  507 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13306  508 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
509 
==> union(**A, x, y, z) <> sats(A, union_fm(i,j,k), env)" 

510 
by (simp add: sats_union_fm) 

13298  511 

13314  512 
theorem union_reflection: 
13429  513 
"REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)), 
13314  514 
\<lambda>i x. union(**Lset(i),f(x),g(x),h(x))]" 
515 
apply (simp only: union_def setclass_simps) 

13429  516 
apply (intro FOL_reflections) 
13314  517 
done 
13306  518 

13298  519 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

520 
subsubsection{*Set ``Cons,'' Internalized*} 
13306  521 

522 
constdefs cons_fm :: "[i,i,i]=>i" 

13429  523 
"cons_fm(x,y,z) == 
13306  524 
Exists(And(upair_fm(succ(x),succ(x),0), 
525 
union_fm(0,succ(y),succ(z))))" 

13298  526 

527 

13306  528 
lemma cons_type [TC]: 
529 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> cons_fm(x,y,z) \<in> formula" 

13429  530 
by (simp add: cons_fm_def) 
13306  531 

532 
lemma arity_cons_fm [simp]: 

13429  533 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13306  534 
==> arity(cons_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  535 
by (simp add: cons_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  536 

537 
lemma sats_cons_fm [simp]: 

538 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  539 
==> sats(A, cons_fm(x,y,z), env) <> 
13306  540 
is_cons(**A, nth(x,env), nth(y,env), nth(z,env))" 
541 
by (simp add: cons_fm_def is_cons_def) 

542 

543 
lemma cons_iff_sats: 

13429  544 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13306  545 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
546 
==> is_cons(**A, x, y, z) <> sats(A, cons_fm(i,j,k), env)" 

547 
by simp 

548 

13314  549 
theorem cons_reflection: 
13429  550 
"REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)), 
13314  551 
\<lambda>i x. is_cons(**Lset(i),f(x),g(x),h(x))]" 
552 
apply (simp only: is_cons_def setclass_simps) 

13429  553 
apply (intro FOL_reflections upair_reflection union_reflection) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

554 
done 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

555 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

556 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

557 
subsubsection{*Successor Function, Internalized*} 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

558 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

559 
constdefs succ_fm :: "[i,i]=>i" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

560 
"succ_fm(x,y) == cons_fm(x,x,y)" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

561 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

562 
lemma succ_type [TC]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

563 
"[ x \<in> nat; y \<in> nat ] ==> succ_fm(x,y) \<in> formula" 
13429  564 
by (simp add: succ_fm_def) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

565 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

566 
lemma arity_succ_fm [simp]: 
13429  567 
"[ x \<in> nat; y \<in> nat ] 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

568 
==> arity(succ_fm(x,y)) = succ(x) \<union> succ(y)" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

569 
by (simp add: succ_fm_def) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

570 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

571 
lemma sats_succ_fm [simp]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

572 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 
13429  573 
==> sats(A, succ_fm(x,y), env) <> 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

574 
successor(**A, nth(x,env), nth(y,env))" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

575 
by (simp add: succ_fm_def successor_def) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

576 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

577 
lemma successor_iff_sats: 
13429  578 
"[ nth(i,env) = x; nth(j,env) = y; 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

579 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

580 
==> successor(**A, x, y) <> sats(A, succ_fm(i,j), env)" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

581 
by simp 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

582 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

583 
theorem successor_reflection: 
13429  584 
"REFLECTS[\<lambda>x. successor(L,f(x),g(x)), 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

585 
\<lambda>i x. successor(**Lset(i),f(x),g(x))]" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

586 
apply (simp only: successor_def setclass_simps) 
13429  587 
apply (intro cons_reflection) 
13314  588 
done 
13298  589 

590 

13363  591 
subsubsection{*The Number 1, Internalized*} 
592 

593 
(* "number1(M,a) == (\<exists>x[M]. empty(M,x) & successor(M,x,a))" *) 

594 
constdefs number1_fm :: "i=>i" 

595 
"number1_fm(a) == Exists(And(empty_fm(0), succ_fm(0,succ(a))))" 

596 

597 
lemma number1_type [TC]: 

598 
"x \<in> nat ==> number1_fm(x) \<in> formula" 

13429  599 
by (simp add: number1_fm_def) 
13363  600 

601 
lemma arity_number1_fm [simp]: 

602 
"x \<in> nat ==> arity(number1_fm(x)) = succ(x)" 

13429  603 
by (simp add: number1_fm_def succ_Un_distrib [symmetric] Un_ac) 
13363  604 

605 
lemma sats_number1_fm [simp]: 

606 
"[ x \<in> nat; env \<in> list(A)] 

607 
==> sats(A, number1_fm(x), env) <> number1(**A, nth(x,env))" 

608 
by (simp add: number1_fm_def number1_def) 

609 

610 
lemma number1_iff_sats: 

13429  611 
"[ nth(i,env) = x; nth(j,env) = y; 
13363  612 
i \<in> nat; env \<in> list(A)] 
613 
==> number1(**A, x) <> sats(A, number1_fm(i), env)" 

614 
by simp 

615 

616 
theorem number1_reflection: 

13429  617 
"REFLECTS[\<lambda>x. number1(L,f(x)), 
13363  618 
\<lambda>i x. number1(**Lset(i),f(x))]" 
619 
apply (simp only: number1_def setclass_simps) 

620 
apply (intro FOL_reflections empty_reflection successor_reflection) 

621 
done 

622 

623 

13352  624 
subsubsection{*Big Union, Internalized*} 
13306  625 

13352  626 
(* "big_union(M,A,z) == \<forall>x[M]. x \<in> z <> (\<exists>y[M]. y\<in>A & x \<in> y)" *) 
627 
constdefs big_union_fm :: "[i,i]=>i" 

13429  628 
"big_union_fm(A,z) == 
13352  629 
Forall(Iff(Member(0,succ(z)), 
630 
Exists(And(Member(0,succ(succ(A))), Member(1,0)))))" 

13298  631 

13352  632 
lemma big_union_type [TC]: 
633 
"[ x \<in> nat; y \<in> nat ] ==> big_union_fm(x,y) \<in> formula" 

13429  634 
by (simp add: big_union_fm_def) 
13306  635 

13352  636 
lemma arity_big_union_fm [simp]: 
13429  637 
"[ x \<in> nat; y \<in> nat ] 
13352  638 
==> arity(big_union_fm(x,y)) = succ(x) \<union> succ(y)" 
639 
by (simp add: big_union_fm_def succ_Un_distrib [symmetric] Un_ac) 

13298  640 

13352  641 
lemma sats_big_union_fm [simp]: 
642 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 

13429  643 
==> sats(A, big_union_fm(x,y), env) <> 
13352  644 
big_union(**A, nth(x,env), nth(y,env))" 
645 
by (simp add: big_union_fm_def big_union_def) 

13306  646 

13352  647 
lemma big_union_iff_sats: 
13429  648 
"[ nth(i,env) = x; nth(j,env) = y; 
13352  649 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
650 
==> big_union(**A, x, y) <> sats(A, big_union_fm(i,j), env)" 

13306  651 
by simp 
652 

13352  653 
theorem big_union_reflection: 
13429  654 
"REFLECTS[\<lambda>x. big_union(L,f(x),g(x)), 
13352  655 
\<lambda>i x. big_union(**Lset(i),f(x),g(x))]" 
656 
apply (simp only: big_union_def setclass_simps) 

13429  657 
apply (intro FOL_reflections) 
13314  658 
done 
13298  659 

660 

13306  661 
subsubsection{*Variants of Satisfaction Definitions for Ordinals, etc.*} 
662 

663 
text{*Differs from the one in Formula by using "ordinal" rather than "Ord"*} 

664 

665 

666 
lemma sats_subset_fm': 

667 
"[x \<in> nat; y \<in> nat; env \<in> list(A)] 

13429  668 
==> sats(A, subset_fm(x,y), env) <> subset(**A, nth(x,env), nth(y,env))" 
669 
by (simp add: subset_fm_def Relative.subset_def) 

13298  670 

13314  671 
theorem subset_reflection: 
13429  672 
"REFLECTS[\<lambda>x. subset(L,f(x),g(x)), 
673 
\<lambda>i x. subset(**Lset(i),f(x),g(x))]" 

13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

674 
apply (simp only: Relative.subset_def setclass_simps) 
13429  675 
apply (intro FOL_reflections) 
13314  676 
done 
13306  677 

678 
lemma sats_transset_fm': 

679 
"[x \<in> nat; env \<in> list(A)] 

680 
==> sats(A, transset_fm(x), env) <> transitive_set(**A, nth(x,env))" 

13429  681 
by (simp add: sats_subset_fm' transset_fm_def transitive_set_def) 
13298  682 

13314  683 
theorem transitive_set_reflection: 
684 
"REFLECTS[\<lambda>x. transitive_set(L,f(x)), 

685 
\<lambda>i x. transitive_set(**Lset(i),f(x))]" 

686 
apply (simp only: transitive_set_def setclass_simps) 

13429  687 
apply (intro FOL_reflections subset_reflection) 
13314  688 
done 
13306  689 

690 
lemma sats_ordinal_fm': 

691 
"[x \<in> nat; env \<in> list(A)] 

692 
==> sats(A, ordinal_fm(x), env) <> ordinal(**A,nth(x,env))" 

693 
by (simp add: sats_transset_fm' ordinal_fm_def ordinal_def) 

694 

695 
lemma ordinal_iff_sats: 

696 
"[ nth(i,env) = x; i \<in> nat; env \<in> list(A)] 

697 
==> ordinal(**A, x) <> sats(A, ordinal_fm(i), env)" 

698 
by (simp add: sats_ordinal_fm') 

699 

13314  700 
theorem ordinal_reflection: 
701 
"REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(**Lset(i),f(x))]" 

702 
apply (simp only: ordinal_def setclass_simps) 

13429  703 
apply (intro FOL_reflections transitive_set_reflection) 
13314  704 
done 
13298  705 

706 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

707 
subsubsection{*Membership Relation, Internalized*} 
13298  708 

13306  709 
constdefs Memrel_fm :: "[i,i]=>i" 
13429  710 
"Memrel_fm(A,r) == 
13306  711 
Forall(Iff(Member(0,succ(r)), 
712 
Exists(And(Member(0,succ(succ(A))), 

713 
Exists(And(Member(0,succ(succ(succ(A)))), 

714 
And(Member(1,0), 

715 
pair_fm(1,0,2))))))))" 

716 

717 
lemma Memrel_type [TC]: 

718 
"[ x \<in> nat; y \<in> nat ] ==> Memrel_fm(x,y) \<in> formula" 

13429  719 
by (simp add: Memrel_fm_def) 
13298  720 

13306  721 
lemma arity_Memrel_fm [simp]: 
13429  722 
"[ x \<in> nat; y \<in> nat ] 
13306  723 
==> arity(Memrel_fm(x,y)) = succ(x) \<union> succ(y)" 
13429  724 
by (simp add: Memrel_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  725 

726 
lemma sats_Memrel_fm [simp]: 

727 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 

13429  728 
==> sats(A, Memrel_fm(x,y), env) <> 
13306  729 
membership(**A, nth(x,env), nth(y,env))" 
730 
by (simp add: Memrel_fm_def membership_def) 

13298  731 

13306  732 
lemma Memrel_iff_sats: 
13429  733 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  734 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
735 
==> membership(**A, x, y) <> sats(A, Memrel_fm(i,j), env)" 

736 
by simp 

13304  737 

13314  738 
theorem membership_reflection: 
13429  739 
"REFLECTS[\<lambda>x. membership(L,f(x),g(x)), 
13314  740 
\<lambda>i x. membership(**Lset(i),f(x),g(x))]" 
741 
apply (simp only: membership_def setclass_simps) 

13429  742 
apply (intro FOL_reflections pair_reflection) 
13314  743 
done 
13304  744 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

745 
subsubsection{*Predecessor Set, Internalized*} 
13304  746 

13306  747 
constdefs pred_set_fm :: "[i,i,i,i]=>i" 
13429  748 
"pred_set_fm(A,x,r,B) == 
13306  749 
Forall(Iff(Member(0,succ(B)), 
750 
Exists(And(Member(0,succ(succ(r))), 

751 
And(Member(1,succ(succ(A))), 

752 
pair_fm(1,succ(succ(x)),0))))))" 

753 

754 

755 
lemma pred_set_type [TC]: 

13429  756 
"[ A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat ] 
13306  757 
==> pred_set_fm(A,x,r,B) \<in> formula" 
13429  758 
by (simp add: pred_set_fm_def) 
13304  759 

13306  760 
lemma arity_pred_set_fm [simp]: 
13429  761 
"[ A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat ] 
13306  762 
==> arity(pred_set_fm(A,x,r,B)) = succ(A) \<union> succ(x) \<union> succ(r) \<union> succ(B)" 
13429  763 
by (simp add: pred_set_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  764 

765 
lemma sats_pred_set_fm [simp]: 

766 
"[ U \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat; env \<in> list(A)] 

13429  767 
==> sats(A, pred_set_fm(U,x,r,B), env) <> 
13306  768 
pred_set(**A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))" 
769 
by (simp add: pred_set_fm_def pred_set_def) 

770 

771 
lemma pred_set_iff_sats: 

13429  772 
"[ nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B; 
13306  773 
i \<in> nat; j \<in> nat; k \<in> nat; l \<in> nat; env \<in> list(A)] 
774 
==> pred_set(**A,U,x,r,B) <> sats(A, pred_set_fm(i,j,k,l), env)" 

775 
by (simp add: sats_pred_set_fm) 

776 

13314  777 
theorem pred_set_reflection: 
13429  778 
"REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)), 
779 
\<lambda>i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]" 

13314  780 
apply (simp only: pred_set_def setclass_simps) 
13429  781 
apply (intro FOL_reflections pair_reflection) 
13314  782 
done 
13304  783 

784 

13298  785 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

786 
subsubsection{*Domain of a Relation, Internalized*} 
13306  787 

13429  788 
(* "is_domain(M,r,z) == 
789 
\<forall>x[M]. (x \<in> z <> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))" *) 

13306  790 
constdefs domain_fm :: "[i,i]=>i" 
13429  791 
"domain_fm(r,z) == 
13306  792 
Forall(Iff(Member(0,succ(z)), 
793 
Exists(And(Member(0,succ(succ(r))), 

794 
Exists(pair_fm(2,0,1))))))" 

795 

796 
lemma domain_type [TC]: 

797 
"[ x \<in> nat; y \<in> nat ] ==> domain_fm(x,y) \<in> formula" 

13429  798 
by (simp add: domain_fm_def) 
13306  799 

800 
lemma arity_domain_fm [simp]: 

13429  801 
"[ x \<in> nat; y \<in> nat ] 
13306  802 
==> arity(domain_fm(x,y)) = succ(x) \<union> succ(y)" 
13429  803 
by (simp add: domain_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  804 

805 
lemma sats_domain_fm [simp]: 

806 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 

13429  807 
==> sats(A, domain_fm(x,y), env) <> 
13306  808 
is_domain(**A, nth(x,env), nth(y,env))" 
809 
by (simp add: domain_fm_def is_domain_def) 

810 

811 
lemma domain_iff_sats: 

13429  812 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  813 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
814 
==> is_domain(**A, x, y) <> sats(A, domain_fm(i,j), env)" 

815 
by simp 

816 

13314  817 
theorem domain_reflection: 
13429  818 
"REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)), 
13314  819 
\<lambda>i x. is_domain(**Lset(i),f(x),g(x))]" 
820 
apply (simp only: is_domain_def setclass_simps) 

13429  821 
apply (intro FOL_reflections pair_reflection) 
13314  822 
done 
13306  823 

824 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

825 
subsubsection{*Range of a Relation, Internalized*} 
13306  826 

13429  827 
(* "is_range(M,r,z) == 
828 
\<forall>y[M]. (y \<in> z <> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))" *) 

13306  829 
constdefs range_fm :: "[i,i]=>i" 
13429  830 
"range_fm(r,z) == 
13306  831 
Forall(Iff(Member(0,succ(z)), 
832 
Exists(And(Member(0,succ(succ(r))), 

833 
Exists(pair_fm(0,2,1))))))" 

834 

835 
lemma range_type [TC]: 

836 
"[ x \<in> nat; y \<in> nat ] ==> range_fm(x,y) \<in> formula" 

13429  837 
by (simp add: range_fm_def) 
13306  838 

839 
lemma arity_range_fm [simp]: 

13429  840 
"[ x \<in> nat; y \<in> nat ] 
13306  841 
==> arity(range_fm(x,y)) = succ(x) \<union> succ(y)" 
13429  842 
by (simp add: range_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  843 

844 
lemma sats_range_fm [simp]: 

845 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 

13429  846 
==> sats(A, range_fm(x,y), env) <> 
13306  847 
is_range(**A, nth(x,env), nth(y,env))" 
848 
by (simp add: range_fm_def is_range_def) 

849 

850 
lemma range_iff_sats: 

13429  851 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  852 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
853 
==> is_range(**A, x, y) <> sats(A, range_fm(i,j), env)" 

854 
by simp 

855 

13314  856 
theorem range_reflection: 
13429  857 
"REFLECTS[\<lambda>x. is_range(L,f(x),g(x)), 
13314  858 
\<lambda>i x. is_range(**Lset(i),f(x),g(x))]" 
859 
apply (simp only: is_range_def setclass_simps) 

13429  860 
apply (intro FOL_reflections pair_reflection) 
13314  861 
done 
13306  862 

13429  863 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

864 
subsubsection{*Field of a Relation, Internalized*} 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

865 

13429  866 
(* "is_field(M,r,z) == 
867 
\<exists>dr[M]. is_domain(M,r,dr) & 

13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

868 
(\<exists>rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))" *) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

869 
constdefs field_fm :: "[i,i]=>i" 
13429  870 
"field_fm(r,z) == 
871 
Exists(And(domain_fm(succ(r),0), 

872 
Exists(And(range_fm(succ(succ(r)),0), 

13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

873 
union_fm(1,0,succ(succ(z)))))))" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

874 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

875 
lemma field_type [TC]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

876 
"[ x \<in> nat; y \<in> nat ] ==> field_fm(x,y) \<in> formula" 
13429  877 
by (simp add: field_fm_def) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

878 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

879 
lemma arity_field_fm [simp]: 
13429  880 
"[ x \<in> nat; y \<in> nat ] 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

881 
==> arity(field_fm(x,y)) = succ(x) \<union> succ(y)" 
13429  882 
by (simp add: field_fm_def succ_Un_distrib [symmetric] Un_ac) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

883 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

884 
lemma sats_field_fm [simp]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

885 
"[ x \<in> nat; y \<in> nat; env \<in> list(A)] 
13429  886 
==> sats(A, field_fm(x,y), env) <> 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

887 
is_field(**A, nth(x,env), nth(y,env))" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

888 
by (simp add: field_fm_def is_field_def) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

889 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

890 
lemma field_iff_sats: 
13429  891 
"[ nth(i,env) = x; nth(j,env) = y; 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

892 
i \<in> nat; j \<in> nat; env \<in> list(A)] 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

893 
==> is_field(**A, x, y) <> sats(A, field_fm(i,j), env)" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

894 
by simp 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

895 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

896 
theorem field_reflection: 
13429  897 
"REFLECTS[\<lambda>x. is_field(L,f(x),g(x)), 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

898 
\<lambda>i x. is_field(**Lset(i),f(x),g(x))]" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

899 
apply (simp only: is_field_def setclass_simps) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

900 
apply (intro FOL_reflections domain_reflection range_reflection 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

901 
union_reflection) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

902 
done 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

903 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

904 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

905 
subsubsection{*Image under a Relation, Internalized*} 
13306  906 

13429  907 
(* "image(M,r,A,z) == 
13306  908 
\<forall>y[M]. (y \<in> z <> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))" *) 
909 
constdefs image_fm :: "[i,i,i]=>i" 

13429  910 
"image_fm(r,A,z) == 
13306  911 
Forall(Iff(Member(0,succ(z)), 
912 
Exists(And(Member(0,succ(succ(r))), 

913 
Exists(And(Member(0,succ(succ(succ(A)))), 

13429  914 
pair_fm(0,2,1)))))))" 
13306  915 

916 
lemma image_type [TC]: 

917 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> image_fm(x,y,z) \<in> formula" 

13429  918 
by (simp add: image_fm_def) 
13306  919 

920 
lemma arity_image_fm [simp]: 

13429  921 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13306  922 
==> arity(image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  923 
by (simp add: image_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  924 

925 
lemma sats_image_fm [simp]: 

926 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  927 
==> sats(A, image_fm(x,y,z), env) <> 
13306  928 
image(**A, nth(x,env), nth(y,env), nth(z,env))" 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

929 
by (simp add: image_fm_def Relative.image_def) 
13306  930 

931 
lemma image_iff_sats: 

13429  932 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13306  933 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
934 
==> image(**A, x, y, z) <> sats(A, image_fm(i,j,k), env)" 

935 
by (simp add: sats_image_fm) 

936 

13314  937 
theorem image_reflection: 
13429  938 
"REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)), 
13314  939 
\<lambda>i x. image(**Lset(i),f(x),g(x),h(x))]" 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

940 
apply (simp only: Relative.image_def setclass_simps) 
13429  941 
apply (intro FOL_reflections pair_reflection) 
13314  942 
done 
13306  943 

944 

13348  945 
subsubsection{*PreImage under a Relation, Internalized*} 
946 

13429  947 
(* "pre_image(M,r,A,z) == 
948 
\<forall>x[M]. x \<in> z <> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. y\<in>A & pair(M,x,y,w)))" *) 

13348  949 
constdefs pre_image_fm :: "[i,i,i]=>i" 
13429  950 
"pre_image_fm(r,A,z) == 
13348  951 
Forall(Iff(Member(0,succ(z)), 
952 
Exists(And(Member(0,succ(succ(r))), 

953 
Exists(And(Member(0,succ(succ(succ(A)))), 

13429  954 
pair_fm(2,0,1)))))))" 
13348  955 

956 
lemma pre_image_type [TC]: 

957 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> pre_image_fm(x,y,z) \<in> formula" 

13429  958 
by (simp add: pre_image_fm_def) 
13348  959 

960 
lemma arity_pre_image_fm [simp]: 

13429  961 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13348  962 
==> arity(pre_image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  963 
by (simp add: pre_image_fm_def succ_Un_distrib [symmetric] Un_ac) 
13348  964 

965 
lemma sats_pre_image_fm [simp]: 

966 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  967 
==> sats(A, pre_image_fm(x,y,z), env) <> 
13348  968 
pre_image(**A, nth(x,env), nth(y,env), nth(z,env))" 
969 
by (simp add: pre_image_fm_def Relative.pre_image_def) 

970 

971 
lemma pre_image_iff_sats: 

13429  972 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13348  973 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
974 
==> pre_image(**A, x, y, z) <> sats(A, pre_image_fm(i,j,k), env)" 

975 
by (simp add: sats_pre_image_fm) 

976 

977 
theorem pre_image_reflection: 

13429  978 
"REFLECTS[\<lambda>x. pre_image(L,f(x),g(x),h(x)), 
13348  979 
\<lambda>i x. pre_image(**Lset(i),f(x),g(x),h(x))]" 
980 
apply (simp only: Relative.pre_image_def setclass_simps) 

13429  981 
apply (intro FOL_reflections pair_reflection) 
13348  982 
done 
983 

984 

13352  985 
subsubsection{*Function Application, Internalized*} 
986 

13429  987 
(* "fun_apply(M,f,x,y) == 
988 
(\<exists>xs[M]. \<exists>fxs[M]. 

13352  989 
upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" *) 
990 
constdefs fun_apply_fm :: "[i,i,i]=>i" 

13429  991 
"fun_apply_fm(f,x,y) == 
13352  992 
Exists(Exists(And(upair_fm(succ(succ(x)), succ(succ(x)), 1), 
13429  993 
And(image_fm(succ(succ(f)), 1, 0), 
13352  994 
big_union_fm(0,succ(succ(y)))))))" 
995 

996 
lemma fun_apply_type [TC]: 

997 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> fun_apply_fm(x,y,z) \<in> formula" 

13429  998 
by (simp add: fun_apply_fm_def) 
13352  999 

1000 
lemma arity_fun_apply_fm [simp]: 

13429  1001 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13352  1002 
==> arity(fun_apply_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  1003 
by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac) 
13352  1004 

1005 
lemma sats_fun_apply_fm [simp]: 

1006 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  1007 
==> sats(A, fun_apply_fm(x,y,z), env) <> 
13352  1008 
fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))" 
1009 
by (simp add: fun_apply_fm_def fun_apply_def) 

1010 

1011 
lemma fun_apply_iff_sats: 

13429  1012 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13352  1013 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
1014 
==> fun_apply(**A, x, y, z) <> sats(A, fun_apply_fm(i,j,k), env)" 

1015 
by simp 

1016 

1017 
theorem fun_apply_reflection: 

13429  1018 
"REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)), 
1019 
\<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]" 

13352  1020 
apply (simp only: fun_apply_def setclass_simps) 
1021 
apply (intro FOL_reflections upair_reflection image_reflection 

13429  1022 
big_union_reflection) 
13352  1023 
done 
1024 

1025 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

1026 
subsubsection{*The Concept of Relation, Internalized*} 
13306  1027 

13429  1028 
(* "is_relation(M,r) == 
13306  1029 
(\<forall>z[M]. z\<in>r > (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))" *) 
1030 
constdefs relation_fm :: "i=>i" 

13429  1031 
"relation_fm(r) == 
13306  1032 
Forall(Implies(Member(0,succ(r)), Exists(Exists(pair_fm(1,0,2)))))" 
1033 

1034 
lemma relation_type [TC]: 

1035 
"[ x \<in> nat ] ==> relation_fm(x) \<in> formula" 

13429  1036 
by (simp add: relation_fm_def) 
13306  1037 

1038 
lemma arity_relation_fm [simp]: 

1039 
"x \<in> nat ==> arity(relation_fm(x)) = succ(x)" 

13429  1040 
by (simp add: relation_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  1041 

1042 
lemma sats_relation_fm [simp]: 

1043 
"[ x \<in> nat; env \<in> list(A)] 

1044 
==> sats(A, relation_fm(x), env) <> is_relation(**A, nth(x,env))" 

1045 
by (simp add: relation_fm_def is_relation_def) 

1046 

1047 
lemma relation_iff_sats: 

13429  1048 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  1049 
i \<in> nat; env \<in> list(A)] 
1050 
==> is_relation(**A, x) <> sats(A, relation_fm(i), env)" 

1051 
by simp 

1052 

13314  1053 
theorem is_relation_reflection: 
13429  1054 
"REFLECTS[\<lambda>x. is_relation(L,f(x)), 
13314  1055 
\<lambda>i x. is_relation(**Lset(i),f(x))]" 
1056 
apply (simp only: is_relation_def setclass_simps) 

13429  1057 
apply (intro FOL_reflections pair_reflection) 
13314  1058 
done 
13306  1059 

1060 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

1061 
subsubsection{*The Concept of Function, Internalized*} 
13306  1062 

13429  1063 
(* "is_function(M,r) == 
1064 
\<forall>x[M]. \<forall>y[M]. \<forall>y'[M]. \<forall>p[M]. \<forall>p'[M]. 

13306  1065 
pair(M,x,y,p) > pair(M,x,y',p') > p\<in>r > p'\<in>r > y=y'" *) 
1066 
constdefs function_fm :: "i=>i" 

13429  1067 
"function_fm(r) == 
13306  1068 
Forall(Forall(Forall(Forall(Forall( 
1069 
Implies(pair_fm(4,3,1), 

1070 
Implies(pair_fm(4,2,0), 

1071 
Implies(Member(1,r#+5), 

1072 
Implies(Member(0,r#+5), Equal(3,2))))))))))" 

1073 

1074 
lemma function_type [TC]: 

1075 
"[ x \<in> nat ] ==> function_fm(x) \<in> formula" 

13429  1076 
by (simp add: function_fm_def) 
13306  1077 

1078 
lemma arity_function_fm [simp]: 

1079 
"x \<in> nat ==> arity(function_fm(x)) = succ(x)" 

13429  1080 
by (simp add: function_fm_def succ_Un_distrib [symmetric] Un_ac) 
13306  1081 

1082 
lemma sats_function_fm [simp]: 

1083 
"[ x \<in> nat; env \<in> list(A)] 

1084 
==> sats(A, function_fm(x), env) <> is_function(**A, nth(x,env))" 

1085 
by (simp add: function_fm_def is_function_def) 

1086 

13505  1087 
lemma is_function_iff_sats: 
13429  1088 
"[ nth(i,env) = x; nth(j,env) = y; 
13306  1089 
i \<in> nat; env \<in> list(A)] 
1090 
==> is_function(**A, x) <> sats(A, function_fm(i), env)" 

1091 
by simp 

1092 

13314  1093 
theorem is_function_reflection: 
13429  1094 
"REFLECTS[\<lambda>x. is_function(L,f(x)), 
13314  1095 
\<lambda>i x. is_function(**Lset(i),f(x))]" 
1096 
apply (simp only: is_function_def setclass_simps) 

13429  1097 
apply (intro FOL_reflections pair_reflection) 
13314  1098 
done 
13298  1099 

1100 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

1101 
subsubsection{*Typed Functions, Internalized*} 
13309  1102 

13429  1103 
(* "typed_function(M,A,B,r) == 
13309  1104 
is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) & 
1105 
(\<forall>u[M]. u\<in>r > (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) > y\<in>B))" *) 

1106 

1107 
constdefs typed_function_fm :: "[i,i,i]=>i" 

13429  1108 
"typed_function_fm(A,B,r) == 
13309  1109 
And(function_fm(r), 
1110 
And(relation_fm(r), 

1111 
And(domain_fm(r,A), 

1112 
Forall(Implies(Member(0,succ(r)), 

1113 
Forall(Forall(Implies(pair_fm(1,0,2),Member(0,B#+3)))))))))" 

1114 

1115 
lemma typed_function_type [TC]: 

1116 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> typed_function_fm(x,y,z) \<in> formula" 

13429  1117 
by (simp add: typed_function_fm_def) 
13309  1118 

1119 
lemma arity_typed_function_fm [simp]: 

13429  1120 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13309  1121 
==> arity(typed_function_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  1122 
by (simp add: typed_function_fm_def succ_Un_distrib [symmetric] Un_ac) 
13309  1123 

1124 
lemma sats_typed_function_fm [simp]: 

1125 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  1126 
==> sats(A, typed_function_fm(x,y,z), env) <> 
13309  1127 
typed_function(**A, nth(x,env), nth(y,env), nth(z,env))" 
1128 
by (simp add: typed_function_fm_def typed_function_def) 

1129 

1130 
lemma typed_function_iff_sats: 

13429  1131 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13309  1132 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
1133 
==> typed_function(**A, x, y, z) <> sats(A, typed_function_fm(i,j,k), env)" 

1134 
by simp 

1135 

13429  1136 
lemmas function_reflections = 
13363  1137 
empty_reflection number1_reflection 
13429  1138 
upair_reflection pair_reflection union_reflection 
1139 
big_union_reflection cons_reflection successor_reflection 

13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1140 
fun_apply_reflection subset_reflection 
13429  1141 
transitive_set_reflection membership_reflection 
1142 
pred_set_reflection domain_reflection range_reflection field_reflection 

13348  1143 
image_reflection pre_image_reflection 
13429  1144 
is_relation_reflection is_function_reflection 
13309  1145 

13429  1146 
lemmas function_iff_sats = 
1147 
empty_iff_sats number1_iff_sats 

1148 
upair_iff_sats pair_iff_sats union_iff_sats 

13505  1149 
big_union_iff_sats cons_iff_sats successor_iff_sats 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1150 
fun_apply_iff_sats Memrel_iff_sats 
13429  1151 
pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats 
1152 
image_iff_sats pre_image_iff_sats 

13505  1153 
relation_iff_sats is_function_iff_sats 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1154 

13309  1155 

13314  1156 
theorem typed_function_reflection: 
13429  1157 
"REFLECTS[\<lambda>x. typed_function(L,f(x),g(x),h(x)), 
13314  1158 
\<lambda>i x. typed_function(**Lset(i),f(x),g(x),h(x))]" 
1159 
apply (simp only: typed_function_def setclass_simps) 

13429  1160 
apply (intro FOL_reflections function_reflections) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1161 
done 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1162 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1163 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

1164 
subsubsection{*Composition of Relations, Internalized*} 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1165 

13429  1166 
(* "composition(M,r,s,t) == 
1167 
\<forall>p[M]. p \<in> t <> 

1168 
(\<exists>x[M]. \<exists>y[M]. \<exists>z[M]. \<exists>xy[M]. \<exists>yz[M]. 

1169 
pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & 

13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1170 
xy \<in> s & yz \<in> r)" *) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1171 
constdefs composition_fm :: "[i,i,i]=>i" 
13429  1172 
"composition_fm(r,s,t) == 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1173 
Forall(Iff(Member(0,succ(t)), 
13429  1174 
Exists(Exists(Exists(Exists(Exists( 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1175 
And(pair_fm(4,2,5), 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1176 
And(pair_fm(4,3,1), 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1177 
And(pair_fm(3,2,0), 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1178 
And(Member(1,s#+6), Member(0,r#+6))))))))))))" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1179 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1180 
lemma composition_type [TC]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1181 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> composition_fm(x,y,z) \<in> formula" 
13429  1182 
by (simp add: composition_fm_def) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1183 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1184 
lemma arity_composition_fm [simp]: 
13429  1185 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1186 
==> arity(composition_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  1187 
by (simp add: composition_fm_def succ_Un_distrib [symmetric] Un_ac) 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1188 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1189 
lemma sats_composition_fm [simp]: 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1190 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 
13429  1191 
==> sats(A, composition_fm(x,y,z), env) <> 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1192 
composition(**A, nth(x,env), nth(y,env), nth(z,env))" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1193 
by (simp add: composition_fm_def composition_def) 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1194 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1195 
lemma composition_iff_sats: 
13429  1196 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1197 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)] 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1198 
==> composition(**A, x, y, z) <> sats(A, composition_fm(i,j,k), env)" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1199 
by simp 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1200 

2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1201 
theorem composition_reflection: 
13429  1202 
"REFLECTS[\<lambda>x. composition(L,f(x),g(x),h(x)), 
13323
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1203 
\<lambda>i x. composition(**Lset(i),f(x),g(x),h(x))]" 
2c287f50c9f3
More relativization, reflection and proofs of separation
paulson
parents:
13316
diff
changeset

1204 
apply (simp only: composition_def setclass_simps) 
13429  1205 
apply (intro FOL_reflections pair_reflection) 
13314  1206 
done 
1207 

13309  1208 

13339
0f89104dd377
Fixed quantified variable name preservation for ball and bex (bounded quants)
paulson
parents:
13323
diff
changeset

1209 
subsubsection{*Injections, Internalized*} 
13309  1210 

13429  1211 
(* "injection(M,A,B,f) == 
1212 
typed_function(M,A,B,f) & 

1213 
(\<forall>x[M]. \<forall>x'[M]. \<forall>y[M]. \<forall>p[M]. \<forall>p'[M]. 

13309  1214 
pair(M,x,y,p) > pair(M,x',y,p') > p\<in>f > p'\<in>f > x=x')" *) 
1215 
constdefs injection_fm :: "[i,i,i]=>i" 

13429  1216 
"injection_fm(A,B,f) == 
13309  1217 
And(typed_function_fm(A,B,f), 
1218 
Forall(Forall(Forall(Forall(Forall( 

1219 
Implies(pair_fm(4,2,1), 

1220 
Implies(pair_fm(3,2,0), 

1221 
Implies(Member(1,f#+5), 

1222 
Implies(Member(0,f#+5), Equal(4,3)))))))))))" 

1223 

1224 

1225 
lemma injection_type [TC]: 

1226 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] ==> injection_fm(x,y,z) \<in> formula" 

13429  1227 
by (simp add: injection_fm_def) 
13309  1228 

1229 
lemma arity_injection_fm [simp]: 

13429  1230 
"[ x \<in> nat; y \<in> nat; z \<in> nat ] 
13309  1231 
==> arity(injection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)" 
13429  1232 
by (simp add: injection_fm_def succ_Un_distrib [symmetric] Un_ac) 
13309  1233 

1234 
lemma sats_injection_fm [simp]: 

1235 
"[ x \<in> nat; y \<in> nat; z \<in> nat; env \<in> list(A)] 

13429  1236 
==> sats(A, injection_fm(x,y,z), env) <> 
13309  1237 
injection(**A, nth(x,env), nth(y,env), nth(z,env))&qu 