# HG changeset patch
# User huffman
# Date 1214874840 -7200
# Node ID 07e04ab0177a82df5ae02754ce8f712c54c9e1ff
# Parent  be852e06d546d4321640e93d6ac202edd481534c
remove unused lemmas ub2ub_monofun' and dir2dir_monofun

diff -r be852e06d546 -r 07e04ab0177a src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Tue Jul 01 03:12:39 2008 +0200
+++ b/src/HOLCF/Cont.thy	Tue Jul 01 03:14:00 2008 +0200
@@ -76,36 +76,6 @@
 apply (erule ub_rangeD)
 done
 
-lemma ub2ub_monofun':
-  "\<lbrakk>monofun f; S <| u\<rbrakk> \<Longrightarrow> f ` S <| f u"
-apply (rule ub_imageI)
-apply (erule monofunE)
-apply (erule (1) is_ubD)
-done
-
-text {* monotone functions map directed sets to directed sets *}
-
-lemma dir2dir_monofun:
-  assumes f: "monofun f"
-  assumes S: "directed S"
-  shows "directed (f ` S)"
-proof (rule directedI)
-  from directedD1 [OF S]
-  obtain x where "x \<in> S" ..
-  hence "f x \<in> f ` S" by simp
-  thus "\<exists>x. x \<in> f ` S" ..
-next
-  fix x assume "x \<in> f ` S"
-  then obtain a where x: "x = f a" and a: "a \<in> S" ..
-  fix y assume "y \<in> f ` S"
-  then obtain b where y: "y = f b" and b: "b \<in> S" ..
-  from directedD2 [OF S a b]
-  obtain c where "c \<in> S" and "a \<sqsubseteq> c \<and> b \<sqsubseteq> c" ..
-  hence "f c \<in> f ` S" and "x \<sqsubseteq> f c \<and> y \<sqsubseteq> f c"
-    using monofunE [OF f] x y by simp_all
-  thus "\<exists>z\<in>f ` S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z" ..
-qed
-
 text {* left to right: @{prop "monofun f \<and> contlub f \<Longrightarrow> cont f"} *}
 
 lemma monocontlub2cont: "\<lbrakk>monofun f; contlub f\<rbrakk> \<Longrightarrow> cont f"