# Theory Refine_Interval

```theory
Refine_Interval
imports
Refine_Unions
Refine_Vector_List
Refine_Hyperplane
Refine_Invar
begin

subsubsection ‹interval approximation of many›

definition ivl_rep_of_sets::"'a::lattice set set ⇒ ('a × 'a) nres" where
"ivl_rep_of_sets (XS::'a set set) = SPEC (λ(i, s). i ≤ s ∧ (∀X∈XS. X ⊆ {i..s}))"
lemmas [refine_vcg] = ivl_rep_of_sets_def[THEN eq_refl, THEN order.trans]

subsection ‹Interval representation›

consts i_ivl::"interface ⇒ interface"

context includes autoref_syntax begin

definition "set_of_ivl x = {fst x .. snd x}"

definition "set_of_lvivl ivl = (set_of_ivl (map_prod eucl_of_list eucl_of_list ivl)::'a::executable_euclidean_space set)"

definition ivl_rel::"('a × 'b::ordered_euclidean_space) set ⇒ (('a × 'a) × 'b set) set" where
ivl_rel_internal: "ivl_rel S = (S ×⇩r S) O br set_of_ivl top"
lemma ivl_rel_def: "⟨S⟩ivl_rel = (S ×⇩r S) O br set_of_ivl top"
unfolding relAPP_def ivl_rel_internal ..

lemmas [autoref_rel_intf] = REL_INTFI[of "ivl_rel" "i_ivl"]

lemma ivl_rel_sv[relator_props]: "single_valued R ⟹ single_valued (⟨R⟩ivl_rel)"
unfolding relAPP_def
by (auto simp: ivl_rel_internal intro!: relator_props)

definition [simp]: "op_atLeastAtMost_ivl = atLeastAtMost"
lemma [autoref_op_pat]: "atLeastAtMost ≡ OP op_atLeastAtMost_ivl"
by simp

lemma atLeastAtMost_ivlrel[autoref_rules]:
"(Pair, op_atLeastAtMost_ivl) ∈ A → A → ⟨A⟩ivl_rel"
by (auto simp: br_def set_of_ivl_def ivl_rel_def intro!: prod_relI)

definition [refine_vcg_def]: "ivl_rep X = SPEC (λ(l, u). X = {l .. u})"

lemma ivl_rep_autoref[autoref_rules]: "(RETURN, ivl_rep) ∈ ⟨A⟩ivl_rel → ⟨A ×⇩r A⟩nres_rel"
by (force intro!: nres_relI RETURN_SPEC_refine simp: ivl_rep_def ivl_rel_def br_def set_of_ivl_def)

lemma Inf_ivl_rel[autoref_rules]:
fixes X::"'a::ordered_euclidean_space set"
assumes "SIDE_PRECOND (X ≠ {})"
assumes "(Xi, X) ∈ ⟨A⟩ivl_rel"
shows "(fst Xi, Inf \$ X) ∈ A"
using assms
by (auto simp: ivl_rel_def br_def set_of_ivl_def)

lemma Sup_ivl_rel[autoref_rules]:
fixes X::"'a::ordered_euclidean_space set"
assumes "SIDE_PRECOND (X ≠ {})"
assumes "(Xi, X) ∈ ⟨A⟩ivl_rel"
shows "(snd Xi, Sup \$ X) ∈ A"
using assms
by (auto simp: ivl_rel_def br_def set_of_ivl_def)

definition "filter_empty_ivls_impl le ivls = [(i, s) ← ivls. le i s]"

lemma filter_empty_ivls_impl_simps[simp]:
shows
"filter_empty_ivls_impl le [] = []"
"filter_empty_ivls_impl le (a # xs) =
(if le (fst a) (snd a) then a#filter_empty_ivls_impl le xs else filter_empty_ivls_impl le xs)"
by (auto simp: filter_empty_ivls_impl_def)

definition [simp]: "filter_empty_ivls X = X"

lemma clw_rel_empty_iff:
assumes "single_valued A"
assumes "(x, {}) ∈ A" "(xs, X) ∈ clw_rel A"
shows "(x#xs, X) ∈ clw_rel A"
using assms
by (auto simp: lw_rel_def Union_rel_br elim!: single_valued_as_brE) (auto simp: br_def)

lemma
empty_ivl_relD:
"(a, Y) ∈ ⟨A⟩ivl_rel ⟹ single_valued A ⟹ (le, (≤)) ∈ A → A → bool_rel ⟹ ¬ le (fst a) (snd a) ⟹ Y = {}"
by (fastforce simp: ivl_rel_def br_def set_of_ivl_def dest: fun_relD )

lemma union_clw_relI: "(set xs, YS) ∈ ⟨A⟩set_rel ⟹ (xs, ⋃YS) ∈ clw_rel (A)"
apply (auto simp: clw_rel_def br_def )
apply (auto simp: lw_rel_def Union_rel_br set_rel_def )
apply (auto simp: br_def)
done

lemma filter_empty_ivls_impl_mem_clw_rel_ivl_rel_iff:
"(filter_empty_ivls_impl (≤) xs, X) ∈ clw_rel (⟨rnv_rel⟩ivl_rel) ⟷ (xs, X) ∈ clw_rel (⟨rnv_rel⟩ivl_rel)"
by (force simp: lw_rel_def ivl_rel_def Union_rel_br filter_empty_ivls_impl_def
set_of_ivl_def dest!: brD intro!: brI)

lemma filter_empty_ivls_eucl:
"(filter_empty_ivls_impl (≤), filter_empty_ivls) ∈ clw_rel (⟨rnv_rel⟩ivl_rel) → clw_rel (⟨rnv_rel⟩ivl_rel)"
by (auto simp: filter_empty_ivls_impl_mem_clw_rel_ivl_rel_iff)

lemma filter_param[param]:
"(filter, filter) ∈ (A → bool_rel) → ⟨A⟩list_rel → ⟨A⟩list_rel"
unfolding List.filter_def[abs_def]
by parametricity

lemma prod_rel_comp_ivl_rel:
assumes "single_valued A" "single_valued B"
shows "(A ×⇩r A) O ⟨B⟩ivl_rel = ⟨A O B⟩ivl_rel"
using assms
by (auto simp: ivl_rel_def set_of_ivl_def br_chain br_rel_prod
elim!: single_valued_as_brE
intro!:brI dest!: brD)

lemma filter_empty_ivls[autoref_rules]:
assumes [THEN PREFER_sv_D, relator_props]: "PREFER single_valued A"
assumes [THEN GEN_OP_D, param]: "GEN_OP le (≤) (A → A → bool_rel)"
assumes xs: "(xs, X) ∈ clw_rel (⟨A⟩ivl_rel)"
shows "(filter_empty_ivls_impl le xs, filter_empty_ivls \$ X) ∈ clw_rel (⟨A⟩ivl_rel)"
proof -
have "(filter_empty_ivls_impl le, filter_empty_ivls_impl (≤)) ∈ ⟨A×⇩rA⟩list_rel → ⟨A×⇩rA⟩list_rel"
unfolding filter_empty_ivls_impl_def
by parametricity
moreover
have "(filter_empty_ivls_impl (≤), filter_empty_ivls) ∈ clw_rel (⟨rnv_rel⟩ivl_rel) → clw_rel (⟨rnv_rel⟩ivl_rel)"
by (rule filter_empty_ivls_eucl)
ultimately have "(filter_empty_ivls_impl le, filter_empty_ivls) ∈
(⟨A ×⇩r A⟩list_rel → ⟨A ×⇩r A⟩list_rel) O (clw_rel (⟨rnv_rel⟩ivl_rel) → clw_rel (⟨rnv_rel⟩ivl_rel))" ..
also have "… ⊆ (⟨A ×⇩r A⟩list_rel O clw_rel (⟨rnv_rel⟩ivl_rel)) → (⟨A ×⇩r A⟩list_rel O clw_rel (⟨rnv_rel⟩ivl_rel))"
by (rule fun_rel_comp_dist)
also have "(⟨A ×⇩r A⟩list_rel O clw_rel (⟨rnv_rel⟩ivl_rel)) = clw_rel (⟨A⟩ivl_rel)"
unfolding Id_arbitrary_interface_def
apply (subst list_rel_comp_Union_rel)
apply (intro relator_props)
apply (subst prod_rel_comp_ivl_rel)
apply (intro relator_props)
apply (intro relator_props)
apply simp
done
finally show ?thesis using xs by (auto dest: fun_relD)
qed

definition [simp]: "op_inter_ivl = (∩)"
lemma [autoref_op_pat]: "(∩) ≡ OP op_inter_ivl"
by simp
lemma inter_ivl_rel[autoref_rules]:
assumes infi[THEN GEN_OP_D, param_fo]: "GEN_OP infi inf (A → A → A)"
assumes supi[THEN GEN_OP_D, param_fo]:"GEN_OP supi sup (A → A → A)"
shows "(λ(i, s). λ(i', s'). (supi i i', infi s s'), op_inter_ivl) ∈ ⟨A⟩ivl_rel → ⟨A⟩ivl_rel → ⟨A⟩ivl_rel"
using assms
by (fastforce simp: ivl_rel_def br_def set_of_ivl_def intro!: infi supi prod_relI)

definition [simp]: "op_inter_ivl_coll = (∩)"
lemma [autoref_op_pat]: "(∩) ≡ OP op_inter_ivl_coll"
by simp
lemma inter_ivl_clw_aux:
assumes sv: "single_valued A"
assumes intr: "(intr, (∩)) ∈ (⟨A⟩ivl_rel → ⟨A⟩ivl_rel → ⟨A⟩ivl_rel)"
shows "(λxs y. map (intr y) xs, (∩)) ∈ clw_rel (⟨A⟩ivl_rel) →  ⟨A⟩ivl_rel → clw_rel (⟨A⟩ivl_rel)"
apply (rule fun_relI)
apply (rule fun_relI)
using sv
apply (rule single_valued_as_brE)
apply simp
unfolding ivl_rel_def br_rel_prod br_chain prod_rel_id_simp Id_O_R
apply (rule map_mem_clw_rel_br)
apply (auto simp: set_of_ivl_def)
subgoal for a b c d e f g h i j
using intr[param_fo, of "(c, d)" "{f c .. f d}" "(i, j)" "{f i .. f j}"]
apply (auto simp: lw_rel_def Union_rel_br ivl_rel_def set_of_ivl_def br_rel_prod br_chain)
apply (auto simp: br_def set_of_ivl_def split_beta')
apply (rule bexI) prefer 2 apply assumption
apply simp
by (metis (mono_tags, lifting) Int_iff atLeastAtMost_iff fst_conv snd_conv)
subgoal for a b c d e f g h i j
using intr[param_fo, of "(c, d)" "{f c .. f d}" "(i, j)" "{f i .. f j}"]
apply (auto simp: lw_rel_def Union_rel_br ivl_rel_def set_of_ivl_def br_rel_prod br_chain)
apply (auto simp: br_def set_of_ivl_def split_beta')
by (metis (mono_tags, lifting) Int_iff atLeastAtMost_iff fst_conv snd_conv)+
subgoal for a b c d e f g h
using intr[param_fo, of "(c, d)" "{f c .. f d}" ]
apply (auto simp: lw_rel_def Union_rel_br ivl_rel_def set_of_ivl_def br_rel_prod br_chain)
apply (auto simp: br_def set_of_ivl_def split_beta')
apply (rule bexI) prefer 2 apply assumption
by (metis (mono_tags, lifting) Int_iff atLeastAtMost_iff fst_conv snd_conv)
subgoal for a b c d e f g h
using intr[param_fo, of "(c, d)" "{f c .. f d}" ]
apply (auto simp: lw_rel_def Union_rel_br ivl_rel_def set_of_ivl_def br_rel_prod br_chain)
apply (auto simp: br_def set_of_ivl_def split_beta')
by (metis (mono_tags, lifting) fst_conv snd_conv)
subgoal for a b c d e f g h
using intr[param_fo, of "(c, d)" "{f c .. f d}" ]
apply (auto simp: lw_rel_def Union_rel_br ivl_rel_def set_of_ivl_def br_rel_prod br_chain)
apply (auto simp: br_def set_of_ivl_def split_beta')
by (metis (mono_tags, lifting) fst_conv snd_conv)
done

lemma inter_ivl_clw[autoref_rules]:
assumes sv[THEN PREFER_sv_D]: "PREFER single_valued A"
assumes intr[THEN GEN_OP_D]: "GEN_OP intr op_inter_ivl (⟨A⟩ivl_rel → ⟨A⟩ivl_rel → ⟨A⟩ivl_rel)"
assumes "GEN_OP le (≤) (A → A → bool_rel)"
shows "(λxs y. filter_empty_ivls_impl le (map (intr y) xs), op_inter_ivl_coll) ∈ clw_rel (⟨A⟩ivl_rel) → (⟨A⟩ivl_rel) → clw_rel (⟨A⟩ivl_rel)"
apply safe
subgoal premises prems
using filter_empty_ivls[OF assms(1,3), param_fo, OF inter_ivl_clw_aux[OF sv intr[unfolded op_inter_ivl_def], param_fo, OF prems]]
by simp
done

lemma ivl_rel_br: "⟨br a I⟩ivl_rel = br (λ(x, y). set_of_ivl (a x, a y)) (λ(x, y). I x ∧ I y)"
unfolding ivl_rel_def br_rel_prod br_chain

lemma Inf_spec_ivl_rel[autoref_rules]:
"(λx. RETURN (fst x), Inf_spec) ∈ ⟨A⟩ivl_rel → ⟨A⟩nres_rel"
and Sup_spec_ivl_rel[autoref_rules]:
"(λx. RETURN (snd x), Sup_spec) ∈ ⟨A⟩ivl_rel → ⟨A⟩nres_rel"
by (force simp: Inf_spec_def Sup_spec_def nres_rel_def ivl_rel_def br_def set_of_ivl_def
intro!: RETURN_SPEC_refine)+

abbreviation "lvivl_rel ≡ ⟨lv_rel⟩ivl_rel"

lemma set_of_lvivl: "length (l) = DIM('a::executable_euclidean_space) ⟹
length u = DIM('a) ⟹
((l, u), set_of_lvivl (l, u)::'a set) ∈ lvivl_rel"
by (force simp: set_of_lvivl_def ivl_rel_br ivl_rel_def lv_rel_def br_def)

lemma lvivl_rel_br: "lvivl_rel = br (λ(x, y). set_of_ivl (eucl_of_list x, eucl_of_list y::'a)) (λ(x, y). length x = DIM('a::executable_euclidean_space) ∧ length y = DIM('a))"
unfolding lv_rel_def ivl_rel_br by (simp add: split_beta')

lemma disjoint_sets_nres:
fixes X Y::"'a::executable_euclidean_space set"
shows "do {
(iX, sX) ← ivl_rep X;
(iY, sY) ← ivl_rep Y;
RETURN (list_ex (λi. sX ∙ i < iY ∙ i ∨ sY ∙ i < iX ∙ i) Basis_list)
} ≤ disjoint_sets X Y"
by (force simp: Inf_spec_def Sup_spec_def disjoint_sets_def list_ex_iff eucl_le[where 'a='a]
intro!: refine_vcg)

schematic_goal disjoint_sets_impl:
fixes A::"(_ * 'a::executable_euclidean_space set) set"
assumes [autoref_rules_raw]: "DIM_precond (TYPE('a)) n"
assumes [autoref_rules]: "(ai, a::'a set) ∈ lvivl_rel"
assumes [autoref_rules]: "(bi, b) ∈ lvivl_rel"
shows "(nres_of (?f::?'r dres), disjoint_sets \$ a \$ b) ∈ ?R"
unfolding autoref_tag_defs

concrete_definition disjoint_sets_impl for n ai bi uses disjoint_sets_impl
lemma disjoint_sets_impl_refine[autoref_rules]:
"DIM_precond (TYPE('a::executable_euclidean_space)) n ⟹
(λai bi. nres_of (disjoint_sets_impl n ai bi), disjoint_sets::'a set ⇒ _) ∈ lvivl_rel → lvivl_rel → ⟨bool_rel⟩nres_rel"
using disjoint_sets_impl.refine by force

definition [simp]: "project_set_ivl X b y = do {
CHECK (λ_. ()) (b ∈ set Basis_list ∨ -b ∈ set Basis_list);
(i, s) ← ivl_rep X;
RETURN (op_atLeastAtMost_ivl (i + (y - i ∙ b) *⇩R b) (s + (y - s ∙ b) *⇩R b):::⟨lv_rel⟩ivl_rel)
}"

schematic_goal project_set_ivl:
fixes b::"'a::executable_euclidean_space" and y
assumes [autoref_rules_raw]: "DIM_precond (TYPE('a)) n"
assumes [autoref_rules]: "(Xi, X) ∈ ⟨lv_rel⟩ivl_rel"
assumes [autoref_rules]: "(bi, b) ∈ lv_rel"
assumes [autoref_rules]: "(yi, y) ∈ rnv_rel"
shows "(nres_of (?f::?'r dres), project_set_ivl X b y) ∈ ?R"
unfolding project_set_ivl_def
concrete_definition project_set_ivl_impl for n Xi bi yi uses project_set_ivl
lemma project_set_ivl_refine[autoref_rules]:
"DIM_precond (TYPE('a)) n ⟹
(λXi bi yi. nres_of (project_set_ivl_impl n Xi bi yi), project_set_ivl) ∈
⟨lv_rel⟩ivl_rel → (lv_rel::(_×'a::executable_euclidean_space) set) → rnv_rel → ⟨⟨lv_rel⟩ivl_rel⟩nres_rel"
using project_set_ivl_impl.refine by force

lemma project_set_ivl_spec[le, refine_vcg]: "project_set_ivl X b y ≤
SPEC (λR. abs b ∈ Basis ∧ (∃i s. X = {i .. s} ∧ R = {i + (y - i ∙ b) *⇩R b .. s + (y - s ∙ b) *⇩R b}))"
proof -
define b' where "b' ≡ abs b"
then have "b ∈ Basis ⟹ b' ∈ Basis"
"- b ∈ Basis ⟹ b' ∈ Basis"
"b ∈ Basis ⟹ b = b'"
"-b ∈ Basis ⟹ b = - b'"
using Basis_nonneg by (fastforce)+
then show ?thesis
unfolding project_set_ivl_def
by refine_vcg
(auto 0 4 simp: subset_iff eucl_le[where 'a='a] algebra_simps inner_Basis)
qed

lemma projection_notempty:
fixes b::"'a::executable_euclidean_space"
assumes "b ∈ Basis ∨ -b ∈ Basis"
assumes "x ≤ z"
shows "x + (y - x ∙ b) *⇩R b ≤ z + (y - z ∙ b) *⇩R b"
proof -
define b' where "b' ≡ - b"
then have b_dest: "-b ∈ Basis ⟹ b = -b' ∧ b' ∈ Basis"
by simp
show ?thesis using assms
by (auto simp: eucl_le[where 'a='a] algebra_simps inner_Basis dest!: b_dest)
qed

end

definition restrict_to_halfspace::"'a::executable_euclidean_space sctn ⇒ 'a set ⇒ 'a set nres"
where
"restrict_to_halfspace sctn X = do {
CHECK (λ_. ()) (normal sctn ∈ set Basis_list ∨ - normal sctn ∈ set Basis_list);
let y = pstn sctn;
let b = normal sctn;
(i, s) ← ivl_rep X;
let i' = (if b ≤ 0 then (i + (min (y - i ∙ b) 0) *⇩R b) else i);
let s' = (if b ≥ 0 then (s + (min (y - s ∙ b) 0) *⇩R b) else s);
RETURN ({i' .. s'}:::⇩i⟨i_rnv⟩⇩ii_ivl)
}"

context includes autoref_syntax begin

schematic_goal restrict_to_halfspace_impl:
fixes b y
assumes [autoref_rules_raw]: "DIM_precond (TYPE('a::executable_euclidean_space)) n"
assumes [autoref_rules]: "(Xi, X) ∈ ⟨lv_rel⟩ivl_rel"
assumes [autoref_rules]: "(sctni, sctn::'a sctn) ∈ ⟨lv_rel⟩sctn_rel"
shows "(nres_of (?f::?'r dres), restrict_to_halfspace sctn X) ∈ ?R"
unfolding restrict_to_halfspace_def[abs_def]
concrete_definition restrict_to_halfspace_impl for n sctni Xi uses restrict_to_halfspace_impl
lemma restrict_to_halfspace_impl_refine[autoref_rules]:
"DIM_precond (TYPE('a::executable_euclidean_space)) n ⟹
(λsctni Xi. nres_of (restrict_to_halfspace_impl n sctni Xi), restrict_to_halfspace::'a sctn⇒_) ∈
⟨lv_rel⟩sctn_rel → ⟨lv_rel⟩ivl_rel → ⟨⟨lv_rel⟩ivl_rel⟩nres_rel"
using restrict_to_halfspace_impl.refine by force
lemma restrict_to_halfspace[THEN order_trans, refine_vcg]:
"restrict_to_halfspace sctn X ≤ SPEC (λR. R = X ∩ below_halfspace sctn)"
unfolding restrict_to_halfspace_def
apply (refine_vcg)
subgoal premises prems for x a b
proof -
from prems obtain i where i: "i ∈ Basis" and disj: "normal sctn = i ∨ normal sctn = - i"
by auto
note nn = Basis_nonneg[OF i]
note nz = nonzero_Basis[OF i]
have ne: "- i ≠ i" using nn nz
by (metis antisym neg_le_0_iff_le)
have nn_iff: "0 ≤ normal sctn ⟷ normal sctn = i"
using disj nn
by (auto)
from prems have X: "X = {a .. b}" by auto
from disj show ?thesis
unfolding nn_iff
apply (rule disjE)
using nn nz ne
unfolding X using i
by (auto simp: eucl_le[where 'a='a] min_def algebra_simps inner_Basis
split: if_splits)
(auto simp: algebra_simps not_le)
qed
done

lemma restrict_to_halfspaces_impl:
"do {
ASSUME (finite sctns);
FOREACH⇗λsctns' Y. Y = X ∩ below_halfspaces (sctns - sctns')⇖ sctns restrict_to_halfspace X
} ≤ restrict_to_halfspaces sctns X"
unfolding restrict_to_halfspaces_def
by (refine_vcg) (auto simp: halfspace_simps)

schematic_goal restrict_to_halfspaces_ivl:
assumes [autoref_rules_raw]: "DIM_precond (TYPE('a::executable_euclidean_space)) n"
assumes [autoref_rules]: "(Xi, X) ∈ ⟨lv_rel⟩ivl_rel"
assumes sctns[autoref_rules]: "(sctnsi, sctns) ∈ sctns_rel"
notes [simp] = list_set_rel_finiteD[OF sctns]
shows "(nres_of (?f::?'r dres), restrict_to_halfspaces sctns X::'a set nres) ∈ ?R"
concrete_definition restrict_to_halfspaces_ivl for n sctnsi Xi uses restrict_to_halfspaces_ivl
lemma restrict_to_halfspaces_impl_refine[autoref_rules]:
"DIM_precond (TYPE('a::executable_euclidean_space)) n ⟹
(λsctni Xi. nres_of (restrict_to_halfspaces_ivl n sctni Xi), restrict_to_halfspaces) ∈
sctns_rel → ⟨(lv_rel::(_×'a) set)⟩ivl_rel → ⟨⟨lv_rel⟩ivl_rel⟩nres_rel"
using restrict_to_halfspaces_ivl.refine[of n] by force

definition [simp]: "restrict_to_halfspaces_clw = restrict_to_halfspaces"
lemma restrict_to_halfspaces_clw:
"do {
XS ← sets_of_coll X;
FORWEAK XS (RETURN op_empty_coll) (λX. do {R ← restrict_to_halfspaces sctns X; RETURN (filter_empty_ivls (mk_coll R))})
(λX Y. RETURN (Y ∪ X))
} ≤ restrict_to_halfspaces_clw sctns X"
unfolding restrict_to_halfspaces_def restrict_to_halfspaces_clw_def
by (refine_vcg FORWEAK_mono_rule[where
I="λXS R. ⋃XS ∩ below_halfspaces sctns ⊆ R ∧ R ⊆ X ∩ below_halfspaces sctns"])
auto
schematic_goal restrict_to_halfspaces_clw_rel:
fixes X::"'a::executable_euclidean_space set"
assumes [autoref_rules_raw]: "DIM_precond (TYPE('a)) n"
assumes [autoref_rules]: "(Xi, X) ∈ clw_rel (⟨lv_rel⟩ivl_rel)"
assumes sctns[autoref_rules]: "(sctnsi, sctns) ∈ sctns_rel"
notes [simp] = list_set_rel_finiteD[OF sctns]
shows "(nres_of (?f::?'r dres), restrict_to_halfspaces_clw sctns X) ∈ ?R"
concrete_definition restrict_to_halfspaces_clw_rel for n sctnsi Xi uses restrict_to_halfspaces_clw_rel
lemma restrict_to_halfspaces_clw_rel_refine[autoref_rules]:
"DIM_precond (TYPE('a::executable_euclidean_space)) n ⟹
(λsctni Xi. nres_of (restrict_to_halfspaces_clw_rel n sctni Xi), restrict_to_halfspaces_clw) ∈
sctns_rel → clw_rel (⟨lv_rel⟩ivl_rel) → ⟨clw_rel (⟨(lv_rel::(_×'a) set)⟩ivl_rel)⟩nres_rel"
using restrict_to_halfspaces_clw_rel.refine by force

definition [simp]: "restrict_to_halfspaces_invar_clw = restrict_to_halfspaces"
lemma restrict_to_halfspaces_invar_clw_ref:
"do {
XS ← (sets_of_coll X);
FORWEAK XS (RETURN op_empty_coll) (λX. do {
(X, i) ← get_invar a X;
R ← restrict_to_halfspaces sctns X;
ASSERT (R ⊆ a i);
RETURN (with_invar i (filter_empty_ivls (mk_coll R)):::clw_rel (⟨I, lvivl_rel⟩invar_rel a))
}) (λX Y. RETURN (Y ∪ X))
} ≤ restrict_to_halfspaces_invar_clw sctns X"
unfolding restrict_to_halfspaces_def restrict_to_halfspaces_invar_clw_def
by (refine_vcg FORWEAK_mono_rule[where
I="λXS R. ⋃XS ∩ below_halfspaces sctns ⊆ R ∧ R ⊆ X ∩ below_halfspaces sctns"])
auto

schematic_goal restrict_to_halfspaces_invar_clw_impl:
fixes X::"'a::executable_euclidean_space set"
assumes [autoref_rules_raw]: "DIM_precond (TYPE('a)) n"
assumes [autoref_rules]: "(Xi, X) ∈ clw_rel (⟨I, lvivl_rel⟩invar_rel a)"
assumes sctns[autoref_rules]: "(sctnsi, sctns) ∈ sctns_rel"
notes [simp] = list_set_rel_finiteD[OF sctns]
shows "(nres_of (?f::?'r dres), restrict_to_halfspaces_invar_clw sctns X) ∈ ?R"
including art
by (rule nres_rel_trans2[OF restrict_to_halfspaces_invar_clw_ref[where a=a and I=I]])

concrete_definition restrict_to_halfspaces_invar_clw_impl for n sctnsi Xi uses restrict_to_halfspaces_invar_clw_impl
lemma restrict_to_halfspaces_invar_clw_refine[autoref_rules]:
"DIM_precond (TYPE('a::executable_euclidean_space)) n ⟹
(λsctnsi Xi. nres_of (restrict_to_halfspaces_invar_clw_impl n sctnsi Xi), restrict_to_halfspaces_invar_clw::'a sctn set ⇒ _) ∈
sctns_rel → clw_rel (⟨I, lvivl_rel⟩invar_rel a) → ⟨clw_rel (⟨I, lvivl_rel⟩invar_rel a)⟩nres_rel"
using restrict_to_halfspaces_invar_clw_impl.refine[of n _ _ a I] by force

abbreviation "below_invar_rel ≡ λA. ⟨⟨lv_rel⟩sctn_rel, A⟩invar_rel below_halfspace"
abbreviation "sbelow_invar_rel ≡ λA. ⟨⟨lv_rel⟩sctn_rel, A⟩invar_rel sbelow_halfspace"
abbreviation "plane_invar_rel ≡ λA. ⟨⟨lv_rel⟩sctn_rel, A⟩invar_rel plane_of"
abbreviation "belows_invar_rel ≡ λA. ⟨sctns_rel, A⟩invar_rel below_halfspaces"
abbreviation "sbelows_invar_rel ≡ λA. ⟨sctns_rel, A⟩invar_rel sbelow_halfspaces"

definition [simp]: "with_invar_on_invar = with_invar"
lemma with_invar_on_invar_impl[autoref_rules]:
assumes "PREFER single_valued S"
assumes "PREFER single_valued A"
assumes "(sctni, sctn) ∈ S"
assumes "GEN_OP uni (∪) (S → S → S)"
assumes "(Xi, X) ∈ clw_rel (⟨S, A⟩invar_rel a)"
assumes "SIDE_PRECOND (X ⊆ a sctn)"
assumes a_distrib: "SIDE_PRECOND (∀x y. a (x ∪ y) = a x ∩ a y)"
shows "(map (λ(x, y). (x, uni sctni y)) Xi, with_invar_on_invar \$ sctn \$ X) ∈ clw_rel (⟨S, A⟩invar_rel a)"
using assms(1-6) a_distrib[unfolded autoref_tag_defs, rule_format]
apply (auto simp: invar_rel_br intro!: map_mem_clw_rel_br elim!: single_valued_as_brE)
apply (auto simp: lw_rel_def Union_rel_br)
apply (auto simp: br_def)
apply (metis (no_types, lifting) case_prod_conv)
apply (drule_tac x=sctni and x' = sctn in fun_relD, force)
apply (drule_tac x=b and x' = "α b" in fun_relD, force)
apply force
apply (drule_tac x=sctni and x' = sctn in fun_relD, force)
apply (drule_tac x=b and x' = "α b" in fun_relD, force)
apply safe
proof -
fix α :: "'a ⇒ 'b set" and invar :: "'a ⇒ bool" and α' :: "'c ⇒ 'd set" and invara :: "'c ⇒ bool" and aa :: 'c and b :: 'a and x :: 'd
assume a1: "x ∈ α' aa"
assume a2: "(aa, b) ∈ set Xi"
assume a3: "(⋃x∈set Xi. case x of (x, s) ⇒ α' x) ⊆ a (α sctni)"
assume a4: "∀x∈set Xi. case x of (x, s) ⇒ invara x ∧ invar s ∧ α' x ⊆ a (α s)"
assume a5: "⋀x y. a (x ∪ y) = a x ∩ a y"
assume a6: "α sctni ∪ α b = α (uni sctni b)"
have f7: "invara aa ∧ invar b ∧ α' aa ⊆ a (α b)"
using a4 a2 by fastforce
have "x ∈ a (α sctni)"
using a3 a2 a1 by blast
then show "x ∈ a (α (uni sctni b))"
using f7 a6 a5 a1 by (metis (full_types) Int_iff subsetCE)
qed

lemma
set_of_ivl_union:
fixes i1 i2 s1 s2::"'a::executable_euclidean_space"
shows "set_of_ivl (i1, s1) ∪ set_of_ivl (i2, s2) ⊆ set_of_ivl (inf i1 i2, sup s1 s2)"
by (auto simp: set_of_ivl_def)

lemma fold_set_of_ivl:
fixes i s::"'a::executable_euclidean_space"
assumes "⋀i s. (i, s) ∈ set xs ⟹ i ≤ s"
assumes "i ≤ s"
shows "⋃ (set_of_ivl ` insert (i, s) (set xs)) ⊆
set_of_ivl (fold (λ(i1, s1) (i2, s2). (inf i1 i2, sup s1 s2)) xs (i, s))"
using assms
proof (induction xs arbitrary: i s)
case (Cons x xs i s)
then show ?case
apply (auto simp: set_of_ivl_def
simp: split_beta' le_infI2 le_supI2 le_infI1 le_supI1)
apply (metis (no_types, lifting) inf.absorb_iff2 inf_sup_ord(2) le_infE le_supI2)
apply (metis (no_types, lifting) inf.absorb_iff2 inf_sup_ord(2) le_infE le_supI2)
apply (metis (no_types, lifting) inf.absorb_iff2 inf_sup_ord(2) le_infE le_supI2)
by (metis (no_types, lifting) inf_sup_absorb le_infI2 le_supI2)
qed simp

lemma fold_infsup_le:
fixes i s::"'a::executable_euclidean_space"
assumes "⋀i s. (i, s) ∈ set xs ⟹ i ≤ s"
assumes "i ≤ s"
shows "case (fold (λ(i1, s1) (i2, s2). (inf i1 i2, sup s1 s2)) xs (i, s)) of (i, s) ⇒ i ≤ s"
using assms
proof (induction xs arbitrary: i s)
case (Cons x xs i s)
then show ?case
by (auto simp: set_of_ivl_def
simp: split_beta' le_infI2 le_supI2 le_infI1 le_supI1)
qed simp

definition "max_coord M (x::'a::executable_euclidean_space) =
snd (fold (λa (b, c). let d = abs x ∙ a in if d ≥ b then (d, a) else (b, c)) (take M Basis_list) (0, 0))"

schematic_goal max_coord_autoref:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) n"
assumes [autoref_rules]: "(Xi, X::'a) ∈ lv_rel"
assumes [autoref_rules]: "(Mi, M) ∈ nat_rel"
shows "(?r, max_coord M X) ∈ lv_rel"
unfolding max_coord_def
by autoref
concrete_definition max_coord_lv_rel for n Mi Xi uses max_coord_autoref
lemma max_coord_lv_rel_refine[autoref_rules]:
"DIM_precond TYPE('a::executable_euclidean_space) n ⟹ (λMi Xi. max_coord_lv_rel n Mi Xi, max_coord::nat⇒'a⇒_) ∈ nat_rel → lv_rel → lv_rel"
using max_coord_lv_rel.refine by force

definition "split_ivl_at_halfspace sctn1 x =
do {
(i, s) ← ivl_rep x;
let sctn2 = Sctn (- normal sctn1) (- pstn sctn1);
x1 ← restrict_to_halfspace sctn1 x;
x2 ← restrict_to_halfspace sctn2 x;
RETURN (x1, x2)
}"

lemma split_ivl_at_halfspace[THEN order_trans, refine_vcg]:
"split_ivl_at_halfspace sctn x ≤ split_spec_exact x"
unfolding split_ivl_at_halfspace_def split_spec_exact_def
by refine_vcg (auto simp: halfspace_simps)

schematic_goal split_ivl_at_halfspace_impl:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) n"
assumes [autoref_rules]: "(Xi, X) ∈ lvivl_rel"
assumes [autoref_rules]: "(sctni, sctn) ∈ ⟨lv_rel⟩sctn_rel"
shows "(nres_of ?X, split_ivl_at_halfspace sctn (X::'a set)) ∈ ⟨lvivl_rel ×⇩r lvivl_rel⟩nres_rel"
unfolding split_ivl_at_halfspace_def
concrete_definition split_ivl_at_halfspace_impl for n sctni Xi uses split_ivl_at_halfspace_impl
lemma split_ivl_at_halfspace_impl_refine[autoref_rules]:
"DIM_precond TYPE('a::executable_euclidean_space) n ⟹
(λsctni Xi. nres_of (split_ivl_at_halfspace_impl n sctni Xi), split_ivl_at_halfspace::_ ⇒ 'a set ⇒ _) ∈
⟨lv_rel⟩sctn_rel → lvivl_rel → ⟨lvivl_rel ×⇩r lvivl_rel⟩nres_rel"
using split_ivl_at_halfspace_impl.refine
by force

definition "split_spec_ivl M x =
do {
(i, s) ← ivl_rep x;
let d = s - i;
let b = max_coord M d;
let m = (i ∙ b + s ∙ b)/2;
split_ivl_at_halfspace (Sctn b m) x
}"

lemma split_spec_ivl_split_spec_exact[THEN order_trans, refine_vcg]:
"split_spec_ivl M x ≤ split_spec_exact x"
unfolding split_spec_ivl_def split_spec_exact_def
by refine_vcg

schematic_goal split_spec_exact_ivl_rel:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) n"
assumes [autoref_rules]: "(Xi, X) ∈ lvivl_rel"
assumes [autoref_rules]: "(Mi, M) ∈ nat_rel"
shows "(nres_of ?X, split_spec_ivl M (X::'a set)) ∈ ⟨lvivl_rel ×⇩r lvivl_rel⟩nres_rel"
unfolding split_spec_ivl_def
concrete_definition split_spec_exact_ivl_rel for n Mi Xi uses split_spec_exact_ivl_rel
lemma split_spec_exact_ivl_rel_refine[autoref_rules]:
"DIM_precond TYPE('a::executable_euclidean_space) n ⟹
(λMi Xi. nres_of (split_spec_exact_ivl_rel n Mi Xi), split_spec_ivl::nat ⇒ 'a set ⇒ _) ∈
nat_rel → lvivl_rel → ⟨lvivl_rel ×⇩r lvivl_rel⟩nres_rel"
using split_spec_exact_ivl_rel.refine
by force

lemma [autoref_itype]: "op_set_isEmpty ::⇩i ⟨L, ⟨A⟩⇩ii_ivl⟩⇩ii_coll →⇩i i_bool"
by simp

lemma op_set_isEmpty_clw_rel_ivl_rel[autoref_rules]:
assumes sv[THEN PREFER_sv_D, relator_props]: "PREFER single_valued A"
assumes le[THEN GEN_OP_D, param_fo]: "GEN_OP le (≤) (A → A → bool_rel)"
shows "(λxs. filter_empty_ivls_impl le xs = [], op_set_isEmpty) ∈ clw_rel (⟨A⟩ivl_rel) → bool_rel"
apply (rule fun_relI)
subgoal premises prems for a b
using filter_empty_ivls[OF assms prems] sv
apply (auto simp: list_wset_rel_def ivl_rel_br Union_rel_br filter_empty_ivls_impl_def filter_empty_conv
set_of_ivl_def split_beta' Id_arbitrary_interface_def
dest!: brD elim!: single_valued_as_brE)
subgoal for α I x y
using le[of x "α x"  y "α y"]
apply (auto simp: br_def)
done
done
done

lemma project_sets_FOREACH_refine:
"do {
Xs ← (sets_of_coll X ::: ⟨⟨A⟩list_wset_rel⟩nres_rel);
FORWEAK Xs (RETURN {}) (λX. do { ivl ← project_set X b y; RETURN (mk_coll ivl)}) (λa b. RETURN (a ∪ b))
} ≤ project_sets X b y"
unfolding project_sets_def autoref_tag_defs
by (refine_vcg FORWEAK_mono_rule'[where I="λS s. ⋃S ∩ {x. x ∙ b = y} ⊆ s ∧ s ⊆ {x. x ∙ b = y}"])
auto

definition split_intersecting
where [refine_vcg_def]: "split_intersecting X Y = SPEC (λ(R, S). X = R ∪ S ∧ X ∩ Y ⊆ R ∧ S ∩ Y = {})"

definition intersecting_sets where
"intersecting_sets X Z = do {
ZS ← sets_of_coll (Z);
XS ← sets_of_coll (X);
FORWEAK XS (RETURN (op_empty_coll, op_empty_coll)) (λX. do {
d ← FORWEAK ZS (RETURN True) (disjoint_sets X) (λa b. RETURN (a ∧ b));
RETURN (if d then (op_empty_coll, mk_coll X) else (mk_coll X, op_empty_coll))
}) (λ(R, S). λ(R', S'). RETURN (R' ∪ R, S' ∪ S))
}"

