Theory M2L_Normalization

(* Author: Dmitriy Traytel *)

section ‹Normalization of M2L Formulas›

(*<*)
theory M2L_Normalization
imports M2L
begin
(*>*)

fun nNot where
  "nNot (FNot φ) = φ"
| "nNot (FAnd φ1 φ2) = FOr (nNot φ1) (nNot φ2)"
| "nNot (FOr φ1 φ2) = FAnd (nNot φ1) (nNot φ2)"
| "nNot φ = FNot φ"

primrec norm where
  "norm (FQ a m) = FQ a m"
| "norm (FLess m n) = FLess m n"
| "norm (FIn m M) = FIn m M"
| "norm (FOr φ ψ) = FOr (norm φ) (norm ψ)"
| "norm (FAnd φ ψ) = FAnd (norm φ) (norm ψ)"
| "norm (FNot φ) = nNot (norm φ)"
| "norm (FExists φ) = FExists (norm φ)"
| "norm (FEXISTS φ) = FEXISTS (norm φ)"

context formula
begin

lemma satisfies_nNot[simp]: "satisfies (w, I) (nNot φ) = satisfies (w,I) (FNot φ)"
  by (induct φ rule: nNot.induct) auto

lemma FOV_nNot[simp]: "FOV (nNot φ) = FOV (FNot φ)"
  by (induct φ rule: nNot.induct) auto

lemma SOV_nNot[simp]: "SOV (nNot φ) = SOV (FNot φ)"
  by (induct φ rule: nNot.induct) auto

lemma pre_wf_formula_nNot[simp]: "pre_wf_formula n (nNot φ) = pre_wf_formula n (FNot φ)"
  by (induct φ rule: nNot.induct) auto

lemma FOV_norm[simp]: "FOV (norm φ) = FOV φ"
  by (induct φ) auto

lemma SOV_norm[simp]: "SOV (norm φ) = SOV φ"
  by (induct φ) auto

lemma pre_wf_formula_norm[simp]: "pre_wf_formula n (norm φ) = pre_wf_formula n φ"
  by (induct φ arbitrary: n) auto

lemma satisfies_norm[simp]: "satisfies (w, I) (norm φ) = satisfies (w, I) φ"
  by (induct φ arbitrary: I) auto

lemma lang⇩_M⇩₂⇩_L_norm[simp]: "lang⇩_M⇩₂⇩_L n (norm φ) = lang⇩_M⇩₂⇩_L n φ"
  unfolding lang⇩_M⇩₂⇩_L_def by auto

end

(*<*)
end
(*>*)