--- a/src/HOL/IMP/Abs_Int1_ivl.thy Sat Dec 24 15:54:58 2011 +0100
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy Sat Dec 24 15:55:03 2011 +0100
@@ -1,7 +1,7 @@
(* Author: Tobias Nipkow *)
theory Abs_Int1_ivl
-imports Abs_Int1 Abs_Int_Tests
+imports Abs_Int1 Abs_Int_Tests "~~/src/HOL/Library/More_Set"
begin
subsection "Interval Analysis"
@@ -25,6 +25,20 @@
definition "num_ivl n = {n\<dots>n}"
+definition
+ "contained_in i k \<longleftrightarrow> k \<in> rep_ivl i"
+
+lemma in_rep_ivl_contained_in [code_unfold_post]:
+ "k \<in> rep_ivl i \<longleftrightarrow> contained_in i k"
+ by (simp only: contained_in_def)
+
+lemma contained_in_simps [code]:
+ "contained_in (I (Some l) (Some h)) k \<longleftrightarrow> l \<le> k \<and> k \<le> h"
+ "contained_in (I (Some l) None) k \<longleftrightarrow> l \<le> k"
+ "contained_in (I None (Some h)) k \<longleftrightarrow> k \<le> h"
+ "contained_in (I None None) k \<longleftrightarrow> True"
+ by (simp_all add: contained_in_def rep_ivl_def)
+
instantiation option :: (plus)plus
begin
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Sat Dec 24 15:54:58 2011 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Sat Dec 24 15:55:03 2011 +0100
@@ -1,7 +1,7 @@
(* Author: Tobias Nipkow *)
theory Abs_Int_den1_ivl
-imports Abs_Int_den1
+imports Abs_Int_den1 "~~/src/HOL/Library/More_Set"
begin
subsection "Interval Analysis"
@@ -21,6 +21,20 @@
definition "num_ivl n = I (Some n) (Some n)"
+definition
+ "contained_in i k \<longleftrightarrow> k \<in> rep_ivl i"
+
+lemma in_rep_ivl_contained_in [code_unfold_post]:
+ "k \<in> rep_ivl i \<longleftrightarrow> contained_in i k"
+ by (simp only: contained_in_def)
+
+lemma contained_in_simps [code]:
+ "contained_in (I (Some l) (Some h)) k \<longleftrightarrow> l \<le> k \<and> k \<le> h"
+ "contained_in (I (Some l) None) k \<longleftrightarrow> l \<le> k"
+ "contained_in (I None (Some h)) k \<longleftrightarrow> k \<le> h"
+ "contained_in (I None None) k \<longleftrightarrow> True"
+ by (simp_all add: contained_in_def rep_ivl_def)
+
instantiation option :: (plus)plus
begin