lemma intersecting_sets_spec:
shows "intersecting_sets X Y ≤ split_intersecting X Y"
unfolding intersecting_sets_def split_intersecting_def
autoref_tag_defs
apply (refine_vcg)
apply (rule FORWEAK_mono_rule[where I="λXS. λ(R, S).
R ∪ S ⊆ X ∧ ⋃XS ⊆ R ∪ S ∧ ⋃XS ∩ Y ⊆ R ∧ S ∩ Y = {}"])
subgoal by (refine_vcg)
subgoal for a b c
by (refine_vcg FORWEAK_mono_rule[where I="λZS d. d ⟶ ⋃ZS ∩ c = {}"]) (auto split: if_splits)
subgoal by (auto; blast)
subgoal for a b c d e
by (refine_vcg FORWEAK_mono_rule[where I="λZS d. d ⟶ ⋃ZS ∩ c = {}"]) (auto split: if_splits)
subgoal by auto
done

schematic_goal split_intersecting_impl:
fixes A::"(_ × 'a::executable_euclidean_space set) set"
assumes [autoref_rules_raw]: "DIM_precond (TYPE('a)) n"
assumes [autoref_rules]: "(Xi,X::'a set)∈clw_rel lvivl_rel"
assumes [autoref_rules]: "(Zi,Z)∈clw_rel lvivl_rel"
shows "(nres_of ?f, split_intersecting \$ X \$ Z)∈⟨clw_rel lvivl_rel ×⇩r clw_rel lvivl_rel⟩nres_rel"
unfolding autoref_tag_defs
apply (rule nres_rel_trans2[OF intersecting_sets_spec])
unfolding intersecting_sets_def

concrete_definition split_intersecting_impl for Xi Zi uses split_intersecting_impl
lemmas [autoref_rules] = split_intersecting_impl.refine

definition inter_overappr where [refine_vcg_def]: "inter_overappr X Y = SPEC (λR. X ∩ Y ⊆ R ∧ R ⊆ X)"

lemma inter_overappr_impl: "do {(X, _) ← split_intersecting X Y; RETURN X} ≤ inter_overappr X Y"
unfolding split_intersecting_def inter_overappr_def autoref_tag_defs
by (refine_vcg) auto

schematic_goal inter_overappr_autoref:
assumes [autoref_rules_raw]: "DIM_precond (TYPE('a::executable_euclidean_space)) n"
assumes [autoref_rules]: "(Xi,X)∈clw_rel lvivl_rel"
assumes [autoref_rules]: "(Zi,Z)∈clw_rel lvivl_rel"
shows "(nres_of ?f, inter_overappr X Z::'a set nres)∈⟨clw_rel lvivl_rel⟩nres_rel"
unfolding autoref_tag_defs
concrete_definition inter_overappr_impl for Xi Zi uses inter_overappr_autoref
lemmas [autoref_rules] = inter_overappr_impl.refine[autoref_higher_order_rule(1)]

definition "sctnbounds_of_ivl M X = do {
(l, u) ← ivl_rep X;
let ls = (λb. Sctn (- b) (- l ∙ b)) ` (set (take M Basis_list)::'a::executable_euclidean_space set);
let us = (λb. Sctn (b) (u ∙ b)) ` (set (take M Basis_list)::'a set);
RETURN (ls ∪ us)
}"

lemma sctnbounds_of_ivl[THEN order_trans, refine_vcg]:
"sctnbounds_of_ivl M X ≤ SPEC (λsctns. finite sctns ∧ (∀sctn ∈ sctns. normal sctn ≠ 0))"
unfolding sctnbounds_of_ivl_def
by refine_vcg (auto dest!: in_set_takeD)

schematic_goal sctnbounds_of_ivl_impl:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) D"
assumes [autoref_rules]: "(Xi, X::'a set) ∈ lvivl_rel" "(Mi, M) ∈ nat_rel"
shows "(?f, sctnbounds_of_ivl \$ M \$ X) ∈ ⟨sctns_rel⟩nres_rel"
unfolding autoref_tag_defs
unfolding sctnbounds_of_ivl_def
concrete_definition sctnbounds_of_ivl_impl for Mi Xi uses sctnbounds_of_ivl_impl
lemma sctnbounds_of_ivl_impl_refine[autoref_rules]:
"DIM_precond TYPE('a::executable_euclidean_space) D ⟹
(λMi Xi. RETURN (sctnbounds_of_ivl_impl D Mi Xi), sctnbounds_of_ivl::nat ⇒ 'a set ⇒ _)
∈ nat_rel → ⟨lv_rel⟩ivl_rel → ⟨sctns_rel⟩nres_rel"
using sctnbounds_of_ivl_impl.refine by force

lemma SPEC_True_mono: "b ≤ c ⟹ SPEC (λ_. True) ⤜ (λ_. b) ≤ c"
by (auto simp: bind_le_nofailI)

definition "split_ivls_at_halfspace sctn XS = do {
XS ← sets_of_coll XS;
FORWEAK XS (RETURN op_empty_coll) (λX. do {
(A, B) ← split_ivl_at_halfspace sctn X;
RETURN (filter_empty_ivls (mk_coll A ∪ mk_coll B))
}) (λX X'. RETURN (X' ∪ X))
}"

