Theory Abstract_Formula

section ‹Derivatives of Abstract Formulas›
(* Author: Dmitriy Traytel *)

(*<*)
theory Abstract_Formula
imports
  Automaton
  Deriving.Compare_Instances
  "HOL-Library.Code_Target_Nat"
  While_Default
begin
(*>*)

subsection ‹Preliminaries›

lemma pred_Diff_0[simp]: "0 ∉ A ⟹ i ∈ (λx. x - Suc 0) ` A ⟷ Suc i ∈ A"
  by (cases i) (fastforce simp: image_iff le_Suc_eq  elim: contrapos_np)+

lemma funpow_cycle_mult: "(f ^^ k) x = x ⟹ (f ^^ (m * k)) x = x"
  by (induct m) (auto simp: funpow_add)

lemma funpow_cycle: "(f ^^ k) x = x ⟹ (f ^^ l) x = (f ^^ (l mod k)) x"
  by (subst div_mult_mod_eq[symmetric, of l k])
    (simp only: add.commute funpow_add funpow_cycle_mult o_apply)

lemma funpow_cycle_offset:
  fixes f :: "'a ⇒ 'a"
  assumes "(f ^^ k) x = (f ^^ i) x" "i ≤ k" "i ≤ l"
  shows "(f ^^ l) x = (f ^^ ((l - i) mod (k - i) + i)) x"
proof -
  from assms have
    "(f ^^ (k - i)) ((f ^^ i) x) = ((f ^^ i) x)"
    "(f ^^ l) x = (f ^^ (l - i)) ((f ^^ i) x)"
    unfolding fun_cong[OF funpow_add[symmetric, unfolded o_def]] by simp_all
  from funpow_cycle[OF this(1), of "l - i"] this(2) show ?thesis
    by (simp add: funpow_add)
qed

lemma in_set_tlD: "x ∈ set (tl xs) ⟹ x ∈ set xs"
  by (cases xs) auto

definition "dec k m = (if m > k then m - Suc 0 else m :: nat)"


subsection ‹Abstract formulas›

datatype (discs_sels) ('a, 'k) aformula =
  FBool bool
| FBase 'a
| FNot "('a, 'k) aformula"
| FOr "('a, 'k) aformula" "('a, 'k) aformula"
| FAnd "('a, 'k) aformula" "('a, 'k) aformula"
| FEx 'k "('a, 'k) aformula"
| FAll 'k "('a, 'k) aformula"
derive linorder aformula

fun nFOR where
  "nFOR [] = FBool False"
| "nFOR [x] = x"
| "nFOR (x # xs) = FOr x (nFOR xs)"

fun nFAND where
  "nFAND [] = FBool True"
| "nFAND [x] = x"
| "nFAND (x # xs) = FAnd x (nFAND xs)"

definition "NFOR = nFOR o sorted_list_of_set"
definition "NFAND = nFAND o sorted_list_of_set"

fun disjuncts where
  "disjuncts (FOr φ ψ) = disjuncts φ ∪ disjuncts ψ"
| "disjuncts φ = {φ}"

fun conjuncts where
  "conjuncts (FAnd φ ψ) = conjuncts φ ∪ conjuncts ψ"
| "conjuncts φ = {φ}"

fun disjuncts_list where
  "disjuncts_list (FOr φ ψ) = disjuncts_list φ @ disjuncts_list ψ"
| "disjuncts_list φ = [φ]"

fun conjuncts_list where
  "conjuncts_list (FAnd φ ψ) = conjuncts_list φ @ conjuncts_list ψ"
| "conjuncts_list φ = [φ]"

lemma finite_juncts[simp]: "finite (disjuncts φ)" "finite (conjuncts φ)"
  and nonempty_juncts[simp]: "disjuncts φ ≠ {}" "conjuncts φ ≠ {}"
  by (induct φ) auto

lemma juncts_eq_set_juncts_list:
  "disjuncts φ = set (disjuncts_list φ)"
  "conjuncts φ = set (conjuncts_list φ)"
  by (induct φ) auto

lemma notin_juncts:
  "⟦ψ ∈ disjuncts φ; is_FOr ψ⟧ ⟹ False"
  "⟦ψ ∈ conjuncts φ; is_FAnd ψ⟧ ⟹ False"
  by (induct φ) auto

lemma juncts_list_singleton:
  "¬ is_FOr φ ⟹ disjuncts_list φ = [φ]"
  "¬ is_FAnd φ ⟹ conjuncts_list φ = [φ]"
  by (induct φ) auto

lemma juncts_singleton:
  "¬ is_FOr φ ⟹ disjuncts φ = {φ}"
  "¬ is_FAnd φ ⟹ conjuncts φ = {φ}"
  by (induct φ) auto

lemma nonempty_juncts_list: "conjuncts_list φ ≠ []" "disjuncts_list φ ≠ []"
  using nonempty_juncts[of φ] by (auto simp: Suc_le_eq juncts_eq_set_juncts_list)

primrec norm_ACI (‹⟨_⟩›) where
  "⟨FBool b⟩ = FBool b"
| "⟨FBase a⟩ = FBase a"
| "⟨FNot φ⟩ = FNot ⟨φ⟩"
| "⟨FOr φ ψ⟩ = NFOR (disjuncts (FOr ⟨φ⟩ ⟨ψ⟩))"
| "⟨FAnd φ ψ⟩ = NFAND (conjuncts (FAnd ⟨φ⟩ ⟨ψ⟩))"
| "⟨FEx k φ⟩ = FEx k ⟨φ⟩"
| "⟨FAll k φ⟩ = FAll k ⟨φ⟩"

fun nf_ACI where
  "nf_ACI (FOr ψ1 ψ2) = (¬ is_FOr ψ1 ∧ (let φs = ψ1 # disjuncts_list ψ2 in
    sorted φs ∧ distinct φs ∧ nf_ACI ψ1 ∧ nf_ACI ψ2))"
| "nf_ACI (FAnd ψ1 ψ2) = (¬ is_FAnd ψ1 ∧ (let φs = ψ1 # conjuncts_list ψ2 in
    sorted φs ∧ distinct φs ∧ nf_ACI ψ1 ∧ nf_ACI ψ2))"
| "nf_ACI (FNot φ) = nf_ACI φ"
| "nf_ACI (FEx k φ) = nf_ACI φ"
| "nf_ACI (FAll k φ) = nf_ACI φ"
| "nf_ACI φ = True"

lemma nf_ACI_D:
  "nf_ACI φ ⟹ sorted (disjuncts_list φ)"
  "nf_ACI φ ⟹ sorted (conjuncts_list φ)"
  "nf_ACI φ ⟹ distinct (disjuncts_list φ)"
  "nf_ACI φ ⟹ distinct (conjuncts_list φ)"
  "nf_ACI φ ⟹ list_all nf_ACI (disjuncts_list φ)"
  "nf_ACI φ ⟹ list_all nf_ACI (conjuncts_list φ)"
  by (induct φ) (auto simp: juncts_list_singleton)

lemma disjuncts_list_nFOR:
  "⟦list_all (λx. ¬ is_FOr x) φs; φs ≠ []⟧ ⟹ disjuncts_list (nFOR φs) = φs"
  by (induct φs rule: nFOR.induct) (auto simp: juncts_list_singleton)

lemma conjuncts_list_nFAND:
  "⟦list_all (λx. ¬ is_FAnd x) φs; φs ≠ []⟧ ⟹ conjuncts_list (nFAND φs) = φs"
  by (induct φs rule: nFAND.induct) (auto simp: juncts_list_singleton)

lemma disjuncts_NFOR:
  "⟦finite X; X ≠ {}; ∀x ∈ X. ¬ is_FOr x⟧ ⟹ disjuncts (NFOR X) = X"
  unfolding NFOR_def by (auto simp: juncts_eq_set_juncts_list list_all_iff disjuncts_list_nFOR)

lemma conjuncts_NFAND:
  "⟦finite X; X ≠ {}; ∀x ∈ X. ¬ is_FAnd x⟧ ⟹ conjuncts (NFAND X) = X"
  unfolding NFAND_def by (auto simp: juncts_eq_set_juncts_list list_all_iff conjuncts_list_nFAND)

lemma nf_ACI_nFOR: 
  "⟦sorted φs; distinct φs; list_all nf_ACI φs; list_all (λx. ¬ is_FOr x) φs⟧ ⟹ nf_ACI (nFOR φs)"
  by (induct φs rule: nFOR.induct)
    (auto simp: juncts_list_singleton disjuncts_list_nFOR nf_ACI_D)

lemma nf_ACI_nFAND: 
  "⟦sorted φs; distinct φs; list_all nf_ACI φs; list_all (λx. ¬ is_FAnd x) φs⟧ ⟹ nf_ACI (nFAND φs)"
  by (induct φs rule: nFAND.induct)
    (auto simp: juncts_list_singleton conjuncts_list_nFAND nf_ACI_D)

lemma nf_ACI_juncts:
  "⟦ψ ∈ disjuncts φ; nf_ACI φ⟧ ⟹ nf_ACI ψ"
  "⟦ψ ∈ conjuncts φ; nf_ACI φ⟧ ⟹ nf_ACI ψ"
  by (induct φ) auto

lemma nf_ACI_norm_ACI: "nf_ACI ⟨φ⟩"
  by (induct φ)
    (force simp: NFOR_def NFAND_def list_all_iff
      intro!: nf_ACI_nFOR nf_ACI_nFAND elim: nf_ACI_juncts notin_juncts)+

lemma nFOR_Cons: "nFOR (x # xs) = (if xs = [] then x else FOr x (nFOR xs))"
  by (cases xs) simp_all

lemma nFAND_Cons: "nFAND (x # xs) = (if xs = [] then x else FAnd x (nFAND xs))"
  by (cases xs) simp_all

lemma nFOR_disjuncts: "nf_ACI ψ ⟹ nFOR (disjuncts_list ψ) = ψ"
  by (induct ψ) (auto simp: juncts_list_singleton nFOR_Cons)

lemma nFAND_conjuncts: "nf_ACI ψ ⟹ nFAND (conjuncts_list ψ) = ψ"
  by (induct ψ) (auto simp: juncts_list_singleton nFAND_Cons)

lemma NFOR_disjuncts: "nf_ACI ψ ⟹ NFOR (disjuncts ψ) = ψ"
  using nFOR_disjuncts[of ψ] unfolding NFOR_def o_apply juncts_eq_set_juncts_list
  by (metis finite_set finite_sorted_distinct_unique nf_ACI_D(1,3) sorted_list_of_set)

