# HG changeset patch
# User hoelzl
# Date 1283421249 -7200
# Node ID b3a9b6734663530188903852b606b530241efa37
# Parent  a18e5946d63c9cdc4c77ee092600698e56c02162
Introduce surj_on and replace surj and bij by abbreviations.

diff -r a18e5946d63c -r b3a9b6734663 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Sep 02 10:45:51 2010 +0200
+++ b/src/HOL/Fun.thy	Thu Sep 02 11:54:09 2010 +0200
@@ -117,31 +117,27 @@
 no_notation fcomp (infixl "\<circ>>" 60)
 
 
-subsection {* Injectivity and Surjectivity *}
+subsection {* Injectivity, Surjectivity and Bijectivity *}
+
+definition inj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> bool" where -- "injective"
+  "inj_on f A \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>A. f x = f y \<longrightarrow> x = y)"
 
-definition
-  inj_on :: "['a => 'b, 'a set] => bool" where
-  -- "injective"
-  "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y"
+definition surj_on :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> bool" where -- "surjective"
+  "surj_on f B \<longleftrightarrow> B \<subseteq> range f"
+
+definition bij_betw :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool" where -- "bijective"
+  "bij_betw f A B \<longleftrightarrow> inj_on f A \<and> f ` A = B"
 
 text{*A common special case: functions injective over the entire domain type.*}
 
 abbreviation
-  "inj f == inj_on f UNIV"
-
-definition
-  bij_betw :: "('a => 'b) => 'a set => 'b set => bool" where -- "bijective"
-  "bij_betw f A B \<longleftrightarrow> inj_on f A & f ` A = B"
+  "inj f \<equiv> inj_on f UNIV"
 
-definition
-  surj :: "('a => 'b) => bool" where
-  -- "surjective"
-  "surj f == ! y. ? x. y=f(x)"
+abbreviation
+  "surj f \<equiv> surj_on f UNIV"
 
-definition
-  bij :: "('a => 'b) => bool" where
-  -- "bijective"
-  "bij f == inj f & surj f"
+abbreviation
+  "bij f \<equiv> bij_betw f UNIV UNIV"
 
 lemma injI:
   assumes "\<And>x y. f x = f y \<Longrightarrow> x = y"
@@ -173,16 +169,16 @@
 by (simp add: inj_on_eq_iff)
 
 lemma inj_on_id[simp]: "inj_on id A"
-  by (simp add: inj_on_def) 
+  by (simp add: inj_on_def)
 
 lemma inj_on_id2[simp]: "inj_on (%x. x) A"
-by (simp add: inj_on_def) 
+by (simp add: inj_on_def)
 
-lemma surj_id[simp]: "surj id"
-by (simp add: surj_def) 
+lemma surj_id[simp]: "surj_on id A"
+by (simp add: surj_on_def)
 
-lemma bij_id[simp]: "bij id"
-by (simp add: bij_def)
+lemma bij_id[simp]: "bij_betw id A A"
+by (simp add: bij_betw_def)
 
 lemma inj_onI:
     "(!! x y. [|  x:A;  y:A;  f(x) = f(y) |] ==> x=y) ==> inj_on f A"
@@ -242,19 +238,26 @@
 apply (blast)
 done
 
-lemma surjI: "(!! x. g(f x) = x) ==> surj g"
-apply (simp add: surj_def)
-apply (blast intro: sym)
-done
+lemma surj_onI: "(\<And>x. x \<in> B \<Longrightarrow> g (f x) = x) \<Longrightarrow> surj_on g B"
+  by (simp add: surj_on_def) (blast intro: sym)
+
+lemma surj_onD: "surj_on f B \<Longrightarrow> y \<in> B \<Longrightarrow> \<exists>x. y = f x"
+  by (auto simp: surj_on_def)
+
+lemma surj_on_range_iff: "surj_on f B \<longleftrightarrow> (\<exists>A. f ` A = B)"
+  unfolding surj_on_def by (auto intro!: exI[of _ "f -` B"])
 
-lemma surj_range: "surj f ==> range f = UNIV"
-by (auto simp add: surj_def)
+lemma surj_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
+  by (simp add: surj_on_def subset_eq image_iff)
+
+lemma surjI: "(\<And> x. g (f x) = x) \<Longrightarrow> surj g"
+  by (blast intro: surj_onI)
 
-lemma surjD: "surj f ==> EX x. y = f x"
-by (simp add: surj_def)
+lemma surjD: "surj f \<Longrightarrow> \<exists>x. y = f x"
+  by (simp add: surj_def)
 
-lemma surjE: "surj f ==> (!!x. y = f x ==> C) ==> C"
-by (simp add: surj_def, blast)
+lemma surjE: "surj f \<Longrightarrow> (\<And>x. y = f x \<Longrightarrow> C) \<Longrightarrow> C"
+  by (simp add: surj_def, blast)
 
 lemma comp_surj: "[| surj f;  surj g |] ==> surj (g o f)"
 apply (simp add: comp_def surj_def, clarify)
@@ -262,14 +265,17 @@
 apply (drule_tac x = x in spec, blast)
 done
 
