22141

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 

22205

23 
ML {*


24 
fun dest_bit (Const ("False", _)) = 0


25 
 dest_bit (Const ("True", _)) = 1


26 
 dest_bit t = raise TERM ("dest_bit", [t]);


27 


28 
fun dest_binary (Const ("HOL.zero", Type ("nat", _))) = 0


29 
 dest_binary (Const ("HOL.one", Type ("nat", _))) = 1


30 
 dest_binary (Const ("Binary.bit", _) $ bs $ b) =


31 
2 * dest_binary bs + IntInf.fromInt (dest_bit b)


32 
 dest_binary t = raise TERM ("dest_binary", [t]);


33 


34 
fun mk_bit 0 = @{term False}


35 
 mk_bit 1 = @{term True}


36 
 mk_bit _ = raise TERM ("mk_bit", []);


37 


38 
fun mk_binary 0 = @{term "0::nat"}


39 
 mk_binary 1 = @{term "1::nat"}


40 
 mk_binary n =


41 
if n < 0 then raise TERM ("mk_binary", [])


42 
else


43 
let val (q, r) = IntInf.divMod (n, 2)


44 
in @{term bit} $ mk_binary q $ mk_bit (IntInf.toInt r) end;


45 
*}


46 

22141

47 


48 
subsection {* Direct operations  plain normalization *}


49 


50 
lemma binary_norm:


51 
"bit 0 False = 0"


52 
"bit 0 True = 1"


53 
unfolding bit_def by simp_all


54 


55 
lemma binary_add:


56 
"n + 0 = n"


57 
"0 + n = n"


58 
"1 + 1 = bit 1 False"


59 
"bit n False + 1 = bit n True"


60 
"bit n True + 1 = bit (n + 1) False"


61 
"1 + bit n False = bit n True"


62 
"1 + bit n True = bit (n + 1) False"


63 
"bit m False + bit n False = bit (m + n) False"


64 
"bit m False + bit n True = bit (m + n) True"


65 
"bit m True + bit n False = bit (m + n) True"


66 
"bit m True + bit n True = bit ((m + n) + 1) False"


67 
by (simp_all add: bit_simps)


68 


69 
lemma binary_mult:


70 
"n * 0 = 0"


71 
"0 * n = 0"


72 
"n * 1 = n"


73 
"1 * n = n"


74 
"bit m True * n = bit (m * n) False + n"


75 
"bit m False * n = bit (m * n) False"


76 
"n * bit m True = bit (m * n) False + n"


77 
"n * bit m False = bit (m * n) False"


78 
by (simp_all add: bit_simps)


79 


80 
lemmas binary_simps = binary_norm binary_add binary_mult


81 


82 


83 
subsection {* Indirect operations  ML will produce witnesses *}


84 


85 
lemma binary_less_eq:


86 
fixes n :: nat


87 
shows "n \<equiv> m + k \<Longrightarrow> (m \<le> n) \<equiv> True"


88 
and "m \<equiv> n + k + 1 \<Longrightarrow> (m \<le> n) \<equiv> False"


89 
by simp_all


90 


91 
lemma binary_less:


92 
fixes n :: nat


93 
shows "m \<equiv> n + k \<Longrightarrow> (m < n) \<equiv> False"


94 
and "n \<equiv> m + k + 1 \<Longrightarrow> (m < n) \<equiv> True"


95 
by simp_all


96 


97 
lemma binary_diff:


98 
fixes n :: nat


99 
shows "m \<equiv> n + k \<Longrightarrow> m  n \<equiv> k"


100 
and "n \<equiv> m + k \<Longrightarrow> m  n \<equiv> 0"


101 
by simp_all


102 


103 
lemma binary_divmod:


104 
fixes n :: nat


105 
assumes "m \<equiv> n * k + l" and "0 < n" and "l < n"


106 
shows "m div n \<equiv> k"


107 
and "m mod n \<equiv> l"


108 
proof 


