# Theory Weak_Set

```theory Weak_Set
imports
Autoref_Misc
begin

subsection ‹generic things›

lemma nres_rel_trans1: "a ≤ b ⟹ (b, i) ∈ ⟨R⟩nres_rel ⟹ (a, i) ∈ ⟨R⟩nres_rel"
using nres_relD order_trans
by (blast intro: nres_relI)

lemma nres_rel_trans2: "a ≤ b ⟹ (i, a) ∈ ⟨R⟩nres_rel ⟹ (i, b) ∈ ⟨R⟩nres_rel"
using nres_relD
by (blast intro: nres_relI ref_two_step)

lemma param_Union[param]: "(Union, Union) ∈ ⟨⟨R⟩set_rel⟩set_rel → ⟨R⟩set_rel"
by (fastforce simp: set_rel_def)

subsection ‹relation›

definition list_wset_rel_internal_def: "list_wset_rel R = br set top O ⟨R⟩set_rel"

lemma list_wset_rel_def: "⟨R⟩list_wset_rel = br set top O ⟨R⟩set_rel"
unfolding list_wset_rel_internal_def[abs_def] by (simp add: relAPP_def)

lemma list_wset_rel_br_eq: "⟨br a I⟩list_wset_rel = br (λxs. a ` set xs) (λxs. ∀x ∈ set xs. I x)"
by (auto simp: list_wset_rel_def br_def set_rel_def)

lemma mem_br_list_wset_rel_iff:
"(xs, X) ∈ ⟨br a I⟩list_wset_rel ⟷ (X = (a ` set xs) ∧ (∀x ∈ set xs. I x))"
by (auto simp: list_wset_rel_def set_rel_def br_def)

lemma list_set_rel_sv[relator_props]:
"single_valued R ⟹ single_valued (⟨R⟩list_wset_rel)"
unfolding list_wset_rel_def
by tagged_solver

lemmas [autoref_rel_intf] = REL_INTFI[of list_wset_rel i_set]

lemma list_wset_relD:
assumes "(a, b) ∈ ⟨R⟩list_wset_rel"
shows "(set a, b) ∈ ⟨R⟩set_rel"
using assms
by (auto simp: list_wset_rel_def br_def)

subsection ‹operations›

definition "op_set_ndelete x X = RES {X - {x}, X}"

lemma op_set_ndelete_spec: "op_set_ndelete x X = SPEC(λR. R = X - {x} ∨ R = X)"
by (auto simp: op_set_ndelete_def)

subsection ‹implementations›

lemma list_wset_autoref_empty[autoref_rules]:
"([],{})∈⟨R⟩list_wset_rel"
by (auto simp: list_wset_rel_def br_def relcompI)

context includes autoref_syntax begin

lemma mem_set_list_relE1:
assumes "(xs, ys) ∈ ⟨R⟩list_rel"
assumes "x ∈ set xs"
obtains y where "y ∈ set ys" "(x, y) ∈ R"
by (metis (no_types, lifting) assms in_set_conv_decomp list_relE3 list_rel_append1)

lemma mem_set_list_relE2:
assumes "(xs, ys) ∈ ⟨R⟩list_rel"
assumes "y ∈ set ys"
obtains x where "x ∈ set xs" "(x, y) ∈ R"
by (metis assms in_set_conv_decomp list_relE4 list_rel_append2)

lemma in_domain_list_relE:
assumes "⋀x. x ∈ set xs ⟹ x ∈ Domain R"
obtains ys where "(xs, ys) ∈ ⟨R⟩list_rel"
proof -
obtain y where y: "⋀x. x ∈ set xs ⟹ (x, y x) ∈ R"
using assms by (metis for_in_RI)
have "(xs, map y xs) ∈ ⟨R⟩list_rel"
by (auto simp: list_rel_def list_all2_iff in_set_zip intro!: y)
then show ?thesis ..
qed

lemma list_rel_comp_list_wset_rel:
assumes "single_valued R"
shows "⟨R⟩list_rel O ⟨S⟩list_wset_rel = ⟨R O S⟩list_wset_rel"
proof (safe, goal_cases)
case hyps: (1 a b x y z)
show ?case
unfolding list_wset_rel_def
proof (rule relcompI[where b = "set x"])
show "(set x, z) ∈ ⟨R O S⟩set_rel"
unfolding set_rel_def
using hyps
by (clarsimp simp: list_wset_rel_def br_def set_rel_def)
(meson mem_set_list_relE1 mem_set_list_relE2 relcomp.relcompI)
qed (simp add: br_def)
next
case hyps: (2 xs zs)
then have "⋀x. x ∈ set xs ⟹ x ∈ Domain R"
by (auto simp: list_wset_rel_def br_def set_rel_def)
from in_domain_list_relE[OF this]
obtain ys where ys: "(xs, ys) ∈ ⟨R⟩list_rel" .
have set_rel: "(set ys, zs) ∈ ⟨S⟩set_rel"
unfolding list_wset_rel_def set_rel_def
using hyps
by (clarsimp simp: list_wset_rel_def br_def set_rel_def)
(metis (full_types) assms mem_set_list_relE1 mem_set_list_relE2 relcompEpair single_valued_def ys)
from ys show ?case
by (rule relcompI)
(auto simp: list_wset_rel_def br_def intro!: relcompI[where b="set ys"] set_rel)
qed

