# HG changeset patch
# User huffman
# Date 1200338939 -3600
# Node ID 2179c66612189f9780a0a0fd97d2b380fefc92ec
# Parent  098469c6c351c3f1c3784f373f1ba44aa23ed8e9
class bifinite supersedes class dcpo; remove unnecessary dcpo stuff

diff -r 098469c6c351 -r 2179c6661218 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Mon Jan 14 20:04:40 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Mon Jan 14 20:28:59 2008 +0100
@@ -118,26 +118,6 @@
 apply (erule monofun_snd [THEN ub2ub_monofun])
 done
 
-lemma directed_lub_cprod:
-  fixes S :: "('a::dcpo \<times> 'b::dcpo) set"
-  assumes S: "directed S"
-  shows "S <<| (\<Squnion>x\<in>S. fst x, \<Squnion>x\<in>S. snd x)"
-apply (rule is_lubI)
-apply (rule is_ubI)
-apply (rule_tac t=x in surjective_pairing [THEN ssubst])
-apply (rule monofun_pair)
-apply (erule is_ub_thelub' [OF dir2dir_monofun [OF monofun_fst S] imageI])
-apply (erule is_ub_thelub' [OF dir2dir_monofun [OF monofun_snd S] imageI])
-apply (rule_tac t=u in surjective_pairing [THEN ssubst])
-apply (rule monofun_pair)
-apply (rule is_lub_thelub')
-apply (rule dir2dir_monofun [OF monofun_fst S])
-apply (erule ub2ub_monofun' [OF monofun_fst])
-apply (rule is_lub_thelub')
-apply (rule dir2dir_monofun [OF monofun_snd S])
-apply (erule ub2ub_monofun' [OF monofun_snd])
-done
-
 lemma thelub_cprod:
   "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
     \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
@@ -152,15 +132,6 @@
   thus "\<exists>x. range S <<| x" ..
 qed
 
-instance "*" :: (dcpo, dcpo) dcpo
-proof
-  fix S :: "('a \<times> 'b) set"
-  assume "directed S"
-  hence "S <<| (\<Squnion>x\<in>S. fst x, \<Squnion>x\<in>S. snd x)"
-    by (rule directed_lub_cprod)
-  thus "\<exists>x. S <<| x" ..
-qed
-
 instance "*" :: (finite_po, finite_po) finite_po ..
 
 subsection {* Product type is pointed *}
diff -r 098469c6c351 -r 2179c6661218 src/HOLCF/Discrete.thy
--- a/src/HOLCF/Discrete.thy	Mon Jan 14 20:04:40 2008 +0100
+++ b/src/HOLCF/Discrete.thy	Mon Jan 14 20:28:59 2008 +0100
@@ -51,31 +51,6 @@
  "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
 by (fast elim: discr_chain0)
 
-lemma discr_directed_lemma:
-  fixes S :: "'a::type discr set"
-  assumes S: "directed S"
-  shows "\<exists>x. S = {x}"
-proof -
-  obtain x where x: "x \<in> S"
-    using S by (rule directedE1)
-  hence "S = {x}"
-  proof (safe)
-    fix y assume y: "y \<in> S"
-    obtain z where "x \<sqsubseteq> z" "y \<sqsubseteq> z"
-      using S x y by (rule directedE2)
-    thus "y = x" by simp
-  qed
-  thus "\<exists>x. S = {x}" ..
-qed
-
-instance discr :: (type) dcpo
-proof
-  fix S :: "'a discr set"
-  assume "directed S"
-  hence "\<exists>x. S = {x}" by (rule discr_directed_lemma)
-  thus "\<exists>x. S <<| x" by (fast intro: is_lub_singleton)
-qed
-
 instance discr :: (finite) finite_po
 proof
   have "finite (Discr ` (UNIV :: 'a set))"
diff -r 098469c6c351 -r 2179c6661218 src/HOLCF/Ffun.thy
--- a/src/HOLCF/Ffun.thy	Mon Jan 14 20:04:40 2008 +0100
+++ b/src/HOLCF/Ffun.thy	Mon Jan 14 20:28:59 2008 +0100
@@ -84,32 +84,11 @@
 apply (erule ub2ub_fun)
 done
 
-lemma lub_fun':
-  fixes S :: "('a::type \<Rightarrow> 'b::dcpo) set"
-  assumes S: "directed S"
-  shows "S <<| (\<lambda>x. \<Squnion>f\<in>S. f x)"
-apply (rule is_lubI)
-apply (rule is_ubI)
-apply (rule less_fun_ext)
-apply (rule is_ub_thelub')
-apply (rule dir2dir_monofun [OF monofun_app S])
-apply (erule imageI)
-apply (rule less_fun_ext)
-apply (rule is_lub_thelub')
-apply (rule dir2dir_monofun [OF monofun_app S])
-apply (erule ub2ub_monofun' [OF monofun_app])
-done
-
 lemma thelub_fun:
   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo)
     \<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)"
 by (rule lub_fun [THEN thelubI])
 
-lemma thelub_fun':
-  "directed (S::('a::type \<Rightarrow> 'b::dcpo) set)
-    \<Longrightarrow> lub S = (\<lambda>x. \<Squnion>f\<in>S. f x)"
-by (rule lub_fun' [THEN thelubI])
-
 lemma cpo_fun:
   "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
 by (rule exI, erule lub_fun)
@@ -117,13 +96,6 @@
 instance "fun"  :: (type, cpo) cpo
 by intro_classes (rule cpo_fun)
 
-lemma dcpo_fun:
-  "directed (S::('a::type \<Rightarrow> 'b::dcpo) set) \<Longrightarrow> \<exists>x. S <<| x"
-by (rule exI, erule lub_fun')
-
-instance "fun" :: (type, dcpo) dcpo
-by intro_classes (rule dcpo_fun)
-
 instance "fun" :: (finite, finite_po) finite_po ..
 
 text {* chain-finite function spaces *}
diff -r 098469c6c351 -r 2179c6661218 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Mon Jan 14 20:04:40 2008 +0100
+++ b/src/HOLCF/Pcpo.thy	Mon Jan 14 20:28:59 2008 +0100
@@ -17,40 +17,20 @@
         -- {* class axiom: *}
   cpo:   "chain S \<Longrightarrow> \<exists>x. range S <<| x" 
 
-axclass dcpo < po
-  dcpo: "directed S \<Longrightarrow> \<exists>x. S <<| x"
-
-instance dcpo < cpo
-by (intro_classes, rule dcpo [OF directed_chain])
-
 text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
 
 lemma thelubE: "\<lbrakk>chain S; (\<Squnion>i. S i) = (l::'a::cpo)\<rbrakk> \<Longrightarrow> range S <<| l"
 by (blast dest: cpo intro: lubI)
 
-lemma thelubE': "\<lbrakk>directed S; lub S = (l::'a::dcpo)\<rbrakk> \<Longrightarrow> S <<| l"
-by (blast dest: dcpo intro: lubI)
-
 text {* Properties of the lub *}
 
 lemma is_ub_thelub: "chain (S::nat \<Rightarrow> 'a::cpo) \<Longrightarrow> S x \<sqsubseteq> (\<Squnion>i. S i)"
 by (blast dest: cpo intro: lubI [THEN is_ub_lub])
 
-lemma is_ub_thelub': "\<lbrakk>directed S; (x::'a::dcpo) \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> lub S"
-apply (drule thelubE' [OF _ refl])
-apply (drule is_lubD1)
-apply (erule (1) is_ubD)
-done
-
 lemma is_lub_thelub:
   "\<lbrakk>chain (S::nat \<Rightarrow> 'a::cpo); range S <| x\<rbrakk> \<Longrightarrow> (\<Squnion>i. S i) \<sqsubseteq> x"
 by (blast dest: cpo intro: lubI [THEN is_lub_lub])
 
-lemma is_lub_thelub': "\<lbrakk>directed S; S <| x\<rbrakk> \<Longrightarrow> lub S \<sqsubseteq> (x::'a::dcpo)"
-apply (drule dcpo, clarify, drule lubI)
-apply (erule is_lub_lub, assumption)
-done
-
 lemma lub_range_mono:
   "\<lbrakk>range X \<subseteq> range Y; chain Y; chain (X::nat \<Rightarrow> 'a::cpo)\<rbrakk>
     \<Longrightarrow> (\<Squnion>i. X i) \<sqsubseteq> (\<Squnion>i. Y i)"
@@ -289,8 +269,9 @@
 apply (simp add: finite_chain_def)
 done
 
-instance finite_po < dcpo
+instance finite_po < cpo
 apply intro_classes
+apply (drule directed_chain)
 apply (drule directed_finiteD [OF _ finite subset_refl])
 apply (erule bexE, rule exI)
 apply (erule (1) is_lub_maximal)
diff -r 098469c6c351 -r 2179c6661218 src/HOLCF/SetPcpo.thy
--- a/src/HOLCF/SetPcpo.thy	Mon Jan 14 20:04:40 2008 +0100
+++ b/src/HOLCF/SetPcpo.thy	Mon Jan 14 20:28:59 2008 +0100
@@ -25,7 +25,7 @@
 lemma Union_is_lub: "A <<| Union A"
 unfolding is_lub_def is_ub_def less_set_def by fast
 
-instance set :: (type) dcpo
+instance set :: (type) cpo
 by (intro_classes, rule exI, rule Union_is_lub)
 
 lemma lub_eq_Union: "lub = Union"
diff -r 098469c6c351 -r 2179c6661218 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Mon Jan 14 20:04:40 2008 +0100
+++ b/src/HOLCF/Up.thy	Mon Jan 14 20:28:59 2008 +0100
@@ -177,55 +177,6 @@
 instance u :: (cpo) cpo
 by intro_classes (rule cpo_up)
 
-lemma up_directed_lemma:
-  "directed (S::'a::dcpo u set) \<Longrightarrow>
-    (directed (Iup -` S) \<and> S <<| Iup (lub (Iup -` S))) \<or>
-    S = {Ibottom}"
-apply (case_tac "\<exists>x. Iup x \<in> S")
-apply (rule disjI1)
-apply (subgoal_tac "directed (Iup -` S)")
-apply (rule conjI, assumption)
-apply (rule is_lubI)
-apply (rule is_ubI)
-apply (case_tac x, simp, simp)
-apply (erule is_ub_thelub', simp)
-apply (case_tac u)
-apply (erule exE)
-apply (drule (1) is_ubD)
-apply simp
-apply simp
-apply (erule is_lub_thelub')
-apply (rule is_ubI, simp)
-apply (drule (1) is_ubD, simp)
-apply (rule directedI)
-apply (erule exE)
-apply (rule exI)
-apply (erule vimageI2)
-apply simp
-apply (drule_tac x="Iup x" and y="Iup y" in directedD2, assumption+)
-apply (erule bexE, rename_tac z)
-apply (case_tac z)
-apply simp
-apply (rule_tac x=a in bexI)
-apply simp
-apply simp
-apply (rule disjI2)
-apply (simp, safe)
-apply (case_tac x, simp, simp)
-apply (drule directedD1)
-apply (clarify, rename_tac x)
-apply (case_tac x, simp, simp)
-done
-
-lemma dcpo_up: "directed (S::'a::dcpo u set) \<Longrightarrow> \<exists>x. S <<| x"
-apply (frule up_directed_lemma, safe)
-apply (erule exI)
-apply (rule exI, rule is_lub_singleton)
-done
-
-instance u :: (dcpo) dcpo
-by intro_classes (rule dcpo_up)
-
 subsection {* Lifted cpo is pointed *}
 
 lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"