Theory Init_ODE_Solver

theory Init_ODE_Solver
imports
  Concrete_Reachability_Analysis_C1
  Refine_Reachability_Analysis_C1
  Refine_Rigorous_Numerics_Aform
begin

subsection ‹``Final'' Theorems, stated outside of refinement framework.›

lemma br_Times_Univ: "br a I ×r (UNIV::(_ × unit) set) = br (λ(x, _). (a x, ())) (λ(x, _). I x)"
  by (auto simp: br_def)

lemma TRANSFER_refl: "TRANSFER (x ≤ (x::_nres))" by auto
lemma init_ode_ops: "(y ⟹ x) ⟹ (init_ode_ops x y odo, odo) ∈ ode_ops_rel"
  by (auto simp: ode_ops_rel_def init_ode_ops_def)

context approximate_sets begin

context includes autoref_syntax begin

theorem solves_poincare_map_ncc:
  fixes sctni pos ivli ssc XS ph rl ru dRi CXS X0 S trap
  defines "P ≡ set_of_lvivl ivli ∩ plane_of (map_sctn eucl_of_list sctni)"
  defines "Sa ≡ below_halfspace (map_sctn eucl_of_list S)::'n::enum rvec set"
  defines "X0 ≡ c1_info_of_apprse XS"
  defines "X1 ≡ flow1_of_vec1 ` ({eucl_of_list rl .. eucl_of_list ru} × set_of_lvivl' dRi)"
  assumes ncc: "ncc_precond TYPE('n rvec)" "ncc_precond TYPE('n vec1)"
  assumes ret: "solves_poincare_map odo symstart [S] guards ivli sctni roi XS (rl, ru) dRi"
  assumes symstart: "(symstart, symstarta::'n eucl1 set ⇒ ('n rvec set × 'n eucl1 set)nres) ∈ appr1e_rel → ⟨clw_rel appr_rel ×r clw_rel appr1e_rel⟩dres_nres_rel"
  assumes symstart_spec: "⋀X0. X0 ⊆ Csafe odo × UNIV ⟹ symstarta X0 ≤ SPEC (λ(CX, X). flowsto odo (X0 - trap × UNIV) {0..} (CX × UNIV) (X))"
  assumes trapprop: "stable_on odo (Csafe odo - P) trap"
  assumes invar: "⋀X. X ∈ set XS ⟹ c1_info_invare CARD('n) X"
  assumes lens: "length (ode_e odo) = CARD('n)" "length (normal sctni) = CARD('n)" "length (fst ivli) = CARD('n)" "length (snd ivli) = CARD('n)"
    "length (normal S) = CARD('n)" "length rl = CARD('n)" "length ru = CARD('n)"
     "lvivl'_invar (CARD('n)*CARD('n)) dRi"
    "⋀a xs b ba ro. (xs, ro) ∈ set guards ⟹ ((a, b), ba) ∈ set xs ⟹ length a = CARD('n) ∧ length b = CARD('n) ∧ length (normal ba) = CARD('n)"
  shows "poincare_mapsto odo P (X0 - trap × UNIV) Sa (Csafe odo - P) X1"