+lemma surj_range: "surj f \<Longrightarrow> range f = UNIV"
+  by (auto simp add: surj_on_def)
+
 lemma surj_range_iff: "surj f \<longleftrightarrow> range f = UNIV"
-  unfolding expand_set_eq image_iff surj_def by auto
+  unfolding surj_on_def by auto
 
 lemma bij_betw_imp_surj: "bij_betw f A UNIV \<Longrightarrow> surj f"
   unfolding bij_betw_def surj_range_iff by auto
 
-lemma bij_eq_bij_betw: "bij f \<longleftrightarrow> bij_betw f UNIV UNIV"
-  unfolding bij_def surj_range_iff bij_betw_def ..
+lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
+  unfolding surj_range_iff bij_betw_def ..
 
 lemma bijI: "[| inj f; surj f |] ==> bij f"
 by (simp add: bij_def)
@@ -283,6 +289,9 @@
 lemma bij_betw_imp_inj_on: "bij_betw f A B \<Longrightarrow> inj_on f A"
 by (simp add: bij_betw_def)
 
+lemma bij_betw_imp_surj_on: "bij_betw f A B \<Longrightarrow> surj_on f B"
+by (auto simp: bij_betw_def surj_on_range_iff)
+
 lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
 by(fastsimp intro: comp_inj_on comp_surj simp: bij_def surj_range)
 
@@ -511,12 +520,21 @@
 lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
 by (rule ext, simp add: fun_upd_def swap_def)
 
+lemma swap_image_eq [simp]:
+  assumes "a \<in> A" "b \<in> A" shows "swap a b f ` A = f ` A"
+proof -
+  have subset: "\<And>f. swap a b f ` A \<subseteq> f ` A"
+    using assms by (auto simp: image_iff swap_def)
+  then have "swap a b (swap a b f) ` A \<subseteq> (swap a b f) ` A" .
+  with subset[of f] show ?thesis by auto
+qed
+
 lemma inj_on_imp_inj_on_swap:
-  "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
-by (simp add: inj_on_def swap_def, blast)
+  "\<lbrakk>inj_on f A; a \<in> A; b \<in> A\<rbrakk> \<Longrightarrow> inj_on (swap a b f) A"
+  by (simp add: inj_on_def swap_def, blast)
 
 lemma inj_on_swap_iff [simp]:
-  assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A = inj_on f A"
+  assumes A: "a \<in> A" "b \<in> A" shows "inj_on (swap a b f) A \<longleftrightarrow> inj_on f A"
 proof
   assume "inj_on (swap a b f) A"
   with A have "inj_on (swap a b (swap a b f)) A"
@@ -527,51 +545,21 @@
   with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
 qed
 
-lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
-apply (simp add: surj_def swap_def, clarify)
-apply (case_tac "y = f b", blast)
-apply (case_tac "y = f a", auto)
-done
+lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (swap a b f)"
+  unfolding surj_range_iff by simp
 
-lemma surj_swap_iff [simp]: "surj (swap a b f) = surj f"
-proof
-  assume "surj (swap a b f)"
-  hence "surj (swap a b (swap a b f))" by (rule surj_imp_surj_swap)
-  thus "surj f" by simp
-next
-  assume "surj f"
-  thus "surj (swap a b f)" by (rule surj_imp_surj_swap)
-qed
-
-lemma bij_swap_iff: "bij (swap a b f) = bij f"
-by (simp add: bij_def)
+lemma surj_swap_iff [simp]: "surj (swap a b f) \<longleftrightarrow> surj f"
+  unfolding surj_range_iff by simp
 
-lemma bij_betw_swap:
-  assumes "bij_betw f A B" "x \<in> A" "y \<in> A"
-  shows "bij_betw (Fun.swap x y f) A B"
-proof (unfold bij_betw_def, intro conjI)
-  show "inj_on (Fun.swap x y f) A" using assms
-    by (intro inj_on_imp_inj_on_swap) (auto simp: bij_betw_def)
-  show "Fun.swap x y f ` A = B"
-  proof safe
-    fix z assume "z \<in> A"
-    then show "Fun.swap x y f z \<in> B"
-      using assms unfolding bij_betw_def
-      by (auto simp: image_iff Fun.swap_def
-               intro!: bexI[of _ "if z = x then y else if z = y then x else z"])
-  next
-    fix z assume "z \<in> B"
-    then obtain v where "v \<in> A" "z = f v" using assms unfolding bij_betw_def by auto
-    then show "z \<in> Fun.swap x y f ` A" unfolding image_iff
-      using assms
-      by (auto simp add: Fun.swap_def split: split_if_asm
-               intro!: bexI[of _ "if v = x then y else if v = y then x else v"])
-  qed
-qed
+lemma bij_betw_swap_iff [simp]:
+  "\<lbrakk> x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> bij_betw (swap x y f) A B \<longleftrightarrow> bij_betw f A B"
+  by (auto simp: bij_betw_def)
+
+lemma bij_swap_iff [simp]: "bij (swap a b f) \<longleftrightarrow> bij f"
+  by simp
 
 hide_const (open) swap
 
-
 subsection {* Inversion of injective functions *}
 
 definition the_inv_into :: "'a set => ('a => 'b) => ('b => 'a)" where