Theory Literal_Functor

theory Literal_Functor
  imports
    Abstract_Substitution.Natural_Functor
    Saturation_Framework_Extensions.Clausal_Calculus
begin

setup natural_functor_setups

lemma literal_cases: "⟦𝒫 ∈ {Pos, Neg}; 𝒫 = Pos ⟹ P; 𝒫 = Neg ⟹ P⟧ ⟹ P"
  by blast

lemma literals_distinct [simp]: "Pos ≠ Neg" "Neg ≠ Pos"
  by (metis literal.distinct(1))+

lemma set_literal_not_empty [iff]: "set_literal l ≠ {}"
  by (cases l) simp_all

global_interpretation literal_functor: natural_functor_conversion where
  map = map_literal and to_set = set_literal and map_to = map_literal and map_from = map_literal and
  map' = map_literal and to_set' = set_literal
  by unfold_locales (auto simp: literal.set_map literal.map_comp)

end