Theory MLSS_Semantics

theory MLSS_Semantics
  imports MLSS_Logic HereditarilyFinite.Finitary "HOL-Library.Adhoc_Overloading"
begin

section ‹Definition of MLSS›
text ‹
  Here, we define the syntax and semantics of multi-level syllogistic
  with singleton (MLSS). Additionally, we define a number of functions
  working on the syntax such as a function that collects all the subterms
  of a term.
›

subsection ‹Syntax and Semantics›

datatype (vars_term: 'a) pset_term = 
  Empty nat | is_Var: Var 'a |
  Union "'a pset_term" "'a pset_term" |
  Inter "'a pset_term" "'a pset_term" |
  Diff "'a pset_term" "'a pset_term" |
  Single "'a pset_term"

datatype (vars_atom: 'a) pset_atom =
  Elem "'a pset_term" "'a pset_term" | 
  Equal "'a pset_term" "'a pset_term"

bundle mlss_notation
begin

notation Empty (‹∅ _›)
notation Union (infixr ‹⊔⇩s› 165)
notation Inter (infixr ‹⊓⇩s› 170)
notation Diff (infixl ‹-⇩s› 180)

notation Elem (infix ‹∈⇩s› 150)
notation Equal (infix ‹=⇩s› 150)

end

bundle mlss_no_notation
begin

no_notation Empty (‹∅ _›)
no_notation Union (infixr ‹⊔⇩s› 165)
no_notation Inter (infixr ‹⊓⇩s› 170)
no_notation Diff (infixl ‹-⇩s› 180)

no_notation Elem (infix ‹∈⇩s› 150)
no_notation Equal (infix ‹=⇩s› 150)

end

unbundle mlss_notation


abbreviation "AT a ≡ Atom a"
abbreviation "AF a ≡ Neg (Atom a)"

type_synonym 'a pset_fm = "'a pset_atom fm"
type_synonym 'a branch = "'a pset_fm list"

fun I⇩s⇩t :: "('a ⇒ hf) ⇒ 'a pset_term ⇒ hf" where
  "I⇩s⇩t v (∅ n) = 0"
| "I⇩s⇩t v (Var x) = v x"
| "I⇩s⇩t v (s1 ⊔⇩s s2) = I⇩s⇩t v s1 ⊔ I⇩s⇩t v s2"
| "I⇩s⇩t v (s1 ⊓⇩s s2) = I⇩s⇩t v s1 ⊓ I⇩s⇩t v s2"
| "I⇩s⇩t v (s1 -⇩s s2) = I⇩s⇩t v s1 - I⇩s⇩t v s2"
| "I⇩s⇩t v (Single s) = HF {I⇩s⇩t v s}"

fun I⇩s⇩a :: "('a ⇒ hf) ⇒ 'a pset_atom ⇒ bool" where
  "I⇩s⇩a v (t1 ∈⇩s t2) ⟷ I⇩s⇩t v t1 ❙∈ I⇩s⇩t v t2"
| "I⇩s⇩a v (t1 =⇩s t2) ⟷ I⇩s⇩t v t1 = I⇩s⇩t v t2"


subsection ‹Variables›

definition vars_fm :: "'a pset_fm ⇒ 'a set" where
  "vars_fm φ ≡ ⋃(vars_atom ` atoms φ)"

definition vars_branch :: "'a branch ⇒ 'a set" where
  "vars_branch b ≡ ⋃(vars_fm ` set b)"

consts vars :: "'b ⇒ 'a set"
adhoc_overloading
  vars vars_term and
  vars vars_atom and
  vars vars_fm and
  vars vars_branch

lemma vars_fm_simps[simp]:
  "vars (Atom a) = vars a"
  "vars (And p q) = vars p ∪ vars q"
  "vars (Or p q) = vars p ∪ vars q"
  "vars (Neg p) = vars p"
  unfolding vars_fm_def
     apply(auto)
  done

lemma vars_fmI:
  "x ∈ vars p ⟹ x ∈ vars (And p q)"
  "x ∈ vars q ⟹ x ∈ vars (And p q)"
  "x ∈ vars p ⟹ x ∈ vars (Or p q)"
  "x ∈ vars q ⟹ x ∈ vars (Or p q)"
  "x ∈ vars p ⟹ x ∈ vars (Neg p)"
  by auto

lemma vars_branch_simps:
  "vars [] = {}"
  "vars (x # xs) = vars x ∪ vars xs"
  unfolding vars_branch_def by auto

lemma vars_branch_append:
  "vars (b1 @ b2) = vars b1 ∪ vars b2"
  unfolding vars_branch_def by simp

lemma vars_fm_vars_branchI:
  "φ ∈ set b ⟹ x ∈ vars_fm φ ⟹ x ∈ vars_branch b"
  unfolding vars_branch_def by blast


subsection ‹Subformulae and Subterms›

subsubsection ‹Subformulae›

fun subfms :: "'a fm ⇒ 'a fm set"  where
  "subfms (Atom a) = {Atom a}"
| "subfms (And p q) = {And p q} ∪ subfms p ∪ subfms q"
| "subfms (Or p q) = {Or p q} ∪ subfms p ∪ subfms q"
| "subfms (Neg q) = {Neg q} ∪ subfms q"

definition subfms_branch :: "'a fm list ⇒ 'a fm set" where
  "subfms_branch b ≡ ⋃(subfms ` set b)"

lemma subfms_branch_simps:
  "subfms_branch [] = {}"
  "subfms_branch (x # xs) = subfms x ∪ subfms_branch xs"
  unfolding subfms_branch_def by auto

lemma subfms_refl[simp]: "p ∈ subfms p"
  by (cases p) auto

lemma subfmsI:
  "a ∈ subfms p ⟹ a ∈ subfms (And p q)"
  "a ∈ subfms q ⟹ a ∈ subfms (And p q)"
  "a ∈ subfms p ⟹ a ∈ subfms (Or p q)"
  "a ∈ subfms q ⟹ a ∈ subfms (Or p q)"
  "a ∈ subfms p ⟹ a ∈ subfms (Neg p)"
  by auto

lemma subfms_trans: "q ∈ subfms p ⟹ p ∈ subfms r ⟹ q ∈ subfms r"
  by (induction r) auto

lemma subfmsD:
  "And p q ∈ subfms φ ⟹ p ∈ subfms φ"
  "And p q ∈ subfms φ ⟹ q ∈ subfms φ"
  "Or p q ∈ subfms φ ⟹ p ∈ subfms φ"
  "Or p q ∈ subfms φ ⟹ q ∈ subfms φ"
  "Neg p ∈ subfms φ ⟹ p ∈ subfms φ"
  using subfmsI subfms_refl subfms_trans by metis+


subsubsection ‹Subterms›

fun subterms_term :: "'a pset_term ⇒ 'a pset_term set"  where
  "subterms_term (∅ n) = {∅ n}"
| "subterms_term (Var i) = {Var i}"
| "subterms_term (t1 ⊔⇩s t2) = {t1 ⊔⇩s t2} ∪ subterms_term t1 ∪ subterms_term t2"
| "subterms_term (t1 ⊓⇩s t2) = {t1 ⊓⇩s t2} ∪ subterms_term t1 ∪ subterms_term t2"
| "subterms_term (t1 -⇩s t2) = {t1 -⇩s t2} ∪ subterms_term t1 ∪ subterms_term t2"
| "subterms_term (Single t) = {Single t} ∪ subterms_term t"

fun subterms_atom :: "'a pset_atom ⇒ 'a pset_term set"  where
  "subterms_atom (t1 ∈⇩s t2) = subterms_term t1 ∪ subterms_term t2"
| "subterms_atom (t1 =⇩s t2) = subterms_term t1 ∪ subterms_term t2"

definition subterms_fm :: "'a pset_fm ⇒ 'a pset_term set" where
 "subterms_fm φ ≡ ⋃(subterms_atom ` atoms φ)"

definition subterms_branch :: "'a branch ⇒ 'a pset_term set" where
  "subterms_branch b ≡ ⋃(subterms_fm ` set b)"

consts subterms :: "'a ⇒ 'b set"
adhoc_overloading 
  subterms subterms_term and
  subterms subterms_atom and
  subterms subterms_fm and
  subterms subterms_branch

lemma subterms_fm_simps[simp]:
  "subterms (Atom a) = subterms a"
  "subterms (And p q) = subterms p ∪ subterms q"
  "subterms (Or p q) = subterms p ∪ subterms q"
  "subterms (Neg p) = subterms p"
  unfolding subterms_fm_def by auto

lemma subterms_branch_simps:
  "subterms [] = {}"
  "subterms (x # xs) = subterms x ∪ subterms xs"
  unfolding subterms_branch_def by auto

lemma subterms_refl[simp]:
  "t ∈ subterms t"
  by (induction t) auto

lemma subterms_term_subterms_term_trans:
  "s ∈ subterms_term t ⟹ t ∈ subterms_term v ⟹ s ∈ subterms_term v"
  apply(induction v)
       apply(auto)
  done

lemma subterms_term_subterms_atom_trans:
  "s ∈ subterms_term t ⟹ t ∈ subterms_atom v ⟹ s ∈ subterms_atom v"
  apply(cases v rule: subterms_atom.cases)
  using subterms_term_subterms_term_trans by auto

lemma subterms_term_subterms_fm_trans:
  "s ∈ subterms_term t ⟹ t ∈ subterms_fm φ ⟹ s ∈ subterms_fm φ"
  apply(induction φ)
     apply(auto simp: subterms_term_subterms_atom_trans)
  done

lemma subterms_fmD:
  "t1 ⊔⇩s t2 ∈ subterms_fm φ ⟹ t1 ∈ subterms_fm φ"
  "t1 ⊔⇩s t2 ∈ subterms_fm φ ⟹ t2 ∈ subterms_fm φ"
  "t1 ⊓⇩s t2 ∈ subterms_fm φ ⟹ t1 ∈ subterms_fm φ"
  "t1 ⊓⇩s t2 ∈ subterms_fm φ ⟹ t2 ∈ subterms_fm φ"
  "t1 -⇩s t2 ∈ subterms_fm φ ⟹ t1 ∈ subterms_fm φ"
  "t1 -⇩s t2 ∈ subterms_fm φ ⟹ t2 ∈ subterms_fm φ"
  "Single t ∈ subterms_fm φ ⟹ t ∈ subterms_fm φ"
  by (metis UnCI subterms_term.simps subterms_refl subterms_term_subterms_fm_trans)+

lemma subterms_branchD:
  "t1 ⊔⇩s t2 ∈ subterms_branch b ⟹ t1 ∈ subterms_branch b"
  "t1 ⊔⇩s t2 ∈ subterms_branch b ⟹ t2 ∈ subterms_branch b"
  "t1 ⊓⇩s t2 ∈ subterms_branch b ⟹ t1 ∈ subterms_branch b"
  "t1 ⊓⇩s t2 ∈ subterms_branch b ⟹ t2 ∈ subterms_branch b"
  "t1 -⇩s t2 ∈ subterms_branch b ⟹ t1 ∈ subterms_branch b"
  "t1 -⇩s t2 ∈ subterms_branch b ⟹ t2 ∈ subterms_branch b"
  "Single t ∈ subterms_branch b ⟹ t ∈ subterms_branch b"
  unfolding subterms_branch_def using subterms_fmD by fast+

lemma subterms_term_subterms_branch_trans:
  "s ∈ subterms_term t ⟹ t ∈ subterms_branch b ⟹ s ∈ subterms_branch b"
  unfolding subterms_branch_def using subterms_term_subterms_fm_trans by blast

lemma AT_mem_subterms_branchD:
  assumes "AT (s ∈⇩s t) ∈ set b"
  shows "s ∈ subterms b" "t ∈ subterms b"
  using assms unfolding subterms_branch_def by force+

lemma AF_mem_subterms_branchD:
  assumes "AF (s ∈⇩s t) ∈ set b"
  shows "s ∈ subterms b" "t ∈ subterms b"
  using assms unfolding subterms_branch_def by force+

lemma AT_eq_subterms_branchD:
  assumes "AT (s =⇩s t) ∈ set b"
  shows "s ∈ subterms b" "t ∈ subterms b"
  using assms unfolding subterms_branch_def by force+

lemma AF_eq_subterms_branchD:
  assumes "AF (s =⇩s t) ∈ set b"
  shows "s ∈ subterms b" "t ∈ subterms b"
  using assms unfolding subterms_branch_def by force+


subsubsection ‹Interactions between Subterms and Subformulae›

lemma Un_vars_term_subterms_term_eq_vars_term:
  "⋃(vars_term ` subterms t) = vars_term t"
  by (induction t) auto

lemma Un_vars_term_subterms_fm_eq_vars_fm:
  "⋃(vars_term ` subterms_fm φ) = vars_fm φ"
proof(induction φ)
  case (Atom a)
  then show ?case
    by (cases a) (auto simp: Un_vars_term_subterms_term_eq_vars_term)
qed (fastforce)+

lemma Un_vars_term_subterms_branch_eq_vars_branch:
  "⋃(vars_term ` subterms_branch b) = vars_branch b"
  using Un_vars_term_subterms_fm_eq_vars_fm
  unfolding vars_branch_def subterms_branch_def
  by force

lemma subs_vars_branch_if_subs_subterms_branch:
  "subterms_branch b1 ⊆ subterms_branch b2 ⟹ vars_branch b1 ⊆ vars_branch b2"
  using Un_vars_term_subterms_branch_eq_vars_branch
  by (metis complete_lattice_class.Sup_subset_mono subset_image_iff)

lemma subterms_branch_eq_if_vars_branch_eq:
  "subterms_branch b1 = subterms_branch b2 ⟹ vars_branch b1 = vars_branch b2"
  using subs_vars_branch_if_subs_subterms_branch by blast

lemma mem_vars_term_if_mem_subterms_term:
  "x ∈ vars_term s ⟹ s ∈ subterms_term t ⟹ x ∈ vars_term t"
  apply(induction t)
       apply(auto intro: pset_term.set_intros)
  done

lemma mem_vars_fm_if_mem_subterms_fm:
  "x ∈ vars_term s ⟹ s ∈ subterms_fm φ ⟹ x ∈ vars_fm φ"
proof(induction φ)
  case (Atom a)
  then show ?case
    by (cases a) (auto simp: mem_vars_term_if_mem_subterms_term)
qed (auto simp: vars_fm_def)


lemma vars_term_subs_subterms_term:
  "v ∈ vars_term t ⟹ Var v ∈ subterms_term t"
  apply(induction t)
       apply(auto)
  done

lemma vars_atom_subs_subterms_atom:
  "v ∈ vars_atom a ⟹ Var v ∈ subterms_atom a"
  apply(cases a)
   apply(auto simp: vars_term_subs_subterms_term)
  done

lemma vars_fm_subs_subterms_fm:
  "v ∈ vars_fm φ ⟹ Var v ∈ subterms_fm φ"
  apply(induction φ)
     apply(auto simp: vars_atom_subs_subterms_atom)
  done

lemma vars_branch_subs_subterms_branch:
  "Var ` vars_branch b ⊆ subterms_branch b"
  unfolding vars_branch_def subterms_branch_def
  apply(auto simp: vars_fm_subs_subterms_fm)
  done

lemma subterms_term_subterms_atom_Atom_trans:
  "Atom a ∈ set b ⟹ x ∈ subterms_term s ⟹ s ∈ subterms_atom a ⟹ x ∈ subterms_branch b"
  unfolding subterms_branch_def
  by (metis UN_I subterms_fm_simps(1) subterms_term_subterms_atom_trans)

lemma subterms_branch_subterms_subterms_fm_trans:
  "b ≠ [] ⟹ x ∈ subterms_term t ⟹ t ∈ subterms_fm (last b) ⟹ x ∈ subterms_branch b"
  using subterms_branch_def subterms_term_subterms_fm_trans by fastforce


subsubsection ‹Set Atoms in a Branch›

abbreviation pset_atoms_branch :: "'a fm list ⇒ 'a set" where
  "pset_atoms_branch b ≡ ⋃(atoms ` set b)"

section ‹Finiteness›

lemma finite_vars_term: "finite (vars_term t)"
  apply(induction t)
       apply(auto)
  done

lemma finite_vars_atom: "finite (vars_atom a)"
  apply(cases a)
   apply(auto simp: finite_vars_term)
  done

lemma finite_vars_fm: "finite (vars_fm φ)"
  apply(induction φ)
     apply(auto simp: finite_vars_atom)
  done

lemma finite_vars_branch: "finite (vars_branch b)"
  apply(induction b)
   apply(auto simp: vars_branch_def finite_vars_fm)
  done

lemma finite_subterms_term: "finite (subterms_term l)"
  apply(induction l)
       apply(auto)
  done

lemma finite_subterms_atom: "finite (subterms_atom l)"
  apply(cases l rule: subterms_atom.cases)
   apply(auto simp: finite_subterms_term)
  done

lemma finite_subterms_fm: "finite (subterms_fm φ)"
  apply(induction φ)
     apply(auto simp: finite_subterms_atom)
  done

lemma finite_subterms_branch: "finite (subterms_branch b)"
  apply(induction b)
   apply(auto simp: subterms_branch_def finite_subterms_fm)
  done

lemma finite_subfms: "finite (subfms φ)"
  apply(induction φ)
     apply(auto)
  done

lemma finite_subfms_branch: "finite (subfms_branch b)"
  by (induction b) (auto simp: subfms_branch_simps finite_subfms)

lemma finite_atoms: "finite (atoms φ)"
  by (induction φ) auto

lemma finite_pset_atoms_branch: "finite (pset_atoms_branch b)"
  by (auto simp: finite_atoms)

subsection ‹Non-Emptiness›

lemma subterms_term_nonempty[simp]: "subterms_term t ≠ {}"
  by (induction t) auto

lemma subterms_atom_nonempty[simp]: "subterms_atom l ≠ {}"
  by (cases l rule: subterms_atom.cases) auto

lemma subterms_fm_nonempty[simp]: "subterms_fm φ ≠ {}"
  by (induction φ) auto

end