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.34 +apply (simp add: inv_onto_def)
    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.56 +by (simp add: inv_onto_f_f)
    1.57 +
    1.58 +lemma f_inv_onto_f: "y : f`A  ==> f (inv_onto A f y) = y"
    1.59 +apply (simp add: inv_onto_def)
    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.69 +by (simp add:inv_onto_f_eq)
    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.94  by (simp add: o_assoc[symmetric])
    1.95  
    1.96 -lemma inv_image_cancel[simp]:
    1.97 -  "inj f ==> inv f ` f ` S = S"
    1.98 -by (simp add: image_compose[symmetric])
    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.108 -apply (simp add: inv_def)
   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.206 -apply (simp add: Inv_def)
   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.226 -apply (simp add: Inv_def)
   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