Theory Concrete_Reachability_Analysis

theory Concrete_Reachability_Analysis

abbreviation "num_optns_rel  (Id::'b numeric_options rel)"

consts i_flow1::interface
consts i_appr1::interface

abbreviation "float10_rel  Id::(float10 × float10) set"

lemma inj_on_nat_add_square: "inj_on (λa::nat. a + a * a) S"
  by (rule strict_mono_imp_inj_on) (auto intro!: strict_monoI add_strict_mono mult_strict_mono)

lemma add_sq_eq[simp]: "a + a * a = b + b * b  a = b" for a b::nat
  using inj_on_nat_add_square[of UNIV, unfolded inj_on_def, rule_format, of a b]
  by auto

context includes autoref_syntax begin
lemma [autoref_rules]:
  "(precision, precision)num_optns_rel  nat_rel"
  "(start_stepsize, start_stepsize)num_optns_rel  rnv_rel"
  "(iterations, iterations) num_optns_rel nat_rel"
  "(halve_stepsizes, halve_stepsizes) (num_optns_rel)  nat_rel"
  "(widening_mod, widening_mod) (num_optns_rel) nat_rel"
  "(rk2_param, rk2_param) (num_optns_rel)  rnv_rel"
  "(method_id, method_id) (num_optns_rel)  nat_rel"
  "(adaptive_atol, adaptive_atol) (num_optns_rel)  rnv_rel"
  "(adaptive_rtol, adaptive_rtol) (num_optns_rel)  rnv_rel"
  "(printing_fun, printing_fun) (num_optns_rel)  bool_rel  I  unit_rel"
  "(tracing_fun, tracing_fun) (num_optns_rel)  string_rel  Ioption_rel  unit_rel"
  by auto


lemma [autoref_op_pat_def]:
  includes autoref_syntax
    "(λxs. xs @ replicate D 0) ` X  OP (pad_zeroes D) $ X"
    "pad_zeroes D X  OP (pad_zeroes D) $ X"
  by simp_all

subsection ‹Relation Implementing ode_ops›: Caching slp_of›-Programs.›

definition "ode_slps_of ode_ops =
  (approximate_sets_ode.ode_slp ode_ops,
    approximate_sets_ode.euler_incr_slp ode_ops,
    approximate_sets_ode.euler_slp ode_ops,
    approximate_sets_ode.rk2_slp ode_ops,
    approximate_sets_ode.D ode_ops)"

