# HG changeset patch
# User hoelzl
# Date 1290418473 -3600
# Node ID cf26dd7395e48efa3b4dd99052afd4b848e52a06
# Parent  a3f37b3d303ada3ffcee4262942652bba5a4e588
Replace surj by abbreviation; remove surj_on.

diff -r a3f37b3d303a -r cf26dd7395e4 NEWS
--- a/NEWS	Wed Nov 24 10:52:02 2010 +0100
+++ b/NEWS	Mon Nov 22 10:34:33 2010 +0100
@@ -291,9 +291,10 @@
 derive instantiated and simplified equations for inductive predicates,
 similar to inductive_cases.
 
-* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". surj_on is a
-generalization of surj, and "surj f" is now a abbreviation of "surj_on f UNIV".
-The theorems bij_def and surj_def are unchanged.
+* "bij f" is now an abbreviation of "bij_betw f UNIV UNIV". "surj f" is now an
+abbreviation of "range f = UIV". The theorems bij_def and surj_def are
+unchanged.
+INCOMPATIBILITY.
 
 * Function package: .psimps rules are no longer implicitly declared [simp].
 INCOMPATIBILITY.
diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -2286,7 +2286,7 @@
 
 lemma finite_UNIV_surj_inj: fixes f :: "'a \<Rightarrow> 'a"
 shows "finite(UNIV:: 'a set) \<Longrightarrow> surj f \<Longrightarrow> inj f"
-by (blast intro: finite_surj_inj subset_UNIV dest:surj_range)
+by (blast intro: finite_surj_inj subset_UNIV)
 
 lemma finite_UNIV_inj_surj: fixes f :: "'a \<Rightarrow> 'a"
 shows "finite(UNIV:: 'a set) \<Longrightarrow> inj f \<Longrightarrow> surj f"
diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Fun.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -130,24 +130,22 @@
   by (simp_all add: fun_eq_iff)
 
 
-subsection {* Injectivity, Surjectivity and Bijectivity *}
+subsection {* Injectivity 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 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.*}
+text{*A common special case: functions injective, surjective or bijective over
+the entire domain type.*}
 
 abbreviation
   "inj f \<equiv> inj_on f UNIV"
 
-abbreviation
-  "surj f \<equiv> surj_on f UNIV"
+abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool" where -- "surjective"
+  "surj f \<equiv> (range f = UNIV)"
 
 abbreviation
   "bij f \<equiv> bij_betw f UNIV UNIV"
@@ -187,8 +185,8 @@
 lemma inj_on_id2[simp]: "inj_on (%x. x) A"
 by (simp add: inj_on_def)
 
-lemma surj_id[simp]: "surj_on id A"
-by (simp add: surj_on_def)
+lemma surj_id: "surj id"
+by simp
 
 lemma bij_id[simp]: "bij id"
 by (simp add: bij_betw_def)
@@ -251,20 +249,11 @@
 apply (blast)
 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_def: "surj f \<longleftrightarrow> (\<forall>y. \<exists>x. y = f x)"
+  by auto
 
-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_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 surjI: assumes *: "\<And> x. g (f x) = x" shows "surj g"
+  using *[symmetric] by auto
 
 lemma surjD: "surj f \<Longrightarrow> \<exists>x. y = f x"
   by (simp add: surj_def)
@@ -278,17 +267,11 @@
 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 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
+  unfolding bij_betw_def by auto
 
 lemma bij_def: "bij f \<longleftrightarrow> inj f \<and> surj f"
-  unfolding surj_range_iff bij_betw_def ..
+  unfolding bij_betw_def ..
 
 lemma bijI: "[| inj f; surj f |] ==> bij f"
 by (simp add: bij_def)
@@ -302,16 +285,13 @@
 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)
-
 lemma bij_betw_trans:
   "bij_betw f A B \<Longrightarrow> bij_betw g B C \<Longrightarrow> bij_betw (g o f) A C"
 by(auto simp add:bij_betw_def comp_inj_on)
 