lemma split_ivls_at_halfspace[THEN order_trans, refine_vcg]:
"split_ivls_at_halfspace sctn X ≤ SPEC (λR. R = X)"
unfolding split_ivls_at_halfspace_def
by (refine_vcg FORWEAK_mono_rule[where I="λXi XS. ⋃Xi ⊆ XS ∧ XS ⊆ X"]) auto

schematic_goal split_ivls_at_halfspace_impl:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) D"
assumes [autoref_rules]: "(Xi, X::'a set) ∈ clw_rel lvivl_rel" "(sctni, sctn) ∈ ⟨lv_rel⟩sctn_rel"
shows "(?f, split_ivls_at_halfspace \$ sctn \$ X) ∈ ⟨clw_rel lvivl_rel⟩nres_rel"
unfolding autoref_tag_defs
unfolding split_ivls_at_halfspace_def
concrete_definition split_ivls_at_halfspace_impl for sctni Xi uses split_ivls_at_halfspace_impl
lemma split_ivls_at_halfspace_impl_refine[autoref_rules]:
"DIM_precond TYPE('a::executable_euclidean_space) D ⟹
(λXi sctni. nres_of (split_ivls_at_halfspace_impl D Xi sctni), split_ivls_at_halfspace::'a sctn ⇒ _)
∈  ⟨lv_rel⟩sctn_rel → clw_rel (⟨lv_rel⟩ivl_rel) → ⟨clw_rel (⟨lv_rel⟩ivl_rel)⟩nres_rel"
using split_ivls_at_halfspace_impl.refine
by force

definition "split_along_ivls M X IS = do {
IS ← sets_of_coll IS;
sctns ← FORWEAK IS (RETURN {}) (sctnbounds_of_ivl M) (λsctns sctns'. RETURN (sctns' ∪ sctns));
FOREACH⇗λ_ R. R = X⇖ sctns split_ivls_at_halfspace X
}"

