Theory HOL-Library.Interval
section ‹Interval Type›
theory Interval
imports
Complex_Main
Lattice_Algebras
Set_Algebras
begin
text ‹A type of non-empty, closed intervals.›
typedef (overloaded) 'a interval =
"{(a::'a::preorder, b). a ≤ b}"
morphisms bounds_of_interval Interval
by auto
setup_lifting type_definition_interval
lift_definition lower::"('a::preorder) interval ⇒ 'a" is fst .
lift_definition upper::"('a::preorder) interval ⇒ 'a" is snd .
lemma interval_eq_iff: "a = b ⟷ lower a = lower b ∧ upper a = upper b"
by transfer auto
lemma interval_eqI: "lower a = lower b ⟹ upper a = upper b ⟹ a = b"
by (auto simp: interval_eq_iff)
lemma lower_le_upper[simp]: "lower i ≤ upper i"
by transfer auto
lift_definition set_of :: "'a::preorder interval ⇒ 'a set" is "λx. {fst x .. snd x}" .
lemma set_of_eq: "set_of x = {lower x .. upper x}"
by transfer simp
context notes [[typedef_overloaded]] begin
lift_definition(code_dt) Interval'::"'a::preorder ⇒ 'a::preorder ⇒ 'a interval option"
is "λa b. if a ≤ b then Some (a, b) else None"
by auto
lemma Interval'_split:
"P (Interval' a b) ⟷
(∀ivl. a ≤ b ⟶ lower ivl = a ⟶ upper ivl = b ⟶ P (Some ivl)) ∧ (¬a≤b ⟶ P None)"
by transfer auto
lemma Interval'_split_asm:
"P (Interval' a b) ⟷
¬((∃ivl. a ≤ b ∧ lower ivl = a ∧ upper ivl = b ∧ ¬P (Some ivl)) ∨ (¬a≤b ∧ ¬P None))"
unfolding Interval'_split
by auto
lemmas Interval'_splits = Interval'_split Interval'_split_asm
lemma Interval'_eq_Some: "Interval' a b = Some i ⟹ lower i = a ∧ upper i = b"
by (simp split: Interval'_splits)
end
instantiation "interval" :: ("{preorder,equal}") equal
begin
definition "equal_class.equal a b ≡ (lower a = lower b) ∧ (upper a = upper b)"
instance proof qed (simp add: equal_interval_def interval_eq_iff)
end
instantiation interval :: ("preorder") ord begin
definition less_eq_interval :: "'a interval ⇒ 'a interval ⇒ bool"
where "less_eq_interval a b ⟷ lower b ≤ lower a ∧ upper a ≤ upper b"
definition less_interval :: "'a interval ⇒ 'a interval ⇒ bool"
where "less_interval x y = (x ≤ y ∧ ¬ y ≤ x)"
instance proof qed
end
instantiation interval :: ("lattice") semilattice_sup
begin
lift_definition sup_interval :: "'a interval ⇒ 'a interval ⇒ 'a interval"
is "λ(a, b) (c, d). (inf a c, sup b d)"
by (auto simp: le_infI1 le_supI1)
lemma lower_sup[simp]: "lower (sup A B) = inf (lower A) (lower B)"
by transfer auto
lemma upper_sup[simp]: "upper (sup A B) = sup (upper A) (upper B)"
by transfer auto
instance proof qed (auto simp: less_eq_interval_def less_interval_def interval_eq_iff)
end
lemma set_of_interval_union: "set_of A ∪ set_of B ⊆ set_of (sup A B)" for A::"'a::lattice interval"
by (auto simp: set_of_eq)
lemma interval_union_commute: "sup A B = sup B A" for A::"'a::lattice interval"
by (auto simp add: interval_eq_iff inf.commute sup.commute)
lemma interval_union_mono1: "set_of a ⊆ set_of (sup a A)" for A :: "'a::lattice interval"
using set_of_interval_union by blast
lemma interval_union_mono2: "set_of A ⊆ set_of (sup a A)" for A :: "'a::lattice interval"
using set_of_interval_union by blast
lift_definition interval_of :: "'a::preorder ⇒ 'a interval" is "λx. (x, x)"
by auto
lemma lower_interval_of[simp]: "lower (interval_of a) = a"
by transfer auto
lemma upper_interval_of[simp]: "upper (interval_of a) = a"
by transfer auto
definition width :: "'a::{preorder,minus} interval ⇒ 'a"
where "width i = upper i - lower i"
instantiation "interval" :: ("ordered_ab_semigroup_add") ab_semigroup_add
begin
lift_definition plus_interval::"'a interval ⇒ 'a interval ⇒ 'a interval"
is "λ(a, b). λ(c, d). (a + c, b + d)"
by (auto intro!: add_mono)
lemma lower_plus[simp]: "lower (plus A B) = plus (lower A) (lower B)"
by transfer auto
lemma upper_plus[simp]: "upper (plus A B) = plus (upper A) (upper B)"
by transfer auto
instance proof qed (auto simp: interval_eq_iff less_eq_interval_def ac_simps)
end
instance "interval" :: ("{ordered_ab_semigroup_add, lattice}") ordered_ab_semigroup_add
proof qed (auto simp: less_eq_interval_def intro!: add_mono)
instantiation "interval" :: ("{preorder,zero}") zero
begin
lift_definition zero_interval::"'a interval" is "(0, 0)" by auto
lemma lower_zero[simp]: "lower 0 = 0"
by transfer auto
lemma upper_zero[simp]: "upper 0 = 0"
by transfer auto
instance proof qed
end
instance "interval" :: ("{ordered_comm_monoid_add}") comm_monoid_add
proof qed (auto simp: interval_eq_iff)
instance "interval" :: ("{ordered_comm_monoid_add,lattice}") ordered_comm_monoid_add ..
instantiation "interval" :: ("{ordered_ab_group_add}") uminus
begin
lift_definition uminus_interval::"'a interval ⇒ 'a interval" is "λ(a, b). (-b, -a)" by auto
lemma lower_uminus[simp]: "lower (- A) = - upper A"
by transfer auto
lemma upper_uminus[simp]: "upper (- A) = - lower A"
by transfer auto
instance ..
end
instantiation "interval" :: ("{ordered_ab_group_add}") minus
begin
definition minus_interval::"'a interval ⇒ 'a interval ⇒ 'a interval"
where "minus_interval a b = a + - b"
lemma lower_minus[simp]: "lower (minus A B) = minus (lower A) (upper B)"
by (auto simp: minus_interval_def)
lemma upper_minus[simp]: "upper (minus A B) = minus (upper A) (lower B)"
by (auto simp: minus_interval_def)
instance ..
end
instantiation "interval" :: ("{times, linorder}") times
begin
lift_definition times_interval :: "'a interval ⇒ 'a interval ⇒ 'a interval"
is "λ(a1, a2). λ(b1, b2).
(let x1 = a1 * b1; x2 = a1 * b2; x3 = a2 * b1; x4 = a2 * b2
in (min x1 (min x2 (min x3 x4)), max x1 (max x2 (max x3 x4))))"
by (auto simp: Let_def intro!: min.coboundedI1 max.coboundedI1)
lemma lower_times:
"lower (times A B) = Min {lower A * lower B, lower A * upper B, upper A * lower B, upper A * upper B}"
by transfer (auto simp: Let_def)
lemma upper_times:
"upper (times A B) = Max {lower A * lower B, lower A * upper B, upper A * lower B, upper A * upper B}"
by transfer (auto simp: Let_def)
instance ..
end
lemma interval_eq_set_of_iff: "X = Y ⟷ set_of X = set_of Y" for X Y::"'a::order interval"
by (auto simp: set_of_eq interval_eq_iff)
subsection ‹Membership›
abbreviation (in preorder) in_interval (‹(‹notation=‹infix ∈⇩i››_/ ∈⇩i _)› [51, 51] 50)
where "in_interval x X ≡ x ∈ set_of X"
lemma in_interval_to_interval[intro!]: "a ∈⇩i interval_of a"
by (auto simp: set_of_eq)
lemma plus_in_intervalI:
fixes x y :: "'a :: ordered_ab_semigroup_add"
shows "x ∈⇩i X ⟹ y ∈⇩i Y ⟹ x + y ∈⇩i X + Y"
by (simp add: add_mono_thms_linordered_semiring(1) set_of_eq)
lemma connected_set_of[intro, simp]:
"connected (set_of X)" for X::"'a::linear_continuum_topology interval"
by (auto simp: set_of_eq )
lemma ex_sum_in_interval_lemma: "∃xa∈{la .. ua}. ∃xb∈{lb .. ub}. x = xa + xb"
if "la ≤ ua" "lb ≤ ub" "la + lb ≤ x" "x ≤ ua + ub"
"ua - la ≤ ub - lb"
for la b c d::"'a::linordered_ab_group_add"
proof -
define wa where "wa = ua - la"
define wb where "wb = ub - lb"
define w where "w = wa + wb"
define d where "d = x - la - lb"
define da where "da = max 0 (min wa (d - wa))"
define db where "db = d - da"
from that have nonneg: "0 ≤ wa" "0 ≤ wb" "0 ≤ w" "0 ≤ d" "d ≤ w"
by (auto simp add: wa_def wb_def w_def d_def add.commute le_diff_eq)
have "0 ≤ db"
by (auto simp: da_def nonneg db_def intro!: min.coboundedI2)
have "x = (la + da) + (lb + db)"
by (simp add: da_def db_def d_def)
moreover
have "x - la - ub ≤ da"
using that
unfolding da_def
by (intro max.coboundedI2) (auto simp: wa_def d_def diff_le_eq diff_add_eq)
then have "db ≤ wb"
by (auto simp: db_def d_def wb_def algebra_simps)
with ‹0 ≤ db› that nonneg have "lb + db ∈ {lb..ub}"
by (auto simp: wb_def algebra_simps)
moreover
have "da ≤ wa"
by (auto simp: da_def nonneg)
then have "la + da ∈ {la..ua}"
by (auto simp: da_def wa_def algebra_simps)
ultimately show ?thesis
by force
qed
lemma ex_sum_in_interval: "∃xa≥la. xa ≤ ua ∧ (∃xb≥lb. xb ≤ ub ∧ x = xa + xb)"
if a: "la ≤ ua" and b: "lb ≤ ub" and x: "la + lb ≤ x" "x ≤ ua + ub"
for la b c d::"'a::linordered_ab_group_add"
proof -
from linear consider "ua - la ≤ ub - lb" | "ub - lb ≤ ua - la"
by blast
then show ?thesis
proof cases
case 1
from ex_sum_in_interval_lemma[OF that 1]
show ?thesis by auto
next
case 2
from x have "lb + la ≤ x" "x ≤ ub + ua" by (simp_all add: ac_simps)
from ex_sum_in_interval_lemma[OF b a this 2]
show ?thesis by auto
qed
qed
lemma Icc_plus_Icc:
"{a .. b} + {c .. d} = {a + c .. b + d}"
if "a ≤ b" "c ≤ d"
for a b c d::"'a::linordered_ab_group_add"
using ex_sum_in_interval[OF that]
by (auto intro: add_mono simp: atLeastAtMost_iff Bex_def set_plus_def)
lemma set_of_plus:
fixes A :: "'a::linordered_ab_group_add interval"
shows "set_of (A + B) = set_of A + set_of B"
using Icc_plus_Icc[of "lower A" "upper A" "lower B" "upper B"]
by (auto simp: set_of_eq)
lemma plus_in_intervalE:
fixes xy :: "'a :: linordered_ab_group_add"
assumes "xy ∈⇩i X + Y"
obtains x y where "xy = x + y" "x ∈⇩i X" "y ∈⇩i Y"
using assms
unfolding set_of_plus set_plus_def
by auto
lemma set_of_uminus: "set_of (-X) = {- x | x. x ∈ set_of X}"
for X :: "'a :: ordered_ab_group_add interval"
by (auto simp: set_of_eq simp: le_minus_iff minus_le_iff
intro!: exI[where x="-x" for x])
lemma uminus_in_intervalI:
fixes x :: "'a :: ordered_ab_group_add"
shows "x ∈⇩i X ⟹ -x ∈⇩i -X"
by (auto simp: set_of_uminus)
lemma uminus_in_intervalD:
fixes x :: "'a :: ordered_ab_group_add"
shows "x ∈⇩i - X ⟹ - x ∈⇩i X"
by (auto simp: set_of_uminus)
lemma minus_in_intervalI:
fixes x y :: "'a :: ordered_ab_group_add"
shows "x ∈⇩i X ⟹ y ∈⇩i Y ⟹ x - y ∈⇩i X - Y"
by (metis diff_conv_add_uminus minus_interval_def plus_in_intervalI uminus_in_intervalI)
lemma set_of_minus: "set_of (X - Y) = {x - y | x y . x ∈ set_of X ∧ y ∈ set_of Y}"
for X Y :: "'a :: linordered_ab_group_add interval"
unfolding minus_interval_def set_of_plus set_of_uminus set_plus_def
by force
lemma times_in_intervalI:
fixes x y::"'a::linordered_ring"
assumes "x ∈⇩i X" "y ∈⇩i Y"
shows "x * y ∈⇩i X * Y"
proof -
define X1 where "X1 ≡ lower X"
define X2 where "X2 ≡ upper X"
define Y1 where "Y1 ≡ lower Y"
define Y2 where "Y2 ≡ upper Y"
from assms have assms: "X1 ≤ x" "x ≤ X2" "Y1 ≤ y" "y ≤ Y2"
by (auto simp: X1_def X2_def Y1_def Y2_def set_of_eq)
have "(X1 * Y1 ≤ x * y ∨ X1 * Y2 ≤ x * y ∨ X2 * Y1 ≤ x * y ∨ X2 * Y2 ≤ x * y) ∧
(X1 * Y1 ≥ x * y ∨ X1 * Y2 ≥ x * y ∨ X2 * Y1 ≥ x * y ∨ X2 * Y2 ≥ x * y)"
proof (cases x "0::'a" rule: linorder_cases)
case x0: less
show ?thesis
proof (cases "y < 0")
case y0: True
from y0 x0 assms have "x * y ≤ X1 * y" by (intro mult_right_mono_neg, auto)
also from x0 y0 assms have "X1 * y ≤ X1 * Y1" by (intro mult_left_mono_neg, auto)
finally have 1: "x * y ≤ X1 * Y1".
show ?thesis proof(cases "X2 ≤ 0")
case True
with assms have "X2 * Y2 ≤ X2 * y" by (auto intro: mult_left_mono_neg)
also from assms y0 have "... ≤ x * y" by (auto intro: mult_right_mono_neg)
finally have "X2 * Y2 ≤ x * y".
with 1 show ?thesis by auto
next
case False
with assms have "X2 * Y1 ≤ X2 * y" by (auto intro: mult_left_mono)
also from assms y0 have "... ≤ x * y" by (auto intro: mult_right_mono_neg)
finally have "X2 * Y1 ≤ x * y".
with 1 show ?thesis by auto
qed
next
case False
then have y0: "y ≥ 0" by auto
from x0 y0 assms have "X1 * Y2 ≤ x * Y2" by (intro mult_right_mono, auto)
also from y0 x0 assms have "... ≤ x * y" by (intro mult_left_mono_neg, auto)
finally have 1: "X1 * Y2 ≤ x * y".
show ?thesis
proof(cases "X2 ≤ 0")
case X2: True
from assms y0 have "x * y ≤ X2 * y" by (intro mult_right_mono)
also from assms X2 have "... ≤ X2 * Y1" by (auto intro: mult_left_mono_neg)
finally have "x * y ≤ X2 * Y1".
with 1 show ?thesis by auto
next
case X2: False
from assms y0 have "x * y ≤ X2 * y" by (intro mult_right_mono)
also from assms X2 have "... ≤ X2 * Y2" by (auto intro: mult_left_mono)
finally have "x * y ≤ X2 * Y2".
with 1 show ?thesis by auto
qed
qed
next
case [simp]: equal
with assms show ?thesis by (cases "Y2 ≤ 0", auto intro:mult_sign_intros)
next
case x0: greater
show ?thesis
proof (cases "y < 0")
case y0: True
from x0 y0 assms have "X2 * Y1 ≤ X2 * y" by (intro mult_left_mono, auto)
also from y0 x0 assms have "X2 * y ≤ x * y" by (intro mult_right_mono_neg, auto)
finally have 1: "X2 * Y1 ≤ x * y".
show ?thesis
proof(cases "Y2 ≤ 0")
case Y2: True
from x0 assms have "x * y ≤ x * Y2" by (auto intro: mult_left_mono)
also from assms Y2 have "... ≤ X1 * Y2" by (auto intro: mult_right_mono_neg)
finally have "x * y ≤ X1 * Y2".
with 1 show ?thesis by auto
next
case Y2: False
from x0 assms have "x * y ≤ x * Y2" by (auto intro: mult_left_mono)
also from assms Y2 have "... ≤ X2 * Y2" by (auto intro: mult_right_mono)
finally have "x * y ≤ X2 * Y2".
with 1 show ?thesis by auto
qed
next
case y0: False
from x0 y0 assms have "x * y ≤ X2 * y" by (intro mult_right_mono, auto)
also from y0 x0 assms have "... ≤ X2 * Y2" by (intro mult_left_mono, auto)
finally have 1: "x * y ≤ X2 * Y2".
show ?thesis
proof(cases "X1 ≤ 0")
case True
with assms have "X1 * Y2 ≤ X1 * y" by (auto intro: mult_left_mono_neg)
also from assms y0 have "... ≤ x * y" by (auto intro: mult_right_mono)
finally have "X1 * Y2 ≤ x * y".
with 1 show ?thesis by auto
next
case False
with assms have "X1 * Y1 ≤ X1 * y" by (auto intro: mult_left_mono)
also from assms y0 have "... ≤ x * y" by (auto intro: mult_right_mono)
finally have "X1 * Y1 ≤ x * y".
with 1 show ?thesis by auto
qed
qed
qed
hence min:"min (X1 * Y1) (min (X1 * Y2) (min (X2 * Y1) (X2 * Y2))) ≤ x * y"
and max:"x * y ≤ max (X1 * Y1) (max (X1 * Y2) (max (X2 * Y1) (X2 * Y2)))"
by (auto simp:min_le_iff_disj le_max_iff_disj)
show ?thesis using min max
by (auto simp: Let_def X1_def X2_def Y1_def Y2_def set_of_eq lower_times upper_times)
qed
lemma times_in_intervalE:
fixes xy :: "'a :: {linorder, real_normed_algebra, linear_continuum_topology}"
assumes "xy ∈⇩i X * Y"
obtains x y where "xy = x * y" "x ∈⇩i X" "y ∈⇩i Y"
proof -
let ?mult = "λ(x, y). x * y"
let ?XY = "set_of X × set_of Y"
have cont: "continuous_on ?XY ?mult"
by (auto intro!: tendsto_eq_intros simp: continuous_on_def split_beta')
have conn: "connected (?mult ` ?XY)"
by (rule connected_continuous_image[OF cont]) auto
have "lower (X * Y) ∈ ?mult ` ?XY" "upper (X * Y) ∈ ?mult ` ?XY"
by (auto simp: set_of_eq lower_times upper_times min_def max_def split: if_splits)
from connectedD_interval[OF conn this, of xy] assms
obtain x y where "xy = x * y" "x ∈⇩i X" "y ∈⇩i Y" by (auto simp: set_of_eq)
then show ?thesis ..
qed
thm times_in_intervalE[of "1::real"]
lemma set_of_times: "set_of (X * Y) = {x * y | x y. x ∈ set_of X ∧ y ∈ set_of Y}"
for X Y::"'a :: {linordered_ring, real_normed_algebra, linear_continuum_topology} interval"
by (auto intro!: times_in_intervalI elim!: times_in_intervalE)
instance "interval" :: (linordered_idom) cancel_semigroup_add
proof qed (auto simp: interval_eq_iff)
lemma interval_mul_commute: "A * B = B * A" for A B:: "'a::linordered_idom interval"
by (simp add: interval_eq_iff lower_times upper_times ac_simps)
lemma interval_times_zero_right[simp]: "A * 0 = 0" for A :: "'a::linordered_ring interval"
by (simp add: interval_eq_iff lower_times upper_times ac_simps)
lemma interval_times_zero_left[simp]:
"0 * A = 0" for A :: "'a::linordered_ring interval"
by (simp add: interval_eq_iff lower_times upper_times ac_simps)
instantiation "interval" :: ("{preorder,one}") one
begin
lift_definition one_interval::"'a interval" is "(1, 1)" by auto
lemma lower_one[simp]: "lower 1 = 1"
by transfer auto
lemma upper_one[simp]: "upper 1 = 1"
by transfer auto
instance proof qed
end
instance interval :: ("{one, preorder, linorder, times}") power
proof qed
lemma set_of_one[simp]: "set_of (1::'a::{one, order} interval) = {1}"
by (auto simp: set_of_eq)
instance "interval" ::
("{linordered_idom, real_normed_algebra, linear_continuum_topology}") monoid_mult
apply standard
unfolding interval_eq_set_of_iff set_of_times
subgoal
by (auto simp: interval_eq_set_of_iff set_of_times; metis mult.assoc)
by auto
lemma one_times_ivl_left[simp]: "1 * A = A" for A :: "'a::linordered_idom interval"
by (simp add: interval_eq_iff lower_times upper_times ac_simps min_def max_def)
lemma one_times_ivl_right[simp]: "A * 1 = A" for A :: "'a::linordered_idom interval"
by (metis interval_mul_commute one_times_ivl_left)
lemma set_of_power_mono: "a^n ∈ set_of (A^n)" if "a ∈ set_of A"
for a :: "'a::linordered_idom"
using that
by (induction n) (auto intro!: times_in_intervalI)
lemma set_of_add_cong:
"set_of (A + B) = set_of (A' + B')"
if "set_of A = set_of A'" "set_of B = set_of B'"
for A :: "'a::linordered_ab_group_add interval"
unfolding set_of_plus that ..
lemma set_of_add_inc_left:
"set_of (A + B) ⊆ set_of (A' + B)"
if "set_of A ⊆ set_of A'"
for A :: "'a::linordered_ab_group_add interval"
unfolding set_of_plus using that by (auto simp: set_plus_def)
lemma set_of_add_inc_right:
"set_of (A + B) ⊆ set_of (A + B')"
if "set_of B ⊆ set_of B'"
for A :: "'a::linordered_ab_group_add interval"
using set_of_add_inc_left[OF that]
by (simp add: add.commute)
lemma set_of_add_inc:
"set_of (A + B) ⊆ set_of (A' + B')"
if "set_of A ⊆ set_of A'" "set_of B ⊆ set_of B'"
for A :: "'a::linordered_ab_group_add interval"
using set_of_add_inc_left[OF that(1)] set_of_add_inc_right[OF that(2)]
by auto
lemma set_of_neg_inc:
"set_of (-A) ⊆ set_of (-A')"
if "set_of A ⊆ set_of A'"
for A :: "'a::ordered_ab_group_add interval"
using that
unfolding set_of_uminus
by auto
lemma set_of_sub_inc_left:
"set_of (A - B) ⊆ set_of (A' - B)"
if "set_of A ⊆ set_of A'"
for A :: "'a::linordered_ab_group_add interval"
using that
unfolding set_of_minus
by auto
lemma set_of_sub_inc_right:
"set_of (A - B) ⊆ set_of (A - B')"
if "set_of B ⊆ set_of B'"
for A :: "'a::linordered_ab_group_add interval"
using that
unfolding set_of_minus
by auto
lemma set_of_sub_inc:
"set_of (A - B) ⊆ set_of (A' - B')"
if "set_of A ⊆ set_of A'" "set_of B ⊆ set_of B'"
for A :: "'a::linordered_idom interval"
using set_of_sub_inc_left[OF that(1)] set_of_sub_inc_right[OF that(2)]
by auto
lemma set_of_mul_inc_right:
"set_of (A * B) ⊆ set_of (A * B')"
if "set_of B ⊆ set_of B'"
for A :: "'a::linordered_ring interval"
using that
apply transfer
apply (clarsimp simp add: Let_def)
by (smt (verit, best) linorder_le_cases max.coboundedI1 max.coboundedI2 min.absorb1 min.coboundedI2 mult_left_mono mult_left_mono_neg)
lemma set_of_distrib_left:
"set_of (B * (A1 + A2)) ⊆ set_of (B * A1 + B * A2)"
for A1 :: "'a::linordered_ring interval"
apply transfer
apply (clarsimp simp: Let_def distrib_left distrib_right)
apply (intro conjI)
apply (metis add_mono min.cobounded1 min.left_commute)
apply (metis add_mono min.cobounded1 min.left_commute)
apply (metis add_mono min.cobounded1 min.left_commute)
apply (metis add_mono min.assoc min.cobounded2)
apply (meson add_mono order.trans max.cobounded1 max.cobounded2)
apply (meson add_mono order.trans max.cobounded1 max.cobounded2)
apply (meson add_mono order.trans max.cobounded1 max.cobounded2)
apply (meson add_mono order.trans max.cobounded1 max.cobounded2)
done
lemma set_of_distrib_right:
"set_of ((A1 + A2) * B) ⊆ set_of (A1 * B + A2 * B)"
for A1 A2 B :: "'a::{linordered_ring, real_normed_algebra, linear_continuum_topology} interval"
unfolding set_of_times set_of_plus set_plus_def
using distrib_right by blast
lemma set_of_mul_inc_left:
"set_of (A * B) ⊆ set_of (A' * B)"
if "set_of A ⊆ set_of A'"
for A :: "'a::{linordered_ring, real_normed_algebra, linear_continuum_topology} interval"
using that
unfolding set_of_times
by auto
lemma set_of_mul_inc:
"set_of (A * B) ⊆ set_of (A' * B')"
if "set_of A ⊆ set_of A'" "set_of B ⊆ set_of B'"
for A :: "'a::{linordered_ring, real_normed_algebra, linear_continuum_topology} interval"
using that unfolding set_of_times by auto
lemma set_of_pow_inc:
"set_of (A^n) ⊆ set_of (A'^n)"
if "set_of A ⊆ set_of A'"
for A :: "'a::{linordered_idom, real_normed_algebra, linear_continuum_topology} interval"
using that
by (induction n, simp_all add: set_of_mul_inc)
lemma set_of_distrib_right_left:
"set_of ((A1 + A2) * (B1 + B2)) ⊆ set_of (A1 * B1 + A1 * B2 + A2 * B1 + A2 * B2)"
for A1 :: "'a::{linordered_idom, real_normed_algebra, linear_continuum_topology} interval"
proof-
have "set_of ((A1 + A2) * (B1 + B2)) ⊆ set_of (A1 * (B1 + B2) + A2 * (B1 + B2))"
by (rule set_of_distrib_right)
also have "... ⊆ set_of ((A1 * B1 + A1 * B2) + A2 * (B1 + B2))"
by (rule set_of_add_inc_left[OF set_of_distrib_left])
also have "... ⊆ set_of ((A1 * B1 + A1 * B2) + (A2 * B1 + A2 * B2))"
by (rule set_of_add_inc_right[OF set_of_distrib_left])
finally show ?thesis
by (simp add: add.assoc)
qed
lemma mult_bounds_enclose_zero1:
"min (la * lb) (min (la * ub) (min (lb * ua) (ua * ub))) ≤ 0"
"0 ≤ max (la * lb) (max (la * ub) (max (lb * ua) (ua * ub)))"
if "la ≤ 0" "0 ≤ ua"
for la lb ua ub:: "'a::linordered_idom"
subgoal by (metis (no_types, opaque_lifting) that eq_iff min_le_iff_disj mult_zero_left mult_zero_right
zero_le_mult_iff)
subgoal by (metis that le_max_iff_disj mult_zero_right order_refl zero_le_mult_iff)
done
lemma mult_bounds_enclose_zero2:
"min (la * lb) (min (la * ub) (min (lb * ua) (ua * ub))) ≤ 0"
"0 ≤ max (la * lb) (max (la * ub) (max (lb * ua) (ua * ub)))"
if "lb ≤ 0" "0 ≤ ub"
for la lb ua ub:: "'a::linordered_idom"
using mult_bounds_enclose_zero1[OF that, of la ua]
by (simp_all add: ac_simps)
lemma set_of_mul_contains_zero:
"0 ∈ set_of (A * B)"
if "0 ∈ set_of A ∨ 0 ∈ set_of B"
for A :: "'a::linordered_idom interval"
using that
by (auto simp: set_of_eq lower_times upper_times algebra_simps mult_le_0_iff
mult_bounds_enclose_zero1 mult_bounds_enclose_zero2)
instance "interval" :: ("{linordered_semiring, zero, times}") mult_zero
by (standard; transfer; auto)
lift_definition min_interval::"'a::linorder interval ⇒ 'a interval ⇒ 'a interval" is
"λ(l1, u1). λ(l2, u2). (min l1 l2, min u1 u2)"
by (auto simp: min_def)
lemma lower_min_interval[simp]: "lower (min_interval x y) = min (lower x) (lower y)"
by transfer auto
lemma upper_min_interval[simp]: "upper (min_interval x y) = min (upper x) (upper y)"
by transfer auto
lemma min_intervalI:
"a ∈⇩i A ⟹ b ∈⇩i B ⟹ min a b ∈⇩i min_interval A B"
by (auto simp: set_of_eq min_def)
lift_definition max_interval::"'a::linorder interval ⇒ 'a interval ⇒ 'a interval" is
"λ(l1, u1). λ(l2, u2). (max l1 l2, max u1 u2)"
by (auto simp: max_def)
lemma lower_max_interval[simp]: "lower (max_interval x y) = max (lower x) (lower y)"
by transfer auto
lemma upper_max_interval[simp]: "upper (max_interval x y) = max (upper x) (upper y)"
by transfer auto
lemma max_intervalI:
"a ∈⇩i A ⟹ b ∈⇩i B ⟹ max a b ∈⇩i max_interval A B"
by (auto simp: set_of_eq max_def)
lift_definition abs_interval::"'a::linordered_idom interval ⇒ 'a interval" is
"(λ(l,u). (if l < 0 ∧ 0 < u then 0 else min ¦l¦ ¦u¦, max ¦l¦ ¦u¦))"
by auto
lemma lower_abs_interval[simp]:
"lower (abs_interval x) = (if lower x < 0 ∧ 0 < upper x then 0 else min ¦lower x¦ ¦upper x¦)"
by transfer auto
lemma upper_abs_interval[simp]: "upper (abs_interval x) = max ¦lower x¦ ¦upper x¦"
by transfer auto
lemma in_abs_intervalI1:
"lx < 0 ⟹ 0 < ux ⟹ 0 ≤ xa ⟹ xa ≤ max (- lx) (ux) ⟹ xa ∈ abs ` {lx..ux}"
for xa::"'a::linordered_idom"
by (metis abs_minus_cancel abs_of_nonneg atLeastAtMost_iff image_eqI le_less le_max_iff_disj
le_minus_iff neg_le_0_iff_le order_trans)
lemma in_abs_intervalI2:
"min (¦lx¦) ¦ux¦ ≤ xa ⟹ xa ≤ max ¦lx¦ ¦ux¦ ⟹ lx ≤ ux ⟹ 0 ≤ lx ∨ ux ≤ 0 ⟹
xa ∈ abs ` {lx..ux}"
for xa::"'a::linordered_idom"
by (force intro: image_eqI[where x="-xa"] image_eqI[where x="xa"])
lemma set_of_abs_interval: "set_of (abs_interval x) = abs ` set_of x"
by (auto simp: set_of_eq not_less intro: in_abs_intervalI1 in_abs_intervalI2 cong del: image_cong_simp)
fun split_domain :: "('a::preorder interval ⇒ 'a interval list) ⇒ 'a interval list ⇒ 'a interval list list"
where "split_domain split [] = [[]]"
| "split_domain split (I#Is) = (
let S = split I;
D = split_domain split Is
in concat (map (λd. map (λs. s # d) S) D)
)"
context notes [[typedef_overloaded]] begin
lift_definition(code_dt) split_interval::"'a::linorder interval ⇒ 'a ⇒ ('a interval × 'a interval)"
is "λ(l, u) x. ((min l x, max l x), (min u x, max u x))"
by (auto simp: min_def)
end
lemma split_domain_nonempty:
assumes "⋀I. split I ≠ []"
shows "split_domain split I ≠ []"
using last_in_set assms
by (induction I, auto)
lemma lower_split_interval1: "lower (fst (split_interval X m)) = min (lower X) m"
and lower_split_interval2: "lower (snd (split_interval X m)) = min (upper X) m"
and upper_split_interval1: "upper (fst (split_interval X m)) = max (lower X) m"
and upper_split_interval2: "upper (snd (split_interval X m)) = max (upper X) m"
subgoal by transfer auto
subgoal by transfer (auto simp: min.commute)
subgoal by transfer auto
subgoal by transfer auto
done
lemma split_intervalD: "split_interval X x = (A, B) ⟹ set_of X ⊆ set_of A ∪ set_of B"
unfolding set_of_eq
by transfer (auto simp: min_def max_def split: if_splits)
instantiation interval :: ("{topological_space, preorder}") topological_space
begin
definition open_interval_def[code del]: "open (X::'a interval set) =
(∀x∈X.
∃A B.
open A ∧
open B ∧
lower x ∈ A ∧ upper x ∈ B ∧ Interval ` (A × B) ⊆ X)"
instance
proof
show "open (UNIV :: ('a interval) set)"
unfolding open_interval_def by auto
next
fix S T :: "('a interval) set"
assume "open S" "open T"
show "open (S ∩ T)"
unfolding open_interval_def
proof (safe)
fix x assume "x ∈ S" "x ∈ T"
from ‹x ∈ S› ‹open S› obtain Sl Su where S:
"open Sl" "open Su" "lower x ∈ Sl" "upper x ∈ Su" "Interval ` (Sl × Su) ⊆ S"
by (auto simp: open_interval_def)
from ‹x ∈ T› ‹open T› obtain Tl Tu where T:
"open Tl" "open Tu" "lower x ∈ Tl" "upper x ∈ Tu" "Interval ` (Tl × Tu) ⊆ T"
by (auto simp: open_interval_def)
let ?L = "Sl ∩ Tl" and ?U = "Su ∩ Tu"
have "open ?L ∧ open ?U ∧ lower x ∈ ?L ∧ upper x ∈ ?U ∧ Interval ` (?L × ?U) ⊆ S ∩ T"
using S T by (auto simp add: open_Int)
then show "∃A B. open A ∧ open B ∧ lower x ∈ A ∧ upper x ∈ B ∧ Interval ` (A × B) ⊆ S ∩ T"
by fast
qed
qed (unfold open_interval_def, fast)
end
subsection ‹Quickcheck›
lift_definition Ivl::"'a ⇒ 'a::preorder ⇒ 'a interval" is "λa b. (min a b, b)"
by (auto simp: min_def)
instantiation interval :: ("{exhaustive,preorder}") exhaustive
begin
definition exhaustive_interval::"('a interval ⇒ (bool × term list) option)
⇒ natural ⇒ (bool × term list) option"
where
"exhaustive_interval f d =
Quickcheck_Exhaustive.exhaustive (λx. Quickcheck_Exhaustive.exhaustive (λy. f (Ivl x y)) d) d"
instance ..
end
context
includes term_syntax
begin
definition [code_unfold]:
"valtermify_interval x y = Code_Evaluation.valtermify (Ivl::'a::{preorder,typerep}⇒_) {⋅} x {⋅} y"
end
instantiation interval :: ("{full_exhaustive,preorder,typerep}") full_exhaustive
begin
definition full_exhaustive_interval::
"('a interval × (unit ⇒ term) ⇒ (bool × term list) option)
⇒ natural ⇒ (bool × term list) option" where
"full_exhaustive_interval f d =
Quickcheck_Exhaustive.full_exhaustive
(λx. Quickcheck_Exhaustive.full_exhaustive (λy. f (valtermify_interval x y)) d) d"
instance ..
end
instantiation interval :: ("{random,preorder,typerep}") random
begin
definition random_interval ::
"natural
⇒ natural × natural
⇒ ('a interval × (unit ⇒ term)) × natural × natural" where
"random_interval i =
scomp (Quickcheck_Random.random i)
(λman. scomp (Quickcheck_Random.random i) (λexp. Pair (valtermify_interval man exp)))"
instance ..
end
lifting_update interval.lifting
lifting_forget interval.lifting
end