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,350 +1,412 @@
 (*  Title:       Preliminaries for hybrid systems verification
-    Author:      Jonathan Julián Huerta y Munive, 2020
+    Author:      Jonathan Julián Huerta y Munive, 2021
     Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
 *)
 
 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
 
-\<comment> \<open> Syntax \<close>
+\<comment> \<open> Notation \<close>
+
+bundle derivative_notation
+begin
 
 no_notation has_vderiv_on (infix "(has'_vderiv'_on)" 50)
 
 notation has_derivative ("(1(D _ \<mapsto> (_))/ _)" [65,65] 61)
      and has_vderiv_on ("(1 D _ = (_)/ on _)" [65,65] 61)
-     and norm ("(1\<parallel>_\<parallel>)" [65] 61)
+
+end
+
+bundle derivative_no_notation
+begin
+
+notation has_vderiv_on (infix "(has'_vderiv'_on)" 50)
+
+no_notation has_derivative ("(1(D _ \<mapsto> (_))/ _)" [65,65] 61)
+     and has_vderiv_on ("(1 D _ = (_)/ on _)" [65,65] 61)
+
+end
+
+unbundle derivative_notation
+
+notation norm ("\<parallel>_\<parallel>")
 
 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 is_interval_real_nonneg[simp]: "is_interval (Collect ((\<le>) (0::real)))"
   by (auto simp: is_interval_def)
 
 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
 
+lemma sum_eq_Sum:
+  assumes "inj_on f A"
+  shows "(\<Sum>x\<in>A. f x) = (\<Sum> {f x |x. x \<in> A})"
+proof-
+  have "(\<Sum> {f x |x. x \<in> A}) = (\<Sum> (f ` A))"
+    apply(auto simp: image_def)
+    by (rule_tac f=Sum in arg_cong, auto)
+  also have "... = (\<Sum>x\<in>A. f x)"
+    by (subst sum.image_eq[OF assms], simp)
+  finally show "(\<Sum>x\<in>A. f x) = (\<Sum> {f x |x. x \<in> A})"
+    by simp
+qed
+
+lemma triangle_norm_vec_le_sum: "\<parallel>x\<parallel> \<le> (\<Sum>i\<in>UNIV. \<parallel>x $ i\<parallel>)"
+  by (simp add: L2_set_le_sum norm_vec_def)
+
 
 subsection \<open> Single variable derivatives \<close>
 
 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]
     and has_vderiv_on_ln[poly_derivatives]
 
 lemma vderiv_on_composeI:
   assumes "D f = f' on g ` T" 
     and " D g = g' on T"
     and "h = (\<lambda>t. g' t *\<^sub>R f' (g t))"
   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_uminusI[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_npowI[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"
   using assms unfolding has_vderiv_on_def has_vector_derivative_def 
   by (auto intro: derivative_eq_intros simp: field_simps)
 
 lemma vderiv_divI[poly_derivatives]:
   assumes "\<forall>t\<in>T. g t \<noteq> (0::real)" and "D f = f' on T"and "D g = g' on T" 
     and "h = (\<lambda>t. (f' t * g t - f t * (g' t)) / (g t)^2)"
   shows "D (\<lambda>t. (f t)/(g t)) = h on T"
   apply(subgoal_tac "(\<lambda>t. (f t)/(g t)) = (\<lambda>t. (f t) * (1/(g t)))")
    apply(erule ssubst, rule poly_derivatives(5)[OF assms(2)])
   apply(rule vderiv_on_composeI[where g=g and f="\<lambda>t. 1/t" and f'="\<lambda>t. - 1/t^2", OF _ assms(3)])
   apply(subst has_vderiv_on_def, subst has_vector_derivative_def, clarsimp)
    using assms(1) apply(force intro!: derivative_eq_intros simp: fun_eq_iff power2_eq_square)
    using assms by (auto simp: field_simps power2_eq_square)
 
 lemma vderiv_cosI[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"
   apply(rule vderiv_on_composeI[OF _ assms(1), of "\<lambda>t. cos t"])
   unfolding has_vderiv_on_def has_vector_derivative_def 
   by (auto intro!: derivative_eq_intros simp: assms)
 
 lemma vderiv_sinI[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"
   apply(rule vderiv_on_composeI[OF _ assms(1), of "\<lambda>t. sin t"])
   unfolding has_vderiv_on_def has_vector_derivative_def 
   by (auto intro!: derivative_eq_intros simp: assms)
 
 lemma vderiv_expI[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"
   apply(rule vderiv_on_composeI[OF _ assms(1), of "\<lambda>t. exp t"])
   unfolding has_vderiv_on_def has_vector_derivative_def 
   by (auto intro!: derivative_eq_intros simp: assms)
 
 \<comment> \<open>Examples for checking derivatives\<close>
 
 lemma "D (*) a = (\<lambda>t. a) on T"
   by (auto intro!: poly_derivatives)
 
 lemma "a \<noteq> 0 \<Longrightarrow> D (\<lambda>t. t/a) = (\<lambda>t. 1/a) on T"
   by (auto intro!: poly_derivatives simp: power2_eq_square)
 
 lemma "(a::real) \<noteq> 0 \<Longrightarrow> D f = f' on T \<Longrightarrow> g = (\<lambda>t. (f' t)/a) \<Longrightarrow> D (\<lambda>t. (f t)/a) = g on T"
   by (auto intro!: poly_derivatives simp: power2_eq_square)
 
 lemma "\<forall>t\<in>T. f t \<noteq> (0::real) \<Longrightarrow> D f = f' on T \<Longrightarrow> g = (\<lambda>t. - a * f' t / (f t)^2) \<Longrightarrow> 
   D (\<lambda>t. a/(f t)) = g on T"
   by (auto intro!: poly_derivatives simp: power2_eq_square)
 
 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 "D x = x' on (\<lambda>\<tau>. \<tau> + t) ` T \<Longrightarrow> D (\<lambda>\<tau>. x (\<tau> + t)) = (\<lambda>\<tau>. x' (\<tau> + t)) on T"
   by (rule vderiv_on_composeI, auto intro: poly_derivatives)
 
 lemma "a \<noteq> 0 \<Longrightarrow> D (\<lambda>t. t/a) = (\<lambda>t. 1/a) on T"
   by (auto intro!: poly_derivatives simp: power2_eq_square)
 
 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 simp: power2_eq_square)
 
 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"
   by(auto intro!: poly_derivatives simp: power2_eq_square)
 
 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"
   by (intro poly_derivatives) (auto intro!: poly_derivatives simp: power2_eq_square)
 
 
 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>
 
 definition vec_upd :: "('a^'b) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'a^'b"
   where "vec_upd s i a = (\<chi> j. ((($) s)(i := a)) j)"
 
 lemma vec_upd_eq: "vec_upd s i a = (\<chi> j. if j = i then a else s$j)"
   by (simp add: vec_upd_def)
 
-lemma frechet_vec_lambda:
+lemma has_derivative_vec_nth[derivative_intros]: 
+  "D (\<lambda>s. s $ i) \<mapsto> (\<lambda>s. s $ i) (at x within S)"
+  by (clarsimp simp: has_derivative_within) standard
+
+lemma bounded_linear_component:
+  "(bounded_linear f) \<longleftrightarrow> (\<forall>i. bounded_linear (\<lambda>x. (f x) $ i))" (is "?lhs = ?rhs")
+proof
+  assume ?lhs 
+  thus ?rhs
+    apply(clarsimp, rule_tac f="(\<lambda>x. x $ i)" in bounded_linear_compose)
+     apply(simp_all add: bounded_linear_def bounded_linear_axioms_def linear_iff)
+    by (rule_tac x=1 in exI, clarsimp) (meson Finite_Cartesian_Product.norm_nth_le)
+next
+  assume ?rhs
+  hence "(\<forall>i. \<exists>K. \<forall>x. \<parallel>f x $ i\<parallel> \<le> \<parallel>x\<parallel> * K)" "linear f"
+    by (auto simp: bounded_linear_def bounded_linear_axioms_def linear_iff vec_eq_iff)
+  then obtain F where F: "\<And>i x. \<parallel>f x $ i\<parallel> \<le> \<parallel>x\<parallel> * F i"
+    by metis
+  have "\<parallel>f x\<parallel> \<le> \<parallel>x\<parallel> * sum F UNIV" for x
+  proof -
+    have "norm (f x) \<le> (\<Sum>i\<in>UNIV. \<parallel>f x $ i\<parallel>)"
+      by (simp add: L2_set_le_sum norm_vec_def)
+    also have "... \<le> (\<Sum>i\<in>UNIV. norm x * F i)"
+      by (metis F sum_mono)
+    also have "... = norm x * sum F UNIV"
+      by (simp add: sum_distrib_left)
+    finally show ?thesis .
+  qed
+  then show ?lhs
+    by (force simp: bounded_linear_def bounded_linear_axioms_def \<open>linear f\<close>)
+qed
+
+lemma open_preimage_nth:
+  "open S \<Longrightarrow> open {s::('a::real_normed_vector^'n::finite). s $ i \<in> S}"
+  unfolding open_contains_ball apply clarsimp
+  apply(erule_tac x="x$i" in ballE; clarsimp)
+  apply(rule_tac x=e in exI; clarsimp simp: dist_norm subset_eq ball_def)
+  apply(rename_tac x e y, erule_tac x="y$i" in allE)
+  using Finite_Cartesian_Product.norm_nth_le
+  by (metis le_less_trans vector_minus_component)
+
+lemma tendsto_nth_iff: \<comment> \<open> following @{thm tendsto_componentwise_iff} \<close>
+  fixes l::"'a::real_normed_vector^'n::finite"
+  defines "m \<equiv> real CARD('n)"
+  shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i. ((\<lambda>x. f x $ i) \<longlongrightarrow> l $ i) F)" (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  thus ?rhs
+    unfolding tendsto_def
+    by (clarify, drule_tac x="{s. s $ i \<in> S}" in spec) (auto simp: open_preimage_nth)
+next
+  assume ?rhs
+  thus ?lhs
+  proof(unfold tendsto_iff dist_norm, clarify)
+    fix \<epsilon>::real assume "0 < \<epsilon>"
+    assume evnt_h: "\<forall>i \<epsilon>. 0 < \<epsilon> \<longrightarrow> (\<forall>\<^sub>F x in F. \<parallel>f x $ i - l $ i\<parallel> < \<epsilon>)"
+    {fix x assume hyp: "\<forall>i. \<parallel>f x $ i - l $ i\<parallel> < (\<epsilon>/m)"
+      have "\<parallel>f x - l\<parallel> \<le> (\<Sum>i\<in>UNIV. \<parallel>f x $ i - l $ i\<parallel>)"
+        using triangle_norm_vec_le_sum[of "f x - l"] by auto
+      also have "... < (\<Sum>(i::'n)\<in>UNIV. (\<epsilon>/m))"
+        apply(rule sum_strict_mono[of UNIV "\<lambda>i. \<parallel>f x $ i - l $ i\<parallel>" "\<lambda>i. \<epsilon>/m"])
+        using hyp by auto
+      also have "... = m * (\<epsilon>/m)"
+        unfolding assms by simp
+      finally have "\<parallel>f x - l\<parallel> < \<epsilon>" 
+        unfolding assms by simp}
+    hence key: "\<And>x. \<forall>i. \<parallel>f x $ i - l $ i\<parallel> < (\<epsilon>/m) \<Longrightarrow> \<parallel>f x - l\<parallel> < \<epsilon>"
+      by blast
+    have obs: "\<forall>\<^sub>F x in F. \<forall>i. \<parallel>f x $ i - l $ i\<parallel> < (\<epsilon>/m)"
+      apply(rule eventually_all_finite)
+      using \<open>0 < \<epsilon>\<close> evnt_h unfolding assms by auto
+    thus "\<forall>\<^sub>F x in F. \<parallel>f x - l\<parallel> < \<epsilon>"
+      by (rule eventually_mono[OF _ key], simp)
+  qed
+qed
+
+lemma has_derivative_component[simp]: \<comment> \<open> following @{thm has_derivative_componentwise_within} \<close>
+  "(D f \<mapsto> f' at x within S) \<longleftrightarrow> (\<forall>i. D (\<lambda>s. f s $ i) \<mapsto> (\<lambda>s. f' s $ i) at x within S)"
+  by (simp add: has_derivative_within tendsto_nth_iff 
+      bounded_linear_component all_conj_distrib)
+
+lemma has_vderiv_on_component[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 by auto
+
+lemma frechet_tendsto_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
+  using assms by (simp add: tendsto_nth_iff)
 
 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:
+lemma frechet_tendsto_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
diff --git a/thys/Hybrid_Systems_VCs/HS_VC_Examples.thy b/thys/Hybrid_Systems_VCs/HS_VC_Examples.thy
--- a/thys/Hybrid_Systems_VCs/HS_VC_Examples.thy
+++ b/thys/Hybrid_Systems_VCs/HS_VC_Examples.thy
@@ -1,357 +1,357 @@
 (*  Title:       Examples of hybrid systems verifications
     Author:      Jonathan Julián Huerta y Munive, 2020
     Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
 *)
 
 subsection \<open> Examples \<close>
 
 text \<open> We prove partial correctness specifications of some hybrid systems with our
 verification components.\<close>
 
 theory HS_VC_Examples
   imports HS_VC_Spartan
 
 begin
 
 
 subsubsection \<open>Pendulum\<close>
 
 text \<open> The ODEs @{text "x' t = y t"} and {text "y' t = - x t"} describe the circular motion of
 a mass attached to a string looked from above. We use @{text "s$1"} to represent the x-coordinate
 and @{text "s$2"} for the y-coordinate. We prove that this motion remains circular. \<close>
 
 abbreviation fpend :: "real^2 \<Rightarrow> real^2" ("f")
   where "f s \<equiv> (\<chi> i. if i = 1 then s$2 else -s$1)"
 
 abbreviation pend_flow :: "real \<Rightarrow> real^2 \<Rightarrow> real^2" ("\<phi>")
   where "\<phi> t s \<equiv> (\<chi> i. if i = 1 then s$1 * cos t + s$2 * sin t else - s$1 * sin t + s$2 * cos t)"
 
 \<comment> \<open>Verified with annotated dynamics. \<close>
 
 lemma pendulum_dyn: "(\<lambda>s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2) \<le> |EVOL \<phi> G T] (\<lambda>s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2)"
   by force
 
 \<comment> \<open>Verified with differential invariants. \<close>
 
 lemma pendulum_inv: "(\<lambda>s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2) \<le> |x\<acute>= f & G] (\<lambda>s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2)"
   by (auto intro!: diff_invariant_rules poly_derivatives)
 
 \<comment> \<open>Verified with the flow. \<close>
 
 lemma local_flow_pend: "local_flow f UNIV UNIV \<phi>"
   apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def vec_eq_iff, clarsimp)
     apply(rule_tac x="1" in exI, clarsimp, rule_tac x=1 in exI)
     apply(simp add: dist_norm norm_vec_def L2_set_def power2_commute UNIV_2)
   by (auto simp: forall_2 intro!: poly_derivatives)
 
 lemma pendulum_flow: "(\<lambda>s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2) \<le> |x\<acute>=f & G] (\<lambda>s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2)"
   by (force simp: local_flow.fbox_g_ode_subset[OF local_flow_pend])
 
 no_notation fpend ("f")
         and pend_flow ("\<phi>")
 
 
 subsubsection \<open> Bouncing Ball \<close>
 
 text \<open> A ball is dropped from rest at an initial height @{text "h"}. The motion is described with
 the free-fall equations @{text "x' t = v t"} and @{text "v' t = g"} where @{text "g"} is the
 constant acceleration due to gravity. The bounce is modelled with a variable assignment that
 flips the velocity. That is, we model it as a completely elastic collision with the ground. We use 
 @{text "s$1"} to represent the ball's height and @{text "s$2"} for its velocity. We prove that the 
 ball remains above ground and below its initial resting position. \<close>
 
 abbreviation fball :: "real \<Rightarrow> real^2 \<Rightarrow> real^2" ("f")
   where "f g s \<equiv> (\<chi> i. if i = 1 then s$2 else g)"
 
 abbreviation ball_flow :: "real \<Rightarrow> real \<Rightarrow> real^2 \<Rightarrow> real^2" ("\<phi>")
   where "\<phi> g t s \<equiv> (\<chi> i. if i = 1 then g * t ^ 2/2 + s$2 * t + s$1 else g * t + s$2)"
 
 \<comment> \<open>Verified with differential invariants. \<close>
 
 named_theorems bb_real_arith "real arithmetic properties for the bouncing ball."
 
 lemma inv_imp_pos_le[bb_real_arith]:
   assumes "0 > g" and inv: "2 * g * x - 2 * g * h = v * v"
   shows "(x::real) \<le> h"
 proof-
   have "v * v = 2 * g * x - 2 * g * h \<and> 0 > g"
     using inv and \<open>0 > g\<close> by auto
   hence obs:"v * v = 2 * g * (x - h) \<and> 0 > g \<and> v * v \<ge> 0"
     using left_diff_distrib mult.commute by (metis zero_le_square)
   hence "(v * v)/(2 * g) = (x - h)"
     by auto
   also from obs have "(v * v)/(2 * g) \<le> 0"
     using divide_nonneg_neg by fastforce
   ultimately have "h - x \<ge> 0"
     by linarith
   thus ?thesis by auto
 qed
 
 lemma "diff_invariant (\<lambda>s. 2 * g * s$1 - 2 * g * h - s$2 * s$2 = 0) (\<lambda>t. f g) (\<lambda>s. UNIV) S t\<^sub>0 G"
   by (auto intro!: poly_derivatives diff_invariant_rules)
 
 lemma bouncing_ball_inv: "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow>
   (\<lambda>s. s$1 = h \<and> s$2 = 0) \<le>
   |LOOP (
     (x\<acute>=(f g) & (\<lambda> s. s$1 \<ge> 0) DINV (\<lambda>s. 2 * g * s$1 - 2 * g * h - s$2 * s$2 = 0)) ;
     (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip))
   INV (\<lambda>s. 0 \<le> s$1 \<and> 2 * g * s$1 - 2 * g * h - s$2 * s$2 = 0)]
   (\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h)"
   apply(rule fbox_loopI, simp_all, force, force simp: bb_real_arith)
   by (rule fbox_g_odei) (auto intro!: poly_derivatives diff_invariant_rules)
 
 \<comment> \<open>Verified with annotated dynamics. \<close>
 
 lemma inv_conserv_at_ground[bb_real_arith]:
   assumes invar: "2 * g * x = 2 * g * h + v * v"
     and pos: "g * \<tau>\<^sup>2 / 2 + v * \<tau> + (x::real) = 0"
   shows "2 * g * h + (g * \<tau> + v) * (g * \<tau> + v) = 0"
 proof-
   from pos have "g * \<tau>\<^sup>2  + 2 * v * \<tau> + 2 * x = 0" by auto
   then have "g\<^sup>2 * \<tau>\<^sup>2  + 2 * g * v * \<tau> + 2 * g * x = 0"
-    by (metis (mono_tags, opaque_lifting) Groups.mult_ac(1,3) mult_zero_right
+    by (metis (mono_tags) Groups.mult_ac(1,3) mult_zero_right
         monoid_mult_class.power2_eq_square semiring_class.distrib_left)
   hence "g\<^sup>2 * \<tau>\<^sup>2 + 2 * g * v * \<tau> + v\<^sup>2 + 2 * g * h = 0"
     using invar by (simp add: monoid_mult_class.power2_eq_square)
   hence obs: "(g * \<tau> + v)\<^sup>2 + 2 * g * h = 0"
-    apply(subst power2_sum) by (metis (no_types, opaque_lifting) Groups.add_ac(2, 3)
+    apply(subst power2_sum) by (metis (no_types) Groups.add_ac(2, 3)
         Groups.mult_ac(2, 3) monoid_mult_class.power2_eq_square nat_distrib(2))
   thus "2 * g * h + (g * \<tau> + v) * (g * \<tau> + v) = 0"
     by (simp add: add.commute distrib_right power2_eq_square)
 qed
 
 lemma inv_conserv_at_air[bb_real_arith]:
   assumes invar: "2 * g * x = 2 * g * h + v * v"
   shows "2 * g * (g * \<tau>\<^sup>2 / 2 + v * \<tau> + (x::real)) =
   2 * g * h + (g * \<tau> + v) * (g * \<tau> + v)" (is "?lhs = ?rhs")
 proof-
   have "?lhs = g\<^sup>2 * \<tau>\<^sup>2 + 2 * g * v * \<tau> + 2 * g * x"
     by(auto simp: algebra_simps semiring_normalization_rules(29))
   also have "... = g\<^sup>2 * \<tau>\<^sup>2 + 2 * g * v * \<tau> + 2 * g * h + v * v" (is "... = ?middle")
     by(subst invar, simp)
   finally have "?lhs = ?middle".
   moreover
   {have "?rhs = g * g * (\<tau> * \<tau>) + 2 * g * v * \<tau> + 2 * g * h + v * v"
     by (simp add: Groups.mult_ac(2,3) semiring_class.distrib_left)
   also have "... = ?middle"
     by (simp add: semiring_normalization_rules(29))
   finally have "?rhs = ?middle".}
   ultimately show ?thesis by auto
 qed
 
 lemma bouncing_ball_dyn: "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow>
   (\<lambda>s. s$1 = h \<and> s$2 = 0) \<le>
   |LOOP (
     (EVOL (\<phi> g) (\<lambda> s. s$1 \<ge> 0) T) ;
     (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip))
   INV (\<lambda>s. 0 \<le> s$1 \<and>2 * g * s$1 = 2 * g * h + s$2 * s$2)]
   (\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h)"
   by (rule fbox_loopI) (auto simp: bb_real_arith)
 
 \<comment> \<open>Verified with the flow. \<close>
 
 lemma local_flow_ball: "local_flow (f g) UNIV UNIV (\<phi> g)"
   apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def vec_eq_iff, clarsimp)
     apply(rule_tac x="1/2" in exI, clarsimp, rule_tac x=1 in exI)
     apply(simp add: dist_norm norm_vec_def L2_set_def UNIV_2)
   by (auto simp: forall_2 intro!: poly_derivatives)
 
 lemma bouncing_ball_flow: "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow>
   (\<lambda>s. s$1 = h \<and> s$2 = 0) \<le>
   |LOOP (
     (x\<acute>=(\<lambda>t. f g) & (\<lambda> s. s$1 \<ge> 0) on (\<lambda>s. UNIV) UNIV @ 0) ;
     (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip))
   INV (\<lambda>s. 0 \<le> s$1 \<and>2 * g * s$1 = 2 * g * h + s$2 * s$2)]
   (\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h)"
   apply(rule fbox_loopI, simp_all add: local_flow.fbox_g_ode_subset[OF local_flow_ball])
   by (auto simp: bb_real_arith)
 
 no_notation fball ("f")
         and ball_flow ("\<phi>")
 
 
 subsubsection \<open> Thermostat \<close>
 
 text \<open> A thermostat has a chronometer, a thermometer and a switch to turn on and off a heater.
 At most every @{text "t"} minutes, it sets its chronometer to @{term "0::real"}, it registers
 the room temperature, and it turns the heater on (or off) based on this reading. The temperature
 follows the ODE @{text "T' = - a * (T - U)"} where @{text "U"} is @{text "L \<ge> 0"} when the heater
 is on, and @{text "0"} when it is off. We use @{term "1::4"} to denote the room's temperature,
 @{term "2::4"} is time as measured by the thermostat's chronometer, @{term "3::4"} is the
 temperature detected by the thermometer, and @{term "4::4"} states whether the heater is on
 (@{text "s$4 = 1"}) or off (@{text "s$4 = 0"}). We prove that the thermostat keeps the room's
 temperature between @{text "Tmin"} and @{text "Tmax"}. \<close>
 
 abbreviation temp_vec_field :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> real^4" ("f")
   where "f a L s \<equiv> (\<chi> i. if i = 2 then 1 else (if i = 1 then - a * (s$1 - L) else 0))"
 
 abbreviation temp_flow :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> real^4" ("\<phi>")
   where "\<phi> a L t s \<equiv> (\<chi> i. if i = 1 then - exp(-a * t) * (L - s$1) + L else
   (if i = 2 then t + s$2 else s$i))"
 
 \<comment> \<open>Verified with the flow. \<close>
 
 lemma norm_diff_temp_dyn: "0 < a \<Longrightarrow> \<parallel>f a L s\<^sub>1 - f a L s\<^sub>2\<parallel> = \<bar>a\<bar> * \<bar>s\<^sub>1$1 - s\<^sub>2$1\<bar>"
 proof(simp add: norm_vec_def L2_set_def, unfold UNIV_4, simp)
   assume a1: "0 < a"
   have f2: "\<And>r ra. \<bar>(r::real) + - ra\<bar> = \<bar>ra + - r\<bar>"
     by (metis abs_minus_commute minus_real_def)
   have "\<And>r ra rb. (r::real) * ra + - (r * rb) = r * (ra + - rb)"
     by (metis minus_real_def right_diff_distrib)
   hence "\<bar>a * (s\<^sub>1$1 + - L) + - (a * (s\<^sub>2$1 + - L))\<bar> = a * \<bar>s\<^sub>1$1 + - s\<^sub>2$1\<bar>"
     using a1 by (simp add: abs_mult)
   thus "\<bar>a * (s\<^sub>2$1 - L) - a * (s\<^sub>1$1 - L)\<bar> = a * \<bar>s\<^sub>1$1 - s\<^sub>2$1\<bar>"
     using f2 minus_real_def by presburger
 qed
 
 lemma local_lipschitz_temp_dyn:
   assumes "0 < (a::real)"
   shows "local_lipschitz UNIV UNIV (\<lambda>t::real. f a L)"
   apply(unfold local_lipschitz_def lipschitz_on_def dist_norm)
   apply(clarsimp, rule_tac x=1 in exI, clarsimp, rule_tac x=a in exI)
   using assms
   apply(simp add: norm_diff_temp_dyn)
   apply(simp add: norm_vec_def L2_set_def, unfold UNIV_4, clarsimp)
   unfolding real_sqrt_abs[symmetric] by (rule real_le_lsqrt) auto
 
 lemma local_flow_temp: "a > 0 \<Longrightarrow> local_flow (f a L) UNIV UNIV (\<phi> a L)"
   by (unfold_locales, auto intro!: poly_derivatives local_lipschitz_temp_dyn simp: forall_4 vec_eq_iff)
 
 lemma temp_dyn_down_real_arith:
   assumes "a > 0" and Thyps: "0 < Tmin" "Tmin \<le> T" "T \<le> Tmax"
     and thyps: "0 \<le> (t::real)" "\<forall>\<tau>\<in>{0..t}. \<tau> \<le> - (ln (Tmin / T) / a) "
   shows "Tmin \<le> exp (-a * t) * T" and "exp (-a * t) * T \<le> Tmax"
 proof-
   have "0 \<le> t \<and> t \<le> - (ln (Tmin / T) / a)"
     using thyps by auto
   hence "ln (Tmin / T) \<le> - a * t \<and> - a * t \<le> 0"
     using assms(1) divide_le_cancel by fastforce
   also have "Tmin / T > 0"
     using Thyps by auto
   ultimately have obs: "Tmin / T \<le> exp (-a * t)" "exp (-a * t) \<le> 1"
     using exp_ln exp_le_one_iff by (metis exp_less_cancel_iff not_less, simp)
   thus "Tmin \<le> exp (-a * t) * T"
     using Thyps by (simp add: pos_divide_le_eq)
   show "exp (-a * t) * T \<le> Tmax"
     using Thyps mult_left_le_one_le[OF _ exp_ge_zero obs(2), of T]
       less_eq_real_def order_trans_rules(23) by blast
 qed
 
 lemma temp_dyn_up_real_arith:
   assumes "a > 0" and Thyps: "Tmin \<le> T" "T \<le> Tmax" "Tmax < (L::real)"
     and thyps: "0 \<le> t" "\<forall>\<tau>\<in>{0..t}. \<tau> \<le> - (ln ((L - Tmax) / (L - T)) / a) "
   shows "L - Tmax \<le> exp (-(a * t)) * (L - T)"
     and "L - exp (-(a * t)) * (L - T) \<le> Tmax"
     and "Tmin \<le> L - exp (-(a * t)) * (L - T)"
 proof-
   have "0 \<le> t \<and> t \<le> - (ln ((L - Tmax) / (L - T)) / a)"
     using thyps by auto
   hence "ln ((L - Tmax) / (L - T)) \<le> - a * t \<and> - a * t \<le> 0"
     using assms(1) divide_le_cancel by fastforce
   also have "(L - Tmax) / (L - T) > 0"
     using Thyps by auto
   ultimately have "(L - Tmax) / (L - T) \<le> exp (-a * t) \<and> exp (-a * t) \<le> 1"
     using exp_ln exp_le_one_iff by (metis exp_less_cancel_iff not_less)
   moreover have "L - T > 0"
     using Thyps by auto
   ultimately have obs: "(L - Tmax) \<le> exp (-a * t) * (L - T) \<and> exp (-a * t) * (L - T) \<le> (L - T)"
     by (simp add: pos_divide_le_eq)
   thus "(L - Tmax) \<le> exp (-(a * t)) * (L - T)"
     by auto
   thus "L - exp (-(a * t)) * (L - T) \<le> Tmax"
     by auto
   show "Tmin \<le> L - exp (-(a * t)) * (L - T)"
     using Thyps and obs by auto
 qed
 
 lemmas fbox_temp_dyn = local_flow.fbox_g_ode_subset[OF local_flow_temp]
 
 lemma thermostat:
   assumes "a > 0" and "0 < Tmin" and "Tmax < L"
   shows "(\<lambda>s. Tmin \<le> s$1 \<and> s$1 \<le> Tmax \<and> s$4 = 0) \<le>
   |LOOP
     \<comment> \<open>control\<close>
     ((2 ::= (\<lambda>s. 0));(3 ::= (\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> Tmin + 1) THEN (4 ::= (\<lambda>s.1)) ELSE
     (IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> Tmax - 1) THEN (4 ::= (\<lambda>s.0)) ELSE skip));
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN (x\<acute>= f a 0 & (\<lambda>s. s$2 \<le> - (ln (Tmin/s$3))/a))
     ELSE (x\<acute>= f a L & (\<lambda>s. s$2 \<le> - (ln ((L-Tmax)/(L-s$3)))/a))) )
   INV (\<lambda>s. Tmin \<le>s$1 \<and> s$1 \<le> Tmax \<and> (s$4 = 0 \<or> s$4 = 1))]
   (\<lambda>s. Tmin \<le> s$1 \<and> s$1 \<le> Tmax)"
   apply(rule fbox_loopI, simp_all add: fbox_temp_dyn[OF assms(1)] le_fun_def)
   using temp_dyn_up_real_arith[OF assms(1) _ _ assms(3), of Tmin]
     and temp_dyn_down_real_arith[OF assms(1,2), of _ Tmax] by auto
 
 no_notation temp_vec_field ("f")
         and temp_flow ("\<phi>")
 
 subsubsection \<open> Tank \<close>
 
 text \<open> A controller turns a water pump on and off to keep the level of water @{text "h"} in a tank
 within an acceptable range @{text "hmin \<le> h \<le> hmax"}. Just like in the previous example, after 
 each intervention, the controller registers the current level of water and resets its chronometer,
 then it changes the status of the water pump accordingly. The level of water grows linearly 
 @{text "h' = k"} at a rate of @{text "k = c\<^sub>i-c\<^sub>o"} if the pump is on, and at a rate of 
 @{text "k = -c\<^sub>o"} if the pump is off. We use @{term "1::4"} to denote the tank's level of water,
 @{term "2::4"} is time as measured by the controller's chronometer, @{term "3::4"} is the
 level of water measured by the chronometer, and @{term "4::4"} states whether the pump is on
 (@{text "s$4 = 1"}) or off (@{text "s$4 = 0"}). We prove that the controller keeps the level of
 water between @{text "hmin"} and @{text "hmax"}. \<close>
 
 abbreviation tank_vec_field :: "real \<Rightarrow> real^4 \<Rightarrow> real^4" ("f")
   where "f k s \<equiv> (\<chi> i. if i = 2 then 1 else (if i = 1 then k else 0))"
 
 abbreviation tank_flow :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> real^4" ("\<phi>")
   where "\<phi> k \<tau> s \<equiv> (\<chi> i. if i = 1 then k * \<tau> + s$1 else 
   (if i = 2 then \<tau> + s$2 else s$i))"
 
 abbreviation tank_guard :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("G")
   where "G Hm k s \<equiv> s$2 \<le> (Hm - s$3)/k"
 
 abbreviation tank_loop_inv :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("I")
   where "I hmin hmax s \<equiv> hmin \<le> s$1 \<and> s$1 \<le> hmax \<and> (s$4 = 0 \<or> s$4 = 1)"
 
 abbreviation tank_diff_inv :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("dI")
   where "dI hmin hmax k s \<equiv> s$1 = k * s$2 + s$3 \<and> 0 \<le> s$2 \<and> 
     hmin \<le> s$3 \<and> s$3 \<le> hmax \<and> (s$4 =0 \<or> s$4 = 1)"
 
 lemma local_flow_tank: "local_flow (f k) UNIV UNIV (\<phi> k)"
   apply (unfold_locales, unfold local_lipschitz_def lipschitz_on_def, simp_all, clarsimp)
   apply(rule_tac x="1/2" in exI, clarsimp, rule_tac x=1 in exI)
   apply(simp add: dist_norm norm_vec_def L2_set_def, unfold UNIV_4)
   by (auto intro!: poly_derivatives simp: vec_eq_iff)
 
 lemma tank_arith:
   assumes "0 \<le> (\<tau>::real)" and "0 < c\<^sub>o" and "c\<^sub>o < c\<^sub>i"
   shows "\<forall>\<tau>\<in>{0..\<tau>}. \<tau> \<le> - ((hmin - y) / c\<^sub>o) \<Longrightarrow>  hmin \<le> y - c\<^sub>o * \<tau>"
     and "\<forall>\<tau>\<in>{0..\<tau>}. \<tau> \<le> (hmax - y) / (c\<^sub>i - c\<^sub>o) \<Longrightarrow>  (c\<^sub>i - c\<^sub>o) * \<tau> + y \<le> hmax"
     and "hmin \<le> y \<Longrightarrow> hmin \<le> (c\<^sub>i - c\<^sub>o) * \<tau> + y"
     and "y \<le> hmax \<Longrightarrow> y - c\<^sub>o * \<tau> \<le> hmax"
   apply(simp_all add: field_simps le_divide_eq assms)
   using assms apply (meson add_mono less_eq_real_def mult_left_mono)
   using assms by (meson add_increasing2 less_eq_real_def mult_nonneg_nonneg) 
 
 lemma tank_flow:
   assumes "0 < c\<^sub>o" and "c\<^sub>o < c\<^sub>i"
   shows "I hmin hmax \<le>
   |LOOP 
     \<comment> \<open>control\<close>
     ((2 ::=(\<lambda>s.0));(3 ::=(\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> hmin + 1) THEN (4 ::= (\<lambda>s.1)) ELSE 
     (IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> hmax - 1) THEN (4 ::= (\<lambda>s.0)) ELSE skip));
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN (x\<acute>= f (c\<^sub>i-c\<^sub>o) & (G hmax (c\<^sub>i-c\<^sub>o))) 
      ELSE (x\<acute>= f (-c\<^sub>o) & (G hmin (-c\<^sub>o)))) ) INV I hmin hmax]  
   I hmin hmax"
   apply(rule fbox_loopI, simp_all add: le_fun_def)
   apply(clarsimp simp: le_fun_def local_flow.fbox_g_ode_subset[OF local_flow_tank])
   using assms tank_arith[OF _ assms] by auto
 
 no_notation tank_vec_field ("f")
         and tank_flow ("\<phi>")
         and tank_loop_inv ("I")
         and tank_diff_inv ("dI")
         and tank_guard ("G")
 
 end
