Theory DataRefinementIBP.Preliminaries

section ‹Preliminaries›

theory Preliminaries
imports Main LatticeProperties.Complete_Lattice_Prop 
  LatticeProperties.Conj_Disj
begin

notation
  less_eq (infix "⊑" 50) and
  less (infix "⊏" 50) and
  inf (infixl "⊓" 70) and
  sup (infixl "⊔" 65) and
  top ("⊤") and
  bot ("⊥") and
  Inf ("⨅_" [900] 900) and
  Sup ("⨆_" [900] 900)

subsection ‹Simplification Lemmas›

declare fun_upd_idem[simp]

lemma simp_eq_emptyset:
  "(X = {}) = (∀ x. x ∉ X)"
  by blast

lemma mono_comp: "mono f ⟹ mono g ⟹ mono (f o g)" 
  by (unfold mono_def) auto

text ‹Some lattice simplification rules›

lemma inf_bot_bot: (* FIXME *)
  "(x::'a::{semilattice_inf,order_bot}) ⊓ ⊥ = ⊥"
  apply (rule antisym)
  by auto

end