[STATEMENT]
lemma norm_X_Y_bound:
shows "\<forall>t \<in> J \<inter> G.existence_ivl 0 x0. norm (flow0 t - Y t) \<le> e / K * (exp(K * \<bar>t\<bar>) - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>t\<in>J \<inter> G.existence_ivl 0 x0. norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
proof(safe)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>t \<in> J; t \<in> G.existence_ivl 0 x0\<rbrakk> \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>t \<in> J; t \<in> G.existence_ivl 0 x0\<rbrakk> \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
assume "t \<in> J"
[PROOF STATE]
proof (state)
this:
t \<in> J

goal (1 subgoal):
 1. \<And>t. \<lbrakk>t \<in> J; t \<in> G.existence_ivl 0 x0\<rbrakk> \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
assume tG: "t \<in> G.existence_ivl 0 x0"
[PROOF STATE]
proof (state)
this:
t \<in> G.existence_ivl 0 x0

goal (1 subgoal):
 1. \<And>t. \<lbrakk>t \<in> J; t \<in> G.existence_ivl 0 x0\<rbrakk> \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
have "0 \<in> J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<in> J
[PROOF STEP]
by (simp add: t0_in_J)
[PROOF STATE]
proof (state)
this:
0 \<in> J

goal (1 subgoal):
 1. \<And>t. \<lbrakk>t \<in> J; t \<in> G.existence_ivl 0 x0\<rbrakk> \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
let ?u="\<lambda>t. norm (flow0 t - Y t)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>t \<in> J; t \<in> G.existence_ivl 0 x0\<rbrakk> \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
show "norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
proof(cases "0 \<le> t")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
 2. \<not> 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
assume "0 \<le> t"
[PROOF STATE]
proof (state)
this:
0 \<le> t

goal (2 subgoals):
 1. 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
 2. \<not> 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
hence [simp]: "\<bar>t\<bar> = t"
[PROOF STATE]
proof (prove)
using this:
0 \<le> t

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

goal (2 subgoals):
 1. 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
 2. \<not> 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
have t0_t_in_J: "{0..t} \<subseteq> J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..t} \<subseteq> J
[PROOF STEP]
using \<open>t \<in> J\<close> \<open>0 \<in> J\<close> J_ivl
[PROOF STATE]
proof (prove)
using this:
t \<in> J
0 \<in> J
is_interval J

goal (1 subgoal):
 1. {0..t} \<subseteq> J
[PROOF STEP]
using mem_is_interval_1_I atLeastAtMost_iff subsetI
[PROOF STATE]
proof (prove)
using this:
t \<in> J
0 \<in> J
is_interval J
\<lbrakk>is_interval ?S; ?a \<in> ?S; ?c \<in> ?S; ?a \<le> ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?b \<in> ?S
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)
(\<And>x. x \<in> ?A \<Longrightarrow> x \<in> ?B) \<Longrightarrow> ?A \<subseteq> ?B

goal (1 subgoal):
 1. {0..t} \<subseteq> J
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{0..t} \<subseteq> J

goal (2 subgoals):
 1. 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
 2. \<not> 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
note F_G_flow_cont[continuous_intros] =
      continuous_on_subset[OF F.flow_continuous_on]
      continuous_on_subset[OF G.flow_continuous_on]
[PROOF STATE]
proof (state)
this:
?t \<subseteq> F.existence_ivl ?t0.1 ?x0.1 \<Longrightarrow> continuous_on ?t (F.flow ?t0.1 ?x0.1)
?t \<subseteq> G.existence_ivl ?t0.1 ?x0.1 \<Longrightarrow> continuous_on ?t (G.flow ?t0.1 ?x0.1)

goal (2 subgoals):
 1. 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
 2. \<not> 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
have "?u t + e/K \<le> e/K * exp(K * t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (flow0 t - Y t) + e / K \<le> e / K * exp (K * t)
[PROOF STEP]
proof(rule gronwall[where g="\<lambda>t. ?u t + e/K", OF _ _ _ _ K_pos \<open>0 \<le> t\<close> order.refl])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
assume "0 \<le> s" "s \<le> t"
[PROOF STATE]
proof (state)
this:
0 \<le> s
s \<le> t

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
hence "{0..s} \<subseteq> J"
[PROOF STATE]
proof (prove)
using this:
0 \<le> s
s \<le> t

goal (1 subgoal):
 1. {0..s} \<subseteq> J
[PROOF STEP]
using t0_t_in_J
[PROOF STATE]
proof (prove)
using this:
0 \<le> s
s \<le> t
{0..t} \<subseteq> J

goal (1 subgoal):
 1. {0..s} \<subseteq> J
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..s} \<subseteq> J

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
hence t0_s_in_existence:
        "{0..s} \<subseteq> F.existence_ivl 0 x0"
        "{0..s} \<subseteq> G.existence_ivl 0 x0"
[PROOF STATE]
proof (prove)
using this:
{0..s} \<subseteq> J

goal (1 subgoal):
 1. {0..s} \<subseteq> F.existence_ivl 0 x0 &&& {0..s} \<subseteq> G.existence_ivl 0 x0
[PROOF STEP]
using J_subset tG \<open>0 \<le> s\<close> \<open>s \<le> t\<close> G.ivl_subset_existence_ivl[OF tG]
[PROOF STATE]
proof (prove)
using this:
{0..s} \<subseteq> J
J \<subseteq> F.existence_ivl 0 x0
t \<in> G.existence_ivl 0 x0
0 \<le> s
s \<le> t
{0..t} \<subseteq> G.existence_ivl 0 x0

goal (1 subgoal):
 1. {0..s} \<subseteq> F.existence_ivl 0 x0 &&& {0..s} \<subseteq> G.existence_ivl 0 x0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{0..s} \<subseteq> F.existence_ivl 0 x0
{0..s} \<subseteq> G.existence_ivl 0 x0

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
hence s_in_existence:
        "s \<in> F.existence_ivl 0 x0"
        "s \<in> G.existence_ivl 0 x0"
[PROOF STATE]
proof (prove)
using this:
{0..s} \<subseteq> F.existence_ivl 0 x0
{0..s} \<subseteq> G.existence_ivl 0 x0

goal (1 subgoal):
 1. s \<in> F.existence_ivl 0 x0 &&& s \<in> G.existence_ivl 0 x0
