# Theory Refine_ScaleR2

```theory Refine_ScaleR2
imports
Refine_Unions
Refine_Interval
Refine_String
begin

definition "scaleR2 l u X = (λ(r, (x, y)). (x, r *⇩R y)) ` (ereal -` {l .. u} × X)"

lemma scaleR2_1_1[simp]: "scaleR2 1 1 = (λx::(_×'x::real_vector)set. x)"
by (force simp: scaleR2_def[abs_def] image_def vimage_def)

consts i_scaleR2::"interface⇒interface"

abbreviation "ereal_rel ≡ (Id::ereal rel)"

definition scaleR2_rel where scaleR2_rel_internal:
"scaleR2_rel A = ((ereal_rel ×⇩r ereal_rel) ×⇩r A) O
br (λ((l, u), X). scaleR2 l u X) (λ((l, u), _). ereal -` {l..u} ≠ {})"

definition [refine_vcg_def]: "scaleR2_rep X = SPEC (λ((l, u), Y). ereal -` {l..u} ≠ {} ∧ X = scaleR2 l u Y)"

definition [refine_vcg_def]: "scaleRe_ivl_spec l u X = SPEC (λY. Y = scaleR2 l u X)"

definition [simp]: "op_image_fst_colle = (`) fst"

definition [simp]: "op_image_fste = (`) fst"

definition "scaleR2_rep_coll X = do {
XS ← sets_of_coll X;
FORWEAK XS (RETURN ((0, 0), op_empty_coll)) (λX. do {
((l, u), Y) ← scaleR2_rep X;
RETURN ((l, u), mk_coll Y)
}) (λ((l, u), Y) ((l', u'), Y'). RETURN ((inf l' l, sup u' u), Y' ∪ Y))
}"

abbreviation "elvivl_rel ≡ ⟨lvivl_rel⟩scaleR2_rel"

definition [simp]: "op_times_UNIV_coll X = X × UNIV"

definition [simp]: "op_inter_fst X Y = X ∩ Y × UNIV"

definition "scaleRe_ivl_coll_spec l u X = do {
XS ← sets_of_coll X;
FORWEAK XS (RETURN op_empty_coll)
(λX. do {I ← scaleRe_ivl_spec l u X; RETURN (mk_coll I)})
(λX X'. RETURN (X' ∪ X))
}"

definition "op_inter_fst_ivl_scaleR2 X Y = do {
((l, u), X) ← scaleR2_rep X;
(i, s) ← ivl_rep (op_inter_fst X Y);
let R = op_inter_fst (op_atLeastAtMost_ivl i s) Y;
scaleRe_ivl_coll_spec l u (filter_empty_ivls (mk_coll R))
}"

definition "op_inter_fst_ivl_coll_scaleR2 X Y = do {
Xs ← sets_of_coll X;
FORWEAK Xs (RETURN op_empty_coll) (λX. op_inter_fst_ivl_scaleR2 X Y) (λX X'. RETURN (X' ∪ X))
}"

definition [refine_vcg_def]: "op_image_fst_ivl X = SPEC (λR. R = fst ` X)"

definition "op_image_fst_ivl_coll X = do {
Xs ← sets_of_coll X;
FORWEAK Xs (RETURN op_empty_coll) (λX. do {i ← op_image_fst_ivl X; RETURN (mk_coll i)}) (λX' X. RETURN (X' ∪ X))
}"

