# HG changeset patch
# User haftmann
# Date 1174375642 -3600
# Node ID be9ae8b19271d2356e2e257572f356b41179781f
# Parent  088e141084a680d38fb787cbdd8330168a228728
new lemmas

diff -r 088e141084a6 -r be9ae8b19271 src/HOL/FixedPoint.thy
--- a/src/HOL/FixedPoint.thy	Tue Mar 20 08:27:21 2007 +0100
+++ b/src/HOL/FixedPoint.thy	Tue Mar 20 08:27:22 2007 +0100
@@ -125,6 +125,28 @@
 lemma top_greatest[simp]: "(x::'a::complete_lattice) \<le> Inf{}"
   by (rule Inf_greatest) simp
 
+lemma inf_Inf_empty:
+  "inf a (Inf {}) = a"
+proof -
+  have "a \<le> Inf {}" by (rule top_greatest)
+  then show ?thesis by (rule inf_absorb1)
+qed
+
+lemma inf_binary:
+  "Inf {a, b} = inf a b"
+unfolding Inf_insert inf_Inf_empty ..
+
+lemma sup_Sup_empty:
+  "sup a (Sup {}) = a"
+proof -
+  have "Sup {} \<le> a" by (rule bot_least)
+  then show ?thesis by (rule sup_absorb1)
+qed
+
+lemma sup_binary:
+  "Sup {a, b} = sup a b"
+unfolding Sup_insert sup_Sup_empty ..
+
 lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
   by (auto intro: order_antisym SUP_leI le_SUPI)