11 (* AC1 ==> AC18 *) |
11 (* AC1 ==> AC18 *) |
12 (* ********************************************************************** *) |
12 (* ********************************************************************** *) |
13 |
13 |
14 goal thy "!!f. [| f: (PROD b:{P(a). a:A}. b); ALL a:A. P(a)<=Q(a) |] \ |
14 goal thy "!!f. [| f: (PROD b:{P(a). a:A}. b); ALL a:A. P(a)<=Q(a) |] \ |
15 \ ==> (lam a:A. f`P(a)):(PROD a:A. Q(a))"; |
15 \ ==> (lam a:A. f`P(a)):(PROD a:A. Q(a))"; |
16 by (resolve_tac [lam_type] 1); |
16 by (rtac lam_type 1); |
17 by (dresolve_tac [apply_type] 1); |
17 by (dtac apply_type 1); |
18 by (resolve_tac [RepFunI] 1 THEN (assume_tac 1)); |
18 by (rtac RepFunI 1 THEN (assume_tac 1)); |
19 by (dresolve_tac [bspec] 1 THEN (assume_tac 1)); |
19 by (dtac bspec 1 THEN (assume_tac 1)); |
20 by (eresolve_tac [subsetD] 1 THEN (assume_tac 1)); |
20 by (etac subsetD 1 THEN (assume_tac 1)); |
21 val PROD_subsets = result(); |
21 val PROD_subsets = result(); |
22 |
22 |
23 goal thy "!!X. [| ALL A. 0 ~: A --> (EX f. f : (PROD X:A. X)); A ~= 0 |] ==> \ |
23 goal thy "!!X. [| ALL A. 0 ~: A --> (EX f. f : (PROD X:A. X)); A ~= 0 |] ==> \ |
24 \ (INT a:A. UN b:B(a). X(a, b)) <= (UN f:PROD a:A. B(a). INT a:A. X(a, f`a))"; |
24 \ (INT a:A. UN b:B(a). X(a, b)) <= (UN f:PROD a:A. B(a). INT a:A. X(a, f`a))"; |
25 by (resolve_tac [subsetI] 1); |
25 by (rtac subsetI 1); |
26 by (eres_inst_tac [("x","{{b:B(a). x:X(a,b)}. a:A}")] allE 1); |
26 by (eres_inst_tac [("x","{{b:B(a). x:X(a,b)}. a:A}")] allE 1); |
27 by (eresolve_tac [impE] 1); |
27 by (etac impE 1); |
28 by (fast_tac (AC_cs addSEs [RepFunE] addSDs [INT_E] |
28 by (fast_tac (AC_cs addSEs [RepFunE] addSDs [INT_E] |
29 addEs [UN_E, sym RS equals0D]) 1); |
29 addEs [UN_E, sym RS equals0D]) 1); |
30 by (eresolve_tac [exE] 1); |
30 by (etac exE 1); |
31 by (resolve_tac [UN_I] 1); |
31 by (rtac UN_I 1); |
32 by (fast_tac (AC_cs addSEs [PROD_subsets]) 1); |
32 by (fast_tac (AC_cs addSEs [PROD_subsets]) 1); |
33 by (simp_tac AC_ss 1); |
33 by (simp_tac AC_ss 1); |
34 by (fast_tac (FOL_cs addSEs [not_emptyE] addDs [RepFunI RSN (2, apply_type)] |
34 by (fast_tac (FOL_cs addSEs [not_emptyE] addDs [RepFunI RSN (2, apply_type)] |
35 addEs [CollectD2] addSIs [INT_I]) 1); |
35 addEs [CollectD2] addSIs [INT_I]) 1); |
36 val lemma_AC18 = result(); |
36 val lemma_AC18 = result(); |
44 (* ********************************************************************** *) |
44 (* ********************************************************************** *) |
45 (* AC18 ==> AC19 *) |
45 (* AC18 ==> AC19 *) |
46 (* ********************************************************************** *) |
46 (* ********************************************************************** *) |
47 |
47 |
48 val [prem] = goalw thy [AC18_def, AC19_def] "AC18 ==> AC19"; |
48 val [prem] = goalw thy [AC18_def, AC19_def] "AC18 ==> AC19"; |
49 by (resolve_tac [allI] 1); |
49 by (rtac allI 1); |
50 by (res_inst_tac [("B1","%x.x")] (forall_elim_vars 0 prem RS revcut_rl) 1); |
50 by (res_inst_tac [("B1","%x.x")] (forall_elim_vars 0 prem RS revcut_rl) 1); |
51 by (fast_tac AC_cs 1); |
51 by (fast_tac AC_cs 1); |
52 qed "AC18_AC19"; |
52 qed "AC18_AC19"; |
53 |
53 |
54 (* ********************************************************************** *) |
54 (* ********************************************************************** *) |
62 addSDs [sym RS (RepFun_eq_0_iff RS iffD1)]) 1); |
62 addSDs [sym RS (RepFun_eq_0_iff RS iffD1)]) 1); |
63 val RepRep_conj = result(); |
63 val RepRep_conj = result(); |
64 |
64 |
65 goal thy "!!c. [|c : a; x = c Un {0}; x ~: a |] ==> x - {0} : a"; |
65 goal thy "!!c. [|c : a; x = c Un {0}; x ~: a |] ==> x - {0} : a"; |
66 by (hyp_subst_tac 1); |
66 by (hyp_subst_tac 1); |
67 by (resolve_tac [subst_elem] 1 THEN (assume_tac 1)); |
67 by (rtac subst_elem 1 THEN (assume_tac 1)); |
68 by (resolve_tac [equalityI] 1); |
68 by (rtac equalityI 1); |
69 by (fast_tac AC_cs 1); |
69 by (fast_tac AC_cs 1); |
70 by (resolve_tac [subsetI] 1); |
70 by (rtac subsetI 1); |
71 by (excluded_middle_tac "x=0" 1); |
71 by (excluded_middle_tac "x=0" 1); |
72 by (fast_tac AC_cs 1); |
72 by (fast_tac AC_cs 1); |
73 by (fast_tac (AC_cs addEs [notE, subst_elem] addSIs [equalityI]) 1); |
73 by (fast_tac (AC_cs addEs [notE, subst_elem] addSIs [equalityI]) 1); |
74 val lemma1_1 = result(); |
74 val lemma1_1 = result(); |
75 |
75 |
79 by (fast_tac (AC_cs addSEs [RepFunI, RepFunE, lemma1_1] |
79 by (fast_tac (AC_cs addSEs [RepFunI, RepFunE, lemma1_1] |
80 addSDs [apply_type]) 1); |
80 addSDs [apply_type]) 1); |
81 val lemma1_2 = result(); |
81 val lemma1_2 = result(); |
82 |
82 |
83 goal thy "!!A. EX f. f: (PROD B:{u_(a). a:A}. B) ==> EX f. f: (PROD B:A. B)"; |
83 goal thy "!!A. EX f. f: (PROD B:{u_(a). a:A}. B) ==> EX f. f: (PROD B:A. B)"; |
84 by (eresolve_tac [exE] 1); |
84 by (etac exE 1); |
85 by (res_inst_tac |
85 by (res_inst_tac |
86 [("x","lam a:A. if(f`(u_(a)) : a, f`(u_(a)), f`(u_(a))-{0})")] exI 1); |
86 [("x","lam a:A. if(f`(u_(a)) : a, f`(u_(a)), f`(u_(a))-{0})")] exI 1); |
87 by (resolve_tac [lam_type] 1); |
87 by (rtac lam_type 1); |
88 by (split_tac [expand_if] 1); |
88 by (split_tac [expand_if] 1); |
89 by (resolve_tac [conjI] 1); |
89 by (rtac conjI 1); |
90 by (fast_tac AC_cs 1); |
90 by (fast_tac AC_cs 1); |
91 by (fast_tac (AC_cs addSEs [lemma1_2]) 1); |
91 by (fast_tac (AC_cs addSEs [lemma1_2]) 1); |
92 val lemma1 = result(); |
92 val lemma1 = result(); |
93 |
93 |
94 goalw thy [u_def] "!!a. a~=0 ==> 0: (UN b:u_(a). b)"; |
94 goalw thy [u_def] "!!a. a~=0 ==> 0: (UN b:u_(a). b)"; |
95 by (fast_tac (AC_cs addSEs [not_emptyE] addSIs [UN_I, RepFunI]) 1); |
95 by (fast_tac (AC_cs addSEs [not_emptyE] addSIs [UN_I, RepFunI]) 1); |
96 val lemma2_1 = result(); |
96 val lemma2_1 = result(); |
97 |
97 |
98 goal thy "!!A C. [| A~=0; 0~:A |] ==> (INT x:{u_(a). a:A}. UN b:x. b) ~= 0"; |
98 goal thy "!!A C. [| A~=0; 0~:A |] ==> (INT x:{u_(a). a:A}. UN b:x. b) ~= 0"; |
99 by (eresolve_tac [not_emptyE] 1); |
99 by (etac not_emptyE 1); |
100 by (res_inst_tac [("a","0")] not_emptyI 1); |
100 by (res_inst_tac [("a","0")] not_emptyI 1); |
101 by (fast_tac (AC_cs addSIs [INT_I, RepFunI, lemma2_1] addSEs [RepFunE]) 1); |
101 by (fast_tac (AC_cs addSIs [INT_I, RepFunI, lemma2_1] addSEs [RepFunE]) 1); |
102 val lemma2 = result(); |
102 val lemma2 = result(); |
103 |
103 |
104 goal thy "!!F. (UN f:F. P(f)) ~= 0 ==> F ~= 0"; |
104 goal thy "!!F. (UN f:F. P(f)) ~= 0 ==> F ~= 0"; |
108 goalw thy AC_defs "!!Z. AC19 ==> AC1"; |
108 goalw thy AC_defs "!!Z. AC19 ==> AC1"; |
109 by (REPEAT (resolve_tac [allI,impI] 1)); |
109 by (REPEAT (resolve_tac [allI,impI] 1)); |
110 by (excluded_middle_tac "A=0" 1); |
110 by (excluded_middle_tac "A=0" 1); |
111 by (fast_tac (AC_cs addSIs [empty_fun]) 2); |
111 by (fast_tac (AC_cs addSIs [empty_fun]) 2); |
112 by (eres_inst_tac [("x","{u_(a). a:A}")] allE 1); |
112 by (eres_inst_tac [("x","{u_(a). a:A}")] allE 1); |
113 by (eresolve_tac [impE] 1); |
113 by (etac impE 1); |
114 by (eresolve_tac [RepRep_conj] 1 THEN (assume_tac 1)); |
114 by (etac RepRep_conj 1 THEN (assume_tac 1)); |
115 by (resolve_tac [lemma1] 1); |
115 by (rtac lemma1 1); |
116 by (dresolve_tac [lemma2] 1 THEN (assume_tac 1)); |
116 by (dtac lemma2 1 THEN (assume_tac 1)); |
117 by (dres_inst_tac [("P","%x. x~=0")] subst 1 THEN (assume_tac 1)); |
117 by (dres_inst_tac [("P","%x. x~=0")] subst 1 THEN (assume_tac 1)); |
118 by (fast_tac (AC_cs addSEs [lemma3 RS not_emptyE]) 1); |
118 by (fast_tac (AC_cs addSEs [lemma3 RS not_emptyE]) 1); |
119 qed "AC19_AC1"; |
119 qed "AC19_AC1"; |
120 |
120 |
121 |
121 |