Theory Refine_While

section ‹While-Loops›
theory Refine_While
imports 
  Refine_Basic Refine_Leof "Generic/RefineG_While"
begin

definition WHILEIT ("WHILE⇩T⇗_⇖") where 
  "WHILEIT ≡ iWHILEIT bind RETURN"
definition WHILEI ("WHILE⇗_⇖") where "WHILEI ≡ iWHILEI bind RETURN"
definition WHILET ("WHILE⇩T") where "WHILET ≡ iWHILET bind RETURN"
definition WHILE where "WHILE ≡ iWHILE bind RETURN"

interpretation while?: generic_WHILE_rules bind RETURN SPEC
  WHILEIT WHILEI WHILET WHILE
  apply unfold_locales
  apply (simp_all add: WHILEIT_def WHILEI_def WHILET_def WHILE_def)
  apply refine_mono
  apply refine_mono

  apply (subst RES_Sup_RETURN[symmetric]) 
  apply (rule_tac f=Sup in arg_cong) apply auto []
  apply (erule bind_rule)
  done

lemmas [refine_vcg] = WHILEI_rule
lemmas [refine_vcg] = WHILEIT_rule

subsection ‹Data Refinement Rules›

lemma ref_WHILEI_invarI:
  assumes "I s ⟹ M ≤ ⇓R (WHILEI I b f s)"
  shows "M ≤ ⇓R (WHILEI I b f s)"
  apply (subst WHILEI_unfold)
  apply (cases "I s")
  apply (subst WHILEI_unfold[symmetric])
  apply (erule assms)
  apply simp
  done

lemma ref_WHILEIT_invarI:
  assumes "I s ⟹ M ≤ ⇓R (WHILEIT I b f s)"
  shows "M ≤ ⇓R (WHILEIT I b f s)"
  apply (subst WHILEIT_unfold)
  apply (cases "I s")
  apply (subst WHILEIT_unfold[symmetric])
  apply (erule assms)
  apply simp
  done


lemma WHILEI_le_rule:
  assumes R0: "(s,s')∈R"
  assumes RS: "⋀W s s'. ⟦⋀s s'. (s,s')∈R ⟹ W s ≤ M s'; (s,s')∈R⟧ ⟹ 
    do {ASSERT (I s); if b s then bind (f s) W else RETURN s} ≤ M s'"
  shows "WHILEI I b f s ≤ M s'"
  unfolding WHILEI_def
  apply (rule REC_le_rule[where M=M])
  apply (simp add: WHILEI_body_def, refine_mono)
  apply (rule R0)
  apply (erule (1) order_trans[rotated,OF RS])
  unfolding WHILEI_body_def
  apply auto
  done


text ‹WHILE-refinement rule with invisible concrete steps.
  Intuitively, a concrete step may either refine an abstract step, or
  must not change the corresponding abstract state.›