lemma scaleR2_rel_def:
"⟨A⟩scaleR2_rel = ((ereal_rel ×⇩r ereal_rel) ×⇩r A) O
br (λ((l, u), X). scaleR2 l u X) (λ((l, u), _). ereal -` {l..u} ≠ {})"
by (auto simp: relAPP_def scaleR2_rel_internal)
lemmas [autoref_rel_intf] = REL_INTFI[of scaleR2_rel i_scaleR2]

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_rel_br: "⟨br a I⟩scaleR2_rel =
br (λ((x, xa), y). scaleR2 x xa (a y)) (λ((l, u), y). I y ∧ ereal -` {l..u} ≠ {})"
unfolding scaleR2_rel_def
unfolding Id_br br_rel_prod br_chain o_def
by (auto simp: split_beta')

context includes autoref_syntax begin

lemma [autoref_rules]:
"(sup, sup) ∈ ereal_rel → ereal_rel → ereal_rel"
"(inf, inf) ∈ ereal_rel → ereal_rel → ereal_rel"
by auto

lemma [autoref_rules]:
"(ereal, ereal) ∈ rnv_rel → ereal_rel"
"((*), (*)) ∈ ereal_rel → ereal_rel → ereal_rel"
by auto

lemma [autoref_rules]: "(∞, ∞) ∈ ereal_rel"
by auto

lemma lift_scaleR2:
"(λ(lu, x). (lu, fi x), f) ∈ ⟨A⟩scaleR2_rel → ⟨B⟩scaleR2_rel"
if "(fi, f) ∈ A → B"
"⋀l u x. x ∈ Range A ⟹ ereal -` {l..u} ≠ {} ⟹ scaleR2 l u (f x) = f (scaleR2 l u x)"
using that
apply (auto simp: scaleR2_rel_def )
apply (rule relcompI)
apply (rule prod_relI)
apply (rule IdI)
apply (drule fun_relD, assumption, assumption)
apply (auto simp: br_def vimage_def)
done

lemma appr1e_rep_impl[autoref_rules]:
"(λx. RETURN x, scaleR2_rep) ∈ ⟨A⟩scaleR2_rel → ⟨(ereal_rel ×⇩r ereal_rel) ×⇩r A⟩nres_rel"
by (force simp: nres_rel_def scaleR2_rep_def scaleR2_rel_def image_image split_beta'
dest!: brD intro!: RETURN_SPEC_refine)

lemma [autoref_op_pat]: "fst ` X ≡ (OP op_image_fst_colle) \$ X"
by auto

lemma [autoref_op_pat]: "fst ` X ≡ (OP op_image_fste) \$ X"
by simp

lemma scaleRe_ivl_impl[autoref_rules]:
"(λl u X. if l < u ∨ l > - ∞ ∧ l ≤ u ∧ u < ∞ then RETURN ((l, u), X) else SUCCEED,
scaleRe_ivl_spec) ∈ ereal_rel → ereal_rel → A → ⟨⟨A⟩scaleR2_rel⟩nres_rel"
apply (auto simp: scaleRe_ivl_spec_def scaleR2_rep_def scaleR2_rel_def nres_rel_def
RETURN_RES_refine_iff
intro!: RETURN_SPEC_refine )
apply (rule relcompI)
apply (rule prod_relI)
apply (rule IdI)
apply assumption defer
apply (rule relcompI)
apply (rule prod_relI)
apply (rule IdI)
apply assumption defer
apply (auto intro!: brI)
subgoal for a b c d
apply (cases a; cases b)
by (auto simp: vimage_def)
subgoal for a b c d
apply (cases a; cases b)
by (auto simp: vimage_def)
done

lemma is_empty_scaleR2_rel[autoref_rules]:
assumes "GEN_OP ie is_empty (A → bool_rel)"
shows "(λ(_, b). ie b, is_empty) ∈ (⟨A⟩scaleR2_rel → bool_rel)"
using assms[THEN GEN_OP_D, param_fo]
by (auto simp: scaleR2_rep_def scaleR2_rel_def  scaleR2_def vimage_def
dest!: brD)

lemma sv_appr1e_rel[relator_props]: "single_valued A ⟹ single_valued (⟨A⟩scaleR2_rel)"
by (auto simp: scaleR2_rep_def scaleR2_rel_def intro!: relator_props)

