src/HOL/Integ/Numeral.thy
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 16417 9bc16273c2d4
child 19380 b808efaa5828
permissions -rw-r--r--
adaptions to codegen_package
paulson@15013
     1
(*  Title:	HOL/Integ/Numeral.thy
paulson@15013
     2
    ID:         $Id$
paulson@15013
     3
    Author:	Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@15013
     4
    Copyright	1994  University of Cambridge
paulson@15013
     5
*)
paulson@15013
     6
paulson@15013
     7
header{*Arithmetic on Binary Integers*}
paulson@15013
     8
nipkow@15131
     9
theory Numeral
paulson@15620
    10
imports IntDef Datatype
haftmann@16417
    11
uses "../Tools/numeral_syntax.ML"
nipkow@15131
    12
begin
paulson@15013
    13
paulson@15013
    14
text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
paulson@15013
    15
   Only qualified access Numeral.Pls and Numeral.Min is allowed.
paulson@15620
    16
   The datatype constructors bit.B0 and bit.B1 are similarly hidden.
paulson@15013
    17
   We do not hide Bit because we need the BIT infix syntax.*}
paulson@15013
    18
paulson@15013
    19
text{*This formalization defines binary arithmetic in terms of the integers
paulson@15013
    20
rather than using a datatype. This avoids multiple representations (leading
paulson@15013
    21
zeroes, etc.)  See @{text "ZF/Integ/twos-compl.ML"}, function @{text
paulson@15013
    22
int_of_binary}, for the numerical interpretation.
paulson@15013
    23
paulson@15013
    24
The representation expects that @{text "(m mod 2)"} is 0 or 1,
paulson@15013
    25
even if m is negative;
paulson@15013
    26
For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
paulson@15013
    27
@{text "-5 = (-3)*2 + 1"}.
paulson@15013
    28
*}
paulson@15013
    29
paulson@15013
    30
paulson@15013
    31
typedef (Bin)
paulson@15013
    32
  bin = "UNIV::int set"
paulson@15013
    33
    by (auto)
paulson@15013
    34
paulson@15620
    35
paulson@15620
    36
text{*This datatype avoids the use of type @{typ bool}, which would make
paulson@15620
    37
all of the rewrite rules higher-order. If the use of datatype causes
paulson@15620
    38
problems, this two-element type can easily be formalized using typedef.*}
paulson@15620
    39
datatype bit = B0 | B1
paulson@15620
    40
paulson@15013
    41
constdefs
paulson@15013
    42
  Pls :: "bin"
paulson@15013
    43
   "Pls == Abs_Bin 0"
paulson@15013
    44
paulson@15013
    45
  Min :: "bin"
paulson@15013
    46
   "Min == Abs_Bin (- 1)"
paulson@15013
    47
paulson@15620
    48
  Bit :: "[bin,bit] => bin"    (infixl "BIT" 90)
paulson@15013
    49
   --{*That is, 2w+b*}
paulson@15620
    50
   "w BIT b == Abs_Bin ((case b of B0 => 0 | B1 => 1) + Rep_Bin w + Rep_Bin w)"
paulson@15013
    51
paulson@15013
    52
paulson@15013
    53
axclass
paulson@15013
    54
  number < type  -- {* for numeric types: nat, int, real, \dots *}
paulson@15013
    55
paulson@15013
    56
consts
paulson@15013
    57
  number_of :: "bin => 'a::number"
paulson@15013
    58
paulson@15013
    59
syntax
paulson@15013
    60
  "_Numeral" :: "num_const => 'a"    ("_")
paulson@15013
    61
  Numeral0 :: 'a
paulson@15013
    62
  Numeral1 :: 'a
paulson@15013
    63
paulson@15013
    64
translations
paulson@15013
    65
  "Numeral0" == "number_of Numeral.Pls"
paulson@15620
    66
  "Numeral1" == "number_of (Numeral.Pls BIT bit.B1)"
