src/HOL/ex/Binary.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 26187 3e099fc47afd
child 30510 4120fc59dd85
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
     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