src/HOLCF/Cprod.thy
changeset 25906 2179c6661218
parent 25905 098469c6c351
child 25907 695a9d88d697
--- 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 *}