src/HOL/Numeral.thy
author haftmann
Wed Sep 26 20:27:55 2007 +0200 (2007-09-26)
changeset 24728 e2b3a1065676
parent 24630 351a308ab58d
child 25089 04b8456f7754
permissions -rw-r--r--
moved Finite_Set before Datatype
wenzelm@23164
     1
(*  Title:      HOL/Numeral.thy
wenzelm@23164
     2
    ID:         $Id$
wenzelm@23164
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@23164
     4
    Copyright   1994  University of Cambridge
wenzelm@23164
     5
*)
wenzelm@23164
     6
wenzelm@23164
     7
header {* Arithmetic on Binary Integers *}
wenzelm@23164
     8
wenzelm@23164
     9
theory Numeral
haftmann@23708
    10
imports Datatype IntDef
wenzelm@23574
    11
uses
wenzelm@23574
    12
  ("Tools/numeral.ML")
wenzelm@23574
    13
  ("Tools/numeral_syntax.ML")
wenzelm@23164
    14
begin
wenzelm@23164
    15
wenzelm@23164
    16
subsection {* Binary representation *}
wenzelm@23164
    17
wenzelm@23164
    18
text {*
wenzelm@23164
    19
  This formalization defines binary arithmetic in terms of the integers
wenzelm@23164
    20
  rather than using a datatype. This avoids multiple representations (leading
wenzelm@23164
    21
  zeroes, etc.)  See @{text "ZF/Tools/twos-compl.ML"}, function @{text
wenzelm@23164
    22
  int_of_binary}, for the numerical interpretation.
wenzelm@23164
    23
wenzelm@23164
    24
  The representation expects that @{text "(m mod 2)"} is 0 or 1,
wenzelm@23164
    25
  even if m is negative;
wenzelm@23164
    26
  For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
wenzelm@23164
    27
  @{text "-5 = (-3)*2 + 1"}.
wenzelm@23164
    28
*}
wenzelm@23164
    29
wenzelm@23164
    30
datatype bit = B0 | B1
wenzelm@23164
    31
wenzelm@23164
    32
text{*
wenzelm@23164
    33
  Type @{typ bit} avoids the use of type @{typ bool}, which would make
wenzelm@23164
    34
  all of the rewrite rules higher-order.
wenzelm@23164
    35
*}
wenzelm@23164
    36
wenzelm@23164
    37
definition
wenzelm@23164
    38
  Pls :: int where
haftmann@24166
    39
  [code func del]: "Pls = 0"
wenzelm@23164
    40
wenzelm@23164
    41
definition
wenzelm@23164
    42
  Min :: int where
haftmann@24166
    43
  [code func del]: "Min = - 1"
wenzelm@23164
    44
wenzelm@23164
    45
definition
wenzelm@23164
    46
  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
wenzelm@23164
    47
  [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
wenzelm@23164
    48
wenzelm@23164
    49
class number = type + -- {* for numeric types: nat, int, real, \dots *}
wenzelm@23164
    50
  fixes number_of :: "int \<Rightarrow> 'a"
wenzelm@23164
    51
wenzelm@23574
    52
use "Tools/numeral.ML"
wenzelm@23574
    53
wenzelm@23164
    54
syntax
wenzelm@23164
    55
  "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")
wenzelm@23164
    56
wenzelm@23164
    57
use "Tools/numeral_syntax.ML"
wenzelm@23164
    58
setup NumeralSyntax.setup
wenzelm@23164
    59
wenzelm@23164
    60
abbreviation
wenzelm@23164
    61
  "Numeral0 \<equiv> number_of Pls"
wenzelm@23164
    62
wenzelm@23164
    63
abbreviation
wenzelm@23164
    64
  "Numeral1 \<equiv> number_of (Pls BIT B1)"
wenzelm@23164
    65
wenzelm@23164
    66
lemma Let_number_of [simp]: "Let (number_of v) f = f (number_of v)"
wenzelm@23164
    67
  -- {* Unfold all @{text let}s involving constants *}
wenzelm@23164
    68
  unfolding Let_def ..
wenzelm@23164
    69
wenzelm@23164
    70
definition
wenzelm@23164
    71
  succ :: "int \<Rightarrow> int" where
wenzelm@23164
    72
  [code func del]: "succ k = k + 1"
wenzelm@23164
    73
wenzelm@23164
    74
definition
wenzelm@23164
    75
  pred :: "int \<Rightarrow> int" where
wenzelm@23164
    76
  [code func del]: "pred k = k - 1"
wenzelm@23164
    77
wenzelm@23164
    78
lemmas
wenzelm@23164
    79
  max_number_of [simp] = max_def
wenzelm@23164
    80
    [of "number_of u" "number_of v", standard, simp]
wenzelm@23164
    81
and
wenzelm@23164
    82
  min_number_of [simp] = min_def 
wenzelm@23164
    83
    [of "number_of u" "number_of v", standard, simp]
wenzelm@23164
    84
  -- {* unfolding @{text minx} and @{text max} on numerals *}
wenzelm@23164
    85
