theory Poincare
imports "../IVP/Flow"
begin

text {* TODO: adapt lib*}
lemma setsum_Basis_prod_eq:
  fixes f::"('a::euclidean_space*'b::euclidean_space)\<Rightarrow>'c::comm_monoid_add"
  shows "setsum f Basis = setsum (\<lambda>i. f (i, 0)) Basis + setsum (\<lambda>i. f (0, i)) Basis"
proof -
  have "inj_on (\<lambda>u. (u::'a, 0::'b)) Basis" "inj_on (\<lambda>u. (0::'a, u::'b)) Basis"
    by (auto intro!: inj_onI Pair_inject)
  thus ?thesis
    unfolding Basis_prod_def
    by (subst setsum.union_disjoint) (auto simp: Basis_prod_def setsum.reindex)
qed

primrec heads where
  "heads [] = []"
| "heads (x#xs) = [x]#map (\<lambda>ys. x # ys) (heads xs)"

lemma heads_append: "heads (xs @ ys) = heads xs @ map (\<lambda>ys. xs @ ys) (heads ys)"
  by (induct xs) (auto )

lemma empty_set_heads[simp]: "[] \<in> set (heads xs) \<longleftrightarrow> False"
  by (induct xs) auto

lemma inj_on_Cons: "inj_on (Cons x) s"
  by (rule inj_onI) (auto simp: )

lemma distinct_headsI: "distinct xs \<Longrightarrow> distinct (heads xs)"
  by (induct xs) (auto simp: distinct_map inj_on_Cons)

lemma in_set_heads_last_in_set: "y \<in> set (heads xs) \<Longrightarrow> last y \<in> set xs"
  by (induct xs arbitrary: y) auto

lemma in_set_heads_in_set: "xs \<in> set (heads ys) \<Longrightarrow> x \<in> set xs \<Longrightarrow> x \<in> set ys"
  by (induct ys arbitrary: xs x) auto

lemma inj_on_last_set_heads: "distinct xs \<Longrightarrow> inj_on last (set (heads xs))"
  by (induct xs) (auto simp: inj_on_def in_set_heads_last_in_set)

lemma in_set_in_set_heads: "x \<in> set xs \<Longrightarrow> x \<in> last ` set (heads xs)"
proof (induct xs arbitrary: x)
  case Nil thus ?case by auto
next
  case (Cons y ys)
  thus ?case
    apply (auto )
    apply (drule Cons)
    apply auto
    by (metis empty_set_heads imageI last.simps)
qed

lemma in_set_heads_distinct: "i \<in> set (heads xs) \<Longrightarrow> distinct xs \<Longrightarrow> distinct i"
  by (induct xs arbitrary: i) (auto simp: dest: in_set_heads_in_set)

text {* TODO: OMG... *}
lemma set_telescope_aux:
  fixes z::"'a set \<Rightarrow> 'b::ab_group_add"
  assumes "distinct I"
  assumes "\<And>j J. j \<in> set I \<Longrightarrow> J \<subseteq> set I \<Longrightarrow> j \<notin> J \<Longrightarrow> z (insert j J) = z J + r j J"
  shows "z (set I) - z {} = (\<Sum>xs \<leftarrow> rev (heads (rev I)). r (last xs) (set (butlast xs)))"
  using assms
proof (induct I)
  case Nil thus ?case by simp
next
  case (Cons j J)
  hence hyp: "z (set J) + r j (set J) - z {} = (\<Sum>xs\<leftarrow>rev (heads (rev J)). r (last xs) (set (butlast xs))) + r j (set J)" by auto
  from Cons(3)[of j "set J"] Cons(2) have prem: "z (insert j (set J)) = z (set J) + r j (set J)"
    by auto
  show ?case
    by (simp add: prem hyp heads_append)
qed

lemma aux1: "distinct I \<Longrightarrow> a \<in> set (heads I) \<Longrightarrow> takeWhile (\<lambda>j. j \<noteq> last a) I @ [last a] = a"
  by (induct I arbitrary: a) (auto split: split_if_asm simp: in_set_heads_last_in_set)

