Theory Refine_Reachability_Analysis_C1

theory Refine_Reachability_Analysis_C1
  imports
    Abstract_Reachability_Analysis_C1
    Refine_Reachability_Analysis
begin

lemma fst_flow1_of_vec1[simp]: "fst (flow1_of_vec1 x) = fst x"
  by (auto simp: flow1_of_vec1_def)

lemma fst_vec1_of_flow[simp]: "fst (vec1_of_flow1 x) = fst x"
  by (auto simp: vec1_of_flow1_def)

context approximate_sets_ode'
begin

lemma poincare_mapsto_scaleR2I:
  "poincare_mapsto P (scaleR2 x1 x2 baa) UNIV x1b (scaleR2 x1 x2 aca)"
  if "poincare_mapsto P (baa) UNIV x1b (aca)"
  using that
  apply (auto simp: poincare_mapsto_def scaleR2_def image_def vimage_def)
  apply (drule bspec, assumption)
  apply auto
  apply (rule exI, rule conjI, assumption)
  apply (rule exI, rule conjI, assumption, rule conjI, assumption)
  apply (rule bexI) prefer 2 apply assumption
  apply (auto simp: scaleR_blinfun_compose_right)
  done

context includes ode_ops.lifting begin
lemma var_safe_form_eq[simp]: "var.safe_form = safe_form"
  unfolding var.safe_form_def
  by transfer (auto simp: var_ode_ops_def safe_form_def)

lemma var_ode_e: "var.ode_e = ode_e'"
  unfolding var.ode_e_def
  by transfer (auto simp: var_ode_ops_def)
end

lemma wd_imp_var_wd[refine_vcg, intro]: "wd (TYPE('n rvec))  var.wd (TYPE('n::enum vec1))"
  unfolding var.wd_def
  by (auto simp: wd_def length_concat o_def sum_list_distinct_conv_sum_set
      concat_map_map_index var_ode_e D_def ode_e'_def
      intro!: max_Var_floatariths_mmult_fa[le] max_Var_floatariths_mapI
      max_Var_floatarith_FDERIV_floatarith[le]
      max_Var_floatariths_fold_const_fa[le]
      max_Var_floatarith_le_max_Var_floatariths_nthI
      max_Var_floatariths_list_updateI max_Var_floatariths_replicateI)

lemma safe_eq:
  assumes "wd TYPE('n::enum rvec)"
  shows "var.Csafe = ((Csafe × UNIV)::'n vec1 set)"
  using assms var.wdD[OF wd_imp_var_wd[OF assms]] wdD[OF assms]
  unfolding var.safe_def safe_def var.wd_def wd_def var.Csafe_def Csafe_def
  unfolding ode_e'_def var_ode_e
  apply (auto simp: D_def)
  subgoal
    apply (subst interpret_form_max_Var_cong) prefer 2 apply assumption
    by (auto simp: nth_Basis_list_prod)
  subgoal for a b
    apply (drule isFDERIV_appendD1)
        apply simp apply simp apply (auto intro!: max_Var_floatariths_fold_const_fa[le])[]
    apply (rule isFDERIV_max_Var_congI, assumption)
    by (auto simp: nth_Basis_list_prod)
  subgoal
    apply (subst interpret_form_max_Var_cong) prefer 2 apply assumption
    by (auto simp: nth_Basis_list_prod)
  subgoal for a b
    apply (rule isFDERIV_appendI1)
    apply (rule isFDERIV_max_Var_congI, assumption)
        apply (auto simp: nth_Basis_list_prod)
     apply (auto simp: isFDERIV_def FDERIV_floatariths_def in_set_conv_nth isDERIV_inner_iff
      length_concat o_def sum_list_distinct_conv_sum_set concat_map_map_index
        intro!: isDERIV_FDERIV_floatarith isDERIV_mmult_fa_nth)
     apply (rule isDERIV_max_Var_floatarithI[where ys="list_of_eucl a"])
    subgoal for i j k
      apply (cases "i < CARD('n)")
      subgoal by auto
      subgoal apply (rule isDERIV_max_VarI)
         apply (rule max_Var_floatarith_le_max_Var_floatariths_nthI)
          apply force
         apply auto
        done
      done
    subgoal for i j k l by (auto dest!: max_Var_floatariths_lessI simp: nth_Basis_list_prod)
    subgoal by (auto simp: nth_list_update)
    done
  done

lemma
  var_ode_eq:
  fixes x::"'n::enum vec1"
  assumes "wd TYPE('n rvec)" and [simp]: "(fst x)  Csafe"
  shows "var.ode x = (ode (fst x), matrix (ode_d1 (fst x)) ** snd x)"