\ No newline at end of file
diff --git a/thys/Hybrid_Systems_VCs/KleeneAlgebraTests/HS_VC_KAT_Examples_ndfun.thy b/thys/Hybrid_Systems_VCs/KleeneAlgebraTests/HS_VC_KAT_Examples_ndfun.thy
--- a/thys/Hybrid_Systems_VCs/KleeneAlgebraTests/HS_VC_KAT_Examples_ndfun.thy
+++ b/thys/Hybrid_Systems_VCs/KleeneAlgebraTests/HS_VC_KAT_Examples_ndfun.thy
@@ -1,639 +1,639 @@
 (*  Title:       Examples of hybrid systems verifications
     Author:      Jonathan Julián Huerta y Munive, 2020
     Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
 *)
 
 subsection \<open> Examples \<close>
 
 text \<open> We prove partial correctness specifications of some hybrid systems with our 
 refinement and verification components.\<close>
 
 theory HS_VC_KAT_Examples_ndfun
   imports 
     HS_VC_KAT_ndfun
     "HOL-Eisbach.Eisbach"
 
 begin
 
 \<comment> \<open>A tactic for verification of hybrid programs \<close>
 
 named_theorems hoare_intros
 
 declare H_assignl [hoare_intros]
     and H_cond [hoare_intros]
     and local_flow.H_g_ode_subset [hoare_intros]
     and H_g_ode_inv [hoare_intros]
 
 method body_hoare 
   = (rule hoare_intros,(simp)?; body_hoare?)
 
 method hyb_hoare for P::"'a pred" 
   = (rule H_loopI, rule H_seq[where R=P]; body_hoare?)
 
 \<comment> \<open>A tactic for refinement of hybrid programs \<close>
 
 named_theorems refine_intros "selected refinement lemmas"
 
 declare R_loopI [refine_intros]
     and R_loop_mono [refine_intros]
     and R_cond_law [refine_intros]
     and R_cond_mono [refine_intros]
     and R_while_law [refine_intros]
     and R_assignl [refine_intros]
     and R_seq_law [refine_intros]
     and R_seq_mono [refine_intros]
     and R_g_evol_law [refine_intros]
     and R_skip [refine_intros]
     and R_g_ode_inv [refine_intros]
 
 method refinement
   = (rule refine_intros; (refinement)?)
 
 subsubsection \<open>Pendulum\<close>
 
 text \<open> The ODEs @{text "x' t = y t"} and {text "y' t = - x t"} describe the circular motion of 
 a mass attached to a string looked from above. We use @{text "s$1"} to represent the x-coordinate
 and @{text "s$2"} for the y-coordinate. We prove that this motion remains circular. \<close>
 
 abbreviation fpend :: "real^2 \<Rightarrow> real^2" ("f")
   where "f s \<equiv> (\<chi> i. if i=1 then s$2 else -s$1)"
 
 abbreviation pend_flow :: "real \<Rightarrow> real^2 \<Rightarrow> real^2" ("\<phi>")
   where "\<phi> \<tau> s \<equiv> (\<chi> i. if i = 1 then s$1 \<cdot> cos \<tau> + s$2 \<cdot> sin \<tau> 
   else - s$1 \<cdot> sin \<tau> + s$2 \<cdot> cos \<tau>)"
 
 \<comment> \<open>Verified with annotated dynamics \<close>
 
 lemma pendulum_dyn: "\<^bold>{\<lambda>s. r\<^sup>2 = (s $ 1)\<^sup>2 + (s $ 2)\<^sup>2\<^bold>} EVOL \<phi> G T \<^bold>{\<lambda>s. r\<^sup>2 = (s $ 1)\<^sup>2 + (s $ 2)\<^sup>2\<^bold>}"
   by simp
 
 \<comment> \<open>Verified with differential invariants \<close>
 
 lemma pendulum_inv: "\<^bold>{\<lambda>s. r\<^sup>2 = (s $ 1)\<^sup>2 + (s $ 2)\<^sup>2\<^bold>} (x\<acute>=f & G) \<^bold>{\<lambda>s. r\<^sup>2 = (s $ 1)\<^sup>2 + (s $ 2)\<^sup>2\<^bold>}"
   by (auto intro!: diff_invariant_rules poly_derivatives)
 
 \<comment> \<open>Verified with the flow \<close>
 
 lemma local_flow_pend: "local_flow f UNIV UNIV \<phi>"
   apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def vec_eq_iff, clarsimp)
   apply(rule_tac x="1" in exI, clarsimp, rule_tac x=1 in exI)
     apply(simp add: dist_norm norm_vec_def L2_set_def power2_commute UNIV_2)
   by (auto simp: forall_2 intro!: poly_derivatives)
 
 lemma pendulum_flow: "\<^bold>{\<lambda>s. r\<^sup>2 = (s $ 1)\<^sup>2 + (s $ 2)\<^sup>2\<^bold>} (x\<acute>=f & G) \<^bold>{\<lambda>s. r\<^sup>2 = (s $ 1)\<^sup>2 + (s $ 2)\<^sup>2\<^bold>}"
   by (subst local_flow.sH_g_ode_subset[OF local_flow_pend], simp_all)
 
 no_notation fpend ("f")
         and pend_flow ("\<phi>")
 
 
 subsubsection \<open> Bouncing Ball \<close>
 
 text \<open> A ball is dropped from rest at an initial height @{text "h"}. The motion is described with
 the free-fall equations @{text "x' t = v t"} and @{text "v' t = g"} where @{text "g"} is the
 constant acceleration due to gravity. The bounce is modelled with a variable assignment that
 flips the velocity. That is, we model it as a completely elastic collision with the ground. We use 
 @{text "s$1"} to represent the ball's height and @{text "s$2"} for its velocity. We prove that the 
 ball remains above ground and below its initial resting position. \<close>
 
 abbreviation fball :: "real \<Rightarrow> real^2 \<Rightarrow> real^2" ("f") 
   where "f g s \<equiv> (\<chi> i. if i=1 then s$2 else g)"
 
 abbreviation ball_flow :: "real \<Rightarrow> real \<Rightarrow> real^2 \<Rightarrow> real^2" ("\<phi>") 
   where "\<phi> g \<tau> s \<equiv> (\<chi> i. if i=1 then g \<cdot> \<tau> ^ 2/2 + s$2 \<cdot> \<tau> + s$1 else g \<cdot> \<tau> + s$2)"
 
 \<comment> \<open>Verified with differential invariants \<close>
 
 named_theorems bb_real_arith "real arithmetic properties for the bouncing ball."
 
 lemma [bb_real_arith]: 
   assumes "0 > g" and inv: "2 \<cdot> g \<cdot> x - 2 \<cdot> g \<cdot> h = v \<cdot> v"
   shows "(x::real) \<le> h"
 proof-
   have "v \<cdot> v = 2 \<cdot> g \<cdot> x - 2 \<cdot> g \<cdot> h \<and> 0 > g" 
     using inv and \<open>0 > g\<close> by auto
   hence obs:"v \<cdot> v = 2 \<cdot> g \<cdot> (x - h) \<and> 0 > g \<and> v \<cdot> v \<ge> 0" 
     using left_diff_distrib mult.commute by (metis zero_le_square) 
   hence "(v \<cdot> v)/(2 \<cdot> g) = (x - h)" 
     by auto 
   also from obs have "(v \<cdot> v)/(2 \<cdot> g) \<le> 0"
     using divide_nonneg_neg by fastforce 
   ultimately have "h - x \<ge> 0" 
     by linarith
   thus ?thesis by auto
 qed
 
 lemma fball_invariant: 
   fixes g h :: real
   defines dinv: "I \<equiv> (\<lambda>s. 2 \<cdot> g \<cdot> s$1 - 2 \<cdot> g \<cdot> h - (s$2 \<cdot> s$2) = 0)"
   shows "diff_invariant I (\<lambda>t. f g) (\<lambda>s. UNIV) UNIV 0 G"
   unfolding dinv apply(rule diff_invariant_rules, simp)
   by(auto intro!: poly_derivatives)
 
 lemma bouncing_ball_inv: "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow> 
   \<^bold>{\<lambda>s. s$1 = h \<and> s$2 = 0\<^bold>}
   (LOOP 
       ((x\<acute>= f g & (\<lambda> s. s$1 \<ge> 0) DINV (\<lambda>s. 2 \<cdot> g \<cdot> s$1 - 2 \<cdot> g \<cdot> h - s$2 \<cdot> s$2 = 0));
        (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip)) 
     INV (\<lambda>s. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2)
   ) \<^bold>{\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h\<^bold>}"
   apply(hyb_hoare "\<lambda>s::real^2. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2")
   using fball_invariant by (auto simp: bb_real_arith intro!: poly_derivatives diff_invariant_rules)
 
 \<comment> \<open>Verified with annotated dynamics \<close>
 
 lemma [bb_real_arith]:
   assumes invar: "2 \<cdot> g \<cdot> x = 2 \<cdot> g \<cdot> h + v \<cdot> v"
     and pos: "g \<cdot> \<tau>\<^sup>2 / 2 + v \<cdot> \<tau> + (x::real) = 0"
   shows "2 \<cdot> g \<cdot> h + (- (g \<cdot> \<tau>) - v) \<cdot> (- (g \<cdot> \<tau>) - v) = 0"
     and "2 \<cdot> g \<cdot> h + (g \<cdot> \<tau> \<cdot> (g \<cdot> \<tau> + v) + v \<cdot> (g \<cdot> \<tau> + v)) = 0"
 proof-
   from pos have "g \<cdot> \<tau>\<^sup>2  + 2 \<cdot> v \<cdot> \<tau> + 2 \<cdot> x = 0" by auto
   then have "g\<^sup>2  \<cdot> \<tau>\<^sup>2  + 2 \<cdot> g \<cdot> v \<cdot> \<tau> + 2 \<cdot> g \<cdot> x = 0"
