src/ZF/Constructible/L_axioms.thy
 author paulson Mon Jul 08 15:56:39 2002 +0200 (2002-07-08) changeset 13314 84b9de3cbc91 parent 13309 a6adee8ea75a child 13316 d16629fd0f95 permissions -rw-r--r--
Defining a meta-existential quantifier.
Using it to streamline reflection proofs.
 paulson@13306 ` 1` ```header {*The Class L Satisfies the ZF Axioms*} ``` paulson@13223 ` 2` paulson@13314 ` 3` ```theory L_axioms = Formula + Relative + Reflection + MetaExists: ``` paulson@13223 ` 4` paulson@13223 ` 5` paulson@13223 ` 6` ```text {* The class L satisfies the premises of locale @{text M_axioms} *} ``` paulson@13223 ` 7` paulson@13223 ` 8` ```lemma transL: "[| y\x; L(x) |] ==> L(y)" ``` paulson@13223 ` 9` ```apply (insert Transset_Lset) ``` paulson@13223 ` 10` ```apply (simp add: Transset_def L_def, blast) ``` paulson@13223 ` 11` ```done ``` paulson@13223 ` 12` paulson@13223 ` 13` ```lemma nonempty: "L(0)" ``` paulson@13223 ` 14` ```apply (simp add: L_def) ``` paulson@13223 ` 15` ```apply (blast intro: zero_in_Lset) ``` paulson@13223 ` 16` ```done ``` paulson@13223 ` 17` paulson@13223 ` 18` ```lemma upair_ax: "upair_ax(L)" ``` paulson@13223 ` 19` ```apply (simp add: upair_ax_def upair_def, clarify) ``` paulson@13299 ` 20` ```apply (rule_tac x="{x,y}" in rexI) ``` paulson@13299 ` 21` ```apply (simp_all add: doubleton_in_L) ``` paulson@13223 ` 22` ```done ``` paulson@13223 ` 23` paulson@13223 ` 24` ```lemma Union_ax: "Union_ax(L)" ``` paulson@13223 ` 25` ```apply (simp add: Union_ax_def big_union_def, clarify) ``` paulson@13299 ` 26` ```apply (rule_tac x="Union(x)" in rexI) ``` paulson@13299 ` 27` ```apply (simp_all add: Union_in_L, auto) ``` paulson@13223 ` 28` ```apply (blast intro: transL) ``` paulson@13223 ` 29` ```done ``` paulson@13223 ` 30` paulson@13223 ` 31` ```lemma power_ax: "power_ax(L)" ``` paulson@13223 ` 32` ```apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify) ``` paulson@13299 ` 33` ```apply (rule_tac x="{y \ Pow(x). L(y)}" in rexI) ``` paulson@13299 ` 34` ```apply (simp_all add: LPow_in_L, auto) ``` paulson@13223 ` 35` ```apply (blast intro: transL) ``` paulson@13223 ` 36` ```done ``` paulson@13223 ` 37` paulson@13223 ` 38` ```subsubsection{*For L to satisfy Replacement *} ``` paulson@13223 ` 39` paulson@13223 ` 40` ```(*Can't move these to Formula unless the definition of univalent is moved ``` paulson@13223 ` 41` ```there too!*) ``` paulson@13223 ` 42` paulson@13223 ` 43` ```lemma LReplace_in_Lset: ``` paulson@13223 ` 44` ``` "[|X \ Lset(i); univalent(L,X,Q); Ord(i)|] ``` paulson@13223 ` 45` ``` ==> \j. Ord(j) & Replace(X, %x y. Q(x,y) & L(y)) \ Lset(j)" ``` paulson@13223 ` 46` ```apply (rule_tac x="\y \ Replace(X, %x y. Q(x,y) & L(y)). succ(lrank(y))" ``` paulson@13223 ` 47` ``` in exI) ``` paulson@13223 ` 48` ```apply simp ``` paulson@13223 ` 49` ```apply clarify ``` paulson@13223 ` 50` ```apply (rule_tac a="x" in UN_I) ``` paulson@13223 ` 51` ``` apply (simp_all add: Replace_iff univalent_def) ``` paulson@13223 ` 52` ```apply (blast dest: transL L_I) ``` paulson@13223 ` 53` ```done ``` paulson@13223 ` 54` paulson@13223 ` 55` ```lemma LReplace_in_L: ``` paulson@13223 ` 56` ``` "[|L(X); univalent(L,X,Q)|] ``` paulson@13223 ` 57` ``` ==> \Y. L(Y) & Replace(X, %x y. Q(x,y) & L(y)) \ Y" ``` paulson@13223 ` 58` ```apply (drule L_D, clarify) ``` paulson@13223 ` 59` ```apply (drule LReplace_in_Lset, assumption+) ``` paulson@13223 ` 60` ```apply (blast intro: L_I Lset_in_Lset_succ) ``` paulson@13223 ` 61` ```done ``` paulson@13223 ` 62` paulson@13223 ` 63` ```lemma replacement: "replacement(L,P)" ``` paulson@13223 ` 64` ```apply (simp add: replacement_def, clarify) ``` paulson@13268 ` 65` ```apply (frule LReplace_in_L, assumption+, clarify) ``` paulson@13299 ` 66` ```apply (rule_tac x=Y in rexI) ``` paulson@13299 ` 67` ```apply (simp_all add: Replace_iff univalent_def, blast) ``` paulson@13223 ` 68` ```done ``` paulson@13223 ` 69` paulson@13291 ` 70` ```subsection{*Instantiation of the locale @{text M_triv_axioms}*} ``` 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@13291 ` 94` ```fun trivaxL 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@13291 ` 99` ```bind_thm ("ball_abs", trivaxL (thm "M_triv_axioms.ball_abs")); ``` paulson@13291 ` 100` ```bind_thm ("rall_abs", trivaxL (thm "M_triv_axioms.rall_abs")); ``` paulson@13291 ` 101` ```bind_thm ("bex_abs", trivaxL (thm "M_triv_axioms.bex_abs")); ``` paulson@13291 ` 102` ```bind_thm ("rex_abs", trivaxL (thm "M_triv_axioms.rex_abs")); ``` paulson@13291 ` 103` ```bind_thm ("ball_iff_equiv", trivaxL (thm "M_triv_axioms.ball_iff_equiv")); ``` paulson@13291 ` 104` ```bind_thm ("M_equalityI", trivaxL (thm "M_triv_axioms.M_equalityI")); ``` paulson@13291 ` 105` ```bind_thm ("empty_abs", trivaxL (thm "M_triv_axioms.empty_abs")); ``` paulson@13291 ` 106` ```bind_thm ("subset_abs", trivaxL (thm "M_triv_axioms.subset_abs")); ``` paulson@13291 ` 107` ```bind_thm ("upair_abs", trivaxL (thm "M_triv_axioms.upair_abs")); ``` paulson@13291 ` 108` ```bind_thm ("upair_in_M_iff", trivaxL (thm "M_triv_axioms.upair_in_M_iff")); ``` paulson@13291 ` 109` ```bind_thm ("singleton_in_M_iff", trivaxL (thm "M_triv_axioms.singleton_in_M_iff")); ``` paulson@13291 ` 110` ```bind_thm ("pair_abs", trivaxL (thm "M_triv_axioms.pair_abs")); ``` paulson@13291 ` 111` ```bind_thm ("pair_in_M_iff", trivaxL (thm "M_triv_axioms.pair_in_M_iff")); ``` paulson@13291 ` 112` ```bind_thm ("pair_components_in_M", trivaxL (thm "M_triv_axioms.pair_components_in_M")); ``` paulson@13291 ` 113` ```bind_thm ("cartprod_abs", trivaxL (thm "M_triv_axioms.cartprod_abs")); ``` paulson@13291 ` 114` ```bind_thm ("union_abs", trivaxL (thm "M_triv_axioms.union_abs")); ``` paulson@13291 ` 115` ```bind_thm ("inter_abs", trivaxL (thm "M_triv_axioms.inter_abs")); ``` paulson@13291 ` 116` ```bind_thm ("setdiff_abs", trivaxL (thm "M_triv_axioms.setdiff_abs")); ``` paulson@13291 ` 117` ```bind_thm ("Union_abs", trivaxL (thm "M_triv_axioms.Union_abs")); ``` paulson@13291 ` 118` ```bind_thm ("Union_closed", trivaxL (thm "M_triv_axioms.Union_closed")); ``` paulson@13291 ` 119` ```bind_thm ("Un_closed", trivaxL (thm "M_triv_axioms.Un_closed")); ``` paulson@13291 ` 120` ```bind_thm ("cons_closed", trivaxL (thm "M_triv_axioms.cons_closed")); ``` paulson@13291 ` 121` ```bind_thm ("successor_abs", trivaxL (thm "M_triv_axioms.successor_abs")); ``` paulson@13291 ` 122` ```bind_thm ("succ_in_M_iff", trivaxL (thm "M_triv_axioms.succ_in_M_iff")); ``` paulson@13291 ` 123` ```bind_thm ("separation_closed", trivaxL (thm "M_triv_axioms.separation_closed")); ``` paulson@13291 ` 124` ```bind_thm ("strong_replacementI", trivaxL (thm "M_triv_axioms.strong_replacementI")); ``` paulson@13291 ` 125` ```bind_thm ("strong_replacement_closed", trivaxL (thm "M_triv_axioms.strong_replacement_closed")); ``` paulson@13291 ` 126` ```bind_thm ("RepFun_closed", trivaxL (thm "M_triv_axioms.RepFun_closed")); ``` paulson@13291 ` 127` ```bind_thm ("lam_closed", trivaxL (thm "M_triv_axioms.lam_closed")); ``` paulson@13291 ` 128` ```bind_thm ("image_abs", trivaxL (thm "M_triv_axioms.image_abs")); ``` paulson@13291 ` 129` ```bind_thm ("powerset_Pow", trivaxL (thm "M_triv_axioms.powerset_Pow")); ``` paulson@13291 ` 130` ```bind_thm ("powerset_imp_subset_Pow", trivaxL (thm "M_triv_axioms.powerset_imp_subset_Pow")); ``` paulson@13291 ` 131` ```bind_thm ("nat_into_M", trivaxL (thm "M_triv_axioms.nat_into_M")); ``` paulson@13291 ` 132` ```bind_thm ("nat_case_closed", trivaxL (thm "M_triv_axioms.nat_case_closed")); ``` paulson@13291 ` 133` ```bind_thm ("Inl_in_M_iff", trivaxL (thm "M_triv_axioms.Inl_in_M_iff")); ``` paulson@13291 ` 134` ```bind_thm ("Inr_in_M_iff", trivaxL (thm "M_triv_axioms.Inr_in_M_iff")); ``` paulson@13291 ` 135` ```bind_thm ("lt_closed", trivaxL (thm "M_triv_axioms.lt_closed")); ``` paulson@13291 ` 136` ```bind_thm ("transitive_set_abs", trivaxL (thm "M_triv_axioms.transitive_set_abs")); ``` paulson@13291 ` 137` ```bind_thm ("ordinal_abs", trivaxL (thm "M_triv_axioms.ordinal_abs")); ``` paulson@13291 ` 138` ```bind_thm ("limit_ordinal_abs", trivaxL (thm "M_triv_axioms.limit_ordinal_abs")); ``` paulson@13291 ` 139` ```bind_thm ("successor_ordinal_abs", trivaxL (thm "M_triv_axioms.successor_ordinal_abs")); ``` paulson@13291 ` 140` ```bind_thm ("finite_ordinal_abs", trivaxL (thm "M_triv_axioms.finite_ordinal_abs")); ``` paulson@13291 ` 141` ```bind_thm ("omega_abs", trivaxL (thm "M_triv_axioms.omega_abs")); ``` paulson@13291 ` 142` ```bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs")); ``` paulson@13291 ` 143` ```bind_thm ("number1_abs", trivaxL (thm "M_triv_axioms.number1_abs")); ``` paulson@13291 ` 144` ```bind_thm ("number3_abs", trivaxL (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@13314 ` 295` ```lemmas FOL_reflection = ``` 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@13314 ` 312` ```apply (drule ReflectsD, assumption) ``` paulson@13314 ` 313` ```apply blast ``` paulson@13314 ` 314` ```done ``` paulson@13291 ` 315` paulson@13291 ` 316` ```lemma Collect_mem_eq: "{x\A. x\B} = A \ B"; ``` paulson@13291 ` 317` ```by blast ``` paulson@13291 ` 318` paulson@13291 ` 319` paulson@13298 ` 320` ```subsection{*Internalized formulas for some relativized ones*} ``` paulson@13298 ` 321` paulson@13306 ` 322` ```lemmas setclass_simps = rall_setclass_is_ball rex_setclass_is_bex ``` paulson@13306 ` 323` paulson@13306 ` 324` ```subsubsection{*Some numbers to help write de Bruijn indices*} ``` paulson@13306 ` 325` paulson@13306 ` 326` ```syntax ``` paulson@13306 ` 327` ``` "3" :: i ("3") ``` paulson@13306 ` 328` ``` "4" :: i ("4") ``` paulson@13306 ` 329` ``` "5" :: i ("5") ``` paulson@13306 ` 330` ``` "6" :: i ("6") ``` paulson@13306 ` 331` ``` "7" :: i ("7") ``` paulson@13306 ` 332` ``` "8" :: i ("8") ``` paulson@13306 ` 333` ``` "9" :: i ("9") ``` paulson@13306 ` 334` paulson@13306 ` 335` ```translations ``` paulson@13306 ` 336` ``` "3" == "succ(2)" ``` paulson@13306 ` 337` ``` "4" == "succ(3)" ``` paulson@13306 ` 338` ``` "5" == "succ(4)" ``` paulson@13306 ` 339` ``` "6" == "succ(5)" ``` paulson@13306 ` 340` ``` "7" == "succ(6)" ``` paulson@13306 ` 341` ``` "8" == "succ(7)" ``` paulson@13306 ` 342` ``` "9" == "succ(8)" ``` paulson@13306 ` 343` paulson@13298 ` 344` ```subsubsection{*Unordered pairs*} ``` paulson@13298 ` 345` paulson@13298 ` 346` ```constdefs upair_fm :: "[i,i,i]=>i" ``` paulson@13298 ` 347` ``` "upair_fm(x,y,z) == ``` paulson@13298 ` 348` ``` And(Member(x,z), ``` paulson@13298 ` 349` ``` And(Member(y,z), ``` paulson@13298 ` 350` ``` Forall(Implies(Member(0,succ(z)), ``` paulson@13298 ` 351` ``` Or(Equal(0,succ(x)), Equal(0,succ(y)))))))" ``` paulson@13298 ` 352` paulson@13298 ` 353` ```lemma upair_type [TC]: ``` paulson@13298 ` 354` ``` "[| x \ nat; y \ nat; z \ nat |] ==> upair_fm(x,y,z) \ formula" ``` paulson@13298 ` 355` ```by (simp add: upair_fm_def) ``` paulson@13298 ` 356` paulson@13298 ` 357` ```lemma arity_upair_fm [simp]: ``` paulson@13298 ` 358` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13298 ` 359` ``` ==> arity(upair_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13298 ` 360` ```by (simp add: upair_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13298 ` 361` paulson@13298 ` 362` ```lemma sats_upair_fm [simp]: ``` paulson@13298 ` 363` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13298 ` 364` ``` ==> sats(A, upair_fm(x,y,z), env) <-> ``` paulson@13298 ` 365` ``` upair(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13298 ` 366` ```by (simp add: upair_fm_def upair_def) ``` paulson@13298 ` 367` paulson@13298 ` 368` ```lemma upair_iff_sats: ``` paulson@13298 ` 369` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13298 ` 370` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13298 ` 371` ``` ==> upair(**A, x, y, z) <-> sats(A, upair_fm(i,j,k), env)" ``` paulson@13298 ` 372` ```by (simp add: sats_upair_fm) ``` paulson@13298 ` 373` paulson@13298 ` 374` ```text{*Useful? At least it refers to "real" unordered pairs*} ``` paulson@13298 ` 375` ```lemma sats_upair_fm2 [simp]: ``` paulson@13298 ` 376` ``` "[| x \ nat; y \ nat; z < length(env); env \ list(A); Transset(A)|] ``` paulson@13298 ` 377` ``` ==> sats(A, upair_fm(x,y,z), env) <-> ``` paulson@13298 ` 378` ``` nth(z,env) = {nth(x,env), nth(y,env)}" ``` paulson@13298 ` 379` ```apply (frule lt_length_in_nat, assumption) ``` paulson@13298 ` 380` ```apply (simp add: upair_fm_def Transset_def, auto) ``` paulson@13298 ` 381` ```apply (blast intro: nth_type) ``` paulson@13298 ` 382` ```done ``` paulson@13298 ` 383` paulson@13314 ` 384` ```theorem upair_reflection: ``` paulson@13314 ` 385` ``` "REFLECTS[\x. upair(L,f(x),g(x),h(x)), ``` paulson@13314 ` 386` ``` \i x. upair(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 387` ```apply (simp add: upair_def) ``` paulson@13314 ` 388` ```apply (intro FOL_reflection) ``` paulson@13314 ` 389` ```done ``` paulson@13306 ` 390` paulson@13298 ` 391` ```subsubsection{*Ordered pairs*} ``` paulson@13298 ` 392` paulson@13298 ` 393` ```constdefs pair_fm :: "[i,i,i]=>i" ``` paulson@13298 ` 394` ``` "pair_fm(x,y,z) == ``` paulson@13298 ` 395` ``` Exists(And(upair_fm(succ(x),succ(x),0), ``` paulson@13298 ` 396` ``` Exists(And(upair_fm(succ(succ(x)),succ(succ(y)),0), ``` paulson@13298 ` 397` ``` upair_fm(1,0,succ(succ(z)))))))" ``` paulson@13298 ` 398` paulson@13298 ` 399` ```lemma pair_type [TC]: ``` paulson@13298 ` 400` ``` "[| x \ nat; y \ nat; z \ nat |] ==> pair_fm(x,y,z) \ formula" ``` paulson@13298 ` 401` ```by (simp add: pair_fm_def) ``` paulson@13298 ` 402` paulson@13298 ` 403` ```lemma arity_pair_fm [simp]: ``` paulson@13298 ` 404` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13298 ` 405` ``` ==> arity(pair_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13298 ` 406` ```by (simp add: pair_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13298 ` 407` paulson@13298 ` 408` ```lemma sats_pair_fm [simp]: ``` paulson@13298 ` 409` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13298 ` 410` ``` ==> sats(A, pair_fm(x,y,z), env) <-> ``` paulson@13298 ` 411` ``` pair(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13298 ` 412` ```by (simp add: pair_fm_def pair_def) ``` paulson@13298 ` 413` paulson@13298 ` 414` ```lemma pair_iff_sats: ``` paulson@13298 ` 415` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13298 ` 416` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13298 ` 417` ``` ==> pair(**A, x, y, z) <-> sats(A, pair_fm(i,j,k), env)" ``` paulson@13298 ` 418` ```by (simp add: sats_pair_fm) ``` paulson@13298 ` 419` paulson@13314 ` 420` ```theorem pair_reflection: ``` paulson@13314 ` 421` ``` "REFLECTS[\x. pair(L,f(x),g(x),h(x)), ``` paulson@13314 ` 422` ``` \i x. pair(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 423` ```apply (simp only: pair_def setclass_simps) ``` paulson@13314 ` 424` ```apply (intro FOL_reflection upair_reflection) ``` paulson@13314 ` 425` ```done ``` paulson@13306 ` 426` paulson@13306 ` 427` paulson@13306 ` 428` ```subsubsection{*Binary Unions*} ``` paulson@13298 ` 429` paulson@13306 ` 430` ```constdefs union_fm :: "[i,i,i]=>i" ``` paulson@13306 ` 431` ``` "union_fm(x,y,z) == ``` paulson@13306 ` 432` ``` Forall(Iff(Member(0,succ(z)), ``` paulson@13306 ` 433` ``` Or(Member(0,succ(x)),Member(0,succ(y)))))" ``` paulson@13306 ` 434` paulson@13306 ` 435` ```lemma union_type [TC]: ``` paulson@13306 ` 436` ``` "[| x \ nat; y \ nat; z \ nat |] ==> union_fm(x,y,z) \ formula" ``` paulson@13306 ` 437` ```by (simp add: union_fm_def) ``` paulson@13306 ` 438` paulson@13306 ` 439` ```lemma arity_union_fm [simp]: ``` paulson@13306 ` 440` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13306 ` 441` ``` ==> arity(union_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13306 ` 442` ```by (simp add: union_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13298 ` 443` paulson@13306 ` 444` ```lemma sats_union_fm [simp]: ``` paulson@13306 ` 445` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13306 ` 446` ``` ==> sats(A, union_fm(x,y,z), env) <-> ``` paulson@13306 ` 447` ``` union(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13306 ` 448` ```by (simp add: union_fm_def union_def) ``` paulson@13306 ` 449` paulson@13306 ` 450` ```lemma union_iff_sats: ``` paulson@13306 ` 451` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13306 ` 452` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13306 ` 453` ``` ==> union(**A, x, y, z) <-> sats(A, union_fm(i,j,k), env)" ``` paulson@13306 ` 454` ```by (simp add: sats_union_fm) ``` paulson@13298 ` 455` paulson@13314 ` 456` ```theorem union_reflection: ``` paulson@13314 ` 457` ``` "REFLECTS[\x. union(L,f(x),g(x),h(x)), ``` paulson@13314 ` 458` ``` \i x. union(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 459` ```apply (simp only: union_def setclass_simps) ``` paulson@13314 ` 460` ```apply (intro FOL_reflection) ``` paulson@13314 ` 461` ```done ``` paulson@13306 ` 462` paulson@13298 ` 463` paulson@13306 ` 464` ```subsubsection{*`Cons' for sets*} ``` paulson@13306 ` 465` paulson@13306 ` 466` ```constdefs cons_fm :: "[i,i,i]=>i" ``` paulson@13306 ` 467` ``` "cons_fm(x,y,z) == ``` paulson@13306 ` 468` ``` Exists(And(upair_fm(succ(x),succ(x),0), ``` paulson@13306 ` 469` ``` union_fm(0,succ(y),succ(z))))" ``` paulson@13298 ` 470` paulson@13298 ` 471` paulson@13306 ` 472` ```lemma cons_type [TC]: ``` paulson@13306 ` 473` ``` "[| x \ nat; y \ nat; z \ nat |] ==> cons_fm(x,y,z) \ formula" ``` paulson@13306 ` 474` ```by (simp add: cons_fm_def) ``` paulson@13306 ` 475` paulson@13306 ` 476` ```lemma arity_cons_fm [simp]: ``` paulson@13306 ` 477` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13306 ` 478` ``` ==> arity(cons_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13306 ` 479` ```by (simp add: cons_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 480` paulson@13306 ` 481` ```lemma sats_cons_fm [simp]: ``` paulson@13306 ` 482` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13306 ` 483` ``` ==> sats(A, cons_fm(x,y,z), env) <-> ``` paulson@13306 ` 484` ``` is_cons(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13306 ` 485` ```by (simp add: cons_fm_def is_cons_def) ``` paulson@13306 ` 486` paulson@13306 ` 487` ```lemma cons_iff_sats: ``` paulson@13306 ` 488` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13306 ` 489` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13306 ` 490` ``` ==> is_cons(**A, x, y, z) <-> sats(A, cons_fm(i,j,k), env)" ``` paulson@13306 ` 491` ```by simp ``` paulson@13306 ` 492` paulson@13314 ` 493` ```theorem cons_reflection: ``` paulson@13314 ` 494` ``` "REFLECTS[\x. is_cons(L,f(x),g(x),h(x)), ``` paulson@13314 ` 495` ``` \i x. is_cons(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 496` ```apply (simp only: is_cons_def setclass_simps) ``` paulson@13314 ` 497` ```apply (intro FOL_reflection upair_reflection union_reflection) ``` paulson@13314 ` 498` ```done ``` paulson@13298 ` 499` paulson@13298 ` 500` paulson@13306 ` 501` ```subsubsection{*Function Applications*} ``` paulson@13306 ` 502` paulson@13306 ` 503` ```constdefs fun_apply_fm :: "[i,i,i]=>i" ``` paulson@13306 ` 504` ``` "fun_apply_fm(f,x,y) == ``` paulson@13306 ` 505` ``` Forall(Iff(Exists(And(Member(0,succ(succ(f))), ``` paulson@13306 ` 506` ``` pair_fm(succ(succ(x)), 1, 0))), ``` paulson@13306 ` 507` ``` Equal(succ(y),0)))" ``` paulson@13298 ` 508` paulson@13306 ` 509` ```lemma fun_apply_type [TC]: ``` paulson@13306 ` 510` ``` "[| x \ nat; y \ nat; z \ nat |] ==> fun_apply_fm(x,y,z) \ formula" ``` paulson@13306 ` 511` ```by (simp add: fun_apply_fm_def) ``` paulson@13306 ` 512` paulson@13306 ` 513` ```lemma arity_fun_apply_fm [simp]: ``` paulson@13306 ` 514` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13306 ` 515` ``` ==> arity(fun_apply_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13306 ` 516` ```by (simp add: fun_apply_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13298 ` 517` paulson@13306 ` 518` ```lemma sats_fun_apply_fm [simp]: ``` paulson@13306 ` 519` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13306 ` 520` ``` ==> sats(A, fun_apply_fm(x,y,z), env) <-> ``` paulson@13306 ` 521` ``` fun_apply(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13306 ` 522` ```by (simp add: fun_apply_fm_def fun_apply_def) ``` paulson@13306 ` 523` paulson@13306 ` 524` ```lemma fun_apply_iff_sats: ``` paulson@13306 ` 525` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13306 ` 526` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13306 ` 527` ``` ==> fun_apply(**A, x, y, z) <-> sats(A, fun_apply_fm(i,j,k), env)" ``` paulson@13306 ` 528` ```by simp ``` paulson@13306 ` 529` paulson@13314 ` 530` ```theorem fun_apply_reflection: ``` paulson@13314 ` 531` ``` "REFLECTS[\x. fun_apply(L,f(x),g(x),h(x)), ``` paulson@13314 ` 532` ``` \i x. fun_apply(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 533` ```apply (simp only: fun_apply_def setclass_simps) ``` paulson@13314 ` 534` ```apply (intro FOL_reflection pair_reflection) ``` paulson@13314 ` 535` ```done ``` paulson@13298 ` 536` paulson@13298 ` 537` paulson@13306 ` 538` ```subsubsection{*Variants of Satisfaction Definitions for Ordinals, etc.*} ``` paulson@13306 ` 539` paulson@13306 ` 540` ```text{*Differs from the one in Formula by using "ordinal" rather than "Ord"*} ``` paulson@13306 ` 541` paulson@13306 ` 542` paulson@13306 ` 543` ```lemma sats_subset_fm': ``` paulson@13306 ` 544` ``` "[|x \ nat; y \ nat; env \ list(A)|] ``` paulson@13306 ` 545` ``` ==> sats(A, subset_fm(x,y), env) <-> subset(**A, nth(x,env), nth(y,env))" ``` paulson@13306 ` 546` ```by (simp add: subset_fm_def subset_def) ``` paulson@13298 ` 547` paulson@13314 ` 548` ```theorem subset_reflection: ``` paulson@13314 ` 549` ``` "REFLECTS[\x. subset(L,f(x),g(x)), ``` paulson@13314 ` 550` ``` \i x. subset(**Lset(i),f(x),g(x))]" ``` paulson@13314 ` 551` ```apply (simp only: subset_def setclass_simps) ``` paulson@13314 ` 552` ```apply (intro FOL_reflection) ``` paulson@13314 ` 553` ```done ``` paulson@13306 ` 554` paulson@13306 ` 555` ```lemma sats_transset_fm': ``` paulson@13306 ` 556` ``` "[|x \ nat; env \ list(A)|] ``` paulson@13306 ` 557` ``` ==> sats(A, transset_fm(x), env) <-> transitive_set(**A, nth(x,env))" ``` paulson@13306 ` 558` ```by (simp add: sats_subset_fm' transset_fm_def transitive_set_def) ``` paulson@13298 ` 559` paulson@13314 ` 560` ```theorem transitive_set_reflection: ``` paulson@13314 ` 561` ``` "REFLECTS[\x. transitive_set(L,f(x)), ``` paulson@13314 ` 562` ``` \i x. transitive_set(**Lset(i),f(x))]" ``` paulson@13314 ` 563` ```apply (simp only: transitive_set_def setclass_simps) ``` paulson@13314 ` 564` ```apply (intro FOL_reflection subset_reflection) ``` paulson@13314 ` 565` ```done ``` paulson@13306 ` 566` paulson@13306 ` 567` ```lemma sats_ordinal_fm': ``` paulson@13306 ` 568` ``` "[|x \ nat; env \ list(A)|] ``` paulson@13306 ` 569` ``` ==> sats(A, ordinal_fm(x), env) <-> ordinal(**A,nth(x,env))" ``` paulson@13306 ` 570` ```by (simp add: sats_transset_fm' ordinal_fm_def ordinal_def) ``` paulson@13306 ` 571` paulson@13306 ` 572` ```lemma ordinal_iff_sats: ``` paulson@13306 ` 573` ``` "[| nth(i,env) = x; i \ nat; env \ list(A)|] ``` paulson@13306 ` 574` ``` ==> ordinal(**A, x) <-> sats(A, ordinal_fm(i), env)" ``` paulson@13306 ` 575` ```by (simp add: sats_ordinal_fm') ``` paulson@13306 ` 576` paulson@13314 ` 577` ```theorem ordinal_reflection: ``` paulson@13314 ` 578` ``` "REFLECTS[\x. ordinal(L,f(x)), \i x. ordinal(**Lset(i),f(x))]" ``` paulson@13314 ` 579` ```apply (simp only: ordinal_def setclass_simps) ``` paulson@13314 ` 580` ```apply (intro FOL_reflection transitive_set_reflection) ``` paulson@13314 ` 581` ```done ``` paulson@13298 ` 582` paulson@13298 ` 583` paulson@13306 ` 584` ```subsubsection{*Membership Relation*} ``` paulson@13298 ` 585` paulson@13306 ` 586` ```constdefs Memrel_fm :: "[i,i]=>i" ``` paulson@13306 ` 587` ``` "Memrel_fm(A,r) == ``` paulson@13306 ` 588` ``` Forall(Iff(Member(0,succ(r)), ``` paulson@13306 ` 589` ``` Exists(And(Member(0,succ(succ(A))), ``` paulson@13306 ` 590` ``` Exists(And(Member(0,succ(succ(succ(A)))), ``` paulson@13306 ` 591` ``` And(Member(1,0), ``` paulson@13306 ` 592` ``` pair_fm(1,0,2))))))))" ``` paulson@13306 ` 593` paulson@13306 ` 594` ```lemma Memrel_type [TC]: ``` paulson@13306 ` 595` ``` "[| x \ nat; y \ nat |] ==> Memrel_fm(x,y) \ formula" ``` paulson@13306 ` 596` ```by (simp add: Memrel_fm_def) ``` paulson@13298 ` 597` paulson@13306 ` 598` ```lemma arity_Memrel_fm [simp]: ``` paulson@13306 ` 599` ``` "[| x \ nat; y \ nat |] ``` paulson@13306 ` 600` ``` ==> arity(Memrel_fm(x,y)) = succ(x) \ succ(y)" ``` paulson@13306 ` 601` ```by (simp add: Memrel_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 602` paulson@13306 ` 603` ```lemma sats_Memrel_fm [simp]: ``` paulson@13306 ` 604` ``` "[| x \ nat; y \ nat; env \ list(A)|] ``` paulson@13306 ` 605` ``` ==> sats(A, Memrel_fm(x,y), env) <-> ``` paulson@13306 ` 606` ``` membership(**A, nth(x,env), nth(y,env))" ``` paulson@13306 ` 607` ```by (simp add: Memrel_fm_def membership_def) ``` paulson@13298 ` 608` paulson@13306 ` 609` ```lemma Memrel_iff_sats: ``` paulson@13306 ` 610` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13306 ` 611` ``` i \ nat; j \ nat; env \ list(A)|] ``` paulson@13306 ` 612` ``` ==> membership(**A, x, y) <-> sats(A, Memrel_fm(i,j), env)" ``` paulson@13306 ` 613` ```by simp ``` paulson@13304 ` 614` paulson@13314 ` 615` ```theorem membership_reflection: ``` paulson@13314 ` 616` ``` "REFLECTS[\x. membership(L,f(x),g(x)), ``` paulson@13314 ` 617` ``` \i x. membership(**Lset(i),f(x),g(x))]" ``` paulson@13314 ` 618` ```apply (simp only: membership_def setclass_simps) ``` paulson@13314 ` 619` ```apply (intro FOL_reflection pair_reflection) ``` paulson@13314 ` 620` ```done ``` paulson@13304 ` 621` paulson@13306 ` 622` ```subsubsection{*Predecessor Set*} ``` paulson@13304 ` 623` paulson@13306 ` 624` ```constdefs pred_set_fm :: "[i,i,i,i]=>i" ``` paulson@13306 ` 625` ``` "pred_set_fm(A,x,r,B) == ``` paulson@13306 ` 626` ``` Forall(Iff(Member(0,succ(B)), ``` paulson@13306 ` 627` ``` Exists(And(Member(0,succ(succ(r))), ``` paulson@13306 ` 628` ``` And(Member(1,succ(succ(A))), ``` paulson@13306 ` 629` ``` pair_fm(1,succ(succ(x)),0))))))" ``` paulson@13306 ` 630` paulson@13306 ` 631` paulson@13306 ` 632` ```lemma pred_set_type [TC]: ``` paulson@13306 ` 633` ``` "[| A \ nat; x \ nat; r \ nat; B \ nat |] ``` paulson@13306 ` 634` ``` ==> pred_set_fm(A,x,r,B) \ formula" ``` paulson@13306 ` 635` ```by (simp add: pred_set_fm_def) ``` paulson@13304 ` 636` paulson@13306 ` 637` ```lemma arity_pred_set_fm [simp]: ``` paulson@13306 ` 638` ``` "[| A \ nat; x \ nat; r \ nat; B \ nat |] ``` paulson@13306 ` 639` ``` ==> arity(pred_set_fm(A,x,r,B)) = succ(A) \ succ(x) \ succ(r) \ succ(B)" ``` paulson@13306 ` 640` ```by (simp add: pred_set_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 641` paulson@13306 ` 642` ```lemma sats_pred_set_fm [simp]: ``` paulson@13306 ` 643` ``` "[| U \ nat; x \ nat; r \ nat; B \ nat; env \ list(A)|] ``` paulson@13306 ` 644` ``` ==> sats(A, pred_set_fm(U,x,r,B), env) <-> ``` paulson@13306 ` 645` ``` pred_set(**A, nth(U,env), nth(x,env), nth(r,env), nth(B,env))" ``` paulson@13306 ` 646` ```by (simp add: pred_set_fm_def pred_set_def) ``` paulson@13306 ` 647` paulson@13306 ` 648` ```lemma pred_set_iff_sats: ``` paulson@13306 ` 649` ``` "[| nth(i,env) = U; nth(j,env) = x; nth(k,env) = r; nth(l,env) = B; ``` paulson@13306 ` 650` ``` i \ nat; j \ nat; k \ nat; l \ nat; env \ list(A)|] ``` paulson@13306 ` 651` ``` ==> pred_set(**A,U,x,r,B) <-> sats(A, pred_set_fm(i,j,k,l), env)" ``` paulson@13306 ` 652` ```by (simp add: sats_pred_set_fm) ``` paulson@13306 ` 653` paulson@13314 ` 654` ```theorem pred_set_reflection: ``` paulson@13314 ` 655` ``` "REFLECTS[\x. pred_set(L,f(x),g(x),h(x),b(x)), ``` paulson@13314 ` 656` ``` \i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]" ``` paulson@13314 ` 657` ```apply (simp only: pred_set_def setclass_simps) ``` paulson@13314 ` 658` ```apply (intro FOL_reflection pair_reflection) ``` paulson@13314 ` 659` ```done ``` paulson@13304 ` 660` paulson@13304 ` 661` paulson@13298 ` 662` paulson@13306 ` 663` ```subsubsection{*Domain*} ``` paulson@13306 ` 664` paulson@13306 ` 665` ```(* "is_domain(M,r,z) == ``` paulson@13306 ` 666` ``` \x[M]. (x \ z <-> (\w[M]. w\r & (\y[M]. pair(M,x,y,w))))" *) ``` paulson@13306 ` 667` ```constdefs domain_fm :: "[i,i]=>i" ``` paulson@13306 ` 668` ``` "domain_fm(r,z) == ``` paulson@13306 ` 669` ``` Forall(Iff(Member(0,succ(z)), ``` paulson@13306 ` 670` ``` Exists(And(Member(0,succ(succ(r))), ``` paulson@13306 ` 671` ``` Exists(pair_fm(2,0,1))))))" ``` paulson@13306 ` 672` paulson@13306 ` 673` ```lemma domain_type [TC]: ``` paulson@13306 ` 674` ``` "[| x \ nat; y \ nat |] ==> domain_fm(x,y) \ formula" ``` paulson@13306 ` 675` ```by (simp add: domain_fm_def) ``` paulson@13306 ` 676` paulson@13306 ` 677` ```lemma arity_domain_fm [simp]: ``` paulson@13306 ` 678` ``` "[| x \ nat; y \ nat |] ``` paulson@13306 ` 679` ``` ==> arity(domain_fm(x,y)) = succ(x) \ succ(y)" ``` paulson@13306 ` 680` ```by (simp add: domain_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 681` paulson@13306 ` 682` ```lemma sats_domain_fm [simp]: ``` paulson@13306 ` 683` ``` "[| x \ nat; y \ nat; env \ list(A)|] ``` paulson@13306 ` 684` ``` ==> sats(A, domain_fm(x,y), env) <-> ``` paulson@13306 ` 685` ``` is_domain(**A, nth(x,env), nth(y,env))" ``` paulson@13306 ` 686` ```by (simp add: domain_fm_def is_domain_def) ``` paulson@13306 ` 687` paulson@13306 ` 688` ```lemma domain_iff_sats: ``` paulson@13306 ` 689` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13306 ` 690` ``` i \ nat; j \ nat; env \ list(A)|] ``` paulson@13306 ` 691` ``` ==> is_domain(**A, x, y) <-> sats(A, domain_fm(i,j), env)" ``` paulson@13306 ` 692` ```by simp ``` paulson@13306 ` 693` paulson@13314 ` 694` ```theorem domain_reflection: ``` paulson@13314 ` 695` ``` "REFLECTS[\x. is_domain(L,f(x),g(x)), ``` paulson@13314 ` 696` ``` \i x. is_domain(**Lset(i),f(x),g(x))]" ``` paulson@13314 ` 697` ```apply (simp only: is_domain_def setclass_simps) ``` paulson@13314 ` 698` ```apply (intro FOL_reflection pair_reflection) ``` paulson@13314 ` 699` ```done ``` paulson@13306 ` 700` paulson@13306 ` 701` paulson@13306 ` 702` ```subsubsection{*Range*} ``` paulson@13306 ` 703` paulson@13306 ` 704` ```(* "is_range(M,r,z) == ``` paulson@13306 ` 705` ``` \y[M]. (y \ z <-> (\w[M]. w\r & (\x[M]. pair(M,x,y,w))))" *) ``` paulson@13306 ` 706` ```constdefs range_fm :: "[i,i]=>i" ``` paulson@13306 ` 707` ``` "range_fm(r,z) == ``` paulson@13306 ` 708` ``` Forall(Iff(Member(0,succ(z)), ``` paulson@13306 ` 709` ``` Exists(And(Member(0,succ(succ(r))), ``` paulson@13306 ` 710` ``` Exists(pair_fm(0,2,1))))))" ``` paulson@13306 ` 711` paulson@13306 ` 712` ```lemma range_type [TC]: ``` paulson@13306 ` 713` ``` "[| x \ nat; y \ nat |] ==> range_fm(x,y) \ formula" ``` paulson@13306 ` 714` ```by (simp add: range_fm_def) ``` paulson@13306 ` 715` paulson@13306 ` 716` ```lemma arity_range_fm [simp]: ``` paulson@13306 ` 717` ``` "[| x \ nat; y \ nat |] ``` paulson@13306 ` 718` ``` ==> arity(range_fm(x,y)) = succ(x) \ succ(y)" ``` paulson@13306 ` 719` ```by (simp add: range_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 720` paulson@13306 ` 721` ```lemma sats_range_fm [simp]: ``` paulson@13306 ` 722` ``` "[| x \ nat; y \ nat; env \ list(A)|] ``` paulson@13306 ` 723` ``` ==> sats(A, range_fm(x,y), env) <-> ``` paulson@13306 ` 724` ``` is_range(**A, nth(x,env), nth(y,env))" ``` paulson@13306 ` 725` ```by (simp add: range_fm_def is_range_def) ``` paulson@13306 ` 726` paulson@13306 ` 727` ```lemma range_iff_sats: ``` paulson@13306 ` 728` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13306 ` 729` ``` i \ nat; j \ nat; env \ list(A)|] ``` paulson@13306 ` 730` ``` ==> is_range(**A, x, y) <-> sats(A, range_fm(i,j), env)" ``` paulson@13306 ` 731` ```by simp ``` paulson@13306 ` 732` paulson@13314 ` 733` ```theorem range_reflection: ``` paulson@13314 ` 734` ``` "REFLECTS[\x. is_range(L,f(x),g(x)), ``` paulson@13314 ` 735` ``` \i x. is_range(**Lset(i),f(x),g(x))]" ``` paulson@13314 ` 736` ```apply (simp only: is_range_def setclass_simps) ``` paulson@13314 ` 737` ```apply (intro FOL_reflection pair_reflection) ``` paulson@13314 ` 738` ```done ``` paulson@13306 ` 739` paulson@13306 ` 740` ``` ``` paulson@13306 ` 741` ```subsubsection{*Image*} ``` paulson@13306 ` 742` paulson@13306 ` 743` ```(* "image(M,r,A,z) == ``` paulson@13306 ` 744` ``` \y[M]. (y \ z <-> (\w[M]. w\r & (\x[M]. x\A & pair(M,x,y,w))))" *) ``` paulson@13306 ` 745` ```constdefs image_fm :: "[i,i,i]=>i" ``` paulson@13306 ` 746` ``` "image_fm(r,A,z) == ``` paulson@13306 ` 747` ``` Forall(Iff(Member(0,succ(z)), ``` paulson@13306 ` 748` ``` Exists(And(Member(0,succ(succ(r))), ``` paulson@13306 ` 749` ``` Exists(And(Member(0,succ(succ(succ(A)))), ``` paulson@13306 ` 750` ``` pair_fm(0,2,1)))))))" ``` paulson@13306 ` 751` paulson@13306 ` 752` ```lemma image_type [TC]: ``` paulson@13306 ` 753` ``` "[| x \ nat; y \ nat; z \ nat |] ==> image_fm(x,y,z) \ formula" ``` paulson@13306 ` 754` ```by (simp add: image_fm_def) ``` paulson@13306 ` 755` paulson@13306 ` 756` ```lemma arity_image_fm [simp]: ``` paulson@13306 ` 757` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13306 ` 758` ``` ==> arity(image_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13306 ` 759` ```by (simp add: image_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 760` paulson@13306 ` 761` ```lemma sats_image_fm [simp]: ``` paulson@13306 ` 762` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13306 ` 763` ``` ==> sats(A, image_fm(x,y,z), env) <-> ``` paulson@13306 ` 764` ``` image(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13306 ` 765` ```by (simp add: image_fm_def image_def) ``` paulson@13306 ` 766` paulson@13306 ` 767` ```lemma image_iff_sats: ``` paulson@13306 ` 768` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13306 ` 769` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13306 ` 770` ``` ==> image(**A, x, y, z) <-> sats(A, image_fm(i,j,k), env)" ``` paulson@13306 ` 771` ```by (simp add: sats_image_fm) ``` paulson@13306 ` 772` paulson@13314 ` 773` ```theorem image_reflection: ``` paulson@13314 ` 774` ``` "REFLECTS[\x. image(L,f(x),g(x),h(x)), ``` paulson@13314 ` 775` ``` \i x. image(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 776` ```apply (simp only: image_def setclass_simps) ``` paulson@13314 ` 777` ```apply (intro FOL_reflection pair_reflection) ``` paulson@13314 ` 778` ```done ``` paulson@13306 ` 779` paulson@13306 ` 780` paulson@13306 ` 781` ```subsubsection{*The Concept of Relation*} ``` paulson@13306 ` 782` paulson@13306 ` 783` ```(* "is_relation(M,r) == ``` paulson@13306 ` 784` ``` (\z[M]. z\r --> (\x[M]. \y[M]. pair(M,x,y,z)))" *) ``` paulson@13306 ` 785` ```constdefs relation_fm :: "i=>i" ``` paulson@13306 ` 786` ``` "relation_fm(r) == ``` paulson@13306 ` 787` ``` Forall(Implies(Member(0,succ(r)), Exists(Exists(pair_fm(1,0,2)))))" ``` paulson@13306 ` 788` paulson@13306 ` 789` ```lemma relation_type [TC]: ``` paulson@13306 ` 790` ``` "[| x \ nat |] ==> relation_fm(x) \ formula" ``` paulson@13306 ` 791` ```by (simp add: relation_fm_def) ``` paulson@13306 ` 792` paulson@13306 ` 793` ```lemma arity_relation_fm [simp]: ``` paulson@13306 ` 794` ``` "x \ nat ==> arity(relation_fm(x)) = succ(x)" ``` paulson@13306 ` 795` ```by (simp add: relation_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 796` paulson@13306 ` 797` ```lemma sats_relation_fm [simp]: ``` paulson@13306 ` 798` ``` "[| x \ nat; env \ list(A)|] ``` paulson@13306 ` 799` ``` ==> sats(A, relation_fm(x), env) <-> is_relation(**A, nth(x,env))" ``` paulson@13306 ` 800` ```by (simp add: relation_fm_def is_relation_def) ``` paulson@13306 ` 801` paulson@13306 ` 802` ```lemma relation_iff_sats: ``` paulson@13306 ` 803` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13306 ` 804` ``` i \ nat; env \ list(A)|] ``` paulson@13306 ` 805` ``` ==> is_relation(**A, x) <-> sats(A, relation_fm(i), env)" ``` paulson@13306 ` 806` ```by simp ``` paulson@13306 ` 807` paulson@13314 ` 808` ```theorem is_relation_reflection: ``` paulson@13314 ` 809` ``` "REFLECTS[\x. is_relation(L,f(x)), ``` paulson@13314 ` 810` ``` \i x. is_relation(**Lset(i),f(x))]" ``` paulson@13314 ` 811` ```apply (simp only: is_relation_def setclass_simps) ``` paulson@13314 ` 812` ```apply (intro FOL_reflection pair_reflection) ``` paulson@13314 ` 813` ```done ``` paulson@13306 ` 814` paulson@13306 ` 815` paulson@13306 ` 816` ```subsubsection{*The Concept of Function*} ``` paulson@13306 ` 817` paulson@13306 ` 818` ```(* "is_function(M,r) == ``` paulson@13306 ` 819` ``` \x[M]. \y[M]. \y'[M]. \p[M]. \p'[M]. ``` paulson@13306 ` 820` ``` pair(M,x,y,p) --> pair(M,x,y',p') --> p\r --> p'\r --> y=y'" *) ``` paulson@13306 ` 821` ```constdefs function_fm :: "i=>i" ``` paulson@13306 ` 822` ``` "function_fm(r) == ``` paulson@13306 ` 823` ``` Forall(Forall(Forall(Forall(Forall( ``` paulson@13306 ` 824` ``` Implies(pair_fm(4,3,1), ``` paulson@13306 ` 825` ``` Implies(pair_fm(4,2,0), ``` paulson@13306 ` 826` ``` Implies(Member(1,r#+5), ``` paulson@13306 ` 827` ``` Implies(Member(0,r#+5), Equal(3,2))))))))))" ``` paulson@13306 ` 828` paulson@13306 ` 829` ```lemma function_type [TC]: ``` paulson@13306 ` 830` ``` "[| x \ nat |] ==> function_fm(x) \ formula" ``` paulson@13306 ` 831` ```by (simp add: function_fm_def) ``` paulson@13306 ` 832` paulson@13306 ` 833` ```lemma arity_function_fm [simp]: ``` paulson@13306 ` 834` ``` "x \ nat ==> arity(function_fm(x)) = succ(x)" ``` paulson@13306 ` 835` ```by (simp add: function_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13306 ` 836` paulson@13306 ` 837` ```lemma sats_function_fm [simp]: ``` paulson@13306 ` 838` ``` "[| x \ nat; env \ list(A)|] ``` paulson@13306 ` 839` ``` ==> sats(A, function_fm(x), env) <-> is_function(**A, nth(x,env))" ``` paulson@13306 ` 840` ```by (simp add: function_fm_def is_function_def) ``` paulson@13306 ` 841` paulson@13306 ` 842` ```lemma function_iff_sats: ``` paulson@13306 ` 843` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13306 ` 844` ``` i \ nat; env \ list(A)|] ``` paulson@13306 ` 845` ``` ==> is_function(**A, x) <-> sats(A, function_fm(i), env)" ``` paulson@13306 ` 846` ```by simp ``` paulson@13306 ` 847` paulson@13314 ` 848` ```theorem is_function_reflection: ``` paulson@13314 ` 849` ``` "REFLECTS[\x. is_function(L,f(x)), ``` paulson@13314 ` 850` ``` \i x. is_function(**Lset(i),f(x))]" ``` paulson@13314 ` 851` ```apply (simp only: is_function_def setclass_simps) ``` paulson@13314 ` 852` ```apply (intro FOL_reflection pair_reflection) ``` paulson@13314 ` 853` ```done ``` paulson@13298 ` 854` paulson@13298 ` 855` paulson@13309 ` 856` ```subsubsection{*Typed Functions*} ``` paulson@13309 ` 857` paulson@13309 ` 858` ```(* "typed_function(M,A,B,r) == ``` paulson@13309 ` 859` ``` is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) & ``` paulson@13309 ` 860` ``` (\u[M]. u\r --> (\x[M]. \y[M]. pair(M,x,y,u) --> y\B))" *) ``` paulson@13309 ` 861` paulson@13309 ` 862` ```constdefs typed_function_fm :: "[i,i,i]=>i" ``` paulson@13309 ` 863` ``` "typed_function_fm(A,B,r) == ``` paulson@13309 ` 864` ``` And(function_fm(r), ``` paulson@13309 ` 865` ``` And(relation_fm(r), ``` paulson@13309 ` 866` ``` And(domain_fm(r,A), ``` paulson@13309 ` 867` ``` Forall(Implies(Member(0,succ(r)), ``` paulson@13309 ` 868` ``` Forall(Forall(Implies(pair_fm(1,0,2),Member(0,B#+3)))))))))" ``` paulson@13309 ` 869` paulson@13309 ` 870` ```lemma typed_function_type [TC]: ``` paulson@13309 ` 871` ``` "[| x \ nat; y \ nat; z \ nat |] ==> typed_function_fm(x,y,z) \ formula" ``` paulson@13309 ` 872` ```by (simp add: typed_function_fm_def) ``` paulson@13309 ` 873` paulson@13309 ` 874` ```lemma arity_typed_function_fm [simp]: ``` paulson@13309 ` 875` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13309 ` 876` ``` ==> arity(typed_function_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13309 ` 877` ```by (simp add: typed_function_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13309 ` 878` paulson@13309 ` 879` ```lemma sats_typed_function_fm [simp]: ``` paulson@13309 ` 880` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13309 ` 881` ``` ==> sats(A, typed_function_fm(x,y,z), env) <-> ``` paulson@13309 ` 882` ``` typed_function(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13309 ` 883` ```by (simp add: typed_function_fm_def typed_function_def) ``` paulson@13309 ` 884` paulson@13309 ` 885` ```lemma typed_function_iff_sats: ``` paulson@13309 ` 886` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13309 ` 887` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13309 ` 888` ``` ==> typed_function(**A, x, y, z) <-> sats(A, typed_function_fm(i,j,k), env)" ``` paulson@13309 ` 889` ```by simp ``` paulson@13309 ` 890` paulson@13314 ` 891` ```lemmas function_reflection = ``` paulson@13314 ` 892` ``` upair_reflection pair_reflection union_reflection ``` paulson@13314 ` 893` ``` cons_reflection fun_apply_reflection subset_reflection ``` paulson@13314 ` 894` ``` transitive_set_reflection ordinal_reflection membership_reflection ``` paulson@13314 ` 895` ``` pred_set_reflection domain_reflection range_reflection image_reflection ``` paulson@13314 ` 896` ``` is_relation_reflection is_function_reflection ``` paulson@13309 ` 897` paulson@13309 ` 898` paulson@13314 ` 899` ```theorem typed_function_reflection: ``` paulson@13314 ` 900` ``` "REFLECTS[\x. typed_function(L,f(x),g(x),h(x)), ``` paulson@13314 ` 901` ``` \i x. typed_function(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 902` ```apply (simp only: typed_function_def setclass_simps) ``` paulson@13314 ` 903` ```apply (intro FOL_reflection function_reflection) ``` paulson@13314 ` 904` ```done ``` paulson@13314 ` 905` paulson@13309 ` 906` paulson@13309 ` 907` ```subsubsection{*Injections*} ``` paulson@13309 ` 908` paulson@13309 ` 909` ```(* "injection(M,A,B,f) == ``` paulson@13309 ` 910` ``` typed_function(M,A,B,f) & ``` paulson@13309 ` 911` ``` (\x[M]. \x'[M]. \y[M]. \p[M]. \p'[M]. ``` paulson@13309 ` 912` ``` pair(M,x,y,p) --> pair(M,x',y,p') --> p\f --> p'\f --> x=x')" *) ``` paulson@13309 ` 913` ```constdefs injection_fm :: "[i,i,i]=>i" ``` paulson@13309 ` 914` ``` "injection_fm(A,B,f) == ``` paulson@13309 ` 915` ``` And(typed_function_fm(A,B,f), ``` paulson@13309 ` 916` ``` Forall(Forall(Forall(Forall(Forall( ``` paulson@13309 ` 917` ``` Implies(pair_fm(4,2,1), ``` paulson@13309 ` 918` ``` Implies(pair_fm(3,2,0), ``` paulson@13309 ` 919` ``` Implies(Member(1,f#+5), ``` paulson@13309 ` 920` ``` Implies(Member(0,f#+5), Equal(4,3)))))))))))" ``` paulson@13309 ` 921` paulson@13309 ` 922` paulson@13309 ` 923` ```lemma injection_type [TC]: ``` paulson@13309 ` 924` ``` "[| x \ nat; y \ nat; z \ nat |] ==> injection_fm(x,y,z) \ formula" ``` paulson@13309 ` 925` ```by (simp add: injection_fm_def) ``` paulson@13309 ` 926` paulson@13309 ` 927` ```lemma arity_injection_fm [simp]: ``` paulson@13309 ` 928` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13309 ` 929` ``` ==> arity(injection_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13309 ` 930` ```by (simp add: injection_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13309 ` 931` paulson@13309 ` 932` ```lemma sats_injection_fm [simp]: ``` paulson@13309 ` 933` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13309 ` 934` ``` ==> sats(A, injection_fm(x,y,z), env) <-> ``` paulson@13309 ` 935` ``` injection(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13309 ` 936` ```by (simp add: injection_fm_def injection_def) ``` paulson@13309 ` 937` paulson@13309 ` 938` ```lemma injection_iff_sats: ``` paulson@13309 ` 939` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13309 ` 940` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13309 ` 941` ``` ==> injection(**A, x, y, z) <-> sats(A, injection_fm(i,j,k), env)" ``` paulson@13309 ` 942` ```by simp ``` paulson@13309 ` 943` paulson@13314 ` 944` ```theorem injection_reflection: ``` paulson@13314 ` 945` ``` "REFLECTS[\x. injection(L,f(x),g(x),h(x)), ``` paulson@13314 ` 946` ``` \i x. injection(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 947` ```apply (simp only: injection_def setclass_simps) ``` paulson@13314 ` 948` ```apply (intro FOL_reflection function_reflection typed_function_reflection) ``` paulson@13314 ` 949` ```done ``` paulson@13309 ` 950` paulson@13309 ` 951` paulson@13309 ` 952` ```subsubsection{*Surjections*} ``` paulson@13309 ` 953` paulson@13309 ` 954` ```(* surjection :: "[i=>o,i,i,i] => o" ``` paulson@13309 ` 955` ``` "surjection(M,A,B,f) == ``` paulson@13309 ` 956` ``` typed_function(M,A,B,f) & ``` paulson@13309 ` 957` ``` (\y[M]. y\B --> (\x[M]. x\A & fun_apply(M,f,x,y)))" *) ``` paulson@13309 ` 958` ```constdefs surjection_fm :: "[i,i,i]=>i" ``` paulson@13309 ` 959` ``` "surjection_fm(A,B,f) == ``` paulson@13309 ` 960` ``` And(typed_function_fm(A,B,f), ``` paulson@13309 ` 961` ``` Forall(Implies(Member(0,succ(B)), ``` paulson@13309 ` 962` ``` Exists(And(Member(0,succ(succ(A))), ``` paulson@13309 ` 963` ``` fun_apply_fm(succ(succ(f)),0,1))))))" ``` paulson@13309 ` 964` paulson@13309 ` 965` ```lemma surjection_type [TC]: ``` paulson@13309 ` 966` ``` "[| x \ nat; y \ nat; z \ nat |] ==> surjection_fm(x,y,z) \ formula" ``` paulson@13309 ` 967` ```by (simp add: surjection_fm_def) ``` paulson@13309 ` 968` paulson@13309 ` 969` ```lemma arity_surjection_fm [simp]: ``` paulson@13309 ` 970` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13309 ` 971` ``` ==> arity(surjection_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13309 ` 972` ```by (simp add: surjection_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13309 ` 973` paulson@13309 ` 974` ```lemma sats_surjection_fm [simp]: ``` paulson@13309 ` 975` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13309 ` 976` ``` ==> sats(A, surjection_fm(x,y,z), env) <-> ``` paulson@13309 ` 977` ``` surjection(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13309 ` 978` ```by (simp add: surjection_fm_def surjection_def) ``` paulson@13309 ` 979` paulson@13309 ` 980` ```lemma surjection_iff_sats: ``` paulson@13309 ` 981` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13309 ` 982` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13309 ` 983` ``` ==> surjection(**A, x, y, z) <-> sats(A, surjection_fm(i,j,k), env)" ``` paulson@13309 ` 984` ```by simp ``` paulson@13309 ` 985` paulson@13314 ` 986` ```theorem surjection_reflection: ``` paulson@13314 ` 987` ``` "REFLECTS[\x. surjection(L,f(x),g(x),h(x)), ``` paulson@13314 ` 988` ``` \i x. surjection(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 989` ```apply (simp only: surjection_def setclass_simps) ``` paulson@13314 ` 990` ```apply (intro FOL_reflection function_reflection typed_function_reflection) ``` paulson@13314 ` 991` ```done ``` paulson@13309 ` 992` paulson@13309 ` 993` paulson@13309 ` 994` paulson@13309 ` 995` ```subsubsection{*Bijections*} ``` paulson@13309 ` 996` paulson@13309 ` 997` ```(* bijection :: "[i=>o,i,i,i] => o" ``` paulson@13309 ` 998` ``` "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" *) ``` paulson@13309 ` 999` ```constdefs bijection_fm :: "[i,i,i]=>i" ``` paulson@13309 ` 1000` ``` "bijection_fm(A,B,f) == And(injection_fm(A,B,f), surjection_fm(A,B,f))" ``` paulson@13309 ` 1001` paulson@13309 ` 1002` ```lemma bijection_type [TC]: ``` paulson@13309 ` 1003` ``` "[| x \ nat; y \ nat; z \ nat |] ==> bijection_fm(x,y,z) \ formula" ``` paulson@13309 ` 1004` ```by (simp add: bijection_fm_def) ``` paulson@13309 ` 1005` paulson@13309 ` 1006` ```lemma arity_bijection_fm [simp]: ``` paulson@13309 ` 1007` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13309 ` 1008` ``` ==> arity(bijection_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13309 ` 1009` ```by (simp add: bijection_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13309 ` 1010` paulson@13309 ` 1011` ```lemma sats_bijection_fm [simp]: ``` paulson@13309 ` 1012` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13309 ` 1013` ``` ==> sats(A, bijection_fm(x,y,z), env) <-> ``` paulson@13309 ` 1014` ``` bijection(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13309 ` 1015` ```by (simp add: bijection_fm_def bijection_def) ``` paulson@13309 ` 1016` paulson@13309 ` 1017` ```lemma bijection_iff_sats: ``` paulson@13309 ` 1018` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13309 ` 1019` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13309 ` 1020` ``` ==> bijection(**A, x, y, z) <-> sats(A, bijection_fm(i,j,k), env)" ``` paulson@13309 ` 1021` ```by simp ``` paulson@13309 ` 1022` paulson@13314 ` 1023` ```theorem bijection_reflection: ``` paulson@13314 ` 1024` ``` "REFLECTS[\x. bijection(L,f(x),g(x),h(x)), ``` paulson@13314 ` 1025` ``` \i x. bijection(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13314 ` 1026` ```apply (simp only: bijection_def setclass_simps) ``` paulson@13314 ` 1027` ```apply (intro And_reflection injection_reflection surjection_reflection) ``` paulson@13314 ` 1028` ```done ``` paulson@13309 ` 1029` paulson@13309 ` 1030` paulson@13309 ` 1031` ```subsubsection{*Order-Isomorphisms*} ``` paulson@13309 ` 1032` paulson@13309 ` 1033` ```(* order_isomorphism :: "[i=>o,i,i,i,i,i] => o" ``` paulson@13309 ` 1034` ``` "order_isomorphism(M,A,r,B,s,f) == ``` paulson@13309 ` 1035` ``` bijection(M,A,B,f) & ``` paulson@13309 ` 1036` ``` (\x[M]. x\A --> (\y[M]. y\A --> ``` paulson@13309 ` 1037` ``` (\p[M]. \fx[M]. \fy[M]. \q[M]. ``` paulson@13309 ` 1038` ``` pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) --> ``` paulson@13309 ` 1039` ``` pair(M,fx,fy,q) --> (p\r <-> q\s))))" ``` paulson@13309 ` 1040` ``` *) ``` paulson@13309 ` 1041` paulson@13309 ` 1042` ```constdefs order_isomorphism_fm :: "[i,i,i,i,i]=>i" ``` paulson@13309 ` 1043` ``` "order_isomorphism_fm(A,r,B,s,f) == ``` paulson@13309 ` 1044` ``` And(bijection_fm(A,B,f), ``` paulson@13309 ` 1045` ``` Forall(Implies(Member(0,succ(A)), ``` paulson@13309 ` 1046` ``` Forall(Implies(Member(0,succ(succ(A))), ``` paulson@13309 ` 1047` ``` Forall(Forall(Forall(Forall( ``` paulson@13309 ` 1048` ``` Implies(pair_fm(5,4,3), ``` paulson@13309 ` 1049` ``` Implies(fun_apply_fm(f#+6,5,2), ``` paulson@13309 ` 1050` ``` Implies(fun_apply_fm(f#+6,4,1), ``` paulson@13309 ` 1051` ``` Implies(pair_fm(2,1,0), ``` paulson@13309 ` 1052` ``` Iff(Member(3,r#+6), Member(0,s#+6)))))))))))))))" ``` paulson@13309 ` 1053` paulson@13309 ` 1054` ```lemma order_isomorphism_type [TC]: ``` paulson@13309 ` 1055` ``` "[| A \ nat; r \ nat; B \ nat; s \ nat; f \ nat |] ``` paulson@13309 ` 1056` ``` ==> order_isomorphism_fm(A,r,B,s,f) \ formula" ``` paulson@13309 ` 1057` ```by (simp add: order_isomorphism_fm_def) ``` paulson@13309 ` 1058` paulson@13309 ` 1059` ```lemma arity_order_isomorphism_fm [simp]: ``` paulson@13309 ` 1060` ``` "[| A \ nat; r \ nat; B \ nat; s \ nat; f \ nat |] ``` paulson@13309 ` 1061` ``` ==> arity(order_isomorphism_fm(A,r,B,s,f)) = ``` paulson@13309 ` 1062` ``` succ(A) \ succ(r) \ succ(B) \ succ(s) \ succ(f)" ``` paulson@13309 ` 1063` ```by (simp add: order_isomorphism_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13309 ` 1064` paulson@13309 ` 1065` ```lemma sats_order_isomorphism_fm [simp]: ``` paulson@13309 ` 1066` ``` "[| U \ nat; r \ nat; B \ nat; s \ nat; f \ nat; env \ list(A)|] ``` paulson@13309 ` 1067` ``` ==> sats(A, order_isomorphism_fm(U,r,B,s,f), env) <-> ``` paulson@13309 ` 1068` ``` order_isomorphism(**A, nth(U,env), nth(r,env), nth(B,env), ``` paulson@13309 ` 1069` ``` nth(s,env), nth(f,env))" ``` paulson@13309 ` 1070` ```by (simp add: order_isomorphism_fm_def order_isomorphism_def) ``` paulson@13309 ` 1071` paulson@13309 ` 1072` ```lemma order_isomorphism_iff_sats: ``` paulson@13309 ` 1073` ``` "[| nth(i,env) = U; nth(j,env) = r; nth(k,env) = B; nth(j',env) = s; ``` paulson@13309 ` 1074` ``` nth(k',env) = f; ``` paulson@13309 ` 1075` ``` i \ nat; j \ nat; k \ nat; j' \ nat; k' \ nat; env \ list(A)|] ``` paulson@13309 ` 1076` ``` ==> order_isomorphism(**A,U,r,B,s,f) <-> ``` paulson@13309 ` 1077` ``` sats(A, order_isomorphism_fm(i,j,k,j',k'), env)" ``` paulson@13309 ` 1078` ```by simp ``` paulson@13309 ` 1079` paulson@13314 ` 1080` ```theorem order_isomorphism_reflection: ``` paulson@13314 ` 1081` ``` "REFLECTS[\x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)), ``` paulson@13314 ` 1082` ``` \i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]" ``` paulson@13314 ` 1083` ```apply (simp only: order_isomorphism_def setclass_simps) ``` paulson@13314 ` 1084` ```apply (intro FOL_reflection function_reflection bijection_reflection) ``` paulson@13314 ` 1085` ```done ``` paulson@13309 ` 1086` paulson@13223 ` 1087` ```end ```