[PROOF STEP]
using \<open>0 \<le> s\<close>
[PROOF STATE]
proof (prove)
using this:
{0..s} \<subseteq> F.existence_ivl 0 x0
{0..s} \<subseteq> G.existence_ivl 0 x0
0 \<le> s

goal (1 subgoal):
 1. s \<in> F.existence_ivl 0 x0 &&& s \<in> G.existence_ivl 0 x0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> F.existence_ivl 0 x0
s \<in> G.existence_ivl 0 x0

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
note cont_statements[continuous_intros] =
        F_iv_defined (*  G.iv_defined *)
        F.flow_in_domain
        G.flow_in_domain
        F.mem_existence_ivl_subset
        G.mem_existence_ivl_subset
[PROOF STATE]
proof (state)
this:
0 \<in> T1
x0 \<in> X
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> F.flow ?t0.0 ?x0.0 ?t \<in> X
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> G.flow ?t0.0 ?x0.0 ?t \<in> X
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> ?t \<in> T1
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> ?t \<in> T2

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
have [integrable_on_simps]:
        "continuous_on {0..s} (\<lambda>s. F s (F.flow 0 x0 s))"
        "continuous_on {0..s} (\<lambda>s. G s (G.flow 0 x0 s))"
        "continuous_on {0..s} (\<lambda>s. F s (G.flow 0 x0 s))"
        "continuous_on {0..s} (\<lambda>s. G s (F.flow 0 x0 s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (continuous_on {0..s} (\<lambda>s. F s (F.flow 0 x0 s)) &&& continuous_on {0..s} (\<lambda>s. G s (G.flow 0 x0 s))) &&& continuous_on {0..s} (\<lambda>s. F s (G.flow 0 x0 s)) &&& continuous_on {0..s} (\<lambda>s. G s (F.flow 0 x0 s))
[PROOF STEP]
using t0_s_in_existence
[PROOF STATE]
proof (prove)
using this:
{0..s} \<subseteq> F.existence_ivl 0 x0
{0..s} \<subseteq> G.existence_ivl 0 x0

goal (1 subgoal):
 1. (continuous_on {0..s} (\<lambda>s. F s (F.flow 0 x0 s)) &&& continuous_on {0..s} (\<lambda>s. G s (G.flow 0 x0 s))) &&& continuous_on {0..s} (\<lambda>s. F s (G.flow 0 x0 s)) &&& continuous_on {0..s} (\<lambda>s. G s (F.flow 0 x0 s))
[PROOF STEP]
by (auto intro!: continuous_intros integrable_continuous_real)
[PROOF STATE]
proof (state)
this:
continuous_on {0..s} (\<lambda>s. F s (F.flow 0 x0 s))
continuous_on {0..s} (\<lambda>s. G s (G.flow 0 x0 s))
continuous_on {0..s} (\<lambda>s. F s (G.flow 0 x0 s))
continuous_on {0..s} (\<lambda>s. G s (F.flow 0 x0 s))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
have "flow0 s - Y s = integral {0..s} (\<lambda>s. F s (flow0 s) - G s (Y s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. flow0 s - Y s = integral {0..s} (\<lambda>s. F s (flow0 s) - G s (Y s))
[PROOF STEP]
using \<open>0 \<le> s\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> s

goal (1 subgoal):
 1. flow0 s - Y s = integral {0..s} (\<lambda>s. F s (flow0 s) - G s (Y s))
[PROOF STEP]
by (simp add: flow0_def Y_def Henstock_Kurzweil_Integration.integral_diff integrable_on_simps ivl_integral_def
               F.flow_fixed_point[OF s_in_existence(1)]
               G.flow_fixed_point[OF s_in_existence(2)])
[PROOF STATE]
proof (state)
this:
flow0 s - Y s = integral {0..s} (\<lambda>s. F s (flow0 s) - G s (Y s))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
flow0 s - Y s = integral {0..s} (\<lambda>s. F s (flow0 s) - G s (Y s))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
have "... = integral {0..s} (\<lambda>s. (F s (flow0 s) - F s (Y s)) + (F s (Y s) - G s (Y s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..s} (\<lambda>s. F s (flow0 s) - G s (Y s)) = integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s) + (F s (Y s) - G s (Y s)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
integral {0..s} (\<lambda>s. F s (flow0 s) - G s (Y s)) = integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s) + (F s (Y s) - G s (Y s)))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral {0..s} (\<lambda>s. F s (flow0 s) - G s (Y s)) = integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s) + (F s (Y s) - G s (Y s)))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
have "... = integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s)) + integral {0..s} (\<lambda>s. F s (Y s) - G s (Y s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s) + (F s (Y s) - G s (Y s))) = integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s)) + integral {0..s} (\<lambda>s. F s (Y s) - G s (Y s))
[PROOF STEP]
by (simp add: Henstock_Kurzweil_Integration.integral_diff Henstock_Kurzweil_Integration.integral_add flow0_def Y_def integrable_on_simps)
[PROOF STATE]
proof (state)
this:
integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s) + (F s (Y s) - G s (Y s))) = integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s)) + integral {0..s} (\<lambda>s. F s (Y s) - G s (Y s))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
flow0 s - Y s = integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s)) + integral {0..s} (\<lambda>s. F s (Y s) - G s (Y s))
[PROOF STEP]
have "?u s \<le> norm (integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {0..s} (\<lambda>s. F s (Y s) - G s (Y s)))"
[PROOF STATE]
proof (prove)
using this:
flow0 s - Y s = integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s)) + integral {0..s} (\<lambda>s. F s (Y s) - G s (Y s))

goal (1 subgoal):
 1. norm (flow0 s - Y s) \<le> norm (integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {0..s} (\<lambda>s. F s (Y s) - G s (Y s)))
[PROOF STEP]
by (simp add: norm_triangle_ineq)
[PROOF STATE]
proof (state)
this:
norm (flow0 s - Y s) \<le> norm (integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {0..s} (\<lambda>s. F s (Y s) - G s (Y s)))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (flow0 s - Y s) \<le> norm (integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {0..s} (\<lambda>s. F s (Y s) - G s (Y s)))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
have "... \<le> integral {0..s} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {0..s} (\<lambda>s. norm (F s (Y s) - G s (Y s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {0..s} (\<lambda>s. F s (Y s) - G s (Y s))) \<le> integral {0..s} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {0..s} (\<lambda>s. norm (F s (Y s) - G s (Y s)))
[PROOF STEP]
using t0_s_in_existence
[PROOF STATE]
proof (prove)
using this:
{0..s} \<subseteq> F.existence_ivl 0 x0
{0..s} \<subseteq> G.existence_ivl 0 x0

