# HG changeset patch
# User huffman
# Date 1198012711 -3600
# Node ID 73fbe868b4e71c228ef9741b1fc3770e3e5039ec
# Parent  185ea28035ac7fd2e3ebdb70b7e67a8111dfed9f
add class ppo of pointed partial orders;
define UU in class ppo instead of pcpo;
add new lemmas about lub

diff -r 185ea28035ac -r 73fbe868b4e7 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Tue Dec 18 19:54:34 2007 +0100
+++ b/src/HOLCF/Cfun.thy	Tue Dec 18 22:18:31 2007 +0100
@@ -496,7 +496,9 @@
 done
 
 (*FIXME: long proof*)
-lemma contlub_strictify2: "contlub (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
+lemma contlub_strictify2:
+  fixes f :: "'a::pcpo \<rightarrow> 'b::pcpo"
+  shows "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 185ea28035ac -r 73fbe868b4e7 src/HOLCF/Lift.thy
--- a/src/HOLCF/Lift.thy	Tue Dec 18 19:54:34 2007 +0100
+++ b/src/HOLCF/Lift.thy	Tue Dec 18 22:18:31 2007 +0100
@@ -133,7 +133,7 @@
 apply (rule cont_id [THEN cont2cont_fun])
 done
 
-lemma cont_lift_case2: "cont (\<lambda>x. lift_case \<bottom> f x)"
+lemma cont_lift_case2: "cont (\<lambda>x. lift_case (\<bottom>::'a::pcpo) f x)"
 apply (rule flatdom_strict2cont)
 apply simp
 done
@@ -152,7 +152,8 @@
 done
 
 lemma cont2cont_lift_case:
-  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case UU (f x) (g x))"
+  "\<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))"
 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 185ea28035ac -r 73fbe868b4e7 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Tue Dec 18 19:54:34 2007 +0100
+++ b/src/HOLCF/Pcpo.thy	Tue Dec 18 22:18:31 2007 +0100
@@ -168,65 +168,9 @@
 
 text {* The class pcpo of pointed cpos *}
 
-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
+axclass pcpo < cpo, ppo
 
-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>"
+lemma chain_UU_I: "\<lbrakk>chain Y; (\<Squnion>i. Y i) = \<bottom>\<rbrakk> \<Longrightarrow> \<forall>i. Y i = (\<bottom>::'a::pcpo)"
 apply (rule allI)
 apply (rule UU_I)
 apply (erule subst)
@@ -255,7 +199,7 @@
 axclass chfin < po
   chfin: "\<forall>Y. chain Y \<longrightarrow> (\<exists>n. max_in_chain n Y)"
 
-axclass flat < pcpo
+axclass flat < ppo
   ax_flat: "\<forall>x y. x \<sqsubseteq> y \<longrightarrow> (x = \<bottom>) \<or> (x = y)"
 
 text {* some properties for chfin and flat *}
@@ -289,6 +233,8 @@
 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 185ea28035ac -r 73fbe868b4e7 src/HOLCF/Tools/domain/domain_library.ML
--- a/src/HOLCF/Tools/domain/domain_library.ML	Tue Dec 18 19:54:34 2007 +0100
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Tue Dec 18 22:18:31 2007 +0100
@@ -100,7 +100,7 @@
 (* ----- qualified names of HOLCF constants ----- *)
 
 val lessN      = @{const_name Porder.sq_le};
-val UU_N       = "Pcpo.UU";
+val UU_N       = "Porder.UU";
 val admN       = "Adm.adm";
 val compactN   = "Adm.compact";
 val Rep_CFunN  = "Cfun.Rep_CFun";
diff -r 185ea28035ac -r 73fbe868b4e7 src/HOLCF/Tools/pcpodef_package.ML
--- a/src/HOLCF/Tools/pcpodef_package.ML	Tue Dec 18 19:54:34 2007 +0100
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Tue Dec 18 22:18:31 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 ("Pcpo.UU", oldT), A);
+    fun mk_UU_mem A = HOLogic.mk_mem (Const ("Porder.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));