Session Formula_Derivatives

Theory While_Default

theory While_Default
imports "HOL-Library.While_Combinator"
begin

context
  fixes d :: "'a"
  and b :: "'a β‡’ bool"
  and c :: "'a β‡’ 'a"
begin

definition while_default :: "'a β‡’ 'a" where
  "while_default s =
     (if βˆ€k. b ((c^^k) s) then d else the (while_option b c s))"

lemma while_default_code[code]:
   "while_default s = (if b s then while_default (c s) else s)"
proof (cases "βˆ€k. b ((c^^k) s)")
  case True
  moreover
  from spec[OF True, of "0"] have "b s" by simp_all
  moreover
  from spec[OF True, of "Suc m" for m] have "βˆ€k. b ((c^^k) (c s))"
    by (simp add: funpow_Suc_right del: funpow.simps(2))
  ultimately show ?thesis unfolding while_default_def by simp
next
  case False
  define k where "k = (LEAST k. Β¬ b ((c ^^ k) s))"
  with False have k: "Β¬ b ((c ^^ k) s)"
    "β‹€l. Β¬ b ((c ^^ l) s) ⟹ k ≀ l"
    by (auto intro!: LeastI_ex[of "Ξ»k. Β¬ b ((c ^^ k) s)"] Least_le)
  show ?thesis
  proof (cases k)
    case 0
    with k(1) have "Β¬ b s" by auto
    with False show ?thesis by (auto simp add: while_default_def while_option_unfold)
  next
    case (Suc k)
    with k(2) have "b ((c ^^ 0) s)" by blast
    then have "b s" by simp
    with k(1) Suc False show ?thesis unfolding while_default_def
      by (subst while_option_unfold) (auto simp add: funpow_Suc_right simp del: funpow.simps(2))
  qed
qed

lemma while_default_rule:
  assumes c: "β‹€s. P s ⟹ b s ⟹ P (c s)"
  and t: "β‹€s. P s ⟹ Β¬ b s ⟹ Q s"
  and s: "P s" and d: "Q d"
  shows "Q (while_default s)"
proof (cases "βˆ€k. b ((c^^k) s)")
  case False
  then obtain t where "while_option b c s = Some t" unfolding while_option_def by auto
  with False show ?thesis using while_option_rule[of P b c s t] while_option_stop[of b c s t] s c t
    by (auto simp add: while_default_def)
qed (simp add: while_default_def d t)

end

end

Theory FSet_More

theory FSet_More
imports  "HOL-Library.FSet"
begin

lemma Suc_pred_image[simp]: "0 βˆ‰ P ⟹ (Ξ»x. Suc (x - Suc 0)) ` P = P"
    unfolding image_def by safe (metis Suc_pred neq0_conv)+

context includes fset.lifting begin

lemmas Suc_pred_fimage[simp] = Suc_pred_image[Transfer.transferred]

end

lemma ffilter_eq_fempty_iff:
  "ffilter P X = {||} ⟷ (βˆ€x. x |∈| X ⟢ Β¬ P x)"
  "{||} = ffilter P X ⟷ (βˆ€x. x |∈| X ⟢ Β¬ P x)"
  by auto

lemma max_ffilter_below[simp]: "⟦x |∈| P; x < n⟧ ⟹
  max n (Suc (fMax (ffilter (Ξ»i. i < n) P))) = n"
  by (metis max.absorb1 Suc_leI fMax_in fempty_iff ffmember_filter)

lemma fMax_boundedD:
  "⟦fMax P < n; x |∈| P⟧ ⟹ x < n"
  "⟦fMax P ≀ n; n |βˆ‰| P; x |∈| P⟧ ⟹ x < n"
  by (metis fMax_ge le_less_trans, metis fMax_ge leD neqE order.strict_trans2)

lemma fMax_ffilter_less: "x |∈| P ⟹ x < n ⟹ fMax (ffilter (λi. i < n) P) < n"
  by (metis fMax_in ffilter_eq_fempty_iff(2) ffmember_filter)

end

Theory Automaton

(*  Author: Dmitriy Traytel *)

section "Equivalence Framework"

(*<*)
theory Automaton
imports
  "HOL-Library.While_Combinator"
  Coinductive_Languages.Coinductive_Language
begin
(*>*)

coinductive rel_language where
  "βŸ¦π”¬ L = 𝔬 K; β‹€a b. R a b ⟹ rel_language R (𝔑 L a) (𝔑 K b)⟧ ⟹ rel_language R L K"

declare rel_language.coinduct[consumes 1, case_names Lang, coinduct pred]

lemma rel_language_alt:
  "rel_language R L K = rel_fun (list_all2 R) (=) (in_language L) (in_language K)"
unfolding rel_fun_def proof (rule iffI, safe del: iffI)
  fix xs ys
  assume "list_all2 R xs ys" "rel_language R L K"
  then show "in_language L xs = in_language K ys"
    by (induct xs ys arbitrary: L K) (auto del: iffI elim: rel_language.cases)
next
  assume "βˆ€xs ys. list_all2 R xs ys ⟢ in_language L xs = in_language K ys"
  then show "rel_language R L K" by (coinduction arbitrary: L K) (auto dest: spec2)
qed

lemma rel_language_eq: "rel_language (=) = (=)"
  unfolding rel_language_alt[abs_def] list.rel_eq fun.rel_eq
  by (subst (2) fun_eq_iff)+
    (auto intro: box_equals[OF _ to_language_in_language to_language_in_language])

abbreviation "𝔑s ≑ fold (Ξ»a L. 𝔑 L a)"

lemma in_language_𝔑s: "in_language (𝔑s w L) v ⟷ in_language L (w @ v)"
  by (induct w arbitrary: L) simp_all

lemma 𝔬_𝔑s: "𝔬 (𝔑s w L) ⟷ in_language L w"
  by (induct w arbitrary: L) auto

lemma in_language_to_language[simp]: "in_language (to_language L) w ⟷ w ∈ L"
  by (metis in_language_to_language mem_Collect_eq)

lemma rtrancl_fold_product:
shows "{((r, s), (f a r, g b s)) | a b r s. a ∈ A ∧ b ∈ B ∧ R a b}^* =
       {((r, s), (fold f w1 r, fold g w2 s)) | w1 w2 r s. w1 ∈ lists A ∧ w2 ∈ lists B ∧ list_all2 R w1 w2}"
  (is "?L = ?R")
proof-
  { fix r s r' s'
    have "((r, s), (r', s')) : ?L ⟹ ((r, s), (r', s')) ∈ ?R"
    proof(induction rule: converse_rtrancl_induct2)
      case refl show ?case by(force intro!: fold_simps(1)[symmetric])
    next
      case step thus ?case by(force intro!: fold_simps(2)[symmetric])
    qed
  }
  hence "β‹€x. x ∈ ?L ⟹ x ∈ ?R" by force
  moreover
  { fix r s r' s'
    { fix w1 w2 assume "list_all2 R w1 w2" "w1 ∈ lists A" "w2 ∈ lists B"
      then have "((r, s), fold f w1 r, fold g w2 s) ∈ ?L"
      proof(induction w1 w2 arbitrary: r s)
        case Nil show ?case by simp
      next
        case Cons thus ?case by (force elim!: converse_rtrancl_into_rtrancl[rotated])
      qed
    }
    hence "((r, s), (r', s')) ∈ ?R ⟹ ((r, s), (r', s')) ∈ ?L" by auto
  }
  hence "β‹€x. x ∈ ?R ⟹ x ∈ ?L" by blast
  ultimately show ?thesis by blast
qed

lemma rtrancl_fold_product1:
shows "{(r, s). βˆƒa ∈ A. s = f a r}^* = {(r, s). βˆƒa ∈ lists A. s = fold f a r}" (is "?L = ?R")
proof-
  { fix r s
    have "(r, s) ∈ ?L ⟹ (r, s) ∈ ?R"
    proof(induction rule: converse_rtrancl_induct)
      case base show ?case by(force intro!: fold_simps(1)[symmetric])
    next
      case step thus ?case by(force intro!: fold_simps(2)[symmetric])
    qed
  } moreover
  { fix r s
    { fix w assume "w ∈ lists A"
      then have "(r, fold f w r) ∈ ?L"
      proof(induction w rule: rev_induct)
        case Nil show ?case by simp
      next
        case snoc thus ?case by (force elim!: rtrancl_into_rtrancl)
      qed
    } 
    hence "(r, s) ∈ ?R ⟹ (r, s) ∈ ?L" by auto
  } ultimately show ?thesis by (auto 10 0)
qed

lemma lang_eq_ext_Nil_fold_Deriv:
  fixes K L A R
  assumes
    "β‹€w. in_language K w ⟹ w ∈ lists A"
    "β‹€w. in_language L w ⟹ w ∈ lists B"
    "β‹€a b. R a b ⟹ a ∈ A ⟷ b ∈ B"
  defines "𝔅 ≑ {(𝔑s w1 K, 𝔑s w2 L) | w1 w2. w1 ∈ lists A ∧ w2 ∈ lists B ∧ list_all2 R w1 w2}"
  shows "rel_language R K L ⟷ (βˆ€(K, L) ∈ 𝔅. 𝔬 K ⟷ 𝔬 L)"
proof
  assume "βˆ€(K, L)βˆˆπ”…. 𝔬 K = 𝔬 L"
  then show "rel_language R K L"
  unfolding 𝔅_def using assms(1,2)
  proof (coinduction arbitrary: K L)
    case (Lang K L)
    then have CIH: "β‹€K' L'. βˆƒw1 w2.
      K' = 𝔑s w1 K ∧ L' = 𝔑s w2 L ∧ w1 ∈ lists A ∧ w2 ∈ lists B ∧ list_all2 R w1 w2 ⟹ 𝔬 K' = 𝔬 L'" and
      [dest]: "β‹€w. in_language K w ⟹ w ∈ lists A" "β‹€w. in_language L w ⟹ w ∈ lists B" 
      by blast+
    show ?case unfolding ex_simps simp_thms
    proof (safe del: iffI)
      show "𝔬 K = 𝔬 L" by (intro CIH[OF exI[where x = "[]"]]) simp
    next
      fix x y w1 w2 assume "βˆ€x∈set w1. x ∈ A" "βˆ€x∈set w2. x ∈ B" "list_all2 R w1 w2" "R x y"
      then show "𝔬 (𝔑s w1 (𝔑 K x)) = 𝔬 (𝔑s w2 (𝔑 L y))"
      proof (cases "x ∈ A ∧ y ∈ B")
        assume "¬ (x ∈ A ∧ y ∈ B)"
        with assms(3)[OF β€ΉR x yβ€Ί] show ?thesis
          by (auto simp: in_language_𝔑s in_language.simps[symmetric] simp del: in_language.simps)
      qed (intro CIH exI[where x = "x # w1"] exI[where x = "y # w2"], auto)
    qed (auto simp add: in_language.simps[symmetric] simp del: in_language.simps)
  qed
qed (auto simp: 𝔅_def rel_language_alt rel_fun_def 𝔬_𝔑s)

subsection β€ΉAbstract Deterministic Automatonβ€Ί

locale DA =
fixes alphabet :: "'a list"
fixes init :: "'t β‡’ 's"
fixes delta :: "'a β‡’ 's β‡’ 's"
fixes accept :: "'s β‡’ bool"
fixes wellformed :: "'s β‡’ bool"
fixes Language :: "'s β‡’ 'a language"
fixes wf :: "'t β‡’ bool"
fixes Lang :: "'t β‡’ 'a language"
assumes distinct_alphabet: "distinct alphabet"
assumes Language_init: "wf t ⟹ Language (init t) = Lang t"
assumes wellformed_init: "wf t ⟹ wellformed (init t)"
assumes Language_alphabet: "⟦wellformed s; in_language (Language s) w⟧ ⟹ w ∈ lists (set alphabet)"
assumes wellformed_delta: "⟦wellformed s; a ∈ set alphabet⟧ ⟹ wellformed (delta a s)"
assumes Language_delta: "⟦wellformed s; a ∈ set alphabet⟧ ⟹ Language (delta a s) = 𝔑 (Language s) a"
assumes accept_Language: "wellformed s ⟹ accept s ⟷ 𝔬 (Language s)"
begin

lemma this: "DA alphabet init delta accept wellformed Language wf Lang" by unfold_locales

lemma wellformed_deltas:
  "⟦wellformed s; w ∈ lists (set alphabet)⟧ ⟹ wellformed (fold delta w s)"
  by (induction w arbitrary: s) (auto simp add: Language_delta wellformed_delta)

lemma Language_deltas:
  "⟦wellformed s; w ∈ lists (set alphabet)⟧ ⟹ Language (fold delta w s) = 𝔑s w (Language s)"
  by (induction w arbitrary: s) (auto simp add: Language_delta wellformed_delta)

