Theory Embedding

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

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

section "A Shallow Embedding of pGCL in HOL"

theory Embedding imports Misc Induction begin

subsection ‹Core Primitives and Syntax›

text_raw ‹\label{s:syntax}›

text ‹A pGCL program is embedded directly as its strict or liberal transformer.  This is
achieved with an additional parameter, specifying which semantics should be obeyed.›

type_synonym 's prog = "bool ⇒ ('s ⇒ real) ⇒ ('s ⇒ real)"

text ‹@{term Abort} either always fails, @{term "λP s. 0"}, or always succeeds,
@{term "λP s. 1"}.›
definition Abort :: "'s prog"
where     "Abort ≡ λab P s. if ab then 0 else 1"

text ‹@{term Skip} does nothing at all.›
definition Skip :: "'s prog"
where     "Skip ≡ λab P. P"

text ‹@{term Apply} lifts a state transformer into the space of programs.›
definition Apply :: "('s ⇒ 's) ⇒ 's prog"
where     "Apply f ≡ λab P s. P (f s)"

text ‹@{term Seq} is sequential composition.›
definition Seq :: "'s prog ⇒ 's prog ⇒ 's prog"
                 (infixl ";;" 59)
where     "Seq a b ≡ (λab. a ab o b ab)"

text ‹@{term PC} is \emph{probabilistic} choice between programs.›
definition PC :: "'s prog ⇒ ('s ⇒ real) ⇒ 's prog ⇒ 's prog"
                 ("_ ⇘_⇙⊕ _" [58,57,57] 57)
where     "PC a P b ≡ λab Q s. P s * a ab Q s + (1 - P s) * b ab Q s" 

text ‹@{term DC} is \emph{demonic} choice between programs.›
definition DC :: "'s prog ⇒ 's prog ⇒ 's prog" ("_ ⨅ _" [58,57] 57)
where     "DC a b ≡ λab Q s. min (a ab Q s) (b ab Q s)"

text ‹@{term AC} is \emph{angelic} choice between programs.›
definition AC :: "'s prog ⇒ 's prog ⇒ 's prog" ("_ ⨆ _" [58,57] 57)
where     "AC a b ≡ λab Q s. max (a ab Q s) (b ab Q s)"

text ‹@{term Embed} allows any expectation transformer to be treated
  syntactically as a program, by ignoring the failure flag.›
definition Embed :: "'s trans ⇒ 's prog"
where     "Embed t = (λab. t)"

text ‹@{term Mu} is the recursive primitive, and is either then
  least or greatest fixed point.›
definition Mu :: "('s prog ⇒ 's prog) ⇒ 's prog" (binder "μ" 50)
where     "Mu(T) ≡ (λab. if ab then lfp_trans (λt. T (Embed t) ab)
                               else gfp_trans (λt. T (Embed t) ab))"

text ‹@{term repeat} expresses finite repetition›
primrec
  repeat :: "nat ⇒ 'a prog ⇒ 'a prog"
where
  "repeat 0 p = Skip" |
  "repeat (Suc n) p = p ;; repeat n p"

text ‹@{term SetDC} is demonic choice between a set of alternatives,
  which may depend on the state.›
definition SetDC :: "('a ⇒ 's prog) ⇒ ('s ⇒ 'a set) ⇒ 's prog"
  where "SetDC f S ≡ λab P s. Inf ((λa. f a ab P s) ` S s)"

syntax "_SetDC" :: "pttrn => ('s => 'a set) => 's prog => 's prog"
                   ("⨅_∈_./ _" 100)
translations "⨅x∈S. p" == "CONST SetDC (%x. p) S"

text ‹The above syntax allows us to write @{term "⨅x∈S. Apply f"}›

text ‹@{term SetPC} is \emph{probabilistic} choice from a set.  Note that this is only
meaningful for distributions of finite support.›
definition
  SetPC :: "('a ⇒ 's prog) ⇒ ('s ⇒ 'a ⇒ real) ⇒ 's prog"
where
  "SetPC f p ≡ λab P s. ∑a∈supp (p s). p s a * f a ab P s"

text ‹@{term Bind} allows us to name an expression in the current state, and re-use it later.›
definition
  Bind :: "('s ⇒ 'a) ⇒ ('a ⇒ 's prog) ⇒ 's prog"
where
  "Bind g f ab ≡ λP s. let a = g s in f a ab P s"

text ‹This gives us something like let syntax›
syntax "_Bind" :: "pttrn => ('s => 'a) => 's prog => 's prog"
       ("_ is _ in _" [55,55,55]55)
