Theory MLSS_Extras

theory MLSS_Extras
  imports MLSS_Decision_Proc.MLSS_Semantics
begin

inductive normalized_MLSS_literal :: "'a pset_fm ⇒ bool" where
  eq_empty:
  "normalized_MLSS_literal (AT (Var x =⇩s ∅ n))"
| eq:
  "normalized_MLSS_literal (AT (Var x =⇩s Var y))"
| neq:
  "normalized_MLSS_literal (AF (Var x =⇩s Var y))"
| union: 
  "normalized_MLSS_literal (AT (Var x =⇩s Var y ⊔⇩s Var z))"
| diff:
  "normalized_MLSS_literal (AT (Var x =⇩s Var y -⇩s Var z))"
| singleton: 
  "normalized_MLSS_literal (AT (Var x =⇩s Single (Var y)))"

locale normalized_MLSS_clause =
    fixes 𝒞 :: "'a pset_fm set"
  assumes norm_𝒞: "∀lt ∈ 𝒞. normalized_MLSS_literal lt"
      and finite_𝒞: "finite 𝒞"
begin

―‹only valid for normalized literals›
fun singleton_vars :: "'a pset_fm ⇒ 'a set" where
  "singleton_vars (AT (Var x =⇩s Single (Var y))) = {y}"
| "singleton_vars _ = {}"

lemma singleton_vars_subset_vars: "singleton_vars φ ⊆ vars φ"
  apply (cases φ)
     apply simp_all
  by (smt (z3) Un_iff subset_iff empty_iff
      fm.inject(1) pset_atom.simps(16) pset_term.simps(92) pset_term.simps(96) singleton_vars.elims)

abbreviation "V ≡ ⋃ (vars ` 𝒞)"
abbreviation "W ≡ ⋃ (singleton_vars ` 𝒞)"

lemma W_subset_V: "W ⊆ V"
  using singleton_vars_subset_vars by fast

lemma memW_E[elim]:
  assumes "w ∈ W"
    shows "∃x. AT (Var x =⇩s Single (Var w)) ∈ 𝒞"
proof -
  from ‹w ∈ W› obtain lt where lt: "lt ∈ 𝒞" "w ∈ singleton_vars lt" by blast
  then obtain x where "lt = AT (Var x =⇩s Single (Var w))"
    by (cases lt rule: singleton_vars.cases) auto
  with lt show ?thesis by blast
qed

end

lemma AT_inj: "inj AT"
  by (standard; rule ccontr) auto

end