Quelle  Loops.thy

(*
 * Copyright (C) 2014 NICTA
 * All rights reserved.
 *)

(* Author: David Cock - David.Cock@nicta.com.au *)

section ‹The Loop Rules›

theory Loops imports WellDefined begin

text_raw ‹\label{s:loop_rules}›

text ‹Given a well-defined body, we can annotate a loop using an invariant, just as in the
  setting.›

subsection ‹Liberal and Strict Invariants.›

text ‹A probabilistic invariant generalises a boolean one: it \emph{entails} itself, given
  loop guard.›

definition
  wp_inv :: "('s ==> bool) ==> 's prog ==> ('s ==> real) ==> bool"
where
  "wp_inv G body I ⟷ (∀s. «G¬ s * I s ≤ wp body I s)"

lemma wp_invI:
  "∧I. (∧s. «G¬ s * I s ≤ wp body I s) ==> wp_inv G body I"
  by(simp add:wp_inv_def)

definition
  wlp_inv :: "('s ==> bool) ==> 's prog ==> ('s ==> real) ==> bool"
where
  "wlp_inv G body I ⟷ (∀s. «G¬ s * I s ≤ wlp body I s)"

lemma wlp_invI:
  "∧I. (∧s. «G¬ s * I s ≤ wlp body I s) ==> wlp_inv G body I"
  by(simp add:wlp_inv_def)

lemma wlp_invD:
  "wlp_inv G body I ==> «G¬ s * I s ≤ wlp body I s"
  by(simp add:wlp_inv_def)

text ‹For standard invariants, the multiplication reduces to conjunction.›
lemma wp_inv_stdD:
  assumes inv: "wp_inv G body «I¬"
  and     hb:  "healthy (wp body)"
  shows "«G¬ && «I¬ ⊨!!! wp body «I¬"
proof(rule le_funI)
  fix s
  show "(«G¬ && «I¬) s ≤ wp body «I¬ s"
  proof(cases "G s")
    case False
    with hb show ?thesis
      by(auto simp:exp_conj_def)
  next
    case True
    hence "(«G¬ && «I¬) s = «G¬ s * «I¬ s"
      by(simp add:exp_conj_def)
    also from inv have "«G¬ s * «I¬ s ≤ wp body «I¬ s"
      by(simp add:wp_inv_def)
    finally show ?thesis .
  qed
qed

subsection ‹Partial Correctness›

text ‹Partial correctness for loops🍋‹‹Lemma 7.2.2, \S7, p.~185› in "McIver_M_04"›.›
lemma wlp_Loop:
  assumes wd: "well_def body"
      and uI: "unitary I"
      and inv: "wlp_inv G body I"
  shows "I ≤ wlp do G ⟶ body od (λs. «N G¬ s * I s)"
  (is "I ≤ wlp do G ⟶ body od ?P")
proof -
  let "?f Q s" = "«G¬ s * wlp body Q s + «N G¬ s * ?P s"
  have "I ⊨!!! gfp_exp ?f"
  proof(rule gfp_exp_upperbound[OF _ uI])
    have "I = (λs. («G¬ s + «N G¬ s) * I s)" by(simp add:negate_embed)
    also have "... = (λs. «G¬ s * I s + «N G¬ s * I s)"
      by(simp add:algebra_simps)
    also have "... = (λs. «G¬ s * («G¬ s * I s) + «N G¬ s * («N G¬ s * I s))"
      by(simp add:embed_bool_idem algebra_simps)
    also have "... ⊨!!! (λs. «G¬ s * wlp body I s + «N G¬ s * («N G¬ s * I s))"
      using inv by(auto dest:wlp_invD intro:add_mono mult_left_mono)
    finally show "I ⊨!!! (λs. «G¬ s * wlp body I s + «N G¬ s * («N G¬ s * I s))" .
  qed
  also from uI well_def_wlp_nearly_healthy[OF wd] have "... = wlp do G ⟶ body od ?P"
    by(auto intro!:wlp_Loop1[symmetric] unitary_intros)
  finally show ?thesis .
qed