goal (1 subgoal):
 1. norm (integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {0..s} (\<lambda>s. F s (Y s) - G s (Y s))) \<le> integral {0..s} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {0..s} (\<lambda>s. norm (F s (Y s) - G s (Y s)))
[PROOF STEP]
by (auto simp add: flow0_def Y_def
          intro!: add_mono continuous_intros continuous_on_imp_absolutely_integrable_on)
[PROOF STATE]
proof (state)
this:
norm (integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {0..s} (\<lambda>s. F s (Y s) - G s (Y s))) \<le> integral {0..s} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {0..s} (\<lambda>s. norm (F s (Y s) - G s (Y s)))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (integral {0..s} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {0..s} (\<lambda>s. F s (Y s) - G s (Y s))) \<le> integral {0..s} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {0..s} (\<lambda>s. norm (F s (Y s) - G s (Y s)))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
have "... \<le> integral {0..s} (\<lambda>s. K * ?u s) + integral {0..s} (\<lambda>s. e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..s} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {0..s} (\<lambda>s. norm (F s (Y s) - G s (Y s))) \<le> integral {0..s} (\<lambda>s. K * norm (flow0 s - Y s)) + integral {0..s} (\<lambda>s. e)
[PROOF STEP]
proof (rule add_mono[OF integral_le integral_le])
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) integrable_on {0..s}
 2. (\<lambda>s. K * norm (flow0 s - Y s)) integrable_on {0..s}
 3. \<And>x. x \<in> {0..s} \<Longrightarrow> norm (F x (flow0 x) - F x (Y x)) \<le> K * norm (flow0 x - Y x)
 4. (\<lambda>s. norm (F s (Y s) - G s (Y s))) integrable_on {0..s}
 5. (\<lambda>s. e) integrable_on {0..s}
 6. \<And>x. x \<in> {0..s} \<Longrightarrow> norm (F x (Y x) - G x (Y x)) \<le> e
[PROOF STEP]
show "norm (F x (flow0 x) - F x (Y x)) \<le> K * norm (flow0 x - Y x)" if "x \<in> {0..s}" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (F x (flow0 x) - F x (Y x)) \<le> K * norm (flow0 x - Y x)
[PROOF STEP]
using F_lipschitz[unfolded lipschitz_on_def, THEN conjunct2] that
            cont_statements(1,2,4)
            t0_s_in_existence F_iv_defined
[PROOF STATE]
proof (prove)
using this:
?t1 \<in> J \<Longrightarrow> \<forall>x\<in>X. \<forall>y\<in>X. dist (F ?t1 x) (F ?t1 y) \<le> K * dist x y
x \<in> {0..s}
0 \<in> T1
x0 \<in> X
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> G.flow ?t0.0 ?x0.0 ?t \<in> X
{0..s} \<subseteq> F.existence_ivl 0 x0
{0..s} \<subseteq> G.existence_ivl 0 x0
0 \<in> T1
x0 \<in> X

goal (1 subgoal):
 1. norm (F x (flow0 x) - F x (Y x)) \<le> K * norm (flow0 x - Y x)
[PROOF STEP]
(* G.iv_defined *)
[PROOF STATE]
proof (prove)
using this:
?t1 \<in> J \<Longrightarrow> \<forall>x\<in>X. \<forall>y\<in>X. dist (F ?t1 x) (F ?t1 y) \<le> K * dist x y
x \<in> {0..s}
0 \<in> T1
x0 \<in> X
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> G.flow ?t0.0 ?x0.0 ?t \<in> X
{0..s} \<subseteq> F.existence_ivl 0 x0
{0..s} \<subseteq> G.existence_ivl 0 x0
0 \<in> T1
x0 \<in> X

goal (1 subgoal):
 1. norm (F x (flow0 x) - F x (Y x)) \<le> K * norm (flow0 x - Y x)
[PROOF STEP]
by (metis F_lipschitz flow0_def Y_def \<open>{0..s} \<subseteq> J\<close> lipschitz_on_normD F.flow_in_domain
            G.flow_in_domain subsetCE)
[PROOF STATE]
proof (state)
this:
?x \<in> {0..s} \<Longrightarrow> norm (F ?x (flow0 ?x) - F ?x (Y ?x)) \<le> K * norm (flow0 ?x - Y ?x)

goal (5 subgoals):
 1. (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) integrable_on {0..s}
 2. (\<lambda>s. K * norm (flow0 s - Y s)) integrable_on {0..s}
 3. (\<lambda>s. norm (F s (Y s) - G s (Y s))) integrable_on {0..s}
 4. (\<lambda>s. e) integrable_on {0..s}
 5. \<And>x. x \<in> {0..s} \<Longrightarrow> norm (F x (Y x) - G x (Y x)) \<le> e
[PROOF STEP]
show "\<And>x. x \<in> {0..s} \<Longrightarrow> norm (F x (Y x) - G x (Y x)) \<le> e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {0..s} \<Longrightarrow> norm (F x (Y x) - G x (Y x)) \<le> e
[PROOF STEP]
using F_G_norm_ineq cont_statements(2,3) t0_s_in_existence
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t \<in> J; ?x \<in> X\<rbrakk> \<Longrightarrow> norm (F ?t ?x - G ?t ?x) < e
x0 \<in> X
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> F.flow ?t0.0 ?x0.0 ?t \<in> X
{0..s} \<subseteq> F.existence_ivl 0 x0
{0..s} \<subseteq> G.existence_ivl 0 x0

goal (1 subgoal):
 1. \<And>x. x \<in> {0..s} \<Longrightarrow> norm (F x (Y x) - G x (Y x)) \<le> e
[PROOF STEP]
using Y_def \<open>{0..s} \<subseteq> J\<close> cont_statements(5) subset_iff G.flow_in_domain
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t \<in> J; ?x \<in> X\<rbrakk> \<Longrightarrow> norm (F ?t ?x - G ?t ?x) < e
x0 \<in> X
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> F.flow ?t0.0 ?x0.0 ?t \<in> X
{0..s} \<subseteq> F.existence_ivl 0 x0
{0..s} \<subseteq> G.existence_ivl 0 x0
Y ?t = G.flow 0 x0 ?t
{0..s} \<subseteq> J
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> ?t \<in> T1
(?A \<subseteq> ?B) = (\<forall>t. t \<in> ?A \<longrightarrow> t \<in> ?B)
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> G.flow ?t0.0 ?x0.0 ?t \<in> X

