# HG changeset patch
# User paulson
# Date 828101906 -3600
# Node ID 39e146ac224c411b0310fc311410ca9e6e758ff8
# Parent  26570790f089b7dc55f896f16e7baed8049109d2
Binary integers and their numeric syntax

diff -r 26570790f089 -r 39e146ac224c src/HOL/Integ/Bin.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Bin.ML	Fri Mar 29 13:18:26 1996 +0100
@@ -0,0 +1,217 @@
+(*  Title:	HOL/Integ/Bin.ML
+    Authors:	Lawrence C Paulson, Cambridge University Computer Laboratory
+		David Spelt, University of Twente 
+    Copyright   1994  University of Cambridge
+    Copyright   1996 University of Twente
+
+Arithmetic on binary integers.
+*)
+
+open Bin;
+
+(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
+
+qed_goal "norm_Bcons_Plus_0" Bin.thy "norm_Bcons Plus False = Plus"
+	(fn prem => [(Simp_tac 1)]);
+
+qed_goal "norm_Bcons_Plus_1" Bin.thy "norm_Bcons Plus True = Bcons Plus True"
+	(fn prem => [(Simp_tac 1)]);
+
+qed_goal "norm_Bcons_Minus_0" Bin.thy "norm_Bcons Minus False = Bcons Minus False"
+	(fn prem => [(Simp_tac 1)]);
+
+qed_goal "norm_Bcons_Minus_1" Bin.thy "norm_Bcons Minus True = Minus"
+	(fn prem => [(Simp_tac 1)]);
+
+qed_goal "norm_Bcons_Bcons" Bin.thy "norm_Bcons (Bcons w x) b = Bcons (Bcons w x) b"
+	(fn prem => [(Simp_tac 1)]);
+
+qed_goal "bin_succ_Bcons1" Bin.thy "bin_succ(Bcons w True) = Bcons (bin_succ w) False"
+	(fn prem => [(Simp_tac 1)]);
+
+qed_goal "bin_succ_Bcons0" Bin.thy "bin_succ(Bcons w False) =  norm_Bcons w True"
+	(fn prem => [(Simp_tac 1)]);
+
+qed_goal "bin_pred_Bcons1" Bin.thy "bin_pred(Bcons w True) = norm_Bcons w False"
+	(fn prem => [(Simp_tac 1)]);
+
+qed_goal "bin_pred_Bcons0" Bin.thy "bin_pred(Bcons w False) = Bcons (bin_pred w) True"
+	(fn prem => [(Simp_tac 1)]);
+
+qed_goal "bin_minus_Bcons1" Bin.thy "bin_minus(Bcons w True) = bin_pred (Bcons(bin_minus w) False)"
+	(fn prem => [(Simp_tac 1)]);
+
+qed_goal "bin_minus_Bcons0" Bin.thy "bin_minus(Bcons w False) = Bcons (bin_minus w) False"
+	(fn prem => [(Simp_tac 1)]);
+
+(*** bin_add: binary addition ***)
+
+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"
+	(fn prem => [(Simp_tac 1)]);
+
+qed_goal "bin_add_Bcons_Bcons10" Bin.thy "bin_add (Bcons v True) (Bcons w False) = norm_Bcons (bin_add v w) True"
+	(fn prem => [(Simp_tac 1)]);
+
+(* SHOULD THIS THEOREM BE ADDED TO HOL_SS ? *)
+val my = prove_goal HOL.thy "(False = (~P)) = P"
+	(fn prem => [(fast_tac HOL_cs 1)]);
+
+qed_goal "bin_add_Bcons_Bcons0" Bin.thy "bin_add (Bcons v False) (Bcons w y) = norm_Bcons (bin_add v w) y"
+	(fn prem => [(simp_tac (!simpset addsimps [my]) 1)]);
+
+qed_goal "bin_add_Bcons_Plus" Bin.thy "bin_add (Bcons v x) Plus = Bcons v x"
+	(fn prems => [(Simp_tac 1)]);
+
+qed_goal "bin_add_Bcons_Minus" Bin.thy "bin_add (Bcons v x) Minus = bin_pred (Bcons v x)"
+	(fn prems => [(Simp_tac 1)]);
+
+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)"
+	(fn prems => [(Simp_tac 1)]);
+
+
+(*** bin_add: binary multiplication ***)
+
+qed_goal "bin_mult_Bcons1" Bin.thy "bin_mult (Bcons v True) w = bin_add (norm_Bcons (bin_mult v w) False) w"
+	(fn prem => [(Simp_tac 1)]);
+
+qed_goal "bin_mult_Bcons0" Bin.thy "bin_mult (Bcons v False) w = norm_Bcons (bin_mult v w) False"
+	(fn prem => [(Simp_tac 1)]);
+
+
+(**** The carry/borrow functions, bin_succ and bin_pred ****)
+
+(** Lemmas **)
+
+qed_goal "zadd_assoc_cong" Integ.thy "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
+  (fn prems => [(asm_simp_tac (!simpset addsimps (prems @ [zadd_assoc RS sym])) 1)]);
+
+qed_goal "zadd_assoc_swap" Integ.thy "(z::int) + (v + w) = v + (z + w)"
+   (fn prems => [(REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1))]);
+
+
+val my_ss = !simpset setloop (split_tac [expand_if]) ;
+
+
+(**** integ_of_bin ****)
+
+
+qed_goal "integ_of_bin_norm_Bcons" Bin.thy "integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)"
+   (fn prems=>[	(bin.induct_tac "w" 1),
+		(REPEAT(simp_tac (!simpset setloop (split_tac [expand_if])) 1)) ]);
+
+qed_goal "integ_of_bin_succ" Bin.thy "integ_of_bin(bin_succ w) = $#1 + integ_of_bin w"
+   (fn prems=>[	(rtac bin.induct 1),
+		(REPEAT(asm_simp_tac (!simpset addsimps (integ_of_bin_norm_Bcons::zadd_ac)
+					       setloop (split_tac [expand_if])) 1)) ]);
+
+qed_goal "integ_of_bin_pred" Bin.thy "integ_of_bin(bin_pred w) = $~ ($#1) + integ_of_bin w"
+   (fn prems=>[	(rtac bin.induct 1),
+		(REPEAT(asm_simp_tac (!simpset addsimps (integ_of_bin_norm_Bcons::zadd_ac)
+					       setloop (split_tac [expand_if])) 1)) ]);
+
+qed_goal "integ_of_bin_minus" Bin.thy "integ_of_bin(bin_minus w) = $~ (integ_of_bin w)"
+   (fn prems=>[	(rtac bin.induct 1),
+		(Simp_tac 1),
+		(Simp_tac 1),
+		(asm_simp_tac (!simpset
+				delsimps [pred_Plus,pred_Minus,pred_Bcons]
+				addsimps [integ_of_bin_succ,integ_of_bin_pred,
+					  zadd_assoc]
+				setloop (split_tac [expand_if])) 1)]);
+
+ 
+val bin_add_simps = [add_Plus,add_Minus,bin_add_Bcons_Plus,bin_add_Bcons_Minus,bin_add_Bcons_Bcons,
+		     integ_of_bin_succ, integ_of_bin_pred,
+		     integ_of_bin_norm_Bcons];
+val bin_simps = [iob_Plus,iob_Minus,iob_Bcons];
+
+goal Bin.thy "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
+by (bin.induct_tac "v" 1);
+by (simp_tac (my_ss addsimps bin_add_simps) 1);
+by (simp_tac (my_ss addsimps bin_add_simps) 1);
+by (rtac allI 1);
+by (bin.induct_tac "w" 1);
+by (asm_simp_tac (my_ss addsimps (bin_add_simps)) 1);
+by (asm_simp_tac (my_ss addsimps (bin_add_simps @ zadd_ac)) 1);
+by (cut_inst_tac [("P","bool")] True_or_False 1);
+by (etac disjE 1);
+by (asm_simp_tac (my_ss addsimps (bin_add_simps @ zadd_ac)) 1);
+by (asm_simp_tac (my_ss addsimps (bin_add_simps @ zadd_ac)) 1);
+val integ_of_bin_add_lemma = result();
+
+goal Bin.thy "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
+by (cut_facts_tac [integ_of_bin_add_lemma] 1);
+by (fast_tac HOL_cs 1);
+qed "integ_of_bin_add";
+
+val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add,integ_of_bin_norm_Bcons];
+
+goal Bin.thy "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w";
+by (bin.induct_tac "v" 1);
+by (simp_tac (my_ss addsimps bin_mult_simps) 1);
+by (simp_tac (my_ss addsimps bin_mult_simps) 1);
+by (cut_inst_tac [("P","bool")] True_or_False 1);
+by (etac disjE 1);
+by (asm_simp_tac (my_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2);
+by (asm_simp_tac (my_ss addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac)) 1);
+qed "integ_of_bin_mult";
+
+
+Delsimps [succ_Bcons,pred_Bcons,min_Bcons,add_Bcons,mult_Bcons,
+	  iob_Plus,iob_Minus,iob_Bcons,
+	  norm_Plus,norm_Minus,norm_Bcons];
+
+Addsimps [integ_of_bin_add RS sym,
+	  integ_of_bin_minus RS sym,
+	  integ_of_bin_mult RS sym,
+	  bin_succ_Bcons1,bin_succ_Bcons0,
+	  bin_pred_Bcons1,bin_pred_Bcons0,
+	  bin_minus_Bcons1,bin_minus_Bcons0, 
+	  bin_add_Bcons_Plus,bin_add_Bcons_Minus,
+	  bin_add_Bcons_Bcons0,bin_add_Bcons_Bcons10,bin_add_Bcons_Bcons11,
+	  bin_mult_Bcons1,bin_mult_Bcons0,
+	  norm_Bcons_Plus_0,norm_Bcons_Plus_1,
+	  norm_Bcons_Minus_0,norm_Bcons_Minus_1,
+	  norm_Bcons_Bcons];
+
+(*** Examples of performing binary arithmetic by simplification ***)
+
+goal Bin.thy "#13  +  #19 = #32";
+by (Simp_tac 1);
+result();
+
+goal Bin.thy "#1234  +  #5678 = #6912";
+by (Simp_tac 1);
+result();
+
+goal Bin.thy "#1359  +  #~2468 = #~1109";
+by (Simp_tac 1);
+result();
+
+goal Bin.thy "#93746 +  #~46375 = #47371";
+by (Simp_tac 1);
+result();
+
+goal Bin.thy "$~ #65745 = #~65745";
+by (Simp_tac 1);
+result();
+
+goal Bin.thy "$~ #~54321 = #54321";
+by (Simp_tac 1);
+result();
+
+goal Bin.thy "#13  *  #19 = #247";
+by (Simp_tac 1);
+result();
+
+goal Bin.thy "#~84  *  #51 = #~4284";
+by (Simp_tac 1);
+result();
+
+goal Bin.thy "#255  *  #255 = #65025";
+by (Simp_tac 1);
+result();
+
+goal Bin.thy "#1359  *  #~2468 = #~3354012";
+by (Simp_tac 1);
+result();
diff -r 26570790f089 -r 39e146ac224c src/HOL/Integ/Bin.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Bin.thy	Fri Mar 29 13:18:26 1996 +0100
@@ -0,0 +1,163 @@
+(*  Title:	HOL/Integ/Bin.thy
+    Authors:	Lawrence C Paulson, Cambridge University Computer Laboratory
+		David Spelt, University of Twente 
+    Copyright	1994  University of Cambridge
+    Copyright   1996 University of Twente
+
+Arithmetic on binary integers.
+
+   The sign Plus stands for an infinite string of leading F's.
+   The sign Minus stands for an infinite string of leading T's.
+
+A number can have multiple representations, namely leading F's with sign
+Plus and leading T's with sign Minus.  See twos-compl.ML/int_of_binary for
+the numerical interpretation.
+
+The representation expects that (m mod 2) is 0 or 1, even if m is negative;
+For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
+
+Division is not defined yet!
+*)
+
+Bin = Integ + 
+
+syntax
+  "_Int"           :: xnum => int        ("_")
+
+datatype
+   bin = Plus
+        | Minus
+        | Bcons bin bool
+
+consts
+  integ_of_bin     :: bin=>int
+  norm_Bcons       :: [bin,bool]=>bin
+  bin_succ         :: bin=>bin
+  bin_pred         :: bin=>bin
+  bin_minus        :: bin=>bin
+  bin_add,bin_mult :: [bin,bin]=>bin
+  h_bin :: [bin,bool,bin]=>bin
+
+(*norm_Bcons adds a bit, suppressing leading 0s and 1s*)
+
+primrec norm_Bcons bin
+  norm_Plus  "norm_Bcons Plus  b = (if b then (Bcons Plus b) else Plus)"
+  norm_Minus "norm_Bcons Minus b = (if b then Minus else (Bcons Minus b))"
+  norm_Bcons "norm_Bcons (Bcons w' x') b = Bcons (Bcons w' x') b"
+ 
+primrec integ_of_bin bin
+  iob_Plus  "integ_of_bin Plus = $#0"
+  iob_Minus "integ_of_bin Minus = $~($#1)"
+  iob_Bcons "integ_of_bin(Bcons w x) = (if x then $#1 else $#0) + (integ_of_bin w) + (integ_of_bin w)" 
+
+primrec bin_succ bin
+  succ_Plus  "bin_succ Plus = Bcons Plus True" 
+  succ_Minus "bin_succ Minus = Plus"
+  succ_Bcons "bin_succ(Bcons w x) = (if x then (Bcons (bin_succ w) False) else (norm_Bcons w True))"
+
+primrec bin_pred bin
+  pred_Plus  "bin_pred(Plus) = Minus"
+  pred_Minus "bin_pred(Minus) = Bcons Minus False"
+  pred_Bcons "bin_pred(Bcons w x) = (if x then (norm_Bcons w False) else (Bcons (bin_pred w) True))"
+ 
+primrec bin_minus bin
+  min_Plus  "bin_minus Plus = Plus"
+  min_Minus "bin_minus Minus = Bcons Plus True"
+  min_Bcons "bin_minus(Bcons w x) = (if x then (bin_pred (Bcons (bin_minus w) False)) else (Bcons (bin_minus w) False))"
+
+primrec bin_add bin
+  add_Plus  "bin_add Plus w = w"
+  add_Minus "bin_add Minus w = bin_pred w"
+  add_Bcons "bin_add (Bcons v x) w = h_bin v x w"
+
+primrec bin_mult bin
+  mult_Plus "bin_mult Plus w = Plus"
+  mult_Minus "bin_mult Minus w = bin_minus w"
+  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))"
+
+primrec h_bin bin
+  h_Plus  "h_bin v x Plus =  Bcons v x"
+  h_Minus "h_bin v x Minus = bin_pred (Bcons v x)"
+  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)" 
+
+end
+
+ML
+
+(** Concrete syntax for integers **)
+
+local
+  open Syntax;
+
+  (* Bits *)
+
+  fun mk_bit 0 = const "False"
+    | mk_bit 1 = const "True"
+    | mk_bit _ = sys_error "mk_bit";
+
+  fun dest_bit (Const ("False", _)) = 0
+    | dest_bit (Const ("True", _)) = 1
+    | dest_bit _ = raise Match;
+
+
+  (* Bit strings *)   (*we try to handle superfluous leading digits nicely*)
+
+  fun prefix_len _ [] = 0
+    | prefix_len pred (x :: xs) =
+        if pred x then 1 + prefix_len pred xs else 0;
+
+  fun mk_bin str =
+    let
+      val (sign, digs) =
+        (case explode str of
+          "#" :: "~" :: cs => (~1, cs)
+        | "#" :: cs => (1, cs)
+        | _ => raise ERROR);
+
+      val zs = prefix_len (equal "0") digs;
+
+      fun bin_of 0 = replicate zs 0
+        | bin_of ~1 = replicate zs 1 @ [~1]
+        | bin_of n = (n mod 2) :: bin_of (n div 2);
+
+      fun term_of [] = const "Plus"
+        | term_of [~1] = const "Minus"
+        | term_of (b :: bs) = const "Bcons" $ term_of bs $ mk_bit b;
+    in
+      term_of (bin_of (sign * (#1 (scan_int digs))))
+    end;
+
+  fun dest_bin tm =
+    let
+      fun bin_of (Const ("Plus", _)) = []
+        | bin_of (Const ("Minus", _)) = [~1]
+        | bin_of (Const ("Bcons", _) $ bs $ b) = dest_bit b :: bin_of bs
+        | bin_of _ = raise Match;
+
+      fun int_of [] = 0
+        | int_of (b :: bs) = b + 2 * int_of bs;
+
+      val rev_digs = bin_of tm;
+      val (sign, zs) =
+        (case rev rev_digs of
+          ~1 :: bs => ("~", prefix_len (equal 1) bs)
+        | bs => ("", prefix_len (equal 0) bs));
+      val num = string_of_int (abs (int_of rev_digs));
+    in
+      "#" ^ sign ^ implode (replicate zs "0") ^ num
+    end;
+
+
+  (* translation of integer constant tokens to and from binary *)
+
+  fun int_tr (*"_Int"*) [t as Free (str, _)] =
+        (const "integ_of_bin" $
+          (mk_bin str handle ERROR => raise_term "int_tr" [t]))
+    | int_tr (*"_Int"*) ts = raise_term "int_tr" ts;
+
+  fun int_tr' (*"integ_of"*) [t] = const "_Int" $ free (dest_bin t)
+    | int_tr' (*"integ_of"*) _ = raise Match;
+in
+  val parse_translation = [("_Int", int_tr)];
+  val print_translation = [("integ_of_bin", int_tr')]; 
+end;
diff -r 26570790f089 -r 39e146ac224c src/HOL/Integ/ROOT.ML
--- a/src/HOL/Integ/ROOT.ML	Fri Mar 29 13:16:38 1996 +0100
+++ b/src/HOL/Integ/ROOT.ML	Fri Mar 29 13:18:26 1996 +0100
@@ -8,4 +8,4 @@
 
 HOL_build_completed;    (*Cause examples to fail if HOL did*)
 
-time_use_thy "Integ";
+time_use_thy "Bin";