+lemma bij_comp: "bij f \<Longrightarrow> bij g \<Longrightarrow> bij (g o f)"
+  by (rule bij_betw_trans)
+
 lemma bij_betw_inv: assumes "bij_betw f A B" shows "EX g. bij_betw g B A"
 proof -
   have i: "inj_on f A" and s: "f ` A = B"
@@ -349,15 +329,13 @@
   using assms unfolding bij_betw_def inj_on_Un image_Un by auto
 
 lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
-by (simp add: surj_range)
+by simp
 
 lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A"
 by (simp add: inj_on_def, blast)
 
 lemma vimage_subsetD: "surj f ==> f -` B <= A ==> B <= f ` A"
-apply (unfold surj_def)
-apply (blast intro: sym)
-done
+by (blast intro: sym)
 
 lemma vimage_subsetI: "inj f ==> B <= f ` A ==> f -` B <= A"
 by (unfold inj_on_def, blast)
@@ -410,7 +388,7 @@
 done
 
 lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)"
-by (auto simp add: surj_def)
+by auto
 
 lemma inj_image_Compl_subset: "inj f ==> f`(-A) <= -(f`A)"
 by (auto simp add: inj_on_def)
@@ -559,10 +537,10 @@
 qed
 
 lemma surj_imp_surj_swap: "surj f \<Longrightarrow> surj (swap a b f)"
-  unfolding surj_range_iff by simp
+  by simp
 
 lemma surj_swap_iff [simp]: "surj (swap a b f) \<longleftrightarrow> surj f"
-  unfolding surj_range_iff by simp
+  by simp
 
 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"
diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -151,10 +151,10 @@
 by(fastsimp simp: image_def)
 
 lemma inj_imp_surj_inv: "inj f ==> surj (inv f)"
-by (blast intro: surjI inv_into_f_f)
+by (blast intro!: surjI inv_into_f_f)
 
 lemma surj_f_inv_f: "surj f ==> f(inv f y) = y"
-by (simp add: f_inv_into_f surj_range)
+by (simp add: f_inv_into_f)
 
 lemma inv_into_injective:
   assumes eq: "inv_into A f x = inv_into A f y"
@@ -173,12 +173,13 @@
 by (auto simp add: bij_betw_def inj_on_inv_into)
 
 lemma surj_imp_inj_inv: "surj f ==> inj (inv f)"
-by (simp add: inj_on_inv_into surj_range)
+by (simp add: inj_on_inv_into)
 
 lemma surj_iff: "(surj f) = (f o inv f = id)"
-apply (simp add: o_def fun_eq_iff)
-apply (blast intro: surjI surj_f_inv_f)
-done
+by (auto intro!: surjI simp: surj_f_inv_f fun_eq_iff[where 'b='a])
+
+lemma surj_iff_all: "surj f \<longleftrightarrow> (\<forall>x. f (inv f x) = x)"
+  unfolding surj_iff by (simp add: o_def fun_eq_iff)
 
 lemma surj_imp_inv_eq: "[| surj f; \<forall>x. g(f x) = x |] ==> inv f = g"
 apply (rule ext)
diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/Lattice/Orders.thy
--- a/src/HOL/Lattice/Orders.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Lattice/Orders.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -118,8 +118,8 @@
   qed
 qed
 
-lemma range_dual [simp]: "dual ` UNIV = UNIV"
-proof (rule surj_range)
+lemma range_dual [simp]: "surj dual"
+proof -
   have "\<And>x'. dual (undual x') = x'" by simp
   thus "surj dual" by (rule surjI)
 qed
diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/Library/ContNotDenum.thy
--- a/src/HOL/Library/ContNotDenum.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Library/ContNotDenum.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -565,8 +565,7 @@
   shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
 proof -- "by contradiction"
   assume "\<exists>f::nat\<Rightarrow>real. surj f"
-  then obtain f::"nat\<Rightarrow>real" where "surj f" by auto
-  hence rangeF: "range f = UNIV" by (rule surj_range)
+  then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
   -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
   have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
   moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Library/Countable.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -165,7 +165,7 @@
 qed
 
 lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj"
