Theory LatticeProperties.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