--- a/src/HOL/Library/Interval.thy Sun Nov 03 19:59:56 2019 -0500
+++ b/src/HOL/Library/Interval.thy Mon Nov 04 21:41:55 2019 -0500
@@ -43,6 +43,22 @@
is "\<lambda>a b. if a \<le> b then Some (a, b) else None"
by auto
+lemma Interval'_split:
+ "P (Interval' a b) \<longleftrightarrow>
+ (\<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) \<longleftrightarrow>
+ \<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
--- a/src/HOL/Library/Interval_Float.thy Sun Nov 03 19:59:56 2019 -0500
+++ b/src/HOL/Library/Interval_Float.thy Mon Nov 04 21:41:55 2019 -0500
@@ -105,6 +105,9 @@
lemma in_round_intervalI: "x \<in>\<^sub>r A \<Longrightarrow> x \<in>\<^sub>r (round_interval prec A)"
by (auto simp: set_of_eq float_round_down_le float_round_up_le)
+lemma zero_in_float_intervalI: "0 \<in>\<^sub>r 0"
+ by (auto simp: set_of_eq)
+
lemma plus_in_float_intervalI: "a + b \<in>\<^sub>r A + B" if "a \<in>\<^sub>r A" "b \<in>\<^sub>r B"
using that
by (auto simp: set_of_eq)