wenzelm@23164
    86
lemmas numeral_simps = 
wenzelm@23164
    87
  succ_def pred_def Pls_def Min_def Bit_def
wenzelm@23164
    88
wenzelm@23164
    89
text {* Removal of leading zeroes *}
wenzelm@23164
    90
haftmann@24166
    91
lemma Pls_0_eq [simp, code post]:
wenzelm@23164
    92
  "Pls BIT B0 = Pls"
wenzelm@23164
    93
  unfolding numeral_simps by simp
wenzelm@23164
    94
haftmann@24166
    95
lemma Min_1_eq [simp, code post]:
wenzelm@23164
    96
  "Min BIT B1 = Min"
wenzelm@23164
    97
  unfolding numeral_simps by simp
wenzelm@23164
    98
wenzelm@23164
    99
wenzelm@23164
   100
subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}
wenzelm@23164
   101
wenzelm@23164
   102
lemma succ_Pls [simp]:
wenzelm@23164
   103
  "succ Pls = Pls BIT B1"
wenzelm@23164
   104
  unfolding numeral_simps by simp
wenzelm@23164
   105
wenzelm@23164
   106
lemma succ_Min [simp]:
wenzelm@23164
   107
  "succ Min = Pls"
wenzelm@23164
   108
  unfolding numeral_simps by simp
wenzelm@23164
   109
wenzelm@23164
   110
lemma succ_1 [simp]:
wenzelm@23164
   111
  "succ (k BIT B1) = succ k BIT B0"
wenzelm@23164
   112
  unfolding numeral_simps by simp
wenzelm@23164
   113
wenzelm@23164
   114
lemma succ_0 [simp]:
wenzelm@23164
   115
  "succ (k BIT B0) = k BIT B1"
wenzelm@23164
   116
  unfolding numeral_simps by simp
wenzelm@23164
   117
wenzelm@23164
   118
lemma pred_Pls [simp]:
wenzelm@23164
   119
  "pred Pls = Min"
wenzelm@23164
   120
  unfolding numeral_simps by simp
wenzelm@23164
   121
wenzelm@23164
   122
lemma pred_Min [simp]:
wenzelm@23164
   123
  "pred Min = Min BIT B0"
wenzelm@23164
   124
  unfolding numeral_simps by simp
wenzelm@23164
   125
wenzelm@23164
   126
lemma pred_1 [simp]:
wenzelm@23164
   127
  "pred (k BIT B1) = k BIT B0"
wenzelm@23164
   128
  unfolding numeral_simps by simp
wenzelm@23164
   129
wenzelm@23164
   130
lemma pred_0 [simp]:
wenzelm@23164
   131
  "pred (k BIT B0) = pred k BIT B1"
wenzelm@23164
   132
  unfolding numeral_simps by simp 
wenzelm@23164
   133
wenzelm@23164
   134
lemma minus_Pls [simp]:
wenzelm@23164
   135
  "- Pls = Pls"
wenzelm@23164
   136
  unfolding numeral_simps by simp 
wenzelm@23164
   137
wenzelm@23164
   138
lemma minus_Min [simp]:
wenzelm@23164
   139
  "- Min = Pls BIT B1"
wenzelm@23164
   140
  unfolding numeral_simps by simp 
wenzelm@23164
   141
wenzelm@23164
   142
lemma minus_1 [simp]:
wenzelm@23164
   143
  "- (k BIT B1) = pred (- k) BIT B1"
wenzelm@23164
   144
  unfolding numeral_simps by simp 
wenzelm@23164
   145
wenzelm@23164
   146
lemma minus_0 [simp]:
wenzelm@23164
   147
  "- (k BIT B0) = (- k) BIT B0"
wenzelm@23164
   148
  unfolding numeral_simps by simp 
wenzelm@23164
   149
wenzelm@23164
   150
wenzelm@23164
   151
