[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


[STATEMENT]
lemma Q_infer1:
  "infer1 pq X = {(fst pq, r) | q r. (q, r) |\<in>| eps A \<and> q = snd pq} \<union>
    {(r, snd pq) |r p'. (r, p') \<in> X \<and> p' = fst pq} \<union>
    {(fst pq, r) |q' r. (q', r) \<in> (insert pq X) \<and> q' = snd pq}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infer1 pq X = {uu_. \<exists>q r. uu_ = (fst pq, r) \<and> (q, r) |\<in>| eps A \<and> q = snd pq} \<union> {uu_. \<exists>r p'. uu_ = (r, snd pq) \<and> (r, p') \<in> X \<and> p' = fst pq} \<union> {uu_. \<exists>q' r. uu_ = (fst pq, r) \<and> (q', r) \<in> insert pq X \<and> q' = snd pq}
[PROOF STEP]
unfolding Q_inf_rules_def horn_infer1_union
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. horn.infer1 {uu_. \<exists>f ps p i. uu_ = [] \<rightarrow>\<^sub>h (ps ! i, p) \<and> lift_None_Some f ps \<rightarrow> p |\<in>| rules A \<and> i < length ps} pq X \<union> horn.infer1 {[(p, q)] \<rightarrow>\<^sub>h (p, r) |p q r. (q, r) |\<in>| eps A} pq X \<union> horn.infer1 {[(p, q), (q, r)] \<rightarrow>\<^sub>h (p, r) |p q r. True} pq X = {uu_. \<exists>q r. uu_ = (fst pq, r) \<and> (q, r) |\<in>| eps A \<and> q = snd pq} \<union> {uu_. \<exists>r p'. uu_ = (r, snd pq) \<and> (r, p') \<in> X \<and> p' = fst pq} \<union> {uu_. \<exists>q' r. uu_ = (fst pq, r) \<and> (q', r) \<in> insert pq X \<and> q' = snd pq}
[PROOF STEP]
by (auto simp: horn.infer1_def simp flip: ex_simps(1)) force+


[STATEMENT]
lemma bst_joinR:
  "\<lbrakk>bst l; bst r; \<forall>x\<in>set_tree l. x < a; \<forall>y\<in>set_tree r. a < y \<rbrakk>
  \<Longrightarrow> bst (joinR l a r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Tree2.bst l; Tree2.bst r; \<forall>x\<in>Tree2.set_tree l. x < a; \<forall>y\<in>Tree2.set_tree r. a < y\<rbrakk> \<Longrightarrow> Tree2.bst (joinR l a r)
[PROOF STEP]
proof(induction l a r rule: joinR.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l x r. \<lbrakk>\<And>x21 x22 x23 xa y. \<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>x21, x22, x23\<rangle>; (xa, y) = x22; y = Red; Tree2.bst x23; Tree2.bst r; \<forall>xa\<in>Tree2.set_tree x23. xa < x; Ball (Tree2.set_tree r) ((<) x)\<rbrakk> \<Longrightarrow> Tree2.bst (joinR x23 x r); \<And>x21 x22 x23 xa y. \<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>x21, x22, x23\<rangle>; (xa, y) = x22; y = Black; Tree2.bst x23; Tree2.bst r; \<forall>xa\<in>Tree2.set_tree x23. xa < x; Ball (Tree2.set_tree r) ((<) x)\<rbrakk> \<Longrightarrow> Tree2.bst (joinR x23 x r); Tree2.bst l; Tree2.bst r; \<forall>xa\<in>Tree2.set_tree l. xa < x; Ball (Tree2.set_tree r) ((<) x)\<rbrakk> \<Longrightarrow> Tree2.bst (joinR l x r)
[PROOF STEP]
case (1 l a r)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>?x21.0, ?x22.0, ?x23.0\<rangle>; (?xa, ?y) = ?x22.0; ?y = Red; Tree2.bst ?x23.0; Tree2.bst r; \<forall>x\<in>Tree2.set_tree ?x23.0. x < a; \<forall>a\<in>Tree2.set_tree r. a < a\<rbrakk> \<Longrightarrow> Tree2.bst (joinR ?x23.0 a r)
\<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>?x21.0, ?x22.0, ?x23.0\<rangle>; (?xa, ?y) = ?x22.0; ?y = Black; Tree2.bst ?x23.0; Tree2.bst r; \<forall>x\<in>Tree2.set_tree ?x23.0. x < a; \<forall>a\<in>Tree2.set_tree r. a < a\<rbrakk> \<Longrightarrow> Tree2.bst (joinR ?x23.0 a r)
Tree2.bst l
Tree2.bst r
\<forall>x\<in>Tree2.set_tree l. x < a
\<forall>a\<in>Tree2.set_tree r. a < a

goal (1 subgoal):
 1. \<And>l x r. \<lbrakk>\<And>x21 x22 x23 xa y. \<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>x21, x22, x23\<rangle>; (xa, y) = x22; y = Red; Tree2.bst x23; Tree2.bst r; \<forall>xa\<in>Tree2.set_tree x23. xa < x; Ball (Tree2.set_tree r) ((<) x)\<rbrakk> \<Longrightarrow> Tree2.bst (joinR x23 x r); \<And>x21 x22 x23 xa y. \<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>x21, x22, x23\<rangle>; (xa, y) = x22; y = Black; Tree2.bst x23; Tree2.bst r; \<forall>xa\<in>Tree2.set_tree x23. xa < x; Ball (Tree2.set_tree r) ((<) x)\<rbrakk> \<Longrightarrow> Tree2.bst (joinR x23 x r); Tree2.bst l; Tree2.bst r; \<forall>xa\<in>Tree2.set_tree l. xa < x; Ball (Tree2.set_tree r) ((<) x)\<rbrakk> \<Longrightarrow> Tree2.bst (joinR l x r)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>?x21.0, ?x22.0, ?x23.0\<rangle>; (?xa, ?y) = ?x22.0; ?y = Red; Tree2.bst ?x23.0; Tree2.bst r; \<forall>x\<in>Tree2.set_tree ?x23.0. x < a; \<forall>a\<in>Tree2.set_tree r. a < a\<rbrakk> \<Longrightarrow> Tree2.bst (joinR ?x23.0 a r)
\<lbrakk>\<not> bheight l \<le> bheight r; l = \<langle>?x21.0, ?x22.0, ?x23.0\<rangle>; (?xa, ?y) = ?x22.0; ?y = Black; Tree2.bst ?x23.0; Tree2.bst r; \<forall>x\<in>Tree2.set_tree ?x23.0. x < a; \<forall>a\<in>Tree2.set_tree r. a < a\<rbrakk> \<Longrightarrow> Tree2.bst (joinR ?x23.0 a r)
Tree2.bst l
Tree2.bst r
\<forall>x\<in>Tree2.set_tree l. x < a
\<forall>a\<in>Tree2.set_tree r. a < a

goal (1 subgoal):
 1. Tree2.bst (joinR l a r)
[PROOF STEP]
by(auto simp: set_baliR joinR.simps[of l a r] set_joinR ball_Un intro!: bst_baliR
        split!: tree.splits color.splits)
[PROOF STATE]
proof (state)
this:
Tree2.bst (joinR l a r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lookup_eqvt[eqvt]:
  fixes pi::"name prm"
  and   \<theta>::"(name\<times>trm) list"
  and   x::"name"
  shows "pi \<bullet> (lookup \<theta> x) = lookup (pi \<bullet> \<theta>) (pi \<bullet> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pi \<bullet> lookup \<theta> x = lookup (pi \<bullet> \<theta>) (pi \<bullet> x)
[PROOF STEP]
by (induct \<theta>) (auto simp add: eqvts)


[STATEMENT]
lemma set_take_two:
  assumes "card A \<ge> 2"
  obtains x y where "x \<in> A" "y \<in> A" "x \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
2 \<le> card A
[PROOF STEP]
obtain k where "card A = Suc (Suc k)"
[PROOF STATE]
proof (prove)
using this:
2 \<le> card A

goal (1 subgoal):
 1. (\<And>k. card A = Suc (Suc k) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: le_iff_add)
[PROOF STATE]
proof (state)
this:
card A = Suc (Suc k)

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from card_eq_SucD[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = Suc k \<and> (Suc k = 0 \<longrightarrow> B = {})
[PROOF STEP]
obtain x B where x: "A = insert x B" "x \<notin> B" "card B = Suc k"
[PROOF STATE]
proof (prove)
using this:
\<exists>b B. A = insert b B \<and> b \<notin> B \<and> card B = Suc k \<and> (Suc k = 0 \<longrightarrow> B = {})

goal (1 subgoal):
 1. (\<And>x B. \<lbrakk>A = insert x B; x \<notin> B; card B = Suc k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = insert x B
x \<notin> B
card B = Suc k

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from card_eq_SucD[OF this(3)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>b Ba. B = insert b Ba \<and> b \<notin> Ba \<and> card Ba = k \<and> (k = 0 \<longrightarrow> Ba = {})
[PROOF STEP]
obtain y where y: "y \<in> B"
[PROOF STATE]
proof (prove)
using this:
\<exists>b Ba. B = insert b Ba \<and> b \<notin> Ba \<and> card Ba = k \<and> (k = 0 \<longrightarrow> Ba = {})

goal (1 subgoal):
 1. (\<And>y. y \<in> B \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> B

goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> A; y \<in> A; x \<noteq> y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from x y
[PROOF STATE]
proof (chain)
picking this:
A = insert x B
x \<notin> B
card B = Suc k
y \<in> B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A = insert x B
x \<notin> B
card B = Suc k
y \<in> B

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by - (rule that[of x y], auto)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hausdorff_distance_closures [simp]:
  "hausdorff_distance (closure A) (closure B) = hausdorff_distance A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
proof (cases "A = {} \<or> B = {} \<or> (\<not>(bounded A)) \<or> (\<not>(bounded B))")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
 2. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B

goal (2 subgoals):
 1. A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
 2. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B
[PROOF STEP]
have *: "hausdorff_distance A B = 0"
[PROOF STATE]
proof (prove)
using this:
A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B

goal (1 subgoal):
 1. hausdorff_distance A B = 0
[PROOF STEP]
unfolding hausdorff_distance_def
[PROOF STATE]
proof (prove)
using this:
A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B

goal (1 subgoal):
 1. (if A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B then 0 else max (SUP x\<in>A. infdist x B) (SUP x\<in>B. infdist x A)) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance A B = 0

goal (2 subgoals):
 1. A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
 2. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "closure A = {} \<or> (\<not>(bounded (closure A))) \<or> closure B = {} \<or> (\<not>(bounded (closure B)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure A = {} \<or> \<not> bounded (closure A) \<or> closure B = {} \<or> \<not> bounded (closure B)
[PROOF STEP]
using True bounded_subset closure_subset
[PROOF STATE]
proof (prove)
using this:
A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B
\<lbrakk>bounded ?T; ?S \<subseteq> ?T\<rbrakk> \<Longrightarrow> bounded ?S
?S \<subseteq> closure ?S

goal (1 subgoal):
 1. closure A = {} \<or> \<not> bounded (closure A) \<or> closure B = {} \<or> \<not> bounded (closure B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closure A = {} \<or> \<not> bounded (closure A) \<or> closure B = {} \<or> \<not> bounded (closure B)

goal (2 subgoals):
 1. A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
 2. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closure A = {} \<or> \<not> bounded (closure A) \<or> closure B = {} \<or> \<not> bounded (closure B)
[PROOF STEP]
have "hausdorff_distance (closure A) (closure B) = 0"
[PROOF STATE]
proof (prove)
using this:
closure A = {} \<or> \<not> bounded (closure A) \<or> closure B = {} \<or> \<not> bounded (closure B)

goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) = 0
[PROOF STEP]
unfolding hausdorff_distance_def
[PROOF STATE]
proof (prove)
using this:
closure A = {} \<or> \<not> bounded (closure A) \<or> closure B = {} \<or> \<not> bounded (closure B)

goal (1 subgoal):
 1. (if closure A = {} \<or> closure B = {} \<or> \<not> bounded (closure A) \<or> \<not> bounded (closure B) then 0 else max (SUP x\<in>closure A. infdist x (closure B)) (SUP x\<in>closure B. infdist x (closure A))) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) (closure B) = 0

goal (2 subgoals):
 1. A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
 2. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hausdorff_distance (closure A) (closure B) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (closure A) (closure B) = 0

goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (closure A) (closure B) = 0
hausdorff_distance A B = 0

goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) (closure B) = hausdorff_distance A B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B)
[PROOF STEP]
have H: "A \<noteq> {}" "B \<noteq> {}" "bounded A" "bounded B"
[PROOF STATE]
proof (prove)
using this:
\<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B)

goal (1 subgoal):
 1. (A \<noteq> {} &&& B \<noteq> {}) &&& bounded A &&& bounded B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<noteq> {}
B \<noteq> {}
bounded A
bounded B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<noteq> {}
B \<noteq> {}
bounded A
bounded B
[PROOF STEP]
have H2: "closure A \<noteq> {}" "closure B \<noteq> {}" "bounded (closure A)" "bounded (closure B)"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
B \<noteq> {}
bounded A
bounded B

goal (1 subgoal):
 1. (closure A \<noteq> {} &&& closure B \<noteq> {}) &&& bounded (closure A) &&& bounded (closure B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
closure A \<noteq> {}
closure B \<noteq> {}
bounded (closure A)
bounded (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "hausdorff_distance A B \<le> hausdorff_distance A (closure A) + hausdorff_distance (closure A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance A B \<le> hausdorff_distance A (closure A) + hausdorff_distance (closure A) B
[PROOF STEP]
apply (rule hausdorff_distance_triangle)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. closure A \<noteq> {}
 2. bounded (closure A)
[PROOF STEP]
using H H2
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
B \<noteq> {}
bounded A
bounded B
closure A \<noteq> {}
closure B \<noteq> {}
bounded (closure A)
bounded (closure B)

goal (2 subgoals):
 1. closure A \<noteq> {}
 2. bounded (closure A)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance A B \<le> hausdorff_distance A (closure A) + hausdorff_distance (closure A) B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hausdorff_distance A B \<le> hausdorff_distance A (closure A) + hausdorff_distance (closure A) B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "... = hausdorff_distance (closure A) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance A (closure A) + hausdorff_distance (closure A) B = hausdorff_distance (closure A) B
[PROOF STEP]
using hausdorff_distance_closure
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance ?A (closure ?A) = 0

goal (1 subgoal):
 1. hausdorff_distance A (closure A) + hausdorff_distance (closure A) B = hausdorff_distance (closure A) B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance A (closure A) + hausdorff_distance (closure A) B = hausdorff_distance (closure A) B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hausdorff_distance A (closure A) + hausdorff_distance (closure A) B = hausdorff_distance (closure A) B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "... \<le> hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (closure A) B \<le> hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B
[PROOF STEP]
apply (rule hausdorff_distance_triangle)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. closure B \<noteq> {}
 2. bounded (closure B)
[PROOF STEP]
using H H2
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
B \<noteq> {}
bounded A
bounded B
closure A \<noteq> {}
closure B \<noteq> {}
bounded (closure A)
bounded (closure B)

goal (2 subgoals):
 1. closure B \<noteq> {}
 2. bounded (closure B)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) B \<le> hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) B \<le> hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "... = hausdorff_distance (closure A) (closure B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B = hausdorff_distance (closure A) (closure B)
[PROOF STEP]
using hausdorff_distance_closure
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance ?A (closure ?A) = 0

goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B = hausdorff_distance (closure A) (closure B)
[PROOF STEP]
by (auto simp add: hausdorff_distance_sym)
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) (closure B) + hausdorff_distance (closure B) B = hausdorff_distance (closure A) (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
hausdorff_distance A B \<le> hausdorff_distance (closure A) (closure B)
[PROOF STEP]
have *: "hausdorff_distance A B \<le> hausdorff_distance (closure A) (closure B)"
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance A B \<le> hausdorff_distance (closure A) (closure B)

goal (1 subgoal):
 1. hausdorff_distance A B \<le> hausdorff_distance (closure A) (closure B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hausdorff_distance A B \<le> hausdorff_distance (closure A) (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance (closure A) A + hausdorff_distance A (closure B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance (closure A) A + hausdorff_distance A (closure B)
[PROOF STEP]
apply (rule hausdorff_distance_triangle)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. A \<noteq> {}
 2. bounded A
[PROOF STEP]
using H H2
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
B \<noteq> {}
bounded A
bounded B
closure A \<noteq> {}
closure B \<noteq> {}
bounded (closure A)
bounded (closure B)

goal (2 subgoals):
 1. A \<noteq> {}
 2. bounded A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance (closure A) A + hausdorff_distance A (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance (closure A) A + hausdorff_distance A (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "... = hausdorff_distance A (closure B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance (closure A) A + hausdorff_distance A (closure B) = hausdorff_distance A (closure B)
[PROOF STEP]
using hausdorff_distance_closure
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance ?A (closure ?A) = 0

goal (1 subgoal):
 1. hausdorff_distance (closure A) A + hausdorff_distance A (closure B) = hausdorff_distance A (closure B)
[PROOF STEP]
by (auto simp add: hausdorff_distance_sym)
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) A + hausdorff_distance A (closure B) = hausdorff_distance A (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) A + hausdorff_distance A (closure B) = hausdorff_distance A (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "... \<le> hausdorff_distance A B + hausdorff_distance B (closure B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance A (closure B) \<le> hausdorff_distance A B + hausdorff_distance B (closure B)
[PROOF STEP]
apply (rule hausdorff_distance_triangle)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. B \<noteq> {}
 2. bounded B
[PROOF STEP]
using H H2
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
B \<noteq> {}
bounded A
bounded B
closure A \<noteq> {}
closure B \<noteq> {}
bounded (closure A)
bounded (closure B)

goal (2 subgoals):
 1. B \<noteq> {}
 2. bounded B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance A (closure B) \<le> hausdorff_distance A B + hausdorff_distance B (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hausdorff_distance A (closure B) \<le> hausdorff_distance A B + hausdorff_distance B (closure B)

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
have "... = hausdorff_distance A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hausdorff_distance A B + hausdorff_distance B (closure B) = hausdorff_distance A B
[PROOF STEP]
using hausdorff_distance_closure
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance ?A (closure ?A) = 0

goal (1 subgoal):
 1. hausdorff_distance A B + hausdorff_distance B (closure B) = hausdorff_distance A B
[PROOF STEP]
by (auto simp add: hausdorff_distance_sym)
[PROOF STATE]
proof (state)
this:
hausdorff_distance A B + hausdorff_distance B (closure B) = hausdorff_distance A B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B
[PROOF STEP]
have "hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B"
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B

goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B

goal (1 subgoal):
 1. \<not> (A = {} \<or> B = {} \<or> \<not> bounded A \<or> \<not> bounded B) \<Longrightarrow> hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B

goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
hausdorff_distance (closure A) (closure B) \<le> hausdorff_distance A B
hausdorff_distance A B \<le> hausdorff_distance (closure A) (closure B)

goal (1 subgoal):
 1. hausdorff_distance (closure A) (closure B) = hausdorff_distance A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hausdorff_distance (closure A) (closure B) = hausdorff_distance A B

goal:
No subgoals!
[PROOF STEP]
qed