# HG changeset patch # User paulson # Date 1026228342 -7200 # Node ID 39d1b3a4c6f41e5ddb96158c94da46431411f878 # Parent 2c287f50c9f3bce91a382f54436a2ab0b4c35813 more and simpler separation proofs diff -r 2c287f50c9f3 -r 39d1b3a4c6f4 src/ZF/Constructible/Separation.thy --- a/src/ZF/Constructible/Separation.thy Tue Jul 09 15:39:44 2002 +0200 +++ b/src/ZF/Constructible/Separation.thy Tue Jul 09 17:25:42 2002 +0200 @@ -2,7 +2,7 @@ (*This theory proves all instances needed for locale M_axioms*) -theory Separation = L_axioms + WFrec: +theory Separation = L_axioms + WF_absolute: text{*Helps us solve for de Bruijn indices!*} lemma nth_ConsI: "[|nth(n,l) = x; n \ nat|] ==> nth(succ(n), Cons(a,l)) = x" @@ -633,56 +633,80 @@ subsection{*Separation for Reflexive/Transitive Closure*} -lemma rtrancl_reflects: - "REFLECTS[\p. - \nnat[L]. \n[L]. \n'[L]. omega(L,nnat) & n\nnat & successor(L,n,n') & - (\f[L]. - typed_function(L,n',A,f) & - (\x[L]. \y[L]. \zero[L]. pair(L,x,y,p) & empty(L,zero) & - fun_apply(L,f,zero,x) & fun_apply(L,f,n,y)) & - (\j[L]. j\n --> - (\fj[L]. \sj[L]. \fsj[L]. \ffp[L]. - fun_apply(L,f,j,fj) & successor(L,j,sj) & - fun_apply(L,f,sj,fsj) & pair(L,fj,fsj,ffp) & ffp \ r))), -\i p. - \nnat \ Lset(i). \n \ Lset(i). \n' \ Lset(i). - omega(**Lset(i),nnat) & n\nnat & successor(**Lset(i),n,n') & - (\f \ Lset(i). - typed_function(**Lset(i),n',A,f) & - (\x \ Lset(i). \y \ Lset(i). \zero \ Lset(i). pair(**Lset(i),x,y,p) & empty(**Lset(i),zero) & - fun_apply(**Lset(i),f,zero,x) & fun_apply(**Lset(i),f,n,y)) & - (\j \ Lset(i). j\n --> - (\fj \ Lset(i). \sj \ Lset(i). \fsj \ Lset(i). \ffp \ Lset(i). - fun_apply(**Lset(i),f,j,fj) & successor(**Lset(i),j,sj) & - fun_apply(**Lset(i),f,sj,fsj) & pair(**Lset(i),fj,fsj,ffp) & ffp \ r)))]" -by (intro FOL_reflections function_reflections fun_plus_reflections) +subsubsection{*First, The Defining Formula*} + +(* "rtran_closure_mem(M,A,r,p) == + \nnat[M]. \n[M]. \n'[M]. + omega(M,nnat) & n\nnat & successor(M,n,n') & + (\f[M]. typed_function(M,n',A,f) & + (\x[M]. \y[M]. \zero[M]. pair(M,x,y,p) & empty(M,zero) & + fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) & + (\j[M]. j\n --> + (\fj[M]. \sj[M]. \fsj[M]. \ffp[M]. + fun_apply(M,f,j,fj) & successor(M,j,sj) & + fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \ r)))"*) +constdefs rtran_closure_mem_fm :: "[i,i,i]=>i" + "rtran_closure_mem_fm(A,r,p) == + Exists(Exists(Exists( + And(omega_fm(2), + And(Member(1,2), + And(succ_fm(1,0), + Exists(And(typed_function_fm(1, A#+4, 0), + And(Exists(Exists(Exists( + And(pair_fm(2,1,p#+7), + And(empty_fm(0), + And(fun_apply_fm(3,0,2), fun_apply_fm(3,5,1))))))), + Forall(Implies(Member(0,3), + Exists(Exists(Exists(Exists( + And(fun_apply_fm(5,4,3), + And(succ_fm(4,2), + And(fun_apply_fm(5,2,1), + And(pair_fm(3,1,0), Member(0,r#+9))))))))))))))))))))" + + +lemma rtran_closure_mem_type [TC]: + "[| x \ nat; y \ nat; z \ nat |] ==> rtran_closure_mem_fm(x,y,z) \ formula" +by (simp add: rtran_closure_mem_fm_def) + +lemma arity_rtran_closure_mem_fm [simp]: + "[| x \ nat; y \ nat; z \ nat |] + ==> arity(rtran_closure_mem_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" +by (simp add: rtran_closure_mem_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_rtran_closure_mem_fm [simp]: + "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> sats(A, rtran_closure_mem_fm(x,y,z), env) <-> + rtran_closure_mem(**A, nth(x,env), nth(y,env), nth(z,env))" +by (simp add: rtran_closure_mem_fm_def rtran_closure_mem_def) + +lemma rtran_closure_mem_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j \ nat; k \ nat; env \ list(A)|] + ==> rtran_closure_mem(**A, x, y, z) <-> sats(A, rtran_closure_mem_fm(i,j,k), env)" +by (simp add: sats_rtran_closure_mem_fm) + +theorem rtran_closure_mem_reflection: + "REFLECTS[\x. rtran_closure_mem(L,f(x),g(x),h(x)), + \i x. rtran_closure_mem(**Lset(i),f(x),g(x),h(x))]" +apply (simp only: rtran_closure_mem_def setclass_simps) +apply (intro FOL_reflections function_reflections fun_plus_reflections) +done + +subsubsection{*Then, the Instance of Separation*} text{*This formula describes @{term "rtrancl(r)"}.*} lemma rtrancl_separation: - "[| L(r); L(A) |] ==> - separation (L, \p. - \nnat[L]. \n[L]. \n'[L]. - omega(L,nnat) & n\nnat & successor(L,n,n') & - (\f[L]. - typed_function(L,n',A,f) & - (\x[L]. \y[L]. \zero[L]. pair(L,x,y,p) & empty(L,zero) & - fun_apply(L,f,zero,x) & fun_apply(L,f,n,y)) & - (\j[L]. j\n --> - (\fj[L]. \sj[L]. \fsj[L]. \ffp[L]. - fun_apply(L,f,j,fj) & successor(L,j,sj) & - fun_apply(L,f,sj,fsj) & pair(L,fj,fsj,ffp) & ffp \ r))))" + "[| L(r); L(A) |] ==> separation (L, rtran_closure_mem(L,A,r))" apply (rule separation_CollectI) apply (rule_tac A="{r,A,z}" in subset_LsetE, blast ) -apply (rule ReflectsE [OF rtrancl_reflects], assumption) +apply (rule ReflectsE [OF rtran_closure_mem_reflection], assumption) apply (drule subset_Lset_ltD, assumption) apply (erule reflection_imp_L_separation) apply (simp_all add: lt_Ord2) apply (rule DPowI2) -apply (rename_tac u) -apply (rule bex_iff_sats conj_iff_sats)+ -apply (rule_tac env = "[x,u,r,A]" in omega_iff_sats) -txt{*SLOW, maybe just due to the formula's size*} +apply (rename_tac u) +apply (rule_tac env = "[u,r,A]" in rtran_closure_mem_iff_sats) apply (rule sep_rules | simp)+ apply (simp_all add: succ_Un_distrib [symmetric]) done diff -r 2c287f50c9f3 -r 39d1b3a4c6f4 src/ZF/Constructible/WF_absolute.thy --- a/src/ZF/Constructible/WF_absolute.thy Tue Jul 09 15:39:44 2002 +0200 +++ b/src/ZF/Constructible/WF_absolute.thy Tue Jul 09 17:25:42 2002 +0200 @@ -111,41 +111,43 @@ constdefs + rtran_closure_mem :: "[i=>o,i,i,i] => o" + --{*The property of belonging to @{text "rtran_closure(r)"}*} + "rtran_closure_mem(M,A,r,p) == + \nnat[M]. \n[M]. \n'[M]. + omega(M,nnat) & n\nnat & successor(M,n,n') & + (\f[M]. typed_function(M,n',A,f) & + (\x[M]. \y[M]. \zero[M]. pair(M,x,y,p) & empty(M,zero) & + fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) & + (\j[M]. j\n --> + (\fj[M]. \sj[M]. \fsj[M]. \ffp[M]. + fun_apply(M,f,j,fj) & successor(M,j,sj) & + fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \ r)))" + rtran_closure :: "[i=>o,i,i] => o" - "rtran_closure(M,r,s) == - \A. M(A) --> is_field(M,r,A) --> - (\p. M(p) --> - (p \ s <-> - (\n\nat. M(n) & - (\n'. M(n') & successor(M,n,n') & - (\f. M(f) & typed_function(M,n',A,f) & - (\x\A. M(x) & (\y\A. M(y) & pair(M,x,y,p) & - fun_apply(M,f,0,x) & fun_apply(M,f,n,y))) & - (\i\n. M(i) --> - (\i'. M(i') --> successor(M,i,i') --> - (\fi. M(fi) --> fun_apply(M,f,i,fi) --> - (\fi'. M(fi') --> fun_apply(M,f,i',fi') --> - (\q. M(q) --> pair(M,fi,fi',q) --> q \ r))))))))))" + "rtran_closure(M,r,s) == + \A[M]. is_field(M,r,A) --> + (\p[M]. p \ s <-> rtran_closure_mem(M,A,r,p))" tran_closure :: "[i=>o,i,i] => o" "tran_closure(M,r,t) == \s[M]. rtran_closure(M,r,s) & composition(M,r,s,t)" +lemma (in M_axioms) rtran_closure_mem_iff: + "[|M(A); M(r); M(p)|] + ==> rtran_closure_mem(M,A,r,p) <-> + (\n[M]. n\nat & + (\f[M]. f \ succ(n) -> A & + (\x[M]. \y[M]. p = & f`0 = x & f`n = y) & + (\i\n. \ r)))" +apply (simp add: rtran_closure_mem_def typed_apply_abs + Ord_succ_mem_iff nat_0_le [THEN ltD]) +apply (blast intro: elim:); +done locale M_trancl = M_axioms + assumes rtrancl_separation: - "[| M(r); M(A) |] ==> - separation (M, \p. - \nnat[M]. \n[M]. \n'[M]. - omega(M,nnat) & n\nnat & successor(M,n,n') & - (\f[M]. - typed_function(M,n',A,f) & - (\x[M]. \y[M]. \zero[M]. pair(M,x,y,p) & empty(M,zero) & - fun_apply(M,f,zero,x) & fun_apply(M,f,n,y)) & - (\j[M]. j\n --> - (\fj[M]. \sj[M]. \fsj[M]. \ffp[M]. - fun_apply(M,f,j,fj) & successor(M,j,sj) & - fun_apply(M,f,sj,fsj) & pair(M,fj,fsj,ffp) & ffp \ r))))" + "[| M(r); M(A) |] ==> separation (M, rtran_closure_mem(M,A,r))" and wellfounded_trancl_separation: "[| M(r); M(Z) |] ==> separation (M, \x. @@ -155,29 +157,16 @@ lemma (in M_trancl) rtran_closure_rtrancl: "M(r) ==> rtran_closure(M,r,rtrancl(r))" -apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric] - rtrancl_alt_def field_closed typed_apply_abs apply_closed - Ord_succ_mem_iff M_nat nat_0_le [THEN ltD], clarify) -apply (rule iffI) - apply clarify - apply simp - apply (rename_tac n f) - apply (rule_tac x=n in bexI) - apply (rule_tac x=f in exI) - apply simp - apply (blast dest: finite_fun_closed dest: transM) - apply assumption -apply clarify -apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast) +apply (simp add: rtran_closure_def rtran_closure_mem_iff + rtrancl_alt_eq_rtrancl [symmetric] rtrancl_alt_def) +apply (auto simp add: nat_0_le [THEN ltD] apply_funtype); done lemma (in M_trancl) rtrancl_closed [intro,simp]: "M(r) ==> M(rtrancl(r))" apply (insert rtrancl_separation [of r "field(r)"]) apply (simp add: rtrancl_alt_eq_rtrancl [symmetric] - rtrancl_alt_def field_closed typed_apply_abs apply_closed - Ord_succ_mem_iff M_nat nat_into_M - nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype) + rtrancl_alt_def rtran_closure_mem_iff) done lemma (in M_trancl) rtrancl_abs [simp]: @@ -187,20 +176,10 @@ prefer 2 apply (blast intro: rtran_closure_rtrancl) apply (rule M_equalityI) apply (simp add: rtran_closure_def rtrancl_alt_eq_rtrancl [symmetric] - rtrancl_alt_def field_closed typed_apply_abs apply_closed - Ord_succ_mem_iff M_nat - nat_0_le [THEN ltD] leI [THEN ltD] ltI apply_funtype) - prefer 2 apply assumption - prefer 2 apply blast -apply (rule iffI, clarify) -apply (simp add: nat_0_le [THEN ltD] apply_funtype, blast, clarify, simp) - apply (rename_tac n f) - apply (rule_tac x=n in bexI) - apply (rule_tac x=f in exI) - apply (blast dest!: finite_fun_closed, assumption) + rtrancl_alt_def rtran_closure_mem_iff) +apply (auto simp add: nat_0_le [THEN ltD] apply_funtype); done - lemma (in M_trancl) trancl_closed [intro,simp]: "M(r) ==> M(trancl(r))" by (simp add: trancl_def comp_closed rtrancl_closed)