Theory Formula

(* Author: Dmitriy Traytel *)

section ‹Monadic Second-Order Logic Formulas›

(*<*)
theory Formula
imports Pi_Regular_Operators List_More
begin
(*>*)

subsection ‹Interpretations and Encodings›

type_synonym 'a interp = "'a list × (nat + nat set) list"

abbreviation "enc_atom_bool I n ≡ map (λx. case x of Inl p ⇒ n = p | Inr P ⇒ n ∈ P) I"

abbreviation "enc_atom I n a ≡ (a, enc_atom_bool I n)"

subsection ‹Syntax and Semantics of MSO›

datatype 'a formula =
  FQ 'a nat
| FLess nat nat
| FIn nat nat
| FNot "'a formula"
| FOr "'a formula" "'a formula"
| FAnd "'a formula" "'a formula"
| FExists "'a formula"
| FEXISTS "'a formula"

primrec FOV :: "'a formula ⇒ nat set" where
  "FOV (FQ a m) = {m}"
| "FOV (FLess m1 m2) = {m1, m2}"
| "FOV (FIn m M) = {m}"
| "FOV (FNot φ) = FOV φ"
| "FOV (FOr φ⇩1 φ⇩2) = FOV φ⇩1 ∪ FOV φ⇩2"
| "FOV (FAnd φ⇩1 φ⇩2) = FOV φ⇩1 ∪ FOV φ⇩2"
| "FOV (FExists φ) = (λx. x - 1) ` (FOV φ - {0})"
| "FOV (FEXISTS φ) = (λx. x - 1) ` FOV φ"

primrec SOV :: "'a formula ⇒ nat set" where
  "SOV (FQ a m) = {}"
| "SOV (FLess m1 m2) = {}"
| "SOV (FIn m M) = {M}"
| "SOV (FNot φ) = SOV φ"
| "SOV (FOr φ⇩1 φ⇩2) = SOV φ⇩1 ∪ SOV φ⇩2"
| "SOV (FAnd φ⇩1 φ⇩2) = SOV φ⇩1 ∪ SOV φ⇩2"
| "SOV (FExists φ) = (λx. x - 1) ` SOV φ"
| "SOV (FEXISTS φ) = (λx. x - 1) ` (SOV φ - {0})"

definition "σ = (λΣ n. concat (map (λbs. map (λa. (a, bs)) Σ) (List.n_lists n [True, False])))"
definition "π = (λ(a, bs). (a, tl bs))"
definition "ε = (λΣ (a::'a, bs). if a ∈ set Σ then [(a, True # bs), (a, False # bs)] else [])"

datatype 'a atom =
    Singleton 'a "bool list"
  | AQ nat 'a
  | Arbitrary_Except nat bool
  | Arbitrary_Except2 nat nat
derive linorder atom

fun wf_atom where
  "wf_atom Σ n (Singleton a bs) = (a ∈ set Σ ∧ length bs = n)"
| "wf_atom Σ n (AQ m a) = (a ∈ set Σ ∧ m < n)"
| "wf_atom Σ n (Arbitrary_Except m _) = (m < n)"
| "wf_atom Σ n (Arbitrary_Except2 m1 m2) = (m1 < n ∧ m2 < n)"

fun lookup where
  "lookup (Singleton a' bs') (a, bs) = (a = a' ∧ bs = bs')"
| "lookup (AQ m a') (a, bs) = (a = a' ∧ bs ! m)"
| "lookup (Arbitrary_Except m b) (_, bs) = (bs ! m = b)"
| "lookup (Arbitrary_Except2 m1 m2) (_, bs) = (bs ! m1 ∧ bs ! m2)"

lemma π_σ: "π ` (set o σ Σ) (n + 1) = (set o σ Σ) n"
  unfolding π_def σ_def set_map[symmetric] o_apply map_concat by auto

locale formula = embed2 "set o (σ Σ)" "wf_atom Σ" π lookup "ε Σ" "case_prod Singleton"
for Σ :: "'a :: linorder list" +
assumes nonempty: "Σ ≠ []"
begin

abbreviation "Σ_product_lists n ≡
   List.maps (λbools. map (λa. (a, bools)) Σ) (bool_product_lists n)"

