Theory WB_More_Refinement

theory WB_More_Refinement
imports WB_List_More Cardinality Rewrite Refine_Foreach
theory WB_More_Refinement
  imports Weidenbach_Book_Base.WB_List_More
    "HOL-Library.Cardinality"
    "HOL-Library.Rewrite"
    "HOL-Eisbach.Eisbach"
    Refine_Monadic.Refine_Basic
    Automatic_Refinement.Automatic_Refinement
    Automatic_Refinement.Relators
    Refine_Monadic.Refine_While
    Refine_Monadic.Refine_Foreach
begin
(*
  term ‹a →f b›
no_notation fref ("[_]f _ → _" [0,60,60] 60)
no_notation freft ("_ →f _" [60,60] 60) *)

hide_const Autoref_Fix_Rel.CONSTRAINT

definition fref :: "('c ⇒ bool) ⇒ ('a × 'c) set ⇒ ('b × 'd) set
           ⇒ (('a ⇒ 'b) × ('c ⇒ 'd)) set"
    ("[_]f _ → _" [0,60,60] 60)
  where "[P]f R → S ≡ {(f,g). ∀x y. P y ∧ (x,y)∈R ⟶ (f x, g y)∈S}"

abbreviation freft ("_ →f _" [60,60] 60) where "R →f S ≡ ([λ_. True]f R → S)"

lemma frefI[intro?]:
  assumes "⋀x y. ⟦P y; (x,y)∈R⟧ ⟹ (f x, g y)∈S"
  shows "(f,g)∈fref P R S"
  using assms
  unfolding fref_def
  by auto
lemma fref_mono: "⟦ ⋀x. P' x ⟹ P x; R' ⊆ R; S ⊆ S' ⟧
    ⟹ fref P R S ⊆ fref P' R' S'"
    unfolding fref_def
    by auto blast

(* taken from IICF*)
lemma meta_same_imp_rule: "(⟦PROP P; PROP P⟧ ⟹ PROP Q) ≡ (PROP P ⟹ PROP Q)"
  by rule
lemma split_prod_bound: "(λp. f p) = (λ(a,b). f (a,b))" by auto

