Theory Concrete_Rigorous_Numerics

theory Concrete_Rigorous_Numerics
  imports
    Abstract_Rigorous_Numerics
begin

context includes autoref_syntax begin

lemma [autoref_rules]:
  "(slp_of_fas, slp_of_fas) ∈ fas_rel → slp_rel"
  "(Norm, Norm) ∈ fas_rel → Id"
  by auto

lemma [autoref_rules]: "(norm2_slp, norm2_slp) ∈ nat_rel → Id"
  by auto

lemma [autoref_rules]:
  "(floatarith.Var, floatarith.Var) ∈ nat_rel → Id"
  "(slp_of_fas, slp_of_fas) ∈ ⟨Id⟩list_rel → ⟨Id⟩list_rel"
  "(fold_const_fa, fold_const_fa) ∈ Id → Id"
  "(open_form, open_form) ∈ Id → bool_rel"
  "(max_Var_floatariths, max_Var_floatariths) ∈ ⟨Id⟩list_rel → nat_rel"
  "(max_Var_form, max_Var_form) ∈ Id → nat_rel"
  "(length, length) ∈ ⟨A⟩list_rel → nat_rel"
  by (auto simp: list_rel_imp_same_length)

end

context approximate_sets begin

lemma prod_rel_relcomp_distr: "(R ×⇩r S) O (T ×⇩r U) = (R O T) ×⇩r (S O U)"
  by (auto simp: prod_rel_def)

lemma appr_relp_comp: "appr_rell O ⟨lv_rel⟩set_rel ⊆ appr_rel"
  "appr_rel ⊆ appr_rell O ⟨lv_rel⟩set_rel"
  by (auto simp: appr_rel_def)

lemma rnv_rel_comp2:
  "rnv_rel ⊆ rnv_rel O rnv_rel"
  "rnv_rel O rnv_rel ⊆ rnv_rel"
  by auto

lemma rl_comp_lv: "rl_rel O lv_rel ⊆ lv_rel"
  "lv_rel ⊆ rl_rel O lv_rel"
  by auto

lemmas rel_lemmas =
  fun_rel_comp_dist[THEN order_trans]
  fun_rel_mono nres_rel_comp[THEN eq_refl, THEN order_trans]
  nres_rel_mono prod_rel_mono prod_rel_relcomp_distr[THEN eq_refl, THEN order_trans]
  appr_relp_comp
  rnv_rel_comp2
  rl_comp_lv
  sctn_rel

lemma width_spec_width_spec: "(width_spec, width_spec) ∈ ⟨lv_rel⟩set_rel → ⟨rnv_rel⟩nres_rel"
  by (auto simp: width_spec_def nres_relI)

lemma [autoref_itype]:
  "width_spec ::⇩i A →⇩i ⟨i_rnv⟩⇩ii_nres"
  "Inf_spec ::⇩i A →⇩i ⟨B⟩⇩ii_nres"
  "Sup_spec ::⇩i A →⇩i ⟨B⟩⇩ii_nres"
  "inter_sctn_spec ::⇩i A →⇩i ⟨B⟩⇩ii_sctn →⇩i ⟨C⟩⇩ii_nres"
  "split_spec ::⇩i A →⇩i ⟨⟨B, B⟩⇩ii_prod⟩⇩ii_nres"
  "split_spec_param ::⇩i i_nat →⇩i A →⇩i ⟨⟨B, B⟩⇩ii_prod⟩⇩ii_nres"
  "Inf_inner ::⇩i A →⇩i B →⇩i ⟨i_rnv⟩⇩ii_nres"
  "Sup_inner ::⇩i A →⇩i B →⇩i ⟨i_rnv⟩⇩ii_nres"
  by auto