definition "init_ode_ops poincare c1 ode_ops =
  (ode_ops, ode_slps_of ode_ops,
    (if poincare then Some(approximate_sets_ode.solve_poincare_slp ode_ops) else None),
    (if c1 then Some(ode_slps_of (approximate_sets_ode'.var_ode_ops ode_ops)) else None))"

definition "ode_ops_rel =
  {(init, ode_ops). init = init_ode_ops True True ode_ops
     init = init_ode_ops True False ode_ops
     init = init_ode_ops False False ode_ops }"

consts i_ode_ops::interface
lemmas [autoref_rel_intf] = REL_INTFI[of ode_ops_rel i_ode_ops]
lemmas [autoref_tyrel] = TYRELI[of ode_ops_rel]

context approximate_sets begin

unbundle autoref_syntax

lemma print_set_impl[autoref_rules]:
  shows "(printing_fun optns, print_set)  bool_rel  A  Id"
  by auto

lemma trace_set_impl[autoref_rules]:
  shows "(tracing_fun optns, trace_set)  string_rel  Aoption_rel  Id"
  by auto

definition "print_msg_impl s = tracing_fun optns s None"

lemma print_msg_impl[autoref_rules]:
  shows "(print_msg_impl, print_msg)  string_rel  unit_rel"
  unfolding print_msg_def
  by auto

definition "start_stepsize_impl = (if start_stepsize optns > 0 then start_stepsize optns else 1)"
definition "rk2_param_impl = (let rk = rk2_param optns in if rk > 0  rk  1 then rk else 1)"

lemma options_impl[autoref_rules]:
  "(RETURN (precision optns), precision_spec)  nat_relnres_rel"
  "(RETURN (adaptive_atol optns), adaptive_atol_spec)  rnv_relnres_rel"
  "(RETURN (adaptive_rtol optns), adaptive_rtol_spec)  rnv_relnres_rel"
  "(RETURN (method_id optns), method_spec)  nat_relnres_rel"
  "(RETURN start_stepsize_impl, start_stepsize_spec)  rnv_relnres_rel"
  "(RETURN (iterations optns), iterations_spec)  nat_relnres_rel"
  "(RETURN (widening_mod optns), widening_mod_spec)  nat_relnres_rel"
  "(RETURN (halve_stepsizes optns), halve_stepsizes_spec)  nat_relnres_rel"
  "(RETURN (rk2_param_impl), rk2_param_spec)  rnv_relnres_rel"
  by (auto simp: nres_rel_def
      start_stepsize_spec_def start_stepsize_impl_def
      rk2_param_spec_def rk2_param_impl_def Let_def)

sublocale approximate_sets_ode where ode_ops = ode_ops for ode_ops :: ode_ops ..

schematic_goal trace_sets_impl:
  assumes [autoref_rules]: "(si, s)  string_rel" "(Xi, X)  clw_rel appr_rel"
  shows "(RETURN ?f, trace_sets s X)  unit_relnres_rel"
  unfolding trace_sets_def
  by (subst rel_ANNOT_eq[of X "clw_rel appr_rel"]) (autoref_monadic (plain))
concrete_definition trace_sets_impl for si Xi uses trace_sets_impl
lemmas [autoref_rules] = trace_sets_impl.refine[autoref_higher_order_rule]

schematic_goal print_sets_impl:
  assumes [autoref_rules]: "(si, s)  bool_rel" "(Xi, X)  clw_rel appr_rel"
  shows "(RETURN ?f, print_sets s X)  unit_relnres_rel"
  unfolding print_sets_def
  by (subst rel_ANNOT_eq[of X "clw_rel appr_rel"]) (autoref_monadic (plain))
concrete_definition print_sets_impl for si Xi uses print_sets_impl
lemmas [autoref_rules] = print_sets_impl.refine[autoref_higher_order_rule]

definition "ode_slp_impl ode_ops =        (case ode_ops of (_, (x, _, _, _, _), _, _)  x)"
definition "euler_incr_slp_impl ode_ops = (case ode_ops of (_, (_, x, _, _, _), _, _)  x)"
definition "euler_slp_impl ode_ops =      (case ode_ops of (_, (_, _, x, _, _), _, _)  x)"
definition "rk2_slp_impl ode_ops =        (case ode_ops of (_, (_, _, _, x, _), _, _)  x)"
definition "D_impl ode_ops =              (case ode_ops of (_, (_, _, _, _, x), _, _)  x)"
definition "poincare_slp_impl ode_ops =   (case ode_ops of (ode_ops, (_, _, _, _, _), x, _) 
  (case x of
    None  let _ = print_msg_impl (''ODE solver not initialized: pslp missing'') in solve_poincare_slp ode_ops
  | Some pslp  pslp))"

lemma autoref_parameters[autoref_rules]:
  "(ode_slp_impl, ode_slp)  ode_ops_rel  slp_rel"
  "(euler_incr_slp_impl, euler_incr_slp)  ode_ops_rel  slp_rel"
  "(euler_slp_impl, euler_slp)  ode_ops_rel  slp_rel"
  "(rk2_slp_impl, rk2_slp)  ode_ops_rel  slp_rel"
  "(poincare_slp_impl, solve_poincare_slp)  ode_ops_rel  slp_rellist_rel"
  "(D_impl, D)  ode_ops_rel  nat_rel"
  by (auto simp: ode_ops_rel_def ode_slp_impl_def euler_incr_slp_def D_impl_def init_ode_ops_def
      euler_incr_slp_impl_def euler_slp_impl_def rk2_slp_impl_def poincare_slp_impl_def
      split: option.splits prod.splits)

definition "ode_e_impl = (λ(ode_ops, _). ode_expression ode_ops)"
lemma ode_e_impl[autoref_rules]: "(ode_e_impl, ode_e)  ode_ops_rel  fas_rel"
  by (auto simp: ode_e_impl_def ode_e_def ode_ops_rel_def init_ode_ops_def)

definition "safe_form_impl = (λ(ode_ops, _). safe_form ode_ops)"
lemma safe_form_impl[autoref_rules]: "(safe_form_impl, safe_form)  ode_ops_rel  Id"
  by (auto simp: safe_form_impl_def ode_ops_rel_def init_ode_ops_def)

schematic_goal safe_set_appr:
  assumes [autoref_rules]: "(Xi, X::'a::executable_euclidean_space set)  appr_rel"
  assumes [autoref_rules]: "(odoi, odo)  ode_ops_rel"
  notes [autoref_rules] = autoref_parameters
  shows "(nres_of ?f, safe_set odo X)  bool_relnres_rel"
  unfolding safe_set_def
  including art
  by autoref_monadic
concrete_definition safe_set_appr for odoi Xi uses safe_set_appr
lemmas safe_set_appr_refine[autoref_rules] = safe_set_appr.refine[autoref_higher_order_rule]

schematic_goal mk_safe_impl:
  assumes [autoref_rules]: "(odoi, odo)  ode_ops_rel"
  assumes [autoref_rules]: "(Ri, R)  appr_rel"
  shows "(nres_of ?f, mk_safe odo (R::'a::executable_euclidean_space set))  appr_relnres_rel"
  unfolding autoref_tag_defs
  unfolding mk_safe_def
  including art
  by autoref_monadic
concrete_definition mk_safe_impl for odoi Ri uses mk_safe_impl
lemmas mk_safe_impl_refine[autoref_rules] = mk_safe_impl.refine[autoref_higher_order_rule]
sublocale autoref_op_pat_def mk_safe .

schematic_goal mk_safe_coll_impl:
  assumes [autoref_rules]: "(ISi, IS)  clw_rel appr_rel"
  assumes [autoref_rules]: "(odoi, odo)  ode_ops_rel"
  shows "(nres_of (?f), mk_safe_coll odo (IS::'a::executable_euclidean_space set))  clw_rel appr_relnres_rel"
  unfolding mk_safe_coll_def
  by autoref_monadic
concrete_definition mk_safe_coll_impl for ISi uses mk_safe_coll_impl
lemmas mk_safe_coll_impl_refine[autoref_rules] = mk_safe_coll_impl.refine[autoref_higher_order_rule]
sublocale autoref_op_pat_def mk_safe_coll .

schematic_goal ode_set_impl:
  assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) E"
  assumes [autoref_rules]: "(Xi, X)  appr_rel"
  assumes [autoref_rules]: "(odoi, odo)  ode_ops_rel"
  notes [autoref_rules] = autoref_parameters
  shows "(nres_of ?f, ode_set odo X::'a set nres)  appr_relnres_rel"
  unfolding ode_set_def[abs_def]
  including art
  by autoref_monadic
concrete_definition ode_set_impl for E odoi Xi uses ode_set_impl
lemmas ode_set_impl_refine[autoref_rules] = ode_set_impl.refine[autoref_higher_order_rule (1)]
sublocale autoref_op_pat_def ode_set .

schematic_goal Picard_step_ivl_impl:
  fixes h::real
  assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) E"
  assumes [autoref_rules]: "(odoi, odo)  ode_ops_rel"
  assumes [autoref_rules]: "(X0i,X0)appr_rel" "(hi, h)  rnv_rel" "(t0i, t0)  rnv_rel" "(PHIi,PHI)appr_rel"
  notes [autoref_rules] = autoref_parameters
  shows "(nres_of ?f, Picard_step_ivl odo X0 t0 h PHI::'a set option nres)  appr_reloption_relnres_rel"
  unfolding autoref_tag_defs
  unfolding Picard_step_ivl_def
  including art
  by autoref_monadic
concrete_definition Picard_step_ivl_impl for X0i t0i hi PHIi uses Picard_step_ivl_impl
lemmas Picard_step_ivl_impl_refine[autoref_rules] =
  Picard_step_ivl_impl.refine[autoref_higher_order_rule (1)]
sublocale autoref_op_pat_def Picard_step_ivl .

lemma [autoref_rules]:
  "(abs, abs:: 'a  'a::executable_euclidean_space)  rnv_rel  rnv_rel"
  by simp_all

lemma widening_spec[autoref_rules]:
  "(λi. RETURN (widening_mod optns mod i = 0), do_widening_spec)  nat_rel  bool_relnres_rel"
  by (auto simp: do_widening_spec_def nres_rel_def)

schematic_goal P_iter_impl:
  fixes h::real and i::nat
  assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) E"
  assumes [autoref_rules]: "(odoi, odo)  ode_ops_rel"
  assumes [autoref_rules]: "(X0i,X0)appr_rel" "(PHIi,PHI)appr_rel"
    "(hi, h)  Id" "(i_i, i)  Id"
  notes [autoref_rules] = autoref_parameters
  shows "(nres_of (?f::?'r dres), P_iter odo X0 h i PHI::'a set option nres)  ?R"
  unfolding P_iter_def uncurry_rec_nat APP_def
  including art
  by autoref_monadic

