[STATEMENT]
lemma region_continuous:
  assumes "valid_region X k I r"
  defines R: "R \<equiv> region X I r"
  assumes between: "0 \<le> t1" "t1 \<le> t2"
  assumes elem: "u \<in> R" "u \<oplus> t2 \<in> R"
  shows "u \<oplus> t1 \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<oplus> t1 \<in> R
[PROOF STEP]
unfolding R
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<oplus> t1 \<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> t1) x
 2. \<forall>x\<in>X. Regions.intv_elem x (u \<oplus> t1) (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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
from \<open>0 \<le> t1\<close> \<open>u \<in> R\<close>
[PROOF STATE]
proof (chain)
picking this:
0 \<le> t1
u \<in> R
[PROOF STEP]
show "\<forall>x\<in>X. 0 \<le> (u \<oplus> t1) x"
[PROOF STATE]
proof (prove)
using this:
0 \<le> t1
u \<in> R

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

goal (3 subgoals):
 1. \<forall>x\<in>X. Regions.intv_elem x (u \<oplus> t1) (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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
have "intv_elem x (u \<oplus> t1) (I x)" if "x \<in> X" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Regions.intv_elem x (u \<oplus> t1) (I x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Regions.intv_elem x (u \<oplus> t1) (I x)
[PROOF STEP]
from elem that
[PROOF STATE]
proof (chain)
picking this:
u \<in> R
u \<oplus> t2 \<in> R
x \<in> X
[PROOF STEP]
have "intv_elem x u (I x)" "intv_elem x (u \<oplus> t2) (I x)"
[PROOF STATE]
proof (prove)
using this:
u \<in> R
u \<oplus> t2 \<in> R
x \<in> X

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

goal (1 subgoal):
 1. Regions.intv_elem x (u \<oplus> t1) (I x)
[PROOF STEP]
with between
[PROOF STATE]
proof (chain)
picking this:
0 \<le> t1
t1 \<le> t2
Regions.intv_elem x u (I x)
Regions.intv_elem x (u \<oplus> t2) (I x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 \<le> t1
t1 \<le> t2
Regions.intv_elem x u (I x)
Regions.intv_elem x (u \<oplus> t2) (I x)

goal (1 subgoal):
 1. Regions.intv_elem x (u \<oplus> t1) (I x)
[PROOF STEP]
by (cases "I x", auto simp: cval_add_def)
[PROOF STATE]
proof (state)
this:
Regions.intv_elem x (u \<oplus> t1) (I x)

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

goal (3 subgoals):
 1. \<forall>x\<in>X. Regions.intv_elem x (u \<oplus> t1) (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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x \<in> X \<Longrightarrow> Regions.intv_elem ?x (u \<oplus> t1) (I ?x)
[PROOF STEP]
show "\<forall> x \<in> X. intv_elem x (u \<oplus> t1) (I x)"
[PROOF STATE]
proof (prove)
using this:
?x \<in> X \<Longrightarrow> Regions.intv_elem ?x (u \<oplus> t1) (I ?x)

goal (1 subgoal):
 1. \<forall>x\<in>X. Regions.intv_elem x (u \<oplus> t1) (I x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>X. Regions.intv_elem x (u \<oplus> t1) (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> t1) x) \<le> frac ((u \<oplus> t1) 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> t1) x) \<le> frac ((u \<oplus> t1) 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]
..
[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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
from elem
[PROOF STATE]
proof (chain)
picking this:
u \<in> R
u \<oplus> t2 \<in> R
[PROOF STEP]
have "\<forall> x \<in> ?X\<^sub>0. \<forall> y \<in> ?X\<^sub>0. (x, y) \<in> r \<longleftrightarrow> frac (u x) \<le> frac (u y)"
[PROOF STATE]
proof (prove)
using this:
u \<in> R
u \<oplus> t2 \<in> R

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) \<le> frac (u y))
[PROOF STEP]
by (auto simp: R)
[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 x) \<le> frac (u y))

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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
moreover
[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 x) \<le> frac (u y))

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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
{
[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 x) \<le> frac (u y))

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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
fix x y c d
[PROOF STATE]
proof (state)
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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
assume A: "x \<in> X" "y \<in> X" "I x = Intv c" "I y = Intv d"
[PROOF STATE]
proof (state)
this:
x \<in> X
y \<in> X
I x = Regions.intv.Intv c
I y = 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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
from A elem between
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
y \<in> X
I x = Regions.intv.Intv c
I y = Regions.intv.Intv d
u \<in> R
u \<oplus> t2 \<in> R
0 \<le> t1
t1 \<le> t2
[PROOF STEP]
have *:
      "c < u x" "u x < c + 1" "c < u x + t1" "u x + t1 < c + 1"
[PROOF STATE]
proof (prove)
using this:
x \<in> X
y \<in> X
I x = Regions.intv.Intv c
I y = Regions.intv.Intv d
u \<in> R
u \<oplus> t2 \<in> R
0 \<le> t1
t1 \<le> t2

goal (1 subgoal):
 1. (real c < u x &&& u x < real (c + 1)) &&& real c < u x + t1 &&& u x + t1 < real (c + 1)
[PROOF STEP]
by (fastforce simp: cval_add_def R)+
[PROOF STATE]
proof (state)
this:
real c < u x
u x < real (c + 1)
real c < u x + t1
u x + t1 < real (c + 1)

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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
real c < u x
u x < real (c + 1)
real c < u x + t1
u x + t1 < real (c + 1)

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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
from A(2,4) elem between
[PROOF STATE]
proof (chain)
picking this:
y \<in> X
I y = Regions.intv.Intv d
u \<in> R
u \<oplus> t2 \<in> R
0 \<le> t1
t1 \<le> t2
[PROOF STEP]
have **:
      "d < u y" "u y < d + 1" "d < u y + t1" "u y + t1 < d + 1"
[PROOF STATE]
proof (prove)
using this:
y \<in> X
I y = Regions.intv.Intv d
u \<in> R
u \<oplus> t2 \<in> R
0 \<le> t1
t1 \<le> t2

goal (1 subgoal):
 1. (real d < u y &&& u y < real (d + 1)) &&& real d < u y + t1 &&& u y + t1 < real (d + 1)
[PROOF STEP]
by (fastforce simp: cval_add_def R)+
[PROOF STATE]
proof (state)
this:
real d < u y
u y < real (d + 1)
real d < u y + t1
u y + t1 < real (d + 1)

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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
real c < u x
u x < real (c + 1)
real c < u x + t1
u x + t1 < real (c + 1)
real d < u y
u y < real (d + 1)
real d < u y + t1
u y + t1 < real (d + 1)
[PROOF STEP]
have "u x = c + frac (u x)" "u y = d + frac (u y)"
[PROOF STATE]
proof (prove)
using this:
real c < u x
u x < real (c + 1)
real c < u x + t1
u x + t1 < real (c + 1)
real d < u y
u y < real (d + 1)
real d < u y + t1
u y + t1 < real (d + 1)

goal (1 subgoal):
 1. u x = real c + frac (u x) &&& u y = real d + frac (u y)
[PROOF STEP]
using nat_intv_frac_decomp
[PROOF STATE]
proof (prove)
using this:
real c < u x
u x < real (c + 1)
real c < u x + t1
u x + t1 < real (c + 1)
real d < u y
u y < real (d + 1)
real d < u y + t1
u y + t1 < real (d + 1)
\<lbrakk>real ?c < ?d; ?d < real (?c + 1)\<rbrakk> \<Longrightarrow> ?d = real ?c + frac ?d

goal (1 subgoal):
 1. u x = real c + frac (u x) &&& u y = real d + frac (u y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u x = real c + frac (u x)
u y = real d + frac (u y)

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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u x = real c + frac (u x)
u y = real d + frac (u y)
[PROOF STEP]
have
      "frac (u x + t1) = frac (u x) + t1" "frac (u y + t1) = frac (u y) + t1"
[PROOF STATE]
proof (prove)
using this:
u x = real c + frac (u x)
u y = real d + frac (u y)

goal (1 subgoal):
 1. frac (u x + t1) = frac (u x) + t1 &&& frac (u y + t1) = frac (u y) + t1
[PROOF STEP]
using *(3,4) **(3,4) nat_intv_frac_decomp
[PROOF STATE]
proof (prove)
using this:
u x = real c + frac (u x)
u y = real d + frac (u y)
real c < u x + t1
u x + t1 < real (c + 1)
real d < u y + t1
u y + t1 < real (d + 1)
\<lbrakk>real ?c < ?d; ?d < real (?c + 1)\<rbrakk> \<Longrightarrow> ?d = real ?c + frac ?d

goal (1 subgoal):
 1. frac (u x + t1) = frac (u x) + t1 &&& frac (u y + t1) = frac (u y) + t1
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
frac (u x + t1) = frac (u x) + t1
frac (u y + t1) = frac (u y) + t1

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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
frac (u x + t1) = frac (u x) + t1
frac (u y + t1) = frac (u y) + t1
[PROOF STEP]
have
      "frac (u x) \<le> frac (u y) \<longleftrightarrow> frac ((u \<oplus> t1) x) \<le> frac ((u \<oplus> t1) y)"
[PROOF STATE]
proof (prove)
using this:
frac (u x + t1) = frac (u x) + t1
frac (u y + t1) = frac (u y) + t1

goal (1 subgoal):
 1. (frac (u x) \<le> frac (u y)) = (frac ((u \<oplus> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
by (auto simp: cval_add_def)
[PROOF STATE]
proof (state)
this:
(frac (u x) \<le> frac (u y)) = (frac ((u \<oplus> t1) x) \<le> frac ((u \<oplus> t1) y))

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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2 \<in> X; ?y2 \<in> X; I ?x2 = Regions.intv.Intv ?c2; I ?y2 = Regions.intv.Intv ?d2\<rbrakk> \<Longrightarrow> (frac (u ?x2) \<le> frac (u ?y2)) = (frac ((u \<oplus> t1) ?x2) \<le> frac ((u \<oplus> t1) ?y2))

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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking 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 x) \<le> frac (u y))
\<lbrakk>?x2 \<in> X; ?y2 \<in> X; I ?x2 = Regions.intv.Intv ?c2; I ?y2 = Regions.intv.Intv ?d2\<rbrakk> \<Longrightarrow> (frac (u ?x2) \<le> frac (u ?y2)) = (frac ((u \<oplus> t1) ?x2) \<le> frac ((u \<oplus> t1) ?y2))
[PROOF STEP]
show
    "\<forall> x \<in> ?X\<^sub>0. \<forall> y \<in> ?X\<^sub>0. (x, y) \<in> r \<longleftrightarrow> frac ((u \<oplus> t1) x) \<le> frac ((u \<oplus> t1) y)"
[PROOF STATE]
proof (prove)
using 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 x) \<le> frac (u y))
\<lbrakk>?x2 \<in> X; ?y2 \<in> X; I ?x2 = Regions.intv.Intv ?c2; I ?y2 = Regions.intv.Intv ?d2\<rbrakk> \<Longrightarrow> (frac (u ?x2) \<le> frac (u ?y2)) = (frac ((u \<oplus> t1) ?x2) \<le> frac ((u \<oplus> t1) ?y2))

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> t1) x) \<le> frac ((u \<oplus> t1) y))
[PROOF STEP]
by (auto simp: cval_add_def)
[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> t1) x) \<le> frac ((u \<oplus> t1) y))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma upper_right_eq:
  assumes "finite X" "valid_region X k I r"
  shows "(\<forall> x \<in> X. isGreater (I x)) \<longleftrightarrow> is_upper_right (region X I r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>X. Regions.isGreater (I x)) = (\<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite X