lemma transfer_operations[unfolded comps, autoref_rules]:
  "SIDE_PRECOND (list_all2 (≤) xrs yrs) ⟹
    (xri, xrs) ∈ ⟨rnv_rel⟩list_rel ⟹
    (yri, yrs) ∈ ⟨rnv_rel⟩list_rel ⟹
    (appr_of_ivl ops xri yri, lv_ivl $ xrs $ yrs) ∈ appr_rell"
  "(product_appr ops, product_listset) ∈ appr_rell → appr_rell → appr_rell"
  "(msum_appr ops, (+)) ∈ appr_rel → appr_rel → appr_rel"
  "(RETURN o inf_of_appr ops optns, Inf_spec) ∈ appr_rel → ⟨lv_rel⟩nres_rel"
  "(RETURN o sup_of_appr ops optns, Sup_spec) ∈ appr_rel → ⟨lv_rel⟩nres_rel"
  "(RETURN o2 split_appr ops, split_spec_param) ∈ nat_rel → appr_rel → ⟨appr_rel ×⇩r appr_rel⟩nres_rel"
  "(RETURN o2 appr_inf_inner ops optns, Inf_inner) ∈ appr_rel → lv_rel → ⟨rnv_rel⟩nres_rel"
  "(RETURN o2 appr_sup_inner ops optns, Sup_inner) ∈ appr_rel → lv_rel → ⟨rnv_rel⟩nres_rel"
  "(nres_of o2 inter_appr_plane ops optns, inter_sctn_spec) ∈ appr_rel → ⟨lv_rel⟩sctn_rel → ⟨appr_rel⟩nres_rel"
  "(RETURN o2 reduce_appr ops optns, reduce_spec) ∈ reduce_argument_rel TYPE('b) → appr_rel → ⟨appr_rel⟩nres_rel"
  "(RETURN o width_appr ops optns, width_spec) ∈ appr_rel → ⟨rnv_rel⟩nres_rel"
  "(nres_of o3 approx_slp_dres ops optns, approx_slp_spec fas) ∈ nat_rel → slp_rel → appr_rell → ⟨⟨appr_rell⟩option_rel⟩nres_rel"
  subgoal premises prems using transfer_operations_rl(1)[OF prems] by simp
  subgoal premises prems using transfer_operations_rl(2)[OF prems] by simp
  subgoal premises prems using transfer_operations_rl(3)[OF prems]
    unfolding appr_rel_def set_plus_def
    apply auto
    apply (drule fun_relD, assumption, drule fun_relD, assumption, rule relcompI, assumption)
    apply (auto simp: set_rel_sv[OF lv_rel_sv])
      apply (rule ImageI)
       apply (rule lv_rel_add[param_fo], assumption, assumption)
      apply force
    subgoal for a b c d e f g
      apply (rule bexI[where x="eucl_of_list f"])
       apply (rule bexI[where x="eucl_of_list g"])
      using lv_rel_add[param_fo, of f "eucl_of_list f", of g "eucl_of_list g::'a"]
      by (auto simp: lv_rel_def br_def subset_iff)
    subgoal
      by (auto simp: lv_rel_def br_def subset_iff)
    done
  subgoal apply (auto simp: appr_rel_def)
  proof goal_cases
    case (1 x y z)
    from transfer_operations_rl(4)[OF 1(1) refl]
    have Is: "(RETURN (inf_of_appr ops optns x), Inf_specs (length x) y) ∈ ⟨rl_rel⟩nres_rel"
      by auto
    from 1 have "length x = DIM('c)"
      unfolding set_rel_sv[OF lv_rel_sv]
      by (auto simp: lv_rel_def br_def appr_rell_internal length_set_of_appr subset_iff)
    from relcompI[OF _ Inf_specs_Inf_spec[param_fo], OF Is ‹length x = _› 1(2)]
    have "(RETURN (inf_of_appr ops optns x), Inf_spec z) ∈ ⟨rl_rel⟩nres_rel O ⟨lv_rel⟩nres_rel"
      by simp
    then show ?case
      by (simp add: nres_rel_comp)
  qed
  subgoal apply (auto simp: appr_rel_def)
  proof goal_cases
    case (1 x y z)
    from transfer_operations_rl(5)[OF 1(1) refl]
    have Is: "(RETURN (sup_of_appr ops optns x), Sup_specs (length x) y) ∈ ⟨rl_rel⟩nres_rel"
      by auto
    from 1 have "length x = DIM('d)"
      unfolding set_rel_sv[OF lv_rel_sv]
      by (auto simp: lv_rel_def br_def appr_rell_internal length_set_of_appr subset_iff)
    from relcompI[OF _ Sup_specs_Sup_spec[param_fo], OF Is ‹length x = _› 1(2)]
    have "(RETURN (sup_of_appr ops optns x), Sup_spec z) ∈ ⟨rl_rel⟩nres_rel O ⟨lv_rel⟩nres_rel"
      by simp
    then show ?case
      by (simp add: nres_rel_comp)
  qed
  subgoal apply (auto simp: appr_rel_def)
  proof goal_cases
    case (1 n x y z)
    from transfer_operations_rl(6)[OF _ 1(1) refl]
    have Is: "(RETURN (split_appr ops n x), split_spec_params (length x) n y) ∈ ⟨appr_rell ×⇩r appr_rell⟩nres_rel"
      by auto
    from 1 have "length x = DIM('e)"
      unfolding set_rel_sv[OF lv_rel_sv]
      by (auto simp: lv_rel_def br_def appr_rell_internal length_set_of_appr subset_iff)
    from relcompI[OF _ split_spec_params_split_spec_param[param_fo], OF Is ‹length x = _› IdI 1(2)]
    have "(RETURN (split_appr ops n x), split_spec_param n z) ∈
        ⟨appr_rell ×⇩r appr_rell⟩nres_rel O ⟨⟨lv_rel⟩set_rel ×⇩r ⟨lv_rel⟩set_rel⟩nres_rel"
      by simp
    then show ?case
      by (simp add: nres_rel_comp prod_rel_relcomp_distr comps)
  qed
  subgoal
    by (intro relcompI[OF transfer_operations_rl(7) Inf_inners_Inf_inner, THEN rev_subsetD] rel_lemmas)
  subgoal
    by (intro relcompI[OF transfer_operations_rl(8) Sup_inners_Sup_inner, THEN rev_subsetD] rel_lemmas)
  subgoal apply (auto simp: appr_rel_def)
  proof goal_cases
    case (1 r s x y z)
    from 1 have lens: "length (normal r) = length x"
      apply (cases r; cases s)
      apply (auto simp: sctn_rel_def)
      unfolding set_rel_sv[OF lv_rel_sv]
      by (auto simp: lv_rel_def br_def appr_rell_internal length_set_of_appr subset_iff)
    have poslen: "0 < length x"
      using 1
      apply (cases r; cases s)
      apply (auto simp: sctn_rel_def)
      by (auto simp: lv_rel_def set_rel_def br_def appr_rell_internal)
    have rr: "(r, r) ∈ ⟨rl_rel⟩sctn_rel"
      by (cases r) (auto simp: sctn_rel_def)
    from transfer_operations_rl(9)[OF 1(2) refl lens poslen rr]
    have Is: "(nres_of (inter_appr_plane ops optns x r), inter_sctn_specs (length x) y r) ∈ ⟨appr_rell⟩nres_rel"
      by (auto dest!: fun_relD)
    from 1 have "length x = DIM('h)"
      unfolding set_rel_sv[OF lv_rel_sv]
      by (auto simp: lv_rel_def br_def appr_rell_internal length_set_of_appr subset_iff)
    from relcompI[OF _ inter_sctn_specs_inter_sctn_spec[param_fo], OF Is, OF ‹length x = _› 1(3) 1(1)]
    have "(nres_of (inter_appr_plane ops optns x r), inter_sctn_spec z s) ∈ ⟨appr_rell⟩nres_rel O ⟨⟨lv_rel⟩set_rel⟩nres_rel"
      by simp
    then show ?case
      by (simp add: nres_rel_comp prod_rel_relcomp_distr comps)
  qed
  subgoal apply (auto simp: appr_rel_def)
  proof goal_cases
    case (1 ro x y z)
    from transfer_operations_rl(10)[OF 1(2) refl 1(1)]
    have Is: "(RETURN (reduce_appr ops optns ro x), reduce_specs (length x) () y) ∈ ⟨appr_rell⟩nres_rel"
      by auto
    from 1 have "length x = DIM('i)"
      unfolding set_rel_sv[OF lv_rel_sv]
      by (auto simp: lv_rel_def br_def appr_rell_internal length_set_of_appr subset_iff)
    from relcompI[OF _ reduce_specs_reduce_spec[param_fo], OF Is ‹length x = _› IdI 1(3)]
    have "(RETURN (reduce_appr ops optns ro x), reduce_spec () z) ∈ ⟨appr_rell⟩nres_rel O ⟨⟨lv_rel⟩set_rel⟩nres_rel"
      by simp
    then show ?case
      by (simp add: nres_rel_comp prod_rel_relcomp_distr comps)
  qed
  subgoal
    by (intro relcompI[OF transfer_operations_rl(11) width_spec_width_spec, THEN rev_subsetD] rel_lemmas)
  subgoal using transfer_operations_rl(12) by auto
  done

lemma approx_slp_spec[autoref_op_pat_def]: "approx_slp_spec fas ≡ OP (approx_slp_spec fas)"
  by auto

