# HG changeset patch # User lcp # Date 798800812 -7200 # Node ID 96dfc9977bf50014b5343ff151f604ce299cab81 # Parent d290a2f3b9b0c90d01d83d5854fed5afc3261548 Simple updates for compatibility with KG diff -r d290a2f3b9b0 -r 96dfc9977bf5 src/ZF/AC/AC_Equiv.ML --- a/src/ZF/AC/AC_Equiv.ML Tue Apr 25 11:01:57 1995 +0200 +++ b/src/ZF/AC/AC_Equiv.ML Tue Apr 25 11:06:52 1995 +0200 @@ -7,6 +7,13 @@ open AC_Equiv; +val WO_defs = [WO1_def, WO2_def, WO3_def, WO4_def, WO5_def, WO6_def, WO8_def]; + +val AC_defs = [AC0_def, AC1_def, AC2_def, AC3_def, AC4_def, AC5_def, + AC6_def, AC7_def, AC8_def, AC9_def, AC10_def, AC11_def, + AC12_def, AC13_def, AC14_def, AC15_def, AC16_def, + AC17_def, AC18_def, AC19_def]; + val AC_aux_defs = [pairwise_disjoint_def, sets_of_size_between_def]; (* ******************************************** *) diff -r d290a2f3b9b0 -r 96dfc9977bf5 src/ZF/AC/AC_Equiv.thy --- a/src/ZF/AC/AC_Equiv.thy Tue Apr 25 11:01:57 1995 +0200 +++ b/src/ZF/AC/AC_Equiv.thy Tue Apr 25 11:06:52 1995 +0200 @@ -22,9 +22,10 @@ (* Axioms of Choice *) AC0, AC1, AC2, AC3, AC4, AC5, AC6, AC7, AC8, AC9, - AC11, AC12, AC14, AC15, AC17, AC18, AC19 :: "o" + AC11, AC12, AC14, AC15, AC17, AC19 :: "o" AC10, AC13 :: "i => o" AC16 :: "[i, i] => o" + AC18 :: "prop" ("AC18") (* Auxiliary definitions used in theorems *) first :: "[i, i, i] => o" @@ -114,12 +115,9 @@ AC17_def "AC17 == ALL A. ALL g: (Pow(A)-{0} -> A) -> Pow(A)-{0}. \ \ EX f: Pow(A)-{0} -> A. f`(g`f) : g`f" -(***problems! X is free, and is higher-order! - AC18_def "AC18 == ALL A. A~=0 --> (ALL F. (domain(F) = A & \ -\ (ALL a:A. F`a ~= 0)) --> \ -\ ((INT a:A. UN b:F`a. X(a,b)) = \ -\ (UN f: PROD a:A. F`a. INT a:A. X(a, f`a))))" -***) + AC18_def "AC18 == (!!X A B. A~=0 & (ALL a:A. B(a) ~= 0) --> \ +\ ((INT a:A. UN b:B(a). X(a,b)) = \ +\ (UN f: PROD a:A. B(a). INT a:A. X(a, f`a))))" AC19_def "AC19 == ALL A. A~=0 & 0~:A --> ((INT a:A. UN b:a. b) = \ \ (UN f:{f: A->Union(A). ALL B:A. f`B:B}. INT a:A. f`a))" diff -r d290a2f3b9b0 -r 96dfc9977bf5 src/ZF/AC/ROOT.ML --- a/src/ZF/AC/ROOT.ML Tue Apr 25 11:01:57 1995 +0200 +++ b/src/ZF/AC/ROOT.ML Tue Apr 25 11:06:52 1995 +0200 @@ -15,4 +15,19 @@ time_use_thy "WO6_WO1"; +(*New ones pending on ~kg10006/isabelle +time_use "AC10_AC11.ML"; +time_use "AC11_AC12.ML"; +time_use "AC1_AC13.ML"; +time_use "AC13_AC1.ML"; +time_use "AC13_AC13.ML"; +time_use "AC13_AC14.ML"; +time_use "AC14_AC15.ML"; +time_use_thy "lemmas_AC13_AC15"; +time_use_thy "AC10_AC13"; +time_use_thy "AC11_AC14"; +time_use_thy "AC12_AC15"; +time_use "AC14_AC15.ML"; +*) + writeln"END: Root file for ZF/AC"; diff -r d290a2f3b9b0 -r 96dfc9977bf5 src/ZF/AC/WO6_WO1.ML --- a/src/ZF/AC/WO6_WO1.ML Tue Apr 25 11:01:57 1995 +0200 +++ b/src/ZF/AC/WO6_WO1.ML Tue Apr 25 11:06:52 1995 +0200 @@ -159,12 +159,12 @@ (* Case 2 : vv2_subset *) (* ********************************************************************** *) -goalw thy [uu_def] "!!f. [| b EX d \ -\ domain(uu(f, b, g, d)) eqpoll succ(m); \ -\ ALL b uu(f,b,g,LEAST d. uu(f,b,g,d)~=0) : f`b -> f`g"; -by (eres_inst_tac [("x","g")] oallE 1 THEN (contr_tac 2)); -by (eres_inst_tac [("P","%z. ?QQ(z) ~= 0 --> ?RR(z)")] oallE 1); -by (eresolve_tac [impE] 1); -by (eresolve_tac [uu_not_empty RS (uu_subset1 RS not_empty_rel_imp_domain)] 1 - THEN REPEAT (assume_tac 1)); -by (eresolve_tac [Least_uu_not_empty_lt_a RSN (2, notE)] 2 - THEN (TRYALL assume_tac)); + "!!a. [| ALL g \ +\ domain(uu(f, b, g, d)) eqpoll succ(m); \ +\ ALL b uu(f, b, g, LEAST d. uu(f,b,g,d)~=0) : f`b -> f`g"; +by (dres_inst_tac [("x2","g")] (ospec RS ospec RS mp) 1); +by (rtac ([uu_subset1, uu_not_empty] MRS not_empty_rel_imp_domain) 3); +by (rtac Least_uu_not_empty_lt_a 2 THEN TRYALL assume_tac); by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RS (Least_uu_not_empty_lt_a RSN (2, uu_lepoll_m) RSN (2, uu_subset1 RSN (4, rel_is_fun)))] 1 - THEN (TRYALL assume_tac)); -by (resolve_tac [eqpoll_sym RS eqpoll_imp_lepoll RSN (2, - supset_lepoll_imp_eq)] 1); + THEN TRYALL assume_tac); +by (rtac (eqpoll_sym RS eqpoll_imp_lepoll RSN (2, supset_lepoll_imp_eq)) 1); by (REPEAT (fast_tac (AC_cs addSIs [domain_uu_subset, nat_succI]) 1)); val uu_Least_is_fun = result(); @@ -382,8 +378,7 @@ (* ********************************************************************** *) goalw thy [WO6_def, NN_def] "!!y. WO6 ==> NN(y) ~= 0"; -by (eresolve_tac [allE] 1); -by (fast_tac (ZF_cs addSIs [not_emptyI]) 1); +by (fast_tac (ZF_cs addEs [equals0D]) 1); val WO6_imp_NN_not_empty = result(); (* ********************************************************************** *)