-    by (metis (mono_tags, opaque_lifting) Groups.mult_ac(1,3) mult_zero_right
+    by (metis (mono_tags) Groups.mult_ac(1,3) mult_zero_right
         monoid_mult_class.power2_eq_square semiring_class.distrib_left)
   hence "g\<^sup>2 \<cdot> \<tau>\<^sup>2 + 2 \<cdot> g \<cdot> v \<cdot> \<tau> + v\<^sup>2 + 2 \<cdot> g \<cdot> h = 0"
     using invar by (simp add: monoid_mult_class.power2_eq_square) 
   hence obs: "(g \<cdot> \<tau> + v)\<^sup>2 + 2 \<cdot> g \<cdot> h = 0"
-    apply(subst power2_sum) by (metis (no_types, opaque_lifting) Groups.add_ac(2, 3) 
+    apply(subst power2_sum) by (metis (no_types) Groups.add_ac(2, 3) 
         Groups.mult_ac(2, 3) monoid_mult_class.power2_eq_square nat_distrib(2))
   thus "2 \<cdot> g \<cdot> h + (g \<cdot> \<tau> \<cdot> (g \<cdot> \<tau> + v) + v \<cdot> (g \<cdot> \<tau> + v)) = 0"
     by (simp add: monoid_mult_class.power2_eq_square)
   have  "2 \<cdot> g \<cdot> h + (- ((g \<cdot> \<tau>) + v))\<^sup>2 = 0"
     using obs by (metis Groups.add_ac(2) power2_minus)
   thus "2 \<cdot> g \<cdot> h + (- (g \<cdot> \<tau>) - v) \<cdot> (- (g \<cdot> \<tau>) - v) = 0"
     by (simp add: monoid_mult_class.power2_eq_square)
 qed
 
 lemma [bb_real_arith]:
   assumes invar: "2 \<cdot> g \<cdot> x = 2 \<cdot> g \<cdot> h + v \<cdot> v"
   shows "2 \<cdot> g \<cdot> (g \<cdot> \<tau>\<^sup>2 / 2 + v \<cdot> \<tau> + (x::real)) = 
   2 \<cdot> g \<cdot> h + (g \<cdot> \<tau> \<cdot> (g \<cdot> \<tau> + v) + v \<cdot> (g \<cdot> \<tau> + v))" (is "?lhs = ?rhs")
 proof-
   have "?lhs = g\<^sup>2 \<cdot> \<tau>\<^sup>2 + 2 \<cdot> g \<cdot> v \<cdot> \<tau> + 2 \<cdot> g \<cdot> x" 
     by(auto simp: algebra_simps semiring_normalization_rules(29))
   also have "... = g\<^sup>2 \<cdot> \<tau>\<^sup>2 + 2 \<cdot> g \<cdot> v \<cdot> \<tau> + 2 \<cdot> g \<cdot> h + v \<cdot> v" (is "... = ?middle")
       by(subst invar, simp)
     finally have "?lhs = ?middle".
   moreover 
   {have "?rhs = g \<cdot> g \<cdot> (\<tau> \<cdot> \<tau>) + 2 \<cdot> g \<cdot> v \<cdot> \<tau> + 2 \<cdot> g \<cdot> h + v \<cdot> v"
     by (simp add: Groups.mult_ac(2,3) semiring_class.distrib_left)
   also have "... = ?middle"
     by (simp add: semiring_normalization_rules(29))
   finally have "?rhs = ?middle".}
   ultimately show ?thesis by auto
 qed
 
 lemma bouncing_ball_dyn: "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow>
   \<^bold>{\<lambda>s. s$1 = h \<and> s$2 = 0\<^bold>}
   (LOOP 
       ((EVOL (\<phi> g) (\<lambda> s. s$1 \<ge> 0) T);
        (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip)) 
     INV (\<lambda>s. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2)
   ) \<^bold>{\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h\<^bold>}"
   apply(hyb_hoare "\<lambda>s::real^2. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2")
   by (auto simp: bb_real_arith)
 
 \<comment> \<open>Verified with the flow \<close>
 
 lemma local_flow_ball: "local_flow (f g) UNIV UNIV (\<phi> g)"
   apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def vec_eq_iff, clarsimp)
   apply(rule_tac x="1/2" in exI, clarsimp, rule_tac x=1 in exI)
     apply(simp add: dist_norm norm_vec_def L2_set_def UNIV_2)
   by (auto simp: forall_2 intro!: poly_derivatives)
 
 lemma bouncing_ball_flow: "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow>
   \<^bold>{\<lambda>s. s$1 = h \<and> s$2 = 0\<^bold>}
   (LOOP 
       ((x\<acute>= f g & (\<lambda> s. s$1 \<ge> 0));
        (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip)) 
     INV (\<lambda>s. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2)
   ) \<^bold>{\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h\<^bold>}"
   apply(rule H_loopI; (rule H_seq[where R="\<lambda>s. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2"])?)
      apply(subst local_flow.sH_g_ode_subset[OF local_flow_ball])
   by (auto simp: bb_real_arith)
 
 \<comment> \<open>Refined with annotated dynamics \<close>
 
 lemma R_bb_assign: "g < (0::real) \<Longrightarrow> 0 \<le> h \<Longrightarrow> 
   2 ::= (\<lambda>s. - s$2) \<le> Ref 
     \<lceil>\<lambda>s. s$1 = 0 \<and> 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2\<rceil> 
     \<lceil>\<lambda>s. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2\<rceil>"
   by (rule R_assign_law, auto)
 
 lemma R_bouncing_ball_dyn:
   assumes "g < 0" and "h \<ge> 0"
   shows "Ref \<lceil>\<lambda>s. s$1 = h \<and> s$2 = 0\<rceil> \<lceil>\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h\<rceil> \<ge> 
   (LOOP 
       ((EVOL (\<phi> g) (\<lambda> s. s$1 \<ge> 0) T);
        (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip)) 
     INV (\<lambda>s. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2))"
   apply(refinement; (rule R_bb_assign[OF assms])?)
   using assms by (auto simp: bb_real_arith)
 
 no_notation fball ("f")
         and ball_flow ("\<phi>")
 
 
 subsubsection \<open> Thermostat \<close>
 
 text \<open> A thermostat has a chronometer, a thermometer and a switch to turn on and off a heater.
 At most every @{text "t"} minutes, it sets its chronometer to @{term "0::real"}, it registers
 the room temperature, and it turns the heater on (or off) based on this reading. The temperature
 follows the ODE @{text "T' = - a * (T - U)"} where @{text "U"} is @{text "L \<ge> 0"} when the heater
 is on, and @{text "0"} when it is off. We use @{term "1::4"} to denote the room's temperature,
 @{term "2::4"} is time as measured by the thermostat's chronometer, @{term "3::4"} is the
 temperature detected by the thermometer, and @{term "4::4"} states whether the heater is on
 (@{text "s$4 = 1"}) or off (@{text "s$4 = 0"}). We prove that the thermostat keeps the room's
 temperature between @{text "Tmin"} and @{text "Tmax"}. \<close>
 
 abbreviation therm_vec_field :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> real^4" ("f")
   where "f a L s \<equiv> (\<chi> i. if i = 2 then 1 else (if i = 1 then - a * (s$1 - L) else 0))"
 
 abbreviation therm_guard :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("G")
   where "G Tmin Tmax a L s \<equiv> (s$2 \<le> - (ln ((L-(if L=0 then Tmin else Tmax))/(L-s$3)))/a)"
 
 abbreviation therm_loop_inv :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("I")
   where "I Tmin Tmax s \<equiv> Tmin \<le> s$1 \<and> s$1 \<le> Tmax \<and> (s$4 = 0 \<or> s$4 = 1)"
 
 abbreviation therm_flow :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> real^4" ("\<phi>")
   where "\<phi> a L \<tau> s \<equiv> (\<chi> i. if i = 1 then - exp(-a * \<tau>) * (L - s$1) + L else 
   (if i = 2 then \<tau> + s$2 else s$i))"
 
 \<comment> \<open>Verified with the flow \<close>
 
 lemma norm_diff_therm_dyn: "0 < a \<Longrightarrow> \<parallel>f a L s\<^sub>1 - f a L s\<^sub>2\<parallel> = \<bar>a\<bar> * \<bar>s\<^sub>1$1 - s\<^sub>2$1\<bar>"
 proof(simp add: norm_vec_def L2_set_def, unfold UNIV_4, simp)
   assume a1: "0 < a"
   have f2: "\<And>r ra. \<bar>(r::real) + - ra\<bar> = \<bar>ra + - r\<bar>"
     by (metis abs_minus_commute minus_real_def)
   have "\<And>r ra rb. (r::real) * ra + - (r * rb) = r * (ra + - rb)"
     by (metis minus_real_def right_diff_distrib)
   hence "\<bar>a * (s\<^sub>1$1 + - L) + - (a * (s\<^sub>2$1 + - L))\<bar> = a * \<bar>s\<^sub>1$1 + - s\<^sub>2$1\<bar>"
     using a1 by (simp add: abs_mult)
   thus "\<bar>a * (s\<^sub>2$1 - L) - a * (s\<^sub>1$1 - L)\<bar> = a * \<bar>s\<^sub>1$1 - s\<^sub>2$1\<bar>"
     using f2 minus_real_def by presburger
 qed
 
 lemma local_lipschitz_therm_dyn:
   assumes "0 < (a::real)"
   shows "local_lipschitz UNIV UNIV (\<lambda>t::real. f a L)"
   apply(unfold local_lipschitz_def lipschitz_on_def dist_norm)
   apply(clarsimp, rule_tac x=1 in exI, clarsimp, rule_tac x=a in exI)
   using assms apply(simp_all add: norm_diff_therm_dyn)
   apply(simp add: norm_vec_def L2_set_def, unfold UNIV_4, clarsimp)
   unfolding real_sqrt_abs[symmetric] by (rule real_le_lsqrt) auto
 
 lemma local_flow_therm: "a > 0 \<Longrightarrow> local_flow (f a L) UNIV UNIV (\<phi> a L)"
   by (unfold_locales, auto intro!: poly_derivatives local_lipschitz_therm_dyn 
       simp: forall_4 vec_eq_iff)
 
 lemma therm_dyn_down_real_arith:
   assumes "a > 0" and Thyps: "0 < Tmin" "Tmin \<le> T" "T \<le> Tmax"
     and thyps: "0 \<le> (\<tau>::real)" "\<forall>\<tau>\<in>{0..\<tau>}. \<tau> \<le> - (ln (Tmin / T) / a) "
   shows "Tmin \<le> exp (-a * \<tau>) * T" and "exp (-a * \<tau>) * T \<le> Tmax"
 proof-
   have "0 \<le> \<tau> \<and> \<tau> \<le> - (ln (Tmin / T) / a)"
     using thyps by auto
   hence "ln (Tmin / T) \<le> - a * \<tau> \<and> - a * \<tau> \<le> 0"
     using assms(1) divide_le_cancel by fastforce
   also have "Tmin / T > 0"
     using Thyps by auto
   ultimately have obs: "Tmin / T \<le> exp (-a * \<tau>)" "exp (-a * \<tau>) \<le> 1"
     using exp_ln exp_le_one_iff by (metis exp_less_cancel_iff not_less, simp)
   thus "Tmin \<le> exp (-a * \<tau>) * T"
     using Thyps by (simp add: pos_divide_le_eq)
   show "exp (-a * \<tau>) * T \<le> Tmax"
     using Thyps mult_left_le_one_le[OF _ exp_ge_zero obs(2), of T] 
       less_eq_real_def order_trans_rules(23) by blast
 qed
 
 lemma therm_dyn_up_real_arith:
   assumes "a > 0" and Thyps: "Tmin \<le> T" "T \<le> Tmax" "Tmax < (L::real)"
     and thyps: "0 \<le> \<tau>" "\<forall>\<tau>\<in>{0..\<tau>}. \<tau> \<le> - (ln ((L - Tmax) / (L - T)) / a) "
   shows "L - Tmax \<le> exp (-(a * \<tau>)) * (L - T)" 
     and "L - exp (-(a * \<tau>)) * (L - T) \<le> Tmax" 
     and "Tmin \<le> L - exp (-(a * \<tau>)) * (L - T)"
 proof-
   have "0 \<le> \<tau> \<and> \<tau> \<le> - (ln ((L - Tmax) / (L - T)) / a)"
     using thyps by auto
   hence "ln ((L - Tmax) / (L - T)) \<le> - a * \<tau> \<and> - a * \<tau> \<le> 0"
     using assms(1) divide_le_cancel by fastforce
   also have "(L - Tmax) / (L - T) > 0"
     using Thyps by auto
   ultimately have "(L - Tmax) / (L - T) \<le> exp (-a * \<tau>) \<and> exp (-a * \<tau>) \<le> 1"
     using exp_ln exp_le_one_iff by (metis exp_less_cancel_iff not_less)
   moreover have "L - T > 0"
     using Thyps by auto
   ultimately have obs: "(L - Tmax) \<le> exp (-a * \<tau>) * (L - T) \<and> exp (-a * \<tau>) * (L - T) \<le> (L - T)"
     by (simp add: pos_divide_le_eq)
   thus "(L - Tmax) \<le> exp (-(a * \<tau>)) * (L - T)"
     by auto
   thus "L - exp (-(a * \<tau>)) * (L - T) \<le> Tmax"
     by auto
   show "Tmin \<le> L - exp (-(a * \<tau>)) * (L - T)"
     using Thyps and obs by auto
 qed
 
 lemmas H_g_ode_therm = local_flow.sH_g_ode_ivl[OF local_flow_therm _ UNIV_I]
 
 lemma thermostat_flow: 
   assumes "0 < a" and "0 \<le> \<tau>" and "0 < Tmin" and "Tmax < L"
   shows "\<^bold>{I Tmin Tmax\<^bold>}
   (LOOP (
     \<comment> \<open>control\<close>
     (2 ::= (\<lambda>s. 0));
     (3 ::= (\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> Tmin + 1) THEN 
       (4 ::= (\<lambda>s.1)) 
      ELSE IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> Tmax - 1) THEN 
       (4 ::= (\<lambda>s.0)) 
      ELSE skip);
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN 
       (x\<acute>= (\<lambda>t. f a 0) & G Tmin Tmax a 0 on (\<lambda>s. {0..\<tau>}) UNIV @ 0) 
     ELSE 
       (x\<acute>= (\<lambda>t. f a L) & G Tmin Tmax a L on (\<lambda>s. {0..\<tau>}) UNIV @ 0))
   ) INV I Tmin Tmax)
    \<^bold>{I Tmin Tmax\<^bold>}"
   apply(rule H_loopI)
     apply(rule_tac R="\<lambda>s. I Tmin Tmax s \<and> s$2=0 \<and> s$3 = s$1" in H_seq)
      apply(rule_tac R="\<lambda>s. I Tmin Tmax s\<and> s$2=0 \<and> s$3 = s$1" in H_seq)
       apply(rule_tac R="\<lambda>s. I Tmin Tmax s \<and> s$2 = 0" in H_seq, simp, simp)
       apply(rule H_cond, simp_all add: H_g_ode_therm[OF assms(1,2)])+
   using therm_dyn_up_real_arith[OF assms(1) _ _ assms(4), of Tmin]
     and therm_dyn_down_real_arith[OF assms(1,3), of _ Tmax] by auto
 
 \<comment> \<open>Refined with the flow \<close>
 
 lemma R_therm_dyn_down: 
   assumes "a > 0" and "0 \<le> \<tau>" and "0 < Tmin" and "Tmax < L"
   shows "Ref \<lceil>\<lambda>s. s$4 = 0 \<and> I Tmin Tmax s \<and> s$2 = 0 \<and> s$3 = s$1\<rceil> \<lceil>I Tmin Tmax\<rceil> \<ge> 
     (x\<acute>= (\<lambda>t. f a 0) & G Tmin Tmax a 0 on (\<lambda>s. {0..\<tau>}) UNIV @ 0)"
   apply(rule local_flow.R_g_ode_ivl[OF local_flow_therm])
   using assms therm_dyn_down_real_arith[OF assms(1,3), of _ Tmax] by auto
 
 lemma R_therm_dyn_up: 
   assumes "a > 0" and "0 \<le> \<tau>" and "0 < Tmin" and "Tmax < L"
   shows "Ref \<lceil>\<lambda>s. s$4 \<noteq> 0 \<and> I Tmin Tmax s \<and> s$2 = 0 \<and> s$3 = s$1\<rceil> \<lceil>I Tmin Tmax\<rceil> \<ge> 
     (x\<acute>= (\<lambda>t. f a L) & G Tmin Tmax a L on (\<lambda>s. {0..\<tau>}) UNIV @ 0)"
   apply(rule local_flow.R_g_ode_ivl[OF local_flow_therm])
   using assms therm_dyn_up_real_arith[OF assms(1) _ _ assms(4), of Tmin] by auto
 
 lemma R_therm_dyn:
   assumes "a > 0" and "0 \<le> \<tau>" and "0 < Tmin" and "Tmax < L"
   shows "Ref \<lceil>\<lambda>s. I Tmin Tmax s \<and> s$2 = 0 \<and> s$3 = s$1\<rceil> \<lceil>I Tmin Tmax\<rceil> \<ge> 
   (IF (\<lambda>s. s$4 = 0) THEN 
     (x\<acute>= (\<lambda>t. f a 0) & G Tmin Tmax a 0 on (\<lambda>s. {0..\<tau>}) UNIV @ 0) 
   ELSE 
     (x\<acute>= (\<lambda>t. f a L) & G Tmin Tmax a L on (\<lambda>s. {0..\<tau>}) UNIV @ 0))"
   apply(rule order_trans, rule R_cond_mono)
   using R_therm_dyn_down[OF assms] R_therm_dyn_up[OF assms] by (auto intro!: R_cond)
 
 lemma R_therm_assign1: "Ref \<lceil>I Tmin Tmax\<rceil> \<lceil>\<lambda>s. I Tmin Tmax s \<and> s$2 = 0\<rceil> \<ge> (2 ::= (\<lambda>s. 0))"
   by (auto simp: R_assign_law)
 
 lemma R_therm_assign2: 
   "Ref \<lceil>\<lambda>s. I Tmin Tmax s \<and> s$2 = 0\<rceil> \<lceil>\<lambda>s. I Tmin Tmax s \<and> s$2 = 0 \<and> s$3 = s$1\<rceil> \<ge> (3 ::= (\<lambda>s. s$1))"
   by (auto simp: R_assign_law)
 
 lemma R_therm_ctrl:
   "Ref \<lceil>I Tmin Tmax\<rceil> \<lceil>\<lambda>s. I Tmin Tmax s \<and> s$2 = 0 \<and> s$3 = s$1\<rceil> \<ge>
   (2 ::= (\<lambda>s. 0));
   (3 ::= (\<lambda>s. s$1));
   (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> Tmin + 1) THEN 
     (4 ::= (\<lambda>s.1)) 
    ELSE IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> Tmax - 1) THEN 
     (4 ::= (\<lambda>s.0)) 
    ELSE skip)"
   apply(refinement, rule R_therm_assign1, rule R_therm_assign2)
   by (rule R_assign_law, simp)+ auto
 
 lemma R_therm_loop: "Ref \<lceil>I Tmin Tmax\<rceil> \<lceil>I Tmin Tmax\<rceil> \<ge> 
   (LOOP 
     Ref \<lceil>I Tmin Tmax\<rceil> \<lceil>\<lambda>s. I Tmin Tmax s \<and> s$2 = 0 \<and> s$3 = s$1\<rceil>;
     Ref \<lceil>\<lambda>s. I Tmin Tmax s \<and> s$2 = 0 \<and> s$3 = s$1\<rceil> \<lceil>I Tmin Tmax\<rceil>
   INV I Tmin Tmax)"
   by (intro R_loop R_seq, simp_all)
 
 lemma R_thermostat_flow: 
   assumes "a > 0" and "0 \<le> \<tau>" and "0 < Tmin" and "Tmax < L"
   shows "Ref \<lceil>I Tmin Tmax\<rceil> \<lceil>I Tmin Tmax\<rceil> \<ge> 
   (LOOP (
     \<comment> \<open>control\<close>
     (2 ::= (\<lambda>s. 0));(3 ::= (\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> Tmin + 1) THEN 
       (4 ::= (\<lambda>s.1)) 
      ELSE IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> Tmax - 1) THEN 
       (4 ::= (\<lambda>s.0)) 
      ELSE skip);
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN 
       (x\<acute>= (\<lambda>t. f a 0) & G Tmin Tmax a 0 on (\<lambda>s. {0..\<tau>}) UNIV @ 0) 
     ELSE 
       (x\<acute>= (\<lambda>t. f a L) & G Tmin Tmax a L on (\<lambda>s. {0..\<tau>}) UNIV @ 0))
   ) INV I Tmin Tmax)"
   by (intro order_trans[OF _ R_therm_loop] R_loop_mono 
       R_seq_mono R_therm_ctrl R_therm_dyn[OF assms])
 
 no_notation therm_vec_field ("f")
         and therm_flow ("\<phi>")
         and therm_guard ("G")
         and therm_loop_inv ("I")
 
 
 subsubsection \<open> Water tank \<close> \<comment> \<open> Variation of Hespanha and Alur's tank \<close>
 
 subsubsection \<open> Tank \<close>
 
 text \<open> A controller turns a water pump on and off to keep the level of water @{text "h"} in a tank
 within an acceptable range @{text "hmin \<le> h \<le> hmax"}. Just like in the previous example, after 
 each intervention, the controller registers the current level of water and resets its chronometer,
 then it changes the status of the water pump accordingly. The level of water grows linearly 
 @{text "h' = k"} at a rate of @{text "k = c\<^sub>i-c\<^sub>o"} if the pump is on, and at a rate of 
 @{text "k = -c\<^sub>o"} if the pump is off. We use @{term "1::4"} to denote the tank's level of water,
 @{term "2::4"} is time as measured by the controller's chronometer, @{term "3::4"} is the
 level of water measured by the chronometer, and @{term "4::4"} states whether the pump is on
 (@{text "s$4 = 1"}) or off (@{text "s$4 = 0"}). We prove that the controller keeps the level of
 water between @{text "hmin"} and @{text "hmax"}. \<close>
 
 abbreviation tank_vec_field :: "real \<Rightarrow> real^4 \<Rightarrow> real^4" ("f")
   where "f k s \<equiv> (\<chi> i. if i = 2 then 1 else (if i = 1 then k else 0))"
 
 abbreviation tank_flow :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> real^4" ("\<phi>")
   where "\<phi> k \<tau> s \<equiv> (\<chi> i. if i = 1 then k * \<tau> + s$1 else 
   (if i = 2 then \<tau> + s$2 else s$i))"
 
 abbreviation tank_guard :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("G")
   where "G Hm k s \<equiv> s$2 \<le> (Hm - s$3)/k"
 
 abbreviation tank_loop_inv :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("I")
   where "I hmin hmax s \<equiv> hmin \<le> s$1 \<and> s$1 \<le> hmax \<and> (s$4 = 0 \<or> s$4 = 1)"
 
 abbreviation tank_diff_inv :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("dI")
   where "dI hmin hmax k s \<equiv> s$1 = k \<cdot> s$2 + s$3 \<and> 0 \<le> s$2 \<and> 
     hmin \<le> s$3 \<and> s$3 \<le> hmax \<and> (s$4 = 0 \<or> s$4 = 1)"
 
 \<comment> \<open>Verified with the flow \<close>
 
 lemma local_flow_tank: "local_flow (f k) UNIV UNIV (\<phi> k)"
   apply (unfold_locales, unfold local_lipschitz_def lipschitz_on_def, simp_all, clarsimp)
   apply(rule_tac x="1/2" in exI, clarsimp, rule_tac x=1 in exI)
   apply(simp add: dist_norm norm_vec_def L2_set_def, unfold UNIV_4)
   by (auto intro!: poly_derivatives simp: vec_eq_iff)
 
 lemma tank_arith:
   assumes "0 \<le> (\<tau>::real)" and "0 < c\<^sub>o" and "c\<^sub>o < c\<^sub>i"
   shows "\<forall>\<tau>\<in>{0..\<tau>}. \<tau> \<le> - ((hmin - y) / c\<^sub>o) \<Longrightarrow>  hmin \<le> y - c\<^sub>o * \<tau>"
     and "\<forall>\<tau>\<in>{0..\<tau>}. \<tau> \<le> (hmax - y) / (c\<^sub>i - c\<^sub>o) \<Longrightarrow>  (c\<^sub>i - c\<^sub>o) * \<tau> + y \<le> hmax"
     and "hmin \<le> y \<Longrightarrow> hmin \<le> (c\<^sub>i - c\<^sub>o) \<cdot> \<tau> + y"
     and "y \<le> hmax \<Longrightarrow> y - c\<^sub>o \<cdot> \<tau> \<le> hmax"
   apply(simp_all add: field_simps le_divide_eq assms)
   using assms apply (meson add_mono less_eq_real_def mult_left_mono)
   using assms by (meson add_increasing2 less_eq_real_def mult_nonneg_nonneg) 
 
 lemmas H_g_ode_tank = local_flow.sH_g_ode_ivl[OF local_flow_tank _ UNIV_I]
 
 lemma tank_flow:
   assumes "0 \<le> \<tau>" and "0 < c\<^sub>o" and "c\<^sub>o < c\<^sub>i"
   shows "\<^bold>{I hmin hmax\<^bold>}
   (LOOP 
     \<comment> \<open>control\<close>
     ((2 ::=(\<lambda>s.0));(3 ::=(\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> hmin + 1) THEN (4 ::= (\<lambda>s.1)) ELSE 
     (IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> hmax - 1) THEN (4 ::= (\<lambda>s.0)) ELSE skip));
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN (x\<acute>= (\<lambda>t. f (c\<^sub>i-c\<^sub>o)) & G hmax (c\<^sub>i-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0) 
      ELSE (x\<acute>= (\<lambda>t. f (-c\<^sub>o)) & G hmin (-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0)) )
   INV I hmin hmax) 
   \<^bold>{I hmin hmax\<^bold>}"
   apply(rule H_loopI)
     apply(rule_tac R="\<lambda>s. I hmin hmax s \<and> s$2=0 \<and> s$3 = s$1" in H_seq)
      apply(rule_tac R="\<lambda>s. I hmin hmax s \<and> s$2=0 \<and> s$3 = s$1" in H_seq)
       apply(rule_tac R="\<lambda>s. I hmin hmax s \<and> s$2=0" in H_seq, simp, simp)
      apply(rule H_cond, simp_all add: H_g_ode_tank[OF assms(1)])
   using assms tank_arith[OF _ assms(2,3)] by auto
 
 \<comment> \<open>Verified with differential invariants \<close>
 
 lemma tank_diff_inv:
   "0 \<le> \<tau> \<Longrightarrow> diff_invariant (dI hmin hmax k) (\<lambda>t. f k) (\<lambda>s. {0..\<tau>}) UNIV 0 Guard"
   apply(intro diff_invariant_conj_rule)
       apply(force intro!: poly_derivatives diff_invariant_rules)
      apply(rule_tac \<nu>'="\<lambda>t. 0" and \<mu>'="\<lambda>t. 1" in diff_invariant_leq_rule, simp_all, presburger)
     apply(rule_tac \<nu>'="\<lambda>t. 0" and \<mu>'="\<lambda>t. 0" in diff_invariant_leq_rule, simp_all)
     apply(force intro!: poly_derivatives)+
   by (auto intro!: poly_derivatives diff_invariant_rules)
 
 lemma tank_inv_arith1:
   assumes "0 \<le> (\<tau>::real)" and "c\<^sub>o < c\<^sub>i" and b: "hmin \<le> y\<^sub>0" and g: "\<tau> \<le> (hmax - y\<^sub>0) / (c\<^sub>i - c\<^sub>o)"
   shows "hmin \<le> (c\<^sub>i - c\<^sub>o) \<cdot> \<tau> + y\<^sub>0" and "(c\<^sub>i - c\<^sub>o) \<cdot> \<tau> + y\<^sub>0 \<le> hmax"
 proof-
   have "(c\<^sub>i - c\<^sub>o) \<cdot> \<tau> \<le> (hmax - y\<^sub>0)"
     using g assms(2,3) by (metis diff_gt_0_iff_gt mult.commute pos_le_divide_eq) 
   thus "(c\<^sub>i - c\<^sub>o) \<cdot> \<tau> + y\<^sub>0 \<le> hmax"
     by auto
   show "hmin \<le> (c\<^sub>i - c\<^sub>o) \<cdot> \<tau> + y\<^sub>0"
     using b assms(1,2) by (metis add.commute add_increasing2 diff_ge_0_iff_ge 
         less_eq_real_def mult_nonneg_nonneg) 
 qed
 
 lemma tank_inv_arith2:
   assumes "0 \<le> (\<tau>::real)" and "0 < c\<^sub>o" and b: "y\<^sub>0 \<le> hmax" and g: "\<tau> \<le> - ((hmin - y\<^sub>0) / c\<^sub>o)"
   shows "hmin \<le> y\<^sub>0 - c\<^sub>o \<cdot> \<tau>" and "y\<^sub>0 - c\<^sub>o \<cdot> \<tau> \<le> hmax"
 proof-
   have "\<tau> \<cdot> c\<^sub>o \<le> y\<^sub>0 - hmin"
     using g \<open>0 < c\<^sub>o\<close> pos_le_minus_divide_eq by fastforce 
   thus "hmin \<le> y\<^sub>0 - c\<^sub>o \<cdot> \<tau>"
     by (auto simp: mult.commute)
   show "y\<^sub>0 - c\<^sub>o \<cdot> \<tau> \<le> hmax" 
     using b assms(1,2) by (smt mult_nonneg_nonneg) 
 qed
 
 lemma tank_inv:
   assumes "0 \<le> \<tau>" and "0 < c\<^sub>o" and "c\<^sub>o < c\<^sub>i"
   shows "\<^bold>{I hmin hmax\<^bold>}
   (LOOP 
     \<comment> \<open>control\<close>
     ((2 ::=(\<lambda>s.0));(3 ::=(\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> hmin + 1) THEN (4 ::= (\<lambda>s.1)) ELSE 
     (IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> hmax - 1) THEN (4 ::= (\<lambda>s.0)) ELSE skip));
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN 
       (x\<acute>= (\<lambda>t. f (c\<^sub>i-c\<^sub>o)) & G hmax (c\<^sub>i-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0 DINV (dI hmin hmax (c\<^sub>i-c\<^sub>o))) 
      ELSE 
       (x\<acute>= (\<lambda>t. f (-c\<^sub>o)) & G hmin (-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0 DINV (dI hmin hmax (-c\<^sub>o)))) )
   INV I hmin hmax)
   \<^bold>{I hmin hmax\<^bold>}"
   apply(rule H_loopI)
     apply(rule_tac R="\<lambda>s. I hmin hmax s \<and> s$2=0 \<and> s$3 = s$1" in H_seq)
      apply(rule_tac R="\<lambda>s. I hmin hmax s \<and> s$2=0 \<and> s$3 = s$1" in H_seq)
       apply(rule_tac R="\<lambda>s. I hmin hmax s \<and> s$2=0" in H_seq, simp, simp)
      apply(rule H_cond, simp, simp)+
     apply(rule H_cond, rule H_g_ode_inv)
   using assms tank_inv_arith1 apply(force simp: tank_diff_inv, simp, clarsimp)
     apply(rule H_g_ode_inv)
   using assms tank_diff_inv[of _ "-c\<^sub>o" hmin hmax] tank_inv_arith2 by auto
 
 \<comment> \<open>Refined with differential invariants \<close>
 
 abbreviation tank_ctrl :: "real \<Rightarrow> real \<Rightarrow> (real^4) nd_fun" ("ctrl")
   where "ctrl hmin hmax \<equiv> ((2 ::=(\<lambda>s.0));(3 ::=(\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> hmin + 1) THEN (4 ::= (\<lambda>s.1)) ELSE 
     (IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> hmax - 1) THEN (4 ::= (\<lambda>s.0)) ELSE skip)))"
 
 abbreviation tank_dyn_dinv :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real^4) nd_fun" ("dyn")
   where "dyn c\<^sub>i c\<^sub>o hmin hmax \<tau> \<equiv> (IF (\<lambda>s. s$4 = 0) THEN 
       (x\<acute>= (\<lambda>t. f (c\<^sub>i-c\<^sub>o)) & G hmax (c\<^sub>i-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0 DINV (dI hmin hmax (c\<^sub>i-c\<^sub>o))) 
      ELSE 
       (x\<acute>= (\<lambda>t. f (-c\<^sub>o)) & G hmin (-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0 DINV (dI hmin hmax (-c\<^sub>o))))"
 
 abbreviation "tank_dinv c\<^sub>i c\<^sub>o hmin hmax \<tau> \<equiv> LOOP (ctrl hmin hmax ; dyn c\<^sub>i c\<^sub>o hmin hmax \<tau>) INV (I hmin hmax)"
 
 lemma R_tank_inv:
   assumes "0 \<le> \<tau>" and "0 < c\<^sub>o" and "c\<^sub>o < c\<^sub>i"
   shows "Ref \<lceil>I hmin hmax\<rceil> \<lceil>I hmin hmax\<rceil> \<ge> 
   (LOOP 
     \<comment> \<open>control\<close>
     ((2 ::=(\<lambda>s.0));(3 ::=(\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> hmin + 1) THEN (4 ::= (\<lambda>s.1)) ELSE 
     (IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> hmax - 1) THEN (4 ::= (\<lambda>s.0)) ELSE skip));
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN 
       (x\<acute>= (\<lambda>t. f (c\<^sub>i-c\<^sub>o)) & G hmax (c\<^sub>i-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0 DINV (dI hmin hmax (c\<^sub>i-c\<^sub>o))) 
      ELSE 
       (x\<acute>= (\<lambda>t. f (-c\<^sub>o)) & G hmin (-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0 DINV (dI hmin hmax (-c\<^sub>o)))) )
   INV I hmin hmax)"
 proof-
   have "Ref \<lceil>I hmin hmax\<rceil> \<lceil>I hmin hmax\<rceil> \<ge> 
     LOOP (
       (2 ::= (\<lambda>s. 0)); (Ref \<lceil>\<lambda>s. I hmin hmax s \<and> s$2 = 0\<rceil> \<lceil>I hmin hmax\<rceil>)
     ) INV I hmin hmax" (is "_ \<ge> ?R")
     by (refinement, auto)
   moreover have 
     "?R \<ge> LOOP (
       (2 ::= (\<lambda>s. 0));(3 ::=(\<lambda>s. s$1));
       (Ref \<lceil>\<lambda>s. I hmin hmax s \<and> s$2 = 0 \<and> s$3=s$1\<rceil> \<lceil>I hmin hmax\<rceil>)
     ) INV I hmin hmax" (is "_ \<ge> ?R")
     by (simp only: mult.assoc, refinement, auto)
   moreover have 
     "?R \<ge> LOOP (
       ctrl hmin hmax;
       (Ref \<lceil>\<lambda>s. I hmin hmax s \<and> s$2 = 0 \<and> s$3=s$1\<rceil> \<lceil>I hmin hmax\<rceil>)
     ) INV I hmin hmax" (is "_ \<ge> ?R")
     by (simp only: mult.assoc, refinement; (force)?, (rule R_assign_law)?) auto
   moreover have 
     "?R \<ge> LOOP (ctrl hmin hmax; dyn c\<^sub>i c\<^sub>o hmin hmax \<tau>) INV I hmin hmax"
     apply(simp only: mult.assoc, refinement; ((rule tank_diff_inv[OF assms(1)])? | (simp)?))
     using tank_inv_arith1 tank_inv_arith2 assms by auto
   ultimately show ?thesis
     by auto
 qed
 
 no_notation tank_vec_field ("f")
         and tank_flow ("\<phi>")
         and tank_guard ("G")
         and tank_loop_inv ("I")
         and tank_diff_inv ("dI")
 
 end
\ No newline at end of file
diff --git a/thys/Hybrid_Systems_VCs/KleeneAlgebraTests/HS_VC_KAT_Examples_rel.thy b/thys/Hybrid_Systems_VCs/KleeneAlgebraTests/HS_VC_KAT_Examples_rel.thy
--- a/thys/Hybrid_Systems_VCs/KleeneAlgebraTests/HS_VC_KAT_Examples_rel.thy
+++ b/thys/Hybrid_Systems_VCs/KleeneAlgebraTests/HS_VC_KAT_Examples_rel.thy
@@ -1,643 +1,643 @@
 (*  Title:       Examples of hybrid systems verifications
     Author:      Jonathan Julián Huerta y Munive, 2020
     Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
 *)
 
 subsection \<open> Examples \<close>
 
 text \<open> We prove partial correctness specifications of some hybrid systems with our 
 refinement and verification components.\<close>
 
 theory HS_VC_KAT_Examples_rel
   imports 
     HS_VC_KAT_rel
     "HOL-Eisbach.Eisbach"
 
 begin
 
 \<comment> \<open>A tactic for verification of hybrid programs \<close>
 
 named_theorems hoare_intros
 
 declare H_assignl [hoare_intros]
     and H_cond [hoare_intros]
     and local_flow.H_g_ode_subset [hoare_intros]
     and H_g_ode_inv [hoare_intros]
 
 method body_hoare 
   = (rule hoare_intros,(simp)?; body_hoare?)
 
 method hyb_hoare for P::"'a pred" 
   = (rule H_loopI, rule H_seq[where R=P]; body_hoare?)
 
 \<comment> \<open>A tactic for refinement of hybrid programs \<close>
 
 named_theorems refine_intros "selected refinement lemmas"
 
 declare R_loopI [refine_intros]
     and R_loop_mono [refine_intros]
     and R_cond_law [refine_intros]
     and R_cond_mono [refine_intros]
     and R_while_law [refine_intros]
     and R_assignl [refine_intros]
     and R_seq_law [refine_intros]
     and R_seq_mono [refine_intros]
     and R_g_evol_law [refine_intros]
     and R_skip [refine_intros]
     and R_g_ode_inv [refine_intros]
 
 method refinement
   = (rule refine_intros; (refinement)?)
 
 subsubsection \<open>Pendulum\<close>
 
 text \<open> The ODEs @{text "x' t = y t"} and {text "y' t = - x t"} describe the circular motion of 
 a mass attached to a string looked from above. We use @{text "s$1"} to represent the x-coordinate
 and @{text "s$2"} for the y-coordinate. We prove that this motion remains circular. \<close>
 
 abbreviation fpend :: "real^2 \<Rightarrow> real^2" ("f")
   where "f s \<equiv> (\<chi> i. if i=1 then s$2 else -s$1)"
 
 abbreviation pend_flow :: "real \<Rightarrow> real^2 \<Rightarrow> real^2" ("\<phi>")
   where "\<phi> \<tau> s \<equiv> (\<chi> i. if i = 1 then s$1 \<cdot> cos \<tau> + s$2 \<cdot> sin \<tau> 
   else - s$1 \<cdot> sin \<tau> + s$2 \<cdot> cos \<tau>)"
 
 \<comment> \<open>Verified with annotated dynamics \<close>
 
 lemma pendulum_dyn: "\<^bold>{\<lambda>s. r\<^sup>2 = (s $ 1)\<^sup>2 + (s $ 2)\<^sup>2\<^bold>} EVOL \<phi> G T \<^bold>{\<lambda>s. r\<^sup>2 = (s $ 1)\<^sup>2 + (s $ 2)\<^sup>2\<^bold>}"
   by simp
 
 \<comment> \<open>Verified with differential invariants \<close>
 
 lemma pendulum_inv: "\<^bold>{\<lambda>s. r\<^sup>2 = (s $ 1)\<^sup>2 + (s $ 2)\<^sup>2\<^bold>} (x\<acute>=f & G) \<^bold>{\<lambda>s. r\<^sup>2 = (s $ 1)\<^sup>2 + (s $ 2)\<^sup>2\<^bold>}"
   by (auto intro!: diff_invariant_rules poly_derivatives)
 
 \<comment> \<open>Verified with the flow \<close>
 
 lemma local_flow_pend: "local_flow f UNIV UNIV \<phi>"
   apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def vec_eq_iff, clarsimp)
   apply(rule_tac x="1" in exI, clarsimp, rule_tac x=1 in exI)
     apply(simp add: dist_norm norm_vec_def L2_set_def power2_commute UNIV_2)
   by (auto simp: forall_2 intro!: poly_derivatives)
 
 lemma pendulum_flow: "\<^bold>{\<lambda>s. r\<^sup>2 = (s $ 1)\<^sup>2 + (s $ 2)\<^sup>2\<^bold>} (x\<acute>=f & G) \<^bold>{\<lambda>s. r\<^sup>2 = (s $ 1)\<^sup>2 + (s $ 2)\<^sup>2\<^bold>}"
   by (subst local_flow.sH_g_ode_subset[OF local_flow_pend], simp_all)
 
 no_notation fpend ("f")
         and pend_flow ("\<phi>")
 
 
 subsubsection \<open> Bouncing Ball \<close>
 
 text \<open> A ball is dropped from rest at an initial height @{text "h"}. The motion is described with
 the free-fall equations @{text "x' t = v t"} and @{text "v' t = g"} where @{text "g"} is the
 constant acceleration due to gravity. The bounce is modelled with a variable assignment that
 flips the velocity. That is, we model it as a completely elastic collision with the ground. We use 
 @{text "s$1"} to represent the ball's height and @{text "s$2"} for its velocity. We prove that the 
 ball remains above ground and below its initial resting position. \<close>
 
 abbreviation fball :: "real \<Rightarrow> real^2 \<Rightarrow> real^2" ("f") 
   where "f g s \<equiv> (\<chi> i. if i=1 then s$2 else g)"
 
 abbreviation ball_flow :: "real \<Rightarrow> real \<Rightarrow> real^2 \<Rightarrow> real^2" ("\<phi>") 
   where "\<phi> g \<tau> s \<equiv> (\<chi> i. if i=1 then g \<cdot> \<tau> ^ 2/2 + s$2 \<cdot> \<tau> + s$1 else g \<cdot> \<tau> + s$2)"
 
 \<comment> \<open>Verified with differential invariants \<close>
 
 named_theorems bb_real_arith "real arithmetic properties for the bouncing ball."
 
 lemma [bb_real_arith]: 
   assumes "0 > g" and inv: "2 \<cdot> g \<cdot> x - 2 \<cdot> g \<cdot> h = v \<cdot> v"
   shows "(x::real) \<le> h"
 proof-
   have "v \<cdot> v = 2 \<cdot> g \<cdot> x - 2 \<cdot> g \<cdot> h \<and> 0 > g" 
     using inv and \<open>0 > g\<close> by auto
   hence obs:"v \<cdot> v = 2 \<cdot> g \<cdot> (x - h) \<and> 0 > g \<and> v \<cdot> v \<ge> 0" 
     using left_diff_distrib mult.commute by (metis zero_le_square) 
   hence "(v \<cdot> v)/(2 \<cdot> g) = (x - h)" 
     by auto 
   also from obs have "(v \<cdot> v)/(2 \<cdot> g) \<le> 0"
     using divide_nonneg_neg by fastforce 
   ultimately have "h - x \<ge> 0" 
     by linarith
   thus ?thesis by auto
 qed
 
 lemma fball_invariant: 
   fixes g h :: real
   defines dinv: "I \<equiv> (\<lambda>s. 2 \<cdot> g \<cdot> s$1 - 2 \<cdot> g \<cdot> h - (s$2 \<cdot> s$2) = 0)"
   shows "diff_invariant I (\<lambda>t. f g) (\<lambda>s. UNIV) UNIV 0 G"
   unfolding dinv apply(rule diff_invariant_rules, simp)
   by(auto intro!: poly_derivatives)
 
 lemma bouncing_ball_inv: "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow>
  \<^bold>{\<lambda>s. s$1 = h \<and> s$2 = 0\<^bold>}
   (LOOP 
       ((x\<acute>= f g & (\<lambda> s. s$1 \<ge> 0) DINV (\<lambda>s. 2 \<cdot> g \<cdot> s$1 - 2 \<cdot> g \<cdot> h - s$2 \<cdot> s$2 = 0));
        (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip)) 
     INV (\<lambda>s. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2))
  \<^bold>{\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h\<^bold>}"
   apply(hyb_hoare "\<lambda>s::real^2. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2")
   using fball_invariant by (auto simp: bb_real_arith intro!: poly_derivatives diff_invariant_rules)
 
 \<comment> \<open>Verified with annotated dynamics \<close>
 
 lemma [bb_real_arith]:
   assumes invar: "2 \<cdot> g \<cdot> x = 2 \<cdot> g \<cdot> h + v \<cdot> v"
     and pos: "g \<cdot> \<tau>\<^sup>2 / 2 + v \<cdot> \<tau> + (x::real) = 0"
   shows "2 \<cdot> g \<cdot> h + (- (g \<cdot> \<tau>) - v) \<cdot> (- (g \<cdot> \<tau>) - v) = 0"
     and "2 \<cdot> g \<cdot> h + (g \<cdot> \<tau> \<cdot> (g \<cdot> \<tau> + v) + v \<cdot> (g \<cdot> \<tau> + v)) = 0"
 proof-
   from pos have "g \<cdot> \<tau>\<^sup>2  + 2 \<cdot> v \<cdot> \<tau> + 2 \<cdot> x = 0" by auto
   then have "g\<^sup>2  \<cdot> \<tau>\<^sup>2  + 2 \<cdot> g \<cdot> v \<cdot> \<tau> + 2 \<cdot> g \<cdot> x = 0"