subsection ‹Total Correctness›
text_raw ‹\label{s:loop_total}›

text ‹The first total correctness lemma for loops which terminate with probability 1🍋‹‹Lemma
 .3.1, \S7, p.~186› in "McIver_M_04"›.›

lemma wp_Loop:
  assumes wd:   "well_def body"
      and inv:  "wlp_inv G body I"
      and unit: "unitary I"
  shows "I && wp (do G ⟶ body od) (λs. 1) ⊨!!! wp (do G ⟶ body od) (λs. «N G¬ s * I s)"
    (is "I && ?T ⊨!!! wp ?loop ?X")
proof -
  txt ‹We first appeal to the \emph{liberal} loop rule:›
  from assms have "I && ?T ⊨!!! wlp ?loop ?X && ?T"
    by(blast intro:exp_conj_mono_left wlp_Loop)

  txt ‹Next, by sub-conjunctivity:›
  also {
    from wd have sdp_loop: "sub_distrib_pconj (do G ⟶ body od)"
      by(blast intro:sdp_intros)

    from wd unit have "wlp ?loop ?X && ?T ⊨!!! wp ?loop (?X && (λs. 1))"
      by(blast intro:sub_distrib_pconjD sdp_intros unitary_intros)
  }

  txt ‹Finally, the conjunction collapses:›
  finally show ?thesis
    by(simp add:exp_conj_1_right sound_intros sound_nneg unit unitary_sound)
qed

subsection ‹Unfolding›

lemma wp_loop_unfold:
  fixes body :: "'s prog"
  assumes sP: "sound P"
      and h: "healthy (wp body)"
  shows "wp (do G ⟶ body od) P =
   (λs. «N G¬ s * P s + «G¬ s * wp body (wp (do G ⟶ body od) P) s)"
proof (simp only: wp_eval)
  let "?X t" = "wp (body ;; Embed t _{<guillemotleft> G ¬}⊕ Skip)"
  have "equiv_trans (lfp_trans ?X)
    (wp (body ;; Embed (lfp_trans ?X) _{<guillemotleft> G ¬}⊕ Skip))"
  proof(intro lfp_trans_unfold)
    fix t::"'s trans" and P::"'s expect"
    assume st: "∧Q. sound Q ==> sound (t Q)"
       and sP: "sound P"
    with h show "sound (?X t P)"
      by(rule wp_loop_step_sound)
  next
    fix t u::"'s trans"
    assume "le_trans t u" "(∧P. sound P ==> sound (t P))"
           "(∧P. sound P ==> sound (u P))"
    with h show "le_trans (wp (body ;; Embed t _{<guillemotleft> G ¬}⊕ Skip))
                          (wp (body ;; Embed u _{<guillemotleft> G ¬}⊕ Skip))"
      by(iprover intro:wp_loop_step_mono)
  next
    let ?v = "λP s. bound_of P"
    from h show "le_trans (wp (body ;; Embed ?v _{<guillemotleft> G ¬}⊕ Skip)) ?v"
      by(intro le_transI, simp add:wp_eval lfp_loop_fp[unfolded negate_embed])
    fix P::"'s expect"
    assume "sound P" thus "sound (?v P)" by(auto)
  qed
  also have "equiv_trans ...
    (λP s. «N G¬ s * P s + «G¬ s * wp body (wp (Embed (lfp_trans ?X)) P) s)"
    by(rule equiv_transI, simp add:wp_eval algebra_simps negate_embed)
  finally show "lfp_trans ?X P =
    (λs. «N G¬ s * P s + «G¬ s * wp body (lfp_trans ?X P) s)"
    using sP unfolding wp_eval by(blast)
qed

lemma wp_loop_nguard:
  "[ healthy (wp body); sound P; ¬ G s ] ==> wp do G ⟶ body od P s = P s"
  by(subst wp_loop_unfold, simp_all)

lemma wp_loop_guard:
  "[ healthy (wp body); sound P; G s ] ==>
   wp do G ⟶ body od P s = wp (body ;; do G ⟶ body od) P s"
  by(subst wp_loop_unfold, simp_all add:wp_eval)

end