goal (1 subgoal):
 1. \<And>x. x \<in> {0..s} \<Longrightarrow> norm (F x (Y x) - G x (Y x)) \<le> e
[PROOF STEP]
by (metis eucl_less_le_not_le)
[PROOF STATE]
proof (state)
this:
?x \<in> {0..s} \<Longrightarrow> norm (F ?x (Y ?x) - G ?x (Y ?x)) \<le> e

goal (4 subgoals):
 1. (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) integrable_on {0..s}
 2. (\<lambda>s. K * norm (flow0 s - Y s)) integrable_on {0..s}
 3. (\<lambda>s. norm (F s (Y s) - G s (Y s))) integrable_on {0..s}
 4. (\<lambda>s. e) integrable_on {0..s}
[PROOF STEP]
qed (simp_all add: t0_s_in_existence continuous_intros integrable_on_simps flow0_def Y_def)
[PROOF STATE]
proof (state)
this:
integral {0..s} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {0..s} (\<lambda>s. norm (F s (Y s) - G s (Y s))) \<le> integral {0..s} (\<lambda>s. K * norm (flow0 s - Y s)) + integral {0..s} (\<lambda>s. e)

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral {0..s} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {0..s} (\<lambda>s. norm (F s (Y s) - G s (Y s))) \<le> integral {0..s} (\<lambda>s. K * norm (flow0 s - Y s)) + integral {0..s} (\<lambda>s. e)

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
have "... = K * integral {0..s} (\<lambda>s. ?u s + e / K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {0..s} (\<lambda>s. K * norm (flow0 s - Y s)) + integral {0..s} (\<lambda>s. e) = K * integral {0..s} (\<lambda>s. norm (flow0 s - Y s) + e / K)
[PROOF STEP]
using K_pos t0_s_in_existence
[PROOF STATE]
proof (prove)
using this:
0 < K
{0..s} \<subseteq> F.existence_ivl 0 x0
{0..s} \<subseteq> G.existence_ivl 0 x0

goal (1 subgoal):
 1. integral {0..s} (\<lambda>s. K * norm (flow0 s - Y s)) + integral {0..s} (\<lambda>s. e) = K * integral {0..s} (\<lambda>s. norm (flow0 s - Y s) + e / K)
[PROOF STEP]
by (simp_all add: algebra_simps Henstock_Kurzweil_Integration.integral_add flow0_def Y_def continuous_intros
          continuous_on_imp_absolutely_integrable_on)
[PROOF STATE]
proof (state)
this:
integral {0..s} (\<lambda>s. K * norm (flow0 s - Y s)) + integral {0..s} (\<lambda>s. e) = K * integral {0..s} (\<lambda>s. norm (flow0 s - Y s) + e / K)

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {0..ta} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
norm (flow0 s - Y s) \<le> K * integral {0..s} (\<lambda>s. norm (flow0 s - Y s) + e / K)
[PROOF STEP]
show "?u s + e / K \<le> e / K + K * integral {0..s} (\<lambda>s. ?u s + e / K)"
[PROOF STATE]
proof (prove)
using this:
norm (flow0 s - Y s) \<le> K * integral {0..s} (\<lambda>s. norm (flow0 s - Y s) + e / K)

goal (1 subgoal):
 1. norm (flow0 s - Y s) + e / K \<le> e / K + K * integral {0..s} (\<lambda>s. norm (flow0 s - Y s) + e / K)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm (flow0 s - Y s) + e / K \<le> e / K + K * integral {0..s} (\<lambda>s. norm (flow0 s - Y s) + e / K)

goal (3 subgoals):
 1. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 2. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 3. 0 < e / K
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 2. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 3. 0 < e / K
[PROOF STEP]
show "continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
[PROOF STEP]
using t0_t_in_J J_subset G.ivl_subset_existence_ivl[OF tG]
[PROOF STATE]
proof (prove)
using this:
{0..t} \<subseteq> J
J \<subseteq> F.existence_ivl 0 x0
{0..t} \<subseteq> G.existence_ivl 0 x0

goal (1 subgoal):
 1. continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)
[PROOF STEP]
by (auto simp add: flow0_def Y_def intro!: continuous_intros)
[PROOF STATE]
proof (state)
this:
continuous_on {0..t} (\<lambda>t. norm (flow0 t - Y t) + e / K)

goal (2 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 2. 0 < e / K
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 2. 0 < e / K
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 2. 0 < e / K
[PROOF STEP]
assume "0 \<le> s" "s \<le> t"
[PROOF STATE]
proof (state)
this:
0 \<le> s
s \<le> t

goal (2 subgoals):
 1. \<And>ta. \<lbrakk>0 \<le> ta; ta \<le> t\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 2. 0 < e / K
[PROOF STEP]
show "0 \<le> norm (flow0 s - Y s) + e / K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> norm (flow0 s - Y s) + e / K
[PROOF STEP]
using e_pos K_pos
[PROOF STATE]
proof (prove)
using this:
0 < e
0 < K

goal (1 subgoal):
 1. 0 \<le> norm (flow0 s - Y s) + e / K
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> norm (flow0 s - Y s) + e / K

goal (1 subgoal):
 1. 0 < e / K
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < e / K
[PROOF STEP]
show "0 < e / K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < e / K
[PROOF STEP]
using e_pos K_pos
[PROOF STATE]
proof (prove)
using this:
0 < e
0 < K

goal (1 subgoal):
 1. 0 < e / K
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < e / K

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
norm (flow0 t - Y t) + e / K \<le> e / K * exp (K * t)

goal (2 subgoals):
 1. 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
 2. \<not> 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
norm (flow0 t - Y t) + e / K \<le> e / K * exp (K * t)

goal (1 subgoal):
 1. norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)

goal (1 subgoal):
 1. \<not> 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
assume "\<not>0 \<le> t"
[PROOF STATE]
proof (state)
this:
\<not> 0 \<le> t

goal (1 subgoal):
 1. \<not> 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
hence "t \<le> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> 0 \<le> t

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

goal (1 subgoal):
 1. \<not> 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
hence [simp]: "\<bar>t\<bar> = -t"
[PROOF STATE]
proof (prove)
using this:
t \<le> 0

