13306

1 
header {*The Class L Satisfies the ZF Axioms*}

13223

2 

13314

3 
theory L_axioms = Formula + Relative + Reflection + MetaExists:

13223

4 


5 


6 
text {* The class L satisfies the premises of locale @{text M_axioms} *}


7 


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


9 
apply (insert Transset_Lset)


10 
apply (simp add: Transset_def L_def, blast)


11 
done


12 


13 
lemma nonempty: "L(0)"


14 
apply (simp add: L_def)


15 
apply (blast intro: zero_in_Lset)


16 
done


17 


18 
lemma upair_ax: "upair_ax(L)"


19 
apply (simp add: upair_ax_def upair_def, clarify)

13299

20 
apply (rule_tac x="{x,y}" in rexI)


21 
apply (simp_all add: doubleton_in_L)

13223

22 
done


23 


24 
lemma Union_ax: "Union_ax(L)"


25 
apply (simp add: Union_ax_def big_union_def, clarify)

13299

26 
apply (rule_tac x="Union(x)" in rexI)


27 
apply (simp_all add: Union_in_L, auto)

13223

28 
apply (blast intro: transL)


29 
done


30 


31 
lemma power_ax: "power_ax(L)"


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

13299

33 
apply (rule_tac x="{y \<in> Pow(x). L(y)}" in rexI)


34 
apply (simp_all add: LPow_in_L, auto)

13223

35 
apply (blast intro: transL)


36 
done


37 


38 
subsubsection{*For L to satisfy Replacement *}


39 


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


41 
there too!*)


42 


43 
lemma LReplace_in_Lset:


44 
"[X \<in> Lset(i); univalent(L,X,Q); Ord(i)]


45 
==> \<exists>j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Lset(j)"


46 
apply (rule_tac x="\<Union>y \<in> Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))"


47 
in exI)


48 
apply simp


49 
apply clarify


50 
apply (rule_tac a="x" in UN_I)


51 
apply (simp_all add: Replace_iff univalent_def)


52 
apply (blast dest: transL L_I)


53 
done


54 


55 
lemma LReplace_in_L:


56 
"[L(X); univalent(L,X,Q)]


57 
==> \<exists>Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \<subseteq> Y"


58 
apply (drule L_D, clarify)


59 
apply (drule LReplace_in_Lset, assumption+)


60 
apply (blast intro: L_I Lset_in_Lset_succ)


61 
done


62 


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


64 
apply (simp add: replacement_def, clarify)

13268

65 
apply (frule LReplace_in_L, assumption+, clarify)

13299

66 
apply (rule_tac x=Y in rexI)


67 
apply (simp_all add: Replace_iff univalent_def, blast)

13223

68 
done


69 

13291

70 
subsection{*Instantiation of the locale @{text M_triv_axioms}*}


71 


72 
lemma Lset_mono_le: "mono_le_subset(Lset)"


73 
by (simp add: mono_le_subset_def le_imp_subset Lset_mono)


74 


75 
lemma Lset_cont: "cont_Ord(Lset)"


76 
by (simp add: cont_Ord_def Limit_Lset_eq OUnion_def Limit_is_Ord)


77 


78 
lemmas Pair_in_Lset = Formula.Pair_in_LLimit;


79 


80 
lemmas L_nat = Ord_in_L [OF Ord_nat];


81 


82 
ML


83 
{*


84 
val transL = thm "transL";


85 
val nonempty = thm "nonempty";


86 
val upair_ax = thm "upair_ax";


87 
val Union_ax = thm "Union_ax";


88 
val power_ax = thm "power_ax";


89 
val replacement = thm "replacement";


90 
val L_nat = thm "L_nat";


91 


92 
fun kill_flex_triv_prems st = Seq.hd ((REPEAT_FIRST assume_tac) st);


93 


94 
fun trivaxL th =


95 
kill_flex_triv_prems


96 
([transL, nonempty, upair_ax, Union_ax, power_ax, replacement, L_nat]


97 
MRS (inst "M" "L" th));


98 


99 
bind_thm ("ball_abs", trivaxL (thm "M_triv_axioms.ball_abs"));


100 
bind_thm ("rall_abs", trivaxL (thm "M_triv_axioms.rall_abs"));


101 
bind_thm ("bex_abs", trivaxL (thm "M_triv_axioms.bex_abs"));


102 
bind_thm ("rex_abs", trivaxL (thm "M_triv_axioms.rex_abs"));


103 
bind_thm ("ball_iff_equiv", trivaxL (thm "M_triv_axioms.ball_iff_equiv"));


104 
bind_thm ("M_equalityI", trivaxL (thm "M_triv_axioms.M_equalityI"));


105 
bind_thm ("empty_abs", trivaxL (thm "M_triv_axioms.empty_abs"));


106 
bind_thm ("subset_abs", trivaxL (thm "M_triv_axioms.subset_abs"));


107 
bind_thm ("upair_abs", trivaxL (thm "M_triv_axioms.upair_abs"));


108 
bind_thm ("upair_in_M_iff", trivaxL (thm "M_triv_axioms.upair_in_M_iff"));


109 
bind_thm ("singleton_in_M_iff", trivaxL (thm "M_triv_axioms.singleton_in_M_iff"));


110 
bind_thm ("pair_abs", trivaxL (thm "M_triv_axioms.pair_abs"));


111 
bind_thm ("pair_in_M_iff", trivaxL (thm "M_triv_axioms.pair_in_M_iff"));


112 
bind_thm ("pair_components_in_M", trivaxL (thm "M_triv_axioms.pair_components_in_M"));


113 
bind_thm ("cartprod_abs", trivaxL (thm "M_triv_axioms.cartprod_abs"));


114 
bind_thm ("union_abs", trivaxL (thm "M_triv_axioms.union_abs"));


115 
bind_thm ("inter_abs", trivaxL (thm "M_triv_axioms.inter_abs"));


116 
bind_thm ("setdiff_abs", trivaxL (thm "M_triv_axioms.setdiff_abs"));


117 
bind_thm ("Union_abs", trivaxL (thm "M_triv_axioms.Union_abs"));


118 
bind_thm ("Union_closed", trivaxL (thm "M_triv_axioms.Union_closed"));


119 
bind_thm ("Un_closed", trivaxL (thm "M_triv_axioms.Un_closed"));


120 
bind_thm ("cons_closed", trivaxL (thm "M_triv_axioms.cons_closed"));


121 
bind_thm ("successor_abs", trivaxL (thm "M_triv_axioms.successor_abs"));


122 
bind_thm ("succ_in_M_iff", trivaxL (thm "M_triv_axioms.succ_in_M_iff"));


123 
bind_thm ("separation_closed", trivaxL (thm "M_triv_axioms.separation_closed"));


124 
bind_thm ("strong_replacementI", trivaxL (thm "M_triv_axioms.strong_replacementI"));


125 
bind_thm ("strong_replacement_closed", trivaxL (thm "M_triv_axioms.strong_replacement_closed"));


126 
bind_thm ("RepFun_closed", trivaxL (thm "M_triv_axioms.RepFun_closed"));


127 
bind_thm ("lam_closed", trivaxL (thm "M_triv_axioms.lam_closed"));


128 
bind_thm ("image_abs", trivaxL (thm "M_triv_axioms.image_abs"));


129 
bind_thm ("powerset_Pow", trivaxL (thm "M_triv_axioms.powerset_Pow"));


130 
bind_thm ("powerset_imp_subset_Pow", trivaxL (thm "M_triv_axioms.powerset_imp_subset_Pow"));


131 
bind_thm ("nat_into_M", trivaxL (thm "M_triv_axioms.nat_into_M"));


132 
bind_thm ("nat_case_closed", trivaxL (thm "M_triv_axioms.nat_case_closed"));


133 
bind_thm ("Inl_in_M_iff", trivaxL (thm "M_triv_axioms.Inl_in_M_iff"));


134 
bind_thm ("Inr_in_M_iff", trivaxL (thm "M_triv_axioms.Inr_in_M_iff"));


135 
bind_thm ("lt_closed", trivaxL (thm "M_triv_axioms.lt_closed"));


136 
bind_thm ("transitive_set_abs", trivaxL (thm "M_triv_axioms.transitive_set_abs"));


137 
bind_thm ("ordinal_abs", trivaxL (thm "M_triv_axioms.ordinal_abs"));


138 
bind_thm ("limit_ordinal_abs", trivaxL (thm "M_triv_axioms.limit_ordinal_abs"));


139 
bind_thm ("successor_ordinal_abs", trivaxL (thm "M_triv_axioms.successor_ordinal_abs"));


140 
bind_thm ("finite_ordinal_abs", trivaxL (thm "M_triv_axioms.finite_ordinal_abs"));


141 
bind_thm ("omega_abs", trivaxL (thm "M_triv_axioms.omega_abs"));


142 
bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));