textβ€ΉAuxiliary functions:β€Ί
definition reachable :: "'a list β‡’ 's β‡’ 's set" where
  "reachable as s = snd (the (rtrancl_while (Ξ»_. True) (Ξ»s. map (Ξ»a. delta a s) as) s))"

definition automaton :: "'a list β‡’ 's β‡’ (('s * 'a) * 's) set" where
  "automaton as s =
    snd (the
    (let start = (([s], {s}), {});
         test = Ξ»((ws, Z), A). ws β‰  [];
         step = Ξ»((ws, Z), A).
           (let s = hd ws;
                new_edges = map (Ξ»a. ((s, a), delta a s)) as;
                new = remdups (filter (Ξ»ss. ss βˆ‰ Z) (map snd new_edges))
           in ((new @ tl ws, set new βˆͺ Z), set new_edges βˆͺ A))
    in while_option test step start))"

definition match :: "'s β‡’ 'a list β‡’ bool" where
  "match s w = accept (fold delta w s)"

lemma match_correct:
  assumes "wellformed s" "w ∈ lists (set alphabet)"
  shows "match s w ⟷ in_language (Language s) w"
  unfolding match_def accept_Language[OF wellformed_deltas[OF assms]] Language_deltas[OF assms] 𝔬_𝔑s ..

end

locale DAs =
  M: DA alphabet1 init1 delta1 accept1 wellformed1 Language1 wf1 Lang1 +
  N: DA alphabet2 init2 delta2 accept2 wellformed2 Language2 wf2 Lang2
  for alphabet1 :: "'a1 list" and init1 :: "'t1 β‡’ 's1" and delta1 accept1 wellformed1 Language1 wf1 Lang1
  and alphabet2 :: "'a2 list" and init2 :: "'t2 β‡’ 's2" and delta2 accept2 wellformed2 Language2 wf2 Lang2 +
  fixes letter_eq :: "'a1 β‡’ 'a2 β‡’ bool"
  assumes letter_eq: "β‹€a b. letter_eq a b ⟹ a ∈ set alphabet1 ⟷ b ∈ set alphabet2"
begin

abbreviation step where
  "step ≑ (Ξ»(p, q). map (Ξ»(a, b). (delta1 a p, delta2 b q))
    (filter (case_prod letter_eq) (List.product alphabet1 alphabet2)))"

abbreviation closure :: "'s1 * 's2 β‡’ (('s1 * 's2) list * ('s1 * 's2) set) option" where
  "closure ≑ rtrancl_while (Ξ»(p, q). accept1 p = accept2 q) step"

theorem closure_sound_complete:
assumes wf: "wf1 r" "wf2 s"
and result: "closure (init1 r, init2 s) = Some (ws, R)" (is "closure (?r, ?s) = _")
shows "ws = [] ⟷ rel_language letter_eq (Lang1 r) (Lang2 s)"
proof -
  from wf have wellformed: "wellformed1 ?r" "wellformed2 ?s"
    using M.wellformed_init N.wellformed_init by blast+
  note Language_alphabets[simp] =
    M.Language_alphabet[OF wellformed(1)] N.Language_alphabet[OF wellformed(2)]
  note Language_deltass = M.Language_deltas[OF wellformed(1)] N.Language_deltas[OF wellformed(2)]

  have bisim: "rel_language letter_eq (Language1 ?r) (Language2 ?s) =
    (βˆ€a b. (βˆƒw1 w2. a = 𝔑s w1 (Language1 ?r) ∧ b = 𝔑s w2 (Language2 ?s) ∧
      w1 ∈ lists (set alphabet1) ∧ w2 ∈ lists (set alphabet2) ∧ list_all2 letter_eq w1 w2) ⟢
    𝔬 a = 𝔬 b)"
    by (subst lang_eq_ext_Nil_fold_Deriv) (auto dest: letter_eq)

  have leq: "rel_language letter_eq (Language1 ?r) (Language2 ?s) =
  (βˆ€(r', s') ∈ {((r, s), (delta1 a r, delta2 b s)) | a b r s.
    a ∈ set alphabet1 ∧ b ∈ set alphabet2 ∧ letter_eq a b}^* `` {(?r, ?s)}.
    accept1 r' = accept2 s')" using Language_deltass
      M.accept_Language[OF M.wellformed_deltas[OF wellformed(1)]]
      N.accept_Language[OF N.wellformed_deltas[OF wellformed(2)]]
      unfolding rtrancl_fold_product in_lists_conv_set bisim
      by (auto 10 0)
  have "{(x,y). y ∈ set (step x)} =
    {((r, s), (delta1 a r, delta2 b s)) | a b r s. a ∈ set alphabet1 ∧ b ∈ set alphabet2 ∧ letter_eq a b}"
    by auto
  with rtrancl_while_Some[OF result]
  have "(ws = []) = rel_language letter_eq (Language1 ?r) (Language2 ?s)"
    by (auto simp add: leq Ball_def split: if_splits)
  then show ?thesis unfolding M.Language_init[OF wf(1)] N.Language_init[OF wf(2)] .
qed

subsection β€ΉThe overall procedureβ€Ί

definition check_eqv :: "'t1 β‡’ 't2 β‡’ bool" where
"check_eqv r s = (wf1 r ∧ wf2 s ∧ (case closure (init1 r, init2 s) of Some([], _) β‡’ True | _ β‡’ False))"

lemma soundness: 
assumes "check_eqv r s" shows "rel_language letter_eq (Lang1 r) (Lang2 s)"
proof -
  obtain R where "wf1 r" "wf2 s" "closure (init1 r, init2 s) = Some([], R)"
    using assms by (auto simp: check_eqv_def Let_def split: option.splits list.splits)
  from closure_sound_complete[OF this] show "rel_language letter_eq (Lang1 r) (Lang2 s)" by simp
qed

(* completeness needs termination of closure, otherwise result could be None *)

end

subsection β€ΉAbstract Deterministic Finite Automatonβ€Ί

locale DFA = DA +
assumes fin: "wellformed s ⟹ finite {fold delta w s | w. w ∈ lists (set alphabet)}"
begin

lemma finite_rtrancl_delta_Image1:
  "wellformed r ⟹ finite ({(r, s). βˆƒa ∈ set alphabet. s = delta a r}^* `` {r})"
  unfolding rtrancl_fold_product1 by (auto intro: finite_subset[OF _ fin])

lemma
  assumes "wellformed r" "set as βŠ† set alphabet"
  shows reachable: "reachable as r = {fold delta w r | w. w ∈ lists (set as)}"
  and finite_reachable: "finite (reachable as r)"
proof -
  obtain wsZ where *: "rtrancl_while (Ξ»_. True) (Ξ»s. map (Ξ»a. delta a s) as) r = Some wsZ"
    using assms by (atomize_elim, intro rtrancl_while_finite_Some Image_mono rtrancl_mono
      finite_subset[OF _ finite_rtrancl_delta_Image1[of r]]) auto
  then show "reachable as r = {fold delta w r | w. w ∈ lists (set as)}"
    unfolding reachable_def by (cases wsZ)
      (auto dest!: rtrancl_while_Some split: if_splits simp: rtrancl_fold_product1 image_iff)
  then show "finite (reachable as r)" using assms by (force intro: finite_subset[OF _ fin])
qed

end

locale DFAs =
  M: DFA alphabet1 init1 delta1 accept1 wellformed1 Language1 wf1 Lang1 +
  N: DFA alphabet2 init2 delta2 accept2 wellformed2 Language2 wf2 Lang2
  for alphabet1 :: "'a1 list" and init1 :: "'t1 β‡’ 's1" and delta1 accept1 wellformed1 Language1 wf1 Lang1
  and alphabet2 :: "'a2 list" and init2 :: "'t2 β‡’ 's2" and delta2 accept2 wellformed2 Language2 wf2 Lang2 +
  fixes letter_eq :: "'a1 β‡’ 'a2 β‡’ bool"
  assumes letter_eq: "β‹€a b. letter_eq a b ⟹ a ∈ set alphabet1 ⟷ b ∈ set alphabet2"
begin

interpretation DAs by unfold_locales (auto dest: letter_eq)

lemma finite_rtrancl_delta_Image:
  "⟦wellformed1 r; wellformed2 s⟧ ⟹
  finite ({((r, s), (delta1 a r, delta2 b s))| a b r s.
    a ∈ set alphabet1 ∧ b ∈ set alphabet2 ∧ R a b}^* `` {(r, s)})"
  unfolding rtrancl_fold_product Image_singleton
  by (auto intro: finite_subset[OF _ finite_cartesian_product[OF M.fin N.fin]])

lemma "termination":
  assumes "wellformed1 r" "wellformed2 s"
  shows "βˆƒst. closure (r, s) = Some st" (is "βˆƒ_. closure  ?i = _")
proof (rule rtrancl_while_finite_Some)
  show "finite ({(x, st). st ∈ set (step x)}* `` {?i})"
    by (rule finite_subset[OF Image_mono[OF rtrancl_mono]
      finite_rtrancl_delta_Image[OF assms, of letter_eq]]) auto
qed

lemma completeness: 
assumes "wf1 r" "wf2 s" "rel_language letter_eq (Lang1 r) (Lang2 s)" shows "check_eqv r s"
proof -
  obtain ws R where 1: "closure (init1 r, init2 s) = Some (ws, R)" using "termination"
    M.wellformed_init N.wellformed_init assms by fastforce
  with closure_sound_complete[OF _ _ this] assms
  show "check_eqv r s" by (simp add: check_eqv_def)
qed
  
end

sublocale DA < DAs
  alphabet init delta accept wellformed Language wf Lang
  alphabet init delta accept wellformed Language wf Lang "(=)"
  by unfold_locales auto

sublocale DFA < DFAs
  alphabet init delta accept wellformed Language wf Lang
  alphabet init delta accept wellformed Language wf Lang "(=)"
  by unfold_locales auto

lemma (in DA) step_alt: "step = (Ξ»(p, q). map (Ξ»a. (delta a p, delta a q)) alphabet)"
  using distinct_alphabet
proof (induct alphabet)
  case (Cons x xs)
  moreover
  { fix x :: 'a and xs ys :: "'a list"
    assume "x βˆ‰ set xs"
    then have "[(x, y)←List.product xs (x # ys) . x = y] = [(x, y)←List.product xs ys . x = y]"
      by (induct xs arbitrary: x) auto
  }
  moreover
  { fix x :: 'a and xs :: "'a list"
    assume "x βˆ‰ set xs"
    then have "[(x, y)←map (Pair x) xs . x = y] = []"
      by (induct xs) auto
  }
  ultimately show ?case by (auto simp: fun_eq_iff)
qed simp

(*<*)
end
(*>*)

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 𝔄) ⟹
    mExtend k i 𝔄 Pk' = (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 𝔄) ⟹ mSNOC (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

Theory WS1S_Prelim

section β€ΉWS1S Interpretationsβ€Ί

(*<*)
theory WS1S_Prelim
imports
  FSet_More
  Deriving.Compare_Instances
  "List-Index.List_Index"
begin

hide_const (open) cut
(*>*)

definition "eval P x = (x |∈| P)"
definition "downshift P = (Ξ»x. x - Suc 0) |`| (P |-| {|0|})"
definition "upshift P = Suc |`| P"
definition "lift bs i P = (if bs ! i then finsert 0 (upshift P) else upshift P)"
definition "snoc n bs i P = (if bs ! i then finsert n P else P)"
definition "cut n P = ffilter (Ξ»i. i < n) P"
definition "len P = (if P = {||} then 0 else Suc (fMax P))"

datatype order = FO | SO
derive linorder order
instantiation order :: enum begin
  definition "enum_order = [FO, SO]"
  definition "enum_all_order P = (P FO ∧ P SO)"
  definition "enum_ex_order P = (P FO ∨ P SO)"
  lemmas enum_defs = enum_order_def enum_all_order_def enum_ex_order_def
  instance proof qed (auto simp: enum_defs, (metis (full_types) order.exhaust)+)
end

typedef idx = "UNIV :: (nat Γ— nat) set" by (rule UNIV_witness)

setup_lifting type_definition_idx

lift_definition SUC :: "order β‡’ idx β‡’ idx" is
  "Ξ»ord (m, n). case ord of FO β‡’ (Suc m, n) | SO β‡’ (m, Suc n)" .
lift_definition LESS :: "order β‡’ nat β‡’ idx β‡’ bool" is
  "Ξ»ord l (m, n). case ord of FO β‡’ l < m | SO β‡’ l < n" .
abbreviation "LEQ ord l idx ≑ LESS ord l (SUC ord idx)"

definition "MSB Is ≑
  if βˆ€P ∈ set Is. P = {||} then 0 else Suc (Max (⋃P ∈ set Is. fset P))"

lemma MSB_Nil[simp]: "MSB [] = 0"
  unfolding MSB_def by simp