schematic_goal scaleR2_rep_coll_impl:
assumes [THEN PREFER_sv_D, relator_props]: "PREFER single_valued A"
assumes [autoref_rules]: "(ai, a) ∈ clw_rel (⟨A⟩scaleR2_rel)"
shows "(nres_of ?r, scaleR2_rep_coll a) ∈ ⟨(ereal_rel ×⇩r ereal_rel) ×⇩r clw_rel A⟩nres_rel"
unfolding scaleR2_rep_coll_def
including art
concrete_definition scaleR2_rep_coll_impl for ai uses scaleR2_rep_coll_impl
lemmas scaleR2_rep_coll_impl_refine[autoref_rules] =
scaleR2_rep_coll_impl.refine[autoref_higher_order_rule (1)]

lemma fst_imageIcc:
"fst ` {a::'a::ordered_euclidean_space×'c::ordered_euclidean_space .. b} =
(if a ≤ b then {fst a .. fst b} else {})"
by (auto intro!: simp: less_eq_prod_def)

lemma
interval_inter_times_UNIVI:
assumes "{fst a .. fst b} ∩ {c .. d} = {fst e .. fst f}"
assumes "{snd a .. snd b} = {snd e .. snd f}"
shows "{a::('a::ordered_euclidean_space × 'c::ordered_euclidean_space) .. b} ∩
({c .. d} × UNIV) = {e .. f}"
using assms
by (cases a; cases b; cases e; cases f) (auto simp: subset_iff set_eq_iff)

