Theory Poincare_Bendixson.ODE_Misc

section ‹Additions to the ODE Library›
theory ODE_Misc
  imports
    Ordinary_Differential_Equations.ODE_Analysis
    Analysis_Misc
begin

lemma local_lipschitz_compact_bicomposeE:
  assumes ll: "local_lipschitz T X f"
  assumes cf: "x. x  X  continuous_on I (λt. f t x)"
  assumes cI: "compact I"
  assumes "I  T"
  assumes cv: "continuous_on I v"
  assumes cw: "continuous_on I w"
  assumes v: "v ` I  X"
  assumes w: "w ` I  X"
  obtains L where "L > 0" "x. x  I  dist (f x (v x)) (f x (w x))  L * dist (v x) (w x)"
proof -
  from v w have "v ` I  w ` I  X" by auto
  with ll I  T have llI:"local_lipschitz I (v ` I  w ` I) f"
    by (rule local_lipschitz_subset)
  have cvwI: "compact (v ` I  w ` I)"
    by (auto intro!: compact_continuous_image cv cw cI)    

  from local_lipschitz_compact_implies_lipschitz[OF llI cvwI compact I cf]
  obtain L where L: "t. t  I  L-lipschitz_on (v ` I  w ` I) (f t)"
    using v w
    by blast
  define L' where "L' = max L 1"
  with L have "L' > 0" "x. x  I  dist (f x (v x)) (f x (w x))  L' * dist (v x) (w x)"
     apply (auto simp: lipschitz_on_def L'_def)
    by (smt Un_iff image_eqI mult_right_mono zero_le_dist)
  then show ?thesis ..
qed

subsection ‹Comparison Principle›

lemma comparison_principle_le:
  fixes f::"real  real  real"
    and φ ψ::"real  real"
  assumes ll: "local_lipschitz X Y f"
  assumes cf: "x. x  Y  continuous_on {a..b} (λt. f t x)"
  assumes abX: "{a .. b}  X"
  assumes φ': "x. x  {a .. b}  (φ has_real_derivative φ' x) (at x)"
  assumes ψ': "x. x  {a .. b}  (ψ has_real_derivative ψ' x) (at x)"
  assumes φ_in: "φ ` {a..b}  Y"
  assumes ψ_in: "ψ ` {a..b}  Y"
  assumes init: "φ a  ψ a"
  assumes defect: "x. x  {a .. b}  φ' x - f x (φ x)  ψ' x - f x (ψ x)"
  shows "x  {a .. b}. φ x  ψ x" (is "?th1")
    (*
    "(∀x ∈ {a .. b}. φ x < ψ x) ∨ (∃c∈{a..b}. (∀x∈{a..c}. φ x ≤ ψ x) ∧ (∀x∈{c<..b}. φ x < ψ x))"
    (is "?th2")
*)
  unfolding atomize_conj
  apply (cases "a  b")
   defer subgoal by simp