lemma aux2: "distinct I \<Longrightarrow> b \<in> set I \<Longrightarrow> takeWhile (\<lambda>j. j \<noteq> b) I @ [b] \<in> set (heads I)"
  by (induct I) (auto split: split_if_asm simp: in_set_heads_last_in_set)

lemma aux3: "distinct I \<Longrightarrow> a \<in> set (heads (rev I)) \<Longrightarrow> takeWhile (\<lambda>j. j \<noteq> last a) (rev I) = butlast a"
  apply (induct I arbitrary: a)
  apply (auto )
  by (metis aux1 butlast_snoc distinct.simps(2) distinct_rev rev.simps(2))

lemma set_telescope:
  fixes z::"'a set \<Rightarrow> 'b::ab_group_add"
  assumes "distinct I"
  assumes "\<And>j J. j \<in> set I \<Longrightarrow> J \<subseteq> set I \<Longrightarrow> j \<notin> J \<Longrightarrow> z (insert j J) = z J + r j J"
  obtains s where  "z (set I) - z {} = (\<Sum>i\<in>set I. r i (s i))" "\<And>i. i \<in> set I \<Longrightarrow> i \<notin> s i" "\<And>i. i \<in> set I \<Longrightarrow> s i \<subseteq> set I"
proof -
  def s \<equiv> "\<lambda>i. (takeWhile (\<lambda>j. j \<noteq> i) (rev I))"
  from assms
  have "z (set I) - z {} = (\<Sum>xs\<leftarrow>rev (heads (rev I)). r (last xs) (set (butlast xs)))"
    by (rule set_telescope_aux)
  also have "\<dots> = (\<Sum>i\<in>set I. r i (set (s i)))"
    apply (auto simp: listsum_distinct_conv_setsum_set assms distinct_headsI)
    apply (rule setsum.reindex_bij_witness[where i = "\<lambda>i. s i @ [i]" and j = "\<lambda>xs. last xs"])
    apply (auto simp: s_def assms aux1 aux2 aux3)
    apply (metis append_butlast_last_id empty_set_heads)
    apply (metis in_set_heads_last_in_set set_rev)
    done
  finally have "z (set I) - z {} = (\<Sum>i\<in>set I. r i (set (s i)))" .
  moreover have "\<And>i. i \<in> set I \<Longrightarrow> i \<notin> set (s i)"
    by (auto simp: s_def assms dest!: set_takeWhileD)
  moreover have "\<And>i. i \<in> set I \<Longrightarrow> set (s i) \<subseteq> set I"
    by (auto simp: s_def assms dest!: set_takeWhileD)
  ultimately show ?thesis ..
qed

lemma last_in_butlastD: "last xs \<in> set (butlast xs) \<Longrightarrow> xs = [] \<or> \<not> distinct xs"
  by (induct xs) (auto  split: split_if_asm)

lemma norm_le_componentwise:
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> norm (x \<bullet> i) \<le> norm (y \<bullet> i)"
  shows "norm x \<le> norm y"
  apply (auto simp: norm_le)
  apply (subst euclidean_inner[where 'a='a])
  apply (subst (3)euclidean_inner[where 'a='a])
  apply (auto intro!: setsum_mono)
  using assms
  apply (auto simp: )
  by (metis Convex_Euclidean_Space.norm_le assms inner_real_def)

lemma setsum_mult_delta:
  fixes f::"'a \<Rightarrow> 'b::ring_1"
  shows "finite K \<Longrightarrow> (\<Sum>k\<in>K. f k * (if k = i then 1 else 0)) = (if i \<in> K then f i else 0)"
  by (simp add: if_distrib setsum.delta cong: if_cong)

lemma norm_divide_tendsto_componentwiseI:
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> (\<lambda>x. abs (r x \<bullet> i) / norm x) -- 0 --> 0"
  shows "(\<lambda>x. norm (r x) / norm x) -- 0 --> 0"
