Binary integers and their numeric syntax
authorpaulson
Fri Mar 29 13:18:26 1996 +0100 (1996-03-29)
changeset 163239e146ac224c
parent 1631 26570790f089
child 1633 9cb70937b426
Binary integers and their numeric syntax
src/HOL/Integ/Bin.ML
src/HOL/Integ/Bin.thy
src/HOL/Integ/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Integ/Bin.ML	Fri Mar 29 13:18:26 1996 +0100
     1.3 @@ -0,0 +1,217 @@
     1.4 +(*  Title:	HOL/Integ/Bin.ML
     1.5 +    Authors:	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6 +		David Spelt, University of Twente 
     1.7 +    Copyright   1994  University of Cambridge
     1.8 +    Copyright   1996 University of Twente
     1.9 +
    1.10 +Arithmetic on binary integers.
    1.11 +*)
    1.12 +
    1.13 +open Bin;
    1.14 +
    1.15 +(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
    1.16 +
    1.17 +qed_goal "norm_Bcons_Plus_0" Bin.thy "norm_Bcons Plus False = Plus"
    1.18 +	(fn prem => [(Simp_tac 1)]);
    1.19 +
    1.20 +qed_goal "norm_Bcons_Plus_1" Bin.thy "norm_Bcons Plus True = Bcons Plus True"
    1.21 +	(fn prem => [(Simp_tac 1)]);
    1.22 +
    1.23 +qed_goal "norm_Bcons_Minus_0" Bin.thy "norm_Bcons Minus False = Bcons Minus False"
    1.24 +	(fn prem => [(Simp_tac 1)]);
    1.25 +
    1.26 +qed_goal "norm_Bcons_Minus_1" Bin.thy "norm_Bcons Minus True = Minus"
    1.27 +	(fn prem => [(Simp_tac 1)]);
    1.28 +
    1.29 +qed_goal "norm_Bcons_Bcons" Bin.thy "norm_Bcons (Bcons w x) b = Bcons (Bcons w x) b"
    1.30 +	(fn prem => [(Simp_tac 1)]);
    1.31 +
    1.32 +qed_goal "bin_succ_Bcons1" Bin.thy "bin_succ(Bcons w True) = Bcons (bin_succ w) False"
    1.33 +	(fn prem => [(Simp_tac 1)]);
    1.34 +
    1.35 +qed_goal "bin_succ_Bcons0" Bin.thy "bin_succ(Bcons w False) =  norm_Bcons w True"
    1.36 +	(fn prem => [(Simp_tac 1)]);
    1.37 +
    1.38 +qed_goal "bin_pred_Bcons1" Bin.thy "bin_pred(Bcons w True) = norm_Bcons w False"
    1.39 +	(fn prem => [(Simp_tac 1)]);
    1.40 +
    1.41 +qed_goal "bin_pred_Bcons0" Bin.thy "bin_pred(Bcons w False) = Bcons (bin_pred w) True"
    1.42 +	(fn prem => [(Simp_tac 1)]);
    1.43 +
    1.44 +qed_goal "bin_minus_Bcons1" Bin.thy "bin_minus(Bcons w True) = bin_pred (Bcons(bin_minus w) False)"
    1.45 +	(fn prem => [(Simp_tac 1)]);
    1.46 +
    1.47 +qed_goal "bin_minus_Bcons0" Bin.thy "bin_minus(Bcons w False) = Bcons (bin_minus w) False"
    1.48 +	(fn prem => [(Simp_tac 1)]);
    1.49 +
    1.50 +(*** bin_add: binary addition ***)
    1.51 +
    1.52 +qed_goal "bin_add_Bcons_Bcons11" Bin.thy "bin_add (Bcons v True) (Bcons w True) = norm_Bcons (bin_add v (bin_succ w)) False"
    1.53 +	(fn prem => [(Simp_tac 1)]);
    1.54 +
    1.55 +qed_goal "bin_add_Bcons_Bcons10" Bin.thy "bin_add (Bcons v True) (Bcons w False) = norm_Bcons (bin_add v w) True"
    1.56 +	(fn prem => [(Simp_tac 1)]);
    1.57 +
    1.58 +(* SHOULD THIS THEOREM BE ADDED TO HOL_SS ? *)
    1.59 +val my = prove_goal HOL.thy "(False = (~P)) = P"
    1.60 +	(fn prem => [(fast_tac HOL_cs 1)]);
    1.61 +
    1.62 +qed_goal "bin_add_Bcons_Bcons0" Bin.thy "bin_add (Bcons v False) (Bcons w y) = norm_Bcons (bin_add v w) y"
    1.63 +	(fn prem => [(simp_tac (!simpset addsimps [my]) 1)]);
    1.64 +
    1.65 +qed_goal "bin_add_Bcons_Plus" Bin.thy "bin_add (Bcons v x) Plus = Bcons v x"
    1.66 +	(fn prems => [(Simp_tac 1)]);
    1.67 +
    1.68 +qed_goal "bin_add_Bcons_Minus" Bin.thy "bin_add (Bcons v x) Minus = bin_pred (Bcons v x)"
    1.69 +	(fn prems => [(Simp_tac 1)]);
    1.70 +
    1.71 +qed_goal "bin_add_Bcons_Bcons" Bin.thy "bin_add (Bcons v x) (Bcons w y) = norm_Bcons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
    1.72 +	(fn prems => [(Simp_tac 1)]);
    1.73 +
    1.74 +
    1.75 +(*** bin_add: binary multiplication ***)
    1.76 +
    1.77 +qed_goal "bin_mult_Bcons1" Bin.thy "bin_mult (Bcons v True) w = bin_add (norm_Bcons (bin_mult v w) False) w"
    1.78 +	(fn prem => [(Simp_tac 1)]);
    1.79 +
    1.80 +qed_goal "bin_mult_Bcons0" Bin.thy "bin_mult (Bcons v False) w = norm_Bcons (bin_mult v w) False"
    1.81 +	(fn prem => [(Simp_tac 1)]);
    1.82 +
    1.83 +
    1.84 +(**** The carry/borrow functions, bin_succ and bin_pred ****)
    1.85 +
    1.86 +(** Lemmas **)
    1.87 +
    1.88 +qed_goal "zadd_assoc_cong" Integ.thy "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
    1.89 +  (fn prems => [(asm_simp_tac (!simpset addsimps (prems @ [zadd_assoc RS sym])) 1)]);
    1.90 +
    1.91 +qed_goal "zadd_assoc_swap" Integ.thy "(z::int) + (v + w) = v + (z + w)"
    1.92 +   (fn prems => [(REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1))]);
    1.93 +
    1.94 +
    1.95 +val my_ss = !simpset setloop (split_tac [expand_if]) ;
    1.96 +
    1.97 +
    1.98 +(**** integ_of_bin ****)
    1.99 +
   1.100 +
   1.101 +qed_goal "integ_of_bin_norm_Bcons" Bin.thy "integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)"
   1.102 +   (fn prems=>[	(bin.induct_tac "w" 1),
   1.103 +		(REPEAT(simp_tac (!simpset setloop (split_tac [expand_if])) 1)) ]);
   1.104 +
   1.105 +qed_goal "integ_of_bin_succ" Bin.thy "integ_of_bin(bin_succ w) = $#1 + integ_of_bin w"
   1.106 +   (fn prems=>[	(rtac bin.induct 1),
   1.107 +		(REPEAT(asm_simp_tac (!simpset addsimps (integ_of_bin_norm_Bcons::zadd_ac)
   1.108 +					       setloop (split_tac [expand_if])) 1)) ]);
   1.109 +
   1.110 +qed_goal "integ_of_bin_pred" Bin.thy "integ_of_bin(bin_pred w) = $~ ($#1) + integ_of_bin w"
   1.111 +   (fn prems=>[	(rtac bin.induct 1),
   1.112 +		(REPEAT(asm_simp_tac (!simpset addsimps (integ_of_bin_norm_Bcons::zadd_ac)
   1.113 +					       setloop (split_tac [expand_if])) 1)) ]);
   1.114 +
   1.115 +qed_goal "integ_of_bin_minus" Bin.thy "integ_of_bin(bin_minus w) = $~ (integ_of_bin w)"
   1.116 +   (fn prems=>[	(rtac bin.induct 1),
   1.117 +		(Simp_tac 1),
   1.118 +		(Simp_tac 1),
   1.119 +		(asm_simp_tac (!simpset
   1.120 +				delsimps [pred_Plus,pred_Minus,pred_Bcons]
   1.121 +				addsimps [integ_of_bin_succ,integ_of_bin_pred,
   1.122 +					  zadd_assoc]
   1.123 +				setloop (split_tac [expand_if])) 1)]);
   1.124 +
   1.125 + 
   1.126 +val bin_add_simps = [add_Plus,add_Minus,bin_add_Bcons_Plus,bin_add_Bcons_Minus,bin_add_Bcons_Bcons,
   1.127 +		     integ_of_bin_succ, integ_of_bin_pred,
   1.128 +		     integ_of_bin_norm_Bcons];
   1.129 +val bin_simps = [iob_Plus,iob_Minus,iob_Bcons];
   1.130 +
   1.131 +goal Bin.thy "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
   1.132 +by (bin.induct_tac "v" 1);
   1.133 +by (simp_tac (my_ss addsimps bin_add_simps) 1);
   1.134 +by (simp_tac (my_ss addsimps bin_add_simps) 1);
   1.135 +by (rtac allI 1);
   1.136 +by (bin.induct_tac "w" 1);
   1.137 +by (asm_simp_tac (my_ss addsimps (bin_add_simps)) 1);
   1.138 +by (asm_simp_tac (my_ss addsimps (bin_add_simps @ zadd_ac)) 1);
   1.139 +by (cut_inst_tac [("P","bool")] True_or_False 1);
   1.140 +by (etac disjE 1);
   1.141 +by (asm_simp_tac (my_ss addsimps (bin_add_simps @ zadd_ac)) 1);
   1.142 +by (asm_simp_tac (my_ss addsimps (bin_add_simps @ zadd_ac)) 1);
   1.143 +val integ_of_bin_add_lemma = result();
   1.144 +
   1.145 +goal Bin.thy "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
   1.146 +by (cut_facts_tac [integ_of_bin_add_lemma] 1);
   1.147 +by (fast_tac HOL_cs 1);
   1.148 +qed "integ_of_bin_add";
   1.149 +
   1.150 +val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add,integ_of_bin_norm_Bcons];
   1.151 +
   1.152 +goal Bin.thy "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w";
   1.153 +by (bin.induct_tac "v" 1);
   1.154 +by (simp_tac (my_ss addsimps bin_mult_simps) 1);
   1.155 +by (simp_tac (my_ss addsimps bin_mult_simps) 1);
   1.156 +by (cut_inst_tac [("P","bool")] True_or_False 1);
   1.157 +by (etac disjE 1);
   1.158 +by (asm_simp_tac (my_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2);
   1.159 +by (asm_simp_tac (my_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac)) 1);
   1.160 +qed "integ_of_bin_mult";
   1.161 +
   1.162 +
   1.163 +Delsimps [succ_Bcons,pred_Bcons,min_Bcons,add_Bcons,mult_Bcons,
   1.164 +	  iob_Plus,iob_Minus,iob_Bcons,
   1.165 +	  norm_Plus,norm_Minus,norm_Bcons];
   1.166 +
   1.167 +Addsimps [integ_of_bin_add RS sym,
   1.168 +	  integ_of_bin_minus RS sym,
   1.169 +	  integ_of_bin_mult RS sym,
   1.170 +	  bin_succ_Bcons1,bin_succ_Bcons0,
   1.171 +	  bin_pred_Bcons1,bin_pred_Bcons0,
   1.172 +	  bin_minus_Bcons1,bin_minus_Bcons0, 
   1.173 +	  bin_add_Bcons_Plus,bin_add_Bcons_Minus,
   1.174 +	  bin_add_Bcons_Bcons0,bin_add_Bcons_Bcons10,bin_add_Bcons_Bcons11,
   1.175 +	  bin_mult_Bcons1,bin_mult_Bcons0,
   1.176 +	  norm_Bcons_Plus_0,norm_Bcons_Plus_1,
   1.177 +	  norm_Bcons_Minus_0,norm_Bcons_Minus_1,
   1.178 +	  norm_Bcons_Bcons];
   1.179 +
   1.180 +(*** Examples of performing binary arithmetic by simplification ***)
   1.181 +
   1.182 +goal Bin.thy "#13  +  #19 = #32";
   1.183 +by (Simp_tac 1);
   1.184 +result();
   1.185 +
   1.186 +goal Bin.thy "#1234  +  #5678 = #6912";
   1.187 +by (Simp_tac 1);
   1.188 +result();
   1.189 +
   1.190 +goal Bin.thy "#1359  +  #~2468 = #~1109";
   1.191 +by (Simp_tac 1);
   1.192 +result();
   1.193 +
   1.194 +goal Bin.thy "#93746 +  #~46375 = #47371";
   1.195 +by (Simp_tac 1);
   1.196 +result();
   1.197 +
   1.198 +goal Bin.thy "$~ #65745 = #~65745";
   1.199 +by (Simp_tac 1);
   1.200 +result();
   1.201 +
   1.202 +goal Bin.thy "$~ #~54321 = #54321";
   1.203 +by (Simp_tac 1);
   1.204 +result();
   1.205 +
   1.206 +goal Bin.thy "#13  *  #19 = #247";
   1.207 +by (Simp_tac 1);
   1.208 +result();
   1.209 +
   1.210 +goal Bin.thy "#~84  *  #51 = #~4284";
   1.211 +by (Simp_tac 1);
   1.212 +result();
   1.213 +
   1.214 +goal Bin.thy "#255  *  #255 = #65025";
   1.215 +by (Simp_tac 1);
   1.216 +result();
   1.217 +
   1.218 +goal Bin.thy "#1359  *  #~2468 = #~3354012";
   1.219 +by (Simp_tac 1);
   1.220 +result();
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Integ/Bin.thy	Fri Mar 29 13:18:26 1996 +0100
     2.3 @@ -0,0 +1,163 @@
     2.4 +(*  Title:	HOL/Integ/Bin.thy
     2.5 +    Authors:	Lawrence C Paulson, Cambridge University Computer Laboratory
     2.6 +		David Spelt, University of Twente 
     2.7 +    Copyright	1994  University of Cambridge
     2.8 +    Copyright   1996 University of Twente
     2.9 +
    2.10 +Arithmetic on binary integers.
    2.11 +
    2.12 +   The sign Plus stands for an infinite string of leading F's.
    2.13 +   The sign Minus stands for an infinite string of leading T's.
    2.14 +
    2.15 +A number can have multiple representations, namely leading F's with sign
    2.16 +Plus and leading T's with sign Minus.  See twos-compl.ML/int_of_binary for
    2.17 +the numerical interpretation.
    2.18 +
    2.19 +The representation expects that (m mod 2) is 0 or 1, even if m is negative;
    2.20 +For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
    2.21 +
    2.22 +Division is not defined yet!
    2.23 +*)
    2.24 +
    2.25 +Bin = Integ + 
    2.26 +
    2.27 +syntax
    2.28 +  "_Int"           :: xnum => int        ("_")
    2.29 +
    2.30 +datatype
    2.31 +   bin = Plus
    2.32 +        | Minus
    2.33 +        | Bcons bin bool
    2.34 +
    2.35 +consts
    2.36 +  integ_of_bin     :: bin=>int
    2.37 +  norm_Bcons       :: [bin,bool]=>bin
    2.38 +  bin_succ         :: bin=>bin
    2.39 +  bin_pred         :: bin=>bin
    2.40 +  bin_minus        :: bin=>bin
    2.41 +  bin_add,bin_mult :: [bin,bin]=>bin
    2.42 +  h_bin :: [bin,bool,bin]=>bin
    2.43 +
    2.44 +(*norm_Bcons adds a bit, suppressing leading 0s and 1s*)
    2.45 +
    2.46 +primrec norm_Bcons bin
    2.47 +  norm_Plus  "norm_Bcons Plus  b = (if b then (Bcons Plus b) else Plus)"
    2.48 +  norm_Minus "norm_Bcons Minus b = (if b then Minus else (Bcons Minus b))"
    2.49 +  norm_Bcons "norm_Bcons (Bcons w' x') b = Bcons (Bcons w' x') b"
    2.50 + 
    2.51 +primrec integ_of_bin bin
    2.52 +  iob_Plus  "integ_of_bin Plus = $#0"
    2.53 +  iob_Minus "integ_of_bin Minus = $~($#1)"
    2.54 +  iob_Bcons "integ_of_bin(Bcons w x) = (if x then $#1 else $#0) + (integ_of_bin w) + (integ_of_bin w)" 
    2.55 +
    2.56 +primrec bin_succ bin
    2.57 +  succ_Plus  "bin_succ Plus = Bcons Plus True" 
    2.58 +  succ_Minus "bin_succ Minus = Plus"
    2.59 +  succ_Bcons "bin_succ(Bcons w x) = (if x then (Bcons (bin_succ w) False) else (norm_Bcons w True))"
    2.60 +
    2.61 +primrec bin_pred bin
    2.62 +  pred_Plus  "bin_pred(Plus) = Minus"
    2.63 +  pred_Minus "bin_pred(Minus) = Bcons Minus False"
    2.64 +  pred_Bcons "bin_pred(Bcons w x) = (if x then (norm_Bcons w False) else (Bcons (bin_pred w) True))"
    2.65 + 
    2.66 +primrec bin_minus bin
    2.67 +  min_Plus  "bin_minus Plus = Plus"
    2.68 +  min_Minus "bin_minus Minus = Bcons Plus True"
    2.69 +  min_Bcons "bin_minus(Bcons w x) = (if x then (bin_pred (Bcons (bin_minus w) False)) else (Bcons (bin_minus w) False))"
    2.70 +
    2.71 +primrec bin_add bin
    2.72 +  add_Plus  "bin_add Plus w = w"
    2.73 +  add_Minus "bin_add Minus w = bin_pred w"
    2.74 +  add_Bcons "bin_add (Bcons v x) w = h_bin v x w"
    2.75 +
    2.76 +primrec bin_mult bin
    2.77 +  mult_Plus "bin_mult Plus w = Plus"
    2.78 +  mult_Minus "bin_mult Minus w = bin_minus w"
    2.79 +  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))"
    2.80 +
    2.81 +primrec h_bin bin
    2.82 +  h_Plus  "h_bin v x Plus =  Bcons v x"
    2.83 +  h_Minus "h_bin v x Minus = bin_pred (Bcons v x)"
    2.84 +  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)" 
    2.85 +
    2.86 +end
    2.87 +
    2.88 +ML
    2.89 +
    2.90 +(** Concrete syntax for integers **)
    2.91 +
    2.92 +local
    2.93 +  open Syntax;
    2.94 +
    2.95 +  (* Bits *)
    2.96 +
    2.97 +  fun mk_bit 0 = const "False"
    2.98 +    | mk_bit 1 = const "True"
    2.99 +    | mk_bit _ = sys_error "mk_bit";
   2.100 +
   2.101 +  fun dest_bit (Const ("False", _)) = 0
   2.102 +    | dest_bit (Const ("True", _)) = 1
   2.103 +    | dest_bit _ = raise Match;
   2.104 +
   2.105 +
   2.106 +  (* Bit strings *)   (*we try to handle superfluous leading digits nicely*)
   2.107 +
   2.108 +  fun prefix_len _ [] = 0
   2.109 +    | prefix_len pred (x :: xs) =
   2.110 +        if pred x then 1 + prefix_len pred xs else 0;
   2.111 +
   2.112 +  fun mk_bin str =
   2.113 +    let
   2.114 +      val (sign, digs) =
   2.115 +        (case explode str of
   2.116 +          "#" :: "~" :: cs => (~1, cs)
   2.117 +        | "#" :: cs => (1, cs)
   2.118 +        | _ => raise ERROR);
   2.119 +
   2.120 +      val zs = prefix_len (equal "0") digs;
   2.121 +
   2.122 +      fun bin_of 0 = replicate zs 0
   2.123 +        | bin_of ~1 = replicate zs 1 @ [~1]
   2.124 +        | bin_of n = (n mod 2) :: bin_of (n div 2);
   2.125 +
   2.126 +      fun term_of [] = const "Plus"
   2.127 +        | term_of [~1] = const "Minus"
   2.128 +        | term_of (b :: bs) = const "Bcons" $ term_of bs $ mk_bit b;
   2.129 +    in
   2.130 +      term_of (bin_of (sign * (#1 (scan_int digs))))
   2.131 +    end;
   2.132 +
   2.133 +  fun dest_bin tm =
   2.134 +    let
   2.135 +      fun bin_of (Const ("Plus", _)) = []
   2.136 +        | bin_of (Const ("Minus", _)) = [~1]
   2.137 +        | bin_of (Const ("Bcons", _) $ bs $ b) = dest_bit b :: bin_of bs
   2.138 +        | bin_of _ = raise Match;
   2.139 +
   2.140 +      fun int_of [] = 0
   2.141 +        | int_of (b :: bs) = b + 2 * int_of bs;
   2.142 +
   2.143 +      val rev_digs = bin_of tm;
   2.144 +      val (sign, zs) =
   2.145 +        (case rev rev_digs of
   2.146 +          ~1 :: bs => ("~", prefix_len (equal 1) bs)
   2.147 +        | bs => ("", prefix_len (equal 0) bs));
   2.148 +      val num = string_of_int (abs (int_of rev_digs));
   2.149 +    in
   2.150 +      "#" ^ sign ^ implode (replicate zs "0") ^ num
   2.151 +    end;
   2.152 +
   2.153 +
   2.154 +  (* translation of integer constant tokens to and from binary *)
   2.155 +
   2.156 +  fun int_tr (*"_Int"*) [t as Free (str, _)] =
   2.157 +        (const "integ_of_bin" $
   2.158 +          (mk_bin str handle ERROR => raise_term "int_tr" [t]))
   2.159 +    | int_tr (*"_Int"*) ts = raise_term "int_tr" ts;
   2.160 +
   2.161 +  fun int_tr' (*"integ_of"*) [t] = const "_Int" $ free (dest_bin t)
   2.162 +    | int_tr' (*"integ_of"*) _ = raise Match;
   2.163 +in
   2.164 +  val parse_translation = [("_Int", int_tr)];
   2.165 +  val print_translation = [("integ_of_bin", int_tr')]; 
   2.166 +end;
     3.1 --- a/src/HOL/Integ/ROOT.ML	Fri Mar 29 13:16:38 1996 +0100
     3.2 +++ b/src/HOL/Integ/ROOT.ML	Fri Mar 29 13:18:26 1996 +0100
     3.3 @@ -8,4 +8,4 @@
     3.4  
     3.5  HOL_build_completed;    (*Cause examples to fail if HOL did*)
     3.6  
     3.7 -time_use_thy "Integ";
     3.8 +time_use_thy "Bin";