section {* Runge Kutta methods on Affine Forms *}
theory Euler_Affine
imports
  "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
  "../IVP/Flow"
  Euler_Affine_Code
begin
text {* \label{sec:rk-affine} *}
sledgehammer_params [fact_filter=mepo]

lemma scaleR_mono'':
  fixes a b and c d::"'a::ordered_real_vector"
  shows "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> d \<Longrightarrow> a *\<^sub>R c \<le> b *\<^sub>R d"
  by (metis order_trans scaleR_left_mono scaleR_right_mono)

lemma
  scaleR_mono_neg:
  fixes a b and c::"'a::ordered_euclidean_space"
  assumes "0 \<le> b" "b \<le> a" "d \<le> 0" "d \<le> c"
  shows "a *\<^sub>R d \<le> b *\<^sub>R c"
proof -
  have "b *\<^sub>R (-c) \<le> a *\<^sub>R (-d)"
    apply (rule scaleR_mono'')
    using assms
    apply auto
    done
  thus ?thesis by auto
qed

lemma scaleR_inf_eq:
  fixes a b::"'a::ordered_euclidean_space"
  shows "h *\<^sub>R inf a b = (if h \<ge> 0 then inf (h *\<^sub>R a) (h *\<^sub>R b) else sup (h *\<^sub>R a) (h *\<^sub>R b))"
  apply (auto simp: eucl_inf[where 'a='a] scaleR_setsum_right inf_real_def eucl_sup[where 'a='a] sup_real_def)
  apply (rule setsum.cong)
  apply (auto simp: min_def)
  apply (metis le_less mult_le_cancel_left)
  apply (rule setsum.cong)
  apply (auto simp: max_def)
  done

lemma scaleR_sup_eq:
  fixes a b::"'a::ordered_euclidean_space"
  shows "h *\<^sub>R sup a b = (if h \<ge> 0 then sup (h *\<^sub>R a) (h *\<^sub>R b) else inf (h *\<^sub>R a) (h *\<^sub>R b))"
  apply (auto simp: eucl_inf[where 'a='a] scaleR_setsum_right inf_real_def eucl_sup[where 'a='a] sup_real_def)
  apply (rule setsum.cong)
  apply (auto simp: max_def)
  apply (metis le_less mult_le_cancel_left)
  apply (rule setsum.cong)
  apply (auto simp: min_def)
  done

lemma prod_Basis_cases:
  fixes x::"'a::euclidean_space * 'b::euclidean_space "
  assumes "x \<in> Basis"
  obtains "fst x \<in> Basis" "snd x = 0" | "snd x \<in> Basis " "fst x = 0"
  using assms by (auto simp: Basis_prod_def)

text{*\label{sec:euleraform}*}

lemma inf_le_sup_same1: "inf a (b::'a::ordered_euclidean_space) \<le> sup a d"
  by (metis inf.coboundedI1 sup.cobounded1)

lemma fixes a::"'a option"
  shows split_option_bind: "P (a \<guillemotright>= f) \<longleftrightarrow> ((a = None \<longrightarrow> P None) \<and> (\<forall>x. a = Some x \<longrightarrow> P (f x)))"
  and split_option_bind_asm:  "P (a \<guillemotright>= f) \<longleftrightarrow> (\<not> (a = None \<and> \<not> P None \<or> (\<exists>x. a = Some x \<and> \<not> P (f x))))"
  unfolding atomize_conj
  by (cases a) (auto split: option.split)

lemma msum_subsetI:
  assumes "X \<subseteq> X'" "Y \<subseteq> Y'"
  shows "{(x::'a::group_add) + y |x y. x \<in> X \<and> y \<in> Y} \<subseteq> {x + y |x y. x \<in> X' \<and> y \<in> Y'}"
proof safe
  fix x y
  assume xy: "x \<in> X" "y \<in> Y"
  show "\<exists>x' y'. x + y = x' + y' \<and> x' \<in> X' \<and> y' \<in> Y'"
    apply (rule exI[where x=x])
    apply (rule exI[where x=y])
    using xy assms by auto
qed

subsection {* operations on intervals *}

text {* include separate type of intervals in @{text approximate_sets0} *}

type_synonym 'a ivl = "'a*'a"

definition set_of_ivl::"'a ivl \<Rightarrow> 'a::executable_euclidean_space set"
  where "set_of_ivl x = {fst x .. snd x}"

definition split_ivl::"'a ivl \<Rightarrow> real \<Rightarrow> 'a \<Rightarrow> 'a ivl * 'a::executable_euclidean_space ivl"
  where "split_ivl x s i = ((fst x, snd x + (s - snd x \<bullet> i)*\<^sub>Ri), (fst x + (s - fst x \<bullet> i)*\<^sub>Ri, snd x))"

lemma split_ivl:
  assumes "i \<in> Basis"
  assumes "s \<in> {fst X \<bullet> i .. snd X \<bullet> i}"
  shows "x \<in> set_of_ivl X \<longleftrightarrow> x \<in> (set_of_ivl (fst (split_ivl X s i)) \<union> set_of_ivl (snd (split_ivl X s i)))"
  using assms
  by (auto simp: set_of_ivl_def split_ivl_def eucl_le[where 'a='a] not_le algebra_simps inner_Basis)


fun Pair_of_list::"'a list \<Rightarrow> 'a*'a" where
  "Pair_of_list [a, b] = (a, b)"
fun Triple_of_list::"'a list \<Rightarrow> 'a*'a*'a" where
  "Triple_of_list [a, b, c] = (a, b, c)"

locale approximate_sets = approximate_sets0 +
  assumes msum_appr_eq: "set_of_appr (msum_appr X Y) = {x + y |x y. x \<in> set_of_appr X \<and> y \<in> set_of_appr Y}"
  assumes inf_of_appr_msum_appr: "inf_of_appr (msum_appr X Y) = inf_of_appr X + inf_of_appr Y"
  assumes sup_of_appr_msum_appr: "sup_of_appr (msum_appr X Y) = sup_of_appr X + sup_of_appr Y"
  assumes inf_of_appr_Inf: "inf_of_appr X \<le> Inf (set_of_appr X)"
  assumes sup_of_appr_Sup: "sup_of_appr X \<ge> Sup (set_of_appr X)"
  assumes sup_of_appr_of_ivl: "l \<le> u \<Longrightarrow> sup_of_appr (appr_of_ivl l u) = u"
  assumes inf_of_appr_of_ivl: "l \<le> u \<Longrightarrow> inf_of_appr (appr_of_ivl l u) = l"
  assumes set_of_appr_of_ivl: "l \<le> u \<Longrightarrow> set_of_appr (appr_of_ivl l u) = {l .. u}"
  assumes set_of_appr_nonempty: "set_of_appr X \<noteq> {}"
  assumes set_of_appr_compact: "compact (set_of_appr X)"
  assumes set_of_appr_convex: "convex (set_of_appr X)"
  assumes set_of_apprs_set_of_appr: "[x] \<in> set_of_apprs [X] \<longleftrightarrow> x \<in> set_of_appr X"
  assumes set_of_apprs_switch: "x#y#xs \<in> set_of_apprs (X#Y#XS) \<Longrightarrow> y#x#xs \<in> set_of_apprs (Y#X#XS)"
  assumes set_of_apprs_rotate: "x#y#xs \<in> set_of_apprs (X#Y#XS) \<Longrightarrow> y#xs@[x] \<in> set_of_apprs (Y#XS@[X])" --"TODO: better use the set (zip ...) property?"
  assumes set_of_apprs_Nil: "xs \<in> set_of_apprs [] \<Longrightarrow> xs = []"
  assumes length_set_of_apprs: "xs \<in> set_of_apprs XS \<Longrightarrow> length xs = length XS"
  assumes set_of_apprs_imp': "xs \<in> set_of_apprs XS \<longrightarrow> length xs = length XS \<longrightarrow> length ys = length YS \<longrightarrow> set (zip ys YS) \<subseteq> set (zip xs XS) \<longrightarrow> ys \<in> set_of_apprs YS"
  assumes set_of_apprs_Cons_ex: "xs \<in> set_of_apprs (X#XS) \<Longrightarrow> (\<exists>y ys. xs = y#ys \<and> y \<in> set_of_appr X \<and> ys \<in> set_of_apprs XS)"
  assumes in_image_Pair_of_listI[simp, intro]:
    "[x, y] \<in> set_of_apprs [X, Y] \<Longrightarrow> (x, y) \<in> Pair_of_list ` set_of_apprs [X, Y]"
  assumes in_image_Triple_of_listI[simp, intro]:
    "[x, y, z] \<in> set_of_apprs [X, Y, Z] \<Longrightarrow> (x, y, z) \<in> Triple_of_list ` set_of_apprs [X, Y, Z]"
  assumes add_appr: "(x # y # ys) \<in> set_of_apprs (X # Y # YS) \<Longrightarrow> (add_appr optns X Y YS) = Some S \<Longrightarrow> (x + y)#x#y#ys \<in> set_of_apprs (S#X#Y#YS)"
  assumes scale_appr: "(x#xs) \<in> set_of_apprs (X#XS) \<Longrightarrow> (scale_appr optns r s X XS) = Some S \<Longrightarrow> ((r/s) *\<^sub>R x # x # xs) \<in> set_of_apprs (S#X#XS)"
  assumes scale_appr_ivl: "s \<in> {r..t} \<Longrightarrow> (x#xs) \<in> set_of_apprs (X#XS) \<Longrightarrow> (scale_appr_ivl optns r t X XS) = Some S \<Longrightarrow> (s *\<^sub>R x # x # xs) \<in> set_of_apprs (S#X#XS)"
  assumes split_appr: "x \<in> set_of_appr X \<Longrightarrow> list_ex (\<lambda>X. x \<in> set_of_appr X) (split_appr optns X)"
  assumes inter_appr_plane: "inter_appr_plane optns X sctn = Some Y \<Longrightarrow> set_of_appr X \<inter> plane_of sctn \<subseteq> set_of_appr Y"
  assumes appr_inf_inner: "x \<in> set_of_appr X \<Longrightarrow> appr_inf_inner optns X y \<le> x \<bullet> y"
  assumes appr_sup_inner: "x \<in> set_of_appr X \<Longrightarrow> appr_sup_inner optns X y \<ge> x \<bullet> y"
  assumes reduce_appr: "set_of_appr X \<subseteq> set_of_appr (reduce_appr optns X)"
  assumes independent_appr: "x \<in> set_of_appr X \<Longrightarrow> y \<in> set_of_appr Y \<Longrightarrow> [x, y] \<in> set_of_apprs [X, independent_appr X Y]"
  assumes independent_appr_eq: "set_of_appr (independent_appr X Y) = set_of_appr Y"
begin

lemma set_of_apprs_imp:
  "xs \<in> set_of_apprs XS \<Longrightarrow> length xs = length XS \<Longrightarrow> length ys = length YS \<Longrightarrow> set (zip ys YS) \<subseteq> set (zip xs XS) \<Longrightarrow> ys \<in> set_of_apprs YS"
  using set_of_apprs_imp' by blast

lemma set_of_appr_bounded[intro]: "bounded (set_of_appr X)"
  by (rule compact_imp_bounded) (rule set_of_appr_compact)

lemma inf_of_appr[simp]: "x \<in> set_of_appr X \<Longrightarrow> inf_of_appr X \<le> x"
  by (auto intro!: order_trans[OF inf_of_appr_Inf] cInf_lower bounded_imp_bdd_below)

lemma sup_of_appr[simp]: "x \<in> set_of_appr X \<Longrightarrow> x \<le> sup_of_appr X"
  by (auto intro!: order_trans[OF _ sup_of_appr_Sup] cSup_upper bounded_imp_bdd_above)

lemma inf_of_appr_le_sup_of_appr[simp]:
  "inf_of_appr a \<le> sup_of_appr a"
  using set_of_appr_nonempty[of a] order_trans[OF inf_of_appr sup_of_appr]
  by auto

lemma set_of_apprs_Cons: "x#xs \<in> set_of_apprs (X#XS) \<Longrightarrow> xs \<in> set_of_apprs XS"
  by (auto dest: set_of_apprs_Cons_ex)

lemma set_of_apprsE:
  assumes "xs \<in> set_of_apprs (X#XS)"
  obtains y ys where "xs = y # ys" "y \<in> set_of_appr X" "ys \<in> set_of_apprs XS"
  using set_of_apprs_Cons_ex assms by blast

lemma set_of_apprs_rotate3:
  "[x,y, z] \<in> set_of_apprs [X, Y, Z] \<Longrightarrow> [y, z, x] \<in> set_of_apprs [Y,Z,X]"
  by (metis Cons_eq_appendI eq_Nil_appendI set_of_apprs_rotate)

lemma
  intersects_appr: "\<not>intersects_appr optns X sctn \<Longrightarrow> set_of_appr X \<inter> plane_of sctn = {}"
  using appr_inf_inner[of _ X optns "normal sctn"] appr_sup_inner[of _ X "normal sctn" optns]
  apply (auto simp: intersects_appr_def not_le plane_of_def)
  apply (metis not_le)+
  done

lemma
  appr_above_sctn: "appr_above_sctn optns X sctn \<Longrightarrow> x \<in> set_of_appr X \<Longrightarrow> \<not>le_halfspace sctn x"
  by (auto simp: appr_above_sctn_def not_le le_halfspace_def less_le_trans appr_inf_inner)

lemma
  appr_below_sctn: "appr_below_sctn optns X sctn \<Longrightarrow> x \<in> set_of_appr X \<Longrightarrow> le_halfspace sctn x"
  apply (auto simp: appr_below_sctn_def not_le le_halfspace_def less_le_trans appr_sup_inner order_trans)
  by (metis appr_sup_inner order_trans)

lemma disjoint_apprs:
  assumes "disjoint_apprs X Y"
  shows "set_of_appr X \<inter> set_of_appr Y = {}"
proof -
  have "set_of_appr X \<subseteq> {inf_of_appr X .. sup_of_appr X}"
    "set_of_appr Y \<subseteq> {inf_of_appr Y .. sup_of_appr Y}"
    by auto
  moreover
  from assms have "{inf_of_appr X .. sup_of_appr X} \<inter> {inf_of_appr Y .. sup_of_appr Y} = {}"
    apply (auto simp: list_ex_iff disjoint_apprs_def
      algebra_simps eucl_le[where 'a='a])
    apply (metis le_less_trans not_le)
    apply (metis le_less_trans not_le)
    done
  ultimately show ?thesis by auto
qed

lemma in_set_of_appr_msum_apprI:
  assumes "z = x + y"
  assumes "x \<in> set_of_appr X" "y \<in> set_of_appr Y"
  shows "z \<in> set_of_appr (msum_appr X Y)"
  unfolding msum_appr_eq assms
  using assms by force
end

lemma tendsto_singleton[tendsto_intros]: "(f ---> f x) (at x within {x})"
  by (auto simp: tendsto_def eventually_at_filter)

lemma continuous_on_singleton[continuous_intros]: "continuous_on {x} f"
  unfolding continuous_on_def
  by (auto intro!: tendsto_singleton)