proof -
  have "(\<lambda>x. (\<Sum>i\<in>Basis. norm (r x \<bullet> i)) / norm x) -- 0 --> 0"
    by (auto simp: setsum_divide_distrib intro: tendsto_eq_intros assms)
  hence "(\<lambda>x. norm (\<Sum>i\<in>Basis. (r x \<bullet> i) *\<^sub>R i) / norm x) -- 0 --> 0"
    by (rule tendsto_0_le[where K=1]) (auto simp: eventually_at_filter field_simps order_trans[OF norm_setsum])
  thus ?thesis
    by (simp add: euclidean_representation)
qed

lemma Zfun_ident: "Zfun (\<lambda>x::'a::real_normed_vector. x) (at 0)"
  using tendsto_ident_at[of "0::'a" UNIV, simplified tendsto_Zfun_iff]
  by simp

lemma has_derivative_continuous_pderivsI:
  fixes f::"'a::euclidean_space\<Rightarrow>'b::euclidean_space" and x::'a
  assumes "x \<in> X" "open X"
  assumes df0: "\<And>x i. i \<in> Basis \<Longrightarrow> x \<in> X \<Longrightarrow> ((\<lambda>h. f (x + h *\<^sub>R i)) has_vector_derivative df x i) (at 0)"
  assumes df_cont: "\<And>i. i \<in> Basis \<Longrightarrow> continuous (at x) (\<lambda>x. df x i)"
  defines "Jf \<equiv> \<lambda>h. \<Sum>i\<in>Basis. (h \<bullet> i) *\<^sub>R (df x i)"
  shows "(f has_derivative Jf) (at x)"