paulson@15013
    67
paulson@15013
    68
paulson@15013
    69
setup NumeralSyntax.setup
paulson@15013
    70
paulson@15013
    71
syntax (xsymbols)
paulson@15013
    72
  "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
paulson@15013
    73
syntax (HTML output)
paulson@15013
    74
  "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
paulson@15013
    75
syntax (output)
paulson@15013
    76
  "_square" :: "'a => 'a"  ("(_ ^/ 2)" [81] 80)
paulson@15013
    77
translations
paulson@15013
    78
  "x\<twosuperior>" == "x^2"
paulson@15013
    79
  "x\<twosuperior>" <= "x^(2::nat)"
paulson@15013
    80
paulson@15013
    81
paulson@15013
    82
lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
paulson@15013
    83
  -- {* Unfold all @{text let}s involving constants *}
paulson@15013
    84
  by (simp add: Let_def)
paulson@15013
    85
paulson@15013
    86
lemma Let_0 [simp]: "Let 0 f == f 0"
paulson@15013
    87
  by (simp add: Let_def)
paulson@15013
    88
paulson@15013
    89
lemma Let_1 [simp]: "Let 1 f == f 1"
paulson@15013
    90
  by (simp add: Let_def)
paulson@15013
    91
paulson@15013
    92
paulson@15013
    93
constdefs
paulson@15013
    94
  bin_succ  :: "bin=>bin"
paulson@15013
    95
   "bin_succ w == Abs_Bin(Rep_Bin w + 1)"
paulson@15013
    96
paulson@15013
    97
  bin_pred  :: "bin=>bin"
paulson@15013
    98
   "bin_pred w == Abs_Bin(Rep_Bin w - 1)"
paulson@15013
    99
paulson@15013
   100
  bin_minus  :: "bin=>bin"
paulson@15013
   101
   "bin_minus w == Abs_Bin(- (Rep_Bin w))"
paulson@15013
   102
paulson@15013
   103
  bin_add  :: "[bin,bin]=>bin"
paulson@15013
   104
   "bin_add v w == Abs_Bin(Rep_Bin v + Rep_Bin w)"
paulson@15013
   105
paulson@15013
   106
  bin_mult  :: "[bin,bin]=>bin"
paulson@15013
   107
   "bin_mult v w == Abs_Bin(Rep_Bin v * Rep_Bin w)"
paulson@15013
   108
paulson@15013
   109
paulson@15013
   110
lemmas Bin_simps = 
paulson@15013
   111
       bin_succ_def bin_pred_def bin_minus_def bin_add_def bin_mult_def
paulson@15013
   112
       Pls_def Min_def Bit_def Abs_Bin_inverse Rep_Bin_inverse Bin_def
paulson@15013
   113
paulson@15013
   114
text{*Removal of leading zeroes*}
paulson@15620
   115
lemma Pls_0_eq [simp]: "Numeral.Pls BIT bit.B0 = Numeral.Pls"
paulson@15013
   116
by (simp add: Bin_simps)
paulson@15013
   117
paulson@15620
   118
lemma Min_1_eq [simp]: "Numeral.Min BIT bit.B1 = Numeral.Min"
paulson@15013
   119
by (simp add: Bin_simps)
paulson@15013
   120
paulson@15013
   121
subsection{*The Functions @{term bin_succ},  @{term bin_pred} and @{term bin_minus}*}
paulson@15013
   122
paulson@15620
   123
lemma bin_succ_Pls [simp]: "bin_succ Numeral.Pls = Numeral.Pls BIT bit.B1"
paulson@15013
   124
by (simp add: Bin_simps) 
paulson@15013
   125
paulson@15013
   126
lemma bin_succ_Min [simp]: "bin_succ Numeral.Min = Numeral.Pls"
paulson@15013
   127
by (simp add: Bin_simps) 
paulson@15013
   128
paulson@15620
   129
