# HG changeset patch # User paulson # Date 1008684207 -3600 # Node ID e9a7292593856ae52ad898e585e1d22b8263a0a0 # Parent 626eaec7b5ad00738076fb8037a5e6a5e9456313 replaced lepoll_lesspoll_lesspoll, lesspoll_lepoll_lesspoll by lesspoll_trans1, lesspoll_trans2 diff -r 626eaec7b5ad -r e9a729259385 src/ZF/AC/AC16_WO4.ML --- a/src/ZF/AC/AC16_WO4.ML Tue Dec 18 14:27:57 2001 +0100 +++ b/src/ZF/AC/AC16_WO4.ML Tue Dec 18 15:03:27 2001 +0100 @@ -76,7 +76,10 @@ Goal "[| ~(\\x \\ A. f`x=y); f \\ inj(A, B); y \\ B |] \ \ ==> (\\a \\ succ(A). if(a=A, y, f`a)) \\ inj(succ(A), B)"; by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1); -by (auto_tac (claset(), simpset() addsimps [inj_is_fun RS apply_type])); +by (force_tac (claset(), simpset() addsimps [inj_is_fun RS apply_type]) 1); +(*this preliminary simplification prevents looping somehow*) +by (Asm_simp_tac 1); +by (force_tac (claset(), simpset() addsimps []) 1); qed "succ_not_lepoll_lemma"; Goalw [lepoll_def, eqpoll_def, bij_def, surj_def] @@ -251,14 +254,14 @@ Goal "[| l eqpoll a; a \\ y |] ==> y - a eqpoll y"; by (cut_facts_tac [WO_R, Infinite, lnat] 1); -by (fast_tac (empty_cs addIs [lepoll_lesspoll_lesspoll] +by (fast_tac (empty_cs addIs [lesspoll_trans1] addSIs [Card_cardinal, Diff_lesspoll_eqpoll_Card RS eqpoll_trans, Card_cardinal RS Card_is_Ord RS nat_le_infinite_Ord RS le_imp_lepoll] addSEs [well_ord_cardinal_eqpoll, well_ord_cardinal_eqpoll RS eqpoll_sym, eqpoll_sym RS eqpoll_imp_lepoll, - n_lesspoll_nat RS lesspoll_lepoll_lesspoll, + n_lesspoll_nat RS lesspoll_trans2, well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_infinite]) 1); qed "Diff_Finite_eqpoll"; @@ -605,3 +608,4 @@ by (Clarify_tac 1); by (DEPTH_SOLVE (ares_tac [export conclusion] 1)); qed "AC16_WO4"; + diff -r 626eaec7b5ad -r e9a729259385 src/ZF/AC/AC_Equiv.thy --- a/src/ZF/AC/AC_Equiv.thy Tue Dec 18 14:27:57 2001 +0100 +++ b/src/ZF/AC/AC_Equiv.thy Tue Dec 18 15:03:27 2001 +0100 @@ -13,9 +13,7 @@ *) -AC_Equiv = CardinalArith + Univ + - (*NOT "Main" because that theory includes AC!!!*) - +AC_Equiv = Main + (*obviously not Main_ZFC*) consts diff -r 626eaec7b5ad -r e9a729259385 src/ZF/AC/Cardinal_aux.ML --- a/src/ZF/AC/Cardinal_aux.ML Tue Dec 18 14:27:57 2001 +0100 +++ b/src/ZF/AC/Cardinal_aux.ML Tue Dec 18 15:03:27 2001 +0100 @@ -171,8 +171,7 @@ (* Diff_lesspoll_eqpoll_Card *) (* ********************************************************************** *) -Goal "[| A eqpoll a; ~Finite(a); Card(a); B lesspoll a; \ -\ A-B lesspoll a |] ==> P"; +Goal "[| A\\a; ~Finite(a); Card(a); B lesspoll a; A-B lesspoll a |] ==> P"; by (REPEAT (eresolve_tac [lesspoll_imp_ex_lt_eqpoll RS exE, Card_is_Ord, conjE] 1)); by (forw_inst_tac [("j","xa")] ([lt_Ord, lt_Ord] MRS Un_upper1_le) 1 @@ -192,11 +191,10 @@ by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_Finite] 2); by (fast_tac (claset() addDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_Finite]) 2); -by (dresolve_tac [ Un_lepoll_Inf_Ord] 1 - THEN (REPEAT (assume_tac 1))); +by (dresolve_tac [ Un_lepoll_Inf_Ord] 1 THEN (REPEAT (assume_tac 1))); by (fast_tac (claset() addSEs [ltE, Ord_in_Ord]) 1); -by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_trans RSN - (3, lt_Card_imp_lesspoll RS lepoll_lesspoll_lesspoll)] 1 +by (dresolve_tac [subset_Un_Diff RS subset_imp_lepoll RS lepoll_trans RS + (lt_Card_imp_lesspoll RSN (2, lesspoll_trans1))] 1 THEN (TRYALL assume_tac)); by (fast_tac (claset() addSDs [lesspoll_def RS def_imp_iff RS iffD1]) 1); qed "Diff_lesspoll_eqpoll_Card_lemma"; diff -r 626eaec7b5ad -r e9a729259385 src/ZF/AC/DC.ML --- a/src/ZF/AC/DC.ML Tue Dec 18 14:27:57 2001 +0100 +++ b/src/ZF/AC/DC.ML Tue Dec 18 15:03:27 2001 +0100 @@ -62,8 +62,8 @@ by (Blast_tac 2); by (Clarify_tac 1); by (forward_tac [fun_is_rel RS image_subset RS PowI RS (all_ex RS bspec)] 1); -by (eresolve_tac [[n_lesspoll_nat, nat_into_Ord RSN (2, image_Ord_lepoll)] - MRS lepoll_lesspoll_lesspoll RSN (2, impE)] 1 +by (eresolve_tac [[nat_into_Ord RSN (2, image_Ord_lepoll), n_lesspoll_nat] + MRS lesspoll_trans1 RSN (2, impE)] 1 THEN REPEAT (assume_tac 1)); by (etac bexE 1); by (res_inst_tac [("x","cons(, g)")] exI 1); @@ -517,8 +517,8 @@ addsimps [[lam_type_RepFun, subset_refl] MRS image_fun]) 1); by (etac lemmaX 1 THEN assume_tac 1); by (blast_tac (claset() addIs [Card_is_Ord RSN (2, OrdmemD) RS subsetD]) 1); -by (fast_tac (claset() addSEs [[in_Card_imp_lesspoll, RepFun_lepoll] - MRS lepoll_lesspoll_lesspoll]) 1); +by (blast_tac (claset() addIs [lesspoll_trans1, in_Card_imp_lesspoll, + RepFun_lepoll]) 1); qed "lemma"; Goalw [DC_def, WO1_def] "WO1 ==> \\K. Card(K) --> DC(K)"; diff -r 626eaec7b5ad -r e9a729259385 src/ZF/AC/WO2_AC16.ML --- a/src/ZF/AC/WO2_AC16.ML Tue Dec 18 14:27:57 2001 +0100 +++ b/src/ZF/AC/WO2_AC16.ML Tue Dec 18 15:03:27 2001 +0100 @@ -145,12 +145,8 @@ by (forward_tac [bij_is_surj RS surj_image_eq] 1); by (dresolve_tac [[bij_is_fun, subset_refl] MRS image_fun] 1); by (dresolve_tac [sym RS trans] 1 THEN (assume_tac 1)); -by (hyp_subst_tac 1); -by (rtac lepoll_lesspoll_lesspoll 1); -by (eresolve_tac [lt_trans1 RSN (2, lt_Card_imp_lesspoll)] 1 - THEN REPEAT (assume_tac 1)); -by (rtac UN_lepoll 1 - THEN (TRYALL (fast_tac (claset() addSEs [lt_Ord])))); +by (blast_tac (claset() addIs [lesspoll_trans1, UN_lepoll, lt_Ord, + lt_trans1 RSN (2, lt_Card_imp_lesspoll)]) 1); qed "Union_lesspoll"; (* ********************************************************************** *) diff -r 626eaec7b5ad -r e9a729259385 src/ZF/Cardinal.ML --- a/src/ZF/Cardinal.ML Tue Dec 18 14:27:57 2001 +0100 +++ b/src/ZF/Cardinal.ML Tue Dec 18 15:03:27 2001 +0100 @@ -169,15 +169,15 @@ by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1); qed "lesspoll_trans"; +Goalw [lesspoll_def] + "[| X lepoll Y; Y lesspoll Z |] ==> X lesspoll Z"; +by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1); +qed "lesspoll_trans1"; + Goalw [lesspoll_def] "[| X lesspoll Y; Y lepoll Z |] ==> X lesspoll Z"; by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1); -qed "lesspoll_lepoll_lesspoll"; - -Goalw [lesspoll_def] - "[| X lesspoll Y; Z lepoll X |] ==> Z lesspoll Y"; -by (blast_tac (claset() addSEs [eqpollE] addIs [eqpollI, lepoll_trans]) 1); -qed "lepoll_lesspoll_lesspoll"; +qed "lesspoll_trans2"; (** LEAST -- the least number operator [from HOL/Univ.ML] **)