# HG changeset patch
# User paulson
# Date 861357294 -7200
# Node ID d38f330e58b324f925fd57c919385ecdd4caa4f9
# Parent  becc227bad4d4de09c5f02a7b57fc779d0c46f46
Renamed sign constructors to eliminate clash with the Plus infix of Sum.thy

diff -r becc227bad4d -r d38f330e58b3 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Fri Apr 18 11:53:55 1997 +0200
+++ b/src/HOL/Integ/Bin.ML	Fri Apr 18 11:54:54 1997 +0200
@@ -12,19 +12,19 @@
 (** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
 
 qed_goal "norm_Bcons_Plus_0" Bin.thy
-    "norm_Bcons Plus False = Plus"
+    "norm_Bcons PlusSign False = PlusSign"
  (fn _ => [(Simp_tac 1)]);
 
 qed_goal "norm_Bcons_Plus_1" Bin.thy
-    "norm_Bcons Plus True = Bcons Plus True"
+    "norm_Bcons PlusSign True = Bcons PlusSign True"
  (fn _ => [(Simp_tac 1)]);
 
 qed_goal "norm_Bcons_Minus_0" Bin.thy
-    "norm_Bcons Minus False = Bcons Minus False"
+    "norm_Bcons MinusSign False = Bcons MinusSign False"
  (fn _ => [(Simp_tac 1)]);
 
 qed_goal "norm_Bcons_Minus_1" Bin.thy
-    "norm_Bcons Minus True = Minus"
+    "norm_Bcons MinusSign True = MinusSign"
  (fn _ => [(Simp_tac 1)]);
 
 qed_goal "norm_Bcons_Bcons" Bin.thy
@@ -74,11 +74,11 @@
  (fn _ => [(simp_tac (!simpset addsimps [lemma]) 1)]);
 
 qed_goal "bin_add_Bcons_Plus" Bin.thy
-    "bin_add (Bcons v x) Plus = Bcons v x"
+    "bin_add (Bcons v x) PlusSign = Bcons v x"
  (fn _ => [(Simp_tac 1)]);
 
 qed_goal "bin_add_Bcons_Minus" Bin.thy
-    "bin_add (Bcons v x) Minus = bin_pred (Bcons v x)"
+    "bin_add (Bcons v x) MinusSign = bin_pred (Bcons v x)"
  (fn _ => [(Simp_tac 1)]);
 
 qed_goal "bin_add_Bcons_Bcons" Bin.thy
@@ -211,11 +211,11 @@
                        zadd_zminus_inverse2]) 1); 
 val iob_eq_eq_diff_0 = result(); 
 
-goal Bin.thy "(integ_of_bin Plus = $# 0) = True"; 
+goal Bin.thy "(integ_of_bin PlusSign = $# 0) = True"; 
   by (stac iob_Plus 1); by (Simp_tac 1); 
 val iob_Plus_eq_0 = result(); 
 
-goal Bin.thy "(integ_of_bin Minus = $# 0) = False"; 
+goal Bin.thy "(integ_of_bin MinusSign = $# 0) = False"; 
   by (stac iob_Minus 1); 
   by (Simp_tac 1);
 val iob_Minus_not_eq_0 = result(); 
@@ -242,11 +242,11 @@
   by (Simp_tac 1); 
 val iob_less_eq_diff_lt_0 = result(); 
 
-goal Bin.thy "(integ_of_bin Plus < $# 0) = False"; 
+goal Bin.thy "(integ_of_bin PlusSign < $# 0) = False"; 
   by (stac iob_Plus 1); by (Simp_tac 1); 
 val iob_Plus_not_lt_0 = result(); 
 
-goal Bin.thy "(integ_of_bin Minus < $# 0) = True"; 
+goal Bin.thy "(integ_of_bin MinusSign < $# 0) = True"; 
   by (stac iob_Minus 1); by (Simp_tac 1);
 val iob_Minus_lt_0 = result(); 
 
diff -r becc227bad4d -r d38f330e58b3 src/HOL/Integ/Bin.thy
--- a/src/HOL/Integ/Bin.thy	Fri Apr 18 11:53:55 1997 +0200
+++ b/src/HOL/Integ/Bin.thy	Fri Apr 18 11:54:54 1997 +0200
@@ -6,17 +6,20 @@
 
 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.
+   The sign PlusSign stands for an infinite string of leading F's.
+   The sign MinusSign 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.
+PlusSign and leading T's with sign MinusSign.  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!
+Division is not defined yet!  To do it efficiently requires computing the
+quotient and remainder using ML and checking the answer using multiplication
+by proof.  Then uniqueness of the quotient and remainder yields theorems
+quoting the previously computed values.  (Or code an oracle...)
 *)
 
 Bin = Integ + 
@@ -25,8 +28,8 @@
   "_Int"           :: xnum => int        ("_")
 
 datatype
-   bin = Plus
-        | Minus
+    bin = PlusSign
+        | MinusSign
         | Bcons bin bool
 
 consts
@@ -41,43 +44,43 @@
 (*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_Plus  "norm_Bcons PlusSign  b = (if b then (Bcons PlusSign b) else PlusSign)"
+  norm_Minus "norm_Bcons MinusSign b = (if b then MinusSign else (Bcons MinusSign 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_Plus  "integ_of_bin PlusSign = $#0"
+  iob_Minus "integ_of_bin MinusSign = $~($#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_Plus  "bin_succ PlusSign = Bcons PlusSign True" 
+  succ_Minus "bin_succ MinusSign = PlusSign"
   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_Plus  "bin_pred(PlusSign) = MinusSign"
+  pred_Minus "bin_pred(MinusSign) = Bcons MinusSign 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_Plus  "bin_minus PlusSign = PlusSign"
+  min_Minus "bin_minus MinusSign = Bcons PlusSign 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_Plus  "bin_add PlusSign w = w"
+  add_Minus "bin_add MinusSign 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_Plus "bin_mult PlusSign w = PlusSign"
+  mult_Minus "bin_mult MinusSign 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_Plus  "h_bin v x PlusSign =  Bcons v x"
+  h_Minus "h_bin v x MinusSign = 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
@@ -120,8 +123,8 @@
         | 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"
+      fun term_of [] = const "PlusSign"
+        | term_of [~1] = const "MinusSign"
         | term_of (b :: bs) = const "Bcons" $ term_of bs $ mk_bit b;
     in
       term_of (bin_of (sign * (#1 (scan_int digs))))
@@ -129,8 +132,8 @@
 
   fun dest_bin tm =
     let
-      fun bin_of (Const ("Plus", _)) = []
-        | bin_of (Const ("Minus", _)) = [~1]
+      fun bin_of (Const ("PlusSign", _)) = []
+        | bin_of (Const ("MinusSign", _)) = [~1]
         | bin_of (Const ("Bcons", _) $ bs $ b) = dest_bit b :: bin_of bs
         | bin_of _ = raise Match;