# HG changeset patch
# User immler
# Date 1572921715 18000
# Node ID bd3d4702b4f2998ba6607d5a9dc8a583c70284bf
# Parent  f630f2e707a6ef4b3e05581622adb9f180039053
add lemmas

diff -r f630f2e707a6 -r bd3d4702b4f2 src/HOL/Library/Interval.thy
--- 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
diff -r f630f2e707a6 -r bd3d4702b4f2 src/HOL/Library/Interval_Float.thy
--- 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)