src/HOL/ex/Binary.thy
author wenzelm
Sat Mar 01 14:10:13 2008 +0100 (2008-03-01)
changeset 26187 3e099fc47afd
parent 24630 351a308ab58d
child 30510 4120fc59dd85
permissions -rw-r--r--
use more antiquotations;
wenzelm@22141
     1
(*  Title:      HOL/ex/Binary.thy
wenzelm@22141
     2
    ID:         $Id$
wenzelm@22141
     3
    Author:     Makarius
wenzelm@22141
     4
*)
wenzelm@22141
     5
wenzelm@22141
     6
header {* Simple and efficient binary numerals *}
wenzelm@22141
     7
wenzelm@22141
     8
theory Binary
wenzelm@22141
     9
imports Main
wenzelm@22141
    10
begin
wenzelm@22141
    11
wenzelm@22141
    12
subsection {* Binary representation of natural numbers *}
wenzelm@22141
    13
wenzelm@22141
    14
definition
wenzelm@22141
    15
  bit :: "nat \<Rightarrow> bool \<Rightarrow> nat" where
wenzelm@22141
    16
  "bit n b = (if b then 2 * n + 1 else 2 * n)"
wenzelm@22141
    17
wenzelm@22141
    18
lemma bit_simps:
wenzelm@22141
    19
    "bit n False = 2 * n"
wenzelm@22141
    20
    "bit n True = 2 * n + 1"
wenzelm@22141
    21
  unfolding bit_def by simp_all
wenzelm@22141
    22
wenzelm@22205
    23
ML {*
wenzelm@24227
    24
structure Binary =
wenzelm@24227
    25
struct
wenzelm@26187
    26
  fun dest_bit (Const (@{const_name False}, _)) = 0
wenzelm@26187
    27
    | dest_bit (Const (@{const_name True}, _)) = 1
wenzelm@22205
    28
    | dest_bit t = raise TERM ("dest_bit", [t]);
wenzelm@22205
    29
wenzelm@26187
    30
  fun dest_binary (Const (@{const_name HOL.zero}, Type (@{type_name nat}, _))) = 0
wenzelm@26187
    31
    | dest_binary (Const (@{const_name HOL.one}, Type (@{type_name nat}, _))) = 1
wenzelm@26187
    32
    | dest_binary (Const (@{const_name bit}, _) $ bs $ b) = 2 * dest_binary bs + dest_bit b
wenzelm@22205
    33
    | dest_binary t = raise TERM ("dest_binary", [t]);
wenzelm@22205
    34
wenzelm@22205
    35
  fun mk_bit 0 = @{term False}
wenzelm@22205
    36
    | mk_bit 1 = @{term True}
wenzelm@22205
    37
    | mk_bit _ = raise TERM ("mk_bit", []);
wenzelm@22205
    38
wenzelm@22205
    39
  fun mk_binary 0 = @{term "0::nat"}
wenzelm@22205
    40
    | mk_binary 1 = @{term "1::nat"}
wenzelm@22205
    41
    | mk_binary n =
wenzelm@22205
    42
        if n < 0 then raise TERM ("mk_binary", [])
wenzelm@22205
    43
        else
wenzelm@24630
    44
          let val (q, r) = Integer.div_mod n 2
wenzelm@24630
    45
          in @{term bit} $ mk_binary q $ mk_bit r end;
wenzelm@24227
    46
end
wenzelm@22205
    47
*}
wenzelm@22205
    48
wenzelm@22141
    49
wenzelm@22141
    50
subsection {* Direct operations -- plain normalization *}
wenzelm@22141
    51
wenzelm@22141
    52
lemma binary_norm:
wenzelm@22141
    53
    "bit 0 False = 0"
wenzelm@22141
    54
    "bit 0 True = 1"
wenzelm@22141
    55
  unfolding bit_def by simp_all
wenzelm@22141
    56
wenzelm@22141
    57
