# 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 ← WHILE⇩T⇗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 ← WHILE⇩T⇗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.mult⇩D⇩M[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
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]]
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]]
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]]
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
(*>*)
```