diff --git a/thys/Hybrid_Systems_VCs/HS_ODEs.thy b/thys/Hybrid_Systems_VCs/HS_ODEs.thy
--- a/thys/Hybrid_Systems_VCs/HS_ODEs.thy
+++ b/thys/Hybrid_Systems_VCs/HS_ODEs.thy
@@ -1,571 +1,636 @@
 (*  Title:       ODEs and Dynamical Systems for HS verification
     Author:      Jonathan Julián Huerta y Munive, 2019
     Maintainer:  Jonathan Julián Huerta y Munive <jjhuertaymunive1@sheffield.ac.uk>
 *)
 
 section \<open> Ordinary Differential Equations \<close>
 
 text \<open>Vector fields @{text "f::real \<Rightarrow> 'a \<Rightarrow> ('a::real_normed_vector)"} represent systems 
 of ordinary differential equations (ODEs). Picard-Lindeloef's theorem guarantees existence 
 and uniqueness of local solutions to initial value problems involving Lipschitz continuous 
 vector fields. A (local) flow @{text "\<phi>::real \<Rightarrow> 'a \<Rightarrow> ('a::real_normed_vector)"} for such 
 a system is the function that maps initial conditions to their unique solutions. In dynamical 
 systems, the set of all points @{text "\<phi> t s::'a"} for a fixed @{text "s::'a"} is the flow's 
 orbit. If the orbit of each @{text "s \<in> I"} is conatined in @{text I}, then @{text I} is an 
 invariant set of this system. This section formalises these concepts with a focus on hybrid 
 systems (HS) verification.\<close>
 
 theory HS_ODEs
   imports "HS_Preliminaries"
 begin
 
 subsection \<open> Initial value problems and orbits \<close>
 
 notation image ("\<P>")
 
 lemma image_le_pred[simp]: "(\<P> f A \<subseteq> {s. G s}) = (\<forall>x\<in>A. G (f x))"
   unfolding image_def by force
 
 definition ivp_sols :: "(real \<Rightarrow> 'a \<Rightarrow> ('a::real_normed_vector)) \<Rightarrow> real set \<Rightarrow> 'a set \<Rightarrow> 
   real \<Rightarrow> 'a \<Rightarrow> (real \<Rightarrow> 'a) set" ("Sols")
   where "Sols f T S t\<^sub>0 s = {X |X. (D X = (\<lambda>t. f t (X t)) on T) \<and> X t\<^sub>0 = s \<and> X \<in> T \<rightarrow> S}"
 
 lemma ivp_solsI: 
   assumes "D X = (\<lambda>t. f t (X t)) on T" "X t\<^sub>0 = s" "X \<in> T \<rightarrow> S"
   shows "X \<in> Sols f T S t\<^sub>0 s"
   using assms unfolding ivp_sols_def by blast
 
 lemma ivp_solsD:
   assumes "X \<in> Sols f T S t\<^sub>0 s"
   shows "D X = (\<lambda>t. f t (X t)) on T"
     and "X t\<^sub>0 = s" and "X \<in> T \<rightarrow> S"
   using assms unfolding ivp_sols_def by auto
 
 abbreviation "down T t \<equiv> {\<tau>\<in>T. \<tau>\<le> t}"
 
 definition g_orbit :: "(('a::ord) \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set" ("\<gamma>")
   where "\<gamma> X G T = \<Union>{\<P> X (down T t) |t. \<P> X (down T t) \<subseteq> {s. G s}}"
 
 lemma g_orbit_eq: 
   fixes X::"('a::preorder) \<Rightarrow> 'b"
   shows "\<gamma> X G T = {X t |t. t \<in> T \<and> (\<forall>\<tau>\<in>down T t. G (X \<tau>))}"
   unfolding g_orbit_def apply safe
   using le_left_mono by blast auto
 
 definition g_orbital :: "('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> real set \<Rightarrow> 'a set \<Rightarrow> real \<Rightarrow> 
   ('a::real_normed_vector) \<Rightarrow> 'a set" 
   where "g_orbital f G T S t\<^sub>0 s = \<Union>{\<gamma> X G T |X. X \<in> ivp_sols (\<lambda>t. f) T S t\<^sub>0 s}"
 
 lemma g_orbital_eq: "g_orbital f G T S t\<^sub>0 s = 
   {X t |t X. t \<in> T \<and> \<P> X (down T t) \<subseteq> {s. G s} \<and> X \<in> Sols (\<lambda>t. f) T S t\<^sub>0 s }" 
   unfolding g_orbital_def ivp_sols_def g_orbit_eq image_le_pred by auto
 
 lemma g_orbitalI:
   assumes "X \<in> Sols (\<lambda>t. f) T S t\<^sub>0 s"
     and "t \<in> T" and "(\<P> X (down T t) \<subseteq> {s. G s})"
   shows "X t \<in> g_orbital f G T S t\<^sub>0 s"
   using assms unfolding g_orbital_eq(1) by auto
 
 lemma g_orbitalD:
   assumes "s' \<in> g_orbital f G T S t\<^sub>0 s"
   obtains X and t where "X \<in> Sols (\<lambda>t. f) T S t\<^sub>0 s"
   and "X t = s'" and "t \<in> T" and "(\<P> X (down T t) \<subseteq> {s. G s})"
   using assms unfolding g_orbital_def g_orbit_eq by auto
 
 no_notation g_orbit ("\<gamma>")
 
 
 subsection \<open> Differential Invariants \<close>
 
 definition diff_invariant :: "('a \<Rightarrow> bool) \<Rightarrow> (('a::real_normed_vector) \<Rightarrow> 'a) \<Rightarrow> real set \<Rightarrow> 
   'a set \<Rightarrow> real \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" 
   where "diff_invariant I f T S t\<^sub>0 G \<equiv> (\<Union> \<circ> (\<P> (g_orbital f G T S t\<^sub>0))) {s. I s} \<subseteq> {s. I s}"
 
 lemma diff_invariant_eq: "diff_invariant I f T S t\<^sub>0 G = 
   (\<forall>s. I s \<longrightarrow> (\<forall>X\<in>Sols (\<lambda>t. f) T S t\<^sub>0 s. (\<forall>t\<in>T.(\<forall>\<tau>\<in>(down T t). G (X \<tau>)) \<longrightarrow> I (X t))))"
   unfolding diff_invariant_def g_orbital_eq image_le_pred by auto
 
 lemma diff_inv_eq_inv_set:
   "diff_invariant I f T S t\<^sub>0 G = (\<forall>s. I s \<longrightarrow> (g_orbital f G T S t\<^sub>0 s) \<subseteq> {s. I s})"
   unfolding diff_invariant_eq g_orbital_eq image_le_pred by auto
 
 named_theorems diff_invariant_rules "rules for certifying differential invariants."
 
 lemma diff_invariant_eq_rule [diff_invariant_rules]:
   assumes Thyp: "is_interval T" "t\<^sub>0 \<in> T"
     and "\<forall>X. (D X = (\<lambda>\<tau>. f (X \<tau>)) on T) \<longrightarrow> (D (\<lambda>\<tau>. \<mu> (X \<tau>) - \<nu> (X \<tau>)) = ((*\<^sub>R) 0) on T)"
   shows "diff_invariant (\<lambda>s. \<mu> s = \<nu> s) f T S t\<^sub>0 G"
 proof(simp add: diff_invariant_eq ivp_sols_def, clarsimp)
   fix X \<tau> assume tHyp:"\<tau> \<in> T" and x_ivp:"D X = (\<lambda>\<tau>. f (X \<tau>)) on T" "\<mu> (X t\<^sub>0) = \<nu> (X t\<^sub>0)" 
   hence obs1: "\<forall>t\<in>T. D (\<lambda>\<tau>. \<mu> (X \<tau>) - \<nu> (X \<tau>)) \<mapsto> (\<lambda>\<tau>. \<tau> *\<^sub>R 0) at t within T"
     using assms by (auto simp: has_vderiv_on_def has_vector_derivative_def)
   have obs2: "{t\<^sub>0--\<tau>} \<subseteq> T"
     using closed_segment_subset_interval tHyp Thyp by blast
   hence "D (\<lambda>\<tau>. \<mu> (X \<tau>) - \<nu> (X \<tau>)) = (\<lambda>\<tau>. \<tau> *\<^sub>R 0) on {t\<^sub>0--\<tau>}"
     using obs1 x_ivp by (auto intro!: has_derivative_subset[OF _ obs2]
         simp: has_vderiv_on_def has_vector_derivative_def)
   then obtain t where "t \<in> {t\<^sub>0--\<tau>}" and "\<mu> (X \<tau>) - \<nu> (X \<tau>) - (\<mu> (X t\<^sub>0) - \<nu> (X t\<^sub>0)) = (\<tau> - t\<^sub>0) * t *\<^sub>R 0"
     using mvt_very_simple_closed_segmentE by blast
   thus "\<mu> (X \<tau>) = \<nu> (X \<tau>)" 
     by (simp add: x_ivp(2))
 qed
 
 lemma diff_invariant_leq_rule [diff_invariant_rules]:
   fixes \<mu>::"'a::banach \<Rightarrow> real"
   assumes Thyp: "is_interval T" "t\<^sub>0 \<in> T"
     and "\<forall>X. (D X = (\<lambda>\<tau>. f (X \<tau>)) on T) \<longrightarrow> (\<forall>\<tau>\<in>T. (\<tau> > t\<^sub>0 \<longrightarrow> \<mu>' (X \<tau>) \<ge> \<nu>' (X \<tau>)) \<and> 
   (\<tau> < t\<^sub>0 \<longrightarrow> \<mu>' (X \<tau>) \<le> \<nu>' (X \<tau>))) \<and> (D (\<lambda>\<tau>. \<mu> (X \<tau>) - \<nu> (X \<tau>)) = (\<lambda>\<tau>. \<mu>' (X \<tau>) - \<nu>' (X \<tau>)) on T)"
   shows "diff_invariant (\<lambda>s. \<nu> s \<le> \<mu> s) f T S t\<^sub>0 G"
 proof(simp add: diff_invariant_eq ivp_sols_def, clarsimp)
   fix X \<tau> assume "\<tau> \<in> T" and x_ivp:"D X = (\<lambda>\<tau>. f (X \<tau>)) on T" "\<nu> (X t\<^sub>0) \<le> \<mu> (X t\<^sub>0)"
   {assume "\<tau> \<noteq> t\<^sub>0"
   hence primed: "\<And>\<tau>. \<tau> \<in> T \<Longrightarrow> \<tau> > t\<^sub>0 \<Longrightarrow> \<mu>' (X \<tau>) \<ge> \<nu>' (X \<tau>)" 
     "\<And>\<tau>. \<tau> \<in> T \<Longrightarrow> \<tau> < t\<^sub>0 \<Longrightarrow> \<mu>' (X \<tau>) \<le> \<nu>' (X \<tau>)"
     using x_ivp assms by auto
   have obs1: "\<forall>t\<in>T. D (\<lambda>\<tau>. \<mu> (X \<tau>) - \<nu> (X \<tau>)) \<mapsto> (\<lambda>\<tau>. \<tau> *\<^sub>R (\<mu>' (X t) - \<nu>' (X t))) at t within T"
     using assms x_ivp by (auto simp: has_vderiv_on_def has_vector_derivative_def)
   have obs2: "{t\<^sub>0<--<\<tau>} \<subseteq> T" "{t\<^sub>0--\<tau>} \<subseteq> T"
     using \<open>\<tau> \<in> T\<close> Thyp \<open>\<tau> \<noteq> t\<^sub>0\<close> by (auto simp: convex_contains_open_segment 
         is_interval_convex_1 closed_segment_subset_interval)
   hence "D (\<lambda>\<tau>. \<mu> (X \<tau>) - \<nu> (X \<tau>)) = (\<lambda>\<tau>. \<mu>' (X \<tau>) - \<nu>' (X \<tau>)) on {t\<^sub>0--\<tau>}"
     using obs1 x_ivp by (auto intro!: has_derivative_subset[OF _ obs2(2)]
         simp: has_vderiv_on_def has_vector_derivative_def)
   then obtain t where "t \<in> {t\<^sub>0<--<\<tau>}" and
     "(\<mu> (X \<tau>) - \<nu> (X \<tau>)) - (\<mu> (X t\<^sub>0) - \<nu> (X t\<^sub>0)) = (\<lambda>\<tau>. \<tau> * (\<mu>' (X t) -  \<nu>' (X t))) (\<tau> - t\<^sub>0)"
     using mvt_simple_closed_segmentE \<open>\<tau> \<noteq> t\<^sub>0\<close> by blast
   hence mvt: "\<mu> (X \<tau>) - \<nu> (X \<tau>) = (\<tau> - t\<^sub>0) * (\<mu>' (X t) -  \<nu>' (X t)) + (\<mu> (X t\<^sub>0) - \<nu> (X t\<^sub>0))" 
     by force
   have  "\<tau> > t\<^sub>0 \<Longrightarrow> t > t\<^sub>0" "\<not> t\<^sub>0 \<le> \<tau> \<Longrightarrow> t < t\<^sub>0" "t \<in> T"
     using \<open>t \<in> {t\<^sub>0<--<\<tau>}\<close> obs2 unfolding open_segment_eq_real_ivl by auto
   moreover have "t > t\<^sub>0 \<Longrightarrow> (\<mu>' (X t) -  \<nu>' (X t)) \<ge> 0" "t < t\<^sub>0 \<Longrightarrow> (\<mu>' (X t) -  \<nu>' (X t)) \<le> 0"
     using primed(1,2)[OF \<open>t \<in> T\<close>] by auto
   ultimately have "(\<tau> - t\<^sub>0) * (\<mu>' (X t) -  \<nu>' (X t)) \<ge> 0"
     apply(case_tac "\<tau> \<ge> t\<^sub>0") 
     by (force, auto simp: split_mult_pos_le)
   hence "(\<tau> - t\<^sub>0) * (\<mu>' (X t) -  \<nu>' (X t)) + (\<mu> (X t\<^sub>0) - \<nu> (X t\<^sub>0)) \<ge> 0" 
     using  x_ivp(2) by auto
   hence "\<nu> (X \<tau>) \<le> \<mu> (X \<tau>)" 
     using mvt by simp}
   thus "\<nu> (X \<tau>) \<le> \<mu> (X \<tau>)"
     using x_ivp by blast
 qed
 
 lemma diff_invariant_less_rule [diff_invariant_rules]:
   fixes \<mu>::"'a::banach \<Rightarrow> real"
   assumes Thyp: "is_interval T" "t\<^sub>0 \<in> T"
     and "\<forall> X. (D X = (\<lambda>\<tau>. f (X \<tau>)) on T) \<longrightarrow> (\<forall>\<tau>\<in>T. (\<tau> > t\<^sub>0 \<longrightarrow> \<mu>' (X \<tau>) \<ge> \<nu>' (X \<tau>)) \<and> 
   (\<tau> < t\<^sub>0 \<longrightarrow> \<mu>' (X \<tau>) \<le> \<nu>' (X \<tau>))) \<and> (D (\<lambda>\<tau>. \<mu> (X \<tau>) - \<nu> (X \<tau>)) = (\<lambda>\<tau>. \<mu>' (X \<tau>) - \<nu>' (X \<tau>)) on T)"
   shows "diff_invariant (\<lambda>s. \<nu> s < \<mu> s) f T S t\<^sub>0 G"
 proof(simp add: diff_invariant_eq ivp_sols_def, clarsimp)
   fix X \<tau> assume "\<tau> \<in> T" and x_ivp:"D X = (\<lambda>\<tau>. f (X \<tau>)) on T" "\<nu> (X t\<^sub>0) < \<mu> (X t\<^sub>0)"
   {assume "\<tau> \<noteq> t\<^sub>0"
   hence primed: "\<And>\<tau>. \<tau> \<in> T \<Longrightarrow> \<tau> > t\<^sub>0 \<Longrightarrow> \<mu>' (X \<tau>) \<ge> \<nu>' (X \<tau>)" 
     "\<And>\<tau>. \<tau> \<in> T \<Longrightarrow> \<tau> < t\<^sub>0 \<Longrightarrow> \<mu>' (X \<tau>) \<le> \<nu>' (X \<tau>)"
     using x_ivp assms by auto
   have obs1: "\<forall>t\<in>T. D (\<lambda>\<tau>. \<mu> (X \<tau>) - \<nu> (X \<tau>)) \<mapsto> (\<lambda>\<tau>. \<tau> *\<^sub>R (\<mu>' (X t) - \<nu>' (X t))) at t within T"
     using assms x_ivp by (auto simp: has_vderiv_on_def has_vector_derivative_def)
   have obs2: "{t\<^sub>0<--<\<tau>} \<subseteq> T" "{t\<^sub>0--\<tau>} \<subseteq> T"
     using \<open>\<tau> \<in> T\<close> Thyp \<open>\<tau> \<noteq> t\<^sub>0\<close> by (auto simp: convex_contains_open_segment 
         is_interval_convex_1 closed_segment_subset_interval)
   hence "D (\<lambda>\<tau>. \<mu> (X \<tau>) - \<nu> (X \<tau>)) = (\<lambda>\<tau>. \<mu>' (X \<tau>) - \<nu>' (X \<tau>)) on {t\<^sub>0--\<tau>}"
     using obs1 x_ivp by (auto intro!: has_derivative_subset[OF _ obs2(2)]
         simp: has_vderiv_on_def has_vector_derivative_def)
   then obtain t where "t \<in> {t\<^sub>0<--<\<tau>}" and
     "(\<mu> (X \<tau>) - \<nu> (X \<tau>)) - (\<mu> (X t\<^sub>0) - \<nu> (X t\<^sub>0)) = (\<lambda>\<tau>. \<tau> * (\<mu>' (X t) -  \<nu>' (X t))) (\<tau> - t\<^sub>0)"
     using mvt_simple_closed_segmentE \<open>\<tau> \<noteq> t\<^sub>0\<close> by blast
   hence mvt: "\<mu> (X \<tau>) - \<nu> (X \<tau>) = (\<tau> - t\<^sub>0) * (\<mu>' (X t) -  \<nu>' (X t)) + (\<mu> (X t\<^sub>0) - \<nu> (X t\<^sub>0))" 
     by force
   have  "\<tau> > t\<^sub>0 \<Longrightarrow> t > t\<^sub>0" "\<not> t\<^sub>0 \<le> \<tau> \<Longrightarrow> t < t\<^sub>0" "t \<in> T"
     using \<open>t \<in> {t\<^sub>0<--<\<tau>}\<close> obs2 unfolding open_segment_eq_real_ivl by auto
   moreover have "t > t\<^sub>0 \<Longrightarrow> (\<mu>' (X t) -  \<nu>' (X t)) \<ge> 0" "t < t\<^sub>0 \<Longrightarrow> (\<mu>' (X t) -  \<nu>' (X t)) \<le> 0"
     using primed(1,2)[OF \<open>t \<in> T\<close>] by auto
   ultimately have "(\<tau> - t\<^sub>0) * (\<mu>' (X t) -  \<nu>' (X t)) \<ge> 0"
     apply(case_tac "\<tau> \<ge> t\<^sub>0") 
     by (force, auto simp: split_mult_pos_le)
   hence "(\<tau> - t\<^sub>0) * (\<mu>' (X t) -  \<nu>' (X t)) + (\<mu> (X t\<^sub>0) - \<nu> (X t\<^sub>0)) > 0" 
     using x_ivp(2) by auto
   hence "\<nu> (X \<tau>) < \<mu> (X \<tau>)" 
     using mvt by simp}
   thus "\<nu> (X \<tau>) < \<mu> (X \<tau>)"
     using x_ivp by blast
 qed
 