143 
bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs"));


144 
bind_thm ("number3_abs", trivaxL (thm "M_triv_axioms.number3_abs"));


145 
*}


146 


147 
declare ball_abs [simp]


148 
declare rall_abs [simp]


149 
declare bex_abs [simp]


150 
declare rex_abs [simp]


151 
declare empty_abs [simp]


152 
declare subset_abs [simp]


153 
declare upair_abs [simp]


154 
declare upair_in_M_iff [iff]


155 
declare singleton_in_M_iff [iff]


156 
declare pair_abs [simp]


157 
declare pair_in_M_iff [iff]


158 
declare cartprod_abs [simp]


159 
declare union_abs [simp]


160 
declare inter_abs [simp]


161 
declare setdiff_abs [simp]


162 
declare Union_abs [simp]


163 
declare Union_closed [intro,simp]


164 
declare Un_closed [intro,simp]


165 
declare cons_closed [intro,simp]


166 
declare successor_abs [simp]


167 
declare succ_in_M_iff [iff]


168 
declare separation_closed [intro,simp]

13306

169 
declare strong_replacementI

13291

170 
declare strong_replacement_closed [intro,simp]


171 
declare RepFun_closed [intro,simp]


172 
declare lam_closed [intro,simp]


173 
declare image_abs [simp]


174 
declare nat_into_M [intro]


175 
declare Inl_in_M_iff [iff]


176 
declare Inr_in_M_iff [iff]


177 
declare transitive_set_abs [simp]


178 
declare ordinal_abs [simp]


179 
declare limit_ordinal_abs [simp]


180 
declare successor_ordinal_abs [simp]


181 
declare finite_ordinal_abs [simp]


182 
declare omega_abs [simp]


183 
declare number1_abs [simp]


184 
declare number1_abs [simp]


185 
declare number3_abs [simp]


186 


187 


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


189 


190 
text{*instances of locale constants*}


191 
constdefs


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


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


194 


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


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


197 


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


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


200 


201 

13314

202 
text{*We must use the metaexistential quantifier; otherwise the reflection


203 
terms become enormous!*}


204 
constdefs


205 
L_Reflects :: "[i=>o,[i,i]=>o] => prop" ("(3REFLECTS/ [_,/ _])")


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


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

13291

208 


209 

13314

210 
theorem Triv_reflection:


211 
"REFLECTS[P, \<lambda>a x. P(x)]"


212 
apply (simp add: L_Reflects_def)


213 
apply (rule meta_exI)


214 
apply (rule Closed_Unbounded_Ord)


215 
done


216 


217 
theorem Not_reflection:


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


219 
apply (unfold L_Reflects_def)


220 
apply (erule meta_exE)


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


222 
done


223 


224 
theorem And_reflection:


225 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ]


226 
==> REFLECTS[\<lambda>x. P(x) \<and> P'(x), \<lambda>a x. Q(a,x) \<and> Q'(a,x)]"


227 
apply (unfold L_Reflects_def)


228 
apply (elim meta_exE)


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


230 
apply (simp add: Closed_Unbounded_Int, blast)


231 
done


232 


233 
theorem Or_reflection:


234 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ]


235 
==> REFLECTS[\<lambda>x. P(x) \<or> P'(x), \<lambda>a x. Q(a,x) \<or> Q'(a,x)]"


236 
apply (unfold L_Reflects_def)


237 
apply (elim meta_exE)


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


