# Theory Restrict_Frees_Impl

```(*<*)
theory Restrict_Frees_Impl
imports
Restrict_Bounds_Impl
Restrict_Frees
begin
(*>*)

section ‹Refining the Non-Deterministic @{term simplification.split} Function›

definition "fixfree_impl 𝒬 = map (apsnd set) (filter (λ(Q, _ :: (nat × nat) list). ∃x ∈ fv Q. gen_impl x Q = [])
(sorted_list_of_set ((apsnd sorted_list_of_set) ` 𝒬)))"

definition "nongens_impl Q = filter (λx. gen_impl x Q = []) (sorted_list_of_set (fv Q))"

lemma set_nongens_impl: "set (nongens_impl Q) = nongens Q"
by (auto simp: nongens_def nongens_impl_def set_gen_impl simp flip: List.set_empty)

lemma set_fixfree_impl: "finite 𝒬 ⟹ ∀(_, Qeq) ∈ 𝒬. finite Qeq ⟹ set (fixfree_impl 𝒬) = fixfree 𝒬"
by (fastforce simp: fixfree_def nongens_def fixfree_impl_def set_gen_impl image_iff apsnd_def map_prod_def
simp flip: List.set_empty split: prod.splits intro: exI[of _ "sorted_list_of_set _"])

lemma fixfree_empty_iff: "finite 𝒬 ⟹ ∀(_, Qeq) ∈ 𝒬. finite Qeq ⟹ fixfree 𝒬 ≠ {} ⟷ fixfree_impl 𝒬 ≠ []"
by (auto simp: set_fixfree_impl dest: arg_cong[of _ _ set] simp flip: List.set_empty)

