Theory Refine_Imperative_HOL.IICF_Multiset
section ‹Multiset Interface›
theory IICF_Multiset
imports "../../Sepref"
begin
subsection ‹Additions to Multiset Theory›
lemma rel_mset_Plus_gen:
assumes "rel_mset A m m'"
assumes "rel_mset A n n'"
shows "rel_mset A (m+n) (m'+n')"
using assms
by induction (auto simp: algebra_simps dest: rel_mset_Plus)
lemma rel_mset_single:
assumes "A x y"
shows "rel_mset A {#x#} {#y#}"
unfolding rel_mset_def
apply (rule exI[where x="[x]"])
apply (rule exI[where x="[y]"])
using assms by auto
lemma rel_mset_Minus:
assumes BIU: "bi_unique A"
shows "⟦ rel_mset A m n; A x y ⟧ ⟹ rel_mset A (m-{#x#}) (n-{#y#})"
unfolding rel_mset_def
proof clarsimp
fix ml nl
assume A: "A x y"
assume R: "list_all2 A ml nl"
show "∃ml'. mset ml' = mset ml - {#x#} ∧
(∃nl'. mset nl' = mset nl - {#y#} ∧ list_all2 A ml' nl')"
proof (cases "x∈set ml")
case False
have "y ∉ set nl" using A R
apply (auto simp: in_set_conv_decomp list_all2_append2 list_all2_Cons2)
using False BIU[unfolded bi_unique_alt_def]
apply (auto dest: left_uniqueD)
done
with False R show ?thesis by (auto simp: diff_single_trivial in_multiset_in_set)
next
case True
then obtain ml1 ml2 where [simp]: "ml=ml1@x#ml2" by (auto simp: in_set_conv_decomp)
then obtain nl1 nl2 where [simp]: "nl=nl1@y#nl2"
and LA: "list_all2 A ml1 nl1" "list_all2 A ml2 nl2"
using A R
apply (auto simp: in_set_conv_decomp list_all2_append1 list_all2_Cons1)
using BIU[unfolded bi_unique_alt_def]
apply (auto dest: right_uniqueD)
done
have
"mset (ml1@ml2) = mset ml - {#x#}"
"mset (nl1@nl2) = mset nl - {#y#}"
using R
by (auto simp: algebra_simps add_implies_diff union_assoc)
moreover have "list_all2 A (ml1@ml2) (nl1@nl2)"
by (rule list_all2_appendI) fact+
ultimately show ?thesis by blast
qed
qed
lemma rel_mset_Minus_gen:
assumes BIU: "bi_unique A"
assumes "rel_mset A m m'"
assumes "rel_mset A n n'"
shows "rel_mset A (m-n) (m'-n')"
using assms(3,2)
apply (induction R≡A _ _ rule: rel_mset_induct)
apply (auto dest: rel_mset_Minus[OF BIU] simp: algebra_simps)
done
lemma pcr_count:
assumes "bi_unique A"
shows "rel_fun (rel_mset A) (rel_fun A (=)) count count"
apply (intro rel_funI)
unfolding rel_mset_def
apply clarsimp
subgoal for x y xs ys
apply (rotate_tac,induction xs ys rule: list_all2_induct)
using assms
by (auto simp: bi_unique_alt_def left_uniqueD right_uniqueD)
done
subsection ‹Parametricity Setup›
definition [to_relAPP]: "mset_rel A ≡ p2rel (rel_mset (rel2p A))"
lemma rel2p_mset[rel2p]: "rel2p (⟨A⟩mset_rel) = rel_mset (rel2p A)"
by (simp add: mset_rel_def)
lemma p2re_mset[p2rel]: "p2rel (rel_mset A) = ⟨p2rel A⟩mset_rel"
by (simp add: mset_rel_def)
lemma mset_rel_empty[simp]:
"(a,{#})∈⟨A⟩mset_rel ⟷ a={#}"
"({#},b)∈⟨A⟩mset_rel ⟷ b={#}"
by (auto simp: mset_rel_def p2rel_def rel_mset_def)
lemma param_mset_empty[param]: "({#},{#}) ∈ ⟨A⟩mset_rel"
by simp
lemma param_mset_Plus[param]: "((+),(+))∈⟨A⟩mset_rel → ⟨A⟩mset_rel → ⟨A⟩mset_rel"
apply (rule rel2pD)
apply (simp add: rel2p)
apply (intro rel_funI)
by (rule rel_mset_Plus_gen)
lemma param_mset_add[param]: "(add_mset, add_mset) ∈ A → ⟨A⟩mset_rel → ⟨A⟩mset_rel"
apply (rule rel2pD)
apply (simp add: rel2p)
apply (intro rel_funI)
by (rule rel_mset_Plus)
lemma param_mset_minus[param]: "⟦single_valued A; single_valued (A¯)⟧
⟹ ((-), (-)) ∈ ⟨A⟩mset_rel → ⟨A⟩mset_rel → ⟨A⟩mset_rel"
apply (rule rel2pD)
apply (simp add: rel2p)
apply (intro rel_funI)
apply (rule rel_mset_Minus_gen)
subgoal apply (unfold IS_LEFT_UNIQUE_def[symmetric])
by (simp add: prop2p bi_unique_alt_def)
apply (simp; fail)
apply (simp; fail)
done
lemma param_count[param]: "⟦single_valued A; single_valued (A¯)⟧ ⟹ (count,count)∈⟨A⟩mset_rel → A → nat_rel"
apply (rule rel2pD)
apply (simp add: prop2p rel2p)
apply (rule pcr_count)
apply (simp add: bi_unique_alt_def)
done
lemma param_set_mset[param]:
shows "(set_mset, set_mset) ∈ ⟨A⟩mset_rel → ⟨A⟩set_rel"
apply (rule rel2pD; simp add: rel2p)
by (rule multiset.set_transfer)
definition [simp]: "mset_is_empty m ≡ m = {#}"
lemma mset_is_empty_param[param]: "(mset_is_empty,mset_is_empty) ∈ ⟨A⟩mset_rel → bool_rel"
unfolding mset_rel_def mset_is_empty_def[abs_def]
by (auto simp: p2rel_def rel_mset_def intro: nres_relI)
subsection ‹Operations›
sepref_decl_op mset_empty: "{#}" :: "⟨A⟩mset_rel" .
sepref_decl_op mset_is_empty: "λm. m={#}" :: "⟨A⟩mset_rel → bool_rel"
unfolding mset_is_empty_def[symmetric]
apply (rule frefI)
by parametricity
sepref_decl_op mset_insert: "add_mset" :: "A → ⟨A⟩mset_rel → ⟨A⟩mset_rel" .
sepref_decl_op mset_delete: "λx m. m - {#x#}" :: "A → ⟨A⟩mset_rel → ⟨A⟩mset_rel"
where "single_valued A" "single_valued (A¯)" .
sepref_decl_op mset_plus: "(+)::_ multiset ⇒ _" :: "⟨A⟩mset_rel → ⟨A⟩mset_rel → ⟨A⟩mset_rel" .
sepref_decl_op mset_minus: "(-)::_ multiset ⇒ _" :: "⟨A⟩mset_rel → ⟨A⟩mset_rel → ⟨A⟩mset_rel"
where "single_valued A" "single_valued (A¯)" .
sepref_decl_op mset_contains: "(∈#)" :: "A → ⟨A⟩mset_rel → bool_rel"
where "single_valued A" "single_valued (A¯)" .
sepref_decl_op mset_count: "λx y. count y x" :: "A → ⟨A⟩mset_rel → nat_rel"
where "single_valued A" "single_valued (A¯)" .
sepref_decl_op mset_pick: "λm. SPEC (λ(x,m'). m = {#x#} + m')" ::
"[λm. m≠{#}]⇩f ⟨A⟩mset_rel → A ×⇩r ⟨A⟩mset_rel"
unfolding mset_is_empty_def[symmetric]
apply (intro frefI nres_relI)
apply (refine_vcg SPEC_refine)
apply1 (rule ccontr; clarsimp)
applyS (metis msed_rel_invL rel2p_def rel2p_mset union_ac(2))
applyS parametricity
done
subsection ‹Patterns›
lemma [def_pat_rules]:
"{#} ≡ op_mset_empty"
"add_mset ≡ op_mset_insert"
"(=) $b${#} ≡ op_mset_is_empty$b"
"(=) ${#}$b ≡ op_mset_is_empty$b"
"(+) $a$b ≡ op_mset_plus$a$b"
"(-) $a$b ≡ op_mset_minus$a$b"
by (auto intro!: eq_reflection simp: algebra_simps)
lemma [def_pat_rules]:
"(+) $b$(add_mset$x${#}) ≡ op_mset_insert$x$b"
"(+) $(add_mset$x${#})$b ≡ op_mset_insert$x$b"
"(-) $b$(add_mset$x${#}) ≡ op_mset_delete$x$b"
"(<) $0$(count$a$x) ≡ op_mset_contains$x$a"
"(∈) $x$(set_mset$a) ≡ op_mset_contains$x$a"
by (auto intro!: eq_reflection simp: algebra_simps)
locale mset_custom_empty =
fixes rel empty and op_custom_empty :: "'a multiset"
assumes customize_hnr_aux: "(uncurry0 empty,uncurry0 (RETURN (op_mset_empty::'a multiset))) ∈ unit_assn⇧k →⇩a rel"
assumes op_custom_empty_def: "op_custom_empty = op_mset_empty"
begin
sepref_register op_custom_empty :: "'ax multiset"
lemma fold_custom_empty:
"{#} = op_custom_empty"
"op_mset_empty = op_custom_empty"
"mop_mset_empty = RETURN op_custom_empty"
unfolding op_custom_empty_def by simp_all
lemmas custom_hnr[sepref_fr_rules] = customize_hnr_aux[folded op_custom_empty_def]
end
end