[STATEMENT]
lemma region_set'_closed:
  fixes d :: nat
  assumes "R \<in> \<R>" "d \<ge> 0" "\<forall>x\<in>set r. d \<le> k x" "set r \<subseteq> X"
  shows "region_set' R r d \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. region_set' R r (real d) \<in> \<R>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. region_set' R r (real d) \<in> \<R>
[PROOF STEP]
from region_not_empty[OF finite] assms(1)
[PROOF STATE]
proof (chain)
picking this:
Regions.valid_region X ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region X ?I ?r
R \<in> \<R>
[PROOF STEP]
obtain u where "u \<in> R"
[PROOF STATE]
proof (prove)
using this:
Regions.valid_region X ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region X ?I ?r
R \<in> \<R>

goal (1 subgoal):
 1. (\<And>u. u \<in> R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<R>_def
[PROOF STATE]
proof (prove)
using this:
Regions.valid_region X ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region X ?I ?r
R \<in> \<R>
\<R> \<equiv> {Regions.region X I r |I r. Regions.valid_region X k I r}

goal (1 subgoal):
 1. (\<And>u. u \<in> R \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
u \<in> R

goal (1 subgoal):
 1. region_set' R r (real d) \<in> \<R>
[PROOF STEP]
from region_set'_id[OF _ _  finite, of _ k, folded \<R>_def] assms this
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?R \<in> \<R>; ?v \<in> ?R; 0 \<le> ?c; \<forall>x\<in>set ?r. ?c \<le> k x; set ?r \<subseteq> X\<rbrakk> \<Longrightarrow> [[?r\<rightarrow>real ?c]?v]\<^sub>\<R> = region_set' ?R ?r (real ?c) \<and> [[?r\<rightarrow>real ?c]?v]\<^sub>\<R> \<in> \<R> \<and> [?r\<rightarrow>real ?c]?v \<in> [[?r\<rightarrow>real ?c]?v]\<^sub>\<R>
R \<in> \<R>
0 \<le> d
\<forall>x\<in>set r. d \<le> k x
set r \<subseteq> X
u \<in> R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?R \<in> \<R>; ?v \<in> ?R; 0 \<le> ?c; \<forall>x\<in>set ?r. ?c \<le> k x; set ?r \<subseteq> X\<rbrakk> \<Longrightarrow> [[?r\<rightarrow>real ?c]?v]\<^sub>\<R> = region_set' ?R ?r (real ?c) \<and> [[?r\<rightarrow>real ?c]?v]\<^sub>\<R> \<in> \<R> \<and> [?r\<rightarrow>real ?c]?v \<in> [[?r\<rightarrow>real ?c]?v]\<^sub>\<R>
R \<in> \<R>
0 \<le> d
\<forall>x\<in>set r. d \<le> k x
set r \<subseteq> X
u \<in> R

goal (1 subgoal):
 1. region_set' R r (real d) \<in> \<R>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
region_set' R r (real d) \<in> \<R>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma clock_set_cong[simp]:
  assumes "\<forall> c \<in> set r. u c = d"
  shows "[r \<rightarrow> d]u = u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [r\<rightarrow>d]u = u
[PROOF STEP]
proof standard
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. ([r\<rightarrow>d]u) x = u x
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. ([r\<rightarrow>d]u) x = u x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>c\<in>set r. u c = d
[PROOF STEP]
show "([r \<rightarrow> d]u) c = u c"
[PROOF STATE]
proof (prove)
using this:
\<forall>c\<in>set r. u c = d

goal (1 subgoal):
 1. ([r\<rightarrow>d]u) c = u c
[PROOF STEP]
by (cases "c \<in> set r"; auto)
[PROOF STATE]
proof (state)
this:
([r\<rightarrow>d]u) c = u c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma guard_continuous:
  assumes "u \<turnstile> g" "u \<oplus> t \<turnstile> g" "0 \<le> (t'::'t::time)" "t' \<le> t"
  shows "u \<oplus> t' \<turnstile> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<oplus> t' \<turnstile> g
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<turnstile> g
u \<oplus> t \<turnstile> g
(0::'t) \<le> t'
t' \<le> t

goal (1 subgoal):
 1. u \<oplus> t' \<turnstile> g
[PROOF STEP]
by (induction g;
      auto 4 3
        simp: cval_add_def order_le_less_subst2 order_subst2 add_increasing2
        intro: less_le_trans
     )


[STATEMENT]
lemma valid_abstractionD[dest]:
  assumes "valid_abstraction A X k"
  shows "(\<forall>(x,m) \<in> clkp_set A. m \<le> k x \<and> x \<in> X \<and> m \<in> \<nat>)" "collect_clkvt A \<subseteq> X" "finite X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(x, m)\<in>PTA.clkp_set A. m \<le> k x \<and> x \<in> X \<and> m \<in> \<nat> &&& PTA.collect_clkvt A \<subseteq> X &&& finite X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
PTA.valid_abstraction A X k

goal (1 subgoal):
 1. \<forall>(x, m)\<in>PTA.clkp_set A. m \<le> k x \<and> x \<in> X \<and> m \<in> \<nat> &&& PTA.collect_clkvt A \<subseteq> X &&& finite X
[PROOF STEP]
unfolding valid_abstraction_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>(x, m)\<in>PTA.clkp_set A. m \<le> k x \<and> x \<in> X \<and> m \<in> \<nat>) \<and> PTA.collect_clkvt A \<subseteq> X \<and> finite X

goal (1 subgoal):
 1. \<forall>(x, m)\<in>PTA.clkp_set A. m \<le> k x \<and> x \<in> X \<and> m \<in> \<nat> &&& PTA.collect_clkvt A \<subseteq> X &&& finite X
[PROOF STEP]
by auto


[STATEMENT]
lemma valid_abstractionI[intro]:
  assumes "(\<forall>(x,m) \<in> clkp_set A. m \<le> k x \<and> x \<in> X \<and> m \<in> \<nat>)" "collect_clkvt A \<subseteq> X" "finite X"
  shows "valid_abstraction A X k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PTA.valid_abstraction A X k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>(x, m)\<in>PTA.clkp_set A. m \<le> k x \<and> x \<in> X \<and> m \<in> \<nat>
PTA.collect_clkvt A \<subseteq> X
finite X

goal (1 subgoal):
 1. PTA.valid_abstraction A X k
[PROOF STEP]
unfolding valid_abstraction_def
[PROOF STATE]
proof (prove)
using this:
\<forall>(x, m)\<in>PTA.clkp_set A. m \<le> k x \<and> x \<in> X \<and> m \<in> \<nat>
PTA.collect_clkvt A \<subseteq> X
finite X

goal (1 subgoal):
 1. (\<forall>(x, m)\<in>PTA.clkp_set A. m \<le> k x \<and> x \<in> X \<and> m \<in> \<nat>) \<and> PTA.collect_clkvt A \<subseteq> X \<and> finite X
[PROOF STEP]
by auto


[STATEMENT]
lemma S_alt_def: "S = {(l, u) . l \<in> L \<and> u \<in> V \<and> u \<turnstile> inv_of A l}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S = {(l, u). l \<in> L \<and> u \<in> V \<and> u \<turnstile> PTA.inv_of A l}
[PROOF STEP]
unfolding V_def S_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(l, u). l \<in> L \<and> (\<forall>x\<in>\<X>. 0 \<le> u x) \<and> u \<turnstile> PTA.inv_of A l} = {(l, u). l \<in> L \<and> u \<in> {v. \<forall>x\<in>\<X>. 0 \<le> v x} \<and> u \<turnstile> PTA.inv_of A l}
[PROOF STEP]
by auto


[STATEMENT]
lemma transition_def:
  "(A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l') = ((l, g, \<mu>) \<in> trans_of A \<and> (X, l') \<in> \<mu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l' = ((l, g, \<mu>) \<in> PTA.trans_of A \<and> (X, l') \<in> set_pmf \<mu>)
[PROOF STEP]
unfolding Edges_def edges_def trans_of_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((l, g, \<mu>, X, l') \<in> \<Union> {case t of (l, g, p) \<Rightarrow> {(l, g, p, X, l') |X l'. (X, l') \<in> set_pmf p} |t. t \<in> fst A}) = ((l, g, \<mu>) \<in> fst A \<and> (X, l') \<in> set_pmf \<mu>)
[PROOF STEP]
by auto


[STATEMENT]
lemma transitionI[intro]:
  "A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'" if "(l, g, \<mu>) \<in> trans_of A" "(X, l') \<in> \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
(l, g, \<mu>) \<in> PTA.trans_of A
(X, l') \<in> set_pmf \<mu>

goal (1 subgoal):
 1. A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'
[PROOF STEP]
unfolding transition_def
[PROOF STATE]
proof (prove)
using this:
(l, g, \<mu>) \<in> PTA.trans_of A
(X, l') \<in> set_pmf \<mu>

goal (1 subgoal):
 1. (l, g, \<mu>) \<in> PTA.trans_of A \<and> (X, l') \<in> set_pmf \<mu>
[PROOF STEP]
..


[STATEMENT]
lemma transitionD[dest]:
  "(l, g, \<mu>) \<in> trans_of A" "(X, l') \<in> \<mu>" if "A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, g, \<mu>) \<in> PTA.trans_of A &&& (X, l') \<in> set_pmf \<mu>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'

goal (1 subgoal):
 1. (l, g, \<mu>) \<in> PTA.trans_of A &&& (X, l') \<in> set_pmf \<mu>
[PROOF STEP]
unfolding transition_def
[PROOF STATE]
proof (prove)
using this:
(l, g, \<mu>) \<in> PTA.trans_of A \<and> (X, l') \<in> set_pmf \<mu>

goal (1 subgoal):
 1. (l, g, \<mu>) \<in> PTA.trans_of A &&& (X, l') \<in> set_pmf \<mu>
[PROOF STEP]
by auto


[STATEMENT]
lemma bex_Edges:
  "(\<exists> x \<in> Edges A. P x) = (\<exists> l g \<mu> X l'. A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l' \<and> P (l, g, \<mu>, X, l'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x\<in>Edges A. P x) = (\<exists>l g \<mu> X l'. A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l' \<and> P (l, g, \<mu>, X, l'))
[PROOF STEP]
by fastforce


[STATEMENT]
lemma L_trans[intro]:
  assumes "(l, g, \<mu>) \<in> trans_of A" "(X, l') \<in> \<mu>"
  shows "l \<in> L" "l' \<in> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l \<in> L &&& l' \<in> L
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(l, g, \<mu>) \<in> PTA.trans_of A
(X, l') \<in> set_pmf \<mu>

goal (1 subgoal):
 1. l \<in> L &&& l' \<in> L
[PROOF STEP]
unfolding L_def locations_def
[PROOF STATE]
proof (prove)
using this:
(l, g, \<mu>) \<in> PTA.trans_of A
(X, l') \<in> set_pmf \<mu>

goal (1 subgoal):
 1. l \<in> fst ` Edges A \<union> (snd \<circ> snd \<circ> snd \<circ> snd) ` Edges A &&& l' \<in> fst ` Edges A \<union> (snd \<circ> snd \<circ> snd \<circ> snd) ` Edges A
[PROOF STEP]
by (auto simp: image_iff bex_Edges transition_def)


[STATEMENT]
lemma transition_\<X>:
  "X \<subseteq> \<X>" if "A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<subseteq> \<X>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'

goal (1 subgoal):
 1. X \<subseteq> \<X>
[PROOF STEP]
unfolding \<X>_def collect_clkvt_def clkp_set_def
[PROOF STATE]
proof (prove)
using this:
A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'

goal (1 subgoal):
 1. X \<subseteq> fst ` (PTA.collect_clki (PTA.inv_of A) \<union> PTA.collect_clkt (PTA.trans_of A)) \<union> \<Union> ((fst \<circ> snd \<circ> snd \<circ> snd) ` Edges A)
[PROOF STEP]
by auto


[STATEMENT]
lemma admissible_targets_alt:
  "A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l' \<Longrightarrow> \<lbrace>g\<rbrace>\<^bsub>X \<rightarrow> 0\<^esub> \<subseteq> \<lbrace>inv_of A l'\<rbrace>"
  "A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l' \<Longrightarrow> X \<subseteq> clocks A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l' \<Longrightarrow> {v. v \<turnstile> g}\<^bsub>X \<rightarrow> 0\<^esub> \<subseteq> {v. v \<turnstile> PTA.inv_of A l'}) &&& (A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l' \<Longrightarrow> X \<subseteq> clocks A)
[PROOF STEP]
by (intro admissible_targets; blast)+


[STATEMENT]
lemma V_reset_closed[intro]:
  assumes "u \<in> V"
  shows "[r \<rightarrow> (d::nat)]u \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [r\<rightarrow>real d]u \<in> V
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<in> V

goal (1 subgoal):
 1. [r\<rightarrow>real d]u \<in> V
[PROOF STEP]
unfolding V_def
[PROOF STATE]
proof (prove)
using this:
u \<in> {v. \<forall>x\<in>\<X>. 0 \<le> v x}

goal (1 subgoal):
 1. [r\<rightarrow>real d]u \<in> {v. \<forall>x\<in>\<X>. 0 \<le> v x}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>\<X>. 0 \<le> u x; x \<in> \<X>\<rbrakk> \<Longrightarrow> 0 \<le> ([r\<rightarrow>real d]u) x
[PROOF STEP]
subgoal for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>\<X>. 0 \<le> u x; x \<in> \<X>\<rbrakk> \<Longrightarrow> 0 \<le> ([r\<rightarrow>real d]u) x
[PROOF STEP]
by (cases "x \<in> set r"; auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma regions_part_ex[intro]:
  assumes "u \<in> V"
  shows "u \<in> [u]\<^sub>\<R>" "[u]\<^sub>\<R> \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> [u]\<^sub>\<R> &&& [u]\<^sub>\<R> \<in> \<R>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u \<in> [u]\<^sub>\<R>
 2. [u]\<^sub>\<R> \<in> \<R>
[PROOF STEP]
from assms regions_partition[OF meta_eq_to_obj_eq[OF \<R>_def]]
[PROOF STATE]
proof (chain)
picking this:
u \<in> V
\<forall>x\<in>\<X>. 0 \<le> ?u x \<Longrightarrow> \<exists>!R. R \<in> \<R> \<and> ?u \<in> R
[PROOF STEP]
have
    "\<exists>!R. R \<in> \<R> \<and> u \<in> R"
[PROOF STATE]
proof (prove)
using this:
u \<in> V
\<forall>x\<in>\<X>. 0 \<le> ?u x \<Longrightarrow> \<exists>!R. R \<in> \<R> \<and> ?u \<in> R

goal (1 subgoal):
 1. \<exists>!R. R \<in> \<R> \<and> u \<in> R
[PROOF STEP]
unfolding V_def
[PROOF STATE]
proof (prove)
using this:
u \<in> {v. \<forall>x\<in>\<X>. 0 \<le> v x}
\<forall>x\<in>\<X>. 0 \<le> ?u x \<Longrightarrow> \<exists>!R. R \<in> \<R> \<and> ?u \<in> R

goal (1 subgoal):
 1. \<exists>!R. R \<in> \<R> \<and> u \<in> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>!R. R \<in> \<R> \<and> u \<in> R

goal (2 subgoals):
 1. u \<in> [u]\<^sub>\<R>
 2. [u]\<^sub>\<R> \<in> \<R>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>!R. R \<in> \<R> \<and> u \<in> R
[PROOF STEP]
show "[u]\<^sub>\<R> \<in> \<R>" "u \<in> [u]\<^sub>\<R>"
[PROOF STATE]
proof (prove)
using this:
\<exists>!R. R \<in> \<R> \<and> u \<in> R

goal (1 subgoal):
 1. [u]\<^sub>\<R> \<in> \<R> &&& u \<in> [u]\<^sub>\<R>
[PROOF STEP]
using alpha_interp.region_unique_spec
[PROOF STATE]
proof (prove)
using this:
\<exists>!R. R \<in> \<R> \<and> u \<in> R
\<lbrakk>?u \<in> ?R; ?R \<in> \<R>\<rbrakk> \<Longrightarrow> [?u]\<^sub>\<R> = ?R

goal (1 subgoal):
 1. [u]\<^sub>\<R> \<in> \<R> &&& u \<in> [u]\<^sub>\<R>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[u]\<^sub>\<R> \<in> \<R>
u \<in> [u]\<^sub>\<R>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rep_\<R>_ex[intro]:
  assumes "R \<in> \<R>"
  shows "(SOME u. u \<in> R) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME u. u \<in> R) \<in> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (SOME u. u \<in> R) \<in> R
[PROOF STEP]
from assms region_not_empty[OF finite(1)]
[PROOF STATE]
proof (chain)
picking this:
R \<in> \<R>
Regions.valid_region \<X> ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region \<X> ?I ?r
[PROOF STEP]
have "\<exists> u. u \<in> R"
[PROOF STATE]
proof (prove)
using this:
R \<in> \<R>
Regions.valid_region \<X> ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region \<X> ?I ?r

goal (1 subgoal):
 1. \<exists>u. u \<in> R
[PROOF STEP]
unfolding \<R>_def
[PROOF STATE]
proof (prove)
using this:
R \<in> {Regions.region \<X> I r |I r. Regions.valid_region \<X> k I r}
Regions.valid_region \<X> ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region \<X> ?I ?r

goal (1 subgoal):
 1. \<exists>u. u \<in> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u. u \<in> R

goal (1 subgoal):
 1. (SOME u. u \<in> R) \<in> R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>u. u \<in> R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>u. u \<in> R

goal (1 subgoal):
 1. (SOME u. u \<in> R) \<in> R
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(SOME u. u \<in> R) \<in> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma V_nn_closed[intro]:
  "u \<in> V \<Longrightarrow> t \<ge> 0 \<Longrightarrow> u \<oplus> t \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<in> V; (0::'a) \<le> t\<rbrakk> \<Longrightarrow> u \<oplus> t \<in> V
[PROOF STEP]
unfolding V_def cval_add_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u \<in> {v. \<forall>x\<in>\<X>. (0::'a) \<le> v x}; (0::'a) \<le> t\<rbrakk> \<Longrightarrow> (\<lambda>x. u x + t) \<in> {v. \<forall>x\<in>\<X>. (0::'a) \<le> v x}
[PROOF STEP]
by auto


[STATEMENT]
lemma K_S_closed[intro]:
  assumes "\<mu> \<in> K s" "s' \<in> \<mu>" "s \<in> S"
  shows "s' \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s' \<in> S
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> K s
s' \<in> set_pmf \<mu>
s \<in> S

goal (1 subgoal):
 1. s' \<in> S
[PROOF STEP]
by (cases rule: K.cases, auto simp: S_alt_def dest: admissible_targets[unfolded zone_set_def])


[STATEMENT]
lemma S_V[intro]:
  "(l, u) \<in> S \<Longrightarrow> u \<in> V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, u) \<in> S \<Longrightarrow> u \<in> V
[PROOF STEP]
unfolding S_alt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, u) \<in> {(l, u). l \<in> L \<and> u \<in> V \<and> u \<turnstile> PTA.inv_of A l} \<Longrightarrow> u \<in> V
[PROOF STEP]
by auto


[STATEMENT]
lemma L_V[intro]:
  "(l, u) \<in> S \<Longrightarrow> l \<in> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, u) \<in> S \<Longrightarrow> l \<in> L
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, u) \<in> {(l, u). l \<in> L \<and> (\<forall>x\<in>\<X>. 0 \<le> u x) \<and> u \<turnstile> PTA.inv_of A l} \<Longrightarrow> l \<in> L
[PROOF STEP]
by auto


[STATEMENT]
lemma \<S>_V[intro]:
  "(l, R) \<in> \<S> \<Longrightarrow> R \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, R) \<in> \<S> \<Longrightarrow> R \<in> \<R>
[PROOF STEP]
unfolding \<S>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, R) \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}} \<Longrightarrow> R \<in> \<R>
[PROOF STEP]
by auto


[STATEMENT]
lemma admissible_targets':
  assumes "(l, g, \<mu>) \<in> trans_of A" "(X, l') \<in> \<mu>" "R \<subseteq> \<lbrace>g\<rbrace>"
  shows "region_set' R (SOME r. set r = X) 0 \<subseteq> \<lbrace>inv_of A l'\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [X::=0]R \<subseteq> {v. v \<turnstile> PTA.inv_of A l'}
[PROOF STEP]
using admissible_targets(1)[OF assms(1,2)] assms(3)
[PROOF STATE]
proof (prove)
using this:
{v. v \<turnstile> g}\<^bsub>X \<rightarrow> 0\<^esub> \<subseteq> {v. v \<turnstile> PTA.inv_of A l'}
R \<subseteq> {v. v \<turnstile> g}

goal (1 subgoal):
 1. [X::=0]R \<subseteq> {v. v \<turnstile> PTA.inv_of A l'}
[PROOF STEP]
unfolding region_set'_def zone_set_def
[PROOF STATE]
proof (prove)
using this:
{[(SOME r. set r = X)\<rightarrow>0]u |u. u \<in> {v. v \<turnstile> g}} \<subseteq> {v. v \<turnstile> PTA.inv_of A l'}
R \<subseteq> {v. v \<turnstile> g}

goal (1 subgoal):
 1. {[(SOME r. set r = X)\<rightarrow>0]v |v. v \<in> R} \<subseteq> {v. v \<turnstile> PTA.inv_of A l'}
[PROOF STEP]
by auto


[STATEMENT]
lemma \<S>_finite:
  "finite \<S>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite \<S>
[PROOF STEP]
using finite finite_\<R>
[PROOF STATE]
proof (prove)
using this:
finite \<X>
finite L
finite (PTA.trans_of A)
finite \<R>

goal (1 subgoal):
 1. finite \<S>
[PROOF STEP]
unfolding \<S>_def
[PROOF STATE]
proof (prove)
using this:
finite \<X>
finite L
finite (PTA.trans_of A)
finite \<R>

goal (1 subgoal):
 1. finite {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}}
[PROOF STEP]
by auto


[STATEMENT]
lemma \<K>_finite:
  "finite (\<K> st)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
let ?B1 = "{(R', l, R). st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> \<lbrace>inv_of A l\<rbrace>}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
let ?S1 = "(\<lambda>(R', l, R). return_pmf (l, R')) ` ?B1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
let ?S1 = "{return_pmf (l, R') | R' l R. st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> \<lbrace>inv_of A l\<rbrace>}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
let ?S2 = "{map_pmf (\<lambda> (X, l). (l, region_set' R (SOME r. set r = X) 0)) \<mu>
             | R \<mu>. \<exists> l g. st \<in> \<S> \<and> st = (l, R ) \<and> (l, g, \<mu>) \<in> trans_of A \<and> R \<subseteq> \<lbrace>g\<rbrace>}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
have "?B1 \<subseteq> {(R', l, R). R' \<in> \<R> \<and> (l, R) \<in> \<S> }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(R', l, R). st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}} \<subseteq> {(R', l, R). R' \<in> \<R> \<and> (l, R) \<in> \<S>}
[PROOF STEP]
unfolding \<S>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(R', l, R). st \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}} \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}} \<subseteq> {(R', l, R). R' \<in> \<R> \<and> (l, R) \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(R', l, R). st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}} \<subseteq> {(R', l, R). R' \<in> \<R> \<and> (l, R) \<in> \<S>}

goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
with \<S>_finite finite_\<R>
[PROOF STATE]
proof (chain)
picking this:
finite \<S>
finite \<R>
{(R', l, R). st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}} \<subseteq> {(R', l, R). R' \<in> \<R> \<and> (l, R) \<in> \<S>}
[PROOF STEP]
have "finite ?B1"
[PROOF STATE]
proof (prove)
using this:
finite \<S>
finite \<R>
{(R', l, R). st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}} \<subseteq> {(R', l, R). R' \<in> \<R> \<and> (l, R) \<in> \<S>}

goal (1 subgoal):
 1. finite {(R', l, R). st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}}
[PROOF STEP]
by - (rule finite_subset, auto)
[PROOF STATE]
proof (state)
this:
finite {(R', l, R). st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}}

goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {(R', l, R). st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}}

goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
have "?S1 = (\<lambda>(R', l, R). return_pmf (l, R')) ` ?B1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {uu_. \<exists>R' l R. uu_ = return_pmf (l, R') \<and> st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}} = (\<lambda>(R', l, R). return_pmf (l, R')) ` {(R', l, R). st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}}
[PROOF STEP]
by (auto simp: image_def)
[PROOF STATE]
proof (state)
this:
{uu_. \<exists>R' l R. uu_ = return_pmf (l, R') \<and> st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}} = (\<lambda>(R', l, R). return_pmf (l, R')) ` {(R', l, R). st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}}

goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite {(R', l, R). st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}}
{uu_. \<exists>R' l R. uu_ = return_pmf (l, R') \<and> st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}} = (\<lambda>(R', l, R). return_pmf (l, R')) ` {(R', l, R). st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}}
[PROOF STEP]
have *: "finite ?S1"
[PROOF STATE]
proof (prove)
using this:
finite {(R', l, R). st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}}
{uu_. \<exists>R' l R. uu_ = return_pmf (l, R') \<and> st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}} = (\<lambda>(R', l, R). return_pmf (l, R')) ` {(R', l, R). st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}}

goal (1 subgoal):
 1. finite {uu_. \<exists>R' l R. uu_ = return_pmf (l, R') \<and> st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {uu_. \<exists>R' l R. uu_ = return_pmf (l, R') \<and> st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}}

goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
have "{\<mu>. \<exists>l g. (l, g, \<mu>) \<in> PTA.trans_of A} = ((\<lambda> (l, g, \<mu>). \<mu>) ` PTA.trans_of A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {\<mu>. \<exists>l g. (l, g, \<mu>) \<in> PTA.trans_of A} = (\<lambda>(l, g, \<mu>). \<mu>) ` PTA.trans_of A
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{\<mu>. \<exists>l g. (l, g, \<mu>) \<in> PTA.trans_of A} = (\<lambda>(l, g, \<mu>). \<mu>) ` PTA.trans_of A

goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
with finite(3) finite_\<R>
[PROOF STATE]
proof (chain)
picking this:
finite (PTA.trans_of A)
finite \<R>
{\<mu>. \<exists>l g. (l, g, \<mu>) \<in> PTA.trans_of A} = (\<lambda>(l, g, \<mu>). \<mu>) ` PTA.trans_of A
[PROOF STEP]
have "finite {(R, \<mu>). \<exists> l g. R \<in> \<R> \<and> (l, g, \<mu>) \<in> trans_of A}"
[PROOF STATE]
proof (prove)
using this:
finite (PTA.trans_of A)
finite \<R>
{\<mu>. \<exists>l g. (l, g, \<mu>) \<in> PTA.trans_of A} = (\<lambda>(l, g, \<mu>). \<mu>) ` PTA.trans_of A

goal (1 subgoal):
 1. finite {(R, \<mu>). \<exists>l g. R \<in> \<R> \<and> (l, g, \<mu>) \<in> PTA.trans_of A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {(R, \<mu>). \<exists>l g. R \<in> \<R> \<and> (l, g, \<mu>) \<in> PTA.trans_of A}

goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {(R, \<mu>). \<exists>l g. R \<in> \<R> \<and> (l, g, \<mu>) \<in> PTA.trans_of A}

goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
have
    "{(R, \<mu>). \<exists> l g. st \<in> \<S> \<and> st = (l, R ) \<and> (l, g, \<mu>) \<in> trans_of A \<and> R \<subseteq> \<lbrace>g\<rbrace>} \<subseteq> \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(R, \<mu>). \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}} \<subseteq> {(R, \<mu>). \<exists>l g. R \<in> \<R> \<and> (l, g, \<mu>) \<in> PTA.trans_of A}
[PROOF STEP]
unfolding \<S>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(R, \<mu>). \<exists>l g. st \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}} \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}} \<subseteq> {(R, \<mu>). \<exists>l g. R \<in> \<R> \<and> (l, g, \<mu>) \<in> PTA.trans_of A}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
{(R, \<mu>). \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}} \<subseteq> {(R, \<mu>). \<exists>l g. R \<in> \<R> \<and> (l, g, \<mu>) \<in> PTA.trans_of A}

goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite {(R, \<mu>). \<exists>l g. R \<in> \<R> \<and> (l, g, \<mu>) \<in> PTA.trans_of A}
{(R, \<mu>). \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}} \<subseteq> {(R, \<mu>). \<exists>l g. R \<in> \<R> \<and> (l, g, \<mu>) \<in> PTA.trans_of A}
[PROOF STEP]
have **:
    "finite {(R, \<mu>). \<exists> l g. st \<in> \<S> \<and> st = (l, R ) \<and> (l, g, \<mu>) \<in> trans_of A \<and> R \<subseteq> \<lbrace>g\<rbrace>}"
[PROOF STATE]
proof (prove)
using this:
finite {(R, \<mu>). \<exists>l g. R \<in> \<R> \<and> (l, g, \<mu>) \<in> PTA.trans_of A}
{(R, \<mu>). \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}} \<subseteq> {(R, \<mu>). \<exists>l g. R \<in> \<R> \<and> (l, g, \<mu>) \<in> PTA.trans_of A}

goal (1 subgoal):
 1. finite {(R, \<mu>). \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}}
[PROOF STEP]
unfolding \<S>_def
[PROOF STATE]
proof (prove)
using this:
finite {(R, \<mu>). \<exists>l g. R \<in> \<R> \<and> (l, g, \<mu>) \<in> PTA.trans_of A}
{(R, \<mu>). \<exists>l g. st \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}} \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}} \<subseteq> {(R, \<mu>). \<exists>l g. R \<in> \<R> \<and> (l, g, \<mu>) \<in> PTA.trans_of A}

goal (1 subgoal):
 1. finite {(R, \<mu>). \<exists>l g. st \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}} \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}}
[PROOF STEP]
by (blast intro: finite_subset)
[PROOF STATE]
proof (state)
this:
finite {(R, \<mu>). \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}}

goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite {(R, \<mu>). \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}}
[PROOF STEP]
have "finite ?S2"
[PROOF STATE]
proof (prove)
using this:
finite {(R, \<mu>). \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}}