-    by (metis (mono_tags, opaque_lifting) Groups.mult_ac(1,3) mult_zero_right
+    by (metis (mono_tags) Groups.mult_ac(1,3) mult_zero_right
         monoid_mult_class.power2_eq_square semiring_class.distrib_left)
   hence "g\<^sup>2 \<cdot> \<tau>\<^sup>2 + 2 \<cdot> g \<cdot> v \<cdot> \<tau> + v\<^sup>2 + 2 \<cdot> g \<cdot> h = 0"
     using invar by (simp add: monoid_mult_class.power2_eq_square) 
   hence obs: "(g \<cdot> \<tau> + v)\<^sup>2 + 2 \<cdot> g \<cdot> h = 0"
-    apply(subst power2_sum) by (metis (no_types, opaque_lifting) Groups.add_ac(2, 3) 
+    apply(subst power2_sum) by (metis (no_types) Groups.add_ac(2, 3) 
         Groups.mult_ac(2, 3) monoid_mult_class.power2_eq_square nat_distrib(2))
   thus "2 \<cdot> g \<cdot> h + (g \<cdot> \<tau> \<cdot> (g \<cdot> \<tau> + v) + v \<cdot> (g \<cdot> \<tau> + v)) = 0"
     by (simp add: monoid_mult_class.power2_eq_square)
   have  "2 \<cdot> g \<cdot> h + (- ((g \<cdot> \<tau>) + v))\<^sup>2 = 0"
     using obs by (metis Groups.add_ac(2) power2_minus)
   thus "2 \<cdot> g \<cdot> h + (- (g \<cdot> \<tau>) - v) \<cdot> (- (g \<cdot> \<tau>) - v) = 0"
     by (simp add: monoid_mult_class.power2_eq_square)
 qed
 
 lemma [bb_real_arith]:
   assumes invar: "2 \<cdot> g \<cdot> x = 2 \<cdot> g \<cdot> h + v \<cdot> v"
   shows "2 \<cdot> g \<cdot> (g \<cdot> \<tau>\<^sup>2 / 2 + v \<cdot> \<tau> + (x::real)) = 
   2 \<cdot> g \<cdot> h + (g \<cdot> \<tau> \<cdot> (g \<cdot> \<tau> + v) + v \<cdot> (g \<cdot> \<tau> + v))" (is "?lhs = ?rhs")
 proof-
   have "?lhs = g\<^sup>2 \<cdot> \<tau>\<^sup>2 + 2 \<cdot> g \<cdot> v \<cdot> \<tau> + 2 \<cdot> g \<cdot> x" 
     by(auto simp: algebra_simps semiring_normalization_rules(29))
     also have "... = g\<^sup>2 \<cdot> \<tau>\<^sup>2 + 2 \<cdot> g \<cdot> v \<cdot> \<tau> + 2 \<cdot> g \<cdot> h + v \<cdot> v" (is "... = ?middle")
       by(subst invar, simp)
     finally have "?lhs = ?middle".
   moreover 
   {have "?rhs = g \<cdot> g \<cdot> (\<tau> \<cdot> \<tau>) + 2 \<cdot> g \<cdot> v \<cdot> \<tau> + 2 \<cdot> g \<cdot> h + v \<cdot> v"
     by (simp add: Groups.mult_ac(2,3) semiring_class.distrib_left)
   also have "... = ?middle"
     by (simp add: semiring_normalization_rules(29))
   finally have "?rhs = ?middle".}
   ultimately show ?thesis by auto
 qed
 
 lemma bouncing_ball_dyn: "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow>
   \<^bold>{\<lambda>s. s$1 = h \<and> s$2 = 0\<^bold>}
   (LOOP 
       ((EVOL (\<phi> g) (\<lambda> s. s$1 \<ge> 0) T);
        (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip)) 
     INV (\<lambda>s. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2)
   ) \<^bold>{\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h\<^bold>}"
   apply(hyb_hoare "\<lambda>s::real^2. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2")
   by (auto simp: bb_real_arith)
 
 \<comment> \<open>Verified with the flow \<close>
 
 lemma local_flow_ball: "local_flow (f g) UNIV UNIV (\<phi> g)"
   apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def vec_eq_iff, clarsimp)
   apply(rule_tac x="1/2" in exI, clarsimp, rule_tac x=1 in exI)
     apply(simp add: dist_norm norm_vec_def L2_set_def UNIV_2)
   by (auto simp: forall_2 intro!: poly_derivatives)
 
 lemma bouncing_ball_flow: "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow>
   \<^bold>{\<lambda>s. s$1 = h \<and> s$2 = 0\<^bold>}
   (LOOP 
       ((x\<acute>= f g & (\<lambda> s. s$1 \<ge> 0));
        (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip)) 
     INV (\<lambda>s. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2)
   ) \<^bold>{\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h\<^bold>}"
   apply(rule H_loopI; (rule H_seq[where R="\<lambda>s. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2"])?)
      apply(subst local_flow.sH_g_ode_subset[OF local_flow_ball])
   by (auto simp: bb_real_arith)
 
 \<comment> \<open>Refined with annotated dynamics \<close>
 
 lemma R_bb_assign: "g < (0::real) \<Longrightarrow> 0 \<le> h \<Longrightarrow> 
   2 ::= (\<lambda>s. - s$2) \<le> rel_R 
     \<lceil>\<lambda>s. s$1 = 0 \<and> 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2\<rceil> 
     \<lceil>\<lambda>s. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2\<rceil>"
   by (rule R_assign_law, auto)
 
 lemma R_bouncing_ball_dyn:
   assumes "g < 0" and "h \<ge> 0"
   shows "rel_R \<lceil>\<lambda>s. s$1 = h \<and> s$2 = 0\<rceil> \<lceil>\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h\<rceil> \<ge> 
   (LOOP 
       ((EVOL (\<phi> g) (\<lambda> s. s$1 \<ge> 0) T);
        (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip)) 
     INV (\<lambda>s. 0 \<le> s$1 \<and> 2 \<cdot> g \<cdot> s$1 = 2 \<cdot> g \<cdot> h + s$2 \<cdot> s$2))"
   apply(refinement; (rule R_bb_assign[OF assms])?)
   using assms by (auto simp: bb_real_arith)
 
 no_notation fball ("f")
         and ball_flow ("\<phi>")
 
 
 subsubsection \<open> Thermostat \<close>
 
 text \<open> A thermostat has a chronometer, a thermometer and a switch to turn on and off a heater. 
 At most every @{text "\<tau>"} minutes, it sets its chronometer to @{term "0::real"}, it registers 
 the room temperature, and it turns the heater on (or off) based on this reading. The temperature 
 follows the ODE @{text "T' = - a * (T - U)"} where @{text "U = L \<ge> 0"} when the heater 
 is on, and @{text "U = 0"} when it is off. We use @{term "1::4"} to denote the room's temperature, 
 @{term "2::4"} is time as measured by the thermostat's chronometer, and @{term "3::4"} is a variable
 to save temperature measurements. Finally, @{term "4::5"} states whether the heater is on 
 (@{text "s$4 = 1"}) or off (@{text "s$4 = 0"}). We prove that the thermostat keeps the room's 
 temperature between @{text "Tmin"} and @{text "Tmax"}. \<close>
 
 abbreviation therm_vec_field :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> real^4" ("f")
   where "f a L s \<equiv> (\<chi> i. if i = 2 then 1 else (if i = 1 then - a * (s$1 - L) else 0))"
 
 abbreviation therm_guard :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("G")
   where "G Tmin Tmax a L s \<equiv> (s$2 \<le> - (ln ((L-(if L=0 then Tmin else Tmax))/(L-s$3)))/a)"
 
 abbreviation therm_loop_inv :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("I")
   where "I Tmin Tmax s \<equiv> Tmin \<le> s$1 \<and> s$1 \<le> Tmax \<and> (s$4 = 0 \<or> s$4 = 1)"
 
 abbreviation therm_flow :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> real^4" ("\<phi>")
   where "\<phi> a L \<tau> s \<equiv> (\<chi> i. if i = 1 then - exp(-a * \<tau>) * (L - s$1) + L else 
   (if i = 2 then \<tau> + s$2 else s$i))"
 
 \<comment> \<open>Verified with the flow \<close>
 
 lemma norm_diff_therm_dyn: "0 < a \<Longrightarrow> \<parallel>f a L s\<^sub>1 - f a L s\<^sub>2\<parallel> = \<bar>a\<bar> * \<bar>s\<^sub>1$1 - s\<^sub>2$1\<bar>"
 proof(simp add: norm_vec_def L2_set_def, unfold UNIV_4, simp)
   assume a1: "0 < a"
   have f2: "\<And>r ra. \<bar>(r::real) + - ra\<bar> = \<bar>ra + - r\<bar>"
     by (metis abs_minus_commute minus_real_def)
   have "\<And>r ra rb. (r::real) * ra + - (r * rb) = r * (ra + - rb)"
     by (metis minus_real_def right_diff_distrib)
   hence "\<bar>a * (s\<^sub>1$1 + - L) + - (a * (s\<^sub>2$1 + - L))\<bar> = a * \<bar>s\<^sub>1$1 + - s\<^sub>2$1\<bar>"
     using a1 by (simp add: abs_mult)
   thus "\<bar>a * (s\<^sub>2$1 - L) - a * (s\<^sub>1$1 - L)\<bar> = a * \<bar>s\<^sub>1$1 - s\<^sub>2$1\<bar>"
     using f2 minus_real_def by presburger
 qed
 
 lemma local_lipschitz_therm_dyn:
   assumes "0 < (a::real)"
   shows "local_lipschitz UNIV UNIV (\<lambda>t::real. f a L)"
   apply(unfold local_lipschitz_def lipschitz_on_def dist_norm)
   apply(clarsimp, rule_tac x=1 in exI, clarsimp, rule_tac x=a in exI)
   using assms apply(simp_all add: norm_diff_therm_dyn)
   apply(simp add: norm_vec_def L2_set_def, unfold UNIV_4, clarsimp)
   unfolding real_sqrt_abs[symmetric] by (rule real_le_lsqrt) auto
 
 lemma local_flow_therm: "a > 0 \<Longrightarrow> local_flow (f a L) UNIV UNIV (\<phi> a L)"
   by (unfold_locales, auto intro!: poly_derivatives local_lipschitz_therm_dyn 
       simp: forall_4 vec_eq_iff)
 
 lemma therm_dyn_down_real_arith:
   assumes "a > 0" and Thyps: "0 < Tmin" "Tmin \<le> T" "T \<le> Tmax"
     and thyps: "0 \<le> (\<tau>::real)" "\<forall>\<tau>\<in>{0..\<tau>}. \<tau> \<le> - (ln (Tmin / T) / a) "
   shows "Tmin \<le> exp (-a * \<tau>) * T" and "exp (-a * \<tau>) * T \<le> Tmax"
 proof-
   have "0 \<le> \<tau> \<and> \<tau> \<le> - (ln (Tmin / T) / a)"
     using thyps by auto
   hence "ln (Tmin / T) \<le> - a * \<tau> \<and> - a * \<tau> \<le> 0"
     using assms(1) divide_le_cancel by fastforce
   also have "Tmin / T > 0"
     using Thyps by auto
   ultimately have obs: "Tmin / T \<le> exp (-a * \<tau>)" "exp (-a * \<tau>) \<le> 1"
     using exp_ln exp_le_one_iff by (metis exp_less_cancel_iff not_less, simp)
   thus "Tmin \<le> exp (-a * \<tau>) * T"
     using Thyps by (simp add: pos_divide_le_eq)
   show "exp (-a * \<tau>) * T \<le> Tmax"
     using Thyps mult_left_le_one_le[OF _ exp_ge_zero obs(2), of T] 
       less_eq_real_def order_trans_rules(23) by blast
 qed
 
 lemma therm_dyn_up_real_arith:
   assumes "a > 0" and Thyps: "Tmin \<le> T" "T \<le> Tmax" "Tmax < (L::real)"
     and thyps: "0 \<le> \<tau>" "\<forall>\<tau>\<in>{0..\<tau>}. \<tau> \<le> - (ln ((L - Tmax) / (L - T)) / a) "
   shows "L - Tmax \<le> exp (-(a * \<tau>)) * (L - T)" 
     and "L - exp (-(a * \<tau>)) * (L - T) \<le> Tmax" 
     and "Tmin \<le> L - exp (-(a * \<tau>)) * (L - T)"
 proof-
   have "0 \<le> \<tau> \<and> \<tau> \<le> - (ln ((L - Tmax) / (L - T)) / a)"
     using thyps by auto
   hence "ln ((L - Tmax) / (L - T)) \<le> - a * \<tau> \<and> - a * \<tau> \<le> 0"
     using assms(1) divide_le_cancel by fastforce
   also have "(L - Tmax) / (L - T) > 0"
     using Thyps by auto
   ultimately have "(L - Tmax) / (L - T) \<le> exp (-a * \<tau>) \<and> exp (-a * \<tau>) \<le> 1"
     using exp_ln exp_le_one_iff by (metis exp_less_cancel_iff not_less)
   moreover have "L - T > 0"
     using Thyps by auto
   ultimately have obs: "(L - Tmax) \<le> exp (-a * \<tau>) * (L - T) \<and> exp (-a * \<tau>) * (L - T) \<le> (L - T)"
     by (simp add: pos_divide_le_eq)
   thus "(L - Tmax) \<le> exp (-(a * \<tau>)) * (L - T)"
     by auto
   thus "L - exp (-(a * \<tau>)) * (L - T) \<le> Tmax"
     by auto
   show "Tmin \<le> L - exp (-(a * \<tau>)) * (L - T)"
     using Thyps and obs by auto
 qed
 
 lemmas H_g_ode_therm = local_flow.sH_g_ode_ivl[OF local_flow_therm _ UNIV_I]
 
 lemma thermostat_flow: 
   assumes "0 < a" and "0 \<le> \<tau>" and "0 < Tmin" and "Tmax < L"
   shows "\<^bold>{I Tmin Tmax\<^bold>}
   (LOOP (
     \<comment> \<open>control\<close>
     (2 ::= (\<lambda>s. 0));
     (3 ::= (\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> Tmin + 1) THEN 
       (4 ::= (\<lambda>s.1)) 
      ELSE IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> Tmax - 1) THEN 
       (4 ::= (\<lambda>s.0)) 
      ELSE skip);
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN 
       (x\<acute>= (\<lambda>t. f a 0) & G Tmin Tmax a 0 on (\<lambda>s. {0..\<tau>}) UNIV @ 0) 
     ELSE 
       (x\<acute>= (\<lambda>t. f a L) & G Tmin Tmax a L on (\<lambda>s. {0..\<tau>}) UNIV @ 0))
   ) INV I Tmin Tmax)
    \<^bold>{I Tmin Tmax\<^bold>}"
   apply(rule H_loopI)
     apply(rule_tac R="\<lambda>s. I Tmin Tmax s \<and> s$2=0" in H_seq, simp)
      apply(rule_tac R="\<lambda>s. I Tmin Tmax s \<and> s$2=0 \<and> s$1 = s$3" in H_seq, simp)
   apply(rule_tac R="\<lambda>s. I Tmin Tmax s \<and> s$2=0 \<and> s$1 = s$3" in H_seq, simp)
     apply(rule H_cond, simp_all add: H_g_ode_therm[OF assms(1,2)], safe)
   using therm_dyn_up_real_arith[OF assms(1) _ _ assms(4), of Tmin]
     and therm_dyn_down_real_arith[OF assms(1,3), of _ Tmax] by auto
 
 \<comment> \<open>Refined with the flow \<close>
 
 lemma R_therm_dyn_down: 
   assumes "a > 0" and "0 \<le> \<tau>" and "0 < Tmin" and "Tmax < L"
   shows "rel_R \<lceil>\<lambda>s. s$4 = 0 \<and> I Tmin Tmax s \<and> s$2 = 0 \<and> s$3 = s$1\<rceil> \<lceil>I Tmin Tmax\<rceil> \<ge> 
     (x\<acute>= (\<lambda>t. f a 0) & G Tmin Tmax a 0 on (\<lambda>s. {0..\<tau>}) UNIV @ 0)"
   apply(rule local_flow.R_g_ode_ivl[OF local_flow_therm])
   using assms therm_dyn_down_real_arith[OF assms(1,3), of _ Tmax] by auto
 
 lemma R_therm_dyn_up: 
   assumes "a > 0" and "0 \<le> \<tau>" and "0 < Tmin" and "Tmax < L"
   shows "rel_R \<lceil>\<lambda>s. s$4 \<noteq> 0 \<and> I Tmin Tmax s \<and> s$2 = 0 \<and> s$3 = s$1\<rceil> \<lceil>I Tmin Tmax\<rceil> \<ge> 
     (x\<acute>= (\<lambda>t. f a L) & G Tmin Tmax a L on (\<lambda>s. {0..\<tau>}) UNIV @ 0)"
   apply(rule local_flow.R_g_ode_ivl[OF local_flow_therm])
   using assms therm_dyn_up_real_arith[OF assms(1) _ _ assms(4), of Tmin] by auto
 
 lemma R_therm_dyn:
   assumes "a > 0" and "0 \<le> \<tau>" and "0 < Tmin" and "Tmax < L"
   shows "rel_R \<lceil>\<lambda>s. I Tmin Tmax s \<and> s$2 = 0 \<and> s$3 = s$1\<rceil> \<lceil>I Tmin Tmax\<rceil> \<ge> 
   (IF (\<lambda>s. s$4 = 0) THEN 
     (x\<acute>= (\<lambda>t. f a 0) & G Tmin Tmax a 0 on (\<lambda>s. {0..\<tau>}) UNIV @ 0) 
   ELSE 
     (x\<acute>= (\<lambda>t. f a L) & G Tmin Tmax a L on (\<lambda>s. {0..\<tau>}) UNIV @ 0))"
   apply(rule order_trans, rule R_cond_mono)
   apply(rule R_therm_dyn_down[OF assms])
   using R_therm_dyn_down[OF assms] R_therm_dyn_up[OF assms] by (auto intro!: R_cond)
 
 lemma R_therm_assign1: "rel_R \<lceil>I Tmin Tmax\<rceil> \<lceil>\<lambda>s. I Tmin Tmax s \<and> s$2 = 0\<rceil> \<ge> (2 ::= (\<lambda>s. 0))"
   by (auto simp: R_assign_law)
 
 lemma R_therm_assign2: 
   "rel_R \<lceil>\<lambda>s. I Tmin Tmax s \<and> s$2 = 0\<rceil> \<lceil>\<lambda>s. I Tmin Tmax s \<and> s$2 = 0 \<and> s$3 = s$1\<rceil> \<ge> (3 ::= (\<lambda>s. s$1))"
   by (auto simp: R_assign_law)
 
 lemma R_therm_ctrl:
   "rel_R \<lceil>I Tmin Tmax\<rceil> \<lceil>\<lambda>s. I Tmin Tmax s \<and> s$2 = 0 \<and> s$3 = s$1\<rceil> \<ge>
   (2 ::= (\<lambda>s. 0));
   (3 ::= (\<lambda>s. s$1));
   (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> Tmin + 1) THEN 
     (4 ::= (\<lambda>s.1)) 
    ELSE IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> Tmax - 1) THEN 
     (4 ::= (\<lambda>s.0)) 
    ELSE skip)"
   apply(refinement, rule R_therm_assign1, rule R_therm_assign2)
   by (rule R_assign_law, simp)+ auto
 
 lemma R_therm_loop: "rel_R \<lceil>I Tmin Tmax\<rceil> \<lceil>I Tmin Tmax\<rceil> \<ge> 
   (LOOP 
     rel_R \<lceil>I Tmin Tmax\<rceil> \<lceil>\<lambda>s. I Tmin Tmax s \<and> s$2 = 0 \<and> s$3 = s$1\<rceil>;
     rel_R \<lceil>\<lambda>s. I Tmin Tmax s \<and> s$2 = 0 \<and> s$3 = s$1\<rceil> \<lceil>I Tmin Tmax\<rceil>
   INV I Tmin Tmax)"
   by (intro R_loopI R_seq, simp_all)
 
 lemma R_thermostat_flow: 
   assumes "a > 0" and "0 \<le> \<tau>" and "0 < Tmin" and "Tmax < L"
   shows "rel_R \<lceil>I Tmin Tmax\<rceil> \<lceil>I Tmin Tmax\<rceil> \<ge> 
   (LOOP (
     \<comment> \<open>control\<close>
     (2 ::= (\<lambda>s. 0));(3 ::= (\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> Tmin + 1) THEN 
       (4 ::= (\<lambda>s.1)) 
      ELSE IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> Tmax - 1) THEN 
       (4 ::= (\<lambda>s.0)) 
      ELSE skip);
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN 
       (x\<acute>= (\<lambda>t. f a 0) & G Tmin Tmax a 0 on (\<lambda>s. {0..\<tau>}) UNIV @ 0) 
     ELSE 
       (x\<acute>= (\<lambda>t. f a L) & G Tmin Tmax a L on (\<lambda>s. {0..\<tau>}) UNIV @ 0))
   ) INV I Tmin Tmax)"
   apply(refinement; (rule R_therm_assign1)?, (rule R_therm_assign2)?,
       (rule R_therm_dyn_down)?, (rule R_therm_dyn_up)?, (rule R_assign_law)?)
   using assms by auto
 
 no_notation therm_vec_field ("f")
         and therm_flow ("\<phi>")
         and therm_guard ("G")
         and therm_loop_inv ("I")
 
 
 subsubsection \<open> Water tank \<close> \<comment> \<open> Variation of Hespanha and Alur's tank \<close>
 
 subsubsection \<open> Tank \<close>
 
 text \<open> A controller turns a water pump on and off to keep the level of water @{text "h"} in a tank
 within an acceptable range @{text "hmin \<le> h \<le> hmax"}. Just like in the previous example, after 
 each intervention, the controller registers the current level of water and resets its chronometer,
 then it changes the status of the water pump accordingly. The level of water grows linearly 
 @{text "h' = k"} at a rate of @{text "k = c\<^sub>i-c\<^sub>o"} if the pump is on, and at a rate of 
 @{text "k = -c\<^sub>o"} if the pump is off. We use @{term "1::4"} to denote the tank's level of water,
 @{term "2::4"} is time as measured by the controller's chronometer, @{term "3::4"} is the
 level of water measured by the chronometer, and @{term "4::4"} states whether the pump is on
 (@{text "s$4 = 1"}) or off (@{text "s$4 = 0"}). We prove that the controller keeps the level of
 water between @{text "hmin"} and @{text "hmax"}. \<close>
 
 abbreviation tank_vec_field :: "real \<Rightarrow> real^4 \<Rightarrow> real^4" ("f")
   where "f k s \<equiv> (\<chi> i. if i = 2 then 1 else (if i = 1 then k else 0))"
 
 abbreviation tank_flow :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> real^4" ("\<phi>")
   where "\<phi> k \<tau> s \<equiv> (\<chi> i. if i = 1 then k * \<tau> + s$1 else 
   (if i = 2 then \<tau> + s$2 else s$i))"
 
 abbreviation tank_guard :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("G")
   where "G Hm k s \<equiv> s$2 \<le> (Hm - s$3)/k"
 
 abbreviation tank_loop_inv :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("I")
   where "I hmin hmax s \<equiv> hmin \<le> s$1 \<and> s$1 \<le> hmax \<and> (s$4 = 0 \<or> s$4 = 1)"
 
 abbreviation tank_diff_inv :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("dI")
   where "dI hmin hmax k s \<equiv> s$1 = k \<cdot> s$2 + s$3 \<and> 0 \<le> s$2 \<and> 
     hmin \<le> s$3 \<and> s$3 \<le> hmax \<and> (s$4 =0 \<or> s$4 = 1)"
 
 \<comment> \<open>Verified with the flow \<close>
 
 lemma local_flow_tank: "local_flow (f k) UNIV UNIV (\<phi> k)"
   apply (unfold_locales, unfold local_lipschitz_def lipschitz_on_def, simp_all, clarsimp)
   apply(rule_tac x="1/2" in exI, clarsimp, rule_tac x=1 in exI)
   apply(simp add: dist_norm norm_vec_def L2_set_def, unfold UNIV_4)
   by (auto intro!: poly_derivatives simp: vec_eq_iff)
 
 lemma tank_arith:
   assumes "0 \<le> (\<tau>::real)" and "0 < c\<^sub>o" and "c\<^sub>o < c\<^sub>i"
   shows "\<forall>\<tau>\<in>{0..\<tau>}. \<tau> \<le> - ((hmin - y) / c\<^sub>o) \<Longrightarrow>  hmin \<le> y - c\<^sub>o * \<tau>"
     and "\<forall>\<tau>\<in>{0..\<tau>}. \<tau> \<le> (hmax - y) / (c\<^sub>i - c\<^sub>o) \<Longrightarrow>  (c\<^sub>i - c\<^sub>o) * \<tau> + y \<le> hmax"
     and "hmin \<le> y \<Longrightarrow> hmin \<le> (c\<^sub>i - c\<^sub>o) \<cdot> \<tau> + y"
     and "y \<le> hmax \<Longrightarrow> y - c\<^sub>o \<cdot> \<tau> \<le> hmax"
   apply(simp_all add: field_simps le_divide_eq assms)
   using assms apply (meson add_mono less_eq_real_def mult_left_mono)
   using assms by (meson add_increasing2 less_eq_real_def mult_nonneg_nonneg) 
 
 lemmas H_g_ode_tank = local_flow.sH_g_ode_ivl[OF local_flow_tank _ UNIV_I]
 
 lemma tank_flow:
   assumes "0 \<le> \<tau>" and "0 < c\<^sub>o" and "c\<^sub>o < c\<^sub>i"
   shows "\<^bold>{I hmin hmax\<^bold>}
   (LOOP 
     \<comment> \<open>control\<close>
     ((2 ::=(\<lambda>s.0));(3 ::=(\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> hmin + 1) THEN (4 ::= (\<lambda>s.1)) ELSE 
     (IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> hmax - 1) THEN (4 ::= (\<lambda>s.0)) ELSE skip));
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN (x\<acute>= (\<lambda>t. f (c\<^sub>i-c\<^sub>o)) & G hmax (c\<^sub>i-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0) 
      ELSE (x\<acute>= (\<lambda>t. f (-c\<^sub>o)) & G hmin (-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0)) )
   INV I hmin hmax) 
   \<^bold>{I hmin hmax\<^bold>}"
    apply(rule H_loopI)
     apply(rule_tac R="\<lambda>s. I hmin hmax s \<and> s$2=0" in H_seq, simp)
      apply(rule_tac R="\<lambda>s. I hmin hmax s \<and> s$2=0 \<and> s$3 = s$1" in H_seq, simp)
       apply(rule_tac R="\<lambda>s. I hmin hmax s \<and> s$2=0 \<and> s$3 = s$1" in H_seq, simp)
      apply(rule H_cond, simp_all add: H_g_ode_tank[OF assms(1)])
   using assms tank_arith[OF _ assms(2,3)] by auto
 
 \<comment> \<open>Verified with differential invariants \<close>
 
 lemma tank_diff_inv:
   "0 \<le> \<tau> \<Longrightarrow> diff_invariant (dI hmin hmax k) (\<lambda>t. f k) (\<lambda>s. {0..\<tau>}) UNIV 0 Guard"
   apply(intro diff_invariant_conj_rule)
       apply(force intro!: poly_derivatives diff_invariant_rules)
      apply(rule_tac \<nu>'="\<lambda>t. 0" and \<mu>'="\<lambda>t. 1" in diff_invariant_leq_rule, simp_all, presburger)
     apply(rule_tac \<nu>'="\<lambda>t. 0" and \<mu>'="\<lambda>t. 0" in diff_invariant_leq_rule, simp_all)
     apply(force intro!: poly_derivatives)+
   by (auto intro!: poly_derivatives diff_invariant_rules)
 
 lemma tank_inv_arith1:
   assumes "0 \<le> (\<tau>::real)" and "c\<^sub>o < c\<^sub>i" and b: "hmin \<le> y\<^sub>0" and g: "\<tau> \<le> (hmax - y\<^sub>0) / (c\<^sub>i - c\<^sub>o)"
   shows "hmin \<le> (c\<^sub>i - c\<^sub>o) \<cdot> \<tau> + y\<^sub>0" and "(c\<^sub>i - c\<^sub>o) \<cdot> \<tau> + y\<^sub>0 \<le> hmax"
 proof-
   have "(c\<^sub>i - c\<^sub>o) \<cdot> \<tau> \<le> (hmax - y\<^sub>0)"
     using g assms(2,3) by (metis diff_gt_0_iff_gt mult.commute pos_le_divide_eq) 
   thus "(c\<^sub>i - c\<^sub>o) \<cdot> \<tau> + y\<^sub>0 \<le> hmax"
     by auto
   show "hmin \<le> (c\<^sub>i - c\<^sub>o) \<cdot> \<tau> + y\<^sub>0"
     using b assms(1,2) by (metis add.commute add_increasing2 diff_ge_0_iff_ge 
         less_eq_real_def mult_nonneg_nonneg) 
 qed
 
 lemma tank_inv_arith2:
   assumes "0 \<le> (\<tau>::real)" and "0 < c\<^sub>o" and b: "y\<^sub>0 \<le> hmax" and g: "\<tau> \<le> - ((hmin - y\<^sub>0) / c\<^sub>o)"
   shows "hmin \<le> y\<^sub>0 - c\<^sub>o \<cdot> \<tau>" and "y\<^sub>0 - c\<^sub>o \<cdot> \<tau> \<le> hmax"
 proof-
   have "\<tau> \<cdot> c\<^sub>o \<le> y\<^sub>0 - hmin"
     using g \<open>0 < c\<^sub>o\<close> pos_le_minus_divide_eq by fastforce 
   thus "hmin \<le> y\<^sub>0 - c\<^sub>o \<cdot> \<tau>"
     by (auto simp: mult.commute)
   show "y\<^sub>0 - c\<^sub>o \<cdot> \<tau> \<le> hmax" 
     using b assms(1,2) by (smt mult_nonneg_nonneg) 
 qed
 
 lemma tank_inv:
   assumes "0 \<le> \<tau>" and "0 < c\<^sub>o" and "c\<^sub>o < c\<^sub>i"
   shows "\<^bold>{I hmin hmax\<^bold>}
   (LOOP 
     \<comment> \<open>control\<close>
     ((2 ::=(\<lambda>s.0));(3 ::=(\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> hmin + 1) THEN (4 ::= (\<lambda>s.1)) ELSE 
     (IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> hmax - 1) THEN (4 ::= (\<lambda>s.0)) ELSE skip));
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN 
       (x\<acute>= (\<lambda>t. f (c\<^sub>i-c\<^sub>o)) & G hmax (c\<^sub>i-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0 DINV (dI hmin hmax (c\<^sub>i-c\<^sub>o))) 
      ELSE 
       (x\<acute>= (\<lambda>t. f (-c\<^sub>o)) & G hmin (-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0 DINV (dI hmin hmax (-c\<^sub>o)))) )
   INV I hmin hmax)
   \<^bold>{I hmin hmax\<^bold>}"
   apply(rule H_loopI)
     apply(rule_tac R="\<lambda>s. I hmin hmax s \<and> s$2=0" in H_seq, simp)
     apply(rule_tac R="\<lambda>s. I hmin hmax s \<and> s$2=0 \<and> s$3 = s$1" in H_seq, simp)
       apply(rule_tac R="\<lambda>s. I hmin hmax s \<and> s$2=0 \<and> s$3 = s$1" in H_seq, simp)
     apply(rule H_cond, simp)
      apply(rule H_g_ode_inv, simp add: tank_diff_inv[OF assms(1)], clarsimp, clarsimp)
   using assms tank_inv_arith1 apply force
     apply(rule H_g_ode_inv, simp only: sH_diff_inv)
       apply(rule tank_diff_inv[OF assms(1)])
   using assms tank_inv_arith2 by auto
 
 \<comment> \<open>Refined with differential invariants \<close>
 
 abbreviation tank_ctrl :: "real \<Rightarrow> real \<Rightarrow> (real^4) rel" ("ctrl")
   where "ctrl hmin hmax \<equiv> ((2 ::=(\<lambda>s.0));(3 ::=(\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> hmin + 1) THEN (4 ::= (\<lambda>s.1)) ELSE 
     (IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> hmax - 1) THEN (4 ::= (\<lambda>s.0)) ELSE skip)))"
 
 abbreviation tank_dyn_dinv :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real^4) rel" ("dyn")
   where "dyn c\<^sub>i c\<^sub>o hmin hmax \<tau> \<equiv> (IF (\<lambda>s. s$4 = 0) THEN 
       (x\<acute>= (\<lambda>t. f (c\<^sub>i-c\<^sub>o)) & G hmax (c\<^sub>i-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0 DINV (dI hmin hmax (c\<^sub>i-c\<^sub>o))) 
      ELSE 
       (x\<acute>= (\<lambda>t. f (-c\<^sub>o)) & G hmin (-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0 DINV (dI hmin hmax (-c\<^sub>o))))"
 
 abbreviation "tank_dinv c\<^sub>i c\<^sub>o hmin hmax \<tau> \<equiv> 
   LOOP (ctrl hmin hmax ; dyn c\<^sub>i c\<^sub>o hmin hmax \<tau>) INV (I hmin hmax)"
 
 lemma R_tank_inv:
   assumes "0 \<le> \<tau>" and "0 < c\<^sub>o" and "c\<^sub>o < c\<^sub>i"
   shows "rel_R \<lceil>I hmin hmax\<rceil> \<lceil>I hmin hmax\<rceil> \<ge> 
   (LOOP 
     \<comment> \<open>control\<close>
     ((2 ::=(\<lambda>s.0));(3 ::=(\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> hmin + 1) THEN (4 ::= (\<lambda>s.1)) ELSE 
     (IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> hmax - 1) THEN (4 ::= (\<lambda>s.0)) ELSE skip));
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN 
       (x\<acute>= (\<lambda>t. f (c\<^sub>i-c\<^sub>o)) & G hmax (c\<^sub>i-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0 DINV (dI hmin hmax (c\<^sub>i-c\<^sub>o))) 
      ELSE 
       (x\<acute>= (\<lambda>t. f (-c\<^sub>o)) & G hmin (-c\<^sub>o) on (\<lambda>s. {0..\<tau>}) UNIV @ 0 DINV (dI hmin hmax (-c\<^sub>o)))) )
   INV I hmin hmax)"
 proof-
   have "rel_R \<lceil>I hmin hmax\<rceil> \<lceil>I hmin hmax\<rceil> \<ge> 
     LOOP (
       (2 ::= (\<lambda>s. 0)); (rel_R \<lceil>\<lambda>s. I hmin hmax s \<and> s$2 = 0\<rceil> \<lceil>I hmin hmax\<rceil>)
     ) INV I hmin hmax" (is "_ \<ge> ?R")
     by (refinement, auto)
   moreover have 
     "?R \<ge> LOOP (
       (2 ::= (\<lambda>s. 0));(3 ::=(\<lambda>s. s$1));
       (rel_R \<lceil>\<lambda>s. I hmin hmax s \<and> s$2 = 0 \<and> s$3=s$1\<rceil> \<lceil>I hmin hmax\<rceil>)
     ) INV I hmin hmax" (is "_ \<ge> ?R")
     by (refinement, auto)
   moreover have 
     "?R \<ge> LOOP (
       ctrl hmin hmax;
       (rel_R \<lceil>\<lambda>s. I hmin hmax s \<and> s$2 = 0 \<and> s$3=s$1\<rceil> \<lceil>I hmin hmax\<rceil>)
     ) INV I hmin hmax" (is "_ \<ge> ?R")
     by (simp only: O_assoc, refinement; (force)?, (rule R_assign_law)?) auto
   moreover have 
     "?R \<ge> LOOP (ctrl hmin hmax; dyn c\<^sub>i c\<^sub>o hmin hmax \<tau>) INV I hmin hmax"
     apply(simp only: O_assoc, refinement; ((rule tank_diff_inv[OF assms(1)])? | (simp)?))
     using tank_inv_arith1 tank_inv_arith2 assms by auto
   ultimately show ?thesis
     by (auto simp: O_assoc)
 qed
 
 no_notation tank_vec_field ("f")
         and tank_flow ("\<phi>")
         and tank_guard ("G")
         and tank_loop_inv ("I")
         and tank_diff_inv ("dI")
 
 end
