Theory Ailamazyan

theory Ailamazyan
  imports Eval_FO Cluster Mapping_Code
begin

fun SP :: "('a, 'b) fo_fmla ⇒ nat set" where
  "SP (Eqa (Var n) (Var n')) = (if n ≠ n' then {n, n'} else {})"
| "SP (Neg φ) = SP φ"
| "SP (Conj φ ψ) = SP φ ∪ SP ψ"
| "SP (Disj φ ψ) = SP φ ∪ SP ψ"
| "SP (Exists n φ) = SP φ - {n}"
| "SP (Forall n φ) = SP φ - {n}"
| "SP _ = {}"

lemma SP_fv: "SP φ ⊆ fv_fo_fmla φ"
  by (induction φ rule: SP.induct) auto

lemma finite_SP: "finite (SP φ)"
  using SP_fv finite_fv_fo_fmla finite_subset by fastforce

fun SP_list_rec :: "('a, 'b) fo_fmla ⇒ nat list" where
  "SP_list_rec (Eqa (Var n) (Var n')) = (if n ≠ n' then [n, n'] else [])"
| "SP_list_rec (Neg φ) = SP_list_rec φ"
| "SP_list_rec (Conj φ ψ) = SP_list_rec φ @ SP_list_rec ψ"
| "SP_list_rec (Disj φ ψ) = SP_list_rec φ @ SP_list_rec ψ"
| "SP_list_rec (Exists n φ) = filter (λm. n ≠ m) (SP_list_rec φ)"
| "SP_list_rec (Forall n φ) = filter (λm. n ≠ m) (SP_list_rec φ)"
| "SP_list_rec _ = []"

definition SP_list :: "('a, 'b) fo_fmla ⇒ nat list" where
  "SP_list φ = remdups_adj (sort (SP_list_rec φ))"

lemma SP_list_set: "set (SP_list φ) = SP φ"
  unfolding SP_list_def
  by (induction φ rule: SP.induct) (auto simp: fv_fo_terms_set_list)

lemma sorted_distinct_SP_list: "sorted_distinct (SP_list φ)"
  unfolding SP_list_def
  by (auto intro: distinct_remdups_adj_sort)

fun d :: "('a, 'b) fo_fmla ⇒ nat" where
  "d (Eqa (Var n) (Var n')) = (if n ≠ n' then 2 else 1)"
| "d (Neg φ) = d φ"
| "d (Conj φ ψ) = max (d φ) (max (d ψ) (card (SP (Conj φ ψ))))"
| "d (Disj φ ψ) = max (d φ) (max (d ψ) (card (SP (Disj φ ψ))))"
| "d (Exists n φ) = d φ"
| "d (Forall n φ) = d φ"
| "d _ = 1"

lemma d_pos: "1 ≤ d φ"
  by (induction φ rule: d.induct) auto

lemma card_SP_d: "card (SP φ) ≤ d φ"
  using dual_order.trans
  by (induction φ rule: SP.induct) (fastforce simp: card_Diff1_le finite_SP)+

fun eval_eterm :: "('a + 'c) val ⇒ 'a fo_term ⇒ 'a + 'c" (infix "⋅e" 60) where
  "eval_eterm σ (Const c) = Inl c"
| "eval_eterm σ (Var n) = σ n"

definition eval_eterms :: "('a + 'c) val ⇒ ('a fo_term) list ⇒
  ('a + 'c) list" (infix "⊙e" 60) where
  "eval_eterms σ ts = map (eval_eterm σ) ts"

lemma eval_eterm_cong: "(⋀n. n ∈ fv_fo_term_set t ⟹ σ n = σ' n) ⟹
  eval_eterm σ t = eval_eterm σ' t"
  by (cases t) auto

lemma eval_eterms_fv_fo_terms_set: "σ ⊙e ts = σ' ⊙e ts ⟹ n ∈ fv_fo_terms_set ts ⟹ σ n = σ' n"
proof (induction ts)
  case (Cons t ts)
  then show ?case
    by (cases t) (auto simp: eval_eterms_def fv_fo_terms_set_def)
qed (auto simp: eval_eterms_def fv_fo_terms_set_def)

lemma eval_eterms_cong: "(⋀n. n ∈ fv_fo_terms_set ts ⟹ σ n = σ' n) ⟹
  eval_eterms σ ts = eval_eterms σ' ts"
  by (auto simp: eval_eterms_def fv_fo_terms_set_def intro: eval_eterm_cong)

lemma eval_terms_eterms: "map Inl (σ ⊙ ts) = (Inl ∘ σ) ⊙e ts"
proof (induction ts)
  case (Cons t ts)
  then show ?case
    by (cases t) (auto simp: eval_terms_def eval_eterms_def)
qed (auto simp: eval_terms_def eval_eterms_def)

fun ad_equiv_pair :: "'a set ⇒ ('a + 'c) × ('a + 'c) ⇒ bool" where
  "ad_equiv_pair X (a, a') ⟷ (a ∈ Inl ` X ⟶ a = a') ∧ (a' ∈ Inl ` X ⟶ a = a')"

fun sp_equiv_pair :: "'a × 'b ⇒ 'a × 'b ⇒ bool" where
  "sp_equiv_pair (a, b) (a', b') ⟷ (a = a' ⟷ b = b')"

definition ad_equiv_list :: "'a set ⇒ ('a + 'c) list ⇒ ('a + 'c) list ⇒ bool" where
  "ad_equiv_list X xs ys ⟷ length xs = length ys ∧ (∀x ∈ set (zip xs ys). ad_equiv_pair X x)"

definition sp_equiv_list :: "('a + 'c) list ⇒ ('a + 'c) list ⇒ bool" where
  "sp_equiv_list xs ys ⟷ length xs = length ys ∧ pairwise sp_equiv_pair (set (zip xs ys))"

definition ad_agr_list :: "'a set ⇒ ('a + 'c) list ⇒ ('a + 'c) list ⇒ bool" where
  "ad_agr_list X xs ys ⟷ length xs = length ys ∧ ad_equiv_list X xs ys ∧ sp_equiv_list xs ys"

lemma ad_equiv_pair_refl[simp]: "ad_equiv_pair X (a, a)"
  by auto

declare ad_equiv_pair.simps[simp del]

lemma ad_equiv_pair_comm: "ad_equiv_pair X (a, a') ⟷ ad_equiv_pair X (a', a)"
  by (auto simp: ad_equiv_pair.simps)

lemma ad_equiv_pair_mono: "X ⊆ Y ⟹ ad_equiv_pair Y (a, a') ⟹ ad_equiv_pair X (a, a')"
  unfolding ad_equiv_pair.simps
  by fastforce

lemma sp_equiv_pair_comm: "sp_equiv_pair x y ⟷ sp_equiv_pair y x"
  by (cases x; cases y) auto

definition sp_equiv :: "('a + 'c) val ⇒ ('a + 'c) val ⇒ nat set ⇒ bool" where
  "sp_equiv σ τ I ⟷ pairwise sp_equiv_pair ((λn. (σ n, τ n)) ` I)"

lemma sp_equiv_mono: "I ⊆ J ⟹ sp_equiv σ τ J ⟹ sp_equiv σ τ I"
  by (auto simp: sp_equiv_def pairwise_def)

definition ad_agr_sets :: "nat set ⇒ nat set ⇒ 'a set ⇒ ('a + 'c) val ⇒
  ('a + 'c) val ⇒ bool" where
  "ad_agr_sets FV S X σ τ ⟷ (∀i ∈ FV. ad_equiv_pair X (σ i, τ i)) ∧ sp_equiv σ τ S"

lemma ad_agr_sets_comm: "ad_agr_sets FV S X σ τ ⟹ ad_agr_sets FV S X τ σ"
  unfolding ad_agr_sets_def sp_equiv_def pairwise_def
  by (subst ad_equiv_pair_comm) auto

lemma ad_agr_sets_mono: "X ⊆ Y ⟹ ad_agr_sets FV S Y σ τ ⟹ ad_agr_sets FV S X σ τ"
  using ad_equiv_pair_mono
  by (fastforce simp: ad_agr_sets_def)

lemma ad_agr_sets_mono': "S ⊆ S' ⟹ ad_agr_sets FV S' X σ τ ⟹ ad_agr_sets FV S X σ τ"
  by (auto simp: ad_agr_sets_def sp_equiv_def pairwise_def)

lemma ad_equiv_list_comm: "ad_equiv_list X xs ys ⟹ ad_equiv_list X ys xs"
  by (auto simp: ad_equiv_list_def) (smt (verit, del_insts) ad_equiv_pair_comm in_set_zip prod.sel(1) prod.sel(2))

lemma ad_equiv_list_mono: "X ⊆ Y ⟹ ad_equiv_list Y xs ys ⟹ ad_equiv_list X xs ys"
  using ad_equiv_pair_mono
  by (fastforce simp: ad_equiv_list_def)

