# Theory Restrict_Bounds_Impl

```(*<*)
theory Restrict_Bounds_Impl
imports Restrict_Bounds
begin
(*>*)

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

fun gen_size where
"gen_size (Bool b) = 1"
| "gen_size (Eq x t) = 1"
| "gen_size (Pred p ts) = 1"
| "gen_size (Neg (Neg Q)) = Suc (gen_size Q)"
| "gen_size (Neg (Conj Q1 Q2)) = Suc (Suc (gen_size (Neg Q1) + gen_size (Neg Q2)))"
| "gen_size (Neg (Disj Q1 Q2)) = Suc (Suc (gen_size (Neg Q1) + gen_size (Neg Q2)))"
| "gen_size (Neg Q) = Suc (gen_size Q)"
| "gen_size (Conj Q1 Q2) = Suc (gen_size Q1 + gen_size Q2)"
| "gen_size (Disj Q1 Q2) = Suc (gen_size Q1 + gen_size Q2)"
| "gen_size (Exists x Q) = Suc (gen_size Q)"

function (sequential) gen_impl where
"gen_impl x (Bool False) = [{}]"
| "gen_impl x (Bool True) = []"
| "gen_impl x (Eq y (Const c)) = (if x = y then [{Eq y (Const c)}] else [])"
| "gen_impl x (Eq y (Var z)) = []"
| "gen_impl x (Pred p ts) = (if x ∈ fv_terms_set ts then [{Pred p ts}] else [])"
| "gen_impl x (Neg (Neg Q)) = gen_impl x Q"
| "gen_impl x (Neg (Conj Q1 Q2)) = gen_impl x (Disj (Neg Q1) (Neg Q2))"
| "gen_impl x (Neg (Disj Q1 Q2)) = gen_impl x (Conj (Neg Q1) (Neg Q2))"
| "gen_impl x (Neg _) = []"
| "gen_impl x (Disj Q1 Q2) =  [G1 ∪ G2. G1 ← gen_impl x Q1, G2 ← gen_impl x Q2]"
| "gen_impl x (Conj Q1 (y ≈ z)) = (if x = y then List.union (gen_impl x Q1) (map (image (λQ. cp (Q[z ❙→ x]))) (gen_impl z Q1))
else if x = z then List.union (gen_impl x Q1) (map (image (λQ. cp (Q[y ❙→ x]))) (gen_impl y Q1))
else gen_impl x Q1)"|
"gen_impl x (Conj Q1 Q2) = List.union (gen_impl x Q1) (gen_impl x Q2)"
| "gen_impl x (Exists y Q) = (if x = y then [] else map (image (exists y)) (gen_impl x Q))"
by pat_completeness auto
termination by (relation "measure (λ(x, Q). gen_size Q)") simp_all

lemma gen_impl_gen: "G ∈ set (gen_impl x Q) ⟹ gen x Q G"
by (induct x Q arbitrary: G rule: gen_impl.induct)
(auto 5 2 simp: fv_terms_set_def intro: gen.intros simp: image_iff split: if_splits)

lemma gen_gen_impl: "gen x Q G ⟹ G ∈ set (gen_impl x Q)"
proof (induct x Q G rule: gen.induct)
case (7 x Q1 G Q2)
then show ?case
proof (cases Q2)
case (Eq x t)
with 7 show ?thesis
by (cases t) auto
qed auto
qed (auto elim!: ap.cases simp: image_iff)

lemma set_gen_impl: "set (gen_impl x Q) = {G. gen x Q G}"
by (auto simp: gen_impl_gen gen_gen_impl)

definition "flat xss = fold List.union xss []"

(*much faster than fun*)
primrec cov_impl where
"cov_impl x (Bool b) = [{}]"
| "cov_impl x (Eq y t) = (case t of
Const c ⇒ [if x = y then {Eq y (Const c)} else {}]
| Var z ⇒ [if x = y ∧ x ≠ z then {x ≈ z}
else if x = z ∧ x ≠ y then {x ≈ y}
else {}])"
| "cov_impl x (Pred p ts) = [if x ∈ fv_terms_set ts then {Pred p ts} else {}]"
| "cov_impl x (Neg Q) = cov_impl x Q"
| "cov_impl x (Disj Q1 Q2) = (case (cp (Q1 ❙⊥ x), cp (Q2 ❙⊥ x)) of
(Bool True, Bool True) ⇒ List.union (cov_impl x Q1) (cov_impl x Q2)
| (Bool True, _) ⇒ cov_impl x Q1
| (_, Bool True) ⇒ cov_impl x Q2
| (_, _) ⇒ [G1 ∪ G2. G1 ← cov_impl x Q1, G2 ← cov_impl x Q2])"
| "cov_impl x (Conj Q1 Q2) = (case (cp (Q1 ❙⊥ x), cp (Q2 ❙⊥ x)) of
(Bool False, Bool False) ⇒ List.union (cov_impl x Q1) (cov_impl x Q2)
| (Bool False, _) ⇒ cov_impl x Q1
| (_, Bool False) ⇒ cov_impl x Q2
| (_, _) ⇒ [G1 ∪ G2. G1 ← cov_impl x Q1, G2 ← cov_impl x Q2])"
| "cov_impl x (Exists y Q) = (if x = y then [{}] else flat (map (λG.
(if x ≈ y ∈ G then [exists y ` (G - {x ≈ y}) ∪ (λQ. cp (Q[y ❙→ x])) ` G'. G' ← gen_impl y Q]
else [exists y ` G])) (cov_impl x Q)))"