\ No newline at end of file
diff --git a/thys/Hybrid_Systems_VCs/ModalKleeneAlgebra/HS_VC_MKA_Examples_ndfun.thy b/thys/Hybrid_Systems_VCs/ModalKleeneAlgebra/HS_VC_MKA_Examples_ndfun.thy
--- a/thys/Hybrid_Systems_VCs/ModalKleeneAlgebra/HS_VC_MKA_Examples_ndfun.thy
+++ b/thys/Hybrid_Systems_VCs/ModalKleeneAlgebra/HS_VC_MKA_Examples_ndfun.thy
@@ -1,367 +1,367 @@
 (*  Title:       Examples of hybrid systems verifications
     Author:      Jonathan Julián Huerta y Munive, 2020
     Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
 *)
 
 subsection \<open> Examples \<close>
 
 text \<open> We prove partial correctness specifications of some hybrid systems with our
 recently described verification components. Notice that this is an exact copy of
 the file @{text HS_VC_MKA_Examples}, meaning our components are truly modular and
 we can choose either a relational or predicate transformer semantics.\<close>
 
 theory HS_VC_MKA_Examples_ndfun
   imports HS_VC_MKA_ndfun
 
 begin
 
 
 subsubsection\<open>Pendulum\<close>
 
 text \<open> The ODEs @{text "x' t = y t"} and {text "y' t = - x t"} describe the circular motion of
 a mass attached to a string looked from above. We use @{text "s$1"} to represent the x-coordinate
 and @{text "s$2"} for the y-coordinate. We prove that this motion remains circular. \<close>
 
 abbreviation fpend :: "real^2 \<Rightarrow> real^2" ("f")
   where "f s \<equiv> (\<chi> i. if i = 1 then s$2 else -s$1)"
 
 abbreviation pend_flow :: "real \<Rightarrow> real^2 \<Rightarrow> real^2" ("\<phi>")
   where "\<phi> t s \<equiv> (\<chi> i. if i = 1 then s$1 * cos t + s$2 * sin t
   else - s$1 * sin t + s$2 * cos t)"
 
 \<comment> \<open>Verified by providing dynamics. \<close>
 
 lemma pendulum_dyn:
   "\<lceil>\<lambda>s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2\<rceil> \<le> wp (EVOL \<phi> G T) \<lceil>\<lambda>s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2\<rceil>"
   by simp
 
 \<comment> \<open>Verified with differential invariants. \<close>
 
 lemma pendulum_inv:
   "\<lceil>\<lambda>s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2\<rceil> \<le> wp (x\<acute>= f & G) \<lceil>\<lambda>s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2\<rceil>"
   by (auto intro!: poly_derivatives diff_invariant_rules)
 
 \<comment> \<open>Verified with the flow. \<close>
 
 lemma local_flow_pend: "local_flow f UNIV UNIV \<phi>"
   apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def vec_eq_iff, clarsimp)
     apply(rule_tac x="1" in exI, clarsimp, rule_tac x=1 in exI)
     apply(simp add: dist_norm norm_vec_def L2_set_def power2_commute UNIV_2)
   by (auto simp: forall_2 intro!: poly_derivatives)
 
 lemma pendulum_flow:
   "\<lceil>\<lambda>s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2\<rceil> \<le> wp (x\<acute>= f & G) \<lceil>\<lambda>s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2\<rceil>"
   by (simp add: local_flow.wp_g_ode_subset[OF local_flow_pend])
 
 no_notation fpend ("f")
         and pend_flow ("\<phi>")
 
 
 subsubsection\<open> Bouncing Ball \<close>
 
 text \<open> A ball is dropped from rest at an initial height @{text "h"}. The motion is described with
 the free-fall equations @{text "x' t = v t"} and @{text "v' t = g"} where @{text "g"} is the
 constant acceleration due to gravity. The bounce is modelled with a variable assignment that
 flips the velocity. That is, we model it as a completely elastic collision with the ground. We use 
 @{text "s$1"} to represent the ball's height and @{text "s$2"} for its velocity. We prove that the 
 ball remains above ground and below its initial resting position. \<close>
 
 abbreviation fball :: "real \<Rightarrow> real^2 \<Rightarrow> real^2" ("f")
   where "f g s \<equiv> (\<chi> i. if i = 1 then s$2 else g)"
 
 abbreviation ball_flow :: "real \<Rightarrow> real \<Rightarrow> real^2 \<Rightarrow> real^2" ("\<phi>")
   where "\<phi> g t s \<equiv> (\<chi> i. if i = 1 then g * t ^ 2/2 + s$2 * t + s$1 else g * t + s$2)"
 
 \<comment> \<open>Verified with differential invariants. \<close>
 
 named_theorems bb_real_arith "real arithmetic properties for the bouncing ball."
 
 lemma inv_imp_pos_le[bb_real_arith]:
   assumes "0 > g" and inv: "2 * g * x - 2 * g * h = v * v"
   shows "(x::real) \<le> h"
 proof-
   have "v * v = 2 * g * x - 2 * g * h \<and> 0 > g"
     using inv and \<open>0 > g\<close> by auto
   hence obs:"v * v = 2 * g * (x - h) \<and> 0 > g \<and> v * v \<ge> 0"
     using left_diff_distrib mult.commute by (metis zero_le_square)
   hence "(v * v)/(2 * g) = (x - h)"
     by auto
   also from obs have "(v * v)/(2 * g) \<le> 0"
     using divide_nonneg_neg by fastforce
   ultimately have "h - x \<ge> 0"
     by linarith
   thus ?thesis by auto
 qed
 
 lemma bouncing_ball_inv:
   fixes h::real
   shows "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow> \<lceil>\<lambda>s. s$1 = h \<and> s$2 = 0\<rceil> \<le>
   wp
     (LOOP
       ((x\<acute>= f g & (\<lambda> s. s$1 \<ge> 0) DINV (\<lambda>s. 2 * g * s$1 - 2 * g * h - s$2 * s$2 = 0));
        (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip))
     INV (\<lambda>s. 0 \<le> s$1 \<and> 2 * g * s$1 - 2 * g * h - s$2 * s$2 = 0)
   ) \<lceil>\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h\<rceil>"
   apply(rule wp_loopI, simp_all, force simp: bb_real_arith)
   by (rule wp_g_odei) (auto intro!: poly_derivatives diff_invariant_rules)
 
 \<comment> \<open>Verified with annotated dynamics. \<close>
 
 lemma inv_conserv_at_ground[bb_real_arith]:
   assumes invar: "2 * g * x = 2 * g * h + v * v"
     and pos: "g * \<tau>\<^sup>2 / 2 + v * \<tau> + (x::real) = 0"
   shows "2 * g * h + (g * \<tau> * (g * \<tau> + v) + v * (g * \<tau> + v)) = 0"
 proof-
   from pos have "g * \<tau>\<^sup>2  + 2 * v * \<tau> + 2 * x = 0" by auto
   then have "g\<^sup>2 * \<tau>\<^sup>2  + 2 * g * v * \<tau> + 2 * g * x = 0"
-    by (metis (mono_tags, opaque_lifting) Groups.mult_ac(1,3) mult_zero_right
+    by (metis (mono_tags) Groups.mult_ac(1,3) mult_zero_right
         monoid_mult_class.power2_eq_square semiring_class.distrib_left)
   hence "g\<^sup>2 * \<tau>\<^sup>2 + 2 * g * v * \<tau> + v\<^sup>2 + 2 * g * h = 0"
     using invar by (simp add: monoid_mult_class.power2_eq_square)
   hence obs: "(g * \<tau> + v)\<^sup>2 + 2 * g * h = 0"
-    apply(subst power2_sum) by (metis (no_types, opaque_lifting) Groups.add_ac(2, 3)
+    apply(subst power2_sum) by (metis (no_types) Groups.add_ac(2, 3)
         Groups.mult_ac(2, 3) monoid_mult_class.power2_eq_square nat_distrib(2))
   thus "2 * g * h + (g * \<tau> * (g * \<tau> + v) + v * (g * \<tau> + v)) = 0"
     by (simp add: monoid_mult_class.power2_eq_square)
 qed
 
 lemma inv_conserv_at_air[bb_real_arith]:
   assumes invar: "2 * g * x = 2 * g * h + v * v"
   shows "2 * g * (g * \<tau>\<^sup>2 / 2 + v * \<tau> + (x::real)) =
   2 * g * h + (g * \<tau> * (g * \<tau> + v) + v * (g * \<tau> + v))" (is "?lhs = ?rhs")
 proof-
   have "?lhs = g\<^sup>2 * \<tau>\<^sup>2 + 2 * g * v * \<tau> + 2 * g * x"
     by(auto simp: algebra_simps semiring_normalization_rules(29))
   also have "... = g\<^sup>2 * \<tau>\<^sup>2 + 2 * g * v * \<tau> + 2 * g * h + v * v" (is "... = ?middle")
     by(subst invar, simp)
   finally have "?lhs = ?middle".
   moreover
   {have "?rhs = g * g * (\<tau> * \<tau>) + 2 * g * v * \<tau> + 2 * g * h + v * v"
     by (simp add: Groups.mult_ac(2,3) semiring_class.distrib_left)
   also have "... = ?middle"
     by (simp add: semiring_normalization_rules(29))
   finally have "?rhs = ?middle".}
   ultimately show ?thesis by auto
 qed
 
 lemma bouncing_ball_dyn:
   fixes h::real
   assumes "g < 0" and "h \<ge> 0"
   shows "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow>
   \<lceil>\<lambda>s. s$1 = h \<and> s$2 = 0\<rceil> \<le> wp
     (LOOP
       ((EVOL (\<phi> g) (\<lambda>s. 0 \<le> s$1) T);
       (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip))
     INV (\<lambda>s. 0 \<le> s$1 \<and> 2 * g * s$1 = 2 * g * h + s$2 * s$2))
   \<lceil>\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h\<rceil>"
   by (rule wp_loopI) (auto simp: bb_real_arith)
 
 \<comment> \<open>Verified with the flow. \<close>
 
 lemma local_flow_ball: "local_flow (f g) UNIV UNIV (\<phi> g)"
   apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def vec_eq_iff, clarsimp)
     apply(rule_tac x="1/2" in exI, clarsimp, rule_tac x=1 in exI)
     apply(simp add: dist_norm norm_vec_def L2_set_def UNIV_2)
   by (auto simp: forall_2 intro!: poly_derivatives)
 
 lemma bouncing_ball_flow:
   fixes h::real
   assumes "g < 0" and "h \<ge> 0"
   shows "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow>
   \<lceil>\<lambda>s. s$1 = h \<and> s$2 = 0\<rceil> \<le> wp
     (LOOP
       ((x\<acute>= (\<lambda>t. f g) & (\<lambda> s. s$1 \<ge> 0) on (\<lambda>s. UNIV) UNIV @ 0);
       (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip))
     INV (\<lambda>s. 0 \<le> s$1 \<and> 2 * g * s$1 = 2 * g * h + s$2 * s$2))
   \<lceil>\<lambda>s. 0 \<le> s$1 \<and> s$1 \<le> h\<rceil>"
   apply(rule wp_loopI, simp_all add: local_flow.wp_g_ode_subset[OF local_flow_ball])
   by (auto simp: bb_real_arith)
 
 no_notation fball ("f")
         and ball_flow ("\<phi>")
 
 
 subsubsection\<open> Thermostat \<close>
 
 text \<open> A thermostat has a chronometer, a thermometer and a switch to turn on and off a heater.
 At most every @{text "t"} minutes, it sets its chronometer to @{term "0::real"}, it registers
 the room temperature, and it turns the heater on (or off) based on this reading. The temperature
 follows the ODE @{text "T' = - a * (T - U)"} where @{text "U"} is @{text "L \<ge> 0"} when the heater
 is on, and @{text "0"} when it is off. We use @{term "1::4"} to denote the room's temperature,
 @{term "2::4"} is time as measured by the thermostat's chronometer, @{term "3::4"} is the
 temperature detected by the thermometer, and @{term "4::4"} states whether the heater is on
 (@{text "s$4 = 1"}) or off (@{text "s$4 = 0"}). We prove that the thermostat keeps the room's
 temperature between @{text "Tmin"} and @{text "Tmax"}. \<close>
 
 abbreviation temp_vec_field :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> real^4" ("f")
   where "f a L s \<equiv> (\<chi> i. if i = 2 then 1 else (if i = 1 then - a * (s$1 - L) else 0))"
 
 abbreviation temp_flow :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> real^4" ("\<phi>")
   where "\<phi> a L t s \<equiv> (\<chi> i. if i = 1 then - exp(-a * t) * (L - s$1) + L else
   (if i = 2 then t + s$2 else s$i))"
 
 \<comment> \<open>Verified with the flow. \<close>
 
 lemma norm_diff_temp_dyn: "0 < a \<Longrightarrow> \<parallel>f a L s\<^sub>1 - f a L s\<^sub>2\<parallel> = \<bar>a\<bar> * \<bar>s\<^sub>1$1 - s\<^sub>2$1\<bar>"
 proof(simp add: norm_vec_def L2_set_def, unfold UNIV_4, simp)
   assume a1: "0 < a"
   have f2: "\<And>r ra. \<bar>(r::real) + - ra\<bar> = \<bar>ra + - r\<bar>"
     by (metis abs_minus_commute minus_real_def)
   have "\<And>r ra rb. (r::real) * ra + - (r * rb) = r * (ra + - rb)"
     by (metis minus_real_def right_diff_distrib)
   hence "\<bar>a * (s\<^sub>1$1 + - L) + - (a * (s\<^sub>2$1 + - L))\<bar> = a * \<bar>s\<^sub>1$1 + - s\<^sub>2$1\<bar>"
     using a1 by (simp add: abs_mult)
   thus "\<bar>a * (s\<^sub>2$1 - L) - a * (s\<^sub>1$1 - L)\<bar> = a * \<bar>s\<^sub>1$1 - s\<^sub>2$1\<bar>"
     using f2 minus_real_def by presburger
 qed
 
 lemma local_lipschitz_temp_dyn:
   assumes "0 < (a::real)"
   shows "local_lipschitz UNIV UNIV (\<lambda>t::real. f a L)"
   apply(unfold local_lipschitz_def lipschitz_on_def dist_norm)
   apply(clarsimp, rule_tac x=1 in exI, clarsimp, rule_tac x=a in exI)
   using assms
   apply(simp_all add: norm_diff_temp_dyn)
   apply(simp add: norm_vec_def L2_set_def, unfold UNIV_4, clarsimp)
   unfolding real_sqrt_abs[symmetric] by (rule real_le_lsqrt) auto
 
 lemma local_flow_temp: "a > 0 \<Longrightarrow> local_flow (f a L) UNIV UNIV (\<phi> a L)"
   by (unfold_locales, auto intro!: poly_derivatives local_lipschitz_temp_dyn simp: forall_4 vec_eq_iff)
 
 lemma temp_dyn_down_real_arith:
   assumes "a > 0" and Thyps: "0 < Tmin" "Tmin \<le> T" "T \<le> Tmax"
     and thyps: "0 \<le> (t::real)" "\<forall>\<tau>\<in>{0..t}. \<tau> \<le> - (ln (Tmin / T) / a) "
   shows "Tmin \<le> exp (-a * t) * T" and "exp (-a * t) * T \<le> Tmax"
 proof-
   have "0 \<le> t \<and> t \<le> - (ln (Tmin / T) / a)"
     using thyps by auto
   hence "ln (Tmin / T) \<le> - a * t \<and> - a * t \<le> 0"
     using assms(1) divide_le_cancel by fastforce
   also have "Tmin / T > 0"
     using Thyps by auto
   ultimately have obs: "Tmin / T \<le> exp (-a * t)" "exp (-a * t) \<le> 1"
     using exp_ln exp_le_one_iff by (metis exp_less_cancel_iff not_less, simp)
   thus "Tmin \<le> exp (-a * t) * T"
     using Thyps by (simp add: pos_divide_le_eq)
   show "exp (-a * t) * T \<le> Tmax"
     using Thyps mult_left_le_one_le[OF _ exp_ge_zero obs(2), of T]
       less_eq_real_def order_trans_rules(23) by blast
 qed
 
 lemma temp_dyn_up_real_arith:
   assumes "a > 0" and Thyps: "Tmin \<le> T" "T \<le> Tmax" "Tmax < (L::real)"
     and thyps: "0 \<le> t" "\<forall>\<tau>\<in>{0..t}. \<tau> \<le> - (ln ((L - Tmax) / (L - T)) / a) "
   shows "L - Tmax \<le> exp (-(a * t)) * (L - T)"
     and "L - exp (-(a * t)) * (L - T) \<le> Tmax"
     and "Tmin \<le> L - exp (-(a * t)) * (L - T)"
 proof-
   have "0 \<le> t \<and> t \<le> - (ln ((L - Tmax) / (L - T)) / a)"
     using thyps by auto
   hence "ln ((L - Tmax) / (L - T)) \<le> - a * t \<and> - a * t \<le> 0"
     using assms(1) divide_le_cancel by fastforce
   also have "(L - Tmax) / (L - T) > 0"
     using Thyps by auto
   ultimately have "(L - Tmax) / (L - T) \<le> exp (-a * t) \<and> exp (-a * t) \<le> 1"
     using exp_ln exp_le_one_iff by (metis exp_less_cancel_iff not_less)
   moreover have "L - T > 0"
     using Thyps by auto
   ultimately have obs: "(L - Tmax) \<le> exp (-a * t) * (L - T) \<and> exp (-a * t) * (L - T) \<le> (L - T)"
     by (simp add: pos_divide_le_eq)
   thus "(L - Tmax) \<le> exp (-(a * t)) * (L - T)"
     by auto
   thus "L - exp (-(a * t)) * (L - T) \<le> Tmax"
     by auto
   show "Tmin \<le> L - exp (-(a * t)) * (L - T)"
     using Thyps and obs by auto
 qed
 
 lemmas fbox_temp_dyn = local_flow.wp_g_ode_subset[OF local_flow_temp]
 
 lemma thermostat:
   assumes "a > 0" and "0 < Tmin" and "Tmax < L"
   shows "\<lceil>\<lambda>s. Tmin \<le> s$1 \<and> s$1 \<le> Tmax \<and> s$4 = 0\<rceil> \<le> wp
   (LOOP
     \<comment> \<open>control\<close>
     ((2 ::= (\<lambda>s. 0));(3 ::= (\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> Tmin + 1) THEN (4 ::= (\<lambda>s.1)) ELSE
     (IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> Tmax - 1) THEN (4 ::= (\<lambda>s.0)) ELSE skip));
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN (x\<acute>= f a 0 & (\<lambda>s. s$2 \<le> - (ln (Tmin/s$3))/a))
     ELSE (x\<acute>= f a L & (\<lambda>s. s$2 \<le> - (ln ((L-Tmax)/(L-s$3)))/a))) )
   INV (\<lambda>s. Tmin \<le>s$1 \<and> s$1 \<le> Tmax \<and> (s$4 = 0 \<or> s$4 = 1)))
   \<lceil>\<lambda>s. Tmin \<le> s$1 \<and> s$1 \<le> Tmax\<rceil>"
   apply(rule wp_loopI, simp_all add: fbox_temp_dyn[OF assms(1)])
   using temp_dyn_up_real_arith[OF assms(1) _ _ assms(3), of Tmin]
     and temp_dyn_down_real_arith[OF assms(1,2), of _ Tmax] by auto
 
 no_notation temp_vec_field ("f")
         and temp_flow ("\<phi>")
 
 subsubsection \<open> Tank \<close>
 
 text \<open> A controller turns a water pump on and off to keep the level of water @{text "h"} in a tank
 within an acceptable range @{text "hmin \<le> h \<le> hmax"}. Just like in the previous example, after 
 each intervention, the controller registers the current level of water and resets its chronometer,
 then it changes the status of the water pump accordingly. The level of water grows linearly 
 @{text "h' = k"} at a rate of @{text "k = c\<^sub>i-c\<^sub>o"} if the pump is on, and at a rate of 
 @{text "k = -c\<^sub>o"} if the pump is off. We use @{term "1::4"} to denote the tank's level of water,
 @{term "2::4"} is time as measured by the controller's chronometer, @{term "3::4"} is the
 level of water measured by the chronometer, and @{term "4::4"} states whether the pump is on
 (@{text "s$4 = 1"}) or off (@{text "s$4 = 0"}). We prove that the controller keeps the level of
 water between @{text "hmin"} and @{text "hmax"}. \<close>
 
 abbreviation tank_vec_field :: "real \<Rightarrow> real^4 \<Rightarrow> real^4" ("f")
   where "f k s \<equiv> (\<chi> i. if i = 2 then 1 else (if i = 1 then k else 0))"
 
 abbreviation tank_flow :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> real^4" ("\<phi>")
   where "\<phi> k \<tau> s \<equiv> (\<chi> i. if i = 1 then k * \<tau> + s$1 else 
   (if i = 2 then \<tau> + s$2 else s$i))"
 
 abbreviation tank_guard :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("G")
   where "G Hm k s \<equiv> s$2 \<le> (Hm - s$3)/k"
 
 abbreviation tank_loop_inv :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("I")
   where "I hmin hmax s \<equiv> hmin \<le> s$1 \<and> s$1 \<le> hmax \<and> (s$4 = 0 \<or> s$4 = 1)"
 
 abbreviation tank_diff_inv :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("dI")
   where "dI hmin hmax k s \<equiv> s$1 = k * s$2 + s$3 \<and> 0 \<le> s$2 \<and> 
     hmin \<le> s$3 \<and> s$3 \<le> hmax \<and> (s$4 =0 \<or> s$4 = 1)"
 
 lemma local_flow_tank: "local_flow (f k) UNIV UNIV (\<phi> k)"
   apply (unfold_locales, unfold local_lipschitz_def lipschitz_on_def, simp_all, clarsimp)
   apply(rule_tac x="1/2" in exI, clarsimp, rule_tac x=1 in exI)
   apply(simp add: dist_norm norm_vec_def L2_set_def, unfold UNIV_4)
   by (auto intro!: poly_derivatives simp: vec_eq_iff)
 
 lemma tank_arith:
   assumes "0 \<le> (\<tau>::real)" and "0 < c\<^sub>o" and "c\<^sub>o < c\<^sub>i"
   shows "\<forall>\<tau>\<in>{0..\<tau>}. \<tau> \<le> - ((hmin - y) / c\<^sub>o) \<Longrightarrow>  hmin \<le> y - c\<^sub>o * \<tau>"
     and "\<forall>\<tau>\<in>{0..\<tau>}. \<tau> \<le> (hmax - y) / (c\<^sub>i - c\<^sub>o) \<Longrightarrow>  (c\<^sub>i - c\<^sub>o) * \<tau> + y \<le> hmax"
     and "hmin \<le> y \<Longrightarrow> hmin \<le> (c\<^sub>i - c\<^sub>o) * \<tau> + y"
     and "y \<le> hmax \<Longrightarrow> y - c\<^sub>o * \<tau> \<le> hmax"
   apply(simp_all add: field_simps le_divide_eq assms)
   using assms apply (meson add_mono less_eq_real_def mult_left_mono)
   using assms by (meson add_increasing2 less_eq_real_def mult_nonneg_nonneg) 
 
 lemma tank_flow:
   assumes "0 < c\<^sub>o" and "c\<^sub>o < c\<^sub>i"
   shows "\<lceil>\<lambda>s. I hmin hmax s\<rceil> \<le> wp
   (LOOP 
     \<comment> \<open>control\<close>
     ((2 ::=(\<lambda>s.0));(3 ::=(\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> hmin + 1) THEN (4 ::= (\<lambda>s.1)) ELSE 
     (IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> hmax - 1) THEN (4 ::= (\<lambda>s.0)) ELSE skip));
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN (x\<acute>= f (c\<^sub>i-c\<^sub>o) & (G hmax (c\<^sub>i-c\<^sub>o))) 
      ELSE (x\<acute>= f (-c\<^sub>o) & (G hmin (-c\<^sub>o)))) ) INV I hmin hmax) 
   \<lceil>\<lambda>s. I hmin hmax s\<rceil>"
   apply(rule wp_loopI, simp_all add: local_flow.wp_g_ode_subset[OF local_flow_tank])
   using assms tank_arith[OF _ assms] by auto
 
 no_notation tank_vec_field ("f")
         and tank_flow ("\<phi>")
         and tank_loop_inv ("I")
         and tank_diff_inv ("dI")
         and tank_guard ("G")
 
 end