goal (1 subgoal):
 1. \<bar>t\<bar> = - t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<bar>t\<bar> = - t

goal (1 subgoal):
 1. \<not> 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
have t0_t_in_J: "{t..0} \<subseteq> J"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {t..0} \<subseteq> J
[PROOF STEP]
using \<open>t \<in> J\<close> \<open>0 \<in> J\<close> J_ivl \<open>\<not> 0 \<le> t\<close> atMostAtLeast_subset_convex is_interval_convex_1
[PROOF STATE]
proof (prove)
using this:
t \<in> J
0 \<in> J
is_interval J
\<not> 0 \<le> t
\<lbrakk>convex ?C; ?x \<in> ?C; ?y \<in> ?C; ?x < ?y\<rbrakk> \<Longrightarrow> {?x..?y} \<subseteq> ?C
is_interval ?S = convex ?S

goal (1 subgoal):
 1. {t..0} \<subseteq> J
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{t..0} \<subseteq> J

goal (1 subgoal):
 1. \<not> 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
note F_G_flow_cont[continuous_intros] =
      continuous_on_subset[OF F.flow_continuous_on]
      continuous_on_subset[OF G.flow_continuous_on]
[PROOF STATE]
proof (state)
this:
?t \<subseteq> F.existence_ivl ?t0.1 ?x0.1 \<Longrightarrow> continuous_on ?t (F.flow ?t0.1 ?x0.1)
?t \<subseteq> G.existence_ivl ?t0.1 ?x0.1 \<Longrightarrow> continuous_on ?t (G.flow ?t0.1 ?x0.1)

goal (1 subgoal):
 1. \<not> 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
have "?u t + e/K \<le> e/K * exp(- K * t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (flow0 t - Y t) + e / K \<le> e / K * exp (- K * t)
[PROOF STEP]
proof(rule gronwall_left[where g="\<lambda>t. ?u t + e/K", OF _ _ _ _ K_pos order.refl \<open>t \<le> 0\<close>])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
assume "t \<le> s" "s \<le> 0"
[PROOF STATE]
proof (state)
this:
t \<le> s
s \<le> 0

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
hence "{s..0} \<subseteq> J"
[PROOF STATE]
proof (prove)
using this:
t \<le> s
s \<le> 0

goal (1 subgoal):
 1. {s..0} \<subseteq> J
[PROOF STEP]
using t0_t_in_J
[PROOF STATE]
proof (prove)
using this:
t \<le> s
s \<le> 0
{t..0} \<subseteq> J

goal (1 subgoal):
 1. {s..0} \<subseteq> J
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{s..0} \<subseteq> J

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
hence t0_s_in_existence:
        "{s..0} \<subseteq> F.existence_ivl 0 x0"
        "{s..0} \<subseteq> G.existence_ivl 0 x0"
[PROOF STATE]
proof (prove)
using this:
{s..0} \<subseteq> J

goal (1 subgoal):
 1. {s..0} \<subseteq> F.existence_ivl 0 x0 &&& {s..0} \<subseteq> G.existence_ivl 0 x0
[PROOF STEP]
using J_subset G.ivl_subset_existence_ivl'[OF tG] \<open>s \<le> 0\<close> \<open>t \<le> s\<close>
[PROOF STATE]
proof (prove)
using this:
{s..0} \<subseteq> J
J \<subseteq> F.existence_ivl 0 x0
{t..0} \<subseteq> G.existence_ivl 0 x0
s \<le> 0
t \<le> s

goal (1 subgoal):
 1. {s..0} \<subseteq> F.existence_ivl 0 x0 &&& {s..0} \<subseteq> G.existence_ivl 0 x0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{s..0} \<subseteq> F.existence_ivl 0 x0
{s..0} \<subseteq> G.existence_ivl 0 x0

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
hence s_in_existence:
        "s \<in> F.existence_ivl 0 x0"
        "s \<in> G.existence_ivl 0 x0"
[PROOF STATE]
proof (prove)
using this:
{s..0} \<subseteq> F.existence_ivl 0 x0
{s..0} \<subseteq> G.existence_ivl 0 x0

goal (1 subgoal):
 1. s \<in> F.existence_ivl 0 x0 &&& s \<in> G.existence_ivl 0 x0
[PROOF STEP]
using \<open>s \<le> 0\<close>
[PROOF STATE]
proof (prove)
using this:
{s..0} \<subseteq> F.existence_ivl 0 x0
{s..0} \<subseteq> G.existence_ivl 0 x0
s \<le> 0

goal (1 subgoal):
 1. s \<in> F.existence_ivl 0 x0 &&& s \<in> G.existence_ivl 0 x0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> F.existence_ivl 0 x0
s \<in> G.existence_ivl 0 x0

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
note cont_statements[continuous_intros] =
        F_iv_defined
        F.flow_in_domain
        G.flow_in_domain
        F.mem_existence_ivl_subset
        G.mem_existence_ivl_subset
[PROOF STATE]
proof (state)
this:
0 \<in> T1
x0 \<in> X
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> F.flow ?t0.0 ?x0.0 ?t \<in> X
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> G.flow ?t0.0 ?x0.0 ?t \<in> X
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> ?t \<in> T1
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> ?t \<in> T2

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<in> T1
x0 \<in> X
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> F.flow ?t0.0 ?x0.0 ?t \<in> X
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> G.flow ?t0.0 ?x0.0 ?t \<in> X
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> ?t \<in> T1
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> ?t \<in> T2
[PROOF STEP]
have [continuous_intros]:
        "{s..0} \<subseteq> T1"
        "{s..0} \<subseteq> T2"
        "F.flow 0 x0 ` {s..0} \<subseteq> X"
        "G.flow 0 x0 ` {s..0} \<subseteq> X"
        "s \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> x \<in> F.existence_ivl 0 x0"
        "s \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> x \<in> G.existence_ivl 0 x0" for x
[PROOF STATE]
proof (prove)
using this:
0 \<in> T1
x0 \<in> X
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> F.flow ?t0.0 ?x0.0 ?t \<in> X
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> G.flow ?t0.0 ?x0.0 ?t \<in> X
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> ?t \<in> T1
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> ?t \<in> T2

