Theory Refine_Invar

theory Refine_Invar
  imports
    Refine_Unions
    Refine_Intersection
begin

consts i_invar::"interface ⇒ interface ⇒ interface"

definition [simp]: "uninvar X = X"

definition with_invar::"'invar ⇒ 'a set ⇒ 'a set"
  where [simp]: "with_invar i X = X"

definition get_invar::"('invar ⇒ 'a set) ⇒ 'a set ⇒ ('a set × 'invar) nres"
  where [refine_vcg_def]: "get_invar a X = SPEC (λ(Y, invar). Y = X ∧ Y ⊆ a invar)"
lemma get_invar_pat[autoref_op_pat_def]: "get_invar i ≡ Autoref_Tagging.OP (get_invar i)"
  by auto

definition split_with_invar::"('c ⇒ 'a set) ⇒ 'a set ⇒ (('a set × 'c) × 'a set) nres"
  where [refine_vcg_def]: "split_with_invar i X = SPEC (λ((Y, sctn), YS). X = Y ∪ YS ∧ Y ⊆ i sctn)"
lemma split_with_invar_pat[autoref_op_pat_def]:
  "split_with_invar i ≡ Autoref_Tagging.OP (split_with_invar i)"
  by auto

context includes autoref_syntax begin

definition invar_rel_internal:
  "invar_rel a X S = {((x, s'), y). ∃s. (s', s) ∈ X ∧ (x, y) ∈ S ∧ y ⊆ a s}"
lemma invar_rel_def: "⟨X, S⟩invar_rel a = {((x, s'), y). ∃s. (s', s) ∈ X ∧ (x, y) ∈ S ∧ y ⊆ a s}"
  by (auto simp: invar_rel_internal relAPP_def)
lemmas [autoref_rel_intf] = REL_INTFI[of "invar_rel a" i_invar for a]

lemma invar_rel_br: "⟨(br a' I'), (br a I)⟩invar_rel b =
  br (λ(x, s). a x) (λ(x, s). I x ∧ I' s ∧ (a x ⊆ b (a' s)))"
  by (auto simp: invar_rel_def br_def)

lemma sv_appr_invar_rel[relator_props]: "single_valued S ⟹ single_valued (⟨X, S⟩invar_rel a)"
  and sv_inter_rel[relator_props]: "single_valued S ⟹ single_valued T ⟹ single_valued (⟨T, S⟩inter_rel)"
  unfolding relAPP_def
   apply (auto simp: invar_rel_internal inter_rel_internal single_valued_def set_rel_def)
     apply blast
    apply blast
  done

lemma with_invar_impl[autoref_rules]:
  assumes "(sctni, sctn) ∈ S"
  assumes "(Xi, X) ∈ clw_rel A"
  assumes "PREFER single_valued A"
  assumes "SIDE_PRECOND (X ⊆ a sctn)"
  shows "(map (λx. (x, sctni)) Xi, with_invar $ sctn $ X) ∈ clw_rel (⟨S,A⟩invar_rel a)"
  unfolding autoref_tag_defs
  using assms
  apply (auto simp: clw_rel_def elim!: single_valued_as_brE)
  subgoal for a i Y Z
    apply (rule relcompI)
    apply (force simp: lw_rel_def br_def)
    apply (rule relcompI[where b=Z])
    apply (auto simp: set_rel_def lw_rel_def invar_rel_def br_def)
    apply (metis Sup_le_iff)
    apply (metis Sup_le_iff)
    done
  done

lemma get_invar_autoref[autoref_rules]:
  "(λx. RETURN x, get_invar a) ∈ ⟨X, S⟩invar_rel a → ⟨S ×⇩r X⟩nres_rel"
  by (force simp: get_invar_def invar_rel_def nres_rel_def intro!: RETURN_SPEC_refine)

