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