got rid of Numeral.bin type
authorhaftmann
Wed Sep 06 13:48:02 2006 +0200 (2006-09-06)
changeset 204853078fd2eec7b
parent 20484 3d3d24186352
child 20486 02ca20e33030
got rid of Numeral.bin type
NEWS
src/HOL/Complex/Complex.thy
src/HOL/Complex/NSComplex.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Import/HOL/HOL4Prob.thy
src/HOL/Import/HOL/HOL4Real.thy
src/HOL/Import/HOL/HOL4Vec.thy
src/HOL/Import/HOL/HOL4Word32.thy
src/HOL/Integ/IntArith.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/IntDiv.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/NatSimprocs.thy
src/HOL/Integ/Numeral.thy
src/HOL/Integ/Presburger.thy
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/int_factor_simprocs.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/Integ/presburger.ML
src/HOL/Library/Word.thy
src/HOL/Library/word_setup.ML
src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
src/HOL/Matrix/cplex/MatrixLP.ML
src/HOL/Presburger.thy
src/HOL/Real/Float.ML
src/HOL/Real/Float.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
src/HOL/Real/ferrante_rackoff.ML
src/HOL/Tools/Presburger/presburger.ML
src/HOL/arith_data.ML
src/HOL/ex/Abstract_NAT.thy
src/HOL/hologic.ML
src/Pure/Tools/codegen_package.ML
     1.1 --- a/NEWS	Wed Sep 06 10:01:27 2006 +0200
     1.2 +++ b/NEWS	Wed Sep 06 13:48:02 2006 +0200
     1.3 @@ -465,6 +465,20 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Numeral syntax: type 'bin' which was a mere type copy of 'int' has been
     1.8 +abandoned in favour of plain 'int'. Significant changes for setting up numeral
     1.9 +syntax for types:
    1.10 +
    1.11 +  - new constants Numeral.pred and Numeral.succ instead
    1.12 +      of former Numeral.bin_pred and Numeral.bin_succ.
    1.13 +  - Use integer operations instead of bin_add, bin_mult and so on.
    1.14 +  - Numeral simplification theorems named Numeral.numeral_simps instead of Bin_simps.
    1.15 +  - ML structure Bin_Simprocs now named Int_Numeral_Base_Simprocs.
    1.16 +
    1.17 +See HOL/Integ/IntArith.thy for an example setup.
    1.18 +
    1.19 +INCOMPATIBILITY.
    1.20 +
    1.21  * New top level command 'normal_form' computes the normal form of a term
    1.22  that may contain free variables. For example 'normal_form "rev[a,b,c]"'
    1.23  prints '[b,c,a]'. This command is suitable for heavy-duty computations
     2.1 --- a/src/HOL/Complex/Complex.thy	Wed Sep 06 10:01:27 2006 +0200
     2.2 +++ b/src/HOL/Complex/Complex.thy	Wed Sep 06 13:48:02 2006 +0200
     2.3 @@ -830,7 +830,7 @@
     2.4  instance complex :: number ..
     2.5  
     2.6  defs (overloaded)
     2.7 -  complex_number_of_def: "(number_of w :: complex) == of_int (Rep_Bin w)"
     2.8 +  complex_number_of_def: "(number_of w :: complex) == of_int w"
     2.9      --{*the type constraint is essential!*}
    2.10  
    2.11  instance complex :: number_ring
     3.1 --- a/src/HOL/Complex/NSComplex.thy	Wed Sep 06 10:01:27 2006 +0200
     3.2 +++ b/src/HOL/Complex/NSComplex.thy	Wed Sep 06 13:48:02 2006 +0200
     3.3 @@ -783,7 +783,7 @@
     3.4  
     3.5  subsection{*Numerals and Arithmetic*}
     3.6  
     3.7 -lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int (Rep_Bin w)"
     3.8 +lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int w"
     3.9  by (transfer, rule number_of_eq [THEN eq_reflection])
    3.10  
    3.11  lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: 
     4.1 --- a/src/HOL/Hyperreal/NSA.thy	Wed Sep 06 10:01:27 2006 +0200
     4.2 +++ b/src/HOL/Hyperreal/NSA.thy	Wed Sep 06 13:48:02 2006 +0200
     4.3 @@ -547,7 +547,7 @@
     4.4  
     4.5  in
     4.6  val approx_reorient_simproc =
     4.7 -  Bin_Simprocs.prep_simproc
     4.8 +  Int_Numeral_Base_Simprocs.prep_simproc
     4.9      ("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc);
    4.10  end;
    4.11  
     5.1 --- a/src/HOL/Import/HOL/HOL4Prob.thy	Wed Sep 06 10:01:27 2006 +0200
     5.2 +++ b/src/HOL/Import/HOL/HOL4Prob.thy	Wed Sep 06 13:48:02 2006 +0200
     5.3 @@ -35,28 +35,28 @@
     5.4  lemma DIV_TWO_BASIC: "(op &::bool => bool => bool)
     5.5   ((op =::nat => nat => bool)
     5.6     ((op div::nat => nat => nat) (0::nat)
     5.7 -     ((number_of::bin => nat)
     5.8 -       ((op BIT::bin => bit => bin)
     5.9 -         ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    5.10 +     ((number_of \<Colon> int => nat)
    5.11 +       ((op BIT \<Colon> int => bit => int)
    5.12 +         ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
    5.13           (bit.B0::bit))))
    5.14     (0::nat))
    5.15   ((op &::bool => bool => bool)
    5.16     ((op =::nat => nat => bool)
    5.17       ((op div::nat => nat => nat) (1::nat)
    5.18 -       ((number_of::bin => nat)
    5.19 -         ((op BIT::bin => bit => bin)
    5.20 -           ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    5.21 +       ((number_of \<Colon> int => nat)
    5.22 +         ((op BIT \<Colon> int => bit => int)
    5.23 +           ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
    5.24             (bit.B0::bit))))
    5.25       (0::nat))
    5.26     ((op =::nat => nat => bool)
    5.27       ((op div::nat => nat => nat)
    5.28 -       ((number_of::bin => nat)
    5.29 -         ((op BIT::bin => bit => bin)
    5.30 -           ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    5.31 +       ((number_of \<Colon> int => nat)
    5.32 +         ((op BIT \<Colon> int => bit => int)
    5.33 +           ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
    5.34             (bit.B0::bit)))
    5.35 -       ((number_of::bin => nat)
    5.36 -         ((op BIT::bin => bit => bin)
    5.37 -           ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    5.38 +       ((number_of \<Colon> int => nat)
    5.39 +         ((op BIT \<Colon> int => bit => int)
    5.40 +           ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
    5.41             (bit.B0::bit))))
    5.42       (1::nat)))"
    5.43    by (import prob_extra DIV_TWO_BASIC)
    5.44 @@ -75,19 +75,19 @@
    5.45       (op =::nat => nat => bool)
    5.46        ((op div::nat => nat => nat)
    5.47          ((op ^::nat => nat => nat)
    5.48 -          ((number_of::bin => nat)
    5.49 -            ((op BIT::bin => bit => bin)
    5.50 -              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    5.51 +          ((number_of \<Colon> int => nat)
    5.52 +            ((op BIT \<Colon> int => bit => int)
    5.53 +              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
    5.54                (bit.B0::bit)))
    5.55            ((Suc::nat => nat) n))
    5.56 -        ((number_of::bin => nat)
    5.57 -          ((op BIT::bin => bit => bin)
    5.58 -            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    5.59 +        ((number_of \<Colon> int => nat)
    5.60 +          ((op BIT \<Colon> int => bit => int)
    5.61 +            ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
    5.62              (bit.B0::bit))))
    5.63        ((op ^::nat => nat => nat)
    5.64 -        ((number_of::bin => nat)
    5.65 -          ((op BIT::bin => bit => bin)
    5.66 -            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    5.67 +        ((number_of \<Colon> int => nat)
    5.68 +          ((op BIT \<Colon> int => bit => int)
    5.69 +            ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
    5.70              (bit.B0::bit)))
    5.71          n))"
    5.72    by (import prob_extra EXP_DIV_TWO)
    5.73 @@ -125,22 +125,22 @@
    5.74  
    5.75  lemma HALF_POS: "(op <::real => real => bool) (0::real)
    5.76   ((op /::real => real => real) (1::real)
    5.77 -   ((number_of::bin => real)
    5.78 -     ((op BIT::bin => bit => bin)
    5.79 -       ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    5.80 +   ((number_of \<Colon> int => real)
    5.81 +     ((op BIT \<Colon> int => bit => int)
    5.82 +       ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
    5.83         (bit.B0::bit))))"
    5.84    by (import prob_extra HALF_POS)
    5.85  
    5.86  lemma HALF_CANCEL: "(op =::real => real => bool)
    5.87   ((op *::real => real => real)
    5.88 -   ((number_of::bin => real)
    5.89 -     ((op BIT::bin => bit => bin)
    5.90 -       ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    5.91 +   ((number_of \<Colon> int => real)
    5.92 +     ((op BIT \<Colon> int => bit => int)
    5.93 +       ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
    5.94         (bit.B0::bit)))
    5.95     ((op /::real => real => real) (1::real)
    5.96 -     ((number_of::bin => real)
    5.97 -       ((op BIT::bin => bit => bin)
    5.98 -         ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    5.99 +     ((number_of \<Colon> int => real)
   5.100 +       ((op BIT \<Colon> int => bit => int)
   5.101 +         ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
   5.102           (bit.B0::bit)))))
   5.103   (1::real)"
   5.104    by (import prob_extra HALF_CANCEL)
   5.105 @@ -150,9 +150,9 @@
   5.106       (op <::real => real => bool) (0::real)
   5.107        ((op ^::real => nat => real)
   5.108          ((op /::real => real => real) (1::real)
   5.109 -          ((number_of::bin => real)
   5.110 -            ((op BIT::bin => bit => bin)
   5.111 -              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   5.112 +          ((number_of \<Colon> int => real)
   5.113 +            ((op BIT \<Colon> int => bit => int)
   5.114 +              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
   5.115                (bit.B0::bit))))
   5.116          n))"
   5.117    by (import prob_extra POW_HALF_POS)
   5.118 @@ -165,17 +165,17 @@
   5.119             ((op <=::real => real => bool)
   5.120               ((op ^::real => nat => real)
   5.121                 ((op /::real => real => real) (1::real)
   5.122 -                 ((number_of::bin => real)
   5.123 -                   ((op BIT::bin => bit => bin)
   5.124 -                     ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   5.125 +                 ((number_of \<Colon> int => real)
   5.126 +                   ((op BIT \<Colon> int => bit => int)
   5.127 +                     ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
   5.128                         (bit.B1::bit))
   5.129                       (bit.B0::bit))))
   5.130                 n)
   5.131               ((op ^::real => nat => real)
   5.132                 ((op /::real => real => real) (1::real)
   5.133 -                 ((number_of::bin => real)
   5.134 -                   ((op BIT::bin => bit => bin)
   5.135 -                     ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   5.136 +                 ((number_of \<Colon> int => real)
   5.137 +                   ((op BIT \<Colon> int => bit => int)
   5.138 +                     ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
   5.139                         (bit.B1::bit))
   5.140                       (bit.B0::bit))))
   5.141                 m))))"
   5.142 @@ -186,21 +186,21 @@
   5.143       (op =::real => real => bool)
   5.144        ((op ^::real => nat => real)
   5.145          ((op /::real => real => real) (1::real)
   5.146 -          ((number_of::bin => real)
   5.147 -            ((op BIT::bin => bit => bin)
   5.148 -              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   5.149 +          ((number_of \<Colon> int => real)
   5.150 +            ((op BIT \<Colon> int => bit => int)
   5.151 +              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
   5.152                (bit.B0::bit))))
   5.153          n)
   5.154        ((op *::real => real => real)
   5.155 -        ((number_of::bin => real)
   5.156 -          ((op BIT::bin => bit => bin)
   5.157 -            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   5.158 +        ((number_of \<Colon> int => real)
   5.159 +          ((op BIT \<Colon> int => bit => int)
   5.160 +            ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
   5.161              (bit.B0::bit)))
   5.162          ((op ^::real => nat => real)
   5.163            ((op /::real => real => real) (1::real)
   5.164 -            ((number_of::bin => real)
   5.165 -              ((op BIT::bin => bit => bin)
   5.166 -                ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   5.167 +            ((number_of \<Colon> int => real)
   5.168 +              ((op BIT \<Colon> int => bit => int)
   5.169 +                ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
   5.170                    (bit.B1::bit))
   5.171                  (bit.B0::bit))))
   5.172            ((Suc::nat => nat) n))))"
   5.173 @@ -227,22 +227,22 @@
   5.174  lemma ONE_MINUS_HALF: "(op =::real => real => bool)
   5.175   ((op -::real => real => real) (1::real)
   5.176     ((op /::real => real => real) (1::real)
   5.177 -     ((number_of::bin => real)
   5.178 -       ((op BIT::bin => bit => bin)
   5.179 -         ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   5.180 +     ((number_of \<Colon> int => real)
   5.181 +       ((op BIT \<Colon> int => bit => int)
   5.182 +         ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
   5.183           (bit.B0::bit)))))
   5.184   ((op /::real => real => real) (1::real)
   5.185 -   ((number_of::bin => real)
   5.186 -     ((op BIT::bin => bit => bin)
   5.187 -       ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   5.188 +   ((number_of \<Colon> int => real)
   5.189 +     ((op BIT \<Colon> int => bit => int)
   5.190 +       ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
   5.191         (bit.B0::bit))))"
   5.192    by (import prob_extra ONE_MINUS_HALF)
   5.193  
   5.194  lemma HALF_LT_1: "(op <::real => real => bool)
   5.195   ((op /::real => real => real) (1::real)
   5.196 -   ((number_of::bin => real)
   5.197 -     ((op BIT::bin => bit => bin)
   5.198 -       ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   5.199 +   ((number_of \<Colon> int => real)
   5.200 +     ((op BIT \<Colon> int => bit => int)
   5.201 +       ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
   5.202         (bit.B0::bit))))
   5.203   (1::real)"
   5.204    by (import prob_extra HALF_LT_1)
   5.205 @@ -252,17 +252,17 @@
   5.206       (op =::real => real => bool)
   5.207        ((op ^::real => nat => real)
   5.208          ((op /::real => real => real) (1::real)
   5.209 -          ((number_of::bin => real)
   5.210 -            ((op BIT::bin => bit => bin)
   5.211 -              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   5.212 +          ((number_of \<Colon> int => real)
   5.213 +            ((op BIT \<Colon> int => bit => int)
   5.214 +              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
   5.215                (bit.B0::bit))))
   5.216          n)
   5.217        ((inverse::real => real)
   5.218          ((real::nat => real)
   5.219            ((op ^::nat => nat => nat)
   5.220 -            ((number_of::bin => nat)
   5.221 -              ((op BIT::bin => bit => bin)
   5.222 -                ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   5.223 +            ((number_of \<Colon> int => nat)
   5.224 +              ((op BIT \<Colon> int => bit => int)
   5.225 +                ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
   5.226                    (bit.B1::bit))
   5.227                  (bit.B0::bit)))
   5.228              n))))"
   5.229 @@ -1405,27 +1405,27 @@
   5.230        ((op +::real => real => real)
   5.231          ((op ^::real => nat => real)
   5.232            ((op /::real => real => real) (1::real)
   5.233 -            ((number_of::bin => real)
   5.234 -              ((op BIT::bin => bit => bin)
   5.235 -                ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   5.236 +            ((number_of \<Colon> int => real)
   5.237 +              ((op BIT \<Colon> int => bit => int)
   5.238 +                ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
   5.239                    (bit.B1::bit))
   5.240                  (bit.B0::bit))))
   5.241            ((size::bool list => nat)
   5.242              ((SNOC::bool => bool list => bool list) (True::bool) l)))
   5.243          ((op ^::real => nat => real)
   5.244            ((op /::real => real => real) (1::real)
   5.245 -            ((number_of::bin => real)
   5.246 -              ((op BIT::bin => bit => bin)
   5.247 -                ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   5.248 +            ((number_of \<Colon> int => real)
   5.249 +              ((op BIT \<Colon> int => bit => int)
   5.250 +                ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
   5.251                    (bit.B1::bit))
   5.252                  (bit.B0::bit))))
   5.253            ((size::bool list => nat)
   5.254              ((SNOC::bool => bool list => bool list) (False::bool) l))))
   5.255        ((op ^::real => nat => real)
   5.256          ((op /::real => real => real) (1::real)
   5.257 -          ((number_of::bin => real)
   5.258 -            ((op BIT::bin => bit => bin)
   5.259 -              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
   5.260 +          ((number_of \<Colon> int => real)
   5.261 +            ((op BIT \<Colon> int => bit => int)
   5.262 +              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
   5.263                (bit.B0::bit))))
   5.264          ((size::bool list => nat) l)))"
   5.265    by (import prob ALG_TWINS_MEASURE)
     6.1 --- a/src/HOL/Import/HOL/HOL4Real.thy	Wed Sep 06 10:01:27 2006 +0200
     6.2 +++ b/src/HOL/Import/HOL/HOL4Real.thy	Wed Sep 06 13:48:02 2006 +0200
     6.3 @@ -525,9 +525,9 @@
     6.4        ((op <=::real => real => bool) (1::real) x)
     6.5        ((op <=::real => real => bool) (1::real)
     6.6          ((op ^::real => nat => real) x
     6.7 -          ((number_of::bin => nat)
     6.8 -            ((op BIT::bin => bit => bin)
     6.9 -              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    6.10 +          ((number_of \<Colon> int => nat)
    6.11 +            ((op BIT \<Colon> int => bit => int)
    6.12 +              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
    6.13                (bit.B0::bit))))))"
    6.14    by (import real REAL_LE1_POW2)
    6.15  
    6.16 @@ -537,9 +537,9 @@
    6.17        ((op <::real => real => bool) (1::real) x)
    6.18        ((op <::real => real => bool) (1::real)
    6.19          ((op ^::real => nat => real) x
    6.20 -          ((number_of::bin => nat)
    6.21 -            ((op BIT::bin => bit => bin)
    6.22 -              ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    6.23 +          ((number_of \<Colon> int => nat)
    6.24 +            ((op BIT \<Colon> int => bit => int)
    6.25 +              ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
    6.26                (bit.B0::bit))))))"
    6.27    by (import real REAL_LT1_POW2)
    6.28  
     7.1 --- a/src/HOL/Import/HOL/HOL4Vec.thy	Wed Sep 06 10:01:27 2006 +0200
     7.2 +++ b/src/HOL/Import/HOL/HOL4Vec.thy	Wed Sep 06 13:48:02 2006 +0200
     7.3 @@ -1282,9 +1282,9 @@
     7.4   (%x::nat.
     7.5       (op -->::bool => bool => bool)
     7.6        ((op <::nat => nat => bool) x
     7.7 -        ((number_of::bin => nat)
     7.8 -          ((op BIT::bin => bit => bin)
     7.9 -            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    7.10 +        ((number_of \<Colon> int => nat)
    7.11 +          ((op BIT \<Colon> int => bit => int)
    7.12 +            ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
    7.13              (bit.B0::bit))))
    7.14        ((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
    7.15          x))"
    7.16 @@ -1499,10 +1499,10 @@
    7.17                                   k (0::nat) w2)))
    7.18                             ((BV::bool => nat) cin))
    7.19                           ((op ^::nat => nat => nat)
    7.20 -                           ((number_of::bin => nat)
    7.21 -                             ((op BIT::bin => bit => bin)
    7.22 -                               ((op BIT::bin => bit => bin)
    7.23 -                                 (Numeral.Pls::bin) (bit.B1::bit))
    7.24 +                           ((number_of \<Colon> int => nat)
    7.25 +                             ((op BIT \<Colon> int => bit => int)
    7.26 +                               ((op BIT \<Colon> int => bit => int)
    7.27 +                                 (Numeral.Pls \<Colon> int) (bit.B1::bit))
    7.28                                 (bit.B0::bit)))
    7.29                             k)))))))"
    7.30    by (import bword_arith ACARRY_EQ_ADD_DIV)
     8.1 --- a/src/HOL/Import/HOL/HOL4Word32.thy	Wed Sep 06 10:01:27 2006 +0200
     8.2 +++ b/src/HOL/Import/HOL/HOL4Word32.thy	Wed Sep 06 13:48:02 2006 +0200
     8.3 @@ -116,9 +116,9 @@
     8.4   (%n::nat.
     8.5       (op <::nat => nat => bool) (0::nat)
     8.6        ((op ^::nat => nat => nat)
     8.7 -        ((number_of::bin => nat)
     8.8 -          ((op BIT::bin => bit => bin)
     8.9 -            ((op BIT::bin => bit => bin) (Numeral.Pls::bin) (bit.B1::bit))
    8.10 +        ((number_of \<Colon> int => nat)
    8.11 +          ((op BIT \<Colon> int => bit => int)
    8.12 +            ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int) (bit.B1::bit))
    8.13              (bit.B0::bit)))
    8.14          n))"
    8.15    by (import bits ZERO_LT_TWOEXP)
    8.16 @@ -136,16 +136,16 @@
    8.17            (op -->::bool => bool => bool) ((op <::nat => nat => bool) a b)
    8.18             ((op <::nat => nat => bool)
    8.19               ((op ^::nat => nat => nat)
    8.20 -               ((number_of::bin => nat)
    8.21 -                 ((op BIT::bin => bit => bin)
    8.22 -                   ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
    8.23 +               ((number_of \<Colon> int => nat)
    8.24 +                 ((op BIT \<Colon> int => bit => int)
    8.25 +                   ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
    8.26                       (bit.B1::bit))
    8.27                     (bit.B0::bit)))
    8.28                 a)
    8.29               ((op ^::nat => nat => nat)
    8.30 -               ((number_of::bin => nat)
    8.31 -                 ((op BIT::bin => bit => bin)
    8.32 -                   ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
    8.33 +               ((number_of \<Colon> int => nat)
    8.34 +                 ((op BIT \<Colon> int => bit => int)
    8.35 +                   ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
    8.36                       (bit.B1::bit))
    8.37                     (bit.B0::bit)))
    8.38                 b))))"
    8.39 @@ -158,16 +158,16 @@
    8.40            (op -->::bool => bool => bool) ((op <=::nat => nat => bool) a b)
    8.41             ((op <=::nat => nat => bool)
    8.42               ((op ^::nat => nat => nat)
    8.43 -               ((number_of::bin => nat)
    8.44 -                 ((op BIT::bin => bit => bin)
    8.45 -                   ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
    8.46 +               ((number_of \<Colon> int => nat)
    8.47 +                 ((op BIT \<Colon> int => bit => int)
    8.48 +                   ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
    8.49                       (bit.B1::bit))
    8.50                     (bit.B0::bit)))
    8.51                 a)
    8.52               ((op ^::nat => nat => nat)
    8.53 -               ((number_of::bin => nat)
    8.54 -                 ((op BIT::bin => bit => bin)
    8.55 -                   ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
    8.56 +               ((number_of \<Colon> int => nat)
    8.57 +                 ((op BIT \<Colon> int => bit => int)
    8.58 +                   ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
    8.59                       (bit.B1::bit))
    8.60                     (bit.B0::bit)))
    8.61                 b))))"
    8.62 @@ -179,16 +179,16 @@
    8.63        (%b::nat.
    8.64            (op <=::nat => nat => bool)
    8.65             ((op ^::nat => nat => nat)
    8.66 -             ((number_of::bin => nat)
    8.67 -               ((op BIT::bin => bit => bin)
    8.68 -                 ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
    8.69 +             ((number_of \<Colon> int => nat)
    8.70 +               ((op BIT \<Colon> int => bit => int)
    8.71 +                 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
    8.72                     (bit.B1::bit))
    8.73                   (bit.B0::bit)))
    8.74               ((op -::nat => nat => nat) a b))
    8.75             ((op ^::nat => nat => nat)
    8.76 -             ((number_of::bin => nat)
    8.77 -               ((op BIT::bin => bit => bin)
    8.78 -                 ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
    8.79 +             ((number_of \<Colon> int => nat)
    8.80 +               ((op BIT \<Colon> int => bit => int)
    8.81 +                 ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
    8.82                     (bit.B1::bit))
    8.83                   (bit.B0::bit)))
    8.84               a)))"
    8.85 @@ -348,24 +348,24 @@
    8.86               (%x::nat.
    8.87                   (op =::nat => nat => bool)
    8.88                    ((op ^::nat => nat => nat)
    8.89 -                    ((number_of::bin => nat)
    8.90 -                      ((op BIT::bin => bit => bin)
    8.91 -                        ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
    8.92 +                    ((number_of \<Colon> int => nat)
    8.93 +                      ((op BIT \<Colon> int => bit => int)
    8.94 +                        ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
    8.95                            (bit.B1::bit))
    8.96                          (bit.B0::bit)))
    8.97                      b)
    8.98                    ((op *::nat => nat => nat)
    8.99                      ((op ^::nat => nat => nat)
   8.100 -                      ((number_of::bin => nat)
   8.101 -                        ((op BIT::bin => bit => bin)
   8.102 -                          ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   8.103 +                      ((number_of \<Colon> int => nat)
   8.104 +                        ((op BIT \<Colon> int => bit => int)
   8.105 +                          ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
   8.106                              (bit.B1::bit))
   8.107                            (bit.B0::bit)))
   8.108                        ((op +::nat => nat => nat) x (1::nat)))
   8.109                      ((op ^::nat => nat => nat)
   8.110 -                      ((number_of::bin => nat)
   8.111 -                        ((op BIT::bin => bit => bin)
   8.112 -                          ((op BIT::bin => bit => bin) (Numeral.Pls::bin)
   8.113 +                      ((number_of \<Colon> int => nat)
   8.114 +                        ((op BIT \<Colon> int => bit => int)
   8.115 +                          ((op BIT \<Colon> int => bit => int) (Numeral.Pls \<Colon> int)
   8.116                              (bit.B1::bit))
   8.117                            (bit.B0::bit)))
   8.118                        a))))))"
     9.1 --- a/src/HOL/Integ/IntArith.thy	Wed Sep 06 10:01:27 2006 +0200
     9.2 +++ b/src/HOL/Integ/IntArith.thy	Wed Sep 06 13:48:02 2006 +0200
     9.3 @@ -20,7 +20,7 @@
     9.4    int :: number ..
     9.5  
     9.6  defs (overloaded)
     9.7 -  int_number_of_def: "(number_of w :: int) == of_int (Rep_Bin w)"
     9.8 +  int_number_of_def: "(number_of w :: int) == of_int w"
     9.9      --{*the type constraint is essential!*}
    9.10  
    9.11  instance int :: number_ring
    9.12 @@ -365,12 +365,9 @@
    9.13  subsection {* code generator setup *}
    9.14  
    9.15  code_typename
    9.16 -  "Numeral.bin" "IntDef.bin"
    9.17    "Numeral.bit" "IntDef.bit"
    9.18  
    9.19  code_constname
    9.20 -  "Numeral.Abs_Bin" "IntDef.bin"
    9.21 -  "Numeral.Rep_Bin" "IntDef.int_of_bin"
    9.22    "Numeral.Pls" "IntDef.pls"
    9.23    "Numeral.Min" "IntDef.min"
    9.24    "Numeral.Bit" "IntDef.bit"
    9.25 @@ -387,36 +384,29 @@
    9.26  lemma
    9.27    Numeral_Bit_refl [code fun]: "Numeral.Bit = Numeral.Bit" ..
    9.28  
    9.29 -lemma
    9.30 -  number_of_is_rep_bin [code inline]: "number_of = Rep_Bin"
    9.31 -proof
    9.32 -  fix b
    9.33 -  show "number_of b = Rep_Bin b" 
    9.34 -  unfolding int_number_of_def by simp
    9.35 -qed
    9.36 +lemma zero_is_num_zero [code fun, code inline]:
    9.37 +  "(0::int) = Numeral.Pls" 
    9.38 +  unfolding Pls_def ..
    9.39  
    9.40 -lemma zero_is_num_zero [code, code inline]:
    9.41 -  "(0::int) = Rep_Bin Numeral.Pls" 
    9.42 -  unfolding Pls_def Abs_Bin_inverse' ..
    9.43 +lemma one_is_num_one [code fun, code inline]:
    9.44 +  "(1::int) = Numeral.Pls BIT bit.B1" 
    9.45 +  unfolding Pls_def Bit_def by simp 
    9.46  
    9.47 -lemma one_is_num_one [code, code inline]:
    9.48 -  "(1::int) = Rep_Bin (Numeral.Pls BIT bit.B1)" 
    9.49 -  unfolding Pls_def Bit_def Abs_Bin_inverse' by simp 
    9.50 +lemma number_of_is_id [code fun, code inline]:
    9.51 +  "number_of (k::int) = k"
    9.52 +  unfolding int_number_of_def by simp
    9.53  
    9.54 -lemma negate_bin_minus:
    9.55 -  "(Rep_Bin b :: int) = - Rep_Bin (bin_minus b)"
    9.56 -  unfolding bin_minus_def Abs_Bin_inverse' by simp
    9.57 -
    9.58 -lemmas [code inline] =
    9.59 -  bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
    9.60 -  bin_pred_Pls  bin_pred_Min  bin_pred_1  bin_pred_0
    9.61 +lemma number_of_minus:
    9.62 +  "number_of (b :: int) = (- number_of (- b) :: int)"
    9.63 +  unfolding int_number_of_def by simp
    9.64  
    9.65  ML {*
    9.66  structure Numeral =
    9.67  struct
    9.68  
    9.69 -val negate_bin_minus_thm = eq_reflection OF [thm "negate_bin_minus"];
    9.70 -val number_of_is_rep_bin_thm = eq_reflection OF [thm "number_of_is_rep_bin"];
    9.71 +val number_of_minus_thm = eq_reflection OF [thm "number_of_minus"];
    9.72 +val minus_rewrites = map (fn thm => eq_reflection OF [thm])
    9.73 +  [minus_1, minus_0, minus_Pls, minus_Min, pred_1, pred_0, pred_Pls, pred_Min];
    9.74  
    9.75  fun int_of_numeral thy num = HOLogic.dest_binum num
    9.76    handle TERM _
    9.77 @@ -424,7 +414,6 @@
    9.78  
    9.79  fun elim_negate thy thms =
    9.80    let
    9.81 -    val thms' = map (CodegenTheorems.rewrite_fun [number_of_is_rep_bin_thm]) thms;
    9.82      fun bins_of (Const _) =
    9.83            I
    9.84        | bins_of (Var _) =
    9.85 @@ -437,28 +426,32 @@
    9.86            bins_of t
    9.87        | bins_of (t as _ $ _) =
    9.88            case strip_comb t
    9.89 -           of (Const ("Numeral.Rep_Bin", _), [bin]) => cons bin
    9.90 +           of (Const ("Numeral.Bit", _), _) => cons t
    9.91              | (t', ts) => bins_of t' #> fold bins_of ts;
    9.92 -    fun is_negative bin = case try HOLogic.dest_binum bin
    9.93 +    fun is_negative num = case try HOLogic.dest_binum num
    9.94       of SOME i => i < 0
    9.95        | _ => false;
    9.96      fun instantiate_with bin =
    9.97 -      Drule.instantiate' [] [(SOME o cterm_of thy) bin] negate_bin_minus_thm;
    9.98 +      Drule.instantiate' [] [(SOME o cterm_of thy) bin] number_of_minus_thm;
    9.99      val rewrites  =
   9.100        []
   9.101 -      |> fold (bins_of o prop_of) thms'
   9.102 +      |> fold (bins_of o prop_of) thms
   9.103        |> filter is_negative
   9.104        |> map instantiate_with
   9.105 -  in if null rewrites then thms' else
   9.106 -    map (CodegenTheorems.rewrite_fun rewrites) thms'
   9.107 +  in if null rewrites then thms else
   9.108 +    map (CodegenTheorems.rewrite_fun (rewrites @ minus_rewrites)) thms
   9.109    end;
   9.110  
   9.111  end;
   9.112  *}
   9.113  
   9.114 +code_const "Numeral.Pls" and "Numeral.Min"
   9.115 +  (SML target_atom "(0 : IntInf.int)" and target_atom "(~1 : IntInf.int)")
   9.116 +  (Haskell target_atom "0" and target_atom "(negate ~1)")
   9.117 +
   9.118  setup {*
   9.119    CodegenTheorems.add_preproc Numeral.elim_negate
   9.120 -  #> CodegenPackage.add_appconst ("Numeral.Rep_Bin", CodegenPackage.appgen_rep_bin Numeral.int_of_numeral)
   9.121 +  #> CodegenPackage.add_appconst ("Numeral.Bit", CodegenPackage.appgen_rep_bin Numeral.int_of_numeral)
   9.122  *}
   9.123  
   9.124  
    10.1 --- a/src/HOL/Integ/IntDef.thy	Wed Sep 06 10:01:27 2006 +0200
    10.2 +++ b/src/HOL/Integ/IntDef.thy	Wed Sep 06 13:48:02 2006 +0200
    10.3 @@ -935,7 +935,7 @@
    10.4        Type ("fun", [_, Type ("nat", [])])) $ bin) =
    10.5          SOME (Codegen.invoke_codegen thy defs s thyname b (gr,
    10.6            Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
    10.7 -            (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin)))
    10.8 +            (Const ("Numeral.number_of", HOLogic.intT --> HOLogic.intT) $ bin)))
    10.9    | number_of_codegen _ _ _ _ _ _ _ = NONE;
   10.10  *}
   10.11  
    11.1 --- a/src/HOL/Integ/IntDiv.thy	Wed Sep 06 10:01:27 2006 +0200
    11.2 +++ b/src/HOL/Integ/IntDiv.thy	Wed Sep 06 13:48:02 2006 +0200
    11.3 @@ -9,7 +9,7 @@
    11.4  header{*The Division Operators div and mod; the Divides Relation dvd*}
    11.5  
    11.6  theory IntDiv
    11.7 -imports SetInterval Recdef
    11.8 +imports "../SetInterval" "../Recdef"
    11.9  uses ("IntDiv_setup.ML")
   11.10  begin
   11.11  
   11.12 @@ -959,7 +959,7 @@
   11.13            (if b=bit.B0 | (0::int) \<le> number_of w                    
   11.14             then number_of v div (number_of w)     
   11.15             else (number_of v + (1::int)) div (number_of w))"
   11.16 -apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if) 
   11.17 +apply (simp only: number_of_eq numeral_simps UNIV_I split: split_if) 
   11.18  apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac 
   11.19              split: bit.split)
   11.20  done
   11.21 @@ -1001,7 +1001,7 @@
   11.22          | bit.B1 => if (0::int) \<le> number_of w  
   11.23                  then 2 * (number_of v mod number_of w) + 1     
   11.24                  else 2 * ((number_of v + (1::int)) mod number_of w) - 1)"
   11.25 -apply (simp only: number_of_eq Bin_simps UNIV_I split: bit.split) 
   11.26 +apply (simp only: number_of_eq numeral_simps UNIV_I split: bit.split) 
   11.27  apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
   11.28                   not_0_le_lemma neg_zmod_mult_2 add_ac)
   11.29  done
    12.1 --- a/src/HOL/Integ/NatBin.thy	Wed Sep 06 10:01:27 2006 +0200
    12.2 +++ b/src/HOL/Integ/NatBin.thy	Wed Sep 06 13:48:02 2006 +0200
    12.3 @@ -17,8 +17,7 @@
    12.4  instance nat :: number ..
    12.5  
    12.6  defs (overloaded)
    12.7 -  nat_number_of_def:
    12.8 -  "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
    12.9 +  nat_number_of_def: "number_of v == nat (number_of (v\<Colon>int))"
   12.10  
   12.11  abbreviation (xsymbols)
   12.12    square :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999)
   12.13 @@ -113,14 +112,14 @@
   12.14  
   12.15  lemma Suc_nat_number_of_add:
   12.16       "Suc (number_of v + n) =  
   12.17 -        (if neg (number_of v :: int) then 1+n else number_of (bin_succ v) + n)" 
   12.18 +        (if neg (number_of v :: int) then 1+n else number_of (succ v) + n)" 
   12.19  by (simp del: nat_number_of 
   12.20           add: nat_number_of_def neg_nat
   12.21                Suc_nat_eq_nat_zadd1 number_of_succ) 
   12.22  
   12.23  lemma Suc_nat_number_of [simp]:
   12.24       "Suc (number_of v) =  
   12.25 -        (if neg (number_of v :: int) then 1 else number_of (bin_succ v))"
   12.26 +        (if neg (number_of v :: int) then 1 else number_of (succ v))"
   12.27  apply (cut_tac n = 0 in Suc_nat_number_of_add)
   12.28  apply (simp cong del: if_weak_cong)
   12.29  done
   12.30 @@ -133,7 +132,7 @@
   12.31       "(number_of v :: nat) + number_of v' =  
   12.32           (if neg (number_of v :: int) then number_of v'  
   12.33            else if neg (number_of v' :: int) then number_of v  
   12.34 -          else number_of (bin_add v v'))"
   12.35 +          else number_of (v + v'))"
   12.36  by (force dest!: neg_nat
   12.37            simp del: nat_number_of
   12.38            simp add: nat_number_of_def nat_add_distrib [symmetric]) 
   12.39 @@ -152,7 +151,7 @@
   12.40  lemma diff_nat_number_of [simp]: 
   12.41       "(number_of v :: nat) - number_of v' =  
   12.42          (if neg (number_of v' :: int) then number_of v  
   12.43 -         else let d = number_of (bin_add v (bin_minus v')) in     
   12.44 +         else let d = number_of (v + uminus v') in     
   12.45                if neg d then 0 else nat d)"
   12.46  by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def) 
   12.47  
   12.48 @@ -162,7 +161,7 @@
   12.49  
   12.50  lemma mult_nat_number_of [simp]:
   12.51       "(number_of v :: nat) * number_of v' =  
   12.52 -       (if neg (number_of v :: int) then 0 else number_of (bin_mult v v'))"
   12.53 +       (if neg (number_of v :: int) then 0 else number_of (v * v'))"
   12.54  by (force dest!: neg_nat
   12.55            simp del: nat_number_of
   12.56            simp add: nat_number_of_def nat_mult_distrib [symmetric]) 
   12.57 @@ -246,7 +245,7 @@
   12.58       "((number_of v :: nat) = number_of v') =  
   12.59        (if neg (number_of v :: int) then (iszero (number_of v' :: int) | neg (number_of v' :: int))  
   12.60         else if neg (number_of v' :: int) then iszero (number_of v :: int)  
   12.61 -       else iszero (number_of (bin_add v (bin_minus v')) :: int))"
   12.62 +       else iszero (number_of (v + uminus v') :: int))"
   12.63  apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
   12.64                    eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def
   12.65              split add: split_if cong add: imp_cong)
   12.66 @@ -260,13 +259,11 @@
   12.67  (*"neg" is used in rewrite rules for binary comparisons*)
   12.68  lemma less_nat_number_of [simp]:
   12.69       "((number_of v :: nat) < number_of v') =  
   12.70 -         (if neg (number_of v :: int) then neg (number_of (bin_minus v') :: int)  
   12.71 -          else neg (number_of (bin_add v (bin_minus v')) :: int))"
   12.72 +         (if neg (number_of v :: int) then neg (number_of (uminus v') :: int)  
   12.73 +          else neg (number_of (v + uminus v') :: int))"
   12.74  by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
   12.75                  nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
   12.76 -         cong add: imp_cong, simp) 
   12.77 -
   12.78 -
   12.79 +         cong add: imp_cong, simp add: Pls_def)
   12.80  
   12.81  
   12.82  (*Maps #n to n for n = 0, 1, 2*)
   12.83 @@ -437,8 +434,8 @@
   12.84  by (rule trans [OF eq_sym_conv eq_number_of_0])
   12.85  
   12.86  lemma less_0_number_of [simp]:
   12.87 -     "((0::nat) < number_of v) = neg (number_of (bin_minus v) :: int)"
   12.88 -by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric])
   12.89 +     "((0::nat) < number_of v) = neg (number_of (uminus v) :: int)"
   12.90 +by (simp del: nat_numeral_0_eq_0 add: nat_numeral_0_eq_0 [symmetric] Pls_def)
   12.91  
   12.92  
   12.93  lemma neg_imp_number_of_eq_0: "neg (number_of v :: int) ==> number_of v = (0::nat)"
   12.94 @@ -450,7 +447,7 @@
   12.95  
   12.96  lemma eq_number_of_Suc [simp]:
   12.97       "(number_of v = Suc n) =  
   12.98 -        (let pv = number_of (bin_pred v) in  
   12.99 +        (let pv = number_of (pred v) in  
  12.100           if neg pv then False else nat pv = n)"
  12.101  apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
  12.102                    number_of_pred nat_number_of_def 
  12.103 @@ -461,13 +458,13 @@
  12.104  
  12.105  lemma Suc_eq_number_of [simp]:
  12.106       "(Suc n = number_of v) =  
  12.107 -        (let pv = number_of (bin_pred v) in  
  12.108 +        (let pv = number_of (pred v) in  
  12.109           if neg pv then False else nat pv = n)"
  12.110  by (rule trans [OF eq_sym_conv eq_number_of_Suc])
  12.111  
  12.112  lemma less_number_of_Suc [simp]:
  12.113       "(number_of v < Suc n) =  
  12.114 -        (let pv = number_of (bin_pred v) in  
  12.115 +        (let pv = number_of (pred v) in  
  12.116           if neg pv then True else nat pv < n)"
  12.117  apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
  12.118                    number_of_pred nat_number_of_def  
  12.119 @@ -478,7 +475,7 @@
  12.120  
  12.121  lemma less_Suc_number_of [simp]:
  12.122       "(Suc n < number_of v) =  
  12.123 -        (let pv = number_of (bin_pred v) in  
  12.124 +        (let pv = number_of (pred v) in  
  12.125           if neg pv then False else n < nat pv)"
  12.126  apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
  12.127                    number_of_pred nat_number_of_def
  12.128 @@ -489,13 +486,13 @@
  12.129  
  12.130  lemma le_number_of_Suc [simp]:
  12.131       "(number_of v <= Suc n) =  
  12.132 -        (let pv = number_of (bin_pred v) in  
  12.133 +        (let pv = number_of (pred v) in  
  12.134           if neg pv then True else nat pv <= n)"
  12.135  by (simp add: Let_def less_Suc_number_of linorder_not_less [symmetric])
  12.136  
  12.137  lemma le_Suc_number_of [simp]:
  12.138       "(Suc n <= number_of v) =  
  12.139 -        (let pv = number_of (bin_pred v) in  
  12.140 +        (let pv = number_of (pred v) in  
  12.141           if neg pv then False else n <= nat pv)"
  12.142  by (simp add: Let_def less_number_of_Suc linorder_not_less [symmetric])
  12.143  
  12.144 @@ -568,23 +565,20 @@
  12.145  text{*For the integers*}
  12.146  
  12.147  lemma zpower_number_of_even:
  12.148 -     "(z::int) ^ number_of (w BIT bit.B0) =  
  12.149 -      (let w = z ^ (number_of w) in  w*w)"
  12.150 -apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
  12.151 -apply (simp only: number_of_add) 
  12.152 +  "(z::int) ^ number_of (w BIT bit.B0) = (let w = z ^ (number_of w) in w * w)"
  12.153 +unfolding Let_def nat_number_of_def number_of_BIT bit.cases
  12.154  apply (rule_tac x = "number_of w" in spec, clarify)
  12.155  apply (case_tac " (0::int) <= x")
  12.156  apply (auto simp add: nat_mult_distrib power_even_eq power2_eq_square)
  12.157  done
  12.158  
  12.159  lemma zpower_number_of_odd:
  12.160 -     "(z::int) ^ number_of (w BIT bit.B1) =  
  12.161 -          (if (0::int) <= number_of w                    
  12.162 -           then (let w = z ^ (number_of w) in  z*w*w)    
  12.163 -           else 1)"
  12.164 -apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
  12.165 -apply (simp only: number_of_add nat_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0) 
  12.166 -apply (rule_tac x = "number_of w" in spec, clarify)
  12.167 +  "(z::int) ^ number_of (w BIT bit.B1) = (if (0::int) <= number_of w                    
  12.168 +     then (let w = z ^ (number_of w) in z * w * w) else 1)"
  12.169 +unfolding Let_def nat_number_of_def number_of_BIT bit.cases
  12.170 +apply (rule_tac x = "number_of w" in spec, auto)
  12.171 +apply (simp only: nat_add_distrib nat_mult_distrib)
  12.172 +apply simp
  12.173  apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat)
  12.174  done
  12.175  
  12.176 @@ -695,13 +689,13 @@
  12.177       "number_of v + (number_of v' + (k::nat)) =  
  12.178           (if neg (number_of v :: int) then number_of v' + k  
  12.179            else if neg (number_of v' :: int) then number_of v + k  
  12.180 -          else number_of (bin_add v v') + k)"
  12.181 +          else number_of (v + v') + k)"
  12.182  by simp
  12.183  
  12.184  lemma nat_number_of_mult_left:
  12.185       "number_of v * (number_of v' * (k::nat)) =  
  12.186           (if neg (number_of v :: int) then 0
  12.187 -          else number_of (bin_mult v v') * k)"
  12.188 +          else number_of (v * v') * k)"
  12.189  by simp
  12.190  
  12.191  
  12.192 @@ -780,7 +774,7 @@
  12.193  subsection {* code generator setup *}
  12.194  
  12.195  lemma number_of_is_nat_rep_bin [code inline]:
  12.196 -  "(number_of b :: nat) = nat (Rep_Bin b)"
  12.197 +  "(number_of b :: nat) = nat (number_of b)"
  12.198    unfolding nat_number_of_def int_number_of_def by simp
  12.199  
  12.200  
    13.1 --- a/src/HOL/Integ/NatSimprocs.thy	Wed Sep 06 10:01:27 2006 +0200
    13.2 +++ b/src/HOL/Integ/NatSimprocs.thy	Wed Sep 06 13:48:02 2006 +0200
    13.3 @@ -22,9 +22,9 @@
    13.4  text {*Now just instantiating @{text n} to @{text "number_of v"} does
    13.5    the right simplification, but with some redundant inequality
    13.6    tests.*}
    13.7 -lemma neg_number_of_bin_pred_iff_0:
    13.8 -     "neg (number_of (bin_pred v)::int) = (number_of v = (0::nat))"
    13.9 -apply (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0) ")
   13.10 +lemma neg_number_of_pred_iff_0:
   13.11 +  "neg (number_of (pred v)::int) = (number_of v = (0::nat))"
   13.12 +apply (subgoal_tac "neg (number_of (pred v)) = (number_of v < Suc 0) ")
   13.13  apply (simp only: less_Suc_eq_le le_0_eq)
   13.14  apply (subst less_number_of_Suc, simp)
   13.15  done
   13.16 @@ -32,13 +32,13 @@
   13.17  text{*No longer required as a simprule because of the @{text inverse_fold}
   13.18     simproc*}
   13.19  lemma Suc_diff_number_of:
   13.20 -     "neg (number_of (bin_minus v)::int) ==>  
   13.21 -      Suc m - (number_of v) = m - (number_of (bin_pred v))"
   13.22 +     "neg (number_of (uminus v)::int) ==>  
   13.23 +      Suc m - (number_of v) = m - (number_of (pred v))"
   13.24  apply (subst Suc_diff_eq_diff_pred)
   13.25  apply simp
   13.26  apply (simp del: nat_numeral_1_eq_1)
   13.27  apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] 
   13.28 -                        neg_number_of_bin_pred_iff_0)
   13.29 +                        neg_number_of_pred_iff_0)
   13.30  done
   13.31  
   13.32  lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
   13.33 @@ -49,40 +49,40 @@
   13.34  
   13.35  lemma nat_case_number_of [simp]:
   13.36       "nat_case a f (number_of v) =  
   13.37 -        (let pv = number_of (bin_pred v) in  
   13.38 +        (let pv = number_of (pred v) in  
   13.39           if neg pv then a else f (nat pv))"
   13.40 -by (simp split add: nat.split add: Let_def neg_number_of_bin_pred_iff_0)
   13.41 +by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0)
   13.42  
   13.43  lemma nat_case_add_eq_if [simp]:
   13.44       "nat_case a f ((number_of v) + n) =  
   13.45 -       (let pv = number_of (bin_pred v) in  
   13.46 +       (let pv = number_of (pred v) in  
   13.47           if neg pv then nat_case a f n else f (nat pv + n))"
   13.48  apply (subst add_eq_if)
   13.49  apply (simp split add: nat.split
   13.50              del: nat_numeral_1_eq_1
   13.51  	    add: numeral_1_eq_Suc_0 [symmetric] Let_def 
   13.52 -                 neg_imp_number_of_eq_0 neg_number_of_bin_pred_iff_0)
   13.53 +                 neg_imp_number_of_eq_0 neg_number_of_pred_iff_0)
   13.54  done
   13.55  
   13.56  lemma nat_rec_number_of [simp]:
   13.57       "nat_rec a f (number_of v) =  
   13.58 -        (let pv = number_of (bin_pred v) in  
   13.59 +        (let pv = number_of (pred v) in  
   13.60           if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
   13.61  apply (case_tac " (number_of v) ::nat")
   13.62 -apply (simp_all (no_asm_simp) add: Let_def neg_number_of_bin_pred_iff_0)
   13.63 +apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0)
   13.64  apply (simp split add: split_if_asm)
   13.65  done
   13.66  
   13.67  lemma nat_rec_add_eq_if [simp]:
   13.68       "nat_rec a f (number_of v + n) =  
   13.69 -        (let pv = number_of (bin_pred v) in  
   13.70 +        (let pv = number_of (pred v) in  
   13.71           if neg pv then nat_rec a f n  
   13.72                     else f (nat pv + n) (nat_rec a f (nat pv + n)))"
   13.73  apply (subst add_eq_if)
   13.74  apply (simp split add: nat.split
   13.75              del: nat_numeral_1_eq_1
   13.76              add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0
   13.77 -                 neg_number_of_bin_pred_iff_0)
   13.78 +                 neg_number_of_pred_iff_0)
   13.79  done
   13.80  
   13.81  
    14.1 --- a/src/HOL/Integ/Numeral.thy	Wed Sep 06 10:01:27 2006 +0200
    14.2 +++ b/src/HOL/Integ/Numeral.thy	Wed Sep 06 13:48:02 2006 +0200
    14.3 @@ -1,292 +1,315 @@
    14.4 -(*  Title:	HOL/Integ/Numeral.thy
    14.5 +(*  Title:      HOL/Integ/Numeral.thy
    14.6      ID:         $Id$
    14.7 -    Author:	Lawrence C Paulson, Cambridge University Computer Laboratory
    14.8 -    Copyright	1994  University of Cambridge
    14.9 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
   14.10 +    Copyright   1994  University of Cambridge
   14.11  *)
   14.12  
   14.13 -header{*Arithmetic on Binary Integers*}
   14.14 +header {* Arithmetic on Binary Integers *}
   14.15  
   14.16  theory Numeral
   14.17  imports IntDef Datatype
   14.18  uses "../Tools/numeral_syntax.ML"
   14.19  begin
   14.20  
   14.21 -text{*This formalization defines binary arithmetic in terms of the integers
   14.22 -rather than using a datatype. This avoids multiple representations (leading
   14.23 -zeroes, etc.)  See @{text "ZF/Integ/twos-compl.ML"}, function @{text
   14.24 -int_of_binary}, for the numerical interpretation.
   14.25 +text {*
   14.26 +  This formalization defines binary arithmetic in terms of the integers
   14.27 +  rather than using a datatype. This avoids multiple representations (leading
   14.28 +  zeroes, etc.)  See @{text "ZF/Integ/twos-compl.ML"}, function @{text
   14.29 +  int_of_binary}, for the numerical interpretation.
   14.30  
   14.31 -The representation expects that @{text "(m mod 2)"} is 0 or 1,
   14.32 -even if m is negative;
   14.33 -For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
   14.34 -@{text "-5 = (-3)*2 + 1"}.
   14.35 +  The representation expects that @{text "(m mod 2)"} is 0 or 1,
   14.36 +  even if m is negative;
   14.37 +  For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
   14.38 +  @{text "-5 = (-3)*2 + 1"}.
   14.39  *}
   14.40  
   14.41 +text{*
   14.42 +  This datatype avoids the use of type @{typ bool}, which would make
   14.43 +  all of the rewrite rules higher-order.
   14.44 +*}
   14.45  
   14.46 -typedef (Bin)
   14.47 -  bin = "UNIV::int set"
   14.48 -    by (auto)
   14.49 -
   14.50 -text{*This datatype avoids the use of type @{typ bool}, which would make
   14.51 -all of the rewrite rules higher-order. If the use of datatype causes
   14.52 -problems, this two-element type can easily be formalized using typedef.*}
   14.53  datatype bit = B0 | B1
   14.54  
   14.55  constdefs
   14.56 -  Pls :: "bin"
   14.57 -   "Pls == Abs_Bin 0"
   14.58 -
   14.59 -  Min :: "bin"
   14.60 -   "Min == Abs_Bin (- 1)"
   14.61 -
   14.62 -  Bit :: "[bin,bit] => bin"    (infixl "BIT" 90)
   14.63 -   --{*That is, 2w+b*}
   14.64 -   "w BIT b == Abs_Bin ((case b of B0 => 0 | B1 => 1) + Rep_Bin w + Rep_Bin w)"
   14.65 -
   14.66 +  Pls :: int
   14.67 +  "Pls == 0"
   14.68 +  Min :: int
   14.69 +  "Min == - 1"
   14.70 +  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90)
   14.71 +  "k BIT b == (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
   14.72  
   14.73  axclass
   14.74    number < type  -- {* for numeric types: nat, int, real, \dots *}
   14.75  
   14.76  consts
   14.77 -  number_of :: "bin => 'a::number"
   14.78 +  number_of :: "int \<Rightarrow> 'a::number"
   14.79  
   14.80  syntax
   14.81 -  "_Numeral" :: "num_const => 'a"    ("_")
   14.82 +  "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
   14.83  
   14.84  setup NumeralSyntax.setup
   14.85  
   14.86  abbreviation
   14.87 -  "Numeral0 == number_of Pls"
   14.88 -  "Numeral1 == number_of (Pls BIT B1)"
   14.89 +  "Numeral0 \<equiv> number_of Pls"
   14.90 +  "Numeral1 \<equiv> number_of (Pls BIT B1)"
   14.91  
   14.92 -lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
   14.93 +lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
   14.94    -- {* Unfold all @{text let}s involving constants *}
   14.95 -  by (simp add: Let_def)
   14.96 +  unfolding Let_def ..
   14.97 +
   14.98 +lemma Let_0 [simp]: "Let 0 f = f 0"
   14.99 +  unfolding Let_def ..
  14.100 +
  14.101 +lemma Let_1 [simp]: "Let 1 f = f 1"
  14.102 +  unfolding Let_def ..
  14.103  
  14.104 -lemma Let_0 [simp]: "Let 0 f == f 0"
  14.105 -  by (simp add: Let_def)
  14.106 +definition
  14.107 +  succ :: "int \<Rightarrow> int"
  14.108 +  "succ k = k + 1"
  14.109 +  pred :: "int \<Rightarrow> int"
  14.110 +  "pred k = k - 1"
  14.111 +
  14.112 +lemmas numeral_simps = 
  14.113 +  succ_def pred_def Pls_def Min_def Bit_def
  14.114  
  14.115 -lemma Let_1 [simp]: "Let 1 f == f 1"
  14.116 -  by (simp add: Let_def)
  14.117 +text {* Removal of leading zeroes *}
  14.118 +
  14.119 +lemma Pls_0_eq [simp]:
  14.120 +  "Pls BIT B0 = Pls"
  14.121 +  unfolding numeral_simps by simp
  14.122 +
  14.123 +lemma Min_1_eq [simp]:
  14.124 +  "Min BIT B1 = Min"
  14.125 +  unfolding numeral_simps by simp
  14.126  
  14.127  
  14.128 -constdefs
  14.129 -  bin_succ  :: "bin=>bin"
  14.130 -   "bin_succ w == Abs_Bin(Rep_Bin w + 1)"
  14.131 -
  14.132 -  bin_pred  :: "bin=>bin"
  14.133 -   "bin_pred w == Abs_Bin(Rep_Bin w - 1)"
  14.134 +subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
  14.135  
  14.136 -  bin_minus  :: "bin=>bin"
  14.137 -   "bin_minus w == Abs_Bin(- (Rep_Bin w))"
  14.138 +lemma succ_Pls [simp]:
  14.139 +  "succ Pls = Pls BIT B1"
  14.140 +  unfolding numeral_simps by simp
  14.141  
  14.142 -  bin_add  :: "[bin,bin]=>bin"
  14.143 -   "bin_add v w == Abs_Bin(Rep_Bin v + Rep_Bin w)"
  14.144 -
  14.145 -  bin_mult  :: "[bin,bin]=>bin"
  14.146 -   "bin_mult v w == Abs_Bin(Rep_Bin v * Rep_Bin w)"
  14.147 +lemma succ_Min [simp]:
  14.148 +  "succ Min = Pls"
  14.149 +  unfolding numeral_simps by simp
  14.150  
  14.151 -lemma Abs_Bin_inverse':
  14.152 -  "Rep_Bin (Abs_Bin x) = x"
  14.153 -by (rule Abs_Bin_inverse) (auto simp add: Bin_def)
  14.154 -
  14.155 -lemmas Bin_simps = 
  14.156 -       bin_succ_def bin_pred_def bin_minus_def bin_add_def bin_mult_def
  14.157 -       Pls_def Min_def Bit_def Abs_Bin_inverse Rep_Bin_inverse Bin_def
  14.158 +lemma succ_1 [simp]:
  14.159 +  "succ (k BIT B1) = succ k BIT B0"
  14.160 +  unfolding numeral_simps by simp
  14.161  
  14.162 -text{*Removal of leading zeroes*}
  14.163 -lemma Pls_0_eq [simp]: "Pls BIT B0 = Pls"
  14.164 -by (simp add: Bin_simps)
  14.165 +lemma succ_0 [simp]:
  14.166 +  "succ (k BIT B0) = k BIT B1"
  14.167 +  unfolding numeral_simps by simp
  14.168  
  14.169 -lemma Min_1_eq [simp]: "Min BIT B1 = Min"
  14.170 -by (simp add: Bin_simps)
  14.171 -
  14.172 -subsection{*The Functions @{term bin_succ},  @{term bin_pred} and @{term bin_minus}*}
  14.173 +lemma pred_Pls [simp]:
  14.174 +  "pred Pls = Min"
  14.175 +  unfolding numeral_simps by simp
  14.176  
  14.177 -lemma bin_succ_Pls [simp]: "bin_succ Pls = Pls BIT B1"
  14.178 -by (simp add: Bin_simps) 
  14.179 -
  14.180 -lemma bin_succ_Min [simp]: "bin_succ Min = Pls"
  14.181 -by (simp add: Bin_simps) 
  14.182 -
  14.183 -lemma bin_succ_1 [simp]: "bin_succ(w BIT B1) = (bin_succ w) BIT B0"
  14.184 -by (simp add: Bin_simps add_ac) 
  14.185 +lemma pred_Min [simp]:
  14.186 +  "pred Min = Min BIT B0"
  14.187 +  unfolding numeral_simps by simp
  14.188  
  14.189 -lemma bin_succ_0 [simp]: "bin_succ(w BIT B0) = w BIT B1"
  14.190 -by (simp add: Bin_simps add_ac) 
  14.191 +lemma pred_1 [simp]:
  14.192 +  "pred (k BIT B1) = k BIT B0"
  14.193 +  unfolding numeral_simps by simp
  14.194  
  14.195 -lemma bin_pred_Pls [simp]: "bin_pred Pls = Min"
  14.196 -by (simp add: Bin_simps) 
  14.197 -
  14.198 -lemma bin_pred_Min [simp]: "bin_pred Min = Min BIT B0"
  14.199 -by (simp add: Bin_simps diff_minus) 
  14.200 +lemma pred_0 [simp]:
  14.201 +  "pred (k BIT B0) = pred k BIT B1"
  14.202 +  unfolding numeral_simps by simp 
  14.203  
  14.204 -lemma bin_pred_1 [simp]: "bin_pred(w BIT B1) = w BIT B0"
  14.205 -by (simp add: Bin_simps) 
  14.206 +lemma minus_Pls [simp]:
  14.207 +  "- Pls = Pls"
  14.208 +  unfolding numeral_simps by simp 
  14.209  
  14.210 -lemma bin_pred_0 [simp]: "bin_pred(w BIT B0) = (bin_pred w) BIT B1"
  14.211 -by (simp add: Bin_simps diff_minus add_ac) 
  14.212 -
  14.213 -lemma bin_minus_Pls [simp]: "bin_minus Pls = Pls"
  14.214 -by (simp add: Bin_simps) 
  14.215 +lemma minus_Min [simp]:
  14.216 +  "- Min = Pls BIT B1"
  14.217 +  unfolding numeral_simps by simp 
  14.218  
  14.219 -lemma bin_minus_Min [simp]: "bin_minus Min = Pls BIT B1"
  14.220 -by (simp add: Bin_simps) 
  14.221 +lemma minus_1 [simp]:
  14.222 +  "- (k BIT B1) = pred (- k) BIT B1"
  14.223 +  unfolding numeral_simps by simp 
  14.224  
  14.225 -lemma bin_minus_1 [simp]:
  14.226 -     "bin_minus (w BIT B1) = bin_pred (bin_minus w) BIT B1"
  14.227 -by (simp add: Bin_simps add_ac diff_minus) 
  14.228 -
  14.229 - lemma bin_minus_0 [simp]: "bin_minus(w BIT B0) = (bin_minus w) BIT B0"
  14.230 -by (simp add: Bin_simps) 
  14.231 +lemma minus_0 [simp]:
  14.232 +  "- (k BIT B0) = (- k) BIT B0"
  14.233 +  unfolding numeral_simps by simp 
  14.234  
  14.235  
  14.236 -subsection{*Binary Addition and Multiplication:
  14.237 -         @{term bin_add} and @{term bin_mult}*}
  14.238 +subsection {*
  14.239 +  Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
  14.240 +    and @{term "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
  14.241 +*}
  14.242  
  14.243 -lemma bin_add_Pls [simp]: "bin_add Pls w = w"
  14.244 -by (simp add: Bin_simps) 
  14.245 +lemma add_Pls [simp]:
  14.246 +  "Pls + k = k"
  14.247 +  unfolding numeral_simps by simp 
  14.248  
  14.249 -lemma bin_add_Min [simp]: "bin_add Min w = bin_pred w"
  14.250 -by (simp add: Bin_simps diff_minus add_ac) 
  14.251 +lemma add_Min [simp]:
  14.252 +  "Min + k = pred k"
  14.253 +  unfolding numeral_simps by simp
  14.254  
  14.255 -lemma bin_add_BIT_11 [simp]:
  14.256 -     "bin_add (v BIT B1) (w BIT B1) = bin_add v (bin_succ w) BIT B0"
  14.257 -by (simp add: Bin_simps add_ac)
  14.258 +lemma add_BIT_11 [simp]:
  14.259 +  "(k BIT B1) + (l BIT B1) = (k + succ l) BIT B0"
  14.260 +  unfolding numeral_simps by simp
  14.261  
  14.262 -lemma bin_add_BIT_10 [simp]:
  14.263 -     "bin_add (v BIT B1) (w BIT B0) = (bin_add v w) BIT B1"
  14.264 -by (simp add: Bin_simps add_ac)
  14.265 +lemma add_BIT_10 [simp]:
  14.266 +  "(k BIT B1) + (l BIT B0) = (k + l) BIT B1"
  14.267 +  unfolding numeral_simps by simp
  14.268  
  14.269 -lemma bin_add_BIT_0 [simp]:
  14.270 -     "bin_add (v BIT B0) (w BIT y) = bin_add v w BIT y"
  14.271 -by (simp add: Bin_simps add_ac)
  14.272 +lemma add_BIT_0 [simp]:
  14.273 +  "(k BIT B0) + (l BIT b) = (k + l) BIT b"
  14.274 +  unfolding numeral_simps by simp 
  14.275  
  14.276 -lemma bin_add_Pls_right [simp]: "bin_add w Pls = w"
  14.277 -by (simp add: Bin_simps) 
  14.278 +lemma add_Pls_right [simp]:
  14.279 +  "k + Pls = k"
  14.280 +  unfolding numeral_simps by simp 
  14.281  
  14.282 -lemma bin_add_Min_right [simp]: "bin_add w Min = bin_pred w"
  14.283 -by (simp add: Bin_simps diff_minus) 
  14.284 +lemma add_Min_right [simp]:
  14.285 +  "k + Min = pred k"
  14.286 +  unfolding numeral_simps by simp 
  14.287  
  14.288 -lemma bin_mult_Pls [simp]: "bin_mult Pls w = Pls"
  14.289 -by (simp add: Bin_simps) 
  14.290 +lemma mult_Pls [simp]:
  14.291 +  "Pls * w = Pls"
  14.292 +  unfolding numeral_simps by simp 
  14.293  
  14.294 -lemma bin_mult_Min [simp]: "bin_mult Min w = bin_minus w"
  14.295 -by (simp add: Bin_simps) 
  14.296 +lemma mult_Min [simp]:
  14.297 +  "Min * k = - k"
  14.298 +  unfolding numeral_simps by simp 
  14.299  
  14.300 -lemma bin_mult_1 [simp]:
  14.301 -     "bin_mult (v BIT B1) w = bin_add ((bin_mult v w) BIT B0) w"
  14.302 -by (simp add: Bin_simps add_ac left_distrib)
  14.303 +lemma mult_num1 [simp]:
  14.304 +  "(k BIT B1) * l = ((k * l) BIT B0) + l"
  14.305 +  unfolding numeral_simps int_distrib by simp 
  14.306  
  14.307 -lemma bin_mult_0 [simp]: "bin_mult (v BIT B0) w = (bin_mult v w) BIT B0"
  14.308 -by (simp add: Bin_simps left_distrib)
  14.309 +lemma mult_num0 [simp]:
  14.310 +  "(k BIT B0) * l = (k * l) BIT B0"
  14.311 +  unfolding numeral_simps int_distrib by simp 
  14.312  
  14.313  
  14.314  
  14.315 -subsection{*Converting Numerals to Rings: @{term number_of}*}
  14.316 +subsection {* Converting Numerals to Rings: @{term number_of} *}
  14.317  
  14.318  axclass number_ring \<subseteq> number, comm_ring_1
  14.319 -  number_of_eq: "number_of w = of_int (Rep_Bin w)"
  14.320 +  number_of_eq: "number_of k = of_int k"
  14.321  
  14.322  lemma number_of_succ:
  14.323 -     "number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)"
  14.324 -by (simp add: number_of_eq Bin_simps)
  14.325 +  "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
  14.326 +  unfolding number_of_eq numeral_simps by simp
  14.327  
  14.328  lemma number_of_pred:
  14.329 -     "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
  14.330 -by (simp add: number_of_eq Bin_simps)
  14.331 +  "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
  14.332 +  unfolding number_of_eq numeral_simps by simp
  14.333  
  14.334  lemma number_of_minus:
  14.335 -     "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)"
  14.336 -by (simp add: number_of_eq Bin_simps) 
  14.337 +  "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
  14.338 +  unfolding number_of_eq numeral_simps by simp
  14.339  
  14.340  lemma number_of_add:
  14.341 -     "number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)"
  14.342 -by (simp add: number_of_eq Bin_simps) 
  14.343 +  "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
  14.344 +  unfolding number_of_eq numeral_simps by simp
  14.345  
  14.346  lemma number_of_mult:
  14.347 -     "number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)"
  14.348 -by (simp add: number_of_eq Bin_simps) 
  14.349 +  "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
  14.350 +  unfolding number_of_eq numeral_simps by simp
  14.351  
  14.352 -text{*The correctness of shifting.  But it doesn't seem to give a measurable
  14.353 -  speed-up.*}
  14.354 +text {*
  14.355 +  The correctness of shifting.
  14.356 +  But it doesn't seem to give a measurable speed-up.
  14.357 +*}
  14.358 +
  14.359  lemma double_number_of_BIT:
  14.360 -     "(1+1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)"
  14.361 -by (simp add: number_of_eq Bin_simps left_distrib) 
  14.362 +  "(1 + 1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)"
  14.363 +  unfolding number_of_eq numeral_simps left_distrib by simp
  14.364  
  14.365 -text{*Converting numerals 0 and 1 to their abstract versions*}
  14.366 -lemma numeral_0_eq_0 [simp]: "Numeral0 = (0::'a::number_ring)"
  14.367 -by (simp add: number_of_eq Bin_simps) 
  14.368 +text {*
  14.369 +  Converting numerals 0 and 1 to their abstract versions.
  14.370 +*}
  14.371 +
  14.372 +lemma numeral_0_eq_0 [simp]:
  14.373 +  "Numeral0 = (0::'a::number_ring)"
  14.374 +  unfolding number_of_eq numeral_simps by simp
  14.375  
  14.376 -lemma numeral_1_eq_1 [simp]: "Numeral1 = (1::'a::number_ring)"
  14.377 -by (simp add: number_of_eq Bin_simps) 
  14.378 +lemma numeral_1_eq_1 [simp]:
  14.379 +  "Numeral1 = (1::'a::number_ring)"
  14.380 +  unfolding number_of_eq numeral_simps by simp
  14.381  
  14.382 -text{*Special-case simplification for small constants*}
  14.383 +text {*
  14.384 +  Special-case simplification for small constants.
  14.385 +*}
  14.386  
  14.387 -text{*Unary minus for the abstract constant 1. Cannot be inserted
  14.388 -  as a simprule until later: it is @{text number_of_Min} re-oriented!*}
  14.389 -lemma numeral_m1_eq_minus_1: "(-1::'a::number_ring) = - 1"
  14.390 -by (simp add: number_of_eq Bin_simps) 
  14.391 -
  14.392 +text{*
  14.393 +  Unary minus for the abstract constant 1. Cannot be inserted
  14.394 +  as a simprule until later: it is @{text number_of_Min} re-oriented!
  14.395 +*}
  14.396  
  14.397 -lemma mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)"
  14.398 -by (simp add: numeral_m1_eq_minus_1)
  14.399 +lemma numeral_m1_eq_minus_1:
  14.400 +  "(-1::'a::number_ring) = - 1"
  14.401 +  unfolding number_of_eq numeral_simps by simp
  14.402  
  14.403 -lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)"
  14.404 -by (simp add: numeral_m1_eq_minus_1)
  14.405 +lemma mult_minus1 [simp]:
  14.406 +  "-1 * z = -(z::'a::number_ring)"
  14.407 +  unfolding number_of_eq numeral_simps by simp
  14.408 +
  14.409 +lemma mult_minus1_right [simp]:
  14.410 +  "z * -1 = -(z::'a::number_ring)"
  14.411 +  unfolding number_of_eq numeral_simps by simp
  14.412  
  14.413  (*Negation of a coefficient*)
  14.414  lemma minus_number_of_mult [simp]:
  14.415 -     "- (number_of w) * z = number_of(bin_minus w) * (z::'a::number_ring)"
  14.416 -by (simp add: number_of_minus)
  14.417 +   "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
  14.418 +   unfolding number_of_eq by simp
  14.419 +
  14.420 +text {* Subtraction *}
  14.421 +
  14.422 +lemma diff_number_of_eq:
  14.423 +  "number_of v - number_of w =
  14.424 +    (number_of (v + uminus w)::'a::number_ring)"
  14.425 +  unfolding number_of_eq by simp
  14.426  
  14.427 -text{*Subtraction*}
  14.428 -lemma diff_number_of_eq:
  14.429 -     "number_of v - number_of w =
  14.430 -      (number_of(bin_add v (bin_minus w))::'a::number_ring)"
  14.431 -by (simp add: diff_minus number_of_add number_of_minus)
  14.432 +lemma number_of_Pls:
  14.433 +  "number_of Pls = (0::'a::number_ring)"
  14.434 +  unfolding number_of_eq numeral_simps by simp
  14.435 +
  14.436 +lemma number_of_Min:
  14.437 +  "number_of Min = (- 1::'a::number_ring)"
  14.438 +  unfolding number_of_eq numeral_simps by simp
  14.439 +
  14.440 +lemma number_of_BIT:
  14.441 +  "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring))
  14.442 +    + (number_of w) + (number_of w)"
  14.443 +  unfolding number_of_eq numeral_simps by (simp split: bit.split)
  14.444  
  14.445  
  14.446 -lemma number_of_Pls: "number_of Pls = (0::'a::number_ring)"
  14.447 -by (simp add: number_of_eq Bin_simps) 
  14.448 -
  14.449 -lemma number_of_Min: "number_of Min = (- 1::'a::number_ring)"
  14.450 -by (simp add: number_of_eq Bin_simps) 
  14.451 +subsection {* Equality of Binary Numbers *}
  14.452  
  14.453 -lemma number_of_BIT:
  14.454 -     "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring)) +
  14.455 -	                   (number_of w) + (number_of w)"
  14.456 -by (simp add: number_of_eq Bin_simps split: bit.split) 
  14.457 -
  14.458 -
  14.459 -
  14.460 -subsection{*Equality of Binary Numbers*}
  14.461 -
  14.462 -text{*First version by Norbert Voelker*}
  14.463 +text {* First version by Norbert Voelker *}
  14.464  
  14.465  lemma eq_number_of_eq:
  14.466    "((number_of x::'a::number_ring) = number_of y) =
  14.467 -   iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
  14.468 -by (simp add: iszero_def compare_rls number_of_add number_of_minus)
  14.469 +   iszero (number_of (x + uminus y) :: 'a)"
  14.470 +  unfolding iszero_def number_of_add number_of_minus
  14.471 +  by (simp add: compare_rls)
  14.472  
  14.473 -lemma iszero_number_of_Pls: "iszero ((number_of Pls)::'a::number_ring)"
  14.474 -by (simp add: iszero_def numeral_0_eq_0)
  14.475 +lemma iszero_number_of_Pls:
  14.476 +  "iszero ((number_of Pls)::'a::number_ring)"
  14.477 +  unfolding iszero_def numeral_0_eq_0 ..
  14.478  
  14.479 -lemma nonzero_number_of_Min: "~ iszero ((number_of Min)::'a::number_ring)"
  14.480 -by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
  14.481 +lemma nonzero_number_of_Min:
  14.482 +  "~ iszero ((number_of Min)::'a::number_ring)"
  14.483 +  unfolding iszero_def numeral_m1_eq_minus_1 by simp
  14.484  
  14.485  
  14.486 -subsection{*Comparisons, for Ordered Rings*}
  14.487 +subsection {* Comparisons, for Ordered Rings *}
  14.488  
  14.489 -lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))"
  14.490 +lemma double_eq_0_iff:
  14.491 +  "(a + a = 0) = (a = (0::'a::ordered_idom))"
  14.492  proof -
  14.493 -  have "a + a = (1+1)*a" by (simp add: left_distrib)
  14.494 +  have "a + a = (1 + 1) * a" unfolding left_distrib by simp
  14.495    with zero_less_two [where 'a = 'a]
  14.496    show ?thesis by force
  14.497  qed
  14.498  
  14.499  lemma le_imp_0_less: 
  14.500 -  assumes le: "0 \<le> z" shows "(0::int) < 1 + z"
  14.501 +  assumes le: "0 \<le> z"
  14.502 +  shows "(0::int) < 1 + z"
  14.503  proof -
  14.504    have "0 \<le> z" .
  14.505    also have "... < z + 1" by (rule less_add_one) 
  14.506 @@ -294,7 +317,8 @@
  14.507    finally show "0 < 1 + z" .
  14.508  qed
  14.509  
  14.510 -lemma odd_nonzero: "1 + z + z \<noteq> (0::int)";
  14.511 +lemma odd_nonzero:
  14.512 +  "1 + z + z \<noteq> (0::int)";
  14.513  proof (cases z rule: int_cases)
  14.514    case (nonneg n)
  14.515    have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
  14.516 @@ -315,11 +339,13 @@
  14.517    qed
  14.518  qed
  14.519  
  14.520 +text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
  14.521  
  14.522 -text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
  14.523 -lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)"
  14.524 -proof (unfold Ints_def) 
  14.525 -  assume "a \<in> range of_int"
  14.526 +lemma Ints_odd_nonzero:
  14.527 +  assumes in_Ints: "a \<in> Ints"
  14.528 +  shows "1 + a + a \<noteq> (0::'a::ordered_idom)"
  14.529 +proof -
  14.530 +  from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
  14.531    then obtain z where a: "a = of_int z" ..
  14.532    show ?thesis
  14.533    proof
  14.534 @@ -330,46 +356,50 @@
  14.535    qed
  14.536  qed 
  14.537  
  14.538 -lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"
  14.539 -by (simp add: number_of_eq Ints_def) 
  14.540 -
  14.541 +lemma Ints_number_of:
  14.542 +  "(number_of w :: 'a::number_ring) \<in> Ints"
  14.543 +  unfolding number_of_eq Ints_def by simp
  14.544  
  14.545  lemma iszero_number_of_BIT:
  14.546 -     "iszero (number_of (w BIT x)::'a) = 
  14.547 -      (x=B0 & iszero (number_of w::'a::{ordered_idom,number_ring}))"
  14.548 -by (simp add: iszero_def number_of_eq Bin_simps double_eq_0_iff 
  14.549 -              Ints_odd_nonzero Ints_def split: bit.split)
  14.550 +  "iszero (number_of (w BIT x)::'a) = 
  14.551 +   (x = B0 \<and> iszero (number_of w::'a::{ordered_idom,number_ring}))"
  14.552 +  by (simp add: iszero_def number_of_eq numeral_simps double_eq_0_iff 
  14.553 +    Ints_odd_nonzero Ints_def split: bit.split)
  14.554  
  14.555  lemma iszero_number_of_0:
  14.556 -     "iszero (number_of (w BIT B0) :: 'a::{ordered_idom,number_ring}) = 
  14.557 -      iszero (number_of w :: 'a)"
  14.558 -by (simp only: iszero_number_of_BIT simp_thms)
  14.559 +  "iszero (number_of (w BIT B0) :: 'a::{ordered_idom,number_ring}) = 
  14.560 +  iszero (number_of w :: 'a)"
  14.561 +  by (simp only: iszero_number_of_BIT simp_thms)
  14.562  
  14.563  lemma iszero_number_of_1:
  14.564 -     "~ iszero (number_of (w BIT B1)::'a::{ordered_idom,number_ring})"
  14.565 -by (simp add: iszero_number_of_BIT) 
  14.566 +  "~ iszero (number_of (w BIT B1)::'a::{ordered_idom,number_ring})"
  14.567 +  by (simp add: iszero_number_of_BIT) 
  14.568  
  14.569  
  14.570 -subsection{*The Less-Than Relation*}
  14.571 +subsection {* The Less-Than Relation *}
  14.572  
  14.573  lemma less_number_of_eq_neg:
  14.574 -    "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
  14.575 -     = neg (number_of (bin_add x (bin_minus y)) :: 'a)"
  14.576 +  "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
  14.577 +  = neg (number_of (x + uminus y) :: 'a)"
  14.578  apply (subst less_iff_diff_less_0) 
  14.579  apply (simp add: neg_def diff_minus number_of_add number_of_minus)
  14.580  done
  14.581  
  14.582 -text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
  14.583 -  @{term Numeral0} IS @{term "number_of Pls"} *}
  14.584 +text {*
  14.585 +  If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
  14.586 +  @{term Numeral0} IS @{term "number_of Pls"}
  14.587 +*}
  14.588 +
  14.589  lemma not_neg_number_of_Pls:
  14.590 -     "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
  14.591 -by (simp add: neg_def numeral_0_eq_0)
  14.592 +  "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
  14.593 +  by (simp add: neg_def numeral_0_eq_0)
  14.594  
  14.595  lemma neg_number_of_Min:
  14.596 -     "neg (number_of Min ::'a::{ordered_idom,number_ring})"
  14.597 -by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
  14.598 +  "neg (number_of Min ::'a::{ordered_idom,number_ring})"
  14.599 +  by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
  14.600  
  14.601 -lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
  14.602 +lemma double_less_0_iff:
  14.603 +  "(a + a < 0) = (a < (0::'a::ordered_idom))"
  14.604  proof -
  14.605    have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
  14.606    also have "... = (a < 0)"
  14.607 @@ -378,7 +408,8 @@
  14.608    finally show ?thesis .
  14.609  qed
  14.610  
  14.611 -lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))";
  14.612 +lemma odd_less_0:
  14.613 +  "(1 + z + z < 0) = (z < (0::int))";
  14.614  proof (cases z rule: int_cases)
  14.615    case (nonneg n)
  14.616    thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
  14.617 @@ -386,14 +417,16 @@
  14.618  next
  14.619    case (neg n)
  14.620    thus ?thesis by (simp del: int_Suc
  14.621 -			add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
  14.622 +    add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
  14.623  qed
  14.624  
  14.625 -text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
  14.626 +text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
  14.627 +
  14.628  lemma Ints_odd_less_0: 
  14.629 -     "a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
  14.630 -proof (unfold Ints_def) 
  14.631 -  assume "a \<in> range of_int"
  14.632 +  assumes in_Ints: "a \<in> Ints"
  14.633 +  shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))";
  14.634 +proof -
  14.635 +  from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
  14.636    then obtain z where a: "a = of_int z" ..
  14.637    hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
  14.638      by (simp add: a)
  14.639 @@ -403,93 +436,98 @@
  14.640  qed
  14.641  
  14.642  lemma neg_number_of_BIT:
  14.643 -     "neg (number_of (w BIT x)::'a) = 
  14.644 -      neg (number_of w :: 'a::{ordered_idom,number_ring})"
  14.645 -by (simp add: neg_def number_of_eq Bin_simps double_less_0_iff
  14.646 -              Ints_odd_less_0 Ints_def split: bit.split)
  14.647 -
  14.648 +  "neg (number_of (w BIT x)::'a) = 
  14.649 +  neg (number_of w :: 'a::{ordered_idom,number_ring})"
  14.650 +  by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff
  14.651 +    Ints_odd_less_0 Ints_def split: bit.split)
  14.652  
  14.653 -text{*Less-Than or Equals*}
  14.654 +text {* Less-Than or Equals *}
  14.655 +
  14.656 +text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
  14.657  
  14.658 -text{*Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals*}
  14.659  lemmas le_number_of_eq_not_less =
  14.660 -       linorder_not_less [of "number_of w" "number_of v", symmetric, 
  14.661 -                          standard]
  14.662 +  linorder_not_less [of "number_of w" "number_of v", symmetric, 
  14.663 +  standard]
  14.664  
  14.665  lemma le_number_of_eq:
  14.666      "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
  14.667 -     = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"
  14.668 +     = (~ (neg (number_of (y + uminus x) :: 'a)))"
  14.669  by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
  14.670  
  14.671  
  14.672 -text{*Absolute value (@{term abs})*}
  14.673 +text {* Absolute value (@{term abs}) *}
  14.674  
  14.675  lemma abs_number_of:
  14.676 -     "abs(number_of x::'a::{ordered_idom,number_ring}) =
  14.677 -      (if number_of x < (0::'a) then -number_of x else number_of x)"
  14.678 -by (simp add: abs_if)
  14.679 +  "abs(number_of x::'a::{ordered_idom,number_ring}) =
  14.680 +   (if number_of x < (0::'a) then -number_of x else number_of x)"
  14.681 +  by (simp add: abs_if)
  14.682  
  14.683  
  14.684 -text{*Re-orientation of the equation nnn=x*}
  14.685 -lemma number_of_reorient: "(number_of w = x) = (x = number_of w)"
  14.686 -by auto
  14.687 +text {* Re-orientation of the equation nnn=x *}
  14.688  
  14.689 -
  14.690 +lemma number_of_reorient:
  14.691 +  "(number_of w = x) = (x = number_of w)"
  14.692 +  by auto
  14.693  
  14.694  
  14.695 -subsection{*Simplification of arithmetic operations on integer constants.*}
  14.696 +subsection {* Simplification of arithmetic operations on integer constants. *}
  14.697  
  14.698 -lemmas bin_arith_extra_simps = 
  14.699 -       number_of_add [symmetric]
  14.700 -       number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
  14.701 -       number_of_mult [symmetric]
  14.702 -       diff_number_of_eq abs_number_of 
  14.703 +lemmas arith_extra_simps = 
  14.704 +  number_of_add [symmetric]
  14.705 +  number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
  14.706 +  number_of_mult [symmetric]
  14.707 +  diff_number_of_eq abs_number_of 
  14.708 +
  14.709 +text {*
  14.710 +  For making a minimal simpset, one must include these default simprules.
  14.711 +  Also include @{text simp_thms}.
  14.712 +*}
  14.713  
  14.714 -text{*For making a minimal simpset, one must include these default simprules.
  14.715 -  Also include @{text simp_thms} *}
  14.716 -lemmas bin_arith_simps = 
  14.717 -       Numeral.bit.distinct
  14.718 -       Pls_0_eq Min_1_eq
  14.719 -       bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
  14.720 -       bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
  14.721 -       bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
  14.722 -       bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
  14.723 -       bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0 
  14.724 -       bin_add_Pls_right bin_add_Min_right
  14.725 -       abs_zero abs_one bin_arith_extra_simps
  14.726 +lemmas arith_simps = 
  14.727 +  bit.distinct
  14.728 +  Pls_0_eq Min_1_eq
  14.729 +  pred_Pls pred_Min pred_1 pred_0
  14.730 +  succ_Pls succ_Min succ_1 succ_0
  14.731 +  add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
  14.732 +  minus_Pls minus_Min minus_1 minus_0
  14.733 +  mult_Pls mult_Min mult_num1 mult_num0 
  14.734 +  add_Pls_right add_Min_right
  14.735 +  abs_zero abs_one arith_extra_simps
  14.736  
  14.737 -text{*Simplification of relational operations*}
  14.738 -lemmas bin_rel_simps = 
  14.739 -       eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
  14.740 -       iszero_number_of_0 iszero_number_of_1
  14.741 -       less_number_of_eq_neg
  14.742 -       not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
  14.743 -       neg_number_of_Min neg_number_of_BIT
  14.744 -       le_number_of_eq
  14.745 +text {* Simplification of relational operations *}
  14.746  
  14.747 -declare bin_arith_extra_simps [simp]
  14.748 -declare bin_rel_simps [simp]
  14.749 +lemmas rel_simps = 
  14.750 +  eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
  14.751 +  iszero_number_of_0 iszero_number_of_1
  14.752 +  less_number_of_eq_neg
  14.753 +  not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
  14.754 +  neg_number_of_Min neg_number_of_BIT
  14.755 +  le_number_of_eq
  14.756 +
  14.757 +declare arith_extra_simps [simp]
  14.758 +declare rel_simps [simp]
  14.759  
  14.760  
  14.761 -subsection{*Simplification of arithmetic when nested to the right*}
  14.762 +subsection {* Simplification of arithmetic when nested to the right. *}
  14.763  
  14.764  lemma add_number_of_left [simp]:
  14.765 -     "number_of v + (number_of w + z) =
  14.766 -      (number_of(bin_add v w) + z::'a::number_ring)"
  14.767 -by (simp add: add_assoc [symmetric])
  14.768 +  "number_of v + (number_of w + z) =
  14.769 +   (number_of(v + w) + z::'a::number_ring)"
  14.770 +  by (simp add: add_assoc [symmetric])
  14.771  
  14.772  lemma mult_number_of_left [simp]:
  14.773 -    "number_of v * (number_of w * z) =
  14.774 -     (number_of(bin_mult v w) * z::'a::number_ring)"
  14.775 -by (simp add: mult_assoc [symmetric])
  14.776 +  "number_of v * (number_of w * z) =
  14.777 +   (number_of(v * w) * z::'a::number_ring)"
  14.778 +  by (simp add: mult_assoc [symmetric])
  14.779  
  14.780  lemma add_number_of_diff1:
  14.781 -    "number_of v + (number_of w - c) = 
  14.782 -     number_of(bin_add v w) - (c::'a::number_ring)"
  14.783 -by (simp add: diff_minus add_number_of_left)
  14.784 +  "number_of v + (number_of w - c) = 
  14.785 +  number_of(v + w) - (c::'a::number_ring)"
  14.786 +  by (simp add: diff_minus add_number_of_left)
  14.787  
  14.788 -lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) =
  14.789 -     number_of (bin_add v (bin_minus w)) + (c::'a::number_ring)"
  14.790 +lemma add_number_of_diff2 [simp]:
  14.791 +  "number_of v + (c - number_of w) =
  14.792 +   number_of (v + uminus w) + (c::'a::number_ring)"
  14.793  apply (subst diff_number_of_eq [symmetric])
  14.794  apply (simp only: compare_rls)
  14.795  done
    15.1 --- a/src/HOL/Integ/Presburger.thy	Wed Sep 06 10:01:27 2006 +0200
    15.2 +++ b/src/HOL/Integ/Presburger.thy	Wed Sep 06 13:48:02 2006 +0200
    15.3 @@ -992,7 +992,8 @@
    15.4  lemma not_true_eq_false: "(~ True) = False" by simp
    15.5  
    15.6  
    15.7 -lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
    15.8 +lemma int_eq_number_of_eq:
    15.9 +  "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
   15.10    by simp
   15.11  lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" 
   15.12    by (simp only: iszero_number_of_Pls)
   15.13 @@ -1006,7 +1007,7 @@
   15.14  lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)" 
   15.15    by simp
   15.16  
   15.17 -lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
   15.18 +lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
   15.19    by simp
   15.20  
   15.21  lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))" 
   15.22 @@ -1018,18 +1019,20 @@
   15.23  lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
   15.24    by simp
   15.25  
   15.26 -lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
   15.27 +lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
   15.28    by simp
   15.29 -lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)"
   15.30 +lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
   15.31    by simp
   15.32  
   15.33 -lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))"
   15.34 +lemma int_number_of_diff_sym:
   15.35 +  "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
   15.36    by simp
   15.37  
   15.38 -lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)"
   15.39 +lemma int_number_of_mult_sym:
   15.40 +  "((number_of v)::int) * number_of w = number_of (v * w)"
   15.41    by simp
   15.42  
   15.43 -lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)"
   15.44 +lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
   15.45    by simp
   15.46  lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
   15.47    by simp
    16.1 --- a/src/HOL/Integ/int_arith1.ML	Wed Sep 06 10:01:27 2006 +0200
    16.2 +++ b/src/HOL/Integ/int_arith1.ML	Wed Sep 06 13:48:02 2006 +0200
    16.3 @@ -7,90 +7,90 @@
    16.4  
    16.5  (** Misc ML bindings **)
    16.6  
    16.7 -val bin_succ_Pls = thm"bin_succ_Pls";
    16.8 -val bin_succ_Min = thm"bin_succ_Min";
    16.9 -val bin_succ_1 = thm"bin_succ_1";
   16.10 -val bin_succ_0 = thm"bin_succ_0";
   16.11 +val succ_Pls = thm "succ_Pls";
   16.12 +val succ_Min = thm "succ_Min";
   16.13 +val succ_1 = thm "succ_1";
   16.14 +val succ_0 = thm "succ_0";
   16.15  
   16.16 -val bin_pred_Pls = thm"bin_pred_Pls";
   16.17 -val bin_pred_Min = thm"bin_pred_Min";
   16.18 -val bin_pred_1 = thm"bin_pred_1";
   16.19 -val bin_pred_0 = thm"bin_pred_0";
   16.20 +val pred_Pls = thm "pred_Pls";
   16.21 +val pred_Min = thm "pred_Min";
   16.22 +val pred_1 = thm "pred_1";
   16.23 +val pred_0 = thm "pred_0";
   16.24  
   16.25 -val bin_minus_Pls = thm"bin_minus_Pls";
   16.26 -val bin_minus_Min = thm"bin_minus_Min";
   16.27 -val bin_minus_1 = thm"bin_minus_1";
   16.28 -val bin_minus_0 = thm"bin_minus_0";
   16.29 +val minus_Pls = thm "minus_Pls";
   16.30 +val minus_Min = thm "minus_Min";
   16.31 +val minus_1 = thm "minus_1";
   16.32 +val minus_0 = thm "minus_0";
   16.33  
   16.34 -val bin_add_Pls = thm"bin_add_Pls";
   16.35 -val bin_add_Min = thm"bin_add_Min";
   16.36 -val bin_add_BIT_11 = thm"bin_add_BIT_11";
   16.37 -val bin_add_BIT_10 = thm"bin_add_BIT_10";
   16.38 -val bin_add_BIT_0 = thm"bin_add_BIT_0";
   16.39 -val bin_add_Pls_right = thm"bin_add_Pls_right";
   16.40 -val bin_add_Min_right = thm"bin_add_Min_right";
   16.41 +val add_Pls = thm "add_Pls";
   16.42 +val add_Min = thm "add_Min";
   16.43 +val add_BIT_11 = thm "add_BIT_11";
   16.44 +val add_BIT_10 = thm "add_BIT_10";
   16.45 +val add_BIT_0 = thm "add_BIT_0";
   16.46 +val add_Pls_right = thm "add_Pls_right";
   16.47 +val add_Min_right = thm "add_Min_right";
   16.48  
   16.49 -val bin_mult_Pls = thm"bin_mult_Pls";
   16.50 -val bin_mult_Min = thm"bin_mult_Min";
   16.51 -val bin_mult_1 = thm"bin_mult_1";
   16.52 -val bin_mult_0 = thm"bin_mult_0";
   16.53 +val mult_Pls = thm "mult_Pls";
   16.54 +val mult_Min = thm "mult_Min";
   16.55 +val mult_num1 = thm "mult_num1";
   16.56 +val mult_num0 = thm "mult_num0";
   16.57  
   16.58  val neg_def = thm "neg_def";
   16.59  val iszero_def = thm "iszero_def";
   16.60  
   16.61 -val number_of_succ = thm"number_of_succ";
   16.62 -val number_of_pred = thm"number_of_pred";
   16.63 -val number_of_minus = thm"number_of_minus";
   16.64 -val number_of_add = thm"number_of_add";
   16.65 -val diff_number_of_eq = thm"diff_number_of_eq";
   16.66 -val number_of_mult = thm"number_of_mult";
   16.67 -val double_number_of_BIT = thm"double_number_of_BIT";
   16.68 -val numeral_0_eq_0 = thm"numeral_0_eq_0";
   16.69 -val numeral_1_eq_1 = thm"numeral_1_eq_1";
   16.70 -val numeral_m1_eq_minus_1 = thm"numeral_m1_eq_minus_1";
   16.71 -val mult_minus1 = thm"mult_minus1";
   16.72 -val mult_minus1_right = thm"mult_minus1_right";
   16.73 -val minus_number_of_mult = thm"minus_number_of_mult";
   16.74 -val zero_less_nat_eq = thm"zero_less_nat_eq";
   16.75 -val eq_number_of_eq = thm"eq_number_of_eq";
   16.76 -val iszero_number_of_Pls = thm"iszero_number_of_Pls";
   16.77 -val nonzero_number_of_Min = thm"nonzero_number_of_Min";
   16.78 -val iszero_number_of_BIT = thm"iszero_number_of_BIT";
   16.79 -val iszero_number_of_0 = thm"iszero_number_of_0";
   16.80 -val iszero_number_of_1 = thm"iszero_number_of_1";
   16.81 -val less_number_of_eq_neg = thm"less_number_of_eq_neg";
   16.82 -val le_number_of_eq = thm"le_number_of_eq";
   16.83 -val not_neg_number_of_Pls = thm"not_neg_number_of_Pls";
   16.84 -val neg_number_of_Min = thm"neg_number_of_Min";
   16.85 -val neg_number_of_BIT = thm"neg_number_of_BIT";
   16.86 -val le_number_of_eq_not_less = thm"le_number_of_eq_not_less";
   16.87 -val abs_number_of = thm"abs_number_of";
   16.88 -val number_of_reorient = thm"number_of_reorient";
   16.89 -val add_number_of_left = thm"add_number_of_left";
   16.90 -val mult_number_of_left = thm"mult_number_of_left";
   16.91 -val add_number_of_diff1 = thm"add_number_of_diff1";
   16.92 -val add_number_of_diff2 = thm"add_number_of_diff2";
   16.93 -val less_iff_diff_less_0 = thm"less_iff_diff_less_0";
   16.94 -val eq_iff_diff_eq_0 = thm"eq_iff_diff_eq_0";
   16.95 -val le_iff_diff_le_0 = thm"le_iff_diff_le_0";
   16.96 +val number_of_succ = thm "number_of_succ";
   16.97 +val number_of_pred = thm "number_of_pred";
   16.98 +val number_of_minus = thm "number_of_minus";
   16.99 +val number_of_add = thm "number_of_add";
  16.100 +val diff_number_of_eq = thm "diff_number_of_eq";
  16.101 +val number_of_mult = thm "number_of_mult";
  16.102 +val double_number_of_BIT = thm "double_number_of_BIT";
  16.103 +val numeral_0_eq_0 = thm "numeral_0_eq_0";
  16.104 +val numeral_1_eq_1 = thm "numeral_1_eq_1";
  16.105 +val numeral_m1_eq_minus_1 = thm "numeral_m1_eq_minus_1";
  16.106 +val mult_minus1 = thm "mult_minus1";
  16.107 +val mult_minus1_right = thm "mult_minus1_right";
  16.108 +val minus_number_of_mult = thm "minus_number_of_mult";
  16.109 +val zero_less_nat_eq = thm "zero_less_nat_eq";
  16.110 +val eq_number_of_eq = thm "eq_number_of_eq";
  16.111 +val iszero_number_of_Pls = thm "iszero_number_of_Pls";
  16.112 +val nonzero_number_of_Min = thm "nonzero_number_of_Min";
  16.113 +val iszero_number_of_BIT = thm "iszero_number_of_BIT";
  16.114 +val iszero_number_of_0 = thm "iszero_number_of_0";
  16.115 +val iszero_number_of_1 = thm "iszero_number_of_1";
  16.116 +val less_number_of_eq_neg = thm "less_number_of_eq_neg";
  16.117 +val le_number_of_eq = thm "le_number_of_eq";
  16.118 +val not_neg_number_of_Pls = thm "not_neg_number_of_Pls";
  16.119 +val neg_number_of_Min = thm "neg_number_of_Min";
  16.120 +val neg_number_of_BIT = thm "neg_number_of_BIT";
  16.121 +val le_number_of_eq_not_less = thm "le_number_of_eq_not_less";
  16.122 +val abs_number_of = thm "abs_number_of";
  16.123 +val number_of_reorient = thm "number_of_reorient";
  16.124 +val add_number_of_left = thm "add_number_of_left";
  16.125 +val mult_number_of_left = thm "mult_number_of_left";
  16.126 +val add_number_of_diff1 = thm "add_number_of_diff1";
  16.127 +val add_number_of_diff2 = thm "add_number_of_diff2";
  16.128 +val less_iff_diff_less_0 = thm "less_iff_diff_less_0";
  16.129 +val eq_iff_diff_eq_0 = thm "eq_iff_diff_eq_0";
  16.130 +val le_iff_diff_le_0 = thm "le_iff_diff_le_0";
  16.131  
  16.132 -val bin_arith_extra_simps = thms"bin_arith_extra_simps";
  16.133 -val bin_arith_simps = thms"bin_arith_simps";
  16.134 -val bin_rel_simps = thms"bin_rel_simps";
  16.135 +val arith_extra_simps = thms "arith_extra_simps";
  16.136 +val arith_simps = thms "arith_simps";
  16.137 +val rel_simps = thms "rel_simps";
  16.138  
  16.139  val zless_imp_add1_zle = thm "zless_imp_add1_zle";
  16.140  
  16.141 -val combine_common_factor = thm"combine_common_factor";
  16.142 -val eq_add_iff1 = thm"eq_add_iff1";
  16.143 -val eq_add_iff2 = thm"eq_add_iff2";
  16.144 -val less_add_iff1 = thm"less_add_iff1";
  16.145 -val less_add_iff2 = thm"less_add_iff2";
  16.146 -val le_add_iff1 = thm"le_add_iff1";
  16.147 -val le_add_iff2 = thm"le_add_iff2";
  16.148 +val combine_common_factor = thm "combine_common_factor";
  16.149 +val eq_add_iff1 = thm "eq_add_iff1";
  16.150 +val eq_add_iff2 = thm "eq_add_iff2";
  16.151 +val less_add_iff1 = thm "less_add_iff1";
  16.152 +val less_add_iff2 = thm "less_add_iff2";
  16.153 +val le_add_iff1 = thm "le_add_iff1";
  16.154 +val le_add_iff2 = thm "le_add_iff2";
  16.155  
  16.156 -val arith_special = thms"arith_special";
  16.157 +val arith_special = thms "arith_special";
  16.158  
  16.159 -structure Bin_Simprocs =
  16.160 +structure Int_Numeral_Base_Simprocs =
  16.161    struct
  16.162    fun prove_conv tacs ctxt (_: thm list) (t, u) =
  16.163      if t aconv u then NONE
  16.164 @@ -133,13 +133,13 @@
  16.165  
  16.166  
  16.167  Addsimps arith_special;
  16.168 -Addsimprocs [Bin_Simprocs.reorient_simproc];
  16.169 +Addsimprocs [Int_Numeral_Base_Simprocs.reorient_simproc];
  16.170  
  16.171  
  16.172  structure Int_Numeral_Simprocs =
  16.173  struct
  16.174  
  16.175 -(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in simprocs
  16.176 +(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic in Int_Numeral_Base_Simprocs
  16.177    isn't complicated by the abstract 0 and 1.*)
  16.178  val numeral_syms = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym];
  16.179  
  16.180 @@ -175,7 +175,7 @@
  16.181  
  16.182  fun numtermless tu = (numterm_ord tu = LESS);
  16.183  
  16.184 -(*Defined in this file, but perhaps needed only for simprocs of type nat.*)
  16.185 +(*Defined in this file, but perhaps needed only for Int_Numeral_Base_Simprocs of type nat.*)
  16.186  val num_ss = HOL_ss settermless numtermless;
  16.187  
  16.188  
  16.189 @@ -273,20 +273,20 @@
  16.190  val mult_1s = thms "mult_1s";
  16.191  
  16.192  (*To perform binary arithmetic.  The "left" rewriting handles patterns
  16.193 -  created by the simprocs, such as 3 * (5 * x). *)
  16.194 -val bin_simps = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym,
  16.195 +  created by the Int_Numeral_Base_Simprocs, such as 3 * (5 * x). *)
  16.196 +val simps = [numeral_0_eq_0 RS sym, numeral_1_eq_1 RS sym,
  16.197                   add_number_of_left, mult_number_of_left] @
  16.198 -                bin_arith_simps @ bin_rel_simps;
  16.199 +                arith_simps @ rel_simps;
  16.200  
  16.201  (*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms
  16.202    during re-arrangement*)
  16.203 -val non_add_bin_simps =
  16.204 -  subtract Thm.eq_thm [add_number_of_left, number_of_add RS sym] bin_simps;
  16.205 +val non_add_simps =
  16.206 +  subtract Thm.eq_thm [add_number_of_left, number_of_add RS sym] simps;
  16.207  
  16.208  (*To evaluate binary negations of coefficients*)
  16.209  val minus_simps = [numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,
  16.210 -                   bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
  16.211 -                   bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
  16.212 +                   minus_1, minus_0, minus_Pls, minus_Min,
  16.213 +                   pred_1, pred_0, pred_Pls, pred_Min];
  16.214  
  16.215  (*To let us treat subtraction as addition*)
  16.216  val diff_simps = [diff_minus, minus_add_distrib, minus_minus];
  16.217 @@ -322,14 +322,14 @@
  16.218  
  16.219    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
  16.220      diff_simps @ minus_simps @ add_ac
  16.221 -  val norm_ss2 = num_ss addsimps non_add_bin_simps @ mult_minus_simps
  16.222 +  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
  16.223    val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
  16.224    fun norm_tac ss =
  16.225      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
  16.226      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
  16.227      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
  16.228  
  16.229 -  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps
  16.230 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
  16.231    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
  16.232    val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
  16.233    end;
  16.234 @@ -337,7 +337,7 @@
  16.235  
  16.236  structure EqCancelNumerals = CancelNumeralsFun
  16.237   (open CancelNumeralsCommon
  16.238 -  val prove_conv = Bin_Simprocs.prove_conv
  16.239 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  16.240    val mk_bal   = HOLogic.mk_eq
  16.241    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
  16.242    val bal_add1 = eq_add_iff1 RS trans
  16.243 @@ -346,7 +346,7 @@
  16.244  
  16.245  structure LessCancelNumerals = CancelNumeralsFun
  16.246   (open CancelNumeralsCommon
  16.247 -  val prove_conv = Bin_Simprocs.prove_conv
  16.248 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  16.249    val mk_bal   = HOLogic.mk_binrel "Orderings.less"
  16.250    val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT
  16.251    val bal_add1 = less_add_iff1 RS trans
  16.252 @@ -355,7 +355,7 @@
  16.253  
  16.254  structure LeCancelNumerals = CancelNumeralsFun
  16.255   (open CancelNumeralsCommon
  16.256 -  val prove_conv = Bin_Simprocs.prove_conv
  16.257 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  16.258    val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
  16.259    val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT
  16.260    val bal_add1 = le_add_iff1 RS trans
  16.261 @@ -363,7 +363,7 @@
  16.262  );
  16.263  
  16.264  val cancel_numerals =
  16.265 -  map Bin_Simprocs.prep_simproc
  16.266 +  map Int_Numeral_Base_Simprocs.prep_simproc
  16.267     [("inteq_cancel_numerals",
  16.268       ["(l::'a::number_ring) + m = n",
  16.269        "(l::'a::number_ring) = m + n",
  16.270 @@ -398,19 +398,19 @@
  16.271    val mk_coeff          = mk_coeff
  16.272    val dest_coeff        = dest_coeff 1
  16.273    val left_distrib      = combine_common_factor RS trans
  16.274 -  val prove_conv        = Bin_Simprocs.prove_conv_nohyps
  16.275 +  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
  16.276    val trans_tac         = fn _ => trans_tac
  16.277  
  16.278    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
  16.279      diff_simps @ minus_simps @ add_ac
  16.280 -  val norm_ss2 = num_ss addsimps non_add_bin_simps @ mult_minus_simps
  16.281 +  val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps
  16.282    val norm_ss3 = num_ss addsimps minus_from_mult_simps @ add_ac @ mult_ac
  16.283    fun norm_tac ss =
  16.284      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
  16.285      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
  16.286      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
  16.287  
  16.288 -  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps
  16.289 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ simps
  16.290    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
  16.291    val simplify_meta_eq = simplify_meta_eq (add_0s @ mult_1s)
  16.292    end;
  16.293 @@ -418,7 +418,7 @@
  16.294  structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
  16.295  
  16.296  val combine_numerals =
  16.297 -  Bin_Simprocs.prep_simproc
  16.298 +  Int_Numeral_Base_Simprocs.prep_simproc
  16.299      ("int_combine_numerals", 
  16.300       ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], 
  16.301       K CombineNumerals.proc);
  16.302 @@ -479,7 +479,7 @@
  16.303  structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
  16.304  
  16.305  val assoc_fold_simproc =
  16.306 -  Bin_Simprocs.prep_simproc
  16.307 +  Int_Numeral_Base_Simprocs.prep_simproc
  16.308     ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
  16.309      K Semiring_Times_Assoc.proc);
  16.310  
  16.311 @@ -503,10 +503,10 @@
  16.312  
  16.313  (* reduce contradictory <= to False *)
  16.314  val add_rules =
  16.315 -    simp_thms @ bin_arith_simps @ bin_rel_simps @ arith_special @
  16.316 +    simp_thms @ arith_simps @ rel_simps @ arith_special @
  16.317      [neg_le_iff_le, numeral_0_eq_0, numeral_1_eq_1,
  16.318       minus_zero, diff_minus, left_minus, right_minus,
  16.319 -     mult_zero_left, mult_zero_right, mult_1, mult_1_right,
  16.320 +     mult_zero_left, mult_zero_right, mult_num1, mult_1_right,
  16.321       minus_mult_left RS sym, minus_mult_right RS sym,
  16.322       minus_add_distrib, minus_minus, mult_assoc,
  16.323       of_nat_0, of_nat_1, of_nat_Suc, of_nat_add, of_nat_mult,
  16.324 @@ -515,7 +515,7 @@
  16.325  val nat_inj_thms = [zle_int RS iffD2,
  16.326                      int_int_eq RS iffD2]
  16.327  
  16.328 -val simprocs = [assoc_fold_simproc, Int_Numeral_Simprocs.combine_numerals]@
  16.329 +val Int_Numeral_Base_Simprocs = [assoc_fold_simproc, Int_Numeral_Simprocs.combine_numerals]@
  16.330                 Int_Numeral_Simprocs.cancel_numerals
  16.331  
  16.332  in
  16.333 @@ -528,7 +528,7 @@
  16.334      lessD = lessD @ [zless_imp_add1_zle],
  16.335      neqE = neqE,
  16.336      simpset = simpset addsimps add_rules
  16.337 -                      addsimprocs simprocs
  16.338 +                      addsimprocs Int_Numeral_Base_Simprocs
  16.339                        addcongs [if_weak_cong]}) #>
  16.340    arith_inj_const ("NatArith.of_nat", HOLogic.natT --> HOLogic.intT) #>
  16.341    arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT) #>
    17.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Wed Sep 06 10:01:27 2006 +0200
    17.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Wed Sep 06 13:48:02 2006 +0200
    17.3 @@ -45,25 +45,25 @@
    17.4    val trans_tac         = fn _ => trans_tac
    17.5  
    17.6    val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
    17.7 -  val norm_ss2 = HOL_ss addsimps bin_simps@mult_minus_simps
    17.8 +  val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
    17.9    val norm_ss3 = HOL_ss addsimps mult_ac
   17.10    fun norm_tac ss =
   17.11      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   17.12      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   17.13      THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3))
   17.14  
   17.15 -  val numeral_simp_ss = HOL_ss addsimps rel_number_of @ bin_simps
   17.16 +  val numeral_simp_ss = HOL_ss addsimps rel_number_of @ simps
   17.17    fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   17.18    val simplify_meta_eq = 
   17.19  	Int_Numeral_Simprocs.simplify_meta_eq
   17.20  	     [add_0, add_0_right,
   17.21 -	      mult_zero_left, mult_zero_right, mult_1, mult_1_right];
   17.22 +	      mult_zero_left, mult_zero_right, mult_num1, mult_1_right];
   17.23    end
   17.24  
   17.25  (*Version for integer division*)
   17.26  structure DivCancelNumeralFactor = CancelNumeralFactorFun
   17.27   (open CancelNumeralFactorCommon
   17.28 -  val prove_conv = Bin_Simprocs.prove_conv
   17.29 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   17.30    val mk_bal   = HOLogic.mk_binop "Divides.op div"
   17.31    val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
   17.32    val cancel = int_mult_div_cancel1 RS trans
   17.33 @@ -73,7 +73,7 @@
   17.34  (*Version for fields*)
   17.35  structure FieldDivCancelNumeralFactor = CancelNumeralFactorFun
   17.36   (open CancelNumeralFactorCommon
   17.37 -  val prove_conv = Bin_Simprocs.prove_conv
   17.38 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   17.39    val mk_bal   = HOLogic.mk_binop "HOL.divide"
   17.40    val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
   17.41    val cancel = mult_divide_cancel_left RS trans
   17.42 @@ -83,7 +83,7 @@
   17.43  (*Version for ordered rings: mult_cancel_left requires an ordering*)
   17.44  structure EqCancelNumeralFactor = CancelNumeralFactorFun
   17.45   (open CancelNumeralFactorCommon
   17.46 -  val prove_conv = Bin_Simprocs.prove_conv
   17.47 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   17.48    val mk_bal   = HOLogic.mk_eq
   17.49    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   17.50    val cancel = mult_cancel_left RS trans
   17.51 @@ -93,7 +93,7 @@
   17.52  (*Version for (unordered) fields*)
   17.53  structure FieldEqCancelNumeralFactor = CancelNumeralFactorFun
   17.54   (open CancelNumeralFactorCommon
   17.55 -  val prove_conv = Bin_Simprocs.prove_conv
   17.56 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   17.57    val mk_bal   = HOLogic.mk_eq
   17.58    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
   17.59    val cancel = field_mult_cancel_left RS trans
   17.60 @@ -102,7 +102,7 @@
   17.61  
   17.62  structure LessCancelNumeralFactor = CancelNumeralFactorFun
   17.63   (open CancelNumeralFactorCommon
   17.64 -  val prove_conv = Bin_Simprocs.prove_conv
   17.65 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   17.66    val mk_bal   = HOLogic.mk_binrel "Orderings.less"
   17.67    val dest_bal = HOLogic.dest_bin "Orderings.less" Term.dummyT
   17.68    val cancel = mult_less_cancel_left RS trans
   17.69 @@ -111,7 +111,7 @@
   17.70  
   17.71  structure LeCancelNumeralFactor = CancelNumeralFactorFun
   17.72   (open CancelNumeralFactorCommon
   17.73 -  val prove_conv = Bin_Simprocs.prove_conv
   17.74 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   17.75    val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
   17.76    val dest_bal = HOLogic.dest_bin "Orderings.less_eq" Term.dummyT
   17.77    val cancel = mult_le_cancel_left RS trans
   17.78 @@ -119,7 +119,7 @@
   17.79  )
   17.80  
   17.81  val ring_cancel_numeral_factors =
   17.82 -  map Bin_Simprocs.prep_simproc
   17.83 +  map Int_Numeral_Base_Simprocs.prep_simproc
   17.84     [("ring_eq_cancel_numeral_factor",
   17.85       ["(l::'a::{ordered_idom,number_ring}) * m = n",
   17.86        "(l::'a::{ordered_idom,number_ring}) = m * n"],
   17.87 @@ -138,7 +138,7 @@
   17.88  
   17.89  
   17.90  val field_cancel_numeral_factors =
   17.91 -  map Bin_Simprocs.prep_simproc
   17.92 +  map Int_Numeral_Base_Simprocs.prep_simproc
   17.93     [("field_eq_cancel_numeral_factor",
   17.94       ["(l::'a::{field,number_ring}) * m = n",
   17.95        "(l::'a::{field,number_ring}) = m * n"],
   17.96 @@ -261,7 +261,7 @@
   17.97    rat_arith.ML works for all fields.*)
   17.98  structure EqCancelFactor = ExtractCommonTermFun
   17.99   (open CancelFactorCommon
  17.100 -  val prove_conv = Bin_Simprocs.prove_conv
  17.101 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  17.102    val mk_bal   = HOLogic.mk_eq
  17.103    val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
  17.104    val simplify_meta_eq  = cancel_simplify_meta_eq mult_cancel_left
  17.105 @@ -271,14 +271,14 @@
  17.106    rat_arith.ML works for all fields, using real division (/).*)
  17.107  structure DivideCancelFactor = ExtractCommonTermFun
  17.108   (open CancelFactorCommon
  17.109 -  val prove_conv = Bin_Simprocs.prove_conv
  17.110 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  17.111    val mk_bal   = HOLogic.mk_binop "Divides.op div"
  17.112    val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
  17.113    val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
  17.114  );
  17.115  
  17.116  val int_cancel_factor =
  17.117 -  map Bin_Simprocs.prep_simproc
  17.118 +  map Int_Numeral_Base_Simprocs.prep_simproc
  17.119     [("ring_eq_cancel_factor", ["(l::int) * m = n", "(l::int) = m * n"],
  17.120      K EqCancelFactor.proc),
  17.121      ("int_divide_cancel_factor", ["((l::int) * m) div n", "(l::int) div (m*n)"],
  17.122 @@ -288,7 +288,7 @@
  17.123  
  17.124  structure FieldEqCancelFactor = ExtractCommonTermFun
  17.125   (open CancelFactorCommon
  17.126 -  val prove_conv = Bin_Simprocs.prove_conv
  17.127 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  17.128    val mk_bal   = HOLogic.mk_eq
  17.129    val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
  17.130    val simplify_meta_eq  = cancel_simplify_meta_eq field_mult_cancel_left
  17.131 @@ -296,7 +296,7 @@
  17.132  
  17.133  structure FieldDivideCancelFactor = ExtractCommonTermFun
  17.134   (open CancelFactorCommon
  17.135 -  val prove_conv = Bin_Simprocs.prove_conv
  17.136 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  17.137    val mk_bal   = HOLogic.mk_binop "HOL.divide"
  17.138    val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
  17.139    val simplify_meta_eq  = cancel_simplify_meta_eq mult_divide_cancel_eq_if
  17.140 @@ -305,7 +305,7 @@
  17.141  (*The number_ring class is necessary because the simprocs refer to the
  17.142    binary number 1.  FIXME: probably they could use 1 instead.*)
  17.143  val field_cancel_factor =
  17.144 -  map Bin_Simprocs.prep_simproc
  17.145 +  map Int_Numeral_Base_Simprocs.prep_simproc
  17.146     [("field_eq_cancel_factor",
  17.147       ["(l::'a::{field,number_ring}) * m = n",
  17.148        "(l::'a::{field,number_ring}) = m * n"],
    18.1 --- a/src/HOL/Integ/nat_simprocs.ML	Wed Sep 06 10:01:27 2006 +0200
    18.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Wed Sep 06 13:48:02 2006 +0200
    18.3 @@ -64,7 +64,7 @@
    18.4        mult_nat_number_of, nat_number_of_mult_left, 
    18.5        less_nat_number_of, 
    18.6        Let_number_of, nat_number_of] @
    18.7 -     bin_arith_simps @ bin_rel_simps;
    18.8 +     arith_simps @ rel_simps;
    18.9  
   18.10  fun prep_simproc (name, pats, proc) =
   18.11    Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
   18.12 @@ -182,7 +182,7 @@
   18.13  
   18.14  structure EqCancelNumerals = CancelNumeralsFun
   18.15   (open CancelNumeralsCommon
   18.16 -  val prove_conv = Bin_Simprocs.prove_conv
   18.17 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   18.18    val mk_bal   = HOLogic.mk_eq
   18.19    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   18.20    val bal_add1 = nat_eq_add_iff1 RS trans
   18.21 @@ -191,7 +191,7 @@
   18.22  
   18.23  structure LessCancelNumerals = CancelNumeralsFun
   18.24   (open CancelNumeralsCommon
   18.25 -  val prove_conv = Bin_Simprocs.prove_conv
   18.26 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   18.27    val mk_bal   = HOLogic.mk_binrel "Orderings.less"
   18.28    val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
   18.29    val bal_add1 = nat_less_add_iff1 RS trans
   18.30 @@ -200,7 +200,7 @@
   18.31  
   18.32  structure LeCancelNumerals = CancelNumeralsFun
   18.33   (open CancelNumeralsCommon
   18.34 -  val prove_conv = Bin_Simprocs.prove_conv
   18.35 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   18.36    val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
   18.37    val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
   18.38    val bal_add1 = nat_le_add_iff1 RS trans
   18.39 @@ -209,7 +209,7 @@
   18.40  
   18.41  structure DiffCancelNumerals = CancelNumeralsFun
   18.42   (open CancelNumeralsCommon
   18.43 -  val prove_conv = Bin_Simprocs.prove_conv
   18.44 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   18.45    val mk_bal   = HOLogic.mk_binop "HOL.minus"
   18.46    val dest_bal = HOLogic.dest_bin "HOL.minus" HOLogic.natT
   18.47    val bal_add1 = nat_diff_add_eq1 RS trans
   18.48 @@ -251,7 +251,7 @@
   18.49    val mk_coeff          = mk_coeff
   18.50    val dest_coeff        = dest_coeff
   18.51    val left_distrib      = left_add_mult_distrib RS trans
   18.52 -  val prove_conv        = Bin_Simprocs.prove_conv_nohyps
   18.53 +  val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
   18.54    val trans_tac         = fn _ => trans_tac
   18.55  
   18.56    val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [Suc_eq_add_numeral_1] @ add_ac
   18.57 @@ -293,7 +293,7 @@
   18.58  
   18.59  structure DivCancelNumeralFactor = CancelNumeralFactorFun
   18.60   (open CancelNumeralFactorCommon
   18.61 -  val prove_conv = Bin_Simprocs.prove_conv
   18.62 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   18.63    val mk_bal   = HOLogic.mk_binop "Divides.op div"
   18.64    val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
   18.65    val cancel = nat_mult_div_cancel1 RS trans
   18.66 @@ -302,7 +302,7 @@
   18.67  
   18.68  structure EqCancelNumeralFactor = CancelNumeralFactorFun
   18.69   (open CancelNumeralFactorCommon
   18.70 -  val prove_conv = Bin_Simprocs.prove_conv
   18.71 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   18.72    val mk_bal   = HOLogic.mk_eq
   18.73    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   18.74    val cancel = nat_mult_eq_cancel1 RS trans
   18.75 @@ -311,7 +311,7 @@
   18.76  
   18.77  structure LessCancelNumeralFactor = CancelNumeralFactorFun
   18.78   (open CancelNumeralFactorCommon
   18.79 -  val prove_conv = Bin_Simprocs.prove_conv
   18.80 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   18.81    val mk_bal   = HOLogic.mk_binrel "Orderings.less"
   18.82    val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
   18.83    val cancel = nat_mult_less_cancel1 RS trans
   18.84 @@ -320,7 +320,7 @@
   18.85  
   18.86  structure LeCancelNumeralFactor = CancelNumeralFactorFun
   18.87   (open CancelNumeralFactorCommon
   18.88 -  val prove_conv = Bin_Simprocs.prove_conv
   18.89 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   18.90    val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
   18.91    val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
   18.92    val cancel = nat_mult_le_cancel1 RS trans
   18.93 @@ -379,7 +379,7 @@
   18.94  
   18.95  structure EqCancelFactor = ExtractCommonTermFun
   18.96   (open CancelFactorCommon
   18.97 -  val prove_conv = Bin_Simprocs.prove_conv
   18.98 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   18.99    val mk_bal   = HOLogic.mk_eq
  18.100    val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
  18.101    val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_eq_cancel_disj
  18.102 @@ -387,7 +387,7 @@
  18.103  
  18.104  structure LessCancelFactor = ExtractCommonTermFun
  18.105   (open CancelFactorCommon
  18.106 -  val prove_conv = Bin_Simprocs.prove_conv
  18.107 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  18.108    val mk_bal   = HOLogic.mk_binrel "Orderings.less"
  18.109    val dest_bal = HOLogic.dest_bin "Orderings.less" HOLogic.natT
  18.110    val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_less_cancel_disj
  18.111 @@ -395,7 +395,7 @@
  18.112  
  18.113  structure LeCancelFactor = ExtractCommonTermFun
  18.114   (open CancelFactorCommon
  18.115 -  val prove_conv = Bin_Simprocs.prove_conv
  18.116 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  18.117    val mk_bal   = HOLogic.mk_binrel "Orderings.less_eq"
  18.118    val dest_bal = HOLogic.dest_bin "Orderings.less_eq" HOLogic.natT
  18.119    val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_le_cancel_disj
  18.120 @@ -403,7 +403,7 @@
  18.121  
  18.122  structure DivideCancelFactor = ExtractCommonTermFun
  18.123   (open CancelFactorCommon
  18.124 -  val prove_conv = Bin_Simprocs.prove_conv
  18.125 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
  18.126    val mk_bal   = HOLogic.mk_binop "Divides.op div"
  18.127    val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
  18.128    val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_div_cancel_disj
    19.1 --- a/src/HOL/Integ/presburger.ML	Wed Sep 06 10:01:27 2006 +0200
    19.2 +++ b/src/HOL/Integ/presburger.ML	Wed Sep 06 13:48:02 2006 +0200
    19.3 @@ -33,12 +33,12 @@
    19.4  val presburger_ss = simpset ();
    19.5  val binarith = map thm
    19.6    ["Pls_0_eq", "Min_1_eq",
    19.7 - "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
    19.8 -  "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
    19.9 -  "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
   19.10 -  "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
   19.11 -  "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
   19.12 -  "bin_add_Pls_right", "bin_add_Min_right"];
   19.13 + "pred_Pls","pred_Min","pred_1","pred_0",
   19.14 +  "succ_Pls", "succ_Min", "succ_1", "succ_0",
   19.15 +  "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10",
   19.16 +  "add_BIT_11", "minus_Pls", "minus_Min", "minus_1", 
   19.17 +  "minus_0", "mult_Pls", "mult_Min", "mult_num1", "mult_num0", 
   19.18 +  "add_Pls_right", "add_Min_right"];
   19.19   val intarithrel = 
   19.20       (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
   19.21  		"int_le_number_of_eq","int_iszero_number_of_0",
   19.22 @@ -116,7 +116,6 @@
   19.23  val bT = HOLogic.boolT;
   19.24  val bitT = HOLogic.bitT;
   19.25  val iT = HOLogic.intT;
   19.26 -val binT = HOLogic.binT;
   19.27  val nT = HOLogic.natT;
   19.28  
   19.29  (* Allowed Consts in formulae for presburger tactic*)
   19.30 @@ -162,11 +161,11 @@
   19.31  
   19.32     ("Numeral.bit.B0", bitT),
   19.33     ("Numeral.bit.B1", bitT),
   19.34 -   ("Numeral.Bit", binT --> bitT --> binT),
   19.35 -   ("Numeral.Pls", binT),
   19.36 -   ("Numeral.Min", binT),
   19.37 -   ("Numeral.number_of", binT --> iT),
   19.38 -   ("Numeral.number_of", binT --> nT),
   19.39 +   ("Numeral.Bit", iT --> bitT --> iT),
   19.40 +   ("Numeral.Pls", iT),
   19.41 +   ("Numeral.Min", iT),
   19.42 +   ("Numeral.number_of", iT --> iT),
   19.43 +   ("Numeral.number_of", iT --> nT),
   19.44     ("0", nT),
   19.45     ("0", iT),
   19.46     ("1", nT),
    20.1 --- a/src/HOL/Library/Word.thy	Wed Sep 06 10:01:27 2006 +0200
    20.2 +++ b/src/HOL/Library/Word.thy	Wed Sep 06 13:48:02 2006 +0200
    20.3 @@ -2513,92 +2513,12 @@
    20.4  lemma "nat_to_bv (number_of Numeral.Pls) = []"
    20.5    by simp
    20.6  
    20.7 -(***NO LONGER WORKS
    20.8  consts
    20.9 -  fast_nat_to_bv_helper :: "bin => bit list => bit list"
   20.10 +  fast_bv_to_nat_helper :: "[bit list, int] => int"
   20.11  
   20.12  primrec
   20.13 -  fast_nat_to_bv_Pls: "fast_nat_to_bv_helper Numeral.Pls res = res"
   20.14 -  fast_nat_to_bv_Bit: "fast_nat_to_bv_helper (w BIT b) res = fast_nat_to_bv_helper w ((if b then \<one> else \<zero>) # res)"
   20.15 -
   20.16 -lemma fast_nat_to_bv_def:
   20.17 -  assumes pos_w: "(0::int) \<le> number_of w"
   20.18 -  shows "nat_to_bv (number_of w) == norm_unsigned (fast_nat_to_bv_helper w [])"
   20.19 -proof -
   20.20 -  have h [rule_format]: "(0::int) \<le> number_of w ==> \<forall> l. norm_unsigned (nat_to_bv_helper (number_of w) l) = norm_unsigned (fast_nat_to_bv_helper w l)"
   20.21 -  proof (induct w,simp add: nat_to_bv_helper.simps,simp)
   20.22 -    fix bin b
   20.23 -    assume ind: "(0::int) \<le> number_of bin ==> \<forall> l. norm_unsigned (nat_to_bv_helper (number_of bin) l) = norm_unsigned (fast_nat_to_bv_helper bin l)"
   20.24 -    def qq == "number_of bin::int"
   20.25 -    assume posbb: "(0::int) \<le> number_of (bin BIT b)"
   20.26 -    hence indq [rule_format]: "\<forall> l. norm_unsigned (nat_to_bv_helper qq l) = norm_unsigned (fast_nat_to_bv_helper bin l)"
   20.27 -      apply (unfold qq_def)
   20.28 -      apply (rule ind)
   20.29 -      apply simp
   20.30 -      done
   20.31 -    from posbb
   20.32 -    have "0 \<le> qq"
   20.33 -      by (simp add: qq_def)
   20.34 -    with posbb
   20.35 -    show "\<forall> l. norm_unsigned (nat_to_bv_helper (number_of (bin BIT b)) l) = norm_unsigned (fast_nat_to_bv_helper (bin BIT b) l)"
   20.36 -      apply (subst pos_number_of)
   20.37 -      apply safe
   20.38 -      apply (fold qq_def)
   20.39 -      apply (cases "qq = 0")
   20.40 -      apply (simp add: nat_to_bv_helper.simps)
   20.41 -      apply (subst indq [symmetric])
   20.42 -      apply (subst indq [symmetric])
   20.43 -      apply (simp add: nat_to_bv_helper.simps)
   20.44 -      apply (subgoal_tac "0 < qq")
   20.45 -      prefer 2
   20.46 -      apply simp
   20.47 -      apply simp
   20.48 -      apply (subst indq [symmetric])
   20.49 -      apply (subst indq [symmetric])
   20.50 -      apply auto
   20.51 -      apply (simp only: nat_to_bv_helper.simps [of "2 * qq + 1"])
   20.52 -      apply simp
   20.53 -      apply safe
   20.54 -      apply (subgoal_tac "2 * qq + 1 ~= 2 * q")
   20.55 -      apply simp
   20.56 -      apply arith
   20.57 -      apply (subgoal_tac "(2 * qq + 1) div 2 = qq")
   20.58 -      apply simp
   20.59 -      apply (subst zdiv_zadd1_eq,simp)
   20.60 -      apply (simp only: nat_to_bv_helper.simps [of "2 * qq"])
   20.61 -      apply simp
   20.62 -      done
   20.63 -  qed
   20.64 -  from pos_w
   20.65 -  have "nat_to_bv (number_of w) = norm_unsigned (nat_to_bv (number_of w))"
   20.66 -    by simp
   20.67 -  also have "... = norm_unsigned (fast_nat_to_bv_helper w [])"
   20.68 -    apply (unfold nat_to_bv_def)
   20.69 -    apply (rule h)
   20.70 -    apply (rule pos_w)
   20.71 -    done
   20.72 -  finally show "nat_to_bv (number_of w) == norm_unsigned (fast_nat_to_bv_helper w [])"
   20.73 -    by simp
   20.74 -qed
   20.75 -
   20.76 -lemma fast_nat_to_bv_Bit0: "fast_nat_to_bv_helper (w BIT False) res = fast_nat_to_bv_helper w (\<zero> # res)"
   20.77 -  by simp
   20.78 -
   20.79 -lemma fast_nat_to_bv_Bit1: "fast_nat_to_bv_helper (w BIT True) res = fast_nat_to_bv_helper w (\<one> # res)"
   20.80 -  by simp
   20.81 -
   20.82 -declare fast_nat_to_bv_Bit [simp del]
   20.83 -declare fast_nat_to_bv_Bit0 [simp]
   20.84 -declare fast_nat_to_bv_Bit1 [simp]
   20.85 -****)
   20.86 -
   20.87 -
   20.88 -consts
   20.89 -  fast_bv_to_nat_helper :: "[bit list, bin] => bin"
   20.90 -
   20.91 -primrec
   20.92 -  fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] bin = bin"
   20.93 -  fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) bin = fast_bv_to_nat_helper bs (bin BIT (bit_case bit.B0 bit.B1 b))"
   20.94 +  fast_bv_to_nat_Nil: "fast_bv_to_nat_helper [] k = k"
   20.95 +  fast_bv_to_nat_Cons: "fast_bv_to_nat_helper (b#bs) k = fast_bv_to_nat_helper bs (k BIT (bit_case bit.B0 bit.B1 b))"
   20.96  
   20.97  lemma fast_bv_to_nat_Cons0: "fast_bv_to_nat_helper (\<zero>#bs) bin = fast_bv_to_nat_helper bs (bin BIT bit.B0)"
   20.98    by simp
    21.1 --- a/src/HOL/Library/word_setup.ML	Wed Sep 06 10:01:27 2006 +0200
    21.2 +++ b/src/HOL/Library/word_setup.ML	Wed Sep 06 13:48:02 2006 +0200
    21.3 @@ -27,7 +27,7 @@
    21.4  	    val fast2_th = PureThy.get_thm thy (Name "Word.fast_bv_to_nat_def")
    21.5   (*lcp**	    fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
    21.6  		if num_is_usable t
    21.7 -		then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("Numeral.bin",[]))),cterm_of sg t)] fast1_th)
    21.8 +		then SOME (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("IntDef.int",[]))),cterm_of sg t)] fast1_th)
    21.9  		else NONE
   21.10  	      | f _ _ _ = NONE **)
   21.11  	    fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) =
    22.1 --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Wed Sep 06 10:01:27 2006 +0200
    22.2 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Wed Sep 06 13:48:02 2006 +0200
    22.3 @@ -32,7 +32,7 @@
    22.4      val v_only_elem : vector -> int option
    22.5      val v_fold : ('a * (int * string) -> 'a) -> 'a -> vector -> 'a
    22.6      val m_fold : ('a * (int * vector) -> 'a) -> 'a -> matrix -> 'a
    22.7 -				   
    22.8 +
    22.9      val transpose_matrix : matrix -> matrix
   22.10  
   22.11      val cut_vector : int -> vector -> vector
   22.12 @@ -80,53 +80,27 @@
   22.13  
   22.14  val Cons_spvec_const = Const (term_Cons, spvec_elemT --> spvecT --> spvecT)
   22.15  val Cons_spmat_const = Const (term_Cons, spmat_elemT --> spmatT --> spmatT) 
   22.16 -			 
   22.17 +
   22.18  val float_const = Float.float_const
   22.19  
   22.20 -(*val float_const = Const (readterm "float", HOLogic.mk_prodT (HOLogic.intT, HOLogic.intT) --> HOLogic.realT)*)
   22.21 -		  
   22.22  val zero = IntInf.fromInt 0
   22.23  val minus_one = IntInf.fromInt ~1
   22.24  val two = IntInf.fromInt 2
   22.25 -	  
   22.26 +
   22.27  val mk_intinf = Float.mk_intinf
   22.28 -(*    let
   22.29 -	fun mk_bit n = if n = zero then HOLogic.false_const else HOLogic.true_const
   22.30 -								 
   22.31 -	fun bin_of n = 
   22.32 -	    if n = zero then HOLogic.pls_const
   22.33 -	    else if n = minus_one then HOLogic.min_const
   22.34 -	    else 
   22.35 -		let 
   22.36 -		    (*val (q,r) = IntInf.divMod (n, two): doesn't work in SML 10.0.7, but in newer versions!!!*)
   22.37 -	            val q = IntInf.div (n, two)
   22.38 -		    val r = IntInf.mod (n, two)
   22.39 -		in
   22.40 -		    HOLogic.bit_const $ bin_of q $ mk_bit r
   22.41 -		end
   22.42 -    in 
   22.43 -	HOLogic.number_of_const ty $ (bin_of n)
   22.44 -    end*)
   22.45  
   22.46  val mk_float  = Float.mk_float 
   22.47 -(*    float_const $ (HOLogic.mk_prod ((mk_intinf HOLogic.intT a), (mk_intinf HOLogic.intT b)))*)
   22.48  
   22.49  fun float2cterm (a,b) = cterm_of sg (mk_float (a,b))
   22.50  
   22.51  fun approx_value_term prec f = Float.approx_float prec (fn (x, y) => (f x, f y))
   22.52 -(*    let
   22.53 -	val (flower, fupper) = ExactFloatingPoint.approx_decstr_by_bin prec value
   22.54 -	val (flower, fupper) = (f flower, f fupper)
   22.55 -    in
   22.56 -	(mk_float flower, mk_float fupper)
   22.57 -    end*)
   22.58  
   22.59  fun approx_value prec pprt value = 
   22.60 -    let
   22.61 -	val (flower, fupper) = approx_value_term prec pprt value			       
   22.62 -    in
   22.63 -	(cterm_of sg flower, cterm_of sg fupper)
   22.64 -    end
   22.65 +  let
   22.66 +    val (flower, fupper) = approx_value_term prec pprt value
   22.67 +  in
   22.68 +    (cterm_of sg flower, cterm_of sg fupper)
   22.69 +  end
   22.70  
   22.71  fun sign_term t = cterm_of sg t
   22.72  
    23.1 --- a/src/HOL/Matrix/cplex/MatrixLP.ML	Wed Sep 06 10:01:27 2006 +0200
    23.2 +++ b/src/HOL/Matrix/cplex/MatrixLP.ML	Wed Sep 06 13:48:02 2006 +0200
    23.3 @@ -16,15 +16,15 @@
    23.4  structure MatrixLP : MATRIX_LP =
    23.5  struct
    23.6  
    23.7 -val sg = sign_of (theory "MatrixLP")
    23.8 +val thy = theory "MatrixLP";
    23.9  
   23.10 -fun inst_real thm = standard (Thm.instantiate ([(ctyp_of sg (TVar (hd (term_tvars (prop_of thm)))),
   23.11 -						 ctyp_of sg HOLogic.realT)], []) thm)
   23.12 +fun inst_real thm = standard (Thm.instantiate ([(ctyp_of thy (TVar (hd (term_tvars (prop_of thm)))),
   23.13 +						 ctyp_of thy HOLogic.realT)], []) thm)
   23.14  
   23.15  fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) = 
   23.16      let
   23.17  	val th = inst_real (thm "SparseMatrix.spm_mult_le_dual_prts_no_let")
   23.18 -	fun var s x = (cterm_of sg (Var ((s,0), FloatSparseMatrixBuilder.real_spmatT)), x)
   23.19 +	fun var s x = (cterm_of thy (Var ((s,0), FloatSparseMatrixBuilder.real_spmatT)), x)
   23.20  	val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, 
   23.21  				       var "r1" r1, var "r2" r2, var "b" b]) th
   23.22      in
   23.23 @@ -43,8 +43,8 @@
   23.24      in
   23.25  	lp_dual_estimate_prt_primitive certificate
   23.26      end
   23.27 -	 
   23.28 -fun read_ct s = read_cterm sg (s, TypeInfer.logicT);
   23.29 +
   23.30 +fun read_ct s = read_cterm thy (s, TypeInfer.logicT);
   23.31      
   23.32  fun is_meta_eq th =
   23.33      let
   23.34 @@ -56,19 +56,19 @@
   23.35      
   23.36  fun prep ths = (Library.filter is_meta_eq ths) @ (map (standard o mk_meta_eq) (Library.filter (not o is_meta_eq) ths))
   23.37  
   23.38 -fun make ths = Compute.basic_make sg ths
   23.39 +fun make ths = Compute.basic_make thy ths
   23.40  	  
   23.41  fun inst_tvar ty thm = 
   23.42      let
   23.43  	val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord)
   23.44  	val v = TVar (hd (sort ord (term_tvars (prop_of thm))))
   23.45      in	
   23.46 -	standard (Thm.instantiate ([(ctyp_of sg v, ctyp_of sg ty)], []) thm)
   23.47 +	standard (Thm.instantiate ([(ctyp_of thy v, ctyp_of thy ty)], []) thm)
   23.48      end
   23.49      
   23.50  fun inst_tvars [] thms = thms
   23.51    | inst_tvars (ty::tys) thms = inst_tvars tys (map (inst_tvar ty) thms)
   23.52 -				
   23.53 +
   23.54  val matrix_compute =
   23.55      let 
   23.56  	val spvecT = FloatSparseMatrixBuilder.real_spvecT
   23.57 @@ -117,8 +117,8 @@
   23.58  	matrix_simplify th
   23.59      end
   23.60  
   23.61 -fun realFromStr s = valOf (Real.fromString s)
   23.62 -fun float2real (x,y) = (realFromStr x) * (Math.pow (2.0, realFromStr y))
   23.63 +val realFromStr = the o Real.fromString;
   23.64 +fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y);
   23.65  
   23.66  end
   23.67  
    24.1 --- a/src/HOL/Presburger.thy	Wed Sep 06 10:01:27 2006 +0200
    24.2 +++ b/src/HOL/Presburger.thy	Wed Sep 06 13:48:02 2006 +0200
    24.3 @@ -992,7 +992,8 @@
    24.4  lemma not_true_eq_false: "(~ True) = False" by simp
    24.5  
    24.6  
    24.7 -lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
    24.8 +lemma int_eq_number_of_eq:
    24.9 +  "(((number_of v)::int) = (number_of w)) = iszero ((number_of (v + (uminus w)))::int)"
   24.10    by simp
   24.11  lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" 
   24.12    by (simp only: iszero_number_of_Pls)
   24.13 @@ -1006,7 +1007,7 @@
   24.14  lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)" 
   24.15    by simp
   24.16  
   24.17 -lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
   24.18 +lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
   24.19    by simp
   24.20  
   24.21  lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))" 
   24.22 @@ -1018,18 +1019,20 @@
   24.23  lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
   24.24    by simp
   24.25  
   24.26 -lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
   24.27 +lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
   24.28    by simp
   24.29 -lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)"
   24.30 +lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
   24.31    by simp
   24.32  
   24.33 -lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))"
   24.34 +lemma int_number_of_diff_sym:
   24.35 +  "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
   24.36    by simp
   24.37  
   24.38 -lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)"
   24.39 +lemma int_number_of_mult_sym:
   24.40 +  "((number_of v)::int) * number_of w = number_of (v * w)"
   24.41    by simp
   24.42  
   24.43 -lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)"
   24.44 +lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
   24.45    by simp
   24.46  lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
   24.47    by simp
    25.1 --- a/src/HOL/Real/Float.ML	Wed Sep 06 10:01:27 2006 +0200
    25.2 +++ b/src/HOL/Real/Float.ML	Wed Sep 06 13:48:02 2006 +0200
    25.3 @@ -7,9 +7,9 @@
    25.4  sig
    25.5      exception Destruct_floatstr of string
    25.6      val destruct_floatstr : (char -> bool) -> (char -> bool) -> string -> bool * string * string * bool * string
    25.7 -									  
    25.8 +
    25.9      exception Floating_point of string
   25.10 -				
   25.11 +
   25.12      type floatrep = IntInf.int * IntInf.int
   25.13      val approx_dec_by_bin : IntInf.int -> floatrep -> floatrep * floatrep
   25.14      val approx_decstr_by_bin : int -> string -> floatrep * floatrep
   25.15 @@ -351,23 +351,19 @@
   25.16  exception Dest_float;
   25.17  
   25.18  fun mk_intinf ty n =
   25.19 -    let
   25.20 -	fun mk_bit n = if n = zero then HOLogic.B0_const else HOLogic.B1_const
   25.21 -								 
   25.22 -	fun bin_of n = 
   25.23 -	    if n = zero then HOLogic.pls_const
   25.24 -	    else if n = minus_one then HOLogic.min_const
   25.25 -	    else 
   25.26 -		let 
   25.27 -		    (*val (q,r) = IntInf.divMod (n, two): doesn't work in SML 10.0.7, but in newer versions!!!*)
   25.28 -	            val q = IntInf.div (n, two)
   25.29 -		    val r = IntInf.mod (n, two)
   25.30 -		in
   25.31 -		    HOLogic.bit_const $ bin_of q $ mk_bit r
   25.32 -		end
   25.33 -    in 
   25.34 -	HOLogic.number_of_const ty $ (bin_of n)
   25.35 -    end
   25.36 +  let
   25.37 +    fun mk_bit n = if n = zero then HOLogic.B0_const else HOLogic.B1_const
   25.38 +    fun bin_of n = 
   25.39 +      if n = zero then HOLogic.pls_const
   25.40 +      else if n = minus_one then HOLogic.min_const
   25.41 +      else let 
   25.42 +        val (q,r) = IntInf.divMod (n, two)
   25.43 +      in
   25.44 +        HOLogic.bit_const $ bin_of q $ mk_bit r
   25.45 +      end
   25.46 +  in 
   25.47 +    HOLogic.number_of_const ty $ (bin_of n)
   25.48 +  end
   25.49  
   25.50  fun dest_intinf n = 
   25.51      let
    26.1 --- a/src/HOL/Real/Float.thy	Wed Sep 06 10:01:27 2006 +0200
    26.2 +++ b/src/HOL/Real/Float.thy	Wed Sep 06 13:48:02 2006 +0200
    26.3 @@ -3,7 +3,9 @@
    26.4      Author: Steven Obua
    26.5  *)
    26.6  
    26.7 -theory Float imports Real begin
    26.8 +theory Float
    26.9 +imports Real
   26.10 +begin
   26.11  
   26.12  definition
   26.13    pow2 :: "int \<Rightarrow> real"
   26.14 @@ -177,7 +179,7 @@
   26.15    ultimately show ?thesis by auto
   26.16  qed
   26.17  
   26.18 -lemma real_is_int_number_of[simp]: "real_is_int ((number_of::bin\<Rightarrow>real) x)"
   26.19 +lemma real_is_int_number_of[simp]: "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
   26.20  proof -
   26.21    have neg1: "real_is_int (-1::real)"
   26.22    proof -
   26.23 @@ -187,11 +189,9 @@
   26.24    qed
   26.25  
   26.26    {
   26.27 -    fix x::int
   26.28 -    have "!! y. real_is_int ((number_of::bin\<Rightarrow>real) (Abs_Bin x))"
   26.29 -      apply (simp add: number_of_eq)
   26.30 -      apply (subst Abs_Bin_inverse)
   26.31 -      apply (simp add: Bin_def)
   26.32 +    fix x :: int
   26.33 +    have "real_is_int ((number_of \<Colon> int \<Rightarrow> real) x)"
   26.34 +      unfolding number_of_eq
   26.35        apply (induct x)
   26.36        apply (induct_tac n)
   26.37        apply (simp)
   26.38 @@ -212,13 +212,13 @@
   26.39    }
   26.40    note Abs_Bin = this
   26.41    {
   26.42 -    fix x :: bin
   26.43 -    have "? u. x = Abs_Bin u"
   26.44 -      apply (rule exI[where x = "Rep_Bin x"])
   26.45 -      apply (simp add: Rep_Bin_inverse)
   26.46 +    fix x :: int
   26.47 +    have "? u. x = u"
   26.48 +      apply (rule exI[where x = "x"])
   26.49 +      apply (simp)
   26.50        done
   26.51    }
   26.52 -  then obtain u::int where "x = Abs_Bin u" by auto
   26.53 +  then obtain u::int where "x = u" by auto
   26.54    with Abs_Bin show ?thesis by auto
   26.55  qed
   26.56  
   26.57 @@ -448,17 +448,17 @@
   26.58  
   26.59  lemma not_true_eq_false: "(~ True) = False" by simp
   26.60  
   26.61 -
   26.62  lemmas binarith =
   26.63    Pls_0_eq Min_1_eq
   26.64 -  bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
   26.65 -  bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
   26.66 -  bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10
   26.67 -  bin_add_BIT_11 bin_minus_Pls bin_minus_Min bin_minus_1
   26.68 -  bin_minus_0 bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0
   26.69 -  bin_add_Pls_right bin_add_Min_right
   26.70 +  pred_Pls pred_Min pred_1 pred_0
   26.71 +  succ_Pls succ_Min succ_1 succ_0
   26.72 +  add_Pls add_Min add_BIT_0 add_BIT_10
   26.73 +  add_BIT_11 minus_Pls minus_Min minus_1
   26.74 +  minus_0 mult_Pls mult_Min mult_num1 mult_num0
   26.75 +  add_Pls_right add_Min_right
   26.76  
   26.77 -lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
   26.78 +lemma int_eq_number_of_eq:
   26.79 +  "(((number_of v)::int)=(number_of w)) = iszero ((number_of (v + uminus w))::int)"
   26.80    by simp
   26.81  
   26.82  lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
   26.83 @@ -473,7 +473,7 @@
   26.84  lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
   26.85    by simp
   26.86  
   26.87 -lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
   26.88 +lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
   26.89    by simp
   26.90  
   26.91  lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
   26.92 @@ -485,7 +485,7 @@
   26.93  lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
   26.94    by simp
   26.95  
   26.96 -lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
   26.97 +lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (y + (uminus x)))::int))"
   26.98    by simp
   26.99  
  26.100  lemmas intarithrel =
  26.101 @@ -494,16 +494,16 @@
  26.102    lift_bool[OF int_iszero_number_of_1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min]
  26.103    int_neg_number_of_BIT int_le_number_of_eq
  26.104  
  26.105 -lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)"
  26.106 +lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (v + w)"
  26.107    by simp
  26.108  
  26.109 -lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))"
  26.110 +lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (v + (uminus w))"
  26.111    by simp
  26.112  
  26.113 -lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)"
  26.114 +lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (v * w)"
  26.115    by simp
  26.116  
  26.117 -lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)"
  26.118 +lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (uminus v)"
  26.119    by simp
  26.120  
  26.121  lemmas intarith = int_number_of_add_sym int_number_of_minus_sym int_number_of_diff_sym int_number_of_mult_sym
    27.1 --- a/src/HOL/Real/Rational.thy	Wed Sep 06 10:01:27 2006 +0200
    27.2 +++ b/src/HOL/Real/Rational.thy	Wed Sep 06 13:48:02 2006 +0200
    27.3 @@ -451,7 +451,7 @@
    27.4  instance rat :: number ..
    27.5  
    27.6  defs (overloaded)
    27.7 -  rat_number_of_def: "(number_of w :: rat) == of_int (Rep_Bin w)"
    27.8 +  rat_number_of_def: "(number_of w :: rat) == of_int w"
    27.9      --{*the type constraint is essential!*}
   27.10  
   27.11  instance rat :: number_ring
    28.1 --- a/src/HOL/Real/RealDef.thy	Wed Sep 06 10:01:27 2006 +0200
    28.2 +++ b/src/HOL/Real/RealDef.thy	Wed Sep 06 13:48:02 2006 +0200
    28.3 @@ -922,7 +922,7 @@
    28.4  instance real :: number ..
    28.5  
    28.6  defs (overloaded)
    28.7 -  real_number_of_def: "(number_of w :: real) == of_int (Rep_Bin w)"
    28.8 +  real_number_of_def: "(number_of w :: real) == of_int w"
    28.9      --{*the type constraint is essential!*}
   28.10  
   28.11  instance real :: number_ring
    29.1 --- a/src/HOL/Real/ferrante_rackoff.ML	Wed Sep 06 10:01:27 2006 +0200
    29.2 +++ b/src/HOL/Real/ferrante_rackoff.ML	Wed Sep 06 13:48:02 2006 +0200
    29.3 @@ -21,12 +21,12 @@
    29.4  val nT = HOLogic.natT;
    29.5  val binarith = map thm
    29.6    ["Pls_0_eq", "Min_1_eq",
    29.7 - "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
    29.8 -  "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
    29.9 -  "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
   29.10 -  "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
   29.11 -  "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
   29.12 -  "bin_add_Pls_right", "bin_add_Min_right"];
   29.13 + "pred_Pls","pred_Min","pred_1","pred_0",
   29.14 +  "succ_Pls", "succ_Min", "succ_1", "succ_0",
   29.15 +  "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10",
   29.16 +  "add_BIT_11", "minus_Pls", "minus_Min", "minus_1", 
   29.17 +  "minus_0", "mult_Pls", "mult_Min", "mult_1", "mult_0", 
   29.18 +  "add_Pls_right", "add_Min_right"];
   29.19   val intarithrel = 
   29.20       (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
   29.21  		"int_le_number_of_eq","int_iszero_number_of_0",
    30.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Wed Sep 06 10:01:27 2006 +0200
    30.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Wed Sep 06 13:48:02 2006 +0200
    30.3 @@ -33,12 +33,12 @@
    30.4  val presburger_ss = simpset ();
    30.5  val binarith = map thm
    30.6    ["Pls_0_eq", "Min_1_eq",
    30.7 - "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
    30.8 -  "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
    30.9 -  "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
   30.10 -  "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
   30.11 -  "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
   30.12 -  "bin_add_Pls_right", "bin_add_Min_right"];
   30.13 + "pred_Pls","pred_Min","pred_1","pred_0",
   30.14 +  "succ_Pls", "succ_Min", "succ_1", "succ_0",
   30.15 +  "add_Pls", "add_Min", "add_BIT_0", "add_BIT_10",
   30.16 +  "add_BIT_11", "minus_Pls", "minus_Min", "minus_1", 
   30.17 +  "minus_0", "mult_Pls", "mult_Min", "mult_num1", "mult_num0", 
   30.18 +  "add_Pls_right", "add_Min_right"];
   30.19   val intarithrel = 
   30.20       (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
   30.21  		"int_le_number_of_eq","int_iszero_number_of_0",
   30.22 @@ -116,7 +116,6 @@
   30.23  val bT = HOLogic.boolT;
   30.24  val bitT = HOLogic.bitT;
   30.25  val iT = HOLogic.intT;
   30.26 -val binT = HOLogic.binT;
   30.27  val nT = HOLogic.natT;
   30.28  
   30.29  (* Allowed Consts in formulae for presburger tactic*)
   30.30 @@ -162,11 +161,11 @@
   30.31  
   30.32     ("Numeral.bit.B0", bitT),
   30.33     ("Numeral.bit.B1", bitT),
   30.34 -   ("Numeral.Bit", binT --> bitT --> binT),
   30.35 -   ("Numeral.Pls", binT),
   30.36 -   ("Numeral.Min", binT),
   30.37 -   ("Numeral.number_of", binT --> iT),
   30.38 -   ("Numeral.number_of", binT --> nT),
   30.39 +   ("Numeral.Bit", iT --> bitT --> iT),
   30.40 +   ("Numeral.Pls", iT),
   30.41 +   ("Numeral.Min", iT),
   30.42 +   ("Numeral.number_of", iT --> iT),
   30.43 +   ("Numeral.number_of", iT --> nT),
   30.44     ("0", nT),
   30.45     ("0", iT),
   30.46     ("1", nT),
    31.1 --- a/src/HOL/arith_data.ML	Wed Sep 06 10:01:27 2006 +0200
    31.2 +++ b/src/HOL/arith_data.ML	Wed Sep 06 13:48:02 2006 +0200
    31.3 @@ -680,7 +680,7 @@
    31.4        end
    31.5      (* "?P ((?n::int) mod (number_of ?k)) =
    31.6           ((iszero (number_of ?k) --> ?P ?n) &
    31.7 -          (neg (number_of (bin_minus ?k)) -->
    31.8 +          (neg (number_of (uminus ?k)) -->
    31.9              (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
   31.10            (neg (number_of ?k) -->
   31.11              (ALL i j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j --> ?P j))) *)
   31.12 @@ -699,8 +699,8 @@
   31.13          val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
   31.14          val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
   31.15                                          (number_of $
   31.16 -                                          (Const ("Numeral.bin_minus",
   31.17 -                                            HOLogic.binT --> HOLogic.binT) $ k'))
   31.18 +                                          (Const ("HOL.uminus",
   31.19 +                                            HOLogic.intT --> HOLogic.intT) $ k'))
   31.20          val zero_leq_j              = Const ("Orderings.less_eq",
   31.21                                          split_type --> split_type --> HOLogic.boolT) $ zero $ j
   31.22          val j_lt_t2                 = Const ("Orderings.less",
   31.23 @@ -732,7 +732,7 @@
   31.24        end
   31.25      (* "?P ((?n::int) div (number_of ?k)) =
   31.26           ((iszero (number_of ?k) --> ?P 0) &
   31.27 -          (neg (number_of (bin_minus ?k)) -->
   31.28 +          (neg (number_of (uminus ?k)) -->
   31.29              (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &
   31.30            (neg (number_of ?k) -->
   31.31              (ALL i. (EX j. number_of ?k < j & j <= 0 & ?n = number_of ?k * i + j) --> ?P i))) *)
   31.32 @@ -751,8 +751,8 @@
   31.33          val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
   31.34          val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
   31.35                                          (number_of $
   31.36 -                                          (Const ("Numeral.bin_minus",
   31.37 -                                            HOLogic.binT --> HOLogic.binT) $ k'))
   31.38 +                                          (Const ("Numeral.uminus",
   31.39 +                                            HOLogic.intT --> HOLogic.intT) $ k'))
   31.40          val zero_leq_j              = Const ("Orderings.less_eq",
   31.41                                          split_type --> split_type --> HOLogic.boolT) $ zero $ j
   31.42          val j_lt_t2                 = Const ("Orderings.less",
    32.1 --- a/src/HOL/ex/Abstract_NAT.thy	Wed Sep 06 10:01:27 2006 +0200
    32.2 +++ b/src/HOL/ex/Abstract_NAT.thy	Wed Sep 06 13:48:02 2006 +0200
    32.3 @@ -11,6 +11,8 @@
    32.4  
    32.5  text {* Axiomatic Natural Numbers (Peano) -- a monomorphic theory. *}
    32.6  
    32.7 +hide (open) const succ
    32.8 +
    32.9  locale NAT =
   32.10    fixes zero :: 'n
   32.11      and succ :: "'n \<Rightarrow> 'n"
    33.1 --- a/src/HOL/hologic.ML	Wed Sep 06 10:01:27 2006 +0200
    33.2 +++ b/src/HOL/hologic.ML	Wed Sep 06 13:48:02 2006 +0200
    33.3 @@ -76,7 +76,6 @@
    33.4    val bitT: typ
    33.5    val B0_const: term
    33.6    val B1_const: term
    33.7 -  val binT: typ
    33.8    val pls_const: term
    33.9    val min_const: term
   33.10    val bit_const: term
   33.11 @@ -280,26 +279,25 @@
   33.12    | dest_nat t = raise TERM ("dest_nat", [t]);
   33.13  
   33.14  
   33.15 -(* binary numerals *)
   33.16 +(* binary numerals and int *)
   33.17  
   33.18 -val binT = Type ("Numeral.bin", []);
   33.19 -
   33.20 +val intT = Type ("IntDef.int", []);
   33.21  val bitT = Type ("Numeral.bit", []);
   33.22  
   33.23  val B0_const = Const ("Numeral.bit.B0", bitT);
   33.24  val B1_const =  Const ("Numeral.bit.B1", bitT);
   33.25  
   33.26 -val pls_const = Const ("Numeral.Pls", binT)
   33.27 -and min_const = Const ("Numeral.Min", binT)
   33.28 -and bit_const = Const ("Numeral.Bit", [binT, bitT] ---> binT);
   33.29 +val pls_const = Const ("Numeral.Pls", intT)
   33.30 +and min_const = Const ("Numeral.Min", intT)
   33.31 +and bit_const = Const ("Numeral.Bit", [intT, bitT] ---> intT);
   33.32  
   33.33 -fun number_of_const T = Const ("Numeral.number_of", binT --> T);
   33.34 +fun number_of_const T = Const ("Numeral.number_of", intT --> T);
   33.35  
   33.36  fun int_of [] = 0
   33.37    | int_of (b :: bs) = IntInf.fromInt b + (2 * int_of bs);
   33.38  
   33.39  (*When called from a print translation, the Numeral qualifier will probably have
   33.40 -  been removed from Bit, bin.B0, etc.*)
   33.41 +  been removed from Bit, bit.B0, etc.*)
   33.42  fun dest_bit (Const ("Numeral.bit.B0", _)) = 0
   33.43    | dest_bit (Const ("Numeral.bit.B1", _)) = 1
   33.44    | dest_bit (Const ("bit.B0", _)) = 0
   33.45 @@ -334,11 +332,6 @@
   33.46          in bit_const $ bin_of q $ mk_bit r end;
   33.47    in bin_of n end;
   33.48  
   33.49 -
   33.50 -(* int *)
   33.51 -
   33.52 -val intT = Type ("IntDef.int", []);
   33.53 -
   33.54  fun mk_int 0 = Const ("0", intT)
   33.55    | mk_int 1 = Const ("1", intT)
   33.56    | mk_int i = number_of_const intT $ mk_binum i;
    34.1 --- a/src/Pure/Tools/codegen_package.ML	Wed Sep 06 10:01:27 2006 +0200
    34.2 +++ b/src/Pure/Tools/codegen_package.ML	Wed Sep 06 13:48:02 2006 +0200
    34.3 @@ -609,19 +609,18 @@
    34.4  (* parametrized application generators, for instantiation in object logic *)
    34.5  (* (axiomatic extensions of extraction kernel *)
    34.6  
    34.7 -fun appgen_rep_bin int_of_numeral thy algbr thmtab strct (app as (c as (_, ty), [bin])) trns =
    34.8 -  case try (int_of_numeral thy) bin
    34.9 +fun appgen_rep_bin int_of_numeral thy algbr thmtab strct (app as (c, ts)) trns =
   34.10 +  case try (int_of_numeral thy) (list_comb (Const c, ts))
   34.11     of SOME i => if i < 0 then (*preprocessor eliminates negative numerals*)
   34.12          trns
   34.13          |> appgen_default thy algbr thmtab (no_strict strct) app
   34.14        else
   34.15          trns
   34.16 -        |> exprgen_term thy algbr thmtab (no_strict strct) (Const c)
   34.17 -        ||>> exprgen_term thy algbr thmtab (no_strict strct) bin
   34.18 -        |-> (fn (e1, e2) => pair (CodegenThingol.INum (i, e1 `$ e2)))
   34.19 +        |> appgen_default thy algbr thmtab (no_strict strct) app
   34.20 +        |-> (fn e => pair (CodegenThingol.INum (i, e)))
   34.21      | NONE =>
   34.22          trns
   34.23 -        |> appgen_default thy algbr thmtab strct app;
   34.24 +        |> appgen_default thy algbr thmtab (no_strict strct) app;
   34.25  
   34.26  fun appgen_char char_to_index thy algbr thmtab strct (app as ((_, ty), _)) trns =
   34.27    case (char_to_index o list_comb o apfst Const) app