\ No newline at end of file
diff --git a/thys/Hybrid_Systems_VCs/PredicateTransformers/HS_VC_PT_Examples.thy b/thys/Hybrid_Systems_VCs/PredicateTransformers/HS_VC_PT_Examples.thy
--- a/thys/Hybrid_Systems_VCs/PredicateTransformers/HS_VC_PT_Examples.thy
+++ b/thys/Hybrid_Systems_VCs/PredicateTransformers/HS_VC_PT_Examples.thy
@@ -1,355 +1,355 @@
 (*  Title:       Examples of hybrid systems verifications
     Author:      Jonathan Julián Huerta y Munive, 2020
     Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
 *)
 
 subsection \<open> Examples \<close>
 
 text \<open> We prove partial correctness specifications of some hybrid systems with our
 recently described verification components.\<close>
 
 theory HS_VC_PT_Examples
   imports HS_VC_PT
 
 begin
 
 
 subsubsection \<open> Pendulum \<close>
 
 text \<open> The ODEs @{text "x' t = y t"} and {text "y' t = - x t"} describe the circular motion of
 a mass attached to a string looked from above. We use @{text "s$1"} to represent the x-coordinate
 and @{text "s$2"} for the y-coordinate. We prove that this motion remains circular. \<close>
 
 abbreviation fpend :: "real^2 \<Rightarrow> real^2" ("f")
   where "f s \<equiv> (\<chi> i. if i = 1 then s$2 else -s$1)"
 
 abbreviation pend_flow :: "real \<Rightarrow> real^2 \<Rightarrow> real^2" ("\<phi>")
   where "\<phi> t s \<equiv> (\<chi> i. if i = 1 then s$1 * cos t + s$2 * sin t else - s$1 * sin t + s$2 * cos t)"
 
 \<comment> \<open>Verified by providing the dynamics\<close>
 
 lemma pendulum_dyn: "{s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2} \<le> fb\<^sub>\<F> (EVOL \<phi> G T) {s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2}"
   by force
 
 \<comment> \<open>Verified with differential invariants. \<close>
 
 lemma pendulum_inv: "{s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2} \<le> fb\<^sub>\<F> (x\<acute>= f & G) {s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2}"
   by (auto intro!: diff_invariant_rules poly_derivatives)
 
 \<comment> \<open>Verified with the flow. \<close>
 
 lemma local_flow_pend: "local_flow f UNIV UNIV \<phi>"
   apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def vec_eq_iff, clarsimp)
     apply(rule_tac x="1" in exI, clarsimp, rule_tac x=1 in exI)
     apply(simp add: dist_norm norm_vec_def L2_set_def power2_commute UNIV_2)
   by (auto simp: forall_2 intro!: poly_derivatives)
 
 lemma pendulum_flow: "{s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2} \<le> fb\<^sub>\<F> (x\<acute>= f & G) {s. r\<^sup>2 = (s$1)\<^sup>2 + (s$2)\<^sup>2}"
   by (force simp: local_flow.ffb_g_ode_subset[OF local_flow_pend])
 
 no_notation fpend ("f")
         and pend_flow ("\<phi>")
 
 
 subsubsection \<open> Bouncing Ball \<close>
 
 text \<open> A ball is dropped from rest at an initial height @{text "h"}. The motion is described with
 the free-fall equations @{text "x' t = v t"} and @{text "v' t = g"} where @{text "g"} is the
 constant acceleration due to gravity. The bounce is modelled with a variable assignment that
 flips the velocity. That is, we model it as a completely elastic collision with the ground. We use 
 @{text "s$1"} to represent the ball's height and @{text "s$2"} for its velocity. We prove that the 
 ball remains above ground and below its initial resting position. \<close>
 
 abbreviation fball :: "real \<Rightarrow> real^2 \<Rightarrow> real^2" ("f")
   where "f g s \<equiv> (\<chi> i. if i = 1 then s$2 else g)"
 
 abbreviation ball_flow :: "real \<Rightarrow> real \<Rightarrow> real^2 \<Rightarrow> real^2" ("\<phi>")
   where "\<phi> g t s \<equiv> (\<chi> i. if i = 1 then g * t ^ 2/2 + s$2 * t + s$1 else g * t + s$2)"
 
 \<comment> \<open>Verified with differential invariants. \<close>
 
 named_theorems bb_real_arith "real arithmetic properties for the bouncing ball."
 
 lemma inv_imp_pos_le[bb_real_arith]:
   assumes "0 > g" and inv: "2 * g * x - 2 * g * h = v * v"
   shows "(x::real) \<le> h"
 proof-
   have "v * v = 2 * g * x - 2 * g * h \<and> 0 > g"
     using inv and \<open>0 > g\<close> by auto
   hence obs:"v * v = 2 * g * (x - h) \<and> 0 > g \<and> v * v \<ge> 0"
     using left_diff_distrib mult.commute by (metis zero_le_square)
   hence "(v * v)/(2 * g) = (x - h)"
     by auto
   also from obs have "(v * v)/(2 * g) \<le> 0"
     using divide_nonneg_neg by fastforce
   ultimately have "h - x \<ge> 0"
     by linarith
   thus ?thesis by auto
 qed
 
 lemma bouncing_ball_inv: "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow>
   {s. s$1 = h \<and> s$2 = 0} \<le> fb\<^sub>\<F>
   (LOOP (
     (x\<acute>=(f g) & (\<lambda> s. s$1 \<ge> 0) DINV (\<lambda>s. 2 * g * s$1 - 2 * g * h - s$2 * s$2 = 0)) ;
     (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip))
   INV (\<lambda>s. 0 \<le> s$1 \<and>2 * g * s$1 - 2 * g * h - s$2 * s$2 = 0))
   {s. 0 \<le> s$1 \<and> s$1 \<le> h}"
   apply(rule ffb_loopI, simp_all)
     apply(force, force simp: bb_real_arith)
   apply(rule ffb_g_odei)
   by (auto intro!: diff_invariant_rules poly_derivatives simp: bb_real_arith)
 
 \<comment> \<open>Verified with annotated dynamics. \<close>
 
 lemma inv_conserv_at_ground[bb_real_arith]:
   assumes invar: "2 * g * x = 2 * g * h + v * v"
     and pos: "g * \<tau>\<^sup>2 / 2 + v * \<tau> + (x::real) = 0"
   shows "2 * g * h + (g * \<tau> * (g * \<tau> + v) + v * (g * \<tau> + v)) = 0"
 proof-
   from pos have "g * \<tau>\<^sup>2  + 2 * v * \<tau> + 2 * x = 0" by auto
   then have "g\<^sup>2 * \<tau>\<^sup>2  + 2 * g * v * \<tau> + 2 * g * x = 0"
-    by (metis (mono_tags, opaque_lifting) Groups.mult_ac(1,3) mult_zero_right
+    by (metis (mono_tags) Groups.mult_ac(1,3) mult_zero_right
         monoid_mult_class.power2_eq_square semiring_class.distrib_left)
   hence "g\<^sup>2 * \<tau>\<^sup>2 + 2 * g * v * \<tau> + v\<^sup>2 + 2 * g * h = 0"
     using invar by (simp add: monoid_mult_class.power2_eq_square)
   hence obs: "(g * \<tau> + v)\<^sup>2 + 2 * g * h = 0"
-    apply(subst power2_sum) by (metis (no_types, opaque_lifting) Groups.add_ac(2, 3)
+    apply(subst power2_sum) by (metis (no_types) Groups.add_ac(2, 3)
         Groups.mult_ac(2, 3) monoid_mult_class.power2_eq_square nat_distrib(2))
   thus "2 * g * h + (g * \<tau> * (g * \<tau> + v) + v * (g * \<tau> + v)) = 0"
     by (simp add: add.commute distrib_right power2_eq_square)
 qed
 
 lemma inv_conserv_at_air[bb_real_arith]:
   assumes invar: "2 * g * x = 2 * g * h + v * v"
   shows "2 * g * (g * \<tau>\<^sup>2 / 2 + v * \<tau> + (x::real)) =
   2 * g * h + (g * \<tau> + v) * (g * \<tau> + v)" (is "?lhs = ?rhs")
 proof-
   have "?lhs = g\<^sup>2 * \<tau>\<^sup>2 + 2 * g * v * \<tau> + 2 * g * x"
     by(auto simp: algebra_simps semiring_normalization_rules(29))
   also have "... = g\<^sup>2 * \<tau>\<^sup>2 + 2 * g * v * \<tau> + 2 * g * h + v * v" (is "... = ?middle")
     by(subst invar, simp)
   finally have "?lhs = ?middle".
   moreover
   {have "?rhs = g * g * (\<tau> * \<tau>) + 2 * g * v * \<tau> + 2 * g * h + v * v"
     by (simp add: Groups.mult_ac(2,3) semiring_class.distrib_left)
   also have "... = ?middle"
     by (simp add: semiring_normalization_rules(29))
   finally have "?rhs = ?middle".}
   ultimately show ?thesis by auto
 qed
 
 lemma bouncing_ball_dyn: "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow>
   {s. s$1 = h \<and> s$2 = 0} \<le> fb\<^sub>\<F>
   (LOOP (
     (EVOL (\<phi> g) (\<lambda> s. s$1 \<ge> 0) T) ;
     (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip))
   INV (\<lambda>s. 0 \<le> s$1 \<and> 2 * g * s$1 = 2 * g * h + s$2 * s$2))
   {s. 0 \<le> s$1 \<and> s$1 \<le> h}"
   by (rule ffb_loopI) (auto simp: bb_real_arith)
 
 \<comment> \<open>Verified with the flow. \<close>
 
 lemma local_flow_ball: "local_flow (f g) UNIV UNIV (\<phi> g)"
   apply(unfold_locales, simp_all add: local_lipschitz_def lipschitz_on_def vec_eq_iff, clarsimp)
     apply(rule_tac x="1/2" in exI, clarsimp, rule_tac x=1 in exI)
     apply(simp add: dist_norm norm_vec_def L2_set_def UNIV_2)
   by (auto simp: forall_2 intro!: poly_derivatives)
 
 lemma bouncing_ball_flow: "g < 0 \<Longrightarrow> h \<ge> 0 \<Longrightarrow>
   {s. s$1 = h \<and> s$2 = 0} \<le> fb\<^sub>\<F>
   (LOOP (
     (x\<acute>=(\<lambda>t. f g) & (\<lambda> s. s$1 \<ge> 0) on (\<lambda>s. UNIV) UNIV @ 0) ;
     (IF (\<lambda> s. s$1 = 0) THEN (2 ::= (\<lambda>s. - s$2)) ELSE skip))
   INV (\<lambda>s. 0 \<le> s$1 \<and> 2 * g * s$1 = 2 * g * h + s$2 * s$2))
   {s. 0 \<le> s$1 \<and> s$1 \<le> h}"
   by (rule ffb_loopI) (auto simp: bb_real_arith local_flow.ffb_g_ode[OF local_flow_ball])
 
 no_notation fball ("f")
         and ball_flow ("\<phi>")
 
 
 subsubsection \<open> Thermostat \<close>
 
 text \<open> A thermostat has a chronometer, a thermometer and a switch to turn on and off a heater.
 At most every @{text "t"} minutes, it sets its chronometer to @{term "0::real"}, it registers
 the room temperature, and it turns the heater on (or off) based on this reading. The temperature
 follows the ODE @{text "T' = - a * (T - U)"} where @{text "U"} is @{text "L \<ge> 0"} when the heater
 is on, and @{text "0"} when it is off. We use @{term "1::4"} to denote the room's temperature,
 @{term "2::4"} is time as measured by the thermostat's chronometer, @{term "3::4"} is the
 temperature detected by the thermometer, and @{term "4::4"} states whether the heater is on
 (@{text "s$4 = 1"}) or off (@{text "s$4 = 0"}). We prove that the thermostat keeps the room's
 temperature between @{text "Tmin"} and @{text "Tmax"}. \<close>
 
 abbreviation temp_vec_field :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> real^4" ("f")
   where "f a L s \<equiv> (\<chi> i. if i = 2 then 1 else (if i = 1 then - a * (s$1 - L) else 0))"
 
 abbreviation temp_flow :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> real^4" ("\<phi>")
   where "\<phi> a L t s \<equiv> (\<chi> i. if i = 1 then - exp(-a * t) * (L - s$1) + L else
   (if i = 2 then t + s$2 else s$i))"
 
 \<comment> \<open>Verified with the flow. \<close>
 
 lemma norm_diff_temp_dyn: "0 < a \<Longrightarrow> \<parallel>f a L s\<^sub>1 - f a L s\<^sub>2\<parallel> = \<bar>a\<bar> * \<bar>s\<^sub>1$1 - s\<^sub>2$1\<bar>"
 proof(simp add: norm_vec_def L2_set_def, unfold UNIV_4, simp)
   assume a1: "0 < a"
   have f2: "\<And>r ra. \<bar>(r::real) + - ra\<bar> = \<bar>ra + - r\<bar>"
     by (metis abs_minus_commute minus_real_def)
   have "\<And>r ra rb. (r::real) * ra + - (r * rb) = r * (ra + - rb)"
     by (metis minus_real_def right_diff_distrib)
   hence "\<bar>a * (s\<^sub>1$1 + - L) + - (a * (s\<^sub>2$1 + - L))\<bar> = a * \<bar>s\<^sub>1$1 + - s\<^sub>2$1\<bar>"
     using a1 by (simp add: abs_mult)
   thus "\<bar>a * (s\<^sub>2$1 - L) - a * (s\<^sub>1$1 - L)\<bar> = a * \<bar>s\<^sub>1$1 - s\<^sub>2$1\<bar>"
     using f2 minus_real_def by presburger
 qed
 
 lemma local_lipschitz_temp_dyn:
   assumes "0 < (a::real)"
   shows "local_lipschitz UNIV UNIV (\<lambda>t::real. f a L)"
   apply(unfold local_lipschitz_def lipschitz_on_def dist_norm)
   apply(clarsimp, rule_tac x=1 in exI, clarsimp, rule_tac x=a in exI)
   using assms
   apply(simp_all add: norm_diff_temp_dyn)
   apply(simp add: norm_vec_def L2_set_def, unfold UNIV_4, clarsimp)
   unfolding real_sqrt_abs[symmetric] by (rule real_le_lsqrt) auto
 
 lemma local_flow_temp: "a > 0 \<Longrightarrow> local_flow (f a L) UNIV UNIV (\<phi> a L)"
   by (unfold_locales, auto intro!: poly_derivatives local_lipschitz_temp_dyn simp: forall_4 vec_eq_iff)
 
 lemma temp_dyn_down_real_arith:
   assumes "a > 0" and Thyps: "0 < Tmin" "Tmin \<le> T" "T \<le> Tmax"
     and thyps: "0 \<le> (t::real)" "\<forall>\<tau>\<in>{0..t}. \<tau> \<le> - (ln (Tmin / T) / a) "
   shows "Tmin \<le> exp (-a * t) * T" and "exp (-a * t) * T \<le> Tmax"
 proof-
   have "0 \<le> t \<and> t \<le> - (ln (Tmin / T) / a)"
     using thyps by auto
   hence "ln (Tmin / T) \<le> - a * t \<and> - a * t \<le> 0"
     using assms(1) divide_le_cancel by fastforce
   also have "Tmin / T > 0"
     using Thyps by auto
   ultimately have obs: "Tmin / T \<le> exp (-a * t)" "exp (-a * t) \<le> 1"
     using exp_ln exp_le_one_iff by (metis exp_less_cancel_iff not_less, simp)
   thus "Tmin \<le> exp (-a * t) * T"
     using Thyps by (simp add: pos_divide_le_eq)
   show "exp (-a * t) * T \<le> Tmax"
     using Thyps mult_left_le_one_le[OF _ exp_ge_zero obs(2), of T]
       less_eq_real_def order_trans_rules(23) by blast
 qed
 
 lemma temp_dyn_up_real_arith:
   assumes "a > 0" and Thyps: "Tmin \<le> T" "T \<le> Tmax" "Tmax < (L::real)"
     and thyps: "0 \<le> t" "\<forall>\<tau>\<in>{0..t}. \<tau> \<le> - (ln ((L - Tmax) / (L - T)) / a) "
   shows "L - Tmax \<le> exp (-(a * t)) * (L - T)"
     and "L - exp (-(a * t)) * (L - T) \<le> Tmax"
     and "Tmin \<le> L - exp (-(a * t)) * (L - T)"
 proof-
   have "0 \<le> t \<and> t \<le> - (ln ((L - Tmax) / (L - T)) / a)"
     using thyps by auto
   hence "ln ((L - Tmax) / (L - T)) \<le> - a * t \<and> - a * t \<le> 0"
     using assms(1) divide_le_cancel by fastforce
   also have "(L - Tmax) / (L - T) > 0"
     using Thyps by auto
   ultimately have "(L - Tmax) / (L - T) \<le> exp (-a * t) \<and> exp (-a * t) \<le> 1"
     using exp_ln exp_le_one_iff by (metis exp_less_cancel_iff not_less)
   moreover have "L - T > 0"
     using Thyps by auto
   ultimately have obs: "(L - Tmax) \<le> exp (-a * t) * (L - T) \<and> exp (-a * t) * (L - T) \<le> (L - T)"
     by (simp add: pos_divide_le_eq)
   thus "(L - Tmax) \<le> exp (-(a * t)) * (L - T)"
     by auto
   thus "L - exp (-(a * t)) * (L - T) \<le> Tmax"
     by auto
   show "Tmin \<le> L - exp (-(a * t)) * (L - T)"
     using Thyps and obs by auto
 qed
 
 lemmas ffb_temp_dyn = local_flow.ffb_g_ode_ivl[OF local_flow_temp _ UNIV_I]
 
 lemma thermostat:
   assumes "a > 0" and "0 \<le> t" and "0 < Tmin" and "Tmax < L"
   shows "{s. Tmin \<le> s$1 \<and> s$1 \<le> Tmax \<and> s$4 = 0} \<le> fb\<^sub>\<F>
   (LOOP
     \<comment> \<open>control\<close>
     ((2 ::= (\<lambda>s. 0));(3 ::= (\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> Tmin + 1) THEN (4 ::= (\<lambda>s.1)) ELSE
     (IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> Tmax - 1) THEN (4 ::= (\<lambda>s.0)) ELSE skip));
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN (x\<acute>=(\<lambda>t. f a 0) & (\<lambda>s. s$2 \<le> - (ln (Tmin/s$3))/a) on (\<lambda>s. {0..t}) UNIV @ 0)
     ELSE (x\<acute>=(\<lambda>t. f a L) & (\<lambda>s. s$2 \<le> - (ln ((L-Tmax)/(L-s$3)))/a) on (\<lambda>s. {0..t}) UNIV @ 0)) )
   INV (\<lambda>s. Tmin \<le>s$1 \<and> s$1 \<le> Tmax \<and> (s$4 = 0 \<or> s$4 = 1)))
   {s. Tmin \<le> s$1 \<and> s$1 \<le> Tmax}"
   apply(rule ffb_loopI, simp_all add: ffb_temp_dyn[OF assms(1,2)] le_fun_def, safe)
   using temp_dyn_up_real_arith[OF assms(1) _ _ assms(4), of Tmin]
     and temp_dyn_down_real_arith[OF assms(1,3), of _ Tmax] by auto
 
 no_notation temp_vec_field ("f")
         and temp_flow ("\<phi>")
 
 subsubsection \<open> Tank \<close>
 
 text \<open> A controller turns a water pump on and off to keep the level of water @{text "h"} in a tank
 within an acceptable range @{text "hmin \<le> h \<le> hmax"}. Just like in the previous example, after 
 each intervention, the controller registers the current level of water and resets its chronometer,
 then it changes the status of the water pump accordingly. The level of water grows linearly 
 @{text "h' = k"} at a rate of @{text "k = c\<^sub>i-c\<^sub>o"} if the pump is on, and at a rate of 
 @{text "k = -c\<^sub>o"} if the pump is off. We use @{term "1::4"} to denote the tank's level of water,
 @{term "2::4"} is time as measured by the controller's chronometer, @{term "3::4"} is the
 level of water measured by the chronometer, and @{term "4::4"} states whether the pump is on
 (@{text "s$4 = 1"}) or off (@{text "s$4 = 0"}). We prove that the controller keeps the level of
 water between @{text "hmin"} and @{text "hmax"}. \<close>
 
 abbreviation tank_vec_field :: "real \<Rightarrow> real^4 \<Rightarrow> real^4" ("f")
   where "f k s \<equiv> (\<chi> i. if i = 2 then 1 else (if i = 1 then k else 0))"
 
 abbreviation tank_flow :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> real^4" ("\<phi>")
   where "\<phi> k \<tau> s \<equiv> (\<chi> i. if i = 1 then k * \<tau> + s$1 else 
   (if i = 2 then \<tau> + s$2 else s$i))"
 
 abbreviation tank_guard :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("G")
   where "G Hm k s \<equiv> s$2 \<le> (Hm - s$3)/k"
 
 abbreviation tank_loop_inv :: "real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("I")
   where "I hmin hmax s \<equiv> hmin \<le> s$1 \<and> s$1 \<le> hmax \<and> (s$4 = 0 \<or> s$4 = 1)"
 
 abbreviation tank_diff_inv :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real^4 \<Rightarrow> bool" ("dI")
   where "dI hmin hmax k s \<equiv> s$1 = k * s$2 + s$3 \<and> 0 \<le> s$2 \<and> 
     hmin \<le> s$3 \<and> s$3 \<le> hmax \<and> (s$4 =0 \<or> s$4 = 1)"
 
 lemma local_flow_tank: "local_flow (f k) UNIV UNIV (\<phi> k)"
   apply (unfold_locales, unfold local_lipschitz_def lipschitz_on_def, simp_all, clarsimp)
   apply(rule_tac x="1/2" in exI, clarsimp, rule_tac x=1 in exI)
   apply(simp add: dist_norm norm_vec_def L2_set_def, unfold UNIV_4)
   by (auto intro!: poly_derivatives simp: vec_eq_iff)
 
 lemma tank_arith:
   assumes "0 \<le> (\<tau>::real)" and "0 < c\<^sub>o" and "c\<^sub>o < c\<^sub>i"
   shows "\<forall>\<tau>\<in>{0..\<tau>}. \<tau> \<le> - ((hmin - y) / c\<^sub>o) \<Longrightarrow>  hmin \<le> y - c\<^sub>o * \<tau>"
     and "\<forall>\<tau>\<in>{0..\<tau>}. \<tau> \<le> (hmax - y) / (c\<^sub>i - c\<^sub>o) \<Longrightarrow>  (c\<^sub>i - c\<^sub>o) * \<tau> + y \<le> hmax"
     and "hmin \<le> y \<Longrightarrow> hmin \<le> (c\<^sub>i - c\<^sub>o) * \<tau> + y"
     and "y \<le> hmax \<Longrightarrow> y - c\<^sub>o * \<tau> \<le> hmax"
   apply(simp_all add: field_simps le_divide_eq assms)
   using assms apply (meson add_mono less_eq_real_def mult_left_mono)
   using assms by (meson add_increasing2 less_eq_real_def mult_nonneg_nonneg) 
 
 lemma tank_flow:
   assumes "0 < c\<^sub>o" and "c\<^sub>o < c\<^sub>i"
   shows "Collect (I hmin hmax) \<le> fb\<^sub>\<F>
   (LOOP 
     \<comment> \<open>control\<close>
     ((2 ::=(\<lambda>s.0));(3 ::=(\<lambda>s. s$1));
     (IF (\<lambda>s. s$4 = 0 \<and> s$3 \<le> hmin + 1) THEN (4 ::= (\<lambda>s.1)) ELSE 
     (IF (\<lambda>s. s$4 = 1 \<and> s$3 \<ge> hmax - 1) THEN (4 ::= (\<lambda>s.0)) ELSE skip));
     \<comment> \<open>dynamics\<close>
     (IF (\<lambda>s. s$4 = 0) THEN (x\<acute>= f (c\<^sub>i-c\<^sub>o) & (G hmax (c\<^sub>i-c\<^sub>o))) 
      ELSE (x\<acute>= f (-c\<^sub>o) & (G hmin (-c\<^sub>o)))) ) INV I hmin hmax)  
   (Collect (I hmin hmax))"
   apply(rule ffb_loopI, simp_all add: le_fun_def)
   apply(clarsimp simp: le_fun_def local_flow.ffb_g_ode_subset[OF local_flow_tank])
   using assms tank_arith[OF _ assms] by auto
 
 no_notation tank_vec_field ("f")
         and tank_flow ("\<phi>")
         and tank_loop_inv ("I")
         and tank_diff_inv ("dI")
         and tank_guard ("G")
 
 end