proof -
  {
    fix x i::'a assume "i \<in> Basis" "x \<in> X"
    from df0[OF this]
    have "((\<lambda>y. y - x \<bullet> i) has_vector_derivative 1) (at (x \<bullet> i))"
      "((\<lambda>h. f (x + h *\<^sub>R i)) has_vector_derivative df x i) (at ((x \<bullet> i - x \<bullet> i)))"
      by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
    from vector_diff_chain_at[OF this]
    have "((\<lambda>y. f (x + (y - x \<bullet> i) *\<^sub>R i)) has_vector_derivative df x i) (at (x \<bullet> i))"
      by (simp add: o_def)
  } note df = this
  show ?thesis
    unfolding Deriv.has_derivative_at
  proof safe
    note df' = df[simplified has_vector_derivative_def]
    note bl = has_derivative_bounded_linear[OF df']
    {
      fix a
      have "norm (\<Sum>i\<in>Basis. (a \<bullet> i) *\<^sub>R df x i) \<le> (\<Sum>i\<in>Basis. norm ((a \<bullet> i) *\<^sub>R df x i))"
        by (rule norm_setsum)
      also have "\<dots> \<le> (\<Sum>i\<in>Basis. norm a * norm (df x i))"
        by (auto intro!: setsum_mono mult_right_mono Basis_le_norm)
      finally have "norm (\<Sum>i\<in>Basis. (a \<bullet> i) *\<^sub>R df x i) \<le> norm a * (\<Sum>i\<in>Basis. norm (df x i))"
        by (simp add: setsum_right_distrib)
    } note bound = this
    show "bounded_linear Jf"
      unfolding Jf_def
      using bound
      by unfold_locales (auto simp: algebra_simps setsum.distrib[symmetric]
        scaleR_setsum_right intro!: exI[where x="(\<Sum>i\<in>Basis. norm (df x i))"])
  next
    def r \<equiv> "\<lambda>h. f (x + h) - f x - Jf h"
    from openE[OF assms(2,1)]
    obtain d where d: "d > 0" "ball x d \<subseteq> X" .
    have hd: "eventually (\<lambda>h. norm h < d) (at 0)"
      using Zfun_ident `d > 0`
      by (rule ZfunD)
    {
      fix i::'b assume i: "i \<in> Basis"
      hence ri_eq: "\<And>h. r h \<bullet> i = f (x + h) \<bullet> i - f x \<bullet> i - (\<Sum>j\<in>Basis. (df x j \<bullet> i) * (h \<bullet> j))"
        by (auto simp: r_def algebra_simps Jf_def inner_setsum_left)
      {
        fix h::'a
        assume h: "norm h < d"
        def z \<equiv> "\<lambda>J. x + (\<Sum>k\<in>J. (h \<bullet> k) *\<^sub>R k)"
        {
          fix t j J
          assume J: "J \<subseteq> Basis" "j \<in> Basis" "j \<notin> J" "t \<in> closed_segment 0 (h \<bullet> j)"
          hence [simp]: "\<And>k. k \<in> J \<Longrightarrow> k \<in> Basis" "finite J"
            by (auto simp: finite_subset)
          have "norm (- (\<Sum>k\<in>J. (h \<bullet> k) *\<^sub>R k) - t *\<^sub>R j) \<le> norm h"
            apply (rule norm_le_componentwise)
            using i J
            by (auto intro!: mult_left_le_one_le simp: algebra_simps inner_Basis inner_setsum_left setsum_mult_delta closed_segment_def
              abs_mult)
          hence "z J + t *\<^sub>R j \<in> ball x d"
            using h by (auto simp: z_def dist_norm)
          also note d(2)
          finally have "z J + t *\<^sub>R j\<in> X" .
        } note seg = this
        have z_Basis: "z Basis = x + h" and z_empty: "z {} = x"
          by (auto simp: z_def euclidean_representation)
        {
          fix j and J::"'a set"
          assume jJ: "j \<in> Basis" "j \<notin> J" "J \<subseteq> Basis"
          hence [intro, simp]: "finite J"
            by (metis finite_Basis infinite_super)
          from jJ have z_insert: "z (insert j J) = z J + (h \<bullet> j) *\<^sub>R j"
            by (auto simp: z_def)
          def g \<equiv> "\<lambda>t. f (z J + t *\<^sub>R j) \<bullet> i"
          have comp: "\<lambda>x. f (z J + x *\<^sub>R j) \<equiv> (\<lambda>x. f (z J + (x - z J \<bullet> j) *\<^sub>R j)) o (op + (z J \<bullet> j))"
            by (auto simp: o_def)
          have "\<And>t. t \<in> closed_segment 0 (h \<bullet> j) \<Longrightarrow>
            (g has_vector_derivative df (z J + t *\<^sub>R j) j \<bullet> i) (at t within closed_segment 0 (h \<bullet> j))"
            apply (auto intro!: derivative_eq_intros simp: g_def has_vector_derivative_def comp)
            apply (rule refl)+
            apply (rule has_derivative_at_within)
            using df[unfolded has_vector_derivative_def, OF `j \<in> _`, of "z J + t *\<^sub>R j" for t, OF seg[OF jJ(3,1,2)]]
            apply (auto simp add: algebra_simps inner_Basis `j \<in> Basis`)
            done
          from mvt_closed_segmentE[of 0 "h \<bullet> j" g, OF this]
          obtain \<tau> where tau: "\<tau> \<in> closed_segment 0 (h \<bullet> j)" "g (h \<bullet> j) = g 0 + (h \<bullet> j - 0) * (df (z J + \<tau> *\<^sub>R j) j \<bullet> i)"
            by (auto simp: algebra_simps)
          with tau have "\<exists>\<tau> \<in> closed_segment 0 (h \<bullet> j). f (z (insert j J)) \<bullet> i = f (z J) \<bullet> i + (df (z J + \<tau> *\<^sub>R j) j \<bullet> i) * (h \<bullet> j)"
            by (auto simp: z_insert g_def closed_segment_def algebra_simps)
        } then obtain \<tau> where tau:
          "\<And>j J. j \<in> Basis \<Longrightarrow> j \<notin> J \<Longrightarrow> J \<subseteq> Basis \<Longrightarrow> \<tau> j J \<in> closed_segment 0 (h \<bullet> j)"
          "\<And>j J. j \<in> Basis \<Longrightarrow> j \<notin> J \<Longrightarrow> J \<subseteq> Basis \<Longrightarrow> f (z (insert j J)) \<bullet> i = f (z J) \<bullet> i + (df (z J + \<tau> j J *\<^sub>R j) j \<bullet> i) * (h \<bullet> j)"
          by metis
        def \<eta> \<equiv> "\<lambda>j J. z J + \<tau> j J *\<^sub>R j"
        obtain Bl::"'a list" where Bl: "set Bl = Basis" "distinct Bl"
          by (metis finite_Basis finite_distinct_list)
        from set_telescope[OF `distinct Bl`, of "\<lambda>J. f (z J) \<bullet> i", OF tau(2)]
        obtain s where "f (x + h) \<bullet> i - f x \<bullet> i = (\<Sum>j\<in>Basis. df (\<eta> j (s j)) j \<bullet> i * (h \<bullet> j))"
          (is "_ = ?etas")
          and s: "\<And>i. i \<in> Basis \<Longrightarrow> i \<notin> s i" "\<And>i. i \<in> Basis \<Longrightarrow> s i \<subseteq> Basis"
          unfolding Bl z_Basis z_empty \<eta>_def
          by blast
        hence "r h \<bullet> i = ?etas - (\<Sum>j\<in>Basis. (df x j \<bullet> i) * (h \<bullet> j))"
          by (auto simp: ri_eq)
        also have "\<dots> = (\<Sum>j\<in>Basis. (df (\<eta> j (s j)) j \<bullet> i - df x j \<bullet> i) * (h \<bullet> j))"
          by (simp add: setsum_subtractf listsum_distinct_conv_setsum_set distinct_headsI Bl
            algebra_simps)
        also have "abs \<dots> \<le> norm h * (\<Sum>j\<in>Basis. abs (df (\<eta> j (s j)) j \<bullet> i - df x j \<bullet> i))"
          apply (rule order_trans[OF setsum_abs])
          apply (rule order_trans[OF setsum_mono])
          unfolding abs_mult
          apply (rule mult_left_mono[OF Basis_le_norm])
          apply (force simp add: Bl(1) dest!: in_set_heads_last_in_set)
          apply simp
          apply (simp add: setsum_right_distrib ac_simps)
          done
        also have "\<dots> = norm h *
          (\<Sum>j\<in>Basis.
            \<bar>df (x + ((\<Sum>k\<in>s j. (h \<bullet> k) *\<^sub>R k) + \<tau> j (s j) *\<^sub>R j)) j \<bullet> i -
             df x j \<bullet> i\<bar>)"
          (is "_ = _ * (setsum (\<lambda>i. _ (x + ?r i))) _")
          by (auto simp: \<eta>_def z_def ac_simps)
        finally have "\<bar>r h \<bullet> i\<bar> \<le> norm h * (\<Sum>xa\<in>Basis. \<bar>(df (x + ?r xa) (xa) - df x xa) \<bullet> i\<bar>)"
          by (auto simp: algebra_simps)
        moreover
        {
          fix i::'a
          assume i: "i \<in> Basis"
          have *: "\<And>x. x \<in> insert i (s i) \<Longrightarrow> x \<in> Basis"
            using s i by auto
          have in_set_ne_last: "\<And>k. k\<in>s i \<Longrightarrow> k \<noteq> i"
            using s[OF i] by auto
          have "\<tau> i (s i) \<in> closed_segment 0 (h \<bullet> i)"
            using s[OF i] i by (auto intro!: tau)
          hence tau_le_h: "abs (\<tau> i (s i)) \<le> abs (h \<bullet> i)"
            by (auto simp: closed_segment_def abs_mult intro!: mult_left_le_one_le)
          have "norm (?r i) = norm (\<Sum>k\<in>insert i (s i).
            (if k = i then \<tau> i (s i) else (h \<bullet> k)) *\<^sub>R k)"
            using i s[OF i]
            by (subst setsum.insert) (auto simp: algebra_simps in_set_ne_last finite_subset)
          also have "\<dots> \<le> norm (\<Sum>k\<in>Basis. (h \<bullet> k) *\<^sub>R k)"
            apply (rule norm_le_componentwise)
            using s[OF i]
            apply (auto simp: inner_setsum_left * inner_Basis setsum_mult_delta)
            apply (subst setsum_mult_delta)
            apply (auto simp: tau_le_h finite_subset)
            done
          also have "\<dots> \<le> norm h"
            by (simp add: euclidean_representation)
          finally have "norm (?r i) \<le> norm h" .
        }
        ultimately
        have "\<exists>tau. \<bar>r h \<bullet> i\<bar> \<le> norm h * (\<Sum>xa\<in>Basis. \<bar>(df (x + tau xa) xa - df x xa) \<bullet> i\<bar>) \<and>
            (\<forall>i \<in> Basis. norm (tau i) \<le> norm h)"
          by force
      }
    }
    hence "\<forall>i \<in> Basis. \<forall>h. (\<exists>tau. norm h < d \<longrightarrow>\<bar>r h \<bullet> i\<bar> \<le> norm h * (\<Sum>xa\<in>Basis. \<bar>(df (x + tau xa) xa - df x xa) \<bullet> i\<bar>) \<and>
          (\<forall>i\<in>Basis. norm (tau i) \<le> norm h))"
      by auto
    from this[simplified choice_iff bchoice_iff]
    obtain tau where tau:
      "\<And>h i. i \<in> Basis \<Longrightarrow> norm h < d \<Longrightarrow> \<bar>r h \<bullet> i\<bar> \<le> norm h * (\<Sum>xa\<in>Basis. \<bar>(df (x + tau i h xa) xa - df x xa) \<bullet> i\<bar>)"
      (is "\<And>h i. _ \<Longrightarrow> _ \<Longrightarrow> _ h \<le> norm h * ?s i h")
      "\<And>h i j. i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> norm h < d \<Longrightarrow> norm (tau i h j) \<le> norm h"
      by auto
    have ene: "eventually (\<lambda>h::'a. h \<noteq> 0) (at 0)"
      by (auto simp: eventually_at_filter)
    {
      fix i::'b assume "i \<in> Basis"
      {
        fix j::'a and i::'b assume "j \<in> Basis" "i \<in> Basis"
        have df_cont: "(\<lambda>h. df (x + h) j) -- 0 --> df x j"
          using df_cont[OF `j \<in> _`, simplified isCont_def]
          by (subst (asm) LIM_offset_zero_iff)
        have tau_zero: "(\<lambda>h. tau i h j) -- 0 --> 0"
          using tendsto_ident_at
          apply (rule tendsto_0_le[where K=1])
          using hd
          apply eventually_elim
          using tau(2)[OF `i\<in>Basis` `j \<in> Basis`]
          by auto
        have "(\<lambda>h. (df (x + tau i h j) j - df x j)) -- 0 --> 0"
          using LIM_o[OF df_cont[THEN tendsto_eq_rhs] tau_zero]
          by (auto simp: o_def LIM_zero_iff)
      } note df = this
      have "(?s i) -- 0 --> 0"
        apply (rule tendsto_eq_rhs)
        apply (rule tendsto_setsum)
        apply (rule tendsto_intros)
        apply (rule tendsto_intros)
        apply (rule df)
        apply assumption
        apply (rule `i \<in> Basis`)
        apply (rule tendsto_intros)
        apply simp
        done
    } hence s: "\<And>i. i \<in> Basis \<Longrightarrow> (?s i) -- 0 --> 0"
      by simp
    have "(\<lambda>x. norm (r x) / norm x) -- 0 --> 0"
      apply (rule norm_divide_tendsto_componentwiseI)
      using s
      apply (rule tendsto_0_le[where K=1])
      apply assumption
      using ene hd
      apply eventually_elim
      using tau
      apply (simp add: field_simps)
      done
    thus "(\<lambda>h. norm (f (x + h) - f x - Jf h) / norm h) -- 0 --> 0"
      by (auto simp: r_def)
  qed
