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: "(sS. 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 "sS. (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: "sS. (s'S. M s s' * x s') = a s"
  assumes unique: "y. sS. (s'S. M s s' * y s') = a s  sS. 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 "  (sS. (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 
      (sS. (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 "sS. (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) {xspace (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 Φ Ψ = {sS. 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 Φ Ψ) Φ Ψ = {sS. AE ω in T s. (HLD Φ suntil HLD Ψ) (s ## ω)}"
    (is "Prob1 ?P0 _ _ = {sS. ?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 " = {sS. 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 tS 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 ω) = (tS. τ 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) = (tS. τ 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  (tS. τ 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
      tS. τ 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 "sS. 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))" "(xS - 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 "tN. (s, t)  acc"
          using Ψ  N by auto
        show "l1 s = integralL (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 = integralL (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:
    "sS. (s'S. LES (Prob0 (svalid F1) (svalid F2)  svalid F2) s s' * l s') =
      (if s  svalid F2 then 1 else 0)"
  shows "sS. 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 =
    (tS. τ 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] sS
    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. sS  (s'S. LES (S - Y  ?F) s s' * l s') = const s"
  shows "sS. l s = enn2real (+ω. reward (Future F) (s ## ω) T s)"
    (is "sS. 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 qS]) (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 "sS. l s = 𝒫(ω in T s. pvalid (U F1 F2) (s ## ω))"
  proof (rule uniqueness_of_ProbU)
    show "sS. (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: "sS. 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. sS  (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 "sS. (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 "sS. (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