src/HOL/Hilbert_Choice_lemmas.ML
 author paulson Thu Sep 26 10:51:29 2002 +0200 (2002-09-26) changeset 13585 db4005b40cc6 parent 12459 6978ab7cac64 permissions -rw-r--r--
Converted Fun to Isar style.
Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy.
Renamed constant "Fun.op o" to "Fun.comp"
1 (*  Title:      HOL/Hilbert_Choice_lemmas
2     ID: \$Id\$
3     Author:     Lawrence C Paulson
4     Copyright   2001  University of Cambridge
6 Lemmas for Hilbert's epsilon-operator and the Axiom of Choice
7 *)
10 (* ML bindings *)
11 val someI = thm "someI";
13 section "SOME: Hilbert's Epsilon-operator";
15 (*Easier to apply than someI if witness ?a comes from an EX-formula*)
16 Goal "EX x. P x ==> P (SOME x. P x)";
17 by (etac exE 1);
18 by (etac someI 1);
19 qed "someI_ex";
21 (*Easier to apply than someI: conclusion has only one occurrence of P*)
22 val prems = Goal "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
23 by (resolve_tac prems 1);
24 by (rtac someI 1);
25 by (resolve_tac prems 1) ;
26 qed "someI2";
28 (*Easier to apply than someI2 if witness ?a comes from an EX-formula*)
29 val [major,minor] = Goal "[| EX a. P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)";
30 by (rtac (major RS exE) 1);
31 by (etac someI2 1 THEN etac minor 1);
32 qed "someI2_ex";
34 val prems = Goal "[| P a;  !!x. P x ==> x=a |] ==> (SOME x. P x) = a";
35 by (rtac someI2 1);
36 by (REPEAT (ares_tac prems 1)) ;
37 qed "some_equality";
40 Goal "[| EX!x. P x; P a |] ==> (SOME x. P x) = a";
41 by (rtac some_equality 1);
42 by  (atac 1);
43 by (etac ex1E 1);
44 by (etac all_dupE 1);
45 by (dtac mp 1);
46 by  (atac 1);
47 by (etac ssubst 1);
48 by (etac allE 1);
49 by (etac mp 1);
50 by (atac 1);
51 qed "some1_equality";
53 Goal "P (SOME x. P x) =  (EX x. P x)";
54 by (rtac iffI 1);
55 by (etac exI 1);
56 by (etac exE 1);
57 by (etac someI 1);
58 qed "some_eq_ex";
60 Goal "(SOME y. y=x) = x";
61 by (rtac some_equality 1);
62 by (rtac refl 1);
63 by (atac 1);
64 qed "some_eq_trivial";
66 Goal "(SOME y. x=y) = x";
67 by (rtac some_equality 1);
68 by (rtac refl 1);
69 by (etac sym 1);
70 qed "some_sym_eq_trivial";
71 Addsimps [some_eq_trivial, some_sym_eq_trivial];
74 (** "Axiom" of Choice, proved using the description operator **)
76 (*Used in Tools/meson.ML*)
77 Goal "ALL x. EX y. Q x y ==> EX f. ALL x. Q x (f x)";
78 by (fast_tac (claset() addEs [someI]) 1);
79 qed "choice";
81 Goal "ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
82 by (fast_tac (claset() addEs [someI]) 1);
83 qed "bchoice";
86 section "Function Inverse";
88 val inv_def = thm "inv_def";
89 val Inv_def = thm "Inv_def";
91 Goal "inv id = id";
92 by (simp_tac (simpset() addsimps [inv_def,id_def]) 1);
93 qed "inv_id";
96 (*A one-to-one function has an inverse.*)
97 Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
98 by (asm_simp_tac (simpset() addsimps [inj_eq]) 1);
99 qed "inv_f_f";
102 Goal "[| inj(f);  f x = y |] ==> inv f y = x";
103 by (etac subst 1);
104 by (etac inv_f_f 1);
105 qed "inv_f_eq";
107 Goal "[| inj f; ALL x. f(g x) = x |] ==> inv f = g";
108 by (blast_tac (claset() addIs [ext, inv_f_eq]) 1);
109 qed "inj_imp_inv_eq";
111 (* Useful??? *)
112 val [oneone,minor] = Goal
113     "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
114 by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
115 by (rtac (rangeI RS minor) 1);
116 qed "inj_transfer";
118 Goal "(inj f) = (inv f o f = id)";
119 by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
120 by (blast_tac (claset() addIs [inj_inverseI, inv_f_f]) 1);
121 qed "inj_iff";
123 Goal "inj f ==> surj (inv f)";
124 by (blast_tac (claset() addIs [surjI, inv_f_f]) 1);
125 qed "inj_imp_surj_inv";
127 Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
128 by (fast_tac (claset() addIs [someI]) 1);
129 qed "f_inv_f";
131 Goal "surj f ==> f(inv f y) = y";
132 by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1);
133 qed "surj_f_inv_f";
135 Goal "[| inv f x = inv f y;  x: range(f);  y: range(f) |] ==> x=y";
136 by (rtac (arg_cong RS box_equals) 1);
137 by (REPEAT (ares_tac [f_inv_f] 1));
138 qed "inv_injective";
140 Goal "A <= range(f) ==> inj_on (inv f) A";
141 by (fast_tac (claset() addIs [inj_onI]
142                        addEs [inv_injective, injD]) 1);
143 qed "inj_on_inv";
145 Goal "surj f ==> inj (inv f)";
146 by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1);
147 qed "surj_imp_inj_inv";
149 Goal "(surj f) = (f o inv f = id)";
150 by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
151 by (blast_tac (claset() addIs [surjI, surj_f_inv_f]) 1);
152 qed "surj_iff";
154 Goal "[| surj f; ALL x. g(f x) = x |] ==> inv f = g";
155 by (rtac ext 1);
156 by (dres_inst_tac [("x","inv f x")] spec 1);
157 by (asm_full_simp_tac (simpset() addsimps [surj_f_inv_f]) 1);
158 qed "surj_imp_inv_eq";
160 Goalw [bij_def] "bij f ==> bij (inv f)";
161 by (asm_simp_tac (simpset() addsimps [inj_imp_surj_inv, surj_imp_inj_inv]) 1);
162 qed "bij_imp_bij_inv";
164 val prems =
165 Goalw [inv_def] "[| !! x. g (f x) = x;  !! y. f (g y) = y |] ==> inv f = g";
166 by (rtac ext 1);
167 by (auto_tac (claset(), simpset() addsimps prems));
168 qed "inv_equality";
170 Goalw [bij_def] "bij f ==> inv (inv f) = f";
171 by (rtac inv_equality 1);
172 by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
173 qed "inv_inv_eq";
175 (** bij(inv f) implies little about f.  Consider f::bool=>bool such that
176     f(True)=f(False)=True.  Then it's consistent with axiom someI that
177     inv(f) could be any function at all, including the identity function.
178     If inv(f)=id then inv(f) is a bijection, but inj(f), surj(f) and
179     inv(inv(f))=f all fail.
180 **)
182 Goalw [bij_def] "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f";
183 by (rtac (inv_equality) 1);
184 by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
185 qed "o_inv_distrib";
188 Goal "surj f ==> f ` (inv f ` A) = A";
189 by (asm_simp_tac (simpset() addsimps [image_eq_UN, surj_f_inv_f]) 1);
190 qed "image_surj_f_inv_f";
192 Goal "inj f ==> (inv f) ` (f ` A) = A";
193 by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 1);
194 qed "image_inv_f_f";
196 Goalw [image_def] "inj(f) ==> inv(f)`(f`X) = X";
197 by Auto_tac;
198 qed "inv_image_comp";
200 Goal "bij f ==> f ` Collect P = {y. P (inv f y)}";
201 by Auto_tac;
202 by (force_tac (claset(), simpset() addsimps [bij_is_inj]) 1);
203 by (blast_tac (claset() addIs [bij_is_surj RS surj_f_inv_f RS sym]) 1);
204 qed "bij_image_Collect_eq";
206 Goal "bij f ==> f -` A = inv f ` A";
207 by Safe_tac;
208 by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2);
209 by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
210 qed "bij_vimage_eq_inv_image";
213 section "Inverse of a PI-function (restricted domain)";
215 Goal "[| inj_on f A;  x : A |] ==> Inv A f (f x) = x";
216 by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
217 by (blast_tac (claset() addIs [someI2]) 1);
218 qed "Inv_f_f";
220 Goal "y : f`A  ==> f (Inv A f y) = y";
221 by (asm_simp_tac (simpset() addsimps [Inv_def]) 1);
222 by (fast_tac (claset() addIs [someI2]) 1);
223 qed "f_Inv_f";
225 Goal "[| Inv A f x = Inv A f y;  x : f`A;  y : f`A |] ==> x=y";
226 by (rtac (arg_cong RS box_equals) 1);
227 by (REPEAT (ares_tac [f_Inv_f] 1));
228 qed "Inv_injective";
230 Goal "B <= f`A ==> inj_on (Inv A f) B";
231 by (rtac inj_onI 1);
232 by (blast_tac (claset() addIs [inj_onI] addDs [Inv_injective, injD]) 1);
233 qed "inj_on_Inv";
237 section "split and SOME";
239 (*Can't be added to simpset: loops!*)
240 Goal "(SOME x. P x) = (SOME (a,b). P(a,b))";
241 by (simp_tac (simpset() addsimps [split_Pair_apply]) 1);
242 qed "split_paired_Eps";
244 Goalw [split_def] "Eps (split P) = (SOME xy. P (fst xy) (snd xy))";
245 by (rtac refl 1);
246 qed "Eps_split";
248 Goal "(@(x',y'). x = x' & y = y') = (x,y)";
249 by (Blast_tac 1);
250 qed "Eps_split_eq";
254 section "A relation is wellfounded iff it has no infinite descending chain";
256 Goalw [wf_eq_minimal RS eq_reflection]
257   "wf r = (~(EX f. ALL i. (f(Suc i),f i) : r))";
258 by (rtac iffI 1);
259  by (rtac notI 1);
260  by (etac exE 1);
261  by (eres_inst_tac [("x","{w. EX i. w=f i}")] allE 1);
262  by (Blast_tac 1);
263 by (etac contrapos_np 1);
264 by (Asm_full_simp_tac 1);
265 by (Clarify_tac 1);
266 by (subgoal_tac "ALL n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
267  by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
268  by (rtac allI 1);
269  by (Simp_tac 1);
270  by (rtac someI2_ex 1);
271   by (Blast_tac 1);
272  by (Blast_tac 1);
273 by (rtac allI 1);
274 by (induct_tac "n" 1);
275  by (Asm_simp_tac 1);
276 by (Simp_tac 1);
277 by (rtac someI2_ex 1);
278  by (Blast_tac 1);
279 by (Blast_tac 1);
280 qed "wf_iff_no_infinite_down_chain";