src/ZF/Constructible/Separation.thy
 author paulson Mon Jul 08 15:56:39 2002 +0200 (2002-07-08) changeset 13314 84b9de3cbc91 parent 13306 6eebcddee32b child 13316 d16629fd0f95 permissions -rw-r--r--
Defining a meta-existential quantifier.
Using it to streamline reflection proofs.
 paulson@13306 ` 1` ```header{*Proving instances of Separation using Reflection!*} ``` paulson@13306 ` 2` paulson@13306 ` 3` ```theory Separation = L_axioms: ``` paulson@13306 ` 4` paulson@13306 ` 5` ```text{*Helps us solve for de Bruijn indices!*} ``` paulson@13306 ` 6` ```lemma nth_ConsI: "[|nth(n,l) = x; n \ nat|] ==> nth(succ(n), Cons(a,l)) = x" ``` paulson@13306 ` 7` ```by simp ``` paulson@13306 ` 8` paulson@13306 ` 9` paulson@13306 ` 10` ```lemma Collect_conj_in_DPow: ``` paulson@13306 ` 11` ``` "[| {x\A. P(x)} \ DPow(A); {x\A. Q(x)} \ DPow(A) |] ``` paulson@13306 ` 12` ``` ==> {x\A. P(x) & Q(x)} \ DPow(A)" ``` paulson@13306 ` 13` ```by (simp add: Int_in_DPow Collect_Int_Collect_eq [symmetric]) ``` paulson@13306 ` 14` paulson@13306 ` 15` ```lemma Collect_conj_in_DPow_Lset: ``` paulson@13306 ` 16` ``` "[|z \ Lset(j); {x \ Lset(j). P(x)} \ DPow(Lset(j))|] ``` paulson@13306 ` 17` ``` ==> {x \ Lset(j). x \ z & P(x)} \ DPow(Lset(j))" ``` paulson@13306 ` 18` ```apply (frule mem_Lset_imp_subset_Lset) ``` paulson@13306 ` 19` ```apply (simp add: Collect_conj_in_DPow Collect_mem_eq ``` paulson@13306 ` 20` ``` subset_Int_iff2 elem_subset_in_DPow) ``` paulson@13306 ` 21` ```done ``` paulson@13306 ` 22` paulson@13306 ` 23` ```lemma separation_CollectI: ``` paulson@13306 ` 24` ``` "(\z. L(z) ==> L({x \ z . P(x)})) ==> separation(L, \x. P(x))" ``` paulson@13306 ` 25` ```apply (unfold separation_def, clarify) ``` paulson@13306 ` 26` ```apply (rule_tac x="{x\z. P(x)}" in rexI) ``` paulson@13306 ` 27` ```apply simp_all ``` paulson@13306 ` 28` ```done ``` paulson@13306 ` 29` paulson@13306 ` 30` ```text{*Reduces the original comprehension to the reflected one*} ``` paulson@13306 ` 31` ```lemma reflection_imp_L_separation: ``` paulson@13306 ` 32` ``` "[| \x\Lset(j). P(x) <-> Q(x); ``` paulson@13306 ` 33` ``` {x \ Lset(j) . Q(x)} \ DPow(Lset(j)); ``` paulson@13306 ` 34` ``` Ord(j); z \ Lset(j)|] ==> L({x \ z . P(x)})" ``` paulson@13306 ` 35` ```apply (rule_tac i = "succ(j)" in L_I) ``` paulson@13306 ` 36` ``` prefer 2 apply simp ``` paulson@13306 ` 37` ```apply (subgoal_tac "{x \ z. P(x)} = {x \ Lset(j). x \ z & (Q(x))}") ``` paulson@13306 ` 38` ``` prefer 2 ``` paulson@13306 ` 39` ``` apply (blast dest: mem_Lset_imp_subset_Lset) ``` paulson@13306 ` 40` ```apply (simp add: Lset_succ Collect_conj_in_DPow_Lset) ``` paulson@13306 ` 41` ```done ``` paulson@13306 ` 42` paulson@13306 ` 43` paulson@13306 ` 44` ```subsubsection{*Separation for Intersection*} ``` paulson@13306 ` 45` paulson@13306 ` 46` ```lemma Inter_Reflects: ``` paulson@13314 ` 47` ``` "REFLECTS[\x. \y[L]. y\A --> x \ y, ``` paulson@13314 ` 48` ``` \i x. \y\Lset(i). y\A --> x \ y]" ``` paulson@13314 ` 49` ```by (intro FOL_reflection) ``` paulson@13306 ` 50` paulson@13306 ` 51` ```lemma Inter_separation: ``` paulson@13306 ` 52` ``` "L(A) ==> separation(L, \x. \y[L]. y\A --> x\y)" ``` paulson@13306 ` 53` ```apply (rule separation_CollectI) ``` paulson@13306 ` 54` ```apply (rule_tac A="{A,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 55` ```apply (rule ReflectsE [OF Inter_Reflects], assumption) ``` paulson@13306 ` 56` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 57` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 58` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13306 ` 59` ```apply (rule DPowI2) ``` paulson@13306 ` 60` ```apply (rule ball_iff_sats) ``` paulson@13306 ` 61` ```apply (rule imp_iff_sats) ``` paulson@13306 ` 62` ```apply (rule_tac [2] i=1 and j=0 and env="[y,x,A]" in mem_iff_sats) ``` paulson@13306 ` 63` ```apply (rule_tac i=0 and j=2 in mem_iff_sats) ``` paulson@13306 ` 64` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13306 ` 65` ```done ``` paulson@13306 ` 66` paulson@13306 ` 67` ```subsubsection{*Separation for Cartesian Product*} ``` paulson@13306 ` 68` paulson@13306 ` 69` ```lemma cartprod_Reflects [simplified]: ``` paulson@13314 ` 70` ``` "REFLECTS[\z. \x[L]. x\A & (\y[L]. y\B & pair(L,x,y,z)), ``` paulson@13306 ` 71` ``` \i z. \x\Lset(i). x\A & (\y\Lset(i). y\B & ``` paulson@13314 ` 72` ``` pair(**Lset(i),x,y,z))]" ``` paulson@13314 ` 73` ```by (intro FOL_reflection function_reflection) ``` paulson@13306 ` 74` paulson@13306 ` 75` ```lemma cartprod_separation: ``` paulson@13306 ` 76` ``` "[| L(A); L(B) |] ``` paulson@13306 ` 77` ``` ==> separation(L, \z. \x[L]. x\A & (\y[L]. y\B & pair(L,x,y,z)))" ``` paulson@13306 ` 78` ```apply (rule separation_CollectI) ``` paulson@13306 ` 79` ```apply (rule_tac A="{A,B,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 80` ```apply (rule ReflectsE [OF cartprod_Reflects], assumption) ``` paulson@13306 ` 81` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 82` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 83` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13306 ` 84` ```apply (rule DPowI2) ``` paulson@13306 ` 85` ```apply (rename_tac u) ``` paulson@13306 ` 86` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 87` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 88` ```apply (rule_tac i=0 and j=2 and env="[x,u,A,B]" in mem_iff_sats, simp_all) ``` paulson@13306 ` 89` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 90` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 91` ```apply (rule mem_iff_sats) ``` paulson@13306 ` 92` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 93` ```apply (blast intro: nth_0 nth_ConsI, simp_all) ``` paulson@13306 ` 94` ```apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats) ``` paulson@13306 ` 95` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13306 ` 96` ```done ``` paulson@13306 ` 97` paulson@13306 ` 98` ```subsubsection{*Separation for Image*} ``` paulson@13306 ` 99` paulson@13306 ` 100` ```text{*No @{text simplified} here: it simplifies the occurrence of ``` paulson@13306 ` 101` ``` the predicate @{term pair}!*} ``` paulson@13306 ` 102` ```lemma image_Reflects: ``` paulson@13314 ` 103` ``` "REFLECTS[\y. \p[L]. p\r & (\x[L]. x\A & pair(L,x,y,p)), ``` paulson@13314 ` 104` ``` \i y. \p\Lset(i). p\r & (\x\Lset(i). x\A & pair(**Lset(i),x,y,p))]" ``` paulson@13314 ` 105` ```by (intro FOL_reflection function_reflection) ``` paulson@13306 ` 106` paulson@13306 ` 107` paulson@13306 ` 108` ```lemma image_separation: ``` paulson@13306 ` 109` ``` "[| L(A); L(r) |] ``` paulson@13306 ` 110` ``` ==> separation(L, \y. \p[L]. p\r & (\x[L]. x\A & pair(L,x,y,p)))" ``` paulson@13306 ` 111` ```apply (rule separation_CollectI) ``` paulson@13306 ` 112` ```apply (rule_tac A="{A,r,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 113` ```apply (rule ReflectsE [OF image_Reflects], assumption) ``` paulson@13306 ` 114` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 115` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 116` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13306 ` 117` ```apply (rule DPowI2) ``` paulson@13306 ` 118` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 119` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 120` ```apply (rule_tac env="[p,y,A,r]" in mem_iff_sats) ``` paulson@13306 ` 121` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 122` ```apply (blast intro: nth_0 nth_ConsI, simp_all) ``` paulson@13306 ` 123` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 124` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 125` ```apply (rule mem_iff_sats) ``` paulson@13306 ` 126` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 127` ```apply (blast intro: nth_0 nth_ConsI, simp_all) ``` paulson@13306 ` 128` ```apply (rule pair_iff_sats) ``` paulson@13306 ` 129` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 130` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 131` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 132` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13306 ` 133` ```done ``` paulson@13306 ` 134` paulson@13306 ` 135` paulson@13306 ` 136` ```subsubsection{*Separation for Converse*} ``` paulson@13306 ` 137` paulson@13306 ` 138` ```lemma converse_Reflects: ``` paulson@13314 ` 139` ``` "REFLECTS[\z. \p[L]. p\r & (\x[L]. \y[L]. pair(L,x,y,p) & pair(L,y,x,z)), ``` paulson@13306 ` 140` ``` \i z. \p\Lset(i). p\r & (\x\Lset(i). \y\Lset(i). ``` paulson@13314 ` 141` ``` pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z))]" ``` paulson@13314 ` 142` ```by (intro FOL_reflection function_reflection) ``` paulson@13306 ` 143` paulson@13306 ` 144` ```lemma converse_separation: ``` paulson@13306 ` 145` ``` "L(r) ==> separation(L, ``` paulson@13306 ` 146` ``` \z. \p[L]. p\r & (\x[L]. \y[L]. pair(L,x,y,p) & pair(L,y,x,z)))" ``` paulson@13306 ` 147` ```apply (rule separation_CollectI) ``` paulson@13306 ` 148` ```apply (rule_tac A="{r,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 149` ```apply (rule ReflectsE [OF converse_Reflects], assumption) ``` paulson@13306 ` 150` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 151` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 152` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13306 ` 153` ```apply (rule DPowI2) ``` paulson@13306 ` 154` ```apply (rename_tac u) ``` paulson@13306 ` 155` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 156` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 157` ```apply (rule_tac i=0 and j="2" and env="[p,u,r]" in mem_iff_sats, simp_all) ``` paulson@13306 ` 158` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 159` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 160` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 161` ```apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats, simp_all) ``` paulson@13306 ` 162` ```apply (rule pair_iff_sats) ``` paulson@13306 ` 163` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 164` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 165` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 166` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13306 ` 167` ```done ``` paulson@13306 ` 168` paulson@13306 ` 169` paulson@13306 ` 170` ```subsubsection{*Separation for Restriction*} ``` paulson@13306 ` 171` paulson@13306 ` 172` ```lemma restrict_Reflects: ``` paulson@13314 ` 173` ``` "REFLECTS[\z. \x[L]. x\A & (\y[L]. pair(L,x,y,z)), ``` paulson@13314 ` 174` ``` \i z. \x\Lset(i). x\A & (\y\Lset(i). pair(**Lset(i),x,y,z))]" ``` paulson@13314 ` 175` ```by (intro FOL_reflection function_reflection) ``` paulson@13306 ` 176` paulson@13306 ` 177` ```lemma restrict_separation: ``` paulson@13306 ` 178` ``` "L(A) ==> separation(L, \z. \x[L]. x\A & (\y[L]. pair(L,x,y,z)))" ``` paulson@13306 ` 179` ```apply (rule separation_CollectI) ``` paulson@13306 ` 180` ```apply (rule_tac A="{A,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 181` ```apply (rule ReflectsE [OF restrict_Reflects], assumption) ``` paulson@13306 ` 182` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 183` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 184` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13306 ` 185` ```apply (rule DPowI2) ``` paulson@13306 ` 186` ```apply (rename_tac u) ``` paulson@13306 ` 187` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 188` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 189` ```apply (rule_tac i=0 and j="2" and env="[x,u,A]" in mem_iff_sats, simp_all) ``` paulson@13306 ` 190` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 191` ```apply (rule_tac i=1 and j=0 and k=2 in pair_iff_sats) ``` paulson@13306 ` 192` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13306 ` 193` ```done ``` paulson@13306 ` 194` paulson@13306 ` 195` paulson@13306 ` 196` ```subsubsection{*Separation for Composition*} ``` paulson@13306 ` 197` paulson@13306 ` 198` ```lemma comp_Reflects: ``` paulson@13314 ` 199` ``` "REFLECTS[\xz. \x[L]. \y[L]. \z[L]. \xy[L]. \yz[L]. ``` paulson@13306 ` 200` ``` pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & ``` paulson@13306 ` 201` ``` xy\s & yz\r, ``` paulson@13306 ` 202` ``` \i xz. \x\Lset(i). \y\Lset(i). \z\Lset(i). \xy\Lset(i). \yz\Lset(i). ``` paulson@13306 ` 203` ``` pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) & ``` paulson@13314 ` 204` ``` pair(**Lset(i),y,z,yz) & xy\s & yz\r]" ``` paulson@13314 ` 205` ```by (intro FOL_reflection function_reflection) ``` paulson@13306 ` 206` paulson@13306 ` 207` ```lemma comp_separation: ``` paulson@13306 ` 208` ``` "[| L(r); L(s) |] ``` paulson@13306 ` 209` ``` ==> separation(L, \xz. \x[L]. \y[L]. \z[L]. \xy[L]. \yz[L]. ``` paulson@13306 ` 210` ``` pair(L,x,z,xz) & pair(L,x,y,xy) & pair(L,y,z,yz) & ``` paulson@13306 ` 211` ``` xy\s & yz\r)" ``` paulson@13306 ` 212` ```apply (rule separation_CollectI) ``` paulson@13306 ` 213` ```apply (rule_tac A="{r,s,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 214` ```apply (rule ReflectsE [OF comp_Reflects], assumption) ``` paulson@13306 ` 215` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 216` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 217` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13306 ` 218` ```apply (rule DPowI2) ``` paulson@13306 ` 219` ```apply (rename_tac u) ``` paulson@13306 ` 220` ```apply (rule bex_iff_sats)+ ``` paulson@13306 ` 221` ```apply (rename_tac x y z) ``` paulson@13306 ` 222` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 223` ```apply (rule_tac env="[z,y,x,u,r,s]" in pair_iff_sats) ``` paulson@13306 ` 224` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 225` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 226` ```apply (blast intro: nth_0 nth_ConsI, simp_all) ``` paulson@13306 ` 227` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 228` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 229` ```apply (rule pair_iff_sats) ``` paulson@13306 ` 230` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 231` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 232` ```apply (blast intro: nth_0 nth_ConsI, simp_all) ``` paulson@13306 ` 233` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 234` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 235` ```apply (rule pair_iff_sats) ``` paulson@13306 ` 236` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 237` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 238` ```apply (blast intro: nth_0 nth_ConsI, simp_all) ``` paulson@13306 ` 239` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 240` ```apply (rule mem_iff_sats) ``` paulson@13306 ` 241` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 242` ```apply (blast intro: nth_0 nth_ConsI, simp) ``` paulson@13306 ` 243` ```apply (rule mem_iff_sats) ``` paulson@13306 ` 244` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 245` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 246` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13306 ` 247` ```done ``` paulson@13306 ` 248` paulson@13306 ` 249` ```subsubsection{*Separation for Predecessors in an Order*} ``` paulson@13306 ` 250` paulson@13306 ` 251` ```lemma pred_Reflects: ``` paulson@13314 ` 252` ``` "REFLECTS[\y. \p[L]. p\r & pair(L,y,x,p), ``` paulson@13314 ` 253` ``` \i y. \p \ Lset(i). p\r & pair(**Lset(i),y,x,p)]" ``` paulson@13314 ` 254` ```by (intro FOL_reflection function_reflection) ``` paulson@13306 ` 255` paulson@13306 ` 256` ```lemma pred_separation: ``` paulson@13306 ` 257` ``` "[| L(r); L(x) |] ==> separation(L, \y. \p[L]. p\r & pair(L,y,x,p))" ``` paulson@13306 ` 258` ```apply (rule separation_CollectI) ``` paulson@13306 ` 259` ```apply (rule_tac A="{r,x,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 260` ```apply (rule ReflectsE [OF pred_Reflects], assumption) ``` paulson@13306 ` 261` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 262` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 263` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13306 ` 264` ```apply (rule DPowI2) ``` paulson@13306 ` 265` ```apply (rename_tac u) ``` paulson@13306 ` 266` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 267` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 268` ```apply (rule_tac env = "[p,u,r,x]" in mem_iff_sats) ``` paulson@13306 ` 269` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 270` ```apply (blast intro: nth_0 nth_ConsI, simp) ``` paulson@13306 ` 271` ```apply (rule pair_iff_sats) ``` paulson@13306 ` 272` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 273` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 274` ```apply (blast intro: nth_0 nth_ConsI, simp_all) ``` paulson@13306 ` 275` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13306 ` 276` ```done ``` paulson@13306 ` 277` paulson@13306 ` 278` paulson@13306 ` 279` ```subsubsection{*Separation for the Membership Relation*} ``` paulson@13306 ` 280` paulson@13306 ` 281` ```lemma Memrel_Reflects: ``` paulson@13314 ` 282` ``` "REFLECTS[\z. \x[L]. \y[L]. pair(L,x,y,z) & x \ y, ``` paulson@13314 ` 283` ``` \i z. \x \ Lset(i). \y \ Lset(i). pair(**Lset(i),x,y,z) & x \ y]" ``` paulson@13314 ` 284` ```by (intro FOL_reflection function_reflection) ``` paulson@13306 ` 285` paulson@13306 ` 286` ```lemma Memrel_separation: ``` paulson@13306 ` 287` ``` "separation(L, \z. \x[L]. \y[L]. pair(L,x,y,z) & x \ y)" ``` paulson@13306 ` 288` ```apply (rule separation_CollectI) ``` paulson@13306 ` 289` ```apply (rule_tac A="{z}" in subset_LsetE, blast ) ``` paulson@13306 ` 290` ```apply (rule ReflectsE [OF Memrel_Reflects], assumption) ``` paulson@13306 ` 291` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 292` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 293` ``` apply (simp_all add: lt_Ord2) ``` paulson@13306 ` 294` ```apply (rule DPowI2) ``` paulson@13306 ` 295` ```apply (rename_tac u) ``` paulson@13306 ` 296` ```apply (rule bex_iff_sats)+ ``` paulson@13306 ` 297` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 298` ```apply (rule_tac env = "[y,x,u]" in pair_iff_sats) ``` paulson@13306 ` 299` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 300` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 301` ```apply (blast intro: nth_0 nth_ConsI, simp_all) ``` paulson@13306 ` 302` ```apply (rule mem_iff_sats) ``` paulson@13306 ` 303` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 304` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 305` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13306 ` 306` ```done ``` paulson@13306 ` 307` paulson@13306 ` 308` paulson@13306 ` 309` ```subsubsection{*Replacement for FunSpace*} ``` paulson@13306 ` 310` ``` ``` paulson@13306 ` 311` ```lemma funspace_succ_Reflects: ``` paulson@13314 ` 312` ``` "REFLECTS[\z. \p[L]. p\A & (\f[L]. \b[L]. \nb[L]. \cnbf[L]. ``` paulson@13306 ` 313` ``` pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) & ``` paulson@13306 ` 314` ``` upair(L,cnbf,cnbf,z)), ``` paulson@13306 ` 315` ``` \i z. \p \ Lset(i). p\A & (\f \ Lset(i). \b \ Lset(i). ``` paulson@13306 ` 316` ``` \nb \ Lset(i). \cnbf \ Lset(i). ``` paulson@13306 ` 317` ``` pair(**Lset(i),f,b,p) & pair(**Lset(i),n,b,nb) & ``` paulson@13314 ` 318` ``` is_cons(**Lset(i),nb,f,cnbf) & upair(**Lset(i),cnbf,cnbf,z))]" ``` paulson@13314 ` 319` ```by (intro FOL_reflection function_reflection) ``` paulson@13306 ` 320` paulson@13306 ` 321` ```lemma funspace_succ_replacement: ``` paulson@13306 ` 322` ``` "L(n) ==> ``` paulson@13306 ` 323` ``` strong_replacement(L, \p z. \f[L]. \b[L]. \nb[L]. \cnbf[L]. ``` paulson@13306 ` 324` ``` pair(L,f,b,p) & pair(L,n,b,nb) & is_cons(L,nb,f,cnbf) & ``` paulson@13306 ` 325` ``` upair(L,cnbf,cnbf,z))" ``` paulson@13306 ` 326` ```apply (rule strong_replacementI) ``` paulson@13306 ` 327` ```apply (rule rallI) ``` paulson@13306 ` 328` ```apply (rule separation_CollectI) ``` paulson@13306 ` 329` ```apply (rule_tac A="{n,A,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 330` ```apply (rule ReflectsE [OF funspace_succ_Reflects], assumption) ``` paulson@13306 ` 331` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 332` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 333` ``` apply (simp_all add: lt_Ord2) ``` paulson@13306 ` 334` ```apply (rule DPowI2) ``` paulson@13306 ` 335` ```apply (rename_tac u) ``` paulson@13306 ` 336` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 337` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 338` ```apply (rule_tac env = "[x,u,n,A]" in mem_iff_sats) ``` paulson@13306 ` 339` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 340` ```apply (blast intro: nth_0 nth_ConsI, simp_all) ``` paulson@13306 ` 341` ```apply (rule conj_iff_sats bex_iff_sats)+ ``` paulson@13306 ` 342` ```apply (rule pair_iff_sats) ``` paulson@13306 ` 343` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 344` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 345` ```apply (blast intro: nth_0 nth_ConsI, simp_all) ``` paulson@13306 ` 346` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 347` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 348` ```apply (rule pair_iff_sats) ``` paulson@13306 ` 349` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 350` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 351` ```apply (blast intro: nth_0 nth_ConsI, simp_all) ``` paulson@13306 ` 352` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 353` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 354` ```apply (rule cons_iff_sats) ``` paulson@13306 ` 355` ```apply (blast intro!: nth_0 nth_ConsI) ``` paulson@13306 ` 356` ```apply (blast intro!: nth_0 nth_ConsI) ``` paulson@13306 ` 357` ```apply (blast intro!: nth_0 nth_ConsI, simp_all) ``` paulson@13306 ` 358` ```apply (rule upair_iff_sats) ``` paulson@13306 ` 359` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 360` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 361` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 362` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13306 ` 363` ```done ``` paulson@13306 ` 364` paulson@13306 ` 365` paulson@13306 ` 366` ```subsubsection{*Separation for Order-Isomorphisms*} ``` paulson@13306 ` 367` paulson@13306 ` 368` ```lemma well_ord_iso_Reflects: ``` paulson@13314 ` 369` ``` "REFLECTS[\x. x\A --> ``` paulson@13314 ` 370` ``` (\y[L]. \p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \ r), ``` paulson@13314 ` 371` ``` \i x. x\A --> (\y \ Lset(i). \p \ Lset(i). ``` paulson@13314 ` 372` ``` fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \ r)]" ``` paulson@13314 ` 373` ```by (intro FOL_reflection function_reflection) ``` paulson@13306 ` 374` paulson@13306 ` 375` ```lemma well_ord_iso_separation: ``` paulson@13306 ` 376` ``` "[| L(A); L(f); L(r) |] ``` paulson@13306 ` 377` ``` ==> separation (L, \x. x\A --> (\y[L]. (\p[L]. ``` paulson@13306 ` 378` ``` fun_apply(L,f,x,y) & pair(L,y,x,p) & p \ r)))" ``` paulson@13306 ` 379` ```apply (rule separation_CollectI) ``` paulson@13306 ` 380` ```apply (rule_tac A="{A,f,r,z}" in subset_LsetE, blast ) ``` paulson@13306 ` 381` ```apply (rule ReflectsE [OF well_ord_iso_Reflects], assumption) ``` paulson@13306 ` 382` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13306 ` 383` ```apply (erule reflection_imp_L_separation) ``` paulson@13306 ` 384` ``` apply (simp_all add: lt_Ord2) ``` paulson@13306 ` 385` ```apply (rule DPowI2) ``` paulson@13306 ` 386` ```apply (rename_tac u) ``` paulson@13306 ` 387` ```apply (rule imp_iff_sats) ``` paulson@13306 ` 388` ```apply (rule_tac env = "[u,A,f,r]" in mem_iff_sats) ``` paulson@13306 ` 389` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 390` ```apply (blast intro: nth_0 nth_ConsI, simp_all) ``` paulson@13306 ` 391` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 392` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 393` ```apply (rule fun_apply_iff_sats) ``` paulson@13306 ` 394` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 395` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 396` ```apply (blast intro: nth_0 nth_ConsI, simp_all) ``` paulson@13306 ` 397` ```apply (rule bex_iff_sats) ``` paulson@13306 ` 398` ```apply (rule conj_iff_sats) ``` paulson@13306 ` 399` ```apply (rule pair_iff_sats) ``` paulson@13306 ` 400` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 401` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 402` ```apply (blast intro: nth_0 nth_ConsI, simp_all) ``` paulson@13306 ` 403` ```apply (rule mem_iff_sats) ``` paulson@13306 ` 404` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 405` ```apply (blast intro: nth_0 nth_ConsI) ``` paulson@13306 ` 406` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13306 ` 407` ```done ``` paulson@13306 ` 408` paulson@13306 ` 409` ```end ```