Theory PGCL

(* Author: Johannes Hölzl <hoelzl@in.tum.de> *)

section ‹Probabilistic Guarded Command Language (pGCL)›

theory PGCL
  imports "../Markov_Decision_Process"
begin

subsection ‹Syntax›

datatype 's pgcl =
    Skip
  | Abort
  | Assign "'s ⇒ 's"
  | Seq "'s pgcl" "'s pgcl"
  | Par "'s pgcl" "'s pgcl"
  | If "'s ⇒ bool" "'s pgcl" "'s pgcl"
  | Prob "bool pmf" "'s pgcl" "'s pgcl"
  | While "'s ⇒ bool" "'s pgcl"

subsection ‹Denotational Semantics›

primrec wp :: "'s pgcl ⇒ ('s ⇒ ennreal) ⇒ ('s ⇒ ennreal)" where
  "wp Skip f          = f"
| "wp Abort f         = (λ_. 0)"
| "wp (Assign u) f    = f ∘ u"
| "wp (Seq c1 c2) f    = wp c1 (wp c2 f)"
| "wp (If b c1 c2) f   = (λs. if b s then wp c1 f s else wp c2 f s)"
| "wp (Par c1 c2) f    = wp c1 f ⊓ wp c2 f"
| "wp (Prob p c1 c2) f = (λs. pmf p True * wp c1 f s + pmf p False * wp c2 f s)"
| "wp (While b c) f   = lfp (λX s. if b s then wp c X s else f s)"

lemma wp_mono: "mono (wp c)"
  by (induction c)
     (auto simp: monotone_def le_fun_def intro: order_trans le_infI1 le_infI2
           intro!: add_mono mult_left_mono lfp_mono[THEN le_funD])

abbreviation det :: "'s pgcl ⇒ 's ⇒ ('s pgcl × 's) pmf set" ("≪ _, _ ≫") where
  "det c s ≡ {return_pmf (c, s)}"

subsection ‹Operational Semantics›

fun step :: "('s pgcl × 's) ⇒ ('s pgcl × 's) pmf set" where
  "step (Skip, s)        = ≪Skip, s≫"
| "step (Abort, s)       = ≪Abort, s≫"
| "step (Assign u, s)    = ≪Skip, u s≫"
| "step (Seq c1 c2, s)    = (map_pmf (λ(p1', s'). (if p1' = Skip then c2 else Seq p1' c2, s'))) ` step (c1, s)"
| "step (If b c1 c2, s)   = (if b s then ≪c1, s≫ else ≪c2, s≫)"
| "step (Par c1 c2, s)    = ≪c1, s≫ ∪ ≪c2, s≫"
| "step (Prob p c1 c2, s) = {map_pmf (λb. if b then (c1, s) else (c2, s)) p}"
| "step (While b c, s)   = (if b s then ≪Seq c (While b c), s≫ else ≪Skip, s≫)"

lemma step_finite: "finite (step x)"
  by (induction x rule: step.induct) simp_all

lemma step_non_empty: "step x ≠ {}"
  by (induction x rule: step.induct) simp_all

interpretation step: Markov_Decision_Process step
  proof qed (rule step_non_empty)

definition rF :: "('s ⇒ ennreal) ⇒ (('s pgcl × 's) stream ⇒ ennreal) ⇒ ('s pgcl × 's) stream ⇒ ennreal" where
  "rF f F ω = (if fst (shd ω) = Skip then f (snd (shd ω)) else F (stl ω))"

abbreviation r :: "('s ⇒ ennreal) ⇒ ('s pgcl × 's) stream ⇒ ennreal" where
  "r f ≡ lfp (rF f)"

lemma continuous_rF: "sup_continuous (rF f)"
  unfolding rF_def[abs_def]
  by (auto simp: sup_continuous_def fun_eq_iff SUP_sup_distrib [symmetric] image_comp
           split: prod.splits pgcl.splits)

lemma mono_rF: "mono (rF f)"
  using continuous_rF by (rule sup_continuous_mono)

lemma r_unfold: "r f ω = (if fst (shd ω) = Skip then f (snd (shd ω)) else r f (stl ω))"
  by (subst lfp_unfold[OF mono_rF]) (simp add: rF_def)

lemma mono_r: "F ≤ G ⟹ r F ω ≤ r G ω"
  by (rule le_funD[of _ _ ω], rule lfp_mono)
     (auto intro!: lfp_mono simp: rF_def le_fun_def max.coboundedI2)

lemma measurable_rF:
  assumes F[measurable]: "F ∈ borel_measurable step.St"
  shows "rF f F ∈ borel_measurable step.St"
  unfolding rF_def[abs_def]
  apply measurable
  apply (rule measurable_compose[OF measurable_shd])
  apply measurable []
  apply (rule measurable_compose[OF measurable_stl])
  apply measurable []
  apply (rule predE)
  apply (rule measurable_compose[OF measurable_shd])
  apply measurable
  done

