(* 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  :: "nat → 's"
  where "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 P(ψ 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^\<infinity> F1 F2) = HLD (svalid F1) suntil HLD (svalid F2)" |

"reward (C^\<le> 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)<sup>*</sup> `` {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)<sup>*</sup> `` {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)<sup>*</sup> `` {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)<sup>*</sup>"
      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)<sup>*</sup> `` {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^\<infinity> 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 ==> P(ψ in T s. P ψ) = (∑t∈S. τ s t * P(ψ 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) = P(ψ 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 "P(ψ 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 * P(ψ 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 = P(ψ in T s. pvalid (U^\<infinity> 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 "P(ψ in T s. pvalid (U^\<infinity> F1 F2) (s ## ψ)) - 0 =
    (∑t∈S. τ s t * P(ψ in T t. pvalid (U^\<infinity> 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 = P(ψ in T s. pvalid (U^\<infinity> 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 "P(ψ in T s. pvalid (U^\<infinity> 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 = P(ψ in T s. pvalid (U^\<infinity> 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 = P(ψ in T s. pvalid (U^\<infinity> 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) = P(ψ 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 = P(ψ in T s. pvalid (U^\<infinity> 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' * P(ψ in T s'. pvalid (U^\<infinity> Φ Ψ) (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) * P(ψ in T s'. pvalid (U^\<infinity> Φ Ψ) (s' ## ψ))) = 1"
        by (simp add: single_l suntil_Stream)
    next
      fix s assume s: "s ∉ svalid Ψ" "s ∈ S"
      let ?x = "λs'. P(ψ in T s'. pvalid (U^\<infinity> Φ Ψ) (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^\<infinity> Φ Ψ) (s ## s' ## ψ) = pvalid (U^\<infinity> Φ Ψ) (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