lemma
  concat_appr:
  assumes "(xsi, xs) ∈ ⟨appr_rell⟩list_rel"
  shows "(concat_appr ops xsi, concat ` listset xs) ∈ appr_rell"
  using assms
  apply (auto simp: appr_rell_internal br_def)
  subgoal premises prems for xi
  proof -
    have "length xi = length xs" "length xs = length xsi"
      using prems
       by (auto simp: list_rel_def list_all2_iff length_listset)
    then show ?thesis using prems
    proof (induction rule: list_induct3)
      case Nil
      then show ?case by simp
    next
      case (Cons x xs y ys z zs)
      have "(z, set_of_appr z) ∈ appr_rell"
        "(concat_appr ops zs, set_of_appr (concat_appr ops zs)) ∈ appr_rell"
        by (auto simp: appr_rell_internal br_def)
      from transfer_operations(2)[param_fo, OF this]
      have *: "set_of_appr (product_appr ops z (concat_appr ops zs)) =
        (λ(x, y). x @ y) ` (set_of_appr z × set_of_appr (concat_appr ops zs))"
        by (simp add: appr_rell_internal br_def product_listset_def)
      show ?case
        using Cons
        apply (auto simp: appr_rell_internal *)
        apply (rule image_eqI[where x="(x, concat xs)"])
         by (auto simp: set_Cons_def)
     qed
   qed
   subgoal premises prems for z
   proof -
     have "length xsi = length xs"
       using prems
       by (auto simp: list_rel_def list_all2_iff)
     then show ?thesis
       using prems
     proof (induction arbitrary: z rule: list_induct2 )
       case Nil
       then show ?case by simp
     next
       case (Cons x xs y ys)
       have "(x, set_of_appr x) ∈ appr_rell" "(concat_appr ops xs, set_of_appr (concat_appr ops xs)) ∈ appr_rell"
         by (auto simp: appr_rell_internal br_def)
       from transfer_operations(2)[param_fo, OF this]
       have *: "set_of_appr (product_appr ops x (concat_appr ops xs)) =
          product_listset (set_of_appr x) (set_of_appr (concat_appr ops xs))"
         by (auto simp: appr_rell_internal br_def)
       show ?case using Cons
         apply (auto simp: * product_listset_def list_rel_def set_Cons_def)
         subgoal premises prems for a b
           using prems(2)[OF prems(7)] prems(6)
           apply (auto )
           subgoal for ya
           apply (rule image_eqI[where x="a#ya"])
             by (auto simp: set_Cons_def)
           done
         done
     qed
   qed
   done

lemma op_concat_listset_autoref[autoref_rules]:
  "(concat_appr ops, op_concat_listset) ∈ ⟨appr_rell⟩list_rel → appr_rell"
  using concat_appr by force

lemma transfer_operations1[autoref_rules]:
  assumes "SIDE_PRECOND (x ≤ y)" "(xi, x) ∈ lv_rel" "(yi, y) ∈ lv_rel"
  shows "(appr_of_ivl ops xi yi, op_atLeastAtMost_appr $ x $ y) ∈ appr_rel"
proof -
  have "(appr_of_ivl ops xi yi, lv_ivl (list_of_eucl x) (list_of_eucl y)) ∈ appr_rell"
    apply (rule transfer_operations_rl[unfolded autoref_tag_defs])
    using assms lv_rel_le[param_fo, of xi x yi y]
    by (auto simp: lv_rel_def br_def)
  then have "(appr_of_ivl ops xi yi, eucl_of_list ` lv_ivl (list_of_eucl x) (list_of_eucl y)::'a set) ∈ appr_rel"
    unfolding appr_rel_br
    using assms[unfolded lv_rel_def]
    using lv_rel_le[param_fo, of xi x yi y]
    by (auto simp: appr_rell_internal br_def appr_rel_br)
       (auto simp: lv_rel_def br_def)
  also have "eucl_of_list ` lv_ivl (list_of_eucl x) (list_of_eucl y) = {x .. y}"
    by (subst eucl_of_list_image_lv_ivl) auto
  finally show ?thesis by simp
qed

lemma appr_of_ivl_point_appr_rel:
  "(appr_of_ivl ops x x, {eucl_of_list x::'a::executable_euclidean_space}) ∈ appr_rel"
  if "length x = DIM('a)"
  using transfer_operations1[OF _ lv_relI lv_relI, OF _ that that]
  by auto

lemmas [autoref_post_simps] = concat.simps append_Nil2 append.simps

lemma is_empty_appr_rel[autoref_rules]:
  "(λ_. False, is_empty) ∈ appr_rel → bool_rel"
  by (auto simp: appr_rel_br br_def)

lemma appr_rel_nonempty: "(x, X) ∈ appr_rel ⟹ X ≠ {}"
  by (auto simp: appr_rel_br br_def)

lemma [autoref_rules]: "(ops, ops) ∈ Id"
  by simp

lemma single_valued_appr_rel[relator_props]:
  "single_valued (appr_rel)"
  by (auto simp: appr_rel_br)

schematic_goal ivl_rep_of_set_impl:
  fixes X::"'a::executable_euclidean_space set"
  assumes [autoref_rules]: "(ai, X) ∈ appr_rel"
  shows "(RETURN (?f::?'r), op_ivl_rep_of_set X) ∈ ?R"
  unfolding op_ivl_rep_of_set_def including art by (autoref_monadic (plain))
concrete_definition ivl_rep_of_set_impl for  ai uses ivl_rep_of_set_impl
lemma ivl_rep_of_set_autoref[autoref_rules]:
  shows "(λx. RETURN (ivl_rep_of_set_impl x), op_ivl_rep_of_set) ∈ appr_rel → ⟨lv_rel ×⇩r lv_rel⟩nres_rel"
  using ivl_rep_of_set_impl.refine
  by auto

schematic_goal ivl_rep_of_sets_impl:
  assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) n"
  assumes [autoref_rules]: "(ai, a) ∈ ⟨appr_rel⟩list_wset_rel"
  notes [refine_transfer] = FORWEAK_LIST_plain.refine
  shows "(RETURN (?f), op_ivl_rep_of_sets a::('a × 'a)nres) ∈ ⟨lv_rel ×⇩r lv_rel⟩nres_rel"
  unfolding op_ivl_rep_of_sets_def
  by (autoref_monadic(plain))
concrete_definition ivl_rep_of_sets_impl for n ai uses ivl_rep_of_sets_impl
lemma ivl_rep_of_sets_impl_refine[autoref_rules]:
  "DIM_precond TYPE('a::executable_euclidean_space) n ⟹
  (λai. RETURN (ivl_rep_of_sets_impl n ai), op_ivl_rep_of_sets::_⇒('a × 'a)nres) ∈ ⟨appr_rel⟩list_wset_rel → ⟨lv_rel ×⇩r lv_rel⟩nres_rel"
  using ivl_rep_of_sets_impl.refine by force

schematic_goal ivl_rep_of_set_coll_impl:
  assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) n"
  assumes [autoref_rules]: "(ai, a) ∈ clw_rel appr_rel"
  shows "(RETURN (?f), ivl_rep_of_set_coll a::('a×'a) nres) ∈ ⟨lv_rel ×⇩r lv_rel⟩nres_rel"
  unfolding ivl_rep_of_set_coll_def
  by (autoref_monadic (plain))
