# HG changeset patch
# User huffman
# Date 1198116380 -3600
# Node ID 80c06e4d4db63459e36cdf1546ac01566983dc0a
# Parent  0a104ddb72d92a27614ea9ee43a42cca7786bfc7
move bottom-related stuff back into Pcpo.thy

diff -r 0a104ddb72d9 -r 80c06e4d4db6 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Thu Dec 20 01:07:21 2007 +0100
+++ b/src/HOLCF/Cfun.thy	Thu Dec 20 03:06:20 2007 +0100
@@ -496,9 +496,7 @@
 done
 
 (*FIXME: long proof*)
-lemma contlub_strictify2:
-  fixes f :: "'a::pcpo \<rightarrow> 'b::pcpo"
-  shows "contlub (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
+lemma contlub_strictify2: "contlub (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
 apply (rule contlubI)
 apply (case_tac "lub (range Y) = \<bottom>")
 apply (drule (1) chain_UU_I)
diff -r 0a104ddb72d9 -r 80c06e4d4db6 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Thu Dec 20 01:07:21 2007 +0100
+++ b/src/HOLCF/Lift.thy	Thu Dec 20 03:06:20 2007 +0100
@@ -133,7 +133,7 @@
 apply (rule cont_id [THEN cont2cont_fun])
 done
 
-lemma cont_lift_case2: "cont (\<lambda>x. lift_case (\<bottom>::'a::pcpo) f x)"
+lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)"
 apply (rule flatdom_strict2cont)
 apply simp
 done
@@ -152,8 +152,7 @@
 done
 
 lemma cont2cont_lift_case:
-  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow>
-    cont (\<lambda>x. lift_case (UU::'a::pcpo) (f x) (g x))"
+  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case UU (f x) (g x))"
 apply (subgoal_tac "cont (\<lambda>x. (FLIFT y. f x y)\<cdot>(g x))")
 apply (simp add: flift1_def cont_lift_case2)
 apply (simp add: cont2cont_flift1)
diff -r 0a104ddb72d9 -r 80c06e4d4db6 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Thu Dec 20 01:07:21 2007 +0100
+++ b/src/HOLCF/Pcpo.thy	Thu Dec 20 03:06:20 2007 +0100
@@ -168,9 +168,65 @@
 
 text {* The class pcpo of pointed cpos *}
 
-axclass pcpo < cpo, ppo
+axclass pcpo < cpo
+  least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
+
+definition
+  UU :: "'a::pcpo" where
+  "UU = (THE x. \<forall>y. x \<sqsubseteq> y)"
+
+notation (xsymbols)
+  UU  ("\<bottom>")
+
+text {* derive the old rule minimal *}
+ 
+lemma UU_least: "\<forall>z. \<bottom> \<sqsubseteq> z"
+apply (unfold UU_def)
+apply (rule theI')
+apply (rule ex_ex1I)
+apply (rule least)
+apply (blast intro: antisym_less)
+done
+
+lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
+by (rule UU_least [THEN spec])
+
+lemma UU_reorient: "(\<bottom> = x) = (x = \<bottom>)"
+by auto
 
-lemma chain_UU_I: "\<lbrakk>chain Y; (\<Squnion>i. Y i) = \<bottom>\<rbrakk> \<Longrightarrow> \<forall>i. Y i = (\<bottom>::'a::pcpo)"
+ML_setup {*
+local
+  val meta_UU_reorient = thm "UU_reorient" RS eq_reflection;
+  fun reorient_proc sg _ (_ $ t $ u) =
+    case u of
+        Const("Pcpo.UU",_) => NONE
+      | Const("HOL.zero", _) => NONE
+      | Const("HOL.one", _) => NONE
+      | Const("Numeral.number_of", _) $ _ => NONE
+      | _ => SOME meta_UU_reorient;
+in
+  val UU_reorient_simproc = 
+    Simplifier.simproc @{theory} "UU_reorient_simproc" ["UU=x"] reorient_proc
+end;
+
+Addsimprocs [UU_reorient_simproc];
+*}
+
+text {* useful lemmas about @{term \<bottom>} *}
+
+lemma less_UU_iff [simp]: "(x \<sqsubseteq> \<bottom>) = (x = \<bottom>)"
+by (simp add: po_eq_conv)
+
+lemma eq_UU_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"
+by simp
+
+lemma UU_I: "x \<sqsubseteq> \<bottom> \<Longrightarrow> x = \<bottom>"
+by (subst eq_UU_iff)
+
+lemma not_less2not_eq: "\<not> (x::'a::po) \<sqsubseteq> y \<Longrightarrow> x \<noteq> y"
+by auto
+
+lemma chain_UU_I: "\<lbrakk>chain Y; (\<Squnion>i. Y i) = \<bottom>\<rbrakk> \<Longrightarrow> \<forall>i. Y i = \<bottom>"
 apply (rule allI)
 apply (rule UU_I)
 apply (erule subst)
@@ -199,7 +255,7 @@
 axclass chfin < po
   chfin: "\<forall>Y. chain Y \<longrightarrow> (\<exists>n. max_in_chain n Y)"
 
-axclass flat < ppo
+axclass flat < pcpo
   ax_flat: "\<forall>x y. x \<sqsubseteq> y \<longrightarrow> (x = \<bottom>) \<or> (x = y)"
 
 text {* some properties for chfin and flat *}
@@ -233,8 +289,6 @@
 instance flat < chfin
 by intro_classes (rule flat_imp_chfin)
 
-instance flat < pcpo ..
-
 text {* flat subclass of chfin; @{text adm_flat} not needed *}
 
 lemma flat_eq: "(a::'a::flat) \<noteq> \<bottom> \<Longrightarrow> a \<sqsubseteq> b = (a = b)"
diff -r 0a104ddb72d9 -r 80c06e4d4db6 src/HOLCF/Tools/domain/domain_library.ML
--- a/src/HOLCF/Tools/domain/domain_library.ML	Thu Dec 20 01:07:21 2007 +0100
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Thu Dec 20 03:06:20 2007 +0100
@@ -100,7 +100,7 @@
 (* ----- qualified names of HOLCF constants ----- *)
 
 val lessN      = @{const_name Porder.sq_le};
-val UU_N       = "Porder.UU";
+val UU_N       = "Pcpo.UU";
 val admN       = "Adm.adm";
 val compactN   = "Adm.compact";
 val Rep_CFunN  = "Cfun.Rep_CFun";
diff -r 0a104ddb72d9 -r 80c06e4d4db6 src/HOLCF/Tools/pcpodef_package.ML
--- a/src/HOLCF/Tools/pcpodef_package.ML	Thu Dec 20 01:07:21 2007 +0100
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Thu Dec 20 03:06:20 2007 +0100
@@ -72,7 +72,7 @@
       HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
     fun mk_admissible A =
       mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
-    fun mk_UU_mem A = HOLogic.mk_mem (Const ("Porder.UU", oldT), A);
+    fun mk_UU_mem A = HOLogic.mk_mem (Const ("Pcpo.UU", oldT), A);
     val goal = if pcpo
       then HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_UU_mem set, mk_admissible set))
       else HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_nonempty set, mk_admissible set));