goal (1 subgoal):
 1. ({s..0} \<subseteq> T1 &&& {s..0} \<subseteq> T2 &&& F.flow 0 x0 ` {s..0} \<subseteq> X) &&& G.flow 0 x0 ` {s..0} \<subseteq> X &&& (\<lbrakk>s \<le> x; x \<le> 0\<rbrakk> \<Longrightarrow> x \<in> F.existence_ivl 0 x0) &&& (\<lbrakk>s \<le> x; x \<le> 0\<rbrakk> \<Longrightarrow> x \<in> G.existence_ivl 0 x0)
[PROOF STEP]
using t0_s_in_existence
[PROOF STATE]
proof (prove)
using this:
0 \<in> T1
x0 \<in> X
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> F.flow ?t0.0 ?x0.0 ?t \<in> X
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> G.flow ?t0.0 ?x0.0 ?t \<in> X
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> ?t \<in> T1
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> ?t \<in> T2
{s..0} \<subseteq> F.existence_ivl 0 x0
{s..0} \<subseteq> G.existence_ivl 0 x0

goal (1 subgoal):
 1. ({s..0} \<subseteq> T1 &&& {s..0} \<subseteq> T2 &&& F.flow 0 x0 ` {s..0} \<subseteq> X) &&& G.flow 0 x0 ` {s..0} \<subseteq> X &&& (\<lbrakk>s \<le> x; x \<le> 0\<rbrakk> \<Longrightarrow> x \<in> F.existence_ivl 0 x0) &&& (\<lbrakk>s \<le> x; x \<le> 0\<rbrakk> \<Longrightarrow> x \<in> G.existence_ivl 0 x0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{s..0} \<subseteq> T1
{s..0} \<subseteq> T2
F.flow 0 x0 ` {s..0} \<subseteq> X
G.flow 0 x0 ` {s..0} \<subseteq> X
\<lbrakk>s \<le> ?x; ?x \<le> 0\<rbrakk> \<Longrightarrow> ?x \<in> F.existence_ivl 0 x0
\<lbrakk>s \<le> ?x; ?x \<le> 0\<rbrakk> \<Longrightarrow> ?x \<in> G.existence_ivl 0 x0

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
have "flow0 s - Y s = - integral {s..0} (\<lambda>s. F s (flow0 s) - G s (Y s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. flow0 s - Y s = - integral {s..0} (\<lambda>s. F s (flow0 s) - G s (Y s))
[PROOF STEP]
using t0_s_in_existence \<open>s \<le> 0\<close>
[PROOF STATE]
proof (prove)
using this:
{s..0} \<subseteq> F.existence_ivl 0 x0
{s..0} \<subseteq> G.existence_ivl 0 x0
s \<le> 0

goal (1 subgoal):
 1. flow0 s - Y s = - integral {s..0} (\<lambda>s. F s (flow0 s) - G s (Y s))
[PROOF STEP]
by (simp add: flow0_def Y_def ivl_integral_def
               F.flow_fixed_point[OF s_in_existence(1)]
               G.flow_fixed_point[OF s_in_existence(2)]
               continuous_intros integrable_on_simps Henstock_Kurzweil_Integration.integral_diff)
[PROOF STATE]
proof (state)
this:
flow0 s - Y s = - integral {s..0} (\<lambda>s. F s (flow0 s) - G s (Y s))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
flow0 s - Y s = - integral {s..0} (\<lambda>s. F s (flow0 s) - G s (Y s))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
have "... = - integral {s..0} (\<lambda>s. (F s (flow0 s) - F s (Y s)) + (F s (Y s) - G s (Y s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - integral {s..0} (\<lambda>s. F s (flow0 s) - G s (Y s)) = - integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s) + (F s (Y s) - G s (Y s)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- integral {s..0} (\<lambda>s. F s (flow0 s) - G s (Y s)) = - integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s) + (F s (Y s) - G s (Y s)))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- integral {s..0} (\<lambda>s. F s (flow0 s) - G s (Y s)) = - integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s) + (F s (Y s) - G s (Y s)))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
have "... = - (integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s)) + integral {s..0} (\<lambda>s. F s (Y s) - G s (Y s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s) + (F s (Y s) - G s (Y s))) = - (integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s)) + integral {s..0} (\<lambda>s. F s (Y s) - G s (Y s)))
[PROOF STEP]
using t0_s_in_existence
[PROOF STATE]
proof (prove)
using this:
{s..0} \<subseteq> F.existence_ivl 0 x0
{s..0} \<subseteq> G.existence_ivl 0 x0

goal (1 subgoal):
 1. - integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s) + (F s (Y s) - G s (Y s))) = - (integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s)) + integral {s..0} (\<lambda>s. F s (Y s) - G s (Y s)))
[PROOF STEP]
by (subst Henstock_Kurzweil_Integration.integral_add) (simp_all add: integral_add flow0_def Y_def continuous_intros integrable_on_simps)
[PROOF STATE]
proof (state)
this:
- integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s) + (F s (Y s) - G s (Y s))) = - (integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s)) + integral {s..0} (\<lambda>s. F s (Y s) - G s (Y s)))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
flow0 s - Y s = - (integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s)) + integral {s..0} (\<lambda>s. F s (Y s) - G s (Y s)))
[PROOF STEP]
have "?u s \<le> norm (integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {s..0} (\<lambda>s. F s (Y s) - G s (Y s)))"
[PROOF STATE]
proof (prove)
using this:
flow0 s - Y s = - (integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s)) + integral {s..0} (\<lambda>s. F s (Y s) - G s (Y s)))

goal (1 subgoal):
 1. norm (flow0 s - Y s) \<le> norm (integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {s..0} (\<lambda>s. F s (Y s) - G s (Y s)))
[PROOF STEP]
by (metis (no_types, lifting) norm_minus_cancel norm_triangle_ineq)
[PROOF STATE]
proof (state)
this:
norm (flow0 s - Y s) \<le> norm (integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {s..0} (\<lambda>s. F s (Y s) - G s (Y s)))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (flow0 s - Y s) \<le> norm (integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {s..0} (\<lambda>s. F s (Y s) - G s (Y s)))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
have "... \<le> integral {s..0} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {s..0} (\<lambda>s. norm (F s (Y s) - G s (Y s)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {s..0} (\<lambda>s. F s (Y s) - G s (Y s))) \<le> integral {s..0} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {s..0} (\<lambda>s. norm (F s (Y s) - G s (Y s)))
[PROOF STEP]
using t0_s_in_existence
[PROOF STATE]
proof (prove)
using this:
{s..0} \<subseteq> F.existence_ivl 0 x0
{s..0} \<subseteq> G.existence_ivl 0 x0