(* Normal form: quantified variables are used in the body *)
primrec pre_wf_formula :: "nat ⇒ 'a formula ⇒ bool" where
  "pre_wf_formula n (FQ a m) = (a ∈ set Σ ∧ m < n)"
| "pre_wf_formula n (FLess m1 m2) = (m1 < n ∧ m2 < n)"
| "pre_wf_formula n (FIn m M) = (m < n ∧ M < n)"
| "pre_wf_formula n (FNot φ) = pre_wf_formula n φ"
| "pre_wf_formula n (FOr φ⇩1 φ⇩2) = (pre_wf_formula n φ⇩1 ∧ pre_wf_formula n φ⇩2)"
| "pre_wf_formula n (FAnd φ⇩1 φ⇩2) = (pre_wf_formula n φ⇩1 ∧ pre_wf_formula n φ⇩2)"
| "pre_wf_formula n (FExists φ) = (pre_wf_formula (n + 1) φ ∧ 0 ∈ FOV φ ∧ 0 ∉ SOV φ)"
| "pre_wf_formula n (FEXISTS φ) = (pre_wf_formula (n + 1) φ ∧ 0 ∉ FOV φ ∧ 0 ∈ SOV φ)"

abbreviation "closed ≡ pre_wf_formula 0"

definition [simp]: "wf_formula n φ ≡ pre_wf_formula n φ ∧ FOV φ ∩ SOV φ = {}"

lemma max_idx_vars: "pre_wf_formula n φ ⟹ ∀p ∈ FOV φ ∪ SOV φ. p < n"
  by (induct φ arbitrary: n)
   (auto split: if_split_asm, (metis Un_iff diff_Suc_less less_SucE less_imp_diff_less)+)

lemma finite_FOV: "finite (FOV φ)"
  by (induct φ) (auto split: if_split_asm)

subsection ‹ENC›

definition valid_ENC :: "nat ⇒ nat ⇒ ('a atom) rexp" where
  "valid_ENC n p = (if n = 0 then Full else
    TIMES [
      Star (Atom (Arbitrary_Except p False)),
      Atom (Arbitrary_Except p True),
      Star (Atom (Arbitrary_Except p False))])"

lemma wf_rexp_valid_ENC: "n = 0 ∨ p < n ⟹ wf n (valid_ENC n p)"
  unfolding valid_ENC_def by auto

definition ENC :: "nat ⇒ nat set ⇒ ('a atom) rexp" where
  "ENC n V = flatten INTERSECT (valid_ENC n ` V)"

lemma wf_rexp_ENC: "⟦finite V; n = 0 ∨ (∀v ∈ V. v < n)⟧ ⟹ wf n (ENC n V)"
  unfolding ENC_def
  by (intro iffD2[OF wf_flatten_INTERSECT]) (auto simp: wf_rexp_valid_ENC)

lemma enc_atom_σ_eq: "i < length w ⟹
 (length I = n ∧ p ∈ set Σ) ⟷ enc_atom I i p ∈ set (σ Σ n)"
  by (auto simp: σ_def set_n_lists intro!: exI[of _ "enc_atom_bool I i"] imageI)

lemmas enc_atom_σ = iffD1[OF enc_atom_σ_eq, OF _ conjI]

lemma enc_atom_bool_take_drop_True:
  "⟦r < length I; case I ! r of Inl p' ⇒ p = p' | Inr P ⇒ p ∈ P⟧ ⟹
    enc_atom_bool I p = take r (enc_atom_bool I p) @ True # drop (Suc r) (enc_atom_bool I p)"
  by (auto intro: trans[OF id_take_nth_drop])

lemma enc_atom_bool_take_drop_True2:
  "⟦r < length I; case I ! r of Inl p' ⇒ p = p' | Inr P ⇒ p ∈ P;
    s < length I; case I ! s of Inl p' ⇒ p = p' | Inr P ⇒ p ∈ P; r < s⟧ ⟹
    enc_atom_bool I p = take r (enc_atom_bool I p) @ True #
      take (s - Suc r) (drop (Suc r) (enc_atom_bool I p)) @ True #
      drop (Suc s) (enc_atom_bool I p)"
  using id_take_nth_drop[of r "enc_atom_bool I p"]
      id_take_nth_drop[of "s - r - 1" "drop (Suc r) (enc_atom_bool I p)"]
  by auto

