src/HOL/Hilbert_Choice.thy
 changeset 32988 d1d4d7a08a66 parent 31723 f5cafe803b55 child 33014 85d7a096e63f
```     1.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Oct 17 13:46:55 2009 +0200
1.2 +++ b/src/HOL/Hilbert_Choice.thy	Sun Oct 18 12:07:25 2009 +0200
1.3 @@ -1,5 +1,5 @@
1.4  (*  Title:      HOL/Hilbert_Choice.thy
1.5 -    Author:     Lawrence C Paulson
1.6 +    Author:     Lawrence C Paulson, Tobias Nipkow
1.7      Copyright   2001  University of Cambridge
1.8  *)
1.9
1.10 @@ -31,12 +31,11 @@
1.11       in Syntax.const "_Eps" \$ x \$ t end)]
1.12  *}
1.13
1.14 -constdefs
1.15 -  inv :: "('a => 'b) => ('b => 'a)"
1.16 -  "inv(f :: 'a => 'b) == %y. SOME x. f x = y"
1.17 +definition inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where
1.18 +"inv_onto A f == %x. SOME y. y : A & f y = x"
1.19
1.20 -  Inv :: "'a set => ('a => 'b) => ('b => 'a)"
1.21 -  "Inv A f == %x. SOME y. y \<in> A & f y = x"
1.22 +abbreviation inv :: "('a => 'b) => ('b => 'a)" where
1.23 +"inv == inv_onto UNIV"
1.24
1.25
1.26  subsection {*Hilbert's Epsilon-operator*}
1.27 @@ -92,20 +91,38 @@
1.28
1.29  subsection {*Function Inverse*}
1.30
1.31 -lemma inv_id [simp]: "inv id = id"
1.32 -by (simp add: inv_def id_def)
1.33 +lemma inv_onto_into: "x : f ` A ==> inv_onto A f x : A"
1.35 +apply (fast intro: someI2)
1.36 +done
1.37
1.38 -text{*A one-to-one function has an inverse.*}
1.39 -lemma inv_f_f [simp]: "inj f ==> inv f (f x) = x"
1.40 -by (simp add: inv_def inj_eq)
1.41 +lemma inv_id [simp]: "inv id = id"
1.42 +by (simp add: inv_onto_def id_def)
1.43
1.44 -lemma inv_f_eq: "[| inj f;  f x = y |] ==> inv f y = x"
1.45 -apply (erule subst)
1.46 -apply (erule inv_f_f)
1.47 +lemma inv_onto_f_f [simp]:
1.48 +  "[| inj_on f A;  x : A |] ==> inv_onto A f (f x) = x"
1.49 +apply (simp add: inv_onto_def inj_on_def)
1.50 +apply (blast intro: someI2)
1.51  done
1.52
1.53 -lemma inj_imp_inv_eq: "[| inj f; \<forall>x. f(g x) = x |] ==> inv f = g"
1.54 -by (blast intro: ext inv_f_eq)
1.55 +lemma inv_f_f: "inj f ==> inv f (f x) = x"
1.57 +
1.58 +lemma f_inv_onto_f: "y : f`A  ==> f (inv_onto A f y) = y"
1.60 +apply (fast intro: someI2)
1.61 +done
1.62 +
1.63 +lemma inv_onto_f_eq: "[| inj_on f A; x : A; f x = y |] ==> inv_onto A f y = x"
1.64 +apply (erule subst)
1.65 +apply (fast intro: inv_onto_f_f)
1.66 +done
1.67 +
1.68 +lemma inv_f_eq: "[| inj f; f x = y |] ==> inv f y = x"
1.70 +
1.71 +lemma inj_imp_inv_eq: "[| inj f; ALL x. f(g x) = x |] ==> inv f = g"
1.72 +by (blast intro: ext inv_onto_f_eq)
1.73
1.74  text{*But is it useful?*}
1.75  lemma inj_transfer:
1.76 @@ -114,13 +131,12 @@
1.77  proof -
1.78    have "f x \<in> range f" by auto
1.79    hence "P(inv f (f x))" by (rule minor)
1.80 -  thus "P x" by (simp add: inv_f_f [OF injf])
1.81 +  thus "P x" by (simp add: inv_onto_f_f [OF injf])
1.82  qed
1.83
1.84 -
1.85  lemma inj_iff: "(inj f) = (inv f o f = id)"
1.86  apply (simp add: o_def expand_fun_eq)
1.87 -apply (blast intro: inj_on_inverseI inv_f_f)
1.88 +apply (blast intro: inj_on_inverseI inv_onto_f_f)
1.89  done
1.90
1.91  lemma inv_o_cancel[simp]: "inj f ==> inv f o f = id"
1.92 @@ -129,36 +145,34 @@
1.93  lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
1.95
1.96 -lemma inv_image_cancel[simp]:
1.97 -  "inj f ==> inv f ` f ` S = S"
1.99 -
1.100 +lemma inv_onto_image_cancel[simp]:
1.101 +  "inj_on f A ==> S <= A ==> inv_onto A f ` f ` S = S"
1.102 +by(fastsimp simp: image_def)
1.103 +
1.104  lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
1.105 -by (blast intro: surjI inv_f_f)
1.106 -
1.107 -lemma f_inv_f: "y \<in> range(f) ==> f(inv f y) = y"
1.109 -apply (fast intro: someI)
1.110 -done
1.111 +by (blast intro: surjI inv_onto_f_f)
1.112
1.113  lemma surj_f_inv_f: "surj f ==> f(inv f y) = y"
1.114 -by (simp add: f_inv_f surj_range)
1.115 +by (simp add: f_inv_onto_f surj_range)
1.116
1.117 -lemma inv_injective:
1.118 -  assumes eq: "inv f x = inv f y"
1.119 -      and x: "x: range f"
1.120 -      and y: "y: range f"
1.121 +lemma inv_onto_injective:
1.122 +  assumes eq: "inv_onto A f x = inv_onto A f y"
1.123 +      and x: "x: f`A"
1.124 +      and y: "y: f`A"
1.125    shows "x=y"
1.126  proof -
1.127 -  have "f (inv f x) = f (inv f y)" using eq by simp
1.128 -  thus ?thesis by (simp add: f_inv_f x y)
1.129 +  have "f (inv_onto A f x) = f (inv_onto A f y)" using eq by simp
1.130 +  thus ?thesis by (simp add: f_inv_onto_f x y)
1.131  qed
1.132
1.133 -lemma inj_on_inv: "A <= range(f) ==> inj_on (inv f) A"
1.134 -by (fast intro: inj_onI elim: inv_injective injD)
1.135 +lemma inj_on_inv_onto: "B <= f`A ==> inj_on (inv_onto A f) B"
1.136 +by (blast intro: inj_onI dest: inv_onto_injective injD)
1.137 +
1.138 +lemma bij_betw_inv_onto: "bij_betw f A B ==> bij_betw (inv_onto A f) B A"
1.139 +by (auto simp add: bij_betw_def inj_on_inv_onto)
1.140
1.141  lemma surj_imp_inj_inv: "surj f ==> inj (inv f)"
1.142 -by (simp add: inj_on_inv surj_range)
1.143 +by (simp add: inj_on_inv_onto surj_range)
1.144
1.145  lemma surj_iff: "(surj f) = (f o inv f = id)"
1.146  apply (simp add: o_def expand_fun_eq)
1.147 @@ -176,7 +190,7 @@
1.148
1.149  lemma inv_equality: "[| !!x. g (f x) = x;  !!y. f (g y) = y |] ==> inv f = g"
1.150  apply (rule ext)
1.151 -apply (auto simp add: inv_def)
1.152 +apply (auto simp add: inv_onto_def)
1.153  done
1.154
1.155  lemma inv_inv_eq: "bij f ==> inv (inv f) = f"
1.156 @@ -191,12 +205,20 @@
1.157      inv(inv f)=f all fail.
1.158  **)
1.159
1.160 +lemma inv_onto_comp:
1.161 +  "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
1.162 +  inv_onto A (f o g) x = (inv_onto A g o inv_onto (g ` A) f) x"
1.163 +apply (rule inv_onto_f_eq)
1.164 +  apply (fast intro: comp_inj_on)
1.165 + apply (simp add: inv_onto_into)
1.166 +apply (simp add: f_inv_onto_f inv_onto_into)
1.167 +done
1.168 +
1.169  lemma o_inv_distrib: "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f"
1.170  apply (rule inv_equality)
1.171  apply (auto simp add: bij_def surj_f_inv_f)
1.172  done
1.173
1.174 -
1.175  lemma image_surj_f_inv_f: "surj f ==> f ` (inv f ` A) = A"
1.176  by (simp add: image_eq_UN surj_f_inv_f)
1.177
1.178 @@ -214,7 +236,7 @@
1.179
1.180  lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A"
1.181  apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
1.182 -apply (blast intro: bij_is_inj [THEN inv_f_f, symmetric])
1.183 +apply (blast intro: bij_is_inj [THEN inv_onto_f_f, symmetric])
1.184  done
1.185
1.186  lemma finite_fun_UNIVD1:
1.187 @@ -231,64 +253,12 @@
1.188    moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
1.189    proof (rule UNIV_eq_I)
1.190      fix x :: 'a
1.191 -    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_def)
1.192 +    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_onto_def)
1.193      thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
1.194    qed
1.195    ultimately show "finite (UNIV :: 'a set)" by simp
1.196  qed
1.197
1.198 -subsection {*Inverse of a PI-function (restricted domain)*}
1.199 -
1.200 -lemma Inv_f_f: "[| inj_on f A;  x \<in> A |] ==> Inv A f (f x) = x"
1.201 -apply (simp add: Inv_def inj_on_def)
1.202 -apply (blast intro: someI2)
1.203 -done
1.204 -
1.205 -lemma f_Inv_f: "y \<in> f`A  ==> f (Inv A f y) = y"
1.207 -apply (fast intro: someI2)
1.208 -done
1.209 -
1.210 -lemma Inv_injective:
1.211 -  assumes eq: "Inv A f x = Inv A f y"
1.212 -      and x: "x: f`A"
1.213 -      and y: "y: f`A"
1.214 -  shows "x=y"
1.215 -proof -
1.216 -  have "f (Inv A f x) = f (Inv A f y)" using eq by simp
1.217 -  thus ?thesis by (simp add: f_Inv_f x y)
1.218 -qed
1.219 -
1.220 -lemma inj_on_Inv: "B <= f`A ==> inj_on (Inv A f) B"
1.221 -apply (rule inj_onI)
1.222 -apply (blast intro: inj_onI dest: Inv_injective injD)
1.223 -done
1.224 -
1.225 -lemma Inv_mem: "[| f ` A = B;  x \<in> B |] ==> Inv A f x \<in> A"
1.227 -apply (fast intro: someI2)
1.228 -done
1.229 -
1.230 -lemma Inv_f_eq: "[| inj_on f A; f x = y; x \<in> A |] ==> Inv A f y = x"
1.231 -  apply (erule subst)
1.232 -  apply (erule Inv_f_f, assumption)
1.233 -  done
1.234 -
1.235 -lemma Inv_comp:
1.236 -  "[| inj_on f (g ` A); inj_on g A; x \<in> f ` g ` A |] ==>
1.237 -  Inv A (f o g) x = (Inv A g o Inv (g ` A) f) x"
1.238 -  apply simp
1.239 -  apply (rule Inv_f_eq)
1.240 -    apply (fast intro: comp_inj_on)
1.241 -   apply (simp add: f_Inv_f Inv_mem)
1.242 -  apply (simp add: Inv_mem)
1.243 -  done
1.244 -
1.245 -lemma bij_betw_Inv: "bij_betw f A B \<Longrightarrow> bij_betw (Inv A f) B A"
1.246 -  apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem)
1.247 -  apply (simp add: image_compose [symmetric] o_def)
1.248 -  apply (simp add: image_def Inv_f_f)
1.249 -  done
1.250
1.251  subsection {*Other Consequences of Hilbert's Epsilon*}
1.252
```