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.50  by (simp add: inj_on_eq_iff)
    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.57 -by (simp add: inj_on_def) 
    1.58 +by (simp add: inj_on_def)
    1.59  
    1.60 -lemma surj_id[simp]: "surj id"
    1.61 -by (simp add: surj_def) 
    1.62 +lemma surj_id[simp]: "surj_on id A"
    1.63 +by (simp add: surj_on_def)
    1.64  
    1.65 -lemma bij_id[simp]: "bij id"
    1.66 -by (simp add: bij_def)
    1.67 +lemma bij_id[simp]: "bij_betw id A A"
    1.68 +by (simp add: bij_betw_def)
    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.77 -apply (simp add: surj_def)
    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.98 -by (simp add: surj_def)
    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.129  by (simp add: bij_def)
   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.132  by (simp add: bij_betw_def)
   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.188 -by (simp add: bij_def)
   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