1.1 --- a/NEWS Sun Oct 18 00:10:20 2009 +0200
1.2 +++ b/NEWS Sun Oct 18 12:07:56 2009 +0200
1.3 @@ -149,6 +149,10 @@
1.4 this. Fix using O_assoc[symmetric]. The same applies to the curried
1.5 version "R OO S".
1.6
1.7 +* Function "Inv" is renamed to "inv_onto" and function "inv" is now an
1.8 +abbreviation for "inv_onto UNIV". Lemmas are renamed accordingly.
1.9 +INCOMPATIBILITY.
1.10 +
1.11 * ML antiquotation @{code_datatype} inserts definition of a datatype
1.12 generated by the code generator; see Predicate.thy for an example.
1.13
2.1 --- a/src/HOL/Algebra/Bij.thy Sun Oct 18 00:10:20 2009 +0200
2.2 +++ b/src/HOL/Algebra/Bij.thy Sun Oct 18 12:07:56 2009 +0200
2.3 @@ -31,8 +31,8 @@
2.4
2.5 subsection {*Bijections Form a Group *}
2.6
2.7 -lemma restrict_Inv_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (Inv S f) x) \<in> Bij S"
2.8 - by (simp add: Bij_def bij_betw_Inv)
2.9 +lemma restrict_inv_onto_Bij: "f \<in> Bij S \<Longrightarrow> (\<lambda>x \<in> S. (inv_onto S f) x) \<in> Bij S"
2.10 + by (simp add: Bij_def bij_betw_inv_onto)
2.11
2.12 lemma id_Bij: "(\<lambda>x\<in>S. x) \<in> Bij S "
2.13 by (auto simp add: Bij_def bij_betw_def inj_on_def)
2.14 @@ -41,8 +41,8 @@
2.15 by (auto simp add: Bij_def bij_betw_compose)
2.16
2.17 lemma Bij_compose_restrict_eq:
2.18 - "f \<in> Bij S \<Longrightarrow> compose S (restrict (Inv S f) S) f = (\<lambda>x\<in>S. x)"
2.19 - by (simp add: Bij_def compose_Inv_id)
2.20 + "f \<in> Bij S \<Longrightarrow> compose S (restrict (inv_onto S f) S) f = (\<lambda>x\<in>S. x)"
2.21 + by (simp add: Bij_def compose_inv_onto_id)
2.22
2.23 theorem group_BijGroup: "group (BijGroup S)"
2.24 apply (simp add: BijGroup_def)
2.25 @@ -52,22 +52,22 @@
2.26 apply (simp add: compose_Bij)
2.27 apply (blast intro: compose_assoc [symmetric] dest: Bij_imp_funcset)
2.28 apply (simp add: id_Bij Bij_imp_funcset Bij_imp_extensional, simp)
2.29 -apply (blast intro: Bij_compose_restrict_eq restrict_Inv_Bij)
2.30 +apply (blast intro: Bij_compose_restrict_eq restrict_inv_onto_Bij)
2.31 done
2.32
2.33
2.34 subsection{*Automorphisms Form a Group*}
2.35
2.36 -lemma Bij_Inv_mem: "\<lbrakk> f \<in> Bij S; x \<in> S\<rbrakk> \<Longrightarrow> Inv S f x \<in> S"
2.37 -by (simp add: Bij_def bij_betw_def Inv_mem)
2.38 +lemma Bij_inv_onto_mem: "\<lbrakk> f \<in> Bij S; x \<in> S\<rbrakk> \<Longrightarrow> inv_onto S f x \<in> S"
2.39 +by (simp add: Bij_def bij_betw_def inv_onto_into)
2.40
2.41 -lemma Bij_Inv_lemma:
2.42 +lemma Bij_inv_onto_lemma:
2.43 assumes eq: "\<And>x y. \<lbrakk>x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> h(g x y) = g (h x) (h y)"
2.44 shows "\<lbrakk>h \<in> Bij S; g \<in> S \<rightarrow> S \<rightarrow> S; x \<in> S; y \<in> S\<rbrakk>
2.45 - \<Longrightarrow> Inv S h (g x y) = g (Inv S h x) (Inv S h y)"
2.46 + \<Longrightarrow> inv_onto S h (g x y) = g (inv_onto S h x) (inv_onto S h y)"
2.47 apply (simp add: Bij_def bij_betw_def)
2.48 apply (subgoal_tac "\<exists>x'\<in>S. \<exists>y'\<in>S. x = h x' & y = h y'", clarify)
2.49 - apply (simp add: eq [symmetric] Inv_f_f funcset_mem [THEN funcset_mem], blast)
2.50 + apply (simp add: eq [symmetric] inv_f_f funcset_mem [THEN funcset_mem], blast)
2.51 done
2.52
2.53
2.54 @@ -84,17 +84,17 @@
2.55 lemma (in group) mult_funcset: "mult G \<in> carrier G \<rightarrow> carrier G \<rightarrow> carrier G"
2.56 by (simp add: Pi_I group.axioms)
2.57
2.58 -lemma (in group) restrict_Inv_hom:
2.59 +lemma (in group) restrict_inv_onto_hom:
2.60 "\<lbrakk>h \<in> hom G G; h \<in> Bij (carrier G)\<rbrakk>
2.61 - \<Longrightarrow> restrict (Inv (carrier G) h) (carrier G) \<in> hom G G"
2.62 - by (simp add: hom_def Bij_Inv_mem restrictI mult_funcset
2.63 - group.axioms Bij_Inv_lemma)
2.64 + \<Longrightarrow> restrict (inv_onto (carrier G) h) (carrier G) \<in> hom G G"
2.65 + by (simp add: hom_def Bij_inv_onto_mem restrictI mult_funcset
2.66 + group.axioms Bij_inv_onto_lemma)
2.67
2.68 lemma inv_BijGroup:
2.69 - "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (Inv S f) x)"
2.70 + "f \<in> Bij S \<Longrightarrow> m_inv (BijGroup S) f = (\<lambda>x \<in> S. (inv_onto S f) x)"
2.71 apply (rule group.inv_equality)
2.72 apply (rule group_BijGroup)
2.73 -apply (simp_all add: BijGroup_def restrict_Inv_Bij Bij_compose_restrict_eq)
2.74 +apply (simp_all add:BijGroup_def restrict_inv_onto_Bij Bij_compose_restrict_eq)
2.75 done
2.76
2.77 lemma (in group) subgroup_auto:
2.78 @@ -115,7 +115,7 @@
2.79 assume "x \<in> auto G"
2.80 thus "inv\<^bsub>BijGroup (carrier G)\<^esub> x \<in> auto G"
2.81 by (simp del: restrict_apply
2.82 - add: inv_BijGroup auto_def restrict_Inv_Bij restrict_Inv_hom)
2.83 + add: inv_BijGroup auto_def restrict_inv_onto_Bij restrict_inv_onto_hom)
2.84 qed
2.85
2.86 theorem (in group) AutoGroup: "group (AutoGroup G)"
3.1 --- a/src/HOL/Algebra/Group.thy Sun Oct 18 00:10:20 2009 +0200
3.2 +++ b/src/HOL/Algebra/Group.thy Sun Oct 18 12:07:56 2009 +0200
3.3 @@ -553,11 +553,11 @@
3.4 by (simp add: iso_def hom_def inj_on_def bij_betw_def Pi_def)
3.5
3.6 lemma (in group) iso_sym:
3.7 - "h \<in> G \<cong> H \<Longrightarrow> Inv (carrier G) h \<in> H \<cong> G"
3.8 -apply (simp add: iso_def bij_betw_Inv)
3.9 -apply (subgoal_tac "Inv (carrier G) h \<in> carrier H \<rightarrow> carrier G")
3.10 - prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_Inv])
3.11 -apply (simp add: hom_def bij_betw_def Inv_f_eq f_Inv_f Pi_def)
3.12 + "h \<in> G \<cong> H \<Longrightarrow> inv_onto (carrier G) h \<in> H \<cong> G"
3.13 +apply (simp add: iso_def bij_betw_inv_onto)
3.14 +apply (subgoal_tac "inv_onto (carrier G) h \<in> carrier H \<rightarrow> carrier G")
3.15 + prefer 2 apply (simp add: bij_betw_imp_funcset [OF bij_betw_inv_onto])
3.16 +apply (simp add: hom_def bij_betw_def inv_onto_f_eq f_inv_onto_f Pi_def)
3.17 done
3.18
3.19 lemma (in group) iso_trans:
4.1 --- a/src/HOL/Finite_Set.thy Sun Oct 18 00:10:20 2009 +0200
4.2 +++ b/src/HOL/Finite_Set.thy Sun Oct 18 12:07:56 2009 +0200
4.3 @@ -155,6 +155,19 @@
4.4 "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
4.5 by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
4.6
4.7 +lemma finite_imp_inj_to_nat_seg:
4.8 +assumes "finite A"
4.9 +shows "EX f n::nat. f`A = {i. i<n} & inj_on f A"
4.10 +proof -
4.11 + from finite_imp_nat_seg_image_inj_on[OF `finite A`]
4.12 + obtain f and n::nat where bij: "bij_betw f {i. i<n} A"
4.13 + by (auto simp:bij_betw_def)
4.14 + let ?f = "the_inv_onto {i. i<n} f"
4.15 + have "inj_on ?f A & ?f ` A = {i. i<n}"
4.16 + by (fold bij_betw_def) (rule bij_betw_the_inv_onto[OF bij])
4.17 + thus ?thesis by blast
4.18 +qed
4.19 +
4.20 lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}"
4.21 by(fastsimp simp: finite_conv_nat_seg_image)
4.22
5.1 --- a/src/HOL/Fun.thy Sun Oct 18 00:10:20 2009 +0200
5.2 +++ b/src/HOL/Fun.thy Sun Oct 18 12:07:56 2009 +0200
5.3 @@ -145,10 +145,12 @@
5.4 lemma injD: "[| inj(f); f(x) = f(y) |] ==> x=y"
5.5 by (simp add: inj_on_def)
5.6
5.7 -(*Useful with the simplifier*)
5.8 -lemma inj_eq: "inj(f) ==> (f(x) = f(y)) = (x=y)"
5.9 +lemma inj_on_eq_iff: "inj_on f A ==> x:A ==> y:A ==> (f(x) = f(y)) = (x=y)"
5.10 by (force simp add: inj_on_def)
5.11
5.12 +lemma inj_eq: "inj f ==> (f(x) = f(y)) = (x=y)"
5.13 +by (simp add: inj_on_eq_iff)
5.14 +
5.15 lemma inj_on_id[simp]: "inj_on id A"
5.16 by (simp add: inj_on_def)
5.17
5.18 @@ -511,7 +513,7 @@
5.19 shows "inv f (f x) = x"
5.20 proof -
5.21 from assms have "(THE x'. f x' = f x) = (THE x'. x' = x)"
5.22 - by (simp only: inj_eq)
5.23 + by (simp add: inj_on_eq_iff)
5.24 also have "... = x" by (rule the_eq_trivial)
5.25 finally show ?thesis by (unfold inv_def)
5.26 qed
6.1 --- a/src/HOL/Hilbert_Choice.thy Sun Oct 18 00:10:20 2009 +0200
6.2 +++ b/src/HOL/Hilbert_Choice.thy Sun Oct 18 12:07:56 2009 +0200
6.3 @@ -1,5 +1,5 @@
6.4 (* Title: HOL/Hilbert_Choice.thy
6.5 - Author: Lawrence C Paulson
6.6 + Author: Lawrence C Paulson, Tobias Nipkow
6.7 Copyright 2001 University of Cambridge
6.8 *)
6.9
6.10 @@ -31,12 +31,11 @@
6.11 in Syntax.const "_Eps" $ x $ t end)]
6.12 *}
6.13
6.14 -constdefs
6.15 - inv :: "('a => 'b) => ('b => 'a)"
6.16 - "inv(f :: 'a => 'b) == %y. SOME x. f x = y"
6.17 +definition inv_onto :: "'a set => ('a => 'b) => ('b => 'a)" where
6.18 +"inv_onto A f == %x. SOME y. y : A & f y = x"
6.19
6.20 - Inv :: "'a set => ('a => 'b) => ('b => 'a)"
6.21 - "Inv A f == %x. SOME y. y \<in> A & f y = x"
6.22 +abbreviation inv :: "('a => 'b) => ('b => 'a)" where
6.23 +"inv == inv_onto UNIV"
6.24
6.25
6.26 subsection {*Hilbert's Epsilon-operator*}
6.27 @@ -92,20 +91,38 @@
6.28
6.29 subsection {*Function Inverse*}
6.30
6.31 -lemma inv_id [simp]: "inv id = id"
6.32 -by (simp add: inv_def id_def)
6.33 -
6.34 -text{*A one-to-one function has an inverse.*}
6.35 -lemma inv_f_f [simp]: "inj f ==> inv f (f x) = x"
6.36 -by (simp add: inv_def inj_eq)
6.37 -
6.38 -lemma inv_f_eq: "[| inj f; f x = y |] ==> inv f y = x"
6.39 -apply (erule subst)
6.40 -apply (erule inv_f_f)
6.41 +lemma inv_onto_into: "x : f ` A ==> inv_onto A f x : A"
6.42 +apply (simp add: inv_onto_def)
6.43 +apply (fast intro: someI2)
6.44 done
6.45
6.46 -lemma inj_imp_inv_eq: "[| inj f; \<forall>x. f(g x) = x |] ==> inv f = g"
6.47 -by (blast intro: ext inv_f_eq)
6.48 +lemma inv_id [simp]: "inv id = id"
6.49 +by (simp add: inv_onto_def id_def)
6.50 +
6.51 +lemma inv_onto_f_f [simp]:
6.52 + "[| inj_on f A; x : A |] ==> inv_onto A f (f x) = x"
6.53 +apply (simp add: inv_onto_def inj_on_def)
6.54 +apply (blast intro: someI2)
6.55 +done
6.56 +
6.57 +lemma inv_f_f: "inj f ==> inv f (f x) = x"
6.58 +by (simp add: inv_onto_f_f)
6.59 +
6.60 +lemma f_inv_onto_f: "y : f`A ==> f (inv_onto A f y) = y"
6.61 +apply (simp add: inv_onto_def)
6.62 +apply (fast intro: someI2)
6.63 +done
6.64 +
6.65 +lemma inv_onto_f_eq: "[| inj_on f A; x : A; f x = y |] ==> inv_onto A f y = x"
6.66 +apply (erule subst)
6.67 +apply (fast intro: inv_onto_f_f)
6.68 +done
6.69 +
6.70 +lemma inv_f_eq: "[| inj f; f x = y |] ==> inv f y = x"
6.71 +by (simp add:inv_onto_f_eq)
6.72 +
6.73 +lemma inj_imp_inv_eq: "[| inj f; ALL x. f(g x) = x |] ==> inv f = g"
6.74 +by (blast intro: ext inv_onto_f_eq)
6.75
6.76 text{*But is it useful?*}
6.77 lemma inj_transfer:
6.78 @@ -114,13 +131,12 @@
6.79 proof -
6.80 have "f x \<in> range f" by auto
6.81 hence "P(inv f (f x))" by (rule minor)
6.82 - thus "P x" by (simp add: inv_f_f [OF injf])
6.83 + thus "P x" by (simp add: inv_onto_f_f [OF injf])
6.84 qed
6.85
6.86 -
6.87 lemma inj_iff: "(inj f) = (inv f o f = id)"
6.88 apply (simp add: o_def expand_fun_eq)
6.89 -apply (blast intro: inj_on_inverseI inv_f_f)
6.90 +apply (blast intro: inj_on_inverseI inv_onto_f_f)
6.91 done
6.92
6.93 lemma inv_o_cancel[simp]: "inj f ==> inv f o f = id"
6.94 @@ -129,36 +145,34 @@
6.95 lemma o_inv_o_cancel[simp]: "inj f ==> g o inv f o f = g"
6.96 by (simp add: o_assoc[symmetric])
6.97
6.98 -lemma inv_image_cancel[simp]:
6.99 - "inj f ==> inv f ` f ` S = S"
6.100 -by (simp add: image_compose[symmetric])
6.101 -
6.102 +lemma inv_onto_image_cancel[simp]:
6.103 + "inj_on f A ==> S <= A ==> inv_onto A f ` f ` S = S"
6.104 +by(fastsimp simp: image_def)
6.105 +
6.106 lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
6.107 -by (blast intro: surjI inv_f_f)
6.108 -
6.109 -lemma f_inv_f: "y \<in> range(f) ==> f(inv f y) = y"
6.110 -apply (simp add: inv_def)
6.111 -apply (fast intro: someI)
6.112 -done
6.113 +by (blast intro: surjI inv_onto_f_f)
6.114
6.115 lemma surj_f_inv_f: "surj f ==> f(inv f y) = y"
6.116 -by (simp add: f_inv_f surj_range)
6.117 +by (simp add: f_inv_onto_f surj_range)
6.118
6.119 -lemma inv_injective:
6.120 - assumes eq: "inv f x = inv f y"
6.121 - and x: "x: range f"
6.122 - and y: "y: range f"
6.123 +lemma inv_onto_injective:
6.124 + assumes eq: "inv_onto A f x = inv_onto A f y"
6.125 + and x: "x: f`A"
6.126 + and y: "y: f`A"
6.127 shows "x=y"
6.128 proof -
6.129 - have "f (inv f x) = f (inv f y)" using eq by simp
6.130 - thus ?thesis by (simp add: f_inv_f x y)
6.131 + have "f (inv_onto A f x) = f (inv_onto A f y)" using eq by simp
6.132 + thus ?thesis by (simp add: f_inv_onto_f x y)
6.133 qed
6.134
6.135 -lemma inj_on_inv: "A <= range(f) ==> inj_on (inv f) A"
6.136 -by (fast intro: inj_onI elim: inv_injective injD)
6.137 +lemma inj_on_inv_onto: "B <= f`A ==> inj_on (inv_onto A f) B"
6.138 +by (blast intro: inj_onI dest: inv_onto_injective injD)
6.139 +
6.140 +lemma bij_betw_inv_onto: "bij_betw f A B ==> bij_betw (inv_onto A f) B A"
6.141 +by (auto simp add: bij_betw_def inj_on_inv_onto)
6.142
6.143 lemma surj_imp_inj_inv: "surj f ==> inj (inv f)"
6.144 -by (simp add: inj_on_inv surj_range)
6.145 +by (simp add: inj_on_inv_onto surj_range)
6.146
6.147 lemma surj_iff: "(surj f) = (f o inv f = id)"
6.148 apply (simp add: o_def expand_fun_eq)
6.149 @@ -176,7 +190,7 @@
6.150
6.151 lemma inv_equality: "[| !!x. g (f x) = x; !!y. f (g y) = y |] ==> inv f = g"
6.152 apply (rule ext)
6.153 -apply (auto simp add: inv_def)
6.154 +apply (auto simp add: inv_onto_def)
6.155 done
6.156
6.157 lemma inv_inv_eq: "bij f ==> inv (inv f) = f"
6.158 @@ -191,12 +205,20 @@
6.159 inv(inv f)=f all fail.
6.160 **)
6.161
6.162 +lemma inv_onto_comp:
6.163 + "[| inj_on f (g ` A); inj_on g A; x : f ` g ` A |] ==>
6.164 + inv_onto A (f o g) x = (inv_onto A g o inv_onto (g ` A) f) x"
6.165 +apply (rule inv_onto_f_eq)
6.166 + apply (fast intro: comp_inj_on)
6.167 + apply (simp add: inv_onto_into)
6.168 +apply (simp add: f_inv_onto_f inv_onto_into)
6.169 +done
6.170 +
6.171 lemma o_inv_distrib: "[| bij f; bij g |] ==> inv (f o g) = inv g o inv f"
6.172 apply (rule inv_equality)
6.173 apply (auto simp add: bij_def surj_f_inv_f)
6.174 done
6.175
6.176 -
6.177 lemma image_surj_f_inv_f: "surj f ==> f ` (inv f ` A) = A"
6.178 by (simp add: image_eq_UN surj_f_inv_f)
6.179
6.180 @@ -214,7 +236,7 @@
6.181
6.182 lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A"
6.183 apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
6.184 -apply (blast intro: bij_is_inj [THEN inv_f_f, symmetric])
6.185 +apply (blast intro: bij_is_inj [THEN inv_onto_f_f, symmetric])
6.186 done
6.187
6.188 lemma finite_fun_UNIVD1:
6.189 @@ -231,64 +253,12 @@
6.190 moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
6.191 proof (rule UNIV_eq_I)
6.192 fix x :: 'a
6.193 - from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_def)
6.194 + from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_onto_def)
6.195 thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
6.196 qed
6.197 ultimately show "finite (UNIV :: 'a set)" by simp
6.198 qed
6.199
6.200 -subsection {*Inverse of a PI-function (restricted domain)*}
6.201 -
6.202 -lemma Inv_f_f: "[| inj_on f A; x \<in> A |] ==> Inv A f (f x) = x"
6.203 -apply (simp add: Inv_def inj_on_def)
6.204 -apply (blast intro: someI2)
6.205 -done
6.206 -
6.207 -lemma f_Inv_f: "y \<in> f`A ==> f (Inv A f y) = y"
6.208 -apply (simp add: Inv_def)
6.209 -apply (fast intro: someI2)
6.210 -done
6.211 -
6.212 -lemma Inv_injective:
6.213 - assumes eq: "Inv A f x = Inv A f y"
6.214 - and x: "x: f`A"
6.215 - and y: "y: f`A"
6.216 - shows "x=y"
6.217 -proof -
6.218 - have "f (Inv A f x) = f (Inv A f y)" using eq by simp
6.219 - thus ?thesis by (simp add: f_Inv_f x y)
6.220 -qed
6.221 -
6.222 -lemma inj_on_Inv: "B <= f`A ==> inj_on (Inv A f) B"
6.223 -apply (rule inj_onI)
6.224 -apply (blast intro: inj_onI dest: Inv_injective injD)
6.225 -done
6.226 -
6.227 -lemma Inv_mem: "[| f ` A = B; x \<in> B |] ==> Inv A f x \<in> A"
6.228 -apply (simp add: Inv_def)
6.229 -apply (fast intro: someI2)
6.230 -done
6.231 -
6.232 -lemma Inv_f_eq: "[| inj_on f A; f x = y; x \<in> A |] ==> Inv A f y = x"
6.233 - apply (erule subst)
6.234 - apply (erule Inv_f_f, assumption)
6.235 - done
6.236 -
6.237 -lemma Inv_comp:
6.238 - "[| inj_on f (g ` A); inj_on g A; x \<in> f ` g ` A |] ==>
6.239 - Inv A (f o g) x = (Inv A g o Inv (g ` A) f) x"
6.240 - apply simp
6.241 - apply (rule Inv_f_eq)
6.242 - apply (fast intro: comp_inj_on)
6.243 - apply (simp add: f_Inv_f Inv_mem)
6.244 - apply (simp add: Inv_mem)
6.245 - done
6.246 -
6.247 -lemma bij_betw_Inv: "bij_betw f A B \<Longrightarrow> bij_betw (Inv A f) B A"
6.248 - apply (auto simp add: bij_betw_def inj_on_Inv Inv_mem)
6.249 - apply (simp add: image_compose [symmetric] o_def)
6.250 - apply (simp add: image_def Inv_f_f)
6.251 - done
6.252
6.253 subsection {*Other Consequences of Hilbert's Epsilon*}
6.254
7.1 --- a/src/HOL/Library/FuncSet.thy Sun Oct 18 00:10:20 2009 +0200
7.2 +++ b/src/HOL/Library/FuncSet.thy Sun Oct 18 12:07:56 2009 +0200
7.3 @@ -157,7 +157,7 @@
7.4 the theorems belong here, or need at least @{term Hilbert_Choice}.*}
7.5
7.6 lemma bij_betw_imp_funcset: "bij_betw f A B \<Longrightarrow> f \<in> A \<rightarrow> B"
7.7 -by (auto simp add: bij_betw_def inj_on_Inv)
7.8 +by (auto simp add: bij_betw_def)
7.9
7.10 lemma inj_on_compose:
7.11 "[| bij_betw f A B; inj_on g B |] ==> inj_on (compose A g f) A"
7.12 @@ -190,22 +190,20 @@
7.13 !!x. x\<in>A ==> f x = g x |] ==> f = g"
7.14 by (force simp add: expand_fun_eq extensional_def)
7.15
7.16 -lemma Inv_funcset: "f ` A = B ==> (\<lambda>x\<in>B. Inv A f x) : B -> A"
7.17 -by (unfold Inv_def) (fast intro: someI2)
7.18 +lemma inv_onto_funcset: "f ` A = B ==> (\<lambda>x\<in>B. inv_onto A f x) : B -> A"
7.19 +by (unfold inv_onto_def) (fast intro: someI2)
7.20
7.21 -lemma compose_Inv_id:
7.22 - "bij_betw f A B ==> compose A (\<lambda>y\<in>B. Inv A f y) f = (\<lambda>x\<in>A. x)"
7.23 +lemma compose_inv_onto_id:
7.24 + "bij_betw f A B ==> compose A (\<lambda>y\<in>B. inv_onto A f y) f = (\<lambda>x\<in>A. x)"
7.25 apply (simp add: bij_betw_def compose_def)
7.26 apply (rule restrict_ext, auto)
7.27 -apply (erule subst)
7.28 -apply (simp add: Inv_f_f)
7.29 done
7.30
7.31 -lemma compose_id_Inv:
7.32 - "f ` A = B ==> compose B f (\<lambda>y\<in>B. Inv A f y) = (\<lambda>x\<in>B. x)"
7.33 +lemma compose_id_inv_onto:
7.34 + "f ` A = B ==> compose B f (\<lambda>y\<in>B. inv_onto A f y) = (\<lambda>x\<in>B. x)"
7.35 apply (simp add: compose_def)
7.36 apply (rule restrict_ext)
7.37 -apply (simp add: f_Inv_f)
7.38 +apply (simp add: f_inv_onto_f)
7.39 done
7.40
7.41
8.1 --- a/src/HOL/Library/Permutations.thy Sun Oct 18 00:10:20 2009 +0200
8.2 +++ b/src/HOL/Library/Permutations.thy Sun Oct 18 12:07:56 2009 +0200
8.3 @@ -5,11 +5,9 @@
8.4 header {* Permutations, both general and specifically on finite sets.*}
8.5
8.6 theory Permutations
8.7 -imports Finite_Cartesian_Product Parity Fact Main
8.8 +imports Finite_Cartesian_Product Parity Fact
8.9 begin
8.10
8.11 - (* Why should I import Main just to solve the Typerep problem! *)
8.12 -
8.13 definition permutes (infixr "permutes" 41) where
8.14 "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"
8.15
8.16 @@ -85,7 +83,7 @@
8.17 unfolding permutes_def by simp
8.18
8.19 lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y"
8.20 - unfolding permutes_def inv_def apply auto
8.21 + unfolding permutes_def inv_onto_def apply auto
8.22 apply (erule allE[where x=y])
8.23 apply (erule allE[where x=y])
8.24 apply (rule someI_ex) apply blast
8.25 @@ -95,10 +93,11 @@
8.26 done
8.27
8.28 lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S ==> Fun.swap a b id permutes S"
8.29 - unfolding permutes_def swap_def fun_upd_def apply auto apply metis done
8.30 + unfolding permutes_def swap_def fun_upd_def by auto metis
8.31
8.32 -lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
8.33 -apply (simp add: Ball_def permutes_def Diff_iff) by metis
8.34 +lemma permutes_superset:
8.35 + "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
8.36 +by (simp add: Ball_def permutes_def Diff_iff) metis
8.37
8.38 (* ------------------------------------------------------------------------- *)
8.39 (* Group properties. *)
9.1 --- a/src/HOL/SizeChange/Correctness.thy Sun Oct 18 00:10:20 2009 +0200
9.2 +++ b/src/HOL/SizeChange/Correctness.thy Sun Oct 18 12:07:56 2009 +0200
9.3 @@ -1146,7 +1146,7 @@
9.4 assumes "finite S"
9.5 shows "set (set2list S) = S"
9.6 unfolding set2list_def
9.7 -proof (rule f_inv_f)
9.8 +proof (rule f_inv_onto_f)
9.9 from `finite S` have "\<exists>l. set l = S"
9.10 by (rule finite_list)
9.11 thus "S \<in> range set"
10.1 --- a/src/HOL/UNITY/Extend.thy Sun Oct 18 00:10:20 2009 +0200
10.2 +++ b/src/HOL/UNITY/Extend.thy Sun Oct 18 12:07:56 2009 +0200
10.3 @@ -121,12 +121,7 @@
10.4 assumes surj_h: "surj h"
10.5 and prem: "!! x y. g (h(x,y)) = x"
10.6 shows "fst (inv h z) = g z"
10.7 -apply (unfold inv_def)
10.8 -apply (rule_tac y1 = z in surj_h [THEN surjD, THEN exE])
10.9 -apply (rule someI2)
10.10 -apply (drule_tac [2] f = g in arg_cong)
10.11 -apply (auto simp add: prem)
10.12 -done
10.13 +by (metis UNIV_I f_inv_onto_f pair_collapse prem surj_h surj_range)
10.14
10.15
10.16 subsection{*Trivial properties of f, g, h*}
11.1 --- a/src/HOL/ZF/HOLZF.thy Sun Oct 18 00:10:20 2009 +0200
11.2 +++ b/src/HOL/ZF/HOLZF.thy Sun Oct 18 12:07:56 2009 +0200
11.3 @@ -626,7 +626,7 @@
11.4
11.5 lemma nat2Nat_Nat2nat[simp]: "Elem n Nat \<Longrightarrow> nat2Nat (Nat2nat n) = n"
11.6 apply (simp add: Nat2nat_def)
11.7 - apply (rule_tac f_inv_f)
11.8 + apply (rule_tac f_inv_onto_f)
11.9 apply (auto simp add: image_def Nat_def Sep)
11.10 done
11.11
12.1 --- a/src/HOL/ZF/Zet.thy Sun Oct 18 00:10:20 2009 +0200
12.2 +++ b/src/HOL/ZF/Zet.thy Sun Oct 18 12:07:56 2009 +0200
12.3 @@ -33,27 +33,12 @@
12.4 apply (auto simp add: explode_def Sep)
12.5 done
12.6
12.7 -lemma image_Inv_f_f: "inj_on f B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (Inv B f) ` f ` A = A"
12.8 - apply (rule set_ext)
12.9 - apply (auto simp add: Inv_f_f image_def)
12.10 - apply (rule_tac x="f x" in exI)
12.11 - apply (auto simp add: Inv_f_f)
12.12 - done
12.13 -
12.14 lemma image_zet_rep: "A \<in> zet \<Longrightarrow> ? z . g ` A = explode z"
12.15 apply (auto simp add: zet_def')
12.16 - apply (rule_tac x="Repl z (g o (Inv A f))" in exI)
12.17 + apply (rule_tac x="Repl z (g o (inv_onto A f))" in exI)
12.18 apply (simp add: explode_Repl_eq)
12.19 apply (subgoal_tac "explode z = f ` A")
12.20 - apply (simp_all add: comp_image_eq image_Inv_f_f)
12.21 - done
12.22 -
12.23 -lemma Inv_f_f_mem:
12.24 - assumes "x \<in> A"
12.25 - shows "Inv A g (g x) \<in> A"
12.26 - apply (simp add: Inv_def)
12.27 - apply (rule someI2)
12.28 - using `x \<in> A` apply auto
12.29 + apply (simp_all add: comp_image_eq)
12.30 done
12.31
12.32 lemma zet_image_mem:
12.33 @@ -64,10 +49,10 @@
12.34 by (auto simp add: zet_def')
12.35 then obtain f where injf: "inj_on (f :: _ \<Rightarrow> ZF) A"
12.36 by auto
12.37 - let ?w = "f o (Inv A g)"
12.38 - have subset: "(Inv A g) ` (g ` A) \<subseteq> A"
12.39 - by (auto simp add: Inv_f_f_mem)
12.40 - have "inj_on (Inv A g) (g ` A)" by (simp add: inj_on_Inv)
12.41 + let ?w = "f o (inv_onto A g)"
12.42 + have subset: "(inv_onto A g) ` (g ` A) \<subseteq> A"
12.43 + by (auto simp add: inv_onto_into)
12.44 + have "inj_on (inv_onto A g) (g ` A)" by (simp add: inj_on_inv_onto)
12.45 then have injw: "inj_on ?w (g ` A)"
12.46 apply (rule comp_inj_on)
12.47 apply (rule subset_inj_on[where B=A])
12.48 @@ -101,7 +86,7 @@
12.49 lemma zexplode_zimplode: "zexplode (zimplode A) = A"
12.50 apply (simp add: zimplode_def zexplode_def)
12.51 apply (simp add: implode_def)
12.52 - apply (subst f_inv_f[where y="Rep_zet A"])
12.53 + apply (subst f_inv_onto_f[where y="Rep_zet A"])
12.54 apply (auto simp add: Rep_zet_inverse Rep_zet_eq_explode image_def)
12.55 done
12.56
13.1 --- a/src/HOL/ex/set.thy Sun Oct 18 00:10:20 2009 +0200
13.2 +++ b/src/HOL/ex/set.thy Sun Oct 18 12:07:56 2009 +0200
13.3 @@ -104,7 +104,7 @@
13.4 --{*The term above can be synthesized by a sufficiently detailed proof.*}
13.5 apply (rule bij_if_then_else)
13.6 apply (rule_tac [4] refl)
13.7 - apply (rule_tac [2] inj_on_inv)
13.8 + apply (rule_tac [2] inj_on_inv_onto)
13.9 apply (erule subset_inj_on [OF _ subset_UNIV])
13.10 apply blast
13.11 apply (erule ssubst, subst double_complement, erule inv_image_comp [symmetric])