Theory Refine_Info

theory
  Refine_Info
  imports
    Refine_Unions
    Refine_Vector_List
begin

consts i_info::"interface⇒interface⇒interface"

definition info_rel_internal: "info_rel I S = (I ×⇩r S) O br snd top"
lemma info_rel_def: "⟨I, S⟩info_rel = (I ×⇩r S) O br snd top"
  by (auto simp: relAPP_def info_rel_internal)
lemmas [autoref_rel_intf] = REL_INTFI[of "info_rel" i_info]

lemma info_rel_br: "⟨br a I, (br b J)⟩info_rel = br (λy. b (snd y)) (λx. I (fst x) ∧ J (snd x))"
  by (auto simp: info_rel_def br_def prod_rel_def)

lemma sv_info_rel[relator_props]:
  "single_valued S ⟹single_valued I ⟹ single_valued (⟨I, S⟩info_rel)"
  by (auto simp: info_rel_def intro!: relator_props)

definition [simp]: "op_info_is_empty = is_empty"
context includes autoref_syntax begin
lemma [autoref_op_pat]:  "is_empty ≡ OP op_info_is_empty"
  by simp
end

lemma op_set_isEmpty_info_rel_set[autoref_rules]:
  "GEN_OP empty_i (is_empty) (A → bool_rel) ⟹ (λx. empty_i (snd x), op_info_is_empty) ∈ ⟨I, A⟩info_rel → bool_rel"
  by (auto simp: info_rel_def br_def op_set_isEmpty_def[abs_def] dest: fun_relD)

definition [refine_vcg_def]: "get_info X = SPEC (λ(h, Y). Y = X)"
lemma get_info_autoref[autoref_rules]:
  shows "(λx. RETURN x, get_info) ∈ ⟨I, A⟩info_rel → ⟨I ×⇩r A⟩nres_rel"
  by (force simp: get_info_def info_rel_def nres_rel_def br_def intro!: RETURN_SPEC_refine)

definition with_info::"'b ⇒ 'a set ⇒ 'a set"
  where [simp, refine_vcg_def]: "with_info h x = x"

lemma with_stepsize_autoref[autoref_rules]:
  "((λh x. (h, x)), with_info) ∈ R → A → ⟨R, A⟩info_rel"
  by (auto simp: info_rel_def br_def intro!: prod_relI)

definition with_half_stepsizes::"'a set ⇒ 'a set"
  where [simp, refine_vcg_def]: "with_half_stepsizes x = x"
lemma with_half_stepsize_autoref[autoref_rules]:
  "((map (λ(h, x). (h/2, x))), with_half_stepsizes) ∈
  clw_rel (⟨rnv_rel, A⟩info_rel) → clw_rel (⟨rnv_rel, A⟩info_rel)"
  if  [unfolded autoref_tag_defs, relator_props]: "single_valued A"
  unfolding with_half_stepsizes_def
  apply (rule lift_clw_rel_map)
     apply (rule relator_props)+
  by (auto simp: info_rel_def br_def prod_rel_def)

definition with_infos::"'b ⇒ 'a set ⇒ 'a set"
  where [simp, refine_vcg_def]: "with_infos h x = x"
lemma with_infos_autoref[autoref_rules]:
  "(λh. map (Pair h), with_infos) ∈ R → clw_rel A → clw_rel (⟨R, A⟩info_rel)"
  if [unfolded autoref_tag_defs, relator_props]: "PREFER single_valued A" "PREFER single_valued R"
  unfolding with_infos_def
  apply (rule fun_relI)
  apply (rule lift_clw_rel_map)
     apply (rule relator_props)+
  by (auto simp: info_rel_def br_def prod_rel_def)

abbreviation "with_stepsize ≡ (with_info::real⇒_)"

definition split_with_info::"'a set ⇒ ('c × 'a set × 'a set) nres"
  where [refine_vcg_def]: "split_with_info X = SPEC (λ(S, Y, YS). X = Y ∪ YS)"

