1.1 --- a/src/HOL/ROOT Wed May 29 18:55:37 2013 +0200
1.2 +++ b/src/HOL/ROOT Wed May 29 23:11:21 2013 +0200
1.3 @@ -506,7 +506,6 @@
1.4 Higher_Order_Logic
1.5 Abstract_NAT
1.6 Guess
1.7 - Binary
1.8 Fundefs
1.9 Induction_Schema
1.10 LocaleTest2
2.1 --- a/src/HOL/ex/Binary.thy Wed May 29 18:55:37 2013 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,303 +0,0 @@
2.4 -(* Title: HOL/ex/Binary.thy
2.5 - Author: Makarius
2.6 -*)
2.7 -
2.8 -header {* Simple and efficient binary numerals *}
2.9 -
2.10 -theory Binary
2.11 -imports Main
2.12 -begin
2.13 -
2.14 -subsection {* Binary representation of natural numbers *}
2.15 -
2.16 -definition
2.17 - bit :: "nat \<Rightarrow> bool \<Rightarrow> nat" where
2.18 - "bit n b = (if b then 2 * n + 1 else 2 * n)"
2.19 -
2.20 -lemma bit_simps:
2.21 - "bit n False = 2 * n"
2.22 - "bit n True = 2 * n + 1"
2.23 - unfolding bit_def by simp_all
2.24 -
2.25 -ML {*
2.26 - fun dest_bit (Const (@{const_name False}, _)) = 0
2.27 - | dest_bit (Const (@{const_name True}, _)) = 1
2.28 - | dest_bit t = raise TERM ("dest_bit", [t]);
2.29 -
2.30 - fun dest_binary (Const (@{const_name Groups.zero}, Type (@{type_name nat}, _))) = 0
2.31 - | dest_binary (Const (@{const_name Groups.one}, Type (@{type_name nat}, _))) = 1
2.32 - | dest_binary (Const (@{const_name bit}, _) $ bs $ b) = 2 * dest_binary bs + dest_bit b
2.33 - | dest_binary t = raise TERM ("dest_binary", [t]);
2.34 -
2.35 - fun mk_bit 0 = @{term False}
2.36 - | mk_bit 1 = @{term True}
2.37 - | mk_bit _ = raise TERM ("mk_bit", []);
2.38 -
2.39 - fun mk_binary 0 = @{term "0::nat"}
2.40 - | mk_binary 1 = @{term "1::nat"}
2.41 - | mk_binary n =
2.42 - if n < 0 then raise TERM ("mk_binary", [])
2.43 - else
2.44 - let val (q, r) = Integer.div_mod n 2
2.45 - in @{term bit} $ mk_binary q $ mk_bit r end;
2.46 -*}
2.47 -
2.48 -
2.49 -subsection {* Direct operations -- plain normalization *}
2.50 -
2.51 -lemma binary_norm:
2.52 - "bit 0 False = 0"
2.53 - "bit 0 True = 1"
2.54 - unfolding bit_def by simp_all
2.55 -
2.56 -lemma binary_add:
2.57 - "n + 0 = n"
2.58 - "0 + n = n"
2.59 - "1 + 1 = bit 1 False"
2.60 - "bit n False + 1 = bit n True"
2.61 - "bit n True + 1 = bit (n + 1) False"
2.62 - "1 + bit n False = bit n True"
2.63 - "1 + bit n True = bit (n + 1) False"
2.64 - "bit m False + bit n False = bit (m + n) False"
2.65 - "bit m False + bit n True = bit (m + n) True"
2.66 - "bit m True + bit n False = bit (m + n) True"
2.67 - "bit m True + bit n True = bit ((m + n) + 1) False"
2.68 - by (simp_all add: bit_simps)
2.69 -
2.70 -lemma binary_mult:
2.71 - "n * 0 = 0"
2.72 - "0 * n = 0"
2.73 - "n * 1 = n"
2.74 - "1 * n = n"
2.75 - "bit m True * n = bit (m * n) False + n"
2.76 - "bit m False * n = bit (m * n) False"
2.77 - "n * bit m True = bit (m * n) False + n"
2.78 - "n * bit m False = bit (m * n) False"
2.79 - by (simp_all add: bit_simps)
2.80 -
2.81 -lemmas binary_simps = binary_norm binary_add binary_mult
2.82 -
2.83 -
2.84 -subsection {* Indirect operations -- ML will produce witnesses *}
2.85 -
2.86 -lemma binary_less_eq:
2.87 - fixes n :: nat
2.88 - shows "n \<equiv> m + k \<Longrightarrow> (m \<le> n) \<equiv> True"
2.89 - and "m \<equiv> n + k + 1 \<Longrightarrow> (m \<le> n) \<equiv> False"
2.90 - by simp_all
2.91 -
2.92 -lemma binary_less:
2.93 - fixes n :: nat
2.94 - shows "m \<equiv> n + k \<Longrightarrow> (m < n) \<equiv> False"
2.95 - and "n \<equiv> m + k + 1 \<Longrightarrow> (m < n) \<equiv> True"
2.96 - by simp_all
2.97 -
2.98 -lemma binary_diff:
2.99 - fixes n :: nat
2.100 - shows "m \<equiv> n + k \<Longrightarrow> m - n \<equiv> k"
2.101 - and "n \<equiv> m + k \<Longrightarrow> m - n \<equiv> 0"
2.102 - by simp_all
2.103 -
2.104 -lemma binary_divmod:
2.105 - fixes n :: nat
2.106 - assumes "m \<equiv> n * k + l" and "0 < n" and "l < n"
2.107 - shows "m div n \<equiv> k"
2.108 - and "m mod n \<equiv> l"
2.109 -proof -
2.110 - from `m \<equiv> n * k + l` have "m = l + k * n" by simp
2.111 - with `0 < n` and `l < n` show "m div n \<equiv> k" and "m mod n \<equiv> l" by simp_all
2.112 -qed
2.113 -
2.114 -ML {*
2.115 -local
2.116 - infix ==;
2.117 - val op == = Logic.mk_equals;
2.118 - fun plus m n = @{term "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n;
2.119 - fun mult m n = @{term "times :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n;
2.120 -
2.121 - val binary_ss =
2.122 - simpset_of (put_simpset HOL_basic_ss @{context} addsimps @{thms binary_simps});
2.123 - fun prove ctxt prop =
2.124 - Goal.prove ctxt [] [] prop
2.125 - (fn _ => ALLGOALS (full_simp_tac (put_simpset binary_ss ctxt)));
2.126 -
2.127 - fun binary_proc proc ctxt ct =
2.128 - (case Thm.term_of ct of
2.129 - _ $ t $ u =>
2.130 - (case try (pairself (`dest_binary)) (t, u) of
2.131 - SOME args => proc ctxt args
2.132 - | NONE => NONE)
2.133 - | _ => NONE);
2.134 -in
2.135 -
2.136 -val less_eq_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
2.137 - let val k = n - m in
2.138 - if k >= 0 then
2.139 - SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (mk_binary k))])
2.140 - else
2.141 - SOME (@{thm binary_less_eq(2)} OF
2.142 - [prove ctxt (t == plus (plus u (mk_binary (~ k - 1))) (mk_binary 1))])
2.143 - end);
2.144 -
2.145 -val less_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
2.146 - let val k = m - n in
2.147 - if k >= 0 then
2.148 - SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (mk_binary k))])
2.149 - else
2.150 - SOME (@{thm binary_less(2)} OF
2.151 - [prove ctxt (u == plus (plus t (mk_binary (~ k - 1))) (mk_binary 1))])
2.152 - end);
2.153 -
2.154 -val diff_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
2.155 - let val k = m - n in
2.156 - if k >= 0 then
2.157 - SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (mk_binary k))])
2.158 - else
2.159 - SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (mk_binary (~ k)))])
2.160 - end);
2.161 -
2.162 -fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
2.163 - if n = 0 then NONE
2.164 - else
2.165 - let val (k, l) = Integer.div_mod m n
2.166 - in SOME (rule OF [prove ctxt (t == plus (mult u (mk_binary k)) (mk_binary l))]) end);
2.167 -
2.168 -end;
2.169 -*}
2.170 -
2.171 -simproc_setup binary_nat_less_eq ("m <= (n::nat)") = {* K less_eq_proc *}
2.172 -simproc_setup binary_nat_less ("m < (n::nat)") = {* K less_proc *}
2.173 -simproc_setup binary_nat_diff ("m - (n::nat)") = {* K diff_proc *}
2.174 -simproc_setup binary_nat_div ("m div (n::nat)") = {* K (divmod_proc @{thm binary_divmod(1)}) *}
2.175 -simproc_setup binary_nat_mod ("m mod (n::nat)") = {* K (divmod_proc @{thm binary_divmod(2)}) *}
2.176 -
2.177 -method_setup binary_simp = {*
2.178 - Scan.succeed (fn ctxt => SIMPLE_METHOD'
2.179 - (full_simp_tac
2.180 - (put_simpset HOL_basic_ss ctxt
2.181 - addsimps @{thms binary_simps}
2.182 - addsimprocs
2.183 - [@{simproc binary_nat_less_eq},
2.184 - @{simproc binary_nat_less},
2.185 - @{simproc binary_nat_diff},
2.186 - @{simproc binary_nat_div},
2.187 - @{simproc binary_nat_mod}])))
2.188 -*}
2.189 -
2.190 -
2.191 -subsection {* Concrete syntax *}
2.192 -
2.193 -syntax
2.194 - "_Binary" :: "num_const \<Rightarrow> 'a" ("$_")
2.195 -
2.196 -parse_translation {*
2.197 - let
2.198 - val syntax_consts =
2.199 - map_aterms (fn Const (c, T) => Const (Lexicon.mark_const c, T) | a => a);
2.200 -
2.201 - fun binary_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ binary_tr [t] $ u
2.202 - | binary_tr [Const (num, _)] =
2.203 - let
2.204 - val {leading_zeros = z, value = n, ...} = Lexicon.read_xnum num;
2.205 - val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);
2.206 - in syntax_consts (mk_binary n) end
2.207 - | binary_tr ts = raise TERM ("binary_tr", ts);
2.208 -
2.209 - in [(@{syntax_const "_Binary"}, K binary_tr)] end
2.210 -*}
2.211 -
2.212 -
2.213 -subsection {* Examples *}
2.214 -
2.215 -lemma "$6 = 6"
2.216 - by (simp add: bit_simps)
2.217 -
2.218 -lemma "bit (bit (bit 0 False) False) True = 1"
2.219 - by (simp add: bit_simps)
2.220 -
2.221 -lemma "bit (bit (bit 0 False) False) True = bit 0 True"
2.222 - by (simp add: bit_simps)
2.223 -
2.224 -lemma "$5 + $3 = $8"
2.225 - by binary_simp
2.226 -
2.227 -lemma "$5 * $3 = $15"
2.228 - by binary_simp
2.229 -
2.230 -lemma "$5 - $3 = $2"
2.231 - by binary_simp
2.232 -
2.233 -lemma "$3 - $5 = 0"
2.234 - by binary_simp
2.235 -
2.236 -lemma "$123456789 - $123 = $123456666"
2.237 - by binary_simp
2.238 -
2.239 -lemma "$1111111111222222222233333333334444444444 - $998877665544332211 =
2.240 - $1111111111222222222232334455668900112233"
2.241 - by binary_simp
2.242 -
2.243 -lemma "(1111111111222222222233333333334444444444::nat) - 998877665544332211 =
2.244 - 1111111111222222222232334455668900112233"
2.245 - by simp
2.246 -
2.247 -lemma "(1111111111222222222233333333334444444444::int) - 998877665544332211 =
2.248 - 1111111111222222222232334455668900112233"
2.249 - by simp
2.250 -
2.251 -lemma "$1111111111222222222233333333334444444444 * $998877665544332211 =
2.252 - $1109864072938022197293802219729380221972383090160869185684"
2.253 - by binary_simp
2.254 -
2.255 -lemma "$1111111111222222222233333333334444444444 * $998877665544332211 -
2.256 - $5555555555666666666677777777778888888888 =
2.257 - $1109864072938022191738246664062713555294605312381980296796"
2.258 - by binary_simp
2.259 -
2.260 -lemma "$42 < $4 = False"
2.261 - by binary_simp
2.262 -
2.263 -lemma "$4 < $42 = True"
2.264 - by binary_simp
2.265 -
2.266 -lemma "$42 <= $4 = False"
2.267 - by binary_simp
2.268 -
2.269 -lemma "$4 <= $42 = True"
2.270 - by binary_simp
2.271 -
2.272 -lemma "$1111111111222222222233333333334444444444 < $998877665544332211 = False"
2.273 - by binary_simp
2.274 -
2.275 -lemma "$998877665544332211 < $1111111111222222222233333333334444444444 = True"
2.276 - by binary_simp
2.277 -
2.278 -lemma "$1111111111222222222233333333334444444444 <= $998877665544332211 = False"
2.279 - by binary_simp
2.280 -
2.281 -lemma "$998877665544332211 <= $1111111111222222222233333333334444444444 = True"
2.282 - by binary_simp
2.283 -
2.284 -lemma "$1234 div $23 = $53"
2.285 - by binary_simp
2.286 -
2.287 -lemma "$1234 mod $23 = $15"
2.288 - by binary_simp
2.289 -
2.290 -lemma "$1111111111222222222233333333334444444444 div $998877665544332211 =
2.291 - $1112359550673033707875"
2.292 - by binary_simp
2.293 -
2.294 -lemma "$1111111111222222222233333333334444444444 mod $998877665544332211 =
2.295 - $42245174317582819"
2.296 - by binary_simp
2.297 -
2.298 -lemma "(1111111111222222222233333333334444444444::int) div 998877665544332211 =
2.299 - 1112359550673033707875"
2.300 - by simp -- {* legacy numerals: 30 times slower *}
2.301 -
2.302 -lemma "(1111111111222222222233333333334444444444::int) mod 998877665544332211 =
2.303 - 42245174317582819"
2.304 - by simp -- {* legacy numerals: 30 times slower *}
2.305 -
2.306 -end