lemma MSB_Cons[simp]: "MSB (I # Is) = max (if I = {||} then 0 else Suc (fMax I)) (MSB Is)"
  unfolding MSB_def including fset.lifting
  by transfer (auto simp: Max_Un list_all_iff Sup_bot_conv(2)[symmetric] simp del: Sup_bot_conv(2))

lemma MSB_append[simp]: "MSB (I1 @ I2) = max (MSB I1) (MSB I2)"
  by (induct I1) auto

lemma MSB_insert_nth[simp]:
  "MSB (insert_nth n P Is) = max (if P = {||} then 0 else Suc (fMax P)) (MSB Is)"
  by (subst (2) append_take_drop_id[of n Is, symmetric])
    (simp only: insert_nth_take_drop MSB_append MSB_Cons MSB_Nil)

lemma MSB_greater:
  "⟦i < length Is; p |∈| Is ! i⟧ ⟹ p < MSB Is"
  unfolding MSB_def by (fastforce simp: Bex_def in_set_conv_nth less_Suc_eq_le intro: Max_ge)

lemma MSB_mono: "set I1 βŠ† set I2 ⟹ MSB I1 ≀ MSB I2"
  unfolding MSB_def including fset.lifting
  by transfer (auto simp: list_all_iff intro!: Max_ge)

lemma MSB_map_index'_CONS[simp]:
  "MSB (map_index' i (lift bs) Is) =
  (if MSB Is = 0 ∧ (βˆ€i ∈ {i ..< i + length Is}. Β¬ bs ! i) then 0 else Suc (MSB Is))"
  by (induct Is arbitrary: i)
   (auto split: if_splits simp: mono_fMax_commute[where f = Suc, symmetric] mono_def
    lift_def upshift_def,
    metis atLeastLessThan_iff le_antisym not_less_eq_eq)

lemma MSB_map_index'_SNOC[simp]:
  "MSB Is ≀ n ⟹ MSB (map_index' i (snoc n bs) Is) =
  (if (βˆ€i ∈ {i ..< i + length Is}. Β¬ bs ! i) then MSB Is else Suc n)"
  by (induct Is arbitrary: i)
    (auto split: if_splits simp: mono_fMax_commute[where f = Suc, symmetric] mono_def
    snoc_def, (metis atLeastLessThan_iff le_antisym not_less_eq_eq)+)

lemma MSB_replicate[simp]: "MSB (replicate n P) = (if P = {||} ∨ n = 0 then 0 else Suc (fMax P))"
  by (induct n) auto

typedef interp =
  "{(n :: nat, I1 :: nat fset list, I2  :: nat fset list) | n I1 I2. MSB (I1 @ I2) ≀ n}"
  by auto

setup_lifting type_definition_interp

lift_definition assigns :: "nat β‡’ interp β‡’ order β‡’ nat fset" ("_β‡—_β‡–_" [900, 999, 999] 999)
  is "Ξ»n (_, I1, I2) ord. case ord of FO β‡’ if n < length I1 then I1 ! n else {||}
    | SO β‡’ if n < length I2 then I2 ! n else {||}" .
lift_definition nvars :: "interp β‡’ idx" ("#V _" [1000] 900)
  is "Ξ»(_, I1, I2). (length I1, length I2)" .
lift_definition Length :: "interp β‡’ nat"
  is "Ξ»(n, _, _). n" .
lift_definition Extend :: "order β‡’ nat β‡’ interp β‡’ nat fset β‡’ interp"
  is "Ξ»ord i (n, I1, I2) P. case ord of
      FO β‡’ (max n (if P = {||} then 0 else Suc (fMax P)), insert_nth i P I1, I2)
    | SO β‡’ (max n (if P = {||} then 0 else Suc (fMax P)), I1, insert_nth i P I2)"
  using MSB_mono by (auto simp del: insert_nth_take_drop split: order.splits)

lift_definition CONS :: "(bool list Γ— bool list) β‡’ interp β‡’ interp"
  is "Ξ»(bs1, bs2) (n, I1, I2).
   (Suc n, map_index (lift bs1) I1, map_index (lift bs2) I2)"
  by auto

lift_definition SNOC :: "(bool list Γ— bool list) β‡’ interp β‡’ interp"
  is "Ξ»(bs1, bs2) (n, I1, I2).
   (Suc n, map_index (snoc n bs1) I1, map_index (snoc n bs2) I2)"
  by (auto simp: Let_def)

type_synonym atom = "bool list Γ— bool list"

lift_definition zero :: "idx β‡’ atom"
  is "Ξ»(m, n). (replicate m False, replicate n False)" .

