Theory Determinism

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

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

section ‹Determinism›

theory Determinism imports WellDefined begin

text_raw ‹\label{s:prog_determ}›

text ‹We provide a set of lemmas for establishing that
  appropriately restricted programs are fully additive, and
  maximal in the refinement order.  This is particularly useful
  with data refinement, as it implies correspondence.›

subsection  ‹Additivity›

lemma additive_wp_Abort:
  "additive (wp (Abort))"
  by(auto simp:wp_eval)

text ‹@{term "wlp Abort"} is not additive.›

lemma additive_wp_Skip:
  "additive (wp (Skip))"
  by(auto simp:wp_eval)

lemma additive_wp_Apply:
  "additive (wp (Apply f))"
  by(auto simp:wp_eval)

lemma additive_wp_Seq:
  fixes a::"'s prog"
  assumes adda: "additive (wp a)"
      and addb: "additive (wp b)"
      and wb:   "well_def b"
  shows "additive (wp (a ;; b))"
proof(rule additiveI, unfold wp_eval o_def)
  fix P::"'s ⇒ real" and Q::"'s ⇒ real" and s::'s
  assume sP: "sound P" and sQ: "sound Q"

  note hb = well_def_wp_healthy[OF wb]

  from addb sP sQ
  have "wp b (λs. P s + Q s) = (λs. wp b P s + wp b Q s)"
    by(blast dest:additiveD)
  with adda sP sQ hb
  show "wp a (wp b (λs. P s + Q s)) s =
        wp a (wp b P) s + (wp a (wp b Q)) s"
    by(auto intro:fun_cong[OF additiveD])
qed

lemma additive_wp_PC:
  "⟦ additive (wp a); additive (wp b) ⟧ ⟹ additive (wp (a ⇘P⇙⊕ b))"
  by(rule additiveI, simp add:additiveD field_simps wp_eval)

text ‹@{term DC} is not additive.›

lemma additive_wp_SetPC:
  "⟦ ⋀x s. x ∈ supp (p s) ⟹ additive (wp (a x)); ⋀s. finite (supp (p s)) ⟧ ⟹
   additive (wp (SetPC a p))"
  by(rule additiveI,
     simp add:wp_eval additiveD distrib_left sum.distrib)

lemma additive_wp_Bind:
  "⟦ ⋀x. additive (wp (a (f x))) ⟧ ⟹ additive (wp (Bind f a))"
  by(simp add:wp_eval additive_def)

lemma additive_wp_Embed:
  "⟦ additive t ⟧ ⟹ additive (wp (Embed t))"
  by(simp add:wp_eval)

lemma additive_wp_repeat:
  "additive (wp a) ⟹ well_def a ⟹ additive (wp (repeat n a))"
  by(induct n, auto simp:additive_wp_Skip intro:additive_wp_Seq wd_intros)

lemmas fa_intros =
  additive_wp_Abort additive_wp_Skip
  additive_wp_Apply additive_wp_Seq
  additive_wp_PC    additive_wp_SetPC
  additive_wp_Bind  additive_wp_Embed
  additive_wp_repeat

subsection ‹Maximality›

lemma max_wp_Skip:
  "maximal (wp Skip)"
  by(simp add:maximal_def wp_eval)

lemma max_wp_Apply:
  "maximal (wp (Apply f))"
  by(auto simp:wp_eval o_def)

lemma max_wp_Seq:
  "⟦ maximal (wp a); maximal (wp b) ⟧ ⟹ maximal (wp (a ;; b))"
  by(simp add:wp_eval maximal_def)

lemma max_wp_PC:
  "⟦ maximal (wp a); maximal (wp b) ⟧ ⟹ maximal (wp (a ⇘P⇙⊕ b))"
  by(rule maximalI, simp add:maximalD field_simps wp_eval)

lemma max_wp_DC:
  "⟦ maximal (wp a); maximal (wp b) ⟧ ⟹ maximal (wp (a ⨅ b))"
  by(rule maximalI, simp add:wp_eval maximalD)

lemma max_wp_SetPC:
  "⟦ ⋀s a. a ∈ supp (P s) ⟹ maximal (wp (p a)); ⋀s. (∑a∈supp (P s). P s a) = 1 ⟧ ⟹
  maximal (wp (SetPC p P))"
  by(auto simp:maximalD wp_def SetPC_def sum_distrib_right[symmetric])

