src/ZF/Constructible/Separation.thy
 author paulson Wed Jul 31 14:40:40 2002 +0200 (2002-07-31) changeset 13437 01b3fc0cc1b8 parent 13429 2232810416fc child 13440 cdde97e1db1c permissions -rw-r--r--
separate "axioms" proofs: more flexible for locale reasoning
 paulson@13437 ` 1` ```(* Title: ZF/Constructible/Separation.thy ``` paulson@13437 ` 2` ``` ID: \$Id\$ ``` paulson@13437 ` 3` ``` Author: Lawrence C Paulson, Cambridge University Computer Laboratory ``` paulson@13437 ` 4` ``` Copyright 2002 University of Cambridge ``` paulson@13437 ` 5` ```*) ``` paulson@13437 ` 6` paulson@13339 ` 7` ```header{*Early Instances of Separation and Strong Replacement*} ``` paulson@13323 ` 8` paulson@13324 ` 9` ```theory Separation = L_axioms + WF_absolute: ``` paulson@13306 ` 10` paulson@13339 ` 11` ```text{*This theory proves all instances needed for locale @{text "M_axioms"}*} ``` paulson@13339 ` 12` paulson@13306 ` 13` ```text{*Helps us solve for de Bruijn indices!*} ``` paulson@13306 ` 14` ```lemma nth_ConsI: "[|nth(n,l) = x; n \ nat|] ==> nth(succ(n), Cons(a,l)) = x" ``` paulson@13306 ` 15` ```by simp ``` paulson@13306 ` 16` paulson@13316 ` 17` ```lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI ``` wenzelm@13428 ` 18` ```lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats function_iff_sats ``` paulson@13323 ` 19` ``` fun_plus_iff_sats ``` paulson@13306 ` 20` paulson@13306 ` 21` ```lemma Collect_conj_in_DPow: ``` wenzelm@13428 ` 22` ``` "[| {x\A. P(x)} \ DPow(A); {x\A. Q(x)} \ DPow(A) |] ``` paulson@13306 ` 23` ``` ==> {x\A. P(x) & Q(x)} \ DPow(A)" ``` wenzelm@13428 ` 24` ```by (simp add: Int_in_DPow Collect_Int_Collect_eq [symmetric]) ``` paulson@13306 ` 25` paulson@13306 ` 26` ```lemma Collect_conj_in_DPow_Lset: ``` paulson@13306 ` 27` ``` "[|z \ Lset(j); {x \ Lset(j). P(x)} \ DPow(Lset(j))|] ``` paulson@13306 ` 28` ``` ==> {x \ Lset(j). x \ z & P(x)} \ DPow(Lset(j))" ``` paulson@13306 ` 29` ```apply (frule mem_Lset_imp_subset_Lset) ``` wenzelm@13428 ` 30` ```apply (simp add: Collect_conj_in_DPow Collect_mem_eq ``` paulson@13306 ` 31` ``` subset_Int_iff2 elem_subset_in_DPow) ``` paulson@13306 ` 32` ```done ``` paulson@13306 ` 33` paulson@13306 ` 34` ```lemma separation_CollectI: ``` paulson@13306 ` 35` ``` "(\z. L(z) ==> L({x \ z . P(x)})) ==> separation(L, \x. P(x))" ``` wenzelm@13428 ` 36` ```apply (unfold separation_def, clarify) ``` wenzelm@13428 ` 37` ```apply (rule_tac x="{x\z. P(x)}" in rexI) ``` paulson@13306 ` 38` ```apply simp_all ``` paulson@13306 ` 39` ```done ``` paulson@13306 ` 40` paulson@13306 ` 41` ```text{*Reduces the original comprehension to the reflected one*} ``` paulson@13306 ` 42` ```lemma reflection_imp_L_separation: ``` paulson@13306 ` 43` ``` "[| \x\Lset(j). P(x) <-> Q(x); ``` wenzelm@13428 ` 44` ``` {x \ Lset(j) . Q(x)} \ DPow(Lset(j)); ``` paulson@13306 ` 45` ``` Ord(j); z \ Lset(j)|] ==> L({x \ z . P(x)})" ``` paulson@13306 ` 46` ```apply (rule_tac i = "succ(j)" in L_I) ``` paulson@13306 ` 47` ``` prefer 2 apply simp ``` paulson@13306 ` 48` ```apply (subgoal_tac "{x \ z. P(x)} = {x \ Lset(j). x \ z & (Q(x))}") ``` paulson@13306 ` 49` ``` prefer 2 ``` wenzelm@13428 ` 50` ``` apply (blast dest: mem_Lset_imp_subset_Lset) ``` paulson@13306 ` 51` ```apply (simp add: Lset_succ Collect_conj_in_DPow_Lset) ``` paulson@13306 ` 52` ```done ``` paulson@13306 ` 53` paulson@13306 ` 54` paulson@13316 ` 55` ```subsection{*Separation for Intersection*} ``` paulson@13306 ` 56` paulson@13306 ` 57` ```lemma Inter_Reflects: ``` wenzelm@13428 ` 58` ``` "REFLECTS[\x. \y[L]. y\A --> x \ y, ``` paulson@13314 ` 59` ``` \i x. \y\Lset(i). y\A --> x \ y]" ``` wenzelm@13428 ` 60` ```by (intro FOL_reflections) ``` paulson@13306 ` 61` paulson@13306 ` 62` ```lemma Inter_separation: ``` paulson@13306 ` 63` ``` "L(A) ==> separation(L, \x. \y[L]. y\A --> x\y)" ``` wenzelm@13428 ` 64` ```apply (rule separation_CollectI) ``` wenzelm@13428 ` 65` ```apply (rule_tac A="{A,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 66` ```apply (rule ReflectsE [OF Inter_Reflects], assumption) ``` wenzelm@13428 ` 67` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 68` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 69` ``` apply (simp_all add: lt_Ord2, clarify) ``` wenzelm@13428 ` 70` ```apply (rule DPow_LsetI) ``` wenzelm@13428 ` 71` ```apply (rule ball_iff_sats) ``` paulson@13306 ` 72` ```apply (rule imp_iff_sats) ``` paulson@13306 ` 73` ```apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats) ``` paulson@13306 ` 74` ```apply (rule_tac i=0 and j=2 in mem_iff_sats) ``` paulson@13306 ` 75` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13306 ` 76` ```done ``` paulson@13306 ` 77` paulson@13437 ` 78` ```subsection{*Separation for Set Difference*} ``` paulson@13437 ` 79` paulson@13437 ` 80` ```lemma Diff_Reflects: ``` paulson@13437 ` 81` ``` "REFLECTS[\x. x \ B, \i x. x \ B]" ``` paulson@13437 ` 82` ```by (intro FOL_reflections) ``` paulson@13437 ` 83` paulson@13437 ` 84` ```lemma Diff_separation: ``` paulson@13437 ` 85` ``` "L(B) ==> separation(L, \x. x \ B)" ``` paulson@13437 ` 86` ```apply (rule separation_CollectI) ``` paulson@13437 ` 87` ```apply (rule_tac A="{B,z}" in subset_LsetE, blast ) ``` paulson@13437 ` 88` ```apply (rule ReflectsE [OF Diff_Reflects], assumption) ``` paulson@13437 ` 89` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13437 ` 90` ```apply (erule reflection_imp_L_separation) ``` paulson@13437 ` 91` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13437 ` 92` ```apply (rule DPow_LsetI) ``` paulson@13437 ` 93` ```apply (rule not_iff_sats) ``` paulson@13437 ` 94` ```apply (rule_tac env="[x,B]" in mem_iff_sats) ``` paulson@13437 ` 95` ```apply (rule sep_rules | simp)+ ``` paulson@13437 ` 96` ```done ``` paulson@13437 ` 97` paulson@13316 ` 98` ```subsection{*Separation for Cartesian Product*} ``` paulson@13306 ` 99` paulson@13323 ` 100` ```lemma cartprod_Reflects: ``` paulson@13314 ` 101` ``` "REFLECTS[\z. \x[L]. x\A & (\y[L]. y\B & pair(L,x,y,z)), ``` wenzelm@13428 ` 102` ``` \i z. \x\Lset(i). x\A & (\y\Lset(i). y\B & ``` paulson@13314 ` 103` ``` pair(**Lset(i),x,y,z))]" ``` paulson@13323 ` 104` ```by (intro FOL_reflections function_reflections) ``` paulson@13306 ` 105` paulson@13306 ` 106` ```lemma cartprod_separation: ``` wenzelm@13428 ` 107` ``` "[| L(A); L(B) |] ``` paulson@13306 ` 108` ``` ==> separation(L, \z. \x[L]. x\A & (\y[L]. y\B & pair(L,x,y,z)))" ``` wenzelm@13428 ` 109` ```apply (rule separation_CollectI) ``` wenzelm@13428 ` 110` ```apply (rule_tac A="{A,B,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 111` ```apply (rule ReflectsE [OF cartprod_Reflects], assumption) ``` wenzelm@13428 ` 112` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 113` ```apply (erule reflection_imp_L_separation) ``` wenzelm@13428 ` 114` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13385 ` 115` ```apply (rule DPow_LsetI) ``` wenzelm@13428 ` 116` ```apply (rename_tac u) ``` wenzelm@13428 ` 117` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 118` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 119` ```apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all) ``` paulson@13316 ` 120` ```apply (rule sep_rules | simp)+ ``` paulson@13306 ` 121` ```done ``` paulson@13306 ` 122` paulson@13316 ` 123` ```subsection{*Separation for Image*} ``` paulson@13306 ` 124` paulson@13306 ` 125` ```lemma image_Reflects: ``` paulson@13314 ` 126` ``` "REFLECTS[\y. \p[L]. p\r & (\x[L]. x\A & pair(L,x,y,p)), ``` paulson@13314 ` 127` ``` \i y. \p\Lset(i). p\r & (\x\Lset(i). x\A & pair(**Lset(i),x,y,p))]" ``` paulson@13323 ` 128` ```by (intro FOL_reflections function_reflections) ``` paulson@13306 ` 129` paulson@13306 ` 130` ```lemma image_separation: ``` wenzelm@13428 ` 131` ``` "[| L(A); L(r) |] ``` paulson@13306 ` 132` ``` ==> separation(L, \y. \p[L]. p\r & (\x[L]. x\A & pair(L,x,y,p)))" ``` wenzelm@13428 ` 133` ```apply (rule separation_CollectI) ``` wenzelm@13428 ` 134` ```apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 135` ```apply (rule ReflectsE [OF image_Reflects], assumption) ``` wenzelm@13428 ` 136` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 137` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 138` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13385 ` 139` ```apply (rule DPow_LsetI) ``` wenzelm@13428 ` 140` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 141` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 142` ```apply (rule_tac env="[p,y,A,r]" in mem_iff_sats) ``` paulson@13316 ` 143` ```apply (rule sep_rules | simp)+ ``` paulson@13306 ` 144` ```done ``` paulson@13306 ` 145` paulson@13306 ` 146` paulson@13316 ` 147` ```subsection{*Separation for Converse*} ``` paulson@13306 ` 148` paulson@13306 ` 149` ```lemma converse_Reflects: ``` paulson@13314 ` 150` ``` "REFLECTS[\z. \p[L]. p\r & (\x[L]. \y[L]. pair(L,x,y,p) & pair(L,y,x,z)), ``` wenzelm@13428 ` 151` ``` \i z. \p\Lset(i). p\r & (\x\Lset(i). \y\Lset(i). ``` paulson@13314 ` 152` ``` pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z))]" ``` paulson@13323 ` 153` ```by (intro FOL_reflections function_reflections) ``` paulson@13306 ` 154` paulson@13306 ` 155` ```lemma converse_separation: ``` wenzelm@13428 ` 156` ``` "L(r) ==> separation(L, ``` paulson@13306 ` 157` ``` \z. \p[L]. p\r & (\x[L]. \y[L]. pair(L,x,y,p) & pair(L,y,x,z)))" ``` wenzelm@13428 ` 158` ```apply (rule separation_CollectI) ``` wenzelm@13428 ` 159` ```apply (rule_tac A="{r,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 160` ```apply (rule ReflectsE [OF converse_Reflects], assumption) ``` wenzelm@13428 ` 161` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 162` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 163` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13385 ` 164` ```apply (rule DPow_LsetI) ``` wenzelm@13428 ` 165` ```apply (rename_tac u) ``` wenzelm@13428 ` 166` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 167` ```apply (rule conj_iff_sats) ``` paulson@13339 ` 168` ```apply (rule_tac i=0 and j=2 and env="[p,u,r]" in mem_iff_sats, simp_all) ``` paulson@13316 ` 169` ```apply (rule sep_rules | simp)+ ``` paulson@13306 ` 170` ```done ``` paulson@13306 ` 171` paulson@13306 ` 172` paulson@13316 ` 173` ```subsection{*Separation for Restriction*} ``` paulson@13306 ` 174` paulson@13306 ` 175` ```lemma restrict_Reflects: ``` paulson@13314 ` 176` ``` "REFLECTS[\z. \x[L]. x\A & (\y[L]. pair(L,x,y,z)), ``` paulson@13314 ` 177` ``` \i z. \x\Lset(i). x\A & (\y\Lset(i). pair(**Lset(i),x,y,z))]" ``` paulson@13323 ` 178` ```by (intro FOL_reflections function_reflections) ``` paulson@13306 ` 179` paulson@13306 ` 180` ```lemma restrict_separation: ``` paulson@13306 ` 181` ``` "L(A) ==> separation(L, \z. \x[L]. x\A & (\y[L]. pair(L,x,y,z)))" ``` wenzelm@13428 ` 182` ```apply (rule separation_CollectI) ``` wenzelm@13428 ` 183` ```apply (rule_tac A="{A,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 184` ```apply (rule ReflectsE [OF restrict_Reflects], assumption) ``` wenzelm@13428 ` 185` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 186` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 187` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13385 ` 188` ```apply (rule DPow_LsetI) ``` wenzelm@13428 ` 189` ```apply (rename_tac u) ``` wenzelm@13428 ` 190` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 191` ```apply (rule conj_iff_sats) ``` paulson@13339 ` 192` ```apply (rule_tac i=0 and j=2 and env="[x,u,A]" in mem_iff_sats, simp_all) ``` paulson@13316 ` 193` ```apply (rule sep_rules | simp)+ ``` paulson@13306 ` 194` ```done ``` paulson@13306 ` 195` paulson@13306 ` 196` paulson@13316 ` 197` ```subsection{*Separation for Composition*} ``` paulson@13306 ` 198` paulson@13306 ` 199` ```lemma comp_Reflects: ``` wenzelm@13428 ` 200` ``` "REFLECTS[\xz. \x[L]. \y[L]. \z[L]. \xy[L]. \yz[L]. ``` wenzelm@13428 ` 201` ``` pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & ``` paulson@13306 ` 202` ``` xy\s & yz\r, ``` wenzelm@13428 ` 203` ``` \i xz. \x\Lset(i). \y\Lset(i). \z\Lset(i). \xy\Lset(i). \yz\Lset(i). ``` wenzelm@13428 ` 204` ``` pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) & ``` paulson@13314 ` 205` ``` pair(**Lset(i),y,z,yz) & xy\s & yz\r]" ``` paulson@13323 ` 206` ```by (intro FOL_reflections function_reflections) ``` paulson@13306 ` 207` paulson@13306 ` 208` ```lemma comp_separation: ``` paulson@13306 ` 209` ``` "[| L(r); L(s) |] ``` wenzelm@13428 ` 210` ``` ==> separation(L, \xz. \x[L]. \y[L]. \z[L]. \xy[L]. \yz[L]. ``` wenzelm@13428 ` 211` ``` pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & ``` paulson@13306 ` 212` ``` xy\s & yz\r)" ``` wenzelm@13428 ` 213` ```apply (rule separation_CollectI) ``` wenzelm@13428 ` 214` ```apply (rule_tac A="{r,s,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 215` ```apply (rule ReflectsE [OF comp_Reflects], assumption) ``` wenzelm@13428 ` 216` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 217` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 218` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13385 ` 219` ```apply (rule DPow_LsetI) ``` wenzelm@13428 ` 220` ```apply (rename_tac u) ``` paulson@13306 ` 221` ```apply (rule bex_iff_sats)+ ``` wenzelm@13428 ` 222` ```apply (rename_tac x y z) ``` paulson@13306 ` 223` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 224` ```apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats) ``` paulson@13316 ` 225` ```apply (rule sep_rules | simp)+ ``` paulson@13306 ` 226` ```done ``` paulson@13306 ` 227` paulson@13316 ` 228` ```subsection{*Separation for Predecessors in an Order*} ``` paulson@13306 ` 229` paulson@13306 ` 230` ```lemma pred_Reflects: ``` paulson@13314 ` 231` ``` "REFLECTS[\y. \p[L]. p\r & pair(L,y,x,p), ``` paulson@13314 ` 232` ``` \i y. \p \ Lset(i). p\r & pair(**Lset(i),y,x,p)]" ``` paulson@13323 ` 233` ```by (intro FOL_reflections function_reflections) ``` paulson@13306 ` 234` paulson@13306 ` 235` ```lemma pred_separation: ``` paulson@13306 ` 236` ``` "[| L(r); L(x) |] ==> separation(L, \y. \p[L]. p\r & pair(L,y,x,p))" ``` wenzelm@13428 ` 237` ```apply (rule separation_CollectI) ``` wenzelm@13428 ` 238` ```apply (rule_tac A="{r,x,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 239` ```apply (rule ReflectsE [OF pred_Reflects], assumption) ``` wenzelm@13428 ` 240` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 241` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 242` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13385 ` 243` ```apply (rule DPow_LsetI) ``` wenzelm@13428 ` 244` ```apply (rename_tac u) ``` paulson@13306 ` 245` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 246` ```apply (rule conj_iff_sats) ``` wenzelm@13428 ` 247` ```apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats) ``` paulson@13316 ` 248` ```apply (rule sep_rules | simp)+ ``` paulson@13306 ` 249` ```done ``` paulson@13306 ` 250` paulson@13306 ` 251` paulson@13316 ` 252` ```subsection{*Separation for the Membership Relation*} ``` paulson@13306 ` 253` paulson@13306 ` 254` ```lemma Memrel_Reflects: ``` paulson@13314 ` 255` ``` "REFLECTS[\z. \x[L]. \y[L]. pair(L,x,y,z) & x \ y, ``` paulson@13314 ` 256` ``` \i z. \x \ Lset(i). \y \ Lset(i). pair(**Lset(i),x,y,z) & x \ y]" ``` paulson@13323 ` 257` ```by (intro FOL_reflections function_reflections) ``` paulson@13306 ` 258` paulson@13306 ` 259` ```lemma Memrel_separation: ``` paulson@13306 ` 260` ``` "separation(L, \z. \x[L]. \y[L]. pair(L,x,y,z) & x \ y)" ``` wenzelm@13428 ` 261` ```apply (rule separation_CollectI) ``` wenzelm@13428 ` 262` ```apply (rule_tac A="{z}" in subset_LsetE, blast ) ``` paulson@13306 ` 263` ```apply (rule ReflectsE [OF Memrel_Reflects], assumption) ``` wenzelm@13428 ` 264` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 265` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 266` ``` apply (simp_all add: lt_Ord2) ``` paulson@13385 ` 267` ```apply (rule DPow_LsetI) ``` wenzelm@13428 ` 268` ```apply (rename_tac u) ``` paulson@13316 ` 269` ```apply (rule bex_iff_sats conj_iff_sats)+ ``` wenzelm@13428 ` 270` ```apply (rule_tac env = "[y,x,u]" in pair_iff_sats) ``` paulson@13316 ` 271` ```apply (rule sep_rules | simp)+ ``` paulson@13306 ` 272` ```done ``` paulson@13306 ` 273` paulson@13306 ` 274` paulson@13316 ` 275` ```subsection{*Replacement for FunSpace*} ``` wenzelm@13428 ` 276` paulson@13306 ` 277` ```lemma funspace_succ_Reflects: ``` wenzelm@13428 ` 278` ``` "REFLECTS[\z. \p[L]. p\A & (\f[L]. \b[L]. \nb[L]. \cnbf[L]. ``` wenzelm@13428 ` 279` ``` pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) & ``` wenzelm@13428 ` 280` ``` upair(L,cnbf,cnbf,z)), ``` wenzelm@13428 ` 281` ``` \i z. \p \ Lset(i). p\A & (\f \ Lset(i). \b \ Lset(i). ``` wenzelm@13428 ` 282` ``` \nb \ Lset(i). \cnbf \ Lset(i). ``` wenzelm@13428 ` 283` ``` pair(**Lset(i),f,b,p) & pair(**Lset(i),n,b,nb) & ``` wenzelm@13428 ` 284` ``` is_cons(**Lset(i),nb,f,cnbf) & upair(**Lset(i),cnbf,cnbf,z))]" ``` paulson@13323 ` 285` ```by (intro FOL_reflections function_reflections) ``` paulson@13306 ` 286` paulson@13306 ` 287` ```lemma funspace_succ_replacement: ``` wenzelm@13428 ` 288` ``` "L(n) ==> ``` wenzelm@13428 ` 289` ``` strong_replacement(L, \p z. \f[L]. \b[L]. \nb[L]. \cnbf[L]. ``` paulson@13306 ` 290` ``` pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) & ``` paulson@13306 ` 291` ``` upair(L,cnbf,cnbf,z))" ``` wenzelm@13428 ` 292` ```apply (rule strong_replacementI) ``` wenzelm@13428 ` 293` ```apply (rule rallI) ``` wenzelm@13428 ` 294` ```apply (rule separation_CollectI) ``` wenzelm@13428 ` 295` ```apply (rule_tac A="{n,A,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 296` ```apply (rule ReflectsE [OF funspace_succ_Reflects], assumption) ``` wenzelm@13428 ` 297` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 298` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 299` ``` apply (simp_all add: lt_Ord2) ``` paulson@13385 ` 300` ```apply (rule DPow_LsetI) ``` wenzelm@13428 ` 301` ```apply (rename_tac u) ``` paulson@13306 ` 302` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 303` ```apply (rule conj_iff_sats) ``` wenzelm@13428 ` 304` ```apply (rule_tac env = "[p,u,n,A]" in mem_iff_sats) ``` paulson@13316 ` 305` ```apply (rule sep_rules | simp)+ ``` paulson@13306 ` 306` ```done ``` paulson@13306 ` 307` paulson@13306 ` 308` paulson@13316 ` 309` ```subsection{*Separation for Order-Isomorphisms*} ``` paulson@13306 ` 310` paulson@13306 ` 311` ```lemma well_ord_iso_Reflects: ``` wenzelm@13428 ` 312` ``` "REFLECTS[\x. x\A --> ``` paulson@13314 ` 313` ``` (\y[L]. \p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \ r), ``` wenzelm@13428 ` 314` ``` \i x. x\A --> (\y \ Lset(i). \p \ Lset(i). ``` paulson@13314 ` 315` ``` fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \ r)]" ``` paulson@13323 ` 316` ```by (intro FOL_reflections function_reflections) ``` paulson@13306 ` 317` paulson@13306 ` 318` ```lemma well_ord_iso_separation: ``` wenzelm@13428 ` 319` ``` "[| L(A); L(f); L(r) |] ``` wenzelm@13428 ` 320` ``` ==> separation (L, \x. x\A --> (\y[L]. (\p[L]. ``` wenzelm@13428 ` 321` ``` fun_apply(L,f,x,y) & pair(L,y,x,p) & p \ r)))" ``` wenzelm@13428 ` 322` ```apply (rule separation_CollectI) ``` wenzelm@13428 ` 323` ```apply (rule_tac A="{A,f,r,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 324` ```apply (rule ReflectsE [OF well_ord_iso_Reflects], assumption) ``` wenzelm@13428 ` 325` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 326` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 327` ``` apply (simp_all add: lt_Ord2) ``` paulson@13385 ` 328` ```apply (rule DPow_LsetI) ``` wenzelm@13428 ` 329` ```apply (rename_tac u) ``` paulson@13306 ` 330` ```apply (rule imp_iff_sats) ``` wenzelm@13428 ` 331` ```apply (rule_tac env = "[u,A,f,r]" in mem_iff_sats) ``` paulson@13316 ` 332` ```apply (rule sep_rules | simp)+ ``` paulson@13316 ` 333` ```done ``` paulson@13316 ` 334` paulson@13316 ` 335` paulson@13316 ` 336` ```subsection{*Separation for @{term "obase"}*} ``` paulson@13316 ` 337` paulson@13316 ` 338` ```lemma obase_reflects: ``` wenzelm@13428 ` 339` ``` "REFLECTS[\a. \x[L]. \g[L]. \mx[L]. \par[L]. ``` wenzelm@13428 ` 340` ``` ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) & ``` wenzelm@13428 ` 341` ``` order_isomorphism(L,par,r,x,mx,g), ``` wenzelm@13428 ` 342` ``` \i a. \x \ Lset(i). \g \ Lset(i). \mx \ Lset(i). \par \ Lset(i). ``` wenzelm@13428 ` 343` ``` ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) & ``` wenzelm@13428 ` 344` ``` order_isomorphism(**Lset(i),par,r,x,mx,g)]" ``` paulson@13323 ` 345` ```by (intro FOL_reflections function_reflections fun_plus_reflections) ``` paulson@13316 ` 346` paulson@13316 ` 347` ```lemma obase_separation: ``` paulson@13316 ` 348` ``` --{*part of the order type formalization*} ``` wenzelm@13428 ` 349` ``` "[| L(A); L(r) |] ``` wenzelm@13428 ` 350` ``` ==> separation(L, \a. \x[L]. \g[L]. \mx[L]. \par[L]. ``` wenzelm@13428 ` 351` ``` ordinal(L,x) & membership(L,x,mx) & pred_set(L,A,a,r,par) & ``` wenzelm@13428 ` 352` ``` order_isomorphism(L,par,r,x,mx,g))" ``` wenzelm@13428 ` 353` ```apply (rule separation_CollectI) ``` wenzelm@13428 ` 354` ```apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) ``` paulson@13316 ` 355` ```apply (rule ReflectsE [OF obase_reflects], assumption) ``` wenzelm@13428 ` 356` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13316 ` 357` ```apply (erule reflection_imp_L_separation) ``` paulson@13316 ` 358` ``` apply (simp_all add: lt_Ord2) ``` paulson@13385 ` 359` ```apply (rule DPow_LsetI) ``` wenzelm@13428 ` 360` ```apply (rename_tac u) ``` paulson@13306 ` 361` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 362` ```apply (rule conj_iff_sats) ``` wenzelm@13428 ` 363` ```apply (rule_tac env = "[x,u,A,r]" in ordinal_iff_sats) ``` paulson@13316 ` 364` ```apply (rule sep_rules | simp)+ ``` paulson@13316 ` 365` ```done ``` paulson@13316 ` 366` paulson@13316 ` 367` paulson@13319 ` 368` ```subsection{*Separation for a Theorem about @{term "obase"}*} ``` paulson@13316 ` 369` paulson@13316 ` 370` ```lemma obase_equals_reflects: ``` wenzelm@13428 ` 371` ``` "REFLECTS[\x. x\A --> ~(\y[L]. \g[L]. ``` wenzelm@13428 ` 372` ``` ordinal(L,y) & (\my[L]. \pxr[L]. ``` wenzelm@13428 ` 373` ``` membership(L,y,my) & pred_set(L,A,x,r,pxr) & ``` wenzelm@13428 ` 374` ``` order_isomorphism(L,pxr,r,y,my,g))), ``` wenzelm@13428 ` 375` ``` \i x. x\A --> ~(\y \ Lset(i). \g \ Lset(i). ``` wenzelm@13428 ` 376` ``` ordinal(**Lset(i),y) & (\my \ Lset(i). \pxr \ Lset(i). ``` wenzelm@13428 ` 377` ``` membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) & ``` wenzelm@13428 ` 378` ``` order_isomorphism(**Lset(i),pxr,r,y,my,g)))]" ``` paulson@13323 ` 379` ```by (intro FOL_reflections function_reflections fun_plus_reflections) ``` paulson@13316 ` 380` paulson@13316 ` 381` paulson@13316 ` 382` ```lemma obase_equals_separation: ``` wenzelm@13428 ` 383` ``` "[| L(A); L(r) |] ``` wenzelm@13428 ` 384` ``` ==> separation (L, \x. x\A --> ~(\y[L]. \g[L]. ``` wenzelm@13428 ` 385` ``` ordinal(L,y) & (\my[L]. \pxr[L]. ``` wenzelm@13428 ` 386` ``` membership(L,y,my) & pred_set(L,A,x,r,pxr) & ``` wenzelm@13428 ` 387` ``` order_isomorphism(L,pxr,r,y,my,g))))" ``` wenzelm@13428 ` 388` ```apply (rule separation_CollectI) ``` wenzelm@13428 ` 389` ```apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) ``` paulson@13316 ` 390` ```apply (rule ReflectsE [OF obase_equals_reflects], assumption) ``` wenzelm@13428 ` 391` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13316 ` 392` ```apply (erule reflection_imp_L_separation) ``` paulson@13316 ` 393` ``` apply (simp_all add: lt_Ord2) ``` paulson@13385 ` 394` ```apply (rule DPow_LsetI) ``` wenzelm@13428 ` 395` ```apply (rename_tac u) ``` paulson@13316 ` 396` ```apply (rule imp_iff_sats ball_iff_sats disj_iff_sats not_iff_sats)+ ``` wenzelm@13428 ` 397` ```apply (rule_tac env = "[u,A,r]" in mem_iff_sats) ``` paulson@13316 ` 398` ```apply (rule sep_rules | simp)+ ``` paulson@13316 ` 399` ```done ``` paulson@13316 ` 400` paulson@13316 ` 401` paulson@13316 ` 402` ```subsection{*Replacement for @{term "omap"}*} ``` paulson@13316 ` 403` paulson@13316 ` 404` ```lemma omap_reflects: ``` wenzelm@13428 ` 405` ``` "REFLECTS[\z. \a[L]. a\B & (\x[L]. \g[L]. \mx[L]. \par[L]. ``` wenzelm@13428 ` 406` ``` ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & ``` paulson@13316 ` 407` ``` pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g)), ``` wenzelm@13428 ` 408` ``` \i z. \a \ Lset(i). a\B & (\x \ Lset(i). \g \ Lset(i). \mx \ Lset(i). ``` wenzelm@13428 ` 409` ``` \par \ Lset(i). ``` wenzelm@13428 ` 410` ``` ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) & ``` wenzelm@13428 ` 411` ``` membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) & ``` paulson@13316 ` 412` ``` order_isomorphism(**Lset(i),par,r,x,mx,g))]" ``` paulson@13323 ` 413` ```by (intro FOL_reflections function_reflections fun_plus_reflections) ``` paulson@13316 ` 414` paulson@13316 ` 415` ```lemma omap_replacement: ``` wenzelm@13428 ` 416` ``` "[| L(A); L(r) |] ``` paulson@13316 ` 417` ``` ==> strong_replacement(L, ``` wenzelm@13428 ` 418` ``` \a z. \x[L]. \g[L]. \mx[L]. \par[L]. ``` wenzelm@13428 ` 419` ``` ordinal(L,x) & pair(L,a,x,z) & membership(L,x,mx) & ``` wenzelm@13428 ` 420` ``` pred_set(L,A,a,r,par) & order_isomorphism(L,par,r,x,mx,g))" ``` wenzelm@13428 ` 421` ```apply (rule strong_replacementI) ``` paulson@13316 ` 422` ```apply (rule rallI) ``` wenzelm@13428 ` 423` ```apply (rename_tac B) ``` wenzelm@13428 ` 424` ```apply (rule separation_CollectI) ``` wenzelm@13428 ` 425` ```apply (rule_tac A="{A,B,r,z}" in subset_LsetE, blast ) ``` paulson@13316 ` 426` ```apply (rule ReflectsE [OF omap_reflects], assumption) ``` wenzelm@13428 ` 427` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13316 ` 428` ```apply (erule reflection_imp_L_separation) ``` paulson@13316 ` 429` ``` apply (simp_all add: lt_Ord2) ``` paulson@13385 ` 430` ```apply (rule DPow_LsetI) ``` wenzelm@13428 ` 431` ```apply (rename_tac u) ``` paulson@13316 ` 432` ```apply (rule bex_iff_sats conj_iff_sats)+ ``` wenzelm@13428 ` 433` ```apply (rule_tac env = "[a,u,A,B,r]" in mem_iff_sats) ``` paulson@13316 ` 434` ```apply (rule sep_rules | simp)+ ``` paulson@13306 ` 435` ```done ``` paulson@13306 ` 436` paulson@13323 ` 437` paulson@13323 ` 438` ```subsection{*Separation for a Theorem about @{term "obase"}*} ``` paulson@13323 ` 439` paulson@13323 ` 440` ```lemma is_recfun_reflects: ``` wenzelm@13428 ` 441` ``` "REFLECTS[\x. \xa[L]. \xb[L]. ``` wenzelm@13428 ` 442` ``` pair(L,x,a,xa) & xa \ r & pair(L,x,b,xb) & xb \ r & ``` wenzelm@13428 ` 443` ``` (\fx[L]. \gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & ``` paulson@13323 ` 444` ``` fx \ gx), ``` wenzelm@13428 ` 445` ``` \i x. \xa \ Lset(i). \xb \ Lset(i). ``` paulson@13323 ` 446` ``` pair(**Lset(i),x,a,xa) & xa \ r & pair(**Lset(i),x,b,xb) & xb \ r & ``` wenzelm@13428 ` 447` ``` (\fx \ Lset(i). \gx \ Lset(i). fun_apply(**Lset(i),f,x,fx) & ``` paulson@13323 ` 448` ``` fun_apply(**Lset(i),g,x,gx) & fx \ gx)]" ``` paulson@13323 ` 449` ```by (intro FOL_reflections function_reflections fun_plus_reflections) ``` paulson@13323 ` 450` paulson@13323 ` 451` ```lemma is_recfun_separation: ``` paulson@13323 ` 452` ``` --{*for well-founded recursion*} ``` wenzelm@13428 ` 453` ``` "[| L(r); L(f); L(g); L(a); L(b) |] ``` wenzelm@13428 ` 454` ``` ==> separation(L, ``` wenzelm@13428 ` 455` ``` \x. \xa[L]. \xb[L]. ``` wenzelm@13428 ` 456` ``` pair(L,x,a,xa) & xa \ r & pair(L,x,b,xb) & xb \ r & ``` wenzelm@13428 ` 457` ``` (\fx[L]. \gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & ``` paulson@13323 ` 458` ``` fx \ gx))" ``` wenzelm@13428 ` 459` ```apply (rule separation_CollectI) ``` wenzelm@13428 ` 460` ```apply (rule_tac A="{r,f,g,a,b,z}" in subset_LsetE, blast ) ``` paulson@13323 ` 461` ```apply (rule ReflectsE [OF is_recfun_reflects], assumption) ``` wenzelm@13428 ` 462` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13323 ` 463` ```apply (erule reflection_imp_L_separation) ``` paulson@13323 ` 464` ``` apply (simp_all add: lt_Ord2) ``` paulson@13385 ` 465` ```apply (rule DPow_LsetI) ``` wenzelm@13428 ` 466` ```apply (rename_tac u) ``` paulson@13323 ` 467` ```apply (rule bex_iff_sats conj_iff_sats)+ ``` wenzelm@13428 ` 468` ```apply (rule_tac env = "[xa,u,r,f,g,a,b]" in pair_iff_sats) ``` paulson@13323 ` 469` ```apply (rule sep_rules | simp)+ ``` paulson@13323 ` 470` ```done ``` paulson@13323 ` 471` paulson@13323 ` 472` paulson@13363 ` 473` ```subsection{*Instantiating the locale @{text M_axioms}*} ``` paulson@13363 ` 474` ```text{*Separation (and Strong Replacement) for basic set-theoretic constructions ``` paulson@13363 ` 475` ```such as intersection, Cartesian Product and image.*} ``` paulson@13363 ` 476` paulson@13437 ` 477` ```lemma M_axioms_axioms_L: "M_axioms_axioms(L)" ``` wenzelm@13428 ` 478` ``` apply (rule M_axioms_axioms.intro) ``` paulson@13437 ` 479` ``` apply (assumption | rule ``` paulson@13437 ` 480` ``` Inter_separation Diff_separation cartprod_separation image_separation ``` paulson@13437 ` 481` ``` converse_separation restrict_separation ``` paulson@13437 ` 482` ``` comp_separation pred_separation Memrel_separation ``` paulson@13437 ` 483` ``` funspace_succ_replacement well_ord_iso_separation ``` paulson@13437 ` 484` ``` obase_separation obase_equals_separation ``` paulson@13437 ` 485` ``` omap_replacement is_recfun_separation)+ ``` wenzelm@13428 ` 486` ``` done ``` paulson@13323 ` 487` paulson@13437 ` 488` ```theorem M_axioms_L: "PROP M_axioms(L)" ``` paulson@13437 ` 489` ```by (rule M_axioms.intro [OF M_triv_axioms_L M_axioms_axioms_L]) ``` paulson@13437 ` 490` paulson@13437 ` 491` wenzelm@13428 ` 492` ```lemmas cartprod_iff = M_axioms.cartprod_iff [OF M_axioms_L] ``` wenzelm@13428 ` 493` ``` and cartprod_closed = M_axioms.cartprod_closed [OF M_axioms_L] ``` wenzelm@13428 ` 494` ``` and sum_closed = M_axioms.sum_closed [OF M_axioms_L] ``` wenzelm@13428 ` 495` ``` and M_converse_iff = M_axioms.M_converse_iff [OF M_axioms_L] ``` wenzelm@13428 ` 496` ``` and converse_closed = M_axioms.converse_closed [OF M_axioms_L] ``` wenzelm@13428 ` 497` ``` and converse_abs = M_axioms.converse_abs [OF M_axioms_L] ``` wenzelm@13428 ` 498` ``` and image_closed = M_axioms.image_closed [OF M_axioms_L] ``` wenzelm@13428 ` 499` ``` and vimage_abs = M_axioms.vimage_abs [OF M_axioms_L] ``` wenzelm@13428 ` 500` ``` and vimage_closed = M_axioms.vimage_closed [OF M_axioms_L] ``` wenzelm@13428 ` 501` ``` and domain_abs = M_axioms.domain_abs [OF M_axioms_L] ``` wenzelm@13428 ` 502` ``` and domain_closed = M_axioms.domain_closed [OF M_axioms_L] ``` wenzelm@13428 ` 503` ``` and range_abs = M_axioms.range_abs [OF M_axioms_L] ``` wenzelm@13428 ` 504` ``` and range_closed = M_axioms.range_closed [OF M_axioms_L] ``` wenzelm@13428 ` 505` ``` and field_abs = M_axioms.field_abs [OF M_axioms_L] ``` wenzelm@13428 ` 506` ``` and field_closed = M_axioms.field_closed [OF M_axioms_L] ``` wenzelm@13428 ` 507` ``` and relation_abs = M_axioms.relation_abs [OF M_axioms_L] ``` wenzelm@13428 ` 508` ``` and function_abs = M_axioms.function_abs [OF M_axioms_L] ``` wenzelm@13428 ` 509` ``` and apply_closed = M_axioms.apply_closed [OF M_axioms_L] ``` wenzelm@13428 ` 510` ``` and apply_abs = M_axioms.apply_abs [OF M_axioms_L] ``` wenzelm@13428 ` 511` ``` and typed_function_abs = M_axioms.typed_function_abs [OF M_axioms_L] ``` wenzelm@13428 ` 512` ``` and injection_abs = M_axioms.injection_abs [OF M_axioms_L] ``` wenzelm@13428 ` 513` ``` and surjection_abs = M_axioms.surjection_abs [OF M_axioms_L] ``` wenzelm@13428 ` 514` ``` and bijection_abs = M_axioms.bijection_abs [OF M_axioms_L] ``` wenzelm@13428 ` 515` ``` and M_comp_iff = M_axioms.M_comp_iff [OF M_axioms_L] ``` wenzelm@13428 ` 516` ``` and comp_closed = M_axioms.comp_closed [OF M_axioms_L] ``` wenzelm@13428 ` 517` ``` and composition_abs = M_axioms.composition_abs [OF M_axioms_L] ``` wenzelm@13428 ` 518` ``` and restriction_is_function = M_axioms.restriction_is_function [OF M_axioms_L] ``` wenzelm@13428 ` 519` ``` and restriction_abs = M_axioms.restriction_abs [OF M_axioms_L] ``` wenzelm@13428 ` 520` ``` and M_restrict_iff = M_axioms.M_restrict_iff [OF M_axioms_L] ``` wenzelm@13428 ` 521` ``` and restrict_closed = M_axioms.restrict_closed [OF M_axioms_L] ``` wenzelm@13428 ` 522` ``` and Inter_abs = M_axioms.Inter_abs [OF M_axioms_L] ``` wenzelm@13428 ` 523` ``` and Inter_closed = M_axioms.Inter_closed [OF M_axioms_L] ``` wenzelm@13428 ` 524` ``` and Int_closed = M_axioms.Int_closed [OF M_axioms_L] ``` wenzelm@13428 ` 525` ``` and finite_fun_closed = M_axioms.finite_fun_closed [OF M_axioms_L] ``` wenzelm@13428 ` 526` ``` and is_funspace_abs = M_axioms.is_funspace_abs [OF M_axioms_L] ``` wenzelm@13428 ` 527` ``` and succ_fun_eq2 = M_axioms.succ_fun_eq2 [OF M_axioms_L] ``` wenzelm@13428 ` 528` ``` and funspace_succ = M_axioms.funspace_succ [OF M_axioms_L] ``` wenzelm@13428 ` 529` ``` and finite_funspace_closed = M_axioms.finite_funspace_closed [OF M_axioms_L] ``` paulson@13323 ` 530` wenzelm@13428 ` 531` ```lemmas is_recfun_equal = M_axioms.is_recfun_equal [OF M_axioms_L] ``` wenzelm@13428 ` 532` ``` and is_recfun_cut = M_axioms.is_recfun_cut [OF M_axioms_L] ``` wenzelm@13428 ` 533` ``` and is_recfun_functional = M_axioms.is_recfun_functional [OF M_axioms_L] ``` wenzelm@13428 ` 534` ``` and is_recfun_relativize = M_axioms.is_recfun_relativize [OF M_axioms_L] ``` wenzelm@13428 ` 535` ``` and is_recfun_restrict = M_axioms.is_recfun_restrict [OF M_axioms_L] ``` wenzelm@13428 ` 536` ``` and univalent_is_recfun = M_axioms.univalent_is_recfun [OF M_axioms_L] ``` wenzelm@13428 ` 537` ``` and exists_is_recfun_indstep = M_axioms.exists_is_recfun_indstep [OF M_axioms_L] ``` wenzelm@13428 ` 538` ``` and wellfounded_exists_is_recfun = M_axioms.wellfounded_exists_is_recfun [OF M_axioms_L] ``` wenzelm@13428 ` 539` ``` and wf_exists_is_recfun = M_axioms.wf_exists_is_recfun [OF M_axioms_L] ``` wenzelm@13428 ` 540` ``` and is_recfun_abs = M_axioms.is_recfun_abs [OF M_axioms_L] ``` wenzelm@13428 ` 541` ``` and irreflexive_abs = M_axioms.irreflexive_abs [OF M_axioms_L] ``` wenzelm@13428 ` 542` ``` and transitive_rel_abs = M_axioms.transitive_rel_abs [OF M_axioms_L] ``` wenzelm@13428 ` 543` ``` and linear_rel_abs = M_axioms.linear_rel_abs [OF M_axioms_L] ``` wenzelm@13428 ` 544` ``` and wellordered_is_trans_on = M_axioms.wellordered_is_trans_on [OF M_axioms_L] ``` wenzelm@13428 ` 545` ``` and wellordered_is_linear = M_axioms.wellordered_is_linear [OF M_axioms_L] ``` wenzelm@13428 ` 546` ``` and wellordered_is_wellfounded_on = M_axioms.wellordered_is_wellfounded_on [OF M_axioms_L] ``` wenzelm@13428 ` 547` ``` and wellfounded_imp_wellfounded_on = M_axioms.wellfounded_imp_wellfounded_on [OF M_axioms_L] ``` wenzelm@13428 ` 548` ``` and wellfounded_on_subset_A = M_axioms.wellfounded_on_subset_A [OF M_axioms_L] ``` wenzelm@13428 ` 549` ``` and wellfounded_on_iff_wellfounded = M_axioms.wellfounded_on_iff_wellfounded [OF M_axioms_L] ``` wenzelm@13428 ` 550` ``` and wellfounded_on_imp_wellfounded = M_axioms.wellfounded_on_imp_wellfounded [OF M_axioms_L] ``` wenzelm@13428 ` 551` ``` and wellfounded_on_field_imp_wellfounded = M_axioms.wellfounded_on_field_imp_wellfounded [OF M_axioms_L] ``` wenzelm@13428 ` 552` ``` and wellfounded_iff_wellfounded_on_field = M_axioms.wellfounded_iff_wellfounded_on_field [OF M_axioms_L] ``` wenzelm@13428 ` 553` ``` and wellfounded_induct = M_axioms.wellfounded_induct [OF M_axioms_L] ``` wenzelm@13428 ` 554` ``` and wellfounded_on_induct = M_axioms.wellfounded_on_induct [OF M_axioms_L] ``` wenzelm@13428 ` 555` ``` and wellfounded_on_induct2 = M_axioms.wellfounded_on_induct2 [OF M_axioms_L] ``` wenzelm@13428 ` 556` ``` and linear_imp_relativized = M_axioms.linear_imp_relativized [OF M_axioms_L] ``` wenzelm@13428 ` 557` ``` and trans_on_imp_relativized = M_axioms.trans_on_imp_relativized [OF M_axioms_L] ``` wenzelm@13428 ` 558` ``` and wf_on_imp_relativized = M_axioms.wf_on_imp_relativized [OF M_axioms_L] ``` wenzelm@13428 ` 559` ``` and wf_imp_relativized = M_axioms.wf_imp_relativized [OF M_axioms_L] ``` wenzelm@13428 ` 560` ``` and well_ord_imp_relativized = M_axioms.well_ord_imp_relativized [OF M_axioms_L] ``` wenzelm@13428 ` 561` ``` and order_isomorphism_abs = M_axioms.order_isomorphism_abs [OF M_axioms_L] ``` wenzelm@13428 ` 562` ``` and pred_set_abs = M_axioms.pred_set_abs [OF M_axioms_L] ``` paulson@13323 ` 563` wenzelm@13428 ` 564` ```lemmas pred_closed = M_axioms.pred_closed [OF M_axioms_L] ``` wenzelm@13428 ` 565` ``` and membership_abs = M_axioms.membership_abs [OF M_axioms_L] ``` wenzelm@13428 ` 566` ``` and M_Memrel_iff = M_axioms.M_Memrel_iff [OF M_axioms_L] ``` wenzelm@13428 ` 567` ``` and Memrel_closed = M_axioms.Memrel_closed [OF M_axioms_L] ``` wenzelm@13428 ` 568` ``` and wellordered_iso_predD = M_axioms.wellordered_iso_predD [OF M_axioms_L] ``` wenzelm@13428 ` 569` ``` and wellordered_iso_pred_eq = M_axioms.wellordered_iso_pred_eq [OF M_axioms_L] ``` wenzelm@13428 ` 570` ``` and wellfounded_on_asym = M_axioms.wellfounded_on_asym [OF M_axioms_L] ``` wenzelm@13428 ` 571` ``` and wellordered_asym = M_axioms.wellordered_asym [OF M_axioms_L] ``` wenzelm@13428 ` 572` ``` and ord_iso_pred_imp_lt = M_axioms.ord_iso_pred_imp_lt [OF M_axioms_L] ``` wenzelm@13428 ` 573` ``` and obase_iff = M_axioms.obase_iff [OF M_axioms_L] ``` wenzelm@13428 ` 574` ``` and omap_iff = M_axioms.omap_iff [OF M_axioms_L] ``` wenzelm@13428 ` 575` ``` and omap_unique = M_axioms.omap_unique [OF M_axioms_L] ``` wenzelm@13428 ` 576` ``` and omap_yields_Ord = M_axioms.omap_yields_Ord [OF M_axioms_L] ``` wenzelm@13428 ` 577` ``` and otype_iff = M_axioms.otype_iff [OF M_axioms_L] ``` wenzelm@13428 ` 578` ``` and otype_eq_range = M_axioms.otype_eq_range [OF M_axioms_L] ``` wenzelm@13428 ` 579` ``` and Ord_otype = M_axioms.Ord_otype [OF M_axioms_L] ``` wenzelm@13428 ` 580` ``` and domain_omap = M_axioms.domain_omap [OF M_axioms_L] ``` wenzelm@13428 ` 581` ``` and omap_subset = M_axioms.omap_subset [OF M_axioms_L] ``` wenzelm@13428 ` 582` ``` and omap_funtype = M_axioms.omap_funtype [OF M_axioms_L] ``` wenzelm@13428 ` 583` ``` and wellordered_omap_bij = M_axioms.wellordered_omap_bij [OF M_axioms_L] ``` wenzelm@13428 ` 584` ``` and omap_ord_iso = M_axioms.omap_ord_iso [OF M_axioms_L] ``` wenzelm@13428 ` 585` ``` and Ord_omap_image_pred = M_axioms.Ord_omap_image_pred [OF M_axioms_L] ``` wenzelm@13428 ` 586` ``` and restrict_omap_ord_iso = M_axioms.restrict_omap_ord_iso [OF M_axioms_L] ``` wenzelm@13428 ` 587` ``` and obase_equals = M_axioms.obase_equals [OF M_axioms_L] ``` wenzelm@13428 ` 588` ``` and omap_ord_iso_otype = M_axioms.omap_ord_iso_otype [OF M_axioms_L] ``` wenzelm@13428 ` 589` ``` and obase_exists = M_axioms.obase_exists [OF M_axioms_L] ``` wenzelm@13428 ` 590` ``` and omap_exists = M_axioms.omap_exists [OF M_axioms_L] ``` wenzelm@13428 ` 591` ``` and otype_exists = M_axioms.otype_exists [OF M_axioms_L] ``` wenzelm@13428 ` 592` ``` and omap_ord_iso_otype' = M_axioms.omap_ord_iso_otype' [OF M_axioms_L] ``` wenzelm@13428 ` 593` ``` and ordertype_exists = M_axioms.ordertype_exists [OF M_axioms_L] ``` wenzelm@13428 ` 594` ``` and relativized_imp_well_ord = M_axioms.relativized_imp_well_ord [OF M_axioms_L] ``` wenzelm@13428 ` 595` ``` and well_ord_abs = M_axioms.well_ord_abs [OF M_axioms_L] ``` wenzelm@13428 ` 596` wenzelm@13429 ` 597` ```declare cartprod_closed [intro, simp] ``` wenzelm@13429 ` 598` ```declare sum_closed [intro, simp] ``` wenzelm@13429 ` 599` ```declare converse_closed [intro, simp] ``` paulson@13323 ` 600` ```declare converse_abs [simp] ``` wenzelm@13429 ` 601` ```declare image_closed [intro, simp] ``` paulson@13323 ` 602` ```declare vimage_abs [simp] ``` wenzelm@13429 ` 603` ```declare vimage_closed [intro, simp] ``` paulson@13323 ` 604` ```declare domain_abs [simp] ``` wenzelm@13429 ` 605` ```declare domain_closed [intro, simp] ``` paulson@13323 ` 606` ```declare range_abs [simp] ``` wenzelm@13429 ` 607` ```declare range_closed [intro, simp] ``` paulson@13323 ` 608` ```declare field_abs [simp] ``` wenzelm@13429 ` 609` ```declare field_closed [intro, simp] ``` paulson@13323 ` 610` ```declare relation_abs [simp] ``` paulson@13323 ` 611` ```declare function_abs [simp] ``` wenzelm@13429 ` 612` ```declare apply_closed [intro, simp] ``` paulson@13323 ` 613` ```declare typed_function_abs [simp] ``` paulson@13323 ` 614` ```declare injection_abs [simp] ``` paulson@13323 ` 615` ```declare surjection_abs [simp] ``` paulson@13323 ` 616` ```declare bijection_abs [simp] ``` wenzelm@13429 ` 617` ```declare comp_closed [intro, simp] ``` paulson@13323 ` 618` ```declare composition_abs [simp] ``` paulson@13323 ` 619` ```declare restriction_abs [simp] ``` wenzelm@13429 ` 620` ```declare restrict_closed [intro, simp] ``` paulson@13323 ` 621` ```declare Inter_abs [simp] ``` wenzelm@13429 ` 622` ```declare Inter_closed [intro, simp] ``` wenzelm@13429 ` 623` ```declare Int_closed [intro, simp] ``` paulson@13323 ` 624` ```declare is_funspace_abs [simp] ``` wenzelm@13429 ` 625` ```declare finite_funspace_closed [intro, simp] ``` paulson@13323 ` 626` paulson@13306 ` 627` ```end ```