concrete_definition P_iter_impl for E odoi X0i hi i_i PHIi uses P_iter_impl
lemmas [autoref_rules] = P_iter_impl.refine[autoref_higher_order_rule(1)]
sublocale autoref_op_pat_def P_iter .

schematic_goal cert_stepsize_impl_nres:
  fixes h::real and i n::nat
  assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) E"
  assumes [autoref_rules]:
    "(mi, m)(appr_rel  rnv_rel  rnv_rel  appr_rel  appr_rel ×r R option_relnres_rel)"
    "(X0i,X0)appr_rel" "(hi, h)  rnv_rel" "(ni, n)  nat_rel" "(i_i, i)  nat_rel"
  assumes [autoref_rules]: "(odoi, odo)  ode_ops_rel"
  shows "(?f::?'r nres, cert_stepsize odo m (X0::'a set) h n i)  ?R"
  unfolding cert_stepsize_def uncurry_rec_nat autoref_tag_defs
  by autoref
concrete_definition cert_stepsize_impl_nres for mi X0i hi ni i_i uses cert_stepsize_impl_nres
lemmas [autoref_rules] = cert_stepsize_impl_nres.refine[autoref_higher_order_rule(1)]
sublocale autoref_op_pat_def cert_stepsize .

schematic_goal cert_stepsize_impl_dres[refine_transfer]:
  assumes [refine_transfer]: "a b c d. nres_of (m a b c d)  m' a b c d"
  shows "nres_of ?f  cert_stepsize_impl_nres E odo m' x h n i"
  unfolding cert_stepsize_impl_nres_def
  by (refine_transfer)

