Theory Lattice_Prop

section‹Simplification Lemmas for Lattices›

(*
    Author: Viorel Preoteasa
*)

theory Lattice_Prop
imports Main
begin

text‹
This theory introduces some simplification lemmas
for semilattices and lattices
›

notation 
   inf (infixl "⊓" 70) and
   sup (infixl "⊔" 65)

context semilattice_inf begin
lemma [simp]: "(x ⊓ y) ⊓ z ≤ x"
  by (metis inf_le1 order_trans)

lemma [simp]: "x ⊓ y ⊓ z ≤ y"
  by (rule_tac y = "x ⊓ y" in order_trans, rule inf_le1, simp)

lemma [simp]: "x ⊓ (y ⊓ z) ≤ y"
  by (rule_tac y = "y ⊓ z" in order_trans, rule inf_le2, simp)

lemma [simp]: "x ⊓ (y ⊓ z) ≤ z"
  by (rule_tac y = "y ⊓ z" in order_trans, rule inf_le2, simp)
end

context semilattice_sup begin

lemma [simp]: "x ≤ x ⊔ y ⊔ z"
  by (rule_tac y = "x ⊔ y" in order_trans, simp_all) 

lemma [simp]: "y ≤ x ⊔ y ⊔ z"
  by (rule_tac y = "x ⊔ y" in order_trans, simp_all)

lemma [simp]: "y ≤ x ⊔ (y ⊔ z)"
  by (rule_tac y = "y ⊔ z" in order_trans, simp_all)

lemma [simp]: "z ≤ x ⊔ (y ⊔ z)"
  by (rule_tac y = "y ⊔ z" in order_trans, simp_all)
end

context lattice begin

lemma [simp]: "x ⊓ y ≤ x ⊔ z"
  by (rule_tac y = x in order_trans, simp_all)

lemma [simp]: "y ⊓ x ≤ x ⊔ z"
  by (rule_tac y = x in order_trans, simp_all)

lemma [simp]: "x ⊓ y ≤ z ⊔ x"
  by (rule_tac y = x in order_trans, simp_all)

lemma [simp]: "y ⊓ x ≤ z ⊔ x"
  by (rule_tac y = x in order_trans, simp_all)

end

end