# HG changeset patch
# User haftmann
# Date 1324738503 -3600
# Node ID d3325de5f2999b37bbfffa7197507f5234951d69
# Parent  e3accf78bb07ce074d4e7bcf53ba6104bca9bb14
executable intervals

diff -r e3accf78bb07 -r d3325de5f299 src/HOL/IMP/Abs_Int1_ivl.thy
--- 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
 
diff -r e3accf78bb07 -r d3325de5f299 src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy
--- 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