author wenzelm Sun Sep 18 15:16:42 2016 +0200 (2016-09-18) changeset 63909 cc15bd7c5396 parent 63908 ca41b6670904 child 63910 e4fdf9580372
clarified notation;
 NEWS file | annotate | diff | revisions src/HOL/HOL.thy file | annotate | diff | revisions
```     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.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>
```