# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1474216597 -7200
# Node ID 255294779d401332a9ee55df0c09d1a4692a82e7
# Parent  6b886cadba7cfed078fe58e2910415366cf389b3# Parent  9f8325206465ac59e7205372ca2230958109a8f7
merged

diff -r 6b886cadba7c -r 255294779d40 NEWS
--- a/NEWS	Sun Sep 18 18:23:59 2016 +0200
+++ b/NEWS	Sun Sep 18 18:36:37 2016 +0200
@@ -231,6 +231,14 @@
 
 *** HOL ***
 
+* The unique existence quantifier no longer provides 'binder' syntax,
+but uses syntax translations (as for bounded unique existence). Thus
+iterated quantification \<exists>!x y. P x y with its slightly confusing
+sequential meaning \<exists>!x. \<exists>!y. P x y is no longer possible. Instead,
+pattern abstraction admits simultaneous unique existence \<exists>!(x, y). P x y
+(analogous existing notation \<exists>!(x, y)\<in>A. P x y). Potential
+INCOMPATIBILITY in rare situations.
+
 * Renamed session HOL-Multivariate_Analysis to HOL-Analysis.
 
 * Moved measure theory from HOL-Probability to HOL-Analysis. When importing
diff -r 6b886cadba7c -r 255294779d40 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Sep 18 18:23:59 2016 +0200
+++ b/src/HOL/HOL.thy	Sun Sep 18 18:36:37 2016 +0200
@@ -99,17 +99,31 @@
 definition disj :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<or>" 30)
   where or_def: "P \<or> Q \<equiv> \<forall>R. (P \<longrightarrow> R) \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> R"
 
-definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>!" 10)
+definition Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
   where "Ex1 P \<equiv> \<exists>x. P x \<and> (\<forall>y. P y \<longrightarrow> y = x)"
 
 
 subsubsection \<open>Additional concrete syntax\<close>
 
-abbreviation Not_Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<nexists>" 10)
-  where "\<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)"
+syntax (ASCII)
+  "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3EX! _./ _)" [0, 10] 10)
+syntax (input)
+  "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3?! _./ _)" [0, 10] 10)
+syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<exists>!_./ _)" [0, 10] 10)
+translations "\<exists>!x. P" \<rightleftharpoons> "CONST Ex1 (\<lambda>x. P)"
 
-abbreviation Not_Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<nexists>!" 10)
-  where "\<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)"
+print_translation \<open>
+ [Syntax_Trans.preserve_binder_abs_tr' @{const_syntax Ex1} @{syntax_const "_Ex1"}]
+\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
+
+
+syntax
+  "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>_./ _)" [0, 10] 10)
+  "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>!_./ _)" [0, 10] 10)
+translations
+  "\<nexists>x. P" \<rightleftharpoons> "\<not> (\<exists>x. P)"
+  "\<nexists>!x. P" \<rightleftharpoons> "\<not> (\<exists>!x. P)"
+
 
 abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool"  (infixl "\<noteq>" 50)
   where "x \<noteq> y \<equiv> \<not> (x = y)"
@@ -158,13 +172,11 @@
 
 notation (ASCII)
   All  (binder "ALL " 10) and
-  Ex  (binder "EX " 10) and
-  Ex1  (binder "EX! " 10)
+  Ex  (binder "EX " 10)
 
 notation (input)
   All  (binder "! " 10) and
-  Ex  (binder "? " 10) and
-  Ex1  (binder "?! " 10)
+  Ex  (binder "? " 10)
 
 
 subsubsection \<open>Axioms and basic definitions\<close>
diff -r 6b886cadba7c -r 255294779d40 src/HOL/Hahn_Banach/Subspace.thy
--- a/src/HOL/Hahn_Banach/Subspace.thy	Sun Sep 18 18:23:59 2016 +0200
+++ b/src/HOL/Hahn_Banach/Subspace.thy	Sun Sep 18 18:36:37 2016 +0200
@@ -479,7 +479,7 @@
   interpret vectorspace E by fact
   interpret subspace H E by fact
   from x y x' have "x \<in> H + lin x'" by auto
-  have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")
+  have "\<exists>!(y, a). x = y + a \<cdot> x' \<and> y \<in> H" (is "\<exists>!p. ?P p")
   proof (rule ex_ex1I)
     from x y show "\<exists>p. ?P p" by blast
     fix p q assume p: "?P p" and q: "?P q"
diff -r 6b886cadba7c -r 255294779d40 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sun Sep 18 18:23:59 2016 +0200
+++ b/src/HOL/Rat.thy	Sun Sep 18 18:36:37 2016 +0200
@@ -339,12 +339,11 @@
   then show ?thesis
   proof (rule ex1I)
     fix p
-    obtain c d :: int where p: "p = (c, d)"
-      by (cases p)
-    assume "r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)"
-    with p have Fract': "r = Fract c d" "d > 0" "coprime c d"
+    assume r: "r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)"
+    obtain c d where p: "p = (c, d)" by (cases p)
+    with r have Fract': "r = Fract c d" "d > 0" "coprime c d"
       by simp_all
-    have "c = a \<and> d = b"
+    have "(c, d) = (a, b)"
     proof (cases "a = 0")
       case True
       with Fract Fract' show ?thesis
@@ -382,9 +381,9 @@
   moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime)
     by (rule normalize_coprime) simp
   ultimately have "?Fract \<and> ?denom_pos \<and> ?coprime" by blast
-  with quotient_of_unique
-  have "(THE p. Fract a b = Fract (fst p) (snd p) \<and> 0 < snd p \<and>
-    coprime (fst p) (snd p)) = normalize (a, b)" by (rule the1_equality)
+  then have "(THE p. Fract a b = Fract (fst p) (snd p) \<and> 0 < snd p \<and>
+    coprime (fst p) (snd p)) = normalize (a, b)"
+    by (rule the1_equality [OF quotient_of_unique])
   then show ?thesis by (simp add: quotient_of_def)
 qed