\ No newline at end of file
diff --git a/thys/Matrices_for_ODEs/MTX_Examples.thy b/thys/Matrices_for_ODEs/MTX_Examples.thy
--- a/thys/Matrices_for_ODEs/MTX_Examples.thy
+++ b/thys/Matrices_for_ODEs/MTX_Examples.thy
@@ -1,238 +1,238 @@
 (*  Title:       Verification Examples
-    Author:      Jonathan Julián Huerta y Munive, 2020
+    Author:      Jonathan Julián Huerta y Munive, 2021
     Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
 *)
 
 section \<open> Verification examples \<close>
 
 
 theory MTX_Examples
   imports 
     MTX_Flows 
     Hybrid_Systems_VCs.HS_VC_Spartan
 
 begin
 
 
 subsection \<open> Examples \<close>
 
 abbreviation hoareT :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a set) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" 
   ("PRE_ HP _ POST _" [85,85]85) where "PRE P HP X POST Q \<equiv> (P \<le> |X]Q)"
 
 
 subsubsection \<open> Verification by uniqueness. \<close>
 
 abbreviation mtx_circ :: "2 sq_mtx" ("A")
   where "A \<equiv> mtx  
    ([0,  1] # 
     [-1, 0] # [])"
 
 abbreviation mtx_circ_flow :: "real \<Rightarrow> real^2 \<Rightarrow> real^2" ("\<phi>")
   where "\<phi> t s \<equiv> (\<chi> i. if i = 1 then s$1 * cos t + s$2 * sin t else - s$1 * sin t + s$2 * cos t)"
 
 lemma mtx_circ_flow_eq: "exp (t *\<^sub>R A) *\<^sub>V s = \<phi> t s"
   apply(rule local_flow.eq_solution[OF local_flow_sq_mtx_linear, symmetric, of _ "\<lambda>s. UNIV"], simp_all)
     apply(rule ivp_solsI, simp_all add: sq_mtx_vec_mult_eq vec_eq_iff)
   unfolding UNIV_2 using exhaust_2
   by (force intro!: poly_derivatives simp: matrix_vector_mult_def)+
 
 lemma mtx_circ: 
   "PRE(\<lambda>s. r\<^sup>2 = (s $ 1)\<^sup>2 + (s $ 2)\<^sup>2) 
   HP x\<acute>=(*\<^sub>V) A & G 
   POST (\<lambda>s. r\<^sup>2 = (s $ 1)\<^sup>2 + (s $ 2)\<^sup>2)"
   apply(subst local_flow.fbox_g_ode_subset[OF local_flow_sq_mtx_linear])
   unfolding mtx_circ_flow_eq by auto
 
 no_notation mtx_circ ("A")
         and mtx_circ_flow ("\<phi>")
 
 
 subsubsection \<open> Flow of diagonalisable matrix. \<close>
 
 abbreviation mtx_hOsc :: "real \<Rightarrow> real \<Rightarrow> 2 sq_mtx" ("A")
   where "A a b \<equiv> mtx  
    ([0, 1] # 
     [a, b] # [])"
 
 abbreviation mtx_chB_hOsc :: "real \<Rightarrow> real \<Rightarrow> 2 sq_mtx" ("P")
   where "P a b \<equiv> mtx
    ([a, b] # 
     [1, 1] # [])"
 
 lemma inv_mtx_chB_hOsc: 
   "a \<noteq> b \<Longrightarrow> (P a b)\<^sup>-\<^sup>1 = (1/(a - b)) *\<^sub>R mtx 
    ([ 1, -b] # 
     [-1,  a] # [])"
   apply(rule sq_mtx_inv_unique, unfold scaleR_mtx2 times_mtx2)
   by (simp add: diff_divide_distrib[symmetric] one_mtx2)+
 
 lemma invertible_mtx_chB_hOsc: "a \<noteq> b \<Longrightarrow> mtx_invertible (P a b)"
   apply(rule mtx_invertibleI[of _ "(P a b)\<^sup>-\<^sup>1"])
    apply(unfold inv_mtx_chB_hOsc scaleR_mtx2 times_mtx2 one_mtx2)
   by (subst sq_mtx_eq_iff, simp add: vector_def frac_diff_eq1)+
 
 lemma mtx_hOsc_diagonalizable:
   fixes a b :: real
   defines "\<iota>\<^sub>1 \<equiv> (b - sqrt (b^2+4*a))/2" and "\<iota>\<^sub>2 \<equiv> (b + sqrt (b^2+4*a))/2"
   assumes "b\<^sup>2 + a * 4 > 0" and "a \<noteq> 0"
   shows "A a b = P (-\<iota>\<^sub>2/a) (-\<iota>\<^sub>1/a) * (\<d>\<i>\<a>\<g> i. if i = 1 then \<iota>\<^sub>1 else \<iota>\<^sub>2) * (P (-\<iota>\<^sub>2/a) (-\<iota>\<^sub>1/a))\<^sup>-\<^sup>1"
   unfolding assms apply(subst inv_mtx_chB_hOsc)
   using assms(3,4) apply(simp_all add: diag2_eq[symmetric])
   unfolding sq_mtx_times_eq sq_mtx_scaleR_eq UNIV_2 apply(subst sq_mtx_eq_iff)
   using exhaust_2 assms by (auto simp: field_simps, auto simp: field_power_simps)
 
 lemma mtx_hOsc_solution_eq:
   fixes a b :: real
   defines "\<iota>\<^sub>1 \<equiv> (b - sqrt (b\<^sup>2+4*a))/2" and "\<iota>\<^sub>2 \<equiv> (b + sqrt (b\<^sup>2+4*a))/2"
   defines "\<Phi> t \<equiv> mtx (
    [\<iota>\<^sub>2*exp(t*\<iota>\<^sub>1) - \<iota>\<^sub>1*exp(t*\<iota>\<^sub>2),     exp(t*\<iota>\<^sub>2)-exp(t*\<iota>\<^sub>1)]#
    [a*exp(t*\<iota>\<^sub>2) - a*exp(t*\<iota>\<^sub>1), \<iota>\<^sub>2*exp(t*\<iota>\<^sub>2)-\<iota>\<^sub>1*exp(t*\<iota>\<^sub>1)]#[])"
   assumes "b\<^sup>2 + a * 4 > 0" and "a \<noteq> 0"
   shows "P (-\<iota>\<^sub>2/a) (-\<iota>\<^sub>1/a) * (\<d>\<i>\<a>\<g> i. exp (t * (if i=1 then \<iota>\<^sub>1 else \<iota>\<^sub>2))) * (P (-\<iota>\<^sub>2/a) (-\<iota>\<^sub>1/a))\<^sup>-\<^sup>1 
   = (1/sqrt (b\<^sup>2 + a * 4)) *\<^sub>R (\<Phi> t)"
   unfolding assms apply(subst inv_mtx_chB_hOsc)
   using assms apply(simp_all add: mtx_times_scaleR_commute, subst sq_mtx_eq_iff)
   unfolding UNIV_2 sq_mtx_times_eq sq_mtx_scaleR_eq sq_mtx_uminus_eq apply(simp_all add: axis_def)
   by (auto simp: field_simps, auto simp: field_power_simps)+
  
 lemma local_flow_mtx_hOsc:
   fixes a b
   defines "\<iota>\<^sub>1 \<equiv> (b - sqrt (b^2+4*a))/2" and "\<iota>\<^sub>2 \<equiv> (b + sqrt (b^2+4*a))/2"
   defines "\<Phi> t \<equiv> mtx (
    [\<iota>\<^sub>2*exp(t*\<iota>\<^sub>1) - \<iota>\<^sub>1*exp(t*\<iota>\<^sub>2),     exp(t*\<iota>\<^sub>2)-exp(t*\<iota>\<^sub>1)]#
    [a*exp(t*\<iota>\<^sub>2) - a*exp(t*\<iota>\<^sub>1), \<iota>\<^sub>2*exp(t*\<iota>\<^sub>2)-\<iota>\<^sub>1*exp(t*\<iota>\<^sub>1)]#[])"
   assumes "b\<^sup>2 + a * 4 > 0" and "a \<noteq> 0"
   shows "local_flow ((*\<^sub>V) (A a b)) UNIV UNIV (\<lambda>t. (*\<^sub>V) ((1/sqrt (b\<^sup>2 + a * 4)) *\<^sub>R \<Phi> t))"
   unfolding assms using local_flow_sq_mtx_linear[of "A a b"] assms
   apply(subst (asm) exp_scaleR_diagonal2[OF invertible_mtx_chB_hOsc mtx_hOsc_diagonalizable])
      apply(simp, simp, simp)
   by (subst (asm) mtx_hOsc_solution_eq) simp_all
 
 lemma overdamped_door_arith:
   assumes "b\<^sup>2 + a * 4 > 0" and "a < 0" and "b \<le> 0" and "t \<ge> 0" and "s1 > 0"
   shows "0 \<le> ((b + sqrt (b\<^sup>2 + 4 * a)) * exp (t * (b - sqrt (b\<^sup>2 + 4 * a)) / 2) / 2 - 
 (b - sqrt (b\<^sup>2 + 4 * a)) * exp (t * (b + sqrt (b\<^sup>2 + 4 * a)) / 2) / 2) * s1 / sqrt (b\<^sup>2 + a * 4)"
 proof(subst diff_divide_distrib[symmetric], simp)
   have f0: "s1 / (2 * sqrt (b\<^sup>2 + a * 4)) > 0"  (is "s1/?c3 > 0")
     using assms(1,5) by simp
   have f1: "(b - sqrt (b\<^sup>2 + 4 * a)) < (b + sqrt (b\<^sup>2 + 4 * a))" (is "?c2 < ?c1") 
     and f2: "(b + sqrt (b\<^sup>2 + 4 * a)) < 0"
     using sqrt_ge_absD[of b "b\<^sup>2 + 4 * a"] assms by (force, linarith)
   hence f3: "exp (t * ?c2 / 2) \<le> exp (t * ?c1 / 2)" (is "exp ?t1 \<le> exp ?t2")
     unfolding exp_le_cancel_iff 
     using assms(4) by (case_tac "t=0", simp_all)
   hence "?c2 * exp ?t2 \<le> ?c2 * exp ?t1"
     using f1 f2 mult_le_cancel_left_pos[of "-?c2" "exp ?t1" "exp ?t2"] by linarith 
   also have "... < ?c1 * exp ?t1"
     using f1 by auto
   also have"... \<le> ?c1 * exp ?t1"
     using f1 f2 by auto
   ultimately show "0 \<le> (?c1 * exp ?t1 - ?c2 * exp ?t2) * s1 / ?c3"
     using f0 f1 assms(5) by auto
 qed
 
 abbreviation "open_door s \<equiv> {s. s$1 > 0 \<and> s$2 = 0}"
 
 lemma overdamped_door:
   assumes "b\<^sup>2 + a * 4 > 0" and "a < 0" and "b \<le> 0"
   shows "PRE (\<lambda>s. s$1 = 0)
   HP (LOOP open_door; (x\<acute>=((*\<^sub>V) (A a b)) & G) INV (\<lambda>s. 0 \<le> s$1))
   POST (\<lambda>s. 0 \<le> s $ 1)"
   apply(rule fbox_loopI, simp_all add: le_fun_def)
   apply(subst local_flow.fbox_g_ode_subset[OF local_flow_mtx_hOsc[OF assms(1)]])
   using assms apply(simp_all add: le_fun_def fbox_def)
   unfolding sq_mtx_scaleR_eq UNIV_2 sq_mtx_vec_mult_eq
   by (clarsimp simp: overdamped_door_arith)
 
 
 no_notation mtx_hOsc ("A")
         and mtx_chB_hOsc ("P")
 
 
 subsubsection \<open> Flow of non-diagonalisable matrix. \<close>
 
 abbreviation mtx_cnst_acc :: "3 sq_mtx" ("K")
   where "K \<equiv> mtx (
   [0,1,0] #
   [0,0,1] # 
   [0,0,0] # [])"
 
 lemma pow2_scaleR_mtx_cnst_acc: "(t *\<^sub>R K)\<^sup>2 = mtx (
   [0,0,t\<^sup>2] #
   [0,0,0] # 
   [0,0,0] # [])"
   unfolding power2_eq_square apply(subst sq_mtx_eq_iff)
   unfolding sq_mtx_times_eq UNIV_3 by auto
 
 lemma powN_scaleR_mtx_cnst_acc: "n > 2 \<Longrightarrow> (t *\<^sub>R K)^n = 0"
   apply(induct n, simp, case_tac "n \<le> 2")
    apply(subgoal_tac "n = 2", erule ssubst)
   unfolding power_Suc2 pow2_scaleR_mtx_cnst_acc sq_mtx_times_eq UNIV_3
   by (auto simp: sq_mtx_eq_iff)
 
 lemma exp_mtx_cnst_acc: "exp (t *\<^sub>R K) = ((t *\<^sub>R K)\<^sup>2/\<^sub>R 2) + (t *\<^sub>R K) + 1"
   unfolding exp_def apply(subst suminf_eq_sum[of 2])
   using powN_scaleR_mtx_cnst_acc by (simp_all add: numeral_2_eq_2)
  
 lemma exp_mtx_cnst_acc_simps:
   "exp (t *\<^sub>R K) $$ 1 $ 1 = 1" "exp (t *\<^sub>R K) $$ 1 $ 2 = t" "exp (t *\<^sub>R K) $$ 1 $ 3 = t^2/2"
   "exp (t *\<^sub>R K) $$ 2 $ 1 = 0" "exp (t *\<^sub>R K) $$ 2 $ 2 = 1" "exp (t *\<^sub>R K) $$ 2 $ 3 = t"
   "exp (t *\<^sub>R K) $$ 3 $ 1 = 0" "exp (t *\<^sub>R K) $$ 3 $ 2 = 0" "exp (t *\<^sub>R K) $$ 3 $ 3 = 1"
   unfolding exp_mtx_cnst_acc one_mtx3 pow2_scaleR_mtx_cnst_acc by simp_all
 
 lemma exp_mtx_cnst_acc_vec_mult_eq: "exp (t *\<^sub>R K) *\<^sub>V s = 
   vector [s$3 * t^2/2 + s$2 * t + s$1, s$3 * t + s$2, s$3]"
   apply(subst exp_mtx_cnst_acc, subst pow2_scaleR_mtx_cnst_acc)
   apply(simp add: sq_mtx_vec_mult_eq vector_def)
   unfolding UNIV_3 by (simp add: fun_eq_iff)
 
 lemma local_flow_mtx_cnst_acc:
   "local_flow ((*\<^sub>V) K) UNIV UNIV (\<lambda>t s. ((t *\<^sub>R K)\<^sup>2/\<^sub>R 2 + (t *\<^sub>R K) + 1) *\<^sub>V s)"
   using local_flow_sq_mtx_linear[of K] unfolding exp_mtx_cnst_acc .  
 
 lemma docking_station_arith:
   assumes "(d::real) > x" and "v > 0"
   shows "(v = v\<^sup>2 * t / (2 * d - 2 * x)) \<longleftrightarrow> (v * t - v\<^sup>2 * t\<^sup>2 / (4 * d - 4 * x) + x = d)"
 proof
   assume "v = v\<^sup>2 * t / (2 * d - 2 * x)"
   hence "v * t = 2 * (d - x)"
     using assms by (simp add: eq_divide_eq power2_eq_square) 
   hence "v * t - v\<^sup>2 * t\<^sup>2 / (4 * d - 4 * x) + x = 2 * (d - x) - 4 * (d - x)\<^sup>2 / (4 * (d - x)) + x"
     apply(subst power_mult_distrib[symmetric])
     by (erule ssubst, subst power_mult_distrib, simp)
   also have "... = d"
     apply(simp only: mult_divide_mult_cancel_left_if)
     using assms by (auto simp: power2_eq_square)
   finally show "v * t - v\<^sup>2 * t\<^sup>2 / (4 * d - 4 * x) + x = d" .
 next
   assume "v * t - v\<^sup>2 * t\<^sup>2 / (4 * d - 4 * x) + x = d"
   hence "0 = v\<^sup>2 * t\<^sup>2 / (4 * (d - x)) + (d - x) - v * t"
     by auto
   hence "0 = (4 * (d - x)) * (v\<^sup>2 * t\<^sup>2 / (4 * (d - x)) + (d - x) - v * t)"
     by auto
   also have "... = v\<^sup>2 * t\<^sup>2 + 4 * (d - x)\<^sup>2  - (4 * (d - x)) * (v * t)"
     using assms apply(simp add: distrib_left right_diff_distrib)
     apply(subst right_diff_distrib[symmetric])+
     by (simp add: power2_eq_square)
   also have "... = (v * t - 2 * (d - x))\<^sup>2"
     by (simp only: power2_diff, auto simp: field_simps power2_diff)
   finally have "0 = (v * t - 2 * (d - x))\<^sup>2" .
   hence "v * t = 2 * (d - x)"
     by auto
   thus "v = v\<^sup>2 * t / (2 * d - 2 * x)"
     apply(subst power2_eq_square, subst mult.assoc)
     apply(erule ssubst, subst right_diff_distrib[symmetric])
     using assms by auto
 qed
 
 lemma docking_station:
   assumes "d > x\<^sub>0" and "v\<^sub>0 > 0"
   shows "PRE (\<lambda>s. s$1 = x\<^sub>0 \<and> s$2 = v\<^sub>0)
   HP ((3 ::= (\<lambda>s. -(v\<^sub>0^2/(2*(d-x\<^sub>0))))); x\<acute>=(*\<^sub>V) K & G)
   POST (\<lambda>s. s$2 = 0 \<longleftrightarrow> s$1 = d)"
   apply(clarsimp simp: le_fun_def local_flow.fbox_g_ode_subset[OF local_flow_sq_mtx_linear[of K]])
   unfolding exp_mtx_cnst_acc_vec_mult_eq using assms by (simp add: docking_station_arith)
 
 no_notation mtx_cnst_acc ("K")
 
 end
\ No newline at end of file
diff --git a/thys/Matrices_for_ODEs/MTX_Flows.thy b/thys/Matrices_for_ODEs/MTX_Flows.thy
--- a/thys/Matrices_for_ODEs/MTX_Flows.thy
+++ b/thys/Matrices_for_ODEs/MTX_Flows.thy
@@ -1,290 +1,293 @@
 (*  Title:       Affine systems of ODEs
     Author:      Jonathan Julián Huerta y Munive, 2020
     Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
 *)
 
 section \<open> Affine systems of ODEs \<close>
 
 text \<open>Affine systems of ordinary differential equations (ODEs) are those whose vector 
 fields are linear operators. Broadly speaking, if there are functions $A$ and $B$ such that the 
 system of ODEs $X'\, t = f\, (X\, t)$ turns into $X'\, t = (A\, t)\cdot (X\, t)+(B\, t)$, then it
 is affine. The end goal of this section is to prove that every affine system of ODEs has a unique 
 solution, and to obtain a characterization of said solution. \<close>
 
 theory MTX_Flows
   imports 
     SQ_MTX 
     Hybrid_Systems_VCs.HS_ODEs
 
 begin
 
 
 subsection \<open> Existence and uniqueness for affine systems \<close>
 
 definition matrix_continuous_on :: "real set \<Rightarrow> (real \<Rightarrow> ('a::real_normed_algebra_1)^'n^'m) \<Rightarrow> bool" 
   where "matrix_continuous_on T A = (\<forall>t \<in> T. \<forall>\<epsilon> > 0. \<exists> \<delta> > 0. \<forall>\<tau>\<in>T. \<bar>\<tau> - t\<bar> < \<delta> \<longrightarrow> \<parallel>A \<tau> - A t\<parallel>\<^sub>o\<^sub>p \<le> \<epsilon>)"
 
 lemma continuous_on_matrix_vector_multl:
   assumes "matrix_continuous_on T A"
   shows "continuous_on T (\<lambda>t. A t *v s)"
 proof(rule continuous_onI, simp add: dist_norm)
   fix e t::real assume "0 < e" and "t \<in> T"
   let ?\<epsilon> = "e/(\<parallel>(if s = 0 then 1 else s)\<parallel>)"
   have "?\<epsilon> > 0"
     using \<open>0 < e\<close> by simp 
   then obtain \<delta> where dHyp: "\<delta> > 0 \<and> (\<forall>\<tau>\<in>T. \<bar>\<tau> - t\<bar> < \<delta> \<longrightarrow> \<parallel>A \<tau> - A t\<parallel>\<^sub>o\<^sub>p \<le> ?\<epsilon>)"
     using assms \<open>t \<in> T\<close> unfolding dist_norm matrix_continuous_on_def by fastforce
   {fix \<tau> assume "\<tau> \<in> T" and "\<bar>\<tau> - t\<bar> < \<delta>"
     have obs: "?\<epsilon> * (\<parallel>s\<parallel>) = (if s = 0 then 0 else e)"
       by auto
     have "\<parallel>A \<tau> *v s - A t *v s\<parallel> = \<parallel>(A \<tau> - A t) *v s\<parallel>"
       by (simp add: matrix_vector_mult_diff_rdistrib)      
     also have "... \<le> (\<parallel>A \<tau> - A t\<parallel>\<^sub>o\<^sub>p) * (\<parallel>s\<parallel>)"
       using norm_matrix_le_mult_op_norm by blast
     also have "... \<le> ?\<epsilon> * (\<parallel>s\<parallel>)"
       using dHyp \<open>\<tau> \<in> T\<close> \<open>\<bar>\<tau> - t\<bar> < \<delta>\<close> mult_right_mono norm_ge_zero by blast 
     finally have "\<parallel>A \<tau> *v s - A t *v s\<parallel> \<le> e"
-      by (subst (asm) obs) (metis (mono_tags, opaque_lifting) \<open>0 < e\<close> less_eq_real_def order_trans)}
+      by (subst (asm) obs) (metis (mono_tags) \<open>0 < e\<close> less_eq_real_def order_trans)}
   thus "\<exists>d>0. \<forall>\<tau>\<in>T. \<bar>\<tau> - t\<bar> < d \<longrightarrow> \<parallel>A \<tau> *v s - A t *v s\<parallel> \<le> e"
     using dHyp by blast
 qed
 
 lemma lipschitz_cond_affine:
   fixes A :: "real \<Rightarrow> 'a::real_normed_algebra_1^'n^'m" and T::"real set"
   defines "L \<equiv> Sup {\<parallel>A t\<parallel>\<^sub>o\<^sub>p |t. t \<in> T}"
   assumes "t \<in> T" and "bdd_above {\<parallel>A t\<parallel>\<^sub>o\<^sub>p |t. t \<in> T}"
   shows "\<parallel>A t *v x - A t *v y\<parallel> \<le> L * (\<parallel>x - y\<parallel>)"
 proof-
   have obs: "\<parallel>A t\<parallel>\<^sub>o\<^sub>p \<le> Sup {\<parallel>A t\<parallel>\<^sub>o\<^sub>p |t. t \<in> T}"
     apply(rule cSup_upper)
     using continuous_on_subset assms by (auto simp: dist_norm)
   have "\<parallel>A t *v x - A t *v y\<parallel> = \<parallel>A t *v (x - y)\<parallel>"
     by (simp add: matrix_vector_mult_diff_distrib)
   also have "... \<le> (\<parallel>A t\<parallel>\<^sub>o\<^sub>p) * (\<parallel>x - y\<parallel>)"
     using norm_matrix_le_mult_op_norm by blast
   also have "... \<le> Sup {\<parallel>A t\<parallel>\<^sub>o\<^sub>p |t. t \<in> T} * (\<parallel>x - y\<parallel>)"
     using obs mult_right_mono norm_ge_zero by blast 
   finally show "\<parallel>A t *v x - A t *v y\<parallel> \<le> L * (\<parallel>x - y\<parallel>)"
     unfolding assms .
 qed
 
 lemma local_lipschitz_affine:
   fixes A :: "real \<Rightarrow> 'a::real_normed_algebra_1^'n^'m"
   assumes "open T" and "open S" 
     and Ahyp: "\<And>\<tau> \<epsilon>. \<epsilon> > 0 \<Longrightarrow> \<tau> \<in> T \<Longrightarrow> cball \<tau> \<epsilon> \<subseteq> T \<Longrightarrow> bdd_above {\<parallel>A t\<parallel>\<^sub>o\<^sub>p |t. t \<in> cball \<tau> \<epsilon>}"
   shows "local_lipschitz T S (\<lambda>t s. A t *v s + B t)"
 proof(unfold local_lipschitz_def lipschitz_on_def, clarsimp)
   fix s t assume "s \<in> S" and "t \<in> T"
   then obtain e1 e2 where "cball t e1 \<subseteq> T" and "cball s e2 \<subseteq> S" and "min e1 e2 > 0"
     using open_cballE[OF _ \<open>open T\<close>] open_cballE[OF _ \<open>open S\<close>] by force
   hence obs: "cball t (min e1 e2) \<subseteq> T"
     by auto
   let ?L = "Sup {\<parallel>A \<tau>\<parallel>\<^sub>o\<^sub>p |\<tau>. \<tau> \<in> cball t (min e1 e2)}"
   have "\<parallel>A t\<parallel>\<^sub>o\<^sub>p \<in> {\<parallel>A \<tau>\<parallel>\<^sub>o\<^sub>p |\<tau>. \<tau> \<in> cball t (min e1 e2)}"
     using \<open>min e1 e2 > 0\<close> by auto
   moreover have bdd: "bdd_above {\<parallel>A \<tau>\<parallel>\<^sub>o\<^sub>p |\<tau>. \<tau> \<in> cball t (min e1 e2)}"
     by (rule Ahyp, simp only: \<open>min e1 e2 > 0\<close>, simp_all add: \<open>t \<in> T\<close> obs)
   moreover have "Sup {\<parallel>A \<tau>\<parallel>\<^sub>o\<^sub>p |\<tau>. \<tau> \<in> cball t (min e1 e2)} \<ge> 0"
     apply(rule order.trans[OF op_norm_ge_0[of "A t"]])
     by (rule cSup_upper[OF calculation])
   moreover have "\<forall>x\<in>cball s (min e1 e2) \<inter> S. \<forall>y\<in>cball s (min e1 e2) \<inter> S. 
     \<forall>\<tau>\<in>cball t (min e1 e2) \<inter> T. dist (A \<tau> *v x) (A \<tau> *v y) \<le> ?L * dist x y"
     apply(clarify, simp only: dist_norm, rule lipschitz_cond_affine)
     using \<open>min e1 e2 > 0\<close> bdd by auto
   ultimately show "\<exists>e>0. \<exists>L. \<forall>t\<in>cball t e \<inter> T. 0 \<le> L \<and> 
     (\<forall>x\<in>cball s e \<inter> S. \<forall>y\<in>cball s e \<inter> S. dist (A t *v x) (A t *v y) \<le> L * dist x y)"
     using \<open>min e1 e2 > 0\<close> by blast
 qed
 
 lemma picard_lindeloef_affine:
   fixes A :: "real \<Rightarrow> 'a::{banach,real_normed_algebra_1,heine_borel}^'n^'n"
   assumes Ahyp: "matrix_continuous_on T A"
       and "\<And>\<tau> \<epsilon>. \<tau> \<in> T \<Longrightarrow> \<epsilon> > 0 \<Longrightarrow> bdd_above {\<parallel>A t\<parallel>\<^sub>o\<^sub>p |t. dist \<tau> t \<le> \<epsilon>}"
       and Bhyp: "continuous_on T B" and "open S" 
       and "t\<^sub>0 \<in> T" and Thyp: "open T" "is_interval T" 
     shows "picard_lindeloef (\<lambda> t s. A t *v s + B t) T S t\<^sub>0"
   apply (unfold_locales, simp_all add: assms, clarsimp)
    apply (rule continuous_on_add[OF continuous_on_matrix_vector_multl[OF Ahyp] Bhyp])
   by (rule local_lipschitz_affine) (simp_all add: assms)
 
 lemma picard_lindeloef_autonomous_affine: 
   fixes A :: "'a::{banach,real_normed_field,heine_borel}^'n^'n"
   shows "picard_lindeloef (\<lambda> t s. A *v s + B) UNIV UNIV t\<^sub>0"
   using picard_lindeloef_affine[of _ "\<lambda>t. A" "\<lambda>t. B"] 
   unfolding matrix_continuous_on_def by (simp only: diff_self op_norm0, auto)
 
 lemma picard_lindeloef_autonomous_linear:
   fixes A :: "'a::{banach,real_normed_field,heine_borel}^'n^'n"
   shows "picard_lindeloef (\<lambda> t. (*v) A) UNIV UNIV t\<^sub>0"
   using picard_lindeloef_autonomous_affine[of A 0] by force
 
 lemmas unique_sol_autonomous_affine = picard_lindeloef.ivp_unique_solution[OF 
     picard_lindeloef_autonomous_affine UNIV_I _ subset_UNIV]
 
 lemmas unique_sol_autonomous_linear = picard_lindeloef.ivp_unique_solution[OF 
     picard_lindeloef_autonomous_linear UNIV_I _ subset_UNIV]
 
 
 subsection \<open> Flow for affine systems \<close>
 
 
 subsubsection \<open> Derivative rules for square matrices \<close>
 
+declare has_derivative_component [simp del]
+
 lemma has_derivative_exp_scaleRl[derivative_intros]:
   fixes f::"real \<Rightarrow> real" (* by Fabian Immler and Johannes Hölzl *)
   assumes "D f \<mapsto> f' at t within T"
   shows "D (\<lambda>t. exp (f t *\<^sub>R A)) \<mapsto> (\<lambda>h. f' h *\<^sub>R (exp (f t *\<^sub>R A) * A)) at t within T"
 proof -
   have "bounded_linear f'" 
     using assms by auto
   then obtain m where obs: "f' = (\<lambda>h. h * m)"
     using real_bounded_linear by blast
   thus ?thesis
     using vector_diff_chain_within[OF _ exp_scaleR_has_vector_derivative_right] 
       assms obs by (auto simp: has_vector_derivative_def comp_def)
 qed
 
 lemma vderiv_on_exp_scaleRlI[poly_derivatives]:
   assumes "D f = f' on T" and "g' = (\<lambda>x. f' x *\<^sub>R exp (f x *\<^sub>R A) * A)"
   shows "D (\<lambda>x. exp (f x *\<^sub>R A)) = g' on T"
   using assms unfolding has_vderiv_on_def has_vector_derivative_def apply clarsimp
   by (rule has_derivative_exp_scaleRl, auto simp: fun_eq_iff)
 
 lemma has_derivative_mtx_ith[derivative_intros]:
   fixes t::real and T :: "real set"
   defines "t\<^sub>0 \<equiv> netlimit (at t within T)"
   assumes "D A \<mapsto> (\<lambda>h. h *\<^sub>R A' t) at t within T"
   shows "D (\<lambda>t. A t $$ i) \<mapsto> (\<lambda>h. h *\<^sub>R A' t $$ i) at t within T"
   using assms unfolding has_derivative_def apply safe
    apply(force simp: bounded_linear_def bounded_linear_axioms_def)
   apply(rule_tac F="\<lambda>\<tau>. (A \<tau> - A t\<^sub>0 - (\<tau> - t\<^sub>0) *\<^sub>R A' t) /\<^sub>R (\<parallel>\<tau> - t\<^sub>0\<parallel>)" in tendsto_zero_norm_bound)
   by (clarsimp, rule mult_left_mono, metis (no_types, lifting) norm_column_le_norm 
       sq_mtx_minus_ith sq_mtx_scaleR_ith) simp_all
 
 lemmas has_derivative_mtx_vec_mult[derivative_intros] = 
   bounded_bilinear.FDERIV[OF bounded_bilinear_sq_mtx_vec_mult]
 
 lemma vderiv_on_mtx_vec_multI[poly_derivatives]:
   assumes "D u = u' on T" and "D A = A' on T"
       and "g = (\<lambda>t. A t *\<^sub>V u' t + A' t *\<^sub>V u t )"
     shows "D (\<lambda>t. A t *\<^sub>V u t) = g on T"
-  using assms unfolding has_vderiv_on_def has_vector_derivative_def apply clarsimp
+  using assms unfolding has_vderiv_on_def has_vector_derivative_def apply clarify
   apply(erule_tac x=x in ballE, simp_all)+
   apply(rule derivative_eq_intros)
   by (auto simp: fun_eq_iff mtx_vec_scaleR_commute pth_6 scaleR_mtx_vec_assoc)
 
 lemmas has_vderiv_on_ivl_integral = ivl_integral_has_vderiv_on[OF vderiv_on_continuous_on]
 
 declare has_vderiv_on_ivl_integral [poly_derivatives]
 
 lemma has_derivative_mtx_vec_multl[derivative_intros]:
   assumes "\<And> i j. D (\<lambda>t. (A t) $$ i $ j) \<mapsto> (\<lambda>\<tau>. \<tau> *\<^sub>R (A' t) $$ i $ j) (at t within T)"
   shows "D (\<lambda>t. A t *\<^sub>V x) \<mapsto> (\<lambda>\<tau>. \<tau> *\<^sub>R (A' t) *\<^sub>V x) at t within T"
   unfolding sq_mtx_vec_mult_sum_cols
   apply(rule_tac f'1="\<lambda>i \<tau>. \<tau> *\<^sub>R  (x $ i *\<^sub>R \<c>\<o>\<l> i (A' t))" in derivative_eq_intros(10))
    apply(simp_all add: scaleR_right.sum)
   apply(rule_tac g'1="\<lambda>\<tau>. \<tau> *\<^sub>R \<c>\<o>\<l> i (A' t)" in derivative_eq_intros(4), simp_all add: mult.commute)
-  using assms unfolding sq_mtx_col_def column_def apply(transfer, simp)
-  apply(rule has_derivative_vec_lambda)
-  by (simp add: scaleR_vec_def)
+  using assms unfolding sq_mtx_col_def column_def 
+  by (transfer, simp add: has_derivative_component)
+
+declare has_derivative_component [simp]
 
 lemma continuous_on_mtx_vec_multr: "continuous_on S ((*\<^sub>V) A)"
   by transfer (simp add: matrix_vector_mult_linear_continuous_on)
 
-\<comment> \<open>Automatically generated derivative rules from this subsubsection \<close>
+text \<open>Isabelle automatically generates derivative rules from this subsubsection \<close>
 
-thm derivative_eq_intros(140,141,142,143)
+thm derivative_eq_intros(140-)
 
 
 subsubsection \<open> Existence and uniqueness with square matrices \<close>
 
 text \<open>Finally, we can use the @{term exp} operation to characterize the general solutions for affine 
 systems of ODEs. We show that they satisfy the @{term "local_flow"} locale.\<close>
 
 lemma continuous_on_sq_mtx_vec_multl:
   fixes A :: "real \<Rightarrow> ('n::finite) sq_mtx"
   assumes "continuous_on T A"
   shows "continuous_on T (\<lambda>t. A t *\<^sub>V s)"
 proof-
   have "matrix_continuous_on T (\<lambda>t. to_vec (A t))"
     using assms by (force simp: continuous_on_iff dist_norm norm_sq_mtx_def matrix_continuous_on_def)
   hence "continuous_on T (\<lambda>t. to_vec (A t) *v s)"
     by (rule continuous_on_matrix_vector_multl)
   thus ?thesis
     by transfer
 qed
 
 lemmas continuous_on_affine = continuous_on_add[OF continuous_on_sq_mtx_vec_multl]
 
 lemma local_lipschitz_sq_mtx_affine:
   fixes A :: "real \<Rightarrow> ('n::finite) sq_mtx"
   assumes "continuous_on T A" "open T" "open S"
   shows "local_lipschitz T S (\<lambda>t s. A t *\<^sub>V s + B t)"
 proof-
   have obs: "\<And>\<tau> \<epsilon>. 0 < \<epsilon> \<Longrightarrow>  \<tau> \<in> T \<Longrightarrow> cball \<tau> \<epsilon> \<subseteq> T \<Longrightarrow> bdd_above {\<parallel>A t\<parallel> |t. t \<in> cball \<tau> \<epsilon>}"
     by (rule bdd_above_norm_cont_comp, rule continuous_on_subset[OF assms(1)], simp_all)
   hence "\<And>\<tau> \<epsilon>. 0 < \<epsilon> \<Longrightarrow> \<tau> \<in> T \<Longrightarrow> cball \<tau> \<epsilon> \<subseteq> T \<Longrightarrow> bdd_above {\<parallel>to_vec (A t)\<parallel>\<^sub>o\<^sub>p |t. t \<in> cball \<tau> \<epsilon>}"
     by (simp add: norm_sq_mtx_def)
   hence "local_lipschitz T S (\<lambda>t s. to_vec (A t) *v s + B t)"
     using local_lipschitz_affine[OF assms(2,3), of "\<lambda>t. to_vec (A t)"] by force
   thus ?thesis
     by transfer 
 qed
 
 lemma picard_lindeloef_sq_mtx_affine:
   assumes "continuous_on T A" and "continuous_on T B" 
     and "t\<^sub>0 \<in> T" "is_interval T" "open T" and "open S"
   shows "picard_lindeloef (\<lambda>t s. A t *\<^sub>V s + B t) T S t\<^sub>0"
   apply(unfold_locales, simp_all add: assms, clarsimp)
   using continuous_on_affine assms apply blast
   by (rule local_lipschitz_sq_mtx_affine, simp_all add: assms)
 
 lemmas sq_mtx_unique_sol_autonomous_affine = picard_lindeloef.ivp_unique_solution[OF 
     picard_lindeloef_sq_mtx_affine[OF
       continuous_on_const 
       continuous_on_const 
       UNIV_I is_interval_univ 
       open_UNIV open_UNIV] 
     UNIV_I _ subset_UNIV]
 
 lemma has_vderiv_on_sq_mtx_linear:
   "D (\<lambda>t. exp ((t - t\<^sub>0) *\<^sub>R A) *\<^sub>V s) = (\<lambda>t. A *\<^sub>V (exp ((t - t\<^sub>0) *\<^sub>R A) *\<^sub>V s)) on {t\<^sub>0--t}"
   by (rule poly_derivatives)+ (auto simp: exp_times_scaleR_commute sq_mtx_times_vec_assoc)
 
 lemma has_vderiv_on_sq_mtx_affine:
   fixes t\<^sub>0::real and A :: "('a::finite) sq_mtx"
   defines "lSol c t \<equiv> exp ((c * (t - t\<^sub>0)) *\<^sub>R A)"
   shows "D (\<lambda>t. lSol 1 t *\<^sub>V s + lSol 1 t *\<^sub>V (\<integral>\<^sub>t\<^sub>0\<^sup>t (lSol (-1) \<tau> *\<^sub>V B) \<partial>\<tau>)) = 
   (\<lambda>t. A *\<^sub>V (lSol 1 t *\<^sub>V s + lSol 1 t *\<^sub>V (\<integral>\<^sub>t\<^sub>0\<^sup>t (lSol (-1) \<tau> *\<^sub>V B) \<partial>\<tau>)) + B) on {t\<^sub>0--t}"
   unfolding assms apply(simp only: mult.left_neutral mult_minus1)
   apply(rule poly_derivatives, (force)?, (force)?, (force)?, (force)?)+
   by (simp add: mtx_vec_mult_add_rdistl sq_mtx_times_vec_assoc[symmetric] 
       exp_minus_inverse exp_times_scaleR_commute mult_exp_exp  scale_left_distrib[symmetric])
 
 lemma autonomous_linear_sol_is_exp:
   assumes "D X = (\<lambda>t. A *\<^sub>V X t) on {t\<^sub>0--t}" and "X t\<^sub>0 = s" 
   shows "X t = exp ((t - t\<^sub>0) *\<^sub>R A) *\<^sub>V s"
   apply(rule sq_mtx_unique_sol_autonomous_affine[of "\<lambda>s. {t\<^sub>0--t}" _ t X A 0])
   using assms apply(simp_all add: ivp_sols_def)
   using has_vderiv_on_sq_mtx_linear by force+
 
 lemma autonomous_affine_sol_is_exp_plus_int:
   assumes "D X = (\<lambda>t. A *\<^sub>V X t + B) on {t\<^sub>0--t}" and "X t\<^sub>0 = s" 
   shows "X t = exp ((t - t\<^sub>0) *\<^sub>R A) *\<^sub>V s + exp ((t - t\<^sub>0) *\<^sub>R A) *\<^sub>V (\<integral>\<^sub>t\<^sub>0\<^sup>t(exp (- (\<tau> - t\<^sub>0) *\<^sub>R A) *\<^sub>V B)\<partial>\<tau>)"
   apply(rule sq_mtx_unique_sol_autonomous_affine[of "\<lambda>s. {t\<^sub>0--t}" _ t X A B])
   using assms apply(simp_all add: ivp_sols_def)
   using has_vderiv_on_sq_mtx_affine by force+
 
 lemma local_flow_sq_mtx_linear: "local_flow ((*\<^sub>V) A) UNIV UNIV (\<lambda>t s. exp (t *\<^sub>R A) *\<^sub>V s)"
   unfolding local_flow_def local_flow_axioms_def apply safe
   using picard_lindeloef_sq_mtx_affine[of _ "\<lambda>t. A" "\<lambda>t. 0"] apply force
   using has_vderiv_on_sq_mtx_linear[of 0] by auto
 
 lemma local_flow_sq_mtx_affine: "local_flow (\<lambda>s. A *\<^sub>V s + B) UNIV UNIV 
   (\<lambda>t s. exp (t *\<^sub>R A) *\<^sub>V s + exp (t *\<^sub>R A) *\<^sub>V (\<integral>\<^sub>0\<^sup>t(exp (- \<tau> *\<^sub>R A) *\<^sub>V B)\<partial>\<tau>))"
   unfolding local_flow_def local_flow_axioms_def apply safe
   using picard_lindeloef_sq_mtx_affine[of _ "\<lambda>t. A" "\<lambda>t. B"] apply force
   using has_vderiv_on_sq_mtx_affine[of 0 A] by auto
 
 
 end
\ No newline at end of file
diff --git a/thys/Matrices_for_ODEs/MTX_Preliminaries.thy b/thys/Matrices_for_ODEs/MTX_Preliminaries.thy
--- a/thys/Matrices_for_ODEs/MTX_Preliminaries.thy
+++ b/thys/Matrices_for_ODEs/MTX_Preliminaries.thy
@@ -1,403 +1,403 @@
 (*  Title:       Mathematical Preliminaries
     Author:      Jonathan Julián Huerta y Munive, 2020
     Maintainer:  Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
 *)
 
 section \<open> Mathematical Preliminaries \<close>
 
 text \<open>This section adds useful syntax, abbreviations and theorems to the Isabelle distribution. \<close>
 
 theory MTX_Preliminaries
   imports Hybrid_Systems_VCs.HS_Preliminaries
 
 begin
 
 
 subsection \<open> Syntax \<close>
 
 abbreviation "\<e> k \<equiv> axis k 1"
 
 syntax
   "_ivl_integral" :: "real \<Rightarrow> real \<Rightarrow> 'a \<Rightarrow> pttrn \<Rightarrow> bool" ("(3\<integral>\<^sub>_\<^sup>_ (_)\<partial>/_)" [0, 0, 10] 10)
 
 translations
   "\<integral>\<^sub>a\<^sup>b f \<partial>x" \<rightleftharpoons> "CONST ivl_integral a b (\<lambda>x. f)"
 
 notation matrix_inv ("_\<^sup>-\<^sup>1" [90])
 
 abbreviation "entries (A::'a^'n^'m) \<equiv> {A $ i $ j | i j. i \<in> UNIV \<and> j \<in> UNIV}"
 
 
 subsection \<open> Topology and sets \<close>
 
 lemmas compact_imp_bdd_above = compact_imp_bounded[THEN bounded_imp_bdd_above]
 
 lemma comp_cont_image_spec: "continuous_on T f \<Longrightarrow> compact T \<Longrightarrow> compact {f t |t. t \<in> T}"
   using compact_continuous_image by (simp add: Setcompr_eq_image)
 
 lemmas bdd_above_cont_comp_spec = compact_imp_bdd_above[OF comp_cont_image_spec]
 
 lemmas bdd_above_norm_cont_comp = continuous_on_norm[THEN bdd_above_cont_comp_spec]
 
 lemma open_cballE: "t\<^sub>0 \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>e>0. cball t\<^sub>0 e \<subseteq> T"
   using open_contains_cball by blast
 
 lemma open_ballE: "t\<^sub>0 \<in> T \<Longrightarrow> open T \<Longrightarrow> \<exists>e>0. ball t\<^sub>0 e \<subseteq> T"
   using open_contains_ball by blast
 
 lemma funcset_UNIV: "f \<in> A \<rightarrow> UNIV"
   by auto
 
 lemma finite_image_of_finite[simp]:
   fixes f::"'a::finite \<Rightarrow> 'b"
   shows "finite {x. \<exists>i. x = f i}"
   using finite_Atleast_Atmost_nat by force
 
 lemma finite_image_of_finite2:
   fixes f :: "'a::finite \<Rightarrow> 'b::finite \<Rightarrow> 'c"
   shows "finite {f x y |x y. P x y}"
 proof-
   have "finite (\<Union>x. {f x y|y. P x y})"
     by simp
   moreover have "{f x y|x y. P x y} = (\<Union>x. {f x y|y. P x y})"
     by auto
   ultimately show ?thesis 
     by simp
 qed
 
 
 subsection \<open> Functions \<close>
 
 lemma finite_sum_univ_singleton: "(sum g UNIV) = sum g {i::'a::finite} + sum g (UNIV - {i})"
   by (metis add.commute finite_class.finite_UNIV sum.subset_diff top_greatest)
 
 lemma suminfI:
   fixes f :: "nat \<Rightarrow> 'a::{t2_space,comm_monoid_add}"
   shows "f sums k \<Longrightarrow> suminf f = k"
   unfolding sums_iff by simp
 
 lemma suminf_eq_sum:
   fixes f :: "nat \<Rightarrow> ('a::real_normed_vector)"
   assumes "\<And>n. n > m \<Longrightarrow> f n = 0"
   shows "(\<Sum>n. f n) = (\<Sum>n \<le> m. f n)"
   using assms by (meson atMost_iff finite_atMost not_le suminf_finite)
 
 lemma suminf_multr: "summable f \<Longrightarrow> (\<Sum>n. f n * c) = (\<Sum>n. f n) * c" for c::"'a::real_normed_algebra"
   by (rule bounded_linear.suminf [OF bounded_linear_mult_left, symmetric])
 
 lemma sum_if_then_else_simps[simp]:
   fixes q :: "('a::semiring_0)" and i :: "'n::finite"
   shows "(\<Sum>j\<in>UNIV. f j * (if j = i then q else 0)) = f i * q"
     and "(\<Sum>j\<in>UNIV. f j * (if i = j then q else 0)) = f i * q"
     and "(\<Sum>j\<in>UNIV. (if i = j then q else 0) * f j) = q * f i"
     and "(\<Sum>j\<in>UNIV. (if j = i then q else 0) * f j) = q * f i"
   by (auto simp: finite_sum_univ_singleton[of _ i])
 
 
 subsection \<open> Suprema \<close>
 
 lemma le_max_image_of_finite[simp]:
   fixes f::"'a::finite \<Rightarrow> 'b::linorder"
   shows "(f i) \<le> Max {x. \<exists>i. x = f i}"
   by (rule Max.coboundedI, simp_all) (rule_tac x=i in exI, simp)
 
 lemma cSup_eq:
   fixes c::"'a::conditionally_complete_lattice"
   assumes "\<forall>x \<in> X. x \<le> c" and "\<exists>x \<in> X. c \<le> x"
   shows "Sup X = c"
   by (metis assms cSup_eq_maximum order_class.order.antisym)
 
 lemma cSup_mem_eq: 
   "c \<in> X \<Longrightarrow> \<forall>x \<in> X. x \<le> c \<Longrightarrow> Sup X = c" for c::"'a::conditionally_complete_lattice"
   by (rule cSup_eq, auto)
 
 lemma cSup_finite_ex:
   "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>x\<in>X. Sup X = x" for X::"'a::conditionally_complete_linorder set"
   by (metis (full_types) bdd_finite(1) cSup_upper finite_Sup_less_iff order_less_le)
 
 lemma cMax_finite_ex:
   "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>x\<in>X. Max X = x" for X::"'a::conditionally_complete_linorder set"
   apply(subst cSup_eq_Max[symmetric])
   using cSup_finite_ex by auto
 
 lemma finite_nat_minimal_witness:
   fixes P :: "('a::finite) \<Rightarrow> nat \<Rightarrow> bool"
   assumes "\<forall>i. \<exists>N::nat. \<forall>n \<ge> N. P i n"
   shows "\<exists>N. \<forall>i. \<forall>n \<ge> N. P i n" 
 proof-
   let "?bound i" = "(LEAST N. \<forall>n \<ge> N. P i n)"
   let ?N = "Max {?bound i |i. i \<in> UNIV}"
   {fix n::nat and i::'a 
     assume "n \<ge> ?N" 
     obtain M where "\<forall>n \<ge> M. P i n" 
       using assms by blast
     hence obs: "\<forall> m \<ge> ?bound i. P i m"
       using LeastI[of "\<lambda>N. \<forall>n \<ge> N. P i n"] by blast
     have "finite {?bound i |i. i \<in> UNIV}"
       by simp
     hence "?N \<ge> ?bound i"
       using Max_ge by blast
     hence "n \<ge> ?bound i" 
       using \<open>n \<ge> ?N\<close> by linarith
     hence "P i n" 
       using obs by blast}
   thus "\<exists>N. \<forall>i n. N \<le> n \<longrightarrow> P i n" 
     by blast
 qed
 
 
 subsection \<open> Real numbers \<close>
 
 named_theorems field_power_simps "simplification rules for powers to the nth"
 
 declare semiring_normalization_rules(18) [field_power_simps]
     and semiring_normalization_rules(26) [field_power_simps]
     and semiring_normalization_rules(27) [field_power_simps]
     and semiring_normalization_rules(28) [field_power_simps]
     and semiring_normalization_rules(29) [field_power_simps]
 
 text \<open>WARNING: Adding @{thm semiring_normalization_rules(27)} to our tactic makes 
 its combination with simp to loop infinitely in some proofs.\<close>
 
 lemma sq_le_cancel:
   shows "(a::real) \<ge> 0 \<Longrightarrow> b \<ge> 0 \<Longrightarrow> a^2 \<le> b * a \<Longrightarrow> a \<le> b"
   and "(a::real) \<ge> 0 \<Longrightarrow> b \<ge> 0 \<Longrightarrow> a^2 \<le> a * b \<Longrightarrow> a \<le> b"
    apply (metis less_eq_real_def mult.commute mult_le_cancel_left semiring_normalization_rules(29))
   by (metis less_eq_real_def mult_le_cancel_left semiring_normalization_rules(29))
 
 lemma frac_diff_eq1: "a \<noteq> b \<Longrightarrow> a / (a - b) - b / (a - b) = 1" for a::real
-  by (metis (no_types, opaque_lifting) ab_left_minus add.commute add_left_cancel 
+  by (metis (no_types) ab_left_minus add.commute add_left_cancel 
       diff_divide_distrib diff_minus_eq_add div_self)
 
 lemma exp_add: "x * y - y * x = 0 \<Longrightarrow> exp (x + y) = exp x * exp y" 
   by (rule exp_add_commuting) (simp add: ac_simps)
 
 lemmas mult_exp_exp = exp_add[symmetric]
 
 
 subsection \<open> Vectors and matrices \<close>
 
 lemma sum_axis[simp]:
   fixes q :: "('a::semiring_0)"
   shows "(\<Sum>j\<in>UNIV. f j * axis i q $ j) = f i * q"
     and "(\<Sum>j\<in>UNIV. axis i q $ j * f j) = q * f i"
   unfolding axis_def by(auto simp: vec_eq_iff)
 
 lemma sum_scalar_nth_axis: "sum (\<lambda>i. (x $ i) *s \<e> i) UNIV = x" for x :: "('a::semiring_1)^'n"
   unfolding vec_eq_iff axis_def by simp
 
 lemma scalar_eq_scaleR[simp]: "c *s x = c *\<^sub>R x"
   unfolding vec_eq_iff by simp
 
 lemma matrix_add_rdistrib: "((B + C) ** A) = (B ** A) + (C ** A)"
   by (vector matrix_matrix_mult_def sum.distrib[symmetric] field_simps)
 
 lemma vec_mult_inner: "(A *v v) \<bullet> w = v \<bullet> (transpose A *v w)" for A :: "real ^'n^'n"
   unfolding matrix_vector_mult_def transpose_def inner_vec_def
   apply(simp add: sum_distrib_right sum_distrib_left)
   apply(subst sum.swap)
   apply(subgoal_tac "\<forall>i j. A $ i $ j * v $ j * w $ i = v $ j * (A $ i $ j * w $ i)")
   by presburger simp
 
 lemma uminus_axis_eq[simp]: "- axis i k = axis i (-k)" for k :: "'a::ring"
   unfolding axis_def by(simp add: vec_eq_iff)
 
 lemma norm_axis_eq[simp]: "\<parallel>axis i k\<parallel> = \<parallel>k\<parallel>"
 proof(simp add: axis_def norm_vec_def L2_set_def)
   let "?\<delta>\<^sub>K" = "\<lambda>i j k. if i = j then k else 0" 
   have "(\<Sum>j\<in>UNIV. (\<parallel>(?\<delta>\<^sub>K j i k)\<parallel>)\<^sup>2) = (\<Sum>j\<in>{i}. (\<parallel>(?\<delta>\<^sub>K j i k)\<parallel>)\<^sup>2) + (\<Sum>j\<in>(UNIV-{i}). (\<parallel>(?\<delta>\<^sub>K j i k)\<parallel>)\<^sup>2)"
     using finite_sum_univ_singleton by blast 
   also have "... = (\<parallel>k\<parallel>)\<^sup>2" 
     by simp
   finally show "sqrt (\<Sum>j\<in>UNIV. (norm (if j = i then k else 0))\<^sup>2) = norm k" 
     by simp
 qed
 
 lemma matrix_axis_0: 
   fixes A :: "('a::idom)^'n^'m"
   assumes "k \<noteq> 0 " and h:"\<forall>i. (A *v (axis i k)) = 0"
   shows "A = 0"  
 proof-
   {fix i::'n
     have "0 = (\<Sum>j\<in>UNIV. (axis i k) $ j *s column j A)" 
       using h matrix_mult_sum[of A "axis i k"] by simp
     also have "... = k *s column i A" 
       by (simp add: axis_def vector_scalar_mult_def column_def vec_eq_iff mult.commute)
     finally have "k *s column i A = 0"
       unfolding axis_def by simp
     hence "column i A = 0" 
       using vector_mul_eq_0 \<open>k \<noteq> 0\<close> by blast}
   thus "A = 0" 
     unfolding column_def vec_eq_iff by simp
 qed
 
 lemma scaleR_norm_sgn_eq: "(\<parallel>x\<parallel>) *\<^sub>R sgn x = x"
   by (metis divideR_right norm_eq_zero scale_eq_0_iff sgn_div_norm)
 
 lemma vector_scaleR_commute: "A *v c *\<^sub>R x = c *\<^sub>R (A *v x)" for x :: "('a::real_normed_algebra_1)^'n"
   unfolding scaleR_vec_def matrix_vector_mult_def by(auto simp: vec_eq_iff scaleR_right.sum)
 
 lemma scaleR_vector_assoc: "c *\<^sub>R (A *v x) = (c *\<^sub>R A) *v x" for x :: "('a::real_normed_algebra_1)^'n"
   unfolding matrix_vector_mult_def by(auto simp: vec_eq_iff scaleR_right.sum)
 
 lemma mult_norm_matrix_sgn_eq:
   fixes x :: "('a::real_normed_algebra_1)^'n"
   shows "(\<parallel>A *v sgn x\<parallel>) * (\<parallel>x\<parallel>) = \<parallel>A *v x\<parallel>"
 proof-
   have "\<parallel>A *v x\<parallel> = \<parallel>A *v ((\<parallel>x\<parallel>) *\<^sub>R sgn x)\<parallel>"
     by(simp add: scaleR_norm_sgn_eq)
   also have "... = (\<parallel>A *v sgn x\<parallel>) * (\<parallel>x\<parallel>)"
     by(simp add: vector_scaleR_commute)
   finally show ?thesis ..
 qed
 
 
 subsection\<open> Diagonalization \<close>
 
 lemma invertibleI: "A ** B = mat 1 \<Longrightarrow> B ** A = mat 1 \<Longrightarrow> invertible A"
   unfolding invertible_def by auto
 
 lemma invertibleD[simp]:
   assumes "invertible A" 
   shows "A\<^sup>-\<^sup>1 ** A = mat 1" and "A ** A\<^sup>-\<^sup>1 = mat 1"
   using assms unfolding matrix_inv_def invertible_def
   by (simp_all add: verit_sko_ex')
 
 lemma matrix_inv_unique:
   assumes "A ** B = mat 1" and "B ** A = mat 1"
   shows "A\<^sup>-\<^sup>1 = B"
   by (metis assms invertibleD(2) invertibleI matrix_mul_assoc matrix_mul_lid)
 
 lemma invertible_matrix_inv: "invertible A \<Longrightarrow> invertible (A\<^sup>-\<^sup>1)"
   using invertibleD invertibleI by blast
 
 lemma matrix_inv_idempotent[simp]: "invertible A \<Longrightarrow> A\<^sup>-\<^sup>1\<^sup>-\<^sup>1 = A"
   using invertibleD matrix_inv_unique by blast
   
 lemma matrix_inv_matrix_mul:
   assumes "invertible A" and "invertible B"
   shows "(A ** B)\<^sup>-\<^sup>1 = B\<^sup>-\<^sup>1 ** A\<^sup>-\<^sup>1"
 proof(rule matrix_inv_unique)
   have "A ** B ** (B\<^sup>-\<^sup>1 ** A\<^sup>-\<^sup>1) = A ** (B ** B\<^sup>-\<^sup>1) ** A\<^sup>-\<^sup>1"
     by (simp add: matrix_mul_assoc)
   also have "... = mat 1"
     using assms by simp
   finally show "A ** B ** (B\<^sup>-\<^sup>1 ** A\<^sup>-\<^sup>1) = mat 1" .
 next
   have "B\<^sup>-\<^sup>1 ** A\<^sup>-\<^sup>1 ** (A ** B) = B\<^sup>-\<^sup>1 ** (A\<^sup>-\<^sup>1 ** A) ** B"
     by (simp add: matrix_mul_assoc)
   also have "... = mat 1"
     using assms by simp
   finally show "B\<^sup>-\<^sup>1 ** A\<^sup>-\<^sup>1 ** (A ** B) = mat 1" .
 qed
 
 lemma mat_inverse_simps[simp]:
   fixes c :: "'a::division_ring"
   assumes "c \<noteq> 0"
   shows "mat (inverse c) ** mat c = mat 1" 
     and "mat c ** mat (inverse c) = mat 1"
   unfolding matrix_matrix_mult_def mat_def by (auto simp: vec_eq_iff assms)
 
 lemma matrix_inv_mat[simp]: "c \<noteq> 0 \<Longrightarrow> (mat c)\<^sup>-\<^sup>1 = mat (inverse c)" for c :: "'a::division_ring"
   by (simp add: matrix_inv_unique)
 
 lemma invertible_mat[simp]: "c \<noteq> 0 \<Longrightarrow> invertible (mat c)" for c :: "'a::division_ring"
   using invertibleI mat_inverse_simps(1) mat_inverse_simps(2) by blast
 
 lemma matrix_inv_mat_1: "(mat (1::'a::division_ring))\<^sup>-\<^sup>1 = mat 1"
   by simp
 
 lemma invertible_mat_1: "invertible (mat (1::'a::division_ring))"
   by simp
 
 definition similar_matrix :: "('a::semiring_1)^'m^'m \<Rightarrow> ('a::semiring_1)^'n^'n \<Rightarrow> bool" (infixr "\<sim>" 25)
   where "similar_matrix A B \<longleftrightarrow> (\<exists> P. invertible P \<and> A = P\<^sup>-\<^sup>1 ** B ** P)"
 
 lemma similar_matrix_refl[simp]: "A \<sim> A" for A :: "'a::division_ring^'n^'n"
   by (unfold similar_matrix_def, rule_tac x="mat 1" in exI, simp)
 
 lemma similar_matrix_simm: "A \<sim> B \<Longrightarrow> B \<sim> A" for A B :: "('a::semiring_1)^'n^'n"
   apply(unfold similar_matrix_def, clarsimp)
   apply(rule_tac x="P\<^sup>-\<^sup>1" in exI, simp add: invertible_matrix_inv)
   by (metis invertible_def matrix_inv_unique matrix_mul_assoc matrix_mul_lid matrix_mul_rid)
 
 lemma similar_matrix_trans: "A \<sim> B \<Longrightarrow> B \<sim> C \<Longrightarrow> A \<sim> C" for A B C :: "('a::semiring_1)^'n^'n"
 proof(unfold similar_matrix_def, clarsimp)
   fix P Q
   assume "A = P\<^sup>-\<^sup>1 ** (Q\<^sup>-\<^sup>1 ** C ** Q) ** P" and "B = Q\<^sup>-\<^sup>1 ** C ** Q"
   let ?R = "Q ** P"
   assume inverts: "invertible Q" "invertible P"
   hence "?R\<^sup>-\<^sup>1 = P\<^sup>-\<^sup>1 ** Q\<^sup>-\<^sup>1"
     by (rule matrix_inv_matrix_mul)
   also have "invertible ?R"
     using inverts invertible_mult by blast 
   ultimately show "\<exists>R. invertible R \<and> P\<^sup>-\<^sup>1 ** (Q\<^sup>-\<^sup>1 ** C ** Q) ** P = R\<^sup>-\<^sup>1 ** C ** R"
     by (metis matrix_mul_assoc)
 qed
 
 lemma mat_vec_nth_simps[simp]:
   "i = j \<Longrightarrow> mat c $ i $ j = c" 
   "i \<noteq> j \<Longrightarrow> mat c $ i $ j = 0"
   by (simp_all add: mat_def)
 
 definition "diag_mat f = (\<chi> i j. if i = j then f i else 0)"
 
 lemma diag_mat_vec_nth_simps[simp]:
   "i = j \<Longrightarrow> diag_mat f $ i $ j = f i"
   "i \<noteq> j \<Longrightarrow> diag_mat f $ i $ j = 0"
   unfolding diag_mat_def by simp_all
 
 lemma diag_mat_const_eq[simp]: "diag_mat (\<lambda>i. c) = mat c"
   unfolding mat_def diag_mat_def by simp
 
 lemma matrix_vector_mul_diag_mat: "diag_mat f *v s = (\<chi> i. f i * s$i)"
   unfolding diag_mat_def matrix_vector_mult_def by simp
 
 lemma matrix_vector_mul_diag_axis[simp]: "diag_mat f *v (axis i k) = axis i (f i * k)"
   by (simp add: matrix_vector_mul_diag_mat axis_def fun_eq_iff)
 
 lemma matrix_mul_diag_matl: "diag_mat f ** A = (\<chi> i j. f i * A$i$j)"
   unfolding diag_mat_def matrix_matrix_mult_def by simp
 
 lemma matrix_matrix_mul_diag_matr: "A ** diag_mat f = (\<chi> i j. A$i$j * f j)"
   unfolding diag_mat_def matrix_matrix_mult_def apply(clarsimp simp: fun_eq_iff)
   subgoal for i j 
     by (auto simp: finite_sum_univ_singleton[of _ j])
   done
 
 lemma matrix_mul_diag_diag: "diag_mat f ** diag_mat g = diag_mat (\<lambda>i. f i * g i)"
   unfolding diag_mat_def matrix_matrix_mult_def vec_eq_iff by simp
 
 lemma compow_matrix_mul_diag_mat_eq: "((**) (diag_mat f) ^^ n) (mat 1) = diag_mat (\<lambda>i. f i^n)"
   apply(induct n, simp_all add: matrix_mul_diag_matl)
   by (auto simp: vec_eq_iff diag_mat_def)
 
 lemma compow_similar_diag_mat_eq:
   assumes "invertible P" 
       and "A = P\<^sup>-\<^sup>1 ** (diag_mat f) ** P"
     shows "((**) A ^^ n) (mat 1) = P\<^sup>-\<^sup>1 ** (diag_mat (\<lambda>i. f i^n)) ** P"
 proof(induct n, simp_all add: assms)
   fix n::nat
   have "P\<^sup>-\<^sup>1 ** diag_mat f ** P ** (P\<^sup>-\<^sup>1 ** diag_mat (\<lambda>i. f i ^ n) ** P) = 
   P\<^sup>-\<^sup>1 ** diag_mat f ** diag_mat (\<lambda>i. f i ^ n) ** P" (is "?lhs = _")
     by (metis (no_types, lifting) assms(1) invertibleD(2) matrix_mul_rid matrix_mul_assoc) 
   also have "... = P\<^sup>-\<^sup>1 ** diag_mat (\<lambda>i. f i * f i ^ n) ** P" (is "_ = ?rhs")
     by (metis (full_types) matrix_mul_assoc matrix_mul_diag_diag)
   finally show "?lhs = ?rhs" .
 qed
 
 lemma compow_similar_diag_mat:
   assumes "A \<sim> (diag_mat f)"
   shows "((**) A ^^ n) (mat 1) \<sim> diag_mat (\<lambda>i. f i^n)"
 proof(unfold similar_matrix_def)
   obtain P where "invertible P" and "A = P\<^sup>-\<^sup>1 ** (diag_mat f) ** P"
     using assms unfolding similar_matrix_def by blast
   thus "\<exists>P. invertible P \<and> ((**) A ^^ n) (mat 1) = P\<^sup>-\<^sup>1 ** diag_mat (\<lambda>i. f i ^ n) ** P"
     using compow_similar_diag_mat_eq by blast
 qed
 
 no_notation matrix_inv ("_\<^sup>-\<^sup>1" [90])
         and similar_matrix (infixr "\<sim>" 25)
 
 
 end
\ No newline at end of file