translations "x is f in a" => "CONST Bind f (%x. a)"

definition flip :: "('a ⇒ 'b ⇒ 'c) ⇒ 'b ⇒ 'a ⇒ 'c"
where [simp]: "flip f = (λb a. f a b)"

text ‹The following pair of translations introduce let-style syntax
  for @{term SetPC} and @{term SetDC}, respectively.›
syntax "_PBind" :: "pttrn => ('s => real) => 's prog => 's prog"
                   ("bind _ at _ in _" [55,55,55]55)
translations "bind x at p in a" => "CONST SetPC (%x. a) (CONST flip (%x. p))"

syntax "_DBind" :: "pttrn => ('s => 'a set) ⇒ 's prog => 's prog"
                   ("bind _ from _ in _" [55,55,55]55)
translations "bind x from S in a" => "CONST SetDC (%x. a) S"

text ‹The following syntax translations are for convenience when
  using a record as the state type.›
syntax
  "_assign" :: "ident => 'a => 's prog" ("_ := _" [1000,900]900)
ML ‹
  fun assign_tr _ [Const (name,_), arg] =
      Const ("Embedding.Apply", dummyT) $
      Abs ("s", dummyT,
           Syntax.const (suffix Record.updateN name) $
           Abs (Name.uu_, dummyT, arg $ Bound 1) $ Bound 0)
    | assign_tr _ ts = raise TERM ("assign_tr", ts)
›
parse_translation ‹[(@{syntax_const "_assign"}, assign_tr)]›

syntax
  "_SetPC" :: "ident => ('s => 'a => real) => 's prog"
              ("choose _ at _" [66,66]66)
ML ‹
  fun set_pc_tr _ [Const (f,_), P] =
      Const ("SetPC", dummyT) $
      Abs ("v", dummyT,
           (Const ("Embedding.Apply", dummyT) $
            Abs ("s", dummyT,
                 Syntax.const (suffix Record.updateN f) $
                 Abs (Name.uu_, dummyT, Bound 2) $ Bound 0))) $
      P
    | set_pc_tr _ ts = raise TERM ("set_pc_tr", ts)
›
parse_translation ‹[(@{syntax_const "_SetPC"}, set_pc_tr)]›

syntax
  "_set_dc" :: "ident => ('s => 'a set) => 's prog" ("_ :∈ _" [66,66]66)
ML ‹
  fun set_dc_tr _ [Const (f,_), S] =
      Const ("SetDC", dummyT) $
      Abs ("v", dummyT,
           (Const ("Embedding.Apply", dummyT) $
            Abs ("s", dummyT,
                 Syntax.const (suffix Record.updateN f) $
                 Abs (Name.uu_, dummyT, Bound 2) $ Bound 0))) $
      S
    | set_dc_tr _ ts = raise TERM ("set_dc_tr", ts)
›
parse_translation ‹[(@{syntax_const "_set_dc"}, set_dc_tr)]›

text ‹These definitions instantiate the embedding as either
        weakest precondition (True) or weakest liberal precondition
        (False).›

syntax
  "_set_dc_UNIV" :: "ident => 's prog" ("any _" [66]66)

translations
  "_set_dc_UNIV x" => "_set_dc x (%_. CONST UNIV)"

definition
  wp :: "'s prog ⇒ 's trans"
where
  "wp pr ≡ pr True"

definition
  wlp :: "'s prog ⇒ 's trans"
where
  "wlp pr ≡ pr False"

text ‹If-Then-Else as a degenerate probabilistic choice.›
abbreviation(input)
  if_then_else :: "['s ⇒ bool, 's prog, 's prog] ⇒ 's prog"
      ("If _ Then _ Else _" 58)
where
  "If P Then a Else b == a ⇘«P»⇙⊕ b"

text ‹Syntax for loops›
abbreviation
  do_while :: "['s ⇒ bool, 's prog] ⇒ 's prog"
              ("do _ ⟶// (4 _) //od")
where
  "do_while P a ≡ μ x. If P Then a ;; x Else Skip"

subsection ‹Unfolding rules for non-recursive primitives›

lemma eval_wp_Abort:
  "wp Abort P = (λs. 0)"
  unfolding wp_def Abort_def by(simp)

lemma eval_wlp_Abort:
  "wlp Abort P = (λs. 1)"
  unfolding wlp_def Abort_def by(simp)

lemma eval_wp_Skip:
  "wp Skip P = P"
  unfolding wp_def Skip_def by(simp)

lemma eval_wlp_Skip:
  "wlp Skip P = P"
  unfolding wlp_def Skip_def by(simp)

