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