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