239 
apply (simp add: Closed_Unbounded_Int, blast)


240 
done


241 


242 
theorem Imp_reflection:


243 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ]


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


245 
apply (unfold L_Reflects_def)


246 
apply (elim meta_exE)


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


248 
apply (simp add: Closed_Unbounded_Int, blast)


249 
done


250 


251 
theorem Iff_reflection:


252 
"[ REFLECTS[P,Q]; REFLECTS[P',Q'] ]


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


254 
apply (unfold L_Reflects_def)


255 
apply (elim meta_exE)


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


257 
apply (simp add: Closed_Unbounded_Int, blast)


258 
done


259 


260 


261 
theorem Ex_reflection:


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


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

13291

264 
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)

13314

265 
apply (elim meta_exE)


266 
apply (rule meta_exI)

13291

267 
apply (rule reflection.Ex_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset],


268 
assumption+)


269 
done


270 

13314

271 
theorem All_reflection:


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


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

13291

274 
apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def)

13314

275 
apply (elim meta_exE)


276 
apply (rule meta_exI)

13291

277 
apply (rule reflection.All_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset],


278 
assumption+)


279 
done


280 

13314

281 
theorem Rex_reflection:


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


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


284 
apply (unfold rex_def)


285 
apply (intro And_reflection Ex_reflection, assumption)


286 
done

13291

287 

13314

288 
theorem Rall_reflection:


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


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


291 
apply (unfold rall_def)


292 
apply (intro Imp_reflection All_reflection, assumption)


293 
done


294 


295 
lemmas FOL_reflection =


296 
Triv_reflection Not_reflection And_reflection Or_reflection


297 
Imp_reflection Iff_reflection Ex_reflection All_reflection


298 
Rex_reflection Rall_reflection

13291

299 


300 
lemma ReflectsD:

13314

301 
"[REFLECTS[P,Q]; Ord(i)]

13291

302 
==> \<exists>j. i<j & (\<forall>x \<in> Lset(j). P(x) <> Q(j,x))"

13314

303 
apply (unfold L_Reflects_def Closed_Unbounded_def)


304 
apply (elim meta_exE, clarify)

13291

305 
apply (blast dest!: UnboundedD)


306 
done


307 


308 
lemma ReflectsE:

13314

309 
"[ REFLECTS[P,Q]; Ord(i);

13291

310 
!!j. [i<j; \<forall>x \<in> Lset(j). P(x) <> Q(j,x)] ==> R ]


311 
==> R"

13316

312 
apply (drule ReflectsD, assumption, blast)

13314

313 
done

13291

314 


315 
lemma Collect_mem_eq: "{x\<in>A. x\<in>B} = A \<inter> B";


316 
by blast


317 


318 

13298

319 
subsection{*Internalized formulas for some relativized ones*}


320 

13306

321 
lemmas setclass_simps = rall_setclass_is_ball rex_setclass_is_bex


322 


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


324 


325 
syntax


326 
"3" :: i ("3")


327 
"4" :: i ("4")


328 
"5" :: i ("5")


329 
"6" :: i ("6")


330 
"7" :: i ("7")


331 
"8" :: i ("8")


332 
"9" :: i ("9")


333 


334 
translations


335 
"3" == "succ(2)"


336 
"4" == "succ(3)"


337 
"5" == "succ(4)"


338 
"6" == "succ(5)"


339 
"7" == "succ(6)"


340 
"8" == "succ(7)"


341 
"9" == "succ(8)"


342 

13298

343 
subsubsection{*Unordered pairs*}


344 


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


346 
"upair_fm(x,y,z) ==


347 
And(Member(x,z),


348 
And(Member(y,z),


349 
Forall(Implies(Member(0,succ(z)),


350 
Or(Equal(0,succ(x)), Equal(0,succ(y)))))))"


351 


352 
lemma upair_type [TC]:


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


354 
by (simp add: upair_fm_def)


355 


356 
lemma arity_upair_fm [simp]:


357 
"[ x \<in> nat; y \<in> nat; z \<in> nat ]


358 
==> arity(upair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"


359 
by (simp add: upair_fm_def succ_Un_distrib [symmetric] Un_ac)


360 


361 
lemma sats_upair_fm [simp]:


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


363 
==> sats(A, upair_fm(x,y,z), env) <>


364 
upair(**A, nth(x,env), nth(y,env), nth(z,env))"


365 
by (simp add: upair_fm_def upair_def)


366 


367 
lemma upair_iff_sats:


368 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;


369 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)]


370 
==> upair(**A, x, y, z) <> sats(A, upair_fm(i,j,k), env)"


371 
by (simp add: sats_upair_fm)


372 


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


374 
lemma sats_upair_fm2 [simp]:


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


376 
==> sats(A, upair_fm(x,y,z), env) <>


377 
nth(z,env) = {nth(x,env), nth(y,env)}"


378 
apply (frule lt_length_in_nat, assumption)


379 
apply (simp add: upair_fm_def Transset_def, auto)


380 
apply (blast intro: nth_type)


381 
done


382 

13314

383 
theorem upair_reflection:


384 
"REFLECTS[\<lambda>x. upair(L,f(x),g(x),h(x)),


385 
\<lambda>i x. upair(**Lset(i),f(x),g(x),h(x))]"


386 
apply (simp add: upair_def)


387 
apply (intro FOL_reflection)


388 
done

13306

389 

13298

390 
subsubsection{*Ordered pairs*}


391 


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


393 
"pair_fm(x,y,z) ==


394 
Exists(And(upair_fm(succ(x),succ(x),0),


395 
Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0),


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


397 


398 
lemma pair_type [TC]:


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


400 
by (simp add: pair_fm_def)


401 


402 
lemma arity_pair_fm [simp]:


403 
"[ x \<in> nat; y \<in> nat; z \<in> nat ]


404 
==> arity(pair_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"


405 
by (simp add: pair_fm_def succ_Un_distrib [symmetric] Un_ac)


406 


407 
lemma sats_pair_fm [simp]:


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


409 
==> sats(A, pair_fm(x,y,z), env) <>


410 
pair(**A, nth(x,env), nth(y,env), nth(z,env))"


411 
by (simp add: pair_fm_def pair_def)


412 


413 
lemma pair_iff_sats:


414 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;


415 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)]


