hide Fin in output of value via postprocessor; no hinding needed elsewhere
authornipkow
Thu Jan 23 16:01:53 2014 +0100 (2014-01-23)
changeset 551250e0c09fca7bc
parent 55123 a389b50e6a42
child 55126 9f9db4e6fabc
hide Fin in output of value via postprocessor; no hinding needed elsewhere
src/HOL/IMP/Abs_Int2_ivl.thy
     1.1 --- a/src/HOL/IMP/Abs_Int2_ivl.thy	Thu Jan 23 14:26:16 2014 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Thu Jan 23 16:01:53 2014 +0100
     1.3 @@ -6,11 +6,9 @@
     1.4  
     1.5  subsection "Interval Analysis"
     1.6  
     1.7 -text{* Drop @{const Fin} around numerals on output: *}
     1.8 -translations
     1.9 -"_Numeral i" <= "CONST Fin(_Numeral i)"
    1.10 -"0" <= "CONST Fin 0"
    1.11 -"1" <= "CONST Fin 1"
    1.12 +text{* Drop @{const Fin} around numerals on output from value command: *}
    1.13 +declare Fin_numeral[code_post] Fin_neg_numeral[code_post]
    1.14 +  zero_extended_def[symmetric, code_post] one_extended_def[symmetric, code_post]
    1.15  
    1.16  type_synonym eint = "int extended"
    1.17  type_synonym eint2 = "eint * eint"
    1.18 @@ -291,8 +289,8 @@
    1.19  definition inv_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
    1.20  "inv_less_ivl res iv1 iv2 =
    1.21    (if res
    1.22 -   then (iv1 \<sqinter> (below iv2 - [Fin 1,Fin 1]),
    1.23 -         iv2 \<sqinter> (above iv1 + [Fin 1,Fin 1]))
    1.24 +   then (iv1 \<sqinter> (below iv2 - [1,1]),
    1.25 +         iv2 \<sqinter> (above iv1 + [1,1]))
    1.26     else (iv1 \<sqinter> above iv2, iv2 \<sqinter> below iv1))"
    1.27  
    1.28  lemma above_nice: "above[l,h] = (if [l,h] = \<bottom> then \<bottom> else [l,\<infinity>])"
    1.29 @@ -348,7 +346,7 @@
    1.30      by(simp add:  \<gamma>_uminus)
    1.31  next
    1.32    case goal3 thus ?case
    1.33 -    unfolding inv_less_ivl_def minus_ivl_def
    1.34 +    unfolding inv_less_ivl_def minus_ivl_def one_extended_def
    1.35      apply(clarsimp simp add: \<gamma>_inf split: if_splits)
    1.36      using gamma_plus'[of "i1+1" _ "-1"] gamma_plus'[of "i2 - 1" _ "1"]
    1.37      apply(simp add: \<gamma>_belowI[of i2] \<gamma>_aboveI[of i1]