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