src/HOL/Integ/Bin.thy
 author paulson Fri Mar 29 13:18:26 1996 +0100 (1996-03-29) changeset 1632 39e146ac224c child 2988 d38f330e58b3 permissions -rw-r--r--
Binary integers and their numeric syntax
 paulson@1632 ` 1` ```(* Title: HOL/Integ/Bin.thy ``` paulson@1632 ` 2` ``` Authors: Lawrence C Paulson, Cambridge University Computer Laboratory ``` paulson@1632 ` 3` ``` David Spelt, University of Twente ``` paulson@1632 ` 4` ``` Copyright 1994 University of Cambridge ``` paulson@1632 ` 5` ``` Copyright 1996 University of Twente ``` paulson@1632 ` 6` paulson@1632 ` 7` ```Arithmetic on binary integers. ``` paulson@1632 ` 8` paulson@1632 ` 9` ``` The sign Plus stands for an infinite string of leading F's. ``` paulson@1632 ` 10` ``` The sign Minus stands for an infinite string of leading T's. ``` paulson@1632 ` 11` paulson@1632 ` 12` ```A number can have multiple representations, namely leading F's with sign ``` paulson@1632 ` 13` ```Plus and leading T's with sign Minus. See twos-compl.ML/int_of_binary for ``` paulson@1632 ` 14` ```the numerical interpretation. ``` paulson@1632 ` 15` paulson@1632 ` 16` ```The representation expects that (m mod 2) is 0 or 1, even if m is negative; ``` paulson@1632 ` 17` ```For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1 ``` paulson@1632 ` 18` paulson@1632 ` 19` ```Division is not defined yet! ``` paulson@1632 ` 20` ```*) ``` paulson@1632 ` 21` paulson@1632 ` 22` ```Bin = Integ + ``` paulson@1632 ` 23` paulson@1632 ` 24` ```syntax ``` paulson@1632 ` 25` ``` "_Int" :: xnum => int ("_") ``` paulson@1632 ` 26` paulson@1632 ` 27` ```datatype ``` paulson@1632 ` 28` ``` bin = Plus ``` paulson@1632 ` 29` ``` | Minus ``` paulson@1632 ` 30` ``` | Bcons bin bool ``` paulson@1632 ` 31` paulson@1632 ` 32` ```consts ``` paulson@1632 ` 33` ``` integ_of_bin :: bin=>int ``` paulson@1632 ` 34` ``` norm_Bcons :: [bin,bool]=>bin ``` paulson@1632 ` 35` ``` bin_succ :: bin=>bin ``` paulson@1632 ` 36` ``` bin_pred :: bin=>bin ``` paulson@1632 ` 37` ``` bin_minus :: bin=>bin ``` paulson@1632 ` 38` ``` bin_add,bin_mult :: [bin,bin]=>bin ``` paulson@1632 ` 39` ``` h_bin :: [bin,bool,bin]=>bin ``` paulson@1632 ` 40` paulson@1632 ` 41` ```(*norm_Bcons adds a bit, suppressing leading 0s and 1s*) ``` paulson@1632 ` 42` paulson@1632 ` 43` ```primrec norm_Bcons bin ``` paulson@1632 ` 44` ``` norm_Plus "norm_Bcons Plus b = (if b then (Bcons Plus b) else Plus)" ``` paulson@1632 ` 45` ``` norm_Minus "norm_Bcons Minus b = (if b then Minus else (Bcons Minus b))" ``` paulson@1632 ` 46` ``` norm_Bcons "norm_Bcons (Bcons w' x') b = Bcons (Bcons w' x') b" ``` paulson@1632 ` 47` ``` ``` paulson@1632 ` 48` ```primrec integ_of_bin bin ``` paulson@1632 ` 49` ``` iob_Plus "integ_of_bin Plus = \$#0" ``` paulson@1632 ` 50` ``` iob_Minus "integ_of_bin Minus = \$~(\$#1)" ``` paulson@1632 ` 51` ``` iob_Bcons "integ_of_bin(Bcons w x) = (if x then \$#1 else \$#0) + (integ_of_bin w) + (integ_of_bin w)" ``` paulson@1632 ` 52` paulson@1632 ` 53` ```primrec bin_succ bin ``` paulson@1632 ` 54` ``` succ_Plus "bin_succ Plus = Bcons Plus True" ``` paulson@1632 ` 55` ``` succ_Minus "bin_succ Minus = Plus" ``` paulson@1632 ` 56` ``` succ_Bcons "bin_succ(Bcons w x) = (if x then (Bcons (bin_succ w) False) else (norm_Bcons w True))" ``` paulson@1632 ` 57` paulson@1632 ` 58` ```primrec bin_pred bin ``` paulson@1632 ` 59` ``` pred_Plus "bin_pred(Plus) = Minus" ``` paulson@1632 ` 60` ``` pred_Minus "bin_pred(Minus) = Bcons Minus False" ``` paulson@1632 ` 61` ``` pred_Bcons "bin_pred(Bcons w x) = (if x then (norm_Bcons w False) else (Bcons (bin_pred w) True))" ``` paulson@1632 ` 62` ``` ``` paulson@1632 ` 63` ```primrec bin_minus bin ``` paulson@1632 ` 64` ``` min_Plus "bin_minus Plus = Plus" ``` paulson@1632 ` 65` ``` min_Minus "bin_minus Minus = Bcons Plus True" ``` paulson@1632 ` 66` ``` min_Bcons "bin_minus(Bcons w x) = (if x then (bin_pred (Bcons (bin_minus w) False)) else (Bcons (bin_minus w) False))" ``` paulson@1632 ` 67` paulson@1632 ` 68` ```primrec bin_add bin ``` paulson@1632 ` 69` ``` add_Plus "bin_add Plus w = w" ``` paulson@1632 ` 70` ``` add_Minus "bin_add Minus w = bin_pred w" ``` paulson@1632 ` 71` ``` add_Bcons "bin_add (Bcons v x) w = h_bin v x w" ``` paulson@1632 ` 72` paulson@1632 ` 73` ```primrec bin_mult bin ``` paulson@1632 ` 74` ``` mult_Plus "bin_mult Plus w = Plus" ``` paulson@1632 ` 75` ``` mult_Minus "bin_mult Minus w = bin_minus w" ``` paulson@1632 ` 76` ``` mult_Bcons "bin_mult (Bcons v x) w = (if x then (bin_add (norm_Bcons (bin_mult v w) False) w) else (norm_Bcons (bin_mult v w) False))" ``` paulson@1632 ` 77` paulson@1632 ` 78` ```primrec h_bin bin ``` paulson@1632 ` 79` ``` h_Plus "h_bin v x Plus = Bcons v x" ``` paulson@1632 ` 80` ``` h_Minus "h_bin v x Minus = bin_pred (Bcons v x)" ``` paulson@1632 ` 81` ``` h_BCons "h_bin v x (Bcons w y) = norm_Bcons (bin_add v (if (x & y) then bin_succ w else w)) (x~=y)" ``` paulson@1632 ` 82` paulson@1632 ` 83` ```end ``` paulson@1632 ` 84` paulson@1632 ` 85` ```ML ``` paulson@1632 ` 86` paulson@1632 ` 87` ```(** Concrete syntax for integers **) ``` paulson@1632 ` 88` paulson@1632 ` 89` ```local ``` paulson@1632 ` 90` ``` open Syntax; ``` paulson@1632 ` 91` paulson@1632 ` 92` ``` (* Bits *) ``` paulson@1632 ` 93` paulson@1632 ` 94` ``` fun mk_bit 0 = const "False" ``` paulson@1632 ` 95` ``` | mk_bit 1 = const "True" ``` paulson@1632 ` 96` ``` | mk_bit _ = sys_error "mk_bit"; ``` paulson@1632 ` 97` paulson@1632 ` 98` ``` fun dest_bit (Const ("False", _)) = 0 ``` paulson@1632 ` 99` ``` | dest_bit (Const ("True", _)) = 1 ``` paulson@1632 ` 100` ``` | dest_bit _ = raise Match; ``` paulson@1632 ` 101` paulson@1632 ` 102` paulson@1632 ` 103` ``` (* Bit strings *) (*we try to handle superfluous leading digits nicely*) ``` paulson@1632 ` 104` paulson@1632 ` 105` ``` fun prefix_len _ [] = 0 ``` paulson@1632 ` 106` ``` | prefix_len pred (x :: xs) = ``` paulson@1632 ` 107` ``` if pred x then 1 + prefix_len pred xs else 0; ``` paulson@1632 ` 108` paulson@1632 ` 109` ``` fun mk_bin str = ``` paulson@1632 ` 110` ``` let ``` paulson@1632 ` 111` ``` val (sign, digs) = ``` paulson@1632 ` 112` ``` (case explode str of ``` paulson@1632 ` 113` ``` "#" :: "~" :: cs => (~1, cs) ``` paulson@1632 ` 114` ``` | "#" :: cs => (1, cs) ``` paulson@1632 ` 115` ``` | _ => raise ERROR); ``` paulson@1632 ` 116` paulson@1632 ` 117` ``` val zs = prefix_len (equal "0") digs; ``` paulson@1632 ` 118` paulson@1632 ` 119` ``` fun bin_of 0 = replicate zs 0 ``` paulson@1632 ` 120` ``` | bin_of ~1 = replicate zs 1 @ [~1] ``` paulson@1632 ` 121` ``` | bin_of n = (n mod 2) :: bin_of (n div 2); ``` paulson@1632 ` 122` paulson@1632 ` 123` ``` fun term_of [] = const "Plus" ``` paulson@1632 ` 124` ``` | term_of [~1] = const "Minus" ``` paulson@1632 ` 125` ``` | term_of (b :: bs) = const "Bcons" \$ term_of bs \$ mk_bit b; ``` paulson@1632 ` 126` ``` in ``` paulson@1632 ` 127` ``` term_of (bin_of (sign * (#1 (scan_int digs)))) ``` paulson@1632 ` 128` ``` end; ``` paulson@1632 ` 129` paulson@1632 ` 130` ``` fun dest_bin tm = ``` paulson@1632 ` 131` ``` let ``` paulson@1632 ` 132` ``` fun bin_of (Const ("Plus", _)) = [] ``` paulson@1632 ` 133` ``` | bin_of (Const ("Minus", _)) = [~1] ``` paulson@1632 ` 134` ``` | bin_of (Const ("Bcons", _) \$ bs \$ b) = dest_bit b :: bin_of bs ``` paulson@1632 ` 135` ``` | bin_of _ = raise Match; ``` paulson@1632 ` 136` paulson@1632 ` 137` ``` fun int_of [] = 0 ``` paulson@1632 ` 138` ``` | int_of (b :: bs) = b + 2 * int_of bs; ``` paulson@1632 ` 139` paulson@1632 ` 140` ``` val rev_digs = bin_of tm; ``` paulson@1632 ` 141` ``` val (sign, zs) = ``` paulson@1632 ` 142` ``` (case rev rev_digs of ``` paulson@1632 ` 143` ``` ~1 :: bs => ("~", prefix_len (equal 1) bs) ``` paulson@1632 ` 144` ``` | bs => ("", prefix_len (equal 0) bs)); ``` paulson@1632 ` 145` ``` val num = string_of_int (abs (int_of rev_digs)); ``` paulson@1632 ` 146` ``` in ``` paulson@1632 ` 147` ``` "#" ^ sign ^ implode (replicate zs "0") ^ num ``` paulson@1632 ` 148` ``` end; ``` paulson@1632 ` 149` paulson@1632 ` 150` paulson@1632 ` 151` ``` (* translation of integer constant tokens to and from binary *) ``` paulson@1632 ` 152` paulson@1632 ` 153` ``` fun int_tr (*"_Int"*) [t as Free (str, _)] = ``` paulson@1632 ` 154` ``` (const "integ_of_bin" \$ ``` paulson@1632 ` 155` ``` (mk_bin str handle ERROR => raise_term "int_tr" [t])) ``` paulson@1632 ` 156` ``` | int_tr (*"_Int"*) ts = raise_term "int_tr" ts; ``` paulson@1632 ` 157` paulson@1632 ` 158` ``` fun int_tr' (*"integ_of"*) [t] = const "_Int" \$ free (dest_bin t) ``` paulson@1632 ` 159` ``` | int_tr' (*"integ_of"*) _ = raise Match; ``` paulson@1632 ` 160` ```in ``` paulson@1632 ` 161` ``` val parse_translation = [("_Int", int_tr)]; ``` paulson@1632 ` 162` ``` val print_translation = [("integ_of_bin", int_tr')]; ``` paulson@1632 ` 163` ```end; ```