Theory Concrete_Reachability_Analysis
theory Concrete_Reachability_Analysis
imports
Concrete_Rigorous_Numerics
Abstract_Reachability_Analysis
begin
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 → ⟨I⟩option_rel → unit_rel"
by auto
end
lemma [autoref_op_pat_def]:
includes autoref_syntax
shows
"(λ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 → ⟨A⟩option_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_rel⟩nres_rel"
"(RETURN (adaptive_atol optns), adaptive_atol_spec) ∈ ⟨rnv_rel⟩nres_rel"
"(RETURN (adaptive_rtol optns), adaptive_rtol_spec) ∈ ⟨rnv_rel⟩nres_rel"
"(RETURN (method_id optns), method_spec) ∈ ⟨nat_rel⟩nres_rel"
"(RETURN start_stepsize_impl, start_stepsize_spec) ∈ ⟨rnv_rel⟩nres_rel"
"(RETURN (iterations optns), iterations_spec) ∈ ⟨nat_rel⟩nres_rel"
"(RETURN (widening_mod optns), widening_mod_spec) ∈ ⟨nat_rel⟩nres_rel"
"(RETURN (halve_stepsizes optns), halve_stepsizes_spec) ∈ ⟨nat_rel⟩nres_rel"
"(RETURN (rk2_param_impl), rk2_param_spec) ∈ ⟨rnv_rel⟩nres_rel"
by (auto simp: nres_rel_def
precision_spec_def
adaptive_atol_spec_def
adaptive_rtol_spec_def
method_spec_def
start_stepsize_spec_def start_stepsize_impl_def
iterations_spec_def
widening_mod_spec_def
halve_stepsizes_spec_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_rel⟩nres_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_rel⟩nres_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_rel⟩list_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
ode_slps_of_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_rel⟩nres_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_rel⟩nres_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_rel⟩nres_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_rel⟩nres_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_rel⟩option_rel⟩nres_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_rel⟩nres_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_rel⟩nres_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_rel⟩nres_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_rel⟩nres_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 .
lemma
assumes "GEN_OP ws width_spec (A → ⟨rnv_rel⟩nres_rel)"
assumes "⋀x. TRANSFER (RETURN (wsd x) ≤ ws x)"
shows width_spec_invar_rel[autoref_rules]:
"(λ(a, b). RETURN (wsd a), width_spec) ∈ ⟨S, A⟩invar_rel b → ⟨rnv_rel⟩nres_rel"
and width_spec_inter_rel[autoref_rules]:
"(λ(a, b). RETURN (wsd a), width_spec) ∈ ⟨S, A⟩inter_rel → ⟨rnv_rel⟩nres_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_rel⟩nres_rel)"
assumes "⋀x. TRANSFER (RETURN (wsd x) ≤ ws x)"
shows "(λxs. RETURN (sum_list (map wsd xs)), width_spec) ∈ clw_rel A → ⟨rnv_rel⟩nres_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_rel⟩nres_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_rel⟩nres_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]
lemma
take_set_of_apprI:
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) ∈ ⟨A⟩ivl_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
done
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) → ⟨A⟩option_rel → ⟨B⟩option_rel"
by (rule map_option_param)
lemma sv_plane_rel[relator_props]: "single_valued A ⟹ single_valued (⟨A⟩plane_rel)"
by (auto simp: plane_rel_def intro!: relator_props)
lemma sv_below_rel[relator_props]: "single_valued A ⟹ single_valued (⟨A⟩below_rel)"
by (auto simp: below_rel_def intro!: relator_props)
lemma sv_sbelow_rel[relator_props]: "single_valued A ⟹ single_valued (⟨A⟩sbelow_rel)"
by (auto simp: sbelow_rel_def intro!: relator_props)
lemma sv_sbelows_rel[relator_props]: "single_valued A ⟹ single_valued (⟨A⟩sbelows_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 → ⟨⟨Id⟩option_rel⟩list_rel → ⟨Id⟩option_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, X⟩info_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
done
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) ∈ ⟨A⟩ivl_rel → ⟨A⟩ivl_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)
done
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) ∈ ⟨A⟩ivl_rel → ⟨A⟩ivl_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
done
concrete_definition eq_ivl_impl uses eq_ivl_impl
lemmas [autoref_rules] = eq_ivl_impl.refine
lemma [autoref_rules]: "(RETURN, get_plane) ∈ ⟨A⟩plane_rel → ⟨⟨A⟩sctn_rel⟩nres_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_space⇒real)) ∈ 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)
subgoal
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)
done
done
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_rel⟩nres_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
lemma
list_wset_rel_finite:
assumes "single_valued A"
shows "(xs, X) ∈ ⟨A⟩list_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 B⟩list_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
lemma
rec_list_fun_eq1:
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')
lemma
rec_list_fun_eq2:
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)
end
end