lemma binary_add:
wenzelm@22141
    58
    "n + 0 = n"
wenzelm@22141
    59
    "0 + n = n"
wenzelm@22141
    60
    "1 + 1 = bit 1 False"
wenzelm@22141
    61
    "bit n False + 1 = bit n True"
wenzelm@22141
    62
    "bit n True + 1 = bit (n + 1) False"
wenzelm@22141
    63
    "1 + bit n False = bit n True"
wenzelm@22141
    64
    "1 + bit n True = bit (n + 1) False"
wenzelm@22141
    65
    "bit m False + bit n False = bit (m + n) False"
wenzelm@22141
    66
    "bit m False + bit n True = bit (m + n) True"
wenzelm@22141
    67
    "bit m True + bit n False = bit (m + n) True"
wenzelm@22141
    68
    "bit m True + bit n True = bit ((m + n) + 1) False"
wenzelm@22141
    69
  by (simp_all add: bit_simps)
wenzelm@22141
    70
wenzelm@22141
    71
lemma binary_mult:
wenzelm@22141
    72
    "n * 0 = 0"
wenzelm@22141
    73
    "0 * n = 0"
wenzelm@22141
    74
    "n * 1 = n"
wenzelm@22141
    75
    "1 * n = n"
wenzelm@22141
    76
    "bit m True * n = bit (m * n) False + n"
wenzelm@22141
    77
    "bit m False * n = bit (m * n) False"
wenzelm@22141
    78
    "n * bit m True = bit (m * n) False + n"
wenzelm@22141
    79
    "n * bit m False = bit (m * n) False"
wenzelm@22141
    80
  by (simp_all add: bit_simps)
wenzelm@22141
    81
wenzelm@22141
    82
lemmas binary_simps = binary_norm binary_add binary_mult
wenzelm@22141
    83
wenzelm@22141
    84
wenzelm@22141
    85
subsection {* Indirect operations -- ML will produce witnesses *}
wenzelm@22141
    86
wenzelm@22141
    87
lemma binary_less_eq:
wenzelm@22141
    88
  fixes n :: nat
wenzelm@22141
    89
  shows "n \<equiv> m + k \<Longrightarrow> (m \<le> n) \<equiv> True"
wenzelm@22141
    90
    and "m \<equiv> n + k + 1 \<Longrightarrow> (m \<le> n) \<equiv> False"
wenzelm@22141
    91
  by simp_all
wenzelm@22141
    92
  
wenzelm@22141
    93
lemma binary_less:
wenzelm@22141
    94
  fixes n :: nat
wenzelm@22141
    95
  shows "m \<equiv> n + k \<Longrightarrow> (m < n) \<equiv> False"
wenzelm@22141
    96
    and "n \<equiv> m + k + 1 \<Longrightarrow> (m < n) \<equiv> True"
wenzelm@22141
    97
  by simp_all
wenzelm@22141
    98
wenzelm@22141
    99
lemma binary_diff:
wenzelm@22141
   100
  fixes n :: nat
wenzelm@22141
   101
  shows "m \<equiv> n + k \<Longrightarrow> m - n \<equiv> k"
wenzelm@22141
   102
    and "n \<equiv> m + k \<Longrightarrow> m - n \<equiv> 0"
wenzelm@22141
   103
  by simp_all
wenzelm@22141
   104
wenzelm@22141
   105
lemma binary_divmod:
wenzelm@22141
   106
  fixes n :: nat
wenzelm@22141
   107
  assumes "m \<equiv> n * k + l" and "0 < n" and "l < n"
wenzelm@22141
   108
  shows "m div n \<equiv> k"
wenzelm@22141
   109
    and "m mod n \<equiv> l"
wenzelm@22141
   110
proof -
wenzelm@22141
   111
  from `m \<equiv> n * k + l` have "m = l + k * n" by simp
wenzelm@22141
   112
  with `0 < n` and `l < n` show "m div n \<equiv> k" and "m mod n \<equiv> l" by simp_all
