# HG changeset patch
# User wenzelm
# Date 931288474 -7200
# Node ID 7c3503ae3d785cab5bf4b02cece49952110ffc47
# Parent  21601bc4f3c215cc96057711146fc6d6767738b9
use generic numeral encoding and syntax;

diff -r 21601bc4f3c2 -r 7c3503ae3d78 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Tue Jul 06 21:13:12 1999 +0200
+++ b/src/HOL/Integ/Bin.ML	Tue Jul 06 21:14:34 1999 +0200
@@ -12,59 +12,59 @@
 
 (** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
 
-qed_goal "NCons_Pls_0" Bin.thy
+qed_goal "NCons_Pls_0" thy
     "NCons Pls False = Pls"
  (fn _ => [(Simp_tac 1)]);
 
-qed_goal "NCons_Pls_1" Bin.thy
+qed_goal "NCons_Pls_1" thy
     "NCons Pls True = Pls BIT True"
  (fn _ => [(Simp_tac 1)]);
 
-qed_goal "NCons_Min_0" Bin.thy
+qed_goal "NCons_Min_0" thy
     "NCons Min False = Min BIT False"
  (fn _ => [(Simp_tac 1)]);
 
-qed_goal "NCons_Min_1" Bin.thy
+qed_goal "NCons_Min_1" thy
     "NCons Min True = Min"
  (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_succ_1" Bin.thy
+qed_goal "bin_succ_1" thy
     "bin_succ(w BIT True) = (bin_succ w) BIT False"
  (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_succ_0" Bin.thy
+qed_goal "bin_succ_0" thy
     "bin_succ(w BIT False) =  NCons w True"
  (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_pred_1" Bin.thy
+qed_goal "bin_pred_1" thy
     "bin_pred(w BIT True) = NCons w False"
  (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_pred_0" Bin.thy
+qed_goal "bin_pred_0" thy
     "bin_pred(w BIT False) = (bin_pred w) BIT True"
  (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_minus_1" Bin.thy
+qed_goal "bin_minus_1" thy
     "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)"
  (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_minus_0" Bin.thy
+qed_goal "bin_minus_0" thy
     "bin_minus(w BIT False) = (bin_minus w) BIT False"
  (fn _ => [(Simp_tac 1)]);
 
 
 (*** bin_add: binary addition ***)
 
-qed_goal "bin_add_BIT_11" Bin.thy
+qed_goal "bin_add_BIT_11" thy
     "bin_add (v BIT True) (w BIT True) = \
 \    NCons (bin_add v (bin_succ w)) False"
  (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_add_BIT_10" Bin.thy
+qed_goal "bin_add_BIT_10" thy
     "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True"
  (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_add_BIT_0" Bin.thy
+qed_goal "bin_add_BIT_0" thy
     "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"
  (fn _ => [Auto_tac]);
 
@@ -73,11 +73,11 @@
 by Auto_tac;
 qed "bin_add_Pls_right";
 
-qed_goal "bin_add_BIT_Min" Bin.thy
+qed_goal "bin_add_BIT_Min" thy
     "bin_add (v BIT x) Min = bin_pred (v BIT x)"
  (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_add_BIT_BIT" Bin.thy
+qed_goal "bin_add_BIT_BIT" thy
     "bin_add (v BIT x) (w BIT y) = \
 \    NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
  (fn _ => [(Simp_tac 1)]);
@@ -85,11 +85,11 @@
 
 (*** bin_mult: binary multiplication ***)
 
-qed_goal "bin_mult_1" Bin.thy
+qed_goal "bin_mult_1" thy
     "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"
  (fn _ => [(Simp_tac 1)]);
 
-qed_goal "bin_mult_0" Bin.thy
+qed_goal "bin_mult_0" thy
     "bin_mult (v BIT False) w = NCons (bin_mult v w) False"
  (fn _ => [(Simp_tac 1)]);
 
@@ -97,73 +97,73 @@
 (**** The carry/borrow functions, bin_succ and bin_pred ****)
 
 
-(**** integ_of ****)
+(**** number_of ****)
 
-qed_goal "integ_of_NCons" Bin.thy
-    "integ_of(NCons w b) = integ_of(w BIT b)"
+qed_goal "number_of_NCons" thy
+    "number_of(NCons w b) = (number_of(w BIT b)::int)"
  (fn _ =>[(induct_tac "w" 1),
           (ALLGOALS Asm_simp_tac) ]);
 
-Addsimps [integ_of_NCons];
+Addsimps [number_of_NCons];
 
-qed_goal "integ_of_succ" Bin.thy
-    "integ_of(bin_succ w) = int 1 + integ_of w"
- (fn _ =>[(rtac bin.induct 1),
+qed_goal "number_of_succ" thy
+    "number_of(bin_succ w) = int 1 + number_of w"
+ (fn _ =>[induct_tac "w" 1,
           (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]);
 
-qed_goal "integ_of_pred" Bin.thy
-    "integ_of(bin_pred w) = - (int 1) + integ_of w"
- (fn _ =>[(rtac bin.induct 1),
+qed_goal "number_of_pred" thy
+    "number_of(bin_pred w) = - (int 1) + number_of w"
+ (fn _ =>[induct_tac "w" 1,
           (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]);
 
-Goal "integ_of(bin_minus w) = - (integ_of w)";
-by (rtac bin.induct 1);
+Goal "number_of(bin_minus w) = (- (number_of w)::int)";
+by (induct_tac "w" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (asm_simp_tac (simpset()
 		  delsimps [bin_pred_Pls, bin_pred_Min, bin_pred_BIT]
-		  addsimps [integ_of_succ,integ_of_pred,
+		  addsimps [number_of_succ,number_of_pred,
 			    zadd_assoc]) 1);
-qed "integ_of_minus";
+qed "number_of_minus";
 
  
-val bin_add_simps = [bin_add_BIT_BIT, integ_of_succ, integ_of_pred];
+val bin_add_simps = [bin_add_BIT_BIT, number_of_succ, number_of_pred];
 
 (*This proof is complicated by the mutual recursion*)
-Goal "! w. integ_of(bin_add v w) = integ_of v + integ_of w";
+Goal "! w. number_of(bin_add v w) = (number_of v + number_of w::int)";
 by (induct_tac "v" 1);
 by (simp_tac (simpset() addsimps bin_add_simps) 1);
 by (simp_tac (simpset() addsimps bin_add_simps) 1);
 by (rtac allI 1);
 by (induct_tac "w" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps bin_add_simps @ zadd_ac)));
-qed_spec_mp "integ_of_add";
+qed_spec_mp "number_of_add";
 
 
 (*Subtraction*)
 Goalw [zdiff_def]
-     "integ_of v - integ_of w = integ_of(bin_add v (bin_minus w))";
-by (simp_tac (simpset() addsimps [integ_of_add, integ_of_minus]) 1);
-qed "diff_integ_of_eq";
+     "number_of v - number_of w = (number_of(bin_add v (bin_minus w))::int)";
+by (simp_tac (simpset() addsimps [number_of_add, number_of_minus]) 1);
+qed "diff_number_of_eq";
 
-val bin_mult_simps = [zmult_zminus, integ_of_minus, integ_of_add];
+val bin_mult_simps = [zmult_zminus, number_of_minus, number_of_add];
 
-Goal "integ_of(bin_mult v w) = integ_of v * integ_of w";
+Goal "number_of(bin_mult v w) = (number_of v * number_of w::int)";
 by (induct_tac "v" 1);
 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
 by (asm_simp_tac
     (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1);
-qed "integ_of_mult";
+qed "number_of_mult";
 
 
 (** Simplification rules with integer constants **)
 
-Goal "#0 + z = z";
+Goal "#0 + z = (z::int)";
 by (Simp_tac 1);
 qed "zadd_0";
 
-Goal "z + #0 = z";
+Goal "z + #0 = (z::int)";
 by (Simp_tac 1);
 qed "zadd_0_right";
 
@@ -173,28 +173,28 @@
 (** Converting simple cases of (int n) to numerals **)
 
 (*int 0 = #0 *)
-bind_thm ("int_0", integ_of_Pls RS sym);
+bind_thm ("int_0", number_of_Pls RS sym);
 
 Goal "int (Suc n) = #1 + int n";
 by (simp_tac (simpset() addsimps [zadd_int]) 1);
 qed "int_Suc";
 
-Goal "- (#0) = #0";
+Goal "- (#0) = (#0::int)";
 by (Simp_tac 1);
 qed "zminus_0";
 
 Addsimps [zminus_0];
 
 
-Goal "#0 - x = -x";
+Goal "(#0::int) - x = -x";
 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
 qed "zdiff0";
 
-Goal "x - #0 = x";
+Goal "x - (#0::int) = x";
 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
 qed "zdiff0_right";
 
-Goal "x - x = #0";
+Goal "x - x = (#0::int)";
 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
 qed "zdiff_self";
 
@@ -202,45 +202,45 @@
 
 (** Distributive laws for constants only **)
 
-Addsimps (map (read_instantiate_sg (sign_of Bin.thy) [("w", "integ_of ?v")])
+Addsimps (map (read_instantiate_sg (sign_of thy) [("w", "number_of ?v")])
 	  [zadd_zmult_distrib, zadd_zmult_distrib2,
 	   zdiff_zmult_distrib, zdiff_zmult_distrib2]);
 
 (** Special-case simplification for small constants **)
 
-Goal "#0 * z = #0";
+Goal "#0 * z = (#0::int)";
 by (Simp_tac 1);
 qed "zmult_0";
 
-Goal "z * #0 = #0";
+Goal "z * #0 = (#0::int)";
 by (Simp_tac 1);
 qed "zmult_0_right";
 
-Goal "#1 * z = z";
+Goal "#1 * z = (z::int)";
 by (Simp_tac 1);
 qed "zmult_1";
 
-Goal "z * #1 = z";
+Goal "z * #1 = (z::int)";
 by (Simp_tac 1);
 qed "zmult_1_right";
 
 (*For specialist use*)
-Goal "#2 * z = z+z";
+Goal "#2 * z = (z+z::int)";
 by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
 qed "zmult_2";
 
-Goal "z * #2 = z+z";
+Goal "z * #2 = (z+z::int)";
 by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
 qed "zmult_2_right";
 
 Addsimps [zmult_0, zmult_0_right, 
 	  zmult_1, zmult_1_right];
 
-Goal "(w < z + #1) = (w<z | w=z)";
+Goal "(w < z + (#1::int)) = (w<z | w=z)";
 by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1);
 qed "zless_add1_eq";
 
-Goal "(w + #1 <= z) = (w<z)";
+Goal "(w + (#1::int) <= z) = (w<z)";
 by (simp_tac (simpset() addsimps [add_int_Suc_zle_eq]) 1);
 qed "add1_zle_eq";
 Addsimps [add1_zle_eq];
@@ -286,94 +286,94 @@
 (** Equals (=) **)
 
 Goalw [iszero_def]
-  "(integ_of x = integ_of y) = iszero(integ_of (bin_add x (bin_minus y)))"; 
+  "((number_of x::int) = number_of y) = iszero(number_of (bin_add x (bin_minus y)))"; 
 by (simp_tac (simpset() addsimps
-              (zcompare_rls @ [integ_of_add, integ_of_minus])) 1); 
-qed "eq_integ_of_eq"; 
+              (zcompare_rls @ [number_of_add, number_of_minus])) 1); 
+qed "eq_number_of_eq"; 
 
-Goalw [iszero_def] "iszero (integ_of Pls)"; 
+Goalw [iszero_def] "iszero ((number_of Pls)::int)"; 
 by (Simp_tac 1); 
-qed "iszero_integ_of_Pls"; 
+qed "iszero_number_of_Pls"; 
 
-Goalw [iszero_def] "~ iszero(integ_of Min)"; 
+Goalw [iszero_def] "~ iszero ((number_of Min)::int)"; 
 by (Simp_tac 1);
-qed "nonzero_integ_of_Min"; 
+qed "nonzero_number_of_Min"; 
 
 Goalw [iszero_def]
-     "iszero (integ_of (w BIT x)) = (~x & iszero (integ_of w))"; 
+     "iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))"; 
 by (Simp_tac 1);
-by (int_case_tac "integ_of w" 1); 
+by (int_case_tac "number_of w" 1); 
 by (ALLGOALS (asm_simp_tac 
 	      (simpset() addsimps zcompare_rls @ 
 				  [zminus_zadd_distrib RS sym, 
 				   zadd_int]))); 
-qed "iszero_integ_of_BIT"; 
+qed "iszero_number_of_BIT"; 
 
-Goal "iszero (integ_of (w BIT False)) = iszero (integ_of w)"; 
-by (simp_tac (HOL_ss addsimps [iszero_integ_of_BIT]) 1); 
-qed "iszero_integ_of_0"; 
+Goal "iszero (number_of (w BIT False)) = iszero (number_of w::int)"; 
+by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); 
+qed "iszero_number_of_0"; 
 
-Goal "~ iszero (integ_of (w BIT True))"; 
-by (simp_tac (HOL_ss addsimps [iszero_integ_of_BIT]) 1); 
-qed "iszero_integ_of_1"; 
+Goal "~ iszero (number_of (w BIT True)::int)"; 
+by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); 
+qed "iszero_number_of_1"; 
 
 
 
 (** Less-than (<) **)
 
 Goalw [zless_def,zdiff_def] 
-    "integ_of x < integ_of y \
-\    = neg (integ_of (bin_add x (bin_minus y)))";
+    "(number_of x::int) < number_of y \
+\    = neg (number_of (bin_add x (bin_minus y)))";
 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
-qed "less_integ_of_eq_neg"; 
+qed "less_number_of_eq_neg"; 
 
-Goal "~ neg (integ_of Pls)"; 
+Goal "~ neg (number_of Pls)"; 
 by (Simp_tac 1); 
-qed "not_neg_integ_of_Pls"; 
+qed "not_neg_number_of_Pls"; 
 
-Goal "neg (integ_of Min)"; 
+Goal "neg (number_of Min)"; 
 by (Simp_tac 1);
-qed "neg_integ_of_Min"; 
+qed "neg_number_of_Min"; 
 
-Goal "neg (integ_of (w BIT x)) = neg (integ_of w)"; 
+Goal "neg (number_of (w BIT x)) = neg (number_of w)"; 
 by (Asm_simp_tac 1); 
-by (int_case_tac "integ_of w" 1); 
+by (int_case_tac "number_of w" 1); 
 by (ALLGOALS (asm_simp_tac 
 	      (simpset() addsimps [zadd_int, neg_eq_less_nat0, 
 				   symmetric zdiff_def] @ zcompare_rls))); 
-qed "neg_integ_of_BIT"; 
+qed "neg_number_of_BIT"; 
 
 
 (** Less-than-or-equals (<=) **)
 
-Goal "(integ_of x <= integ_of y) = (~ integ_of y < integ_of x)";
+Goal "(number_of x <= (number_of y::int)) = (~ number_of y < (number_of x::int))";
 by (simp_tac (simpset() addsimps [zle_def]) 1);
-qed "le_integ_of_eq_not_less"; 
+qed "le_number_of_eq_not_less"; 
 
 (*Delete the original rewrites, with their clumsy conditional expressions*)
 Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, 
           NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT];
 
 (*Hide the binary representation of integer constants*)
-Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT];
+Delsimps [number_of_Pls, number_of_Min, number_of_BIT];
 
 (*simplification of arithmetic operations on integer constants*)
 val bin_arith_extra_simps =
-    [integ_of_add RS sym,
-     integ_of_minus RS sym,
-     integ_of_mult RS sym,
+    [number_of_add RS sym,
+     number_of_minus RS sym,
+     number_of_mult RS sym,
      bin_succ_1, bin_succ_0, 
      bin_pred_1, bin_pred_0, 
      bin_minus_1, bin_minus_0,  
      bin_add_Pls_right, bin_add_BIT_Min,
      bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
-     diff_integ_of_eq, 
+     diff_number_of_eq, 
      bin_mult_1, bin_mult_0, 
      NCons_Pls_0, NCons_Pls_1, 
      NCons_Min_0, NCons_Min_1, NCons_BIT];
 
 (*For making a minimal simpset, one must include these default simprules
-  of Bin.thy.  Also include simp_thms, or at least (~False)=True*)
+  of thy.  Also include simp_thms, or at least (~False)=True*)
 val bin_arith_simps =
     [bin_pred_Pls, bin_pred_Min,
      bin_succ_Pls, bin_succ_Min,
@@ -383,11 +383,11 @@
 
 (*Simplification of relational operations*)
 val bin_rel_simps =
-    [eq_integ_of_eq, iszero_integ_of_Pls, nonzero_integ_of_Min,
-     iszero_integ_of_0, iszero_integ_of_1,
-     less_integ_of_eq_neg,
-     not_neg_integ_of_Pls, neg_integ_of_Min, neg_integ_of_BIT,
-     le_integ_of_eq_not_less];
+    [eq_number_of_eq, iszero_number_of_Pls, nonzero_number_of_Min,
+     iszero_number_of_0, iszero_number_of_1,
+     less_number_of_eq_neg,
+     not_neg_number_of_Pls, neg_number_of_Min, neg_number_of_BIT,
+     le_number_of_eq_not_less];
 
 Addsimps bin_arith_extra_simps;
 Addsimps bin_rel_simps;
@@ -410,23 +410,6 @@
 
 val lessD = Nat_LA_Data.lessD @ [add1_zle_eq RS iffD2];
 
-(* borrowed from Bin.thy: *)
-fun dest_bit (Const ("False", _)) = 0
-  | dest_bit (Const ("True", _)) = 1
-  | dest_bit _ = raise Match;
-
-fun dest_bin tm =
-  let
-    fun bin_of (Const ("Bin.bin.Pls", _)) = []
-      | bin_of (Const ("Bin.bin.Min", _)) = [~1]
-      | bin_of (Const ("Bin.bin.op BIT", _) $ 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;
-
-  in int_of(bin_of tm) end;
-
 fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i)
                            | Some n => (overwrite(p,(t,n+m:int)), i));
 
@@ -434,10 +417,10 @@
 fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
   | poly(Const("op -",_) $ s $ t, m, pi) = poly(s,m,poly(t,~1*m,pi))
   | poly(Const("uminus",_) $ t, m, pi) =   poly(t,~1*m,pi)
-  | poly(all as Const("op *",_) $ (Const("Bin.integ_of",_)$c) $ t, m, pi) =
-      (poly(t,m*dest_bin c,pi) handle Match => add_atom(all,m,pi))
-  | poly(all as Const("Bin.integ_of",_)$t,m,(p,i)) =
-     ((p,i + m*dest_bin t) handle Match => add_atom(all,m,(p,i)))
+  | poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi) =
+      (poly(t,m*NumeralSyntax.dest_bin c,pi) handle Match => add_atom(all,m,pi))
+  | poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) =
+     ((p,i + m*NumeralSyntax.dest_bin t) handle Match => add_atom(all,m,(p,i)))
   | poly x  = add_atom x;
 
 fun decomp2(rel,lhs,rhs) =
@@ -541,66 +524,66 @@
 
 (** Simplification of arithmetic when nested to the right **)
 
-Goal "integ_of v + (integ_of w + z) = integ_of(bin_add v w) + z";
+Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::int)";
 by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
-qed "add_integ_of_left";
+qed "add_number_of_left";
 
-Goal "integ_of v * (integ_of w * z) = integ_of(bin_mult v w) * z";
+Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::int)";
 by (simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
-qed "mult_integ_of_left";
+qed "mult_number_of_left";
 
-Addsimps [add_integ_of_left, mult_integ_of_left];
+Addsimps [add_number_of_left, mult_number_of_left];
 
 (** Simplification of inequalities involving numerical constants **)
 
-Goal "(w <= z + #1) = (w<=z | w = z + #1)";
+Goal "(w <= z + (#1::int)) = (w<=z | w = z + (#1::int))";
 by (arith_tac 1);
 qed "zle_add1_eq";
 
-Goal "(w <= z - #1) = (w<z)";
+Goal "(w <= z - (#1::int)) = (w<(z::int))";
 by (arith_tac 1);
 qed "zle_diff1_eq";
 Addsimps [zle_diff1_eq];
 
 (*2nd premise can be proved automatically if v is a literal*)
-Goal "[| w <= z; #0 <= v |] ==> w <= z + v";
+Goal "[| w <= z; #0 <= v |] ==> w <= z + (v::int)";
 by (fast_arith_tac 1);
 qed "zle_imp_zle_zadd";
 
-Goal "w <= z ==> w <= z + #1";
+Goal "w <= z ==> w <= z + (#1::int)";
 by (fast_arith_tac 1);
 qed "zle_imp_zle_zadd1";
 
 (*2nd premise can be proved automatically if v is a literal*)
-Goal "[| w < z; #0 <= v |] ==> w < z + v";
+Goal "[| w < z; #0 <= v |] ==> w < z + (v::int)";
 by (fast_arith_tac 1);
 qed "zless_imp_zless_zadd";
 
-Goal "w < z ==> w < z + #1";
+Goal "w < z ==> w < z + (#1::int)";
 by (fast_arith_tac 1);
 qed "zless_imp_zless_zadd1";
 
-Goal "(w < z + #1) = (w<=z)";
+Goal "(w < z + #1) = (w<=(z::int))";
 by (arith_tac 1);
 qed "zle_add1_eq_le";
 Addsimps [zle_add1_eq_le];
 
-Goal "(z = z + w) = (w = #0)";
+Goal "(z = z + w) = (w = (#0::int))";
 by (arith_tac 1);
 qed "zadd_left_cancel0";
 Addsimps [zadd_left_cancel0];
 
 (*LOOPS as a simprule!*)
-Goal "[| w + v < z; #0 <= v |] ==> w < z";
+Goal "[| w + v < z; #0 <= v |] ==> w < (z::int)";
 by (fast_arith_tac 1);
 qed "zless_zadd_imp_zless";
 
 (*LOOPS as a simprule!  Analogous to Suc_lessD*)
-Goal "w + #1 < z ==> w < z";
+Goal "w + #1 < z ==> w < (z::int)";
 by (fast_arith_tac 1);
 qed "zless_zadd1_imp_zless";
 
-Goal "w + #-1 = w - #1";
+Goal "w + #-1 = w - (#1::int)";
 by (Simp_tac 1);
 qed "zplus_minus1_conv";
 
diff -r 21601bc4f3c2 -r 7c3503ae3d78 src/HOL/Integ/Bin.thy
--- a/src/HOL/Integ/Bin.thy	Tue Jul 06 21:13:12 1999 +0200
+++ b/src/HOL/Integ/Bin.thy	Tue Jul 06 21:14:34 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title:	HOL/Integ/Bin.thy
+    ID:         $Id$
     Authors:	Lawrence C Paulson, Cambridge University Computer Laboratory
 		David Spelt, University of Twente 
     Copyright	1994  University of Cambridge
@@ -22,36 +23,29 @@
 quoting the previously computed values.  (Or code an oracle...)
 *)
 
-Bin = Int + Datatype +
-
-syntax
-  "_Int"           :: xnum => int        ("_")
-
-datatype
-    bin = Pls
-        | Min
-        | BIT bin bool	(infixl 90)
+Bin = Int + Numeral +
 
 consts
-  integ_of         :: bin=>int
   NCons            :: [bin,bool]=>bin
   bin_succ         :: bin=>bin
   bin_pred         :: bin=>bin
   bin_minus        :: bin=>bin
   bin_add,bin_mult :: [bin,bin]=>bin
-  adding            :: [bin,bool,bin]=>bin
+  adding           :: [bin,bool,bin]=>bin
 
 (*NCons inserts a bit, suppressing leading 0s and 1s*)
 primrec
   NCons_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)"
   NCons_Min "NCons Min b = (if b then Min else (Min BIT b))"
   NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b"
- 
+
+instance
+  int :: numeral 
 primrec
-  integ_of_Pls  "integ_of Pls = int 0"
-  integ_of_Min  "integ_of Min = - (int 1)"
-  integ_of_BIT  "integ_of(w BIT x) = (if x then int 1 else int 0) +
-	                             (integ_of w) + (integ_of w)" 
+  number_of_Pls  "number_of Pls = int 0"
+  number_of_Min  "number_of Min = - (int 1)"
+  number_of_BIT  "number_of(w BIT x) = (if x then int 1 else int 0) +
+	                             (number_of w) + (number_of w)" 
 
 primrec
   bin_succ_Pls  "bin_succ Pls = Pls BIT True" 
@@ -95,85 +89,3 @@
 
 
 end
-
-ML
-
-(** Concrete syntax for integers **)
-
-local
-
-  (* Bits *)
-
-  fun mk_bit 0 = Syntax.const "False"
-    | mk_bit 1 = Syntax.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 Symbol.explode str of
-          "#" :: "-" :: cs => (~1, cs)
-        | "#" :: cs => (1, cs)
-        | _ => raise ERROR);
-
-      fun bin_of 0  = []
-        | bin_of ~1 = [~1]
-        | bin_of n  = (n mod 2) :: bin_of (n div 2);
-
-      fun term_of []   = Syntax.const "Bin.bin.Pls"
-        | term_of [~1] = Syntax.const "Bin.bin.Min"
-        | term_of (b :: bs) = Syntax.const "Bin.bin.op BIT" $ term_of bs $ mk_bit b;
-    in
-      term_of (bin_of (sign * (#1 (read_int digs))))
-    end;
-
-  fun dest_bin tm =
-    let
-      (*we consider both "spellings", since Min might be declared elsewhere*)
-      fun bin_of (Const ("Pls", _))     = []
-        | bin_of (Const ("bin.Pls", _)) = []
-        | bin_of (Const ("Min", _))     = [~1]
-        | bin_of (Const ("bin.Min", _)) = [~1]
-        | bin_of (Const ("op BIT", _) $ bs $ b)     = dest_bit b :: bin_of bs
-        | bin_of (Const ("bin.op BIT", _) $ 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, _)] =
-        (Syntax.const "integ_of" $
-          (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] =
-        Syntax.const "_Int" $ (Syntax.const "_xnum" $ Syntax.free (dest_bin t))
-    | int_tr' (*"integ_of"*) _ = raise Match;
-in
-  val parse_translation = [("_Int", int_tr)];
-  val print_translation = [("integ_of", int_tr')]; 
-end;