context includes autoref_syntax begin
lemma split_with_info_appr_plane_autoref[autoref_rules]:
  assumes "PREFER single_valued A"
  assumes "PREFER single_valued S"
  assumes "(xs, X) ∈ clw_rel (⟨A,S⟩info_rel)"
  shows
    "(if xs = [] then SUCCEED else let s = fst (hd xs); (a, b) = List.partition (λ(sctn, _). sctn = s) xs in RETURN (s, map snd a, b),
    split_with_info $ X) ∈
    ⟨A ×⇩r clw_rel S ×⇩r clw_rel (⟨A, S⟩info_rel)⟩nres_rel"
  using assms
  by (fastforce simp: Let_def split_with_info_def split_beta'
      lw_rel_def Union_rel_br info_rel_br ex_br_conj_iff Id_br[where 'a="'a sctn"]
      split: if_splits
      elim!: single_valued_as_brE
      intro!: nres_relI RETURN_SPEC_refine brI hd_in_set
      dest!: brD )

definition
  "explicit_info_set X0 =
    do {
      e ← isEmpty_spec X0;
      (_, _, Xis) ← WHILE⇗λ(e, X, Y).
          (e ⟶ X = {}) ∧
          X0 = X ∪ (⋃(sctn, IS)∈Y. IS)⇖
        (λ(e, X, Y). ¬e)
        (λ(e, X, Y).
          do {
            (sctn, S, X') ← split_with_info X;
            e ← isEmpty_spec X';
            RETURN (e, X', insert (sctn, S) Y)
          }
        )
        (e, X0, {});
      RETURN Xis
    }"

schematic_goal explicit_info_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⟩info_rel)"
  shows "(nres_of ?f, explicit_info_set $ XS) ∈ ⟨⟨S ×⇩r clw_rel A⟩list_wset_rel⟩nres_rel"
  unfolding autoref_tag_defs
  unfolding explicit_info_set_def
  including art
  by autoref_monadic
concrete_definition explicit_info_setc for XSi uses explicit_info_setc
lemmas [autoref_rules] = explicit_info_setc.refine

lemma explicit_info_set[THEN order_trans, refine_vcg]:
  "explicit_info_set X ≤ SPEC (λR. X = (⋃(sctn, IS) ∈ R. IS))"
  unfolding explicit_info_set_def
  by (refine_vcg) (auto simp: split_beta' subset_iff)

lemmas [relator_props del] = sv_info_rel
lemma sv_info_rel'[relator_props]:
  "single_valued S ⟹ single_valued (⟨I, S⟩info_rel)"
  by (auto simp: info_rel_def single_valued_def br_def)

lemma
  is_empty_info_rel_autoref[autoref_rules]:
  "GEN_OP ie is_empty (A → bool_rel) ⟹ (λx. ie(snd x), is_empty) ∈ ⟨R, A⟩info_rel → bool_rel"
  by (force simp: info_rel_def br_def dest: fun_relD)

definition with_coll_infos::"'c set ⇒ 'a set ⇒ 'a set nres"
  where [simp, refine_vcg_def]: "with_coll_infos h x = SPEC (λr. r = x)"

lemma with_coll_infos_autoref[autoref_rules]:
  "((λri ai. nres_of (if ri = [] then dSUCCEED else dRETURN (List.product ri ai))), with_coll_infos) ∈
    clw_rel R → clw_rel A → ⟨clw_rel (⟨R, A⟩info_rel)⟩nres_rel"
  if "PREFER single_valued R" "PREFER single_valued A"
  using that
  by (force simp: relcomp_unfold nres_rel_def info_rel_br list_wset_rel_def Union_rel_br
      Id_arbitrary_interface_def RETURN_RES_refine_iff set_rel_br
      elim!: single_valued_as_brE
      intro!: brI dest!: brD
      split: if_splits)

end

end