lemma NFAND_conjuncts: "nf_ACI ψ ⟹ NFAND (conjuncts ψ) = ψ"
  using nFAND_conjuncts[of ψ] unfolding NFAND_def o_apply juncts_eq_set_juncts_list
  by (metis finite_set finite_sorted_distinct_unique nf_ACI_D(2,4) sorted_list_of_set)

lemma norm_ACI_if_nf_ACI: "nf_ACI φ ⟹ ⟨φ⟩ = φ"
  by (induct φ)
    (auto simp: juncts_list_singleton juncts_eq_set_juncts_list nonempty_juncts_list
      NFOR_def NFAND_def nFOR_Cons nFAND_Cons nFOR_disjuncts nFAND_conjuncts
      sorted_list_of_set_sort_remdups distinct_remdups_id sorted_sort_id insort_is_Cons)

lemma norm_ACI_idem: "⟨⟨φ⟩⟩ = ⟨φ⟩"
  by (metis nf_ACI_norm_ACI norm_ACI_if_nf_ACI)

lemma norm_ACI_juncts:
  "nf_ACI φ ⟹ norm_ACI ` disjuncts φ = disjuncts φ"
  "nf_ACI φ ⟹ norm_ACI ` conjuncts φ = conjuncts φ"
  by (drule nf_ACI_D(5,6), force simp: list_all_iff juncts_eq_set_juncts_list norm_ACI_if_nf_ACI)+

lemma
  norm_ACI_NFOR: "nf_ACI φ ⟹ φ = NFOR (norm_ACI ` disjuncts φ)" and
  norm_ACI_NFAND: "nf_ACI φ ⟹ φ = NFAND (norm_ACI ` conjuncts φ)"
  by (simp_all add: norm_ACI_juncts NFOR_disjuncts NFAND_conjuncts)

