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 oL d0)  X1  (h'  {0 .. h}. (flow0 x0 h', Dflow x0 h' oL 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 oL d0)  X1"
    and flowpipe_cont: "hl  h  h  hu  (x0, d0)  X0  0  h'  h'  h  (flow0 x0 h', Dflow x0 h' oL 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 oL d0)  X1  (h'  open_segment 0 h. (flow0 x0 h', Dflow x0 h' oL 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 oL d0)  X1"
    "h'. h'  open_segment 0 h  (flow0 x0 h', Dflow x0 h' oL 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 = "{xX0. flowsto {x} T CX Y}"
  let ?X2 = "{xX0. 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) oL d0)  C"
    "h'. h'  {0<--<h}  (flow0 x0 h', Dflow x0 h' oL 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 oL Dflow x0 h oL d0)  E"
    "h'. h'  {0<--<i}  (flow0 (flow0 x0 h) h', Dflow (flow0 x0 h) h' oL (Dflow x0 h oL 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) oL 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' oL 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 oL d0)  E  (h'{0<--<h}. (flow0 x0 h', Dflow x0 h' oL 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 oL 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 oL 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) oL d)  Y" "h'. h'  {0<--<h}  (flow0 x h', (Dflow x h') oL 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) oL c = (a oL c) - (b oL 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)) oL (blinfun_scaleR_left (inverse (f x  n)) oL (blinfun_inner_left n oL 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 = "{xX0. flowsto {x} {0 <.. t} ?CX (CX  (?P × UNIV))}"
  let ?X2 = "{xX0. 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 oL d)  CX" "(flow0 x t, Dflow x t oL 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' oL 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') oL 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 oL 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 oL 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) oL 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 oL 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 oL 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 oL 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 oL (D1 oL 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 oL 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 oL D1) oL 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 oL 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 oL d0)  P1" (is "(?x0, _)  _")
    "(h'. h'  {0<--<h}  (flow0 x0 h', Dflow x0 h' oL d0)  CX)"
    by auto
  then have CX: "(h'. 0 < h'  h' < h  (flow0 x0 h', Dflow x0 h' oL 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 oL (?D1 oL 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 oL ?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 oL ?D1) oL 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 oL 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 oL d)  X1"
      "(h'. h'  {0<--<h}  (flow0 x h', Dflow x h' oL 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