lemma enc_atom_bool_take_drop_False:
  "⟦r < length I; case I ! r of Inl p' ⇒ p ≠ p' | Inr P ⇒ p ∉ P⟧ ⟹
    enc_atom_bool I p = take r (enc_atom_bool I p) @ False # drop (Suc r) (enc_atom_bool I p)"
  by (auto intro: trans[OF id_take_nth_drop] split: sum.splits)

lemma enc_atom_lang_AQ: "⟦r < length I;
   case I ! r of Inl p' ⇒ p = p' | Inr P ⇒ p ∈ P; length I = n; a ∈ set Σ⟧ ⟹
  [enc_atom I p a] ∈ lang n (Atom (AQ r a))"
  unfolding lang.simps
  by (force intro!: enc_atom_bool_take_drop_True
    image_eqI[of _ _ "(λJ. take r J @ drop (r + 1) J) (enc_atom_bool I p)"]
    simp: σ_def set_n_lists)

lemma enc_atom_lang_Arbitrary_Except_True: "⟦r < length I;
   case I ! r of Inl p' ⇒ p = p' | Inr P ⇒ p ∈ P; length I = n; a ∈ set Σ⟧ ⟹
  [enc_atom I p a] ∈ lang n (Atom (Arbitrary_Except r True))"
  unfolding lang.simps
  by (force intro!: enc_atom_bool_take_drop_True
    image_eqI[of _ _ "(λJ. take r J @ drop (r + 1) J) (enc_atom_bool I p)"]
    simp: σ_def set_n_lists)

lemma enc_atom_lang_Arbitrary_Except2:"⟦r < length I; s < length I; 
  case I ! r of Inl p' ⇒ p = p' | Inr P ⇒ p ∈ P;
  case I ! s of Inl p' ⇒ p = p' | Inr P ⇒ p ∈ P; length I = n; a ∈ set Σ⟧ ⟹
  [enc_atom I p a] ∈ lang n (Atom (Arbitrary_Except2 r s))"
  unfolding lang.simps
  by (force intro!: enc_atom_bool_take_drop_True2
    simp: set_n_lists σ_def take_Cons' drop_Cons' numeral_eq_Suc)

lemma enc_atom_lang_Arbitrary_Except_False: "⟦r < length I;
  case I ! r of Inl p' ⇒ p ≠ p' | Inr P ⇒ p ∉ P; length I = n; a ∈ set Σ⟧ ⟹
  [enc_atom I p a] ∈ lang n (Atom (Arbitrary_Except r False))"
  unfolding lang.simps
  by (force intro!: enc_atom_bool_take_drop_False
    image_eqI[of _ _ "(λJ. take r J @ drop (r + 1) J) (enc_atom_bool I p)"]
    simp: set_n_lists σ_def split: sum.splits)

lemma AQ_D:
  assumes "v ∈ lang n (Atom (AQ m a))" "m < n" "a ∈ set Σ"
  shows "∃x. v = [x] ∧ fst x = a ∧ snd x ! m"
  using assms by auto

lemma Arbitrary_ExceptD:
  assumes "v ∈ lang n (Atom (Arbitrary_Except r b))" "r < n"
  shows "∃x. v = [x] ∧ snd x ! r = b"
  using assms by auto

lemma Arbitrary_Except2D:
  assumes "v ∈ lang n (Atom (Arbitrary_Except2 r s))" "r < n" "s < n"
  shows "∃x. v = [x] ∧ snd x ! r ∧ snd x ! s"
  using assms by auto

lemma star_Arbitrary_ExceptD:
  "⟦v ∈ star (lang n (Atom (Arbitrary_Except r b))); r < n; i < length v⟧ ⟹
    snd (v ! i) ! r = b"
proof (induct arbitrary: i rule: star_induct)
  case (append u v) thus ?case by (cases i) (auto dest: Arbitrary_ExceptD)
qed simp

end

end