# HG changeset patch
# User huffman
# Date 1115344064 -7200
# Node ID 145651bc64a83a0f0d371665f4c352e97eeacaf2
# Parent  68bd1e16552a09b5ec429c23a3886425018a3721
Replaced all unnecessary uses of SOME with THE or LEAST

diff -r 68bd1e16552a -r 145651bc64a8 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Thu May 05 13:21:05 2005 +0200
+++ b/src/HOLCF/Lift.thy	Fri May 06 03:47:44 2005 +0200
@@ -43,7 +43,7 @@
 lemma minimal_lift [iff]: "Undef << x"
   by (simp add: inst_lift_po)
 
-lemma UU_lift_def: "(SOME u. \<forall>y. u \<sqsubseteq> y) = Undef"
+lemma UU_lift_def: "(THE u. \<forall>y. u \<sqsubseteq> y) = Undef"
   apply (rule minimal2UU [symmetric])
   apply (rule minimal_lift)
   done
@@ -195,7 +195,7 @@
   For @{term "x ~= UU"} in assumptions @{text def_tac} replaces @{text
   x} by @{text "Def a"} in conclusion. *}
 
-ML {*
+ML_setup {*
   local val not_Undef_is_Def = thm "not_Undef_is_Def"
   in val def_tac = SIMPSET' (fn ss =>
     etac (not_Undef_is_Def RS iffD1 RS exE) THEN' asm_simp_tac ss)
diff -r 68bd1e16552a -r 145651bc64a8 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Thu May 05 13:21:05 2005 +0200
+++ b/src/HOLCF/Pcpo.thy	Fri May 06 03:47:44 2005 +0200
@@ -140,14 +140,16 @@
   UU            :: "'a::pcpo"                           ("\<bottom>")
 
 defs
-  UU_def:        "UU == @x.!y. x<<y"
+  UU_def:        "UU == THE x. ALL y. x<<y"
 
 text {* derive the old rule minimal *}
  
 lemma UU_least: "ALL z. UU << z"
 apply (unfold UU_def)
-apply (rule some_eq_ex [THEN iffD2])
+apply (rule theI')
+apply (rule ex_ex1I)
 apply (rule least)
+apply (blast intro: antisym_less)
 done
 
 lemmas minimal = UU_least [THEN spec, standard]
diff -r 68bd1e16552a -r 145651bc64a8 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Thu May 05 13:21:05 2005 +0200
+++ b/src/HOLCF/Porder.thy	Fri May 06 03:47:44 2005 +0200
@@ -33,9 +33,8 @@
 
 text {* minimal fixes least element *}
 
-lemma minimal2UU[OF allI] : "!x::'a::po. uu<<x ==> uu=(@u.!y. u<<y)"
-apply (blast intro: someI2 antisym_less)
-done
+lemma minimal2UU[OF allI] : "!x::'a::po. uu<<x ==> uu=(THE u.!y. u<<y)"
+by (blast intro: theI2 antisym_less)
 
 text {* the reverse law of anti-symmetry of @{term "op <<"} *}
 
@@ -89,7 +88,7 @@
 max_in_chain_def: "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" 
 finite_chain_def: "finite_chain C == chain(C) & (? i. max_in_chain i C)"
 
-lub_def:          "lub S == (@x. S <<| x)"
+lub_def:          "lub S == (THE x. S <<| x)"
 
 text {* lubs are unique *}
 
@@ -128,13 +127,17 @@
 lemmas lub = lub_def [THEN meta_eq_to_obj_eq, standard]
 
 lemma lubI[OF exI]: "EX x. M <<| x ==> M <<| lub(M)"
-apply (simp add: lub some_eq_ex)
+apply (unfold lub_def)
+apply (rule theI')
+apply (erule ex_ex1I)
+apply (erule unique_lub)
+apply assumption
 done
 
 lemma thelubI: "M <<| l ==> lub(M) = l"
 apply (rule unique_lub)
-apply (subst lub)
-apply (erule someI)
+apply (rule lubI)
+apply assumption
 apply assumption
 done
 
@@ -211,10 +214,10 @@
 done
 
 lemma lub_finch2: 
-        "finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)"
+        "finite_chain(C) ==> range(C) <<| C(LEAST i. max_in_chain i C)"
 apply (unfold finite_chain_def)
 apply (rule lub_finch1)
-prefer 2 apply (best intro: someI)
+prefer 2 apply (best intro: LeastI)
 apply blast
 done
 
diff -r 68bd1e16552a -r 145651bc64a8 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Thu May 05 13:21:05 2005 +0200
+++ b/src/HOLCF/Sprod.thy	Fri May 06 03:47:44 2005 +0200
@@ -36,10 +36,10 @@
 
   Ispair_def:    "Ispair a b == Abs_Sprod(Spair_Rep a b)"
 
-  Isfst_def:     "Isfst(p) == @z.        (p=Ispair UU UU --> z=UU)
+  Isfst_def:     "Isfst(p) == THE z.     (p=Ispair UU UU --> z=UU)
                 &(! a b. ~a=UU & ~b=UU & p=Ispair a b   --> z=a)"  
 
-  Issnd_def:     "Issnd(p) == @z.        (p=Ispair UU UU  --> z=UU)
+  Issnd_def:     "Issnd(p) == THE z.     (p=Ispair UU UU  --> z=UU)
                 &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
 
 text {* A non-emptiness result for Sprod *}
@@ -189,7 +189,7 @@
 
 lemma strict_Isfst: "p=Ispair UU UU ==> Isfst p = UU"
 apply (unfold Isfst_def)
-apply (rule some_equality)
+apply (rule the_equality)
 apply (rule conjI)
 apply fast
 apply (intro strip)
@@ -213,7 +213,7 @@
 
 lemma strict_Issnd: "p=Ispair UU UU ==>Issnd p=UU"
 apply (unfold Issnd_def)
-apply (rule some_equality)
+apply (rule the_equality)
 apply (rule conjI)
 apply fast
 apply (intro strip)
@@ -237,7 +237,7 @@
 
 lemma Isfst: "[|x~=UU ;y~=UU |] ==> Isfst(Ispair x y) = x"
 apply (unfold Isfst_def)
-apply (rule some_equality)
+apply (rule the_equality)
 apply (rule conjI)
 apply (intro strip)
 apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)
@@ -252,7 +252,7 @@
 
 lemma Issnd: "[|x~=UU ;y~=UU |] ==> Issnd(Ispair x y) = y"
 apply (unfold Issnd_def)
-apply (rule some_equality)
+apply (rule the_equality)
 apply (rule conjI)
 apply (intro strip)
 apply (rule_tac P = "Ispair x y = Ispair UU UU" in notE)