lemma list_set_autoref_insert[autoref_rules]:
assumes "PREFER single_valued R"
shows "(Cons,Set.insert) ∈ R → ⟨R⟩list_wset_rel → ⟨R⟩list_wset_rel"
proof -
have 1: "(Cons, Cons) ∈ R → ⟨R⟩list_rel → ⟨R⟩list_rel"
by parametricity
moreover have 2: "(Cons, Set.insert) ∈ Id → ⟨Id⟩list_wset_rel → ⟨Id⟩list_wset_rel"
by (auto simp: list_wset_rel_def br_def)
ultimately have "(Cons, Set.insert) ∈ (R → ⟨R⟩list_rel → ⟨R⟩list_rel) O (Id → ⟨Id⟩list_wset_rel → ⟨Id⟩list_wset_rel)"
by auto
also have "… ⊆ R → ⟨R⟩list_wset_rel → ⟨R⟩list_wset_rel"
proof -
have "⟨R⟩list_rel O ⟨Id⟩list_wset_rel → ⟨R⟩list_rel O ⟨Id⟩list_wset_rel ⊆
⟨R⟩list_wset_rel → ⟨R⟩list_wset_rel"
by (rule fun_rel_mono)
(simp_all add: list_rel_comp_list_wset_rel assms[unfolded autoref_tag_defs])
then have "(⟨R⟩list_rel → ⟨R⟩list_rel) O (⟨Id⟩list_wset_rel → ⟨Id⟩list_wset_rel) ⊆
⟨R⟩list_wset_rel → ⟨R⟩list_wset_rel"
by (rule order_trans[OF fun_rel_comp_dist])
from _ this have
"R O Id → (⟨R⟩list_rel → ⟨R⟩list_rel) O (⟨Id⟩list_wset_rel → ⟨Id⟩list_wset_rel) ⊆
R → ⟨R⟩list_wset_rel → ⟨R⟩list_wset_rel"
by (rule fun_rel_mono) simp
then show ?thesis
by (rule order_trans[OF fun_rel_comp_dist])
qed
finally show ?thesis .
qed

lemma op_set_ndelete_wset_refine[autoref_rules]:
assumes "PREFER single_valued R"
assumes "(x, y) ∈ R" "(xs, Y) ∈ ⟨R⟩list_wset_rel"
shows "(nres_of (dRETURN (List.remove1 x xs)),op_set_ndelete \$ y \$ Y) ∈ ⟨⟨R⟩list_wset_rel⟩nres_rel"
proof -
from assms(3)[unfolded list_wset_rel_def]
obtain u where u: "(xs, u) ∈ br set top" "(u, Y) ∈ ⟨R⟩set_rel"
by (rule relcompE) auto
have "∃x'. (remove1 x xs, x') ∈ ⟨R⟩list_wset_rel ∧ (x' = Y - {y} ∨ x' = Y)"
proof (cases "x ∈ set (remove1 x xs)")
case True
then have "set (remove1 x xs) = set xs"
by (metis in_set_remove1 set_remove1_subset subsetI subset_antisym)
then show ?thesis
using True u
by (auto intro!: simp: list_wset_rel_def br_def)
next
case False
then have r: "set (remove1 x xs) = set xs - {x}"
using in_set_remove1[of _ x xs] u
by (auto simp del: in_set_remove1 simp add: br_def)
from assms old_set_rel_sv_eq[of R] have [simp]: "⟨R⟩set_rel = ⟨R⟩old_set_rel" by simp
show ?thesis
using False ‹(x, y) ∈ R› assms
by (auto simp: relcomp_unfold r old_set_rel_def single_valued_def br_def list_wset_rel_def)
qed
then show ?thesis
unfolding op_set_ndelete_spec autoref_tag_defs
by (safe intro!: nres_relI SPEC_refine det_SPEC elim!: relcompE)
qed

subsection ‹pick›

lemma
pick_wset_refine[autoref_rules]:
assumes[unfolded autoref_tag_defs, simp]: "SIDE_PRECOND (X ≠ {})"
assumes "(XS, X) ∈ ⟨A⟩list_wset_rel"
shows "(nres_of (dRETURN (hd XS)), op_set_pick \$ X) ∈ ⟨A⟩nres_rel"
proof -
have "∀x∈set XS. ∃y∈X. (x, y) ∈ A ⟹ ∀y∈X. ∃x∈set XS. (x, y) ∈ A ⟹
∀x'. (hd XS, x') ∈ A ⟶ x' ∉ X ⟹ xa ∉ X" for xa
by (metis (full_types) empty_iff insertCI list.exhaust list.sel(1) list.set)
show ?thesis
using assms(2)
unfolding op_set_pick_def[abs_def] autoref_tag_defs
by (cases XS)
(auto simp: Let_def list_wset_rel_def set_rel_def br_def intro!: nres_relI RETURN_RES_refine det_SPEC)
qed

subsection ‹pick remove›

definition "op_set_npick_remove X = SPEC (λ(x, X'). x ∈ X ∧ (X' = X - {x} ∨ X' = X))"
lemma op_set_pick_remove_pat[autoref_op_pat]:
"SPEC (λ(x, X'). x ∈ X ∧ (X' = X - {x} ∨ X' = X)) ≡ op_set_npick_remove \$ X"
"SPEC (λ(x, X'). x ∈ X ∧ (X' = X ∨ X' = X - {x})) ≡ op_set_npick_remove \$ X"
"do { x ← SPEC (λx. x ∈ X); X' ← op_set_ndelete x X; f x X' } ≡ do { (x, X') ← op_set_npick_remove X; f x X'}"
by (auto simp: op_set_npick_remove_def op_set_ndelete_def pw_eq_iff refine_pw_simps intro!: eq_reflection)

lemma op_set_npick_remove_def':
"X ≠ {} ⟹ op_set_npick_remove X =
do { ASSERT (X ≠ {}); x ← op_set_pick X; X' ← op_set_ndelete x X; RETURN (x, X')}"
by (auto simp: op_set_npick_remove_def op_set_ndelete_def pw_eq_iff refine_pw_simps )

lemma aux: "(a, c) ∈ R ⟹ a = b ⟹ (b, c) ∈ R"
by simp

