# Theory PCTL

```(* Author: Johannes Hölzl <hoelzl@in.tum.de>
Author: Tobias Nipkow <nipkow@in.tum.de> *)
theory PCTL
imports
"../Discrete_Time_Markov_Chain"
"Gauss-Jordan-Elim-Fun.Gauss_Jordan_Elim_Fun"
"HOL-Library.While_Combinator"
"HOL-Library.Monad_Syntax"
begin

section ‹Adapt Gauss-Jordan elimination to DTMCs›

locale Finite_DTMC =
fixes K :: "'s ⇒ 's pmf" and S :: "'s set" and ρ :: "'s ⇒ real" and ι :: "'s ⇒ 's ⇒ real"
assumes ι_nonneg[simp]: "⋀s t. 0 ≤ ι s t" and ρ_nonneg[simp]: "⋀s. 0 ≤ ρ s"
assumes measurable_ι: "(λ(a, b). ι a b) ∈ borel_measurable (count_space UNIV ⨂⇩M count_space UNIV)"
assumes finite_S[simp]: "finite S" and S_not_empty: "S ≠ {}"
assumes E_closed: "(⋃s∈S. set_pmf (K s)) ⊆ S"
begin

lemma measurable_ι'[measurable (raw)]:
"f ∈ measurable M (count_space UNIV) ⟹ g ∈ measurable M (count_space UNIV) ⟹
(λx. ι (f x) (g x)) ∈ borel_measurable M"
using measurable_compose[OF _ measurable_ι, of "λx. (f x, g x)" M] by simp

lemma measurable_ρ[measurable]: "ρ ∈ borel_measurable (count_space UNIV)"
by simp

sublocale R?: MC_with_rewards K ι ρ
by standard (auto intro: ι_nonneg ρ_nonneg)

lemma single_l:
fixes s and x :: real assumes "s ∈ S"
shows "(∑s'∈S. (if s' = s then 1 else 0) * l s') = x ⟷ l s = x"
by (simp add: assms if_distrib [of "λx. x * a" for a] cong: if_cong)

definition "order = (SOME f. bij_betw f {..< card S} S)"

lemma
shows bij_order[simp]: "bij_betw order {..< card S} S"
and inj_order[simp]: "inj_on order {..<card S}"
and image_order[simp]: "order ` {..<card S} = S"
and order_S[simp, intro]: "⋀i. i < card S ⟹ order i ∈ S"
proof -
from finite_same_card_bij[OF _ finite_S] show "bij_betw order {..< card S} S"
unfolding order_def by (rule someI_ex) auto
then show "inj_on order {..<card S}" "order ` {..<card S} = S"
unfolding bij_betw_def by auto
then show "⋀i. i < card S ⟹ order i ∈ S"
by auto
qed

lemma order_Ex:
assumes "s ∈ S" obtains i where "i < card S" "s = order i"
proof -
from ‹s ∈ S› have "s ∈ order ` {..<card S}"
by simp
with that show thesis
by (auto simp del: image_order)
qed

definition "iorder = the_inv_into {..<card S} order"

lemma bij_iorder: "bij_betw iorder S {..<card S}"
unfolding iorder_def by (rule bij_betw_the_inv_into bij_order)+

lemma iorder_image_eq: "iorder ` S = {..<card S}"
and inj_iorder: "inj_on iorder S"
using bij_iorder  unfolding bij_betw_def by auto

lemma order_iorder: "⋀s. s ∈ S ⟹ order (iorder s) = s"
unfolding iorder_def using bij_order
by (intro f_the_inv_into_f) (auto simp: bij_betw_def)

definition gauss_jordan' :: "('s ⇒ 's ⇒ real) ⇒ ('s ⇒ real) ⇒ ('s ⇒ real) option" where
"gauss_jordan' M a = do {
let M' = (λi j. if j = card S then a (order i) else M (order i) (order j)) ;
sol ← gauss_jordan M' (card S) ;
Some (λi. sol (iorder i) (card S))
}"

