author | paulson |
Thu, 06 Aug 1998 10:38:57 +0200 | |
changeset 5265 | 9d1d4c43c76d |
parent 5241 | e5129172cb2b |
child 9683 | f87c8c449018 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/AC18_AC19.ML |
1123 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1123 | 4 |
|
5 |
The proof of AC1 ==> AC18 ==> AC19 ==> AC1 |
|
6 |
*) |
|
7 |
||
8 |
open AC18_AC19; |
|
9 |
||
10 |
(* ********************************************************************** *) |
|
1461 | 11 |
(* AC1 ==> AC18 *) |
1123 | 12 |
(* ********************************************************************** *) |
13 |
||
5137 | 14 |
Goal "[| f: (PROD b:{P(a). a:A}. b); ALL a:A. P(a)<=Q(a) |] \ |
1461 | 15 |
\ ==> (lam a:A. f`P(a)):(PROD a:A. Q(a))"; |
1206 | 16 |
by (rtac lam_type 1); |
17 |
by (dtac apply_type 1); |
|
18 |
by (rtac RepFunI 1 THEN (assume_tac 1)); |
|
19 |
by (dtac bspec 1 THEN (assume_tac 1)); |
|
20 |
by (etac subsetD 1 THEN (assume_tac 1)); |
|
3731 | 21 |
qed "PROD_subsets"; |
1123 | 22 |
|
5137 | 23 |
Goal "[| ALL A. 0 ~: A --> (EX f. f : (PROD X:A. X)); A ~= 0 |] ==> \ |
1123 | 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))"; |
1206 | 25 |
by (rtac subsetI 1); |
1123 | 26 |
by (eres_inst_tac [("x","{{b:B(a). x:X(a,b)}. a:A}")] allE 1); |
1206 | 27 |
by (etac impE 1); |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
28 |
by (Fast_tac 1); |
1206 | 29 |
by (etac exE 1); |
30 |
by (rtac UN_I 1); |
|
4091 | 31 |
by (fast_tac (claset() addSEs [PROD_subsets]) 1); |
2469 | 32 |
by (Simp_tac 1); |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
33 |
by (fast_tac (claset() addSEs [not_emptyE] |
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
34 |
addDs [RepFunI RSN (2, apply_type)]) 1); |
3731 | 35 |
qed "lemma_AC18"; |
1123 | 36 |
|
37 |
val [prem] = goalw thy (AC18_def::AC_defs) "AC1 ==> AC18"; |
|
38 |
by (resolve_tac [prem RS revcut_rl] 1); |
|
4091 | 39 |
by (fast_tac (claset() addSEs [lemma_AC18, not_emptyE, apply_type] |
1461 | 40 |
addSIs [equalityI, INT_I, UN_I]) 1); |
1196 | 41 |
qed "AC1_AC18"; |
1123 | 42 |
|
43 |
(* ********************************************************************** *) |
|
1461 | 44 |
(* AC18 ==> AC19 *) |
1123 | 45 |
(* ********************************************************************** *) |
46 |
||
47 |
val [prem] = goalw thy [AC18_def, AC19_def] "AC18 ==> AC19"; |
|
1206 | 48 |
by (rtac allI 1); |
3840 | 49 |
by (res_inst_tac [("B1","%x. x")] (forall_elim_vars 0 prem RS revcut_rl) 1); |
2469 | 50 |
by (Fast_tac 1); |
1196 | 51 |
qed "AC18_AC19"; |
1123 | 52 |
|
53 |
(* ********************************************************************** *) |
|
1461 | 54 |
(* AC19 ==> AC1 *) |
1123 | 55 |
(* ********************************************************************** *) |
56 |
||
5068 | 57 |
Goalw [u_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
58 |
"[| A ~= 0; 0 ~: A |] ==> {u_(a). a:A} ~= 0 & 0 ~: {u_(a). a:A}"; |
5241 | 59 |
by (fast_tac (claset() addSIs [not_emptyI] |
60 |
addSEs [not_emptyE] |
|
1461 | 61 |
addSDs [sym RS (RepFun_eq_0_iff RS iffD1)]) 1); |
3731 | 62 |
qed "RepRep_conj"; |
1123 | 63 |
|
5137 | 64 |
Goal "[|c : a; x = c Un {0}; x ~: a |] ==> x - {0} : a"; |
1123 | 65 |
by (hyp_subst_tac 1); |
1206 | 66 |
by (rtac subst_elem 1 THEN (assume_tac 1)); |
67 |
by (rtac equalityI 1); |
|
2469 | 68 |
by (Fast_tac 1); |
1206 | 69 |
by (rtac subsetI 1); |
1123 | 70 |
by (excluded_middle_tac "x=0" 1); |
2469 | 71 |
by (Fast_tac 1); |
4091 | 72 |
by (fast_tac (claset() addEs [notE, subst_elem]) 1); |
1123 | 73 |
val lemma1_1 = result(); |
74 |
||
5068 | 75 |
Goalw [u_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
76 |
"[| f`(u_(a)) ~: a; f: (PROD B:{u_(a). a:A}. B); a:A |] \ |
1461 | 77 |
\ ==> f`(u_(a))-{0} : a"; |
5241 | 78 |
by (fast_tac (claset() addSEs [lemma1_1] addSDs [apply_type]) 1); |
1123 | 79 |
val lemma1_2 = result(); |
80 |
||
5137 | 81 |
Goal "EX f. f: (PROD B:{u_(a). a:A}. B) ==> EX f. f: (PROD B:A. B)"; |
1206 | 82 |
by (etac exE 1); |
1123 | 83 |
by (res_inst_tac |
1461 | 84 |
[("x","lam a:A. if(f`(u_(a)) : a, f`(u_(a)), f`(u_(a))-{0})")] exI 1); |
1206 | 85 |
by (rtac lam_type 1); |
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
5068
diff
changeset
|
86 |
by (split_tac [split_if] 1); |
1206 | 87 |
by (rtac conjI 1); |
2469 | 88 |
by (Fast_tac 1); |
4091 | 89 |
by (fast_tac (claset() addSEs [lemma1_2]) 1); |
1123 | 90 |
val lemma1 = result(); |
91 |
||
5137 | 92 |
Goalw [u_def] "a~=0 ==> 0: (UN b:u_(a). b)"; |
4091 | 93 |
by (fast_tac (claset() addSEs [not_emptyE] addSIs [UN_I, RepFunI]) 1); |
1123 | 94 |
val lemma2_1 = result(); |
95 |
||
5137 | 96 |
Goal "[| A~=0; 0~:A |] ==> (INT x:{u_(a). a:A}. UN b:x. b) ~= 0"; |
1206 | 97 |
by (etac not_emptyE 1); |
1123 | 98 |
by (res_inst_tac [("a","0")] not_emptyI 1); |
5241 | 99 |
by (fast_tac (claset() addSIs [lemma2_1]) 1); |
1123 | 100 |
val lemma2 = result(); |
101 |
||
5137 | 102 |
Goal "(UN f:F. P(f)) ~= 0 ==> F ~= 0"; |
4091 | 103 |
by (fast_tac (claset() addSEs [not_emptyE]) 1); |
1123 | 104 |
val lemma3 = result(); |
105 |
||
5137 | 106 |
Goalw AC_defs "AC19 ==> AC1"; |
1123 | 107 |
by (REPEAT (resolve_tac [allI,impI] 1)); |
108 |
by (excluded_middle_tac "A=0" 1); |
|
4091 | 109 |
by (fast_tac (claset() addSIs [exI, empty_fun]) 2); |
1123 | 110 |
by (eres_inst_tac [("x","{u_(a). a:A}")] allE 1); |
1206 | 111 |
by (etac impE 1); |
112 |
by (etac RepRep_conj 1 THEN (assume_tac 1)); |
|
113 |
by (rtac lemma1 1); |
|
114 |
by (dtac lemma2 1 THEN (assume_tac 1)); |
|
1123 | 115 |
by (dres_inst_tac [("P","%x. x~=0")] subst 1 THEN (assume_tac 1)); |
4091 | 116 |
by (fast_tac (claset() addSEs [lemma3 RS not_emptyE]) 1); |
1196 | 117 |
qed "AC19_AC1"; |
1123 | 118 |
|
119 |