lemma
op_set_npick_remove_refine[autoref_rules]:
assumes [THEN PREFER_sv_D, relator_props]: "PREFER single_valued A"
assumes "SIDE_PRECOND (X ≠ {})"
assumes [autoref_rules]: "(XS, X) ∈ ⟨A⟩list_wset_rel"
shows "(RETURN (hd XS, tl XS), op_set_npick_remove \$ X) ∈ ⟨A ×⇩r ⟨A⟩list_wset_rel⟩nres_rel"
proof -
have "(RETURN (hd XS, remove1 (hd XS) XS), ASSERT (X ≠ {}) ⤜ (λ_. op_set_pick X ⤜ (λx. op_set_ndelete x X ⤜ (λX'. RETURN (x, X')))))
∈ ⟨A ×⇩r ⟨A⟩list_wset_rel⟩nres_rel"
by (rule aux, autoref, simp)
then show ?thesis
unfolding autoref_tag_defs op_set_npick_remove_def'[OF assms(2)[unfolded autoref_tag_defs]]
using assms
by (subst remove1_tl[symmetric]) (force simp: list_wset_rel_def br_def set_rel_def)
qed

subsection ‹emptiness check›

lemma isEmpty_wset_refine[autoref_rules]:
assumes "(xs, X) ∈ ⟨A⟩list_wset_rel"
shows "(xs = [], op_set_isEmpty \$ X) ∈ bool_rel"
using assms
by (auto simp: list_wset_rel_def br_def set_rel_def)

subsection ‹union›

lemma union_wset_refine[autoref_rules]:
"(append, (∪)) ∈ ⟨R⟩list_wset_rel → ⟨R⟩list_wset_rel → ⟨R⟩list_wset_rel"
by (auto 0 3 simp: list_wset_rel_def set_rel_def relcomp_unfold br_def)

subsection ‹of list›

lemma set_wset_refine[autoref_rules]:
assumes "PREFER single_valued R"
shows "((λx. x), set) ∈ ⟨R⟩list_rel → ⟨R⟩list_wset_rel"
proof (rule fun_relI)
fix a a'
assume aa': "(a, a') ∈ ⟨R⟩list_rel"
moreover have "(a, a') ∈ ⟨R⟩list_rel ⟹ (set a, set a') ∈ ⟨R⟩set_rel"
using assms[THEN PREFER_sv_D]
by parametricity
ultimately show "(a, set a') ∈ ⟨R⟩list_wset_rel"
unfolding list_wset_rel_def
by (intro relcompI[where b="set a"]) (simp_all add: br_def)
qed

subsection ‹filter set›

lemma bCollect_param: "((λy a. {x ∈ y. a x}), (λz a'. {x ∈ z. a' x})) ∈ ⟨R⟩set_rel → (R → bool_rel) → ⟨R⟩set_rel"
unfolding set_rel_def
apply safe
subgoal using tagged_fun_relD_both by fastforce
subgoal using tagged_fun_relD_both by fastforce
done

lemma op_set_filter_list_wset_refine[autoref_rules]:
"(filter, op_set_filter) ∈ (R → bool_rel) → ⟨R⟩list_wset_rel → ⟨R⟩list_wset_rel"
by (force simp: list_wset_rel_def br_def bCollect_param[param_fo])

subsection ‹bound on cardinality›

definition "op_set_wcard X = SPEC (λc. card X ≤ c)"

lemma op_set_wcard_refine[autoref_rules]: "PREFER single_valued R ⟹ ((λxs. RETURN (length xs)), op_set_wcard) ∈ ⟨R⟩list_wset_rel → ⟨Id⟩nres_rel"
proof (auto simp: list_wset_rel_def nres_rel_def br_def op_set_wcard_def, goal_cases)
case (1 x z)
thus ?case
by (induction x arbitrary: z)
(auto simp: old_set_rel_sv_eq[symmetric] old_set_rel_def Image_insert intro!: card_insert_le_m1)
qed

lemmas op_set_wcard_spec[refine_vcg] = op_set_wcard_def[THEN eq_refl, THEN order_trans]

subsection ‹big union›

lemma Union_list_wset_rel[autoref_rules]:
assumes "PREFER single_valued A"
shows "(concat, Union) ∈ ⟨⟨A⟩list_wset_rel⟩list_wset_rel → ⟨A⟩list_wset_rel"
proof -
have "(concat, concat) ∈ ⟨⟨A⟩list_rel⟩list_rel → ⟨A⟩list_rel" (is "_ ∈ ?A")
by parametricity
moreover have "(concat, Union) ∈ ⟨⟨Id⟩list_wset_rel⟩list_wset_rel → ⟨Id⟩list_wset_rel" (is "_ ∈ ?B")
by (auto simp: list_wset_rel_def br_def relcomp_unfold set_rel_def; meson)
ultimately have "(concat, Union) ∈ ?A O ?B"
by auto
also note fun_rel_comp_dist
finally show ?thesis
using assms
by (simp add: list_rel_comp_list_wset_rel list_rel_sv_iff)
qed

subsection ‹image›

lemma image_list_wset_rel[autoref_rules]:
assumes "PREFER single_valued B"
shows "(map, (`)) ∈ (A → B) → ⟨A⟩list_wset_rel → ⟨B⟩list_wset_rel"
unfolding list_wset_rel_def relcomp_unfold
proof safe
fix a a' aa a'a y
assume H: "(a, a') ∈ A → B" "(aa, y) ∈ br set top" "(y, a'a) ∈ ⟨A⟩set_rel"
have "(map a aa, a ` y) ∈ br set top"
using H
by (auto simp: br_def)
moreover have " (a ` y, a' ` a'a) ∈ ⟨B⟩set_rel"
using H
by (fastforce simp: fun_rel_def set_rel_def split: prod.split)
ultimately show "∃y. (map a aa, y) ∈ br set top ∧ (y, a' ` a'a) ∈ ⟨B⟩set_rel"
by (safe intro!: exI[where x = "a ` y"])
qed

subsection ‹Ball›

