1.1 --- a/src/HOL/IMP/Abs_Int0_fun.thy	Wed Sep 28 09:59:55 2011 +0200
     1.2 +++ b/src/HOL/IMP/Abs_Int0_fun.thy	Wed Sep 28 10:35:56 2011 +0200
     1.3 @@ -11,11 +11,11 @@
     1.4  datatype 'a acom =
     1.5    SKIP   'a                           ("SKIP {_}") |
     1.6    Assign name aexp 'a                 ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
     1.7 -  Semi   "'a acom" "'a acom"          ("_;// _"  [60, 61] 60) |
     1.8 +  Semi   "'a acom" "'a acom"          ("_;//_"  [60, 61] 60) |
     1.9    If     bexp "'a acom" "'a acom" 'a
    1.10 -    ("((IF _/ THEN _/ ELSE _)/ {_})"  [0, 0, 61, 0] 61) |
    1.11 +    ("(IF _/ THEN _/ ELSE _//{_})"  [0, 0, 61, 0] 61) |
    1.12    While  'a bexp "'a acom" 'a
    1.13 -    ("({_}// WHILE _/ DO (_)// {_})"  [0, 0, 61, 0] 61)
    1.14 +    ("({_}//WHILE _/ DO (_)//{_})"  [0, 0, 61, 0] 61)
    1.15  
    1.16  fun post :: "'a acom \<Rightarrow>'a" where
    1.17  "post (SKIP {P}) = P" |

     2.1 --- a/src/HOL/IMP/Abs_Int1_ivl.thy	Wed Sep 28 09:59:55 2011 +0200
     2.2 +++ b/src/HOL/IMP/Abs_Int1_ivl.thy	Wed Sep 28 10:35:56 2011 +0200
     2.3 @@ -14,7 +14,16 @@
     2.4    I None (Some h) \<Rightarrow> {..h} |
     2.5    I None None \<Rightarrow> UNIV)"
     2.6  
     2.7 -definition "num_ivl n = I (Some n) (Some n)"
     2.8 +abbreviation I_Some_Some :: "int \<Rightarrow> int \<Rightarrow> ivl"  ("{_\<dots>_}") where
     2.9 +"{lo\<dots>hi} == I (Some lo) (Some hi)"
    2.10 +abbreviation I_Some_None :: "int \<Rightarrow> ivl"  ("{_\<dots>}") where
    2.11 +"{lo\<dots>} == I (Some lo) None"
    2.12 +abbreviation I_None_Some :: "int \<Rightarrow> ivl"  ("{\<dots>_}") where
    2.13 +"{\<dots>hi} == I None (Some hi)"
    2.14 +abbreviation I_None_None :: "ivl"  ("{\<dots>}") where
    2.15 +"{\<dots>} == I None None"
    2.16 +
    2.17 +definition "num_ivl n = {n\<dots>n}"
    2.18  
    2.19  instantiation option :: (plus)plus
    2.20  begin
    2.21 @@ -27,10 +36,10 @@
    2.22  
    2.23  end
    2.24  
    2.25 -definition empty where "empty = I (Some 1) (Some 0)"
    2.26 +definition empty where "empty = {1\<dots>0}"
    2.27  
    2.28  fun is_empty where
    2.29 -"is_empty(I (Some l) (Some h)) = (h<l)" |
    2.30 +"is_empty {l\<dots>h} = (h<l)" |
    2.31  "is_empty _ = False"
    2.32  
    2.33  lemma [simp]: "is_empty(I l h) =
    2.34 @@ -70,7 +79,7 @@
    2.35    else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
    2.36            I (min_option False l1 l2) (max_option True h1 h2))"
    2.37  
    2.38 -definition "\<top> = I None None"
    2.39 +definition "\<top> = {\<dots>}"
    2.40  
    2.41  instance
    2.42  proof
    2.43 @@ -221,12 +230,6 @@
    2.44   THEN ''y'' ::= Plus (V ''y'') (V ''x'')
    2.45   ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
    2.46  
    2.47 -translations
    2.48 -"{i..j}" <= "CONST I (CONST Some i) (CONST Some j)"
    2.49 -"{..j}" <= "CONST I (CONST None) (CONST Some j)"
    2.50 -"{i..}" <= "CONST I (CONST Some i) (CONST None)"
    2.51 -"CONST UNIV" <= "CONST I (CONST None) (CONST None)"
    2.52 -
    2.53  value [code] "show_acom (AI_ivl test1_ivl)"
    2.54  
    2.55  value [code] "show_acom (AI_const test3_const)"