# HG changeset patch
# User haftmann
# Date 1468014191 -7200
# Node ID 6af79184bef3dc9cfa15111ca70a0ab73eab4b2b
# Parent  8f91c2f447a0f338edcb0e8751b1cdd272a1dc21
avoid to hide equality behind (output) abbreviation

diff -r 8f91c2f447a0 -r 6af79184bef3 NEWS
--- a/NEWS	Fri Jul 08 23:43:11 2016 +0200
+++ b/NEWS	Fri Jul 08 23:43:11 2016 +0200
@@ -150,6 +150,9 @@
 equations in functional programming style: variables present on the
 left-hand but not on the righ-hand side are replaced by underscores.
 
+* "surj" is a mere input abbreviation, to avoid hiding an equation in
+term output.  Minor INCOMPATIBILITY.
+
 * Theory Library/Combinator_PER.thy: combinator to build partial
 equivalence relations from a predicate and an equivalence relation.
 
diff -r 8f91c2f447a0 -r 6af79184bef3 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Fri Jul 08 23:43:11 2016 +0200
+++ b/src/HOL/Fun.thy	Fri Jul 08 23:43:11 2016 +0200
@@ -150,15 +150,11 @@
 
 abbreviation "inj f \<equiv> inj_on f UNIV"
 
-abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  \<comment> "surjective"
+abbreviation (input) surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
   where "surj f \<equiv> range f = UNIV"
 
 abbreviation "bij f \<equiv> bij_betw f UNIV UNIV"
 
-text \<open>The negated case:\<close>
-translations
-  "\<not> CONST surj f" \<leftharpoondown> "CONST range f \<noteq> CONST UNIV"
-
 lemma injI: "(\<And>x y. f x = f y \<Longrightarrow> x = y) \<Longrightarrow> inj f"
   unfolding inj_on_def by auto
 
@@ -303,13 +299,7 @@
   by (simp add: surj_def, blast)
 
 lemma comp_surj: "surj f \<Longrightarrow> surj g \<Longrightarrow> surj (g \<circ> f)"
-  apply (simp add: comp_def surj_def)
-  apply clarify
-  apply (drule_tac x = y in spec)
-  apply clarify
-  apply (drule_tac x = x in spec)
-  apply blast
-  done
+  by (simp add: image_comp [symmetric])
 
 lemma bij_betw_imageI: "inj_on f A \<Longrightarrow> f ` A = B \<Longrightarrow> bij_betw f A B"
   unfolding bij_betw_def by clarify