Theory OptionMonadWP

(*
 * Copyright 2014, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

(*
Hoare reasoning and WP (weakest-precondition) generator rules for the option monad.

This list is almost certainly incomplete; add rules here as they are needed.
*)

theory OptionMonadWP
imports
  OptionMonadND
  "wp/WP"
begin

declare K_def [simp]

(* Hoare triples.
   TODO: design a sensible syntax for them. *)

(* Partial correctness. *)
definition ovalid :: "('s ⇒ bool) ⇒ ('s ⇒ 'a option) ⇒ ('a ⇒ 's ⇒ bool) ⇒ bool" where
  "ovalid P f Q ≡ ∀s r. P s ∧ f s = Some r ⟶ Q r s"
(* Total correctness. *)
definition ovalidNF :: "('s ⇒ bool) ⇒ ('s ⇒ 'a option) ⇒ ('a ⇒ 's ⇒ bool) ⇒ bool" where
  "ovalidNF P f Q ≡ ∀s. P s ⟶ (f s ≠ None ∧ (∀r. f s = Some r ⟶ Q r s))"
(* Termination. *)
definition no_ofail where "no_ofail P f ≡ ∀s. P s ⟶ f s ≠ None"

(*
This rule lets us apply ovalidNF machinery for proving no_ofail.
However, we ought to eventually write working wp rules for no_ofail (see below).
*)
lemma no_ofail_is_ovalidNF: "no_ofail P f ≡ ovalidNF P f (λ_ _. True)"
  by (simp add: no_ofail_def ovalidNF_def)
lemma ovalidNF_combine: "⟦ ovalid P f Q; no_ofail P f ⟧ ⟹ ovalidNF P f Q"
  by (auto simp: ovalidNF_def ovalid_def no_ofail_def)


(* Annotating programs with loop invariant and measure. *)
definition owhile_inv ::
  "('a ⇒ 's ⇒ bool) ⇒ ('a ⇒ 's ⇒ 'a option) ⇒ 'a
   ⇒ ('a ⇒ 's ⇒ bool) ⇒ ('a ⇒ 's ⇒ nat) ⇒ 's ⇒ 'a option"
  where "owhile_inv C B x I M = owhile C B x"  

lemmas owhile_add_inv = owhile_inv_def[symmetric]


(* WP rules for ovalid. *)
lemma obind_wp [wp]:
  "⟦ ⋀r. ovalid (R r) (g r) Q; ovalid P f R ⟧ ⟹ ovalid P (obind f g) Q"
  by (simp add: ovalid_def obind_def split: option.splits, fast)

lemma oreturn_wp [wp]:
  "ovalid (P x) (oreturn x) P"
  by (simp add: ovalid_def oreturn_def K_def)

lemma ocondition_wp [wp]:
  "⟦ ovalid L l Q; ovalid R r Q ⟧
   ⟹ ovalid (λs. if C s then L s else R s) (ocondition C l r) Q"
  by (auto simp: ovalid_def ocondition_def)

lemma ofail_wp [wp]:
  "ovalid (λ_. True) ofail Q"
  by (simp add: ovalid_def ofail_def)

lemma ovalid_K_bind_wp [wp]:
  "ovalid P f Q ⟹ ovalid P (K_bind f x) Q"
  by simp

lemma ogets_wp [wp]: "ovalid (λs. P (f s) s) (ogets f) P"
  by (simp add: ovalid_def ogets_def)

lemma oguard_wp [wp]: "ovalid (λs. f s ⟶ P () s) (oguard f) P"
  by (simp add: ovalid_def oguard_def)

lemma oskip_wp [wp]:
  "ovalid (λs. P () s) oskip P"
  by (simp add: ovalid_def oskip_def)

lemma ovalid_case_prod [wp]:
  assumes "(⋀x y. ovalid (P x y) (B x y) Q)"
  shows "ovalid (case v of (x, y) ⇒ P x y) (case v of (x, y) ⇒ B x y) Q"
  using assms unfolding ovalid_def by auto

lemma owhile_ovalid [wp]:
"⟦⋀a. ovalid (λs. I a s ∧ C a s) (B a) I;
   ⋀a s. ⟦I a s; ¬ C a s⟧ ⟹ Q a s⟧
  ⟹ ovalid (I a) (owhile_inv C B a I M) Q"
  unfolding owhile_inv_def owhile_def ovalid_def
  apply clarify
  apply (frule_tac I = "λa. I a s" in option_while_rule)
  apply auto
  done

definition ovalid_property where "ovalid_property P x = (λs f. (∀r. Some r = x s f ⟶ P r s))"
lemma ovalid_is_triple [wp_trip]:
  "ovalid P f Q = triple_judgement P f (ovalid_property Q (λs f. f s))"
  by (auto simp: triple_judgement_def ovalid_def ovalid_property_def)


lemma ovalid_wp_comb1 [wp_comb]:
  "⟦ ovalid P' f Q; ovalid P f Q'; ⋀s. P s ⟹ P' s ⟧ ⟹ ovalid P f (λr s. Q r s ∧ Q' r s)"
  by (simp add: ovalid_def)

lemma ovalid_wp_comb2 [wp_comb]:
  "⟦ ovalid P f Q; ⋀s. P' s ⟹ P s ⟧ ⟹ ovalid P' f Q"
  by (auto simp: ovalid_def)

lemma ovalid_wp_comb3 [wp_comb]:
  "⟦ ovalid P f Q; ovalid P' f Q' ⟧ ⟹ ovalid (λs. P s ∧ P' s) f (λr s. Q r s ∧ Q' r s)"
  by (auto simp: ovalid_def)



(* WP rules for ovalidNF. *)
lemma obind_NF_wp [wp]:
  "⟦ ⋀r. ovalidNF (R r) (g r) Q; ovalidNF P f R ⟧ ⟹ ovalidNF P (obind f g) Q"
  by (auto simp: ovalidNF_def obind_def split: option.splits)

lemma oreturn_NF_wp [wp]:
  "ovalidNF (P x) (oreturn x) P"
  by (simp add: ovalidNF_def oreturn_def)

lemma ocondition_NF_wp [wp]:
  "⟦ ovalidNF L l Q; ovalidNF R r Q ⟧
   ⟹ ovalidNF (λs. if C s then L s else R s) (ocondition C l r) Q"
  by (simp add: ovalidNF_def ocondition_def)

lemma ofail_NF_wp [wp]:
  "ovalidNF (λ_. False) ofail Q"
  by (simp add: ovalidNF_def ofail_def)

lemma ovalidNF_K_bind_wp [wp]:
  "ovalidNF P f Q ⟹ ovalidNF P (K_bind f x) Q"
  by simp

lemma ogets_NF_wp [wp]:
  "ovalidNF (λs. P (f s) s) (ogets f) P"
  by (simp add: ovalidNF_def ogets_def)

lemma oguard_NF_wp [wp]:
  "ovalidNF (λs. f s ∧ P () s) (oguard f) P"
  by (simp add: ovalidNF_def oguard_def)

lemma oskip_NF_wp [wp]:
  "ovalidNF (λs. P () s) oskip P"
  by (simp add: ovalidNF_def oskip_def)

lemma ovalid_NF_case_prod [wp]:
  assumes "(⋀x y. ovalidNF (P x y) (B x y) Q)"
  shows "ovalidNF (case v of (x, y) ⇒ P x y) (case v of (x, y) ⇒ B x y) Q"
  using assms unfolding ovalidNF_def by auto

lemma owhile_NF [wp]:
"⟦⋀a. ovalidNF (λs. I a s ∧ C a s) (B a) I;
   ⋀a m. ovalid (λs. I a s ∧ C a s ∧ M a s = m) (B a) (λr s. M r s < m);
   ⋀a s. ⟦I a s; ¬ C a s⟧ ⟹ Q a s⟧
  ⟹ ovalidNF (I a) (owhile_inv C B a I M) Q"
  unfolding owhile_inv_def ovalidNF_def ovalid_def
  apply clarify
  apply (rename_tac s, rule_tac I = I and M = "measure (λr. M r s)" in owhile_rule)
       apply fastforce
      apply fastforce
     apply fastforce
    apply blast+
  done

definition ovalidNF_property where "ovalidNF_property P x = (λs f. (x s f ≠ None ∧ (∀r. Some r = x s f ⟶ P r s)))"
lemma ovalidNF_is_triple [wp_trip]:
  "ovalidNF P f Q = triple_judgement P f (ovalidNF_property Q (λs f. f s))"
  by (auto simp: triple_judgement_def ovalidNF_def ovalidNF_property_def)


lemma ovalidNF_wp_comb1 [wp_comb]:
  "⟦ ovalidNF P' f Q; ovalidNF P f Q'; ⋀s. P s ⟹ P' s ⟧ ⟹ ovalidNF P f (λr s. Q r s ∧ Q' r s)"
  by (simp add: ovalidNF_def)

lemma ovalidNF_wp_comb2 [wp_comb]:
  "⟦ ovalidNF P f Q; ⋀s. P' s ⟹ P s ⟧ ⟹ ovalidNF P' f Q"
  by (simp add: ovalidNF_def)

lemma ovalidNF_wp_comb3 [wp_comb]:
  "⟦ ovalidNF P f Q; ovalidNF P' f Q' ⟧ ⟹ ovalidNF (λs. P s ∧ P' s) f (λr s. Q r s ∧ Q' r s)"
  by (simp add: ovalidNF_def)



(* FIXME: WP rules for no_ofail, which might not be correct. *)
lemma no_ofail_ofail [wp]: "no_ofail (λ_. False) ofail"
  by (simp add: no_ofail_def ofail_def)

lemma no_ofail_ogets [wp]: "no_ofail (λ_. True) (ogets f)"
  by (simp add: no_ofail_def ogets_def)

lemma no_ofail_obind [wp]:
  "⟦ ⋀r. no_ofail (P r) (g r); no_ofail Q f; ovalid Q f P ⟧ ⟹ no_ofail Q (obind f g)"
  by (auto simp: no_ofail_def obind_def ovalid_def)

lemma no_ofail_K_bind [wp]:
  "no_ofail P f ⟹ no_ofail P (K_bind f x)"
  by simp

lemma no_ofail_oguard [wp]:
  "no_ofail (λs. f s) (oguard f)"
  by (auto simp: no_ofail_def oguard_def)

lemma no_ofail_ocondition [wp]:
  "⟦ no_ofail L l; no_ofail R r ⟧
     ⟹ no_ofail (λs. if C s then L s else R s) (ocondition C l r)"
  by (simp add: no_ofail_def ocondition_def)

lemma no_ofail_oreturn [wp]:
  "no_ofail (λ_. True) (oreturn x)"
  by (simp add: no_ofail_def oreturn_def)

lemma no_ofail_oskip [wp]:
  "no_ofail (λ_. True) oskip"
  by (simp add: no_ofail_def oskip_def)

lemma no_ofail_is_triple [wp_trip]:
  "no_ofail P f = triple_judgement P f (λs f. f s ≠ None)"
  by (auto simp: triple_judgement_def no_ofail_def)

lemma no_ofail_wp_comb1 [wp_comb]:
  "⟦ no_ofail P f; ⋀s. P' s ⟹ P s ⟧ ⟹ no_ofail P' f"
  by (simp add: no_ofail_def)

lemma no_ofail_wp_comb2 [wp_comb]:
  "⟦ no_ofail P f; no_ofail P' f ⟧ ⟹ no_ofail (λs. P s ∧ P' s) f"
  by (simp add: no_ofail_def)



(* Some extra lemmas for our predicates. *)
lemma ovalid_grab_asm:
  "(G ⟹ ovalid P f Q) ⟹ ovalid (λs. G ∧ P s) f Q"
  by (simp add: ovalid_def)
lemma ovalidNF_grab_asm:
  "(G ⟹ ovalidNF P f Q) ⟹ ovalidNF (λs. G ∧ P s) f Q"
  by (simp add: ovalidNF_def)
lemma no_ofail_grab_asm:
  "(G ⟹ no_ofail P f) ⟹ no_ofail (λs. G ∧ P s) f"
  by (simp add: no_ofail_def)

lemma ovalid_assume_pre:
  "(⋀s. P s ⟹ ovalid P f Q) ⟹ ovalid P f Q"
  by (auto simp: ovalid_def)
lemma ovalidNF_assume_pre:
  "(⋀s. P s ⟹ ovalidNF P f Q) ⟹ ovalidNF P f Q"
  by (simp add: ovalidNF_def)
lemma no_ofail_assume_pre:
  "(⋀s. P s ⟹ no_ofail P f) ⟹ no_ofail P f"
  by (simp add: no_ofail_def)

lemma ovalid_pre_imp:
  "⟦ ⋀s. P' s ⟹ P s; ovalid P f Q ⟧ ⟹ ovalid P' f Q"
  by (simp add: ovalid_def)
lemma ovalidNF_pre_imp:
  "⟦ ⋀s. P' s ⟹ P s; ovalidNF P f Q ⟧ ⟹ ovalidNF P' f Q"
  by (simp add: ovalidNF_def)
lemma no_ofail_pre_imp:
  "⟦ ⋀s. P' s ⟹ P s; no_ofail P f ⟧ ⟹ no_ofail P' f"
  by (simp add: no_ofail_def)

lemma ovalid_post_imp:
  "⟦ ⋀r s. Q r s ⟹ Q' r s; ovalid P f Q ⟧ ⟹ ovalid P f Q'"
  by (simp add: ovalid_def)
lemma ovalidNF_post_imp:
  "⟦ ⋀r s. Q r s ⟹ Q' r s; ovalidNF P f Q ⟧ ⟹ ovalidNF P f Q'"
  by (simp add: ovalidNF_def)

lemma ovalid_post_imp_assuming_pre:
  "⟦ ⋀r s. ⟦ P s; Q r s ⟧ ⟹ Q' r s; ovalid P f Q ⟧ ⟹ ovalid P f Q'"
  by (simp add: ovalid_def)
lemma ovalidNF_post_imp_assuming_pre:
  "⟦ ⋀r s. ⟦ P s; Q r s ⟧ ⟹ Q' r s; ovalidNF P f Q ⟧ ⟹ ovalidNF P f Q'"
  by (simp add: ovalidNF_def)

end