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