goal (1 subgoal):
 1. finite {map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu> |R \<mu>. \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}}
[PROOF STEP]
unfolding \<S>_def
[PROOF STATE]
proof (prove)
using this:
finite {(R, \<mu>). \<exists>l g. st \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}} \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}}

goal (1 subgoal):
 1. finite {map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu> |R \<mu>. \<exists>l g. st \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}} \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu> |R \<mu>. \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}}

goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
have "\<K> st = ?S1 \<union> ?S2 \<union> {return_pmf st}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<K> st = {uu_. \<exists>R' l R. uu_ = return_pmf (l, R') \<and> st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}} \<union> {map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu> |R \<mu>. \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}} \<union> {return_pmf st}
[PROOF STEP]
by (safe, cases rule: \<K>.cases, auto)
[PROOF STATE]
proof (state)
this:
\<K> st = {uu_. \<exists>R' l R. uu_ = return_pmf (l, R') \<and> st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}} \<union> {map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu> |R \<mu>. \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}} \<union> {return_pmf st}

goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
with * **
[PROOF STATE]
proof (chain)
picking this:
finite {uu_. \<exists>R' l R. uu_ = return_pmf (l, R') \<and> st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}}
finite {(R, \<mu>). \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}}
\<K> st = {uu_. \<exists>R' l R. uu_ = return_pmf (l, R') \<and> st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}} \<union> {map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu> |R \<mu>. \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}} \<union> {return_pmf st}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {uu_. \<exists>R' l R. uu_ = return_pmf (l, R') \<and> st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}}
finite {(R, \<mu>). \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}}
\<K> st = {uu_. \<exists>R' l R. uu_ = return_pmf (l, R') \<and> st \<in> \<S> \<and> st = (l, R) \<and> R' \<in> Succ \<R> R \<and> R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}} \<union> {map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu> |R \<mu>. \<exists>l g. st \<in> \<S> \<and> st = (l, R) \<and> (l, g, \<mu>) \<in> PTA.trans_of A \<and> R \<subseteq> {v. v \<turnstile> g}} \<union> {return_pmf st}