lemma bin_succ_1 [simp]: "bin_succ(w BIT bit.B1) = (bin_succ w) BIT bit.B0"
paulson@15013
   130
by (simp add: Bin_simps add_ac) 
paulson@15013
   131
paulson@15620
   132
lemma bin_succ_0 [simp]: "bin_succ(w BIT bit.B0) = w BIT bit.B1"
paulson@15013
   133
by (simp add: Bin_simps add_ac) 
paulson@15013
   134
paulson@15013
   135
lemma bin_pred_Pls [simp]: "bin_pred Numeral.Pls = Numeral.Min"
paulson@15013
   136
by (simp add: Bin_simps) 
paulson@15013
   137
paulson@15620
   138
lemma bin_pred_Min [simp]: "bin_pred Numeral.Min = Numeral.Min BIT bit.B0"
paulson@15013
   139
by (simp add: Bin_simps diff_minus) 
paulson@15013
   140
paulson@15620
   141
lemma bin_pred_1 [simp]: "bin_pred(w BIT bit.B1) = w BIT bit.B0"
paulson@15013
   142
by (simp add: Bin_simps) 
paulson@15013
   143
paulson@15620
   144
lemma bin_pred_0 [simp]: "bin_pred(w BIT bit.B0) = (bin_pred w) BIT bit.B1"
paulson@15013
   145
by (simp add: Bin_simps diff_minus add_ac) 
paulson@15013
   146
paulson@15013
   147
lemma bin_minus_Pls [simp]: "bin_minus Numeral.Pls = Numeral.Pls"
paulson@15013
   148
by (simp add: Bin_simps) 
paulson@15013
   149
paulson@15620
   150
lemma bin_minus_Min [simp]: "bin_minus Numeral.Min = Numeral.Pls BIT bit.B1"
paulson@15013
   151
by (simp add: Bin_simps) 
paulson@15013
   152
paulson@15013
   153
lemma bin_minus_1 [simp]:
paulson@15620
   154
     "bin_minus (w BIT bit.B1) = bin_pred (bin_minus w) BIT bit.B1"
paulson@15013
   155
by (simp add: Bin_simps add_ac diff_minus) 
paulson@15013
   156
paulson@15620
   157
 lemma bin_minus_0 [simp]: "bin_minus(w BIT bit.B0) = (bin_minus w) BIT bit.B0"
paulson@15013
   158
by (simp add: Bin_simps) 
paulson@15013
   159
paulson@15013
   160
paulson@15013
   161
subsection{*Binary Addition and Multiplication:
paulson@15013
   162
         @{term bin_add} and @{term bin_mult}*}
paulson@15013
   163
paulson@15013
   164
lemma bin_add_Pls [simp]: "bin_add Numeral.Pls w = w"
paulson@15013
   165
by (simp add: Bin_simps) 
paulson@15013
   166
paulson@15013
   167
lemma bin_add_Min [simp]: "bin_add Numeral.Min w = bin_pred w"
paulson@15013
   168
by (simp add: Bin_simps diff_minus add_ac) 
paulson@15013
   169
paulson@15013
   170
lemma bin_add_BIT_11 [simp]:
paulson@15620
   171
     "bin_add (v BIT bit.B1) (w BIT bit.B1) = bin_add v (bin_succ w) BIT bit.B0"
paulson@15013
   172
by (simp add: Bin_simps add_ac)
paulson@15013
   173
paulson@15013
   174
lemma bin_add_BIT_10 [simp]:
paulson@15620
   175
     "bin_add (v BIT bit.B1) (w BIT bit.B0) = (bin_add v w) BIT bit.B1"
paulson@15013
   176
by (simp add: Bin_simps add_ac)
paulson@15013
   177
paulson@15013
   178
lemma bin_add_BIT_0 [simp]:
paulson@15620
   179
     "bin_add (v BIT bit.B0) (w BIT y) = bin_add v w BIT y"
