# HG changeset patch # User paulson # Date 1033739852 -7200 # Node ID 87482b5e3f2e780515cbc460b130aa84a1cf8723 # Parent 67b0b7500a9dbde470f58ffc626b684b993adf04 Various simplifications of the Constructible theories diff -r 67b0b7500a9d -r 87482b5e3f2e src/ZF/Constructible/L_axioms.thy --- a/src/ZF/Constructible/L_axioms.thy Fri Oct 04 15:23:58 2002 +0200 +++ b/src/ZF/Constructible/L_axioms.thy Fri Oct 04 15:57:32 2002 +0200 @@ -95,8 +95,7 @@ theorem M_trivial_L: "PROP M_trivial(L)" apply (rule M_trivial.intro) - apply (erule (1) transL) - apply (rule nonempty) + apply (erule (1) transL) apply (rule upair_ax) apply (rule Union_ax) apply (rule power_ax) diff -r 67b0b7500a9d -r 87482b5e3f2e src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Fri Oct 04 15:23:58 2002 +0200 +++ b/src/ZF/Constructible/Relative.thy Fri Oct 04 15:57:32 2002 +0200 @@ -21,7 +21,7 @@ "upair(M,a,b,z) == a \ z & b \ z & (\x[M]. x\z --> x = a | x = b)" pair :: "[i=>o,i,i,i] => o" - "pair(M,a,b,z) == \x[M]. upair(M,a,a,x) & + "pair(M,a,b,z) == \x[M]. upair(M,a,a,x) & (\y[M]. upair(M,a,b,y) & upair(M,x,y,z))" @@ -62,17 +62,17 @@ "big_union(M,A,z) == \x[M]. x \ z <-> (\y[M]. y\A & x \ y)" big_inter :: "[i=>o,i,i] => o" - "big_inter(M,A,z) == + "big_inter(M,A,z) == (A=0 --> z=0) & (A\0 --> (\x[M]. x \ z <-> (\y[M]. y\A --> x \ y)))" cartprod :: "[i=>o,i,i,i] => o" - "cartprod(M,A,B,z) == + "cartprod(M,A,B,z) == \u[M]. u \ z <-> (\x[M]. x\A & (\y[M]. y\B & pair(M,x,y,u)))" is_sum :: "[i=>o,i,i,i] => o" - "is_sum(M,A,B,Z) == - \A0[M]. \n1[M]. \s1[M]. \B1[M]. + "is_sum(M,A,B,Z) == + \A0[M]. \n1[M]. \s1[M]. \B1[M]. number1(M,n1) & cartprod(M,n1,A,A0) & upair(M,n1,n1,s1) & cartprod(M,s1,B,B1) & union(M,A0,B1,Z)" @@ -83,73 +83,73 @@ "is_Inr(M,a,z) == \n1[M]. number1(M,n1) & pair(M,n1,a,z)" is_converse :: "[i=>o,i,i] => o" - "is_converse(M,r,z) == - \x[M]. x \ z <-> + "is_converse(M,r,z) == + \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) == + "pre_image(M,r,A,z) == \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) == + "is_domain(M,r,z) == \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) == + "image(M,r,A,z) == \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 + --{*the cleaner @{term "\r'[M]. is_converse(M,r,r') & is_domain(M,r',z)"} - unfortunately needs an instance of separation in order to prove + unfortunately needs an instance of separation in order to prove @{term "M(converse(r))"}.*} - "is_range(M,r,z) == + "is_range(M,r,z) == \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) == - \dr[M]. \rr[M]. is_domain(M,r,dr) & is_range(M,r,rr) & + "is_field(M,r,z) == + \dr[M]. \rr[M]. is_domain(M,r,dr) & is_range(M,r,rr) & union(M,dr,rr,z)" is_relation :: "[i=>o,i] => o" - "is_relation(M,r) == + "is_relation(M,r) == (\z[M]. z\r --> (\x[M]. \y[M]. pair(M,x,y,z)))" is_function :: "[i=>o,i] => o" - "is_function(M,r) == - \x[M]. \y[M]. \y'[M]. \p[M]. \p'[M]. + "is_function(M,r) == + \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) == - (\xs[M]. \fxs[M]. + "fun_apply(M,f,x,y) == + (\xs[M]. \fxs[M]. upair(M,x,x,xs) & image(M,f,xs,fxs) & big_union(M,fxs,y))" typed_function :: "[i=>o,i,i,i] => o" - "typed_function(M,A,B,r) == + "typed_function(M,A,B,r) == is_function(M,r) & is_relation(M,r) & is_domain(M,r,A) & (\u[M]. u\r --> (\x[M]. \y[M]. pair(M,x,y,u) --> y\B))" is_funspace :: "[i=>o,i,i,i] => o" - "is_funspace(M,A,B,F) == + "is_funspace(M,A,B,F) == \f[M]. f \ F <-> typed_function(M,A,B,f)" composition :: "[i=>o,i,i,i] => o" - "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) & + "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)" injection :: "[i=>o,i,i,i] => o" - "injection(M,A,B,f) == + "injection(M,A,B,f) == typed_function(M,A,B,f) & - (\x[M]. \x'[M]. \y[M]. \p[M]. \p'[M]. + (\x[M]. \x'[M]. \y[M]. \p[M]. \p'[M]. pair(M,x,y,p) --> pair(M,x',y,p') --> p\f --> p'\f --> x=x')" surjection :: "[i=>o,i,i,i] => o" - "surjection(M,A,B,f) == + "surjection(M,A,B,f) == typed_function(M,A,B,f) & (\y[M]. y\B --> (\x[M]. x\A & fun_apply(M,f,x,y)))" @@ -157,7 +157,7 @@ "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) == + "restriction(M,r,A,z) == \x[M]. x \ z <-> (x \ r & (\u[M]. u\A & (\v[M]. pair(M,u,v,x))))" transitive_set :: "[i=>o,i] => o" @@ -169,19 +169,19 @@ 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) & + "limit_ordinal(M,a) == + ordinal(M,a) & ~ empty(M,a) & (\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*} - "successor_ordinal(M,a) == + "successor_ordinal(M,a) == ordinal(M,a) & ~ empty(M,a) & ~ limit_ordinal(M,a)" finite_ordinal :: "[i=>o,i] => o" --{*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) & + "finite_ordinal(M,a) == + ordinal(M,a) & ~ limit_ordinal(M,a) & (\x[M]. x\a --> ~ limit_ordinal(M,x))" omega :: "[i=>o,i] => o" @@ -192,7 +192,7 @@ "is_quasinat(M,z) == empty(M,z) | (\m[M]. successor(M,m,z))" is_nat_case :: "[i=>o, i, [i,i]=>o, i, i] => o" - "is_nat_case(M, a, is_b, k, z) == + "is_nat_case(M, a, is_b, k, z) == (empty(M,k) --> z=a) & (\m[M]. successor(M,m,k) --> is_b(m,z)) & (is_quasinat(M,k) | empty(M,z))" @@ -202,7 +202,7 @@ Relativize1 :: "[i=>o, i, [i,i]=>o, i=>i] => o" --{*as above, but typed*} - "Relativize1(M,A,is_f,f) == + "Relativize1(M,A,is_f,f) == \x[M]. \y[M]. x\A --> is_f(x,y) <-> y = f(x)" relativize2 :: "[i=>o, [i,i,i]=>o, [i,i]=>i] => o" @@ -213,42 +213,42 @@ \x[M]. \y[M]. \z[M]. x\A --> y\B --> is_f(x,y,z) <-> z = f(x,y)" relativize3 :: "[i=>o, [i,i,i,i]=>o, [i,i,i]=>i] => o" - "relativize3(M,is_f,f) == + "relativize3(M,is_f,f) == \x[M]. \y[M]. \z[M]. \u[M]. is_f(x,y,z,u) <-> u = f(x,y,z)" Relativize3 :: "[i=>o, i, i, i, [i,i,i,i]=>o, [i,i,i]=>i] => o" - "Relativize3(M,A,B,C,is_f,f) == - \x[M]. \y[M]. \z[M]. \u[M]. + "Relativize3(M,A,B,C,is_f,f) == + \x[M]. \y[M]. \z[M]. \u[M]. x\A --> y\B --> z\C --> is_f(x,y,z,u) <-> u = f(x,y,z)" relativize4 :: "[i=>o, [i,i,i,i,i]=>o, [i,i,i,i]=>i] => o" - "relativize4(M,is_f,f) == + "relativize4(M,is_f,f) == \u[M]. \x[M]. \y[M]. \z[M]. \a[M]. is_f(u,x,y,z,a) <-> a = f(u,x,y,z)" text{*Useful when absoluteness reasoning has replaced the predicates by terms*} lemma triv_Relativize1: "Relativize1(M, A, \x y. y = f(x), f)" -by (simp add: Relativize1_def) +by (simp add: Relativize1_def) lemma triv_Relativize2: "Relativize2(M, A, B, \x y a. a = f(x,y), f)" -by (simp add: Relativize2_def) +by (simp add: Relativize2_def) subsection {*The relativized ZF axioms*} constdefs extensionality :: "(i=>o) => o" - "extensionality(M) == + "extensionality(M) == \x[M]. \y[M]. (\z[M]. z \ x <-> z \ y) --> x=y" separation :: "[i=>o, i=>o] => o" --{*The formula @{text P} should only involve parameters - belonging to @{text M}. But we can't prove separation as a scheme - anyway. Every instance that we need must individually be assumed - and later proved.*} - "separation(M,P) == + belonging to @{text M} and all its quantifiers must be relativized + to @{text M}. We do not have separation as a scheme; every instance + that we need must be assumed (and later proved) separately.*} + "separation(M,P) == \z[M]. \y[M]. \x[M]. x \ y <-> x \ z & P(x)" upair_ax :: "(i=>o) => o" @@ -261,73 +261,73 @@ "power_ax(M) == \x[M]. \z[M]. powerset(M,x,z)" univalent :: "[i=>o, i, [i,i]=>o] => o" - "univalent(M,A,P) == - (\x[M]. x\A --> (\y[M]. \z[M]. P(x,y) & P(x,z) --> y=z))" + "univalent(M,A,P) == + \x[M]. x\A --> (\y[M]. \z[M]. P(x,y) & P(x,z) --> y=z)" replacement :: "[i=>o, [i,i]=>o] => o" - "replacement(M,P) == + "replacement(M,P) == \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) == + "strong_replacement(M,P) == \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) == + "foundation_ax(M) == \x[M]. (\y[M]. y\x) --> (\y[M]. y\x & ~(\z[M]. z\x & z \ y))" subsection{*A trivial consistency proof for $V_\omega$ *} -text{*We prove that $V_\omega$ +text{*We prove that $V_\omega$ (or @{text univ} in Isabelle) satisfies some ZF axioms. Kunen, Theorem IV 3.13, page 123.*} lemma univ0_downwards_mem: "[| y \ x; x \ univ(0) |] ==> y \ univ(0)" -apply (insert Transset_univ [OF Transset_0]) -apply (simp add: Transset_def, blast) +apply (insert Transset_univ [OF Transset_0]) +apply (simp add: Transset_def, blast) done -lemma univ0_Ball_abs [simp]: - "A \ univ(0) ==> (\x\A. x \ univ(0) --> P(x)) <-> (\x\A. P(x))" -by (blast intro: univ0_downwards_mem) +lemma univ0_Ball_abs [simp]: + "A \ univ(0) ==> (\x\A. x \ univ(0) --> P(x)) <-> (\x\A. P(x))" +by (blast intro: univ0_downwards_mem) -lemma univ0_Bex_abs [simp]: - "A \ univ(0) ==> (\x\A. x \ univ(0) & P(x)) <-> (\x\A. P(x))" -by (blast intro: univ0_downwards_mem) +lemma univ0_Bex_abs [simp]: + "A \ univ(0) ==> (\x\A. x \ univ(0) & P(x)) <-> (\x\A. P(x))" +by (blast intro: univ0_downwards_mem) text{*Congruence rule for separation: can assume the variable is in @{text M}*} lemma separation_cong [cong]: - "(!!x. M(x) ==> P(x) <-> P'(x)) + "(!!x. M(x) ==> P(x) <-> P'(x)) ==> separation(M, %x. P(x)) <-> separation(M, %x. P'(x))" -by (simp add: separation_def) +by (simp add: separation_def) lemma univalent_cong [cong]: - "[| A=A'; !!x y. [| x\A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] + "[| A=A'; !!x y. [| x\A; M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] ==> univalent(M, A, %x y. P(x,y)) <-> univalent(M, A', %x y. P'(x,y))" -by (simp add: univalent_def) +by (simp add: univalent_def) lemma univalent_triv [intro,simp]: "univalent(M, A, \x y. y = f(x))" -by (simp add: univalent_def) +by (simp add: univalent_def) lemma univalent_conjI2 [intro,simp]: "univalent(M,A,Q) ==> univalent(M, A, \x y. P(x,y) & Q(x,y))" -by (simp add: univalent_def, blast) +by (simp add: univalent_def, blast) text{*Congruence rule for replacement*} lemma strong_replacement_cong [cong]: - "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] - ==> strong_replacement(M, %x y. P(x,y)) <-> - strong_replacement(M, %x y. P'(x,y))" -by (simp add: strong_replacement_def) + "[| !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y) |] + ==> strong_replacement(M, %x y. P(x,y)) <-> + strong_replacement(M, %x y. P'(x,y))" +by (simp add: strong_replacement_def) text{*The extensionality axiom*} lemma "extensionality(\x. x \ univ(0))" apply (simp add: extensionality_def) -apply (blast intro: univ0_downwards_mem) +apply (blast intro: univ0_downwards_mem) done text{*The separation axiom requires some lemmas*} @@ -339,7 +339,7 @@ done lemma Collect_in_VLimit: - "[| X \ Vfrom(A,i); Limit(i); Transset(A) |] + "[| X \ Vfrom(A,i); Limit(i); Transset(A) |] ==> Collect(X,P) \ Vfrom(A,i)" apply (rule Limit_VfromE, assumption+) apply (blast intro: Limit_has_succ VfromI Collect_in_Vfrom) @@ -350,23 +350,23 @@ by (simp add: univ_def Collect_in_VLimit Limit_nat) lemma "separation(\x. x \ univ(0), P)" -apply (simp add: separation_def, clarify) -apply (rule_tac x = "Collect(z,P)" in bexI) +apply (simp add: separation_def, clarify) +apply (rule_tac x = "Collect(z,P)" in bexI) apply (blast intro: Collect_in_univ Transset_0)+ done text{*Unordered pairing axiom*} lemma "upair_ax(\x. x \ univ(0))" -apply (simp add: upair_ax_def upair_def) -apply (blast intro: doubleton_in_univ) +apply (simp add: upair_ax_def upair_def) +apply (blast intro: doubleton_in_univ) done text{*Union axiom*} -lemma "Union_ax(\x. x \ univ(0))" -apply (simp add: Union_ax_def big_union_def, clarify) -apply (rule_tac x="\x" in bexI) +lemma "Union_ax(\x. x \ univ(0))" +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) +apply (blast intro: Union_in_univ Transset_0) done text{*Powerset axiom*} @@ -376,88 +376,88 @@ apply (simp add: univ_def Pow_in_VLimit Limit_nat) done -lemma "power_ax(\x. x \ univ(0))" -apply (simp add: power_ax_def powerset_def subset_def, clarify) +lemma "power_ax(\x. x \ univ(0))" +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) +apply (blast intro: Pow_in_univ Transset_0) done text{*Foundation axiom*} -lemma "foundation_ax(\x. x \ univ(0))" +lemma "foundation_ax(\x. x \ univ(0))" apply (simp add: foundation_ax_def, clarify) -apply (cut_tac A=x in foundation) +apply (cut_tac A=x in foundation) apply (blast intro: univ0_downwards_mem) done -lemma "replacement(\x. x \ univ(0), P)" -apply (simp add: replacement_def, clarify) +lemma "replacement(\x. x \ univ(0), P)" +apply (simp add: replacement_def, clarify) oops text{*no idea: maybe prove by induction on the rank of A?*} text{*Still missing: Replacement, Choice*} -subsection{*lemmas needed to reduce some set constructions to instances +subsection{*Lemmas Needed to Reduce Some Set Constructions to Instances of Separation*} lemma image_iff_Collect: "r `` A = {y \ Union(Union(r)). \p\r. \x\A. p=}" -apply (rule equalityI, auto) -apply (simp add: Pair_def, blast) +apply (rule equalityI, auto) +apply (simp add: Pair_def, blast) done lemma vimage_iff_Collect: "r -`` A = {x \ Union(Union(r)). \p\r. \y\A. p=}" -apply (rule equalityI, auto) -apply (simp add: Pair_def, blast) +apply (rule equalityI, auto) +apply (simp add: Pair_def, blast) done -text{*These two lemmas lets us prove @{text domain_closed} and +text{*These two lemmas lets us prove @{text domain_closed} and @{text range_closed} without new instances of separation*} lemma domain_eq_vimage: "domain(r) = r -`` Union(Union(r))" apply (rule equalityI, auto) apply (rule vimageI, assumption) -apply (simp add: Pair_def, blast) +apply (simp add: Pair_def, blast) done lemma range_eq_image: "range(r) = r `` Union(Union(r))" apply (rule equalityI, auto) apply (rule imageI, assumption) -apply (simp add: Pair_def, blast) +apply (simp add: Pair_def, blast) done lemma replacementD: "[| replacement(M,P); M(A); univalent(M,A,P) |] ==> \Y[M]. (\b[M]. ((\x[M]. x\A & P(x,b)) --> b \ Y))" -by (simp add: replacement_def) +by (simp add: replacement_def) lemma strong_replacementD: "[| strong_replacement(M,P); M(A); univalent(M,A,P) |] ==> \Y[M]. (\b[M]. (b \ Y <-> (\x[M]. x\A & P(x,b))))" -by (simp add: strong_replacement_def) +by (simp add: strong_replacement_def) lemma separationD: "[| separation(M,P); M(z) |] ==> \y[M]. \x[M]. x \ y <-> x \ z & P(x)" -by (simp add: separation_def) +by (simp add: separation_def) text{*More constants, for order types*} constdefs order_isomorphism :: "[i=>o,i,i,i,i,i] => o" - "order_isomorphism(M,A,r,B,s,f) == - bijection(M,A,B,f) & + "order_isomorphism(M,A,r,B,s,f) == + bijection(M,A,B,f) & (\x[M]. x\A --> (\y[M]. y\A --> (\p[M]. \fx[M]. \fy[M]. \q[M]. - pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) --> + pair(M,x,y,p) --> fun_apply(M,f,x,fx) --> fun_apply(M,f,y,fy) --> pair(M,fx,fy,q) --> (p\r <-> q\s))))" pred_set :: "[i=>o,i,i,i,i] => o" - "pred_set(M,A,x,r,B) == + "pred_set(M,A,x,r,B) == \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) == + "membership(M,A,r) == \p[M]. p \ r <-> (\x[M]. x\A & (\y[M]. y\A & x\y & pair(M,x,y,p)))" @@ -468,67 +468,72 @@ locale M_trivial = fixes M assumes transM: "[| y\x; M(x) |] ==> M(y)" - and nonempty [simp]: "M(0)" and upair_ax: "upair_ax(M)" and Union_ax: "Union_ax(M)" and power_ax: "power_ax(M)" and replacement: "replacement(M,P)" and M_nat [iff]: "M(nat)" (*i.e. the axiom of infinity*) -lemma (in M_trivial) rall_abs [simp]: - "M(A) ==> (\x[M]. x\A --> P(x)) <-> (\x\A. P(x))" -by (blast intro: transM) + +text{*Automatically discovers the proof using @{text transM}, @{text nat_0I} +and @{text M_nat}.*} +lemma (in M_trivial) nonempty [simp]: "M(0)" +by (blast intro: transM) -lemma (in M_trivial) rex_abs [simp]: - "M(A) ==> (\x[M]. x\A & P(x)) <-> (\x\A. P(x))" -by (blast intro: transM) +lemma (in M_trivial) rall_abs [simp]: + "M(A) ==> (\x[M]. x\A --> P(x)) <-> (\x\A. P(x))" +by (blast intro: transM) -lemma (in M_trivial) ball_iff_equiv: - "M(A) ==> (\x[M]. (x\A <-> P(x))) <-> - (\x\A. P(x)) & (\x. P(x) --> M(x) --> x\A)" +lemma (in M_trivial) rex_abs [simp]: + "M(A) ==> (\x[M]. x\A & P(x)) <-> (\x\A. P(x))" +by (blast intro: transM) + +lemma (in M_trivial) ball_iff_equiv: + "M(A) ==> (\x[M]. (x\A <-> P(x))) <-> + (\x\A. P(x)) & (\x. P(x) --> M(x) --> x\A)" by (blast intro: transM) text{*Simplifies proofs of equalities when there's an iff-equality available for rewriting, universally quantified over M. *} -lemma (in M_trivial) M_equalityI: +lemma (in M_trivial) M_equalityI: "[| !!x. M(x) ==> x\A <-> x\B; M(A); M(B) |] ==> A=B" -by (blast intro!: equalityI dest: transM) +by (blast intro!: equalityI dest: transM) subsubsection{*Trivial Absoluteness Proofs: Empty Set, Pairs, etc.*} -lemma (in M_trivial) empty_abs [simp]: +lemma (in M_trivial) empty_abs [simp]: "M(z) ==> empty(M,z) <-> z=0" apply (simp add: empty_def) -apply (blast intro: transM) +apply (blast intro: transM) done -lemma (in M_trivial) subset_abs [simp]: +lemma (in M_trivial) subset_abs [simp]: "M(A) ==> subset(M,A,B) <-> A \ B" -apply (simp add: subset_def) -apply (blast intro: transM) +apply (simp add: subset_def) +apply (blast intro: transM) done -lemma (in M_trivial) upair_abs [simp]: +lemma (in M_trivial) upair_abs [simp]: "M(z) ==> upair(M,a,b,z) <-> z={a,b}" -apply (simp add: upair_def) -apply (blast intro: transM) +apply (simp add: upair_def) +apply (blast intro: transM) done lemma (in M_trivial) upair_in_M_iff [iff]: "M({a,b}) <-> M(a) & M(b)" -apply (insert upair_ax, simp add: upair_ax_def) -apply (blast intro: transM) +apply (insert upair_ax, simp add: upair_ax_def) +apply (blast intro: transM) done lemma (in M_trivial) singleton_in_M_iff [iff]: "M({a}) <-> M(a)" -by (insert upair_in_M_iff [of a a], simp) +by (insert upair_in_M_iff [of a a], simp) -lemma (in M_trivial) pair_abs [simp]: +lemma (in M_trivial) pair_abs [simp]: "M(z) ==> pair(M,a,b,z) <-> z=" apply (simp add: pair_def ZF.Pair_def) -apply (blast intro: transM) +apply (blast intro: transM) done lemma (in M_trivial) pair_in_M_iff [iff]: @@ -538,84 +543,84 @@ lemma (in M_trivial) pair_components_in_M: "[| \ A; M(A) |] ==> M(x) & M(y)" apply (simp add: Pair_def) -apply (blast dest: transM) +apply (blast dest: transM) done -lemma (in M_trivial) cartprod_abs [simp]: +lemma (in M_trivial) cartprod_abs [simp]: "[| M(A); M(B); M(z) |] ==> cartprod(M,A,B,z) <-> z = A*B" apply (simp add: cartprod_def) -apply (rule iffI) - apply (blast intro!: equalityI intro: transM dest!: rspec) -apply (blast dest: transM) +apply (rule iffI) + apply (blast intro!: equalityI intro: transM dest!: rspec) +apply (blast dest: transM) done subsubsection{*Absoluteness for Unions and Intersections*} -lemma (in M_trivial) union_abs [simp]: +lemma (in M_trivial) union_abs [simp]: "[| M(a); M(b); M(z) |] ==> union(M,a,b,z) <-> z = a Un b" -apply (simp add: union_def) -apply (blast intro: transM) +apply (simp add: union_def) +apply (blast intro: transM) done -lemma (in M_trivial) inter_abs [simp]: +lemma (in M_trivial) inter_abs [simp]: "[| M(a); M(b); M(z) |] ==> inter(M,a,b,z) <-> z = a Int b" -apply (simp add: inter_def) -apply (blast intro: transM) +apply (simp add: inter_def) +apply (blast intro: transM) done -lemma (in M_trivial) setdiff_abs [simp]: +lemma (in M_trivial) setdiff_abs [simp]: "[| M(a); M(b); M(z) |] ==> setdiff(M,a,b,z) <-> z = a-b" -apply (simp add: setdiff_def) -apply (blast intro: transM) +apply (simp add: setdiff_def) +apply (blast intro: transM) done -lemma (in M_trivial) Union_abs [simp]: +lemma (in M_trivial) Union_abs [simp]: "[| M(A); M(z) |] ==> big_union(M,A,z) <-> z = Union(A)" -apply (simp add: big_union_def) -apply (blast intro!: equalityI dest: transM) +apply (simp add: big_union_def) +apply (blast intro!: equalityI dest: transM) done lemma (in M_trivial) Union_closed [intro,simp]: "M(A) ==> M(Union(A))" -by (insert Union_ax, simp add: Union_ax_def) +by (insert Union_ax, simp add: Union_ax_def) lemma (in M_trivial) Un_closed [intro,simp]: "[| M(A); M(B) |] ==> M(A Un B)" -by (simp only: Un_eq_Union, blast) +by (simp only: Un_eq_Union, blast) lemma (in M_trivial) cons_closed [intro,simp]: "[| M(a); M(A) |] ==> M(cons(a,A))" -by (subst cons_eq [symmetric], blast) +by (subst cons_eq [symmetric], blast) -lemma (in M_trivial) cons_abs [simp]: +lemma (in M_trivial) cons_abs [simp]: "[| M(b); M(z) |] ==> is_cons(M,a,b,z) <-> z = cons(a,b)" -by (simp add: is_cons_def, blast intro: transM) +by (simp add: is_cons_def, blast intro: transM) -lemma (in M_trivial) successor_abs [simp]: +lemma (in M_trivial) successor_abs [simp]: "[| M(a); M(z) |] ==> successor(M,a,z) <-> z = succ(a)" -by (simp add: successor_def, blast) +by (simp add: successor_def, blast) lemma (in M_trivial) succ_in_M_iff [iff]: "M(succ(a)) <-> M(a)" -apply (simp add: succ_def) -apply (blast intro: transM) +apply (simp add: succ_def) +apply (blast intro: transM) done subsubsection{*Absoluteness for Separation and Replacement*} lemma (in M_trivial) separation_closed [intro,simp]: "[| separation(M,P); M(A) |] ==> M(Collect(A,P))" -apply (insert separation, simp add: separation_def) -apply (drule rspec, assumption, clarify) +apply (insert separation, simp add: separation_def) +apply (drule rspec, assumption, clarify) apply (subgoal_tac "y = Collect(A,P)", blast) -apply (blast dest: transM) +apply (blast dest: transM) done lemma separation_iff: "separation(M,P) <-> (\z[M]. \y[M]. is_Collect(M,z,P,y))" -by (simp add: separation_def is_Collect_def) +by (simp add: separation_def is_Collect_def) -lemma (in M_trivial) Collect_abs [simp]: +lemma (in M_trivial) Collect_abs [simp]: "[| M(A); M(z) |] ==> is_Collect(M,A,P,z) <-> z = Collect(A,P)" apply (simp add: is_Collect_def) apply (blast intro!: equalityI dest: transM) @@ -625,70 +630,68 @@ lemma (in M_trivial) strong_replacementI [rule_format]: "[| \A[M]. separation(M, %u. \x[M]. 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 rspec, clarify) -apply (drule_tac z=Y in separationD, assumption, clarify) -apply (rule_tac x=y in rexI) -apply (blast dest: transM)+ +apply (simp add: strong_replacement_def, clarify) +apply (frule replacementD [OF replacement], assumption, clarify) +apply (drule_tac x=A in rspec, clarify) +apply (drule_tac z=Y in separationD, assumption, clarify) +apply (rule_tac x=y in rexI, force, assumption) done - subsubsection{*The Operator @{term is_Replace}*} lemma is_Replace_cong [cong]: - "[| A=A'; + "[| A=A'; !!x y. [| M(x); M(y) |] ==> P(x,y) <-> P'(x,y); - z=z' |] - ==> is_Replace(M, A, %x y. P(x,y), z) <-> - is_Replace(M, A', %x y. P'(x,y), z')" -by (simp add: is_Replace_def) + z=z' |] + ==> is_Replace(M, A, %x y. P(x,y), z) <-> + is_Replace(M, A', %x y. P'(x,y), z')" +by (simp add: is_Replace_def) -lemma (in M_trivial) univalent_Replace_iff: +lemma (in M_trivial) univalent_Replace_iff: "[| M(A); univalent(M,A,P); - !!x y. [| x\A; P(x,y) |] ==> M(y) |] + !!x y. [| x\A; P(x,y) |] ==> M(y) |] ==> u \ Replace(A,P) <-> (\x. x\A & P(x,u))" -apply (simp add: Replace_iff univalent_def) +apply (simp add: Replace_iff univalent_def) apply (blast dest: transM) done (*The last premise expresses that P takes M to M*) lemma (in M_trivial) strong_replacement_closed [intro,simp]: - "[| strong_replacement(M,P); M(A); univalent(M,A,P); + "[| strong_replacement(M,P); M(A); univalent(M,A,P); !!x y. [| x\A; P(x,y) |] ==> M(y) |] ==> M(Replace(A,P))" -apply (simp add: strong_replacement_def) -apply (drule_tac x=A in rspec, safe) +apply (simp add: strong_replacement_def) +apply (drule_tac x=A in rspec, safe) apply (subgoal_tac "Replace(A,P) = Y") - apply simp + apply simp apply (rule equality_iffI) apply (simp add: univalent_Replace_iff) -apply (blast dest: transM) +apply (blast dest: transM) done -lemma (in M_trivial) Replace_abs: +lemma (in M_trivial) Replace_abs: "[| M(A); M(z); univalent(M,A,P); strong_replacement(M, P); - !!x y. [| x\A; P(x,y) |] ==> M(y) |] + !!x y. [| x\A; P(x,y) |] ==> M(y) |] ==> is_Replace(M,A,P,z) <-> z = Replace(A,P)" apply (simp add: is_Replace_def) -apply (rule iffI) -apply (rule M_equalityI) -apply (simp_all add: univalent_Replace_iff, blast, blast) +apply (rule iffI) +apply (rule M_equalityI) +apply (simp_all add: univalent_Replace_iff, blast, blast) done (*The first premise can't simply be assumed as a schema. It is essential to take care when asserting instances of Replacement. Let K be a nonconstructible subset of nat and define - f(x) = x if x:K and f(x)=0 otherwise. Then RepFun(nat,f) = cons(0,K), a + f(x) = x if x:K and f(x)=0 otherwise. Then RepFun(nat,f) = cons(0,K), a nonconstructible set. So we cannot assume that M(X) implies M(RepFun(X,f)) even for f : M -> M. *) lemma (in M_trivial) RepFun_closed: "[| strong_replacement(M, \x y. y = f(x)); M(A); \x\A. M(f(x)) |] ==> M(RepFun(A,f))" -apply (simp add: RepFun_def) -apply (rule strong_replacement_closed) -apply (auto dest: transM simp add: univalent_def) +apply (simp add: RepFun_def) +apply (rule strong_replacement_closed) +apply (auto dest: transM simp add: univalent_def) done lemma Replace_conj_eq: "{y . x \ A, x\A & y=f(x)} = {y . x\A, y=f(x)}" @@ -701,69 +704,69 @@ ==> M(RepFun(A, %x. f(x)))" apply (simp add: RepFun_def) apply (frule strong_replacement_closed, assumption) -apply (auto dest: transM simp add: Replace_conj_eq univalent_def) +apply (auto dest: transM simp add: Replace_conj_eq univalent_def) done subsubsection {*Absoluteness for @{term Lambda}*} constdefs is_lambda :: "[i=>o, i, [i,i]=>o, i] => o" - "is_lambda(M, A, is_b, z) == + "is_lambda(M, A, is_b, z) == \p[M]. p \ z <-> (\u[M]. \v[M]. u\A & pair(M,u,v,p) & is_b(u,v))" lemma (in M_trivial) lam_closed: "[| strong_replacement(M, \x y. y = ); M(A); \x\A. M(b(x)) |] ==> M(\x\A. b(x))" -by (simp add: lam_def, blast intro: RepFun_closed dest: transM) +by (simp add: lam_def, blast intro: RepFun_closed dest: transM) text{*Better than @{text lam_closed}: has the formula @{term "x\A"}*} lemma (in M_trivial) lam_closed2: "[|strong_replacement(M, \x y. x\A & y = \x, b(x)\); M(A); \m[M]. m\A --> M(b(m))|] ==> M(Lambda(A,b))" apply (simp add: lam_def) -apply (blast intro: RepFun_closed2 dest: transM) +apply (blast intro: RepFun_closed2 dest: transM) done -lemma (in M_trivial) lambda_abs2 [simp]: +lemma (in M_trivial) lambda_abs2 [simp]: "[| strong_replacement(M, \x y. x\A & y = \x, b(x)\); - Relativize1(M,A,is_b,b); M(A); \m[M]. m\A --> M(b(m)); M(z) |] + Relativize1(M,A,is_b,b); M(A); \m[M]. m\A --> M(b(m)); M(z) |] ==> is_lambda(M,A,is_b,z) <-> z = Lambda(A,b)" apply (simp add: Relativize1_def is_lambda_def) apply (rule iffI) - prefer 2 apply (simp add: lam_def) + prefer 2 apply (simp add: lam_def) apply (rule M_equalityI) - apply (simp add: lam_def) + apply (simp add: lam_def) apply (simp add: lam_closed2)+ done lemma is_lambda_cong [cong]: - "[| A=A'; z=z'; - !!x y. [| x\A; M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |] - ==> is_lambda(M, A, %x y. is_b(x,y), z) <-> - is_lambda(M, A', %x y. is_b'(x,y), z')" -by (simp add: is_lambda_def) + "[| A=A'; z=z'; + !!x y. [| x\A; M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |] + ==> is_lambda(M, A, %x y. is_b(x,y), z) <-> + is_lambda(M, A', %x y. is_b'(x,y), z')" +by (simp add: is_lambda_def) -lemma (in M_trivial) image_abs [simp]: +lemma (in M_trivial) image_abs [simp]: "[| M(r); M(A); M(z) |] ==> image(M,r,A,z) <-> z = r``A" apply (simp add: image_def) -apply (rule iffI) - apply (blast intro!: equalityI dest: transM, blast) +apply (rule iffI) + apply (blast intro!: equalityI dest: transM, blast) done text{*What about @{text Pow_abs}? Powerset is NOT absolute! This result is one direction of absoluteness.*} -lemma (in M_trivial) powerset_Pow: +lemma (in M_trivial) powerset_Pow: "powerset(M, x, Pow(x))" by (simp add: powerset_def) text{*But we can't prove that the powerset in @{text M} includes the real powerset.*} -lemma (in M_trivial) powerset_imp_subset_Pow: +lemma (in M_trivial) powerset_imp_subset_Pow: "[| powerset(M,x,y); M(y) |] ==> y <= Pow(x)" -apply (simp add: powerset_def) -apply (blast dest: transM) +apply (simp add: powerset_def) +apply (blast dest: transM) done subsubsection{*Absoluteness for the Natural Numbers*} @@ -774,126 +777,123 @@ lemma (in M_trivial) nat_case_closed [intro,simp]: "[|M(k); M(a); \m[M]. M(b(m))|] ==> M(nat_case(a,b,k))" -apply (case_tac "k=0", simp) +apply (case_tac "k=0", simp) apply (case_tac "\m. k = succ(m)", force) -apply (simp add: nat_case_def) +apply (simp add: nat_case_def) done -lemma (in M_trivial) quasinat_abs [simp]: +lemma (in M_trivial) quasinat_abs [simp]: "M(z) ==> is_quasinat(M,z) <-> quasinat(z)" by (auto simp add: is_quasinat_def quasinat_def) -lemma (in M_trivial) nat_case_abs [simp]: - "[| relativize1(M,is_b,b); M(k); M(z) |] +lemma (in M_trivial) nat_case_abs [simp]: + "[| relativize1(M,is_b,b); M(k); M(z) |] ==> is_nat_case(M,a,is_b,k,z) <-> z = nat_case(a,b,k)" -apply (case_tac "quasinat(k)") - prefer 2 - apply (simp add: is_nat_case_def non_nat_case) - apply (force simp add: quasinat_def) +apply (case_tac "quasinat(k)") + prefer 2 + apply (simp add: is_nat_case_def non_nat_case) + apply (force simp add: quasinat_def) apply (simp add: quasinat_def is_nat_case_def) -apply (elim disjE exE) - apply (simp_all add: relativize1_def) +apply (elim disjE exE) + apply (simp_all add: relativize1_def) done -(*NOT for the simplifier. The assumption M(z') is apparently necessary, but +(*NOT for the simplifier. The assumption M(z') is apparently necessary, but causes the error "Failed congruence proof!" It may be better to replace is_nat_case by nat_case before attempting congruence reasoning.*) lemma is_nat_case_cong: "[| a = a'; k = k'; z = z'; M(z'); !!x y. [| M(x); M(y) |] ==> is_b(x,y) <-> is_b'(x,y) |] ==> is_nat_case(M, a, is_b, k, z) <-> is_nat_case(M, a', is_b', k', z')" -by (simp add: is_nat_case_def) +by (simp add: is_nat_case_def) subsection{*Absoluteness for Ordinals*} text{*These results constitute Theorem IV 5.1 of Kunen (page 126).*} lemma (in M_trivial) lt_closed: - "[| j M(j)" -by (blast dest: ltD intro: transM) + "[| j M(j)" +by (blast dest: ltD intro: transM) -lemma (in M_trivial) transitive_set_abs [simp]: +lemma (in M_trivial) transitive_set_abs [simp]: "M(a) ==> transitive_set(M,a) <-> Transset(a)" by (simp add: transitive_set_def Transset_def) -lemma (in M_trivial) ordinal_abs [simp]: +lemma (in M_trivial) ordinal_abs [simp]: "M(a) ==> ordinal(M,a) <-> Ord(a)" by (simp add: ordinal_def Ord_def) -lemma (in M_trivial) limit_ordinal_abs [simp]: - "M(a) ==> limit_ordinal(M,a) <-> Limit(a)" -apply (unfold Limit_def limit_ordinal_def) -apply (simp add: Ord_0_lt_iff) -apply (simp add: lt_def, blast) +lemma (in M_trivial) limit_ordinal_abs [simp]: + "M(a) ==> limit_ordinal(M,a) <-> Limit(a)" +apply (unfold Limit_def limit_ordinal_def) +apply (simp add: Ord_0_lt_iff) +apply (simp add: lt_def, blast) done -lemma (in M_trivial) successor_ordinal_abs [simp]: +lemma (in M_trivial) successor_ordinal_abs [simp]: "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) +apply (drule Ord_cases_disj, auto) done lemma finite_Ord_is_nat: "[| Ord(a); ~ Limit(a); \x\a. ~ Limit(x) |] ==> a \ nat" by (induct a rule: trans_induct3, simp_all) -lemma naturals_not_limit: "a \ nat ==> ~ Limit(a)" -by (induct a rule: nat_induct, auto) - -lemma (in M_trivial) finite_ordinal_abs [simp]: +lemma (in M_trivial) finite_ordinal_abs [simp]: "M(a) ==> finite_ordinal(M,a) <-> a \ nat" apply (simp add: finite_ordinal_def) -apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord +apply (blast intro: finite_Ord_is_nat intro: nat_into_Ord dest: Ord_trans naturals_not_limit) done lemma Limit_non_Limit_implies_nat: "[| Limit(a); \x\a. ~ Limit(x) |] ==> a = nat" -apply (rule le_anti_sym) -apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord) - apply (simp add: lt_def) - apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) +apply (rule le_anti_sym) +apply (rule all_lt_imp_le, blast, blast intro: Limit_is_Ord) + apply (simp add: lt_def) + apply (blast intro: Ord_in_Ord Ord_trans finite_Ord_is_nat) apply (erule nat_le_Limit) done -lemma (in M_trivial) omega_abs [simp]: +lemma (in M_trivial) omega_abs [simp]: "M(a) ==> omega(M,a) <-> a = nat" -apply (simp add: omega_def) +apply (simp add: omega_def) apply (blast intro: Limit_non_Limit_implies_nat dest: naturals_not_limit) done -lemma (in M_trivial) number1_abs [simp]: +lemma (in M_trivial) number1_abs [simp]: "M(a) ==> number1(M,a) <-> a = 1" -by (simp add: number1_def) +by (simp add: number1_def) -lemma (in M_trivial) number2_abs [simp]: +lemma (in M_trivial) number2_abs [simp]: "M(a) ==> number2(M,a) <-> a = succ(1)" -by (simp add: number2_def) +by (simp add: number2_def) -lemma (in M_trivial) number3_abs [simp]: +lemma (in M_trivial) number3_abs [simp]: "M(a) ==> number3(M,a) <-> a = succ(succ(1))" -by (simp add: number3_def) +by (simp add: number3_def) text{*Kunen continued to 20...*} -(*Could not get this to work. The \x\nat is essential because everything +(*Could not get this to work. The \x\nat is essential because everything but the recursion variable must stay unchanged. But then the recursion - equations only hold for x\nat (or in some other set) and not for the + equations only hold for x\nat (or in some other set) and not for the whole of the class M. consts natnumber_aux :: "[i=>o,i] => i" 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]. natnumber_aux(M,n)`y=1 & successor(M,y,x)) + "natnumber_aux(M,succ(n)) = + (\x\nat. if (\y[M]. natnumber_aux(M,n)`y=1 & successor(M,y,x)) then 1 else 0)" constdefs natnumber :: "[i=>o,i,i] => o" "natnumber(M,n,x) == natnumber_aux(M,n)`x = 1" - lemma (in M_trivial) [simp]: + lemma (in M_trivial) [simp]: "natnumber(M,0,x) == x=0" *) @@ -905,114 +905,110 @@ and Diff_separation: "M(B) ==> separation(M, \x. x \ B)" and cartprod_separation: - "[| M(A); M(B) |] + "[| M(A); M(B) |] ==> separation(M, \z. \x[M]. x\A & (\y[M]. y\B & pair(M,x,y,z)))" and image_separation: - "[| M(A); M(r) |] + "[| M(A); M(r) |] ==> separation(M, \y. \p[M]. p\r & (\x[M]. x\A & pair(M,x,y,p)))" and converse_separation: - "M(r) ==> separation(M, + "M(r) ==> separation(M, \z. \p[M]. p\r & (\x[M]. \y[M]. pair(M,x,y,p) & pair(M,y,x,z)))" and restrict_separation: "M(A) ==> separation(M, \z. \x[M]. x\A & (\y[M]. pair(M,x,y,z)))" and comp_separation: "[| M(r); M(s) |] - ==> separation(M, \xz. \x[M]. \y[M]. \z[M]. \xy[M]. \yz[M]. - pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & + ==> separation(M, \xz. \x[M]. \y[M]. \z[M]. \xy[M]. \yz[M]. + pair(M,x,z,xz) & pair(M,x,y,xy) & pair(M,y,z,yz) & xy\s & yz\r)" and pred_separation: "[| M(r); M(x) |] ==> separation(M, \y. \p[M]. p\r & pair(M,y,x,p))" and Memrel_separation: "separation(M, \z. \x[M]. \y[M]. pair(M,x,y,z) & x \ y)" and funspace_succ_replacement: - "M(n) ==> - strong_replacement(M, \p z. \f[M]. \b[M]. \nb[M]. \cnbf[M]. + "M(n) ==> + strong_replacement(M, \p z. \f[M]. \b[M]. \nb[M]. \cnbf[M]. pair(M,f,b,p) & pair(M,n,b,nb) & is_cons(M,nb,f,cnbf) & upair(M,cnbf,cnbf,z))" and well_ord_iso_separation: - "[| M(A); M(f); M(r) |] - ==> separation (M, \x. x\A --> (\y[M]. (\p[M]. + "[| M(A); M(f); M(r) |] + ==> separation (M, \x. x\A --> (\y[M]. (\p[M]. fun_apply(M,f,x,y) & pair(M,y,x,p) & p \ r)))" and obase_separation: --{*part of the order type formalization*} - "[| M(A); M(r) |] - ==> separation(M, \a. \x[M]. \g[M]. \mx[M]. \par[M]. + "[| M(A); M(r) |] + ==> separation(M, \a. \x[M]. \g[M]. \mx[M]. \par[M]. ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))" and obase_equals_separation: - "[| M(A); M(r) |] - ==> separation (M, \x. x\A --> ~(\y[M]. \g[M]. - ordinal(M,y) & (\my[M]. \pxr[M]. + "[| M(A); M(r) |] + ==> separation (M, \x. x\A --> ~(\y[M]. \g[M]. + ordinal(M,y) & (\my[M]. \pxr[M]. membership(M,y,my) & pred_set(M,A,x,r,pxr) & order_isomorphism(M,pxr,r,y,my,g))))" and omap_replacement: - "[| M(A); M(r) |] + "[| M(A); M(r) |] ==> strong_replacement(M, - \a z. \x[M]. \g[M]. \mx[M]. \par[M]. - ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & + \a z. \x[M]. \g[M]. \mx[M]. \par[M]. + ordinal(M,x) & pair(M,a,x,z) & membership(M,x,mx) & pred_set(M,A,a,r,par) & order_isomorphism(M,par,r,x,mx,g))" and is_recfun_separation: --{*for well-founded recursion*} - "[| M(r); M(f); M(g); M(a); M(b) |] - ==> separation(M, - \x. \xa[M]. \xb[M]. - pair(M,x,a,xa) & xa \ r & pair(M,x,b,xb) & xb \ r & - (\fx[M]. \gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) & + "[| M(r); M(f); M(g); M(a); M(b) |] + ==> separation(M, + \x. \xa[M]. \xb[M]. + pair(M,x,a,xa) & xa \ r & pair(M,x,b,xb) & xb \ r & + (\fx[M]. \gx[M]. fun_apply(M,f,x,fx) & fun_apply(M,g,x,gx) & fx \ gx))" lemma (in M_basic) cartprod_iff_lemma: - "[| M(C); \u[M]. u \ C <-> (\x\A. \y\B. u = {{x}, {x,y}}); + "[| M(C); \u[M]. u \ C <-> (\x\A. \y\B. u = {{x}, {x,y}}); powerset(M, A \ B, p1); powerset(M, p1, p2); M(p2) |] ==> C = {u \ p2 . \x\A. \y\B. u = {{x}, {x,y}}}" -apply (simp add: powerset_def) +apply (simp add: powerset_def) apply (rule equalityI, clarify, simp) - apply (frule transM, assumption) + apply (frule transM, assumption) apply (frule transM, assumption, simp (no_asm_simp)) - apply blast + apply blast apply clarify -apply (frule transM, assumption, force) +apply (frule transM, assumption, force) done lemma (in M_basic) cartprod_iff: - "[| M(A); M(B); M(C) |] - ==> cartprod(M,A,B,C) <-> - (\p1 p2. M(p1) & M(p2) & powerset(M,A Un B,p1) & powerset(M,p1,p2) & + "[| M(A); M(B); M(C) |] + ==> cartprod(M,A,B,C) <-> + (\p1[M]. \p2[M]. powerset(M,A Un B,p1) & powerset(M,p1,p2) & C = {z \ p2. \x\A. \y\B. z = })" apply (simp add: Pair_def cartprod_def, safe) -defer 1 - apply (simp add: powerset_def) - apply blast +defer 1 + apply (simp add: powerset_def) + 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. rex(M,?Q(x))" in rspec) -apply (blast, clarify) +apply (insert power_ax, simp add: power_ax_def) +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) +apply (blast intro: cartprod_iff_lemma) done lemma (in M_basic) cartprod_closed_lemma: "[| 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. rex(M,?Q(x))" in rspec) -apply (blast, clarify) -apply (drule_tac x=z and P="\x. rex(M,?Q(x))" in rspec) +apply (insert power_ax, simp add: power_ax_def) +apply (frule_tac x="A Un B" 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) +apply (drule_tac x=z and P="\x. rex(M,?Q(x))" in rspec, auto) +apply (intro rexI conjI, simp+) +apply (insert cartprod_separation [of A B], simp) done text{*All the lemmas above are necessary because Powerset is not absolute. I should have used Replacement instead!*} -lemma (in M_basic) cartprod_closed [intro,simp]: +lemma (in M_basic) cartprod_closed [intro,simp]: "[| M(A); M(B) |] ==> M(A*B)" by (frule cartprod_closed_lemma, assumption, force) -lemma (in M_basic) sum_closed [intro,simp]: +lemma (in M_basic) sum_closed [intro,simp]: "[| M(A); M(B) |] ==> M(A+B)" by (simp add: sum_def) @@ -1022,7 +1018,7 @@ lemma (in M_trivial) Inl_in_M_iff [iff]: "M(Inl(a)) <-> M(a)" -by (simp add: Inl_def) +by (simp add: Inl_def) lemma (in M_trivial) Inl_abs [simp]: "M(Z) ==> is_Inl(M,a,Z) <-> (Z = Inl(a))" @@ -1030,7 +1026,7 @@ lemma (in M_trivial) Inr_in_M_iff [iff]: "M(Inr(a)) <-> M(a)" -by (simp add: Inr_def) +by (simp add: Inr_def) lemma (in M_trivial) Inr_abs [simp]: "M(Z) ==> is_Inr(M,a,Z) <-> (Z = Inr(a))" @@ -1040,27 +1036,27 @@ subsubsection {*converse of a relation*} lemma (in M_basic) M_converse_iff: - "M(r) ==> - converse(r) = - {z \ Union(Union(r)) * Union(Union(r)). + "M(r) ==> + converse(r) = + {z \ Union(Union(r)) * Union(Union(r)). \p\r. \x[M]. \y[M]. p = \x,y\ & z = \y,x\}" apply (rule equalityI) - prefer 2 apply (blast dest: transM, clarify, simp) -apply (simp add: Pair_def) -apply (blast dest: transM) + prefer 2 apply (blast dest: transM, clarify, simp) +apply (simp add: Pair_def) +apply (blast dest: transM) done -lemma (in M_basic) converse_closed [intro,simp]: +lemma (in M_basic) converse_closed [intro,simp]: "M(r) ==> M(converse(r))" apply (simp add: M_converse_iff) apply (insert converse_separation [of r], simp) done -lemma (in M_basic) converse_abs [simp]: +lemma (in M_basic) converse_abs [simp]: "[| M(r); M(z) |] ==> is_converse(M,r,z) <-> z = converse(r)" apply (simp add: is_converse_def) apply (rule iffI) - prefer 2 apply blast + prefer 2 apply blast apply (rule M_equalityI) apply simp apply (blast dest: transM)+ @@ -1069,98 +1065,98 @@ subsubsection {*image, preimage, domain, range*} -lemma (in M_basic) image_closed [intro,simp]: +lemma (in M_basic) image_closed [intro,simp]: "[| M(A); M(r) |] ==> M(r``A)" apply (simp add: image_iff_Collect) -apply (insert image_separation [of A r], simp) +apply (insert image_separation [of A r], simp) done -lemma (in M_basic) vimage_abs [simp]: +lemma (in M_basic) vimage_abs [simp]: "[| M(r); M(A); M(z) |] ==> pre_image(M,r,A,z) <-> z = r-``A" apply (simp add: pre_image_def) -apply (rule iffI) - apply (blast intro!: equalityI dest: transM, blast) +apply (rule iffI) + apply (blast intro!: equalityI dest: transM, blast) done -lemma (in M_basic) vimage_closed [intro,simp]: +lemma (in M_basic) vimage_closed [intro,simp]: "[| M(A); M(r) |] ==> M(r-``A)" by (simp add: vimage_def) subsubsection{*Domain, range and field*} -lemma (in M_basic) domain_abs [simp]: +lemma (in M_basic) domain_abs [simp]: "[| M(r); M(z) |] ==> is_domain(M,r,z) <-> z = domain(r)" -apply (simp add: is_domain_def) -apply (blast intro!: equalityI dest: transM) +apply (simp add: is_domain_def) +apply (blast intro!: equalityI dest: transM) done -lemma (in M_basic) domain_closed [intro,simp]: +lemma (in M_basic) domain_closed [intro,simp]: "M(r) ==> M(domain(r))" apply (simp add: domain_eq_vimage) done -lemma (in M_basic) range_abs [simp]: +lemma (in M_basic) range_abs [simp]: "[| M(r); M(z) |] ==> is_range(M,r,z) <-> z = range(r)" apply (simp add: is_range_def) apply (blast intro!: equalityI dest: transM) done -lemma (in M_basic) range_closed [intro,simp]: +lemma (in M_basic) range_closed [intro,simp]: "M(r) ==> M(range(r))" apply (simp add: range_eq_image) done -lemma (in M_basic) field_abs [simp]: +lemma (in M_basic) field_abs [simp]: "[| M(r); M(z) |] ==> is_field(M,r,z) <-> z = field(r)" by (simp add: domain_closed range_closed is_field_def field_def) -lemma (in M_basic) field_closed [intro,simp]: +lemma (in M_basic) field_closed [intro,simp]: "M(r) ==> M(field(r))" -by (simp add: domain_closed range_closed Un_closed field_def) +by (simp add: domain_closed range_closed Un_closed field_def) subsubsection{*Relations, functions and application*} -lemma (in M_basic) relation_abs [simp]: +lemma (in M_basic) relation_abs [simp]: "M(r) ==> is_relation(M,r) <-> relation(r)" -apply (simp add: is_relation_def relation_def) +apply (simp add: is_relation_def relation_def) apply (blast dest!: bspec dest: pair_components_in_M)+ done -lemma (in M_basic) function_abs [simp]: +lemma (in M_basic) function_abs [simp]: "M(r) ==> is_function(M,r) <-> function(r)" -apply (simp add: is_function_def function_def, safe) - apply (frule transM, assumption) +apply (simp add: is_function_def function_def, safe) + apply (frule transM, assumption) apply (blast dest: pair_components_in_M)+ done -lemma (in M_basic) apply_closed [intro,simp]: +lemma (in M_basic) apply_closed [intro,simp]: "[|M(f); M(a)|] ==> M(f`a)" by (simp add: apply_def) -lemma (in M_basic) apply_abs [simp]: +lemma (in M_basic) apply_abs [simp]: "[| M(f); M(x); M(y) |] ==> fun_apply(M,f,x,y) <-> f`x = y" -apply (simp add: fun_apply_def apply_def, blast) +apply (simp add: fun_apply_def apply_def, blast) done -lemma (in M_basic) typed_function_abs [simp]: +lemma (in M_basic) typed_function_abs [simp]: "[| M(A); M(f) |] ==> typed_function(M,A,B,f) <-> f \ A -> B" -apply (auto simp add: typed_function_def relation_def Pi_iff) +apply (auto simp add: typed_function_def relation_def Pi_iff) apply (blast dest: pair_components_in_M)+ done -lemma (in M_basic) injection_abs [simp]: +lemma (in M_basic) injection_abs [simp]: "[| M(A); M(f) |] ==> injection(M,A,B,f) <-> f \ inj(A,B)" apply (simp add: injection_def apply_iff inj_def apply_closed) -apply (blast dest: transM [of _ A]) +apply (blast dest: transM [of _ A]) done -lemma (in M_basic) surjection_abs [simp]: +lemma (in M_basic) surjection_abs [simp]: "[| M(A); M(B); M(f) |] ==> surjection(M,A,B,f) <-> f \ surj(A,B)" by (simp add: surjection_def surj_def) -lemma (in M_basic) bijection_abs [simp]: +lemma (in M_basic) bijection_abs [simp]: "[| M(A); M(B); M(f) |] ==> bijection(M,A,B,f) <-> f \ bij(A,B)" by (simp add: bijection_def bij_def) @@ -1168,31 +1164,31 @@ subsubsection{*Composition of relations*} lemma (in M_basic) M_comp_iff: - "[| M(r); M(s) |] - ==> r O s = - {xz \ domain(s) * range(r). + "[| M(r); M(s) |] + ==> r O s = + {xz \ domain(s) * range(r). \x[M]. \y[M]. \z[M]. xz = \x,z\ & \x,y\ \ s & \y,z\ \ r}" apply (simp add: comp_def) -apply (rule equalityI) - apply clarify - apply simp +apply (rule equalityI) + apply clarify + apply simp apply (blast dest: transM)+ done -lemma (in M_basic) comp_closed [intro,simp]: +lemma (in M_basic) comp_closed [intro,simp]: "[| M(r); M(s) |] ==> M(r O s)" apply (simp add: M_comp_iff) -apply (insert comp_separation [of r s], simp) +apply (insert comp_separation [of r s], simp) done -lemma (in M_basic) composition_abs [simp]: - "[| M(r); M(s); M(t) |] +lemma (in M_basic) composition_abs [simp]: + "[| M(r); M(s); M(t) |] ==> composition(M,r,s,t) <-> t = r O s" apply safe txt{*Proving @{term "composition(M, r, s, r O s)"}*} - prefer 2 + prefer 2 apply (simp add: composition_def comp_def) - apply (blast dest: transM) + apply (blast dest: transM) txt{*Opposite implication*} apply (rule M_equalityI) apply (simp add: composition_def comp_def) @@ -1200,18 +1196,18 @@ done text{*no longer needed*} -lemma (in M_basic) restriction_is_function: - "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] +lemma (in M_basic) restriction_is_function: + "[| restriction(M,f,A,z); function(f); M(f); M(A); M(z) |] ==> function(z)" -apply (simp add: restriction_def ball_iff_equiv) -apply (unfold function_def, blast) +apply (simp add: restriction_def ball_iff_equiv) +apply (unfold function_def, blast) done -lemma (in M_basic) restriction_abs [simp]: - "[| M(f); M(A); M(z) |] +lemma (in M_basic) restriction_abs [simp]: + "[| M(f); M(A); M(z) |] ==> restriction(M,f,A,z) <-> z = restrict(f,A)" apply (simp add: ball_iff_equiv restriction_def restrict_def) -apply (blast intro!: equalityI dest: transM) +apply (blast intro!: equalityI dest: transM) done @@ -1219,16 +1215,16 @@ "M(r) ==> restrict(r,A) = {z \ r . \x\A. \y[M]. z = \x, y\}" by (simp add: restrict_def, blast dest: transM) -lemma (in M_basic) restrict_closed [intro,simp]: +lemma (in M_basic) restrict_closed [intro,simp]: "[| M(A); M(r) |] ==> M(restrict(r,A))" apply (simp add: M_restrict_iff) -apply (insert restrict_separation [of A], simp) +apply (insert restrict_separation [of A], simp) done -lemma (in M_basic) Inter_abs [simp]: +lemma (in M_basic) Inter_abs [simp]: "[| M(A); M(z) |] ==> big_inter(M,A,z) <-> z = Inter(A)" -apply (simp add: big_inter_def Inter_def) -apply (blast intro!: equalityI dest: transM) +apply (simp add: big_inter_def Inter_def) +apply (blast intro!: equalityI dest: transM) done lemma (in M_basic) Inter_closed [intro,simp]: @@ -1238,7 +1234,7 @@ lemma (in M_basic) Int_closed [intro,simp]: "[| M(A); M(B) |] ==> M(A Int B)" apply (subgoal_tac "M({A,B})") -apply (frule Inter_closed, force+) +apply (frule Inter_closed, force+) done lemma (in M_basic) Diff_closed [intro,simp]: @@ -1250,7 +1246,7 @@ lemma (in M_basic) separation_conj: "[|separation(M,P); separation(M,Q)|] ==> separation(M, \z. P(z) & Q(z))" by (simp del: separation_closed - add: separation_iff Collect_Int_Collect_eq [symmetric]) + add: separation_iff Collect_Int_Collect_eq [symmetric]) (*???equalities*) lemma Collect_Un_Collect_eq: @@ -1262,90 +1258,74 @@ by blast lemma (in M_trivial) Collect_rall_eq: - "M(Y) ==> Collect(A, %x. \y[M]. y\Y --> P(x,y)) = + "M(Y) ==> Collect(A, %x. \y[M]. y\Y --> P(x,y)) = (if Y=0 then A else (\y \ Y. {x \ A. P(x,y)}))" -apply simp -apply (blast intro!: equalityI dest: transM) +apply simp +apply (blast intro!: equalityI dest: transM) done lemma (in M_basic) separation_disj: "[|separation(M,P); separation(M,Q)|] ==> separation(M, \z. P(z) | Q(z))" by (simp del: separation_closed - add: separation_iff Collect_Un_Collect_eq [symmetric]) + add: separation_iff Collect_Un_Collect_eq [symmetric]) lemma (in M_basic) separation_neg: "separation(M,P) ==> separation(M, \z. ~P(z))" by (simp del: separation_closed - add: separation_iff Diff_Collect_eq [symmetric]) + add: separation_iff Diff_Collect_eq [symmetric]) lemma (in M_basic) separation_imp: - "[|separation(M,P); separation(M,Q)|] + "[|separation(M,P); separation(M,Q)|] ==> separation(M, \z. P(z) --> Q(z))" -by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric]) +by (simp add: separation_neg separation_disj not_disj_iff_imp [symmetric]) -text{*This result is a hint of how little can be done without the Reflection +text{*This result is a hint of how little can be done without the Reflection Theorem. The quantifier has to be bounded by a set. We also need another instance of Separation!*} lemma (in M_basic) separation_rall: - "[|M(Y); \y[M]. separation(M, \x. P(x,y)); + "[|M(Y); \y[M]. separation(M, \x. P(x,y)); \z[M]. strong_replacement(M, \x y. y = {u \ z . P(u,x)})|] - ==> separation(M, \x. \y[M]. y\Y --> P(x,y))" + ==> separation(M, \x. \y[M]. y\Y --> P(x,y))" apply (simp del: separation_closed rall_abs - add: separation_iff Collect_rall_eq) -apply (blast intro!: Inter_closed RepFun_closed dest: transM) + add: separation_iff Collect_rall_eq) +apply (blast intro!: Inter_closed RepFun_closed dest: transM) done subsubsection{*Functions and function space*} -text{*M contains all finite functions*} -lemma (in M_basic) finite_fun_closed_lemma [rule_format]: - "[| n \ nat; M(A) |] ==> \f \ n -> A. M(f)" -apply (induct_tac n, simp) -apply (rule ballI) -apply (simp add: succ_def) -apply (frule fun_cons_restrict_eq) -apply (erule ssubst) -apply (subgoal_tac "M(f`x) & restrict(f,x) \ x -> A") - apply (simp add: cons_closed nat_into_M apply_closed) -apply (blast intro: apply_funtype transM restrict_type2) -done - -lemma (in M_basic) finite_fun_closed [rule_format]: - "[| f \ n -> A; n \ nat; M(A) |] ==> M(f)" -by (blast intro: finite_fun_closed_lemma) - -text{*The assumption @{term "M(A->B)"} is unusual, but essential: in +text{*The assumption @{term "M(A->B)"} is unusual, but essential: in all but trivial cases, A->B cannot be expected to belong to @{term M}.*} lemma (in M_basic) is_funspace_abs [simp]: "[|M(A); M(B); M(F); M(A->B)|] ==> is_funspace(M,A,B,F) <-> F = A->B"; apply (simp add: is_funspace_def) apply (rule iffI) - prefer 2 apply blast + prefer 2 apply blast apply (rule M_equalityI) apply simp_all done lemma (in M_basic) succ_fun_eq2: "[|M(B); M(n->B)|] ==> - succ(n) -> B = + succ(n) -> B = \{z. p \ (n->B)*B, \f[M]. \b[M]. p = & z = {cons(, f)}}" apply (simp add: succ_fun_eq) -apply (blast dest: transM) +apply (blast dest: transM) done lemma (in M_basic) funspace_succ: "[|M(n); M(B); M(n->B) |] ==> M(succ(n) -> B)" -apply (insert funspace_succ_replacement [of n], simp) -apply (force simp add: succ_fun_eq2 univalent_def) +apply (insert funspace_succ_replacement [of n], simp) +apply (force simp add: succ_fun_eq2 univalent_def) done text{*@{term M} contains all finite function spaces. Needed to prove the -absoluteness of transitive closure.*} +absoluteness of transitive closure. See the definition of +@{text rtrancl_alt} in in @{text WF_absolute.thy}.*} lemma (in M_basic) finite_funspace_closed [intro,simp]: "[|n\nat; M(B)|] ==> M(n->B)" apply (induct_tac n, simp) -apply (simp add: funspace_succ nat_into_M) +apply (simp add: funspace_succ nat_into_M) done @@ -1356,50 +1336,50 @@ "is_bool_of_o(M,P,z) == (P & number1(M,z)) | (~P & empty(M,z))" is_not :: "[i=>o, i, i] => o" - "is_not(M,a,z) == (number1(M,a) & empty(M,z)) | + "is_not(M,a,z) == (number1(M,a) & empty(M,z)) | (~number1(M,a) & number1(M,z))" is_and :: "[i=>o, i, i, i] => o" - "is_and(M,a,b,z) == (number1(M,a) & z=b) | + "is_and(M,a,b,z) == (number1(M,a) & z=b) | (~number1(M,a) & empty(M,z))" is_or :: "[i=>o, i, i, i] => o" - "is_or(M,a,b,z) == (number1(M,a) & number1(M,z)) | + "is_or(M,a,b,z) == (number1(M,a) & number1(M,z)) | (~number1(M,a) & z=b)" -lemma (in M_trivial) bool_of_o_abs [simp]: - "M(z) ==> is_bool_of_o(M,P,z) <-> z = bool_of_o(P)" -by (simp add: is_bool_of_o_def bool_of_o_def) +lemma (in M_trivial) bool_of_o_abs [simp]: + "M(z) ==> is_bool_of_o(M,P,z) <-> z = bool_of_o(P)" +by (simp add: is_bool_of_o_def bool_of_o_def) -lemma (in M_trivial) not_abs [simp]: +lemma (in M_trivial) not_abs [simp]: "[| M(a); M(z)|] ==> is_not(M,a,z) <-> z = not(a)" -by (simp add: Bool.not_def cond_def is_not_def) +by (simp add: Bool.not_def cond_def is_not_def) -lemma (in M_trivial) and_abs [simp]: +lemma (in M_trivial) and_abs [simp]: "[| M(a); M(b); M(z)|] ==> is_and(M,a,b,z) <-> z = a and b" -by (simp add: Bool.and_def cond_def is_and_def) +by (simp add: Bool.and_def cond_def is_and_def) -lemma (in M_trivial) or_abs [simp]: +lemma (in M_trivial) or_abs [simp]: "[| M(a); M(b); M(z)|] ==> is_or(M,a,b,z) <-> z = a or b" by (simp add: Bool.or_def cond_def is_or_def) lemma (in M_trivial) bool_of_o_closed [intro,simp]: "M(bool_of_o(P))" -by (simp add: bool_of_o_def) +by (simp add: bool_of_o_def) lemma (in M_trivial) and_closed [intro,simp]: "[| M(p); M(q) |] ==> M(p and q)" -by (simp add: and_def cond_def) +by (simp add: and_def cond_def) lemma (in M_trivial) or_closed [intro,simp]: "[| M(p); M(q) |] ==> M(p or q)" -by (simp add: or_def cond_def) +by (simp add: or_def cond_def) lemma (in M_trivial) not_closed [intro,simp]: "M(p) ==> M(not(p))" -by (simp add: Bool.not_def cond_def) +by (simp add: Bool.not_def cond_def) subsection{*Relativization and Absoluteness for List Operators*} @@ -1422,7 +1402,7 @@ by (simp add: is_Nil_def Nil_def) lemma (in M_trivial) Cons_in_M_iff [iff]: "M(Cons(a,l)) <-> M(a) & M(l)" -by (simp add: Cons_def) +by (simp add: Cons_def) lemma (in M_trivial) Cons_abs [simp]: "[|M(a); M(l); M(Z)|] ==> is_Cons(M,a,l,Z) <-> (Z = Cons(a,l))" @@ -1439,35 +1419,35 @@ list_case' :: "[i, [i,i]=>i, i] => i" --{*A version of @{term list_case} that's always defined.*} - "list_case'(a,b,xs) == - if quasilist(xs) then list_case(a,b,xs) else 0" + "list_case'(a,b,xs) == + if quasilist(xs) then list_case(a,b,xs) else 0" is_list_case :: "[i=>o, i, [i,i,i]=>o, i, i] => o" --{*Returns 0 for non-lists*} - "is_list_case(M, a, is_b, xs, z) == + "is_list_case(M, a, is_b, xs, z) == (is_Nil(M,xs) --> z=a) & (\x[M]. \l[M]. is_Cons(M,x,l,xs) --> is_b(x,l,z)) & (is_quasilist(M,xs) | empty(M,z))" hd' :: "i => i" --{*A version of @{term hd} that's always defined.*} - "hd'(xs) == if quasilist(xs) then hd(xs) else 0" + "hd'(xs) == if quasilist(xs) then hd(xs) else 0" tl' :: "i => i" --{*A version of @{term tl} that's always defined.*} - "tl'(xs) == if quasilist(xs) then tl(xs) else 0" + "tl'(xs) == if quasilist(xs) then tl(xs) else 0" is_hd :: "[i=>o,i,i] => o" --{* @{term "hd([]) = 0"} no constraints if not a list. Avoiding implication prevents the simplifier's looping.*} - "is_hd(M,xs,H) == + "is_hd(M,xs,H) == (is_Nil(M,xs) --> empty(M,H)) & (\x[M]. \l[M]. ~ is_Cons(M,x,l,xs) | H=x) & (is_quasilist(M,xs) | empty(M,H))" is_tl :: "[i=>o,i,i] => o" --{* @{term "tl([]) = []"}; see comments about @{term is_hd}*} - "is_tl(M,xs,T) == + "is_tl(M,xs,T) == (is_Nil(M,xs) --> T=xs) & (\x[M]. \l[M]. ~ is_Cons(M,x,l,xs) | T=l) & (is_quasilist(M,xs) | empty(M,T))" @@ -1491,8 +1471,8 @@ lemma list_case'_Cons [simp]: "list_case'(a,b,Cons(x,l)) = b(x,l)" by (simp add: list_case'_def quasilist_def) -lemma non_list_case: "~ quasilist(x) ==> list_case'(a,b,x) = 0" -by (simp add: quasilist_def list_case'_def) +lemma non_list_case: "~ quasilist(x) ==> list_case'(a,b,x) = 0" +by (simp add: quasilist_def list_case'_def) lemma list_case'_eq_list_case [simp]: "xs \ list(A) ==>list_case'(a,b,xs) = list_case(a,b,xs)" @@ -1500,25 +1480,25 @@ lemma (in M_basic) list_case'_closed [intro,simp]: "[|M(k); M(a); \x[M]. \y[M]. M(b(x,y))|] ==> M(list_case'(a,b,k))" -apply (case_tac "quasilist(k)") - apply (simp add: quasilist_def, force) -apply (simp add: non_list_case) +apply (case_tac "quasilist(k)") + apply (simp add: quasilist_def, force) +apply (simp add: non_list_case) done -lemma (in M_trivial) quasilist_abs [simp]: +lemma (in M_trivial) quasilist_abs [simp]: "M(z) ==> is_quasilist(M,z) <-> quasilist(z)" by (auto simp add: is_quasilist_def quasilist_def) -lemma (in M_trivial) list_case_abs [simp]: - "[| relativize2(M,is_b,b); M(k); M(z) |] +lemma (in M_trivial) list_case_abs [simp]: + "[| relativize2(M,is_b,b); M(k); M(z) |] ==> is_list_case(M,a,is_b,k,z) <-> z = list_case'(a,b,k)" -apply (case_tac "quasilist(k)") - prefer 2 - apply (simp add: is_list_case_def non_list_case) - apply (force simp add: quasilist_def) +apply (case_tac "quasilist(k)") + prefer 2 + apply (simp add: is_list_case_def non_list_case) + apply (force simp add: quasilist_def) apply (simp add: quasilist_def is_list_case_def) -apply (elim disjE exE) - apply (simp_all add: relativize2_def) +apply (elim disjE exE) + apply (simp_all add: relativize2_def) done @@ -1529,34 +1509,34 @@ lemma (in M_trivial) is_hd_Cons: "[|M(a); M(l)|] ==> is_hd(M,Cons(a,l),Z) <-> Z = a" -by (force simp add: is_hd_def) +by (force simp add: is_hd_def) lemma (in M_trivial) hd_abs [simp]: "[|M(x); M(y)|] ==> is_hd(M,x,y) <-> y = hd'(x)" apply (simp add: hd'_def) apply (intro impI conjI) - prefer 2 apply (force simp add: is_hd_def) + prefer 2 apply (force simp add: is_hd_def) apply (simp add: quasilist_def is_hd_def) apply (elim disjE exE, auto) -done +done lemma (in M_trivial) is_tl_Nil: "is_tl(M,[],Z) <-> Z = []" by (simp add: is_tl_def) lemma (in M_trivial) is_tl_Cons: "[|M(a); M(l)|] ==> is_tl(M,Cons(a,l),Z) <-> Z = l" -by (force simp add: is_tl_def) +by (force simp add: is_tl_def) lemma (in M_trivial) tl_abs [simp]: "[|M(x); M(y)|] ==> is_tl(M,x,y) <-> y = tl'(x)" apply (simp add: tl'_def) apply (intro impI conjI) - prefer 2 apply (force simp add: is_tl_def) + prefer 2 apply (force simp add: is_tl_def) apply (simp add: quasilist_def is_tl_def) apply (elim disjE exE, auto) -done +done -lemma (in M_trivial) relativize1_tl: "relativize1(M, is_tl(M), tl')" +lemma (in M_trivial) relativize1_tl: "relativize1(M, is_tl(M), tl')" by (simp add: relativize1_def) lemma hd'_Nil: "hd'([]) = 0" @@ -1572,8 +1552,8 @@ by (simp add: tl'_def) lemma iterates_tl_Nil: "n \ nat ==> tl'^n ([]) = []" -apply (induct_tac n) -apply (simp_all add: tl'_Nil) +apply (induct_tac n) +apply (simp_all add: tl'_Nil) done lemma (in M_basic) tl'_closed: "M(x) ==> M(tl'(x))" diff -r 67b0b7500a9d -r 87482b5e3f2e src/ZF/Constructible/Separation.thy --- a/src/ZF/Constructible/Separation.thy Fri Oct 04 15:23:58 2002 +0200 +++ b/src/ZF/Constructible/Separation.thy Fri Oct 04 15:57:32 2002 +0200 @@ -458,7 +458,6 @@ and Inter_abs = M_basic.Inter_abs [OF M_basic_L] and Inter_closed = M_basic.Inter_closed [OF M_basic_L] and Int_closed = M_basic.Int_closed [OF M_basic_L] - and finite_fun_closed = M_basic.finite_fun_closed [OF M_basic_L] and is_funspace_abs = M_basic.is_funspace_abs [OF M_basic_L] and succ_fun_eq2 = M_basic.succ_fun_eq2 [OF M_basic_L] and funspace_succ = M_basic.funspace_succ [OF M_basic_L] @@ -488,7 +487,6 @@ and wellfounded_iff_wellfounded_on_field = M_basic.wellfounded_iff_wellfounded_on_field [OF M_basic_L] and wellfounded_induct = M_basic.wellfounded_induct [OF M_basic_L] and wellfounded_on_induct = M_basic.wellfounded_on_induct [OF M_basic_L] - and wellfounded_on_induct2 = M_basic.wellfounded_on_induct2 [OF M_basic_L] and linear_imp_relativized = M_basic.linear_imp_relativized [OF M_basic_L] and trans_on_imp_relativized = M_basic.trans_on_imp_relativized [OF M_basic_L] and wf_on_imp_relativized = M_basic.wf_on_imp_relativized [OF M_basic_L] diff -r 67b0b7500a9d -r 87482b5e3f2e src/ZF/Constructible/Wellorderings.thy --- a/src/ZF/Constructible/Wellorderings.thy Fri Oct 04 15:23:58 2002 +0200 +++ b/src/ZF/Constructible/Wellorderings.thy Fri Oct 04 15:57:32 2002 +0200 @@ -33,13 +33,11 @@ wellfounded :: "[i=>o,i]=>o" --{*EVERY non-empty set has an @{text r}-minimal element*} "wellfounded(M,r) == - \x[M]. ~ empty(M,x) - --> (\y[M]. y\x & ~(\z[M]. z\x & \ r))" + \x[M]. x\0 --> (\y[M]. y\x & ~(\z[M]. z\x & \ r))" wellfounded_on :: "[i=>o,i,i]=>o" --{*every non-empty SUBSET OF @{text A} has an @{text r}-minimal element*} "wellfounded_on(M,A,r) == - \x[M]. ~ empty(M,x) --> subset(M,x,A) - --> (\y[M]. y\x & ~(\z[M]. z\x & \ r))" + \x[M]. x\0 --> x\A --> (\y[M]. y\x & ~(\z[M]. z\x & \ r))" wellordered :: "[i=>o,i,i]=>o" --{*linear and wellfounded on @{text A}*} @@ -124,15 +122,6 @@ apply (blast intro: transM)+ done -text{*The assumption @{term "r \ A*A"} justifies strengthening the induction - hypothesis by removing the restriction to @{term A}.*} -lemma (in M_basic) wellfounded_on_induct2: - "[| a\A; wellfounded_on(M,A,r); M(A); r \ A*A; - separation(M, \x. x\A --> ~P(x)); - \x\A. M(x) & (\y. \ r --> P(y)) --> P(x) |] - ==> P(a)"; -by (rule wellfounded_on_induct, assumption+, blast) - subsubsection {*Kunen's lemma IV 3.14, page 123*} @@ -297,13 +286,13 @@ by (simp add: wellordered_def, blast dest: wellfounded_on_asym) -text{*Surely a shorter proof using lemmas in @{text Order}? - Like @{text well_ord_iso_preserving}?*} +text{*Can't use @{text well_ord_iso_preserving} because it needs the +strong premise @{term "well_ord(A,r)"}*} lemma (in M_basic) ord_iso_pred_imp_lt: "[| f \ ord_iso(Order.pred(A,x,r), r, i, Memrel(i)); - g \ ord_iso(Order.pred(A,y,r), r, j, Memrel(j)); - wellordered(M,A,r); x \ A; y \ A; M(A); M(r); M(f); M(g); M(j); - Ord(i); Ord(j); \x,y\ \ r |] + g \ ord_iso(Order.pred(A,y,r), r, j, Memrel(j)); + wellordered(M,A,r); x \ A; y \ A; M(A); M(r); M(f); M(g); M(j); + Ord(i); Ord(j); \x,y\ \ r |] ==> i < j" apply (frule wellordered_is_trans_on, assumption) apply (frule_tac y=y in transM, assumption) @@ -351,9 +340,8 @@ "obase(M,A,r,z) == \a[M]. a \ z <-> - (a\A & (\x[M]. \g[M]. \mx[M]. \par[M]. - ordinal(M,x) & membership(M,x,mx) & pred_set(M,A,a,r,par) & - order_isomorphism(M,par,r,x,mx,g)))" + (a\A & (\x[M]. \g[M]. Ord(x) & + order_isomorphism(M,Order.pred(A,a,r),r,x,Memrel(x),g)))" omap :: "[i=>o,i,i,i] => o" diff -r 67b0b7500a9d -r 87482b5e3f2e src/ZF/Nat.thy --- a/src/ZF/Nat.thy Fri Oct 04 15:23:58 2002 +0200 +++ b/src/ZF/Nat.thy Fri Oct 04 15:57:32 2002 +0200 @@ -110,6 +110,9 @@ apply (erule ltD) done +lemma naturals_not_limit: "a \ nat ==> ~ Limit(a)" +by (induct a rule: nat_induct, auto) + lemma succ_natD [dest!]: "succ(i): nat ==> i: nat" by (rule Ord_trans [OF succI1], auto)