clarified notation;
authorwenzelm
Sun Sep 18 15:16:42 2016 +0200 (2016-09-18)
changeset 63909cc15bd7c5396
parent 63908 ca41b6670904
child 63910 e4fdf9580372
clarified notation;
NEWS
src/HOL/HOL.thy
     1.1 --- a/NEWS	Sun Sep 18 11:31:19 2016 +0200
     1.2 +++ b/NEWS	Sun Sep 18 15:16:42 2016 +0200
     1.3 @@ -231,6 +231,14 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* The unique existence quantifier no longer provides 'binder' syntax,
     1.8 +but uses syntax translations (as for bounded unique existence). Thus
     1.9 +iterated quantification \<exists>!x y. P x y with its slightly confusing
    1.10 +sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead,
    1.11 +pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y
    1.12 +(analogous existing notation \<exists>!(x, y)\<in>A. P x y). Potential
    1.13 +INCOMPATIBILITY in rare situations.
    1.14 +
    1.15  * Renamed session HOL-Multivariate_Analysis to HOL-Analysis.
    1.16  
    1.17  * Moved measure theory from HOL-Probability to HOL-Analysis. When importing
     2.1 --- a/src/HOL/HOL.thy	Sun Sep 18 11:31:19 2016 +0200
     2.2 +++ b/src/HOL/HOL.thy	Sun Sep 18 15:16:42 2016 +0200
     2.3 @@ -99,12 +99,24 @@
     2.4  definition disj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<or>" 30)
     2.5    where or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
     2.6  
     2.7 -definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>!" 10)
     2.8 +definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
     2.9    where "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)"
    2.10  
    2.11  
    2.12  subsubsection \<open>Additional concrete syntax\<close>
    2.13  
    2.14 +syntax (ASCII)
    2.15 +  "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3EX! _./ _)" [0, 10] 10)
    2.16 +syntax (input)
    2.17 +  "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3?! _./ _)" [0, 10] 10)
    2.18 +syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<exists>!_./ _)" [0, 10] 10)
    2.19 +translations "\<exists>!x. P" \<rightleftharpoons> "CONST Ex1 (\<lambda>x. P)"
    2.20 +
    2.21 +print_translation \<open>
    2.22 + [Syntax_Trans.preserve_binder_abs_tr' @{const_syntax Ex1} @{syntax_const "_Ex1"}]
    2.23 +\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
    2.24 +
    2.25 +
    2.26  abbreviation Not_Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<nexists>" 10)
    2.27    where "\<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)"
    2.28  
    2.29 @@ -158,13 +170,11 @@
    2.30  
    2.31  notation (ASCII)
    2.32    All  (binder "ALL " 10) and
    2.33 -  Ex  (binder "EX " 10) and
    2.34 -  Ex1  (binder "EX! " 10)
    2.35 +  Ex  (binder "EX " 10)
    2.36  
    2.37  notation (input)
    2.38    All  (binder "! " 10) and
    2.39 -  Ex  (binder "? " 10) and
    2.40 -  Ex1  (binder "?! " 10)
    2.41 +  Ex  (binder "? " 10)
    2.42  
    2.43  
    2.44  subsubsection \<open>Axioms and basic definitions\<close>