proof -
  define guardsa::"('n rvec set × unit) list"  where "guardsa ≡ map (λ(x, y). (⋃x∈set x. case x of (x, y) ⇒ (case x of (x, y) ⇒ set_of_ivl (eucl_of_list x, eucl_of_list y)) ∩ plane_of (map_sctn eucl_of_list y), ())) guards"
  define roa where "roa = ()"
  have spm:
    "(XS, X0) ∈ clw_rel (appr1e_rel)"
    "([S], Sa) ∈ ⟨lv_rel⟩halfspaces_rel"
    "(guards, guardsa) ∈ ⟨clw_rel (iplane_rel lvivl_rel) ×r reach_optns_rel⟩list_rel"
    "(ivli, set_of_lvivl ivli::'n rvec set) ∈ lvivl_rel"
    "(sctni, map_sctn eucl_of_list sctni::'n rvec sctn) ∈ ⟨lv_rel⟩sctn_rel"
    "(roi, roa) ∈ reach_optns_rel"
    "(λx. nres_of (symstart x), symstarta) ∈ appr1e_rel → ⟨clw_rel appr_rel ×r clw_rel appr1e_rel⟩nres_rel"
    "((), trap) ∈ ghost_rel"
    using lens symstart[THEN dres_nres_rel_nres_relD]
    by (auto simp: X0_def X1_def Sa_def P_def appr_rel_br set_rel_br
        br_chain o_def clw_rel_br  lv_rel_def sctn_rel_br ivl_rel_br set_of_lvivl_def
        halfspaces_rel_def list_set_rel_brp below_halfspaces_def ghost_relI
        br_rel_prod br_list_rel guardsa_def Id_br inter_rel_br plane_rel_br
        roa_def br_Times_Univ reach_options_rel_def
        split: sctn.splits
        intro!: brI list_allI clw_rel_appr1e_relI assms)

  have ivls: "((rl, ru), {eucl_of_list rl .. eucl_of_list ru::'n rvec}) ∈ lvivl_rel"
    "(dRi, set_of_lvivl' dRi::(('n rvec), 'n) vec set) ∈ ⟨lvivl_rel⟩default_rel UNIV"
    by (auto intro!: lvivl_relI lvivl_default_relI lens simp: lens set_of_lvivl_def set_of_ivl_def
        split: option.splits)

  from lens(1) have wd: "wd odo TYPE('n rvec)" by (auto simp: wd_def)
  from lens(1) have DIM_precond: "DIM_precond TYPE('n rvec) (D odo)"
    by (auto simp: D_def)
  have pmspec: "poincare_onto_from_in_ivl $ odo $ symstarta $ trap $ S $ guards $ ivl $ sctn $ ro $ XS0 $ IVL $ dIVL
  ≤ SPEC (λb. b ⟶ poincare_mapsto odo (ivl ∩ plane_of sctn) (XS0 - trap × UNIV) S (Csafe odo - ivl ∩ plane_of sctn)
                      (flow1_of_vec1 ` (IVL × dIVL)))"
    if trapprop: "stable_on odo (Csafe odo - ivl ∩ plane_of sctn) trap"
    for ivl sctn XS0 S guards ro IVL dIVL
    using poincare_onto_from_in_ivl[OF wd symstart_spec trapprop order_refl,
        of S guards ro XS0 IVL dIVL]
    by auto

  have odo_init: "(init_ode_ops True (carries_c1 (hd XS)) odo, odo) ∈ ode_ops_rel"
    by (auto simp: intro!: init_ode_ops)
  from nres_rel_trans2[OF
      pmspec
      poincare_onto_from_in_ivl_impl.refine[OF DIM_precond ncc odo_init spm(1-7) TRANSFER_refl spm(8) ivls]
      ] ret trapprop
  show ?thesis
    by (auto simp: solves_poincare_map_def nres_rel_def P_def X1_def)
qed

lemma solves_poincare_map'_ncc:
  "ncc_precond TYPE('n::enum rvec) ⟹
  ncc_precond TYPE('n vec1) ⟹
  solves_poincare_map' odo S guards ivli sctni roi XS (rl, ru) dRi ⟹
  (⋀X. X ∈ set XS ⟹ c1_info_invare CARD('n) X) ⟹
  length (ode_e odo) = CARD('n) ⟹
  length (normal sctni) = CARD('n) ⟹
  length (fst ivli) = CARD('n) ⟹
  length (snd ivli) = CARD('n) ⟹
  length (normal S) = CARD('n) ⟹
  length (rl) = CARD('n) ⟹
  length (ru) = CARD('n) ⟹
  lvivl'_invar (CARD('n)*CARD('n)) dRi ⟹
  (⋀a xs b ba ro.
      (xs, ro) ∈ set guards ⟹
      ((a, b), ba) ∈ set xs ⟹
      length a = CARD('n) ∧
      length b = CARD('n) ∧ length (normal ba) = CARD('n)) ⟹
  poincare_mapsto odo
   (set_of_lvivl ivli ∩ plane_of (map_sctn eucl_of_list sctni)::'n rvec set)
   (c1_info_of_apprse XS) (below_halfspace (map_sctn eucl_of_list S))
   (Csafe odo - set_of_lvivl ivli ∩ plane_of (map_sctn eucl_of_list sctni))
   (flow1_of_vec1 ` ({eucl_of_list rl .. eucl_of_list ru} × set_of_lvivl' dRi))"
  by (rule solves_poincare_map_ncc[OF _ _ _
        empty_symstart_dres_nres_rel[unfolded empty_symstart_def op_empty_coll_def mk_coll_def]
         empty_symstart_flowsto,
    folded solves_poincare_map'_def, simplified])
    auto


lemma one_step_until_time_ivl_in_ivl_spec[le, refine_vcg]:
  "one_step_until_time_ivl_in_ivl odo (X0::'n::enum eucl1 set) t1 t2 R dR ≤ SPEC (λb. b ⟶
    (∀(x0, d0) ∈ X0. {t1 .. t2} ⊆ existence_ivl0 odo x0 ∧
      (∀t ∈ {t1 .. t2}. (flow0 odo x0 t, Dflow odo x0 t oL d0) ∈ flow1_of_vec1 ` (R × dR))))"
  if [simp]: "length (ode_e odo) = CARD('n::enum)"
proof -
  have wd[refine_vcg]: "wd odo TYPE((real, 'n) vec)" by (simp add: wd_def)
  show ?thesis
    unfolding one_step_until_time_ivl_in_ivl_def
    apply (refine_vcg, clarsimp_all)
    subgoal for X CX Y CY CY' x0 d0
        apply (drule bspec, assumption, clarsimp)
      subgoal for t
          apply (drule bspec[where x=t], force)
        by (simp add: subset_iff )
      done
    done
qed

theorem one_step_in_ivl_ncc:
  "t ∈ existence_ivl0 odo x0 ∧ (flow0 odo x0 t::'n rvec) ∈ R ∧ Dflow odo x0 t oL d0 ∈ dR"
  if ncc: "ncc_precond TYPE('n::enum rvec)" "ncc_precond TYPE('n vec1)"
   and t: "t ∈ {t0 .. t1}"
   and x0: "(x0, d0) ∈ c1_info_of_appre X"
   and invar: "c1_info_invare CARD('n) X"
   and R: "{eucl_of_list rl .. eucl_of_list ru} ⊆ R"
   and lens: "length rl = CARD('n)" "length ru = CARD('n)"
   and dRinvar: "lvivl'_invar (CARD('n)*CARD('n)) dRi"
   and dR: "blinfun_of_vmatrix ` set_of_lvivl' dRi ⊆ dR"
   and len_ode: "length (ode_e odo) = CARD('n)"
   and chk: "one_step_until_time_ivl_in_ivl_check odo X t0 t1 (rl, ru) dRi"
proof -
  have ivl: "((rl, ru), {eucl_of_list rl .. eucl_of_list ru::'n rvec}) ∈ ⟨lv_rel⟩ivl_rel"
    apply (rule lv_relivl_relI)
    using lens
    by auto
  from dRinvar have "lvivl'_invar DIM(((real, 'n) vec, 'n) vec) dRi" by simp
  note dRi = lvivl_default_relI[OF this]
  from len_ode have DIM_precond: "DIM_precond TYPE('n rvec) (D odo)"
    by (auto simp: D_def)
  have odo: "(init_ode_ops True (carries_c1 X) odo, odo) ∈ ode_ops_rel"
    by (auto intro!: init_ode_ops)
  from one_step_until_time_ivl_in_ivl_impl_refine[param_fo, OF DIM_precond ncc odo appr1e_relI[OF invar] IdI IdI ivl dRi, of t0 t1]
  have "nres_of (one_step_until_time_ivl_in_ivl_impl (D odo) (init_ode_ops True (carries_c1 X) odo) X t0 t1 (rl, ru) dRi)
    ≤ one_step_until_time_ivl_in_ivl odo (c1_info_of_appre X) t0 t1 {eucl_of_list rl::'n rvec..eucl_of_list ru} (set_of_lvivl' dRi)"
    by (auto simp: nres_rel_def)
  also note one_step_until_time_ivl_in_ivl_spec[OF len_ode order_refl]
  also have "one_step_until_time_ivl_in_ivl_impl (D odo) (init_ode_ops True (carries_c1 X) odo) X t0 t1 (rl, ru) dRi = dRETURN True"
    unfolding one_step_until_time_ivl_in_ivl_check_def[symmetric]
    using chk .
  finally show ?thesis
    using t R dR
    by (auto dest!: bspec[OF _ x0] bspec[where x=t] simp: vec1_of_flow1_def)
qed

subsection ‹Poincare onto (from the outside)›

theorem solves_poincare_map_onto_ncc:
  fixes sctni pos ivli ssc XS ph rl ru dRi CXS X0
  defines "P ≡ set_of_lvivl ivli ∩ plane_of (map_sctn eucl_of_list sctni)"
  defines "X0 ≡ c1_info_of_apprse XS"
  defines "X1 ≡ flow1_of_vec1 ` ({eucl_of_list rl .. eucl_of_list ru} × set_of_lvivl' dRi)"
  assumes ncc: "ncc_precond TYPE('n::enum rvec)" "ncc_precond TYPE('n vec1)"
  assumes ret: "solves_poincare_map_onto odo guards ivli sctni roi XS (rl, ru) dRi"
  assumes invar: "⋀X. X ∈ set XS ⟹ c1_info_invare CARD('n) X"
  assumes lens: "length (ode_e odo) = CARD('n)" "length (normal sctni) = CARD('n)" "length (fst ivli) = CARD('n)" "length (snd ivli) = CARD('n)"
    "length rl = CARD('n)" "length ru = CARD('n)"
     "lvivl'_invar (CARD('n)*CARD('n)) dRi"
    "⋀a xs b ba ro. (xs, ro) ∈ set guards ⟹ ((a, b), ba) ∈ set xs ⟹ length a = CARD('n) ∧ length b = CARD('n) ∧ length (normal ba) = CARD('n)"
  shows "poincare_maps_onto odo P (X0::('n rvec × _)set) X1"
proof -
  define guardsa::"('n rvec set × unit) list"  where "guardsa ≡ map (λ(x, y). (⋃x∈set x. case x of (x, y) ⇒ (case x of (x, y) ⇒ set_of_ivl (eucl_of_list x, eucl_of_list y)) ∩ plane_of (map_sctn eucl_of_list y), ())) guards"
  define roa where "roa = ()"
  have spm:
    "(XS, X0) ∈ clw_rel (appr1e_rel)"
    "(guards, guardsa) ∈ ⟨clw_rel (iplane_rel lvivl_rel) ×r reach_optns_rel⟩list_rel"
    "(ivli, set_of_lvivl ivli::'n rvec set) ∈ lvivl_rel"
    "(sctni, map_sctn eucl_of_list sctni::'n rvec sctn) ∈ ⟨lv_rel⟩sctn_rel"
    "(roi, roa) ∈ reach_optns_rel"
    using lens
    by (auto simp: X0_def X1_def P_def appr_rel_br set_rel_br
        br_chain o_def clw_rel_br  lv_rel_def sctn_rel_br ivl_rel_br set_of_lvivl_def
        halfspaces_rel_def list_set_rel_brp below_halfspaces_def ghost_relI
        br_rel_prod br_list_rel guardsa_def Id_br inter_rel_br plane_rel_br
        reach_options_rel_def br_Times_Univ
        split: sctn.splits
        intro!: brI list_allI clw_rel_appr1e_relI assms)

  have ivls: "((rl, ru), {eucl_of_list rl .. eucl_of_list ru::'n rvec}) ∈ lvivl_rel"
    "(dRi, set_of_lvivl' dRi::(('n rvec), 'n) vec set) ∈ ⟨lvivl_rel⟩default_rel UNIV"
    by (auto intro!: lvivl_relI lvivl_default_relI lens simp: lens set_of_lvivl_def set_of_ivl_def
        split: option.splits)

  have pmspec: "poincare_onto_in_ivl odo guards ivl sctn ro XS0 IVL dIVL
  ≤ SPEC (λb. b ⟶ poincare_mapsto odo (ivl ∩ plane_of sctn) (XS0) UNIV (Csafe odo - ivl ∩ plane_of sctn)
                      (flow1_of_vec1 ` (IVL × dIVL)))"
    for ivl::"'n rvec set" and sctn XS0 guards ro IVL dIVL
    using poincare_onto_in_ivl[OF lens(1) order_refl, of guards ivl sctn ro XS0 IVL dIVL]
    by auto
  from lens(1) have DIM_precond: "DIM_precond TYPE('n rvec) (D odo)"
    by (auto simp: D_def)
  have odo: "(init_ode_ops True (carries_c1 (hd XS)) odo, odo) ∈ ode_ops_rel"
    by (auto intro!: init_ode_ops)
  from nres_rel_trans2[OF
      pmspec
      poincare_onto_in_ivl_impl.refine[OF DIM_precond ncc odo spm(1-5) ivls]
      ] ret
  show ?thesis
    by (auto simp: poincare_maps_onto_def solves_poincare_map_onto_def nres_rel_def P_def X1_def)
qed

end
end

subsection ‹Executable definitions for ODE solver based on affine arithmetic›

global_interpretation aform: approximate_sets aform_ops Joints aforms_rel optns for optns
  defines solves_poincare_map_aform = aform.solves_poincare_map
    and solves_poincare_map_aform' = aform.solves_poincare_map'
    and solves_poincare_map_onto_aform = aform.solves_poincare_map_onto
    and solves_one_step_until_time_aform = aform.one_step_until_time_ivl_in_ivl_check
    and solve_poincare_map_aform = aform.poincare_onto_from_impl
    and one_step_until_time_ivl_in_ivl_impl_aform = aform.one_step_until_time_ivl_in_ivl_impl
    and poincare_onto_from_in_ivl_impl_aform = aform.poincare_onto_from_in_ivl_impl
    and poincare_onto_in_ivl_impl_aform = aform.poincare_onto_in_ivl_impl
    and solve_poincare_onto_aform = aform.poincare_onto_impl
    and solve_one_step_until_time_aform = aform.one_step_until_time_ivl
    and one_step_until_time_impl_aform = aform.one_step_until_time_impl
    and op_image_fst_coll_nres_impl_aform = aform.op_image_fst_coll_nres_impl
    and poincare_onto_series_impl_aform = aform.poincare_onto_series_impl
    and poincare_start_on_impl_aform = aform.poincare_start_on_impl
    and leaves_halfspace_impl_aform = aform.leaves_halfspace_impl
    and approximate_sets_aform = aform.subset_spec_ivl_collc
    and subset_spec_plane_impl_aform = aform.subset_spec_plane_impl
    and disjoints_spec_impl_aform = aform.disjoints_spec_impl
    and partition_set_impl_aform = aform.partition_set_impl
    and fst_safe_coll_impl_aform = aform.fst_safe_coll_impl
    and choose_step1_impl_aform = aform.choose_step1_impl
    and ivl_rep_of_set_coll_impl_aform = aform.ivl_rep_of_set_coll_impl
    and ode_set_impl_aform = aform.ode_set_impl
    and mk_safe_impl_aform = aform.mk_safe_impl
    and subset_spec_ivlc_aform = aform.subset_spec_ivlc
    and sbelow_sctn_impl_aform = aform.sbelow_sctn_impl
    and below_sctn_impl_aform = aform.below_sctn_impl
    and split_under_threshold_impl_aform = aform.split_under_threshold_impl
    and do_intersection_coll_impl_aform = aform.do_intersection_coll_impl
    and partition_ivl_impl_aform = aform.partition_ivl_impl
    and mk_safe_coll_impl_aform = aform.mk_safe_coll_impl
    and choose_step_impl_aform = aform.choose_step_impl
    and reach_cont_impl_aform = aform.reach_cont_impl
    and vec1reps_impl_aform = aform.vec1reps_impl
    and ivl_rep_of_sets_impl_aform = aform.ivl_rep_of_sets_impl
    and ivl_rep_of_set_impl_aform = aform.ivl_rep_of_set_impl
    and ivls_of_sets_impl_aform = aform.ivls_of_sets_impl
    and tolerate_error_impl_aform = aform.tolerate_error_impl
    and tolerate_error1_impl_aform = aform.tolerate_error1_impl
    and pre_intersection_step_impl_aform = aform.pre_intersection_step_impl
    and split_spec_param1_impl_aform = aform.split_spec_param1_impl
    and do_intersection_impl_aform = aform.do_intersection_impl
    and resolve_step_impl_aform = aform.resolve_step_impl
    and euler_step_impl_aform = aform.euler_step_impl
    and rk2_step_impl_aform = aform.rk2_step_impl
    and op_eventually_within_sctn_impl_aform = aform.op_eventually_within_sctn_impl
    and solve_poincare_plane_impl_aform = aform.solve_poincare_plane_impl
    and cert_stepsize_impl_dres_aform = aform.cert_stepsize_impl_dres
    and step_adapt_time_impl_aform = aform.step_adapt_time_impl
    and inter_sctn1_impl_aform = aform.inter_sctn1_impl
    and step_split_impl_aform = aform.step_split_impl
    and intersects_impl_aform = aform.intersects_impl
    and above_sctn_impl_aform = aform.above_sctn_impl
    and nonzero_component_impl_aform = aform.nonzero_component_impl
    and P_iter_impl_aform = aform.P_iter_impl
    and partition_sets_impl_aform = aform.partition_sets_impl
    and reach_conts_impl_aform = aform.reach_conts_impl
    and subsets_iplane_coll_impl_aform = aform.subsets_iplane_coll_impl
    and reach_cont_symstart_impl_aform = aform.reach_cont_symstart_impl
    and subset_iplane_coll_impl_aform = aform.subset_iplane_coll_impl
    and symstart_coll_impl_aform = aform.symstart_coll_impl
    and subset_spec_ivls_clw_impl_aform = aform.subset_spec_ivls_clw_impl
    and poincare_onto2_impl_aform = aform.poincare_onto2_impl
    and poincare_onto_empty_impl_aform = aform.poincare_onto_empty_impl
    and resolve_ivlplanes_impl_aform = aform.resolve_ivlplanes_impl
    and empty_remainders_impl_aform = aform.empty_remainders_impl
    and adapt_stepsize_fa_aform = aform.adapt_stepsize_fa
    and split_spec_param1e_impl_aform = aform.split_spec_param1e_impl
    and setse_of_ivlse_impl_aform = aform.setse_of_ivlse_impl
    and ivlse_of_setse_impl_aform = aform.ivlse_of_setse_impl
    and choose_step1e_impl_aform = aform.choose_step1e_impl
    and vec1repse_impl_aform = aform.vec1repse_impl
    and scaleR2_rep1_impl_aform = aform.scaleR2_rep1_impl
    and list_of_appr1e_aform = aform.list_of_appr1e
    and list_of_appr1_aform = aform.list_of_appr1
    and nonzero_component_within_impl_aform = aform.nonzero_component_within_impl
    and approx_fas_impl_aform = aform.approx_slp_appr_impl
    and mig_set_impl_aform = aform.mig_set_impl
    and op_eucl_of_list_image_pad_aform = aform.op_eucl_of_list_image_pad
    and reach_cont_par_impl_aform = aform.reach_cont_par_impl
    and do_intersection_core_impl_aform = aform.do_intersection_core_impl
    and reduce_spec1e_impl_aform = aform.reduce_spec1e_impl
    and reduce_spec1_impl_aform = aform.reduce_spec1_impl
    and one_step_until_time_ivl_impl_aform = aform.one_step_until_time_ivl_impl
    and subset_spec1_collc_aform = aform.subset_spec1_collc
    and ivl_of_appr1_coll_impl_aform = aform.ivl_of_appr1_coll_impl
    and do_intersection_body_impl_aform = aform.do_intersection_body_impl
    and ode_slp_impl_aform = aform.ode_slp_impl
    and print_msg_impl_aform = aform.print_msg_impl
    and ode_e_impl_aform = aform.ode_e_impl
    and safe_form_impl_aform = aform.safe_form_impl
    and D_impl_aform = aform.D_impl
    and safe_set_appr_aform = aform.safe_set_appr
    and var_ode_ops_impl = aform.var_ode_ops_impl
    and start_stepsize_impl_aform = aform.start_stepsize_impl
    and poincare_slp_impl_aform = aform.poincare_slp_impl
    and rk2_param_impl_aform = aform.rk2_param_impl

  unfolding aform_approximate_sets_def[symmetric]
  by (rule aform_approximate_sets)

lemma aform_ncc[autoref_rules_raw]: "aform.ncc_precond TYPE('a::executable_euclidean_space)"
  using aform.appr_rel_nonempty
  by (auto simp: aform.ncc_precond_def aform.ncc_def aform.appr_rel_br br_def compact_Affine
    convex_Affine
      eucl_of_list_image_Joints)

fun parts::"nat⇒'a list⇒'a list list"
  where
    "parts n [] = []"
| "parts 0 xs = [xs]"
| "parts n xs = take n xs # parts n (drop n xs)"


lemma Joints_in_lv_rel_set_relD:
  "(Joints xs, X) ∈ ⟨lv_rel⟩set_rel ⟹ X = Affine (eucl_of_list_aform xs)"
  apply auto
   apply (subst eucl_of_list_image_Joints[symmetric])
  unfolding lv_rel_def set_rel_br
    apply (auto simp: br_def )
  using aform.length_set_of_appr apply auto[1]
  apply (subst (asm) eucl_of_list_image_Joints[symmetric])
  unfolding lv_rel_def set_rel_br
   apply (auto simp: br_def )
  using aform.length_set_of_appr apply auto[1]
  done

lemma ncc_precond: "aform.ncc_precond TYPE('a::executable_euclidean_space)"
  apply (auto simp: aform.ncc_precond_def aform.ncc_def aform.appr_rel_def)
  apply (auto simp: aforms_rel_def br_def)
  subgoal by (auto simp: compact_Affine dest!: Joints_in_lv_rel_set_relD)
  subgoal by (auto simp: convex_Affine dest!: Joints_in_lv_rel_set_relD)
  done

lemma fst_eucl_of_list_aform_map: "fst (eucl_of_list_aform (map (λx. (fst x, asdf x)) x)) =
  fst (eucl_of_list_aform x)"
  by (auto simp: eucl_of_list_aform_def o_def)

lemma
  Affine_pdevs_of_list:― ‹TODO: move!›
  "Affine (fst x, pdevs_of_list (map snd (list_of_pdevs (snd x)))) = Affine x"
  by (auto simp: Affine_def valuate_def aform_val_def
      elim: pdevs_val_of_list_of_pdevs2[where X = "snd x"]
        pdevs_val_of_list_of_pdevs[where X = "snd x"])

lemmas one_step_in_ivl = aform.one_step_in_ivl_ncc[OF ncc_precond ncc_precond]
lemmas solves_poincare_map = aform.solves_poincare_map_ncc[OF ncc_precond ncc_precond]
lemmas solves_poincare_map' = aform.solves_poincare_map'_ncc[OF ncc_precond ncc_precond]
lemmas solves_poincare_map_onto = aform.solves_poincare_map_onto_ncc[OF ncc_precond ncc_precond]

end