416 
==> pair(**A, x, y, z) <> sats(A, pair_fm(i,j,k), env)"


417 
by (simp add: sats_pair_fm)


418 

13314

419 
theorem pair_reflection:


420 
"REFLECTS[\<lambda>x. pair(L,f(x),g(x),h(x)),


421 
\<lambda>i x. pair(**Lset(i),f(x),g(x),h(x))]"


422 
apply (simp only: pair_def setclass_simps)


423 
apply (intro FOL_reflection upair_reflection)


424 
done

13306

425 


426 


427 
subsubsection{*Binary Unions*}

13298

428 

13306

429 
constdefs union_fm :: "[i,i,i]=>i"


430 
"union_fm(x,y,z) ==


431 
Forall(Iff(Member(0,succ(z)),


432 
Or(Member(0,succ(x)),Member(0,succ(y)))))"


433 


434 
lemma union_type [TC]:


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


436 
by (simp add: union_fm_def)


437 


438 
lemma arity_union_fm [simp]:


439 
"[ x \<in> nat; y \<in> nat; z \<in> nat ]


440 
==> arity(union_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"


441 
by (simp add: union_fm_def succ_Un_distrib [symmetric] Un_ac)

13298

442 

13306

443 
lemma sats_union_fm [simp]:


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


445 
==> sats(A, union_fm(x,y,z), env) <>


446 
union(**A, nth(x,env), nth(y,env), nth(z,env))"


447 
by (simp add: union_fm_def union_def)


448 


449 
lemma union_iff_sats:


450 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;


451 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)]


452 
==> union(**A, x, y, z) <> sats(A, union_fm(i,j,k), env)"


453 
by (simp add: sats_union_fm)

13298

454 

13314

455 
theorem union_reflection:


456 
"REFLECTS[\<lambda>x. union(L,f(x),g(x),h(x)),


457 
\<lambda>i x. union(**Lset(i),f(x),g(x),h(x))]"


458 
apply (simp only: union_def setclass_simps)


459 
apply (intro FOL_reflection)


460 
done

13306

461 

13298

462 

13306

