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