text ‹This lemma cannot be moved to \<^theory>‹Weidenbach_Book_Base.WB_List_More›, because the syntax
 \<^term>‹CARD('a)› does not exist there.›
lemma finite_length_le_CARD:
  assumes ‹distinct (xs :: 'a :: finite list)›
  shows ‹length xs ≤ CARD('a)›
proof -
  have ‹set xs ⊆ UNIV›
    by auto
  show ?thesis
    by (metis assms card_ge_UNIV distinct_card le_cases)
qed


subsection ‹Some Tooling for Refinement›

text ‹
  The following very simple tactics remove duplicate variables generated by some tactic like
  ‹refine_rcg›. For example, if the problem contains \<^term>‹(i, C) = (xa, xb)›, then only
  \<^term>‹i› and \<^term>‹C› will remain. It can also prove trivial goals where the goals already
  appears in the assumptions.
  ›

method remove_dummy_vars uses simps =
  ((unfold prod.inject)?; (simp only: prod.inject)?; (elim conjE)?;
    hypsubst?; (simp only: triv_forall_equality simps)?)


subsubsection ‹From @{text →} to @{text ⇓}›

lemma Ball2_split_def: ‹(∀(x, y) ∈ A. P x y) ⟷ (∀x y. (x, y) ∈ A ⟶ P x y)›
  by blast

lemma in_pair_collect_simp: "(a,b)∈{(a,b). P a b} ⟷ P a b"
  by auto

ML ‹
signature MORE_REFINEMENT = sig
  val down_converse: Proof.context -> thm -> thm
end

structure More_Refinement: MORE_REFINEMENT = struct
  val unfold_refine = (fn context => Local_Defs.unfold (context)
   @{thms refine_rel_defs nres_rel_def in_pair_collect_simp})
  val unfold_Ball = (fn context => Local_Defs.unfold (context)
    @{thms Ball2_split_def all_to_meta})
  val replace_ALL_by_meta = (fn context => fn thm => Object_Logic.rulify context thm)
  val down_converse = (fn context =>
    replace_ALL_by_meta context o (unfold_Ball context) o (unfold_refine context))
end
›

attribute_setup "to_⇓" = ‹
    Scan.succeed (Thm.rule_attribute [] (More_Refinement.down_converse o Context.proof_of))
  › "convert theorem from @{text →}-form to @{text ⇓}-form."

method "to_⇓" =
   (unfold refine_rel_defs nres_rel_def in_pair_collect_simp;
   unfold Ball2_split_def all_to_meta;
   intro allI impI)


subsubsection ‹Merge Post-Conditions›

lemma Down_add_assumption_middle:
  assumes
    ‹nofail U› and
    ‹V ≤ ⇓ {(T1, T0). Q T1 T0 ∧ P T1 ∧ Q' T1 T0} U› and
    ‹W ≤ ⇓ {(T2, T1). R T2 T1} V›
  shows ‹W ≤ ⇓ {(T2, T1). R T2 T1 ∧ P T1} V›
  using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
  by blast

lemma Down_del_assumption_middle:
  assumes
    ‹S1 ≤ ⇓ {(T1, T0). Q T1 T0 ∧ P T1 ∧ Q' T1 T0} S0›
  shows ‹S1 ≤ ⇓ {(T1, T0). Q T1 T0 ∧ Q' T1 T0} S0›
  using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
  by blast

lemma Down_add_assumption_beginning:
  assumes
    ‹nofail U› and
    ‹V ≤ ⇓ {(T1, T0). P T1 ∧ Q' T1 T0} U› and
    ‹W ≤ ⇓ {(T2, T1). R T2 T1} V›
  shows ‹W ≤ ⇓ {(T2, T1). R T2 T1 ∧ P T1} V›
  using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
  by blast

lemma Down_add_assumption_beginning_single:
  assumes
    ‹nofail U› and
    ‹V ≤ ⇓ {(T1, T0). P T1} U› and
    ‹W ≤ ⇓ {(T2, T1). R T2 T1} V›
  shows ‹W ≤ ⇓ {(T2, T1). R T2 T1 ∧ P T1} V›
  using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
  by blast

lemma Down_del_assumption_beginning:
  fixes U :: ‹'a nres› and V :: ‹'b nres› and Q Q' :: ‹'b ⇒ 'a ⇒ bool›
  assumes
    ‹V ≤ ⇓ {(T1, T0). Q T1 T0 ∧ Q' T1 T0} U›
  shows ‹V ≤ ⇓ {(T1, T0). Q' T1 T0} U›
  using assms unfolding nres_rel_def fun_rel_def pw_le_iff pw_conc_inres pw_conc_nofail
  by blast

method unify_Down_invs2_normalisation_post =
  ((unfold meta_same_imp_rule True_implies_equals conj_assoc)?)

method unify_Down_invs2 =
  (match premises in
      ― ‹if the relation 2-1 has not assumption, we add True. Then we call out method again and
           this time it will match since it has an assumption.›
      I: ‹S1 ≤ ⇓ R10 S0› and
      J[thin]: ‹S2 ≤ ⇓ R21 S1›
       for S1:: ‹'b nres› and S0 :: ‹'a nres› and S2 :: ‹'c nres› and R10 R21 
        ‹insert True_implies_equals[where P = ‹S2 ≤ ⇓ R21 S1›, symmetric,
           THEN equal_elim_rule1, OF J]›
    ¦ I[thin]: ‹S1 ≤ ⇓ {(T1, T0). P T1} S0› (multi) and
      J[thin]: _ for S1:: ‹'b nres› and S0 :: ‹'a nres› and P :: ‹'b ⇒ bool› 
       ‹match J[uncurry] in
         J[curry]: ‹_ ⟹ S2 ≤ ⇓ {(T2, T1). R T2 T1} S1› for S2 :: ‹'c nres› and R ⇒
          ‹insert Down_add_assumption_beginning_single[where P = P and R = R and
               W = S2 and V = S1 and U = S0, OF _ I J];
           unify_Down_invs2_normalisation_post›
       ¦ _ ⇒ ‹fail››
   ¦ I[thin]: ‹S1 ≤ ⇓ {(T1, T0). P T1 ∧ Q' T1 T0} S0› (multi) and
     J[thin]: _ for S1:: ‹'b nres› and S0 :: ‹'a nres› and Q' and P :: ‹'b ⇒ bool› 
       ‹match J[uncurry] in
         J[curry]: ‹_ ⟹ S2 ≤ ⇓ {(T2, T1). R T2 T1} S1› for S2 :: ‹'c nres› and R ⇒
          ‹insert Down_add_assumption_beginning[where Q' = Q' and P = P and R = R and
              W = S2 and V = S1 and U = S0,
              OF _ I J];
           insert Down_del_assumption_beginning[where Q = ‹λS _. P S› and Q' = Q' and V = S1 and
             U = S0, OF I];
          unify_Down_invs2_normalisation_post›
       ¦ _ ⇒ ‹fail››
   ¦ I[thin]: ‹S1 ≤ ⇓ {(T1, T0). Q T0 T1∧ Q' T1 T0} S0› (multi) and
     J: _ for S1:: ‹'b nres› and S0 :: ‹'a nres› and Q Q' 
       ‹match J[uncurry] in
         J[curry]: ‹_ ⟹ S2 ≤ ⇓ {(T2, T1). R T2 T1} S1› for S2 :: ‹'c nres› and R ⇒
          ‹insert Down_del_assumption_beginning[where Q = ‹λ x y. Q y x› and Q' = Q', OF I];
           unify_Down_invs2_normalisation_post›
       ¦ _ ⇒ ‹fail››
  )

text ‹Example:›
lemma
  assumes
    ‹nofail S0› and
    1: ‹S1 ≤ ⇓ {(T1, T0). Q T1 T0 ∧ P T1 ∧ P' T1 ∧ P''' T1 ∧ Q' T1 T0 ∧ P42 T1} S0› and
    2: ‹S2 ≤ ⇓ {(T2, T1). R T2 T1} S1›
  shows ‹S2
     ≤ ⇓ {(T2, T1).
           R T2 T1 ∧
           P T1 ∧ P' T1 ∧ P''' T1 ∧ P42 T1}
         S1›
  using assms apply -
  apply unify_Down_invs2+
  apply fast
  done

subsubsection ‹Inversion Tactics›

lemma refinement_trans_long:
  ‹A = A' ⟹ B = B' ⟹ R ⊆ R' ⟹ A ≤ ⇓ R B ⟹ A' ≤ ⇓ R' B'›
  by (meson pw_ref_iff subsetCE)

lemma mem_set_trans:
  ‹A ⊆ B ⟹ a ∈ A ⟹ a ∈ B›
  by auto

lemma fun_rel_syn_invert:
  ‹a = a' ⟹ b ⊆ b' ⟹ a → b ⊆ a' → b'›
  by (auto simp: refine_rel_defs)

lemma fref_param1: "R→S = fref (λ_. True) R S"
  by (auto simp: fref_def fun_relD)

lemma fref_syn_invert:
  ‹a = a' ⟹ b ⊆ b' ⟹ a →f b ⊆ a' →f b'›
  unfolding fref_param1[symmetric]
  by (rule fun_rel_syn_invert)

lemma nres_rel_mono:
  ‹a ⊆ a'  ⟹ ⟨a⟩ nres_rel ⊆ ⟨a'⟩ nres_rel›
  by (fastforce simp: refine_rel_defs nres_rel_def pw_ref_iff)

method match_spec =
  (match conclusion in ‹(f, g) ∈ R› for f g R 
    ‹print_term f; match premises in I[thin]: ‹(f, g) ∈ R'› for R'
       ⇒ ‹print_term R'; rule mem_set_trans[OF _ I]››)

method match_fun_rel =
  ((match conclusion in
       ‹_ → _ ⊆ _ → _›  ‹rule fun_rel_mono›
     ¦ ‹_ →f _ ⊆ _ →f _›  ‹rule fref_syn_invert›
     ¦ ‹⟨_⟩nres_rel ⊆ ⟨_⟩nres_rel›  ‹rule nres_rel_mono›
     ¦ ‹[_]f _ → _ ⊆ [_]f _ → _›  ‹rule fref_mono›
   )+)

lemma weaken_SPEC2: ‹m' ≤ SPEC Φ ⟹ m = m' ⟹ (⋀x. Φ x ⟹ Ψ x) ⟹ m ≤ SPEC Ψ›
  using weaken_SPEC by auto

method match_spec_trans =
  (match conclusion in ‹f ≤ SPEC R› for f :: ‹'a nres› and R :: ‹'a ⇒ bool› 
    ‹print_term f; match premises in I: ‹_ ⟹ _ ⟹ f' ≤ SPEC R'› for f' :: ‹'a nres› and R' :: ‹'a ⇒ bool›
       ⇒ ‹print_term f'; rule weaken_SPEC2[of f' R' f R]››)


subsection ‹More Notations›

abbreviation "uncurry2 f ≡ uncurry (uncurry f)"
abbreviation "curry2 f ≡ curry (curry f)"
abbreviation "uncurry3 f ≡ uncurry (uncurry2 f)"
abbreviation "curry3 f ≡ curry (curry2 f)"
abbreviation "uncurry4 f ≡ uncurry (uncurry3 f)"
abbreviation "curry4 f ≡ curry (curry3 f)"
abbreviation "uncurry5 f ≡ uncurry (uncurry4 f)"
abbreviation "curry5 f ≡ curry (curry4 f)"
abbreviation "uncurry6 f ≡ uncurry (uncurry5 f)"
abbreviation "curry6 f ≡ curry (curry5 f)"
abbreviation "uncurry7 f ≡ uncurry (uncurry6 f)"
abbreviation "curry7 f ≡ curry (curry6 f)"
abbreviation "uncurry8 f ≡ uncurry (uncurry7 f)"
abbreviation "curry8 f ≡ curry (curry7 f)"
abbreviation "uncurry9 f ≡ uncurry (uncurry8 f)"
abbreviation "curry9 f ≡ curry (curry8 f)"
abbreviation "uncurry10 f ≡ uncurry (uncurry9 f)"
abbreviation "curry10 f ≡ curry (curry9 f)"
abbreviation "uncurry11 f ≡ uncurry (uncurry10 f)"
abbreviation "curry11 f ≡ curry (curry10 f)"
abbreviation "uncurry12 f ≡ uncurry (uncurry11 f)"
abbreviation "curry12 f ≡ curry (curry11 f)"
abbreviation "uncurry13 f ≡ uncurry (uncurry12 f)"
abbreviation "curry13 f ≡ curry (curry12 f)"
abbreviation "uncurry14 f ≡ uncurry (uncurry13 f)"
abbreviation "curry14 f ≡ curry (curry13 f)"
abbreviation "uncurry15 f ≡ uncurry (uncurry14 f)"
abbreviation "curry15 f ≡ curry (curry14 f)"
abbreviation "uncurry16 f ≡ uncurry (uncurry15 f)"
abbreviation "curry16 f ≡ curry (curry15 f)"
abbreviation "uncurry17 f ≡ uncurry (uncurry16 f)"
abbreviation "curry17 f ≡ curry (curry16 f)"
abbreviation "uncurry18 f ≡ uncurry (uncurry17 f)"
abbreviation "curry18 f ≡ curry (curry17 f)"
abbreviation "uncurry19 f ≡ uncurry (uncurry18 f)"
abbreviation "curry19 f ≡ curry (curry18 f)"
abbreviation "uncurry20 f ≡ uncurry (uncurry19 f)"
abbreviation "curry20 f ≡ curry (curry19 f)"


abbreviation comp4  (infixl "oooo" 55)       where "f oooo g ≡       λx. f ooo (g x)"
abbreviation comp5  (infixl "ooooo" 55)      where "f ooooo g ≡      λx. f oooo (g x)"
abbreviation comp6  (infixl "oooooo" 55)     where "f oooooo g ≡     λx. f ooooo (g x)"
abbreviation comp7  (infixl "ooooooo" 55)    where "f ooooooo g ≡    λx. f oooooo (g x)"
abbreviation comp8  (infixl "oooooooo" 55)   where "f oooooooo g ≡   λx. f ooooooo (g x)"
abbreviation comp9  (infixl "ooooooooo" 55)  where "f ooooooooo g ≡  λx. f oooooooo (g x)"
abbreviation comp10 (infixl "oooooooooo" 55) where "f oooooooooo g ≡ λx. f ooooooooo (g x)"
abbreviation comp11 (infixl "o11" 55) where "f o11 g ≡ λx. f oooooooooo (g x)"
abbreviation comp12 (infixl "o12" 55) where "f o12 g ≡ λx. f o11 (g x)"
abbreviation comp13 (infixl "o13" 55) where "f o13 g ≡ λx. f o12 (g x)"
abbreviation comp14 (infixl "o14" 55) where "f o14 g ≡ λx. f o13 (g x)"
abbreviation comp15 (infixl "o15" 55) where "f o15 g ≡ λx. f o14 (g x)"
abbreviation comp16 (infixl "o16" 55) where "f o16 g ≡ λx. f o15 (g x)"
abbreviation comp17 (infixl "o17" 55) where "f o17 g ≡ λx. f o16 (g x)"
abbreviation comp18 (infixl "o18" 55) where "f o18 g ≡ λx. f o17 (g x)"
abbreviation comp19 (infixl "o19" 55) where "f o19 g ≡ λx. f o18 (g x)"
abbreviation comp20 (infixl "o20" 55) where "f o20 g ≡ λx. f o19 (g x)"

notation
  comp4 (infixl "∘∘∘" 55) and
  comp5 (infixl "∘∘∘∘" 55) and
  comp6 (infixl "∘∘∘∘∘" 55) and
  comp7 (infixl "∘∘∘∘∘∘" 55) and
  comp8 (infixl "∘∘∘∘∘∘∘" 55) and
  comp9 (infixl "∘∘∘∘∘∘∘∘" 55) and
  comp10 (infixl "∘∘∘∘∘∘∘∘∘" 55) and
  comp11 (infixl "∘11" 55) and
  comp12 (infixl "∘12" 55) and
  comp13 (infixl "∘13" 55) and
  comp14 (infixl "∘14" 55) and
  comp15 (infixl "∘15" 55) and
  comp16 (infixl "∘16" 55) and
  comp17 (infixl "∘17" 55) and
  comp18 (infixl "∘18" 55) and
  comp19 (infixl "∘19" 55) and
  comp20 (infixl "∘20" 55)


subsection ‹More Theorems for Refinement›

lemma SPEC_add_information: ‹P ⟹ A ≤ SPEC Q ⟹ A ≤ SPEC(λx. Q x ∧ P)›
  by auto

lemma bind_refine_spec: ‹(⋀x. Φ x ⟹ f x ≤ ⇓ R M) ⟹ M' ≤ SPEC Φ ⟹ M' ⤜ f ≤ ⇓ R M›
  by (auto simp add: pw_le_iff refine_pw_simps)

lemma intro_spec_iff:
  ‹(RES X ⤜ f ≤ M) = (∀x∈X. f x ≤ M)›
  using intro_spec_refine_iff[of X f Id M] by auto

lemma case_prod_bind:
  assumes ‹⋀x1 x2. x = (x1, x2) ⟹ f x1 x2 ≤ ⇓ R I›
  shows ‹(case x of (x1, x2) ⇒ f x1 x2) ≤ ⇓ R I›
  using assms by (cases x) auto

lemma (in transfer) transfer_bool[refine_transfer]:
  assumes "α fa ≤ Fa"
  assumes "α fb ≤ Fb"
  shows "α (case_bool fa fb x) ≤ case_bool Fa Fb x"
  using assms by (auto split: bool.split)

lemma ref_two_step': ‹A ≤ B ⟹ ⇓ R A ≤  ⇓ R B›
  by (auto intro: ref_two_step)

lemma RES_RETURN_RES: ‹RES Φ ⤜ (λT. RETURN (f T)) = RES (f ` Φ)›
  by (simp add: bind_RES_RETURN_eq setcompr_eq_image)

lemma RES_RES_RETURN_RES: ‹RES A ⤜ (λT. RES (f T)) = RES (⋃(f ` A))›
  by (auto simp:  pw_eq_iff refine_pw_simps)

lemma RES_RES2_RETURN_RES: ‹RES A ⤜ (λ(T, T'). RES (f T T')) = RES (⋃(uncurry f ` A))›
  by (auto simp:  pw_eq_iff refine_pw_simps uncurry_def)

lemma RES_RES3_RETURN_RES:
   ‹RES A ⤜ (λ(T, T', T''). RES (f T T' T'')) = RES (⋃((λ(a, b, c). f a b c) ` A))›
  by (auto simp:  pw_eq_iff refine_pw_simps uncurry_def)

lemma RES_RETURN_RES3:
   ‹SPEC Φ ⤜ (λ(T, T', T''). RETURN (f T T' T'')) = RES ((λ(a, b, c). f a b c) ` {T. Φ T})›
  using RES_RETURN_RES[of ‹Collect Φ› ‹λ(a, b, c). f a b c›]
  apply (subst (asm)(2) split_prod_bound)
  apply (subst (asm)(3) split_prod_bound)
  by auto

lemma RES_RES_RETURN_RES2: ‹RES A ⤜ (λ(T, T'). RETURN (f T T')) = RES (uncurry f ` A)›
  by (auto simp:  pw_eq_iff refine_pw_simps uncurry_def)

lemma bind_refine_res: ‹(⋀x. x ∈ Φ ⟹ f x ≤ ⇓ R M) ⟹ M' ≤ RES Φ ⟹ M' ⤜ f ≤ ⇓ R M›
  by (auto simp add: pw_le_iff refine_pw_simps)

lemma RES_RETURN_RES_RES2:
   ‹RES Φ ⤜ (λ(T, T'). RETURN (f T T')) = RES (uncurry f ` Φ)›
  using RES_RES2_RETURN_RES[of ‹Φ› ‹λT T'. {f T T'}›]
  apply (subst (asm)(2) split_prod_bound)
  by (auto simp: RETURN_def uncurry_def)

text ‹
  This theorem adds the invariant at the beginning of next iteration to the current invariant,
  i.e., the invariant is added as a post-condition on the current iteration.

  This is useful to reduce duplication in theorems while refining.
›

lemma RECT_WHILEI_body_add_post_condition:
    ‹RECT (WHILEI_body (⤜) RETURN I' b' f) x' =
     (RECT (WHILEI_body (⤜) RETURN (λx'. I' x' ∧ (b' x' ⟶ f x' = FAIL ∨ f x' ≤ SPEC I')) b' f) x')›
  (is ‹RECT ?f x' = RECT ?f' x'›)
proof -
  have le: ‹flatf_gfp ?f x' ≤ flatf_gfp ?f' x'› for x'
  proof (induct arbitrary: x' rule: flatf_ord.fixp_induct[where b = top and
        f = ?f'])
    case 1
    then show ?case
      unfolding fun_lub_def pw_le_iff
      by (rule ccpo.admissibleI)
        (smt chain_fun flat_lub_in_chain mem_Collect_eq nofail_simps(1))
  next
    case 2
    then show ?case by (auto simp: WHILEI_mono_ge)
  next
    case 3
    then show ?case by simp
  next
    case (4 x)
    have  ‹(RES X ⤜ f ≤ M) = (∀x∈X. f x ≤ M)› for x f M X
      using intro_spec_refine_iff[of _ _ ‹Id›] by auto
    thm bind_refine_RES(2)[of _ Id, simplified]
    have [simp]: ‹flatf_mono FAIL (WHILEI_body (⤜) RETURN I' b' f)›
      by (simp add: WHILEI_mono_ge)

    have ‹flatf_gfp ?f x' = ?f (?f (flatf_gfp ?f)) x'›
      apply (subst flatf_ord.fixp_unfold)
       apply (solves ‹simp›)
      apply (subst flatf_ord.fixp_unfold)
       apply (solves ‹simp›)
      ..
    also have ‹… = WHILEI_body (⤜) RETURN (λx'. I' x' ∧ (b' x' ⟶ f x' = FAIL ∨ f x' ≤ SPEC I')) b' f (WHILEI_body (⤜) RETURN I' b' f (flatf_gfp (WHILEI_body (⤜) RETURN I' b' f))) x'›
      apply (subst (1) WHILEI_body_def, subst (1) WHILEI_body_def)
      apply (subst (2) WHILEI_body_def, subst (2) WHILEI_body_def)
      apply simp_all
      apply (cases ‹f x'›)
       apply (auto simp: RES_RETURN_RES nofail_def[symmetric] pw_RES_bind_choose
          split: if_splits)
      done
    also have ‹… =  WHILEI_body (⤜) RETURN (λx'. I' x' ∧ (b' x' ⟶ f x' = FAIL ∨ f x' ≤ SPEC I')) b' f ((flatf_gfp (WHILEI_body (⤜) RETURN I' b' f))) x'›
      apply (subst (2) flatf_ord.fixp_unfold)
       apply (solves ‹simp›)
      ..
    finally have unfold1: ‹flatf_gfp (WHILEI_body (⤜) RETURN I' b' f) x' =
         ?f' (flatf_gfp (WHILEI_body (⤜) RETURN I' b' f)) x'›
      .
    have [intro!]: ‹(⋀x. g x ≤ (h:: 'a ⇒ 'a nres) x) ⟹ fx ⤜ g ≤ fx ⤜ h› for g h fx fy
      by (refine_rcg bind_refine'[where R = ‹Id›, simplified]) fast
    show ?case
      apply (subst unfold1)
      using 4 unfolding WHILEI_body_def by auto
  qed

  have ge: ‹flatf_gfp ?f x' ≥  flatf_gfp ?f' x'› for x'
  proof (induct arbitrary: x' rule: flatf_ord.fixp_induct[where b = top and
        f = ?f])
    case 1
    then show ?case
      unfolding fun_lub_def pw_le_iff
      by (rule ccpo.admissibleI) (smt chain_fun flat_lub_in_chain mem_Collect_eq nofail_simps(1))
  next
    case 2
    then show ?case by (auto simp: WHILEI_mono_ge)
  next
    case 3
    then show ?case by simp
  next
    case (4 x)
    have  ‹(RES X ⤜ f ≤ M) = (∀x∈X. f x ≤ M)› for x f M X
      using intro_spec_refine_iff[of _ _ ‹Id›] by auto
    thm bind_refine_RES(2)[of _ Id, simplified]
    have [simp]: ‹flatf_mono FAIL ?f'›
      by (simp add: WHILEI_mono_ge)
    have H: ‹A = FAIL ⟷ ¬nofail A› for A by (auto simp: nofail_def)
    have ‹flatf_gfp ?f' x' = ?f' (?f' (flatf_gfp ?f')) x'›
      apply (subst flatf_ord.fixp_unfold)
       apply (solves ‹simp›)
      apply (subst flatf_ord.fixp_unfold)
       apply (solves ‹simp›)
      ..
    also have ‹… = ?f (?f' (flatf_gfp ?f')) x'›
      apply (subst (1) WHILEI_body_def, subst (1) WHILEI_body_def)
      apply (subst (2) WHILEI_body_def, subst (2) WHILEI_body_def)
      apply simp_all
      apply (cases ‹f x'›)
       apply (auto simp: RES_RETURN_RES nofail_def[symmetric] pw_RES_bind_choose
          eq_commute[of ‹FAIL›] H
          split: if_splits
          cong: if_cong)
      done
    also have ‹… = ?f (flatf_gfp ?f') x'›
      apply (subst (2) flatf_ord.fixp_unfold)
       apply (solves ‹simp›)
      ..
    finally have unfold1: ‹flatf_gfp ?f' x' =
         ?f (flatf_gfp ?f') x'›
      .
    have [intro!]: ‹(⋀x. g x ≤(h:: 'a ⇒ 'a nres) x) ⟹ fx ⤜ g ≤ fx ⤜ h› for g h fx fy
      by (refine_rcg bind_refine'[where R = ‹Id›, simplified]) fast
    show ?case
      apply (subst unfold1)
      using 4
      unfolding WHILEI_body_def
      by (auto intro: bind_refine'[where R = ‹Id›, simplified])
  qed
  show ?thesis
    unfolding RECT_def
    using le[of x'] ge[of x'] by (auto simp: WHILEI_body_trimono)
qed

lemma WHILEIT_add_post_condition:
 ‹(WHILEIT I' b' f' x') =
  (WHILEIT (λx'. I' x' ∧ (b' x' ⟶ f' x' = FAIL ∨ f' x' ≤ SPEC I'))
    b' f' x')›
  unfolding WHILEIT_def
  apply (subst RECT_WHILEI_body_add_post_condition)
  ..

lemma WHILEIT_rule_stronger_inv:
  assumes
    ‹wf R› and
    ‹I s› and
    ‹I' s› and
    ‹⋀s. I s ⟹ I' s ⟹ b s ⟹ f s ≤ SPEC (λs'. I s' ∧  I' s' ∧ (s', s) ∈ R)› and
    ‹⋀s. I s ⟹ I' s ⟹ ¬ b s ⟹ Φ s›
 shows ‹WHILETI b f s ≤ SPEC Φ›
proof -
  have ‹WHILETI b f s ≤ WHILETλs. I s ∧ I' s b f s›
    by (metis (mono_tags, lifting) WHILEIT_weaken)
  also have ‹WHILETλs. I s ∧ I' s b f s ≤ SPEC Φ›
    by (rule WHILEIT_rule) (use assms in ‹auto simp: ›)
  finally show ?thesis .
qed

lemma RES_RETURN_RES2:
   ‹SPEC Φ ⤜ (λ(T, T'). RETURN (f T T')) = RES (uncurry f ` {T. Φ T})›
  using RES_RETURN_RES[of ‹Collect Φ› ‹uncurry f›]
  apply (subst (asm)(2) split_prod_bound)
  by auto

lemma WHILEIT_rule_stronger_inv_RES:
  assumes
    ‹wf R› and
    ‹I s› and
    ‹I' s›
    ‹⋀s. I s ⟹ I' s ⟹ b s ⟹ f s ≤ SPEC (λs'. I s' ∧  I' s' ∧ (s', s) ∈ R)› and
   ‹⋀s. I s ⟹ I' s ⟹ ¬ b s ⟹ s ∈ Φ›
 shows ‹WHILETI b f s ≤ RES Φ›
proof -
  have RES_SPEC: ‹RES Φ = SPEC(λs. s ∈ Φ)›
    by auto
  have ‹WHILETI b f s ≤ WHILETλs. I s ∧ I' s b f s›
    by (metis (mono_tags, lifting) WHILEIT_weaken)
  also have ‹WHILETλs. I s ∧ I' s b f s ≤ RES Φ›
    unfolding RES_SPEC
    by (rule WHILEIT_rule) (use assms in ‹auto simp: ›)
  finally show ?thesis .
qed


lemma fref_weaken_pre_weaken:
  assumes "⋀x. P x ⟶ P' x"
  assumes "(f,h) ∈ fref P' R S"
  assumes ‹S ⊆ S'›
  shows "(f,h) ∈ fref P R S'"
  using assms unfolding fref_def by blast

lemma bind_rule_complete_RES: ‹(M ⤜ f ≤ RES Φ) = (M ≤ SPEC (λx. f x ≤ RES Φ))›
  by (auto simp: pw_le_iff refine_pw_simps)

lemma fref_to_Down:
  ‹(f, g) ∈ [P]f A → ⟨B⟩nres_rel ⟹
     (⋀x x'. P x' ⟹ (x, x') ∈ A ⟹ f x ≤ ⇓ B (g x'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_curry_left:
  fixes f:: ‹'a ⇒ 'b ⇒ 'c nres› and
    A::‹(('a × 'b) × 'd) set›
  shows
    ‹(uncurry f, g) ∈ [P]f A → ⟨B⟩nres_rel ⟹
      (⋀a b x'. P x' ⟹ ((a, b), x') ∈ A ⟹ f a b ≤ ⇓ B (g x'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_curry:
  ‹(uncurry f, uncurry g) ∈ [P]f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ f x y ≤ ⇓ B (g x' y'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_curry2:
  ‹(uncurry2 f, uncurry2 g) ∈ [P]f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y' z z'. P ((x', y'), z') ⟹ (((x, y), z), ((x', y'), z')) ∈ A⟹
         f x y z ≤ ⇓ B (g x' y' z'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_curry2':
  ‹(uncurry2 f, uncurry2 g) ∈ A →f ⟨B⟩nres_rel ⟹
     (⋀x x' y y' z z'. (((x, y), z), ((x', y'), z')) ∈ A ⟹
         f x y z ≤ ⇓ B (g x' y' z'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_curry3:
  ‹(uncurry3 f, uncurry3 g) ∈ [P]f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y' z z' a a'. P (((x', y'), z'), a') ⟹
        ((((x, y), z), a), (((x', y'), z'), a')) ∈ A ⟹
         f x y z a ≤ ⇓ B (g x' y' z' a'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_curry4:
  ‹(uncurry4 f, uncurry4 g) ∈ [P]f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y' z z' a a' b b'. P ((((x', y'), z'), a'), b') ⟹
        (((((x, y), z), a), b), ((((x', y'), z'), a'), b')) ∈ A ⟹
         f x y z a b ≤ ⇓ B (g x' y' z' a' b'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_curry5:
  ‹(uncurry5 f, uncurry5 g) ∈ [P]f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y' z z' a a' b b' c c'. P (((((x', y'), z'), a'), b'), c') ⟹
        ((((((x, y), z), a), b), c), (((((x', y'), z'), a'), b'), c')) ∈ A ⟹
         f x y z a b c ≤ ⇓ B (g x' y' z' a' b' c'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_curry6:
  ‹(uncurry6 f, uncurry6 g) ∈ [P]f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y' z z' a a' b b' c c' d d'. P ((((((x', y'), z'), a'), b'), c'), d') ⟹
        (((((((x, y), z), a), b), c), d), ((((((x', y'), z'), a'), b'), c'), d')) ∈ A ⟹
         f x y z a b c d ≤ ⇓ B (g x' y' z' a' b' c' d'))›
  unfolding fref_def uncurry_def nres_rel_def by auto

lemma fref_to_Down_curry7:
  ‹(uncurry7 f, uncurry7 g) ∈ [P]f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y' z z' a a' b b' c c' d d' e e'. P (((((((x', y'), z'), a'), b'), c'), d'), e') ⟹
        ((((((((x, y), z), a), b), c), d), e), (((((((x', y'), z'), a'), b'), c'), d'), e')) ∈ A ⟹
         f x y z a b c d e ≤ ⇓ B (g x' y' z' a' b' c' d' e'))›
  unfolding fref_def uncurry_def nres_rel_def by auto

lemma fref_to_Down_explode:
  ‹(f a, g a) ∈ [P]f A → ⟨B⟩nres_rel ⟹
     (⋀x x' b. P x' ⟹ (x, x') ∈ A ⟹ b = a ⟹ f a x ≤ ⇓ B (g b x'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_curry_no_nres_Id:
  ‹(uncurry (RETURN oo f), uncurry (RETURN oo g)) ∈ [P]f A → ⟨Id⟩nres_rel ⟹
     (⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ f x y = g x' y')›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_no_nres:
  ‹((RETURN o f), (RETURN o g)) ∈ [P]f A → ⟨B⟩nres_rel ⟹
     (⋀x x'. P (x') ⟹ (x, x') ∈ A ⟹ (f x, g x') ∈ B)›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_curry_no_nres:
  ‹(uncurry (RETURN oo f), uncurry (RETURN oo g)) ∈ [P]f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ (f x y, g x' y') ∈ B)›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma RES_RETURN_RES4:
   ‹SPEC Φ ⤜ (λ(T, T', T'', T'''). RETURN (f T T' T'' T''')) =
      RES ((λ(a, b, c, d). f a b c d) ` {T. Φ T})›
  using RES_RETURN_RES[of ‹Collect Φ› ‹λ(a, b, c, d). f a b c d›]
  apply (subst (asm)(2) split_prod_bound)
  apply (subst (asm)(3) split_prod_bound)
  apply (subst (asm)(4) split_prod_bound)
  by auto

declare RETURN_as_SPEC_refine[refine2 del]


lemma fref_to_Down_unRET_uncurry_Id:
  ‹(uncurry (RETURN oo f), uncurry (RETURN oo g)) ∈ [P]f A → ⟨Id⟩nres_rel ⟹
     (⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ f x y = (g x' y'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto
lemma fref_to_Down_unRET_uncurry:
  ‹(uncurry (RETURN oo f), uncurry (RETURN oo g)) ∈ [P]f A → ⟨B⟩nres_rel ⟹
     (⋀x x' y y'. P (x', y') ⟹ ((x, y), (x', y')) ∈ A ⟹ (f x y, g x' y') ∈ B)›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_unRET_Id:
  ‹((RETURN o f), (RETURN o g)) ∈ [P]f A → ⟨Id⟩nres_rel ⟹
     (⋀x x'. P x' ⟹ (x, x') ∈ A ⟹ f x = (g x'))›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_unRET:
  ‹((RETURN o f), (RETURN o g)) ∈ [P]f A → ⟨B⟩nres_rel ⟹
     (⋀x x'. P x' ⟹ (x, x') ∈ A ⟹ (f x, g x') ∈ B)›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_unRET_uncurry2:
  fixes f :: ‹'a ⇒ 'b ⇒ 'c ⇒ 'f›
    and g :: ‹'a2 ⇒ 'b2 ⇒ 'c2 ⇒ 'g›
  shows
    ‹(uncurry2 (RETURN ooo f), uncurry2 (RETURN ooo g)) ∈ [P]f A → ⟨B⟩nres_rel ⟹
       (⋀(x :: 'a) x' y y' (z :: 'c) (z' :: 'c2).
         P ((x', y'), z') ⟹ (((x, y), z), ((x', y'), z')) ∈ A ⟹
         (f x y z, g x' y' z') ∈ B)›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_unRET_uncurry3:
  shows
    ‹(uncurry3 (RETURN oooo f), uncurry3 (RETURN oooo g)) ∈ [P]f A → ⟨B⟩nres_rel ⟹
       (⋀(x :: 'a) x' y y' (z :: 'c) (z' :: 'c2) a a'.
         P (((x', y'), z'), a') ⟹ ((((x, y), z), a), (((x', y'), z'), a')) ∈ A ⟹
         (f x y z a, g x' y' z' a') ∈ B)›
  unfolding fref_def uncurry_def nres_rel_def
  by auto

lemma fref_to_Down_unRET_uncurry4:
  shows
    ‹(uncurry4 (RETURN ooooo f), uncurry4 (RETURN ooooo g)) ∈ [P]f A → ⟨B⟩nres_rel ⟹
       (⋀(x :: 'a) x' y y' (z :: 'c) (z' :: 'c2) a a' b b'.
         P ((((x', y'), z'), a'), b') ⟹ (((((x, y), z), a), b), ((((x', y'), z'), a'), b')) ∈ A ⟹
         (f x y z a b, g x' y' z' a' b') ∈ B)›
  unfolding fref_def uncurry_def nres_rel_def
  by auto


subsubsection ‹More Simplification Theorems›

lemma nofail_Down_nofail: ‹nofail gS ⟹ fS ≤ ⇓ R gS ⟹ nofail fS›
  using pw_ref_iff by blast

text ‹This is the refinement version of @{thm WHILEIT_add_post_condition}.›
lemma WHILEIT_refine_with_post:
  assumes R0: "I' x' ⟹ (x,x')∈R"
  assumes IREF: "⋀x x'. ⟦ (x,x')∈R; I' x' ⟧ ⟹ I x"
  assumes COND_REF: "⋀x x'. ⟦ (x,x')∈R; I x; I' x' ⟧ ⟹ b x = b' x'"
  assumes STEP_REF:
    "⋀x x'. ⟦ (x,x')∈R; b x; b' x'; I x; I' x'; f' x' ≤ SPEC I' ⟧ ⟹ f x ≤ ⇓R (f' x')"
  shows "WHILEIT I b f x ≤⇓R (WHILEIT I' b' f' x')"
  apply (subst (2) WHILEIT_add_post_condition)
  apply (rule WHILEIT_refine)
  subgoal using R0 by blast
  subgoal using IREF by blast
  subgoal using COND_REF by blast
  subgoal using STEP_REF by auto
  done


subsection ‹Some Refinement›

lemma Collect_eq_comp: ‹{(c, a). a = f c} O {(x, y). P x y} = {(c, y). P (f c) y}›
  by auto

lemma Collect_eq_comp_right:
  ‹{(x, y). P x y} O {(c, a). a = f c} = {(x, c). ∃y. P x y ∧ c = f y} ›
  by auto


lemma no_fail_spec_le_RETURN_itself: ‹nofail f ⟹ f ≤ SPEC(λx. RETURN x ≤ f)›
  by (metis RES_rule nres_order_simps(21) the_RES_inv)

lemma refine_add_invariants':
  assumes
    ‹f S ≤ ⇓ {(S, S'). Q' S S' ∧ Q S} gS› and
    ‹y ≤ ⇓ {((i, S), S'). P i S S'} (f S)› and
    ‹nofail gS›
  shows ‹y ≤ ⇓ {((i, S), S'). P i S S' ∧ Q S'} (f S)›
  using assms unfolding pw_le_iff pw_conc_inres pw_conc_nofail
  by force

lemma "weaken_⇓": ‹R' ⊆ R ⟹ f ≤ ⇓ R' g ⟹ f ≤ ⇓ R g›
  by (meson pw_ref_iff subset_eq)

method match_Down =
  (match conclusion in ‹f ≤ ⇓ R g› for f g R 
    ‹match premises in I: ‹f ≤ ⇓ R' g› for R'
       ⇒ ‹rule "weaken_⇓"[OF _ I]››)


lemma refine_SPEC_refine_Down:
  ‹f ≤ SPEC C ⟷ f ≤ ⇓ {(T', T). T = T' ∧ C T'} (SPEC C)›
  apply (rule iffI)
  subgoal
    by (rule SPEC_refine)  auto
  subgoal
    by (metis (no_types, lifting) RETURN_ref_SPECD SPEC_cons_rule dual_order.trans
        in_pair_collect_simp no_fail_spec_le_RETURN_itself nofail_Down_nofail nofail_simps(2))
  done



subsection ‹More declarations›

(* TODO: only input notation? *)
notation prod_rel_syn (infixl f" 70)


lemma diff_add_mset_remove1: ‹NO_MATCH {#} N ⟹ M - add_mset a N = remove1_mset a (M - N)›
  by auto


subsection ‹List relation›

lemma list_rel_take:
  ‹(ba, ab) ∈ ⟨A⟩list_rel ⟹ (take b ba, take b ab) ∈ ⟨A⟩list_rel›
  by (auto simp: list_rel_def)

lemma list_rel_update':
  fixes R
  assumes rel: ‹(xs, ys) ∈ ⟨R⟩list_rel› and
   h: ‹(bi, b) ∈ R›
  shows ‹(list_update xs ba bi, list_update ys ba b) ∈ ⟨R⟩list_rel›
proof -
  have [simp]: ‹(bi, b) ∈ R›
    using h by auto
  have ‹length xs = length ys›
    using assms list_rel_imp_same_length by blast

  then show ?thesis
    using rel
    by (induction xs ys arbitrary: ba rule: list_induct2) (auto split: nat.splits)
qed


lemma list_rel_in_find_correspondanceE:
  assumes ‹(M, M') ∈ ⟨R⟩list_rel› and ‹L ∈ set M›
  obtains L' where ‹(L, L') ∈ R› and ‹L' ∈ set M'›
  using assms[unfolded in_set_conv_decomp] by (auto simp: list_rel_append1
      elim!: list_relE3)



subsection ‹More Functions, Relations, and Theorems›

definition emptied_list :: ‹'a list ⇒ 'a list› where
  ‹emptied_list l = []›


lemma Down_id_eq: "⇓ Id a = a"
  by auto

lemma Down_itself_via_SPEC:
  assumes ‹I ≤ SPEC P› and ‹⋀x. P x ⟹ (x, x) ∈ R›
  shows ‹I ≤ ⇓ R I›
  using assms by (meson inres_SPEC pw_ref_I)
lemma RES_ASSERT_moveout:
  "(⋀a. a ∈ P ⟹ Q a) ⟹ do {a ← RES P; ASSERT(Q a); (f a)} =
   do {a← RES P; (f a)}"
  apply (subst order_class.eq_iff)
  apply (rule conjI)
  subgoal
    by (refine_rcg bind_refine_RES[where R=Id, unfolded Down_id_eq])
      auto
  subgoal
    by (refine_rcg bind_refine_RES[where R=Id, unfolded Down_id_eq])
      auto
  done

lemma bind_if_inverse:
  ‹do {
    S ← H;
    if b then f S else g S
    } =
    (if b then do {S ← H; f S} else do {S ← H; g S})
  › for H :: ‹'a nres›
  by auto


subsubsection ‹Ghost parameters›
text ‹
  This is a trick to recover from consumption of a variable (\<^term>‹𝒜in›) that is passed as
  argument and destroyed by the initialisation: We copy it as a zero-cost
  (by creating a \<^term>‹()›), because we don't need it in the code and only in the specification.

  This is a way to have ghost parameters, without having them: The parameter is replaced by \<^term>‹()›
  and we hope that the compiler will do the right thing.
›
definition virtual_copy where
  [simp]: ‹virtual_copy = id›

definition virtual_copy_rel where
  ‹virtual_copy_rel = {(c, b). c = ()}›


lemma bind_cong_nres: ‹(⋀x. g x = g' x) ⟹ (do {a ← f :: 'a nres;  g a}) = (do {a ← f :: 'a nres;  g' a})›
  by auto

lemma case_prod_cong:
  ‹(⋀a b. f a b = g a b) ⟹ (case x of (a, b) ⇒ f a b) = (case x of (a, b) ⇒ g a b)›
  by (cases x) auto

lemma if_replace_cond: ‹(if b then P b else Q b) = (if b then P True else Q False)›
  by auto


lemma foldli_cong2:
  assumes
    le: ‹length l = length l'› and
    σ: ‹σ = σ'› and
    c: ‹c = c'› and
    H: ‹⋀σ x. x < length l ⟹ c' σ ⟹ f (l ! x) σ = f' (l' ! x) σ›
  shows ‹foldli l c f σ = foldli l' c' f' σ'›
proof -
  show ?thesis
    using le H unfolding c[symmetric] σ[symmetric]
  proof (induction l arbitrary: l' σ)
    case Nil
    then show ?case by simp
  next
    case (Cons a l l'') note IH=this(1) and le = this(2) and H = this(3)
    show ?case
      using le H[of ‹Suc _›] H[of 0] IH[of ‹tl l''› ‹f' (hd l'') σ›]
      by (cases l'') auto
  qed
qed

lemma foldli_foldli_list_nth:
  ‹foldli xs c P a = foldli [0..<length xs] c (λi. P (xs ! i)) a›
proof (induction xs arbitrary: a)
  case Nil
  then show ?case by auto
next
  case (Cons x xs) note IH = this(1)
  have 1: ‹[0..<length (x # xs)] = 0 # [1..<length (x#xs)]›
    by (subst upt_rec)  simp
  have 2: ‹[1..<length (x#xs)] = map Suc [0..<length xs]›
    by (induction xs) auto
  have AB: ‹foldli [0..<length (x # xs)] c (λi. P ((x # xs) ! i)) a =
      foldli (0 # [1..<length (x#xs)]) c (λi. P ((x # xs) ! i)) a›
      (is ‹?A = ?B›)
    unfolding 1 ..
  {
    assume [simp]: ‹c a›
    have ‹foldli (0 # [1..<length (x#xs)]) c (λi. P ((x # xs) ! i)) a =
       foldli [1..<length (x#xs)] c (λi. P ((x # xs) ! i)) (P x a)›
      by simp
    also have ‹…  = foldli [0..<length xs] c (λi. P (xs ! i)) (P x a)›
      unfolding 2
      by (rule foldli_cong2) auto
    finally have ‹?A = foldli [0..<length xs] c (λi. P (xs ! i)) (P x a)›
      using AB
      by simp
  }
  moreover {
    assume [simp]: ‹¬c a›
    have ‹?B = a›
      by simp
  }
  ultimately show ?case by (auto simp: IH)
qed

lemma RES_RES13_RETURN_RES: ‹do {
  (M, N, D, Q, W, vm, φ, clvls, cach, lbd, outl, stats, fast_ema, slow_ema, ccount,
       vdom, avdom, lcount) ← RES A;
  RES (f M N D Q W vm φ clvls cach lbd outl stats fast_ema slow_ema ccount
      vdom avdom lcount)
} = RES (⋃(M, N, D, Q, W, vm, φ, clvls, cach, lbd, outl, stats, fast_ema, slow_ema, ccount,
       vdom, avdom, lcount)∈A. f M N D Q W vm φ clvls cach lbd outl stats fast_ema slow_ema ccount
      vdom avdom lcount)›
  by (force simp:  pw_eq_iff refine_pw_simps uncurry_def)


lemma RES_SPEC_conv: ‹RES P = SPEC (λv. v ∈ P)›
  by auto

lemma add_invar_refineI_P: ‹A ≤ ⇓ {(x,y). R x y} B ⟹ (nofail A ⟹A ≤ SPEC P) ⟹ A ≤ ⇓ {(x,y). R x y ∧ P x} B›
  using add_invar_refineI[of ‹λ_. A› _  _ ‹λ_. B› P, where R=‹{(x,y). R x y}› and I=P]
  by auto


lemma (in -)WHILEIT_rule_stronger_inv_RES':
  assumes
    ‹wf R› and
    ‹I s› and
    ‹I' s›
    ‹⋀s. I s ⟹ I' s ⟹ b s ⟹ f s ≤ SPEC (λs'. I s' ∧  I' s' ∧ (s', s) ∈ R)› and
   ‹⋀s. I s ⟹ I' s ⟹ ¬ b s ⟹ RETURN s ≤ ⇓ H (RES Φ)›
 shows ‹WHILETI b f s ≤ ⇓ H (RES Φ)›
proof -
  have RES_SPEC: ‹RES Φ = SPEC(λs. s ∈ Φ)›
    by auto
  have ‹WHILETI b f s ≤ WHILETλs. I s ∧ I' s b f s›
    by (metis (mono_tags, lifting) WHILEIT_weaken)
  also have ‹WHILETλs. I s ∧ I' s b f s ≤ ⇓ H (RES Φ)›
    unfolding RES_SPEC conc_fun_SPEC
    apply (rule WHILEIT_rule[OF assms(1)])
    subgoal using assms(2,3) by auto
    subgoal using assms(4) by auto
    subgoal using assms(5) unfolding RES_SPEC conc_fun_SPEC by auto
    done
  finally show ?thesis .
qed

lemma same_in_Id_option_rel:
  ‹x = x' ⟹ (x, x') ∈ ⟨Id⟩option_rel›
  by auto

definition find_in_list_between :: ‹('a ⇒ bool) ⇒ nat ⇒ nat ⇒ 'a list ⇒ nat option nres› where
  ‹find_in_list_between P a b C = do {
      (x, _) ← WHILETλ(found, i). i ≥ a ∧ i ≤ length C ∧ i ≤ b ∧ (∀j∈{a..<i}. ¬P (C!j)) ∧
        (∀j. found = Some j ⟶ (i = j ∧ P (C ! j) ∧ j < b ∧ j ≥ a))
        (λ(found, i). found = None ∧ i < b)
        (λ(_, i). do {
          ASSERT(i < length C);
          if P (C!i) then RETURN (Some i, i) else RETURN (None, i+1)
        })
        (None, a);
      RETURN x
  }›

lemma find_in_list_between_spec:
  assumes ‹a ≤ length C› and ‹b ≤ length C› and ‹a ≤ b›
  shows
    ‹find_in_list_between P a b C ≤ SPEC(λi.
       (i ≠ None ⟶  P (C ! the i) ∧ the i ≥ a ∧ the i < b) ∧
       (i = None ⟶ (∀j. j ≥ a ⟶ j < b ⟶ ¬P (C!j))))›
  unfolding find_in_list_between_def
  apply (refine_vcg WHILEIT_rule[where R = ‹measure (λ(f, i). Suc (length C) - (i + (if f = None then 0 else 1)))›])
  subgoal by auto
  subgoal by auto
  subgoal using assms by auto
  subgoal using assms by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal using assms by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by (auto simp: less_Suc_eq)
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  subgoal by auto
  done


lemma nfoldli_cong2:
  assumes
    le: ‹length l = length l'› and
    σ: ‹σ = σ'› and
    c: ‹c = c'› and
    H: ‹⋀σ x. x < length l ⟹ c' σ ⟹ f (l ! x) σ = f' (l' ! x) σ›
  shows ‹nfoldli l c f σ = nfoldli l' c' f' σ'›
proof -
  show ?thesis
    using le H unfolding c[symmetric] σ[symmetric]
  proof (induction l arbitrary: l' σ)
    case Nil
    then show ?case by simp
  next
    case (Cons a l l'') note IH=this(1) and le = this(2) and H = this(3)
    show ?case
      using le H[of ‹Suc _›] H[of 0] IH[of ‹tl l''› ‹_›]
      by (cases l'')
        (auto intro: bind_cong_nres)
  qed
qed

lemma nfoldli_nfoldli_list_nth:
  ‹nfoldli xs c P a = nfoldli [0..<length xs] c (λi. P (xs ! i)) a›
proof (induction xs arbitrary: a)
  case Nil
  then show ?case by auto
next
  case (Cons x xs) note IH = this(1)
  have 1: ‹[0..<length (x # xs)] = 0 # [1..<length (x#xs)]›
    by (subst upt_rec)  simp
  have 2: ‹[1..<length (x#xs)] = map Suc [0..<length xs]›
    by (induction xs) auto
  have AB: ‹nfoldli [0..<length (x # xs)] c (λi. P ((x # xs) ! i)) a =
      nfoldli (0 # [1..<length (x#xs)]) c (λi. P ((x # xs) ! i)) a›
      (is ‹?A = ?B›)
    unfolding 1 ..
  {
    assume [simp]: ‹c a›
    have ‹nfoldli (0 # [1..<length (x#xs)]) c (λi. P ((x # xs) ! i)) a =
       do {
         σ ← (P x a);
         nfoldli [1..<length (x#xs)] c (λi. P ((x # xs) ! i)) σ
        }›
      by simp
    moreover have ‹nfoldli [1..<length (x#xs)] c (λi. P ((x # xs) ! i)) σ  =
       nfoldli [0..<length xs] c (λi. P (xs ! i)) σ› for σ
      unfolding 2
      by (rule nfoldli_cong2) auto
    ultimately have ‹?A = do {
         σ ← (P x a);
         nfoldli [0..<length xs] c (λi. P (xs ! i))  σ
        }›
      using AB
      by (auto intro: bind_cong_nres)
  }
  moreover {
    assume [simp]: ‹¬c a›
    have ‹?B = RETURN a›
      by simp
  }
  ultimately show ?case by (auto simp: IH intro: bind_cong_nres)
qed

(*TODO kill once shared*)
definition "list_mset_rel ≡ br mset (λ_. True)"

lemma
  Nil_list_mset_rel_iff:
    ‹([], aaa) ∈ list_mset_rel ⟷ aaa = {#}› and
  empty_list_mset_rel_iff:
    ‹(a, {#}) ∈ list_mset_rel ⟷ a = []›
  by (auto simp: list_mset_rel_def br_def)

definition list_rel_mset_rel where list_rel_mset_rel_internal:
‹list_rel_mset_rel ≡ λR. ⟨R⟩list_rel O list_mset_rel›

lemma list_rel_mset_rel_def[refine_rel_defs]:
  ‹⟨R⟩list_rel_mset_rel = ⟨R⟩list_rel O list_mset_rel›
  unfolding relAPP_def list_rel_mset_rel_internal ..

lemma list_rel_mset_rel_imp_same_length: ‹(a, b) ∈ ⟨R⟩list_rel_mset_rel ⟹ length a = size b›
  by (auto simp: list_rel_mset_rel_def list_mset_rel_def br_def
      dest: list_rel_imp_same_length)

lemma while_upt_while_direct1:
  "b ≥ a ⟹
  do {
    (_,σ) ← WHILET (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) ([a..<b],σ);
    RETURN σ
  } ≤ do {
    (_,σ) ← WHILET (λ(i, x). i < b ∧ c x) (λ(i, x). do {ASSERT (i < b);  σ'←f i x; RETURN (i+1,σ')
}) (a,σ);
    RETURN σ
  }"
  apply (rewrite at ‹_ ≤ ⌑› Down_id_eq[symmetric])
  apply (refine_vcg WHILET_refine[where R = ‹{((l, x'), (i::nat, x::'a)). x= x' ∧ i ≤ b ∧ i ≥ a ∧ l = drop (i-a) [a..<b]}›])
  subgoal by auto
  subgoal by (auto simp: FOREACH_cond_def)
  subgoal by (auto simp: FOREACH_body_def intro!: bind_refine[OF Id_refine])
  subgoal by auto
  done

lemma while_upt_while_direct2:
  "b ≥ a ⟹
  do {
    (_,σ) ← WHILET (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) ([a..<b],σ);
    RETURN σ
  } ≥ do {
    (_,σ) ← WHILET (λ(i, x). i < b ∧ c x) (λ(i, x). do {ASSERT (i < b);  σ'←f i x; RETURN (i+1,σ')
}) (a,σ);
    RETURN σ
  }"
  apply (rewrite at ‹_ ≤ ⌑› Down_id_eq[symmetric])
  apply (refine_vcg WHILET_refine[where R = ‹{((i::nat, x::'a), (l, x')). x= x' ∧ i ≤ b ∧ i ≥ a ∧ l = drop (i-a) [a..<b]}›])
  subgoal by auto
  subgoal by (auto simp: FOREACH_cond_def)
  subgoal by (auto simp: FOREACH_body_def intro!: bind_refine[OF Id_refine])
  subgoal by (auto simp: FOREACH_body_def intro!: bind_refine[OF Id_refine])
  subgoal by auto
  done

lemma while_upt_while_direct:
  "b ≥ a ⟹
  do {
    (_,σ) ← WHILET (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) ([a..<b],σ);
    RETURN σ
  } = do {
    (_,σ) ← WHILET (λ(i, x). i < b ∧ c x) (λ(i, x). do {ASSERT (i < b);  σ'←f i x; RETURN (i+1,σ')
}) (a,σ);
    RETURN σ
  }"
  using while_upt_while_direct1[of a b] while_upt_while_direct2[of a b] unfolding order_class.eq_iff by fast


lemma while_nfoldli:
  "do {
    (_,σ) ← WHILET (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l,σ);
    RETURN σ
  } ≤ nfoldli l c f σ"
  apply (induct l arbitrary: σ)
  apply (subst WHILET_unfold)
  apply (simp add: FOREACH_cond_def)

  apply (subst WHILET_unfold)
  apply (auto
    simp: FOREACH_cond_def FOREACH_body_def
    intro: bind_mono Refine_Basic.bind_mono(1))
 done
lemma nfoldli_while: "nfoldli l c f σ
          ≤
         (WHILETI
           (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l, σ) ⤜
          (λ(_, σ). RETURN σ))"
proof (induct l arbitrary: σ)
  case Nil thus ?case by (subst WHILEIT_unfold) (auto simp: FOREACH_cond_def)
next
  case (Cons x ls)
  show ?case
  proof (cases "c σ")
    case False thus ?thesis
      apply (subst WHILEIT_unfold)
      unfolding FOREACH_cond_def
      by simp
  next
    case [simp]: True
    from Cons show ?thesis
      apply (subst WHILEIT_unfold)
      unfolding FOREACH_cond_def FOREACH_body_def
      apply clarsimp
      apply (rule Refine_Basic.bind_mono)
      apply simp_all
      done
  qed
qed

lemma while_eq_nfoldli: "do {
    (_,σ) ← WHILET (FOREACH_cond c) (λx. do {ASSERT (FOREACH_cond c x); FOREACH_body f x}) (l,σ);
    RETURN σ
  } = nfoldli l c f σ"
  apply (rule antisym)
  apply (rule while_nfoldli)
  apply (rule order_trans[OF nfoldli_while[where I="λ_. True"]])
  apply (simp add: WHILET_def)
  done

end