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