concrete_definition cert_stepsize_impl_dres for E m x h n i uses cert_stepsize_impl_dres
lemmas [refine_transfer] = cert_stepsize_impl_dres.refine

lemma DIM_obvious[autoref_rules_raw]: "DIM_precond TYPE('a) DIM('a::executable_euclidean_space)"
  by auto

lemma default_reduce_argument_spec_impl[autoref_rules]:
  "(RETURN (default_reduce optns), default_reduce_argument_spec)  reduce_argument_rel TYPE('b)nres_rel"
  by (auto simp: nres_rel_def default_reduce_argument_spec_def reduce_argument_rel_def
      intro!: RETURN_RES_refine)

schematic_goal euler_step_impl:
  assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) E"
  assumes ncc: "ncc_precond TYPE('a::executable_euclidean_space)"
  notes [simp] = ncc_precondD[OF ncc]
  assumes [autoref_rules]: "(Xi, X)  appr_rel" "(hi, h)  Id"
  assumes [autoref_rules]: "(odoi, odo)  ode_ops_rel"
  shows "(nres_of (?f::?'r dres), euler_step odo (X::'a set) h)  ?R"
  unfolding one_step_def euler_step_def[abs_def]
  including art
  by autoref_monadic
concrete_definition euler_step_impl for odoi Xi hi uses euler_step_impl
lemmas [autoref_rules] = euler_step_impl.refine[autoref_higher_order_rule(1 2)]
sublocale autoref_op_pat_def euler_step .

