src/HOL/Fun.thy
 changeset 40702 cf26dd7395e4 parent 40602 91e583511113 child 40703 d1fc454d6735
```     1.1 --- a/src/HOL/Fun.thy	Wed Nov 24 10:52:02 2010 +0100
1.2 +++ b/src/HOL/Fun.thy	Mon Nov 22 10:34:33 2010 +0100
1.3 @@ -130,24 +130,22 @@
1.5
1.6
1.7 -subsection {* Injectivity, Surjectivity and Bijectivity *}
1.8 +subsection {* Injectivity and Bijectivity *}
1.9
1.10  definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where -- "injective"
1.11    "inj_on f A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y)"
1.12
1.13 -definition surj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> bool" where -- "surjective"
1.14 -  "surj_on f B \<longleftrightarrow> B \<subseteq> range f"
1.15 -
1.16  definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where -- "bijective"
1.17    "bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
1.18
1.19 -text{*A common special case: functions injective over the entire domain type.*}
1.20 +text{*A common special case: functions injective, surjective or bijective over
1.21 +the entire domain type.*}
1.22
1.23  abbreviation
1.24    "inj f \<equiv> inj_on f UNIV"
1.25
1.26 -abbreviation
1.27 -  "surj f \<equiv> surj_on f UNIV"
1.28 +abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where -- "surjective"
1.29 +  "surj f \<equiv> (range f = UNIV)"
1.30
1.31  abbreviation
1.32    "bij f \<equiv> bij_betw f UNIV UNIV"
1.33 @@ -187,8 +185,8 @@
1.34  lemma inj_on_id2[simp]: "inj_on (%x. x) A"
1.36
1.37 -lemma surj_id[simp]: "surj_on id A"
1.39 +lemma surj_id: "surj id"
1.40 +by simp
1.41
1.42  lemma bij_id[simp]: "bij id"
1.44 @@ -251,20 +249,11 @@
1.45  apply (blast)
1.46  done
1.47
1.48 -lemma surj_onI: "(\<And>x. x \<in> B \<Longrightarrow> g (f x) = x) \<Longrightarrow> surj_on g B"
1.49 -  by (simp add: surj_on_def) (blast intro: sym)
1.50 -
1.51 -lemma surj_onD: "surj_on f B \<Longrightarrow> y \<in> B \<Longrightarrow> \<exists>x. y = f x"
1.52 -  by (auto simp: surj_on_def)
1.53 +lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
1.54 +  by auto
1.55
1.56 -lemma surj_on_range_iff: "surj_on f B \<longleftrightarrow> (\<exists>A. f ` A = B)"
1.57 -  unfolding surj_on_def by (auto intro!: exI[of _ "f -` B"])
1.58 -
1.59 -lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
1.60 -  by (simp add: surj_on_def subset_eq image_iff)
1.61 -
1.62 -lemma surjI: "(\<And> x. g (f x) = x) \<Longrightarrow> surj g"
1.63 -  by (blast intro: surj_onI)
1.64 +lemma surjI: assumes *: "\<And> x. g (f x) = x" shows "surj g"
1.65 +  using *[symmetric] by auto
1.66
1.67  lemma surjD: "surj f \<Longrightarrow> \<exists>x. y = f x"
1.69 @@ -278,17 +267,11 @@
1.70  apply (drule_tac x = x in spec, blast)
1.71  done
1.72
1.73 -lemma surj_range: "surj f \<Longrightarrow> range f = UNIV"
1.74 -  by (auto simp add: surj_on_def)
1.75 -
1.76 -lemma surj_range_iff: "surj f \<longleftrightarrow> range f = UNIV"
1.77 -  unfolding surj_on_def by auto
1.78 -
1.79  lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
1.80 -  unfolding bij_betw_def surj_range_iff by auto
1.81 +  unfolding bij_betw_def by auto
1.82
1.83  lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
1.84 -  unfolding surj_range_iff bij_betw_def ..
1.85 +  unfolding bij_betw_def ..
1.86
1.87  lemma bijI: "[| inj f; surj f |] ==> bij f"
1.89 @@ -302,16 +285,13 @@
1.90  lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
1.92
1.93 -lemma bij_betw_imp_surj_on: "bij_betw f A B \<Longrightarrow> surj_on f B"
1.94 -by (auto simp: bij_betw_def surj_on_range_iff)
1.95 -
1.96 -lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
1.97 -by(fastsimp intro: comp_inj_on comp_surj simp: bij_def surj_range)
1.98 -
1.99  lemma bij_betw_trans:
1.100    "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
1.102
1.103 +lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
1.104 +  by (rule bij_betw_trans)
1.105 +
1.106  lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
1.107  proof -
1.108    have i: "inj_on f A" and s: "f ` A = B"
1.109 @@ -349,15 +329,13 @@
1.110    using assms unfolding bij_betw_def inj_on_Un image_Un by auto
1.111
1.112  lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
1.114 +by simp
1.115
1.116  lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
1.117  by (simp add: inj_on_def, blast)
1.118
1.119  lemma vimage_subsetD: "surj f ==> f -` B <= A ==> B <= f ` A"
1.120 -apply (unfold surj_def)
1.121 -apply (blast intro: sym)
1.122 -done
1.123 +by (blast intro: sym)
1.124
1.125  lemma vimage_subsetI: "inj f ==> B <= f ` A ==> f -` B <= A"
1.126  by (unfold inj_on_def, blast)
1.127 @@ -410,7 +388,7 @@
1.128  done
1.129
1.130  lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)"
1.131 -by (auto simp add: surj_def)
1.132 +by auto
1.133
1.134  lemma inj_image_Compl_subset: "inj f ==> f`(-A) <= -(f`A)"
1.135  by (auto simp add: inj_on_def)
1.136 @@ -559,10 +537,10 @@
1.137  qed
1.138
1.139  lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (swap a b f)"
1.140 -  unfolding surj_range_iff by simp
1.141 +  by simp
1.142
1.143  lemma surj_swap_iff [simp]: "surj (swap a b f) \<longleftrightarrow> surj f"
1.144 -  unfolding surj_range_iff by simp
1.145 +  by simp
1.146
1.147  lemma bij_betw_swap_iff [simp]:
1.148    "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> bij_betw (swap x y f) A B \<longleftrightarrow> bij_betw f A B"
```