463 
subsubsection{*`Cons' for sets*}


464 


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


466 
"cons_fm(x,y,z) ==


467 
Exists(And(upair_fm(succ(x),succ(x),0),


468 
union_fm(0,succ(y),succ(z))))"

13298

469 


470 

13306

471 
lemma cons_type [TC]:


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


473 
by (simp add: cons_fm_def)


474 


475 
lemma arity_cons_fm [simp]:


476 
"[ x \<in> nat; y \<in> nat; z \<in> nat ]


477 
==> arity(cons_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"


478 
by (simp add: cons_fm_def succ_Un_distrib [symmetric] Un_ac)


479 


480 
lemma sats_cons_fm [simp]:


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


482 
==> sats(A, cons_fm(x,y,z), env) <>


483 
is_cons(**A, nth(x,env), nth(y,env), nth(z,env))"


484 
by (simp add: cons_fm_def is_cons_def)


485 


486 
lemma cons_iff_sats:


487 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;


488 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)]


489 
==> is_cons(**A, x, y, z) <> sats(A, cons_fm(i,j,k), env)"


490 
by simp


491 

13314

492 
theorem cons_reflection:


493 
"REFLECTS[\<lambda>x. is_cons(L,f(x),g(x),h(x)),


494 
\<lambda>i x. is_cons(**Lset(i),f(x),g(x),h(x))]"


495 
apply (simp only: is_cons_def setclass_simps)


496 
apply (intro FOL_reflection upair_reflection union_reflection)


497 
done

13298

498 


499 

13306

500 
subsubsection{*Function Applications*}


501 


502 
constdefs fun_apply_fm :: "[i,i,i]=>i"


503 
"fun_apply_fm(f,x,y) ==


504 
Forall(Iff(Exists(And(Member(0,succ(succ(f))),


505 
pair_fm(succ(succ(x)), 1, 0))),


506 
Equal(succ(y),0)))"

13298

507 

13306

508 
lemma fun_apply_type [TC]:


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


510 
by (simp add: fun_apply_fm_def)


511 


512 
lemma arity_fun_apply_fm [simp]:


513 
"[ x \<in> nat; y \<in> nat; z \<in> nat ]


514 
==> arity(fun_apply_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"


515 
by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac)

13298

516 

13306

517 
lemma sats_fun_apply_fm [simp]:


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


519 
==> sats(A, fun_apply_fm(x,y,z), env) <>


520 
fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))"


521 
by (simp add: fun_apply_fm_def fun_apply_def)


522 


523 
lemma fun_apply_iff_sats:


524 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;


525 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)]


526 
==> fun_apply(**A, x, y, z) <> sats(A, fun_apply_fm(i,j,k), env)"


527 
by simp


528 

13314

529 
theorem fun_apply_reflection:


530 
"REFLECTS[\<lambda>x. fun_apply(L,f(x),g(x),h(x)),


531 
\<lambda>i x. fun_apply(**Lset(i),f(x),g(x),h(x))]"


532 
apply (simp only: fun_apply_def setclass_simps)


533 
apply (intro FOL_reflection pair_reflection)


534 
done

13298

535 


536 

13306

537 
subsubsection{*Variants of Satisfaction Definitions for Ordinals, etc.*}


538 


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


540 


541 


542 
lemma sats_subset_fm':


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


544 
==> sats(A, subset_fm(x,y), env) <> subset(**A, nth(x,env), nth(y,env))"


545 
by (simp add: subset_fm_def subset_def)

13298

546 

13314

547 
theorem subset_reflection:


548 
"REFLECTS[\<lambda>x. subset(L,f(x),g(x)),


549 
\<lambda>i x. subset(**Lset(i),f(x),g(x))]"


550 
apply (simp only: subset_def setclass_simps)


551 
apply (intro FOL_reflection)


552 
done

13306

553 


554 
lemma sats_transset_fm':


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


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


557 
by (simp add: sats_subset_fm' transset_fm_def transitive_set_def)

13298

558 

13314

559 
theorem transitive_set_reflection:


560 
"REFLECTS[\<lambda>x. transitive_set(L,f(x)),


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


562 
apply (simp only: transitive_set_def setclass_simps)


563 
apply (intro FOL_reflection subset_reflection)


564 
done

13306

565 


566 
lemma sats_ordinal_fm':


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


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


569 
by (simp add: sats_transset_fm' ordinal_fm_def ordinal_def)


570 


571 
lemma ordinal_iff_sats:


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


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


574 
by (simp add: sats_ordinal_fm')


575 

13314

576 
theorem ordinal_reflection:


577 
"REFLECTS[\<lambda>x. ordinal(L,f(x)), \<lambda>i x. ordinal(**Lset(i),f(x))]"


578 
apply (simp only: ordinal_def setclass_simps)


579 
apply (intro FOL_reflection transitive_set_reflection)


580 
done

13298

581 


582 

13306

583 
subsubsection{*Membership Relation*}

13298

584 

13306

585 
constdefs Memrel_fm :: "[i,i]=>i"


586 
"Memrel_fm(A,r) ==


587 
Forall(Iff(Member(0,succ(r)),


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


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


590 
And(Member(1,0),


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


592 


593 
lemma Memrel_type [TC]:


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


595 
by (simp add: Memrel_fm_def)

13298

596 

13306

597 
lemma arity_Memrel_fm [simp]:


598 
"[ x \<in> nat; y \<in> nat ]


599 
==> arity(Memrel_fm(x,y)) = succ(x) \<union> succ(y)"


600 
by (simp add: Memrel_fm_def succ_Un_distrib [symmetric] Un_ac)


601 


602 
lemma sats_Memrel_fm [simp]:


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


604 
==> sats(A, Memrel_fm(x,y), env) <>


605 
membership(**A, nth(x,env), nth(y,env))"


606 
by (simp add: Memrel_fm_def membership_def)

13298

607 

13306

608 
lemma Memrel_iff_sats:


609 
"[ nth(i,env) = x; nth(j,env) = y;


610 
i \<in> nat; j \<in> nat; env \<in> list(A)]


611 
==> membership(**A, x, y) <> sats(A, Memrel_fm(i,j), env)"


612 
by simp

13304

613 

13314

614 
theorem membership_reflection:


615 
"REFLECTS[\<lambda>x. membership(L,f(x),g(x)),


616 
\<lambda>i x. membership(**Lset(i),f(x),g(x))]"


617 
apply (simp only: membership_def setclass_simps)


618 
apply (intro FOL_reflection pair_reflection)


619 
done

13304

620 

13306

621 
subsubsection{*Predecessor Set*}

13304

622 

13306

623 
constdefs pred_set_fm :: "[i,i,i,i]=>i"


624 
"pred_set_fm(A,x,r,B) ==


625 
Forall(Iff(Member(0,succ(B)),


626 
Exists(And(Member(0,succ(succ(r))),


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


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


629 


630 


631 
lemma pred_set_type [TC]:


632 
"[ A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat ]


633 
==> pred_set_fm(A,x,r,B) \<in> formula"


634 
by (simp add: pred_set_fm_def)

13304

635 

13306

636 
lemma arity_pred_set_fm [simp]:


637 
"[ A \<in> nat; x \<in> nat; r \<in> nat; B \<in> nat ]


638 
==> arity(pred_set_fm(A,x,r,B)) = succ(A) \<union> succ(x) \<union> succ(r) \<union> succ(B)"


639 
by (simp add: pred_set_fm_def succ_Un_distrib [symmetric] Un_ac)


640 


641 
lemma sats_pred_set_fm [simp]:


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


643 
==> sats(A, pred_set_fm(U,x,r,B), env) <>


644 
pred_set(**A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))"


645 
by (simp add: pred_set_fm_def pred_set_def)


646 


647 
lemma pred_set_iff_sats:


648 
"[ nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B;


649 
i \<in> nat; j \<in> nat; k \<in> nat; l \<in> nat; env \<in> list(A)]


650 
==> pred_set(**A,U,x,r,B) <> sats(A, pred_set_fm(i,j,k,l), env)"


651 
by (simp add: sats_pred_set_fm)


652 

13314

653 
theorem pred_set_reflection:


654 
"REFLECTS[\<lambda>x. pred_set(L,f(x),g(x),h(x),b(x)),


655 
\<lambda>i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]"


656 
apply (simp only: pred_set_def setclass_simps)


657 
apply (intro FOL_reflection pair_reflection)


658 
done

13304

659 


660 

13298

661 

13306

662 
subsubsection{*Domain*}


663 


664 
(* "is_domain(M,r,z) ==


665 
\<forall>x[M]. (x \<in> z <> (\<exists>w[M]. w\<in>r & (\<exists>y[M]. pair(M,x,y,w))))" *)


666 
constdefs domain_fm :: "[i,i]=>i"


667 
"domain_fm(r,z) ==


668 
Forall(Iff(Member(0,succ(z)),


669 
Exists(And(Member(0,succ(succ(r))),


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


671 


672 
lemma domain_type [TC]:


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


674 
by (simp add: domain_fm_def)


675 


676 
lemma arity_domain_fm [simp]:


677 
"[ x \<in> nat; y \<in> nat ]


678 
==> arity(domain_fm(x,y)) = succ(x) \<union> succ(y)"


679 
by (simp add: domain_fm_def succ_Un_distrib [symmetric] Un_ac)


680 


681 
lemma sats_domain_fm [simp]:


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


683 
==> sats(A, domain_fm(x,y), env) <>


684 
is_domain(**A, nth(x,env), nth(y,env))"


685 
by (simp add: domain_fm_def is_domain_def)


686 


687 
lemma domain_iff_sats:


688 
"[ nth(i,env) = x; nth(j,env) = y;


689 
i \<in> nat; j \<in> nat; env \<in> list(A)]


690 
==> is_domain(**A, x, y) <> sats(A, domain_fm(i,j), env)"


691 
by simp


692 

13314

693 
theorem domain_reflection:


694 
"REFLECTS[\<lambda>x. is_domain(L,f(x),g(x)),


695 
\<lambda>i x. is_domain(**Lset(i),f(x),g(x))]"


696 
apply (simp only: is_domain_def setclass_simps)


697 
apply (intro FOL_reflection pair_reflection)


698 
done

13306

699 


700 


701 
subsubsection{*Range*}


702 


703 
(* "is_range(M,r,z) ==


704 
\<forall>y[M]. (y \<in> z <> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. pair(M,x,y,w))))" *)


705 
constdefs range_fm :: "[i,i]=>i"


706 
"range_fm(r,z) ==


707 
Forall(Iff(Member(0,succ(z)),


708 
Exists(And(Member(0,succ(succ(r))),


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


710 


711 
lemma range_type [TC]:


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


713 
by (simp add: range_fm_def)


714 


715 
lemma arity_range_fm [simp]:


716 
"[ x \<in> nat; y \<in> nat ]


717 
==> arity(range_fm(x,y)) = succ(x) \<union> succ(y)"


718 
by (simp add: range_fm_def succ_Un_distrib [symmetric] Un_ac)


719 


720 
lemma sats_range_fm [simp]:


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


722 
==> sats(A, range_fm(x,y), env) <>


723 
is_range(**A, nth(x,env), nth(y,env))"


724 
by (simp add: range_fm_def is_range_def)


725 


726 
lemma range_iff_sats:


727 
"[ nth(i,env) = x; nth(j,env) = y;


728 
i \<in> nat; j \<in> nat; env \<in> list(A)]


729 
==> is_range(**A, x, y) <> sats(A, range_fm(i,j), env)"


730 
by simp


731 

13314

732 
theorem range_reflection:


733 
"REFLECTS[\<lambda>x. is_range(L,f(x),g(x)),


734 
\<lambda>i x. is_range(**Lset(i),f(x),g(x))]"


735 
apply (simp only: is_range_def setclass_simps)


736 
apply (intro FOL_reflection pair_reflection)


737 
done

13306

738 


739 


740 
subsubsection{*Image*}


741 


742 
(* "image(M,r,A,z) ==


743 
\<forall>y[M]. (y \<in> z <> (\<exists>w[M]. w\<in>r & (\<exists>x[M]. x\<in>A & pair(M,x,y,w))))" *)


744 
constdefs image_fm :: "[i,i,i]=>i"


745 
"image_fm(r,A,z) ==


746 
Forall(Iff(Member(0,succ(z)),


747 
Exists(And(Member(0,succ(succ(r))),


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


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


750 


751 
lemma image_type [TC]:


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


753 
by (simp add: image_fm_def)


754 


755 
lemma arity_image_fm [simp]:


756 
"[ x \<in> nat; y \<in> nat; z \<in> nat ]


757 
==> arity(image_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"


758 
by (simp add: image_fm_def succ_Un_distrib [symmetric] Un_ac)


759 


760 
lemma sats_image_fm [simp]:


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


762 
==> sats(A, image_fm(x,y,z), env) <>


763 
image(**A, nth(x,env), nth(y,env), nth(z,env))"


764 
by (simp add: image_fm_def image_def)


765 


766 
lemma image_iff_sats:


767 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;


768 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)]


769 
==> image(**A, x, y, z) <> sats(A, image_fm(i,j,k), env)"


770 
by (simp add: sats_image_fm)


771 

13314

772 
theorem image_reflection:


773 
"REFLECTS[\<lambda>x. image(L,f(x),g(x),h(x)),


774 
\<lambda>i x. image(**Lset(i),f(x),g(x),h(x))]"


775 
apply (simp only: image_def setclass_simps)


776 
apply (intro FOL_reflection pair_reflection)


777 
done

13306

778 


779 


780 
subsubsection{*The Concept of Relation*}


781 


782 
(* "is_relation(M,r) ==


783 
(\<forall>z[M]. z\<in>r > (\<exists>x[M]. \<exists>y[M]. pair(M,x,y,z)))" *)


784 
constdefs relation_fm :: "i=>i"


785 
"relation_fm(r) ==


786 
Forall(Implies(Member(0,succ(r)), Exists(Exists(pair_fm(1,0,2)))))"


787 


788 
lemma relation_type [TC]:


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


790 
by (simp add: relation_fm_def)


791 


792 
lemma arity_relation_fm [simp]:


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


794 
by (simp add: relation_fm_def succ_Un_distrib [symmetric] Un_ac)


795 


796 
lemma sats_relation_fm [simp]:


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


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


799 
by (simp add: relation_fm_def is_relation_def)


800 


801 
lemma relation_iff_sats:


802 
"[ nth(i,env) = x; nth(j,env) = y;


803 
i \<in> nat; env \<in> list(A)]


804 
==> is_relation(**A, x) <> sats(A, relation_fm(i), env)"


805 
by simp


806 

13314

807 
theorem is_relation_reflection:


808 
"REFLECTS[\<lambda>x. is_relation(L,f(x)),


809 
\<lambda>i x. is_relation(**Lset(i),f(x))]"


810 
apply (simp only: is_relation_def setclass_simps)


811 
apply (intro FOL_reflection pair_reflection)


812 
done

13306

813 


814 


815 
subsubsection{*The Concept of Function*}


816 


817 
(* "is_function(M,r) ==


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


819 
pair(M,x,y,p) > pair(M,x,y',p') > p\<in>r > p'\<in>r > y=y'" *)


820 
constdefs function_fm :: "i=>i"


821 
"function_fm(r) ==


822 
Forall(Forall(Forall(Forall(Forall(


823 
Implies(pair_fm(4,3,1),


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


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


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


827 


828 
lemma function_type [TC]:


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


830 
by (simp add: function_fm_def)


831 


832 
lemma arity_function_fm [simp]:


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


834 
by (simp add: function_fm_def succ_Un_distrib [symmetric] Un_ac)


835 


836 
lemma sats_function_fm [simp]:


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


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


839 
by (simp add: function_fm_def is_function_def)


840 


841 
lemma function_iff_sats:


842 
"[ nth(i,env) = x; nth(j,env) = y;


843 
i \<in> nat; env \<in> list(A)]


844 
==> is_function(**A, x) <> sats(A, function_fm(i), env)"


845 
by simp


846 

13314

847 
theorem is_function_reflection:


848 
"REFLECTS[\<lambda>x. is_function(L,f(x)),


849 
\<lambda>i x. is_function(**Lset(i),f(x))]"


850 
apply (simp only: is_function_def setclass_simps)


851 
apply (intro FOL_reflection pair_reflection)


852 
done

13298

853 


854 

13309

855 
subsubsection{*Typed Functions*}


856 


857 
(* "typed_function(M,A,B,r) ==


858 
is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) &


859 
(\<forall>u[M]. u\<in>r > (\<forall>x[M]. \<forall>y[M]. pair(M,x,y,u) > y\<in>B))" *)


860 


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


862 
"typed_function_fm(A,B,r) ==


863 
And(function_fm(r),


864 
And(relation_fm(r),


865 
And(domain_fm(r,A),


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


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


868 


869 
lemma typed_function_type [TC]:


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


871 
by (simp add: typed_function_fm_def)


872 


873 
lemma arity_typed_function_fm [simp]:


874 
"[ x \<in> nat; y \<in> nat; z \<in> nat ]


875 
==> arity(typed_function_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"


876 
by (simp add: typed_function_fm_def succ_Un_distrib [symmetric] Un_ac)


877 


878 
lemma sats_typed_function_fm [simp]:


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


880 
==> sats(A, typed_function_fm(x,y,z), env) <>


881 
typed_function(**A, nth(x,env), nth(y,env), nth(z,env))"


882 
by (simp add: typed_function_fm_def typed_function_def)


883 


884 
lemma typed_function_iff_sats:


885 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;


886 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)]


887 
==> typed_function(**A, x, y, z) <> sats(A, typed_function_fm(i,j,k), env)"


888 
by simp


889 

13314

890 
lemmas function_reflection =


891 
upair_reflection pair_reflection union_reflection


892 
cons_reflection fun_apply_reflection subset_reflection


893 
transitive_set_reflection ordinal_reflection membership_reflection


894 
pred_set_reflection domain_reflection range_reflection image_reflection


895 
is_relation_reflection is_function_reflection

13309

896 


897 

13314

898 
theorem typed_function_reflection:


899 
"REFLECTS[\<lambda>x. typed_function(L,f(x),g(x),h(x)),


900 
\<lambda>i x. typed_function(**Lset(i),f(x),g(x),h(x))]"


901 
apply (simp only: typed_function_def setclass_simps)


902 
apply (intro FOL_reflection function_reflection)


903 
done


904 

13309

905 


906 
subsubsection{*Injections*}


907 


908 
(* "injection(M,A,B,f) ==


909 
typed_function(M,A,B,f) &


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


911 
pair(M,x,y,p) > pair(M,x',y,p') > p\<in>f > p'\<in>f > x=x')" *)


912 
constdefs injection_fm :: "[i,i,i]=>i"


913 
"injection_fm(A,B,f) ==


914 
And(typed_function_fm(A,B,f),


915 
Forall(Forall(Forall(Forall(Forall(


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


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


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


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


920 


921 


922 
lemma injection_type [TC]:


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


924 
by (simp add: injection_fm_def)


925 


926 
lemma arity_injection_fm [simp]:


927 
"[ x \<in> nat; y \<in> nat; z \<in> nat ]


928 
==> arity(injection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"


929 
by (simp add: injection_fm_def succ_Un_distrib [symmetric] Un_ac)


930 


931 
lemma sats_injection_fm [simp]:


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


933 
==> sats(A, injection_fm(x,y,z), env) <>


934 
injection(**A, nth(x,env), nth(y,env), nth(z,env))"


935 
by (simp add: injection_fm_def injection_def)


936 


937 
lemma injection_iff_sats:


938 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;


939 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)]


940 
==> injection(**A, x, y, z) <> sats(A, injection_fm(i,j,k), env)"


941 
by simp


942 

13314

943 
theorem injection_reflection:


944 
"REFLECTS[\<lambda>x. injection(L,f(x),g(x),h(x)),


945 
\<lambda>i x. injection(**Lset(i),f(x),g(x),h(x))]"


946 
apply (simp only: injection_def setclass_simps)


947 
apply (intro FOL_reflection function_reflection typed_function_reflection)


948 
done

13309

949 


950 


951 
subsubsection{*Surjections*}


952 


953 
(* surjection :: "[i=>o,i,i,i] => o"


954 
"surjection(M,A,B,f) ==


955 
typed_function(M,A,B,f) &


956 
(\<forall>y[M]. y\<in>B > (\<exists>x[M]. x\<in>A & fun_apply(M,f,x,y)))" *)


957 
constdefs surjection_fm :: "[i,i,i]=>i"


958 
"surjection_fm(A,B,f) ==


959 
And(typed_function_fm(A,B,f),


960 
Forall(Implies(Member(0,succ(B)),


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


962 
fun_apply_fm(succ(succ(f)),0,1))))))"


963 


964 
lemma surjection_type [TC]:


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


966 
by (simp add: surjection_fm_def)


967 


968 
lemma arity_surjection_fm [simp]:


969 
"[ x \<in> nat; y \<in> nat; z \<in> nat ]


970 
==> arity(surjection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"


971 
by (simp add: surjection_fm_def succ_Un_distrib [symmetric] Un_ac)


972 


973 
lemma sats_surjection_fm [simp]:


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


975 
==> sats(A, surjection_fm(x,y,z), env) <>


976 
surjection(**A, nth(x,env), nth(y,env), nth(z,env))"


977 
by (simp add: surjection_fm_def surjection_def)


978 


979 
lemma surjection_iff_sats:


980 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;


981 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)]


982 
==> surjection(**A, x, y, z) <> sats(A, surjection_fm(i,j,k), env)"


983 
by simp


984 

13314

985 
theorem surjection_reflection:


986 
"REFLECTS[\<lambda>x. surjection(L,f(x),g(x),h(x)),


987 
\<lambda>i x. surjection(**Lset(i),f(x),g(x),h(x))]"


988 
apply (simp only: surjection_def setclass_simps)


989 
apply (intro FOL_reflection function_reflection typed_function_reflection)


990 
done

13309

991 


992 


993 


994 
subsubsection{*Bijections*}


995 


996 
(* bijection :: "[i=>o,i,i,i] => o"


997 
"bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" *)


998 
constdefs bijection_fm :: "[i,i,i]=>i"


999 
"bijection_fm(A,B,f) == And(injection_fm(A,B,f), surjection_fm(A,B,f))"


1000 


1001 
lemma bijection_type [TC]:


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


1003 
by (simp add: bijection_fm_def)


1004 


1005 
lemma arity_bijection_fm [simp]:


1006 
"[ x \<in> nat; y \<in> nat; z \<in> nat ]


1007 
==> arity(bijection_fm(x,y,z)) = succ(x) \<union> succ(y) \<union> succ(z)"


1008 
by (simp add: bijection_fm_def succ_Un_distrib [symmetric] Un_ac)


1009 


1010 
lemma sats_bijection_fm [simp]:


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


1012 
==> sats(A, bijection_fm(x,y,z), env) <>


1013 
bijection(**A, nth(x,env), nth(y,env), nth(z,env))"


1014 
by (simp add: bijection_fm_def bijection_def)


1015 


1016 
lemma bijection_iff_sats:


1017 
"[ nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;


1018 
i \<in> nat; j \<in> nat; k \<in> nat; env \<in> list(A)]


1019 
==> bijection(**A, x, y, z) <> sats(A, bijection_fm(i,j,k), env)"


1020 
by simp


1021 

13314

1022 
theorem bijection_reflection:


1023 
"REFLECTS[\<lambda>x. bijection(L,f(x),g(x),h(x)),


1024 
\<lambda>i x. bijection(**Lset(i),f(x),g(x),h(x))]"


1025 
apply (simp only: bijection_def setclass_simps)


1026 
apply (intro And_reflection injection_reflection surjection_reflection)


1027 
done

13309

1028 


1029 


1030 
subsubsection{*OrderIsomorphisms*}


1031 


1032 
(* order_isomorphism :: "[i=>o,i,i,i,i,i] => o"


1033 
"order_isomorphism(M,A,r,B,s,f) ==


1034 
bijection(M,A,B,f) &


1035 
(\<forall>x[M]. x\<in>A > (\<forall>y[M]. y\<in>A >


1036 
(\<forall>p[M]. \<forall>fx[M]. \<forall>fy[M]. \<forall>q[M].


1037 
pair(M,x,y,p) > fun_apply(M,f,x,fx) > fun_apply(M,f,y,fy) >


1038 
pair(M,fx,fy,q) > (p\<in>r <> q\<in>s))))"


1039 
*)


1040 


1041 
constdefs order_isomorphism_fm :: "[i,i,i,i,i]=>i"


1042 
"order_isomorphism_fm(A,r,B,s,f) ==


1043 
And(bijection_fm(A,B,f),


1044 
Forall(Implies(Member(0,succ(A)),


1045 
Forall(Implies(Member(0,succ(succ(A))),


1046 
Forall(Forall(Forall(Forall(


1047 
Implies(pair_fm(5,4,3),


1048 
Implies(fun_apply_fm(f#+6,5,2),


1049 
Implies(fun_apply_fm(f#+6,4,1),


1050 
Implies(pair_fm(2,1,0),


1051 
Iff(Member(3,r#+6), Member(0,s#+6)))))))))))))))"


1052 


1053 
lemma order_isomorphism_type [TC]:


1054 
"[ A \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat ]


1055 
==> order_isomorphism_fm(A,r,B,s,f) \<in> formula"


1056 
by (simp add: order_isomorphism_fm_def)


1057 


1058 
lemma arity_order_isomorphism_fm [simp]:


1059 
"[ A \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat ]


1060 
==> arity(order_isomorphism_fm(A,r,B,s,f)) =


1061 
succ(A) \<union> succ(r) \<union> succ(B) \<union> succ(s) \<union> succ(f)"


1062 
by (simp add: order_isomorphism_fm_def succ_Un_distrib [symmetric] Un_ac)


1063 


1064 
lemma sats_order_isomorphism_fm [simp]:


1065 
"[ U \<in> nat; r \<in> nat; B \<in> nat; s \<in> nat; f \<in> nat; env \<in> list(A)]


1066 
==> sats(A, order_isomorphism_fm(U,r,B,s,f), env) <>


1067 
order_isomorphism(**A, nth(U,env), nth(r,env), nth(B,env),


1068 
nth(s,env), nth(f,env))"


1069 
by (simp add: order_isomorphism_fm_def order_isomorphism_def)


1070 


1071 
lemma order_isomorphism_iff_sats:


1072 
"[ nth(i,env) = U; nth(j,env) = r; nth(k,env) = B; nth(j',env) = s;


1073 
nth(k',env) = f;


1074 
i \<in> nat; j \<in> nat; k \<in> nat; j' \<in> nat; k' \<in> nat; env \<in> list(A)]


1075 
==> order_isomorphism(**A,U,r,B,s,f) <>


1076 
sats(A, order_isomorphism_fm(i,j,k,j',k'), env)"


1077 
by simp


1078 

13314

1079 
theorem order_isomorphism_reflection:


1080 
"REFLECTS[\<lambda>x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)),


1081 
\<lambda>i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"


1082 
apply (simp only: order_isomorphism_def setclass_simps)


1083 
apply (intro FOL_reflection function_reflection bijection_reflection)


1084 
done

13309

1085 

13316

1086 
lemmas fun_plus_reflection =


1087 
typed_function_reflection injection_reflection surjection_reflection


1088 
bijection_reflection order_isomorphism_reflection


1089 


1090 
lemmas fun_plus_iff_sats = upair_iff_sats pair_iff_sats union_iff_sats


1091 
cons_iff_sats fun_apply_iff_sats ordinal_iff_sats Memrel_iff_sats


1092 
pred_set_iff_sats domain_iff_sats range_iff_sats image_iff_sats


1093 
relation_iff_sats function_iff_sats typed_function_iff_sats


1094 
injection_iff_sats surjection_iff_sats bijection_iff_sats


1095 
order_isomorphism_iff_sats


1096 

13223

1097 
end