schematic_goal rk2_step_impl:
  assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) E"
  assumes ncc: "ncc_precond TYPE('a::executable_euclidean_space)"
  assumes [autoref_rules]: "(Xi, X)  appr_rel" "(hi, h)  Id"
  notes [simp] = ncc_precondD[OF ncc]
  assumes [autoref_rules]: "(odoi, odo)  ode_ops_rel"
  shows "(nres_of (?f::?'r dres), rk2_step odo (X::'a set) h)  ?R"
  unfolding one_step_def rk2_step_def[abs_def]
  by autoref_monadic

concrete_definition rk2_step_impl for odoi Xi hi uses rk2_step_impl
lemmas [autoref_rules] = rk2_step_impl.refine[autoref_higher_order_rule (1 2)]
sublocale autoref_op_pat_def rk2_step .

schematic_goal choose_step_impl:
  assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) E"
  assumes [autoref_rules_raw]: "ncc_precond TYPE('a)"
  assumes [autoref_rules]: "(Xi, X)  appr_rel" "(hi, h)  rnv_rel"
  assumes [autoref_rules]: "(odoi, odo)  ode_ops_rel"
  shows "(nres_of (?f), choose_step odo (X::'a set) h)  rnv_rel ×r appr_rel ×r appr_rel ×r appr_relnres_rel"
  unfolding choose_step_def autoref_tag_defs if_distribR ncc_precond_def
  including art
  by autoref_monadic

concrete_definition choose_step_impl for Xi hi uses choose_step_impl
lemmas [autoref_rules] = choose_step_impl.refine[autoref_higher_order_rule (1 2)]
sublocale autoref_op_pat_def choose_step .

lemma [autoref_rules]: "(sgn, sgn)  rnv_rel  rnv_rel"
  by auto

schematic_goal strongest_direction_impl:
  assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) E"
  assumes [autoref_rules]: "(xs, x)  lv_rel"
  shows "(?f, strongest_direction (x::'a))  lv_rel ×r rnv_rel"
  unfolding strongest_direction_def
  including art
  by autoref
concrete_definition strongest_direction_impl for xs uses strongest_direction_impl
lemmas [autoref_rules] = strongest_direction_impl.refine[autoref_higher_order_rule (1)]
sublocale autoref_op_pat_def strongest_direction .

lemma [autoref_rules]:
  "(real_divl, real_divl)  nat_rel  rnv_rel  rnv_rel  rnv_rel"
  "(truncate_down, truncate_down)  nat_rel  rnv_rel  rnv_rel"
  "(eucl_truncate_down, eucl_truncate_down)  nat_rel  rnv_rel  rnv_rel"
  "(truncate_up, truncate_up)  nat_rel  rnv_rel  rnv_rel"
  "(eucl_truncate_up, eucl_truncate_up)  nat_rel  rnv_rel  rnv_rel"
  "(max, max)  rnv_rel  rnv_rel  rnv_rel"
  "(min, min)  rnv_rel  rnv_rel  rnv_rel"
  "((/), (/))  rnv_rel  rnv_rel  rnv_rel"
  "(lfloat10, lfloat10)  rnv_rel  float10_rel"
  "(ufloat10, ufloat10)  rnv_rel  float10_rel"
  "(shows_prec, shows_prec)  nat_rel  nat_rel  string_rel  string_rel"
  "(shows_prec, shows_prec)  nat_rel  int_rel  string_rel  string_rel"
  "(shows_prec, shows_prec)  nat_rel  float10_rel  string_rel  string_rel"
  "(int, int)  nat_rel  int_rel"
  by (auto simp: string_rel_def)

schematic_goal intersects_sctns_spec_impl:
  assumes [autoref_rules]: "(ai, a)  appr_rel"
  assumes sctns[autoref_rules]: "(sctnsi, sctns)  sctns_rel"
  notes [simp] = list_set_rel_finiteD[OF sctns]
  shows "(nres_of (?x::_ dres), intersects_sctns (a::'a::executable_euclidean_space set) sctns)  bool_relnres_rel"
  unfolding autoref_tag_defs
  unfolding intersects_sctns_def
  by autoref_monadic