proof -
  assume "a  b"
  note φ_cont = has_real_derivative_imp_continuous_on[OF φ']
  note ψ_cont = has_real_derivative_imp_continuous_on[OF ψ']
  from local_lipschitz_compact_bicomposeE[OF ll cf compact_Icc abX φ_cont ψ_cont φ_in ψ_in]
  obtain L where L: "L > 0" "x. x  {a..b}  dist (f x (φ x)) (f x (ψ x))  L * dist (φ x) (ψ x)" by blast
  define w where "w x = ψ x - φ x" for x

  have w'[derivative_intros]: "x. x  {a .. b}  (w has_real_derivative ψ' x - φ' x) (at x)"
    using φ' ψ'
    by (auto simp: has_vderiv_on_def w_def[abs_def] intro!: derivative_eq_intros)
  note w_cont[continuous_intros] = has_real_derivative_imp_continuous_on[OF w', THEN continuous_on_compose2]
  have "w d  0" if "d  {a .. b}" for d
  proof (rule ccontr, unfold not_le)
    assume "w d < 0"
    let ?N = "(w -` {..0}  {a .. d})"
    from w d < 0 that have "d  ?N" by auto
    then have "?N  {}" by auto
    have "closed ?N"
      unfolding compact_eq_bounded_closed
      using that
      by (intro conjI closed_vimage_Int) (auto intro!: continuous_intros)

    let ?N' = "{a0  {a .. d}. w ` {a0 .. d}  {..0}}"
    from w d < 0 that have "d  ?N'" by simp
    then have "?N'  {}" by auto
    have "compact ?N'"
      unfolding compact_eq_bounded_closed
    proof
      have "?N'  {a .. d}" using that by auto
      then show "bounded ?N'"
        by (rule bounded_subset[rotated]) simp
      have "w u  0" if "(n. x n  ?N')" "x  l" "l  u" "u  d" for x l u
      proof cases
        assume "l = u"
        have "n. x n  ?N" using that(1) by force
        from closed_sequentially[OF closed ?N] this x  l
        show ?thesis
          using l = u by blast
      next
        assume "l  u" with that have "l < u" by auto
        from order_tendstoD(2)[OF x  l l < u] obtain n where "x n < u"
          by (auto dest: eventually_happens)
        with that show ?thesis using l < u
          by (auto dest!: spec[where x=n] simp: image_subset_iff)
      qed
      then show "closed ?N'"
        unfolding closed_sequential_limits
        by (auto simp: Lim_bounded Lim_bounded2)
    qed

    from compact_attains_inf[OF compact ?N' ?N'  {}]
    obtain a0 where a0: "a  a0" "a0  d" "w ` {a0..d}  {..0}"
      and a0_least: "x. a  x  x  d  w ` {x..d}  {..0}  a0  x"
      by auto
    have a0d: "{a0 .. d}  {a .. b}" using that a0
      by auto
    have L_w_bound: "L * w x  ψ' x - φ' x" if "x  {a0 .. d}" for x
    proof -
      from set_mp[OF a0d that] have "x  {a .. b}" .
      from defect[OF this]
      have "φ' x - ψ' x  dist (f x (φ x)) (f x (ψ x))"
        by (simp add: dist_real_def)
      also have "  L * dist (φ x) (ψ x)"
        using x  {a .. b}
        by (rule L)
      also have "  -L * w x"
        using 0 < L a0 that
        by (force simp add: dist_real_def abs_real_def w_def algebra_split_simps )
      finally show ?thesis
        by simp
    qed
    have mono: "mono_on {a0..d} (λx. w x * exp(-L*x))"
      apply (rule mono_onI)
      apply (rule DERIV_nonneg_imp_nondecreasing, assumption)
      using a0d
      by (auto intro!: exI[where x="(ψ' x - φ' x) * exp (- (L * x)) - exp (- (L * x)) * L * w x" for x]
          derivative_eq_intros L_w_bound simp: )
    then have "w a0 * exp (-L * a0)  w d * exp (-L * d)"
      by (rule mono_onD) (use that a0 in auto)
    also have " < 0" using w d < 0 by (simp add: algebra_split_simps)
    finally have "w a0 * exp (- L * a0) < 0" .
    then have "w a0 < 0" by (simp add: algebra_split_simps)
    have "a0  a"
    proof (rule ccontr, unfold not_le)
      assume "a < a0"
      have "continuous_on {a.. a0} w"
        by (rule continuous_intros, assumption) (use a0 a0d in auto)
      from continuous_on_Icc_at_leftD[OF this a < a0]
      have "(w  w a0) (at_left a0)" .
      from order_tendstoD(2)[OF this w a0 < 0] have "F x in at_left a0. w x < 0" .
      moreover have "F x in at_left a0. a < x"
        by (rule order_tendstoD) (auto intro!: a < a0)
      ultimately have "F x in at_left a0. a < x  w x < 0" by eventually_elim auto
      then obtain a1' where "a1'<a0" and a1_neg: "y. y > a1'  y < a0  a < y  w y < 0"
        unfolding eventually_at_left_field by auto
      define a1 where "a1 = (a1' + a0)/2"
      have "a1 < a0" using a1' < a0 by (auto simp: a1_def)
      have "a  a1"
        using a < a0 a1_neg by (force simp: a1_def)
      moreover have "a1  d"
        using a1' < a0 a0(2) by (auto simp: a1_def)
      moreover have "w ` {a1..a0}  {..0}"
        using w a0 < 0 a1_neg a0(3)
        by (auto simp: a1_def) smt
      moreover have "w ` {a0..d}  {..0}" using a0 by auto
      ultimately
      have "a0  a1"
        apply (intro a0_least) apply assumption apply assumption
        by (smt atLeastAtMost_iff image_subset_iff)
      with a1<a0 show False by simp
    qed
    then have "a0 = a" using a  a0 by simp
    with w a0 < 0 have "w a < 0" by simp
    with init show False
      by (auto simp: w_def)
  qed
  then show ?thesis
    by (auto simp: w_def)
qed

lemma local_lipschitz_mult:
  shows "local_lipschitz  (UNIV::real set) (UNIV::real set) (*)"
  apply (auto intro!: c1_implies_local_lipschitz[where f'="λp. blinfun_mult_left (fst p)"])
   apply (simp add: has_derivative_mult_right mult_commute_abs)
  by (auto intro!: continuous_intros)

lemma comparison_principle_le_linear:
  fixes φ :: "real  real"
  assumes "continuous_on {a..b} g"
  assumes "(t. t  {a..b}  (φ has_real_derivative φ' t) (at t))"
  assumes "φ a  0"
  assumes "(t. t  {a..b}  φ' t  g t *R φ t)"
  shows "t{a..b}. φ t  0"
proof -
  have *: "x. continuous_on {a..b} (λt. g t * x)"
    using assms(1) continuous_on_mult_right by blast
  then have "local_lipschitz (g`{a..b}) UNIV (*)"
    using local_lipschitz_subset[OF local_lipschitz_mult] by blast 
  from local_lipschitz_compose1[OF this assms(1)]
  have "local_lipschitz {a..b} UNIV (λt. (*) (g t))" .
  from comparison_principle_le[OF this _ _ assms(2) _ _ _ assms(3), of b "λt.0"] * assms(4)
  show ?thesis by auto
qed

subsection ‹Locally Lipschitz ODEs›

context ll_on_open_it begin

lemma flow_lipschitzE:
  assumes "{a .. b}  existence_ivl t0 x"
  obtains L where "L-lipschitz_on {a .. b} (flow t0 x)"
proof -
  have f': "(flow t0 x has_derivative (λi. i *R f t (flow t0 x t))) (at t within {a .. b})" if "t  {a .. b}" for t
    using flow_has_derivative[of t x] assms that
    by (auto simp: has_derivative_at_withinI)

  have "compact ((λt. f t (flow t0 x t)) ` {a .. b})"
    using assms
    apply (auto intro!: compact_continuous_image continuous_intros)
    using local.existence_ivl_empty2 apply fastforce
     apply (meson atLeastAtMost_iff general.existence_ivl_subset in_mono)
    by (simp add: general.flow_in_domain subset_iff)
  then obtain C where "t  {a .. b}  norm (f t (flow t0 x t))  C" for t
    by (fastforce dest!: compact_imp_bounded simp: bounded_iff intro: that)
  then have "t  {a..b}  onorm (λi. i *R f t (flow t0 x t))  max 0 C" for t
    apply (subst onorm_scaleR_left) 
     apply (auto simp: onorm_id max_def)
    by (metis diff_0_right diff_mono diff_self norm_ge_zero)
  from bounded_derivative_imp_lipschitz[OF f' _ this]
  have "(max 0 C)-lipschitz_on {a..b} (flow t0 x)"
    by auto
  then show ?thesis ..
qed

lemma flow_undefined0: "t  existence_ivl t0 x  flow t0 x t = 0"
  unfolding flow_def by auto

lemma csols_undefined: "x  X  csols t0 x = {}"
  apply (auto simp: csols_def)
  using general.existence_ivl_empty2 general.existence_ivl_maximal_segment
  apply blast
  done

lemmas existence_ivl_undefined = existence_ivl_empty2

end

subsection ‹Reverse flow as Sublocale›

lemma range_preflect_0[simp]: "range (preflect 0) = UNIV"
  by (auto simp: preflect_def)
lemma range_uminus[simp]: "range uminus = (UNIV::'a::ab_group_add set)"
  by auto

context auto_ll_on_open begin

sublocale rev: auto_ll_on_open "-f" rewrites "-(-f) = f"
   apply unfold_locales
  using auto_local_lipschitz auto_open_domain
  unfolding fun_Compl_def local_lipschitz_minus
  by auto

lemma existence_ivl_eq_rev0: "existence_ivl0 y = uminus ` rev.existence_ivl0 y" for y
  by (auto simp: existence_ivl_eq_rev rev.existence_ivl0_def preflect_def)

lemma rev_existence_ivl_eq0: "rev.existence_ivl0 y = uminus ` existence_ivl0 y" for y
  using uminus_uminus_image[of "rev.existence_ivl0 y"]
  by (simp add: existence_ivl_eq_rev0)

lemma flow_eq_rev0: "flow0 y t = rev.flow0 y (-t)" for y t
  apply (cases "t  existence_ivl0 y")
  subgoal
    apply (subst flow_eq_rev(2), assumption)
    apply (subst rev.flow0_def)
    by (simp add: preflect_def)
  subgoal
    apply (frule flow_undefined0)
    by (auto simp: existence_ivl_eq_rev0 rev.flow_undefined0)
  done

lemma rev_eq_flow: "rev.flow0 y t = flow0 y (-t)" for y t
  apply (subst flow_eq_rev0)
  using uminus_uminus_image[of "rev.existence_ivl0 y"]
  apply -
  apply (subst (asm) existence_ivl_eq_rev0[symmetric])
  by auto

lemma rev_flow_image_eq: "rev.flow0 x ` S = flow0 x ` (uminus ` S)"
  unfolding rev_eq_flow[abs_def]
  by force

lemma flow_image_eq_rev: "flow0 x ` S = rev.flow0 x ` (uminus ` S)"
  unfolding rev_eq_flow[abs_def]
  by force

end

context c1_on_open begin

sublocale rev: c1_on_open "-f" "-f'" rewrites "-(-f) = f" and "-(-f') = f'"
  by (rule c1_on_open_rev) auto

end

context c1_on_open_euclidean begin

sublocale rev: c1_on_open_euclidean "-f" "-f'" rewrites "-(-f) = f" and "-(-f') = f'"
  by unfold_locales auto

end


subsection ‹Autonomous LL ODE : Existence Interval and trapping on the interval›

lemma bdd_above_is_intervalI: "bdd_above I"
  if "is_interval I" "a  b" "a  I" "b  I" for I::"real set"
  by (meson bdd_above_def is_interval_1 le_cases that) 

lemma bdd_below_is_intervalI: "bdd_below I"
  if "is_interval I" "a  b" "a  I" "b  I" for I::"real set"
  by (meson bdd_below_def is_interval_1 le_cases that) 

context auto_ll_on_open begin

lemma open_existence_ivl0:
  assumes x : "x  X"
  shows "a b. a < 0  0 < b  {a..b}  existence_ivl0 x"
proof -
  have a1:"0  existence_ivl0 x"
    by (simp add: x)
  have a2: "open (existence_ivl0 x)"
    by (simp add: x)
  from a1 a2 obtain d where "d > 0" "ball 0 d  existence_ivl0 x"
    using openE by blast
  have "{-d/2..d/2}  ball 0 d"
    using 0 < d dist_norm mem_ball by auto
  thus ?thesis
    by (smt 0 < d ball 0 d  existence_ivl0 x divide_minus_left half_gt_zero order_trans)
qed

lemma open_existence_ivl':
  assumes x : "x  X"
  obtains a where "a > 0"  "{-a..a}  existence_ivl0 x"
proof -
  from open_existence_ivl0[OF assms(1)]
  obtain a b where ab: "a < 0" "0 < b" "{a..b}  existence_ivl0 x" by auto
  then have "min (-a) b > 0" by linarith
  have "{-min (-a) b .. min(-a) b}  {a..b}" by auto
  thus ?thesis using ab(3) that[OF min (-a) b > 0] by blast
qed

lemma open_existence_ivl_on_compact:
  assumes C: "C  X" and "compact C" "C  {}"
  obtains a where "a > 0" "x. x  C  {-a..a}  existence_ivl0 x"
proof -
  from existence_ivl_cballs
  have "xC. e>0. t>0. ycball x e. cball 0 texistence_ivl0 y"
    by (metis (full_types) C Int_absorb1 Int_iff UNIV_I)
  then
  obtain d' t' where *:
    "xC. 0 < d' x  t' x > 0  (ycball x (d' x). cball 0 (t' x)  existence_ivl0 y)"
    by metis
  with compactE_image[OF compact C, of C "λx. ball x (d' x)"]
  obtain C' where "C'  C" and [simp]: "finite C'" and C_subset: "C  (cC'. ball c (d' c))"
    by force
  from C_subset C  {} have [simp]: "C'  {}" by auto
  define d where "d = Min (d' ` C')"
  define t where "t = Min (t' ` C')"
  have "t > 0" using * C'  C
    by (auto simp: t_def)
  moreover have "{-t .. t}  existence_ivl0 x" if "x  C" for x
  proof -
    from C_subset that C'  C
    obtain c where c: "c  C'" "x  ball c (d' c)" "c  C" by force
    then have "{-t .. t}  cball 0 (t' c)"
      by (auto simp: abs_real_def t_def minus_le_iff)
    also
    from c have "cball 0 (t' c)  existence_ivl0 x"
      using *[rule_format, OF c  C] by auto
    finally show ?thesis .
  qed
  ultimately show ?thesis ..
qed

definition "trapped_forward x K  (flow0 x ` (existence_ivl0 x  {0..})  K)"
  ― ‹TODO: use this for backwards trapped, invariant, and all assumptions›

definition "trapped_backward x K  (flow0 x ` (existence_ivl0 x  {..0})  K)"

definition "trapped x K  trapped_forward x K  trapped_backward x K"

lemma trapped_iff_on_existence_ivl0:
  "trapped x K  (flow0 x ` (existence_ivl0 x)  K)"
  unfolding trapped_def trapped_forward_def trapped_backward_def
  apply (auto)
  by (metis IntI atLeast_iff atMost_iff image_subset_iff less_eq_real_def linorder_not_less)
end

context auto_ll_on_open begin

lemma infinite_rev_existence_ivl0_rewrites:
  "{0..}  rev.existence_ivl0 x  {..0}  existence_ivl0 x"
  "{..0}  rev.existence_ivl0 x  {0..}  existence_ivl0 x"
   apply (auto simp add: rev.rev_existence_ivl_eq0 subset_iff)
  using neg_le_0_iff_le apply fastforce
  using neg_0_le_iff_le by fastforce

lemma trapped_backward_iff_rev_trapped_forward:
  "trapped_backward x K   rev.trapped_forward x K"
  unfolding trapped_backward_def rev.trapped_forward_def
  by (auto simp add: rev_flow_image_eq existence_ivl_eq_rev0 image_subset_iff)

text ‹If solution is trapped in a compact set at some time
  on its existence interval then it is trapped forever›
lemma trapped_sol_right:
  ― ‹TODO: when building on afp-devel (??? outdated):
    🌐‹https://bitbucket.org/isa-afp/afp-devel/commits/0c3edf9248d5389197f248c723b625c419e4d3eb›
  assumes "compact K" "K  X"
  assumes "x  X" "trapped_forward x K"
  shows "{0..}  existence_ivl0 x"
proof (rule ccontr)
  assume "¬ {0..}  existence_ivl0 x"
  from this obtain t where "0  t" "t  existence_ivl0 x" by blast
  then have bdd: "bdd_above (existence_ivl0 x)" 
    by (auto intro!: bdd_above_is_intervalI x  X)
  from flow_leaves_compact_ivl_right [OF UNIV_I x  X bdd UNIV_I assms(1-2)]
  show False by (metis assms(4) trapped_forward_def IntI atLeast_iff image_subset_iff)
qed

lemma trapped_sol_right_gen:
  assumes "compact K" "K  X"
  assumes "t  existence_ivl0 x" "trapped_forward (flow0 x t) K"
  shows "{t..}  existence_ivl0 x"
proof -
  have "x  X"
    using assms(3) local.existence_ivl_empty_iff by fastforce 
  have xtk: "flow0 x t  X"
    by (simp add: assms(3) local.flow_in_domain)
  from trapped_sol_right[OF assms(1-2) xtk assms(4)] have "{0..}  existence_ivl0 (flow0 x t)" .
  thus "{t..}  existence_ivl0 x"
    using existence_ivl_trans[OF assms(3)]
    by (metis add.commute atLeast_iff diff_add_cancel le_add_same_cancel1 subset_iff)
qed

lemma trapped_sol_left:
  ― ‹TODO: when building on afp-devel:
    🌐‹https://bitbucket.org/isa-afp/afp-devel/commits/0c3edf9248d5389197f248c723b625c419e4d3eb›
  assumes "compact K" "K  X"
  assumes "x  X" "trapped_backward x K"
  shows "{..0}  existence_ivl0 x"
proof (rule ccontr)
  assume "¬ {..0}  existence_ivl0 x"
  from this obtain t where "t  0" "t  existence_ivl0 x" by blast
  then have bdd: "bdd_below (existence_ivl0 x)" 
    by (auto intro!: bdd_below_is_intervalI x  X)
  from flow_leaves_compact_ivl_left [OF UNIV_I x  X bdd UNIV_I assms(1-2)]
  show False
    by (metis IntI assms(4) atMost_iff auto_ll_on_open.trapped_backward_def auto_ll_on_open_axioms image_subset_iff)
qed

lemma trapped_sol_left_gen:
  assumes "compact K" "K  X"
  assumes "t  existence_ivl0 x" "trapped_backward (flow0 x t) K"
  shows "{..t}  existence_ivl0 x"
proof -
  have "x  X"
    using assms(3) local.existence_ivl_empty_iff by fastforce 
  have xtk: "flow0 x t  X"
    by (simp add: assms(3) local.flow_in_domain)
  from trapped_sol_left[OF assms(1-2) xtk assms(4)] have "{..0}  existence_ivl0 (flow0 x t)" .
  thus "{..t}  existence_ivl0 x"
    using existence_ivl_trans[OF assms(3)]
    by (metis add.commute add_le_same_cancel1 atMost_iff diff_add_cancel subset_eq)
qed

lemma trapped_sol:
  assumes "compact K" "K  X"
  assumes "x  X" "trapped x K"
  shows "existence_ivl0 x = UNIV"
  by (metis (mono_tags, lifting) assms existence_ivl_zero image_subset_iff interval local.existence_ivl_initial_time_iff local.existence_ivl_subset local.subset_mem_compact_implies_subset_existence_interval order_refl subset_antisym trapped_iff_on_existence_ivl0)

(* Follows from rectification *)
lemma regular_locally_noteq:― ‹TODO: should be true in ll_on_open_it›
  assumes "x  X" "f x  0"
  shows "eventually (λt. flow0 x t  x) (at 0)"
proof -
  have nf:"norm (f x) > 0" by (simp add: assms(2)) 
      (* By continuity of solutions and f probably *)
  obtain a where
    a: "a>0"
    "{-a--a}  existence_ivl0 x"
    "0  {-a--a}"
    "t. t  {-a--a}  norm(f (flow0 x t) - f (flow0 x 0))  norm(f x)/2"
  proof -
    from open_existence_ivl'[OF assms(1)]
    obtain a1 where a1: "a1 > 0" "{-a1..a1}  existence_ivl0 x" .
    have "continuous (at 0) (λt. norm(f (flow0 x t) - f (flow0 x 0) ))"
      apply (auto intro!: continuous_intros)
      by (simp add: assms(1) local.f_flow_continuous)
    then obtain a2 where "a2>0"
      "t. norm t < a2 
             norm (f (flow0 x t) - f (flow0 x 0)) < norm(f x)/2"
      unfolding continuous_at_real_range
      by (metis abs_norm_cancel cancel_comm_monoid_add_class.diff_cancel diff_zero half_gt_zero nf norm_zero)
    then have 
      t: "t. t  {-a2<--<a2}  norm(f (flow0 x t) - f (flow0 x 0))  norm(f x)/2"
      by (smt open_segment_bound(2) open_segment_bound1 real_norm_def)
    define a where "a = min a1 (a2/2)"
    have t1:"a > 0" unfolding a_def using a1 > 0 a2 > 0 by auto
    then have t3:"0 {-a--a}"
      using closed_segment_eq_real_ivl by auto
    have "{-a--a}  {-a1..a1}" unfolding a_def using a1 > 0 a2 > 0
      using ODE_Auxiliarities.closed_segment_eq_real_ivl by auto
    then have t2:"{-a--a}  existence_ivl0 x" using a1 by auto
    have "{-a--a}  {-a2<--<a2}" unfolding a_def using a1 > 0 a2 > 0
      by (smt Diff_iff closed_segment_eq_real_ivl atLeastAtMost_iff empty_iff half_gt_zero insert_iff pos_half_less segment(1) subset_eq)
    then have t4:"t. t  {-a--a}  norm(f (flow0 x t) - f (flow0 x 0))  norm(f x)/2" using t by auto
    show ?thesis using t1 t2 t3 t4 that by auto
  qed
  have "t. t  {-a--a}  (flow0 x has_vector_derivative f (flow0 x t)) (at t within {-a--a})"
    apply (rule has_vector_derivative_at_within)
    using a(2) by (auto intro!:flow_has_vector_derivative)
  from vector_differentiable_bound_linearization[OF this _ a(4)]
  have nb:"c d. {c--d}  {-a--a} 
   norm (flow0 x d - flow0 x c - (d - c) *R f (flow0 x 0))   norm (d - c) * (norm (f x) / 2)"
    using a(3) by blast
  have "t. dist t 0 < a  t  0  flow0 x t  x"
  proof (rule ccontr)
    fix t
    assume "dist t 0 < a" "t  0" "¬ flow0 x t  x"
    then have tx:"flow0 x t = x" by auto
    have "t  {-a--a}"
      using closed_segment_eq_real_ivl dist t 0 < a by auto
    have "t > 0  t < 0" using t  0 by linarith
    moreover {
      assume "t > 0"
      then have "{0--t}  {-a--a}"
        by (simp add: t  {-a--a} a(3) subset_closed_segment) 
      from nb[OF this] have
        "norm (flow0 x t - x - t *R f x)  norm t * (norm (f x) / 2)"
        by (simp add: assms(1))
      then have "norm (t *R f x)  norm t * (norm (f x) / 2)" using tx by auto
      then have False using nf
        using 0 < t by auto 
    }
    moreover {
      assume "t < 0"
      then have "{t--0}  {-a--a}"
        by (simp add: t  {-a--a} a(3) subset_closed_segment) 
      from nb[OF this] have
        "norm (x - flow0 x t + t *R f x)  norm t * (norm (f x) / 2)"
        by (simp add: assms(1))
      then have "norm (t *R f x)  norm t * (norm (f x) / 2)" using tx by auto
      then have False using nf
        using t < 0 by auto 
    }
    ultimately show False by blast
  qed
  thus ?thesis unfolding eventually_at
    using a(1) by blast
qed

lemma compact_max_time_flow_in_closed:
  assumes "closed M" and t_ex: "t  existence_ivl0 x"
  shows "compact {s  {0..t}. flow0 x ` {0..s}  M}" (is "compact ?C")
  unfolding compact_eq_bounded_closed
proof
  have "bounded {0 .. t}" by auto
  then show "bounded ?C"
    by (rule bounded_subset) auto
  show "closed ?C"
    unfolding closed_def
  proof (rule topological_space_class.openI, clarsimp)
    ― ‹TODO: there must be a more abstract argument for this, e.g., with
      @{thm continuous_on_closed_vimageI} and then reasoning about the connected component around 0?›
    fix s
    assume notM: "s  t  0  s  ¬ flow0 x ` {0..s}  M"
    consider "0  s" "s  t" "flow0 x s  M" | "0  s" "s  t" "flow0 x s  M" | "s < 0" | "s > t"
      by arith
    then show "T. open T  s  T  T  - {s. 0  s  s  t  flow0 x ` {0..s}  M}"
    proof cases
      assume s: "0  s" "s  t" and sM: "flow0 x s  M"
      have "isCont (flow0 x) s"
        using s ivl_subset_existence_ivl[OF t_ex]
        by (auto intro!: flow_continuous)
      from this[unfolded continuous_at_open, rule_format, of "-M"] sM closed M
      obtain S where "open S" "s  S" "(x'S. flow0 x x'  - M)"
        by auto
      then show ?thesis
        by (force intro!: exI[where x=S])
    next
      assume s: "0  s" "s  t" and sM: "flow0 x s  M"
      from this notM obtain s0 where s0: "0  s0" "s0 < s" "flow0 x s0  M"
        by force
      from order_tendstoD(1)[OF tendsto_ident_at s0 < s, of UNIV, unfolded eventually_at_topological]
      obtain S where "open S" "s  S" "x. x  S  x  s  s0 < x"
        by auto
      then show ?thesis using s0
        by (auto simp: intro!: exI[where x=S]) (smt atLeastAtMost_iff image_subset_iff)
    qed (force intro: exI[where x="{t<..}"] exI[where x="{..<0}"])+
  qed
qed

lemma flow_in_closed_max_timeE:
  assumes "closed M" "t  existence_ivl0 x" "0  t" "x  M"
  obtains T where "0  T" "T  t" "flow0 x ` {0..T}  M"
    "s'. 0  s'  s'  t  flow0 x ` {0..s'}  M  s'  T"
proof -
  let ?C = "{s  {0..t}. flow0 x ` {0..s}  M}"
  have "?C  {}"
    using assms
    using local.mem_existence_ivl_iv_defined
    by (auto intro!: exI[where x=0])
  from compact_max_time_flow_in_closed[OF assms(1,2)]
  have "compact ?C" .
  from compact_attains_sup[OF this ?C  {}]
  obtain s where s: "0  s" "s  t" "flow0 x ` {0..s}  M"
    and s_max: "s'. 0  s'  s'  t  flow0 x ` {0..s'}  M  s'  s"
    by auto
  then show ?thesis ..
qed

lemma flow_leaves_closed_at_frontierE:
  assumes "closed M" and t_ex: "t  existence_ivl0 x" and "0  t" "x  M" "flow0 x t  M"
  obtains s where "0  s" "s < t" "flow0 x ` {0..s}  M"
    "flow0 x s  frontier M"
    "F s' in at_right s. flow0 x s'  M"
proof -
  from flow_in_closed_max_timeE[OF assms(1-4)] assms(5)
  obtain s where s: "0  s" "s < t" "flow0 x ` {0..s}  M"
    and s_max: "s'. 0  s'  s'  t  flow0 x ` {0..s'}  M  s'  s"
    by (smt atLeastAtMost_iff image_subset_iff)
  note s
  moreover
  have "flow0 x s  interior M"
  proof
    assume interior: "flow0 x s  interior M"
    have "s  existence_ivl0 x" using ivl_subset_existence_ivl[OF t  _] s by auto
    from flow_continuous[OF this, THEN isContD, THEN topological_tendstoD, OF open_interior interior]
    have "F s' in at s. flow0 x s'  interior M" by auto
    then have "F s' in at_right s. flow0 x s'  interior M"
      by (auto simp: eventually_at_split)
    moreover have "F s' in at_right s. s' < t"
      using tendsto_ident_at s < t
      by (rule order_tendstoD)
    ultimately have "F s' in at_right s. flow0 x s'  M  s' < t"
      by eventually_elim (use interior_subset[of M] in auto)
    then obtain s' where s': "s < s'" "s' < t" "y. y > s  y  s'  flow0 x y  M"
      by (auto simp: eventually_at_right_field_le)
    have s'_ivl: "flow0 x ` {0..s'}  M"
    proof safe
      fix s'' assume "s''  {0 .. s'}"
      then show "flow0 x s''  M"
        using s interior_subset[of M] s'
        by (cases "s''  s") auto
    qed
    with s_max[of s'] s' < t 0  s s < s' show False by auto
  qed
  then have "flow0 x s  frontier M"
    using s closure_subset[of M]
    by (force simp: frontier_def)
  moreover
  have "compact (flow0 x -` M  {s..t})" (is "compact ?C")
    unfolding compact_eq_bounded_closed
  proof
    have "bounded {s .. t}" by simp
    then show "bounded ?C"
      by (rule bounded_subset) auto
    show "closed ?C"
      using closed M assms mem_existence_ivl_iv_defined(2)[OF t_ex] ivl_subset_existence_ivl[OF t_ex] 0  s
      by (intro closed_vimage_Int) (auto intro!: continuous_intros)
  qed
  have "F s' in at_right s. flow0 x s'  M"
    apply (rule ccontr)
    unfolding not_frequently
  proof -
    assume "F s' in at_right s. ¬ flow0 x s'  M"
    moreover have "F s' in at_right s. s' < t"
      using tendsto_ident_at s < t
      by (rule order_tendstoD)
    ultimately have "F s' in at_right s. flow0 x s'  M  s' < t" by eventually_elim auto
    then obtain s' where s': "s < s'"
      "y. y > s  y < s'  flow0 x y  M"
      "y. y > s  y < s'  y < t"
      by (auto simp: eventually_at_right_field)
    define s'' where "s'' = (s + s') / 2"
    have "0  s''" "s''  t"  "s < s''" "s'' < s'"
      using s s'
      by (auto simp del: divide_le_eq_numeral1 le_divide_eq_numeral1 simp: s''_def) fastforce
    then have "flow0 x ` {0..s''}  M"
      using s s'
      apply auto
      subgoal for u
        by (cases "us") auto
      done
    from s_max[OF 0  s'' s'' t this] s'' > s
    show False by simp
  qed
  ultimately show ?thesis ..
qed


subsection ‹Connectedness›

lemma fcontX:
  shows "continuous_on X f"
  using auto_local_lipschitz local_lipschitz_continuous_on by blast

lemma fcontx:
  assumes "x  X"
  shows "continuous (at x) f"
proof -
  have "open X" by simp
  from continuous_on_eq_continuous_at[OF this]
  show ?thesis using fcontX assms(1) by blast
qed

lemma continuous_at_imp_cball:
  assumes "continuous (at x) g"
  assumes "g x > (0::real)"
  obtains r where "r > 0" "y  cball x r. g y > 0"
proof -
  from assms(1)
  obtain d where "d>0" "g ` (ball x d)  ball (g x) ((g x)/2)"
    by (meson assms(2) continuous_at_ball half_gt_zero)
  then have "y  cball x (d/2). g y > 0"
    by (smt assms(2) dist_norm image_subset_iff mem_ball mem_cball pos_half_less real_norm_def)
  thus ?thesis
    using 0 < d that half_gt_zero by blast
qed

text flow0› is path_connected›
lemma flow0_path_connected_time:
  assumes "ts  existence_ivl0 x" "path_connected ts"
  shows "path_connected (flow0 x ` ts)"
proof -
  have "continuous_on ts (flow0 x)"
    by (meson assms continuous_on_sequentially flow_continuous_on subsetD)
  from path_connected_continuous_image[OF this assms(2)] 
  show ?thesis .
qed

lemma flow0_path_connected:
  assumes "path_connected D"
    "path_connected ts"
    "x. x  D  ts  existence_ivl0 x"
  shows "path_connected ( (λ(x, y). flow0 x y) ` (D × ts))"
proof -
  have "D × ts  Sigma X existence_ivl0"
    using assms(3) subset_iff by fastforce
  then have a1:"continuous_on (D × ts) (λ(x, y). flow0 x y)"
    using flow_continuous_on_state_space continuous_on_subset by blast 
  have a2 : "path_connected (D × ts)" using path_connected_Times assms by auto
  from path_connected_continuous_image[OF a1 a2]
  show ?thesis .
qed

end

subsection ‹Return Time and Implicit Function Theorem›

context c1_on_open_euclidean begin

lemma flow_implicit_function:
  ― ‹TODO: generalization of @{thm returns_to_implicit_function}!›
  fixes s::"'a::euclidean_space  real" and S::"'a set"
  assumes t: "t  existence_ivl0 x" and x: "x  X" and st: "s (flow0 x t) = 0"
  assumes Ds: "x. (s has_derivative blinfun_apply (Ds x)) (at x)"
  assumes DsC: "isCont Ds (flow0 x t)"
  assumes nz: "Ds (flow0 x t) (f (flow0 x t))  0"
  obtains u e
  where "s (flow0 x (u x)) = 0"
    "u x = t"
    "(y. y  cball x e  s (flow0 y (u y)) = 0)"
    "continuous_on (cball x e) u"
    "(λt. (t, u t)) ` cball x e  Sigma X existence_ivl0"
    "0 < e" "(u has_derivative (- blinfun_scaleR_left
                   (inverse (blinfun_apply (Ds (flow0 x t)) (f (flow0 x t)))) oL
                      (Ds (flow0 x t) oL flowderiv x t) oL embed1_blinfun)) (at x)"
proof -
  note [derivative_intros] = has_derivative_compose[OF _ Ds]
  have cont_s: "continuous_on UNIV s" by (rule has_derivative_continuous_on[OF Ds])
  note cls[simp, intro] = closed_levelset[OF cont_s]
  then have xt1: "(x, t)  Sigma X existence_ivl0"
    by (auto simp: t x)
  have D: "(x. x  Sigma X existence_ivl0 
      ((λ(x, t). s (flow0 x t)) has_derivative
       blinfun_apply (Ds (flow0 (fst x) (snd x)) oL (flowderiv (fst x) (snd x))))
       (at x))"
    by (auto intro!: derivative_eq_intros)
  have C: "isCont (λx. Ds (flow0 (fst x) (snd x)) oL flowderiv (fst x) (snd x))
   (x, t)"
    using flowderiv_continuous_on[unfolded continuous_on_eq_continuous_within,
        rule_format, OF xt1]
    using at_within_open[OF xt1 open_state_space]
    by (auto intro!: continuous_intros tendsto_eq_intros x t
        isCont_tendsto_compose[OF DsC, unfolded poincare_map_def]
        simp: split_beta' isCont_def)
  have Z: "(case (x, t) of (x, t)  s (flow0 x t)) = 0"
    by (auto simp: st)
  have I1: "blinfun_scaleR_left (inverse (Ds (flow0 x t)(f (flow0 x t)))) oL 
    ((Ds (flow0 (fst (x, t))
            (snd (x, t))) oL
       flowderiv (fst (x, t))
        (snd (x, t))) oL
      embed2_blinfun)
     = 1L"
    using nz
    by (auto intro!: blinfun_eqI
        simp: flowderiv_def blinfun.bilinear_simps inverse_eq_divide poincare_map_def)
  have I2: "((Ds (flow0 (fst (x, t))
            (snd (x, t))) oL
       flowderiv (fst (x, t))
        (snd (x, t))) oL
      embed2_blinfun) oL blinfun_scaleR_left (inverse (Ds (flow0 x t)(f (flow0 x t))))
     = 1L"
    using nz
    by (auto intro!: blinfun_eqI
        simp: flowderiv_def blinfun.bilinear_simps inverse_eq_divide poincare_map_def)
  show ?thesis
    apply (rule implicit_function_theorem[where f="λ(x, t). s (flow0 x t)"
          and S="Sigma X existence_ivl0", OF D xt1 open_state_space order_refl C Z I1 I2])
     apply blast
    unfolding split_beta' fst_conv snd_conv poincare_map_def[symmetric]
    ..
qed

lemma flow_implicit_function_at:
  fixes s::"'a::euclidean_space  real" and S::"'a set"
  assumes x: "x  X" and st: "s x = 0"
  assumes Ds: "x. (s has_derivative blinfun_apply (Ds x)) (at x)"
  assumes DsC: "isCont Ds x"
  assumes nz: "Ds x (f x)  0"
  assumes pos: "e > 0"
  obtains u d
  where
    "0 < d"
    "u x = 0"
    "y. y  cball x d  s (flow0 y (u y)) = 0"
    "y. y  cball x d  ¦u y¦ < e"
    "y. y  cball x d  u y  existence_ivl0 y"
    "continuous_on (cball x d) u"
    "(u has_derivative -Ds x /R (Ds x) (f x)) (at x)"
proof -
  have x0: "flow0 x 0 = x" by (simp add: x)
  from flow_implicit_function[OF existence_ivl_zero[OF x] x, unfolded x0, of s, OF st Ds DsC nz]
  obtain u d0 where
    s0: "s (flow0 x (u x)) = 0"
    and u0: "u x = 0"
    and u: "y. y  cball x d0  s (flow0 y (u y)) = 0"
    and uc: "continuous_on (cball x d0) u"
    and uex: "(λt. (t, u t)) ` cball x d0  Sigma X existence_ivl0"
    and d0: "0 < d0"
    and u': "(u has_derivative
     blinfun_apply
      (- blinfun_scaleR_left (inverse (blinfun_apply (Ds x) (f x))) oL (Ds x oL flowderiv x 0) oL embed1_blinfun))
     (at x)"
    by blast
  have "at x within cball x d0 = at x" by (rule at_within_interior) (auto simp: 0 < d0)
  then have "(u  0) (at x)"
    using uc d0 by (auto simp: continuous_on_def u0 dest!: bspec[where x=x])
  from tendstoD[OF this 0 < e] pos u0
  obtain d1 where d1: "0 < d1" "xa. dist xa x  d1  ¦u xa¦ < e"
    unfolding eventually_at_le
    by force
  define d where "d = min d0 d1"
  have "0 < d" by (auto simp: d_def d0 d1)
  moreover note u0
  moreover have "y. y  cball x d  s (flow0 y (u y)) = 0" by (auto intro!: u simp: d_def)
  moreover have "y. y  cball x d  ¦u y¦ < e" using d1 by (auto simp: d_def dist_commute)
  moreover have "y. y  cball x d  u y  existence_ivl0 y"
    using uex by (force simp: d_def)
  moreover have "continuous_on (cball x d) u"
    using uc by (rule continuous_on_subset) (auto simp: d_def)
  moreover
  have "(u has_derivative -Ds x /R (Ds x) (f x)) (at x)"
    using u'
    by (rule has_derivative_subst) (auto intro!: ext simp: x x0 flowderiv_def blinfun.bilinear_simps)
  ultimately show ?thesis ..
qed

lemma returns_to_implicit_function_gen:
  ― ‹TODO: generalizes proof of @{thm returns_to_implicit_function}!›
  fixes s::"'a::euclidean_space  real"
  assumes rt: "returns_to {x  S. s x = 0} x" (is "returns_to ?P x")
  assumes cS: "closed S"
  assumes Ds: "x. (s has_derivative blinfun_apply (Ds x)) (at x)"
    "isCont Ds (poincare_map ?P x)"
    "Ds (poincare_map ?P x) (f (poincare_map ?P x))  0"
  obtains u e
  where "s (flow0 x (u x)) = 0"
    "u x = return_time ?P x"
    "(y. y  cball x e  s (flow0 y (u y)) = 0)"
    "continuous_on (cball x e) u"
    "(λt. (t, u t)) ` cball x e  Sigma X existence_ivl0"
    "0 < e" "(u has_derivative (- blinfun_scaleR_left
                   (inverse (blinfun_apply (Ds (poincare_map ?P x)) (f (poincare_map ?P x)))) oL
                      (Ds (poincare_map ?P x) oL flowderiv x (return_time ?P x)) oL embed1_blinfun)) (at x)"