lemma Ball_list_wset_rel[autoref_rules]:
"((λxs p. foldli xs (λx. x) (λa _. p a) True), Ball) ∈ ⟨A⟩list_wset_rel → (A → bool_rel) → bool_rel"
proof -
have "(set a, a') ∈ ⟨A⟩set_rel ⟹ (Ball (set a), Ball a') ∈ (A → bool_rel) → bool_rel" for a a'
by parametricity
then have "(λxs. Ball (set xs), Ball) ∈ {(x, z). (set x, z) ∈ ⟨A⟩set_rel} → (A → bool_rel) → bool_rel"
unfolding mem_Collect_eq split_beta' fst_conv snd_conv
by (rule fun_relI) auto
then show ?thesis
by (simp add: relcomp_unfold br_def foldli_ball_aux list_wset_rel_def)
qed

subsection ‹weak foreach loop›

definition FORWEAK :: "'a set ⇒ 'b nres ⇒ ('a ⇒ 'b nres) ⇒ ('b ⇒ 'b ⇒ 'b nres) ⇒ 'b nres"
where "FORWEAK X d f c =
(if X = {} then d
else do {
(a, X) ← op_set_npick_remove X;
b ← f a;
(b, _) ← WHILE (λ(_, X). ¬ op_set_isEmpty X) (λ(b, X).
do {
ASSERT (X ≠ {});
(a, X) ← op_set_npick_remove X;
b' ← f a;
b ← c b b';
RETURN (b, X)
}) (b, X);
RETURN b
})"

schematic_goal
FORWEAK_wset_WHILE_refine:
assumes [relator_props]: "single_valued A"
assumes [autoref_rules]:
"(Xi, X) ∈ ⟨A⟩list_wset_rel"
"(di, d) ∈ ⟨B⟩nres_rel"
"(fi, f) ∈ A → ⟨B⟩nres_rel"
"(ci, c) ∈ B → B → ⟨B⟩nres_rel"
shows "(?f, FORWEAK X d f c) ∈ ⟨B⟩nres_rel"
unfolding FORWEAK_def
by autoref

lemma FORWEAK_LIST_transfer_nfoldli:
"nfoldli xs (λ_. True) (λx a. c a x) a ≤ do {
(a, _) ←
WHILE (λ(a, xs). xs ≠ []) (λ(a, xs). do {
(x, xs) ← RETURN (hd xs, tl xs);
a ← c a x;
RETURN (a, xs)
}) (a, xs);
RETURN a}"
proof (induct xs arbitrary: a)
case Nil thus ?case by (auto simp: WHILE_unfold)
next
case (Cons x xs)
show ?case
by (auto simp: WHILE_unfold intro!: bind_mono Cons[THEN order.trans])
qed

lemma
FORWEAK_wset_refine:
assumes [relator_props]: "PREFER single_valued A"
assumes [autoref_rules]:
"(Xi, X) ∈ ⟨A⟩list_wset_rel"
"(di, d) ∈ ⟨B⟩nres_rel"
"(fi, f) ∈ A → ⟨B⟩nres_rel"
"(ci, c) ∈ B → B → ⟨B⟩nres_rel"
shows
"((if Xi = [] then di else do { b ← fi (hd Xi); nfoldli (tl Xi) (λ_. True) (λx b. do {b' ← fi x; ci b b'}) b }),
(OP FORWEAK ::: ⟨A⟩list_wset_rel → ⟨B⟩nres_rel → (A → ⟨B⟩nres_rel) → (B → B → ⟨B⟩nres_rel) → ⟨B⟩nres_rel) \$ X \$ d \$ f \$ c) ∈ ⟨B⟩nres_rel"
unfolding autoref_tag_defs
by (rule nres_rel_trans1[OF _ FORWEAK_wset_WHILE_refine[OF assms[simplified autoref_tag_defs]]])
(auto intro!: bind_mono FORWEAK_LIST_transfer_nfoldli[THEN order.trans])
concrete_definition FORWEAK_LIST for Xi di fi ci uses FORWEAK_wset_refine
lemmas [autoref_rules] = FORWEAK_LIST.refine

schematic_goal FORWEAK_LIST_transfer_nres:
assumes [refine_transfer]: "nres_of d ≤ d'"
assumes [refine_transfer]: "⋀x. nres_of (f x) ≤ f' x"
assumes [refine_transfer]: "⋀x y. nres_of (g x y) ≤ g' x y"
shows
"nres_of (?f) ≤ FORWEAK_LIST xs d' f' g'"
unfolding FORWEAK_LIST_def
by refine_transfer
concrete_definition dFORWEAK_LIST for xs d f g uses FORWEAK_LIST_transfer_nres
lemmas [refine_transfer] = dFORWEAK_LIST.refine

schematic_goal FORWEAK_LIST_transfer_plain:
assumes [refine_transfer]: "RETURN d ≤ d'"
assumes [refine_transfer]: "⋀x. RETURN (f x) ≤ f' x"
assumes [refine_transfer]: "⋀x y. RETURN (g x y) ≤ g' x y"
shows "RETURN ?f ≤ FORWEAK_LIST xs d' f' g'"
unfolding FORWEAK_LIST_def
by refine_transfer
concrete_definition FORWEAK_LIST_plain for xs f g uses FORWEAK_LIST_transfer_plain
lemmas [refine_transfer] = FORWEAK_LIST_plain.refine

schematic_goal FORWEAK_LIST_transfer_ne_plain:
assumes "SIDE_PRECOND_OPT (xs ≠ [])"
assumes [refine_transfer]: "⋀x. RETURN (f x) ≤ f' x"
assumes [refine_transfer]: "⋀x y. RETURN (g x y) ≤ g' x y"
shows "RETURN ?f ≤ FORWEAK_LIST xs d' f' g'"
using assms
by (simp add: FORWEAK_LIST_def) refine_transfer
concrete_definition FORWEAK_LIST_ne_plain for xs f g uses FORWEAK_LIST_transfer_ne_plain

lemma FORWEAK_empty[simp]: "FORWEAK {} = (λd _ _. d)"
by (auto simp: FORWEAK_def[abs_def])

