# HG changeset patch # User paulson # Date 1025800190 -7200 # Node ID 3a932abf97e84cb2eb49b075dcc8a56c0be50a81 # Parent b4f370679c6516ef57e03fa93e49038003617d66 More use of relativized quantifiers diff -r b4f370679c65 -r 3a932abf97e8 src/ZF/Constructible/L_axioms.thy --- a/src/ZF/Constructible/L_axioms.thy Thu Jul 04 16:59:54 2002 +0200 +++ b/src/ZF/Constructible/L_axioms.thy Thu Jul 04 18:29:50 2002 +0200 @@ -17,21 +17,21 @@ lemma upair_ax: "upair_ax(L)" apply (simp add: upair_ax_def upair_def, clarify) -apply (rule_tac x="{x,y}" in exI) -apply (simp add: doubleton_in_L) +apply (rule_tac x="{x,y}" in rexI) +apply (simp_all add: doubleton_in_L) done lemma Union_ax: "Union_ax(L)" apply (simp add: Union_ax_def big_union_def, clarify) -apply (rule_tac x="Union(x)" in exI) -apply (simp add: Union_in_L, auto) +apply (rule_tac x="Union(x)" in rexI) +apply (simp_all add: Union_in_L, auto) apply (blast intro: transL) done lemma power_ax: "power_ax(L)" apply (simp add: power_ax_def powerset_def Relative.subset_def, clarify) -apply (rule_tac x="{y \ Pow(x). L(y)}" in exI) -apply (simp add: LPow_in_L, auto) +apply (rule_tac x="{y \ Pow(x). L(y)}" in rexI) +apply (simp_all add: LPow_in_L, auto) apply (blast intro: transL) done @@ -63,8 +63,8 @@ lemma replacement: "replacement(L,P)" apply (simp add: replacement_def, clarify) apply (frule LReplace_in_L, assumption+, clarify) -apply (rule_tac x=Y in exI) -apply (simp add: Replace_iff univalent_def, blast) +apply (rule_tac x=Y in rexI) +apply (simp_all add: Replace_iff univalent_def, blast) done subsection{*Instantiation of the locale @{text M_triv_axioms}*} diff -r b4f370679c65 -r 3a932abf97e8 src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Thu Jul 04 16:59:54 2002 +0200 +++ b/src/ZF/Constructible/Relative.thy Thu Jul 04 18:29:50 2002 +0200 @@ -47,29 +47,28 @@ is_converse :: "[i=>o,i,i] => o" "is_converse(M,r,z) == - \x. M(x) --> - (x \ z <-> - (\w[M]. w\r & (\u[M]. \v[M]. pair(M,u,v,w) & pair(M,v,u,x))))" + \x[M]. x \ z <-> + (\w[M]. w\r & (\u[M]. \v[M]. pair(M,u,v,w) & pair(M,v,u,x)))" pre_image :: "[i=>o,i,i,i] => o" "pre_image(M,r,A,z) == - \x. M(x) --> (x \ z <-> (\w[M]. w\r & (\y[M]. y\A & pair(M,x,y,w))))" + \x[M]. x \ z <-> (\w[M]. w\r & (\y[M]. y\A & pair(M,x,y,w)))" is_domain :: "[i=>o,i,i] => o" "is_domain(M,r,z) == - \x. M(x) --> (x \ z <-> (\w[M]. w\r & (\y[M]. pair(M,x,y,w))))" + \x[M]. (x \ z <-> (\w[M]. w\r & (\y[M]. pair(M,x,y,w))))" image :: "[i=>o,i,i,i] => o" "image(M,r,A,z) == - \y. M(y) --> (y \ z <-> (\w[M]. w\r & (\x[M]. x\A & pair(M,x,y,w))))" + \y[M]. (y \ z <-> (\w[M]. w\r & (\x[M]. x\A & pair(M,x,y,w))))" is_range :: "[i=>o,i,i] => o" --{*the cleaner - @{term "\r'. M(r') & is_converse(M,r,r') & is_domain(M,r',z)"} + @{term "\r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"} unfortunately needs an instance of separation in order to prove @{term "M(converse(r))"}.*} "is_range(M,r,z) == - \y. M(y) --> (y \ z <-> (\w[M]. w\r & (\x[M]. pair(M,x,y,w))))" + \y[M]. (y \ z <-> (\w[M]. w\r & (\x[M]. pair(M,x,y,w))))" is_field :: "[i=>o,i,i] => o" "is_field(M,r,z) == @@ -82,18 +81,17 @@ is_function :: "[i=>o,i] => o" "is_function(M,r) == - (\x y y' p p'. M(x) --> M(y) --> M(y') --> M(p) --> M(p') --> - pair(M,x,y,p) --> pair(M,x,y',p') --> p\r --> p'\r --> - y=y')" + \x[M]. \y[M]. \y'[M]. \p[M]. \p'[M]. + pair(M,x,y,p) --> pair(M,x,y',p') --> p\r --> p'\r --> y=y'" fun_apply :: "[i=>o,i,i,i] => o" "fun_apply(M,f,x,y) == - (\y'. M(y') --> ((\u\f. M(u) & pair(M,x,y',u)) <-> y=y'))" + (\y'[M]. (\u[M]. u\f & pair(M,x,y',u)) <-> y=y')" typed_function :: "[i=>o,i,i,i] => o" "typed_function(M,A,B,r) == is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) & - (\u\r. M(u) --> (\x y. M(x) & M(y) & pair(M,x,y,u) --> y\B))" + (\u[M]. u\r --> (\x y. M(x) & M(y) & pair(M,x,y,u) --> y\B))" is_funspace :: "[i=>o,i,i,i] => o" "is_funspace(M,A,B,F) == @@ -101,8 +99,8 @@ composition :: "[i=>o,i,i,i] => o" "composition(M,r,s,t) == - \p. M(p) --> (p \ t <-> - (\x. M(x) & (\y. M(y) & (\z. M(z) & + \p[M]. (p \ t <-> + (\x[M]. (\y[M]. (\z[M]. p = \x,z\ & \x,y\ \ s & \y,z\ \ r))))" @@ -116,29 +114,29 @@ surjection :: "[i=>o,i,i,i] => o" "surjection(M,A,B,f) == typed_function(M,A,B,f) & - (\y\B. M(y) --> (\x\A. M(x) & fun_apply(M,f,x,y)))" + (\y[M]. y\B --> (\x[M]. x\A & fun_apply(M,f,x,y)))" bijection :: "[i=>o,i,i,i] => o" "bijection(M,A,B,f) == injection(M,A,B,f) & surjection(M,A,B,f)" restriction :: "[i=>o,i,i,i] => o" "restriction(M,r,A,z) == - \x. M(x) --> + \x[M]. (x \ z <-> - (x \ r & (\u\A. M(u) & (\v. M(v) & pair(M,u,v,x)))))" + (x \ r & (\u[M]. u\A & (\v[M]. pair(M,u,v,x)))))" transitive_set :: "[i=>o,i] => o" - "transitive_set(M,a) == \x\a. M(x) --> subset(M,x,a)" + "transitive_set(M,a) == \x[M]. x\a --> subset(M,x,a)" ordinal :: "[i=>o,i] => o" --{*an ordinal is a transitive set of transitive sets*} - "ordinal(M,a) == transitive_set(M,a) & (\x\a. M(x) --> transitive_set(M,x))" + "ordinal(M,a) == transitive_set(M,a) & (\x[M]. x\a --> transitive_set(M,x))" limit_ordinal :: "[i=>o,i] => o" --{*a limit ordinal is a non-empty, successor-closed ordinal*} "limit_ordinal(M,a) == ordinal(M,a) & ~ empty(M,a) & - (\x\a. M(x) --> (\y\a. M(y) & successor(M,x,y)))" + (\x[M]. x\a --> (\y[M]. y\a & successor(M,x,y)))" successor_ordinal :: "[i=>o,i] => o" --{*a successor ordinal is any ordinal that is neither empty nor limit*} @@ -149,20 +147,20 @@ --{*an ordinal is finite if neither it nor any of its elements are limit*} "finite_ordinal(M,a) == ordinal(M,a) & ~ limit_ordinal(M,a) & - (\x\a. M(x) --> ~ limit_ordinal(M,x))" + (\x[M]. x\a --> ~ limit_ordinal(M,x))" omega :: "[i=>o,i] => o" --{*omega is a limit ordinal none of whose elements are limit*} - "omega(M,a) == limit_ordinal(M,a) & (\x\a. M(x) --> ~ limit_ordinal(M,x))" + "omega(M,a) == limit_ordinal(M,a) & (\x[M]. x\a --> ~ limit_ordinal(M,x))" number1 :: "[i=>o,i] => o" - "number1(M,a) == (\x. M(x) & empty(M,x) & successor(M,x,a))" + "number1(M,a) == (\x[M]. empty(M,x) & successor(M,x,a))" number2 :: "[i=>o,i] => o" - "number2(M,a) == (\x. M(x) & number1(M,x) & successor(M,x,a))" + "number2(M,a) == (\x[M]. number1(M,x) & successor(M,x,a))" number3 :: "[i=>o,i] => o" - "number3(M,a) == (\x. M(x) & number2(M,x) & successor(M,x,a))" + "number3(M,a) == (\x[M]. number2(M,x) & successor(M,x,a))" subsection {*The relativized ZF axioms*} @@ -179,32 +177,32 @@ \z[M]. \y[M]. \x[M]. x \ y <-> x \ z & P(x)" upair_ax :: "(i=>o) => o" - "upair_ax(M) == \x y. M(x) --> M(y) --> (\z. M(z) & upair(M,x,y,z))" + "upair_ax(M) == \x y. M(x) --> M(y) --> (\z[M]. upair(M,x,y,z))" Union_ax :: "(i=>o) => o" - "Union_ax(M) == \x. M(x) --> (\z. M(z) & big_union(M,x,z))" + "Union_ax(M) == \x[M]. (\z[M]. big_union(M,x,z))" power_ax :: "(i=>o) => o" - "power_ax(M) == \x. M(x) --> (\z. M(z) & powerset(M,x,z))" + "power_ax(M) == \x[M]. (\z[M]. powerset(M,x,z))" univalent :: "[i=>o, i, [i,i]=>o] => o" "univalent(M,A,P) == - (\x\A. M(x) --> (\y z. M(y) --> M(z) --> P(x,y) & P(x,z) --> y=z))" + (\x[M]. x\A --> (\y z. M(y) --> M(z) --> P(x,y) & P(x,z) --> y=z))" replacement :: "[i=>o, [i,i]=>o] => o" "replacement(M,P) == - \A. M(A) --> univalent(M,A,P) --> - (\Y. M(Y) & (\b. M(b) --> ((\x\A. M(x) & P(x,b)) --> b \ Y)))" + \A[M]. univalent(M,A,P) --> + (\Y[M]. (\b[M]. ((\x[M]. x\A & P(x,b)) --> b \ Y)))" strong_replacement :: "[i=>o, [i,i]=>o] => o" "strong_replacement(M,P) == - \A. M(A) --> univalent(M,A,P) --> - (\Y. M(Y) & (\b. M(b) --> (b \ Y <-> (\x\A. M(x) & P(x,b)))))" + \A[M]. univalent(M,A,P) --> + (\Y[M]. (\b[M]. (b \ Y <-> (\x[M]. x\A & P(x,b)))))" foundation_ax :: "(i=>o) => o" "foundation_ax(M) == - \x. M(x) --> (\y\x. M(y)) - --> (\y\x. M(y) & ~(\z\x. M(z) & z \ y))" + \x[M]. (\y\x. M(y)) + --> (\y[M]. y\x & ~(\z[M]. z\x & z \ y))" subsection{*A trivial consistency proof for $V_\omega$ *} @@ -281,8 +279,10 @@ text{*Union axiom*} lemma "Union_ax(\x. x \ univ(0))" -apply (simp add: Union_ax_def big_union_def) -apply (blast intro: Union_in_univ Transset_0 univ0_downwards_mem) +apply (simp add: Union_ax_def big_union_def, clarify) +apply (rule_tac x="\x" in bexI) + apply (blast intro: univ0_downwards_mem) +apply (blast intro: Union_in_univ Transset_0) done text{*Powerset axiom*} @@ -293,14 +293,17 @@ done lemma "power_ax(\x. x \ univ(0))" -apply (simp add: power_ax_def powerset_def subset_def) -apply (blast intro: Pow_in_univ Transset_0 univ0_downwards_mem) +apply (simp add: power_ax_def powerset_def subset_def, clarify) +apply (rule_tac x="Pow(x)" in bexI) + apply (blast intro: univ0_downwards_mem) +apply (blast intro: Pow_in_univ Transset_0) done text{*Foundation axiom*} lemma "foundation_ax(\x. x \ univ(0))" apply (simp add: foundation_ax_def, clarify) -apply (cut_tac A=x in foundation, blast) +apply (cut_tac A=x in foundation) +apply (blast intro: univ0_downwards_mem) done lemma "replacement(\x. x \ univ(0), P)" @@ -341,12 +344,12 @@ lemma replacementD: "[| replacement(M,P); M(A); univalent(M,A,P) |] - ==> \Y. M(Y) & (\b. M(b) --> ((\x\A. M(x) & P(x,b)) --> b \ Y))" + ==> \Y[M]. (\b[M]. ((\x[M]. x\A & P(x,b)) --> b \ Y))" by (simp add: replacement_def) lemma strong_replacementD: "[| strong_replacement(M,P); M(A); univalent(M,A,P) |] - ==> \Y. M(Y) & (\b. M(b) --> (b \ Y <-> (\x\A. M(x) & P(x,b))))" + ==> \Y[M]. (\b[M]. (b \ Y <-> (\x[M]. x\A & P(x,b))))" by (simp add: strong_replacement_def) lemma separationD: @@ -368,12 +371,11 @@ pred_set :: "[i=>o,i,i,i,i] => o" "pred_set(M,A,x,r,B) == - \y. M(y) --> (y \ B <-> (\p\r. M(p) & y \ A & pair(M,y,x,p)))" + \y[M]. y \ B <-> (\p[M]. p\r & y \ A & pair(M,y,x,p))" membership :: "[i=>o,i,i] => o" --{*membership relation*} "membership(M,A,r) == - \p. M(p) --> - (p \ r <-> (\x\A. \y\A. M(x) & M(y) & x\y & pair(M,x,y,p)))" + \p[M]. p \ r <-> (\x\A. \y\A. M(x) & M(y) & x\y & pair(M,x,y,p))" subsection{*Absoluteness for a transitive class model*} @@ -407,7 +409,7 @@ by (blast intro: transM) lemma (in M_triv_axioms) ball_iff_equiv: - "M(A) ==> (\x. M(x) --> (x\A <-> P(x))) <-> + "M(A) ==> (\x[M]. (x\A <-> P(x))) <-> (\x\A. P(x)) & (\x. P(x) --> M(x) --> x\A)" by (blast intro: transM) @@ -525,13 +527,14 @@ text{*Probably the premise and conclusion are equivalent*} lemma (in M_triv_axioms) strong_replacementI [rule_format]: - "[| \A. M(A) --> separation(M, %u. \x\A. P(x,u)) |] + "[| \A[M]. separation(M, %u. \x\A. P(x,u)) |] ==> strong_replacement(M,P)" apply (simp add: strong_replacement_def, clarify) apply (frule replacementD [OF replacement], assumption, clarify) -apply (drule_tac x=A in spec, clarify) +apply (drule_tac x=A in rspec, clarify) apply (drule_tac z=Y in separationD, assumption, clarify) -apply (blast dest: transM) +apply (rule_tac x=y in rexI) +apply (blast dest: transM)+ done @@ -540,7 +543,7 @@ "[| strong_replacement(M,P); M(A); univalent(M,A,P); !!x y. [| x\A; P(x,y); M(x) |] ==> M(y) |] ==> M(Replace(A,P))" apply (simp add: strong_replacement_def) -apply (drule spec [THEN mp], auto) +apply (drule rspec, auto) apply (subgoal_tac "Replace(A,P) = Y") apply simp apply (rule equality_iffI) @@ -548,7 +551,7 @@ apply (blast dest: transM) apply (frule transM, assumption) apply (simp add: univalent_def) - apply (drule spec [THEN mp, THEN iffD1], assumption, assumption) + apply (drule rspec [THEN iffD1], assumption, assumption) apply (blast dest: transM) done @@ -636,7 +639,7 @@ done lemma (in M_triv_axioms) successor_ordinal_abs [simp]: - "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\b. M(b) & a = succ(b))" + "M(a) ==> successor_ordinal(M,a) <-> Ord(a) & (\b[M]. a = succ(b))" apply (simp add: successor_ordinal_def, safe) apply (drule Ord_cases_disj, auto) done @@ -694,7 +697,7 @@ primrec "natnumber_aux(M,0) = (\x\nat. if empty(M,x) then 1 else 0)" "natnumber_aux(M,succ(n)) = - (\x\nat. if (\y. M(y) & natnumber_aux(M,n)`y=1 & successor(M,y,x)) + (\x\nat. if (\y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x)) then 1 else 0)" constdefs @@ -742,12 +745,12 @@ pair(M,f,b,p) & pair(M,n,b,nb) & z = {cons(nb,f)})" and well_ord_iso_separation: "[| M(A); M(f); M(r) |] - ==> separation (M, \x. x\A --> (\y. M(y) & (\p. M(p) & + ==> separation (M, \x. x\A --> (\y[M]. (\p[M]. fun_apply(M,f,x,y) & pair(M,y,x,p) & p \ r)))" and obase_equals_separation: "[| M(A); M(r) |] ==> separation - (M, \x. x\A --> ~(\y. M(y) & (\g. M(g) & + (M, \x. x\A --> ~(\y[M]. (\g. M(g) & ordinal(M,y) & (\my pxr. M(my) & M(pxr) & membership(M,y,my) & pred_set(M,A,x,r,pxr) & order_isomorphism(M,pxr,r,y,my,g)))))" @@ -786,24 +789,25 @@ apply blast txt{*Final, difficult case: the left-to-right direction of the theorem.*} apply (insert power_ax, simp add: power_ax_def) -apply (frule_tac x="A Un B" and P="\x. M(x) --> Ex(?Q(x))" in spec) -apply (erule impE, blast, clarify) -apply (drule_tac x=z and P="\x. M(x) --> Ex(?Q(x))" in spec) +apply (frule_tac x="A Un B" and P="\x. rex(M,?Q(x))" in rspec) +apply (blast, clarify) +apply (drule_tac x=z and P="\x. rex(M,?Q(x))" in rspec) +apply assumption apply (blast intro: cartprod_iff_lemma) done lemma (in M_axioms) cartprod_closed_lemma: - "[| M(A); M(B) |] ==> \C. M(C) & cartprod(M,A,B,C)" + "[| M(A); M(B) |] ==> \C[M]. cartprod(M,A,B,C)" apply (simp del: cartprod_abs add: cartprod_iff) apply (insert power_ax, simp add: power_ax_def) -apply (frule_tac x="A Un B" and P="\x. M(x) --> Ex(?Q(x))" in spec) -apply (erule impE, blast, clarify) -apply (drule_tac x=z and P="\x. M(x) --> Ex(?Q(x))" in spec) -apply (erule impE, blast, clarify) -apply (intro exI conjI) -prefer 6 apply (rule refl) -prefer 4 apply assumption -prefer 4 apply assumption +apply (frule_tac x="A Un B" and P="\x. rex(M,?Q(x))" in rspec) +apply (blast, clarify) +apply (drule_tac x=z and P="\x. rex(M,?Q(x))" in rspec) +apply (blast, clarify) +apply (intro rexI exI conjI) +prefer 5 apply (rule refl) +prefer 3 apply assumption +prefer 3 apply assumption apply (insert cartprod_separation [of A B], auto) done diff -r b4f370679c65 -r 3a932abf97e8 src/ZF/Constructible/WF_absolute.thy --- a/src/ZF/Constructible/WF_absolute.thy Thu Jul 04 16:59:54 2002 +0200 +++ b/src/ZF/Constructible/WF_absolute.thy Thu Jul 04 18:29:50 2002 +0200 @@ -221,7 +221,7 @@ apply (subgoal_tac "M({x\A. \w[M]. w \ Z & \w,x\ \ r^+})") prefer 2 apply (blast intro: wellfounded_trancl_separation) -apply (drule_tac x = "{x\A. \w[M]. w \ Z & \w,x\ \ r^+}" in spec, safe) +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) apply (drule_tac x=w in bspec, assumption, clarify) diff -r b4f370679c65 -r 3a932abf97e8 src/ZF/Constructible/WFrec.thy --- a/src/ZF/Constructible/WFrec.thy Thu Jul 04 16:59:54 2002 +0200 +++ b/src/ZF/Constructible/WFrec.thy Thu Jul 04 18:29:50 2002 +0200 @@ -169,16 +169,15 @@ lemma (in M_axioms) restrict_Y_lemma: "[| wellfounded(M,r); trans(r); M(r); \x[M]. \g[M]. function(g) --> M(H(x,g)); M(Y); - \b. M(b) --> + \b[M]. b \ Y <-> - (\x\r -`` {a1}. \y[M]. \g[M]. - b = \x,y\ & is_recfun(r,x,H,g) \ y = H(x,g)); - \x,a1\ \ r; M(f); is_recfun(r,x,H,f) |] + (\x[M]. \ r & + (\y[M]. b = \x,y\ & (\g[M]. is_recfun(r,x,H,g) \ y = H(x,g)))); + \x,a1\ \ r; is_recfun(r,x,H,f); M(f) |] ==> restrict(Y, r -`` {x}) = f" apply (subgoal_tac "\y \ r-``{x}. \z. :Y <-> :f") apply (simp (no_asm_simp) add: restrict_def) apply (thin_tac "rall(M,?P)")+ --{*essential for efficiency*} - apply (thin_tac "All(?P)")+ --{*essential for efficiency*} apply (frule is_recfun_type [THEN fun_is_rel], blast) apply (frule pair_components_in_M, assumption, clarify) apply (rule iffI) @@ -205,6 +204,7 @@ apply (blast dest: is_recfun_functional) done + text{*Proof of the inductive step for @{text exists_is_recfun}, since we must prove two versions.*} lemma (in M_axioms) exists_is_recfun_indstep: @@ -225,13 +225,17 @@ apply (simp (no_asm_simp) add: is_recfun_relativize [of concl: _ a1]) txt{*The big iff-formula defining @{term Y} is now redundant*} apply safe - apply (simp add: vimage_singleton_iff restrict_Y_lemma [of r H]) + apply (simp add: vimage_singleton_iff restrict_Y_lemma [of r H _ a1]) txt{*one more case*} apply (simp (no_asm_simp) add: Bex_def vimage_singleton_iff) apply (drule_tac x1=x in spec [THEN mp], assumption, clarify) apply (rename_tac f) apply (rule_tac x=f in rexI) apply (simp_all add: restrict_Y_lemma [of r H]) +txt{*FIXME: should not be needed!*} +apply (subst restrict_Y_lemma [of r H]) +apply (simp add: vimage_singleton_iff)+ +apply blast+ done text{*Relativized version, when we have the (currently weaker) premise diff -r b4f370679c65 -r 3a932abf97e8 src/ZF/Constructible/Wellorderings.thy --- a/src/ZF/Constructible/Wellorderings.thy Thu Jul 04 16:59:54 2002 +0200 +++ b/src/ZF/Constructible/Wellorderings.thy Thu Jul 04 18:29:50 2002 +0200 @@ -13,27 +13,27 @@ constdefs irreflexive :: "[i=>o,i,i]=>o" - "irreflexive(M,A,r) == \x\A. M(x) --> \ r" + "irreflexive(M,A,r) == \x[M]. x\A --> \ r" transitive_rel :: "[i=>o,i,i]=>o" "transitive_rel(M,A,r) == - \x\A. M(x) --> (\y\A. M(y) --> (\z\A. M(z) --> + \x[M]. x\A --> (\y[M]. y\A --> (\z[M]. z\A --> \r --> \r --> \r))" linear_rel :: "[i=>o,i,i]=>o" "linear_rel(M,A,r) == - \x\A. M(x) --> (\y\A. M(y) --> \