definition "extend ord b ≑
  Ξ»(bs1, bs2). case ord of FO β‡’ (b # bs1, bs2) | SO β‡’ (bs1, b # bs2)"
lift_definition size_atom :: "bool list Γ— bool list β‡’ idx"
  is "Ξ»(bs1, bs2). (length bs1, length bs2)" .

lift_definition Οƒ :: "idx β‡’ atom list"
  is "(Ξ»(n, N). map (Ξ»bs. (take n bs, drop n bs)) (List.n_lists (n + N) [True, False]))" .

lemma fMin_fimage_Suc[simp]: "x |∈| A ⟹ fMin (Suc |`| A) = Suc (fMin A)"
  by (rule fMin_eqI) (auto intro: fMin_in)

lemma fMin_eq_0[simp]: "0 |∈| A ⟹ fMin A = (0 :: nat)"
  by (rule fMin_eqI) auto

lemma insert_nth_Cons[simp]:
  "insert_nth i x (y # xs) = (case i of 0 β‡’ x # y # xs | Suc i β‡’ y # insert_nth i x xs)"
  by (cases i) simp_all

lemma insert_nth_commute[simp]:
  assumes "j ≀ i" "i ≀ length xs"
  shows "insert_nth j y (insert_nth i x xs) = insert_nth (Suc i) x (insert_nth j y xs)"
  using assms by (induct xs arbitrary: i j) (auto simp del: insert_nth_take_drop split: nat.splits)

lemma SUC_SUC[simp]: "SUC ord (SUC ord' idx) = SUC ord' (SUC ord idx)"
  by transfer (auto split: order.splits)

lemma LESS_SUC[simp]:
  "LESS ord 0 (SUC ord idx)"
  "LESS ord (Suc l) (SUC ord idx) = LESS ord l idx"
  "ord β‰  ord' ⟹ LESS ord l (SUC ord' idx) = LESS ord l idx"
  "LESS ord l idx ⟹ LESS ord l (SUC ord' idx)"
  by (transfer, force split: order.splits)+

lemma nvars_Extend[simp]:
  "#V (Extend ord i 𝔄 P) = SUC ord (#V 𝔄)"
  by (transfer, force split: order.splits)

lemma Length_Extend[simp]:
  "Length (Extend k i 𝔄 P) = max (Length 𝔄) (if P = {||} then 0 else Suc (fMax P))"
  unfolding max_def by (split if_splits, transfer) (force split: order.splits)

lemma assigns_Extend[simp]:
  "LEQ ord i (#V 𝔄) ⟹mExtend ord i 𝔄 Pord = (if m = i then P else (if m > i then m - Suc 0 else m)𝔄ord)"
  "ord β‰  ord' ⟹ mExtend ord i 𝔄 Pord' = m𝔄ord'"
  by (transfer, force simp: min_def nth_append split: order.splits)+

lemma Extend_commute_safe[simp]:
  "⟦j ≀ i; LEQ ord i (#V 𝔄)⟧ ⟹
    Extend ord j (Extend ord i 𝔄 P1) P2 = Extend ord (Suc i) (Extend ord j 𝔄 P2) P1"
  by (transfer,
    force simp del: insert_nth_take_drop simp: replicate_add[symmetric] split: order.splits)

lemma Extend_commute_unsafe:
  "ord β‰  ord' ⟹ Extend ord j (Extend ord' i 𝔄 P1) P2 = Extend ord' i (Extend ord j 𝔄 P2) P1"
  by (transfer, force simp: replicate_add[symmetric] split: order.splits)

lemma Length_CONS[simp]:
  "Length (CONS x 𝔄) = Suc (Length 𝔄)"
  by (transfer, force split: order.splits)

lemma Length_SNOC[simp]:
  "Length (SNOC x 𝔄) = Suc (Length 𝔄)"
  by (transfer, force simp: Let_def split: order.splits)

lemma nvars_CONS[simp]:
  "#V (CONS x 𝔄) = #V 𝔄"
  by (transfer, force)

lemma nvars_SNOC[simp]:
  "#V (SNOC x 𝔄) = #V 𝔄"
  by (transfer, force simp: Let_def)

lemma assigns_CONS[simp]:
  assumes "#V 𝔄 = size_atom bs1_bs2"
  shows "LESS ord x (#V 𝔄) ⟹ xCONS bs1_bs2 𝔄ord =
    (if case_prod case_order bs1_bs2 ord ! x then finsert 0 (upshift (x𝔄ord)) else upshift (x𝔄ord))"
  by (insert assms, transfer) (auto simp: lift_def split: order.splits)

lemma assigns_SNOC[simp]:
  assumes "#V 𝔄 = size_atom bs1_bs2"
  shows "LESS ord x (#V 𝔄) ⟹ xSNOC bs1_bs2 𝔄ord =
    (if case_prod case_order bs1_bs2 ord ! x then finsert (Length 𝔄) (x𝔄ord) else x𝔄ord)"
  by (insert assms, transfer) (force simp: snoc_def Let_def split: order.splits)

lemma map_index'_eq_conv[simp]:
  "map_index' i f xs = map_index' j g xs = (βˆ€k < length xs. f (i + k) (xs ! k) = g (j + k) (xs ! k))"
proof (induct xs arbitrary: i j)
  case Cons from Cons(1)[of "Suc i" "Suc j"] show ?case by (auto simp: nth_Cons split: nat.splits)
qed simp

lemma fMax_Diff_0[simp]: "Suc m |∈| P ⟹ fMax (P |-| {|0|}) = fMax P"
  by (rule fMax_eqI) (auto intro: fMax_in dest: fMax_ge)

lemma Suc_fMax_pred_fimage[simp]:
  assumes "Suc p |∈| P" "0 |βˆ‰| P"
  shows "Suc (fMax ((Ξ»x. x - Suc 0) |`| P)) = fMax P"
  using assms by (subst mono_fMax_commute[of Suc, unfolded mono_def, simplified]) (auto simp: o_def)

lemma Extend_CONS[simp]: "#V 𝔄 = size_atom x ⟹ Extend ord 0 (CONS x 𝔄) P =
  CONS (extend ord (eval P 0) x) (Extend ord 0 𝔄 (downshift P))"
  by transfer (auto simp: extend_def o_def gr0_conv_Suc
    mono_fMax_commute[of Suc, symmetric, unfolded mono_def, simplified]
    lift_def upshift_def downshift_def eval_def
    dest!: fsubset_fsingletonD split: order.splits)

lemma size_atom_extend[simp]:
  "size_atom (extend ord b x) = SUC ord (size_atom x)"
  unfolding extend_def by transfer (simp split: prod.splits order.splits)

lemma size_atom_zero[simp]:
  "size_atom (zero idx) = idx"
  unfolding extend_def by transfer (simp split: prod.splits order.splits)

lemma interp_eqI:
  "⟦Length 𝔄 = Length 𝔅; #V 𝔄 = #V 𝔅; β‹€m k. LESS k m (#V 𝔄) ⟹ m𝔄k = m𝔅k⟧ ⟹ 𝔄 = 𝔅"
  by transfer (force split: order.splits intro!: nth_equalityI)

lemma Extend_SNOC_cut[unfolded eval_def cut_def Length_SNOC, simp]:
  "⟦len P ≀ Length (SNOC x 𝔄); #V 𝔄 = size_atom x⟧ ⟹
  Extend ord 0 (SNOC x 𝔄) P =
    SNOC (extend ord (if eval P (Length 𝔄) then True else False) x) (Extend ord 0 𝔄 (cut (Length 𝔄) P))"
  by transfer (fastforce simp: extend_def len_def cut_def ffilter_eq_fempty_iff snoc_def eval_def
    split: if_splits order.splits dest: fMax_ge fMax_boundedD intro: fMax_in)

lemma nth_replicate_simp: "replicate m x ! i = (if i < m then x else [] ! (i - m))"
  by (induct m arbitrary: i) (auto simp: nth_Cons')

lemma MSB_eq_SucD: "MSB Is = Suc x ⟹ βˆƒP∈set Is. x |∈| P"
  using Max_in[of "⋃x∈set Is. fset x"]
  unfolding MSB_def by (force simp: fmember_def split: if_splits)

lemma append_replicate_inj:
  assumes "xs β‰  [] ⟹ last xs β‰  x" and "ys β‰  [] ⟹ last ys β‰  x"
  shows "xs @ replicate m x = ys @ replicate n x ⟷ (xs = ys ∧ m = n)"
proof safe
  from assms have assms': "xs β‰  [] ⟹ rev xs ! 0 β‰  x" "ys β‰  [] ⟹ rev ys ! 0 β‰  x"
    by (auto simp: hd_rev hd_conv_nth[symmetric])
  assume *: "xs @ replicate m x = ys @ replicate n x"
  then have "rev (xs @ replicate m x) = rev (ys @ replicate n x)" ..
  then have "replicate m x @ rev xs = replicate n x @ rev ys" by simp
  then have "take (max m n) (replicate m x @ rev xs) = take (max m n) (replicate n x @ rev ys)" by simp
  then have "replicate m x @ take (max m n - m) (rev xs) =
    replicate n x @ take (max m n - n) (rev ys)" by (auto simp: min_def max_def split: if_splits)
  then have "(replicate m x @ take (max m n - m) (rev xs)) ! min m n =
    (replicate n x @ take (max m n - n) (rev ys)) ! min m n" by simp
  with arg_cong[OF *, of length, simplified] assms' show "m = n"
    by (cases "xs = []" "ys = []" rule: bool.exhaust[case_product bool.exhaust])
      (auto simp: min_def nth_append split: if_splits)
  with * show "xs = ys" by auto
qed

lemma fin_lift[simp]: "m |∈| lift bs i (I ! i) ⟷ (case m of 0 β‡’ bs ! i | Suc m β‡’ m |∈| I ! i)"
  unfolding lift_def upshift_def by (auto split: nat.splits)

lemma ex_Length_0[simp]:
  "βˆƒπ”„. Length 𝔄 = 0 ∧ #V 𝔄 = idx"
  by transfer (auto intro!: exI[of _ "replicate m {||}" for m])

lemma is_empty_inj[simp]: "⟦Length 𝔄 = 0; Length 𝔅 = 0; #V 𝔄 = #V π”…βŸ§ ⟹ 𝔄 = 𝔅"
  by transfer (simp add: list_eq_iff_nth_eq split: prod.splits,
    metis MSB_greater fMax_in less_nat_zero_code)

lemma set_Οƒ_length_atom[simp]: "(x ∈ set (Οƒ idx)) ⟷ idx = size_atom x"
  by transfer (auto simp: set_n_lists enum_UNIV image_iff intro!: exI[of _ "I1 @ I2" for I1 I2])

lemma distinct_Οƒ[simp]: "distinct (Οƒ idx)"
  by transfer (auto 0 4 simp: distinct_map distinct_n_lists set_n_lists inj_on_def
    intro: iffD2[OF append_eq_append_conv]
      box_equals[OF _ append_take_drop_id append_take_drop_id, of n _ n for n])

lemma fMin_less_Length[simp]: "x |∈| m1𝔄k ⟹ fMin (m1𝔄k) < Length 𝔄"
  by transfer
    (force elim: order.strict_trans2[OF MSB_greater, rotated -1] intro: fMin_in split: order.splits)

lemma fMax_less_Length[simp]: "x |∈| m1𝔄k ⟹ fMax (m1𝔄k) < Length 𝔄"
  by transfer
    (force elim: order.strict_trans2[OF MSB_greater, rotated -1] intro: fMax_in split: order.splits)

lemma min_Length_fMin[simp]: "x |∈| m1𝔄k ⟹ min (Length 𝔄) (fMin (m1𝔄k)) = fMin (m1𝔄k)"
  using fMin_less_Length[of x m1 𝔄 k] unfolding fMin_def by auto

lemma max_Length_fMin[simp]: "x |∈| m1𝔄k ⟹ max (Length 𝔄) (fMin (m1𝔄k)) = Length 𝔄"
  using fMin_less_Length[of x m1 𝔄 k] unfolding fMin_def by auto

lemma min_Length_fMax[simp]: "x |∈| m1𝔄k ⟹ min (Length 𝔄) (fMax (m1𝔄k)) = fMax (m1𝔄k)"
  using fMax_less_Length[of x m1 𝔄 k] unfolding fMax_def by auto

lemma max_Length_fMax[simp]: "x |∈| m1𝔄k ⟹ max (Length 𝔄) (fMax (m1𝔄k)) = Length 𝔄"
  using fMax_less_Length[of x m1 𝔄 k] unfolding fMax_def by auto

lemma assigns_less_Length[simp]: "x |∈| m1𝔄k ⟹ x < Length 𝔄"
  by transfer (force dest: MSB_greater split: order.splits if_splits)

lemma Length_notin_assigns[simp]: "Length 𝔄 |βˆ‰| m𝔄k"
  by (metis assigns_less_Length less_not_refl)

lemma nth_zero[simp]: "LESS ord m (#V 𝔄) ⟹ Β¬ case_prod case_order (zero (#V 𝔄)) ord ! m"
  by transfer (auto split: order.splits)

lemma in_fimage_Suc[simp]: "x |∈| Suc |`| A ⟷ (βˆƒy. y |∈| A ∧ x = Suc y)"
  by blast

lemma fimage_Suc_inj[simp]: "Suc |`| A = Suc |`| B ⟷ A = B"
  by blast

lemma MSB_eq0_D: "MSB I = 0 ⟹ x < length I ⟹ I ! x = {||}"
  unfolding MSB_def by (auto split: if_splits)

lemma Suc_in_fimage_Suc: "Suc x |∈| Suc |`| X ⟷ x |∈| X"
  by auto

lemma Suc_in_fimage_Suc_o_Suc[simp]: "Suc x |∈| (Suc ∘ Suc) |`| X ⟷ x |∈| Suc |`| X"
  by auto

lemma finsert_same_eq_iff[simp]: "finsert k X = finsert k Y ⟷ X |-| {|k|} = Y |-| {|k|}"
  by auto


lemma fimage_Suc_o_Suc_eq_fimage_Suc_iff[simp]:
  "((Suc ∘ Suc) |`| X = Suc |`| Y) ⟷ (Suc |`| X = Y)"
  by (metis fimage_Suc_inj fset.map_comp)

lemma fMax_image_Suc[simp]: "x |∈| P ⟹ fMax (Suc |`| P) = Suc (fMax P)"
  by (rule fMax_eqI) (metis Suc_le_mono fMax_ge fimageE, metis fimageI fempty_iff fMax_in)

lemma fimage_Suc_eq_singleton[simp]: "(fimage Suc Z = {|y|}) ⟷ (βˆƒx. Z = {|x|} ∧ Suc x = y)"
  by (cases y) auto

lemma len_downshift_helper:
  "x |∈| P ⟹ Suc (fMax ((Ξ»x. x - Suc 0) |`| (P |-| {|0|}))) β‰  fMax P ⟹ xa |∈| P ⟹ xa = 0"
proof -
  assume a1: "xa |∈| P"
  assume a2: "Suc (fMax ((Ξ»x. x - Suc 0) |`| (P |-| {|0|}))) β‰  fMax P"
  have "xa |∈| {|0|} ⟢ xa = 0" by fastforce
  moreover
  { assume "xa |βˆ‰| {|0|}"
    hence "0 |βˆ‰| P |-| {|0|} ∧ xa |βˆ‰| {|0|}" by blast
    then obtain esk11 :: "nat β‡’ nat" where "xa = 0" using a1 a2 by (metis Suc_fMax_pred_fimage fMax_Diff_0 fminus_iff not0_implies_Suc) }
  ultimately show "xa = 0" by blast
qed

lemma CONS_inj[simp]: "size_atom x = #V 𝔄 ⟹ size_atom y = #V 𝔄 ⟹ #V 𝔄 = #V 𝔅 ⟹
  CONS x 𝔄 = CONS y 𝔅 ⟷ (x = y ∧ 𝔄 = 𝔅)"
  by transfer (auto simp: list_eq_iff_nth_eq lift_def upshift_def split: if_splits; blast)

lemma Suc_minus1: "Suc (x - Suc 0) = (if x = 0 then Suc 0 else x)"
  by auto

lemma fset_eq_empty_iff: "(fset X = {}) = (X = {||})"
  by (metis bot_fset.rep_eq fset_inverse)

lemma fset_le_singleton_iff: "(fset X βŠ† {x}) = (X = {||} ∨ X = {|x|})"
  by (metis finsert.rep_eq fset_eq_empty_iff fset_inject order_refl singleton_insert_inj_eq subset_singletonD)

lemma MSB_decreases:
  "MSB I ≀ Suc m ⟹ MSB (map (Ξ»X. (Ξ»I1. I1 - Suc 0) |`| (X |-| {|0|})) I) ≀ m"
  unfolding MSB_def
  by (auto simp add: not_le less_Suc_eq_le fset_eq_empty_iff fset_le_singleton_iff
    split: if_splits dest!: iffD1[OF Max_le_iff, rotated -1] iffD1[OF Max_ge_iff, rotated -1]; force)

lemma CONS_surj[dest]: "Length 𝔄 > 0 ⟹
  βˆƒx 𝔅. 𝔄 = CONS x 𝔅 ∧ #V 𝔅 = #V 𝔄 ∧ size_atom x = #V 𝔄"
  by transfer (auto simp: gr0_conv_Suc list_eq_iff_nth_eq lift_def upshift_def split: if_splits
    intro!: exI[of _ "map (λX. 0 |∈| X) _"] exI[of _ "map (λX. (λx. x - Suc 0) |`| (X |-| {|0|})) _"],
    auto simp: MSB_decreases upshift_def Suc_minus1 fimage_iff intro: rev_fBexI split: if_splits)
 
(*<*)
end
(*>*)

Theory WS1S_Formula

section β€ΉConcrete Atomic WS1S Formulas (Minimum Semantics for FO Variables)β€Ί

(*<*)
theory WS1S_Formula
imports
  Abstract_Formula
  WS1S_Prelim
begin
(*>*)

datatype (FOV0: 'fo, SOV0: 'so) atomic =
  Fo 'fo |
  Eq_Const "nat option" 'fo nat |
  Less "bool option" 'fo 'fo |
  Plus_FO "nat option" 'fo 'fo nat |
  Eq_FO bool 'fo 'fo |
  Eq_SO 'so 'so |
  Suc_SO bool bool 'so 'so |
  Empty 'so |
  Singleton 'so |
  Subset 'so 'so |
  In bool 'fo 'so |
  Eq_Max bool 'fo 'so |
  Eq_Min bool 'fo 'so |
  Eq_Union 'so 'so 'so |
  Eq_Inter 'so 'so 'so |
  Eq_Diff 'so 'so 'so |
  Disjoint 'so 'so |
  Eq_Presb "nat option" 'so nat

derive linorder option
derive linorder atomic ― β€Ήvery slowβ€Ί

type_synonym fo = nat
type_synonym so = nat
type_synonym ws1s = "(fo, so) atomic"
type_synonym formula = "(ws1s, order) aformula"

primrec wf0 where
  "wf0 idx (Fo m) = LESS FO m idx"
| "wf0 idx (Eq_Const i m n) = (LESS FO m idx ∧ (case i of Some i β‡’ i ≀ n | _ β‡’ True))"
| "wf0 idx (Less _ m1 m2) = (LESS FO m1 idx ∧ LESS FO m2 idx)"
| "wf0 idx (Plus_FO i m1 m2 n) =
  (LESS FO m1 idx ∧ LESS FO m2 idx ∧ (case i of Some i β‡’ i ≀ n | _ β‡’ True))"
| "wf0 idx (Eq_FO _ m1 m2) = (LESS FO m1 idx ∧ LESS FO m2 idx)"
| "wf0 idx (Eq_SO M1 M2) = (LESS SO M1 idx ∧ LESS SO M2 idx)"
| "wf0 idx (Suc_SO br bl M1 M2) = (LESS SO M1 idx ∧ LESS SO M2 idx)"
| "wf0 idx (Empty M) = LESS SO M idx"
| "wf0 idx (Singleton M) = LESS SO M idx"
| "wf0 idx (Subset M1 M2) = (LESS SO M1 idx ∧ LESS SO M2 idx)"
| "wf0 idx (In _ m M) = (LESS FO m idx ∧ LESS SO M idx)"
| "wf0 idx (Eq_Max _ m M) = (LESS FO m idx ∧ LESS SO M idx)"
| "wf0 idx (Eq_Min _ m M) = (LESS FO m idx ∧ LESS SO M idx)"
| "wf0 idx (Eq_Union M1 M2 M3) = (LESS SO M1 idx ∧ LESS SO M2 idx ∧ LESS SO M3 idx)"
| "wf0 idx (Eq_Inter M1 M2 M3) = (LESS SO M1 idx ∧ LESS SO M2 idx ∧ LESS SO M3 idx)"
| "wf0 idx (Eq_Diff M1 M2 M3) = (LESS SO M1 idx ∧ LESS SO M2 idx ∧ LESS SO M3 idx)"
| "wf0 idx (Disjoint M1 M2) = (LESS SO M1 idx ∧ LESS SO M2 idx)"
| "wf0 idx (Eq_Presb _ M n) = LESS SO M idx"

inductive lformula0 where
  "lformula0 (Fo m)"
| "lformula0 (Eq_Const None m n)"
| "lformula0 (Less None m1 m2)"
| "lformula0 (Plus_FO None m1 m2 n)"
| "lformula0 (Eq_FO False m1 m2)"
| "lformula0 (Eq_SO M1 M2)"
| "lformula0 (Suc_SO False bl M1 M2)"
| "lformula0 (Empty M)"
| "lformula0 (Singleton M)"
| "lformula0 (Subset M1 M2)"
| "lformula0 (In False m M)"
| "lformula0 (Eq_Max False m M)"
| "lformula0 (Eq_Min False m M)"
| "lformula0 (Eq_Union M1 M2 M3)"
| "lformula0 (Eq_Inter M1 M2 M3)"
| "lformula0 (Eq_Diff M1 M2 M3)"
| "lformula0 (Disjoint M1 M2)"
| "lformula0 (Eq_Presb None M n)"

code_pred lformula0 .

declare lformula0.intros[simp]

inductive_cases lformula0E[elim]: "lformula0 a"

abbreviation "FV0 ≑ case_order FOV0 SOV0"

fun find0 where
  "find0 FO i (Fo m) = (i = m)"
| "find0 FO i (Eq_Const _ m _) = (i = m)"
| "find0 FO i (Less _ m1 m2) = (i = m1 ∨ i = m2)"
| "find0 FO i (Plus_FO _ m1 m2 _) = (i = m1 ∨ i = m2)"
| "find0 FO i (Eq_FO _ m1 m2) = (i = m1 ∨ i = m2)"
| "find0 SO i (Eq_SO M1 M2) = (i = M1 ∨ i = M2)"
| "find0 SO i (Suc_SO _ _ M1 M2) = (i = M1 ∨ i = M2)"
| "find0 SO i (Empty M) = (i = M)"
| "find0 SO i (Singleton M) = (i = M)"
| "find0 SO i (Subset M1 M2) = (i = M1 ∨ i = M2)"
| "find0 FO i (In _ m _) = (i = m)"
| "find0 SO i (In _ _ M) = (i = M)"
| "find0 FO i (Eq_Max _ m _) = (i = m)"
| "find0 SO i (Eq_Max _ _ M) = (i = M)"
| "find0 FO i (Eq_Min _ m _) = (i = m)"
| "find0 SO i (Eq_Min _ _ M) = (i = M)"
| "find0 SO i (Eq_Union M1 M2 M3) = (i = M1 ∨ i = M2 ∨ i = M3)"
| "find0 SO i (Eq_Inter M1 M2 M3) = (i = M1 ∨ i = M2 ∨ i = M3)"
| "find0 SO i (Eq_Diff M1 M2 M3) = (i = M1 ∨ i = M2 ∨ i = M3)"
| "find0 SO i (Disjoint M1 M2) = (i = M1 ∨ i = M2)"
| "find0 SO i (Eq_Presb _ M _) = (i = M)"
| "find0 _ _ _ = False"

abbreviation "decr0 ord k ≑ map_atomic (case_order (dec k) id ord) (case_order id (dec k) ord)"

lemma sum_pow2_image_Suc:
  "finite X ⟹ sum ((^) (2 :: nat)) (Suc ` X) = 2 * sum ((^) 2) X"
  by (induct X rule: finite_induct) (auto intro: trans[OF sum.insert])

lemma sum_pow2_insert0:
  "⟦finite X; 0 βˆ‰ X⟧ ⟹ sum ((^) (2 :: nat)) (insert 0 X) = Suc (sum ((^) 2) X)"
  by (induct X rule: finite_induct) (auto intro: trans[OF sum.insert])

lemma sum_pow2_upto: "sum ((^) (2 :: nat)) {0 ..< x} = 2 ^ x - 1"
  by (induct x) (auto simp: algebra_simps)

lemma sum_pow2_inj:
  "⟦finite X; finite Y; (βˆ‘x∈X. 2 ^ x :: nat) = (βˆ‘x∈Y. 2 ^ x)⟧ ⟹ X = Y"
  (is "_ ⟹ _ ⟹ ?f X = ?f Y ⟹ _")
proof (induct X arbitrary: Y rule: finite_linorder_max_induct)
  case (insert x X)
  from insert(2) have "?f X ≀ ?f {0 ..< x}" by (intro sum_mono2) auto
  also have "… < 2 ^ x" by (induct x) simp_all
  finally have "?f X < 2 ^ x" .
  moreover from insert(1,2) have *: "?f X + 2 ^ x = ?f Y"
    using trans[OF sym[OF insert(5)] sum.insert] by auto
  ultimately have "?f Y < 2 ^ Suc x" by simp

  have "βˆ€y ∈ Y. y ≀ x"
  proof (rule ccontr)
    assume "Β¬ (βˆ€y∈Y. y ≀ x)"
    then obtain y where "y ∈ Y" "Suc x ≀ y" by auto
    from this(2) have "2 ^ Suc x ≀ (2 ^ y :: nat)" by (intro power_increasing) auto
    also from β€Ήy ∈ Yβ€Ί insert(4) have "… ≀ ?f Y" by (metis order.refl sum.remove trans_le_add1)
    finally show False using β€Ή?f Y < 2 ^ Suc xβ€Ί by simp
  qed

  { assume "x βˆ‰ Y"
    with β€Ήβˆ€y ∈ Y. y ≀ xβ€Ί have "?f Y ≀ ?f {0 ..< x}" by (intro sum_mono2) (auto simp: le_less)
    also have "… < 2 ^ x" by (induct x) simp_all
    finally have "?f Y < 2 ^ x" .
    with * have False by auto
  }
  then have "x ∈ Y" by blast

  from insert(4) have "?f (Y - {x}) + 2 ^ x = ?f (insert x (Y - {x}))"by (subst sum.insert) auto
  also have "… = ?f X + 2 ^ x" unfolding * using β€Ήx ∈ Yβ€Ί by (simp add: insert_absorb)
  finally have "?f X = ?f (Y - {x})" by simp
  with insert(3,4) have "X = Y - {x}" by simp
  with β€Ήx ∈ Yβ€Ί show ?case by auto
qed simp

lemma finite_pow2_eq:
  fixes n :: nat
  shows "finite {i. 2 ^ i = n}"
proof -
  have "((^) 2) ` {i. 2 ^ i = n} βŠ† {n}" by auto
  then have "finite (((^) (2 :: nat)) ` {i. 2 ^ i = n})" by (rule finite_subset) blast
  then show "finite {i. 2 ^ i = n}" by (rule finite_imageD) (auto simp: inj_on_def)
qed

lemma finite_pow2_le[simp]:
  fixes n :: nat
  shows "finite {i. 2 ^ i ≀ n}"
  by (induct n) (auto simp: le_Suc_eq finite_pow2_eq)

lemma le_pow2[simp]: "x ≀ y ⟹ x ≀ 2 ^ y"
  by (induct x arbitrary: y) (force simp add: Suc_le_eq order.strict_iff_order)+

lemma ld_bounded: "Max {i. 2 ^ i ≀ Suc n} ≀ Suc n" (is "?m ≀ Suc n")
proof -
  have "?m ≀ 2 ^ ?m" by (rule le_pow2) simp
  moreover
  have "?m ∈ {i. 2 ^ i ≀ Suc n}" by (rule Max_in) (auto intro: exI[of _ 0])
  then have "2 ^ ?m ≀ Suc n" by simp
  ultimately show ?thesis by linarith
qed

primrec satisfies0 where
  "satisfies0 𝔄 (Fo m) = (m𝔄FO β‰  {||})"
| "satisfies0 𝔄 (Eq_Const i m n) =
   (let P = m𝔄FO in if P = {||}
   then (case i of Some i β‡’ Length 𝔄 = i | _ β‡’ False)
   else fMin P = n)"
| "satisfies0 𝔄 (Less b m1 m2) =
   (let P1 = m1𝔄FO; P2 = m2𝔄FO in if P1 = {||} ∨ P2 = {||}
   then (case b of None β‡’ False | Some True β‡’ P2 = {||} | Some False β‡’ P1 β‰  {||})
   else fMin P1 < fMin P2)"
| "satisfies0 𝔄 (Plus_FO i m1 m2 n) =
   (let P1 = m1𝔄FO; P2 = m2𝔄FO in if P1 = {||} ∨ P2 = {||}
   then (case i of Some 0 β‡’ P1 = P2 | Some i β‡’ P2 β‰  {||} ∧ fMin P2 + i = Length 𝔄 | _ β‡’ False)
   else fMin P1 = fMin P2 + n)"
| "satisfies0 𝔄 (Eq_FO b m1 m2) =
   (let P1 = m1𝔄FO; P2 = m2𝔄FO in if P1 = {||} ∨ P2 = {||}
   then b ∧ P1 = P2
   else fMin P1 = fMin P2)"
| "satisfies0 𝔄 (Eq_SO M1 M2) = (M1𝔄SO = M2𝔄SO)"
| "satisfies0 𝔄 (Suc_SO br bl M1 M2) =
   ((if br then finsert (Length 𝔄) else id) (M1𝔄SO) =
    (if bl then finsert 0 else id) (Suc |`| M2𝔄SO))"
| "satisfies0 𝔄 (Empty M) = (M𝔄SO = {||})"
| "satisfies0 𝔄 (Singleton M) = (βˆƒx. M𝔄SO = {|x|})"
| "satisfies0 𝔄 (Subset M1 M2) = (M1𝔄SO |βŠ†| M2𝔄SO)"
| "satisfies0 𝔄 (In b m M) =
   (let P = m𝔄FO in if P = {||} then b else fMin P |∈| M𝔄SO)"
| "satisfies0 𝔄 (Eq_Max b m M) =
   (let P1 = m𝔄FO; P2 = M𝔄SO in if b then P1 = {||}
   else if P1 = {||} ∨ P2 = {||} then False else fMin P1 = fMax P2)"
| "satisfies0 𝔄 (Eq_Min b m M) =
   (let P1 = m𝔄FO; P2 = M𝔄SO in if P1 = {||} ∨ P2 = {||} then b ∧ P1 = P2 else fMin P1 = fMin P2)"
| "satisfies0 𝔄 (Eq_Union M1 M2 M3) = (M1𝔄SO = M2𝔄SO |βˆͺ| M3𝔄SO)"
| "satisfies0 𝔄 (Eq_Inter M1 M2 M3) = (M1𝔄SO = M2𝔄SO |∩| M3𝔄SO)"
| "satisfies0 𝔄 (Eq_Diff M1 M2 M3) = (M1𝔄SO = M2𝔄SO |-| M3𝔄SO)"
| "satisfies0 𝔄 (Disjoint M1 M2) = (M1𝔄SO |∩| M2𝔄SO = {||})"
| "satisfies0 𝔄 (Eq_Presb i M n) = (((βˆ‘x∈fset (M𝔄SO). 2 ^ x) = n) ∧
   (case i of None β‡’ True | Some l β‡’ Length 𝔄 = l))"

fun lderiv0 where
  "lderiv0 (bs1, bs2) (Fo m) = (if bs1 ! m then FBool True else FBase (Fo m))"
| "lderiv0 (bs1, bs2) (Eq_Const None m n) = (if n = 0 ∧ bs1 ! m then FBool True
     else if n = 0 ∨ bs1 ! m then FBool False else FBase (Eq_Const None m (n - 1)))"
| "lderiv0 (bs1, bs2) (Less None m1 m2) = (case (bs1 ! m1, bs1 ! m2) of
    (False, False) β‡’ FBase (Less None m1 m2)
  | (True, False) β‡’ FBase (Fo m2)
  | _ β‡’ FBool False)"|
 "lderiv0 (bs1, bs2) (Eq_FO False m1 m2) = (case (bs1 ! m1, bs1 ! m2) of
    (False, False) β‡’ FBase (Eq_FO False m1 m2)
  | (True, True) β‡’ FBool True
  | _ β‡’ FBool False)"
| "lderiv0 (bs1, bs2) (Plus_FO None m1 m2 n) = (if n = 0
  then
    (case (bs1 ! m1, bs1 ! m2) of
      (False, False) β‡’ FBase (Plus_FO None m1 m2 n)
    | (True, True) β‡’ FBool True
    | _ β‡’ FBool False)
  else 
    (case (bs1 ! m1, bs1 ! m2) of
      (False, False) β‡’ FBase (Plus_FO None m1 m2 n)
    | (False, True) β‡’ FBase (Eq_Const None m1 (n - 1))
    | _ β‡’ FBool False))"
| "lderiv0 (bs1, bs2) (Eq_SO M1 M2) =
  (if bs2 ! M1 = bs2 ! M2 then FBase (Eq_SO M1 M2) else FBool False)"
| "lderiv0 (bs1, bs2) (Suc_SO False bl M1 M2) = (if bl = bs2 ! M1
    then FBase (Suc_SO False (bs2 ! M2) M1 M2) else FBool False)"
| "lderiv0 (bs1, bs2) (Empty M) = (case bs2 ! M of
    True β‡’ FBool False
  | False β‡’ FBase (Empty M))"
| "lderiv0 (bs1, bs2) (Singleton M) = (case bs2 ! M of
    True β‡’ FBase (Empty M)
  | False β‡’ FBase (Singleton M))"
| "lderiv0 (bs1, bs2) (Subset M1 M2) = (case (bs2 ! M1, bs2 ! M2) of
    (True, False) β‡’ FBool False
  | _ β‡’ FBase (Subset M1 M2))"
| "lderiv0 (bs1, bs2) (In False m M) = (case (bs1 ! m, bs2 ! M) of
    (False, _) β‡’ FBase (In False m M)
  | (True, True) β‡’ FBool True
  | _ β‡’ FBool False)"
| "lderiv0 (bs1, bs2) (Eq_Max False m M) = (case (bs1 ! m, bs2 ! M) of
    (False, _) β‡’ FBase (Eq_Max False m M)
  | (True, True) β‡’ FBase (Empty M)
  | _ β‡’ FBool False)"
| "lderiv0 (bs1, bs2) (Eq_Min False m M) = (case (bs1 ! m, bs2 ! M) of
    (False, False) β‡’ FBase (Eq_Min False m M)
  | (True, True) β‡’ FBool True
  | _ β‡’ FBool False)"
| "lderiv0 (bs1, bs2) (Eq_Union M1 M2 M3) = (if bs2 ! M1 = (bs2 ! M2 ∨ bs2 ! M3)
   then FBase (Eq_Union M1 M2 M3) else FBool False)"
| "lderiv0 (bs1, bs2) (Eq_Inter M1 M2 M3) = (if bs2 ! M1 = (bs2 ! M2 ∧ bs2 ! M3)
   then FBase (Eq_Inter M1 M2 M3) else FBool False)"
| "lderiv0 (bs1, bs2) (Eq_Diff M1 M2 M3) = (if bs2 ! M1 = (bs2 ! M2 ∧ ¬ bs2 ! M3)
   then FBase (Eq_Diff M1 M2 M3) else FBool False)"
| "lderiv0 (bs1, bs2) (Disjoint M1 M2) =
  (if bs2 ! M1 ∧ bs2 ! M2 then FBool False else FBase (Disjoint M1 M2))"
| "lderiv0 (bs1, bs2) (Eq_Presb None M n) = (if bs2 ! M = (n mod 2 = 0)
   then FBool False else FBase (Eq_Presb None M (n div 2)))"
| "lderiv0 _ _ = undefined"

fun ld where
  "ld 0 = 0"
| "ld (Suc 0) = 0"
| "ld n = Suc (ld (n div 2))"

lemma ld_alt[simp]: "n > 0 ⟹ ld n = Max {i. 2 ^ i ≀ n}"
proof (safe intro!: Max_eqI[symmetric])
  assume "n > 0" then show "2 ^ ld n ≀ n" by (induct n rule: ld.induct) auto
next
  fix y
  assume "2 ^ y ≀ n"
  then show "y ≀ ld n"
  proof (induct n arbitrary: y rule: ld.induct)
    case (3 z)
    then have "y - 1 ≀ ld (Suc (Suc z) div 2)"
      by (cases y) simp_all
    then show ?case by simp
  qed (auto simp: le_eq_less_or_eq)
qed simp

fun rderiv0 where
  "rderiv0 (bs1, bs2) (Fo m) = (if bs1 ! m then FBool True else FBase (Fo m))"
| "rderiv0 (bs1, bs2) (Eq_Const i m n) = (case bs1 ! m of
    False β‡’ FBase (Eq_Const (case i of Some (Suc i) β‡’ Some i | _ β‡’ None) m n)
  | True β‡’ FBase (Eq_Const (Some n) m n))"
| "rderiv0 (bs1, bs2) (Less b m1 m2) = (case bs1 ! m2 of
    False β‡’ (case b of
      Some False β‡’ (case bs1 ! m1 of
        True β‡’ FBase (Less (Some True) m1 m2)
      | False β‡’ FBase (Less (Some False) m1 m2))
    | _ β‡’ FBase (Less b m1 m2))
  | True β‡’ FBase (Less (Some False) m1 m2))"
| "rderiv0 (bs1, bs2) (Plus_FO i m1 m2 n) = (if n = 0
  then
    (case (bs1 ! m1, bs1 ! m2) of
      (False, False) β‡’ FBase (Plus_FO i m1 m2 n)
    | (True, True) β‡’ FBase (Plus_FO (Some 0) m1 m2 n)
    | _ β‡’ FBase (Plus_FO None m1 m2 n))
  else
    (case bs1 ! m1 of
      True β‡’ FBase (Plus_FO (Some n) m1 m2 n)
    | False β‡’ (case bs1 ! m2 of
        False β‡’ (case i of
          Some (Suc (Suc i)) β‡’ FBase (Plus_FO (Some (Suc i)) m1 m2 n)
        | Some (Suc 0) β‡’ FBase (Plus_FO None m1 m2 n)
        | _ β‡’ FBase (Plus_FO i m1 m2 n))
      | True β‡’ (case i of
          Some (Suc i) β‡’ FBase (Plus_FO (Some i) m1 m2 n)
        | _ β‡’ FBase (Plus_FO None m1 m2 n)))))"
| "rderiv0 (bs1, bs2) (Eq_FO b m1 m2) = (case (bs1 ! m1, bs1 ! m2) of
    (False, False) β‡’ FBase (Eq_FO b m1 m2)
  | (True, True) β‡’ FBase (Eq_FO True m1 m2)
  | _ β‡’ FBase (Eq_FO False m1 m2))"
| "rderiv0 (bs1, bs2) (Eq_SO M1 M2) =
  (if bs2 ! M1 = bs2 ! M2 then FBase (Eq_SO M1 M2) else FBool False)"
| "rderiv0 (bs1, bs2) (Suc_SO br bl M1 M2) = (if br = bs2 ! M2
    then FBase (Suc_SO  (bs2 ! M1) bl M1 M2) else FBool False)"
| "rderiv0 (bs1, bs2) (Empty M) = (case bs2 ! M of
    True β‡’ FBool False
  | False β‡’ FBase (Empty M))"
| "rderiv0 (bs1, bs2) (Singleton M) = (case bs2 ! M of
    True β‡’ FBase (Empty M)
  | False β‡’ FBase (Singleton M))"
| "rderiv0 (bs1, bs2) (Subset M1 M2) = (case (bs2 ! M1, bs2 ! M2) of
    (True, False) β‡’ FBool False
  | _ β‡’ FBase (Subset M1 M2))"
| "rderiv0 (bs1, bs2) (In b m M) = (case (bs1 ! m, bs2 ! M) of
    (True, True) β‡’ FBase (In True m M)
  | (True, False) β‡’ FBase (In False m M)
  | _ β‡’ FBase (In b m M))"
| "rderiv0 (bs1, bs2) (Eq_Max b m M) =  (case (bs1 ! m, bs2 ! M) of
    (True, True) β‡’ if b then FBool False else FBase (Eq_Max True m M)
  | (True, False) β‡’ if b then FBool False else FBase (Eq_Max False m M)
  | (False, True) β‡’ if b then FBase (Eq_Max True m M) else FBool False
  | (False, False) β‡’ FBase (Eq_Max b m M))"
| "rderiv0 (bs1, bs2) (Eq_Min b m M) =  (case (bs1 ! m, bs2 ! M) of
    (True, True) β‡’ FBase (Eq_Min True m M)
  | (False, False) β‡’ FBase (Eq_Min b m M)
  | _ β‡’ FBase (Eq_Min False m M))"
| "rderiv0 (bs1, bs2) (Eq_Union M1 M2 M3) = (if bs2 ! M1 = (bs2 ! M2 ∨ bs2 ! M3)
   then FBase (Eq_Union M1 M2 M3) else FBool False)"
| "rderiv0 (bs1, bs2) (Eq_Inter M1 M2 M3) = (if bs2 ! M1 = (bs2 ! M2 ∧ bs2 ! M3)
   then FBase (Eq_Inter M1 M2 M3) else FBool False)"
| "rderiv0 (bs1, bs2) (Eq_Diff M1 M2 M3) = (if bs2 ! M1 = (bs2 ! M2 ∧ ¬ bs2 ! M3)
   then FBase (Eq_Diff M1 M2 M3) else FBool False)"
| "rderiv0 (bs1, bs2) (Disjoint M1 M2) =
  (if bs2 ! M1 ∧ bs2 ! M2 then FBool False else FBase (Disjoint M1 M2))"
| "rderiv0 (bs1, bs2) (Eq_Presb l M n) = (case l of
     None β‡’ if bs2 ! M then
         if n = 0 then FBool False
         else let l = ld n in FBase (Eq_Presb (Some l) M (n - 2 ^ l))
       else FBase (Eq_Presb l M n)
  | Some 0 β‡’ FBool False
  | Some (Suc l) β‡’ if bs2 ! M ∧ n β‰₯ 2 ^ l then FBase (Eq_Presb (Some l) M (n - 2 ^ l))
      else if ¬ bs2 ! M ∧ n < 2 ^ l then FBase (Eq_Presb (Some l) M n)
      else FBool False)"

primrec nullable0 where
  "nullable0 (Fo m) = False"
| "nullable0 (Eq_Const i m n) = (i = Some 0)"
| "nullable0 (Less b m1 m2) = (case b of None β‡’ False | Some b β‡’ b)"
| "nullable0 (Plus_FO i m1 m2 n) = (i = Some 0)"
| "nullable0 (Eq_FO b m1 m2) = b"
| "nullable0 (Eq_SO M1 M2) = True"
| "nullable0 (Suc_SO br bl M1 M2) = (bl = br)"
| "nullable0 (Empty M) = True"
| "nullable0 (Singleton M) = False"
| "nullable0 (Subset M1 M2) = True"
| "nullable0 (In b m M) = b"
| "nullable0 (Eq_Max b m M) = b"
| "nullable0 (Eq_Min b m M) = b"
| "nullable0 (Eq_Union M1 M2 M3) = True"
| "nullable0 (Eq_Inter M1 M2 M3) = True"
| "nullable0 (Eq_Diff M1 M2 M3) = True"
| "nullable0 (Disjoint M1 M2) = True"
| "nullable0 (Eq_Presb l M n) = (n = 0 ∧ (l = Some 0 ∨ l = None))"

definition "restrict ord P = (case ord of FO β‡’ P β‰  {||} | SO β‡’ True)"
definition "Restrict ord i = (case ord of FO β‡’ FBase (Fo i) | SO β‡’ FBool True)"

declare [[goals_limit = 50]]


global_interpretation WS1S: Formula SUC LESS assigns nvars Extend CONS SNOC Length
  extend size_atom zero Οƒ eval downshift upshift finsert cut len restrict Restrict
  lformula0 FV0 find0 wf0 decr0 satisfies0 nullable0 lderiv0 rderiv0 undefined
  defines norm = "Formula_Operations.norm find0 decr0"
  and nFOr = "Formula_Operations.nFOr :: formula β‡’ _"
  and nFAnd = "Formula_Operations.nFAnd :: formula β‡’ _"
  and nFNot = "Formula_Operations.nFNot find0 decr0 :: formula β‡’ _"
  and nFEx = "Formula_Operations.nFEx find0 decr0"
  and nFAll = "Formula_Operations.nFAll find0 decr0"
  and decr = "Formula_Operations.decr decr0 :: _ β‡’ _ β‡’ formula β‡’ _"
  and find = "Formula_Operations.find find0 :: _ β‡’ _ β‡’ formula β‡’ _"
  and FV = "Formula_Operations.FV FV0"
  and RESTR = "Formula_Operations.RESTR Restrict :: _ β‡’ formula"
  and RESTRICT = "Formula_Operations.RESTRICT Restrict FV0"
  and deriv = "Ξ»d0 (a :: atom) (Ο† :: formula). Formula_Operations.deriv extend d0 a Ο†"
  and nullable = "λφ :: formula. Formula_Operations.nullable nullable0 Ο†"
  and fut_default = "Formula.fut_default extend zero rderiv0"
  and fut = "Formula.fut extend zero find0 decr0 rderiv0"
  and finalize = "Formula.finalize SUC extend zero find0 decr0 rderiv0"
  and final = "Formula.final SUC extend zero find0 decr0
     nullable0 rderiv0 :: idx β‡’ formula β‡’ _"
  and ws1s_wf = "Formula_Operations.wf SUC (wf0 :: idx β‡’ ws1s β‡’ _)"
  and ws1s_lformula = "Formula_Operations.lformula lformula0 :: formula β‡’ _"
  and check_eqv = "Ξ»idx. DAs.check_eqv
    (Οƒ idx) (λφ. norm (RESTRICT Ο†) :: (ws1s, order) aformula)
    (Ξ»a Ο†. norm (deriv (lderiv0 :: _ β‡’ _ β‡’ formula) (a :: atom) Ο†))
    (final idx) (λφ :: formula. ws1s_wf idx Ο† ∧ ws1s_lformula Ο†)
    (Οƒ idx) (λφ. norm (RESTRICT Ο†) :: (ws1s, order) aformula)
    (Ξ»a Ο†. norm (deriv (lderiv0 :: _ β‡’ _ β‡’ formula) (a :: atom) Ο†))
    (final idx) (λφ :: formula. ws1s_wf idx Ο† ∧ ws1s_lformula Ο†) (=)"
  and bounded_check_eqv = "Ξ»idx. DAs.check_eqv
    (Οƒ idx) (λφ. norm (RESTRICT Ο†) :: (ws1s, order) aformula)
    (Ξ»a Ο†. norm (deriv (lderiv0 :: _ β‡’ _ β‡’ formula) (a :: atom) Ο†))
    nullable (λφ :: formula. ws1s_wf idx Ο† ∧ ws1s_lformula Ο†)
    (Οƒ idx) (λφ. norm (RESTRICT Ο†) :: (ws1s, order) aformula)
    (Ξ»a Ο†. norm (deriv (lderiv0 :: _ β‡’ _ β‡’ formula) (a :: atom) Ο†))
    nullable (λφ :: formula. ws1s_wf idx Ο† ∧ ws1s_lformula Ο†) (=)"
  and automaton = "DA.automaton
    (Ξ»a Ο†. norm (deriv lderiv0 (a :: atom) Ο† :: formula))"
proof
  fix k idx and a :: ws1s and l assume "wf0 (SUC k idx) a" "LESS k l (SUC k idx)" "Β¬ find0 k l a"
  then show "wf0 idx (decr0 k l a)"
    by (induct a) (unfold wf0.simps atomic.map find0.simps,
     (transfer, force simp: dec_def split!: if_splits order.splits)+)
next
  fix k and a :: ws1s and l assume "lformula0 a"
  then show "lformula0 (decr0 k l a)" by (induct a) auto
next
  fix i k and a :: ws1s and 𝔄 :: interp and P assume *: "Β¬ find0 k i a" "LESS k i (SUC k (#V 𝔄))"
    and disj: "lformula0 a ∨ len P ≀ Length 𝔄"
  from disj show "satisfies0 (Extend k i 𝔄 P) a = satisfies0 𝔄 (decr0 k i a)"
  proof
    assume "lformula0 a"
    then show ?thesis using *
      by (induct a rule: lformula0.induct)
        (auto simp: dec_def split: if_splits order.split option.splits bool.splits) ― β€Ήslowβ€Ί
  next
    note dec_def[simp]
    assume "len P ≀ Length 𝔄"
    with * show ?thesis
    proof (induct a)
      case Fo then show ?case by (cases k) auto
    next
      case Eq_Const then show ?case
        by (cases k) (auto simp: Let_def len_def split: if_splits option.splits)
    next
      case Less then show ?case by (cases k) auto
    next
      case Plus_FO then show ?case
        by (cases k) (auto simp: max_def len_def Let_def split: option.splits nat.splits)
    next
      case Eq_FO then show ?case by (cases k) auto
    next
      case Eq_SO then show ?case by (cases k) auto
    next
      case (Suc_SO br bl M1 M2) then show ?case
        by (cases k) (auto simp: max_def len_def)
    next
      case Empty then show ?case by (cases k) auto
    next
      case Singleton then show ?case by (cases k) auto
    next
      case Subset then show ?case by (cases k) auto
    next
      case In then show ?case by (cases k) auto
    qed (auto simp: len_def max_def split!: option.splits order.splits)
  qed
next
  fix idx and a :: ws1s and x assume "lformula0 a" "wf0 idx a"
  then show "Formula_Operations.wf SUC wf0 idx (lderiv0 x a)"
    by (induct a rule: lderiv0.induct)
      (auto simp: Formula_Operations.wf.simps Let_def split: bool.splits order.splits)
next
  fix a :: ws1s and x assume "lformula0 a"
  then show "Formula_Operations.lformula lformula0 (lderiv0 x a)"
    by (induct a rule: lderiv0.induct)
      (auto simp: Formula_Operations.lformula.simps split: bool.splits)
next
  fix idx and a :: ws1s and x assume "wf0 idx a"
  then show "Formula_Operations.wf SUC wf0 idx (rderiv0 x a)"
    by (induct a rule: lderiv0.induct)
      (auto simp: Formula_Operations.wf.simps Let_def sorted_append
        split: bool.splits order.splits nat.splits)
next
  fix 𝔄 :: interp and a :: ws1s
  note fmember.rep_eq[symmetric, simp]
  assume "Length 𝔄 = 0"
  then show "nullable0 a = satisfies0 𝔄 a"
    by (induct a, unfold wf0.simps nullable0.simps satisfies0.simps Let_def)
      (transfer, (auto 0 3 dest: MSB_greater split: prod.splits if_splits option.splits bool.splits nat.splits) [])+  ― β€Ήslowβ€Ί
next
   note Formula_Operations.satisfies_gen.simps[simp] Let_def[simp] upshift_def[simp]
   fix x :: atom and a :: ws1s and 𝔄 :: interp
   assume "lformula0 a" "wf0 (#V 𝔄) a" "#V 𝔄 = size_atom x"
   then show "Formula_Operations.satisfies Extend Length satisfies0 𝔄 (lderiv0 x a) =
     satisfies0 (CONS x 𝔄) a"
   proof (induct a)
     case 18
     then show ?case
       apply (auto simp: sum_pow2_image_Suc sum_pow2_insert0 image_iff split: prod.splits)
       apply presburger+
       done
   qed (auto split: prod.splits bool.splits)
next
   note Formula_Operations.satisfies_gen.simps[simp] Let_def[simp] upshift_def[simp]
   fix x :: atom and a :: ws1s and 𝔄 :: interp
   assume "lformula0 a" "wf0 (#V 𝔄) a" "#V 𝔄 = size_atom x"
   then show "Formula_Operations.satisfies_bounded Extend Length len satisfies0 𝔄 (lderiv0 x a) =
     satisfies0 (CONS x 𝔄) a"
   proof (induct a)
     case 18
     then show ?case
       apply (auto simp: sum_pow2_image_Suc sum_pow2_insert0 image_iff split: prod.splits)
       apply presburger+
       done
   qed (auto split: prod.splits bool.splits)
next
   note Formula_Operations.satisfies_gen.simps[simp] Let_def[simp]
   fix x :: atom and a :: ws1s and 𝔄 :: interp
   assume "wf0 (#V 𝔄) a" "#V 𝔄 = size_atom x"
   then show "Formula_Operations.satisfies_bounded Extend Length len satisfies0 𝔄 (rderiv0 x a) =
     satisfies0 (SNOC x 𝔄) a"
   proof (induct a)
     case Eq_Const then show ?case by (auto split: prod.splits option.splits nat.splits)
   next
     case Less then show ?case
       by (auto split: prod.splits option.splits bool.splits) (metis fMin_less_Length less_not_sym)+
   next
     case (Plus_FO i m1 m2 n) then show ?case
       by (auto simp: min.commute dest: fMin_less_Length
          split: prod.splits option.splits nat.splits bool.splits)
   next
     case Eq_FO then show ?case
       by (auto split: prod.splits option.splits bool.splits) (metis fMin_less_Length less_not_sym)+
   next
     case Eq_SO then show ?case
       by (auto split: prod.splits option.splits bool.splits)
         (metis assigns_less_Length finsertI1 less_not_refl)+
   next
     case Suc_SO then show ?case
     apply (auto 2 1 split: prod.splits)
                       apply (metis finsert_iff gr0_implies_Suc in_fimage_Suc nat.distinct(2))
                      apply (metis finsert_iff in_fimage_Suc less_not_refl)
                     apply (metis (no_types, hide_lams) fimage_finsert finsertE finsertI1 finsert_commute in_fimage_Suc n_not_Suc_n)
                    apply (metis (no_types, hide_lams) assigns_less_Length order.strict_iff_order finsert_iff in_fimage_Suc not_less_eq_eq order_refl)
                   apply (metis assigns_less_Length fimageI finsert_iff less_irrefl_nat nat.inject)
                  apply (metis finsertE finsertI1 finsert_commute finsert_fminus_single in_fimage_Suc n_not_Suc_n)
                 apply (metis (no_types, hide_lams) assigns_less_Length finsertE fminus_finsert2 fminus_iff in_fimage_Suc lessI not_less_iff_gr_or_eq)
                apply (metis assigns_less_Length finsert_iff lessI not_less_iff_gr_or_eq)
               apply (metis assigns_less_Length fimage_finsert finsert_iff not_less_eq not_less_iff_gr_or_eq)
              apply metis
             apply (metis assigns_less_Length order.strict_iff_order finsert_iff in_fimage_Suc not_less_eq_eq order_refl)
            apply (metis Suc_leI assigns_less_Length fimageI finsert_iff le_eq_less_or_eq lessI less_imp_not_less)
           apply (metis assigns_less_Length fimageE finsertI1 finsert_fminus_if fminus_finsert_absorb lessI less_not_sym)
          apply (metis assigns_less_Length order.strict_iff_order finsert_iff not_less_eq_eq order_refl)
         apply (metis assigns_less_Length order.strict_iff_order finsert_iff not_less_eq_eq order_refl)
        apply (metis assigns_less_Length fimage_Suc_inj fimage_finsert finsert_absorb finsert_iff less_not_refl nat.distinct(2))
       apply (metis assigns_less_Length fimage_Suc_inj fimage_finsert finsertI1 finsert_absorb less_not_refl)
      apply (metis assigns_less_Length fimage_Suc_inj fimage_finsert finsert_absorb finsert_iff less_not_refl nat.distinct(2))
     apply (metis assigns_less_Length fimage_Suc_inj fimage_finsert finsertI1 finsert_absorb2 less_not_refl)
     done
   next
     case In then show ?case by (auto split: prod.splits) (metis fMin_less_Length less_not_sym)+
   next
     case (Eq_Max b m M) then show ?case
       by (auto split: prod.splits bool.splits)
         (metis fMax_less_Length less_not_sym, (metis fMin_less_Length less_not_sym)+)
   next
     case Eq_Min then show ?case
      by (auto split: prod.splits bool.splits) (metis fMin_less_Length less_not_sym)+
   next
     case Eq_Union then show ?case
       by (auto 0 0 simp add: fset_eq_iff split: prod.splits) (metis assigns_less_Length less_not_refl)+
   next
     case Eq_Inter then show ?case
       by (auto 0 0 simp add: fset_eq_iff split: prod.splits) (metis assigns_less_Length less_not_refl)+
   next
     case Eq_Diff then show ?case
       by (auto 0 1 simp add: fset_eq_iff split: prod.splits) (metis assigns_less_Length less_not_refl)+
   next
     let ?f = "sum ((^) (2 :: nat))"
     note fmember.rep_eq[symmetric, simp]
     case (Eq_Presb l M n)
     moreover
     let ?M = "fset (M𝔄SO)" and ?L = "Length 𝔄"
     have "?f (insert ?L ?M) = 2 ^ ?L + ?f ?M"
       by (subst sum.insert) auto
     moreover have "n > 0 ⟹ 2 ^ Max {i. 2 ^ i ≀ n} ≀ n"
       using Max_in[of "{i. 2 ^ i ≀ n}", simplified, OF exI[of _ 0]] by auto
     moreover
     { have "?f ?M ≀ ?f {0 ..< ?L}" by (rule sum_mono2) auto
       also have "… = 2 ^ ?L - 1" by (rule sum_pow2_upto)
       also have "… < 2 ^ ?L" by simp
       finally have "?f ?M < 2 ^ ?L" .
     }
     moreover have "Max {i. 2 ^ i ≀ 2 ^ ?L + ?f ?M} = ?L"
     proof (intro Max_eqI, safe)
       fix y assume "2 ^ y ≀ 2 ^ ?L + ?f ?M"
       { assume "?L < y"
         then have "(2 :: nat) ^ ?L + 2 ^ ?L ≀ 2 ^ y"
           by (cases y) (auto simp: less_Suc_eq_le numeral_eq_Suc add_le_mono)
         also note β€Ή2 ^ y ≀ 2 ^ ?L + ?f ?Mβ€Ί
         finally have " 2 ^ ?L ≀ ?f ?M" by simp
         with β€Ή?f ?M < 2 ^ ?Lβ€Ί have False by auto
       } then show "y ≀ ?L" by (intro leI) blast
     qed auto
     ultimately show ?case by (auto split: prod.splits option.splits nat.splits)
   qed (auto split: prod.splits)
next
   fix a :: ws1s and 𝔄 𝔅 :: interp
   assume "wf0 (#V 𝔅) a" "#V 𝔄 = #V 𝔅" "(β‹€m k. LESS k m (#V 𝔅) ⟹ m𝔄k = m𝔅k)" "lformula0 a"
   then show "satisfies0 𝔄 a ⟷ satisfies0 𝔅 a" by (induct a) auto
next
   fix a :: ws1s
   assume "lformula0 a"
   moreover
   define d where "d = Formula_Operations.deriv extend lderiv0"
   define Ξ¦ :: "_ β‡’ (ws1s, order) aformula set"
     where "Ξ¦ a =
       (case a of
         Fo m β‡’ {FBase (Fo m), FBool True}
       | Eq_Const None m n β‡’ {FBase (Eq_Const None m i) | i . i ≀ n} βˆͺ {FBool True, FBool False}
       | Less None m1 m2 β‡’ {FBase (Less None m1 m2), FBase (Fo m2), FBool True, FBool False}
       | Plus_FO None m1 m2 n β‡’ {FBase (Eq_Const None m1 i) | i . i ≀ n} βˆͺ
          {FBase (Plus_FO None m1 m2 n), FBool True, FBool False}
       | Eq_FO False m1 m2 β‡’ {FBase (Eq_FO False m1 m2), FBool True, FBool False}
       | Eq_SO M1 M2 β‡’ {FBase (Eq_SO M1 M2), FBool False}
       | Suc_SO False bl M1 M2 β‡’ {FBase (Suc_SO False True M1 M2), FBase (Suc_SO False False M1 M2),
           FBool False}
       | Empty M β‡’ {FBase (Empty M), FBool False}
       | Singleton M β‡’ {FBase (Singleton M), FBase (Empty M), FBool False}
       | Subset M1 M2 β‡’ {FBase (Subset M1 M2), FBool False}
       | In False i I β‡’ {FBase (In False i I), FBool True, FBool False}
       | Eq_Max False m M β‡’ {FBase (Eq_Max False m M), FBase (Empty M), FBool False}
       | Eq_Min False m M β‡’ {FBase (Eq_Min False m M), FBool True, FBool False}
       | Eq_Union M1 M2 M3 β‡’ {FBase (Eq_Union M1 M2 M3), FBool False}
       | Eq_Inter M1 M2 M3 β‡’ {FBase (Eq_Inter M1 M2 M3), FBool False}
       | Eq_Diff M1 M2 M3 β‡’ {FBase (Eq_Diff M1 M2 M3), FBool False}
       | Disjoint M1 M2 β‡’ {FBase (Disjoint M1 M2), FBool False}
       | Eq_Presb None M n β‡’ {FBase (Eq_Presb None M i) | i . i ≀ n} βˆͺ {FBool False}
       | _ β‡’ {})" for a
   { fix xs
     note Formula_Operations.fold_deriv_FBool[simp] Formula_Operations.deriv.simps[simp] Ξ¦_def[simp]
     from β€Ήlformula0 aβ€Ί have "FBase a ∈ Ξ¦ a" by auto
     moreover have "β‹€x Ο†. Ο† ∈ Ξ¦ a ⟹ d x Ο† ∈ Ξ¦ a"
       by (auto simp: d_def split: atomic.splits list.splits bool.splits if_splits option.splits)
     then have "β‹€Ο†. Ο† ∈ Ξ¦ a ⟹ fold d xs Ο† ∈ Ξ¦ a" by (induct xs) auto
     ultimately have "fold d xs (FBase a) ∈ Φ a" by blast
   }
   moreover have "finite (Ξ¦ a)" using β€Ήlformula0 aβ€Ί unfolding Ξ¦_def by (auto split: atomic.splits)
   ultimately show "finite {fold d xs (FBase a) | xs. True}" by (blast intro: finite_subset)
next
   fix a :: ws1s
   define d where "d = Formula_Operations.deriv extend rderiv0"
   define Ξ¦ :: "_ β‡’ (ws1s, order) aformula set"
     where "Ξ¦ a =
       (case a of
         Fo m β‡’ {FBase (Fo m), FBool True}
       | Eq_Const i m n β‡’
          {FBase (Eq_Const (Some j) m n) | j . j ≀ (case i of Some i β‡’ max i n | _ β‡’ n)} βˆͺ
          {FBase (Eq_Const None m n)}
       | Less b m1 m2 β‡’ {FBase (Less None m1 m2), FBase (Less (Some True) m1 m2),
          FBase (Less (Some False) m1 m2)}
       | Plus_FO i m1 m2 n β‡’ 
          {FBase (Plus_FO (Some j) m1 m2 n) | j . j ≀ (case i of Some i β‡’ max i n | _ β‡’ n)} βˆͺ
          {FBase (Plus_FO None m1 m2 n)}
       | Eq_FO b m1 m2 β‡’ {FBase (Eq_FO True m1 m2), FBase (Eq_FO False m1 m2)}
       | Eq_SO M1 M2 β‡’ {FBase (Eq_SO M1 M2), FBool False}
       | Suc_SO br bl M1 M2 β‡’ {FBase (Suc_SO False True M1 M2), FBase (Suc_SO False False M1 M2),
           FBase (Suc_SO True True M1 M2), FBase (Suc_SO True False M1 M2), FBool False}
       | Empty M β‡’ {FBase (Empty M), FBool False}
       | Singleton M β‡’ {FBase (Singleton M), FBase (Empty M), FBool False}
       | Subset M1 M2 β‡’ {FBase (Subset M1 M2), FBool False}
       | In b i I β‡’ {FBase (In True i I), FBase (In False i I)}
       | Eq_Max b m M β‡’ {FBase (Eq_Max False m M), FBase (Eq_Max True m M), FBool False}
       | Eq_Min b m M β‡’ {FBase (Eq_Min False m M), FBase (Eq_Min True m M)}
       | Eq_Union M1 M2 M3 β‡’ {FBase (Eq_Union M1 M2 M3), FBool False}
       | Eq_Inter M1 M2 M3 β‡’ {FBase (Eq_Inter M1 M2 M3), FBool False}
       | Eq_Diff M1 M2 M3 β‡’ {FBase (Eq_Diff M1 M2 M3), FBool False}
       | Disjoint M1 M2 β‡’ {FBase (Disjoint M1 M2), FBool False}
       | Eq_Presb i M n β‡’ {FBase (Eq_Presb (Some l) M j) | j l .
           j ≀ (case i of Some i β‡’ max i n | _ β‡’ n) ∧ l ≀ (case i of Some i β‡’ max i n | _ β‡’ n)} βˆͺ
           {FBase (Eq_Presb None M n), FBool False})" for a
   { fix xs
     note Formula_Operations.fold_deriv_FBool[simp] Formula_Operations.deriv.simps[simp] Ξ¦_def[simp]
     then have "FBase a ∈ Φ a" by (auto split: atomic.splits option.splits)
     moreover have "β‹€x Ο†. Ο† ∈ Ξ¦ a ⟹ d x Ο† ∈ Ξ¦ a"
       by (auto simp add: d_def Let_def not_le gr0_conv_Suc leD[OF ld_bounded]
         split: atomic.splits list.splits bool.splits if_splits option.splits nat.splits)
     then have "β‹€Ο†. Ο† ∈ Ξ¦ a ⟹ fold d xs Ο† ∈ Ξ¦ a"
       by (induct xs) auto
     ultimately have "fold d xs (FBase a) ∈ Φ a" by blast
   }
   moreover have "finite (Ξ¦ a)" unfolding Ξ¦_def using [[simproc add: finite_Collect]]
     by (auto split: atomic.splits)
   ultimately show "finite {fold d xs (FBase a) | xs. True}" by (blast intro: finite_subset)
next
  fix k l and a :: ws1s
  show "find0 k l a ⟷ l ∈ FV0 k a" by (induct a rule: find0.induct) auto
next
  fix a :: ws1s and k :: order
  show "finite (FV0 k a)" by (cases k) (induct a, auto)+
next
  fix idx a k v
  assume "wf0 idx a" "v ∈ FV0 k a"
  then show "LESS k v idx" by (cases k) (induct a, auto)+
next
  fix idx k i
  assume "LESS k i idx"
  then show "Formula_Operations.wf SUC wf0 idx (Restrict k i)"
     unfolding Restrict_def by (cases k) (auto simp: Formula_Operations.wf.simps)
next
  fix k and i :: nat
  show "Formula_Operations.lformula lformula0 (Restrict k i)"
    unfolding Restrict_def by (cases k) (auto simp: Formula_Operations.lformula.simps)
next
  fix i 𝔄 k P r
  assume "i𝔄k = P"
  then show "restrict k P ⟷
    Formula_Operations.satisfies_gen Extend Length satisfies0 r 𝔄 (Restrict k i)"
    unfolding restrict_def Restrict_def
    by (cases k) (auto simp: Formula_Operations.satisfies_gen.simps)
qed (auto simp: Extend_commute_unsafe downshift_def upshift_def fimage_iff Suc_le_eq len_def
  dec_def eval_def cut_def len_downshift_helper dest!: CONS_surj
  dest: fMax_ge fMax_ffilter_less fMax_boundedD fsubset_fsingletonD
  split!: order.splits if_splits)

(*Workaround for code generation*)
lemma check_eqv_code[code]: "check_eqv idx r s =
  ((ws1s_wf idx r ∧ ws1s_lformula r) ∧ (ws1s_wf idx s ∧ ws1s_lformula s) ∧
  (case rtrancl_while (Ξ»(p, q). final idx p = final idx q)
    (Ξ»(p, q). map (Ξ»a. (norm (deriv lderiv0 a p), norm (deriv lderiv0 a q))) (Οƒ idx))
    (norm (RESTRICT r), norm (RESTRICT s)) of
    None β‡’ False
  | Some ([], x) β‡’ True
  | Some (a # list, x) β‡’ False))"
  unfolding check_eqv_def WS1S.check_eqv_def WS1S.step_alt ..

definition while where [code del, code_abbrev]: "while idx Ο† = while_default (fut_default idx Ο†)"
declare while_default_code[of "fut_default idx Ο†" for idx Ο†, folded while_def, code]

lemma check_eqv_sound: 
  "⟦#V 𝔄 = idx; check_eqv idx Ο† ψ⟧ ⟹ (WS1S.sat 𝔄 Ο† ⟷ WS1S.sat 𝔄 ψ)"
  unfolding check_eqv_def by (rule WS1S.check_eqv_soundness)

lemma bounded_check_eqv_sound:
  "⟦#V 𝔄 = idx; bounded_check_eqv idx Ο† ψ⟧ ⟹ (WS1S.satb 𝔄 Ο† ⟷ WS1S.satb 𝔄 ψ)"
  unfolding bounded_check_eqv_def by (rule WS1S.bounded_check_eqv_soundness)

method_setup check_equiv = β€Ή
  let
    fun tac ctxt =
      let
        val conv = @{computation_check terms: Trueprop
          "0 :: nat" "1 :: nat" "2 :: nat" "3 :: nat" Suc
          "plus :: nat β‡’ _" "minus :: nat β‡’ _"
          "times :: nat β‡’ _" "divide :: nat β‡’ _" "modulo :: nat β‡’ _"
          "0 :: int" "1 :: int" "2 :: int" "3 :: int" "-1 :: int"
          check_eqv datatypes: formula "int list" integer idx
         "nat Γ— nat" "nat option" "bool option"} ctxt
      in
        CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
        resolve_tac ctxt [TrueI]
      end
  in
    Scan.succeed (SIMPLE_METHOD' o tac)
  end
β€Ί

end

Theory WS1S_Alt_Formula

section β€ΉConcrete Atomic WS1S Formulas (Singleton Semantics for FO Variables)β€Ί

(*<*)
theory WS1S_Alt_Formula
imports
  Abstract_Formula
  WS1S_Prelim
begin
(*>*)

datatype (FOV0: 'fo, SOV0: 'so) atomic =
  Fo 'fo |
  Z 'fo |
  Less 'fo 'fo |
  In 'fo 'so

derive linorder atomic

type_synonym fo = nat
type_synonym so = nat
type_synonym ws1s = "(fo, so) atomic"
type_synonym formula = "(ws1s, order) aformula"

primrec wf0 where
  "wf0 idx (Fo m) = LESS FO m idx"
| "wf0 idx (Z m) = LESS FO m idx"
| "wf0