[STATEMENT]
lemma K_elem_abs_inj:
  assumes A: "\<mu> \<in> K (l, u)"
  defines "f \<equiv> \<lambda> (l, u). (l, [u]\<^sub>\<R>)"
  shows "inj_on f \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f (set_pmf \<mu>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj_on f (set_pmf \<mu>)
[PROOF STEP]
have "(l1, u1) = (l2, u2)"
    if id: "(l1, [u1]\<^sub>\<R>) = (l2, [u2]\<^sub>\<R>)" and elem: "(l1, u1) \<in> \<mu>" "(l2, u2) \<in> \<mu>" for l1 l2 u1 u2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l1, u1) = (l2, u2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (l1, u1) = (l2, u2)
[PROOF STEP]
from id
[PROOF STATE]
proof (chain)
picking this:
(l1, [u1]\<^sub>\<R>) = (l2, [u2]\<^sub>\<R>)
[PROOF STEP]
have [simp]: "l2 = l1"
[PROOF STATE]
proof (prove)
using this:
(l1, [u1]\<^sub>\<R>) = (l2, [u2]\<^sub>\<R>)

goal (1 subgoal):
 1. l2 = l1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l2 = l1

goal (1 subgoal):
 1. (l1, u1) = (l2, u2)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
\<mu> \<in> K (l, u)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> K (l, u)

goal (1 subgoal):
 1. (l1, u1) = (l2, u2)
[PROOF STEP]
proof (cases, safe, goal_cases)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>la ua t. \<lbrakk>(l, u) \<in> S; 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l; return_pmf (l, u \<oplus> t) \<in> K (l, u); \<mu> = return_pmf (l, u \<oplus> t)\<rbrakk> \<Longrightarrow> l1 = l2
 2. \<And>la ua t. \<lbrakk>(l, u) \<in> S; 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l; return_pmf (l, u \<oplus> t) \<in> K (l, u); \<mu> = return_pmf (l, u \<oplus> t)\<rbrakk> \<Longrightarrow> u1 = u2
 3. \<And>la ua g \<mu>'. \<lbrakk>(l, u) \<in> S; (l, g, \<mu>') \<in> PTA.trans_of A; u \<turnstile> g; map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K (l, u); \<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'\<rbrakk> \<Longrightarrow> l1 = l2
 4. \<And>la ua g \<mu>'. \<lbrakk>(l, u) \<in> S; (l, g, \<mu>') \<in> PTA.trans_of A; u \<turnstile> g; map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K (l, u); \<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'\<rbrakk> \<Longrightarrow> u1 = u2
 5. \<lbrakk>return_pmf (l, u) \<in> K (l, u); \<mu> = return_pmf (l, u)\<rbrakk> \<Longrightarrow> l1 = l2
 6. \<lbrakk>return_pmf (l, u) \<in> K (l, u); \<mu> = return_pmf (l, u)\<rbrakk> \<Longrightarrow> u1 = u2
[PROOF STEP]
case (4 _ _ \<tau> \<mu>')
[PROOF STATE]
proof (state)
this:
(l, u) \<in> S
(l, \<tau>, \<mu>') \<in> PTA.trans_of A
u \<turnstile> \<tau>
map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K (l, u)
\<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'

goal (6 subgoals):
 1. \<And>la ua t. \<lbrakk>(l, u) \<in> S; 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l; return_pmf (l, u \<oplus> t) \<in> K (l, u); \<mu> = return_pmf (l, u \<oplus> t)\<rbrakk> \<Longrightarrow> l1 = l2
 2. \<And>la ua t. \<lbrakk>(l, u) \<in> S; 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l; return_pmf (l, u \<oplus> t) \<in> K (l, u); \<mu> = return_pmf (l, u \<oplus> t)\<rbrakk> \<Longrightarrow> u1 = u2
 3. \<And>la ua g \<mu>'. \<lbrakk>(l, u) \<in> S; (l, g, \<mu>') \<in> PTA.trans_of A; u \<turnstile> g; map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K (l, u); \<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'\<rbrakk> \<Longrightarrow> l1 = l2
 4. \<And>la ua g \<mu>'. \<lbrakk>(l, u) \<in> S; (l, g, \<mu>') \<in> PTA.trans_of A; u \<turnstile> g; map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K (l, u); \<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'\<rbrakk> \<Longrightarrow> u1 = u2
 5. \<lbrakk>return_pmf (l, u) \<in> K (l, u); \<mu> = return_pmf (l, u)\<rbrakk> \<Longrightarrow> l1 = l2
 6. \<lbrakk>return_pmf (l, u) \<in> K (l, u); \<mu> = return_pmf (l, u)\<rbrakk> \<Longrightarrow> u1 = u2
[PROOF STEP]
from \<open>\<mu> = _\<close> elem
[PROOF STATE]
proof (chain)
picking this:
\<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'
(l1, u1) \<in> set_pmf \<mu>
(l2, u2) \<in> set_pmf \<mu>
[PROOF STEP]
obtain X1 X2 where
        "u1 = [(SOME r. set r = X1)\<rightarrow>0]u" "(X1, l1) \<in> \<mu>'"
        "u2 = [(SOME r. set r = X2)\<rightarrow>0]u" "(X2, l1) \<in> \<mu>'"
[PROOF STATE]
proof (prove)
using this:
\<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'
(l1, u1) \<in> set_pmf \<mu>
(l2, u2) \<in> set_pmf \<mu>

goal (1 subgoal):
 1. (\<And>X1 X2. \<lbrakk>u1 = [(SOME r. set r = X1)\<rightarrow>0]u; (X1, l1) \<in> set_pmf \<mu>'; u2 = [(SOME r. set r = X2)\<rightarrow>0]u; (X2, l1) \<in> set_pmf \<mu>'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u1 = [(SOME r. set r = X1)\<rightarrow>0]u
(X1, l1) \<in> set_pmf \<mu>'
u2 = [(SOME r. set r = X2)\<rightarrow>0]u
(X2, l1) \<in> set_pmf \<mu>'

goal (6 subgoals):
 1. \<And>la ua t. \<lbrakk>(l, u) \<in> S; 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l; return_pmf (l, u \<oplus> t) \<in> K (l, u); \<mu> = return_pmf (l, u \<oplus> t)\<rbrakk> \<Longrightarrow> l1 = l2
 2. \<And>la ua t. \<lbrakk>(l, u) \<in> S; 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l; return_pmf (l, u \<oplus> t) \<in> K (l, u); \<mu> = return_pmf (l, u \<oplus> t)\<rbrakk> \<Longrightarrow> u1 = u2
 3. \<And>la ua g \<mu>'. \<lbrakk>(l, u) \<in> S; (l, g, \<mu>') \<in> PTA.trans_of A; u \<turnstile> g; map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K (l, u); \<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'\<rbrakk> \<Longrightarrow> l1 = l2
 4. \<And>la ua g \<mu>'. \<lbrakk>(l, u) \<in> S; (l, g, \<mu>') \<in> PTA.trans_of A; u \<turnstile> g; map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K (l, u); \<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'\<rbrakk> \<Longrightarrow> u1 = u2
 5. \<lbrakk>return_pmf (l, u) \<in> K (l, u); \<mu> = return_pmf (l, u)\<rbrakk> \<Longrightarrow> l1 = l2
 6. \<lbrakk>return_pmf (l, u) \<in> K (l, u); \<mu> = return_pmf (l, u)\<rbrakk> \<Longrightarrow> u1 = u2