locale approximate_ivp = approximate_ivp0 + approximate_sets +
  fixes ode::"'a  \<Rightarrow> 'a"
  fixes ode_d::"'a \<Rightarrow> 'a \<Rightarrow> 'a"
  fixes ode_d2::"'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  assumes ode_approx:
    "x#xs \<in> set_of_apprs (X'#XS) \<Longrightarrow>
    ode_approx optns (X'#XS) = Some A \<Longrightarrow>
    (ode x#x#xs) \<in> set_of_apprs (A#X'#XS)"
  assumes fderiv[derivative_intros]: "(ode has_derivative ode_d x) (at x)"
  assumes fderiv2[derivative_intros]:
    "((\<lambda>x. ode_d x dx) has_derivative ode_d2 x dx) (at x)"
  assumes ode_d_approx:
    "x#dx#xs \<in> set_of_apprs (X'#DX'#XS) \<Longrightarrow>
     ode_d_approx optns (X'#DX'#XS) = (Some D') \<Longrightarrow>
     ode_d x dx#x#dx#xs \<in> set_of_apprs (D'#X'#DX'#XS)"
  assumes ode_d2_approx:
    "x#dx#dx2#xs \<in> set_of_apprs (X' # DX' # DX2' # XS) \<Longrightarrow>
     ode_d2_approx optns (X' # DX' # DX2' # XS) = (Some D') \<Longrightarrow>
     ode_d2 x dx dx2 # x # dx # dx2 # xs \<in> set_of_apprs (D' # X' # DX' # DX2' # XS)"
  assumes cont_fderiv2: "i \<in> Basis \<Longrightarrow> j \<in> Basis \<Longrightarrow> continuous_on UNIV (\<lambda>x. ode_d2 x i j)"
begin

lemma cont_fderiv: "i \<in> Basis \<Longrightarrow> continuous_on UNIV (\<lambda>x. ode_d x i)"
  by (rule has_derivative_continuous_on) (rule derivative_intros)

lemma Blinfun_ode_d_reverse[simp]: "blinfun_apply (Blinfun (ode_d x)) = ode_d x"
  using fderiv
  by (metis bounded_linear_Blinfun_apply comp_id fun.map_cong0 has_derivative_bounded_linear)

sublocale c1_on_open ode "Blinfun o ode_d" UNIV
  using cont_fderiv
  by unfold_locales
    (auto simp: continuous_on_eq_continuous_within at_within_open[symmetric]
      intro!: derivative_eq_intros cont_fderiv continuous_at_imp_continuous_on continuous_blinfun_componentwiseI)

lemma fderiv'[derivative_intros]:
  "((\<lambda>(t, y). ode y) has_derivative (\<lambda>(t, x) (dt, dx). ode_d x dx) (t, x)) (at (t, x) within X)"
  by (auto intro!: derivative_eq_intros has_derivative_compose[of snd])

lemma picard_approx:
  assumes appr: "ode_approx optns [X] = Some Y"
  assumes bb: "inf_of_appr Y = l" "sup_of_appr Y = u"
  assumes x_in: "(\<And>t. t \<in> {t0 .. t1} \<Longrightarrow> x t \<in> set_of_appr X)"
  assumes cont: "continuous_on {t0 .. t1} x"
  assumes ivl: "t0 \<le> t1"
  shows "x0 + integral {t0..t1} (\<lambda>t. ode (x t)) \<in> {x0 + (t1 - t0) *\<^sub>R l .. x0 + (t1 - t0) *\<^sub>R u}"
proof -
  {
    fix t::real
    assume "0 \<le> t" "t \<le> 1"
    hence "t * (t1 - t0) \<le> t1 - t0" using ivl
      by (auto intro!: mult_left_le_one_le )
    hence "t0 + t * (t1 - t0) \<le> t1"
      by (simp add: algebra_simps)
  } note segment[simp] = this
  {
    fix t::real
    assume t: "t \<in> {0 .. 1}"
    have "ode (x (t0 + t * (t1 - t0))) \<in> set_of_appr Y"
      unfolding set_of_apprs_set_of_appr[symmetric]
      apply (rule set_of_apprs_Cons)
      apply (rule set_of_apprs_switch)
      apply (rule ode_approx[OF _ appr])
      using t ivl
      by (auto intro!: x_in ode_approx simp: set_of_apprs_set_of_appr)
    also from bb inf_of_appr sup_of_appr have "set_of_appr Y \<subseteq> {l..u}" by auto
    finally have "ode (x (t0 + t * (t1 - t0))) \<in> {l..u}" .
  } note ode_lu = this
  have cont_ode_x: "continuous_on {t0..t1} (\<lambda>xa. ode (x xa))"
    apply (rule continuous_on_compose2[of _ ode _ x])
    apply (rule continuous_on_subset)
    apply (rule has_derivative_continuous_on[OF fderiv])
    by (auto intro!: has_derivative_continuous_on[OF fderiv] continuous_on_compose2[of _ ode _ x]
      cont)
  have cmp: "(\<lambda>t. ode (x (t0 + t * (t1 - t0)))) = (\<lambda>t. ode (x t)) o (\<lambda>t. (t0 + t * (t1 - t0)))"
    by auto
  have cnt: "continuous_on {0 .. 1}(\<lambda>t. ode (x (t0 + t * (t1 - t0))))"
    unfolding cmp using ivl
    by (intro continuous_on_compose)
      (auto intro!: continuous_intros simp: image_linear_atLeastAtMost cont_ode_x not_less)
  have "integral {t0..t1} (\<lambda>t. ode (x t)) =
    (t1 - t0) *\<^sub>R integral {0..1} (\<lambda>t. ode (x (t0 + t * (t1 - t0))))"
    using ivl
    by (intro mvt_integral(2)[of _ "\<lambda>t1. integral {t0..t1} (\<lambda>t. ode (x t))" "\<lambda>t u. u *\<^sub>R ode (x t)"
        t0 "t1 - t0", simplified, OF _ cont_ode_x])
      (auto intro!: integral_has_vector_derivative[OF cont_ode_x]
      simp: has_vector_derivative_def[symmetric])
  also
  {
    have "integral {0..1} (\<lambda>t. ode (x (t0 + t * (t1 - t0)))) \<le> integral {0..1} (\<lambda>t::real . u)"
      using ode_lu
      by (auto simp: eucl_le[where 'a='a] intro!: order_trans[OF integral_component_ubound_real] cnt)
    moreover have "integral {0..1} (\<lambda>t::real . l) \<le> integral {0..1} (\<lambda>t. ode (x (t0 + t * (t1 - t0))))"
      using ode_lu
      by (auto simp: eucl_le[where 'a='a] intro!: order_trans[OF _ integral_component_lbound_real] cnt)
    ultimately have "integral {0..1} (\<lambda>t. ode (x (t0 + t * (t1 - t0)))) \<in> {l .. u}"
      by simp
    hence "(t1 - t0) *\<^sub>R integral {0..1} (\<lambda>t. ode (x (t0 + t * (t1 - t0)))) \<in> {(t1 - t0) *\<^sub>R l .. (t1 - t0) *\<^sub>R u}"
      using ivl
      by (auto intro!: scaleR_left_mono)
  }
  finally show ?thesis by auto
qed

lemma picard_approx_ivl:
  assumes appr: "ode_approx optns [X] = Some Y"
  assumes bb: "inf_of_appr Y = l" "sup_of_appr Y = u"
  assumes x_in: "(\<And>t. t \<in> {t0 .. t1} \<Longrightarrow> x t \<in> set_of_appr X)"
  assumes cont: "continuous_on {t0 .. t1} x"
  assumes ivl: "t0 \<le> t" "t \<le> t1"
  shows "x0 + integral {t0..t} (\<lambda>t. ode (x t)) \<in> {x0 + inf 0 ((t1 - t0) *\<^sub>R l) .. x0 + sup 0 ((t1 - t0) *\<^sub>R u)}"
  using ivl inf_of_appr_le_sup_of_appr[of Y]
  by (intro set_rev_mp[OF picard_approx[OF appr bb x_in continuous_on_subset[OF cont]]])
    (auto simp: eucl_le[where 'a='a] inner_Basis_inf_left inner_Basis_sup_left inf_real_def
      sup_real_def min_def max_def zero_le_mult_iff not_le inner_add_left not_less bb
      intro: mult_right_mono mult_nonneg_nonpos mult_right_mono_neg)

text {* automatic Picard operator *}

lemma P_appr_Some_ode_approxE:
  assumes "P_appr optns X0 h X = Some R"
  obtains Y where "ode_approx optns [X] = Some Y" "R = extend_appr X0 (inf 0 (h *\<^sub>R inf_of_appr Y)) (sup 0 (h *\<^sub>R sup_of_appr Y))"
  using assms
  unfolding P_appr_def
  using assms by (auto simp: P_appr_def)

lemma
  assumes x0: "x0 \<in> set_of_appr X0"
  assumes x: "\<And>t. t \<in> {t0..t1} \<Longrightarrow> x t \<in> set_of_appr X"
  assumes cont: "continuous_on {t0..t1} x"
  assumes h': "0 \<le> t1 - t0" "t1 - t0 \<le> h"
  assumes P_res: "P_appr optns X0 h X = Some R"
  shows P_appr: "x0 + integral {t0..t1} (\<lambda>t. ode (x t)) \<in> set_of_appr R"
    and P_appr_euler: "\<And>t h'. t \<in> {t0..t1} \<Longrightarrow> h' \<in> {0 .. h} \<Longrightarrow> x0 + h' *\<^sub>R ode (x t) \<in> set_of_appr R"
proof -
  from P_res obtain Y where Y: "ode_approx optns [X] = Some Y"
    "R = extend_appr X0 (inf 0 (h *\<^sub>R inf_of_appr Y)) (sup 0 (h *\<^sub>R sup_of_appr Y))"
    by (rule P_appr_Some_ode_approxE)
  have "x0 + integral {t0 .. t1} (\<lambda>t. ode (x t)) \<in>
    {x0 + inf 0 ((t1 - t0) *\<^sub>R inf_of_appr Y) .. x0 + sup 0 ((t1 - t0) *\<^sub>R sup_of_appr Y)}"
    using assms
    by (intro picard_approx_ivl[OF Y(1) refl refl x cont]) auto
  also have "\<dots> \<subseteq> {x + y |x y. x \<in> set_of_appr X0 \<and>
      y \<in> {inf 0 ((t1 - t0) *\<^sub>R inf_of_appr Y) .. sup 0 ((t1 - t0) *\<^sub>R sup_of_appr Y)}}"
  proof safe
    case goal1
    show ?case
      apply (rule exI[where x=x0])
      apply (rule exI[where x="x - x0"])
      using goal1 assms
      by (simp add: algebra_simps)
  qed
  also have "\<dots> \<subseteq> {x + y |x y. x \<in> set_of_appr X0 \<and> y \<in> {inf 0 (h *\<^sub>R inf_of_appr Y) .. sup 0 (h *\<^sub>R sup_of_appr Y)}}"
    using assms
    by (intro msum_subsetI) (auto simp: eucl_le[where 'a='a] inner_Basis_inf_left inf_real_def
      inner_Basis_sup_left sup_real_def not_le not_less min_zero_mult_nonneg_le max_zero_mult_nonneg_le)
  also have *: "\<dots> = set_of_appr R"
    using assms
    by (simp add: inf_le_sup_same1 scaleR_left_mono set_of_appr_of_ivl Y msum_appr_eq)
  finally show "x0 + integral {t0..t1} (\<lambda>t. ode (x t)) \<in> set_of_appr R" .

  from h' have "0 \<le> h" by simp
  have "op *\<^sub>R h ` set_of_appr Y \<subseteq> op *\<^sub>R h ` {inf 0 (inf_of_appr Y)..sup 0 (sup_of_appr Y)}"
    by (rule image_mono) (auto simp: intro!: inf.coboundedI2 sup.coboundedI2)
  also have "\<dots> \<subseteq> {inf 0 (h *\<^sub>R inf_of_appr Y)..sup 0 (h *\<^sub>R sup_of_appr Y)}"
    using `0 \<le> h`
    by (cases "h = 0")
      (auto intro!: image_eqI[where x=0] simp: scaleR_image_atLeastAtMost scaleR_inf_eq scaleR_sup_eq)
  finally
  have subset: "op *\<^sub>R h ` set_of_appr Y \<subseteq> {inf 0 (h *\<^sub>R inf_of_appr Y)..sup 0 (h *\<^sub>R sup_of_appr Y)}" .
  {
    fix t h' assume t: "t \<in> {t0 .. t1}" and h': "h' \<in> {0 .. h}"
    hence "[x t] \<in> set_of_apprs [X]"
      using assms by (simp add: set_of_apprs_set_of_appr)
    from ode_approx[OF this Y(1)] have odeY: "[ode (x t), x t] \<in> set_of_apprs [Y, X]"
      by simp
    have "x0 + h' *\<^sub>R ode (x t) \<in> {x' + y|x' y. x' \<in> {x0} \<and> y \<in> {h' *\<^sub>R ode (x t)}}"
      by auto
    also have "\<dots> \<subseteq> {x + y |x y. x \<in> set_of_appr X0 \<and> y \<in> op *\<^sub>R h' ` set_of_appr Y}"
      apply (rule msum_subsetI)
      using assms t odeY
      apply (auto simp: assms)
      apply (drule set_of_apprs_switch)
      apply (force simp: set_of_apprs_set_of_appr dest: set_of_apprs_Cons)
      done
    also have "\<dots> \<subseteq> {x + y |x y. x \<in> set_of_appr X0 \<and>
        y \<in> {inf 0 (h' *\<^sub>R inf_of_appr Y)..sup 0 (h' *\<^sub>R sup_of_appr Y)}}"
      using assms h' subset
      by (intro msum_subsetI)
        (auto intro!: inf.coboundedI2 sup.coboundedI2 scaleR_left_mono)
    also have "\<dots> \<subseteq> {x + y |x y. x \<in> set_of_appr X0 \<and>
        y \<in> {inf 0 (h *\<^sub>R inf_of_appr Y)..sup 0 (h *\<^sub>R sup_of_appr Y)}}"
      using assms h' subset scaleR_inf_eq[of h 0 "inf_of_appr Y",symmetric]
        scaleR_sup_eq[of h 0 "sup_of_appr Y",symmetric]
      apply (intro msum_subsetI)
      apply (auto intro!: scaleR_right_mono simp:)
      apply (metis inf_sup_ord(1))
      apply (rule scaleR_mono_neg) apply assumption apply assumption apply simp apply simp
      apply (rule scaleR_nonneg_nonneg) apply simp apply simp
      apply (rule scaleR_mono'') apply assumption apply simp apply simp apply simp
      done
    also note *
    finally show "x0 + h' *\<^sub>R ode (x t) \<in> set_of_appr R" .
  }
qed

lemma P_iterE:
assumes "P_iter optns X0 h i X = Some X'"
obtains
  X'' where "P_appr optns X0 h X' = Some X''"
    "{inf_of_appr X'' .. sup_of_appr X''} \<subseteq> {inf_of_appr X' .. sup_of_appr X'}"
  using assms
proof (induct i arbitrary: X)
  case (Suc i) thus ?case
    by (cases "P_appr optns X0 h X") (auto simp: split: split_if_asm )
qed simp

lemma extend_appr_ivl:
  assumes "set_of_appr X = {inf_of_appr X .. sup_of_appr X}"
  assumes le2: "a \<le> 0" "0 \<le> b"
  assumes set_of_apprI: "\<And>x. inf_of_appr X \<le> x \<Longrightarrow> x \<le> sup_of_appr X \<Longrightarrow> x \<in> set_of_appr X"
  shows "set_of_appr (extend_appr X a b) = {inf_of_appr X + a .. sup_of_appr X + b}"
proof -
  have "{inf_of_appr X + a..sup_of_appr X + b} = {x + y|x y. x \<in> {inf_of_appr X ..sup_of_appr X} \<and> y \<in> {a .. b}}"
  proof safe
    fix x assume x: "x \<in> {inf_of_appr X + a..sup_of_appr X + b}"
    let ?x' = "\<Sum>i\<in>Basis. (if (x \<bullet> i) \<le> inf_of_appr X \<bullet> i then inf_of_appr X \<bullet> i
      else if (x \<bullet> i) \<le> sup_of_appr X \<bullet> i then x \<bullet> i else sup_of_appr X \<bullet> i)*\<^sub>R i"
    show "\<exists>x' y. x = x' + y \<and> x' \<in> {inf_of_appr X..sup_of_appr X} \<and> y \<in> {a..b}"
      apply (rule exI[where x = ?x'])
      apply (rule exI[where x = "x - ?x'"])
      unfolding assms
      using le2 x inf_of_appr_le_sup_of_appr
      by (auto simp: eucl_le[where 'a='a] algebra_simps intro!: set_of_apprI)
  qed (auto intro!: add_mono)
  also have "\<dots> = set_of_appr (extend_appr X a b)"
    unfolding msum_appr_eq using le2
    by (intro antisym msum_subsetI) (auto simp: set_of_appr_of_ivl assms(1))
  finally show ?thesis by simp
qed

lemma P_appr_ivl:
  assumes "P_appr optns X0 h X = Some X'"
  assumes "h \<ge> 0"
  assumes ivl_0: "{inf_of_appr X0..sup_of_appr X0} = set_of_appr X0"
  shows "{inf_of_appr X'..sup_of_appr X'} = set_of_appr X'"
proof -
  from assms obtain z where z: "ode_approx optns [X] = Some z"
    and X': "extend_appr X0 (inf 0 (h *\<^sub>R inf_of_appr z)) (sup 0 (h *\<^sub>R sup_of_appr z)) = X'"
    by (auto simp: P_appr_def)
  have [simp]: "inf 0 (h *\<^sub>R inf_of_appr z) \<le> sup 0 (h *\<^sub>R sup_of_appr z)"
    by (metis inf.coboundedI1 sup.cobounded1)
  show ?thesis
    unfolding X'[symmetric]
    by (auto simp: ivl_0[symmetric] extend_appr_ivl inf_of_appr_msum_appr sup_of_appr_msum_appr
      inf_of_appr_of_ivl sup_of_appr_of_ivl)
qed

lemma P_iter_ivl:
  assumes "P_iter optns X0 h i X = Some X'"
  assumes "h \<ge> 0"
  assumes "{inf_of_appr X0..sup_of_appr X0} = set_of_appr X0"
  assumes "{inf_of_appr X..sup_of_appr X} = set_of_appr X"
  shows "{inf_of_appr X'..sup_of_appr X'} = set_of_appr X'"
  using assms
proof (induct i arbitrary: X X')
  case (Suc i)
  thus ?case
  proof (cases "P_appr optns X0 h X")
    fix a
    assume *: "P_appr optns X0 h X = Some a"
    show ?thesis
    proof (cases "inf_of_appr X \<le> inf_of_appr a \<and> sup_of_appr a \<le> sup_of_appr X")
      case True
      with * Suc(2) have "X' = X" by simp
      with Suc show ?thesis by simp
    next
      case False
      with * Suc(2) have ind_step: "P_iter optns X0 h i
         (appr_of_ivl
           (inf (inf_of_appr a) (inf_of_appr X) -
            (if i mod widening_mod optns = 0 then \<bar>inf_of_appr a - inf_of_appr X\<bar> else 0))
           (sup (sup_of_appr a) (sup_of_appr X) +
            (if i mod widening_mod optns = 0 then \<bar>sup_of_appr a - sup_of_appr X\<bar> else 0))) =
              Some X'"
        by (simp add: *)
      have inf_le_sup: "inf (inf_of_appr a) (inf_of_appr X) \<le> sup (sup_of_appr a) (sup_of_appr X)"
        by (metis inf_of_appr_le_sup_of_appr le_infI2 le_supI2)
      hence min_le_max: "inf (inf_of_appr a) (inf_of_appr X) - \<bar>inf_of_appr a - inf_of_appr X\<bar>
           \<le> sup (sup_of_appr a) (sup_of_appr X) + \<bar>sup_of_appr a - sup_of_appr X\<bar>"
        unfolding diff_conv_add_uminus
        by (rule add_mono) (metis abs_ge_zero dual_order.trans neg_le_0_iff_le)
      show "{inf_of_appr X'..sup_of_appr X'} = set_of_appr X'"
        by (rule Suc(1)[OF ind_step])
         (auto simp add: Suc inf_of_appr_of_ivl sup_of_appr_of_ivl min_le_max set_of_appr_of_ivl inf_le_sup)
    qed
  qed simp
qed simp

lemma P_iter_mono:
  assumes "P_iter optns X0 h i X = Some X'"
  shows "set_of_appr X0 \<subseteq> {inf_of_appr X'..sup_of_appr X'}"
proof -
  from P_iterE[OF assms(1)] obtain X'' where X'':
    "P_appr optns X0 h X' = Some X''"
    "{inf_of_appr X''..sup_of_appr X''} \<subseteq> {inf_of_appr X'..sup_of_appr X'}" .
  from X''(1) have "set_of_appr X0 \<subseteq> set_of_appr X''"
    by (force simp: P_appr_def msum_appr_eq set_of_appr_of_ivl inf_le_sup_same1)
  also have "\<dots> \<subseteq> {inf_of_appr X''..sup_of_appr X''}"
    by auto
  also note X''(2)
  finally show ?thesis .
qed

lemma P_iter_eq:
  assumes "P_iter optns X0 h i X = Some X'"
  assumes "h \<ge> 0"
  assumes "{inf_of_appr X0..sup_of_appr X0} = set_of_appr X0"
  assumes "{inf_of_appr X..sup_of_appr X} = set_of_appr X"
  shows "set_of_appr X' = {inf_of_appr X'..sup_of_appr X'}"
  using assms
  by (simp add: P_iter_ivl[OF assms])

lemma P_iter_cert_stepsize:
  assumes "cert_stepsize optns X0 h n i = Some (h', X')"
  shows "P_iter optns (ivl_appr_of_appr X0) h' n (ivl_appr_of_appr X0) = Some X'"
  using assms
  by (induct i arbitrary: h) (auto split: option.split_asm)

definition step_ivp::"real \<Rightarrow> 'a \<Rightarrow> real \<Rightarrow> 'b \<Rightarrow> 'a ivp" where
"step_ivp t0 x0 t1 CX =
  \<lparr>ivp_f = (\<lambda>(t, x). ode x),
  ivp_t0 = t0, ivp_x0 = x0,
  ivp_T = {t0 .. t1},
  ivp_X = set_of_appr CX\<rparr>"

lemma step_ivp_simps[simp]:
  "ivp_f (step_ivp t0 x0 t1 CX) = (\<lambda>(t, x). ode x)"
  "ivp_t0 (step_ivp t0 x0 t1 CX) = t0"
  "ivp_x0 (step_ivp t0 x0 t1 CX) = x0"
  "ivp_T (step_ivp t0 x0 t1 CX) = {t0 .. t1}"
  "ivp_X (step_ivp t0 x0 t1 CX) = set_of_appr CX"
  by (simp_all add: step_ivp_def)


abbreviation "below_halfspace sctn \<equiv> Collect (le_halfspace sctn)"
lemma below_halfspace_def: "below_halfspace sctn = {x. x \<bullet> normal sctn \<le> pstn sctn}"
  by (auto simp: le_halfspace_def)


definition "flowsto X CX Y \<longleftrightarrow> (\<forall>x \<in> X. \<exists>t\<ge>0.
  t \<in> existence_ivl x \<and> (\<forall>s \<in> {0 .. t}. flow x s \<in> CX) \<and> flow x t \<in> Y)"

lemma flowsto_self[intro, simp]: "X \<subseteq> CX \<Longrightarrow> flowsto X CX X" by (force simp: flowsto_def)

lemma flowsto_unionI[intro, simp]:
  "flowsto X CX Y \<Longrightarrow> flowsto Z CZ W \<Longrightarrow> flowsto (X \<union> Z) (CX \<union> CZ) (Y \<union> W)"
  apply (auto simp: flowsto_def)
  apply (drule_tac x=x in bspec, assumption)
  apply auto
  apply (drule_tac x=x in bspec, assumption)
  apply auto
  done

lemma flowsto_inter1[intro, simp]: "flowsto X CX Y \<Longrightarrow> flowsto (X \<inter> Z) CX Y"
  and flowsto_inter2[intro, simp]: "flowsto X CX Y \<Longrightarrow> flowsto (Z \<inter> X) CX Y"
  by (auto simp: flowsto_def)

lemma flowsto_trans_Un: "flowsto X CX (Y \<union> Z) \<Longrightarrow> flowsto Y CY W \<Longrightarrow> flowsto X (CY \<union> CX) (W \<union> Z)"
proof (auto simp: flowsto_def)
  case goal1
  then obtain t where t: "t \<ge> 0" "t \<in> existence_ivl x"
    "(\<forall>s\<in>{0..t}. flow x s \<in> CX)"
    "flow x t \<in> Y \<or> flow x t \<in> Z"
    by auto
  from t(4) show ?case
  proof
    assume "flow x t \<in> Y"
    with goal1 t obtain s where s: "s \<ge> 0" "s \<in> existence_ivl (flow x t)"
      "(\<forall>s'\<in>{0..s}. flow (flow x t) s' \<in> CY)"
      "flow (flow x t) s \<in> W"
      by auto
    show ?case
      apply (rule exI[where x="t + s"])
      apply safe
      using s t apply simp
      apply (rule existence_ivl_trans)
      apply (rule t)
      apply (rule s)
      apply simp
      apply (case_tac "sa \<le> t")
      using t apply simp
      defer
      apply (simp add: flow_trans s(2) s(4) t(2))
    proof -
      case (goal1 s')
      with s t have st: "s' = t + (s' - t)" "s' - t \<ge> 0" "s' - t \<le> s" by auto
      hence "c1_on_open.flow ode UNIV (flow x t) (s' - t) \<in> CY"
        using s by auto
      thus ?case
        apply (subst (asm) flow_trans[symmetric])
        using s t goal1 st apply simp_all
        by (meson UNIV_I existence_ivl_zero is_interval_1 is_interval_existence_ivl st(2))
    qed
  next
    assume "flow x t \<in> Z"
    thus ?case
      using t
      by (auto simp: intro!: exI[where x=t])
  qed
qed

lemma flowsto_trans: "flowsto X CX Y \<Longrightarrow> flowsto Y CY Z \<Longrightarrow> flowsto X (CX \<union> CY) Z"
  by (smt flowsto_trans_Un inf_sup_aci(5) inf_sup_aci(6) sup_idem)

lemma flowsto_UnE:
  assumes "flowsto X CX (Y \<union> Z)"
  obtains X1 X2 where "X = X1 \<union> X2" "flowsto X1 CX Y" "flowsto X2 CX Z"
proof -
  let ?X1 = "{x\<in>X. flowsto {x} CX Y}"
  let ?X2 = "{x\<in>X. flowsto {x} CX Z}"
  from assms have "X = ?X1 \<union> ?X2" "flowsto ?X1 CX Y" "flowsto ?X2 CX Z"
    by (auto simp: flowsto_def)
  thus ?thesis ..
qed

lemma flowsto_subset: "flowsto X CX Y \<Longrightarrow> Y \<subseteq> Z \<Longrightarrow> CX \<subseteq> CZ \<Longrightarrow> flowsto X CZ Z"
  by (auto simp: flowsto_def) blast

text {* execution of @{term euler_step} *}
context
  fixes optns::"('a, 'b, 'c) options" and x0 X0
  assumes x0: "x0 \<in> set_of_appr X0"
  assumes pos_prestep: "0 < stepsize optns"
begin

text {* certified stepsize *}
context
  fixes h n i CX t0 t1
  assumes pos_step: "0 < h"
  assumes step_eq: "t0 + h = t1"
  assumes certified_stepsize: "cert_stepsize optns X0 (stepsize optns) n i = Some (h, CX)"
begin

lemma nonneg_step: "0 \<le> h" using pos_step by auto
lemma step_less: "t0 < t1" using step_eq pos_step by auto

lemma set_of_appr_eq: "set_of_appr CX = {inf_of_appr CX .. sup_of_appr CX}"
  by (subst P_iter_eq[OF P_iter_cert_stepsize[OF certified_stepsize]])
    (auto simp: ivl_appr_of_appr_def sup_of_appr_of_ivl inf_of_appr_of_ivl set_of_appr_of_ivl nonneg_step)

interpretation continuous_rhs T X "\<lambda>(t, x). ode x" for T X
  apply unfold_locales
  unfolding split_beta'
  apply (rule continuous_on_compose2[of _ ode _ snd])
  apply (rule continuous_on_subset[OF f_continuous_on])
  apply (auto simp add: split_beta intro!: continuous_intros
    continuous_on_compose2[of _ ode _ snd] has_derivative_continuous_on[OF fderiv])
  done

interpretation derivative_on_convex "{t0 .. t1}" "set_of_appr CX" "\<lambda>(t, x). ode x" "\<lambda>(t, x) (dt, dx). ode_d x dx"
  by default
    (auto simp: step_less set_of_appr_eq  nonneg_step less_imp_le convex_real_interval
      convex_closed_interval
      simp del: inf_of_appr sup_of_appr
      intro!: derivative_eq_intros has_derivative_eq_rhs[OF has_derivative_compose, of snd])

interpretation ivp_on_interval "step_ivp t0 x0 t1 CX" t1
  using nonneg_step step_eq
proof (unfold_locales, simp_all add: step_ivp_def step_less less_imp_le)
  have "x0 \<in> set_of_appr (ivl_appr_of_appr X0)"
     by (auto simp: ivl_appr_of_appr_def set_of_appr_of_ivl x0)
  also have "\<dots> \<subseteq> {inf_of_appr CX..sup_of_appr CX}"
    by (metis P_iter_mono P_iter_cert_stepsize certified_stepsize)
  also have "\<dots> = set_of_appr CX"
    by (rule set_of_appr_eq[symmetric])
  finally show "x0 \<in> set_of_appr CX" .
qed

interpretation unique_on_compact_continuously_diff t1 "\<lambda>x. Blinfun (\<lambda>dx. ode_d x dx)" "step_ivp t0 x0 t1 CX"
  apply intro_locales
  defer
  apply simp
proof unfold_locales
  let ?step = "step_ivp t0 x0 t1 CX"
  fix t x
  assume xt0: "x (ivp_t0 ?step) = ivp_x0 ?step"
  from this have "x t0 \<in> set_of_appr (ivl_appr_of_appr X0)" using x0
    by (auto simp: ivl_appr_of_appr_def set_of_appr_of_ivl)
  moreover
  assume "x \<in> {ivp_t0 ?step..t} \<rightarrow> ivp_X ?step"
  from this have "\<And>ta. ta \<in> {t0..t0 + (t - t0)} \<Longrightarrow> x ta \<in> set_of_appr CX" by auto
  moreover
  assume "continuous_on {ivp_t0 ?step..t} x"
  from this have "continuous_on {t0..t0 + (t - t0)} x" by simp
  moreover
  assume "t \<in> ivp_T ?step"
  from this step_eq have "0 \<le> t0 + (t - t0) - t0" "t0 + (t - t0) - t0 \<le> h"
    by simp_all
  moreover
  from P_iter_cert_stepsize[OF certified_stepsize, THEN P_iterE]
  obtain X'' where "P_appr optns (ivl_appr_of_appr X0) h CX = Some X''"
    and subset: "{inf_of_appr X''..sup_of_appr X''} \<subseteq> {inf_of_appr CX..sup_of_appr CX}" .
  note this(1)
  ultimately have "x t0 + integral {t0..t0 + (t - t0)} (\<lambda>t. ode (x t)) \<in> set_of_appr X''"
    by (rule P_appr)
  also have "\<dots> \<subseteq> {inf_of_appr X''..sup_of_appr X''}" by auto
  also note subset
  also note set_of_appr_eq[symmetric]
  finally show "ivp_x0 ?step + integral {ivp_t0 ?step..t} (\<lambda>t. ivp_f ?step (t, x t)) \<in> ivp_X ?step"
    using xt0 by simp
next
  show "continuous_on (ivp_X (step_ivp t0 x0 t1 CX)) (\<lambda>x. Blinfun (ode_d x))"
    using continuous_derivative
    by (auto simp: intro: continuous_on_subset)
qed (auto simp: set_of_appr_compact step_less less_imp_le set_of_appr_nonempty)

lemma flow_eq_solution:
  assumes "t0 + s \<in> {t0 .. t1}"
  shows "flow x0 s = solution (t0 + s)"
proof -
  have "solution t0 = flow x0 0"
    using solution_t0 by simp
  moreover
  have "\<And>s. s \<in> {t0 .. t1} \<Longrightarrow> (solution has_vector_derivative ode (solution s)) (at s within {t0 .. t1})"
    using solution_has_deriv by simp
  ultimately
  show ?thesis
    apply (rule flow_eqI)
    using assms
    apply auto
    done
qed

lemma flow_in: "t0 + s \<in> {t0 .. t1} \<Longrightarrow> flow x0 s \<in> set_of_appr CX"
  using solution_in_D[of "t0 + s"]
  by (simp add: flow_eq_solution)

lemma unique_solution_step_ivp: "unique_solution (step_ivp t0 x0 t1 CX)" by default

lemma existence_ivl: "h \<in> existence_ivl x0"
proof -
  have "solution t0 = flow x0 0"
    using solution_t0
    by simp
  moreover
  from solution_has_deriv
  have "\<And>t. t \<in> {t0 .. t1} \<Longrightarrow> (solution has_vector_derivative ode (solution t)) (at t within {t0 .. t1})"
    by simp
  ultimately show ?thesis
    apply (rule in_existence_ivlI)
    using nonneg_step step_less
    by (auto simp: step_eq)
qed

lemma certified_rk:
  assumes "h1 \<in> {0 .. h}" "h2 \<in> {0 .. h}"
  shows "x0 + h1 *\<^sub>R ode (flow x0 h2) \<in> set_of_appr CX"
proof -
  from P_iter_cert_stepsize[OF certified_stepsize, THEN P_iterE] guess X'' . note X'' = this
  have "x0 + h1 *\<^sub>R ode (flow x0 h2) \<in> set_of_appr X''"
  proof (rule P_appr_euler)
    show "x0 \<in> set_of_appr (ivl_appr_of_appr X0)"
      using x0 by (auto simp: ivl_appr_of_appr_def set_of_appr_of_ivl)
    show "0 \<le> h - 0" using `0 \<le> h` by simp
    show "\<And>t. t \<in> {0..h} \<Longrightarrow> flow x0 t \<in> set_of_appr CX"
      apply (rule flow_in)
      using assms step_eq
      by auto
    show "continuous_on {0..h} (flow x0)"
      apply (rule continuous_on_subset)
      apply (rule flow_continuous_on)
      apply simp
      apply (rule ivl_subset_existence_ivl)
      apply simp
      apply (rule existence_ivl)
      done
    from X'' show "local.P_appr optns (ivl_appr_of_appr X0) h CX = Some X''" by simp
    from assms show "h1 \<in> {0..h}" "h2 \<in> {0..h}" by simp_all
  qed auto
  also have "set_of_appr X'' \<subseteq> {inf_of_appr X'' .. sup_of_appr X''}" by auto
  also note X''(2)
  also note set_of_appr_eq[symmetric]
  finally show "x0 + h1 *\<^sub>R ode (c1_on_open.flow ode UNIV x0 h2) \<in> set_of_appr CX" .
qed

text {* intermediate results of euler step *}
context
  fixes RES_ivl RES_at X0' F D ERR S S' X1 CX1 err
  assumes euler_step_returns: "euler_step optns X0 = Some (h, err, RES_ivl, RES_at)"
  assumes bounded_ode: "ode_approx optns [X0] = Some X0'"
  assumes bounded_total_ode: "ode_approx optns [CX] = Some F"
  assumes bounded_ode_d: "ode_d_approx optns [CX, F] = Some D"
  assumes bounded_err: "scale_appr optns (h*h) 2 (ivl_appr_of_appr D) [] = Some ERR"
  assumes bounded_scale_euler: "scale_appr optns h 1 X0' [X0] = Some S"
  assumes bounded_scale_ivl_euler: "scale_appr_ivl optns 0 h X0' [X0] = Some S'"
  assumes bounded_add_euler: "add_appr optns X0 S [] = Some X1"
  assumes bounded_add_euler_ivl: "add_appr optns X0 S' [] = Some CX1"
  assumes RES_ivl: "RES_ivl = msum_appr CX1 (appr_of_ivl (inf 0 (inf_of_appr ERR)) (sup 0 (sup_of_appr ERR)))"
  assumes RES_at: "RES_at = msum_appr X1 (ivl_appr_of_appr ERR)"
begin

lemma x0_in_CX1: "x0 \<in> set_of_appr CX1"
proof -
  from nonneg_step have "0 \<in> {0 .. h}" by auto
  from scale_appr_ivl[OF this ode_approx[OF x0[simplified set_of_apprs_set_of_appr[symmetric]] bounded_ode] bounded_scale_ivl_euler]
  have "[x0, 0] \<in> set_of_apprs [X0, S']"
    by (metis pth_4(1) set_of_apprs_Cons set_of_apprs_rotate3)
  from add_appr[OF this bounded_add_euler_ivl]
  show "x0 \<in> set_of_appr CX1"
    by (metis comm_monoid_add_class.add.right_neutral set_of_apprs_Cons set_of_apprs_rotate3
      set_of_apprs_set_of_appr)
qed

interpretation derivative_set_bounded "{t0 .. t1}" "set_of_appr CX" "\<lambda>(t, x). ode x" "\<lambda>(t, x) (dt, dx). ode_d x dx" "Pair_of_list ` set_of_apprs [CX, F]"
  "{inf_of_appr D .. sup_of_appr D}"
proof
  have "Pair_of_list ` set_of_apprs [CX, F] \<subseteq> set_of_appr CX \<times> set_of_appr F"
    by (auto elim!: set_of_apprsE dest!: set_of_apprs_Nil)
  moreover have "bounded (\<dots>)"
    by (rule set_of_appr_compact compact_imp_bounded bounded_Times)+
  ultimately show "bounded (Pair_of_list ` set_of_apprs [CX, F])"
    by (blast intro: bounded_subset)
  show "bounded {inf_of_appr D .. sup_of_appr D}"
    by (simp add: bounded_closed_interval)
  fix t x
  assume "t \<in> {t0 .. t1}" "x \<in> set_of_appr CX"
  hence x: "[x] \<in> set_of_apprs [CX]" by (auto simp: set_of_apprs_set_of_appr)
  with ode_approx
  have "[x, ode x] \<in> set_of_apprs [CX, F]"
    by (auto intro!: ode_approx bounded_total_ode intro: set_of_apprs_switch)
  thus " (x, case (t, x) of (t, x) \<Rightarrow> ode x) \<in> Pair_of_list ` set_of_apprs [CX, F]"
    by auto
next
  fix t x d
  assume "t \<in> {t0..t1}"
  assume "(x, d) \<in> Pair_of_list ` set_of_apprs [CX, F]"
  then obtain xs where xs: "Pair_of_list xs = (x, d)" "xs \<in> set_of_apprs [CX, F]" by auto
  hence "xs = [x, d]"
    by (auto elim!: set_of_apprsE dest!: set_of_apprs_Nil)
  with xs have "[x, d] \<in> set_of_apprs [CX, F]" by simp
  hence "[x, d, ode_d x d] \<in> set_of_apprs [CX, F, D]"
    by (auto intro!: ode_d_approx bounded_ode_d intro: set_of_apprs_switch set_of_apprs_rotate3)
  hence "ode_d x d \<in> set_of_appr D"
    unfolding set_of_apprs_set_of_appr[symmetric]
    by (blast intro: set_of_apprs_Cons)
  thus "(case (t, x) of (t, x) \<Rightarrow> \<lambda>(dt, dx). ode_d x dx) (1, d) \<in> {inf_of_appr D .. sup_of_appr D}"
    by auto
qed (simp add: is_interval_closed_interval)

lemma euler_consistent_solution':
  assumes "t1' \<in> {t0 .. t1}"
  shows "flow x0 ((t1' - t0)) - discrete_evolution (euler_increment ((\<lambda>(t, x). ode x))) (t0 + (t1' - t0)) t0 (flow x0 0) \<in>
    op *\<^sub>R ((t1' - t0)\<^sup>2 / 2) ` {inf_of_appr D..sup_of_appr D}"
  apply (subst flow_eq_solution)
  using assms apply simp
  apply (subst flow_eq_solution)
  using assms apply simp
  unfolding add_0_right
  using assms solution_has_deriv solution_in_D
  by (intro euler_consistent_traj_set2[where u=t1]) auto

lemma euler_consistent_solution:
  assumes "t0 + h' \<in> {t0 .. t1}"
  shows "flow x0 h' - discrete_evolution (euler_increment f) (t0 + h') t0 x0 \<in> op *\<^sub>R (h'\<^sup>2 / 2) ` {inf_of_appr D..sup_of_appr D}"
  using euler_consistent_solution'[OF assms]
  by simp

lemma error_overapproximation:
  shows  "flow x0 h \<in> set_of_appr RES_at"
proof -
  def euler_res \<equiv> "discrete_evolution (euler_increment f) (t0 + h) t0 x0"
  have step_ok: "t0 + h \<in> {t0 .. t1}" using step_eq pos_step by auto
  from this have "flow x0 h \<in> {euler_res + (h^2 / 2) *\<^sub>R inf_of_appr D .. euler_res + (h^2 / 2) *\<^sub>R sup_of_appr D}"
    using euler_consistent_solution[OF step_ok] step_eq
    by (auto simp: euler_res_def algebra_simps intro!: scaleR_left_mono)
  also have "\<dots> = {x + y |x y. x \<in> {euler_res} \<and> y \<in> {(h * h / 2) *\<^sub>R inf_of_appr D .. (h * h / 2) *\<^sub>R sup_of_appr D}}"
    by (auto intro!: exI[where x="x - euler_res" for x] simp: algebra_simps power2_eq_square)
  also have "\<dots> \<subseteq> set_of_appr (msum_appr X1 (ivl_appr_of_appr ERR))"
    unfolding msum_appr_eq
  proof (rule msum_subsetI)
    have ode_x0: "[ode x0, x0] \<in> set_of_apprs [X0', X0]"
      by (metis bounded_ode ode_approx x0 set_of_apprs_set_of_appr)
    note scale_appr[where r=h and X = "X0'" and XS = "[X0]" and x = "ode x0" and xs = "[x0]" and optns = optns,
      THEN set_of_apprs_rotate, simplified append_Cons append_Nil,
      THEN set_of_apprs_Cons]
    from add_appr[OF this , of _ _ optns , THEN set_of_apprs_switch, THEN set_of_apprs_Cons,
      THEN set_of_apprs_switch, THEN set_of_apprs_Cons,
      simplified set_of_apprs_set_of_appr, OF ode_x0 bounded_scale_euler bounded_add_euler]
    show "{euler_res} \<subseteq> set_of_appr X1"
      using x0
      unfolding euler_res_def discrete_evolution_def euler_increment
      by (simp add: step_ivp_def)
  next
    from
      scale_appr[where r="(h * h)" and s=2 and X = "ivl_appr_of_appr D" and XS="[]" and xs="[]"
        and x="inf_of_appr D" and optns=optns,
        THEN set_of_apprs_switch, THEN set_of_apprs_Cons, OF _ bounded_err]
      scale_appr[where r="(h * h)" and s = 2 and X = "ivl_appr_of_appr D" and XS="[]" and xs="[]"
        and x="sup_of_appr D" and optns=optns,
        THEN set_of_apprs_switch, THEN set_of_apprs_Cons, OF _ bounded_err]
    show "{(h * h / 2) *\<^sub>R inf_of_appr D..(h * h / 2) *\<^sub>R sup_of_appr D} \<subseteq> set_of_appr (ivl_appr_of_appr ERR)"
      by (simp_all add: set_of_apprs_set_of_appr ivl_appr_of_appr_def set_of_appr_of_ivl)
  qed
  finally show ?thesis unfolding RES_at .
qed

lemma error_overapproximation_ivl:
  assumes h': "h' \<in> {0..h}"
  shows "flow x0 h' \<in> set_of_appr RES_ivl"
proof -
  def euler_res \<equiv> "discrete_evolution (euler_increment f) (t0 + h') t0 x0"
  have step_ok: "t0 + h' \<in> {t0 .. t1}" using step_eq pos_step assms by auto

  have "flow x0 h' \<in> {euler_res + (h'^2 / 2) *\<^sub>R inf_of_appr D .. euler_res + (h'^2 / 2) *\<^sub>R sup_of_appr D}"
    using euler_consistent_solution[OF step_ok] step_eq
    by (auto simp: euler_res_def algebra_simps intro!: scaleR_left_mono)
  also have "\<dots> = {x + y |x y. x \<in> {euler_res} \<and> y \<in> {(h' * h' / 2) *\<^sub>R inf_of_appr D .. (h' * h' / 2) *\<^sub>R sup_of_appr D}}"
    by (auto intro!: exI[where x="x - euler_res" for x] simp: algebra_simps power2_eq_square)
  also have "\<dots> \<subseteq> set_of_appr (msum_appr CX1 (appr_of_ivl (inf 0 (inf_of_appr ERR)) (sup 0 (sup_of_appr ERR))))"
    unfolding msum_appr_eq
  proof (rule msum_subsetI)
    have ode_x0: "[ode x0, x0] \<in> set_of_apprs [X0', X0]"
      by (metis bounded_ode ode_approx x0 set_of_apprs_set_of_appr)
    note scale_appr[where r=h and X = "X0'" and XS = "[X0]" and x = "ode x0" and xs = "[x0]" and optns = optns,
      THEN set_of_apprs_rotate, simplified append_Cons append_Nil,
      THEN set_of_apprs_Cons]
    note scale_appr_ivl[OF h', where X = "X0'" and XS = "[X0]" and x = "ode x0" and xs = "[x0]" and optns = optns,
      THEN set_of_apprs_rotate, simplified append_Cons append_Nil,
      THEN set_of_apprs_Cons]
    from add_appr[OF this , of _ optns , THEN set_of_apprs_switch, THEN set_of_apprs_Cons,
      THEN set_of_apprs_switch, THEN set_of_apprs_Cons,
      simplified set_of_apprs_set_of_appr, OF ode_x0 bounded_scale_ivl_euler bounded_add_euler_ivl]
    show "{euler_res} \<subseteq> set_of_appr CX1"
      using x0
      unfolding euler_res_def discrete_evolution_def euler_increment
      by (simp add: step_ivp_def)
  next
    have infsup[simp]: "inf 0 (inf_of_appr ERR) \<le> (sup 0 (sup_of_appr ERR))"
      by (metis inf_sup_ord(1) le_supI1)
    have "{(h' * h' / 2) *\<^sub>R inf_of_appr D .. (h' * h' / 2) *\<^sub>R sup_of_appr D} \<subseteq>
        {inf 0 ((h * h / 2) *\<^sub>R inf_of_appr D) .. sup 0 ((h * h / 2) *\<^sub>R sup_of_appr D)}"
      unfolding interval_cbox
    proof (rule subset_box_imp, safe)
      fix i::'a assume "i \<in> Basis"
      show "inf 0 ((h * h / 2) *\<^sub>R inf_of_appr D) \<bullet> i \<le> (h' * h' / 2) *\<^sub>R inf_of_appr D \<bullet> i"
        using assms
        unfolding inner_Basis_inf_left[OF `i \<in> Basis`] inner_zero_left inf_real_def inner_scaleR_left
        by (intro min_zero_mult_nonneg_le) (auto intro!: mult_mono)
      show "(h' * h' / 2) *\<^sub>R sup_of_appr D \<bullet> i \<le> sup 0 ((h * h / 2) *\<^sub>R sup_of_appr D) \<bullet> i"
        using assms
        unfolding inner_Basis_sup_left[OF `i \<in> Basis`] inner_zero_left sup_real_def inner_scaleR_left
        by (intro max_zero_mult_nonneg_le) (auto intro!: mult_mono)
    qed
    also
    from
      scale_appr[where r="(h * h)" and s=2 and X = "ivl_appr_of_appr D" and XS="[]" and xs="[]"
        and x="inf_of_appr D" and optns=optns,
        THEN set_of_apprs_switch, THEN set_of_apprs_Cons, OF _ bounded_err]
      scale_appr[where r="(h * h)" and s=2 and X = "ivl_appr_of_appr D" and XS="[]" and xs="[]"
        and x="sup_of_appr D" and optns=optns,
        THEN set_of_apprs_switch, THEN set_of_apprs_Cons, OF _ bounded_err]
    have "\<dots> \<subseteq> set_of_appr (appr_of_ivl (inf 0 (inf_of_appr ERR)) (sup 0 (sup_of_appr ERR)))"
      by (auto simp add: set_of_apprs_set_of_appr ivl_appr_of_appr_def set_of_appr_of_ivl
        intro!: le_infI2 le_supI2)
    finally show "{(h' * h' / 2) *\<^sub>R inf_of_appr D..(h' * h' / 2) *\<^sub>R sup_of_appr D} \<subseteq>
        set_of_appr ((appr_of_ivl (inf 0 (inf_of_appr ERR)) (sup 0 (sup_of_appr ERR))))"
      by (auto simp add: ivl_appr_of_appr_def set_of_appr_of_ivl)
  qed
  finally show ?thesis unfolding RES_ivl .
qed

end

end

lemma unique_on_euler_step:
  assumes "t0 + h = t1"
  assumes euler_step_returns: "euler_step optns X0 = Some (h, err, RES_ivl, RES_at)"
  shows
    "h > 0"
    "\<And>h. t0 + h \<in> {t0 .. t1} \<Longrightarrow> flow x0 h \<in> set_of_appr RES_ivl" (is "\<And>h. ?ass2 h \<Longrightarrow> ?th2 h") and
    "flow x0 h \<in> set_of_appr RES_at" (is ?th3)
    "h \<in> existence_ivl x0"
proof -
  from euler_step_returns
  obtain X0' CX F D ERR S S' X1' X1'' where intermediate_results:
    "cert_stepsize optns X0 (stepsize optns) (iterations optns) (halve_stepsizes optns) = Some (h, CX)"
    "euler_step optns X0 = Some (h, err, RES_ivl, RES_at)"
    "ode_approx optns [X0] = Some X0'"
    "ode_approx optns [CX] = Some F"
    "ode_d_approx optns [CX, F] = Some D"
    "scale_appr optns (h * h) 2 (ivl_appr_of_appr D) [] = Some ERR"
    "scale_appr optns h 1 X0' [X0] = Some S"
    "scale_appr_ivl optns 0 h X0' [X0] = Some S'"
    "add_appr optns X0 S [] = Some X1'"
    "add_appr optns X0 S' [] = Some X1''"
    "RES_ivl = extend_appr X1'' (inf 0 (inf_of_appr ERR)) (sup 0 (sup_of_appr ERR))"
    "RES_at = msum_appr X1' (ivl_appr_of_appr ERR)"
    using pos_prestep euler_step_returns
    by (auto simp: euler_step_def split: split_option_bind_asm)
  from cert_stepsize_pos[OF intermediate_results(1) pos_prestep] show "0 < h" .
  have "t1 = t0 + h" by (simp add: assms)
  thus "\<And>h. ?ass2 h \<Longrightarrow> ?th2 h"
    by (intro error_overapproximation_ivl[OF `0 < h` _ intermediate_results]) auto
  show ?th3
    by (rule error_overapproximation[OF `0 < h` assms(1) intermediate_results])
  show "h \<in> existence_ivl x0"
    using existence_ivl[OF `0 < h` assms(1) intermediate_results(1)] .
qed

lemma unique_on_euler_step_simple:
  assumes "euler_step optns X0 = Some (h, err, RES_ivl, RES_at)"
  shows
  "h > 0" "\<And>s. 0 \<le> s \<Longrightarrow> s \<le> h \<Longrightarrow> flow x0 s \<in> set_of_appr RES_ivl"
  "flow x0 h \<in> set_of_appr RES_at" "h \<in> existence_ivl x0"
  using unique_on_euler_step[of 0 h, OF _ assms(1)]
  by auto

end

definition "step_spec X0 = SPEC
  (\<lambda>(h,_, CX, X). h > 0 \<and>
    (\<forall>x0 \<in> set_of_appr X0. h \<in> existence_ivl x0 \<and> flow x0 h \<in> set_of_appr X \<and>
    (\<forall>t\<in>{0..h}. flow x0 t \<in> set_of_appr CX)))"

lemma euler_step_nres_spec:
  assumes "0 < stepsize optns"
  shows "euler_step_nres optns X0 \<le> step_spec X0"
  using set_of_appr_nonempty[of X0]
  by (auto intro!: THE_NRES_rule  simp: euler_step_nres_def assms unique_on_euler_step[OF _ assms(1)]
    step_spec_def)


lemma
  assumes "0 < stepsize optns"
  assumes "local.euler_step optns X0 = Some (h, ERR, CX, X)"
  shows euler_step_flowsto_at: "flowsto (set_of_appr X0) (set_of_appr CX) (set_of_appr X)"
    and euler_step_flowsto_ivl: "flowsto (set_of_appr X0) (set_of_appr CX) (set_of_appr CX)"
  using unique_on_euler_step_simple[OF _ assms]
  by (force simp: flowsto_def intro!: exI[where x=h])+

lemma ode_approx_eq_SomeD:
  assumes "ode_approx optns (X'#XS) = Some D'"
  shows "x#xs \<in> set_of_apprs (X'#XS) \<longrightarrow> ode x#x#xs \<in> set_of_apprs (D'#X'#XS)"
  using ode_approx assms by blast

lemma ode_d_approx_eq_SomeD:
  assumes "ode_d_approx optns (X' # DX' # XS) = Some D'"
  shows "x#dx#xs \<in> set_of_apprs (X' # DX' # XS) \<longrightarrow> ode_d x dx # x # dx # xs \<in> set_of_apprs (D' # X' # DX' # XS)"
  using ode_d_approx assms by blast

lemma ode_d2_approx_eq_SomeD:
  assumes "ode_d2_approx optns (X' # DX' # DY' # XS) = Some D'"
  shows "(x # dx # dy # xs) \<in> set_of_apprs (X' # DX' # DY' # XS) \<longrightarrow> (ode_d2 x dx dy # x # dx # dy # xs) \<in> set_of_apprs (D' # X' # DX' # DY' # XS)"
  using ode_d2_approx assms by blast

lemma add_appr_drop2:
  assumes "x # y # xs \<in> set_of_apprs (X # Y # XS)" "add_appr optns X Y XS = Some S"
  shows "((x+y)#xs) \<in> set_of_apprs (S # XS)"
  using add_appr[OF assms]
  apply -
  apply (drule set_of_apprs_switch)
  apply (drule  set_of_apprs_Cons)
  apply (drule set_of_apprs_switch)
  apply (drule  set_of_apprs_Cons)
  apply assumption
  done

lemma scale_appr_drop2:
  assumes "x # xs \<in> set_of_apprs (X # XS)" "scale_appr optns r s X XS = Some S"
  shows "(r / s) *\<^sub>R x # xs \<in> set_of_apprs (S # XS)"
  using scale_appr[OF assms]
  apply -
  apply (drule set_of_apprs_switch)
  apply (drule  set_of_apprs_Cons)
  apply assumption
  done

lemma
  ode_d2_approx_spec:
    "THE_NRES (ode_d2_approx optns (Y # FY # FY' # XS)) \<le>
      SPEC (\<lambda>R. \<forall>y fy fy' xs. y # fy # fy' # xs \<in> set_of_apprs     (Y # FY # FY' # XS) \<longrightarrow>
        ((ode_d2 y fy fy') # y # fy # fy' # xs) \<in> set_of_apprs (R # Y # FY # FY' # XS))"
  by (intro refine_vcg) (auto dest: ode_d2_approx)

lemma
  ode_d_approx_spec: "THE_NRES (ode_d_approx optns (Y#FY#XS)) \<le>
    SPEC (\<lambda>R. \<forall>y fy xs. y # fy # xs \<in> set_of_apprs (Y#FY#XS) \<longrightarrow> (ode_d y fy # y # fy # xs) \<in> set_of_apprs (R # Y # FY # XS))"
  by (intro refine_vcg) (auto intro!: ode_d_approx)

lemma
  ode_approx_spec: "THE_NRES (ode_approx optns (Y # XS)) \<le>
    SPEC (\<lambda>R. \<forall>y xs. y#xs \<in> set_of_apprs (Y#XS) \<longrightarrow> ode y # y # xs \<in> set_of_apprs (R # Y # XS))"
  by (intro refine_vcg) (auto intro!: ode_approx)

lemma add_appr_spec: "THE_NRES (add_appr optns X Y XS) \<le> SPEC (\<lambda>R. \<forall>x y xs. (x#y#xs) \<in> set_of_apprs (X#Y#XS) \<longrightarrow> ((x + y)#x#y#xs) \<in> set_of_apprs (R#X#Y#XS))"
  by (intro refine_vcg) (auto intro!: add_appr)

lemma scale_appr_spec: "THE_NRES (scale_appr optns r s X XS) \<le> SPEC (\<lambda>R. \<forall>x xs. (x#xs) \<in> set_of_apprs (X#XS) \<longrightarrow> (((r/s)*\<^sub>R x)#x#xs) \<in> set_of_apprs (R#X#XS))"
  by (intro refine_vcg) (auto intro!: scale_appr)

lemma scale_appr_ivl_spec: "THE_NRES (scale_appr_ivl optns r s X XS) \<le> SPEC (\<lambda>R. \<forall>x t xs. t \<in> {r .. s} \<longrightarrow> (x#xs) \<in> set_of_apprs (X#XS) \<longrightarrow> ((t *\<^sub>R x)#x#xs) \<in> set_of_apprs (R#X#XS))"
  by (intro refine_vcg) (auto intro!: scale_appr_ivl)

lemma inter_appr_plane_spec: "THE_NRES (inter_appr_plane optns X sctn) \<le> SPEC (\<lambda>R. set_of_appr X \<inter> plane_of sctn \<subseteq> set_of_appr R)"
  by (intro refine_vcg) (auto intro!: inter_appr_plane)


declare order_trans[OF ode_d2_approx_spec, refine_vcg]
  order_trans[OF ode_d_approx_spec, refine_vcg]
  order_trans[OF ode_approx_spec, refine_vcg]
  order_trans[OF add_appr_spec, refine_vcg]
  order_trans[OF scale_appr_spec, refine_vcg]
  order_trans[OF scale_appr_ivl_spec, refine_vcg]
  order_trans[OF inter_appr_plane_spec, refine_vcg]

lemma zip_eq_Nil_iff: "zip xs ys = [] \<longleftrightarrow> xs = [] \<or> ys = []"
  apply (auto )
  apply (cases xs)
  apply simp
  apply (cases ys)
  apply simp
  apply simp
  done

lemma cert_stepsize_spec:
  assumes "0 < stepsize optns" "0 < rk2_param optns"
  shows "THE_NRES (cert_stepsize optns X0 (stepsize optns) n i) \<le> SPEC (\<lambda>(hc, CX).
    0 < hc \<and>
    {inf_of_appr CX .. sup_of_appr CX} = set_of_appr CX \<and>
    (\<forall>x0 \<in> set_of_appr X0.
      hc \<in> existence_ivl x0 \<and>
      (\<forall>h\<in>{0..hc}. flow x0 h \<in> set_of_appr CX) \<and>
      (\<forall>h1\<in>{0..hc}. \<forall>h2\<in>{0..hc}. x0 + h1 *\<^sub>R ode (flow x0 h2) \<in> set_of_appr CX)))"
  apply (intro refine_vcg)
  apply (auto intro!: )
  apply (rule cert_stepsize_pos, assumption, rule assms)+
  defer
  apply (rule existence_ivl, assumption, rule assms)
  apply (rule cert_stepsize_pos, assumption, rule assms)
  apply (rule refl)
  apply assumption
  apply (rule flow_in, assumption, rule assms)
  apply (rule cert_stepsize_pos, assumption, rule assms)
  apply (rule refl)
  apply assumption
  apply force
  apply (rule certified_rk, assumption, rule assms)
  apply (rule cert_stepsize_pos, assumption, rule assms)
  apply (rule refl)
  apply assumption
  apply force
  apply force
proof -
  case goal1
  hence "0 < a"
    by -(rule cert_stepsize_pos, assumption, rule assms)+
  from set_of_appr_eq[OF _ assms(1) this _ goal1(1)] set_of_appr_nonempty
  have "set_of_appr b = {inf_of_appr b..sup_of_appr b}" by force
  thus ?case
    using goal1 by simp
qed

declare order_trans[OF cert_stepsize_spec, refine_vcg]

lemma rk2_incr_nres_spec:
  assumes "0 < h" "0 < rk2_param optns"
  shows "rk2_incr_nres optns h X \<le>
    SPEC (\<lambda>(R, R').
      (\<forall>t x. [x] \<in> set_of_apprs [X] \<longrightarrow> [rk2_increment (rk2_param optns) (\<lambda>(t, x). ode x) h t x, x] \<in> set_of_apprs [R, X] \<and>
       (\<forall>h'\<in>{0..h}. [rk2_increment (rk2_param optns) (\<lambda>(t, x). ode x) h' t x, x] \<in> set_of_apprs [R', X])))"
  unfolding rk2_incr_nres_def
  apply (intro refine_vcg)
proof safe
  case (goal1 FX A S XpS F2 B S' XpS' F2' B' R R' t x)
  from goal1(1)[rule_format, OF `[x] \<in> set_of_apprs [X]`]
  have "[ode x, x] \<in> set_of_apprs [FX, X]" (is "(?fx#_)\<in> _")
    by auto
  from goal1(2)[rule_format, OF this]
  have "[((rk2_param optns * 2 - 1) / (rk2_param optns * 2)) *\<^sub>R ode x, ode x, x] \<in> set_of_apprs [A, FX, X]" (is "(?a#_)\<in> _") .
  hence "[?fx, ?a, x] \<in> set_of_apprs [FX, A, X]" by (rule set_of_apprs_imp) auto
  from goal1(3)[rule_format, OF this]
  have "[(h * rk2_param optns / 1) *\<^sub>R ?fx, ?fx, ?a, x] \<in> set_of_apprs [S, FX, A, X]" (is "(?s#_)\<in> _") .
  hence "[x, ?s, ?a, x] \<in> set_of_apprs [X, S, A, X]" by (rule set_of_apprs_imp) auto
  from goal1(4)[rule_format, OF this]
  have "[x + ?s, x, ?s, ?a, x] \<in> set_of_apprs [XpS, X, S, A, X]" (is "(?xps#_)\<in> _") .

  hence "[?xps, x, ?a] \<in> set_of_apprs [XpS, X, A]" by (rule set_of_apprs_imp) auto
  from goal1(5)[rule_format, OF this]
  have "[ode ?xps, ?xps, x, ?a] \<in> set_of_apprs [F2, XpS, X, A]" (is "(?f2#_)\<in> _") .

  hence "[?f2, x, ?a] \<in> set_of_apprs [F2, X, A]" by (rule set_of_apprs_imp) auto
  from goal1(6)[rule_format, OF this]
  have "[(1 / (rk2_param optns * 2)) *\<^sub>R ?f2, ?f2, x, ?a] \<in> set_of_apprs [B, F2, X, A]" (is "(?b#_)\<in> _") .
  hence "[?a, ?b, x] \<in> set_of_apprs [A, B, X]" by (rule set_of_apprs_imp) auto
  from goal1(11)[rule_format, OF this]
  have "[?a + ?b, ?a, ?b, x] \<in> set_of_apprs [R, A, B, X]" .
  hence "[?a + ?b, x] \<in> set_of_apprs [R, X]" by (rule set_of_apprs_imp) auto
  thus ?case using assms
    by (auto simp: rk2_increment algebra_simps diff_divide_distrib)
next
  case (goal2 FX A S XpS F2 B S' XpS' F2' B' R R' t x h')
  hence h': "h' * rk2_param optns \<in> {0..h * rk2_param optns}"
    by (auto intro!: assms mult_right_mono mult_nonneg_nonneg intro: less_imp_le)
  from goal2(1)[rule_format, OF `[x] \<in> set_of_apprs [X]`]
  have "[ode x, x] \<in> set_of_apprs [FX, X]" (is "(?fx#_)\<in> _")
    by auto
  from goal2(2)[rule_format, OF this]
  have "[((rk2_param optns * 2 - 1) / (rk2_param optns * 2)) *\<^sub>R ode x, ode x, x] \<in> set_of_apprs [A, FX, X]" (is "(?a#_)\<in> _") .
  hence "[?fx, ?a, x] \<in> set_of_apprs [FX, A, X]" by (rule set_of_apprs_imp) auto
  from goal2(7)[rule_format, OF h' this]
  have "[(h' * rk2_param optns) *\<^sub>R ?fx, ?fx, ?a, x] \<in> set_of_apprs [S', FX, A, X]" (is "(?s#_)\<in> _") .
  hence "[x, ?s, ?a, x] \<in> set_of_apprs [X, S', A, X]" by (rule set_of_apprs_imp) auto
  from goal2(8)[rule_format, OF this]
  have "[x + ?s, x, ?s, ?a, x] \<in> set_of_apprs [XpS', X, S', A, X]" (is "(?xps#_)\<in> _") .

  hence "[?xps, x, ?a] \<in> set_of_apprs [XpS', X, A]" by (rule set_of_apprs_imp) auto
  from goal2(9)[rule_format, OF this]
  have "[ode ?xps, ?xps, x, ?a] \<in> set_of_apprs [F2', XpS', X, A]" (is "(?f2#_)\<in> _") .

  hence "[?f2, x, ?a] \<in> set_of_apprs [F2', X, A]" by (rule set_of_apprs_imp) auto
  from goal2(10)[rule_format, OF this]
  have "[(1 / (rk2_param optns * 2)) *\<^sub>R ?f2, ?f2, x, ?a] \<in> set_of_apprs [B', F2', X, A]" (is "(?b#_)\<in> _") .
  hence "[?a, ?b, x] \<in> set_of_apprs [A, B', X]" by (rule set_of_apprs_imp) auto
  from goal2(12)[rule_format, OF this]
  have "[?a + ?b, ?a, ?b, x] \<in> set_of_apprs [R', A, B', X]" .
  hence "[?a + ?b, x] \<in> set_of_apprs [R', X]" by (rule set_of_apprs_imp) auto
  thus ?case using assms
    by (auto simp: rk2_increment algebra_simps diff_divide_distrib)
qed

lemma rk2_remainder_nres_spec:
  assumes "0 < h" "0 \<le> rk2_param optns"
  shows "rk2_remainder_nres optns h X Y FY \<le>
    SPEC (\<lambda>(R, R'). \<forall>x y fy. \<forall>tt\<in>{0..1}. \<forall>h1\<in>{0..h}. [x, y, fy] \<in> set_of_apprs [X, Y, FY] \<longrightarrow>
      [h ^ 3 *\<^sub>R ((1 / 6) *\<^sub>R (ode_d2 y fy fy + ode_d y (ode_d y fy)) -
        (rk2_param optns / 4) *\<^sub>R ode_d2 (x + (h1 * rk2_param optns * tt) *\<^sub>R ode x) (ode x) (ode x)), x, y, fy] \<in> set_of_apprs [R, X, Y, FY] \<and>
      [h1 ^ 3 *\<^sub>R ((1 / 6) *\<^sub>R (ode_d2 y fy fy + ode_d y (ode_d y fy)) -
        (rk2_param optns / 4) *\<^sub>R ode_d2 (x + (h1 * rk2_param optns * tt) *\<^sub>R ode x) (ode x) (ode x)), x, y, fy] \<in> set_of_apprs [R', X, Y, FY])"
  unfolding rk2_remainder_nres_def
  apply (intro refine_vcg)
proof safe
  case (goal1 a b c d e fxt f fa g h' i j j' x y fy tt h1)
  from goal1(16) have "[y, fy, fy, x] \<in> set_of_apprs [Y, FY, FY, X]"
    by (rule set_of_apprs_imp) auto
  with goal1(1) have "[ode_d2 y fy fy, y, fy, fy, x] \<in> set_of_apprs [a, Y, FY, FY, X]" (is "(?a#_)\<in> _")
    by auto
  hence "[y, fy, ?a, x] \<in> set_of_apprs [Y, FY, a, X]"
    by (rule set_of_apprs_imp) auto
  from goal1(2)[rule_format, OF this] have "[ode_d y fy, y, fy, ?a, x] \<in> set_of_apprs [b, Y, FY, a, X]" (is "(?b#_)\<in> _") .
  hence "[y, ?b, ?a, x, fy] \<in> set_of_apprs [Y, b, a, X, FY]"
    by (rule set_of_apprs_imp) auto
  from goal1(3)[rule_format, OF this]
  have "[ode_d y (ode_d y fy), y, ?b, ?a, x, fy] \<in> set_of_apprs [c, Y, b, a, X, FY]" (is "(?c#_)\<in>_") .
  hence "[?a, ?c, x, y, fy] \<in> set_of_apprs [a, c, X, Y, FY]"
    by (rule set_of_apprs_imp) auto
  from goal1(4)[rule_format, OF this]
  have "[?a + ?c, ?a, ?c, x, y, fy] \<in> set_of_apprs [d, a, c, X, Y, FY]" (is "(?d#_)\<in>_") .
  hence "[?d, x, y, fy] \<in> set_of_apprs [d, X, Y, FY]"
    by (rule set_of_apprs_imp) auto
  from goal1(5)[rule_format, OF this]
  have "[(1/6)*\<^sub>R?d, ?d, x, y, fy] \<in> set_of_apprs [e, d, X, Y, FY]" (is "(?e#_)\<in>_") .
  hence "[x, ?e, y, fy] \<in> set_of_apprs [X, e, Y, FY]"
    by (rule set_of_apprs_imp) auto
  from goal1(6)[rule_format, OF this]
  have "[ode x, x, ?e, y, fy] \<in> set_of_apprs [fxt, X, e, Y, FY]" (is "(?fxt#_)\<in>_") .
  hence *: "[?fxt, ?e, x, y, fy] \<in> set_of_apprs [fxt, e, X, Y, FY]"
    by (rule set_of_apprs_imp) auto
  have "h1 * rk2_param optns * tt \<in> {0..h * rk2_param optns}"
    using `tt \<in> _` assms `h1 \<in> _`
    apply (auto intro!: mult_nonneg_nonneg)
    apply (rule order_trans)
    defer
    apply (rule mult_right_le_one_le)
    apply (auto intro!: mult_nonneg_nonneg mult_mono)
    done
  from goal1(7)[rule_format, OF this *]
  have "[(h1 * rk2_param optns * tt)*\<^sub>R?fxt, ?fxt, ?e, x, y, fy] \<in> set_of_apprs [f, fxt, e, X, Y, FY]" (is "(?f#_)\<in>_") .
  hence "[x, ?f, ?fxt, ?e, y, fy] \<in> set_of_apprs [X, f, fxt, e, Y, FY]"
    by (rule set_of_apprs_imp) auto
  from goal1(8)[rule_format, OF this]
  have "[x + ?f, x, ?f, ?fxt, ?e, y, fy] \<in> set_of_apprs [fa, X, f, fxt, e, Y, FY]"  (is "(?fa#_)\<in>_") .
  hence "[?fa, ?fxt, ?fxt, ?e, x, y, fy] \<in> set_of_apprs [fa, fxt, fxt, e, X, Y, FY]"
    by (rule set_of_apprs_imp) auto
  from goal1(9)[rule_format, OF this]
  have "[ode_d2 ?fa ?fxt ?fxt, ?fa, ?fxt, ?fxt, ?e, x, y, fy] \<in> set_of_apprs [g, fa, fxt, fxt, e, X, Y, FY]" (is "(?g#_)\<in>_") .
  hence "[?g, ?e, x, y, fy] \<in> set_of_apprs [g, e, X, Y, FY]"
    by (rule set_of_apprs_imp) auto
  from goal1(10)[rule_format, OF this]
  have "[(- rk2_param optns / 4) *\<^sub>R ?g, ?g, ?e, x, y, fy] \<in> set_of_apprs [h', g, e, X, Y, FY]" (is "(?h'#_)\<in>_") .
  hence "[(- rk2_param optns / 4) *\<^sub>R ?g, ?e, x, y, fy] \<in> set_of_apprs [h', e, X, Y, FY]"
    by (rule set_of_apprs_imp) auto
  from goal1(11)[rule_format, OF this]
  have "[?h' + ?e, ?h', ?e, x, y, fy] \<in> set_of_apprs [i, h', e, X, Y, FY]" (is "(?i#_)\<in>_") .
  hence i: "[?i, x, y, fy] \<in> set_of_apprs [i, X, Y, FY]"
    by (rule set_of_apprs_imp) auto
  from goal1(12)[rule_format, OF this]
  have "[h^3 *\<^sub>R?i, ?i, x, y, fy] \<in> set_of_apprs [j, i, X, Y, FY]" (is "(?j#_)\<in>_") by simp
  hence "[?j, x, y, fy] \<in> set_of_apprs [j, X, Y, FY]"
    by (rule set_of_apprs_imp) auto
  thus ?case
    by (simp add: algebra_simps)
  have "h1^3 \<in> {0..h ^ 3}"
    using `h1 \<in> _` by (auto intro!: power_mono)
  from goal1(13)[rule_format, OF this i]
  have "[h1^3 *\<^sub>R?i, ?i, x, y, fy] \<in> set_of_apprs [j', i, X, Y, FY]" (is "(?j'#_)\<in>_") by simp
  hence j': "[?j', x, y, fy] \<in> set_of_apprs [j', X, Y, FY]"
    by (rule set_of_apprs_imp) auto
  thus "[h1 ^ 3 *\<^sub>R
     ((1 / 6) *\<^sub>R (ode_d2 y fy fy + ode_d y (ode_d y fy)) -
      (rk2_param optns / 4) *\<^sub>R
      ode_d2 (x + (h1 * rk2_param optns * tt) *\<^sub>R ode x)
       (ode x) (ode x)),
     x, y, fy]
    \<in> set_of_apprs [j', X, Y, FY]"
    by (simp add: algebra_simps)
qed

lemma rk2_step_spec:
  assumes "0 < stepsize optns" "0 < rk2_param optns" "rk2_param optns \<le> 1"
  shows "rk2_step optns X0 \<le> step_spec X0"
  unfolding rk2_step_def step_spec_def
  apply (intro refine_vcg)
  apply (rule assms)+
  apply auto
  apply (rule_tac order_trans[OF rk2_remainder_nres_spec])
  apply assumption apply (rule less_imp_le[OF assms(2)])
  apply (intro refine_vcg)
  apply (rule_tac order_trans[OF rk2_incr_nres_spec])
  apply assumption apply (rule assms)
  apply (intro refine_vcg)
  apply (auto simp: )
  defer
  defer
proof -
  case (goal1 h' CX0 FX0 FCX Rem Rem' I I' Step Step_ivl DE DE' x0)
  hence "0 \<le> h'" by simp
  let ?CX = "independent_appr X0 CX0"
  have "Triple_of_list ` set_of_apprs [X0, ?CX, FCX] \<subseteq> set_of_appr X0 \<times> set_of_appr ?CX \<times> set_of_appr FCX"
    by (auto elim!: set_of_apprsE dest!: set_of_apprs_Nil)
  moreover have "bounded (\<dots>)"
    by (rule set_of_appr_compact compact_imp_bounded bounded_Times)+
  ultimately have bounded: "bounded (Triple_of_list ` set_of_apprs [X0, ?CX, FCX])"
    by (blast intro: bounded_subset)

  interpret derivative2_set_bounded
    "\<lambda>(t, x). ode x" "\<lambda>(t, x) (dt, dx). ode_d x dx" "\<lambda>(t, x) (dt, dx) (dt', dy). ode_d2 x dx dy"
    apply unfold_locales
    apply (auto simp: convex_closed_interval set_of_appr_convex less_imp_le set_of_appr_nonempty)
    apply (rule derivative_eq_intros)+ apply simp
    apply simp
    apply (auto simp: split_beta' o_def)
    apply (rule diff_chain_at[OF has_derivative_snd[OF has_derivative_id] fderiv2, simplified o_def, THEN has_derivative_eq_rhs])
    apply simp
    done
  {
    fix h' h0::real and Rem assume "0 \<le> h0" "h0 \<le> h'" "0 \<le> h'" "h' \<in> existence_ivl x0"
    assume goal15: "\<forall>h\<in>{0..h'}. c1_on_open.flow ode UNIV x0 h \<in> set_of_appr ?CX"
    assume goal16: "\<forall>h1\<in>{0..h'}. \<forall>h2\<in>{0..h'}. x0 + h1 *\<^sub>R ode (c1_on_open.flow ode UNIV x0 h2) \<in> set_of_appr ?CX"
    assume goal18: "\<forall>x y fy. [x, y, fy] \<in> set_of_apprs [X0, ?CX, FCX] \<longrightarrow>
      (\<forall>tt\<in>{0..1}. \<forall>h1\<in>{h0..h'}.
          [h1 ^ 3 *\<^sub>R ((1 / 6) *\<^sub>R (ode_d2 y fy fy + ode_d y (ode_d y fy)) -
            (rk2_param optns / 4) *\<^sub>R ode_d2 (x + (h1 * rk2_param optns * tt) *\<^sub>R ode x) (ode x) (ode x)),
           x, y, fy] \<in> set_of_apprs [Rem, X0, ?CX, FCX])"
    have "flow x0 (0 + h') -
        discrete_evolution (rk2_increment (rk2_param optns) (\<lambda>(t, x). ode x)) (0 + h') 0 (flow x0 0)
      \<in> set_of_appr (ivl_appr_of_appr Rem)"
    proof (rule rk2_consistent_traj_set)
      show "0 \<le> h'" "0 + h' \<le> h'" "{0..h'} \<subseteq> UNIV" "set_of_appr X0 \<noteq> {}" "set_of_appr ?CX \<noteq> {}"
        "convex (set_of_appr ?CX)" "0 < rk2_param optns" "rk2_param optns \<le> 1" "flow x0 0 \<in> set_of_appr X0"
        using `0 \<le> h'`
        by (auto simp: set_of_appr_nonempty set_of_appr_convex assms `x0 \<in> set_of_appr X0`)
      show "\<And>s. s \<in> {0..h'} \<Longrightarrow> (flow x0 has_vector_derivative (case (s, flow x0 s) of (t, x) \<Rightarrow> ode x))
          (at s within {0..h'})"
        using flow_has_vector_derivative[of x0] ivl_subset_existence_ivl[OF _ `h' \<in> existence_ivl x0`]
        by (auto simp: has_vector_derivative_at_within)
      show "\<And>s. s \<in> {0..h'} \<Longrightarrow> c1_on_open.flow ode UNIV x0 s \<in> set_of_appr ?CX"
        using goal15 by simp
      from bounded
      show "bounded (Triple_of_list ` set_of_apprs [X0, ?CX, FCX])" by simp
      { 
        fix t::real and x x0 assume x0: "x0 \<in> set_of_appr X0" and x: "x \<in> set_of_appr ?CX"
        from x have CX0: "x \<in> set_of_appr CX0" by (simp add: independent_appr_eq)
        from x0 have "[x0] \<in> set_of_apprs [X0]" by (simp add: set_of_apprs_set_of_appr)
        hence "[x, x0] \<in> set_of_apprs [?CX, X0]"
          using independent_appr set_of_apprs_switch x0 CX0 by blast
        hence "[ode x, x, x0] \<in> set_of_apprs [FCX, ?CX, X0]"
          using goal1(2) by auto
        hence "[x0, x, ode x] \<in> set_of_apprs [X0, ?CX, FCX]"
          by (rule set_of_apprs_imp) auto
        thus "(x0, x, case (t, x) of (t, x) \<Rightarrow> ode x) \<in> Triple_of_list ` set_of_apprs [X0, ?CX, FCX]"
          by auto
      }
      show "flow x0 0 + (h' * rk2_param optns) *\<^sub>R (case (0, flow x0 0) of (t, x) \<Rightarrow> ode x) \<in> set_of_appr ?CX"
        apply simp
        apply (rule goal16[rule_format, of _ 0, simplified])
        using assms `h' \<ge> 0`
        by (auto intro!: mult_nonneg_nonneg mult_right_le_one_le)
      show "is_interval (set_of_appr (local.ivl_appr_of_appr Rem))"
        by (auto simp: ivl_appr_of_appr_def set_of_appr_of_ivl is_interval_closed_interval)
      fix ttt t tt ::real and xttt fxttt xt::'a
      assume tt: "tt \<in> {0..1}" and "(xt, xttt, fxttt) \<in> Triple_of_list ` set_of_apprs [X0, ?CX, FCX]"
      then obtain ys where ys: "Triple_of_list ys = (xt, xttt, fxttt)" "ys \<in> set_of_apprs [X0, ?CX, FCX]"
        by auto
      with length_set_of_apprs have "length ys = 3" by auto
      with ys have *: "[xt, xttt, fxttt] \<in> set_of_apprs [X0, ?CX, FCX]"
        by (auto simp: length_Suc_conv numeral_3_eq_3)
      from goal18[rule_format, OF * tt] have Rem_sets:
        "[h' ^ 3 *\<^sub>R ((1 / 6) *\<^sub>R
        (ode_d2 xttt fxttt fxttt + ode_d xttt (ode_d xttt fxttt)) -
        (rk2_param optns / 4) *\<^sub>R ode_d2 (xt + (h' * rk2_param optns * tt) *\<^sub>R ode xt) (ode xt) (ode xt)), xt, xttt, fxttt] \<in>
          set_of_apprs [Rem, X0, ?CX, FCX]"
        using `0 \<le> h'` `h0 \<le> h'`
        by simp
      from Rem_sets have "h' ^ 3 *\<^sub>R ((1 / 6) *\<^sub>R
        (ode_d2 xttt fxttt fxttt + ode_d xttt (ode_d xttt fxttt)) -
        (rk2_param optns / 4) *\<^sub>R ode_d2 (xt + (h' * rk2_param optns * tt) *\<^sub>R ode xt) (ode xt) (ode xt)) \<in>
          set_of_appr Rem"
       unfolding set_of_apprs_set_of_appr[symmetric]
       by (rule set_of_apprs_imp) auto
      also have "\<dots> \<subseteq> set_of_appr (ivl_appr_of_appr Rem)"
        by (auto simp: ivl_appr_of_appr_def set_of_appr_of_ivl)
      finally
      show "h' ^ 3 *\<^sub>R ((1 / 6) *\<^sub>R
          ((case (ttt, xttt) of (t, x) \<Rightarrow> \<lambda>(dt, dx) (dt', dy). ode_d2 x dx dy)
            (1, fxttt) (1, fxttt) + (case (ttt, xttt) of (t, x) \<Rightarrow> \<lambda>(dt, dx). ode_d x dx)
            (0, (case (ttt, xttt) of (t, x) \<Rightarrow> \<lambda>(dt, dx). ode_d x dx) (1, fxttt))) -
          (rk2_param optns / 4) *\<^sub>R (case (t + h' * (rk2_param optns * tt), xt + (h' * (rk2_param optns * tt)) *\<^sub>R
                 (case (t, xt) of (t, x) \<Rightarrow> ode x)) of (t, x) \<Rightarrow> \<lambda>(dt, dx) (dt', dy). ode_d2 x dx dy)
           (1, case (t, xt) of (t, x) \<Rightarrow> ode x) (1, case (t, xt) of (t, x) \<Rightarrow> ode x))
         \<in> set_of_appr (local.ivl_appr_of_appr Rem)"
        by (simp add: algebra_simps)
    qed
    hence Rem: "flow x0 h' - discrete_evolution (rk2_increment (rk2_param optns) (\<lambda>(t, x). ode x)) h' 0 x0
        \<in> set_of_appr (local.ivl_appr_of_appr Rem)"
      by simp
  } note Rem_wlog = this
  have x0s: "[x0] \<in> set_of_apprs [X0]" by (simp add: `x0 \<in> _` set_of_apprs_set_of_appr)
  from goal1(7)[rule_format, OF this]
  have I: "[rk2_increment (rk2_param optns) (\<lambda>(t, y). ode y) h' 0 x0, x0] \<in> set_of_apprs [I, X0]"
    (is "?res#_ \<in> _")
    by simp
  from goal1(8)[rule_format, OF this]
  have "[h' *\<^sub>R ?res, ?res, x0] \<in> set_of_apprs [Step, I, X0]" using `0 < h'` by simp
  hence "[x0, h' *\<^sub>R ?res] \<in> set_of_apprs [X0, Step]" by (rule set_of_apprs_imp) auto
  from goal1(10)[rule_format, OF this]
  have "[x0 + h' *\<^sub>R ?res, x0, h' *\<^sub>R ?res] \<in> set_of_apprs [DE, X0, Step]" by simp
  hence DE: "x0 + h' *\<^sub>R ?res \<in> set_of_appr DE"
    unfolding set_of_apprs_set_of_appr[symmetric]
    by (rule set_of_apprs_imp) auto
  from goal1(5) `x0 \<in> _` `0 < h'`
  have "h' \<in> existence_ivl x0" and goal15: "\<forall>h \<in> {0..h'}. flow x0 h \<in> set_of_appr ?CX"
    "\<forall>h1\<in>{0..h'}. \<forall>h2\<in>{0..h'}. x0 + h1 *\<^sub>R ode (c1_on_open.flow ode UNIV x0 h2) \<in> set_of_appr ?CX"
    by (simp_all add: independent_appr_eq)
  show "flow x0 h' \<in> set_of_appr (msum_appr DE (local.ivl_appr_of_appr Rem))"
    using goal1(6) `0 < h'`
    by (intro in_set_of_appr_msum_apprI[OF _ DE Rem_wlog[OF `0 \<le> h'` order_refl `0 \<le> h'` `h' \<in> _` goal15]])
      (simp_all add: discrete_evolution_def)
  {
    fix t
    assume t: "0 \<le> t" "t \<le> h'"
    with goal1(7)[rule_format, OF x0s]
    have I': "[rk2_increment (rk2_param optns) (\<lambda>(t, y). ode y) t 0 x0, x0] \<in> set_of_apprs [I', X0]"
      (is "?res#_ \<in> _")
      by simp
    from goal1(9)[rule_format, OF conjI, OF t I']
    have "[t *\<^sub>R ?res, ?res, x0] \<in> set_of_apprs [Step_ivl, I', X0]" .
    hence "[x0, t *\<^sub>R ?res] \<in> set_of_apprs [X0, Step_ivl]"
      by (rule set_of_apprs_imp) auto
    from goal1(11)[rule_format, OF this]
    have "[x0 + t *\<^sub>R ?res, x0, t *\<^sub>R ?res] \<in> set_of_apprs [DE', X0, Step_ivl]" .
    hence Res_ivl: "x0 + t *\<^sub>R ?res \<in> set_of_appr DE'"
      unfolding set_of_apprs_set_of_appr[symmetric]
      by (rule set_of_apprs_imp) auto
    have "t \<in> existence_ivl x0" using t ivl_subset_existence_ivl[OF _ `h' \<in> _`]
      by auto
    from goal1(5) `x0 \<in> _`
    have fi: "\<forall>h\<in>{0..t}. c1_on_open.flow ode UNIV x0 h \<in> set_of_appr ?CX"
      and rki: "\<forall>h1\<in>{0..t}. \<forall>h2\<in>{0..t}. x0 + h1 *\<^sub>R ode (c1_on_open.flow ode UNIV x0 h2) \<in> set_of_appr ?CX"
      using t by (auto simp: independent_appr_eq)
    from goal1(6) t have Rem': "\<forall>x y fy. [x, y, fy] \<in> set_of_apprs [X0, ?CX, FCX] \<longrightarrow>
      (\<forall>tt\<in>{0..1}. \<forall>h1\<in>{0..t}. [h1 ^ 3 *\<^sub>R ((1 / 6) *\<^sub>R (ode_d2 y fy fy + ode_d y (ode_d y fy)) -
        (rk2_param optns / 4) *\<^sub>R ode_d2 (x + (h1 * rk2_param optns * tt) *\<^sub>R ode x) (ode x) (ode x)),
          x, y, fy] \<in> set_of_apprs [Rem', X0, ?CX, FCX])" by auto
    show "flow x0 t \<in> set_of_appr (msum_appr DE' (local.ivl_appr_of_appr Rem'))"
      apply (intro in_set_of_appr_msum_apprI)
      defer
      defer
      apply (rule Rem_wlog[OF order_refl `0 \<le> t` `0 \<le> t`  `t \<in> _` fi rki Rem'])
      defer
      apply (rule Res_ivl)
      apply (simp add: discrete_evolution_def)
      done
  }
qed

lemma in_set_of_appr_atLeastAtMostD: "x \<in> set_of_appr X \<Longrightarrow> x \<in> {inf_of_appr X .. sup_of_appr X}"
  by auto

lemma
  below_inter_below_halfspace_eq:
  "appr_below_sctn optns X sctn \<Longrightarrow> set_of_appr X \<inter> below_halfspace sctn = set_of_appr X"
  by (auto intro!: appr_below_sctn)

lemma
  belows_inter_below_halfspace_eq:
  "(\<forall>X\<in>set XS. local.appr_below_sctn optns X sctn) \<Longrightarrow>
  UNION (set XS) set_of_appr \<inter> below_halfspace sctn = UNION (set XS) set_of_appr"
  by (auto intro!: appr_below_sctn)

lemma
  above_inter_below_halfspace_eq:
  "appr_above_sctn optns X sctn \<Longrightarrow> set_of_appr X \<inter> below_halfspace sctn = {}"
  by (auto dest: appr_above_sctn)

lemma
  not_intersecting_appr_below_sctnI:
  assumes "le_halfspace sctn x"
  assumes "x \<in> set_of_appr X"
  assumes "\<not>intersects_appr optns X sctn"
  shows "appr_below_sctn optns X sctn"
  using assms appr_inf_inner[of x X optns "normal sctn"]
  using appr_sup_inner[of x X "normal sctn" optns]
  by (auto simp: plane_of_def le_halfspace_def intersects_appr_def appr_below_sctn_def not_le)

lemma method_split:
  notes order_trans[OF rk2_step_spec[unfolded step_spec_def], refine_vcg]
    order_trans[OF euler_step_nres_spec[unfolded step_spec_def], refine_vcg]
  shows "0 < stepsize optns \<Longrightarrow> 0 < rk2_param optns \<Longrightarrow> rk2_param optns \<le> 1 \<Longrightarrow>
    (if method_id optns' = 2 then rk2_step else euler_step_nres) optns X \<le> step_spec X"
  unfolding step_spec_def euler_step_nres_def[symmetric] cond_application_beta
  by (refine_transfer refine_vcg)

declare order_trans[OF method_split[simplified step_spec_def], refine_vcg]

lemma
  intersection_iteration_impl:
  assumes "0 < stepsize optns" "0 < rk2_param optns" "rk2_param optns \<le> 1"
  shows "intersection_iteration_impl optns sctn X \<le>
    SPEC (\<lambda>(X', F, PS, CXS).
      flowsto (set_of_appr X  \<inter> below_halfspace sctn) (\<Union>(set_of_appr ` set CXS)) (set_of_appr X' \<inter> below_halfspace sctn \<union> \<Union>(set_of_appr ` set PS) \<inter> plane_of sctn))"
  using assms
  unfolding intersection_iteration_impl_def
  apply (refine_transfer refine_vcg)
  apply (rule WHILE_rule[where I="\<lambda>(X', F, PS, CXS). flowsto (set_of_appr X \<inter> below_halfspace sctn) (\<Union>(set_of_appr ` set CXS)) (set_of_appr X' \<inter> below_halfspace sctn \<union> \<Union>(set_of_appr ` set PS) \<inter> plane_of sctn)"])
  apply (simp add: below_inter_below_halfspace_eq)
  defer
  apply (force split: option.split split: split_if_asm)
  apply (refine_transfer refine_vcg)
  apply auto
proof -
  case (goal1 OX X1 _ PS CXS h CX X2 Inter OX2)
  from flowsto_UnE[OF `flowsto (set_of_appr X \<inter> _) _ (_ \<union> _)`] guess Xa Xb . note X = this
  {
    fix x assume x: "x \<in> set_of_appr X1" "x \<in> Collect (le_halfspace sctn)"
    let ?f = "\<lambda>s. flow x s \<bullet> normal sctn"
    from x have "?f 0 \<le> pstn sctn" by (auto simp: le_halfspace_def)
    from x goal1(11)
    have h: "h \<in> existence_ivl x" "flow x h \<in> set_of_appr X2" by auto
    {
      assume "\<not> le_halfspace sctn (flow x h)"
      hence "pstn sctn \<le> ?f h"
        by (auto simp: le_halfspace_def)
      have "\<forall>h'. 0 \<le> h' \<and> h' \<le> h \<longrightarrow> isCont (\<lambda>s. flow x s \<bullet> normal sctn) h'"
        using ivl_subset_existence_ivl[OF _ `h \<in> existence_ivl _`]
        by (auto intro!: continuous_intros flow_continuous)
      from IVT[OF `?f _ \<le> _` `_ \<le> ?f _` less_imp_le[OF `0 < h`] this]
      obtain s where s: "0 \<le> s" "s \<le> h" "?f s = pstn sctn" by auto
      hence "flow x s \<in> plane_of sctn"
        by (auto simp: plane_of_def)
      moreover
      have "flow x s \<in> set_of_appr CX"
        using goal1(11)[rule_format, of x] x s by auto
      hence "flow x s \<in> set_of_appr (reduce_appr optns CX)"
        using reduce_appr[of CX optns] by auto
      ultimately
      have "\<exists>s\<ge>0. s \<in> existence_ivl x \<and> flow x s \<in> set_of_appr Inter \<inter> plane_of sctn \<and>
          (\<forall>s\<in>{0..s}. c1_on_open.flow ode UNIV x s \<in> set_of_appr CX)"
        using ivl_subset_existence_ivl[OF _ `h \<in> existence_ivl _`] s goal1(6) goal1(11) x
        by (auto intro!: exI[where x=s])
    } moreover {
      assume "le_halfspace sctn (flow x h)"
      hence "\<exists>s\<ge>0. s \<in> existence_ivl x \<and> flow x s \<in> set_of_appr X2 \<inter> Collect (le_halfspace sctn) \<and>
          (\<forall>s\<in>{0..s}. c1_on_open.flow ode UNIV x s \<in> set_of_appr CX)"
        using h `0 < h` goal1(11) x
        by (auto intro!: exI[where x=h])
    } ultimately
    have "\<exists>s\<ge>0. s \<in> existence_ivl x \<and> flow x s \<in> set_of_appr Inter \<inter> plane_of sctn \<union> set_of_appr X2 \<inter> Collect (le_halfspace sctn)
      \<and> (\<forall>s\<in>{0..s}. c1_on_open.flow ode UNIV x s \<in> set_of_appr CX)"
      by auto
  } hence "flowsto (set_of_appr X1 \<inter> Collect (le_halfspace sctn)) (set_of_appr CX) (set_of_appr Inter \<inter> plane_of sctn \<union> set_of_appr X2 \<inter> Collect (le_halfspace sctn))"
    by (auto simp: flowsto_def)
  from flowsto_trans[OF X(2) this]
  have "flowsto Xa (set_of_appr CX \<union> (\<Union>x\<in>set CXS. set_of_appr x)) (set_of_appr Inter \<inter> plane_of sctn \<union> set_of_appr X2 \<inter> Collect (le_halfspace sctn))"
    by (simp add: ac_simps)
  from flowsto_unionI[OF this X(3)] X(1)
  have "flowsto (set_of_appr X \<inter> below_halfspace sctn) (set_of_appr CX \<union> (\<Union>x\<in>set CXS. set_of_appr x))
      (set_of_appr Inter \<inter> plane_of sctn \<union> set_of_appr X2 \<inter> Collect (le_halfspace sctn) \<union>
      (\<Union>x\<in>set PS. set_of_appr x) \<inter> plane_of sctn)"
    by simp
  also have "(set_of_appr Inter \<inter> plane_of sctn \<union> set_of_appr X2 \<inter> Collect (le_halfspace sctn) \<union>
      (\<Union>x\<in>set PS. set_of_appr x) \<inter> plane_of sctn) =
    (set_of_appr X2 \<inter> Collect (le_halfspace sctn) \<union> (set_of_appr Inter \<union> (\<Union>x\<in>set PS. set_of_appr x)) \<inter> plane_of sctn)"
    by auto
  finally show ?case .
qed

lemma
  do_intersection:
  assumes "0 < stepsize optns" "0 < rk2_param optns" "rk2_param optns \<le> 1"
  shows "do_intersection optns sctn X \<le> SPEC (\<lambda>(PS, CXS, RS).
    flowsto (set_of_appr X \<inter> below_halfspace sctn) (\<Union>(set_of_appr ` set CXS)) (\<Union>(set_of_appr ` set PS) \<inter> plane_of sctn \<union> (\<Union>(set_of_appr ` set RS)) \<inter> below_halfspace sctn))"
  using assms
  unfolding do_intersection_def
  apply (refine_transfer refine_vcg)
  apply (rule order_trans[OF intersection_iteration_impl])
  apply (auto simp: above_inter_below_halfspace_eq intro: flowsto_subset)
  done

fun resolve_sctn_invar where
  "resolve_sctn_invar optns sctn X0S (XS, PS, RS) \<longleftrightarrow>
    list_all (\<lambda>(h::real, _). h > 0) X0S \<and>
    list_all (\<lambda>(h::real, X). h > 0 \<and> safe_appr optns X) XS \<and>
    list_all (\<lambda>(X, XS). safe_appr optns X \<and> list_all (safe_appr optns) XS) PS \<and>
    list_all (safe_appr optns) RS \<and>
    (\<exists>CXS. (\<forall>CX\<in>CXS. safe_appr optns CX) \<and>
      flowsto (UNION (set (map snd X0S)) set_of_appr \<inter> below_halfspace sctn)
        (\<Union>(set_of_appr ` CXS))
        (((\<Union>(set_of_appr ` set (concat (map snd PS)))) \<inter> plane_of sctn)
          \<union> (\<Union>(set_of_appr ` set (map snd XS@RS))) \<inter> below_halfspace sctn) \<and>
       flowsto (UNION (set (map snd X0S)) set_of_appr \<inter> below_halfspace sctn)
        (\<Union>(set_of_appr ` CXS))
        (((\<Union>(set_of_appr ` set (map fst PS@(map snd XS)@RS))) \<inter> below_halfspace sctn)))"

lemma resolve_sctn_invar_empty23I:
  "(\<forall>(h, CX) \<in> set X0S. h > 0 \<and> safe_appr optns CX) \<Longrightarrow> resolve_sctn_invar optns sctn X0S (X0S, [], [])"
  by (auto simp add: list_all_iff split_beta' intro!: exI[where x="set (map snd X0S)"])

lemma resolve_sctn_invar1:
  assumes "resolve_sctn_invar optns sctn X0S (a, aa, ba)"
  assumes "(ab, bb) \<notin> set xa \<and> set a = insert (ab, bb) (set xa)"
  assumes "list_all (safe_appr optns) (split_appr optns bb)"
  shows "resolve_sctn_invar optns sctn X0S (map (Pair ab) (split_appr optns bb) @ xa, aa, ba)"
  using assms
  apply (simp add: list_all_iff)
  apply safe
  apply simp_all
  apply force
  apply force
  apply (rule_tac x=CXS in exI)
proof safe
  case goal1
  have subs: "set_of_appr bb \<subseteq> (UNION (set (split_appr optns bb)) set_of_appr)"
    by (auto simp: list_ex_iff dest!: split_appr[where optns=optns])
  have "flowsto ((\<Union>a\<in>set X0S. set_of_appr (snd a)) \<inter> Collect (le_halfspace sctn))
     (\<Union>x\<in>CXS. set_of_appr x)
     ((\<Union>x\<in>set aa. \<Union>x\<in>set (snd x). set_of_appr x) \<inter> plane_of sctn \<union>
      (set_of_appr bb \<union>
       ((\<Union>a\<in>set xa. set_of_appr (snd a)) \<union> (\<Union>x\<in>set ba. set_of_appr x))) \<inter>
      Collect (le_halfspace sctn))"
    using goal1 by auto
  thus ?case
    apply (rule flowsto_subset)
    using subs
    apply (auto)
    done
next
  case goal2
  have subs: "set_of_appr bb \<subseteq> (UNION (set (split_appr optns bb)) set_of_appr)"
    by (auto simp: list_ex_iff dest!: split_appr[where optns=optns])
  have "flowsto ((\<Union>a\<in>set X0S. set_of_appr (snd a)) \<inter> Collect (le_halfspace sctn))
     (\<Union>x\<in>CXS. set_of_appr x)
     ((set_of_appr bb \<union>
       ((\<Union>a\<in>set aa. set_of_appr (fst a)) \<union>
        ((\<Union>a\<in>set xa. set_of_appr (snd a)) \<union> (\<Union>x\<in>set ba. set_of_appr x)))) \<inter>
      Collect (le_halfspace sctn))"
    using goal2 by auto
  thus ?case
    apply (rule flowsto_subset)
    using subs
    apply (auto)
    done
qed

lemma resolve_sctn_invar_stepmod:
  assumes "resolve_sctn_invar optns sctn X0S (a, aa, ba)"
  assumes "snd ` set a = snd ` set a2"
  assumes "list_all (\<lambda>(h, _). h > 0) a2"
  shows "resolve_sctn_invar optns sctn X0S (a2, aa, ba)"
  using assms
  apply (auto simp: list_all_iff split_beta' intro!: divide_pos_pos)
  by (metis (no_types, lifting) image_iff img_snd)

lemma resolve_sctn_invar2:
  assumes "resolve_sctn_invar optns sctn X0S (a, aa, ba)"
  assumes "set a = insert (ab, bb) (set xa)"
  assumes "ac > 0"
  shows "resolve_sctn_invar optns sctn X0S ((ac / 2, bb) # map (\<lambda>(h, y). (h / 2, y)) xa, aa, ba)"
  using assms by (auto simp: list_all_iff split_beta')

lemma resolve_sctn_invar3:
  assumes "resolve_sctn_invar optns sctn X0S (a, aa, ba)"
  assumes "set a = insert (ab, bb) (set xa)"
  assumes "ac > 0"
  shows "resolve_sctn_invar optns sctn X0S ((ac / 2, bb) # xa, aa, ba)"
  using assms
  by (auto simp: list_all_iff split_beta' intro!: divide_pos_pos)

lemma resolve_sctn_invar_append:
  assumes "resolve_sctn_invar optns sctn X0S (a, aa, ba)"
  assumes "(ab, bb) \<notin> set xa \<and> set a = insert (ab, bb) (set xa)"
  assumes "0 < ac \<and>
       (\<forall>x0\<in>set_of_appr bb.
           ac \<in> c1_on_open.existence_ivl ode UNIV x0 \<and>
           c1_on_open.flow ode UNIV x0 ac \<in> set_of_appr be \<and>
           (\<forall>t\<in>{0..ac}. c1_on_open.flow ode UNIV x0 t \<in> set_of_appr ae))"
  assumes "\<not> local.intersects_appr optns ae sctn \<and> \<not> local.intersects_appr optns be sctn"
  assumes "h' > 0"
  assumes "safe_appr optns be"
  assumes "safe_appr optns ae"
  shows "resolve_sctn_invar optns sctn X0S (xa @ [(h', be)], aa, ba)"
  using assms
  apply (simp add: list_all_iff)
  apply safe
  apply simp_all
  apply (rule_tac x="insert ae CXS" in exI)
proof (auto simp: list_all_iff)
  case goal1 note * = this
  from goal1(17) have "flowsto ((\<Union>a\<in>set X0S. set_of_appr (snd a)) \<inter> Collect (le_halfspace sctn))
     (\<Union>x\<in>CXS. set_of_appr x)
     (set_of_appr bb \<inter> Collect (le_halfspace sctn) \<union>
      ((\<Union>x\<in>set aa. \<Union>x\<in>set (snd x). set_of_appr x) \<inter> plane_of sctn \<union>
      (((\<Union>a\<in>set xa. set_of_appr (snd a)) \<union> (\<Union>x\<in>set ba. set_of_appr x))) \<inter>
      Collect (le_halfspace sctn)))"
    by (rule flowsto_subset) auto
  also
  have xbc: "flowsto (set_of_appr bb \<inter> Collect (le_halfspace sctn)) (set_of_appr ae) (set_of_appr be \<inter> below_halfspace sctn)"
  proof (auto simp: flowsto_def)
    case (goal1 y)
    from assms have "0 \<in> {0..ac}" by simp
    with goal1(1) *(8)
    have 2: "y \<in> set_of_appr ae"
      by force
    have 3: "\<not> local.intersects_appr optns ae sctn"
      using * by auto
    from not_intersecting_appr_below_sctnI[OF `le_halfspace sctn y` 2 3]
    have ac_below: "appr_below_sctn optns ae sctn" .
    from * goal1 have "flow y ac \<in> set_of_appr be" by auto
    thus ?case using * goal1 ac_below
      by (auto intro!: exI[where x=ac] simp: appr_below_sctn)
  qed
  finally (flowsto_trans_Un)
  show ?case
    by (rule flowsto_subset) auto
  case (goal2 CXS)
  from goal2(18) have "flowsto ((\<Union>a\<in>set X0S. set_of_appr (snd a)) \<inter> Collect (le_halfspace sctn))
     (\<Union>x\<in>CXS. set_of_appr x)
     (set_of_appr bb \<inter> Collect (le_halfspace sctn) \<union>
       (((\<Union>a\<in>set aa. set_of_appr (fst a)) \<union>
        ((\<Union>a\<in>set xa. set_of_appr (snd a)) \<union> (\<Union>x\<in>set ba. set_of_appr x))) \<inter> Collect (le_halfspace sctn)))"
    by (rule flowsto_subset) auto
  also note xbc
  finally (flowsto_trans_Un)
  show ?case
    by (rule flowsto_subset) auto
qed

lemma resolve_sctn_invar4:
  assumes "resolve_sctn_invar optns sctn X0S (a, aa, ba)"
  assumes "list_all (\<lambda>(h, CX). 0 < h \<and> safe_appr optns CX) X0S"
  assumes "list_all (safe_appr optns) ag"
  assumes "list_all (safe_appr optns) af"
  assumes "list_all (safe_appr optns) bf"
  assumes  "(ab, bb) \<notin> set xa \<and> set a = insert (ab, bb) (set xa)"
  assumes "flowsto (set_of_appr bb \<inter> Collect (le_halfspace sctn))
        (\<Union>x\<in>set ag. set_of_appr x)
        ((\<Union>x\<in>set af. set_of_appr x) \<inter> plane_of sctn \<union>
         (\<Union>x\<in>set bf. set_of_appr x) \<inter> Collect (le_halfspace sctn))"
  shows "resolve_sctn_invar optns sctn X0S (xa, (bb, af) # aa, bf @ ba)"
  using assms
  apply (simp add: list_all_iff)
  apply safe
  apply simp_all
  apply (rule_tac x="set ag \<union> CXS" in exI)
proof (auto simp: list_all_iff)
  case goal1
  from goal1(15)
  have "flowsto ((\<Union>a\<in>set X0S. set_of_appr (snd a)) \<inter> Collect (le_halfspace sctn))
     (\<Union>x\<in>CXS. set_of_appr x)
     (set_of_appr bb \<inter> Collect (le_halfspace sctn) \<union>
        ((\<Union>x\<in>set aa. \<Union>x\<in>set (snd x). set_of_appr x) \<inter> plane_of sctn \<union>
        (((\<Union>a\<in>set xa. set_of_appr (snd a)) \<union> (\<Union>x\<in>set ba. set_of_appr x))) \<inter> Collect (le_halfspace sctn)))"
    by (rule flowsto_subset) auto
  also note goal1(5)
  finally (flowsto_trans_Un)
  show ?case
    by (rule flowsto_subset) auto
next
  case goal2
  from goal2(16)
  show ?case
    by (rule flowsto_subset) auto
qed

lemma resolve_sctn_invar5:
  assumes "resolve_sctn_invar optns sctn X0S (a, aa, ba)"
       "list_all (\<lambda>(h, CX). 0 < h \<and> safe_appr optns CX) X0S"
       "(ab, bb) \<notin> set xa \<and> set a = insert (ab, bb) (set xa)"
       "0 < ac \<and>
       (\<forall>x0\<in>set_of_appr bb.
           ac \<in> c1_on_open.existence_ivl ode UNIV x0 \<and>
           c1_on_open.flow ode UNIV x0 ac \<in> set_of_appr be \<and>
           (\<forall>t\<in>{0..ac}. c1_on_open.flow ode UNIV x0 t \<in> set_of_appr ae))"
       "\<not> local.intersects_appr optns ae sctn \<and> \<not> local.intersects_appr optns be sctn"
       "safe_appr optns ae"
       "safe_appr optns be"
  shows "resolve_sctn_invar optns sctn X0S (xa, aa, be # ba)"
  using assms
  apply (simp add: list_all_iff)
  apply safe
  apply (rule_tac x="insert ae CXS" in exI)
proof (auto simp: list_all_iff)
  case goal1 note * = this
  from goal1(17) have "flowsto ((\<Union>a\<in>set X0S. set_of_appr (snd a)) \<inter> Collect (le_halfspace sctn))
   (\<Union>x\<in>CXS. set_of_appr x)
   (set_of_appr bb \<inter> Collect (le_halfspace sctn) \<union> ((\<Union>x\<in>set aa. \<Union>x\<in>set (snd x). set_of_appr x) \<inter> plane_of sctn \<union>
    (((\<Union>a\<in>set xa. set_of_appr (snd a)) \<union> (\<Union>x\<in>set ba. set_of_appr x))) \<inter>
    Collect (le_halfspace sctn)))"
    by (rule flowsto_subset) auto
  also
  have xbc: "flowsto (set_of_appr bb \<inter> Collect (le_halfspace sctn))
    (set_of_appr ae)
    (set_of_appr be \<inter> below_halfspace sctn)"
  proof (auto simp: flowsto_def)
    case (goal1 y)
    from assms have "0 \<in> {0..ac}" by simp
    with goal1(1) *(8)
    have 2: "y \<in> set_of_appr ae"
      by force
    have 3: "\<not> local.intersects_appr optns ae sctn"
      using * by auto
    from not_intersecting_appr_below_sctnI[OF `le_halfspace sctn y` 2 3]
    have ac_below: "appr_below_sctn optns ae sctn" .
    from * goal1 have "flow y ac \<in> set_of_appr be" by auto
    thus ?case using * goal1 ac_below
      by (auto intro!: exI[where x=ac] simp: appr_below_sctn)
  qed
  finally (flowsto_trans_Un)
  show ?case
    by (rule flowsto_subset) auto
  case goal2
  from goal2(18)
  have "flowsto ((\<Union>a\<in>set X0S. set_of_appr (snd a)) \<inter> Collect (le_halfspace sctn))
     (\<Union>x\<in>CXS. set_of_appr x)
     (set_of_appr bb \<inter> Collect (le_halfspace sctn) \<union> (((\<Union>a\<in>set aa. set_of_appr (fst a)) \<union>
        ((\<Union>a\<in>set xa. set_of_appr (snd a)) \<union> (\<Union>x\<in>set ba. set_of_appr x)))) \<inter>
      Collect (le_halfspace sctn))"
    by (rule flowsto_subset) auto
  also note xbc
  finally (flowsto_trans_Un)
  show ?case
    by (rule flowsto_subset) auto
qed

declare resolve_sctn_invar.simps[simp del]

declare order_trans[OF do_intersection, refine_vcg]

lemma
  resolve_sctn:
  assumes optns: "0 < stepsize optns" "0 < rk2_param optns" "rk2_param optns \<le> 1"
    "list_all (\<lambda>(h, CX). h > 0 \<and> safe_appr optns CX) X0S"
  shows "resolve_sctn optns sctn X0S \<le> SPEC (\<lambda>(XS, PS, RS). resolve_sctn_invar optns sctn X0S (XS, PS, RS) \<and> XS = [])"
  using assms
  unfolding resolve_sctn_def
  apply (intro WHILE_rule[where I="resolve_sctn_invar optns sctn X0S"])
    apply (rule local.resolve_sctn_invar_empty23I)
    apply (simp add: belows_inter_below_halfspace_eq split_beta list_all_iff)
   defer
   apply force
  apply (refine_transfer refine_vcg)
   apply simp
   apply (metis resolve_sctn_invar1)
  apply (refine_transfer refine_vcg)
     apply (fastforce simp add: list_all_iff split_beta' resolve_sctn_invar.simps)
    apply simp
   apply simp
  apply (refine_transfer refine_vcg)
   apply simp
   apply (metis resolve_sctn_invar2)
  apply (refine_transfer refine_vcg)
    apply simp
    apply (metis resolve_sctn_invar3)
   apply (refine_transfer refine_vcg)
      apply (fastforce simp add: list_all_iff split_beta' resolve_sctn_invar.simps)
     apply (fastforce simp add: list_all_iff split_beta' resolve_sctn_invar.simps)
    apply (fastforce simp add: list_all_iff split_beta' resolve_sctn_invar.simps)
   apply (refine_transfer refine_vcg)
   apply (simp add: )
  apply (metis resolve_sctn_invar4)
  apply (refine_transfer refine_vcg)
   apply simp
   apply (rule resolve_sctn_invar_append) apply assumption+
     apply (fastforce simp add: list_all_iff split_beta' resolve_sctn_invar.simps)
    apply assumption
   apply assumption
  apply (refine_transfer refine_vcg)
  apply simp
  apply (rule resolve_sctn_invar5) apply assumption+
  done

lemma ivl_of_apprs: "(\<Union>x\<in>set XS. set_of_appr x) \<subseteq> set_of_appr (ivl_of_apprs XS)"
  by (auto simp: ivl_of_apprs_def set_of_appr_of_ivl cINF_lower2 cSUP_upper2)

lemma not_disjoint_imp_le1: "\<not> disjoint_apprs xd x \<Longrightarrow> inf_of_appr xd \<le> sup_of_appr x"
  by (auto simp: disjoint_apprs_def list_ex_iff not_less eucl_le[where 'a='a])

lemma not_disjoint_imp_le2: "\<not> disjoint_apprs xd x \<Longrightarrow> inf_of_appr x \<le> sup_of_appr xd"
  by (auto simp: disjoint_apprs_def list_ex_iff not_less eucl_le[where 'a='a])

lemma partition_overappr:
  "partition optns XS \<le> SPEC (\<lambda>YS. UNION (set XS) set_of_appr \<subseteq> UNION (set YS) set_of_appr)"
  unfolding partition_def
  apply (intro refine_vcg)
  apply (rule WHILE_rule[where I="\<lambda>(RS, PS). UNION (set XS) set_of_appr \<subseteq> UNION (set (RS@PS)) set_of_appr"])
  apply (simp add: ivl_of_apprs)
  defer
  apply force
  apply (intro refine_vcg)
  apply (auto simp: filter_empty_conv dest!: disjoint_apprs)
proof -
  case goal1
  hence "xb \<in> (\<Union>x\<in>set [a\<leftarrow>XS . \<not> disjoint_apprs a x]. set_of_appr x)"
    by (auto intro!: exI[where x=xc] dest!: disjoint_apprs)
  also note ivl_of_apprs
  finally have "xb \<in> set_of_appr (ivl_of_apprs [a\<leftarrow>XS . \<not> disjoint_apprs a x])" .
  hence "xb \<in> set_of_appr (appr_of_ivl
    (sup (inf_of_appr x) (inf_of_appr (local.ivl_of_apprs [a\<leftarrow>XS . \<not> disjoint_apprs a x])))
    (inf (sup_of_appr x) (sup_of_appr (local.ivl_of_apprs [a\<leftarrow>XS . \<not> disjoint_apprs a x]))))"
    apply (subst set_of_appr_of_ivl)
    using goal1
    apply (auto simp: inf_of_appr_of_ivl sup_of_appr_of_ivl not_disjoint_imp_le1
      not_disjoint_imp_le2 ivl_of_apprs_def set_of_appr_of_ivl cINF_lower2 cSUP_upper2)
    done
  thus ?case
    by (auto dest!: split_appr simp: list_ex_iff)
qed

lemmas partition_overappr_le[refine_vcg] = partition_overappr[THEN order_trans]

lemma in_plane_of_imp_le_halfspace[simp]: "x \<in> plane_of sctn \<Longrightarrow> le_halfspace sctn x"
  by (auto simp: plane_of_def le_halfspace_def)

lemma resolve_collect:
  assumes "0 < stepsize optns" "0 < rk2_param optns" "rk2_param optns \<le> 1"
  assumes "list_all (safe_appr optns) X0S"
  shows "resolve_collect optns sctn X0S \<le>
    SPEC (\<lambda>(XS, XSg, RS).
      (\<exists>CXS. (\<forall>CX\<in>CXS. safe_appr optns CX) \<and>
        flowsto
          (UNION (set X0S) set_of_appr \<inter> below_halfspace sctn)
          (UNION CXS set_of_appr)
          (UNION (set (XS@RS)) set_of_appr \<inter> below_halfspace sctn) \<and>
        (flowsto
          (UNION (set X0S) set_of_appr \<inter> below_halfspace sctn)
          (UNION CXS set_of_appr)
          ((UNION (set (XSg)) set_of_appr \<inter> plane_of sctn) \<union> (UNION (set (RS)) set_of_appr \<inter> below_halfspace sctn)))))"
  unfolding resolve_collect_def
  apply (refine_transfer refine_vcg)
  apply (rule order_trans[OF resolve_sctn])
  apply fact+
  using assms apply (fastforce simp add: list_all_iff)
  apply (refine_transfer refine_vcg)
  apply (force simp: resolve_sctn_invar.simps)
  apply (refine_transfer refine_vcg)
  apply (simp add: resolve_sctn_invar.simps)
  apply safe
  apply (rule_tac x=CXS in exI)
  apply simp
  apply rule
  apply (rule flowsto_subset) apply assumption  apply (auto simp: )[2]
  apply (rule flowsto_subset) apply assumption  apply (auto simp: )[2]
  apply (refine_transfer refine_vcg)
  apply (simp add: resolve_sctn_invar.simps)
  apply safe
  apply (rule_tac x=CXS in exI)
  apply simp
  apply (rule flowsto_subset) apply assumption apply (auto simp: )[2]
  done

lemmas resolve_collect_le[refine_vcg] = resolve_collect[THEN order_trans]

lemma
  next_sections_set_eq:
  shows "next_sections optns d xs \<le> SPEC (\<lambda>ys. set (List.maps fst ys) = set xs)"
  unfolding next_sections_def
  apply (refine_transfer refine_vcg)
  apply (rule FOREACH_rule[where I="\<lambda>ys x. set xs = ys \<union> set (map fst x)"])
  apply simp
  apply simp
  apply (refine_transfer refine_vcg)
  apply (force)
  apply (refine_transfer refine_vcg)
  apply (auto simp: List.maps_def o_def split_beta' Let_def)
  done

lemma
  inf_of_ivl_of_apprs: "x \<in> set xs \<Longrightarrow> inf_of_appr (local.ivl_of_apprs xs) \<le> inf_of_appr x"
  and sup_of_ivl_of_apprs: "x \<in> set xs \<Longrightarrow> sup_of_appr x \<le> sup_of_appr (local.ivl_of_apprs xs)"
  using ivl_of_apprs[of xs]
  by (auto simp: ivl_of_apprs_def set_of_appr_of_ivl cINF_lower2 cSUP_upper2)

lemma appr_inf_inner_le: "appr_inf_inner optns x b \<le> appr_sup_inner optns x b"
proof -
  obtain y where "y \<in> set_of_appr x" using set_of_appr_nonempty[of x] by auto
  from appr_inf_inner[OF this, of optns b] appr_sup_inner[OF this, of b optns]
  show ?thesis by simp
qed

lemma max_height_lemma:
  assumes "X \<in> set XS"
  shows "appr_sup_inner optns X b \<le> max_height optns b XS"
  using assms
  by (cases XS) (force simp: max_height_def set_of_appr_of_ivl algebra_simps
    intro: add_mono fold_max_le_self fold_max_le)+

lemma max_height_lemma':
  assumes "x \<in> set_of_appr X"
  assumes "X \<in> set XS"
  shows "x \<bullet> b \<le> max_height optns b XS"
  using assms
  by (rule order_trans[OF appr_sup_inner max_height_lemma])

(*
lemma next_section_lemma:
  assumes "x \<in> set (map fst xs)" "\<And>x. x \<in> set (map snd xs) \<Longrightarrow> x \<ge> 0" "d \<ge> 0"
  shows "appr_below_sctn optns x (next_section optns b d xs)"
  using assms
  unfolding appr_below_sctn_def next_section_def'
  apply (auto simp: appr_below_sctn_def  Let_def intro!: order_trans[OF appr_inf_inner_le])
proof -
  case (goal1 c)
  hence in_set: "max_height_of optns b (d * c) x \<in> ((\<lambda>(X, f). local.max_height_of optns b (d * f) X) ` set xs)"
    "c \<ge> 0"
    by auto
  have "appr_sup_inner optns x b \<le> max_height_of optns b (d * c) x"
    by (rule max_height_lemma') (rule mult_nonneg_nonneg[OF `d \<ge> 0` `c \<ge> 0`])
  also have "\<dots> \<le> Max (insert 0 ((\<lambda>(X, f). local.max_height_of optns b (d * f) X) ` set xs))"
    using in_set by simp
  finally show ?case ?case by auto
qed
*)

lemma snd_strongest_transversal_nonneg: "0 \<le> snd (strongest_transversal r)"
  by (auto simp: strongest_transversal_def strongest_direction_def Let_def)

lemma
  next_sections_below:
  shows "next_sections optns d xs \<le> SPEC (list_all (\<lambda>(xs, sctn). list_all (\<lambda>x. appr_below_sctn optns x sctn) xs))"
  unfolding next_sections_def
  apply (refine_transfer refine_vcg)
  apply (rule FOREACH_rule[where I="\<lambda>ys x. set xs = ys \<union> set (map fst x) \<and> (\<forall>y \<in> set (map snd x). snd y \<ge> 0)"])
    --"TODO: extract lemma from @{thm next_sections_set_eq} ?"
  apply simp
  apply simp
  apply (refine_transfer refine_vcg)
  apply (force simp: snd_strongest_transversal_nonneg)
  apply simp
  apply (auto simp: list_all_iff)
  unfolding Let_def
  apply simp
  apply safe
  apply (simp add: appr_below_sctn_def)
proof -
  case (goal1)
  hence "x \<in> set (map (fst \<circ> (\<lambda>(x, _, y). (x, y))) [(x, b', s)\<leftarrow>\<sigma> . aa = b'])"
    by simp
  note * = order_trans[OF max_height_lemma[OF this, of optns ]]
  show ?case
    by (fastforce intro!: * add_nonneg_nonneg goal1 split: option.split option.split_asm dest!: find_SomeD(1))
qed

definition "next_sections_spec optns XS \<equiv> \<lambda>R. set (List.maps fst R) = set XS \<and>
  list_all (\<lambda>(xs, sctn). list_all (\<lambda>x. local.appr_below_sctn optns x sctn) xs) R"

lemma next_sections_spec[refine_vcg]:
  "SPEC (next_sections_spec optns xs) \<le> z \<Longrightarrow> next_sections optns d xs \<le> z"
  unfolding next_sections_spec_def
  by (rule order_trans[OF SPEC_rule_conjI[OF next_sections_set_eq next_sections_below]])

definition "poincare_distance_d_invar optns X0S = (\<lambda>(unres, cps, stops).
  (\<exists>CXS. Ball CXS (safe_appr optns) \<and> flowsto (UNION (set X0S) set_of_appr)
    (UNION CXS set_of_appr)
    ((\<Union>(xs, sctn)\<in>set unres. UNION (set xs) set_of_appr \<inter> below_halfspace sctn) \<union>
    (\<Union>(xs, sctn)\<in>set cps. UNION (set xs) set_of_appr \<inter> below_halfspace sctn) \<union>
    (\<Union>(xs, sctn)\<in>set stops. UNION (set xs) set_of_appr \<inter> plane_of sctn))))"

lemma list_all_nested_fst: "list_all (\<lambda>(xs, _). list_all P xs) ys \<longleftrightarrow> list_all P (List.maps fst ys)"
  by (induct ys) (auto simp add: maps_def)

lemma Un_both_mono: "(\<And>x. x \<in> X \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>X. g x)"
  by auto

lemma poincare_distance_d1:
"poincare_distance_d_invar optns X0S (ab, aaa, baa) \<Longrightarrow>
       ab \<noteq> [] \<Longrightarrow>
       hd ab = (aba, bb) \<Longrightarrow>
       list_all (safe_appr optns) aba \<Longrightarrow>
       next_sections_spec optns bda xa \<Longrightarrow>
       \<forall>x\<in>CXS'. safe_appr optns x \<Longrightarrow>
       flowsto ((\<Union>x\<in>set aba. set_of_appr x) \<inter> Collect (le_halfspace bb))
        (\<Union>x\<in>CXS'. set_of_appr x)
        (((\<Union>x\<in>set aca. set_of_appr x) \<union> (\<Union>x\<in>set bda. set_of_appr x)) \<inter>
         Collect (le_halfspace bb)) \<Longrightarrow>
       flowsto ((\<Union>x\<in>set aba. set_of_appr x) \<inter> Collect (le_halfspace bb))
        (\<Union>x\<in>CXS'. set_of_appr x)
        ((\<Union>x\<in>set ada. set_of_appr x) \<inter> plane_of bb \<union>
         (\<Union>x\<in>set bda. set_of_appr x) \<inter> Collect (le_halfspace bb)) \<Longrightarrow>
       poincare_distance_d_invar optns X0S
        (tl ab @ xa, aaa, (ada, bb) # baa)"
  apply (simp add: poincare_distance_d_invar_def next_sections_spec_def, safe)
  apply (rule_tac x="CXS' \<union> CXS" in exI)
  apply (auto simp: neq_Nil_conv)
proof -
  case goal1
  hence bda: "set bda = set (List.maps fst xa)" by simp
  from goal1(8) have *: "flowsto (\<Union>x\<in>set X0S. set_of_appr x) (\<Union>x\<in>CXS. set_of_appr x)
     ((\<Union>x\<in>set aba. set_of_appr x) \<inter> Collect (le_halfspace bb) \<union> (
      (\<Union>x\<in>set ys. case x of (xs, sctn) \<Rightarrow> (\<Union>x\<in>set xs. set_of_appr x) \<inter> Collect (le_halfspace sctn)) \<union>
      (\<Union>x\<in>set aaa. case x of (xs, sctn) \<Rightarrow> (\<Union>x\<in>set xs. set_of_appr x) \<inter> Collect (le_halfspace sctn)) \<union>
      (\<Union>x\<in>set baa. case x of (xs, sctn) \<Rightarrow> (\<Union>x\<in>set xs. set_of_appr x) \<inter> plane_of sctn)))"
    by (auto simp: ac_simps)
  have "(\<Union>x\<in>set xa. (\<Union>x\<in>set (fst x). set_of_appr x) \<inter> Collect (le_halfspace (snd x))) =
    (\<Union>x\<in>set xa. (\<Union>x\<in>set (fst x). set_of_appr x))"
    apply rule apply force
    apply (rule Un_both_mono)
    using goal1(6)
    apply (subst belows_inter_below_halfspace_eq[where optns=optns])
    apply safe
    apply (auto simp: list_all_iff)
    done
  with flowsto_trans_Un[OF * goal1(4)]
  show ?case unfolding bda
    apply (simp add: maps_def split_beta')
    apply (rule flowsto_subset, assumption)
    apply auto
    done
qed

lemma poincare_distance_d2:
"poincare_distance_d_invar optns X0S (ab, aaa, baa) \<Longrightarrow>
       ab \<noteq> [] \<Longrightarrow>
       hd ab = (aba, bb) \<Longrightarrow>
       list_all (safe_appr optns) aba \<Longrightarrow>
       next_sections_spec optns bda xa \<Longrightarrow>
       bb \<notin> set (stop_sections optns) \<Longrightarrow>
       bb \<in> set (checkpoint_sections optns) \<Longrightarrow>
       \<forall>x\<in>CXS'. safe_appr optns x \<Longrightarrow>
       flowsto ((\<Union>x\<in>set aba. set_of_appr x) \<inter> Collect (le_halfspace bb))
        (\<Union>x\<in>CXS'. set_of_appr x)
        (((\<Union>x\<in>set aca. set_of_appr x) \<union> (\<Union>x\<in>set bda. set_of_appr x)) \<inter>
         Collect (le_halfspace bb)) \<Longrightarrow>
       flowsto ((\<Union>x\<in>set aba. set_of_appr x) \<inter> Collect (le_halfspace bb))
        (\<Union>x\<in>CXS'. set_of_appr x)
        ((\<Union>x\<in>set ada. set_of_appr x) \<inter> plane_of bb \<union>
         (\<Union>x\<in>set bda. set_of_appr x) \<inter> Collect (le_halfspace bb)) \<Longrightarrow>
       poincare_distance_d_invar optns X0S (tl ab @ xa, (ada, bb) # aaa, baa)"
  apply (simp add: poincare_distance_d_invar_def next_sections_spec_def, safe)
  apply (rule_tac x="CXS' \<union> CXS" in exI)
  apply (auto simp: neq_Nil_conv)
proof -
  case goal1
  hence bda: "set bda = set (List.maps fst xa)" by simp
  from goal1(10) have *: "flowsto (\<Union>x\<in>set X0S. set_of_appr x) (\<Union>x\<in>CXS. set_of_appr x)
     ((\<Union>x\<in>set aba. set_of_appr x) \<inter> Collect (le_halfspace bb) \<union> (
      (\<Union>x\<in>set ys. case x of (xs, sctn) \<Rightarrow> (\<Union>x\<in>set xs. set_of_appr x) \<inter> Collect (le_halfspace sctn)) \<union>
      (\<Union>x\<in>set aaa. case x of (xs, sctn) \<Rightarrow> (\<Union>x\<in>set xs. set_of_appr x) \<inter> Collect (le_halfspace sctn)) \<union>
      (\<Union>x\<in>set baa. case x of (xs, sctn) \<Rightarrow> (\<Union>x\<in>set xs. set_of_appr x) \<inter> plane_of sctn)))"
    by (auto simp: ac_simps)
  have "(\<Union>x\<in>set xa. (\<Union>x\<in>set (fst x). set_of_appr x) \<inter> Collect (le_halfspace (snd x))) =
    (\<Union>x\<in>set xa. (\<Union>x\<in>set (fst x). set_of_appr x))"
    apply rule apply force
    apply (rule Un_both_mono)
    using goal1(8)
    apply (subst belows_inter_below_halfspace_eq[where optns=optns])
    apply safe
    apply (auto simp: list_all_iff)
    done
  with flowsto_trans_Un[OF * goal1(6)]
  show ?case unfolding bda
    apply (simp add: maps_def split_beta')
    apply (rule flowsto_subset, assumption)
    apply auto
    done
qed

lemma poincare_distance_d3:
"poincare_distance_d_invar optns X0S (ab, aaa, baa) \<Longrightarrow>
       ab \<noteq> [] \<Longrightarrow>
       hd ab = (aba, bb) \<Longrightarrow>
       list_all (safe_appr optns) aba \<Longrightarrow>
       next_sections_spec optns bda xa \<Longrightarrow>
       bb \<notin> set (stop_sections optns) \<Longrightarrow>
       bb \<notin> set (checkpoint_sections optns) \<Longrightarrow>
       next_sections_spec optns aca xb \<Longrightarrow>
       \<forall>x\<in>CXS'. safe_appr optns x \<Longrightarrow>
       flowsto ((\<Union>x\<in>set aba. set_of_appr x) \<inter> Collect (le_halfspace bb))
        (\<Union>x\<in>CXS'. set_of_appr x)
        (((\<Union>x\<in>set aca. set_of_appr x) \<union> (\<Union>x\<in>set bda. set_of_appr x)) \<inter>
         Collect (le_halfspace bb)) \<Longrightarrow>
       flowsto ((\<Union>x\<in>set aba. set_of_appr x) \<inter> Collect (le_halfspace bb))
        (\<Union>x\<in>CXS'. set_of_appr x)
        ((\<Union>x\<in>set ada. set_of_appr x) \<inter> plane_of bb \<union>
         (\<Union>x\<in>set bda. set_of_appr x) \<inter> Collect (le_halfspace bb)) \<Longrightarrow>
       poincare_distance_d_invar optns X0S (tl ab @ xb @ xa, aaa, baa)"
  apply (simp add: poincare_distance_d_invar_def next_sections_spec_def, safe)
  apply (rule_tac x="CXS' \<union> CXS" in exI)
  apply (auto simp: neq_Nil_conv)
proof -
  case goal1
  hence bda: "set bda = set (List.maps fst xa)" by simp
  from goal1 have ada: "set aca = set (List.maps fst xb)" by simp
  from goal1(12) have *: "flowsto (\<Union>x\<in>set X0S. set_of_appr x) (\<Union>x\<in>CXS. set_of_appr x)
     ((\<Union>x\<in>set aba. set_of_appr x) \<inter> Collect (le_halfspace bb) \<union> (
      (\<Union>x\<in>set ys. case x of (xs, sctn) \<Rightarrow> (\<Union>x\<in>set xs. set_of_appr x) \<inter> Collect (le_halfspace sctn)) \<union>
      (\<Union>x\<in>set aaa. case x of (xs, sctn) \<Rightarrow> (\<Union>x\<in>set xs. set_of_appr x) \<inter> Collect (le_halfspace sctn)) \<union>
      (\<Union>x\<in>set baa. case x of (xs, sctn) \<Rightarrow> (\<Union>x\<in>set xs. set_of_appr x) \<inter> plane_of sctn)))"
    by (auto simp: ac_simps)
  have xa: "(\<Union>x\<in>set xa. (\<Union>x\<in>set (fst x). set_of_appr x) \<inter> Collect (le_halfspace (snd x))) =
    (\<Union>x\<in>set xa. (\<Union>x\<in>set (fst x). set_of_appr x))"
    apply rule apply force
    apply (rule Un_both_mono)
    using goal1(8)
    apply (subst belows_inter_below_halfspace_eq[where optns=optns])
    apply safe
    apply (auto simp: list_all_iff)
    done
  have xb: "(\<Union>x\<in>set xb. (\<Union>x\<in>set (fst x). set_of_appr x) \<inter> Collect (le_halfspace (snd x))) =
    (\<Union>x\<in>set xb. (\<Union>x\<in>set (fst x). set_of_appr x))"
    apply rule apply force
    apply (rule Un_both_mono)
    using goal1
    apply (subst belows_inter_below_halfspace_eq[where optns=optns])
    apply safe
    apply (auto simp: list_all_iff)
    done
  from xa xb flowsto_trans_Un[OF * goal1(5)]
  show ?case unfolding bda ada
    apply (simp add: maps_def split_beta')
    apply (rule flowsto_subset, assumption)
    apply auto
    done
qed

lemma poincare_distance_d_invar4:
  "poincare_distance_d_invar optns X0S ([], aaa, baa) \<Longrightarrow>
       aaa \<noteq> [] \<Longrightarrow>
       list_all (\<lambda>(xs, sctn). list_all (\<lambda>x. local.appr_below_sctn optns x sctn) xs) \<sigma> \<Longrightarrow>
       set (List.maps fst aaa) = set (List.maps fst \<sigma>) \<Longrightarrow>
       poincare_distance_d_invar optns X0S (\<sigma>, [], baa)"
  apply (simp add: poincare_distance_d_invar_def next_sections_spec_def, safe)
  apply (rule_tac x="CXS" in exI)
  apply (auto simp: neq_Nil_conv)
  apply (auto simp: split_beta' list_all_iff maps_def)
proof -
  case goal1
  have *: "(\<Union>x\<in>set \<sigma>. (\<Union>x\<in>set (fst x). set_of_appr x) \<inter> Collect (le_halfspace (snd x))) =
    (\<Union>x\<in>set \<sigma>. (\<Union>x\<in>set (fst x). set_of_appr x))"
    apply rule apply force
    apply (rule Un_both_mono)
    using goal1
    apply (subst belows_inter_below_halfspace_eq[where optns=optns])
    apply safe
    apply (auto simp: list_all_iff)
    done
  have **: "(\<Union>x\<in>set \<sigma>. UNION (set (fst x)) set_of_appr) =
    \<Union>(set_of_appr `(\<Union>a\<in>set \<sigma>. set (fst a)))"
    by auto
  from goal1(4) show ?case unfolding * ** goal1(2)[symmetric]
    by (rule flowsto_subset) auto
qed

lemma poincare_distance_d:
  assumes [refine_vcg]: "0 < stepsize optns" "0 < rk2_param optns" "rk2_param optns \<le> 1"
  assumes start_below: "\<forall>x\<in>set X0S. local.appr_below_sctn optns x (start_section optns)"
  assumes start_safe: "\<forall>x\<in>set X0S. safe_appr optns x"
  shows "poincare_distance_d optns X0S \<le>
    SPEC (\<lambda>stops.
      (\<exists>CXS. Ball CXS (safe_appr optns) \<and> flowsto
      (UNION (set X0S) set_of_appr)
      (UNION (CXS) set_of_appr)
      (\<Union>(XS, sctn)\<in>set stops. (UNION (set XS) set_of_appr) \<inter> plane_of sctn)))"
  unfolding poincare_distance_d_def
  apply (refine_transfer refine_vcg)
  apply (rule WHILE_rule[where I = "poincare_distance_d_invar optns X0S"])
  apply (simp add: List.maps_def assms poincare_distance_d_invar_def belows_inter_below_halfspace_eq[OF start_below])
  defer
  apply (refine_transfer refine_vcg)
  apply (auto simp: )[1]
  apply (metis poincare_distance_d1)
  apply (refine_transfer refine_vcg)
  apply (auto simp: )[1]
  apply (metis poincare_distance_d2)
  apply (refine_transfer refine_vcg)
  apply (auto simp: )[1]
  apply (metis poincare_distance_d3)
  apply (refine_transfer refine_vcg)
  apply (rule_tac I="\<lambda>INPUT STATE.
    (list_all (\<lambda>(xs, sctn). list_all (\<lambda>x. local.appr_below_sctn optns x sctn) xs) STATE) \<and>
(set (List.maps fst aa) = (\<Union>(set ` fst ` INPUT)) \<union> set (List.maps fst STATE))" in FOREACH_rule, simp, simp)
  apply (auto simp add: List.maps_def list_all_iff poincare_distance_d_invar_def)[1]
  apply force
  apply (refine_transfer refine_vcg)
  apply (auto simp add: List.maps_def next_sections_spec_def list_all_iff split_beta')[1]
  apply (refine_transfer refine_vcg)
  apply (auto )[1]
  apply (metis poincare_distance_d_invar4)
  apply (refine_transfer refine_vcg)
  apply (simp add: poincare_distance_d_invar_def list_all_iff)
  apply (rule exI[where x="set X0S"])
  using assms by auto

fun set_res_of_appr_res
  where "set_res_of_appr_res (t0', CX, t1', X) = (t0', set_of_appr CX, t1', set_of_appr X)"

definition
  "enclosure f t0 t1 xs = list_all (\<lambda>(t0', CX, t1', X).
    f t1' \<in> X \<and> (\<forall>t \<in> {t0'::real .. t1'}. f t \<in> CX) \<and>
      t0 \<le> t0' \<and> t0' \<le> t1' \<and> t1' \<le> t1) xs"

lemma enclosure_ConsI:
  assumes "enclosure f t0 t1 ress0"
  assumes "f (fst (snd (snd r))) \<in> snd (snd (snd r))"
  assumes "\<And>t. t \<in> {fst r .. fst (snd (snd r))} \<Longrightarrow> f t \<in> fst (snd r)"
  assumes "t0 \<le> fst r" "fst r \<le> fst (snd (snd r))" "fst (snd (snd r)) \<le> t1"
  shows "enclosure f t0 t1 (r # ress0)"
  using assms by (auto simp: enclosure_def)

lemma enclosure_Nil_iff[simp]: "enclosure f t0 t1 [] \<longleftrightarrow> True" by (auto simp: enclosure_def)

lemma enclosure_Cons_iff:
  shows "enclosure f t0 t1 ((t0', CX, t1', X1) # ress0) \<longleftrightarrow>
    (f t1' \<in> X1 \<and> (\<forall>t\<in>{t0' .. t1'}. f t \<in> CX) \<and>
      t0 \<le> t0' \<and> t0' \<le> t1' \<and> t1' \<le> t1 \<and> enclosure f t0 t1 ress0)"
  using assms by (auto simp: enclosure_def)

lemma enclosure_subst:
  assumes "enclosure f t0 t1 ress"
  assumes "\<And>t. t \<in> {t0 .. t1} \<Longrightarrow> f t = g t"
  shows "enclosure g t0 t1 ress"
  using assms
  by (induct ress) (auto simp: enclosure_Cons_iff)

lemma enclosure_mono:
  assumes "t1 \<le> t2"
  assumes "enclosure f t0 t1 ress"
  shows "enclosure f t0 t2 ress"
  using assms
  by (induct ress) (auto simp: enclosure_Cons_iff)

text {* execution of @{term advance_euler} *}

lemma advance_euler_enclosure:
  assumes pos_prestep: "0 < stepsize optns"
  assumes pos_step: "t0 \<le> t1"
  assumes encl: "enclosure (\<lambda>t. flow x0 (t - t0)) t0 t1 (map set_res_of_appr_res xs)"
  assumes sol: "flow x0 (t1 - t0) \<in> set_of_appr X1"
  assumes ex_ivl: "t1 - t0 \<in> existence_ivl x0"
  assumes adv: "advance_euler optns (Some (i, t1, X1, xs)) = Some (j, t2, X2, ys)"
  shows "enclosure ((\<lambda>t. flow x0 (t - t0))) t0 t2 (map set_res_of_appr_res ys)" (is ?encl)
    and "flow x0 (t2 - t0) \<in> set_of_appr X2" (is ?sol)
    and "t2 - t0 \<in> existence_ivl x0" (is ?ex_ivl)
    and "t0 \<le> t2"
proof -
  from adv obtain CX err where step: "euler_step optns X1 = Some (t2 - t1, err, CX, X2)"
    and ys: "ys = (t1, CX, t2, X2)#xs"
    by (auto simp: split: option.split_asm)
  have "t1 + (t2 - t1) = t2" by simp
  note sol_step = unique_on_euler_step[OF sol pos_prestep this step]
  hence "t1 \<le> t2" by simp
  {
    fix t assume t: "t \<in> {t1 .. t2}"
    have "t - t1 \<in> existence_ivl (flow x0 (t1 - t0))"
      using t
      by (intro in_existence_between_zeroI[OF _ sol_step(4)]) auto
    from flow_trans[OF ex_ivl this] sol_step(2) t
    have "flow x0 (t - t0) \<in> set_of_appr CX" by simp
  } note * = this
  from sol_step(4) ex_ivl show ?ex_ivl
    by (metis (no_types, hide_lams) ab_group_add_class.add_diff_cancel_left add_diff_cancel
      diff_minus_eq_add existence_ivl_trans iso_tuple_UNIV_I minus_minus uminus_add_conv_diff)
  from sol_step(3) show sol: ?sol
    by (auto simp: flow_trans[symmetric, OF ex_ivl sol_step(4)])

  have "enclosure (\<lambda>t. flow x0 (t - t0)) t0 t2 (map set_res_of_appr_res xs)"
    by (auto intro!: enclosure_mono[OF `t1 \<le> t2`] enclosure_subst[OF encl])
  from this
  show ?encl "t0 \<le> t2"
    using sol_step `t0 \<le> t1` `t1 \<le> t2` encl sol *
    by (auto simp: ys enclosure_Cons_iff)
qed

lemma euler_series_enclosure:
  assumes pos_prestep: "0 < stepsize optns"
  assumes x0: "x0 \<in> set_of_appr X0"
  assumes euler_series_returns: "euler_series optns t0 X0 i = Some (j, t2, X2, ress)"
  shows
    "enclosure (\<lambda>t. flow x0 (t - t0)) t0 t2 (map set_res_of_appr_res ress)"
    "flow x0 (t2 - t0) \<in> set_of_appr X2"
    "t2 - t0 \<in> existence_ivl x0"
    "t0 \<le> t2"
  unfolding atomize_conj
  using x0 euler_series_returns
proof (induct i arbitrary: t0 ress t2 X2 j)
  case (Suc i)
  then obtain t1 X1 r1 j' where ser: "euler_series optns t0 X0 i = Some (j', t1, X1, r1)"
    by (cases "euler_series optns t0 X0 i") auto
  with Suc have adv: "advance_euler optns (Some (j', t1, X1, r1)) = Some (j, t2, X2, ress)"
    by simp
  from Suc.hyps[OF Suc.prems(1) ser]
  have IH: "t0 \<le> t1" "enclosure (\<lambda>t. c1_on_open.flow ode UNIV x0 (t - t0)) t0 t1 (map set_res_of_appr_res r1)"
   "c1_on_open.flow ode UNIV x0 (t1 - t0) \<in> set_of_appr X1"
   "t1 - t0 \<in> c1_on_open.existence_ivl ode UNIV x0"
    by simp_all
  from advance_euler_enclosure[OF pos_prestep IH adv]
  show ?case by auto
qed simp

end

lemma aform_val_inner_aform: "aform_val e (inner_aform x n) = aform_val e x \<bullet> n"
  by (auto simp: aform_val_def inner_aform_def algebra_simps)

sublocale aform_approximate_ivp0 \<subseteq>
  approximate_sets
    aform_of_ivl msum_aform' Affine Joints
    Inf_aform Sup_aform
    "uncurry_options add_aform_componentwise::('a, 'a::executable_euclidean_space aform, (real \<times> ((real \<times> 'a \<times> 'a \<times> real \<times> 'a \<times> 'a) list))) options \<Rightarrow> _"
    "uncurry_options scaleQ_aform_componentwise"
    "uncurry_options scaleR_aform_ivl"
    split_aform_largest
    support_aform
    aform_inf_inner
    aform_sup_inner
    inter_aform_plane
    reduce_aform
    independent_aform
    width_aform
proof
  fix x y::'a and X Y and xs ys::"'a list" and XS YS and r s S
    and optns::"('a, 'a aform, (real \<times> ((real \<times> 'a \<times> 'a \<times> real \<times> 'a \<times> 'a) list))) options"
  show "([x] \<in> Joints [X]) = (x \<in> Affine X)"
    by (auto simp: Affine_def valuate_def Joints_def)
  show "Affine X \<noteq> {}" by (rule Affine_notempty)
  show "compact (Affine X)" by (rule compact_Affine)
  {
    assume "x # y # xs \<in> Joints (X # Y # XS)"
    thus "y # x # xs \<in> Joints (Y # X # XS)" "y # xs @ [x] \<in> Joints (Y # XS @ [X])"
      by (auto simp: Joints_def valuate_def)
  }
  {
    assume "xs \<in> Joints []"
    thus "xs = []" by (auto simp: Joints_def valuate_def)
  }
  {
    assume "xs \<in> Joints (X # XS)"
    thus "\<exists>y ys. xs = y # ys \<and> y \<in> Affine X \<and> ys \<in> Joints XS"
      by (auto simp: Joints_def Affine_def valuate_def)
  }
  {
    assume "[x, y] \<in> Joints [X, Y]"
    thus "(x, y) \<in> Pair_of_list ` Joints [X, Y]"
      by (auto simp: Joints_def valuate_def intro!: image_eqI[where x="[aform_val e X, aform_val e Y]" for e])
  }
  {
    assume "uncurry_options add_aform_componentwise optns X Y YS = Some S" "x # y # ys \<in> Joints (X # Y # YS)"
    from add_aform_componentwise[OF this]
    show "(x + y) # x # y # ys \<in> Joints (S # X # Y # YS)" .
  }
  {
    assume "uncurry_options scaleQ_aform_componentwise optns r s X XS = Some S" "x # xs \<in> Joints (X # XS)"
    from scaleQ_aform_componentwise[OF this]
    show "(r/s) *\<^sub>R x # x # xs \<in> Joints (S # X # XS)" .
  }
  {
    fix s t::real
    assume "uncurry_options scaleR_aform_ivl optns r t X XS = Some S" "x # xs \<in> Joints (X # XS)"
      "s \<in> {r .. t}"
    from scaleR_aform_ivl[OF this]
    show "s *\<^sub>R x # x # xs \<in> Joints (S # X # XS)" .
  }
  {
    assume "x \<in> Affine X"
    then obtain e where e: "e \<in> funcset UNIV {-1 .. 1}" "x = aform_val e X"
      by (auto simp: Affine_def valuate_def)
    let ?sum = "summarize_threshold (precision optns) (presplit_summary_tolerance optns) (degree_aform X) (snd X)"
    obtain e' where e': "e' \<in> funcset UNIV {-1 .. 1}"
      "aform_val e' (fst X, ?sum) = aform_val e X"
      by (rule summarize_pdevsE[OF e(1) order_refl, of "snd X" "precision optns"
          "(\<lambda>i y. presplit_summary_tolerance optns * infnorm (eucl_truncate_up (precision optns) (Radius' (precision optns) X)) \<le> infnorm y)"])
        (auto simp: summarize_threshold_def aform_val_def)
    from e e' have x: "x = aform_val e' (fst X, ?sum)"
      by simp
    show "list_ex (\<lambda>X. x \<in> Affine X) (split_aform_largest optns X)"
    proof (rule split_aformE[OF e'(1) x, where i="fst (max_pdev ?sum)"])
      fix err::real
      assume "err \<in> {-1 .. 1}" "x = aform_val (e'(fst (max_pdev ?sum) := err))
          (fst (split_aform (fst X, ?sum) (fst (max_pdev ?sum))))"
      thus "list_ex (\<lambda>X. x \<in> Affine X) (split_aform_largest optns X)"
        using e'(1)
        by (force simp: split_aform_largest_def split_aform_largest_uncond_def Affine_def valuate_def
          intro!: image_eqI[where x="e' (a := err)" for a] split: prod.split)
    next
      fix err::real
      assume "err \<in> {-1 .. 1}" "x = aform_val (e'(fst (max_pdev ?sum) := err))
          (snd (split_aform (fst X, ?sum) (fst (max_pdev ?sum))))"
      thus "list_ex (\<lambda>X. x \<in> Affine X) (split_aform_largest optns X)"
        using e'(1)
        by (force simp: split_aform_largest_def split_aform_largest_uncond_def Affine_def valuate_def
          intro: image_eqI[where x="e' (a := err)" for a err]
          split: prod.split)
    qed
  }
  show "Affine (msum_aform' X Y) = {x + y |x y. x \<in> Affine X \<and> y \<in> Affine Y}"
    by (rule Affine_msum_aform) simp
  show "Inf_aform (msum_aform' X Y) = Inf_aform X + Inf_aform Y"
    "Sup_aform (msum_aform' X Y) = Sup_aform X + Sup_aform Y"
    by (auto simp: Inf_aform_msum_aform Sup_aform_msum_aform)
  show "Inf_aform X \<le> Inf (Affine X)" "Sup (Affine X) \<le> Sup_aform X"
    by (auto simp: Affine_def valuate_def Inf_aform Sup_aform intro!: cINF_greatest cSUP_least)
  {
    fix l u::'a assume le: "l \<le> u"
    show "Sup_aform (aform_of_ivl l u) = u"
     "Inf_aform (aform_of_ivl l u) = l"
     "Affine (aform_of_ivl l u) = {l..u}"
     using Inf_aform_aform_of_ivl[OF le] Sup_aform_aform_of_ivl[OF le]
       Affine_aform_of_ivl[OF le]
     by auto
  }
  show "convex (Affine X)"
    by (rule convex_Affine)
  show "Affine X \<subseteq> Affine (reduce_aform optns X)"
  proof (auto simp: reduce_aform_def summarize_threshold_def[abs_def] Affine_def valuate_def
    aform_val_def)
    case goal1
    from summarize_pdevsE[OF `e \<in> _` order_refl, of "snd X" "precision optns"
      "(\<lambda>(i::nat) y. presplit_summary_tolerance optns * infnorm (eucl_truncate_up (precision optns)
      (tdev' (precision optns) (snd X))) \<le> infnorm y)"]
    guess e' .
    thus ?case
      by (auto intro!: image_eqI[where x=e'])
  qed
  {
    fix sctn
    assume "inter_aform_plane optns X sctn = Some Y"
    thus "Affine X \<inter> plane_of sctn \<subseteq> Affine Y"
      by (auto simp: inter_aform_plane_def plane_of_def dest!: inter_inter_aform_plane_ortho)
  }
  {
    assume x: "x \<in> Affine X"
    thus "aform_inf_inner optns X y \<le> x \<bullet> y"
      "x \<bullet> y \<le> aform_sup_inner optns X y"
      by (auto simp: aform_inf_inner_def aform_sup_inner_def
        Affine_def valuate_def aform_val_inner_aform
        dest: Inf_aform[where X="inner_aform X y"]
        Sup_aform[where X="inner_aform X y"]
        intro!: order_trans[OF Inf_aform'] order_trans[OF _ Sup_aform'])
  }
  show "xs \<in> Joints XS \<Longrightarrow> length xs = length XS" by (auto simp: Joints_def valuate_def)
  show "\<And>z Z. [x, y, z] \<in> Joints [X, Y, Z] \<Longrightarrow> (x, y, z) \<in> Triple_of_list ` Joints [X, Y, Z]"
    by (rule_tac x = "[x, y, z]" in image_eqI) auto
  show "x \<in> Affine X \<Longrightarrow> y \<in> Affine Y \<Longrightarrow> [x, y] \<in> Joints [X, independent_aform X Y]"
    by (rule independent_aform_Joints)
  show "Affine (independent_aform X Y) = Affine Y"
    by (rule Affine_independent_aform)
  show "xs \<in> Joints XS \<longrightarrow> length xs = length XS \<longrightarrow> length ys = length YS \<longrightarrow>
    set (zip ys YS) \<subseteq> set (zip xs XS) \<longrightarrow> ys \<in> Joints YS"
    by safe (rule Joints_set_zip_subset)
qed

locale aform_approximate_ivp = aform_approximate_ivp0 +
  approximate_ivp
    aform_of_ivl msum_aform' Affine Joints
    Inf_aform Sup_aform
    "uncurry_options add_aform_componentwise::('a, 'a::executable_euclidean_space aform, (real \<times> ((real \<times> 'a \<times> 'a \<times> real \<times> 'a \<times> 'a) list))) options \<Rightarrow> _"
    "uncurry_options scaleQ_aform_componentwise"
    "uncurry_options scaleR_aform_ivl"
    split_aform_largest
    support_aform
    aform_inf_inner
    aform_sup_inner
    inter_aform_plane
    reduce_aform
    independent_aform
    width_aform
begin

text {* TODO: prove these lemmas generically *}

lemma ivls_of_aforms:
  assumes "enclosure f t0 t1 (map set_res_of_appr_res xs)"
  shows "enclosure f t0 t1 (map set_res_of_ivl_res (ivls_of_aforms p xs))"
  using assms
proof (induct xs)
  case (Cons x xs)
  thus ?case
    by (cases x) (auto simp: ivls_of_aforms_def o_def enclosure_Cons_iff
      intro: inf_of_appr eucl_truncate_down_le sup_of_appr eucl_truncate_up_le)
qed (simp add: ivls_of_aforms_def)

lemma summarize_ivls:
  fixes f::"real \<Rightarrow> 'a"
  assumes "enclosure f t0 t1 (map set_res_of_ivl_res xs)"
  shows "enclosure f t0 t1 (case summarize_ivls xs of Some x \<Rightarrow> [set_res_of_ivl_res x] | None \<Rightarrow> [])"
  using assms
proof (induct xs)
  case Nil
  thus ?case by simp
next
  case (Cons x xs)
  have inf_cases: "\<And>t t0 t1 t2 a b.
    \<forall>t\<in>{t1..t2}. a \<le> f t \<Longrightarrow>
    \<forall>t\<in>{t0..t1}. b \<le> f t \<Longrightarrow>
    t0 \<le> t \<Longrightarrow> t \<le> t2 \<Longrightarrow>
    inf a b \<le> f t"
    by (metis atLeastAtMost_iff le_cases le_infI1 le_infI2)
  have sup_cases: "\<And>t t0 t1 t2 a b.
       \<forall>t\<in>{t1..t2}. f t \<le> a \<Longrightarrow>
       \<forall>t\<in>{t0..t1}. f t \<le> b \<Longrightarrow>
       t0 \<le> t \<Longrightarrow> t \<le> t2 \<Longrightarrow>
       f t \<le> sup a b"
    by (metis atLeastAtMost_iff le_cases le_supI1 le_supI2)
  show ?case
    using Cons
    by (cases x) (fastforce simp: min_def max_def enclosure_Cons_iff
      split: split_if_asm option.split
      intro: inf_cases sup_cases inf.coboundedI1 inf.coboundedI2 le_infI2 le_supI1 le_supI2
        sup.coboundedI1 sup.coboundedI2)
qed

lemma enclosure_takeD:
  assumes "enclosure f t0 t1 (map set_res_of_ivl_res xs)"
  shows "enclosure f t0 t1 (map set_res_of_ivl_res (take m xs))"
using assms
proof (induct xs arbitrary: m)
  case (Cons x xs)
  thus ?case
    by (cases m) (auto simp: enclosure_def)
qed simp

lemma enclosure_dropD:
  assumes "enclosure f t0 t1 (map set_res_of_ivl_res xs)"
  shows "enclosure f t0 t1 (map set_res_of_ivl_res (drop m xs))"
using assms
proof (induct xs arbitrary: m)
  case (Cons x xs)
  thus ?case
    by (cases m) (auto simp: enclosure_def)
qed simp

lemma summarize_option_map_filter_aux: "(case f xs of None \<Rightarrow> [] | Some x \<Rightarrow> [set_res_of_ivl_res x]) =
     (map set_res_of_ivl_res (map the (filter (- Option.is_none) (map f [xs]))))"
   by (auto split: option.split simp: is_none_def)

lemma enclosure_Cons_splitI:
  "enclosure f t0 t1 (map set_res_of_ivl_res (map the (filter (- Option.is_none) ([X])))) \<Longrightarrow>
  enclosure f t0 t1 (map set_res_of_ivl_res (map the (filter (- Option.is_none) ((Xs))))) \<Longrightarrow>
  enclosure f t0 t1 (map set_res_of_ivl_res (map the (filter (- Option.is_none) ((X # Xs)))))"
  by (case_tac "set_res_of_ivl_res (the X)") (auto simp: enclosure_Cons_iff)

lemma summarize_enclosure_aux:
  fixes f::"real \<Rightarrow> 'a"
  assumes "enclosure f t0 t1 (map set_res_of_ivl_res xs)"
  shows "enclosure f t0 t1 (map set_res_of_ivl_res (map the (filter (-Option.is_none) (map summarize_ivls (parts m xs)))))"
  using assms
proof (induct m xs rule: parts.induct)
  case 1 thus ?case by simp
next
  case (2 x xs)
  from summarize_ivls[OF 2]
  show ?case unfolding parts.simps summarize_option_map_filter_aux .
next
  case (3 m x xs)
  have "enclosure f t0 t1 (map set_res_of_ivl_res (map the (filter (- Option.is_none) [summarize_ivls (take (Suc m) (x # xs))])))"
    using summarize_ivls summarize_option_map_filter_aux[symmetric,
        of summarize_ivls "(take (Suc m) (x # xs))", simplified list.map]
    by (metis "3.prems" enclosure_takeD)
  moreover
  from 3 have "enclosure f t0 t1
     (map set_res_of_ivl_res (map the (filter (- Option.is_none) (map summarize_ivls (parts (Suc m) (drop (Suc m) (x # xs)))))))"
     by (metis enclosure_dropD)
  ultimately
  show ?case
    unfolding parts.simps list.map
    by (rule enclosure_Cons_splitI)
qed

lemma
  summarize_enclosure:
  "enclosure f t0 t1 (map set_res_of_appr_res xs) \<Longrightarrow>
    enclosure f t0 t1 (map set_res_of_ivl_res (summarize_enclosure p m xs))"
  unfolding summarize_enclosure_def
  by (intro summarize_enclosure_aux ivls_of_aforms)

lemma euler_series_ivls_result:
  assumes pos_prestep: "0 < stepsize optns"
  assumes x0: "x0 \<in> Affine X0"
  assumes ivls_result: "result_fun optns = ivls_result p m"
  assumes euler_series_returns: "euler_series_result optns t0 X0 i = Some (t1, xs)"
  shows
    "enclosure (\<lambda>t. flow x0 (t - t0)) t0 t1 (map set_res_of_ivl_res xs)" (is ?th1)
    "t1 - t0 \<in> existence_ivl x0" (is ?th2)
proof -
  from euler_series_returns obtain j X1 ress
    where ress: "euler_series optns t0 X0 i = Some (j, t1, X1, ress)"
    and xs: "xs = summarize_enclosure p m ress"
    by (auto simp: ivls_result ivls_result_def)
  from euler_series_enclosure[OF assms(1-2) ress]
  show ?th1 ?th2
    by (auto intro!: summarize_enclosure simp: xs)
qed

end

end