(*
'a - atomic formula
'i - interpretation
'k - kind of quantifier
'n - De Brujin index
'x - alphabet element
'v - valuation
*)
locale Formula_Operations =
  fixes TYPEVARS :: "'a :: linorder × 'i × 'k :: {linorder, enum} × 'n × 'x × 'v"

  (* De Bruijn indices abstractly *)
  and SUC :: "'k ⇒ 'n ⇒ 'n"
  and LESS :: "'k ⇒ nat ⇒ 'n ⇒ bool"

  (* Interpratations *)
  and assigns :: "nat ⇒ 'i ⇒ 'k ⇒ 'v" (‹_⇗_⇖_› [900, 999, 999] 999)
  and nvars :: "'i ⇒ 'n" (‹#V _› [1000] 900)
  and Extend :: "'k ⇒ nat ⇒ 'i ⇒ 'v ⇒ 'i"
  and CONS :: "'x ⇒ 'i ⇒ 'i"
  and SNOC :: "'x ⇒ 'i ⇒ 'i"
  and Length :: "'i ⇒ nat"

  (* Alphabet elements *)
  and extend :: "'k ⇒ bool ⇒ 'x ⇒ 'x"
  and size :: "'x ⇒ 'n"
  and zero :: "'n ⇒ 'x"
  and alphabet :: "'n ⇒ 'x list"

  (* Valuations *)
  and eval :: "'v ⇒ nat ⇒ bool"
  and downshift :: "'v ⇒ 'v"
  and upshift :: "'v ⇒ 'v"
  and add :: "nat ⇒ 'v ⇒ 'v"
  and cut :: "nat ⇒ 'v ⇒ 'v"
  and len :: "'v ⇒ nat"

  (* Restrictions *)
  and restrict :: "'k ⇒ 'v ⇒ bool"
  and Restrict :: "'k ⇒ nat ⇒ ('a, 'k) aformula"

  (* Function extensions for the base cases *)
  and lformula0 :: "'a ⇒ bool"
  and FV0 :: "'k ⇒ 'a ⇒ nat set"
  and find0 :: "'k ⇒ nat ⇒ 'a ⇒ bool"
  and wf0 :: "'n ⇒ 'a ⇒ bool"
  and decr0 :: "'k ⇒ nat ⇒ 'a ⇒ 'a"
  and satisfies0 :: "'i ⇒ 'a ⇒ bool" (infix ‹⊨0› 50)
  and nullable0 :: "'a ⇒ bool"
  and lderiv0 :: "'x ⇒ 'a ⇒ ('a, 'k) aformula"
  and rderiv0 :: "'x ⇒ 'a ⇒ ('a, 'k) aformula"
begin

abbreviation "LEQ k l n ≡ LESS k l (SUC k n)"

primrec FV where
  "FV (FBool _) k = {}"
| "FV (FBase a) k = FV0 k a"
| "FV (FNot φ) k = FV φ k"
| "FV (FOr φ ψ) k = FV φ k ∪ FV ψ k"
| "FV (FAnd φ ψ) k = FV φ k ∪ FV ψ k"
| "FV (FEx k' φ) k = (if k' = k then (λx. x - 1) ` (FV φ k - {0}) else FV φ k)"
| "FV (FAll k' φ) k = (if k' = k then (λx. x - 1) ` (FV φ k - {0}) else FV φ k)"

primrec find where
  "find k l (FBool _) = False"
| "find k l (FBase a) = find0 k l a"
| "find k l (FNot φ) = find k l φ"
| "find k l (FOr φ ψ) = (find k l φ ∨ find k l ψ)"
| "find k l (FAnd φ ψ) = (find k l φ ∨ find k l ψ)"
| "find k l (FEx k' φ) = find k (if k = k' then Suc l else l) φ"
| "find k l (FAll k' φ) = find k (if k = k' then Suc l else l) φ"

primrec wf :: "'n ⇒ ('a, 'k) aformula ⇒ bool" where
  "wf n (FBool _) = True"
| "wf n (FBase a) = wf0 n a"
| "wf n (FNot φ) = wf n φ"
| "wf n (FOr φ ψ) = (wf n φ ∧ wf n ψ)"
| "wf n (FAnd φ ψ) = (wf n φ ∧ wf n ψ)"
| "wf n (FEx k φ) = wf (SUC k n) φ"
| "wf n (FAll k φ) = wf (SUC k n) φ"

primrec lformula :: "('a, 'k) aformula ⇒ bool" where
  "lformula (FBool _) = True"
| "lformula (FBase a) = lformula0 a"
| "lformula (FNot φ) = lformula φ"
| "lformula (FOr φ ψ) = (lformula φ ∧ lformula ψ)"
| "lformula (FAnd φ ψ) = (lformula φ ∧ lformula ψ)"
| "lformula (FEx k φ) = lformula φ"
| "lformula (FAll k φ) = lformula φ"

primrec decr :: "'k ⇒ nat ⇒ ('a, 'k) aformula ⇒ ('a, 'k) aformula" where
  "decr k l (FBool b) = FBool b"
| "decr k l (FBase a) = FBase (decr0 k l a)"
| "decr k l (FNot φ) = FNot (decr k l φ)"
| "decr k l (FOr φ ψ) = FOr (decr k l φ) (decr k l ψ)"
| "decr k l (FAnd φ ψ) = FAnd (decr k l φ) (decr k l ψ)"
| "decr k l (FEx k' φ) = FEx k' (decr k (if k = k' then Suc l else l) φ)"
| "decr k l (FAll k' φ) = FAll k' (decr k (if k = k' then Suc l else l) φ)"

primrec satisfies_gen :: "('k ⇒ 'v ⇒ nat ⇒ bool) ⇒ 'i ⇒ ('a, 'k) aformula ⇒ bool" where
  "satisfies_gen r 𝔄 (FBool b) = b"
| "satisfies_gen r 𝔄 (FBase a) = (𝔄 ⊨0 a)"
| "satisfies_gen r 𝔄 (FNot φ) = (¬ satisfies_gen r 𝔄 φ)"
| "satisfies_gen r 𝔄 (FOr φ1 φ2) = (satisfies_gen r 𝔄 φ1 ∨ satisfies_gen r 𝔄 φ2)"
| "satisfies_gen r 𝔄 (FAnd φ1 φ2) = (satisfies_gen r 𝔄 φ1 ∧ satisfies_gen r 𝔄 φ2)"
| "satisfies_gen r 𝔄 (FEx k φ) = (∃P. r k P (Length 𝔄) ∧ satisfies_gen r (Extend k 0 𝔄 P) φ)"
| "satisfies_gen r 𝔄 (FAll k φ) = (∀P. r k P (Length 𝔄) ⟶ satisfies_gen r (Extend k 0 𝔄 P) φ)"

abbreviation satisfies (infix ‹⊨› 50) where
  "𝔄 ⊨ φ ≡ satisfies_gen (λ_ _ _. True) 𝔄 φ"

abbreviation satisfies_bounded (infix ‹⊨b› 50) where
  "𝔄 ⊨b φ ≡ satisfies_gen (λ_ P n. len P ≤ n) 𝔄 φ"

abbreviation sat_vars_gen where
  "sat_vars_gen r K 𝔄 φ ≡
    satisfies_gen (λk P n. restrict k P ∧ r k P n) 𝔄 φ ∧ (∀k ∈ K. ∀x ∈ FV φ k. restrict k (x⇗𝔄⇖k))"

definition sat where
  "sat 𝔄 φ ≡ sat_vars_gen (λ_ _ _. True) UNIV 𝔄 φ"

definition satb where
  "satb 𝔄 φ ≡ sat_vars_gen (λ_ P n. len P ≤ n) UNIV 𝔄 φ"

fun RESTR where
  "RESTR (FOr φ ψ) = FOr (RESTR φ) (RESTR ψ)"
| "RESTR (FAnd φ ψ) = FAnd (RESTR φ) (RESTR ψ)"
| "RESTR (FNot φ) = FNot (RESTR φ)"
| "RESTR (FEx k φ) = FEx k (FAnd (Restrict k 0) (RESTR φ))"
| "RESTR (FAll k φ) = FAll k (FOr (FNot (Restrict k 0)) (RESTR φ))"
| "RESTR φ = φ"

abbreviation RESTRICT_VARS where
  "RESTRICT_VARS ks V φ ≡
     foldr (%k φ. foldr (λx φ. FAnd (Restrict k x) φ) (V k) φ) ks (RESTR φ)"

definition RESTRICT where
  "RESTRICT φ ≡ RESTRICT_VARS Enum.enum (sorted_list_of_set o FV φ) φ"

primrec nullable :: "('a, 'k) aformula ⇒ bool" where
  "nullable (FBool b) = b"
| "nullable (FBase a) = nullable0 a"
| "nullable (FNot φ) = (¬ nullable φ)"
| "nullable (FOr φ ψ) = (nullable φ ∨ nullable ψ)"
| "nullable (FAnd φ ψ) = (nullable φ ∧ nullable ψ)"
| "nullable (FEx k φ) = nullable φ"
| "nullable (FAll k φ) = nullable φ"

fun nFOr :: "('a, 'k) aformula ⇒ ('a, 'k) aformula ⇒ ('a, 'k) aformula" where
  "nFOr (FBool b1) (FBool b2) = FBool (b1 ∨ b2)"
| "nFOr (FBool b) ψ = (if b then FBool True else ψ)"
| "nFOr φ (FBool b) = (if b then FBool True else φ)"
| "nFOr (FOr φ1 φ2) ψ = nFOr φ1 (nFOr φ2 ψ)"
| "nFOr φ (FOr ψ1 ψ2) =
  (if φ = ψ1 then FOr ψ1 ψ2
  else if φ < ψ1 then FOr φ (FOr ψ1 ψ2)
  else FOr ψ1 (nFOr φ ψ2))"
| "nFOr φ ψ =
  (if φ = ψ then φ
  else if φ < ψ then FOr φ ψ
  else FOr ψ φ)"

fun nFAnd :: "('a, 'k) aformula ⇒ ('a, 'k) aformula ⇒ ('a, 'k) aformula" where
  "nFAnd (FBool b1) (FBool b2) = FBool (b1 ∧ b2)"
| "nFAnd (FBool b) ψ = (if b then ψ else FBool False)"
| "nFAnd φ (FBool b) = (if b then φ else FBool False)"
| "nFAnd (FAnd φ1 φ2) ψ = nFAnd φ1 (nFAnd φ2 ψ)"
| "nFAnd φ (FAnd ψ1 ψ2) =
  (if φ = ψ1 then FAnd ψ1 ψ2
  else if φ < ψ1 then FAnd φ (FAnd ψ1 ψ2)
  else FAnd ψ1 (nFAnd φ ψ2))"
| "nFAnd φ ψ =
  (if φ = ψ then φ
  else if φ < ψ then FAnd φ ψ
  else FAnd ψ φ)"

fun nFEx :: "'k ⇒ ('a, 'k) aformula ⇒ ('a, 'k) aformula" where
  "nFEx k (FOr φ ψ) = nFOr (nFEx k φ) (nFEx k ψ)"
| "nFEx k φ = (if find k 0 φ then FEx k φ else decr k 0 φ)"

fun nFAll where
  "nFAll k (FAnd φ ψ) = nFAnd (nFAll k φ) (nFAll k ψ)"
| "nFAll k φ = (if find k 0 φ then FAll k φ else decr k 0 φ)"

fun nFNot :: "('a, 'k) aformula ⇒ ('a, 'k) aformula" where
  "nFNot (FNot φ) = φ"
| "nFNot (FOr φ ψ) = nFAnd (nFNot φ) (nFNot ψ)"
| "nFNot (FAnd φ ψ) = nFOr (nFNot φ) (nFNot ψ)"
| "nFNot (FEx b φ) = nFAll b (nFNot φ)"
| "nFNot (FAll b φ) = nFEx b (nFNot φ)"
| "nFNot (FBool b) = FBool (¬ b)"
| "nFNot φ = FNot φ"

fun norm where
  "norm (FOr φ ψ) = nFOr (norm φ) (norm ψ)"
| "norm (FAnd φ ψ) = nFAnd (norm φ) (norm ψ)"
| "norm (FNot φ) = nFNot (norm φ)"
| "norm (FEx k φ) = nFEx k (norm φ)"
| "norm (FAll k φ) = nFAll k (norm φ)"
| "norm φ = φ"

context
fixes deriv0 :: "'x ⇒ 'a ⇒ ('a, 'k) aformula"
begin

primrec deriv :: "'x ⇒ ('a, 'k) aformula ⇒ ('a, 'k) aformula" where
  "deriv x (FBool b) = FBool b"
| "deriv x (FBase a) = deriv0 x a"
| "deriv x (FNot φ) = FNot (deriv x φ)"
| "deriv x (FOr φ ψ) = FOr (deriv x φ) (deriv x ψ)"
| "deriv x (FAnd φ ψ) = FAnd (deriv x φ) (deriv x ψ)"
| "deriv x (FEx k φ) = FEx k (FOr (deriv (extend k True x) φ) (deriv (extend k False x) φ))"
| "deriv x (FAll k φ) = FAll k (FAnd (deriv (extend k True x) φ) (deriv (extend k False x) φ))"

end

abbreviation "lderiv ≡ deriv lderiv0"
abbreviation "rderiv ≡ deriv rderiv0"

lemma fold_deriv_FBool: "fold (deriv d0) xs (FBool b) = FBool b"
  by (induct xs) auto

lemma fold_deriv_FNot:
  "fold (deriv d0) xs (FNot φ) = FNot (fold (deriv d0) xs φ)"
  by (induct xs arbitrary: φ) auto

lemma fold_deriv_FOr:
  "fold (deriv d0) xs (FOr φ ψ) = FOr (fold (deriv d0) xs φ) (fold (deriv d0) xs ψ)"
  by (induct xs arbitrary: φ ψ) auto

lemma fold_deriv_FAnd:
  "fold (deriv d0) xs (FAnd φ ψ) = FAnd (fold (deriv d0) xs φ) (fold (deriv d0) xs ψ)"
  by (induct xs arbitrary: φ ψ) auto

lemma fold_deriv_FEx:
  "{⟨fold (deriv d0) xs (FEx k φ)⟩ | xs. True} ⊆
    {FEx k ψ | ψ. nf_ACI ψ ∧ disjuncts ψ ⊆ (⋃xs. disjuncts ⟨fold (deriv d0) xs φ⟩)}"
proof -
  { fix xs
    have "∃ψ. ⟨fold (deriv d0) xs (FEx k φ)⟩ = FEx k ψ ∧
      nf_ACI ψ ∧ disjuncts ψ ⊆ (⋃xs. disjuncts ⟨fold (deriv d0) xs φ⟩)"
    proof (induct xs arbitrary: φ)
      case (Cons x xs)
      let ?φ = "FOr (deriv d0 (extend k True x) φ) (deriv d0 (extend k False x) φ)"
      from Cons[of ?φ] obtain ψ where "⟨fold (deriv d0) xs (FEx k ?φ)⟩ = FEx k ψ"
        "nf_ACI ψ" and *: "disjuncts ψ ⊆ (⋃xs. disjuncts ⟨fold (deriv d0) xs ?φ⟩)" by blast+
      then show ?case
      proof (intro exI conjI)
        have "(⋃xs. disjuncts ⟨fold (deriv d0) xs ?φ⟩) ⊆
          (⋃xs. disjuncts ⟨fold (Formula_Operations.deriv extend d0) xs φ⟩)"
        by (force simp: fold_deriv_FOr nf_ACI_juncts nf_ACI_norm_ACI
          dest: notin_juncts subsetD[OF equalityD1[OF disjuncts_NFOR], rotated -1]
          intro: exI[of _ "extend k b x # xs" for b xs])
        with * show "disjuncts ψ ⊆ …" by blast
      qed simp_all
    qed (auto simp: nf_ACI_norm_ACI intro!: exI[of _ "[]"])
  }
  then show ?thesis by blast
qed

lemma fold_deriv_FAll:
  "{⟨fold (deriv d0) xs (FAll k φ)⟩ | xs. True} ⊆
    {FAll k ψ | ψ. nf_ACI ψ ∧ conjuncts ψ ⊆ (⋃xs. conjuncts ⟨fold (deriv d0) xs φ⟩)}"
proof -
  { fix xs
    have "∃ψ. ⟨fold (deriv d0) xs (FAll k φ)⟩ = FAll k ψ ∧
      nf_ACI ψ ∧ conjuncts ψ ⊆ (⋃xs. conjuncts ⟨fold (deriv d0) xs φ⟩)"
    proof (induct xs arbitrary: φ)
      case (Cons x xs)
      let ?φ = "FAnd (deriv d0 (extend k True x) φ) (deriv d0 (extend k False x) φ)"
      from Cons[of ?φ] obtain ψ where "⟨fold (deriv d0) xs (FAll k ?φ)⟩ = FAll k ψ"
        "nf_ACI ψ" and *: "conjuncts ψ ⊆ (⋃xs. conjuncts ⟨fold (deriv d0) xs ?φ⟩)" by blast+
      then show ?case
      proof (intro exI conjI)
        have "(⋃xs. conjuncts ⟨fold (deriv d0) xs ?φ⟩) ⊆
          (⋃xs. conjuncts ⟨fold (Formula_Operations.deriv extend d0) xs φ⟩)"
        by (force simp: fold_deriv_FAnd nf_ACI_juncts nf_ACI_norm_ACI
          dest: notin_juncts subsetD[OF equalityD1[OF conjuncts_NFAND], rotated -1]
          intro: exI[of _ "extend k b x # xs" for b xs])
        with * show "conjuncts ψ ⊆ …" by blast
      qed simp_all
    qed (auto simp: nf_ACI_norm_ACI intro!: exI[of _ "[]"])
  }
  then show ?thesis by blast
qed

lemma finite_norm_ACI_juncts:
  fixes f :: "('a, 'k) aformula ⇒ ('a, 'k) aformula"
  shows "finite B ⟹ finite {f φ | φ. nf_ACI φ ∧ disjuncts φ ⊆ B}"
        "finite B ⟹ finite {f φ | φ. nf_ACI φ ∧ conjuncts φ ⊆ B}"
  by (elim finite_surj[OF iffD2[OF finite_Pow_iff], of _ _ "f o NFOR o image norm_ACI"]
    finite_surj[OF iffD2[OF finite_Pow_iff], of _ _ "f o NFAND o image norm_ACI"],
    force simp: Pow_def image_Collect intro: arg_cong[OF norm_ACI_NFOR] arg_cong[OF norm_ACI_NFAND])+

end

locale Formula = Formula_Operations
  where TYPEVARS = TYPEVARS
  for TYPEVARS :: "'a :: linorder × 'i × 'k :: {linorder, enum} × 'n × 'x × 'v" +
  (* De Bruijn indices abstractly *)
  assumes SUC_SUC: "SUC k (SUC k' idx) = SUC k' (SUC k idx)"
  and LEQ_0: "LEQ k 0 idx"
  and LESS_SUC: "LEQ k (Suc l) idx = LESS k l idx"
    "k ≠ k' ⟹ LESS k l (SUC k' idx) = LESS k l idx"

  (* Interpretations *)
  and nvars_Extend: "#V (Extend k i 𝔄 P) = SUC k (#V 𝔄)"
  and Length_Extend: "Length (Extend k i 𝔄 P) = max (Length 𝔄) (len P)"
  and Length_0_inj: "⟦Length 𝔄 = 0; Length 𝔅 = 0; #V 𝔄 = #V 𝔅⟧ ⟹ 𝔄 = 𝔅"
  and ex_Length_0: "∃𝔄. Length 𝔄 = 0 ∧ #V 𝔄 = idx"
  and Extend_commute_safe: "⟦j ≤ i; LEQ k i (#V 𝔄)⟧ ⟹
      Extend k j (Extend k i 𝔄 P) Q = Extend k (Suc i) (Extend k j 𝔄 Q) P"
  and Extend_commute_unsafe: "k ≠ k' ⟹
      Extend k j (Extend k' i 𝔄 P) Q = Extend k' i (Extend k j 𝔄 Q) P"
  and assigns_Extend:  "LEQ k i (#V 𝔄) ⟹
    m⇗Extend k i 𝔄 P⇖k' = (if k = k' then (if m = i then P else dec i m⇗𝔄⇖k) else m⇗𝔄⇖k')"
  and assigns_SNOC_zero: "LESS k m (#V 𝔄) ⟹ m⇗SNOC (zero (#V 𝔄)) 𝔄⇖k = m⇗𝔄⇖k"
  and Length_CONS: "Length (CONS x 𝔄) = Length 𝔄 + 1"
  and Length_SNOC: "Length (SNOC x 𝔄) = Suc (Length 𝔄)"
  and nvars_CONS: "#V (CONS x 𝔄) = #V 𝔄"
  and nvars_SNOC: "#V (SNOC x 𝔄) = #V 𝔄"
  and Extend_CONS: "#V 𝔄 = size x ⟹ Extend k 0 (CONS x 𝔄) P =
      CONS (extend k (if eval P 0 then True else False) x) (Extend k 0 𝔄 (downshift P))"
  and Extend_SNOC_cut: "#V 𝔄 = size x ⟹ len P ≤ Length (SNOC x 𝔄) ⟹
    Extend k 0 (SNOC x 𝔄) P =
    SNOC (extend k (if eval P (Length 𝔄) then True else False) x) (Extend k 0 𝔄 (cut (Length 𝔄) P))"
  and CONS_inj: "size x = #V 𝔄 ⟹ size y = #V 𝔄 ⟹ #V 𝔄 = #V 𝔅 ⟹
    CONS x 𝔄 = CONS y 𝔅 ⟷ (x = y ∧ 𝔄 = 𝔅)"
  and CONS_surj: "Length 𝔄 ≠ 0 ⟹ #V 𝔄 = idx ⟹
    ∃x 𝔅. 𝔄 = CONS x 𝔅 ∧ #V 𝔅 = idx ∧ size x = idx"

  (* Alphabet elements *)
  and size_zero: "size (zero idx) = idx"
  and size_extend: "size (extend k b x) = SUC k (size x)"
  and distinct_alphabet: "distinct (alphabet idx)"
  and alphabet_size: "x ∈ set (alphabet idx) ⟷ size x = idx"

  (* Valuations *)
  and downshift_upshift: "downshift (upshift P) = P"
  and downshift_add_zero: "downshift (add 0 P) = downshift P"
  and eval_add: "eval (add n P) n"
  and eval_upshift: "¬ eval (upshift P) 0"
  and eval_ge_len: "p ≥ len P ⟹ ¬ eval P p"
  and len_cut_le: "len (cut n P) ≤ n"
  and len_cut: "len P ≤ n ⟹ cut n P = P"
  and cut_add: "cut n (add m P) = (if m ≥ n then cut n P else add m (cut n P))"
  and len_add: "len (add m P) = max (Suc m) (len P)"
  and len_upshift: "len (upshift P) = (case len P of 0 ⇒ 0 | n ⇒ Suc n)"
  and len_downshift: "len (downshift P) = (case len P of 0 ⇒ 0 | Suc n ⇒ n)"

  (* Function extensions for the base cases *)
  and wf0_decr0: "⟦wf0 (SUC k idx) a; LESS k l (SUC k idx); ¬ find0 k l a⟧ ⟹ wf0 idx (decr0 k l a)"
  and lformula0_decr0: "lformula0 φ ⟹ lformula0 (decr0 k l φ)"
  and Extend_satisfies0: "⟦¬ find0 k i a; LESS k i (SUC k (#V 𝔄)); lformula0 a ∨ len P ≤ Length 𝔄⟧ ⟹
      Extend k i 𝔄 P ⊨0 a ⟷ 𝔄 ⊨0 decr0 k i a"
  and nullable0_satisfies0: "Length 𝔄 = 0 ⟹ nullable0 a ⟷ 𝔄 ⊨0 a"
  and satisfies0_eqI: "wf0 (#V 𝔅) a ⟹ #V 𝔄 = #V 𝔅 ⟹ lformula0 a ⟹
    (⋀m k. LESS k m (#V 𝔅) ⟹ m⇗𝔄⇖k = m⇗𝔅⇖k) ⟹ 𝔄 ⊨0 a ⟷ 𝔅 ⊨0 a"
  and wf_lderiv0: "⟦wf0 idx a; lformula0 a⟧ ⟹ wf idx (lderiv0 x a)"
  and lformula_lderiv0: "lformula0 a ⟹ lformula (lderiv0 x a)"
  and wf_rderiv0: "wf0 idx a ⟹ wf idx (rderiv0 x a)"
  and satisfies_lderiv0:
    "⟦wf0 (#V 𝔄) a; #V 𝔄 = size x; lformula0 a⟧ ⟹ 𝔄 ⊨ lderiv0 x a ⟷ CONS x 𝔄 ⊨0 a"
  and satisfies_bounded_lderiv0:
    "⟦wf0 (#V 𝔄) a; #V 𝔄 = size x; lformula0 a⟧ ⟹ 𝔄 ⊨b lderiv0 x a ⟷ CONS x 𝔄 ⊨0 a"
  and satisfies_bounded_rderiv0:
    "⟦wf0 (#V 𝔄) a; #V 𝔄 = size x⟧ ⟹ 𝔄 ⊨b rderiv0 x a ⟷ SNOC x 𝔄 ⊨0 a"
  and find0_FV0: "⟦wf0 idx a; LESS k l idx⟧ ⟹ find0 k l a ⟷ l ∈ FV0 k a"
  and finite_FV0: "finite (FV0 k a)"
  and wf0_FV0_LESS: "⟦wf0 idx a; v ∈ FV0 k a⟧ ⟹ LESS k v idx"
  and restrict_Restrict: "i⇗𝔄⇖k = P ⟹ restrict k P ⟷ satisfies_gen r 𝔄 (Restrict k i)"
  and wf_Restrict: "LESS k i idx ⟹ wf idx (Restrict k i)"
  and lformula_Restrict: "lformula (Restrict k i)"
  and finite_lderiv0: "lformula0 a ⟹ finite {fold lderiv xs (FBase a) | xs. True}"
  and finite_rderiv0: "finite {fold rderiv xs (FBase a) | xs. True}"

context Formula
begin

lemma satisfies_eqI:
  "⟦wf (#V 𝔄) φ; #V 𝔄 = #V 𝔅; ⋀m k. LESS k m (#V 𝔄) ⟹ m⇗𝔄⇖k = m⇗𝔅⇖k; lformula φ⟧ ⟹
   𝔄 ⊨ φ ⟷ 𝔅 ⊨ φ"
proof (induct φ arbitrary: 𝔄 𝔅)
  case (FEx k φ)
  from FEx.prems have "⋀P. (Extend k 0 𝔄 P ⊨ φ) ⟷ (Extend k 0 𝔅 P ⊨ φ)"
    by (intro FEx.hyps) (auto simp: nvars_Extend assigns_Extend dec_def gr0_conv_Suc LEQ_0 LESS_SUC)
  then show ?case by simp
next
  case (FAll k φ)
  from FAll.prems have "⋀P. (Extend k 0 𝔄 P ⊨ φ) ⟷ (Extend k 0 𝔅 P ⊨ φ)"
    by (intro FAll.hyps) (auto simp: nvars_Extend assigns_Extend dec_def gr0_conv_Suc LEQ_0 LESS_SUC)
  then show ?case by simp
next
  case (FNot φ)
  from FNot.prems have "(𝔄 ⊨ φ) ⟷ (𝔅 ⊨ φ)" by (intro FNot.hyps) simp_all
  then show ?case by simp
qed (auto dest: satisfies0_eqI)

lemma wf_decr:
  "⟦wf (SUC k idx) φ; LEQ k l idx; ¬ find k l φ⟧ ⟹ wf idx (decr k l φ)"
  by (induct φ arbitrary: idx l) (auto simp: wf0_decr0 LESS_SUC SUC_SUC)

lemma lformula_decr:
  "lformula φ ⟹ lformula (decr k l φ)"
  by (induct φ arbitrary: l) (auto simp: lformula0_decr0)

lemma Extend_satisfies_decr:
  "⟦¬ find k i φ; LEQ k i (#V 𝔄); lformula φ⟧ ⟹ Extend k i 𝔄 P ⊨ φ ⟷ 𝔄 ⊨ decr k i φ"
  by (induct φ arbitrary: i 𝔄)
    (auto simp: Extend_commute_unsafe[of _ k 0 _ _ P] Extend_commute_safe
      Extend_satisfies0 nvars_Extend LESS_SUC SUC_SUC split: bool.splits)

lemma LEQ_SUC: "k ≠ k' ⟹ LEQ k i (SUC k' idx) = LEQ k i idx"
  by (metis LESS_SUC(2) SUC_SUC)

lemma Extend_satisfies_bounded_decr:
  "⟦¬ find k i φ; LEQ k i (#V 𝔄); len P ≤ Length 𝔄⟧ ⟹
   Extend k i 𝔄 P ⊨b φ ⟷ 𝔄 ⊨b decr k i φ"
proof (induct φ arbitrary: i 𝔄 P)
  case (FEx k' φ)
  show ?case
  proof (cases "k = k'")
    case True
    with FEx(2,3,4) show ?thesis
      using FEx(1)[of "Suc i" "Extend k' 0 𝔄 Q" P for Q j]
      by (auto simp: Extend_commute_safe LESS_SUC Length_Extend nvars_Extend max_def)
  next
    case False
    with FEx(2,3,4) show ?thesis
      using FEx(1)[of "i" "Extend k' j 𝔄 Q" P for Q j]
      by (auto simp: Extend_commute_unsafe LEQ_SUC Length_Extend nvars_Extend max_def)
  qed
next
  case (FAll k' φ)  show ?case
  proof (cases "k = k'")
    case True
    with FAll(2,3,4) show ?thesis
      using FAll(1)[of "Suc i" "Extend k' 0 𝔄 Q" P for Q j]
      by (auto simp: Extend_commute_safe LESS_SUC Length_Extend nvars_Extend max_def)
  next
    case False
    with FAll(2,3,4) show ?thesis
      using FAll(1)[of "i" "Extend k' j 𝔄 Q" P for Q j]
      by (auto simp: Extend_commute_unsafe LEQ_SUC Length_Extend nvars_Extend max_def)
  qed
qed (auto simp: Extend_satisfies0 split: bool.splits)


subsection ‹Normalization›

lemma wf_nFOr:
  "wf idx (FOr φ ψ) ⟹ wf idx (nFOr φ ψ)"
  by (induct φ ψ rule: nFOr.induct) (simp_all add: Let_def)

lemma wf_nFAnd:
  "wf idx (FAnd φ ψ) ⟹ wf idx (nFAnd φ ψ)"
  by (induct φ ψ rule: nFAnd.induct) (simp_all add: Let_def)

lemma wf_nFEx:
  "wf idx (FEx b φ) ⟹ wf idx (nFEx b φ)"
  by (induct φ arbitrary: idx rule: nFEx.induct)
    (auto simp: SUC_SUC LEQ_0 LESS_SUC(1) gr0_conv_Suc wf_nFOr intro: wf0_decr0 wf_decr)

lemma wf_nFAll:
  "wf idx (FAll b φ) ⟹ wf idx (nFAll b φ)"
  by (induct φ arbitrary: idx rule: nFAll.induct)
    (auto simp: SUC_SUC LEQ_0 LESS_SUC(1) gr0_conv_Suc wf_nFAnd intro: wf0_decr0 wf_decr)

lemma wf_nFNot:
  "wf idx (FNot φ) ⟹ wf idx (nFNot φ)"
  by (induct φ arbitrary: idx rule: nFNot.induct) (auto simp: wf_nFOr wf_nFAnd wf_nFEx wf_nFAll)

lemma wf_norm: "wf idx φ ⟹ wf idx (norm φ)"
  by (induct φ arbitrary: idx) (simp_all add: wf_nFOr wf_nFAnd wf_nFNot wf_nFEx wf_nFAll)

lemma lformula_nFOr:
  "lformula (FOr φ ψ) ⟹ lformula (nFOr φ ψ)"
  by (induct φ ψ rule: nFOr.induct) (simp_all add: Let_def)

lemma lformula_nFAnd:
  "lformula (FAnd φ ψ) ⟹ lformula (nFAnd φ ψ)"
  by (induct φ ψ rule: nFAnd.induct) (simp_all add: Let_def)

lemma lformula_nFEx:
  "lformula (FEx b φ) ⟹ lformula (nFEx b φ)"
  by (induct φ rule: nFEx.induct)
    (auto simp: lformula_nFOr lformula0_decr0 lformula_decr)

lemma lformula_nFAll:
  "lformula (FAll b φ) ⟹ lformula (nFAll b φ)"
  by (induct φ rule: nFAll.induct)
    (auto simp: lformula_nFAnd lformula0_decr0 lformula_decr)

lemma lformula_nFNot:
  "lformula (FNot φ) ⟹ lformula (nFNot φ)"
  by (induct φ rule: nFNot.induct) (auto simp: lformula_nFOr lformula_nFAnd lformula_nFEx lformula_nFAll)

lemma lformula_norm: "lformula φ ⟹ lformula (norm φ)"
  by (induct φ) (simp_all add: lformula_nFOr lformula_nFAnd lformula_nFNot
    lformula_nFEx lformula_nFAll)

lemma satisfies_nFOr:
  "𝔄 ⊨ nFOr φ ψ ⟷ 𝔄 ⊨ FOr φ ψ"
  by (induct φ ψ arbitrary: 𝔄 rule: nFOr.induct) auto

lemma satisfies_nFAnd:
  "𝔄 ⊨ nFAnd φ ψ ⟷ 𝔄 ⊨ FAnd φ ψ"
  by (induct φ ψ arbitrary: 𝔄 rule: nFAnd.induct) auto

lemma satisfies_nFEx: "lformula φ ⟹ 𝔄 ⊨ nFEx b φ ⟷ 𝔄 ⊨ FEx b φ"
  by (induct φ rule: nFEx.induct)
    (auto simp add: satisfies_nFOr Extend_satisfies_decr
      LEQ_0 LESS_SUC(1) nvars_Extend Extend_satisfies0 Extend_commute_safe Extend_commute_unsafe)

lemma satisfies_nFAll: "lformula φ ⟹ 𝔄 ⊨ nFAll b φ ⟷ 𝔄 ⊨ FAll b φ"
  by (induct φ rule: nFAll.induct)
    (auto simp add: satisfies_nFAnd Extend_satisfies_decr
      Extend_satisfies0 LEQ_0 LESS_SUC(1) nvars_Extend Extend_commute_safe Extend_commute_unsafe)

lemma satisfies_nFNot:
  "lformula φ ⟹ 𝔄 ⊨ nFNot φ ⟷ 𝔄 ⊨ FNot φ"
  by (induct φ arbitrary: 𝔄)
    (simp_all add: satisfies_nFOr satisfies_nFAnd satisfies_nFEx satisfies_nFAll
    lformula_nFNot)

lemma satisfies_norm: "lformula φ ⟹ 𝔄 ⊨ norm φ ⟷ 𝔄 ⊨ φ"
  using satisfies_nFOr satisfies_nFAnd satisfies_nFNot satisfies_nFEx satisfies_nFAll
  by (induct φ arbitrary: 𝔄) (simp_all add: lformula_norm)

lemma satisfies_bounded_nFOr:
  "𝔄 ⊨b nFOr φ ψ ⟷ 𝔄 ⊨b FOr φ ψ"
  by (induct φ ψ arbitrary: 𝔄 rule: nFOr.induct) auto

lemma satisfies_bounded_nFAnd:
  "𝔄 ⊨b nFAnd φ ψ ⟷ 𝔄 ⊨b FAnd φ ψ"
  by (induct φ ψ arbitrary: 𝔄 rule: nFAnd.induct) auto

lemma len_cut_0: "len (cut 0 P) = 0"
  by (metis le_0_eq len_cut_le)

lemma satisfies_bounded_nFEx: "𝔄 ⊨b nFEx b φ ⟷ 𝔄 ⊨b FEx b φ"
  by (induct φ rule: nFEx.induct)
    (auto 4 4 simp add: satisfies_bounded_nFOr Extend_satisfies_bounded_decr
      LEQ_0 LESS_SUC(1) nvars_Extend Length_Extend len_cut_0
      Extend_satisfies0 Extend_commute_safe Extend_commute_unsafe cong: ex_cong split: bool.splits
      intro: exI[where P = "λx. P x ∧ Q x" for P Q, OF conjI[rotated]] exI[of _ "cut 0 P" for P])

lemma satisfies_bounded_nFAll: "𝔄 ⊨b nFAll b φ ⟷ 𝔄 ⊨b FAll b φ"
  by (induct φ rule: nFAll.induct)
    (auto 4 4 simp add: satisfies_bounded_nFAnd Extend_satisfies_bounded_decr
      LEQ_0 LESS_SUC(1) nvars_Extend Length_Extend len_cut_0
      Extend_satisfies0 Extend_commute_safe Extend_commute_unsafe cong: split: bool.splits
      intro: exI[where P = "λx. P x ∧ Q x" for P Q, OF conjI[rotated]] dest: spec[of _ "cut 0 P" for P])

lemma satisfies_bounded_nFNot:
  "𝔄 ⊨b nFNot φ ⟷ 𝔄 ⊨b FNot φ"
  by (induct φ arbitrary: 𝔄)
    (auto simp: satisfies_bounded_nFOr satisfies_bounded_nFAnd satisfies_bounded_nFEx satisfies_bounded_nFAll)

lemma satisfies_bounded_norm: "𝔄 ⊨b norm φ ⟷ 𝔄 ⊨b φ"
  by (induct φ arbitrary: 𝔄)
    (simp_all add: satisfies_bounded_nFOr satisfies_bounded_nFAnd
      satisfies_bounded_nFNot satisfies_bounded_nFEx satisfies_bounded_nFAll)


subsection ‹Derivatives of Formulas›

lemma wf_lderiv:
  "⟦wf idx φ; lformula φ⟧ ⟹ wf idx (lderiv x φ)"
  by (induct φ arbitrary: x idx) (auto simp: wf_lderiv0)

lemma lformula_lderiv:
  "lformula φ ⟹ lformula (lderiv x φ)"
  by (induct φ arbitrary: x) (auto simp: lformula_lderiv0)

lemma wf_rderiv:
  "wf idx φ ⟹ wf idx (rderiv x φ)"
  by (induct φ arbitrary: x idx) (auto simp: wf_rderiv0)

theorem satisfies_lderiv:
  "⟦wf (#V 𝔄) φ; #V 𝔄 = size x; lformula φ⟧ ⟹ 𝔄 ⊨ lderiv x φ ⟷ CONS x 𝔄 ⊨ φ"
proof (induct φ arbitrary: x 𝔄)
  case (FEx k φ)
  from FEx.prems FEx.hyps[of "Extend k 0 𝔄 P" "extend k b x" for P b] show ?case
    by (auto simp: nvars_Extend size_extend Extend_CONS
      downshift_upshift eval_add eval_upshift downshift_add_zero
      intro: exI[of _ "add 0 (upshift P)" for P] exI[of _ "upshift P" for P])
next
  case (FAll k φ)
  from FAll.prems FAll.hyps[of "Extend k 0 𝔄 P" "extend k b x" for P b] show ?case
    by (auto simp: nvars_Extend size_extend Extend_CONS
      downshift_upshift eval_add eval_upshift downshift_add_zero
      dest: spec[of _ "add 0 (upshift P)" for P] spec[of _ "upshift P" for P])
qed (simp_all add: satisfies_lderiv0 split: bool.splits)

theorem satisfies_bounded_lderiv:
  "⟦wf (#V 𝔄) φ; #V 𝔄 = size x; lformula φ⟧ ⟹ 𝔄 ⊨b lderiv x φ ⟷ CONS x 𝔄 ⊨b φ"
proof (induct φ arbitrary: x 𝔄)
  case (FEx k φ)
  note [simp] = nvars_Extend size_extend Extend_CONS Length_CONS
    downshift_upshift eval_add eval_upshift downshift_add_zero len_add len_upshift len_downshift
  from FEx.prems FEx.hyps[of "Extend k 0 𝔄 P" "extend k b x" for P b] show ?case
    by auto (force intro: exI[of _ "add 0 (upshift P)" for P] exI[of _ "upshift P" for P] split: nat.splits)+
next
  case (FAll k φ)
  note [simp] = nvars_Extend size_extend Extend_CONS Length_CONS
    downshift_upshift eval_add eval_upshift downshift_add_zero len_add len_upshift len_downshift
  from FAll.prems FAll.hyps[of "Extend k 0 𝔄 P" "extend k b x" for P b] show ?case
    by auto (force dest: spec[of _ "add 0 (upshift P)" for P] spec[of _ "upshift P" for P] split: nat.splits)+
qed (simp_all add: satisfies_bounded_lderiv0 split: bool.splits)

theorem satisfies_bounded_rderiv:
  "⟦wf (#V 𝔄) φ; #V 𝔄 = size x⟧ ⟹ 𝔄 ⊨b rderiv x φ ⟷ SNOC x 𝔄 ⊨b φ"
proof (induct φ arbitrary: x 𝔄)
  case (FEx k φ)
  from FEx.prems FEx.hyps[of "Extend k 0 𝔄 P" "extend k b x" for P b] show ?case
    by (auto simp: nvars_Extend size_extend Extend_SNOC_cut len_cut_le eval_ge_len 
      eval_add cut_add Length_SNOC len_add len_cut le_Suc_eq max_def
      intro: exI[of _ "cut (Length 𝔄) P" for P] exI[of _ "add (Length 𝔄) P" for P] split: if_splits)
next
  case (FAll k φ)
  from FAll.prems FAll.hyps[of "Extend k 0 𝔄 P" "extend k b x" for P b] show ?case
    by (auto simp: nvars_Extend size_extend Extend_SNOC_cut len_cut_le eval_ge_len 
      eval_add cut_add Length_SNOC len_add len_cut le_Suc_eq max_def
      dest: spec[of _ "cut (Length 𝔄) P" for P] spec[of _ "add (Length 𝔄) P" for P] split: if_splits)
qed (simp_all add: satisfies_bounded_rderiv0 split: bool.splits)

lemma wf_norm_rderivs: "wf idx φ ⟹ wf idx (((norm ∘ rderiv (zero idx)) ^^ k) φ)"
  by (induct k) (auto simp: wf_norm wf_rderiv)

subsection ‹Finiteness of Derivatives Modulo ACI›

lemma finite_fold_deriv:
  assumes "(d0 = lderiv0 ∧ lformula φ) ∨ d0 = rderiv0"
  shows "finite {⟨fold (deriv d0) xs φ⟩ | xs. True}"
using assms proof (induct φ)
  case (FBase a) then show ?case
    by (auto intro:
      finite_subset[OF _ finite_imageI[OF finite_lderiv0]]
      finite_subset[OF _ finite_imageI[OF finite_rderiv0]])
next
  case (FNot φ)
  then show ?case
    by (auto simp: fold_deriv_FNot intro!: finite_surj[OF FNot(1)])
next
  case (FOr φ ψ)
  then show ?case
    by (auto simp: fold_deriv_FOr intro!: finite_surj[OF finite_cartesian_product[OF FOr(1,2)]])
next
  case (FAnd φ ψ)
  then show ?case
    by (auto simp: fold_deriv_FAnd intro!: finite_surj[OF finite_cartesian_product[OF FAnd(1,2)]])
next
  case (FEx k φ)
  then have "finite (⋃ (disjuncts ` {⟨fold (deriv d0) xs φ⟩ | xs . True}))" by auto
  then have "finite (⋃xs. disjuncts ⟨fold (deriv d0) xs φ⟩)" by (rule finite_subset[rotated]) auto
  then have "finite {FEx k ψ | ψ. nf_ACI ψ ∧ disjuncts ψ ⊆ (⋃xs. disjuncts ⟨fold (deriv d0) xs φ⟩)}"
    by (rule finite_norm_ACI_juncts)
  then show ?case by (rule finite_subset[OF fold_deriv_FEx])
next
  case (FAll k φ)
  then have "finite (⋃ (conjuncts ` {⟨fold (deriv d0) xs φ⟩ | xs . True}))" by auto
  then have "finite (⋃xs. conjuncts ⟨fold (deriv d0) xs φ⟩)" by (rule finite_subset[rotated]) auto
  then have "finite {FAll k ψ | ψ. nf_ACI ψ ∧ conjuncts ψ ⊆ (⋃xs. conjuncts ⟨fold (deriv d0) xs φ⟩)}"
    by (rule finite_norm_ACI_juncts)
  then show ?case  by (rule finite_subset[OF fold_deriv_FAll])
qed (simp add: fold_deriv_FBool)

lemma lformula_nFOR: "lformula (nFOR φs) = (∀φ ∈ set φs. lformula φ)"
  by (induct φs rule: nFOR.induct) auto

lemma lformula_nFAND: "lformula (nFAND φs) = (∀φ ∈ set φs. lformula φ)"
  by (induct φs rule: nFAND.induct) auto

lemma lformula_NFOR: "finite Φ ⟹ lformula (NFOR Φ) = (∀φ ∈ Φ. lformula φ)"
  unfolding NFOR_def o_apply lformula_nFOR by simp

lemma lformula_NFAND: "finite Φ ⟹ lformula (NFAND Φ) = (∀φ ∈ Φ. lformula φ)"
  unfolding NFAND_def o_apply lformula_nFAND by simp

lemma lformula_disjuncts: "(∀ψ ∈ disjuncts φ. lformula ψ) = lformula φ"
  by (induct φ rule: disjuncts.induct) fastforce+

lemma lformula_conjuncts: "(∀ψ ∈ conjuncts φ. lformula ψ) = lformula φ"
  by (induct φ rule: conjuncts.induct) fastforce+

lemma lformula_norm_ACI: "lformula ⟨φ⟩ = lformula φ"
  by (induct φ) (simp_all add: ball_Un
    lformula_NFOR lformula_disjuncts lformula_NFAND lformula_conjuncts)

theorem
  finite_fold_lderiv: "lformula φ ⟹ finite {⟨fold lderiv xs ⟨φ⟩⟩ | xs. True}" and
  finite_fold_rderiv: "finite {⟨fold rderiv xs ⟨φ⟩⟩ | xs. True}"
  by (subst (asm) lformula_norm_ACI[symmetric]) (blast intro: nf_ACI_norm_ACI finite_fold_deriv)+

lemma wf_nFOR: "wf idx (nFOR φs) ⟷ (∀φ ∈ set φs. wf idx φ)"
  by (induct rule: nFOR.induct) auto

lemma wf_nFAND: "wf idx (nFAND φs) ⟷ (∀φ ∈ set φs. wf idx φ)"
  by (induct rule: nFAND.induct) auto

lemma wf_NFOR: "finite Φ ⟹ wf idx (NFOR Φ) ⟷ (∀φ ∈ Φ. wf idx φ)"
  unfolding NFOR_def o_apply by (auto simp: wf_nFOR)

lemma wf_NFAND: "finite Φ ⟹ wf idx (NFAND Φ) ⟷ (∀φ ∈ Φ. wf idx φ)"
  unfolding NFAND_def o_apply by (auto simp: wf_nFAND)

lemma satisfies_bounded_nFOR: "𝔄 ⊨b nFOR φs ⟷ (∃φ ∈ set φs. 𝔄 ⊨b φ)"
  by (induct rule: nFOR.induct) (auto simp: satisfies_bounded_nFOr)

lemma satisfies_bounded_nFAND: "𝔄 ⊨b nFAND φs ⟷ (∀φ ∈ set φs. 𝔄 ⊨b φ)"
  by (induct rule: nFAND.induct) (auto simp: satisfies_bounded_nFAnd)

lemma satisfies_bounded_NFOR: "finite Φ ⟹ 𝔄 ⊨b NFOR Φ ⟷ (∃φ ∈ Φ. 𝔄 ⊨b φ)"
  unfolding NFOR_def o_apply by (auto simp: satisfies_bounded_nFOR)

lemma satisfies_bounded_NFAND: "finite Φ ⟹ 𝔄 ⊨b NFAND Φ ⟷ (∀φ ∈ Φ. 𝔄 ⊨b φ)"
  unfolding NFAND_def o_apply by (auto simp: satisfies_bounded_nFAND)

lemma wf_juncts:
  "wf idx φ ⟷ (∀ψ ∈ disjuncts φ. wf idx ψ)"
  "wf idx φ ⟷ (∀ψ ∈ conjuncts φ. wf idx ψ)"
  by (induct φ) auto

lemma wf_norm_ACI: "wf idx ⟨φ⟩ = wf idx φ"
  by (induct φ arbitrary: idx) (auto simp: wf_NFOR wf_NFAND ball_Un wf_juncts[symmetric])

lemma satisfies_bounded_disjuncts:
  "𝔄 ⊨b φ ⟷ (∃ψ ∈ disjuncts φ. 𝔄 ⊨b ψ)"
  by (induct φ arbitrary: 𝔄) auto

lemma satisfies_bounded_conjuncts:
  "𝔄 ⊨b φ ⟷ (∀ψ ∈ conjuncts φ. 𝔄 ⊨b ψ)"
  by (induct φ arbitrary: 𝔄) auto

lemma satisfies_bounded_norm_ACI: "𝔄 ⊨b ⟨φ⟩ ⟷ 𝔄 ⊨b φ"
  by (rule sym, induct φ arbitrary: 𝔄)
    (auto simp: satisfies_bounded_NFOR satisfies_bounded_NFAND
      intro: iffD2[OF satisfies_bounded_disjuncts] iffD2[OF satisfies_bounded_conjuncts]
      dest: iffD1[OF satisfies_bounded_disjuncts] iffD1[OF satisfies_bounded_conjuncts])

lemma nvars_SNOCs: "#V ((SNOC x^^k) 𝔄) = #V 𝔄"
  by (induct k) (auto simp: nvars_SNOC)

lemma wf_fold_rderiv: "wf idx φ ⟹ wf idx (fold rderiv (replicate k x) φ)"
  by (induct k arbitrary: φ) (auto simp: wf_rderiv)

lemma satisfies_bounded_fold_rderiv:
  "⟦wf idx φ; #V 𝔄 = idx; size x = idx⟧ ⟹
     𝔄 ⊨b fold rderiv (replicate k x) φ ⟷ (SNOC x^^k) 𝔄 ⊨b φ"
  by (induct k arbitrary: 𝔄 φ) (auto simp: satisfies_bounded_rderiv wf_rderiv nvars_SNOCs)


subsection ‹Emptiness Check›

context
  fixes b :: bool
  and idx :: 'n
  and ψ :: "('a, 'k) aformula"
begin

abbreviation "fut_test ≡ λ(φ, Φ). φ ∉ set Φ"
abbreviation "fut_step ≡ λ(φ, Φ). (norm (rderiv (zero idx) φ), φ # Φ)"
definition "fut_derivs k φ ≡ ((norm o rderiv (zero idx))^^k) φ"

lemma fut_derivs_Suc[simp]: "norm (rderiv (zero idx) (fut_derivs k φ)) = fut_derivs (Suc k) φ"
  unfolding fut_derivs_def by auto

definition "fut_invariant =
  (λ(φ, Φ). wf idx φ ∧ (∀φ ∈ set Φ. wf idx φ) ∧
    (∃k. φ = fut_derivs k ψ ∧ Φ = map (λi. fut_derivs i ψ) (rev [0 ..< k])))"
definition "fut_spec φΦ ≡ (∀φ ∈ set (snd φΦ). wf idx φ) ∧
  (∀𝔄. #V 𝔄 = idx ⟶
    (if b then (∃k. (SNOC (zero idx) ^^ k) 𝔄 ⊨b ψ) ⟷ (∃φ ∈ set (snd φΦ). 𝔄 ⊨b φ)
    else (∀k. (SNOC (zero idx) ^^ k) 𝔄 ⊨b ψ) ⟷ (∀φ ∈ set (snd φΦ). 𝔄 ⊨b φ)))"

definition "fut_default =
  (ψ, sorted_list_of_set {⟨fold rderiv (replicate k (zero idx)) ⟨ψ⟩⟩ | k. True})"

lemma finite_fold_rderiv_zeros: "finite {⟨fold rderiv (replicate k (zero idx)) ⟨ψ⟩⟩ | k. True}"
  by (rule finite_subset[OF _ finite_fold_rderiv[of ψ]]) blast

definition fut :: "('a, 'k) aformula" where
  "fut = (if b then nFOR else nFAND) (snd (while_default fut_default fut_test fut_step (ψ, [])))"

context
  assumes wf: "wf idx ψ"
begin 

lemma wf_fut_derivs:
  "wf idx (fut_derivs k ψ)"
  by (induct k) (auto simp: wf_norm wf_rderiv wf fut_derivs_def)

lemma satisfies_bounded_fut_derivs:
  "#V 𝔄 = idx ⟹ 𝔄 ⊨b fut_derivs k ψ ⟷ (SNOC (zero idx)^^k) 𝔄 ⊨b ψ"
  by (induct k arbitrary: 𝔄) (auto simp: fut_derivs_def satisfies_bounded_rderiv satisfies_bounded_norm
    wf_norm_rderivs size_zero nvars_SNOC funpow_swap1[of "SNOC x" for x] wf)

lemma fut_init: "fut_invariant (ψ, [])"
  unfolding fut_invariant_def by (auto simp: fut_derivs_def wf)

lemma fut_spec_default: "fut_spec fut_default"
  using satisfies_bounded_fold_rderiv[OF iffD2[OF wf_norm_ACI wf] sym size_zero] 
  unfolding fut_spec_def fut_default_def snd_conv
    set_sorted_list_of_set[OF finite_fold_rderiv_zeros]
  by (auto simp: satisfies_bounded_norm_ACI wf_fold_rderiv wf wf_norm_ACI simp del: fold_replicate)

lemma fut_invariant: "fut_invariant φΦ ⟹ fut_test φΦ ⟹ fut_invariant (fut_step φΦ)"
  by (cases φΦ) (auto simp: fut_invariant_def wf_norm wf_rderiv split: if_splits)

lemma fut_terminate: "fut_invariant φΦ ⟹ ¬ fut_test φΦ ⟹ fut_spec φΦ"
proof (induct φΦ, unfold prod.case not_not)
  fix φ Φ assume "fut_invariant (φ, Φ)" "φ ∈ set Φ"
  then obtain i k where "i < k" and φ_def: "φ = fut_derivs i ψ"
    and Φ_def: "Φ = map (λi. fut_derivs i ψ) (rev [0..<k])"
    and *: "fut_derivs k ψ = fut_derivs i ψ" unfolding fut_invariant_def by auto
  have "set Φ = {fut_derivs k ψ | k . True}"
  unfolding Φ_def set_map set_rev set_upt proof safe
    fix j
    show "fut_derivs j ψ ∈ (λi. fut_derivs i ψ) ` {0..<k}"
    proof (cases "j < k")
      case False
      with * ‹i < k› have "fut_derivs j ψ = fut_derivs ((j - i) mod (k - i) + i) ψ"
        unfolding fut_derivs_def by (auto intro: funpow_cycle_offset)
      then show ?thesis using ‹i < k› ‹¬ j < k›
        by (metis image_eqI atLeastLessThan_iff le0 less_diff_conv mod_less_divisor zero_less_diff)
    qed simp
  qed (blast intro: *)
  then show "fut_spec (φ, Φ)"
    unfolding fut_spec_def using satisfies_bounded_fut_derivs by (auto simp: wf_fut_derivs)
qed

lemma fut_spec_while_default:
  "fut_spec (while_default fut_default fut_test fut_step (ψ, []))"
  using fut_invariant fut_terminate fut_init fut_spec_default by (rule while_default_rule)

lemma wf_fut: "wf idx fut"
  using fut_spec_while_default unfolding fut_def fut_spec_def by (auto simp: wf_nFOR wf_nFAND)

lemma satisfies_bounded_fut:
  assumes "#V 𝔄 = idx"
  shows "𝔄 ⊨b fut ⟷
    (if b then (∃k. (SNOC (zero idx) ^^ k) 𝔄 ⊨b ψ) else (∀k. (SNOC (zero idx) ^^ k) 𝔄 ⊨b ψ))"
  using fut_spec_while_default assms unfolding fut_def fut_spec_def
  by (auto simp: satisfies_bounded_nFOR satisfies_bounded_nFAND)

end

end

fun finalize :: "'n ⇒ ('a, 'k) aformula ⇒ ('a, 'k) aformula" where
  "finalize idx (FEx k φ) = fut True idx (nFEx k (finalize (SUC k idx) φ))"
| "finalize idx (FAll k φ) = fut False idx (nFAll k (finalize (SUC k idx) φ))"
| "finalize idx (FOr φ ψ) = FOr (finalize idx φ) (finalize idx ψ)"
| "finalize idx (FAnd φ ψ) = FAnd (finalize idx φ) (finalize idx ψ)"
| "finalize idx (FNot φ) = FNot (finalize idx φ)"
| "finalize idx φ = φ"

definition final :: "'n ⇒ ('a, 'k) aformula ⇒ bool" where
  "final idx = nullable o finalize idx"

lemma wf_finalize: "wf idx φ ⟹ wf idx (finalize idx φ)"
  by (induct φ arbitrary: idx) (auto simp: wf_fut wf_nFEx wf_nFAll)

lemma Length_SNOCs: "Length ((SNOC x ^^ i) 𝔄) = Length 𝔄 + i"
  by (induct i arbitrary: 𝔄) (auto simp: Length_SNOC)

lemma assigns_SNOCs_zero:
  "⟦LESS k m (#V 𝔄); #V 𝔄 = idx⟧  ⟹ m⇗(SNOC (zero idx) ^^ i) 𝔄⇖k = m⇗𝔄⇖k"
  by (induct i arbitrary: 𝔄) (auto simp: assigns_SNOC_zero nvars_SNOC funpow_swap1)

lemma Extend_SNOCs_zero_satisfies: "⟦wf (SUC k idx) φ; #V 𝔄 = idx; lformula φ⟧ ⟹
  Extend k 0 ((SNOC (zero (#V 𝔄)) ^^ i) 𝔄) P ⊨ φ ⟷ Extend k 0 𝔄 P ⊨ φ"
  by (rule satisfies_eqI)
   (auto simp: nvars_Extend nvars_SNOCs assigns_Extend assigns_SNOCs_zero LEQ_0 LESS_SUC
     dec_def gr0_conv_Suc)

lemma finalize_satisfies: "⟦wf idx φ; #V 𝔄 = idx; lformula φ⟧ ⟹ 𝔄 ⊨b finalize idx φ ⟷ 𝔄 ⊨ φ"
  by (induct φ arbitrary: idx 𝔄)
    (force simp add: wf_nFEx wf_nFAll wf_finalize Length_SNOCs nvars_Extend nvars_SNOCs
      satisfies_bounded_fut satisfies_bounded_nFEx satisfies_bounded_nFAll Extend_SNOCs_zero_satisfies
      intro: le_add2)+

lemma Extend_empty_satisfies0:
  "⟦Length 𝔄 = 0; len P = 0⟧ ⟹ Extend k i 𝔄 P ⊨0 a ⟷ 𝔄 ⊨0 a"
  by (intro box_equals[OF _ nullable0_satisfies0 nullable0_satisfies0])
    (auto simp: nvars_Extend Length_Extend)

lemma Extend_empty_satisfies_bounded:
  "⟦Length 𝔄 = 0; len P = 0⟧ ⟹ Extend k 0 𝔄 P ⊨b φ ⟷ 𝔄 ⊨b φ"
  by (induct φ arbitrary: k 𝔄 P)
    (auto simp: Extend_empty_satisfies0 Length_Extend split: bool.splits)

lemma nullable_satisfies_bounded: "Length 𝔄 = 0 ⟹ nullable φ ⟷ 𝔄 ⊨b φ"
  by (induct φ) (auto simp: nullable0_satisfies0 Extend_empty_satisfies_bounded len_cut_0
    intro: exI[of _ "cut 0 P" for P])

lemma final_satisfies:
  "⟦wf idx φ ∧ lformula φ; Length 𝔄 = 0; #V 𝔄 = idx⟧ ⟹ final idx φ = (𝔄 ⊨ φ)"
  by (simp only: final_def o_apply nullable_satisfies_bounded finalize_satisfies)

subsection ‹Restrictions›

lemma satisfies_gen_restrict_RESTR:
  "satisfies_gen (λk P n. restrict k P ∧ r k P n) 𝔄 φ ⟷ satisfies_gen r 𝔄 (RESTR φ)"
  by (induct φ arbitrary: 𝔄) (auto simp: restrict_Restrict[symmetric] assigns_Extend LEQ_0)

lemma finite_FV: "finite (FV φ k)"
  by (induct φ) (auto simp: finite_FV0)

lemma satisfies_gen_restrict:
  "satisfies_gen r 𝔄 φ ∧ (∀x∈set V. restrict k (x⇗𝔄⇖k)) ⟷
   satisfies_gen r 𝔄 (foldr (λx. FAnd (Restrict k x)) V φ)"
  by (induct V arbitrary: φ) (auto simp: restrict_Restrict[symmetric])

lemma sat_vars_RESTRICT_VARS:
  fixes φ
  defines "vs ≡ sorted_list_of_set o FV φ"
  assumes "∀k ∈ set ks. finite (FV φ k)"
  shows "sat_vars_gen r (set ks) 𝔄 φ ⟷ satisfies_gen r 𝔄 (RESTRICT_VARS ks vs φ)"
using assms proof (induct ks)
  case (Cons k ks)
  with satisfies_gen_restrict[of r 𝔄 "(RESTRICT_VARS ks vs φ)" "vs k"] show ?case by auto
qed (simp add: satisfies_gen_restrict_RESTR)

lemma sat_RESTRICT: "sat 𝔄 φ ⟷ 𝔄 ⊨ RESTRICT φ"
  unfolding sat_def RESTRICT_def using sat_vars_RESTRICT_VARS[of Enum.enum, symmetric]
  by (auto simp: finite_FV enum_UNIV)

lemma satb_RESTRICT: "satb 𝔄 φ ⟷ 𝔄 ⊨b RESTRICT φ"
  unfolding satb_def RESTRICT_def using sat_vars_RESTRICT_VARS[of Enum.enum, symmetric]
  by (auto simp: finite_FV enum_UNIV)

lemma wf_RESTR: "wf idx φ ⟹ wf idx (RESTR φ)"
  by (induct φ arbitrary: idx) (auto simp: wf_Restrict LESS_SUC LEQ_0)

lemma wf_RESTRICT_VARS: "⟦wf idx φ; ∀k ∈ set ks. ∀v ∈ set (vs k). LESS k v idx⟧ ⟹
  wf idx (RESTRICT_VARS ks vs φ)"
proof (induct ks)
  case (Cons k ks)
  moreover
  { fix vs φ assume "∀v ∈ set vs. LESS k v idx" "wf idx φ"
    then have "wf idx (foldr (λx. FAnd (Restrict k x)) vs φ)"
      by (induct vs arbitrary: φ) (auto simp: wf_Restrict)
  }
  ultimately show ?case by auto
qed (simp add: wf_RESTR)

lemma wf_FV_LESS: "⟦wf idx φ; v ∈ FV φ k⟧ ⟹ LESS k v idx"
  by (induct φ arbitrary: idx v)
    (force simp: wf0_FV0_LESS LESS_SUC split: if_splits)+

lemma wf_RESTRICT: "wf idx φ ⟹ wf idx (RESTRICT φ)"
  unfolding RESTRICT_def by (rule wf_RESTRICT_VARS) (auto simp: list_all_iff wf_FV_LESS finite_FV)

lemma lformula_RESTR: "lformula φ ⟹ lformula (RESTR φ)"
  by (induct φ) (auto simp: lformula_Restrict)

lemma lformula_RESTRICT_VARS: "lformula φ ⟹ lformula (RESTRICT_VARS ks vs φ)"
proof (induct ks)
  case (Cons k ks)
  moreover
  { fix vs φ assume "lformula φ"
    then have "lformula (foldr (λx. FAnd (Restrict k x)) vs φ)"
      by (induct vs arbitrary: φ) (auto simp: lformula_Restrict)
  }
  ultimately show ?case by auto
qed (simp add: lformula_RESTR)

lemma lformula_RESTRICT: "lformula φ ⟹ lformula (RESTRICT φ)"
  unfolding RESTRICT_def by (rule lformula_RESTRICT_VARS)

lemma ex_fold_CONS: "∃xs 𝔅. 𝔄 = fold CONS xs 𝔅 ∧ Length 𝔅 = 0 ∧ Length 𝔄 = length xs ∧
   #V 𝔅 = #V 𝔄 ∧ (∀x ∈ set xs. size x = #V 𝔄)"
proof (induct "Length 𝔄" arbitrary: 𝔄)
  case (Suc m)
  from Suc(2) CONS_surj obtain a 𝔅 where "𝔄 = CONS a 𝔅" "#V 𝔅 = #V 𝔄" "size a = #V 𝔄" by force
  moreover with Suc(2) have "Length 𝔅 = m" by (simp add: Length_CONS)
  with Suc(1)[of 𝔅] obtain xs ℭ where "𝔅 = fold CONS xs ℭ" "Length ℭ = 0" "Length 𝔅 = length xs"
    "#V ℭ = #V 𝔅" "∀x ∈ set xs. size x = #V 𝔅" by blast
  ultimately show ?case by (intro exI[of _ "xs @ [a]"] exI[of _ ℭ]) (auto simp: Length_CONS)
qed simp

primcorec L where
  "L idx I = Lang (∃𝔄. Length 𝔄 = 0 ∧ #V 𝔄 = idx ∧ 𝔄 ∈ I)
    (λa. if size a = idx then L idx {𝔅. CONS a 𝔅 ∈ I} else Zero)"

lemma L_empty: "L idx {} = Zero"
  by coinduction auto

lemma L_alt: "L idx I =
    to_language {xs. ∃𝔄 ∈ I. ∃𝔅. 𝔄 = fold CONS (rev xs) 𝔅 ∧ Length 𝔅 = 0 ∧
      #V 𝔅 = idx ∧ (∀x ∈ set xs. size x = idx)}"
  by (coinduction arbitrary: I)
    (auto 0 4 simp: L_empty intro: exI[of _ "{}"] arg_cong[of _ _ to_language])

definition "lang idx φ = L idx {𝔄. 𝔄 ⊨ φ ∧ #V 𝔄 = idx}"
definition "langb idx φ = L idx {𝔄. 𝔄 ⊨b φ ∧ #V 𝔄 = idx}"
definition "language idx φ = L idx {𝔄. sat 𝔄 φ ∧ #V 𝔄 = idx}"
definition "languageb idx φ = L idx {𝔄. satb 𝔄 φ ∧ #V 𝔄 = idx}"

lemma "lformula φ ⟹ lang n (norm φ) = lang n φ"
  unfolding lang_def using satisfies_norm by auto

lemma in_language_Zero[simp]: "¬ in_language Zero w"
  by (induct w) auto

lemma in_language_L_size: "in_language (L idx I) w ⟹ x ∈ set w ⟹ size x = idx"
  by (induct w arbitrary: x I) (auto split: if_splits)

end

sublocale Formula <
  bounded: DA "alphabet idx" "λφ. norm (RESTRICT φ)" "λa φ. norm (lderiv a φ)" "nullable"
     "λφ. wf idx φ ∧ lformula φ" "langb idx"
     "λφ. wf idx φ ∧ lformula φ" "languageb idx" for idx
  using ex_Length_0[of idx]
  by unfold_locales
    (auto simp: lformula_norm lformula_lderiv distinct_alphabet alphabet_size wf_norm wf_lderiv
    langb_def languageb_def nullable_satisfies_bounded wf_RESTRICT lformula_RESTRICT satb_RESTRICT
    satisfies_bounded_norm in_language_L_size satisfies_bounded_lderiv nvars_CONS
    dest: Length_0_inj intro: arg_cong[of _ _ "L (size _)"])

sublocale Formula <
  unbounded?: DA "alphabet idx" "λφ. norm (RESTRICT φ)" "λa φ. norm (lderiv a φ)" "final idx"
     "λφ. wf idx φ ∧ lformula φ" "lang idx"
     "λφ. wf idx φ ∧ lformula φ" "language idx" for idx
  using ex_Length_0[of idx]
  by unfold_locales
    (auto simp: lformula_norm lformula_lderiv distinct_alphabet alphabet_size wf_norm wf_lderiv
    lang_def language_def final_satisfies wf_RESTRICT lformula_RESTRICT sat_RESTRICT
    satisfies_norm in_language_L_size satisfies_lderiv nvars_CONS
    dest: Length_0_inj intro: arg_cong[of _ _ "L (size _)"])

lemma (in Formula) check_eqv_soundness:
  "⟦#V 𝔄 = idx; check_eqv idx φ ψ⟧ ⟹ sat 𝔄 φ ⟷ sat 𝔄 ψ"
  using ex_fold_CONS[of 𝔄]
  by (auto simp: language_def L_alt set_eq_iff
    dest!: soundness[unfolded rel_language_eq] injD[OF bij_is_inj[OF to_language_bij]])
    (metis Length_0_inj rev_rev_ident set_rev)+

lemma (in Formula) bounded_check_eqv_soundness:
  "⟦#V 𝔄 = idx; bounded.check_eqv idx φ ψ⟧ ⟹ satb 𝔄 φ ⟷ satb 𝔄 ψ"
  using ex_fold_CONS[of 𝔄]
  by (auto simp: languageb_def L_alt set_eq_iff
    dest!: bounded.soundness[unfolded rel_language_eq] injD[OF bij_is_inj[OF to_language_bij]])
    (metis Length_0_inj rev_rev_ident set_rev)+

end