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.4    by (simp_all add: fun_eq_iff)
     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.35  by (simp add: inj_on_def)
    1.36  
    1.37 -lemma surj_id[simp]: "surj_on id A"
    1.38 -by (simp add: surj_on_def)
    1.39 +lemma surj_id: "surj id"
    1.40 +by simp
    1.41  
    1.42  lemma bij_id[simp]: "bij id"
    1.43  by (simp add: bij_betw_def)
    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.68    by (simp add: surj_def)
    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.88  by (simp add: bij_def)
    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.91  by (simp add: bij_betw_def)
    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.101  by(auto simp add:bij_betw_def comp_inj_on)
   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.113 -by (simp add: surj_range)
   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"