# Theory Restrict_Bounds

```(*<*)
theory Restrict_Bounds
imports
Relational_Calculus
"Collections.Collections"
begin
(*>*)

section ‹Restricting Bound Variables›

fun flat_Disj where
"flat_Disj (Disj Q1 Q2) = flat_Disj Q1 ∪ flat_Disj Q2"
| "flat_Disj Q = {Q}"

lemma finite_flat_Disj[simp]: "finite (flat_Disj Q)"
by (induct Q rule: flat_Disj.induct) auto

lemma DISJ_flat_Disj: "DISJ (flat_Disj Q) ≜ Q"
by (induct Q rule: flat_Disj.induct) (auto simp: DISJ_union[THEN equiv_trans] simp del: cp.simps)

lemma fv_flat_Disj: "(⋃Q' ∈ flat_Disj Q. fv Q') = fv Q"
by (induct Q rule: flat_Disj.induct) auto

lemma fv_flat_DisjD: "Q' ∈ flat_Disj Q ⟹ x ∈ fv Q' ⟹ x ∈ fv Q"
by (auto simp: fv_flat_Disj[of Q, symmetric])

lemma cpropagated_flat_DisjD: "Q' ∈ flat_Disj Q ⟹ cpropagated Q ⟹ cpropagated Q'"
by (induct Q rule: flat_Disj.induct) auto

lemma flat_Disj_sub: "flat_Disj Q ⊆ sub Q"
by (induct Q) auto

lemma (in simplification) simplified_flat_DisjD: "Q' ∈ flat_Disj Q ⟹ simplified Q ⟹ simplified Q'"
by (elim simplified_sub set_mp[OF flat_Disj_sub])

definition fixbound where
"fixbound 𝒬 x = {Q ∈ 𝒬. x ∈ nongens Q}"

definition (in simplification) rb_spec where
"rb_spec Q = SPEC (λQ'. rrb Q' ∧ simplified Q' ∧ Q ≜ Q' ∧ fv Q' ⊆ fv Q)"

definition (in simplification) rb_INV where
"rb_INV x Q 𝒬 = (finite 𝒬 ∧
Exists x Q ≜ DISJ (exists x ` 𝒬) ∧
(∀Q' ∈ 𝒬. rrb Q' ∧ fv Q' ⊆ fv Q ∧ simplified Q'))"

lemma (in simplification) rb_INV_I:
"finite 𝒬 ⟹ Exists x Q ≜ DISJ (exists x ` 𝒬) ⟹ (⋀Q'. Q' ∈ 𝒬 ⟹ rrb Q') ⟹
(⋀Q'. Q' ∈ 𝒬 ⟹ fv Q' ⊆ fv Q) ⟹ (⋀Q'. Q' ∈ 𝒬 ⟹ simplified Q') ⟹ rb_INV x Q 𝒬"
unfolding rb_INV_def by auto

