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