more symbols;
authorwenzelm
Fri Sep 16 21:28:09 2016 +0200 (2016-09-16)
changeset 639014ce989e962e0
parent 63899 dc036b1a2a6f
child 63902 f83ef97d8d7d
more symbols;
src/FOL/IFOL.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/List.thy
src/HOL/Matrix_LP/ComputeFloat.thy
src/HOL/Nonstandard_Analysis/NSA.thy
src/HOL/Nonstandard_Analysis/NSCA.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
src/HOL/ZF/HOLZF.thy
src/HOL/ex/Refute_Examples.thy
src/ZF/Epsilon.thy
src/ZF/Order.thy
src/ZF/Perm.thy
src/ZF/ZF.thy
src/ZF/func.thy
src/ZF/upair.thy
     1.1 --- a/src/FOL/IFOL.thy	Fri Sep 16 18:09:13 2016 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Fri Sep 16 21:28:09 2016 +0200
     1.3 @@ -275,10 +275,10 @@
     1.4  text \<open>
     1.5    NOTE THAT the following 2 quantifications:
     1.6  
     1.7 -    \<^item> EX!x such that [EX!y such that P(x,y)]     (sequential)
     1.8 -    \<^item> EX!x,y such that P(x,y)                    (simultaneous)
     1.9 +    \<^item> \<exists>!x such that [\<exists>!y such that P(x,y)]     (sequential)
    1.10 +    \<^item> \<exists>!x,y such that P(x,y)                   (simultaneous)
    1.11  
    1.12 -  do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential.
    1.13 +  do NOT mean the same thing. The parser treats \<exists>!x y.P(x,y) as sequential.
    1.14  \<close>
    1.15  
    1.16  lemma ex1I: "P(a) \<Longrightarrow> (\<And>x. P(x) \<Longrightarrow> x = a) \<Longrightarrow> \<exists>!x. P(x)"
     2.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Sep 16 18:09:13 2016 +0200
     2.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Sep 16 21:28:09 2016 +0200
     2.3 @@ -1429,7 +1429,7 @@
     2.4  
     2.5  theorem UP_universal_property:
     2.6    assumes S: "s \<in> carrier S"
     2.7 -  shows "EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
     2.8 +  shows "\<exists>!Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
     2.9      Phi (monom P \<one> 1) = s &
    2.10      (ALL r : carrier R. Phi (monom P r 0) = h r)"
    2.11    using S eval_monom1
     3.1 --- a/src/HOL/List.thy	Fri Sep 16 18:09:13 2016 +0200
     3.2 +++ b/src/HOL/List.thy	Fri Sep 16 21:28:09 2016 +0200
     3.3 @@ -4913,7 +4913,7 @@
     3.4  qed
     3.5  
     3.6  lemma finite_sorted_distinct_unique:
     3.7 -shows "finite A \<Longrightarrow> EX! xs. set xs = A & sorted xs & distinct xs"
     3.8 +shows "finite A \<Longrightarrow> \<exists>!xs. set xs = A \<and> sorted xs \<and> distinct xs"
     3.9  apply(drule finite_distinct_list)
    3.10  apply clarify
    3.11  apply(rule_tac a="sort xs" in ex1I)
     4.1 --- a/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Sep 16 18:09:13 2016 +0200
     4.2 +++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Fri Sep 16 21:28:09 2016 +0200
     4.3 @@ -46,7 +46,7 @@
     4.4  apply (simp add: int_of_real_sub real_int_of_real)
     4.5  done
     4.6  
     4.7 -lemma real_is_int_rep: "real_is_int x \<Longrightarrow> ?! (a::int). real_of_int a = x"
     4.8 +lemma real_is_int_rep: "real_is_int x \<Longrightarrow> \<exists>!(a::int). real_of_int a = x"
     4.9  by (auto simp add: real_is_int_def)
    4.10  
    4.11  lemma int_of_real_mult:
     5.1 --- a/src/HOL/Nonstandard_Analysis/NSA.thy	Fri Sep 16 18:09:13 2016 +0200
     5.2 +++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Fri Sep 16 21:28:09 2016 +0200
     5.3 @@ -1268,7 +1268,7 @@
     5.4  done
     5.5  
     5.6  text\<open>There is a unique real infinitely close\<close>
     5.7 -lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> \<real> & x \<approx> t"
     5.8 +lemma st_part_Ex1: "x \<in> HFinite ==> \<exists>!t::hypreal. t \<in> \<real> & x \<approx> t"
     5.9  apply (drule st_part_Ex, safe)
    5.10  apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
    5.11  apply (auto intro!: approx_unique_real)
     6.1 --- a/src/HOL/Nonstandard_Analysis/NSCA.thy	Fri Sep 16 18:09:13 2016 +0200
     6.2 +++ b/src/HOL/Nonstandard_Analysis/NSCA.thy	Fri Sep 16 21:28:09 2016 +0200
     6.3 @@ -350,7 +350,7 @@
     6.4  apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard])
     6.5  done
     6.6  
     6.7 -lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex &  x \<approx> t"
     6.8 +lemma stc_part_Ex1: "x:HFinite ==> \<exists>!t. t \<in> SComplex &  x \<approx> t"
     6.9  apply (drule stc_part_Ex, safe)
    6.10  apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
    6.11  apply (auto intro!: approx_unique_complex)
     7.1 --- a/src/HOL/Number_Theory/Cong.thy	Fri Sep 16 18:09:13 2016 +0200
     7.2 +++ b/src/HOL/Number_Theory/Cong.thy	Fri Sep 16 21:28:09 2016 +0200
     7.3 @@ -698,7 +698,7 @@
     7.4  lemma binary_chinese_remainder_unique_nat:
     7.5    assumes a: "coprime (m1::nat) m2"
     7.6      and nz: "m1 \<noteq> 0" "m2 \<noteq> 0"
     7.7 -  shows "EX! x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
     7.8 +  shows "\<exists>!x. x < m1 * m2 \<and> [x = u1] (mod m1) \<and> [x = u2] (mod m2)"
     7.9  proof -
    7.10    from binary_chinese_remainder_nat [OF a] obtain y where
    7.11        "[y = u1] (mod m1)" and "[y = u2] (mod m2)"
    7.12 @@ -834,7 +834,7 @@
    7.13    assumes fin: "finite A"
    7.14      and nz: "\<forall>i\<in>A. m i \<noteq> 0"
    7.15      and cop: "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
    7.16 -  shows "EX! x. x < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))"
    7.17 +  shows "\<exists>!x. x < (\<Prod>i\<in>A. m i) \<and> (\<forall>i\<in>A. [x = u i] (mod m i))"
    7.18  proof -
    7.19    from chinese_remainder_nat [OF fin cop]
    7.20    obtain y where one: "(ALL i:A. [y = u i] (mod m i))"
     8.1 --- a/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Fri Sep 16 18:09:13 2016 +0200
     8.2 +++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy	Fri Sep 16 21:28:09 2016 +0200
     8.3 @@ -270,7 +270,7 @@
     8.4    quickcheck[expect = counterexample]
     8.5  oops
     8.6  
     8.7 -lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
     8.8 +lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
     8.9    quickcheck[random, expect = counterexample]
    8.10    quickcheck[expect = counterexample]
    8.11  oops
     9.1 --- a/src/HOL/ZF/HOLZF.thy	Fri Sep 16 18:09:13 2016 +0200
     9.2 +++ b/src/HOL/ZF/HOLZF.thy	Fri Sep 16 21:28:09 2016 +0200
     9.3 @@ -270,7 +270,7 @@
     9.4    by (auto simp add: Fun_def Sep Domain)
     9.5  
     9.6  
     9.7 -lemma unique_fun_value: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> ?! y. Elem (Opair x y) f"
     9.8 +lemma unique_fun_value: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> \<exists>!y. Elem (Opair x y) f"
     9.9    by (auto simp add: Domain isFun_def)
    9.10  
    9.11  lemma fun_value_in_range: "\<lbrakk>isFun f; Elem x (Domain f)\<rbrakk> \<Longrightarrow> Elem (f\<acute>x) (Range f)"
    10.1 --- a/src/HOL/ex/Refute_Examples.thy	Fri Sep 16 18:09:13 2016 +0200
    10.2 +++ b/src/HOL/ex/Refute_Examples.thy	Fri Sep 16 21:28:09 2016 +0200
    10.3 @@ -128,7 +128,7 @@
    10.4  refute [expect = genuine]
    10.5  oops
    10.6  
    10.7 -lemma "EX! x. P x"
    10.8 +lemma "\<exists>!x. P x"
    10.9  refute [expect = genuine]
   10.10  oops
   10.11  
   10.12 @@ -152,7 +152,7 @@
   10.13  refute [expect = genuine]
   10.14  oops
   10.15  
   10.16 -lemma "(\<exists>x. P x) \<longrightarrow> (EX! x. P x)"
   10.17 +lemma "(\<exists>x. P x) \<longrightarrow> (\<exists>!x. P x)"
   10.18  refute [expect = genuine]
   10.19  oops
   10.20  
   10.21 @@ -220,11 +220,11 @@
   10.22  refute [expect = genuine]
   10.23  oops
   10.24  
   10.25 -lemma "EX! P. P"
   10.26 +lemma "\<exists>!P. P"
   10.27  refute [expect = none]
   10.28  by auto
   10.29  
   10.30 -lemma "EX! P. P x"
   10.31 +lemma "\<exists>!P. P x"
   10.32  refute [expect = genuine]
   10.33  oops
   10.34  
   10.35 @@ -280,7 +280,7 @@
   10.36  
   10.37  text \<open>Axiom of Choice: first an incorrect version ...\<close>
   10.38  
   10.39 -lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
   10.40 +lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
   10.41  refute [expect = genuine]
   10.42  oops
   10.43  
   10.44 @@ -290,7 +290,7 @@
   10.45  refute [maxsize = 4, expect = none]
   10.46  by (simp add: choice)
   10.47  
   10.48 -lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
   10.49 +lemma "(\<forall>x. \<exists>!y. P x y) \<longrightarrow> (\<exists>!f. \<forall>x. P x (f x))"
   10.50  refute [maxsize = 2, expect = none]
   10.51  apply auto
   10.52    apply (simp add: ex1_implies_ex choice)
    11.1 --- a/src/ZF/Epsilon.thy	Fri Sep 16 18:09:13 2016 +0200
    11.2 +++ b/src/ZF/Epsilon.thy	Fri Sep 16 21:28:09 2016 +0200
    11.3 @@ -305,7 +305,7 @@
    11.4  (*Not clear how to remove the P(a) condition, since the "then" part
    11.5    must refer to "a"*)
    11.6  lemma the_equality_if:
    11.7 -     "P(a) ==> (THE x. P(x)) = (if (EX!x. P(x)) then a else 0)"
    11.8 +     "P(a) ==> (THE x. P(x)) = (if (\<exists>!x. P(x)) then a else 0)"
    11.9  by (simp add: the_0 the_equality2)
   11.10  
   11.11  (*The first premise not only fixs i but ensures @{term"f\<noteq>0"}.
    12.1 --- a/src/ZF/Order.thy	Fri Sep 16 18:09:13 2016 +0200
    12.2 +++ b/src/ZF/Order.thy	Fri Sep 16 21:28:09 2016 +0200
    12.3 @@ -641,7 +641,7 @@
    12.4  by (unfold first_def, blast)
    12.5  
    12.6  lemma well_ord_imp_ex1_first:
    12.7 -        "[| well_ord(A,r); B<=A; B\<noteq>0 |] ==> (EX! b. first(b,B,r))"
    12.8 +        "[| well_ord(A,r); B<=A; B\<noteq>0 |] ==> (\<exists>!b. first(b,B,r))"
    12.9  apply (unfold well_ord_def wf_on_def wf_def first_def)
   12.10  apply (elim conjE allE disjE, blast)
   12.11  apply (erule bexE)
    13.1 --- a/src/ZF/Perm.thy	Fri Sep 16 18:09:13 2016 +0200
    13.2 +++ b/src/ZF/Perm.thy	Fri Sep 16 21:28:09 2016 +0200
    13.3 @@ -137,7 +137,7 @@
    13.4  apply (blast intro!: lam_injective lam_surjective)
    13.5  done
    13.6  
    13.7 -lemma RepFun_bijective: "(\<forall>y\<in>x. EX! y'. f(y') = f(y))
    13.8 +lemma RepFun_bijective: "(\<forall>y\<in>x. \<exists>!y'. f(y') = f(y))
    13.9        ==> (\<lambda>z\<in>{f(y). y \<in> x}. THE y. f(y) = z) \<in> bij({f(y). y \<in> x}, x)"
   13.10  apply (rule_tac d = f in lam_bijective)
   13.11  apply (auto simp add: the_equality2)
    14.1 --- a/src/ZF/ZF.thy	Fri Sep 16 18:09:13 2016 +0200
    14.2 +++ b/src/ZF/ZF.thy	Fri Sep 16 21:28:09 2016 +0200
    14.3 @@ -49,7 +49,7 @@
    14.4     The resulting set (for functional P) is the same as with
    14.5     PrimReplace, but the rules are simpler. *)
    14.6  definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
    14.7 -  where "Replace(A,P) == PrimReplace(A, %x y. (EX!z. P(x,z)) & P(x,y))"
    14.8 +  where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))"
    14.9  
   14.10  syntax
   14.11    "_Replace"  :: "[pttrn, pttrn, i, o] => i"  ("(1{_ ./ _ \<in> _, _})")
    15.1 --- a/src/ZF/func.thy	Fri Sep 16 18:09:13 2016 +0200
    15.2 +++ b/src/ZF/func.thy	Fri Sep 16 21:28:09 2016 +0200
    15.3 @@ -25,7 +25,7 @@
    15.4  
    15.5  (*For upward compatibility with the former definition*)
    15.6  lemma Pi_iff_old:
    15.7 -    "f \<in> Pi(A,B) \<longleftrightarrow> f<=Sigma(A,B) & (\<forall>x\<in>A. EX! y. <x,y>: f)"
    15.8 +    "f \<in> Pi(A,B) \<longleftrightarrow> f<=Sigma(A,B) & (\<forall>x\<in>A. \<exists>!y. <x,y>: f)"
    15.9  by (unfold Pi_def function_def, blast)
   15.10  
   15.11  lemma fun_is_function: "f \<in> Pi(A,B) ==> function(f)"
   15.12 @@ -175,7 +175,7 @@
   15.13  by (simp only: lam_def cong add: RepFun_cong)
   15.14  
   15.15  lemma lam_theI:
   15.16 -    "(!!x. x \<in> A ==> EX! y. Q(x,y)) ==> \<exists>f. \<forall>x\<in>A. Q(x, f`x)"
   15.17 +    "(!!x. x \<in> A ==> \<exists>!y. Q(x,y)) ==> \<exists>f. \<forall>x\<in>A. Q(x, f`x)"
   15.18  apply (rule_tac x = "\<lambda>x\<in>A. THE y. Q (x,y)" in exI)
   15.19  apply simp
   15.20  apply (blast intro: theI)
    16.1 --- a/src/ZF/upair.thy	Fri Sep 16 18:09:13 2016 +0200
    16.2 +++ b/src/ZF/upair.thy	Fri Sep 16 21:28:09 2016 +0200
    16.3 @@ -156,11 +156,11 @@
    16.4  apply (fast dest: subst)
    16.5  done
    16.6  
    16.7 -(* Only use this if you already know EX!x. P(x) *)
    16.8 -lemma the_equality2: "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
    16.9 +(* Only use this if you already know \<exists>!x. P(x) *)
   16.10 +lemma the_equality2: "[| \<exists>!x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
   16.11  by blast
   16.12  
   16.13 -lemma theI: "EX! x. P(x) ==> P(THE x. P(x))"
   16.14 +lemma theI: "\<exists>!x. P(x) ==> P(THE x. P(x))"
   16.15  apply (erule ex1E)
   16.16  apply (subst the_equality)
   16.17  apply (blast+)
   16.18 @@ -170,14 +170,14 @@
   16.19    @{term "THE x.P(x)"}  rewrites to @{term "THE x.Q(x)"} *)
   16.20  
   16.21  (*If it's "undefined", it's zero!*)
   16.22 -lemma the_0: "~ (EX! x. P(x)) ==> (THE x. P(x))=0"
   16.23 +lemma the_0: "~ (\<exists>!x. P(x)) ==> (THE x. P(x))=0"
   16.24  apply (unfold the_def)
   16.25  apply (blast elim!: ReplaceE)
   16.26  done
   16.27  
   16.28  (*Easier to apply than theI: conclusion has only one occurrence of P*)
   16.29  lemma theI2:
   16.30 -    assumes p1: "~ Q(0) ==> EX! x. P(x)"
   16.31 +    assumes p1: "~ Q(0) ==> \<exists>!x. P(x)"
   16.32          and p2: "!!x. P(x) ==> Q(x)"
   16.33      shows "Q(THE x. P(x))"
   16.34  apply (rule classical)