paulson@15013
   180
by (simp add: Bin_simps add_ac)
paulson@15013
   181
paulson@15013
   182
lemma bin_add_Pls_right [simp]: "bin_add w Numeral.Pls = w"
paulson@15013
   183
by (simp add: Bin_simps) 
paulson@15013
   184
paulson@15013
   185
lemma bin_add_Min_right [simp]: "bin_add w Numeral.Min = bin_pred w"
paulson@15013
   186
by (simp add: Bin_simps diff_minus) 
paulson@15013
   187
paulson@15013
   188
lemma bin_mult_Pls [simp]: "bin_mult Numeral.Pls w = Numeral.Pls"
paulson@15013
   189
by (simp add: Bin_simps) 
paulson@15013
   190
paulson@15013
   191
lemma bin_mult_Min [simp]: "bin_mult Numeral.Min w = bin_minus w"
paulson@15013
   192
by (simp add: Bin_simps) 
paulson@15013
   193
paulson@15013
   194
lemma bin_mult_1 [simp]:
paulson@15620
   195
     "bin_mult (v BIT bit.B1) w = bin_add ((bin_mult v w) BIT bit.B0) w"
paulson@15013
   196
by (simp add: Bin_simps add_ac left_distrib)
paulson@15013
   197
paulson@15620
   198
lemma bin_mult_0 [simp]: "bin_mult (v BIT bit.B0) w = (bin_mult v w) BIT bit.B0"
paulson@15013
   199
by (simp add: Bin_simps left_distrib)
paulson@15013
   200
paulson@15013
   201
paulson@15013
   202
paulson@15013
   203
subsection{*Converting Numerals to Rings: @{term number_of}*}
paulson@15013
   204
paulson@15013
   205
axclass number_ring \<subseteq> number, comm_ring_1
paulson@15013
   206
  number_of_eq: "number_of w = of_int (Rep_Bin w)"
paulson@15013
   207
paulson@15013
   208
lemma number_of_succ:
paulson@15013
   209
     "number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)"
paulson@15013
   210
by (simp add: number_of_eq Bin_simps)
paulson@15013
   211
paulson@15013
   212
lemma number_of_pred:
paulson@15013
   213
     "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
paulson@15013
   214
by (simp add: number_of_eq Bin_simps)
paulson@15013
   215
paulson@15013
   216
lemma number_of_minus:
paulson@15013
   217
     "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)"
paulson@15013
   218
by (simp add: number_of_eq Bin_simps) 
paulson@15013
   219
paulson@15013
   220
lemma number_of_add:
paulson@15013
   221
     "number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)"
paulson@15013
   222
by (simp add: number_of_eq Bin_simps) 
paulson@15013
   223
paulson@15013
   224
lemma number_of_mult:
paulson@15013
   225
     "number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)"
paulson@15013
   226
by (simp add: number_of_eq Bin_simps) 
paulson@15013
   227
paulson@15013
   228
text{*The correctness of shifting.  But it doesn't seem to give a measurable
paulson@15013
   229
  speed-up.*}
paulson@15013
   230
lemma double_number_of_BIT:
paulson@15620
   231
     "(1+1) * number_of w = (number_of (w BIT bit.B0) ::'a::number_ring)"
paulson@15013
   232
by (simp add: number_of_eq Bin_simps left_distrib) 
paulson@15013
   233
paulson@15013
   234
text{*Converting numerals 0 and 1 to their abstract versions*}
paulson@15013
   235
lemma numeral_0_eq_0 [simp]: "Numeral0 = (0::'a::number_ring)"
paulson@15013
   236
by (simp add: number_of_eq Bin_simps) 
paulson@15013
   237
paulson@15013
   238
lemma numeral_1_eq_1 [simp]: "Numeral1 = (1::'a::number_ring)"
paulson@15013
   239
by (simp add: number_of_eq Bin_simps) 
paulson@15013
   240
