src/HOL/Lattices.thy
changeset 21312 1d39091a3208
parent 21249 d594c58e24ed
child 21381 79e065f2be95
     1.1 --- a/src/HOL/Lattices.thy	Sat Nov 11 23:58:46 2006 +0100
     1.2 +++ b/src/HOL/Lattices.thy	Sun Nov 12 19:22:10 2006 +0100
     1.3 @@ -18,12 +18,12 @@
     1.4  
     1.5  locale lower_semilattice = partial_order +
     1.6    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
     1.7 -  assumes inf_le1: "x \<sqinter> y \<sqsubseteq> x" and inf_le2: "x \<sqinter> y \<sqsubseteq> y"
     1.8 +  assumes inf_le1[simp]: "x \<sqinter> y \<sqsubseteq> x" and inf_le2[simp]: "x \<sqinter> y \<sqsubseteq> y"
     1.9    and inf_least: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    1.10  
    1.11  locale upper_semilattice = partial_order +
    1.12    fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    1.13 -  assumes sup_ge1: "x \<sqsubseteq> x \<squnion> y" and sup_ge2: "y \<sqsubseteq> x \<squnion> y"
    1.14 +  assumes sup_ge1[simp]: "x \<sqsubseteq> x \<squnion> y" and sup_ge2[simp]: "y \<sqsubseteq> x \<squnion> y"
    1.15    and sup_greatest: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
    1.16  
    1.17  locale lattice = lower_semilattice + upper_semilattice