--- 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)