goal (1 subgoal):
 1. norm (integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {s..0} (\<lambda>s. F s (Y s) - G s (Y s))) \<le> integral {s..0} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {s..0} (\<lambda>s. norm (F s (Y s) - G s (Y s)))
[PROOF STEP]
by (auto simp add: flow0_def Y_def intro!: continuous_intros continuous_on_imp_absolutely_integrable_on add_mono)
[PROOF STATE]
proof (state)
this:
norm (integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {s..0} (\<lambda>s. F s (Y s) - G s (Y s))) \<le> integral {s..0} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {s..0} (\<lambda>s. norm (F s (Y s) - G s (Y s)))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm (integral {s..0} (\<lambda>s. F s (flow0 s) - F s (Y s))) + norm (integral {s..0} (\<lambda>s. F s (Y s) - G s (Y s))) \<le> integral {s..0} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {s..0} (\<lambda>s. norm (F s (Y s) - G s (Y s)))

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
have "... \<le> integral {s..0} (\<lambda>s. K * ?u s) + integral {s..0} (\<lambda>s. e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {s..0} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {s..0} (\<lambda>s. norm (F s (Y s) - G s (Y s))) \<le> integral {s..0} (\<lambda>s. K * norm (flow0 s - Y s)) + integral {s..0} (\<lambda>s. e)
[PROOF STEP]
proof (rule add_mono[OF integral_le integral_le])
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) integrable_on {s..0}
 2. (\<lambda>s. K * norm (flow0 s - Y s)) integrable_on {s..0}
 3. \<And>x. x \<in> {s..0} \<Longrightarrow> norm (F x (flow0 x) - F x (Y x)) \<le> K * norm (flow0 x - Y x)
 4. (\<lambda>s. norm (F s (Y s) - G s (Y s))) integrable_on {s..0}
 5. (\<lambda>s. e) integrable_on {s..0}
 6. \<And>x. x \<in> {s..0} \<Longrightarrow> norm (F x (Y x) - G x (Y x)) \<le> e
[PROOF STEP]
show "norm (F x (flow0 x) - F x (Y x)) \<le> K * norm (flow0 x - Y x)" if "x\<in>{s..0}" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm (F x (flow0 x) - F x (Y x)) \<le> K * norm (flow0 x - Y x)
[PROOF STEP]
using F_lipschitz[unfolded lipschitz_on_def, THEN conjunct2]
            cont_statements(1,2,4) that
            t0_s_in_existence F_iv_defined
[PROOF STATE]
proof (prove)
using this:
?t1 \<in> J \<Longrightarrow> \<forall>x\<in>X. \<forall>y\<in>X. dist (F ?t1 x) (F ?t1 y) \<le> K * dist x y
0 \<in> T1
x0 \<in> X
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> G.flow ?t0.0 ?x0.0 ?t \<in> X
x \<in> {s..0}
{s..0} \<subseteq> F.existence_ivl 0 x0
{s..0} \<subseteq> G.existence_ivl 0 x0
0 \<in> T1
x0 \<in> X

goal (1 subgoal):
 1. norm (F x (flow0 x) - F x (Y x)) \<le> K * norm (flow0 x - Y x)
[PROOF STEP]
(* G.iv_defined *)
[PROOF STATE]
proof (prove)
using this:
?t1 \<in> J \<Longrightarrow> \<forall>x\<in>X. \<forall>y\<in>X. dist (F ?t1 x) (F ?t1 y) \<le> K * dist x y
0 \<in> T1
x0 \<in> X
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> G.flow ?t0.0 ?x0.0 ?t \<in> X
x \<in> {s..0}
{s..0} \<subseteq> F.existence_ivl 0 x0
{s..0} \<subseteq> G.existence_ivl 0 x0
0 \<in> T1
x0 \<in> X

goal (1 subgoal):
 1. norm (F x (flow0 x) - F x (Y x)) \<le> K * norm (flow0 x - Y x)
[PROOF STEP]
by (metis F_lipschitz flow0_def Y_def \<open>{s..0} \<subseteq> J\<close> lipschitz_on_normD F.flow_in_domain
            G.flow_in_domain subsetCE)
[PROOF STATE]
proof (state)
this:
?x \<in> {s..0} \<Longrightarrow> norm (F ?x (flow0 ?x) - F ?x (Y ?x)) \<le> K * norm (flow0 ?x - Y ?x)

goal (5 subgoals):
 1. (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) integrable_on {s..0}
 2. (\<lambda>s. K * norm (flow0 s - Y s)) integrable_on {s..0}
 3. (\<lambda>s. norm (F s (Y s) - G s (Y s))) integrable_on {s..0}
 4. (\<lambda>s. e) integrable_on {s..0}
 5. \<And>x. x \<in> {s..0} \<Longrightarrow> norm (F x (Y x) - G x (Y x)) \<le> e