concrete_definition intersects_sctns_spec_impl for ai sctnsi uses intersects_sctns_spec_impl
lemmas intersects_sctns_refine[autoref_rules] = intersects_sctns_spec_impl.refine[autoref_higher_order_rule]
sublocale autoref_op_pat_def intersects_sctns .

  assumes "GEN_OP ws width_spec (A  rnv_relnres_rel)"
  assumes "x. TRANSFER (RETURN (wsd x)  ws x)"
  shows width_spec_invar_rel[autoref_rules]:
    "(λ(a, b). RETURN (wsd a), width_spec)  S, Ainvar_rel b  rnv_relnres_rel"
    and width_spec_inter_rel[autoref_rules]:
    "(λ(a, b). RETURN (wsd a), width_spec)  S, Ainter_rel  rnv_relnres_rel"
  using assms
  by (auto simp: nres_rel_def width_spec_def invar_rel_def dest!: fun_relD)

lemma width_spec_coll[autoref_rules]:
  assumes "GEN_OP ws width_spec (A  rnv_relnres_rel)"
  assumes "x. TRANSFER (RETURN (wsd x)  ws x)"
  shows "(λxs. RETURN (sum_list (map wsd xs)), width_spec)  clw_rel A  rnv_relnres_rel"
  by (auto simp: nres_rel_def width_spec_def)

schematic_goal intersects_sections_spec_clw[autoref_rules]:
  assumes [autoref_rules]: "(Ri, R)  clw_rel appr_rel" "(sctnsi, sctns)  sctns_rel"
  shows "(nres_of (?r::_ dres), intersects_sctns_spec_clw $ R $ sctns)  bool_relnres_rel"
  unfolding intersects_sctns_spec_clw_def
  including art
  by autoref_monadic

schematic_goal nonzero_component_impl:
  assumes [autoref_rules]: "(Xi, X)  appr_rel" "(ni, n)  lv_rel" "(si, s)  string_rel"
  shows "(nres_of ?f, nonzero_component s X n)  unit_relnres_rel"
  unfolding nonzero_component_def autoref_tag_defs
  by autoref_monadic
concrete_definition nonzero_component_impl for si Xi ni uses nonzero_component_impl
lemmas nonzero_component_impl_refine[autoref_rules] = nonzero_component_impl.refine[autoref_higher_order_rule]
  assumes "xs  set_of_appr XS" "tXS = take d XS" "d < length xs"
  shows "take d xs  set_of_appr tXS"
  using set_of_appr_project[OF assms(1), of "[0..<d]"]
  apply (auto simp: assms take_eq_map_nth length_set_of_appr)
  using assms(1) assms(3) length_set_of_appr take_eq_map_nth by fastforce

lemma sv_appr_rell[relator_props]: "single_valued appr_rell"
  by (auto simp: appr_rell_internal)

lemma single_valued_union:
  shows "single_valued X  single_valued Y  Domain X  Domain Y = {}  single_valued (X  Y)"
  by (auto simp: single_valued_def)

lemma is_empty_ivl_rel[autoref_rules]:
  assumes le[THEN GEN_OP_D, param_fo]: "GEN_OP le (≤) (A  A  bool_rel)"
  shows "(λ(x, y). ¬ le x y, is_empty)  Aivl_rel  bool_rel"
  apply (auto simp: ivl_rel_def br_def set_of_ivl_def)
  subgoal premises prems for a b c d
    using le[OF prems(2, 3)] prems(1,4-) order_trans
    by auto
  subgoal premises prems for a b c d
    using le[OF prems(3,4)] prems(1,2) order_trans
    by auto

lemma real_autoref[autoref_rules]:
  "(real, real)  nat_rel  rnv_rel"
  by auto

lemma map_option_autoref[autoref_rules]: "(map_option, map_option)  (A  B)  Aoption_rel  Boption_rel"
  by (rule map_option_param)

lemma sv_plane_rel[relator_props]: "single_valued A  single_valued (Aplane_rel)"
  by (auto simp: plane_rel_def intro!: relator_props)
lemma sv_below_rel[relator_props]: "single_valued A  single_valued (Abelow_rel)"
  by (auto simp: below_rel_def intro!: relator_props)