proof -
  note [derivative_intros] = has_derivative_compose[OF _ Ds(1)]
  have cont_s: "continuous_on UNIV s" by (rule has_derivative_continuous_on[OF Ds(1)])
  note cls[simp, intro] = closed_levelset[OF cont_s]
  let ?t1 = "return_time ?P x"
  have cls[simp, intro]: "closed {x  S. s x = 0}"
    by (rule closed_levelset_within) (auto intro!: cS continuous_on_subset[OF cont_s])

  have *: "poincare_map ?P x = flow0 x (return_time {x  S. s x = 0} x)"
    by (simp add: poincare_map_def)
  have "return_time {x  S. s x = 0} x  existence_ivl0 x"
    "x  X"
    "s (poincare_map ?P x) = 0"
    using poincare_map_returns rt
    by (auto intro!: return_time_exivl rt)
  note E = flow_implicit_function[of "return_time ?P x" x s Ds, OF this[unfolded *] Ds[unfolded *],
      folded *]
  show ?thesis
    by (rule E) rule
qed

text ‹c.f. Perko Section 3.7 Lemma 2 part 1.›

lemma flow_transversal_surface_finite_intersections:
  fixes s::"'a  'b::real_normed_vector"
    and Ds::"'a  'a L 'b"
  assumes "closed S"
  assumes "x. (s has_derivative (Ds x)) (at x)"
  assumes "x. x  S  s x = 0  Ds x (f x)  0"
  assumes "a  b" "{a .. b}  existence_ivl0 x"
  shows "finite {t{a..b}. flow0 x t  {x  S. s x = 0}}"
    ― ‹TODO: define notion of (compact/closed)-(continuous/differentiable/C1)-surface?›