lemma max_wp_SetDC:
  fixes p::"'a ⇒ 's prog"
  assumes mp: "⋀s a. a ∈ S s ⟹ maximal (wp (p a))"
      and ne: "⋀s. S s ≠ {}"
  shows "maximal (wp (SetDC p S))"
proof(rule maximalI, rule ext, unfold wp_eval)
  fix c::real and s::'s
  assume "0 ≤ c"
  hence "Inf ((λa. wp (p a) (λ_. c) s) ` S s) = Inf ((λ_. c) ` S s)"
    using mp by(simp add:maximalD cong:image_cong)
  also {
    from ne obtain a where "a ∈ S s" by blast
    hence "Inf ((λ_. c) ` S s) = c"
      by (auto simp add: image_constant_conv cong del: INF_cong_simp)
  }
  finally show "Inf ((λa. wp (p a) (λ_. c) s) ` S s) = c" .
qed
 
lemma max_wp_Embed:
  "maximal t ⟹ maximal (wp (Embed t))"
  by(simp add:wp_eval)

lemma max_wp_repeat:
  "maximal (wp a) ⟹ maximal (wp (repeat n a))"
  by(induct n, simp_all add:max_wp_Skip max_wp_Seq)

lemma max_wp_Bind:
  assumes ma: "⋀s. maximal (wp (a (f s)))"
  shows "maximal (wp (Bind f a))"
proof(rule maximalI, rule ext, simp add:wp_eval)
  fix c::real and s
  assume "0 ≤ c"
  with ma have "wp (a (f s)) (λ_. c) = (λ_. c)" by(blast)
  thus "wp (a (f s)) (λ_. c) s = c" by(auto)
qed

lemmas max_intros =
  max_wp_Skip  max_wp_Apply
  max_wp_Seq   max_wp_PC
  max_wp_DC    max_wp_SetPC
  max_wp_SetDC max_wp_Embed
  max_wp_Bind  max_wp_repeat

text ‹A healthy transformer that terminates is maximal.›
lemma healthy_term_max:
  assumes ht: "healthy t"
      and trm: "λs. 1 ⊩ t (λs. 1)"
  shows "maximal t"
proof(intro maximalI ext)
  fix c::real and s
  assume nnc: "0 ≤ c"

  have "t (λs. c) s = t (λs. 1 * c) s" by(simp)
  also from nnc healthy_scalingD[OF ht]
  have "... = c * t (λs. 1) s" by(simp add:scalingD)
  also {
    from ht have "t (λs. 1) ⊩ λs. 1" by(auto)
    with trm have "t (λs. 1) = (λs. 1)" by(auto)
    hence "c * t (λs. 1) s = c" by(simp)
  }
  finally show "t (λs. c) s = c" .
qed

subsection ‹Determinism›

lemma det_wp_Skip:
  "determ (wp Skip)"
  using max_intros fa_intros by(blast)

lemma det_wp_Apply:
  "determ (wp (Apply f))"
  by(intro determI fa_intros max_intros)

lemma det_wp_Seq:
  "determ (wp a) ⟹ determ (wp b) ⟹ well_def b ⟹ determ (wp (a ;; b))"
  by(intro determI fa_intros max_intros, auto)

lemma det_wp_PC:
  "determ (wp a) ⟹ determ (wp b) ⟹ determ (wp (a ⇘P⇙⊕ b))"
  by(intro determI fa_intros max_intros, auto)

lemma det_wp_SetPC:
  "(⋀x s. x ∈ supp (p s) ⟹ determ (wp (a x))) ⟹
   (⋀s. finite (supp (p s))) ⟹
   (⋀s. sum (p s) (supp (p s)) = 1) ⟹
   determ (wp (SetPC a p))"
  by(intro determI fa_intros max_intros, auto)

lemma det_wp_Bind:
  "(⋀x. determ (wp (a (f x)))) ⟹ determ (wp (Bind f a))"
  by(intro determI fa_intros max_intros, auto)

lemma det_wp_Embed:
  "determ t ⟹ determ (wp (Embed t))"
  by(simp add:wp_eval)

lemma det_wp_repeat:
  "determ (wp a) ⟹ well_def a ⟹ determ (wp (repeat n a))"
  by(intro determI fa_intros max_intros, auto)

lemmas determ_intros =
  det_wp_Skip det_wp_Apply
  det_wp_Seq  det_wp_PC
  det_wp_SetPC det_wp_Bind
  det_wp_Embed det_wp_repeat

end