# HG changeset patch
# User wenzelm
# Date 1474054089 -7200
# Node ID 4ce989e962e0749a402491d8378c05d08f8316df
# Parent  dc036b1a2a6f22d68bcbc5ec5ccae37f66f77b77
more symbols;

diff -r dc036b1a2a6f -r 4ce989e962e0 src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/FOL/IFOL.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -275,10 +275,10 @@
 text \<open>
   NOTE THAT the following 2 quantifications:
 
-    \<^item> EX!x such that [EX!y such that P(x,y)]     (sequential)
-    \<^item> EX!x,y such that P(x,y)                    (simultaneous)
+    \<^item> \<exists>!x such that [\<exists>!y such that P(x,y)]     (sequential)
+    \<^item> \<exists>!x,y such that P(x,y)                   (simultaneous)
 
-  do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential.
+  do NOT mean the same thing. The parser treats \<exists>!x y.P(x,y) as sequential.
 \<close>
 
 lemma ex1I: "P(a) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> x = a) \<Longrightarrow> \<exists>!x. P(x)"
diff -r dc036b1a2a6f -r 4ce989e962e0 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -1429,7 +1429,7 @@
 
 theorem UP_universal_property:
   assumes S: "s \<in> carrier S"
-  shows "EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
+  shows "\<exists>!Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
     Phi (monom P \<one> 1) = s &
     (ALL r : carrier R. Phi (monom P r 0) = h r)"
   using S eval_monom1
diff -r dc036b1a2a6f -r 4ce989e962e0 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/HOL/List.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -4913,7 +4913,7 @@
 qed
 
 lemma finite_sorted_distinct_unique:
-shows "finite A \<Longrightarrow> EX! xs. set xs = A & sorted xs & distinct xs"
+shows "finite A \<Longrightarrow> \<exists>!xs. set xs = A \<and> sorted xs \<and> distinct xs"
 apply(drule finite_distinct_list)
 apply clarify
 apply(rule_tac a="sort xs" in ex1I)
diff -r dc036b1a2a6f -r 4ce989e962e0 src/HOL/Matrix_LP/ComputeFloat.thy
--- a/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -46,7 +46,7 @@
 apply (simp add: int_of_real_sub real_int_of_real)
 done
 
-lemma real_is_int_rep: "real_is_int x \<Longrightarrow> ?! (a::int). real_of_int a = x"
+lemma real_is_int_rep: "real_is_int x \<Longrightarrow> \<exists>!(a::int). real_of_int a = x"
 by (auto simp add: real_is_int_def)
 
 lemma int_of_real_mult:
diff -r dc036b1a2a6f -r 4ce989e962e0 src/HOL/Nonstandard_Analysis/NSA.thy
--- a/src/HOL/Nonstandard_Analysis/NSA.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -1268,7 +1268,7 @@
 done
 
 text\<open>There is a unique real infinitely close\<close>
-lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> \<real> & x \<approx> t"
+lemma st_part_Ex1: "x \<in> HFinite ==> \<exists>!t::hypreal. t \<in> \<real> & x \<approx> t"
 apply (drule st_part_Ex, safe)
 apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
 apply (auto intro!: approx_unique_real)
diff -r dc036b1a2a6f -r 4ce989e962e0 src/HOL/Nonstandard_Analysis/NSCA.thy
--- a/src/HOL/Nonstandard_Analysis/NSCA.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSCA.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -350,7 +350,7 @@
 apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard])
 done
 
-lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex &  x \<approx> t"
+lemma stc_part_Ex1: "x:HFinite ==> \<exists>!t. t \<in> SComplex &  x \<approx> t"
 apply (drule stc_part_Ex, safe)
 apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
 apply (auto intro!: approx_unique_complex)
diff -r dc036b1a2a6f -r 4ce989e962e0 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -698,7 +698,7 @@
 lemma binary_chinese_remainder_unique_nat:
   assumes a: "coprime (m1::nat) m2"
     and nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
