# HG changeset patch
# User nipkow
# Date 1367551514 -7200
# Node ID f16bd7d2359c0094e8823a17af4cdc453b2f0c43
# Parent  a331fbefcdb1bb52c37e80c933b318e791b067a5
added lemma

diff -r a331fbefcdb1 -r f16bd7d2359c src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Fri May 03 02:52:25 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Fri May 03 05:25:14 2013 +0200
@@ -21,11 +21,14 @@
 quotient_type ivl = eint2 / eq_ivl
 by(rule equivpI)(auto simp: reflp_def symp_def transp_def eq_ivl_def)
 
+abbreviation ivl_abbr :: "eint \<Rightarrow> eint \<Rightarrow> ivl" ("[_\<dots>_]") where
+"[l\<dots>h] == abs_ivl(l,h)"
+
 lift_definition \<gamma>_ivl :: "ivl \<Rightarrow> int set" is \<gamma>_rep
 by(simp add: eq_ivl_def)
 
-abbreviation ivl_abbr :: "eint \<Rightarrow> eint \<Rightarrow> ivl" ("[_\<dots>_]") where
-"[l\<dots>h] == abs_ivl(l,h)"
+lemma \<gamma>_ivl_nice: "\<gamma>_ivl[l\<dots>h] = {i. l \<le> Fin i \<and> Fin i \<le> h}"
+by transfer (simp add: \<gamma>_rep_def)
 
 lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)"
 by(auto simp: eq_ivl_def)