src/HOL/Fun.thy
 changeset 39076 b3a9b6734663 parent 39075 a18e5946d63c child 39101 606432dd1896
```     1.1 --- a/src/HOL/Fun.thy	Thu Sep 02 10:45:51 2010 +0200
1.2 +++ b/src/HOL/Fun.thy	Thu Sep 02 11:54:09 2010 +0200
1.3 @@ -117,31 +117,27 @@
1.4  no_notation fcomp (infixl "\<circ>>" 60)
1.5
1.6
1.7 -subsection {* Injectivity and Surjectivity *}
1.8 +subsection {* Injectivity, Surjectivity 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
1.14 -  inj_on :: "['a => 'b, 'a set] => bool" where
1.15 -  -- "injective"
1.16 -  "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
1.17 +definition surj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> bool" where -- "surjective"
1.18 +  "surj_on f B \<longleftrightarrow> B \<subseteq> range f"
1.19 +
1.20 +definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where -- "bijective"
1.21 +  "bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
1.22
1.23  text{*A common special case: functions injective over the entire domain type.*}
1.24
1.25  abbreviation
1.26 -  "inj f == inj_on f UNIV"
1.27 -
1.28 -definition
1.29 -  bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
1.30 -  "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
1.31 +  "inj f \<equiv> inj_on f UNIV"
1.32
1.33 -definition
1.34 -  surj :: "('a => 'b) => bool" where
1.35 -  -- "surjective"
1.36 -  "surj f == ! y. ? x. y=f(x)"
1.37 +abbreviation
1.38 +  "surj f \<equiv> surj_on f UNIV"
1.39
1.40 -definition
1.41 -  bij :: "('a => 'b) => bool" where
1.42 -  -- "bijective"
1.43 -  "bij f == inj f & surj f"
1.44 +abbreviation
1.45 +  "bij f \<equiv> bij_betw f UNIV UNIV"
1.46
1.47  lemma injI:
1.48    assumes "\<And>x y. f x = f y \<Longrightarrow> x = y"
1.49 @@ -173,16 +169,16 @@
1.51
1.52  lemma inj_on_id[simp]: "inj_on id A"
1.53 -  by (simp add: inj_on_def)
1.54 +  by (simp add: inj_on_def)
1.55
1.56  lemma inj_on_id2[simp]: "inj_on (%x. x) A"
1.59
1.60 -lemma surj_id[simp]: "surj id"
1.62 +lemma surj_id[simp]: "surj_on id A"
1.64
1.65 -lemma bij_id[simp]: "bij id"
1.67 +lemma bij_id[simp]: "bij_betw id A A"
1.69
1.70  lemma inj_onI:
1.71      "(!! x y. [|  x:A;  y:A;  f(x) = f(y) |] ==> x=y) ==> inj_on f A"
1.72 @@ -242,19 +238,26 @@
1.73  apply (blast)
1.74  done
1.75
1.76 -lemma surjI: "(!! x. g(f x) = x) ==> surj g"
1.78 -apply (blast intro: sym)
1.79 -done
1.80 +lemma surj_onI: "(\<And>x. x \<in> B \<Longrightarrow> g (f x) = x) \<Longrightarrow> surj_on g B"
1.81 +  by (simp add: surj_on_def) (blast intro: sym)
1.82 +
1.83 +lemma surj_onD: "surj_on f B \<Longrightarrow> y \<in> B \<Longrightarrow> \<exists>x. y = f x"
1.84 +  by (auto simp: surj_on_def)
1.85 +
1.86 +lemma surj_on_range_iff: "surj_on f B \<longleftrightarrow> (\<exists>A. f ` A = B)"
1.87 +  unfolding surj_on_def by (auto intro!: exI[of _ "f -` B"])
1.88
1.89 -lemma surj_range: "surj f ==> range f = UNIV"
1.90 -by (auto simp add: surj_def)
1.91 +lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
1.92 +  by (simp add: surj_on_def subset_eq image_iff)
1.93 +
1.94 +lemma surjI: "(\<And> x. g (f x) = x) \<Longrightarrow> surj g"
1.95 +  by (blast intro: surj_onI)
1.96
1.97 -lemma surjD: "surj f ==> EX x. y = f x"
1.99 +lemma surjD: "surj f \<Longrightarrow> \<exists>x. y = f x"
1.100 +  by (simp add: surj_def)
1.101
1.102 -lemma surjE: "surj f ==> (!!x. y = f x ==> C) ==> C"
1.103 -by (simp add: surj_def, blast)
1.104 +lemma surjE: "surj f \<Longrightarrow> (\<And>x. y = f x \<Longrightarrow> C) \<Longrightarrow> C"
1.105 +  by (simp add: surj_def, blast)
1.106
1.107  lemma comp_surj: "[| surj f;  surj g |] ==> surj (g o f)"
1.108  apply (simp add: comp_def surj_def, clarify)
1.109 @@ -262,14 +265,17 @@
1.110  apply (drule_tac x = x in spec, blast)
1.111  done
1.112
1.113 +lemma surj_range: "surj f \<Longrightarrow> range f = UNIV"
1.114 +  by (auto simp add: surj_on_def)
1.115 +
1.116  lemma surj_range_iff: "surj f \<longleftrightarrow> range f = UNIV"
1.117 -  unfolding expand_set_eq image_iff surj_def by auto
1.118 +  unfolding surj_on_def by auto
1.119
1.120  lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
1.121    unfolding bij_betw_def surj_range_iff by auto
1.122
1.123 -lemma bij_eq_bij_betw: "bij f \<longleftrightarrow> bij_betw f UNIV UNIV"
1.124 -  unfolding bij_def surj_range_iff bij_betw_def ..
1.125 +lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
1.126 +  unfolding surj_range_iff bij_betw_def ..
1.127
1.128  lemma bijI: "[| inj f; surj f |] ==> bij f"
1.130 @@ -283,6 +289,9 @@
1.131  lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
1.133
1.134 +lemma bij_betw_imp_surj_on: "bij_betw f A B \<Longrightarrow> surj_on f B"
1.135 +by (auto simp: bij_betw_def surj_on_range_iff)
1.136 +
1.137  lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
1.138  by(fastsimp intro: comp_inj_on comp_surj simp: bij_def surj_range)
1.139
1.140 @@ -511,12 +520,21 @@
1.141  lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
1.142  by (rule ext, simp add: fun_upd_def swap_def)
1.143
1.144 +lemma swap_image_eq [simp]:
1.145 +  assumes "a \<in> A" "b \<in> A" shows "swap a b f ` A = f ` A"
1.146 +proof -
1.147 +  have subset: "\<And>f. swap a b f ` A \<subseteq> f ` A"
1.148 +    using assms by (auto simp: image_iff swap_def)
1.149 +  then have "swap a b (swap a b f) ` A \<subseteq> (swap a b f) ` A" .
1.150 +  with subset[of f] show ?thesis by auto
1.151 +qed
1.152 +
1.153  lemma inj_on_imp_inj_on_swap:
1.154 -  "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
1.155 -by (simp add: inj_on_def swap_def, blast)
1.156 +  "\<lbrakk>inj_on f A; a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> inj_on (swap a b f) A"
1.157 +  by (simp add: inj_on_def swap_def, blast)
1.158
1.159  lemma inj_on_swap_iff [simp]:
1.160 -  assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A = inj_on f A"
1.161 +  assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A \<longleftrightarrow> inj_on f A"
1.162  proof
1.163    assume "inj_on (swap a b f) A"
1.164    with A have "inj_on (swap a b (swap a b f)) A"
1.165 @@ -527,51 +545,21 @@
1.166    with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
1.167  qed
1.168
1.169 -lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
1.170 -apply (simp add: surj_def swap_def, clarify)
1.171 -apply (case_tac "y = f b", blast)
1.172 -apply (case_tac "y = f a", auto)
1.173 -done
1.174 +lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (swap a b f)"
1.175 +  unfolding surj_range_iff by simp
1.176
1.177 -lemma surj_swap_iff [simp]: "surj (swap a b f) = surj f"
1.178 -proof
1.179 -  assume "surj (swap a b f)"
1.180 -  hence "surj (swap a b (swap a b f))" by (rule surj_imp_surj_swap)
1.181 -  thus "surj f" by simp
1.182 -next
1.183 -  assume "surj f"
1.184 -  thus "surj (swap a b f)" by (rule surj_imp_surj_swap)
1.185 -qed
1.186 -
1.187 -lemma bij_swap_iff: "bij (swap a b f) = bij f"
1.189 +lemma surj_swap_iff [simp]: "surj (swap a b f) \<longleftrightarrow> surj f"
1.190 +  unfolding surj_range_iff by simp
1.191
1.192 -lemma bij_betw_swap:
1.193 -  assumes "bij_betw f A B" "x \<in> A" "y \<in> A"
1.194 -  shows "bij_betw (Fun.swap x y f) A B"
1.195 -proof (unfold bij_betw_def, intro conjI)
1.196 -  show "inj_on (Fun.swap x y f) A" using assms
1.197 -    by (intro inj_on_imp_inj_on_swap) (auto simp: bij_betw_def)
1.198 -  show "Fun.swap x y f ` A = B"
1.199 -  proof safe
1.200 -    fix z assume "z \<in> A"
1.201 -    then show "Fun.swap x y f z \<in> B"
1.202 -      using assms unfolding bij_betw_def
1.203 -      by (auto simp: image_iff Fun.swap_def
1.204 -               intro!: bexI[of _ "if z = x then y else if z = y then x else z"])
1.205 -  next
1.206 -    fix z assume "z \<in> B"
1.207 -    then obtain v where "v \<in> A" "z = f v" using assms unfolding bij_betw_def by auto
1.208 -    then show "z \<in> Fun.swap x y f ` A" unfolding image_iff
1.209 -      using assms
1.210 -      by (auto simp add: Fun.swap_def split: split_if_asm
1.211 -               intro!: bexI[of _ "if v = x then y else if v = y then x else v"])
1.212 -  qed
1.213 -qed
1.214 +lemma bij_betw_swap_iff [simp]:
1.215 +  "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> bij_betw (swap x y f) A B \<longleftrightarrow> bij_betw f A B"
1.216 +  by (auto simp: bij_betw_def)
1.217 +
1.218 +lemma bij_swap_iff [simp]: "bij (swap a b f) \<longleftrightarrow> bij f"
1.219 +  by simp
1.220
1.221  hide_const (open) swap
1.222
1.223 -
1.224  subsection {* Inversion of injective functions *}
1.225
1.226  definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where
```