--- a/src/Doc/Main/Main_Doc.thy Fri Sep 16 18:44:18 2016 +0200
+++ b/src/Doc/Main/Main_Doc.thy Fri Sep 16 21:40:47 2016 +0200
@@ -31,7 +31,9 @@
\section*{HOL}
-The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop"Not P"}, @{prop"P & Q"}, @{prop "P | Q"}, @{prop "P --> Q"}, @{prop"ALL x. P"}, @{prop"EX x. P"}, @{prop"EX! x. P"}, @{term"THE x. P"}.
+The basic logic: @{prop "x = y"}, @{const True}, @{const False}, @{prop "\<not> P"}, @{prop"P \<and> Q"},
+@{prop "P \<or> Q"}, @{prop "P \<longrightarrow> Q"}, @{prop "\<forall>x. P"}, @{prop "\<exists>x. P"}, @{prop"\<exists>! x. P"},
+@{term"THE x. P"}.
\<^smallskip>
\begin{tabular}{@ {} l @ {~::~} l @ {}}
@@ -42,10 +44,10 @@
\subsubsection*{Syntax}
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
-@{term"~(x = y)"} & @{term[source]"\<not> (x = y)"} & (\<^verbatim>\<open>~=\<close>)\\
+@{term"\<not> (x = y)"} & @{term[source]"\<not> (x = y)"} & (\<^verbatim>\<open>~=\<close>)\\
@{term[source]"P \<longleftrightarrow> Q"} & @{term"P \<longleftrightarrow> Q"} \\
@{term"If x y z"} & @{term[source]"If x y z"}\\
-@{term"Let e\<^sub>1 (%x. e\<^sub>2)"} & @{term[source]"Let e\<^sub>1 (\<lambda>x. e\<^sub>2)"}\\
+@{term"Let e\<^sub>1 (\<lambda>x. e\<^sub>2)"} & @{term[source]"Let e\<^sub>1 (\<lambda>x. e\<^sub>2)"}\\
\end{supertabular}
@@ -72,10 +74,10 @@
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
@{term[source]"x \<ge> y"} & @{term"x \<ge> y"} & (\<^verbatim>\<open>>=\<close>)\\
@{term[source]"x > y"} & @{term"x > y"}\\
-@{term"ALL x<=y. P"} & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\
-@{term"EX x<=y. P"} & @{term[source]"\<exists>x. x \<le> y \<and> P"}\\
+@{term "\<forall>x\<le>y. P"} & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\
+@{term "\<exists>x\<le>y. P"} & @{term[source]"\<exists>x. x \<le> y \<and> P"}\\
\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\
-@{term"LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\
+@{term "LEAST x. P"} & @{term[source]"Least (\<lambda>x. P)"}\\
\end{supertabular}
@@ -131,20 +133,20 @@
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
\<open>{a\<^sub>1,\<dots>,a\<^sub>n}\<close> & \<open>insert a\<^sub>1 (\<dots> (insert a\<^sub>n {})\<dots>)\<close>\\
-@{term"a ~: A"} & @{term[source]"\<not>(x \<in> A)"}\\
-@{term"A \<subseteq> B"} & @{term[source]"A \<le> B"}\\
-@{term"A \<subset> B"} & @{term[source]"A < B"}\\
+@{term "a \<notin> A"} & @{term[source]"\<not>(x \<in> A)"}\\
+@{term "A \<subseteq> B"} & @{term[source]"A \<le> B"}\\
+@{term "A \<subset> B"} & @{term[source]"A < B"}\\
@{term[source]"A \<supseteq> B"} & @{term[source]"B \<le> A"}\\
@{term[source]"A \<supset> B"} & @{term[source]"B < A"}\\
-@{term"{x. P}"} & @{term[source]"Collect (\<lambda>x. P)"}\\
+@{term "{x. P}"} & @{term[source]"Collect (\<lambda>x. P)"}\\
\<open>{t | x\<^sub>1 \<dots> x\<^sub>n. P}\<close> & \<open>{v. \<exists>x\<^sub>1 \<dots> x\<^sub>n. v = t \<and> P}\<close>\\
@{term[source]"\<Union>x\<in>I. A"} & @{term[source]"UNION I (\<lambda>x. A)"} & (\texttt{UN})\\
@{term[source]"\<Union>x. A"} & @{term[source]"UNION UNIV (\<lambda>x. A)"}\\
@{term[source]"\<Inter>x\<in>I. A"} & @{term[source]"INTER I (\<lambda>x. A)"} & (\texttt{INT})\\
@{term[source]"\<Inter>x. A"} & @{term[source]"INTER UNIV (\<lambda>x. A)"}\\
-@{term"ALL x:A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
-@{term"EX x:A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
-@{term"range f"} & @{term[source]"f ` UNIV"}\\
+@{term "\<forall>x\<in>A. P"} & @{term[source]"Ball A (\<lambda>x. P)"}\\
+@{term "\<exists>x\<in>A. P"} & @{term[source]"Bex A (\<lambda>x. P)"}\\
+@{term "range f"} & @{term[source]"f ` UNIV"}\\
\end{supertabular}
@@ -225,15 +227,15 @@
\subsubsection*{Syntax}
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
-@{term"Pair a b"} & @{term[source]"Pair a b"}\\
-@{term"case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\
-@{term"A \<times> B"} & \<open>Sigma A (\<lambda>\<^raw:\_>. B)\<close>
+@{term "Pair a b"} & @{term[source]"Pair a b"}\\
+@{term "case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\
+@{term "A \<times> B"} & \<open>Sigma A (\<lambda>\<^raw:\_>. B)\<close>
\end{tabular}
Pairs may be nested. Nesting to the right is printed as a tuple,
-e.g.\ \mbox{@{term"(a,b,c)"}} is really \mbox{\<open>(a, (b, c))\<close>.}
+e.g.\ \mbox{@{term "(a,b,c)"}} is really \mbox{\<open>(a, (b, c))\<close>.}
Pattern matching with pairs and tuples extends to all binders,
-e.g.\ \mbox{@{prop"ALL (x,y):A. P"},} @{term"{(x,y). P}"}, etc.
+e.g.\ \mbox{@{prop "\<forall>(x,y)\<in>A. P"},} @{term "{(x,y). P}"}, etc.
\section*{Relation}
@@ -331,7 +333,7 @@
\subsubsection*{Syntax}
\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
-@{term"abs x"} & @{term[source]"abs x"}
+@{term "\<bar>x\<bar>"} & @{term[source] "abs x"}
\end{tabular}
@@ -404,19 +406,19 @@
\begin{supertabular}{@ {} l @ {~::~} l @ {}}
@{const Finite_Set.finite} & @{term_type_only Finite_Set.finite "'a set\<Rightarrow>bool"}\\
-@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set => nat"}\\
+@{const Finite_Set.card} & @{term_type_only Finite_Set.card "'a set \<Rightarrow> nat"}\\
@{const Finite_Set.fold} & @{term_type_only Finite_Set.fold "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\
-@{const Groups_Big.setsum} & @{term_type_only Groups_Big.setsum "('a => 'b) => 'a set => 'b::comm_monoid_add"}\\
-@{const Groups_Big.setprod} & @{term_type_only Groups_Big.setprod "('a => 'b) => 'a set => 'b::comm_monoid_mult"}\\
+@{const Groups_Big.setsum} & @{term_type_only Groups_Big.setsum "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_add"}\\
+@{const Groups_Big.setprod} & @{term_type_only Groups_Big.setprod "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_mult"}\\
\end{supertabular}
\subsubsection*{Syntax}
\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
-@{term"setsum (%x. x) A"} & @{term[source]"setsum (\<lambda>x. x) A"} & (\<^verbatim>\<open>SUM\<close>)\\
-@{term"setsum (%x. t) A"} & @{term[source]"setsum (\<lambda>x. t) A"}\\
-@{term[source]"\<Sum>x|P. t"} & @{term"\<Sum>x|P. t"}\\
+@{term "setsum (\<lambda>x. x) A"} & @{term[source]"setsum (\<lambda>x. x) A"} & (\<^verbatim>\<open>SUM\<close>)\\
+@{term "setsum (\<lambda>x. t) A"} & @{term[source]"setsum (\<lambda>x. t) A"}\\
+@{term[source] "\<Sum>x|P. t"} & @{term"\<Sum>x|P. t"}\\
\multicolumn{2}{@ {}l@ {}}{Similarly for \<open>\<Prod>\<close> instead of \<open>\<Sum>\<close>} & (\<^verbatim>\<open>PROD\<close>)\\
\end{supertabular}
@@ -461,10 +463,10 @@
@{term[source] "\<Union>i\<le>n. A"} & @{term[source] "\<Union>i \<in> {..n}. A"}\\
@{term[source] "\<Union>i<n. A"} & @{term[source] "\<Union>i \<in> {..<n}. A"}\\
\multicolumn{2}{@ {}l@ {}}{Similarly for \<open>\<Inter>\<close> instead of \<open>\<Union>\<close>}\\
-@{term "setsum (%x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\
-@{term "setsum (%x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\
-@{term "setsum (%x. t) {..b}"} & @{term[source] "setsum (\<lambda>x. t) {..b}"}\\
-@{term "setsum (%x. t) {..<b}"} & @{term[source] "setsum (\<lambda>x. t) {..<b}"}\\
+@{term "setsum (\<lambda>x. t) {a..b}"} & @{term[source] "setsum (\<lambda>x. t) {a..b}"}\\
+@{term "setsum (\<lambda>x. t) {a..<b}"} & @{term[source] "setsum (\<lambda>x. t) {a..<b}"}\\
+@{term "setsum (\<lambda>x. t) {..b}"} & @{term[source] "setsum (\<lambda>x. t) {..b}"}\\
+@{term "setsum (\<lambda>x. t) {..<b}"} & @{term[source] "setsum (\<lambda>x. t) {..<b}"}\\
\multicolumn{2}{@ {}l@ {}}{Similarly for \<open>\<Prod>\<close> instead of \<open>\<Sum>\<close>}\\
\end{supertabular}
--- a/src/FOL/IFOL.thy Fri Sep 16 18:44:18 2016 +0200
+++ b/src/FOL/IFOL.thy Fri Sep 16 21:40:47 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:44:18 2016 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy Fri Sep 16 21:40:47 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:44:18 2016 +0200
+++ b/src/HOL/List.thy Fri Sep 16 21:40:47 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:44:18 2016 +0200
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy Fri Sep 16 21:40:47 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:44:18 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy Fri Sep 16 21:40:47 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:44:18 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSCA.thy Fri Sep 16 21:40:47 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:44:18 2016 +0200
+++ b/src/HOL/Number_Theory/Cong.thy Fri Sep 16 21:40:47 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:44:18 2016 +0200
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy Fri Sep 16 21:40:47 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:44:18 2016 +0200
+++ b/src/HOL/ZF/HOLZF.thy Fri Sep 16 21:40:47 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:44:18 2016 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Fri Sep 16 21:40:47 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:44:18 2016 +0200
+++ b/src/ZF/Epsilon.thy Fri Sep 16 21:40:47 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:44:18 2016 +0200
+++ b/src/ZF/Order.thy Fri Sep 16 21:40:47 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:44:18 2016 +0200
+++ b/src/ZF/Perm.thy Fri Sep 16 21:40:47 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:44:18 2016 +0200
+++ b/src/ZF/ZF.thy Fri Sep 16 21:40:47 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:44:18 2016 +0200
+++ b/src/ZF/func.thy Fri Sep 16 21:40:47 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:44:18 2016 +0200
+++ b/src/ZF/upair.thy Fri Sep 16 21:40:47 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)