src/HOL/Lattices.thy
changeset 54859 64ff7f16d5b7
parent 54858 c1c334198504
child 54861 00d551179872
     1.1 --- a/src/HOL/Lattices.thy	Wed Dec 25 10:09:43 2013 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Wed Dec 25 15:52:25 2013 +0100
     1.3 @@ -98,14 +98,14 @@
     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 (* [simp] CANDIDATE *):
     1.8 +lemma bounded_iff [simp]:
     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  lemma strict_boundedE:
    1.13    assumes "a \<prec> b * c"
    1.14    obtains "a \<prec> b" and "a \<prec> c"
    1.15 -  using assms by (auto simp add: commute strict_iff_order bounded_iff elim: orderE intro!: that)+
    1.16 +  using assms by (auto simp add: commute strict_iff_order elim: orderE intro!: that)+
    1.17  
    1.18  lemma coboundedI1:
    1.19    "a \<preceq> c \<Longrightarrow> a * b \<preceq> c"
    1.20 @@ -128,10 +128,10 @@
    1.21    by (blast intro: boundedI coboundedI1 coboundedI2)
    1.22  
    1.23  lemma absorb1: "a \<preceq> b \<Longrightarrow> a * b = a"
    1.24 -  by (rule antisym) (auto simp add: bounded_iff refl)
    1.25 +  by (rule antisym) (auto simp add: refl)
    1.26  
    1.27  lemma absorb2: "b \<preceq> a \<Longrightarrow> a * b = b"
    1.28 -  by (rule antisym) (auto simp add: bounded_iff refl)
    1.29 +  by (rule antisym) (auto simp add: refl)
    1.30  
    1.31  lemma absorb_iff1: "a \<preceq> b \<longleftrightarrow> a * b = a"
    1.32    using order_iff by auto
    1.33 @@ -210,13 +210,13 @@
    1.34  lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
    1.35    by (blast intro: order_trans inf_le1 inf_le2)
    1.36  
    1.37 -lemma le_inf_iff [simp]:
    1.38 +lemma le_inf_iff:
    1.39    "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
    1.40    by (blast intro: le_infI elim: le_infE)
    1.41  
    1.42  lemma le_iff_inf:
    1.43    "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
    1.44 -  by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
    1.45 +  by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1] simp add: le_inf_iff)
    1.46  
    1.47  lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
    1.48    by (fast intro: inf_greatest le_infI1 le_infI2)
    1.49 @@ -247,13 +247,13 @@
    1.50    "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
    1.51    by (blast intro: order_trans sup_ge1 sup_ge2)
    1.52  
    1.53 -lemma le_sup_iff [simp]:
    1.54 +lemma le_sup_iff:
    1.55    "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
    1.56    by (blast intro: le_supI elim: le_supE)
    1.57  
    1.58  lemma le_iff_sup:
    1.59    "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
    1.60 -  by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
    1.61 +  by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1] simp add: le_sup_iff)
    1.62  
    1.63  lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
    1.64    by (fast intro: sup_least le_supI1 le_supI2)
    1.65 @@ -275,11 +275,11 @@
    1.66  proof
    1.67    fix a b c
    1.68    show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"
    1.69 -    by (rule antisym) (auto intro: le_infI1 le_infI2)
    1.70 +    by (rule antisym) (auto intro: le_infI1 le_infI2 simp add: le_inf_iff)
    1.71    show "a \<sqinter> b = b \<sqinter> a"
    1.72 -    by (rule antisym) auto
    1.73 +    by (rule antisym) (auto simp add: le_inf_iff)
    1.74    show "a \<sqinter> a = a"
    1.75 -    by (rule antisym) auto
    1.76 +    by (rule antisym) (auto simp add: le_inf_iff)
    1.77  qed
    1.78  
    1.79  sublocale inf!: semilattice_order inf less_eq less
    1.80 @@ -320,11 +320,11 @@
    1.81  proof
    1.82    fix a b c
    1.83    show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"
    1.84 -    by (rule antisym) (auto intro: le_supI1 le_supI2)
    1.85 +    by (rule antisym) (auto intro: le_supI1 le_supI2 simp add: le_sup_iff)
    1.86    show "a \<squnion> b = b \<squnion> a"
    1.87 -    by (rule antisym) auto
    1.88 +    by (rule antisym) (auto simp add: le_sup_iff)
    1.89    show "a \<squnion> a = a"
    1.90 -    by (rule antisym) auto
    1.91 +    by (rule antisym) (auto simp add: le_sup_iff)
    1.92  qed
    1.93  
    1.94  sublocale sup!: semilattice_order sup greater_eq greater