qed

text {* TODO:
  - Orbit / Invariant Set
  - Manifolds / Submanifolds
*}

context c1_on_open
begin

text {* forward time... *}

definition flowsto::"'a set \<Rightarrow> 'a \<Rightarrow> bool"
  where "flowsto S x = (\<exists>t \<in> existence_ivl x. t \<ge> 0 \<and> flow x t \<in> S)"

definition flowtime::"'a set \<Rightarrow> 'a \<Rightarrow> real"
  where "flowtime S x = Inf {t. t \<in> existence_ivl x \<and> t \<ge> 0 \<and> flow x t \<in> S}"

definition poincare::"'a set \<Rightarrow> 'a \<Rightarrow> 'a"
  where "poincare S x = flow x (flowtime S x)"

context
  fixes x::'a and S::"'a set"
  assumes flowsto: "flowsto S x"
  assumes closed: "closed S"
  assumes in_domain: "x \<in> X"
begin

lemma flowtime:
  "flowtime S x \<in> existence_ivl x" "flowtime S x \<ge> 0" "flow x (flowtime S x) \<in> S"
  "\<And>t. t \<in> existence_ivl x \<Longrightarrow> t \<ge> 0 \<Longrightarrow> flow x t \<in> S \<Longrightarrow> flowtime S x \<le> t"
