Theory MLSS_Logic

theory MLSS_Logic
  imports Main
begin

section ‹Propositional formulae›
text ‹
  This theory contains syntax and semantics of propositional formulae.
›

datatype (atoms: 'a) fm =
  is_Atom: Atom 'a | And "'a fm" "'a fm" | Or "'a fm" "'a fm" |
  Neg "'a fm"

fun "interp" :: "('model ⇒ 'a ⇒ bool) ⇒ 'model ⇒ 'a fm ⇒ bool" where
  "interp I⇩a M (Atom a) = I⇩a M a" |
  "interp I⇩a M (And φ⇩1 φ⇩2) = (interp I⇩a M φ⇩1 ∧ interp I⇩a M φ⇩2)" |
  "interp I⇩a M (Or φ⇩1 φ⇩2) = (interp I⇩a M φ⇩1 ∨ interp I⇩a M φ⇩2)" |
  "interp I⇩a M (Neg φ) = (¬ interp I⇩a M φ)"

locale ATOM =
  fixes I⇩a :: "'model ⇒ 'a ⇒ bool"
begin

abbreviation I where "I ≡ interp I⇩a"

end

definition "Atoms A ≡ {a |a. Atom a ∈ A}"

lemma Atoms_Un[simp]: "Atoms (A ∪ B) = Atoms A ∪ Atoms B"
  unfolding Atoms_def by auto

lemma Atoms_mono: "A ⊆ B ⟹ Atoms A ⊆ Atoms B"
  unfolding Atoms_def by auto

end