lemma union_empty_iff: "List.union xs ys = [] ⟷ xs = [] ∧ ys = []"
by (induct xs arbitrary: ys) (force simp: List.union_def List.insert_def)+

lemma fold_union_empty_iff: "fold List.union xss ys = [] ⟷ (∀xs ∈ set xss. xs = []) ∧ ys = []"
by (induct xss arbitrary: ys) (auto simp: union_empty_iff)

lemma flat_empty_iff: "flat xss = [] ⟷ (∀xs ∈ set xss. xs = [])"
by (auto simp: flat_def fold_union_empty_iff)

lemma set_fold_union: "set (fold List.union xss ys) = (⋃ (set ` set xss)) ∪ set ys"
by (induct xss arbitrary: ys) auto

lemma set_flat: "set (flat xss) = ⋃ (set ` set xss)"
unfolding flat_def by (auto simp: set_fold_union)

lemma rrb_cov_impl: "rrb Q ⟹ cov_impl x Q ≠ []"
proof (induct Q arbitrary: x)
case (Exists y Q)
then show ?case
by (cases "∃G ∈ set (cov_impl x Q). x ≈ y ∈ G")
(auto simp: flat_empty_iff image_iff dest: gen_gen_impl intro!: UnI1 bexI[rotated])
qed (auto split: term.splits fmla.splits bool.splits simp: union_empty_iff)

lemma cov_Eq_self: "cov x (y ≈ y) {}"
by (metis Un_absorb cov.Eq_self cov.nonfree fv.simps(3) fv_term_set.simps(1) singletonD)

lemma cov_impl_cov: "G ∈ set (cov_impl x Q) ⟹ cov x Q G"
proof (induct Q arbitrary: x G)
case (Eq y t)
then show ?case
by (auto simp: cov_Eq_self intro: cov.intros ap.intros split: term.splits)
qed (auto simp: set_flat set_gen_impl intro: cov.intros ap.intros
split: term.splits fmla.splits bool.splits if_splits)

definition "fixbound_impl 𝒬 x = filter (λQ. x ∈ fv Q ∧ gen_impl x Q = []) (sorted_list_of_set 𝒬)"

lemma set_fixbound_impl: "finite 𝒬 ⟹ set (fixbound_impl 𝒬 x) = fixbound 𝒬 x"
by (auto simp: fixbound_def nongens_def fixbound_impl_def set_gen_impl
dest: arg_cong[of _ _ set] simp flip: List.set_empty)

lemma fixbound_empty_iff: "finite 𝒬 ⟹ fixbound 𝒬 x ≠ {} ⟷ fixbound_impl 𝒬 x ≠ []"
by (auto simp: set_fixbound_impl dest: arg_cong[of _ _ set] simp flip: List.set_empty)

lemma fixbound_impl_hd_in: "finite 𝒬 ⟹ fixbound_impl 𝒬 x = y # ys ⟹ y ∈ 𝒬"
by (auto simp: fixbound_impl_def dest!: arg_cong[of _ _ set])