lemma split_along_ivls[THEN order_trans, refine_vcg]:"split_along_ivls M X IS ≤ SPEC (λR. R = X)"
unfolding split_along_ivls_def
by (refine_vcg FORWEAK_mono_rule[where I="λ_ r. finite r"])

schematic_goal split_along_ivls_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 "(?f, split_along_ivls \$ M \$ X \$ IS) ∈ ⟨clw_rel lvivl_rel⟩nres_rel"
unfolding autoref_tag_defs
unfolding split_along_ivls_def
concrete_definition split_along_ivls_impl uses split_along_ivls_impl
lemmas [autoref_rules] = split_along_ivls_impl.refine

definition "op_ivl_rep_of_set X =
do { let X = (X); i ← Inf_spec X; s ← Sup_spec X; RETURN (inf i s, s)}"

definition "op_ivl_rep_of_sets XS =
FORWEAK XS (RETURN (0, 0)) op_ivl_rep_of_set (λ(i, s) (i', s').
RETURN (inf i i':::lv_rel, sup s s':::lv_rel))"

definition "op_ivl_of_ivl_coll XS =
do {XS ← sets_of_coll XS;
(l, u) ← FORWEAK XS (RETURN (0, 0)) ivl_rep (λ(i, s) (i', s').
RETURN (inf i i':::lv_rel, sup s s':::lv_rel));
RETURN (op_atLeastAtMost_ivl l u)
}"

