Theory WS1S_Normalization

(* Author: Dmitriy Traytel *)

section ‹Normalization of WS1S Formulas›

(*<*)
theory WS1S_Normalization
imports WS1S
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]: "(w, I) ⊨ nNot φ ⟷ (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]: "wI ⊨ norm φ ⟷ wI ⊨ φ"
  by (induct φ arbitrary: wI) auto

lemma lang⇩_W⇩_S⇩₁⇩_S_norm[simp]: "lang⇩_W⇩_S⇩₁⇩_S n (norm φ) = lang⇩_W⇩_S⇩₁⇩_S n φ"
  unfolding lang⇩_W⇩_S⇩₁⇩_S_def by auto

end

(*<*)
end
(*>*)