proof cases
  note Ds = x. (s has_derivative (Ds x)) (at x)
  note transversal = x. x  S  s x = 0  Ds x (f x)  0
  assume "a < b"
  show ?thesis
  proof (rule ccontr)
    let ?S = "{x  S. s x = 0}"
    let ?T = "{t{a..b}. flow0 x t  {x  S. s x = 0}}"
    define φ where "φ = flow0 x"
    have [THEN continuous_on_compose2, continuous_intros]: "continuous_on S s"
      by (auto simp: intro!: has_derivative_continuous_on Ds intro: has_derivative_at_withinI)
    assume "infinite ?T"
    from compact_sequentialE[OF compact_Icc[of a b] this]
    obtain t tl where t: "t n  ?T" "flow0 x (t n)  ?S" "t n  {a .. b}" "t n  tl"
      and tl: "t  tl" "tl  {a..b}"
    for n
      by force
    have tl_ex: "tl  existence_ivl0 x" using {a .. b}  existence_ivl0 x tl  {a .. b} by auto
    have "closed ?S"
      by (auto intro!: closed_levelset_within closed S continuous_intros)
    moreover
    have "n. flow0 x (t n)  ?S"
      using t by auto
    moreover
    have flow_t: "(λn. flow0 x (t n))  flow0 x tl"
      by (auto intro!: tendsto_eq_intros tl_ex tl)
    ultimately have "flow0 x tl  ?S"
      by (metis (no_types, lifting) closed_sequentially)

    let ?qt = "λt. (flow0 x t - flow0 x tl) /R (t - tl)"
    from flow_has_vector_derivative[OF tl_ex, THEN has_vector_derivative_withinD]
    have qt_tendsto: "?qt tl f (flow0 x tl)" .
    let ?q = "λn. ?qt (t n)"
    have "filterlim t (at tl) sequentially"
      using tl(1)
      by (rule filterlim_atI) (simp add: t)
    with qt_tendsto have "?q  f (flow0 x tl)"
      by (rule filterlim_compose)
    then have "((λn. Ds (flow0 x tl) (?q n)))  Ds (flow0 x tl) (f (flow0 x tl))"
      by (auto intro!: tendsto_intros)
    moreover

    from flow_lipschitzE[OF {a .. b}  existence_ivl0 x] obtain L' where L': "L'-lipschitz_on {a..b} (flow0 x)" .
    define L where "L = L' + 1"
    from lipschitz_on_le[OF L', of L] lipschitz_on_nonneg[OF L']
    have L: "L-lipschitz_on {a .. b} (flow0 x)" and "L > 0"
      by (auto simp: L_def)
    from flow_lipschitzE[OF {a .. b}  existence_ivl0 x] obtain L' where "L'-lipschitz_on {a..b} (flow0 x)" .
        ― ‹TODO: is this reasoning (below) with this Lipschitz constant really necessary?›
    have s[simp]: "s (flow0 x (t n)) = 0""s (flow0 x tl) = 0"
      for n
      using t flow0 x tl  ?S
      by auto

    from Ds(1)[of "flow0 x tl", unfolded has_derivative_within]
    have "(λy. (1 / norm (y - flow0 x tl)) *R (s y - (s (flow0 x tl) + blinfun_apply (Ds (flow0 x tl)) (y - flow0 x tl)))) flow0 x tl 0"
      by auto
    then have "((λy. (1 / norm (y - flow0 x tl)) *R (s y - (s (flow0 x tl) + blinfun_apply (Ds (flow0 x tl)) (y - flow0 x tl))))  0)
      (nhds (flow0 x tl))"
      by (rule tendsto_nhds_continuousI) simp

    from filterlim_compose[OF this flow_t]
    have "(λxa. (blinfun_apply (Ds (flow0 x tl)) (flow0 x (t xa) - flow0 x tl)) /R norm (flow0 x (t xa) - flow0 x tl))
       0"
      using t
      by (auto simp: inverse_eq_divide tendsto_minus_cancel_right)
    from tendsto_mult[OF tendsto_const[of "L"] tendsto_norm[OF this, simplified, simplified divide_inverse_commute[symmetric]]]― ‹TODO: uuugly›
    have Ds0: "(λxa. norm (blinfun_apply (Ds (flow0 x tl)) (flow0 x (t xa) - flow0 x tl)) / (norm (flow0 x (t xa) - flow0 x tl)/(L)))  0"
      by (auto simp: ac_simps)

    from _ Ds0 have "((λn. Ds (flow0 x tl) (?q n))  0)"
      apply (rule Lim_null_comparison)
      apply (rule eventuallyI)
      unfolding norm_scaleR blinfun.scaleR_right abs_inverse divide_inverse_commute[symmetric]
      subgoal for n
        apply (cases "flow0 x (t n) = flow0 x tl")
        subgoal by (simp add: blinfun.bilinear_simps)
        subgoal
          apply (rule divide_left_mono)
          using lipschitz_onD[OF L, of "t n" tl] 0 < L t(3) tl(2)
          by (auto simp: algebra_split_simps zero_less_divide_iff dist_norm pos_divide_le_eq
              intro!: add_pos_nonneg)
        done
      done
    ultimately have "Ds (flow0 x tl) (f (flow0 x tl)) = 0"
      by (rule LIMSEQ_unique)
    moreover have "Ds (flow0 x tl) (f (flow0 x tl))  0"
      by (rule transversal) (use flow0 x tl  ?S in auto)
    ultimately show False by auto
  qed