[PROOF STEP]
show "\<And>x. x \<in> {s..0} \<Longrightarrow> norm (F x (Y x) - G x (Y x)) \<le> e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> {s..0} \<Longrightarrow> norm (F x (Y x) - G x (Y x)) \<le> e
[PROOF STEP]
using F_G_norm_ineq Y_def \<open>{s..0} \<subseteq> J\<close> cont_statements(5) subset_iff t0_s_in_existence(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t \<in> J; ?x \<in> X\<rbrakk> \<Longrightarrow> norm (F ?t ?x - G ?t ?x) < e
Y ?t = G.flow 0 x0 ?t
{s..0} \<subseteq> J
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> ?t \<in> T1
(?A \<subseteq> ?B) = (\<forall>t. t \<in> ?A \<longrightarrow> t \<in> ?B)
{s..0} \<subseteq> G.existence_ivl 0 x0

goal (1 subgoal):
 1. \<And>x. x \<in> {s..0} \<Longrightarrow> norm (F x (Y x) - G x (Y x)) \<le> e
[PROOF STEP]
using Y_def \<open>{s..0} \<subseteq> J\<close> cont_statements(5) subset_iff G.flow_in_domain
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?t \<in> J; ?x \<in> X\<rbrakk> \<Longrightarrow> norm (F ?t ?x - G ?t ?x) < e
Y ?t = G.flow 0 x0 ?t
{s..0} \<subseteq> J
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> ?t \<in> T1
(?A \<subseteq> ?B) = (\<forall>t. t \<in> ?A \<longrightarrow> t \<in> ?B)
{s..0} \<subseteq> G.existence_ivl 0 x0
Y ?t = G.flow 0 x0 ?t
{s..0} \<subseteq> J
?t \<in> F.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> ?t \<in> T1
(?A \<subseteq> ?B) = (\<forall>t. t \<in> ?A \<longrightarrow> t \<in> ?B)
?t \<in> G.existence_ivl ?t0.0 ?x0.0 \<Longrightarrow> G.flow ?t0.0 ?x0.0 ?t \<in> X

goal (1 subgoal):
 1. \<And>x. x \<in> {s..0} \<Longrightarrow> norm (F x (Y x) - G x (Y x)) \<le> e
[PROOF STEP]
by (metis eucl_less_le_not_le)
[PROOF STATE]
proof (state)
this:
?x \<in> {s..0} \<Longrightarrow> norm (F ?x (Y ?x) - G ?x (Y ?x)) \<le> e

goal (4 subgoals):
 1. (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) integrable_on {s..0}
 2. (\<lambda>s. K * norm (flow0 s - Y s)) integrable_on {s..0}
 3. (\<lambda>s. norm (F s (Y s) - G s (Y s))) integrable_on {s..0}
 4. (\<lambda>s. e) integrable_on {s..0}
[PROOF STEP]
qed (simp_all add: t0_s_in_existence continuous_intros integrable_on_simps flow0_def Y_def)
[PROOF STATE]
proof (state)
this:
integral {s..0} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {s..0} (\<lambda>s. norm (F s (Y s) - G s (Y s))) \<le> integral {s..0} (\<lambda>s. K * norm (flow0 s - Y s)) + integral {s..0} (\<lambda>s. e)

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
integral {s..0} (\<lambda>s. norm (F s (flow0 s) - F s (Y s))) + integral {s..0} (\<lambda>s. norm (F s (Y s) - G s (Y s))) \<le> integral {s..0} (\<lambda>s. K * norm (flow0 s - Y s)) + integral {s..0} (\<lambda>s. e)

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
have "... = K * integral {s..0} (\<lambda>s. ?u s + e / K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integral {s..0} (\<lambda>s. K * norm (flow0 s - Y s)) + integral {s..0} (\<lambda>s. e) = K * integral {s..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
[PROOF STEP]
using K_pos t0_s_in_existence
[PROOF STATE]
proof (prove)
using this:
0 < K
{s..0} \<subseteq> F.existence_ivl 0 x0
{s..0} \<subseteq> G.existence_ivl 0 x0

goal (1 subgoal):
 1. integral {s..0} (\<lambda>s. K * norm (flow0 s - Y s)) + integral {s..0} (\<lambda>s. e) = K * integral {s..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
[PROOF STEP]
by (simp_all add: algebra_simps Henstock_Kurzweil_Integration.integral_add t0_s_in_existence continuous_intros integrable_on_simps flow0_def Y_def)
[PROOF STATE]
proof (state)
this:
integral {s..0} (\<lambda>s. K * norm (flow0 s - Y s)) + integral {s..0} (\<lambda>s. e) = K * integral {s..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)

goal (4 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> norm (flow0 ta - Y ta) + e / K \<le> e / K + K * integral {ta..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
 2. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 3. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 4. 0 < e / K
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
norm (flow0 s - Y s) \<le> K * integral {s..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
[PROOF STEP]
show "?u s + e / K \<le> e / K + K * integral {s..0} (\<lambda>s. ?u s + e / K)"
[PROOF STATE]
proof (prove)
using this:
norm (flow0 s - Y s) \<le> K * integral {s..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)

goal (1 subgoal):
 1. norm (flow0 s - Y s) + e / K \<le> e / K + K * integral {s..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
norm (flow0 s - Y s) + e / K \<le> e / K + K * integral {s..0} (\<lambda>s. norm (flow0 s - Y s) + e / K)

goal (3 subgoals):
 1. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 2. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 3. 0 < e / K
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
 2. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 3. 0 < e / K
[PROOF STEP]
show "continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
[PROOF STEP]
using t0_t_in_J J_subset G.ivl_subset_existence_ivl'[OF tG] F_iv_defined
[PROOF STATE]
proof (prove)
using this:
{t..0} \<subseteq> J
J \<subseteq> F.existence_ivl 0 x0
{t..0} \<subseteq> G.existence_ivl 0 x0
0 \<in> T1
x0 \<in> X

goal (1 subgoal):
 1. continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)
[PROOF STEP]
by (auto simp add: flow0_def Y_def intro!: continuous_intros)
[PROOF STATE]
proof (state)
this:
continuous_on {t..0} (\<lambda>t. norm (flow0 t - Y t) + e / K)

goal (2 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 2. 0 < e / K
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 2. 0 < e / K
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 2. 0 < e / K
[PROOF STEP]
assume "t \<le> s" "s \<le> 0"
[PROOF STATE]
proof (state)
this:
t \<le> s
s \<le> 0

goal (2 subgoals):
 1. \<And>ta. \<lbrakk>t \<le> ta; ta \<le> 0\<rbrakk> \<Longrightarrow> 0 \<le> norm (flow0 ta - Y ta) + e / K
 2. 0 < e / K
[PROOF STEP]
show "0 \<le> norm (flow0 s - Y s) + e / K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> norm (flow0 s - Y s) + e / K
[PROOF STEP]
using e_pos K_pos
[PROOF STATE]
proof (prove)
using this:
0 < e
0 < K

goal (1 subgoal):
 1. 0 \<le> norm (flow0 s - Y s) + e / K
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> norm (flow0 s - Y s) + e / K

goal (1 subgoal):
 1. 0 < e / K
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < e / K
[PROOF STEP]
show "0 < e / K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < e / K
[PROOF STEP]
using e_pos K_pos
[PROOF STATE]
proof (prove)
using this:
0 < e
0 < K

goal (1 subgoal):
 1. 0 < e / K
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < e / K

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
norm (flow0 t - Y t) + e / K \<le> e / K * exp (- K * t)

goal (1 subgoal):
 1. \<not> 0 \<le> t \<Longrightarrow> norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
norm (flow0 t - Y t) + e / K \<le> e / K * exp (- K * t)

goal (1 subgoal):
 1. norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
norm (flow0 t - Y t) \<le> e / K * (exp (K * \<bar>t\<bar>) - 1)

goal:
No subgoals!
[PROOF STEP]
qed