Theory Flow_Congs
theory Flow_Congs
imports Reachability_Analysis
begin
lemma lipschitz_on_congI:
assumes "L'-lipschitz_on s' g'"
assumes "s' = s"
assumes "L' ≤ L"
assumes "⋀x y. x ∈ s ⟹ g' x = g x"
shows "L-lipschitz_on s g"
using assms
by (auto simp: lipschitz_on_def intro!: order_trans[OF _ mult_right_mono[OF ‹L' ≤ L›]])
lemma local_lipschitz_congI:
assumes "local_lipschitz s' t' g'"
assumes "s' = s"
assumes "t' = t"
assumes "⋀x y. x ∈ s ⟹ y ∈ t ⟹ g' x y = g x y"
shows "local_lipschitz s t g"
proof -
from assms have "local_lipschitz s t g'"
by (auto simp: local_lipschitz_def)
then show ?thesis
apply (auto simp: local_lipschitz_def)
apply (drule_tac bspec, assumption)
apply (drule_tac bspec, assumption)
apply auto
subgoal for x y u L
apply (rule exI[where x=u])
apply (auto intro!: exI[where x=L])
apply (drule bspec)
apply simp
apply (rule lipschitz_on_congI, assumption, rule refl, rule order_refl)
using assms
apply (auto)
done
done
qed
context ll_on_open_it
begin
context fixes S Y g assumes cong: "X = Y" "T = S" "⋀x t. x ∈ Y ⟹ t ∈ S ⟹ f t x = g t x"
begin
lemma ll_on_open_congI: "ll_on_open S g Y"
proof -
interpret Y: ll_on_open_it S f Y t0
apply (subst cong(1)[symmetric])
apply (subst cong(2)[symmetric])
by unfold_locales
show ?thesis
apply standard
subgoal
using local_lipschitz
apply (rule local_lipschitz_congI)
using cong by simp_all
subgoal apply (subst continuous_on_cong) prefer 3 apply (rule cont)
using cong by (auto)
subgoal using open_domain by (auto simp: cong)
subgoal using open_domain by (auto simp: cong)
done
qed
lemma existence_ivl_subsetI:
assumes t: "t ∈ existence_ivl t0 x0"
shows "t ∈ ll_on_open.existence_ivl S g Y t0 x0"
proof -
from assms have ‹t0 ∈ T› "x0 ∈ X"
by (rule mem_existence_ivl_iv_defined)+
interpret Y: ll_on_open S g Y by (rule ll_on_open_congI)
have "(flow t0 x0 solves_ode f) (existence_ivl t0 x0) X"
by (rule flow_solves_ode) (auto simp: ‹x0 ∈ X› ‹t0 ∈ T›)
then have "(flow t0 x0 solves_ode f) {t0--t} X"
by (rule solves_ode_on_subset)
(auto simp add: t local.closed_segment_subset_existence_ivl)
then have "(flow t0 x0 solves_ode g) {t0--t} Y"
apply (rule solves_ode_congI)
apply (auto intro!: assms cong)
using ‹(flow t0 x0 solves_ode f) {t0--t} X› local.cong(1) solves_ode_domainD apply blast
using ‹t0 ∈ T› assms closed_segment_subset_domainI general.mem_existence_ivl_subset local.cong(2)
by blast
then show ?thesis
apply (rule Y.existence_ivl_maximal_segment)
subgoal by (simp add: ‹t0 ∈ T› ‹x0 ∈ X›)
apply (subst cong[symmetric])
using ‹t0 ∈ T› assms closed_segment_subset_domainI general.mem_existence_ivl_subset local.cong(2)
by blast
qed
lemma existence_ivl_cong:
shows "existence_ivl t0 x0 = ll_on_open.existence_ivl S g Y t0 x0"
proof -
interpret Y: ll_on_open S g Y by (rule ll_on_open_congI)
show ?thesis
apply (auto )
subgoal by (rule existence_ivl_subsetI)
subgoal
apply (rule Y.existence_ivl_subsetI)
using cong
by auto
done
qed
lemma flow_cong:
assumes "t ∈ existence_ivl t0 x0"
shows "flow t0 x0 t = ll_on_open.flow S g Y t0 x0 t"
proof -
interpret Y: ll_on_open S g Y by (rule ll_on_open_congI)
from assms have "t0 ∈ T" "x0 ∈ X"
by (rule mem_existence_ivl_iv_defined)+
from cong ‹x0 ∈ X› have "x0 ∈ Y" by auto
from cong ‹t0 ∈ T› have "t0 ∈ S" by auto
show ?thesis
apply (rule Y.equals_flowI[where T'="existence_ivl t0 x0"])
subgoal using ‹t0 ∈ T› ‹x0 ∈ X› by auto
subgoal using ‹x0 ∈ X› by auto
subgoal by (auto simp: existence_ivl_cong ‹x0 ∈ X›)
subgoal
apply (rule solves_ode_congI)
apply (rule flow_solves_ode[OF ‹t0 ∈ T› ‹x0 ∈ X›])
using existence_ivl_subset[of x0]
by (auto simp: cong(2)[symmetric] cong(1)[symmetric] assms flow_in_domain intro!: cong)
subgoal using ‹t0 ∈ S› ‹t0 ∈ T› ‹x0 ∈ X› ‹x0 ∈ Y›
by (auto simp:)
subgoal by fact
done
qed
end
end
context auto_ll_on_open begin
context fixes Y g assumes cong: "X = Y" "⋀x t. x ∈ Y ⟹ f x = g x"
begin
lemma auto_ll_on_open_congI: "auto_ll_on_open g Y"
apply unfold_locales
subgoal
using local_lipschitz
apply (rule local_lipschitz_congI)
using cong by auto
subgoal
using open_domain
using cong by auto
done
lemma existence_ivl0_cong:
shows "existence_ivl0 x0 = auto_ll_on_open.existence_ivl0 g Y x0"
proof -
interpret Y: auto_ll_on_open g Y by (rule auto_ll_on_open_congI)
show ?thesis
unfolding Y.existence_ivl0_def
apply (rule existence_ivl_cong)
using cong by auto
qed
lemma flow0_cong:
assumes "t ∈ existence_ivl0 x0"
shows "flow0 x0 t = auto_ll_on_open.flow0 g Y x0 t"
proof -
interpret Y: auto_ll_on_open g Y by (rule auto_ll_on_open_congI)
show ?thesis
unfolding Y.flow0_def
apply (rule flow_cong)
using cong assms by auto
qed
end
end
context c1_on_open_euclidean begin
context fixes Y g assumes cong: "X = Y" "⋀x t. x ∈ Y ⟹ f x = g x"
begin
lemma f'_cong: "(g has_derivative blinfun_apply (f' x)) (at x)" if "x ∈ Y"
proof -
from derivative_rhs[of x] that cong
have "(f has_derivative blinfun_apply (f' x)) (at x within Y)"
by (auto intro!: has_derivative_at_withinI)
then have "(g has_derivative blinfun_apply (f' x)) (at x within Y)"
by (rule has_derivative_transform_within[OF _ zero_less_one that])
(auto simp: cong)
then show ?thesis
using at_within_open[OF that] cong open_dom
by auto
qed
lemma c1_on_open_euclidean_congI: "c1_on_open_euclidean g f' Y"
proof -
interpret Y: c1_on_open_euclidean f f' Y unfolding cong[symmetric] by unfold_locales
show ?thesis
apply standard
subgoal using cong by simp
subgoal by (rule f'_cong)
subgoal by (simp add: cong[symmetric] continuous_derivative)
done
qed
lemma vareq_cong: "vareq x0 t = c1_on_open_euclidean.vareq g f' Y x0 t"
if "t ∈ existence_ivl0 x0"
proof -
interpret Y: c1_on_open_euclidean g f' Y by (rule c1_on_open_euclidean_congI)
show ?thesis
unfolding vareq_def Y.vareq_def
apply (rule arg_cong[where f=f'])
apply (rule flow0_cong)
using cong that by auto
qed
lemma Dflow_cong:
assumes "t ∈ existence_ivl0 x0"
shows "Dflow x0 t = c1_on_open_euclidean.Dflow g f' Y x0 t"
proof -
interpret Y: c1_on_open_euclidean g f' Y by (rule c1_on_open_euclidean_congI)
from assms have "x0 ∈ X"
by (rule mem_existence_ivl_iv_defined)
from cong ‹x0 ∈ X› have "x0 ∈ Y" by auto
show ?thesis
unfolding Dflow_def Y.Dflow_def
apply (rule mvar.equals_flowI[symmetric, OF _ _ order_refl])
subgoal using ‹x0 ∈ X› by auto
subgoal using ‹x0 ∈ X› by auto
subgoal
apply (rule solves_ode_congI)
apply (rule Y.mvar.flow_solves_ode)
prefer 3 apply (rule refl)
subgoal using ‹x0 ∈ X› ‹x0 ∈ Y› by auto
subgoal using ‹x0 ∈ X› ‹x0 ∈ Y› by auto
subgoal for t
apply (subst vareq_cong)
apply (subst (asm) Y.mvar_existence_ivl_eq_existence_ivl)
subgoal using ‹x0 ∈ Y› by simp
subgoal
using cong
by (subst (asm) existence_ivl0_cong[symmetric]) auto
subgoal using ‹x0 ∈ Y› by simp
done
subgoal using ‹x0 ∈ X› ‹x0 ∈ Y›
apply (subst mvar_existence_ivl_eq_existence_ivl)
subgoal by simp
apply (subst Y.mvar_existence_ivl_eq_existence_ivl)
subgoal by simp
using cong
by (subst existence_ivl0_cong[symmetric]) auto
subgoal by simp
done
subgoal using ‹x0 ∈ X› ‹x0 ∈ Y› by auto
subgoal
apply (subst mvar_existence_ivl_eq_existence_ivl)
apply auto
apply fact+
done
done
qed
lemma flowsto_congI1:
assumes "flowsto A B C D"
shows "c1_on_open_euclidean.flowsto g f' Y A B C D"
proof -
interpret Y: c1_on_open_euclidean g f' Y by (rule c1_on_open_euclidean_congI)
show ?thesis
using assms
unfolding flowsto_def Y.flowsto_def
apply (auto simp: existence_ivl0_cong[OF cong] flow0_cong[OF cong])
apply (drule bspec, assumption)
apply clarsimp
apply (rule bexI)
apply (rule conjI)
apply assumption
apply (subst flow0_cong[symmetric, OF cong])
apply auto
apply (subst existence_ivl0_cong[OF cong])
apply auto
apply (subst Dflow_cong[symmetric])
apply auto
apply (subst existence_ivl0_cong[OF cong])
apply auto
apply (drule bspec, assumption)
apply (subst flow0_cong[symmetric, OF cong])
apply auto
apply (subst existence_ivl0_cong[OF cong])
apply auto defer
apply (subst Dflow_cong[symmetric])
apply auto
apply (subst existence_ivl0_cong[OF cong])
apply auto
apply (drule Y.closed_segment_subset_existence_ivl;
auto simp: open_segment_eq_real_ivl closed_segment_eq_real_ivl split: if_splits)+
done
qed
lemma flowsto_congI2:
assumes "c1_on_open_euclidean.flowsto g f' Y A B C D"
shows "flowsto A B C D"
proof -
interpret Y: c1_on_open_euclidean g f' Y by (rule c1_on_open_euclidean_congI)
show ?thesis
apply (rule Y.flowsto_congI1)
using assms
by (auto simp: cong)
qed
lemma flowsto_congI: "flowsto A B C D = c1_on_open_euclidean.flowsto g f' Y A B C D"
using flowsto_congI1[of A B C D] flowsto_congI2[of A B C D] by auto
lemma
returns_to_congI1:
assumes "returns_to A x"
shows "auto_ll_on_open.returns_to g Y A x"
proof -
interpret Y: c1_on_open_euclidean g f' Y by (rule c1_on_open_euclidean_congI)
from assms obtain t where t:
"∀⇩F t in at_right 0. flow0 x t ∉ A"
"0 < t" "t ∈ existence_ivl0 x" "flow0 x t ∈ A"
by (auto simp: returns_to_def)
note t(1)
moreover
have "∀⇩F s in at_right 0. s < t"
using tendsto_ident_at ‹0 < t›
by (rule order_tendstoD)
moreover have "∀⇩F s in at_right 0. 0 < s"
by (auto simp: eventually_at_topological)
ultimately have "∀⇩F t in at_right 0. Y.flow0 x t ∉ A"
apply eventually_elim
using ivl_subset_existence_ivl[OF ‹t ∈ _›]
apply (subst (asm) flow0_cong[OF cong])
by auto
moreover have "∃t>0. t ∈ Y.existence_ivl0 x ∧ Y.flow0 x t ∈ A"
using t
by (auto intro!: exI[where x=t] simp: flow0_cong[OF cong] existence_ivl0_cong[OF cong])
ultimately show ?thesis
by (auto simp: Y.returns_to_def)
qed
lemma
returns_to_congI2:
assumes "auto_ll_on_open.returns_to g Y x A"
shows "returns_to x A"
proof -
interpret Y: c1_on_open_euclidean g f' Y by (rule c1_on_open_euclidean_congI)
show ?thesis
by (rule Y.returns_to_congI1) (auto simp: assms cong)
qed
lemma returns_to_cong: "auto_ll_on_open.returns_to g Y A x = returns_to A x"
using returns_to_congI1 returns_to_congI2 by blast
lemma
return_time_cong:
shows "return_time A x = auto_ll_on_open.return_time g Y A x"
proof -
interpret Y: c1_on_open_euclidean g f' Y by (rule c1_on_open_euclidean_congI)
have P_eq: "0 < t ∧ t ∈ existence_ivl0 x ∧ flow0 x t ∈ A ∧ (∀s∈{0<..<t}. flow0 x s ∉ A) ⟷
0 < t ∧ t ∈ Y.existence_ivl0 x ∧ Y.flow0 x t ∈ A ∧ (∀s∈{0<..<t}. Y.flow0 x s ∉ A)"
for t
using ivl_subset_existence_ivl[of t x]
apply (auto simp: existence_ivl0_cong[OF cong] flow0_cong[OF cong])
apply (drule bspec)
apply force
apply (subst (asm) flow0_cong[OF cong])
apply auto
apply (auto simp: existence_ivl0_cong[OF cong, symmetric] flow0_cong[OF cong])
apply (subst (asm) flow0_cong[OF cong])
apply auto
done
show ?thesis
unfolding return_time_def Y.return_time_def
by (auto simp: returns_to_cong P_eq)
qed
lemma poincare_mapsto_congI1:
assumes "poincare_mapsto A B C D E" "closed A"
shows "c1_on_open_euclidean.poincare_mapsto g Y A B C D E"
proof -
interpret Y: c1_on_open_euclidean g f' Y by (rule c1_on_open_euclidean_congI)
show ?thesis
using assms
unfolding poincare_mapsto_def Y.poincare_mapsto_def
apply auto
subgoal for a b
by (rule returns_to_congI1) auto
subgoal for a b
by (subst return_time_cong[abs_def, symmetric]) auto
subgoal for a b
unfolding poincare_map_def Y.poincare_map_def
apply (drule bspec, assumption)
apply safe
subgoal for D
apply (auto intro!: exI[where x=D])
subgoal premises prems
proof -
have "∀⇩F y in at a within C. returns_to A y"
apply (rule eventually_returns_to_continuousI)
apply fact apply fact
apply (rule differentiable_imp_continuous_within)
apply fact
done
moreover have "∀⇩F y in at a within C. y ∈ C"
by (auto simp: eventually_at_filter)
ultimately have "∀⇩F x' in at a within C. flow0 x' (return_time A x') = Y.flow0 x' (Y.return_time A x')"
proof eventually_elim
case (elim x')
then show ?case
apply (subst flow0_cong[OF cong, symmetric], force)
apply (subst return_time_cong[symmetric])
using prems
apply (auto intro!: return_time_exivl)
apply (subst return_time_cong[symmetric])
apply auto
done
qed
with prems(7)
show ?thesis
apply (rule has_derivative_transform_eventually)
using prems
apply (subst flow0_cong[OF cong, symmetric], force)
apply (subst return_time_cong[symmetric])
using prems
apply (auto intro!: return_time_exivl)
apply (subst return_time_cong[symmetric])
apply auto
done
qed
subgoal
apply (subst flow0_cong[OF cong, symmetric], force)
apply (subst return_time_cong[symmetric])
apply (auto intro!: return_time_exivl)
apply (subst return_time_cong[symmetric])
apply auto
done
done
done
subgoal for a b t
apply (drule bspec, assumption)
apply (subst flow0_cong[OF cong, symmetric])
apply auto
apply (subst (asm) return_time_cong[symmetric])
apply (rule less_return_time_imp_exivl)
apply (rule less_imp_le, assumption)
apply (auto simp: return_time_cong)
done
done
qed
lemma poincare_mapsto_congI2:
assumes "c1_on_open_euclidean.poincare_mapsto g Y A B C D E" "closed A"
shows "poincare_mapsto A B C D E"
proof -
interpret Y: c1_on_open_euclidean g f' Y by (rule c1_on_open_euclidean_congI)
show ?thesis
apply (rule Y.poincare_mapsto_congI1)
using assms
by (auto simp: cong)
qed
lemma poincare_mapsto_cong: "closed A ⟹
poincare_mapsto A B C D E = c1_on_open_euclidean.poincare_mapsto g Y A B C D E"
using poincare_mapsto_congI1[of A B C] poincare_mapsto_congI2[of A B C] by auto
end
end
end