concrete_definition ivl_rep_of_set_coll_impl for n ai uses ivl_rep_of_set_coll_impl
lemma ivl_rep_of_set_coll_impl_refine[autoref_rules]:
  "DIM_precond TYPE('a::executable_euclidean_space) n ⟹
  (λai. RETURN (ivl_rep_of_set_coll_impl n ai), ivl_rep_of_set_coll::_⇒('a×'a) nres) ∈ clw_rel appr_rel → ⟨lv_rel ×⇩r lv_rel⟩nres_rel"
  using ivl_rep_of_set_coll_impl.refine by force

schematic_goal ivls_of_sets_impl:
  assumes [autoref_rules]: "(xsi, xs) ∈ clw_rel appr_rel"
  shows "(nres_of (?f), ivls_of_sets $ xs) ∈ ⟨clw_rel lvivl_rel⟩nres_rel"
  unfolding ivls_of_sets_def
  by autoref_monadic
concrete_definition ivls_of_sets_impl for xsi uses ivls_of_sets_impl
lemma ivls_of_set_impl_refine[autoref_rules]:
  "(λai. nres_of (ivls_of_sets_impl ai), ivls_of_sets) ∈ clw_rel appr_rel → ⟨clw_rel lvivl_rel⟩nres_rel"
  using ivls_of_sets_impl.refine by force

lemma card_info[autoref_rules]:
  "((λx. RETURN (length x)), card_info) ∈ clw_rel R → ⟨nat_rel⟩nres_rel"
  by (auto simp: card_info_def nres_rel_def)

lemma ivl_to_set[autoref_rules]:
  "(λ(i, s). if list_all2 (≤) i s then [appr_of_ivl ops i s] else [], ivl_to_set::_⇒'a::executable_euclidean_space set) ∈ lvivl_rel → clw_rel (appr_rel)"
  supply le = lv_rel_le[param_fo]
  apply (clarsimp simp add: ivl_rel_def)
  subgoal premises prems for ls us l u X
    using le[OF ‹(_, l) ∈ _› ‹(_, u) ∈ _›] prems transfer_operations1[of l u ls us]
    apply (auto simp: Cons_mem_clw_rel_iff single_valued_appr_rel ivl_rel_def[symmetric] intro!: exI[where x=X])
    subgoal by (auto simp: set_of_ivl_def br_def)
    subgoal using Union_rel_empty by (auto simp: set_of_ivl_def br_def )
    done
  done

lemma sets_of_ivls[autoref_rules]:
  shows "(λxs. map (λ(i, s). appr_of_ivl ops i s) [(i,s) ← xs. list_all2 (≤) i s], sets_of_ivls::_⇒'a::executable_euclidean_space set) ∈ clw_rel lvivl_rel → clw_rel (appr_rel)"
  supply le = lv_rel_le[param_fo]
  apply (rule fun_relI)
  unfolding appr_rel_br ivl_rel_br clw_rel_br lvivl_rel_br
  apply (auto simp: br_def set_of_ivl_def)
  subgoal for a b c d
    apply (rule exI conjI le le[param_fo,THEN IdD, THEN iffD2] lv_relI| assumption | force)+
    using transfer_operations1[where 'a='a, of "eucl_of_list c" "eucl_of_list d" c d]
    apply (auto simp: appr_rel_br br_def lvivl_rel_br set_of_ivl_def lv_rel_def)
    by (metis (mono_tags, lifting) atLeastAtMost_iff atLeastatMost_empty_iff case_prodD empty_iff)
  subgoal for a b c d
    using transfer_operations1[where 'a='a, of "eucl_of_list b" "eucl_of_list c" b c]
      le[of b _ c _, OF lv_relI lv_relI]
    by (auto simp: appr_rel_br br_def lvivl_rel_br set_of_ivl_def lv_rel_def intro!: bexI)
  done

schematic_goal above_sctn_impl:
  assumes [autoref_rules]: "(Xi, X) ∈ appr_rel" "(sctni, sctn) ∈ ⟨lv_rel⟩sctn_rel"
  shows "(?f::?'r, above_sctn $ X $ sctn) ∈ ?R"
  unfolding autoref_tag_defs
  by (rule above_sctn_nres[THEN nres_rel_trans2]) autoref_monadic
concrete_definition above_sctn_impl for Xi sctni uses above_sctn_impl
lemma above_sctn_impl_refine[autoref_rules]:
  "(λai sctni. RETURN (above_sctn_impl ai sctni), above_sctn) ∈ appr_rel → ⟨lv_rel⟩sctn_rel → ⟨bool_rel⟩nres_rel"
  using above_sctn_impl.refine by force

schematic_goal below_sctn_impl:
  assumes [autoref_rules]: "(ai, a) ∈ appr_rel"
  assumes [autoref_rules]: "(sctni, sctn) ∈ ⟨lv_rel⟩sctn_rel"
  shows "(?f::?'r, below_sctn $ a $ sctn) ∈ ?R"
  unfolding autoref_tag_defs
  by (rule below_sctn_nres[THEN nres_rel_trans2]) (autoref_monadic (plain))
concrete_definition below_sctn_impl for ai sctni uses below_sctn_impl
lemma below_sctn_impl_refine[autoref_rules]:
  "(λai sctni. RETURN (below_sctn_impl ai sctni), below_sctn) ∈ appr_rel → ⟨lv_rel⟩sctn_rel → ⟨bool_rel⟩nres_rel"
  using below_sctn_impl.refine by force

schematic_goal sbelow_sctn_impl:
  assumes [autoref_rules]: "(ai, a) ∈ appr_rel"
  assumes [autoref_rules]: "(sctni, sctn) ∈ ⟨lv_rel⟩sctn_rel"
  shows "(?f::?'r, sbelow_sctn $ a $ sctn) ∈ ?R"
  unfolding autoref_tag_defs
  by (rule sbelow_sctn_nres[THEN nres_rel_trans2]) (autoref_monadic (plain))
concrete_definition sbelow_sctn_impl for ai sctni uses sbelow_sctn_impl
lemma sbelow_sctn_impl_refine[autoref_rules]:
  "(λai sctni. RETURN (sbelow_sctn_impl ai sctni), sbelow_sctn) ∈
    appr_rel → ⟨lv_rel⟩sctn_rel → ⟨bool_rel⟩nres_rel"
  using sbelow_sctn_impl.refine by force

schematic_goal sbelow_sctns_impl:
  assumes [autoref_rules]: "(ai, a) ∈ appr_rel"
  assumes [autoref_rules]: "(sctnsi, sctns) ∈ sctns_rel"
  shows "(?f::?'r, sbelow_sctns $ a $ sctns) ∈ ?R"
  unfolding autoref_tag_defs
  apply (rule sbelow_sctns_nres[THEN nres_rel_trans2])
  subgoal using list_set_rel_finiteD[of sctnsi sctns "⟨lv_rel⟩sctn_rel"] ‹(sctnsi, sctns) ∈ _› by (simp add: relAPP_def)
  by (autoref_monadic (plain))
