# HG changeset patch
# User nipkow
# Date 1367889863 -7200
# Node ID 150d3494a8f273b184dff46de7049a61589f2b95
# Parent  e7fac4a483b5122222c40ccdfd3a6cdd95bc357c
tuned

diff -r e7fac4a483b5 -r 150d3494a8f2 src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Mon May 06 22:49:26 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Tue May 07 03:24:23 2013 +0200
@@ -33,11 +33,12 @@
 lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)"
 by(auto simp: eq_ivl_def)
 
-fun in_ivl_rep :: "int \<Rightarrow> eint2 \<Rightarrow> bool" where
-"in_ivl_rep k (l,h) \<longleftrightarrow> l \<le> Fin k \<and> Fin k \<le> h"
+lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool"
+  is "\<lambda>i (l,h). l \<le> Fin i \<and> Fin i \<le> h"
+by(auto simp: eq_ivl_def \<gamma>_rep_def)
 
-lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" is in_ivl_rep
-by(auto simp: eq_ivl_def \<gamma>_rep_def)
+lemma in_ivl_nice: "in_ivl i [l\<dots>h] = (l \<le> Fin i \<and> Fin i \<le> h)"
+by transfer simp
 
 definition is_empty_rep :: "eint2 \<Rightarrow> bool" where
 "is_empty_rep p = (let (l,h) = p in l>h | l=Pinf & h=Pinf | l=Minf & h=Minf)"