proof -
  let ?S = "{t. t \<in> existence_ivl x \<and> t \<ge> 0 \<and> flow x t \<in> S}"
  have "bdd_below ?S" by auto
  from flowsto obtain t where t: "t \<in> existence_ivl x" "t \<ge> 0" "flow x t \<in> S"
    by (auto simp: flowsto_def)
  hence "t \<in> ?S" by auto
  from cInf_lower[OF this `bdd_below ?S`]
  have "flowtime S x \<le> t" by (auto simp: flowtime_def)

  note subset = ivl_subset_existence_ivl[OF in_domain t(1)]

  have "?S = ({0 .. t} \<inter> existence_ivl x \<inter> flow x -` S) \<union> ({t ..} \<inter> existence_ivl x \<inter> flow x -` S)"
    (is "_ = ?S1 \<union> ?S2")
    using t by (auto simp: )
  also have "Inf \<dots> = Inf ({0 .. t} \<inter> existence_ivl x \<inter> flow x -` S)"
    using t
    apply (subst cInf_union_distrib)
    apply (auto simp: inf_real_def min_def)
  proof -
    case goal1
    have "Inf ?S1 \<le> t"
      using t by (auto intro!: cInf_lower)
    also have "t \<le> Inf ?S2"
      using t by (auto intro!: cInf_greatest)
    finally show ?case .
  qed
  also
  have "{0 .. t} \<inter> existence_ivl x = {0 .. t}"
    using ivl_subset_existence_ivl[OF in_domain t(1)]
    by auto
  finally
  have flowtime_eq: "flowtime S x = Inf (flow x -` S \<inter> {0..t})"
    (is "_ = Inf ?T")
    by (simp add: flowtime_def Int_commute)
  have "continuous_on {0 .. t} (flow x)"
    apply (rule has_derivative_continuous_on)
    apply (rule has_derivative_subset[OF ])
    apply (rule flow_has_derivative)
    apply (rule in_domain)
    using subset
    apply (auto simp: in_domain)
    done
  hence "?T \<noteq> {}" "bdd_below ?T" "closed ?T"
    using t
    by (auto simp add: continuous_on_closed_vimage closed)
  from closed_contains_Inf[OF this]
  have flowtime_in: "flowtime S x \<in> ?T"
    by (auto simp: flowtime_eq)
  case goal1
  show ?case using flowtime_in subset by auto
  case goal2
  show ?case using flowtime_in subset by auto
  case goal3
  show ?case using flowtime_in subset by auto
  case (goal4 s)
  thus ?case
    unfolding flowtime_def
    by (auto intro!: cInf_lower)
