# 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 (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)
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 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

(* 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 "∀x∈X. 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 ?X⇩0 = "{x ∈ X. ∃d. I x = Intv d}"
show "?X⇩0 = ?X⇩0" ..

from elem have "∀ x ∈ ?X⇩0. ∀ y ∈ ?X⇩0. (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"
moreover from A(2,4) elem between have **:
"d < u y" "u y < d + 1" "d < u y + t1" "u y + t1 < d + 1"
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)"
}
ultimately show
"∀ x ∈ ?X⇩0. ∀ y ∈ ?X⇩0. (x, y) ∈ r ⟷ frac ((u ⊕ t1) x) ≤ frac ((u ⊕ t1) y)"
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'. ∀ t≥0. (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'))"
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 *: "∀x∈X. ¬ Regions.isConst (I x)" by auto
let ?X⇩0 = "{x ∈ X. isIntv (I x)}"
let ?M = "{x ∈ ?X⇩0. ∀y∈?X⇩0. (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 "?X⇩0 ≠ {}" by auto
have "?X⇩0 = {x ∈ X. ∃d. I x = Intv d}" by auto
with R(2) have r: "total_on ?X⇩0 r" "trans r" by auto
from total_finite_trans_max[OF ‹?X⇩0 ≠ {}› _ this] finite
obtain x' where x': "x' ∈ ?X⇩0" "∀ y ∈ ?X⇩0. x' ≠ y ⟶ (y, x') ∈ r" by fastforce
from this(2) have "∀y∈?X⇩0. (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'. ∀ t≥0. (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" "∀x∈set 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 = [[r→0]u]⇩ℛ"
by (force simp: ℛ_def)
show ?thesis
proof (cases "∀ x ∈ set r. u x = 0")
case True
then have "[r→0]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 "[r→0]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 "([r→0]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
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,X⇖ l') ≡ (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)"

(* 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
"Z⇘X → 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"
"(l, g, μ) ∈ trans_of A ⟹ (X, l') ∈ μ ⟹ ⦃g⦄⇘X → 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,μ,X⇖ l') = ((l, g, μ) ∈ trans_of A ∧ (X, l') ∈ μ)"
unfolding Edges_def edges_def trans_of_def by auto

lemma transitionI[intro]:
"A ⊢ l ⟶⇗g,μ,X⇖ l'" 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,μ,X⇖ l'"
using that unfolding transition_def by auto

lemma bex_Edges:
"(∃ x ∈ Edges A. P x) = (∃ l g μ X l'. A ⊢ l ⟶⇗g,μ,X⇖ l' ∧ 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,μ,X⇖ l'"
using that unfolding 𝒳_def collect_clkvt_def clkp_set_def by auto

"A ⊢ l ⟶⇗g,μ,X⇖ l' ⟹ ⦃g⦄⇘X → 0⇙ ⊆ ⦃inv_of A l'⦄"
"A ⊢ l ⟶⇗g,μ,X⇖ l' ⟹ X ⊆ clocks A"

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"

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

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,μ,X⇖ l'"
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 ⊆ 𝒳"
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: "([r→0]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

assumes "(l, g, μ) ∈ trans_of A" "(X, l') ∈ μ"
shows "X ⊆ 𝒳" "set (SOME r. set r = X) ⊆ 𝒳"
proof -
"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 ⟹ (⋃D∈K 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
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 = [