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