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