# 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 c⇩1 c⇩2) f    = wp c⇩1 (wp c⇩2 f)"
| "wp (If b c⇩1 c⇩2) f   = (λs. if b s then wp c⇩1 f s else wp c⇩2 f s)"
| "wp (Par c⇩1 c⇩2) f    = wp c⇩1 f ⊓ wp c⇩2 f"
| "wp (Prob p c⇩1 c⇩2) f = (λs. pmf p True * wp c⇩1 f s + pmf p False * wp c⇩2 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

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 c⇩1 c⇩2, s)    = (map_pmf (λ(p1', s'). (if p1' = Skip then c⇩2 else Seq p1' c⇩2, s'))) ` step (c⇩1, s)"
| "step (If b c⇩1 c⇩2, s)   = (if b s then ≪c⇩1, s≫ else ≪c⇩2, s≫)"
| "step (Par c⇩1 c⇩2, s)    = ≪c⇩1, s≫ ∪ ≪c⇩2, s≫"
| "step (Prob p c⇩1 c⇩2, s) = {map_pmf (λb. if b then (c⇩1, s) else (c⇩2, 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 (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
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