lemma op_inter_fst_impl:
assumes "DIM_precond TYPE('a::executable_euclidean_space) D"
assumes "GEN_OP intr (op_inter_ivl::('a) set⇒_) (lvivl_rel → lvivl_rel → lvivl_rel)"
assumes "GEN_OP le   ((≤) ::'a×('b::executable_euclidean_space) ⇒_) (lv_rel → lv_rel → bool_rel)"
shows "(λx y.
if le (fst x) (snd x) then
case (intr (pairself (take D) x) y, pairself (drop D) x) of
((i, s), j, t) ⇒ (i @ j, s @ t)
else x,
op_inter_fst::('a × 'b) set ⇒ 'a set ⇒ ('a × 'b) set) ∈ lvivl_rel → lvivl_rel → lvivl_rel"
proof (auto simp: split: prod.splits, goal_cases)
case (1 a b c d e f g h)
from 1 have lens: "length a = DIM('a) + DIM('b)" "length b = DIM('a) + DIM('b)"
by (auto simp: lvivl_rel_br br_def)
have f_eq: "f = {eucl_of_list d .. eucl_of_list e}"
and c_eq: "c = {eucl_of_list a .. eucl_of_list b}"
using 1
by (auto simp: lvivl_rel_br br_def set_of_ivl_def)
from 1 assms(1,2) assms(3)[THEN GEN_OP_D, param_fo, OF lv_relI lv_relI, of a b]
have "((take D a, take D b), fst ` c) ∈ ⟨lv_rel⟩ivl_rel"
apply (auto simp: lv_rel_def ivl_rel_def dest!: brD)
apply (rule relcompI)
apply (rule prod_relI)
apply (rule brI)
apply (rule refl)
apply (simp;fail)
apply (rule brI)
apply (rule refl)
apply (simp;fail)
apply (rule brI)
by (auto simp: eucl_of_list_prod)
from assms(1) assms(2)[THEN GEN_OP_D, param_fo, OF this 1(2)]
show ?case
unfolding 1
apply (auto simp: lv_rel_def ivl_rel_def dest!: brD)
apply (rule relcompI)
apply (rule prod_relI)
apply (rule brI)
apply (rule refl)
apply (rule brI)
apply (rule refl)
apply (rule brI)
defer apply (simp; fail)
apply (cases "(eucl_of_list (take DIM('a) a)::'a) ≤ eucl_of_list (take DIM('a) b) ∧
(eucl_of_list (drop DIM('a) a)::'b) ≤ eucl_of_list (drop DIM('a) b)")
subgoal apply (simp split: if_splits add: c_eq f_eq)
apply (rule interval_inter_times_UNIVI)
by (auto simp: eucl_of_list_prod fst_imageIcc split: if_splits)
subgoal
by (auto simp: eucl_of_list_prod fst_imageIcc c_eq f_eq)
done
next
case (2 a b c d e f g h)
from assms(3)[THEN GEN_OP_D, param_fo, OF lv_relI lv_relI, of a b] assms(1) 2
show ?case
apply (auto simp: lv_rel_def ivl_rel_def dest!: brD)
apply (rule relcompI)
apply (rule prod_relI)
apply (rule brI)
apply (rule refl)
apply (simp;fail)
apply (rule brI)
apply (rule refl)
apply (simp;fail)
apply (rule brI)
apply (simp; fail)
done
qed
concrete_definition op_inter_fst_impl uses op_inter_fst_impl
lemmas [autoref_rules] = op_inter_fst_impl.refine

definition "op_inter_fst_coll XS Y = do {
XS ← sets_of_coll XS;
FORWEAK XS (RETURN op_empty_coll) (λX. RETURN (mk_coll (op_inter_fst X Y))) (λX X'. RETURN (X' ∪ X))
}"

schematic_goal op_inter_fst_coll_impl:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) D"
assumes [THEN GEN_OP_D, autoref_rules]: "GEN_OP le ((≤) ::'a×'b::executable_euclidean_space ⇒_) (lv_rel → lv_rel → bool_rel)"
assumes [autoref_rules]: "(XSi, XS::('a × 'b) set) ∈ clw_rel lvivl_rel"
"(Yi, Y::'a set) ∈ lvivl_rel"
shows "(nres_of ?r, op_inter_fst_coll XS Y) ∈ ⟨clw_rel lvivl_rel⟩nres_rel"
unfolding op_inter_fst_coll_def
concrete_definition op_inter_fst_coll_impl uses op_inter_fst_coll_impl
lemmas op_inter_fst_coll_impl_refine[autoref_rules] =
op_inter_fst_coll_impl.refine[autoref_higher_order_rule(1 2)]

lemma [autoref_op_pat]: "X ∩ Y × UNIV ≡ OP op_inter_fst \$ X \$ Y"
by auto

schematic_goal scaleRe_ivl_coll_impl:
assumes [relator_props]: "single_valued A"
assumes [autoref_rules]: "(li, l) ∈ ereal_rel" "(ui, u) ∈ ereal_rel" "(Xi, X) ∈ clw_rel A"
shows "(nres_of ?r, scaleRe_ivl_coll_spec l u X) ∈ ⟨clw_rel (⟨A⟩scaleR2_rel)⟩nres_rel"
unfolding scaleRe_ivl_coll_spec_def
including art
concrete_definition scaleRe_ivl_coll_impl uses scaleRe_ivl_coll_impl
lemma scaleRe_ivl_coll_impl_refine[autoref_rules]:
"PREFER single_valued A ⟹
(λli ui Xi. nres_of (scaleRe_ivl_coll_impl li ui Xi), scaleRe_ivl_coll_spec)
∈ ereal_rel → ereal_rel → clw_rel A → ⟨clw_rel (⟨A⟩scaleR2_rel)⟩nres_rel"
using scaleRe_ivl_coll_impl.refine by force

schematic_goal op_inter_fst_ivl_scaleR2_impl:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) E"
assumes [THEN GEN_OP_D, autoref_rules]: "GEN_OP le ((≤) ::'a×'b::executable_euclidean_space ⇒_) (lv_rel → lv_rel → bool_rel)"
assumes [autoref_rules]: "(XSi, XS::('a×'b) set) ∈ elvivl_rel"
"(Yi, Y::'a set) ∈ lvivl_rel"
shows "(nres_of ?r, op_inter_fst_ivl_scaleR2 XS Y) ∈ ⟨clw_rel elvivl_rel⟩nres_rel"
unfolding op_inter_fst_ivl_scaleR2_def
including art
concrete_definition op_inter_fst_ivl_scaleR2_impl uses op_inter_fst_ivl_scaleR2_impl
lemmas op_inter_fst_ivl_scaleR2_impl_refine[autoref_rules] =
op_inter_fst_ivl_scaleR2_impl.refine[autoref_higher_order_rule(1 2)]

schematic_goal op_inter_fst_ivl_coll_scaleR2_impl:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) E"
assumes [THEN GEN_OP_D, autoref_rules]: "GEN_OP le ((≤) ::'a×'b::executable_euclidean_space ⇒_) (lv_rel → lv_rel → bool_rel)"
assumes [autoref_rules]: "(XSi, XS::('a×'b) set) ∈ clw_rel elvivl_rel"
"(Yi, Y::'a set) ∈ lvivl_rel"
shows "(nres_of ?r, op_inter_fst_ivl_coll_scaleR2 XS Y) ∈ ⟨clw_rel elvivl_rel⟩nres_rel"
unfolding op_inter_fst_ivl_coll_scaleR2_def
including art
concrete_definition op_inter_fst_ivl_coll_scaleR2_impl uses op_inter_fst_ivl_coll_scaleR2_impl
lemmas op_inter_fst_ivl_coll_scaleR2_impl_refine[autoref_rules]
= op_inter_fst_ivl_coll_scaleR2_impl.refine[autoref_higher_order_rule(1 2)]

