# HG changeset patch
# User huffman
# Date 1199294625 -3600
# Node ID 0fd4c238273bbcf27a675ee82ccf6de31ed539af
# Parent  ae71b21de8fbf597aa32d624f8241d8d823ec219
added new lemmas

diff -r ae71b21de8fb -r 0fd4c238273b src/HOLCF/Porder.thy
--- a/src/HOLCF/Porder.thy	Wed Jan 02 17:26:19 2008 +0100
+++ b/src/HOLCF/Porder.thy	Wed Jan 02 18:23:45 2008 +0100
@@ -125,8 +125,17 @@
 lemma thelubI: "M <<| l \<Longrightarrow> lub M = l"
 by (rule unique_lub [OF lubI])
 
+lemma is_lub_singleton: "{x} <<| x"
+by (simp add: is_lub_def is_ub_def)
+
 lemma lub_singleton [simp]: "lub {x} = x"
-by (simp add: thelubI is_lub_def is_ub_def)
+by (rule thelubI [OF is_lub_singleton])
+
+lemma is_lub_bin: "x \<sqsubseteq> y \<Longrightarrow> {x, y} <<| y"
+by (simp add: is_lub_def is_ub_def)
+
+lemma lub_bin: "x \<sqsubseteq> y \<Longrightarrow> lub {x, y} = y"
+by (rule is_lub_bin [THEN thelubI])
 
 text {* access to some definition as inference rule *}
 
@@ -329,6 +338,17 @@
 lemma directedD2: "\<lbrakk>directed S; x \<in> S; y \<in> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
 unfolding directed_def by fast
 
+lemma directedE1:
+  assumes S: "directed S"
+  obtains z where "z \<in> S"
+by (insert directedD1 [OF S], fast)
+
+lemma directedE2:
+  assumes S: "directed S"
+  assumes x: "x \<in> S" and y: "y \<in> S"
+  obtains z where "z \<in> S" "x \<sqsubseteq> z" "y \<sqsubseteq> z"
+by (insert directedD2 [OF S x y], fast)
+
 lemma directed_finiteI:
   assumes U: "\<And>U. \<lbrakk>finite U; U \<subseteq> S\<rbrakk> \<Longrightarrow> \<exists>z\<in>S. \<forall>x\<in>U. x \<sqsubseteq> z"
   shows "directed S"