-by (simp add: Rats_def surj_nat_to_rat_surj surj_range)
+by (simp add: Rats_def surj_nat_to_rat_surj)
 
 context field_char_0
 begin
diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -948,14 +948,12 @@
    assumes lf: "linear f" and gf: "f o g = id"
    shows "linear g"
  proof-
-   from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def fun_eq_iff)
-     by metis 
+   from gf have fi: "surj f" by (auto simp add: surj_def o_def id_def) metis
    from linear_surjective_isomorphism[OF lf fi]
    obtain h:: "'a => 'a" where
      h: "linear h" "\<forall>x. h (f x) = x" "\<forall>x. f (h x) = x" by blast
    have "h = g" apply (rule ext) using gf h(2,3)
-     apply (simp add: o_def id_def fun_eq_iff)
-     by metis
+     by (simp add: o_def id_def fun_eq_iff) metis
    with h(1) show ?thesis by blast
  qed
  
diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -2843,7 +2843,7 @@
     h: "linear h" "\<forall> x\<in> basis ` {..<DIM('b)}. h x = inv f x" by blast
   from h(2)
   have th: "\<forall>i<DIM('b). (f o h) (basis i) = id (basis i)"
-    using sf by(auto simp add: surj_iff o_def fun_eq_iff)
+    using sf by(auto simp add: surj_iff_all)
   from linear_eq_stdbasis[OF linear_compose[OF h(1) lf] linear_id th]
   have "f o h = id" .
   then show ?thesis using h(1) by blast
@@ -2995,7 +2995,7 @@
   {fix f f':: "'a => 'a"
     assume lf: "linear f" "linear f'" and f: "f o f' = id"
     from f have sf: "surj f"
-      apply (auto simp add: o_def fun_eq_iff id_def surj_def)
+      apply (auto simp add: o_def id_def surj_def)
       by metis
     from linear_surjective_isomorphism[OF lf(1) sf] lf f
     have "f' o f = id" unfolding fun_eq_iff o_def id_def
diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/Nominal/Examples/Support.thy
--- a/src/HOL/Nominal/Examples/Support.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Nominal/Examples/Support.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -47,7 +47,7 @@
   also have "\<dots> = (\<lambda>n. atom n) ` ({n. \<exists>i. n = 2*i \<or> n = 2*i+1})" by auto
   also have "\<dots> = (\<lambda>n. atom n) ` (UNIV::nat set)" using even_or_odd by auto
   also have "\<dots> = (UNIV::atom set)" using atom.exhaust
-    by (rule_tac  surj_range) (auto simp add: surj_def)
+    by (auto simp add: surj_def)
   finally show "EVEN \<union> ODD = UNIV" by simp
 qed
 
diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -132,7 +132,7 @@
       by (auto intro!: exI[of _ "from_nat i"])
   qed
   have **: "range ?A' = range A"
-    using surj_range[OF surj_from_nat]
+    using surj_from_nat
     by (auto simp: image_compose intro!: imageI)
   show ?thesis unfolding * ** ..
 qed
diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/Product_Type.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -1135,6 +1135,7 @@
 qed
 
 lemma map_pair_surj:
+  fixes f :: "'a \<Rightarrow> 'b" and g :: "'c \<Rightarrow> 'd"
   assumes "surj f" and "surj g"
   shows "surj (map_pair f g)"
 unfolding surj_def
diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -358,7 +358,7 @@
   done
 
 lemma surj_sysOfAlloc [iff]: "surj sysOfAlloc"
-  apply (simp add: surj_iff fun_eq_iff o_apply)
+  apply (simp add: surj_iff_all)
   apply record_auto
   done
 
@@ -386,7 +386,7 @@
   done
 
 lemma surj_sysOfClient [iff]: "surj sysOfClient"
-  apply (simp add: surj_iff fun_eq_iff o_apply)
+  apply (simp add: surj_iff_all)
   apply record_auto
   done
 
@@ -410,7 +410,7 @@
   done
 
 lemma surj_client_map [iff]: "surj client_map"
-  apply (simp add: surj_iff fun_eq_iff o_apply)
+  apply (simp add: surj_iff_all)
   apply record_auto
   done
 
@@ -682,7 +682,7 @@
 lemma fst_lift_map_eq_fst [simp]: "fst (lift_map i x) i = fst x"
 apply (insert fst_o_lift_map [of i])
 apply (drule fun_cong [where x=x])
-apply (simp add: o_def);
+apply (simp add: o_def)
 done
 
 lemma fst_o_lift_map' [simp]:
@@ -702,7 +702,7 @@
   RS guarantees_PLam_I
   RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2)
   |> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def,
