--- 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)"
--- 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
--- 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)
--- 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:
--- 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)
--- 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)
--- 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))"
--- 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
--- 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)"
--- 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)
--- 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"}.
--- 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)
--- 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)
--- 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> _, _})")
--- 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)
--- 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)