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,317 +1,308 @@ (* Title: Preliminaries for hybrid systems verification Author: Jonathan Julián Huerta y Munive, 2019 Maintainer: Jonathan Julián Huerta y Munive *) section \ Hybrid Systems Preliminaries \ text \Hybrid systems combine continuous dynamics with discrete control. This section contains auxiliary lemmas for verification of hybrid systems.\ theory HS_Preliminaries imports "Ordinary_Differential_Equations.Picard_Lindeloef_Qualitative" begin subsection \ Real numbers \ lemma abs_le_eq: shows "(r::real) > 0 \ (\x\ < r) = (-r < x \ x < r)" and "(r::real) > 0 \ (\x\ \ r) = (-r \ x \ x \ 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<--2 + (x * sin t + y * cos t)\<^sup>2 = x\<^sup>2 + y\<^sup>2" and "(x * cos t + y * sin t)\<^sup>2 + (y * cos t - x * sin t)\<^sup>2 = x\<^sup>2 + y\<^sup>2" proof- have "(x * cos t - y * sin t)\<^sup>2 = x\<^sup>2 * (cos t)\<^sup>2 + y\<^sup>2 * (sin t)\<^sup>2 - 2 * (x * cos t) * (y * sin t)" by(simp add: power2_diff power_mult_distrib) also have "(x * sin t + y * cos t)\<^sup>2 = y\<^sup>2 * (cos t)\<^sup>2 + x\<^sup>2 * (sin t)\<^sup>2 + 2 * (x * cos t) * (y * sin t)" by(simp add: power2_sum power_mult_distrib) ultimately show "(x * cos t - y * sin t)\<^sup>2 + (x * sin t + y * cos t)\<^sup>2 = x\<^sup>2 + y\<^sup>2" by (simp add: Groups.mult_ac(2) Groups.mult_ac(3) right_diff_distrib sin_squared_eq) thus "(x * cos t + y * sin t)\<^sup>2 + (y * cos t - x * sin t)\<^sup>2 = x\<^sup>2 + y\<^sup>2" by (simp add: add.commute add.left_commute power2_diff power2_sum) qed subsection \ Single variable derivatives \ notation has_derivative ("(1(D _ \ (_))/ _)" [65,65] 61) notation has_vderiv_on ("(1 D _ = (_)/ on _)" [65,65] 61) notation norm ("(1\_\)" [65] 61) thy_deps named_theorems poly_derivatives "compilation of optimised miscellaneous derivative rules." declare has_vderiv_on_const [poly_derivatives] and has_vderiv_on_id [poly_derivatives] and has_vderiv_on_add[THEN has_vderiv_on_eq_rhs, poly_derivatives] and has_vderiv_on_diff[THEN has_vderiv_on_eq_rhs, poly_derivatives] and has_vderiv_on_mult[THEN has_vderiv_on_eq_rhs, poly_derivatives] lemma has_vderiv_on_compose_eq: assumes "D f = f' on g ` T" and " D g = g' on T" and "h = (\x. g' x *\<^sub>R f' (g x))" shows "D (\t. f (g t)) = h on T" apply(subst ssubst[of h], simp) using assms has_vderiv_on_compose by auto lemma vderiv_on_compose_add [derivative_intros]: assumes "D x = x' on (\\. \ + t) ` T" shows "D (\\. x (\ + t)) = (\\. x' (\ + t)) on T" apply(rule has_vderiv_on_compose_eq[OF assms]) by(auto intro: derivative_intros) lemma has_vderiv_on_divide_cnst: "a \ 0 \ D (\t. t/a) = (\t. 1/a) on T" unfolding has_vderiv_on_def has_vector_derivative_def apply clarify apply(rule_tac f'1="\t. t" and g'1="\ x. 0" in has_derivative_divide[THEN has_derivative_eq_rhs]) by(auto intro: derivative_eq_intros) lemma has_vderiv_on_power: "n \ 1 \ D (\t. t ^ n) = (\t. n * (t ^ (n - 1))) on T" unfolding has_vderiv_on_def has_vector_derivative_def by (auto intro!: derivative_eq_intros) lemma has_vderiv_on_exp: "D (\t. exp t) = (\t. exp t) on T" unfolding has_vderiv_on_def has_vector_derivative_def by (auto intro: derivative_intros) lemma has_vderiv_on_cos_comp: "D (f::real \ real) = f' on T \ D (\t. cos (f t)) = (\t. - (f' t) * sin (f t)) on T" apply(rule has_vderiv_on_compose_eq[of "\t. cos t"]) unfolding has_vderiv_on_def has_vector_derivative_def apply clarify by(auto intro!: derivative_eq_intros simp: fun_eq_iff) lemma has_vderiv_on_sin_comp: "D (f::real \ real) = f' on T \ D (\t. sin (f t)) = (\t. (f' t) * cos (f t)) on T" apply(rule has_vderiv_on_compose_eq[of "\t. sin t"]) unfolding has_vderiv_on_def has_vector_derivative_def apply clarify by(auto intro!: derivative_eq_intros simp: fun_eq_iff) lemma has_vderiv_on_exp_comp: "D (f::real \ real) = f' on T \ D (\t. exp (f t)) = (\t. (f' t) * exp (f t)) on T" apply(rule has_vderiv_on_compose_eq[of "\t. exp t"]) by (rule has_vderiv_on_exp, simp_all add: mult.commute) lemma vderiv_uminus_intro [poly_derivatives]: "D f = f' on T \ g = (\t. - f' t) \ D (\t. - f t) = g on T" using has_vderiv_on_uminus by auto lemma vderiv_div_cnst_intro [poly_derivatives]: assumes "(a::real) \ 0" and "D f = f' on T" and "g = (\t. (f' t)/a)" shows "D (\t. (f t)/a) = g on T" apply(rule has_vderiv_on_compose_eq[of "\t. t/a" "\t. 1/a"]) using assms by(auto intro: has_vderiv_on_divide_cnst) lemma vderiv_npow_intro [poly_derivatives]: fixes f::"real \ real" assumes "n \ 1" and "D f = f' on T" and "g = (\t. n * (f' t) * (f t)^(n-1))" shows "D (\t. (f t)^n) = g on T" apply(rule has_vderiv_on_compose_eq[of "\t. t^n"]) using assms(1) apply(rule has_vderiv_on_power) using assms by auto lemma vderiv_cos_intro [poly_derivatives]: assumes "D (f::real \ real) = f' on T" and "g = (\t. - (f' t) * sin (f t))" shows "D (\t. cos (f t)) = g on T" using assms and has_vderiv_on_cos_comp by auto lemma vderiv_sin_intro [poly_derivatives]: assumes "D (f::real \ real) = f' on T" and "g = (\t. (f' t) * cos (f t))" shows "D (\t. sin (f t)) = g on T" using assms and has_vderiv_on_sin_comp by auto lemma vderiv_exp_intro [poly_derivatives]: assumes "D (f::real \ real) = f' on T" and "g = (\t. (f' t) * exp (f t))" shows "D (\t. exp (f t)) = g on T" using assms and has_vderiv_on_exp_comp by auto \ \Examples for checking derivatives\ lemma "D (\t. a * t\<^sup>2 / 2 + v * t + x) = (\t. a * t + v) on T" by(auto intro!: poly_derivatives) lemma "D (\t. v * t - a * t\<^sup>2 / 2 + x) = (\x. v - a * x) on T" by(auto intro!: poly_derivatives) lemma "c \ 0 \ D (\t. a5 * t^5 + a3 * (t^3 / c) - a2 * exp (t^2) + a1 * cos t + a0) = (\t. 5 * a5 * t^4 + 3 * a3 * (t^2 / c) - 2 * a2 * t * exp (t^2) - a1 * sin t) on T" by(auto intro!: poly_derivatives) lemma "c \ 0 \ D (\t. - a3 * exp (t^3 / c) + a1 * sin t + a2 * t^2) = (\t. a1 * cos t + 2 * a2 * t - 3 * a3 * t^2 / c * exp (t^3 / c)) on T" apply(intro poly_derivatives) using poly_derivatives(1,2) by force+ lemma "c \ 0 \ D (\t. exp (a * sin (cos (t^4) / c))) = (\t. - 4 * a * t^3 * sin (t^4) / c * cos (cos (t^4) / c) * exp (a * sin (cos (t^4) / c))) on T" apply(intro poly_derivatives) using poly_derivatives(1,2) by force+ subsection \ Filters \ lemma eventually_at_within_mono: assumes "t \ interior T" and "T \ 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 \ interior T" and "T \ S" shows "netlimit (at t within S) = t" using assms(1) interior_mono[OF \T \ S\] netlimit_within_interior by auto lemma has_derivative_at_within_mono: assumes "(t::real) \ interior T" and "T \ S" and "D f \ f' at t within T" shows "D f \ 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) \ 'b \ bool" assumes h:"\i. eventually (P i) F" shows "eventually (\x. \i. P i x) F" proof(unfold eventually_def) let ?F = "Rep_filter F" have obs: "\i. ?F (P i)" using h by auto have "?F (\x. \i \ UNIV. P i x)" apply(rule finite_induct) by(auto intro: eventually_conj simp: obs h) thus "?F (\x. \i. P i x)" by simp qed lemma eventually_all_finite_mono: fixes P :: "('a::finite) \ 'b \ bool" assumes h1: "\i. eventually (P i) F" and h2: "\x. (\i. (P i x)) \ Q x" shows "eventually Q F" proof- have "eventually (\x. \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 \ Multivariable derivatives \ lemma frechet_vec_lambda: fixes f::"real \ ('a::banach)^('m::finite)" and x::real and T::"real set" defines "x\<^sub>0 \ netlimit (at x within T)" and "m \ real CARD('m)" assumes "\i. ((\y. (f y \$ i - f x\<^sub>0 \$ i - (y - x\<^sub>0) *\<^sub>R f' x \$ i) /\<^sub>R (\y - x\<^sub>0\)) \ 0) (at x within T)" shows "((\y. (f y - f x\<^sub>0 - (y - x\<^sub>0) *\<^sub>R f' x) /\<^sub>R (\y - x\<^sub>0\)) \ 0) (at x within T)" proof(simp add: tendsto_iff, clarify) fix \::real assume "0 < \" let "?\" = "\y. y - x\<^sub>0" and "?\f" = "\y. f y - f x\<^sub>0" let "?P" = "\i e y. inverse \?\ y\ * (\f y \$ i - f x\<^sub>0 \$ i - ?\ y *\<^sub>R f' x \$ i\) < e" and "?Q" = "\y. inverse \?\ y\ * (\?\f y - ?\ y *\<^sub>R f' x\) < \" have "0 < \ / sqrt m" using \0 < \\ by (auto simp: assms) hence "\i. eventually (\y. ?P i (\ / 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 \t - x\<^sub>0\" and "?u t" = "\i. f t \$ i - f x\<^sub>0 \$ i - ?\ t *\<^sub>R f' x \$ i" assume hyp:"\i. ?c * (\?u t i\) < \ / sqrt m" hence "\i. (?c *\<^sub>R (\?u t i\))\<^sup>2 < (\ / sqrt m)\<^sup>2" by (simp add: power_strict_mono) hence "\i. ?c\<^sup>2 * ((\?u t i\))\<^sup>2 < \\<^sup>2 / m" by (simp add: power_mult_distrib power_divide assms) hence "\i. ?c\<^sup>2 * ((\?u t i\))\<^sup>2 < \\<^sup>2 / m" by (auto simp: assms) also have "({}::'m set) \ UNIV \ finite (UNIV :: 'm set)" by simp ultimately have "(\i\UNIV. ?c\<^sup>2 * ((\?u t i\))\<^sup>2) < (\(i::'m)\UNIV. \\<^sup>2 / m)" by (metis (lifting) sum_strict_mono) moreover have "?c\<^sup>2 * (\i\UNIV. (\?u t i\)\<^sup>2) = (\i\UNIV. ?c\<^sup>2 * (\?u t i\)\<^sup>2)" using sum_distrib_left by blast ultimately have "?c\<^sup>2 * (\i\UNIV. (\?u t i\)\<^sup>2) < \\<^sup>2" by (simp add: assms) hence "sqrt (?c\<^sup>2 * (\i\UNIV. (\?u t i\)\<^sup>2)) < sqrt (\\<^sup>2)" using real_sqrt_less_iff by blast also have "... = \" using \0 < \\ by auto moreover have "?c * sqrt (\i\UNIV. (\?u t i\)\<^sup>2) = sqrt (?c\<^sup>2 * (\i\UNIV. (\?u t i\)\<^sup>2))" by (simp add: real_sqrt_mult) ultimately show "?c * sqrt (\i\UNIV. (\?u t i\)\<^sup>2) < \" by simp qed qed +lemma tendsto_norm_bound: + "\x. \G x - L\ \ \F x - L\ \ (F \ L) net \ (G \ L) net" + apply(unfold tendsto_iff dist_norm, clarsimp) + apply(rule_tac P="\x. \F x - L\ < e" in eventually_mono, simp) + by (rename_tac e z) (erule_tac x=z in allE, simp) + +lemma tendsto_zero_norm_bound: + "\x. \G x\ \ \F x\ \ (F \ 0) net \ (G \ 0) net" + apply(unfold tendsto_iff dist_norm, clarsimp) + apply(rule_tac P="\x. \F x\ < e" in eventually_mono, simp) + by (rename_tac e z) (erule_tac x=z in allE, simp) + lemma frechet_vec_nth: - fixes f::"real \ ('a::real_normed_vector)^'m" and x::real and T::"real set" - defines "x\<^sub>0 \ netlimit (at x within T)" - assumes "((\y. (f y - f x\<^sub>0 - (y - x\<^sub>0) *\<^sub>R f' x) /\<^sub>R (\y - x\<^sub>0\)) \ 0) (at x within T)" - shows "((\y. (f y \$ i - f x\<^sub>0 \$ i - (y - x\<^sub>0) *\<^sub>R f' x \$ i) /\<^sub>R (\y - x\<^sub>0\)) \ 0) (at x within T)" -proof(unfold tendsto_iff dist_norm, clarify) - let "?\" = "\y. y - x\<^sub>0" and "?\f" = "\y. f y - f x\<^sub>0" - fix \::real assume "0 < \" - let "?P" = "\y. \(?\f y - ?\ y *\<^sub>R f' x) /\<^sub>R (\?\ y\) - 0\ < \" - and "?Q" = "\y. \(f y \$ i - f x\<^sub>0 \$ i - ?\ y *\<^sub>R f' x \$ i) /\<^sub>R (\?\ y\) - 0\ < \" - have "eventually ?P (at x within T)" - using \0 < \\ assms unfolding tendsto_iff by auto - thus "eventually ?Q (at x within T)" - proof(rule_tac P="?P" in eventually_mono, simp_all) - fix y - let "?u i" = "f y \$ i - f x\<^sub>0 \$ i - ?\ y *\<^sub>R f' x \$ i" - assume hyp:"inverse \?\ y\ * (\?\f y - ?\ y *\<^sub>R f' x\) < \" - have "\(?\f y - ?\ y *\<^sub>R f' x) \$ i\ \ \?\f y - ?\ y *\<^sub>R f' x\" - using Finite_Cartesian_Product.norm_nth_le by blast - also have "\?u i\ = \(?\f y - ?\ y *\<^sub>R f' x) \$ i\" - by simp - ultimately have "\?u i\ \ \?\f y - ?\ y *\<^sub>R f' x\" - by linarith - hence "inverse \?\ y\ * (\?u i\) \ inverse \?\ y\ * (\?\f y - ?\ y *\<^sub>R f' x\)" - by (simp add: mult_left_mono) - thus "inverse \?\ y\ * (\f y \$ i - f x\<^sub>0 \$ i - ?\ y *\<^sub>R f' x \$ i\) < \" - using hyp by linarith - qed -qed + fixes f::"real \ ('a::real_normed_vector)^'m" + assumes "((\x. (f x - f x\<^sub>0 - (x - x\<^sub>0) *\<^sub>R f' t) /\<^sub>R (\x - x\<^sub>0\)) \ 0) (at t within T)" + shows "((\x. (f x \$ i - f x\<^sub>0 \$ i - (x - x\<^sub>0) *\<^sub>R f' t \$ i) /\<^sub>R (\x - x\<^sub>0\)) \ 0) (at t within T)" + apply(rule_tac F="(\x. (f x - f x\<^sub>0 - (x - x\<^sub>0) *\<^sub>R f' t) /\<^sub>R (\x - x\<^sub>0\))" in tendsto_zero_norm_bound) + apply(clarsimp, rule mult_left_mono) + apply (metis norm_nth_le vector_minus_component vector_scaleR_component) + using assms by simp_all lemma has_derivative_vec_lambda: fixes f::"real \ ('a::banach)^('n::finite)" assumes "\i. D (\t. f t \$ i) \ (\ h. h *\<^sub>R f' x \$ i) (at x within T)" shows "D f \ (\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 \ (\h. h *\<^sub>R f' x) at x within T" shows "D (\t. f t \$ i) \ (\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[of x T f] assms unfolding has_derivative_def by auto + using frechet_vec_nth assms unfolding has_derivative_def by auto lemma has_vderiv_on_vec_eq[simp]: fixes x::"real \ ('a::banach)^('n::finite)" shows "(D x = x' on T) = (\i. D (\t. x t \$ i) = (\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