concrete_definition sbelow_sctns_impl for ai sctnsi uses sbelow_sctns_impl
lemma sbelow_sctns_impl_refine[autoref_rules]:
  "(λai sctni. RETURN (sbelow_sctns_impl ai sctni), sbelow_sctns) ∈
    appr_rel → sctns_rel → ⟨bool_rel⟩nres_rel"
  using sbelow_sctns_impl.refine by force

schematic_goal intersects_impl:
  assumes [autoref_rules]: "(ai, a) ∈ appr_rel"
  assumes [autoref_rules]: "(sctni, sctn) ∈ ⟨lv_rel⟩sctn_rel"
  shows "(?f::?'r, op_intersects $ a $ sctn) ∈ ?R"
  unfolding autoref_tag_defs op_intersects_def
  by (autoref_monadic (plain))
concrete_definition intersects_impl for ai sctni uses intersects_impl
lemma intersects_impl_refine[autoref_rules]:
  "(λai sctni. RETURN (intersects_impl ai sctni), op_intersects) ∈ appr_rel → ⟨lv_rel⟩sctn_rel → ⟨bool_rel⟩nres_rel"
  using intersects_impl.refine by force

schematic_goal sbelow_sctns_coll_impl:
  assumes [autoref_rules]: "(ai, a) ∈ clw_rel appr_rel"
  assumes [autoref_rules]: "(sctnsi, sctns) ∈ sctns_rel"
  shows "(?f::?'r, sbelow_sctns_coll $ a $ sctns) ∈ ?R"
  unfolding sbelow_sctns_coll_def
  by autoref
concrete_definition sbelow_sctns_coll_impl for ai sctnsi uses sbelow_sctns_coll_impl
lemma sbelow_sctns_coll_impl_refine[autoref_rules]:
  "(sbelow_sctns_coll_impl, sbelow_sctns_coll) ∈ clw_rel appr_rel → sctns_rel → ⟨bool_rel⟩nres_rel"
  using sbelow_sctns_coll_impl.refine by force

schematic_goal sbelow_sctns_coll_dres:
  "nres_of ?r ≤ sbelow_sctns_coll_impl a sctns"
  unfolding sbelow_sctns_coll_impl_def
  by refine_transfer
concrete_definition sbelow_sctns_coll_dres for a sctns uses sbelow_sctns_coll_dres
lemmas [refine_transfer] = sbelow_sctns_coll_dres.refine

schematic_goal below_sctn_coll_impl:
  assumes [autoref_rules]: "(ai, a) ∈ clw_rel appr_rel"
  assumes [autoref_rules]: "(sctni, sctn) ∈ ⟨lv_rel⟩sctn_rel"
  shows "(?f::?'r, below_sctn_coll $ a $ sctn) ∈ ?R"
  unfolding below_sctn_coll_def by autoref
concrete_definition below_sctn_coll_impl for ai sctni uses below_sctn_coll_impl
lemma below_sctn_coll_impl_refine[autoref_rules]:
  "(below_sctn_coll_impl, below_sctn_coll) ∈ clw_rel appr_rel → ⟨lv_rel⟩sctn_rel → ⟨bool_rel⟩nres_rel"
  using below_sctn_coll_impl.refine by force
schematic_goal below_sctn_coll_dres:
  "nres_of ?r ≤ below_sctn_coll_impl a sctn"
  unfolding below_sctn_coll_impl_def
  by refine_transfer
concrete_definition below_sctn_coll_dres for a sctn uses below_sctn_coll_dres
lemmas [refine_transfer] = below_sctn_coll_dres.refine

schematic_goal intersects_clw_impl:
  assumes [autoref_rules]: "(ai, a) ∈ clw_rel appr_rel"
  assumes [autoref_rules]: "(sctni, sctn) ∈ ⟨lv_rel⟩sctn_rel"
  shows "(?f::?'r, intersects_clw $ a $ sctn) ∈ ?R"
  unfolding intersects_clw_def autoref_tag_defs
  including art
  by (autoref_monadic (plain))
concrete_definition intersects_clw_impl for ai sctni uses intersects_clw_impl
lemma intersects_clw_impl_refine[autoref_rules]:
  "(λai sctni. RETURN (intersects_clw_impl ai sctni), intersects_clw) ∈ clw_rel appr_rel → ⟨lv_rel⟩sctn_rel → ⟨bool_rel⟩nres_rel"
  using intersects_clw_impl.refine by force

schematic_goal subset_spec_ivlc:
  assumes [autoref_rules]: "(Xi, X::'a::executable_euclidean_space set) ∈ appr_rel"
      "(ivli, ivl) ∈ ⟨lv_rel⟩ivl_rel"
  notes [autoref_post_simps] = Let_def
  shows "(RETURN (?f), op_subset $ X $ ivl) ∈ ⟨bool_rel⟩nres_rel"
  unfolding op_subset_def
  by autoref_monadic
concrete_definition subset_spec_ivlc for Xi ivli uses subset_spec_ivlc

lemma subset_spec_ivl_refine[autoref_rules]:
  "(λXi Yi. RETURN (subset_spec_ivlc Xi Yi), op_subset) ∈ appr_rel → ⟨lv_rel⟩ivl_rel → ⟨bool_rel⟩nres_rel"
  for A::"(_ × 'a::executable_euclidean_space set) set"
  using subset_spec_ivlc.refine
  by auto

schematic_goal subset_spec_ivl_collc:
  assumes [autoref_rules]: "(Xi, X::'a::executable_euclidean_space set) ∈ clw_rel appr_rel"
    "(ivli, ivl) ∈ ⟨lv_rel⟩ivl_rel"
  notes [autoref_post_simps] = Let_def
  shows "(RETURN (?f), subset_spec_coll $ X $ ivl) ∈ ⟨bool_rel⟩nres_rel"
  unfolding subset_spec_coll_def
  by (autoref_monadic (plain))
concrete_definition subset_spec_ivl_collc for Xi ivli uses subset_spec_ivl_collc
lemma subset_spec_ivl_collc_refine[autoref_rules]:
  "(λXi Yi. RETURN (subset_spec_ivl_collc Xi Yi), subset_spec_coll) ∈ clw_rel appr_rel → ⟨lv_rel⟩ivl_rel → ⟨bool_rel⟩nres_rel"
  using subset_spec_ivl_collc.refine by force

schematic_goal project_set_appr:
  fixes b::"'a::executable_euclidean_space" and y
  assumes [autoref_rules]: "(Xi, X) ∈ appr_rel"
  assumes [autoref_rules]: "(bi, b) ∈ lv_rel"
  assumes [autoref_rules]: "(yi, y) ∈ rnv_rel"
  shows "(nres_of (?f::?'r dres), op_project_set X b y) ∈ ?R"
  unfolding op_project_set_def
  by autoref_monadic