paulson@15013
   241
text{*Special-case simplification for small constants*}
paulson@15013
   242
paulson@15013
   243
text{*Unary minus for the abstract constant 1. Cannot be inserted
paulson@15013
   244
  as a simprule until later: it is @{text number_of_Min} re-oriented!*}
paulson@15013
   245
lemma numeral_m1_eq_minus_1: "(-1::'a::number_ring) = - 1"
paulson@15013
   246
by (simp add: number_of_eq Bin_simps) 
paulson@15013
   247
paulson@15013
   248
paulson@15013
   249
lemma mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)"
paulson@15013
   250
by (simp add: numeral_m1_eq_minus_1)
paulson@15013
   251
paulson@15013
   252
lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)"
paulson@15013
   253
by (simp add: numeral_m1_eq_minus_1)
paulson@15013
   254
paulson@15013
   255
(*Negation of a coefficient*)
paulson@15013
   256
lemma minus_number_of_mult [simp]:
paulson@15013
   257
     "- (number_of w) * z = number_of(bin_minus w) * (z::'a::number_ring)"
paulson@15013
   258
by (simp add: number_of_minus)
paulson@15013
   259
paulson@15013
   260
text{*Subtraction*}
paulson@15013
   261
lemma diff_number_of_eq:
paulson@15013
   262
     "number_of v - number_of w =
paulson@15013
   263
      (number_of(bin_add v (bin_minus w))::'a::number_ring)"
paulson@15013
   264
by (simp add: diff_minus number_of_add number_of_minus)
paulson@15013
   265
paulson@15013
   266
paulson@15013
   267
lemma number_of_Pls: "number_of Numeral.Pls = (0::'a::number_ring)"
paulson@15013
   268
by (simp add: number_of_eq Bin_simps) 
paulson@15013
   269
paulson@15013
   270
lemma number_of_Min: "number_of Numeral.Min = (- 1::'a::number_ring)"
paulson@15013
   271
by (simp add: number_of_eq Bin_simps) 
paulson@15013
   272
paulson@15013
   273
lemma number_of_BIT:
paulson@15620
   274
     "number_of(w BIT x) = (case x of bit.B0 => 0 | bit.B1 => (1::'a::number_ring)) +
paulson@15013
   275
	                   (number_of w) + (number_of w)"
paulson@15620
   276
by (simp add: number_of_eq Bin_simps split: bit.split) 
paulson@15013
   277
paulson@15013
   278
paulson@15013
   279
paulson@15013
   280
subsection{*Equality of Binary Numbers*}
paulson@15013
   281
paulson@15013
   282
text{*First version by Norbert Voelker*}
paulson@15013
   283
paulson@15013
   284
lemma eq_number_of_eq:
paulson@15013
   285
  "((number_of x::'a::number_ring) = number_of y) =
paulson@15013
   286
   iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
paulson@15013
   287
by (simp add: iszero_def compare_rls number_of_add number_of_minus)
paulson@15013
   288
paulson@15013
   289
lemma iszero_number_of_Pls: "iszero ((number_of Numeral.Pls)::'a::number_ring)"
paulson@15013
   290
by (simp add: iszero_def numeral_0_eq_0)
paulson@15013
   291
paulson@15013
   292
lemma nonzero_number_of_Min: "~ iszero ((number_of Numeral.Min)::'a::number_ring)"
paulson@15013
   293
by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
paulson@15013
   294
paulson@15013
   295
paulson@15013
   296
subsection{*Comparisons, for Ordered Rings*}
paulson@15013
   297
paulson@15013
   298
lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))"
paulson@15013
   299
proof -
paulson@15013
   300
  have "a + a = (1+1)*a" by (simp add: left_distrib)
paulson@15013
   301
  with zero_less_two [where 'a = 'a]
paulson@15013
   302
  show ?thesis by force
paulson@15013
   303
qed
paulson@15013
   304