lemma ad_equiv_list_trans:
  assumes "ad_equiv_list X xs ys" "ad_equiv_list X ys zs"
  shows "ad_equiv_list X xs zs"
proof -
  have lens: "length xs = length ys" "length xs = length zs" "length ys = length zs"
    using assms
    by (auto simp: ad_equiv_list_def)
  have "⋀x z. (x, z) ∈ set (zip xs zs) ⟹ ad_equiv_pair X (x, z)"
  proof -
    fix x z
    assume "(x, z) ∈ set (zip xs zs)"
    then obtain i where i_def: "i < length xs" "xs ! i = x" "zs ! i = z"
      by (auto simp: set_zip)
    define y where "y = ys ! i"
    have "ad_equiv_pair X (x, y)" "ad_equiv_pair X (y, z)"
      using assms lens i_def
      by (fastforce simp: set_zip y_def ad_equiv_list_def)+
    then show "ad_equiv_pair X (x, z)"
      unfolding ad_equiv_pair.simps
      by blast
  qed
  then show ?thesis
    using assms
    by (auto simp: ad_equiv_list_def)
qed

lemma ad_equiv_list_link: "(∀i ∈ set ns. ad_equiv_pair X (σ i, τ i)) ⟷
  ad_equiv_list X (map σ ns) (map τ ns)"
  by (auto simp: ad_equiv_list_def set_zip) (metis in_set_conv_nth nth_map)

lemma set_zip_comm: "(x, y) ∈ set (zip xs ys) ⟹ (y, x) ∈ set (zip ys xs)"
  by (metis in_set_zip prod.sel(1) prod.sel(2))

lemma set_zip_map: "set (zip (map σ ns) (map τ ns)) = (λn. (σ n, τ n)) ` set ns"
  by (induction ns) auto

lemma sp_equiv_list_comm: "sp_equiv_list xs ys ⟹ sp_equiv_list ys xs"
  unfolding sp_equiv_list_def
  using set_zip_comm
  by (auto simp: pairwise_def) force+

lemma sp_equiv_list_trans:
  assumes "sp_equiv_list xs ys" "sp_equiv_list ys zs"
  shows "sp_equiv_list xs zs"