109 
from `m \<equiv> n * k + l` have "m = l + k * n" by simp


110 
with `0 < n` and `l < n` show "m div n \<equiv> k" and "m mod n \<equiv> l" by simp_all


111 
qed


112 


113 
ML {*

22205

114 
local


115 
infix ==;


116 
val op == = Logic.mk_equals;


117 
fun plus m n = @{term "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n;


118 
fun mult m n = @{term "times :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n;

22141

119 


120 
val binary_ss = HOL_basic_ss addsimps @{thms binary_simps};

22156

121 
fun prove ctxt prop =


122 
Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss));

22141

123 

22205

124 
fun binary_proc proc ss ct =


125 
(case Thm.term_of ct of


126 
_ $ t $ u =>


127 
(case try (pairself (`dest_binary)) (t, u) of


128 
SOME args => proc (Simplifier.the_context ss) args


129 
 NONE => NONE)


130 
 _ => NONE);


131 
in

22141

132 

22205

133 
val less_eq_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>


134 
let val k = n  m in


135 
if k >= 0 then


136 
SOME (@{thm binary_less_eq(1)} OF [prove ctxt (u == plus t (mk_binary k))])


137 
else


138 
SOME (@{thm binary_less_eq(2)} OF


139 
[prove ctxt (t == plus (plus u (mk_binary (~ k  1))) (mk_binary 1))])


140 
end);

22141

141 

22205

142 
val less_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>


143 
let val k = m  n in


144 
if k >= 0 then


145 
SOME (@{thm binary_less(1)} OF [prove ctxt (t == plus u (mk_binary k))])


146 
else


147 
SOME (@{thm binary_less(2)} OF


148 
[prove ctxt (u == plus (plus t (mk_binary (~ k  1))) (mk_binary 1))])


149 
end);

22141

150 

22205

151 
val diff_proc = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>


152 
let val k = m  n in


153 
if k >= 0 then


154 
SOME (@{thm binary_diff(1)} OF [prove ctxt (t == plus u (mk_binary k))])


155 
else


156 
SOME (@{thm binary_diff(2)} OF [prove ctxt (u == plus t (mk_binary (~ k)))])


157 
end);

22141

158 

22205

159 
fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>


160 
if n = 0 then NONE


161 
else


162 
let val (k, l) = IntInf.divMod (m, n)


163 
in SOME (rule OF [prove ctxt (t == plus (mult u (mk_binary k)) (mk_binary l))]) end);


164 


165 
end;


166 
*}

22141

167 

22205

168 
simproc_setup binary_nat_less_eq ("m <= (n::nat)") = {* K less_eq_proc *}


169 
simproc_setup binary_nat_less ("m < (n::nat)") = {* K less_proc *}


170 
simproc_setup binary_nat_diff ("m  (n::nat)") = {* K diff_proc *}


171 
simproc_setup binary_nat_div ("m div (n::nat)") = {* K (divmod_proc @{thm binary_divmod(1)}) *}


172 
simproc_setup binary_nat_mod ("m mod (n::nat)") = {* K (divmod_proc @{thm binary_divmod(2)}) *}

22141

173 

22205

174 
method_setup binary_simp = {*


175 
Method.no_args (Method.SIMPLE_METHOD'


176 
(full_simp_tac


177 
(HOL_basic_ss


178 
addsimps @{thms binary_simps}


179 
addsimprocs


180 
[@{simproc binary_nat_less_eq},


181 
@{simproc binary_nat_less},


182 
@{simproc binary_nat_diff},


183 
@{simproc binary_nat_div},


184 
@{simproc binary_nat_mod}])))


185 
*} "binary simplification"

22141

186 


187 


188 
subsection {* Concrete syntax *}


189 


190 
syntax


191 
"_Binary" :: "num_const \<Rightarrow> 'a" ("$_")


192 


193 
parse_translation {*


194 
let


195 


196 
val syntax_consts = map_aterms (fn Const (c, T) => Const (Syntax.constN ^ c, T)  a => a);


197 

22229

198 
fun binary_tr [Const (num, _)] =

22141

199 
let


200 
val {leading_zeros = z, value = n, ...} = Syntax.read_xnum num;


201 
val _ = z = 0 andalso n >= 0 orelse error ("Bad binary number: " ^ num);


202 
in syntax_consts (mk_binary n) end


203 
 binary_tr ts = raise TERM ("binary_tr", ts);


204 


205 
in [("_Binary", binary_tr)] end


206 
*}


207 


208 


209 
subsection {* Examples *}


210 


211 
lemma "$6 = 6"


212 
by (simp add: bit_simps)


213 


214 
lemma "bit (bit (bit 0 False) False) True = 1"


215 
by (simp add: bit_simps)


216 


217 
lemma "bit (bit (bit 0 False) False) True = bit 0 True"


218 
by (simp add: bit_simps)


219 


220 
lemma "$5 + $3 = $8"


221 
by binary_simp


222 


223 
lemma "$5 * $3 = $15"


224 
by binary_simp


225 


226 
lemma "$5  $3 = $2"


227 
by binary_simp


228 


229 
lemma "$3  $5 = 0"


230 
by binary_simp


231 


232 
lemma "$123456789  $123 = $123456666"


233 
by binary_simp


234 


235 
lemma "$1111111111222222222233333333334444444444  $998877665544332211 =


236 
$1111111111222222222232334455668900112233"


237 
by binary_simp


238 


239 
lemma "(1111111111222222222233333333334444444444::nat)  998877665544332211 =


240 
1111111111222222222232334455668900112233"


241 
by simp


242 


243 
lemma "(1111111111222222222233333333334444444444::int)  998877665544332211 =


244 
1111111111222222222232334455668900112233"


245 
by simp


246 


247 
lemma "$1111111111222222222233333333334444444444 * $998877665544332211 =


248 
$1109864072938022197293802219729380221972383090160869185684"


249 
by binary_simp


250 


251 
lemma "$1111111111222222222233333333334444444444 * $998877665544332211 


252 
$5555555555666666666677777777778888888888 =


253 
$1109864072938022191738246664062713555294605312381980296796"


254 
by binary_simp


255 


256 
lemma "$42 < $4 = False"


257 
by binary_simp


258 


259 
lemma "$4 < $42 = True"


260 
by binary_simp


261 


262 
lemma "$42 <= $4 = False"


263 
by binary_simp


264 


265 
lemma "$4 <= $42 = True"


266 
by binary_simp


267 


268 
lemma "$1111111111222222222233333333334444444444 < $998877665544332211 = False"


269 
by binary_simp


270 


271 
lemma "$998877665544332211 < $1111111111222222222233333333334444444444 = True"


272 
by binary_simp


273 


274 
lemma "$1111111111222222222233333333334444444444 <= $998877665544332211 = False"


275 
by binary_simp


276 


277 
lemma "$998877665544332211 <= $1111111111222222222233333333334444444444 = True"


278 
by binary_simp


279 


280 
lemma "$1234 div $23 = $53"


281 
by binary_simp


282 


283 
lemma "$1234 mod $23 = $15"


284 
by binary_simp


285 


286 
lemma "$1111111111222222222233333333334444444444 div $998877665544332211 =


287 
$1112359550673033707875"


288 
by binary_simp


289 


290 
lemma "$1111111111222222222233333333334444444444 mod $998877665544332211 =


291 
$42245174317582819"


292 
by binary_simp


293 

22153

294 
lemma "(1111111111222222222233333333334444444444::int) div 998877665544332211 =


295 
1112359550673033707875"


296 
by simp  {* legacy numerals: 30 times slower *}


297 

22141

298 
lemma "(1111111111222222222233333333334444444444::int) mod 998877665544332211 =


299 
42245174317582819"

22153

300 
by simp  {* legacy numerals: 30 times slower *}

22141

301 


302 
end