lemma FORWEAK_WHILE_casesI:
assumes "X = {} ⟹ d ≤ SPEC P"
assumes "⋀a X'. a ∈ X ⟹ X' = X - {a} ⟹
f a ≤ SPEC (λx. WHILE (λ(_, X). X ≠ {})
(λ(b, X).
do {
ASSERT (X ≠ {});
(a, X) ← op_set_npick_remove X;
b' ← f a;
b ← c b b';
RETURN (b, X)
})
(x, X')
≤ SPEC (λ(b, _). RETURN b ≤ SPEC P))"
assumes "⋀a. a ∈ X ⟹
f a ≤ SPEC (λx. WHILE (λ(_, X). X ≠ {})
(λ(b, X).
do {
ASSERT (X ≠ {});
(a, X) ← op_set_npick_remove X;
b' ← f a;
b ← c b b';
RETURN (b, X)
})
(x, X)
≤ SPEC (λ(b, _). RETURN b ≤ SPEC P))"
shows "FORWEAK X d f c ≤ SPEC P"
unfolding FORWEAK_def
apply (cases "X = {}")
subgoal by (simp add: assms(1))
subgoal
supply op_set_npick_remove_def[refine_vcg_def]
apply (refine_vcg)
apply clarsimp
apply (erule disjE)
subgoal
by (refine_vcg assms(2))
subgoal
by (refine_vcg assms(3))
done
done

lemma FORWEAK_invarI:
fixes I::"'b ⇒ 'a set ⇒ bool"
assumes "X = {} ⟹ d ≤ SPEC P"
assumes fspec_init1[THEN order_trans]: "⋀a. a ∈ X ⟹ f a ≤ SPEC (λx. I x (X - {a}))"
assumes fspec_init2[THEN order_trans]: "⋀a. a ∈ X ⟹ f a ≤ SPEC (λx. I x X)"
assumes fspec_invar1[THEN order_trans]:
"⋀a aa b ba. I aa b ⟹ a ∈ b ⟹ f a ≤ SPEC (λxb. c aa xb ≤ SPEC (λr. I r (b - {a})))"
assumes fspec_invar2[THEN order_trans]: "⋀a aa b ba. I aa b ⟹ a ∈ b ⟹ f a ≤ SPEC (λxb. c aa xb ≤ SPEC (λr. I r b))"
assumes fin: "⋀aa. I aa {} ⟹ P aa"
shows "FORWEAK X d f c ≤ SPEC P"
unfolding FORWEAK_def
apply (cases "X = {}")
subgoal by (simp add: assms(1))
subgoal
supply op_set_npick_remove_def[refine_vcg_def]
apply (refine_vcg)
apply clarsimp
apply (erule disjE)
subgoal
apply (refine_vcg fspec_init1)
apply (rule order_trans[OF WHILE_le_WHILEI[where I="λ(a, b). I a b"]])
apply (refine_vcg)
subgoal
apply clarsimp
apply (erule disjE)
subgoal by (rule fspec_invar1, assumption, assumption)  (refine_vcg)
subgoal by (rule fspec_invar2, assumption, assumption)  (refine_vcg)
done
subgoal by (simp add: fin)
done
subgoal
apply (refine_vcg fspec_init2)
apply (rule order_trans[OF WHILE_le_WHILEI[where I="λ(a, b). I a b"]])
apply (refine_vcg)
subgoal
apply clarsimp
apply (erule disjE)
subgoal by (rule fspec_invar1, assumption, assumption)  (refine_vcg)
subgoal by (rule fspec_invar2, assumption, assumption)  (refine_vcg)
done
subgoal by (simp add: fin)
done
done
done

lemma FORWEAK_mono_rule:
fixes f::"'d ⇒ 'e nres" and c::"'e ⇒ 'e ⇒ 'e nres" and I::"'d set ⇒ 'e ⇒ bool"
assumes empty: "S = {} ⟹ d ≤ SPEC P"
assumes I0[THEN order_trans]: "⋀s. s ∈ S ⟹ f s ≤ SPEC (I {s})"
assumes I_mono: "⋀it it' σ. I it σ ⟹ it' ⊆ it ⟹ it ⊆ S ⟹ I it' σ"
assumes IP[THEN order_trans]:
"⋀x it σ. ⟦ x∈S; it⊆S; I it σ ⟧ ⟹ f x ≤ SPEC (λf'. c σ f' ≤ SPEC (I (insert x it)))"
assumes II: "⋀σ. I S σ ⟹ P σ"
shows "FORWEAK S d f c ≤ SPEC P"
apply (rule FORWEAK_invarI[where I="λb X. X ⊆ S ∧ I (S - X) b"])
subgoal by (rule empty)
subgoal by (auto simp: Diff_Diff_Int intro!: I0)
subgoal
by (metis (mono_tags, lifting) Diff_cancel I0 I_mono Refine_Basic.RES_sng_eq_RETURN iSPEC_rule
less_eq_nres.simps(2) nres_order_simps(21) subset_insertI subset_refl)
subgoal for a b it
apply (rule IP[of _ "S - it" b])
subgoal by force
subgoal by force
subgoal by force
subgoal
apply clarsimp
apply (rule order_trans, assumption)
by (auto simp: it_step_insert_iff intro: order_trans)
done
subgoal for a b it
apply (rule IP[of _ "S - it" b])
subgoal by force
subgoal by force
subgoal by force
subgoal
apply clarsimp
apply (rule order_trans, assumption)
by (auto simp: it_step_insert_iff intro: I_mono)
done
subgoal by (auto intro!: II)
done

lemma FORWEAK_case_rule:
fixes f::"'d ⇒ 'e nres" and c::"'e ⇒ 'e ⇒ 'e nres" and I::"'d set ⇒ 'e ⇒ bool"
assumes empty: "S = {} ⟹ d ≤ SPEC P"
assumes I01[THEN order_trans]: "⋀s. s ∈ S ⟹ f s ≤ SPEC (I (S - {s}))"
assumes I02[THEN order_trans]: "⋀s. s ∈ S ⟹ f s ≤ SPEC (I S)"
assumes IP1[THEN order_trans]:
"⋀x it σ. ⟦ x∈it; it⊆S; I it σ ⟧ ⟹ f x ≤ SPEC (λf'. c σ f' ≤ SPEC (I (it-{x})))"
assumes IP2[THEN order_trans]:
"⋀x it σ. ⟦ x∈it; it⊆S; I it σ ⟧ ⟹ f x ≤ SPEC (λf'. c σ f' ≤ SPEC (I it))"
assumes II: "⋀σ. I {} σ ⟹ P σ"
shows "FORWEAK S d f c ≤ SPEC P"
apply (rule FORWEAK_invarI[where I = "λa b. I b a ∧ b ⊆ S"])
subgoal by (rule empty)
subgoal by (rule I01) auto
subgoal by (rule I02) auto
subgoal for a b it
apply (rule IP1[of a it b])
subgoal by force
subgoal by force
subgoal by force
subgoal
apply clarsimp
by (rule order_trans, assumption) auto
done
subgoal by (rule IP2) auto
subgoal by (rule II) auto
done

lemma FORWEAK_elementwise_rule:
assumes "nofail d"
assumes Inf_spec: "⋀X. X ∈ XX ⟹ Inf_spec X ≤ SPEC (Q X)"
notes [refine_vcg] = order.trans[OF Inf_spec]
assumes comb_spec1: "⋀a b X Y. Q X a ⟹ comb a b ≤ SPEC (Q X)"
assumes comb_spec2: "⋀a b X Y. Q X b ⟹ comb a b ≤ SPEC (Q X)"
shows "FORWEAK XX d Inf_spec comb ≤ SPEC (λi. ∀x∈XX. Q x i)"
apply (rule FORWEAK_mono_rule[where I="λS i. ∀x∈S. Q x i"])
subgoal using ‹nofail d› by (simp add: nofail_SPEC_iff)
subgoal by (simp add: Diff_Diff_Int Inf_spec)
subgoal by force
subgoal for x it σ
apply (refine_transfer refine_vcg)
apply (rule SPEC_BallI)
apply (rule SPEC_nofail)
apply (rule comb_spec2)
apply assumption
subgoal for y z
apply (cases "z = x")
subgoal by simp (rule comb_spec2)
subgoal by (rule comb_spec1) force
done
done
subgoal by force
done

end

lemma nofail_imp_RES_UNIV: "nofail s ⟹ s ≤ RES UNIV"
by (metis Refine_Basic.nofail_SPEC_triv_refine UNIV_I top_empty_eq top_set_def)

lemma FORWEAK_unit_rule[THEN order_trans, refine_vcg]:
assumes "nofail d"
assumes "⋀s. nofail (f s)"
assumes "nofail (c () ())"
shows "FORWEAK XS d f c ≤ SPEC (λ(_::unit). True)"
using assms
by (intro order_trans[OF FORWEAK_elementwise_rule[where Q=top]])
(auto simp: top_fun_def le_SPEC_UNIV_rule nofail_SPEC_triv_refine nofail_imp_RES_UNIV)

lemma FORWEAK_mono_rule':
fixes f::"'d ⇒ 'e nres" and c::"'e ⇒ 'e ⇒ 'e nres" and I::"'d set ⇒ 'e ⇒ bool"
assumes empty: "S = {} ⟹ d ≤ SPEC P"
assumes I0[THEN order_trans]: "⋀s. s ∈ S ⟹ f s ≤ SPEC (I {s})"
assumes I_mono: "⋀ab bb xb. ab ∈ bb ⟹ bb ⊆ S ⟹ I (insert ab (S - bb)) xb ⟹ I (S - bb) xb"
assumes IP[THEN order_trans]:
"⋀x it σ. ⟦ x∈S; it⊆S; I it σ ⟧ ⟹ f x ≤ SPEC (λf'. c σ f' ≤ SPEC (I (insert x it)))"
assumes II: "⋀σ. I S σ ⟹ P σ"
shows "FORWEAK S d f c ≤ SPEC P"
apply (rule FORWEAK_invarI[where I="λb X. X ⊆ S ∧ I (S - X) b"])
subgoal by (rule empty)
subgoal by (auto simp: Diff_Diff_Int intro!: I0)
subgoal
apply (rule I0, assumption)
apply (rule SPEC_rule)
apply (rule conjI)
subgoal by simp
subgoal by (rule I_mono, assumption) auto
done
subgoal for a b it
apply (rule IP[of _ "S - it" b])
subgoal by force
subgoal by force
subgoal by force
subgoal
apply clarsimp
apply (rule order_trans, assumption)
by (auto simp: it_step_insert_iff intro: order_trans)
done
subgoal for a b it
apply (rule IP[of _ "S - it" b])
subgoal by force
subgoal by force
subgoal by force
subgoal
apply clarsimp
apply (rule order_trans, assumption)
by (auto simp: it_step_insert_iff intro: I_mono)
done
subgoal by (auto intro!: II)
done

lemma
op_set_npick_remove_refine_SPEC[refine_vcg]:
assumes "⋀x X'. x ∈ X1 ⟹ X' = X1 - {x} ⟹ Q (x, X')"
assumes "⋀x. x ∈ X1 ⟹ Q (x, X1)"
shows "op_set_npick_remove X1 ≤ SPEC Q"
using assms
by (auto simp: op_set_npick_remove_def )

context includes autoref_syntax begin
definition "op_set_pick_remove X ≡ SPEC (λ(x, X'). x ∈ X ∧ X' = X - {x})"
lemma op_set_pick_removepat[autoref_op_pat]:
"SPEC (λ(x, X'). x ∈ X ∧ X' = X - {x}) ≡ op_set_pick_remove \$ X"
"do { x ← SPEC (λx. x ∈ X); let X' = X - {x}; f x X' } ≡ do { (x, X') ← op_set_pick_remove X; f x X'}"
by (auto simp: op_set_pick_remove_def pw_eq_iff refine_pw_simps intro!: eq_reflection)

lemma list_all2_tlI: "list_all2 A XS y ⟹ list_all2 A (tl XS) (tl y)"
by (metis list.rel_sel list.sel(2))

lemma
op_set_pick_remove_refine[autoref_rules]:
assumes "(XS, X) ∈ ⟨A⟩list_set_rel"
assumes "SIDE_PRECOND (X ≠ {})"
shows "(nres_of (dRETURN (hd XS, tl XS)), op_set_pick_remove \$ X) ∈ ⟨A ×⇩r ⟨A⟩list_set_rel⟩nres_rel"
using assms(1)
unfolding op_set_pick_remove_def[abs_def] autoref_tag_defs list_set_rel_def list_rel_def br_def
apply (intro nres_relI SPEC_refine det_SPEC)
apply safe
subgoal for x y z
using assms(2)
apply (safe intro!: exI[where x="(hd y, set (tl y))"])
subgoal
apply (rule prod_relI)
subgoal by (induct XS y rule: list_all2_induct) auto
subgoal
apply (rule relcompI[where b = "tl y"])
subgoal
unfolding mem_Collect_eq split_beta' fst_conv snd_conv
by (rule list_all2_tlI)
subgoal
unfolding mem_Collect_eq split_beta' fst_conv snd_conv
apply (rule conjI)
subgoal by (metis remove1_tl set_remove1_eq)
subgoal by simp
done
done
done
subgoal by (subst (asm) list.rel_sel) simp
subgoal by (simp add: in_set_tlD)
subgoal by (simp add: distinct_hd_tl)
subgoal by auto (meson in_hd_or_tl_conv)
done
done

definition [simp, refine_vcg_def]: "isEmpty_spec X = SPEC (λb. b ⟶ X = {})"

lemma [autoref_itype]: "isEmpty_spec::⇩i A →⇩i ⟨i_bool⟩⇩ii_nres"
by simp
lemma op_wset_isEmpty_list_wset_rel[autoref_rules]:
"(λx. RETURN (x = []), isEmpty_spec) ∈ ⟨A⟩list_wset_rel → ⟨bool_rel⟩nres_rel"
by (auto simp: nres_rel_def list_wset_rel_def set_rel_def br_def)

definition WEAK_ALL:: "('a ⇒ bool) ⇒ 'a set ⇒ ('a ⇒ bool nres) ⇒ bool nres" ("WEAK'_ALL⇗_⇖") where
"WEAK_ALL I X P = do {
(_, b) ← WHILE⇗λ(Y, b). b ⟶ (∀x ∈ X - Y. I x)⇖ (λ(X, b). b ∧ X ≠ {}) (λ(X, b). do {
ASSERT (X ≠ {});
(x, X') ← op_set_npick_remove X;
b' ← P x;
RETURN (X', b' ∧ b)
}) (X, True); RETURN b}"
schematic_goal WEAK_ALL_list[autoref_rules]:
assumes [relator_props]: "single_valued A"
assumes [autoref_rules]: "(Xi, X) ∈ ⟨A⟩list_wset_rel"
"(P_impl, P) ∈ A → ⟨bool_rel⟩nres_rel"
shows "(?r, WEAK_ALL I X P) ∈ ⟨bool_rel⟩nres_rel"
unfolding WEAK_ALL_def
including art
by (autoref)
concrete_definition WEAK_ALL_list for Xi P_impl uses WEAK_ALL_list
lemma WEAK_ALL_list_refine[autoref_rules]:
"PREFER single_valued A ⟹ (WEAK_ALL_list, WEAK_ALL I) ∈ ⟨A⟩list_wset_rel → (A → ⟨bool_rel⟩nres_rel) → ⟨bool_rel⟩nres_rel"
using WEAK_ALL_list.refine by force

schematic_goal WEAK_ALL_transfer_nres:
assumes [refine_transfer]: "⋀x. nres_of (f x) ≤ f' x"
shows "nres_of (?f) ≤ WEAK_ALL_list xs f'"
unfolding WEAK_ALL_list_def
by refine_transfer
concrete_definition dWEAK_ALL for xs f uses WEAK_ALL_transfer_nres
lemmas [refine_transfer] = dWEAK_ALL.refine

definition WEAK_EX:: "('a ⇒ bool) ⇒ 'a set ⇒ ('a ⇒ bool nres) ⇒ bool nres" ("WEAK'_EX⇗_⇖") where
"WEAK_EX I X P = do {
(_, b) ← WHILE⇗λ(Y, b). Y ⊆ X ∧ (b ⟶ (∃x ∈ X. I x))⇖ (λ(X, b). ¬b ∧ X ≠ {}) (λ(X, b). do {
ASSERT (X ≠ {});
(x, X') ← op_set_npick_remove X;
b' ← P x;
RETURN (X', b' ∨ b)
}) (X, False); RETURN b}"
schematic_goal WEAK_EX_list[autoref_rules]:
assumes [relator_props]: "single_valued A"
assumes [autoref_rules]: "(Xi, X) ∈ ⟨A⟩list_wset_rel"
"(P_impl, P) ∈ A → ⟨bool_rel⟩nres_rel"
shows "(?r, WEAK_EX I X P) ∈ ⟨bool_rel⟩nres_rel"
unfolding WEAK_EX_def
including art
by (autoref)
concrete_definition WEAK_EX_list for Xi P_impl uses WEAK_EX_list
lemma WEAK_EX_list_refine[autoref_rules]:
"PREFER single_valued A ⟹ (WEAK_EX_list, WEAK_EX I) ∈ ⟨A⟩list_wset_rel → (A → ⟨bool_rel⟩nres_rel) → ⟨bool_rel⟩nres_rel"
using WEAK_EX_list.refine by force

schematic_goal WEAK_EX_transfer_nres:
assumes [refine_transfer]: "⋀x. nres_of (f x) ≤ f' x"
shows "nres_of (?f) ≤ WEAK_EX_list xs f'"
unfolding WEAK_EX_list_def
by refine_transfer
concrete_definition dWEAK_EX for xs f uses WEAK_EX_transfer_nres
lemmas [refine_transfer] = dWEAK_EX.refine

lemma WEAK_EX[THEN order_trans, refine_vcg]:
assumes [THEN order_trans, refine_vcg]: "⋀x. F x ≤ SPEC (λr. r ⟶ I x)"
shows "WEAK_EX I X F ≤ SPEC (λr. r ⟶ (∃x∈X. I x))"
unfolding WEAK_EX_def
by (refine_vcg ) auto

lemma WEAK_ALL[THEN order_trans, refine_vcg]:
assumes [THEN order_trans, refine_vcg]: "⋀x. F x ≤ SPEC (λr. r ⟶ I x)"
shows "WEAK_ALL I X F ≤ SPEC (λr. r ⟶ (∀x∈X. I x))"
unfolding WEAK_ALL_def
by (refine_vcg) auto

lemma [autoref_op_pat_def]:
"WEAK_ALL I ≡ OP (WEAK_ALL I)"
"WEAK_EX I ≡ OP (WEAK_EX I)"
by auto

lemma list_spec_impl[autoref_rules]:
"(λx. RETURN x, list_spec) ∈ ⟨A⟩list_wset_rel → ⟨⟨A⟩list_rel⟩nres_rel"
if "PREFER single_valued A"
using that
apply (auto simp: list_spec_def nres_rel_def RETURN_RES_refine_iff list_wset_rel_br_eq
br_list_rel intro!: brI dest!: brD
elim!: single_valued_as_brE)
subgoal for a I xs
apply (rule exI[where x="map a xs"])
by (auto simp: br_def list_all_iff)
done

lemma list_wset_autoref_delete[autoref_rules]:
assumes "PREFER single_valued R"
assumes "GEN_OP eq (=) (R → R → bool_rel)"
shows "(λy xs. [x←xs. ¬eq y x], op_set_delete) ∈ R → ⟨R⟩list_wset_rel → ⟨R⟩list_wset_rel"
using assms
apply (auto simp: list_wset_rel_def dest!: brD elim!: single_valued_as_brE)
apply (rule relcompI)
apply (rule brI)
apply (rule refl)
apply auto
apply (auto simp: set_rel_br)
apply (rule brI)
apply (auto dest!: brD dest: fun_relD)
apply (auto simp: image_iff dest: fun_relD intro: brI)
subgoal for a b c d e
apply (drule spec[where x=e])
apply auto
apply (drule fun_relD)
apply (rule brI[where c="c"])
apply (rule refl)
apply assumption
apply (drule bspec, assumption)
apply (drule fun_relD)
apply (rule brI[where c="e"])
apply (rule refl)
apply assumption
apply auto
done
done

lemma FORWEAK_mono_rule'':
fixes f::"'d ⇒ 'e nres" and c::"'e ⇒ 'e ⇒ 'e nres" and I::"'d set ⇒ 'e ⇒ bool"
assumes empty: "S = {} ⟹ d ≤ SPEC P"
assumes I0[THEN order_trans]: "⋀s. s ∈ S ⟹ f s ≤ SPEC (I {s})"
assumes I_mono: "⋀it it' σ. I it σ ⟹ it' ⊆ it ⟹ it ⊆ S ⟹ I it' σ"
assumes IP[THEN order_trans]:
"⋀x it σ. ⟦ x∈S; x ∉ it; it⊆S; I it σ ⟧ ⟹ f x ≤ SPEC (λf'. c σ f' ≤ SPEC (I (insert x it)))"
assumes II: "⋀σ. I S σ ⟹ P σ"
shows "FORWEAK S d f c ≤ SPEC P"
apply (rule FORWEAK_invarI[where I="λb X. X ⊆ S ∧ I (S - X) b"])
subgoal by (rule empty)
subgoal by (auto simp: Diff_Diff_Int intro!: I0)
subgoal
by (metis (mono_tags, lifting) Diff_cancel I0 I_mono Refine_Basic.RES_sng_eq_RETURN iSPEC_rule
less_eq_nres.simps(2) nres_order_simps(21) subset_insertI subset_refl)
subgoal for a b it
apply (rule IP[of _ "S - it" b])
subgoal by force
subgoal by force
subgoal by force
subgoal by force
subgoal
apply clarsimp
apply (rule order_trans, assumption)
by (auto simp: it_step_insert_iff intro: order_trans)
done
subgoal for a b it
apply (rule IP[of _ "S - it" b])
subgoal by force
subgoal by force
subgoal by force
subgoal by force
subgoal
apply clarsimp
apply (rule order_trans, assumption)
by (auto simp: it_step_insert_iff intro: I_mono)
done
subgoal by (auto intro!: II)
done

lemma FORWEAK_mono_rule_empty:
fixes f::"'d ⇒ 'e nres" and c::"'e ⇒ 'e ⇒ 'e nres" and I::"'d set ⇒ 'e ⇒ bool"
assumes empty: "S = {} ⟹ RETURN d ≤ SPEC P"
assumes I0: "I {} d"
assumes I1: "⋀s x. s ∈ S ⟹ c d x ≤ SPEC (I {s}) ⟹ I {s} x"
assumes I_mono: "⋀it it' σ. I it σ ⟹ it' ⊆ it ⟹ it ⊆ S ⟹ I it' σ"
assumes II: "⋀σ. I S σ ⟹ P σ"
assumes IP: "⋀x it σ. ⟦ x∈S; x ∉ it; it⊆S; I it σ ⟧ ⟹ f x ≤ SPEC (λf'. c σ f' ≤ SPEC (I (insert x it)))"
shows "FORWEAK S (RETURN d) f c ≤ SPEC P"
apply (rule FORWEAK_mono_rule''[where S=S and I=I and P=P])
subgoal by (rule empty)
subgoal for s
apply (rule IP[of _ "{}" d, THEN order_trans])
apply assumption
apply force
apply force
apply (rule I0)
by (auto intro!: I1)
subgoal by (rule I_mono)
subgoal by (rule IP)
subgoal by (rule II)
done

end

end
```