paulson@15013
   305
lemma le_imp_0_less: 
paulson@15013
   306
  assumes le: "0 \<le> z" shows "(0::int) < 1 + z"
paulson@15013
   307
proof -
paulson@15013
   308
  have "0 \<le> z" .
paulson@15013
   309
  also have "... < z + 1" by (rule less_add_one) 
paulson@15013
   310
  also have "... = 1 + z" by (simp add: add_ac)
paulson@15013
   311
  finally show "0 < 1 + z" .
paulson@15013
   312
qed
paulson@15013
   313
paulson@15013
   314
lemma odd_nonzero: "1 + z + z \<noteq> (0::int)";
paulson@15013
   315
proof (cases z rule: int_cases)
paulson@15013
   316
  case (nonneg n)
paulson@15013
   317
  have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
paulson@15013
   318
  thus ?thesis using  le_imp_0_less [OF le]
paulson@15013
   319
    by (auto simp add: add_assoc) 
paulson@15013
   320
next
paulson@15013
   321
  case (neg n)
paulson@15013
   322
  show ?thesis
paulson@15013
   323
  proof
paulson@15013
   324
    assume eq: "1 + z + z = 0"
paulson@15013
   325
    have "0 < 1 + (int n + int n)"
paulson@15013
   326
      by (simp add: le_imp_0_less add_increasing) 
paulson@15013
   327
    also have "... = - (1 + z + z)" 
paulson@15013
   328
      by (simp add: neg add_assoc [symmetric]) 
paulson@15013
   329
    also have "... = 0" by (simp add: eq) 
paulson@15013
   330
    finally have "0<0" ..
paulson@15013
   331
    thus False by blast
paulson@15013
   332
  qed
paulson@15013
   333
qed
paulson@15013
   334
paulson@15013
   335
paulson@15013
   336
text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
paulson@15013
   337
lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)"
paulson@15013
   338
proof (unfold Ints_def) 
paulson@15013
   339
  assume "a \<in> range of_int"
paulson@15013
   340
  then obtain z where a: "a = of_int z" ..
paulson@15013
   341
  show ?thesis
paulson@15013
   342
  proof
paulson@15013
   343
    assume eq: "1 + a + a = 0"
paulson@15013
   344
    hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
paulson@15013
   345
    hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
paulson@15013
   346
    with odd_nonzero show False by blast
paulson@15013
   347
  qed
paulson@15013
   348
qed 
paulson@15013
   349
paulson@15013
   350
lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"
paulson@15013
   351
by (simp add: number_of_eq Ints_def) 
paulson@15013
   352
paulson@15013
   353
paulson@15013
   354
lemma iszero_number_of_BIT:
paulson@15013
   355
     "iszero (number_of (w BIT x)::'a) = 