[PROOF STEP]
with \<open>_ \<in> trans_of _\<close> admissible_targets_clocks
[PROOF STATE]
proof (chain)
picking this:
(l, \<tau>, \<mu>') \<in> PTA.trans_of A
\<lbrakk>(?l, ?g, ?\<mu>) \<in> PTA.trans_of A; (?X, ?l') \<in> set_pmf ?\<mu>\<rbrakk> \<Longrightarrow> ?X \<subseteq> \<X>
\<lbrakk>(?l, ?g, ?\<mu>) \<in> PTA.trans_of A; (?X, ?l') \<in> set_pmf ?\<mu>\<rbrakk> \<Longrightarrow> set (SOME r. set r = ?X) \<subseteq> \<X>
u1 = [(SOME r. set r = X1)\<rightarrow>0]u
(X1, l1) \<in> set_pmf \<mu>'
u2 = [(SOME r. set r = X2)\<rightarrow>0]u
(X2, l1) \<in> set_pmf \<mu>'
[PROOF STEP]
have
        "set (SOME r. set r = X1) \<subseteq> \<X>" "set (SOME r. set r = X2) \<subseteq> \<X>"
[PROOF STATE]
proof (prove)
using this:
(l, \<tau>, \<mu>') \<in> PTA.trans_of A
\<lbrakk>(?l, ?g, ?\<mu>) \<in> PTA.trans_of A; (?X, ?l') \<in> set_pmf ?\<mu>\<rbrakk> \<Longrightarrow> ?X \<subseteq> \<X>
\<lbrakk>(?l, ?g, ?\<mu>) \<in> PTA.trans_of A; (?X, ?l') \<in> set_pmf ?\<mu>\<rbrakk> \<Longrightarrow> set (SOME r. set r = ?X) \<subseteq> \<X>
u1 = [(SOME r. set r = X1)\<rightarrow>0]u
(X1, l1) \<in> set_pmf \<mu>'
u2 = [(SOME r. set r = X2)\<rightarrow>0]u
(X2, l1) \<in> set_pmf \<mu>'

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

goal (6 subgoals):
 1. \<And>la ua t. \<lbrakk>(l, u) \<in> S; 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l; return_pmf (l, u \<oplus> t) \<in> K (l, u); \<mu> = return_pmf (l, u \<oplus> t)\<rbrakk> \<Longrightarrow> l1 = l2
 2. \<And>la ua t. \<lbrakk>(l, u) \<in> S; 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l; return_pmf (l, u \<oplus> t) \<in> K (l, u); \<mu> = return_pmf (l, u \<oplus> t)\<rbrakk> \<Longrightarrow> u1 = u2
 3. \<And>la ua g \<mu>'. \<lbrakk>(l, u) \<in> S; (l, g, \<mu>') \<in> PTA.trans_of A; u \<turnstile> g; map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K (l, u); \<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'\<rbrakk> \<Longrightarrow> l1 = l2
 4. \<And>la ua g \<mu>'. \<lbrakk>(l, u) \<in> S; (l, g, \<mu>') \<in> PTA.trans_of A; u \<turnstile> g; map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K (l, u); \<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'\<rbrakk> \<Longrightarrow> u1 = u2
 5. \<lbrakk>return_pmf (l, u) \<in> K (l, u); \<mu> = return_pmf (l, u)\<rbrakk> \<Longrightarrow> l1 = l2
 6. \<lbrakk>return_pmf (l, u) \<in> K (l, u); \<mu> = return_pmf (l, u)\<rbrakk> \<Longrightarrow> u1 = u2
[PROOF STEP]
with id \<open>u1 = _\<close> \<open>u2 = _\<close> reset_eq[of u] \<open>_ \<in> S\<close>
[PROOF STATE]
proof (chain)
picking this:
(l1, [u1]\<^sub>\<R>) = (l2, [u2]\<^sub>\<R>)
u1 = [(SOME r. set r = X1)\<rightarrow>0]u
u2 = [(SOME r. set r = X2)\<rightarrow>0]u
\<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
(l, u) \<in> S
set (SOME r. set r = X1) \<subseteq> \<X>
set (SOME r. set r = X2) \<subseteq> \<X>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(l1, [u1]\<^sub>\<R>) = (l2, [u2]\<^sub>\<R>)
u1 = [(SOME r. set r = X1)\<rightarrow>0]u
u2 = [(SOME r. set r = X2)\<rightarrow>0]u
\<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
(l, u) \<in> S
set (SOME r. set r = X1) \<subseteq> \<X>
set (SOME r. set r = X2) \<subseteq> \<X>

goal (1 subgoal):
 1. u1 = u2
[PROOF STEP]
by (auto simp: S_def V_def)
[PROOF STATE]
proof (state)
this:
u1 = u2

goal (5 subgoals):
 1. \<And>la ua t. \<lbrakk>(l, u) \<in> S; 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l; return_pmf (l, u \<oplus> t) \<in> K (l, u); \<mu> = return_pmf (l, u \<oplus> t)\<rbrakk> \<Longrightarrow> l1 = l2
 2. \<And>la ua t. \<lbrakk>(l, u) \<in> S; 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l; return_pmf (l, u \<oplus> t) \<in> K (l, u); \<mu> = return_pmf (l, u \<oplus> t)\<rbrakk> \<Longrightarrow> u1 = u2
 3. \<And>la ua g \<mu>'. \<lbrakk>(l, u) \<in> S; (l, g, \<mu>') \<in> PTA.trans_of A; u \<turnstile> g; map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>' \<in> K (l, u); \<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'\<rbrakk> \<Longrightarrow> l1 = l2
 4. \<lbrakk>return_pmf (l, u) \<in> K (l, u); \<mu> = return_pmf (l, u)\<rbrakk> \<Longrightarrow> l1 = l2
 5. \<lbrakk>return_pmf (l, u) \<in> K (l, u); \<mu> = return_pmf (l, u)\<rbrakk> \<Longrightarrow> u1 = u2
[PROOF STEP]
qed (-, insert elem, simp)+
[PROOF STATE]
proof (state)
this:
(l1, u1) = (l2, u2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?l1.3, [?u1.3]\<^sub>\<R>) = (?l2.3, [?u2.3]\<^sub>\<R>); (?l1.3, ?u1.3) \<in> set_pmf \<mu>; (?l2.3, ?u2.3) \<in> set_pmf \<mu>\<rbrakk> \<Longrightarrow> (?l1.3, ?u1.3) = (?l2.3, ?u2.3)

goal (1 subgoal):
 1. inj_on f (set_pmf \<mu>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?l1.3, [?u1.3]\<^sub>\<R>) = (?l2.3, [?u2.3]\<^sub>\<R>); (?l1.3, ?u1.3) \<in> set_pmf \<mu>; (?l2.3, ?u2.3) \<in> set_pmf \<mu>\<rbrakk> \<Longrightarrow> (?l1.3, ?u1.3) = (?l2.3, ?u2.3)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?l1.3, [?u1.3]\<^sub>\<R>) = (?l2.3, [?u2.3]\<^sub>\<R>); (?l1.3, ?u1.3) \<in> set_pmf \<mu>; (?l2.3, ?u2.3) \<in> set_pmf \<mu>\<rbrakk> \<Longrightarrow> (?l1.3, ?u1.3) = (?l2.3, ?u2.3)

goal (1 subgoal):
 1. inj_on f (set_pmf \<mu>)
[PROOF STEP]
unfolding f_def inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?l1.3, [?u1.3]\<^sub>\<R>) = (?l2.3, [?u2.3]\<^sub>\<R>); (?l1.3, ?u1.3) \<in> set_pmf \<mu>; (?l2.3, ?u2.3) \<in> set_pmf \<mu>\<rbrakk> \<Longrightarrow> (?l1.3, ?u1.3) = (?l2.3, ?u2.3)

goal (1 subgoal):
 1. \<forall>x\<in>set_pmf \<mu>. \<forall>y\<in>set_pmf \<mu>. (case x of (l, u) \<Rightarrow> (l, [u]\<^sub>\<R>)) = (case y of (l, u) \<Rightarrow> (l, [u]\<^sub>\<R>)) \<longrightarrow> x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj_on f (set_pmf \<mu>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma K_elem_repr_inj:
  notes alpha_interp.valid_regions_distinct_spec[intro] (* XXX Declare somewhere else *)
  assumes A: "\<mu> \<in> \<K> (l, R)"
  defines "f \<equiv> \<lambda> (l, R). (l, SOME u. u \<in> R)"
  shows "inj_on f \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f (set_pmf \<mu>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj_on f (set_pmf \<mu>)
[PROOF STEP]
have "(l1, R1) = (l2, R2)"
    if id: "(l1, SOME u. u \<in> R1) = (l2, SOME u. u \<in> R2)" and elem: "(l1, R1) \<in> \<mu>" "(l2, R2) \<in> \<mu>"
    for l1 l2 R1 R2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l1, R1) = (l2, R2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (l1, R1) = (l2, R2)
[PROOF STEP]
let ?r1 = "SOME u. u \<in> R1" and ?r2 = "SOME u. u \<in> R2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (l1, R1) = (l2, R2)
[PROOF STEP]
from id
[PROOF STATE]
proof (chain)
picking this:
(l1, SOME u. u \<in> R1) = (l2, SOME u. u \<in> R2)
[PROOF STEP]
have [simp]: "l2 = l1" "?r2 = ?r1"
[PROOF STATE]
proof (prove)
using this:
(l1, SOME u. u \<in> R1) = (l2, SOME u. u \<in> R2)

goal (1 subgoal):
 1. l2 = l1 &&& (SOME u. u \<in> R2) = (SOME u. u \<in> R1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l2 = l1
(SOME u. u \<in> R2) = (SOME u. u \<in> R1)

goal (1 subgoal):
 1. (l1, R1) = (l2, R2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
l2 = l1
(SOME u. u \<in> R2) = (SOME u. u \<in> R1)

goal (1 subgoal):
 1. (l1, R1) = (l2, R2)
[PROOF STEP]
fix g \<mu>' x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (l1, R1) = (l2, R2)
[PROOF STEP]
assume "(l, R) \<in> \<S>" "(l, g, \<mu>') \<in> PTA.trans_of A" "R \<subseteq> {v. v \<turnstile> g}"
         and "\<mu> = map_pmf (\<lambda>(X, l). (l, region_set' R (SOME r. set r = X) 0)) \<mu>'"
[PROOF STATE]
proof (state)
this:
(l, R) \<in> \<S>
(l, g, \<mu>') \<in> PTA.trans_of A
R \<subseteq> {v. v \<turnstile> g}
\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'

goal (1 subgoal):
 1. (l1, R1) = (l2, R2)
[PROOF STEP]
from \<open>\<mu> = _\<close> elem
[PROOF STATE]
proof (chain)
picking this:
\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'
(l1, R1) \<in> set_pmf \<mu>
(l2, R2) \<in> set_pmf \<mu>
[PROOF STEP]
obtain X1 X2 where
        "R1 = region_set' R (SOME r. set r = X1) 0" "(X1, l1) \<in> \<mu>'"
        "R2 = region_set' R (SOME r. set r = X2) 0" "(X2, l1) \<in> \<mu>'"
[PROOF STATE]
proof (prove)
using this:
\<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) \<mu>'
(l1, R1) \<in> set_pmf \<mu>
(l2, R2) \<in> set_pmf \<mu>

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

goal (1 subgoal):
 1. (l1, R1) = (l2, R2)
[PROOF STEP]
with \<open>_ \<in> trans_of _\<close> admissible_targets_clocks
[PROOF STATE]
proof (chain)
picking this:
(l, g, \<mu>') \<in> PTA.trans_of A
\<lbrakk>(?l, ?g, ?\<mu>) \<in> PTA.trans_of A; (?X, ?l') \<in> set_pmf ?\<mu>\<rbrakk> \<Longrightarrow> ?X \<subseteq> \<X>
\<lbrakk>(?l, ?g, ?\<mu>) \<in> PTA.trans_of A; (?X, ?l') \<in> set_pmf ?\<mu>\<rbrakk> \<Longrightarrow> set (SOME r. set r = ?X) \<subseteq> \<X>
R1 = [X1::=0]R
(X1, l1) \<in> set_pmf \<mu>'
R2 = [X2::=0]R
(X2, l1) \<in> set_pmf \<mu>'
[PROOF STEP]
have
        "set (SOME r. set r = X1) \<subseteq> \<X>" "set (SOME r. set r = X2) \<subseteq> \<X>"
[PROOF STATE]
proof (prove)
using this:
(l, g, \<mu>') \<in> PTA.trans_of A
\<lbrakk>(?l, ?g, ?\<mu>) \<in> PTA.trans_of A; (?X, ?l') \<in> set_pmf ?\<mu>\<rbrakk> \<Longrightarrow> ?X \<subseteq> \<X>
\<lbrakk>(?l, ?g, ?\<mu>) \<in> PTA.trans_of A; (?X, ?l') \<in> set_pmf ?\<mu>\<rbrakk> \<Longrightarrow> set (SOME r. set r = ?X) \<subseteq> \<X>
R1 = [X1::=0]R
(X1, l1) \<in> set_pmf \<mu>'
R2 = [X2::=0]R
(X2, l1) \<in> set_pmf \<mu>'

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

goal (1 subgoal):
 1. (l1, R1) = (l2, R2)
[PROOF STEP]
with alpha_interp.region_set'_closed[of _ 0] \<open>R1 = _\<close> \<open>R2 = _\<close> \<open>_ \<in> \<S>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?R \<in> \<R>; 0 \<le> 0; \<forall>x\<in>set ?r. 0 \<le> k x; set ?r \<subseteq> \<X>\<rbrakk> \<Longrightarrow> region_set' ?R ?r (real 0) \<in> \<R>
R1 = [X1::=0]R
R2 = [X2::=0]R
(l, R) \<in> \<S>
set (SOME r. set r = X1) \<subseteq> \<X>
set (SOME r. set r = X2) \<subseteq> \<X>
[PROOF STEP]
have
        "R1 \<in> \<R>" "R2 \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?R \<in> \<R>; 0 \<le> 0; \<forall>x\<in>set ?r. 0 \<le> k x; set ?r \<subseteq> \<X>\<rbrakk> \<Longrightarrow> region_set' ?R ?r (real 0) \<in> \<R>
R1 = [X1::=0]R
R2 = [X2::=0]R
(l, R) \<in> \<S>
set (SOME r. set r = X1) \<subseteq> \<X>
set (SOME r. set r = X2) \<subseteq> \<X>

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

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

goal (1 subgoal):
 1. (l1, R1) = (l2, R2)
[PROOF STEP]
with region_not_empty[OF finite(1)]
[PROOF STATE]
proof (chain)
picking this:
Regions.valid_region \<X> ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region \<X> ?I ?r
R1 \<in> \<R>
R2 \<in> \<R>
[PROOF STEP]
have
        "R1 \<noteq> {}" "R2 \<noteq> {}" "\<exists>u. u \<in> R1" "\<exists>u. u \<in> R2"
[PROOF STATE]
proof (prove)
using this:
Regions.valid_region \<X> ?k ?I ?r \<Longrightarrow> \<exists>u. u \<in> Regions.region \<X> ?I ?r
R1 \<in> \<R>
R2 \<in> \<R>

goal (1 subgoal):
 1. (R1 \<noteq> {} &&& R2 \<noteq> {}) &&& \<exists>u. u \<in> R1 &&& \<exists>u. u \<in> R2
[PROOF STEP]
by (auto simp: \<R>_def)
[PROOF STATE]
proof (state)
this:
R1 \<noteq> {}
R2 \<noteq> {}
\<exists>u. u \<in> R1
\<exists>u. u \<in> R2

goal (1 subgoal):
 1. (l1, R1) = (l2, R2)
[PROOF STEP]
from someI_ex[OF this(3)] someI_ex[OF this(4)]
[PROOF STATE]
proof (chain)
picking this:
(SOME x. x \<in> R1) \<in> R1
(SOME x. x \<in> R2) \<in> R2
[PROOF STEP]
have "?r1 \<in> R1" "?r1 \<in> R2"
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> R1) \<in> R1
(SOME x. x \<in> R2) \<in> R2

goal (1 subgoal):
 1. (SOME u. u \<in> R1) \<in> R1 &&& (SOME u. u \<in> R1) \<in> R2
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
(SOME u. u \<in> R1) \<in> R1
(SOME u. u \<in> R1) \<in> R2

goal (1 subgoal):
 1. (l1, R1) = (l2, R2)
[PROOF STEP]
with \<open>R1 \<in> \<R>\<close> \<open>R2 \<in> \<R>\<close>
[PROOF STATE]
proof (chain)
picking this:
R1 \<in> \<R>
R2 \<in> \<R>
(SOME u. u \<in> R1) \<in> R1
(SOME u. u \<in> R1) \<in> R2
[PROOF STEP]
have "R1 = R2"
[PROOF STATE]
proof (prove)
using this:
R1 \<in> \<R>
R2 \<in> \<R>
(SOME u. u \<in> R1) \<in> R1
(SOME u. u \<in> R1) \<in> R2

goal (1 subgoal):
 1. R1 = R2
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
R1 = R2

goal (1 subgoal):
 1. (l1, R1) = (l2, R2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>(l, R) \<in> \<S>; (l, ?g5, ?\<mu>'5) \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> ?g5}; \<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) ?\<mu>'5\<rbrakk> \<Longrightarrow> R1 = R2

goal (1 subgoal):
 1. (l1, R1) = (l2, R2)
[PROOF STEP]
from A elem this
[PROOF STATE]
proof (chain)
picking this:
\<mu> \<in> \<K> (l, R)
(l1, R1) \<in> set_pmf \<mu>
(l2, R2) \<in> set_pmf \<mu>
\<lbrakk>(l, R) \<in> \<S>; (l, ?g5, ?\<mu>'5) \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> ?g5}; \<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) ?\<mu>'5\<rbrakk> \<Longrightarrow> R1 = R2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> \<K> (l, R)
(l1, R1) \<in> set_pmf \<mu>
(l2, R2) \<in> set_pmf \<mu>
\<lbrakk>(l, R) \<in> \<S>; (l, ?g5, ?\<mu>'5) \<in> PTA.trans_of A; R \<subseteq> {v. v \<turnstile> ?g5}; \<mu> = map_pmf (\<lambda>(X, l). (l, [X::=0]R)) ?\<mu>'5\<rbrakk> \<Longrightarrow> R1 = R2

goal (1 subgoal):
 1. (l1, R1) = (l2, R2)
[PROOF STEP]
by (cases, auto)
[PROOF STATE]
proof (state)
this:
(l1, R1) = (l2, R2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?l1.3, SOME u. u \<in> ?R1.3) = (?l2.3, SOME u. u \<in> ?R2.3); (?l1.3, ?R1.3) \<in> set_pmf \<mu>; (?l2.3, ?R2.3) \<in> set_pmf \<mu>\<rbrakk> \<Longrightarrow> (?l1.3, ?R1.3) = (?l2.3, ?R2.3)

goal (1 subgoal):
 1. inj_on f (set_pmf \<mu>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>(?l1.3, SOME u. u \<in> ?R1.3) = (?l2.3, SOME u. u \<in> ?R2.3); (?l1.3, ?R1.3) \<in> set_pmf \<mu>; (?l2.3, ?R2.3) \<in> set_pmf \<mu>\<rbrakk> \<Longrightarrow> (?l1.3, ?R1.3) = (?l2.3, ?R2.3)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?l1.3, SOME u. u \<in> ?R1.3) = (?l2.3, SOME u. u \<in> ?R2.3); (?l1.3, ?R1.3) \<in> set_pmf \<mu>; (?l2.3, ?R2.3) \<in> set_pmf \<mu>\<rbrakk> \<Longrightarrow> (?l1.3, ?R1.3) = (?l2.3, ?R2.3)

goal (1 subgoal):
 1. inj_on f (set_pmf \<mu>)
[PROOF STEP]
unfolding f_def inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?l1.3, SOME u. u \<in> ?R1.3) = (?l2.3, SOME u. u \<in> ?R2.3); (?l1.3, ?R1.3) \<in> set_pmf \<mu>; (?l2.3, ?R2.3) \<in> set_pmf \<mu>\<rbrakk> \<Longrightarrow> (?l1.3, ?R1.3) = (?l2.3, ?R2.3)

goal (1 subgoal):
 1. \<forall>x\<in>set_pmf \<mu>. \<forall>y\<in>set_pmf \<mu>. (case x of (l, R) \<Rightarrow> (l, SOME u. u \<in> R)) = (case y of (l, R) \<Rightarrow> (l, SOME u. u \<in> R)) \<longrightarrow> x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inj_on f (set_pmf \<mu>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma K_elem_pmf_map_abs:
  assumes A: "\<mu> \<in> K (l, u)" "(l', u') \<in> \<mu>"
  defines "f \<equiv> \<lambda> (l, u). (l, [u]\<^sub>\<R>)"
  shows "pmf (map_pmf f \<mu>) (f (l', u')) = pmf \<mu> (l', u')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (map_pmf f \<mu>) (f (l', u')) = pmf \<mu> (l', u')
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> K (l, u)
(l', u') \<in> set_pmf \<mu>

goal (1 subgoal):
 1. pmf (map_pmf f \<mu>) (f (l', u')) = pmf \<mu> (l', u')
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> K (l, u)
(l', u') \<in> set_pmf \<mu>

goal (1 subgoal):
 1. pmf (map_pmf (\<lambda>(l, u). (l, [u]\<^sub>\<R>)) \<mu>) (case (l', u') of (l, u) \<Rightarrow> (l, [u]\<^sub>\<R>)) = pmf \<mu> (l', u')
[PROOF STEP]
by (blast intro: pmf_map_inj K_elem_abs_inj)


[STATEMENT]
lemma K_elem_pmf_map_repr:
  assumes A: "\<mu> \<in> \<K> (l, R)" "(l', R') \<in> \<mu>"
  defines "f \<equiv> \<lambda> (l, R). (l, SOME u. u \<in> R)"
  shows "pmf (map_pmf f \<mu>) (f (l', R')) = pmf \<mu> (l', R')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (map_pmf f \<mu>) (f (l', R')) = pmf \<mu> (l', R')
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> \<K> (l, R)
(l', R') \<in> set_pmf \<mu>

goal (1 subgoal):
 1. pmf (map_pmf f \<mu>) (f (l', R')) = pmf \<mu> (l', R')
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> \<K> (l, R)
(l', R') \<in> set_pmf \<mu>

goal (1 subgoal):
 1. pmf (map_pmf (\<lambda>(l, R). (l, SOME u. u \<in> R)) \<mu>) (case (l', R') of (l, R) \<Rightarrow> (l, SOME u. u \<in> R)) = pmf \<mu> (l', R')
[PROOF STEP]
by (blast intro: pmf_map_inj K_elem_repr_inj)


[STATEMENT]
lemma \<S>_reps_S[intro]:
  assumes "s \<in> \<S>"
  shows "reps s \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reps s \<in> S
[PROOF STEP]
using assms \<R>_V
[PROOF STATE]
proof (prove)
using this:
s \<in> \<S>
\<Union> \<R> = V

goal (1 subgoal):
 1. reps s \<in> S
[PROOF STEP]
unfolding S_def \<S>_def reps_def V_def
[PROOF STATE]
proof (prove)
using this:
s \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}}
\<Union> \<R> = {v. \<forall>x\<in>\<X>. 0 \<le> v x}

goal (1 subgoal):
 1. (case s of (l, R) \<Rightarrow> if R \<in> \<R> then (l, SOME u. u \<in> R) else (l, \<lambda>_. - 1)) \<in> {(l, u). l \<in> L \<and> (\<forall>x\<in>\<X>. 0 \<le> u x) \<and> u \<turnstile> PTA.inv_of A l}
[PROOF STEP]
by force


[STATEMENT]
lemma S_abss_\<S>[intro]:
  assumes "s \<in> S"
  shows "abss s \<in> \<S>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abss s \<in> \<S>
[PROOF STEP]
using assms ccompatible_inv
[PROOF STATE]
proof (prove)
using this:
s \<in> S
ccompatible \<R> (PTA.inv_of A ?l)

goal (1 subgoal):
 1. abss s \<in> \<S>
[PROOF STEP]
unfolding \<S>_def S_alt_def abss_def ccompatible_def
[PROOF STATE]
proof (prove)
using this:
s \<in> {(l, u). l \<in> L \<and> u \<in> V \<and> u \<turnstile> PTA.inv_of A l}
\<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 = {}

goal (1 subgoal):
 1. (case s of (l, u) \<Rightarrow> if u \<in> V then (l, [u]\<^sub>\<R>) else (l, - V)) \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}}
[PROOF STEP]
by force


[STATEMENT]
lemma \<S>_abss_reps[simp]:
  "s \<in> \<S> \<Longrightarrow> abss (reps s) = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> \<S> \<Longrightarrow> abss (reps s) = s
[PROOF STEP]
using \<R>_V alpha_interp.region_unique_spec
[PROOF STATE]
proof (prove)
using this:
\<Union> \<R> = V
\<lbrakk>?u \<in> ?R; ?R \<in> \<R>\<rbrakk> \<Longrightarrow> [?u]\<^sub>\<R> = ?R

goal (1 subgoal):
 1. s \<in> \<S> \<Longrightarrow> abss (reps s) = s
[PROOF STEP]
by (auto simp: S_def \<S>_def reps_def abss_def; blast)


[STATEMENT]
lemma map_pmf_abs_reps:
  assumes "s \<in> \<S>" "\<mu> \<in> \<K> s"
  shows "map_pmf abss (map_pmf reps \<mu>) = \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf abss (map_pmf reps \<mu>) = \<mu>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_pmf abss (map_pmf reps \<mu>) = \<mu>
[PROOF STEP]
have "map_pmf abss (map_pmf reps \<mu>) = map_pmf (abss o reps) \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf abss (map_pmf reps \<mu>) = map_pmf (abss \<circ> reps) \<mu>
[PROOF STEP]
by (simp add: pmf.map_comp)
[PROOF STATE]
proof (state)
this:
map_pmf abss (map_pmf reps \<mu>) = map_pmf (abss \<circ> reps) \<mu>

goal (1 subgoal):
 1. map_pmf abss (map_pmf reps \<mu>) = \<mu>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_pmf abss (map_pmf reps \<mu>) = map_pmf (abss \<circ> reps) \<mu>

goal (1 subgoal):
 1. map_pmf abss (map_pmf reps \<mu>) = \<mu>
[PROOF STEP]
have "\<dots> = \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf (abss \<circ> reps) \<mu> = \<mu>
[PROOF STEP]
proof (rule map_pmf_idI, safe, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set_pmf \<mu> \<Longrightarrow> (abss \<circ> reps) (a, b) = (a, b)
[PROOF STEP]
case prems: (1 l' R')
[PROOF STATE]
proof (state)
this:
(l', R') \<in> set_pmf \<mu>

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set_pmf \<mu> \<Longrightarrow> (abss \<circ> reps) (a, b) = (a, b)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
s \<in> \<S>
\<mu> \<in> \<K> s
(l', R') \<in> set_pmf \<mu>
[PROOF STEP]
have "(l', R') \<in> \<S>" "reps (l', R') \<in> S"
[PROOF STATE]
proof (prove)
using this:
s \<in> \<S>
\<mu> \<in> \<K> s
(l', R') \<in> set_pmf \<mu>

goal (1 subgoal):
 1. (l', R') \<in> \<S> &&& reps (l', R') \<in> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(l', R') \<in> \<S>
reps (l', R') \<in> S

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> set_pmf \<mu> \<Longrightarrow> (abss \<circ> reps) (a, b) = (a, b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(l', R') \<in> \<S>
reps (l', R') \<in> S
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(l', R') \<in> \<S>
reps (l', R') \<in> S

goal (1 subgoal):
 1. (abss \<circ> reps) (l', R') = (l', R')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(abss \<circ> reps) (l', R') = (l', R')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map_pmf (abss \<circ> reps) \<mu> = \<mu>

goal (1 subgoal):
 1. map_pmf abss (map_pmf reps \<mu>) = \<mu>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
map_pmf abss (map_pmf reps \<mu>) = \<mu>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
map_pmf abss (map_pmf reps \<mu>) = \<mu>

goal (1 subgoal):
 1. map_pmf abss (map_pmf reps \<mu>) = \<mu>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map_pmf abss (map_pmf reps \<mu>) = \<mu>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abss_reps_id:
  notes R_G.cfg_onD_state[simp del]
  assumes "s' \<in> \<S>" "s \<in> set_pmf (action cfg)" "cfg \<in> R_G.cfg_on s'"
  shows "abss (reps s) = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abss (reps s) = s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. abss (reps s) = s
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
s' \<in> \<S>
s \<in> set_pmf (action cfg)
cfg \<in> R_G.cfg_on s'
[PROOF STEP]
have "s \<in> \<S>"
[PROOF STATE]
proof (prove)
using this:
s' \<in> \<S>
s \<in> set_pmf (action cfg)
cfg \<in> R_G.cfg_on s'

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

goal (1 subgoal):
 1. abss (reps s) = s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> \<S>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<in> \<S>

goal (1 subgoal):
 1. abss (reps s) = s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
abss (reps s) = s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abss_S[intro]:
  assumes "(l, u) \<in> S"
  shows "abss (l, u) = (l, [u]\<^sub>\<R>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abss (l, u) = (l, [u]\<^sub>\<R>)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(l, u) \<in> S

goal (1 subgoal):
 1. abss (l, u) = (l, [u]\<^sub>\<R>)
[PROOF STEP]
unfolding abss_def
[PROOF STATE]
proof (prove)
using this:
(l, u) \<in> S

goal (1 subgoal):
 1. (case (l, u) of (l, u) \<Rightarrow> if u \<in> V then (l, [u]\<^sub>\<R>) else (l, - V)) = (l, [u]\<^sub>\<R>)
[PROOF STEP]
by auto


[STATEMENT]
lemma reps_\<S>[intro]:
  assumes "(l, R) \<in> \<S>"
  shows "reps (l, R) = (l, SOME u. u \<in> R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reps (l, R) = (l, SOME u. u \<in> R)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(l, R) \<in> \<S>

goal (1 subgoal):
 1. reps (l, R) = (l, SOME u. u \<in> R)
[PROOF STEP]
unfolding reps_def
[PROOF STATE]
proof (prove)
using this:
(l, R) \<in> \<S>

goal (1 subgoal):
 1. (case (l, R) of (l, R) \<Rightarrow> if R \<in> \<R> then (l, SOME u. u \<in> R) else (l, \<lambda>_. - 1)) = (l, SOME u. u \<in> R)
[PROOF STEP]
by auto


[STATEMENT]
lemma fst_abss:
  "fst (abss st) = fst st" for st
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (abss st) = fst st
[PROOF STEP]
by (cases st) (auto simp: abss_def)


[STATEMENT]
lemma K_elem_abss_inj:
  assumes A: "\<mu> \<in> K (l, u)" "(l, u) \<in> S"
  shows "inj_on abss \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on abss (set_pmf \<mu>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj_on abss (set_pmf \<mu>)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<mu> \<in> K (l, u)
(l, u) \<in> S
[PROOF STEP]
have "abss s' = (\<lambda> (l, u). (l, [u]\<^sub>\<R>)) s'" if "s' \<in> \<mu>" for s'
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> K (l, u)
(l, u) \<in> S

goal (1 subgoal):
 1. abss s' = (case s' of (l, u) \<Rightarrow> (l, [u]\<^sub>\<R>))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> K (l, u)
(l, u) \<in> S
s' \<in> set_pmf \<mu>

goal (1 subgoal):
 1. abss s' = (case s' of (l, u) \<Rightarrow> (l, [u]\<^sub>\<R>))
[PROOF STEP]
by (auto split: prod.split)
[PROOF STATE]
proof (state)
this:
?s'3 \<in> set_pmf \<mu> \<Longrightarrow> abss ?s'3 = (case ?s'3 of (l, u) \<Rightarrow> (l, [u]\<^sub>\<R>))

goal (1 subgoal):
 1. inj_on abss (set_pmf \<mu>)
[PROOF STEP]
from inj_on_cong[OF this] K_elem_abs_inj[OF A(1)]
[PROOF STATE]
proof (chain)
picking this:
(\<And>a. a \<in> ?A \<Longrightarrow> ?s'4 a \<in> set_pmf \<mu>) \<Longrightarrow> inj_on (\<lambda>a. abss (?s'4 a)) ?A = inj_on (\<lambda>a. case ?s'4 a of (l, u) \<Rightarrow> (l, [u]\<^sub>\<R>)) ?A
inj_on (\<lambda>(l, u). (l, [u]\<^sub>\<R>)) (set_pmf \<mu>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>a. a \<in> ?A \<Longrightarrow> ?s'4 a \<in> set_pmf \<mu>) \<Longrightarrow> inj_on (\<lambda>a. abss (?s'4 a)) ?A = inj_on (\<lambda>a. case ?s'4 a of (l, u) \<Rightarrow> (l, [u]\<^sub>\<R>)) ?A
inj_on (\<lambda>(l, u). (l, [u]\<^sub>\<R>)) (set_pmf \<mu>)

goal (1 subgoal):
 1. inj_on abss (set_pmf \<mu>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
inj_on abss (set_pmf \<mu>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma \<K>_elem_reps_inj:
  assumes A: "\<mu> \<in> \<K> (l, R)" "(l, R) \<in> \<S>"
  shows "inj_on reps \<mu>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on reps (set_pmf \<mu>)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inj_on reps (set_pmf \<mu>)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<mu> \<in> \<K> (l, R)
(l, R) \<in> \<S>
[PROOF STEP]
have "reps s' = (\<lambda> (l, R). (l, SOME u. u \<in> R)) s'" if "s' \<in> \<mu>" for s'
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> \<K> (l, R)
(l, R) \<in> \<S>

goal (1 subgoal):
 1. reps s' = (case s' of (l, R) \<Rightarrow> (l, SOME u. u \<in> R))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> \<K> (l, R)
(l, R) \<in> \<S>
s' \<in> set_pmf \<mu>

goal (1 subgoal):
 1. reps s' = (case s' of (l, R) \<Rightarrow> (l, SOME u. u \<in> R))
[PROOF STEP]
by (auto split: prod.split)
[PROOF STATE]
proof (state)
this:
?s'3 \<in> set_pmf \<mu> \<Longrightarrow> reps ?s'3 = (case ?s'3 of (l, R) \<Rightarrow> (l, SOME u. u \<in> R))

goal (1 subgoal):
 1. inj_on reps (set_pmf \<mu>)
[PROOF STEP]
from inj_on_cong[OF this] K_elem_repr_inj[OF A(1)]
[PROOF STATE]
proof (chain)
picking this:
(\<And>a. a \<in> ?A \<Longrightarrow> ?s'4 a \<in> set_pmf \<mu>) \<Longrightarrow> inj_on (\<lambda>a. reps (?s'4 a)) ?A = inj_on (\<lambda>a. case ?s'4 a of (l, R) \<Rightarrow> (l, SOME u. u \<in> R)) ?A
inj_on (\<lambda>(l, R). (l, SOME u. u \<in> R)) (set_pmf \<mu>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>a. a \<in> ?A \<Longrightarrow> ?s'4 a \<in> set_pmf \<mu>) \<Longrightarrow> inj_on (\<lambda>a. reps (?s'4 a)) ?A = inj_on (\<lambda>a. case ?s'4 a of (l, R) \<Rightarrow> (l, SOME u. u \<in> R)) ?A
inj_on (\<lambda>(l, R). (l, SOME u. u \<in> R)) (set_pmf \<mu>)

goal (1 subgoal):
 1. inj_on reps (set_pmf \<mu>)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
inj_on reps (set_pmf \<mu>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma P_elem_pmf_map_abss:
  assumes A: "\<mu> \<in> K (l, u)" "(l, u) \<in> S" "s' \<in> \<mu>"
  shows "pmf (map_pmf abss \<mu>) (abss s') = pmf \<mu> s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (map_pmf abss \<mu>) (abss s') = pmf \<mu> s'
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> K (l, u)
(l, u) \<in> S
s' \<in> set_pmf \<mu>

goal (1 subgoal):
 1. pmf (map_pmf abss \<mu>) (abss s') = pmf \<mu> s'
[PROOF STEP]
by (blast intro: pmf_map_inj K_elem_abss_inj)


[STATEMENT]
lemma \<K>_elem_pmf_map_reps:
  assumes A: "\<mu> \<in> \<K> (l, R)" "(l, R) \<in> \<S>" "(l', R') \<in> \<mu>"
  shows "pmf (map_pmf reps \<mu>) (reps (l', R')) = pmf \<mu> (l', R')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (map_pmf reps \<mu>) (reps (l', R')) = pmf \<mu> (l', R')
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> \<K> (l, R)
(l, R) \<in> \<S>
(l', R') \<in> set_pmf \<mu>

goal (1 subgoal):
 1. pmf (map_pmf reps \<mu>) (reps (l', R')) = pmf \<mu> (l', R')
[PROOF STEP]
by (blast intro: pmf_map_inj \<K>_elem_reps_inj)


[STATEMENT]
lemma not_\<S>_reps:
  "(l, R) \<notin> \<S> \<Longrightarrow> reps (l, R) \<notin> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, R) \<notin> \<S> \<Longrightarrow> reps (l, R) \<notin> S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (l, R) \<notin> \<S> \<Longrightarrow> reps (l, R) \<notin> S
[PROOF STEP]
assume "(l, R) \<notin> \<S>"
[PROOF STATE]
proof (state)
this:
(l, R) \<notin> \<S>

goal (1 subgoal):
 1. (l, R) \<notin> \<S> \<Longrightarrow> reps (l, R) \<notin> S
[PROOF STEP]
let ?u = "SOME u. u \<in> R"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (l, R) \<notin> \<S> \<Longrightarrow> reps (l, R) \<notin> S
[PROOF STEP]
have "\<not> ?u \<turnstile> inv_of A l" if "R \<in> \<R>" "l \<in> L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (SOME u. u \<in> R) \<turnstile> PTA.inv_of A l
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (SOME u. u \<in> R) \<turnstile> PTA.inv_of A l
[PROOF STEP]
(* XXX Refactor -- doing that kind of proof at other places too *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (SOME u. u \<in> R) \<turnstile> PTA.inv_of A l
[PROOF STEP]
from region_not_empty[OF finite(1)] \<open>R \<in> \<R>\<close>
[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]
have "\<exists>u. 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. \<exists>u. u \<in> R
[PROOF STEP]
by (auto simp: \<R>_def)
[PROOF STATE]
proof (state)
this:
\<exists>u. u \<in> R

goal (1 subgoal):
 1. \<not> (SOME u. u \<in> R) \<turnstile> PTA.inv_of A l
[PROOF STEP]
from someI_ex[OF this]
[PROOF STATE]
proof (chain)
picking this:
(SOME x. x \<in> R) \<in> R
[PROOF STEP]
have "?u \<in> R"
[PROOF STATE]
proof (prove)
using this:
(SOME x. x \<in> R) \<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 (1 subgoal):
 1. \<not> (SOME u. u \<in> R) \<turnstile> PTA.inv_of A l
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(SOME u. u \<in> R) \<in> R

goal (1 subgoal):
 1. \<not> (SOME u. u \<in> R) \<turnstile> PTA.inv_of A l
[PROOF STEP]
from \<open>(l, R) \<notin> \<S>\<close> that
[PROOF STATE]
proof (chain)
picking this:
(l, R) \<notin> \<S>
R \<in> \<R>
l \<in> L
[PROOF STEP]
have "\<not> R \<subseteq> \<lbrace>inv_of A l\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
(l, R) \<notin> \<S>
R \<in> \<R>
l \<in> L

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

goal (1 subgoal):
 1. \<not> (SOME u. u \<in> R) \<turnstile> PTA.inv_of A l
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(SOME u. u \<in> R) \<in> R
\<not> R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(SOME u. u \<in> R) \<in> R
\<not> R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}

goal (1 subgoal):
 1. \<not> (SOME u. u \<in> R) \<turnstile> PTA.inv_of A l
[PROOF STEP]
using ccompatible_inv[of l] \<open>R \<in> \<R>\<close>
[PROOF STATE]
proof (prove)
using this:
(SOME u. u \<in> R) \<in> R
\<not> R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
ccompatible \<R> (PTA.inv_of A l)
R \<in> \<R>

goal (1 subgoal):
 1. \<not> (SOME u. u \<in> R) \<turnstile> PTA.inv_of A l
[PROOF STEP]
unfolding ccompatible_def
[PROOF STATE]
proof (prove)
using this:
(SOME u. u \<in> R) \<in> R
\<not> R \<subseteq> {v. v \<turnstile> PTA.inv_of A l}
\<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>

goal (1 subgoal):
 1. \<not> (SOME u. u \<in> R) \<turnstile> PTA.inv_of A l
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<not> (SOME u. u \<in> R) \<turnstile> PTA.inv_of A l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>R \<in> \<R>; l \<in> L\<rbrakk> \<Longrightarrow> \<not> (SOME u. u \<in> R) \<turnstile> PTA.inv_of A l

goal (1 subgoal):
 1. (l, R) \<notin> \<S> \<Longrightarrow> reps (l, R) \<notin> S
[PROOF STEP]
with non_empty \<open>(l, R) \<notin> \<S>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<X> \<noteq> {}
(l, R) \<notin> \<S>
\<lbrakk>R \<in> \<R>; l \<in> L\<rbrakk> \<Longrightarrow> \<not> (SOME u. u \<in> R) \<turnstile> PTA.inv_of A l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<X> \<noteq> {}
(l, R) \<notin> \<S>
\<lbrakk>R \<in> \<R>; l \<in> L\<rbrakk> \<Longrightarrow> \<not> (SOME u. u \<in> R) \<turnstile> PTA.inv_of A l

goal (1 subgoal):
 1. reps (l, R) \<notin> S
[PROOF STEP]
unfolding \<S>_def S_def reps_def
[PROOF STATE]
proof (prove)
using this:
\<X> \<noteq> {}
(l, R) \<notin> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}}
\<lbrakk>R \<in> \<R>; l \<in> L\<rbrakk> \<Longrightarrow> \<not> (SOME u. u \<in> R) \<turnstile> PTA.inv_of A l

goal (1 subgoal):
 1. (case (l, R) of (l, R) \<Rightarrow> if R \<in> \<R> then (l, SOME u. u \<in> R) else (l, \<lambda>_. - 1)) \<notin> {(l, u). l \<in> L \<and> (\<forall>x\<in>\<X>. 0 \<le> u x) \<and> u \<turnstile> PTA.inv_of A l}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
reps (l, R) \<notin> S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma neq_V_not_region:
  "-V \<notin> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - V \<notin> \<R>
[PROOF STEP]
using \<R>_V rep_\<R>_ex
[PROOF STATE]
proof (prove)
using this:
\<Union> \<R> = V
?R \<in> \<R> \<Longrightarrow> (SOME u. u \<in> ?R) \<in> ?R

goal (1 subgoal):
 1. - V \<notin> \<R>
[PROOF STEP]
by auto


[STATEMENT]
lemma \<S>_abss_S:
  "abss s \<in> \<S> \<Longrightarrow> s \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abss s \<in> \<S> \<Longrightarrow> s \<in> S
[PROOF STEP]
unfolding abss_def \<S>_def S_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case s of (l, u) \<Rightarrow> if u \<in> V then (l, [u]\<^sub>\<R>) else (l, - V)) \<in> {(l, R). l \<in> L \<and> R \<in> \<R> \<and> R \<subseteq> {u. u \<turnstile> PTA.inv_of A l}} \<Longrightarrow> s \<in> {(l, u). l \<in> L \<and> (\<forall>x\<in>\<X>. 0 \<le> u x) \<and> u \<turnstile> PTA.inv_of A l}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y l u. \<lbrakk>(if u \<in> V then (l, [u]\<^sub>\<R>) else (l, - V)) = (x, y); s = (l, u); x \<in> L; y \<in> \<R>; y \<subseteq> {u. u \<turnstile> PTA.inv_of A x}\<rbrakk> \<Longrightarrow> l \<in> L
 2. \<And>x y l u xa. \<lbrakk>(if u \<in> V then (l, [u]\<^sub>\<R>) else (l, - V)) = (x, y); s = (l, u); x \<in> L; y \<in> \<R>; y \<subseteq> {u. u \<turnstile> PTA.inv_of A x}; xa \<in> \<X>\<rbrakk> \<Longrightarrow> 0 \<le> u xa
 3. \<And>x y l u. \<lbrakk>(if u \<in> V then (l, [u]\<^sub>\<R>) else (l, - V)) = (x, y); s = (l, u); x \<in> L; y \<in> \<R>; y \<subseteq> {u. u \<turnstile> PTA.inv_of A x}\<rbrakk> \<Longrightarrow> u \<turnstile> PTA.inv_of A l
[PROOF STEP]
subgoal for _ _ _ u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(if u \<in> V then (l_, [u]\<^sub>\<R>) else (l_, - V)) = (x_, y_); s = (l_, u); x_ \<in> L; y_ \<in> \<R>; y_ \<subseteq> {u. u \<turnstile> PTA.inv_of A x_}\<rbrakk> \<Longrightarrow> l_ \<in> L
[PROOF STEP]
by (cases "u \<in> V") auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y l u xa. \<lbrakk>(if u \<in> V then (l, [u]\<^sub>\<R>) else (l, - V)) = (x, y); s = (l, u); x \<in> L; y \<in> \<R>; y \<subseteq> {u. u \<turnstile> PTA.inv_of A x}; xa \<in> \<X>\<rbrakk> \<Longrightarrow> 0 \<le> u xa
 2. \<And>x y l u. \<lbrakk>(if u \<in> V then (l, [u]\<^sub>\<R>) else (l, - V)) = (x, y); s = (l, u); x \<in> L; y \<in> \<R>; y \<subseteq> {u. u \<turnstile> PTA.inv_of A x}\<rbrakk> \<Longrightarrow> u \<turnstile> PTA.inv_of A l
[PROOF STEP]
subgoal for _ _ _ u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(if u \<in> V then (l_, [u]\<^sub>\<R>) else (l_, - V)) = (x_, y_); s = (l_, u); x_ \<in> L; y_ \<in> \<R>; y_ \<subseteq> {u. u \<turnstile> PTA.inv_of A x_}; xa_ \<in> \<X>\<rbrakk> \<Longrightarrow> 0 \<le> u xa_
[PROOF STEP]
using neq_V_not_region
[PROOF STATE]
proof (prove)
using this:
- V \<notin> \<R>

goal (1 subgoal):
 1. \<lbrakk>(if u \<in> V then (l_, [u]\<^sub>\<R>) else (l_, - V)) = (x_, y_); s = (l_, u); x_ \<in> L; y_ \<in> \<R>; y_ \<subseteq> {u. u \<turnstile> PTA.inv_of A x_}; xa_ \<in> \<X>\<rbrakk> \<Longrightarrow> 0 \<le> u xa_
[PROOF STEP]
by (cases "u \<in> V", (auto simp: V_def; fail), auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y l u. \<lbrakk>(if u \<in> V then (l, [u]\<^sub>\<R>) else (l, - V)) = (x, y); s = (l, u); x \<in> L; y \<in> \<R>; y \<subseteq> {u. u \<turnstile> PTA.inv_of A x}\<rbrakk> \<Longrightarrow> u \<turnstile> PTA.inv_of A l
[PROOF STEP]
subgoal for l' y l u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(if u \<in> V then (l, [u]\<^sub>\<R>) else (l, - V)) = (l', y); s = (l, u); l' \<in> L; y \<in> \<R>; y \<subseteq> {u. u \<turnstile> PTA.inv_of A l'}\<rbrakk> \<Longrightarrow> u \<turnstile> PTA.inv_of A l
[PROOF STEP]
using neq_V_not_region
[PROOF STATE]
proof (prove)
using this:
- V \<notin> \<R>

goal (1 subgoal):
 1. \<lbrakk>(if u \<in> V then (l, [u]\<^sub>\<R>) else (l, - V)) = (l', y); s = (l, u); l' \<in> L; y \<in> \<R>; y \<subseteq> {u. u \<turnstile> PTA.inv_of A l'}\<rbrakk> \<Longrightarrow> u \<turnstile> PTA.inv_of A l
[PROOF STEP]
by (cases "u \<in> V"; auto dest: regions_part_ex)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma S_pred_stream_abss_\<S>:
  "pred_stream (\<lambda> s. s \<in> S) xs \<longleftrightarrow> pred_stream (\<lambda> s. s \<in> \<S>) (smap abss xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pred_stream (\<lambda>s. s \<in> S) xs = pred_stream (\<lambda>s. s \<in> \<S>) (smap abss xs)
[PROOF STEP]
using S_abss_\<S> \<S>_abss_S
[PROOF STATE]
proof (prove)
using this:
?s \<in> S \<Longrightarrow> abss ?s \<in> \<S>
abss ?s \<in> \<S> \<Longrightarrow> ?s \<in> S

goal (1 subgoal):
 1. pred_stream (\<lambda>s. s \<in> S) xs = pred_stream (\<lambda>s. s \<in> \<S>) (smap abss xs)
[PROOF STEP]
by (auto simp: stream.pred_set)


[STATEMENT]
lemma K_closed:
  "s \<in> S \<Longrightarrow> (\<Union>D\<in>K s. set_pmf D) \<subseteq> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> S \<Longrightarrow> \<Union> (set_pmf ` K s) \<subseteq> S
[PROOF STEP]
by auto


[STATEMENT]
lemma bisim_loc_id[intro]:
  "(l, u) ~ (l', u') \<Longrightarrow> l = l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, u) ~ (l', u') \<Longrightarrow> l = l'
[PROOF STEP]
unfolding abss_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (l, u) of (l, u) \<Rightarrow> if u \<in> V then (l, [u]\<^sub>\<R>) else (l, - V)) = (case (l', u') of (l, u) \<Rightarrow> if u \<in> V then (l, [u]\<^sub>\<R>) else (l, - V)) \<Longrightarrow> l = l'
[PROOF STEP]
by (cases "u \<in> V"; cases "u' \<in> V"; simp)


[STATEMENT]
lemma bisim_val_id[intro]:
  "[u]\<^sub>\<R> = [u']\<^sub>\<R>" if "u \<in> V" "(l, u) ~ (l', u')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [u]\<^sub>\<R> = [u']\<^sub>\<R>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [u]\<^sub>\<R> = [u']\<^sub>\<R>
[PROOF STEP]
have "(l', - V) \<noteq> (l, [u]\<^sub>\<R>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l', - V) \<noteq> (l, [u]\<^sub>\<R>)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
u \<in> V
(l, u) ~ (l', u')

goal (1 subgoal):
 1. (l', - V) \<noteq> (l, [u]\<^sub>\<R>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(l', - V) \<noteq> (l, [u]\<^sub>\<R>)

goal (1 subgoal):
 1. [u]\<^sub>\<R> = [u']\<^sub>\<R>
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
u \<in> V
(l, u) ~ (l', u')
(l', - V) \<noteq> (l, [u]\<^sub>\<R>)
[PROOF STEP]
have "u' \<in> V"
[PROOF STATE]
proof (prove)
using this:
u \<in> V
(l, u) ~ (l', u')
(l', - V) \<noteq> (l, [u]\<^sub>\<R>)

goal (1 subgoal):
 1. u' \<in> V
[PROOF STEP]
by (force simp: abss_def)
[PROOF STATE]
proof (state)
this:
u' \<in> V

goal (1 subgoal):
 1. [u]\<^sub>\<R> = [u']\<^sub>\<R>
[PROOF STEP]
with that
[PROOF STATE]
proof (chain)
picking this:
u \<in> V
(l, u) ~ (l', u')
u' \<in> V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<in> V
(l, u) ~ (l', u')
u' \<in> V

goal (1 subgoal):
 1. [u]\<^sub>\<R> = [u']\<^sub>\<R>
[PROOF STEP]
by (simp add: abss_def)
[PROOF STATE]
proof (state)
this:
[u]\<^sub>\<R> = [u']\<^sub>\<R>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bisim_symmetric:
  "(l, u) ~ (l', u') = (l', u') ~ (l, u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, u) ~ (l', u') = (l', u') ~ (l, u)
[PROOF STEP]
by (rule eq_commute)


[STATEMENT]
lemma bisim_val_id2[intro]:
  "u' \<in> V \<Longrightarrow> (l, u) ~ (l', u') \<Longrightarrow> [u]\<^sub>\<R> = [u']\<^sub>\<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u' \<in> V; (l, u) ~ (l', u')\<rbrakk> \<Longrightarrow> [u]\<^sub>\<R> = [u']\<^sub>\<R>
[PROOF STEP]
apply (subst (asm) eq_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u' \<in> V; (l', u') ~ (l, u)\<rbrakk> \<Longrightarrow> [u]\<^sub>\<R> = [u']\<^sub>\<R>
[PROOF STEP]
apply (subst eq_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>u' \<in> V; (l', u') ~ (l, u)\<rbrakk> \<Longrightarrow> [u']\<^sub>\<R> = [u]\<^sub>\<R>
[PROOF STEP]
apply (rule bisim_val_id)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>u' \<in> V; (l', u') ~ (l, u)\<rbrakk> \<Longrightarrow> u' \<in> V
 2. \<lbrakk>u' \<in> V; (l', u') ~ (l, u)\<rbrakk> \<Longrightarrow> (?l1, u') ~ (?l'1, u)
[PROOF STEP]
by auto


[STATEMENT]
lemma K_bisim_unique:
  assumes "s \<in> S" "\<mu> \<in> K s" "x \<in> \<mu>" "x' \<in> \<mu>" "x ~ x'"
  shows "x = x'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x'
[PROOF STEP]
using assms(2,1,3-)
[PROOF STATE]
proof (prove)
using this:
\<mu> \<in> K s
s \<in> S
x \<in> set_pmf \<mu>
x' \<in> set_pmf \<mu>
x ~ x'

goal (1 subgoal):
 1. x = x'
[PROOF STEP]
proof (cases rule: K.cases)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>l u t. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf (l, u \<oplus> t); s \<in> S; s = (l, u); 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l\<rbrakk> \<Longrightarrow> x = x'
 2. \<And>l u g \<mu>'. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'; s \<in> S; s = (l, u); (l, g, \<mu>') \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> x = x'
 3. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf s\<rbrakk> \<Longrightarrow> x = x'
[PROOF STEP]
case prems: (action l u \<tau> \<mu>')
[PROOF STATE]
proof (state)
this:
\<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'
s \<in> S
s = (l, u)
(l, \<tau>, \<mu>') \<in> PTA.trans_of A
u \<turnstile> \<tau>

goal (3 subgoals):
 1. \<And>l u t. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf (l, u \<oplus> t); s \<in> S; s = (l, u); 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l\<rbrakk> \<Longrightarrow> x = x'
 2. \<And>l u g \<mu>'. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'; s \<in> S; s = (l, u); (l, g, \<mu>') \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> x = x'
 3. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf s\<rbrakk> \<Longrightarrow> x = x'
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
\<mu> \<in> K s
x \<in> set_pmf \<mu>
x' \<in> set_pmf \<mu>
x ~ x'
\<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'
s \<in> S
s = (l, u)
(l, \<tau>, \<mu>') \<in> PTA.trans_of A
u \<turnstile> \<tau>
[PROOF STEP]
obtain l1 l2 X1 X2 where A:
    "(X1, l1) \<in> set_pmf \<mu>'" "(X2, l2) \<in> set_pmf \<mu>'"
    "x = (l1, [X1:=0]u)" "x' = (l2, [X2:=0]u)"
[PROOF STATE]
proof (prove)
using this:
s \<in> S
\<mu> \<in> K s
x \<in> set_pmf \<mu>
x' \<in> set_pmf \<mu>
x ~ x'
\<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'
s \<in> S
s = (l, u)
(l, \<tau>, \<mu>') \<in> PTA.trans_of A
u \<turnstile> \<tau>

goal (1 subgoal):
 1. (\<And>X1 l1 X2 l2. \<lbrakk>(X1, l1) \<in> set_pmf \<mu>'; (X2, l2) \<in> set_pmf \<mu>'; x = (l1, [(SOME r. set r = X1)\<rightarrow>0]u); x' = (l2, [(SOME r. set r = X2)\<rightarrow>0]u)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(X1, l1) \<in> set_pmf \<mu>'
(X2, l2) \<in> set_pmf \<mu>'
x = (l1, [(SOME r. set r = X1)\<rightarrow>0]u)
x' = (l2, [(SOME r. set r = X2)\<rightarrow>0]u)

goal (3 subgoals):
 1. \<And>l u t. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf (l, u \<oplus> t); s \<in> S; s = (l, u); 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l\<rbrakk> \<Longrightarrow> x = x'
 2. \<And>l u g \<mu>'. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'; s \<in> S; s = (l, u); (l, g, \<mu>') \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> x = x'
 3. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf s\<rbrakk> \<Longrightarrow> x = x'
[PROOF STEP]
from \<open>x ~ x'\<close> A \<open>s \<in> S\<close> \<open>s = (l, u)\<close>
[PROOF STATE]
proof (chain)
picking this:
x ~ x'
(X1, l1) \<in> set_pmf \<mu>'
(X2, l2) \<in> set_pmf \<mu>'
x = (l1, [(SOME r. set r = X1)\<rightarrow>0]u)
x' = (l2, [(SOME r. set r = X2)\<rightarrow>0]u)
s \<in> S
s = (l, u)
[PROOF STEP]
have "[[X1:=0]u]\<^sub>\<R> = [[X2:=0]u]\<^sub>\<R>"
[PROOF STATE]
proof (prove)
using this:
x ~ x'
(X1, l1) \<in> set_pmf \<mu>'
(X2, l2) \<in> set_pmf \<mu>'
x = (l1, [(SOME r. set r = X1)\<rightarrow>0]u)
x' = (l2, [(SOME r. set r = X2)\<rightarrow>0]u)
s \<in> S
s = (l, u)

goal (1 subgoal):
 1. [[(SOME r. set r = X1)\<rightarrow>0]u]\<^sub>\<R> = [[(SOME r. set r = X2)\<rightarrow>0]u]\<^sub>\<R>
[PROOF STEP]
using bisim_val_id[OF S_V] K_S_closed assms(2-4)
[PROOF STATE]
proof (prove)
using this:
x ~ x'
(X1, l1) \<in> set_pmf \<mu>'
(X2, l2) \<in> set_pmf \<mu>'
x = (l1, [(SOME r. set r = X1)\<rightarrow>0]u)
x' = (l2, [(SOME r. set r = X2)\<rightarrow>0]u)
s \<in> S
s = (l, u)
\<lbrakk>(?l1, ?u) \<in> S; (?l, ?u) ~ (?l', ?u')\<rbrakk> \<Longrightarrow> [?u]\<^sub>\<R> = [?u']\<^sub>\<R>
\<lbrakk>?\<mu> \<in> K ?s; ?s' \<in> set_pmf ?\<mu>; ?s \<in> S\<rbrakk> \<Longrightarrow> ?s' \<in> S
\<mu> \<in> K s
x \<in> set_pmf \<mu>
x' \<in> set_pmf \<mu>

goal (1 subgoal):
 1. [[(SOME r. set r = X1)\<rightarrow>0]u]\<^sub>\<R> = [[(SOME r. set r = X2)\<rightarrow>0]u]\<^sub>\<R>
[PROOF STEP]
by (auto intro!: bisim_val_id[OF S_V])
[PROOF STATE]
proof (state)
this:
[[(SOME r. set r = X1)\<rightarrow>0]u]\<^sub>\<R> = [[(SOME r. set r = X2)\<rightarrow>0]u]\<^sub>\<R>

goal (3 subgoals):
 1. \<And>l u t. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf (l, u \<oplus> t); s \<in> S; s = (l, u); 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l\<rbrakk> \<Longrightarrow> x = x'
 2. \<And>l u g \<mu>'. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'; s \<in> S; s = (l, u); (l, g, \<mu>') \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> x = x'
 3. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf s\<rbrakk> \<Longrightarrow> x = x'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[[(SOME r. set r = X1)\<rightarrow>0]u]\<^sub>\<R> = [[(SOME r. set r = X2)\<rightarrow>0]u]\<^sub>\<R>
[PROOF STEP]
have "[X1:=0]u = [X2:=0]u"
[PROOF STATE]
proof (prove)
using this:
[[(SOME r. set r = X1)\<rightarrow>0]u]\<^sub>\<R> = [[(SOME r. set r = X2)\<rightarrow>0]u]\<^sub>\<R>

goal (1 subgoal):
 1. [(SOME r. set r = X1)\<rightarrow>0]u = [(SOME r. set r = X2)\<rightarrow>0]u
[PROOF STEP]
using A admissible_targets_clocks(2)[OF prems(4)] prems(2,3)
[PROOF STATE]
proof (prove)
using this:
[[(SOME r. set r = X1)\<rightarrow>0]u]\<^sub>\<R> = [[(SOME r. set r = X2)\<rightarrow>0]u]\<^sub>\<R>
(X1, l1) \<in> set_pmf \<mu>'
(X2, l2) \<in> set_pmf \<mu>'
x = (l1, [(SOME r. set r = X1)\<rightarrow>0]u)
x' = (l2, [(SOME r. set r = X2)\<rightarrow>0]u)
(?X, ?l') \<in> set_pmf \<mu>' \<Longrightarrow> set (SOME r. set r = ?X) \<subseteq> \<X>
s \<in> S
s = (l, u)

goal (1 subgoal):
 1. [(SOME r. set r = X1)\<rightarrow>0]u = [(SOME r. set r = X2)\<rightarrow>0]u
[PROOF STEP]
by - (rule reset_eq, force)
[PROOF STATE]
proof (state)
this:
[(SOME r. set r = X1)\<rightarrow>0]u = [(SOME r. set r = X2)\<rightarrow>0]u

goal (3 subgoals):
 1. \<And>l u t. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf (l, u \<oplus> t); s \<in> S; s = (l, u); 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l\<rbrakk> \<Longrightarrow> x = x'
 2. \<And>l u g \<mu>'. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = map_pmf (\<lambda>(X, l). (l, [(SOME r. set r = X)\<rightarrow>0]u)) \<mu>'; s \<in> S; s = (l, u); (l, g, \<mu>') \<in> PTA.trans_of A; u \<turnstile> g\<rbrakk> \<Longrightarrow> x = x'
 3. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf s\<rbrakk> \<Longrightarrow> x = x'
[PROOF STEP]
with A \<open>x ~ x'\<close>
[PROOF STATE]
proof (chain)
picking this:
(X1, l1) \<in> set_pmf \<mu>'
(X2, l2) \<in> set_pmf \<mu>'
x = (l1, [(SOME r. set r = X1)\<rightarrow>0]u)
x' = (l2, [(SOME r. set r = X2)\<rightarrow>0]u)
x ~ x'
[(SOME r. set r = X1)\<rightarrow>0]u = [(SOME r. set r = X2)\<rightarrow>0]u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(X1, l1) \<in> set_pmf \<mu>'
(X2, l2) \<in> set_pmf \<mu>'
x = (l1, [(SOME r. set r = X1)\<rightarrow>0]u)
x' = (l2, [(SOME r. set r = X2)\<rightarrow>0]u)
x ~ x'
[(SOME r. set r = X1)\<rightarrow>0]u = [(SOME r. set r = X2)\<rightarrow>0]u

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

goal (2 subgoals):
 1. \<And>l u t. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf (l, u \<oplus> t); s \<in> S; s = (l, u); 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l\<rbrakk> \<Longrightarrow> x = x'
 2. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf s\<rbrakk> \<Longrightarrow> x = x'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l u t. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf (l, u \<oplus> t); s \<in> S; s = (l, u); 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l\<rbrakk> \<Longrightarrow> x = x'
 2. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf s\<rbrakk> \<Longrightarrow> x = x'
[PROOF STEP]
case delay
[PROOF STATE]
proof (state)
this:
\<mu> = return_pmf (l_, u_ \<oplus> t_)
s \<in> S
s = (l_, u_)
0 \<le> t_
u_ \<oplus> t_ \<turnstile> PTA.inv_of A l_

goal (2 subgoals):
 1. \<And>l u t. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf (l, u \<oplus> t); s \<in> S; s = (l, u); 0 \<le> t; u \<oplus> t \<turnstile> PTA.inv_of A l\<rbrakk> \<Longrightarrow> x = x'
 2. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf s\<rbrakk> \<Longrightarrow> x = x'
[PROOF STEP]
with assms(3-)
[PROOF STATE]
proof (chain)
picking this:
x \<in> set_pmf \<mu>
x' \<in> set_pmf \<mu>
x ~ x'
\<mu> = return_pmf (l_, u_ \<oplus> t_)
s \<in> S
s = (l_, u_)
0 \<le> t_
u_ \<oplus> t_ \<turnstile> PTA.inv_of A l_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> set_pmf \<mu>
x' \<in> set_pmf \<mu>
x ~ x'
\<mu> = return_pmf (l_, u_ \<oplus> t_)
s \<in> S
s = (l_, u_)
0 \<le> t_
u_ \<oplus> t_ \<turnstile> PTA.inv_of A l_

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

goal (1 subgoal):
 1. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf s\<rbrakk> \<Longrightarrow> x = x'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf s\<rbrakk> \<Longrightarrow> x = x'
[PROOF STEP]
case loop
[PROOF STATE]
proof (state)
this:
\<mu> = return_pmf s

goal (1 subgoal):
 1. \<lbrakk>s \<in> S; x \<in> set_pmf \<mu>; x' \<in> set_pmf \<mu>; x ~ x'; \<mu> = return_pmf s\<rbrakk> \<Longrightarrow> x = x'
[PROOF STEP]
with assms(3-)
[PROOF STATE]
proof (chain)
picking this:
x \<in> set_pmf \<mu>
x' \<in> set_pmf \<mu>
x ~ x'
\<mu> = return_pmf s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> set_pmf \<mu>
x' \<in> set_pmf \<mu>
x ~ x'
\<mu> = return_pmf s

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abss_\<S>D:
  assumes "abss s \<in> \<S>"
  obtains l u where "s = (l, u)" "u \<in> [u]\<^sub>\<R>" "[u]\<^sub>\<R> \<in> \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>l u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain l u where "s = (l, u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l u. s = (l, u) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
s = (l, u)

goal (1 subgoal):
 1. (\<And>l u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
s = (l, u)

goal (1 subgoal):
 1. (\<And>l u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<S>_abss_S[OF assms]
[PROOF STATE]
proof (chain)
picking this:
s \<in> S
[PROOF STEP]
have "s \<in> S"
[PROOF STATE]
proof (prove)
using this:
s \<in> S

goal (1 subgoal):
 1. s \<in> S
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
s \<in> S

goal (1 subgoal):
 1. (\<And>l u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
s = (l, u)
s \<in> S
[PROOF STEP]
have "abss s = (l, [u]\<^sub>\<R>)" "u \<in> V" "u \<in> [u]\<^sub>\<R>" "[u]\<^sub>\<R> \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
s = (l, u)
s \<in> S

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

goal (1 subgoal):
 1. (\<And>l u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with \<open>s = _\<close>
[PROOF STATE]
proof (chain)
picking this:
s = (l, u)
abss s = (l, [u]\<^sub>\<R>)
u \<in> V
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s = (l, u)
abss s = (l, [u]\<^sub>\<R>)
u \<in> V
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (auto intro: that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abss_\<S>D':
  assumes "abss s \<in> \<S>" "abss s = (l, R)"
  obtains u where "s = (l, u)" "u \<in> [u]\<^sub>\<R>" "[u]\<^sub>\<R> \<in> \<R>" "R = [u]\<^sub>\<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>; R = [u]\<^sub>\<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>; R = [u]\<^sub>\<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from abss_\<S>D[OF assms(1)]
[PROOF STATE]
proof (chain)
picking this:
(\<And>l u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain l' u where u:
    "s = (l', u)" "u \<in> [u]\<^sub>\<R>" "[u]\<^sub>\<R> \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
(\<And>l u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>l' u. \<lbrakk>s = (l', u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
s = (l', u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>; R = [u]\<^sub>\<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with \<R>_V
[PROOF STATE]
proof (chain)
picking this:
\<Union> \<R> = V
s = (l', u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
[PROOF STEP]
have "u \<in> V"
[PROOF STATE]
proof (prove)
using this:
\<Union> \<R> = V
s = (l', u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>

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

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>; R = [u]\<^sub>\<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with \<open>s = _\<close> assms(2)
[PROOF STATE]
proof (chain)
picking this:
s = (l', u)
abss s = (l, R)
u \<in> V
[PROOF STEP]
have "l' = l" "R = [u]\<^sub>\<R>"
[PROOF STATE]
proof (prove)
using this:
s = (l', u)
abss s = (l, R)
u \<in> V

goal (1 subgoal):
 1. l' = l &&& R = [u]\<^sub>\<R>
[PROOF STEP]
unfolding abss_def
[PROOF STATE]
proof (prove)
using this:
s = (l', u)
(case s of (l, u) \<Rightarrow> if u \<in> V then (l, [u]\<^sub>\<R>) else (l, - V)) = (l, R)
u \<in> V

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

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>s = (l, u); u \<in> [u]\<^sub>\<R>; [u]\<^sub>\<R> \<in> \<R>; R = [u]\<^sub>\<R>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with u
[PROOF STATE]
proof (chain)
picking this:
s = (l', u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
l' = l
R = [u]\<^sub>\<R>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s = (l', u)
u \<in> [u]\<^sub>\<R>
[u]\<^sub>\<R> \<in> \<R>
l' = l
R = [u]\<^sub>\<R>

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (auto intro: that)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delayedR_correct_aux_aux:
  fixes c :: nat
  fixes a b :: real
  assumes "c < a" "a < Suc c" "b \<ge> 0" "a + b < Suc c"
  shows "frac (a + b) = frac a + b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frac (a + b) = frac a + b
[PROOF STEP]
(* Working alternative:
by (smt One_nat_def add.right_neutral add_Suc_right assms nat_intv_frac_decomp)
*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frac (a + b) = frac a + b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. frac (a + b) = frac a + b
[PROOF STEP]
have f1: "a + b < real (c + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + b < real (c + 1)
[PROOF STEP]
using assms(4)
[PROOF STATE]
proof (prove)
using this:
a + b < real (Suc c)

goal (1 subgoal):
 1. a + b < real (c + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a + b < real (c + 1)

goal (1 subgoal):
 1. frac (a + b) = frac a + b
[PROOF STEP]
have f2: "\<And>r ra. (r::real) + (- r + ra) = ra"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra. r + (- r + ra) = ra
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
?r5 + (- ?r5 + ?ra5) = ?ra5

goal (1 subgoal):
 1. frac (a + b) = frac a + b
[PROOF STEP]
have f3: "\<And>r. (r::real) = - (- r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. r = - (- r)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
?r5 = - (- ?r5)

goal (1 subgoal):
 1. frac (a + b) = frac a + b
[PROOF STEP]
have f4: "\<And>r ra. - (r::real) + (ra + r) = ra"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r ra. - r + (ra + r) = ra
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
- ?r5 + (?ra5 + ?r5) = ?ra5

goal (1 subgoal):
 1. frac (a + b) = frac a + b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
- ?r5 + (?ra5 + ?r5) = ?ra5
[PROOF STEP]
have f5: "\<And>r n. r + - frac r = real n \<or> \<not> r < real (n + 1) \<or> \<not> real n < r"
[PROOF STATE]
proof (prove)
using this:
- ?r5 + (?ra5 + ?r5) = ?ra5

goal (1 subgoal):
 1. \<And>r n. r + - frac r = real n \<or> \<not> r < real (n + 1) \<or> \<not> real n < r
[PROOF STEP]
using f2
[PROOF STATE]
proof (prove)
using this:
- ?r5 + (?ra5 + ?r5) = ?ra5
?r5 + (- ?r5 + ?ra5) = ?ra5

goal (1 subgoal):
 1. \<And>r n. r + - frac r = real n \<or> \<not> r < real (n + 1) \<or> \<not> real n < r
[PROOF STEP]
by (metis nat_intv_frac_decomp)
[PROOF STATE]
proof (state)
this:
?r5 + - frac ?r5 = real ?n5 \<or> \<not> ?r5 < real (?n5 + 1) \<or> \<not> real ?n5 < ?r5

goal (1 subgoal):
 1. frac (a + b) = frac a + b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?r5 + - frac ?r5 = real ?n5 \<or> \<not> ?r5 < real (?n5 + 1) \<or> \<not> real ?n5 < ?r5
[PROOF STEP]
have "frac a + real c = a"
[PROOF STATE]
proof (prove)
using this:
?r5 + - frac ?r5 = real ?n5 \<or> \<not> ?r5 < real (?n5 + 1) \<or> \<not> real ?n5 < ?r5

goal (1 subgoal):
 1. frac a + real c = a
[PROOF STEP]
using f4 f3
[PROOF STATE]
proof (prove)
using this:
?r5 + - frac ?r5 = real ?n5 \<or> \<not> ?r5 < real (?n5 + 1) \<or> \<not> real ?n5 < ?r5
- ?r5 + (?ra5 + ?r5) = ?ra5
?r5 = - (- ?r5)

goal (1 subgoal):
 1. frac a + real c = a
[PROOF STEP]
by (metis One_nat_def add.right_neutral add_Suc_right assms(1) assms(2))
[PROOF STATE]
proof (state)
this:
frac a + real c = a

goal (1 subgoal):
 1. frac (a + b) = frac a + b
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
frac a + real c = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
frac a + real c = a

goal (1 subgoal):
 1. frac (a + b) = frac a + b
[PROOF STEP]
using f5 f1 assms(1) assms(3)
[PROOF STATE]
proof (prove)
using this:
frac a + real c = a
?r5 + - frac ?r5 = real ?n5 \<or> \<not> ?r5 < real (?n5 + 1) \<or> \<not> real ?n5 < ?r5
a + b < real (c + 1)
real c < a
0 \<le> b

goal (1 subgoal):
 1. frac (a + b) = frac a + b
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
frac (a + b) = frac a + b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delayedR_correct_aux:
  fixes I r
  defines "R \<equiv> region \<X> I r"
  assumes "u \<in> R" "valid_region \<X> k I r" "\<forall> c \<in> \<X>. \<not> isConst (I c)"
          "\<forall> c \<in> \<X>. isIntv (I c) \<longrightarrow> (u \<oplus> t) c < intv_const (I c) + 1"
          "t \<ge> 0"
  shows "u \<oplus> t \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<oplus> t \<in> R
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<oplus> t \<in> Regions.region \<X> I r
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>x\<in>\<X>. 0 \<le> (u \<oplus> t) x
 2. \<forall>x\<in>\<X>. Regions.intv_elem x (u \<oplus> t) (I x)
 3. ?X\<^sub>0 = {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}
 4. \<forall>x\<in>?X\<^sub>0. \<forall>y\<in>?X\<^sub>0. ((x, y) \<in> r) = (frac ((u \<oplus> t) x) \<le> frac ((u \<oplus> t) y))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
R \<equiv> Regions.region \<X> I r
u \<in> R
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> t) c < real (intv_const (I c) + 1)
0 \<le> t
[PROOF STEP]
have "R \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
R \<equiv> Regions.region \<X> I r
u \<in> R
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> t) c < real (intv_const (I c) + 1)
0 \<le> t

goal (1 subgoal):
 1. R \<in> \<R>
[PROOF STEP]
unfolding \<R>_def
[PROOF STATE]
proof (prove)
using this:
R \<equiv> Regions.region \<X> I r
u \<in> R
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> t) c < real (intv_const (I c) + 1)
0 \<le> t

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

goal (4 subgoals):
 1. \<forall>x\<in>\<X>. 0 \<le> (u \<oplus> t) x
 2. \<forall>x\<in>\<X>. Regions.intv_elem x (u \<oplus> t) (I x)
 3. ?X\<^sub>0 = {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}
 4. \<forall>x\<in>?X\<^sub>0. \<forall>y\<in>?X\<^sub>0. ((x, y) \<in> r) = (frac ((u \<oplus> t) x) \<le> frac ((u \<oplus> t) y))
[PROOF STEP]
with \<open>u \<in> R\<close> \<R>_V
[PROOF STATE]
proof (chain)
picking this:
u \<in> R
\<Union> \<R> = V
R \<in> \<R>
[PROOF STEP]
have "u \<in> V"
[PROOF STATE]
proof (prove)
using this:
u \<in> R
\<Union> \<R> = V
R \<in> \<R>

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

goal (4 subgoals):
 1. \<forall>x\<in>\<X>. 0 \<le> (u \<oplus> t) x
 2. \<forall>x\<in>\<X>. Regions.intv_elem x (u \<oplus> t) (I x)
 3. ?X\<^sub>0 = {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}
 4. \<forall>x\<in>?X\<^sub>0. \<forall>y\<in>?X\<^sub>0. ((x, y) \<in> r) = (frac ((u \<oplus> t) x) \<le> frac ((u \<oplus> t) y))
[PROOF STEP]
with \<open>t \<ge> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
0 \<le> t
u \<in> V
[PROOF STEP]
show "\<forall>x\<in>\<X>. 0 \<le> (u \<oplus> t) x"
[PROOF STATE]
proof (prove)
using this:
0 \<le> t
u \<in> V

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

goal (1 subgoal):
 1. \<forall>x\<in>\<X>. 0 \<le> (u \<oplus> t) x
[PROOF STEP]
by (auto simp: cval_add_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>\<X>. 0 \<le> (u \<oplus> t) x

goal (3 subgoals):
 1. \<forall>x\<in>\<X>. Regions.intv_elem x (u \<oplus> t) (I x)
 2. ?X\<^sub>0 = {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}
 3. \<forall>x\<in>?X\<^sub>0. \<forall>y\<in>?X\<^sub>0. ((x, y) \<in> r) = (frac ((u \<oplus> t) x) \<le> frac ((u \<oplus> t) y))
[PROOF STEP]
have "intv_elem x (u \<oplus> t) (I x)" if "x \<in> \<X>" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Regions.intv_elem x (u \<oplus> t) (I x)
[PROOF STEP]
proof (cases "I x")
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1. I x = Regions.intv.Const x1 \<Longrightarrow> Regions.intv_elem x (u \<oplus> t) (I x)
 2. \<And>x2. I x = Regions.intv.Intv x2 \<Longrightarrow> Regions.intv_elem x (u \<oplus> t) (I x)
 3. \<And>x3. I x = Regions.intv.Greater x3 \<Longrightarrow> Regions.intv_elem x (u \<oplus> t) (I x)
[PROOF STEP]
case Const
[PROOF STATE]
proof (state)
this:
I x = Regions.intv.Const x1_

goal (3 subgoals):
 1. \<And>x1. I x = Regions.intv.Const x1 \<Longrightarrow> Regions.intv_elem x (u \<oplus> t) (I x)
 2. \<And>x2. I x = Regions.intv.Intv x2 \<Longrightarrow> Regions.intv_elem x (u \<oplus> t) (I x)
 3. \<And>x3. I x = Regions.intv.Greater x3 \<Longrightarrow> Regions.intv_elem x (u \<oplus> t) (I x)
[PROOF STEP]
with assms \<open>x \<in> \<X>\<close>
[PROOF STATE]
proof (chain)
picking this:
R \<equiv> Regions.region \<X> I r
u \<in> R
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> t) c < real (intv_const (I c) + 1)
0 \<le> t
x \<in> \<X>
I x = Regions.intv.Const x1_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R \<equiv> Regions.region \<X> I r
u \<in> R
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> t) c < real (intv_const (I c) + 1)
0 \<le> t
x \<in> \<X>
I x = Regions.intv.Const x1_

goal (1 subgoal):
 1. Regions.intv_elem x (u \<oplus> t) (I x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Regions.intv_elem x (u \<oplus> t) (I x)

goal (2 subgoals):
 1. \<And>x2. I x = Regions.intv.Intv x2 \<Longrightarrow> Regions.intv_elem x (u \<oplus> t) (I x)
 2. \<And>x3. I x = Regions.intv.Greater x3 \<Longrightarrow> Regions.intv_elem x (u \<oplus> t) (I x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x2. I x = Regions.intv.Intv x2 \<Longrightarrow> Regions.intv_elem x (u \<oplus> t) (I x)
 2. \<And>x3. I x = Regions.intv.Greater x3 \<Longrightarrow> Regions.intv_elem x (u \<oplus> t) (I x)
[PROOF STEP]
case (Intv c)
[PROOF STATE]
proof (state)
this:
I x = Regions.intv.Intv c

goal (2 subgoals):
 1. \<And>x2. I x = Regions.intv.Intv x2 \<Longrightarrow> Regions.intv_elem x (u \<oplus> t) (I x)
 2. \<And>x3. I x = Regions.intv.Greater x3 \<Longrightarrow> Regions.intv_elem x (u \<oplus> t) (I x)
[PROOF STEP]
with assms \<open>x \<in> \<X>\<close>
[PROOF STATE]
proof (chain)
picking this:
R \<equiv> Regions.region \<X> I r
u \<in> R
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> t) c < real (intv_const (I c) + 1)
0 \<le> t
x \<in> \<X>
I x = Regions.intv.Intv c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R \<equiv> Regions.region \<X> I r
u \<in> R
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> t) c < real (intv_const (I c) + 1)
0 \<le> t
x \<in> \<X>
I x = Regions.intv.Intv c

goal (1 subgoal):
 1. Regions.intv_elem x (u \<oplus> t) (I x)
[PROOF STEP]
by (simp add: cval_add_def) (rule; force)
[PROOF STATE]
proof (state)
this:
Regions.intv_elem x (u \<oplus> t) (I x)

goal (1 subgoal):
 1. \<And>x3. I x = Regions.intv.Greater x3 \<Longrightarrow> Regions.intv_elem x (u \<oplus> t) (I x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x3. I x = Regions.intv.Greater x3 \<Longrightarrow> Regions.intv_elem x (u \<oplus> t) (I x)
[PROOF STEP]
case (Greater c)
[PROOF STATE]
proof (state)
this:
I x = Regions.intv.Greater c

goal (1 subgoal):
 1. \<And>x3. I x = Regions.intv.Greater x3 \<Longrightarrow> Regions.intv_elem x (u \<oplus> t) (I x)
[PROOF STEP]
with assms \<open>x \<in> \<X>\<close>
[PROOF STATE]
proof (chain)
picking this:
R \<equiv> Regions.region \<X> I r
u \<in> R
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> t) c < real (intv_const (I c) + 1)
0 \<le> t
x \<in> \<X>
I x = Regions.intv.Greater c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R \<equiv> Regions.region \<X> I r
u \<in> R
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> t) c < real (intv_const (I c) + 1)
0 \<le> t
x \<in> \<X>
I x = Regions.intv.Greater c

goal (1 subgoal):
 1. Regions.intv_elem x (u \<oplus> t) (I x)
[PROOF STEP]
by (fastforce simp add: cval_add_def)
[PROOF STATE]
proof (state)
this:
Regions.intv_elem x (u \<oplus> t) (I x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x5 \<in> \<X> \<Longrightarrow> Regions.intv_elem ?x5 (u \<oplus> t) (I ?x5)

goal (3 subgoals):
 1. \<forall>x\<in>\<X>. Regions.intv_elem x (u \<oplus> t) (I x)
 2. ?X\<^sub>0 = {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}
 3. \<forall>x\<in>?X\<^sub>0. \<forall>y\<in>?X\<^sub>0. ((x, y) \<in> r) = (frac ((u \<oplus> t) x) \<le> frac ((u \<oplus> t) y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x5 \<in> \<X> \<Longrightarrow> Regions.intv_elem ?x5 (u \<oplus> t) (I ?x5)
[PROOF STEP]
show "\<forall>x\<in>\<X>. intv_elem x (u \<oplus> t) (I x)"
[PROOF STATE]
proof (prove)
using this:
?x5 \<in> \<X> \<Longrightarrow> Regions.intv_elem ?x5 (u \<oplus> t) (I ?x5)

goal (1 subgoal):
 1. \<forall>x\<in>\<X>. Regions.intv_elem x (u \<oplus> t) (I x)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>\<X>. Regions.intv_elem x (u \<oplus> t) (I x)

goal (2 subgoals):
 1. ?X\<^sub>0 = {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}
 2. \<forall>x\<in>?X\<^sub>0. \<forall>y\<in>?X\<^sub>0. ((x, y) \<in> r) = (frac ((u \<oplus> t) x) \<le> frac ((u \<oplus> t) y))
[PROOF STEP]
let ?X\<^sub>0 = "{x \<in> \<X>. \<exists>d. I x = Intv d}"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?X\<^sub>0 = {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}
 2. \<forall>x\<in>?X\<^sub>0. \<forall>y\<in>?X\<^sub>0. ((x, y) \<in> r) = (frac ((u \<oplus> t) x) \<le> frac ((u \<oplus> t) y))
[PROOF STEP]
show "?X\<^sub>0 = ?X\<^sub>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d} = {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d} = {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}

goal (1 subgoal):
 1. \<forall>x\<in>{x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}. \<forall>y\<in>{x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}. ((x, y) \<in> r) = (frac ((u \<oplus> t) x) \<le> frac ((u \<oplus> t) y))
[PROOF STEP]
have "frac (u x + t) = frac (u x) + t" if "x \<in> ?X\<^sub>0" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frac (u x + t) = frac (u x) + t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. frac (u x + t) = frac (u x) + t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. frac (u x + t) = frac (u x) + t
[PROOF STEP]
apply (rule delayedR_correct_aux_aux[where c = "intv_const (I x)"])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. real (intv_const (I x)) < u x
 2. u x < real (Suc (intv_const (I x)))
 3. 0 \<le> t
 4. u x + t < real (Suc (intv_const (I x)))
[PROOF STEP]
using assms \<open>x \<in> ?X\<^sub>0\<close>
[PROOF STATE]
proof (prove)
using this:
R \<equiv> Regions.region \<X> I r
u \<in> R
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> t) c < real (intv_const (I c) + 1)
0 \<le> t
x \<in> {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}

goal (4 subgoals):
 1. real (intv_const (I x)) < u x
 2. u x < real (Suc (intv_const (I x)))
 3. 0 \<le> t
 4. u x + t < real (Suc (intv_const (I x)))
[PROOF STEP]
by (force simp add: cval_add_def)+
[PROOF STATE]
proof (state)
this:
frac (u x + t) = frac (u x) + t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x5 \<in> {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d} \<Longrightarrow> frac (u ?x5 + t) = frac (u ?x5) + t

goal (1 subgoal):
 1. \<forall>x\<in>{x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}. \<forall>y\<in>{x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}. ((x, y) \<in> r) = (frac ((u \<oplus> t) x) \<le> frac ((u \<oplus> t) y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x5 \<in> {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d} \<Longrightarrow> frac (u ?x5 + t) = frac (u ?x5) + t
[PROOF STEP]
have "frac (u x) \<le> frac (u y) \<longleftrightarrow> frac (u x + t) \<le> frac (u y + t)" if "x \<in> ?X\<^sub>0" "y \<in> ?X\<^sub>0" for x y
[PROOF STATE]
proof (prove)
using this:
?x5 \<in> {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d} \<Longrightarrow> frac (u ?x5 + t) = frac (u ?x5) + t

goal (1 subgoal):
 1. (frac (u x) \<le> frac (u y)) = (frac (u x + t) \<le> frac (u y + t))
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?x5 \<in> {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d} \<Longrightarrow> frac (u ?x5 + t) = frac (u ?x5) + t
x \<in> {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}
y \<in> {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}

goal (1 subgoal):
 1. (frac (u x) \<le> frac (u y)) = (frac (u x + t) \<le> frac (u y + t))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x5 \<in> {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}; ?y5 \<in> {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}\<rbrakk> \<Longrightarrow> (frac (u ?x5) \<le> frac (u ?y5)) = (frac (u ?x5 + t) \<le> frac (u ?y5 + t))

goal (1 subgoal):
 1. \<forall>x\<in>{x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}. \<forall>y\<in>{x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}. ((x, y) \<in> r) = (frac ((u \<oplus> t) x) \<le> frac ((u \<oplus> t) y))
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
R \<equiv> Regions.region \<X> I r
u \<in> R
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> t) c < real (intv_const (I c) + 1)
0 \<le> t
\<lbrakk>?x5 \<in> {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}; ?y5 \<in> {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}\<rbrakk> \<Longrightarrow> (frac (u ?x5) \<le> frac (u ?y5)) = (frac (u ?x5 + t) \<le> frac (u ?y5 + t))
[PROOF STEP]
show
    "\<forall>x\<in>?X\<^sub>0. \<forall>y\<in>?X\<^sub>0. ((x, y) \<in> r) = (frac ((u \<oplus> t) x) \<le> frac ((u \<oplus> t) y))"
[PROOF STATE]
proof (prove)
using this:
R \<equiv> Regions.region \<X> I r
u \<in> R
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> t) c < real (intv_const (I c) + 1)
0 \<le> t
\<lbrakk>?x5 \<in> {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}; ?y5 \<in> {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}\<rbrakk> \<Longrightarrow> (frac (u ?x5) \<le> frac (u ?y5)) = (frac (u ?x5 + t) \<le> frac (u ?y5 + t))

goal (1 subgoal):
 1. \<forall>x\<in>{x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}. \<forall>y\<in>{x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}. ((x, y) \<in> r) = (frac ((u \<oplus> t) x) \<le> frac ((u \<oplus> t) y))
[PROOF STEP]
unfolding cval_add_def
[PROOF STATE]
proof (prove)
using this:
R \<equiv> Regions.region \<X> I r
u \<in> R
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> u c + t < real (intv_const (I c) + 1)
0 \<le> t
\<lbrakk>?x5 \<in> {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}; ?y5 \<in> {x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}\<rbrakk> \<Longrightarrow> (frac (u ?x5) \<le> frac (u ?y5)) = (frac (u ?x5 + t) \<le> frac (u ?y5 + t))

goal (1 subgoal):
 1. \<forall>x\<in>{x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}. \<forall>y\<in>{x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}. ((x, y) \<in> r) = (frac (u x + t) \<le> frac (u y + t))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>{x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}. \<forall>y\<in>{x \<in> \<X>. \<exists>d. I x = Regions.intv.Intv d}. ((x, y) \<in> r) = (frac ((u \<oplus> t) x) \<le> frac ((u \<oplus> t) y))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma delayedR_correct_aux':
  fixes I r
  defines "R \<equiv> region \<X> I r"
  assumes "u \<oplus> t1 \<in> R" "valid_region \<X> k I r" "\<forall> c \<in> \<X>. \<not> isConst (I c)"
          "\<forall> c \<in> \<X>. isIntv (I c) \<longrightarrow> (u \<oplus> t2) c < intv_const (I c) + 1"
          "t1 \<le> t2"
  shows "u \<oplus> t2 \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<oplus> t2 \<in> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<oplus> t2 \<in> R
[PROOF STEP]
have "(u \<oplus> t1) \<oplus> (t2 - t1) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u \<oplus> t1) \<oplus> t2 - t1 \<in> R
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u \<oplus> t1) \<oplus> t2 - t1 \<in> Regions.region \<X> I r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
R \<equiv> Regions.region \<X> I r
u \<oplus> t1 \<in> R
Regions.valid_region \<X> k I r
\<forall>c\<in>\<X>. \<not> Regions.isConst (I c)
\<forall>c\<in>\<X>. Regions.isIntv (I c) \<longrightarrow> (u \<oplus> t2) c < real (intv_const (I c) + 1)
t1 \<le> t2

goal (1 subgoal):
 1. (u \<oplus> t1) \<oplus> t2 - t1 \<in> Regions.region \<X> I r
[PROOF STEP]
by - (rule delayedR_correct_aux, auto simp: cval_add_def)
[PROOF STATE]
proof (state)
this:
(u \<oplus> t1) \<oplus> t2 - t1 \<in> R

goal (1 subgoal):
 1. u \<oplus> t2 \<in> R
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(u \<oplus> t1) \<oplus> t2 - t1 \<in> R
[PROOF STEP]
show "u \<oplus> t2 \<in> R"
[PROOF STATE]
proof (prove)
using this:
(u \<oplus> t1) \<oplus> t2 - t1 \<in> R

goal (1 subgoal):
 1. u \<oplus> t2 \<in> R
[PROOF STEP]
by (simp add: cval_add_def)
[PROOF STATE]
proof (state)
this:
u \<oplus> t2 \<in> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma valid_regions_intv_distinct:
  "valid_region X k I r \<Longrightarrow> valid_region X k I' r' \<Longrightarrow> u \<in> region X I r \<Longrightarrow> u \<in> region X I' r'
  \<Longrightarrow> x \<in> X \<Longrightarrow> I x = I' x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Regions.valid_region X k I r; Regions.valid_region X k I' r'; u \<in> Regions.region X I r; u \<in> Regions.region X I' r'; x \<in> X\<rbrakk> \<Longrightarrow> I x = I' x
[PROOF STEP]
proof goal_cases
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Regions.valid_region X k I r; Regions.valid_region X k I' r'; u \<in> Regions.region X I r; u \<in> Regions.region X I' r'; x \<in> X\<rbrakk> \<Longrightarrow> I x = I' x
[PROOF STEP]
case A: 1
[PROOF STATE]
proof (state)
this:
Regions.valid_region X k I r
Regions.valid_region X k I' r'
u \<in> Regions.region X I r
u \<in> Regions.region X I' r'
x \<in> X

goal (1 subgoal):
 1. \<lbrakk>Regions.valid_region X k I r; Regions.valid_region X k I' r'; u \<in> Regions.region X I r; u \<in> Regions.region X I' r'; x \<in> X\<rbrakk> \<Longrightarrow> I x = I' x
[PROOF STEP]
note x = \<open>x \<in> X\<close>
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (1 subgoal):
 1. \<lbrakk>Regions.valid_region X k I r; Regions.valid_region X k I' r'; u \<in> Regions.region X I r; u \<in> Regions.region X I' r'; x \<in> X\<rbrakk> \<Longrightarrow> I x = I' x
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
Regions.valid_region X k I r
Regions.valid_region X k I' r'
u \<in> Regions.region X I r
u \<in> Regions.region X I' r'
x \<in> X
x \<in> X
[PROOF STEP]
have "valid_intv (k x) (I x)"
[PROOF STATE]
proof (prove)
using this:
Regions.valid_region X k I r
Regions.valid_region X k I' r'
u \<in> Regions.region X I r
u \<in> Regions.region X I' r'
x \<in> X
x \<in> X

goal (1 subgoal):
 1. Regions.valid_intv (k x) (I x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Regions.valid_intv (k x) (I x)

goal (1 subgoal):
 1. \<lbrakk>Regions.valid_region X k I r; Regions.valid_region X k I' r'; u \<in> Regions.region X I r; u \<in> Regions.region X I' r'; x \<in> X\<rbrakk> \<Longrightarrow> I x = I' x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Regions.valid_intv (k x) (I x)

goal (1 subgoal):
 1. \<lbrakk>Regions.valid_region X k I r; Regions.valid_region X k I' r'; u \<in> Regions.region X I r; u \<in> Regions.region X I' r'; x \<in> X\<rbrakk> \<Longrightarrow> I x = I' x
[PROOF STEP]
from A(2) x
[PROOF STATE]
proof (chain)
picking this:
Regions.valid_region X k I' r'
x \<in> X
[PROOF STEP]
have "valid_intv (k x) (I' x)"
[PROOF STATE]
proof (prove)
using this:
Regions.valid_region X k I' r'
x \<in> X

goal (1 subgoal):
 1. Regions.valid_intv (k x) (I' x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Regions.valid_intv (k x) (I' x)

goal (1 subgoal):
 1. \<lbrakk>Regions.valid_region X k I r; Regions.valid_region X k I' r'; u \<in> Regions.region X I r; u \<in> Regions.region X I' r'; x \<in> X\<rbrakk> \<Longrightarrow> I x = I' x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Regions.valid_intv (k x) (I' x)

goal (1 subgoal):
 1. \<lbrakk>Regions.valid_region X k I r; Regions.valid_region X k I' r'; u \<in> Regions.region X I r; u \<in> Regions.region X I' r'; x \<in> X\<rbrakk> \<Longrightarrow> I x = I' x
[PROOF STEP]
from A(3) x
[PROOF STATE]
proof (chain)
picking this:
u \<in> Regions.region X I r
x \<in> X
[PROOF STEP]
have "intv_elem x u (I x)"
[PROOF STATE]
proof (prove)
using this:
u \<in> Regions.region X I r
x \<in> X

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

goal (1 subgoal):
 1. \<lbrakk>Regions.valid_region X k I r; Regions.valid_region X k I' r'; u \<in> Regions.region X I r; u \<in> Regions.region X I' r'; x \<in> X\<rbrakk> \<Longrightarrow> I x = I' x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Regions.intv_elem x u (I x)

goal (1 subgoal):
 1. \<lbrakk>Regions.valid_region X k I r; Regions.valid_region X k I' r'; u \<in> Regions.region X I r; u \<in> Regions.region X I' r'; x \<in> X\<rbrakk> \<Longrightarrow> I x = I' x
[PROOF STEP]
from A(4) x
[PROOF STATE]
proof (chain)
picking this:
u \<in> Regions.region X I' r'
x \<in> X
[PROOF STEP]
have "intv_elem x u (I' x)"
[PROOF STATE]
proof (prove)
using this:
u \<in> Regions.region X I' r'
x \<in> X

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

goal (1 subgoal):
 1. \<lbrakk>Regions.valid_region X k I r; Regions.valid_region X k I' r'; u \<in> Regions.region X I r; u \<in> Regions.region X I' r'; x \<in> X\<rbrakk> \<Longrightarrow> I x = I' x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Regions.valid_intv (k x) (I x)
Regions.valid_intv (k x) (I' x)
Regions.intv_elem x u (I x)
Regions.intv_elem x u (I' x)
[PROOF STEP]
show "I x = I' x"
[PROOF STATE]
proof (prove)
using this:
Regions.valid_intv (k x) (I x)
Regions.valid_intv (k x) (I' x)
Regions.intv_elem x u (I x)
Regions.intv_elem x u (I' x)

goal (1 subgoal):
 1. I x = I' x
[PROOF STEP]
using valid_intv_distinct
[PROOF STATE]
proof (prove)
using this:
Regions.valid_intv (k x) (I x)
Regions.valid_intv (k x) (I' x)
Regions.intv_elem x u (I x)
Regions.intv_elem x u (I' x)
\<lbrakk>Regions.valid_intv ?c ?I; Regions.valid_intv ?c ?I'; Regions.intv_elem ?x ?u ?I; Regions.intv_elem ?x ?u ?I'\<rbrakk> \<Longrightarrow> ?I = ?I'

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

goal:
No subgoals!
[PROOF STEP]
qed