lemma gauss_jordan'_correct:
assumes "gauss_jordan' M a = Some f"
shows "∀s∈S. (∑s'∈S. M s s' * f s') = a s"
proof -
note ‹gauss_jordan' M a = Some f›
moreover define M' where "M' = (λi j. if j = card S then
a (order i) else M (order i) (order j))"
ultimately obtain sol where sol: "gauss_jordan M' (card S) = Some sol"
and f: "f = (λi. sol (iorder i) (card S))"
by (auto simp: gauss_jordan'_def Let_def split: bind_split_asm)

from gauss_jordan_correct[OF sol]
have "∀i∈{..<card S}. (∑j<card S. M (order i) (order j) * sol j (card S)) = a (order i)"
unfolding solution_def M'_def by (simp add: atLeast0LessThan)
then show ?thesis
unfolding iorder_image_eq[symmetric] f using inj_iorder
by (subst (asm) sum.reindex) (auto simp: order_iorder)
qed

lemma gauss_jordan'_complete:
assumes exists: "∀s∈S. (∑s'∈S. M s s' * x s') = a s"
assumes unique: "⋀y. ∀s∈S. (∑s'∈S. M s s' * y s') = a s ⟹ ∀s∈S. y s = x s"
shows "∃y. gauss_jordan' M a = Some y"
proof -
define M' where "M' = (λi j. if j = card S then
a (order i) else M (order i) (order j))"

{ fix x
have iorder_neq_card_S: "⋀s. s ∈ S ⟹ iorder s ≠ card S"
using iorder_image_eq by (auto simp: set_eq_iff less_le)
have "solution2 M' (card S) (card S) x ⟷
(∀s∈{..<card S}. (∑s'∈{..<card S}. M' s s' * x s') = M' s (card S))"
unfolding solution2_def by (auto simp: atLeast0LessThan)
also have "… ⟷ (∀s∈S. (∑s'∈S. M s s' * x (iorder s')) = a s)"
unfolding iorder_image_eq[symmetric] M'_def
using inj_iorder iorder_neq_card_S
by (simp add: sum.reindex order_iorder)
finally have "solution2 M' (card S) (card S) x ⟷
(∀s∈S. (∑s'∈S. M s s' * x (iorder s')) = a s)" . }
note sol2_eq = this
have "usolution M' (card S) (card S) (λi. x (order i))"
unfolding usolution_def
proof safe
from exists show "solution2 M' (card S) (card S) (λi. x (order i))"
by (simp add: sol2_eq order_iorder)
next
fix y j assume y: "solution2 M' (card S) (card S) y" and "j < card S"
then have "∀s∈S. (∑s'∈S. M s s' * y (iorder s')) = a s"
by (simp add: sol2_eq)
from unique[OF this]
have "∀i∈{..<card S}. y i = x (order i)"
unfolding iorder_image_eq[symmetric]
by (simp add: order_iorder)
with ‹j < card S› show "y j = x (order j)" by simp
qed
from gauss_jordan_complete[OF _ this]
show ?thesis
by (auto simp: gauss_jordan'_def simp: M'_def)
qed

end

section ‹pCTL model checking›

subsection ‹Syntax›

datatype realrel = LessEqual | Less | Greater | GreaterEqual | Equal

datatype 's sform = "true"
| "Label" "'s set"
| "Neg" "'s sform"
| "And" "'s sform" "'s sform"
| "Prob" "realrel" "real" "'s pform"
| "Exp" "realrel" "real" "'s eform"
and 's pform = "X" "'s sform"
| "U" "nat" "'s sform" "'s sform"
| "UInfinity" "'s sform" "'s sform" ("U⇧∞")
and 's eform = "Cumm" "nat" ("C⇧≤")
| "State" "nat" ("I⇧=")
| "Future" "'s sform"

primrec bound_until where
"bound_until 0 φ ψ = ψ"
| "bound_until (Suc n) φ ψ = ψ or (φ aand nxt (bound_until n φ ψ))"

lemma measurable_bound_until[measurable]:
assumes [measurable]: "Measurable.pred (stream_space M) φ" "Measurable.pred (stream_space M) ψ"
shows "Measurable.pred (stream_space M) (bound_until n φ ψ)"
by (induct n) simp_all

subsection ‹Semantics›

primrec inrealrel :: "realrel ⇒ 'a ⇒ ('a::linorder) ⇒ bool" where
"inrealrel LessEqual r q    ⟷ q ≤ r" |
"inrealrel Less r q         ⟷ q < r" |
"inrealrel Greater r q      ⟷ q > r" |
"inrealrel GreaterEqual r q ⟷ q ≥ r" |
"inrealrel Equal r q        ⟷ q = r"

context Finite_DTMC
begin

abbreviation "prob s P ≡ measure (T s) {x∈space (T s). P x}"
abbreviation "E s ≡ set_pmf (K s)"

primrec svalid :: "'s sform ⇒ 's set"
and pvalid :: "'s pform ⇒ 's stream ⇒ bool"
and reward :: "'s eform ⇒ 's stream ⇒ ennreal" where
"svalid true           = S" |
"svalid (Label L)      = {s ∈ S. s ∈ L}" |
"svalid (Neg F)        = S - svalid F" |
"svalid (And F1 F2)    = svalid F1 ∩ svalid F2" |
"svalid (Prob rel r F) = {s ∈ S. inrealrel rel r 𝒫(ω in T s. pvalid F (s ## ω)) }" |
"svalid (Exp rel r F)  = {s ∈ S. inrealrel rel (ennreal r) (∫⇧+ ω. reward F (s ## ω) ∂T s) }" |

"pvalid (X F)        = nxt (HLD (svalid F))" |
"pvalid (U k F1 F2)  = bound_until k (HLD (svalid F1)) (HLD (svalid F2))" |
"pvalid (U⇧∞ F1 F2)   = HLD (svalid F1) suntil HLD (svalid F2)" |

"reward (C⇧≤ k)         = (λω. (∑i<k. ρ (ω !! i) + ι (ω !! i) (ω !! (Suc i))))" |
"reward (I⇧= k)         = (λω. ρ (ω !! k))" |
"reward (Future F)     = (λω. if ev (HLD (svalid F)) ω then reward_until (svalid F) (shd ω) (stl ω) else ∞)"

lemma svalid_subset_S: "svalid F ⊆ S"
by (induct F) auto

lemma finite_svalid[simp, intro]: "finite (svalid F)"
using svalid_subset_S finite_S by (blast intro: finite_subset)

lemma svalid_sets[measurable]: "svalid F ∈ sets (count_space S)"
using svalid_subset_S by auto

lemma pvalid_sets[measurable]: "Measurable.pred R.S (pvalid F)"
by (cases F) (auto intro!: svalid_sets)

lemma reward_measurable[measurable]: "reward F ∈ borel_measurable R.S"
by (cases F) auto

subsection ‹Implementation of ‹Sat››

subsubsection ‹‹Prob0››

definition Prob0 where
"Prob0 Φ Ψ = S - while (λR. ∃s∈Φ. R ∩ E s ≠ {} ∧ s ∉ R) (λR. R ∪ {s∈Φ. R ∩ E s ≠ {}}) Ψ"

lemma Prob0_subset_S: "Prob0 Φ Ψ ⊆ S"
unfolding Prob0_def by auto

lemma Prob0_iff_reachable:
assumes "Φ ⊆ S" "Ψ ⊆ S"
shows "Prob0 Φ Ψ = {s ∈ S. ((SIGMA x:Φ. E x)⇧* `` {s}) ∩ Ψ = {}}" (is "_ = ?U")
unfolding Prob0_def
proof (intro while_rule[where Q="λR. S - R = ?U" and P="λR. Ψ ⊆ R ∧ R ⊆ S - ?U"] conjI)
show "wf {(B, A). A ⊂ B ∧ B ⊆ S}"
by (rule wf_bounded_set[where ub="λ_. S" and f="λx. x"]) auto
show "Ψ ⊆ S - ?U"
using assms by auto

let ?Δ = "λR. {s∈Φ. R ∩ E s ≠ {}}"
{ fix R assume R: "Ψ ⊆ R ∧ R ⊆ S - ?U" and "∃s∈Φ. R ∩ E s ≠ {} ∧ s ∉ R"
with assms show "(R ∪ ?Δ R, R) ∈ {(B, A). A ⊂ B ∧ B ⊆ S}" "Ψ ⊆ R ∪ ?Δ R"
by auto

{ fix s s' assume s: "s ∈ Φ" "s' ∈ R" "s' ∈ E s" and r: "(Sigma Φ E)⇧* `` {s} ∩ Ψ = {}"
with R have "(s, s') ∈ (Sigma Φ E)⇧*" "s' ∈ Φ - Ψ"
by (auto elim: converse_rtranclE)
moreover with ‹s' ∈ R› R obtain s'' where "(s', s'') ∈ (Sigma Φ E)⇧*" "s'' ∈ Ψ"
by auto
ultimately have "(s, s'') ∈ (Sigma Φ E)⇧*" "s'' ∈ Ψ"
by auto
with r have False
by auto }
with ‹Φ ⊆ S› R show "R ∪ ?Δ R ⊆ S - ?U" by auto }

{ fix R assume R: "Ψ ⊆ R ∧ R ⊆ S - ?U" and dR: "¬ (∃s∈Φ. R ∩ E s ≠ {} ∧ s ∉ R)"
{ fix s t assume s: "s ∈ S - R"
assume s_t: "(s, t) ∈ (Sigma Φ E)⇧*" then have "t ∈ S - R"
proof induct
case (step t u) with R dR E_closed show ?case
by auto
qed fact
then have "t ∉ Ψ"
using R by auto }
with R show "S - R = ?U"
by auto }
qed rule

lemma Prob0_iff:
assumes "Φ ⊆ S" "Ψ ⊆ S"
shows "Prob0 Φ Ψ = {s∈S. AE ω in T s. ¬ (HLD Φ suntil HLD Ψ) (s ## ω)}" (is "_ = ?U")
unfolding Prob0_iff_reachable[OF assms]
proof (intro Collect_cong conj_cong refl iffI)
fix s assume s: "s ∈ S" "(Sigma Φ E)⇧* `` {s} ∩ Ψ = {}"
{ fix ω assume "(HLD Φ suntil HLD Ψ) ω" "enabled (shd ω) (stl ω)" "(Sigma Φ E)⇧* `` {shd ω} ∩ Ψ = {}"
from this have False
proof induction
case (step ω)
moreover
then have "(shd ω, shd (stl ω)) ∈ (Sigma Φ E)⇧*"
by (auto simp: enabled.simps[of _ "stl ω"] HLD_iff)
then have "(Sigma Φ E)⇧* `` {shd (stl ω)} ⊆ (Sigma Φ E)⇧* `` {shd ω}"
by auto
ultimately show ?case
by (auto simp add: enabled.simps[of _ "stl ω"])
qed (auto simp: HLD_iff) }
from s this[of "s ## ω" for ω] show "AE ω in T s. ¬ (HLD Φ suntil HLD Ψ) (s ## ω)"
using AE_T_enabled[of s] by auto
next
fix s assume s: "AE ω in T s. ¬ (HLD Φ suntil HLD Ψ) (s ## ω)"
{ fix t assume "(s, t) ∈ (Sigma Φ E)⇧*" from this s have "t ∉ Ψ"
proof (induction rule: converse_rtrancl_induct)
case (step s u) then show ?case
by (simp add: AE_T_iff[where x=s] suntil_Stream[of _ _ s])
qed (simp add: suntil_Stream) }
then show "(Sigma Φ E)⇧* `` {s} ∩ Ψ = {}"
by auto
qed

lemma E_rtrancl_closed:
assumes "s ∈ S" "(s, t) ∈ (SIGMA x:A. B x)⇧*" "⋀x. x ∈ A ⟹ B x ⊆ E x" shows "t ∈ S"
using assms(2,3,1) E_closed by induction force+

subsubsection ‹‹Prob1››

definition Prob1 where
"Prob1 Y Φ Ψ = Prob0 (Φ - Ψ) Y"

lemma Prob1_iff:
assumes "Φ ⊆ S" "Ψ ⊆ S"
shows "Prob1 (Prob0 Φ Ψ) Φ Ψ = {s∈S. AE ω in T s. (HLD Φ suntil HLD Ψ) (s ## ω)}"
(is "Prob1 ?P0 _ _ = {s∈S. ?pU s}")
proof -
note P0 = Prob0_iff_reachable[OF assms]
have *: "Φ - Ψ ⊆ S" "?P0 ⊆ S"
using P0 assms by auto

have P0_subset: "S - Φ - Ψ ⊆ ?P0"
unfolding P0 by (auto elim: converse_rtranclE)

have "Prob1 ?P0 Φ Ψ = {s ∈ S. (Sigma (Φ - Ψ) E)⇧* `` {s} ∩ ?P0 = {}}"
unfolding Prob0_iff_reachable[OF *] Prob1_def ..
also have "… = {s∈S. AE ω in T s. (HLD Φ suntil HLD Ψ) (s ## ω)}"
proof (intro Collect_cong conj_cong refl iffI)
fix s assume s: "s ∈ S" "(Sigma (Φ - Ψ) E)⇧* `` {s} ∩ ?P0 = {}"
then have "s ∉ ?P0"
by auto
then have "s ∈ Φ - Ψ ∨ s ∈ Ψ"
using P0_subset ‹s ∈ S› by auto
moreover
{ assume "s ∈ Φ - Ψ"
have "AE ω in T s. ev (HLD (Ψ ∪ ?P0)) ω"
proof (rule AE_T_ev_HLD)
fix t assume s_t: "(s, t) ∈ acc_on (- (Ψ ∪ ?P0))"
from ‹s ∈ S› s_t have "t ∈ S"
by (rule E_rtrancl_closed) auto

show "∃t'∈Ψ ∪ ?P0. (t, t') ∈ acc"
proof cases
assume "t ∈ ?P0" then show ?thesis by auto
next
assume "t ∉ ?P0"
with ‹t∈S› obtain s where t_s: "(t, s) ∈ (SIGMA x:Φ. E x)⇧*" and "s ∈ Ψ"
unfolding P0 by auto
from t_s have "(t, s) ∈ acc"
by (rule rev_subsetD) (intro rtrancl_mono Sigma_mono, auto)
with ‹s ∈ Ψ› show ?thesis by auto
qed
next
have "acc_on (- (Ψ ∪ ?P0)) `` {s} ⊆ S"
using ‹s ∈ S› by (auto intro: E_rtrancl_closed)
then show "finite (acc_on (- (Ψ ∪ ?P0)) `` {s})"
using finite_S by (auto dest: finite_subset)
qed
then have "AE ω in T s. (HLD Φ suntil HLD Ψ) ω"
using AE_T_enabled
proof eventually_elim
fix ω assume "ev (HLD (Ψ ∪ ?P0)) ω" "enabled s ω"
from this s ‹s ∈ Φ - Ψ› show "(HLD Φ suntil HLD Ψ) ω"
proof (induction arbitrary: s)
case (base ω) then show ?case
by (auto simp: HLD_iff enabled.simps[of s] intro: suntil.intros)
next
case (step ω)
then have "(s, shd ω) ∈ (Sigma (Φ - Ψ) E)"
by (auto simp: enabled.simps[of s])
then have *: "(Sigma (Φ - Ψ) E)⇧* `` {shd ω} ∩ ?P0 = {}"
using step.prems by (auto intro: converse_rtrancl_into_rtrancl)
then have "shd ω ∈ Φ - Ψ ∨ shd ω ∈ Ψ" "shd ω ∈ S"
using P0_subset step.prems(1,2) E_closed by (auto simp add: enabled.simps[of s])
then show ?case
using step.prems(1) step.IH[OF _ _ *] ‹shd ω ∈ S›
by (auto simp add: suntil.simps[of _ _ ω] HLD_iff[abs_def] enabled.simps[of s ω])
qed
qed }
ultimately show "AE ω in T s. (HLD Φ suntil HLD Ψ) (s ## ω)"
by (cases "s ∈ Φ - Ψ") (auto simp add: suntil_Stream)
next
fix s assume s: "s ∈ S" "AE ω in T s. (HLD Φ suntil HLD Ψ) (s ## ω)"
{ fix t assume "(s, t) ∈ (SIGMA s:Φ-Ψ. E s)⇧*"
from this ‹s ∈ S› have "(AE ω in T t. (HLD Φ suntil HLD Ψ) (t ## ω)) ∧ t ∈ S"
proof induction
case (step t u) with E_closed show ?case
by (auto simp add: AE_T_iff[of _ t] suntil_Stream)
qed (insert s, auto)
then have "t ∉ ?P0"
unfolding Prob0_iff[OF assms] by (auto dest: T.AE_contr) }
then show "(Sigma (Φ - Ψ) E)⇧* `` {s} ∩ Prob0 Φ Ψ = {}"
by auto
qed
finally show ?thesis .
qed

subsubsection ‹‹ProbU›,  ‹ExpCumm›, and ‹ExpState››

abbreviation "τ s t ≡ pmf (K s) t"

fun ProbU :: "'s ⇒ nat ⇒ 's set ⇒ 's set ⇒ real" where
"ProbU q 0 S1 S2       = (if q ∈ S2 then 1 else 0)" |
"ProbU q (Suc k) S1 S2 =
(if q ∈ S1 - S2 then (∑q'∈S. τ q q' * ProbU q' k S1 S2)
else if q ∈ S2 then 1 else 0)"

fun ExpCumm :: "'s ⇒ nat ⇒ ennreal" where
"ExpCumm s 0       = 0" |
"ExpCumm s (Suc k) = ρ s + (∑s'∈S. τ s s' * (ι s s' + ExpCumm s' k))"

fun ExpState :: "'s ⇒ nat ⇒ ennreal" where
"ExpState s 0       = ρ s" |
"ExpState s (Suc k) = (∑s'∈S. τ s s' * ExpState s' k)"

subsubsection ‹‹LES››

definition LES :: "'s set ⇒ 's ⇒ 's ⇒ real" where
"LES F r c =
(if r ∈ F then (if c = r then 1 else 0)
else (if c = r then τ r c - 1 else τ r c ))"

subsubsection ‹‹ProbUinfty›, compute unbounded until›

definition ProbUinfty :: "'s set ⇒ 's set ⇒ ('s ⇒ real) option" where
"ProbUinfty S1 S2 = gauss_jordan' (LES (Prob0 S1 S2 ∪ S2))
(λi. if i ∈ S2 then 1 else 0)"

subsubsection ‹‹ExpFuture›, compute unbounded reward›

definition ExpFuture :: "'s set ⇒ ('s ⇒ ennreal) option" where
"ExpFuture F = do {
let N = Prob0 S F ;
let Y = Prob1 N S F ;
sol ← gauss_jordan' (LES (S - Y ∪ F))
(λi. if i ∈ Y ∧ i ∉ F then - ρ i - (∑s'∈S. τ i s' * ι i s') else 0) ;
Some (λs. if s ∈ Y then ennreal (sol s) else ∞)
}"

subsubsection ‹‹Sat››

fun Sat :: "'s sform ⇒ 's set option" where
"Sat true                   = Some S" |
"Sat (Label L)              = Some {s ∈ S. s ∈ L}" |
"Sat (Neg F)                = do { F ← Sat F ; Some (S - F) }" |
"Sat (And F1 F2)            = do { F1 ← Sat F1 ; F2 ← Sat F2 ; Some (F1 ∩ F2) }" |

"Sat (Prob rel r (X F))        = do { F ← Sat F ; Some {q ∈ S. inrealrel rel r (∑q'∈F. τ q q')} }" |
"Sat (Prob rel r (U k F1 F2))  = do { F1 ← Sat F1 ; F2 ← Sat F2 ; Some {q ∈ S. inrealrel rel r (ProbU q k F1 F2) } }" |
"Sat (Prob rel r (U⇧∞ F1 F2))   = do { F1 ← Sat F1 ; F2 ← Sat F2 ; P ← ProbUinfty F1 F2 ; Some {q ∈ S. inrealrel rel r (P q) } }" |

"Sat (Exp rel r (Cumm k))      = Some {s ∈ S. inrealrel rel r (ExpCumm s k) }" |
"Sat (Exp rel r (State k))     = Some {s ∈ S. inrealrel rel r (ExpState s k) }" |
"Sat (Exp rel r (Future F))    = do { F ← Sat F ; E ← ExpFuture F ; Some {q ∈ S. inrealrel rel (ennreal r) (E q) } }"

lemma prob_sum:
"s ∈ S ⟹ Measurable.pred R.S P ⟹ 𝒫(ω in T s. P ω) = (∑t∈S. τ s t * 𝒫(ω in T t. P (t ## ω)))"
unfolding prob_T using E_closed by (subst integral_measure_pmf[OF finite_S]) (auto simp: mult.commute)

lemma nn_integral_eq_sum:
"s ∈ S ⟹ f ∈ borel_measurable R.S ⟹ (∫⇧+x. f x ∂T s) = (∑t∈S. τ s t * (∫⇧+x. f (t ## x) ∂T t))"
unfolding nn_integral_T using E_closed
by (subst nn_integral_measure_pmf_support[OF finite_S])
(auto simp: mult.commute)

lemma T_space[simp]: "measure (T s) (space R.S) = 1"
using T.prob_space by simp

lemma emeasure_T_space[simp]: "emeasure (T s) (space R.S) = 1"
using T.emeasure_space_1 by simp

lemma τ_distr[simp]: "s ∈ S ⟹ (∑t∈S. τ s t) = 1"
using prob_sum[of s "λ_. True"] by simp

lemma ProbU:
"q ∈ S ⟹ ProbU q k (svalid F1) (svalid F2) = 𝒫(ω in T q. pvalid (U k F1 F2) (q ## ω))"
proof (induct k arbitrary: q)
case 0 with T.prob_space show ?case by simp
next
case (Suc k)

have "𝒫(ω in T q. pvalid (U (Suc k) F1 F2) (q ## ω)) =
(if q ∈ svalid F2 then 1 else if q ∈ svalid F1 then
∑t∈S. τ q t * 𝒫(ω in T t. pvalid (U k F1 F2) (t ## ω)) else 0)"
using ‹q ∈ S› by (subst prob_sum) simp_all
also have "… = ProbU q (Suc k) (svalid F1) (svalid F2)"
using Suc by simp
finally show ?case ..
qed

lemma Prob0_imp_not_Psi:
assumes "Φ ⊆ S" "Ψ ⊆ S" "s ∈ Prob0 Φ Ψ" shows "s ∉ Ψ"
proof -
have "s ∈ S" using ‹s ∈ Prob0 Φ Ψ› Prob0_subset_S by auto
with assms show ?thesis by (auto simp add: Prob0_iff suntil_Stream)
qed

lemma Psi_imp_not_Prob0:
assumes "Φ ⊆ S" "Ψ ⊆ S" shows "s ∈ Ψ ⟹ s ∉ Prob0 Φ Ψ"
using Prob0_imp_not_Psi[OF assms] by metis

subsubsection ‹Finite expected reward›

abbreviation "s0 ≡ SOME s. s ∈ S"

lemma s0_in_S: "s0 ∈ S"
using S_not_empty by (auto intro!: someI_ex[of "λx. x ∈ S"])

lemma nn_integral_reward_finite:
assumes "s ∈ S"
assumes until: "AE ω in T s. (HLD S suntil HLD (svalid F)) (s ## ω)"
shows "(∫⇧+ ω. reward (Future F) (s ## ω) ∂T s) ≠ ∞"
proof -
have "(∫⇧+ ω. reward (Future F) (s ## ω) ∂T s) = (∫⇧+ ω. reward_until (svalid F) s ω ∂T s)"
using until by (auto intro!: nn_integral_cong_AE ev_suntil)
also have "… ≠ ∞"
proof cases
assume "s ∉ svalid F"
show ?thesis
proof (rule nn_integral_reward_until_finite)
have "acc `` {s} ⊆ S"
using E_rtrancl_closed[of s _ _ E] ‹s ∈ S› by auto
then show "finite (acc `` {s})"
using finite_S by (auto dest: finite_subset)
show "AE ω in T s. (ev (HLD (svalid F))) ω"
using until by (auto simp add: suntil_Stream ‹s ∉ svalid F› intro: ev_suntil)
qed auto
qed simp
finally show ?thesis .
qed

lemma unique:
assumes in_S: "Φ ⊆ S" "Ψ ⊆ S" "N ⊆ S" "Prob0 Φ Ψ ⊆ N" "Ψ ⊆ N"
assumes l1: "⋀s. s ∈ S ⟹ s ∉ N ⟹ l1 s - c s = (∑s'∈S. τ s s' * l1 s')"
assumes l2: "⋀s. s ∈ S ⟹ s ∉ N ⟹ l2 s - c s = (∑s'∈S. τ s s' * l2 s')"
assumes eq: "⋀s. s ∈ N ⟹ l1 s = l2 s"
shows "∀s∈S. l1 s = l2 s"
proof
fix s assume "s ∈ S"
show "l1 s = l2 s"
proof cases
assume "s ∈ N" then show ?thesis
by (rule eq)
next
assume "s ∉ N"
show ?thesis
proof (rule unique_les[of _ "S - N" K N])
show "finite ((λx. l1 x - l2 x) ` (S - N ∪ N))" "(⋃x∈S - N. E x) ⊆ S - N ∪ N"
using E_closed finite_S ‹N ⊆ S› by (auto dest: finite_subset)
show "⋀s. s ∈ N ⟹ l1 s = l2 s" by fact
{ fix s assume "s ∈ S - N" with E_closed finite_S show "integrable (K s) l1" "integrable (K s) l2"
by (auto intro!: integrable_measure_pmf_finite dest: finite_subset)
obtain t where "(t ∈ Ψ ∧ (s, t) ∈ (Sigma Φ E)⇧*) ∨ s ∈ N"
using ‹s ∈ S - N› in_S(4) unfolding Prob0_iff_reachable[OF in_S(1,2)] by auto
moreover have "(Sigma Φ E)⇧* ⊆ acc"
by (intro rtrancl_mono Sigma_mono) auto
ultimately show "∃t∈N. (s, t) ∈ acc"
using ‹Ψ ⊆ N› by auto
show "l1 s = integral⇧L (K s) l1 + c s"
using E_closed l1 ‹s ∈ S - N›
by (subst integral_measure_pmf[OF finite_S]) (auto simp: subset_eq field_simps)
show "l2 s = integral⇧L (K s) l2 + c s"
using E_closed l2 ‹s ∈ S - N›
by (subst integral_measure_pmf[OF finite_S]) (auto simp: subset_eq field_simps) }
qed (insert ‹s ∉  N› ‹s ∈ S›, auto)
qed
qed

lemma uniqueness_of_ProbU:
assumes sol:
"∀s∈S. (∑s'∈S. LES (Prob0 (svalid F1) (svalid F2) ∪ svalid F2) s s' * l s') =
(if s ∈ svalid F2 then 1 else 0)"
shows "∀s∈S. l s = 𝒫(ω in T s. pvalid (U⇧∞ F1 F2) (s ## ω))"
proof (rule unique)
show "svalid F1 ⊆ S" "svalid F2 ⊆ S"
"Prob0 (svalid F1) (svalid F2) ⊆ Prob0 (svalid F1) (svalid F2) ∪ svalid F2"
"svalid F2 ⊆ Prob0 (svalid F1) (svalid F2) ∪ svalid F2"
"Prob0 (svalid F1) (svalid F2) ∪ svalid F2 ⊆ S"
using svalid_subset_S by (auto simp: Prob0_def)
next
fix s assume s: "s ∈ S" "s ∉ Prob0 (svalid F1) (svalid F2) ∪ svalid F2"
have "(∑s'∈S. (if s' = s then τ s s' - 1 else τ s s') * l s') =
(∑s'∈S. τ s s' * l s' - (if s' = s then 1 else 0) * l s')"
by (auto intro!: sum.cong simp: field_simps)
also have "… = (∑s'∈S. τ s s' * l s') - l s"
using ‹s ∈ S› by (simp add: sum_subtractf single_l)
finally show "l s - 0 = (∑s'∈S. τ s s' * l s')"
using sol[THEN bspec, of s] s by (simp add: LES_def)
next
fix s assume s: "s ∈ S" "s ∉ Prob0 (svalid F1) (svalid F2) ∪ svalid F2"
then show "𝒫(ω in T s. pvalid (U⇧∞ F1 F2) (s ## ω)) - 0 =
(∑t∈S. τ s t * 𝒫(ω in T t. pvalid (U⇧∞ F1 F2) (t ## ω)))"
unfolding Prob0_iff[OF svalid_subset_S svalid_subset_S]
by (subst prob_sum) (auto simp add: suntil_Stream)
next
fix s assume "s ∈ Prob0 (svalid F1) (svalid F2) ∪ svalid F2"
then show "l s = 𝒫(ω in T s. pvalid (U⇧∞ F1 F2) (s ## ω))"
proof
assume P0: "s ∈ Prob0 (svalid F1) (svalid F2)"
then have "s ∈ S" "AE ω in T s. ¬ (HLD (svalid F1) suntil HLD (svalid F2)) (s ## ω)"
unfolding Prob0_iff[OF svalid_subset_S svalid_subset_S] by auto
then have "𝒫(ω in T s. pvalid (U⇧∞ F1 F2) (s ## ω)) = 0"
by (intro T.prob_eq_0_AE) simp
moreover have "l s = 0"
using ‹s ∈ S› P0 sol[THEN bspec, of s] Prob0_subset_S
Prob0_imp_not_Psi[OF svalid_subset_S svalid_subset_S P0]
by (auto simp: LES_def single_l split: if_split_asm)
ultimately show "l s = 𝒫(ω in T s. pvalid (U⇧∞ F1 F2) (s ## ω))" by simp
next
assume s: "s ∈ svalid F2"
moreover with svalid_subset_S have "s ∈ S" by auto
moreover note Psi_imp_not_Prob0[OF svalid_subset_S svalid_subset_S s]
ultimately have "l s = 1"
using sol[THEN bspec, of s]
by (auto simp: LES_def single_l dest: Psi_imp_not_Prob0[OF svalid_subset_S svalid_subset_S])
then show "l s = 𝒫(ω in T s. pvalid (U⇧∞ F1 F2) (s ## ω))"
using s by (simp add: suntil_Stream)
qed
qed

lemma infinite_reward:
fixes s F
defines "N ≡ Prob0 S (svalid F)" (is "_ ≡ Prob0 S ?F")
defines "Y ≡ Prob1 N S (svalid F)"
assumes s: "s ∈ S" "s ∉ Y"
shows "(∫⇧+ω. reward (Future F) (s ## ω) ∂T s) = ∞"
proof -
{ assume "(AE ω in T s. ev (HLD ?F) ω)"
with AE_T_enabled have "(AE ω in T s. (HLD S suntil HLD ?F) ω)"
proof eventually_elim
fix ω assume "ev (HLD ?F) ω" "enabled s ω"
from this ‹s ∈ S› show "(HLD S suntil HLD ?F) ω"
proof (induction arbitrary: s)
case (step ω) show ?case
using E_closed step.IH[of "shd ω"] step.prems
by (auto simp: subset_eq enabled.simps[of s] suntil.simps[of _ _ ω] HLD_iff)
qed (auto intro: suntil.intros)
qed }
moreover have "¬ (AE ω in T s. (HLD S suntil HLD ?F) (s ## ω))"
using s svalid_subset_S unfolding N_def Y_def by (simp add: Prob1_iff)
ultimately have *: "¬ (AE ω in T s. ev (HLD ?F) (s ## ω))"
using ‹s ∈ S› by (cases "s ∈ ?F") (auto simp add: suntil_Stream ev_Stream)

show ?thesis
proof (rule ccontr)
assume "¬ ?thesis"
from nn_integral_PInf_AE[OF _ this] ‹s∈S›
have "AE ω in T s. ev (HLD ?F) (s ## ω)"
by (simp split: if_split_asm)
with * show False ..
qed
qed

subsubsection ‹The expected reward implies a unique LES›

lemma existence_of_ExpFuture:
fixes s F
assumes N_def: "N ≡ Prob0 S (svalid F)" (is "_ ≡ Prob0 S ?F")
assumes Y_def: "Y ≡ Prob1 N S (svalid F)"
assumes s: "s ∈ S" "s ∉ S - (Y - ?F)"
shows "enn2real (∫⇧+ω. reward (Future F) (s ## ω) ∂T s) - (ρ s + (∑s'∈S. τ s s' * ι s s')) =
(∑s'∈S. τ s s' * enn2real (∫⇧+ω. reward (Future F) (s' ## ω) ∂T s'))"
proof -
let ?R = "reward (Future F)"

from s have "s ∈ Prob1 (Prob0 S ?F) S ?F"
unfolding Y_def N_def by auto
then have AE_until: "AE ω in T s. (HLD S suntil HLD (svalid F)) (s ## ω)"
using Prob1_iff[of S ?F] svalid_subset_S by auto

from s have "s ∉ ?F" by auto

let ?E = "λs'. ∫⇧+ ω. reward (Future F) (s' ## ω) ∂T s'"
have *: "(∑s'∈S. τ s s' * ?E s') = (∑s'∈S. ennreal (τ s s' * enn2real (?E s')))"
proof (rule sum.cong)
fix s' assume "s' ∈ S"
show "τ s s' * ?E s' = ennreal (τ s s' * enn2real (?E s'))"
proof cases
assume "τ s s' ≠ 0"
with ‹s ∈ S› ‹s' ∈ S› have "s' ∈ E s" by (simp add: set_pmf_iff)
from ‹s ∉ ?F› AE_until have "AE ω in T s. (HLD S suntil HLD ?F) (s ## ω)"
using svalid_subset_S ‹s ∈ S› by simp
with nn_integral_reward_finite[OF ‹s' ∈ S›, of F] ‹s ∈ S› ‹s' ∈ E s› ‹s ∉ ?F›
have "?E s' ≠ ∞"
by (simp add: AE_T_iff[of _ s] AE_measure_pmf_iff suntil_Stream
del: reward.simps)
then show ?thesis by (cases "?E s'") (auto simp: ennreal_mult)
qed simp
qed simp

have "AE ω in T s. ?R (s ## ω) = ρ s + ι s (shd ω) + ?R ω"
using ‹s ∉ svalid F› by (auto simp: ev_Stream )
then have "(∫⇧+ω. ?R (s ## ω) ∂T s) = (∫⇧+ω. (ρ s + ι s (shd ω)) + ?R ω ∂T s)"
by (rule nn_integral_cong_AE)
also have "… = (∫⇧+ω. ρ s + ι s (shd ω) ∂T s) +
(∫⇧+ω. ?R ω ∂T s)"
using ‹s ∈ S›
by (subst nn_integral_add)
(auto simp add: space_PiM PiE_iff simp del: reward.simps)
also have "… = ennreal (ρ s + (∑s'∈S. τ s s' * ι s s')) + (∫⇧+ω. ?R ω ∂T s)"
using ‹s ∈ S›
by (subst nn_integral_eq_sum)
(auto simp: field_simps sum.distrib sum_distrib_left[symmetric] ennreal_mult[symmetric] sum_nonneg)
finally show ?thesis
apply (simp del: reward.simps)
apply (subst nn_integral_eq_sum[OF ‹s ∈ S› reward_measurable])
apply (simp del: reward.simps ennreal_plus add: * ennreal_plus[symmetric] sum_nonneg)
done
qed

lemma uniqueness_of_ExpFuture:
fixes F
assumes N_def: "N ≡ Prob0 S (svalid F)" (is "_ ≡ Prob0 S ?F")
assumes Y_def: "Y ≡ Prob1 N S (svalid F)"
assumes const_def: "const ≡ λs. if s ∈ Y ∧ s ∉ svalid F then - ρ s - (∑s'∈S. τ s s' * ι s s') else 0"
assumes sol: "⋀s. s∈S ⟹ (∑s'∈S. LES (S - Y ∪ ?F) s s' * l s') = const s"
shows "∀s∈S. l s = enn2real (∫⇧+ω. reward (Future F) (s ## ω) ∂T s)"
(is "∀s∈S. l s = enn2real (∫⇧+ω. ?R (s ## ω) ∂T s)")
proof (rule unique)
show "S ⊆ S" "?F ⊆ S" using svalid_subset_S by auto
show "S - (Y - ?F) ⊆ S" "Prob0 S ?F ⊆ S - (Y - ?F)" "?F ⊆ S - (Y - ?F)"
using svalid_subset_S
by (auto simp add: Y_def N_def Prob1_iff)
(auto simp add: Prob0_iff dest!: T.AE_contr)
next
fix s assume "s ∈ S" "s ∉ S - (Y - ?F)"
then show "enn2real (∫⇧+ω. ?R (s ## ω) ∂T s) - (ρ s + (∑s'∈S. τ s s' * ι s s')) =
(∑s'∈S. τ s s' * enn2real (∫⇧+ω. ?R (s' ## ω) ∂T s'))"
by (rule existence_of_ExpFuture[OF N_def Y_def])
next
fix s assume "s ∈ S" "s ∉ S - (Y - ?F)"
then have "s ∈ Y" "s ∉ ?F" by auto
have "(∑s'∈S. (if s' = s then τ s s' - 1 else τ s s') * l s') =
(∑s'∈S. τ s s' * l s' - (if s' = s then 1 else 0) * l s')"
by (auto intro!: sum.cong simp: field_simps)
also have "… = (∑s'∈S. τ s s' * l s') - l s"
using ‹s ∈ S› by (simp add: sum_subtractf single_l)
finally have "l s = (∑s'∈S. τ s s' * l s') - (∑s'∈S. (if s' = s then τ s s' - 1 else τ s s') * l s')"
by (simp add: field_simps)
then show "l s - (ρ s + (∑s'∈S. τ s s' * ι s s')) = (∑s'∈S. τ s s' * l s')"
using sol[OF ‹s ∈ S›] ‹s ∈ Y› ‹s ∉ ?F› by (simp add: const_def LES_def)
next
fix s assume s: "s ∈ S - (Y - ?F)"
with sol[of s] have "l s = 0"
by (cases "s ∈ ?F") (simp_all add: const_def LES_def single_l)
also have "0 = enn2real (∫⇧+ω. reward (Future F) (s ## ω) ∂T s)"
proof cases
assume "s ∈ ?F" then show ?thesis
by (simp add: HLD_iff ev_Stream)
next
assume "s ∉ ?F"
with s have "s ∈ S - Y" by auto
with infinite_reward[of s F] show ?thesis
by (simp add: Y_def N_def del: reward.simps)
qed
finally show "l s = enn2real (∫⇧+ω. ?R (s ## ω) ∂T s)" .
qed

subsection ‹Soundness of @{const Sat}›

theorem Sat_sound:
"Sat F ≠ None ⟹ Sat F = Some (svalid F)"
proof (induct F rule: Sat.induct)
case (5 rel r F)
{ fix q assume "q ∈ S"
with svalid_subset_S have "sum (τ q) (svalid F) = 𝒫(ω in T q. HLD (svalid F) ω)"
by (subst prob_sum[OF ‹q∈S›]) (auto intro!: sum.mono_neutral_cong_left) }
with 5 show ?case
by (auto split: bind_split_asm)

next
case (6 rel r k F1 F2)
then show ?case
by (simp add: ProbU cong: conj_cong split: bind_split_asm)

next
case (7 rel r F1 F2)
moreover
define constants :: "'s ⇒ real" where "constants = (λs. if s ∈ (svalid F2) then 1 else 0)"
moreover define distr where "distr = LES (Prob0 (svalid F1) (svalid F2) ∪ svalid F2)"
ultimately obtain l where eq: "Sat F1 = Some (svalid F1)" "Sat F2 = Some (svalid F2)"
and l: "gauss_jordan' distr constants = Some l"
by atomize_elim (simp add: ProbUinfty_def split: bind_split_asm)

from l have P: "ProbUinfty (svalid F1) (svalid F2) = Some l"
unfolding ProbUinfty_def constants_def distr_def by simp

have "∀s∈S. l s = 𝒫(ω in T s. pvalid (U⇧∞ F1 F2) (s ## ω))"
proof (rule uniqueness_of_ProbU)
show "∀s∈S. (∑s'∈S. LES (Prob0 (svalid F1) (svalid F2) ∪ svalid F2) s s' * l s') =
(if s ∈ svalid F2 then 1 else 0)"
using gauss_jordan'_correct[OF l]
unfolding distr_def constants_def by simp
qed
then show ?case
by (auto simp add: eq P)
next
case (8 rel r k)
{ fix s assume "s ∈ S"
then have "ExpCumm s k = (∫⇧+ x. ennreal (∑i<k. ρ ((s ## x) !! i) + ι ((s ## x) !! i) (x !! i)) ∂T s)"
proof (induct k arbitrary: s)
case 0 then show ?case by simp
next
case (Suc k)
have "(∫⇧+ω. ennreal (∑i<Suc k. ρ ((s ## ω) !! i) + ι ((s ## ω) !! i) (ω !! i)) ∂T s)
= (∫⇧+ω. ennreal (ρ s + ι s (ω !! 0)) + ennreal (∑i<k. ρ (ω !! i) + ι (ω !! i) (ω !! (Suc i))) ∂T s)"
by (auto intro!: nn_integral_cong
simp del: ennreal_plus
simp: ennreal_plus[symmetric] sum_nonneg sum.reindex lessThan_Suc_eq_insert_0 zero_notin_Suc_image)
also have "… = (∫⇧+ω. ρ s + ι s (ω !! 0) ∂T s) +
(∫⇧+ω. (∑i<k. ρ (ω !! i) + ι (ω !! i) (ω !! (Suc i))) ∂T s)"
using ‹s ∈ S›
by (intro nn_integral_add AE_I2) (auto simp: sum_nonneg)
also have "… = (∑s'∈S. τ s s' * (ρ s + ι s s')) +
(∫⇧+ω. (∑i<k. ρ (ω !! i) + ι (ω !! i) (ω !! (Suc i))) ∂T s)"
using ‹s ∈ S› by (subst nn_integral_eq_sum)
(auto simp del: ennreal_plus simp: ennreal_plus[symmetric] ennreal_mult[symmetric] sum_nonneg)
also have "… = (∑s'∈S. τ s s' * (ρ s + ι s s')) +
(∑s'∈S. τ s s' * ExpCumm s' k)"
using ‹s ∈ S› by (subst nn_integral_eq_sum) (auto simp: Suc)
also have "… = ExpCumm s (Suc k)"
using ‹s ∈ S›
by (simp add: field_simps sum.distrib sum_distrib_left[symmetric] ennreal_mult[symmetric]
ennreal_plus[symmetric] sum_nonneg del: ennreal_plus)
finally show ?case by simp
qed }
then show ?case by auto

next
case (9 rel r k)
{ fix s assume "s ∈ S"
then have "ExpState s k = (∫⇧+ x. ennreal (ρ ((s ## x) !! k)) ∂T s)"
proof (induct k arbitrary: s)
case (Suc k) then show ?case by (simp add: nn_integral_eq_sum[of s])
qed simp }
then show ?case by auto

next
case (10 rel r F)
moreover
let ?F = "svalid F"
define N where "N ≡ Prob0 S ?F"
moreover define Y where "Y ≡ Prob1 N S ?F"
moreover define const where "const ≡ (λs. if s ∈ Y ∧ s ∉ ?F then - ρ s - (∑s'∈S. τ s s' * ι s s') else 0)"
ultimately obtain l
where l: "gauss_jordan' (LES (S - Y ∪ ?F)) const = Some l"
and F: "Sat F = Some ?F"
by (auto simp: ExpFuture_def Let_def split: bind_split_asm)

from l have EF: "ExpFuture ?F =
Some (λs. if s ∈ Y then ennreal (l s) else ∞)"
unfolding ExpFuture_def N_def Y_def const_def by auto

let ?R = "reward (Future F)"
have l_eq: "∀s∈S. l s = enn2real (∫⇧+ω. ?R (s ## ω) ∂T s)"
proof (rule uniqueness_of_ExpFuture[OF N_def Y_def const_def])
fix s assume "s ∈ S"
show "⋀s. s∈S ⟹ (∑s'∈S. LES (S - Y ∪ ?F) s s' * l s') = const s"
using gauss_jordan'_correct[OF l] by auto
qed
{ fix s assume [simp]: "s ∈ S" "s ∈ Y"
then have "s ∈ Prob1 (Prob0 S ?F) S ?F"
unfolding Y_def N_def by auto
then have "AE ω in T s. (HLD S suntil HLD ?F) (s ## ω)"
using svalid_subset_S by (auto simp add: Prob1_iff)
from nn_integral_reward_finite[OF ‹s ∈ S›] this
have "(∫⇧+ω. reward (Future F) (s ## ω) ∂T s) ≠ ∞"
by simp
with l_eq ‹s ∈ S› have "(∫⇧+ω. reward (Future F) (s ## ω) ∂T s) = ennreal (l s)"
by (auto simp: less_top) }
moreover
{ fix s assume "s ∈ S" "s ∉ Y"
with infinite_reward[of s F]
have "(∫⇧+ω. reward (Future F) (s ## ω) ∂T s) = ∞"
by (simp add: Y_def N_def) }
ultimately show ?case
apply (auto simp add: EF F simp del: reward.simps)
apply (case_tac "x ∈ Y")
apply auto
done
qed (auto split: bind_split_asm)

subsection ‹Completeness of @{const Sat}›

theorem Sat_complete:
"Sat F ≠ None"
proof (induct F rule: Sat.induct)
case (7 r rel Φ Ψ)
then have F: "Sat Φ = Some (svalid Φ)" "Sat Ψ = Some (svalid Ψ)"
by (auto intro!: Sat_sound)

define constants :: "'s ⇒ real" where "constants = (λs. if s ∈ svalid Ψ then 1 else 0)"
define distr where "distr = LES (Prob0 (svalid Φ) (svalid Ψ) ∪ svalid Ψ)"
have "∃l. gauss_jordan' distr constants = Some l"
proof (rule gauss_jordan'_complete[OF _ uniqueness_of_ProbU])
show "∀s∈S. (∑s'∈S. distr s s' * 𝒫(ω in T s'. pvalid (U⇧∞ Φ Ψ) (s' ## ω))) = constants s"
apply (simp add: distr_def constants_def LES_def del: pvalid.simps space_T)
proof safe
fix s assume "s ∈ svalid Ψ" "s ∈ S"
then show "(∑s'∈S. (if s' = s then 1 else 0) * 𝒫(ω in T s'. pvalid (U⇧∞ Φ Ψ) (s' ## ω))) = 1"
by (simp add: single_l suntil_Stream)
next
fix s assume s: "s ∉ svalid Ψ" "s ∈ S"
let ?x = "λs'. 𝒫(ω in T s'. pvalid (U⇧∞ Φ Ψ) (s' ## ω))"
show "(∑s'∈S. (if s ∈ Prob0 (svalid Φ) (svalid Ψ) then if s' = s then 1 else 0 else if s' = s then τ s s' - 1 else τ s s') * ?x s') = 0"
proof cases
assume "s ∈ Prob0 (svalid Φ) (svalid Ψ)"
with s show ?thesis
by (simp add: single_l Prob0_iff svalid_subset_S T.prob_eq_0_AE del: space_T)
next
assume s_not_0: "s ∉ Prob0 (svalid Φ) (svalid Ψ)"
with s have *:"⋀s' ω. s' ∈ S ⟹ pvalid (U⇧∞ Φ Ψ) (s ## s' ## ω) = pvalid (U⇧∞ Φ Ψ) (s' ## ω)"
by (auto simp: suntil_Stream Prob0_iff svalid_subset_S)

have "(∑s'∈S. (if s' = s then τ s s' - 1 else τ s s') * ?x s') =
(∑s'∈S. τ s s' * ?x s' - (if s' = s then 1 else 0) * ?x s')"
by (auto intro!: sum.cong simp: field_simps)
also have "… = (∑s'∈S. τ s s' * ?x s') - ?x s"
using s by (simp add: single_l sum_subtractf)
finally show ?thesis
using * prob_sum[OF ‹s ∈ S›] s_not_0 by (simp del: pvalid.simps)
qed
qed
qed (simp add: distr_def constants_def)
then have P: "∃l. ProbUinfty (svalid Φ) (svalid Ψ) = Some l"
unfolding ProbUinfty_def constants_def distr_def by simp
with F show ?case
by auto
next
case (10 rel r Φ)
then have F: "Sat Φ = Some (svalid Φ)"
by (auto intro!: Sat_sound)

let ?F = "svalid Φ"
define N where "N ≡ Prob0 S ?F"
define Y where "Y ≡ Prob1 N S ?F"
define const where "const ≡ (λs. if s ∈ Y ∧ s ∉ ?F then - ρ s - (∑s'∈S. τ s s' * ι s s') else 0)"
let ?E = "λs'. ∫⇧+ ω. reward (Future Φ) (s' ## ω) ∂T s'"
have "∃l. gauss_jordan' (LES (S - Y ∪ ?F)) const = Some l"
proof (rule gauss_jordan'_complete[OF _ uniqueness_of_ExpFuture[OF N_def Y_def const_def]])
show "∀s∈S. (∑s'∈S. LES (S - Y ∪ svalid Φ) s s' * enn2real (?E s')) = const s"
proof
fix s assume "s ∈ S"
show "(∑s'∈S. LES (S - Y ∪ svalid Φ) s s' * enn2real (?E s')) = const s"
proof cases
assume s: "s ∈ S - (Y - svalid Φ)"
show ?thesis
proof cases
assume "s ∈ Y"
with ‹s ∈ S› s ‹s ∈ Y› show ?thesis
by (simp add: LES_def const_def single_l ev_Stream)
next
assume "s ∉ Y"
with infinite_reward[of s Φ] Y_def N_def s ‹s ∈ S›
show ?thesis by (simp add: const_def LES_def single_l del: reward.simps)
qed
next
assume s: "s ∉ S - (Y - svalid Φ)"

have "(∑s'∈S. (if s' = s then τ s s' - 1 else τ s s') * enn2real (?E s')) =
(∑s'∈S. τ s s' * enn2real (?E s') - (if s' = s then 1 else 0) * enn2real (?E s'))"
by (auto intro!: sum.cong simp: field_simps)
also have "… = (∑s'∈S. τ s s' * enn2real (?E s')) - enn2real (?E s)"
using ‹s ∈ S› by (simp add: sum_subtractf single_l)
finally show ?thesis
using s ‹s ∈ S› existence_of_ExpFuture[OF N_def Y_def ‹s ∈ S› s]
by (simp add: LES_def const_def del: reward.simps)
qed
qed
qed simp
then have P: "∃l. ExpFuture (svalid Φ) = Some l"
unfolding ExpFuture_def const_def N_def Y_def by auto
with F show ?case
by auto
qed (force split: bind_split)+

subsection ‹Completeness and Soundness @{const Sat}›

corollary Sat: "Sat Φ = Some (svalid Φ)"
using Sat_sound Sat_complete by auto

end

end
```