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