merged
authorLars Hupel <lars.hupel@mytum.de>
Sun Sep 18 18:36:37 2016 +0200 (2016-09-18)
changeset 63914255294779d40
parent 63913 6b886cadba7c
parent 63912 9f8325206465
child 63916 5e816da75b8f
merged
     1.1 --- a/NEWS	Sun Sep 18 18:23:59 2016 +0200
     1.2 +++ b/NEWS	Sun Sep 18 18:36:37 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 18:23:59 2016 +0200
     2.2 +++ b/src/HOL/HOL.thy	Sun Sep 18 18:36:37 2016 +0200
     2.3 @@ -99,17 +99,31 @@
     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 -abbreviation Not_Ex :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<nexists>" 10)
    2.15 -  where "\<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)"
    2.16 +syntax (ASCII)
    2.17 +  "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3EX! _./ _)" [0, 10] 10)
    2.18 +syntax (input)
    2.19 +  "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3?! _./ _)" [0, 10] 10)
    2.20 +syntax "_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<exists>!_./ _)" [0, 10] 10)
    2.21 +translations "\<exists>!x. P" \<rightleftharpoons> "CONST Ex1 (\<lambda>x. P)"
    2.22  
    2.23 -abbreviation Not_Ex1 :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<nexists>!" 10)
    2.24 -  where "\<nexists>!x. P x \<equiv> \<not> (\<exists>!x. P x)"
    2.25 +print_translation \<open>
    2.26 + [Syntax_Trans.preserve_binder_abs_tr' @{const_syntax Ex1} @{syntax_const "_Ex1"}]
    2.27 +\<close> \<comment> \<open>to avoid eta-contraction of body\<close>
    2.28 +
    2.29 +
    2.30 +syntax
    2.31 +  "_Not_Ex" :: "idts \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>_./ _)" [0, 10] 10)
    2.32 +  "_Not_Ex1" :: "pttrn \<Rightarrow> bool \<Rightarrow> bool"  ("(3\<nexists>!_./ _)" [0, 10] 10)
    2.33 +translations
    2.34 +  "\<nexists>x. P" \<rightleftharpoons> "\<not> (\<exists>x. P)"
    2.35 +  "\<nexists>!x. P" \<rightleftharpoons> "\<not> (\<exists>!x. P)"
    2.36 +
    2.37  
    2.38  abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool"  (infixl "\<noteq>" 50)
    2.39    where "x \<noteq> y \<equiv> \<not> (x = y)"
    2.40 @@ -158,13 +172,11 @@
    2.41  
    2.42  notation (ASCII)
    2.43    All  (binder "ALL " 10) and
    2.44 -  Ex  (binder "EX " 10) and
    2.45 -  Ex1  (binder "EX! " 10)
    2.46 +  Ex  (binder "EX " 10)
    2.47  
    2.48  notation (input)
    2.49    All  (binder "! " 10) and
    2.50 -  Ex  (binder "? " 10) and
    2.51 -  Ex1  (binder "?! " 10)
    2.52 +  Ex  (binder "? " 10)
    2.53  
    2.54  
    2.55  subsubsection \<open>Axioms and basic definitions\<close>
     3.1 --- a/src/HOL/Hahn_Banach/Subspace.thy	Sun Sep 18 18:23:59 2016 +0200
     3.2 +++ b/src/HOL/Hahn_Banach/Subspace.thy	Sun Sep 18 18:36:37 2016 +0200
     3.3 @@ -479,7 +479,7 @@
     3.4    interpret vectorspace E by fact
     3.5    interpret subspace H E by fact
     3.6    from x y x' have "x \<in> H + lin x'" by auto
     3.7 -  have "\<exists>!p. (\<lambda>(y, a). x = y + a \<cdot> x' \<and> y \<in> H) p" (is "\<exists>!p. ?P p")
     3.8 +  have "\<exists>!(y, a). x = y + a \<cdot> x' \<and> y \<in> H" (is "\<exists>!p. ?P p")
     3.9    proof (rule ex_ex1I)
    3.10      from x y show "\<exists>p. ?P p" by blast
    3.11      fix p q assume p: "?P p" and q: "?P q"
     4.1 --- a/src/HOL/Rat.thy	Sun Sep 18 18:23:59 2016 +0200
     4.2 +++ b/src/HOL/Rat.thy	Sun Sep 18 18:36:37 2016 +0200
     4.3 @@ -339,12 +339,11 @@
     4.4    then show ?thesis
     4.5    proof (rule ex1I)
     4.6      fix p
     4.7 -    obtain c d :: int where p: "p = (c, d)"
     4.8 -      by (cases p)
     4.9 -    assume "r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)"
    4.10 -    with p have Fract': "r = Fract c d" "d > 0" "coprime c d"
    4.11 +    assume r: "r = Fract (fst p) (snd p) \<and> snd p > 0 \<and> coprime (fst p) (snd p)"
    4.12 +    obtain c d where p: "p = (c, d)" by (cases p)
    4.13 +    with r have Fract': "r = Fract c d" "d > 0" "coprime c d"
    4.14        by simp_all
    4.15 -    have "c = a \<and> d = b"
    4.16 +    have "(c, d) = (a, b)"
    4.17      proof (cases "a = 0")
    4.18        case True
    4.19        with Fract Fract' show ?thesis
    4.20 @@ -382,9 +381,9 @@
    4.21    moreover have "coprime (fst (normalize (a, b))) (snd (normalize (a, b)))" (is ?coprime)
    4.22      by (rule normalize_coprime) simp
    4.23    ultimately have "?Fract \<and> ?denom_pos \<and> ?coprime" by blast
    4.24 -  with quotient_of_unique
    4.25 -  have "(THE p. Fract a b = Fract (fst p) (snd p) \<and> 0 < snd p \<and>
    4.26 -    coprime (fst p) (snd p)) = normalize (a, b)" by (rule the1_equality)
    4.27 +  then have "(THE p. Fract a b = Fract (fst p) (snd p) \<and> 0 < snd p \<and>
    4.28 +    coprime (fst p) (snd p)) = normalize (a, b)"
    4.29 +    by (rule the1_equality [OF quotient_of_unique])
    4.30    then show ?thesis by (simp add: quotient_of_def)
    4.31  qed
    4.32