fun (in simplification) rb :: "('a :: {infinite, linorder}, 'b :: linorder) fmla ⇒ ('a, 'b) fmla nres" where
"rb (Neg Q) = do { Q' ← rb Q; RETURN (simp (Neg Q'))}"
| "rb (Disj Q1 Q2) = do { Q1' ← rb Q1; Q2' ← rb Q2; RETURN (simp (Disj Q1' Q2'))}"
| "rb (Conj Q1 Q2) = do { Q1' ← rb Q1; Q2' ← rb Q2; RETURN (simp (Conj Q1' Q2'))}"
| "rb (Exists x Q) = do {
Q' ← rb Q;
𝒬 ← WHILE⇩T⇗rb_INV x Q'⇖
(λ𝒬. fixbound 𝒬 x ≠ {}) (λ𝒬. do {
Qfix ← RES (fixbound 𝒬 x);
G ← SPEC (cov 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 Q = do { RETURN (simp Q) }"

lemma (in simplification) cov_fixbound: "cov x Q G ⟹ x ∈ fv Q ⟹
fixbound (insert (cp (Q ❙⊥ x)) (insert (simp (Conj Q (DISJ (qps G))))
(𝒬 - {Q} ∪ ((λy. cp (Q[x ❙→ y])) ` eqs x G)))) x = fixbound 𝒬 x - {Q}"
using Gen_simp[OF cov_Gen_qps[of x Q G]]
by (auto 4 4 simp: fixbound_def nongens_def fv_subst split: if_splits
dest!: fv_cp[THEN set_mp] fv_simp[THEN set_mp] fv_erase[THEN set_mp] dest: arg_cong[of _ _ fv] simp del: cp.simps)

lemma finite_fixbound[simp]: "finite 𝒬 ⟹ finite (fixbound 𝒬 x)"
unfolding fixbound_def by auto

lemma fixboundE[elim_format]: "Q ∈ fixbound 𝒬 x ⟹ x ∈ fv Q ∧ Q ∈ 𝒬 ∧ ¬ Gen x Q"
unfolding fixbound_def nongens_def by auto

lemma fixbound_fv: "Q ∈ fixbound 𝒬 x ⟹ x ∈ fv Q"
unfolding fixbound_def nongens_def by auto

lemma fixbound_in: "Q ∈ fixbound 𝒬 x ⟹ Q ∈ 𝒬"
unfolding fixbound_def nongens_def by auto

lemma fixbound_empty_Gen: "fixbound 𝒬 x = {} ⟹ x ∈ fv Q ⟹ Q ∈ 𝒬 ⟹ Gen x Q"
unfolding fixbound_def nongens_def by auto

lemma fixbound_insert:
"fixbound (insert Q 𝒬) x = (if Gen x Q ∨ x ∉ fv Q then fixbound 𝒬 x else insert Q (fixbound 𝒬 x))"
by (auto simp: fixbound_def nongens_def)

lemma fixbound_empty[simp]:
"fixbound {} x = {}"
by (auto simp: fixbound_def)

lemma flat_Disj_Exists_sub: "Q' ∈ flat_Disj Q ⟹ Exists y Qy ∈ sub Q' ⟹ Exists y Qy ∈ sub Q"
by (induct Q arbitrary: Q' rule: flat_Disj.induct) auto

lemma rrb_flat_Disj[simp]: "Q ∈ flat_Disj Q' ⟹ rrb Q' ⟹ rrb Q"
by (induct Q' rule: flat_Disj.induct) auto

lemma (in simplification) rb_INV_finite[simp]: "rb_INV x Q 𝒬 ⟹ finite 𝒬"
by (auto simp: rb_INV_def)

lemma (in simplification) rb_INV_fv: "rb_INV x Q 𝒬 ⟹ Q' ∈ 𝒬 ⟹ z ∈ fv Q' ⟹ z ∈ fv Q"
by (auto simp: rb_INV_def)

lemma (in simplification) rb_INV_rrb: "rb_INV x Q 𝒬 ⟹ Q' ∈ 𝒬 ⟹ rrb Q'"
by (auto simp: rb_INV_def)

lemma (in simplification) rb_INV_cpropagated: "rb_INV x Q 𝒬 ⟹ Q' ∈ 𝒬 ⟹ simplified Q'"
by (auto simp: rb_INV_def)

lemma (in simplification) rb_INV_equiv: "rb_INV x Q 𝒬 ⟹ Exists x Q ≜ DISJ (exists x ` 𝒬)"
by (auto simp: rb_INV_def)

lemma (in simplification) rb_INV_init[simp]: "simplified Q ⟹ rrb Q ⟹ rb_INV x Q (flat_Disj Q)"
by (auto simp: rb_INV_def fv_flat_DisjD simplified_flat_DisjD
equiv_trans[OF equiv_Exists_cong[OF DISJ_flat_Disj[THEN equiv_sym]] Exists_DISJ, simplified])

lemma (in simplification) rb_INV_step[simp]:
fixes Q :: "('a :: {infinite, linorder}, 'b :: linorder) fmla"
assumes "rb_INV x Q 𝒬" "Q' ∈ fixbound 𝒬 x" "cov x Q' G"
shows "rb_INV x Q (insert (cp (Q' ❙⊥ x)) (insert (simp (Conj Q' (DISJ (qps G)))) (𝒬 - {Q'} ∪ (λy. cp (Q'[x ❙→ y])) ` eqs x G)))"
proof (rule rb_INV_I, goal_cases finite equiv rrb fv simplified)
case finite
from assms(1,3) show ?case by simp
next
case equiv
from assms show ?case
unfolding rb_INV_def
by (auto 0 5 simp: fixbound_fv exists_cp_erase exists_cp_subst eqs_noteq exists_Exists
image_image image_Un insert_commute ac_simps dest: fixbound_in elim!: equiv_trans
intro:
equiv_trans[OF DISJ_push_in]
equiv_trans[OF DISJ_insert_reorder']
equiv_trans[OF DISJ_insert_reorder]
intro!:
equiv_trans[OF DISJ_exists_pull_out]
equiv_trans[OF equiv_Disj_cong[OF cov_Exists_equiv equiv_refl]]
equiv_trans[OF equiv_Disj_cong[OF equiv_Disj_cong[OF equiv_Exists_exists_cong[OF equiv_refl] equiv_refl] equiv_refl]]
simp del: cp.simps)
next
case (rrb Q)
with assms show ?case
unfolding rb_INV_def
by (auto intro!: rrb_cp_subst rrb_cp[OF rrb_erase] rrb_simp[of "Conj _ _"] dest: fixbound_in simp del: cp.simps)
next
case (fv Q')
with assms show ?case
unfolding rb_INV_def
by (auto 0 4 dest!: fv_cp[THEN set_mp] fv_simp[THEN set_mp] fv_DISJ[THEN set_mp, rotated 1] fv_erase[THEN set_mp]
cov_fv[OF assms(3) _ qps_in, rotated]
cov_fv[OF assms(3) _ eqs_in, rotated] dest: fixbound_in
simp: fv_subst fixbound_fv split: if_splits simp del: cp.simps)
next
case (simplified Q')
with assms show ?case
unfolding rb_INV_def by (auto simp: simplified_simp simplified_cp simp del: cp.simps)
qed

lemma (in simplification) rb_correct:
fixes Q :: "('a :: {linorder, infinite}, 'b :: linorder) fmla"
shows "rb Q ≤ rb_spec Q"
proof (induct Q rule: rb.induct[case_names Neg Disj Conj Exists Pred Bool Eq])
case (Exists x Q)
then show ?case
unfolding rb.simps rb_spec_def bind_rule_complete
by (rule order_trans, refine_vcg WHILEIT_rule[where R="measure (λ𝒬. card (fixbound 𝒬 x))"])
(auto simp: rb_INV_rrb rrb_simp simplified_simp fixbound_fv equiv_trans[OF equiv_Exists_cong rb_INV_equiv]
cov_fixbound fixbound_empty_Gen card_gt_0_iff UNION_singleton_eq_range subset_eq
intro!: equiv_simp[THEN equiv_trans, THEN equiv_sym, OF equiv_sym]
dest!: fv_DISJ[THEN set_mp, rotated 1] fv_simp[THEN set_mp] elim!: bspec elim: rb_INV_fv simp del: cp.simps)
qed (auto simp: rb_spec_def bind_rule_complete rrb_simp simplified_simp subset_eq dest!: fv_simp[THEN set_mp]
elim!: order_trans intro!: equiv_simp[THEN equiv_trans, THEN equiv_sym, OF equiv_sym] simp del: cp.simps)

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