Quelle  Embedding.thy

(*
 * 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
  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)
syntax_consts "_SetDC" == SetDC
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
  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)
syntax_consts "_Bind" == Bind
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)
syntax_consts "_PBind" == SetPC
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)
syntax_consts "_DBind" == SetDC
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)
syntax_consts
  "_SetPC" ⇌ SetPC
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)
syntax_consts
  "_set_dc" ⇌ SetDC
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)
syntax_consts
  "_set_dc_UNIV" == SetDC
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 _{<guillemotleft>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 ⊕ 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 ⊕ 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