fun (in simplification) rb_impl :: "('a :: {infinite, linorder}, 'b :: linorder) fmla ⇒ ('a, 'b) fmla nres" where
"rb_impl (Neg Q) = do { Q' ← rb_impl Q; RETURN (simp (Neg Q'))}"
| "rb_impl (Disj Q1 Q2) = do { Q1' ← rb_impl Q1; Q2' ← rb_impl Q2; RETURN (simp (Disj Q1' Q2'))}"
| "rb_impl (Conj Q1 Q2) = do { Q1' ← rb_impl Q1; Q2' ← rb_impl Q2; RETURN (simp (Conj Q1' Q2'))}"
| "rb_impl (Exists x Q) = do {
Q' ← rb_impl Q;
𝒬 ← WHILE
(λ𝒬. fixbound_impl 𝒬 x ≠ []) (λ𝒬. do {
Qfix ← RETURN (hd (fixbound_impl 𝒬 x));
G ← RETURN (hd (cov_impl x Qfix));
RETURN (𝒬 - {Qfix} ∪
{simp (Conj Qfix (DISJ (qps G)))} ∪
(⋃y ∈ eqs x G. {cp (Qfix[x ❙→ y])}) ∪
{cp (Qfix ❙⊥ x)})})
(flat_Disj Q');
RETURN (simp (DISJ (exists x ` 𝒬)))}"
| "rb_impl Q = do { RETURN (simp Q) }"

lemma (in simplification) rb_impl_refines_rb: "rb_impl Q ≤ rb Q"
apply (induct Q)
apply (unfold rb.simps rb_impl.simps)
apply refine_mono
apply refine_mono
apply refine_mono
apply refine_mono
apply refine_mono
apply refine_mono
apply refine_mono
subgoal for x Q' Q
apply (rule order_trans[OF WHILE_le_WHILEI[where I="rb_INV x Q"]])
apply (rule order_trans[OF WHILEI_le_WHILEIT])
apply (rule WHILEIT_refine[OF _ _ _ refine_IdI, THEN refine_IdD])
apply refine_mono
apply (auto simp flip: set_fixbound_impl simp: neq_Nil_conv fixbound_impl_hd_in
intro!: cov_impl_cov rrb_cov_impl hd_in_set rb_INV_rrb)
done
done

fun (in simplification) rb_impl_det :: "('a :: {infinite, linorder}, 'b :: linorder) fmla ⇒ ('a, 'b) fmla dres" where
"rb_impl_det (Neg Q) = do { Q' ← rb_impl_det Q; dRETURN (simp (Neg Q'))}"
| "rb_impl_det (Disj Q1 Q2) = do { Q1' ← rb_impl_det Q1; Q2' ← rb_impl_det Q2; dRETURN (simp (Disj Q1' Q2'))}"
| "rb_impl_det (Conj Q1 Q2) = do { Q1' ← rb_impl_det Q1; Q2' ← rb_impl_det Q2; dRETURN (simp (Conj Q1' Q2'))}"
| "rb_impl_det (Exists x Q) = do {
Q' ← rb_impl_det Q;
𝒬 ← dWHILE
(λ𝒬. fixbound_impl 𝒬 x ≠ []) (λ𝒬. do {
Qfix ← dRETURN (hd (fixbound_impl 𝒬 x));
G ← dRETURN (hd (cov_impl x Qfix));
dRETURN (𝒬 - {Qfix} ∪
{simp (Conj Qfix (DISJ (qps G)))} ∪
(⋃y ∈ eqs x G. {cp (Qfix[x ❙→ y])}) ∪
{cp (Qfix ❙⊥ x)})})
(flat_Disj Q');
dRETURN (simp (DISJ (exists x ` 𝒬)))}"
| "rb_impl_det Q = do { dRETURN (simp Q) }"

lemma (in simplification) rb_impl_det_refines_rb_impl: "nres_of (rb_impl_det Q) ≤ rb_impl Q"
by (induct Q; unfold rb_impl.simps rb_impl_det.simps) refine_transfer+

lemmas (in simplification) RB_correct =
rb_impl_det_refines_rb_impl[THEN order_trans, OF
rb_impl_refines_rb[THEN order_trans, OF
rb_correct]]

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