schematic_goal op_ivl_of_ivl_coll_impl:
assumes [autoref_rules_raw]: "DIM_precond TYPE('a::executable_euclidean_space) D"
assumes [autoref_rules]: "(ISi, IS::'a::executable_euclidean_space set) ∈ clw_rel lvivl_rel"
shows "(?f, op_ivl_of_ivl_coll IS) ∈ ⟨lvivl_rel⟩nres_rel"
unfolding op_ivl_of_ivl_coll_def
concrete_definition op_ivl_of_ivl_coll_impl uses op_ivl_of_ivl_coll_impl
lemmas op_ivl_of_ivl_coll_impl_refine[autoref_rules] =
op_ivl_of_ivl_coll_impl.refine[autoref_higher_order_rule (1)]

lemma is_empty_lvivl_rel[autoref_rules]:
shows "(λ(a, b). ¬ list_all2 (≤) a b, is_empty) ∈ lvivl_rel → bool_rel"
using le_left_mono
by (fastforce simp: ivl_rel_def br_def set_of_ivl_def dest: lv_rel_le[param_fo])

definition [simp]: "op_times_ivl a b = a × b"

lemma [autoref_op_pat]: "a × b ≡ OP op_times_ivl \$ a \$ b"
by auto

lemma op_times_ivl[autoref_rules]:
"(λ(l, u) (l', u'). (l @ l', u @ u'), op_times_ivl) ∈ lvivl_rel → lvivl_rel → lvivl_rel"
apply (auto simp: ivl_rel_def br_def intro!: rel_funI)
subgoal for a b c d e f g h
apply (rule relcompI[where b="((c, g), (d, h))"])
by (auto simp: lv_rel_def br_def set_of_ivl_def)
done

end

end```