Theory Restrict_Frees

(*<*)
theory Restrict_Frees
imports
  Restrict_Bounds
  "HOL-Library.Product_Lexorder"
  "HOL-Library.List_Lexorder"
  "HOL-Library.Multiset_Order"
begin

hide_const (open) SetIndex.index
(*>*)

section ‹Restricting Free Variables›

definition fixfree :: "(('a, 'b) fmla × nat rel) set ⇒ (('a, 'b) fmla × nat rel) set" where
  "fixfree 𝒬fin = {(Qfix, Qeq) ∈ 𝒬fin. nongens Qfix ≠ {}}"

definition "disjointvars Q Qeq = (⋃V ∈ classes Qeq. if V ∩ fv Q = {} then V else {})"

fun Conjs where
  "Conjs Q [] = Q"
| "Conjs Q ((x, y) # xys) = Conjs (Conj Q (x ≈ y)) xys"

function (sequential) Conjs_disjoint where
  "Conjs_disjoint Q xys = (case find (λ(x,y). {x, y} ∩ fv Q ≠ {}) xys of
     None ⇒ Conjs Q xys
   | Some (x, y) ⇒ Conjs_disjoint (Conj Q (x ≈ y)) (remove1 (x, y) xys))"
  by pat_completeness auto
termination
  by (relation "measure (λ(Q, xys). length xys)")
    (auto split: if_splits simp: length_remove1 neq_Nil_conv dest!: find_SomeD dest: length_pos_if_in_set)

declare Conjs_disjoint.simps[simp del]

definition CONJ where
  "CONJ = (λ(Q, Qeq). Conjs Q (sorted_list_of_set Qeq))"

definition CONJ_disjoint where
  "CONJ_disjoint = (λ(Q, Qeq). Conjs_disjoint Q (sorted_list_of_set Qeq))"

definition inf where
  "inf 𝒬fin Q = {(Q', Qeq) ∈ 𝒬fin. disjointvars Q' Qeq ≠ {} ∨ fv Q' ∪ Field Qeq ≠ fv Q}"

definition FV where
  "FV Q Qfin Qinf ≡ (fv Qfin = fv Q ∨ Qfin = Bool False) ∧ fv Qinf = {}"

definition EVAL where
  "EVAL Q Qfin Qinf ≡ (∀I. finite (adom I) ⟶ (if eval Qinf I = {} then
     eval Qfin I = eval Q I else infinite (eval Q I)))"

definition EVAL' where
  "EVAL' Q Qfin Qinf ≡ (∀I. finite (adom I) ⟶ (if eval Qinf I = {} then
     eval_on (fv Q) Qfin I = eval Q I else infinite (eval Q I)))"

definition (in simplification) split_spec :: "('a :: {infinite, linorder}, 'b :: linorder) fmla ⇒ (('a, 'b) fmla × ('a, 'b) fmla) nres" where
  "split_spec Q = SPEC (λ(Qfin, Qinf). sr Qfin ∧ sr Qinf ∧ FV Q Qfin Qinf ∧ EVAL Q Qfin Qinf ∧
     simplified Qfin ∧ simplified Qinf)"

definition (in simplification) "assemble = (λ(𝒬fin, 𝒬inf). (simp (DISJ (CONJ_disjoint ` 𝒬fin)), simp (DISJ (close ` 𝒬inf))))"

fun leftfresh where
  "leftfresh Q [] = True"
| "leftfresh Q ((x, y) # xys) = (x ∉ fv Q ∧ leftfresh (Conj Q (x ≈ y)) xys)"

definition (in simplification) "wf_state Q P =
   (λ(𝒬fin, 𝒬inf). finite 𝒬fin ∧ finite 𝒬inf ∧
     (∀(Qfix, Qeq) ∈ 𝒬fin. P Qfix ∧ simplified Qfix ∧ (∃xs. leftfresh Qfix xs ∧ distinct xs ∧ set xs = Qeq) ∧ fv Qfix ∪ Field Qeq ⊆ fv Q ∧ irrefl Qeq))"

definition (in simplification) "split_INV1 Q = (λ𝒬pair. wf_state Q rrb 𝒬pair ∧ (let (Qfin, Qinf) = assemble 𝒬pair in EVAL' Q Qfin Qinf))"
definition (in simplification) "split_INV2 Q = (λ𝒬pair. wf_state Q sr 𝒬pair ∧ (let (Qfin, Qinf) = assemble 𝒬pair in EVAL' Q Qfin Qinf))"