Regions.valid_region X k I r

goal (1 subgoal):
 1. (\<forall>x\<in>X. Regions.isGreater (I x)) = (\<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r)
[PROOF STEP]
proof (safe, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t u. \<lbrakk>finite X; Regions.valid_region X k I r; \<forall>x\<in>X. Regions.isGreater (I x); 0 \<le> t; u \<in> Regions.region X I r\<rbrakk> \<Longrightarrow> u \<oplus> t \<in> Regions.region X I r
 2. \<And>x. \<lbrakk>finite X; Regions.valid_region X k I r; \<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r; x \<in> X\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
[PROOF STEP]
case (1 t u)
[PROOF STATE]
proof (state)
this:
finite X
Regions.valid_region X k I r
\<forall>x\<in>X. Regions.isGreater (I x)
0 \<le> t
u \<in> Regions.region X I r

goal (2 subgoals):
 1. \<And>t u. \<lbrakk>finite X; Regions.valid_region X k I r; \<forall>x\<in>X. Regions.isGreater (I x); 0 \<le> t; u \<in> Regions.region X I r\<rbrakk> \<Longrightarrow> u \<oplus> t \<in> Regions.region X I r
 2. \<And>x. \<lbrakk>finite X; Regions.valid_region X k I r; \<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r; x \<in> X\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite X
Regions.valid_region X k I r
\<forall>x\<in>X. Regions.isGreater (I x)
0 \<le> t
u \<in> Regions.region X I r
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite X
Regions.valid_region X k I r
\<forall>x\<in>X. Regions.isGreater (I x)
0 \<le> t
u \<in> Regions.region X I r

goal (1 subgoal):
 1. u \<oplus> t \<in> Regions.region X I r
[PROOF STEP]
by - (standard, force simp: cval_add_def)+
[PROOF STATE]
proof (state)
this:
u \<oplus> t \<in> Regions.region X I r

goal (1 subgoal):
 1. \<And>x. \<lbrakk>finite X; Regions.valid_region X k I r; \<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r; x \<in> X\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>finite X; Regions.valid_region X k I r; \<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r; x \<in> X\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
[PROOF STEP]
case (2 x)
[PROOF STATE]
proof (state)
this:
finite X
Regions.valid_region X k I r
\<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r
x \<in> X

goal (1 subgoal):
 1. \<And>x. \<lbrakk>finite X; Regions.valid_region X k I r; \<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r; x \<in> X\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
[PROOF STEP]
(* XXX Does this lemma actually need the finiteness assumption? *)
[PROOF STATE]
proof (state)
this:
finite X
Regions.valid_region X k I r
\<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r
x \<in> X

goal (1 subgoal):
 1. \<And>x. \<lbrakk>finite X; Regions.valid_region X k I r; \<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r; x \<in> X\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
[PROOF STEP]
from region_not_empty[OF assms]
[PROOF STATE]
proof (chain)
picking this:
\<exists>u. u \<in> Regions.region X I r
[PROOF STEP]
obtain u where u: "u \<in> region X I r"
[PROOF STATE]
proof (prove)
using this:
\<exists>u. u \<in> Regions.region X I r

goal (1 subgoal):
 1. (\<And>u. u \<in> Regions.region X I r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
u \<in> Regions.region X I r

goal (1 subgoal):
 1. \<And>x. \<lbrakk>finite X; Regions.valid_region X k I r; \<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r; x \<in> X\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u \<in> Regions.region X I r

goal (1 subgoal):
 1. \<And>x. \<lbrakk>finite X; Regions.valid_region X k I r; \<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r; x \<in> X\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
[PROOF STEP]
have "(1 :: real) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> 1

goal (1 subgoal):
 1. \<And>x. \<lbrakk>finite X; Regions.valid_region X k I r; \<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r; x \<in> X\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u \<in> Regions.region X I r
0 \<le> 1
[PROOF STEP]
have "(u \<oplus> 1) \<in> region X I r"
[PROOF STATE]
proof (prove)
using this:
u \<in> Regions.region X I r
0 \<le> 1

goal (1 subgoal):
 1. u \<oplus> 1 \<in> Regions.region X I r
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
u \<in> Regions.region X I r
0 \<le> 1
finite X
Regions.valid_region X k I r
\<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r
x \<in> X

goal (1 subgoal):
 1. u \<oplus> 1 \<in> Regions.region X I r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u \<oplus> 1 \<in> Regions.region X I r

goal (1 subgoal):
 1. \<And>x. \<lbrakk>finite X; Regions.valid_region X k I r; \<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r; x \<in> X\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
[PROOF STEP]
with \<open>x \<in> X\<close> u
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
u \<in> Regions.region X I r
u \<oplus> 1 \<in> Regions.region X I r
[PROOF STEP]
have "intv_elem x u (I x)" "intv_elem x (u \<oplus> 1) (I x)"
[PROOF STATE]
proof (prove)
using this:
x \<in> X
u \<in> Regions.region X I r
u \<oplus> 1 \<in> Regions.region X I r

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

goal (1 subgoal):
 1. \<And>x. \<lbrakk>finite X; Regions.valid_region X k I r; \<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r; x \<in> X\<rbrakk> \<Longrightarrow> Regions.isGreater (I x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Regions.intv_elem x u (I x)
Regions.intv_elem x (u \<oplus> 1) (I x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Regions.intv_elem x u (I x)
Regions.intv_elem x (u \<oplus> 1) (I x)

goal (1 subgoal):
 1. Regions.isGreater (I x)
[PROOF STEP]
by (cases "I x", auto simp: cval_add_def)
[PROOF STATE]
proof (state)
this:
Regions.isGreater (I x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bounded_region:
  assumes "finite X" "valid_region X k I r"
  defines R: "R \<equiv> region X I r"
  assumes "\<not> is_upper_right R" "u \<in> R"
  shows "u \<oplus> 1 \<notin> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<oplus> 1 \<notin> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<oplus> 1 \<notin> R
[PROOF STEP]
from upper_right_eq[OF assms(1,2)] assms(4)
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x\<in>X. Regions.isGreater (I x)) = (\<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r)
\<not> (\<forall>t\<ge>0. \<forall>u\<in>R. u \<oplus> t \<in> R)
[PROOF STEP]
obtain x where x:
    "x \<in> X" "\<not> isGreater (I x)"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x\<in>X. Regions.isGreater (I x)) = (\<forall>t\<ge>0. \<forall>u\<in>Regions.region X I r. u \<oplus> t \<in> Regions.region X I r)
\<not> (\<forall>t\<ge>0. \<forall>u\<in>R. u \<oplus> t \<in> R)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> X; \<not> Regions.isGreater (I x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: R)
[PROOF STATE]
proof (state)
this:
x \<in> X
\<not> Regions.isGreater (I x)

goal (1 subgoal):
 1. u \<oplus> 1 \<notin> R
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
finite X
Regions.valid_region X k I r
R \<equiv> Regions.region X I r
\<not> (\<forall>t\<ge>0. \<forall>u\<in>R. u \<oplus> t \<in> R)
u \<in> R
x \<in> X
\<not> Regions.isGreater (I x)
[PROOF STEP]
have "intv_elem x u (I x)"
[PROOF STATE]
proof (prove)
using this:
finite X
Regions.valid_region X k I r
R \<equiv> Regions.region X I r
\<not> (\<forall>t\<ge>0. \<forall>u\<in>R. u \<oplus> t \<in> R)
u \<in> R
x \<in> X
\<not> Regions.isGreater (I 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. u \<oplus> 1 \<notin> R
[PROOF STEP]
with x(2)
[PROOF STATE]
proof (chain)
picking this:
\<not> Regions.isGreater (I x)
Regions.intv_elem x u (I x)
[PROOF STEP]
have "\<not> intv_elem x (u \<oplus> 1) (I x)"
[PROOF STATE]
proof (prove)
using this:
\<not> Regions.isGreater (I x)
Regions.intv_elem x u (I x)

goal (1 subgoal):
 1. \<not> Regions.intv_elem x (u \<oplus> 1) (I x)
[PROOF STEP]
by (cases "I x", auto simp: cval_add_def)
[PROOF STATE]
proof (state)
this:
\<not> Regions.intv_elem x (u \<oplus> 1) (I x)

goal (1 subgoal):
 1. u \<oplus> 1 \<notin> R
[PROOF STEP]
with x(1) assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
finite X
Regions.valid_region X k I r
R \<equiv> Regions.region X I r
\<not> (\<forall>t\<ge>0. \<forall>u\<in>R. u \<oplus> t \<in> R)
u \<in> R
\<not> Regions.intv_elem x (u \<oplus> 1) (I x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> X
finite X
Regions.valid_region X k I r
R \<equiv> Regions.region X I r
\<not> (\<forall>t\<ge>0. \<forall>u\<in>R. u \<oplus> t \<in> R)
u \<in> R
\<not> Regions.intv_elem x (u \<oplus> 1) (I x)

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

goal:
No subgoals!
[PROOF STEP]
qed