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
  by autoref_monadic
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)
     apply (simp add: set_of_ivl_def fst_imageIcc)
    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 (simp add: lens;fail)
     apply (rule brI)
      apply (rule refl)
     apply (simp add: lens;fail)
    apply (rule brI)
     apply (simp add: set_of_ivl_def fst_imageIcc)
     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 add: set_of_ivl_def fst_imageIcc)
    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
  by autoref_monadic
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
  by autoref_monadic
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
  by autoref_monadic
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
  by autoref_monadic
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
  by autoref_monadic
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 (simp add: lv_rel_def br_def)
    apply (rule lv_relI)
   apply (simp add: lv_rel_def br_def)
  apply (rule brI)
  subgoal for a b
    apply (drule fun_relD)
     apply (rule lv_relI[where x=a])
      apply (simp add: lv_rel_def br_def)
    apply (drule fun_relD)
     apply (rule lv_relI[where x=b])
      apply (simp add: lv_rel_def br_def)
    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
  by autoref_monadic
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
  by autoref_monadic
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
  by autoref_monadic
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
  by autoref_monadic
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
  by autoref_monadic
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
  by autoref_monadic
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