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
  by (simp add: split_beta' o_def)

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
  by (rule disjoint_sets_nres[THEN nres_rel_trans2]) autoref_monadic

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
  by autoref_monadic
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]
  by (autoref_monadic)
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
       apply (simp_all add: below_halfspace_def le_halfspace_def[abs_def])
      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"
  by (rule nres_rel_trans2[OF restrict_to_halfspaces_impl]) autoref_monadic
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"
  by (rule nres_rel_trans2[OF restrict_to_halfspaces_clw]) autoref_monadic
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]])
    (autoref_monadic)

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
  by (autoref_monadic)
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
  by (autoref_monadic)
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
  by autoref_monadic

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
  by (rule nres_rel_trans2[OF inter_overappr_impl]) (autoref_monadic)
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
  by autoref_monadic
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
  by autoref_monadic
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
  by autoref_monadic
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
  by autoref_monadic
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