qed (use assms in auto)

lemma uniform_limit_flow0_state:― ‹TODO: is that something more general?›
  assumes "compact C"
  assumes "C  X"
  shows "uniform_limit C (λs x. flow0 x s) (λx. flow0 x 0) (at 0)"
proof (cases "C = {}")
  case True then show ?thesis by auto
next
  case False show ?thesis
  proof (rule uniform_limitI)
    fix e::real assume "0 < e"
    {
      fix x assume "x  C"
      with assms have "x  X" by auto
      from existence_ivl_cballs[OF UNIV_I x  X]
      obtain t L u where "y. y  cball x u  cball 0 t  existence_ivl0 y"
        "s y. y  cball x u  s  cball 0 t  flow0 y s  cball y u"
        "L-lipschitz_on (cball 0 t×cball x u) (λ(t, x). flow0 x t)"
        "y. y  cball x u  cball y u  X"
        "0 < t" "0 < u"
        by metis
      then have "L. u>0. t>0. L-lipschitz_on (cball 0 t×cball x u) (λ(t, x). flow0 x t)" by blast
    } then have "xC. L. u>0. t>0. L-lipschitz_on (cball 0 t×cball x u) (λ(t, x). flow0 x t)" ..
    then obtain L d' u' where
      L: "x. x  C  (L x)-lipschitz_on (cball 0 (d' x)×cball x (u' x)) (λ(t, x). flow0 x t)"
      and d': "x. x  C  d' x > 0"
      and u': "x. x  C  u' x > 0"
      by metis
    have "C  (cC. ball c (u' c))" using u' by auto
    from compactE_image[OF compact C _ this]
    obtain C' where "C'  C" and [simp]: "finite C'" and C'_cover: "C  (cC'. ball c (u' c))"
      by auto
    from C'_cover obtain c' where c': "x  C  x  ball (c' x) (u' (c' x))" "x  C  c' x  C'" for x
      by (auto simp: subset_iff) metis
    have "F s in at 0. xball c (u' c). dist (flow0 x s) (flow0 x 0) < e" if "c  C'" for c
    proof -
      have cC: "c  C"
        using c' c  C' d' C'  C
        by auto
      have *: "dist (flow0 x s) (flow0 x 0)  L c * ¦s¦"
        if "xball c (u' c)"
          "s  cball 0 (d' c)"
        for x s
      proof -
        from L[OF cC, THEN lipschitz_onD, of "(0, x)" "(s, x)"] d'[OF cC] that
        show ?thesis
          by (auto simp: dist_prod_def dist_commute)
      qed
      have "F s in at 0. abs s < d' c"
        by (rule order_tendstoD tendsto_intros)+ (use d' cC in auto)
      moreover have "F s in at 0. L c * ¦s¦ < e"
        by (rule order_tendstoD tendsto_intros)+ (use 0 < e in auto)
      ultimately show ?thesis
        apply eventually_elim
        apply (use * in auto)
        by smt
    qed
    then have "F s in at 0. cC'. xball c (u' c). dist (flow0 x s) (flow0 x 0) < e"
      by (simp add: eventually_ball_finite_distrib)
    then show "F s in at 0. xC. dist (flow0 x s) (flow0 x 0) < e"
      apply eventually_elim
      apply auto
      subgoal for s x
        apply (drule bspec[where x="c' x"])
         apply (simp add: c'(2))
        apply (drule bspec) prefer 2 apply assumption
        apply auto
        using c'(1) by auto
      done
  qed
qed

end

subsection ‹Fixpoints›

context auto_ll_on_open begin

lemma fixpoint_sol:
  assumes "x  X" "f x = 0"
  shows "existence_ivl0 x = UNIV" "flow0 x t = x"
proof -
  have sol: "((λt::real. x) solves_ode (λ_. f)) UNIV X"
    apply (rule solves_odeI)
    by(auto simp add: assms intro!: derivative_intros)
  from maximal_existence_flow[OF sol] have
    "UNIV  existence_ivl0 x" "flow0 x t = x" by auto
  thus "existence_ivl0 x = UNIV" "flow0 x t = x" by auto
qed

end

end