Theory Ordinary_Differential_Equations.Reachability_Analysis

theory Reachability_Analysis
imports
  Flow
  Poincare_Map
begin

lemma not_mem_eq_mem_not: "a ∉ A ⟷ a ∈ - A"
  by auto

lemma continuous_orderD:
  fixes g::"'b::t2_space ⇒ 'c::order_topology"
  assumes "continuous (at x within S) g"
  shows "g x > c ⟹ ∀⇩F y in at x within S. g y > c"
    "g x < c ⟹ ∀⇩F y in at x within S. g y < c"
  using order_tendstoD[OF assms[unfolded continuous_within]]
  by auto

lemma frontier_halfspace_component_ge: "n ≠ 0 ⟹ frontier {x. c ≤ x ∙ n} = plane n c"
  apply (subst (1) inner_commute)
  apply (subst (2) inner_commute)
  apply (subst frontier_halfspace_ge[of n c])
  by auto

lemma closed_Collect_le_within:
  fixes f g :: "'a :: topological_space ⇒ 'b::linorder_topology"
  assumes f: "continuous_on UNIV f"
    and g: "continuous_on UNIV g"
    and "closed R"
  shows "closed {x ∈ R. f x ≤ g x}"
proof -
  have *: "- R ∪ {x. g x < f x} = - {x ∈ R. f x ≤ g x}"
    by auto
  have "open (-R)" using assms by auto
  from open_Un[OF this open_Collect_less [OF g f], unfolded *]
  show ?thesis
    by (simp add: closed_open)
qed

subsection ‹explicit representation of hyperplanes / halfspaces›

datatype 'a sctn = Sctn (normal: 'a) (pstn: real)

definition "le_halfspace sctn x ⟷ x ∙ normal sctn ≤ pstn sctn"

definition "lt_halfspace sctn x ⟷ x ∙ normal sctn < pstn sctn"

definition "ge_halfspace sctn x ⟷ x ∙ normal sctn ≥ pstn sctn"

definition "gt_halfspace sctn x ⟷ x ∙ normal sctn > pstn sctn"

definition "plane_of sctn = {x. x ∙ normal sctn = pstn sctn}"

definition "above_halfspace sctn = Collect (ge_halfspace sctn)"

definition "below_halfspace sctn = Collect (le_halfspace sctn)"

definition "sbelow_halfspace sctn = Collect (lt_halfspace sctn)"

definition "sabove_halfspace sctn = Collect (gt_halfspace sctn)"


subsection ‹explicit H representation of polytopes (mind ‹Polytopes.thy›)›

definition below_halfspaces
where "below_halfspaces sctns = ⋂(below_halfspace ` sctns)"

definition sbelow_halfspaces
where "sbelow_halfspaces sctns = ⋂(sbelow_halfspace ` sctns)"

definition above_halfspaces
where "above_halfspaces sctns = ⋂(above_halfspace ` sctns)"

definition sabove_halfspaces
where "sabove_halfspaces sctns = ⋂(sabove_halfspace ` sctns)"

lemmas halfspace_simps =
  above_halfspace_def
  sabove_halfspace_def
  below_halfspace_def
  sbelow_halfspace_def
  below_halfspaces_def
  sbelow_halfspaces_def
  above_halfspaces_def
  sabove_halfspaces_def
  ge_halfspace_def[abs_def]
  gt_halfspace_def[abs_def]
  le_halfspace_def[abs_def]
  lt_halfspace_def[abs_def]

subsection ‹predicates for reachability analysis›

context c1_on_open_euclidean
begin

definition flowpipe ::
  "(('a::euclidean_space) × ('a ⇒⇩L 'a)) set ⇒ real ⇒ real ⇒
   ('a × ('a ⇒⇩L 'a)) set ⇒ ('a × ('a ⇒⇩L 'a)) set ⇒ bool"