lemma sv_sbelow_rel[relator_props]: "single_valued A  single_valued (Asbelow_rel)"
  by (auto simp: sbelow_rel_def intro!: relator_props)
lemma sv_sbelows_rel[relator_props]: "single_valued A  single_valued (Asbelows_rel)"
  by (auto simp: sbelows_rel_def intro!: relator_props)

lemma closed_ivl_rel[intro, simp]:  "(a, b)  lvivl_rel  closed b"
  by (auto simp: ivl_rel_def br_def set_of_ivl_def)

lemma [autoref_rules]:
  "(float_of, float_of)  rnv_rel  Id"
  "(approx, approx)  nat_rel  Id  Idoption_rellist_rel  Idoption_rel"
  by auto

lemma uninfo_autoref[autoref_rules]:
  assumes "PREFER single_valued X"
  assumes "PREFER single_valued R"
  shows "(map snd, uninfo)  clw_rel (R, Xinfo_rel)  clw_rel X"
  using assms
  apply (auto simp: lw_rel_def Union_rel_br info_rel_def br_chain br_rel_prod elim!: single_valued_as_brE
      dest!: brD
      intro!: brI)
  apply force
  apply force
  apply force

lemma [autoref_op_pat]: "(⊆)  OP op_subset_ivl"
  by (force intro!: eq_reflection)

lemma op_subset_ivl:
  assumes le[THEN GEN_OP_D, autoref_rules, param_fo]: "GEN_OP le (≤) (A  A  bool_rel)"
  shows "(λ(a, b) (c, d). le a b  le c a  le b d, op_subset_ivl)  Aivl_rel  Aivl_rel  bool_rel"
  apply (clarsimp dest!: brD simp: ivl_rel_def)
  subgoal for a b c d e f g h
    using le[of a c b d]
    using le[of e g a c]
    using le[of b d f h]
    by (auto simp: set_of_ivl_def)
concrete_definition op_subset_ivl_impl uses op_subset_ivl
lemmas [autoref_rules] = op_subset_ivl_impl.refine

lemma [autoref_op_pat]: "(=)  OP op_eq_ivl"
  by (force intro!: eq_reflection)
lemma eq_ivl_impl:
  assumes le[THEN GEN_OP_D, autoref_rules, param_fo]: "GEN_OP le (≤) (A  A  bool_rel)"
  shows "(λ(a, b) (c, d). (le a b  le c a  le b d)  (le c d  le a c  le d b), op_eq_ivl)  Aivl_rel  Aivl_rel  bool_rel"
  apply (clarsimp dest!: brD simp: )
  subgoal premises prems for a b c d e f
    using op_subset_ivl[param_fo, OF assms prems(1,2)]
      op_subset_ivl[param_fo, OF assms prems(2,1)]
    by auto
concrete_definition eq_ivl_impl uses eq_ivl_impl
lemmas [autoref_rules] = eq_ivl_impl.refine

lemma [autoref_rules]: "(RETURN, get_plane)  Aplane_rel  Asctn_relnres_rel"
  by (auto simp: plane_rel_def get_plane_def nres_rel_def dest!: brD intro!: RETURN_SPEC_refine)

lemma [autoref_op_pat_def del]: "get_inter p  OP (get_inter p)" by auto

lemma inform_autoref[autoref_rules]:
  "(λx. Max (abs ` set x), (infnorm::'a::executable_euclidean_spacereal))  lv_rel  rnv_rel"
  apply (auto simp: lv_rel_def br_def infnorm_def eucl_of_list_inner
      intro!: Max_eqI le_cSup_finite)
  subgoal for a y
    apply (rule exI[where x="Basis_list ! index a y"])
    by (auto simp: eucl_of_list_inner)
    apply (rule rev_subsetD)
     apply (rule closed_contains_Sup)
       apply (auto intro!: finite_imp_closed)
    apply (rule imageI)
    apply (auto simp: eucl_of_list_inner)

schematic_goal tolerate_error_impl:
  assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) dd"
  assumes [autoref_rules]: "(Yi, Y::'a::executable_euclidean_space set)  appr_rel"
  assumes [autoref_rules]: "(Ei, E)  appr_rel"
  shows "(nres_of ?r, tolerate_error Y E)  bool_rel ×r rnv_relnres_rel"
  unfolding tolerate_error_def
  including art
  by autoref_monadic