definition "op_inter_ivl_coll_scaleR2 X Y = do {
eivls ← op_inter_fst_ivl_coll_scaleR2 X Y;
((l, u), ivls) ← scaleR2_rep_coll eivls;
ivl ← op_ivl_of_ivl_coll ivls;
let R = op_inter_fst ivl Y;
scaleRe_ivl_coll_spec l u (filter_empty_ivls (mk_coll R))
}"

definition "op_single_inter_ivl a fxs = do {
let isa = (op_inter_ivl_coll (fxs:::clw_rel lvivl_rel) (a:::lvivl_rel));
(if op_coll_is_empty isa then RETURN op_empty_coll else do {
ivl ← op_ivl_of_ivl_coll isa;
RETURN (mk_coll ((ivl:::lvivl_rel) ∩ a))
})
}"

schematic_goal op_inter_ivl_coll_scaleR2_impl:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) D"
assumes [autoref_rules_raw]: "DIM_precond TYPE('b::executable_euclidean_space) E"
assumes [THEN GEN_OP_D, autoref_rules]: "GEN_OP le ((≤) ::'a×'b::executable_euclidean_space ⇒_) (lv_rel → lv_rel → bool_rel)"
assumes [autoref_rules]: "(XSi, XS::('a×'b) set) ∈ clw_rel elvivl_rel"
"(Yi, Y::'a set) ∈ lvivl_rel"
shows "(nres_of ?r, op_inter_ivl_coll_scaleR2 XS Y) ∈ ⟨clw_rel elvivl_rel⟩nres_rel"
unfolding op_inter_ivl_coll_scaleR2_def
including art
concrete_definition op_inter_ivl_coll_scaleR2_impl uses op_inter_ivl_coll_scaleR2_impl
lemmas op_inter_ivl_coll_scaleR2_impl_refine[autoref_rules] =
op_inter_ivl_coll_scaleR2_impl.refine[autoref_higher_order_rule(1 2 3)]

