Quelle Interval.thy Sprache: Isabelle

(* Title: Interval
   Author: Christoph Traut, TU Muenchen
           Fabian Immler, TU Muenchen
*)
section \<open>Interval Type\<close>
theory Interval
  imports
    Complex_Main
    Lattice_Algebras
    Set_Algebras
begin

text \<open>A type of non-empty, closed intervals.\<close>

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 \<Rightarrow> 'a::preorder \<Rightarrow> 'a interval option"
  is "\a b. if a \ b then Some (a, b) else None"
  by auto

lemma Interval'_split:
  "P (Interval' a b) \
    (\<forall>ivl. a \<le> b \<longrightarrow> lower ivl = a \<longrightarrow> upper ivl = b \<longrightarrow> P (Some ivl)) \<and> (\<not>a\<le>b \<longrightarrow> P None)"
  by transfer auto

lemma Interval'_split_asm:
  "P (Interval' a b) \
    \<not>((\<exists>ivl. a \<le> b \<and> lower ivl = a \<and> upper ivl = b \<and> \<not>P (Some ivl)) \<or> (\<not>a\<le>b \<and> \<not>P None))"
  unfolding Interval'_split
  by auto

lemmas Interval'_splits = Interval'_split Interval'_split_asm

lemma Interval'_eq_Some: "Interval' a b = Some i \<Longrightarrow> lower i = a \<and> 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 \<open>Membership\<close>

abbreviation (in preorder) in_interval (\<open>(\<open>notation=\<open>infix \<in>\<^sub>i\<close>\<close>_/ \<in>\<^sub>i _)\<close> [51, 51] 50)
  where "in_interval x X \ x \ set_of X"

lemma in_interval_to_interval[intro!]: "a \\<^sub>i interval_of a"
  by (auto simp: set_of_eq)

lemma plus_in_intervalI:
  fixes x y :: "'a :: ordered_ab_semigroup_add"
  shows "x \\<^sub>i X \ y \\<^sub>i Y \ x + y \\<^sub>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 \<open>0 \<le> db\<close> that nonneg have "lb + db \<in> {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 \\<^sub>i X + Y"
  obtains x y where "xy = x + y" "x \\<^sub>i X" "y \\<^sub>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 \\<^sub>i X \ -x \\<^sub>i -X"
  by (auto simp: set_of_uminus)

lemma uminus_in_intervalD:
  fixes x :: "'a :: ordered_ab_group_add"
  shows "x \\<^sub>i - X \ - x \\<^sub>i X"
  by (auto simp: set_of_uminus)

lemma minus_in_intervalI:
  fixes x y :: "'a :: ordered_ab_group_add"
  shows "x \\<^sub>i X \ y \\<^sub>i Y \ x - y \\<^sub>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 \\<^sub>i X" "y \\<^sub>i Y"
  shows "x * y \\<^sub>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 \<ge> x * y \<or> X1 * Y2 \<ge> x * y \<or> X2 * Y1 \<ge> x * y \<or> X2 * Y2 \<ge> 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}"
    \<comment> \<open>TODO: linear continuum topology is pretty strong\<close>
  assumes "xy \\<^sub>i X * Y"
  obtains x y where "xy = x * y" "x \\<^sub>i X" "y \\<^sub>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 \\<^sub>i X" "y \\<^sub>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 \\<^sub>i A \ b \\<^sub>i B \ min a b \\<^sub>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 \\<^sub>i A \ b \\<^sub>i B \ max a b \\<^sub>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 \<in> 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 (\<lambda>d. map (\<lambda>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) =
  (\<forall>x\<in>X.
      \<exists>A B.
         open A \<and>
         open B \<and>
         lower x \<in> A \<and> upper x \<in> B \<and> Interval ` (A \<times> B) \<subseteq> 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 \<open>x \<in> S\<close> \<open>open S\<close> 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 \<open>x \<in> T\<close> \<open>open T\<close> 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 \<open>Quickcheck\<close>

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)
     \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option"
  where
    "exhaustive_interval f d =
    Quickcheck_Exhaustive.exhaustive (\<lambda>x. Quickcheck_Exhaustive.exhaustive (\<lambda>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)
     \<Rightarrow> natural \<Rightarrow> (bool \<times> term list) option" where
  "full_exhaustive_interval f d =
    Quickcheck_Exhaustive.full_exhaustive
      (\<lambda>x. Quickcheck_Exhaustive.full_exhaustive (\<lambda>y. f (valtermify_interval x y)) d) d"

instance ..

end

instantiation interval :: ("{random,preorder,typerep}") random
begin

definition random_interval ::
  "natural
  \<Rightarrow> natural \<times> natural
     \<Rightarrow> ('a interval \<times> (unit \<Rightarrow> term)) \<times> natural \<times> natural" where
  "random_interval i =
  scomp (Quickcheck_Random.random i)
    (\<lambda>man. scomp (Quickcheck_Random.random i) (\<lambda>exp. Pair (valtermify_interval man exp)))"

instance ..

end

lifting_update interval.lifting
lifting_forget interval.lifting

end

quality98%

¤ Dauer der Verarbeitung: 0.6 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.