-  shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
+  shows "\<exists>!x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
 proof -
   from binary_chinese_remainder_nat [OF a] obtain y where
       "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
@@ -834,7 +834,7 @@
   assumes fin: "finite A"
     and nz: "\<forall>i\<in>A. m i \<noteq> 0"
     and cop: "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
-  shows "EX! x. x < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))"
+  shows "\<exists>!x. x < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))"
 proof -
   from chinese_remainder_nat [OF fin cop]
   obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
diff -r dc036b1a2a6f -r 4ce989e962e0 src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
--- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -270,7 +270,7 @@
   quickcheck[expect = counterexample]
 oops
 
-lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
+lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
   quickcheck[random, expect = counterexample]
   quickcheck[expect = counterexample]
 oops
diff -r dc036b1a2a6f -r 4ce989e962e0 src/HOL/ZF/HOLZF.thy
--- a/src/HOL/ZF/HOLZF.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/HOL/ZF/HOLZF.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -270,7 +270,7 @@
   by (auto simp add: Fun_def Sep Domain)
 
 
-lemma unique_fun_value: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> ?! y. Elem (Opair x y) f"
+lemma unique_fun_value: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> \<exists>!y. Elem (Opair x y) f"
   by (auto simp add: Domain isFun_def)
 
 lemma fun_value_in_range: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> Elem (f\<acute>x) (Range f)"
diff -r dc036b1a2a6f -r 4ce989e962e0 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -128,7 +128,7 @@
 refute [expect = genuine]
 oops
 
-lemma "EX! x. P x"
+lemma "\<exists>!x. P x"
 refute [expect = genuine]
 oops
 
@@ -152,7 +152,7 @@
 refute [expect = genuine]
 oops
 
-lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
+lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
 refute [expect = genuine]
 oops
 
@@ -220,11 +220,11 @@
 refute [expect = genuine]
 oops
 
-lemma "EX! P. P"
+lemma "\<exists>!P. P"
 refute [expect = none]
 by auto
 
-lemma "EX! P. P x"
+lemma "\<exists>!P. P x"
 refute [expect = genuine]
 oops
 
@@ -280,7 +280,7 @@
 
 text \<open>Axiom of Choice: first an incorrect version ...\<close>
 
-lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
+lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
 refute [expect = genuine]
 oops
 
@@ -290,7 +290,7 @@
 refute [maxsize = 4, expect = none]
 by (simp add: choice)
 
-lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
+lemma "(\<forall>x. \<exists>!y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
 refute [maxsize = 2, expect = none]
 apply auto
   apply (simp add: ex1_implies_ex choice)
diff -r dc036b1a2a6f -r 4ce989e962e0 src/ZF/Epsilon.thy
--- a/src/ZF/Epsilon.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/ZF/Epsilon.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -305,7 +305,7 @@
 (*Not clear how to remove the P(a) condition, since the "then" part
   must refer to "a"*)
 lemma the_equality_if:
-     "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)"
+     "P(a) ==> (THE x. P(x)) = (if (\<exists>!x. P(x)) then a else 0)"
 by (simp add: the_0 the_equality2)
 
 (*The first premise not only fixs i but ensures @{term"f\<noteq>0"}.
diff -r dc036b1a2a6f -r 4ce989e962e0 src/ZF/Order.thy
--- a/src/ZF/Order.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/ZF/Order.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -641,7 +641,7 @@
 by (unfold first_def, blast)
 
 lemma well_ord_imp_ex1_first:
-        "[| well_ord(A,r); B<=A; B\<noteq>0 |] ==> (EX! b. first(b,B,r))"
+        "[| well_ord(A,r); B<=A; B\<noteq>0 |] ==> (\<exists>!b. first(b,B,r))"
 apply (unfold well_ord_def wf_on_def wf_def first_def)
 apply (elim conjE allE disjE, blast)
 apply (erule bexE)
diff -r dc036b1a2a6f -r 4ce989e962e0 src/ZF/Perm.thy
--- a/src/ZF/Perm.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/ZF/Perm.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -137,7 +137,7 @@
 apply (blast intro!: lam_injective lam_surjective)
 done
 
-lemma RepFun_bijective: "(\<forall>y\<in>x. EX! y'. f(y') = f(y))
+lemma RepFun_bijective: "(\<forall>y\<in>x. \<exists>!y'. f(y') = f(y))
       ==> (\<lambda>z\<in>{f(y). y \<in> x}. THE y. f(y) = z) \<in> bij({f(y). y \<in> x}, x)"
 apply (rule_tac d = f in lam_bijective)
 apply (auto simp add: the_equality2)
diff -r dc036b1a2a6f -r 4ce989e962e0 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/ZF/ZF.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -49,7 +49,7 @@
    The resulting set (for functional P) is the same as with
    PrimReplace, but the rules are simpler. *)
 definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
