# HG changeset patch
# User wenzelm
# Date 995830297 -7200
# Node ID 54b23680167196c764135674043b899a014f7ee0
# Parent  e389e4338604851da073396ecb7ba531a474e6fe
replaced SOME by THE;

diff -r e389e4338604 -r 54b236801671 src/HOL/Lattice/CompleteLattice.thy
--- a/src/HOL/Lattice/CompleteLattice.thy	Sun Jul 22 21:31:00 2001 +0200
+++ b/src/HOL/Lattice/CompleteLattice.thy	Sun Jul 22 21:31:37 2001 +0200
@@ -38,8 +38,8 @@
   Meet :: "'a::complete_lattice set \<Rightarrow> 'a"    ("\<Sqinter>_" [90] 90)
   Join :: "'a::complete_lattice set \<Rightarrow> 'a"    ("\<Squnion>_" [90] 90)
 defs
-  Meet_def: "\<Sqinter>A \<equiv> SOME inf. is_Inf A inf"
-  Join_def: "\<Squnion>A \<equiv> SOME sup. is_Sup A sup"
+  Meet_def: "\<Sqinter>A \<equiv> THE inf. is_Inf A inf"
+  Join_def: "\<Squnion>A \<equiv> THE sup. is_Sup A sup"
 
 text {*
   Due to unique existence of bounds, the complete lattice operations
@@ -49,8 +49,8 @@
 lemma Meet_equality [elim?]: "is_Inf A inf \<Longrightarrow> \<Sqinter>A = inf"
 proof (unfold Meet_def)
   assume "is_Inf A inf"
-  thus "(SOME inf. is_Inf A inf) = inf"
-    by (rule some_equality) (rule is_Inf_uniq)
+  thus "(THE inf. is_Inf A inf) = inf"
+    by (rule the_equality) (rule is_Inf_uniq)
 qed
 
 lemma MeetI [intro?]:
@@ -62,8 +62,8 @@
 lemma Join_equality [elim?]: "is_Sup A sup \<Longrightarrow> \<Squnion>A = sup"
 proof (unfold Join_def)
   assume "is_Sup A sup"
-  thus "(SOME sup. is_Sup A sup) = sup"
-    by (rule some_equality) (rule is_Sup_uniq)
+  thus "(THE sup. is_Sup A sup) = sup"
+    by (rule the_equality) (rule is_Sup_uniq)
 qed
 
 lemma JoinI [intro?]:
@@ -80,8 +80,8 @@
 
 lemma is_Inf_Meet [intro?]: "is_Inf A (\<Sqinter>A)"
 proof (unfold Meet_def)
-  from ex_Inf
-  show "is_Inf A (SOME inf. is_Inf A inf)" ..
+  from ex_Inf obtain inf where "is_Inf A inf" ..
+  thus "is_Inf A (THE inf. is_Inf A inf)" by (rule theI) (rule is_Inf_uniq)
 qed
 
 lemma Meet_greatest [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> x \<sqsubseteq> a) \<Longrightarrow> x \<sqsubseteq> \<Sqinter>A"
@@ -93,8 +93,8 @@
 
 lemma is_Sup_Join [intro?]: "is_Sup A (\<Squnion>A)"
 proof (unfold Join_def)
-  from ex_Sup
-  show "is_Sup A (SOME sup. is_Sup A sup)" ..
+  from ex_Sup obtain sup where "is_Sup A sup" ..
+  thus "is_Sup A (THE sup. is_Sup A sup)" by (rule theI) (rule is_Sup_uniq)
 qed
 
 lemma Join_least [intro?]: "(\<And>a. a \<in> A \<Longrightarrow> a \<sqsubseteq> x) \<Longrightarrow> \<Squnion>A \<sqsubseteq> x"
diff -r e389e4338604 -r 54b236801671 src/HOL/Lattice/Lattice.thy
--- a/src/HOL/Lattice/Lattice.thy	Sun Jul 22 21:31:00 2001 +0200
+++ b/src/HOL/Lattice/Lattice.thy	Sun Jul 22 21:31:37 2001 +0200
@@ -31,8 +31,8 @@
   meet :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<sqinter>" 70)
   join :: "'a::lattice \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<squnion>" 65)
 defs
-  meet_def: "x && y \<equiv> SOME inf. is_inf x y inf"
-  join_def: "x || y \<equiv> SOME sup. is_sup x y sup"
+  meet_def: "x && y \<equiv> THE inf. is_inf x y inf"
+  join_def: "x || y \<equiv> THE sup. is_sup x y sup"
 
 text {*
   Due to unique existence of bounds, the lattice operations may be
@@ -42,8 +42,8 @@
 lemma meet_equality [elim?]: "is_inf x y inf \<Longrightarrow> x \<sqinter> y = inf"
 proof (unfold meet_def)
   assume "is_inf x y inf"
-  thus "(SOME inf. is_inf x y inf) = inf"
-    by (rule some_equality) (rule is_inf_uniq)
+  thus "(THE inf. is_inf x y inf) = inf"
+    by (rule the_equality) (rule is_inf_uniq)
 qed
 
 lemma meetI [intro?]:
@@ -53,8 +53,8 @@
 lemma join_equality [elim?]: "is_sup x y sup \<Longrightarrow> x \<squnion> y = sup"
 proof (unfold join_def)
   assume "is_sup x y sup"
-  thus "(SOME sup. is_sup x y sup) = sup"
-    by (rule some_equality) (rule is_sup_uniq)
+  thus "(THE sup. is_sup x y sup) = sup"
+    by (rule the_equality) (rule is_sup_uniq)
 qed
 
 lemma joinI [intro?]: "x \<sqsubseteq> sup \<Longrightarrow> y \<sqsubseteq> sup \<Longrightarrow>
@@ -69,8 +69,8 @@
 
 lemma is_inf_meet [intro?]: "is_inf x y (x \<sqinter> y)"
 proof (unfold meet_def)
-  from ex_inf
-  show "is_inf x y (SOME inf. is_inf x y inf)" ..
+  from ex_inf obtain inf where "is_inf x y inf" ..
+  thus "is_inf x y (THE inf. is_inf x y inf)" by (rule theI) (rule is_inf_uniq)
 qed
 
 lemma meet_greatest [intro?]: "z \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> y \<Longrightarrow> z \<sqsubseteq> x \<sqinter> y"
@@ -85,8 +85,8 @@
 
 lemma is_sup_join [intro?]: "is_sup x y (x \<squnion> y)"
 proof (unfold join_def)
-  from ex_sup
-  show "is_sup x y (SOME sup. is_sup x y sup)" ..
+  from ex_sup obtain sup where "is_sup x y sup" ..
+  thus "is_sup x y (THE sup. is_sup x y sup)" by (rule theI) (rule is_sup_uniq)
 qed
 
 lemma join_least [intro?]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"