subsection {*
wenzelm@23164
   152
  Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
wenzelm@23164
   153
    and @{term "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
wenzelm@23164
   154
*}
wenzelm@23164
   155
wenzelm@23164
   156
lemma add_Pls [simp]:
wenzelm@23164
   157
  "Pls + k = k"
wenzelm@23164
   158
  unfolding numeral_simps by simp 
wenzelm@23164
   159
wenzelm@23164
   160
lemma add_Min [simp]:
wenzelm@23164
   161
  "Min + k = pred k"
wenzelm@23164
   162
  unfolding numeral_simps by simp
wenzelm@23164
   163
wenzelm@23164
   164
lemma add_BIT_11 [simp]:
wenzelm@23164
   165
  "(k BIT B1) + (l BIT B1) = (k + succ l) BIT B0"
wenzelm@23164
   166
  unfolding numeral_simps by simp
wenzelm@23164
   167
wenzelm@23164
   168
lemma add_BIT_10 [simp]:
wenzelm@23164
   169
  "(k BIT B1) + (l BIT B0) = (k + l) BIT B1"
wenzelm@23164
   170
  unfolding numeral_simps by simp
wenzelm@23164
   171
wenzelm@23164
   172
lemma add_BIT_0 [simp]:
wenzelm@23164
   173
  "(k BIT B0) + (l BIT b) = (k + l) BIT b"
wenzelm@23164
   174
  unfolding numeral_simps by simp 
wenzelm@23164
   175
wenzelm@23164
   176
lemma add_Pls_right [simp]:
wenzelm@23164
   177
  "k + Pls = k"
wenzelm@23164
   178
  unfolding numeral_simps by simp 
wenzelm@23164
   179
wenzelm@23164
   180
lemma add_Min_right [simp]:
wenzelm@23164
   181
  "k + Min = pred k"
wenzelm@23164
   182
  unfolding numeral_simps by simp 
wenzelm@23164
   183
wenzelm@23164
   184
lemma mult_Pls [simp]:
wenzelm@23164
   185
  "Pls * w = Pls"
wenzelm@23164
   186
  unfolding numeral_simps by simp 
wenzelm@23164
   187
wenzelm@23164
   188
lemma mult_Min [simp]:
wenzelm@23164
   189
  "Min * k = - k"
wenzelm@23164
   190
  unfolding numeral_simps by simp 
wenzelm@23164
   191
wenzelm@23164
   192
lemma mult_num1 [simp]:
wenzelm@23164
   193
  "(k BIT B1) * l = ((k * l) BIT B0) + l"
wenzelm@23164
   194
  unfolding numeral_simps int_distrib by simp 
wenzelm@23164
   195
wenzelm@23164
   196
lemma mult_num0 [simp]:
wenzelm@23164
   197
  "(k BIT B0) * l = (k * l) BIT B0"
wenzelm@23164
   198
  unfolding numeral_simps int_distrib by simp 
wenzelm@23164
   199
wenzelm@23164
   200
wenzelm@23164
   201
wenzelm@23164
   202
subsection {* Converting Numerals to Rings: @{term number_of} *}
wenzelm@23164
   203
wenzelm@23164
   204
axclass number_ring \<subseteq> number, comm_ring_1
wenzelm@23164
   205
  number_of_eq: "number_of k = of_int k"
wenzelm@23164
   206
haftmann@23855
   207
text {* self-embedding of the integers *}
wenzelm@23164
   208
wenzelm@23164
   209
instance int :: number_ring
wenzelm@23164
   210
  int_number_of_def: "number_of w \<equiv> of_int w"
wenzelm@23164
   211
  by intro_classes (simp only: int_number_of_def)
wenzelm@23164
   212
wenzelm@23164
   213
lemmas [code func del] = int_number_of_def
wenzelm@23164
   214
wenzelm@23164
   215
lemma number_of_is_id:
wenzelm@23164
   216
  "number_of (k::int) = k"
wenzelm@23164
   217
  unfolding int_number_of_def by simp
wenzelm@23164
   218
wenzelm@23164
   219
lemma number_of_succ:
wenzelm@23164
   220
  "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
wenzelm@23164
   221
  unfolding number_of_eq numeral_simps by simp
wenzelm@23164
   222
wenzelm@23164
   223
lemma number_of_pred:
wenzelm@23164
   224
  "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
wenzelm@23164
   225
  unfolding number_of_eq numeral_simps by simp
wenzelm@23164
   226
wenzelm@23164
   227
lemma number_of_minus:
wenzelm@23164
   228
  "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
wenzelm@23164
   229
  unfolding number_of_eq numeral_simps by simp
wenzelm@23164
   230
wenzelm@23164
   231
lemma number_of_add:
wenzelm@23164
   232
  "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
wenzelm@23164
   233
  unfolding number_of_eq numeral_simps by simp
wenzelm@23164
   234
wenzelm@23164
   235
lemma number_of_mult:
wenzelm@23164
   236
  "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
wenzelm@23164
   237
  unfolding number_of_eq numeral_simps by simp
wenzelm@23164
   238
wenzelm@23164
   239
text {*
wenzelm@23164
   240
  The correctness of shifting.
wenzelm@23164
   241
  But it doesn't seem to give a measurable speed-up.
wenzelm@23164
   242
*}
wenzelm@23164
   243
wenzelm@23164
   244
lemma double_number_of_BIT:
wenzelm@23164
   245
  "(1 + 1) * number_of w = (number_of (w BIT B0) ::'a::number_ring)"
wenzelm@23164
   246
  unfolding number_of_eq numeral_simps left_distrib by simp
wenzelm@23164
   247
wenzelm@23164
   248
text {*
wenzelm@23164
   249
  Converting numerals 0 and 1 to their abstract versions.
wenzelm@23164
   250
*}
wenzelm@23164
   251
wenzelm@23164
   252
lemma numeral_0_eq_0 [simp]:
wenzelm@23164
   253
  "Numeral0 = (0::'a::number_ring)"
wenzelm@23164
   254
  unfolding number_of_eq numeral_simps by simp
wenzelm@23164
   255
wenzelm@23164
   256
lemma numeral_1_eq_1 [simp]:
wenzelm@23164
   257
  "Numeral1 = (1::'a::number_ring)"
wenzelm@23164
   258
  unfolding number_of_eq numeral_simps by simp
wenzelm@23164
   259
wenzelm@23164
   260
text {*
wenzelm@23164
   261
  Special-case simplification for small constants.
wenzelm@23164
   262
*}
wenzelm@23164
   263
wenzelm@23164
   264
text{*
wenzelm@23164
   265
  Unary minus for the abstract constant 1. Cannot be inserted
wenzelm@23164
   266
  as a simprule until later: it is @{text number_of_Min} re-oriented!
wenzelm@23164
   267
*}
wenzelm@23164
   268
wenzelm@23164
   269
lemma numeral_m1_eq_minus_1:
wenzelm@23164
   270
  "(-1::'a::number_ring) = - 1"
wenzelm@23164
   271
  unfolding number_of_eq numeral_simps by simp
wenzelm@23164
   272
wenzelm@23164
   273
lemma mult_minus1 [simp]:
wenzelm@23164
   274
  "-1 * z = -(z::'a::number_ring)"
wenzelm@23164
   275
  unfolding number_of_eq numeral_simps by simp
wenzelm@23164
   276
wenzelm@23164
   277
lemma mult_minus1_right [simp]:
wenzelm@23164
   278
  "z * -1 = -(z::'a::number_ring)"
wenzelm@23164
   279
  unfolding number_of_eq numeral_simps by simp
wenzelm@23164
   280
wenzelm@23164
   281
(*Negation of a coefficient*)
wenzelm@23164
   282
lemma minus_number_of_mult [simp]:
wenzelm@23164
   283
   "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
wenzelm@23164
   284
   unfolding number_of_eq by simp
wenzelm@23164
   285
wenzelm@23164
   286
text {* Subtraction *}
wenzelm@23164
   287
wenzelm@23164
   288
lemma diff_number_of_eq:
wenzelm@23164
   289
  "number_of v - number_of w =
wenzelm@23164
   290
    (number_of (v + uminus w)::'a::number_ring)"
wenzelm@23164
   291
  unfolding number_of_eq by simp
wenzelm@23164
   292
wenzelm@23164
   293
lemma number_of_Pls:
wenzelm@23164
   294
  "number_of Pls = (0::'a::number_ring)"
wenzelm@23164
   295
  unfolding number_of_eq numeral_simps by simp
wenzelm@23164
   296
wenzelm@23164
   297
lemma number_of_Min:
wenzelm@23164
   298
  "number_of Min = (- 1::'a::number_ring)"
wenzelm@23164
   299
  unfolding number_of_eq numeral_simps by simp
wenzelm@23164
   300
wenzelm@23164
   301
lemma number_of_BIT:
wenzelm@23164
   302
  "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring))
wenzelm@23164
   303
    + (number_of w) + (number_of w)"
wenzelm@23164
   304
  unfolding number_of_eq numeral_simps by (simp split: bit.split)
wenzelm@23164
   305
wenzelm@23164
   306
wenzelm@23164
   307
subsection {* Equality of Binary Numbers *}
wenzelm@23164
   308
wenzelm@23164
   309
text {* First version by Norbert Voelker *}
wenzelm@23164
   310
wenzelm@23164
   311
lemma eq_number_of_eq:
wenzelm@23164
   312
  "((number_of x::'a::number_ring) = number_of y) =
wenzelm@23164
   313
   iszero (number_of (x + uminus y) :: 'a)"
wenzelm@23164
   314
  unfolding iszero_def number_of_add number_of_minus
wenzelm@23164
   315
  by (simp add: compare_rls)
wenzelm@23164
   316
wenzelm@23164
   317
lemma iszero_number_of_Pls:
wenzelm@23164
   318
  "iszero ((number_of Pls)::'a::number_ring)"
wenzelm@23164
   319
  unfolding iszero_def numeral_0_eq_0 ..
wenzelm@23164
   320
wenzelm@23164
   321
lemma nonzero_number_of_Min:
wenzelm@23164
   322
  "~ iszero ((number_of Min)::'a::number_ring)"
wenzelm@23164
   323
  unfolding iszero_def numeral_m1_eq_minus_1 by simp
wenzelm@23164
   324
wenzelm@23164
   325
wenzelm@23164
   326
subsection {* Comparisons, for Ordered Rings *}
wenzelm@23164
   327
wenzelm@23164
   328
lemma double_eq_0_iff:
wenzelm@23164
   329
  "(a + a = 0) = (a = (0::'a::ordered_idom))"
wenzelm@23164
   330
proof -
wenzelm@23164
   331
  have "a + a = (1 + 1) * a" unfolding left_distrib by simp
wenzelm@23164
   332
  with zero_less_two [where 'a = 'a]
wenzelm@23164
   333
  show ?thesis by force
wenzelm@23164
   334
qed
wenzelm@23164
   335
wenzelm@23164
   336
lemma le_imp_0_less: 
wenzelm@23164
   337
  assumes le: "0 \<le> z"
wenzelm@23164
   338
  shows "(0::int) < 1 + z"
wenzelm@23164
   339
proof -
wenzelm@23389
   340
  have "0 \<le> z" by fact
wenzelm@23164
   341
  also have "... < z + 1" by (rule less_add_one) 
wenzelm@23164
   342
  also have "... = 1 + z" by (simp add: add_ac)
wenzelm@23164
   343
  finally show "0 < 1 + z" .
wenzelm@23164
   344
qed
wenzelm@23164
   345
wenzelm@23164
   346
lemma odd_nonzero:
wenzelm@23164
   347
  "1 + z + z \<noteq> (0::int)";
wenzelm@23164
   348
proof (cases z rule: int_cases)
wenzelm@23164
   349
  case (nonneg n)
wenzelm@23164
   350
  have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
wenzelm@23164
   351
  thus ?thesis using  le_imp_0_less [OF le]
wenzelm@23164
   352
    by (auto simp add: add_assoc) 
wenzelm@23164
   353
next
wenzelm@23164
   354
  case (neg n)
wenzelm@23164
   355
  show ?thesis
wenzelm@23164
   356
  proof
wenzelm@23164
   357
    assume eq: "1 + z + z = 0"
wenzelm@23164
   358
    have "0 < 1 + (int n + int n)"
wenzelm@23164
   359
      by (simp add: le_imp_0_less add_increasing) 
wenzelm@23164
   360
    also have "... = - (1 + z + z)" 
wenzelm@23164
   361
      by (simp add: neg add_assoc [symmetric]) 
wenzelm@23164
   362
    also have "... = 0" by (simp add: eq) 
wenzelm@23164
   363
    finally have "0<0" ..
wenzelm@23164
   364
    thus False by blast
wenzelm@23164
   365
  qed
wenzelm@23164
   366
qed
wenzelm@23164
   367
wenzelm@23164
   368
text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
wenzelm@23164
   369
wenzelm@23164
   370
lemma Ints_double_eq_0_iff:
wenzelm@23164
   371
  assumes in_Ints: "a \<in> Ints"
wenzelm@23164
   372
  shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
wenzelm@23164
   373
proof -
wenzelm@23164
   374
  from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
wenzelm@23164
   375
  then obtain z where a: "a = of_int z" ..
wenzelm@23164
   376
  show ?thesis
wenzelm@23164
   377
  proof
wenzelm@23164
   378
    assume "a = 0"
wenzelm@23164
   379
    thus "a + a = 0" by simp
wenzelm@23164
   380
  next
wenzelm@23164
   381
    assume eq: "a + a = 0"
wenzelm@23164
   382
    hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
wenzelm@23164
   383
    hence "z + z = 0" by (simp only: of_int_eq_iff)
wenzelm@23164
   384
    hence "z = 0" by (simp only: double_eq_0_iff)
wenzelm@23164
   385
    thus "a = 0" by (simp add: a)
wenzelm@23164
   386
  qed
wenzelm@23164
   387
qed
wenzelm@23164
   388
wenzelm@23164
   389
lemma Ints_odd_nonzero:
wenzelm@23164
   390
  assumes in_Ints: "a \<in> Ints"
wenzelm@23164
   391
  shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
wenzelm@23164
   392
proof -
wenzelm@23164
   393
  from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
wenzelm@23164
   394
  then obtain z where a: "a = of_int z" ..
wenzelm@23164
   395
  show ?thesis
wenzelm@23164
   396
  proof
wenzelm@23164
   397
    assume eq: "1 + a + a = 0"
wenzelm@23164
   398
    hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
wenzelm@23164
   399
    hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
wenzelm@23164
   400
    with odd_nonzero show False by blast
wenzelm@23164
   401
  qed
wenzelm@23164
   402
qed 
wenzelm@23164
   403
wenzelm@23164
   404
lemma Ints_number_of:
wenzelm@23164
   405
  "(number_of w :: 'a::number_ring) \<in> Ints"
wenzelm@23164
   406
  unfolding number_of_eq Ints_def by simp
wenzelm@23164
   407
wenzelm@23164
   408
lemma iszero_number_of_BIT:
wenzelm@23164
   409
  "iszero (number_of (w BIT x)::'a) = 
wenzelm@23164
   410
   (x = B0 \<and> iszero (number_of w::'a::{ring_char_0,number_ring}))"
wenzelm@23164
   411
  by (simp add: iszero_def number_of_eq numeral_simps Ints_double_eq_0_iff 
wenzelm@23164
   412
    Ints_odd_nonzero Ints_def split: bit.split)
wenzelm@23164
   413
wenzelm@23164
   414
lemma iszero_number_of_0:
wenzelm@23164
   415
  "iszero (number_of (w BIT B0) :: 'a::{ring_char_0,number_ring}) = 
wenzelm@23164
   416
  iszero (number_of w :: 'a)"
wenzelm@23164
   417
  by (simp only: iszero_number_of_BIT simp_thms)
wenzelm@23164
   418
wenzelm@23164
   419
lemma iszero_number_of_1:
wenzelm@23164
   420
  "~ iszero (number_of (w BIT B1)::'a::{ring_char_0,number_ring})"
wenzelm@23164
   421
  by (simp add: iszero_number_of_BIT) 
wenzelm@23164
   422
wenzelm@23164
   423
wenzelm@23164
   424
subsection {* The Less-Than Relation *}
wenzelm@23164
   425
wenzelm@23164
   426
lemma less_number_of_eq_neg:
wenzelm@23164
   427
  "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
wenzelm@23164
   428
  = neg (number_of (x + uminus y) :: 'a)"
wenzelm@23164
   429
apply (subst less_iff_diff_less_0) 
wenzelm@23164
   430
apply (simp add: neg_def diff_minus number_of_add number_of_minus)
wenzelm@23164
   431
done
wenzelm@23164
   432
wenzelm@23164
   433
text {*
wenzelm@23164
   434
  If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
wenzelm@23164
   435
  @{term Numeral0} IS @{term "number_of Pls"}
wenzelm@23164
   436
*}
wenzelm@23164
   437
wenzelm@23164
   438
lemma not_neg_number_of_Pls:
wenzelm@23164
   439
  "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
wenzelm@23164
   440
  by (simp add: neg_def numeral_0_eq_0)
wenzelm@23164
   441
wenzelm@23164
   442
lemma neg_number_of_Min:
wenzelm@23164
   443
  "neg (number_of Min ::'a::{ordered_idom,number_ring})"
wenzelm@23164
   444
  by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
wenzelm@23164
   445
wenzelm@23164
   446
lemma double_less_0_iff:
wenzelm@23164
   447
  "(a + a < 0) = (a < (0::'a::ordered_idom))"
wenzelm@23164
   448
proof -
wenzelm@23164
   449
  have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
wenzelm@23164
   450
  also have "... = (a < 0)"
wenzelm@23164
   451
    by (simp add: mult_less_0_iff zero_less_two 
wenzelm@23164
   452
                  order_less_not_sym [OF zero_less_two]) 
wenzelm@23164
   453
  finally show ?thesis .
wenzelm@23164
   454
qed
wenzelm@23164
   455
wenzelm@23164
   456
lemma odd_less_0:
wenzelm@23164
   457
  "(1 + z + z < 0) = (z < (0::int))";
huffman@23365
   458
proof (cases z rule: int_cases)
wenzelm@23164
   459
  case (nonneg n)
wenzelm@23164
   460
  thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
wenzelm@23164
   461
                             le_imp_0_less [THEN order_less_imp_le])  
wenzelm@23164
   462
next
wenzelm@23164
   463
  case (neg n)
huffman@23307
   464
  thus ?thesis by (simp del: of_nat_Suc of_nat_add
huffman@23307
   465
    add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
wenzelm@23164
   466
qed
wenzelm@23164
   467
wenzelm@23164
   468
text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
wenzelm@23164
   469
wenzelm@23164
   470
lemma Ints_odd_less_0: 
wenzelm@23164
   471
  assumes in_Ints: "a \<in> Ints"
wenzelm@23164
   472
  shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))";
wenzelm@23164
   473
proof -
wenzelm@23164
   474
  from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
wenzelm@23164
   475
  then obtain z where a: "a = of_int z" ..
wenzelm@23164
   476
  hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
wenzelm@23164
   477
    by (simp add: a)
wenzelm@23164
   478
  also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
wenzelm@23164
   479
  also have "... = (a < 0)" by (simp add: a)
wenzelm@23164
   480
  finally show ?thesis .
wenzelm@23164
   481
qed
wenzelm@23164
   482
wenzelm@23164
   483
lemma neg_number_of_BIT:
wenzelm@23164
   484
  "neg (number_of (w BIT x)::'a) = 
wenzelm@23164
   485
  neg (number_of w :: 'a::{ordered_idom,number_ring})"
wenzelm@23164
   486
  by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff
wenzelm@23164
   487
    Ints_odd_less_0 Ints_def split: bit.split)
wenzelm@23164
   488
wenzelm@23164
   489
wenzelm@23164
   490
text {* Less-Than or Equals *}
wenzelm@23164
   491
wenzelm@23164
   492
text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
wenzelm@23164
   493
wenzelm@23164
   494
lemmas le_number_of_eq_not_less =
wenzelm@23164
   495
  linorder_not_less [of "number_of w" "number_of v", symmetric, 
wenzelm@23164
   496
  standard]
wenzelm@23164
   497
wenzelm@23164
   498
lemma le_number_of_eq:
wenzelm@23164
   499
    "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
wenzelm@23164
   500
     = (~ (neg (number_of (y + uminus x) :: 'a)))"
wenzelm@23164
   501
by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
wenzelm@23164
   502
wenzelm@23164
   503
wenzelm@23164
   504
text {* Absolute value (@{term abs}) *}
wenzelm@23164
   505
wenzelm@23164
   506
lemma abs_number_of:
wenzelm@23164
   507
  "abs(number_of x::'a::{ordered_idom,number_ring}) =
wenzelm@23164
   508
   (if number_of x < (0::'a) then -number_of x else number_of x)"
wenzelm@23164
   509
  by (simp add: abs_if)
wenzelm@23164
   510
wenzelm@23164
   511
wenzelm@23164
   512
text {* Re-orientation of the equation nnn=x *}
wenzelm@23164
   513
wenzelm@23164
   514
lemma number_of_reorient:
wenzelm@23164
   515
  "(number_of w = x) = (x = number_of w)"
wenzelm@23164
   516
  by auto
wenzelm@23164
   517
wenzelm@23164
   518
wenzelm@23164
   519
subsection {* Simplification of arithmetic operations on integer constants. *}
wenzelm@23164
   520
wenzelm@23164
   521
lemmas arith_extra_simps [standard, simp] =
wenzelm@23164
   522
  number_of_add [symmetric]
wenzelm@23164
   523
  number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
wenzelm@23164
   524
  number_of_mult [symmetric]
wenzelm@23164
   525
  diff_number_of_eq abs_number_of 
wenzelm@23164
   526
wenzelm@23164
   527
text {*
wenzelm@23164
   528
  For making a minimal simpset, one must include these default simprules.
wenzelm@23164
   529
  Also include @{text simp_thms}.
wenzelm@23164
   530
*}
wenzelm@23164
   531
wenzelm@23164
   532
lemmas arith_simps = 
wenzelm@23164
   533
  bit.distinct
wenzelm@23164
   534
  Pls_0_eq Min_1_eq
wenzelm@23164
   535
  pred_Pls pred_Min pred_1 pred_0
wenzelm@23164
   536
  succ_Pls succ_Min succ_1 succ_0
wenzelm@23164
   537
  add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
wenzelm@23164
   538
  minus_Pls minus_Min minus_1 minus_0
wenzelm@23164
   539
  mult_Pls mult_Min mult_num1 mult_num0 
wenzelm@23164
   540
  add_Pls_right add_Min_right
wenzelm@23164
   541
  abs_zero abs_one arith_extra_simps
wenzelm@23164
   542
wenzelm@23164
   543
text {* Simplification of relational operations *}
wenzelm@23164
   544
wenzelm@23164
   545
lemmas rel_simps [simp] = 
huffman@24392
   546
  eq_number_of_eq iszero_0 nonzero_number_of_Min
wenzelm@23164
   547
  iszero_number_of_0 iszero_number_of_1
wenzelm@23164
   548
  less_number_of_eq_neg
wenzelm@23164
   549
  not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
wenzelm@23164
   550
  neg_number_of_Min neg_number_of_BIT
wenzelm@23164
   551
  le_number_of_eq
huffman@24392
   552
(* iszero_number_of_Pls would never be used
huffman@24392
   553
   because its lhs simplifies to "iszero 0" *)
wenzelm@23164
   554
wenzelm@23164
   555
wenzelm@23164
   556
subsection {* Simplification of arithmetic when nested to the right. *}
wenzelm@23164
   557
wenzelm@23164
   558
lemma add_number_of_left [simp]:
wenzelm@23164
   559
  "number_of v + (number_of w + z) =
wenzelm@23164
   560
   (number_of(v + w) + z::'a::number_ring)"
wenzelm@23164
   561
  by (simp add: add_assoc [symmetric])
wenzelm@23164
   562
wenzelm@23164
   563
lemma mult_number_of_left [simp]:
wenzelm@23164
   564
  "number_of v * (number_of w * z) =
wenzelm@23164
   565
   (number_of(v * w) * z::'a::number_ring)"
wenzelm@23164
   566
  by (simp add: mult_assoc [symmetric])
wenzelm@23164
   567
wenzelm@23164
   568
lemma add_number_of_diff1:
wenzelm@23164
   569
  "number_of v + (number_of w - c) = 
wenzelm@23164
   570
  number_of(v + w) - (c::'a::number_ring)"
wenzelm@23164
   571
  by (simp add: diff_minus add_number_of_left)
wenzelm@23164
   572
wenzelm@23164
   573
lemma add_number_of_diff2 [simp]:
wenzelm@23164
   574
  "number_of v + (c - number_of w) =
wenzelm@23164
   575
   number_of (v + uminus w) + (c::'a::number_ring)"
wenzelm@23164
   576
apply (subst diff_number_of_eq [symmetric])
wenzelm@23164
   577
apply (simp only: compare_rls)
wenzelm@23164
   578
done
wenzelm@23164
   579
wenzelm@23164
   580
wenzelm@23164
   581
subsection {* Configuration of the code generator *}
wenzelm@23164
   582
wenzelm@23164
   583
instance int :: eq ..
wenzelm@23164
   584
wenzelm@23164
   585
code_datatype Pls Min Bit "number_of \<Colon> int \<Rightarrow> int"
wenzelm@23164
   586
wenzelm@23164
   587
definition
haftmann@23855
   588
  int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
haftmann@23855
   589
  "int_aux n i = int n + i"
wenzelm@23164
   590
wenzelm@23164
   591
lemma [code]:
haftmann@23855
   592
  "int_aux 0 i  = i"
haftmann@23855
   593
  "int_aux (Suc n) i = int_aux n (i + 1)" -- {* tail recursive *}
wenzelm@23164
   594
  by (simp add: int_aux_def)+
wenzelm@23164
   595
huffman@23365
   596
lemma [code unfold]:
haftmann@23855
   597
  "int n = int_aux n 0"
wenzelm@23164
   598
  by (simp add: int_aux_def)
wenzelm@23164
   599
wenzelm@23164
   600
definition
haftmann@23855
   601
  nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
haftmann@23855
   602
  "nat_aux i n = nat i + n"
wenzelm@23164
   603
haftmann@23855
   604
lemma [code]:
haftmann@23855
   605
  "nat_aux i n = (if i \<le> 0 then n else nat_aux (i - 1) (Suc n))"  -- {* tail recursive *}
wenzelm@23164
   606
  by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
wenzelm@23164
   607
    dest: zless_imp_add1_zle)
wenzelm@23164
   608
haftmann@23855
   609
lemma [code]: "nat i = nat_aux i 0"
wenzelm@23164
   610
  by (simp add: nat_aux_def)
wenzelm@23164
   611
haftmann@24166
   612
lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
haftmann@23855
   613
  "(0\<Colon>int) = Numeral0" 
wenzelm@23164
   614
  by simp
wenzelm@23164
   615
haftmann@24166
   616
lemma one_is_num_one [code func, code inline, symmetric, code post]:
haftmann@23855
   617
  "(1\<Colon>int) = Numeral1" 
wenzelm@23164
   618
  by simp 
wenzelm@23164
   619
wenzelm@23164
   620
code_modulename SML
wenzelm@23164
   621
  IntDef Integer
wenzelm@23164
   622
wenzelm@23164
   623
code_modulename OCaml
wenzelm@23164
   624
  IntDef Integer
wenzelm@23164
   625
wenzelm@23164
   626
code_modulename Haskell
wenzelm@23164
   627
  IntDef Integer
wenzelm@23164
   628
wenzelm@23164
   629
code_modulename SML
wenzelm@23164
   630
  Numeral Integer
wenzelm@23164
   631
wenzelm@23164
   632
code_modulename OCaml
wenzelm@23164
   633
  Numeral Integer
wenzelm@23164
   634
wenzelm@23164
   635
code_modulename Haskell
wenzelm@23164
   636
  Numeral Integer
wenzelm@23164
   637
wenzelm@23164
   638
types_code
wenzelm@23164
   639
  "int" ("int")
wenzelm@23164
   640
attach (term_of) {*
wenzelm@24630
   641
val term_of_int = HOLogic.mk_number HOLogic.intT;
wenzelm@23164
   642
*}
wenzelm@23164
   643
attach (test) {*
wenzelm@23164
   644
fun gen_int i = one_of [~1, 1] * random_range 0 i;
wenzelm@23164
   645
*}
wenzelm@23164
   646
wenzelm@23164
   647
setup {*
wenzelm@23164
   648
let
wenzelm@23164
   649
berghofe@24541
   650
fun strip_number_of (@{term "Numeral.number_of :: int => int"} $ t) = t
berghofe@24541
   651
  | strip_number_of t = t;
berghofe@24541
   652
berghofe@24541
   653
fun numeral_codegen thy defs gr dep module b t =
berghofe@24541
   654
  let val i = HOLogic.dest_numeral (strip_number_of t)
berghofe@24541
   655
  in
berghofe@24541
   656
    SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)),
wenzelm@24630
   657
      Pretty.str (string_of_int i))
berghofe@24541
   658
  end handle TERM _ => NONE;
wenzelm@23164
   659
wenzelm@23164
   660
in
wenzelm@23164
   661
berghofe@24541
   662
Codegen.add_codegen "numeral_codegen" numeral_codegen
wenzelm@23164
   663
wenzelm@23164
   664
end
wenzelm@23164
   665
*}
wenzelm@23164
   666
wenzelm@23164
   667
consts_code
berghofe@24541
   668
  "number_of :: int \<Rightarrow> int"    ("(_)")
wenzelm@23164
   669
  "0 :: int"                   ("0")
wenzelm@23164
   670
  "1 :: int"                   ("1")
wenzelm@23164
   671
  "uminus :: int => int"       ("~")
wenzelm@23164
   672
  "op + :: int => int => int"  ("(_ +/ _)")
wenzelm@23164
   673
  "op * :: int => int => int"  ("(_ */ _)")
wenzelm@23164
   674
  "op \<le> :: int => int => bool" ("(_ <=/ _)")
wenzelm@23164
   675
  "op < :: int => int => bool" ("(_ </ _)")
wenzelm@23164
   676
wenzelm@23164
   677
quickcheck_params [default_type = int]
wenzelm@23164
   678
wenzelm@23164
   679
(*setup continues in theory Presburger*)
wenzelm@23164
   680
wenzelm@23164
   681
hide (open) const Pls Min B0 B1 succ pred
wenzelm@23164
   682
wenzelm@23164
   683
end