[STATEMENT]
lemma stability:
  assumes "t j \<le> t1"
  defines incrs: "incrs \<equiv> \<lambda>h t x. incr h t x + s h t x"
  shows "dist
    (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)
    (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le>
        B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
have "t 0 \<le> t1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t 0 \<le> t1
[PROOF STEP]
by (metis assms(1) grid_ge_min order_trans)
[PROOF STATE]
proof (state)
this:
t 0 \<le> t1

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
have error: "norm (stepsize j *\<^sub>R s (stepsize j) (t j)
        (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j))
      \<le> B * stepsize j ^ (p + 1)"
    if "t (Suc j) \<le> t1" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (stepsize j *\<^sub>R s (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ (p + 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norm (stepsize j *\<^sub>R s (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ (p + 1)
[PROOF STEP]
from error[OF that]
[PROOF STATE]
proof (chain)
picking this:
norm (s (stepsize j) (t j) (grid_function (discrete_evolution (\<lambda>h t x. incr h t x + s h t x)) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ p
[PROOF STEP]
have "stepsize j * norm (s (stepsize j) (t j)
        (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j))
       \<le> stepsize j * (B * stepsize j ^ p)"
[PROOF STATE]
proof (prove)
using this:
norm (s (stepsize j) (t j) (grid_function (discrete_evolution (\<lambda>h t x. incr h t x + s h t x)) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ p

goal (1 subgoal):
 1. stepsize j * norm (s (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> stepsize j * (B * stepsize j ^ p)
[PROOF STEP]
using grid_stepsize_nonneg
[PROOF STATE]
proof (prove)
using this:
norm (s (stepsize j) (t j) (grid_function (discrete_evolution (\<lambda>h t x. incr h t x + s h t x)) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ p
0 \<le> stepsize ?j

goal (1 subgoal):
 1. stepsize j * norm (s (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> stepsize j * (B * stepsize j ^ p)
[PROOF STEP]
by (auto intro: mult_left_mono simp: incrs)
[PROOF STATE]
proof (state)
this:
stepsize j * norm (s (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> stepsize j * (B * stepsize j ^ p)

goal (1 subgoal):
 1. norm (stepsize j *\<^sub>R s (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ (p + 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
stepsize j * norm (s (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> stepsize j * (B * stepsize j ^ p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
stepsize j * norm (s (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> stepsize j * (B * stepsize j ^ p)

goal (1 subgoal):
 1. norm (stepsize j *\<^sub>R s (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ (p + 1)
[PROOF STEP]
using grid_stepsize_nonneg
[PROOF STATE]
proof (prove)
using this:
stepsize j * norm (s (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> stepsize j * (B * stepsize j ^ p)
0 \<le> stepsize ?j

goal (1 subgoal):
 1. norm (stepsize j *\<^sub>R s (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ (p + 1)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
norm (stepsize j *\<^sub>R s (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ (p + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t (Suc ?j) \<le> t1 \<Longrightarrow> norm (stepsize ?j *\<^sub>R s (stepsize ?j) (t ?j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t ?j)) \<le> B * stepsize ?j ^ (p + 1)

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
interpret c1: convergent_one_step "t 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. convergent_one_step (t 0) t1 x incr p B r L t
[PROOF STEP]
using max_step_r
[PROOF STATE]
proof (prove)
using this:
t ?j \<le> t1 \<Longrightarrow> max_stepsize ?j \<le> root p (\<bar>r\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))

goal (1 subgoal):
 1. convergent_one_step (t 0) t1 x incr p B r L t
[PROOF STEP]
by unfold_locales simp_all
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
have incr_in: "dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>"
    if "t (Suc j) \<le> t1" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>
[PROOF STEP]
from that
[PROOF STATE]
proof (chain)
picking this:
t (Suc j) \<le> t1
[PROOF STEP]
have "t j \<le> t1"
[PROOF STATE]
proof (prove)
using this:
t (Suc j) \<le> t1

goal (1 subgoal):
 1. t j \<le> t1
[PROOF STEP]
using grid_mono[of j "Suc j"]
[PROOF STATE]
proof (prove)
using this:
t (Suc j) \<le> t1
j \<le> Suc j \<Longrightarrow> t j \<le> t (Suc j)

goal (1 subgoal):
 1. t j \<le> t1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t j \<le> t1

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>
[PROOF STEP]
have "dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j)
      \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
using \<open>t j \<le> t1\<close>
[PROOF STATE]
proof (prove)
using this:
t j \<le> t1

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
by (rule c1.convergence)
[PROOF STATE]
proof (state)
this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>
[PROOF STEP]
have "... \<le> \<bar>r/2\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p \<le> \<bar>r / 2\<bar>
[PROOF STEP]
using max_stepsize_nonneg grid_interval_notempty max_step
      consistent_nonneg lipschitz_nonneg order_pos
      grid_mono \<open>t j \<le> t1\<close> t0_le
[PROOF STATE]
proof (prove)
using this:
0 \<le> max_stepsize ?n
t 0 \<le> t ?n
t ?j \<le> t1 \<Longrightarrow> max_stepsize ?j \<le> root p (\<bar>r / 2\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
0 \<le> B
0 \<le> L
0 < p
?j \<le> ?n \<Longrightarrow> t ?j \<le> t ?n
t j \<le> t1
t ?i \<le> t1 \<Longrightarrow> t 0 \<le> t1

goal (1 subgoal):
 1. B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p \<le> \<bar>r / 2\<bar>
[PROOF STEP]
apply (cases "L = 0", force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>n. 0 \<le> max_stepsize n; \<And>n. t 0 \<le> t n; \<And>j. t j \<le> t1 \<Longrightarrow> max_stepsize j \<le> root p (\<bar>r / 2\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1)); 0 \<le> B; 0 \<le> L; 0 < p; \<And>j n. j \<le> n \<Longrightarrow> t j \<le> t n; t j \<le> t1; \<And>i. t i \<le> t1 \<Longrightarrow> t 0 \<le> t1; L \<noteq> 0\<rbrakk> \<Longrightarrow> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p \<le> \<bar>r / 2\<bar>
[PROOF STEP]
by (intro stepsize_inverse) auto
[PROOF STATE]
proof (state)
this:
B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p \<le> \<bar>r / 2\<bar>

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t (Suc ?j) \<le> t1 \<Longrightarrow> dist (x (t ?j)) (grid_function (discrete_evolution incr) (x (t 0)) t ?j) \<le> \<bar>r / 2\<bar>

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
have incr_in_r: "dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r\<bar>"
    if "t (Suc j) \<le> t1" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r\<bar>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r\<bar>
[PROOF STEP]
note incr_in[OF that]
[PROOF STATE]
proof (state)
this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r\<bar>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r\<bar>
[PROOF STEP]
have "\<bar>r/2\<bar> \<le> \<bar>r\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>r / 2\<bar> \<le> \<bar>r\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>r / 2\<bar> \<le> \<bar>r\<bar>

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r\<bar>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r\<bar>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r\<bar>

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r\<bar>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r\<bar>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t (Suc ?j) \<le> t1 \<Longrightarrow> dist (x (t ?j)) (grid_function (discrete_evolution incr) (x (t 0)) t ?j) \<le> \<bar>r\<bar>

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
have "dist
    (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)
    (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le>
    B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
proof (intro error_accumulation[OF max_step])
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. \<And>j. t (Suc j) \<le> t1 \<Longrightarrow> dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t (Suc j)) (discrete_evolution incr (t (Suc j)) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ (p + 1)
 6. 0 \<le> B
 7. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 8. t j \<le> t1
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. \<And>j. t (Suc j) \<le> t1 \<Longrightarrow> dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t (Suc j)) (discrete_evolution incr (t (Suc j)) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ (p + 1)
 6. 0 \<le> B
 7. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 8. t j \<le> t1
[PROOF STEP]
assume j: "t (Suc j) \<le> t1"
[PROOF STATE]
proof (state)
this:
t (Suc j) \<le> t1

goal (8 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. \<And>j. t (Suc j) \<le> t1 \<Longrightarrow> dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t (Suc j)) (discrete_evolution incr (t (Suc j)) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ (p + 1)
 6. 0 \<le> B
 7. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 8. t j \<le> t1
[PROOF STEP]
show "dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t (Suc j))
      (discrete_evolution incr (t (Suc j)) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j))
      \<le> B * stepsize j ^ (p + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t (Suc j)) (discrete_evolution incr (t (Suc j)) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ (p + 1)
[PROOF STEP]
using error[OF j]
[PROOF STATE]
proof (prove)
using this:
norm (stepsize j *\<^sub>R s (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ (p + 1)

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t (Suc j)) (discrete_evolution incr (t (Suc j)) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ (p + 1)
[PROOF STEP]
by (simp add: incrs discrete_evolution_def[abs_def] dist_norm
        stepsize_def scaleR_right_distrib)
[PROOF STATE]
proof (state)
this:
dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t (Suc j)) (discrete_evolution incr (t (Suc j)) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ (p + 1)

goal (7 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. 0 \<le> B
 6. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 7. t j \<le> t1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. 0 \<le> B
 6. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 7. t j \<le> t1
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. 0 \<le> B
 6. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 7. t j \<le> t1
[PROOF STEP]
assume "t (Suc j) \<le> t1"
[PROOF STATE]
proof (state)
this:
t (Suc j) \<le> t1

goal (7 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. 0 \<le> B
 6. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 7. t j \<le> t1
[PROOF STEP]
hence "t j \<le> t1"
[PROOF STATE]
proof (prove)
using this:
t (Suc j) \<le> t1

goal (1 subgoal):
 1. t j \<le> t1
[PROOF STEP]
using grid_mono[of j "Suc j"]
[PROOF STATE]
proof (prove)
using this:
t (Suc j) \<le> t1
j \<le> Suc j \<Longrightarrow> t j \<le> t (Suc j)

goal (1 subgoal):
 1. t j \<le> t1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t j \<le> t1

goal (7 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. 0 \<le> B
 6. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 7. t j \<le> t1
[PROOF STEP]
have
      "dist (x (t j)) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)
      \<le> dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) +
      dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)
      (grid_function (discrete_evolution incr) (x (t 0)) t j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) \<le> dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) + dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
[PROOF STEP]
by (rule dist_triangle2)
[PROOF STATE]
proof (state)
this:
dist (x (t j)) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) \<le> dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) + dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)

goal (7 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. 0 \<le> B
 6. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 7. t j \<le> t1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (x (t j)) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) \<le> dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) + dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)

goal (7 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. 0 \<le> B
 6. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 7. t j \<le> t1
[PROOF STEP]
have
      "dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le>
      B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
using \<open>t j \<le> t1\<close>
[PROOF STATE]
proof (prove)
using this:
t j \<le> t1

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
by (rule c1.convergence)
[PROOF STATE]
proof (state)
this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p

goal (7 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. 0 \<le> B
 6. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 7. t j \<le> t1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (x (t j)) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p

goal (7 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. 0 \<le> B
 6. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 7. t j \<le> t1
[PROOF STEP]
have "... \<le> \<bar>r/2\<bar>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p \<le> \<bar>r / 2\<bar>
[PROOF STEP]
using max_stepsize_nonneg grid_interval_notempty max_step
        consistent_nonneg lipschitz_nonneg order_pos
        grid_mono \<open>t j \<le> t1\<close> \<open>t 0 \<le> t1\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> max_stepsize ?n
t 0 \<le> t ?n
t ?j \<le> t1 \<Longrightarrow> max_stepsize ?j \<le> root p (\<bar>r / 2\<bar> * L / B / (exp (L * (t1 - t 0) + 1) - 1))
0 \<le> B
0 \<le> L
0 < p
?j \<le> ?n \<Longrightarrow> t ?j \<le> t ?n
t j \<le> t1
t 0 \<le> t1

goal (1 subgoal):
 1. B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p \<le> \<bar>r / 2\<bar>
[PROOF STEP]
by (intro stepsize_inverse) auto
[PROOF STATE]
proof (state)
this:
B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p \<le> \<bar>r / 2\<bar>

goal (7 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. 0 \<le> B
 6. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 7. t j \<le> t1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p \<le> \<bar>r / 2\<bar>

goal (7 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. 0 \<le> B
 6. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 7. t j \<le> t1
[PROOF STEP]
assume "dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)
      (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>"
[PROOF STATE]
proof (state)
this:
dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>

goal (7 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. 0 \<le> B
 6. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 7. t j \<le> t1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>xa y. xa \<le> y \<Longrightarrow> xa + dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> y + dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j); \<And>xa y. xa \<le> y \<Longrightarrow> xa + dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> y + dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j); \<And>x y. x \<le> y \<Longrightarrow> \<bar>r / 2\<bar> + x \<le> \<bar>r / 2\<bar> + y\<rbrakk> \<Longrightarrow> dist (x (t j)) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) \<le> \<bar>r / 2\<bar> + \<bar>r / 2\<bar>
[PROOF STEP]
have "dist
      (x (t j))
      (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) \<le> \<bar>r\<bar>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>xa y. xa \<le> y \<Longrightarrow> xa + dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> y + dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j); \<And>xa y. xa \<le> y \<Longrightarrow> xa + dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> y + dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j); \<And>x y. x \<le> y \<Longrightarrow> \<bar>r / 2\<bar> + x \<le> \<bar>r / 2\<bar> + y\<rbrakk> \<Longrightarrow> dist (x (t j)) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) \<le> \<bar>r / 2\<bar> + \<bar>r / 2\<bar>

goal (1 subgoal):
 1. dist (x (t j)) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) \<le> \<bar>r\<bar>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (x (t j)) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) \<le> \<bar>r\<bar>

goal (7 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. \<And>j. \<lbrakk>t (Suc j) \<le> t1; dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> \<bar>r / 2\<bar>\<rbrakk> \<Longrightarrow> dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
 4. 0 \<le> L
 5. 0 \<le> B
 6. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 7. t j \<le> t1
[PROOF STEP]
thus "dist
      (incr (stepsize j) (t j)
      (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j))
      (incr (stepsize j) (t j)
      (grid_function (discrete_evolution incr) (x (t 0)) t j))
      \<le> L *
      dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)
      (grid_function (discrete_evolution incr) (x (t 0)) t j)"
[PROOF STATE]
proof (prove)
using this:
dist (x (t j)) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) \<le> \<bar>r\<bar>

goal (1 subgoal):
 1. dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
[PROOF STEP]
using  \<open>t j \<le> t1\<close> \<open>t (Suc j) \<le> t1\<close> incr_in_r
        max_stepsize_nonneg
        grid_ge_min
        grid_stepsize_nonneg
        grid_mono[of j]
[PROOF STATE]
proof (prove)
using this:
dist (x (t j)) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) \<le> \<bar>r\<bar>
t j \<le> t1
t (Suc j) \<le> t1
t (Suc ?j) \<le> t1 \<Longrightarrow> dist (x (t ?j)) (grid_function (discrete_evolution incr) (x (t 0)) t ?j) \<le> \<bar>r\<bar>
0 \<le> max_stepsize ?n
t 0 \<le> t ?j
0 \<le> stepsize ?j
j \<le> ?n \<Longrightarrow> t j \<le> t ?n

goal (1 subgoal):
 1. dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)
[PROOF STEP]
by (intro lipschitz_incr[THEN lipschitz_onD]) (auto simp: stepsize_def mem_cball)
[PROOF STATE]
proof (state)
this:
dist (incr (stepsize j) (t j) (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)) \<le> L * dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j)

goal (6 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. 0 \<le> L
 4. 0 \<le> B
 5. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 6. t j \<le> t1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. 0 \<le> L
 4. 0 \<le> B
 5. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
 6. t j \<le> t1
[PROOF STEP]
show "dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0)
      (x (t 0))
      \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
[PROOF STEP]
using initial_error
[PROOF STATE]
proof (prove)
using this:
norm s0 \<le> B / L * (exp 1 - 1) * stepsize 0 ^ p

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L
[PROOF STEP]
by (simp add: dist_norm)
[PROOF STATE]
proof (state)
this:
dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t 0) (x (t 0)) \<le> B * (exp 1 - 1) * stepsize 0 ^ p / L

goal (5 subgoals):
 1. t j \<le> t1
 2. 0 < p
 3. 0 \<le> L
 4. 0 \<le> B
 5. t j \<le> t1
[PROOF STEP]
qed (simp_all add: consistent_nonneg order_pos lipschitz_nonneg \<open>t j \<le> t1\<close>)
[PROOF STATE]
proof (state)
this:
dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
have "... \<le>
    B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
using grid lipschitz_nonneg consistent_nonneg
      max_stepsize_nonneg
      grid_ge_min grid_mono \<open>t j \<le> t1\<close>
[PROOF STATE]
proof (prove)
using this:
t ?i \<le> t (Suc ?i)
0 \<le> L
0 \<le> B
0 \<le> max_stepsize ?n
t 0 \<le> t ?j
?j \<le> ?n \<Longrightarrow> t ?j \<le> t ?n
t j \<le> t1

goal (1 subgoal):
 1. B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
by  (auto simp add: ac_simps intro!: divide_right_mono mult_left_mono)
[PROOF STATE]
proof (state)
this:
B / L * (exp (L * (t j - t 0) + 1) - 1) * max_stepsize j ^ p \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
have "dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j)
   (grid_function (discrete_evolution incr) (x (t 0)) t j)
  \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p"
[PROOF STATE]
proof (prove)
using this:
dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stability:
  assumes "t j \<le> t1"
  shows "dist
   ((grid_function (discrete_evolution incr') (x0') t j))
   (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le>
     B / L * (exp (L * (t1 - (t 0)) + 1) - 1) * max_stepsize j ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incr') x0' t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incr') x0' t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
note fg' = incr_approx
[PROOF STATE]
proof (state)
this:
t ?j \<le> t1 \<Longrightarrow> dist (incr ?h (t ?j) ?x) (incr' ?h (t ?j) ?x) \<le> B * stepsize ?j ^ p

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incr') x0' t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
define s0 where "s0 \<equiv> x0' - x (t 0)"
[PROOF STATE]
proof (state)
this:
s0 \<equiv> x0' - x (t 0)

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incr') x0' t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
hence x0': "x0' = x (t 0) + s0"
[PROOF STATE]
proof (prove)
using this:
s0 \<equiv> x0' - x (t 0)

goal (1 subgoal):
 1. x0' = x (t 0) + s0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x0' = x (t 0) + s0

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incr') x0' t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
define s where "s \<equiv> \<lambda>x xa xb. (incr' x xa xb) - incr x xa xb"
[PROOF STATE]
proof (state)
this:
s \<equiv> \<lambda>x xa xb. incr' x xa xb - incr x xa xb

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incr') x0' t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
define incrs where "incrs \<equiv> \<lambda>h t x. incr h t x + s h t x"
[PROOF STATE]
proof (state)
this:
incrs \<equiv> \<lambda>h t x. incr h t x + s h t x

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incr') x0' t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
have s: "incr' = incrs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incr' = incrs
[PROOF STEP]
by (simp add: s_def incrs_def [abs_def])
[PROOF STATE]
proof (state)
this:
incr' = incrs

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incr') x0' t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
interpret c: stable_one_step t1 x incr p B r L t s s0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stable_one_step t1 x incr p B r L t s s0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. norm s0 \<le> B / L * (exp 1 - 1) * stepsize 0 ^ p
 2. \<And>j. t (Suc j) \<le> t1 \<Longrightarrow> norm (s (stepsize j) (t j) (grid_function (discrete_evolution (\<lambda>h t x. incr h t x + s h t x)) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ p
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. norm s0 \<le> B / L * (exp 1 - 1) * stepsize 0 ^ p
 2. \<And>j. t (Suc j) \<le> t1 \<Longrightarrow> norm (s (stepsize j) (t j) (grid_function (discrete_evolution (\<lambda>h t x. incr h t x + s h t x)) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ p
[PROOF STEP]
assume "(t (Suc j)) \<le> t1"
[PROOF STATE]
proof (state)
this:
t (Suc j) \<le> t1

goal (2 subgoals):
 1. norm s0 \<le> B / L * (exp 1 - 1) * stepsize 0 ^ p
 2. \<And>j. t (Suc j) \<le> t1 \<Longrightarrow> norm (s (stepsize j) (t j) (grid_function (discrete_evolution (\<lambda>h t x. incr h t x + s h t x)) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ p
[PROOF STEP]
hence "t j \<le> t1"
[PROOF STATE]
proof (prove)
using this:
t (Suc j) \<le> t1

goal (1 subgoal):
 1. t j \<le> t1
[PROOF STEP]
using grid_mono[of j "Suc j"]
[PROOF STATE]
proof (prove)
using this:
t (Suc j) \<le> t1
j \<le> Suc j \<Longrightarrow> t j \<le> t (Suc j)

goal (1 subgoal):
 1. t j \<le> t1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t j \<le> t1

goal (2 subgoals):
 1. norm s0 \<le> B / L * (exp 1 - 1) * stepsize 0 ^ p
 2. \<And>j. t (Suc j) \<le> t1 \<Longrightarrow> norm (s (stepsize j) (t j) (grid_function (discrete_evolution (\<lambda>h t x. incr h t x + s h t x)) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ p
[PROOF STEP]
have "norm (s (stepsize j) (t j) (grid_function
             (discrete_evolution (\<lambda>h t x. (incr' h t x)))
             (x (t 0) + s0) t j))
          \<le> B * stepsize j ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (s (stepsize j) (t j) (grid_function (discrete_evolution incr') (x (t 0) + s0) t j)) \<le> B * stepsize j ^ p
[PROOF STEP]
unfolding s_def dist_norm[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (incr' (stepsize j) (t j) (grid_function (discrete_evolution incr') (x (t 0) + s0) t j)) (incr (stepsize j) (t j) (grid_function (discrete_evolution incr') (x (t 0) + s0) t j)) \<le> B * stepsize j ^ p
[PROOF STEP]
by (simp only: dist_commute fg'[OF \<open>t j \<le> t1\<close>])
[PROOF STATE]
proof (state)
this:
norm (s (stepsize j) (t j) (grid_function (discrete_evolution incr') (x (t 0) + s0) t j)) \<le> B * stepsize j ^ p

goal (2 subgoals):
 1. norm s0 \<le> B / L * (exp 1 - 1) * stepsize 0 ^ p
 2. \<And>j. t (Suc j) \<le> t1 \<Longrightarrow> norm (s (stepsize j) (t j) (grid_function (discrete_evolution (\<lambda>h t x. incr h t x + s h t x)) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
norm (s (stepsize j) (t j) (grid_function (discrete_evolution incr') (x (t 0) + s0) t j)) \<le> B * stepsize j ^ p
[PROOF STEP]
show "norm
         (s (stepsize j) (t j)
           (grid_function (discrete_evolution (\<lambda>h t x. incr h t x + s h t x))
             (x (t 0) + s0) (\<lambda>x. (t x)) j))
        \<le> B * stepsize j ^ p"
[PROOF STATE]
proof (prove)
using this:
norm (s (stepsize j) (t j) (grid_function (discrete_evolution incr') (x (t 0) + s0) t j)) \<le> B * stepsize j ^ p

goal (1 subgoal):
 1. norm (s (stepsize j) (t j) (grid_function (discrete_evolution (\<lambda>h t x. incr h t x + s h t x)) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ p
[PROOF STEP]
by (simp add: s incrs_def)
[PROOF STATE]
proof (state)
this:
norm (s (stepsize j) (t j) (grid_function (discrete_evolution (\<lambda>h t x. incr h t x + s h t x)) (x (t 0) + s0) t j)) \<le> B * stepsize j ^ p

goal (1 subgoal):
 1. norm s0 \<le> B / L * (exp 1 - 1) * stepsize 0 ^ p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norm s0 \<le> B / L * (exp 1 - 1) * stepsize 0 ^ p
[PROOF STEP]
show "norm s0 \<le> B / L * (exp 1 - 1) * stepsize 0 ^ p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm s0 \<le> B / L * (exp 1 - 1) * stepsize 0 ^ p
[PROOF STEP]
unfolding s0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (x0' - x (t 0)) \<le> B / L * (exp 1 - 1) * stepsize 0 ^ p
[PROOF STEP]
using initial_error
[PROOF STATE]
proof (prove)
using this:
dist (x (t 0)) x0' \<le> B / L * (exp 1 - 1) * stepsize 0 ^ p

goal (1 subgoal):
 1. norm (x0' - x (t 0)) \<le> B / L * (exp 1 - 1) * stepsize 0 ^ p
[PROOF STEP]
by (simp add: dist_commute dist_norm)
[PROOF STATE]
proof (state)
this:
norm s0 \<le> B / L * (exp 1 - 1) * stepsize 0 ^ p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incr') x0' t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incr') x0' t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
unfolding s x0'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
using \<open>t j \<le> t1\<close>
[PROOF STATE]
proof (prove)
using this:
t j \<le> t1

goal (1 subgoal):
 1. dist (grid_function (discrete_evolution incrs) (x (t 0) + s0) t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p
[PROOF STEP]
by (rule c.stability[simplified incrs_def[symmetric]])
[PROOF STATE]
proof (state)
this:
dist (grid_function (discrete_evolution incr') x0' t j) (grid_function (discrete_evolution incr) (x (t 0)) t j) \<le> B / L * (exp (L * (t1 - t 0) + 1) - 1) * max_stepsize j ^ p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subcomponents_loc:
assumes "correctCompositionLoc x"
       and "subcomponents x = {}"
shows "loc x = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. loc x = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
correctCompositionLoc x
subcomponents x = {}

goal (1 subgoal):
 1. loc x = {}
[PROOF STEP]
by (simp add: correctCompositionLoc_def)


[STATEMENT]
lemma observable_set_stack_in_slice:
  "S,f \<turnstile> (ms,s) -a\<rightarrow> (ms',s')
  \<Longrightarrow> \<forall>mx \<in> set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S,f \<turnstile> (ms,s) -a\<rightarrow> (ms',s') \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
proof(induct rule:observable_move.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>f a s s' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length s' = length s; length ms = length s; hd ms = sourcenode a; ms' = targetnode a # tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. \<And>f a s s' Q r p fs a' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 3. \<And>f a s s' Q p f' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
case (observable_move_intra f a s s' ms S ms')
[PROOF STATE]
proof (state)
this:
pred (f a) s
transfer (f a) s = s'
valid_edge a
intra_kind (kind a)
\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
length s' = length s
length ms = length s
hd ms = sourcenode a
ms' = targetnode a # tl ms

goal (3 subgoals):
 1. \<And>f a s s' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; intra_kind (kind a); \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length s' = length s; length ms = length s; hd ms = sourcenode a; ms' = targetnode a # tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. \<And>f a s s' Q r p fs a' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 3. \<And>f a s s' Q p f' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
pred (f a) s
transfer (f a) s = s'
valid_edge a
intra_kind (kind a)
\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
length s' = length s
length ms = length s
hd ms = sourcenode a
ms' = targetnode a # tl ms

goal (1 subgoal):
 1. \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. \<And>f a s s' Q p f' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. \<And>f a s s' Q p f' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
case (observable_move_call f a s s' Q r p fs a' ms S ms')
[PROOF STATE]
proof (state)
this:
pred (f a) s
transfer (f a) s = s'
valid_edge a
kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs
valid_edge a'
a' \<in> get_return_edges a
\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
length ms = length s
length s' = Suc (length s)
hd ms = sourcenode a
ms' = targetnode a # targetnode a' # tl ms

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. \<And>f a s s' Q p f' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
from \<open>valid_edge a\<close> \<open>valid_edge a'\<close> \<open>a' \<in> get_return_edges a\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a
valid_edge a'
a' \<in> get_return_edges a
[PROOF STEP]
have "call_of_return_node (targetnode a') (sourcenode a)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a
valid_edge a'
a' \<in> get_return_edges a

goal (1 subgoal):
 1. call_of_return_node (targetnode a') (sourcenode a)
[PROOF STEP]
by(fastforce simp:return_node_def call_of_return_node_def)
[PROOF STATE]
proof (state)
this:
call_of_return_node (targetnode a') (sourcenode a)

goal (2 subgoals):
 1. \<And>f a s s' Q r p fs a' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q:r\<hookrightarrow>\<^bsub>p\<^esub>fs; valid_edge a'; a' \<in> get_return_edges a; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s' = Suc (length s); hd ms = sourcenode a; ms' = targetnode a # targetnode a' # tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
 2. \<And>f a s s' Q p f' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
with \<open>hd ms = sourcenode a\<close> \<open>hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
    \<open>ms' = targetnode a # targetnode a' # tl ms\<close>
    \<open>\<forall>mx\<in>set (tl ms). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>\<close>
[PROOF STATE]
proof (chain)
picking this:
hd ms = sourcenode a
hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
ms' = targetnode a # targetnode a' # tl ms
\<forall>mx\<in>set (tl ms). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
call_of_return_node (targetnode a') (sourcenode a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
hd ms = sourcenode a
hd ms \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
ms' = targetnode a # targetnode a' # tl ms
\<forall>mx\<in>set (tl ms). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
call_of_return_node (targetnode a') (sourcenode a)

goal (1 subgoal):
 1. \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal (1 subgoal):
 1. \<And>f a s s' Q p f' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f a s s' Q p f' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
case (observable_move_return f a s s' Q p f' ms S ms')
[PROOF STATE]
proof (state)
this:
pred (f a) s
transfer (f a) s = s'
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'
\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
length ms = length s
length s = Suc (length s')
s' \<noteq> []
hd ms = sourcenode a
hd (tl ms) = targetnode a
ms' = tl ms

goal (1 subgoal):
 1. \<And>f a s s' Q p f' ms S ms'. \<lbrakk>pred (f a) s; transfer (f a) s = s'; valid_edge a; kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'; \<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>; length ms = length s; length s = Suc (length s'); s' \<noteq> []; hd ms = sourcenode a; hd (tl ms) = targetnode a; ms' = tl ms\<rbrakk> \<Longrightarrow> \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
pred (f a) s
transfer (f a) s = s'
valid_edge a
kind a = Q\<hookleftarrow>\<^bsub>p\<^esub>f'
\<forall>m\<in>set (tl ms). \<exists>m'. call_of_return_node m m' \<and> m' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
length ms = length s
length s = Suc (length s')
s' \<noteq> []
hd ms = sourcenode a
hd (tl ms) = targetnode a
ms' = tl ms

goal (1 subgoal):
 1. \<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>
[PROOF STEP]
by(cases "tl ms") auto
[PROOF STATE]
proof (state)
this:
\<forall>mx\<in>set (tl ms'). \<exists>mx'. call_of_return_node mx mx' \<and> mx' \<in> \<lfloor>HRB_slice S\<rfloor>\<^bsub>CFG\<^esub>

goal:
No subgoals!
[PROOF STEP]
qed