lemma op_image_fst_ivl[autoref_rules]:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) D"
assumes [THEN GEN_OP_D, autoref_rules]: "GEN_OP le ((≤) ::'a×'b::executable_euclidean_space ⇒_) (lv_rel → lv_rel → bool_rel)"
shows "(λ(l,u). nres_of (if le l u then dRETURN (pairself (take D) (l, u)) else dSUCCEED)
, op_image_fst_ivl::('a×'b) set⇒_) ∈ lvivl_rel → ⟨lvivl_rel⟩nres_rel"
using assms
apply (auto simp: ivl_rel_def nres_rel_def op_image_fst_ivl_def RETURN_RES_refine_iff
dest!: brD intro!: )
apply (rule relcompI)
apply (rule prod_relI)
apply (rule lv_relI)
apply (rule lv_relI)
apply (rule brI)
subgoal for a b
apply (drule fun_relD)
apply (rule lv_relI[where x=a])
apply (drule fun_relD)
apply (rule lv_relI[where x=b])
apply (auto simp: set_of_ivl_def lv_rel_def br_def fst_imageIcc eucl_of_list_prod)
done
subgoal by simp
done

schematic_goal op_image_fst_ivl_coll_impl[autoref_rules]:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) D"
assumes "GEN_OP le ((≤) ::'a×'b::executable_euclidean_space ⇒_) (lv_rel → lv_rel → bool_rel)"
assumes [autoref_rules]: "(Xi, X) ∈ clw_rel lvivl_rel"
shows "(nres_of ?r, (op_image_fst_ivl_coll::('a×'b) set⇒_) X) ∈ ⟨clw_rel lvivl_rel⟩nres_rel"
unfolding op_image_fst_ivl_coll_def
concrete_definition op_image_fst_ivl_coll_impl uses op_image_fst_ivl_coll_impl
lemmas op_image_fst_ivl_coll_impl_refine[autoref_rules] =
op_image_fst_ivl_coll_impl.refine[autoref_higher_order_rule(1 2)]

schematic_goal op_single_inter_ivl_impl:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) D"
assumes [autoref_rules]: "(FXSi, FXS) ∈ clw_rel lvivl_rel" "(Ai, A::'a set) ∈ lvivl_rel"
shows "(nres_of ?r, op_single_inter_ivl A FXS) ∈ ⟨clw_rel lvivl_rel⟩nres_rel"
unfolding op_single_inter_ivl_def
concrete_definition op_single_inter_ivl_impl for Ai FXSi uses op_single_inter_ivl_impl
lemmas op_single_inter_ivl_impl_refine[autoref_rules]
= op_single_inter_ivl_impl.refine[autoref_higher_order_rule (1)]

definition [refine_vcg_def]: "le_post_inter_granularity_op ro r = SPEC(λx::bool. True)"

lemma le_post_inter_granularity_op_itype[autoref_itype]:
"le_post_inter_granularity_op ::⇩i A →⇩i ⟨i_rnv⟩⇩ii_ivl →⇩i ⟨i_bool⟩⇩ii_nres"
by auto