wenzelm@22141
   113
qed
wenzelm@22141
   114
wenzelm@22141
   115
ML {*
wenzelm@22205
   116
local
wenzelm@22205
   117
  infix ==;
wenzelm@22205
   118
  val op == = Logic.mk_equals;
wenzelm@22205
   119
  fun plus m n = @{term "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n;
wenzelm@22205
   120
  fun mult m n = @{term "times :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n;
wenzelm@22141
   121
wenzelm@22141
   122
  val binary_ss = HOL_basic_ss addsimps @{thms binary_simps};
wenzelm@22156
   123
  fun prove ctxt prop =
wenzelm@22156
   124
    Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss));
wenzelm@22141
   125
wenzelm@22205
   126
  fun binary_proc proc ss ct =
wenzelm@22205
   127
    (case Thm.term_of ct of
wenzelm@22205
   128
      _ $ t $ u =>
wenzelm@24227
   129
      (case try (pairself (`Binary.dest_binary)) (t, u) of
wenzelm@22205
   130
        SOME args => proc (Simplifier.the_context ss) args
wenzelm@22205
   131
      | NONE => NONE)
wenzelm@22205
   132
    | _ => NONE);
wenzelm@22205
   133
in
wenzelm@22141
   134
wenzelm@22205
   135
val less_eq_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
wenzelm@22205
   136
  let val k = n - m in
wenzelm@22205
   137
    if k >= 0 then
wenzelm@24227
   138
      SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (Binary.mk_binary k))])
wenzelm@22205
   139
    else
wenzelm@22205
   140
      SOME (@{thm binary_less_eq(2)} OF
wenzelm@24227
   141
        [prove ctxt (t == plus (plus u (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))])
wenzelm@22205
   142
  end);
wenzelm@22141
   143
wenzelm@22205
   144
val less_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
wenzelm@22205
   145
  let val k = m - n in
wenzelm@22205
   146
    if k >= 0 then
wenzelm@24227
   147
      SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))])
wenzelm@22205
   148
    else
wenzelm@22205
   149
      SOME (@{thm binary_less(2)} OF
wenzelm@24227
   150
        [prove ctxt (u == plus (plus t (Binary.mk_binary (~ k - 1))) (Binary.mk_binary 1))])
wenzelm@22205
   151
  end);
wenzelm@22141
   152
wenzelm@22205
   153
val diff_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
wenzelm@22205
   154
  let val k = m - n in
wenzelm@22205
   155
    if k >= 0 then
wenzelm@24227
   156
      SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (Binary.mk_binary k))])
wenzelm@22205
   157
    else
wenzelm@24227
   158
      SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (Binary.mk_binary (~ k)))])
wenzelm@22205
   159
  end);
wenzelm@22141
   160
wenzelm@22205
   161
fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
wenzelm@22205
   162
  if n = 0 then NONE
wenzelm@22205
   163
  else
wenzelm@24630
   164
    let val (k, l) = Integer.div_mod m n
wenzelm@24227
   165
    in SOME (rule OF [prove ctxt (t == plus (mult u (Binary.mk_binary k)) (Binary.mk_binary l))]) end);
wenzelm@22205
   166
wenzelm@22205
   167
end;
wenzelm@22205
   168
*}
wenzelm@22141
   169
wenzelm@22205
   170
simproc_setup binary_nat_less_eq ("m <= (n::nat)") = {* K less_eq_proc *}
wenzelm@22205
   171
simproc_setup binary_nat_less ("m < (n::nat)") = {* K less_proc *}
wenzelm@22205
   172
simproc_setup binary_nat_diff ("m - (n::nat)") = {* K diff_proc *}
wenzelm@22205
   173
simproc_setup binary_nat_div ("m div (n::nat)") = {* K (divmod_proc @{thm binary_divmod(1)}) *}
wenzelm@22205
   174
simproc_setup binary_nat_mod ("m mod (n::nat)") = {* K (divmod_proc @{thm binary_divmod(2)}) *}
wenzelm@22141
   175
wenzelm@22205
   176
method_setup binary_simp = {*
wenzelm@22205
   177
  Method.no_args (Method.SIMPLE_METHOD'
wenzelm@22205
   178
    (full_simp_tac
wenzelm@22205
   179
      (HOL_basic_ss
wenzelm@22205
   180
        addsimps @{thms binary_simps}
wenzelm@22205
   181
        addsimprocs
wenzelm@22205
   182
         [@{simproc binary_nat_less_eq},
wenzelm@22205
   183
          @{simproc binary_nat_less},
wenzelm@22205
   184
          @{simproc binary_nat_diff},
wenzelm@22205
   185
          @{simproc binary_nat_div},
wenzelm@22205
   186
          @{simproc binary_nat_mod}])))
wenzelm@22205
   187
*} "binary simplification"
wenzelm@22141
   188
wenzelm@22141
   189
wenzelm@22141
   190
subsection {* Concrete syntax *}
wenzelm@22141
   191
wenzelm@22141
   192
syntax
wenzelm@22141
   193
  "_Binary" :: "num_const \<Rightarrow> 'a"    ("$_")
wenzelm@22141
   194
wenzelm@22141
   195
parse_translation {*
wenzelm@22141
   196
let
wenzelm@22141
   197
wenzelm@22141
   198
val syntax_consts = map_aterms (fn Const (c, T) => Const (Syntax.constN ^ c, T) | a => a);
wenzelm@22141
   199
wenzelm@22229
   200
fun binary_tr [Const (num, _)] =
wenzelm@22141
   201
      let
wenzelm@22141
   202
        val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num;
wenzelm@22141
   203
        val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
wenzelm@24227
   204
      in syntax_consts (Binary.mk_binary n) end
wenzelm@22141
   205
  | binary_tr ts = raise TERM ("binary_tr", ts);
wenzelm@22141
   206
wenzelm@22141
   207
in [("_Binary", binary_tr)] end
wenzelm@22141
   208
*}
wenzelm@22141
   209
wenzelm@22141
   210
wenzelm@22141
   211
subsection {* Examples *}
wenzelm@22141
   212
wenzelm@22141
   213
lemma "$6 = 6"
wenzelm@22141
   214
  by (simp add: bit_simps)
wenzelm@22141
   215
wenzelm@22141
   216
lemma "bit (bit (bit 0 False) False) True = 1"
wenzelm@22141
   217
  by (simp add: bit_simps)
wenzelm@22141
   218
wenzelm@22141
   219
lemma "bit (bit (bit 0 False) False) True = bit 0 True"
wenzelm@22141
   220
  by (simp add: bit_simps)
wenzelm@22141
   221
wenzelm@22141
   222
lemma "$5 + $3 = $8"
wenzelm@22141
   223
  by binary_simp
wenzelm@22141
   224
wenzelm@22141
   225
lemma "$5 * $3 = $15"
wenzelm@22141
   226
  by binary_simp
wenzelm@22141
   227
wenzelm@22141
   228
lemma "$5 - $3 = $2"
wenzelm@22141
   229
  by binary_simp
wenzelm@22141
   230
wenzelm@22141
   231
lemma "$3 - $5 = 0"
wenzelm@22141
   232
  by binary_simp
wenzelm@22141
   233
wenzelm@22141
   234
lemma "$123456789 - $123 = $123456666"
wenzelm@22141
   235
  by binary_simp
wenzelm@22141
   236
wenzelm@22141
   237
lemma "$1111111111222222222233333333334444444444 - $998877665544332211 =
wenzelm@22141
   238
  $1111111111222222222232334455668900112233"
wenzelm@22141
   239
  by binary_simp
wenzelm@22141
   240
wenzelm@22141
   241
lemma "(1111111111222222222233333333334444444444::nat) - 998877665544332211 =
wenzelm@22141
   242
  1111111111222222222232334455668900112233"
wenzelm@22141
   243
  by simp
wenzelm@22141
   244
wenzelm@22141
   245
lemma "(1111111111222222222233333333334444444444::int) - 998877665544332211 =
wenzelm@22141
   246
  1111111111222222222232334455668900112233"
wenzelm@22141
   247
  by simp
wenzelm@22141
   248
wenzelm@22141
   249
lemma "$1111111111222222222233333333334444444444 * $998877665544332211 =
wenzelm@22141
   250
    $1109864072938022197293802219729380221972383090160869185684"
wenzelm@22141
   251
  by binary_simp
wenzelm@22141
   252
wenzelm@22141
   253
lemma "$1111111111222222222233333333334444444444 * $998877665544332211 -
wenzelm@22141
   254
      $5555555555666666666677777777778888888888 =
wenzelm@22141
   255
    $1109864072938022191738246664062713555294605312381980296796"
wenzelm@22141
   256
  by binary_simp
wenzelm@22141
   257
wenzelm@22141
   258
lemma "$42 < $4 = False"
wenzelm@22141
   259
  by binary_simp
wenzelm@22141
   260
wenzelm@22141
   261
lemma "$4 < $42 = True"
wenzelm@22141
   262
  by binary_simp
wenzelm@22141
   263
wenzelm@22141
   264
lemma "$42 <= $4 = False"
wenzelm@22141
   265
  by binary_simp
wenzelm@22141
   266
wenzelm@22141
   267
lemma "$4 <= $42 = True"
wenzelm@22141
   268
  by binary_simp
wenzelm@22141
   269
wenzelm@22141
   270
lemma "$1111111111222222222233333333334444444444 < $998877665544332211 = False"
wenzelm@22141
   271
  by binary_simp
wenzelm@22141
   272
wenzelm@22141
   273
lemma "$998877665544332211 < $1111111111222222222233333333334444444444 = True"
wenzelm@22141
   274
  by binary_simp
wenzelm@22141
   275
wenzelm@22141
   276
lemma "$1111111111222222222233333333334444444444 <= $998877665544332211 = False"
wenzelm@22141
   277
  by binary_simp
wenzelm@22141
   278
wenzelm@22141
   279
lemma "$998877665544332211 <= $1111111111222222222233333333334444444444 = True"
wenzelm@22141
   280
  by binary_simp
wenzelm@22141
   281
wenzelm@22141
   282
lemma "$1234 div $23 = $53"
wenzelm@22141
   283
  by binary_simp
wenzelm@22141
   284
wenzelm@22141
   285
lemma "$1234 mod $23 = $15"
wenzelm@22141
   286
  by binary_simp
wenzelm@22141
   287
wenzelm@22141
   288
lemma "$1111111111222222222233333333334444444444 div $998877665544332211 =
wenzelm@22141
   289
    $1112359550673033707875"
wenzelm@22141
   290
  by binary_simp
wenzelm@22141
   291
wenzelm@22141
   292
lemma "$1111111111222222222233333333334444444444 mod $998877665544332211 =
wenzelm@22141
   293
    $42245174317582819"
wenzelm@22141
   294
  by binary_simp
wenzelm@22141
   295
wenzelm@22153
   296
lemma "(1111111111222222222233333333334444444444::int) div 998877665544332211 =
wenzelm@22153
   297
    1112359550673033707875"
wenzelm@22153
   298
  by simp  -- {* legacy numerals: 30 times slower *}
wenzelm@22153
   299
wenzelm@22141
   300
lemma "(1111111111222222222233333333334444444444::int) mod 998877665544332211 =
wenzelm@22141
   301
    42245174317582819"
wenzelm@22153
   302
  by simp  -- {* legacy numerals: 30 times slower *}
wenzelm@22141
   303
wenzelm@22141
   304
end