# HG changeset patch
# User huffman
# Date 1199288247 -3600
# Node ID 74ee4914bb37297d9afc5cd87952e4720185608d
# Parent  4e4eb0f878501e775f66e3ccaa3d91d74d2d06d1
new is_ub lemmas; new lub syntax for set image

diff -r 4e4eb0f87850 -r 74ee4914bb37 src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Wed Jan 02 16:33:07 2008 +0100
+++ b/src/HOLCF/Porder.thy	Wed Jan 02 16:37:27 2008 +0100
@@ -56,12 +56,32 @@
   sq_ord_less_eq_trans
   sq_ord_eq_less_trans
 
-subsection {* Least upper bounds *}
+subsection {* Upper bounds *}
 
 definition
   is_ub :: "['a set, 'a::po] \<Rightarrow> bool"  (infixl "<|" 55)  where
   "(S <| x) = (\<forall>y. y \<in> S \<longrightarrow> y \<sqsubseteq> x)"
 
+lemma is_ubI: "(\<And>x. x \<in> S \<Longrightarrow> x \<sqsubseteq> u) \<Longrightarrow> S <| u"
+by (simp add: is_ub_def)
+
+lemma is_ubD: "\<lbrakk>S <| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
+by (simp add: is_ub_def)
+
+lemma ub_imageI: "(\<And>x. x \<in> S \<Longrightarrow> f x \<sqsubseteq> u) \<Longrightarrow> (\<lambda>x. f x) ` S <| u"
+unfolding is_ub_def by fast
+
+lemma ub_imageD: "\<lbrakk>f ` S <| u; x \<in> S\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> u"
+unfolding is_ub_def by fast
+
+lemma ub_rangeI: "(\<And>i. S i \<sqsubseteq> x) \<Longrightarrow> range S <| x"
+unfolding is_ub_def by fast
+
+lemma ub_rangeD: "range S <| x \<Longrightarrow> S i \<sqsubseteq> x"
+unfolding is_ub_def by fast
+
+subsection {* Least upper bounds *}
+
 definition
   is_lub :: "['a set, 'a::po] \<Rightarrow> bool"  (infixl "<<|" 55)  where
   "(S <<| x) = (S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u))"
@@ -70,6 +90,15 @@
   lub :: "'a set \<Rightarrow> 'a::po" where
   "lub S = (THE x. S <<| x)"
 
+syntax
+  "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3LUB _:_./ _)" [0,0, 10] 10)
+
+syntax (xsymbols)
+  "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0,0, 10] 10)
+
+translations
+  "LUB x:A. t" == "CONST lub ((%x. t) ` A)"
+
 abbreviation
   Lub  (binder "LUB " 10) where
   "LUB n. t n == lub (range t)"
@@ -77,7 +106,6 @@
 notation (xsymbols)
   Lub  (binder "\<Squnion> " 10)
 
-
 text {* lubs are unique *}
 
 lemma unique_lub: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
@@ -146,12 +174,6 @@
 
 text {* technical lemmas about (least) upper bounds of chains *}
 
-lemma ub_rangeD: "range S <| x \<Longrightarrow> S i \<sqsubseteq> x"
-by (unfold is_ub_def, simp)
-
-lemma ub_rangeI: "(\<And>i. S i \<sqsubseteq> x) \<Longrightarrow> range S <| x"
-by (unfold is_ub_def, fast)
-
 lemma is_ub_lub: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x"
 by (rule is_lubD1 [THEN ub_rangeD])