qed

lemma
  poincare_has_derivative:
  assumes "x \<in> X"
  assumes dflowtime':  "(flowtime S has_derivative dflowtime) (at x)"
  assumes flow_deriv: "\<And>x t i. i \<in> Basis \<Longrightarrow> x \<in> X \<Longrightarrow> t \<in> existence_ivl x \<Longrightarrow>
    ((\<lambda>h. flow (x + h *\<^sub>R i) t) has_vector_derivative dflow x t i) (at 0)"
  assumes dflow_cont: "\<And>i. i \<in> Basis \<Longrightarrow> isCont (\<lambda>(x, t). dflow x t i) (x, flowtime S x)"
  shows "(poincare S has_derivative (\<lambda>h. (\<Sum>i\<in>Basis. (h \<bullet> i) *\<^sub>R dflow x (flowtime S x) i) +
         dflowtime h *\<^sub>R f (flow x (flowtime S x)))) (at x)"
proof -
  have poinc_o: "poincare S = (\<lambda>(x, t). flow x t) o (\<lambda>x. (x, flowtime S x))"
    by (auto simp: poincare_def)
  show ?thesis
    apply (rule has_derivative_eq_rhs)
    unfolding poinc_o
    apply (rule diff_chain_at)
    apply (rule derivative_intros)
    apply (rule derivative_intros)
    apply (rule dflowtime')
  proof (rule has_derivative_continuous_pderivsI[where X="Sigma X existence_ivl" and df="\<lambda>(x, t) (i, j). if j = 0 then dflow x t i else f (flow x t)"])
    case goal1
    thus ?case by (auto intro!: assms flowtime)
  next
    case goal2 show ?case by (rule open_state_space)
  next
    case goal3
    thus ?case
      apply (cases i)
      apply (auto simp: in_Basis_prod_iff)
      apply (rule flow_has_vector_derivative_at_0)
      apply simp
      apply simp
      apply (rule flow_deriv)
      apply simp
      apply simp
      apply simp
      done
  next
    case goal4
    have "isCont (f o (\<lambda>(x, t). c1_on_open.flow f X x t)) (x, flowtime S x)"
      apply (rule continuous_intros)
      apply (auto intro!: flow_isCont_state_space assms flowtime f_continuous flow_in_domain)
      done
    with goal4
    show ?case
      using dflow_cont
      apply (cases i)
      by (auto simp: in_Basis_prod_iff split_beta' o_def intro!: continuous_intros)
  next
    case goal5
    thus ?case
      apply (rule )
      apply (auto simp: split_beta setsum_Basis_prod_eq)
      done
  qed
qed

lemma
  poincare_has_derivative':
  assumes "x \<in> X"
  assumes dflowtime': "(flowtime S has_derivative dflowtime) (at x)"
  assumes flow_deriv: "\<And>x t. x \<in> X \<Longrightarrow> t \<in> existence_ivl x \<Longrightarrow>
    ((\<lambda>x. flow x t) has_derivative blinfun_apply (dflow (x, t))) (at x)"
  assumes "continuous (at (x, flowtime S x)) dflow"
  shows "(poincare S has_derivative (\<lambda>h. dflow (x, flowtime S x) h +
         dflowtime h *\<^sub>R f (c1_on_open.flow f X x (flowtime S x)))) (at x)"
