Theory StructuredReasoning

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

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

section "Structured Reasoning"

theory StructuredReasoning imports Algebra begin

text ‹By linking the algebraic, the syntactic, and the semantic views
  of computation, we derive a set of rules for decomposing expectation
  entailment proofs, firstly over the syntactic structure of a program,
  and secondly over the refinement relation.  These rules also form the
  basis for automated reasoning.›

subsection ‹Syntactic Decomposition›

lemma wp_Abort:
  "(λs. 0) ⊩ wp Abort Q"
  unfolding wp_eval by(simp)

lemma wlp_Abort:
  "(λs. 1) ⊩ wlp Abort Q"
  unfolding wp_eval by(simp)

lemma wp_Skip:
  "P ⊩ wp Skip P"
  unfolding wp_eval by(blast)

lemma wlp_Skip:
  "P ⊩ wlp Skip P"
  unfolding wp_eval by(blast)

lemma wp_Apply:
  "Q o f ⊩ wp (Apply f) Q"
  unfolding wp_eval by(simp)

lemma wlp_Apply:
  "Q o f ⊩ wlp (Apply f) Q"
  unfolding wp_eval by(simp)

lemma wp_Seq:
  assumes ent_a: "P ⊩ wp a Q"
      and ent_b: "Q ⊩ wp b R"
      and wa:   "well_def a"
      and wb:   "well_def b"
      and s_Q:   "sound Q"
      and s_R:   "sound R"
  shows "P ⊩ wp (a ;; b) R"
proof -
  note ha = well_def_wp_healthy[OF wa]
  note hb = well_def_wp_healthy[OF wb]
  note ent_a
  also from ent_b ha hb s_Q s_R have "wp a Q ⊩ wp a (wp b R)"
    by(blast intro:healthy_monoD2)
  finally show ?thesis by(simp add:wp_eval)
qed

lemma wlp_Seq:
  assumes ent_a: "P ⊩ wlp a Q"
      and ent_b: "Q ⊩ wlp b R"
      and wa:   "well_def a"
      and wb:   "well_def b"
      and u_Q:   "unitary Q"
      and u_R:   "unitary R"
  shows "P ⊩ wlp (a ;; b) R"
proof -
  note ha = well_def_wlp_nearly_healthy[OF wa]
  note hb = well_def_wlp_nearly_healthy[OF wb]
  note ent_a
  also from ent_b ha hb u_Q u_R have "wlp a Q ⊩ wlp a (wlp b R)"
    by(blast intro:nearly_healthy_monoD[OF ha])
  finally show ?thesis by(simp add:wp_eval)
qed

lemma wp_PC:
  "(λs. P s * wp a Q s + (1 - P s) * wp b Q s) ⊩ wp (a ⇘P⇙⊕ b) Q"
  by(simp add:wp_eval)

lemma wlp_PC:
  "(λs. P s * wlp a Q s + (1 - P s) * wlp b Q s) ⊩ wlp (a ⇘P⇙⊕ b) Q"
  by(simp add:wp_eval)

text ‹A simpler rule for when the probability does not depend on the state.›
lemma PC_fixed:
  assumes wpa: "P ⊩ a ab R"
      and wpb: "Q ⊩ b ab R"
      and np: "0 ≤ p" and bp: "p ≤ 1"
  shows "(λs. p * P s + (1 - p) * Q s) ⊩ (a ⇘(λs. p)⇙⊕ b) ab R"
  unfolding PC_def
proof(rule le_funI)
  fix s
  from wpa and np have "p * P s ≤ p * a ab R s"
    by(auto intro:mult_left_mono)
  moreover {
    from bp have "0 ≤ 1 - p" by(simp)
    with wpb have "(1 - p) * Q s ≤ (1 - p) * b ab R s"
      by(auto intro:mult_left_mono)
  }
  ultimately show "p * P s + (1 - p) * Q s ≤
                   p * a ab R s + (1 - p) * b ab R s"
    by(rule add_mono)
qed

lemma wp_PC_fixed:
  "⟦ P ⊩ wp a R; Q ⊩ wp b R; 0 ≤ p; p ≤ 1 ⟧ ⟹
  (λs. p * P s + (1 - p) * Q s) ⊩ wp (a ⇘(λs. p)⇙⊕ b) R"
  by(simp add:wp_def PC_fixed)

lemma wlp_PC_fixed:
  "⟦ P ⊩ wlp a R; Q ⊩ wlp b R; 0 ≤ p; p ≤ 1 ⟧ ⟹
  (λs. p * P s + (1 - p) * Q s) ⊩ wlp (a ⇘(λs. p)⇙⊕ b) R"
  by(simp add:wlp_def PC_fixed)