-  where "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
+  where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))"
 
 syntax
   "_Replace"  :: "[pttrn, pttrn, i, o] => i"  ("(1{_ ./ _ \<in> _, _})")
diff -r dc036b1a2a6f -r 4ce989e962e0 src/ZF/func.thy
--- a/src/ZF/func.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/ZF/func.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -25,7 +25,7 @@
 
 (*For upward compatibility with the former definition*)
 lemma Pi_iff_old:
-    "f \<in> Pi(A,B) \<longleftrightarrow> f<=Sigma(A,B) & (\<forall>x\<in>A. EX! y. <x,y>: f)"
+    "f \<in> Pi(A,B) \<longleftrightarrow> f<=Sigma(A,B) & (\<forall>x\<in>A. \<exists>!y. <x,y>: f)"
 by (unfold Pi_def function_def, blast)
 
 lemma fun_is_function: "f \<in> Pi(A,B) ==> function(f)"
@@ -175,7 +175,7 @@
 by (simp only: lam_def cong add: RepFun_cong)
 
 lemma lam_theI:
-    "(!!x. x \<in> A ==> EX! y. Q(x,y)) ==> \<exists>f. \<forall>x\<in>A. Q(x, f`x)"
+    "(!!x. x \<in> A ==> \<exists>!y. Q(x,y)) ==> \<exists>f. \<forall>x\<in>A. Q(x, f`x)"
 apply (rule_tac x = "\<lambda>x\<in>A. THE y. Q (x,y)" in exI)
 apply simp
 apply (blast intro: theI)
diff -r dc036b1a2a6f -r 4ce989e962e0 src/ZF/upair.thy
--- a/src/ZF/upair.thy	Fri Sep 16 18:09:13 2016 +0200
+++ b/src/ZF/upair.thy	Fri Sep 16 21:28:09 2016 +0200
@@ -156,11 +156,11 @@
 apply (fast dest: subst)
 done
 
-(* Only use this if you already know EX!x. P(x) *)
-lemma the_equality2: "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
+(* Only use this if you already know \<exists>!x. P(x) *)
+lemma the_equality2: "[| \<exists>!x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
 by blast
 
-lemma theI: "EX! x. P(x) ==> P(THE x. P(x))"
+lemma theI: "\<exists>!x. P(x) ==> P(THE x. P(x))"
 apply (erule ex1E)
 apply (subst the_equality)
 apply (blast+)
@@ -170,14 +170,14 @@
   @{term "THE x.P(x)"}  rewrites to @{term "THE x.Q(x)"} *)
 
 (*If it's "undefined", it's zero!*)
-lemma the_0: "~ (EX! x. P(x)) ==> (THE x. P(x))=0"
+lemma the_0: "~ (\<exists>!x. P(x)) ==> (THE x. P(x))=0"
 apply (unfold the_def)
 apply (blast elim!: ReplaceE)
 done
 
 (*Easier to apply than theI: conclusion has only one occurrence of P*)
 lemma theI2:
-    assumes p1: "~ Q(0) ==> EX! x. P(x)"
+    assumes p1: "~ Q(0) ==> \<exists>!x. P(x)"
         and p2: "!!x. P(x) ==> Q(x)"
     shows "Q(THE x. P(x))"
 apply (rule classical)