# HG changeset patch
# User nipkow
# Date 1317198956 -7200
# Node ID 2a0d7be998bb892596088c1df98a2bccd51302bd
# Parent  32c90199df2e5068ebcc9a948b7f13041bb55e53
added nice interval syntax

diff -r 32c90199df2e -r 2a0d7be998bb src/HOL/IMP/Abs_Int0_fun.thy
--- a/src/HOL/IMP/Abs_Int0_fun.thy	Wed Sep 28 09:59:55 2011 +0200
+++ b/src/HOL/IMP/Abs_Int0_fun.thy	Wed Sep 28 10:35:56 2011 +0200
@@ -11,11 +11,11 @@
 datatype 'a acom =
   SKIP   'a                           ("SKIP {_}") |
   Assign name aexp 'a                 ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
-  Semi   "'a acom" "'a acom"          ("_;// _"  [60, 61] 60) |
+  Semi   "'a acom" "'a acom"          ("_;//_"  [60, 61] 60) |
   If     bexp "'a acom" "'a acom" 'a
-    ("((IF _/ THEN _/ ELSE _)/ {_})"  [0, 0, 61, 0] 61) |
+    ("(IF _/ THEN _/ ELSE _//{_})"  [0, 0, 61, 0] 61) |
   While  'a bexp "'a acom" 'a
-    ("({_}// WHILE _/ DO (_)// {_})"  [0, 0, 61, 0] 61)
+    ("({_}//WHILE _/ DO (_)//{_})"  [0, 0, 61, 0] 61)
 
 fun post :: "'a acom \<Rightarrow>'a" where
 "post (SKIP {P}) = P" |
diff -r 32c90199df2e -r 2a0d7be998bb src/HOL/IMP/Abs_Int1_ivl.thy
--- a/src/HOL/IMP/Abs_Int1_ivl.thy	Wed Sep 28 09:59:55 2011 +0200
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy	Wed Sep 28 10:35:56 2011 +0200
@@ -14,7 +14,16 @@
   I None (Some h) \<Rightarrow> {..h} |
   I None None \<Rightarrow> UNIV)"
 
-definition "num_ivl n = I (Some n) (Some n)"
+abbreviation I_Some_Some :: "int \<Rightarrow> int \<Rightarrow> ivl"  ("{_\<dots>_}") where
+"{lo\<dots>hi} == I (Some lo) (Some hi)"
+abbreviation I_Some_None :: "int \<Rightarrow> ivl"  ("{_\<dots>}") where
+"{lo\<dots>} == I (Some lo) None"
+abbreviation I_None_Some :: "int \<Rightarrow> ivl"  ("{\<dots>_}") where
+"{\<dots>hi} == I None (Some hi)"
+abbreviation I_None_None :: "ivl"  ("{\<dots>}") where
+"{\<dots>} == I None None"
+
+definition "num_ivl n = {n\<dots>n}"
 
 instantiation option :: (plus)plus
 begin
@@ -27,10 +36,10 @@
 
 end
 
-definition empty where "empty = I (Some 1) (Some 0)"
+definition empty where "empty = {1\<dots>0}"
 
 fun is_empty where
-"is_empty(I (Some l) (Some h)) = (h<l)" |
+"is_empty {l\<dots>h} = (h<l)" |
 "is_empty _ = False"
 
 lemma [simp]: "is_empty(I l h) =
@@ -70,7 +79,7 @@
   else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
           I (min_option False l1 l2) (max_option True h1 h2))"
 
-definition "\<top> = I None None"
+definition "\<top> = {\<dots>}"
 
 instance
 proof
@@ -221,12 +230,6 @@
  THEN ''y'' ::= Plus (V ''y'') (V ''x'')
  ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
 
-translations
-"{i..j}" <= "CONST I (CONST Some i) (CONST Some j)"
-"{..j}" <= "CONST I (CONST None) (CONST Some j)"
-"{i..}" <= "CONST I (CONST Some i) (CONST None)"
-"CONST UNIV" <= "CONST I (CONST None) (CONST None)"
-
 value [code] "show_acom (AI_ivl test1_ivl)"
 
 value [code] "show_acom (AI_const test3_const)"