goal (1 subgoal):
 1. finite (\<K> st)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (\<K> st)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<R>_not_empty:
  "\<R> \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R> \<noteq> {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R> \<noteq> {}
[PROOF STEP]
let ?r = "{}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R> \<noteq> {}
[PROOF STEP]
let ?I = "\<lambda> c. Const 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R> \<noteq> {}
[PROOF STEP]
let ?R = "region \<X> ?I ?r"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R> \<noteq> {}
[PROOF STEP]
have "valid_region \<X> k ?I ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Regions.valid_region \<X> k (\<lambda>c. Regions.intv.Const 0) {}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. ?X\<^sub>0 = {x \<in> \<X>. \<exists>d. Regions.intv.Const 0 = Regions.intv.Intv d}
 2. refl_on ?X\<^sub>0 {}
 3. trans {}
 4. total_on ?X\<^sub>0 {}
 5. \<forall>x\<in>\<X>. Regions.valid_intv (k x) (Regions.intv.Const 0)
[PROOF STEP]
show "{} = {x \<in> \<X>. \<exists>d. Const 0 = Intv d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} = {x \<in> \<X>. \<exists>d. Regions.intv.Const 0 = Regions.intv.Intv d}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{} = {x \<in> \<X>. \<exists>d. Regions.intv.Const 0 = Regions.intv.Intv d}

goal (4 subgoals):
 1. refl_on {} {}
 2. trans {}
 3. total_on {} {}
 4. \<forall>x\<in>\<X>. Regions.valid_intv (k x) (Regions.intv.Const 0)
