restored surj as output abbreviation, amending 6af79184bef3
authorhaftmann
Fri Mar 10 13:47:35 2017 +0100 (2017-03-10)
changeset 6517053675f36820d
parent 65169 a8dfa258bf93
child 65178 c4def7e9cfad
restored surj as output abbreviation, amending 6af79184bef3
NEWS
src/HOL/Fun.thy
     1.1 --- a/NEWS	Thu Mar 09 21:55:02 2017 +0100
     1.2 +++ b/NEWS	Fri Mar 10 13:47:35 2017 +0100
     1.3 @@ -48,6 +48,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Constant "surj" is a full input/output abbreviation (again).
     1.8 +Minor INCOMPATIBILITY.
     1.9 +
    1.10  * Theory Library/FinFun has been moved to AFP (again).  INCOMPATIBILITY.
    1.11  
    1.12  * Some old and rarely used ASCII replacement syntax has been removed.
     2.1 --- a/src/HOL/Fun.thy	Thu Mar 09 21:55:02 2017 +0100
     2.2 +++ b/src/HOL/Fun.thy	Fri Mar 10 13:47:35 2017 +0100
     2.3 @@ -148,12 +148,17 @@
     2.4    the entire domain type.
     2.5  \<close>
     2.6  
     2.7 -abbreviation "inj f \<equiv> inj_on f UNIV"
     2.8 +abbreviation inj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
     2.9 +  where "inj f \<equiv> inj_on f UNIV"
    2.10  
    2.11 -abbreviation (input) surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
    2.12 +abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
    2.13    where "surj f \<equiv> range f = UNIV"
    2.14  
    2.15 -abbreviation "bij f \<equiv> bij_betw f UNIV UNIV"
    2.16 +translations -- \<open>The negated case:\<close>
    2.17 +  "\<not> CONST surj f" \<leftharpoondown> "CONST range f \<noteq> CONST UNIV"
    2.18 +
    2.19 +abbreviation bij :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
    2.20 +  where "bij f \<equiv> bij_betw f UNIV UNIV"
    2.21  
    2.22  lemma inj_def: "inj f \<longleftrightarrow> (\<forall>x y. f x = f y \<longrightarrow> x = y)"
    2.23    unfolding inj_on_def by blast