proof -
  have lens: "length xs = length ys" "length xs = length zs" "length ys = length zs"
    using assms
    by (auto simp: sp_equiv_list_def)
  have "pairwise sp_equiv_pair (set (zip xs zs))"
  proof (rule pairwiseI)
    fix xz xz'
    assume "xz ∈ set (zip xs zs)" "xz' ∈ set (zip xs zs)"
    then obtain x z i x' z' i' where xz_def: "i < length xs" "xs ! i = x" "zs ! i = z"
      "xz = (x, z)" "i' < length xs" "xs ! i' = x'" "zs ! i' = z'" "xz' = (x', z')"
      by (auto simp: set_zip)
    define y where "y = ys ! i"
    define y' where "y' = ys ! i'"
    have "sp_equiv_pair (x, y) (x', y')" "sp_equiv_pair (y, z) (y', z')"
      using assms lens xz_def
      by (auto simp: sp_equiv_list_def pairwise_def y_def y'_def set_zip) metis+
    then show "sp_equiv_pair xz xz'"
      by (auto simp: xz_def)
  qed
  then show ?thesis
    using assms
    by (auto simp: sp_equiv_list_def)
qed

lemma sp_equiv_list_link: "sp_equiv_list (map σ ns) (map τ ns) ⟷ sp_equiv σ τ (set ns)"
  apply (auto simp: sp_equiv_list_def sp_equiv_def pairwise_def set_zip in_set_conv_nth)
     apply (metis nth_map)
    apply (metis nth_map)
   apply fastforce+
  done

lemma ad_agr_list_comm: "ad_agr_list X xs ys ⟹ ad_agr_list X ys xs"
  using ad_equiv_list_comm sp_equiv_list_comm
  by (fastforce simp: ad_agr_list_def)

lemma ad_agr_list_mono: "X ⊆ Y ⟹ ad_agr_list Y ys xs ⟹ ad_agr_list X ys xs"
  using ad_equiv_list_mono
  by (force simp: ad_agr_list_def)

lemma ad_agr_list_rev_mono:
  assumes "Y ⊆ X" "ad_agr_list Y ys xs" "Inl -` set xs ⊆ Y" "Inl -` set ys ⊆ Y"
  shows "ad_agr_list X ys xs"
proof -
  have "(a, b) ∈ set (zip ys xs) ⟹ ad_equiv_pair Y (a, b) ⟹ ad_equiv_pair X (a, b)" for a b
    using assms
    apply (cases a; cases b)
       apply (auto simp: ad_agr_list_def ad_equiv_list_def vimage_def set_zip)
    unfolding ad_equiv_pair.simps
       apply (metis Collect_mem_eq Collect_mono_iff imageI nth_mem)
      apply (metis Collect_mem_eq Collect_mono_iff imageI nth_mem)
     apply (metis Collect_mem_eq Collect_mono_iff imageI nth_mem)
    apply (metis Inl_Inr_False image_iff)
    done
  then show ?thesis
    using assms
    by (fastforce simp: ad_agr_list_def ad_equiv_list_def)
qed

lemma ad_agr_list_trans: "ad_agr_list X xs ys ⟹ ad_agr_list X ys zs ⟹ ad_agr_list X xs zs"
  using ad_equiv_list_trans sp_equiv_list_trans
  by (force simp: ad_agr_list_def)

lemma ad_agr_list_refl: "ad_agr_list X xs xs"
  by (auto simp: ad_agr_list_def ad_equiv_list_def set_zip ad_equiv_pair.simps
      sp_equiv_list_def pairwise_def)

lemma ad_agr_list_set: "ad_agr_list X xs ys ⟹ y ∈ X ⟹ Inl y ∈ set ys ⟹ Inl y ∈ set xs"
  by (auto simp: ad_agr_list_def ad_equiv_list_def set_zip in_set_conv_nth)
     (metis ad_equiv_pair.simps image_eqI)

lemma ad_agr_list_length: "ad_agr_list X xs ys ⟹ length xs = length ys"
  by (auto simp: ad_agr_list_def)

lemma ad_agr_list_eq: "set ys ⊆ AD ⟹ ad_agr_list AD (map Inl xs) (map Inl ys) ⟹ xs = ys"
  by (fastforce simp: ad_agr_list_def ad_equiv_list_def set_zip ad_equiv_pair.simps
      intro!: nth_equalityI)

lemma sp_equiv_list_subset:
  assumes "set ms ⊆ set ns" "sp_equiv_list (map σ ns) (map σ' ns)"
  shows "sp_equiv_list (map σ ms) (map σ' ms)"
  unfolding sp_equiv_list_def length_map pairwise_def
proof (rule conjI, rule refl, (rule ballI)+, rule impI)
  fix x y
  assume "x ∈ set (zip (map σ ms) (map σ' ms))" "y ∈ set (zip (map σ ms) (map σ' ms))" "x ≠ y"
  then have "x ∈ set (zip (map σ ns) (map σ' ns))" "y ∈ set (zip (map σ ns) (map σ' ns))" "x ≠ y"
    using assms(1)
    by (auto simp: set_zip) (metis in_set_conv_nth nth_map subset_iff)+
  then show "sp_equiv_pair x y"
    using assms(2)
    by (auto simp: sp_equiv_list_def pairwise_def)
qed

lemma ad_agr_list_subset: "set ms ⊆ set ns ⟹ ad_agr_list X (map σ ns) (map σ' ns) ⟹
  ad_agr_list X (map σ ms) (map σ' ms)"
  by (auto simp: ad_agr_list_def ad_equiv_list_def sp_equiv_list_subset set_zip)
     (metis (no_types, lifting) in_set_conv_nth nth_map subset_iff)

lemma ad_agr_list_link: "ad_agr_sets (set ns) (set ns) AD σ τ ⟷
  ad_agr_list AD (map σ ns) (map τ ns)"
  unfolding ad_agr_sets_def ad_agr_list_def
  using ad_equiv_list_link sp_equiv_list_link
  by fastforce

definition ad_agr :: "('a, 'b) fo_fmla ⇒ 'a set ⇒ ('a + 'c) val ⇒ ('a + 'c) val ⇒ bool" where
  "ad_agr φ X σ τ ⟷ ad_agr_sets (fv_fo_fmla φ) (SP φ) X σ τ"

lemma ad_agr_sets_restrict:
  "ad_agr_sets (set (fv_fo_fmla_list φ)) (set (fv_fo_fmla_list φ)) AD σ τ ⟹ ad_agr φ AD σ τ"
  using sp_equiv_mono SP_fv
  unfolding fv_fo_fmla_list_set
  by (auto simp: ad_agr_sets_def ad_agr_def) blast

lemma finite_Inl: "finite X ⟹ finite (Inl -` X)"
  using finite_vimageI[of X Inl]
  by (auto simp: vimage_def)

lemma ex_out:
  assumes "finite X"
  shows "∃k. k ∉ X ∧ k < Suc (card X)"
  using card_mono[OF assms, of "{..<Suc (card X)}"]
  by auto

lemma extend_τ:
  assumes "ad_agr_sets (FV - {n}) (S - {n}) X σ τ" "S ⊆ FV" "finite S" "τ ` (FV - {n}) ⊆ Z"
    "Inl ` X ∪ Inr ` {..<max 1 (card (Inr -` τ ` (S - {n})) + (if n ∈ S then 1 else 0))} ⊆ Z"
  shows "∃k ∈ Z. ad_agr_sets FV S X (σ(n := x)) (τ(n := k))"
proof (cases "n ∈ S")
  case True
  note n_in_S = True
  show ?thesis
  proof (cases "x ∈ Inl ` X")
    case True
    show ?thesis
      using assms n_in_S True
      apply (auto simp: ad_agr_sets_def sp_equiv_def pairwise_def intro!: bexI[of _ "x"])
      unfolding ad_equiv_pair.simps
         apply (metis True insert_Diff insert_iff subsetD)+
      done
  next
    case False
    note σ_n_not_Inl = False
    show ?thesis
    proof (cases "∃m ∈ S - {n}. x = σ m")
      case True
      obtain m where m_def: "m ∈ S - {n}" "x = σ m"
        using True
        by auto
      have τ_m_in: "τ m ∈ Z"
        using assms m_def
        by auto
      show ?thesis
        using assms n_in_S σ_n_not_Inl True m_def
        by (auto simp: ad_agr_sets_def sp_equiv_def pairwise_def intro!: bexI[of _ "τ m"])
    next
      case False
      have out: "x ∉ σ ` (S - {n})"
        using False
        by auto
      have fin: "finite (Inr -` τ ` (S - {n}))"
        using assms(3)
        by (simp add: finite_vimageI)
      obtain k where k_def: "Inr k ∉ τ ` (S - {n})" "k < Suc (card (Inr -` τ ` (S - {n})))"
        using ex_out[OF fin] True
        by auto
      show ?thesis
        using assms n_in_S σ_n_not_Inl out k_def assms(5)
        apply (auto simp: ad_agr_sets_def sp_equiv_def pairwise_def intro!: bexI[of _ "Inr k"])
        unfolding ad_equiv_pair.simps
         apply fastforce
        apply (metis image_eqI insertE insert_Diff)
        done
    qed
  qed
next
  case False
  show ?thesis
  proof (cases "x ∈ Inl ` X")
    case x_in: True
    then show ?thesis
      using assms False
      by (auto simp: ad_agr_sets_def sp_equiv_def pairwise_def intro!: bexI[of _ "x"])
  next
    case x_out: False
    then show ?thesis
      using assms False
      apply (auto simp: ad_agr_sets_def sp_equiv_def pairwise_def intro!: bexI[of _ "Inr 0"])
      unfolding ad_equiv_pair.simps
      apply fastforce
      done
  qed
qed

lemma esat_Pred:
  assumes "ad_agr_sets FV S (⋃(set ` X)) σ τ" "fv_fo_terms_set ts ⊆ FV" "σ ⊙e ts ∈ map Inl ` X"
    "t ∈ set ts"
  shows "σ ⋅e t = τ ⋅e t"
proof (cases t)
  case (Var n)
  obtain vs where vs_def: "σ ⊙e ts = map Inl vs" "vs ∈ X"
    using assms(3)
    by auto
  have "σ n ∈ set (σ ⊙e ts)"
    using assms(4)
    by (force simp: eval_eterms_def Var)
  then have "σ n ∈ Inl ` ⋃ (set ` X)"
    using vs_def(2)
    unfolding vs_def(1)
    by auto
  moreover have "n ∈ FV"
    using assms(2,4)
    by (fastforce simp: Var fv_fo_terms_set_def)
  ultimately show ?thesis
    using assms(1)
    unfolding ad_equiv_pair.simps ad_agr_sets_def Var
    by fastforce
qed auto

lemma sp_equiv_list_fv:
  assumes "(⋀i. i ∈ fv_fo_terms_set ts ⟹ ad_equiv_pair X (σ i, τ i))"
    "⋃(set_fo_term ` set ts) ⊆ X" "sp_equiv σ τ (fv_fo_terms_set ts)"
  shows "sp_equiv_list (map ((⋅e) σ) ts) (map ((⋅e) τ) ts)"
  using assms
proof (induction ts)
  case (Cons t ts)
  have ind: "sp_equiv_list (map ((⋅e) σ) ts) (map ((⋅e) τ) ts)"
    using Cons
    by (auto simp: fv_fo_terms_set_def sp_equiv_def pairwise_def)
  show ?case
  proof (cases t)
    case (Const c)
    have c_X: "c ∈ X"
      using Cons(3)
      by (auto simp: Const)
    have fv_t: "fv_fo_term_set t = {}"
      by (auto simp: Const)
    have "t' ∈ set ts ⟹ sp_equiv_pair (σ ⋅e t, τ ⋅e t) (σ ⋅e t', τ ⋅e t')" for t'
      using c_X Const Cons(2)
      apply (cases t')
       apply (auto simp: fv_fo_terms_set_def)
      unfolding ad_equiv_pair.simps
      by (metis Cons(2) ad_equiv_pair.simps fv_fo_terms_setI image_insert insert_iff list.set(2)
          mk_disjoint_insert)+
    then show "sp_equiv_list (map ((⋅e) σ) (t # ts)) (map ((⋅e) τ) (t # ts))"
      using ind pairwise_insert[of sp_equiv_pair "(σ ⋅e t, τ ⋅e t)"]
      unfolding sp_equiv_list_def set_zip_map
      by (auto simp: sp_equiv_pair_comm fv_fo_terms_set_def fv_t)
  next
    case (Var n)
    have ad_n: "ad_equiv_pair X (σ n, τ n)"
      using Cons(2)
      by (auto simp: fv_fo_terms_set_def Var)
    have sp_equiv_Var: "⋀n'. Var n' ∈ set ts ⟹ sp_equiv_pair (σ n, τ n) (σ n', τ n')"
      using Cons(4)
      by (auto simp: sp_equiv_def pairwise_def fv_fo_terms_set_def Var)
    have "t' ∈ set ts ⟹ sp_equiv_pair (σ ⋅e t, τ ⋅e t) (σ ⋅e t', τ ⋅e t')" for t'
      using Cons(2,3) sp_equiv_Var  
      apply (cases t')
       apply (auto simp: Var)
       apply (metis SUP_le_iff ad_equiv_pair.simps ad_n fo_term.set_intros imageI subset_eq)
      apply (metis SUP_le_iff ad_equiv_pair.simps ad_n fo_term.set_intros imageI subset_eq)
      done
    then show ?thesis
      using ind pairwise_insert[of sp_equiv_pair "(σ ⋅e t, τ ⋅e t)" "(λn. (σ ⋅e n, τ ⋅e n)) ` set ts"]
      unfolding sp_equiv_list_def set_zip_map
      by (auto simp: sp_equiv_pair_comm)
  qed
qed (auto simp: sp_equiv_def sp_equiv_list_def fv_fo_terms_set_def)

lemma esat_Pred_inf:
  assumes "fv_fo_terms_set ts ⊆ FV" "fv_fo_terms_set ts ⊆ S"
    "ad_agr_sets FV S AD σ τ" "ad_agr_list AD (σ ⊙e ts) vs"
    "⋃(set_fo_term ` set ts) ⊆ AD"
  shows "ad_agr_list AD (τ ⊙e ts) vs"
proof -
  have sp: "sp_equiv σ τ (fv_fo_terms_set ts)"
    using assms(2,3) sp_equiv_mono
    unfolding ad_agr_sets_def
    by auto
  have "(⋀i. i ∈ fv_fo_terms_set ts ⟹ ad_equiv_pair AD (σ i, τ i))"
    using assms(1,3)
    by (auto simp: ad_agr_sets_def)
  then have "sp_equiv_list (map ((⋅e) σ) ts) (map ((⋅e) τ) ts)"
    using sp_equiv_list_fv[OF _ assms(5) sp]
    by auto
  moreover have "t ∈ set ts ⟹ ∀i∈fv_fo_terms_set ts. ad_equiv_pair AD (σ i, τ i) ⟹ sp_equiv σ τ S ⟹ ad_equiv_pair AD (σ ⋅e t, τ ⋅e t)" for t
    by (cases t) (auto simp: ad_equiv_pair.simps intro!: fv_fo_terms_setI)
  ultimately have ad_agr_list:
    "ad_agr_list AD (σ ⊙e ts) (τ ⊙e ts)"
    unfolding eval_eterms_def ad_agr_list_def ad_equiv_list_link[symmetric]
    using assms(1,3)
    by (auto simp: ad_agr_sets_def)
  show ?thesis
    by (rule ad_agr_list_comm[OF ad_agr_list_trans[OF ad_agr_list_comm[OF assms(4)] ad_agr_list]])
qed

type_synonym ('a, 'c) fo_t = "'a set × nat × ('a + 'c) table"

fun esat :: "('a, 'b) fo_fmla ⇒ ('a table, 'b) fo_intp ⇒ ('a + nat) val ⇒ ('a + nat) set ⇒ bool" where
  "esat (Pred r ts) I σ X ⟷ σ ⊙e ts ∈ map Inl ` I (r, length ts)"
| "esat (Bool b) I σ X ⟷ b"
| "esat (Eqa t t') I σ X ⟷ σ ⋅e t = σ ⋅e t'"
| "esat (Neg φ) I σ X ⟷ ¬esat φ I σ X"
| "esat (Conj φ ψ) I σ X ⟷ esat φ I σ X ∧ esat ψ I σ X"
| "esat (Disj φ ψ) I σ X ⟷ esat φ I σ X ∨ esat ψ I σ X"
| "esat (Exists n φ) I σ X ⟷ (∃x ∈ X. esat φ I (σ(n := x)) X)"
| "esat (Forall n φ) I σ X ⟷ (∀x ∈ X. esat φ I (σ(n := x)) X)"

fun sz_fmla :: "('a, 'b) fo_fmla ⇒ nat" where
  "sz_fmla (Neg φ) = Suc (sz_fmla φ)"
| "sz_fmla (Conj φ ψ) = Suc (sz_fmla φ + sz_fmla ψ)"
| "sz_fmla (Disj φ ψ) = Suc (sz_fmla φ + sz_fmla ψ)"
| "sz_fmla (Exists n φ) = Suc (sz_fmla φ)"
| "sz_fmla (Forall n φ) = Suc (Suc (Suc (Suc (sz_fmla φ))))"
| "sz_fmla _ = 0"

lemma sz_fmla_induct[case_names Pred Bool Eqa Neg Conj Disj Exists Forall]:
  "(⋀r ts. P (Pred r ts)) ⟹ (⋀b. P (Bool b)) ⟹
  (⋀t t'. P (Eqa t t')) ⟹ (⋀φ. P φ ⟹ P (Neg φ)) ⟹
  (⋀φ ψ. P φ ⟹ P ψ ⟹ P (Conj φ ψ)) ⟹ (⋀φ ψ. P φ ⟹ P ψ ⟹ P (Disj φ ψ)) ⟹
  (⋀n φ. P φ ⟹ P (Exists n φ)) ⟹ (⋀n φ. P (Exists n (Neg φ)) ⟹ P (Forall n φ)) ⟹ P φ"
proof (induction "sz_fmla φ" arbitrary: φ rule: nat_less_induct)
  case 1
  have IH: "⋀ψ. sz_fmla ψ < sz_fmla φ ⟹ P ψ"
    using 1
    by auto
  then show ?case
    using 1(2,3,4,5,6,7,8,9)
    by (cases φ) auto
qed

lemma esat_fv_cong: "(⋀n. n ∈ fv_fo_fmla φ ⟹ σ n = σ' n) ⟹ esat φ I σ X ⟷ esat φ I σ' X"
proof (induction φ arbitrary: σ σ' rule: sz_fmla_induct)
  case (Pred r ts)
  then show ?case
    by (auto simp: eval_eterms_def fv_fo_terms_set_def)
       (smt comp_apply eval_eterm_cong fv_fo_term_set_cong image_insert insertCI map_eq_conv
        mk_disjoint_insert)+
next
  case (Eqa t t')
  then show ?case
    by (cases t; cases t') auto
next
  case (Neg φ)
  show ?case
    using Neg(1)[of σ σ'] Neg(2) by auto
next
  case (Conj φ1 φ2)
  show ?case
    using Conj(1,2)[of σ σ'] Conj(3) by auto
next
  case (Disj φ1 φ2)
  show ?case
    using Disj(1,2)[of σ σ'] Disj(3) by auto
next
  case (Exists n φ)
  show ?case
  proof (rule iffI)
    assume "esat (Exists n φ) I σ X"
    then obtain x where x_def: "x ∈ X" "esat φ I (σ(n := x)) X"
      by auto
    from x_def(2) have "esat φ I (σ'(n := x)) X"
      using Exists(1)[of "σ(n := x)" "σ'(n := x)"] Exists(2) by fastforce
    with x_def(1) show "esat (Exists n φ) I σ' X"
      by auto
  next
    assume "esat (Exists n φ) I σ' X"
    then obtain x where x_def: "x ∈ X" "esat φ I (σ'(n := x)) X"
      by auto
    from x_def(2) have "esat φ I (σ(n := x)) X"
      using Exists(1)[of "σ(n := x)" "σ'(n := x)"] Exists(2) by fastforce
    with x_def(1) show "esat (Exists n φ) I σ X"
      by auto
  qed
next
  case (Forall n φ)
  then show ?case
    by auto
qed auto

fun ad_terms :: "('a fo_term) list ⇒ 'a set" where
  "ad_terms ts = ⋃(set (map set_fo_term ts))"

fun act_edom :: "('a, 'b) fo_fmla ⇒ ('a table, 'b) fo_intp ⇒ 'a set" where
  "act_edom (Pred r ts) I = ad_terms ts ∪ ⋃(set ` I (r, length ts))"
| "act_edom (Bool b) I = {}"
| "act_edom (Eqa t t') I = set_fo_term t ∪ set_fo_term t'"
| "act_edom (Neg φ) I = act_edom φ I"
| "act_edom (Conj φ ψ) I = act_edom φ I ∪ act_edom ψ I"
| "act_edom (Disj φ ψ) I = act_edom φ I ∪ act_edom ψ I"
| "act_edom (Exists n φ) I = act_edom φ I"
| "act_edom (Forall n φ) I = act_edom φ I"

lemma finite_act_edom: "wf_fo_intp φ I ⟹ finite (act_edom φ I)"
  using finite_Inl
  by (induction φ I rule: wf_fo_intp.induct)
     (auto simp: finite_set_fo_term vimage_def)

fun fo_adom :: "('a, 'c) fo_t ⇒ 'a set" where
  "fo_adom (AD, n, X) = AD"

theorem main: "ad_agr φ AD σ τ ⟹ act_edom φ I ⊆ AD ⟹
  Inl ` AD ∪ Inr ` {..<d φ} ⊆ X ⟹ τ ` fv_fo_fmla φ ⊆ X ⟹
  esat φ I σ UNIV ⟷ esat φ I τ X"
proof (induction φ arbitrary: σ τ rule: sz_fmla_induct)
  case (Pred r ts)
  have fv_sub: "fv_fo_terms_set ts ⊆ fv_fo_fmla (Pred r ts)"
    by auto
  have sub_AD: "⋃(set ` I (r, length ts)) ⊆ AD"
    using Pred(2)
    by auto
  show ?case
    unfolding esat.simps
  proof (rule iffI)
    assume assm: "σ ⊙e ts ∈ map Inl ` I (r, length ts)"
    have "σ ⊙e ts = τ ⊙e ts"
      using esat_Pred[OF ad_agr_sets_mono[OF sub_AD Pred(1)[unfolded ad_agr_def]]
            fv_sub assm]
      by (auto simp: eval_eterms_def)
    with assm show "τ ⊙e ts ∈ map Inl ` I (r, length ts)"
      by auto
  next
    assume assm: "τ ⊙e ts ∈ map Inl ` I (r, length ts)"
    have "τ ⊙e ts = σ ⊙e ts"
      using esat_Pred[OF ad_agr_sets_comm[OF ad_agr_sets_mono[OF
            sub_AD Pred(1)[unfolded ad_agr_def]]] fv_sub assm]
      by (auto simp: eval_eterms_def)
    with assm show "σ ⊙e ts ∈ map Inl ` I (r, length ts)"
      by auto
  qed
next
  case (Eqa x1 x2)
  show ?case
  proof (cases x1; cases x2)
    fix c c'
    assume "x1 = Const c" "x2 = Const c'"
    with Eqa show ?thesis
      by auto
  next
    fix c m'
    assume assms: "x1 = Const c" "x2 = Var m'"
    with Eqa(1,2) have "σ m' = Inl c ⟷ τ m' = Inl c"
      apply (auto simp: ad_agr_def ad_agr_sets_def)
      unfolding ad_equiv_pair.simps
      by fastforce+
    with assms show ?thesis
      by fastforce
  next
    fix m c'
    assume assms: "x1 = Var m" "x2 = Const c'"
    with Eqa(1,2) have "σ m = Inl c' ⟷ τ m = Inl c'"
      apply (auto simp: ad_agr_def ad_agr_sets_def)
      unfolding ad_equiv_pair.simps
      by fastforce+
    with assms show ?thesis
      by auto
  next
    fix m m'
    assume assms: "x1 = Var m" "x2 = Var m'"
    with Eqa(1,2) have "σ m = σ m' ⟷ τ m = τ m'"
      by (auto simp: ad_agr_def ad_agr_sets_def sp_equiv_def pairwise_def split: if_splits)
    with assms show ?thesis
      by auto
  qed
next
  case (Neg φ)
  from Neg(2) have "ad_agr φ AD σ τ"
    by (auto simp: ad_agr_def)
  with Neg show ?case
    by auto
next
  case (Conj φ1 φ2)
  have aux: "ad_agr φ1 AD σ τ" "ad_agr φ2 AD σ τ"
    "Inl ` AD ∪ Inr ` {..<d φ1} ⊆ X" "Inl ` AD ∪ Inr ` {..<d φ2} ⊆ X"
    "τ ` fv_fo_fmla φ1 ⊆ X" "τ ` fv_fo_fmla φ2 ⊆ X"
    using Conj(3,5,6)
    by (auto simp: ad_agr_def ad_agr_sets_def sp_equiv_def pairwise_def)
  show ?case
    using Conj(1)[OF aux(1) _ aux(3) aux(5)] Conj(2)[OF aux(2) _ aux(4) aux(6)] Conj(4)
    by auto
next
  case (Disj φ1 φ2)
  have aux: "ad_agr φ1 AD σ τ" "ad_agr φ2 AD σ τ"
    "Inl ` AD ∪ Inr ` {..<d φ1} ⊆ X" "Inl ` AD ∪ Inr ` {..<d φ2} ⊆ X"
    "τ ` fv_fo_fmla φ1 ⊆ X" "τ ` fv_fo_fmla φ2 ⊆ X"
    using Disj(3,5,6)
    by (auto simp: ad_agr_def ad_agr_sets_def sp_equiv_def pairwise_def)
  show ?case
    using Disj(1)[OF aux(1) _ aux(3) aux(5)] Disj(2)[OF aux(2) _ aux(4) aux(6)] Disj(4)
    by auto
next
  case (Exists m φ)
  show ?case
  proof (rule iffI)
    assume "esat (Exists m φ) I σ UNIV"
    then obtain x where assm: "esat φ I (σ(m := x)) UNIV"
      by auto
    have "m ∈ SP φ ⟹ Suc (card (Inr -` τ ` (SP φ - {m}))) ≤ card (SP φ)"
      by (metis Diff_insert_absorb card_image card_le_Suc_iff finite_Diff finite_SP
          image_vimage_subset inj_Inr mk_disjoint_insert surj_card_le)
    moreover have "card (Inr -` τ ` SP φ) ≤ card (SP φ)"
      by (metis card_image finite_SP image_vimage_subset inj_Inr surj_card_le)
    ultimately have "max 1 (card (Inr -` τ ` (SP φ - {m})) + (if m ∈ SP φ then 1 else 0)) ≤ d φ"
      using d_pos card_SP_d[of φ]
      by auto
    then have "∃x' ∈ X. ad_agr φ AD (σ(m := x)) (τ(m := x'))"
      using extend_τ[OF Exists(2)[unfolded ad_agr_def fv_fo_fmla.simps SP.simps]
            SP_fv[of φ] finite_SP Exists(5)[unfolded fv_fo_fmla.simps]]
            Exists(4)
      by (force simp: ad_agr_def)
    then obtain x' where x'_def: "x' ∈ X" "ad_agr φ AD (σ(m := x)) (τ(m := x'))"
      by auto
    from Exists(5) have "τ(m := x') ` fv_fo_fmla φ ⊆ X"
      using x'_def(1) by fastforce
    then have "esat φ I (τ(m := x')) X"
      using Exists x'_def(1,2) assm
      by fastforce
    with x'_def show "esat (Exists m φ) I τ X"
      by auto
  next
    assume "esat (Exists m φ) I τ X"
    then obtain z where assm: "z ∈ X" "esat φ I (τ(m := z)) X"
      by auto
    have ad_agr: "ad_agr_sets (fv_fo_fmla φ - {m}) (SP φ - {m}) AD τ σ"
      using Exists(2)[unfolded ad_agr_def fv_fo_fmla.simps SP.simps]
      by (rule ad_agr_sets_comm)
    have "∃x. ad_agr φ AD (σ(m := x)) (τ(m := z))"
      using extend_τ[OF ad_agr SP_fv[of φ] finite_SP subset_UNIV subset_UNIV] ad_agr_sets_comm
      unfolding ad_agr_def
      by fastforce
    then obtain x where x_def: "ad_agr φ AD (σ(m := x)) (τ(m := z))"
      by auto
    have "τ(m := z) ` fv_fo_fmla (Exists m φ) ⊆ X"
      using Exists
      by fastforce
    with x_def have "esat φ I (σ(m := x)) UNIV"
      using Exists assm
      by fastforce
    then show "esat (Exists m φ) I σ UNIV"
      by auto
  qed
next
  case (Forall n φ)
  have unfold: "act_edom (Forall n φ) I = act_edom (Exists n (Neg φ)) I"
    "Inl ` AD ∪ Inr ` {..<d (Forall n φ)} = Inl ` AD ∪ Inr ` {..<d (Exists n (Neg φ))}"
    "fv_fo_fmla (Forall n φ) = fv_fo_fmla (Exists n (Neg φ))"
    by auto
  have pred: "ad_agr (Exists n (Neg φ)) AD σ τ"
    using Forall(2)
    by (auto simp: ad_agr_def)
  show ?case
    using Forall(1)[OF pred Forall(3,4,5)[unfolded unfold]]
    by auto
qed auto

lemma main_cor_inf:
  assumes "ad_agr φ AD σ τ" "act_edom φ I ⊆ AD" "d φ ≤ n"
    "τ ` fv_fo_fmla φ ⊆ Inl ` AD ∪ Inr ` {..<n}"
  shows "esat φ I σ UNIV ⟷ esat φ I τ (Inl ` AD ∪ Inr ` {..<n})"
proof -
  show ?thesis
    using main[OF assms(1,2) _ assms(4)] assms(3)
    by fastforce
qed

lemma esat_UNIV_cong:
  fixes σ :: "nat ⇒ 'a + nat"
  assumes "ad_agr φ AD σ τ" "act_edom φ I ⊆ AD"
  shows "esat φ I σ UNIV ⟷ esat φ I τ UNIV"
proof -
  show ?thesis
    using main[OF assms(1,2) subset_UNIV subset_UNIV]
    by auto
qed

lemma esat_UNIV_ad_agr_list:
  fixes σ :: "nat ⇒ 'a + nat"
  assumes "ad_agr_list AD (map σ (fv_fo_fmla_list φ)) (map τ (fv_fo_fmla_list φ))"
    "act_edom φ I ⊆ AD"
  shows "esat φ I σ UNIV ⟷ esat φ I τ UNIV"
  using esat_UNIV_cong[OF iffD2[OF ad_agr_def, OF ad_agr_sets_mono'[OF SP_fv],
        OF iffD2[OF ad_agr_list_link, OF assms(1), unfolded fv_fo_fmla_list_set]] assms(2)] .

fun fo_rep :: "('a, 'c) fo_t ⇒ 'a table" where
  "fo_rep (AD, n, X) = {ts. ∃ts' ∈ X. ad_agr_list AD (map Inl ts) ts'}"

lemma sat_esat_conv:
  fixes φ :: "('a :: infinite, 'b) fo_fmla"
  assumes fin: "wf_fo_intp φ I"
  shows "sat φ I σ ⟷ esat φ I (Inl ∘ σ :: nat ⇒ 'a + nat) UNIV"
  using assms
proof (induction φ arbitrary: I σ rule: sz_fmla_induct)
  case (Pred r ts)
  show ?case
    unfolding sat.simps esat.simps comp_def[symmetric] eval_terms_eterms[symmetric]
    by auto
next
  case (Eqa t t')
  show ?case
    by (cases t; cases t') auto
next
  case (Exists n φ)
  show ?case
  proof (rule iffI)
    assume "sat (Exists n φ) I σ"
    then obtain x where x_def: "esat φ I (Inl ∘ σ(n := x)) UNIV"
      using Exists
      by fastforce
    have Inl_unfold: "Inl ∘ σ(n := x) = (Inl ∘ σ)(n := Inl x)"
      by auto
    show "esat (Exists n φ) I (Inl ∘ σ) UNIV"
      using x_def
      unfolding Inl_unfold
      by auto
  next
    assume "esat (Exists n φ) I (Inl ∘ σ) UNIV"
    then obtain x where x_def: "esat φ I ((Inl ∘ σ)(n := x)) UNIV"
      by auto
    show "sat (Exists n φ) I σ"
    proof (cases x)
      case (Inl a)
      have Inl_unfold: "(Inl ∘ σ)(n := x) = Inl ∘ σ(n := a)"
        by (auto simp: Inl)
      show ?thesis
        using x_def[unfolded Inl_unfold] Exists
        by fastforce
    next
      case (Inr b)
      obtain c where c_def: "c ∉ act_edom φ I ∪ σ ` fv_fo_fmla φ"
        using arb_element finite_act_edom[OF Exists(2), simplified] finite_fv_fo_fmla
        by (metis finite_Un finite_imageI)
      have wf_local: "wf_fo_intp φ I"
        using Exists(2)
        by auto
      have "(a, a') ∈ set (zip (map (λx. if x = n then Inr b else (Inl ∘ σ) x) (fv_fo_fmla_list φ))
        (map (λa. Inl (if a = n then c else σ a)) (fv_fo_fmla_list φ))) ⟹
        ad_equiv_pair (act_edom φ I) (a, a')" for a a'
        using c_def
        by (cases a; cases a') (auto simp: set_zip ad_equiv_pair.simps split: if_splits)
      then have "sat φ I (σ(n := c))"
        using c_def[folded fv_fo_fmla_list_set]
        by (auto simp: ad_agr_list_def ad_equiv_list_def fun_upd_def sp_equiv_list_def pairwise_def set_zip split: if_splits
            intro!: Exists(1)[OF wf_local, THEN iffD2, OF esat_UNIV_ad_agr_list[OF _ subset_refl, THEN iffD1, OF _ x_def[unfolded Inr]]])
      then show ?thesis
        by auto
    qed
  qed
next
  case (Forall n φ)
  show ?case
    using Forall(1)[of I σ] Forall(2)
    by auto
qed auto

lemma sat_ad_agr_list:
  fixes φ :: "('a :: infinite, 'b) fo_fmla"
    and J :: "(('a, nat) fo_t, 'b) fo_intp"
  assumes "wf_fo_intp φ I"
    "ad_agr_list AD (map (Inl ∘ σ :: nat ⇒ 'a + nat) (fv_fo_fmla_list φ))
      (map (Inl ∘ τ) (fv_fo_fmla_list φ))" "act_edom φ I ⊆ AD"
  shows "sat φ I σ ⟷ sat φ I τ"
  using esat_UNIV_ad_agr_list[OF assms(2,3)] sat_esat_conv[OF assms(1)]
  by auto

definition nfv :: "('a, 'b) fo_fmla ⇒ nat" where
  "nfv φ = length (fv_fo_fmla_list φ)"

lemma nfv_card: "nfv φ = card (fv_fo_fmla φ)"
proof -
  have "distinct (fv_fo_fmla_list φ)"
    using sorted_distinct_fv_list
    by auto
  then have "length (fv_fo_fmla_list φ) = card (set (fv_fo_fmla_list φ))"
    using distinct_card by fastforce
  then show ?thesis
    unfolding fv_fo_fmla_list_set by (auto simp: nfv_def)
qed

fun rremdups :: "'a list ⇒ 'a list" where
  "rremdups [] = []"
| "rremdups (x # xs) = x # rremdups (filter ((≠) x) xs)"

lemma filter_rremdups_filter: "filter P (rremdups (filter Q xs)) =
  rremdups (filter (λx. P x ∧ Q x) xs)"
  apply (induction xs arbitrary: Q)
   apply auto
  by metis

lemma filter_rremdups: "filter P (rremdups xs) = rremdups (filter P xs)"
  using filter_rremdups_filter[where Q="λ_. True"]
  by auto

lemma filter_take: "∃j. filter P (take i xs) = take j (filter P xs)"
  apply (induction xs arbitrary: i)
   apply (auto)
   apply (metis filter.simps(1) filter.simps(2) take_Cons' take_Suc_Cons)
  apply (metis filter.simps(2) take0 take_Cons')
  done

lemma rremdups_take: "∃j. rremdups (take i xs) = take j (rremdups xs)"
proof (induction xs arbitrary: i)
  case (Cons x xs)
  show ?case
  proof (cases i)
    case (Suc n)
    obtain j where j_def: "rremdups (take n xs) = take j (rremdups xs)"
      using Cons by auto
    obtain j' where j'_def: "filter ((≠) x) (take j (rremdups xs)) =
      take j' (filter ((≠) x) (rremdups xs))"
      using filter_take
      by blast
    show ?thesis
      by (auto simp: Suc filter_rremdups[symmetric] j_def j'_def intro: exI[of _ "Suc j'"])
  qed (auto simp add: take_Cons')
qed auto

lemma rremdups_app: "rremdups (xs @ [x]) = rremdups xs @ (if x ∈ set xs then [] else [x])"
  apply (induction xs)
   apply auto
   apply (smt filter.simps(1) filter.simps(2) filter_append filter_rremdups)+
  done

lemma rremdups_set: "set (rremdups xs) = set xs"
  by (induction xs) (auto simp: filter_rremdups[symmetric])

lemma distinct_rremdups: "distinct (rremdups xs)"
proof (induction "length xs" arbitrary: xs rule: nat_less_induct)
  case 1
  then have IH: "⋀m ys. length (ys :: 'a list) < length xs ⟹ distinct (rremdups ys)"
    by auto
  show ?case
  proof (cases xs)
    case (Cons z zs)
    show ?thesis
      using IH
      by (auto simp: Cons rremdups_set le_imp_less_Suc)
  qed auto
qed

lemma length_rremdups: "length (rremdups xs) = card (set xs)"
  using distinct_card[OF distinct_rremdups]
  by (subst eq_commute) (auto simp: rremdups_set)

lemma set_map_filter_sum: "set (List.map_filter (case_sum Map.empty Some) xs) = Inr -` set xs"
  by (induction xs) (auto simp: List.map_filter_simps split: sum.splits)

definition nats :: "nat list ⇒ bool" where
  "nats ns = (ns = [0..<length ns])"

definition fo_nmlzd :: "'a set ⇒ ('a + nat) list ⇒ bool" where
  "fo_nmlzd AD xs ⟷ Inl -` set xs ⊆ AD ∧
    (let ns = List.map_filter (case_sum Map.empty Some) xs in nats (rremdups ns))"

lemma fo_nmlzd_all_AD:
  assumes "set xs ⊆ Inl ` AD"
  shows "fo_nmlzd AD xs"
proof -
  have "List.map_filter (case_sum Map.empty Some) xs = []"
    using assms
    by (induction xs) (auto simp: List.map_filter_simps)
  then show ?thesis
    using assms
    by (auto simp: fo_nmlzd_def nats_def Let_def)
qed

lemma card_Inr_vimage_le_length: "card (Inr -` set xs) ≤ length xs"
proof -
  have "card (Inr -` set xs) ≤ card (set xs)"
    by (meson List.finite_set card_inj_on_le image_vimage_subset inj_Inr)
  moreover have "… ≤ length xs"
    by (rule card_length)
  finally show ?thesis .
qed

lemma fo_nmlzd_set:
  assumes "fo_nmlzd AD xs"
  shows "set xs = set xs ∩ Inl ` AD ∪ Inr ` {..<min (length xs) (card (Inr -` set xs))}"
proof -
  have "Inl -` set xs ⊆ AD"
    using assms
    by (auto simp: fo_nmlzd_def)
  moreover have "Inr -` set xs = {..<card (Inr -` set xs)}"
    using assms
    by (auto simp: Let_def fo_nmlzd_def nats_def length_rremdups set_map_filter_sum rremdups_set
        dest!: arg_cong[of _ _ set])
  ultimately have "set xs = set xs ∩ Inl ` AD ∪ Inr ` {..<card (Inr -` set xs)}"
    by auto (metis (no_types, lifting) UNIV_I UNIV_sum UnE image_iff subset_iff vimageI)
  then show ?thesis
    using card_Inr_vimage_le_length[of xs]
    by (metis min.absorb2)
qed

lemma map_filter_take: "∃j. List.map_filter f (take i xs) = take j (List.map_filter f xs)"
  apply (induction xs arbitrary: i)
   apply (auto simp: List.map_filter_simps split: option.splits)
   apply (metis map_filter_simps(1) option.case(1) take0 take_Cons')
  apply (metis map_filter_simps(1) map_filter_simps(2) option.case(2) take_Cons' take_Suc_Cons)
  done

lemma fo_nmlzd_take: assumes "fo_nmlzd AD xs"
  shows "fo_nmlzd AD (take i xs)"
proof -
  have aux: "rremdups zs = [0..<length (rremdups zs)] ⟹ rremdups (take j zs) =
    [0..<length (rremdups (take j zs))]" for j zs
    using rremdups_take[of j zs]
    by (auto simp add: min_def) (metis add_0 linorder_le_cases take_upt)
  show ?thesis
    using assms map_filter_take[of "case_sum Map.empty Some" i xs] set_take_subset
    using aux[where ?zs="List.map_filter (case_sum Map.empty Some) xs"]
    by (fastforce simp: fo_nmlzd_def vimage_def nats_def Let_def)
qed

lemma map_filter_app: "List.map_filter f (xs @ [x]) = List.map_filter f xs @
  (case f x of Some y ⇒ [y] | _ ⇒ [])"
  by (induction xs) (auto simp: List.map_filter_simps split: option.splits)

lemma fo_nmlzd_app_Inr: "Inr n ∉ set xs ⟹ Inr n' ∉ set xs ⟹ fo_nmlzd AD (xs @ [Inr n]) ⟹
  fo_nmlzd AD (xs @ [Inr n']) ⟹ n = n'"
  by (auto simp: List.map_filter_simps fo_nmlzd_def nats_def Let_def map_filter_app
      rremdups_app set_map_filter_sum)

fun all_tuples :: "'c set ⇒ nat ⇒ 'c table" where
  "all_tuples xs 0 = {[]}"
| "all_tuples xs (Suc n) = ⋃((λas. (λx. x # as) ` xs) ` (all_tuples xs n))"

definition nall_tuples :: "'a set ⇒ nat ⇒ ('a + nat) table" where
  "nall_tuples AD n = {zs ∈ all_tuples (Inl ` AD ∪ Inr ` {..<n}) n. fo_nmlzd AD zs}"

lemma all_tuples_finite: "finite xs ⟹ finite (all_tuples xs n)"
  by (induction xs n rule: all_tuples.induct) auto

lemma nall_tuples_finite: "finite AD ⟹ finite (nall_tuples AD n)"
  by (auto simp: nall_tuples_def all_tuples_finite)

lemma all_tuplesI: "length vs = n ⟹ set vs ⊆ xs ⟹ vs ∈ all_tuples xs n"
proof (induction xs n arbitrary: vs rule: all_tuples.induct)
  case (2 xs n)
  then obtain w ws where "vs = w # ws" "length ws = n" "set ws ⊆ xs" "w ∈ xs"
    by (metis Suc_length_conv contra_subsetD list.set_intros(1) order_trans set_subset_Cons)
  with 2(1) show ?case
    by auto
qed auto

lemma nall_tuplesI: "length vs = n ⟹ fo_nmlzd AD vs ⟹ vs ∈ nall_tuples AD n"
  using fo_nmlzd_set[of AD vs]
  by (auto simp: nall_tuples_def intro!: all_tuplesI)

lemma all_tuplesD: "vs ∈ all_tuples xs n ⟹ length vs = n ∧ set vs ⊆ xs"
  by (induction xs n arbitrary: vs rule: all_tuples.induct) auto+

lemma all_tuples_setD: "vs ∈ all_tuples xs n ⟹ set vs ⊆ xs"
  by (auto dest: all_tuplesD)

lemma nall_tuplesD: "vs ∈ nall_tuples AD n ⟹
  length vs = n ∧ set vs ⊆ Inl ` AD ∪ Inr ` {..<n} ∧ fo_nmlzd AD vs"
  by (auto simp: nall_tuples_def dest: all_tuplesD)

lemma all_tuples_set: "all_tuples xs n = {ys. length ys = n ∧ set ys ⊆ xs}"
proof (induction xs n rule: all_tuples.induct)
  case (2 xs n)
  show ?case
  proof (rule subset_antisym; rule subsetI)
    fix ys
    assume "ys ∈ all_tuples xs (Suc n)"
    then show "ys ∈ {ys. length ys = Suc n ∧ set ys ⊆ xs}"
      using 2 by auto
  next
    fix ys
    assume "ys ∈ {ys. length ys = Suc n ∧ set ys ⊆ xs}"
    then have assm: "length ys = Suc n" "set ys ⊆ xs"
      by auto
    then obtain z zs where zs_def: "ys = z # zs" "z ∈ xs" "length zs = n" "set zs ⊆ xs"
      by (cases ys) auto
    with 2 have "zs ∈ all_tuples xs n"
      by auto
    with zs_def(1,2) show "ys ∈ all_tuples xs (Suc n)"
      by auto
  qed
qed auto

lemma nall_tuples_set: "nall_tuples AD n = {ys. length ys = n ∧ fo_nmlzd AD ys}"
  using fo_nmlzd_set[of AD] card_Inr_vimage_le_length
  by (auto simp: nall_tuples_def all_tuples_set) (smt UnE nall_tuplesD nall_tuplesI subsetD)

fun pos :: "'a ⇒ 'a list ⇒ nat option" where
  "pos a [] = None"
| "pos a (x # xs) =
    (if a = x then Some 0 else (case pos a xs of Some n ⇒ Some (Suc n) | _ ⇒ None))"

lemma pos_set: "pos a xs = Some i ⟹ a ∈ set xs"
  by (induction a xs arbitrary: i rule: pos.induct) (auto split: if_splits option.splits)

lemma pos_length: "pos a xs = Some i ⟹ i < length xs"
  by (induction a xs arbitrary: i rule: pos.induct) (auto split: if_splits option.splits)

lemma pos_sound: "pos a xs = Some i ⟹ i < length xs ∧ xs ! i = a"
  by (induction a xs arbitrary: i rule: pos.induct) (auto split: if_splits option.splits)

lemma pos_complete: "pos a xs = None ⟹ a ∉ set xs"
  by (induction a xs rule: pos.induct) (auto split: if_splits option.splits)

fun rem_nth :: "nat ⇒ 'a list ⇒ 'a list" where
  "rem_nth _ [] = []"
| "rem_nth 0 (x # xs) = xs"
| "rem_nth (Suc n) (x # xs) = x # rem_nth n xs"

lemma rem_nth_length: "i < length xs ⟹ length (rem_nth i xs) = length xs - 1"
  by (induction i xs rule: rem_nth.induct) auto

lemma rem_nth_take_drop: "i < length xs ⟹ rem_nth i xs = take i xs @ drop (Suc i) xs"
  by (induction i xs rule: rem_nth.induct) auto

lemma rem_nth_sound: "distinct xs ⟹ pos n xs = Some i ⟹
  rem_nth i (map σ xs) = map σ (filter ((≠) n) xs)"
  apply (induction xs arbitrary: i)
   apply (auto simp: pos_set split: option.splits)
  by (metis (mono_tags, lifting) filter_True)

fun add_nth :: "nat ⇒ 'a ⇒ 'a list ⇒ 'a list" where
  "add_nth 0 a xs = a # xs"
| "add_nth (Suc n) a zs = (case zs of x # xs ⇒ x # add_nth n a xs)"

lemma add_nth_length: "i ≤ length zs ⟹ length (add_nth i z zs) = Suc (length zs)"
  by (induction i z zs rule: add_nth.induct) (auto split: list.splits)

lemma add_nth_take_drop: "i ≤ length zs ⟹ add_nth i v zs = take i zs @ v # drop i zs"
  by (induction i v zs rule: add_nth.induct) (auto split: list.splits)

lemma add_nth_rem_nth_map: "distinct xs ⟹ pos n xs = Some i ⟹
  add_nth i a (rem_nth i (map σ xs)) = map (σ(n := a)) xs"
  by (induction xs arbitrary: i) (auto simp: pos_set split: option.splits)

lemma add_nth_rem_nth_self: "i < length xs ⟹ add_nth i (xs ! i) (rem_nth i xs) = xs"
  by (induction i xs rule: rem_nth.induct) auto

lemma rem_nth_add_nth: "i ≤ length zs ⟹ rem_nth i (add_nth i z zs) = zs"
  by (induction i z zs rule: add_nth.induct) (auto split: list.splits)

fun merge :: "(nat × 'a) list ⇒ (nat × 'a) list ⇒ (nat × 'a) list" where
  "merge [] mys = mys"
| "merge nxs [] = nxs"
| "merge ((n, x) # nxs) ((m, y) # mys) =
    (if n ≤ m then (n, x) # merge nxs ((m, y) # mys)
    else (m, y) # merge ((n, x) # nxs) mys)"

lemma merge_Nil2[simp]: "merge nxs [] = nxs"
  by (cases nxs) auto

lemma merge_length: "length (merge nxs mys) = length (map fst nxs @ map fst mys)"
  by (induction nxs mys rule: merge.induct) auto

lemma insort_aux_le: "∀x∈set nxs. n ≤ fst x ⟹ ∀x∈set mys. m ≤ fst x ⟹ n ≤ m ⟹
  insort n (sort (map fst nxs @ m # map fst mys)) = n # sort (map fst nxs @ m # map fst mys)"
  by (induction nxs) (auto simp: insort_is_Cons insort_left_comm)

lemma insort_aux_gt: "∀x∈set nxs. n ≤ fst x ⟹ ∀x∈set mys. m ≤ fst x ⟹ ¬ n ≤ m ⟹
  insort n (sort (map fst nxs @ m # map fst mys)) =
    m # insort n (sort (map fst nxs @ map fst mys))"
  apply (induction nxs)
   apply (auto simp: insort_is_Cons)
  by (metis dual_order.trans insort_key.simps(2) insort_left_comm)

lemma map_fst_merge: "sorted_distinct (map fst nxs) ⟹ sorted_distinct (map fst mys) ⟹
  map fst (merge nxs mys) = sort (map fst nxs @ map fst mys)"
  by (induction nxs mys rule: merge.induct)
     (auto simp add: sorted_sort_id insort_is_Cons insort_aux_le insort_aux_gt)

lemma merge_map': "sorted_distinct (map fst nxs) ⟹ sorted_distinct (map fst mys) ⟹
  fst ` set nxs ∩ fst ` set mys = {} ⟹
  map snd nxs = map σ (map fst nxs) ⟹ map snd mys = map σ (map fst mys) ⟹
  map snd (merge nxs mys) = map σ (sort (map fst nxs @ map fst mys))"
  by (induction nxs mys rule: merge.induct)
     (auto simp: sorted_sort_id insort_is_Cons insort_aux_le insort_aux_gt)

lemma merge_map: "sorted_distinct ns ⟹ sorted_distinct ms ⟹ set ns ∩ set ms = {} ⟹
  map snd (merge (zip ns (map σ ns)) (zip ms (map σ ms))) = map σ (sort (ns @ ms))"
  using merge_map'[of "zip ns (map σ ns)" "zip ms (map σ ms)" σ]
  by auto (metis length_map list.set_map map_fst_zip)

fun fo_nmlz_rec :: "nat ⇒ ('a + nat ⇀ nat) ⇒ 'a set ⇒
  ('a + nat) list ⇒ ('a + nat) list" where
  "fo_nmlz_rec i m AD [] = []"
| "fo_nmlz_rec i m AD (Inl x # xs) = (if x ∈ AD then Inl x # fo_nmlz_rec i m AD xs else
    (case m (Inl x) of None ⇒ Inr i # fo_nmlz_rec (Suc i) (m(Inl x ↦ i)) AD xs
    | Some j ⇒ Inr j # fo_nmlz_rec i m AD xs))"
| "fo_nmlz_rec i m AD (Inr n # xs) = (case m (Inr n) of None ⇒
    Inr i # fo_nmlz_rec (Suc i) (m(Inr n ↦ i)) AD xs
  | Some j ⇒ Inr j # fo_nmlz_rec i m AD xs)"

lemma fo_nmlz_rec_sound: "ran m ⊆ {..<i} ⟹ filter ((≤) i) (rremdups
  (List.map_filter (case_sum Map.empty Some) (fo_nmlz_rec i m AD xs))) = ns ⟹
  ns = [i..<i + length ns]"
proof (induction i m AD xs arbitrary: ns rule: fo_nmlz_rec.induct)
  case (2 i m AD x xs)
  then show ?case
  proof (cases "x ∈ AD")
    case False
    show ?thesis
    proof (cases "m (Inl x)")
      case None
      have pred: "ran (m(Inl x ↦ i)) ⊆ {..<Suc i}"
        using 2(4) None
        by (auto simp: inj_on_def dom_def ran_def)
      have "ns = i # filter ((≤) (Suc i)) (rremdups
        (List.map_filter (case_sum Map.empty Some) (fo_nmlz_rec (Suc i) (m(Inl x ↦ i)) AD xs)))"
        using 2(5) False None
        by (auto simp: List.map_filter_simps filter_rremdups)
           (metis Suc_leD antisym not_less_eq_eq)
      then show ?thesis
        by (auto simp: 2(2)[OF False None pred, OF refl])
           (smt Suc_le_eq Suc_pred le_add1 le_zero_eq less_add_same_cancel1 not_less_eq_eq
            upt_Suc_append upt_rec)
    next
      case (Some j)
      then have j_lt_i: "j < i"
        using 2(4)
        by (auto simp: ran_def)
      have ns_def: "ns = filter ((≤) i) (rremdups
        (List.map_filter (case_sum Map.empty Some) (fo_nmlz_rec i m AD xs)))"
        using 2(5) False Some j_lt_i
        by (auto simp: List.map_filter_simps filter_rremdups) (metis leD)
      show ?thesis
        by (rule 2(3)[OF False Some 2(4) ns_def[symmetric]])
    qed
  qed (auto simp: List.map_filter_simps split: option.splits)
next
  case (3 i m AD n xs)
  show ?case
  proof (cases "m (Inr n)")
    case None
    have pred: "ran (m(Inr n ↦ i)) ⊆ {..<Suc i}"
      using 3(3) None
      by (auto simp: inj_on_def dom_def ran_def)
    have "ns = i # filter ((≤) (Suc i)) (rremdups
      (List.map_filter (case_sum Map.empty Some) (fo_nmlz_rec (Suc i) (m(Inr n ↦ i)) AD xs)))"
      using 3(4) None
      by (auto simp: List.map_filter_simps filter_rremdups) (metis Suc_leD antisym not_less_eq_eq)
    then show ?thesis
      by (auto simp add: 3(1)[OF None pred, OF refl])
         (smt Suc_le_eq Suc_pred le_add1 le_zero_eq less_add_same_cancel1 not_less_eq_eq
          upt_Suc_append upt_rec)
  next
    case (Some j)
    then have j_lt_i: "j < i"
      using 3(3)
      by (auto simp: ran_def)
    have ns_def: "ns = filter ((≤) i) (rremdups
      (List.map_filter (case_sum Map.empty Some) (fo_nmlz_rec i m AD xs)))"
      using 3(4) Some j_lt_i
      by (auto simp: List.map_filter_simps filter_rremdups) (metis leD)
    show ?thesis
      by (rule 3(2)[OF Some 3(3) ns_def[symmetric]])
  qed
qed (auto simp: List.map_filter_simps)

definition id_map :: "nat ⇒ ('a + nat ⇀ nat)" where
  "id_map n = (λx. case x of Inl x ⇒ None | Inr x ⇒ if x < n then Some x else None)"

lemma fo_nmlz_rec_idem: "Inl -` set ys ⊆ AD ⟹
  rremdups (List.map_filter (case_sum Map.empty Some) ys) = ns ⟹
  set (filter (λn. n < i) ns) ⊆ {..<i} ⟹ filter ((≤) i) ns = [i..<i + k] ⟹
  fo_nmlz_rec i (id_map i) AD ys = ys"
proof (induction ys arbitrary: i k ns)
  case (Cons y ys)
  show ?case
  proof (cases y)
    case (Inl a)
    show ?thesis
      using Cons(1)[OF _ _ Cons(4,5)] Cons(2,3)
      by (auto simp: Inl List.map_filter_simps)
  next
    case (Inr j)
    show ?thesis
    proof (cases "j < i")
      case False
      have j_i: "j = i"
        using False Cons(3,5)
        by (auto simp: Inr List.map_filter_simps filter_rremdups in_mono split: if_splits)
           (metis (no_types, lifting) upt_eq_Cons_conv)
      obtain kk where k_def: "k = Suc kk"
        using Cons(3,5)
        by (cases k) (auto simp: Inr List.map_filter_simps j_i)
      define ns' where "ns' = rremdups (List.map_filter (case_sum Map.empty Some) ys)"
      have id_map_None: "id_map i (Inr i) = None"
        by (auto simp: id_map_def)
      have id_map_upd: "(id_map i)(Inr i ↦ i) = id_map (Suc i)"
        by (auto simp: id_map_def split: sum.splits)
      have "set (filter (λn. n < Suc i) ns') ⊆ {..<Suc i}"
        using Cons(2,3)
        by auto
      moreover have "filter ((≤) (Suc i)) ns' = [Suc i..<i + k]"
        using Cons(3,5)
        by (auto simp: Inr List.map_filter_simps j_i filter_rremdups[symmetric] ns'_def[symmetric])
           (smt One_nat_def Suc_eq_plus1 Suc_le_eq add_diff_cancel_left' diff_is_0_eq'
            dual_order.order_iff_strict filter_cong n_not_Suc_n upt_eq_Cons_conv)
      moreover have "Inl -` set ys ⊆ AD"
        using Cons(2)
        by (auto simp: vimage_def)
      ultimately have "fo_nmlz_rec (Suc i) ((id_map i)(Inr i ↦ i)) AD ys = ys"
        using Cons(1)[OF _ ns'_def[symmetric], of "Suc i" kk]
        by (auto simp: ns'_def k_def id_map_upd split: if_splits)
      then show ?thesis
        by (auto simp: Inr j_i id_map_None)
    next
      case True
      define ns' where "ns' = rremdups (List.map_filter (case_sum Map.empty Some) ys)"
      have "set (filter (λy. y < i) ns') ⊆ set (filter (λy. y < i) ns)"
        "filter ((≤) i) ns' = filter ((≤) i) ns"
        using Cons(3) True
        by (auto simp: Inr List.map_filter_simps filter_rremdups[symmetric] ns'_def[symmetric])
           (smt filter_cong leD)
      then have "fo_nmlz_rec i (id_map i) AD ys = ys"
        using Cons(1)[OF _ ns'_def[symmetric]] Cons(3,5) Cons(2)
        by (auto simp: vimage_def)
      then show ?thesis
        using True
        by (auto simp: Inr id_map_def)
    qed
  qed
qed (auto simp: List.map_filter_simps intro!: exI[of _ "[]"])

lemma fo_nmlz_rec_length: "length (fo_nmlz_rec i m AD xs) =