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