definition "inf_impl 𝒬fin Q =
map (apsnd set) (filter (λ(Qfix, xys). disjointvars Qfix (set xys) ≠ {} ∨ fv Qfix ∪ Field (set xys) ≠ fv Q)
(sorted_list_of_set ((apsnd sorted_list_of_set) ` 𝒬fin)))"

lemma set_inf_impl: "finite 𝒬fin ⟹ ∀(_, Qeq) ∈ 𝒬fin. finite Qeq ⟹ set (inf_impl 𝒬fin Q) = inf 𝒬fin Q"
by (fastforce simp: inf_def inf_impl_def image_iff)

lemma inf_empty_iff: "finite 𝒬fin ⟹ ∀(_, Qeq) ∈ 𝒬fin. finite Qeq ⟹ inf 𝒬fin Q ≠ {} ⟷ inf_impl 𝒬fin Q ≠ []"
by (auto simp: set_inf_impl dest: arg_cong[of _ _ set] simp flip: List.set_empty)

definition (in simplification) split_impl :: "('a :: {infinite, linorder}, 'b :: linorder) fmla ⇒ (('a, 'b) fmla × ('a, 'b) fmla) nres" where
"split_impl Q = do {
Q' ← rb_impl Q;
𝒬pair ← WHILE
(λ(𝒬fin, _). fixfree_impl 𝒬fin ≠ []) (λ(𝒬fin, 𝒬inf). do {
(Qfix, Qeq) ← RETURN (hd (fixfree_impl 𝒬fin));
x ← RETURN (hd (nongens_impl Qfix));
G ← RETURN (hd (cov_impl 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
(λ(𝒬fin, _). inf_impl 𝒬fin Q ≠ []) (λ(𝒬fin, 𝒬inf). do {
Qpair ← RETURN (hd (inf_impl 𝒬fin Q));
let 𝒬fin = 𝒬fin - {Qpair};
let 𝒬inf = 𝒬inf ∪ {CONJ Qpair};
RETURN (𝒬fin, 𝒬inf)})
𝒬pair;
let (Qfin, Qinf) = assemble 𝒬pair;
Qinf ← rb_impl Qinf;
RETURN (Qfin, Qinf)}"

lemma (in simplification) split_INV2_imp_split_INV1: "split_INV2 Q 𝒬pair ⟹ split_INV1 Q 𝒬pair"
unfolding split_INV1_def split_INV2_def wf_state_def sr_def by auto

lemma hd_fixfree_impl_props:
assumes "finite 𝒬" "∀(_, Qeq) ∈ 𝒬. finite Qeq" "fixfree_impl 𝒬 ≠ []"
shows "hd (fixfree_impl 𝒬) ∈ 𝒬" "nongens (fst (hd (fixfree_impl 𝒬))) ≠ {}"
proof -
from hd_in_set[of "fixfree_impl 𝒬"] assms(3) have "hd (fixfree_impl 𝒬) ∈ set (fixfree_impl 𝒬)"
by blast
then have "hd (fixfree_impl 𝒬) ∈ fixfree 𝒬"
by (auto simp: set_fixfree_impl assms(1,2))
then show "hd (fixfree_impl 𝒬) ∈ 𝒬" "nongens (fst (hd (fixfree_impl 𝒬))) ≠ {}"
unfolding fixfree_def by auto
qed

lemma (in simplification) split_impl_refines_split: "split_impl Q ≤ split Q"
apply (unfold split_def split_impl_def Let_def)
supply rb_impl_refines_rb[refine_mono]
apply refine_mono
apply (rule order_trans[OF WHILE_le_WHILEI[where I="split_INV1 Q"]])
apply (rule order_trans[OF WHILEI_le_WHILEIT])
apply (rule WHILEIT_refine[OF _ _ _ refine_IdI, THEN refine_IdD])
apply (simp_all only: pair_in_Id_conv split: prod.splits) [4]
apply (intro allI impI, hypsubst_thin)
apply (subst fixfree_empty_iff; auto simp: split_INV1_def wf_state_def)
apply (intro allI impI, simp only: prod.inject, elim conjE, hypsubst_thin)
apply refine_mono
apply (subst set_fixfree_impl[symmetric]; auto simp: split_INV1_def wf_state_def intro!: hd_in_set)
apply clarsimp
subgoal for Q' 𝒬fin 𝒬inf Qfix Qeq Qfix' Qeq'
using hd_fixfree_impl_props(2)[of 𝒬fin]
by (force simp: split_INV1_def wf_state_def set_nongens_impl[symmetric] dest!: sym[of "(Qfix', _)"] intro!: hd_in_set)
apply clarsimp
subgoal for Q' 𝒬fin 𝒬inf Qfix Qeq Qfix' Qeq'
apply (intro RETURN_rule cov_impl_cov hd_in_set rrb_cov_impl)
using hd_fixfree_impl_props(1)[of 𝒬fin]
by (force simp: split_INV1_def wf_state_def dest!: sym[of "(Qfix', _)"])
apply (rule order_trans[OF WHILE_le_WHILEI[where I="split_INV1 Q"]])
apply (rule order_trans[OF WHILEI_le_WHILEIT])
apply (rule WHILEIT_refine[OF _ _ _ refine_IdI, THEN refine_IdD])
apply (simp_all only: pair_in_Id_conv split_INV2_imp_split_INV1 split: prod.splits) [4]
apply (intro allI impI, simp only: prod.inject, elim conjE, hypsubst_thin)
apply (subst inf_empty_iff; auto simp: split_INV2_def wf_state_def)
apply (intro allI impI, simp only: prod.inject, elim conjE, hypsubst_thin)
apply refine_mono
apply (subst set_inf_impl[symmetric]; auto simp: split_INV2_def wf_state_def intro!: hd_in_set)
done

definition (in simplification) split_impl_det :: "('a :: {infinite, linorder}, 'b :: linorder) fmla ⇒ (('a, 'b) fmla × ('a, 'b) fmla) dres" where
"split_impl_det Q = do {
Q' ← rb_impl_det Q;
𝒬pair ← dWHILE
(λ(𝒬fin, _). fixfree_impl 𝒬fin ≠ []) (λ(𝒬fin, 𝒬inf). do {
(Qfix, Qeq) ← dRETURN (hd (fixfree_impl 𝒬fin));
x ← dRETURN (hd (nongens_impl Qfix));
G ← dRETURN (hd (cov_impl 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)};
dRETURN (𝒬fin, 𝒬inf)})
({(Q', {})}, {});
𝒬pair ← dWHILE
(λ(𝒬fin, _). inf_impl 𝒬fin Q ≠ []) (λ(𝒬fin, 𝒬inf). do {
Qpair ← dRETURN (hd (inf_impl 𝒬fin Q));
let 𝒬fin = 𝒬fin - {Qpair};
let 𝒬inf = 𝒬inf ∪ {CONJ Qpair};
dRETURN (𝒬fin, 𝒬inf)})
𝒬pair;
let (Qfin, Qinf) = assemble 𝒬pair;
Qinf ← rb_impl_det Qinf;
dRETURN (Qfin, Qinf)}"

lemma (in simplification) split_impl_det_refines_split_impl: "nres_of (split_impl_det Q) ≤ split_impl Q"
unfolding split_impl_def split_impl_det_def Let_def
by (refine_transfer rb_impl_det_refines_rb_impl)

lemmas (in simplification) SPLIT_correct =
split_impl_det_refines_split_impl[THEN order_trans, OF
split_impl_refines_split[THEN order_trans, OF
split_correct]]

(*<*)
end
(*>*)```