--- a/src/HOL/Fun.ML Tue Jul 24 11:25:54 2001 +0200
+++ b/src/HOL/Fun.ML Wed Jul 25 13:13:01 2001 +0200
@@ -19,15 +19,6 @@
qed "apply_inverse";
-(** "Axiom" of Choice, proved using the description operator **)
-
-(*"choice" is now proved in Tools/meson.ML*)
-
-Goal "!!S. ALL x:S. EX y. Q x y ==> EX f. ALL x:S. Q x (f x)";
-by (fast_tac (claset() addEs [someI]) 1);
-qed "bchoice";
-
-
section "id";
Goalw [id_def] "id x = x";
@@ -35,11 +26,6 @@
qed "id_apply";
Addsimps [id_apply];
-Goal "inv id = id";
-by (simp_tac (simpset() addsimps [inv_def,id_def]) 1);
-qed "inv_id";
-Addsimps [inv_id];
-
section "o";
@@ -113,28 +99,6 @@
by (assume_tac 1);
qed "inj_eq";
-(*A one-to-one function has an inverse (given using select).*)
-Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
-by (asm_simp_tac (simpset() addsimps [inj_eq]) 1);
-qed "inv_f_f";
-Addsimps [inv_f_f];
-
-Goal "[| inj(f); f x = y |] ==> inv f y = x";
-by (etac subst 1);
-by (etac inv_f_f 1);
-qed "inv_f_eq";
-
-Goal "[| inj f; ALL x. f(g x) = x |] ==> inv f = g";
-by (blast_tac (claset() addIs [ext, inv_f_eq]) 1);
-qed "inj_imp_inv_eq";
-
-(* Useful??? *)
-val [oneone,minor] = Goal
- "[| inj(f); !!y. y: range(f) ==> P(inv f y) |] ==> P(x)";
-by (res_inst_tac [("t", "x")] (oneone RS (inv_f_f RS subst)) 1);
-by (rtac (rangeI RS minor) 1);
-qed "inj_transfer";
-
Goalw [o_def] "[| inj f; f o g = f o h |] ==> g = h";
by (rtac ext 1);
by (etac injD 1);
@@ -157,11 +121,6 @@
qed "inj_on_inverseI";
bind_thm ("inj_inverseI", inj_on_inverseI); (*for compatibility*)
-Goal "(inj f) = (inv f o f = id)";
-by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
-by (blast_tac (claset() addIs [inj_inverseI, inv_f_f]) 1);
-qed "inj_iff";
-
Goalw [inj_on_def] "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y";
by (Blast_tac 1);
qed "inj_onD";
@@ -170,6 +129,10 @@
by (blast_tac (claset() addSDs [inj_onD]) 1);
qed "inj_on_iff";
+Goalw [o_def] "[| inj_on f A; inj_on g (f`A) |] ==> inj_on (g o f) A";
+by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
+qed "comp_inj_on";
+
Goalw [inj_on_def] "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)";
by (Blast_tac 1);
qed "inj_on_contraD";
@@ -198,49 +161,6 @@
by (Blast_tac 1);
qed "surjD";
-Goal "inj f ==> surj (inv f)";
-by (blast_tac (claset() addIs [surjI, inv_f_f]) 1);
-qed "inj_imp_surj_inv";
-
-
-(*** Lemmas about injective functions and inv ***)
-
-Goalw [o_def] "[| inj_on f A; inj_on g (f`A) |] ==> inj_on (g o f) A";
-by (fast_tac (claset() addIs [inj_onI] addEs [inj_onD]) 1);
-qed "comp_inj_on";
-
-Goalw [inv_def] "y : range(f) ==> f(inv f y) = y";
-by (fast_tac (claset() addIs [someI]) 1);
-qed "f_inv_f";
-
-Goal "surj f ==> f(inv f y) = y";
-by (asm_simp_tac (simpset() addsimps [f_inv_f, surj_range]) 1);
-qed "surj_f_inv_f";
-
-Goal "[| inv f x = inv f y; x: range(f); y: range(f) |] ==> x=y";
-by (rtac (arg_cong RS box_equals) 1);
-by (REPEAT (ares_tac [f_inv_f] 1));
-qed "inv_injective";
-
-Goal "A <= range(f) ==> inj_on (inv f) A";
-by (fast_tac (claset() addIs [inj_onI]
- addEs [inv_injective, injD]) 1);
-qed "inj_on_inv";
-
-Goal "surj f ==> inj (inv f)";
-by (asm_simp_tac (simpset() addsimps [inj_on_inv, surj_range]) 1);
-qed "surj_imp_inj_inv";
-
-Goal "(surj f) = (f o inv f = id)";
-by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
-by (blast_tac (claset() addIs [surjI, surj_f_inv_f]) 1);
-qed "surj_iff";
-
-Goal "[| surj f; ALL x. g(f x) = x |] ==> inv f = g";
-by (rtac ext 1);
-by (dres_inst_tac [("x","inv f x")] spec 1);
-by (asm_full_simp_tac (simpset() addsimps [surj_f_inv_f]) 1);
-qed "surj_imp_inv_eq";
(** Bijections **)
@@ -257,33 +177,6 @@
by (Blast_tac 1);
qed "bij_is_surj";
-Goalw [bij_def] "bij f ==> bij (inv f)";
-by (asm_simp_tac (simpset() addsimps [inj_imp_surj_inv, surj_imp_inj_inv]) 1);
-qed "bij_imp_bij_inv";
-
-val prems =
-Goalw [inv_def] "[| !! x. g (f x) = x; !! y. f (g y) = y |] ==> inv f = g";
-by (rtac ext 1);
-by (auto_tac (claset(), simpset() addsimps prems));
-qed "inv_equality";
-
-Goalw [bij_def] "bij f ==> inv (inv f) = f";
-by (rtac inv_equality 1);
-by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
-qed "inv_inv_eq";
-
-(** bij(inv f) implies little about f. Consider f::bool=>bool such that
- f(True)=f(False)=True. Then it's consistent with axiom someI that
- inv(f) could be any function at all, including the identity function.
- If inv(f)=id then inv(f) is a bijection, but inj(f), surj(f) and
- inv(inv(f))=f all fail.
-**)
-
-Goalw [bij_def] "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f";
-by (rtac (inv_equality) 1);
-by (auto_tac (claset(), simpset() addsimps [surj_f_inv_f]));
-qed "o_inv_distrib";
-
(** We seem to need both the id-forms and the (%x. x) forms; the latter can
arise by rewriting, while id may be used explicitly. **)
@@ -323,18 +216,10 @@
by (asm_simp_tac (simpset() addsimps [surj_range]) 1);
qed "surj_image_vimage_eq";
-Goal "surj f ==> f ` (inv f ` A) = A";
-by (asm_simp_tac (simpset() addsimps [image_eq_UN, surj_f_inv_f]) 1);
-qed "image_surj_f_inv_f";
-
Goalw [inj_on_def] "inj f ==> f -` (f ` A) = A";
by (Blast_tac 1);
qed "inj_vimage_image_eq";
-Goal "inj f ==> (inv f) ` (f ` A) = A";
-by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 1);
-qed "image_inv_f_f";
-
Goalw [surj_def] "surj f ==> f -` B <= A ==> B <= f ` A";
by (blast_tac (claset() addIs [sym]) 1);
qed "vimage_subsetD";
@@ -374,10 +259,6 @@
by (Blast_tac 1);
qed "image_set_diff";
-Goalw [image_def] "inj(f) ==> inv(f)`(f`X) = X";
-by Auto_tac;
-qed "inv_image_comp";
-
Goal "inj f ==> (f a : f`A) = (a : A)";
by (blast_tac (claset() addDs [injD]) 1);
qed "inj_image_mem_iff";
@@ -404,22 +285,10 @@
(*Compare with image_INT: no use of inj_on, and if f is surjective then
it doesn't matter whether A is empty*)
Goalw [bij_def] "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)";
-by (force_tac (claset() addSIs [surj_f_inv_f RS sym RS image_eqI],
- simpset()) 1);
+by (asm_full_simp_tac (simpset() addsimps [inj_on_def, surj_def]) 1);
+by (Blast_tac 1);
qed "bij_image_INT";
-Goal "bij f ==> f ` Collect P = {y. P (inv f y)}";
-by Auto_tac;
-by (force_tac (claset(), simpset() addsimps [bij_is_inj]) 1);
-by (blast_tac (claset() addIs [bij_is_surj RS surj_f_inv_f RS sym]) 1);
-qed "bij_image_Collect_eq";
-
-Goal "bij f ==> f -` A = inv f ` A";
-by Safe_tac;
-by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 2);
-by (blast_tac (claset() addIs [bij_is_inj RS inv_f_f RS sym]) 1);
-qed "bij_vimage_eq_inv_image";
-
Goal "surj f ==> -(f`A) <= f`(-A)";
by (auto_tac (claset(), simpset() addsimps [surj_def]));
qed "surj_Compl_image_subset";
@@ -504,13 +373,13 @@
(*** -> and Pi, by Florian Kammueller and LCP ***)
val prems = Goalw [Pi_def]
-"[| !!x. x: A ==> f x: B x; !!x. x ~: A ==> f(x) = (@ y. True)|] \
+"[| !!x. x: A ==> f x: B x; !!x. x ~: A ==> f(x) = arbitrary|] \
\ ==> f: Pi A B";
by (auto_tac (claset(), simpset() addsimps prems));
qed "Pi_I";
val prems = Goal
-"[| !!x. x: A ==> f x: B; !!x. x ~: A ==> f(x) = (@ y. True)|] ==> f: A funcset B";
+"[| !!x. x: A ==> f x: B; !!x. x ~: A ==> f(x) = arbitrary|] ==> f: A funcset B";
by (blast_tac (claset() addIs Pi_I::prems) 1);
qed "funcsetI";
@@ -522,7 +391,7 @@
by Auto_tac;
qed "funcset_mem";
-Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = (@ y. True)";
+Goalw [Pi_def] "[|f: Pi A B; x~: A|] ==> f x = arbitrary";
by Auto_tac;
qed "apply_arb";
@@ -573,7 +442,7 @@
by (asm_simp_tac (simpset() addsimps prems) 1);
qed "restrictI";
-Goal "(lam y: A. f y) x = (if x : A then f x else (@ y. True))";
+Goal "(lam y: A. f y) x = (if x : A then f x else arbitrary)";
by (asm_simp_tac (simpset() addsimps [restrict_def]) 1);
qed "restrict_apply";
Addsimps [restrict_apply];
@@ -590,32 +459,6 @@
qed "inj_on_restrict_eq";
-(*** Inverse ***)
-
-Goalw [Inv_def] "f ` A = B ==> (lam x: B. (Inv A f) x) : B funcset A";
-by (fast_tac (claset() addIs [restrict_in_funcset, someI2]) 1);
-qed "Inv_funcset";
-
-Goal "[| inj_on f A; x : A |] ==> Inv A f (f x) = x";
-by (asm_full_simp_tac (simpset() addsimps [Inv_def, inj_on_def]) 1);
-by (blast_tac (claset() addIs [someI2]) 1);
-qed "Inv_f_f";
-
-Goal "y : f`A ==> f (Inv A f y) = y";
-by (asm_simp_tac (simpset() addsimps [Inv_def]) 1);
-by (fast_tac (claset() addIs [someI2]) 1);
-qed "f_Inv_f";
-
-Goal "[| Inv A f x = Inv A f y; x : f`A; y : f`A |] ==> x=y";
-by (rtac (arg_cong RS box_equals) 1);
-by (REPEAT (ares_tac [f_Inv_f] 1));
-qed "Inv_injective";
-
-Goal "B <= f`A ==> inj_on (Inv A f) B";
-by (rtac inj_onI 1);
-by (blast_tac (claset() addIs [inj_onI] addDs [Inv_injective, injD]) 1);
-qed "inj_on_Inv";
-
Goal "f : A funcset B ==> compose A (lam y:B. y) f = f";
by (rtac ext 1);
by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def]));
@@ -626,15 +469,6 @@
by (auto_tac (claset(), simpset() addsimps [compose_def, Pi_def]));
qed "compose_Id";
-Goal "[| inj_on f A; f ` A = B |] \
-\ ==> compose A (lam y:B. (Inv A f) y) f = (lam x: A. x)";
-by (asm_simp_tac (simpset() addsimps [compose_def]) 1);
-by (rtac restrict_ext 1);
-by Auto_tac;
-by (etac subst 1);
-by (asm_full_simp_tac (simpset() addsimps [Inv_f_f]) 1);
-qed "compose_Inv_id";
-
(*** Pi ***)
@@ -646,7 +480,7 @@
by (blast_tac (HOL_cs addIs [Pi_eq_empty]) 1);
qed "Pi_total1";
-Goal "Pi {} B = { %x. @y. True }";
+Goal "Pi {} B = { %x. arbitrary }";
by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
qed "Pi_empty";