proof -
  interpret linear "blinfun_apply (dflow (x, flowtime S x))"
    by (metis flow_deriv flowtime(1) has_derivative_linear in_domain)
  have "(poincare S has_derivative (\<lambda>h. (\<Sum>i\<in>Basis. (h \<bullet> i) *\<^sub>R dflow (x, flowtime S x) i) +
         dflowtime h *\<^sub>R f (c1_on_open.flow f X x (flowtime S x)))) (at x)"
    apply (rule poincare_has_derivative[OF assms(1,2)])
    apply (auto simp: has_vector_derivative_def)
  proof -
    case goal1
    note fd = flow_deriv[OF `x \<in> X` `t \<in> _`]
    from fd have
      "((\<lambda>h. x + h *\<^sub>R i) has_derivative (\<lambda>x. x *\<^sub>R i)) (at 0)"
      "((\<lambda>x. c1_on_open.flow f X x t) has_derivative dflow (x, t)) (at (x + 0 *\<^sub>R i))"
      by (auto intro!: derivative_eq_intros)
    from diff_chain_at[OF this]
    show ?case
      by (auto simp: o_def)
  next
    case goal2
    thus ?case
      using assms(4)
      by (auto simp: split_beta' continuous_blinfun_apply)
  qed
  thus ?thesis
    by (simp add: scaleR[symmetric] setsum[symmetric] euclidean_representation
      del: blinfun_apply_scaleR)
qed

end

end