paulson@15620
   356
      (x=bit.B0 & iszero (number_of w::'a::{ordered_idom,number_ring}))"
paulson@15013
   357
by (simp add: iszero_def number_of_eq Bin_simps double_eq_0_iff 
paulson@15620
   358
              Ints_odd_nonzero Ints_def split: bit.split)
paulson@15013
   359
paulson@15013
   360
lemma iszero_number_of_0:
paulson@15620
   361
     "iszero (number_of (w BIT bit.B0) :: 'a::{ordered_idom,number_ring}) = 
paulson@15013
   362
      iszero (number_of w :: 'a)"
paulson@15013
   363
by (simp only: iszero_number_of_BIT simp_thms)
paulson@15013
   364
paulson@15013
   365
lemma iszero_number_of_1:
paulson@15620
   366
     "~ iszero (number_of (w BIT bit.B1)::'a::{ordered_idom,number_ring})"
paulson@15620
   367
by (simp add: iszero_number_of_BIT) 
paulson@15013
   368
paulson@15013
   369
paulson@15013
   370
subsection{*The Less-Than Relation*}
paulson@15013
   371
paulson@15013
   372
lemma less_number_of_eq_neg:
paulson@15013
   373
    "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
paulson@15013
   374
     = neg (number_of (bin_add x (bin_minus y)) :: 'a)"
paulson@15013
   375
apply (subst less_iff_diff_less_0) 
paulson@15013
   376
apply (simp add: neg_def diff_minus number_of_add number_of_minus)
paulson@15013
   377
done
paulson@15013
   378
paulson@15013
   379
text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
paulson@15013
   380
  @{term Numeral0} IS @{term "number_of Numeral.Pls"} *}
paulson@15013
   381
lemma not_neg_number_of_Pls:
paulson@15013
   382
     "~ neg (number_of Numeral.Pls ::'a::{ordered_idom,number_ring})"
paulson@15013
   383
by (simp add: neg_def numeral_0_eq_0)
paulson@15013
   384
paulson@15013
   385
lemma neg_number_of_Min:
paulson@15013
   386
     "neg (number_of Numeral.Min ::'a::{ordered_idom,number_ring})"
paulson@15013
   387
by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
paulson@15013
   388
paulson@15013
   389
lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
paulson@15013
   390
proof -
paulson@15013
   391
  have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
paulson@15013
   392
  also have "... = (a < 0)"
paulson@15013
   393
    by (simp add: mult_less_0_iff zero_less_two 
paulson@15013
   394
                  order_less_not_sym [OF zero_less_two]) 
paulson@15013
   395
  finally show ?thesis .
paulson@15013
   396
qed
paulson@15013
   397
paulson@15013
   398
lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))";
paulson@15013
   399
proof (cases z rule: int_cases)
paulson@15013
   400
  case (nonneg n)
paulson@15013
   401
  thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
paulson@15013
   402
                             le_imp_0_less [THEN order_less_imp_le])  
paulson@15013
   403
next
paulson@15013
   404
  case (neg n)
