src/ZF/Constructible/L_axioms.thy
 author paulson Wed Jul 17 15:48:54 2002 +0200 (2002-07-17) changeset 13385 31df66ca0780 parent 13363 c26eeb000470 child 13418 7c0ba9dba978 permissions -rw-r--r--
Expressing Lset and L without using length and arity; simplifies Separation
proofs
 paulson@13339 ` 1` ```header {*The ZF Axioms (Except Separation) in L*} ``` paulson@13223 ` 2` paulson@13314 ` 3` ```theory L_axioms = Formula + Relative + Reflection + MetaExists: ``` paulson@13223 ` 4` paulson@13339 ` 5` ```text {* The class L satisfies the premises of locale @{text M_triv_axioms} *} ``` paulson@13223 ` 6` paulson@13223 ` 7` ```lemma transL: "[| y\x; L(x) |] ==> L(y)" ``` paulson@13223 ` 8` ```apply (insert Transset_Lset) ``` paulson@13223 ` 9` ```apply (simp add: Transset_def L_def, blast) ``` paulson@13223 ` 10` ```done ``` paulson@13223 ` 11` paulson@13223 ` 12` ```lemma nonempty: "L(0)" ``` paulson@13223 ` 13` ```apply (simp add: L_def) ``` paulson@13223 ` 14` ```apply (blast intro: zero_in_Lset) ``` paulson@13223 ` 15` ```done ``` paulson@13223 ` 16` paulson@13223 ` 17` ```lemma upair_ax: "upair_ax(L)" ``` paulson@13223 ` 18` ```apply (simp add: upair_ax_def upair_def, clarify) ``` paulson@13299 ` 19` ```apply (rule_tac x="{x,y}" in rexI) ``` paulson@13299 ` 20` ```apply (simp_all add: doubleton_in_L) ``` paulson@13223 ` 21` ```done ``` paulson@13223 ` 22` paulson@13223 ` 23` ```lemma Union_ax: "Union_ax(L)" ``` paulson@13223 ` 24` ```apply (simp add: Union_ax_def big_union_def, clarify) ``` paulson@13299 ` 25` ```apply (rule_tac x="Union(x)" in rexI) ``` paulson@13299 ` 26` ```apply (simp_all add: Union_in_L, auto) ``` paulson@13223 ` 27` ```apply (blast intro: transL) ``` paulson@13223 ` 28` ```done ``` paulson@13223 ` 29` paulson@13223 ` 30` ```lemma power_ax: "power_ax(L)" ``` paulson@13223 ` 31` ```apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify) ``` paulson@13299 ` 32` ```apply (rule_tac x="{y \ Pow(x). L(y)}" in rexI) ``` paulson@13299 ` 33` ```apply (simp_all add: LPow_in_L, auto) ``` paulson@13223 ` 34` ```apply (blast intro: transL) ``` paulson@13223 ` 35` ```done ``` paulson@13223 ` 36` paulson@13223 ` 37` ```subsubsection{*For L to satisfy Replacement *} ``` paulson@13223 ` 38` paulson@13223 ` 39` ```(*Can't move these to Formula unless the definition of univalent is moved ``` paulson@13223 ` 40` ```there too!*) ``` paulson@13223 ` 41` paulson@13223 ` 42` ```lemma LReplace_in_Lset: ``` paulson@13223 ` 43` ``` "[|X \ Lset(i); univalent(L,X,Q); Ord(i)|] ``` paulson@13223 ` 44` ``` ==> \j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \ Lset(j)" ``` paulson@13223 ` 45` ```apply (rule_tac x="\y \ Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))" ``` paulson@13223 ` 46` ``` in exI) ``` paulson@13223 ` 47` ```apply simp ``` paulson@13223 ` 48` ```apply clarify ``` paulson@13339 ` 49` ```apply (rule_tac a=x in UN_I) ``` paulson@13223 ` 50` ``` apply (simp_all add: Replace_iff univalent_def) ``` paulson@13223 ` 51` ```apply (blast dest: transL L_I) ``` paulson@13223 ` 52` ```done ``` paulson@13223 ` 53` paulson@13223 ` 54` ```lemma LReplace_in_L: ``` paulson@13223 ` 55` ``` "[|L(X); univalent(L,X,Q)|] ``` paulson@13223 ` 56` ``` ==> \Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \ Y" ``` paulson@13223 ` 57` ```apply (drule L_D, clarify) ``` paulson@13223 ` 58` ```apply (drule LReplace_in_Lset, assumption+) ``` paulson@13223 ` 59` ```apply (blast intro: L_I Lset_in_Lset_succ) ``` paulson@13223 ` 60` ```done ``` paulson@13223 ` 61` paulson@13223 ` 62` ```lemma replacement: "replacement(L,P)" ``` paulson@13223 ` 63` ```apply (simp add: replacement_def, clarify) ``` paulson@13268 ` 64` ```apply (frule LReplace_in_L, assumption+, clarify) ``` paulson@13299 ` 65` ```apply (rule_tac x=Y in rexI) ``` paulson@13299 ` 66` ```apply (simp_all add: Replace_iff univalent_def, blast) ``` paulson@13223 ` 67` ```done ``` paulson@13223 ` 68` paulson@13363 ` 69` ```subsection{*Instantiating the locale @{text M_triv_axioms}*} ``` paulson@13363 ` 70` ```text{*No instances of Separation yet.*} ``` paulson@13291 ` 71` paulson@13291 ` 72` ```lemma Lset_mono_le: "mono_le_subset(Lset)" ``` paulson@13291 ` 73` ```by (simp add: mono_le_subset_def le_imp_subset Lset_mono) ``` paulson@13291 ` 74` paulson@13291 ` 75` ```lemma Lset_cont: "cont_Ord(Lset)" ``` paulson@13291 ` 76` ```by (simp add: cont_Ord_def Limit_Lset_eq OUnion_def Limit_is_Ord) ``` paulson@13291 ` 77` paulson@13291 ` 78` ```lemmas Pair_in_Lset = Formula.Pair_in_LLimit; ``` paulson@13291 ` 79` paulson@13291 ` 80` ```lemmas L_nat = Ord_in_L [OF Ord_nat]; ``` paulson@13291 ` 81` paulson@13291 ` 82` ```ML ``` paulson@13291 ` 83` ```{* ``` paulson@13291 ` 84` ```val transL = thm "transL"; ``` paulson@13291 ` 85` ```val nonempty = thm "nonempty"; ``` paulson@13291 ` 86` ```val upair_ax = thm "upair_ax"; ``` paulson@13291 ` 87` ```val Union_ax = thm "Union_ax"; ``` paulson@13291 ` 88` ```val power_ax = thm "power_ax"; ``` paulson@13291 ` 89` ```val replacement = thm "replacement"; ``` paulson@13291 ` 90` ```val L_nat = thm "L_nat"; ``` paulson@13291 ` 91` paulson@13291 ` 92` ```fun kill_flex_triv_prems st = Seq.hd ((REPEAT_FIRST assume_tac) st); ``` paulson@13291 ` 93` paulson@13363 ` 94` ```fun triv_axioms_L th = ``` paulson@13291 ` 95` ``` kill_flex_triv_prems ``` paulson@13291 ` 96` ``` ([transL, nonempty, upair_ax, Union_ax, power_ax, replacement, L_nat] ``` paulson@13291 ` 97` ``` MRS (inst "M" "L" th)); ``` paulson@13291 ` 98` paulson@13363 ` 99` ```bind_thm ("ball_abs", triv_axioms_L (thm "M_triv_axioms.ball_abs")); ``` paulson@13363 ` 100` ```bind_thm ("rall_abs", triv_axioms_L (thm "M_triv_axioms.rall_abs")); ``` paulson@13363 ` 101` ```bind_thm ("bex_abs", triv_axioms_L (thm "M_triv_axioms.bex_abs")); ``` paulson@13363 ` 102` ```bind_thm ("rex_abs", triv_axioms_L (thm "M_triv_axioms.rex_abs")); ``` paulson@13363 ` 103` ```bind_thm ("ball_iff_equiv", triv_axioms_L (thm "M_triv_axioms.ball_iff_equiv")); ``` paulson@13363 ` 104` ```bind_thm ("M_equalityI", triv_axioms_L (thm "M_triv_axioms.M_equalityI")); ``` paulson@13363 ` 105` ```bind_thm ("empty_abs", triv_axioms_L (thm "M_triv_axioms.empty_abs")); ``` paulson@13363 ` 106` ```bind_thm ("subset_abs", triv_axioms_L (thm "M_triv_axioms.subset_abs")); ``` paulson@13363 ` 107` ```bind_thm ("upair_abs", triv_axioms_L (thm "M_triv_axioms.upair_abs")); ``` paulson@13363 ` 108` ```bind_thm ("upair_in_M_iff", triv_axioms_L (thm "M_triv_axioms.upair_in_M_iff")); ``` paulson@13363 ` 109` ```bind_thm ("singleton_in_M_iff", triv_axioms_L (thm "M_triv_axioms.singleton_in_M_iff")); ``` paulson@13363 ` 110` ```bind_thm ("pair_abs", triv_axioms_L (thm "M_triv_axioms.pair_abs")); ``` paulson@13363 ` 111` ```bind_thm ("pair_in_M_iff", triv_axioms_L (thm "M_triv_axioms.pair_in_M_iff")); ``` paulson@13363 ` 112` ```bind_thm ("pair_components_in_M", triv_axioms_L (thm "M_triv_axioms.pair_components_in_M")); ``` paulson@13363 ` 113` ```bind_thm ("cartprod_abs", triv_axioms_L (thm "M_triv_axioms.cartprod_abs")); ``` paulson@13363 ` 114` ```bind_thm ("union_abs", triv_axioms_L (thm "M_triv_axioms.union_abs")); ``` paulson@13363 ` 115` ```bind_thm ("inter_abs", triv_axioms_L (thm "M_triv_axioms.inter_abs")); ``` paulson@13363 ` 116` ```bind_thm ("setdiff_abs", triv_axioms_L (thm "M_triv_axioms.setdiff_abs")); ``` paulson@13363 ` 117` ```bind_thm ("Union_abs", triv_axioms_L (thm "M_triv_axioms.Union_abs")); ``` paulson@13363 ` 118` ```bind_thm ("Union_closed", triv_axioms_L (thm "M_triv_axioms.Union_closed")); ``` paulson@13363 ` 119` ```bind_thm ("Un_closed", triv_axioms_L (thm "M_triv_axioms.Un_closed")); ``` paulson@13363 ` 120` ```bind_thm ("cons_closed", triv_axioms_L (thm "M_triv_axioms.cons_closed")); ``` paulson@13363 ` 121` ```bind_thm ("successor_abs", triv_axioms_L (thm "M_triv_axioms.successor_abs")); ``` paulson@13363 ` 122` ```bind_thm ("succ_in_M_iff", triv_axioms_L (thm "M_triv_axioms.succ_in_M_iff")); ``` paulson@13363 ` 123` ```bind_thm ("separation_closed", triv_axioms_L (thm "M_triv_axioms.separation_closed")); ``` paulson@13363 ` 124` ```bind_thm ("strong_replacementI", triv_axioms_L (thm "M_triv_axioms.strong_replacementI")); ``` paulson@13363 ` 125` ```bind_thm ("strong_replacement_closed", triv_axioms_L (thm "M_triv_axioms.strong_replacement_closed")); ``` paulson@13363 ` 126` ```bind_thm ("RepFun_closed", triv_axioms_L (thm "M_triv_axioms.RepFun_closed")); ``` paulson@13363 ` 127` ```bind_thm ("lam_closed", triv_axioms_L (thm "M_triv_axioms.lam_closed")); ``` paulson@13363 ` 128` ```bind_thm ("image_abs", triv_axioms_L (thm "M_triv_axioms.image_abs")); ``` paulson@13363 ` 129` ```bind_thm ("powerset_Pow", triv_axioms_L (thm "M_triv_axioms.powerset_Pow")); ``` paulson@13363 ` 130` ```bind_thm ("powerset_imp_subset_Pow", triv_axioms_L (thm "M_triv_axioms.powerset_imp_subset_Pow")); ``` paulson@13363 ` 131` ```bind_thm ("nat_into_M", triv_axioms_L (thm "M_triv_axioms.nat_into_M")); ``` paulson@13363 ` 132` ```bind_thm ("nat_case_closed", triv_axioms_L (thm "M_triv_axioms.nat_case_closed")); ``` paulson@13363 ` 133` ```bind_thm ("Inl_in_M_iff", triv_axioms_L (thm "M_triv_axioms.Inl_in_M_iff")); ``` paulson@13363 ` 134` ```bind_thm ("Inr_in_M_iff", triv_axioms_L (thm "M_triv_axioms.Inr_in_M_iff")); ``` paulson@13363 ` 135` ```bind_thm ("lt_closed", triv_axioms_L (thm "M_triv_axioms.lt_closed")); ``` paulson@13363 ` 136` ```bind_thm ("transitive_set_abs", triv_axioms_L (thm "M_triv_axioms.transitive_set_abs")); ``` paulson@13363 ` 137` ```bind_thm ("ordinal_abs", triv_axioms_L (thm "M_triv_axioms.ordinal_abs")); ``` paulson@13363 ` 138` ```bind_thm ("limit_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.limit_ordinal_abs")); ``` paulson@13363 ` 139` ```bind_thm ("successor_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.successor_ordinal_abs")); ``` paulson@13363 ` 140` ```bind_thm ("finite_ordinal_abs", triv_axioms_L (thm "M_triv_axioms.finite_ordinal_abs")); ``` paulson@13363 ` 141` ```bind_thm ("omega_abs", triv_axioms_L (thm "M_triv_axioms.omega_abs")); ``` paulson@13363 ` 142` ```bind_thm ("number1_abs", triv_axioms_L (thm "M_triv_axioms.number1_abs")); ``` paulson@13363 ` 143` ```bind_thm ("number1_abs", triv_axioms_L (thm "M_triv_axioms.number1_abs")); ``` paulson@13363 ` 144` ```bind_thm ("number3_abs", triv_axioms_L (thm "M_triv_axioms.number3_abs")); ``` paulson@13291 ` 145` ```*} ``` paulson@13291 ` 146` paulson@13291 ` 147` ```declare ball_abs [simp] ``` paulson@13291 ` 148` ```declare rall_abs [simp] ``` paulson@13291 ` 149` ```declare bex_abs [simp] ``` paulson@13291 ` 150` ```declare rex_abs [simp] ``` paulson@13291 ` 151` ```declare empty_abs [simp] ``` paulson@13291 ` 152` ```declare subset_abs [simp] ``` paulson@13291 ` 153` ```declare upair_abs [simp] ``` paulson@13291 ` 154` ```declare upair_in_M_iff [iff] ``` paulson@13291 ` 155` ```declare singleton_in_M_iff [iff] ``` paulson@13291 ` 156` ```declare pair_abs [simp] ``` paulson@13291 ` 157` ```declare pair_in_M_iff [iff] ``` paulson@13291 ` 158` ```declare cartprod_abs [simp] ``` paulson@13291 ` 159` ```declare union_abs [simp] ``` paulson@13291 ` 160` ```declare inter_abs [simp] ``` paulson@13291 ` 161` ```declare setdiff_abs [simp] ``` paulson@13291 ` 162` ```declare Union_abs [simp] ``` paulson@13291 ` 163` ```declare Union_closed [intro,simp] ``` paulson@13291 ` 164` ```declare Un_closed [intro,simp] ``` paulson@13291 ` 165` ```declare cons_closed [intro,simp] ``` paulson@13291 ` 166` ```declare successor_abs [simp] ``` paulson@13291 ` 167` ```declare succ_in_M_iff [iff] ``` paulson@13291 ` 168` ```declare separation_closed [intro,simp] ``` paulson@13306 ` 169` ```declare strong_replacementI ``` paulson@13291 ` 170` ```declare strong_replacement_closed [intro,simp] ``` paulson@13291 ` 171` ```declare RepFun_closed [intro,simp] ``` paulson@13291 ` 172` ```declare lam_closed [intro,simp] ``` paulson@13291 ` 173` ```declare image_abs [simp] ``` paulson@13291 ` 174` ```declare nat_into_M [intro] ``` paulson@13291 ` 175` ```declare Inl_in_M_iff [iff] ``` paulson@13291 ` 176` ```declare Inr_in_M_iff [iff] ``` paulson@13291 ` 177` ```declare transitive_set_abs [simp] ``` paulson@13291 ` 178` ```declare ordinal_abs [simp] ``` paulson@13291 ` 179` ```declare limit_ordinal_abs [simp] ``` paulson@13291 ` 180` ```declare successor_ordinal_abs [simp] ``` paulson@13291 ` 181` ```declare finite_ordinal_abs [simp] ``` paulson@13291 ` 182` ```declare omega_abs [simp] ``` paulson@13291 ` 183` ```declare number1_abs [simp] ``` paulson@13291 ` 184` ```declare number1_abs [simp] ``` paulson@13291 ` 185` ```declare number3_abs [simp] ``` paulson@13291 ` 186` paulson@13291 ` 187` paulson@13291 ` 188` ```subsection{*Instantiation of the locale @{text reflection}*} ``` paulson@13291 ` 189` paulson@13291 ` 190` ```text{*instances of locale constants*} ``` paulson@13291 ` 191` ```constdefs ``` paulson@13291 ` 192` ``` L_F0 :: "[i=>o,i] => i" ``` paulson@13291 ` 193` ``` "L_F0(P,y) == \b. (\z. L(z) \ P()) --> (\z\Lset(b). P())" ``` paulson@13291 ` 194` paulson@13291 ` 195` ``` L_FF :: "[i=>o,i] => i" ``` paulson@13291 ` 196` ``` "L_FF(P) == \a. \y\Lset(a). L_F0(P,y)" ``` paulson@13291 ` 197` paulson@13291 ` 198` ``` L_ClEx :: "[i=>o,i] => o" ``` paulson@13291 ` 199` ``` "L_ClEx(P) == \a. Limit(a) \ normalize(L_FF(P),a) = a" ``` paulson@13291 ` 200` paulson@13291 ` 201` paulson@13314 ` 202` ```text{*We must use the meta-existential quantifier; otherwise the reflection ``` paulson@13314 ` 203` ``` terms become enormous!*} ``` paulson@13314 ` 204` ```constdefs ``` paulson@13314 ` 205` ``` L_Reflects :: "[i=>o,[i,i]=>o] => prop" ("(3REFLECTS/ [_,/ _])") ``` paulson@13314 ` 206` ``` "REFLECTS[P,Q] == (??Cl. Closed_Unbounded(Cl) & ``` paulson@13314 ` 207` ``` (\a. Cl(a) --> (\x \ Lset(a). P(x) <-> Q(a,x))))" ``` paulson@13291 ` 208` paulson@13291 ` 209` paulson@13314 ` 210` ```theorem Triv_reflection: ``` paulson@13314 ` 211` ``` "REFLECTS[P, \a x. P(x)]" ``` paulson@13314 ` 212` ```apply (simp add: L_Reflects_def) ``` paulson@13314 ` 213` ```apply (rule meta_exI) ``` paulson@13314 ` 214` ```apply (rule Closed_Unbounded_Ord) ``` paulson@13314 ` 215` ```done ``` paulson@13314 ` 216` paulson@13314 ` 217` ```theorem Not_reflection: ``` paulson@13314 ` 218` ``` "REFLECTS[P,Q] ==> REFLECTS[\x. ~P(x), \a x. ~Q(a,x)]" ``` paulson@13314 ` 219` ```apply (unfold L_Reflects_def) ``` paulson@13314 ` 220` ```apply (erule meta_exE) ``` paulson@13314 ` 221` ```apply (rule_tac x=Cl in meta_exI, simp) ``` paulson@13314 ` 222` ```done ``` paulson@13314 ` 223` paulson@13314 ` 224` ```theorem And_reflection: ``` paulson@13314 ` 225` ``` "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |] ``` paulson@13314 ` 226` ``` ==> REFLECTS[\x. P(x) \ P'(x), \a x. Q(a,x) \ Q'(a,x)]" ``` paulson@13314 ` 227` ```apply (unfold L_Reflects_def) ``` paulson@13314 ` 228` ```apply (elim meta_exE) ``` paulson@13314 ` 229` ```apply (rule_tac x="\a. Cl(a) \ Cla(a)" in meta_exI) ``` paulson@13314 ` 230` ```apply (simp add: Closed_Unbounded_Int, blast) ``` paulson@13314 ` 231` ```done ``` paulson@13314 ` 232` paulson@13314 ` 233` ```theorem Or_reflection: ``` paulson@13314 ` 234` ``` "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |] ``` paulson@13314 ` 235` ``` ==> REFLECTS[\x. P(x) \ P'(x), \a x. Q(a,x) \ Q'(a,x)]" ``` paulson@13314 ` 236` ```apply (unfold L_Reflects_def) ``` paulson@13314 ` 237` ```apply (elim meta_exE) ``` paulson@13314 ` 238` ```apply (rule_tac x="\a. Cl(a) \ Cla(a)" in meta_exI) ``` paulson@13314 ` 239` ```apply (simp add: Closed_Unbounded_Int, blast) ``` paulson@13314 ` 240` ```done ``` paulson@13314 ` 241` paulson@13314 ` 242` ```theorem Imp_reflection: ``` paulson@13314 ` 243` ``` "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |] ``` paulson@13314 ` 244` ``` ==> REFLECTS[\x. P(x) --> P'(x), \a x. Q(a,x) --> Q'(a,x)]" ``` paulson@13314 ` 245` ```apply (unfold L_Reflects_def) ``` paulson@13314 ` 246` ```apply (elim meta_exE) ``` paulson@13314 ` 247` ```apply (rule_tac x="\a. Cl(a) \ Cla(a)" in meta_exI) ``` paulson@13314 ` 248` ```apply (simp add: Closed_Unbounded_Int, blast) ``` paulson@13314 ` 249` ```done ``` paulson@13314 ` 250` paulson@13314 ` 251` ```theorem Iff_reflection: ``` paulson@13314 ` 252` ``` "[| REFLECTS[P,Q]; REFLECTS[P',Q'] |] ``` paulson@13314 ` 253` ``` ==> REFLECTS[\x. P(x) <-> P'(x), \a x. Q(a,x) <-> Q'(a,x)]" ``` paulson@13314 ` 254` ```apply (unfold L_Reflects_def) ``` paulson@13314 ` 255` ```apply (elim meta_exE) ``` paulson@13314 ` 256` ```apply (rule_tac x="\a. Cl(a) \ Cla(a)" in meta_exI) ``` paulson@13314 ` 257` ```apply (simp add: Closed_Unbounded_Int, blast) ``` paulson@13314 ` 258` ```done ``` paulson@13314 ` 259` paulson@13314 ` 260` paulson@13314 ` 261` ```theorem Ex_reflection: ``` paulson@13314 ` 262` ``` "REFLECTS[\x. P(fst(x),snd(x)), \a x. Q(a,fst(x),snd(x))] ``` paulson@13314 ` 263` ``` ==> REFLECTS[\x. \z. L(z) \ P(x,z), \a x. \z\Lset(a). Q(a,x,z)]" ``` paulson@13291 ` 264` ```apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) ``` paulson@13314 ` 265` ```apply (elim meta_exE) ``` paulson@13314 ` 266` ```apply (rule meta_exI) ``` paulson@13291 ` 267` ```apply (rule reflection.Ex_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset], ``` paulson@13291 ` 268` ``` assumption+) ``` paulson@13291 ` 269` ```done ``` paulson@13291 ` 270` paulson@13314 ` 271` ```theorem All_reflection: ``` paulson@13314 ` 272` ``` "REFLECTS[\x. P(fst(x),snd(x)), \a x. Q(a,fst(x),snd(x))] ``` paulson@13314 ` 273` ``` ==> REFLECTS[\x. \z. L(z) --> P(x,z), \a x. \z\Lset(a). Q(a,x,z)]" ``` paulson@13291 ` 274` ```apply (unfold L_Reflects_def L_ClEx_def L_FF_def L_F0_def L_def) ``` paulson@13314 ` 275` ```apply (elim meta_exE) ``` paulson@13314 ` 276` ```apply (rule meta_exI) ``` paulson@13291 ` 277` ```apply (rule reflection.All_reflection [OF Lset_mono_le Lset_cont Pair_in_Lset], ``` paulson@13291 ` 278` ``` assumption+) ``` paulson@13291 ` 279` ```done ``` paulson@13291 ` 280` paulson@13314 ` 281` ```theorem Rex_reflection: ``` paulson@13314 ` 282` ``` "REFLECTS[ \x. P(fst(x),snd(x)), \a x. Q(a,fst(x),snd(x))] ``` paulson@13314 ` 283` ``` ==> REFLECTS[\x. \z[L]. P(x,z), \a x. \z\Lset(a). Q(a,x,z)]" ``` paulson@13314 ` 284` ```apply (unfold rex_def) ``` paulson@13314 ` 285` ```apply (intro And_reflection Ex_reflection, assumption) ``` paulson@13314 ` 286` ```done ``` paulson@13291 ` 287` paulson@13314 ` 288` ```theorem Rall_reflection: ``` paulson@13314 ` 289` ``` "REFLECTS[\x. P(fst(x),snd(x)), \a x. Q(a,fst(x),snd(x))] ``` paulson@13314 ` 290` ``` ==> REFLECTS[\x. \z[L]. P(x,z), \a x. \z\Lset(a). Q(a,x,z)]" ``` paulson@13314 ` 291` ```apply (unfold rall_def) ``` paulson@13314 ` 292` ```apply (intro Imp_reflection All_reflection, assumption) ``` paulson@13314 ` 293` ```done ``` paulson@13314 ` 294` paulson@13323 ` 295` ```lemmas FOL_reflections = ``` paulson@13314 ` 296` ``` Triv_reflection Not_reflection And_reflection Or_reflection ``` paulson@13314 ` 297` ``` Imp_reflection Iff_reflection Ex_reflection All_reflection ``` paulson@13314 ` 298` ``` Rex_reflection Rall_reflection ``` paulson@13291 ` 299` paulson@13291 ` 300` ```lemma ReflectsD: ``` paulson@13314 ` 301` ``` "[|REFLECTS[P,Q]; Ord(i)|] ``` paulson@13291 ` 302` ``` ==> \j. ix \ Lset(j). P(x) <-> Q(j,x))" ``` paulson@13314 ` 303` ```apply (unfold L_Reflects_def Closed_Unbounded_def) ``` paulson@13314 ` 304` ```apply (elim meta_exE, clarify) ``` paulson@13291 ` 305` ```apply (blast dest!: UnboundedD) ``` paulson@13291 ` 306` ```done ``` paulson@13291 ` 307` paulson@13291 ` 308` ```lemma ReflectsE: ``` paulson@13314 ` 309` ``` "[| REFLECTS[P,Q]; Ord(i); ``` paulson@13291 ` 310` ``` !!j. [|ix \ Lset(j). P(x) <-> Q(j,x)|] ==> R |] ``` paulson@13291 ` 311` ``` ==> R" ``` paulson@13316 ` 312` ```apply (drule ReflectsD, assumption, blast) ``` paulson@13314 ` 313` ```done ``` paulson@13291 ` 314` paulson@13291 ` 315` ```lemma Collect_mem_eq: "{x\A. x\B} = A \ B"; ``` paulson@13291 ` 316` ```by blast ``` paulson@13291 ` 317` paulson@13291 ` 318` paulson@13339 ` 319` ```subsection{*Internalized Formulas for some Set-Theoretic Concepts*} ``` paulson@13298 ` 320` paulson@13306 ` 321` ```lemmas setclass_simps = rall_setclass_is_ball rex_setclass_is_bex ``` paulson@13306 ` 322` paulson@13306 ` 323` ```subsubsection{*Some numbers to help write de Bruijn indices*} ``` paulson@13306 ` 324` paulson@13306 ` 325` ```syntax ``` paulson@13306 ` 326` ``` "3" :: i ("3") ``` paulson@13306 ` 327` ``` "4" :: i ("4") ``` paulson@13306 ` 328` ``` "5" :: i ("5") ``` paulson@13306 ` 329` ``` "6" :: i ("6") ``` paulson@13306 ` 330` ``` "7" :: i ("7") ``` paulson@13306 ` 331` ``` "8" :: i ("8") ``` paulson@13306 ` 332` ``` "9" :: i ("9") ``` paulson@13306 ` 333` paulson@13306 ` 334` ```translations ``` paulson@13306 ` 335` ``` "3" == "succ(2)" ``` paulson@13306 ` 336` ``` "4" == "succ(3)" ``` paulson@13306 ` 337` ``` "5" == "succ(4)" ``` paulson@13306 ` 338` ``` "6" == "succ(5)" ``` paulson@13306 ` 339` ``` "7" == "succ(6)" ``` paulson@13306 ` 340` ``` "8" == "succ(7)" ``` paulson@13306 ` 341` ``` "9" == "succ(8)" ``` paulson@13306 ` 342` paulson@13323 ` 343` paulson@13339 ` 344` ```subsubsection{*The Empty Set, Internalized*} ``` paulson@13323 ` 345` paulson@13323 ` 346` ```constdefs empty_fm :: "i=>i" ``` paulson@13323 ` 347` ``` "empty_fm(x) == Forall(Neg(Member(0,succ(x))))" ``` paulson@13323 ` 348` paulson@13323 ` 349` ```lemma empty_type [TC]: ``` paulson@13323 ` 350` ``` "x \ nat ==> empty_fm(x) \ formula" ``` paulson@13323 ` 351` ```by (simp add: empty_fm_def) ``` paulson@13323 ` 352` paulson@13323 ` 353` ```lemma arity_empty_fm [simp]: ``` paulson@13323 ` 354` ``` "x \ nat ==> arity(empty_fm(x)) = succ(x)" ``` paulson@13323 ` 355` ```by (simp add: empty_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13323 ` 356` paulson@13323 ` 357` ```lemma sats_empty_fm [simp]: ``` paulson@13323 ` 358` ``` "[| x \ nat; env \ list(A)|] ``` paulson@13323 ` 359` ``` ==> sats(A, empty_fm(x), env) <-> empty(**A, nth(x,env))" ``` paulson@13323 ` 360` ```by (simp add: empty_fm_def empty_def) ``` paulson@13323 ` 361` paulson@13323 ` 362` ```lemma empty_iff_sats: ``` paulson@13323 ` 363` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13323 ` 364` ``` i \ nat; env \ list(A)|] ``` paulson@13323 ` 365` ``` ==> empty(**A, x) <-> sats(A, empty_fm(i), env)" ``` paulson@13323 ` 366` ```by simp ``` paulson@13323 ` 367` paulson@13323 ` 368` ```theorem empty_reflection: ``` paulson@13323 ` 369` ``` "REFLECTS[\x. empty(L,f(x)), ``` paulson@13323 ` 370` ``` \i x. empty(**Lset(i),f(x))]" ``` paulson@13323 ` 371` ```apply (simp only: empty_def setclass_simps) ``` paulson@13323 ` 372` ```apply (intro FOL_reflections) ``` paulson@13323 ` 373` ```done ``` paulson@13323 ` 374` paulson@13385 ` 375` ```text{*Not used. But maybe useful?*} ``` paulson@13385 ` 376` ```lemma Transset_sats_empty_fm_eq_0: ``` paulson@13385 ` 377` ``` "[| n \ nat; env \ list(A); Transset(A)|] ``` paulson@13385 ` 378` ``` ==> sats(A, empty_fm(n), env) <-> nth(n,env) = 0" ``` paulson@13385 ` 379` ```apply (simp add: empty_fm_def empty_def Transset_def, auto) ``` paulson@13385 ` 380` ```apply (case_tac "n < length(env)") ``` paulson@13385 ` 381` ```apply (frule nth_type, assumption+, blast) ``` paulson@13385 ` 382` ```apply (simp_all add: not_lt_iff_le nth_eq_0) ``` paulson@13385 ` 383` ```done ``` paulson@13385 ` 384` paulson@13323 ` 385` paulson@13339 ` 386` ```subsubsection{*Unordered Pairs, Internalized*} ``` paulson@13298 ` 387` paulson@13298 ` 388` ```constdefs upair_fm :: "[i,i,i]=>i" ``` paulson@13298 ` 389` ``` "upair_fm(x,y,z) == ``` paulson@13298 ` 390` ``` And(Member(x,z), ``` paulson@13298 ` 391` ``` And(Member(y,z), ``` paulson@13298 ` 392` ``` Forall(Implies(Member(0,succ(z)), ``` paulson@13298 ` 393` ``` Or(Equal(0,succ(x)), Equal(0,succ(y)))))))" ``` paulson@13298 ` 394` paulson@13298 ` 395` ```lemma upair_type [TC]: ``` paulson@13298 ` 396` ``` "[| x \ nat; y \ nat; z \ nat |] ==> upair_fm(x,y,z) \ formula" ``` paulson@13298 ` 397` ```by (simp add: upair_fm_def) ``` paulson@13298 ` 398` paulson@13298 ` 399` ```lemma arity_upair_fm [simp]: ``` paulson@13298 ` 400` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13298 ` 401` ``` ==> arity(upair_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13298 ` 402` ```by (simp add: upair_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13298 ` 403` paulson@13298 ` 404` ```lemma sats_upair_fm [simp]: ``` paulson@13298 ` 405` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13298 ` 406` ``` ==> sats(A, upair_fm(x,y,z), env) <-> ``` paulson@13298 ` 407` ``` upair(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13298 ` 408` ```by (simp add: upair_fm_def upair_def) ``` paulson@13298 ` 409` paulson@13298 ` 410` ```lemma upair_iff_sats: ``` paulson@13298 ` 411` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13298 ` 412` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13298 ` 413` ``` ==> upair(**A, x, y, z) <-> sats(A, upair_fm(i,j,k), env)" ``` paulson@13298 ` 414` ```by (simp add: sats_upair_fm) ``` paulson@13298 ` 415` paulson@13298 ` 416` ```text{*Useful? At least it refers to "real" unordered pairs*} ``` paulson@13298 ` 417` ```lemma sats_upair_fm2 [simp]: ``` paulson@13298 ` 418` ``` "[| x \ nat; y \ nat; z < length(env); env \ list(A); Transset(A)|] ``` paulson@13298 ` 419` ``` ==> sats(A, upair_fm(x,y,z), env) <-> ``` paulson@13298 ` 420` ``` nth(z,env) = {nth(x,env), nth(y,env)}" ``` paulson@13298 ` 421` ```apply (frule lt_length_in_nat, assumption) ``` paulson@13298 ` 422` ```apply (simp add: upair_fm_def Transset_def, auto) ``` paulson@13298 ` 423` ```apply (blast intro: nth_type) ``` paulson@13298 ` 424` ```done ``` paulson@13298 ` 425` paulson@13314 ` 426` ```theorem upair_reflection: ``` paulson@13314 ` 427` ``` "REFLECTS[\x. upair(L,f(x),g(x),h(x)), ``` paulson@13314 ` 428` ``` \i x. upair(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 429` ```apply (simp add: upair_def) ``` paulson@13323 ` 430` ```apply (intro FOL_reflections) ``` paulson@13314 ` 431` ```done ``` paulson@13306 ` 432` paulson@13339 ` 433` ```subsubsection{*Ordered pairs, Internalized*} ``` paulson@13298 ` 434` paulson@13298 ` 435` ```constdefs pair_fm :: "[i,i,i]=>i" ``` paulson@13298 ` 436` ``` "pair_fm(x,y,z) == ``` paulson@13298 ` 437` ``` Exists(And(upair_fm(succ(x),succ(x),0), ``` paulson@13298 ` 438` ``` Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0), ``` paulson@13298 ` 439` ``` upair_fm(1,0,succ(succ(z)))))))" ``` paulson@13298 ` 440` paulson@13298 ` 441` ```lemma pair_type [TC]: ``` paulson@13298 ` 442` ``` "[| x \ nat; y \ nat; z \ nat |] ==> pair_fm(x,y,z) \ formula" ``` paulson@13298 ` 443` ```by (simp add: pair_fm_def) ``` paulson@13298 ` 444` paulson@13298 ` 445` ```lemma arity_pair_fm [simp]: ``` paulson@13298 ` 446` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13298 ` 447` ``` ==> arity(pair_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13298 ` 448` ```by (simp add: pair_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13298 ` 449` paulson@13298 ` 450` ```lemma sats_pair_fm [simp]: ``` paulson@13298 ` 451` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13298 ` 452` ``` ==> sats(A, pair_fm(x,y,z), env) <-> ``` paulson@13298 ` 453` ``` pair(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13298 ` 454` ```by (simp add: pair_fm_def pair_def) ``` paulson@13298 ` 455` paulson@13298 ` 456` ```lemma pair_iff_sats: ``` paulson@13298 ` 457` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13298 ` 458` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13298 ` 459` ``` ==> pair(**A, x, y, z) <-> sats(A, pair_fm(i,j,k), env)" ``` paulson@13298 ` 460` ```by (simp add: sats_pair_fm) ``` paulson@13298 ` 461` paulson@13314 ` 462` ```theorem pair_reflection: ``` paulson@13314 ` 463` ``` "REFLECTS[\x. pair(L,f(x),g(x),h(x)), ``` paulson@13314 ` 464` ``` \i x. pair(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 465` ```apply (simp only: pair_def setclass_simps) ``` paulson@13323 ` 466` ```apply (intro FOL_reflections upair_reflection) ``` paulson@13314 ` 467` ```done ``` paulson@13306 ` 468` paulson@13306 ` 469` paulson@13339 ` 470` ```subsubsection{*Binary Unions, Internalized*} ``` paulson@13298 ` 471` paulson@13306 ` 472` ```constdefs union_fm :: "[i,i,i]=>i" ``` paulson@13306 ` 473` ``` "union_fm(x,y,z) == ``` paulson@13306 ` 474` ``` Forall(Iff(Member(0,succ(z)), ``` paulson@13306 ` 475` ``` Or(Member(0,succ(x)),Member(0,succ(y)))))" ``` paulson@13306 ` 476` paulson@13306 ` 477` ```lemma union_type [TC]: ``` paulson@13306 ` 478` ``` "[| x \ nat; y \ nat; z \ nat |] ==> union_fm(x,y,z) \ formula" ``` paulson@13306 ` 479` ```by (simp add: union_fm_def) ``` paulson@13306 ` 480` paulson@13306 ` 481` ```lemma arity_union_fm [simp]: ``` paulson@13306 ` 482` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13306 ` 483` ``` ==> arity(union_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13306 ` 484` ```by (simp add: union_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13298 ` 485` paulson@13306 ` 486` ```lemma sats_union_fm [simp]: ``` paulson@13306 ` 487` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13306 ` 488` ``` ==> sats(A, union_fm(x,y,z), env) <-> ``` paulson@13306 ` 489` ``` union(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13306 ` 490` ```by (simp add: union_fm_def union_def) ``` paulson@13306 ` 491` paulson@13306 ` 492` ```lemma union_iff_sats: ``` paulson@13306 ` 493` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13306 ` 494` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13306 ` 495` ``` ==> union(**A, x, y, z) <-> sats(A, union_fm(i,j,k), env)" ``` paulson@13306 ` 496` ```by (simp add: sats_union_fm) ``` paulson@13298 ` 497` paulson@13314 ` 498` ```theorem union_reflection: ``` paulson@13314 ` 499` ``` "REFLECTS[\x. union(L,f(x),g(x),h(x)), ``` paulson@13314 ` 500` ``` \i x. union(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 501` ```apply (simp only: union_def setclass_simps) ``` paulson@13323 ` 502` ```apply (intro FOL_reflections) ``` paulson@13314 ` 503` ```done ``` paulson@13306 ` 504` paulson@13298 ` 505` paulson@13339 ` 506` ```subsubsection{*Set ``Cons,'' Internalized*} ``` paulson@13306 ` 507` paulson@13306 ` 508` ```constdefs cons_fm :: "[i,i,i]=>i" ``` paulson@13306 ` 509` ``` "cons_fm(x,y,z) == ``` paulson@13306 ` 510` ``` Exists(And(upair_fm(succ(x),succ(x),0), ``` paulson@13306 ` 511` ``` union_fm(0,succ(y),succ(z))))" ``` paulson@13298 ` 512` paulson@13298 ` 513` paulson@13306 ` 514` ```lemma cons_type [TC]: ``` paulson@13306 ` 515` ``` "[| x \ nat; y \ nat; z \ nat |] ==> cons_fm(x,y,z) \ formula" ``` paulson@13306 ` 516` ```by (simp add: cons_fm_def) ``` paulson@13306 ` 517` paulson@13306 ` 518` ```lemma arity_cons_fm [simp]: ``` paulson@13306 ` 519` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13306 ` 520` ``` ==> arity(cons_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13306 ` 521` ```by (simp add: cons_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 522` paulson@13306 ` 523` ```lemma sats_cons_fm [simp]: ``` paulson@13306 ` 524` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13306 ` 525` ``` ==> sats(A, cons_fm(x,y,z), env) <-> ``` paulson@13306 ` 526` ``` is_cons(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13306 ` 527` ```by (simp add: cons_fm_def is_cons_def) ``` paulson@13306 ` 528` paulson@13306 ` 529` ```lemma cons_iff_sats: ``` paulson@13306 ` 530` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13306 ` 531` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13306 ` 532` ``` ==> is_cons(**A, x, y, z) <-> sats(A, cons_fm(i,j,k), env)" ``` paulson@13306 ` 533` ```by simp ``` paulson@13306 ` 534` paulson@13314 ` 535` ```theorem cons_reflection: ``` paulson@13314 ` 536` ``` "REFLECTS[\x. is_cons(L,f(x),g(x),h(x)), ``` paulson@13314 ` 537` ``` \i x. is_cons(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 538` ```apply (simp only: is_cons_def setclass_simps) ``` paulson@13323 ` 539` ```apply (intro FOL_reflections upair_reflection union_reflection) ``` paulson@13323 ` 540` ```done ``` paulson@13323 ` 541` paulson@13323 ` 542` paulson@13339 ` 543` ```subsubsection{*Successor Function, Internalized*} ``` paulson@13323 ` 544` paulson@13323 ` 545` ```constdefs succ_fm :: "[i,i]=>i" ``` paulson@13323 ` 546` ``` "succ_fm(x,y) == cons_fm(x,x,y)" ``` paulson@13323 ` 547` paulson@13323 ` 548` ```lemma succ_type [TC]: ``` paulson@13323 ` 549` ``` "[| x \ nat; y \ nat |] ==> succ_fm(x,y) \ formula" ``` paulson@13323 ` 550` ```by (simp add: succ_fm_def) ``` paulson@13323 ` 551` paulson@13323 ` 552` ```lemma arity_succ_fm [simp]: ``` paulson@13323 ` 553` ``` "[| x \ nat; y \ nat |] ``` paulson@13323 ` 554` ``` ==> arity(succ_fm(x,y)) = succ(x) \ succ(y)" ``` paulson@13323 ` 555` ```by (simp add: succ_fm_def) ``` paulson@13323 ` 556` paulson@13323 ` 557` ```lemma sats_succ_fm [simp]: ``` paulson@13323 ` 558` ``` "[| x \ nat; y \ nat; env \ list(A)|] ``` paulson@13323 ` 559` ``` ==> sats(A, succ_fm(x,y), env) <-> ``` paulson@13323 ` 560` ``` successor(**A, nth(x,env), nth(y,env))" ``` paulson@13323 ` 561` ```by (simp add: succ_fm_def successor_def) ``` paulson@13323 ` 562` paulson@13323 ` 563` ```lemma successor_iff_sats: ``` paulson@13323 ` 564` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13323 ` 565` ``` i \ nat; j \ nat; env \ list(A)|] ``` paulson@13323 ` 566` ``` ==> successor(**A, x, y) <-> sats(A, succ_fm(i,j), env)" ``` paulson@13323 ` 567` ```by simp ``` paulson@13323 ` 568` paulson@13323 ` 569` ```theorem successor_reflection: ``` paulson@13323 ` 570` ``` "REFLECTS[\x. successor(L,f(x),g(x)), ``` paulson@13323 ` 571` ``` \i x. successor(**Lset(i),f(x),g(x))]" ``` paulson@13323 ` 572` ```apply (simp only: successor_def setclass_simps) ``` paulson@13323 ` 573` ```apply (intro cons_reflection) ``` paulson@13314 ` 574` ```done ``` paulson@13298 ` 575` paulson@13298 ` 576` paulson@13363 ` 577` ```subsubsection{*The Number 1, Internalized*} ``` paulson@13363 ` 578` paulson@13363 ` 579` ```(* "number1(M,a) == (\x[M]. empty(M,x) & successor(M,x,a))" *) ``` paulson@13363 ` 580` ```constdefs number1_fm :: "i=>i" ``` paulson@13363 ` 581` ``` "number1_fm(a) == Exists(And(empty_fm(0), succ_fm(0,succ(a))))" ``` paulson@13363 ` 582` paulson@13363 ` 583` ```lemma number1_type [TC]: ``` paulson@13363 ` 584` ``` "x \ nat ==> number1_fm(x) \ formula" ``` paulson@13363 ` 585` ```by (simp add: number1_fm_def) ``` paulson@13363 ` 586` paulson@13363 ` 587` ```lemma arity_number1_fm [simp]: ``` paulson@13363 ` 588` ``` "x \ nat ==> arity(number1_fm(x)) = succ(x)" ``` paulson@13363 ` 589` ```by (simp add: number1_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13363 ` 590` paulson@13363 ` 591` ```lemma sats_number1_fm [simp]: ``` paulson@13363 ` 592` ``` "[| x \ nat; env \ list(A)|] ``` paulson@13363 ` 593` ``` ==> sats(A, number1_fm(x), env) <-> number1(**A, nth(x,env))" ``` paulson@13363 ` 594` ```by (simp add: number1_fm_def number1_def) ``` paulson@13363 ` 595` paulson@13363 ` 596` ```lemma number1_iff_sats: ``` paulson@13363 ` 597` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13363 ` 598` ``` i \ nat; env \ list(A)|] ``` paulson@13363 ` 599` ``` ==> number1(**A, x) <-> sats(A, number1_fm(i), env)" ``` paulson@13363 ` 600` ```by simp ``` paulson@13363 ` 601` paulson@13363 ` 602` ```theorem number1_reflection: ``` paulson@13363 ` 603` ``` "REFLECTS[\x. number1(L,f(x)), ``` paulson@13363 ` 604` ``` \i x. number1(**Lset(i),f(x))]" ``` paulson@13363 ` 605` ```apply (simp only: number1_def setclass_simps) ``` paulson@13363 ` 606` ```apply (intro FOL_reflections empty_reflection successor_reflection) ``` paulson@13363 ` 607` ```done ``` paulson@13363 ` 608` paulson@13363 ` 609` paulson@13352 ` 610` ```subsubsection{*Big Union, Internalized*} ``` paulson@13306 ` 611` paulson@13352 ` 612` ```(* "big_union(M,A,z) == \x[M]. x \ z <-> (\y[M]. y\A & x \ y)" *) ``` paulson@13352 ` 613` ```constdefs big_union_fm :: "[i,i]=>i" ``` paulson@13352 ` 614` ``` "big_union_fm(A,z) == ``` paulson@13352 ` 615` ``` Forall(Iff(Member(0,succ(z)), ``` paulson@13352 ` 616` ``` Exists(And(Member(0,succ(succ(A))), Member(1,0)))))" ``` paulson@13298 ` 617` paulson@13352 ` 618` ```lemma big_union_type [TC]: ``` paulson@13352 ` 619` ``` "[| x \ nat; y \ nat |] ==> big_union_fm(x,y) \ formula" ``` paulson@13352 ` 620` ```by (simp add: big_union_fm_def) ``` paulson@13306 ` 621` paulson@13352 ` 622` ```lemma arity_big_union_fm [simp]: ``` paulson@13352 ` 623` ``` "[| x \ nat; y \ nat |] ``` paulson@13352 ` 624` ``` ==> arity(big_union_fm(x,y)) = succ(x) \ succ(y)" ``` paulson@13352 ` 625` ```by (simp add: big_union_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13298 ` 626` paulson@13352 ` 627` ```lemma sats_big_union_fm [simp]: ``` paulson@13352 ` 628` ``` "[| x \ nat; y \ nat; env \ list(A)|] ``` paulson@13352 ` 629` ``` ==> sats(A, big_union_fm(x,y), env) <-> ``` paulson@13352 ` 630` ``` big_union(**A, nth(x,env), nth(y,env))" ``` paulson@13352 ` 631` ```by (simp add: big_union_fm_def big_union_def) ``` paulson@13306 ` 632` paulson@13352 ` 633` ```lemma big_union_iff_sats: ``` paulson@13352 ` 634` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13352 ` 635` ``` i \ nat; j \ nat; env \ list(A)|] ``` paulson@13352 ` 636` ``` ==> big_union(**A, x, y) <-> sats(A, big_union_fm(i,j), env)" ``` paulson@13306 ` 637` ```by simp ``` paulson@13306 ` 638` paulson@13352 ` 639` ```theorem big_union_reflection: ``` paulson@13352 ` 640` ``` "REFLECTS[\x. big_union(L,f(x),g(x)), ``` paulson@13352 ` 641` ``` \i x. big_union(**Lset(i),f(x),g(x))]" ``` paulson@13352 ` 642` ```apply (simp only: big_union_def setclass_simps) ``` paulson@13352 ` 643` ```apply (intro FOL_reflections) ``` paulson@13314 ` 644` ```done ``` paulson@13298 ` 645` paulson@13298 ` 646` paulson@13306 ` 647` ```subsubsection{*Variants of Satisfaction Definitions for Ordinals, etc.*} ``` paulson@13306 ` 648` paulson@13306 ` 649` ```text{*Differs from the one in Formula by using "ordinal" rather than "Ord"*} ``` paulson@13306 ` 650` paulson@13306 ` 651` paulson@13306 ` 652` ```lemma sats_subset_fm': ``` paulson@13306 ` 653` ``` "[|x \ nat; y \ nat; env \ list(A)|] ``` paulson@13306 ` 654` ``` ==> sats(A, subset_fm(x,y), env) <-> subset(**A, nth(x,env), nth(y,env))" ``` paulson@13323 ` 655` ```by (simp add: subset_fm_def Relative.subset_def) ``` paulson@13298 ` 656` paulson@13314 ` 657` ```theorem subset_reflection: ``` paulson@13314 ` 658` ``` "REFLECTS[\x. subset(L,f(x),g(x)), ``` paulson@13314 ` 659` ``` \i x. subset(**Lset(i),f(x),g(x))]" ``` paulson@13323 ` 660` ```apply (simp only: Relative.subset_def setclass_simps) ``` paulson@13323 ` 661` ```apply (intro FOL_reflections) ``` paulson@13314 ` 662` ```done ``` paulson@13306 ` 663` paulson@13306 ` 664` ```lemma sats_transset_fm': ``` paulson@13306 ` 665` ``` "[|x \ nat; env \ list(A)|] ``` paulson@13306 ` 666` ``` ==> sats(A, transset_fm(x), env) <-> transitive_set(**A, nth(x,env))" ``` paulson@13306 ` 667` ```by (simp add: sats_subset_fm' transset_fm_def transitive_set_def) ``` paulson@13298 ` 668` paulson@13314 ` 669` ```theorem transitive_set_reflection: ``` paulson@13314 ` 670` ``` "REFLECTS[\x. transitive_set(L,f(x)), ``` paulson@13314 ` 671` ``` \i x. transitive_set(**Lset(i),f(x))]" ``` paulson@13314 ` 672` ```apply (simp only: transitive_set_def setclass_simps) ``` paulson@13323 ` 673` ```apply (intro FOL_reflections subset_reflection) ``` paulson@13314 ` 674` ```done ``` paulson@13306 ` 675` paulson@13306 ` 676` ```lemma sats_ordinal_fm': ``` paulson@13306 ` 677` ``` "[|x \ nat; env \ list(A)|] ``` paulson@13306 ` 678` ``` ==> sats(A, ordinal_fm(x), env) <-> ordinal(**A,nth(x,env))" ``` paulson@13306 ` 679` ```by (simp add: sats_transset_fm' ordinal_fm_def ordinal_def) ``` paulson@13306 ` 680` paulson@13306 ` 681` ```lemma ordinal_iff_sats: ``` paulson@13306 ` 682` ``` "[| nth(i,env) = x; i \ nat; env \ list(A)|] ``` paulson@13306 ` 683` ``` ==> ordinal(**A, x) <-> sats(A, ordinal_fm(i), env)" ``` paulson@13306 ` 684` ```by (simp add: sats_ordinal_fm') ``` paulson@13306 ` 685` paulson@13314 ` 686` ```theorem ordinal_reflection: ``` paulson@13314 ` 687` ``` "REFLECTS[\x. ordinal(L,f(x)), \i x. ordinal(**Lset(i),f(x))]" ``` paulson@13314 ` 688` ```apply (simp only: ordinal_def setclass_simps) ``` paulson@13323 ` 689` ```apply (intro FOL_reflections transitive_set_reflection) ``` paulson@13314 ` 690` ```done ``` paulson@13298 ` 691` paulson@13298 ` 692` paulson@13339 ` 693` ```subsubsection{*Membership Relation, Internalized*} ``` paulson@13298 ` 694` paulson@13306 ` 695` ```constdefs Memrel_fm :: "[i,i]=>i" ``` paulson@13306 ` 696` ``` "Memrel_fm(A,r) == ``` paulson@13306 ` 697` ``` Forall(Iff(Member(0,succ(r)), ``` paulson@13306 ` 698` ``` Exists(And(Member(0,succ(succ(A))), ``` paulson@13306 ` 699` ``` Exists(And(Member(0,succ(succ(succ(A)))), ``` paulson@13306 ` 700` ``` And(Member(1,0), ``` paulson@13306 ` 701` ``` pair_fm(1,0,2))))))))" ``` paulson@13306 ` 702` paulson@13306 ` 703` ```lemma Memrel_type [TC]: ``` paulson@13306 ` 704` ``` "[| x \ nat; y \ nat |] ==> Memrel_fm(x,y) \ formula" ``` paulson@13306 ` 705` ```by (simp add: Memrel_fm_def) ``` paulson@13298 ` 706` paulson@13306 ` 707` ```lemma arity_Memrel_fm [simp]: ``` paulson@13306 ` 708` ``` "[| x \ nat; y \ nat |] ``` paulson@13306 ` 709` ``` ==> arity(Memrel_fm(x,y)) = succ(x) \ succ(y)" ``` paulson@13306 ` 710` ```by (simp add: Memrel_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 711` paulson@13306 ` 712` ```lemma sats_Memrel_fm [simp]: ``` paulson@13306 ` 713` ``` "[| x \ nat; y \ nat; env \ list(A)|] ``` paulson@13306 ` 714` ``` ==> sats(A, Memrel_fm(x,y), env) <-> ``` paulson@13306 ` 715` ``` membership(**A, nth(x,env), nth(y,env))" ``` paulson@13306 ` 716` ```by (simp add: Memrel_fm_def membership_def) ``` paulson@13298 ` 717` paulson@13306 ` 718` ```lemma Memrel_iff_sats: ``` paulson@13306 ` 719` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13306 ` 720` ``` i \ nat; j \ nat; env \ list(A)|] ``` paulson@13306 ` 721` ``` ==> membership(**A, x, y) <-> sats(A, Memrel_fm(i,j), env)" ``` paulson@13306 ` 722` ```by simp ``` paulson@13304 ` 723` paulson@13314 ` 724` ```theorem membership_reflection: ``` paulson@13314 ` 725` ``` "REFLECTS[\x. membership(L,f(x),g(x)), ``` paulson@13314 ` 726` ``` \i x. membership(**Lset(i),f(x),g(x))]" ``` paulson@13314 ` 727` ```apply (simp only: membership_def setclass_simps) ``` paulson@13323 ` 728` ```apply (intro FOL_reflections pair_reflection) ``` paulson@13314 ` 729` ```done ``` paulson@13304 ` 730` paulson@13339 ` 731` ```subsubsection{*Predecessor Set, Internalized*} ``` paulson@13304 ` 732` paulson@13306 ` 733` ```constdefs pred_set_fm :: "[i,i,i,i]=>i" ``` paulson@13306 ` 734` ``` "pred_set_fm(A,x,r,B) == ``` paulson@13306 ` 735` ``` Forall(Iff(Member(0,succ(B)), ``` paulson@13306 ` 736` ``` Exists(And(Member(0,succ(succ(r))), ``` paulson@13306 ` 737` ``` And(Member(1,succ(succ(A))), ``` paulson@13306 ` 738` ``` pair_fm(1,succ(succ(x)),0))))))" ``` paulson@13306 ` 739` paulson@13306 ` 740` paulson@13306 ` 741` ```lemma pred_set_type [TC]: ``` paulson@13306 ` 742` ``` "[| A \ nat; x \ nat; r \ nat; B \ nat |] ``` paulson@13306 ` 743` ``` ==> pred_set_fm(A,x,r,B) \ formula" ``` paulson@13306 ` 744` ```by (simp add: pred_set_fm_def) ``` paulson@13304 ` 745` paulson@13306 ` 746` ```lemma arity_pred_set_fm [simp]: ``` paulson@13306 ` 747` ``` "[| A \ nat; x \ nat; r \ nat; B \ nat |] ``` paulson@13306 ` 748` ``` ==> arity(pred_set_fm(A,x,r,B)) = succ(A) \ succ(x) \ succ(r) \ succ(B)" ``` paulson@13306 ` 749` ```by (simp add: pred_set_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 750` paulson@13306 ` 751` ```lemma sats_pred_set_fm [simp]: ``` paulson@13306 ` 752` ``` "[| U \ nat; x \ nat; r \ nat; B \ nat; env \ list(A)|] ``` paulson@13306 ` 753` ``` ==> sats(A, pred_set_fm(U,x,r,B), env) <-> ``` paulson@13306 ` 754` ``` pred_set(**A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))" ``` paulson@13306 ` 755` ```by (simp add: pred_set_fm_def pred_set_def) ``` paulson@13306 ` 756` paulson@13306 ` 757` ```lemma pred_set_iff_sats: ``` paulson@13306 ` 758` ``` "[| nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B; ``` paulson@13306 ` 759` ``` i \ nat; j \ nat; k \ nat; l \ nat; env \ list(A)|] ``` paulson@13306 ` 760` ``` ==> pred_set(**A,U,x,r,B) <-> sats(A, pred_set_fm(i,j,k,l), env)" ``` paulson@13306 ` 761` ```by (simp add: sats_pred_set_fm) ``` paulson@13306 ` 762` paulson@13314 ` 763` ```theorem pred_set_reflection: ``` paulson@13314 ` 764` ``` "REFLECTS[\x. pred_set(L,f(x),g(x),h(x),b(x)), ``` paulson@13314 ` 765` ``` \i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]" ``` paulson@13314 ` 766` ```apply (simp only: pred_set_def setclass_simps) ``` paulson@13323 ` 767` ```apply (intro FOL_reflections pair_reflection) ``` paulson@13314 ` 768` ```done ``` paulson@13304 ` 769` paulson@13304 ` 770` paulson@13298 ` 771` paulson@13339 ` 772` ```subsubsection{*Domain of a Relation, Internalized*} ``` paulson@13306 ` 773` paulson@13306 ` 774` ```(* "is_domain(M,r,z) == ``` paulson@13306 ` 775` ``` \x[M]. (x \ z <-> (\w[M]. w\r & (\y[M]. pair(M,x,y,w))))" *) ``` paulson@13306 ` 776` ```constdefs domain_fm :: "[i,i]=>i" ``` paulson@13306 ` 777` ``` "domain_fm(r,z) == ``` paulson@13306 ` 778` ``` Forall(Iff(Member(0,succ(z)), ``` paulson@13306 ` 779` ``` Exists(And(Member(0,succ(succ(r))), ``` paulson@13306 ` 780` ``` Exists(pair_fm(2,0,1))))))" ``` paulson@13306 ` 781` paulson@13306 ` 782` ```lemma domain_type [TC]: ``` paulson@13306 ` 783` ``` "[| x \ nat; y \ nat |] ==> domain_fm(x,y) \ formula" ``` paulson@13306 ` 784` ```by (simp add: domain_fm_def) ``` paulson@13306 ` 785` paulson@13306 ` 786` ```lemma arity_domain_fm [simp]: ``` paulson@13306 ` 787` ``` "[| x \ nat; y \ nat |] ``` paulson@13306 ` 788` ``` ==> arity(domain_fm(x,y)) = succ(x) \ succ(y)" ``` paulson@13306 ` 789` ```by (simp add: domain_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 790` paulson@13306 ` 791` ```lemma sats_domain_fm [simp]: ``` paulson@13306 ` 792` ``` "[| x \ nat; y \ nat; env \ list(A)|] ``` paulson@13306 ` 793` ``` ==> sats(A, domain_fm(x,y), env) <-> ``` paulson@13306 ` 794` ``` is_domain(**A, nth(x,env), nth(y,env))" ``` paulson@13306 ` 795` ```by (simp add: domain_fm_def is_domain_def) ``` paulson@13306 ` 796` paulson@13306 ` 797` ```lemma domain_iff_sats: ``` paulson@13306 ` 798` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13306 ` 799` ``` i \ nat; j \ nat; env \ list(A)|] ``` paulson@13306 ` 800` ``` ==> is_domain(**A, x, y) <-> sats(A, domain_fm(i,j), env)" ``` paulson@13306 ` 801` ```by simp ``` paulson@13306 ` 802` paulson@13314 ` 803` ```theorem domain_reflection: ``` paulson@13314 ` 804` ``` "REFLECTS[\x. is_domain(L,f(x),g(x)), ``` paulson@13314 ` 805` ``` \i x. is_domain(**Lset(i),f(x),g(x))]" ``` paulson@13314 ` 806` ```apply (simp only: is_domain_def setclass_simps) ``` paulson@13323 ` 807` ```apply (intro FOL_reflections pair_reflection) ``` paulson@13314 ` 808` ```done ``` paulson@13306 ` 809` paulson@13306 ` 810` paulson@13339 ` 811` ```subsubsection{*Range of a Relation, Internalized*} ``` paulson@13306 ` 812` paulson@13306 ` 813` ```(* "is_range(M,r,z) == ``` paulson@13306 ` 814` ``` \y[M]. (y \ z <-> (\w[M]. w\r & (\x[M]. pair(M,x,y,w))))" *) ``` paulson@13306 ` 815` ```constdefs range_fm :: "[i,i]=>i" ``` paulson@13306 ` 816` ``` "range_fm(r,z) == ``` paulson@13306 ` 817` ``` Forall(Iff(Member(0,succ(z)), ``` paulson@13306 ` 818` ``` Exists(And(Member(0,succ(succ(r))), ``` paulson@13306 ` 819` ``` Exists(pair_fm(0,2,1))))))" ``` paulson@13306 ` 820` paulson@13306 ` 821` ```lemma range_type [TC]: ``` paulson@13306 ` 822` ``` "[| x \ nat; y \ nat |] ==> range_fm(x,y) \ formula" ``` paulson@13306 ` 823` ```by (simp add: range_fm_def) ``` paulson@13306 ` 824` paulson@13306 ` 825` ```lemma arity_range_fm [simp]: ``` paulson@13306 ` 826` ``` "[| x \ nat; y \ nat |] ``` paulson@13306 ` 827` ``` ==> arity(range_fm(x,y)) = succ(x) \ succ(y)" ``` paulson@13306 ` 828` ```by (simp add: range_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 829` paulson@13306 ` 830` ```lemma sats_range_fm [simp]: ``` paulson@13306 ` 831` ``` "[| x \ nat; y \ nat; env \ list(A)|] ``` paulson@13306 ` 832` ``` ==> sats(A, range_fm(x,y), env) <-> ``` paulson@13306 ` 833` ``` is_range(**A, nth(x,env), nth(y,env))" ``` paulson@13306 ` 834` ```by (simp add: range_fm_def is_range_def) ``` paulson@13306 ` 835` paulson@13306 ` 836` ```lemma range_iff_sats: ``` paulson@13306 ` 837` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13306 ` 838` ``` i \ nat; j \ nat; env \ list(A)|] ``` paulson@13306 ` 839` ``` ==> is_range(**A, x, y) <-> sats(A, range_fm(i,j), env)" ``` paulson@13306 ` 840` ```by simp ``` paulson@13306 ` 841` paulson@13314 ` 842` ```theorem range_reflection: ``` paulson@13314 ` 843` ``` "REFLECTS[\x. is_range(L,f(x),g(x)), ``` paulson@13314 ` 844` ``` \i x. is_range(**Lset(i),f(x),g(x))]" ``` paulson@13314 ` 845` ```apply (simp only: is_range_def setclass_simps) ``` paulson@13323 ` 846` ```apply (intro FOL_reflections pair_reflection) ``` paulson@13314 ` 847` ```done ``` paulson@13306 ` 848` paulson@13306 ` 849` ``` ``` paulson@13339 ` 850` ```subsubsection{*Field of a Relation, Internalized*} ``` paulson@13323 ` 851` paulson@13323 ` 852` ```(* "is_field(M,r,z) == ``` paulson@13323 ` 853` ``` \dr[M]. is_domain(M,r,dr) & ``` paulson@13323 ` 854` ``` (\rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))" *) ``` paulson@13323 ` 855` ```constdefs field_fm :: "[i,i]=>i" ``` paulson@13323 ` 856` ``` "field_fm(r,z) == ``` paulson@13323 ` 857` ``` Exists(And(domain_fm(succ(r),0), ``` paulson@13323 ` 858` ``` Exists(And(range_fm(succ(succ(r)),0), ``` paulson@13323 ` 859` ``` union_fm(1,0,succ(succ(z)))))))" ``` paulson@13323 ` 860` paulson@13323 ` 861` ```lemma field_type [TC]: ``` paulson@13323 ` 862` ``` "[| x \ nat; y \ nat |] ==> field_fm(x,y) \ formula" ``` paulson@13323 ` 863` ```by (simp add: field_fm_def) ``` paulson@13323 ` 864` paulson@13323 ` 865` ```lemma arity_field_fm [simp]: ``` paulson@13323 ` 866` ``` "[| x \ nat; y \ nat |] ``` paulson@13323 ` 867` ``` ==> arity(field_fm(x,y)) = succ(x) \ succ(y)" ``` paulson@13323 ` 868` ```by (simp add: field_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13323 ` 869` paulson@13323 ` 870` ```lemma sats_field_fm [simp]: ``` paulson@13323 ` 871` ``` "[| x \ nat; y \ nat; env \ list(A)|] ``` paulson@13323 ` 872` ``` ==> sats(A, field_fm(x,y), env) <-> ``` paulson@13323 ` 873` ``` is_field(**A, nth(x,env), nth(y,env))" ``` paulson@13323 ` 874` ```by (simp add: field_fm_def is_field_def) ``` paulson@13323 ` 875` paulson@13323 ` 876` ```lemma field_iff_sats: ``` paulson@13323 ` 877` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13323 ` 878` ``` i \ nat; j \ nat; env \ list(A)|] ``` paulson@13323 ` 879` ``` ==> is_field(**A, x, y) <-> sats(A, field_fm(i,j), env)" ``` paulson@13323 ` 880` ```by simp ``` paulson@13323 ` 881` paulson@13323 ` 882` ```theorem field_reflection: ``` paulson@13323 ` 883` ``` "REFLECTS[\x. is_field(L,f(x),g(x)), ``` paulson@13323 ` 884` ``` \i x. is_field(**Lset(i),f(x),g(x))]" ``` paulson@13323 ` 885` ```apply (simp only: is_field_def setclass_simps) ``` paulson@13323 ` 886` ```apply (intro FOL_reflections domain_reflection range_reflection ``` paulson@13323 ` 887` ``` union_reflection) ``` paulson@13323 ` 888` ```done ``` paulson@13323 ` 889` paulson@13323 ` 890` paulson@13339 ` 891` ```subsubsection{*Image under a Relation, Internalized*} ``` paulson@13306 ` 892` paulson@13306 ` 893` ```(* "image(M,r,A,z) == ``` paulson@13306 ` 894` ``` \y[M]. (y \ z <-> (\w[M]. w\r & (\x[M]. x\A & pair(M,x,y,w))))" *) ``` paulson@13306 ` 895` ```constdefs image_fm :: "[i,i,i]=>i" ``` paulson@13306 ` 896` ``` "image_fm(r,A,z) == ``` paulson@13306 ` 897` ``` Forall(Iff(Member(0,succ(z)), ``` paulson@13306 ` 898` ``` Exists(And(Member(0,succ(succ(r))), ``` paulson@13306 ` 899` ``` Exists(And(Member(0,succ(succ(succ(A)))), ``` paulson@13306 ` 900` ``` pair_fm(0,2,1)))))))" ``` paulson@13306 ` 901` paulson@13306 ` 902` ```lemma image_type [TC]: ``` paulson@13306 ` 903` ``` "[| x \ nat; y \ nat; z \ nat |] ==> image_fm(x,y,z) \ formula" ``` paulson@13306 ` 904` ```by (simp add: image_fm_def) ``` paulson@13306 ` 905` paulson@13306 ` 906` ```lemma arity_image_fm [simp]: ``` paulson@13306 ` 907` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13306 ` 908` ``` ==> arity(image_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13306 ` 909` ```by (simp add: image_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 910` paulson@13306 ` 911` ```lemma sats_image_fm [simp]: ``` paulson@13306 ` 912` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13306 ` 913` ``` ==> sats(A, image_fm(x,y,z), env) <-> ``` paulson@13306 ` 914` ``` image(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13323 ` 915` ```by (simp add: image_fm_def Relative.image_def) ``` paulson@13306 ` 916` paulson@13306 ` 917` ```lemma image_iff_sats: ``` paulson@13306 ` 918` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13306 ` 919` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13306 ` 920` ``` ==> image(**A, x, y, z) <-> sats(A, image_fm(i,j,k), env)" ``` paulson@13306 ` 921` ```by (simp add: sats_image_fm) ``` paulson@13306 ` 922` paulson@13314 ` 923` ```theorem image_reflection: ``` paulson@13314 ` 924` ``` "REFLECTS[\x. image(L,f(x),g(x),h(x)), ``` paulson@13314 ` 925` ``` \i x. image(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13323 ` 926` ```apply (simp only: Relative.image_def setclass_simps) ``` paulson@13323 ` 927` ```apply (intro FOL_reflections pair_reflection) ``` paulson@13314 ` 928` ```done ``` paulson@13306 ` 929` paulson@13306 ` 930` paulson@13348 ` 931` ```subsubsection{*Pre-Image under a Relation, Internalized*} ``` paulson@13348 ` 932` paulson@13348 ` 933` ```(* "pre_image(M,r,A,z) == ``` paulson@13348 ` 934` ``` \x[M]. x \ z <-> (\w[M]. w\r & (\y[M]. y\A & pair(M,x,y,w)))" *) ``` paulson@13348 ` 935` ```constdefs pre_image_fm :: "[i,i,i]=>i" ``` paulson@13348 ` 936` ``` "pre_image_fm(r,A,z) == ``` paulson@13348 ` 937` ``` Forall(Iff(Member(0,succ(z)), ``` paulson@13348 ` 938` ``` Exists(And(Member(0,succ(succ(r))), ``` paulson@13348 ` 939` ``` Exists(And(Member(0,succ(succ(succ(A)))), ``` paulson@13348 ` 940` ``` pair_fm(2,0,1)))))))" ``` paulson@13348 ` 941` paulson@13348 ` 942` ```lemma pre_image_type [TC]: ``` paulson@13348 ` 943` ``` "[| x \ nat; y \ nat; z \ nat |] ==> pre_image_fm(x,y,z) \ formula" ``` paulson@13348 ` 944` ```by (simp add: pre_image_fm_def) ``` paulson@13348 ` 945` paulson@13348 ` 946` ```lemma arity_pre_image_fm [simp]: ``` paulson@13348 ` 947` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13348 ` 948` ``` ==> arity(pre_image_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13348 ` 949` ```by (simp add: pre_image_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13348 ` 950` paulson@13348 ` 951` ```lemma sats_pre_image_fm [simp]: ``` paulson@13348 ` 952` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13348 ` 953` ``` ==> sats(A, pre_image_fm(x,y,z), env) <-> ``` paulson@13348 ` 954` ``` pre_image(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13348 ` 955` ```by (simp add: pre_image_fm_def Relative.pre_image_def) ``` paulson@13348 ` 956` paulson@13348 ` 957` ```lemma pre_image_iff_sats: ``` paulson@13348 ` 958` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13348 ` 959` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13348 ` 960` ``` ==> pre_image(**A, x, y, z) <-> sats(A, pre_image_fm(i,j,k), env)" ``` paulson@13348 ` 961` ```by (simp add: sats_pre_image_fm) ``` paulson@13348 ` 962` paulson@13348 ` 963` ```theorem pre_image_reflection: ``` paulson@13348 ` 964` ``` "REFLECTS[\x. pre_image(L,f(x),g(x),h(x)), ``` paulson@13348 ` 965` ``` \i x. pre_image(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13348 ` 966` ```apply (simp only: Relative.pre_image_def setclass_simps) ``` paulson@13348 ` 967` ```apply (intro FOL_reflections pair_reflection) ``` paulson@13348 ` 968` ```done ``` paulson@13348 ` 969` paulson@13348 ` 970` paulson@13352 ` 971` ```subsubsection{*Function Application, Internalized*} ``` paulson@13352 ` 972` paulson@13352 ` 973` ```(* "fun_apply(M,f,x,y) == ``` paulson@13352 ` 974` ``` (\xs[M]. \fxs[M]. ``` paulson@13352 ` 975` ``` upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" *) ``` paulson@13352 ` 976` ```constdefs fun_apply_fm :: "[i,i,i]=>i" ``` paulson@13352 ` 977` ``` "fun_apply_fm(f,x,y) == ``` paulson@13352 ` 978` ``` Exists(Exists(And(upair_fm(succ(succ(x)), succ(succ(x)), 1), ``` paulson@13352 ` 979` ``` And(image_fm(succ(succ(f)), 1, 0), ``` paulson@13352 ` 980` ``` big_union_fm(0,succ(succ(y)))))))" ``` paulson@13352 ` 981` paulson@13352 ` 982` ```lemma fun_apply_type [TC]: ``` paulson@13352 ` 983` ``` "[| x \ nat; y \ nat; z \ nat |] ==> fun_apply_fm(x,y,z) \ formula" ``` paulson@13352 ` 984` ```by (simp add: fun_apply_fm_def) ``` paulson@13352 ` 985` paulson@13352 ` 986` ```lemma arity_fun_apply_fm [simp]: ``` paulson@13352 ` 987` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13352 ` 988` ``` ==> arity(fun_apply_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13352 ` 989` ```by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13352 ` 990` paulson@13352 ` 991` ```lemma sats_fun_apply_fm [simp]: ``` paulson@13352 ` 992` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13352 ` 993` ``` ==> sats(A, fun_apply_fm(x,y,z), env) <-> ``` paulson@13352 ` 994` ``` fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13352 ` 995` ```by (simp add: fun_apply_fm_def fun_apply_def) ``` paulson@13352 ` 996` paulson@13352 ` 997` ```lemma fun_apply_iff_sats: ``` paulson@13352 ` 998` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13352 ` 999` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13352 ` 1000` ``` ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)" ``` paulson@13352 ` 1001` ```by simp ``` paulson@13352 ` 1002` paulson@13352 ` 1003` ```theorem fun_apply_reflection: ``` paulson@13352 ` 1004` ``` "REFLECTS[\x. fun_apply(L,f(x),g(x),h(x)), ``` paulson@13352 ` 1005` ``` \i x. fun_apply(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13352 ` 1006` ```apply (simp only: fun_apply_def setclass_simps) ``` paulson@13352 ` 1007` ```apply (intro FOL_reflections upair_reflection image_reflection ``` paulson@13352 ` 1008` ``` big_union_reflection) ``` paulson@13352 ` 1009` ```done ``` paulson@13352 ` 1010` paulson@13352 ` 1011` paulson@13339 ` 1012` ```subsubsection{*The Concept of Relation, Internalized*} ``` paulson@13306 ` 1013` paulson@13306 ` 1014` ```(* "is_relation(M,r) == ``` paulson@13306 ` 1015` ``` (\z[M]. z\r --> (\x[M]. \y[M]. pair(M,x,y,z)))" *) ``` paulson@13306 ` 1016` ```constdefs relation_fm :: "i=>i" ``` paulson@13306 ` 1017` ``` "relation_fm(r) == ``` paulson@13306 ` 1018` ``` Forall(Implies(Member(0,succ(r)), Exists(Exists(pair_fm(1,0,2)))))" ``` paulson@13306 ` 1019` paulson@13306 ` 1020` ```lemma relation_type [TC]: ``` paulson@13306 ` 1021` ``` "[| x \ nat |] ==> relation_fm(x) \ formula" ``` paulson@13306 ` 1022` ```by (simp add: relation_fm_def) ``` paulson@13306 ` 1023` paulson@13306 ` 1024` ```lemma arity_relation_fm [simp]: ``` paulson@13306 ` 1025` ``` "x \ nat ==> arity(relation_fm(x)) = succ(x)" ``` paulson@13306 ` 1026` ```by (simp add: relation_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 1027` paulson@13306 ` 1028` ```lemma sats_relation_fm [simp]: ``` paulson@13306 ` 1029` ``` "[| x \ nat; env \ list(A)|] ``` paulson@13306 ` 1030` ``` ==> sats(A, relation_fm(x), env) <-> is_relation(**A, nth(x,env))" ``` paulson@13306 ` 1031` ```by (simp add: relation_fm_def is_relation_def) ``` paulson@13306 ` 1032` paulson@13306 ` 1033` ```lemma relation_iff_sats: ``` paulson@13306 ` 1034` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13306 ` 1035` ``` i \ nat; env \ list(A)|] ``` paulson@13306 ` 1036` ``` ==> is_relation(**A, x) <-> sats(A, relation_fm(i), env)" ``` paulson@13306 ` 1037` ```by simp ``` paulson@13306 ` 1038` paulson@13314 ` 1039` ```theorem is_relation_reflection: ``` paulson@13314 ` 1040` ``` "REFLECTS[\x. is_relation(L,f(x)), ``` paulson@13314 ` 1041` ``` \i x. is_relation(**Lset(i),f(x))]" ``` paulson@13314 ` 1042` ```apply (simp only: is_relation_def setclass_simps) ``` paulson@13323 ` 1043` ```apply (intro FOL_reflections pair_reflection) ``` paulson@13314 ` 1044` ```done ``` paulson@13306 ` 1045` paulson@13306 ` 1046` paulson@13339 ` 1047` ```subsubsection{*The Concept of Function, Internalized*} ``` paulson@13306 ` 1048` paulson@13306 ` 1049` ```(* "is_function(M,r) == ``` paulson@13306 ` 1050` ``` \x[M]. \y[M]. \y'[M]. \p[M]. \p'[M]. ``` paulson@13306 ` 1051` ``` pair(M,x,y,p) --> pair(M,x,y',p') --> p\r --> p'\r --> y=y'" *) ``` paulson@13306 ` 1052` ```constdefs function_fm :: "i=>i" ``` paulson@13306 ` 1053` ``` "function_fm(r) == ``` paulson@13306 ` 1054` ``` Forall(Forall(Forall(Forall(Forall( ``` paulson@13306 ` 1055` ``` Implies(pair_fm(4,3,1), ``` paulson@13306 ` 1056` ``` Implies(pair_fm(4,2,0), ``` paulson@13306 ` 1057` ``` Implies(Member(1,r#+5), ``` paulson@13306 ` 1058` ``` Implies(Member(0,r#+5), Equal(3,2))))))))))" ``` paulson@13306 ` 1059` paulson@13306 ` 1060` ```lemma function_type [TC]: ``` paulson@13306 ` 1061` ``` "[| x \ nat |] ==> function_fm(x) \ formula" ``` paulson@13306 ` 1062` ```by (simp add: function_fm_def) ``` paulson@13306 ` 1063` paulson@13306 ` 1064` ```lemma arity_function_fm [simp]: ``` paulson@13306 ` 1065` ``` "x \ nat ==> arity(function_fm(x)) = succ(x)" ``` paulson@13306 ` 1066` ```by (simp add: function_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 1067` paulson@13306 ` 1068` ```lemma sats_function_fm [simp]: ``` paulson@13306 ` 1069` ``` "[| x \ nat; env \ list(A)|] ``` paulson@13306 ` 1070` ``` ==> sats(A, function_fm(x), env) <-> is_function(**A, nth(x,env))" ``` paulson@13306 ` 1071` ```by (simp add: function_fm_def is_function_def) ``` paulson@13306 ` 1072` paulson@13306 ` 1073` ```lemma function_iff_sats: ``` paulson@13306 ` 1074` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13306 ` 1075` ``` i \ nat; env \ list(A)|] ``` paulson@13306 ` 1076` ``` ==> is_function(**A, x) <-> sats(A, function_fm(i), env)" ``` paulson@13306 ` 1077` ```by simp ``` paulson@13306 ` 1078` paulson@13314 ` 1079` ```theorem is_function_reflection: ``` paulson@13314 ` 1080` ``` "REFLECTS[\x. is_function(L,f(x)), ``` paulson@13314 ` 1081` ``` \i x. is_function(**Lset(i),f(x))]" ``` paulson@13314 ` 1082` ```apply (simp only: is_function_def setclass_simps) ``` paulson@13323 ` 1083` ```apply (intro FOL_reflections pair_reflection) ``` paulson@13314 ` 1084` ```done ``` paulson@13298 ` 1085` paulson@13298 ` 1086` paulson@13339 ` 1087` ```subsubsection{*Typed Functions, Internalized*} ``` paulson@13309 ` 1088` paulson@13309 ` 1089` ```(* "typed_function(M,A,B,r) == ``` paulson@13309 ` 1090` ``` is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) & ``` paulson@13309 ` 1091` ``` (\u[M]. u\r --> (\x[M]. \y[M]. pair(M,x,y,u) --> y\B))" *) ``` paulson@13309 ` 1092` paulson@13309 ` 1093` ```constdefs typed_function_fm :: "[i,i,i]=>i" ``` paulson@13309 ` 1094` ``` "typed_function_fm(A,B,r) == ``` paulson@13309 ` 1095` ``` And(function_fm(r), ``` paulson@13309 ` 1096` ``` And(relation_fm(r), ``` paulson@13309 ` 1097` ``` And(domain_fm(r,A), ``` paulson@13309 ` 1098` ``` Forall(Implies(Member(0,succ(r)), ``` paulson@13309 ` 1099` ``` Forall(Forall(Implies(pair_fm(1,0,2),Member(0,B#+3)))))))))" ``` paulson@13309 ` 1100` paulson@13309 ` 1101` ```lemma typed_function_type [TC]: ``` paulson@13309 ` 1102` ``` "[| x \ nat; y \ nat; z \ nat |] ==> typed_function_fm(x,y,z) \ formula" ``` paulson@13309 ` 1103` ```by (simp add: typed_function_fm_def) ``` paulson@13309 ` 1104` paulson@13309 ` 1105` ```lemma arity_typed_function_fm [simp]: ``` paulson@13309 ` 1106` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13309 ` 1107` ``` ==> arity(typed_function_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13309 ` 1108` ```by (simp add: typed_function_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13309 ` 1109` paulson@13309 ` 1110` ```lemma sats_typed_function_fm [simp]: ``` paulson@13309 ` 1111` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13309 ` 1112` ``` ==> sats(A, typed_function_fm(x,y,z), env) <-> ``` paulson@13309 ` 1113` ``` typed_function(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13309 ` 1114` ```by (simp add: typed_function_fm_def typed_function_def) ``` paulson@13309 ` 1115` paulson@13309 ` 1116` ```lemma typed_function_iff_sats: ``` paulson@13309 ` 1117` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13309 ` 1118` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13309 ` 1119` ``` ==> typed_function(**A, x, y, z) <-> sats(A, typed_function_fm(i,j,k), env)" ``` paulson@13309 ` 1120` ```by simp ``` paulson@13309 ` 1121` paulson@13323 ` 1122` ```lemmas function_reflections = ``` paulson@13363 ` 1123` ``` empty_reflection number1_reflection ``` paulson@13363 ` 1124` ``` upair_reflection pair_reflection union_reflection ``` paulson@13352 ` 1125` ``` big_union_reflection cons_reflection successor_reflection ``` paulson@13323 ` 1126` ``` fun_apply_reflection subset_reflection ``` paulson@13323 ` 1127` ``` transitive_set_reflection membership_reflection ``` paulson@13323 ` 1128` ``` pred_set_reflection domain_reflection range_reflection field_reflection ``` paulson@13348 ` 1129` ``` image_reflection pre_image_reflection ``` paulson@13314 ` 1130` ``` is_relation_reflection is_function_reflection ``` paulson@13309 ` 1131` paulson@13323 ` 1132` ```lemmas function_iff_sats = ``` paulson@13363 ` 1133` ``` empty_iff_sats number1_iff_sats ``` paulson@13363 ` 1134` ``` upair_iff_sats pair_iff_sats union_iff_sats ``` paulson@13323 ` 1135` ``` cons_iff_sats successor_iff_sats ``` paulson@13323 ` 1136` ``` fun_apply_iff_sats Memrel_iff_sats ``` paulson@13323 ` 1137` ``` pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats ``` paulson@13348 ` 1138` ``` image_iff_sats pre_image_iff_sats ``` paulson@13323 ` 1139` ``` relation_iff_sats function_iff_sats ``` paulson@13323 ` 1140` paulson@13309 ` 1141` paulson@13314 ` 1142` ```theorem typed_function_reflection: ``` paulson@13314 ` 1143` ``` "REFLECTS[\x. typed_function(L,f(x),g(x),h(x)), ``` paulson@13314 ` 1144` ``` \i x. typed_function(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 1145` ```apply (simp only: typed_function_def setclass_simps) ``` paulson@13323 ` 1146` ```apply (intro FOL_reflections function_reflections) ``` paulson@13323 ` 1147` ```done ``` paulson@13323 ` 1148` paulson@13323 ` 1149` paulson@13339 ` 1150` ```subsubsection{*Composition of Relations, Internalized*} ``` paulson@13323 ` 1151` paulson@13323 ` 1152` ```(* "composition(M,r,s,t) == ``` paulson@13323 ` 1153` ``` \p[M]. p \ t <-> ``` paulson@13323 ` 1154` ``` (\x[M]. \y[M]. \z[M]. \xy[M]. \yz[M]. ``` paulson@13323 ` 1155` ``` pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & ``` paulson@13323 ` 1156` ``` xy \ s & yz \ r)" *) ``` paulson@13323 ` 1157` ```constdefs composition_fm :: "[i,i,i]=>i" ``` paulson@13323 ` 1158` ``` "composition_fm(r,s,t) == ``` paulson@13323 ` 1159` ``` Forall(Iff(Member(0,succ(t)), ``` paulson@13323 ` 1160` ``` Exists(Exists(Exists(Exists(Exists( ``` paulson@13323 ` 1161` ``` And(pair_fm(4,2,5), ``` paulson@13323 ` 1162` ``` And(pair_fm(4,3,1), ``` paulson@13323 ` 1163` ``` And(pair_fm(3,2,0), ``` paulson@13323 ` 1164` ``` And(Member(1,s#+6), Member(0,r#+6))))))))))))" ``` paulson@13323 ` 1165` paulson@13323 ` 1166` ```lemma composition_type [TC]: ``` paulson@13323 ` 1167` ``` "[| x \ nat; y \ nat; z \ nat |] ==> composition_fm(x,y,z) \ formula" ``` paulson@13323 ` 1168` ```by (simp add: composition_fm_def) ``` paulson@13323 ` 1169` paulson@13323 ` 1170` ```lemma arity_composition_fm [simp]: ``` paulson@13323 ` 1171` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13323 ` 1172` ``` ==> arity(composition_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13323 ` 1173` ```by (simp add: composition_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13323 ` 1174` paulson@13323 ` 1175` ```lemma sats_composition_fm [simp]: ``` paulson@13323 ` 1176` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13323 ` 1177` ``` ==> sats(A, composition_fm(x,y,z), env) <-> ``` paulson@13323 ` 1178` ``` composition(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13323 ` 1179` ```by (simp add: composition_fm_def composition_def) ``` paulson@13323 ` 1180` paulson@13323 ` 1181` ```lemma composition_iff_sats: ``` paulson@13323 ` 1182` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13323 ` 1183` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13323 ` 1184` ``` ==> composition(**A, x, y, z) <-> sats(A, composition_fm(i,j,k), env)" ``` paulson@13323 ` 1185` ```by simp ``` paulson@13323 ` 1186` paulson@13323 ` 1187` ```theorem composition_reflection: ``` paulson@13323 ` 1188` ``` "REFLECTS[\x. composition(L,f(x),g(x),h(x)), ``` paulson@13323 ` 1189` ``` \i x. composition(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13323 ` 1190` ```apply (simp only: composition_def setclass_simps) ``` paulson@13323 ` 1191` ```apply (intro FOL_reflections pair_reflection) ``` paulson@13314 ` 1192` ```done ``` paulson@13314 ` 1193` paulson@13309 ` 1194` paulson@13339 ` 1195` ```subsubsection{*Injections, Internalized*} ``` paulson@13309 ` 1196` paulson@13309 ` 1197` ```(* "injection(M,A,B,f) == ``` paulson@13309 ` 1198` ``` typed_function(M,A,B,f) & ``` paulson@13309 ` 1199` ``` (\x[M]. \x'[M]. \y[M]. \p[M]. \p'[M]. ``` paulson@13309 ` 1200` ``` pair(M,x,y,p) --> pair(M,x',y,p') --> p\f --> p'\f --> x=x')" *) ``` paulson@13309 ` 1201` ```constdefs injection_fm :: "[i,i,i]=>i" ``` paulson@13309 ` 1202` ``` "injection_fm(A,B,f) == ``` paulson@13309 ` 1203` ``` And(typed_function_fm(A,B,f), ``` paulson@13309 ` 1204` ``` Forall(Forall(Forall(Forall(Forall( ``` paulson@13309 ` 1205` ``` Implies(pair_fm(4,2,1), ``` paulson@13309 ` 1206` ``` Implies(pair_fm(3,2,0), ``` paulson@13309 ` 1207` ``` Implies(Member(1,f#+5), ``` paulson@13309 ` 1208` ``` Implies(Member(0,f#+5), Equal(4,3)))))))))))" ``` paulson@13309 ` 1209` paulson@13309 ` 1210` paulson@13309 ` 1211` ```lemma injection_type [TC]: ``` paulson@13309 ` 1212` ``` "[| x \ nat; y \ nat; z \ nat |] ==> injection_fm(x,y,z) \ formula" ``` paulson@13309 ` 1213` ```by (simp add: injection_fm_def) ``` paulson@13309 ` 1214` paulson@13309 ` 1215` ```lemma arity_injection_fm [simp]: ``` paulson@13309 ` 1216` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13309 ` 1217` ``` ==> arity(injection_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13309 ` 1218` ```by (simp add: injection_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13309 ` 1219` paulson@13309 ` 1220` ```lemma sats_injection_fm [simp]: ``` paulson@13309 ` 1221` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13309 ` 1222` ``` ==> sats(A, injection_fm(x,y,z), env) <-> ``` paulson@13309 ` 1223` ``` injection(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13309 ` 1224` ```by (simp add: injection_fm_def injection_def) ``` paulson@13309 ` 1225` paulson@13309 ` 1226` ```lemma injection_iff_sats: ``` paulson@13309 ` 1227` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13309 ` 1228` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13309 ` 1229` ``` ==> injection(**A, x, y, z) <-> sats(A, injection_fm(i,j,k), env)" ``` paulson@13309 ` 1230` ```by simp ``` paulson@13309 ` 1231` paulson@13314 ` 1232` ```theorem injection_reflection: ``` paulson@13314 ` 1233` ``` "REFLECTS[\x. injection(L,f(x),g(x),h(x)), ``` paulson@13314 ` 1234` ``` \i x. injection(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 1235` ```apply (simp only: injection_def setclass_simps) ``` paulson@13323 ` 1236` ```apply (intro FOL_reflections function_reflections typed_function_reflection) ``` paulson@13314 ` 1237` ```done ``` paulson@13309 ` 1238` paulson@13309 ` 1239` paulson@13339 ` 1240` ```subsubsection{*Surjections, Internalized*} ``` paulson@13309 ` 1241` paulson@13309 ` 1242` ```(* surjection :: "[i=>o,i,i,i] => o" ``` paulson@13309 ` 1243` ``` "surjection(M,A,B,f) == ``` paulson@13309 ` 1244` ``` typed_function(M,A,B,f) & ``` paulson@13309 ` 1245` ``` (\y[M]. y\B --> (\x[M]. x\A & fun_apply(M,f,x,y)))" *) ``` paulson@13309 ` 1246` ```constdefs surjection_fm :: "[i,i,i]=>i" ``` paulson@13309 ` 1247` ``` "surjection_fm(A,B,f) == ``` paulson@13309 ` 1248` ``` And(typed_function_fm(A,B,f), ``` paulson@13309 ` 1249` ``` Forall(Implies(Member(0,succ(B)), ``` paulson@13309 ` 1250` ``` Exists(And(Member(0,succ(succ(A))), ``` paulson@13309 ` 1251` ``` fun_apply_fm(succ(succ(f)),0,1))))))" ``` paulson@13309 ` 1252` paulson@13309 ` 1253` ```lemma surjection_type [TC]: ``` paulson@13309 ` 1254` ``` "[| x \ nat; y \ nat; z \ nat |] ==> surjection_fm(x,y,z) \ formula" ``` paulson@13309 ` 1255` ```by (simp add: surjection_fm_def) ``` paulson@13309 ` 1256` paulson@13309 ` 1257` ```lemma arity_surjection_fm [simp]: ``` paulson@13309 ` 1258` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13309 ` 1259` ``` ==> arity(surjection_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13309 ` 1260` ```by (simp add: surjection_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13309 ` 1261` paulson@13309 ` 1262` ```lemma sats_surjection_fm [simp]: ``` paulson@13309 ` 1263` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13309 ` 1264` ``` ==> sats(A, surjection_fm(x,y,z), env) <-> ``` paulson@13309 ` 1265` ``` surjection(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13309 ` 1266` ```by (simp add: surjection_fm_def surjection_def) ``` paulson@13309 ` 1267` paulson@13309 ` 1268` ```lemma surjection_iff_sats: ``` paulson@13309 ` 1269` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13309 ` 1270` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13309 ` 1271` ``` ==> surjection(**A, x, y, z) <-> sats(A, surjection_fm(i,j,k), env)" ``` paulson@13309 ` 1272` ```by simp ``` paulson@13309 ` 1273` paulson@13314 ` 1274` ```theorem surjection_reflection: ``` paulson@13314 ` 1275` ``` "REFLECTS[\x. surjection(L,f(x),g(x),h(x)), ``` paulson@13314 ` 1276` ``` \i x. surjection(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 1277` ```apply (simp only: surjection_def setclass_simps) ``` paulson@13323 ` 1278` ```apply (intro FOL_reflections function_reflections typed_function_reflection) ``` paulson@13314 ` 1279` ```done ``` paulson@13309 ` 1280` paulson@13309 ` 1281` paulson@13309 ` 1282` paulson@13339 ` 1283` ```subsubsection{*Bijections, Internalized*} ``` paulson@13309 ` 1284` paulson@13309 ` 1285` ```(* bijection :: "[i=>o,i,i,i] => o" ``` paulson@13309 ` 1286` ``` "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" *) ``` paulson@13309 ` 1287` ```constdefs bijection_fm :: "[i,i,i]=>i" ``` paulson@13309 ` 1288` ``` "bijection_fm(A,B,f) == And(injection_fm(A,B,f), surjection_fm(A,B,f))" ``` paulson@13309 ` 1289` paulson@13309 ` 1290` ```lemma bijection_type [TC]: ``` paulson@13309 ` 1291` ``` "[| x \ nat; y \ nat; z \ nat |] ==> bijection_fm(x,y,z) \ formula" ``` paulson@13309 ` 1292` ```by (simp add: bijection_fm_def) ``` paulson@13309 ` 1293` paulson@13309 ` 1294` ```lemma arity_bijection_fm [simp]: ``` paulson@13309 ` 1295` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13309 ` 1296` ``` ==> arity(bijection_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13309 ` 1297` ```by (simp add: bijection_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13309 ` 1298` paulson@13309 ` 1299` ```lemma sats_bijection_fm [simp]: ``` paulson@13309 ` 1300` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13309 ` 1301` ``` ==> sats(A, bijection_fm(x,y,z), env) <-> ``` paulson@13309 ` 1302` ``` bijection(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13309 ` 1303` ```by (simp add: bijection_fm_def bijection_def) ``` paulson@13309 ` 1304` paulson@13309 ` 1305` ```lemma bijection_iff_sats: ``` paulson@13309 ` 1306` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13309 ` 1307` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13309 ` 1308` ``` ==> bijection(**A, x, y, z) <-> sats(A, bijection_fm(i,j,k), env)" ``` paulson@13309 ` 1309` ```by simp ``` paulson@13309 ` 1310` paulson@13314 ` 1311` ```theorem bijection_reflection: ``` paulson@13314 ` 1312` ``` "REFLECTS[\x. bijection(L,f(x),g(x),h(x)), ``` paulson@13314 ` 1313` ``` \i x. bijection(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 1314` ```apply (simp only: bijection_def setclass_simps) ``` paulson@13314 ` 1315` ```apply (intro And_reflection injection_reflection surjection_reflection) ``` paulson@13314 ` 1316` ```done ``` paulson@13309 ` 1317` paulson@13309 ` 1318` paulson@13348 ` 1319` ```subsubsection{*Restriction of a Relation, Internalized*} ``` paulson@13348 ` 1320` paulson@13348 ` 1321` paulson@13348 ` 1322` ```(* "restriction(M,r,A,z) == ``` paulson@13348 ` 1323` ``` \x[M]. x \ z <-> (x \ r & (\u[M]. u\A & (\v[M]. pair(M,u,v,x))))" *) ``` paulson@13348 ` 1324` ```constdefs restriction_fm :: "[i,i,i]=>i" ``` paulson@13348 ` 1325` ``` "restriction_fm(r,A,z) == ``` paulson@13348 ` 1326` ``` Forall(Iff(Member(0,succ(z)), ``` paulson@13348 ` 1327` ``` And(Member(0,succ(r)), ``` paulson@13348 ` 1328` ``` Exists(And(Member(0,succ(succ(A))), ``` paulson@13348 ` 1329` ``` Exists(pair_fm(1,0,2)))))))" ``` paulson@13348 ` 1330` paulson@13348 ` 1331` ```lemma restriction_type [TC]: ``` paulson@13348 ` 1332` ``` "[| x \ nat; y \ nat; z \ nat |] ==> restriction_fm(x,y,z) \ formula" ``` paulson@13348 ` 1333` ```by (simp add: restriction_fm_def) ``` paulson@13348 ` 1334` paulson@13348 ` 1335` ```lemma arity_restriction_fm [simp]: ``` paulson@13348 ` 1336` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13348 ` 1337` ``` ==> arity(restriction_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13348 ` 1338` ```by (simp add: restriction_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13348 ` 1339` paulson@13348 ` 1340` ```lemma sats_restriction_fm [simp]: ``` paulson@13348 ` 1341` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13348 ` 1342` ``` ==> sats(A, restriction_fm(x,y,z), env) <-> ``` paulson@13348 ` 1343` ``` restriction(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13348 ` 1344` ```by (simp add: restriction_fm_def restriction_def) ``` paulson@13348 ` 1345` paulson@13348 ` 1346` ```lemma restriction_iff_sats: ``` paulson@13348 ` 1347` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13348 ` 1348` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13348 ` 1349` ``` ==> restriction(**A, x, y, z) <-> sats(A, restriction_fm(i,j,k), env)" ``` paulson@13348 ` 1350` ```by simp ``` paulson@13348 ` 1351` paulson@13348 ` 1352` ```theorem restriction_reflection: ``` paulson@13348 ` 1353` ``` "REFLECTS[\x. restriction(L,f(x),g(x),h(x)), ``` paulson@13348 ` 1354` ``` \i x. restriction(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13348 ` 1355` ```apply (simp only: restriction_def setclass_simps) ``` paulson@13348 ` 1356` ```apply (intro FOL_reflections pair_reflection) ``` paulson@13348 ` 1357` ```done ``` paulson@13348 ` 1358` paulson@13339 ` 1359` ```subsubsection{*Order-Isomorphisms, Internalized*} ``` paulson@13309 ` 1360` paulson@13309 ` 1361` ```(* order_isomorphism :: "[i=>o,i,i,i,i,i] => o" ``` paulson@13309 ` 1362` ``` "order_isomorphism(M,A,r,B,s,f) == ``` paulson@13309 ` 1363` ``` bijection(M,A,B,f) & ``` paulson@13309 ` 1364` ``` (\x[M]. x\A --> (\y[M]. y\A --> ``` paulson@13309 ` 1365` ``` (\p[M]. \fx[M]. \fy[M]. \q[M]. ``` paulson@13309 ` 1366` ``` pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) --> ``` paulson@13309 ` 1367` ``` pair(M,fx,fy,q) --> (p\r <-> q\s))))" ``` paulson@13309 ` 1368` ``` *) ``` paulson@13309 ` 1369` paulson@13309 ` 1370` ```constdefs order_isomorphism_fm :: "[i,i,i,i,i]=>i" ``` paulson@13309 ` 1371` ``` "order_isomorphism_fm(A,r,B,s,f) == ``` paulson@13309 ` 1372` ``` And(bijection_fm(A,B,f), ``` paulson@13309 ` 1373` ``` Forall(Implies(Member(0,succ(A)), ``` paulson@13309 ` 1374` ``` Forall(Implies(Member(0,succ(succ(A))), ``` paulson@13309 ` 1375` ``` Forall(Forall(Forall(Forall( ``` paulson@13309 ` 1376` ``` Implies(pair_fm(5,4,3), ``` paulson@13309 ` 1377` ``` Implies(fun_apply_fm(f#+6,5,2), ``` paulson@13309 ` 1378` ``` Implies(fun_apply_fm(f#+6,4,1), ``` paulson@13309 ` 1379` ``` Implies(pair_fm(2,1,0), ``` paulson@13309 ` 1380` ``` Iff(Member(3,r#+6), Member(0,s#+6)))))))))))))))" ``` paulson@13309 ` 1381` paulson@13309 ` 1382` ```lemma order_isomorphism_type [TC]: ``` paulson@13309 ` 1383` ``` "[| A \ nat; r \ nat; B \ nat; s \ nat; f \ nat |] ``` paulson@13309 ` 1384` ``` ==> order_isomorphism_fm(A,r,B,s,f) \ formula" ``` paulson@13309 ` 1385` ```by (simp add: order_isomorphism_fm_def) ``` paulson@13309 ` 1386` paulson@13309 ` 1387` ```lemma arity_order_isomorphism_fm [simp]: ``` paulson@13309 ` 1388` ``` "[| A \ nat; r \ nat; B \ nat; s \ nat; f \ nat |] ``` paulson@13309 ` 1389` ``` ==> arity(order_isomorphism_fm(A,r,B,s,f)) = ``` paulson@13309 ` 1390` ``` succ(A) \ succ(r) \ succ(B) \ succ(s) \ succ(f)" ``` paulson@13309 ` 1391` ```by (simp add: order_isomorphism_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13309 ` 1392` paulson@13309 ` 1393` ```lemma sats_order_isomorphism_fm [simp]: ``` paulson@13309 ` 1394` ``` "[| U \ nat; r \ nat; B \ nat; s \ nat; f \ nat; env \ list(A)|] ``` paulson@13309 ` 1395` ``` ==> sats(A, order_isomorphism_fm(U,r,B,s,f), env) <-> ``` paulson@13309 ` 1396` ``` order_isomorphism(**A, nth(U,env), nth(r,env), nth(B,env), ``` paulson@13309 ` 1397` ``` nth(s,env), nth(f,env))" ``` paulson@13309 ` 1398` ```by (simp add: order_isomorphism_fm_def order_isomorphism_def) ``` paulson@13309 ` 1399` paulson@13309 ` 1400` ```lemma order_isomorphism_iff_sats: ``` paulson@13309 ` 1401` ``` "[| nth(i,env) = U; nth(j,env) = r; nth(k,env) = B; nth(j',env) = s; ``` paulson@13309 ` 1402` ``` nth(k',env) = f; ``` paulson@13309 ` 1403` ``` i \ nat; j \ nat; k \ nat; j' \ nat; k' \ nat; env \ list(A)|] ``` paulson@13309 ` 1404` ``` ==> order_isomorphism(**A,U,r,B,s,f) <-> ``` paulson@13309 ` 1405` ``` sats(A, order_isomorphism_fm(i,j,k,j',k'), env)" ``` paulson@13309 ` 1406` ```by simp ``` paulson@13309 ` 1407` paulson@13314 ` 1408` ```theorem order_isomorphism_reflection: ``` paulson@13314 ` 1409` ``` "REFLECTS[\x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)), ``` paulson@13314 ` 1410` ``` \i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]" ``` paulson@13314 ` 1411` ```apply (simp only: order_isomorphism_def setclass_simps) ``` paulson@13323 ` 1412` ```apply (intro FOL_reflections function_reflections bijection_reflection) ``` paulson@13323 ` 1413` ```done ``` paulson@13323 ` 1414` paulson@13339 ` 1415` ```subsubsection{*Limit Ordinals, Internalized*} ``` paulson@13323 ` 1416` paulson@13323 ` 1417` ```text{*A limit ordinal is a non-empty, successor-closed ordinal*} ``` paulson@13323 ` 1418` paulson@13323 ` 1419` ```(* "limit_ordinal(M,a) == ``` paulson@13323 ` 1420` ``` ordinal(M,a) & ~ empty(M,a) & ``` paulson@13323 ` 1421` ``` (\x[M]. x\a --> (\y[M]. y\a & successor(M,x,y)))" *) ``` paulson@13323 ` 1422` paulson@13323 ` 1423` ```constdefs limit_ordinal_fm :: "i=>i" ``` paulson@13323 ` 1424` ``` "limit_ordinal_fm(x) == ``` paulson@13323 ` 1425` ``` And(ordinal_fm(x), ``` paulson@13323 ` 1426` ``` And(Neg(empty_fm(x)), ``` paulson@13323 ` 1427` ``` Forall(Implies(Member(0,succ(x)), ``` paulson@13323 ` 1428` ``` Exists(And(Member(0,succ(succ(x))), ``` paulson@13323 ` 1429` ``` succ_fm(1,0)))))))" ``` paulson@13323 ` 1430` paulson@13323 ` 1431` ```lemma limit_ordinal_type [TC]: ``` paulson@13323 ` 1432` ``` "x \ nat ==> limit_ordinal_fm(x) \ formula" ``` paulson@13323 ` 1433` ```by (simp add: limit_ordinal_fm_def) ``` paulson@13323 ` 1434` paulson@13323 ` 1435` ```lemma arity_limit_ordinal_fm [simp]: ``` paulson@13323 ` 1436` ``` "x \ nat ==> arity(limit_ordinal_fm(x)) = succ(x)" ``` paulson@13323 ` 1437` ```by (simp add: limit_ordinal_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13323 ` 1438` paulson@13323 ` 1439` ```lemma sats_limit_ordinal_fm [simp]: ``` paulson@13323 ` 1440` ``` "[| x \ nat; env \ list(A)|] ``` paulson@13323 ` 1441` ``` ==> sats(A, limit_ordinal_fm(x), env) <-> limit_ordinal(**A, nth(x,env))" ``` paulson@13323 ` 1442` ```by (simp add: limit_ordinal_fm_def limit_ordinal_def sats_ordinal_fm') ``` paulson@13323 ` 1443` paulson@13323 ` 1444` ```lemma limit_ordinal_iff_sats: ``` paulson@13323 ` 1445` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13323 ` 1446` ``` i \ nat; env \ list(A)|] ``` paulson@13323 ` 1447` ``` ==> limit_ordinal(**A, x) <-> sats(A, limit_ordinal_fm(i), env)" ``` paulson@13323 ` 1448` ```by simp ``` paulson@13323 ` 1449` paulson@13323 ` 1450` ```theorem limit_ordinal_reflection: ``` paulson@13323 ` 1451` ``` "REFLECTS[\x. limit_ordinal(L,f(x)), ``` paulson@13323 ` 1452` ``` \i x. limit_ordinal(**Lset(i),f(x))]" ``` paulson@13323 ` 1453` ```apply (simp only: limit_ordinal_def setclass_simps) ``` paulson@13323 ` 1454` ```apply (intro FOL_reflections ordinal_reflection ``` paulson@13323 ` 1455` ``` empty_reflection successor_reflection) ``` paulson@13314 ` 1456` ```done ``` paulson@13309 ` 1457` paulson@13323 ` 1458` ```subsubsection{*Omega: The Set of Natural Numbers*} ``` paulson@13323 ` 1459` paulson@13323 ` 1460` ```(* omega(M,a) == limit_ordinal(M,a) & (\x[M]. x\a --> ~ limit_ordinal(M,x)) *) ``` paulson@13323 ` 1461` ```constdefs omega_fm :: "i=>i" ``` paulson@13323 ` 1462` ``` "omega_fm(x) == ``` paulson@13323 ` 1463` ``` And(limit_ordinal_fm(x), ``` paulson@13323 ` 1464` ``` Forall(Implies(Member(0,succ(x)), ``` paulson@13323 ` 1465` ``` Neg(limit_ordinal_fm(0)))))" ``` paulson@13323 ` 1466` paulson@13323 ` 1467` ```lemma omega_type [TC]: ``` paulson@13323 ` 1468` ``` "x \ nat ==> omega_fm(x) \ formula" ``` paulson@13323 ` 1469` ```by (simp add: omega_fm_def) ``` paulson@13323 ` 1470` paulson@13323 ` 1471` ```lemma arity_omega_fm [simp]: ``` paulson@13323 ` 1472` ``` "x \ nat ==> arity(omega_fm(x)) = succ(x)" ``` paulson@13323 ` 1473` ```by (simp add: omega_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13323 ` 1474` paulson@13323 ` 1475` ```lemma sats_omega_fm [simp]: ``` paulson@13323 ` 1476` ``` "[| x \ nat; env \ list(A)|] ``` paulson@13323 ` 1477` ``` ==> sats(A, omega_fm(x), env) <-> omega(**A, nth(x,env))" ``` paulson@13323 ` 1478` ```by (simp add: omega_fm_def omega_def) ``` paulson@13316 ` 1479` paulson@13323 ` 1480` ```lemma omega_iff_sats: ``` paulson@13323 ` 1481` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13323 ` 1482` ``` i \ nat; env \ list(A)|] ``` paulson@13323 ` 1483` ``` ==> omega(**A, x) <-> sats(A, omega_fm(i), env)" ``` paulson@13323 ` 1484` ```by simp ``` paulson@13323 ` 1485` paulson@13323 ` 1486` ```theorem omega_reflection: ``` paulson@13323 ` 1487` ``` "REFLECTS[\x. omega(L,f(x)), ``` paulson@13323 ` 1488` ``` \i x. omega(**Lset(i),f(x))]" ``` paulson@13323 ` 1489` ```apply (simp only: omega_def setclass_simps) ``` paulson@13323 ` 1490` ```apply (intro FOL_reflections limit_ordinal_reflection) ``` paulson@13323 ` 1491` ```done ``` paulson@13323 ` 1492` paulson@13323 ` 1493` paulson@13323 ` 1494` ```lemmas fun_plus_reflections = ``` paulson@13323 ` 1495` ``` typed_function_reflection composition_reflection ``` paulson@13323 ` 1496` ``` injection_reflection surjection_reflection ``` paulson@13348 ` 1497` ``` bijection_reflection restriction_reflection ``` paulson@13348 ` 1498` ``` order_isomorphism_reflection ``` paulson@13323 ` 1499` ``` ordinal_reflection limit_ordinal_reflection omega_reflection ``` paulson@13323 ` 1500` paulson@13323 ` 1501` ```lemmas fun_plus_iff_sats = ``` paulson@13323 ` 1502` ``` typed_function_iff_sats composition_iff_sats ``` paulson@13348 ` 1503` ``` injection_iff_sats surjection_iff_sats ``` paulson@13348 ` 1504` ``` bijection_iff_sats restriction_iff_sats ``` paulson@13316 ` 1505` ``` order_isomorphism_iff_sats ``` paulson@13323 ` 1506` ``` ordinal_iff_sats limit_ordinal_iff_sats omega_iff_sats ``` paulson@13316 ` 1507` paulson@13223 ` 1508` ```end ```