(*<*) 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 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 (*>*)