-                                   surj_rename RS surj_range])
+                                   surj_rename])
 
 However, the "preserves" property remains to be discharged, and the unfolding
 of "o" and "sub" complicates subsequent reasoning.
@@ -723,7 +723,7 @@
     asm_simp_tac
         (ss addsimps [@{thm lift_guarantees_eq_lift_inv},
                       @{thm rename_guarantees_eq_rename_inv},
-                      @{thm bij_imp_bij_inv}, @{thm surj_rename} RS @{thm surj_range},
+                      @{thm bij_imp_bij_inv}, @{thm surj_rename},
                       @{thm inv_inv_eq}]) 1,
     asm_simp_tac
         (@{simpset} addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
@@ -798,9 +798,9 @@
 lemmas rename_Alloc_Increasing =
   Alloc_Increasing
     [THEN rename_guarantees_sysOfAlloc_I,
-     simplified surj_rename [THEN surj_range] o_def sub_apply
+     simplified surj_rename o_def sub_apply
                 rename_image_Increasing bij_sysOfAlloc
-                allocGiv_o_inv_sysOfAlloc_eq'];
+                allocGiv_o_inv_sysOfAlloc_eq']
 
 lemma System_Increasing_allocGiv:
      "i < Nclients ==> System : Increasing (sub i o allocGiv)"
@@ -879,7 +879,7 @@
             \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel) s)}"
   apply (simp add: o_apply)
   apply (insert Alloc_Safety [THEN rename_guarantees_sysOfAlloc_I])
-  apply (simp add: o_def);
+  apply (simp add: o_def)
   apply (erule component_guaranteesD)
   apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def])
   done
diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/UNITY/Extend.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -127,7 +127,7 @@
      assumes surj_h: "surj h"
          and prem:   "!! x y. g (h(x,y)) = x"
      shows "fst (inv h z) = g z"
-by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h surj_range)
+by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h)
 
 
 subsection{*Trivial properties of f, g, h*}
diff -r a3f37b3d303a -r cf26dd7395e4 src/HOL/UNITY/Rename.thy
--- a/src/HOL/UNITY/Rename.thy	Wed Nov 24 10:52:02 2010 +0100
+++ b/src/HOL/UNITY/Rename.thy	Mon Nov 22 10:34:33 2010 +0100
@@ -60,7 +60,8 @@
 lemma bij_extend_act: "bij h ==> bij (extend_act (%(x,u::'c). h x))"
 apply (rule bijI)
 apply (rule Extend.inj_extend_act)
-apply (auto simp add: bij_extend_act_eq_project_act)
+apply simp
+apply (simp add: bij_extend_act_eq_project_act)
 apply (rule surjI)
 apply (rule Extend.extend_act_inverse)
 apply (blast intro: bij_imp_bij_inv good_map_bij)
@@ -75,7 +76,7 @@
                 project_act (%(x,u::'c). h x)"
 apply (simp (no_asm_simp) add: bij_extend_act_eq_project_act [symmetric])
 apply (rule surj_imp_inv_eq)
-apply (blast intro: bij_extend_act bij_is_surj)
+apply (blast intro!: bij_extend_act bij_is_surj)
 apply (simp (no_asm_simp) add: Extend.extend_act_inverse)
 done