concrete_definition project_set_appr for Xi bi yi uses project_set_appr
lemma project_set_appr_refine[autoref_rules]:
  "(λXi bi yi. nres_of (project_set_appr Xi bi yi), op_project_set) ∈ appr_rel → lv_rel → rnv_rel → ⟨appr_rel⟩nres_rel"
  using project_set_appr.refine by force

schematic_goal project_set_clw_impl:
  assumes [autoref_rules]: "(Xi, X) ∈ clw_rel appr_rel"
  assumes [autoref_rules]: "(bi, b) ∈ lv_rel"
  assumes [autoref_rules]: "(yi, y) ∈ rnv_rel"
  shows "(nres_of (?f::?'r dres), project_set_clw X b y) ∈ ?R"
  unfolding project_set_clw_def
  including art
  by autoref_monadic
concrete_definition project_set_clw_impl for Xi bi yi uses project_set_clw_impl
lemma project_set_clw_refine[autoref_rules]:
  "(λXi bi yi. nres_of (project_set_clw_impl Xi bi yi), project_set_clw) ∈
    clw_rel appr_rel → lv_rel → rnv_rel → ⟨clw_rel appr_rel⟩nres_rel"
  using project_set_clw_impl.refine by force

schematic_goal subset_spec_ivls_impl:
  assumes [autoref_rules]: "(Xi, X) ∈ appr_rel" "(Yi, Y) ∈ clw_rel lvivl_rel"
  shows "(RETURN ?f, subset_spec_ivls X Y) ∈ ⟨bool_rel⟩nres_rel"
  unfolding subset_spec_ivls_def
  by (autoref_monadic (plain))
concrete_definition subset_spec_ivls_impl for Xi Yi uses subset_spec_ivls_impl
lemmas [autoref_rules] = subset_spec_ivls_impl.refine[autoref_higher_order_rule]

schematic_goal subset_spec_ivls_clw_impl:
  assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) D"
  assumes [autoref_rules]: "(Xi, X::'a set) ∈ clw_rel lvivl_rel" "(Yi, Y) ∈ clw_rel lvivl_rel"
    "(Mi, M) ∈ nat_rel"
  shows "(nres_of ?f, subset_spec_ivls_clw M X Y) ∈ ⟨bool_rel⟩nres_rel"
  unfolding subset_spec_ivls_clw_def
  including art
  by (autoref_monadic)
concrete_definition subset_spec_ivls_clw_impl for Mi Xi Yi uses subset_spec_ivls_clw_impl
lemma [autoref_rules]:
"DIM_precond TYPE('a::executable_euclidean_space) D ⟹
  (λMi Xi Yi. nres_of (subset_spec_ivls_clw_impl D Mi Xi Yi),
   subset_spec_ivls_clw::nat ⇒ 'a set ⇒ _)
  ∈ nat_rel → clw_rel (⟨lv_rel⟩ivl_rel) → clw_rel (⟨lv_rel⟩ivl_rel) → ⟨bool_rel⟩nres_rel"
  using subset_spec_ivls_clw_impl.refine by force

lemma REMDUPS_impl[autoref_rules]: "(remdups, REMDUPS) ∈ clw_rel A → clw_rel A"
  if "PREFER single_valued A"
  using that
  by (force simp: clw_rel_br dest!: brD intro!: brI elim!: single_valued_as_brE)

schematic_goal split_along_ivls2_impl:
  assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) D"
  assumes [autoref_rules]: "(Xi, X::'a set) ∈ clw_rel lvivl_rel" "(ISi, IS) ∈ clw_rel lvivl_rel"
      "(Mi, M) ∈ nat_rel"
  shows "(nres_of ?f, split_along_ivls2 $ M $ X $ IS) ∈ ⟨clw_rel lvivl_rel⟩nres_rel"
  unfolding autoref_tag_defs
  unfolding split_along_ivls2_def
  by autoref_monadic
concrete_definition split_along_ivls2_impl uses split_along_ivls2_impl
lemmas [autoref_rules] = split_along_ivls2_impl.refine

lemma op_list_of_eucl_image_autoref[autoref_rules]:
  shows "(λxs. xs, op_list_of_eucl_image) ∈ appr_rel → appr_rell"
  by (auto simp: length_set_of_appr appr_rel_def lv_rel_def image_image set_rel_br
      cong: image_cong
      dest!: brD)

lemma op_eucl_of_list_image_autoref[autoref_rules]:
  includes autoref_syntax
  assumes "DIM_precond TYPE('a::executable_euclidean_space) D"
  assumes "(xsi, xs) ∈ appr_rell"
  assumes "SIDE_PRECOND (env_len xs D)"
  shows "(xsi, op_eucl_of_list_image $ (xs)::'a set) ∈ appr_rel"
  using assms
  unfolding appr_rel_br
  by (auto simp: length_set_of_appr appr_rel_br br_def image_image env_len_def appr_rell_internal)

lemma take_set_of_apprD: "xs ∈ set_of_appr XS ⟹ take n xs ∈ set_of_appr (take n XS)"
  apply (cases "n < length xs")
   apply (subst take_eq_map_nth)
    apply simp
   apply (subst take_eq_map_nth)
    apply (simp add: length_set_of_appr)
   apply (rule set_of_appr_project)
  by (auto simp: length_set_of_appr)

lemma set_of_appr_ex_append1:
  "xrs ∈ set_of_appr xs ⟹ ∃r. r @ xrs ∈ set_of_appr (b @ xs)"
proof (induction b)
  case Nil
  then show ?case by (auto intro!: exI[where x=Nil])
next
  case (Cons a b)
  then show ?case
    apply (auto)
    subgoal for r
      apply (drule set_of_apprs_ex_Cons[where b=a and xs="b@xs"])
      apply auto
      by (metis Cons_eq_appendI)
    done
qed

lemma set_of_appr_ex_append2:
  assumes "xrs ∈ set_of_appr xs" shows "∃r. xrs @ r ∈ set_of_appr (xs @ b)"
proof -
  from set_of_appr_ex_append1[OF assms, of b]
  obtain r where r: "r @ xrs ∈ set_of_appr (b @ xs)" by auto
  have "map ((!) (r @ xrs)) ([length b..<length b + length xs] @ [0..<length b])
    ∈ set_of_appr (map ((!) (b @ xs)) ([length b..<length b + length xs] @ [0..<length b]))"
    by (rule set_of_appr_project[OF r, of "[length b..<length b + length xs] @ [0..<length b]"])
      auto
  also have "map ((!) (b @ xs)) ([length b..<length b + length xs] @ [0..<length b]) = xs @ b"
    by (auto intro!: nth_equalityI simp: nth_append)
  also have "map ((!) (r @ xrs)) ([length b..<length b + length xs] @ [0..<length b]) = xrs @ r"
    using length_set_of_appr[OF r] assms length_set_of_appr
    by (auto intro!: nth_equalityI simp: nth_append)
  finally show ?thesis by rule
