--- 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)
--- 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]
--- 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
--- 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)