lemma measurable_r[measurable]: "r f ∈ borel_measurable step.St"
  using continuous_rF measurable_rF by (rule borel_measurable_lfp)

lemma mono_r': "mono (λF s. ⨅D∈step s. ∫+ t. (if fst t = Skip then f (snd t) else F t) ∂measure_pmf D)"
  by (auto intro!: monoI le_funI INF_mono[OF bexI] nn_integral_mono simp: le_fun_def)

lemma E_inf_r:
  "step.E_inf s (r f) =
    lfp (λF s. ⨅D∈step s. ∫+ t. (if fst t = Skip then f (snd t) else F t) ∂measure_pmf D) s"
proof -
  have "step.E_inf s (r f) =
    lfp (λF s. ⨅D∈step s. ∫+ t. (if fst t = Skip then f (snd t) else F t) ∂measure_pmf D) s"
    unfolding rF_def[abs_def]
  proof (rule step.E_inf_lfp[THEN fun_cong])
    let ?F = "λt x. (if fst t = Skip then f (snd t) else x)"
    show "(λ(s, x). ?F s x) ∈ borel_measurable (count_space UNIV ⨂M borel)"
      apply (simp add: measurable_split_conv split_beta')
      apply (intro borel_measurable_max borel_measurable_const measurable_If predE
         measurable_compose[OF measurable_snd] measurable_compose[OF measurable_fst])
      apply measurable
      done
    show "⋀s. sup_continuous (?F s)"
      by (auto simp: sup_continuous_def SUP_sup_distrib[symmetric] split: prod.split pgcl.split)
    show "⋀F cfg. (∫+ω. ?F (state cfg) (F ω) ∂step.T cfg) =
      ?F (state cfg) (nn_integral (step.T cfg) F)"
      by (auto simp: split: pgcl.split prod.split)
  qed (rule step_finite)
  then show ?thesis
    by simp
qed

lemma E_inf_r_unfold:
  "step.E_inf s (r f) = (⨅D∈step s. ∫+ t. (if fst t = Skip then f (snd t) else step.E_inf t (r f)) ∂measure_pmf D)"
  unfolding E_inf_r by (simp add: lfp_unfold[OF mono_r'])

lemma E_inf_r_induct[consumes 1, case_names step]:
  assumes "P s y"
  assumes *: "⋀F s y. P s y ⟹
    (⋀s y. P s y ⟹ F s ≤ y) ⟹ (⋀s. F s ≤ step.E_inf s (r f)) ⟹
    (⨅D∈step s. ∫+ t. (if fst t = Skip then f (snd t) else F t) ∂measure_pmf D) ≤ y"
  shows "step.E_inf s (r f) ≤ y"
  using ‹P s y›
  unfolding E_inf_r
proof (induction arbitrary: s y rule: lfp_ordinal_induct[OF mono_r'[where f=f]])
  case (1 F) with *[of s y F] show ?case
    unfolding le_fun_def E_inf_r[where f=f, symmetric] by simp
qed (auto intro: SUP_least)

lemma E_inf_Skip: "step.E_inf (Skip, s) (r f) = f s"
  by (subst E_inf_r_unfold) simp

lemma E_inf_Seq:
  assumes [simp]: "⋀x. 0 ≤ f x"
  shows "step.E_inf (Seq a b, s) (r f) = step.E_inf (a, s) (r (λs. step.E_inf (b, s) (r f)))"
proof (rule antisym)
  show "step.E_inf (Seq a b, s) (r f) ≤ step.E_inf (a, s) (r (λs. step.E_inf (b, s) (r f)))"
  proof (coinduction arbitrary: a s rule: E_inf_r_induct)
    case step then show ?case
      by (rewrite in "_ ≤ ⌑" E_inf_r_unfold)
         (force intro!: INF_mono[OF bexI] nn_integral_mono intro: le_infI2
                simp: E_inf_Skip image_comp)
  qed
  show "step.E_inf (a, s) (r (λs. step.E_inf (b, s) (r f))) ≤ step.E_inf (Seq a b, s) (r f)"
  proof (coinduction arbitrary: a s rule: E_inf_r_induct)
    case step then show ?case
      by (rewrite in "_ ≤ ⌑" E_inf_r_unfold)
         (force intro!: INF_mono[OF bexI] nn_integral_mono intro: le_infI2
                simp: E_inf_Skip image_comp)
   qed
qed

lemma E_inf_While:
  "step.E_inf (While g c, s) (r f) =
    lfp (λF s. if g s then step.E_inf (c, s) (r F) else f s) s"
proof (rule antisym)
  have E_inf_While_step: "step.E_inf (While g c, s) (r f) =
    (if g s then step.E_inf (c, s) (r (λs. step.E_inf (While g c, s) (r f))) else f s)" for f s
    by (rewrite E_inf_r_unfold) (simp add: min_absorb1 E_inf_Seq)

  have "mono (λF s. if g s then step.E_inf (c, s) (r F) else f s)" (is "mono ?F")
    by (auto intro!: mono_r step.E_inf_mono simp: mono_def le_fun_def max.coboundedI2)
  then show "lfp ?F s ≤ step.E_inf (While g c, s) (r f)"
  proof (induction arbitrary: s rule: lfp_ordinal_induct[consumes 1])
    case mono then show ?case
      by (rewrite E_inf_While_step) (auto intro!: step.E_inf_mono mono_r le_funI)
  qed (auto intro: SUP_least)

  define w where "w F s = (⨅D∈step s. ∫+ t. (if fst t = Skip then if g (snd t) then F (c, snd t) else f (snd t) else F t) ∂measure_pmf D)"
    for F s
  have "mono w"
    by (auto simp: w_def mono_def le_fun_def intro!: INF_mono[OF bexI] nn_integral_mono) []

  define d where "d = c"
  define t where "t = Seq d (While g c)"
  then have "(t = While g c ∧ d = c ∧ g s) ∨ t = Seq d (While g c)"
    by auto
  then have "step.E_inf (t, s) (r f) ≤ lfp w (d, s)"
  proof (coinduction arbitrary: t d s rule: E_inf_r_induct)
    case (step F t d s)
    from step(1)
    show ?case
    proof (elim conjE disjE)
      { fix s have "¬ g s ⟹ F (While g c, s) ≤ f s"
          using step(3)[of "(While g c, s)"] by (simp add: E_inf_While_step) }
      note [simp] = this
      assume "t = Seq d (While g c)" then show ?thesis
        by (rewrite lfp_unfold[OF ‹mono w›])
           (auto simp: max.absorb2 w_def intro!: INF_mono[OF bexI] nn_integral_mono step)
    qed (auto intro!: step)
  qed
  also have "lfp w = lfp (λF s. step.E_inf s (r (λs. if g s then F (c, s) else f s)))"
    unfolding E_inf_r w_def
    by (rule lfp_lfp[symmetric]) (auto simp: le_fun_def intro!: INF_mono[OF bexI] nn_integral_mono)
  finally have "step.E_inf (While g c, s) (r f) ≤ (if g s then … (c, s) else f s)"
    unfolding t_def d_def by (rewrite E_inf_r_unfold) simp
  also have "… = lfp ?F s"
    by (rewrite lfp_rolling[symmetric, of "λF s. if g s then F (c, s) else f s"  "λF s. step.E_inf s (r F)"])
       (auto simp: mono_def le_fun_def sup_apply[abs_def] if_distrib[of "max 0"] max.coboundedI2 max.absorb2
                intro!: step.E_inf_mono mono_r cong del: if_weak_cong)
  finally show "step.E_inf (While g c, s) (r f) ≤ …"
    .
qed

subsection ‹Equate Both Semantics›

lemma E_inf_r_eq_wp: "step.E_inf (c, s) (r f) = wp c f s"
proof (induction c arbitrary: f s)
  case Skip then show ?case
    by (simp add: E_inf_Skip)
next
  case Abort then show ?case
  proof (intro antisym)
    have "lfp (λF s. ⨅D∈step s. ∫+ t. (if fst t = Skip then f (snd t) else F t) ∂measure_pmf D) ≤
      (λs. if ∃t. s = (Abort, t) then 0 else ⊤)"
      by (intro lfp_lowerbound) (auto simp: le_fun_def)
    then show "step.E_inf (Abort, s) (r f) ≤ wp Abort f s"
      by (auto simp: E_inf_r le_fun_def split: if_split_asm)
  qed simp
next
  case Assign then show ?case
    by (rewrite E_inf_r_unfold) (simp add: min_absorb1)
next
  case (If b c1 c2) then show ?case
    by (rewrite E_inf_r_unfold) auto
next
  case (Prob p c1 c2) then show ?case
    apply (rewrite E_inf_r_unfold)
    apply auto
    apply (rewrite nn_integral_measure_pmf_support[of "UNIV::bool set"])
    apply (auto simp: UNIV_bool ac_simps)
    done
next
  case (Par c1 c2) then show ?case
    by (rewrite E_inf_r_unfold) (auto intro: inf.commute)
next
  case (Seq c1 c2) then show ?case
    by (simp add: E_inf_Seq)
next
  case (While g c) then show ?case
    apply (simp add: E_inf_While)
    apply (rewrite While)
    apply auto
    done
qed

end