1.1 --- a/src/HOL/Lattices.thy	Tue Dec 24 11:24:16 2013 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Wed Dec 25 10:09:43 2013 +0100
     1.3 @@ -98,7 +98,7 @@
     1.4    obtains "a \<preceq> b" and "a \<preceq> c"
     1.5    using assms by (blast intro: trans cobounded1 cobounded2)
     1.6  
     1.7 -lemma bounded_iff:
     1.8 +lemma bounded_iff (* [simp] CANDIDATE *):
     1.9    "a \<preceq> b * c \<longleftrightarrow> a \<preceq> b \<and> a \<preceq> c"
    1.10    by (blast intro: boundedI elim: boundedE)
    1.11  
    1.12 @@ -115,14 +115,29 @@
    1.13    "b \<preceq> c \<Longrightarrow> a * b \<preceq> c"
    1.14    by (rule trans) auto
    1.15  
    1.16 +lemma strict_coboundedI1:
    1.17 +  "a \<prec> c \<Longrightarrow> a * b \<prec> c"
    1.18 +  using irrefl
    1.19 +    by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order elim: strict_boundedE)
    1.20 +
    1.21 +lemma strict_coboundedI2:
    1.22 +  "b \<prec> c \<Longrightarrow> a * b \<prec> c"
    1.23 +  using strict_coboundedI1 [of b c a] by (simp add: commute)
    1.24 +
    1.25  lemma mono: "a \<preceq> c \<Longrightarrow> b \<preceq> d \<Longrightarrow> a * b \<preceq> c * d"
    1.26    by (blast intro: boundedI coboundedI1 coboundedI2)
    1.27  
    1.28  lemma absorb1: "a \<preceq> b \<Longrightarrow> a * b = a"
    1.29 -  by (rule antisym) (auto simp add: refl bounded_iff)
    1.30 +  by (rule antisym) (auto simp add: bounded_iff refl)
    1.31  
    1.32  lemma absorb2: "b \<preceq> a \<Longrightarrow> a * b = b"
    1.33 -  by (rule antisym) (auto simp add: refl bounded_iff)
    1.34 +  by (rule antisym) (auto simp add: bounded_iff refl)
    1.35 +
    1.36 +lemma absorb_iff1: "a \<preceq> b \<longleftrightarrow> a * b = a"
    1.37 +  using order_iff by auto
    1.38 +
    1.39 +lemma absorb_iff2: "b \<preceq> a \<longleftrightarrow> a * b = b"
    1.40 +  using order_iff by (auto simp add: commute)
    1.41  
    1.42  end
    1.43