definition partition_ivle::
"_ ⇒ ('a::executable_euclidean_space × 'c::executable_euclidean_space) set ⇒ _ set nres"
where
"partition_ivle ro xse =
(if op_coll_is_empty xse then RETURN (op_empty_coll:::clw_rel (elvivl_rel)) else do {
(_, xs) ← scaleR2_rep_coll xse;
xsf ← op_image_fst_ivl_coll xs;
r ← op_ivl_of_ivl_coll (xsf:::clw_rel (lvivl_rel));
(i, s) ← ivl_rep r;
CHECK (λ_. ()) (i ≤ s);
(rs, ps) ←
WHILE⇗(λ(rs, ps). xse ⊆ (rs × UNIV) ∪ ps)⇖ (λ(rs, ps). ¬ op_coll_is_empty (rs:::clw_rel lvivl_rel))
(λ(rs, ps).
do {
(r, rs') ← (split_spec_exact rs:::⟨lvivl_rel ×⇩r clw_rel lvivl_rel⟩nres_rel);
okay ← le_post_inter_granularity_op ro r;
if okay then do {
I ← op_inter_ivl_coll_scaleR2 (xse) (r);
RETURN (rs', I ∪ ps)
} else do {
(a, b) ← split_spec_ivl DIM('a) r;
fxs ← op_image_fst_ivl_coll xs;
ra' ← op_single_inter_ivl a fxs;
rb' ← op_single_inter_ivl b fxs;
RETURN (ra' ∪ rb' ∪ rs', ps)
}
}) (mk_coll r:::clw_rel lvivl_rel, op_empty_coll :::clw_rel elvivl_rel);
RETURN ps
})"

schematic_goal partition_ivle_nres:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) F"
assumes [autoref_rules_raw]: "DIM_precond TYPE('c::executable_euclidean_space) E"
assumes okgs[THEN GEN_OP_D, autoref_rules]:
"GEN_OP okay_granularityi (le_post_inter_granularity_op::_⇒'a set⇒_) (A → lvivl_rel → ⟨bool_rel⟩nres_rel)"
assumes [unfolded autoref_tag_defs, refine_transfer]:
"⋀ro X. TRANSFER (nres_of (okay_granularityd ro X) ≤ okay_granularityi ro X)"
assumes [autoref_rules]:
"(xsi, xs::('a×'c::executable_euclidean_space) set)∈ clw_rel elvivl_rel"
assumes [autoref_rules]: "(roi, ro) ∈ A"
shows "(nres_of ?f, partition_ivle ro xs)∈⟨clw_rel elvivl_rel⟩nres_rel"
unfolding partition_ivle_def[abs_def]
including art
concrete_definition partition_ivle_nres for okay_granularityd xsi uses partition_ivle_nres
lemmas [autoref_rules] = partition_ivle_nres.refine[autoref_higher_order_rule(1 2 3 4)]

definition "reduce_ivl (X::('a::executable_euclidean_space×'b::executable_euclidean_space)set) b = do {
(i, s) ← ivl_rep X;
CHECK (λ_. ST ''reduce_ivl strange basis'') (b ∈ set Basis_list);
CHECK (λ_. ST ''reduce_ivl strange ivl'') (i ≤ s);
let (i0, i1) = split_lv_rel i;
let (s0, s1) = split_lv_rel s;
let ivl2 = op_atLeastAtMost_ivl i1 s1;
P ← project_set_ivl ivl2 b 0;
(iP, sP) ← ivl_rep P;
if iP ≤ 0 ∧ 0 ≤ sP then
if i1 ∙ b > 0 then do {
let s = (i1 ∙ b) *⇩R b;
let P' = op_atLeastAtMost_ivl (Pair_lv_rel i0 (iP + s)) (Pair_lv_rel s0 (sP + s));
scaleRe_ivl_spec 1 ∞ P'
} else if s1 ∙ b < 0 then do {
let s = (s1 ∙ b) *⇩R b;
let P' = op_atLeastAtMost_ivl (Pair_lv_rel i0 (iP + s)) (Pair_lv_rel s0 (sP + s));
scaleRe_ivl_spec 1 ∞ P'
} else scaleRe_ivl_spec 1 1 X
else scaleRe_ivl_spec 1 1 X
}"

definition "reduce_ivle Y b = do {
((l, u), X) ← scaleR2_rep Y;
R ← reduce_ivl X b;
((l', u'), R) ← scaleR2_rep R;
CHECK (λ_. ()) (0 < l' ∧ 0 < l ∧ 0 ≤ u ∧ l ≤ u ∧ l' ≤ u');
scaleRe_ivl_spec (l'*l) (u' * u) R
}"

definition "reduces_ivle (X::('a::executable_euclidean_space×'b::executable_euclidean_space)set) =
FOREACH⇗λB R. X ⊆ R⇖ (set Basis_list:::⟨lv_rel⟩list_set_rel) (λb X. reduce_ivle X b) X"

definition "setse_of_ivlse (X:: ('a::executable_euclidean_space × 'c::executable_euclidean_space) set) = do {
Xs ← sets_of_coll X;
FORWEAK Xs (RETURN op_empty_coll) (λX. do {
((l, u), x) ← scaleR2_rep X;
(i, s) ← ivl_rep x;
if i ≤ s then do {
x ← scaleRe_ivl_spec l u {i .. s};
RETURN (mk_coll x)
} else RETURN op_empty_coll
}) (λX' X. RETURN (X' ∪ X))
}"

