--- 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
--- 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>
--- 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"
--- 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