[PROOF STEP]
show "refl_on {} {}" and "trans {}" and "total_on {} {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refl_on {} {} &&& trans {} &&& total_on {} {}
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. refl_on {} {} &&& \<forall>x y z. (x, y) \<in> {} \<longrightarrow> (y, z) \<in> {} \<longrightarrow> (x, z) \<in> {} &&& total_on {} {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
refl_on {} {}
trans {}
total_on {} {}

goal (1 subgoal):
 1. \<forall>x\<in>\<X>. Regions.valid_intv (k x) (Regions.intv.Const 0)
[PROOF STEP]
show "\<forall>x \<in> \<X>. Regions.valid_intv (k x) (Const 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>\<X>. Regions.valid_intv (k x) (Regions.intv.Const 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>\<X>. Regions.valid_intv (k x) (Regions.intv.Const 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Regions.valid_region \<X> k (\<lambda>c. Regions.intv.Const 0) {}

goal (1 subgoal):
 1. \<R> \<noteq> {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Regions.valid_region \<X> k (\<lambda>c. Regions.intv.Const 0) {}
[PROOF STEP]
have "?R \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
Regions.valid_region \<X> k (\<lambda>c. Regions.intv.Const 0) {}

goal (1 subgoal):
 1. Regions.region \<X> (\<lambda>c. Regions.intv.Const 0) {} \<in> \<R>
[PROOF STEP]
unfolding \<R>_def
[PROOF STATE]
proof (prove)
using this:
Regions.valid_region \<X> k (\<lambda>c. Regions.intv.Const 0) {}

goal (1 subgoal):
 1. Regions.region \<X> (\<lambda>c. Regions.intv.Const 0) {} \<in> {Regions.region \<X> I r |I r. Regions.valid_region \<X> k I r}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Regions.region \<X> (\<lambda>c. Regions.intv.Const 0) {} \<in> \<R>

goal (1 subgoal):
 1. \<R> \<noteq> {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Regions.region \<X> (\<lambda>c. Regions.intv.Const 0) {} \<in> \<R>
[PROOF STEP]
show "\<R> \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
Regions.region \<X> (\<lambda>c. Regions.intv.Const 0) {} \<in> \<R>

goal (1 subgoal):
 1. \<R> \<noteq> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<R> \<noteq> {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<S>_not_empty:
  "\<S> \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<S> \<noteq> {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<S> \<noteq> {}
[PROOF STEP]
from not_trivial
[PROOF STATE]
proof (chain)
picking this:
\<exists>l\<in>L. \<exists>u\<in>V. u \<turnstile> PTA.inv_of A l
[PROOF STEP]
obtain l u where st: "l \<in> L" "u \<in> V" "u \<turnstile> inv_of A l"
[PROOF STATE]
proof (prove)
using this:
\<exists>l\<in>L. \<exists>u\<in>V. u \<turnstile> PTA.inv_of A l

goal (1 subgoal):
 1. (\<And>l u. \<lbrakk>l \<in> L; u \<in> V; u \<turnstile> PTA.inv_of A l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
l \<in> L
u \<in> V
u \<turnstile> PTA.inv_of A l

goal (1 subgoal):
 1. \<S> \<noteq> {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l \<in> L
u \<in> V
u \<turnstile> PTA.inv_of A l
[PROOF STEP]
obtain R where R: "R \<in> \<R>" "u \<in> R"
[PROOF STATE]
proof (prove)
using this:
l \<in> L
u \<in> V
u \<turnstile> PTA.inv_of A l

goal (1 subgoal):
 1. (\<And>R. \<lbrakk>R \<in> \<R>; u \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<R>_V
[PROOF STATE]
proof (prove)
using this:
l \<in> L
u \<in> V
u \<turnstile> PTA.inv_of A l
\<Union> \<R> = V

goal (1 subgoal):
 1. (\<And>R. \<lbrakk>R \<in> \<R>; u \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R \<in> \<R>
u \<in> R

goal (1 subgoal):
 1. \<S> \<noteq> {}
[PROOF STEP]
from valid
[PROOF STATE]
proof (chain)
picking this:
PTA.valid_abstraction A \<X> (\<lambda>x. real (k x))
[PROOF STEP]
have
    "\<forall>(x, m)\<in>collect_clock_pairs (inv_of A l). m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>"
[PROOF STATE]
proof (prove)
using this:
PTA.valid_abstraction A \<X> (\<lambda>x. real (k x))

goal (1 subgoal):
 1. \<forall>(x, m)\<in>collect_clock_pairs (PTA.inv_of A l). m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>
[PROOF STEP]
by (fastforce simp: clkp_set_def collect_clki_def)
[PROOF STATE]
proof (state)
this:
\<forall>(x, m)\<in>collect_clock_pairs (PTA.inv_of A l). m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>

goal (1 subgoal):
 1. \<S> \<noteq> {}
[PROOF STEP]
from ccompatible[OF this, folded \<R>_def] R st(3)
[PROOF STATE]
proof (chain)
picking this:
ccompatible \<R> (PTA.inv_of A l)
R \<in> \<R>
u \<in> R
u \<turnstile> PTA.inv_of A l
[PROOF STEP]
have
    "R \<subseteq> \<lbrace>inv_of A l\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
ccompatible \<R> (PTA.inv_of A l)
R \<in> \<R>
u \<in> R
u \<turnstile> PTA.inv_of A l

goal (1 subgoal):
 1. R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
[PROOF STEP]
unfolding ccompatible_def ccval_def
[PROOF STATE]
proof (prove)
using this:
\<forall>R\<in>\<R>. R \<subseteq> {v. v \<turnstile> PTA.inv_of A l} \<or> {v. v \<turnstile> PTA.inv_of A l} \<inter> R = {}
R \<in> \<R>
u \<in> R
u \<turnstile> PTA.inv_of A l

goal (1 subgoal):
 1. R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}

goal (1 subgoal):
 1. \<S> \<noteq> {}
[PROOF STEP]
with st(1) R(1)
[PROOF STATE]
proof (chain)
picking this:
l \<in> L
R \<in> \<R>
R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l \<in> L
R \<in> \<R>
R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}

goal (1 subgoal):
 1. \<S> \<noteq> {}
[PROOF STEP]
unfolding \<S>_def
[PROOF STATE]
proof (prove)
using this:
l \<in> L
R \<in> \<R>
R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}

goal (1 subgoal):
 1. {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}} \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<S> \<noteq> {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<K>_\<S>_closed:
  assumes "s \<in> \<S>"
  shows "(\<Union>D\<in>\<K> s. set_pmf D) \<subseteq> \<S>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (set_pmf ` \<K> s) \<subseteq> \<S>
[PROOF STEP]
proof (safe, cases rule: \<K>.cases, blast, goal_cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a b x l R R'. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = return_pmf (l, R'); s \<in> \<S>; s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
 2. \<And>a b x l R g \<mu>. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>; s \<in> \<S>; s = (l, R); (l, g, \<mu>) \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
 3. \<And>a b x. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = return_pmf s\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
[PROOF STEP]
case (1 x a b l R)
[PROOF STATE]
proof (state)
this:
b \<in> \<K> s
(x, a) \<in> set_pmf b
b = return_pmf (l, R'_)
s \<in> \<S>
s = (l, R)
R'_ \<in> Succ \<R> R
R'_ \<subseteq> {v. v \<turnstile> PTA.inv_of A l}

goal (3 subgoals):
 1. \<And>a b x l R R'. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = return_pmf (l, R'); s \<in> \<S>; s = (l, R); R' \<in> Succ \<R> R; R' \<subseteq> {v. v \<turnstile> PTA.inv_of A l}\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
 2. \<And>a b x l R g \<mu>. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>; s \<in> \<S>; s = (l, R); (l, g, \<mu>) \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
 3. \<And>a b x. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = return_pmf s\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b \<in> \<K> s
(x, a) \<in> set_pmf b
b = return_pmf (l, R'_)
s \<in> \<S>
s = (l, R)
R'_ \<in> Succ \<R> R
R'_ \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
b \<in> \<K> s
(x, a) \<in> set_pmf b
b = return_pmf (l, R'_)
s \<in> \<S>
s = (l, R)
R'_ \<in> Succ \<R> R
R'_ \<subseteq> {v. v \<turnstile> PTA.inv_of A l}

goal (1 subgoal):
 1. (x, a) \<in> \<S>
[PROOF STEP]
unfolding \<S>_def
[PROOF STATE]
proof (prove)
using this:
b \<in> \<K> s
(x, a) \<in> set_pmf b
b = return_pmf (l, R'_)
s \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}}
s = (l, R)
R'_ \<in> Succ \<R> R
R'_ \<subseteq> {v. v \<turnstile> PTA.inv_of A l}

goal (1 subgoal):
 1. (x, a) \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}}
[PROOF STEP]
by (auto intro: alpha_interp.succ_ex(1))
[PROOF STATE]
proof (state)
this:
(x, a) \<in> \<S>

goal (2 subgoals):
 1. \<And>a b x l R g \<mu>. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>; s \<in> \<S>; s = (l, R); (l, g, \<mu>) \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
 2. \<And>a b x. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = return_pmf s\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b x l R g \<mu>. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>; s \<in> \<S>; s = (l, R); (l, g, \<mu>) \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
 2. \<And>a b x. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = return_pmf s\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
[PROOF STEP]
case (3 a b x)
[PROOF STATE]
proof (state)
this:
x \<in> \<K> s
(a, b) \<in> set_pmf x
x = return_pmf s

goal (2 subgoals):
 1. \<And>a b x l R g \<mu>. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>; s \<in> \<S>; s = (l, R); (l, g, \<mu>) \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
 2. \<And>a b x. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = return_pmf s\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
[PROOF STEP]
with \<open>s \<in> \<S>\<close>
[PROOF STATE]
proof (chain)
picking this:
s \<in> \<S>
x \<in> \<K> s
(a, b) \<in> set_pmf x
x = return_pmf s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
s \<in> \<S>
x \<in> \<K> s
(a, b) \<in> set_pmf x
x = return_pmf s

goal (1 subgoal):
 1. (a, b) \<in> \<S>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a, b) \<in> \<S>

goal (1 subgoal):
 1. \<And>a b x l R g \<mu>. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>; s \<in> \<S>; s = (l, R); (l, g, \<mu>) \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b x l R g \<mu>. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>; s \<in> \<S>; s = (l, R); (l, g, \<mu>) \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
[PROOF STEP]
case prems: (2 l' R' p l R g \<mu>)
[PROOF STATE]
proof (state)
this:
p \<in> \<K> s
(l', R') \<in> set_pmf p
p = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>
s \<in> \<S>
s = (l, R)
(l, g, \<mu>) \<in> PTA.trans_of A
R \<subseteq> {v. v \<turnstile> g}

goal (1 subgoal):
 1. \<And>a b x l R g \<mu>. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>; s \<in> \<S>; s = (l, R); (l, g, \<mu>) \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> \<K> s
(l', R') \<in> set_pmf p
p = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>
s \<in> \<S>
s = (l, R)
(l, g, \<mu>) \<in> PTA.trans_of A
R \<subseteq> {v. v \<turnstile> g}
[PROOF STEP]
obtain X where *: "(X, l') \<in> set_pmf \<mu>" "R' = region_set' R (SOME r. set r = X) 0"
[PROOF STATE]
proof (prove)
using this:
p \<in> \<K> s
(l', R') \<in> set_pmf p
p = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>
s \<in> \<S>
s = (l, R)
(l, g, \<mu>) \<in> PTA.trans_of A
R \<subseteq> {v. v \<turnstile> g}

goal (1 subgoal):
 1. (\<And>X. \<lbrakk>(X, l') \<in> set_pmf \<mu>; R' = [X::=0]R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(X, l') \<in> set_pmf \<mu>
R' = [X::=0]R

goal (1 subgoal):
 1. \<And>a b x l R g \<mu>. \<lbrakk>x \<in> \<K> s; (a, b) \<in> set_pmf x; x = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>; s \<in> \<S>; s = (l, R); (l, g, \<mu>) \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> g}\<rbrakk> \<Longrightarrow> (a, b) \<in> \<S>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l', R') \<in> \<S>
[PROOF STEP]
unfolding \<S>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l', R') \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}}
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. l' \<in> L
 2. R' \<in> \<R>
 3. \<And>x. x \<in> R' \<Longrightarrow> x \<turnstile> PTA.inv_of A l'
[PROOF STEP]
from *(1)
[PROOF STATE]
proof (chain)
picking this:
(X, l') \<in> set_pmf \<mu>
[PROOF STEP]
have "(l, g, \<mu>, X, l') \<in> edges (l,g, \<mu>)"
[PROOF STATE]
proof (prove)
using this:
(X, l') \<in> set_pmf \<mu>

goal (1 subgoal):
 1. (l, g, \<mu>, X, l') \<in> edges (l, g, \<mu>)
[PROOF STEP]
unfolding edges_def
[PROOF STATE]
proof (prove)
using this:
(X, l') \<in> set_pmf \<mu>

goal (1 subgoal):
 1. (l, g, \<mu>, X, l') \<in> (case (l, g, \<mu>) of (l, g, p) \<Rightarrow> {(l, g, p, X, l') |X l'. (X, l') \<in> set_pmf p})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(l, g, \<mu>, X, l') \<in> edges (l, g, \<mu>)

goal (3 subgoals):
 1. l' \<in> L
 2. R' \<in> \<R>
 3. \<And>x. x \<in> R' \<Longrightarrow> x \<turnstile> PTA.inv_of A l'
[PROOF STEP]
with prems(6)
[PROOF STATE]
proof (chain)
picking this:
(l, g, \<mu>) \<in> PTA.trans_of A
(l, g, \<mu>, X, l') \<in> edges (l, g, \<mu>)
[PROOF STEP]
have "(l, g, \<mu>, X, l') \<in> Edges A"
[PROOF STATE]
proof (prove)
using this:
(l, g, \<mu>) \<in> PTA.trans_of A
(l, g, \<mu>, X, l') \<in> edges (l, g, \<mu>)

goal (1 subgoal):
 1. A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'
[PROOF STEP]
unfolding Edges_def trans_of_def
[PROOF STATE]
proof (prove)
using this:
(l, g, \<mu>) \<in> fst A
(l, g, \<mu>, X, l') \<in> edges (l, g, \<mu>)

goal (1 subgoal):
 1. (l, g, \<mu>, X, l') \<in> \<Union> {edges t |t. t \<in> fst A}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'

goal (3 subgoals):
 1. l' \<in> L
 2. R' \<in> \<R>
 3. \<And>x. x \<in> R' \<Longrightarrow> x \<turnstile> PTA.inv_of A l'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'
[PROOF STEP]
show "l' \<in> L"
[PROOF STATE]
proof (prove)
using this:
A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'

goal (1 subgoal):
 1. l' \<in> L
[PROOF STEP]
unfolding L_def locations_def
[PROOF STATE]
proof (prove)
using this:
A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'

goal (1 subgoal):
 1. l' \<in> fst ` Edges A \<union> (snd \<circ> snd \<circ> snd \<circ> snd) ` Edges A
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
l' \<in> L

goal (2 subgoals):
 1. R' \<in> \<R>
 2. \<And>x. x \<in> R' \<Longrightarrow> x \<turnstile> PTA.inv_of A l'
[PROOF STEP]
show "u \<turnstile> inv_of A l'" if "u \<in> R'" for u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<turnstile> PTA.inv_of A l'
[PROOF STEP]
using admissible_targets'[OF prems(6) *(1) prems(7)] *(2) that
[PROOF STATE]
proof (prove)
using this:
[X::=0]R \<subseteq> {v. v \<turnstile> PTA.inv_of A l'}
R' = [X::=0]R
u \<in> R'

goal (1 subgoal):
 1. u \<turnstile> PTA.inv_of A l'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?u3 \<in> R' \<Longrightarrow> ?u3 \<turnstile> PTA.inv_of A l'

goal (1 subgoal):
 1. R' \<in> \<R>
[PROOF STEP]
from admissible_targets(2)[OF prems(6) *(1)]
[PROOF STATE]
proof (chain)
picking this:
X \<subseteq> clocks A
[PROOF STEP]
have "X \<subseteq> \<X>"
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> clocks A

goal (1 subgoal):
 1. X \<subseteq> \<X>
[PROOF STEP]
unfolding \<X>_def
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> clocks A

goal (1 subgoal):
 1. X \<subseteq> clocks A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X \<subseteq> \<X>

goal (1 subgoal):
 1. R' \<in> \<R>
[PROOF STEP]
with finite(1)
[PROOF STATE]
proof (chain)
picking this:
finite \<X>
X \<subseteq> \<X>
[PROOF STEP]
have "finite X"
[PROOF STATE]
proof (prove)
using this:
finite \<X>
X \<subseteq> \<X>

goal (1 subgoal):
 1. finite X
[PROOF STEP]
by (blast intro: finite_subset)
[PROOF STATE]
proof (state)
this:
finite X

goal (1 subgoal):
 1. R' \<in> \<R>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite X
[PROOF STEP]
obtain r where "set r = X"
[PROOF STATE]
proof (prove)
using this:
finite X

goal (1 subgoal):
 1. (\<And>r. set r = X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_list
[PROOF STATE]
proof (prove)
using this:
finite X
finite ?A \<Longrightarrow> \<exists>xs. set xs = ?A

goal (1 subgoal):
 1. (\<And>r. set r = X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set r = X

goal (1 subgoal):
 1. R' \<in> \<R>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set r = X
[PROOF STEP]
have "set (SOME r. set r = X) = X"
[PROOF STATE]
proof (prove)
using this:
set r = X

goal (1 subgoal):
 1. set (SOME r. set r = X) = X
[PROOF STEP]
by (rule someI)
[PROOF STATE]
proof (state)
this:
set (SOME r. set r = X) = X

goal (1 subgoal):
 1. R' \<in> \<R>
[PROOF STEP]
with \<open>X \<subseteq> \<X>\<close>
[PROOF STATE]
proof (chain)
picking this:
X \<subseteq> \<X>
set (SOME r. set r = X) = X
[PROOF STEP]
have "set (SOME r. set r = X) \<subseteq> \<X>"
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<X>
set (SOME r. set r = X) = X

goal (1 subgoal):
 1. set (SOME r. set r = X) \<subseteq> \<X>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (SOME r. set r = X) \<subseteq> \<X>

goal (1 subgoal):
 1. R' \<in> \<R>
[PROOF STEP]
with alpha_interp.region_set'_closed[of R 0 "SOME r. set r = X"] prems(4,5) *(2)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>R \<in> \<R>; 0 \<le> 0; \<forall>x\<in>set (SOME r. set r = X). 0 \<le> k x; set (SOME r. set r = X) \<subseteq> \<X>\<rbrakk> \<Longrightarrow> [X::=real 0]R \<in> \<R>
s \<in> \<S>
s = (l, R)
R' = [X::=0]R
set (SOME r. set r = X) \<subseteq> \<X>
[PROOF STEP]
show "R' \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>R \<in> \<R>; 0 \<le> 0; \<forall>x\<in>set (SOME r. set r = X). 0 \<le> k x; set (SOME r. set r = X) \<subseteq> \<X>\<rbrakk> \<Longrightarrow> [X::=real 0]R \<in> \<R>
s \<in> \<S>
s = (l, R)
R' = [X::=0]R
set (SOME r. set r = X) \<subseteq> \<X>

goal (1 subgoal):
 1. R' \<in> \<R>
[PROOF STEP]
unfolding \<S>_def \<X>_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>R \<in> Regions.\<R> (clocks A) k; 0 \<le> 0; \<forall>x\<in>set (SOME r. set r = X). 0 \<le> k x; set (SOME r. set r = X) \<subseteq> clocks A\<rbrakk> \<Longrightarrow> [X::=real 0]R \<in> Regions.\<R> (clocks A) k
s \<in> {(l, R). l \<in> L \<and> R \<in> Regions.\<R> (clocks A) k \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}}
s = (l, R)
R' = [X::=0]R
set (SOME r. set r = X) \<subseteq> clocks A

goal (1 subgoal):
 1. R' \<in> Regions.\<R> (clocks A) k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R' \<in> \<R>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(l', R') \<in> \<S>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ccompatible_inv:
  shows "ccompatible \<R> (inv_of A l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccompatible \<R> (PTA.inv_of A l)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ccompatible \<R> (PTA.inv_of A l)
[PROOF STEP]
from valid
[PROOF STATE]
proof (chain)
picking this:
PTA.valid_abstraction A \<X> (\<lambda>x. real (k x))
[PROOF STEP]
have
    "\<forall>(x, m)\<in>collect_clock_pairs (inv_of A l). m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>"
[PROOF STATE]
proof (prove)
using this:
PTA.valid_abstraction A \<X> (\<lambda>x. real (k x))

goal (1 subgoal):
 1. \<forall>(x, m)\<in>collect_clock_pairs (PTA.inv_of A l). m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>
[PROOF STEP]
unfolding valid_abstraction_def clkp_set_def collect_clki_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>(x, m)\<in>\<Union> {collect_clock_pairs (PTA.inv_of A x) |x. True} \<union> PTA.collect_clkt (PTA.trans_of A). m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>) \<and> PTA.collect_clkvt A \<subseteq> \<X> \<and> finite \<X>

goal (1 subgoal):
 1. \<forall>(x, m)\<in>collect_clock_pairs (PTA.inv_of A l). m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>(x, m)\<in>collect_clock_pairs (PTA.inv_of A l). m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>

goal (1 subgoal):
 1. ccompatible \<R> (PTA.inv_of A l)
[PROOF STEP]
with ccompatible[of _ k \<X>, folded \<R>_def]
[PROOF STATE]
proof (chain)
picking this:
\<forall>(x, m)\<in>collect_clock_pairs ?cc. m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat> \<Longrightarrow> ccompatible \<R> ?cc
\<forall>(x, m)\<in>collect_clock_pairs (PTA.inv_of A l). m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>(x, m)\<in>collect_clock_pairs ?cc. m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat> \<Longrightarrow> ccompatible \<R> ?cc
\<forall>(x, m)\<in>collect_clock_pairs (PTA.inv_of A l). m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>

goal (1 subgoal):
 1. ccompatible \<R> (PTA.inv_of A l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ccompatible \<R> (PTA.inv_of A l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ccompatible_guard:
  assumes "(l, g, \<mu>) \<in> trans_of A"
  shows "ccompatible \<R> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ccompatible \<R> g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ccompatible \<R> g
[PROOF STEP]
from assms valid
[PROOF STATE]
proof (chain)
picking this:
(l, g, \<mu>) \<in> PTA.trans_of A
PTA.valid_abstraction A \<X> (\<lambda>x. real (k x))
[PROOF STEP]
have
    "\<forall>(x, m)\<in>collect_clock_pairs g. m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>"
[PROOF STATE]
proof (prove)
using this:
(l, g, \<mu>) \<in> PTA.trans_of A
PTA.valid_abstraction A \<X> (\<lambda>x. real (k x))

goal (1 subgoal):
 1. \<forall>(x, m)\<in>collect_clock_pairs g. m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>
[PROOF STEP]
unfolding valid_abstraction_def clkp_set_def collect_clkt_def trans_of_def
[PROOF STATE]
proof (prove)
using this:
(l, g, \<mu>) \<in> fst A
(\<forall>(x, m)\<in>PTA.collect_clki (PTA.inv_of A) \<union> \<Union> {collect_clock_pairs (fst (snd t)) |t. t \<in> fst A}. m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>) \<and> PTA.collect_clkvt A \<subseteq> \<X> \<and> finite \<X>

goal (1 subgoal):
 1. \<forall>(x, m)\<in>collect_clock_pairs g. m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>(x, m)\<in>collect_clock_pairs g. m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>

goal (1 subgoal):
 1. ccompatible \<R> g
[PROOF STEP]
with assms ccompatible[of _ k \<X>, folded \<R>_def]
[PROOF STATE]
proof (chain)
picking this:
(l, g, \<mu>) \<in> PTA.trans_of A
\<forall>(x, m)\<in>collect_clock_pairs ?cc. m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat> \<Longrightarrow> ccompatible \<R> ?cc
\<forall>(x, m)\<in>collect_clock_pairs g. m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(l, g, \<mu>) \<in> PTA.trans_of A
\<forall>(x, m)\<in>collect_clock_pairs ?cc. m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat> \<Longrightarrow> ccompatible \<R> ?cc
\<forall>(x, m)\<in>collect_clock_pairs g. m \<le> real (k x) \<and> x \<in> \<X> \<and> m \<in> \<nat>

goal (1 subgoal):
 1. ccompatible \<R> g
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ccompatible \<R> g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma region_set'_eq:
  fixes X :: "'c set"
  assumes "R \<in> \<R>" "u \<in> R"
      and "A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'"
  shows
    "[[X:=0]u]\<^sub>\<R> = region_set' R (SOME r. set r = X) 0" "[[X:=0]u]\<^sub>\<R> \<in> \<R>" "[X:=0]u \<in> [[X:=0]u]\<^sub>\<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> = [X::=0]R &&& [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> \<in> \<R> &&& [(SOME r. set r = X)\<rightarrow>0]u \<in> [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> = [X::=0]R
 2. [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>
 3. [(SOME r. set r = X)\<rightarrow>0]u \<in> [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R>
[PROOF STEP]
let ?r = "(SOME r. set r = X)"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> = [X::=0]R
 2. [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>
 3. [(SOME r. set r = X)\<rightarrow>0]u \<in> [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R>
[PROOF STEP]
from admissible_targets_alt[OF assms(3)] \<X>_def finite
[PROOF STATE]
proof (chain)
picking this:
{v. v \<turnstile> g}\<^bsub>X \<rightarrow> 0\<^esub> \<subseteq> {v. v \<turnstile> PTA.inv_of A l'}
X \<subseteq> clocks A
\<X> = clocks A
finite \<X>
finite L
finite (PTA.trans_of A)
[PROOF STEP]
have "finite X"
[PROOF STATE]
proof (prove)
using this:
{v. v \<turnstile> g}\<^bsub>X \<rightarrow> 0\<^esub> \<subseteq> {v. v \<turnstile> PTA.inv_of A l'}
X \<subseteq> clocks A
\<X> = clocks A
finite \<X>
finite L
finite (PTA.trans_of A)

goal (1 subgoal):
 1. finite X
[PROOF STEP]
by (auto intro: finite_subset)
[PROOF STATE]
proof (state)
this:
finite X

goal (3 subgoals):
 1. [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> = [X::=0]R
 2. [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>
 3. [(SOME r. set r = X)\<rightarrow>0]u \<in> [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite X
[PROOF STEP]
obtain r where "set r = X"
[PROOF STATE]
proof (prove)
using this:
finite X

goal (1 subgoal):
 1. (\<And>r. set r = X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_list
[PROOF STATE]
proof (prove)
using this:
finite X
finite ?A \<Longrightarrow> \<exists>xs. set xs = ?A

goal (1 subgoal):
 1. (\<And>r. set r = X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set r = X

goal (3 subgoals):
 1. [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> = [X::=0]R
 2. [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>
 3. [(SOME r. set r = X)\<rightarrow>0]u \<in> [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set r = X
[PROOF STEP]
have "set ?r = X"
[PROOF STATE]
proof (prove)
using this:
set r = X

goal (1 subgoal):
 1. set (SOME r. set r = X) = X
[PROOF STEP]
by (intro someI)
[PROOF STATE]
proof (state)
this:
set (SOME r. set r = X) = X

goal (3 subgoals):
 1. [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> = [X::=0]R
 2. [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>
 3. [(SOME r. set r = X)\<rightarrow>0]u \<in> [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R>
[PROOF STEP]
with valid assms(3)
[PROOF STATE]
proof (chain)
picking this:
PTA.valid_abstraction A \<X> (\<lambda>x. real (k x))
A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'
set (SOME r. set r = X) = X
[PROOF STEP]
have "set ?r \<subseteq> \<X>"
[PROOF STATE]
proof (prove)
using this:
PTA.valid_abstraction A \<X> (\<lambda>x. real (k x))
A \<turnstile> l \<longrightarrow>\<^bsup>g,\<mu>,X\<^esup> l'
set (SOME r. set r = X) = X

goal (1 subgoal):
 1. set (SOME r. set r = X) \<subseteq> \<X>
[PROOF STEP]
by (simp add: transition_\<X>)
[PROOF STATE]
proof (state)
this:
set (SOME r. set r = X) \<subseteq> \<X>

goal (3 subgoals):
 1. [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> = [X::=0]R
 2. [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>
 3. [(SOME r. set r = X)\<rightarrow>0]u \<in> [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R>
[PROOF STEP]
from region_set'_id[of _ \<X> k, folded \<R>_def, OF assms(1,2) finite(1) _ _ this]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 \<le> ?c; \<forall>x\<in>set (SOME r. set r = X). ?c \<le> k x\<rbrakk> \<Longrightarrow> [[(SOME r. set r = X)\<rightarrow>real ?c]u]\<^sub>\<R> = [X::=real ?c]R \<and> [[(SOME r. set r = X)\<rightarrow>real ?c]u]\<^sub>\<R> \<in> \<R> \<and> [(SOME r. set r = X)\<rightarrow>real ?c]u \<in> [[(SOME r. set r = X)\<rightarrow>real ?c]u]\<^sub>\<R>
[PROOF STEP]
show
    "[[X:=0]u]\<^sub>\<R> = region_set' R (SOME r. set r = X) 0" "[[X:=0]u]\<^sub>\<R> \<in> \<R>" "[X:=0]u \<in> [[X:=0]u]\<^sub>\<R>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> ?c; \<forall>x\<in>set (SOME r. set r = X). ?c \<le> k x\<rbrakk> \<Longrightarrow> [[(SOME r. set r = X)\<rightarrow>real ?c]u]\<^sub>\<R> = [X::=real ?c]R \<and> [[(SOME r. set r = X)\<rightarrow>real ?c]u]\<^sub>\<R> \<in> \<R> \<and> [(SOME r. set r = X)\<rightarrow>real ?c]u \<in> [[(SOME r. set r = X)\<rightarrow>real ?c]u]\<^sub>\<R>

goal (1 subgoal):
 1. [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> = [X::=0]R &&& [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> \<in> \<R> &&& [(SOME r. set r = X)\<rightarrow>0]u \<in> [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R>
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
[[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> = [X::=0]R
[[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>
[(SOME r. set r = X)\<rightarrow>0]u \<in> [[(SOME r. set r = X)\<rightarrow>0]u]\<^sub>\<R>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma regions_part_ex_reset:
  assumes "u \<in> V"
  shows  "[r \<rightarrow> (d::nat)]u \<in> [[r \<rightarrow> d]u]\<^sub>\<R>" "[[r \<rightarrow> d]u]\<^sub>\<R> \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [r\<rightarrow>real d]u \<in> [[r\<rightarrow>real d]u]\<^sub>\<R> &&& [[r\<rightarrow>real d]u]\<^sub>\<R> \<in> \<R>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<in> V

goal (1 subgoal):
 1. [r\<rightarrow>real d]u \<in> [[r\<rightarrow>real d]u]\<^sub>\<R> &&& [[r\<rightarrow>real d]u]\<^sub>\<R> \<in> \<R>
[PROOF STEP]
by auto


[STATEMENT]
lemma reset_sets_all_equiv:
  assumes "u \<in> V" "u' \<in> [[r \<rightarrow> (d :: nat)]u]\<^sub>\<R>" "x \<in> set r" "set r \<subseteq> \<X>" "d \<le> k x"
  shows "u' x = d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u' x = real d
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u' x = real d
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
u \<in> V
[PROOF STEP]
have u: "[r \<rightarrow> d]u \<in> [[r \<rightarrow> d]u]\<^sub>\<R>" "[[r \<rightarrow> d]u]\<^sub>\<R> \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
u \<in> V

goal (1 subgoal):
 1. [r\<rightarrow>real d]u \<in> [[r\<rightarrow>real d]u]\<^sub>\<R> &&& [[r\<rightarrow>real d]u]\<^sub>\<R> \<in> \<R>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[r\<rightarrow>real d]u \<in> [[r\<rightarrow>real d]u]\<^sub>\<R>
[[r\<rightarrow>real d]u]\<^sub>\<R> \<in> \<R>

goal (1 subgoal):
 1. u' x = real d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[r\<rightarrow>real d]u \<in> [[r\<rightarrow>real d]u]\<^sub>\<R>
[[r\<rightarrow>real d]u]\<^sub>\<R> \<in> \<R>
[PROOF STEP]
obtain I \<rho> where I: "[[r \<rightarrow> d]u]\<^sub>\<R> = region \<X> I \<rho>" "valid_region \<X> k I \<rho>"
[PROOF STATE]
proof (prove)
using this:
[r\<rightarrow>real d]u \<in> [[r\<rightarrow>real d]u]\<^sub>\<R>
[[r\<rightarrow>real d]u]\<^sub>\<R> \<in> \<R>

goal (1 subgoal):
 1. (\<And>I \<rho>. \<lbrakk>[[r\<rightarrow>real d]u]\<^sub>\<R> = Regions.region \<X> I \<rho>; Regions.valid_region \<X> k I \<rho>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: \<R>_def)
[PROOF STATE]
proof (state)
this:
[[r\<rightarrow>real d]u]\<^sub>\<R> = Regions.region \<X> I \<rho>
Regions.valid_region \<X> k I \<rho>

goal (1 subgoal):
 1. u' x = real d
[PROOF STEP]
with u(1) assms(3-)
[PROOF STATE]
proof (chain)
picking this:
[r\<rightarrow>real d]u \<in> [[r\<rightarrow>real d]u]\<^sub>\<R>
x \<in> set r
set r \<subseteq> \<X>
d \<le> k x
[[r\<rightarrow>real d]u]\<^sub>\<R> = Regions.region \<X> I \<rho>
Regions.valid_region \<X> k I \<rho>
[PROOF STEP]
have "intv_elem x ([r \<rightarrow> d]u) (I x)" "valid_intv (k x) (I x)"
[PROOF STATE]
proof (prove)
using this:
[r\<rightarrow>real d]u \<in> [[r\<rightarrow>real d]u]\<^sub>\<R>
x \<in> set r
set r \<subseteq> \<X>
d \<le> k x
[[r\<rightarrow>real d]u]\<^sub>\<R> = Regions.region \<X> I \<rho>
Regions.valid_region \<X> k I \<rho>

goal (1 subgoal):
 1. Regions.intv_elem x ([r\<rightarrow>real d]u) (I x) &&& Regions.valid_intv (k x) (I x)
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
Regions.intv_elem x ([r\<rightarrow>real d]u) (I x)
Regions.valid_intv (k x) (I x)

goal (1 subgoal):
 1. u' x = real d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Regions.intv_elem x ([r\<rightarrow>real d]u) (I x)
Regions.valid_intv (k x) (I x)

goal (1 subgoal):
 1. u' x = real d
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
u \<in> V
u' \<in> [[r\<rightarrow>real d]u]\<^sub>\<R>
x \<in> set r
set r \<subseteq> \<X>
d \<le> k x
[PROOF STEP]
have "([r \<rightarrow> d]u) x = d"
[PROOF STATE]
proof (prove)
using this:
u \<in> V
u' \<in> [[r\<rightarrow>real d]u]\<^sub>\<R>
x \<in> set r
set r \<subseteq> \<X>
d \<le> k x

goal (1 subgoal):
 1. ([r\<rightarrow>real d]u) x = real d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
([r\<rightarrow>real d]u) x = real d

goal (1 subgoal):
 1. u' x = real d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Regions.intv_elem x ([r\<rightarrow>real d]u) (I x)
Regions.valid_intv (k x) (I x)
([r\<rightarrow>real d]u) x = real d
[PROOF STEP]
have "I x = Const d"
[PROOF STATE]
proof (prove)
using this:
Regions.intv_elem x ([r\<rightarrow>real d]u) (I x)
Regions.valid_intv (k x) (I x)
([r\<rightarrow>real d]u) x = real d

goal (1 subgoal):
 1. I x = Regions.intv.Const d
[PROOF STEP]
using assms(5)
[PROOF STATE]
proof (prove)
using this:
Regions.intv_elem x ([r\<rightarrow>real d]u) (I x)
Regions.valid_intv (k x) (I x)
([r\<rightarrow>real d]u) x = real d
d \<le> k x

goal (1 subgoal):
 1. I x = Regions.intv.Const d
[PROOF STEP]
by (cases "I x") auto
[PROOF STATE]
proof (state)
this:
I x = Regions.intv.Const d

goal (1 subgoal):
 1. u' x = real d
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
I x = Regions.intv.Const d

goal (1 subgoal):
 1. u' x = real d
[PROOF STEP]
from I assms(2-)
[PROOF STATE]
proof (chain)
picking this:
[[r\<rightarrow>real d]u]\<^sub>\<R> = Regions.region \<X> I \<rho>
Regions.valid_region \<X> k I \<rho>
u' \<in> [[r\<rightarrow>real d]u]\<^sub>\<R>
x \<in> set r
set r \<subseteq> \<X>
d \<le> k x
[PROOF STEP]
have "intv_elem x u' (I x)"
[PROOF STATE]
proof (prove)
using this:
[[r\<rightarrow>real d]u]\<^sub>\<R> = Regions.region \<X> I \<rho>
Regions.valid_region \<X> k I \<rho>
u' \<in> [[r\<rightarrow>real d]u]\<^sub>\<R>
x \<in> set r
set r \<subseteq> \<X>
d \<le> k x

goal (1 subgoal):
 1. Regions.intv_elem x u' (I x)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Regions.intv_elem x u' (I x)

goal (1 subgoal):
 1. u' x = real d
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
I x = Regions.intv.Const d
Regions.intv_elem x u' (I x)
[PROOF STEP]
show "u' x = d"
[PROOF STATE]
proof (prove)
using this:
I x = Regions.intv.Const d
Regions.intv_elem x u' (I x)

goal (1 subgoal):
 1. u' x = real d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u' x = real d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reset_eq:
  assumes "u \<in> V" "([[r \<rightarrow> 0]u]\<^sub>\<R>) = ([[r' \<rightarrow> 0]u]\<^sub>\<R>)" "set r \<subseteq> \<X>" "set r' \<subseteq> \<X>"
  shows "[r \<rightarrow> 0]u = [r' \<rightarrow> 0]u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [r\<rightarrow>0]u = [r'\<rightarrow>0]u
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u \<in> V
[[r\<rightarrow>0]u]\<^sub>\<R> = [[r'\<rightarrow>0]u]\<^sub>\<R>
set r \<subseteq> \<X>
set r' \<subseteq> \<X>

goal (1 subgoal):
 1. [r\<rightarrow>0]u = [r'\<rightarrow>0]u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>u \<in> V; [[r\<rightarrow>0]u]\<^sub>\<R> = [[r'\<rightarrow>0]u]\<^sub>\<R>; set r \<subseteq> \<X>; set r' \<subseteq> \<X>\<rbrakk> \<Longrightarrow> [r\<rightarrow>0]u = [r'\<rightarrow>0]u
[PROOF STEP]
have *: "u' x = 0" if "u' \<in> [[r \<rightarrow> 0]u]\<^sub>\<R>" "x \<in> set r" for u' x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u' x = 0
[PROOF STEP]
using reset_sets_all_equiv[of u u' r 0 x] that assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>u \<in> V; u' \<in> [[r\<rightarrow>real 0]u]\<^sub>\<R>; x \<in> set r; set r \<subseteq> \<X>; 0 \<le> k x\<rbrakk> \<Longrightarrow> u' x = real 0
u' \<in> [[r\<rightarrow>0]u]\<^sub>\<R>
x \<in> set r
u \<in> V
[[r\<rightarrow>0]u]\<^sub>\<R> = [[r'\<rightarrow>0]u]\<^sub>\<R>
set r \<subseteq> \<X>
set r' \<subseteq> \<X>

goal (1 subgoal):
 1. u' x = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?u'3 \<in> [[r\<rightarrow>0]u]\<^sub>\<R>; ?x3 \<in> set r\<rbrakk> \<Longrightarrow> ?u'3 ?x3 = 0

goal (1 subgoal):
 1. \<lbrakk>u \<in> V; [[r\<rightarrow>0]u]\<^sub>\<R> = [[r'\<rightarrow>0]u]\<^sub>\<R>; set r \<subseteq> \<X>; set r' \<subseteq> \<X>\<rbrakk> \<Longrightarrow> [r\<rightarrow>0]u = [r'\<rightarrow>0]u
[PROOF STEP]
have "u' x = 0" if "u' \<in> [[r' \<rightarrow> 0]u]\<^sub>\<R>" "x \<in> set r'" for u' x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u' x = 0
[PROOF STEP]
using reset_sets_all_equiv[of u u' r' 0 x] that assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>u \<in> V; u' \<in> [[r'\<rightarrow>real 0]u]\<^sub>\<R>; x \<in> set r'; set r' \<subseteq> \<X>; 0 \<le> k x\<rbrakk> \<Longrightarrow> u' x = real 0
u' \<in> [[r'\<rightarrow>0]u]\<^sub>\<R>
x \<in> set r'
u \<in> V
[[r\<rightarrow>0]u]\<^sub>\<R> = [[r'\<rightarrow>0]u]\<^sub>\<R>
set r \<subseteq> \<X>
set r' \<subseteq> \<X>

goal (1 subgoal):
 1. u' x = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?u'3 \<in> [[r'\<rightarrow>0]u]\<^sub>\<R>; ?x3 \<in> set r'\<rbrakk> \<Longrightarrow> ?u'3 ?x3 = 0

goal (1 subgoal):
 1. \<lbrakk>u \<in> V; [[r\<rightarrow>0]u]\<^sub>\<R> = [[r'\<rightarrow>0]u]\<^sub>\<R>; set r \<subseteq> \<X>; set r' \<subseteq> \<X>\<rbrakk> \<Longrightarrow> [r\<rightarrow>0]u = [r'\<rightarrow>0]u
[PROOF STEP]
from regions_part_ex_reset[OF assms(1), of _ 0] assms(2)
[PROOF STATE]
proof (chain)
picking this:
[?r\<rightarrow>real 0]u \<in> [[?r\<rightarrow>real 0]u]\<^sub>\<R>
[[?r\<rightarrow>real 0]u]\<^sub>\<R> \<in> \<R>
[[r\<rightarrow>0]u]\<^sub>\<R> = [[r'\<rightarrow>0]u]\<^sub>\<R>
[PROOF STEP]
have **:
    "([r' \<rightarrow> 0]u) \<in> [[r \<rightarrow> 0]u]\<^sub>\<R>" "([r \<rightarrow> 0]u) \<in> [[r \<rightarrow> 0]u]\<^sub>\<R>" "[[r \<rightarrow> 0]u]\<^sub>\<R> \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
[?r\<rightarrow>real 0]u \<in> [[?r\<rightarrow>real 0]u]\<^sub>\<R>
[[?r\<rightarrow>real 0]u]\<^sub>\<R> \<in> \<R>
[[r\<rightarrow>0]u]\<^sub>\<R> = [[r'\<rightarrow>0]u]\<^sub>\<R>

goal (1 subgoal):
 1. [r'\<rightarrow>0]u \<in> [[r\<rightarrow>0]u]\<^sub>\<R> &&& [r\<rightarrow>0]u \<in> [[r\<rightarrow>0]u]\<^sub>\<R> &&& [[r\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[r'\<rightarrow>0]u \<in> [[r\<rightarrow>0]u]\<^sub>\<R>
[r\<rightarrow>0]u \<in> [[r\<rightarrow>0]u]\<^sub>\<R>
[[r\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>

goal (1 subgoal):
 1. \<lbrakk>u \<in> V; [[r\<rightarrow>0]u]\<^sub>\<R> = [[r'\<rightarrow>0]u]\<^sub>\<R>; set r \<subseteq> \<X>; set r' \<subseteq> \<X>\<rbrakk> \<Longrightarrow> [r\<rightarrow>0]u = [r'\<rightarrow>0]u
[PROOF STEP]
have "(([r \<rightarrow> 0]u) x) = (([r' \<rightarrow> 0]u) x)" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
proof (cases "x \<in> set r")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> set r \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
 2. x \<notin> set r \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> set r

goal (2 subgoals):
 1. x \<in> set r \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
 2. x \<notin> set r \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set r
[PROOF STEP]
have "([r \<rightarrow> 0]u) x = 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> set r

goal (1 subgoal):
 1. ([r\<rightarrow>0]u) x = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
([r\<rightarrow>0]u) x = 0

goal (2 subgoals):
 1. x \<in> set r \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
 2. x \<notin> set r \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
([r\<rightarrow>0]u) x = 0

goal (2 subgoals):
 1. x \<in> set r \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
 2. x \<notin> set r \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
from * ** True
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?u'3 \<in> [[r\<rightarrow>0]u]\<^sub>\<R>; ?x3 \<in> set r\<rbrakk> \<Longrightarrow> ?u'3 ?x3 = 0
[r'\<rightarrow>0]u \<in> [[r\<rightarrow>0]u]\<^sub>\<R>
[r\<rightarrow>0]u \<in> [[r\<rightarrow>0]u]\<^sub>\<R>
[[r\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>
x \<in> set r
[PROOF STEP]
have "([r' \<rightarrow> 0]u) x = 0"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?u'3 \<in> [[r\<rightarrow>0]u]\<^sub>\<R>; ?x3 \<in> set r\<rbrakk> \<Longrightarrow> ?u'3 ?x3 = 0
[r'\<rightarrow>0]u \<in> [[r\<rightarrow>0]u]\<^sub>\<R>
[r\<rightarrow>0]u \<in> [[r\<rightarrow>0]u]\<^sub>\<R>
[[r\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>
x \<in> set r

goal (1 subgoal):
 1. ([r'\<rightarrow>0]u) x = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([r'\<rightarrow>0]u) x = 0

goal (2 subgoals):
 1. x \<in> set r \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
 2. x \<notin> set r \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
([r\<rightarrow>0]u) x = 0
([r'\<rightarrow>0]u) x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
([r\<rightarrow>0]u) x = 0
([r'\<rightarrow>0]u) x = 0

goal (1 subgoal):
 1. ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x

goal (1 subgoal):
 1. x \<notin> set r \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> set r \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> set r

goal (1 subgoal):
 1. x \<notin> set r \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> set r
[PROOF STEP]
have id: "([r\<rightarrow>0]u) x = u x"
[PROOF STATE]
proof (prove)
using this:
x \<notin> set r

goal (1 subgoal):
 1. ([r\<rightarrow>0]u) x = u x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
([r\<rightarrow>0]u) x = u x

goal (1 subgoal):
 1. x \<notin> set r \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
proof (cases "x \<in> set r'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> set r' \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
 2. x \<notin> set r' \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> set r'

goal (2 subgoals):
 1. x \<in> set r' \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
 2. x \<notin> set r' \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set r'
[PROOF STEP]
have reset: "([r' \<rightarrow> 0]u) x = 0"
[PROOF STATE]
proof (prove)
using this:
x \<in> set r'

goal (1 subgoal):
 1. ([r'\<rightarrow>0]u) x = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
([r'\<rightarrow>0]u) x = 0

goal (2 subgoals):
 1. x \<in> set r' \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
 2. x \<notin> set r' \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
proof (cases "x \<in> \<X>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<in> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
 2. x \<notin> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x \<in> \<X>

goal (2 subgoals):
 1. x \<in> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
 2. x \<notin> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
from **(3)
[PROOF STATE]
proof (chain)
picking this:
[[r\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>
[PROOF STEP]
obtain I \<rho> where
          "([([r \<rightarrow> 0]u)]\<^sub>\<R>) = Regions.region \<X> I \<rho>" "Regions.valid_region \<X> k I \<rho>"
[PROOF STATE]
proof (prove)
using this:
[[r\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>

goal (1 subgoal):
 1. (\<And>I \<rho>. \<lbrakk>[[r\<rightarrow>0]u]\<^sub>\<R> = Regions.region \<X> I \<rho>; Regions.valid_region \<X> k I \<rho>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: \<R>_def)
[PROOF STATE]
proof (state)
this:
[[r\<rightarrow>0]u]\<^sub>\<R> = Regions.region \<X> I \<rho>
Regions.valid_region \<X> k I \<rho>

goal (2 subgoals):
 1. x \<in> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
 2. x \<notin> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
with ** \<open>x \<in> \<X>\<close>
[PROOF STATE]
proof (chain)
picking this:
[r'\<rightarrow>0]u \<in> [[r\<rightarrow>0]u]\<^sub>\<R>
[r\<rightarrow>0]u \<in> [[r\<rightarrow>0]u]\<^sub>\<R>
[[r\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>
x \<in> \<X>
[[r\<rightarrow>0]u]\<^sub>\<R> = Regions.region \<X> I \<rho>
Regions.valid_region \<X> k I \<rho>
[PROOF STEP]
have ***:
          "intv_elem x ([r' \<rightarrow> 0]u) (I x)" "intv_elem x ([r \<rightarrow> 0]u) (I x)"
[PROOF STATE]
proof (prove)
using this:
[r'\<rightarrow>0]u \<in> [[r\<rightarrow>0]u]\<^sub>\<R>
[r\<rightarrow>0]u \<in> [[r\<rightarrow>0]u]\<^sub>\<R>
[[r\<rightarrow>0]u]\<^sub>\<R> \<in> \<R>
x \<in> \<X>
[[r\<rightarrow>0]u]\<^sub>\<R> = Regions.region \<X> I \<rho>
Regions.valid_region \<X> k I \<rho>

goal (1 subgoal):
 1. Regions.intv_elem x ([r'\<rightarrow>0]u) (I x) &&& Regions.intv_elem x ([r\<rightarrow>0]u) (I x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Regions.intv_elem x ([r'\<rightarrow>0]u) (I x)
Regions.intv_elem x ([r\<rightarrow>0]u) (I x)

goal (2 subgoals):
 1. x \<in> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
 2. x \<notin> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
with reset
[PROOF STATE]
proof (chain)
picking this:
([r'\<rightarrow>0]u) x = 0
Regions.intv_elem x ([r'\<rightarrow>0]u) (I x)
Regions.intv_elem x ([r\<rightarrow>0]u) (I x)
[PROOF STEP]
have "I x = Const 0"
[PROOF STATE]
proof (prove)
using this:
([r'\<rightarrow>0]u) x = 0
Regions.intv_elem x ([r'\<rightarrow>0]u) (I x)
Regions.intv_elem x ([r\<rightarrow>0]u) (I x)

goal (1 subgoal):
 1. I x = Regions.intv.Const 0
[PROOF STEP]
by (cases "I x", auto)
[PROOF STATE]
proof (state)
this:
I x = Regions.intv.Const 0

goal (2 subgoals):
 1. x \<in> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
 2. x \<notin> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
with ***(2)
[PROOF STATE]
proof (chain)
picking this:
Regions.intv_elem x ([r\<rightarrow>0]u) (I x)
I x = Regions.intv.Const 0
[PROOF STEP]
have "([r \<rightarrow> 0]u) x = 0"
[PROOF STATE]
proof (prove)
using this:
Regions.intv_elem x ([r\<rightarrow>0]u) (I x)
I x = Regions.intv.Const 0

goal (1 subgoal):
 1. ([r\<rightarrow>0]u) x = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([r\<rightarrow>0]u) x = 0

goal (2 subgoals):
 1. x \<in> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
 2. x \<notin> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
with reset
[PROOF STATE]
proof (chain)
picking this:
([r'\<rightarrow>0]u) x = 0
([r\<rightarrow>0]u) x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
([r'\<rightarrow>0]u) x = 0
([r\<rightarrow>0]u) x = 0

goal (1 subgoal):
 1. ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x

goal (1 subgoal):
 1. x \<notin> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> \<X>

goal (1 subgoal):
 1. x \<notin> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
with assms(3-)
[PROOF STATE]
proof (chain)
picking this:
set r \<subseteq> \<X>
set r' \<subseteq> \<X>
x \<notin> \<X>
[PROOF STEP]
have "x \<notin> set r" "x \<notin> set r'"
[PROOF STATE]
proof (prove)
using this:
set r \<subseteq> \<X>
set r' \<subseteq> \<X>
x \<notin> \<X>

goal (1 subgoal):
 1. x \<notin> set r &&& x \<notin> set r'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> set r
x \<notin> set r'

goal (1 subgoal):
 1. x \<notin> \<X> \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> set r
x \<notin> set r'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<notin> set r
x \<notin> set r'

goal (1 subgoal):
 1. ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x

goal (1 subgoal):
 1. x \<notin> set r' \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> set r' \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<notin> set r'

goal (1 subgoal):
 1. x \<notin> set r' \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<notin> set r'
[PROOF STEP]
have reset: "([r' \<rightarrow> 0]u) x = u x"
[PROOF STATE]
proof (prove)
using this:
x \<notin> set r'

goal (1 subgoal):
 1. ([r'\<rightarrow>0]u) x = u x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
([r'\<rightarrow>0]u) x = u x

goal (1 subgoal):
 1. x \<notin> set r' \<Longrightarrow> ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
with id
[PROOF STATE]
proof (chain)
picking this:
([r\<rightarrow>0]u) x = u x
([r'\<rightarrow>0]u) x = u x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
([r\<rightarrow>0]u) x = u x
([r'\<rightarrow>0]u) x = u x

goal (1 subgoal):
 1. ([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
([r\<rightarrow>0]u) x = ([r'\<rightarrow>0]u) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
([r\<rightarrow>0]u) ?x3 = ([r'\<rightarrow>0]u) ?x3

goal (1 subgoal):
 1. \<lbrakk>u \<in> V; [[r\<rightarrow>0]u]\<^sub>\<R> = [[r'\<rightarrow>0]u]\<^sub>\<R>; set r \<subseteq> \<X>; set r' \<subseteq> \<X>\<rbrakk> \<Longrightarrow> [r\<rightarrow>0]u = [r'\<rightarrow>0]u
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
([r\<rightarrow>0]u) ?x3 = ([r'\<rightarrow>0]u) ?x3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
([r\<rightarrow>0]u) ?x3 = ([r'\<rightarrow>0]u) ?x3

goal (1 subgoal):
 1. [r\<rightarrow>0]u = [r'\<rightarrow>0]u
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
[r\<rightarrow>0]u = [r'\<rightarrow>0]u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma admissible_targets_clocks:
  assumes "(l, g, \<mu>) \<in> trans_of A" "(X, l') \<in> \<mu>"
  shows "X \<subseteq> \<X>" "set (SOME r. set r = X) \<subseteq> \<X>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<subseteq> \<X> &&& set (SOME r. set r = X) \<subseteq> \<X>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. X \<subseteq> \<X>
 2. set (SOME r. set r = X) \<subseteq> \<X>
[PROOF STEP]
from admissible_targets(2)[OF assms] finite
[PROOF STATE]
proof (chain)
picking this:
X \<subseteq> clocks A
finite \<X>
finite L
finite (PTA.trans_of A)
[PROOF STEP]
have
    "finite X" "X \<subseteq> \<X>"
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> clocks A
finite \<X>
finite L
finite (PTA.trans_of A)

goal (1 subgoal):
 1. finite X &&& X \<subseteq> \<X>
[PROOF STEP]
by (auto intro: finite_subset simp: \<X>_def)
[PROOF STATE]
proof (state)
this:
finite X
X \<subseteq> \<X>

goal (2 subgoals):
 1. X \<subseteq> \<X>
 2. set (SOME r. set r = X) \<subseteq> \<X>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite X
X \<subseteq> \<X>
[PROOF STEP]
obtain r where "set r = X"
[PROOF STATE]
proof (prove)
using this:
finite X
X \<subseteq> \<X>

goal (1 subgoal):
 1. (\<And>r. set r = X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_list
[PROOF STATE]
proof (prove)
using this:
finite X
X \<subseteq> \<X>
finite ?A \<Longrightarrow> \<exists>xs. set xs = ?A

goal (1 subgoal):
 1. (\<And>r. set r = X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set r = X

goal (2 subgoals):
 1. X \<subseteq> \<X>
 2. set (SOME r. set r = X) \<subseteq> \<X>
[PROOF STEP]
with \<open>X \<subseteq> \<X>\<close>
[PROOF STATE]
proof (chain)
picking this:
X \<subseteq> \<X>
set r = X
[PROOF STEP]
show "X \<subseteq> \<X>" "set (SOME r. set r = X) \<subseteq> \<X>"
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> \<X>
set r = X

goal (1 subgoal):
 1. X \<subseteq> \<X> &&& set (SOME r. set r = X) \<subseteq> \<X>
[PROOF STEP]
by (metis (mono_tags, lifting) someI_ex)+
[PROOF STATE]
proof (state)
this:
X \<subseteq> \<X>
set (SOME r. set r = X) \<subseteq> \<X>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma K_pmf_rel:
  defines "f \<equiv> \<lambda> (l, u). (l, [u]\<^sub>\<R>)"
  shows "rel_pmf (\<lambda> (l, u) st. (l, [u]\<^sub>\<R>) = st) \<mu> (map_pmf f \<mu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pmf (\<lambda>(l, u). (=) (l, [u]\<^sub>\<R>)) \<mu> (map_pmf f \<mu>)
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pmf (\<lambda>(l, u). (=) (l, [u]\<^sub>\<R>)) \<mu> (map_pmf (\<lambda>(l, u). (l, [u]\<^sub>\<R>)) \<mu>)
[PROOF STEP]
by (subst pmf.rel_map(2)) (rule rel_pmf_reflI, auto)


[STATEMENT]
lemma \<K>_pmf_rel:
  assumes A: "\<mu> \<in> \<K> (l, R)"
  defines "f \<equiv> \<lambda> (l, u). (l, SOME u. u \<in> R)"
  shows "rel_pmf (\<lambda> (l, u) st. (l, SOME u. u \<in> R) = st) \<mu> (map_pmf f \<mu>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pmf (\<lambda>(l, u). (=) (l, SOME u. u \<in> R)) \<mu> (map_pmf f \<mu>)
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_pmf (\<lambda>(l, u). (=) (l, SOME u. u \<in> R)) \<mu> (map_pmf (\<lambda>(l, u). (l, SOME u. u \<in> R)) \<mu>)
[PROOF STEP]
by (subst pmf.rel_map(2)) (rule rel_pmf_reflI, auto)