Theory PTA

theory PTA
  imports "library/Lib"
begin

section ‹Bisimulation on a Relation› text_raw ‹\label{thm:bisim}›

definition rel_set_strong :: "('a  'b  bool)  'a set  'b set  bool"
  where "rel_set_strong R A B  (x y. R x y  (x  A  y  B))"

lemma T_eq_rel_half[consumes 4, case_names prob sets cont]:
  fixes R :: "'s  't  bool" and f :: "'s  't" and S :: "'s set"
  assumes R_def: "s t. R s t  (s  S  f s = t)"
  assumes A[measurable]: "A  sets (stream_space (count_space UNIV))"
    and B[measurable]: "B  sets (stream_space (count_space UNIV))"
    and AB: "rel_set_strong (stream_all2 R) A B" and KL: "rel_fun R (rel_pmf R) K L" and xy: "R x y"
  shows "MC_syntax.T K x A = MC_syntax.T L y B"
proof -
  interpret K: MC_syntax K by unfold_locales
  interpret L: MC_syntax L by unfold_locales

  have "x  S" using R x y by (auto simp: R_def)

  define g where "g t = (SOME s. R s t)" for t
  have measurable_g: "g  count_space UNIV M count_space UNIV" by auto
  have g: "R i j  R (g j) j" for i j
    unfolding g_def by (rule someI)
  
  have K_subset: "x  S  K x  S" for x
    using KL[THEN rel_funD, of x "f x", THEN rel_pmf_imp_rel_set] by (auto simp: rel_set_def R_def)

  have in_S: "AE ω in K.T x. ω  streams S"
    using K.AE_T_enabled
  proof eventually_elim 
    case (elim ω) with x  S show ?case
      apply (coinduction arbitrary: x ω)
      subgoal for x ω using K_subset by (cases ω) (auto simp: K.enabled_Stream)
      done
  qed

  have L_eq: "L y = map_pmf f (K x)" if xy: "R x y" for x y
  proof -
    have "rel_pmf (λx y. x = y) (map_pmf f (K x)) (L y)"
      using KL[THEN rel_funD, OF xy] by (auto intro: pmf.rel_mono_strong simp: R_def pmf.rel_map)
    then show ?thesis unfolding pmf.rel_eq by simp
  qed

  let ?D = "λx. distr (K.T x) K.S (smap f)"
  have prob_space_D: "?D x  space (prob_algebra K.S)" for x 
    by (auto simp: space_prob_algebra K.T.prob_space_distr)

  have D_eq_D: "?D x = ?D x'" if "R x y" "R x' y" for x x' y
  proof (rule stream_space_eq_sstart)
    define A where "A = K.acc `` {x, x'}"
    have x_A: "x  A" "x'  A" by (auto simp: A_def)
    let  = "f ` A"
    show "countable "
      unfolding A_def by (intro countable_image K.countable_acc) auto
    show "prob_space (?D x)" "prob_space (?D x')" by (auto intro!: K.T.prob_space_distr)
    show "sets (?D x) = sets L.S" "sets (?D x') = sets L.S" by auto
    have AE_streams: "AE x in ?D x''. x  streams " if "x''  A" for x''
      apply (simp add: space_stream_space streams_sets AE_distr_iff)
      using K.AE_T_reachable[of x''] unfolding alw_HLD_iff_streams
    proof eventually_elim
      fix s assume "s  streams (K.acc `` {x''})"
      moreover have "K.acc `` {x''}  A"
        using x''  A by (auto simp: A_def Image_def intro: rtrancl_trans)
      ultimately show "smap f s  streams (f ` A)"
        by (auto intro: smap_streams)
    qed
    with x_A show "AE x in ?D x'. x  streams " "AE x in ?D x. x  streams "
      by auto
    from x  A x'  A that show "?D x (sstart (f ` A) xs) = ?D x' (sstart (f ` A) xs)" for xs
    proof (induction xs arbitrary: x x' y)
      case Nil
      moreover have "?D x (streams (f ` A)) = 1" if "x  A" for x
        using AE_streams[of x] that
        by (intro prob_space.emeasure_eq_1_AE[OF K.T.prob_space_distr]) (auto simp: streams_sets)
      ultimately show ?case by simp
    next
      case (Cons z zs x x' y)
      have "rel_pmf (R OO R¯¯) (K x) (K x')"
        using KL[THEN rel_funD, OF Cons(4)] KL[THEN rel_funD, OF Cons(5)]
        unfolding pmf.rel_compp pmf.rel_flip by auto
      then obtain p :: "('s × 's) pmf" where p: "a b. (a, b)  p  (R OO R¯¯) a b" and
        eq: "map_pmf fst p = K x" "map_pmf snd p = K x'"
        by (auto simp: pmf.in_rel)
      let ?S = "stream_space (count_space UNIV)"
      have *: "(##) y -` smap f -` sstart (f ` A) (z # zs) = (if f y = z then smap f -` sstart (f ` A) zs else {})" for y z zs
        by auto
      have **: "?D x (sstart (f ` A) (z # zs)) = (+ y'. (if f y' = z then ?D y' (sstart (f ` A) zs) else 0) K x)" for x
        apply (simp add: emeasure_distr)
        apply (subst K.T_eq_bind)
        apply (subst emeasure_bind[where N="?S"])
           apply simp
          apply (rule measurable_distr2[where M="?S"])
           apply measurable
        apply (intro nn_integral_cong_AE AE_pmfI)
        apply (auto simp add: emeasure_distr)
        apply (simp_all add: * space_stream_space)
        done
      have fst_A: "fst ab  A" if "ab  p" for ab
      proof -
        have "fst ab  K x" using ab  p set_map_pmf [of fst p] by (auto simp: eq)
        with x  A show "fst ab  A"
          by (auto simp: A_def intro: rtrancl.rtrancl_into_rtrancl)
      qed
      have snd_A: "snd ab  A" if "ab  p" for ab
      proof -
        have "snd ab  K x'" using ab  p set_map_pmf [of snd p] by (auto simp: eq)
        with x'  A show "snd ab  A"
          by (auto simp: A_def intro: rtrancl.rtrancl_into_rtrancl)
      qed
      show ?case
        unfolding ** eq[symmetric] nn_integral_map_pmf
        apply (intro nn_integral_cong_AE AE_pmfI)
        subgoal for ab using p[of "fst ab" "snd ab"] by (auto simp: R_def intro!: Cons(1) fst_A snd_A)
        done
    qed
  qed

  have L_eq_D: "L.T y = ?D x"
    using R x y
  proof (coinduction arbitrary: x y rule: L.T_coinduct)
    case (cont x y)
    then have Kx_Ly: "rel_pmf R (K x) (L y)"
      by (rule KL[THEN rel_funD])
    then have *: "y'  L y  x'K x. R x' y'" for y'
      by (auto dest!: rel_pmf_imp_rel_set simp: rel_set_def)
    have **: "y'  L y  R (g y') y'" for y'
      using *[of y'] unfolding g_def by (auto intro: someI)

    have D_SCons_eq_D_D: "distr (K.T i) K.S (λx. z ## smap f x) = distr (?D i) K.S (λx. z ## x)" for i z
      by (subst distr_distr) (auto simp: comp_def)
    have D_eq_D_gi: "?D i = ?D (g (f i))" if i: "i  K x" for i
    proof -
      obtain j where "j  L y" "R i j" "f i = j"
        using Kx_Ly i by (force dest!: rel_pmf_imp_rel_set simp: rel_set_def R_def)
      then show ?thesis
        by (auto intro!: D_eq_D[OF R i j] g)
    qed

    have ***: "?D x = measure_pmf (L y)  (λy. distr (?D (g y)) K.S ((##) y))"
      apply (subst K.T_eq_bind)
      apply (subst distr_bind[of _ _ K.S])
         apply (rule measurable_distr2[of _  _ "K.S"])
          apply (simp_all add: Pi_iff)
      apply (simp add: distr_distr comp_def L_eq[OF cont] map_pmf_rep_eq)
      apply (subst bind_distr[where K=K.S])
         apply measurable []
        apply (rule measurable_distr2[of _  _ "K.S"])
        apply measurable []
        apply (rule measurable_compose[OF measurable_g])
        apply measurable []
       apply simp
      apply (rule bind_measure_pmf_cong[where N="K.S"])
        apply (auto simp: space_subprob_algebra space_stream_space intro!: K.T.subprob_space_distr)
        unfolding D_SCons_eq_D_D D_eq_D_gi ..
    show ?case
      by (intro exI[of _ "λt. distr (K.T (g t)) (stream_space (count_space UNIV)) (smap f)"])
         (auto simp add: K.T.prob_space_distr *** dest: **)
  qed (auto intro: K.T.prob_space_distr)

  have "stream_all2 R s t  (s  streams S  smap f s = t)" for s t 
  proof safe
    show "stream_all2 R s t  s  streams S"
      apply (coinduction arbitrary: s t)
      subgoal for s t by (cases s; cases t) (auto simp: R_def)
      done
    show "stream_all2 R s t  smap f s = t"
      apply (coinduction arbitrary: s t rule: stream.coinduct)
      subgoal for s t by (cases s; cases t) (auto simp: R_def)
      done
  qed (auto intro!: stream.rel_refl_strong simp: stream.rel_map R_def streams_iff_sset)
  then have "ω  streams S  ω  A  smap f ω  B" for ω
    using AB by (auto simp: rel_set_strong_def)
  with in_S have "K.T x A = K.T x (smap f -` B  space (K.T x))"
    by (auto intro!: emeasure_eq_AE streams_sets)
  also have " = (distr (K.T x) K.S (smap f)) B"
    by (intro emeasure_distr[symmetric]) auto
  also have " = (L.T y) B" unfolding L_eq_D ..
  finally show ?thesis .
qed

no_notation ccval ("_" [100])

hide_const succ


section ‹Additional Facts on Regions›

(* XXX Move this to a theory on Timed Automata *)
declare reset_set11[simp] reset_set1[simp]

text ‹
  Defining the closest successor of a region. Only exists if at least one interval is upper-bounded.
›

abbreviation is_upper_right where
  "is_upper_right R  ( t  0.  u  R. u  t  R)"

(* XXX Remove old successor definition *)
definition
  "succ  R 
  if is_upper_right R then R else
  (THE R'. R'  R  R'  Succ  R  ( u  R.  t  0. (u  t)  R  ( t'  t. (u  t')  R'  0  t')))"

lemma region_continuous:
  assumes "valid_region X k I r"
  defines R: "R  region X I r"
  assumes between: "0  t1" "t1  t2"
  assumes elem: "u  R" "u  t2  R"
  shows "u  t1  R"
unfolding R
proof
  from 0  t1 u  R show "xX. 0  (u  t1) x" by (auto simp: R cval_add_def)

  have "intv_elem x (u  t1) (I x)" if "x  X" for x
  proof -
    from elem that have "intv_elem x u (I x)" "intv_elem x (u  t2) (I x)" by (auto simp: R)
    with between show ?thesis by (cases "I x", auto simp: cval_add_def)
  qed
  then show " x  X. intv_elem x (u  t1) (I x)" by blast

  let ?X0 = "{x  X. d. I x = Intv d}"
  show "?X0 = ?X0" ..

  from elem have " x  ?X0.  y  ?X0. (x, y)  r  frac (u x)  frac (u y)" by (auto simp: R)
  moreover
  { fix x y c d assume A: "x  X" "y  X" "I x = Intv c" "I y = Intv d"
    from A elem between have *:
      "c < u x" "u x < c + 1" "c < u x + t1" "u x + t1 < c + 1"
    by (fastforce simp: cval_add_def R)+
    moreover from A(2,4) elem between have **:
      "d < u y" "u y < d + 1" "d < u y + t1" "u y + t1 < d + 1"
    by (fastforce simp: cval_add_def R)+
    ultimately have "u x = c + frac (u x)" "u y = d + frac (u y)" using nat_intv_frac_decomp by auto
    then have
      "frac (u x + t1) = frac (u x) + t1" "frac (u y + t1) = frac (u y) + t1"
    using *(3,4) **(3,4) nat_intv_frac_decomp by force+
    then have
      "frac (u x)  frac (u y)  frac ((u  t1) x)  frac ((u  t1) y)"
    by (auto simp: cval_add_def)
  }
  ultimately show
    " x  ?X0.  y  ?X0. (x, y)  r  frac ((u  t1) x)  frac ((u  t1) y)"
  by (auto simp: cval_add_def)
qed

lemma upper_right_eq:
  assumes "finite X" "valid_region X k I r"
  shows "( x  X. isGreater (I x))  is_upper_right (region X I r)"
using assms
proof (safe, goal_cases)
  case (1 t u)
  then show ?case
    by - (standard, force simp: cval_add_def)+
next
  case (2 x)
  (* XXX Does this lemma actually need the finiteness assumption? *)
  from region_not_empty[OF assms] obtain u where u: "u  region X I r" ..
  moreover have "(1 :: real)  0" by auto
  ultimately have "(u  1)  region X I r" using 2 by auto
  with x  X u have "intv_elem x u (I x)" "intv_elem x (u  1) (I x)" by auto
  then show ?case by (cases "I x", auto simp: cval_add_def)
qed

lemma bounded_region:
  assumes "finite X" "valid_region X k I r"
  defines R: "R  region X I r"
  assumes "¬ is_upper_right R" "u  R"
  shows "u  1  R"
proof -
  from upper_right_eq[OF assms(1,2)] assms(4) obtain x where x:
    "x  X" "¬ isGreater (I x)"
  by (auto simp: R)
  with assms have "intv_elem x u (I x)" by auto
  with x(2) have "¬ intv_elem x (u  1) (I x)" by (cases "I x", auto simp: cval_add_def)
  with x(1) assms show ?thesis by auto
qed

(* XXX Remove Caml case *)
context AlphaClosure
begin

(* XXX Clean *)
no_notation Regions_Beta.part ("[_]⇩_" [61,61] 61)

lemma succ_ex:
  assumes "R  "
  shows "succ  R  " (is "?G1") and "succ  R  Succ  R" (is "?G2")
  and " u  R.  t  0. (u  t)  R  ( t'  t. (u  t')  succ  R  0  t')" (is "?G3")
proof -
  from R   obtain I r where R: "R = region X I r" "valid_region X k I r"
    unfolding ℛ_def by auto
  from region_not_empty[OF finite] R obtain u where u: "u  R"
    by blast
  let ?Z = "{x  X .  c. I x = Const c}"
  let ?succ =
    "λ R'. R'  R  R'  Succ  R
      ( u  R.  t  0. (u  t)  R  ( t'  t. (u  t')  R'  0  t'))"
  consider (upper_right) " x  X. isGreater (I x)" | (intv) " x  X.  d. I x = Intv d  ?Z = {}"
         | (const) "?Z  {}"
  apply (cases " x  X. isGreater (I x)")
   apply fast
  apply (cases "?Z = {}")
   apply safe
   apply (rename_tac x)
   apply (case_tac "I x")
  by auto
  then have "?G1  ?G2  ?G3"
  proof cases
    case const
    with upper_right_eq[OF finite R(2)] have "¬ is_upper_right R" by (auto simp: R(1))
    from closest_prestable_1(1,2)[OF const finite R(2)] closest_valid_1[OF const finite R(2)] R(1)
    obtain R' where R':
      " u  R.  t>0. t't. (u  t')  R'  t'  0" "R'  " " u  R'.  t0. (u  t)  R"
    unfolding ℛ_def by auto
    with region_not_empty[OF finite] obtain u' where "u'  R'" unfolding ℛ_def by blast
    with R'(3) have neq: "R'  R" by (fastforce simp: cval_add_def)
    obtain t:: real where "t > 0" by (auto intro: that[of 1])
    with R'(1,2) u  R obtain t where "t  0" "u  t  R'" by auto
    with R   R'   u  R have "R'  Succ  R" by (intro SuccI3)
    moreover have "( u  R.  t  0. (u  t)  R  ( t'  t. (u  t')  R'  0  t'))"
      using R'(1) unfolding cval_add_def
      apply clarsimp
      subgoal for u t
        by (cases "t = 0") auto
      done
    ultimately have *: "?succ R'" using neq by auto
    have "succ  R = R'" unfolding succ_def
    proof (simp add: ¬ is_upper_right R, intro the_equality, rule *, goal_cases)
      case prems: (1 R'')
      from prems obtain t' u' where R'':
        "R''  " "R''  R" "t'  0" "R'' = [u'  t']⇩" "u'  R"
      using R'(1) by fastforce
      from this(1) obtain I r where R''2:
        "R'' = region X I r" "valid_region X k I r"
        by (auto simp: ℛ_def)
      from R'' have "u'  t'  R" using assms region_unique_spec by blast
      with * t'  0 u'  R obtain t'' where t'': "t''  t'" "u'  t''  R'" "t''  0" by auto
      from this(2) neq have "u'  t''  R" using R'(2) assms region_unique_spec by auto
      with t'' prems u'  R obtain t''' where t''':
        "t'''  t''" "u'  t'''  R''" "t'''  0"
      by auto
      with region_continuous[OF R''2(2) _ _ t'''(2)[unfolded R''2(1)], of "t'' - t'''" "t' - t'''"]
           t'' R'' regions_closed'_spec[OF R   R''(5,3)]
      have "u'  t''  R''" by (auto simp: R''2 cval_add_def)
      with t''(2) show ?case using R''(1) R'(2) region_unique_spec by blast
    qed
    with R' * show ?thesis by auto
  next
    case intv
    then have *: "xX. ¬ Regions.isConst (I x)" by auto
    let ?X0 = "{x  X. isIntv (I x)}"
    let ?M = "{x  ?X0. y?X0. (x, y)  r  (y, x)  r}"
    from intv obtain x c where x: "x  X" "¬ isGreater (I x)" and c: "I x = Intv c" by auto
    with x  X have "?X0  {}" by auto
    have "?X0 = {x  X. d. I x = Intv d}" by auto
    with R(2) have r: "total_on ?X0 r" "trans r" by auto
    from total_finite_trans_max[OF ?X0  {} _ this] finite
    obtain x' where x': "x'  ?X0" " y  ?X0. x'  y  (y, x')  r" by fastforce
    from this(2) have "y?X0. (x', y)  r  (y, x')  r" by auto
    with x'(1) have **: "?M  {}" by fastforce
    with upper_right_eq[OF finite R(2)] have "¬ is_upper_right R" by (auto simp: R(1))
    from closest_prestable_2(1,2)[OF * finite R(2) **] closest_valid_2[OF * finite R(2) **] R(1)
    obtain R' where R':
      "( u  R.  t  0. (u  t)  R  ( t'  t. (u  t')  R'  0  t'))" "R'  "
      " u  R'.  t0. (u  t)  R"
    unfolding ℛ_def by auto
    with region_not_empty[OF finite] obtain u' where "u'  R'" unfolding ℛ_def by blast
    with R'(3) have neq: "R'  R" by (fastforce simp: cval_add_def)
    from bounded_region[OF finite R(2), folded R(1), OF ¬ is_upper_right R u] have
      "u  (1 :: t)  R" "(1 :: t)  0"
    by auto
    with R'(1) u obtain t' where "t'  (1 :: t)" "(u  t')  R'" "0  t'" by fastforce
    with R   R'   u  R have "R'  Succ  R" by (intro SuccI3)
    with R'(1) neq have *: "?succ R'" by auto
    have "succ  R = R'" unfolding succ_def
    proof (simp add: ¬ is_upper_right R, intro the_equality, rule *, goal_cases)
      case prems: (1 R'')
      from prems obtain t' u' where R'':
        "R''  " "R''  R" "t'  0" "R'' = [u'  t']⇩" "u'  R"
      using R'(1) by fastforce
      from this(1) obtain I r where R''2:
        "R'' = region X I r" "valid_region X k I r"
      by (auto simp: ℛ_def)
      from R'' have "u'  t'  R" using assms region_unique_spec by blast
      with * t'  0 u'  R obtain t'' where t'': "t''  t'" "u'  t''  R'" "t''  0" by auto
      from this(2) neq have "u'  t''  R" using R'(2) assms region_unique_spec by auto
      with t'' prems u'  R obtain t''' where t''':
        "t'''  t''" "u'  t'''  R''" "t'''  0"
      by auto
      with region_continuous[OF R''2(2) _ _ t'''(2)[unfolded R''2(1)], of "t'' - t'''" "t' - t'''"]
           t'' R'' regions_closed'_spec[OF R   R''(5,3)]
      have "u'  t''  R''" by (auto simp: cval_add_def R''2)
      with t''(2) show ?case using R''(1) R'(2) region_unique_spec by blast
    qed
    with R' * show ?thesis by auto
  next
    case upper_right
    with upper_right_eq[OF finite R(2)] have "succ  R = R" by (auto simp: R succ_def)
    with R   u show ?thesis by (fastforce simp: cval_add_def intro: SuccI3)
  qed
  then show ?G1 ?G2 ?G3 by auto
qed
      
lemma region_set'_closed:
  fixes d :: nat
  assumes "R  " "d  0" "xset r. d  k x" "set r  X"
  shows "region_set' R r d  "
proof -
  from region_not_empty[OF finite] assms(1) obtain u where "u  R" using ℛ_def by blast
  from region_set'_id[OF _ _  finite, of _ k, folded ℛ_def] assms this show ?thesis by fastforce
qed

(* XXX Move *)
lemma clock_set_cong[simp]:
  assumes " c  set r. u c = d"
  shows "[r  d]u = u"
proof standard
  fix c
  from assms show "([r  d]u) c = u c" by (cases "c  set r"; auto)
qed

lemma region_reset_not_Succ:
  (* XXX Declare globally? *)
  notes regions_closed'_spec[intro]
  assumes "R  " "set r  X"
  shows "region_set' R r 0 = R  region_set' R r 0  Succ  R" (is "?R = R  _")
proof -
  from assms finite obtain u where "u  R" by (meson Succ.cases succ_ex(2))
  with R   have "u  V" "[u]⇩ = R" by (auto simp: region_unique_spec dest: region_V) 
  with region_set'_id[OF R  [unfolded ℛ_def] u  R finite] assms(2) have
    "?R = [[r0]u]⇩"
  by (force simp: ℛ_def)
  show ?thesis
  proof (cases " x  set r. u x = 0")
    case True
    then have "[r0]u = u" by simp
    with ?R = _ _ = R have "?R = R" by (force simp: ℛ_def)
    then show ?thesis ..
  next
    case False
    then obtain x where x: "x  set r" "u x  0" by auto
    { assume "?R  Succ  R"
      with u  R R   obtain t where
        "t  0" "[u  t]⇩ = ?R" "?R  "
      by (meson Succ.cases set_of_regions_spec)
      with u  R assms(1) have "u  t  ?R" by blast
      moreover from ?R = _ u  R have "[r0]u  ?R" by (fastforce simp: region_set'_def)
      moreover from x t  0 u  V assms have "(u  t) x > 0" by (force simp: cval_add_def V_def)
      moreover from x have "([r0]u) x = 0" by auto
      ultimately have False using ?R   x(1) by (fastforce simp: region_set'_def)
    }
    then show ?thesis by auto
  qed
qed

end (* Alpha Closure global *)

subsection ‹Justifying Timed Until vs ‹suntil›

(* XXX Move *)
lemma guard_continuous:
  assumes "u  g" "u  t  g" "0  (t'::'t::time)" "t'  t"
  shows "u  t'  g"
  using assms
  by (induction g;
      auto 4 3
        simp: cval_add_def order_le_less_subst2 order_subst2 add_increasing2
        intro: less_le_trans
     )

(* XXX Move *)
(*
lemma guard_continuous:
  assumes "u ⊢ g" "u ⊕ t ⊢ g" "0 ≤ t'" "t' ≤ t"
  shows "u ⊕ t' ⊢ g"
  using assms by (auto 4 4 intro: atomic_guard_continuous simp: list_all_iff)
*)

section ‹Definition and Semantics›

subsection ‹Syntactic Definition›

text ‹
  We do not include:
   a labelling function, as we will assume that atomic propositions are simply sets of states
   a fixed set of locations or clocks, as we will implicitly derive it from the set of transitions
   start or end locations, as we will primarily study reachability
›

type_synonym
  ('c, 't, 's) transition = "'s * ('c, 't) cconstraint * ('c set * 's) pmf"

type_synonym
  ('c, 't, 's) pta = "('c, 't, 's) transition set * ('c, 't, 's) invassn"

definition
  edges :: "('c, 't, 's) transition  ('s * ('c, 't) cconstraint * ('c set * 's) pmf * 'c set * 's) set"
where
  "edges  λ (l, g, p). {(l, g, p, X, l') | X l'. (X, l')  set_pmf p}"

definition
  "Edges A   {edges t | t. t  fst A}"

definition
  trans_of :: "('c, 't, 's) pta  ('c, 't, 's) transition set"
where
  "trans_of  fst"

definition
  inv_of  :: "('c, 'time, 's) pta  ('c, 'time, 's) invassn"
where
  "inv_of  snd"

no_notation transition ("_  _ ⟶⇗_,_,_ _" [61,61,61,61,61,61] 61)

abbreviation transition ::
  "('c, 'time, 's) pta  's  ('c, 'time) cconstraint  ('c set * 's) pmf  'c set  's  bool"
("_  _ ⟶⇗_,_,_ _" [61,61,61,61,61,61] 61) where
  "(A  l ⟶⇗g,p,Xl')  (l, g, p, X, l')  Edges A"

definition
  locations  :: "('c, 't, 's) pta  's set"
where
  "locations A  (fst ` Edges A)  ((snd o snd o snd o snd) ` Edges A)"


subsubsection ‹Collecting Information About Clocks›

(* XXX Remove sort constraints *)

definition collect_clkt :: "('c, 't::time, 's) transition set  ('c *'t) set"
where
  "collect_clkt S =  {collect_clock_pairs (fst (snd t)) | t . t  S}"

definition collect_clki :: "('c, 't :: time, 's) invassn  ('c *'t) set"
where
  "collect_clki I =  {collect_clock_pairs (I x) | x. True}"

definition clkp_set :: "('c, 't :: time, 's) pta  ('c * 't) set"
where
  "clkp_set A = collect_clki (inv_of A)  collect_clkt (trans_of A)"

definition collect_clkvt :: "('c, 't :: time, 's) pta  'c set"
where
  "collect_clkvt A =  ((fst o snd o snd o snd) ` Edges A)"

abbreviation clocks where "clocks A  fst ` clkp_set A  collect_clkvt A"

definition valid_abstraction
where
  "valid_abstraction A X k 
  ((x,m)  clkp_set A. m  k x  x  X  m  )  collect_clkvt A  X  finite X"

lemma valid_abstractionD[dest]:
  assumes "valid_abstraction A X k"
  shows "((x,m)  clkp_set A. m  k x  x  X  m  )" "collect_clkvt A  X" "finite X"
using assms unfolding valid_abstraction_def by auto

lemma valid_abstractionI[intro]:
  assumes "((x,m)  clkp_set A. m  k x  x  X  m  )" "collect_clkvt A  X" "finite X"
  shows "valid_abstraction A X k"
using assms unfolding valid_abstraction_def by auto

subsection ‹Operational Semantics as an MDP›

abbreviation (input) clock_set_set :: "'c set  't::time  ('c,'t) cval  ('c,'t) cval"
("[_:=_]_" [65,65,65] 65)
where
  "[X:=t]u  clock_set (SOME r. set r = X) t u"

term region_set'

abbreviation region_set_set :: "'c set  't::time  ('c,'t) zone  ('c,'t) zone"
("[_::=_]_" [65,65,65] 65)
where
  "[X::=t]R  region_set' R (SOME r. set r = X) t"

no_notation zone_set ("__  0⇙" [71] 71)

abbreviation zone_set_set :: "('c, 't::time) zone  'c set  ('c, 't) zone"
("__  0⇙" [71] 71)
where
  "ZX  0⇙  zone_set Z (SOME r. set r = X)"

abbreviation (input) ccval ("_" [100]) where "ccval cc  {v. v  cc}"

locale Probabilistic_Timed_Automaton =
  fixes A :: "('c, 't :: time, 's) pta"
  assumes admissible_targets:
    "(l, g, μ)  trans_of A  (X, l')  μ  gX  0⇙  inv_of A l'"
    "(l, g, μ)  trans_of A  (X, l')  μ  X  clocks A"
  ― ‹Not necessarily what we want to have›
begin

subsection ‹Syntactic Definition› text_raw ‹ \label{sem:mdp} ›

definition "L = locations A"

definition "𝒳 = clocks A"

definition "S  {(l, u) . l  L  ( x  𝒳. u x  0)  u  inv_of A l}"

inductive_set
  K :: "('s * ('c, 't) cval)  ('s * ('c, 't) cval) pmf set" for st :: "('s * ('c, 't) cval)"
where
  ― ‹Passage of time› delay:
  "st  S  st = (l, u)  t  0  u  t  inv_of A l  return_pmf (l, u  t)  K st" |
  ― ‹Discrete transitions› action:
  "st  S  st = (l, u)  (l, g, μ)  trans_of A  u  g
   map_pmf (λ (X, l). (l, ([X := 0]u))) μ  K st" |
  ― ‹Self loops -- Note that this does not assume st ∈ S› loop:
  "return_pmf st  K st"

declare K.intros[intro]

sublocale MDP: Markov_Decision_Process K by (standard, auto)

end (* Probabilistic Timed Automaton *)

section ‹Constructing the Corresponding Finite MDP on Regions›

locale Probabilistic_Timed_Automaton_Regions =
  Probabilistic_Timed_Automaton A + Regions 𝒳
  for A :: "('c, t, 's) pta" +
  ― ‹The following are necessary to obtain a finite› MDP›
  assumes finite: "finite 𝒳" "finite L" "finite (trans_of A)"
  assumes not_trivial: " l  L.  u  V. u  inv_of A l"
  assumes valid: "valid_abstraction A 𝒳 k"
begin

lemmas finite_ℛ = finite_ℛ[OF finite(1), of k, folded ℛ_def]


subsection ‹Syntactic Definition› text_raw ‹ \label{sem:mdprg} ›

definition "𝒮  {(l, R) . l  L  R    R  {u. u  inv_of A l}}"

(* XXX Move definition of V somewhere else *)
lemma S_alt_def: "S = {(l, u) . l  L  u  V  u  inv_of A l}" unfolding V_def S_def by auto

text ‹
  Note how we relax the definition to allow more transitions in the first case.
  To obtain a more compact MDP the commented out version can be used an proved equivalent.
›

inductive_set
 𝒦 :: "('s * ('c, t) cval set)  ('s * ('c, t) cval set) pmf set" for st :: "('s * ('c, t) cval set)"
where
  (* 
  -- "Passage of time" delay:
  "st ∈ 𝒮 ⟹ st = (l,R) ⟹ succ ℛ R ⊆ ⦃inv_of A l⦄ ⟹ return_pmf (l, succ ℛ R) ∈ 𝒦 st" |
  *)
   ― ‹Passage of time› delay:
  "st  𝒮  st = (l,R)  R'  Succ  R  R'  inv_of A l  return_pmf (l, R')  𝒦 st" |
  ― ‹Discrete transitions› action:
  "st  𝒮  st = (l, R )  (l, g, μ)  trans_of A  R  g
   map_pmf (λ (X, l). (l, region_set' R (SOME r. set r = X) 0)) μ  𝒦 st" |
  ― ‹Self loops -- Note that this does not assume st ∈ 𝒮› loop:
  "return_pmf st  𝒦 st"

lemmas [intro] = 𝒦.intros


subsection ‹Many Closure Properties›

lemma transition_def:
  "(A  l ⟶⇗g,μ,Xl') = ((l, g, μ)  trans_of A  (X, l')  μ)"
  unfolding Edges_def edges_def trans_of_def by auto

lemma transitionI[intro]:
  "A  l ⟶⇗g,μ,Xl'" if "(l, g, μ)  trans_of A" "(X, l')  μ"
  using that unfolding transition_def ..

lemma transitionD[dest]:
  "(l, g, μ)  trans_of A" "(X, l')  μ" if "A  l ⟶⇗g,μ,Xl'"
  using that unfolding transition_def by auto

lemma bex_Edges:
  "( x  Edges A. P x) = ( l g μ X l'. A  l ⟶⇗g,μ,Xl'  P (l, g, μ, X, l'))"
  by fastforce

(* XXX Move *)
lemma L_trans[intro]:
  assumes "(l, g, μ)  trans_of A" "(X, l')  μ"
  shows "l  L" "l'  L"
  using assms unfolding L_def locations_def by (auto simp: image_iff bex_Edges transition_def)

lemma transition_𝒳:
  "X  𝒳" if "A  l ⟶⇗g,μ,Xl'"
  using that unfolding 𝒳_def collect_clkvt_def clkp_set_def by auto

lemma admissible_targets_alt:
  "A  l ⟶⇗g,μ,Xl'  gX  0⇙  inv_of A l'"
  "A  l ⟶⇗g,μ,Xl'  X  clocks A"
  by (intro admissible_targets; blast)+

lemma V_reset_closed[intro]:
  assumes "u  V"
  shows "[r  (d::nat)]u  V"
using assms unfolding V_def
  apply safe
  subgoal for x
    by (cases "x  set r"; auto)
  done

lemmas V_reset_closed'[intro] = V_reset_closed[of _ _ 0, simplified]

lemma regions_part_ex[intro]:
  assumes "u  V"
  shows "u  [u]⇩" "[u]⇩  "
proof -
  from assms regions_partition[OF meta_eq_to_obj_eq[OF ℛ_def]] have
    "∃!R. R    u  R"
    unfolding V_def by auto
  then show "[u]⇩  " "u  [u]⇩"
    using alpha_interp.region_unique_spec by auto
qed

lemma rep_ℛ_ex[intro]:
  assumes "R  "
  shows "(SOME u. u  R)  R"
proof -
  from assms region_not_empty[OF finite(1)] have " u. u  R" unfolding ℛ_def by auto
  then show ?thesis ..
qed

lemma V_nn_closed[intro]:
  "u  V  t  0  u  t  V"
unfolding V_def cval_add_def by auto

lemma K_S_closed[intro]:
  assumes "μ  K s" "s'  μ" "s  S"
  shows "s'  S"
  using assms
  by (cases rule: K.cases, auto simp: S_alt_def dest: admissible_targets[unfolded zone_set_def])

lemma S_V[intro]:
  "(l, u)  S  u  V"
unfolding S_alt_def by auto

lemma L_V[intro]:
  "(l, u)  S  l  L"
unfolding S_def by auto

lemma 𝒮_V[intro]:
  "(l, R)  𝒮  R  "
unfolding 𝒮_def by auto

lemma admissible_targets':
  assumes "(l, g, μ)  trans_of A" "(X, l')  μ" "R  g"
  shows "region_set' R (SOME r. set r = X) 0  inv_of A l'"
using admissible_targets(1)[OF assms(1,2)] assms(3) unfolding region_set'_def zone_set_def by auto


subsection ‹The Region Graph is a Finite MDP›

lemma 𝒮_finite:
  "finite 𝒮"
using finite finite_ℛ unfolding 𝒮_def by auto

lemma 𝒦_finite:
  "finite (𝒦 st)"
proof -
  let ?B1 = "{(R', l, R). st  𝒮  st = (l, R)  R'  Succ  R  R'  inv_of A l}"
  let ?S1 = "(λ(R', l, R). return_pmf (l, R')) ` ?B1"
  let ?S1 = "{return_pmf (l, R') | R' l R. st  𝒮  st = (l, R)  R'  Succ  R  R'  inv_of A l}"
  let ?S2 = "{map_pmf (λ (X, l). (l, region_set' R (SOME r. set r = X) 0)) μ
             | R μ.  l g. st  𝒮  st = (l, R )  (l, g, μ)  trans_of A  R  g}"
  have "?B1  {(R', l, R). R'    (l, R)  𝒮 }" unfolding 𝒮_def by auto
  with 𝒮_finite finite_ℛ have "finite ?B1" by - (rule finite_subset, auto)
  moreover have "?S1 = (λ(R', l, R). return_pmf (l, R')) ` ?B1" by (auto simp: image_def)
  ultimately have *: "finite ?S1" by auto
  have "{μ. l g. (l, g, μ)  PTA.trans_of A} = ((λ (l, g, μ). μ) ` PTA.trans_of A)" by force
  with finite(3) finite_ℛ have "finite {(R, μ).  l g. R    (l, g, μ)  trans_of A}" by auto
  moreover have
    "{(R, μ).  l g. st  𝒮  st = (l, R )  (l, g, μ)  trans_of A  R  g}  "
  unfolding 𝒮_def by fastforce
  ultimately have **:
    "finite {(R, μ).  l g. st  𝒮  st = (l, R )  (l, g, μ)  trans_of A  R  g}"
  unfolding 𝒮_def by (blast intro: finite_subset)
  then have "finite ?S2" unfolding 𝒮_def by auto
  have "𝒦 st = ?S1  ?S2  {return_pmf st}" by (safe, cases rule: 𝒦.cases, auto)
  with * ** show ?thesis by auto
qed

(* XXX Obsolete in here, move to Regions *)
lemma ℛ_not_empty:
  "  {}"
proof -
  let ?r = "{}"
  let ?I = "λ c. Const 0"
  let ?R = "region 𝒳 ?I ?r"
  have "valid_region 𝒳 k ?I ?r"
  proof
    show "{} = {x  𝒳. d. Const 0 = Intv d}" by auto
    show "refl_on {} {}" and "trans {}" and "total_on {} {}" unfolding trans_def by auto
    show "x  𝒳. Regions.valid_intv (k x) (Const 0)" by auto
  qed
  then have "?R  " unfolding ℛ_def by auto
  then show "  {}" by blast
qed

lemma 𝒮_not_empty:
  "𝒮  {}"
proof -
  from not_trivial obtain l u where st: "l  L" "u  V" "u  inv_of A l" by blast
  then obtain R where R: "R  " "u  R" using ℛ_V by auto
  from valid have
    "(x, m)collect_clock_pairs (inv_of A l). m  real (k x)  x  𝒳  m  "
  by (fastforce simp: clkp_set_def collect_clki_def)
  from ccompatible[OF this, folded ℛ_def] R st(3) have
    "R  inv_of A l"
  unfolding ccompatible_def ccval_def by auto
  with st(1) R(1) show ?thesis unfolding 𝒮_def by auto
qed

lemma 𝒦_𝒮_closed:
  assumes "s  𝒮"
  shows "(D𝒦 s. set_pmf D)  𝒮"
proof (safe, cases rule: 𝒦.cases, blast, goal_cases)
  case (1 x a b l R)
  then show ?case unfolding 𝒮_def by (auto intro: alpha_interp.succ_ex(1))
next
  case (3 a b x)
  with s  𝒮 show ?case by auto
next
  case prems: (2 l' R' p l R g μ)
  then obtain X where *: "(X, l')  set_pmf μ" "R' = region_set' R (SOME r. set r = X) 0" by auto
  
  show ?case unfolding 𝒮_def
  proof safe
    from *(1) have "(l, g, μ, X, l')  edges (l,g, μ)" unfolding edges_def by auto
    with prems(6) have "(l, g, μ, X, l')  Edges A" unfolding Edges_def trans_of_def by auto
    then show "l'  L" unfolding L_def locations_def by force

    show "u  inv_of A l'" if "u  R'" for u
    using admissible_targets'[OF prems(6) *(1) prems(7)] *(2) that by auto    
    
    from admissible_targets(2)[OF prems(6) *(1)] have "X  𝒳" unfolding 𝒳_def by auto
    with finite(1) have "finite X" by (blast intro: finite_subset)
    then obtain r where "set r = X" using finite_list by auto
    then have "set (SOME r. set r = X) = X" by (rule someI)
    with X  𝒳 have "set (SOME r. set r = X)  𝒳" by auto
    with alpha_interp.region_set'_closed[of R 0 "SOME r. set r = X"] prems(4,5) *(2)
    show "R'  " unfolding 𝒮_def 𝒳_def by auto
  qed
qed

sublocale R_G: Finite_Markov_Decision_Process 𝒦 𝒮
by (standard, auto simp: 𝒮_finite 𝒮_not_empty 𝒦_finite 𝒦_𝒮_closed)

lemmas 𝒦_𝒮_closed'[intro] = R_G.set_pmf_closed


section ‹Relating the MDPs›

subsection ‹Translating From K to 𝒦›

(* XXX Clean this for regular automata too *)
(* Assumption of valid too strong? i.e. do not need l ∈ L here *)
lemma ccompatible_inv:
  shows "ccompatible  (inv_of A l)"
proof -
  from valid have
    "(x, m)collect_clock_pairs (inv_of A l). m  real (k x)  x  𝒳  m  "
  unfolding valid_abstraction_def clkp_set_def collect_clki_def by auto
  with ccompatible[of _ k 𝒳, folded ℛ_def] show ?thesis by auto
qed

lemma ccompatible_guard:
  assumes "(l, g, μ)  trans_of A"
  shows "ccompatible  g"
proof -
  from assms valid have
    "(x, m)collect_clock_pairs g. m  real (k x)  x  𝒳  m  "
  unfolding valid_abstraction_def clkp_set_def collect_clkt_def trans_of_def by fastforce
  with assms ccompatible[of _ k 𝒳, folded ℛ_def] show ?thesis by auto
qed

lemmas ccompatible_def = ccompatible_def[unfolded ccval_def]

lemma region_set'_eq:
  fixes X :: "'c set"
  assumes "R  " "u  R"
      and "A  l ⟶⇗g,μ,Xl'"
  shows
    "[[X:=0]u]⇩ = region_set' R (SOME r. set r = X) 0" "[[X:=0]u]⇩  " "[X:=0]u  [[X:=0]u]⇩"
proof -
  let ?r = "(SOME r. set r = X)"
  from admissible_targets_alt[OF assms(3)] 𝒳_def finite have "finite X"
    by (auto intro: finite_subset)
  then obtain r where "set r = X" using finite_list by blast
  then have "set ?r = X" by (intro someI)
  with valid assms(3) have "set ?r  𝒳"
    by (simp add: transition_𝒳)
  from region_set'_id[of _ 𝒳 k, folded ℛ_def, OF assms(1,2) finite(1) _ _ this]
  show
    "[[X:=0]u]⇩ = region_set' R (SOME r. set r = X) 0" "[[X:=0]u]⇩  " "[X:=0]u  [[X:=0]u]⇩"
  by force+
qed

lemma regions_part_ex_reset:
  assumes "u  V"
  shows  "[r  (d::nat)]u  [[r  d]u]⇩" "[[r  d]u]⇩  "
using assms by auto

lemma reset_sets_all_equiv:
  assumes "u  V" "u'  [[r  (d :: nat)]u]⇩" "x  set r" "set r  𝒳" "d  k x"
  shows "u' x = d"
proof -
  from assms(1) have u: "[r  d]u  [[r  d]u]⇩" "[[r  d]u]⇩  " by auto
  then obtain I ρ where I: "[[r  d]u]⇩ = region 𝒳 I ρ" "valid_region 𝒳 k I ρ"
    by (auto simp: ℛ_def)
  with u(1) assms(3-) have "intv_elem x ([r  d]u) (I x)" "valid_intv (k x) (I x)" by fastforce+
  moreover from assms have "([r  d]u) x = d" by simp
  ultimately have "I x = Const d" using assms(5) by (cases "I x") auto
  moreover from I assms(2-) have "intv_elem x u' (I x)" by fastforce
  ultimately show "u' x = d" by auto
qed

lemma reset_eq:
  assumes "u  V" "([[r  0]u]⇩) = ([[r'  0]u]⇩)" "set r  𝒳" "set r'  𝒳"
  shows "[r  0]u = [r'  0]u" using assms 
proof -
  have *: "u' x = 0" if "u'  [[r  0]u]⇩" "x  set r" for u' x
  using reset_sets_all_equiv[of u u' r 0 x] that assms by auto
  have "u' x = 0" if "u'  [[r'  0]u]⇩" "x  set r'" for u' x 
  using reset_sets_all_equiv[of u u' r' 0 x] that assms by auto
  from regions_part_ex_reset[OF assms(1), of _ 0] assms(2) have **:
    "([r'  0]u)  [[r  0]u]⇩" "([r  0]u)  [[r  0]u]⇩" "[[r  0]u]⇩  "
  by auto
  have "(([r  0]u) x) = (([r'  0]u) x)" for x
  proof (cases "x  set r")
    case True
    then have "([r  0]u) x = 0" by simp
    moreover from * ** True have "([r'  0]u) x = 0" by auto
    ultimately show ?thesis ..
  next
    case False
    then have id: "([r0]u) x = u x" by simp
    show ?thesis
    proof (cases "x  set r'")
      case True
      then have reset: "([r'  0]u) x = 0" by simp
      show ?thesis
      proof (cases "x  𝒳")
        case True
        from **(3) obtain I ρ where
          "([([r  0]u)]⇩) = Regions.region 𝒳 I ρ" "Regions.valid_region 𝒳 k I ρ"
        by (auto simp: ℛ_def)
        with ** x  𝒳 have ***:
          "intv_elem x ([r'  0]u) (I x)" "intv_elem x ([r  0]u) (I x)"
        by auto
        with reset have "I x = Const 0" by (cases "I x", auto)
        with ***(2) have "([r  0]u) x = 0" by auto
        with reset show ?thesis by auto
      next
        case False
        with assms(3-) have "x  set r" "x  set r'" by auto
        then show ?thesis by simp
      qed
    next
      case False
      then have reset: "([r'  0]u) x = u x" by simp
      with id show ?thesis by simp
    qed
  qed
  then show ?thesis ..
qed

lemma admissible_targets_clocks:
  assumes "(l, g, μ)  trans_of A" "(X, l')  μ"
  shows "X  𝒳" "set (SOME r. set r = X)  𝒳"
proof -
  from admissible_targets(2)[OF assms] finite have
    "finite X" "X  𝒳"
  by (auto intro: finite_subset simp: 𝒳_def)
  then obtain r where "set r = X" using finite_list by blast
  with X  𝒳 show "X  𝒳" "set (SOME r. set r = X)  𝒳"
    by (metis (mono_tags, lifting) someI_ex)+
qed

lemma
  "rel_pmf (λ a b. f a = b) μ (map_pmf f μ)"
by (subst pmf.rel_map(2)) (rule rel_pmf_reflI, auto)

lemma K_pmf_rel:
  defines "f  λ (l, u). (l, [u]⇩)"
  shows "rel_pmf (λ (l, u) st. (l, [u]⇩) = st) μ (map_pmf f μ)" unfolding f_def
by (subst pmf.rel_map(2)) (rule rel_pmf_reflI, auto)

lemma 𝒦_pmf_rel:
  assumes A: "μ  𝒦 (l, R)"
  defines "f  λ (l, u). (l, SOME u. u  R)"
  shows "rel_pmf (λ (l, u) st. (l, SOME u. u  R) = st) μ (map_pmf f μ)" unfolding f_def
by (subst pmf.rel_map(2)) (rule rel_pmf_reflI, auto)

lemma K_elem_abs_inj:
  assumes A: "μ  K (l, u)"
  defines "f  λ (l, u). (l, [u]⇩)"
  shows "inj_on f μ"
proof -
  have "(l1, u1) = (l2, u2)"
    if id: "(l1, [u1]⇩) = (l2, [u2]⇩)" and elem: "(l1, u1)  μ" "(l2, u2)  μ" for l1 l2 u1 u2
  proof -
    from id have [simp]: "l2 = l1" by auto
    from A
    show ?thesis
    proof (cases, safe, goal_cases)
      case (4 _ _ τ μ')
      from μ = _ elem obtain X1 X2 where
        "u1 = [(SOME r. set r = X1)0]u" "(X1, l1)  μ'"
        "u2 = [(SOME r. set r = X2)0]u" "(X2, l1)  μ'"
      by auto
      with _  trans_of _ admissible_targets_clocks have
        "set (SOME r. set r = X1)  𝒳" "set (SOME r. set r = X2)  𝒳"
      by auto
      with id u1 = _ u2 = _ reset_eq[of u] _  S show ?case by (auto simp: S_def V_def)
    qed (-, insert elem, simp)+
  qed
  then show ?thesis unfolding f_def inj_on_def by auto
qed

lemma K_elem_repr_inj:
  notes alpha_interp.valid_regions_distinct_spec[intro] (* XXX Declare somewhere else *)
  assumes A: "μ  𝒦 (l, R)"
  defines "f  λ (l, R). (l, SOME u. u  R)"
  shows "inj_on f μ"
proof -
  have "(l1, R1) = (l2, R2)"
    if id: "(l1, SOME u. u  R1) = (l2, SOME u. u  R2)" and elem: "(l1, R1)  μ" "(l2, R2)  μ"
    for l1 l2 R1 R2
  proof -
    let ?r1 = "SOME u. u  R1" and ?r2 = "SOME u. u  R2"
    from id have [simp]: "l2 = l1" "?r2 = ?r1" by auto
    { fix g μ' x
      assume "(l, R)  𝒮" "(l, g, μ')  PTA.trans_of A" "R  {v. v  g}"
         and "μ = map_pmf (λ(X, l). (l, region_set' R (SOME r. set r = X) 0)) μ'"
      from μ = _ elem obtain X1 X2 where
        "R1 = region_set' R (SOME r. set r = X1) 0" "(X1, l1)  μ'"
        "R2 = region_set' R (SOME r. set r = X2) 0" "(X2, l1)  μ'"
      by auto
      with _  trans_of _ admissible_targets_clocks have
        "set (SOME r. set r = X1)  𝒳" "set (SOME r. set r = X2)  𝒳"
      by auto
      with alpha_interp.region_set'_closed[of _ 0] R1 = _ R2 = _ _  𝒮 have
        "R1  " "R2  "
      unfolding 𝒮_def by auto
      with region_not_empty[OF finite(1)] have
        "R1  {}" "R2  {}" "u. u  R1" "u. u  R2"
      by (auto simp: ℛ_def)
      from someI_ex[OF this(3)] someI_ex[OF this(4)] have "?r1  R1" "?r1  R2" by simp+
      with R1   R2   have "R1 = R2" ..
    }
    from A elem this show ?thesis by (cases, auto)
  qed
  then show ?thesis unfolding f_def inj_on_def by auto
qed

lemma K_elem_pmf_map_abs:
  assumes A: "μ  K (l, u)" "(l', u')  μ"
  defines "f  λ (l, u). (l, [u]⇩)"
  shows "pmf (map_pmf f μ) (f (l', u')) = pmf μ (l', u')"
using A unfolding f_def by (blast intro: pmf_map_inj K_elem_abs_inj)

lemma K_elem_pmf_map_repr:
  assumes A: "μ  𝒦 (l, R)" "(l', R')  μ"
  defines "f  λ (l, R). (l, SOME u. u  R)"
  shows "pmf (map_pmf f μ) (f (l', R')) = pmf μ (l', R')"
using A unfolding f_def by (blast intro: pmf_map_inj K_elem_repr_inj)



definition transp :: "('s * ('c, t) cval  bool)  's * ('c, t) cval set  bool" where
  "transp φ  λ (l, R).  u  R. φ (l, u)"

subsection ‹Translating Configurations›

subsubsection ‹States›

definition
  abss :: "'s * ('c, t) cval  's * ('c, t) cval set"
where
  "abss  λ (l, u). if u  V then (l, [u]⇩) else (l, -V)"

definition
  reps :: "'s * ('c, t) cval set  's * ('c, t) cval"
where
  "reps  λ (l, R). if R   then (l, SOME u. u  R) else (l, λ_. -1)"

lemma 𝒮_reps_S[intro]:
  assumes "s  𝒮"
  shows "reps s  S"
using assms ℛ_V unfolding S_def 𝒮_def reps_def V_def by force

lemma S_abss_𝒮[intro]:
  assumes "s  S"
  shows "abss s  𝒮"
using assms ccompatible_inv unfolding 𝒮_def S_alt_def abss_def ccompatible_def by force

lemma 𝒮_abss_reps[simp]:
  "s  𝒮  abss (reps s) = s"
using ℛ_V alpha_interp.region_unique_spec by (auto simp: S_def 𝒮_def reps_def abss_def; blast)

lemma map_pmf_abs_reps:
  assumes "s  𝒮" "μ  𝒦 s"
  shows "map_pmf abss (map_pmf reps μ) = μ"
proof -
  have "map_pmf abss (map_pmf reps μ) = map_pmf (abss o reps) μ" by (simp add: pmf.map_comp)
  also have " = μ"
  proof (rule map_pmf_idI, safe, goal_cases)
    case prems: (1 l' R')
    with assms have "(l', R')  𝒮" "reps (l', R')  S" by auto
    then show ?case by auto
  qed
  finally show ?thesis by auto
qed

lemma abss_reps_id:
  notes R_G.cfg_onD_state[simp del]
  assumes "s'  𝒮" "s  set_pmf (action cfg)" "cfg  R_G.cfg_on s'"
  shows "abss (reps s) = s"
proof -
  from assms have "s  𝒮" by auto
  then show ?thesis by auto
qed

lemma abss_S[intro]:
  assumes "(l, u)  S"
  shows "abss (l, u) = (l, [u]⇩)"
using assms unfolding abss_def by auto

lemma reps_𝒮[intro]:
  assumes "(l, R)  𝒮"
  shows "reps (l, R) = (l, SOME u. u  R)"
using assms unfolding reps_def by auto

lemma fst_abss:
  "fst (abss st) = fst st" for st
  by (cases st) (auto simp: abss_def)

lemma K_elem_abss_inj:
  assumes A: "μ  K (l, u)" "(l, u)  S"
  shows "inj_on abss μ"
proof -
  from assms have "abss s' = (λ (l, u). (l, [u]⇩)) s'" if "s'  μ" for s'
  using that by (auto split: prod.split)
  from inj_on_cong[OF this] K_elem_abs_inj[OF A(1)] show ?thesis by force
qed

lemma 𝒦_elem_reps_inj:
  assumes A: "μ  𝒦 (l, R)" "(l, R)  𝒮"
  shows "inj_on reps μ"
proof -
  from assms have "reps s' = (λ (l, R). (l, SOME u. u  R)) s'" if "s'  μ" for s'
  using that by (auto split: prod.split)
  from inj_on_cong[OF this] K_elem_repr_inj[OF A(1)] show ?thesis by force
qed

lemma P_elem_pmf_map_abss:
  assumes A: "μ  K (l, u)" "(l, u)  S" "s'  μ"
  shows "pmf (map_pmf abss μ) (abss s') = pmf μ s'"
using A by (blast intro: pmf_map_inj K_elem_abss_inj)

lemma 𝒦_elem_pmf_map_reps:
  assumes A: "μ  𝒦 (l, R)" "(l, R)  𝒮" "(l', R')  μ"
  shows "pmf (map_pmf reps μ) (reps (l', R')) = pmf μ (l', R')"
using A by (blast intro: pmf_map_inj 𝒦_elem_reps_inj)

text ‹We need that 𝒳› is non-trivial here›
lemma not_𝒮_reps:
  "(l, R)  𝒮  reps (l, R)  S"
proof -
  assume "(l, R)  𝒮"
  let ?u = "SOME u. u  R"
  have "¬ ?u  inv_of A l" if "R  " "l  L"
  proof -
    (* XXX Refactor -- doing that kind of proof at other places too *)
    from region_not_empty[OF finite(1)] R   have "u. u  R" by (auto simp: ℛ_def)
    from someI_ex[OF this] have "?u  R" .
    moreover from (l, R)  𝒮 that have "¬ R  inv_of A l" by (auto simp: 𝒮_def)
    ultimately show ?thesis
      using ccompatible_inv[of l] R   unfolding ccompatible_def by fastforce
  qed
  with non_empty (l, R)  𝒮 show ?thesis unfolding 𝒮_def S_def reps_def by auto
qed

(* XXX Move up *)
lemma neq_V_not_region:
  "-V  "
using ℛ_V rep_ℛ_ex by auto

lemma 𝒮_abss_S:
  "abss s  𝒮  s  S"
  unfolding abss_def 𝒮_def S_def
  apply safe
  subgoal for _ _ _ u
    by (cases "u  V") auto
  subgoal for _ _ _ u
    using neq_V_not_region by (cases "u  V", (auto simp: V_def; fail), auto)
  subgoal for l' y l u
    using neq_V_not_region by (cases "u  V"; auto dest: regions_part_ex)
  done

lemma S_pred_stream_abss_𝒮:
  "pred_stream (λ s. s  S) xs  pred_stream (λ s. s  𝒮) (smap abss xs)"
using S_abss_𝒮 𝒮_abss_S by (auto simp: stream.pred_set)


sublocale MDP: Markov_Decision_Process_Invariant K S by (standard, auto)

abbreviation (input) "valid_cfg  MDP.valid_cfg"

lemma K_closed:
  "s  S  (DK s. set_pmf D)  S" 
  by auto


subsubsection ‹Intermezzo›

(* XXX Correct binding strength *)
abbreviation timed_bisim (infixr "~" 60) where
  "s ~ s'  abss s = abss s'"

lemma bisim_loc_id[intro]:
  "(l, u) ~ (l', u')  l = l'"
unfolding abss_def by (cases "u  V"; cases "u'  V"; simp)

lemma bisim_val_id[intro]:
  "[u]⇩ = [u']⇩" if "u  V" "(l, u) ~ (l', u')"
proof -
  have "(l', - V)  (l, [u]⇩)"
    using that by blast
  with that have "u'  V"
    by (force simp: abss_def)
  with that show ?thesis
    by (simp add: abss_def)
qed

lemma bisim_symmetric:
  "(l, u) ~ (l', u') = (l', u') ~ (l, u)"
by (rule eq_commute)

lemma bisim_val_id2[intro]:
  "u'  V  (l, u) ~ (l', u')  [u]⇩ = [u']⇩"
 apply (subst (asm) eq_commute)
 apply (subst eq_commute)
 apply (rule bisim_val_id)
by auto

lemma K_bisim_unique:
  assumes "s  S" "μ  K s" "x  μ" "x'  μ" "x ~ x'"
  shows "x = x'"
using assms(2,1,3-)
proof (cases rule: K.cases)
  case prems: (action l u τ μ')
  with assms obtain l1 l2 X1 X2 where A:
    "(X1, l1)  set_pmf μ'" "(X2, l2)  set_pmf μ'"
    "x = (l1, [X1:=0]u)" "x' = (l2, [X2:=0]u)"
  by auto
  from x ~ x' A s  S s = (l, u) have "[[X1:=0]u]⇩ = [[X2:=0]u]⇩"
    using bisim_val_id[OF S_V] K_S_closed assms(2-4) by (auto intro!: bisim_val_id[OF S_V])
  then have "[X1:=0]u = [X2:=0]u"
    using A admissible_targets_clocks(2)[OF prems(4)] prems(2,3) by - (rule reset_eq, force)
  with A x ~ x' show ?thesis by auto
next
  case delay
  with assms(3-) show ?thesis by auto
next
  case loop
  with assms(3-) show ?thesis by auto
qed

subsubsection ‹Predicates›

definition absp where
  "absp φ  φ o reps"

definition repp where
  "repp φ  φ o absp"


subsubsection ‹Distributions›

definition
  abst :: "('s * ('c, t) cval) pmf  ('s * ('c, t) cval set) pmf"
where
  "abst = map_pmf abss"

lemma abss_𝒮D:
  assumes "abss s  𝒮"
  obtains l u where "s = (l, u)" "u  [u]⇩" "[u]⇩  "
proof -
  obtain l u where "s = (l, u)" by force
  moreover from 𝒮_abss_S[OF assms] have "s  S" .
  ultimately have "abss s = (l, [u]⇩)" "u  V" "u  [u]⇩" "[u]⇩  " by auto
  with s = _ show ?thesis by (auto intro: that)
qed

lemma abss_𝒮D':
  assumes "abss s  𝒮" "abss s = (l, R)"
  obtains u where "s = (l, u)" "u  [u]⇩" "[u]⇩  " "R = [