1.1 --- a/src/HOL/FixedPoint.thy	Tue Mar 20 08:27:21 2007 +0100
     1.2 +++ b/src/HOL/FixedPoint.thy	Tue Mar 20 08:27:22 2007 +0100
     1.3 @@ -125,6 +125,28 @@
     1.4  lemma top_greatest[simp]: "(x::'a::complete_lattice) \<le> Inf{}"
     1.5    by (rule Inf_greatest) simp
     1.6  
     1.7 +lemma inf_Inf_empty:
     1.8 +  "inf a (Inf {}) = a"
     1.9 +proof -
    1.10 +  have "a \<le> Inf {}" by (rule top_greatest)
    1.11 +  then show ?thesis by (rule inf_absorb1)
    1.12 +qed
    1.13 +
    1.14 +lemma inf_binary:
    1.15 +  "Inf {a, b} = inf a b"
    1.16 +unfolding Inf_insert inf_Inf_empty ..
    1.17 +
    1.18 +lemma sup_Sup_empty:
    1.19 +  "sup a (Sup {}) = a"
    1.20 +proof -
    1.21 +  have "Sup {} \<le> a" by (rule bot_least)
    1.22 +  then show ?thesis by (rule sup_absorb1)
    1.23 +qed
    1.24 +
    1.25 +lemma sup_binary:
    1.26 +  "Sup {a, b} = sup a b"
    1.27 +unfolding Sup_insert sup_Sup_empty ..
    1.28 +
    1.29  lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
    1.30    by (auto intro: order_antisym SUP_leI le_SUPI)
    1.31