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