--- 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 *}
--- 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))"
--- 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 *}
--- 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)
--- 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"
--- 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"