+lemma diff_invariant_nleq_rule:
+  fixes \<mu>::"'a::banach \<Rightarrow> real"
+  shows "diff_invariant (\<lambda>s. \<not> \<nu> s \<le> \<mu> s) f T S t\<^sub>0 G \<longleftrightarrow> diff_invariant (\<lambda>s. \<nu> s > \<mu> s) f T S t\<^sub>0 G"
+  unfolding diff_invariant_eq apply safe
+  by (clarsimp, erule_tac x=s in allE, simp, erule_tac x=X in ballE, force, force)+
+
+lemma diff_invariant_neq_rule [diff_invariant_rules]:
+  fixes \<mu>::"'a::banach \<Rightarrow> real"
+  assumes "diff_invariant (\<lambda>s. \<nu> s < \<mu> s) f T S t\<^sub>0 G"
+    and "diff_invariant (\<lambda>s. \<nu> s > \<mu> s) f T S t\<^sub>0 G"
+  shows "diff_invariant (\<lambda>s. \<nu> s \<noteq> \<mu> s) f T S t\<^sub>0 G"
+proof(unfold diff_invariant_eq, clarsimp)
+  fix s::'a and X::"real \<Rightarrow> 'a" and t::real
+  assume "\<nu> s \<noteq> \<mu> s" and Xhyp: "X \<in> Sols (\<lambda>t. f) T S t\<^sub>0 s" 
+     and thyp: "t \<in> T" and Ghyp: "\<forall>\<tau>. \<tau> \<in> T \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)"
+  hence "\<nu> s < \<mu> s \<or> \<nu> s > \<mu> s"
+    by linarith
+  moreover have "\<nu> s < \<mu> s \<Longrightarrow> \<nu> (X t) < \<mu> (X t)"
+    using assms(1) Xhyp thyp Ghyp unfolding diff_invariant_eq by auto
+  moreover have "\<nu> s > \<mu> s \<Longrightarrow> \<nu> (X t) > \<mu> (X t)"
+    using assms(2) Xhyp thyp Ghyp unfolding diff_invariant_eq by auto
+  ultimately show "\<nu> (X t) = \<mu> (X t) \<Longrightarrow> False"
+    by auto
+qed
+
+lemma diff_invariant_neq_rule_converse:
+  fixes \<mu>::"'a::banach \<Rightarrow> real"
+  assumes Thyp: "is_interval T" "t\<^sub>0 \<in> T" "\<forall>t\<in>T. t\<^sub>0 \<le> t"
+      and conts: "\<forall>X. (D X = (\<lambda>\<tau>. f (X \<tau>)) on T) \<longrightarrow> 
+  continuous_on (\<P> X T) \<nu> \<and> continuous_on (\<P> X T) \<mu>"
+      and dIhyp:"diff_invariant (\<lambda>s. \<nu> s \<noteq> \<mu> s) f T S t\<^sub>0 G"
+    shows "diff_invariant (\<lambda>s. \<nu> s < \<mu> s) f T S t\<^sub>0 G"
+proof(unfold diff_invariant_eq, clarsimp)
+  fix s::'a and X::"real \<Rightarrow> 'a" and t::real
+  assume ineq0: "\<nu> s < \<mu> s" and Xhyp: "X \<in> Sols (\<lambda>t. f) T S t\<^sub>0 s"
+    and Ghyp: "\<forall>\<tau>. \<tau> \<in> T \<and> \<tau> \<le> t \<longrightarrow> G (X \<tau>)" and thyp: "t\<in>T"
+  hence ineq1: "\<nu> (X t\<^sub>0) < \<mu> (X t\<^sub>0)"
+    by (auto simp: ivp_solsD)
+  have "t\<^sub>0 \<le> t" and "\<mu> (X t) \<noteq> \<nu> (X t)"
+    using \<open>t \<in> T\<close> Thyp dIhyp thyp Xhyp Ghyp ineq0 
+    unfolding diff_invariant_eq by force+
+  moreover
+  {assume ineq2:"\<nu> (X t) > \<mu> (X t)"
+    note continuous_on_compose[OF vderiv_on_continuous_on[OF ivp_solsD(1)[OF Xhyp]]]
+    hence "continuous_on T (\<nu> \<circ> X)" and "continuous_on T (\<mu> \<circ> X)"
+      using ivp_solsD(1)[OF Xhyp] conts by auto
+    also have "{t\<^sub>0--t} \<subseteq> T"
+      using Thyp thyp by (simp add: closed_segment_subset_interval)
+    ultimately have "continuous_on {t\<^sub>0--t} (\<lambda>\<tau>. \<nu> (X \<tau>))" 
+      and "continuous_on {t\<^sub>0--t} (\<lambda>\<tau>. \<mu> (X \<tau>))"
+      using continuous_on_subset by auto
+    then obtain \<tau> where "\<tau> \<in> {t\<^sub>0--t}" "\<mu> (X \<tau>) = \<nu> (X \<tau>)"
+      using IVT_two_functions_real_ivl[OF _ _ ineq1 ineq2] by force
+    hence "\<forall>r\<in>down T \<tau>. G (X r)" and "\<tau> \<in> T"
+      using Ghyp \<open>\<tau> \<in> {t\<^sub>0--t}\<close> \<open>t\<^sub>0 \<le> t\<close> \<open>{t\<^sub>0--t} \<subseteq> T\<close> 
+      by (auto simp: closed_segment_eq_real_ivl)
+    hence "\<mu> (X \<tau>) \<noteq> \<nu> (X \<tau>)"
+      using dIhyp Xhyp \<open>\<nu> s < \<mu> s\<close> 
+      unfolding diff_invariant_eq by force
+    hence "False"
+      using \<open>\<mu> (X \<tau>) = \<nu> (X \<tau>)\<close> by blast}
+  ultimately show "\<nu> (X t) < \<mu> (X t)"
+    by fastforce
+qed
+
 lemma diff_invariant_conj_rule [diff_invariant_rules]:
 assumes "diff_invariant I\<^sub>1 f T S t\<^sub>0 G" 
     and "diff_invariant I\<^sub>2 f T S t\<^sub>0 G"
 shows "diff_invariant (\<lambda>s. I\<^sub>1 s \<and> I\<^sub>2 s) f T S t\<^sub>0 G"
   using assms unfolding diff_invariant_def by auto
 
 lemma diff_invariant_disj_rule [diff_invariant_rules]:
 assumes "diff_invariant I\<^sub>1 f T S t\<^sub>0 G" 
     and "diff_invariant I\<^sub>2 f T S t\<^sub>0 G"
 shows "diff_invariant (\<lambda>s. I\<^sub>1 s \<or> I\<^sub>2 s) f T S t\<^sub>0 G"
   using assms unfolding diff_invariant_def by auto
 
 
 subsection \<open> Picard-Lindeloef \<close>
 
 text\<open> A locale with the assumptions of Picard-Lindeloef theorem. It extends 
 @{term "ll_on_open_it"} by providing an initial time @{term "t\<^sub>0 \<in> T"}.\<close>
 
 locale picard_lindeloef =
   fixes f::"real \<Rightarrow> ('a::{heine_borel,banach}) \<Rightarrow> 'a" and T::"real set" and S::"'a set" and t\<^sub>0::real
   assumes open_domain: "open T" "open S"
     and interval_time: "is_interval T"
     and init_time: "t\<^sub>0 \<in> T"
     and cont_vec_field: "\<forall>s \<in> S. continuous_on T (\<lambda>t. f t s)"
     and lipschitz_vec_field: "local_lipschitz T S f"
 begin
 
 sublocale ll_on_open_it T f S t\<^sub>0
   by (unfold_locales) (auto simp: cont_vec_field lipschitz_vec_field interval_time open_domain) 
 
 lemmas subintervalI = closed_segment_subset_domain
 
 lemma csols_eq: "csols t\<^sub>0 s = {(X, t). t \<in> T \<and>  X \<in> Sols f {t\<^sub>0--t} S t\<^sub>0 s}"
   unfolding ivp_sols_def csols_def solves_ode_def using subintervalI[OF init_time] by auto
 
 abbreviation "ex_ivl s \<equiv> existence_ivl t\<^sub>0 s"
 
 lemma unique_solution:
   assumes xivp: "D X = (\<lambda>t. f t (X t)) on {t\<^sub>0--t}" "X t\<^sub>0 = s" "X \<in> {t\<^sub>0--t} \<rightarrow> S" and "t \<in> T"
     and yivp: "D Y = (\<lambda>t. f t (Y t)) on {t\<^sub>0--t}" "Y t\<^sub>0 = s" "Y \<in> {t\<^sub>0--t} \<rightarrow> S" and "s \<in> S" 
   shows "X t = Y t"
 proof-
   have "(X, t) \<in> csols t\<^sub>0 s"
     using xivp \<open>t \<in> T\<close> unfolding csols_eq ivp_sols_def by auto
   hence ivl_fact: "{t\<^sub>0--t} \<subseteq> ex_ivl s"
     unfolding existence_ivl_def by auto
   have obs: "\<And>z T'. t\<^sub>0 \<in> T' \<and> is_interval T' \<and> T' \<subseteq> ex_ivl s \<and> (z solves_ode f) T' S \<Longrightarrow> 
   z t\<^sub>0 = flow t\<^sub>0 s t\<^sub>0 \<Longrightarrow> (\<forall>t\<in>T'. z t = flow t\<^sub>0 s t)"
     using flow_usolves_ode[OF init_time \<open>s \<in> S\<close>] unfolding usolves_ode_from_def by blast
   have "\<forall>\<tau>\<in>{t\<^sub>0--t}. X \<tau> = flow t\<^sub>0 s \<tau>"
     using obs[of "{t\<^sub>0--t}" X] xivp ivl_fact flow_initial_time[OF init_time  \<open>s \<in> S\<close>] 
     unfolding solves_ode_def by simp
   also have "\<forall>\<tau>\<in>{t\<^sub>0--t}. Y \<tau> = flow t\<^sub>0 s \<tau>"
     using obs[of "{t\<^sub>0--t}" Y] yivp ivl_fact flow_initial_time[OF init_time  \<open>s \<in> S\<close>] 
     unfolding solves_ode_def by simp
   ultimately show "X t = Y t"
     by auto
 qed
 
 lemma solution_eq_flow:
   assumes xivp: "D X = (\<lambda>t. f t (X t)) on ex_ivl s" "X t\<^sub>0 = s" "X \<in> ex_ivl s \<rightarrow> S" 
     and "t \<in> ex_ivl s" and "s \<in> S" 
   shows "X t = flow t\<^sub>0 s t"
 proof-
   have obs: "\<And>z T'. t\<^sub>0 \<in> T' \<and> is_interval T' \<and> T' \<subseteq> ex_ivl s \<and> (z solves_ode f) T' S \<Longrightarrow> 
   z t\<^sub>0 = flow t\<^sub>0 s t\<^sub>0 \<Longrightarrow> (\<forall>t\<in>T'. z t = flow t\<^sub>0 s t)"
     using flow_usolves_ode[OF init_time \<open>s \<in> S\<close>] unfolding usolves_ode_from_def by blast
   have "\<forall>\<tau>\<in>ex_ivl s. X \<tau> = flow t\<^sub>0 s \<tau>"
     using obs[of "ex_ivl s" X] existence_ivl_initial_time[OF init_time \<open>s \<in> S\<close>]
       xivp flow_initial_time[OF init_time \<open>s \<in> S\<close>] unfolding solves_ode_def by simp
   thus "X t = flow t\<^sub>0 s t"
     by (auto simp: \<open>t \<in> ex_ivl s\<close>)
 qed
 
 end
 
 lemma local_lipschitz_add: 
   fixes f1 f2 :: "real \<Rightarrow> 'a::banach \<Rightarrow> 'a"
   assumes "local_lipschitz T S f1"
       and "local_lipschitz T S f2" 
     shows "local_lipschitz T S (\<lambda>t s. f1 t s + f2 t s)"
 proof(unfold local_lipschitz_def, clarsimp)
   fix s and t assume "s \<in> S" and "t \<in> T"
   obtain \<epsilon>\<^sub>1 L1 where "\<epsilon>\<^sub>1 > 0" and L1: "\<And>\<tau>. \<tau>\<in>cball t \<epsilon>\<^sub>1 \<inter> T \<Longrightarrow> L1-lipschitz_on (cball s \<epsilon>\<^sub>1 \<inter> S) (f1 \<tau>)"
     using local_lipschitzE[OF assms(1) \<open>t \<in> T\<close> \<open>s \<in> S\<close>] by blast
   obtain \<epsilon>\<^sub>2 L2 where "\<epsilon>\<^sub>2 > 0" and L2: "\<And>\<tau>. \<tau>\<in>cball t \<epsilon>\<^sub>2 \<inter> T \<Longrightarrow> L2-lipschitz_on (cball s \<epsilon>\<^sub>2 \<inter> S) (f2 \<tau>)"
     using local_lipschitzE[OF assms(2) \<open>t \<in> T\<close> \<open>s \<in> S\<close>] by blast
   have ballH: "cball s (min \<epsilon>\<^sub>1 \<epsilon>\<^sub>2) \<inter> S \<subseteq> cball s \<epsilon>\<^sub>1 \<inter> S" "cball s (min \<epsilon>\<^sub>1 \<epsilon>\<^sub>2) \<inter> S \<subseteq> cball s \<epsilon>\<^sub>2 \<inter> S"
     by auto
   have obs1: "\<forall>\<tau>\<in>cball t \<epsilon>\<^sub>1 \<inter> T. L1-lipschitz_on (cball s (min \<epsilon>\<^sub>1 \<epsilon>\<^sub>2) \<inter> S) (f1 \<tau>)"
     using lipschitz_on_subset[OF L1 ballH(1)] by blast
   also have obs2: "\<forall>\<tau>\<in>cball t \<epsilon>\<^sub>2 \<inter> T. L2-lipschitz_on (cball s (min \<epsilon>\<^sub>1 \<epsilon>\<^sub>2) \<inter> S) (f2 \<tau>)"
     using lipschitz_on_subset[OF L2 ballH(2)] by blast
   ultimately have "\<forall>\<tau>\<in>cball t (min \<epsilon>\<^sub>1 \<epsilon>\<^sub>2) \<inter> T. 
     (L1 + L2)-lipschitz_on (cball s (min \<epsilon>\<^sub>1 \<epsilon>\<^sub>2) \<inter> S) (\<lambda>s. f1 \<tau> s + f2 \<tau> s)"
     using lipschitz_on_add by fastforce
   thus "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> T. L-lipschitz_on (cball s u \<inter> S) (\<lambda>s. f1 t s + f2 t s)"
     apply(rule_tac x="min \<epsilon>\<^sub>1 \<epsilon>\<^sub>2" in exI)
     using \<open>\<epsilon>\<^sub>1 > 0\<close> \<open>\<epsilon>\<^sub>2 > 0\<close> by force
 qed
 
 lemma picard_lindeloef_add: "picard_lindeloef f1 T S t\<^sub>0 \<Longrightarrow> picard_lindeloef f2 T S t\<^sub>0 \<Longrightarrow> 
   picard_lindeloef (\<lambda>t s. f1 t s + f2 t s) T S t\<^sub>0"
   unfolding picard_lindeloef_def apply(clarsimp, rule conjI)
   using continuous_on_add apply fastforce
   using local_lipschitz_add by blast
 
 lemma picard_lindeloef_constant: "picard_lindeloef (\<lambda>t s. c) UNIV UNIV t\<^sub>0"
   apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def, clarsimp)
   by (rule_tac x=1 in exI, clarsimp, rule_tac x="1/2" in exI, simp)
 
 
 subsection \<open> Flows for ODEs \<close>
 
 text\<open> A locale designed for verification of hybrid systems. The user can select the interval 
 of existence and the defining flow equation via the variables @{term "T"} and @{term "\<phi>"}.\<close>
 
 locale local_flow = picard_lindeloef "(\<lambda> t. f)" T S 0 
   for f::"'a::{heine_borel,banach} \<Rightarrow> 'a" and T S L +
   fixes \<phi> :: "real \<Rightarrow> 'a \<Rightarrow> 'a"
   assumes ivp:
     "\<And> t s. t \<in> T \<Longrightarrow> s \<in> S \<Longrightarrow> D (\<lambda>t. \<phi> t s) = (\<lambda>t. f (\<phi> t s)) on {0--t}"
     "\<And> s. s \<in> S \<Longrightarrow> \<phi> 0 s = s"
     "\<And> t s. t \<in> T \<Longrightarrow> s \<in> S \<Longrightarrow> (\<lambda>t. \<phi> t s) \<in> {0--t} \<rightarrow> S"
 begin
 
 lemma in_ivp_sols_ivl: 
   assumes "t \<in> T" "s \<in> S"
   shows "(\<lambda>t. \<phi> t s) \<in> Sols (\<lambda>t. f) {0--t} S 0 s"
   apply(rule ivp_solsI)
   using ivp assms by auto
 
 lemma eq_solution_ivl:
   assumes xivp: "D X = (\<lambda>t. f (X t)) on {0--t}" "X 0 = s" "X \<in> {0--t} \<rightarrow> S" 
     and indom: "t \<in> T" "s \<in> S"
   shows "X t = \<phi> t s"
   apply(rule unique_solution[OF xivp \<open>t \<in> T\<close>])
   using \<open>s \<in> S\<close> ivp indom by auto
 
 lemma ex_ivl_eq:
   assumes "s \<in> S"
   shows "ex_ivl s = T"
   using existence_ivl_subset[of s] apply safe
   unfolding existence_ivl_def csols_eq 
   using in_ivp_sols_ivl[OF _ assms] by blast
 
 lemma has_derivative_on_open1: 
   assumes  "t > 0" "t \<in> T" "s \<in> S"
   obtains B where "t \<in> B" and "open B" and "B \<subseteq> T"
     and "D (\<lambda>\<tau>. \<phi> \<tau> s) \<mapsto> (\<lambda>\<tau>. \<tau> *\<^sub>R f (\<phi> t s)) at t within B" 
 proof-
   obtain r::real where rHyp: "r > 0" "ball t r \<subseteq> T"
     using open_contains_ball_eq open_domain(1) \<open>t \<in> T\<close> by blast
   moreover have "t + r/2 > 0"
     using \<open>r > 0\<close> \<open>t > 0\<close> by auto
   moreover have "{0--t} \<subseteq> T" 
     using subintervalI[OF init_time \<open>t \<in> T\<close>] .
   ultimately have subs: "{0<--<t + r/2} \<subseteq> T"
     unfolding abs_le_eq abs_le_eq real_ivl_eqs[OF \<open>t > 0\<close>] real_ivl_eqs[OF \<open>t + r/2 > 0\<close>] 
     by clarify (case_tac "t < x", simp_all add: cball_def ball_def dist_norm subset_eq field_simps)
   have "t + r/2 \<in> T"
     using rHyp unfolding real_ivl_eqs[OF rHyp(1)] by (simp add: subset_eq)
   hence "{0--t + r/2} \<subseteq> T"
     using subintervalI[OF init_time] by blast
   hence "(D (\<lambda>t. \<phi> t s) = (\<lambda>t. f (\<phi> t s)) on {0--(t + r/2)})"
     using ivp(1)[OF _ \<open>s \<in> S\<close>] by auto
   hence vderiv: "(D (\<lambda>t. \<phi> t s) = (\<lambda>t. f (\<phi> t s)) on {0<--<t + r/2})"
     apply(rule has_vderiv_on_subset)
     unfolding real_ivl_eqs[OF \<open>t + r/2 > 0\<close>] by auto
   have "t \<in> {0<--<t + r/2}"
     unfolding real_ivl_eqs[OF \<open>t + r/2 > 0\<close>] using rHyp \<open>t > 0\<close> by simp
   moreover have "D (\<lambda>\<tau>. \<phi> \<tau> s) \<mapsto> (\<lambda>\<tau>. \<tau> *\<^sub>R f (\<phi> t s)) (at t within {0<--<t + r/2})"
     using vderiv calculation unfolding has_vderiv_on_def has_vector_derivative_def by blast
   moreover have "open {0<--<t + r/2}"
     unfolding real_ivl_eqs[OF \<open>t + r/2 > 0\<close>] by simp
   ultimately show ?thesis
     using subs that by blast
 qed
 
 lemma has_derivative_on_open2: 
   assumes "t < 0" "t \<in> T" "s \<in> S"
   obtains B where "t \<in> B" and "open B" and "B \<subseteq> T"
     and "D (\<lambda>\<tau>. \<phi> \<tau> s) \<mapsto> (\<lambda>\<tau>. \<tau> *\<^sub>R f (\<phi> t s)) at t within B" 
 proof-
   obtain r::real where rHyp: "r > 0" "ball t r \<subseteq> T"
     using open_contains_ball_eq open_domain(1) \<open>t \<in> T\<close> by blast
   moreover have "t - r/2 < 0"
     using \<open>r > 0\<close> \<open>t < 0\<close> by auto
   moreover have "{0--t} \<subseteq> T" 
     using subintervalI[OF init_time \<open>t \<in> T\<close>] .
   ultimately have subs: "{0<--<t - r/2} \<subseteq> T"
     unfolding open_segment_eq_real_ivl closed_segment_eq_real_ivl
       real_ivl_eqs[OF rHyp(1)] by(auto simp: subset_eq)
   have "t - r/2 \<in> T"
     using rHyp unfolding real_ivl_eqs by (simp add: subset_eq)
   hence "{0--t - r/2} \<subseteq> T"
     using subintervalI[OF init_time] by blast
   hence "(D (\<lambda>t. \<phi> t s) = (\<lambda>t. f (\<phi> t s)) on {0--(t - r/2)})"
     using ivp(1)[OF _ \<open>s \<in> S\<close>] by auto
   hence vderiv: "(D (\<lambda>t. \<phi> t s) = (\<lambda>t. f (\<phi> t s)) on {0<--<t - r/2})"
     apply(rule has_vderiv_on_subset)
     unfolding open_segment_eq_real_ivl closed_segment_eq_real_ivl by auto
   have "t \<in> {0<--<t - r/2}"
     unfolding open_segment_eq_real_ivl using rHyp \<open>t < 0\<close> by simp
   moreover have "D (\<lambda>\<tau>. \<phi> \<tau> s) \<mapsto> (\<lambda>\<tau>. \<tau> *\<^sub>R f (\<phi> t s)) (at t within {0<--<t - r/2})"
     using vderiv calculation unfolding has_vderiv_on_def has_vector_derivative_def by blast
   moreover have "open {0<--<t - r/2}"
     unfolding open_segment_eq_real_ivl by simp
   ultimately show ?thesis
     using subs that by blast
 qed
 
 lemma has_derivative_on_open3: 
   assumes "s \<in> S"
   obtains B where "0 \<in> B" and "open B" and "B \<subseteq> T"
     and "D (\<lambda>\<tau>. \<phi> \<tau> s) \<mapsto> (\<lambda>\<tau>. \<tau> *\<^sub>R f (\<phi> 0 s)) at 0 within B" 
 proof-
   obtain r::real where rHyp: "r > 0" "ball 0 r \<subseteq> T"
     using open_contains_ball_eq open_domain(1) init_time by blast
   hence "r/2 \<in> T" "-r/2 \<in> T" "r/2 > 0"
     unfolding real_ivl_eqs by auto
   hence subs: "{0--r/2} \<subseteq> T" "{0--(-r/2)} \<subseteq> T"
     using subintervalI[OF init_time] by auto
   hence "(D (\<lambda>t. \<phi> t s) = (\<lambda>t. f (\<phi> t s)) on {0--r/2})"
     "(D (\<lambda>t. \<phi> t s) = (\<lambda>t. f (\<phi> t s)) on {0--(-r/2)})"
     using ivp(1)[OF _ \<open>s \<in> S\<close>] by auto
   also have "{0--r/2} = {0--r/2} \<union> closure {0--r/2} \<inter> closure {0--(-r/2)}"
     "{0--(-r/2)} = {0--(-r/2)} \<union> closure {0--r/2} \<inter> closure {0--(-r/2)}"
     unfolding closed_segment_eq_real_ivl \<open>r/2 > 0\<close> by auto
   ultimately have vderivs:
     "(D (\<lambda>t. \<phi> t s) = (\<lambda>t. f (\<phi> t s)) on {0--r/2} \<union> closure {0--r/2} \<inter> closure {0--(-r/2)})"
     "(D (\<lambda>t. \<phi> t s) = (\<lambda>t. f (\<phi> t s)) on {0--(-r/2)} \<union> closure {0--r/2} \<inter> closure {0--(-r/2)})"
     unfolding closed_segment_eq_real_ivl \<open>r/2 > 0\<close> by auto
   have obs: "0 \<in> {-r/2<--<r/2}"
     unfolding open_segment_eq_real_ivl using \<open>r/2 > 0\<close> by auto
   have union: "{-r/2--r/2} = {0--r/2} \<union> {0--(-r/2)}"
     unfolding closed_segment_eq_real_ivl by auto
   hence "(D (\<lambda>t. \<phi> t s) = (\<lambda>t. f (\<phi> t s)) on {-r/2--r/2})"
     using has_vderiv_on_union[OF vderivs] by simp
   hence "(D (\<lambda>t. \<phi> t s) = (\<lambda>t. f (\<phi> t s)) on {-r/2<--<r/2})"
     using has_vderiv_on_subset[OF _ segment_open_subset_closed[of "-r/2" "r/2"]] by auto
   hence "D (\<lambda>\<tau>. \<phi> \<tau> s) \<mapsto> (\<lambda>\<tau>. \<tau> *\<^sub>R f (\<phi> 0 s)) (at 0 within {-r/2<--<r/2})"
     unfolding has_vderiv_on_def has_vector_derivative_def using obs by blast
   moreover have "open {-r/2<--<r/2}"
     unfolding open_segment_eq_real_ivl by simp
   moreover have "{-r/2<--<r/2} \<subseteq> T"
     using subs union segment_open_subset_closed by blast 
   ultimately show ?thesis
     using obs that by blast
 qed
 
 lemma has_derivative_on_open: 
   assumes "t \<in> T" "s \<in> S"
   obtains B where "t \<in> B" and "open B" and "B \<subseteq> T"
     and "D (\<lambda>\<tau>. \<phi> \<tau> s) \<mapsto> (\<lambda>\<tau>. \<tau> *\<^sub>R f (\<phi> t s)) at t within B" 
   apply(subgoal_tac "t < 0 \<or> t = 0 \<or> t > 0")
   using has_derivative_on_open1[OF _ assms] has_derivative_on_open2[OF _ assms]
     has_derivative_on_open3[OF \<open>s \<in> S\<close>] by blast force
 
 lemma in_domain:
   assumes "s \<in> S"
   shows "(\<lambda>t. \<phi> t s) \<in> T \<rightarrow> S"
   unfolding ex_ivl_eq[symmetric] existence_ivl_def
   using local.mem_existence_ivl_subset ivp(3)[OF _ assms] by blast
 
 lemma has_vderiv_on_domain:
   assumes "s \<in> S"
   shows "D (\<lambda>t. \<phi> t s) = (\<lambda>t. f (\<phi> t s)) on T"
 proof(unfold has_vderiv_on_def has_vector_derivative_def, clarsimp)
   fix t assume "t \<in> T"
   then obtain B where "t \<in> B" and "open B" and "B \<subseteq> T" 
     and Dhyp: "D (\<lambda>t. \<phi> t s) \<mapsto> (\<lambda>\<tau>. \<tau> *\<^sub>R f (\<phi> t s)) at t within B"
     using assms has_derivative_on_open[OF \<open>t \<in> T\<close>] by blast
   hence "t \<in> interior B"
     using interior_eq by auto
   thus "D (\<lambda>t. \<phi> t s) \<mapsto> (\<lambda>\<tau>. \<tau> *\<^sub>R f (\<phi> t s)) at t within T"
     using has_derivative_at_within_mono[OF _ \<open>B \<subseteq> T\<close> Dhyp] by blast
 qed
 
 lemma in_ivp_sols: 
   assumes "s \<in> S"
   shows "(\<lambda>t. \<phi> t s) \<in> Sols (\<lambda>t. f) T S 0 s"
   using has_vderiv_on_domain ivp(2) in_domain apply(rule ivp_solsI)
   using assms by auto
 
 lemma eq_solution:
   assumes "X \<in> Sols (\<lambda>t. f) T S 0 s" and "t \<in> T" and "s \<in> S"
   shows "X t = \<phi> t s"
 proof-
   have "D X = (\<lambda>t. f (X t)) on (ex_ivl s)" and "X 0 = s" and "X \<in> (ex_ivl s) \<rightarrow> S"
     using ivp_solsD[OF assms(1)] unfolding ex_ivl_eq[OF \<open>s \<in> S\<close>] by auto
   note solution_eq_flow[OF this]
   hence "X t = flow 0 s t"
     unfolding ex_ivl_eq[OF \<open>s \<in> S\<close>] using assms by blast
   also have "\<phi> t s = flow 0 s t"
     apply(rule solution_eq_flow ivp)
         apply(simp_all add: assms(2,3) ivp(2)[OF \<open>s \<in> S\<close>])
     unfolding ex_ivl_eq[OF \<open>s \<in> S\<close>] by (auto simp: has_vderiv_on_domain assms in_domain)
   ultimately show "X t = \<phi> t s"
     by simp
 qed
 
 lemma ivp_sols_collapse: 
   assumes "T = UNIV" and "s \<in> S"
   shows "Sols (\<lambda>t. f) T S 0 s = {(\<lambda>t. \<phi> t s)}"
   using in_ivp_sols eq_solution assms by auto
 
 lemma additive_in_ivp_sols:
   assumes "s \<in> S" and "\<P> (\<lambda>\<tau>. \<tau> + t) T \<subseteq> T"
   shows "(\<lambda>\<tau>. \<phi> (\<tau> + t) s) \<in> Sols (\<lambda>t. f) T S 0 (\<phi> (0 + t) s)"
   apply(rule ivp_solsI, rule vderiv_on_compose_add)
   using has_vderiv_on_domain has_vderiv_on_subset assms 
     apply blast
   using in_domain assms by auto
 
 lemma is_monoid_action:
   assumes "s \<in> S" and "T = UNIV"
   shows "\<phi> 0 s = s" and "\<phi> (t\<^sub>1 + t\<^sub>2) s = \<phi> t\<^sub>1 (\<phi> t\<^sub>2 s)"
 proof-
   show "\<phi> 0 s = s"
     using ivp assms by simp
   have "\<phi> (0 + t\<^sub>2) s = \<phi> t\<^sub>2 s" 
     by simp
   also have "\<phi> t\<^sub>2 s \<in> S"
     using in_domain assms by auto
   finally show "\<phi> (t\<^sub>1 + t\<^sub>2) s = \<phi> t\<^sub>1 (\<phi> t\<^sub>2 s)"
     using eq_solution[OF additive_in_ivp_sols] assms by auto
 qed
 
 definition orbit :: "'a \<Rightarrow> 'a set" ("\<gamma>\<^sup>\<phi>")
   where "\<gamma>\<^sup>\<phi> s = g_orbital f (\<lambda>s. True) T S 0 s"
 
 lemma orbit_eq[simp]: 
   assumes "s \<in> S"
   shows "\<gamma>\<^sup>\<phi> s = {\<phi> t s| t. t \<in> T}"
   using eq_solution assms unfolding orbit_def g_orbital_eq ivp_sols_def
   by(auto intro!: has_vderiv_on_domain ivp(2) in_domain)
 
 lemma g_orbital_collapses: 
   assumes "s \<in> S"
   shows "g_orbital f G T S 0 s = {\<phi> t s| t. t \<in> T \<and> (\<forall>\<tau>\<in>down T t. G (\<phi> \<tau> s))}"
 proof(rule subset_antisym, simp_all only: subset_eq)
   let ?gorbit = "{\<phi> t s |t. t \<in> T \<and> (\<forall>\<tau>\<in>down T t. G (\<phi> \<tau> s))}"
   {fix s' assume "s' \<in> g_orbital f G T S 0 s"
     then obtain X and t where x_ivp:"X \<in> Sols (\<lambda>t. f) T S 0 s" 
       and "X t = s'" and "t \<in> T" and guard:"(\<P> X (down T t) \<subseteq> {s. G s})"
       unfolding g_orbital_def g_orbit_eq by auto
     have obs:"\<forall>\<tau>\<in>(down T t). X \<tau> = \<phi> \<tau> s"
       using eq_solution[OF x_ivp _ assms] by blast
     hence "\<P> (\<lambda>t. \<phi> t s) (down T t) \<subseteq> {s. G s}"
       using guard by auto 
     also have "\<phi> t s = X t"
       using eq_solution[OF x_ivp \<open>t \<in> T\<close> assms] by simp
     ultimately have "s' \<in> ?gorbit"
       using \<open>X t = s'\<close> \<open>t \<in> T\<close> by auto}
   thus "\<forall>s'\<in> g_orbital f G T S 0 s. s' \<in> ?gorbit"
     by blast
 next
   let ?gorbit = "{\<phi> t s |t. t \<in> T \<and> (\<forall>\<tau>\<in>down T t. G (\<phi> \<tau> s))}"
   {fix s' assume "s' \<in> ?gorbit"
     then obtain t where "\<P> (\<lambda>t. \<phi> t s) (down T t) \<subseteq> {s. G s}" and "t \<in> T" and "\<phi> t s = s'"
       by blast
     hence "s' \<in> g_orbital f G T S 0 s"
       using assms by(auto intro!: g_orbitalI in_ivp_sols)}
   thus "\<forall>s'\<in>?gorbit. s' \<in> g_orbital f G T S 0 s"
     by blast
 qed
 
 end
 
 lemma line_is_local_flow: 
   "0 \<in> T \<Longrightarrow> is_interval T \<Longrightarrow> open T \<Longrightarrow> local_flow (\<lambda> s. c) T UNIV (\<lambda> t s. s + t *\<^sub>R c)"
   apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def, clarsimp)
    apply(rule_tac x=1 in exI, clarsimp, rule_tac x="1/2" in exI, simp)
   apply(rule_tac f'1="\<lambda> s. 0" and g'1="\<lambda> s. c" in has_vderiv_on_add[THEN has_vderiv_on_eq_rhs])
     apply(rule derivative_intros, simp)+
   by simp_all
 
 end
\ No newline at end of file
diff --git a/thys/Hybrid_Systems_VCs/HS_Preliminaries.thy b/thys/Hybrid_Systems_VCs/HS_Preliminaries.thy
--- a/thys/Hybrid_Systems_VCs/HS_Preliminaries.thy
+++ b/thys/Hybrid_Systems_VCs/HS_Preliminaries.thy
@@ -1,308 +1,351 @@
 (*  Title:       Preliminaries for hybrid systems verification
     Author:      Jonathan Julián Huerta y Munive, 2019
     Maintainer:  Jonathan Julián Huerta y Munive <jjhuertaymunive1@sheffield.ac.uk>
 *)
 
 section \<open> Hybrid Systems Preliminaries \<close>
 
 text \<open>Hybrid systems combine continuous dynamics with discrete control. This section contains
 auxiliary lemmas for verification of hybrid systems.\<close>
 
 theory HS_Preliminaries
   imports "Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative"
 begin
 
 
 subsection \<open> Real numbers \<close>
 
 lemma abs_le_eq:
   shows "(r::real) > 0 \<Longrightarrow> (\<bar>x\<bar> < r) = (-r < x \<and> x < r)"
     and "(r::real) > 0 \<Longrightarrow> (\<bar>x\<bar> \<le> r) = (-r \<le> x \<and> x \<le> r)"
   by linarith+
 
 lemma real_ivl_eqs:
   assumes "0 < r"
   shows "ball x r = {x-r<--< x+r}"         and "{x-r<--< x+r} = {x-r<..< x+r}"
     and "ball (r / 2) (r / 2) = {0<--<r}"  and "{0<--<r} = {0<..<r}"
     and "ball 0 r = {-r<--<r}"             and "{-r<--<r} = {-r<..<r}"
     and "cball x r = {x-r--x+r}"           and "{x-r--x+r} = {x-r..x+r}"
     and "cball (r / 2) (r / 2) = {0--r}"   and "{0--r} = {0..r}"
     and "cball 0 r = {-r--r}"              and "{-r--r} = {-r..r}"
   unfolding open_segment_eq_real_ivl closed_segment_eq_real_ivl
   using assms by (auto simp: cball_def ball_def dist_norm field_simps)
 
 lemma norm_rotate_eq[simp]:
   fixes x :: "'a:: {banach,real_normed_field}"
   shows "(x * cos t - y * sin t)\<^sup>2 + (x * sin t + y * cos t)\<^sup>2 = x\<^sup>2 + y\<^sup>2"
     and "(x * cos t + y * sin t)\<^sup>2 + (y * cos t - x * sin t)\<^sup>2 = x\<^sup>2 + y\<^sup>2"
 proof-
   have "(x * cos t - y * sin t)\<^sup>2 = x\<^sup>2 * (cos t)\<^sup>2 + y\<^sup>2 * (sin t)\<^sup>2 - 2 * (x * cos t) * (y * sin t)"
     by(simp add: power2_diff power_mult_distrib)
   also have "(x * sin t + y * cos t)\<^sup>2 = y\<^sup>2 * (cos t)\<^sup>2 + x\<^sup>2 * (sin t)\<^sup>2 + 2 * (x * cos t) * (y * sin t)"
     by(simp add: power2_sum power_mult_distrib)
   ultimately show "(x * cos t - y * sin t)\<^sup>2 + (x * sin t + y * cos t)\<^sup>2 = x\<^sup>2 + y\<^sup>2"
     by (simp add: Groups.mult_ac(2) Groups.mult_ac(3) right_diff_distrib sin_squared_eq)
   thus "(x * cos t + y * sin t)\<^sup>2 + (y * cos t - x * sin t)\<^sup>2 = x\<^sup>2 + y\<^sup>2"
     by (simp add: add.commute add.left_commute power2_diff power2_sum)
 qed
 
 
 subsection \<open> Single variable derivatives \<close>
 
 notation has_derivative ("(1(D _ \<mapsto> (_))/ _)" [65,65] 61)
 notation has_vderiv_on ("(1 D _ = (_)/ on _)" [65,65] 61)
 notation norm ("(1\<parallel>_\<parallel>)" [65] 61)
 
 thy_deps
 
 named_theorems poly_derivatives "compilation of optimised miscellaneous derivative rules."
 
 declare has_vderiv_on_const [poly_derivatives]
     and has_vderiv_on_id [poly_derivatives]
     and has_vderiv_on_add[THEN has_vderiv_on_eq_rhs, poly_derivatives]
     and has_vderiv_on_diff[THEN has_vderiv_on_eq_rhs, poly_derivatives]
     and has_vderiv_on_mult[THEN has_vderiv_on_eq_rhs, poly_derivatives]
 
 lemma has_vderiv_on_compose_eq:
   assumes "D f = f' on g ` T"
     and " D g = g' on T"
     and "h = (\<lambda>x. g' x *\<^sub>R f' (g x))"
   shows "D (\<lambda>t. f (g t)) = h on T"
   apply(subst ssubst[of h], simp)
   using assms has_vderiv_on_compose by auto
 
 lemma vderiv_on_compose_add [derivative_intros]:
   assumes "D x = x' on (\<lambda>\<tau>. \<tau> + t) ` T"
   shows "D (\<lambda>\<tau>. x (\<tau> + t)) = (\<lambda>\<tau>. x' (\<tau> + t)) on T"
   apply(rule has_vderiv_on_compose_eq[OF assms])
   by(auto intro: derivative_intros)
 
 lemma has_vderiv_on_divide_cnst: "a \<noteq> 0 \<Longrightarrow> D (\<lambda>t. t/a) = (\<lambda>t. 1/a) on T"
   unfolding has_vderiv_on_def has_vector_derivative_def
   apply clarify
   apply(rule_tac f'1="\<lambda>t. t" and g'1="\<lambda> x. 0" in has_derivative_divide[THEN has_derivative_eq_rhs])
   by(auto intro: derivative_eq_intros)
 
 lemma has_vderiv_on_power: "n \<ge> 1 \<Longrightarrow> D (\<lambda>t. t ^ n) = (\<lambda>t. n * (t ^ (n - 1))) on T"
   unfolding has_vderiv_on_def has_vector_derivative_def
   by (auto intro!: derivative_eq_intros)
 
 lemma has_vderiv_on_exp: "D (\<lambda>t. exp t) = (\<lambda>t. exp t) on T"
   unfolding has_vderiv_on_def has_vector_derivative_def by (auto intro: derivative_intros)
 
 lemma has_vderiv_on_cos_comp:
   "D (f::real \<Rightarrow> real) = f' on T \<Longrightarrow> D (\<lambda>t. cos (f t)) = (\<lambda>t. - (f' t) * sin (f t)) on T"
   apply(rule has_vderiv_on_compose_eq[of "\<lambda>t. cos t"])
   unfolding has_vderiv_on_def has_vector_derivative_def
     apply clarify
   by(auto intro!: derivative_eq_intros simp: fun_eq_iff)
 
 lemma has_vderiv_on_sin_comp:
   "D (f::real \<Rightarrow> real) = f' on T \<Longrightarrow> D (\<lambda>t. sin (f t)) = (\<lambda>t. (f' t) * cos (f t)) on T"
   apply(rule has_vderiv_on_compose_eq[of "\<lambda>t. sin t"])
   unfolding has_vderiv_on_def has_vector_derivative_def
     apply clarify
   by(auto intro!: derivative_eq_intros simp: fun_eq_iff)
 
 lemma has_vderiv_on_exp_comp:
   "D (f::real \<Rightarrow> real) = f' on T \<Longrightarrow> D (\<lambda>t. exp (f t)) = (\<lambda>t. (f' t) * exp (f t)) on T"
   apply(rule has_vderiv_on_compose_eq[of "\<lambda>t. exp t"])
   by (rule has_vderiv_on_exp, simp_all add: mult.commute)
 
 lemma vderiv_uminus_intro [poly_derivatives]:
   "D f = f' on T \<Longrightarrow> g = (\<lambda>t. - f' t) \<Longrightarrow> D (\<lambda>t. - f t) = g on T"
   using has_vderiv_on_uminus by auto
 
 lemma vderiv_div_cnst_intro [poly_derivatives]:
   assumes "(a::real) \<noteq> 0" and "D f = f' on T" and "g = (\<lambda>t. (f' t)/a)"
   shows "D (\<lambda>t. (f t)/a) = g on T"
   apply(rule has_vderiv_on_compose_eq[of "\<lambda>t. t/a" "\<lambda>t. 1/a"])
   using assms by(auto intro: has_vderiv_on_divide_cnst)
 
 lemma vderiv_npow_intro [poly_derivatives]:
   fixes f::"real \<Rightarrow> real"
   assumes "n \<ge> 1" and "D f = f' on T" and "g = (\<lambda>t. n * (f' t) * (f t)^(n-1))"
   shows "D (\<lambda>t. (f t)^n) = g on T"
   apply(rule has_vderiv_on_compose_eq[of "\<lambda>t. t^n"])
   using assms(1)
     apply(rule has_vderiv_on_power)
   using assms by auto
 
 lemma vderiv_cos_intro [poly_derivatives]:
   assumes "D (f::real \<Rightarrow> real) = f' on T" and "g = (\<lambda>t. - (f' t) * sin (f t))"
   shows "D (\<lambda>t. cos (f t)) = g on T"
   using assms and has_vderiv_on_cos_comp by auto
 
 lemma vderiv_sin_intro [poly_derivatives]:
   assumes "D (f::real \<Rightarrow> real) = f' on T" and "g = (\<lambda>t. (f' t) * cos (f t))"
   shows "D (\<lambda>t. sin (f t)) = g on T"
   using assms and has_vderiv_on_sin_comp by auto
 
 lemma vderiv_exp_intro [poly_derivatives]:
   assumes "D (f::real \<Rightarrow> real) = f' on T" and "g = (\<lambda>t. (f' t) * exp (f t))"
   shows "D (\<lambda>t. exp (f t)) = g on T"
   using assms and has_vderiv_on_exp_comp by auto
 
 \<comment> \<open>Examples for checking derivatives\<close>
 
 lemma "D (\<lambda>t. a * t\<^sup>2 / 2 + v * t + x) = (\<lambda>t. a * t + v) on T"
   by(auto intro!: poly_derivatives)
 
 lemma "D (\<lambda>t. v * t - a * t\<^sup>2 / 2 + x) = (\<lambda>x. v - a * x) on T"
   by(auto intro!: poly_derivatives)
 
 lemma "c \<noteq> 0 \<Longrightarrow> D (\<lambda>t. a5 * t^5 + a3 * (t^3 / c) - a2 * exp (t^2) + a1 * cos t + a0) =
   (\<lambda>t. 5 * a5 * t^4 + 3 * a3 * (t^2 / c) - 2 * a2 * t * exp (t^2) - a1 * sin t) on T"
   by(auto intro!: poly_derivatives)
 
 lemma "c \<noteq> 0 \<Longrightarrow> D (\<lambda>t. - a3 * exp (t^3 / c) + a1 * sin t + a2 * t^2) =
   (\<lambda>t. a1 * cos t + 2 * a2 * t - 3 * a3 * t^2 / c * exp (t^3 / c)) on T"
   apply(intro poly_derivatives)
   using poly_derivatives(1,2) by force+
 
 lemma "c \<noteq> 0 \<Longrightarrow> D (\<lambda>t. exp (a * sin (cos (t^4) / c))) =
 (\<lambda>t. - 4 * a * t^3 * sin (t^4) / c * cos (cos (t^4) / c) * exp (a * sin (cos (t^4) / c))) on T"
   apply(intro poly_derivatives)
   using poly_derivatives(1,2) by force+
 
 
+subsection \<open> Intermediate Value Theorem \<close>
+
+lemma IVT_two_functions:
+  fixes f :: "('a::{linear_continuum_topology, real_vector}) \<Rightarrow> 
+  ('b::{linorder_topology,real_normed_vector,ordered_ab_group_add})"
+  assumes conts: "continuous_on {a..b} f" "continuous_on {a..b} g"
+      and ahyp: "f a < g a" and bhyp: "g b < f b " and "a \<le> b"
+    shows "\<exists>x\<in>{a..b}. f x = g x"
+proof-
+  let "?h x" = "f x - g x"
+  have "?h a \<le> 0" and "?h b \<ge> 0"
+    using ahyp bhyp by simp_all
+  also have "continuous_on {a..b} ?h"
+    using conts continuous_on_diff by blast 
+  ultimately obtain x where "a \<le> x" "x \<le> b" and "?h x = 0"
+    using IVT'[of "?h"] \<open>a \<le> b\<close> by blast
+  thus ?thesis
+    using \<open>a \<le> b\<close> by auto
+qed
+
+lemma IVT_two_functions_real_ivl:
+  fixes f :: "real \<Rightarrow> real"
+  assumes conts: "continuous_on {a--b} f" "continuous_on {a--b} g"
+      and ahyp: "f a < g a" and bhyp: "g b < f b "
+    shows "\<exists>x\<in>{a--b}. f x = g x"
+proof(cases "a \<le> b")
+  case True
+  then show ?thesis 
+    using IVT_two_functions assms 
+    unfolding closed_segment_eq_real_ivl by auto
+next
+  case False
+  hence "a \<ge> b"
+    by auto
+  hence "continuous_on {b..a} f" "continuous_on {b..a} g"
+    using conts False unfolding closed_segment_eq_real_ivl by auto
+  hence "\<exists>x\<in>{b..a}. g x = f x"
+    using IVT_two_functions[of b a g f] assms(3,4) False by auto
+  then show ?thesis  
+    using \<open>a \<ge> b\<close> unfolding closed_segment_eq_real_ivl by auto force
+qed
+
+
 subsection \<open> Filters \<close>
 
 lemma eventually_at_within_mono:
   assumes "t \<in> interior T" and "T \<subseteq> S"
     and "eventually P (at t within T)"
   shows "eventually P (at t within S)"
   by (meson assms eventually_within_interior interior_mono subsetD)
 
 lemma netlimit_at_within_mono:
   fixes t::"'a::{perfect_space,t2_space}"
   assumes "t \<in> interior T" and "T \<subseteq> S"
   shows "netlimit (at t within S) = t"
   using assms(1) interior_mono[OF \<open>T \<subseteq> S\<close>] netlimit_within_interior by auto
 
 lemma has_derivative_at_within_mono:
   assumes "(t::real) \<in> interior T" and "T \<subseteq> S"
     and "D f \<mapsto> f' at t within T"
   shows "D f \<mapsto> f' at t within S"
   using assms(3) apply(unfold has_derivative_def tendsto_iff, safe)
   unfolding netlimit_at_within_mono[OF assms(1,2)] netlimit_within_interior[OF assms(1)]
   by (rule eventually_at_within_mono[OF assms(1,2)]) simp
 
 lemma eventually_all_finite2:
   fixes P :: "('a::finite) \<Rightarrow> 'b \<Rightarrow> bool"
   assumes h:"\<forall>i. eventually (P i) F"
   shows "eventually (\<lambda>x. \<forall>i. P i x) F"
 proof(unfold eventually_def)
   let ?F = "Rep_filter F"
   have obs: "\<forall>i. ?F (P i)"
     using h by auto
   have "?F (\<lambda>x. \<forall>i \<in> UNIV. P i x)"
     apply(rule finite_induct)
     by(auto intro: eventually_conj simp: obs h)
   thus "?F (\<lambda>x. \<forall>i. P i x)"
     by simp
 qed
 
 lemma eventually_all_finite_mono:
   fixes P :: "('a::finite) \<Rightarrow> 'b \<Rightarrow> bool"
   assumes h1: "\<forall>i. eventually (P i) F"
       and h2: "\<forall>x. (\<forall>i. (P i x)) \<longrightarrow> Q x"
   shows "eventually Q F"
 proof-
   have "eventually (\<lambda>x. \<forall>i. P i x) F"
     using h1 eventually_all_finite2 by blast
   thus "eventually Q F"
     unfolding eventually_def
     using h2 eventually_mono by auto
 qed
 
 
 subsection \<open> Multivariable derivatives \<close>
 
 lemma frechet_vec_lambda:
   fixes f::"real \<Rightarrow> ('a::banach)^('m::finite)" and x::real and T::"real set"
   defines "x\<^sub>0 \<equiv> netlimit (at x within T)" and "m \<equiv> real CARD('m)"
   assumes "\<forall>i. ((\<lambda>y. (f y $ i - f x\<^sub>0 $ i - (y - x\<^sub>0) *\<^sub>R f' x $ i) /\<^sub>R (\<parallel>y - x\<^sub>0\<parallel>)) \<longlongrightarrow> 0) (at x within T)"
   shows "((\<lambda>y. (f y - f x\<^sub>0 - (y - x\<^sub>0) *\<^sub>R f' x) /\<^sub>R (\<parallel>y - x\<^sub>0\<parallel>)) \<longlongrightarrow> 0) (at x within T)"
 proof(simp add: tendsto_iff, clarify)
   fix \<epsilon>::real assume "0 < \<epsilon>"
   let "?\<Delta>" = "\<lambda>y. y - x\<^sub>0" and "?\<Delta>f" = "\<lambda>y. f y - f x\<^sub>0"
   let "?P" = "\<lambda>i e y. inverse \<bar>?\<Delta> y\<bar> * (\<parallel>f y $ i - f x\<^sub>0 $ i - ?\<Delta> y *\<^sub>R f' x $ i\<parallel>) < e"
     and "?Q" = "\<lambda>y. inverse \<bar>?\<Delta> y\<bar> * (\<parallel>?\<Delta>f y - ?\<Delta> y *\<^sub>R f' x\<parallel>) < \<epsilon>"
   have "0 < \<epsilon> / sqrt m"
     using \<open>0 < \<epsilon>\<close> by (auto simp: assms)
   hence "\<forall>i. eventually (\<lambda>y. ?P i (\<epsilon> / sqrt m) y) (at x within T)"
     using assms unfolding tendsto_iff by simp
   thus "eventually ?Q (at x within T)"
   proof(rule eventually_all_finite_mono, simp add: norm_vec_def L2_set_def, clarify)
     fix t::real
     let ?c = "inverse \<bar>t - x\<^sub>0\<bar>" and "?u t" = "\<lambda>i. f t $ i - f x\<^sub>0 $ i - ?\<Delta> t *\<^sub>R f' x $ i"
     assume hyp:"\<forall>i. ?c * (\<parallel>?u t i\<parallel>) < \<epsilon> / sqrt m"
     hence "\<forall>i. (?c *\<^sub>R (\<parallel>?u t i\<parallel>))\<^sup>2 < (\<epsilon> / sqrt m)\<^sup>2"
       by (simp add: power_strict_mono)
     hence "\<forall>i. ?c\<^sup>2 * ((\<parallel>?u t i\<parallel>))\<^sup>2 < \<epsilon>\<^sup>2 / m"
       by (simp add: power_mult_distrib power_divide assms)
     hence "\<forall>i. ?c\<^sup>2 * ((\<parallel>?u t i\<parallel>))\<^sup>2 < \<epsilon>\<^sup>2 / m"
       by (auto simp: assms)
     also have "({}::'m set) \<noteq> UNIV \<and> finite (UNIV :: 'm set)"
       by simp
     ultimately have "(\<Sum>i\<in>UNIV. ?c\<^sup>2 * ((\<parallel>?u t i\<parallel>))\<^sup>2) < (\<Sum>(i::'m)\<in>UNIV. \<epsilon>\<^sup>2 / m)"
       by (metis (lifting) sum_strict_mono)
     moreover have "?c\<^sup>2 * (\<Sum>i\<in>UNIV. (\<parallel>?u t i\<parallel>)\<^sup>2) = (\<Sum>i\<in>UNIV. ?c\<^sup>2 *  (\<parallel>?u t i\<parallel>)\<^sup>2)"
       using sum_distrib_left by blast
     ultimately have "?c\<^sup>2 * (\<Sum>i\<in>UNIV. (\<parallel>?u t i\<parallel>)\<^sup>2) < \<epsilon>\<^sup>2"
       by (simp add: assms)
     hence "sqrt (?c\<^sup>2 * (\<Sum>i\<in>UNIV. (\<parallel>?u t i\<parallel>)\<^sup>2)) < sqrt (\<epsilon>\<^sup>2)"
       using real_sqrt_less_iff by blast
     also have "... = \<epsilon>"
       using \<open>0 < \<epsilon>\<close> by auto
     moreover have "?c * sqrt (\<Sum>i\<in>UNIV. (\<parallel>?u t i\<parallel>)\<^sup>2) = sqrt (?c\<^sup>2 * (\<Sum>i\<in>UNIV. (\<parallel>?u t i\<parallel>)\<^sup>2))"
       by (simp add: real_sqrt_mult)
     ultimately show "?c * sqrt (\<Sum>i\<in>UNIV. (\<parallel>?u t i\<parallel>)\<^sup>2) < \<epsilon>"
       by simp
   qed
 qed
 
 lemma tendsto_norm_bound:
   "\<forall>x. \<parallel>G x - L\<parallel> \<le> \<parallel>F x - L\<parallel> \<Longrightarrow> (F \<longlongrightarrow> L) net \<Longrightarrow> (G \<longlongrightarrow> L) net"
   apply(unfold tendsto_iff dist_norm, clarsimp)
   apply(rule_tac P="\<lambda>x. \<parallel>F x - L\<parallel> < e" in eventually_mono, simp)
   by (rename_tac e z) (erule_tac x=z in allE, simp)
 
 lemma tendsto_zero_norm_bound:
   "\<forall>x. \<parallel>G x\<parallel> \<le> \<parallel>F x\<parallel> \<Longrightarrow> (F \<longlongrightarrow> 0) net \<Longrightarrow> (G \<longlongrightarrow> 0) net"
   apply(unfold tendsto_iff dist_norm, clarsimp)
   apply(rule_tac P="\<lambda>x. \<parallel>F x\<parallel> < e" in eventually_mono, simp)
   by (rename_tac e z) (erule_tac x=z in allE, simp)
 
 lemma frechet_vec_nth:
   fixes f::"real \<Rightarrow> ('a::real_normed_vector)^'m"
   assumes "((\<lambda>x. (f x - f x\<^sub>0 - (x - x\<^sub>0) *\<^sub>R f' t) /\<^sub>R (\<parallel>x - x\<^sub>0\<parallel>)) \<longlongrightarrow> 0) (at t within T)"
   shows "((\<lambda>x. (f x $ i - f x\<^sub>0 $ i - (x - x\<^sub>0) *\<^sub>R f' t $ i) /\<^sub>R (\<parallel>x - x\<^sub>0\<parallel>)) \<longlongrightarrow> 0) (at t within T)"
   apply(rule_tac F="(\<lambda>x. (f x - f x\<^sub>0 - (x - x\<^sub>0) *\<^sub>R f' t) /\<^sub>R (\<parallel>x - x\<^sub>0\<parallel>))" in tendsto_zero_norm_bound)
    apply(clarsimp, rule mult_left_mono)
     apply (metis Finite_Cartesian_Product.norm_nth_le vector_minus_component vector_scaleR_component)
   using assms by simp_all
 
 lemma has_derivative_vec_lambda:
   fixes f::"real \<Rightarrow> ('a::banach)^('n::finite)"
   assumes "\<forall>i. D (\<lambda>t. f t $ i) \<mapsto> (\<lambda> h. h *\<^sub>R f' x $ i) (at x within T)"
   shows "D f \<mapsto> (\<lambda>h. h *\<^sub>R f' x) at x within T"
   apply(unfold has_derivative_def, safe)
    apply(force simp: bounded_linear_def bounded_linear_axioms_def)
   using assms frechet_vec_lambda[of x T ] unfolding has_derivative_def by auto
 
 lemma has_derivative_vec_nth:
   assumes "D f \<mapsto> (\<lambda>h. h *\<^sub>R f' x) at x within T"
   shows "D (\<lambda>t. f t $ i) \<mapsto> (\<lambda>h. h *\<^sub>R f' x $ i) at x within T"
   apply(unfold has_derivative_def, safe)
    apply(force simp: bounded_linear_def bounded_linear_axioms_def)
   using frechet_vec_nth assms unfolding has_derivative_def by auto
 
 lemma has_vderiv_on_vec_eq[simp]:
   fixes x::"real \<Rightarrow> ('a::banach)^('n::finite)"
   shows "(D x = x' on T) = (\<forall>i. D (\<lambda>t. x t $ i) = (\<lambda>t. x' t $ i) on T)"
   unfolding has_vderiv_on_def has_vector_derivative_def apply safe
   using has_derivative_vec_nth has_derivative_vec_lambda by blast+
 
 end
\ No newline at end of file