diff -r 791a4655cae3 -r 764547b68538 src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Wed Oct 21 17:34:35 2009 +0200 +++ b/src/HOL/Hilbert_Choice.thy Thu Oct 22 09:27:48 2009 +0200 @@ -31,11 +31,11 @@ in Syntax.const "_Eps" $ x $ t end)] *} -definition inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where -"inv_onto A f == %x. SOME y. y : A & f y = x" +definition inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where +"inv_into A f == %x. SOME y. y : A & f y = x" abbreviation inv :: "('a => 'b) => ('b => 'a)" where -"inv == inv_onto UNIV" +"inv == inv_into UNIV" subsection {*Hilbert's Epsilon-operator*} @@ -92,40 +92,40 @@ subsection {*Function Inverse*} lemma inv_def: "inv f = (%y. SOME x. f x = y)" -by(simp add: inv_onto_def) +by(simp add: inv_into_def) -lemma inv_onto_into: "x : f ` A ==> inv_onto A f x : A" -apply (simp add: inv_onto_def) +lemma inv_into_into: "x : f ` A ==> inv_into A f x : A" +apply (simp add: inv_into_def) apply (fast intro: someI2) done lemma inv_id [simp]: "inv id = id" -by (simp add: inv_onto_def id_def) +by (simp add: inv_into_def id_def) -lemma inv_onto_f_f [simp]: - "[| inj_on f A; x : A |] ==> inv_onto A f (f x) = x" -apply (simp add: inv_onto_def inj_on_def) +lemma inv_into_f_f [simp]: + "[| inj_on f A; x : A |] ==> inv_into A f (f x) = x" +apply (simp add: inv_into_def inj_on_def) apply (blast intro: someI2) done lemma inv_f_f: "inj f ==> inv f (f x) = x" -by (simp add: inv_onto_f_f) +by (simp add: inv_into_f_f) -lemma f_inv_onto_f: "y : f`A ==> f (inv_onto A f y) = y" -apply (simp add: inv_onto_def) +lemma f_inv_into_f: "y : f`A ==> f (inv_into A f y) = y" +apply (simp add: inv_into_def) apply (fast intro: someI2) done -lemma inv_onto_f_eq: "[| inj_on f A; x : A; f x = y |] ==> inv_onto A f y = x" +lemma inv_into_f_eq: "[| inj_on f A; x : A; f x = y |] ==> inv_into A f y = x" apply (erule subst) -apply (fast intro: inv_onto_f_f) +apply (fast intro: inv_into_f_f) done lemma inv_f_eq: "[| inj f; f x = y |] ==> inv f y = x" -by (simp add:inv_onto_f_eq) +by (simp add:inv_into_f_eq) lemma inj_imp_inv_eq: "[| inj f; ALL x. f(g x) = x |] ==> inv f = g" -by (blast intro: ext inv_onto_f_eq) +by (blast intro: ext inv_into_f_eq) text{*But is it useful?*} lemma inj_transfer: @@ -134,12 +134,12 @@ proof - have "f x \ range f" by auto hence "P(inv f (f x))" by (rule minor) - thus "P x" by (simp add: inv_onto_f_f [OF injf]) + thus "P x" by (simp add: inv_into_f_f [OF injf]) qed lemma inj_iff: "(inj f) = (inv f o f = id)" apply (simp add: o_def expand_fun_eq) -apply (blast intro: inj_on_inverseI inv_onto_f_f) +apply (blast intro: inj_on_inverseI inv_into_f_f) done lemma inv_o_cancel[simp]: "inj f ==> inv f o f = id" @@ -148,34 +148,34 @@ lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g" by (simp add: o_assoc[symmetric]) -lemma inv_onto_image_cancel[simp]: - "inj_on f A ==> S <= A ==> inv_onto A f ` f ` S = S" +lemma inv_into_image_cancel[simp]: + "inj_on f A ==> S <= A ==> inv_into A f ` f ` S = S" by(fastsimp simp: image_def) lemma inj_imp_surj_inv: "inj f ==> surj (inv f)" -by (blast intro: surjI inv_onto_f_f) +by (blast intro: surjI inv_into_f_f) lemma surj_f_inv_f: "surj f ==> f(inv f y) = y" -by (simp add: f_inv_onto_f surj_range) +by (simp add: f_inv_into_f surj_range) -lemma inv_onto_injective: - assumes eq: "inv_onto A f x = inv_onto A f y" +lemma inv_into_injective: + assumes eq: "inv_into A f x = inv_into A f y" and x: "x: f`A" and y: "y: f`A" shows "x=y" proof - - have "f (inv_onto A f x) = f (inv_onto A f y)" using eq by simp - thus ?thesis by (simp add: f_inv_onto_f x y) + have "f (inv_into A f x) = f (inv_into A f y)" using eq by simp + thus ?thesis by (simp add: f_inv_into_f x y) qed -lemma inj_on_inv_onto: "B <= f`A ==> inj_on (inv_onto A f) B" -by (blast intro: inj_onI dest: inv_onto_injective injD) +lemma inj_on_inv_into: "B <= f`A ==> inj_on (inv_into A f) B" +by (blast intro: inj_onI dest: inv_into_injective injD) -lemma bij_betw_inv_onto: "bij_betw f A B ==> bij_betw (inv_onto A f) B A" -by (auto simp add: bij_betw_def inj_on_inv_onto) +lemma bij_betw_inv_into: "bij_betw f A B ==> bij_betw (inv_into A f) B A" +by (auto simp add: bij_betw_def inj_on_inv_into) lemma surj_imp_inj_inv: "surj f ==> inj (inv f)" -by (simp add: inj_on_inv_onto surj_range) +by (simp add: inj_on_inv_into surj_range) lemma surj_iff: "(surj f) = (f o inv f = id)" apply (simp add: o_def expand_fun_eq) @@ -193,7 +193,7 @@ lemma inv_equality: "[| !!x. g (f x) = x; !!y. f (g y) = y |] ==> inv f = g" apply (rule ext) -apply (auto simp add: inv_onto_def) +apply (auto simp add: inv_into_def) done lemma inv_inv_eq: "bij f ==> inv (inv f) = f" @@ -208,13 +208,13 @@ inv(inv f)=f all fail. **) -lemma inv_onto_comp: +lemma inv_into_comp: "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==> - inv_onto A (f o g) x = (inv_onto A g o inv_onto (g ` A) f) x" -apply (rule inv_onto_f_eq) + inv_into A (f o g) x = (inv_into A g o inv_into (g ` A) f) x" +apply (rule inv_into_f_eq) apply (fast intro: comp_inj_on) - apply (simp add: inv_onto_into) -apply (simp add: f_inv_onto_f inv_onto_into) + apply (simp add: inv_into_into) +apply (simp add: f_inv_into_f inv_into_into) done lemma o_inv_distrib: "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f" @@ -239,7 +239,7 @@ lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A" apply (auto simp add: bij_is_surj [THEN surj_f_inv_f]) -apply (blast intro: bij_is_inj [THEN inv_onto_f_f, symmetric]) +apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric]) done lemma finite_fun_UNIVD1: @@ -256,7 +256,7 @@ moreover have "UNIV = range (\f :: 'a \ 'b. inv f b1)" proof (rule UNIV_eq_I) fix x :: 'a - from b1b2 have "x = inv (\y. if y = x then b1 else b2) b1" by (simp add: inv_onto_def) + from b1b2 have "x = inv (\y. if y = x then b1 else b2) b1" by (simp add: inv_into_def) thus "x \ range (\f\'a \ 'b. inv f b1)" by blast qed ultimately show "finite (UNIV :: 'a set)" by simp