src/ZF/Constructible/Rec_Separation.thy
 author paulson Thu Jul 11 13:43:24 2002 +0200 (2002-07-11) changeset 13348 374d05460db4 child 13352 3cd767f8d78b permissions -rw-r--r--
Separation/Replacement up to M_wfrank!
 paulson@13348 ` 1` ```header{*Separation for the Absoluteness of Recursion*} ``` paulson@13348 ` 2` paulson@13348 ` 3` ```theory Rec_Separation = Separation: ``` paulson@13348 ` 4` paulson@13348 ` 5` ```text{*This theory proves all instances needed for locales @{text ``` paulson@13348 ` 6` ```"M_trancl"}, @{text "M_wfrank"} and @{text "M_datatypes"}*} ``` paulson@13348 ` 7` paulson@13348 ` 8` ```subsection{*The Locale @{text "M_trancl"}*} ``` paulson@13348 ` 9` paulson@13348 ` 10` ```subsubsection{*Separation for Reflexive/Transitive Closure*} ``` paulson@13348 ` 11` paulson@13348 ` 12` ```text{*First, The Defining Formula*} ``` paulson@13348 ` 13` paulson@13348 ` 14` ```(* "rtran_closure_mem(M,A,r,p) == ``` paulson@13348 ` 15` ``` \nnat[M]. \n[M]. \n'[M]. ``` paulson@13348 ` 16` ``` omega(M,nnat) & n\nnat & successor(M,n,n') & ``` paulson@13348 ` 17` ``` (\f[M]. typed_function(M,n',A,f) & ``` paulson@13348 ` 18` ``` (\x[M]. \y[M]. \zero[M]. pair(M,x,y,p) & empty(M,zero) & ``` paulson@13348 ` 19` ``` fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) & ``` paulson@13348 ` 20` ``` (\j[M]. j\n --> ``` paulson@13348 ` 21` ``` (\fj[M]. \sj[M]. \fsj[M]. \ffp[M]. ``` paulson@13348 ` 22` ``` fun_apply(M,f,j,fj) & successor(M,j,sj) & ``` paulson@13348 ` 23` ``` fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \ r)))"*) ``` paulson@13348 ` 24` ```constdefs rtran_closure_mem_fm :: "[i,i,i]=>i" ``` paulson@13348 ` 25` ``` "rtran_closure_mem_fm(A,r,p) == ``` paulson@13348 ` 26` ``` Exists(Exists(Exists( ``` paulson@13348 ` 27` ``` And(omega_fm(2), ``` paulson@13348 ` 28` ``` And(Member(1,2), ``` paulson@13348 ` 29` ``` And(succ_fm(1,0), ``` paulson@13348 ` 30` ``` Exists(And(typed_function_fm(1, A#+4, 0), ``` paulson@13348 ` 31` ``` And(Exists(Exists(Exists( ``` paulson@13348 ` 32` ``` And(pair_fm(2,1,p#+7), ``` paulson@13348 ` 33` ``` And(empty_fm(0), ``` paulson@13348 ` 34` ``` And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))), ``` paulson@13348 ` 35` ``` Forall(Implies(Member(0,3), ``` paulson@13348 ` 36` ``` Exists(Exists(Exists(Exists( ``` paulson@13348 ` 37` ``` And(fun_apply_fm(5,4,3), ``` paulson@13348 ` 38` ``` And(succ_fm(4,2), ``` paulson@13348 ` 39` ``` And(fun_apply_fm(5,2,1), ``` paulson@13348 ` 40` ``` And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))" ``` paulson@13348 ` 41` paulson@13348 ` 42` paulson@13348 ` 43` ```lemma rtran_closure_mem_type [TC]: ``` paulson@13348 ` 44` ``` "[| x \ nat; y \ nat; z \ nat |] ==> rtran_closure_mem_fm(x,y,z) \ formula" ``` paulson@13348 ` 45` ```by (simp add: rtran_closure_mem_fm_def) ``` paulson@13348 ` 46` paulson@13348 ` 47` ```lemma arity_rtran_closure_mem_fm [simp]: ``` paulson@13348 ` 48` ``` "[| x \ nat; y \ nat; z \ nat |] ``` paulson@13348 ` 49` ``` ==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13348 ` 50` ```by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13348 ` 51` paulson@13348 ` 52` ```lemma sats_rtran_closure_mem_fm [simp]: ``` paulson@13348 ` 53` ``` "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13348 ` 54` ``` ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <-> ``` paulson@13348 ` 55` ``` rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))" ``` paulson@13348 ` 56` ```by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def) ``` paulson@13348 ` 57` paulson@13348 ` 58` ```lemma rtran_closure_mem_iff_sats: ``` paulson@13348 ` 59` ``` "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13348 ` 60` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13348 ` 61` ``` ==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)" ``` paulson@13348 ` 62` ```by (simp add: sats_rtran_closure_mem_fm) ``` paulson@13348 ` 63` paulson@13348 ` 64` ```theorem rtran_closure_mem_reflection: ``` paulson@13348 ` 65` ``` "REFLECTS[\x. rtran_closure_mem(L,f(x),g(x),h(x)), ``` paulson@13348 ` 66` ``` \i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]" ``` paulson@13348 ` 67` ```apply (simp only: rtran_closure_mem_def setclass_simps) ``` paulson@13348 ` 68` ```apply (intro FOL_reflections function_reflections fun_plus_reflections) ``` paulson@13348 ` 69` ```done ``` paulson@13348 ` 70` paulson@13348 ` 71` ```text{*Separation for @{term "rtrancl(r)"}.*} ``` paulson@13348 ` 72` ```lemma rtrancl_separation: ``` paulson@13348 ` 73` ``` "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))" ``` paulson@13348 ` 74` ```apply (rule separation_CollectI) ``` paulson@13348 ` 75` ```apply (rule_tac A="{r,A,z}" in subset_LsetE, blast ) ``` paulson@13348 ` 76` ```apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption) ``` paulson@13348 ` 77` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13348 ` 78` ```apply (erule reflection_imp_L_separation) ``` paulson@13348 ` 79` ``` apply (simp_all add: lt_Ord2) ``` paulson@13348 ` 80` ```apply (rule DPowI2) ``` paulson@13348 ` 81` ```apply (rename_tac u) ``` paulson@13348 ` 82` ```apply (rule_tac env = "[u,r,A]" in rtran_closure_mem_iff_sats) ``` paulson@13348 ` 83` ```apply (rule sep_rules | simp)+ ``` paulson@13348 ` 84` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13348 ` 85` ```done ``` paulson@13348 ` 86` paulson@13348 ` 87` paulson@13348 ` 88` ```subsubsection{*Reflexive/Transitive Closure, Internalized*} ``` paulson@13348 ` 89` paulson@13348 ` 90` ```(* "rtran_closure(M,r,s) == ``` paulson@13348 ` 91` ``` \A[M]. is_field(M,r,A) --> ``` paulson@13348 ` 92` ``` (\p[M]. p \ s <-> rtran_closure_mem(M,A,r,p))" *) ``` paulson@13348 ` 93` ```constdefs rtran_closure_fm :: "[i,i]=>i" ``` paulson@13348 ` 94` ``` "rtran_closure_fm(r,s) == ``` paulson@13348 ` 95` ``` Forall(Implies(field_fm(succ(r),0), ``` paulson@13348 ` 96` ``` Forall(Iff(Member(0,succ(succ(s))), ``` paulson@13348 ` 97` ``` rtran_closure_mem_fm(1,succ(succ(r)),0)))))" ``` paulson@13348 ` 98` paulson@13348 ` 99` ```lemma rtran_closure_type [TC]: ``` paulson@13348 ` 100` ``` "[| x \ nat; y \ nat |] ==> rtran_closure_fm(x,y) \ formula" ``` paulson@13348 ` 101` ```by (simp add: rtran_closure_fm_def) ``` paulson@13348 ` 102` paulson@13348 ` 103` ```lemma arity_rtran_closure_fm [simp]: ``` paulson@13348 ` 104` ``` "[| x \ nat; y \ nat |] ``` paulson@13348 ` 105` ``` ==> arity(rtran_closure_fm(x,y)) = succ(x) \ succ(y)" ``` paulson@13348 ` 106` ```by (simp add: rtran_closure_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13348 ` 107` paulson@13348 ` 108` ```lemma sats_rtran_closure_fm [simp]: ``` paulson@13348 ` 109` ``` "[| x \ nat; y \ nat; env \ list(A)|] ``` paulson@13348 ` 110` ``` ==> sats(A, rtran_closure_fm(x,y), env) <-> ``` paulson@13348 ` 111` ``` rtran_closure(**A, nth(x,env), nth(y,env))" ``` paulson@13348 ` 112` ```by (simp add: rtran_closure_fm_def rtran_closure_def) ``` paulson@13348 ` 113` paulson@13348 ` 114` ```lemma rtran_closure_iff_sats: ``` paulson@13348 ` 115` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13348 ` 116` ``` i \ nat; j \ nat; env \ list(A)|] ``` paulson@13348 ` 117` ``` ==> rtran_closure(**A, x, y) <-> sats(A, rtran_closure_fm(i,j), env)" ``` paulson@13348 ` 118` ```by simp ``` paulson@13348 ` 119` paulson@13348 ` 120` ```theorem rtran_closure_reflection: ``` paulson@13348 ` 121` ``` "REFLECTS[\x. rtran_closure(L,f(x),g(x)), ``` paulson@13348 ` 122` ``` \i x. rtran_closure(**Lset(i),f(x),g(x))]" ``` paulson@13348 ` 123` ```apply (simp only: rtran_closure_def setclass_simps) ``` paulson@13348 ` 124` ```apply (intro FOL_reflections function_reflections rtran_closure_mem_reflection) ``` paulson@13348 ` 125` ```done ``` paulson@13348 ` 126` paulson@13348 ` 127` paulson@13348 ` 128` ```subsubsection{*Transitive Closure of a Relation, Internalized*} ``` paulson@13348 ` 129` paulson@13348 ` 130` ```(* "tran_closure(M,r,t) == ``` paulson@13348 ` 131` ``` \s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" *) ``` paulson@13348 ` 132` ```constdefs tran_closure_fm :: "[i,i]=>i" ``` paulson@13348 ` 133` ``` "tran_closure_fm(r,s) == ``` paulson@13348 ` 134` ``` Exists(And(rtran_closure_fm(succ(r),0), composition_fm(succ(r),0,succ(s))))" ``` paulson@13348 ` 135` paulson@13348 ` 136` ```lemma tran_closure_type [TC]: ``` paulson@13348 ` 137` ``` "[| x \ nat; y \ nat |] ==> tran_closure_fm(x,y) \ formula" ``` paulson@13348 ` 138` ```by (simp add: tran_closure_fm_def) ``` paulson@13348 ` 139` paulson@13348 ` 140` ```lemma arity_tran_closure_fm [simp]: ``` paulson@13348 ` 141` ``` "[| x \ nat; y \ nat |] ``` paulson@13348 ` 142` ``` ==> arity(tran_closure_fm(x,y)) = succ(x) \ succ(y)" ``` paulson@13348 ` 143` ```by (simp add: tran_closure_fm_def succ_Un_distrib [symmetric] Un_ac) ``` paulson@13348 ` 144` paulson@13348 ` 145` ```lemma sats_tran_closure_fm [simp]: ``` paulson@13348 ` 146` ``` "[| x \ nat; y \ nat; env \ list(A)|] ``` paulson@13348 ` 147` ``` ==> sats(A, tran_closure_fm(x,y), env) <-> ``` paulson@13348 ` 148` ``` tran_closure(**A, nth(x,env), nth(y,env))" ``` paulson@13348 ` 149` ```by (simp add: tran_closure_fm_def tran_closure_def) ``` paulson@13348 ` 150` paulson@13348 ` 151` ```lemma tran_closure_iff_sats: ``` paulson@13348 ` 152` ``` "[| nth(i,env) = x; nth(j,env) = y; ``` paulson@13348 ` 153` ``` i \ nat; j \ nat; env \ list(A)|] ``` paulson@13348 ` 154` ``` ==> tran_closure(**A, x, y) <-> sats(A, tran_closure_fm(i,j), env)" ``` paulson@13348 ` 155` ```by simp ``` paulson@13348 ` 156` paulson@13348 ` 157` ```theorem tran_closure_reflection: ``` paulson@13348 ` 158` ``` "REFLECTS[\x. tran_closure(L,f(x),g(x)), ``` paulson@13348 ` 159` ``` \i x. tran_closure(**Lset(i),f(x),g(x))]" ``` paulson@13348 ` 160` ```apply (simp only: tran_closure_def setclass_simps) ``` paulson@13348 ` 161` ```apply (intro FOL_reflections function_reflections ``` paulson@13348 ` 162` ``` rtran_closure_reflection composition_reflection) ``` paulson@13348 ` 163` ```done ``` paulson@13348 ` 164` paulson@13348 ` 165` paulson@13348 ` 166` ```subsection{*Separation for the Proof of @{text "wellfounded_on_trancl"}*} ``` paulson@13348 ` 167` paulson@13348 ` 168` ```lemma wellfounded_trancl_reflects: ``` paulson@13348 ` 169` ``` "REFLECTS[\x. \w[L]. \wx[L]. \rp[L]. ``` paulson@13348 ` 170` ``` w \ Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \ rp, ``` paulson@13348 ` 171` ``` \i x. \w \ Lset(i). \wx \ Lset(i). \rp \ Lset(i). ``` paulson@13348 ` 172` ``` w \ Z & pair(**Lset(i),w,x,wx) & tran_closure(**Lset(i),r,rp) & ``` paulson@13348 ` 173` ``` wx \ rp]" ``` paulson@13348 ` 174` ```by (intro FOL_reflections function_reflections fun_plus_reflections ``` paulson@13348 ` 175` ``` tran_closure_reflection) ``` paulson@13348 ` 176` paulson@13348 ` 177` paulson@13348 ` 178` ```lemma wellfounded_trancl_separation: ``` paulson@13348 ` 179` ``` "[| L(r); L(Z) |] ==> ``` paulson@13348 ` 180` ``` separation (L, \x. ``` paulson@13348 ` 181` ``` \w[L]. \wx[L]. \rp[L]. ``` paulson@13348 ` 182` ``` w \ Z & pair(L,w,x,wx) & tran_closure(L,r,rp) & wx \ rp)" ``` paulson@13348 ` 183` ```apply (rule separation_CollectI) ``` paulson@13348 ` 184` ```apply (rule_tac A="{r,Z,z}" in subset_LsetE, blast ) ``` paulson@13348 ` 185` ```apply (rule ReflectsE [OF wellfounded_trancl_reflects], assumption) ``` paulson@13348 ` 186` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13348 ` 187` ```apply (erule reflection_imp_L_separation) ``` paulson@13348 ` 188` ``` apply (simp_all add: lt_Ord2) ``` paulson@13348 ` 189` ```apply (rule DPowI2) ``` paulson@13348 ` 190` ```apply (rename_tac u) ``` paulson@13348 ` 191` ```apply (rule bex_iff_sats conj_iff_sats)+ ``` paulson@13348 ` 192` ```apply (rule_tac env = "[w,u,r,Z]" in mem_iff_sats) ``` paulson@13348 ` 193` ```apply (rule sep_rules tran_closure_iff_sats | simp)+ ``` paulson@13348 ` 194` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13348 ` 195` ```done ``` paulson@13348 ` 196` paulson@13348 ` 197` ```subsection{*Well-Founded Recursion!*} ``` paulson@13348 ` 198` paulson@13348 ` 199` ```(* M_is_recfun :: "[i=>o, i, i, [i,i,i]=>o, i] => o" ``` paulson@13348 ` 200` ``` "M_is_recfun(M,r,a,MH,f) == ``` paulson@13348 ` 201` ``` \z[M]. z \ f <-> ``` paulson@13348 ` 202` ``` 5 4 3 2 1 0 ``` paulson@13348 ` 203` ``` (\x[M]. \y[M]. \xa[M]. \sx[M]. \r_sx[M]. \f_r_sx[M]. ``` paulson@13348 ` 204` ``` pair(M,x,y,z) & pair(M,x,a,xa) & upair(M,x,x,sx) & ``` paulson@13348 ` 205` ``` pre_image(M,r,sx,r_sx) & restriction(M,f,r_sx,f_r_sx) & ``` paulson@13348 ` 206` ``` xa \ r & MH(x, f_r_sx, y))" ``` paulson@13348 ` 207` ```*) ``` paulson@13348 ` 208` paulson@13348 ` 209` ```constdefs is_recfun_fm :: "[[i,i,i]=>i, i, i, i]=>i" ``` paulson@13348 ` 210` ``` "is_recfun_fm(p,r,a,f) == ``` paulson@13348 ` 211` ``` Forall(Iff(Member(0,succ(f)), ``` paulson@13348 ` 212` ``` Exists(Exists(Exists(Exists(Exists(Exists( ``` paulson@13348 ` 213` ``` And(pair_fm(5,4,6), ``` paulson@13348 ` 214` ``` And(pair_fm(5,a#+7,3), ``` paulson@13348 ` 215` ``` And(upair_fm(5,5,2), ``` paulson@13348 ` 216` ``` And(pre_image_fm(r#+7,2,1), ``` paulson@13348 ` 217` ``` And(restriction_fm(f#+7,1,0), ``` paulson@13348 ` 218` ``` And(Member(3,r#+7), p(5,0,4)))))))))))))))" ``` paulson@13348 ` 219` paulson@13348 ` 220` paulson@13348 ` 221` ```lemma is_recfun_type_0: ``` paulson@13348 ` 222` ``` "[| !!x y z. [| x \ nat; y \ nat; z \ nat |] ==> p(x,y,z) \ formula; ``` paulson@13348 ` 223` ``` x \ nat; y \ nat; z \ nat |] ``` paulson@13348 ` 224` ``` ==> is_recfun_fm(p,x,y,z) \ formula" ``` paulson@13348 ` 225` ```apply (unfold is_recfun_fm_def) ``` paulson@13348 ` 226` ```(*FIXME: FIND OUT why simp loops!*) ``` paulson@13348 ` 227` ```apply typecheck ``` paulson@13348 ` 228` ```by simp ``` paulson@13348 ` 229` paulson@13348 ` 230` ```lemma is_recfun_type [TC]: ``` paulson@13348 ` 231` ``` "[| p(5,0,4) \ formula; ``` paulson@13348 ` 232` ``` x \ nat; y \ nat; z \ nat |] ``` paulson@13348 ` 233` ``` ==> is_recfun_fm(p,x,y,z) \ formula" ``` paulson@13348 ` 234` ```by (simp add: is_recfun_fm_def) ``` paulson@13348 ` 235` paulson@13348 ` 236` ```lemma arity_is_recfun_fm [simp]: ``` paulson@13348 ` 237` ``` "[| arity(p(5,0,4)) le 8; x \ nat; y \ nat; z \ nat |] ``` paulson@13348 ` 238` ``` ==> arity(is_recfun_fm(p,x,y,z)) = succ(x) \ succ(y) \ succ(z)" ``` paulson@13348 ` 239` ```apply (frule lt_nat_in_nat, simp) ``` paulson@13348 ` 240` ```apply (simp add: is_recfun_fm_def succ_Un_distrib [symmetric] ) ``` paulson@13348 ` 241` ```apply (subst subset_Un_iff2 [of "arity(p(5,0,4))", THEN iffD1]) ``` paulson@13348 ` 242` ```apply (rule le_imp_subset) ``` paulson@13348 ` 243` ```apply (erule le_trans, simp) ``` paulson@13348 ` 244` ```apply (simp add: succ_Un_distrib [symmetric] Un_ac) ``` paulson@13348 ` 245` ```done ``` paulson@13348 ` 246` paulson@13348 ` 247` ```lemma sats_is_recfun_fm: ``` paulson@13348 ` 248` ``` assumes MH_iff_sats: ``` paulson@13348 ` 249` ``` "!!x y z env. ``` paulson@13348 ` 250` ``` [| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13348 ` 251` ``` ==> MH(nth(x,env), nth(y,env), nth(z,env)) <-> sats(A, p(x,y,z), env)" ``` paulson@13348 ` 252` ``` shows ``` paulson@13348 ` 253` ``` "[|x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13348 ` 254` ``` ==> sats(A, is_recfun_fm(p,x,y,z), env) <-> ``` paulson@13348 ` 255` ``` M_is_recfun(**A, nth(x,env), nth(y,env), MH, nth(z,env))" ``` paulson@13348 ` 256` ```by (simp add: is_recfun_fm_def M_is_recfun_def MH_iff_sats [THEN iff_sym]) ``` paulson@13348 ` 257` paulson@13348 ` 258` ```lemma is_recfun_iff_sats: ``` paulson@13348 ` 259` ``` "[| (!!x y z env. [| x \ nat; y \ nat; z \ nat; env \ list(A)|] ``` paulson@13348 ` 260` ``` ==> MH(nth(x,env), nth(y,env), nth(z,env)) <-> ``` paulson@13348 ` 261` ``` sats(A, p(x,y,z), env)); ``` paulson@13348 ` 262` ``` nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; ``` paulson@13348 ` 263` ``` i \ nat; j \ nat; k \ nat; env \ list(A)|] ``` paulson@13348 ` 264` ``` ==> M_is_recfun(**A, x, y, MH, z) <-> sats(A, is_recfun_fm(p,i,j,k), env)" ``` paulson@13348 ` 265` ```by (simp add: sats_is_recfun_fm [of A MH]) ``` paulson@13348 ` 266` paulson@13348 ` 267` ```theorem is_recfun_reflection: ``` paulson@13348 ` 268` ``` assumes MH_reflection: ``` paulson@13348 ` 269` ``` "!!f g h. REFLECTS[\x. MH(L, f(x), g(x), h(x)), ``` paulson@13348 ` 270` ``` \i x. MH(**Lset(i), f(x), g(x), h(x))]" ``` paulson@13348 ` 271` ``` shows "REFLECTS[\x. M_is_recfun(L, f(x), g(x), MH(L), h(x)), ``` paulson@13348 ` 272` ``` \i x. M_is_recfun(**Lset(i), f(x), g(x), MH(**Lset(i)), h(x))]" ``` paulson@13348 ` 273` ```apply (simp (no_asm_use) only: M_is_recfun_def setclass_simps) ``` paulson@13348 ` 274` ```apply (intro FOL_reflections function_reflections ``` paulson@13348 ` 275` ``` restriction_reflection MH_reflection) ``` paulson@13348 ` 276` ```done ``` paulson@13348 ` 277` paulson@13348 ` 278` ```subsection{*Separation for @{term "wfrank"}*} ``` paulson@13348 ` 279` paulson@13348 ` 280` ```lemma wfrank_Reflects: ``` paulson@13348 ` 281` ``` "REFLECTS[\x. \rplus[L]. tran_closure(L,r,rplus) --> ``` paulson@13348 ` 282` ``` ~ (\f[L]. M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f)), ``` paulson@13348 ` 283` ``` \i x. \rplus \ Lset(i). tran_closure(**Lset(i),r,rplus) --> ``` paulson@13348 ` 284` ``` ~ (\f \ Lset(i). M_is_recfun(**Lset(i), rplus, x, %x f y. is_range(**Lset(i),f,y), f))]" ``` paulson@13348 ` 285` ```by (intro FOL_reflections function_reflections is_recfun_reflection tran_closure_reflection) ``` paulson@13348 ` 286` paulson@13348 ` 287` ```lemma wfrank_separation: ``` paulson@13348 ` 288` ``` "L(r) ==> ``` paulson@13348 ` 289` ``` separation (L, \x. \rplus[L]. tran_closure(L,r,rplus) --> ``` paulson@13348 ` 290` ``` ~ (\f[L]. M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f)))" ``` paulson@13348 ` 291` ```apply (rule separation_CollectI) ``` paulson@13348 ` 292` ```apply (rule_tac A="{r,z}" in subset_LsetE, blast ) ``` paulson@13348 ` 293` ```apply (rule ReflectsE [OF wfrank_Reflects], assumption) ``` paulson@13348 ` 294` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13348 ` 295` ```apply (erule reflection_imp_L_separation) ``` paulson@13348 ` 296` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13348 ` 297` ```apply (rule DPowI2) ``` paulson@13348 ` 298` ```apply (rename_tac u) ``` paulson@13348 ` 299` ```apply (rule ball_iff_sats imp_iff_sats)+ ``` paulson@13348 ` 300` ```apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats) ``` paulson@13348 ` 301` ```apply (rule sep_rules is_recfun_iff_sats | simp)+ ``` paulson@13348 ` 302` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13348 ` 303` ```done ``` paulson@13348 ` 304` paulson@13348 ` 305` paulson@13348 ` 306` ```subsection{*Replacement for @{term "wfrank"}*} ``` paulson@13348 ` 307` paulson@13348 ` 308` ```lemma wfrank_replacement_Reflects: ``` paulson@13348 ` 309` ``` "REFLECTS[\z. \x[L]. x \ A & ``` paulson@13348 ` 310` ``` (\rplus[L]. tran_closure(L,r,rplus) --> ``` paulson@13348 ` 311` ``` (\y[L]. \f[L]. pair(L,x,y,z) & ``` paulson@13348 ` 312` ``` M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f) & ``` paulson@13348 ` 313` ``` is_range(L,f,y))), ``` paulson@13348 ` 314` ``` \i z. \x \ Lset(i). x \ A & ``` paulson@13348 ` 315` ``` (\rplus \ Lset(i). tran_closure(**Lset(i),r,rplus) --> ``` paulson@13348 ` 316` ``` (\y \ Lset(i). \f \ Lset(i). pair(**Lset(i),x,y,z) & ``` paulson@13348 ` 317` ``` M_is_recfun(**Lset(i), rplus, x, %x f y. is_range(**Lset(i),f,y), f) & ``` paulson@13348 ` 318` ``` is_range(**Lset(i),f,y)))]" ``` paulson@13348 ` 319` ```by (intro FOL_reflections function_reflections fun_plus_reflections ``` paulson@13348 ` 320` ``` is_recfun_reflection tran_closure_reflection) ``` paulson@13348 ` 321` paulson@13348 ` 322` paulson@13348 ` 323` ```lemma wfrank_strong_replacement: ``` paulson@13348 ` 324` ``` "L(r) ==> ``` paulson@13348 ` 325` ``` strong_replacement(L, \x z. ``` paulson@13348 ` 326` ``` \rplus[L]. tran_closure(L,r,rplus) --> ``` paulson@13348 ` 327` ``` (\y[L]. \f[L]. pair(L,x,y,z) & ``` paulson@13348 ` 328` ``` M_is_recfun(L, rplus, x, %x f y. is_range(L,f,y), f) & ``` paulson@13348 ` 329` ``` is_range(L,f,y)))" ``` paulson@13348 ` 330` ```apply (rule strong_replacementI) ``` paulson@13348 ` 331` ```apply (rule rallI) ``` paulson@13348 ` 332` ```apply (rename_tac B) ``` paulson@13348 ` 333` ```apply (rule separation_CollectI) ``` paulson@13348 ` 334` ```apply (rule_tac A="{B,r,z}" in subset_LsetE, blast ) ``` paulson@13348 ` 335` ```apply (rule ReflectsE [OF wfrank_replacement_Reflects], assumption) ``` paulson@13348 ` 336` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13348 ` 337` ```apply (erule reflection_imp_L_separation) ``` paulson@13348 ` 338` ``` apply (simp_all add: lt_Ord2) ``` paulson@13348 ` 339` ```apply (rule DPowI2) ``` paulson@13348 ` 340` ```apply (rename_tac u) ``` paulson@13348 ` 341` ```apply (rule bex_iff_sats ball_iff_sats conj_iff_sats)+ ``` paulson@13348 ` 342` ```apply (rule_tac env = "[x,u,B,r]" in mem_iff_sats) ``` paulson@13348 ` 343` ```apply (rule sep_rules tran_closure_iff_sats is_recfun_iff_sats | simp)+ ``` paulson@13348 ` 344` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13348 ` 345` ```done ``` paulson@13348 ` 346` paulson@13348 ` 347` paulson@13348 ` 348` ```subsection{*Separation for @{term "wfrank"}*} ``` paulson@13348 ` 349` paulson@13348 ` 350` ```lemma Ord_wfrank_Reflects: ``` paulson@13348 ` 351` ``` "REFLECTS[\x. \rplus[L]. tran_closure(L,r,rplus) --> ``` paulson@13348 ` 352` ``` ~ (\f[L]. \rangef[L]. ``` paulson@13348 ` 353` ``` is_range(L,f,rangef) --> ``` paulson@13348 ` 354` ``` M_is_recfun(L, rplus, x, \x f y. is_range(L,f,y), f) --> ``` paulson@13348 ` 355` ``` ordinal(L,rangef)), ``` paulson@13348 ` 356` ``` \i x. \rplus \ Lset(i). tran_closure(**Lset(i),r,rplus) --> ``` paulson@13348 ` 357` ``` ~ (\f \ Lset(i). \rangef \ Lset(i). ``` paulson@13348 ` 358` ``` is_range(**Lset(i),f,rangef) --> ``` paulson@13348 ` 359` ``` M_is_recfun(**Lset(i), rplus, x, \x f y. is_range(**Lset(i),f,y), f) --> ``` paulson@13348 ` 360` ``` ordinal(**Lset(i),rangef))]" ``` paulson@13348 ` 361` ```by (intro FOL_reflections function_reflections is_recfun_reflection ``` paulson@13348 ` 362` ``` tran_closure_reflection ordinal_reflection) ``` paulson@13348 ` 363` paulson@13348 ` 364` ```lemma Ord_wfrank_separation: ``` paulson@13348 ` 365` ``` "L(r) ==> ``` paulson@13348 ` 366` ``` separation (L, \x. ``` paulson@13348 ` 367` ``` \rplus[L]. tran_closure(L,r,rplus) --> ``` paulson@13348 ` 368` ``` ~ (\f[L]. \rangef[L]. ``` paulson@13348 ` 369` ``` is_range(L,f,rangef) --> ``` paulson@13348 ` 370` ``` M_is_recfun(L, rplus, x, \x f y. is_range(L,f,y), f) --> ``` paulson@13348 ` 371` ``` ordinal(L,rangef)))" ``` paulson@13348 ` 372` ```apply (rule separation_CollectI) ``` paulson@13348 ` 373` ```apply (rule_tac A="{r,z}" in subset_LsetE, blast ) ``` paulson@13348 ` 374` ```apply (rule ReflectsE [OF Ord_wfrank_Reflects], assumption) ``` paulson@13348 ` 375` ```apply (drule subset_Lset_ltD, assumption) ``` paulson@13348 ` 376` ```apply (erule reflection_imp_L_separation) ``` paulson@13348 ` 377` ``` apply (simp_all add: lt_Ord2, clarify) ``` paulson@13348 ` 378` ```apply (rule DPowI2) ``` paulson@13348 ` 379` ```apply (rename_tac u) ``` paulson@13348 ` 380` ```apply (rule ball_iff_sats imp_iff_sats)+ ``` paulson@13348 ` 381` ```apply (rule_tac env="[rplus,u,r]" in tran_closure_iff_sats) ``` paulson@13348 ` 382` ```apply (rule sep_rules is_recfun_iff_sats | simp)+ ``` paulson@13348 ` 383` ```apply (simp_all add: succ_Un_distrib [symmetric]) ``` paulson@13348 ` 384` ```done ``` paulson@13348 ` 385` paulson@13348 ` 386` paulson@13348 ` 387` ```end ```