1 (* Title: ZF/AC/AC2_AC6.ML |
|
2 ID: $Id$ |
|
3 Author: Krzysztof Grabczewski |
|
4 |
|
5 The proofs needed to show that each of AC2, AC3, ..., AC6 is equivalent |
|
6 to AC0 and AC1: |
|
7 AC1 ==> AC2 ==> AC1 |
|
8 AC1 ==> AC4 ==> AC3 ==> AC1 |
|
9 AC4 ==> AC5 ==> AC4 |
|
10 AC1 <-> AC6 |
|
11 *) |
|
12 |
|
13 (* ********************************************************************** *) |
|
14 (* AC1 ==> AC2 *) |
|
15 (* ********************************************************************** *) |
|
16 |
|
17 Goal "[| f:(\\<Pi>X \\<in> A. X); B \\<in> A; 0\\<notin>A |] ==> {f`B} \\<subseteq> B Int {f`C. C \\<in> A}"; |
|
18 by (fast_tac (claset() addSEs [apply_type]) 1); |
|
19 val lemma1 = result(); |
|
20 |
|
21 Goalw [pairwise_disjoint_def] |
|
22 "[| pairwise_disjoint(A); B \\<in> A; C \\<in> A; D \\<in> B; D \\<in> C |] ==> f`B = f`C"; |
|
23 by (Fast_tac 1); |
|
24 val lemma2 = result(); |
|
25 |
|
26 Goalw AC_defs "AC1 ==> AC2"; |
|
27 by (rtac allI 1); |
|
28 by (rtac impI 1); |
|
29 by (REPEAT (eresolve_tac [asm_rl,conjE,allE,exE,impE] 1)); |
|
30 by (REPEAT (resolve_tac [exI,ballI,equalityI] 1)); |
|
31 by (rtac lemma1 2 THEN (REPEAT (assume_tac 2))); |
|
32 by (fast_tac (claset() addSEs [lemma2] addEs [apply_type]) 1); |
|
33 qed "AC1_AC2"; |
|
34 |
|
35 |
|
36 (* ********************************************************************** *) |
|
37 (* AC2 ==> AC1 *) |
|
38 (* ********************************************************************** *) |
|
39 |
|
40 Goal "0\\<notin>A ==> 0 \\<notin> {B*{B}. B \\<in> A}"; |
|
41 by (fast_tac (claset() addSDs [sym RS (Sigma_empty_iff RS iffD1)]) 1); |
|
42 val lemma1 = result(); |
|
43 |
|
44 Goal "[| X*{X} Int C = {y}; X \\<in> A |] \ |
|
45 \ ==> (THE y. X*{X} Int C = {y}): X*A"; |
|
46 by (rtac subst_elem 1); |
|
47 by (fast_tac (claset() addSIs [the_equality] |
|
48 addSEs [sym RS trans RS (singleton_eq_iff RS iffD1)]) 2); |
|
49 by (blast_tac (claset() addSEs [equalityE]) 1); |
|
50 val lemma2 = result(); |
|
51 |
|
52 Goal "\\<forall>D \\<in> {E*{E}. E \\<in> A}. \\<exists>y. D Int C = {y} \ |
|
53 \ ==> (\\<lambda>x \\<in> A. fst(THE z. (x*{x} Int C = {z}))) \\<in> (\\<Pi>X \\<in> A. X)"; |
|
54 by (fast_tac (claset() addSEs [lemma2] |
|
55 addSIs [lam_type, RepFunI, fst_type]) 1); |
|
56 val lemma3 = result(); |
|
57 |
|
58 Goalw (AC_defs@AC_aux_defs) "AC2 ==> AC1"; |
|
59 by (REPEAT (resolve_tac [allI, impI] 1)); |
|
60 by (REPEAT (eresolve_tac [allE, impE] 1)); |
|
61 by (fast_tac (claset() addSEs [lemma3]) 2); |
|
62 by (fast_tac (claset() addSIs [lemma1, equals0I]) 1); |
|
63 qed "AC2_AC1"; |
|
64 |
|
65 |
|
66 (* ********************************************************************** *) |
|
67 (* AC1 ==> AC4 *) |
|
68 (* ********************************************************************** *) |
|
69 |
|
70 Goal "0 \\<notin> {R``{x}. x \\<in> domain(R)}"; |
|
71 by (Blast_tac 1); |
|
72 val lemma = result(); |
|
73 |
|
74 Goalw AC_defs "AC1 ==> AC4"; |
|
75 by (REPEAT (resolve_tac [allI, impI] 1)); |
|
76 by (REPEAT (eresolve_tac [allE, lemma RSN (2, impE), exE] 1)); |
|
77 by (best_tac (claset() addSIs [lam_type] addSEs [apply_type]) 1); |
|
78 qed "AC1_AC4"; |
|
79 |
|
80 |
|
81 (* ********************************************************************** *) |
|
82 (* AC4 ==> AC3 *) |
|
83 (* ********************************************************************** *) |
|
84 |
|
85 Goal "f \\<in> A->B ==> (\\<Union>z \\<in> A. {z}*f`z) \\<subseteq> A*Union(B)"; |
|
86 by (fast_tac (claset() addSDs [apply_type]) 1); |
|
87 val lemma1 = result(); |
|
88 |
|
89 Goal "domain(\\<Union>z \\<in> A. {z}*f(z)) = {a \\<in> A. f(a)\\<noteq>0}"; |
|
90 by (Blast_tac 1); |
|
91 val lemma2 = result(); |
|
92 |
|
93 Goal "x \\<in> A ==> (\\<Union>z \\<in> A. {z}*f(z))``{x} = f(x)"; |
|
94 by (Fast_tac 1); |
|
95 val lemma3 = result(); |
|
96 |
|
97 Goalw AC_defs "AC4 ==> AC3"; |
|
98 by (REPEAT (resolve_tac [allI,ballI] 1)); |
|
99 by (REPEAT (eresolve_tac [allE,impE] 1)); |
|
100 by (etac lemma1 1); |
|
101 by (asm_full_simp_tac (simpset() addsimps [lemma2, lemma3] |
|
102 addcongs [Pi_cong]) 1); |
|
103 qed "AC4_AC3"; |
|
104 |
|
105 (* ********************************************************************** *) |
|
106 (* AC3 ==> AC1 *) |
|
107 (* ********************************************************************** *) |
|
108 |
|
109 Goal "b\\<notin>A ==> (\\<Pi>x \\<in> {a \\<in> A. id(A)`a\\<noteq>b}. id(A)`x) = (\\<Pi>x \\<in> A. x)"; |
|
110 by (asm_full_simp_tac (simpset() addsimps [id_def] addcongs [Pi_cong]) 1); |
|
111 by (res_inst_tac [("b","A")] subst_context 1); |
|
112 by (Fast_tac 1); |
|
113 val lemma = result(); |
|
114 |
|
115 Goalw AC_defs "AC3 ==> AC1"; |
|
116 by (fast_tac (claset() addSIs [id_type] addEs [lemma RS subst]) 1); |
|
117 qed "AC3_AC1"; |
|
118 |
|
119 (* ********************************************************************** *) |
|
120 (* AC4 ==> AC5 *) |
|
121 (* ********************************************************************** *) |
|
122 |
|
123 Goalw (range_def::AC_defs) "AC4 ==> AC5"; |
|
124 by (REPEAT (resolve_tac [allI,ballI] 1)); |
|
125 by (REPEAT (eresolve_tac [allE,impE] 1)); |
|
126 by (eresolve_tac [fun_is_rel RS converse_type] 1); |
|
127 by (etac exE 1); |
|
128 by (rtac bexI 1); |
|
129 by (rtac Pi_type 2 THEN (assume_tac 2)); |
|
130 by (fast_tac (claset() addSDs [apply_type] |
|
131 addSEs [fun_is_rel RS converse_type RS subsetD RS SigmaD2]) 2); |
|
132 by (rtac ballI 1); |
|
133 by (rtac apply_equality 1 THEN (assume_tac 2)); |
|
134 by (etac domainE 1); |
|
135 by (ftac range_type 1 THEN (assume_tac 1)); |
|
136 by (fast_tac (claset() addDs [apply_equality]) 1); |
|
137 qed "AC4_AC5"; |
|
138 |
|
139 |
|
140 (* ********************************************************************** *) |
|
141 (* AC5 ==> AC4, Rubin & Rubin, p. 11 *) |
|
142 (* ********************************************************************** *) |
|
143 |
|
144 Goal "R \\<subseteq> A*B ==> (\\<lambda>x \\<in> R. fst(x)) \\<in> R -> A"; |
|
145 by (fast_tac (claset() addSIs [lam_type, fst_type]) 1); |
|
146 val lemma1 = result(); |
|
147 |
|
148 Goalw [range_def] "R \\<subseteq> A*B ==> range(\\<lambda>x \\<in> R. fst(x)) = domain(R)"; |
|
149 by (force_tac (claset() addIs [lamI RS subst_elem] addSEs [lamE], |
|
150 simpset()) 1); |
|
151 val lemma2 = result(); |
|
152 |
|
153 Goal "[| \\<exists>f \\<in> A->C. P(f,domain(f)); A=B |] ==> \\<exists>f \\<in> B->C. P(f,B)"; |
|
154 by (etac bexE 1); |
|
155 by (ftac domain_of_fun 1); |
|
156 by (Fast_tac 1); |
|
157 val lemma3 = result(); |
|
158 |
|
159 Goal "[| R \\<subseteq> A*B; g \\<in> C->R; \\<forall>x \\<in> C. (\\<lambda>z \\<in> R. fst(z))` (g`x) = x |] \ |
|
160 \ ==> (\\<lambda>x \\<in> C. snd(g`x)): (\\<Pi>x \\<in> C. R``{x})"; |
|
161 by (rtac lam_type 1); |
|
162 by (force_tac (claset() addDs [apply_type], simpset()) 1); |
|
163 val lemma4 = result(); |
|
164 |
|
165 Goalw AC_defs "AC5 ==> AC4"; |
|
166 by (Clarify_tac 1); |
|
167 by (REPEAT (eresolve_tac [allE,ballE] 1)); |
|
168 by (eresolve_tac [lemma1 RSN (2, notE)] 2 THEN (assume_tac 2)); |
|
169 by (dresolve_tac [lemma2 RSN (2, lemma3)] 1 THEN (assume_tac 1)); |
|
170 by (fast_tac (claset() addSEs [lemma4]) 1); |
|
171 qed "AC5_AC4"; |
|
172 |
|
173 |
|
174 (* ********************************************************************** *) |
|
175 (* AC1 <-> AC6 *) |
|
176 (* ********************************************************************** *) |
|
177 |
|
178 Goalw AC_defs "AC1 <-> AC6"; |
|
179 by (Blast_tac 1); |
|
180 qed "AC1_iff_AC6"; |
|