lemma eval_wp_Apply:
  "wp (Apply f) P = P o f"
  unfolding wp_def Apply_def by(simp add:o_def)

lemma eval_wlp_Apply:
  "wlp (Apply f) P = P o f"
  unfolding wlp_def Apply_def by(simp add:o_def)

lemma eval_wp_Seq:
  "wp (a ;; b) P = (wp a o wp b) P"
  unfolding wp_def Seq_def by(simp)

lemma eval_wlp_Seq:
  "wlp (a ;; b) P = (wlp a o wlp b) P"
  unfolding wlp_def Seq_def by(simp)

lemma eval_wp_PC:
  "wp (a ⇘Q⇙⊕ b) P = (λs. Q s * wp a P s + (1 - Q s) * wp b P s)"
  unfolding wp_def PC_def by(simp)

lemma eval_wlp_PC:
  "wlp (a ⇘Q⇙⊕ b) P = (λs. Q s * wlp a P s + (1 - Q s) * wlp b P s)"
  unfolding wlp_def PC_def by(simp)

lemma eval_wp_DC:
  "wp (a ⨅ b) P = (λs. min (wp a P s) (wp b P s))"
  unfolding wp_def DC_def by(simp)

lemma eval_wlp_DC:
  "wlp (a ⨅ b) P = (λs. min (wlp a P s) (wlp b P s))"
  unfolding wlp_def DC_def by(simp)

lemma eval_wp_AC:
  "wp (a ⨆ b) P = (λs. max (wp a P s) (wp b P s))"
  unfolding wp_def AC_def by(simp)

lemma eval_wlp_AC:
  "wlp (a ⨆ b) P = (λs. max (wlp a P s) (wlp b P s))"
  unfolding wlp_def AC_def by(simp)

lemma eval_wp_Embed:
  "wp (Embed t) = t"
  unfolding wp_def Embed_def by(simp)

lemma eval_wlp_Embed:
  "wlp (Embed t) = t"
  unfolding wlp_def Embed_def by(simp)

lemma eval_wp_SetDC:
  "wp (SetDC p S) R s = Inf ((λa. wp (p a) R s) ` S s)"
  unfolding wp_def SetDC_def by(simp)

lemma eval_wlp_SetDC:
  "wlp (SetDC p S) R s = Inf ((λa. wlp (p a) R s) ` S s)"
  unfolding wlp_def SetDC_def by(simp)

lemma eval_wp_SetPC:
  "wp (SetPC f p) P = (λs. ∑a∈supp (p s). p s a * wp (f a) P s)"
  unfolding wp_def SetPC_def by(simp)

lemma eval_wlp_SetPC:
  "wlp (SetPC f p) P = (λs. ∑a∈supp (p s). p s a * wlp (f a) P s)"
  unfolding wlp_def SetPC_def by(simp)

lemma eval_wp_Mu:
  "wp (μ t. T t) = lfp_trans (λt. wp (T (Embed t)))"
  unfolding wp_def Mu_def by(simp)

lemma eval_wlp_Mu:
  "wlp (μ t. T t) = gfp_trans (λt. wlp (T (Embed t)))"
  unfolding wlp_def Mu_def by(simp)

lemma eval_wp_Bind:
  "wp (Bind g f) = (λP s. wp (f (g s)) P s)"
  unfolding Bind_def wp_def Let_def by(simp)

lemma eval_wlp_Bind:
  "wlp (Bind g f) = (λP s. wlp (f (g s)) P s)"
  unfolding Bind_def wlp_def Let_def by(simp)

text ‹Use simp add:wp\_eval to fully unfold a program fragment›
lemmas wp_eval = eval_wp_Abort eval_wlp_Abort eval_wp_Skip eval_wlp_Skip
                 eval_wp_Apply eval_wlp_Apply eval_wp_Seq eval_wlp_Seq
                 eval_wp_PC eval_wlp_PC eval_wp_DC eval_wlp_DC
                 eval_wp_AC eval_wlp_AC
                 eval_wp_Embed eval_wlp_Embed eval_wp_SetDC eval_wlp_SetDC
                 eval_wp_SetPC eval_wlp_SetPC eval_wp_Mu eval_wlp_Mu
                 eval_wp_Bind eval_wlp_Bind

lemma Skip_Seq:
  "Skip ;; A = A"
  unfolding Skip_def Seq_def o_def by(rule refl)

lemma Seq_Skip:
  "A ;; Skip = A"
  unfolding Skip_def Seq_def o_def by(rule refl)

text ‹Use these as simp rules to clear out Skips›
lemmas skip_simps = Skip_Seq Seq_Skip

end