qed

lemma drop_all_conc: "drop (length a) (a@b) = b"
  by (simp)

lemma set_of_appr_takeD: "xs ∈ set_of_appr (take n XS) ⟹ xs ∈ take n ` set_of_appr XS"
  apply (frule set_of_appr_ex_append2[where b="map ((!) XS) [n..<length XS]"])
  apply (auto simp: take_append_take_minus_idem)
  apply (rule image_eqI)
   prefer 2 apply assumption
  by (metis append_eq_append_conv append_take_drop_id drop_all_conc length_drop length_set_of_appr)

lemma op_take_image_autoref[autoref_rules]:
  shows "(λni xs. take ni xs, op_take_image) ∈ nat_rel → appr_rell → appr_rell"
  apply (auto simp: appr_rell_internal br_def )
  subgoal by (rule take_set_of_apprD)
  subgoal by (rule set_of_appr_takeD)
  done

lemma drop_eq_map_nth: "drop n xs = map ((!) xs) [n..<length xs]"
  by (auto intro!: nth_equalityI simp: nth_append)

lemma drop_set_of_apprD: "xs ∈ set_of_appr XS ⟹ drop n xs ∈ set_of_appr (drop n XS)"
   apply (subst drop_eq_map_nth)
   apply (subst drop_eq_map_nth)
    apply (simp add: length_set_of_appr)
   apply (rule set_of_appr_project)
  by (auto simp: length_set_of_appr)

lemma drop_append_drop_minus_idem: "n < length XS ⟹ map ((!) XS) [0..<n] @ drop n XS = XS"
  by (auto intro!: nth_equalityI simp: nth_append)

lemma set_of_appr_dropD: "xs ∈ set_of_appr (drop n XS) ⟹ xs ∈ drop n ` set_of_appr XS"
  apply (cases "n < length XS")
  subgoal
    apply (frule set_of_appr_ex_append1[where b="map ((!) XS) [0..<n]"])
    apply (auto simp: drop_append_drop_minus_idem)
    apply (rule image_eqI)
    prefer 2 apply assumption
    by (metis (mono_tags, lifting) diff_add_inverse2 diff_diff_cancel drop_all_conc length_append
        length_drop length_set_of_appr less_imp_le)
  subgoal
    using set_of_appr_nonempty[of XS]
    by (auto simp: length_set_of_appr image_iff simp del: set_of_appr_nonempty)
  done

lemma op_drop_image_autoref[autoref_rules]:
  shows "(λni xs. drop ni xs, op_drop_image) ∈ nat_rel → appr_rell → appr_rell"
  apply (auto simp: appr_rell_internal br_def )
  subgoal by (rule drop_set_of_apprD)
  subgoal by (rule set_of_appr_dropD)
  done

lemma mem_set_of_appr_appendE:
  assumes "zs ∈ set_of_appr (XS @ YS)"
  obtains xs ys where "zs = xs @ ys" "xs ∈ set_of_appr XS" "ys ∈ set_of_appr YS"
proof -
  have "zs = map ((!) zs) [0..<length XS] @ map ((!) zs) [length XS..<length XS + length YS]"
    using assms
    by (auto intro!: nth_equalityI simp: nth_append dest!: length_set_of_appr)
  moreover
  from
    set_of_appr_project[OF assms, of "[0..<length XS]"]
    set_of_appr_project[OF assms, of "[length XS..<length XS + length YS]"]
  have "map ((!) zs) [0..<length XS] ∈ set_of_appr XS"
    "map ((!) zs) [length XS..<length XS + length YS] ∈ set_of_appr YS"
    by (auto simp : map_nth_append2 map_nth_append1)
  ultimately show ?thesis ..
qed

lemma lv_ivl_self[simp]: "lv_ivl xs xs = {xs}" for xs::"'a::order list"
  by (force simp: lv_ivl_def list_all2_conv_all_nth
      intro!: nth_equalityI)

lemma set_of_appr_of_ivl_point'[simp]:
  "set_of_appr (appr_of_ivl ops (replicate E 0) (replicate E 0)) = {replicate E (0::real)}"
  using transfer_operations_rl(1)[of "(replicate E (0::real))" "(replicate E (0::real))" "(replicate E (0::real))" "(replicate E 0)"]
  by (auto simp: appr_rell_internal br_def)

lemma set_of_appr_of_ivl_point:
  "set_of_appr (appr_of_ivl ops xs xs) = {xs}"
  using transfer_operations_rl(1)[of xs xs xs xs]
  by (auto simp: appr_rell_internal br_def)