lemma wp_DC:
  "(λs. min (wp a Q s) (wp b Q s)) ⊩ wp (a ⨅ b) Q"
  unfolding wp_eval by(simp)

lemma wlp_DC:
  "(λs. min (wlp a Q s) (wlp b Q s)) ⊩ wlp (a ⨅ b) Q"
  unfolding wp_eval by(simp)

text ‹Combining annotations for both branches:›
lemma DC_split:
  fixes a::"'s prog" and b
  assumes wpa: "P ⊩ a ab R"
      and wpb: "Q ⊩ b ab R"
  shows "(λs. min (P s) (Q s)) ⊩ (a ⨅ b) ab R"
  unfolding DC_def
proof(rule le_funI)
  fix s
  from wpa wpb
  have "P s ≤ a ab R s" and "Q s ≤ b ab R s" by(auto)
  thus "min (P s) (Q s) ≤ min (a ab R s) (b ab R s)" by(auto)
qed

lemma wp_DC_split:
  "⟦ P ⊩ wp prog R; Q ⊩ wp prog' R ⟧ ⟹
  (λs. min (P s) (Q s)) ⊩ wp (prog ⨅ prog') R"
  by(simp add:wp_def DC_split)

lemma wlp_DC_split:
  "⟦ P ⊩ wlp prog R; Q ⊩ wlp prog' R ⟧ ⟹
  (λs. min (P s) (Q s)) ⊩ wlp (prog ⨅ prog') R"
  by(simp add:wlp_def DC_split)

lemma wp_DC_split_same:
  "⟦ P ⊩ wp prog Q; P ⊩ wp prog' Q ⟧ ⟹ P ⊩ wp (prog ⨅ prog') Q"
  unfolding wp_eval by(blast intro:min.boundedI)

lemma wlp_DC_split_same:
  "⟦ P ⊩ wlp prog Q; P ⊩ wlp prog' Q ⟧ ⟹ P ⊩ wlp (prog ⨅ prog') Q"
  unfolding wp_eval by(blast intro:min.boundedI)

lemma SetPC_split:
  fixes f::"'x ⇒ 'y prog"
    and p::"'y ⇒ 'x ⇒ real"
  assumes rec: "⋀x s. x ∈ supp (p s) ⟹ P x ⊩ f x ab Q"
      and nnp: "⋀s. nneg (p s)"
  shows "(λs. ∑x ∈ supp (p s). p s x * P x s) ⊩ SetPC f p ab Q"
  unfolding SetPC_def
proof(rule le_funI)
  fix s
  from rec have "⋀x. x ∈ supp (p s) ⟹ P x s ≤ f x ab Q s" by(blast)
  moreover from nnp have "⋀x. 0 ≤ p s x" by(blast)
  ultimately have "⋀x. x ∈ supp (p s) ⟹ p s x * P x s ≤ p s x * f x ab Q s"
    by(blast intro:mult_left_mono)
  thus "(∑x ∈ supp (p s). p s x * P x s) ≤ (∑x ∈ supp (p s). p s x * f x ab Q s)"
    by(rule sum_mono)
qed

lemma wp_SetPC_split:
  "⟦ ⋀x s. x ∈ supp (p s) ⟹ P x ⊩ wp (f x) Q; ⋀s. nneg (p s) ⟧ ⟹
   (λs. ∑x ∈ supp (p s). p s x * P x s) ⊩ wp (SetPC f p) Q"
  by(simp add:wp_def SetPC_split)

lemma wlp_SetPC_split:
  "⟦ ⋀x s. x ∈ supp (p s) ⟹ P x ⊩ wlp (f x) Q; ⋀s. nneg (p s) ⟧ ⟹
   (λs. ∑x ∈ supp (p s). p s x * P x s) ⊩ wlp (SetPC f p) Q"
  by(simp add:wlp_def SetPC_split)

lemma wp_SetDC_split:
  "⟦ ⋀s x. x ∈ S s ⟹ P ⊩ wp (f x) Q; ⋀s. S s ≠ {} ⟧ ⟹
   P ⊩ wp (SetDC f S) Q"
  by(rule le_funI, unfold wp_eval, blast intro!:cInf_greatest)

lemma wlp_SetDC_split:
  "⟦ ⋀s x. x ∈ S s ⟹ P ⊩ wlp (f x) Q; ⋀s. S s ≠ {} ⟧ ⟹
   P ⊩ wlp (SetDC f S) Q"
  by(rule le_funI, unfold wp_eval, blast intro!:cInf_greatest)

lemma wp_SetDC:
  assumes wp: "⋀s x. x ∈ S s ⟹ P x ⊩ wp (f x) Q"
      and ne: "⋀s. S s ≠ {}"
      and sP: "⋀x. sound (P x)"
  shows "(λs. Inf ((λx. P x s) ` S s)) ⊩ wp (SetDC f S) Q"
  using assms by(intro le_funI, simp add:wp_eval, blast intro!:cInf_mono)

lemma wlp_SetDC:
  assumes wp: "⋀s x. x ∈ S s ⟹ P x ⊩ wlp (f x) Q"
      and ne: "⋀s. S s ≠ {}"
      and sP: "⋀x. sound (P x)"
  shows "(λs. Inf ((λx. P x s) ` S s)) ⊩ wlp (SetDC f S) Q"
  using assms by(intro le_funI, simp add:wp_eval, blast intro!:cInf_mono)

lemma wp_Embed:
  "P ⊩ t Q ⟹ P ⊩ wp (Embed t) Q"
  by(simp add:wp_def Embed_def)

lemma wlp_Embed:
  "P ⊩ t Q ⟹ P ⊩ wlp (Embed t) Q"
  by(simp add:wlp_def Embed_def)

lemma wp_Bind:
  "⟦ ⋀s. P s ≤ wp (a (f s)) Q s ⟧ ⟹ P ⊩ wp (Bind f a) Q"
  by(auto simp:wp_def Bind_def)

lemma wlp_Bind:
  "⟦ ⋀s. P s ≤ wlp (a (f s)) Q s ⟧ ⟹ P ⊩ wlp (Bind f a) Q"
  by(auto simp:wlp_def Bind_def)

lemma wp_repeat:
  "⟦ P ⊩ wp a Q; Q ⊩ wp (repeat n a) R;
     well_def a; sound Q; sound R ⟧ ⟹ P ⊩ wp (repeat (Suc n) a) R"
  by(auto intro!:wp_Seq wd_intros)

lemma wlp_repeat:
  "⟦ P ⊩ wlp a Q; Q ⊩ wlp (repeat n a) R;
     well_def a; unitary Q; unitary R ⟧ ⟹ P ⊩ wlp (repeat (Suc n) a) R"
  by(auto intro!:wlp_Seq wd_intros)

text ‹Note that the loop rules presented in section \autoref{s:loop_rules} are of the same form,
and would belong here, had they not already been stated.›

text ‹The following rules are specialisations of those for general
  transformers, and are easier for the unifier to match.›
lemmas wp_strengthen_post=
  entails_strengthen_post[where t="wp a" for a]

lemma wlp_strengthen_post:
  "P ⊩ wlp a Q ⟹ nearly_healthy (wlp a) ⟹ unitary R ⟹ Q ⊩ R ⟹ unitary Q ⟹
   P ⊩ wlp a R"
  by(blast intro:entails_trans)

lemmas wp_weaken_pre=
  entails_weaken_pre[where t="wp a" for a]
lemmas wlp_weaken_pre=
  entails_weaken_pre[where t="wlp a" for a]

lemmas wp_scale=
  entails_scale[where t="wp a" for a, OF _ well_def_wp_healthy]

subsection ‹Algebraic Decomposition›

text ‹Refinement is a powerful tool for decomposition, belied by the simplicity of the rule.
This is an \emph{axiomatic} formulation of refinement (all annotations of the @{term a}
are annotations of @{term b}), rather than an operational version (all traces of @{term b} are
traces of @{term a}.›

lemma wp_refines:
  "⟦ a ⊑ b; P ⊩ wp a Q; sound Q ⟧ ⟹ P ⊩ wp b Q"
  by(auto intro:entails_trans)

lemmas wp_drefines = drefinesD

subsection ‹Hoare triples›

text ‹The Hoare triple, or validity predicate, is logically equivalent to the weakest-precondition
entailment form. The benefit is that it allows us to define transitivity rules for computational
(also/finally) reasoning.›

definition
  wp_valid :: "('a ⇒ real) ⇒ 'a prog ⇒ ('a ⇒ real) ⇒ bool" ("⦃_⦄ _ ⦃_⦄p")
where
  "wp_valid P prog Q ≡ P ⊩ wp prog Q"

lemma wp_validI:
  "P ⊩ wp prog Q ⟹ ⦃P⦄ prog ⦃Q⦄p"
  unfolding wp_valid_def by(assumption)

lemma wp_validD:
  "⦃P⦄ prog ⦃Q⦄p ⟹ P ⊩ wp prog Q"
  unfolding wp_valid_def by(assumption)

lemma valid_Seq:
  "⟦ ⦃P⦄ a ⦃Q⦄p; ⦃Q⦄ b ⦃R⦄p; well_def a; well_def b; sound Q; sound R ⟧ ⟹
  ⦃P⦄ a ;; b ⦃R⦄p"
  unfolding wp_valid_def by(rule wp_Seq)

text ‹We make it available to the computational reasoner:›
declare valid_Seq[trans]

end