concrete_definition tolerate_error_impl for dd Yi Ei uses tolerate_error_impl
lemmas tolerate_error_refine[autoref_rules] = tolerate_error_impl.refine[autoref_higher_order_rule (1)]

lemma adapt_stepsize_fa_autoref[autoref_rules]:
  "(adapt_stepsize_fa, adapt_stepsize_fa)  rnv_rel  nat_rel  rnv_rel  rnv_rel  Id"
  by auto

  assumes "single_valued A"
  shows "(xs, X)  Alist_wset_rel  finite X"
  using assms
  by (auto simp: list_wset_rel_def set_rel_br dest!: brD elim!: single_valued_as_brE)

lemma [autoref_rules_raw del]: "(norm2_slp, norm2_slp)  nat_rel  Id"
  and [autoref_itype del]: "norm2_slp ::i i_nat i i_of_rel (Id::(floatarith list × floatarith list) set)"
  by auto

lemma [autoref_rules]: "(norm2_slp, norm2_slp)  nat_rel  slp_rel"
  by auto

lemma [autoref_rules_raw]: "DIM_precond TYPE(real) (Suc 0)"
  by auto
lemma [autoref_rules]:
  "(real_divr, real_divr)  nat_rel  rnv_rel  rnv_rel  rnv_rel"
  by auto

lemma length_norm2_slp_ge: "length (norm2_slp E)  1"
  unfolding norm2_slp_def
  by (auto simp: slp_of_fas_def split: prod.splits)

lemma blinfun_of_vmatrix_scaleR: "blinfun_of_vmatrix (c *R e) = c *R blinfun_of_vmatrix e"
  including blinfun.lifting
  by transfer (vector sum_distrib_left algebra_simps matrix_vector_mult_def fun_eq_iff)

lemma closed_clw_rel_iplane_rel:
  "(xi, x)  clw_rel (iplane_rel lvivl_rel)  closed x"
  unfolding lvivl_rel_br
  by (force simp: lv_rel_def plane_rel_br inter_rel_br clw_rel_br set_of_ivl_def
      dest!: brD)

lemma closed_ivl_prod3_list_rel:
  assumes "(y, x')  clw_rel (iplane_rel lvivl_rel) ×r A"
  assumes "(xa, x'a)  clw_rel (iplane_rel lvivl_rel) ×r Blist_rel"
  shows "(guard, ro)set (x' # x'a). closed guard"
  using assms closed_clw_rel_iplane_rel
  apply (auto simp: list_rel_def prod_rel_def in_set_conv_nth list_all2_conv_all_nth)
  apply (drule spec)
  by auto

  assumes "x xs a. snd (h x xs a) = snd a"
  shows "rec_list z (λx xs r xa. f x xs xa (r (h x xs xa))) xs ab =
    rec_list (λa. z (a, snd ab)) (λx xs r a. f x xs (a, snd ab) (r (fst (h x xs (a, snd ab))))) xs (fst ab)"
  using assms
  unfolding split_beta'
  by (induction xs arbitrary: ab) (auto simp: split_beta')

  assumes "x xs a. fst (h x xs a) = fst a"
  shows "rec_list z (λx xs r xa. f x xs xa (r (h x xs xa))) xs ab =
    rec_list (λb. z (fst ab, b)) (λx xs r b. f x xs (fst ab, b) (r (snd (h x xs (fst ab, b))))) xs (snd ab)"
  using assms
  unfolding split_beta'
  by (induction xs arbitrary: ab) (auto simp: split_beta')

lemma [autoref_itype]: "compact ::i A i i_bool"
  by auto

lemma lvivl_rel_compact[autoref_rules]:
  "(λ_::_×_. True, compact)  lvivl_rel  bool_rel"
  "(λ_::(_×_)list. True, compact)  clw_rel lvivl_rel  bool_rel"
  by (auto simp: lvivl_rel_br set_of_ivl_def lw_rel_def Union_rel_br dest!: brD)