lemma set_of_appr_of_ivl_append_point:
  "set_of_appr (xs @ appr_of_ivl ops p p) = (λx. x @ p) ` set_of_appr xs"
  apply auto
   apply (frule length_set_of_appr)
  subgoal for x
    apply (rule image_eqI[where x="take (length xs) x"])
     apply (auto intro!: nth_equalityI simp: min_def)
     apply (simp add: nth_append)
    subgoal for i
      apply (frule set_of_appr_project[where ?is="[length xs..<length xs + length p]"])
       apply simp
      apply (auto simp: map_nth_append2 set_of_appr_of_ivl_point)
      subgoal premises prems
      proof -
        from prems
        have "map ((!) x) [length xs..<length xs + length p] ! (i - length xs) =
          p ! (i - length xs)"
          by simp
        also have "map ((!) x) [length xs..<length xs + length p] ! (i - length xs) = x ! i"
          using prems
          apply (auto simp: map_nth)
          by (metis add_diff_cancel_left' add_diff_inverse_nat add_less_cancel_left nth_map_upt)
        finally show ?thesis
          using prems by (simp add: min_def)
      qed
      done
    subgoal
      apply (frule set_of_appr_project[where ?is="[0..<length xs]"])
       apply (auto simp: map_nth_append1 take_eq_map_nth
          elim!: mem_set_of_appr_appendE
          dest: length_set_of_appr)
      done
    done
  subgoal premises prems for x
  proof -
    from set_of_appr_ex_append2[where b="appr_of_ivl ops p p", OF ‹x ∈ set_of_appr xs›]
    obtain r where r: "x @ r ∈ set_of_appr (xs @ appr_of_ivl ops p p)"
      by auto
    have "map ((!) (x @ r)) [length xs..<length xs + (length p)]
        ∈ set_of_appr
            (map ((!) (xs @ appr_of_ivl ops p p))
              [length xs..<length xs + (length p)])"
      by (rule set_of_appr_project[OF r, of "[length xs..<length xs+(length p)]"])
         auto
    also have "map ((!) (x @ r)) [length xs..<length xs + (length p)] = r"
      using length_set_of_appr prems r
      by (auto intro!: nth_equalityI simp: nth_append dest!: length_set_of_appr)
    also have "map ((!) (xs @ appr_of_ivl ops p p))
        [length xs..<length xs + (length p)] = appr_of_ivl ops p p"
      by (auto intro!: nth_equalityI)
    finally have "r = p"
      by (auto simp: set_of_appr_of_ivl_point)
    with r show ?thesis by simp
  qed
  done

lemma nth_append_cond:
  "i < length xs ⟹ (xs @ ys) ! i = xs ! i"
  "i ≥ length xs ⟹ (xs @ ys) ! i = ys ! (i - length xs)"
  by (auto simp: nth_append)

lemma set_of_appr_of_ivl_point_append:
  "set_of_appr (appr_of_ivl ops p p @ xs) = (λx. p @ x) ` set_of_appr xs"
  apply auto
   apply (frule length_set_of_appr)
  subgoal for x
    apply (rule image_eqI[where x="drop (length p) x"])
     apply (auto intro!: nth_equalityI simp: min_def)
     apply (simp add: nth_append)
    subgoal for i
      apply (frule set_of_appr_project[where ?is="[0..<(length p)]"])
       apply simp
      apply (auto simp: map_nth_append1 dest: length_set_of_appr)
      by (metis insertE mem_set_of_appr_appendE memb_imp_not_empty nth_append_cond(1) set_of_appr_of_ivl_point)
    by (metis add_right_imp_eq drop_all_conc drop_set_of_apprD length_append length_set_of_appr)
  subgoal premises prems for x
  proof -
    from set_of_appr_ex_append1[where b="appr_of_ivl ops p p",
        OF ‹x ∈ set_of_appr xs›]
    obtain r where r: "r @ x ∈ set_of_appr (appr_of_ivl ops p p @ xs)"
      by auto
    have "map ((!) (r @ x)) [0..<(length p)]
        ∈ set_of_appr
            (map ((!) (appr_of_ivl ops p p @ xs))
              [0..<(length p)])"
      by (rule set_of_appr_project[OF r, of "[0..<(length p)]"])
         auto
    also have "map ((!) (r @ x)) [0..<(length p)] = r"
      using length_set_of_appr prems r
      by (auto intro!: nth_equalityI simp: nth_append dest!: length_set_of_appr)
    also have "map ((!) (appr_of_ivl ops p p @ xs))
        [0..<(length p)] = appr_of_ivl ops p p"
      by (auto intro!: nth_equalityI simp: nth_append)
    finally have "r = p"
      by (auto simp: set_of_appr_of_ivl_point)
    with r show ?thesis by simp
  qed
  done

lemma op_eucl_of_list_image_pad:
  includes autoref_syntax
  assumes "(xsi, xs) ∈ appr_rell" "DIM_precond TYPE('a::executable_euclidean_space) E"
  shows "(take E xsi @ (let z = replicate (E - length xsi) 0 in appr_of_ivl ops z z),
    op_eucl_of_list_image $ xs::'a set) ∈ appr_rel"
  using assms
  unfolding appr_rel_br
  apply (auto simp: length_set_of_appr appr_rel_br br_def image_image env_len_def appr_rell_internal)
    apply (auto simp: Let_def set_of_appr_of_ivl_append_point length_set_of_appr)
   apply (rule image_eqI)
    prefer 2
    apply (rule image_eqI)
     apply (rule refl)
    apply (rule take_set_of_apprD)
    apply assumption
   apply auto
  apply (drule set_of_appr_takeD)
  apply auto
  done
concrete_definition op_eucl_of_list_image_pad for E xsi uses op_eucl_of_list_image_pad
lemma op_eucl_of_list_image_pad_refine[autoref_rules]:
  "DIM_precond TYPE('a::executable_euclidean_space) E ⟹
  (op_eucl_of_list_image_pad E, op_eucl_of_list_image::_⇒'a set) ∈ appr_rell → appr_rel"
  using op_eucl_of_list_image_pad.refine
  by force

lemma [autoref_op_pat_def]: "approx_slp_appr fas ≡ OP (approx_slp_appr fas)"
  by auto
schematic_goal approx_slp_appr_impl:
  includes autoref_syntax
  assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) E"
  assumes [autoref_rules]: "(slpi, slp) ∈ slp_rel" "(Xi, X) ∈ appr_rell"
    notes [autoref_rules] = IdI[of E]
  shows "(nres_of ?r, approx_slp_appr fas $ slp $ X::'a set nres) ∈ ⟨appr_rel⟩nres_rel"
  unfolding autoref_tag_defs
  unfolding approx_slp_appr_def assms(1)[unfolded DIM_eq_def]
  including art
  by autoref_monadic

concrete_definition approx_slp_appr_impl for E slpi Xi uses approx_slp_appr_impl
lemma approx_slp_appr_impl_refine[autoref_rules]:
  "DIM_precond TYPE('a::executable_euclidean_space) E ⟹
(λslpi Xi. nres_of (approx_slp_appr_impl E slpi Xi), approx_slp_appr fas::_⇒_⇒'a set nres) ∈
    slp_rel → appr_rell → ⟨appr_rel⟩nres_rel"
  using approx_slp_appr_impl.refine[where 'a='a, of E]
  by force

lemma DIM_precond_real[autoref_rules_raw]: "DIM_precond TYPE(real) 1" by simp

schematic_goal mig_set_impl: "(nres_of ?r, mig_set $ D $ X) ∈ ⟨rnv_rel⟩nres_rel"
  if [autoref_rules]: "(Xi, X::'a set) ∈ appr_rel"  "(Di, D) ∈ nat_rel"
  and [autoref_rules_raw, simplified, simp]: "DIM_precond TYPE('a::executable_euclidean_space) D"
  unfolding autoref_tag_defs
  unfolding mig_set_def
  including art
  by autoref_monadic
concrete_definition mig_set_impl for Di Xi uses mig_set_impl
lemma mig_set_impl_refine[autoref_rules]:
  includes autoref_syntax
  assumes "DIM_precond TYPE('a::executable_euclidean_space) D" "(Di, D) ∈ nat_rel"
  shows "(λx. nres_of (mig_set_impl D x), mig_set $ D::'a set⇒_) ∈ appr_rel → ⟨rnv_rel⟩nres_rel"
  using mig_set_impl.refine assms by force

lemma ncc_precondD:
  assumes "ncc_precond TYPE('a::executable_euclidean_space)"
  shows"(Xi, X::'a set) ∈ appr_rel ⟹ ncc X"
  using assms
  by (auto simp: ncc_precond_def split_beta' br_def appr_rel_br
      dest!: bspec[where x="(Xi, X)"])

end

end