proof -
  have "interpret_floatariths ode_e (list_of_eucl x) =
    interpret_floatariths ode_e (list_of_eucl (fst x))"
    apply (rule interpret_floatariths_max_Var_cong)
    using wdD[OF wd _]
    by (auto simp: list_of_eucl_nth_if nth_Basis_list_prod inner_prod_def)
  moreover
  have "eucl_of_list
            (interpret_floatariths
              (mmult_fa D D D
       (concat (map (λj. map (λi. FDERIV_floatarith (ode_e ! j) [0..<D] ((replicate D 0)[i := 1])) [0..<D]) [0..<D]))
       (map floatarith.Var [D..<D + D * D])) (list_of_eucl x)) =
    matrix (blinfun_apply (ode_d 0 (fst x) 0)) ** snd x"
    unfolding matrix_eq
    apply auto
    apply (subst matrix_vector_mul_assoc[symmetric])
    apply (subst matrix_works)
    subgoal by (auto simp: linear_matrix_vector_mul_eq
          intro!: bounded_linear.linear blinfun.bounded_linear_right)
    apply (subst einterpret_mmult_fa[where 'n='n and 'm = 'n and 'l='n])
    subgoal by (simp add: wdD[OF wd _])
    subgoal by (simp add: length_concat o_def sum_list_distinct_conv_sum_set wdD[OF wd _])
    subgoal by (simp add: length_concat o_def sum_list_distinct_conv_sum_set wdD[OF wd _])
    subgoal for v
    proof -
      have v: "einterpret (map floatarith.Var [D..<D + D * D]) (list_of_eucl x) *v v = snd x *v v"
        apply (vector matrix_vector_mult_def)
        apply (simp add: vec_nth_eq_list_of_eucl2 wdD[OF wd _])
        apply (auto simp: vec_nth_eq_list_of_eucl1 sum_index_enum_eq)
        apply (subst sum_index_enum_eq)+
        apply (rule sum.cong)
        by (auto simp: nth_Basis_list_prod prod_eq_iff inner_prod_def)
      show ?thesis
        unfolding matrix_vector_mul_assoc[symmetric]
        apply (subst v)
        apply (auto simp: concat_map_map_index vec_nth_eq_list_of_eucl2)
        apply (subst  eucl_of_list_list_of_eucl[of "snd x *v v", symmetric])
        apply (subst (2) eucl_of_list_list_of_eucl[of "snd x *v v", symmetric])
        apply (subst eucl_of_list_matrix_vector_mult_eq_sum_nth_Basis_list)
        subgoal by (simp add: length_concat o_def sum_list_distinct_conv_sum_set wdD[OF wd _])
        subgoal by simp
        apply (subst blinfun_apply_eq_sum)
         apply (auto simp: vec_nth_eq_list_of_eucl1 sum_index_enum_eq)
        apply (auto simp: scaleR_sum_left ode_d.rep_eq intro!: sum.cong[OF refl])
        apply (auto simp: ode_d_raw_def wdD[OF wd _] eucl_of_list_inner )
        apply (auto simp: ode_d_expr_def FDERIV_floatariths_def wdD[OF wd _] )
        apply (rule interpret_floatarith_FDERIV_floatarith_cong)
        subgoal for x y i
          using wdD[OF wd _]
          by (auto simp add: nth_append inner_prod_def
              nth_Basis_list_prod dest!: max_Var_floatariths_lessI)
        subgoal by auto
        subgoal by auto
        subgoal
          apply (auto simp: wdD[OF wd _] nth_list_update inner_Basis intro!: nth_equalityI)
          by (metis length (list_of_eucl (snd x *v v)) = CARD('n) index_Basis_list_nth length_list_of_eucl)
        done
    qed
    done
  ultimately show ?thesis
    unfolding var.ode_def ode_def
    unfolding ode_e'_def var_ode_e
    by (auto simp: wdD[OF wd _] ode_d1_def intro!: euclidean_eqI[where 'a="'n vec1"])
qed

lemma var_existence_ivl_imp_existence_ivl:
  fixes x::"'n::enum vec1"
  assumes wd: "wd TYPE('n rvec)"
  assumes t: "t  var.existence_ivl0 x"
  shows "t  existence_ivl0 (fst x)"
proof (rule existence_ivl_maximal_segment)
  from var.flow_solves_ode[OF UNIV_I var.mem_existence_ivl_iv_defined(2), OF t]
  have D: "(var.flow0 x solves_ode (λ_. var.ode)) {0--t} (var.Csafe)"
    apply (rule solves_ode_on_subset)
     apply (rule var.closed_segment_subset_existence_ivl)
     apply (rule t)
    apply simp
    done
  show "((λt. fst (var.flow0 x t)) solves_ode (λ_. ode)) {0--t} (Csafe)"
    using var.closed_segment_subset_existence_ivl[OF t]
    apply (auto simp: has_vderiv_on_def has_vector_derivative_def subset_iff
        intro!: solves_odeI derivative_eq_intros)
        apply (rule refl)
       apply (rule refl)
      apply (rule refl)
     apply (auto simp: var.flowderiv_def )
     apply (subst var_ode_eq[OF wd(1)])
      apply (auto simp: blinfun.bilinear_simps)
    subgoal for s
      using solves_odeD(2)[OF D, of s]
      by (subst(asm) (3) safe_eq[OF wd]) (auto )
    subgoal for s
      using solves_odeD(2)[OF D, of s]
      by (subst(asm) (3) safe_eq[OF wd]) (auto )
    done
next
  show "fst (var.flow0 x 0) = fst x"
    apply (subst var.flow_initial_time)
      apply simp
    apply (rule var.mem_existence_ivl_iv_defined[OF t])
    apply auto
    done
qed simp

lemma existence_ivl_imp_var_existence_ivl:
  fixes x::"'n::enum rvec"
  assumes wd: "wd TYPE('n rvec)"
  assumes t: "t  existence_ivl0 x"
  shows "t  var.existence_ivl0 ((x, W)::'n vec1)"
proof (rule var.existence_ivl_maximal_segment)
  from flow_solves_ode[OF UNIV_I mem_existence_ivl_iv_defined(2), OF t]
  have D: "(flow0 x solves_ode (λ_. ode)) {0--t} (Csafe)"
    apply (rule solves_ode_on_subset)
     apply (rule closed_segment_subset_existence_ivl)
     apply (rule t)
    apply simp
    done
  show "((λt. (flow0 x t, matrix (Dflow x t) ** W)) solves_ode (λ_. var.ode)) {0--t} (var.Csafe)"
    using closed_segment_subset_existence_ivl[OF t]
    apply (auto simp: has_vderiv_on_def has_vector_derivative_def subset_iff
        intro!: solves_odeI derivative_eq_intros)
        apply (rule refl)
        apply (rule refl)
        apply (rule refl)
       apply (rule has_derivative_at_withinI)
       apply (rule Dflow_has_derivative)
       apply force
      apply (rule refl)
     apply (auto simp: flowderiv_def )
     apply (subst var_ode_eq)
     apply (auto simp: blinfun.bilinear_simps matrix_blinfun_compose wd
        intro!: ext)
    subgoal for s h
      unfolding matrix_scaleR matrix_blinfun_compose matrix_mul_assoc matrix_scaleR_right ..
    subgoal for s
      using solves_odeD(2)[OF D, of s] safe_eq[OF wd]
      by auto
    done
next
  have "x  Csafe" by rule fact
  then show "(flow0 x 0, matrix (blinfun_apply (Dflow x 0)) ** W) = (x, W)"
    apply (auto )
    apply (vector matrix_def matrix_matrix_mult_def axis_def)
    by (auto simp:  if_distrib if_distribR cong: if_cong)
qed auto

theorem var_existence_ivl0_eq_existence_ivl0:
  fixes x::"'n::enum vec1"
  assumes wd: "wd TYPE('n rvec)"
  shows "var.existence_ivl0 (x::'n vec1) = existence_ivl0 (fst x)"
  apply safe
  subgoal by (rule var_existence_ivl_imp_existence_ivl[OF wd, of _ "x", simplified], simp)
  subgoal
    by (rule existence_ivl_imp_var_existence_ivl[OF wd, of _ "fst x" "snd x", unfolded prod.collapse])
  done

theorem var_flow_eq_flow_Dflow:
  fixes x::"'n::enum vec1"
  assumes wd: "wd TYPE('n rvec)"
  assumes t: "t  var.existence_ivl0 x"
  shows "var.flow0 x t = vec1_of_flow1 (flow0 (fst x) t, Dflow (fst x) t oL blinfun_of_vmatrix (snd x)) "
proof -
  have x: "x  var.Csafe"
    by (rule var.mem_existence_ivl_iv_defined[OF t])
  then have "fst x  Csafe"
    by (subst (asm) safe_eq[OF wd]) auto
  then have sx[simp]: "(fst x)  Csafe" by simp
  show ?thesis
  proof (rule var.flow_unique_on[OF t])
    show "vec1_of_flow1 (flow0 (fst x) 0, Dflow (fst x) 0 oL blinfun_of_vmatrix (snd x)) = x"
      by (auto simp: vec1_of_flow1_def x)
    show "((λa. vec1_of_flow1 (flow0 (fst x) a, Dflow (fst x) a oL blinfun_of_vmatrix (snd x))) has_vderiv_on
     (λt. var.ode (vec1_of_flow1 (flow0 (fst x) t, Dflow (fst x) t oL blinfun_of_vmatrix (snd x)))))
     (var.existence_ivl0 x)"
      apply (auto simp: has_vderiv_on_def has_vector_derivative_def vec1_of_flow1_def
          at_within_open[OF _ var.open_existence_ivl] flowderiv_def
          intro!: derivative_eq_intros var_existence_ivl_imp_existence_ivl[OF wd]
          Dflow_has_derivative ext)
      apply (subst var_ode_eq[OF wd(1)])
       apply (auto simp: blinfun.bilinear_simps)
      subgoal for t
        using flow_in_domain[of t "fst x"]
        by (simp add: var_existence_ivl_imp_existence_ivl[OF wd])
      subgoal for t h
        by (simp add: matrix_blinfun_compose matrix_scaleR matrix_mul_assoc matrix_scaleR_right)
      done
    fix t
    assume "t  var.existence_ivl0 x"
    then show "vec1_of_flow1 (flow0 (fst x) t, Dflow (fst x) t oL blinfun_of_vmatrix (snd x))  var.Csafe"
      by (subst safe_eq[OF wd])
        (auto simp: vec1_of_flow1_def dest!: var_existence_ivl_imp_existence_ivl[OF wd]
          flow_in_domain)
  qed
qed

theorem flow_Dflow_eq_var_flow:
  fixes x::"'n::enum rvec"
  assumes wd: "wd TYPE('n rvec)"
  assumes t: "t  existence_ivl0 x"
  shows "(flow0 x t, Dflow x t oL W) = flow1_of_vec1 (var.flow0 (x, matrix W) t::'n vec1)"
  using var_flow_eq_flow_Dflow[OF wd existence_ivl_imp_var_existence_ivl[OF wd t]]
  unfolding var_flow_eq_flow_Dflow[OF wd existence_ivl_imp_var_existence_ivl[OF wd t]]
  by (auto simp: flow1_of_vec1_def vec1_of_flow1_def)

context includes blinfun.lifting begin
lemma flow1_of_vec1_vec1_of_flow1[simp]:
  "flow1_of_vec1 (vec1_of_flow1 X) = X"
  unfolding vec1_of_flow1_def flow1_of_vec1_def
  by (transfer) auto
end

lemma
  var_flowpipe0_flowpipe:
  assumes wd: "wd TYPE('n::enum rvec)"
  assumes "var.flowpipe0 X0 hl hu (CX) X1"
  assumes "fst ` X0  Csafe"
  assumes "fst ` CX  Csafe"
  assumes "fst ` X1  Csafe"
  shows "flowpipe (flow1_of_vec1 ` X0) hl hu (flow1_of_vec1 ` (CX::'n vec1 set)) (flow1_of_vec1 ` X1)"
  using assms
  unfolding flowpipe_def var.flowpipe0_def
  apply safe
  subgoal by (auto simp add: flow1_of_vec1_def vec1_of_flow1_def safe_eq[OF wd])
  subgoal by (auto simp add: flow1_of_vec1_def vec1_of_flow1_def safe_eq[OF wd])
  subgoal by (auto simp add: flow1_of_vec1_def vec1_of_flow1_def safe_eq[OF wd])
  subgoal for x W y V h
    apply (drule bspec[where x="(y, V)"], force)
    apply (drule bspec, assumption)
    by (simp add: var_existence_ivl0_eq_existence_ivl0[OF wd] flow1_of_vec1_def)
  subgoal for x W y V h
    apply (drule bspec[where x="(y, V)"], force)
    apply (drule bspec, assumption)
    apply (subst flow_Dflow_eq_var_flow[OF wd],
        force simp: var_existence_ivl0_eq_existence_ivl0[OF wd] flow1_of_vec1_def)
    apply (rule imageI)
    by (simp add: vec1_of_flow1_def flow1_of_vec1_def)
  subgoal for x W y V h h'
    apply (drule bspec[where x="vec1_of_flow1 (x, W)"], force)
    apply (drule bspec, assumption)
    apply (subst flow_Dflow_eq_var_flow[OF wd])
     apply (subst (asm) var_existence_ivl0_eq_existence_ivl0[OF wd])
     apply (simp add: flow1_of_vec1_def)
    subgoal
      by (meson local.existence_ivl_initial_time local.mem_existence_ivl_iv_defined(1)
          local.mem_existence_ivl_iv_defined(2) mem_is_interval_1_I mvar.interval)
    subgoal
      apply (rule imageI)
      by (simp add: vec1_of_flow1_def flow1_of_vec1_def)
    done
  done

theorem einterpret_solve_poincare_fas:
  assumes wd: "wd TYPE('n rvec)"
  assumes "length CXs = D + D*D" "n < D"
  assumes nz: "ode (fst (eucl_of_list CXs::'n vec1))  Basis_list ! n  0"
  shows
  "flow1_of_vec1 (einterpret (solve_poincare_fas n) CXs::'n::enum vec1) =
  (let (x, d) = flow1_of_vec1 (eucl_of_list CXs::'n vec1) in (x,
     d - (blinfun_scaleR_left (ode (x)) oL
    (blinfun_scaleR_left (inverse (ode x  Basis_list ! n)) oL (blinfun_inner_left (Basis_list ! n) oL d)))))"
  using assms
  apply (auto intro!: simp: flow1_of_vec1_def solve_poincare_fas_def)
  subgoal
    apply (auto intro!: euclidean_eqI[where 'a="'n rvec"])
    apply (subst eucl_of_list_prod)
    by (auto simp: eucl_of_list_prod length_concat o_def sum_list_distinct_conv_sum_set D_def Let_def
        wdD[OF wd] take_eq_map_nth)
  subgoal premises prems
  proof -
    have ode_e_eq: "interpret_floatarith (ode_e ! i) (map ((!) CXs) [0..<CARD('n)]) = interpret_floatarith (ode_e ! i) CXs"
      if "i < D"
      for i
      apply (rule interpret_floatarith_max_Var_cong)
      apply (drule max_Var_floatariths_lessI)
      using that apply (simp add: wdD[OF wd])
      apply (subst nth_map)
       apply auto
      using wdD[OF wd]
      apply simp
      using wdD[OF wd]
      apply simp
      done
    define z where "z = (0::float)"
    show ?thesis
      supply [simp] = snd_eucl_of_list_prod fst_eucl_of_list_prod
      supply [simp del] = eucl_of_list_take_DIM
      using prems unfolding z_def[symmetric] D_def Let_def
      including blinfun.lifting
      apply (transfer fixing: CXs n z)
      unfolding z_def
      apply (auto simp: o_def ode_def intro!: ext)
      apply (vector matrix_vector_mult_def )
      apply (auto intro!: blinfun_euclidean_eqI simp: inner_Basis_eq_vec_nth wdD[OF wd])
      apply (auto simp: length_concat o_def sum_list_distinct_conv_sum_set wdD[OF wd] take_eq_map_nth)
      apply (auto simp: concat_map_map_index)
      apply (vector )
      apply (subst vec_nth_eq_list_of_eucl2 vec_nth_eq_list_of_eucl1)+
      apply (subst (asm) vec_nth_eq_list_of_eucl2 vec_nth_eq_list_of_eucl1)+
      apply (simp add: less_imp_le wdD[OF wd] index_nth_id )
      apply (auto simp: algebra_simps ode_e_eq wdD[OF wd] divide_simps)
      done
  qed
  done

lemma choose_step'_flowpipe:
  assumes wd[refine_vcg]: "wd TYPE('n::enum rvec)"
  assumes safe: "fst ` X0  Csafe"
  shows "var.choose_step (X0::'n vec1 set) h  SPEC (λ(h', _, RES_ivl, RES::'n vec1 set).
      0 < h'  h'  h  flowpipe (flow1_of_vec1 ` X0) h' h' (flow1_of_vec1 ` RES_ivl) (flow1_of_vec1 ` RES))"
  apply refine_vcg
  apply auto
  apply (frule var.flowpipe0_safeD)
  apply (drule var_flowpipe0_flowpipe[rotated])
  by (auto simp: safe_eq wd)

lemma max_Var_floatariths_solve_poincare_fas[le]:
  assumes wd: "wd (TYPE('n::enum rvec))"
  shows "i < D  max_Var_floatariths (solve_poincare_fas i)  D + D * D"
  by (auto simp: solve_poincare_fas_def concat_map_map_index Let_def
      intro!: max_Var_floatariths_leI Suc_leI)
   (auto intro!: max_Var_floatarith_le_max_Var_floatariths_nthI max_Var_floatariths_ode_e_wd[OF wd]
      simp: wdD[OF wd])

lemma length_solve_poincare_fas[simp]: "length (solve_poincare_fas n) = D + D * D"
  by (auto simp: solve_poincare_fas_def length_concat o_def sum_list_distinct_conv_sum_set D_def Let_def)

theorem interpret_floatariths_solve_poincare_fas:
  assumes wd: "wd TYPE('n::enum rvec)"
  assumes "length CXs = D + D*D" "n < D"
  assumes nz: "ode (fst (eucl_of_list CXs::'n vec1))  Basis_list ! n  0"
  shows
  "interpret_floatariths (solve_poincare_fas n) CXs =
    list_of_eucl (vec1_of_flow1 (let (x, d) = flow1_of_vec1 (eucl_of_list CXs::'n vec1) in (x,
       d - (blinfun_scaleR_left (ode (x)) oL
      (blinfun_scaleR_left (inverse (ode x  Basis_list ! n)) oL (blinfun_inner_left (Basis_list ! n) oL d))))))"
  using arg_cong[where f="list_of_eucl::'n vec1  _", OF arg_cong[where f=vec1_of_flow1, OF einterpret_solve_poincare_fas[OF assms]]]
  apply auto
  apply (subst (asm) list_of_eucl_eucl_of_list)
   apply auto
  apply (auto simp: wdD[OF wd])
  done

lemma length_solve_poincare_slp[simp]: "length solve_poincare_slp = D"
  by (auto simp: solve_poincare_slp_def)

lemma ne_zero_lemma:
  assumes
    "ode ` fst ` CX  FC"
   "bFC. b  n  0"
   "(a, b)  CX"
   "ode a  n = 0"
 shows "False"
proof -
  have "(a, b)  CX" by fact
  then have "ode (fst (a, b))  ode ` fst ` CX" by blast
  also have "  FC"
    by fact
  finally have "ode a  FC" by simp
  with assms show False
    by auto
qed

lemma ne_zero_lemma2:
  assumes
   "ode ` fst ` flow1_of_vec1 ` env  F"
   "xF. x  n  0"
   "(a, b)  env"
   "flow1_of_vec1 (a, b) = (a', b')"
   "ode a'  n = 0"
 shows False
proof -
  have "(a', b')  flow1_of_vec1 ` env"
    apply (rule image_eqI)
    using assms by auto
  then have "ode (fst (a', b'))  ode ` fst ` " by blast
  also from assms have "  F" by simp
  finally have "ode a'  F" by simp
  with assms have "ode a'  n  0" by auto
  with assms show False by simp
qed

lemma solve_poincare_plane[le, refine_vcg]:
  assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
  assumes "n  Basis"
  shows "solve_poincare_plane (n::'n::enum rvec) CX  SPEC (λPDP.
    fst ` PDP  Csafe 
    ((x, d)  CX. (x, d - (blinfun_scaleR_left (ode x) oL
      (blinfun_scaleR_left (inverse (ode x  n)) oL (blinfun_inner_left n oL d))))  PDP) 
    ((x, d)  PDP. ode x  n  0))"
  unfolding solve_poincare_plane_def
  apply (refine_vcg)
  subgoal using assms by auto
  subgoal using assms by auto
  subgoal using assms by auto
  subgoal using assms by (auto simp: solve_poincare_slp_def)
  subgoal using assms by auto
  subgoal for C1 FC _ CX' CX'' P P1 FP _
    apply auto
    apply (drule bspec, assumption)
    apply (rule image_eqI)
     prefer 2 apply assumption
    apply (subst einterpret_solve_poincare_fas)
    subgoal using wd by auto
    subgoal using wd by auto
    subgoal using wd by auto
    subgoal using wd assms by (auto elim!: ne_zero_lemma)
    subgoal using wd assms by auto
    done
  subgoal by (auto elim!: ne_zero_lemma2)
  done

lemma choose_step1_flowpipe[le, refine_vcg]:
  assumes wd[refine_vcg]: "wd TYPE('n::enum rvec)"
  shows "choose_step1 (X0::'n eucl1 set) h  SPEC (λ(h', _, RES_ivl, RES::'n eucl1 set).
      0 < h'  h'  h  flowpipe X0 h' h' RES_ivl RES)"
  using assms
  unfolding choose_step1_def
  by (refine_vcg choose_step'_flowpipe[le] wd)
    (auto simp: image_image,
      auto simp: safe_eq vec1_of_flow1_def flowpipe0_imp_flowpipe env_len_def)

lemma image_flow1_of_vec1I:
  "vec1_of_flow1 x  X  x  flow1_of_vec1 ` X"
  by (rule image_eqI) (rule flow1_of_vec1_vec1_of_flow1[symmetric])

lemma inter_sctn1_spec[le, refine_vcg]:
  "inter_sctn1_spec X sctn  SPEC (λ(R, S). X  plane_of sctn × UNIV  R  fst ` R  plane_of sctn
   X  plane_of sctn × UNIV  S  fst ` S  plane_of sctn)"
  unfolding inter_sctn1_spec_def
  apply (refine_vcg, auto)
  subgoal by (rule image_flow1_of_vec1I) (auto simp: plane_of_def inner_prod_def)
  subgoal by (auto simp: plane_of_def inner_prod_def)
  subgoal by (rule image_flow1_of_vec1I)
         (force simp: set_plus_def plane_of_def inner_prod_def vec1_of_flow1_def)
  subgoal by (force simp: set_plus_def)
  done

lemma fst_safe_coll[le, refine_vcg]:
  "wd TYPE('a) 
      fst_safe_coll (X::('a::executable_euclidean_space*'c) set)  SPEC (λR. R = fst ` X  fst ` X  Csafe)"
  unfolding fst_safe_coll_def
  by refine_vcg

lemma vec1reps[THEN order_trans, refine_vcg]: "vec1reps CX  SPEC (λR. case R of None  True | Some X  X = vec1_of_flow1 ` CX)"
  unfolding vec1reps_def
  apply (refine_vcg FORWEAK_mono_rule[where
        I="λXS R. case R of None  True | Some R  vec1_of_flow1 ` (XS)  R  R  vec1_of_flow1 ` CX"])
  by (auto simp:  split: option.splits) force+

lemma nonzero_component_within[le, refine_vcg]:
  assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
  shows "nonzero_component_within ivl sctn (PDP::'n eucl1 set)  SPEC (λb.
    (b  (xPDP. fst x  ivl  (F x in at (fst x) within plane_of sctn. x  ivl))) 
    fst ` PDP  Csafe 
    (xPDP. ode (fst x)  normal sctn  0))"
  unfolding nonzero_component_within_def
  by refine_vcg auto

lemma do_intersection_invar_inside:
  "do_intersection_invar guards b ivl sctn X (e, f, m, n, p, q, True) 
  fst ` e  sabove_halfspace sctn 
  fst ` mn  ivl 
  mn = m  mn = n 
  do_intersection_spec UNIV guards ivl sctn X (mn, p)"
  subgoal premises prems
  proof -
    from prems have e: "e  sbelow_halfspace sctn × UNIV = {}"
      by (auto simp: halfspace_simps plane_of_def)
    with prems(1) have
      "poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} X UNIV p m"
      "poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} X UNIV p n"
      "e  sbelow_halfspace sctn × UNIV = {}"
      "fst ` X  b = {}"
      "fst ` X  sbelow_halfspace sctn"
      "ivl  plane (normal sctn) (pstn sctn)"
      "fst ` X  p"
      "fst ` m  Csafe"
      "fst ` n  Csafe"
      "p  Csafe"
      "fst ` e  Csafe"
      "f  {0..}"
      "p  sbelow_halfspace sctn - guards"
      "e  (- guards) × UNIV"
      "fst ` (m  n)  guards = {}"
      "0  (λx. ode x  normal sctn) ` fst ` (m  n)"
      "xm  n. F x in at (fst x) within plane (normal sctn) (pstn sctn). x  ivl"
      by (auto simp: do_intersection_invar_def do_intersection_spec_def plane_of_def)
    then show ?thesis
      using prems(2-)
      by (auto simp: do_intersection_spec_def plane_of_def halfspace_simps)
  qed
  done

lemma do_intersection_body_lemma:
  assumes "flowsto A T (i × UNIV) (X'  sbelow_halfspace sctn × UNIV)"
    "poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} B UNIV i PS "
    "poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} B UNIV i PS2"
    "T  {0..}"
    "i  sbelow_halfspace sctn - guards"
    "fst ` (A  B)  sbelow_halfspace sctn"
    "fst ` PS  Csafe "
    "fst ` PS2  Csafe "
    X = A  B
  assumes ivl: "closed ivl" "ivl  plane_of sctn"
  assumes normal_Basis: "¦normal sctn¦  Basis"
    and inter_empties: "fst ` Y  GUARDS = {}" "fst ` CX'  GUARDS = {}"
    "fst ` PDP'  GUARDS = {}" "fst ` PDP''  GUARDS = {}"
    and h': "0 < h'" "h'  h"
    and safe: "fst ` PDP  Csafe" "fst ` CX'  Csafe"
    "fst ` PDP'  Csafe"
    "fst ` PDP''  Csafe"
    and PDP:
    "(x,d)CX'. (x,
            d - (blinfun_scaleR_left (ode x) oL
                  (blinfun_scaleR_left (inverse (ode x  ¦normal sctn¦)) oL
                  (blinfun_inner_left ¦normal sctn¦ oL d))))
                PDP"
    and PDP': "PDP  plane_of sctn × UNIV  PDP'"
    and PDP'': "PDP  plane_of sctn × UNIV  PDP''"
    and evin:
    "xPDP'. fst x  ivl  (F x in at (fst x) within plane_of sctn. x  ivl)"
    "xPDP''. fst x  ivl  (F x in at (fst x) within plane_of sctn. x  ivl)"
    and through: "(x, d)PDP. ode x  ¦normal sctn¦  0"
    "xPDP'. ode (fst x)  normal sctn  0"
    "xPDP''. ode (fst x)  normal sctn  0"
    and plane:
    "fst ` PDP'  plane_of sctn"
    "fst ` PDP''  plane_of sctn"
    and flowpipe: "flowpipe X' h' h' CX' Y"
  shows "A B. X = A  B 
        flowsto A {0<..} ((fst ` CX'  sbelow_halfspace sctn  i) × UNIV) (Y  sbelow_halfspace sctn × UNIV) 
        poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} B UNIV (fst ` CX'  sbelow_halfspace sctn  i) (PDP'  PS) 
        poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} B UNIV (fst ` CX'  sbelow_halfspace sctn  i) (PDP''  PS2)"
proof -
  from flowpipe
  have 1: "flowpipe (X'  (sbelow_halfspace sctn) × UNIV) h' h' CX' Y"
    by (rule flowpipe_subset) (use flowpipe in auto dest!: flowpipe_safeD)
  have 2: "fst ` (X'  (sbelow_halfspace sctn) × UNIV)  {x. pstn sctn  x  normal sctn} = {}"
    by (auto simp: halfspace_simps plane_of_def)
  from normal_Basis have 3: "normal sctn  0"
    by auto
  note 4 = closed ivl
  from ivl  plane_of sctn have 5: "ivl  plane (normal sctn) (pstn sctn)"
    by (auto simp: plane_of_def)
  have 6: "(x, d)  CX'  x  plane (normal sctn) (pstn sctn) 
          (x, d - (blinfun_scaleR_left (ode x) oL
                   (blinfun_scaleR_left (inverse (ode x  normal sctn)) oL (blinfun_inner_left (normal sctn) oL d))))
           PDP'  PDP''" for x d
    unfolding PDP_abs_lemma[OF normal_Basis]
    apply (drule PDP[rule_format, of "(x, d)", unfolded split_beta' fst_conv snd_conv])
    using PDP' PDP''
    by (auto simp: plane_of_def)
  from normal_Basis through
  have 7: "(x, d)  PDP'  ode x  normal sctn  0" for x d
    by (auto elim!: abs_in_BasisE)
  have 8: "(x, d)  PDP'  x  ivl" for x d
    using evin by auto
  have 9: "(x, d)  PDP'  F x in at x within plane (normal sctn) (pstn sctn). x  ivl" for x d
    using evin by (auto simp add: plane_of_def)
  obtain X1 X2
    where X1X2: "X'  sbelow_halfspace sctn × UNIV = X1  X2"
      and X1: "flowsto X1 {0<..h'} (CX'  {x. x  normal sctn < pstn sctn} × UNIV)
                      (CX'  {x  ivl. x  normal sctn = pstn sctn} × UNIV)"
      and X2: "flowsto X2 {h'..h'} (CX'  {x. x  normal sctn < pstn sctn} × UNIV)
                      (Y  {x. x  normal sctn < pstn sctn} × UNIV)"
      and P: "poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} X1 UNIV
                      (fst ` CX'  {x. x  normal sctn < pstn sctn}) (PDP'  PDP'')"
    by (rule flowpipe_split_at_above_halfspace[OF 1 2 3 4 5 6 7 8 9]) (auto simp: Ball_def)
  from flowsto A _ _ _[unfolded X1X2]
  obtain p1 p2 where p1p2: "A = p1  p2" and p1: "flowsto p1 T (i × UNIV) X1" and p2: "flowsto p2 T (i × UNIV) X2"
    by (rule flowsto_unionE)
  have "A  B = p2  (p1  B)" using A = p1  p2
    by auto
  moreover
  from flowsto_trans[OF p2 X2]
  have "flowsto p2 {0<..} ((fst ` CX'  (sbelow_halfspace sctn)  i) × UNIV)
           (Y  (sbelow_halfspace sctn) × UNIV)"
    apply (rule flowsto_subset)
    subgoal by (auto simp: halfspace_simps)
    subgoal using h' T  _ by (auto simp: halfspace_simps intro!: add_nonneg_pos)
    subgoal
      using flowpipe_source_subset[OF 1, unfolded X1X2] X1X2
      apply auto
      by (auto simp: halfspace_simps)
    subgoal by (auto simp: halfspace_simps)
    done
  moreover
  have cls: "closed {x  ivl. x  normal sctn = pstn sctn}"
    by (rule closed_levelset_within continuous_intros closed ivl)+
  from flowsto_trans[OF p1 X1]
  have ftt: "flowsto p1 ({s + t |s t. s  T  t  {0<..h'}})
       (i × UNIV  CX'  {x. x  normal sctn < pstn sctn} × UNIV  X1  X1)
       (X1 - X1  CX'  {x  ivl. x  normal sctn = pstn sctn} × UNIV)"
    by auto
  from X1X2 have X1_sb: "X1  sbelow_halfspace sctn × UNIV" by auto
  have "{x  ivl. x  normal sctn = pstn sctn} × UNIV  (i × UNIV  CX'  {x. x  normal sctn < pstn sctn} × UNIV  X1) = {}"
    apply (intro Int_Un_eq_emptyI)
    subgoal using i  sbelow_halfspace sctn - guards by (auto simp: halfspace_simps)
    subgoal by (auto simp: halfspace_simps)
    subgoal using X1_sb by (auto simp: halfspace_simps)
    done
  then have inter_empty:
    "{x  ivl. x  normal sctn = pstn sctn} × UNIV  (i × UNIV  CX'  {x. x  normal sctn < pstn sctn} × UNIV  X1  X1) = {}"
    by auto
  have p1ret: "returns_to {x  ivl. x  normal sctn = pstn sctn} x"
    and p1pm: "poincare_map {x  ivl. x  normal sctn = pstn sctn} x  fst ` (PDP'  PDP'')"
    if "(x, d)  p1" for x d
     apply (rule flowsto_poincareD[OF ftt _ inter_empty _ _ _ order_refl])
    subgoal by auto
    subgoal by fact
    subgoal using T  _ by auto
    subgoal using that by auto
    subgoal
      apply (rule flowsto_poincareD[OF ftt _ inter_empty])
      subgoal by auto
      subgoal by fact
      subgoal using T  _ by auto
      subgoal using that by auto
      subgoal using 6 by force
      done
    done
  have crt: "isCont (return_time {x  ivl. x  normal sctn - pstn sctn = 0}) x" if "(x, d)  p1" for x d
    apply (rule return_time_isCont_outside[where Ds="λ_. blinfun_inner_left (normal sctn)"])
    subgoal by (simp add: p1ret[OF that])
    subgoal by fact
    subgoal by (auto intro!: derivative_eq_intros)
    subgoal by simp
    subgoal apply simp
      using p1pm[OF that]
      by (auto dest!: 7)
    subgoal
      using p1pm[OF that]
      by (auto dest!: 9 simp: eventually_at_filter)
    subgoal
      using fst ` (A  B)  sbelow_halfspace sctn that p1p2
      by (auto simp: halfspace_simps)
    done
  have pmij: "poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} p1 UNIV
        (fst ` (i × UNIV  X1)  fst ` CX'  {x. x  normal sctn < pstn sctn}) (PDP'  PDP'')"
    apply (rule flowsto_poincare_trans[OF flowsto _ _ _ X1 P])
    subgoal using T  {0..} by auto
    subgoal by auto
    subgoal
      using i  sbelow_halfspace sctn - guards X1X2
      by (force simp: halfspace_simps)
    subgoal by fact
    subgoal for x d using crt by simp
    subgoal by auto
    done
  from pmij have "poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} p1 UNIV (fst ` (i × UNIV  X1)  fst ` CX'  {x. x  normal sctn < pstn sctn}) PDP'"
    apply (rule poincare_mapsto_subset)
    using fst ` PDP'  Csafe
    by auto
  from this poincare_mapsto _ _ _ i PS
  have "poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} (p1  B) UNIV
      ((fst ` (i × UNIV  X1)  fst ` CX'  {x. x  normal sctn < pstn sctn})  i) (PDP'  PS)"
    by (intro poincare_mapsto_unionI) (auto simp: plane_of_def)
  then have "poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} (p1  B) UNIV (fst ` CX'  sbelow_halfspace sctn  i) (PDP'  PS)"
    apply (rule poincare_mapsto_subset)
    subgoal by auto
    subgoal by auto
    subgoal
      using flowpipe_source_subset[OF 1, unfolded X1X2] X1X2 
      apply (auto simp: halfspace_simps subset_iff)
      done
    subgoal using safe fst ` PS  Csafe by auto
    done
  moreover
  from pmij have "poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} p1 UNIV (fst ` (i × UNIV  X1)  fst ` CX'  {x. x  normal sctn < pstn sctn}) PDP''"
    apply (rule poincare_mapsto_subset)
    using fst ` PDP''  Csafe
    by auto
  from this poincare_mapsto _ _ _ i PS2
  have "poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} (p1  B) UNIV
      ((fst ` (i × UNIV  X1)  fst ` CX'  {x. x  normal sctn < pstn sctn})  i) (PDP''  PS2)"
    by (intro poincare_mapsto_unionI) (auto simp: plane_of_def)
  then have "poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} (p1  B) UNIV (fst ` CX'  sbelow_halfspace sctn  i) (PDP''  PS2)"
    apply (rule poincare_mapsto_subset)
    subgoal by auto
    subgoal by auto
    subgoal
      using flowpipe_source_subset[OF 1, unfolded X1X2] X1X2
      apply (auto simp: halfspace_simps subset_iff)
      done
    subgoal using safe fst ` PS2  Csafe by auto
    done
  ultimately
  show ?thesis
    unfolding X = A  B by blast
qed

lemma do_intersection_body_spec:
  fixes guards::"'n::enum rvec set"
  assumes invar: "do_intersection_invar guards GUARDS ivl sctn X (X', T, PS, PS2, i, True, True)"
    and wdp[refine_vcg]: "wd TYPE('n rvec)"
    and X: "fst ` X  Csafe"
    and ivl: "closed ivl" and GUARDS: "guards  GUARDS"
  shows "do_intersection_body GUARDS ivl sctn h (X', T, PS, PS2, i, True, True) 
    SPEC (do_intersection_invar guards GUARDS ivl sctn X)"
proof -
  from invar
  obtain A B where AB: "fst ` (A  B)  GUARDS = {} "
    "fst ` (A  B)  sbelow_halfspace sctn "
    "ivl  plane_of sctn "
    "fst ` (A  B)  i "
    "fst ` PS  Csafe "
    "fst ` PS2  Csafe "
    "i  Csafe "
    "fst ` X'  Csafe "
    "T  {0..}"
    "i  sbelow_halfspace sctn - guards "
    "X'  (- guards) × UNIV "
    "fst ` (PS  PS2)  guards = {} "
    "0  (λx. ode x  normal sctn) ` fst ` (PS  PS2) "
    "xPS  PS2. F x in at (fst x) within plane_of sctn. x  ivl "
    "X = A  B "
    "flowsto A T (i × UNIV) (X'  sbelow_halfspace sctn × UNIV)"
    "poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} B UNIV i PS "
    "poincare_mapsto {x  ivl. x  normal sctn = pstn sctn} B UNIV i PS2"
    by (auto simp: do_intersection_invar_def)

  have ev_in_ivl: "F x in at p within plane_of sctn. x  ivl" if
    xd. fst x  ivl  (F x in at (fst x) within plane_of sctn. x  ivl)
    xe. fst x  ivl  (F x in at (fst x) within plane_of sctn. x  ivl)
    (p, q)  d  (p, q)  PS  (p, q)  e  (p, q)  PS2
    for p q d e
      using xPS  PS2. F x in at (fst x) within plane_of sctn. x  ivl
      using that
      by (auto dest!: bspec[where x="(p, q)"])

  show ?thesis
    unfolding do_intersection_body_def do_intersection_invar_def
    apply simp
    apply (refine_vcg, clarsimp_all)
    subgoal using AB by auto
    subgoal using AB by auto
    subgoal using AB by auto
    subgoal
      apply (rule conjI)
      subgoal using AB by auto― ‹unnecessarily slow›
      subgoal using AB by fastforce
      done
    subgoal using AB by auto
    subgoal using AB by auto
    subgoal using AB by auto
    subgoal by (auto dest!: flowpipe_safeD)
    subgoal
      apply safe
      subgoal using AB GUARDS by auto
      subgoal using AB by auto
      subgoal using AB by auto
      subgoal using AB GUARDS by auto
      subgoal using AB by auto
      subgoal using AB by auto
      done
    subgoal using AB GUARDS by auto
    subgoal using AB GUARDS by auto― ‹unnecessarily slow›
    subgoal using AB GUARDS by auto
    subgoal using AB assms by (auto intro: ev_in_ivl)
    subgoal using AB assms apply - by (rule do_intersection_body_lemma)
    done
qed

lemma
  do_intersection_spec[le, refine_vcg]:
  assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
  shows "do_intersection guards ivl sctn (X::'n eucl1 set) h 
    SPEC (λ(inside, P, P2, CX). (inside 
      (do_intersection_spec UNIV guards ivl sctn X (P, CX) 
       do_intersection_spec UNIV guards ivl sctn X (P2, CX))  fst ` X  CX))"
  using assms
  unfolding do_intersection_def autoref_tag_defs
  apply (refine_vcg, clarsimp_all)
  subgoal
    unfolding do_intersection_invar_def
    apply clarsimp
    apply (intro conjI)
       apply force
      apply force
     apply force
    apply (rule exI[where x=X])
    apply (rule exI[where x="{}"])
    by (auto intro!: flowsto_self)
  subgoal by (rule do_intersection_body_spec)
  subgoal by (rule do_intersection_invar_inside, assumption) auto
  subgoal by (rule do_intersection_invar_inside, assumption) auto
  subgoal by (auto simp: plane_of_def halfspace_simps do_intersection_invar_def)
  done

lemma mem_flow1_of_vec1_image_iff[simp]:
  "(c, d)  flow1_of_vec1 ` a  vec1_of_flow1 (c, d)  a"
  by force

lemma mem_vec1_of_flow1_image_iff[simp]:
  "(c, d)  vec1_of_flow1 ` a  flow1_of_vec1 (c, d)  a"
  by force

lemma split_spec_param1[le, refine_vcg]: "split_spec_param1 X  SPEC (λ(A, B). X  A  B)"
  unfolding split_spec_param1_def
  apply (refine_vcg)
  apply (auto simp add: subset_iff split: option.splits)
  by (metis flow1_of_vec1_vec1_of_flow1 surjective_pairing)

lemma do_intersection_spec_empty:
  "X = {}  Y = {}  do_intersection_spec S sctns ivl sctn X ({}, Y)"
  by (auto simp: do_intersection_spec_def halfspaces_union)

lemma do_intersection_spec_subset:
  "do_intersection_spec S osctns ivl csctns Y (a, b)  X  Y  do_intersection_spec S osctns ivl csctns X (a, b)"
  by (auto simp: do_intersection_spec_def halfspaces_union intro: flowsto_subset poincare_mapsto_subset)

lemma do_intersection_spec_union:
  "do_intersection_spec S osctns ivl csctns a (b, c) 
   do_intersection_spec S osctns ivl csctns f (g, h) 
   do_intersection_spec S osctns ivl csctns (a  f) (b  g, c  h)"
  by (auto simp: do_intersection_spec_def intro!: poincare_mapsto_unionI)

lemma scaleR2_rep_of_coll[le, refine_vcg]:
  "scaleR2_rep_coll X  SPEC (λ((l, u), Y). X  scaleR2 l u Y)"
  unfolding scaleR2_rep_coll_def
  apply (refine_vcg FORWEAK_mono_rule[where I="λXs ((l, u), Y). Xs  scaleR2 l u Y"])
  subgoal by (auto intro: scaleR2_subset)
  subgoal
    apply clarsimp
    apply safe
    subgoal by (auto elim: scaleR2_subset)
    subgoal
      apply (rule set_rev_mp, assumption)
      apply (rule order_trans)
       apply (rule Union_upper, assumption)
      apply (rule order_trans, assumption)
      apply (rule subsetI)
      apply (erule scaleR2_subset)
      by (auto )
    done
  done

lemma split_spec_param1e[le, refine_vcg]: "split_spec_param1e X  SPEC (λ(A, B). X  A  B)"
  unfolding split_spec_param1e_def
  apply (refine_vcg)
  apply clarsimp
    apply (thin_tac "_  {}")
  apply (auto simp: scaleR2_def vimage_def image_def)
  apply (rule exI, rule conjI, assumption, rule conjI, assumption)
  apply (auto simp: split_beta')
  apply (drule_tac x = x in spec)
  apply auto
  by (metis (no_types, lifting) UnE prod.sel(1) prod.sel(2) subset_eq)

lemma reduce_spec1[le, refine_vcg]: "reduce_spec1 ro X  SPEC (λR. X  R)"
  unfolding reduce_spec1_def
  by refine_vcg auto

lemma reduce_spec1e[le, refine_vcg]: "reduce_spec1e ro X  SPEC (λR. X  R)"
  unfolding reduce_spec1e_def
  by refine_vcg (auto simp: scaleR2_def image_def vimage_def, force)

lemma split_under_threshold[le, refine_vcg]:
  "split_under_threshold ro th X  SPEC (λR. X  R)"
  unfolding split_under_threshold_def autoref_tag_defs
  by (refine_vcg) auto

lemma step_split[le, refine_vcg]:
  "wd TYPE((real, 'n::enum) vec)  step_split ro (X::'n eucl1 set)  SPEC (λY. X  Y  fst ` Y  Csafe)"
  unfolding step_split_def
  by (refine_vcg refine_vcg) auto

lemma tolerate_error_SPEC[THEN order_trans, refine_vcg]:
  "tolerate_error Y E  SPEC (λb. True)"
  unfolding tolerate_error_def
  by refine_vcg

lemma flowpipe_scaleR2I: "flowpipe (scaleR2 x1 x2 bc) x1a x1a (fst ` aca × UNIV) (scaleR2 x1 x2 bca)"
  if "flowpipe (bc) x1a x1a (fst ` aca × UNIV) (bca)"
  using that
  apply (auto simp: flowpipe_def scaleR2_def)
  apply (drule bspec, assumption)
  apply (auto simp: image_def vimage_def )
  apply (rule exI, rule conjI, assumption, rule conjI, assumption)
  apply (rule bexI) prefer 2 apply assumption
  by (auto simp: scaleR_blinfun_compose_right)

lemma choose_step1e_flowpipe[le, refine_vcg]:
  assumes vwd[refine_vcg]: "wd TYPE('n::enum rvec)"
  shows "choose_step1e (X0::'n eucl1 set) h  SPEC (λ(h', _, RES_ivl, RES::'n eucl1 set).
      0 < h'  h'  h  flowpipe X0 h' h' (RES_ivl × UNIV) RES)"
  unfolding choose_step1e_def
  apply (refine_vcg)
    apply (auto intro: flowpipe_scaleR2I)
  apply (erule contrapos_np)
  apply (auto intro!: flowpipe_scaleR2I)
  apply (rule flowpipe_subset)
         apply assumption
        apply (auto dest!: flowpipe_safeD)
  done

lemma width_spec_appr1[THEN order_trans, refine_vcg]: "width_spec_appr1 X  SPEC (λ_. True)"
  unfolding width_spec_appr1_def
  by refine_vcg

lemma tolerate_error1_SPEC[THEN order_trans, refine_vcg]:
  "tolerate_error1 Y E  SPEC (λb. True)"
  unfolding tolerate_error1_def
  by refine_vcg

lemma
  step_adapt_time[le, refine_vcg]:
  assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
  shows "step_adapt_time (X::'n eucl1 set) h  SPEC (λ(t, CX, X1, h). flowpipe X t t (CX × UNIV) X1)"
  unfolding step_adapt_time_def  autoref_tag_defs
  apply (refine_vcg refine_vcg, clarsimp)
  apply (auto simp: flowpipe_def)
  apply force
  done

lemma
  resolve_step[le, refine_vcg]:
  assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
  shows "resolve_step roptns (X::'n::enum eucl1 set) h  SPEC (λ(_, CX, X1, _).
    flowsto X {0..} (CX × UNIV) X1  X  X1  CX × UNIV  X1  CX × UNIV  Csafe × UNIV)"
  unfolding resolve_step_def  autoref_tag_defs
  apply (refine_vcg refine_vcg)
  subgoal by (rule flowsto_self) auto
  subgoal by auto
  subgoal by auto
  subgoal
    apply clarsimp
    apply (frule flowpipe_imp_flowsto_nonneg)
    apply (rule flowsto_subset, assumption)
    by auto
  subgoal
    by (auto dest: flowpipe_source_subset)
  subgoal
    by (auto dest!: flowpipe_safeD)
  done

lemma pre_intersection_step[THEN order_trans, refine_vcg]:
  "pre_intersection_step ro (X::'n eucl1 set) h  SPEC (λ(X', CX, G). X  X'  G  X  X'  G  CX × UNIV)"
  if [refine_vcg]: "wd TYPE('n::enum rvec)"
  unfolding pre_intersection_step_def autoref_tag_defs
  by (refine_vcg) auto

lemma [THEN order_trans, refine_vcg]: "select_with_inter ci a  SPEC (λ_. True)"
  unfolding select_with_inter_def
  by (refine_vcg FORWEAK_mono_rule[where I="λ_ _. True"])

lemmas [refine_vcg del] = scaleR2_rep_of_coll

lemma fst_scaleR2_image[simp]: "ad  ereal r  ereal r  bd  fst ` scaleR2 ad bd be = fst ` be"
  by (cases ad; cases bd; force simp: scaleR2_def image_image split_beta' vimage_def)

lemma scaleR2_rep_of_coll2[le, refine_vcg]:
  "scaleR2_rep_coll X  SPEC (λ((l, u), Y). X  scaleR2 l u Y  fst ` X = fst ` Y)"
  unfolding scaleR2_rep_coll_def
  supply [simp del] = mem_scaleR2_union
  apply (refine_vcg FORWEAK_mono_rule[where I="λXs ((l, u), Y).
      Xs  scaleR2 l u Y  fst ` Xs  fst ` Y  fst ` Y  fst ` X"])
        apply (auto intro: scaleR2_subset)
  subgoal by (auto simp: scaleR2_def)
  subgoal by (auto simp: scaleR2_def image_def vimage_def, fastforce)
  subgoal
    apply (rule scaleR2_subset)
       apply (rule subsetD)
        apply assumption
       apply auto
    done
  subgoal by force
  subgoal for a b c d e f g h i j k l
    apply (rule scaleR2_subset)
       apply (rule subsetD)
        apply assumption
    by auto
  subgoal by (auto simp: scaleR2_def)
  subgoal by (auto simp: scaleR2_def)
  subgoal by (auto simp: scaleR2_def image_def vimage_def, fastforce)
  done

lemma reach_cont[le, refine_vcg]:
  assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
  shows "reach_cont roptns guards (X::'n eucl1 set)  SPEC (λ(CX, G).
    G  (CX × UNIV)  (Csafe - guards) × UNIV 
    X  G  CX × UNIV 
    flowsto X {0..} (CX × UNIV) G)"
  using [[simproc del: defined_all]]
  unfolding reach_cont_def autoref_tag_defs
  apply (refine_vcg, clarsimp_all simp add: cancel_times_UNIV_subset)
  subgoal by (rule flowsto_self) auto
  subgoal by (force simp: scaleR2_def)
  subgoal by (fastforce simp: scaleR2_def vimage_def image_def)
  subgoal premises prems for _ _ _ _ _ _ _ g
    using flowsto X _ _ (g  _  _)  flowsto g _ _ _
    apply (rule flowsto_stepI)
    using prems
    by auto
  subgoal
    apply safe
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    done
  subgoal by auto
  subgoal
    by (rule flowsto_subset, assumption) auto
  subgoal
    apply safe
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by fastforce
    subgoal by auto
    subgoal by auto
    subgoal
      by (metis (mono_tags, lifting) Diff_eq_empty_iff Diff_iff IntI)
    done
  subgoal
    apply safe
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    subgoal by auto
    done
  subgoal by auto
  done

lemma reach_cont_par[le, refine_vcg]:
  assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
  shows "reach_cont_par roptns guards (X::'n eucl1 set)  SPEC (λ(CX, G).
    G  (CX × UNIV)  (Csafe - guards) × UNIV 
    X  G  CX × UNIV 
    flowsto X {0..} (CX × UNIV) G)"
  unfolding reach_cont_par_def
  apply refine_vcg
    apply auto
    apply force
    apply force
    apply force
     apply force
  subgoal
    apply (rule bexI)
     prefer 2 apply assumption
    by auto
  subgoal
    apply (rule bexI)
     prefer 2 apply assumption
    by auto
  subgoal for R
    apply (rule flowsto_source_Union)
    apply (drule bspec, assumption)
    apply auto
    apply (rule flowsto_subset, assumption)
       apply auto
    done
  done

lemma subset_iplane_coll[THEN order_trans, refine_vcg]:
  "subset_iplane_coll x ics  SPEC (λb. b  x  ics)"
  unfolding subset_iplane_coll_def
  apply refine_vcg
  subgoal for X icss
    by (refine_vcg FORWEAK_mono_rule[where I="λic b. b  X  (icss)"]) auto
  done

lemma subsets_iplane_coll[THEN order_trans, refine_vcg]:
  "subsets_iplane_coll x ics  SPEC (λb. b  x  ics)"
  unfolding subsets_iplane_coll_def
  by (refine_vcg FORWEAK_mono_rule[where I="λx b. (b  x  ics)"]) auto

lemma symstart_coll[THEN order_trans, refine_vcg]:
  assumes [refine_vcg]: "wd (TYPE('n::enum rvec))"
  assumes [le, refine_vcg]:
    "X0. X0  Csafe × UNIV  symstart X0  SPEC (λ(CX, X). flowsto (X0 - trap × UNIV) {0..} (CX × UNIV) (X))"
  shows "symstart_coll symstart X0  SPEC (λ(CX, X). flowsto ((X0::'n eucl1 set) - trap × UNIV) {0..} (CX × UNIV) X)"
  unfolding symstart_coll_def autoref_tag_defs
  apply (refine_vcg FORWEAK_mono_rule[where I="λX (CY, Y). flowsto (X - trap × UNIV) {0..} (CY × UNIV) Y"], clarsimp_all)
  subgoal by force
  subgoal for a b c d e by (rule flowsto_subset, assumption) auto
  subgoal by force
  subgoal for a b c d e f g
    unfolding Un_Diff
    apply (rule flowsto_source_unionI)
    subgoal by (rule flowsto_subset, assumption) auto
    subgoal by (rule flowsto_subset, assumption) auto
    done
  done

lemma reach_cont_symstart[le, refine_vcg]:
  assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
  assumes [le, refine_vcg]: "X0. X0  Csafe × UNIV  symstart X0  SPEC (λ(CX, X). flowsto (X0 - trap × UNIV) {0..} (CX × UNIV) (X))"
  shows "reach_cont_symstart roptns symstart guards (X::'n eucl1 set)  SPEC (λ(CX, G).
    G  (CX × UNIV)  (Csafe - guards) × UNIV 
    X  CX × UNIV 
    G  CX × UNIV 
    flowsto (X - trap × UNIV) {0..} (CX × UNIV) (G))"
  unfolding reach_cont_symstart_def autoref_tag_defs
  apply (refine_vcg, clarsimp_all)
  subgoal by (auto simp: times_subset_iff)
  subgoal by auto
  subgoal by auto
  subgoal for a b c d e f g
    apply (rule flowsto_stepI[OF _ _ order_refl])
         apply assumption
    by assumption auto
  done

lemma reach_conts[le, refine_vcg]:
  assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
  assumes [refine_vcg]: "X0. X0  Csafe × UNIV  symstart X0  SPEC (λ(CX, X). flowsto (X0 - trap × UNIV) {0..} (CX × UNIV) X)"
  shows "reach_conts roptns symstart trap guards (X::'n eucl1 set)  SPEC (λ(CX, IGs, X0).
    (snd ` IGs)  (CX × UNIV)  (Csafe - guards) × UNIV 
    X  CX × UNIV 
    (snd ` IGs)  CX × UNIV 
    (fst ` IGs)  guards 
    X = (X0 ` (snd ` IGs)) 
    ((I, G)  IGs. flowsto (X0 G - trap × UNIV) {0..} (CX × UNIV) G))"
  unfolding reach_conts_def autoref_tag_defs
  apply (refine_vcg, clarsimp_all)
  subgoal for a b
    apply (erule flowsto_Diff_to_Union_funE)
    apply (force simp: split_beta')
    subgoal for f
      apply (rule exI[where x=f])
      by (auto simp: split_beta')
    done
  subgoal by (auto)
  subgoal by (auto)
  subgoal by (auto)
  done

lemma leaves_halfspace[le, refine_vcg]:
  assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
  shows "leaves_halfspace S (X::'n::enum rvec set) 
    SPEC (λb. case b of None  S = UNIV
      | Some sctn 
        (S = below_halfspace sctn  X  plane_of sctn  (x  X. ode x  normal sctn < 0)))"
  unfolding leaves_halfspace_def autoref_tag_defs op_set_to_list_def
  apply (refine_vcg, clarsimp_all)
  subgoal by (force simp add: halfspace_simps plane_of_def)
  done

lemma poincare_start_on[le, refine_vcg]:
  assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
  shows "poincare_start_on guards sctn (X0::'n eucl1 set)  SPEC (λ(X1S, CX1S).
    fst ` (X1S  (CX1S × UNIV))  Csafe 
    fst ` X1S  sbelow_halfspace sctn 
    fst ` (X1S  (CX1S × UNIV))  guards = {} 
    (X0  (CX1S × UNIV)) 
    ((x, d)  CX1S × UNIV. ode x  normal sctn < 0) 
    flowsto X0 pos_reals ((CX1S × UNIV)  (sbelow_halfspace sctn × UNIV)) X1S)"
  unfolding poincare_start_on_def autoref_tag_defs
  apply refine_vcg
  apply (rule FORWEAK_mono_rule[where I="λX0S (X1S, CX1S).
      flowsto (X0S) pos_reals ((CX1S × UNIV)  sbelow_halfspace sctn × UNIV) X1S 
        fst ` (X1S  (CX1S × UNIV))  Csafe 
        (X0S)  X0 
        (X0S)  (CX1S × UNIV) 
        fst ` (X1S  (CX1S × UNIV))  guards = {} 
        ((x, d)  (CX1S × UNIV). ode x  normal sctn < 0) 
        fst ` X1S   sbelow_halfspace sctn"])
  subgoal by (refine_vcg)
  subgoal for A B
    apply (refine_vcg)
    subgoal
      apply (auto simp: dest!: flowpipe_imp_flowsto)
      apply (rule flowsto_subset)
          apply (rule flowsto_stays_sbelow[where sctn=sctn])
            apply (rule flowsto_subset) apply assumption
               apply (rule order_refl)
              apply force
             apply (rule order_refl)
            apply (rule order_refl)
           apply (auto simp: halfspace_simps)
      apply (rule le_less_trans)
       prefer 2 apply assumption
      apply (drule bspec)
       apply (rule subsetD, assumption)
       prefer 2 apply assumption
      apply auto
      done
    subgoal by auto
    subgoal by force
    subgoal by (auto simp: dest!: flowpipe_source_subset)
    subgoal by auto
    subgoal
      apply (auto simp: halfspace_simps subset_iff)
      apply (rule le_less_trans[rotated], assumption)
      by fastforce
    done
  subgoal by (auto intro: flowsto_subset) force
  subgoal for a b c d
    using assms
    apply (refine_vcg, clarsimp_all)
    subgoal for e f g h i j k l m n
      apply (rule flowsto_source_unionI)
      subgoal
        apply (drule flowpipe_imp_flowsto, assumption)
        apply (rule flowsto_subset[OF flowsto_stays_sbelow[where sctn=sctn] order_refl])
             apply (rule flowsto_subset[OF _ order_refl], assumption)
               apply force
              apply (rule order_refl)
             apply (rule order_refl)
            apply (auto simp: halfspace_simps)
        apply (rule le_less_trans)
         prefer 2 apply assumption
        apply (drule bspec)
         apply (rule subsetD, assumption)
         prefer 2 apply assumption
        apply auto
        done
      by (auto intro!: flowsto_source_unionI dest!: flowpipe_imp_flowsto intro: flowsto_subset[OF _ order_refl])
    subgoal
      apply (auto simp: subset_iff)
      apply (auto simp: image_Un)
      done
    subgoal by auto
    subgoal by (auto dest!: flowpipe_source_subset)
    subgoal by auto
    subgoal
      apply (auto simp: halfspace_simps subset_iff)
      apply (rule le_less_trans[rotated], assumption)
      by fastforce
    subgoal by auto
    done
  subgoal by auto
  done

lemma op_inter_fst_coll[le, refine_vcg]: "op_inter_fst_coll X Y  SPEC (λR. R = X  Y × UNIV)"
  unfolding op_inter_fst_coll_def
  by (refine_vcg FORWEAK_mono_rule[where I="λXs R. Xs  Y × UNIV  R  R  X  Y × UNIV"])
    auto

lemma scaleRe_ivl_coll_spec[le, refine_vcg]: "scaleRe_ivl_coll_spec l u X  SPEC (λY. Y = scaleR2 l u X)"
  unfolding scaleRe_ivl_coll_spec_def
  apply (refine_vcg FORWEAK_mono_rule[where I="λXs R. scaleR2 l u (Xs)  R  R  scaleR2 l u X"])
      apply (auto simp: intro: scaleR2_subset)
  subgoal
    by (force simp: intro: scaleR2_subset)
  done

lemma do_intersection_spec_scaleR2I:
  "do_intersection_spec UNIV sctns ivl sctn (scaleR2 x1 x2 baa) (scaleR2 x1 x2 aca, x1b)"
  if "do_intersection_spec UNIV sctns ivl sctn (baa) (aca, x1b)"
  using that
  by (auto simp: do_intersection_spec_def intro!: poincare_mapsto_scaleR2I)
     (auto simp: scaleR2_def image_def vimage_def)

lemma do_intersection_core[refine_vcg, le]:
  assumes wd[refine_vcg]: "wd (TYPE('n::enum rvec))"
  shows "do_intersection_core sctns ivl sctn (X::'n eucl1 set) 
    SPEC (λ(P1, P2, CX, X0s).
      do_intersection_spec UNIV sctns ivl sctn (X - X0s) (P1, CX) 
      do_intersection_spec UNIV sctns ivl sctn (X - X0s) (P2, CX)
       fst ` (X - X0s)  CX
       X0s  X)"
  unfolding do_intersection_core_def autoref_tag_defs
  apply (refine_vcg assms, clarsimp_all)
  subgoal by (rule do_intersection_spec_scaleR2I) (auto simp: do_intersection_spec_def intro!: )
  subgoal by (rule do_intersection_spec_scaleR2I) (auto simp: do_intersection_spec_def intro!: )
  subgoal by (fastforce simp: scaleR2_def)
  subgoal by (auto simp: do_intersection_spec_def)
  subgoal by (auto simp: do_intersection_spec_def)
  done

lemma do_intersection_spec_Union:
  "do_intersection_spec S sctns ivl sctn (X) A"
  if "x. x  X  do_intersection_spec S sctns ivl sctn x A"
    "X  {}"
  using that(2)
  unfolding do_intersection_spec_def
  apply clarsimp
  apply safe
  subgoal by (rule poincare_mapsto_Union) (auto simp: do_intersection_spec_def dest!: that(1))
  subgoal by (auto simp: do_intersection_spec_def dest!: that(1))
  subgoal by (auto simp: do_intersection_spec_def dest!: that(1))
  subgoal by (fastforce simp: do_intersection_spec_def dest!: that(1))
  subgoal by (fastforce simp: do_intersection_spec_def dest!: that(1))
  subgoal by (fastforce simp: do_intersection_spec_def dest!: that(1))
  subgoal by (force simp: do_intersection_spec_def dest!: that(1))
  subgoal by (auto simp: do_intersection_spec_def dest!: that(1))
  subgoal by (fastforce simp: do_intersection_spec_def dest!: that(1))
  subgoal by (fastforce simp: do_intersection_spec_def dest!: that(1))
  done

lemma do_intersection_spec_subset2:
  "do_intersection_spec S p ivl sctn X1 (ab, CY)  CY  CX  CX  Csafe 
    CX  p = {}  CX  ivl  plane_of sctn = {}  X0  X1 
  do_intersection_spec S p ivl sctn X0 (ab, CX)"
  by (auto simp: do_intersection_spec_def intro: poincare_mapsto_subset)

lemma do_intersection_spec_Union3:
  "do_intersection_spec S osctns ivl csctns (xX. a x) ((xX. b x), (xX. c x))"
  if  "finite X" "X  {}" "x. x  X  do_intersection_spec S osctns ivl csctns (a x) (b x, c x)"
  using that
proof induction
  case empty
  then show ?