Quelle  Imperative_Loops.thy

theory Imperative_Loops
  imports 
    "Refine_Imperative_HOL.Sepref_HOL_Bindings"
    "Refine_Imperative_HOL.Pf_Mono_Prover"
    "Refine_Imperative_HOL.Pf_Add"


begin

section ‹Imperative Loops›

text "An auxiliary while rule provided by Peter Lammich."

lemma heap_WHILET_rule:
  assumes
    "wf R"
    "P ==>_A I s"
    "∧s. <I s * true> bi s <λr. I s * ↑(r ⟷ b s)>_t"
    "∧s. b s ==> <I s * true> f s <λs'. I s' * ↑((s', s) ∈ R)>_t"
    "∧s. ¬ b s ==> I s ==>_A Q s"
  shows "<P * true> heap_WHILET bi f s <Q>_t"
proof -
  have "<I s * true> heap_WHILET bi f s <λs'. I s' * ↑(¬ b s')>_t"
    using assms(1)
  proof (induction arbitrary:)
    case (less s)
    show ?case
    proof (cases "b s")
      case True
      then show ?thesis
        by (subst heap_WHILET_unfold) (sep_auto heap: assms(3,4) less)
    next
      case False
      then show ?thesis
        by (subst heap_WHILET_unfold) (sep_auto heap: assms(3))
    qed
  qed
  then show ?thesis
    apply (rule cons_rule[rotated 2])
     apply (intro ent_star_mono assms(2) ent_refl)
    apply clarsimp
    apply (intro ent_star_mono assms(5) ent_refl)
    .
qed


lemma heap_WHILET_rule':
  assumes
    "wf R"
    "P ==>_A I s si * F"
    "∧si s. <I s si * F> bi si <λr. I s si * F * ↑(r ⟷ b s)>_t"
    "∧si s. b s ==> <I s si * F> f si <λsi'. ∃_As'. I s' si' * F * ↑((s', s) ∈ R)>_t"
    "∧si s. ¬ b s ==> I s si * F ==>_A Q s si"
  shows "<P> heap_WHILET bi f si <λsi. ∃_As. Q s si>_t"
proof -
  have "<I s si * F> heap_WHILET bi f si <λsi'. ∃_As'. I s' si' * F * ↑(¬ b s')>_t"
    using assms(1)
  proof (induction arbitrary: si)
    case (less s)
    show ?case
    proof (cases "b s")
      case True
      then show ?thesis
        apply (subst heap_WHILET_unfold)
        apply (sep_auto heap: assms(3,4) less)
        done
    next
      case False
      then show ?thesis
        by (subst heap_WHILET_unfold) (sep_auto heap: assms(3))
    qed
  qed
  then show ?thesis
    apply (rule cons_rule[rotated 2])
     apply (intro ent_star_mono assms(2) ent_refl)
    apply clarsimp
    apply (sep_auto )
    apply (erule ent_frame_fwd[OF assms(5)])
     apply frame_inference
    by sep_auto

qed

(* Added by NM, just a technicality since this rule fits our use case better *)

text "I derived my own version,
simply because it was a better fit to my use case."

corollary heap_WHILET_rule'':
  assumes
    "wf R"
    "P ==>_A I s"
    "∧s. <I s * true> bi s <λr. I s * ↑(r ⟷ b s)>_t"
    "∧s. b s ==> <I s * true> f s <λs'. I s' * ↑((s', s) ∈ R)>_t"
    "∧s. ¬ b s ==> I s ==>_A Q s"
  shows "<P> heap_WHILET bi f s <Q>_t"
  supply R = heap_WHILET_rule'[of R P "λs si. ↑(s = si) * I s" s _ true bi b f "λs si.↑(s = si) * Q s * true"]
  thm R
  using assms ent_true_drop apply(sep_auto heap: R assms)
  done
    (*
explicit proof:

proof -
  have "<I s * true> heap_WHILET bi f s <\<lambda>s'. I s' * \<up>(\<not> b s')>\<^sub>t"
    using assms(1)
  proof (induction arbitrary:)
    case (less s)
    show ?case
    proof (cases "b s")
      case True
      then show ?thesis
        by (subst heap_WHILET_unfold) (sep_auto heap: assms(3,4) less)
    next
      case False
      then show ?thesis
        by (subst heap_WHILET_unfold) (sep_auto heap: assms(3))
    qed
  qed
  then show ?thesis
    apply (rule cons_rule[rotated 2])
     apply (intro ent_true_drop assms(2) ent_refl)
    apply clarsimp
    apply(intro ent_star_mono assms(5) ent_refl)
    .
qed
*)

end