definition (in simplification) split :: "('a :: {infinite, linorder}, 'b :: linorder) fmla ⇒ (('a, 'b) fmla × ('a, 'b) fmla) nres" where
  "split Q = do {
     Q' ← rb Q;
     𝒬pair ← WHILET⇗split_INV1 Q⇖
        (λ(𝒬fin, _). fixfree 𝒬fin ≠ {}) (λ(𝒬fin, 𝒬inf). do {
          (Qfix, Qeq) ← RES (fixfree 𝒬fin);
          x ← RES (nongens Qfix);
          G ← SPEC (cov x Qfix);
          let 𝒬fin = 𝒬fin - {(Qfix, Qeq)} ∪
            {(simp (Conj Qfix (DISJ (qps G))), Qeq)} ∪
            (⋃y ∈ eqs x G. {(cp (Qfix[x → y]), Qeq ∪ {(x,y)})});
          let 𝒬inf = 𝒬inf ∪ {cp (Qfix ⊥ x)};
          RETURN (𝒬fin, 𝒬inf)})
        ({(Q', {})}, {});
     𝒬pair ← WHILET⇗split_INV2 Q⇖
        (λ(𝒬fin, _). inf 𝒬fin Q ≠ {}) (λ(𝒬fin, 𝒬inf). do {
          Qpair ← RES (inf 𝒬fin Q);
          let 𝒬fin = 𝒬fin - {Qpair};
          let 𝒬inf = 𝒬inf ∪ {CONJ Qpair};
          RETURN (𝒬fin, 𝒬inf)})
        𝒬pair;
     let (Qfin, Qinf) = assemble 𝒬pair;
     Qinf ← rb Qinf;
     RETURN (Qfin, Qinf)}"

lemma finite_fixfree[simp]: "finite 𝒬 ⟹ finite (fixfree 𝒬)"
  unfolding fixfree_def by (auto elim!: finite_subset[rotated])

lemma (in simplification) split_step_in_mult:
  assumes "(Qfin, Qeq) ∈ 𝒬fin" "finite 𝒬fin" "x ∈ nongens Qfin" "cov x Qfin G" "fv Qfin ⊆ F"
  shows "((nongens ∘ fst) `# mset_set (insert (simp (Conj Qfin (DISJ (qps G))), Qeq) (𝒬fin - {(Qfin, Qeq)} ∪ (λy. (cp (Qfin[x → y]), insert (x, y) Qeq)) ` eqs x G)),
          (nongens ∘ fst) `# mset_set 𝒬fin) ∈ mult {(X, Y). X ⊂ Y ∧ Y ⊆ F}"
    (is "(?f (insert ?Q (?A ∪ ?B)), ?C) ∈ mult ?R")
proof (subst preorder.multDM[where less_eq = "(in_rel ?R)=="])
  define X where "X = {(Qfin, Qeq)}"
  define Y where "Y = insert ?Q ?B - (?A ∩ insert ?Q ?B)"
  have "?f X ≠ {#}"
    unfolding X_def by auto
  moreover from assms(1,2) have "?f X ⊆# ?C"
    unfolding X_def by (auto intro!: image_eqI[where x = "(Qfin, Qeq)"])
  moreover from assms(1,2,4) have XY:
    "insert ?Q (?A ∪ ?B) = 𝒬fin - X ∪ Y" "X ⊆ 𝒬fin" "(𝒬fin - X) ∩ Y = {}" "finite X" "finite Y"
    unfolding X_def Y_def by auto
  with assms(2) have "?f (insert ?Q (?A ∪ ?B)) = ?C - ?f X + ?f Y"
    by (force simp: mset_set_Union mset_set_Diff multiset.map_comp o_def
        dest: subset_imp_msubset_mset_set elim: subset_mset.trans
        intro!: subset_imp_msubset_mset_set image_mset_subseteq_mono subset_mset.diff_add_assoc2
        trans[OF image_mset_Diff])
  moreover
  { fix A
    assume "A ∈ Y"
    then have "A ∈ insert ?Q ?B"
      unfolding Y_def by blast
    with assms(3,4) have "nongens (fst A) ⊆ nongens Qfin - {x}"
      using Gen_cp_subst[of _ Qfin x] Gen_simp[OF cov_Gen_qps[OF assms(4)]]
        gen_Gen_simp[OF gen.intros(7)[OF disjI1], of _ Qfin _ "DISJ (qps G)"]
      by (fastforce simp: nongens_def fv_subst simp del: cp.simps
          intro!: gen.intros(7) dest!: fv_cp[THEN set_mp] fv_simp[THEN set_mp] fv_DISJ[THEN set_mp, rotated 1]
          elim: cov_fv[OF assms(4) _ qps_in, THEN conjunct2, THEN set_mp]
          cov_fv[OF assms(4) _ eqs_in, THEN conjunct2, THEN set_mp])
    with assms(3) have "nongens (fst A) ⊂ nongens Qfin"
      by auto
    with assms(5) have "∃B ∈ X. nongens (fst A) ⊂ nongens (fst B) ∧ nongens (fst B) ⊆ F"
      by (auto simp: X_def nongens_def)
  }
  with XY have "⋀A. A ∈# ?f Y ⟹ ∃B. B ∈# ?f X ∧ A ⊂ B ∧ B ⊆ F"
    by auto
  ultimately
  show "∃X Y. X ≠ {#} ∧ X ⊆# ?C ∧ ?f (insert ?Q (?A ∪ ?B)) = ?C - X + Y ∧ (∀k. k ∈# Y ⟶ (∃a. a ∈# X ∧ k ⊂ a ∧ a ⊆ F))"
    by blast
qed (unfold_locales, auto)

lemma EVAL_cong:
  "Qinf ≜ Qinf' ⟹ fv Qinf = fv Qinf' ⟹ EVAL Q Qfin Qinf = EVAL Q Qfin Qinf'"
  using equiv_eval_eqI[of _ Qinf Qinf']
  by (auto simp: EVAL_def)

lemma EVAL'_cong:
  "Qinf ≜ Qinf' ⟹ fv Qinf = fv Qinf' ⟹ EVAL' Q Qfin Qinf = EVAL' Q Qfin Qinf'"
  using equiv_eval_eqI[of _ Qinf Qinf']
  by (auto simp: EVAL'_def)

lemma fv_Conjs[simp]: "fv (Conjs Q xys) = fv Q ∪ Field (set xys)"
  by (induct Q xys rule: Conjs.induct) auto

lemma fv_Conjs_disjoint[simp]: "distinct xys ⟹ fv (Conjs_disjoint Q xys) = fv Q ∪ Field (set xys)"
proof (induct Q xys rule: Conjs_disjoint.induct)
  case (1 Q xys)
  then show ?case
    by (subst Conjs_disjoint.simps)
      (auto split: option.splits simp: Field_def subset_eq dest: find_SomeD(2))
qed

lemma fv_CONJ[simp]: "finite Qeq ⟹ fv (CONJ (Q, Qeq)) = fv Q ∪ Field Qeq"
  unfolding CONJ_def by (auto dest!: fv_cp[THEN set_mp])

lemma fv_CONJ_disjoint[simp]: "finite Qeq ⟹ fv (CONJ_disjoint (Q, Qeq)) = fv Q ∪ Field Qeq"
  unfolding CONJ_disjoint_def by auto

lemma rrb_Conjs: "rrb Q ⟹ rrb (Conjs Q xys)"
  by (induct Q xys rule: Conjs.induct) auto

lemma CONJ_empty[simp]: "CONJ (Q, {}) = Q"
  by (auto simp: CONJ_def)

lemma CONJ_disjoint_empty[simp]: "CONJ_disjoint (Q, {}) = Q"
  by (auto simp: CONJ_disjoint_def Conjs_disjoint.simps)

lemma Conjs_eq_False_iff[simp]: "irrefl (set xys) ⟹ Conjs Q xys = Bool False ⟷ Q = Bool False ∧ xys = []"
  by (induct Q xys rule: Conjs.induct) (auto simp: Let_def is_Bool_def irrefl_def)

lemma CONJ_eq_False_iff[simp]: "finite Qeq ⟹ irrefl Qeq ⟹ CONJ (Q, Qeq) = Bool False ⟷ Q = Bool False ∧ Qeq = {}"
  by (auto simp: CONJ_def)

lemma Conjs_disjoint_eq_False_iff[simp]: "irrefl (set xys) ⟹ Conjs_disjoint Q xys = Bool False ⟷ Q = Bool False ∧ xys = []"
proof (induct Q xys rule: Conjs_disjoint.induct)
  case (1 Q xys)
  then show ?case
    by (subst Conjs_disjoint.simps)
      (auto simp: Let_def is_Bool_def irrefl_def split: option.splits)
qed

lemma CONJ_disjoint_eq_False_iff[simp]: "finite Qeq ⟹ irrefl Qeq ⟹ CONJ_disjoint (Q, Qeq) = Bool False ⟷ Q = Bool False ∧ Qeq = {}"
  by (auto simp: CONJ_disjoint_def)

lemma sr_Conjs_disjoint:
  "distinct xys ⟹ (∀V∈classes (set xys). V ∩ fv Q ≠ {}) ⟹ sr Q ⟹ sr (Conjs_disjoint Q xys)"
proof (induct Q xys rule: Conjs_disjoint.induct)
  case (1 Q xys)
  show ?case
  proof (cases "find (λ(x, y). {x, y} ∩ fv Q ≠ {}) xys")
    case None
    with 1(2-) show ?thesis
      using classes_intersect_find_not_None[of xys "fv Q"]
      by (cases xys) (simp_all add: Conjs_disjoint.simps)
  next
    case (Some xy)
    then obtain x y where xy: "xy = (x, y)" and xy_in: "(x, y) ∈ set xys"
      by (cases xy) (auto dest!: find_SomeD)
    with Some 1(4) have "sr (Conj Q (x ≈ y))"
      by (auto dest: find_SomeD simp: sr_Conj_eq)
    moreover from 1(2,3) have "∀V∈classes (set (remove1 (x, y) xys)). V ∩ fv (Conj Q (x ≈ y)) ≠ {}"
      by (subst (asm) insert_remove_id[OF xy_in], unfold classes_insert)
        (auto simp: class_None_eq class_Some_eq split: option.splits if_splits)
    ultimately show ?thesis
      using 1(2-) Some xy 1(1)[OF Some xy[symmetric]]
      by (simp add: Conjs_disjoint.simps)
  qed
qed

lemma sr_CONJ_disjoint:
  "inf 𝒬fin Q = {} ⟹ (Qfin, Qeq) ∈ 𝒬fin ⟹ finite Qeq ⟹ sr Qfin ⟹ sr (CONJ_disjoint (Qfin, Qeq))"
  unfolding inf_def disjointvars_def CONJ_disjoint_def prod.case
  by (drule arg_cong[of _ _ "λA. (Qfin, Qeq) ∈ A"], intro sr_cp sr_Conjs_disjoint)
    (auto simp only: mem_Collect_eq prod.case simp_thms distinct_sorted_list_of_set
       set_sorted_list_of_set SUP_bot_conv classes_nonempty split: if_splits)

lemma equiv_Conjs_cong: "Q ≜ Q' ⟹ Conjs Q xys ≜ Conjs Q' xys"
  by (induct Q xys arbitrary: Q' rule: Conjs.induct) auto

lemma Conjs_pull_out: "Conjs Q (xys @ (x, y) # xys') ≜ Conjs (Conj Q (x ≈ y)) (xys @ xys')"
  by (induct Q xys rule: Conjs.induct)
    (auto elim!: equiv_trans intro!: equiv_Conjs_cong intro: equiv_def[THEN iffD2])

lemma Conjs_reorder: "distinct xys ⟹ distinct xys' ⟹ set xys = set xys' ⟹ Conjs Q xys ≜ Conjs Q xys'"
proof (induct Q xys arbitrary: xys' rule: Conjs.induct)
  case (2 Q x y xys)
  from 2(4) obtain i where i: "i < length xys'" "xys' ! i = (x, y)"
    by (auto simp: set_eq_iff in_set_conv_nth)
  with 2(2-4) have *: "set xys = set (take i xys') ∪ set (drop (Suc i) xys')"
    by (subst (asm) (1 2) id_take_nth_drop[of i xys'])
      (auto simp: set_eq_iff dest: in_set_takeD in_set_dropD)
  from i 2(2,3) show ?case
    by (subst id_take_nth_drop[OF i(1)], subst (asm) (3) id_take_nth_drop[OF i(1)])
      (auto simp: * intro!: equiv_trans[OF _ Conjs_pull_out[THEN equiv_sym]] 2(1))
qed simp

lemma ex_Conjs_disjoint_eq_Conjs:
  "distinct xys ⟹ ∃xys'. distinct xys' ∧ set xys = set xys' ∧ Conjs_disjoint Q xys = Conjs Q xys'"
proof (induct Q xys rule: Conjs_disjoint.induct)
  case (1 Q xys)
  show ?case
  proof (cases "find (λ(x, y). {x, y} ∩ fv Q ≠ {}) xys")
    case None
    with 1(2) show ?thesis
      by (subst Conjs_disjoint.simps) (auto intro!: exI[of _ xys])
  next
    case (Some xy)
    with 1(1)[of xy "fst xy" "snd xy"] 1(2)
    obtain xys' where "distinct xys'"
      "set xys - {xy} = set xys'"
      "Conjs_disjoint (Conj Q (fst xy ≈ snd xy)) (remove1 xy xys) =
       Conjs (Conj Q (fst xy ≈ snd xy)) xys'"
      by auto
    with Some show ?thesis
      by (subst Conjs_disjoint.simps, intro exI[of _ "xy # xys'"])
        (auto simp: set_eq_iff dest: find_SomeD)
  qed
qed

lemma Conjs_disjoint_equiv_Conjs:
  assumes "distinct xys"
  shows "Conjs_disjoint Q xys ≜ Conjs Q xys"
proof -
  from assms obtain xys' where xys': "distinct xys'" "set xys = set xys'" and "Conjs_disjoint Q xys = Conjs Q xys'"
    using ex_Conjs_disjoint_eq_Conjs by blast
  note this(3)
  also have "… ≜ Conjs Q xys"
    by (intro Conjs_reorder xys' sym assms)
  finally show ?thesis
    by blast
qed

lemma infinite_eval_Conjs: "infinite (eval Q I) ⟹ leftfresh Q xys ⟹ infinite (eval (Conjs Q xys) I)"
proof (induct Q xys rule: Conjs.induct)
  case (2 Q x y xys)
  then show ?case
    unfolding Conjs.simps
    by (intro 2(1) infinite_eval_Conj) auto
qed simp

lemma leftfresh_fv_subset: "leftfresh Q xys ⟹ fv Q' ⊆ fv Q ⟹ leftfresh Q' xys"
  by (induct Q xys arbitrary: Q' rule: leftfresh.induct) (auto simp: subset_eq)

lemma fun_upds_map: "(∀x. x ∉ set ys ⟶ σ x = τ x) ⟹ σ[ys :=* map τ ys] = τ"
  by (induct ys arbitrary: σ) auto

lemma map_fun_upds: "length xs = length ys ⟹ distinct xs ⟹ map (σ[xs :=* ys]) xs = ys"
  by (induct xs ys arbitrary: σ rule: list_induct2) auto

lemma zip_map: "zip xs (map f xs) = map (λx. (x, f x)) xs"
  by (induct xs) auto

lemma filter_sorted_list_of_set:
  "finite B ⟹ A ⊆ B ⟹ filter (λx. x ∈ A) (sorted_list_of_set B) = sorted_list_of_set A"
proof (induct B arbitrary: A rule: finite_induct)
  case (insert x B)
  then have "finite A" by (auto simp: finite_subset)
  moreover
  from insert(1,2) have "filter (λy. y ∈ A - {x}) (sorted_list_of_set B) =
             filter (λx. x ∈ A) (sorted_list_of_set B)"
    by (intro filter_cong) auto
  ultimately  show ?case
    using insert(1,2,4) insert(3)[of "A - {x}"] sorted_list_of_set_insert_remove[of A x]
    by (cases "x ∈ A") (auto  simp: filter_insort filter_insort_triv subset_insert_iff insert_absorb)
qed simp

lemma infinite_eval_eval_on[rotated 2]:
  assumes "fv Q ⊆ X" "finite X"
  shows "infinite (eval Q I) ⟹ infinite (eval_on X Q I)"
proof (erule infinite_surj[of _ "λxs. map snd (filter (λ(x,_). x ∈ fv Q) (zip (sorted_list_of_set X) xs))"],
  unfold eval_deep_def Let_def, safe)
  fix xs σ
  assume len: "length (sorted_list_of_set (fv Q)) = length xs" and
    "sat Q I (σ[sorted_list_of_set (fv Q) :=* xs])" (is "sat Q I ?τ")
  moreover from assms len have "σ[sorted_list_of_set X :=* map ?τ (sorted_list_of_set X)] = ?τ"
    by (intro fun_upds_map) force
  ultimately show "xs ∈ (λxs. map snd (filter (λ(x, _). x ∈ fv Q) (zip (sorted_list_of_set X) xs))) `
    eval_on X Q I" using assms
    by (auto simp: eval_on_def image_iff zip_map filter_map o_def filter_sorted_list_of_set map_fun_upds
      intro!: exI[of _ "map (σ[sorted_list_of_set (fv Q) :=* xs]) (sorted_list_of_set X)"] exI[of _ σ])
qed

lemma infinite_eval_CONJ_disjoint:
  assumes "infinite (eval Q I)" "finite (adom I)" "fv Q ⊆ X" "Field Qeq ⊆ X" "finite X" "∃xys. distinct xys ∧ leftfresh Q xys ∧ set xys = Qeq"
  shows "infinite (eval_on X (CONJ_disjoint (Q, Qeq)) I)"
proof -
  from assms(6) obtain xys where "distinct xys" "leftfresh Q xys" "set xys = Qeq"
    by blast
  with assms(1-5) show ?thesis
    using infinite_eval_eval_on[OF infinite_eval_Conjs[of Q I xys], of X] equiv_eval_on_eqI[of I  "Conjs_disjoint Q (sorted_list_of_set Qeq)" "Conjs Q xys" X]
      equiv_trans[OF Conjs_disjoint_equiv_Conjs[of "sorted_list_of_set Qeq" Q] Conjs_reorder[of _ xys]]
      fv_Conjs[of Q xys]
    by (force simp: CONJ_disjoint_def subset_eq equiv_eval_on_eqI[OF _ equiv_cp])
qed

lemma sat_Conjs: "sat (Conjs Q xys) I σ ⟷ sat Q I σ ∧ (∀(x, y) ∈ set xys. sat (x ≈ y) I σ)"
  by (induct Q xys rule: Conjs.induct) auto

lemma sat_Conjs_disjoint: "sat (Conjs_disjoint Q xys) I σ ⟷ sat Q I σ ∧ (∀(x, y) ∈ set xys. sat (x ≈ y) I σ)"
proof (induct Q xys rule: Conjs_disjoint.induct)
  case (1 Q xys)
  then show ?case
    by (subst Conjs_disjoint.simps)
      (auto simp: sat_Conjs dest: find_SomeD(2) set_remove1_subset[THEN set_mp] in_set_remove_cases[rotated] split: option.splits)
qed

lemma sat_CONJ: "finite Qeq ⟹ sat (CONJ (Q, Qeq)) I σ ⟷ sat Q I σ ∧ (∀(x, y) ∈ Qeq. sat (x ≈ y) I σ)"
  unfolding CONJ_def by (auto simp: sat_Conjs)

lemma sat_CONJ_disjoint: "finite Qeq ⟹ sat (CONJ_disjoint (Q, Qeq)) I σ ⟷ sat Q I σ ∧ (∀(x, y) ∈ Qeq. sat (x ≈ y) I σ)"
  unfolding CONJ_disjoint_def by (auto simp: sat_Conjs_disjoint)

lemma Conjs_inject: "Conjs Q xys = Conjs Q' xys ⟷ Q = Q'"
  by (induct Q xys arbitrary: Q' rule: Conjs.induct) auto

lemma nonempty_disjointvars_infinite:
  assumes "disjointvars (Qfin :: ('a :: infinite, 'b) fmla) Qeq ≠ {}"
    "finite Qeq" "fv Qfin ∪ Field Qeq ⊆ X" "finite X" "sat Qfin I σ" "∀(x, y)∈Qeq. σ x = σ y"
  shows "infinite (eval_on X (CONJ_disjoint (Qfin, Qeq)) I)"
proof -
  from assms(1) obtain x V where xV: "V ∈ classes Qeq" "x ∈ V" "V ∩ fv Qfin = {}"
    by (auto simp: disjointvars_def)
  show ?thesis
  proof (rule infinite_surj[OF infinite_UNIV, of "λds. ds ! index (sorted_list_of_set X) x"], safe)
    fix z
    let ?ds = "map (λv. if v ∈ V then z else σ v) (sorted_list_of_set X)"
    from xV have "x ∈ Field Qeq"
      by (metis UnionI classes_cover)
    { fix a b
      assume *: "(a, b) ∈ Qeq"
      from this edge_same_class[OF xV(1) this] assms(3,6) have "a ∈ X" "b ∈ X" "a ∈ V ⟷ b ∈ V" "σ a = σ b"
        by (auto dest: FieldI1 FieldI2)
      with xV(1) assms(3,4) have "(σ[sorted_list_of_set X :=* ?ds]) a = (σ[sorted_list_of_set X :=* ?ds]) b"
        by (subst (1 2) fun_upds_in) auto
    }
    with assms(2-) xV  ‹x ∈ Field Qeq›
    show "z ∈ (λds. ds ! index (sorted_list_of_set X) x) ` eval_on X (CONJ_disjoint (Qfin, Qeq)) I"
      by (auto simp: eval_on_def CONJ_disjoint_def sat_Conjs_disjoint Let_def image_iff fun_upds_in subset_eq
         intro!: exI[of _ "map (λv. if v ∈ V then z else σ v) (sorted_list_of_set X)"] exI[of _ σ]
         elim!: sat_fv_cong[THEN iffD1, rotated -1])
  qed
qed

lemma EVAL'_EVAL: "EVAL' Q Qfin Qinf ⟹ FV Q Qfin Qinf ⟹ EVAL Q Qfin Qinf"
  unfolding EVAL_def EVAL'_def FV_def
  by (subst (2) eval_def) auto

lemma cpropagated_Conjs_disjoint:
  "distinct xys ⟹ irrefl (set xys) ⟹ ∀V∈classes (set xys). V ∩ fv Q ≠ {} ⟹ cpropagated Q ⟹ cpropagated (Conjs_disjoint Q xys)"
proof (induct Q xys rule: Conjs_disjoint.induct)
  case (1 Q xys)
  show ?case
  proof (cases "find (λ(x, y). {x, y} ∩ fv Q ≠ {}) xys")
    case None
    with 1(2-) show ?thesis
      using classes_intersect_find_not_None[of xys "fv Q"]
      by (cases xys) (simp_all add: Conjs_disjoint.simps)
  next
    case (Some xy)
    then obtain x y where xy: "xy = (x, y)" and xy_in: "(x, y) ∈ set xys"
      by (cases xy) (auto dest!: find_SomeD)
    with Some 1(3,5) have "cpropagated (Conj Q (x ≈ y))"
      by (auto dest: find_SomeD simp: cpropagated_def irrefl_def is_Bool_def)
    moreover from 1(2,4) have "∀V∈classes (set (remove1 (x, y) xys)). V ∩ fv (Conj Q (x ≈ y)) ≠ {}"
      by (subst (asm) insert_remove_id[OF xy_in], unfold classes_insert)
        (auto simp: class_None_eq class_Some_eq split: option.splits if_splits)
    moreover from 1(3) have "irrefl (set xys - {(x, y)})"
      by (auto simp: irrefl_def)
    ultimately show ?thesis
      using 1(2-) Some xy 1(1)[OF Some xy[symmetric]]
      by (simp add: Conjs_disjoint.simps)
  qed
qed

lemma (in simplification) simplified_Conjs_disjoint:
  "distinct xys ⟹ irrefl (set xys) ⟹ ∀V∈classes (set xys). V ∩ fv Q ≠ {} ⟹ simplified Q ⟹ simplified (Conjs_disjoint Q xys)"
proof (induct Q xys rule: Conjs_disjoint.induct)
  case (1 Q xys)
  show ?case
  proof (cases "find (λ(x, y). {x, y} ∩ fv Q ≠ {}) xys")
    case None
    with 1(2-) show ?thesis
      using classes_intersect_find_not_None[of xys "fv Q"]
      by (cases xys) (simp_all add: Conjs_disjoint.simps)
  next
    case (Some xy)
    then obtain x y where xy: "xy = (x, y)" and xy_in: "(x, y) ∈ set xys"
      by (cases xy) (auto dest!: find_SomeD)
    with Some 1(3,5) have "simplified (Conj Q (x ≈ y))"
      by (auto dest: find_SomeD simp: irrefl_def intro!: simplified_Conj_eq)
    moreover from 1(2,4) have "∀V∈classes (set (remove1 (x, y) xys)). V ∩ fv (Conj Q (x ≈ y)) ≠ {}"
      by (subst (asm) insert_remove_id[OF xy_in], unfold classes_insert)
        (auto simp: class_None_eq class_Some_eq split: option.splits if_splits)
    moreover from 1(3) have "irrefl (set xys - {(x, y)})"
      by (auto simp: irrefl_def)
    ultimately show ?thesis
      using 1(2-) Some xy 1(1)[OF Some xy[symmetric]]
      by (simp add: Conjs_disjoint.simps)
  qed
qed

lemma disjointvars_empty_iff: "disjointvars Q Qeq = {} ⟷ (∀V∈classes Qeq. V ∩ fv Q ≠ {})"
  unfolding disjointvars_def UNION_empty_conv
  using classes_nonempty by auto

lemma cpropagated_CONJ_disjoint:
  "finite Qeq ⟹ irrefl Qeq ⟹ disjointvars Q Qeq = {} ⟹ cpropagated Q ⟹ cpropagated (CONJ_disjoint (Q, Qeq))"
  unfolding CONJ_disjoint_def prod.case disjointvars_empty_iff
  by (rule cpropagated_Conjs_disjoint) auto

lemma (in simplification) simplified_CONJ_disjoint:
  "finite Qeq ⟹ irrefl Qeq ⟹ disjointvars Q Qeq = {} ⟹ simplified Q ⟹ simplified (CONJ_disjoint (Q, Qeq))"
  unfolding CONJ_disjoint_def prod.case disjointvars_empty_iff
  by (rule simplified_Conjs_disjoint) auto

lemma (in simplification) split_INV1_init:
  "rrb Q' ⟹ simplified Q' ⟹ Q ≜ Q' ⟹ fv Q' ⊆ fv Q ⟹ split_INV1 Q ({(Q', {})}, {})"
  by (auto simp add: split_INV1_def wf_state_def assemble_def FV_def EVAL'_def eval_def[symmetric] eval_simp_False irrefl_def
    sat_simp equiv_def intro!: equiv_eval_on_eval_eqI del: equalityI dest: fv_simp[THEN set_mp] split: prod.splits)

lemma (in simplification) split_INV1_I:
  "wf_state Q rrb (𝒬fin, 𝒬inf) ⟹ EVAL' Q (simp (DISJ (CONJ_disjoint ` 𝒬fin))) (simp (DISJ (close ` 𝒬inf))) ⟹
    split_INV1 Q (𝒬fin, 𝒬inf)"
  unfolding split_INV1_def assemble_def by auto

lemma EVAL'_I: 
  "(⋀I. finite (adom I) ⟹ eval Qinf I = {} ⟹ eval_on (fv Q) Qfin I = eval Q I) ⟹
   (⋀I. finite (adom I) ⟹ eval Qinf I ≠ {} ⟹ infinite (eval Q I)) ⟹ EVAL' Q Qfin Qinf"
  unfolding EVAL'_def by auto

lemma (in simplification) wf_state_Un:
  "wf_state Q P (𝒬fin, 𝒬inf) ⟹ wf_state Q P (insert Qpair 𝒬new, {Q'}) ⟹
   wf_state Q P (insert Qpair (𝒬fin ∪ 𝒬new), insert Q' 𝒬inf)"
  by (auto simp: wf_state_def)

lemma (in simplification) wf_state_Diff:
  "wf_state Q P (𝒬fin, 𝒬inf) ⟹ wf_state Q P (𝒬fin - 𝒬new, 𝒬inf)"
  by (auto simp: wf_state_def)

lemma (in simplification) split_INV1_step:
  assumes "split_INV1 Q (𝒬fin, 𝒬inf)" "(Qfin, Qeq) ∈ fixfree 𝒬fin" "x ∈ nongens Qfin" "cov x Qfin G"
  shows "split_INV1 Q
    (insert (simp (Conj Qfin (DISJ (qps G))), Qeq)
      (𝒬fin - {(Qfin, Qeq)} ∪ (λy. (cp (Qfin[x → y]), insert (x, y) Qeq)) ` eqs x G),
    insert (cp (Qfin ⊥ x)) 𝒬inf)"
    (is "split_INV1 Q (?Qfin, ?Qinf)")
proof (intro split_INV1_I EVAL'_I, goal_cases wf fin inf)
  case wf
  from assms(1) have wf: "wf_state Q rrb (𝒬fin, 𝒬inf)"
    by (auto simp: split_INV1_def)
  with assms(2,3) obtain xys where *:
    "x ∈ fv Qfin" "(Qfin, Qeq) ∈ 𝒬fin" "finite 𝒬fin" "finite Qeq" "finite 𝒬inf" "fv Qfin ⊆ fv Q" "Field Qeq ⊆ fv Q"
    "distinct xys" "leftfresh Qfin xys" "set xys = Qeq" "rrb Qfin" "irrefl Qeq"
    by (auto simp: fixfree_def nongens_def wf_state_def)
  moreover from * have "∃xs. leftfresh (simp (Conj Qfin (DISJ (qps G)))) xs ∧ distinct xs ∧ set xs = set xys"
    using cov_fv[OF assms(4) _ qps_in] assms(4)
    by (intro exI[of _ xys])
      (force elim!: leftfresh_fv_subset dest!: fv_simp[THEN set_mp] fv_DISJ[THEN set_mp, rotated 1])
  moreover from * have "∃xs. leftfresh (cp (Qfin[x → z])) xs ∧ distinct xs ∧ set xs = insert (x, z) (set xys)"
    if "z ∈ eqs x G" for z
    using cov_fv[OF assms(4) _ eqs_in, of z x] assms(4) that
    by (intro exI[of _ "if (x, z) ∈ set xys then xys else (x, z) # xys"])
      (auto simp: fv_subst dest!: fv_cp[THEN set_mp] elim!: leftfresh_fv_subset)
  ultimately show ?case
    using cov_fv[OF assms(4) _ qps_in] cov_fv[OF assms(4) _ eqs_in] assms(4)
    by (intro wf_state_Un wf_state_Diff wf)
      (auto simp: wf_state_def rrb_simp simplified_simp simplified_cp rrb_cp_subst fv_subst
      subset_eq irrefl_def
      dest!: fv_cp[THEN set_mp] fv_simp[THEN set_mp] fv_DISJ[THEN set_mp, rotated 1])
next
  case (fin I)
  note eq = trans[OF sat_simp sat_DISJ, symmetric]
  from assms have *:
    "x ∈ fv Qfin" "(Qfin, Qeq) ∈ 𝒬fin" "fv Qfin ⊆ fv Q" "Field Qeq ⊆ fv Q" and
    finite[simp]: "finite 𝒬fin" "finite Qeq" "finite 𝒬inf"
    by (auto simp: split_INV1_def fixfree_def nongens_def wf_state_def)
  with fin have unsat: "∀σ. ¬ sat (Qfin ⊥ x) I σ" and "∀x∈𝒬inf. ∀σ. ¬ sat x I σ"
    by (auto simp: eval_empty_close eval_simp_DISJ_closed)
  with fin(1) assms(1) * have "eval_on (fv Q) (simp (DISJ (CONJ_disjoint ` 𝒬fin))) I = eval Q I"
    unfolding split_INV1_def Let_def assemble_def prod.case EVAL'_def
    by (auto simp: eval_empty_close eval_simp_DISJ_closed)
  with assms(4) show ?case
  proof (elim trans[rotated], intro eval_on_cong box_equals[OF _ eq eq])
    fix σ
    from * have "(∃Q∈𝒬fin. sat (CONJ_disjoint Q) I σ) ⟷
        sat (CONJ_disjoint (Qfin, Qeq)) I σ ∨ (∃Q∈𝒬fin - {(Qfin, Qeq)}. sat (CONJ_disjoint Q) I σ)"
      using assms(4) by (auto simp: fixfree_def)
    also have "sat (CONJ_disjoint (Qfin, Qeq)) I σ ⟷
        sat (CONJ_disjoint (simp (Conj Qfin (DISJ (qps G))), Qeq)) I σ ∨
        (∃Q∈(λy. (cp (Qfin[x → y]), insert (x, y) Qeq)) ` eqs x G. sat (CONJ_disjoint Q) I σ)"
      using cov_sat_fin[of x Qfin G I σ] assms(3,4) fin(1) unsat
      by (auto simp: eval_empty_close sat_CONJ_disjoint nongens_def)
    finally show "(∃Q∈CONJ_disjoint ` ?Qfin. sat Q I σ) ⟷ (∃Q∈CONJ_disjoint ` 𝒬fin. sat Q I σ)"
      by auto
  qed simp_all
next
  case (inf I)
  from assms have *:
    "x ∈ fv Qfin" "(Qfin, Qeq) ∈ 𝒬fin" "finite 𝒬fin" "finite Qeq" "finite 𝒬inf" "fv Qfin ⊆ fv Q" "Field Qeq ⊆ fv Q"
    "∃xys. distinct xys ∧ leftfresh Qfin xys ∧ set xys = Qeq"
    by (auto simp: split_INV1_def fixfree_def nongens_def wf_state_def)
  with inf obtain σ where "sat (Qfin ⊥ x) I σ ∨ (∃Q ∈ 𝒬inf. sat Q I σ)"
    by (subst (asm) eval_simp_DISJ_closed) (auto simp: eval_empty_close sat_CONJ simp del: fv_CONJ)
  then show ?case
  proof (elim disjE)
    assume "sat (Qfin ⊥ x) I σ"
    then have "infinite (eval Qfin I)"
      by (rule cov_eval_inf[OF assms(4) *(1) inf(1)])
    then have "infinite (eval_on (fv Q) (CONJ_disjoint (Qfin, Qeq)) I)"
      by (rule infinite_eval_CONJ_disjoint[OF _ inf(1) *(6,7) _ *(8)]) simp
    with * have "infinite (eval_on (fv Q) (simp (DISJ (CONJ_disjoint ` 𝒬fin))) I)"
      by (elim infinite_Implies_mono_on[rotated 3]) (auto simp: sat_simp)
    with inf assms(1) show ?case
      by (auto simp: split_INV1_def assemble_def EVAL'_def split: if_splits)
  next
    assume "∃Q∈𝒬inf. sat Q I σ"
    with inf(1) assms(1) * show ?case
      by (auto simp: split_INV1_def assemble_def EVAL'_def eval_simp_DISJ_closed eval_empty_close
          split: if_splits)
  qed
qed

lemma (in simplification) split_INV1_decreases:
  assumes "split_INV1 Q (𝒬fin, 𝒬inf)" "(Qfin, Qeq) ∈ fixfree 𝒬fin" "x ∈ nongens Qfin" "cov x Qfin G"
  shows "((nongens ∘ fst) `# mset_set (insert (simp (Conj Qfin (DISJ (qps G))), Qeq) (𝒬fin - {(Qfin, Qeq)} ∪ (λy. (cp (Qfin[x → y]), insert (x, y) Qeq)) ` eqs x G)),
          (nongens ∘ fst) `# mset_set 𝒬fin) ∈ mult {(X, Y). X ⊂ Y ∧ Y ⊆ fv Q}"
  using assms by (intro split_step_in_mult) (auto simp: fixfree_def split_INV1_def wf_state_def)

lemma (in simplification) split_INV2_init:
  "split_INV1 Q (𝒬fin, 𝒬inf) ⟹ fixfree 𝒬fin = {} ⟹ split_INV2 Q (𝒬fin, 𝒬inf)"
  by (auto simp: split_INV1_def split_INV2_def wf_state_def sr_def fixfree_def)

lemma (in simplification) split_INV2_I:
  "wf_state Q sr (𝒬fin, 𝒬inf) ⟹ EVAL' Q (simp (DISJ (CONJ_disjoint ` 𝒬fin))) (simp (DISJ (close ` 𝒬inf))) ⟹
    split_INV2 Q (𝒬fin, 𝒬inf)"
  unfolding split_INV2_def assemble_def by auto

lemma (in simplification) split_INV2_step:
  assumes "split_INV2 Q (𝒬fin, 𝒬inf)" "(Qfin, Qeq) ∈ inf 𝒬fin Q"
  shows "split_INV2 Q (𝒬fin - {(Qfin, Qeq)}, insert (CONJ (Qfin, Qeq)) 𝒬inf)"
proof (intro split_INV2_I EVAL'_I, goal_cases wf fin inf)
  case wf
  with assms(1) show ?case 
    by (auto simp: split_INV2_def wf_state_def)
next
  case (fin I)
  with assms have finite[simp]: "finite 𝒬fin" "finite Qeq" and
    unsat: "⋀σ. ¬ sat (CONJ (Qfin, Qeq)) I σ" and
    eval: "eval_on (fv Q) (simp (DISJ (CONJ_disjoint ` 𝒬fin))) I = eval Q I"
    by (auto simp: split_INV2_def inf_def wf_state_def assemble_def EVAL'_def eval_simp_DISJ_closed eval_empty_close)
  from eval show ?case
  proof (elim trans[rotated], unfold eval_on_simp, intro eval_DISJ_prune_unsat ballI allI; (elim DiffE imageE; hypsubst_thin)?)
    fix Qpair σ
    assume "Qpair ∈ 𝒬fin" "CONJ_disjoint Qpair ∉ CONJ_disjoint ` (𝒬fin - {(Qfin, Qeq)})"
    with unsat[of σ] show "¬ sat (CONJ_disjoint Qpair) I σ"
      by (cases "Qeq = snd Qpair"; cases Qpair) (auto simp: sat_CONJ_disjoint sat_CONJ)
  qed auto
next
  case (inf I)
  from assms have *:
    "(Qfin, Qeq) ∈ 𝒬fin" "finite 𝒬fin" "finite Qeq" "finite 𝒬inf" "fv Qfin ⊆ fv Q" "Field Qeq ⊆ fv Q"
    by (auto simp: split_INV2_def inf_def wf_state_def)
  with inf obtain σ where "sat Qfin I σ ∧ (∀(x, y) ∈ Qeq. σ x = σ y) ∨ (∃Q ∈ 𝒬inf. sat Q I σ)"
    by (subst (asm) eval_simp_DISJ_closed) (auto simp: eval_empty_close sat_CONJ simp del: fv_CONJ)
  then show ?case
  proof (elim disjE conjE)
    assume "sat Qfin I σ" "∀(x, y) ∈ Qeq. σ x = σ y"
    with assms * have "infinite (eval_on (fv Q) (CONJ_disjoint (Qfin, Qeq)) I)"
      using nonempty_disjointvars_infinite[of Qfin Qeq "fv Q" I σ]
        infinite_eval_on_extra_variables[of "fv Q" "CONJ_disjoint (Qfin, Qeq)" I, OF _ _ exI, of σ]
      by (cases "fv (CONJ_disjoint (Qfin, Qeq)) ⊂ fv Q") (auto simp: inf_def sat_CONJ sat_CONJ_disjoint)
    with * have "infinite (eval_on (fv Q) (simp (DISJ (CONJ_disjoint ` 𝒬fin))) I)"
      by (elim infinite_Implies_mono_on[rotated 3]) (auto simp: sat_simp)
    with inf assms(1) show ?case
      by (auto simp: split_INV2_def assemble_def EVAL'_def split: if_splits)
  next
    assume "∃Q ∈ 𝒬inf. sat Q I σ"
    with inf(1) assms(1) * show "infinite (eval Q I)"
      by (auto simp: split_INV2_def assemble_def EVAL'_def eval_simp_DISJ_closed eval_empty_close
        split: if_splits)
  qed
qed

lemma (in simplification) split_INV2_decreases:
  "split_INV2 Q (𝒬fin, 𝒬inf) ⟹ (Qfin, Qeq) ∈ Restrict_Frees.inf 𝒬fin Q ⟹ card (𝒬fin - {(Qfin, Qeq)}) < card 𝒬fin"
  by (rule psubset_card_mono) (auto simp: inf_def split_INV2_def wf_state_def)

lemma (in simplification) split_INV2_stop_fin_sr:
  "inf 𝒬fin Q = {} ⟹ split_INV2 Q (𝒬fin, 𝒬inf) ⟹ assemble (𝒬fin, 𝒬inf) = (Qfin, Qinf) ⟹ sr Qfin"
  by (auto 0 4 simp: split_INV2_def assemble_def wf_state_def inf_def
    intro!: sr_simp sr_DISJ[of _ "fv Q"] sr_CONJ_disjoint[of 𝒬fin Q])

lemma (in simplification) split_INV2_stop_inf_sr:
  "split_INV2 Q (𝒬fin, 𝒬inf) ⟹ assemble (𝒬fin, 𝒬inf) = (Qfin, Qinf) ⟹ fv Q' ⊆ fv Qinf ⟹ rrb Q' ⟹ sr Q'"
  using fv_DISJ_close[of 𝒬inf] fv_simp[of "DISJ (close ` 𝒬inf)"]
  by (auto simp: split_INV2_def assemble_def wf_state_def sr_def nongens_def)

lemma (in simplification) split_INV2_stop_FV:
  assumes "fv Q' ⊆ fv Qinf" "inf 𝒬fin Q = {}" "split_INV2 Q (𝒬fin, 𝒬inf)" "assemble (𝒬fin, 𝒬inf) = (Qfin, Qinf)"
  shows "FV Q Qfin Q'"
proof -
  have "simplified Q'" "fv Q' = fv Q" if "Q' ∈ CONJ_disjoint ` 𝒬fin" for Q'
    using that assms(2,3)
    by (auto simp: split_INV2_def wf_state_def inf_def simplified_CONJ_disjoint)
  with assms(1,3,4) show ?thesis
    using fv_simp_DISJ_eq[of "CONJ_disjoint ` 𝒬fin" "fv Q"] fv_DISJ_close[of 𝒬inf] fv_simp[of "DISJ (close ` 𝒬inf)"]
    by (auto simp: split_INV2_def assemble_def wf_state_def FV_def)
qed

lemma (in simplification) split_INV2_stop_EVAL:
  assumes "fv Q' ⊆ fv Qinf" "inf 𝒬fin Q = {}" "split_INV2 Q (𝒬fin, 𝒬inf)" "assemble (𝒬fin, 𝒬inf) = (Qfin, Qinf)" "Qinf ≜ Q'"
  shows "EVAL Q Qfin Q'"
proof -
  have "simplified Q'" "fv Q' = fv Q" if "Q' ∈ CONJ_disjoint ` 𝒬fin" for Q'
    using that assms(2,3)
    by (auto simp: split_INV2_def wf_state_def inf_def simplified_CONJ_disjoint)
  with assms(1,3,4,5) show ?thesis
    using fv_simp_DISJ_eq[of "CONJ_disjoint ` 𝒬fin" "fv Q"] fv_DISJ_close[of 𝒬inf] fv_simp[of "DISJ (close ` 𝒬inf)"]
    by (auto simp: split_INV2_def assemble_def wf_state_def sr_def EVAL'_cong FV_def elim!: EVAL'_EVAL)
qed

lemma (in simplification) simplified_assemble:
  "assemble (𝒬fin, 𝒬inf) = (Qfin, Qinf) ⟹ simplified Qfin"
  by (auto simp: assemble_def simplified_simp)

lemma (in simplification) split_correct:
  notes cp.simps[simp del]
  shows "split Q ≤ split_spec Q"
  unfolding split_def split_spec_def Let_def
  by (refine_vcg rb_correct[THEN order_trans, unfolded rb_spec_def]
      WHILEIT_rule[where I="split_INV1 Q" and R="inv_image (mult {(X, Y). X ⊂ Y ∧ Y ⊆ fv Q}) (image_mset (nongens o fst) o mset_set o fst)"]
      WHILEIT_rule[where I="split_INV2 Q" and R="measure (λ(𝒬fin, _). card 𝒬fin)"])
    (auto simp: wf_mult finite_subset_wf split_step_in_mult
      conj_disj_distribR ex_disj_distrib card_gt_0_iff image_image image_Un
      insert_commute ac_simps UNION_singleton_eq_range simplified_assemble
      split_INV1_init split_INV1_step split_INV1_decreases
      split_INV2_init split_INV2_step split_INV2_decreases
      split_INV2_stop_fin_sr split_INV2_stop_inf_sr split_INV2_stop_FV split_INV2_stop_EVAL)

(*<*)
end
(*>*)