schematic_goal reduce_ivl_impl:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) D"
assumes [autoref_rules_raw]: "DIM_precond TYPE('b::executable_euclidean_space) E"
assumes [autoref_rules]:
"(Yi, Y::('a×'b::executable_euclidean_space) set) ∈ lvivl_rel"
"(bi, b::'b) ∈ lv_rel"
shows "(nres_of ?r, reduce_ivl Y b) ∈ ⟨elvivl_rel⟩nres_rel"
unfolding autoref_tag_defs
unfolding reduce_ivl_def
including art
concrete_definition reduce_ivl_impl for Yi bi uses reduce_ivl_impl
lemmas [autoref_rules] = reduce_ivl_impl.refine[autoref_higher_order_rule(1 2)]

schematic_goal reduce_ivle_impl:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) D"
assumes [autoref_rules_raw]: "DIM_precond TYPE('b::executable_euclidean_space) E"
assumes [autoref_rules]:
"(Yi, Y::('a×'b::executable_euclidean_space) set) ∈ elvivl_rel"
"(bi, b::'b) ∈ lv_rel"
shows "(nres_of ?r, reduce_ivle Y b) ∈ ⟨elvivl_rel⟩nres_rel"
unfolding autoref_tag_defs
unfolding reduce_ivle_def
including art
concrete_definition reduce_ivle_impl for Yi bi uses reduce_ivle_impl
lemmas [autoref_rules] = reduce_ivle_impl.refine[autoref_higher_order_rule(1 2)]

schematic_goal reduces_ivle_impl:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) D"
assumes [autoref_rules_raw]: "DIM_precond TYPE('b::executable_euclidean_space) E"
assumes [autoref_rules]: "(Yi, Y::('a×'b::executable_euclidean_space) set) ∈ elvivl_rel"
shows "(nres_of ?r, reduces_ivle Y) ∈ ⟨elvivl_rel⟩nres_rel"
unfolding autoref_tag_defs
unfolding reduces_ivle_def
including art
concrete_definition reduces_ivle_impl for Yi uses reduces_ivle_impl
lemmas [autoref_rules] = reduces_ivle_impl.refine[autoref_higher_order_rule(1 2)]

lemma scaleR2_subset:
assumes "x ∈ scaleR2 i' j' k'"
assumes "i ≤ i'" "j' ≤ j" "k' ⊆ k"
shows "x ∈ scaleR2 i j k"
using assms
by (force simp: scaleR2_def vimage_def image_def)

lemma subset_scaleR2_fstD: "X ⊆ scaleR2 l u Y ⟹ fst ` X ⊆ fst ` Y"
by (force simp: scaleR2_def subset_iff image_def vimage_def)

lemma mem_scaleR2_union[simp]: "x ∈ scaleR2 l u (A ∪ B) ⟷ x ∈ scaleR2 l u A ∨ x ∈ scaleR2 l u B"
by (force simp: scaleR2_def vimage_def image_def)

lemma scaleR2_empty[simp]: "scaleR2 l u {} = {}"
by (auto simp: scaleR2_def)

lemma scaleR2_eq_empty_iff:
"scaleR2 l u X = {} ⟷ X = {} ∨ ereal -` {l..u} = {}"
by (auto simp: scaleR2_def)

lemma scaleR2_id[simp]: "scaleR2 (1::ereal) 1 = (λ(x::('d × 'c::real_vector) set). x)"
by (rule scaleR2_1_1)

end

end```