# HG changeset patch # User lcp # Date 775221680 -7200 # Node ID 70b789956bd3cedc1a331d2b8ae8e2ad3c3210d3 # Parent 4d1614d8f119371e25059fdcb2d2bca5176f74aa Axiom of choice, cardinality results, etc. diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/AC.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC.ML Tue Jul 26 13:21:20 1994 +0200 @@ -0,0 +1,61 @@ +(* Title: ZF/AC.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +For AC.thy. The Axiom of Choice +*) + +open AC; + +(*The same as AC, but no premise a:A*) +val [nonempty] = goal AC.thy + "[| !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)"; +by (excluded_middle_tac "A=0" 1); +by (asm_simp_tac (ZF_ss addsimps [Pi_empty1]) 2 THEN fast_tac ZF_cs 2); +(*The non-trivial case*) +by (safe_tac eq_cs); +by (fast_tac (ZF_cs addSIs [AC, nonempty]) 1); +val AC_Pi = result(); + +(*Using dtac, this has the advantage of DELETING the universal quantifier*) +goal AC.thy "!!A B. ALL x:A. EX y. y:B(x) ==> EX y. y : Pi(A,B)"; +by (resolve_tac [AC_Pi] 1); +by (eresolve_tac [bspec] 1); +by (assume_tac 1); +val AC_ball_Pi = result(); + +goal AC.thy "EX f. f: (PROD X: Pow(C)-{0}. X)"; +by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1); +by (etac exI 2); +by (fast_tac eq_cs 1); +val AC_Pi_Pow = result(); + +val [nonempty] = goal AC.thy + "[| !!x. x:A ==> (EX y. y:x) \ +\ |] ==> EX f: A->Union(A). ALL x:A. f`x : x"; +by (res_inst_tac [("B1", "%x.x")] (AC_Pi RS exE) 1); +by (etac nonempty 1); +by (fast_tac (ZF_cs addDs [apply_type] addIs [Pi_type]) 1); +val AC_func = result(); + +goal AC.thy "!!x A. [| 0 ~: A; x: A |] ==> EX y. y:x"; +by (resolve_tac [exCI] 1); +by (eresolve_tac [notE] 1); +by (resolve_tac [equals0I RS subst] 1); +by (eresolve_tac [spec RS notE] 1 THEN REPEAT (assume_tac 1)); +val non_empty_family = result(); + +goal AC.thy "!!A. 0 ~: A ==> EX f: A->Union(A). ALL x:A. f`x : x"; +by (rtac AC_func 1); +by (REPEAT (ares_tac [non_empty_family] 1)); +val AC_func0 = result(); + +goal AC.thy "EX f: (Pow(C)-{0}) -> C. ALL x:(Pow(C)-{0}). f`x : x"; +by (resolve_tac [AC_func0 RS bexE] 1); +by (rtac bexI 2); +by (assume_tac 2); +by (eresolve_tac [fun_weaken_type] 2); +by (ALLGOALS (fast_tac ZF_cs)); +val AC_func_Pow = result(); + diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/AC.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/AC.thy Tue Jul 26 13:21:20 1994 +0200 @@ -0,0 +1,14 @@ +(* Title: ZF/AC.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +The Axiom of Choice + +This definition comes from Halmos (1960), page 59. +*) + +AC = ZF + "func" + +rules + AC "[| a: A; !!x. x:A ==> (EX y. y:B(x)) |] ==> EX z. z : Pi(A,B)" +end diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/Cardinal.ML --- a/src/ZF/Cardinal.ML Thu Jul 21 16:51:26 1994 +0200 +++ b/src/ZF/Cardinal.ML Tue Jul 26 13:21:20 1994 +0200 @@ -201,7 +201,7 @@ by (etac (eqpoll_refl RS Least_le) 1); val Ord_cardinal_le = result(); -goalw Cardinal.thy [Card_def] "!!i. Card(i) ==> |i| = i"; +goalw Cardinal.thy [Card_def] "!!K. Card(K) ==> |K| = K"; by (etac sym 1); val Card_cardinal_eq = result(); @@ -216,7 +216,7 @@ by (rtac Ord_Least 1); val Card_is_Ord = result(); -goalw Cardinal.thy [cardinal_def] "Ord( |A| )"; +goalw Cardinal.thy [cardinal_def] "Ord(|A|)"; by (rtac Ord_Least 1); val Ord_cardinal = result(); @@ -225,7 +225,7 @@ by (fast_tac (ZF_cs addSEs [ltE]) 1); val Card_0 = result(); -goalw Cardinal.thy [cardinal_def] "Card( |A| )"; +goalw Cardinal.thy [cardinal_def] "Card(|A|)"; by (excluded_middle_tac "EX i. Ord(i) & i eqpoll A" 1); by (etac (Least_0 RS ssubst) 1 THEN rtac Card_0 1); by (rtac (Ord_Least RS CardI) 1); @@ -265,11 +265,21 @@ by (etac cardinal_mono 1); val cardinal_lt_imp_lt = result(); -goal Cardinal.thy "!!i j. [| |i| < k; Ord(i); Card(k) |] ==> i < k"; +goal Cardinal.thy "!!i j. [| |i| < K; Ord(i); Card(K) |] ==> i < K"; by (asm_simp_tac (ZF_ss addsimps [cardinal_lt_imp_lt, Card_is_Ord, Card_cardinal_eq]) 1); val Card_lt_imp_lt = result(); +goal Cardinal.thy "!!i j. [| Ord(i); Card(K) |] ==> (|i| < K) <-> (i < K)"; +by (fast_tac (ZF_cs addEs [Card_lt_imp_lt, Ord_cardinal_le RS lt_trans1]) 1); +val Card_lt_iff = result(); + +goal Cardinal.thy "!!i j. [| Ord(i); Card(K) |] ==> (K le |i|) <-> (K le i)"; +by (asm_simp_tac (ZF_ss addsimps + [Card_lt_iff, Card_is_Ord, Ord_cardinal, + not_lt_iff_le RS iff_sym]) 1); +val Card_le_iff = result(); + (** The swap operator [NOT USED] **) diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/CardinalArith.ML --- a/src/ZF/CardinalArith.ML Thu Jul 21 16:51:26 1994 +0200 +++ b/src/ZF/CardinalArith.ML Tue Jul 26 13:21:20 1994 +0200 @@ -8,26 +8,7 @@ open CardinalArith; -goalw CardinalArith.thy [jump_cardinal_def] - "Ord(jump_cardinal(K))"; -by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); -by (safe_tac (ZF_cs addSIs [Ord_ordertype])); - -bw Transset_def; -by (safe_tac (ZF_cs addSIs [Ord_ordertype])); -br (ordertype_subset RS exE) 1; -ba 1; -ba 1; -by (safe_tac (ZF_cs addSIs [Ord_ordertype])); -fr UN_I; -br ReplaceI 2; -by (fast_tac ZF_cs 4); -by (fast_tac ZF_cs 1); - -(****************************************************************) - - - +(*** Elementary properties ***) (*Use AC to discharge first premise*) goal CardinalArith.thy @@ -59,18 +40,37 @@ left_inverse_bij, right_inverse_bij]; -(*Congruence law for succ under equipollence*) +(*Congruence law for cons under equipollence*) goalw CardinalArith.thy [eqpoll_def] - "!!A B. A eqpoll B ==> succ(A) eqpoll succ(B)"; + "!!A B. [| A eqpoll B; a ~: A; b ~: B |] ==> cons(a,A) eqpoll cons(b,B)"; by (safe_tac ZF_cs); by (rtac exI 1); -by (res_inst_tac [("c", "%z.if(z=A,B,f`z)"), - ("d", "%z.if(z=B,A,converse(f)`z)")] lam_bijective 1); +by (res_inst_tac [("c", "%z.if(z=a,b,f`z)"), + ("d", "%z.if(z=b,a,converse(f)`z)")] lam_bijective 1); by (ALLGOALS - (asm_simp_tac (bij_inverse_ss addsimps [succI2, mem_imp_not_eq] - setloop etac succE ))); + (asm_simp_tac (bij_inverse_ss addsimps [consI2] + setloop (etac consE ORELSE' + split_tac [expand_if])))); +by (fast_tac (ZF_cs addIs [bij_is_fun RS apply_type]) 1); +by (fast_tac (ZF_cs addIs [bij_converse_bij RS bij_is_fun RS apply_type]) 1); +val cons_eqpoll_cong = result(); + +(*Congruence law for succ under equipollence*) +goalw CardinalArith.thy [succ_def] + "!!A B. A eqpoll B ==> succ(A) eqpoll succ(B)"; +by (REPEAT (ares_tac [cons_eqpoll_cong, mem_not_refl] 1)); val succ_eqpoll_cong = result(); +(*Each element of Fin(A) is equivalent to a natural number*) +goal CardinalArith.thy + "!!X A. X: Fin(A) ==> EX n:nat. X eqpoll n"; +by (eresolve_tac [Fin_induct] 1); +by (fast_tac (ZF_cs addIs [eqpoll_refl, nat_0I]) 1); +by (fast_tac (ZF_cs addSIs [cons_eqpoll_cong, + rewrite_rule [succ_def] nat_succI] + addSEs [mem_irrefl]) 1); +val Fin_eqpoll = result(); + (*Congruence law for + under equipollence*) goalw CardinalArith.thy [eqpoll_def] "!!A B C D. [| A eqpoll C; B eqpoll D |] ==> A+B eqpoll C+D"; @@ -125,7 +125,7 @@ (*Unconditional version requires AC*) goalw CardinalArith.thy [cadd_def] - "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> \ + "!!i j k. [| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==> \ \ (i |+| j) |+| k = i |+| (j |+| k)"; by (rtac cardinal_cong 1); br ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS sum_eqpoll_cong RS @@ -133,8 +133,8 @@ by (rtac (sum_assoc_eqpoll RS eqpoll_trans) 2); br ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS sum_eqpoll_cong RS eqpoll_sym) 2; -by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel] 1)); -val Ord_cadd_assoc = result(); +by (REPEAT (ares_tac [well_ord_radd] 1)); +val well_ord_cadd_assoc = result(); (** 0 is the identity for addition **) @@ -145,7 +145,7 @@ by (ALLGOALS (asm_simp_tac (case_ss setloop eresolve_tac [sumE,emptyE]))); val sum_0_eqpoll = result(); -goalw CardinalArith.thy [cadd_def] "!!i. Card(i) ==> 0 |+| i = i"; +goalw CardinalArith.thy [cadd_def] "!!K. Card(K) ==> 0 |+| K = K"; by (asm_simp_tac (ZF_ss addsimps [sum_0_eqpoll RS cardinal_cong, Card_cardinal_eq]) 1); val cadd_0 = result(); @@ -212,7 +212,7 @@ (*Unconditional version requires AC*) goalw CardinalArith.thy [cmult_def] - "!!i j k. [| Ord(i); Ord(j); Ord(k) |] ==> \ + "!!i j k. [| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |] ==> \ \ (i |*| j) |*| k = i |*| (j |*| k)"; by (rtac cardinal_cong 1); br ([well_ord_cardinal_eqpoll, eqpoll_refl] MRS prod_eqpoll_cong RS @@ -220,8 +220,8 @@ by (rtac (prod_assoc_eqpoll RS eqpoll_trans) 2); br ([eqpoll_refl, well_ord_cardinal_eqpoll] MRS prod_eqpoll_cong RS eqpoll_sym) 2; -by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1)); -val Ord_cmult_assoc = result(); +by (REPEAT (ares_tac [well_ord_rmult] 1)); +val well_ord_cmult_assoc = result(); (** Cardinal multiplication distributes over addition **) @@ -240,7 +240,7 @@ by (simp_tac (ZF_ss addsimps [lam_type]) 1); val prod_square_lepoll = result(); -goalw CardinalArith.thy [cmult_def] "!!k. Card(k) ==> k le k |*| k"; +goalw CardinalArith.thy [cmult_def] "!!K. Card(K) ==> K le K |*| K"; by (rtac le_trans 1); by (rtac well_ord_lepoll_imp_le 2); by (rtac prod_square_lepoll 3); @@ -270,7 +270,7 @@ by (ALLGOALS (asm_simp_tac ZF_ss)); val prod_singleton_eqpoll = result(); -goalw CardinalArith.thy [cmult_def, succ_def] "!!i. Card(i) ==> 1 |*| i = i"; +goalw CardinalArith.thy [cmult_def, succ_def] "!!K. Card(K) ==> 1 |*| K = K"; by (asm_simp_tac (ZF_ss addsimps [prod_singleton_eqpoll RS cardinal_cong, Card_cardinal_eq]) 1); val cmult_1 = result(); @@ -309,6 +309,7 @@ (*** Infinite Cardinals are Limit Ordinals ***) +(*Using lam_injective might simplify this proof!*) goalw CardinalArith.thy [lepoll_def, inj_def] "!!i. nat <= A ==> succ(A) lepoll A"; by (res_inst_tac [("x", @@ -333,12 +334,12 @@ by (rtac (subset_succI RS subset_imp_lepoll) 1); val nat_succ_eqpoll = result(); -goalw CardinalArith.thy [InfCard_def] "!!i. InfCard(i) ==> Card(i)"; +goalw CardinalArith.thy [InfCard_def] "!!K. InfCard(K) ==> Card(K)"; by (etac conjunct1 1); val InfCard_is_Card = result(); (*Kunen's Lemma 10.11*) -goalw CardinalArith.thy [InfCard_def] "!!i. InfCard(i) ==> Limit(i)"; +goalw CardinalArith.thy [InfCard_def] "!!K. InfCard(K) ==> Limit(K)"; by (etac conjE 1); by (rtac (ltI RS non_succ_LimitI) 1); by (etac ([asm_rl, nat_0I] MRS (le_imp_subset RS subsetD)) 1); @@ -369,8 +370,8 @@ (** Establishing the well-ordering **) goalw CardinalArith.thy [inj_def] - "!!k. Ord(k) ==> \ -\ (lam z:k*k. split(%x y. >, z)) : inj(k*k, k*k*k)"; + "!!K. Ord(K) ==> \ +\ (lam z:K*K. split(%x y. >, z)) : inj(K*K, K*K*K)"; by (safe_tac ZF_cs); by (fast_tac (ZF_cs addIs [lam_type, Un_least_lt RS ltD, ltI] addSEs [split_type]) 1); @@ -378,7 +379,7 @@ val csquare_lam_inj = result(); goalw CardinalArith.thy [csquare_rel_def] - "!!k. Ord(k) ==> well_ord(k*k, csquare_rel(k))"; + "!!K. Ord(K) ==> well_ord(K*K, csquare_rel(K))"; by (rtac (csquare_lam_inj RS well_ord_rvimage) 1); by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1)); val well_ord_csquare = result(); @@ -386,8 +387,8 @@ (** Characterising initial segments of the well-ordering **) goalw CardinalArith.thy [csquare_rel_def] - "!!k. [| x \ -\ <, > : csquare_rel(k) --> x le z & y le z"; + "!!K. [| x \ +\ <, > : csquare_rel(K) --> x le z & y le z"; by (REPEAT (etac ltE 1)); by (asm_simp_tac (ZF_ss addsimps [rvimage_iff, rmult_iff, Memrel_iff, Un_absorb, Un_least_mem_iff, ltD]) 1); @@ -398,7 +399,7 @@ val csquareD = csquareD_lemma RS mp |> standard; goalw CardinalArith.thy [pred_def] - "!!k. z pred(k*k, , csquare_rel(k)) <= succ(z)*succ(z)"; + "!!K. z pred(K*K, , csquare_rel(K)) <= succ(z)*succ(z)"; by (safe_tac (lemmas_cs addSEs [SigmaE])); (*avoids using succCI*) by (rtac (csquareD RS conjE) 1); by (rewtac lt_def); @@ -407,9 +408,9 @@ val pred_csquare_subset = result(); goalw CardinalArith.thy [csquare_rel_def] - "!!k. [| x \ -\ <, > : csquare_rel(k)"; -by (subgoals_tac ["x \ +\ <, > : csquare_rel(K)"; +by (subgoals_tac ["x \ -\ <, > : csquare_rel(k) | x=z & y=z"; -by (subgoals_tac ["x \ +\ <, > : csquare_rel(K) | x=z & y=z"; +by (subgoals_tac ["x \ -\ ordermap(k*k, csquare_rel(k)) ` lepoll \ -\ ordermap(k*k, csquare_rel(k)) ` "; -by (subgoals_tac ["z \ +\ ordermap(K*K, csquare_rel(K)) ` lepoll \ +\ ordermap(K*K, csquare_rel(K)) ` "; +by (subgoals_tac ["z: k*k has no more than z*z predecessors..." (page 29) *) +(*Kunen: "each : K*K has no more than z*z predecessors..." (page 29) *) goalw CardinalArith.thy [cmult_def] - "!!k. [| InfCard(k); x \ -\ | ordermap(k*k, csquare_rel(k)) ` | le |succ(z)| |*| |succ(z)|"; + "!!K. [| InfCard(K); x \ +\ | ordermap(K*K, csquare_rel(K)) ` | le |succ(z)| |*| |succ(z)|"; by (rtac (well_ord_rmult RS well_ord_lepoll_imp_le) 1); by (REPEAT (ares_tac [Ord_cardinal, well_ord_Memrel] 1)); -by (subgoals_tac ["z y |*| y = y |] ==> \ -\ ordertype(k*k, csquare_rel(k)) le k"; + "!!K. [| InfCard(K); ALL y:K. InfCard(y) --> y |*| y = y |] ==> \ +\ ordertype(K*K, csquare_rel(K)) le K"; by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1); by (rtac all_lt_imp_le 1); by (assume_tac 1); @@ -504,7 +505,7 @@ (*This lemma can easily be generalized to premise well_ord(A*A,r) *) goalw CardinalArith.thy [cmult_def] - "!!k. Ord(k) ==> k |*| k = |ordertype(k*k, csquare_rel(k))|"; + "!!K. Ord(K) ==> K |*| K = |ordertype(K*K, csquare_rel(K))|"; by (rtac cardinal_cong 1); by (rewtac eqpoll_def); by (rtac exI 1); @@ -512,11 +513,10 @@ val csquare_eq_ordertype = result(); (*Main result: Kunen's Theorem 10.12*) -goal CardinalArith.thy - "!!k. InfCard(k) ==> k |*| k = k"; +goal CardinalArith.thy "!!K. InfCard(K) ==> K |*| K = K"; by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1); by (etac rev_mp 1); -by (trans_ind_tac "k" [] 1); +by (trans_ind_tac "K" [] 1); by (rtac impI 1); by (rtac le_anti_sym 1); by (etac (InfCard_is_Card RS cmult_square_le) 2); @@ -527,3 +527,111 @@ (ZF_ss addsimps [csquare_eq_ordertype, Ord_cardinal_le, well_ord_csquare RS Ord_ordertype]) 1); val InfCard_csquare_eq = result(); + + +goal CardinalArith.thy + "!!A. [| well_ord(A,r); InfCard(|A|) |] ==> A*A eqpoll A"; +by (resolve_tac [prod_eqpoll_cong RS eqpoll_trans] 1); +by (REPEAT (etac (well_ord_cardinal_eqpoll RS eqpoll_sym) 1)); +by (resolve_tac [well_ord_cardinal_eqE] 1); +by (REPEAT (ares_tac [Ord_cardinal, well_ord_rmult, well_ord_Memrel] 1)); +by (asm_simp_tac (ZF_ss addsimps [symmetric cmult_def, InfCard_csquare_eq]) 1); +val well_ord_InfCard_square_eq = result(); + + +(*** For every cardinal number there exists a greater one + [Kunen's Theorem 10.16, which would be trivial using AC] ***) + +goalw CardinalArith.thy [jump_cardinal_def] "Ord(jump_cardinal(K))"; +by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); +by (safe_tac (ZF_cs addSIs [Ord_ordertype])); +bw Transset_def; +by (safe_tac ZF_cs); +by (rtac (ordertype_subset RS exE) 1 THEN REPEAT (assume_tac 1)); +by (resolve_tac [UN_I] 1); +by (resolve_tac [ReplaceI] 2); +by (ALLGOALS (fast_tac (ZF_cs addSEs [well_ord_subset]))); +val Ord_jump_cardinal = result(); + +(*Allows selective unfolding. Less work than deriving intro/elim rules*) +goalw CardinalArith.thy [jump_cardinal_def] + "i : jump_cardinal(K) <-> \ +\ (EX r X. r <= K*K & X <= K & well_ord(X,r) & i = ordertype(X,r))"; +by (fast_tac subset_cs 1); (*It's vital to avoid reasoning about <=*) +val jump_cardinal_iff = result(); + +(*The easy part of Theorem 10.16: jump_cardinal(K) exceeds K*) +goal CardinalArith.thy "!!K. Ord(K) ==> K < jump_cardinal(K)"; +by (resolve_tac [Ord_jump_cardinal RSN (2,ltI)] 1); +by (resolve_tac [jump_cardinal_iff RS iffD2] 1); +by (REPEAT_FIRST (ares_tac [exI, conjI, well_ord_Memrel])); +by (resolve_tac [subset_refl] 2); +by (asm_simp_tac (ZF_ss addsimps [Memrel_def, subset_iff]) 1); +by (asm_simp_tac (ZF_ss addsimps [ordertype_Memrel]) 1); +val K_lt_jump_cardinal = result(); + +(*The proof by contradiction: the bijection f yields a wellordering of X + whose ordertype is jump_cardinal(K). *) +goal CardinalArith.thy + "!!K. [| well_ord(X,r); r <= K * K; X <= K; \ +\ f : bij(ordertype(X,r), jump_cardinal(K)) \ +\ |] ==> jump_cardinal(K) : jump_cardinal(K)"; +by (subgoal_tac "f O ordermap(X,r): bij(X, jump_cardinal(K))" 1); +by (REPEAT (ares_tac [comp_bij, ordermap_bij] 2)); +by (resolve_tac [jump_cardinal_iff RS iffD2] 1); +by (REPEAT_FIRST (resolve_tac [exI, conjI])); +by (rtac ([rvimage_type, Sigma_mono] MRS subset_trans) 1); +by (REPEAT (assume_tac 1)); +by (etac (bij_is_inj RS well_ord_rvimage) 1); +by (rtac (Ord_jump_cardinal RS well_ord_Memrel) 1); +by (asm_simp_tac + (ZF_ss addsimps [well_ord_Memrel RSN (2, bij_ordertype_vimage), + ordertype_Memrel, Ord_jump_cardinal]) 1); +val Card_jump_cardinal_lemma = result(); + +(*The hard part of Theorem 10.16: jump_cardinal(K) is itself a cardinal*) +goal CardinalArith.thy "Card(jump_cardinal(K))"; +by (rtac (Ord_jump_cardinal RS CardI) 1); +by (rewrite_goals_tac [eqpoll_def]); +by (safe_tac (ZF_cs addSDs [ltD, jump_cardinal_iff RS iffD1])); +by (REPEAT (ares_tac [Card_jump_cardinal_lemma RS mem_irrefl] 1)); +val Card_jump_cardinal = result(); + +(*** Basic properties of successor cardinals ***) + +goalw CardinalArith.thy [csucc_def] + "!!K. Ord(K) ==> Card(csucc(K)) & K < csucc(K)"; +by (rtac LeastI 1); +by (REPEAT (ares_tac [conjI, Card_jump_cardinal, K_lt_jump_cardinal, + Ord_jump_cardinal] 1)); +val csucc_basic = result(); + +val Card_csucc = csucc_basic RS conjunct1 |> standard; + +val lt_csucc = csucc_basic RS conjunct2 |> standard; + +goalw CardinalArith.thy [csucc_def] + "!!K L. [| Card(L); K csucc(K) le L"; +by (rtac Least_le 1); +by (REPEAT (ares_tac [conjI, Card_is_Ord] 1)); +val csucc_le = result(); + +goal CardinalArith.thy + "!!K. [| Ord(i); Card(K) |] ==> i < csucc(K) <-> |i| le K"; +by (resolve_tac [iffI] 1); +by (resolve_tac [Card_lt_imp_lt] 2); +by (eresolve_tac [lt_trans1] 2); +by (REPEAT (ares_tac [lt_csucc, Card_csucc, Card_is_Ord] 2)); +by (resolve_tac [notI RS not_lt_imp_le] 1); +by (resolve_tac [Card_cardinal RS csucc_le RS lt_trans1 RS lt_irrefl] 1); +by (assume_tac 1); +by (resolve_tac [Ord_cardinal_le RS lt_trans1] 1); +by (REPEAT (ares_tac [Ord_cardinal] 1 + ORELSE eresolve_tac [ltE, Card_is_Ord] 1)); +val lt_csucc_iff = result(); + +goal CardinalArith.thy + "!!K' K. [| Card(K'); Card(K) |] ==> K' < csucc(K) <-> K' le K"; +by (asm_simp_tac + (ZF_ss addsimps [lt_csucc_iff, Card_cardinal_eq, Card_is_Ord]) 1); +val Card_lt_csucc_iff = result(); diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/CardinalArith.thy --- a/src/ZF/CardinalArith.thy Thu Jul 21 16:51:26 1994 +0200 +++ b/src/ZF/CardinalArith.thy Tue Jul 26 13:21:20 1994 +0200 @@ -6,22 +6,18 @@ Cardinal Arithmetic *) -CardinalArith = Cardinal + OrderArith + Arith + +CardinalArith = Cardinal + OrderArith + Arith + Fin + consts - jump_cardinal :: "i=>i" InfCard :: "i=>o" "|*|" :: "[i,i]=>i" (infixl 70) "|+|" :: "[i,i]=>i" (infixl 65) csquare_rel :: "i=>i" + jump_cardinal :: "i=>i" + csucc :: "i=>i" rules - jump_cardinal_def - "jump_cardinal(K) == \ -\ UN X:Pow(K). {z. r: Pow(X*X), well_ord(X,r) & z = ordertype(X,r)}" - - InfCard_def "InfCard(i) == Card(i) & nat le i" cadd_def "i |+| j == | i+j |" @@ -33,4 +29,13 @@ \ rmult(k,Memrel(k), k*k, \ \ rmult(k,Memrel(k), k,Memrel(k))))" + (*This def is more complex than Kunen's but it more easily proved to + be a cardinal*) + jump_cardinal_def + "jump_cardinal(K) == \ +\ UN X:Pow(K). {z. r: Pow(K*K), well_ord(X,r) & z = ordertype(X,r)}" + + (*needed because jump_cardinal(K) might not be the successor of K*) + csucc_def "csucc(K) == LEAST L. Card(L) & K X eqpoll Y"; +by (resolve_tac [AC_well_ord RS exE] 1); +by (resolve_tac [AC_well_ord RS exE] 1); +by (resolve_tac [well_ord_cardinal_eqE] 1); +by (REPEAT_SOME assume_tac); +val cardinal_eqE = result(); + +goal Cardinal_AC.thy "!!A B. A lepoll B ==> |A| le |B|"; +by (resolve_tac [AC_well_ord RS exE] 1); +by (eresolve_tac [well_ord_lepoll_imp_le] 1); +by (assume_tac 1); +val lepoll_imp_le = result(); + +goal Cardinal_AC.thy "(i |+| j) |+| k = i |+| (j |+| k)"; +by (resolve_tac [AC_well_ord RS exE] 1); +by (resolve_tac [AC_well_ord RS exE] 1); +by (resolve_tac [AC_well_ord RS exE] 1); +by (resolve_tac [well_ord_cadd_assoc] 1); +by (REPEAT_SOME assume_tac); +val cadd_assoc = result(); + +goal Cardinal_AC.thy "(i |*| j) |*| k = i |*| (j |*| k)"; +by (resolve_tac [AC_well_ord RS exE] 1); +by (resolve_tac [AC_well_ord RS exE] 1); +by (resolve_tac [AC_well_ord RS exE] 1); +by (resolve_tac [well_ord_cmult_assoc] 1); +by (REPEAT_SOME assume_tac); +val cmult_assoc = result(); + +goal Cardinal_AC.thy "!!A. InfCard(|A|) ==> A*A eqpoll A"; +by (resolve_tac [AC_well_ord RS exE] 1); +by (eresolve_tac [well_ord_InfCard_square_eq] 1); +by (assume_tac 1); +val InfCard_square_eq = result(); + + +(*** Other applications of AC ***) + +goal Cardinal_AC.thy "!!A B. |A| le |B| ==> A lepoll B"; +by (resolve_tac [cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll RS + lepoll_trans] 1); +by (eresolve_tac [le_imp_subset RS subset_imp_lepoll RS lepoll_trans] 1); +by (resolve_tac [cardinal_eqpoll RS eqpoll_imp_lepoll] 1); +val le_imp_lepoll = result(); + +goal Cardinal_AC.thy "!!A K. Card(K) ==> |A| le K <-> A lepoll K"; +by (eresolve_tac [Card_cardinal_eq RS subst] 1 THEN + rtac iffI 1 THEN + DEPTH_SOLVE (eresolve_tac [le_imp_lepoll,lepoll_imp_le] 1)); +val le_Card_iff = result(); + +goalw Cardinal_AC.thy [surj_def] "!!f. f: surj(X,Y) ==> EX g. g: inj(Y,X)"; +by (etac CollectE 1); +by (res_inst_tac [("A1", "Y"), ("B1", "%y. f-``{y}")] (AC_Pi RS exE) 1); +by (fast_tac (ZF_cs addSEs [apply_Pair]) 1); +by (resolve_tac [exI] 1); +by (rtac f_imp_injective 1); +by (resolve_tac [Pi_type] 1 THEN assume_tac 1); +by (fast_tac (ZF_cs addDs [apply_type] addEs [memberPiE]) 1); +by (fast_tac (ZF_cs addDs [apply_type] addEs [apply_equality]) 1); +val surj_implies_inj = result(); + +(*Kunen's Lemma 10.20*) +goal Cardinal_AC.thy "!!f. f: surj(X,Y) ==> |Y| le |X|"; +by (resolve_tac [lepoll_imp_le] 1); +by (eresolve_tac [surj_implies_inj RS exE] 1); +by (rewtac lepoll_def); +by (eresolve_tac [exI] 1); +val surj_implies_cardinal_le = result(); + +(*Kunen's Lemma 10.21*) +goal Cardinal_AC.thy + "!!K. [| InfCard(K); ALL i:K. |X(i)| le K |] ==> |UN i:K. X(i)| le K"; +by (asm_full_simp_tac (ZF_ss addsimps [InfCard_is_Card, le_Card_iff]) 1); +by (resolve_tac [lepoll_trans] 1); +by (resolve_tac [InfCard_square_eq RS eqpoll_imp_lepoll] 2); +by (asm_simp_tac (ZF_ss addsimps [InfCard_is_Card, Card_cardinal_eq]) 2); +by (rewrite_goals_tac [lepoll_def]); +by (forward_tac [InfCard_is_Card RS Card_is_Ord] 1); +by (etac (AC_ball_Pi RS exE) 1); +by (resolve_tac [exI] 1); +(*Lemma needed in both subgoals, for a fixed z*) +by (subgoal_tac + "ALL z: (UN i:K. X(i)). z: X(LEAST i. z:X(i)) & (LEAST i. z:X(i)) : K" 1); +by (fast_tac (ZF_cs addSIs [Least_le RS lt_trans1 RS ltD, ltI] + addSEs [LeastI, Ord_in_Ord]) 2); +by (res_inst_tac [("c", "%z. "), + ("d", "split(%i j. converse(f`i) ` j)")] + lam_injective 1); +(*Instantiate the lemma proved above*) +by (ALLGOALS ball_tac); +by (fast_tac (ZF_cs addEs [inj_is_fun RS apply_type] + addDs [apply_type]) 1); +by (dresolve_tac [apply_type] 1); +by (eresolve_tac [conjunct2] 1); +by (asm_simp_tac (ZF_ss addsimps [left_inverse]) 1); +val cardinal_UN_le = result(); + + +goal Cardinal_AC.thy + "!!K. [| InfCard(K); ALL i:K. |X(i)| < csucc(K) |] ==> \ +\ |UN i:K. X(i)| < csucc(K)"; +by (asm_full_simp_tac + (ZF_ss addsimps [Card_lt_csucc_iff, cardinal_UN_le, + InfCard_is_Card, Card_cardinal]) 1); +val cardinal_UN_lt_csucc = result(); diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/Cardinal_AC.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Cardinal_AC.thy Tue Jul 26 13:21:20 1994 +0200 @@ -0,0 +1,9 @@ +(* Title: ZF/Cardinal_AC.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Cardinal Arithmetic WITH the Axiom of Choice +*) + +Cardinal_AC = CardinalArith + Zorn diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/Fin.ML --- a/src/ZF/Fin.ML Thu Jul 21 16:51:26 1994 +0200 +++ b/src/ZF/Fin.ML Tue Jul 26 13:21:20 1994 +0200 @@ -1,18 +1,13 @@ (* Title: ZF/ex/Fin.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge + Copyright 1994 University of Cambridge Finite powerset operator -prove X:Fin(A) ==> EX n:nat. EX f. f:bij(X,n) - card(0)=0 - [| a~:b; b: Fin(A) |] ==> card(cons(a,b)) = succ(card(b)) +prove X:Fin(A) ==> |X| < nat -b: Fin(A) ==> inj(b,b)<=surj(b,b) - -Limit(i) ==> Fin(Vfrom(A,i)) <= Un j:i. Fin(Vfrom(A,j)) -Fin(univ(A)) <= univ(A) +prove: b: Fin(A) ==> inj(b,b)<=surj(b,b) *) structure Fin = Inductive_Fun @@ -101,3 +96,11 @@ by (rtac (Fin_0_induct_lemma RS mp) 1); by (REPEAT (ares_tac (subset_refl::prems) 1)); val Fin_0_induct = result(); + +(*Functions from a finite ordinal*) +val prems = goal Fin.thy "n: nat ==> n->A <= Fin(nat*A)"; +by (nat_ind_tac "n" prems 1); +by (simp_tac (ZF_ss addsimps [Pi_empty1, Fin_0I, subset_iff, cons_iff]) 1); +by (asm_simp_tac (ZF_ss addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1); +by (fast_tac (ZF_cs addSIs [Fin_consI]) 1); +val nat_fun_subset_Fin = result(); diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/Fin.thy --- a/src/ZF/Fin.thy Thu Jul 21 16:51:26 1994 +0200 +++ b/src/ZF/Fin.thy Tue Jul 26 13:21:20 1994 +0200 @@ -1,3 +1,3 @@ (*Dummy theory to document dependencies *) -Fin = Arith + "inductive" + "constructor" + "intr_elim" + "equalities" +Fin = Arith + "inductive" + "equalities" diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/Fixedpt.ML --- a/src/ZF/Fixedpt.ML Thu Jul 21 16:51:26 1994 +0200 +++ b/src/ZF/Fixedpt.ML Tue Jul 26 13:21:20 1994 +0200 @@ -74,7 +74,7 @@ val subset0_cs = FOL_cs addSIs [ballI, InterI, CollectI, PowI, empty_subsetI] addIs [bexI, UnionI, ReplaceI, RepFunI] - addSEs [bexE, make_elim PowD, UnionE, ReplaceE, RepFunE, + addSEs [bexE, make_elim PowD, UnionE, ReplaceE2, RepFunE, CollectE, emptyE] addEs [rev_ballE, InterD, make_elim InterD, subsetD]; diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/List.ML --- a/src/ZF/List.ML Thu Jul 21 16:51:26 1994 +0200 +++ b/src/ZF/List.ML Tue Jul 26 13:21:20 1994 +0200 @@ -10,8 +10,8 @@ (val thy = Univ.thy val thy_name = "List" val rec_specs = [("list", "univ(A)", - [(["Nil"], "i", NoSyn), - (["Cons"], "[i,i]=>i", NoSyn)])] + [(["Nil"], "i", NoSyn), + (["Cons"], "[i,i]=>i", NoSyn)])] val rec_styp = "i=>i" val sintrs = ["Nil : list(A)", "[| a: A; l: list(A) |] ==> Cons(a,l) : list(A)"] diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/Makefile --- a/src/ZF/Makefile Thu Jul 21 16:51:26 1994 +0200 +++ b/src/ZF/Makefile Tue Jul 26 13:21:20 1994 +0200 @@ -19,17 +19,18 @@ BIN = $(ISABELLEBIN) COMP = $(ISABELLECOMP) FILES = ROOT.ML ZF.thy ZF.ML upair.ML subset.ML pair.ML domrange.ML \ - func.ML simpdata.ML Bool.thy Bool.ML \ + func.ML AC.thy AC.ML simpdata.ML Bool.thy Bool.ML \ Sum.thy Sum.ML QPair.thy QPair.ML mono.ML Fixedpt.thy Fixedpt.ML \ ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \ equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \ WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \ OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \ Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \ - Nat.thy Nat.ML \ + Cardinal_AC.thy Cardinal_AC.ML \ + Zorn0.thy Zorn0.ML Zorn.thy Zorn.ML Nat.thy Nat.ML Fin.ML \ Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \ QUniv.thy QUniv.ML constructor.ML Datatype.ML \ - Fin.ML List.ML ListFn.thy ListFn.ML + List.ML ListFn.thy ListFn.ML IMP_FILES = IMP/ROOT.ML IMP/Aexp.ML IMP/Aexp.thy IMP/Assign.ML IMP/Assign.thy\ IMP/Bexp.ML IMP/Bexp.thy IMP/Com.ML IMP/Com.thy IMP/Denotation.ML\ @@ -44,8 +45,9 @@ ex/ListN.ML ex/LList.ML ex/LList_Eq.ML ex/LListFn.ML ex/LListFn.thy\ ex/misc.ML ex/ParContract.ML ex/Primrec0.ML ex/Primrec0.thy\ ex/Prop.ML ex/PropLog.ML ex/PropLog.thy ex/Ramsey.ML ex/Ramsey.thy\ - ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy ex/TF.ML\ - ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML + ex/Rmap.ML ex/Term.ML ex/TermFn.ML ex/TermFn.thy \ + ex/Ntree.ML ex/Ntree.thy \ + ex/TF.ML ex/TF_Fn.ML ex/TF_Fn.thy ex/twos_compl.ML #Uses cp rather than make_database because Poly/ML allows only 3 levels $(BIN)/ZF: $(BIN)/FOL $(FILES) diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/Nat.ML --- a/src/ZF/Nat.ML Thu Jul 21 16:51:26 1994 +0200 +++ b/src/ZF/Nat.ML Tue Jul 26 13:21:20 1994 +0200 @@ -95,6 +95,15 @@ by (etac ltD 1); val Limit_nat = result(); +goal Nat.thy "!!i. Limit(i) ==> nat le i"; +by (resolve_tac [subset_imp_le] 1); +by (rtac subsetI 1); +by (eresolve_tac [nat_induct] 1); +by (fast_tac (ZF_cs addIs [Limit_has_succ RS ltD, ltI, Limit_is_Ord]) 2); +by (REPEAT (ares_tac [Limit_has_0 RS ltD, + Ord_nat, Limit_is_Ord] 1)); +val nat_le_Limit = result(); + (* succ(i): nat ==> i: nat *) val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans; diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/Order.ML --- a/src/ZF/Order.ML Thu Jul 21 16:51:26 1994 +0200 +++ b/src/ZF/Order.ML Tue Jul 26 13:21:20 1994 +0200 @@ -25,6 +25,31 @@ by (fast_tac ZF_cs 1); val part_ord_Imp_asym = result(); +(** Subset properties for the various forms of relation **) + + +(*Note: a relation s such that s<=r need not be a partial ordering*) +goalw Order.thy [part_ord_def, irrefl_def, trans_on_def] + "!!A B r. [| part_ord(A,r); B<=A |] ==> part_ord(B,r)"; +by (fast_tac ZF_cs 1); +val part_ord_subset = result(); + +goalw Order.thy [linear_def] + "!!A B r. [| linear(A,r); B<=A |] ==> linear(B,r)"; +by (fast_tac ZF_cs 1); +val linear_subset = result(); + +goalw Order.thy [tot_ord_def] + "!!A B r. [| tot_ord(A,r); B<=A |] ==> tot_ord(B,r)"; +by (fast_tac (ZF_cs addSEs [part_ord_subset, linear_subset]) 1); +val tot_ord_subset = result(); + +goalw Order.thy [well_ord_def] + "!!A B r. [| well_ord(A,r); B<=A |] ==> well_ord(B,r)"; +by (fast_tac (ZF_cs addSEs [tot_ord_subset, wf_on_subset_A]) 1); +val well_ord_subset = result(); + + (** Order-isomorphisms **) goalw Order.thy [ord_iso_def] @@ -169,7 +194,6 @@ by (safe_tac ZF_cs); val well_ord_is_trans_on = result(); - (*** Derived rules for pred(A,x,r) ***) val [major,minor] = goalw Order.thy [pred_def] diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/Perm.ML --- a/src/ZF/Perm.ML Thu Jul 21 16:51:26 1994 +0200 +++ b/src/ZF/Perm.ML Tue Jul 26 13:21:20 1994 +0200 @@ -39,7 +39,25 @@ by (fast_tac ZF_cs 1); val inj_equality = result(); -(** Bijections -- simple lemmas but no intro/elim rules -- use unfolding **) +(** A function with a left inverse is an injection **) + +val prems = goal Perm.thy + "[| f: A->B; !!x. x:A ==> d(f`x)=x |] ==> f: inj(A,B)"; +by (asm_simp_tac (ZF_ss addsimps ([inj_def] @ prems)) 1); +by (safe_tac ZF_cs); +by (eresolve_tac [subst_context RS box_equals] 1); +by (REPEAT (ares_tac prems 1)); +val f_imp_injective = result(); + +val prems = goal Perm.thy + "[| !!x. x:A ==> c(x): B; \ +\ !!x. x:A ==> d(c(x)) = x \ +\ |] ==> (lam x:A.c(x)) : inj(A,B)"; +by (res_inst_tac [("d", "d")] f_imp_injective 1); +by (ALLGOALS (asm_simp_tac (ZF_ss addsimps ([lam_type]@prems)) )); +val lam_injective = result(); + +(** Bijections **) goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> f: inj(A,B)"; by (etac IntD1 1); @@ -347,9 +365,8 @@ \ |] ==> (lam x:A.c(x)) : bij(A,B)"; by (simp_tac (ZF_ss addsimps ([lam_type]@prems)) 1); by (safe_tac ZF_cs); -(*Apply d to both sides then simplify (type constraint is essential) *) -by (dres_inst_tac [("t", "d::i=>i")] subst_context 1); -by (asm_full_simp_tac (ZF_ss addsimps prems) 1); +by (eresolve_tac [subst_context RS box_equals] 1); +by (REPEAT (ares_tac prems 1)); by (fast_tac (ZF_cs addIs prems) 1); val lam_bijective = result(); diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/ROOT.ML --- a/src/ZF/ROOT.ML Thu Jul 21 16:51:26 1994 +0200 +++ b/src/ZF/ROOT.ML Tue Jul 26 13:21:20 1994 +0200 @@ -28,8 +28,7 @@ print_depth 1; -use_thy "CardinalArith"; -use_thy "Fin"; +use_thy "Cardinal_AC"; use_thy "ListFn"; (*printing functions are inherited from FOL*) diff -r 4d1614d8f119 -r 70b789956bd3 src/ZF/Univ.ML --- a/src/ZF/Univ.ML Thu Jul 21 16:51:26 1994 +0200 +++ b/src/ZF/Univ.ML Tue Jul 26 13:21:20 1994 +0200 @@ -200,12 +200,14 @@ by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1)); val Limit_VfromE = result(); +val zero_in_Vfrom_Limit = Limit_has_0 RS ltD RS zero_in_Vfrom; + val [major,limiti] = goal Univ.thy "[| a: Vfrom(A,i); Limit(i) |] ==> {a} : Vfrom(A,i)"; by (rtac ([major,limiti] MRS Limit_VfromE) 1); by (etac ([singleton_in_Vfrom, limiti] MRS Limit_VfromI) 1); by (etac (limiti RS Limit_has_succ) 1); -val singleton_in_Vfrom_limit = result(); +val singleton_in_Vfrom_Limit = result(); val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD) and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD); @@ -220,7 +222,7 @@ by (etac Vfrom_UnI1 1); by (etac Vfrom_UnI2 1); by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1)); -val doubleton_in_Vfrom_limit = result(); +val doubleton_in_Vfrom_Limit = result(); val [aprem,bprem,limiti] = goal Univ.thy "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i) |] ==> \ @@ -233,7 +235,82 @@ by (etac Vfrom_UnI1 1); by (etac Vfrom_UnI2 1); by (REPEAT (ares_tac [limiti, Limit_has_succ, Un_least_lt] 1)); -val Pair_in_Vfrom_limit = result(); +val Pair_in_Vfrom_Limit = result(); + +goal Univ.thy "!!i. Limit(i) ==> Vfrom(A,i)*Vfrom(A,i) <= Vfrom(A,i)"; +by (REPEAT (ares_tac [subsetI,Pair_in_Vfrom_Limit] 1 + ORELSE eresolve_tac [SigmaE, ssubst] 1)); +val product_Vfrom_Limit = result(); + +val Sigma_subset_Vfrom_Limit = + [Sigma_mono, product_Vfrom_Limit] MRS subset_trans |> standard; + +val nat_subset_Vfrom_Limit = + [nat_le_Limit RS le_imp_subset, i_subset_Vfrom] MRS subset_trans + |> standard; + +val nat_into_Vfrom_Limit = standard (nat_subset_Vfrom_Limit RS subsetD); + +(** Closure under disjoint union **) + +val zero_in_Vfrom_Limit = Limit_has_0 RS ltD RS zero_in_Vfrom |> standard; + +goal Univ.thy "!!i. Limit(i) ==> 1 : Vfrom(A,i)"; +by (REPEAT (ares_tac [nat_into_Vfrom_Limit, nat_0I, nat_succI] 1)); +val one_in_Vfrom_Limit = result(); + +goalw Univ.thy [Inl_def] + "!!A a. [| a: Vfrom(A,i); Limit(i) |] ==> Inl(a) : Vfrom(A,i)"; +by (REPEAT (ares_tac [zero_in_Vfrom_Limit, Pair_in_Vfrom_Limit] 1)); +val Inl_in_Vfrom_Limit = result(); + +goalw Univ.thy [Inr_def] + "!!A b. [| b: Vfrom(A,i); Limit(i) |] ==> Inr(b) : Vfrom(A,i)"; +by (REPEAT (ares_tac [one_in_Vfrom_Limit, Pair_in_Vfrom_Limit] 1)); +val Inr_in_Vfrom_Limit = result(); + +goal Univ.thy "!!i. Limit(i) ==> Vfrom(C,i)+Vfrom(C,i) <= Vfrom(C,i)"; +by (fast_tac (sum_cs addSIs [Inl_in_Vfrom_Limit, Inr_in_Vfrom_Limit]) 1); +val sum_Vfrom_Limit = result(); + +val sum_subset_Vfrom_Limit = + [sum_mono, sum_Vfrom_Limit] MRS subset_trans |> standard; + + +(** Closure under finite powerset **) + +goal Univ.thy + "!!i. [| b: Fin(Vfrom(A,i)); Limit(i) |] ==> EX j. b <= Vfrom(A,j) & j Fin(Vfrom(A,i)) <= Vfrom(A,i)"; +by (rtac subsetI 1); +by (dresolve_tac [Fin_Vfrom_lemma] 1); +by (safe_tac ZF_cs); +by (resolve_tac [Vfrom RS ssubst] 1); +by (fast_tac (ZF_cs addSDs [ltD]) 1); +val Fin_Vfrom_Limit = result(); + +val Fin_subset_Vfrom_Limit = + [Fin_mono, Fin_Vfrom_Limit] MRS subset_trans |> standard; + +goal Univ.thy "!!i. [| n: nat; Limit(i) |] ==> n -> Vfrom(A,i) <= Vfrom(A,i)"; +by (eresolve_tac [nat_fun_subset_Fin RS subset_trans] 1); +by (REPEAT (ares_tac [Fin_subset_Vfrom_Limit, Sigma_subset_Vfrom_Limit, + nat_subset_Vfrom_Limit, subset_refl] 1)); +val nat_fun_Vfrom_Limit = result(); + +val nat_fun_subset_Vfrom_Limit = + [Pi_mono, nat_fun_Vfrom_Limit] MRS subset_trans |> standard; + (*** Properties assuming Transset(A) ***) @@ -263,8 +340,8 @@ \ : Vfrom(A,i)"; by (etac (Transset_Pair_subset RS conjE) 1); by (etac Transset_Vfrom 1); -by (REPEAT (ares_tac [Pair_in_Vfrom_limit] 1)); -val Transset_Pair_subset_Vfrom_limit = result(); +by (REPEAT (ares_tac [Pair_in_Vfrom_Limit] 1)); +val Transset_Pair_subset_Vfrom_Limit = result(); (*** Closure under product/sum applied to elements -- thus Vfrom(A,i) @@ -287,7 +364,7 @@ by (etac (Vfrom_UnI1 RS Vfrom_UnI1) 3); by (rtac (succI1 RS UnI2) 2); by (REPEAT (ares_tac [limiti, Limit_has_0, Limit_has_succ, Un_least_lt] 1)); -val in_Vfrom_limit = result(); +val in_Vfrom_Limit = result(); (** products **) @@ -303,10 +380,10 @@ val [aprem,bprem,limiti,transset] = goal Univ.thy "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ \ a*b : Vfrom(A,i)"; -by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_limit) 1); +by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_Limit) 1); by (REPEAT (ares_tac [exI, conjI, prod_in_Vfrom, transset, limiti RS Limit_has_succ] 1)); -val prod_in_Vfrom_limit = result(); +val prod_in_Vfrom_Limit = result(); (** Disjoint sums, aka Quine ordered pairs **) @@ -323,10 +400,10 @@ val [aprem,bprem,limiti,transset] = goal Univ.thy "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ \ a+b : Vfrom(A,i)"; -by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_limit) 1); +by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_Limit) 1); by (REPEAT (ares_tac [exI, conjI, sum_in_Vfrom, transset, limiti RS Limit_has_succ] 1)); -val sum_in_Vfrom_limit = result(); +val sum_in_Vfrom_Limit = result(); (** function space! **) @@ -348,10 +425,10 @@ val [aprem,bprem,limiti,transset] = goal Univ.thy "[| a: Vfrom(A,i); b: Vfrom(A,i); Limit(i); Transset(A) |] ==> \ \ a->b : Vfrom(A,i)"; -by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_limit) 1); +by (rtac ([aprem,bprem,limiti] MRS in_Vfrom_Limit) 1); by (REPEAT (ares_tac [exI, conjI, fun_in_Vfrom, transset, limiti RS Limit_has_succ] 1)); -val fun_in_Vfrom_limit = result(); +val fun_in_Vfrom_Limit = result(); (*** The set Vset(i) ***) @@ -513,33 +590,29 @@ (** Closure under unordered and ordered pairs **) goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> {a} : univ(A)"; -by (rtac singleton_in_Vfrom_limit 1); -by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1)); +by (REPEAT (ares_tac [singleton_in_Vfrom_Limit, Limit_nat] 1)); val singleton_in_univ = result(); goalw Univ.thy [univ_def] "!!A a. [| a: univ(A); b: univ(A) |] ==> {a,b} : univ(A)"; -by (rtac doubleton_in_Vfrom_limit 1); -by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1)); +by (REPEAT (ares_tac [doubleton_in_Vfrom_Limit, Limit_nat] 1)); val doubleton_in_univ = result(); goalw Univ.thy [univ_def] "!!A a. [| a: univ(A); b: univ(A) |] ==> : univ(A)"; -by (rtac Pair_in_Vfrom_limit 1); -by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1)); +by (REPEAT (ares_tac [Pair_in_Vfrom_Limit, Limit_nat] 1)); val Pair_in_univ = result(); -goal Univ.thy "univ(A)*univ(A) <= univ(A)"; -by (REPEAT (ares_tac [subsetI,Pair_in_univ] 1 - ORELSE eresolve_tac [SigmaE, ssubst] 1)); +goalw Univ.thy [univ_def] "univ(A)*univ(A) <= univ(A)"; +by (rtac (Limit_nat RS product_Vfrom_Limit) 1); val product_univ = result(); -val Sigma_subset_univ = standard - (Sigma_mono RS (product_univ RSN (2,subset_trans))); +val Sigma_subset_univ = + [Sigma_mono, product_univ] MRS subset_trans |> standard; goalw Univ.thy [univ_def] "!!a b.[| <= univ(A); Transset(A) |] ==> : univ(A)"; -by (etac Transset_Pair_subset_Vfrom_limit 1); +by (etac Transset_Pair_subset_Vfrom_Limit 1); by (REPEAT (ares_tac [Ord_nat,Limit_nat] 1)); val Transset_Pair_subset_univ = result(); @@ -555,8 +628,8 @@ (** instances for 1 and 2 **) -goal Univ.thy "1 : univ(A)"; -by (REPEAT (ares_tac [nat_into_univ, nat_0I, nat_succI] 1)); +goalw Univ.thy [univ_def] "1 : univ(A)"; +by (rtac (Limit_nat RS one_in_Vfrom_Limit) 1); val one_in_univ = result(); (*unused!*) @@ -573,25 +646,39 @@ (** Closure under disjoint union **) -goalw Univ.thy [Inl_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)"; -by (REPEAT (ares_tac [zero_in_univ,Pair_in_univ] 1)); +goalw Univ.thy [univ_def] "!!A a. a: univ(A) ==> Inl(a) : univ(A)"; +by (etac (Limit_nat RSN (2,Inl_in_Vfrom_Limit)) 1); val Inl_in_univ = result(); -goalw Univ.thy [Inr_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)"; -by (REPEAT (ares_tac [one_in_univ, Pair_in_univ] 1)); +goalw Univ.thy [univ_def] "!!A b. b: univ(A) ==> Inr(b) : univ(A)"; +by (etac (Limit_nat RSN (2,Inr_in_Vfrom_Limit)) 1); val Inr_in_univ = result(); -goal Univ.thy "univ(C)+univ(C) <= univ(C)"; -by (REPEAT (ares_tac [subsetI,Inl_in_univ,Inr_in_univ] 1 - ORELSE eresolve_tac [sumE, ssubst] 1)); +goalw Univ.thy [univ_def] "univ(C)+univ(C) <= univ(C)"; +by (rtac (Limit_nat RS sum_Vfrom_Limit) 1); val sum_univ = result(); -val sum_subset_univ = standard - (sum_mono RS (sum_univ RSN (2,subset_trans))); +val sum_subset_univ = [sum_mono, sum_univ] MRS subset_trans |> standard; + + +(** Closure under finite powerset **) + +goalw Univ.thy [univ_def] "Fin(univ(A)) <= univ(A)"; +by (rtac (Limit_nat RS Fin_Vfrom_Limit) 1); +val Fin_univ = result(); +val Fin_subset_univ = [Fin_mono, Fin_univ] MRS subset_trans |> standard; + +goalw Univ.thy [univ_def] "!!i. n: nat ==> n -> univ(A) <= univ(A)"; +by (etac (Limit_nat RSN (2,nat_fun_Vfrom_Limit)) 1); +val nat_fun_univ = result(); + +val nat_fun_subset_univ = [Pi_mono, nat_fun_univ] MRS subset_trans |> standard; + +goal Univ.thy "!!f. [| f: n -> B; B <= univ(A); n : nat |] ==> f : univ(A)"; +by (REPEAT (ares_tac [nat_fun_subset_univ RS subsetD] 1)); +val nat_fun_into_univ = result(); (** Closure under binary union -- use Un_least **) (** Closure under Collect -- use (Collect_subset RS subset_trans) **) (** Closure under RepFun -- use RepFun_subset **) - -