paulson@15013
   405
  thus ?thesis by (simp del: int_Suc
paulson@15013
   406
			add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
paulson@15013
   407
qed
paulson@15013
   408
paulson@15013
   409
text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
paulson@15013
   410
lemma Ints_odd_less_0: 
paulson@15013
   411
     "a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
paulson@15013
   412
proof (unfold Ints_def) 
paulson@15013
   413
  assume "a \<in> range of_int"
paulson@15013
   414
  then obtain z where a: "a = of_int z" ..
paulson@15013
   415
  hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
paulson@15013
   416
    by (simp add: a)
paulson@15013
   417
  also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
paulson@15013
   418
  also have "... = (a < 0)" by (simp add: a)
paulson@15013
   419
  finally show ?thesis .
paulson@15013
   420
qed
paulson@15013
   421
paulson@15013
   422
lemma neg_number_of_BIT:
paulson@15013
   423
     "neg (number_of (w BIT x)::'a) = 
paulson@15013
   424
      neg (number_of w :: 'a::{ordered_idom,number_ring})"
paulson@15013
   425
by (simp add: neg_def number_of_eq Bin_simps double_less_0_iff
paulson@15620
   426
              Ints_odd_less_0 Ints_def split: bit.split)
paulson@15013
   427
paulson@15013
   428
paulson@15013
   429
text{*Less-Than or Equals*}
paulson@15013
   430
paulson@15013
   431
text{*Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals*}
paulson@15013
   432
lemmas le_number_of_eq_not_less =
paulson@15013
   433
       linorder_not_less [of "number_of w" "number_of v", symmetric, 
paulson@15013
   434
                          standard]
paulson@15013
   435
paulson@15013
   436
lemma le_number_of_eq:
paulson@15013
   437
    "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
paulson@15013
   438
     = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"
paulson@15013
   439
by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
paulson@15013
   440
paulson@15013
   441
paulson@15013
   442
text{*Absolute value (@{term abs})*}
paulson@15013
   443
paulson@15013
   444
lemma abs_number_of:
paulson@15013
   445
     "abs(number_of x::'a::{ordered_idom,number_ring}) =
paulson@15013
   446
      (if number_of x < (0::'a) then -number_of x else number_of x)"
paulson@15013
   447
by (simp add: abs_if)
paulson@15013
   448
paulson@15013
   449
paulson@15013
   450
text{*Re-orientation of the equation nnn=x*}
paulson@15013
   451
lemma number_of_reorient: "(number_of w = x) = (x = number_of w)"
paulson@15013
   452
by auto
paulson@15013
   453
paulson@15013
   454
paulson@15013
   455
paulson@15013
   456
paulson@15013
   457
subsection{*Simplification of arithmetic operations on integer constants.*}
paulson@15013
   458
paulson@15013
   459
lemmas bin_arith_extra_simps = 
paulson@15013
   460
       number_of_add [symmetric]
paulson@15013
   461
       number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
paulson@15013
   462
       number_of_mult [symmetric]
paulson@15013
   463
       diff_number_of_eq abs_number_of 
paulson@15013
   464
paulson@15013
   465
text{*For making a minimal simpset, one must include these default simprules.
paulson@15620
   466
  Also include @{text simp_thms} *}
paulson@15013
   467
lemmas bin_arith_simps = 
paulson@15620
   468
       Numeral.bit.distinct
paulson@15013
   469
       Pls_0_eq Min_1_eq
paulson@15013
   470
       bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
paulson@15013
   471
       bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
paulson@15013
   472
       bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
paulson@15013
   473
       bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
paulson@15013
   474
       bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0 
paulson@15013
   475
       bin_add_Pls_right bin_add_Min_right
paulson@15013
   476
       abs_zero abs_one bin_arith_extra_simps
paulson@15013
   477
paulson@15013
   478
text{*Simplification of relational operations*}
paulson@15013
   479
lemmas bin_rel_simps = 
paulson@15013
   480
       eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
paulson@15013
   481
       iszero_number_of_0 iszero_number_of_1
paulson@15013
   482
       less_number_of_eq_neg
paulson@15013
   483
       not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
paulson@15013
   484
       neg_number_of_Min neg_number_of_BIT
paulson@15013
   485
       le_number_of_eq
paulson@15013
   486
paulson@15013
   487
declare bin_arith_extra_simps [simp]
paulson@15013
   488
declare bin_rel_simps [simp]
paulson@15013
   489
paulson@15013
   490
paulson@15013
   491
subsection{*Simplification of arithmetic when nested to the right*}
paulson@15013
   492
paulson@15013
   493
lemma add_number_of_left [simp]:
paulson@15013
   494
     "number_of v + (number_of w + z) =
paulson@15013
   495
      (number_of(bin_add v w) + z::'a::number_ring)"
paulson@15013
   496
by (simp add: add_assoc [symmetric])
paulson@15013
   497
paulson@15013
   498
lemma mult_number_of_left [simp]:
paulson@15013
   499
    "number_of v * (number_of w * z) =
paulson@15013
   500
     (number_of(bin_mult v w) * z::'a::number_ring)"
paulson@15013
   501
by (simp add: mult_assoc [symmetric])
paulson@15013
   502
paulson@15013
   503
lemma add_number_of_diff1:
paulson@15013
   504
    "number_of v + (number_of w - c) = 
paulson@15013
   505
     number_of(bin_add v w) - (c::'a::number_ring)"
paulson@15013
   506
by (simp add: diff_minus add_number_of_left)
paulson@15013
   507
paulson@15013
   508
lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) =
paulson@15013
   509
     number_of (bin_add v (bin_minus w)) + (c::'a::number_ring)"
paulson@15013
   510
apply (subst diff_number_of_eq [symmetric])
paulson@15013
   511
apply (simp only: compare_rls)
paulson@15013
   512
done
paulson@15013
   513
paulson@15013
   514
end