Theory Refine_Unions
theory
Refine_Unions
imports
Enclosure_Operations
Weak_Set
begin
consts i_coll :: "interface ⇒ interface ⇒ interface"
subsection ‹composed set relations›
definition Union_rel::"('l × 'a set) set ⇒ ('a × 'b set) set ⇒ ('l × 'b set) set"
where Union_rel_internal: "Union_rel L S = L O ⟨S⟩set_rel O br Union top"
lemmas [autoref_rel_intf] = REL_INTFI[of "Union_rel" "i_coll" for L S R]
lemma Union_rel_def: "⟨L, S⟩Union_rel = L O ⟨S⟩set_rel O br Union top"
unfolding relAPP_def Union_rel_internal ..
lemma single_valued_Union_rel[relator_props]:
"single_valued L ⟹ single_valued R ⟹ single_valued (⟨L, R⟩Union_rel)"
unfolding relAPP_def
by (auto simp: Union_rel_internal intro!: relator_props intro: single_valuedI)
lemma Union_rel_br: "⟨(br l lI), (br s sI)⟩Union_rel = br (λa. ⋃(s ` (l a))) (λa. lI a ∧ (∀c ∈ l a. sI c))"
unfolding Union_rel_def br_def
apply (safe)
subgoal by (force simp: set_rel_def)
subgoal by (fastforce simp: set_rel_def)
subgoal by (force simp: set_rel_def)
subgoal for a
by (auto intro!: relcompI[where b="l a"] relcompI[where b="s ` l a"] simp: set_rel_def)
done
subsubsection ‹Implementation of set as union of sets›
context includes autoref_syntax begin
definition [simp]: "op_union_coll = (∪)"
lemma [autoref_op_pat]: "(∪) ≡ OP op_union_coll"
by simp
lemma coll_union12[autoref_rules]:
assumes unI[unfolded autoref_tag_defs]: "GEN_OP uni (∪) (L → L → L)"
shows "(uni, op_union_coll) ∈ ⟨L, S⟩Union_rel → ⟨L, S⟩Union_rel → ⟨L, S⟩Union_rel"
unfolding Union_rel_def
by (auto simp: br_def intro!: relcompI[OF unI[param_fo]]
relcompI[OF param_union[param_fo]])
definition "Id_arbitrary_interface = Id"
abbreviation "lw_rel ≡ ⟨Id_arbitrary_interface⟩list_wset_rel"
lemmas [autoref_rel_intf] = REL_INTFI[of Id_arbitrary_interface S for S::interface]
lemma single_valued_Id_arbitrary_interface[relator_props]: "single_valued Id_arbitrary_interface"
by (auto simp: Id_arbitrary_interface_def)
lemma lw_rel_def: "lw_rel = br set top"
by (simp add: list_wset_rel_def Id_arbitrary_interface_def)
abbreviation "clw_rel A ≡ ⟨lw_rel, A⟩Union_rel"
lemma clw_rel_def: "clw_rel A = lw_rel O ⟨A⟩set_rel O br Union top"
unfolding Union_rel_def
by simp
lemma op_wset_isEmpty_clw_rel[autoref_rules]:
"(λx. RETURN (x = []), isEmpty_spec) ∈ clw_rel A → ⟨bool_rel⟩nres_rel"
by (auto simp: nres_rel_def lw_rel_def Union_rel_def br_def set_rel_def)
lemma lift_clw_rel_map:
assumes "single_valued A"
assumes "single_valued B"
assumes "(fi, f) ∈ A → B"
assumes f_distrib: "⋀X. X ⊆ Range A ⟹ f (⋃X) = ⋃(f ` X)"
shows "(map fi, f) ∈ clw_rel A → clw_rel B"
using assms(1-2)
apply (auto simp: clw_rel_def)
subgoal for xs X YY Z
apply (rule relcompI[where b="fi ` X"])
apply (force simp: lw_rel_def br_def)
apply (rule relcompI[where b="f ` YY"])
prefer 2
apply (rule brI)
apply (subst f_distrib[symmetric])
apply (force simp: br_def set_rel_def)
apply (force simp add: br_def)
apply force
using assms(3)
apply parametricity
done
done
lemma list_rel_comp_Union_rel:
"single_valued R ⟹ (⟨R⟩list_rel O ⟨(⟨Id⟩list_wset_rel), S⟩Union_rel) =
⟨(⟨Id⟩list_wset_rel), (R O S)⟩Union_rel"
unfolding Union_rel_def
unfolding O_assoc[symmetric]
apply (subst list_rel_comp_list_wset_rel) apply simp apply (simp)
by (simp add: O_assoc list_wset_rel_def set_rel_compp)
lemma Cons_mem_clw_rel_iff:
assumes "single_valued A"
shows "(x # xs, X) ∈ clw_rel A ⟷ (∃Y YS. (x, Y) ∈ A ∧ (set xs, YS) ∈ ⟨A⟩set_rel ∧ X = Y ∪ ⋃YS)"
using assms
unfolding clw_rel_def
apply safe
subgoal by (force simp add: br_def lw_rel_def insert_mem_set_rel_iff[OF assms])
subgoal for Y YS
apply (auto intro!: relcompI[where b="insert x (set xs)"] relcompI[where b="insert Y YS"]
param_insert[param_fo]
simp: lw_rel_def br_def)
done
done
lemma split_spec_exact_with_stepsize_autoref[autoref_rules]:
assumes "PREFER single_valued A"
shows "(λxs. case xs of [] ⇒ SUCCEED | (x # xs) ⇒ RETURN (x, xs), split_spec_exact) ∈
clw_rel A → ⟨A ×⇩r clw_rel A⟩nres_rel"
proof -
have "∃a. (x, a) ∈ A ∧ (∃b. (y, b) ∈ clw_rel A ∧ xs ∪ ⋃YS = a ∪ b)"
if "(x, xs) ∈ A" "(set y, YS) ∈ ⟨A⟩set_rel"
for x y xs YS
using that
by (auto intro: exI[where x=xs] exI[where x="⋃YS"] simp: Union_rel_def lw_rel_def br_def)
then show ?thesis
using assms
by (auto simp: split_spec_exact_def Cons_mem_clw_rel_iff
intro!: nres_relI RETURN_SPEC_refine
split: list.splits)
qed
definition "split_spec_coll = split_spec"
lemma clw_rel_split[autoref_rules]:
assumes "PREFER single_valued A"
shows "(λxs. case xs of [] ⇒ SUCCEED | (x # xs) ⇒ RETURN (x, xs), split_spec_coll) ∈
clw_rel A → ⟨A ×⇩r clw_rel A⟩nres_rel"
proof -
have "∃a. (x, a) ∈ A ∧ (∃b. (y, b) ∈ clw_rel A ∧ xs ⊆ a ∪ b ∧ ⋃YS ⊆ a ∪ b)"
if "(x, xs) ∈ A" "(set y, YS) ∈ ⟨A⟩set_rel"
for x y xs YS
using that
by (auto intro: exI[where x=xs] exI[where x="⋃YS"] simp: Union_rel_def lw_rel_def br_def)
then show ?thesis
using assms
by (auto simp: split_spec_coll_def split_spec_def Cons_mem_clw_rel_iff
intro!: nres_relI RETURN_SPEC_refine
split: list.splits)
qed
definition [simp]: "op_Union_coll = Union"
lemma [autoref_op_pat]: "Union ≡ OP op_Union_coll"
by simp
lemma clw_rel_Union[autoref_rules]:
includes autoref_syntax
assumes [unfolded autoref_tag_defs, relator_props]: "PREFER single_valued A"
shows "(concat, op_Union_coll) ∈ ⟨clw_rel A⟩list_wset_rel → clw_rel A"
proof -
have "(concat, concat) ∈ ⟨⟨A⟩list_rel⟩list_rel → ⟨A⟩list_rel" (is "_ ∈ ?L1 → ?L2")
by parametricity
moreover have "(concat, op_Union_coll) ∈ ⟨clw_rel Id⟩list_wset_rel → clw_rel Id" (is "_ ∈ ?R1 → ?R2")
apply (auto simp: list_wset_rel_def Id_arbitrary_interface_def Union_rel_def
br_chain o_def)
apply (auto simp: br_def set_rel_def)
apply force
done
ultimately have "(concat, op_Union_coll) ∈ (?L1 → ?L2) O (?R1 → ?R2)"
by auto
also have "… ⊆ (?L1 O ?R1) → (?L2 O ?R2)" by (rule fun_rel_comp_dist)
also have "?L1 O ?R1 = ⟨clw_rel A⟩list_wset_rel"
apply (subst list_rel_comp_list_wset_rel)
subgoal by (simp add: relator_props)
subgoal using assms by (simp add: list_rel_comp_Union_rel Id_arbitrary_interface_def)
done
also have "?L2 O ?R2 = clw_rel A" using assms
unfolding Id_arbitrary_interface_def
by (subst list_rel_comp_Union_rel) simp_all
finally show ?thesis .
qed
definition [simp]: "op_coll_is_empty ≡ is_empty"
lemma [autoref_op_pat]: "is_empty ≡ OP op_coll_is_empty"
by simp
lemma op_set_isEmpty_Union_rel[autoref_rules]:
assumes "GEN_OP is_empty_i is_empty (A → bool_rel)"
shows "(λxs. xs = [] ∨ list_all is_empty_i xs, op_coll_is_empty) ∈ clw_rel A → bool_rel"
using assms
apply (auto simp: Union_rel_def lw_rel_def br_def set_rel_def op_set_isEmpty_def[abs_def]
op_coll_is_empty_def
list_all_iff dest: fun_relD)
apply (fastforce dest: fun_relD)
using fun_relD by fastforce
definition [simp]: "op_empty_coll = {}"
lemma Union_rel_empty[autoref_rules]:
shows "([], op_empty_coll) ∈ clw_rel R"
by (auto simp: br_def Union_rel_def
intro!: relcompI[OF param_empty] relcompI[OF list_wset_autoref_empty])
definition mk_coll::"'a set ⇒ 'a set" where [refine_vcg_def, simp]: "mk_coll x = x"
lemma mk_coll[autoref_rules]:
"PREFER single_valued R ⟹ (λx. [x], mk_coll) ∈ R → clw_rel R"
apply (rule fun_relI)
subgoal for x x'
by (auto simp: Union_rel_def list_wset_rel_def br_def set_rel_def single_valued_def
Id_arbitrary_interface_def
intro!: relcompI[where b="{xa. (x, xa) ∈ R}"] relcompI[where b="{x}"])
done
lemma map_mem_clw_rel_br:
assumes "⋃((λx. a (f x)) ` set xs) = X"
assumes "⋀x. x ∈ set xs ⟹ I (f x)"
shows "(map f xs, X) ∈ clw_rel (br a I)"
using assms
by (auto simp: lw_rel_def Union_rel_br intro!: brI)
lemma clw_rel_br: "clw_rel (br a I) = br (λxs. ⋃(a ` (set xs))) (λxs. Ball (set xs) I)"
unfolding lw_rel_def Union_rel_br by simp
lemma sets_of_coll_autoref[autoref_rules]:
shows "(λx. RETURN x, sets_of_coll) ∈ clw_rel R → ⟨⟨R⟩list_wset_rel⟩nres_rel"
by (auto simp: lw_rel_def Union_rel_def br_def set_rel_def list_wset_rel_def sets_of_coll_def
Id_arbitrary_interface_def
elim!: single_valued_as_brE
intro!: nres_relI RETURN_SPEC_refine)
auto
lemma Nil_mem_clw_rel_iff[simp]: "([], X) ∈ clw_rel W ⟷ X = {}"
by (auto simp: Union_rel_def br_def set_rel_def lw_rel_def)
end
end