# HG changeset patch # User paulson # Date 1026221984 -7200 # Node ID 2c287f50c9f3bce91a382f54436a2ab0b4c35813 # Parent 3323ecc0b97c1eb30ac550f12ad6ae13364a1c89 More relativization, reflection and proofs of separation diff -r 3323ecc0b97c -r 2c287f50c9f3 src/ZF/Constructible/L_axioms.thy --- a/src/ZF/Constructible/L_axioms.thy Tue Jul 09 13:41:38 2002 +0200 +++ b/src/ZF/Constructible/L_axioms.thy Tue Jul 09 15:39:44 2002 +0200 @@ -292,7 +292,7 @@ apply (intro Imp_reflection All_reflection, assumption) done -lemmas FOL_reflection = +lemmas FOL_reflections = Triv_reflection Not_reflection And_reflection Or_reflection Imp_reflection Iff_reflection Ex_reflection All_reflection Rex_reflection Rall_reflection @@ -340,6 +340,39 @@ "8" == "succ(7)" "9" == "succ(8)" + +subsubsection{*The Empty Set*} + +constdefs empty_fm :: "i=>i" + "empty_fm(x) == Forall(Neg(Member(0,succ(x))))" + +lemma empty_type [TC]: + "x \ nat ==> empty_fm(x) \ formula" +by (simp add: empty_fm_def) + +lemma arity_empty_fm [simp]: + "x \ nat ==> arity(empty_fm(x)) = succ(x)" +by (simp add: empty_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_empty_fm [simp]: + "[| x \ nat; env \ list(A)|] + ==> sats(A, empty_fm(x), env) <-> empty(**A, nth(x,env))" +by (simp add: empty_fm_def empty_def) + +lemma empty_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; env \ list(A)|] + ==> empty(**A, x) <-> sats(A, empty_fm(i), env)" +by simp + +theorem empty_reflection: + "REFLECTS[\x. empty(L,f(x)), + \i x. empty(**Lset(i),f(x))]" +apply (simp only: empty_def setclass_simps) +apply (intro FOL_reflections) +done + + subsubsection{*Unordered pairs*} constdefs upair_fm :: "[i,i,i]=>i" @@ -384,7 +417,7 @@ "REFLECTS[\x. upair(L,f(x),g(x),h(x)), \i x. upair(**Lset(i),f(x),g(x),h(x))]" apply (simp add: upair_def) -apply (intro FOL_reflection) +apply (intro FOL_reflections) done subsubsection{*Ordered pairs*} @@ -420,7 +453,7 @@ "REFLECTS[\x. pair(L,f(x),g(x),h(x)), \i x. pair(**Lset(i),f(x),g(x),h(x))]" apply (simp only: pair_def setclass_simps) -apply (intro FOL_reflection upair_reflection) +apply (intro FOL_reflections upair_reflection) done @@ -456,7 +489,7 @@ "REFLECTS[\x. union(L,f(x),g(x),h(x)), \i x. union(**Lset(i),f(x),g(x),h(x))]" apply (simp only: union_def setclass_simps) -apply (intro FOL_reflection) +apply (intro FOL_reflections) done @@ -493,7 +526,41 @@ "REFLECTS[\x. is_cons(L,f(x),g(x),h(x)), \i x. is_cons(**Lset(i),f(x),g(x),h(x))]" apply (simp only: is_cons_def setclass_simps) -apply (intro FOL_reflection upair_reflection union_reflection) +apply (intro FOL_reflections upair_reflection union_reflection) +done + + +subsubsection{*Successor Function*} + +constdefs succ_fm :: "[i,i]=>i" + "succ_fm(x,y) == cons_fm(x,x,y)" + +lemma succ_type [TC]: + "[| x \ nat; y \ nat |] ==> succ_fm(x,y) \ formula" +by (simp add: succ_fm_def) + +lemma arity_succ_fm [simp]: + "[| x \ nat; y \ nat |] + ==> arity(succ_fm(x,y)) = succ(x) \ succ(y)" +by (simp add: succ_fm_def) + +lemma sats_succ_fm [simp]: + "[| x \ nat; y \ nat; env \ list(A)|] + ==> sats(A, succ_fm(x,y), env) <-> + successor(**A, nth(x,env), nth(y,env))" +by (simp add: succ_fm_def successor_def) + +lemma successor_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; j \ nat; env \ list(A)|] + ==> successor(**A, x, y) <-> sats(A, succ_fm(i,j), env)" +by simp + +theorem successor_reflection: + "REFLECTS[\x. successor(L,f(x),g(x)), + \i x. successor(**Lset(i),f(x),g(x))]" +apply (simp only: successor_def setclass_simps) +apply (intro cons_reflection) done @@ -530,7 +597,7 @@ "REFLECTS[\x. fun_apply(L,f(x),g(x),h(x)), \i x. fun_apply(**Lset(i),f(x),g(x),h(x))]" apply (simp only: fun_apply_def setclass_simps) -apply (intro FOL_reflection pair_reflection) +apply (intro FOL_reflections pair_reflection) done @@ -542,13 +609,13 @@ lemma sats_subset_fm': "[|x \ nat; y \ nat; env \ list(A)|] ==> sats(A, subset_fm(x,y), env) <-> subset(**A, nth(x,env), nth(y,env))" -by (simp add: subset_fm_def subset_def) +by (simp add: subset_fm_def Relative.subset_def) theorem subset_reflection: "REFLECTS[\x. subset(L,f(x),g(x)), \i x. subset(**Lset(i),f(x),g(x))]" -apply (simp only: subset_def setclass_simps) -apply (intro FOL_reflection) +apply (simp only: Relative.subset_def setclass_simps) +apply (intro FOL_reflections) done lemma sats_transset_fm': @@ -560,7 +627,7 @@ "REFLECTS[\x. transitive_set(L,f(x)), \i x. transitive_set(**Lset(i),f(x))]" apply (simp only: transitive_set_def setclass_simps) -apply (intro FOL_reflection subset_reflection) +apply (intro FOL_reflections subset_reflection) done lemma sats_ordinal_fm': @@ -576,7 +643,7 @@ theorem ordinal_reflection: "REFLECTS[\x. ordinal(L,f(x)), \i x. ordinal(**Lset(i),f(x))]" apply (simp only: ordinal_def setclass_simps) -apply (intro FOL_reflection transitive_set_reflection) +apply (intro FOL_reflections transitive_set_reflection) done @@ -615,7 +682,7 @@ "REFLECTS[\x. membership(L,f(x),g(x)), \i x. membership(**Lset(i),f(x),g(x))]" apply (simp only: membership_def setclass_simps) -apply (intro FOL_reflection pair_reflection) +apply (intro FOL_reflections pair_reflection) done subsubsection{*Predecessor Set*} @@ -654,7 +721,7 @@ "REFLECTS[\x. pred_set(L,f(x),g(x),h(x),b(x)), \i x. pred_set(**Lset(i),f(x),g(x),h(x),b(x))]" apply (simp only: pred_set_def setclass_simps) -apply (intro FOL_reflection pair_reflection) +apply (intro FOL_reflections pair_reflection) done @@ -694,7 +761,7 @@ "REFLECTS[\x. is_domain(L,f(x),g(x)), \i x. is_domain(**Lset(i),f(x),g(x))]" apply (simp only: is_domain_def setclass_simps) -apply (intro FOL_reflection pair_reflection) +apply (intro FOL_reflections pair_reflection) done @@ -733,10 +800,51 @@ "REFLECTS[\x. is_range(L,f(x),g(x)), \i x. is_range(**Lset(i),f(x),g(x))]" apply (simp only: is_range_def setclass_simps) -apply (intro FOL_reflection pair_reflection) +apply (intro FOL_reflections pair_reflection) done +subsubsection{*Field*} + +(* "is_field(M,r,z) == + \dr[M]. is_domain(M,r,dr) & + (\rr[M]. is_range(M,r,rr) & union(M,dr,rr,z))" *) +constdefs field_fm :: "[i,i]=>i" + "field_fm(r,z) == + Exists(And(domain_fm(succ(r),0), + Exists(And(range_fm(succ(succ(r)),0), + union_fm(1,0,succ(succ(z)))))))" + +lemma field_type [TC]: + "[| x \ nat; y \ nat |] ==> field_fm(x,y) \ formula" +by (simp add: field_fm_def) + +lemma arity_field_fm [simp]: + "[| x \ nat; y \ nat |] + ==> arity(field_fm(x,y)) = succ(x) \ succ(y)" +by (simp add: field_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_field_fm [simp]: + "[| x \ nat; y \ nat; env \ list(A)|] + ==> sats(A, field_fm(x,y), env) <-> + is_field(**A, nth(x,env), nth(y,env))" +by (simp add: field_fm_def is_field_def) + +lemma field_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; j \ nat; env \ list(A)|] + ==> is_field(**A, x, y) <-> sats(A, field_fm(i,j), env)" +by simp + +theorem field_reflection: + "REFLECTS[\x. is_field(L,f(x),g(x)), + \i x. is_field(**Lset(i),f(x),g(x))]" +apply (simp only: is_field_def setclass_simps) +apply (intro FOL_reflections domain_reflection range_reflection + union_reflection) +done + + subsubsection{*Image*} (* "image(M,r,A,z) == @@ -761,7 +869,7 @@ "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] ==> sats(A, image_fm(x,y,z), env) <-> image(**A, nth(x,env), nth(y,env), nth(z,env))" -by (simp add: image_fm_def image_def) +by (simp add: image_fm_def Relative.image_def) lemma image_iff_sats: "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; @@ -772,8 +880,8 @@ theorem image_reflection: "REFLECTS[\x. image(L,f(x),g(x),h(x)), \i x. image(**Lset(i),f(x),g(x),h(x))]" -apply (simp only: image_def setclass_simps) -apply (intro FOL_reflection pair_reflection) +apply (simp only: Relative.image_def setclass_simps) +apply (intro FOL_reflections pair_reflection) done @@ -808,7 +916,7 @@ "REFLECTS[\x. is_relation(L,f(x)), \i x. is_relation(**Lset(i),f(x))]" apply (simp only: is_relation_def setclass_simps) -apply (intro FOL_reflection pair_reflection) +apply (intro FOL_reflections pair_reflection) done @@ -848,7 +956,7 @@ "REFLECTS[\x. is_function(L,f(x)), \i x. is_function(**Lset(i),f(x))]" apply (simp only: is_function_def setclass_simps) -apply (intro FOL_reflection pair_reflection) +apply (intro FOL_reflections pair_reflection) done @@ -887,19 +995,74 @@ ==> typed_function(**A, x, y, z) <-> sats(A, typed_function_fm(i,j,k), env)" by simp -lemmas function_reflection = - upair_reflection pair_reflection union_reflection - cons_reflection fun_apply_reflection subset_reflection - transitive_set_reflection ordinal_reflection membership_reflection - pred_set_reflection domain_reflection range_reflection image_reflection +lemmas function_reflections = + empty_reflection upair_reflection pair_reflection union_reflection + cons_reflection successor_reflection + fun_apply_reflection subset_reflection + transitive_set_reflection membership_reflection + pred_set_reflection domain_reflection range_reflection field_reflection + image_reflection is_relation_reflection is_function_reflection +lemmas function_iff_sats = + empty_iff_sats upair_iff_sats pair_iff_sats union_iff_sats + cons_iff_sats successor_iff_sats + fun_apply_iff_sats Memrel_iff_sats + pred_set_iff_sats domain_iff_sats range_iff_sats field_iff_sats + image_iff_sats + relation_iff_sats function_iff_sats + theorem typed_function_reflection: "REFLECTS[\x. typed_function(L,f(x),g(x),h(x)), \i x. typed_function(**Lset(i),f(x),g(x),h(x))]" apply (simp only: typed_function_def setclass_simps) -apply (intro FOL_reflection function_reflection) +apply (intro FOL_reflections function_reflections) +done + + +subsubsection{*Composition of Relations*} + +(* "composition(M,r,s,t) == + \p[M]. p \ t <-> + (\x[M]. \y[M]. \z[M]. \xy[M]. \yz[M]. + pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & + xy \ s & yz \ r)" *) +constdefs composition_fm :: "[i,i,i]=>i" + "composition_fm(r,s,t) == + Forall(Iff(Member(0,succ(t)), + Exists(Exists(Exists(Exists(Exists( + And(pair_fm(4,2,5), + And(pair_fm(4,3,1), + And(pair_fm(3,2,0), + And(Member(1,s#+6), Member(0,r#+6))))))))))))" + +lemma composition_type [TC]: + "[| x \ nat; y \ nat; z \ nat |] ==> composition_fm(x,y,z) \ formula" +by (simp add: composition_fm_def) + +lemma arity_composition_fm [simp]: + "[| x \ nat; y \ nat; z \ nat |] + ==> arity(composition_fm(x,y,z)) = succ(x) \ succ(y) \ succ(z)" +by (simp add: composition_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_composition_fm [simp]: + "[| x \ nat; y \ nat; z \ nat; env \ list(A)|] + ==> sats(A, composition_fm(x,y,z), env) <-> + composition(**A, nth(x,env), nth(y,env), nth(z,env))" +by (simp add: composition_fm_def composition_def) + +lemma composition_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z; + i \ nat; j \ nat; k \ nat; env \ list(A)|] + ==> composition(**A, x, y, z) <-> sats(A, composition_fm(i,j,k), env)" +by simp + +theorem composition_reflection: + "REFLECTS[\x. composition(L,f(x),g(x),h(x)), + \i x. composition(**Lset(i),f(x),g(x),h(x))]" +apply (simp only: composition_def setclass_simps) +apply (intro FOL_reflections pair_reflection) done @@ -944,7 +1107,7 @@ "REFLECTS[\x. injection(L,f(x),g(x),h(x)), \i x. injection(**Lset(i),f(x),g(x),h(x))]" apply (simp only: injection_def setclass_simps) -apply (intro FOL_reflection function_reflection typed_function_reflection) +apply (intro FOL_reflections function_reflections typed_function_reflection) done @@ -986,7 +1149,7 @@ "REFLECTS[\x. surjection(L,f(x),g(x),h(x)), \i x. surjection(**Lset(i),f(x),g(x),h(x))]" apply (simp only: surjection_def setclass_simps) -apply (intro FOL_reflection function_reflection typed_function_reflection) +apply (intro FOL_reflections function_reflections typed_function_reflection) done @@ -1080,18 +1243,98 @@ "REFLECTS[\x. order_isomorphism(L,f(x),g(x),h(x),g'(x),h'(x)), \i x. order_isomorphism(**Lset(i),f(x),g(x),h(x),g'(x),h'(x))]" apply (simp only: order_isomorphism_def setclass_simps) -apply (intro FOL_reflection function_reflection bijection_reflection) +apply (intro FOL_reflections function_reflections bijection_reflection) +done + +subsubsection{*Limit Ordinals*} + +text{*A limit ordinal is a non-empty, successor-closed ordinal*} + +(* "limit_ordinal(M,a) == + ordinal(M,a) & ~ empty(M,a) & + (\x[M]. x\a --> (\y[M]. y\a & successor(M,x,y)))" *) + +constdefs limit_ordinal_fm :: "i=>i" + "limit_ordinal_fm(x) == + And(ordinal_fm(x), + And(Neg(empty_fm(x)), + Forall(Implies(Member(0,succ(x)), + Exists(And(Member(0,succ(succ(x))), + succ_fm(1,0)))))))" + +lemma limit_ordinal_type [TC]: + "x \ nat ==> limit_ordinal_fm(x) \ formula" +by (simp add: limit_ordinal_fm_def) + +lemma arity_limit_ordinal_fm [simp]: + "x \ nat ==> arity(limit_ordinal_fm(x)) = succ(x)" +by (simp add: limit_ordinal_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_limit_ordinal_fm [simp]: + "[| x \ nat; env \ list(A)|] + ==> sats(A, limit_ordinal_fm(x), env) <-> limit_ordinal(**A, nth(x,env))" +by (simp add: limit_ordinal_fm_def limit_ordinal_def sats_ordinal_fm') + +lemma limit_ordinal_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; env \ list(A)|] + ==> limit_ordinal(**A, x) <-> sats(A, limit_ordinal_fm(i), env)" +by simp + +theorem limit_ordinal_reflection: + "REFLECTS[\x. limit_ordinal(L,f(x)), + \i x. limit_ordinal(**Lset(i),f(x))]" +apply (simp only: limit_ordinal_def setclass_simps) +apply (intro FOL_reflections ordinal_reflection + empty_reflection successor_reflection) done -lemmas fun_plus_reflection = - typed_function_reflection injection_reflection surjection_reflection - bijection_reflection order_isomorphism_reflection +subsubsection{*Omega: The Set of Natural Numbers*} + +(* omega(M,a) == limit_ordinal(M,a) & (\x[M]. x\a --> ~ limit_ordinal(M,x)) *) +constdefs omega_fm :: "i=>i" + "omega_fm(x) == + And(limit_ordinal_fm(x), + Forall(Implies(Member(0,succ(x)), + Neg(limit_ordinal_fm(0)))))" + +lemma omega_type [TC]: + "x \ nat ==> omega_fm(x) \ formula" +by (simp add: omega_fm_def) + +lemma arity_omega_fm [simp]: + "x \ nat ==> arity(omega_fm(x)) = succ(x)" +by (simp add: omega_fm_def succ_Un_distrib [symmetric] Un_ac) + +lemma sats_omega_fm [simp]: + "[| x \ nat; env \ list(A)|] + ==> sats(A, omega_fm(x), env) <-> omega(**A, nth(x,env))" +by (simp add: omega_fm_def omega_def) -lemmas fun_plus_iff_sats = upair_iff_sats pair_iff_sats union_iff_sats - cons_iff_sats fun_apply_iff_sats ordinal_iff_sats Memrel_iff_sats - pred_set_iff_sats domain_iff_sats range_iff_sats image_iff_sats - relation_iff_sats function_iff_sats typed_function_iff_sats +lemma omega_iff_sats: + "[| nth(i,env) = x; nth(j,env) = y; + i \ nat; env \ list(A)|] + ==> omega(**A, x) <-> sats(A, omega_fm(i), env)" +by simp + +theorem omega_reflection: + "REFLECTS[\x. omega(L,f(x)), + \i x. omega(**Lset(i),f(x))]" +apply (simp only: omega_def setclass_simps) +apply (intro FOL_reflections limit_ordinal_reflection) +done + + +lemmas fun_plus_reflections = + typed_function_reflection composition_reflection + injection_reflection surjection_reflection + bijection_reflection order_isomorphism_reflection + ordinal_reflection limit_ordinal_reflection omega_reflection + +lemmas fun_plus_iff_sats = + typed_function_iff_sats composition_iff_sats injection_iff_sats surjection_iff_sats bijection_iff_sats order_isomorphism_iff_sats + ordinal_iff_sats limit_ordinal_iff_sats omega_iff_sats end diff -r 3323ecc0b97c -r 2c287f50c9f3 src/ZF/Constructible/ROOT.ML --- a/src/ZF/Constructible/ROOT.ML Tue Jul 09 13:41:38 2002 +0200 +++ b/src/ZF/Constructible/ROOT.ML Tue Jul 09 15:39:44 2002 +0200 @@ -4,6 +4,8 @@ Copyright 2002 University of Cambridge Inner Models and Absoluteness + +Build using isatool usedir -d pdf ZF Constructible *) use_thy "Reflection"; diff -r 3323ecc0b97c -r 2c287f50c9f3 src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Tue Jul 09 13:41:38 2002 +0200 +++ b/src/ZF/Constructible/Relative.thy Tue Jul 09 15:39:44 2002 +0200 @@ -104,8 +104,9 @@ composition :: "[i=>o,i,i,i] => o" "composition(M,r,s,t) == \p[M]. p \ t <-> - (\x[M]. \y[M]. \z[M]. pair(M,x,z,p) & \x,y\ \ s & \y,z\ \ r)" - + (\x[M]. \y[M]. \z[M]. \xy[M]. \yz[M]. + pair(M,x,z,p) & pair(M,x,y,xy) & pair(M,y,z,yz) & + xy \ s & yz \ r)" injection :: "[i=>o,i,i,i] => o" "injection(M,A,B,f) == diff -r 3323ecc0b97c -r 2c287f50c9f3 src/ZF/Constructible/Separation.thy --- a/src/ZF/Constructible/Separation.thy Tue Jul 09 13:41:38 2002 +0200 +++ b/src/ZF/Constructible/Separation.thy Tue Jul 09 15:39:44 2002 +0200 @@ -1,13 +1,16 @@ -header{*Proving instances of Separation using Reflection!*} +header{*Some Instances of Separation and Strong Replacement*} -theory Separation = L_axioms: +(*This theory proves all instances needed for locale M_axioms*) + +theory Separation = L_axioms + WFrec: text{*Helps us solve for de Bruijn indices!*} lemma nth_ConsI: "[|nth(n,l) = x; n \ nat|] ==> nth(succ(n), Cons(a,l)) = x" by simp lemmas nth_rules = nth_0 nth_ConsI nat_0I nat_succI -lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats fun_plus_iff_sats +lemmas sep_rules = nth_0 nth_ConsI FOL_iff_sats function_iff_sats + fun_plus_iff_sats lemma Collect_conj_in_DPow: "[| {x\A. P(x)} \ DPow(A); {x\A. Q(x)} \ DPow(A) |] @@ -48,7 +51,7 @@ lemma Inter_Reflects: "REFLECTS[\x. \y[L]. y\A --> x \ y, \i x. \y\Lset(i). y\A --> x \ y]" -by (intro FOL_reflection) +by (intro FOL_reflections) lemma Inter_separation: "L(A) ==> separation(L, \x. \y[L]. y\A --> x\y)" @@ -68,11 +71,11 @@ subsection{*Separation for Cartesian Product*} -lemma cartprod_Reflects [simplified]: +lemma cartprod_Reflects: "REFLECTS[\z. \x[L]. x\A & (\y[L]. y\B & pair(L,x,y,z)), \i z. \x\Lset(i). x\A & (\y\Lset(i). y\B & pair(**Lset(i),x,y,z))]" -by (intro FOL_reflection function_reflection) +by (intro FOL_reflections function_reflections) lemma cartprod_separation: "[| L(A); L(B) |] @@ -94,13 +97,10 @@ subsection{*Separation for Image*} -text{*No @{text simplified} here: it simplifies the occurrence of - the predicate @{term pair}!*} lemma image_Reflects: "REFLECTS[\y. \p[L]. p\r & (\x[L]. x\A & pair(L,x,y,p)), \i y. \p\Lset(i). p\r & (\x\Lset(i). x\A & pair(**Lset(i),x,y,p))]" -by (intro FOL_reflection function_reflection) - +by (intro FOL_reflections function_reflections) lemma image_separation: "[| L(A); L(r) |] @@ -126,7 +126,7 @@ "REFLECTS[\z. \p[L]. p\r & (\x[L]. \y[L]. pair(L,x,y,p) & pair(L,y,x,z)), \i z. \p\Lset(i). p\r & (\x\Lset(i). \y\Lset(i). pair(**Lset(i),x,y,p) & pair(**Lset(i),y,x,z))]" -by (intro FOL_reflection function_reflection) +by (intro FOL_reflections function_reflections) lemma converse_separation: "L(r) ==> separation(L, @@ -152,7 +152,7 @@ lemma restrict_Reflects: "REFLECTS[\z. \x[L]. x\A & (\y[L]. pair(L,x,y,z)), \i z. \x\Lset(i). x\A & (\y\Lset(i). pair(**Lset(i),x,y,z))]" -by (intro FOL_reflection function_reflection) +by (intro FOL_reflections function_reflections) lemma restrict_separation: "L(A) ==> separation(L, \z. \x[L]. x\A & (\y[L]. pair(L,x,y,z)))" @@ -181,7 +181,7 @@ \i xz. \x\Lset(i). \y\Lset(i). \z\Lset(i). \xy\Lset(i). \yz\Lset(i). pair(**Lset(i),x,z,xz) & pair(**Lset(i),x,y,xy) & pair(**Lset(i),y,z,yz) & xy\s & yz\r]" -by (intro FOL_reflection function_reflection) +by (intro FOL_reflections function_reflections) lemma comp_separation: "[| L(r); L(s) |] @@ -209,7 +209,7 @@ lemma pred_Reflects: "REFLECTS[\y. \p[L]. p\r & pair(L,y,x,p), \i y. \p \ Lset(i). p\r & pair(**Lset(i),y,x,p)]" -by (intro FOL_reflection function_reflection) +by (intro FOL_reflections function_reflections) lemma pred_separation: "[| L(r); L(x) |] ==> separation(L, \y. \p[L]. p\r & pair(L,y,x,p))" @@ -234,7 +234,7 @@ lemma Memrel_Reflects: "REFLECTS[\z. \x[L]. \y[L]. pair(L,x,y,z) & x \ y, \i z. \x \ Lset(i). \y \ Lset(i). pair(**Lset(i),x,y,z) & x \ y]" -by (intro FOL_reflection function_reflection) +by (intro FOL_reflections function_reflections) lemma Memrel_separation: "separation(L, \z. \x[L]. \y[L]. pair(L,x,y,z) & x \ y)" @@ -263,7 +263,7 @@ \nb \ Lset(i). \cnbf \ Lset(i). pair(**Lset(i),f,b,p) & pair(**Lset(i),n,b,nb) & is_cons(**Lset(i),nb,f,cnbf) & upair(**Lset(i),cnbf,cnbf,z))]" -by (intro FOL_reflection function_reflection) +by (intro FOL_reflections function_reflections) lemma funspace_succ_replacement: "L(n) ==> @@ -295,7 +295,7 @@ (\y[L]. \p[L]. fun_apply(L,f,x,y) & pair(L,y,x,p) & p \ r), \i x. x\A --> (\y \ Lset(i). \p \ Lset(i). fun_apply(**Lset(i),f,x,y) & pair(**Lset(i),y,x,p) & p \ r)]" -by (intro FOL_reflection function_reflection) +by (intro FOL_reflections function_reflections) lemma well_ord_iso_separation: "[| L(A); L(f); L(r) |] @@ -325,7 +325,7 @@ \i a. \x \ Lset(i). \g \ Lset(i). \mx \ Lset(i). \par \ Lset(i). ordinal(**Lset(i),x) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) & order_isomorphism(**Lset(i),par,r,x,mx,g)]" -by (intro FOL_reflection function_reflection fun_plus_reflection) +by (intro FOL_reflections function_reflections fun_plus_reflections) lemma obase_separation: --{*part of the order type formalization*} @@ -360,7 +360,7 @@ ordinal(**Lset(i),y) & (\my \ Lset(i). \pxr \ Lset(i). membership(**Lset(i),y,my) & pred_set(**Lset(i),A,x,r,pxr) & order_isomorphism(**Lset(i),pxr,r,y,my,g)))]" -by (intro FOL_reflection function_reflection fun_plus_reflection) +by (intro FOL_reflections function_reflections fun_plus_reflections) lemma obase_equals_separation: @@ -395,7 +395,7 @@ ordinal(**Lset(i),x) & pair(**Lset(i),a,x,z) & membership(**Lset(i),x,mx) & pred_set(**Lset(i),A,a,r,par) & order_isomorphism(**Lset(i),par,r,x,mx,g))]" -by (intro FOL_reflection function_reflection fun_plus_reflection) +by (intro FOL_reflections function_reflections fun_plus_reflections) lemma omap_replacement: "[| L(A); L(r) |] @@ -420,4 +420,272 @@ apply (simp_all add: succ_Un_distrib [symmetric]) done + +subsection{*Separation for a Theorem about @{term "obase"}*} + +lemma is_recfun_reflects: + "REFLECTS[\x. \xa[L]. \xb[L]. + pair(L,x,a,xa) & xa \ r & pair(L,x,b,xb) & xb \ r & + (\fx[L]. \gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & + fx \ gx), + \i x. \xa \ Lset(i). \xb \ Lset(i). + pair(**Lset(i),x,a,xa) & xa \ r & pair(**Lset(i),x,b,xb) & xb \ r & + (\fx \ Lset(i). \gx \ Lset(i). fun_apply(**Lset(i),f,x,fx) & + fun_apply(**Lset(i),g,x,gx) & fx \ gx)]" +by (intro FOL_reflections function_reflections fun_plus_reflections) + +lemma is_recfun_separation: + --{*for well-founded recursion*} + "[| L(r); L(f); L(g); L(a); L(b) |] + ==> separation(L, + \x. \xa[L]. \xb[L]. + pair(L,x,a,xa) & xa \ r & pair(L,x,b,xb) & xb \ r & + (\fx[L]. \gx[L]. fun_apply(L,f,x,fx) & fun_apply(L,g,x,gx) & + fx \ gx))" +apply (rule separation_CollectI) +apply (rule_tac A="{r,f,g,a,b,z}" in subset_LsetE, blast ) +apply (rule ReflectsE [OF is_recfun_reflects], 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,f,g,a,b]" in pair_iff_sats) +apply (rule sep_rules | simp)+ +apply (simp_all add: succ_Un_distrib [symmetric]) +done + + +ML +{* +val Inter_separation = thm "Inter_separation"; +val cartprod_separation = thm "cartprod_separation"; +val image_separation = thm "image_separation"; +val converse_separation = thm "converse_separation"; +val restrict_separation = thm "restrict_separation"; +val comp_separation = thm "comp_separation"; +val pred_separation = thm "pred_separation"; +val Memrel_separation = thm "Memrel_separation"; +val funspace_succ_replacement = thm "funspace_succ_replacement"; +val well_ord_iso_separation = thm "well_ord_iso_separation"; +val obase_separation = thm "obase_separation"; +val obase_equals_separation = thm "obase_equals_separation"; +val omap_replacement = thm "omap_replacement"; +val is_recfun_separation = thm "is_recfun_separation"; + +val m_axioms = + [Inter_separation, cartprod_separation, image_separation, + converse_separation, restrict_separation, comp_separation, + pred_separation, Memrel_separation, funspace_succ_replacement, + well_ord_iso_separation, obase_separation, + obase_equals_separation, omap_replacement, is_recfun_separation] + +fun axiomsL th = + kill_flex_triv_prems (m_axioms MRS (trivaxL th)); + +bind_thm ("cartprod_iff", axiomsL (thm "M_axioms.cartprod_iff")); +bind_thm ("cartprod_closed", axiomsL (thm "M_axioms.cartprod_closed")); +bind_thm ("sum_closed", axiomsL (thm "M_axioms.sum_closed")); +bind_thm ("M_converse_iff", axiomsL (thm "M_axioms.M_converse_iff")); +bind_thm ("converse_closed", axiomsL (thm "M_axioms.converse_closed")); +bind_thm ("converse_abs", axiomsL (thm "M_axioms.converse_abs")); +bind_thm ("image_closed", axiomsL (thm "M_axioms.image_closed")); +bind_thm ("vimage_abs", axiomsL (thm "M_axioms.vimage_abs")); +bind_thm ("vimage_closed", axiomsL (thm "M_axioms.vimage_closed")); +bind_thm ("domain_abs", axiomsL (thm "M_axioms.domain_abs")); +bind_thm ("domain_closed", axiomsL (thm "M_axioms.domain_closed")); +bind_thm ("range_abs", axiomsL (thm "M_axioms.range_abs")); +bind_thm ("range_closed", axiomsL (thm "M_axioms.range_closed")); +bind_thm ("field_abs", axiomsL (thm "M_axioms.field_abs")); +bind_thm ("field_closed", axiomsL (thm "M_axioms.field_closed")); +bind_thm ("relation_abs", axiomsL (thm "M_axioms.relation_abs")); +bind_thm ("function_abs", axiomsL (thm "M_axioms.function_abs")); +bind_thm ("apply_closed", axiomsL (thm "M_axioms.apply_closed")); +bind_thm ("apply_abs", axiomsL (thm "M_axioms.apply_abs")); +bind_thm ("typed_apply_abs", axiomsL (thm "M_axioms.typed_apply_abs")); +bind_thm ("typed_function_abs", axiomsL (thm "M_axioms.typed_function_abs")); +bind_thm ("injection_abs", axiomsL (thm "M_axioms.injection_abs")); +bind_thm ("surjection_abs", axiomsL (thm "M_axioms.surjection_abs")); +bind_thm ("bijection_abs", axiomsL (thm "M_axioms.bijection_abs")); +bind_thm ("M_comp_iff", axiomsL (thm "M_axioms.M_comp_iff")); +bind_thm ("comp_closed", axiomsL (thm "M_axioms.comp_closed")); +bind_thm ("composition_abs", axiomsL (thm "M_axioms.composition_abs")); +bind_thm ("restriction_is_function", axiomsL (thm "M_axioms.restriction_is_function")); +bind_thm ("restriction_abs", axiomsL (thm "M_axioms.restriction_abs")); +bind_thm ("M_restrict_iff", axiomsL (thm "M_axioms.M_restrict_iff")); +bind_thm ("restrict_closed", axiomsL (thm "M_axioms.restrict_closed")); +bind_thm ("Inter_abs", axiomsL (thm "M_axioms.Inter_abs")); +bind_thm ("Inter_closed", axiomsL (thm "M_axioms.Inter_closed")); +bind_thm ("Int_closed", axiomsL (thm "M_axioms.Int_closed")); +bind_thm ("finite_fun_closed", axiomsL (thm "M_axioms.finite_fun_closed")); +bind_thm ("is_funspace_abs", axiomsL (thm "M_axioms.is_funspace_abs")); +bind_thm ("succ_fun_eq2", axiomsL (thm "M_axioms.succ_fun_eq2")); +bind_thm ("funspace_succ", axiomsL (thm "M_axioms.funspace_succ")); +bind_thm ("finite_funspace_closed", axiomsL (thm "M_axioms.finite_funspace_closed")); +*} + +ML +{* +bind_thm ("is_recfun_equal", axiomsL (thm "M_axioms.is_recfun_equal")); +bind_thm ("is_recfun_cut", axiomsL (thm "M_axioms.is_recfun_cut")); +bind_thm ("is_recfun_functional", axiomsL (thm "M_axioms.is_recfun_functional")); +bind_thm ("is_recfun_relativize", axiomsL (thm "M_axioms.is_recfun_relativize")); +bind_thm ("is_recfun_restrict", axiomsL (thm "M_axioms.is_recfun_restrict")); +bind_thm ("univalent_is_recfun", axiomsL (thm "M_axioms.univalent_is_recfun")); +bind_thm ("exists_is_recfun_indstep", axiomsL (thm "M_axioms.exists_is_recfun_indstep")); +bind_thm ("wellfounded_exists_is_recfun", axiomsL (thm "M_axioms.wellfounded_exists_is_recfun")); +bind_thm ("wf_exists_is_recfun", axiomsL (thm "M_axioms.wf_exists_is_recfun")); +bind_thm ("is_recfun_iff_M", axiomsL (thm "M_axioms.is_recfun_iff_M")); +bind_thm ("irreflexive_abs", axiomsL (thm "M_axioms.irreflexive_abs")); +bind_thm ("transitive_rel_abs", axiomsL (thm "M_axioms.transitive_rel_abs")); +bind_thm ("linear_rel_abs", axiomsL (thm "M_axioms.linear_rel_abs")); +bind_thm ("wellordered_is_trans_on", axiomsL (thm "M_axioms.wellordered_is_trans_on")); +bind_thm ("wellordered_is_linear", axiomsL (thm "M_axioms.wellordered_is_linear")); +bind_thm ("wellordered_is_wellfounded_on", axiomsL (thm "M_axioms.wellordered_is_wellfounded_on")); +bind_thm ("wellfounded_imp_wellfounded_on", axiomsL (thm "M_axioms.wellfounded_imp_wellfounded_on")); +bind_thm ("wellfounded_on_subset_A", axiomsL (thm "M_axioms.wellfounded_on_subset_A")); +bind_thm ("wellfounded_on_iff_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_iff_wellfounded")); +bind_thm ("wellfounded_on_imp_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_imp_wellfounded")); +bind_thm ("wellfounded_on_field_imp_wellfounded", axiomsL (thm "M_axioms.wellfounded_on_field_imp_wellfounded")); +bind_thm ("wellfounded_iff_wellfounded_on_field", axiomsL (thm "M_axioms.wellfounded_iff_wellfounded_on_field")); +bind_thm ("wellfounded_induct", axiomsL (thm "M_axioms.wellfounded_induct")); +bind_thm ("wellfounded_on_induct", axiomsL (thm "M_axioms.wellfounded_on_induct")); +bind_thm ("wellfounded_on_induct2", axiomsL (thm "M_axioms.wellfounded_on_induct2")); +bind_thm ("linear_imp_relativized", axiomsL (thm "M_axioms.linear_imp_relativized")); +bind_thm ("trans_on_imp_relativized", axiomsL (thm "M_axioms.trans_on_imp_relativized")); +bind_thm ("wf_on_imp_relativized", axiomsL (thm "M_axioms.wf_on_imp_relativized")); +bind_thm ("wf_imp_relativized", axiomsL (thm "M_axioms.wf_imp_relativized")); +bind_thm ("well_ord_imp_relativized", axiomsL (thm "M_axioms.well_ord_imp_relativized")); +bind_thm ("order_isomorphism_abs", axiomsL (thm "M_axioms.order_isomorphism_abs")); +bind_thm ("pred_set_abs", axiomsL (thm "M_axioms.pred_set_abs")); +*} + +ML +{* +bind_thm ("pred_closed", axiomsL (thm "M_axioms.pred_closed")); +bind_thm ("membership_abs", axiomsL (thm "M_axioms.membership_abs")); +bind_thm ("M_Memrel_iff", axiomsL (thm "M_axioms.M_Memrel_iff")); +bind_thm ("Memrel_closed", axiomsL (thm "M_axioms.Memrel_closed")); +bind_thm ("wellordered_iso_predD", axiomsL (thm "M_axioms.wellordered_iso_predD")); +bind_thm ("wellordered_iso_pred_eq", axiomsL (thm "M_axioms.wellordered_iso_pred_eq")); +bind_thm ("wellfounded_on_asym", axiomsL (thm "M_axioms.wellfounded_on_asym")); +bind_thm ("wellordered_asym", axiomsL (thm "M_axioms.wellordered_asym")); +bind_thm ("ord_iso_pred_imp_lt", axiomsL (thm "M_axioms.ord_iso_pred_imp_lt")); +bind_thm ("obase_iff", axiomsL (thm "M_axioms.obase_iff")); +bind_thm ("omap_iff", axiomsL (thm "M_axioms.omap_iff")); +bind_thm ("omap_unique", axiomsL (thm "M_axioms.omap_unique")); +bind_thm ("omap_yields_Ord", axiomsL (thm "M_axioms.omap_yields_Ord")); +bind_thm ("otype_iff", axiomsL (thm "M_axioms.otype_iff")); +bind_thm ("otype_eq_range", axiomsL (thm "M_axioms.otype_eq_range")); +bind_thm ("Ord_otype", axiomsL (thm "M_axioms.Ord_otype")); +bind_thm ("domain_omap", axiomsL (thm "M_axioms.domain_omap")); +bind_thm ("omap_subset", axiomsL (thm "M_axioms.omap_subset")); +bind_thm ("omap_funtype", axiomsL (thm "M_axioms.omap_funtype")); +bind_thm ("wellordered_omap_bij", axiomsL (thm "M_axioms.wellordered_omap_bij")); +bind_thm ("omap_ord_iso", axiomsL (thm "M_axioms.omap_ord_iso")); +bind_thm ("Ord_omap_image_pred", axiomsL (thm "M_axioms.Ord_omap_image_pred")); +bind_thm ("restrict_omap_ord_iso", axiomsL (thm "M_axioms.restrict_omap_ord_iso")); +bind_thm ("obase_equals", axiomsL (thm "M_axioms.obase_equals")); +bind_thm ("omap_ord_iso_otype", axiomsL (thm "M_axioms.omap_ord_iso_otype")); +bind_thm ("obase_exists", axiomsL (thm "M_axioms.obase_exists")); +bind_thm ("omap_exists", axiomsL (thm "M_axioms.omap_exists")); +bind_thm ("otype_exists", axiomsL (thm "M_axioms.otype_exists")); +bind_thm ("omap_ord_iso_otype", axiomsL (thm "M_axioms.omap_ord_iso_otype")); +bind_thm ("ordertype_exists", axiomsL (thm "M_axioms.ordertype_exists")); +bind_thm ("relativized_imp_well_ord", axiomsL (thm "M_axioms.relativized_imp_well_ord")); +bind_thm ("well_ord_abs", axiomsL (thm "M_axioms.well_ord_abs")); +*} + +declare cartprod_closed [intro,simp] +declare sum_closed [intro,simp] +declare converse_closed [intro,simp] +declare converse_abs [simp] +declare image_closed [intro,simp] +declare vimage_abs [simp] +declare vimage_closed [intro,simp] +declare domain_abs [simp] +declare domain_closed [intro,simp] +declare range_abs [simp] +declare range_closed [intro,simp] +declare field_abs [simp] +declare field_closed [intro,simp] +declare relation_abs [simp] +declare function_abs [simp] +declare apply_closed [intro,simp] +declare typed_function_abs [simp] +declare injection_abs [simp] +declare surjection_abs [simp] +declare bijection_abs [simp] +declare comp_closed [intro,simp] +declare composition_abs [simp] +declare restriction_abs [simp] +declare restrict_closed [intro,simp] +declare Inter_abs [simp] +declare Inter_closed [intro,simp] +declare Int_closed [intro,simp] +declare finite_fun_closed [rule_format] +declare is_funspace_abs [simp] +declare finite_funspace_closed [intro,simp] + + +(***NOW FOR THE LOCALE M_TRANCL***) + +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) + + +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))))" +apply (rule separation_CollectI) +apply (rule_tac A="{r,A,z}" in subset_LsetE, blast ) +apply (rule ReflectsE [OF rtrancl_reflects], 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 (rule sep_rules | simp)+ +apply (simp_all add: succ_Un_distrib [symmetric]) +done + + end diff -r 3323ecc0b97c -r 2c287f50c9f3 src/ZF/Constructible/WF_absolute.thy --- a/src/ZF/Constructible/WF_absolute.thy Tue Jul 09 13:41:38 2002 +0200 +++ b/src/ZF/Constructible/WF_absolute.thy Tue Jul 09 15:39:44 2002 +0200 @@ -133,18 +133,24 @@ locale M_trancl = M_axioms + -(*THEY NEED RELATIVIZATION*) assumes rtrancl_separation: - "[| M(r); M(A) |] ==> - separation - (M, \p. \n[M]. n\nat & - (\f[M]. - f \ succ(n) -> A & - (\x[M]. \y[M]. pair(M,x,y,p) & - f`0 = x & f`n = y) & - (\i\n. \ r)))" + "[| 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))))" and wellfounded_trancl_separation: - "[| M(r); M(Z) |] ==> separation (M, \x. \w[M]. w \ Z & \w,x\ \ r^+)" + "[| M(r); M(Z) |] ==> + separation (M, \x. + \w[M]. \wx[M]. \rp[M]. + w \ Z & pair(M,w,x,wx) & tran_closure(M,r,rp) & wx \ rp)" lemma (in M_trancl) rtran_closure_rtrancl: @@ -203,6 +209,9 @@ "[| M(r); M(z) |] ==> tran_closure(M,r,z) <-> z = trancl(r)" by (simp add: tran_closure_def trancl_def) +lemma (in M_trancl) wellfounded_trancl_separation': + "[| M(r); M(Z) |] ==> separation (M, \x. \w[M]. w \ Z & \ r^+)" +by (insert wellfounded_trancl_separation [of r Z], simp) text{*Alternative proof of @{text wf_on_trancl}; inspiration for the relativized version. Original version is on theory WF.*} @@ -213,7 +222,6 @@ apply (blast elim: tranclE) done - lemma (in M_trancl) wellfounded_on_trancl: "[| wellfounded_on(M,A,r); r-``A <= A; M(r); M(A) |] ==> wellfounded_on(M,A,r^+)" @@ -222,7 +230,7 @@ apply (rename_tac Z x) apply (subgoal_tac "M({x\A. \w[M]. w \ Z & \w,x\ \ r^+})") prefer 2 - apply (blast intro: wellfounded_trancl_separation) + apply (blast intro: wellfounded_trancl_separation') apply (drule_tac x = "{x\A. \w[M]. w \ Z & \w,x\ \ r^+}" in rspec, safe) apply (blast dest: transM, simp) apply (rename_tac y w) diff -r 3323ecc0b97c -r 2c287f50c9f3 src/ZF/Constructible/document/root.tex --- a/src/ZF/Constructible/document/root.tex Tue Jul 09 13:41:38 2002 +0200 +++ b/src/ZF/Constructible/document/root.tex Tue Jul 09 15:39:44 2002 +0200 @@ -16,9 +16,8 @@ % this should be the last package used \usepackage{pdfsetup} -% proper setup for best-style documents \urlstyle{rm} -\isabellestyle{it} +\isabellestyle{tt} %and not {it}! \begin{document}