author huffman Tue, 01 Jul 2008 03:14:00 +0200 changeset 27416 07e04ab0177a parent 27415 be852e06d546 child 27417 6cc897e2468a
remove unused lemmas ub2ub_monofun' and dir2dir_monofun
 src/HOLCF/Cont.thy file | annotate | diff | comparison | revisions
```--- 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"```