lemma uninvar_autoref[autoref_rules]:
  assumes "PREFER single_valued A"
  assumes "PREFER single_valued X"
  shows "(map fst, uninvar) ∈ clw_rel (⟨X, A⟩invar_rel b) → clw_rel A"
  using assms
  by (force simp: lw_rel_def Union_rel_br invar_rel_br elim!: single_valued_as_brE
      dest!: brD
      intro!: brI)

abbreviation "splitbysndimpl xs ≡ do {
  let s = snd (hd xs);
  let (ys, zs) = List.partition (λ(_, sctn). sctn = s) xs;
  RETURN ((map fst ys, s), zs)
}"

lemma split_with_invar_autoref[autoref_rules]:
  assumes "PREFER single_valued A"
  assumes "PREFER single_valued S"
  assumes "(xs, X) ∈ clw_rel (⟨S, A⟩invar_rel a)"
  shows
    "(if xs ≠ [] then do { ((xs, sctn), ys) ← splitbysndimpl xs; RETURN ((xs, sctn), ys) } else SUCCEED,
    split_with_invar a $ X) ∈
    ⟨(clw_rel A ×⇩r S) ×⇩r clw_rel (⟨S, A⟩invar_rel a)⟩nres_rel"
  using assms
  by (fastforce simp: Let_def split_with_invar_def split_beta'
      lw_rel_def Union_rel_br ex_br_conj_iff invar_rel_br
      elim!: single_valued_as_brE
      intro!: nres_relI RETURN_SPEC_refine
      dest!: brD)

end

definition
  "explicit_sctn_set po X0 =
    do {
      e ← isEmpty_spec X0;
      (_, _, Xis) ← WHILE⇗λ(e, X, Y).
          (e ⟶ X = {}) ∧
          X0 = X ∪ (⋃(sctn, IS)∈Y. IS) ∧
          (∀(sctn, IS) ∈ Y. IS ⊆ po sctn)⇖
        (λ(e, X, Y). ¬e)
        (λ(e, X, Y).
          do {
            ((S, sctn), X') ← split_with_invar po X;
            e ← isEmpty_spec X';
            RETURN (e, X', insert (sctn, S) Y)
          }
        )
        (e,
          X0,
          {});
      RETURN Xis
    }"
lemma explicit_sctn_set_pat[autoref_op_pat_def]: "explicit_sctn_set po ≡ Autoref_Tagging.OP (explicit_sctn_set po)"
  by auto

context includes autoref_syntax begin

lemma pfi: "PREFER single_valued R ⟹ ((#), OP insert ::: R → ⟨R⟩list_wset_rel → ⟨R⟩list_wset_rel) ∈ R → ⟨R⟩list_wset_rel → ⟨R⟩list_wset_rel"
  using list_set_autoref_insert[of R]
  by auto

schematic_goal explicit_sctn_setc:
  fixes po :: "'d ⇒ 'a::executable_euclidean_space set"
  assumes [THEN PREFER_sv_D, relator_props]: "PREFER single_valued A"
  assumes [THEN PREFER_sv_D, relator_props]: "PREFER single_valued S"
  assumes [autoref_rules]: "(XSi, XS) ∈ clw_rel (⟨S, A⟩invar_rel po)"
  shows "(nres_of ?f, explicit_sctn_set po $ XS) ∈ ⟨⟨S ×⇩r clw_rel A⟩list_wset_rel⟩nres_rel"
  unfolding autoref_tag_defs
  unfolding explicit_sctn_set_def
  by autoref_monadic

concrete_definition explicit_sctn_setc for XSi uses explicit_sctn_setc
lemmas [autoref_rules] = explicit_sctn_setc.refine

lemma explicit_sctn_set[THEN order_trans, refine_vcg]:
  "explicit_sctn_set po X ≤ SPEC (λR. X = (⋃(sctn, IS) ∈ R. IS) ∧ (∀(sctn, IS) ∈ R. IS ⊆ po sctn))"
  unfolding explicit_sctn_set_def
  by (refine_vcg) (auto simp: split_beta' subset_iff)
end

end