lemma WHILEI_invisible_refine_genR:
  assumes R0: "I' s' ⟹ (s,s')∈R'"
  assumes RI: "⋀s s'. ⟦ (s,s')∈R'; I' s' ⟧ ⟹ I s"
  assumes RB: "⋀s s'. ⟦ (s,s')∈R'; I' s'; I s; b' s' ⟧ ⟹ b s"
  assumes RS: "⋀s s'. ⟦ (s,s')∈R'; I' s'; I s; b s ⟧ 
    ⟹ f s ≤ sup (⇓R' (do {ASSUME (b' s'); f' s'})) (⇓R' (RETURN s'))"
  assumes R_REF: 
    "⋀x x'. ⟦ (x,x')∈R'; ¬b x; ¬b' x'; I x; I' x' ⟧ ⟹ (x,x')∈R"
  shows "WHILEI I b f s ≤ ⇓R (WHILEI I' b' f' s')"
  apply (rule ref_WHILEI_invarI)
  apply (rule WHILEI_le_rule[where R=R'])
  apply (erule R0)
  apply (rule ref_WHILEI_invarI)
  apply (frule (1) RI)
  apply (case_tac "b s=False")
  apply (subst WHILEI_unfold)
  apply (auto dest: RB intro: RETURN_refine R_REF) []

  apply simp
  apply (rule order_trans[OF monoD[OF bind_mono1 RS]], assumption+)
  apply (simp only: bind_distrib_sup1)
  apply (rule sup_least)
    apply (subst WHILEI_unfold)
    apply (simp add: RB, intro impI)
    apply (rule bind_refine)
    apply (rule order_refl)
    apply simp

    apply (simp add: pw_le_iff refine_pw_simps, blast)
  done


lemma WHILEI_refine_genR:
  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 ≤ ⇓R' (f' x')"
  assumes R_REF: 
    "⋀x x'. ⟦ (x,x')∈R'; ¬b x; ¬b' x'; I x; I' x' ⟧ ⟹ (x,x')∈R"
  shows "WHILEI I b f x ≤⇓R (WHILEI I' b' f' x')" 
  apply (rule WHILEI_invisible_refine_genR[OF R0])
  apply assumption
  apply (erule (1) IREF)
  apply (simp add: COND_REF)
  apply (rule le_supI1)
  apply (simp add: COND_REF STEP_REF)
  apply (rule R_REF, assumption+)
  done

lemma WHILE_invisible_refine_genR:
  assumes R0: "(s,s')∈R'"
  assumes RB: "⋀s s'. ⟦ (s,s')∈R'; b' s' ⟧ ⟹ b s"
  assumes RS: "⋀s s'. ⟦ (s,s')∈R'; b s ⟧ 
    ⟹ f s ≤ sup (⇓R' (do {ASSUME (b' s'); f' s'})) (⇓R' (RETURN s'))"
  assumes R_REF: 
    "⋀x x'. ⟦ (x,x')∈R'; ¬b x; ¬b' x' ⟧ ⟹ (x,x')∈R"
  shows "WHILE b f s ≤ ⇓R (WHILE b' f' s')"
  unfolding WHILE_def
  apply (rule WHILEI_invisible_refine_genR)
  apply (rule assms, (assumption+)?)+
  done

lemma WHILE_refine_genR:
  assumes R0: "(x,x')∈R'"
  assumes COND_REF: "⋀x x'. ⟦ (x,x')∈R' ⟧ ⟹ b x = b' x'"
  assumes STEP_REF: 
    "⋀x x'. ⟦ (x,x')∈R'; b x; b' x' ⟧ ⟹ f x ≤ ⇓R' (f' x')"
  assumes R_REF: 
    "⋀x x'. ⟦ (x,x')∈R'; ¬b x; ¬b' x' ⟧ ⟹ (x,x')∈R"
  shows "WHILE b f x ≤⇓R (WHILE b' f' x')"
  unfolding WHILE_def
  apply (rule WHILEI_refine_genR)
  apply (rule assms, (assumption+)?)+
  done

lemma WHILE_refine_genR':
  assumes R0: "(x,x')∈R'"
  assumes COND_REF: "⋀x x'. ⟦ (x,x')∈R'; I' x' ⟧ ⟹ b x = b' x'"
  assumes STEP_REF: 
    "⋀x x'. ⟦ (x,x')∈R'; b x; b' x'; I' x' ⟧ ⟹ f x ≤ ⇓R' (f' x')"
  assumes R_REF: 
    "⋀x x'. ⟦ (x,x')∈R'; ¬b x; ¬b' x' ⟧ ⟹ (x,x')∈R"
  shows "WHILE b f x ≤⇓R (WHILEI I' b' f' x')"
  unfolding WHILE_def
  apply (rule WHILEI_refine_genR)
  apply (rule assms TrueI, (assumption+)?)+
  done

text ‹WHILE-refinement rule with invisible concrete steps.
  Intuitively, a concrete step may either refine an abstract step, or
  must not change the corresponding abstract state.›
lemma WHILEI_invisible_refine:
  assumes R0: "I' s' ⟹ (s,s')∈R"
  assumes RI: "⋀s s'. ⟦ (s,s')∈R; I' s' ⟧ ⟹ I s"
  assumes RB: "⋀s s'. ⟦ (s,s')∈R; I' s'; I s; b' s' ⟧ ⟹ b s"
  assumes RS: "⋀s s'. ⟦ (s,s')∈R; I' s'; I s; b s ⟧ 
    ⟹ f s ≤ sup (⇓R (do {ASSUME (b' s'); f' s'})) (⇓R (RETURN s'))"
  shows "WHILEI I b f s ≤ ⇓R (WHILEI I' b' f' s')"
  apply (rule WHILEI_invisible_refine_genR[where R'=R])
  apply (rule assms, (assumption+)?)+
  done

lemma WHILEI_refine[refine]:
  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 ≤ ⇓R (f' x')"
  shows "WHILEI I b f x ≤⇓R (WHILEI I' b' f' x')" 
  apply (rule WHILEI_invisible_refine[OF R0])
  apply assumption
  apply (erule (1) IREF)
  apply (simp add: COND_REF)
  apply (rule le_supI1)
  apply (simp add: COND_REF STEP_REF)
  done

lemma WHILE_invisible_refine:
  assumes R0: "(s,s')∈R"
  assumes RB: "⋀s s'. ⟦ (s,s')∈R; b' s' ⟧ ⟹ b s"
  assumes RS: "⋀s s'. ⟦ (s,s')∈R; b s ⟧ 
    ⟹ f s ≤ sup (⇓R (do {ASSUME (b' s'); f' s'})) (⇓R (RETURN s'))"
  shows "WHILE b f s ≤ ⇓R (WHILE b' f' s')"
  unfolding WHILE_def
  apply (rule WHILEI_invisible_refine)
  using assms by auto

lemma WHILE_le_rule:
  assumes R0: "(s,s')∈R"
  assumes RS: "⋀W s s'. ⟦⋀s s'. (s,s')∈R ⟹ W s ≤ M s'; (s,s')∈R⟧ ⟹ 
    do {if b s then bind (f s) W else RETURN s} ≤ M s'"
  shows "WHILE b f s ≤ M s'"
  unfolding WHILE_def
  apply (rule WHILEI_le_rule[OF R0])
  apply (simp add: RS)
  done

lemma WHILE_refine[refine]:
  assumes R0: "(x,x')∈R"
  assumes COND_REF: "⋀x x'. ⟦ (x,x')∈R ⟧ ⟹ b x = b' x'"
  assumes STEP_REF: 
    "⋀x x'. ⟦ (x,x')∈R; b x; b' x' ⟧ ⟹ f x ≤ ⇓R (f' x')"
  shows "WHILE b f x ≤⇓R (WHILE b' f' x')"
  unfolding WHILE_def
  apply (rule WHILEI_refine)
  using assms by auto

lemma WHILE_refine'[refine]:
  assumes R0: "I' x' ⟹ (x,x')∈R"
  assumes COND_REF: "⋀x x'. ⟦ (x,x')∈R; I' x' ⟧ ⟹ b x = b' x'"
  assumes STEP_REF: 
    "⋀x x'. ⟦ (x,x')∈R; b x; b' x'; I' x' ⟧ ⟹ f x ≤ ⇓R (f' x')"
  shows "WHILE b f x ≤⇓R (WHILEI I' b' f' x')"
  unfolding WHILE_def
  apply (rule WHILEI_refine)
  using assms by auto

lemma AIF_leI: "⟦Φ; Φ ⟹ S≤S'⟧ ⟹ (if Φ then S else FAIL) ≤ S'"
  by auto
lemma ref_AIFI: "⟦Φ ⟹ S≤⇓R S'⟧ ⟹ S ≤ ⇓R (if Φ then S' else FAIL)"
  by (cases Φ) auto

text ‹Refinement with generalized refinement relation. Required to exploit
  the fact that the condition does not hold at the end of the loop.›
lemma WHILEIT_refine_genR:
  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 ≤ ⇓R' (f' x')"
  assumes R_REF: 
    "⋀x x'. ⟦ (x,x')∈R'; ¬b x; ¬b' x'; I x; I' x' ⟧ ⟹ (x,x')∈R"
  shows "WHILEIT I b f x ≤⇓R (WHILEIT I' b' f' x')" 
  apply (rule ref_WHILEIT_invarI)
  unfolding WHILEIT_def
  apply (rule RECT_refine[OF WHILEI_body_trimono R0])
  apply assumption
  unfolding WHILEI_body_def
  apply (rule ref_AIFI)
  apply (rule AIF_leI)
  apply (blast intro: IREF)
  apply (rule if_refine)
  apply (simp add: COND_REF)
  apply (rule bind_refine)
  apply (rule STEP_REF, assumption+) []
  apply assumption

  apply (rule RETURN_refine)
  apply (simp add: R_REF)
  done


lemma WHILET_refine_genR:
  assumes R0: "(x,x')∈R'"
  assumes COND_REF: "⋀x x'. (x,x')∈R' ⟹ b x = b' x'"
  assumes STEP_REF: 
    "⋀x x'. ⟦ (x,x')∈R'; b x; b' x' ⟧ ⟹ f x ≤ ⇓R' (f' x')"
  assumes R_REF: 
    "⋀x x'. ⟦ (x,x')∈R'; ¬b x; ¬b' x' ⟧ ⟹ (x,x')∈R"
  shows "WHILET b f x ≤⇓R (WHILET b' f' x')"
  unfolding WHILET_def
  apply (rule WHILEIT_refine_genR[OF R0])
  apply (rule TrueI)
  apply (rule assms, assumption+)+
  done

lemma WHILET_refine_genR':
  assumes R0: "I' x' ⟹ (x,x')∈R'"
  assumes COND_REF: "⋀x x'. ⟦ (x,x')∈R'; I' x' ⟧ ⟹ b x = b' x'"
  assumes STEP_REF: 
    "⋀x x'. ⟦ (x,x')∈R'; b x; b' x'; I' x' ⟧ ⟹ f x ≤ ⇓R' (f' x')"
  assumes R_REF: 
    "⋀x x'. ⟦ (x,x')∈R'; ¬b x; ¬b' x'; I' x' ⟧ ⟹ (x,x')∈R"
  shows "WHILET b f x ≤⇓R (WHILEIT I' b' f' x')"
  unfolding WHILET_def
  apply (rule WHILEIT_refine_genR[OF R0])
  apply assumption
  apply (rule TrueI)
  apply (rule assms, assumption+)+
  done

lemma WHILEIT_refine[refine]:
  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 ≤ ⇓R (f' x')"
  shows "WHILEIT I b f x ≤⇓R (WHILEIT I' b' f' x')" 
  using WHILEIT_refine_genR[where R=R and R'=R, OF assms] .

lemma WHILET_refine[refine]:
  assumes R0: "(x,x')∈R"
  assumes COND_REF: "⋀x x'. ⟦ (x,x')∈R ⟧ ⟹ b x = b' x'"
  assumes STEP_REF: 
    "⋀x x'. ⟦ (x,x')∈R; b x; b' x' ⟧ ⟹ f x ≤ ⇓R (f' x')"
  shows "WHILET b f x ≤⇓R (WHILET b' f' x')"
  unfolding WHILET_def
  apply (rule WHILEIT_refine)
  using assms by auto

lemma WHILET_refine'[refine]:
  assumes R0: "I' x' ⟹ (x,x')∈R"
  assumes COND_REF: "⋀x x'. ⟦ (x,x')∈R; I' x' ⟧ ⟹ b x = b' x'"
  assumes STEP_REF: 
    "⋀x x'. ⟦ (x,x')∈R; b x; b' x'; I' x' ⟧ ⟹ f x ≤ ⇓R (f' x')"
  shows "WHILET b f x ≤⇓R (WHILEIT I' b' f' x')"
  unfolding WHILET_def
  apply (rule WHILEIT_refine)
  using assms by auto


lemma WHILEI_refine_new_invar:
  assumes R0: "I' x' ⟹ (x,x')∈R"
  assumes INV0: "⟦ I' x'; (x,x')∈R ⟧ ⟹ 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 ≤ ⇓R (f' x')"
  assumes STEP_INV: 
    "⋀x x'. ⟦ (x,x')∈R; b x; b' x'; I x; I' x'; nofail (f x) ⟧ ⟹ f x ≤ SPEC I"
  shows "WHILEI I b f x ≤⇓R (WHILEI I' b' f' x')"
  apply (rule WHILEI_refine_genR[where 
    I=I and I'=I' and x'=x' and x=x and R=R and b=b and b'=b' and f'=f' and f=f
    and R'="{ (c,a). (c,a)∈R ∧ I c }"
    ])
  using assms
  by (auto intro: add_invar_refineI)

lemma WHILEIT_refine_new_invar:
  assumes R0: "I' x' ⟹ (x,x')∈R"
  assumes INV0: "⟦ I' x'; (x,x')∈R ⟧ ⟹ 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 ≤ ⇓R (f' x')"
  assumes STEP_INV: 
    "⋀x x'. ⟦ nofail (f x); (x,x')∈R; b x; b' x'; I x; I' x' ⟧ ⟹ f x ≤ SPEC I"
  shows "WHILEIT I b f x ≤⇓R (WHILEIT I' b' f' x')"
  apply (rule WHILEIT_refine_genR[where 
    I=I and I'=I' and x'=x' and x=x and R=R and b=b and b'=b' and f'=f' and f=f
    and R'="{ (c,a). (c,a)∈R ∧ I c }"
    ])
  using assms
  by (auto intro: add_invar_refineI)


subsection ‹Autoref Setup›

(*lemma id_WHILE[autoref_id_self]: "ID_LIST 
  (l (WHILET,3) (WHILEIT I,3) (WHILE,3) (WHILEI I,3))"
  by simp_all*)

context begin interpretation autoref_syn .

lemma [autoref_op_pat_def]:
  "WHILEIT I ≡ OP (WHILEIT I)"
  "WHILEI I ≡ OP (WHILEI I)"
  by auto

lemma autoref_WHILET[autoref_rules]:
  assumes "⋀x x'. ⟦ (x,x')∈R⟧ ⟹ (c x,c'$x') ∈ Id"
  assumes "⋀x x'. ⟦ REMOVE_INTERNAL c' x'; (x,x')∈R⟧ 
    ⟹ (f x,f'$x') ∈ ⟨R⟩nres_rel"
  assumes "(s,s')∈R"
  shows "(WHILET c f s,
    (OP WHILET:::(R→Id)→(R→⟨R⟩nres_rel)→R→⟨R⟩nres_rel)$c'$f'$s')
   ∈ ⟨R⟩nres_rel"
  using assms
  by (auto simp add: nres_rel_def fun_rel_def intro!: WHILET_refine)

lemma autoref_WHILEIT[autoref_rules]:
  assumes "⋀x x'. ⟦I x'; (x,x')∈R⟧ ⟹ (c x,c'$x') ∈ Id"
  assumes "⋀x x'. ⟦REMOVE_INTERNAL c' x'; I x'; (x,x')∈R⟧ ⟹(f x,f'$x') ∈ ⟨R⟩nres_rel"
  assumes "I s' ⟹ (s,s')∈R"
  shows "(WHILET c f s,
      (OP (WHILEIT I) ::: (R→Id) → (R→⟨R⟩nres_rel) → R → ⟨R⟩nres_rel)$c'$f'$s'
    )∈⟨R⟩nres_rel"
  using assms
  by (auto simp add: nres_rel_def fun_rel_def intro!: WHILET_refine')

lemma autoref_WHILEIT'[autoref_rules]:
  assumes "⋀x x'. ⟦ (x,x')∈R; I x'⟧ ⟹ (c x,c'$x') ∈ Id"
  assumes "⋀x x'. ⟦ REMOVE_INTERNAL c' x'; (x,x')∈R; I x'⟧ 
    ⟹ (f x,f'$x') ∈ ⟨R⟩nres_rel"
  shows "(WHILET c f,
      (OP (WHILEIT I) ::: (R→Id) → (R→⟨R⟩nres_rel) → R → ⟨R⟩nres_rel)$c'$f'
    )∈R → ⟨R⟩nres_rel"
    unfolding autoref_tag_defs
    by (parametricity 
      add: autoref_WHILEIT[unfolded autoref_tag_defs]
      assms[unfolded autoref_tag_defs])

lemma autoref_WHILE[autoref_rules]: (** TODO: obsolete ? **)
  assumes "⋀x x'. ⟦ (x,x')∈R⟧ ⟹ (c x,c'$x') ∈ Id"
  assumes "⋀x x'. ⟦ REMOVE_INTERNAL c' x'; (x,x')∈R⟧ 
    ⟹ (f x,f'$x') ∈ ⟨R⟩nres_rel"
  assumes "(s,s')∈R"
  shows "(WHILE c f s,
      (OP WHILE ::: (R→Id) → (R→⟨R⟩nres_rel) → R → ⟨R⟩nres_rel)$c'$f'$s'
    )∈⟨R⟩nres_rel"
  using assms
  by (auto simp add: nres_rel_def fun_rel_def intro!: WHILE_refine)

lemma autoref_WHILE'[autoref_rules]:
  assumes "⋀x x'. ⟦ (x,x')∈R⟧ ⟹ (c x,c'$x') ∈ Id"
  assumes "⋀x x'. ⟦ REMOVE_INTERNAL c' x'; (x,x')∈R⟧ 
    ⟹ (f x,f'$x') ∈ ⟨R⟩nres_rel"
  shows "(WHILE c f,
      (OP WHILE ::: (R→Id) → (R→⟨R⟩nres_rel) → R → ⟨R⟩nres_rel)$c'$f'
    )∈R → ⟨R⟩nres_rel"
  using assms
  by (auto simp add: nres_rel_def fun_rel_def intro!: WHILE_refine)


lemma autoref_WHILEI[autoref_rules]:
  assumes "⋀x x'. ⟦I x'; (x,x')∈R⟧ ⟹ (c x,c'$x') ∈ Id"
  assumes "⋀x x'. ⟦REMOVE_INTERNAL c' x'; I x'; (x,x')∈R⟧ ⟹(f x,f'$x') ∈ ⟨R⟩nres_rel"
  assumes "I s' ⟹ (s,s')∈R"
  shows "(WHILE c f s,
      (OP (WHILEI I) ::: (R→Id) → (R→⟨R⟩nres_rel) → R → ⟨R⟩nres_rel)$c'$f'$s'
    )∈⟨R⟩nres_rel"
  using assms
  by (auto simp add: nres_rel_def fun_rel_def intro!: WHILE_refine')

lemma autoref_WHILEI'[autoref_rules]:
  assumes "⋀x x'. ⟦ (x,x')∈R; I x'⟧ ⟹ (c x,c'$x') ∈ Id"
  assumes "⋀x x'. ⟦ REMOVE_INTERNAL c' x'; (x,x')∈R; I x'⟧ 
    ⟹ (f x,f'$x') ∈ ⟨R⟩nres_rel"
  shows "(WHILE c f,
      (OP (WHILEI I) ::: (R→Id) → (R→⟨R⟩nres_rel) → R → ⟨R⟩nres_rel)$c'$f'
    )∈R → ⟨R⟩nres_rel"
    unfolding autoref_tag_defs
    by (parametricity 
      add: autoref_WHILEI[unfolded autoref_tag_defs]
      assms[unfolded autoref_tag_defs])



end

subsection ‹Invariants›
subsubsection ‹Tail Recursion›
context begin
  private lemma tailrec_transform_aux1:
    assumes "RETURN s ≤ m"
    shows "REC (λD s. sup (a s ⤜ D) (b s)) s ≤ lfp (λx. sup m (x⤜a)) ⤜ b"
    (is "REC ?F s ≤ lfp ?f ⤜ b")
  proof (rule REC_rule[where pre = "λs. RETURN s ≤ lfp ?f"], refine_mono)
    show "RETURN s ≤ lfp (λx. sup m (x ⤜ a))"
      apply (subst lfp_unfold, tagged_solver)
      using assms apply (simp add: le_supI1)
      done
  next
    fix f x
    assume IH: "⋀x. RETURN x ≤ lfp ?f ⟹
                  f x ≤ lfp ?f ⤜ b"
    and PRE: "RETURN x ≤ lfp ?f"
  
    show " sup (a x ⤜ f) (b x) ≤ lfp ?f ⤜ b"
    proof (rule sup_least)  
      show "b x ≤ lfp ?f ⤜ b"
      using PRE
        by (simp add: pw_le_iff refine_pw_simps) blast
    next
      from PRE have "a x ≤ lfp ?f ⤜ a"
        by (simp add: pw_le_iff refine_pw_simps) blast
      also have "… ≤ lfp ?f"
        apply (subst (2) lfp_unfold, tagged_solver)
        apply (simp add: le_supI2)
        done
      finally show "a x ⤜ f ≤ lfp ?f ⤜ b"
        using IH
        by (simp add: pw_le_iff refine_pw_simps) blast
    qed
  qed  
  
  private corollary tailrec_transform1: 
    fixes m :: "'a nres"
    shows "m⤜REC (λD s. sup (a s ⤜ D) (b s)) ≤ lfp (λx. sup m (x⤜a)) ⤜ b"
    apply (cases "nofail m")
    apply (erule bind_le_nofailI)
    apply (erule tailrec_transform_aux1)
    apply (simp add: not_nofail_iff lfp_const)
    done
  
            
  private lemma tailrec_transform_aux2:
    fixes m :: "'a nres"
    shows "lfp (λx. sup m (x⤜a)) 
      ≤ m ⤜ REC (λD s. sup (a s ⤜ D) (RETURN s))"
    (is "lfp ?f ≤ m ⤜ REC ?F")
    apply (subst gen_kleene_lfp)
    apply (simp add: cont_def pw_eq_iff refine_pw_simps, blast)
    apply (rule SUP_least, simp)
  proof -
    fix i
    show "((λx. x ⤜ a) ^^ i) m ≤ m ⤜ REC (λD s. sup (a s ⤜ D) (RETURN s))"
      apply (induction i arbitrary: m)
      apply simp
      apply (subst REC_unfold, refine_mono)
      apply (simp add: pw_le_iff refine_pw_simps, blast)
      
      apply (subst funpow_Suc_right)
      apply simp
      apply (rule order_trans)
      apply rprems
      apply simp
  
      apply (subst (2) REC_unfold, refine_mono)
      apply (simp add: bind_distrib_sup2)
      done
  qed
  
  
  private lemma tailrec_transform_aux3: "REC (λD s. sup (a s ⤜ D) (RETURN s)) s ⤜ b 
    ≤ REC (λD s. sup (a s ⤜ D) (b s)) s"
    apply (subst bind_le_shift)
    apply (rule REC_rule, refine_mono)
    apply (rule TrueI)
    apply auto
      apply (subst (asm) (4) REC_unfold, refine_mono)
      apply (rule order_trans[OF bind_mono(1)[OF order_refl]])
      apply rprems
      apply (subst (3) REC_unfold, refine_mono)
      apply (simp add: refine_pw_simps pw_le_iff, blast)
  
      apply (subst REC_unfold, refine_mono, simp)
    done
  
  private lemma tailrec_transform2:
    "lfp (λx. sup m (bind x a)) ⤜ b ≤ m ⤜ REC (λD s. sup (a s ⤜ D) (b s))"
  proof -
    from bind_mono(1)[OF tailrec_transform_aux2 order_refl]
    have "lfp (λx. sup m (bind x a)) ⤜ b 
      ≤ m ⤜ (λx. REC (λD s. sup (a s ⤜ D) (RETURN s)) x ⤜ b)"
      by simp
    also from bind_mono(1)[OF order_refl tailrec_transform_aux3]
    have "… ≤ m ⤜ REC (λD s. sup (a s ⤜ D) (b s))" .
    finally show ?thesis .
  qed  
  
  definition "tailrec_body a b ≡ (λD s. sup (bind (a s) D) (b s))"
  
  theorem tailrec_transform: 
    "m ⤜ REC (λD s. sup (a s ⤜ D) (b s)) = lfp (λx. sup m (bind x a)) ⤜ b"
    apply (rule antisym)
    apply (rule tailrec_transform1)  
    apply (rule tailrec_transform2)  
    done
  
  theorem tailrec_transform': 
    "m ⤜ REC (tailrec_body a b) = lfp (λx. sup m (bind x a)) ⤜ b"
    unfolding tailrec_body_def
    by (rule tailrec_transform)
  
  lemma "WHILE c f = 
    REC (tailrec_body 
      (λs. do {ASSUME (c s); f s}) 
      (λs. do {ASSUME (¬c s); RETURN s})
    )"
    unfolding WHILE_def WHILEI_def WHILEI_body_def tailrec_body_def
    apply (fo_rule fun_cong arg_cong)+ apply (intro ext)
    apply auto
    done
  
  lemma WHILEI_tailrec_conv: "WHILEI I c f = 
    REC (tailrec_body 
      (λs. do {ASSERT (I s); ASSUME (c s); f s}) 
      (λs. do {ASSERT (I s); ASSUME (¬c s); RETURN s})
    )"
    unfolding WHILEI_def WHILEI_body_def tailrec_body_def
    apply (fo_rule fun_cong arg_cong)+ apply (intro ext)
    apply auto
    done
  
  lemma WHILEIT_tailrec_conv: "WHILEIT I c f = 
    RECT (tailrec_body 
      (λs. do {ASSERT (I s); ASSUME (c s); f s}) 
      (λs. do {ASSERT (I s); ASSUME (¬c s); RETURN s})
    )"
    unfolding WHILEIT_def WHILEI_body_def tailrec_body_def
    apply (fo_rule fun_cong arg_cong)+ apply (intro ext)
    apply auto
    done
  
  
  definition "WHILEI_lfp_body I m c f ≡ 
    (λx. sup m (do {
       s ← x;
       _ ← ASSERT (I s);
       _ ← ASSUME (c s);
       f s
     }))"
    
  lemma WHILEI_lfp_conv: "m ⤜ WHILEI I c f = 
    do { 
      s ← lfp (WHILEI_lfp_body I m c f); 
      ASSERT (I s); 
      ASSUME (¬c s); 
      RETURN s 
    }"
    unfolding WHILEI_lfp_body_def
    apply (subst WHILEI_tailrec_conv)
    apply (subst tailrec_transform')
    ..

end

subsubsection ‹Most Specific Invariant›
  
definition msii ― ‹Most specific invariant for WHILE-loop›
  where "msii I m c f ≡ lfp (WHILEI_lfp_body I m c f)"

lemma [simp, intro!]: "mono (WHILEI_lfp_body I m c f)"
  unfolding WHILEI_lfp_body_def by tagged_solver

definition "filter_ASSUME c m ≡ do {x←m; ASSUME (c x); RETURN x}"
definition "filter_ASSERT c m ≡ do {x←m; ASSERT (c x); RETURN x}"

lemma [refine_pw_simps]: "nofail (filter_ASSUME c m) ⟷ nofail m"
  unfolding filter_ASSUME_def
  by (simp add: refine_pw_simps)

lemma [refine_pw_simps]: "inres (filter_ASSUME c m) x 
  ⟷ (nofail m ⟶ inres m x ∧ c x)"
  unfolding filter_ASSUME_def
  by (simp add: refine_pw_simps)

lemma msii_is_invar:
  "m ≤ msii I m c f"
  "m ≤ msii I m c f ⟹ bind (filter_ASSUME c (filter_ASSERT I m)) f ≤ msii I m c f"
  unfolding  msii_def
  apply -
  apply (subst lfp_unfold, simp)
  apply (simp add: WHILEI_lfp_body_def)

  unfolding filter_ASSUME_def filter_ASSERT_def
  apply (subst lfp_unfold, simp)
  apply (simp add: WHILEI_lfp_body_def)
  apply (simp only: refine_pw_simps pw_le_iff) apply blast
  done

lemma WHILE_msii_conv: "m ⤜ WHILEI I c f 
  = filter_ASSUME (Not o c) (filter_ASSERT I (msii I m c f))"
  unfolding WHILEI_lfp_conv filter_ASSERT_def filter_ASSUME_def msii_def
  by simp

lemma msii_induct: 
  assumes I0: "m0 ≤ P"
  assumes IS: "⋀m. ⟦m ≤ msii I m0 c f; m ≤ P;
    filter_ASSUME c (filter_ASSERT I m) ⤜ f ≤ msii I m0 c f
      ⟧ ⟹ filter_ASSUME c (filter_ASSERT I m) ⤜ f ≤ P"
  shows "msii I m0 c f ≤ P"
  unfolding msii_def WHILEI_lfp_body_def
  apply (rule lfp_gen_induct, tagged_solver)
  unfolding msii_def[symmetric] WHILEI_lfp_body_def[symmetric]
  apply (rule I0)
  apply (drule IS, assumption)
  unfolding filter_ASSERT_def filter_ASSUME_def
  apply simp_all
  done

subsubsection ‹Reachable without fail›
text ‹Reachable states in a while loop, ignoring failing states›

  (* (R)eachable states (w)ith(o)ut (f)ail. All non-fail states reachable
    in a while-loop. *)
  inductive rwof :: "'a nres ⇒ ('a ⇒ bool) ⇒ ('a ⇒ 'a nres) ⇒ 'a ⇒ bool"
    for m0 cond step 
    where
      init: "⟦ m0=RES X; x∈X ⟧ ⟹ rwof m0 cond step x"
    | step: "⟦ rwof m0 cond step x; cond x; step x = RES Y; y∈Y ⟧ 
      ⟹ rwof m0 cond step y"

  (* This lemma establishes consequences of rwof as invariants. *)
  lemma establish_rwof_invar:
    assumes I: "m0 ≤⇩n SPEC I"
    assumes S: "⋀s. ⟦ rwof m0 cond step s; I s; cond s ⟧ 
      ⟹ step s ≤⇩n SPEC I"
    assumes "rwof m0 cond step s"
    shows "I s"
    using assms(3)
    apply induct
    using I apply auto []
    using S apply fastforce []
    done

  (* Predicate to express an rwof-invariant *)
  definition "is_rwof_invar m0 cond step I ≡ 
      (m0 ≤⇩n SPEC I)
    ∧ (∀s. rwof m0 cond step s ∧ I s ∧ cond s 
        ⟶ step s ≤⇩n SPEC I )"

  lemma is_rwof_invarI[intro?]:
    assumes I: "m0 ≤⇩n SPEC I"
    assumes S: "⋀s. ⟦ rwof m0 cond step s; I s; cond s ⟧ 
      ⟹ step s ≤⇩n SPEC I"
    shows "is_rwof_invar m0 cond step I"
    using assms unfolding is_rwof_invar_def by blast

  lemma rwof_cons: "⟦is_rwof_invar m0 cond step I; rwof m0 cond step s⟧ ⟹ I s"
    unfolding is_rwof_invar_def
    using establish_rwof_invar[of m0 I cond step s]
    by blast
    

  (* This lemma proves a specification for the while loop, based on rwof
    and a nofail-proof. *)
  lemma rwof_WHILE_rule:
    assumes I0: "m0 ≤ SPEC I"
    assumes S: "⋀s. ⟦ rwof m0 cond step s; I s; cond s ⟧ ⟹ step s ≤ SPEC I"
    shows "m0 ⤜ WHILE cond step ≤ SPEC (λs. rwof m0 cond step s ∧ ¬cond s ∧ I s)"
  proof -
    from I0 obtain M0 where [simp]: "m0 = RES M0" and "M0 ⊆ Collect I"
      by (cases m0) auto

    show ?thesis 
      apply simp
      apply refine_vcg
      apply (rule WHILE_rule[where I="λs. I s ∧ rwof m0 cond step s"])
    proof -
      fix s assume "s∈M0" thus "I s ∧ rwof m0 cond step s"
        using I0 by (auto intro: rwof.init) []

    next
      fix s
      assume A: "I s ∧ rwof m0 cond step s" and C: "cond s"
      hence "step s ≤ SPEC I" by - (rule S, simp_all)
      also then obtain S' where "step s = RES S'" by (cases "step s") auto
      from rwof.step[OF conjunct2[OF A] C this] this 
      have "step s ≤ SPEC (rwof m0 cond step)" by auto
      finally (SPEC_rule_conjI) 
      show "step s ≤ SPEC (λs. I s ∧ rwof m0 cond step s)" .
    qed auto
  qed

subsubsection ‹Filtering out states that satisfy the loop condition›
  (* A shortcut definition for filtering out all results that satisfy
    the loop condition. Intuitively, filtering out these results from the 
    best invariant gives the results of the while loop. *)
  definition filter_nb :: "('a ⇒ bool) ⇒ 'a nres ⇒ 'a nres" where 
    "filter_nb b I ≡ do {s←I; ASSUME (¬b s); RETURN s}"
  
  lemma pw_filter_nb[refine_pw_simps]:
    "nofail (filter_nb b I) ⟷ nofail I"
    "inres (filter_nb b I) x ⟷ (nofail I ⟶ inres I x ∧ ¬b x)"
    unfolding filter_nb_def
    by (simp_all add: refine_pw_simps)

  lemma filter_nb_mono: "m≤m' ⟹ filter_nb cond m ≤ filter_nb cond m'"
    unfolding filter_nb_def
    by refine_mono

  lemma filter_nb_cont: 
    "filter_nb cond (Sup M) = Sup {filter_nb cond m | m. m ∈ M}"
    apply (rule antisym)
    apply (simp add: pw_le_iff refine_pw_simps)
    apply (auto intro: not_nofail_inres simp: refine_pw_simps) []
    
    apply (simp add: pw_le_iff refine_pw_simps)
    apply (auto intro: not_nofail_inres simp: refine_pw_simps) []
    done

  lemma filter_nb_FAIL[simp]: "filter_nb cond FAIL = FAIL"
    by (simp add: filter_nb_def)

  lemma filter_nb_RES[simp]: "filter_nb cond (RES X) = RES {x∈X. ¬cond x}"
    by (simp add: pw_eq_iff refine_pw_simps)

subsubsection ‹Bounded while-loop›

  (* A while rule that establishes an inductive invariant,
    and then filters out the results satisfying the condition. *)
  lemma WHILE_rule_gen_le:
    assumes I0: "m0 ≤ I"
    assumes ISTEP: "⋀s. ⟦RETURN s ≤ I; b s⟧ ⟹ f s ≤ I"
    shows "m0 ⤜ WHILE b f ≤ filter_nb b I"
      apply (unfold WHILE_def WHILEI_def)
      apply (refine_rcg order_trans[OF I0] refine_vcg pw_bind_leI)
      using I0 apply (simp add: pw_le_iff refine_pw_simps)

      apply (rule REC_rule[OF WHILEI_body_trimono, where pre="λs. RETURN s ≤ I"])
        using I0 apply (simp add: pw_le_iff refine_pw_simps)
      
        unfolding WHILEI_body_def
        apply (split if_split)+
        apply (intro impI conjI)
        apply (simp_all)
        using ISTEP
        apply (simp (no_asm_use) only: pw_le_iff refine_pw_simps) apply blast
        apply (simp only: pw_le_iff refine_pw_simps) apply metis 
    done


  primrec bounded_WHILE' 
    :: "nat ⇒ ('a ⇒ bool) ⇒ ('a ⇒ 'a nres) ⇒ 'a nres ⇒ 'a nres" 
  where
    "bounded_WHILE' 0 cond step m = m"
  | "bounded_WHILE' (Suc n) cond step m = do {
      x ← m;
      if cond x then bounded_WHILE' n cond step (step x)
      else RETURN x
    }"

  primrec bounded_WHILE
    :: "nat ⇒ ('a ⇒ bool) ⇒ ('a ⇒ 'a nres) ⇒ 'a nres ⇒ 'a nres" 
  where
    "bounded_WHILE 0 cond step m = m"
  | "bounded_WHILE (Suc n) cond step m = do {
      x ← bounded_WHILE n cond step m;
      if cond x then step x
      else RETURN x
    }"

  lemma bounded_WHILE_shift: "do {
             x ← m;
             if cond x then bounded_WHILE n cond step (step x) else RETURN x
           } = do {
             x ← bounded_WHILE n cond step m;
             if cond x then step x else RETURN x
           }"
  proof (induction n arbitrary: m)
    case 0 thus ?case by (simp cong: if_cong)
  next
    case (Suc n) 

    have aux1: "do {
      x ← m;
      if cond x then do {
                       x ← bounded_WHILE n cond step (step x);
                       if cond x then step x else RETURN x
                     }
      else RETURN x
    } = do {
      x ← do {
        x ← m; 
        if cond x then bounded_WHILE n cond step (step x) else RETURN x
      };
      if cond x then step x else RETURN x
    }"
    by (simp add: pw_eq_iff refine_pw_simps)

    show ?case
      apply (simp cong: if_cong)
      apply (subst aux1)
      apply (subst Suc.IH)
      apply (simp add: pw_eq_iff refine_pw_simps)
      done
  qed


  lemma bounded_WHILE'_eq: 
    "bounded_WHILE' n cond step m = bounded_WHILE n cond step m"
    apply (induct n arbitrary: m)
    apply (auto cong: if_cong simp: bounded_WHILE_shift)
    done

  lemma mWHILE_unfold: "m ⤜ WHILE cond step = do {
      x ← m;
      if cond x then step x ⤜ WHILE cond step
      else RETURN x
    }"
    by (subst WHILE_unfold[abs_def]) (rule refl)

  lemma WHILE_bounded_aux1: 
    "filter_nb cond (bounded_WHILE n cond step m) ≤ m ⤜ WHILE cond step"
    unfolding bounded_WHILE'_eq[symmetric]
    apply (induct n arbitrary: m)
    apply simp
    apply (subst mWHILE_unfold)
    apply (simp add: pw_le_iff refine_pw_simps, blast)
    
    apply simp
    apply (subst mWHILE_unfold)
    apply (auto simp add: pw_le_iff refine_pw_simps)
    done

  lemma WHILE_bounded_aux2:
    "m ⤜ WHILE cond step 
      ≤ filter_nb cond (Sup {bounded_WHILE n cond step m | n. True})"
    apply (rule WHILE_rule_gen_le)
    apply (metis (mono_tags, lifting) Sup_upper bounded_WHILE.simps(1) 
      mem_Collect_eq)
  proof - 
    fix s
    assume "RETURN s ≤ Sup {bounded_WHILE n cond step m |n. True}"
    then obtain n where "RETURN s ≤ bounded_WHILE n cond step m"
      by (fold inres_def) (auto simp: refine_pw_simps)
    moreover assume "cond s"
    ultimately have "step s ≤ bounded_WHILE (Suc n) cond step m"
      by (simp add: pw_le_iff refine_pw_simps, blast)
    thus "step s ≤ Sup {bounded_WHILE n cond step m |n. True}"
      by (metis (mono_tags, lifting) Sup_upper2 mem_Collect_eq)
  qed

   
  lemma WHILE_bounded: 
    "m ⤜ WHILE cond step 
    = filter_nb cond (Sup {bounded_WHILE n cond step m | n. True})"
    apply (rule antisym)
    apply (rule WHILE_bounded_aux2)

    apply (simp add: filter_nb_cont)
    apply (rule Sup_least)
    apply (auto simp: WHILE_bounded_aux1)
    done

  subsubsection ‹Relation to rwof›

  lemma rwof_in_bounded_WHILE:
    assumes "rwof m0 cond step s" 
    shows "∃n. RETURN s ≤ (bounded_WHILE n cond step m0)"
    using assms
    apply induction
    apply (rule_tac x=0 in exI)
    apply simp

    apply clarsimp
    apply (rule_tac x="Suc n" in exI)
    apply (auto simp add: pw_le_iff refine_pw_simps) []
    done

  lemma bounded_WHILE_FAIL_rwof:
    assumes "bounded_WHILE n cond step m0 = FAIL"
    assumes M0: "m0 ≠ FAIL"
    shows "∃n'<n. ∃x X. 
        bounded_WHILE n' cond step m0 = RES X 
      ∧ x∈X ∧ cond x ∧ step x = FAIL"
    using assms
  proof (induction n)
    case 0 thus ?case by simp
  next
    case (Suc n)
    assume "bounded_WHILE (Suc n) cond step m0 = FAIL"
    hence "bounded_WHILE n cond step m0 = FAIL 
      ∨ (∃X x. bounded_WHILE n cond step m0 = RES X 
          ∧ x∈X ∧ cond x ∧ step x = FAIL)"
      (is "?C1 ∨ ?C2")
      apply (cases "bounded_WHILE n cond step m0")
      apply simp
      apply (simp add: pw_eq_iff refine_pw_simps split: if_split_asm)
      apply (auto intro: not_nofail_inres simp: refine_pw_simps)
      done
    moreover {
      assume ?C1
      from Suc.IH[OF this M0] obtain n' x X where "n' < n" and
        1: "bounded_WHILE n' cond step m0 = RES X ∧ x∈X ∧ cond x ∧ step x = FAIL"
        by blast
      hence 2: "n' < Suc n" by simp
      from 1 2 have ?case by blast
    } moreover {
      assume ?C2
      hence ?case by blast
    } ultimately show ?case by blast
  qed

  lemma bounded_WHILE_RES_rwof:
    assumes "bounded_WHILE n cond step m0 = RES X"
    assumes "x∈X"
    shows "rwof m0 cond step x"
    using assms
  proof (induction n arbitrary: x X)
    case 0 thus ?case by (simp add: rwof.init)
  next
    case (Suc n)

    from Suc.prems(1) obtain Xh where
      BWN: "bounded_WHILE n cond step m0 = RES Xh"
      and "∀x∈Xh. cond x ⟶ nofail (step x)"
      and "X = {x'. ∃x∈Xh. cond x ∧ inres (step x) x'} ∪ {x. x∈Xh ∧ ¬cond x} "
      apply (cases "bounded_WHILE n cond step m0")
      apply simp
      apply (rule that, assumption)
      apply (force simp: refine_pw_simps pw_eq_iff) []
      apply (auto simp add: refine_pw_simps pw_eq_iff split: if_split_asm)
      done
    with Suc.prems(2) obtain xh X' where 
        "xh∈Xh" and
      C: "cond xh ⟶ step xh = RES X' ∧ x∈X'" and NC:  "¬cond xh ⟶ x=xh"
      by (auto simp: nofail_RES_conv)
    
    show ?case  
      apply (cases "cond xh")
        apply (rule rwof.step[where Y=X'])
          apply (rule Suc.IH[OF BWN ‹xh∈Xh›])
          apply assumption
          apply (simp_all add: C) [2]
        
        apply (rule Suc.IH[OF BWN])
        apply (simp add: NC ‹xh∈Xh›)
      done
  qed
      

  lemma rwof_FAIL_imp_WHILE_FAIL:
    assumes RW: "rwof m0 cond step s" 
    and C: "cond s" 
    and S: "step s = FAIL"
    shows "m0 ⤜ WHILE cond step = FAIL"
  proof -
    from rwof_in_bounded_WHILE[OF RW] obtain n where 
      "RETURN s ≤ bounded_WHILE n cond step m0" ..
    with C have "step s ≤ bounded_WHILE (Suc n) cond step m0"
      by (auto simp add: pw_le_iff refine_pw_simps)
    with S have "bounded_WHILE (Suc n) cond step m0 = FAIL" by simp
    with WHILE_bounded_aux1[of cond "Suc n" step m0] show ?thesis
      by (simp del: bounded_WHILE.simps)
  qed

  lemma pw_bounded_WHILE_RES_rwof: "⟦ nofail (bounded_WHILE n cond step m0); 
    inres (bounded_WHILE n cond step m0) x ⟧ ⟹ rwof m0 cond step x"
    using bounded_WHILE_RES_rwof[of n cond step m0 _ x]
    by (auto simp add: pw_eq_iff)
    
  corollary WHILE_nofail_imp_rwof_nofail:
    assumes "nofail (m0 ⤜ WHILE cond step)"
    assumes RW: "rwof m0 cond step s" 
    assumes C: "cond s"
    shows "nofail (step s)"
    apply (rule ccontr) apply (simp add: nofail_def)
    using assms rwof_FAIL_imp_WHILE_FAIL[OF RW C]
    by auto

  (* TODO: Move *)
  lemma WHILE_le_WHILEI: "WHILE b f s ≤ WHILEI I b f s"
    unfolding WHILE_def
    by (rule WHILEI_weaken) simp

  corollary WHILEI_nofail_imp_rwof_nofail:
    assumes NF: "nofail (m0 ⤜ WHILEI I cond step)"
    assumes RW: "rwof m0 cond step s" 
    assumes C: "cond s"
    shows "nofail (step s)"
  proof -
    from NF have "nofail (m0 ⤜ WHILE cond step)"
      using WHILE_le_WHILEI 
      by (fastforce simp: pw_le_iff refine_pw_simps)
    from WHILE_nofail_imp_rwof_nofail[OF this RW C] show ?thesis .
  qed

  corollary WHILET_nofail_imp_rwof_nofail:
    assumes NF: "nofail (m0 ⤜ WHILET cond step)"
    assumes RW: "rwof m0 cond step s" 
    assumes C: "cond s"
    shows "nofail (step s)"
  proof -
    from NF have "nofail (m0 ⤜ WHILE cond step)"
      using WHILEI_le_WHILEIT unfolding WHILE_def WHILET_def 
      by (fastforce simp: pw_le_iff refine_pw_simps)
    from WHILE_nofail_imp_rwof_nofail[OF this RW C] show ?thesis .
  qed

  corollary WHILEIT_nofail_imp_rwof_nofail:
    assumes NF: "nofail (m0 ⤜ WHILEIT I cond step)"
    assumes RW: "rwof m0 cond step s" 
    assumes C: "cond s"
    shows "nofail (step s)"
  proof -
    from NF have "nofail (m0 ⤜ WHILE cond step)"
      using WHILE_le_WHILEI WHILEI_le_WHILEIT unfolding WHILE_def
      by (fastforce simp: pw_le_iff refine_pw_simps)
    from WHILE_nofail_imp_rwof_nofail[OF this RW C] show ?thesis .
  qed

  lemma pw_rwof_in_bounded_WHILE:
    "rwof m0 cond step x ⟹ ∃n. inres (bounded_WHILE n cond step m0) x"
    using rwof_in_bounded_WHILE[of m0 cond step x]
    by (auto simp add: pw_le_iff intro: not_nofail_inres)

subsubsection ‹WHILE-loops in the nofail-case›
  lemma nofail_WHILE_eq_rwof: 
    assumes NF: "nofail (m0 ⤜ WHILE cond step)"
    shows "m0 ⤜ WHILE cond step = SPEC (λs. rwof m0 cond step s ∧ ¬cond s)"
  proof -
    from NF WHILE_bounded[of m0 cond step] have NF': 
      "nofail (Sup {filter_nb cond m |m. ∃n. m = bounded_WHILE n cond step m0})"
      by (auto simp: filter_nb_cont)

    (*from NF WHILE_bounded[of m0 cond step] obtain X 
      where FR:
        "Sup {filter_nb cond m |m. ∃n. m = bounded_WHILE n cond step m0} = RES X"
      by (auto simp: nofail_RES_conv filter_nb_cont)*)
    
    show ?thesis
      unfolding WHILE_bounded[of m0 cond step] filter_nb_cont
      apply simp
    proof (rule antisym)
      show "Sup {filter_nb cond m |m. ∃n. m = bounded_WHILE n cond step m0}
        ≤ SPEC (λs. rwof m0 cond step s ∧ ¬ cond s)"
        using NF' pw_bounded_WHILE_RES_rwof[of _ cond step m0]
        by (fastforce simp: pw_le_iff refine_pw_simps)
    next
      show "SPEC (λs. rwof m0 cond step s ∧ ¬ cond s)
        ≤ Sup {filter_nb cond m |m. ∃n. m = bounded_WHILE n cond step m0}"      
        using NF' pw_rwof_in_bounded_WHILE[of m0 cond step]
        by (fastforce simp: pw_le_iff refine_pw_simps)
    qed
  qed

  lemma WHILE_refine_rwof:
    assumes "nofail (m ⤜ WHILE c f) ⟹ mi ≤ SPEC (λs. rwof m c f s ∧ ¬c s)"
    shows "mi ≤ m ⤜ WHILE c f"
    apply (cases "nofail (m ⤜ WHILE c f)")
    apply (subst nofail_WHILE_eq_rwof, simp, fact)
    apply (simp add: pw_le_iff)
    done


  lemma pw_rwof_init:
    assumes NF: "nofail (m0 ⤜ WHILE cond step)"
    shows "inres m0 s ⟹ rwof m0 cond step s" and "nofail m0"
    apply -
    using NF apply (cases m0, simp)
    apply (rule rwof.init, assumption)
    apply auto []
    
    using NF apply (simp add: refine_pw_simps)
    done

  lemma rwof_init:
    assumes NF: "nofail (m0 ⤜ WHILE cond step)" 
    shows "m0 ≤ SPEC (rwof m0 cond step)"
    using pw_rwof_init[OF NF]
    by (simp add: pw_le_iff refine_pw_simps)
  
  lemma pw_rwof_step':
    assumes NF: "nofail (step s)"
    assumes R: "rwof m0 cond step s"
    assumes C: "cond s"
    shows "inres (step s) s' ⟹ rwof m0 cond step s'"
    using NF
    apply (clarsimp simp: nofail_RES_conv)
    apply (rule rwof.step[OF R C])
    apply (assumption)
    by simp

  lemma rwof_step': 
    "⟦ nofail (step s); rwof m0 cond step s; cond s ⟧
    ⟹ step s ≤ SPEC (rwof m0 cond step)"
    using pw_rwof_step'[of step s m0 cond]
    by (simp add: pw_le_iff refine_pw_simps)

  lemma pw_rwof_step:
    assumes NF: "nofail (m0 ⤜ WHILE cond step)"
    assumes R: "rwof m0 cond step s"
    assumes C: "cond s"
    shows "inres (step s) s' ⟹ rwof m0 cond step s'"
      and "nofail (step s)"
    using WHILE_nofail_imp_rwof_nofail[OF NF R C] pw_rwof_step'[OF _ assms(2-)]
    by simp_all

  lemma rwof_step: 
    "⟦ nofail (m0 ⤜ WHILE cond step); rwof m0 cond step s; cond s ⟧
    ⟹ step s ≤ SPEC (rwof m0 cond step)"
    using pw_rwof_step[of m0 cond step s]
    by (simp add: pw_le_iff refine_pw_simps)

  lemma (in -) rwof_leof_init: "m ≤⇩n SPEC (rwof m c f)"
    apply rule
    using rwof.init
    apply (fastforce simp: nofail_RES_conv)
    done

  lemma (in -) rwof_leof_step: "⟦rwof m c f s; c s⟧ ⟹ f s ≤⇩n SPEC (rwof m c f)"
    apply rule
    using rwof.step
    apply (fastforce simp: nofail_RES_conv)
    done


  lemma (in -) rwof_step_refine:
    assumes NF: "nofail (m0 ⤜ WHILE cond step)"  
    assumes A: "rwof m0 cond step' s"
    assumes FR: "⋀s. ⟦ rwof m0 cond step s; cond s ⟧ ⟹ step' s ≤⇩n step s"
    shows "rwof m0 cond step s"
    apply (rule establish_rwof_invar[OF _ _ A])
      apply (rule rwof_leof_init)

      apply (rule leof_trans_nofail[OF FR], assumption+)
        apply (rule WHILE_nofail_imp_rwof_nofail[OF NF], assumption+)

        apply (simp add: rwof_leof_step)
    done

subsubsection ‹Adding Invariants›
  lemma WHILE_eq_I_rwof: "m ⤜ WHILE c f = m ⤜ WHILEI (rwof m c f) c f"
  proof (rule antisym)
    have "m ⤜ WHILEI (rwof m c f) c f
      ≤ ⇓{(s,s) | s. rwof m c f s} 
        (m ⤜ WHILE c f)"
      unfolding WHILE_def
      apply (rule bind_refine)
      apply (rule intro_prgR[where R="{(s,s) | s. rwof m c f s}"])
      apply (auto simp: pw_le_iff refine_pw_simps) []
      apply (cases m, simp, rule rwof.init, simp_all) []
    
      apply (rule WHILEI_refine)
      apply (auto simp: pw_le_iff refine_pw_simps pw_rwof_step')
      done
    thus "m ⤜ WHILEI (rwof m c f) c f ≤ m ⤜ WHILE c f"
      by (simp add: pw_le_iff refine_pw_simps)
  next
    show "m ⤜ WHILE c f ≤ m ⤜ WHILEI (rwof m c f) c f"
      unfolding WHILE_def 
      apply (rule bind_mono)
      apply (rule order_refl)
      apply (rule WHILEI_weaken)
      ..
  qed

  lemma WHILET_eq_I_rwof: "m ⤜ WHILET c f = m ⤜ WHILEIT (rwof m c f) c f"
  proof (rule antisym)
    have "m ⤜ WHILEIT (rwof m c f) c f
      ≤ ⇓{(s,s) | s. rwof m c f s} 
        (m ⤜ WHILET c f)"
      unfolding WHILET_def
      apply (rule bind_refine)
      apply (rule intro_prgR[where R="{(s,s) | s. rwof m c f s}"])
      apply (auto simp: pw_le_iff refine_pw_simps) []
      apply (cases m, simp, rule rwof.init, simp_all) []
    
      apply (rule WHILEIT_refine)
      apply (auto simp: pw_le_iff refine_pw_simps pw_rwof_step')
      done
    thus "m ⤜ WHILEIT (rwof m c f) c f ≤ m ⤜ WHILET c f"
      by (simp add: pw_le_iff refine_pw_simps)
  next
    show "m ⤜ WHILET c f ≤ m ⤜ WHILEIT (rwof m c f) c f"
      unfolding WHILET_def 
      apply (rule bind_mono)
      apply (rule order_refl)
      apply (rule WHILEIT_weaken)
      ..
  qed


subsubsection ‹Refinement›
lemma rwof_refine:
  assumes RW: "rwof m c f s"
  assumes NF: "nofail (m' ⤜ WHILE c' f')"
  assumes M: "m ≤⇩n ⇓R m'"
  assumes C: "⋀s s'. ⟦(s,s')∈R; rwof m c f s; rwof m' c' f' s'⟧ ⟹ c s = c' s'"
  assumes S: "⋀s s'. ⟦(s,s')∈R; rwof m c f s; rwof m' c' f' s'; c s; c' s'⟧ ⟹ f s ≤⇩n ⇓R (f' s')"
  shows "∃s'. (s,s')∈R ∧ rwof m' c' f' s'"
  using RW
  apply (induction rule: establish_rwof_invar[rotated -1,consumes 1])
  using M rwof_init[OF NF] 
  apply (simp only: pw_leof_iff pw_le_iff refine_pw_simps, blast) []

  using C S rwof_step[OF NF] 
  apply (simp only: pw_leof_iff pw_le_iff refine_pw_simps, blast) []
  done

subsubsection ‹Total Correct Loops›
text ‹In this theory, we show that every non-failing total-correct 
  while loop gives rise to a compatible well-founded relation›


definition rwof_rel 
  ― ‹Transitions in a while-loop as relation›
  where "rwof_rel init cond step 
    ≡ {(s,s'). rwof init cond step s ∧ cond s ∧ inres (step s) s'}"

lemma rwof_rel_spec: "⟦rwof init cond step s; cond s⟧ 
  ⟹ step s ≤⇩n SPEC (λs'. (s,s')∈rwof_rel init cond step)"
  unfolding rwof_rel_def
  by (auto simp: pw_leof_iff refine_pw_simps)  


lemma rwof_reachable:
  assumes "rwof init cond step s"
  shows "∃s0. inres init s0 ∧ (s0,s)∈(rwof_rel init cond step)⇧*"
  using assms
  apply (induction)
  unfolding rwof_rel_def
  apply (auto intro: rwof.intros) []
  apply clarsimp
  apply (intro exI conjI, assumption)
  apply (rule rtrancl_into_rtrancl, assumption)
  apply (auto intro: rwof.intros) []
  done
  
theorem nofail_WHILEIT_wf_rel: 
  assumes NF: "nofail (init ⤜ WHILEIT I cond step)"
  shows "wf ((rwof_rel init cond step)¯)"
proof (rule ccontr)
  assume "¬wf ((rwof_rel init cond step)¯)"
  then obtain f where IP: "⋀ i. (f i, f (Suc i)) ∈ rwof_rel init cond step"
    unfolding wf_iff_no_infinite_down_chain by auto
  hence "rwof init cond step (f 0)" by (auto simp: rwof_rel_def)
  then obtain s0 sn where "(s0, sn) ∈ (rwof_rel init cond step)⇧*" "inres init s0" "sn = f 0"
    using rwof_reachable by metis
  then obtain f where P: "⋀ i. (f i, f (Suc i)) ∈ rwof_rel init cond step" and I: "inres init (f 0)"
  using IP
  proof (induct arbitrary: f)
    case (step sk sn)
    let ?f = "case_nat sk f"
    have "sk = ?f 0" "⋀ i. (?f i, ?f (Suc i)) ∈ rwof_rel init cond step"
      using step by (auto split: nat.splits)
    then show ?case using step by blast
  qed auto

  from P have [simp]: "⋀i. cond (f i)"
    unfolding rwof_rel_def by auto

  from P have SIR: "⋀i. inres (step (f i)) (f (Suc i))"
    unfolding rwof_rel_def by auto

  define F where "F = (WHILEI_body (⤜) RETURN I cond step)"

  {
    assume M: "trimono F"
    define f' where "f' x = (if x∈range f then FAIL else gfp F x)" for x

    have "f' ≤ F f'"
      unfolding f'_def
      apply (rule le_funI)
      apply (case_tac "x∈range f")
      apply simp_all
      defer
      apply (subst gfp_unfold)
      using M apply (simp add: trimono_def)
      apply (unfold F_def WHILEI_body_def) []
      apply (auto simp: pw_le_iff refine_pw_simps) []      

      apply (unfold F_def WHILEI_body_def not_nofail_iff[symmetric]) []
      using SIR
      apply (auto simp: pw_le_iff refine_pw_simps) []      
      done  
    from gfp_upperbound[of f' F,OF this] have "⋀x. f' x ≤ gfp F x"
      by (auto dest: le_funD)
    from this[of "f 0"] have "gfp F (f 0) = FAIL"
      unfolding f'_def
      by auto

  } note aux=this

  have "FAIL ≤ WHILEIT I cond step (f 0)" 
    unfolding WHILET_def WHILEIT_def RECT_def
    apply clarsimp
    apply (subst gfp_eq_flatf_gfp[symmetric])
    apply (simp_all add: trimono_def) [2]
    apply (unfold F_def[symmetric])
    by (rule aux)
  with NF I show False by (auto simp: refine_pw_simps)
qed


subsection ‹Convenience›

subsubsection ‹Iterate over range of list›
lemma range_set_WHILE:
  assumes CEQ: "⋀i s. c (i,s) ⟷ i<u"
  assumes F0: "F {} s0 = s0"
  assumes Fs: "⋀s i X. ⟦l≤i; i<u⟧ 
    ⟹ f (i, (F X s)) ≤ SPEC (λ(i',r). i'=i+1 ∧ r=F (insert (list!i) X) s)"
  shows "WHILET c f (l,s0) 
    ≤ SPEC (λ(_,r). r=F {list!i | i. l≤i ∧ i<u} s0)"
  apply (cases "¬(l<u)")
  apply (subst WHILET_unfold)
  using F0 apply (simp add: CEQ)
  apply (rule subst, assumption)
  apply ((fo_rule cong refl)+, auto) []

  apply (simp)
  apply (rule WHILET_rule[
    where R = "measure (λ(i,_). u-i)"
    and I = "λ(i,s). l≤i ∧ i≤u ∧ s = F {list!j | j. l≤j ∧ j<i} s0"
    ])
  apply rule

  apply simp
  apply (subst F0[symmetric])
  apply ((fo_rule cong refl)+, auto) []

  apply (clarsimp simp: CEQ)
  apply (rule order_trans[OF Fs], simp_all) []
  apply (auto
    intro!: fun_cong[OF arg_cong[of _ _ F]]
    elim: less_SucE) []

  apply (auto simp: CEQ) []
  done


end