where "flowpipe X0 hl hu CX X1 ⟷ 0 ≤ hl ∧ hl ≤ hu ∧ fst ` X0 ⊆ X ∧ fst ` CX ⊆ X ∧ fst ` X1 ⊆ X ∧
  (∀(x0, d0) ∈ X0. ∀h ∈ {hl .. hu}.
    h ∈ existence_ivl0 x0 ∧ (flow0 x0 h, Dflow x0 h o⇩L d0) ∈ X1 ∧ (∀h' ∈ {0 .. h}. (flow0 x0 h', Dflow x0 h' o⇩L d0) ∈ CX))"

lemma flowpipeD:
  assumes "flowpipe X0 hl hu CX X1"
  shows flowpipe_safeD: "fst ` X0 ∪ fst ` CX ∪ fst ` X1 ⊆ X"
    and flowpipe_nonneg: "0 ≤ hl" "hl ≤ hu"
    and flowpipe_exivl: "hl ≤ h ⟹ h ≤ hu ⟹ (x0, d0) ∈ X0 ⟹ h ∈ existence_ivl0 x0"
    and flowpipe_discrete: "hl ≤ h ⟹ h ≤ hu ⟹ (x0, d0) ∈ X0 ⟹ (flow0 x0 h, Dflow x0 h o⇩L d0) ∈ X1"
    and flowpipe_cont: "hl ≤ h ⟹ h ≤ hu ⟹ (x0, d0) ∈ X0 ⟹ 0 ≤ h' ⟹ h' ≤ h ⟹ (flow0 x0 h', Dflow x0 h' o⇩L d0) ∈ CX"
  using assms
  by (auto simp: flowpipe_def)

lemma flowpipe_source_subset: "flowpipe X0 hl hu CX X1 ⟹ X0 ⊆ CX"
  apply (auto dest: bspec[where x=hl] bspec[where x=0] simp: flowpipe_def)
  apply (drule bspec)
   apply (assumption)
  apply auto
  apply (drule bspec[where x=hl])
   apply auto
  apply (drule bspec[where x=0])
  by (auto simp: flow_initial_time_if)

definition "flowsto X0 T CX X1 ⟷
  (∀(x0, d0) ∈ X0. ∃h ∈ T. h ∈ existence_ivl0 x0 ∧ (flow0 x0 h, Dflow x0 h o⇩L d0) ∈ X1 ∧ (∀h' ∈ open_segment 0 h. (flow0 x0 h', Dflow x0 h' o⇩L d0) ∈ CX))"

lemma flowsto_to_empty_iff[simp]: "flowsto a t b {} ⟷ a = {}"
  by (auto simp: simp: flowsto_def)

lemma flowsto_from_empty_iff[simp]: "flowsto {} t b c"
  by (auto simp: simp: flowsto_def)

lemma flowsto_empty_time_iff[simp]: "flowsto a {} b c ⟷ a = {}"
  by (auto simp: simp: flowsto_def)

lemma flowstoE:
  assumes "flowsto X0 T CX X1" "(x0, d0) ∈ X0"
  obtains h where "h ∈ T" "h ∈ existence_ivl0 x0" "(flow0 x0 h, Dflow x0 h o⇩L d0) ∈ X1"
    "⋀h'. h' ∈ open_segment 0 h ⟹ (flow0 x0 h', Dflow x0 h' o⇩L d0) ∈ CX"
  using assms
  by (auto simp: flowsto_def)

lemma flowsto_safeD: "flowsto X0 T CX X1 ⟹ fst ` X0 ⊆ X"
  by (auto simp: flowsto_def split_beta' mem_existence_ivl_iv_defined)

lemma flowsto_union:
  assumes 1: "flowsto X0 T CX Y" and 2: "flowsto Z S CZ W"
  shows "flowsto (X0 ∪ Z) (T ∪ S) (CX ∪ CZ) (Y ∪ W)"
  using assms unfolding flowsto_def
  by force

lemma flowsto_subset:
  assumes "flowsto X0 T CX Y"
  assumes "Z ⊆ X0" "T ⊆ S" "CX ⊆ CZ" "Y ⊆ W"
  shows "flowsto Z S CZ W"
  unfolding flowsto_def
  using assms
  by (auto elim!: flowstoE) blast

lemmas flowsto_unionI = flowsto_subset[OF flowsto_union]

lemma flowsto_unionE:
  assumes "flowsto X0 T CX (Y ∪ Z)"
  obtains X1 X2 where "X0 = X1 ∪ X2" "flowsto X1 T CX Y" "flowsto X2 T CX Z"
proof -
  let ?X1 = "{x∈X0. flowsto {x} T CX Y}"
  let ?X2 = "{x∈X0. flowsto {x} T CX Z}"
  from assms have "X0 = ?X1 ∪ ?X2" "flowsto ?X1 T CX Y" "flowsto ?X2 T CX Z"
    by (auto simp: flowsto_def)
  thus ?thesis ..
qed

lemma flowsto_trans:
  assumes A: "flowsto A S B C" and C: "flowsto C T D E"
  shows "flowsto A {s + t |s t. s ∈ S ∧ t ∈ T} (B ∪ D ∪ C) E"
  unfolding flowsto_def
proof safe
  fix x0 d0 assume x0: "(x0, d0) ∈ A"
  from flowstoE[OF A x0]
  obtain h where h: "h ∈ S" "h ∈ existence_ivl0 x0" "(flow0 x0 h, (Dflow x0 h) o⇩L d0) ∈ C"
    "⋀h'. h' ∈ {0<--<h} ⟹ (flow0 x0 h', Dflow x0 h' o⇩L d0) ∈ B"
    by auto
  from h(2) have x0[simp]: "x0 ∈ X" by auto
  from flowstoE[OF C ‹_ ∈ C›]
  obtain i where i: "i ∈ T" "i ∈ existence_ivl0 (flow0 x0 h)"
    "(flow0 (flow0 x0 h) i, Dflow (flow0 x0 h) i o⇩L Dflow x0 h o⇩L d0) ∈ E"
    "⋀h'. h' ∈ {0<--<i} ⟹ (flow0 (flow0 x0 h) h', Dflow (flow0 x0 h) h' o⇩L (Dflow x0 h o⇩L d0)) ∈ D"
    by (auto simp: ac_simps)
  have hi: "h + i ∈ existence_ivl0 x0"
    using ‹h ∈ existence_ivl0 x0› ‹i ∈ existence_ivl0 (flow0 x0 h)› existence_ivl_trans by blast
  moreover have "(flow0 x0 (h + i), Dflow x0 (h + i) o⇩L d0) ∈ E"
    apply (subst flow_trans)
      apply fact apply fact
    apply (subst Dflow_trans)
      apply fact apply fact
    apply fact
    done
  moreover have "(flow0 x0 h', Dflow x0 h' o⇩L d0) ∈ B ∪ D ∪ C" if "h'∈{0<--<h + i}" for h'
  proof cases
    assume "h' ∈ {0 <--< h}"
    then show ?thesis using h by simp
  next
    assume "h' ∉ {0 <--< h}"
    with that have h': "h' - h ∈ {0 <--< i}" if "h' ≠ h"
      using that
      by (auto simp: open_segment_eq_real_ivl closed_segment_eq_real_ivl split: if_splits)
    from i(4)[OF this]
    show ?thesis
      apply (cases "h' = h")
      subgoal using h by force
      subgoal
        apply simp
        apply (subst (asm) flow_trans[symmetric])
        subgoal by (rule h)
        subgoal using ‹_ ⟹ h' - h ∈ {0<--<i}› i(2) local.in_existence_between_zeroI
          apply auto
          using open_closed_segment by blast
        subgoal
          unfolding blinfun_compose_assoc[symmetric]
          apply (subst (asm) Dflow_trans[symmetric])
            apply auto
           apply fact+
          done
        done
      done
  qed
  ultimately show "∃h∈{s + t |s t. s ∈ S ∧ t ∈ T}.
      h ∈ existence_ivl0 x0 ∧ (flow0 x0 h, Dflow x0 h o⇩L d0) ∈ E ∧ (∀h'∈{0<--<h}. (flow0 x0 h', Dflow x0 h' o⇩L d0) ∈ B ∪ D ∪ C)"
    using ‹h ∈ S› ‹i ∈ T›
    by (auto intro!: bexI[where x="h + i"])
qed

lemma flowsto_step:
  assumes A: "flowsto A S B C"
  assumes D: "flowsto D T E F"
  shows "flowsto A (S ∪ {s + t |s t. s ∈ S ∧ t ∈ T}) (B ∪ E ∪ C ∩ D) (C - D ∪ F)"
proof -
  have "C = (C ∩ D) ∪ (C - D)" (is "_ = ?C1 ∪ ?C2")
    by auto
  then have "flowsto A S B (?C1 ∪ ?C2)" using A by simp
  from flowsto_unionE[OF this]
  obtain A1 A2 where "A = A1 ∪ A2" and A1: "flowsto A1 S B ?C1" and A2: "flowsto A2 S B ?C2"
    by auto
  have "flowsto ?C1 T E F"
    using D by (rule flowsto_subset) auto
  from flowsto_union[OF flowsto_trans[OF A1 this] A2]
  show ?thesis by (auto simp add: ‹A = _› ac_simps)
qed

lemma
  flowsto_stepI:
    "flowsto X0 U B C ⟹
    flowsto D T E F ⟹
    Z ⊆ X0 ⟹
    (⋀s. s ∈ U ⟹ s ∈ S) ⟹
    (⋀s t. s ∈ U ⟹ t ∈ T ⟹ s + t ∈ S) ⟹
    B ∪ E ∪ D ∩ C ⊆ CZ ⟹ C - D ∪ F ⊆ W ⟹ flowsto Z S CZ W"
  by (rule flowsto_subset[OF flowsto_step]) auto

lemma flowsto_imp_flowsto:
  "flowpipe Y h h CY Z ⟹ flowsto Y {h} (CY) Z"
  unfolding flowpipe_def flowsto_def
  by (auto simp: open_segment_eq_real_ivl split_beta')

lemma connected_below_halfspace:
  assumes "x ∈ below_halfspace sctn"
  assumes "x ∈ S" "connected S"
  assumes "S ∩ plane_of sctn = {}"
  shows "S ⊆ below_halfspace sctn"
proof -
  note ‹connected S›
  moreover
  have "open {x. x ∙ normal sctn < pstn sctn}" (is "open ?X")
    and "open {x. x ∙ normal sctn > pstn sctn}" (is "open ?Y")
    by (auto intro!: open_Collect_less continuous_intros)
  moreover have "?X ∩ ?Y ∩ S = {}" "S ⊆ ?X ∪ ?Y"
    using assms by (auto simp: plane_of_def)
  ultimately have "?X ∩ S = {} ∨ ?Y ∩ S = {}"
    by (rule connectedD)
  then show ?thesis
    using assms
    by (force simp: below_halfspace_def le_halfspace_def plane_of_def)
qed

lemma
  inter_Collect_eq_empty:
  assumes "⋀x. x ∈ X0 ⟹ ¬ g x" shows "X0 ∩ Collect g = {}"
  using assms by auto


subsection ‹Poincare Map›

lemma closed_plane_of[simp]: "closed (plane_of sctn)"
  by (auto simp: plane_of_def intro!: closed_Collect_eq continuous_intros)

definition "poincare_mapsto P X0 S CX Y ⟷ (∀(x, d) ∈ X0.
  returns_to P x ∧ fst ` X0 ⊆ S ∧
  (return_time P differentiable at x within S) ∧
  (∃D. (poincare_map P has_derivative blinfun_apply D) (at x within S) ∧
       (poincare_map P x, D o⇩L d) ∈ Y) ∧
  (∀t∈{0<..<return_time P x}. flow0 x t ∈ CX))"

lemma poincare_mapsto_empty[simp]:
  "poincare_mapsto P {} S CX Y"
  by (auto simp: poincare_mapsto_def)

lemma flowsto_eventually_mem_cont:
  assumes "flowsto X0 T CX Y" "(x, d) ∈ X0" "T ⊆ {0<..}"
  shows "∀⇩F t in at_right 0. (flow0 x t, Dflow x t o⇩L d) ∈ CX"
proof -
  from flowstoE[OF assms(1,2)] assms(3)
  obtain h where h: "0 < h" "h ∈ T" "h ∈ existence_ivl0 x" "(flow0 x h, (Dflow x h) o⇩L d) ∈ Y" "⋀h'. h' ∈ {0<--<h} ⟹ (flow0 x h', (Dflow x h') o⇩L d) ∈ CX"
    by (auto simp: subset_iff)
  have "∀⇩F x in at_right 0. 0 < x ∧ x < h"
    apply (rule eventually_conj[OF eventually_at_right_less])
    using eventually_at_right h(1) by blast
  then show ?thesis
    by eventually_elim (auto intro!: h simp: open_segment_eq_real_ivl)
qed

lemma frontier_aux_lemma:
  fixes R :: "'n::euclidean_space set"
  assumes "closed R" "R ⊆ {x. x ∙ n = c}" and [simp]: "n ≠ 0"
  shows "frontier {x ∈ R. c ≤ x ∙ n} = {x ∈ R. c = x ∙ n}"
  apply (auto simp: frontier_closures)
  subgoal by (metis (full_types) Collect_subset assms(1) closure_minimal subsetD)
  subgoal premises prems for x
  proof -
    note prems
    have "closed {x ∈ R. c ≤ x ∙ n}"
      by (auto intro!: closed_Collect_le_within continuous_intros assms)
    from closure_closed[OF this] prems(1)
    have "x ∈ R" "c ≤ x ∙ n" by auto
    with assms show ?thesis by auto
  qed
  subgoal for x
    using closure_subset by fastforce
  subgoal premises prems for x
  proof -
    note prems
    have *: "{xa ∈ R. x ∙ n ≤ xa ∙ n} = R"
      using assms prems by auto
    have "interior R ⊆ interior (plane n c)"
      by (rule interior_mono) (use assms in auto)
    also have "… = {}"
      by (subst inner_commute) simp
    finally have R: "interior R = {}" by simp
    have "x ∈ closure (- R)"
      unfolding closure_complement
      by (auto simp: R)
    then show ?thesis
      unfolding * by simp
  qed
  done

lemma blinfun_minus_comp_distrib: "(a - b) o⇩L c = (a o⇩L c) - (b o⇩L c)"
  by (auto intro!: blinfun_eqI simp: blinfun.bilinear_simps)


lemma flowpipe_split_at_above_halfspace:
  assumes "flowpipe X0 hl t CX Y" "fst ` X0 ∩ {x. x ∙ n ≥ c} = {}" and [simp]: "n ≠ 0"
  assumes cR: "closed R" and Rs: "R ⊆ plane n c"
  assumes PDP: "⋀x d. (x, d) ∈ CX ⟹ x ∙ n = c ⟹ (x,
     d - (blinfun_scaleR_left (f (x)) o⇩L (blinfun_scaleR_left (inverse (f x ∙ n)) o⇩L (blinfun_inner_left n o⇩L d)))) ∈ PDP"
  assumes PDP_nz: "⋀x d. (x, d) ∈ PDP ⟹ f x ∙ n ≠ 0"
  assumes PDP_inR: "⋀x d. (x, d) ∈ PDP ⟹ x ∈ R"
  assumes PDP_in: "⋀x d. (x, d) ∈ PDP ⟹ ∀⇩F x in at x within plane n c. x ∈ R"
  obtains X1 X2 where "X0 = X1 ∪ X2"
    "flowsto X1 {0<..t} (CX ∩ {x. x ∙ n < c} × UNIV) (CX ∩ {x ∈ R. x ∙ n = c} × UNIV)"
    "flowsto X2 {hl .. t} (CX ∩ {x. x ∙ n < c} × UNIV) (Y ∩ ({x. x ∙ n < c} × UNIV))"
    "poincare_mapsto {x ∈ R. x ∙ n = c} X1 UNIV (fst ` CX ∩ {x. x ∙ n < c}) PDP"
proof -
  let ?sB = "{x. x ∙ n < c}"
  let ?A = "{x. x ∙ n ≥ c}"
  let ?P = "{x ∈ R. x ∙ n = c}"
  have [intro]: "closed ?A" "closed ?P"
    by (auto intro!: closed_Collect_le_within closed_levelset_within continuous_intros cR
        closed_halfspace_component_ge)
  let ?CX = "CX ∩ ?sB × UNIV"
  let ?X1 = "{x∈X0. flowsto {x} {0 <.. t} ?CX (CX ∩ (?P × UNIV))}"
  let ?X2 = "{x∈X0. flowsto {x} {hl .. t} ?CX (Y ∩ (?sB × UNIV))}"
  have "(x, d) ∈ ?X1 ∨ (x, d) ∈ ?X2" if "(x, d) ∈ X0" for x d
  proof -
    from that assms have
      t: "t ∈ existence_ivl0 x" "⋀s. 0 ≤ s ⟹ s ≤ t ⟹ (flow0 x s, Dflow x s o⇩L d) ∈ CX" "(flow0 x t, Dflow x t o⇩L d) ∈ Y"
        apply (auto simp: flowpipe_def dest!: bspec[where x=t])
      apply (drule bspec[where x="(x, d)"], assumption)
      apply simp
      apply (drule bspec[where x=t], force)
      apply auto
      done
    show ?thesis
    proof (cases "∀s∈{0..t}. flow0 x s ∈ ?sB")
      case True
      then have "(x, d) ∈ ?X2" using assms t ‹(x, d) ∈ X0›
        by (auto simp: flowpipe_def flowsto_def open_segment_eq_real_ivl dest!: bspec[where x="(x, d)"])
      then show ?thesis ..
    next
      case False
      then obtain s where s: "0 ≤ s" "s ≤ t" "flow0 x s ∈ ?A"
        by (auto simp: not_less)
      let ?I = "flow0 x -` ?A ∩ {0 .. s}"
      from s have exivlI: "0 ≤ s' ⟹ s' ≤ s ⟹ s' ∈ existence_ivl0 x" for s'
        using ivl_subset_existence_ivl[OF ‹t ∈ existence_ivl0 x›]
        by auto
      then have "compact ?I"
        unfolding compact_eq_bounded_closed
        by (intro conjI bounded_Int bounded_closed_interval disjI2 closed_vimage_Int)
          (auto intro!: continuous_intros closed_Collect_le_within cR)
      moreover
      from s have "?I ≠ {}" by auto
      ultimately have "∃s∈?I. ∀t∈?I. s ≤ t"
        by (rule compact_attains_inf)
      then obtain s' where s': "⋀s''. 0 ≤ s'' ⟹ s'' < s' ⟹ flow0 x s'' ∉ ?A"
          "flow0 x s' ∈ ?A" "0 ≤ s'" "s' ≤ s"
        by (force simp: Ball_def)
      have "flow0 x 0 = x" using local.mem_existence_ivl_iv_defined(2) t(1) by auto
      also have "… ∉ ?A" using assms ‹(x, d) ∈ X0› by auto
      finally have "s' ≠ 0" using s' by auto
      then have "0 < s'" using ‹s' ≥ 0› by simp
      have False if "flow0 x s' ∈ interior ?A"
      proof -
        from that obtain e where "e > 0" and subset: "ball (flow0 x s') e ⊆ ?A"
          by (auto simp: mem_interior)
        from subset have "∀⇩F s'' in at_left s'. ball (flow0 x s') e ⊆ ?A" by simp
        moreover
        from flow_continuous[OF exivlI[OF ‹0 ≤ s'› ‹s' ≤ s›]]
        have "flow0 x ─s'→ flow0 x s'" unfolding isCont_def .
        from tendstoD[OF this ‹0 < e›]
        have "∀⇩F xa in at_left s'. dist (flow0 x xa) (flow0 x s') < e"
          using eventually_at_split by blast
        then have "∀⇩F s'' in at_left s'. flow0 x s'' ∈ ball (flow0 x s') e"
          by (simp add: dist_commute)
        moreover
        have "∀⇩F s'' in at_left s'. 0 < s''"
          using ‹0 < s'›
          using eventually_at_left by blast
        moreover
        have "∀⇩F s'' in at_left s'. s'' < s'"
          by (auto simp: eventually_at_filter)
        ultimately
        have "∀⇩F s'' in at_left s'. False"
          by eventually_elim (use s' in auto)
        then show False
          by auto
      qed
      then have "flow0 x s' ∈ frontier ?A"
        unfolding frontier_def
        using ‹closed ?A› s'
        by auto
      with s' have "(x, d) ∈ ?X1" using assms that s t ‹0 < s'›
        ivl_subset_existence_ivl[OF ‹t ∈ existence_ivl0 x›]
        frontier_subset_closed[OF ‹closed ?A›]
        apply (auto simp: flowsto_def flowpipe_def open_segment_eq_real_ivl frontier_halfspace_component_ge
            intro!:
            dest!: bspec[where x="(x, d)"]
            intro: exivlI)
        apply (safe intro!: bexI[where x=s'])
        subgoal by force
        subgoal premises prems
        proof -
          have CX: "(flow0 x s', Dflow x s' o⇩L d) ∈ CX"
            using prems
            by (auto intro!: prems)
          have "flow0 x s' ∙ n = c" using prems by auto
          from PDP_inR[OF PDP[OF CX this]]
          show "flow0 x s' ∈ R" .
        qed
        subgoal by (auto simp: not_le)
        subgoal by force
        done
      then show ?thesis ..
    qed
  qed
  then have "X0 = ?X1 ∪ ?X2" by auto
  moreover
  have X1: "flowsto ?X1 {0 <.. t} ?CX (CX ∩ (?P × UNIV))"
    and X2: "flowsto ?X2 {hl .. t} ?CX (Y ∩ (?sB × UNIV))"
    by (auto simp: flowsto_def flowpipe_def)
  moreover
  from assms(2) X1 have "poincare_mapsto ?P ?X1 UNIV (fst ` CX ∩ {x. x ∙ n < c}) PDP"
    unfolding poincare_mapsto_def flowsto_def
    apply clarsimp
    subgoal premises prems for x d t
    proof -
      note prems
      have ret: "returns_to ?P x"
        apply (rule returns_to_outsideI[where t=t])
        using prems ‹closed ?P›
        by auto
      moreover
      have ret_le: "return_time ?P x ≤ t"
        apply (rule return_time_le[OF ret _ _ ‹0 < t›])
        using prems ‹closed ?P› by auto
      from prems have CX: "(flow0 x h', (Dflow x h') o⇩L d) ∈ CX" if "0 < h'" "h' ≤ t" for h'
        using that by (auto simp: open_segment_eq_real_ivl)
      have PDP: "(poincare_map ?P x, Dpoincare_map' n c R x o⇩L d) ∈ PDP"
        unfolding poincare_map_def Dpoincare_map'_def
        unfolding blinfun_compose_assoc blinfun_minus_comp_distrib
        apply (rule PDP)
        using poincare_map_returns[OF ret ‹closed ?P›] ret_le
        by (auto simp: poincare_map_def intro!: CX return_time_pos ret)
      have "eventually (returns_to ({x ∈ R. x ∙ n - c = 0})) (at x)"
        apply (rule eventually_returns_to)
        using PDP_nz[OF PDP] assms(2) ‹(x, d) ∈ X0› cR PDP_in[OF PDP]
        by (auto intro!: ret derivative_eq_intros blinfun_inner_left.rep_eq[symmetric]
            simp: eventually_at_filter)
      moreover have "return_time ?P differentiable at x"
        apply (rule differentiableI)
        apply (rule return_time_plane_has_derivative)
        using prems ret PDP_nz[OF PDP] PDP cR PDP_in[OF PDP]
        by (auto simp: eventually_at_filter)
      moreover
      have "(∃D. (poincare_map ?P has_derivative blinfun_apply D) (at x) ∧ (poincare_map ?P x, D o⇩L d) ∈ PDP)"
        apply (intro exI[where x="Dpoincare_map' n c R x"])
        using prems ret PDP_nz[OF PDP] PDP cR PDP_in[OF PDP]
        by (auto simp: eventually_at_filter intro!: poincare_map_plane_has_derivative)
      moreover have
        "flow0 x h ∈ fst ` CX ∧ (c > flow0 x h ∙ n)"
        if "0 < h" "h < return_time ?P x" for h
        using CX[of h] ret that ret_le ‹0 < h›
        apply (auto simp: open_segment_eq_real_ivl intro!: image_eqI[where x="(flow0 x h, (Dflow x h) o⇩L d)"])
        using prems
        by (auto simp add: open_segment_eq_real_ivl dest!: bspec[where x=t])
      ultimately show ?thesis
        unfolding prems(7)[symmetric]
        by force
    qed
    done
  ultimately show ?thesis ..
qed

lemma poincare_map_has_derivative_step:
  assumes Deriv: "(poincare_map P has_derivative blinfun_apply D) (at (flow0 x0 h))"
  assumes ret: "returns_to P x0"
  assumes cont: "continuous (at x0 within S) (return_time P)"
  assumes less: "0 ≤ h" "h < return_time P x0"
  assumes cP: "closed P" and x0: "x0 ∈ S"
  shows "((λx. poincare_map P x) has_derivative (D o⇩L Dflow x0 h)) (at x0 within S)"
proof (rule has_derivative_transform_eventually)
  note return_time_tendsto = cont[unfolded continuous_within, rule_format]
  have "return_time P x0 ∈ existence_ivl0 x0"
    by (auto intro!: return_time_exivl cP ret)
  from ivl_subset_existence_ivl[OF this] less
  have hex: "h ∈ existence_ivl0 x0" by auto
  from eventually_mem_existence_ivl[OF this]
  have "∀⇩F x in at x0 within S. h ∈ existence_ivl0 x"
    by (auto simp: eventually_at)
  moreover
  have "∀⇩F x in at x0 within S. h < return_time P x"
    apply (rule order_tendstoD)
     apply (rule return_time_tendsto)
    by (auto intro!: x0 less)
  moreover have evret: "eventually (returns_to P) (at x0 within S)"
    by (rule eventually_returns_to_continuousI; fact)
  ultimately
  show "∀⇩F x in at x0 within S. poincare_map P (flow0 x h) = poincare_map P x"
    apply eventually_elim
    apply (cases "h = 0")
    subgoal by auto
    subgoal for x
      apply (rule poincare_map_step_flow)
      using ‹0 ≤ h› return_time_least[of P x ]
      by (auto simp: ‹closed P›)
    done
  show "poincare_map P (flow0 x0 h) = poincare_map P x0"
    using less ret x0 cP hex
    apply (cases "h = 0")
    subgoal by auto
    subgoal
      apply (rule poincare_map_step_flow)
      using ‹0 ≤ h› return_time_least[of P x0] ret
      by (auto simp: ‹closed P›)
    done
  show "x0 ∈ S" by fact
  show "((λx. poincare_map P (flow0 x h)) has_derivative blinfun_apply (D o⇩L Dflow x0 h)) (at x0 within S)"
    apply (rule has_derivative_compose[where g="poincare_map P" and f="λx. flow0 x h", OF _ Deriv,
        THEN has_derivative_eq_rhs])
    by (auto intro!: derivative_eq_intros simp: hex flowderiv_def)
qed

lemma poincare_mapsto_trans:
  assumes "poincare_mapsto p1 X0 S    CX P1"
  assumes "poincare_mapsto p2 P1 UNIV CY P2"
  assumes "CX ∪ CY ∪ fst ` P1 ⊆ CZ"
  assumes "p2 ∩ (CX ∪ fst ` P1) = {}"
  assumes [intro, simp]: "closed p1"
  assumes [intro, simp]: "closed p2"
  assumes cont: "⋀x d. (x, d) ∈ X0 ⟹ continuous (at x within S) (return_time p2)"
  shows "poincare_mapsto p2 X0 S CZ P2"
  unfolding poincare_mapsto_def
proof (auto, goal_cases)
  fix x0 d0 assume x0: "(x0, d0) ∈ X0"
  from assms(1) x0 obtain D1 dR1 where 1:
    "returns_to p1 x0"
    "fst ` X0 ⊆ S"
    "(return_time p1 has_derivative dR1) (at x0 within S)"
    "(poincare_map p1 has_derivative blinfun_apply D1) (at x0 within S)"
    "(poincare_map p1 x0, D1 o⇩L d0) ∈ P1"
    "⋀t. 0 < t ⟹ t < return_time p1 x0 ⟹ flow0 x0 t ∈ CX"
    by (auto simp: poincare_mapsto_def differentiable_def)
  then have crt1: "continuous (at x0 within S) (return_time p1)"
    by (auto intro!: has_derivative_continuous)
  show "x0 ∈ S"
    using 1 x0 by auto
  let ?x0 = "poincare_map p1 x0"
  from assms(2) x0 ‹_ ∈ P1›
  obtain D2 dR2 where 2:
    "returns_to p2 ?x0"
    "(return_time p2 has_derivative dR2) (at ?x0)"
    "(poincare_map p2 has_derivative blinfun_apply D2) (at ?x0)"
    "(poincare_map p2 ?x0, D2 o⇩L (D1 o⇩L d0)) ∈ P2"
    "⋀t. t∈{0<..<return_time p2 ?x0} ⟹ flow0 ?x0 t ∈ CY"
    by (auto simp: poincare_mapsto_def differentiable_def)

  have "∀⇩F t in at_right 0. t < return_time p1 x0"
    by (rule order_tendstoD) (auto intro!: return_time_pos 1)
  moreover have "∀⇩F t in at_right 0. 0 < t"
    by (auto simp: eventually_at_filter)
  ultimately have evnotp2: "∀⇩F t in at_right 0. flow0 x0 t ∉ p2"
    by eventually_elim (use assms 1 in auto)
  from 2(1)
  show ret2: "returns_to p2 x0"
    unfolding poincare_map_def
    by (rule returns_to_earlierI)
       (use evnotp2 in ‹auto intro!: less_imp_le return_time_pos 1 return_time_exivl›)
  have not_p2: "0 < t ⟹ t ≤ return_time p1 x0 ⟹ flow0 x0 t ∉ p2" for t
    using 1(5) 1(6)[of t] assms(4)
    by (force simp: poincare_map_def set_eq_iff)
  have pm_eq: "poincare_map p2 x0 = poincare_map p2 (poincare_map p1 x0)"
    using not_p2
    apply (auto simp: poincare_map_def)
    apply (subst flow_trans[symmetric])
      apply (auto intro!: return_time_exivl 1 2[unfolded poincare_map_def])
    apply (subst return_time_step)
    by (auto simp: return_time_step
        intro!: return_time_exivl 1 2[unfolded poincare_map_def] return_time_pos)

  have evret2: "∀⇩F x in at ?x0. returns_to p2 x"
    by (auto intro!: eventually_returns_to_continuousI 2 has_derivative_continuous)

  have evret1: "∀⇩F x in at x0 within S. returns_to p1 x"
    by (auto intro!: eventually_returns_to_continuousI 1 has_derivative_continuous)
  moreover
  from evret2[unfolded eventually_at_topological] 2(1)
  obtain U where U: "open U" "poincare_map p1 x0 ∈ U" "⋀x. x ∈ U ⟹ returns_to p2 x"
    by force
  have "continuous (at x0 within S) (poincare_map p1)"
    by (rule has_derivative_continuous) (rule 1)
  note [tendsto_intros] = this[unfolded continuous_within]
  have "eventually (λx. poincare_map p1 x ∈ U) (at x0 within S)"
    by (rule topological_tendstoD) (auto intro!: tendsto_eq_intros U)
  then have evret_flow: "∀⇩F x in at x0 within S. returns_to p2 (flow0 x (return_time p1 x))"
    unfolding poincare_map_def[symmetric]
    apply eventually_elim
    apply (rule U)
    apply auto
    done
  moreover
  have h_less_rt: "return_time p1 x0 < return_time p2 x0"
    by (rule return_time_gt; fact)
  then have "0 < return_time p2 x0 - return_time p1 x0"
    by (simp )
  from _ this have "∀⇩F x in at x0 within S. 0 < return_time p2 x - return_time p1 x"
    apply (rule order_tendstoD)
    using cont ‹(x0, _) ∈ _›
    by (auto intro!: tendsto_eq_intros crt1 simp: continuous_within[symmetric] continuous_on_def)
  then have evpm2: "∀⇩F x in at x0 within S. ∀s. 0 < s ⟶ s ≤ return_time p1 x ⟶ flow0 x s ∉ p2"
    apply eventually_elim
    apply safe
    subgoal for x s
      using return_time_least[of p2 x s]
      by (auto simp add: return_time_pos_returns_to)
    done
  ultimately
  have pm_eq_at: "∀⇩F x in at x0 within S.
    poincare_map p2 (poincare_map p1 x) = poincare_map p2 x"
    apply (eventually_elim)
    apply (auto simp: poincare_map_def)
    apply (subst flow_trans[symmetric])
      apply (auto intro!: return_time_exivl)
    apply (subst return_time_step)
    by (auto simp: return_time_step
        intro!: return_time_exivl return_time_pos)
  from _ this have "(poincare_map p2 has_derivative blinfun_apply (D2 o⇩L D1)) (at x0 within S)"
    apply (rule has_derivative_transform_eventually)
      apply (rule has_derivative_compose[OF 1(4) 2(3), THEN has_derivative_eq_rhs])
    by (auto simp: ‹x0 ∈ S› pm_eq)
  moreover have "(poincare_map p2 x0, (D2 o⇩L D1) o⇩L d0) ∈ P2"
    using 2(4) unfolding pm_eq blinfun_compose_assoc .
  ultimately
  show "∃D. (poincare_map p2 has_derivative blinfun_apply D) (at x0 within S) ∧
               (poincare_map p2 x0, D o⇩L d0) ∈ P2"
    by auto
  show "0 < t ⟹ t < return_time p2 x0 ⟹ flow0 x0 t ∈ CZ" for t
    apply (cases "t < return_time p1 x0")
    subgoal
      apply (drule 1)
      using assms
      by auto
    subgoal
      apply (cases "t = return_time p1 x0")
      subgoal using 1(5) assms by (auto simp: poincare_map_def)
      subgoal premises prems
      proof -
        have "flow0 x0 t = flow0 ?x0 (t - return_time p1 x0)"
          unfolding poincare_map_def
          apply (subst flow_trans[symmetric])
          using prems
          by (auto simp:
              intro!: return_time_exivl 1 diff_existence_ivl_trans
              less_return_time_imp_exivl[OF _ ret2])
        also have "… ∈ CY"
          apply (rule 2)
          using prems
          apply auto
          using "1"(1) "2"(1) assms poincare_map_def ret2 return_time_exivl
            return_time_least return_time_pos return_time_step
          by auto
        also have "… ⊆ CZ" using assms by auto
        finally show "flow0 x0 t ∈ CZ"
          by simp
      qed
      done
    done
  have rt_eq: "return_time p2 (poincare_map p1 x0) + return_time p1 x0 = return_time p2 x0"
    apply (auto simp: poincare_map_def)
    apply (subst return_time_step)
    by (auto simp: return_time_step poincare_map_def[symmetric] not_p2
        intro!: return_time_exivl return_time_pos 1 2)
  have evrt_eq: "∀⇩F x in at x0 within S.
    return_time p2 (poincare_map p1 x) + return_time p1 x = return_time p2 x"
    using evret_flow evret1 evpm2
    apply (eventually_elim)
    apply (auto simp: poincare_map_def)
    apply (subst return_time_step)
    by (auto simp: return_time_step
        intro!: return_time_exivl return_time_pos)
  from _ evrt_eq
  have "(return_time p2 has_derivative (λx. dR2 (blinfun_apply D1 x) + dR1 x)) (at x0 within S)"
    by (rule has_derivative_transform_eventually)
      (auto intro!: derivative_eq_intros has_derivative_compose[OF 1(4) 2(2)] 1(3) ‹x0 ∈ S›
        simp: rt_eq)
  then show "return_time p2 differentiable at x0 within S" by (auto intro!: differentiableI)
qed

lemma flowsto_poincare_trans:― ‹TODO: the proof is close to @{thm poincare_mapsto_trans}›
  assumes f: "flowsto            X0 T     CX P1"
  assumes "poincare_mapsto p2 P1 UNIV CY P2"
  assumes nn: "⋀t. t ∈ T ⟹ t ≥ 0"
  assumes "fst ` CX ∪ CY ∪ fst ` P1 ⊆ CZ"
  assumes "p2 ∩ (fst ` CX ∪ fst ` P1) = {}"
  assumes [intro, simp]: "closed p2"
  assumes cont: "⋀x d. (x, d) ∈ X0 ⟹ continuous (at x within S) (return_time p2)"
  assumes subset: "fst ` X0 ⊆ S"
  shows "poincare_mapsto p2 X0 S CZ P2"
  unfolding poincare_mapsto_def
proof (auto, goal_cases)
  fix x0 d0 assume x0: "(x0, d0) ∈ X0"
  from flowstoE[OF f x0] obtain h where 1:
    "h ∈ T" "h ∈ existence_ivl0 x0"
    "(flow0 x0 h, Dflow x0 h o⇩L d0) ∈ P1" (is "(?x0, _) ∈ _")
    "(⋀h'. h' ∈ {0<--<h} ⟹ (flow0 x0 h', Dflow x0 h' o⇩L d0) ∈ CX)"
    by auto
  then have CX: "(⋀h'. 0 < h' ⟹ h' < h ⟹ (flow0 x0 h', Dflow x0 h' o⇩L d0) ∈ CX)"
    by (auto simp: nn open_segment_eq_real_ivl)
  from 1 have "0 ≤ h" by (auto simp: nn)
  from assms have CX_p2D: "x ∈ CX ⟹ fst x ∉ p2" for x by auto
  from assms have P1_p2D: "x ∈ P1 ⟹ fst x ∉ p2" for x by auto
  show "x0 ∈ S"
    using x0 1 subset by auto
  let ?D1 = "Dflow x0 h"
  from assms(2) x0 ‹_ ∈ P1›
  obtain D2 dR2 where 2:
    "returns_to p2 ?x0"
    "(return_time p2 has_derivative dR2) (at ?x0)"
    "(poincare_map p2 has_derivative blinfun_apply D2) (at ?x0)"
    "(poincare_map p2 ?x0, D2 o⇩L (?D1 o⇩L d0)) ∈ P2"
    "⋀t. t∈{0<..<return_time p2 ?x0} ⟹ flow0 ?x0 t ∈ CY"
    by (auto simp: poincare_mapsto_def differentiable_def)

  {
    assume pos: "h > 0"
    have "∀⇩F t in at_right 0. t < h"
      by (rule order_tendstoD) (auto intro!: return_time_pos 1 pos)
    moreover have "∀⇩F t in at_right 0. 0 < t"
      by (auto simp: eventually_at_filter)
    ultimately have "∀⇩F t in at_right 0. flow0 x0 t ∉ p2"
      by eventually_elim (use assms in ‹force dest: CX CX_p2D›)
  } note evnotp2 = this
  from 2(1)
  show ret2: "returns_to p2 x0"
    apply (cases "h = 0")
    subgoal using 1 by auto
    unfolding poincare_map_def
    by (rule returns_to_earlierI)
       (use evnotp2 ‹0 ≤ h› in ‹auto intro!: less_imp_le return_time_pos 1 return_time_exivl ›)
  have not_p2: "0 < t ⟹ t ≤ h ⟹ flow0 x0 t ∉ p2" for t
    using 1(1-3) CX[of t] assms(4) CX_p2D P1_p2D
    by (cases "h = t") (auto simp: poincare_map_def set_eq_iff subset_iff)
  have pm_eq: "poincare_map p2 x0 = poincare_map p2 ?x0"
    apply (cases "h = 0", use 1 in force)
    using not_p2 ‹0 ≤ h›
    apply (auto simp: poincare_map_def)
    apply (subst flow_trans[symmetric])
      apply (auto intro!: return_time_exivl 1 2[unfolded poincare_map_def])
    apply (subst return_time_step)
    by (auto simp: return_time_step 
        intro!: return_time_exivl 1 2[unfolded poincare_map_def] return_time_pos)

  have evret2: "∀⇩F x in at ?x0. returns_to p2 x"
    by (auto intro!: eventually_returns_to_continuousI 2 has_derivative_continuous)

  have "∀⇩F x in at x0. h ∈ existence_ivl0 x"
    by (simp add: 1 eventually_mem_existence_ivl)
  then have evex: "∀⇩F x in at x0 within S. h ∈ existence_ivl0 x"
    by (auto simp: eventually_at)
  moreover
  from evret2[unfolded eventually_at_topological] 2(1)
  obtain U where U: "open U" "flow0 x0 h ∈ U" "⋀x. x ∈ U ⟹ returns_to p2 x"
    by force
  note [tendsto_intros] = this[unfolded continuous_within]
  have "eventually (λx. flow0 x h ∈ U) (at x0 within S)"
    by (rule topological_tendstoD) (auto intro!: tendsto_eq_intros U 1)
  then have evret_flow: "∀⇩F x in at x0 within S. returns_to p2 (flow0 x h)"
    unfolding poincare_map_def[symmetric]
    apply eventually_elim
    apply (rule U)
    apply auto
    done
  moreover
  have h_less_rt: "h < return_time p2 x0"
    by (rule return_time_gt; fact)
  then have "0 < return_time p2 x0 - h"
    by (simp )
  from _ this have "∀⇩F x in at x0 within S. 0 < return_time p2 x - h"
    apply (rule order_tendstoD)
    using cont ‹(x0, _) ∈ _›
    by (auto intro!: tendsto_eq_intros simp: continuous_within[symmetric] continuous_on_def)
  then have evpm2: "∀⇩F x in at x0 within S. ∀s. 0 < s ⟶ s ≤ h ⟶ flow0 x s ∉ p2"
    apply eventually_elim
    apply safe
    subgoal for x s
      using return_time_least[of p2 x s]
      by (auto simp add: return_time_pos_returns_to)
    done
  ultimately
  have pm_eq_at: "∀⇩F x in at x0 within S.
    poincare_map p2 (flow0 x h) = poincare_map p2 x"
    apply (eventually_elim)
    apply (cases "h = 0") subgoal by auto
    apply (auto simp: poincare_map_def)
    apply (subst flow_trans[symmetric])
      apply (auto intro!: return_time_exivl)
    apply (subst return_time_step)
    using ‹0 ≤ h›
    by (auto simp: return_time_step intro!: return_time_exivl return_time_pos)
  from _ this have "(poincare_map p2 has_derivative blinfun_apply (D2 o⇩L ?D1)) (at x0 within S)"
    apply (rule has_derivative_transform_eventually)
    apply (rule has_derivative_at_withinI)
    apply (rule has_derivative_compose[OF flow_has_space_derivative 2(3), THEN has_derivative_eq_rhs])
    by (auto simp: ‹x0 ∈ S› pm_eq 1)
  moreover have "(poincare_map p2 x0, (D2 o⇩L ?D1) o⇩L d0) ∈ P2"
    using 2(4) unfolding pm_eq blinfun_compose_assoc .
  ultimately
  show "∃D. (poincare_map p2 has_derivative blinfun_apply D) (at x0 within S) ∧
               (poincare_map p2 x0, D o⇩L d0) ∈ P2"
    by auto
  show "0 < t ⟹ t < return_time p2 x0 ⟹ flow0 x0 t ∈ CZ" for t
    apply (cases "t < h")
    subgoal
      apply (drule CX)
      using assms
      by auto
    subgoal
      apply (cases "t = h")
      subgoal using 1 assms by (auto simp: poincare_map_def)
      subgoal premises prems
      proof -
        have "flow0 x0 t = flow0 ?x0 (t - h)"
          unfolding poincare_map_def
          apply (subst flow_trans[symmetric])
          using prems
          by (auto simp:
              intro!: return_time_exivl 1 diff_existence_ivl_trans
              less_return_time_imp_exivl[OF _ ret2])
        also have "… ∈ CY"
          apply (cases "h = 0")
          subgoal using "1"(2) "2"(5) prems(1) prems(2) by auto
          subgoal
            apply (rule 2)
            using prems
            apply auto
            apply (subst return_time_step)
                 apply (rule returns_to_laterI)
            using ret2 ‹0 ≤ h› ‹h ∈ existence_ivl0 x0› not_p2
            by auto
          done
          also have "… ⊆ CZ" using assms by auto
        finally show "flow0 x0 t ∈ CZ"
          by simp
      qed
      done
    done
  have rt_eq: "return_time p2 ?x0 + h = return_time p2 x0"
    apply (cases "h = 0")
    subgoal using 1 by auto
    subgoal
      apply (subst return_time_step)
      using ‹0 ≤ h›
      by (auto simp: return_time_step poincare_map_def[symmetric] not_p2
          intro!: return_time_exivl return_time_pos 1 2)
    done
  have evrt_eq: "∀⇩F x in at x0 within S.
    return_time p2 (flow0 x h) + h = return_time p2 x"
    using evret_flow evpm2 evex
    apply (eventually_elim)
    apply (cases "h = 0")
    subgoal using 1 by auto
    subgoal
      apply (subst return_time_step)
      using ‹0 ≤ h›
      by (auto simp: return_time_step
          intro!: return_time_exivl return_time_pos)
    done
  from _ evrt_eq
  have "(return_time p2 has_derivative (λx. dR2 (blinfun_apply ?D1 x))) (at x0 within S)"
    apply (rule has_derivative_transform_eventually)
      apply (rule has_derivative_at_withinI)
    by (auto intro!: derivative_eq_intros has_derivative_compose[OF flow_has_space_derivative 2(2)] 1 ‹x0 ∈ S›
        simp: rt_eq)
  then show "return_time p2 differentiable at x0 within S" by (auto intro!: differentiableI)
qed



subsection ‹conditions for continuous return time›


definition "section s Ds S ⟷
  (∀x. (s has_derivative blinfun_apply (Ds x)) (at x)) ∧
  (∀x. isCont Ds x) ∧
  (∀x ∈ S. s x = (0::real) ⟶ Ds x (f x) ≠ 0) ∧
  closed S ∧ S ⊆ X"

lemma sectionD:
  assumes "section s Ds S"
  shows "(s has_derivative blinfun_apply (Ds x)) (at x)"
    "isCont Ds x"
    "x ∈ S ⟹ s x = 0 ⟹ Ds x (f x) ≠ 0"
    "closed S" "S ⊆ X"
  using assms by (auto simp: section_def)

definition "transversal p ⟷ (∀x ∈ p. ∀⇩F t in at_right 0. flow0 x t ∉ p)"

lemma transversalD: "transversal p ⟹ x ∈ p ⟹ ∀⇩F t in at_right 0. flow0 x t ∉ p"
  by (auto simp: transversal_def)

lemma transversal_section:
  fixes c::real
  assumes "section s Ds S"
  shows "transversal {x ∈ S. s x = 0}"
  using assms
  unfolding section_def transversal_def
proof (safe, goal_cases)
  case (1 x)
  then have "x ∈ X" by auto
  have "∀⇩F t in at_right 0. flow0 x t ∉ {xa ∈ S. s xa = 0}"
    by (rule flow_avoids_surface_eventually_at_right)
      (rule disjI2 assms 1[rule_format] refl ‹x ∈ X›)+
  then show ?case
    by simp
qed

lemma section_closed[intro, simp]: "section s Ds S ⟹ closed {x ∈ S. s x = 0}"
  by (auto intro!: closed_levelset_within simp: section_def
      intro!: has_derivative_continuous_on has_derivative_at_withinI[where s=S])


lemma return_time_continuous_belowI:
  assumes ft: "flowsto X0 T CX X1"
  assumes pos: "⋀t. t ∈ T ⟹ t > 0"
  assumes X0: "fst ` X0 ⊆ {x ∈ S. s x = 0}"
  assumes CX: "fst ` CX ∩ {x ∈ S. s x = 0} = {}"
  assumes X1: "fst ` X1 ⊆ {x ∈ S. s x = 0}"
  assumes sec: "section s Ds S"
  assumes nz: "⋀x. x ∈ S ⟹ s x = 0 ⟹ Ds x (f x) ≠ 0"
  assumes Dneg: "(λx. (Ds x) (f x)) ` fst ` X0 ⊆ {..<0}"
  assumes rel_int: "⋀x. x ∈ fst ` X1 ⟹ ∀⇩F x in at x. s x = 0 ⟶ x ∈ S"
  assumes "(x, d) ∈ X0"
  shows "continuous (at x within {x. s x ≤ 0}) (return_time {x ∈ S. s x = 0})"
proof (rule return_time_continuous_below)
  from assms have "x ∈ S" "s x = 0" "x ∈ {x ∈ S. s x = 0}" by auto
  note cs = section_closed[OF sec]
  note sectionD[OF sec]
  from flowstoE[OF ft ‹(x, d) ∈ X0›] obtain h
    where h: "h ∈ T"
      "h ∈ existence_ivl0 x"
      "(flow0 x h, Dflow x h o⇩L d) ∈ X1"
      "(⋀h'. h' ∈ {0<--<h} ⟹ (flow0 x h', Dflow x h' o⇩L d) ∈ CX)"
    by blast
  show ret: "returns_to {x ∈ S. s x = 0} x"
    apply (rule returns_toI)
        apply (rule pos)
        apply (rule h)
    subgoal by (rule h)
    subgoal using h(3) X1 by auto
    subgoal apply (intro transversalD) apply (rule transversal_section) apply (rule sec)
      apply fact
      done
    subgoal by fact
    done
  show "(s has_derivative blinfun_apply (Ds x)) (at x)" for x by fact
  show "closed S" by fact
  show "isCont Ds x" for x by fact
  show "x ∈ S" "s x = 0" by fact+
  let ?p = "poincare_map {x ∈ S. s x = 0} x"
  have "?p ∈ {x ∈ S. s x = 0}" using poincare_map_returns[OF ret cs] .
  with nz show "Ds ?p (f ?p) ≠ 0" by auto
  from Dneg ‹(x, _) ∈ X0› show "Ds x (f x) < 0" by force
  from ‹_ ∈ X1› X1 CX h
  have "return_time {x ∈ S. s x = 0} x = h"
    by (fastforce intro!: return_time_eqI cs pos h simp: open_segment_eq_real_ivl)
  then have "?p ∈ fst ` X1"
    using ‹_ ∈ X1› by (force simp: poincare_map_def)
  from rel_int[OF this] show " ∀⇩F x in at (poincare_map {x ∈ S. s x = 0} x). s x = 0 ⟶ x ∈ S"
    by auto
qed

end

end