# HG changeset patch
# User paulson
# Date 1088677793 -7200
# Node ID 34264f5e469148496dafeab48b4796c0d7d16a81
# Parent  28fa57b57209a64176422acd672f8e9fe6f2cd04
new treatment of binary numerals

diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Complex/CLim.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -666,8 +666,8 @@
 apply (subgoal_tac "xa + - (hcomplex_of_complex x) \<noteq> 0")
  prefer 2 apply (simp add: compare_rls) 
 apply (drule_tac x = "- hcomplex_of_complex x + xa" in bspec)
- prefer 2 apply (simp add: hcomplex_add_assoc [symmetric]) 
-apply (auto simp add: mem_cinfmal_iff [symmetric] hcomplex_add_commute)
+ prefer 2 apply (simp add: add_assoc [symmetric]) 
+apply (auto simp add: mem_cinfmal_iff [symmetric] add_commute)
 apply (drule_tac c = "xa + - hcomplex_of_complex x" in capprox_mult1)
 apply (auto intro: CInfinitesimal_subset_CFinite [THEN subsetD]
             simp add: mult_assoc)
@@ -740,7 +740,7 @@
 		    CInfinitesimal_add CInfinitesimal_mult
 		    CInfinitesimal_hcomplex_of_complex_mult
 		    CInfinitesimal_hcomplex_of_complex_mult2
-            simp add: hcomplex_add_assoc [symmetric])
+            simp add: add_assoc [symmetric])
 done
 
 lemma CDERIV_mult:
@@ -899,7 +899,7 @@
      "CDERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
 apply (induct_tac "n")
 apply (drule_tac [2] CDERIV_Id [THEN CDERIV_mult])
-apply (auto simp add: complex_of_real_add [symmetric] left_distrib real_of_nat_Suc)
+apply (auto simp add: left_distrib real_of_nat_Suc)
 apply (case_tac "n")
 apply (auto simp add: mult_ac add_commute)
 done
@@ -930,7 +930,8 @@
 apply (simp add: hcomplex_add_commute numeral_2_eq_2 inverse_add
                  inverse_mult_distrib [symmetric] inverse_minus_eq [symmetric]
                  add_ac mult_ac 
-            del: inverse_minus_eq inverse_mult_distrib minus_mult_right [symmetric] minus_mult_left [symmetric])
+            del: inverse_minus_eq inverse_mult_distrib
+                 minus_mult_right [symmetric] minus_mult_left [symmetric])
 apply (simp only: mult_assoc [symmetric] right_distrib)
 apply (rule_tac y = " inverse (- hcomplex_of_complex x * hcomplex_of_complex x) " in capprox_trans)
 apply (rule inverse_add_CInfinitesimal_capprox2)
@@ -952,7 +953,8 @@
      "[| CDERIV f x :> d; f(x) \<noteq> 0 |]
       ==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
 apply (rule mult_commute [THEN subst])
-apply (simp (no_asm_simp) add: minus_mult_left power_inverse del: complexpow_Suc minus_mult_left [symmetric])
+apply (simp add: minus_mult_left power_inverse
+            del: complexpow_Suc minus_mult_left [symmetric])
 apply (fold o_def)
 apply (blast intro!: CDERIV_chain CDERIV_inverse)
 done
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Complex/CSeries.thy
--- a/src/HOL/Complex/CSeries.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Complex/CSeries.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -72,7 +72,7 @@
 
 lemma sumc_const [simp]: "sumc 0 n (%i. r) = complex_of_real (real n) * r"
 apply (induct_tac "n")
-apply (auto simp add: left_distrib complex_of_real_add [symmetric] real_of_nat_Suc)
+apply (auto simp add: left_distrib real_of_nat_Suc)
 done
 
 lemma sumc_add_mult_const:
@@ -98,16 +98,16 @@
 
 lemma sumc_interval_const [rule_format (no_asm)]:
      "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na  
-                 --> sumc m na f = (complex_of_real(real (na - m)) * r)"
+      --> sumc m na f = (complex_of_real(real (na - m)) * r)"
 apply (induct_tac "na")
-apply (auto simp add: Suc_diff_le real_of_nat_Suc complex_of_real_add [symmetric] left_distrib)
+apply (auto simp add: Suc_diff_le real_of_nat_Suc left_distrib)
 done
 
 lemma sumc_interval_const2 [rule_format (no_asm)]:
      "(\<forall>n. m \<le> n --> f n = r) & m \<le> na  
       --> sumc m na f = (complex_of_real(real (na - m)) * r)"
 apply (induct_tac "na")
-apply (auto simp add: left_distrib Suc_diff_le real_of_nat_Suc complex_of_real_add [symmetric])
+apply (auto simp add: left_distrib Suc_diff_le real_of_nat_Suc)
 done
 
 (*** 
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Complex/Complex.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -291,35 +291,33 @@
      "(complex_of_real x = complex_of_real y) = (x = y)"
 by (simp add: complex_of_real_def)
 
-lemma complex_of_real_minus: "complex_of_real(-x) = - complex_of_real x"
+lemma complex_of_real_minus [simp]: "complex_of_real(-x) = - complex_of_real x"
 by (simp add: complex_of_real_def complex_minus)
 
-lemma complex_of_real_inverse:
+lemma complex_of_real_inverse [simp]:
      "complex_of_real(inverse x) = inverse(complex_of_real x)"
 apply (case_tac "x=0", simp)
-apply (simp add: complex_inverse complex_of_real_def real_divide_def
-                 inverse_mult_distrib power2_eq_square)
+apply (simp add: complex_of_real_def divide_inverse power2_eq_square)
 done
 
-lemma complex_of_real_add:
-     "complex_of_real x + complex_of_real y = complex_of_real (x + y)"
+lemma complex_of_real_add [simp]:
+     "complex_of_real (x + y) = complex_of_real x + complex_of_real y"
 by (simp add: complex_add complex_of_real_def)
 
-lemma complex_of_real_diff:
-     "complex_of_real x - complex_of_real y = complex_of_real (x - y)"
-by (simp add: complex_of_real_minus [symmetric] complex_diff_def 
-              complex_of_real_add)
+lemma complex_of_real_diff [simp]:
+     "complex_of_real (x - y) = complex_of_real x - complex_of_real y"
+by (simp add: complex_of_real_minus diff_minus)
 
-lemma complex_of_real_mult:
-     "complex_of_real x * complex_of_real y = complex_of_real (x * y)"
+lemma complex_of_real_mult [simp]:
+     "complex_of_real (x * y) = complex_of_real x * complex_of_real y"
 by (simp add: complex_mult complex_of_real_def)
 
-lemma complex_of_real_divide:
-      "complex_of_real x / complex_of_real y = complex_of_real(x/y)"
+lemma complex_of_real_divide [simp]:
+      "complex_of_real(x/y) = complex_of_real x / complex_of_real y"
 apply (simp add: complex_divide_def)
 apply (case_tac "y=0", simp)
-apply (simp add: complex_of_real_mult [symmetric] complex_of_real_inverse 
-                 real_divide_def)
+apply (simp add: complex_of_real_mult complex_of_real_inverse 
+                 divide_inverse)
 done
 
 lemma complex_mod [simp]: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)"
@@ -407,7 +405,7 @@
 by (induct w, induct z, simp add: complex_cnj complex_add)
 
 lemma complex_cnj_diff: "cnj(w - z) = cnj(w) - cnj(z)"
-by (simp add: complex_diff_def complex_cnj_add complex_cnj_minus)
+by (simp add: diff_minus complex_cnj_add complex_cnj_minus)
 
 lemma complex_cnj_mult: "cnj(w * z) = cnj(w) * cnj(z)"
 by (induct w, induct z, simp add: complex_cnj complex_mult)
@@ -423,7 +421,7 @@
 
 lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii"
 apply (induct z)
-apply (simp add: complex_add complex_cnj complex_of_real_def complex_diff_def
+apply (simp add: complex_add complex_cnj complex_of_real_def diff_minus
                  complex_minus i_def complex_mult)
 done
 
@@ -561,7 +559,7 @@
 done
 
 lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)"
-by (simp add: complex_divide_def real_divide_def complex_mod_mult complex_mod_inverse)
+by (simp add: complex_divide_def divide_inverse complex_mod_mult complex_mod_inverse)
 
 
 subsection{*Exponentiation*}
@@ -639,24 +637,33 @@
 lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 & y = 1)"
 by (simp add: i_def)
 
+
+
 lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
-apply (induct z)
-apply (simp add: sgn_def complex_divide_def complex_of_real_inverse [symmetric])
-apply (simp add: complex_of_real_def complex_mult real_divide_def)
-done
+proof (induct z)
+  case (Complex x y)
+    have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))"
+      by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq)
+    thus "Re (sgn (Complex x y)) = Re (Complex x y) /cmod (Complex x y)"
+       by (simp add: sgn_def complex_of_real_def divide_inverse)
+qed
+
 
 lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
-apply (induct z)
-apply (simp add: sgn_def complex_divide_def complex_of_real_inverse [symmetric])
-apply (simp add: complex_of_real_def complex_mult real_divide_def)
-done
+proof (induct z)
+  case (Complex x y)
+    have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))"
+      by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq)
+    thus "Im (sgn (Complex x y)) = Im (Complex x y) /cmod (Complex x y)"
+       by (simp add: sgn_def complex_of_real_def divide_inverse)
+qed
 
 lemma complex_inverse_complex_split:
      "inverse(complex_of_real x + ii * complex_of_real y) =
       complex_of_real(x/(x ^ 2 + y ^ 2)) -
       ii * complex_of_real(y/(x ^ 2 + y ^ 2))"
 by (simp add: complex_of_real_def i_def complex_mult complex_add
-         complex_diff_def complex_minus complex_inverse real_divide_def)
+         diff_minus complex_minus complex_inverse divide_inverse)
 
 (*----------------------------------------------------------------------------*)
 (* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *)
@@ -738,7 +745,8 @@
 by (simp add: rcis_def)
 
 lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
-by (simp add: rcis_def cis_def complex_of_real_mult_Complex cos_add sin_add right_distrib right_diff_distrib)
+by (simp add: rcis_def cis_def cos_add sin_add right_distrib right_diff_distrib
+              complex_of_real_def)
 
 lemma cis_mult: "cis a * cis b = cis (a + b)"
 by (simp add: cis_rcis_eq rcis_mult)
@@ -774,7 +782,7 @@
 
 lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
 by (simp add: cis_def complex_inverse_complex_split complex_of_real_minus 
-              complex_diff_def)
+              diff_minus)
 
 lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
 by (simp add: divide_inverse rcis_def complex_of_real_inverse)
@@ -818,33 +826,31 @@
 
 instance complex :: number ..
 
-primrec (*the type constraint is essential!*)
-  number_of_Pls: "number_of bin.Pls = 0"
-  number_of_Min: "number_of bin.Min = - (1::complex)"
-  number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
-	                               (number_of w) + (number_of w)"
-
-declare number_of_Pls [simp del]
-        number_of_Min [simp del]
-        number_of_BIT [simp del]
+defs (overloaded)
+  complex_number_of_def: "(number_of w :: complex) == of_int (Rep_Bin w)"
+    --{*the type constraint is essential!*}
 
 instance complex :: number_ring
-proof
-  show "Numeral0 = (0::complex)" by (rule number_of_Pls)
-  show "-1 = - (1::complex)" by (rule number_of_Min)
-  fix w :: bin and x :: bool
-  show "(number_of (w BIT x) :: complex) =
-        (if x then 1 else 0) + number_of w + number_of w"
-    by (rule number_of_BIT)
+by (intro_classes, simp add: complex_number_of_def) 
+
+
+lemma complex_of_real_of_nat [simp]: "complex_of_real (of_nat n) = of_nat n"
+by (induct n, simp_all) 
+
+lemma complex_of_real_of_int [simp]: "complex_of_real (of_int z) = of_int z"
+proof (cases z)
+  case (1 n)
+    thus ?thesis by simp
+next
+  case (2 n)
+    thus ?thesis 
+      by (simp only: of_int_minus complex_of_real_minus, simp)
 qed
 
 
 text{*Collapse applications of @{term complex_of_real} to @{term number_of}*}
 lemma complex_number_of [simp]: "complex_of_real (number_of w) = number_of w"
-apply (induct w) 
-apply (simp_all only: number_of complex_of_real_add [symmetric] 
-                      complex_of_real_minus, simp_all) 
-done
+by (simp add: complex_number_of_def real_number_of_def) 
 
 text{*This theorem is necessary because theorems such as
    @{text iszero_number_of_0} only hold for ordered rings. They cannot
@@ -855,50 +861,6 @@
 by (simp only: complex_of_real_zero_iff complex_number_of [symmetric] 
                iszero_def)  
 
-
-(*These allow simplification of expressions involving mixed numbers.
-  Convert???
-Goalw [complex_number_of_def] 
-  "((number_of xa :: complex) + ii * number_of ya =  
-        number_of xb) =  
-   (((number_of xa :: complex) = number_of xb) &  
-    ((number_of ya :: complex) = 0))"
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff2,
-    complex_of_real_zero_iff]));
-qed "complex_number_of_eq_cancel_iff2";
-Addsimps [complex_number_of_eq_cancel_iff2];
-
-Goalw [complex_number_of_def] 
-  "((number_of xa :: complex) + number_of ya * ii = \
-\       number_of xb) = \
-\  (((number_of xa :: complex) = number_of xb) & \
-\   ((number_of ya :: complex) = 0))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff2a,
-    complex_of_real_zero_iff]));
-qed "complex_number_of_eq_cancel_iff2a";
-Addsimps [complex_number_of_eq_cancel_iff2a];
-
-Goalw [complex_number_of_def] 
-  "((number_of xa :: complex) + ii * number_of ya = \
-\    ii * number_of yb) = \
-\  (((number_of xa :: complex) = 0) & \
-\   ((number_of ya :: complex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff3,
-    complex_of_real_zero_iff]));
-qed "complex_number_of_eq_cancel_iff3";
-Addsimps [complex_number_of_eq_cancel_iff3];
-
-Goalw [complex_number_of_def] 
-  "((number_of xa :: complex) + number_of ya * ii= \
-\    ii * number_of yb) = \
-\  (((number_of xa :: complex) = 0) & \
-\   ((number_of ya :: complex) = number_of yb))";
-by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff3a,
-    complex_of_real_zero_iff]));
-qed "complex_number_of_eq_cancel_iff3a";
-Addsimps [complex_number_of_eq_cancel_iff3a];
-*)
-
 lemma complex_number_of_cnj [simp]: "cnj(number_of v :: complex) = number_of v"
 apply (subst complex_number_of [symmetric])
 apply (rule complex_cnj_complex_of_real)
@@ -957,7 +919,6 @@
 val complex_zero_def = thm"complex_zero_def";
 val complex_one_def = thm"complex_one_def";
 val complex_minus_def = thm"complex_minus_def";
-val complex_diff_def = thm"complex_diff_def";
 val complex_divide_def = thm"complex_divide_def";
 val complex_mult_def = thm"complex_mult_def";
 val complex_add_def = thm"complex_add_def";
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Complex/NSCA.thy
--- a/src/HOL/Complex/NSCA.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Complex/NSCA.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -508,7 +508,7 @@
 lemma capprox_SComplex_mult_cancel_zero:
      "[| a \<in> SComplex; a \<noteq> 0; a*x @c= 0 |] ==> x @c= 0"
 apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]])
-apply (auto dest: capprox_mult2 simp add: hcomplex_mult_assoc [symmetric])
+apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
 done
 
 lemma capprox_mult_SComplex1: "[| a \<in> SComplex; x @c= 0 |] ==> x*a @c= 0"
@@ -524,7 +524,7 @@
 lemma capprox_SComplex_mult_cancel:
      "[| a \<in> SComplex; a \<noteq> 0; a* w @c= a*z |] ==> w @c= z"
 apply (drule SComplex_inverse [THEN SComplex_subset_CFinite [THEN subsetD]])
-apply (auto dest: capprox_mult2 simp add: hcomplex_mult_assoc [symmetric])
+apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
 done
 
 lemma capprox_SComplex_mult_cancel_iff1 [simp]:
@@ -618,7 +618,7 @@
 lemma CInfinitesimal_ratio:
      "[| y \<noteq> 0;  y \<in> CInfinitesimal;  x/y \<in> CFinite |] ==> x \<in> CInfinitesimal"
 apply (drule CInfinitesimal_CFinite_mult2, assumption)
-apply (simp add: divide_inverse hcomplex_mult_assoc)
+apply (simp add: divide_inverse mult_assoc)
 done
 
 lemma SComplex_capprox_iff:
@@ -901,10 +901,11 @@
 apply (drule CFinite_inverse2)+
 apply (drule capprox_mult2, assumption, auto)
 apply (drule_tac c = "inverse x" in capprox_mult1, assumption)
-apply (auto intro: capprox_sym simp add: hcomplex_mult_assoc)
+apply (auto intro: capprox_sym simp add: mult_assoc)
 done
 
-lemmas hcomplex_of_complex_capprox_inverse =  hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN [2] capprox_inverse]
+lemmas hcomplex_of_complex_capprox_inverse =
+  hcomplex_of_complex_CFinite_diff_CInfinitesimal [THEN [2] capprox_inverse]
 
 lemma inverse_add_CInfinitesimal_capprox:
      "[| x \<in> CFinite - CInfinitesimal;  
@@ -935,7 +936,7 @@
 apply safe
 apply (frule CFinite_inverse, assumption)
 apply (drule not_CInfinitesimal_not_zero)
-apply (auto dest: capprox_mult2 simp add: hcomplex_mult_assoc [symmetric])
+apply (auto dest: capprox_mult2 simp add: mult_assoc [symmetric])
 done
 
 lemma capprox_CFinite_mult_cancel_iff1:
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -475,51 +475,48 @@
 apply (simp add: hcomplex_of_hypreal)
 done
 
-lemma hcomplex_of_hypreal_minus:
-     "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
-apply (cases x)
-apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus)
-done
-
-lemma hcomplex_of_hypreal_inverse:
-     "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
-apply (cases x)
-apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse)
-done
-
-lemma hcomplex_of_hypreal_add:
-     "hcomplex_of_hypreal x + hcomplex_of_hypreal y =
-      hcomplex_of_hypreal (x + y)"
-apply (cases x, cases y)
-apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add)
-done
-
-lemma hcomplex_of_hypreal_diff:
-     "hcomplex_of_hypreal x - hcomplex_of_hypreal y =
-      hcomplex_of_hypreal (x - y)"
-by (simp add: hcomplex_diff_def hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def)
-
-lemma hcomplex_of_hypreal_mult:
-     "hcomplex_of_hypreal x * hcomplex_of_hypreal y =
-      hcomplex_of_hypreal (x * y)"
-apply (cases x, cases y)
-apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult complex_of_real_mult)
-done
-
-lemma hcomplex_of_hypreal_divide:
-  "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)"
-apply (simp add: hcomplex_divide_def)
-apply (case_tac "y=0", simp)
-apply (auto simp add: hcomplex_of_hypreal_mult hcomplex_of_hypreal_inverse [symmetric])
-apply (simp add: hypreal_divide_def)
-done
-
 lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1"
 by (simp add: hcomplex_one_def hcomplex_of_hypreal hypreal_one_num)
 
 lemma hcomplex_of_hypreal_zero [simp]: "hcomplex_of_hypreal 0 = 0"
 by (simp add: hcomplex_zero_def hypreal_zero_def hcomplex_of_hypreal)
 
+lemma hcomplex_of_hypreal_minus [simp]:
+     "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
+apply (cases x)
+apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus)
+done
+
+lemma hcomplex_of_hypreal_inverse [simp]:
+     "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
+apply (cases x)
+apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse)
+done
+
+lemma hcomplex_of_hypreal_add [simp]:
+  "hcomplex_of_hypreal (x + y) = hcomplex_of_hypreal x + hcomplex_of_hypreal y"
+apply (cases x, cases y)
+apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add)
+done
+
+lemma hcomplex_of_hypreal_diff [simp]:
+     "hcomplex_of_hypreal (x - y) =
+      hcomplex_of_hypreal x - hcomplex_of_hypreal y "
+by (simp add: hcomplex_diff_def hypreal_diff_def)
+
+lemma hcomplex_of_hypreal_mult [simp]:
+  "hcomplex_of_hypreal (x * y) = hcomplex_of_hypreal x * hcomplex_of_hypreal y"
+apply (cases x, cases y)
+apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult)
+done
+
+lemma hcomplex_of_hypreal_divide [simp]:
+  "hcomplex_of_hypreal(x/y) = hcomplex_of_hypreal x / hcomplex_of_hypreal y"
+apply (simp add: hcomplex_divide_def)
+apply (case_tac "y=0", simp)
+apply (simp add: hypreal_divide_def)
+done
+
 lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z"
 apply (cases z)
 apply (auto simp add: hcomplex_of_hypreal hRe)
@@ -599,7 +596,7 @@
 
 lemma HComplex_add [simp]:
      "HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)"
-by (simp add: HComplex_def hcomplex_of_hypreal_add [symmetric] add_ac right_distrib) 
+by (simp add: HComplex_def add_ac right_distrib) 
 
 lemma HComplex_minus [simp]: "- HComplex x y = HComplex (-x) (-y)"
 by (simp add: HComplex_def hcomplex_of_hypreal_minus) 
@@ -611,7 +608,6 @@
 lemma HComplex_mult [simp]:
   "HComplex x1 y1 * HComplex x2 y2 = HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
 by (simp add: HComplex_def diff_minus hcomplex_of_hypreal_minus 
-       hcomplex_of_hypreal_add [symmetric] hcomplex_of_hypreal_mult [symmetric]
        add_ac mult_ac right_distrib)
 
 (*HComplex_inverse is proved below*)
@@ -1000,7 +996,9 @@
       hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
       iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
 apply (cases x, cases y)
-apply (simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide hcomplex_diff complex_inverse_complex_split numeral_2_eq_2)
+apply (simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def
+         starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide
+         hcomplex_diff numeral_2_eq_2 complex_of_real_def i_def)
 apply (simp add: diff_minus) 
 done
 
@@ -1163,8 +1161,7 @@
   "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
 apply (simp add: hrcis_def, cases r1, cases r2, cases a, cases b)
 apply (simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
-                      hcomplex_mult cis_mult [symmetric]
-                      complex_of_real_mult [symmetric])
+                      hcomplex_mult cis_mult [symmetric])
 done
 
 lemma hcis_mult: "hcis a * hcis b = hcis (a + b)"
@@ -1304,17 +1301,28 @@
 
 lemma hcomplex_of_complex_inverse [simp]:
      "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)"
-apply (case_tac "r=0")
-apply (simp add: hcomplex_of_complex_zero)
-apply (rule_tac c1 = "hcomplex_of_complex r"
-       in hcomplex_mult_left_cancel [THEN iffD1])
-apply (force simp add: hcomplex_of_complex_zero_iff)
-apply (subst hcomplex_of_complex_mult [symmetric])
-apply (simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff)
-done
+proof cases
+  assume "r=0" thus ?thesis by simp
+next
+  assume nz: "r\<noteq>0" 
+  show ?thesis
+  proof (rule hcomplex_mult_left_cancel [THEN iffD1]) 
+    show "hcomplex_of_complex r \<noteq> 0"
+      by (simp add: nz) 
+  next
+    have "hcomplex_of_complex r * hcomplex_of_complex (inverse r) =
+          hcomplex_of_complex (r * inverse r)"
+      by simp
+    also have "... = hcomplex_of_complex r * inverse (hcomplex_of_complex r)" 
+      by (simp add: nz)
+    finally show "hcomplex_of_complex r * hcomplex_of_complex (inverse r) =
+                  hcomplex_of_complex r * inverse (hcomplex_of_complex r)" .
+  qed
+qed
 
 lemma hcomplex_of_complex_divide [simp]:
-     "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2"
+     "hcomplex_of_complex (z1 / z2) = 
+      hcomplex_of_complex z1 / hcomplex_of_complex z2"
 by (simp add: hcomplex_divide_def complex_divide_def)
 
 lemma hRe_hcomplex_of_complex:
@@ -1334,38 +1342,38 @@
 
 instance hcomplex :: number ..
 
-primrec (*the type constraint is essential!*)
-  number_of_Pls: "number_of bin.Pls = 0"
-  number_of_Min: "number_of bin.Min = - (1::hcomplex)"
-  number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
-	                               (number_of w) + (number_of w)"
-
-declare number_of_Pls [simp del]
-        number_of_Min [simp del]
-        number_of_BIT [simp del]
+defs (overloaded)
+  hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int (Rep_Bin w)"
+    --{*the type constraint is essential!*}
 
 instance hcomplex :: number_ring
-proof
-  show "Numeral0 = (0::hcomplex)" by (rule number_of_Pls)
-  show "-1 = - (1::hcomplex)" by (rule number_of_Min)
-  fix w :: bin and x :: bool
-  show "(number_of (w BIT x) :: hcomplex) =
-        (if x then 1 else 0) + number_of w + number_of w"
-    by (rule number_of_BIT)
+by (intro_classes, simp add: hcomplex_number_of_def) 
+
+
+lemma hcomplex_of_complex_of_nat [simp]:
+     "hcomplex_of_complex (of_nat n) = of_nat n"
+by (induct n, simp_all) 
+
+lemma hcomplex_of_complex_of_int [simp]:
+     "hcomplex_of_complex (of_int z) = of_int z"
+proof (cases z)
+  case (1 n)
+    thus ?thesis by simp
+next
+  case (2 n)
+    thus ?thesis 
+      by (simp only: of_int_minus hcomplex_of_complex_minus, simp)
 qed
 
 
 text{*Collapse applications of @{term hcomplex_of_complex} to @{term number_of}*}
 lemma hcomplex_number_of [simp]:
      "hcomplex_of_complex (number_of w) = number_of w"
-apply (induct w) 
-apply (simp_all only: number_of hcomplex_of_complex_add 
-                      hcomplex_of_complex_minus, simp_all) 
-done
+by (simp add: hcomplex_number_of_def complex_number_of_def) 
 
 lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: 
      "hcomplex_of_hypreal (hypreal_of_real x) =  
-      hcomplex_of_complex(complex_of_real x)"
+      hcomplex_of_complex (complex_of_real x)"
 by (simp add: hypreal_of_real_def hcomplex_of_hypreal hcomplex_of_complex_def 
               complex_of_real_def)
 
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -9,6 +9,25 @@
 
 theory HTranscendental = Transcendental + Integration:
 
+text{*really belongs in Transcendental*}
+lemma sqrt_divide_self_eq:
+  assumes nneg: "0 \<le> x"
+  shows "sqrt x / x = inverse (sqrt x)"
+proof cases
+  assume "x=0" thus ?thesis by simp
+next
+  assume nz: "x\<noteq>0" 
+  hence pos: "0<x" using nneg by arith
+  show ?thesis
+  proof (rule right_inverse_eq [THEN iffD1, THEN sym]) 
+    show "sqrt x / x \<noteq> 0" by (simp add: divide_inverse nneg nz) 
+    show "inverse (sqrt x) / (sqrt x / x) = 1"
+      by (simp add: divide_inverse mult_assoc [symmetric] 
+                  power2_eq_square [symmetric] real_inv_sqrt_pow2 pos nz) 
+  qed
+qed
+
+
 constdefs
 
   exphr :: "real => hypreal"
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Hyperreal/HyperArith.thy
--- a/src/HOL/Hyperreal/HyperArith.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Hyperreal/HyperArith.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -14,32 +14,18 @@
 
 instance hypreal :: number ..
 
-primrec (*the type constraint is essential!*)
-  number_of_Pls: "number_of bin.Pls = 0"
-  number_of_Min: "number_of bin.Min = - (1::hypreal)"
-  number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
-	                               (number_of w) + (number_of w)"
-
-declare number_of_Pls [simp del]
-        number_of_Min [simp del]
-        number_of_BIT [simp del]
+defs (overloaded)
+  hypreal_number_of_def: "(number_of w :: hypreal) == of_int (Rep_Bin w)"
+    --{*the type constraint is essential!*}
 
 instance hypreal :: number_ring
-proof
-  show "Numeral0 = (0::hypreal)" by (rule number_of_Pls)
-  show "-1 = - (1::hypreal)" by (rule number_of_Min)
-  fix w :: bin and x :: bool
-  show "(number_of (w BIT x) :: hypreal) =
-        (if x then 1 else 0) + number_of w + number_of w"
-    by (rule number_of_BIT)
-qed
+by (intro_classes, simp add: hypreal_number_of_def) 
 
 
 text{*Collapse applications of @{term hypreal_of_real} to @{term number_of}*}
 lemma hypreal_number_of [simp]: "hypreal_of_real (number_of w) = number_of w"
-apply (induct w) 
-apply (simp_all only: number_of hypreal_of_real_add hypreal_of_real_minus, simp_all) 
-done
+by (simp add: hypreal_number_of_def real_number_of_def) 
+
 
 
 use "hypreal_arith.ML"
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -526,6 +526,14 @@
      "hypreal_of_real (w + z) = hypreal_of_real w + hypreal_of_real z"
 by (simp add: hypreal_of_real_def, simp add: hypreal_add left_distrib)
 
+lemma hypreal_of_real_minus [simp]:
+     "hypreal_of_real (-r) = - hypreal_of_real  r"
+by (auto simp add: hypreal_of_real_def hypreal_minus)
+
+lemma hypreal_of_real_diff [simp]: 
+     "hypreal_of_real (w - z) = hypreal_of_real w - hypreal_of_real z"
+by (simp add: diff_minus) 
+
 lemma hypreal_of_real_mult [simp]: 
      "hypreal_of_real (w * z) = hypreal_of_real w * hypreal_of_real z"
 by (simp add: hypreal_of_real_def, simp add: hypreal_mult right_distrib)
@@ -572,10 +580,6 @@
 declare hypreal_of_real_le_iff   [of _ 1, simplified, simp]
 declare hypreal_of_real_eq_iff   [of _ 1, simplified, simp]
 
-lemma hypreal_of_real_minus [simp]:
-     "hypreal_of_real (-r) = - hypreal_of_real  r"
-by (auto simp add: hypreal_of_real_def hypreal_minus)
-
 lemma hypreal_of_real_inverse [simp]:
      "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)"
 apply (case_tac "r=0", simp)
@@ -587,6 +591,19 @@
      "hypreal_of_real (w / z) = hypreal_of_real w / hypreal_of_real z"
 by (simp add: hypreal_divide_def real_divide_def)
 
+lemma hypreal_of_real_of_nat [simp]: "hypreal_of_real (of_nat n) = of_nat n"
+by (induct n, simp_all) 
+
+lemma hypreal_of_real_of_int [simp]:  "hypreal_of_real (of_int z) = of_int z"
+proof (cases z)
+  case (1 n)
+    thus ?thesis  by simp
+next
+  case (2 n)
+    thus ?thesis
+      by (simp only: of_int_minus hypreal_of_real_minus, simp)
+qed
+
 
 subsection{*Misc Others*}
 
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -8,42 +8,42 @@
 Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim + 
 
 constdefs
-    root :: [nat,real] => real
+    root :: "[nat,real] => real"
     "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
 
-    sqrt :: real => real
+    sqrt :: "real => real"
     "sqrt x == root 2 x"
 
-    exp :: real => real
+    exp :: "real => real"
     "exp x == suminf(%n. inverse(real (fact n)) * (x ^ n))"
 
-    sin :: real => real
+    sin :: "real => real"
     "sin x == suminf(%n. (if even(n) then 0 else
              ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
  
-    diffs :: (nat => real) => nat => real
+    diffs :: "(nat => real) => nat => real"
     "diffs c == (%n. real (Suc n) * c(Suc n))"
 
-    cos :: real => real
+    cos :: "real => real"
     "cos x == suminf(%n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n)) 
                           else 0) * x ^ n)"
   
-    ln :: real => real
+    ln :: "real => real"
     "ln x == (@u. exp u = x)"
 
-    pi :: real
+    pi :: "real"
     "pi == 2 * (@x. 0 <= (x::real) & x <= 2 & cos x = 0)"
 
-    tan :: real => real
+    tan :: "real => real"
     "tan x == (sin x)/(cos x)"
 
-    arcsin :: real => real
+    arcsin :: "real => real"
     "arcsin y == (@x. -(pi/2) <= x & x <= pi/2 & sin x = y)"
 
-    arcos :: real => real
+    arcos :: "real => real"
     "arcos y == (@x. 0 <= x & x <= pi & cos x = y)"
      
-    arctan :: real => real
+    arctan :: "real => real"
     "arctan y == (@x. -(pi/2) < x & x < pi/2 & tan x = y)"
   
 end 
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Import/HOL/HOL4Prob.thy
--- a/src/HOL/Import/HOL/HOL4Prob.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Prob.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -27,7 +27,7 @@
                       ((op *::nat => nat => nat)
                         ((number_of::bin => nat)
                           ((op BIT::bin => bool => bin)
-                            ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                            ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                               (True::bool))
                             (False::bool)))
                         q)
@@ -40,14 +40,14 @@
                     ((op div::nat => nat => nat) n
                       ((number_of::bin => nat)
                         ((op BIT::bin => bool => bin)
-                          ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                          ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                             (True::bool))
                           (False::bool)))))
                   ((op =::nat => nat => bool) r
                     ((op mod::nat => nat => nat) n
                       ((number_of::bin => nat)
                         ((op BIT::bin => bool => bin)
-                          ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                          ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                             (True::bool))
                           (False::bool)))))))))"
   by (import prob_extra DIV_TWO_UNIQUE)
@@ -76,13 +76,13 @@
              ((op div::nat => nat => nat) m
                ((number_of::bin => nat)
                  ((op BIT::bin => bool => bin)
-                   ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                   ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                      (True::bool))
                    (False::bool))))
              ((op div::nat => nat => nat) n
                ((number_of::bin => nat)
                  ((op BIT::bin => bool => bin)
-                   ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                   ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                      (True::bool))
                    (False::bool)))))
            ((op <::nat => nat => bool) m n)))"
@@ -98,13 +98,13 @@
                ((op div::nat => nat => nat) m
                  ((number_of::bin => nat)
                    ((op BIT::bin => bool => bin)
-                     ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                     ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                        (True::bool))
                      (False::bool))))
                ((op div::nat => nat => nat) n
                  ((number_of::bin => nat)
                    ((op BIT::bin => bool => bin)
-                     ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                     ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                        (True::bool))
                      (False::bool)))))
              ((op <::nat => nat => bool) m n))))"
@@ -204,7 +204,7 @@
                ((op /::real => real => real) (1::real)
                  ((number_of::bin => real)
                    ((op BIT::bin => bool => bin)
-                     ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                     ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                        (True::bool))
                      (False::bool))))
                n)
@@ -212,7 +212,7 @@
                ((op /::real => real => real) (1::real)
                  ((number_of::bin => real)
                    ((op BIT::bin => bool => bin)
-                     ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                     ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                        (True::bool))
                      (False::bool))))
                m))))"
@@ -2528,7 +2528,7 @@
                ((op /::real => real => real) (1::real)
                  ((number_of::bin => real)
                    ((op BIT::bin => bool => bin)
-                     ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                     ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                        (True::bool))
                      (False::bool))))
                ((prob::((nat => bool) => bool) => real) p)))))"
@@ -3156,7 +3156,7 @@
                           ((op /::real => real => real) (1::real)
                             ((number_of::bin => real)
                               ((op BIT::bin => bool => bin)
-                                ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                                ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                                   (True::bool))
                                 (False::bool))))
                           ((size::bool list => nat) x))
@@ -3382,7 +3382,7 @@
                (P ((op div::nat => nat => nat) ((Suc::nat => nat) v)
                     ((number_of::bin => nat)
                       ((op BIT::bin => bool => bin)
-                        ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                        ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                           (True::bool))
                         (False::bool)))))
                (P ((Suc::nat => nat) v)))))
@@ -3436,7 +3436,7 @@
                     (P ((op div::nat => nat => nat) ((Suc::nat => nat) v2)
                          ((number_of::bin => nat)
                            ((op BIT::bin => bool => bin)
-                             ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                             ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                                (True::bool))
                              (False::bool))))
                       s)
@@ -3716,13 +3716,13 @@
         ((op ^::nat => nat => nat)
           ((number_of::bin => nat)
             ((op BIT::bin => bool => bin)
-              ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+              ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
               (False::bool)))
           ((unif_bound::nat => nat) n))
         ((op *::nat => nat => nat)
           ((number_of::bin => nat)
             ((op BIT::bin => bool => bin)
-              ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+              ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
               (False::bool)))
           n)))"
   by (import prob_uniform UNIF_BOUND_UPPER)
@@ -3771,7 +3771,7 @@
              ((op ^::nat => nat => nat)
                ((number_of::bin => nat)
                  ((op BIT::bin => bool => bin)
-                   ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                   ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                      (True::bool))
                    (False::bool)))
                ((unif_bound::nat => nat) n)))
@@ -3788,7 +3788,7 @@
                  ((op /::real => real => real) (1::real)
                    ((number_of::bin => real)
                      ((op BIT::bin => bool => bin)
-                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                          (True::bool))
                        (False::bool))))
                  ((unif_bound::nat => nat) n))))))"
@@ -3907,7 +3907,7 @@
                          ((op /::real => real => real) (1::real)
                            ((number_of::bin => real)
                              ((op BIT::bin => bool => bin)
-                               ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                               ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                                  (True::bool))
                                (False::bool))))
                          t))))))"
@@ -3938,7 +3938,7 @@
                     ((op /::real => real => real) (1::real)
                       ((number_of::bin => real)
                         ((op BIT::bin => bool => bin)
-                          ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                          ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                             (True::bool))
                           (False::bool))))
                     t)))))"
@@ -3969,7 +3969,7 @@
                     ((op /::real => real => real) (1::real)
                       ((number_of::bin => real)
                         ((op BIT::bin => bool => bin)
-                          ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                          ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                             (True::bool))
                           (False::bool))))
                     t)))))"
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Import/HOL/HOL4Real.thy
--- a/src/HOL/Import/HOL/HOL4Real.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Real.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -1916,13 +1916,13 @@
                ((op *::nat => nat => nat)
                  ((number_of::bin => nat)
                    ((op BIT::bin => bool => bin)
-                     ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                     ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                        (True::bool))
                      (False::bool)))
                  n)
                ((number_of::bin => nat)
                  ((op BIT::bin => bool => bin)
-                   ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                   ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                      (True::bool))
                    (False::bool))))
              f)
@@ -1958,7 +1958,7 @@
                              ((number_of::bin => nat)
                                ((op BIT::bin => bool => bin)
                                  ((op BIT::bin => bool => bin)
-                                   (bin.Pls::bin) (True::bool))
+                                   (Numeral.Pls::bin) (True::bool))
                                  (False::bool)))
                              d)))
                       (f ((op +::nat => nat => nat) n
@@ -1967,7 +1967,7 @@
                                ((number_of::bin => nat)
                                  ((op BIT::bin => bool => bin)
                                    ((op BIT::bin => bool => bin)
-                                     (bin.Pls::bin) (True::bool))
+                                     (Numeral.Pls::bin) (True::bool))
                                    (False::bool)))
                                d)
                              (1::nat))))))))
@@ -2825,7 +2825,7 @@
           ((op ^::real => nat => real) ((inverse::real => real) x)
             ((number_of::bin => nat)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))))
         x))"
   by (import lim DIFF_XM1)
@@ -2848,7 +2848,7 @@
                       ((op ^::real => nat => real) (f x)
                         ((number_of::bin => nat)
                           ((op BIT::bin => bool => bin)
-                            ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                            ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                               (True::bool))
                             (False::bool))))))
                   x))))"
@@ -2886,7 +2886,7 @@
                                 ((number_of::bin => nat)
                                   ((op BIT::bin => bool => bin)
                                     ((op BIT::bin => bool => bin)
-(bin.Pls::bin) (True::bool))
+(Numeral.Pls::bin) (True::bool))
                                     (False::bool)))))
                             x))))))"
   by (import lim DIFF_DIV)
@@ -3869,7 +3869,7 @@
   ((op -::nat => nat => nat) n
     ((number_of::bin => nat)
       ((op BIT::bin => bool => bin)
-        ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+        ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
         (False::bool))))
   p)
 q)))))))))))"
@@ -3917,7 +3917,7 @@
                                  ((number_of::bin => nat)
                                    ((op BIT::bin => bool => bin)
                                      ((op BIT::bin => bool => bin)
- (bin.Pls::bin) (True::bool))
+ (Numeral.Pls::bin) (True::bool))
                                      (False::bool)))))
                              ((abs::real => real) h)))))))))"
   by (import powser TERMDIFF_LEMMA3)
@@ -4112,7 +4112,7 @@
          ((op ^::real => nat => real) (f x)
            ((number_of::bin => nat)
              ((op BIT::bin => bool => bin)
-               ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+               ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                (False::bool))))))
      x))
  ((op &::bool => bool => bool)
@@ -4133,7 +4133,7 @@
          ((op ^::real => nat => real) (g x)
            ((number_of::bin => nat)
              ((op BIT::bin => bool => bin)
-               ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+               ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                (False::bool)))))
        x))
    ((op &::bool => bool => bool)
@@ -4652,7 +4652,7 @@
         ((op ^::real => nat => real) ((sqrt::real => real) x)
           ((number_of::bin => nat)
             ((op BIT::bin => bool => bin)
-              ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+              ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
               (False::bool))))
         x))"
   by (import transc SQRT_POW_2)
@@ -4664,7 +4664,7 @@
      ((op ^::real => nat => real) x
        ((number_of::bin => nat)
          ((op BIT::bin => bool => bin)
-           ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+           ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
            (False::bool)))))
    x)"
   by (import transc POW_2_SQRT)
@@ -4682,7 +4682,7 @@
                  ((op ^::real => nat => real) xa
                    ((number_of::bin => nat)
                      ((op BIT::bin => bool => bin)
-                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                          (True::bool))
                        (False::bool))))
                  x)))
@@ -4746,18 +4746,18 @@
           ((op ^::real => nat => real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))
             n))
         ((op ^::real => nat => real)
           ((number_of::bin => real)
             ((op BIT::bin => bool => bin)
-              ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+              ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
               (False::bool)))
           ((op div::nat => nat => nat) n
             ((number_of::bin => nat)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))))))"
   by (import transc SQRT_EVEN_POW2)
 
@@ -4780,7 +4780,7 @@
                ((op ^::real => nat => real) x
                  ((number_of::bin => nat)
                    ((op BIT::bin => bool => bin)
-                     ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                     ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                        (True::bool))
                      (False::bool))))
                y)
@@ -4848,7 +4848,7 @@
         ((op <::real => real => bool) x
           ((number_of::bin => real)
             ((op BIT::bin => bool => bin)
-              ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+              ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
               (False::bool)))))
       ((op <::real => real => bool) (0::real) ((sin::real => real) x)))"
   by (import transc SIN_POS)
@@ -4923,7 +4923,7 @@
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op <::real => real => bool) (0::real) ((sin::real => real) x)))"
   by (import transc SIN_POS_PI2)
@@ -4937,7 +4937,7 @@
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op <::real => real => bool) (0::real) ((cos::real => real) x)))"
   by (import transc COS_POS_PI2)
@@ -4951,14 +4951,14 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           x)
         ((op <::real => real => bool) x
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op <::real => real => bool) (0::real) ((cos::real => real) x)))"
   by (import transc COS_POS_PI)
@@ -4981,7 +4981,7 @@
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op <=::real => real => bool) (0::real) ((cos::real => real) x)))"
   by (import transc COS_POS_PI2_LE)
@@ -4995,14 +4995,14 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           x)
         ((op <=::real => real => bool) x
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op <=::real => real => bool) (0::real) ((cos::real => real) x)))"
   by (import transc COS_POS_PI_LE)
@@ -5016,7 +5016,7 @@
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op <=::real => real => bool) (0::real) ((sin::real => real) x)))"
   by (import transc SIN_POS_PI2_LE)
@@ -5059,7 +5059,7 @@
                  ((op /::real => real => real) (pi::real)
                    ((number_of::bin => real)
                      ((op BIT::bin => bool => bin)
-                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                          (True::bool))
                        (False::bool)))))
                x)
@@ -5068,7 +5068,7 @@
                  ((op /::real => real => real) (pi::real)
                    ((number_of::bin => real)
                      ((op BIT::bin => bool => bin)
-                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                          (True::bool))
                        (False::bool)))))
                ((op =::real => real => bool) ((sin::real => real) x) y)))))"
@@ -5089,7 +5089,7 @@
                  ((op /::real => real => real) (pi::real)
                    ((number_of::bin => real)
                      ((op BIT::bin => bool => bin)
-                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                          (True::bool))
                        (False::bool)))))))))"
   by (import transc COS_ZERO_LEMMA)
@@ -5108,7 +5108,7 @@
                  ((op /::real => real => real) (pi::real)
                    ((number_of::bin => real)
                      ((op BIT::bin => bool => bin)
-                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                          (True::bool))
                        (False::bool)))))))))"
   by (import transc SIN_ZERO_LEMMA)
@@ -5186,7 +5186,7 @@
               ((op *::real => real => real)
                 ((number_of::bin => real)
                   ((op BIT::bin => bool => bin)
-                    ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                    ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                       (True::bool))
                     (False::bool)))
                 x))
@@ -5196,21 +5196,21 @@
           ((op *::real => real => real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))
             x))
         ((op /::real => real => real)
           ((op *::real => real => real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))
             ((tan::real => real) x))
           ((op -::real => real => real) (1::real)
             ((op ^::real => nat => real) ((tan::real => real) x)
               ((number_of::bin => nat)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool))))))))"
   by (import transc TAN_DOUBLE)
 
@@ -5223,7 +5223,7 @@
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op <::real => real => bool) (0::real) ((tan::real => real) x)))"
   by (import transc TAN_POS_PI2)
@@ -5238,7 +5238,7 @@
           ((op ^::real => nat => real) ((cos::real => real) x)
             ((number_of::bin => nat)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))))
         x))"
   by (import transc DIFF_TAN)
@@ -5256,7 +5256,7 @@
                  ((op /::real => real => real) (pi::real)
                    ((number_of::bin => real)
                      ((op BIT::bin => bool => bin)
-                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                          (True::bool))
                        (False::bool)))))
                ((op <::real => real => bool) y ((tan::real => real) x))))))"
@@ -5275,7 +5275,7 @@
                  ((op /::real => real => real) (pi::real)
                    ((number_of::bin => real)
                      ((op BIT::bin => bool => bin)
-                       ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                       ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                          (True::bool))
                        (False::bool)))))
                ((op =::real => real => bool) ((tan::real => real) x) y)))))"
@@ -5317,7 +5317,7 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           ((asn::real => real) y))
         ((op &::bool => bool => bool)
@@ -5325,7 +5325,7 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           ((op =::real => real => bool)
             ((sin::real => real) ((asn::real => real) y)) y))))"
@@ -5353,14 +5353,14 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           ((asn::real => real) y))
         ((op <=::real => real => bool) ((asn::real => real) y)
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))))))"
   by (import transc ASN_BOUNDS)
 
@@ -5376,14 +5376,14 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           ((asn::real => real) y))
         ((op <::real => real => bool) ((asn::real => real) y)
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))))))"
   by (import transc ASN_BOUNDS_LT)
 
@@ -5396,14 +5396,14 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           x)
         ((op <=::real => real => bool) x
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op =::real => real => bool)
         ((asn::real => real) ((sin::real => real) x)) x))"
@@ -5483,14 +5483,14 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           x)
         ((op <::real => real => bool) x
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op =::real => real => bool)
         ((atn::real => real) ((tan::real => real) x)) x))"
@@ -5506,13 +5506,13 @@
           ((op ^::real => nat => real) ((tan::real => real) x)
             ((number_of::bin => nat)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool)))))
         ((op ^::real => nat => real)
           ((inverse::real => real) ((cos::real => real) x))
           ((number_of::bin => nat)
             ((op BIT::bin => bool => bin)
-              ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+              ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
               (False::bool))))))"
   by (import transc TAN_SEC)
 
@@ -5528,7 +5528,7 @@
             ((op ^::real => nat => real) ((cos::real => real) x)
               ((number_of::bin => nat)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool))))))))"
   by (import transc SIN_COS_SQ)
 
@@ -5541,14 +5541,14 @@
             ((op /::real => real => real) (pi::real)
               ((number_of::bin => real)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool)))))
           x)
         ((op <=::real => real => bool) x
           ((op /::real => real => real) (pi::real)
             ((number_of::bin => real)
               ((op BIT::bin => bool => bin)
-                ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                 (False::bool))))))
       ((op =::real => real => bool) ((cos::real => real) x)
         ((sqrt::real => real)
@@ -5556,7 +5556,7 @@
             ((op ^::real => nat => real) ((sin::real => real) x)
               ((number_of::bin => nat)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool))))))))"
   by (import transc COS_SIN_SQ)
 
@@ -5595,7 +5595,7 @@
             ((op ^::real => nat => real) ((sin::real => real) x)
               ((number_of::bin => nat)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool))))))))"
   by (import transc COS_SIN_SQRT)
 
@@ -5609,7 +5609,7 @@
             ((op ^::real => nat => real) ((cos::real => real) x)
               ((number_of::bin => nat)
                 ((op BIT::bin => bool => bin)
-                  ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+                  ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
                   (False::bool))))))))"
   by (import transc SIN_COS_SQRT)
 
@@ -5646,7 +5646,7 @@
               ((op ^::real => nat => real) x
                 ((number_of::bin => nat)
                   ((op BIT::bin => bool => bin)
-                    ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                    ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                       (True::bool))
                     (False::bool)))))))
         x))"
@@ -5679,7 +5679,7 @@
                 ((op ^::real => nat => real) x
                   ((number_of::bin => nat)
                     ((op BIT::bin => bool => bin)
-                      ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                      ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                         (True::bool))
                       (False::bool))))))))
         x))"
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Import/HOL/HOL4Vec.thy
--- a/src/HOL/Import/HOL/HOL4Vec.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Vec.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -1103,7 +1103,7 @@
       ((op <::nat => nat => bool) x
         ((number_of::bin => nat)
           ((op BIT::bin => bool => bin)
-            ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+            ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
             (False::bool))))
       ((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
         x))"
@@ -1298,7 +1298,7 @@
                          ((op ^::nat => nat => nat)
                            ((number_of::bin => nat)
                              ((op BIT::bin => bool => bin)
-                               ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                               ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                                  (True::bool))
                                (False::bool)))
                            k)))))))"
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Integ/Bin.thy
--- a/src/HOL/Integ/Bin.thy	Wed Jun 30 14:04:58 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,351 +0,0 @@
-(*  Title:	HOL/Integ/Bin.thy
-    ID:         $Id$
-    Authors:	Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright	1994  University of Cambridge
-
-Ported from ZF to HOL by David Spelt.
-*)
-
-header{*Arithmetic on Binary Integers*}
-
-theory Bin = IntDef + Numeral:
-
-axclass number_ring \<subseteq> number, comm_ring_1
-  number_of_Pls: "number_of bin.Pls = 0"
-  number_of_Min: "number_of bin.Min = - 1"
-  number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
-	                               (number_of w) + (number_of w)"
-subsection{*Converting Numerals to Rings: @{term number_of}*}
-
-lemmas number_of = number_of_Pls number_of_Min number_of_BIT
-
-lemma number_of_NCons [simp]:
-     "number_of(NCons w b) = (number_of(w BIT b)::'a::number_ring)"
-by (induct_tac "w", simp_all add: number_of)
-
-lemma number_of_succ: "number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)"
-apply (induct_tac "w")
-apply (simp_all add: number_of add_ac)
-done
-
-lemma number_of_pred: "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
-apply (induct_tac "w")
-apply (simp_all add: number_of add_assoc [symmetric]) 
-done
-
-lemma number_of_minus: "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)"
-apply (induct_tac "w")
-apply (simp_all del: bin_pred_Pls bin_pred_Min bin_pred_BIT 
-            add: number_of number_of_succ number_of_pred add_assoc)
-done
-
-text{*This proof is complicated by the mutual recursion*}
-lemma number_of_add [rule_format]:
-     "\<forall>w. number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)"
-apply (induct_tac "v")
-apply (simp add: number_of)
-apply (simp add: number_of number_of_pred)
-apply (rule allI)
-apply (induct_tac "w")
-apply (simp_all add: number_of bin_add_BIT_BIT number_of_succ number_of_pred add_ac)
-done
-
-lemma number_of_mult:
-     "number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)"
-apply (induct_tac "v", simp add: number_of) 
-apply (simp add: number_of number_of_minus) 
-apply (simp add: number_of number_of_add left_distrib add_ac)
-done
-
-text{*The correctness of shifting.  But it doesn't seem to give a measurable
-  speed-up.*}
-lemma double_number_of_BIT:
-     "(1+1) * number_of w = (number_of (w BIT False) ::'a::number_ring)"
-apply (induct_tac "w")
-apply (simp_all add: number_of number_of_add left_distrib add_ac)
-done
-
-
-text{*Converting numerals 0 and 1 to their abstract versions*}
-lemma numeral_0_eq_0 [simp]: "Numeral0 = (0::'a::number_ring)"
-by (simp add: number_of) 
-
-lemma numeral_1_eq_1 [simp]: "Numeral1 = (1::'a::number_ring)"
-by (simp add: number_of) 
-
-text{*Special-case simplification for small constants*}
-
-text{*Unary minus for the abstract constant 1. Cannot be inserted
-  as a simprule until later: it is @{text number_of_Min} re-oriented!*}
-lemma numeral_m1_eq_minus_1: "(-1::'a::number_ring) = - 1"
-by (simp add: number_of)
-
-lemma mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)"
-by (simp add: numeral_m1_eq_minus_1)
-
-lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)"
-by (simp add: numeral_m1_eq_minus_1)
-
-(*Negation of a coefficient*)
-lemma minus_number_of_mult [simp]:
-     "- (number_of w) * z = number_of(bin_minus w) * (z::'a::number_ring)"
-by (simp add: number_of_minus)
-
-text{*Subtraction*}
-lemma diff_number_of_eq:
-     "number_of v - number_of w =
-      (number_of(bin_add v (bin_minus w))::'a::number_ring)"
-by (simp add: diff_minus number_of_add number_of_minus)
-
-
-subsection{*Equality of Binary Numbers*}
-
-text{*First version by Norbert Voelker*}
-
-lemma eq_number_of_eq:
-  "((number_of x::'a::number_ring) = number_of y) =
-   iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
-by (simp add: iszero_def compare_rls number_of_add number_of_minus)
-
-lemma iszero_number_of_Pls: "iszero ((number_of bin.Pls)::'a::number_ring)"
-by (simp add: iszero_def numeral_0_eq_0)
-
-lemma nonzero_number_of_Min: "~ iszero ((number_of bin.Min)::'a::number_ring)"
-by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
-
-
-subsection{*Comparisons, for Ordered Rings*}
-
-lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))"
-proof -
-  have "a + a = (1+1)*a" by (simp add: left_distrib)
-  with zero_less_two [where 'a = 'a]
-  show ?thesis by force
-qed
-
-lemma le_imp_0_less: 
-  assumes le: "0 \<le> z" shows "(0::int) < 1 + z"
-proof -
-  have "0 \<le> z" .
-  also have "... < z + 1" by (rule less_add_one) 
-  also have "... = 1 + z" by (simp add: add_ac)
-  finally show "0 < 1 + z" .
-qed
-
-lemma odd_nonzero: "1 + z + z \<noteq> (0::int)";
-proof (cases z rule: int_cases)
-  case (nonneg n)
-  have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
-  thus ?thesis using  le_imp_0_less [OF le]
-    by (auto simp add: add_assoc) 
-next
-  case (neg n)
-  show ?thesis
-  proof
-    assume eq: "1 + z + z = 0"
-    have "0 < 1 + (int n + int n)"
-      by (simp add: le_imp_0_less add_increasing) 
-    also have "... = - (1 + z + z)" 
-      by (simp add: neg add_assoc [symmetric]) 
-    also have "... = 0" by (simp add: eq) 
-    finally have "0<0" ..
-    thus False by blast
-  qed
-qed
-
-
-text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
-lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)"
-proof (unfold Ints_def) 
-  assume "a \<in> range of_int"
-  then obtain z where a: "a = of_int z" ..
-  show ?thesis
-  proof
-    assume eq: "1 + a + a = 0"
-    hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
-    hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
-    with odd_nonzero show False by blast
-  qed
-qed 
-
-lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"
-by (induct_tac "w", simp_all add: number_of)
-
-lemma iszero_number_of_BIT:
-     "iszero (number_of (w BIT x)::'a) = 
-      (~x & iszero (number_of w::'a::{ordered_idom,number_ring}))"
-by (simp add: iszero_def compare_rls zero_reorient double_eq_0_iff 
-              number_of Ints_odd_nonzero [OF Ints_number_of])
-
-lemma iszero_number_of_0:
-     "iszero (number_of (w BIT False) :: 'a::{ordered_idom,number_ring}) = 
-      iszero (number_of w :: 'a)"
-by (simp only: iszero_number_of_BIT simp_thms)
-
-lemma iszero_number_of_1:
-     "~ iszero (number_of (w BIT True)::'a::{ordered_idom,number_ring})"
-by (simp only: iszero_number_of_BIT simp_thms)
-
-
-
-subsection{*The Less-Than Relation*}
-
-lemma less_number_of_eq_neg:
-    "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
-     = neg (number_of (bin_add x (bin_minus y)) :: 'a)"
-apply (subst less_iff_diff_less_0) 
-apply (simp add: neg_def diff_minus number_of_add number_of_minus)
-done
-
-text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
-  @{term Numeral0} IS @{term "number_of Pls"} *}
-lemma not_neg_number_of_Pls:
-     "~ neg (number_of bin.Pls ::'a::{ordered_idom,number_ring})"
-by (simp add: neg_def numeral_0_eq_0)
-
-lemma neg_number_of_Min:
-     "neg (number_of bin.Min ::'a::{ordered_idom,number_ring})"
-by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
-
-lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
-proof -
-  have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
-  also have "... = (a < 0)"
-    by (simp add: mult_less_0_iff zero_less_two 
-                  order_less_not_sym [OF zero_less_two]) 
-  finally show ?thesis .
-qed
-
-lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))";
-proof (cases z rule: int_cases)
-  case (nonneg n)
-  thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
-                             le_imp_0_less [THEN order_less_imp_le])  
-next
-  case (neg n)
-  thus ?thesis by (simp del: int_Suc
-			add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
-qed
-
-text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
-lemma Ints_odd_less_0: 
-     "a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
-proof (unfold Ints_def) 
-  assume "a \<in> range of_int"
-  then obtain z where a: "a = of_int z" ..
-  hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
-    by (simp add: a)
-  also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
-  also have "... = (a < 0)" by (simp add: a)
-  finally show ?thesis .
-qed
-
-lemma neg_number_of_BIT:
-     "neg (number_of (w BIT x)::'a) = 
-      neg (number_of w :: 'a::{ordered_idom,number_ring})"
-by (simp add: number_of neg_def double_less_0_iff
-              Ints_odd_less_0 [OF Ints_number_of])
-
-
-text{*Less-Than or Equals*}
-
-text{*Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals*}
-lemmas le_number_of_eq_not_less =
-       linorder_not_less [of "number_of w" "number_of v", symmetric, 
-                          standard]
-
-lemma le_number_of_eq:
-    "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
-     = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"
-by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
-
-
-text{*Absolute value (@{term abs})*}
-
-lemma abs_number_of:
-     "abs(number_of x::'a::{ordered_idom,number_ring}) =
-      (if number_of x < (0::'a) then -number_of x else number_of x)"
-by (simp add: abs_if)
-
-
-text{*Re-orientation of the equation nnn=x*}
-lemma number_of_reorient: "(number_of w = x) = (x = number_of w)"
-by auto
-
-
-(*Delete the original rewrites, with their clumsy conditional expressions*)
-declare bin_succ_BIT [simp del] bin_pred_BIT [simp del]
-        bin_minus_BIT [simp del]
-
-declare bin_add_BIT [simp del] bin_mult_BIT [simp del]
-declare NCons_Pls [simp del] NCons_Min [simp del]
-
-(*Hide the binary representation of integer constants*)
-declare number_of_Pls [simp del] number_of_Min [simp del]
-        number_of_BIT [simp del]
-
-
-
-(*Simplification of arithmetic operations on integer constants.
-  Note that bin_pred_Pls, etc. were added to the simpset by primrec.*)
-
-lemmas NCons_simps = NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT
-
-lemmas bin_arith_extra_simps = 
-       number_of_add [symmetric]
-       number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
-       number_of_mult [symmetric]
-       bin_succ_1 bin_succ_0
-       bin_pred_1 bin_pred_0
-       bin_minus_1 bin_minus_0
-       bin_add_Pls_right bin_add_Min_right
-       bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
-       diff_number_of_eq abs_number_of abs_zero abs_one
-       bin_mult_1 bin_mult_0 NCons_simps
-
-(*For making a minimal simpset, one must include these default simprules
-  of thy.  Also include simp_thms, or at least (~False)=True*)
-lemmas bin_arith_simps = 
-       bin_pred_Pls bin_pred_Min
-       bin_succ_Pls bin_succ_Min
-       bin_add_Pls bin_add_Min
-       bin_minus_Pls bin_minus_Min
-       bin_mult_Pls bin_mult_Min bin_arith_extra_simps
-
-(*Simplification of relational operations*)
-lemmas bin_rel_simps = 
-       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 not_neg_0 not_neg_1 not_iszero_1
-       neg_number_of_Min neg_number_of_BIT
-       le_number_of_eq
-
-declare bin_arith_extra_simps [simp]
-declare bin_rel_simps [simp]
-
-
-subsection{*Simplification of arithmetic when nested to the right*}
-
-lemma add_number_of_left [simp]:
-     "number_of v + (number_of w + z) =
-      (number_of(bin_add v w) + z::'a::number_ring)"
-by (simp add: add_assoc [symmetric])
-
-lemma mult_number_of_left [simp]:
-    "number_of v * (number_of w * z) =
-     (number_of(bin_mult v w) * z::'a::number_ring)"
-by (simp add: mult_assoc [symmetric])
-
-lemma add_number_of_diff1:
-    "number_of v + (number_of w - c) = 
-     number_of(bin_add v w) - (c::'a::number_ring)"
-by (simp add: diff_minus add_number_of_left)
-
-lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) =
-     number_of (bin_add v (bin_minus w)) + (c::'a::number_ring)"
-apply (subst diff_number_of_eq [symmetric])
-apply (simp only: compare_rls)
-done
-
-end
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Integ/IntArith.thy
--- a/src/HOL/Integ/IntArith.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Integ/IntArith.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -5,7 +5,7 @@
 
 header {* Integer arithmetic *}
 
-theory IntArith = Bin
+theory IntArith = Numeral
 files ("int_arith1.ML"):
 
 text{*Duplicate: can't understand why it's necessary*}
@@ -16,26 +16,12 @@
 instance
   int :: number ..
 
-primrec (*the type constraint is essential!*)
-  number_of_Pls: "number_of bin.Pls = 0"
-  number_of_Min: "number_of bin.Min = - (1::int)"
-  number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
-	                               (number_of w) + (number_of w)"
-
-declare number_of_Pls [simp del]
-        number_of_Min [simp del]
-        number_of_BIT [simp del]
+defs (overloaded)
+  int_number_of_def: "(number_of w :: int) == of_int (Rep_Bin w)"
+    --{*the type constraint is essential!*}
 
 instance int :: number_ring
-proof
-  show "Numeral0 = (0::int)" by (rule number_of_Pls)
-  show "-1 = - (1::int)" by (rule number_of_Min)
-  fix w :: bin and x :: bool
-  show "(number_of (w BIT x) :: int) =
-        (if x then 1 else 0) + number_of w + number_of w"
-    by (rule number_of_BIT)
-qed
-
+by (intro_classes, simp add: int_number_of_def) 
 
 
 subsection{*Inequality Reasoning for the Arithmetic Simproc*}
@@ -135,9 +121,7 @@
 
 lemma of_int_number_of_eq:
      "of_int (number_of v) = (number_of v :: 'a :: number_ring)"
-apply (induct v)
-apply (simp_all only: number_of of_int_add, simp_all) 
-done
+by (simp add: number_of_eq) 
 
 text{*Lemmas for specialist use, NOT as default simprules*}
 lemma mult_2: "2 * z = (z+z::'a::number_ring)"
@@ -210,7 +194,7 @@
 
 
 (*Analogous to zadd_int*)
-lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)"
+lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)" 
 by (induct m n rule: diff_induct, simp_all)
 
 lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Integ/IntDef.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -810,10 +810,9 @@
 lemma of_int_of_nat_eq [simp]: "of_int (of_nat n) = of_nat n"
 by (induct n, auto)
 
-lemma of_int_int_eq [simp]: "of_int (int n) = int n"
+lemma of_int_int_eq [simp]: "of_int (int n) = of_nat n"
 by (simp add: int_eq_of_nat)
 
-
 lemma Ints_cases [case_names of_int, cases set: Ints]:
   "q \<in> \<int> ==> (!!z. q = of_int z ==> C) ==> C"
 proof (simp add: Ints_def)
@@ -922,6 +921,12 @@
   by (cases z) auto
 
 
+lemma of_nat_nat: "0 \<le> z ==> of_nat (nat z) = of_int z"
+apply (cases z)
+apply (simp_all add: not_zle_0_negative del: int_Suc)
+done
+
+
 (*Legacy ML bindings, but no longer the structure Int.*)
 ML
 {*
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Integ/IntDiv.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -221,7 +221,7 @@
 (** Basic laws about division and remainder **)
 
 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
 apply (cut_tac a = a and b = b in divAlg_correct)
 apply (auto simp add: quorem_def div_def mod_def)
 done
@@ -302,7 +302,7 @@
 
 (*Simpler laws such as -a div b = -(a div b) FAIL, but see just below*)
 lemma zdiv_zminus_zminus [simp]: "(-a) div (-b) = a div (b::int)"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
 apply (simp add: quorem_div_mod [THEN quorem_neg, simplified, 
                                  THEN quorem_div, THEN sym])
 
@@ -310,7 +310,7 @@
 
 (*Simpler laws such as -a mod b = -(a mod b) FAIL, but see just below*)
 lemma zmod_zminus_zminus [simp]: "(-a) mod (-b) = - (a mod (b::int))"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
 apply (subst quorem_div_mod [THEN quorem_neg, simplified, THEN quorem_mod],
        auto)
 done
@@ -332,7 +332,7 @@
 
 lemma zmod_zminus1_eq_if:
      "(-a::int) mod b = (if a mod b = 0 then 0 else  b - (a mod b))"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
 apply (blast intro: quorem_div_mod [THEN zminus1_lemma, THEN quorem_mod])
 done
 
@@ -384,7 +384,7 @@
 
 (*Here we have 0 mod 0 = 0, also assumed by Knuth (who puts m mod 0 = 0) *)
 lemma zmod_self [simp]: "a mod a = (0::int)"
-apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "a = 0", simp)
 apply (simp add: quorem_div_mod [THEN self_remainder])
 done
 
@@ -588,12 +588,12 @@
 by (force simp add: split_ifs quorem_def linorder_neq_iff right_distrib)
 
 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
-apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "c = 0", simp)
 apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_div])
 done
 
 lemma zmod_zmult1_eq: "(a*b) mod c = a*(b mod c) mod (c::int)"
-apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "c = 0", simp)
 apply (blast intro: quorem_div_mod [THEN zmult1_lemma, THEN quorem_mod])
 done
 
@@ -642,22 +642,22 @@
 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
 lemma zdiv_zadd1_eq:
      "(a+b) div (c::int) = a div c + b div c + ((a mod c + b mod c) div c)"
-apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "c = 0", simp)
 apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_div)
 done
 
 lemma zmod_zadd1_eq: "(a+b) mod (c::int) = (a mod c + b mod c) mod c"
-apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "c = 0", simp)
 apply (blast intro: zadd1_lemma [OF quorem_div_mod quorem_div_mod] quorem_mod)
 done
 
 lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
 apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
 done
 
 lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
 apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
 done
 
@@ -680,12 +680,12 @@
 by (simp add: zdiv_zadd1_eq)
 
 lemma zmod_zadd_self1[simp]: "(a+b) mod a = b mod (a::int)"
-apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "a = 0", simp)
 apply (simp add: zmod_zadd1_eq)
 done
 
 lemma zmod_zadd_self2[simp]: "(b+a) mod a = b mod (a::int)"
-apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "a = 0", simp)
 apply (simp add: zmod_zadd1_eq)
 done
 
@@ -737,13 +737,13 @@
                    zmult2_lemma_aux1 zmult2_lemma_aux2 zmult2_lemma_aux3 zmult2_lemma_aux4)
 
 lemma zdiv_zmult2_eq: "(0::int) < c ==> a div (b*c) = (a div b) div c"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
 apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_div])
 done
 
 lemma zmod_zmult2_eq:
      "(0::int) < c ==> a mod (b*c) = b*(a div b mod c) + a mod b"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
 apply (force simp add: quorem_div_mod [THEN zmult2_lemma, THEN quorem_mod])
 done
 
@@ -759,7 +759,7 @@
 done
 
 lemma zdiv_zmult_zmult1: "c ~= (0::int) ==> (c*a) div (c*b) = a div b"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
 apply (auto simp add: linorder_neq_iff zdiv_zmult_zmult1_aux1 zdiv_zmult_zmult1_aux2)
 done
 
@@ -781,8 +781,8 @@
 done
 
 lemma zmod_zmult_zmult1: "(c*a) mod (c*b) = (c::int) * (a mod b)"
-apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
-apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "b = 0", simp)
+apply (case_tac "c = 0", simp)
 apply (auto simp add: linorder_neq_iff zmod_zmult_zmult1_aux1 zmod_zmult_zmult1_aux2)
 done
 
@@ -832,7 +832,7 @@
    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P i)) & 
    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P i)))"
 apply (case_tac "k=0")
- apply (simp add: DIVISION_BY_ZERO)
+ apply (simp)
 apply (simp only: linorder_neq_iff)
 apply (erule disjE) 
  apply (simp_all add: split_pos_lemma [of concl: "%x y. P x"] 
@@ -845,7 +845,7 @@
    (0<k --> (\<forall>i j. 0\<le>j & j<k & n = k*i + j --> P j)) & 
    (k<0 --> (\<forall>i j. k<j & j\<le>0 & n = k*i + j --> P j)))"
 apply (case_tac "k=0")
- apply (simp add: DIVISION_BY_ZERO)
+ apply (simp)
 apply (simp only: linorder_neq_iff)
 apply (erule disjE) 
  apply (simp_all add: split_pos_lemma [of concl: "%x y. P y"] 
@@ -904,20 +904,16 @@
           (if ~b | (0::int) \<le> number_of w                    
            then number_of v div (number_of w)     
            else (number_of v + (1::int)) div (number_of w))"
-apply (simp only: add_assoc number_of_BIT)
-(*create subgoal because the next step can't simplify numerals*)
-apply (subgoal_tac "2 ~= (0::int) ") 
-apply (simp del: bin_arith_extra_simps arith_special
-         add: zdiv_zmult_zmult1 pos_zdiv_mult_2 not_0_le_lemma neg_zdiv_mult_2)
-apply simp
+apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if) 
+apply (simp add: zdiv_zmult_zmult1 pos_zdiv_mult_2 neg_zdiv_mult_2 add_ac)
 done
 
 
-(** computing mod by shifting (proofs resemble those for div) **)
+subsection{*Computing mod by Shifting (proofs resemble those for div)*}
 
 lemma pos_zmod_mult_2:
      "(0::int) \<le> a ==> (1 + 2*b) mod (2*a) = 1 + 2 * (b mod a)"
-apply (case_tac "a = 0", simp add: DIVISION_BY_ZERO)
+apply (case_tac "a = 0", simp)
 apply (subgoal_tac "1 \<le> a")
  prefer 2 apply arith
 apply (subgoal_tac "1 < a * 2")
@@ -952,15 +948,14 @@
                 then 2 * (number_of v mod number_of w) + 1     
                 else 2 * ((number_of v + (1::int)) mod number_of w) - 1   
            else 2 * (number_of v mod number_of w))"
-apply (simp only: zadd_assoc number_of_BIT)
-apply (simp del: bin_arith_extra_simps bin_rel_simps arith_special
-         add: zmod_zmult_zmult1 pos_zmod_mult_2 not_0_le_lemma neg_zmod_mult_2
- neg_def) 
+apply (simp only: number_of_eq Bin_simps UNIV_I split: split_if) 
+apply (simp add: zmod_zmult_zmult1 pos_zmod_mult_2 
+                 not_0_le_lemma neg_zmod_mult_2 add_ac)
 done
 
 
 
-(** Quotients of signs **)
+subsection{*Quotients of Signs*}
 
 lemma div_neg_pos_less0: "[| a < (0::int);  0 < b |] ==> a div b < 0"
 apply (subgoal_tac "a div b \<le> -1", force)
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Integ/NatBin.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -478,8 +478,8 @@
 
 
 lemma eq_number_of_BIT_Pls:
-     "((number_of (v BIT x) ::int) = number_of bin.Pls) =  
-      (x=False & (((number_of v) ::int) = number_of bin.Pls))"
+     "((number_of (v BIT x) ::int) = Numeral0) =  
+      (x=False & (((number_of v) ::int) = Numeral0))"
 apply (simp only: simp_thms  add: number_of_BIT number_of_Pls eq_commute
             split add: split_if cong: imp_cong)
 apply (rule_tac x = "number_of v" in spec, safe)
@@ -489,15 +489,15 @@
 done
 
 lemma eq_number_of_BIT_Min:
-     "((number_of (v BIT x) ::int) = number_of bin.Min) =  
-      (x=True & (((number_of v) ::int) = number_of bin.Min))"
+     "((number_of (v BIT x) ::int) = number_of Numeral.Min) =  
+      (x=True & (((number_of v) ::int) = number_of Numeral.Min))"
 apply (simp only: simp_thms  add: number_of_BIT number_of_Min eq_commute
             split add: split_if cong: imp_cong)
 apply (rule_tac x = "number_of v" in spec, auto)
 apply (drule_tac f = "%x. x mod 2" in arg_cong, auto)
 done
 
-lemma eq_number_of_Pls_Min: "(number_of bin.Pls ::int) ~= number_of bin.Min"
+lemma eq_number_of_Pls_Min: "(Numeral0 ::int) ~= number_of Numeral.Min"
 by auto
 
 
@@ -569,10 +569,10 @@
 declare split_div[of _ _ "number_of k", standard, arith_split]
 declare split_mod[of _ _ "number_of k", standard, arith_split]
 
-lemma nat_number_of_Pls: "number_of bin.Pls = (0::nat)"
+lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
   by (simp add: number_of_Pls nat_number_of_def)
 
-lemma nat_number_of_Min: "number_of bin.Min = (0::nat)"
+lemma nat_number_of_Min: "number_of Numeral.Min = (0::nat)"
   apply (simp only: number_of_Min nat_number_of_def nat_zminus_int)
   apply (simp add: neg_nat)
   done
@@ -622,23 +622,12 @@
 lemma nat_numeral_m1_eq_0: "-1 = (0::nat)"
 by (simp only:  nat_number_of_def, simp)
 
-lemma int_double_iff: "(0::int) \<le> 2*x + 1 = (0 \<le> x)"
-by arith
-
 lemma of_nat_number_of_lemma:
      "of_nat (number_of v :: nat) =  
          (if 0 \<le> (number_of v :: int) 
           then (number_of v :: 'a :: number_ring)
           else 0)"
-apply (induct v, simp, simp add: nat_numeral_m1_eq_0)
-apply (simp only: number_of nat_number_of_def)
-txt{*Generalize in order to eliminate the function @{term number_of} and
-its annoying simprules*}
-apply (erule rev_mp)
-apply (rule_tac x="number_of bin :: int" in spec) 
-apply (rule_tac x="number_of bin :: 'a" in spec) 
-apply (simp add: nat_add_distrib of_nat_double int_double_iff)
-done
+by (simp add: int_number_of_def nat_number_of_def number_of_eq of_nat_nat);
 
 lemma of_nat_number_of_eq [simp]:
      "of_nat (number_of v :: nat) =  
@@ -850,6 +839,8 @@
   "uminus" :: "int => int"      ("`~")
   "op +" :: "int => int => int" ("(_ `+/ _)")
   "op *" :: "int => int => int" ("(_ `*/ _)")
+  "op div" :: "int => int => int" ("(_ `div/ _)")
+  "op mod" :: "int => int => int" ("(_ `mod/ _)")
   "op <" :: "int => int => bool" ("(_ </ _)")
   "op <=" :: "int => int => bool" ("(_ <=/ _)")
   "neg"                         ("(_ < 0)")
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Integ/Numeral.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Numeral.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -0,0 +1,505 @@
+(*  Title:	HOL/Integ/Numeral.thy
+    ID:         $Id$
+    Author:	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright	1994  University of Cambridge
+*)
+
+header{*Arithmetic on Binary Integers*}
+
+theory Numeral = IntDef
+files "Tools/numeral_syntax.ML":
+
+text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
+   Only qualified access Numeral.Pls and Numeral.Min is allowed.
+   We do not hide Bit because we need the BIT infix syntax.*}
+
+text{*This formalization defines binary arithmetic in terms of the integers
+rather than using a datatype. This avoids multiple representations (leading
+zeroes, etc.)  See @{text "ZF/Integ/twos-compl.ML"}, function @{text
+int_of_binary}, for the numerical interpretation.
+
+The representation expects that @{text "(m mod 2)"} is 0 or 1,
+even if m is negative;
+For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
+@{text "-5 = (-3)*2 + 1"}.
+*}
+
+
+typedef (Bin)
+  bin = "UNIV::int set"
+    by (auto)
+
+constdefs
+  Pls :: "bin"
+   "Pls == Abs_Bin 0"
+
+  Min :: "bin"
+   "Min == Abs_Bin (- 1)"
+
+  Bit :: "[bin,bool] => bin"    (infixl "BIT" 90)
+   --{*That is, 2w+b*}
+   "w BIT b == Abs_Bin ((if b then 1 else 0) + Rep_Bin w + Rep_Bin w)"
+
+
+axclass
+  number < type  -- {* for numeric types: nat, int, real, \dots *}
+
+consts
+  number_of :: "bin => 'a::number"
+
+syntax
+  "_Numeral" :: "num_const => 'a"    ("_")
+  Numeral0 :: 'a
+  Numeral1 :: 'a
+
+translations
+  "Numeral0" == "number_of Numeral.Pls"
+  "Numeral1" == "number_of (Numeral.Pls BIT True)"
+
+
+setup NumeralSyntax.setup
+
+syntax (xsymbols)
+  "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
+syntax (HTML output)
+  "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
+syntax (output)
+  "_square" :: "'a => 'a"  ("(_ ^/ 2)" [81] 80)
+translations
+  "x\<twosuperior>" == "x^2"
+  "x\<twosuperior>" <= "x^(2::nat)"
+
+
+lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
+  -- {* Unfold all @{text let}s involving constants *}
+  by (simp add: Let_def)
+
+lemma Let_0 [simp]: "Let 0 f == f 0"
+  by (simp add: Let_def)
+
+lemma Let_1 [simp]: "Let 1 f == f 1"
+  by (simp add: Let_def)
+
+
+constdefs
+  bin_succ  :: "bin=>bin"
+   "bin_succ w == Abs_Bin(Rep_Bin w + 1)"
+
+  bin_pred  :: "bin=>bin"
+   "bin_pred w == Abs_Bin(Rep_Bin w - 1)"
+
+  bin_minus  :: "bin=>bin"
+   "bin_minus w == Abs_Bin(- (Rep_Bin w))"
+
+  bin_add  :: "[bin,bin]=>bin"
+   "bin_add v w == Abs_Bin(Rep_Bin v + Rep_Bin w)"
+
+  bin_mult  :: "[bin,bin]=>bin"
+   "bin_mult v w == Abs_Bin(Rep_Bin v * Rep_Bin w)"
+
+
+lemmas Bin_simps = 
+       bin_succ_def bin_pred_def bin_minus_def bin_add_def bin_mult_def
+       Pls_def Min_def Bit_def Abs_Bin_inverse Rep_Bin_inverse Bin_def
+
+text{*Removal of leading zeroes*}
+lemma Pls_0_eq [simp]: "Numeral.Pls BIT False = Numeral.Pls"
+by (simp add: Bin_simps)
+
+lemma Min_1_eq [simp]: "Numeral.Min BIT True = Numeral.Min"
+by (simp add: Bin_simps)
+
+subsection{*The Functions @{term bin_succ},  @{term bin_pred} and @{term bin_minus}*}
+
+lemma bin_succ_Pls [simp]: "bin_succ Numeral.Pls = Numeral.Pls BIT True"
+by (simp add: Bin_simps) 
+
+lemma bin_succ_Min [simp]: "bin_succ Numeral.Min = Numeral.Pls"
+by (simp add: Bin_simps) 
+
+lemma bin_succ_1 [simp]: "bin_succ(w BIT True) = (bin_succ w) BIT False"
+by (simp add: Bin_simps add_ac) 
+
+lemma bin_succ_0 [simp]: "bin_succ(w BIT False) = w BIT True"
+by (simp add: Bin_simps add_ac) 
+
+lemma bin_pred_Pls [simp]: "bin_pred Numeral.Pls = Numeral.Min"
+by (simp add: Bin_simps) 
+
+lemma bin_pred_Min [simp]: "bin_pred Numeral.Min = Numeral.Min BIT False"
+by (simp add: Bin_simps diff_minus) 
+
+lemma bin_pred_1 [simp]: "bin_pred(w BIT True) = w BIT False"
+by (simp add: Bin_simps) 
+
+lemma bin_pred_0 [simp]: "bin_pred(w BIT False) = (bin_pred w) BIT True"
+by (simp add: Bin_simps diff_minus add_ac) 
+
+lemma bin_minus_Pls [simp]: "bin_minus Numeral.Pls = Numeral.Pls"
+by (simp add: Bin_simps) 
+
+lemma bin_minus_Min [simp]: "bin_minus Numeral.Min = Numeral.Pls BIT True"
+by (simp add: Bin_simps) 
+
+lemma bin_minus_1 [simp]:
+     "bin_minus (w BIT True) = bin_pred (bin_minus w) BIT True"
+by (simp add: Bin_simps add_ac diff_minus) 
+
+ lemma bin_minus_0 [simp]: "bin_minus(w BIT False) = (bin_minus w) BIT False"
+by (simp add: Bin_simps) 
+
+
+subsection{*Binary Addition and Multiplication:
+         @{term bin_add} and @{term bin_mult}*}
+
+lemma bin_add_Pls [simp]: "bin_add Numeral.Pls w = w"
+by (simp add: Bin_simps) 
+
+lemma bin_add_Min [simp]: "bin_add Numeral.Min w = bin_pred w"
+by (simp add: Bin_simps diff_minus add_ac) 
+
+lemma bin_add_BIT_11 [simp]:
+     "bin_add (v BIT True) (w BIT True) = bin_add v (bin_succ w) BIT False"
+by (simp add: Bin_simps add_ac)
+
+lemma bin_add_BIT_10 [simp]:
+     "bin_add (v BIT True) (w BIT False) = (bin_add v w) BIT True"
+by (simp add: Bin_simps add_ac)
+
+lemma bin_add_BIT_0 [simp]:
+     "bin_add (v BIT False) (w BIT y) = bin_add v w BIT y"
+by (simp add: Bin_simps add_ac)
+
+lemma bin_add_Pls_right [simp]: "bin_add w Numeral.Pls = w"
+by (simp add: Bin_simps) 
+
+lemma bin_add_Min_right [simp]: "bin_add w Numeral.Min = bin_pred w"
+by (simp add: Bin_simps diff_minus) 
+
+lemma bin_mult_Pls [simp]: "bin_mult Numeral.Pls w = Numeral.Pls"
+by (simp add: Bin_simps) 
+
+lemma bin_mult_Min [simp]: "bin_mult Numeral.Min w = bin_minus w"
+by (simp add: Bin_simps) 
+
+lemma bin_mult_1 [simp]:
+     "bin_mult (v BIT True) w = bin_add ((bin_mult v w) BIT False) w"
+by (simp add: Bin_simps add_ac left_distrib)
+
+lemma bin_mult_0 [simp]: "bin_mult (v BIT False) w = (bin_mult v w) BIT False"
+by (simp add: Bin_simps left_distrib)
+
+
+
+subsection{*Converting Numerals to Rings: @{term number_of}*}
+
+axclass number_ring \<subseteq> number, comm_ring_1
+  number_of_eq: "number_of w = of_int (Rep_Bin w)"
+
+lemma number_of_succ:
+     "number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps)
+
+lemma number_of_pred:
+     "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps)
+
+lemma number_of_minus:
+     "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps) 
+
+lemma number_of_add:
+     "number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps) 
+
+lemma number_of_mult:
+     "number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps) 
+
+text{*The correctness of shifting.  But it doesn't seem to give a measurable
+  speed-up.*}
+lemma double_number_of_BIT:
+     "(1+1) * number_of w = (number_of (w BIT False) ::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps left_distrib) 
+
+text{*Converting numerals 0 and 1 to their abstract versions*}
+lemma numeral_0_eq_0 [simp]: "Numeral0 = (0::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps) 
+
+lemma numeral_1_eq_1 [simp]: "Numeral1 = (1::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps) 
+
+text{*Special-case simplification for small constants*}
+
+text{*Unary minus for the abstract constant 1. Cannot be inserted
+  as a simprule until later: it is @{text number_of_Min} re-oriented!*}
+lemma numeral_m1_eq_minus_1: "(-1::'a::number_ring) = - 1"
+by (simp add: number_of_eq Bin_simps) 
+
+
+lemma mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)"
+by (simp add: numeral_m1_eq_minus_1)
+
+lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)"
+by (simp add: numeral_m1_eq_minus_1)
+
+(*Negation of a coefficient*)
+lemma minus_number_of_mult [simp]:
+     "- (number_of w) * z = number_of(bin_minus w) * (z::'a::number_ring)"
+by (simp add: number_of_minus)
+
+text{*Subtraction*}
+lemma diff_number_of_eq:
+     "number_of v - number_of w =
+      (number_of(bin_add v (bin_minus w))::'a::number_ring)"
+by (simp add: diff_minus number_of_add number_of_minus)
+
+
+lemma number_of_Pls: "number_of Numeral.Pls = (0::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps) 
+
+lemma number_of_Min: "number_of Numeral.Min = (- 1::'a::number_ring)"
+by (simp add: number_of_eq Bin_simps) 
+
+lemma number_of_BIT:
+     "number_of(w BIT x) = (if x then 1 else (0::'a::number_ring)) +
+	                   (number_of w) + (number_of w)"
+by (simp add: number_of_eq Bin_simps) 
+
+
+
+subsection{*Equality of Binary Numbers*}
+
+text{*First version by Norbert Voelker*}
+
+lemma eq_number_of_eq:
+  "((number_of x::'a::number_ring) = number_of y) =
+   iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
+by (simp add: iszero_def compare_rls number_of_add number_of_minus)
+
+lemma iszero_number_of_Pls: "iszero ((number_of Numeral.Pls)::'a::number_ring)"
+by (simp add: iszero_def numeral_0_eq_0)
+
+lemma nonzero_number_of_Min: "~ iszero ((number_of Numeral.Min)::'a::number_ring)"
+by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)
+
+
+subsection{*Comparisons, for Ordered Rings*}
+
+lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))"
+proof -
+  have "a + a = (1+1)*a" by (simp add: left_distrib)
+  with zero_less_two [where 'a = 'a]
+  show ?thesis by force
+qed
+
+lemma le_imp_0_less: 
+  assumes le: "0 \<le> z" shows "(0::int) < 1 + z"
+proof -
+  have "0 \<le> z" .
+  also have "... < z + 1" by (rule less_add_one) 
+  also have "... = 1 + z" by (simp add: add_ac)
+  finally show "0 < 1 + z" .
+qed
+
+lemma odd_nonzero: "1 + z + z \<noteq> (0::int)";
+proof (cases z rule: int_cases)
+  case (nonneg n)
+  have le: "0 \<le> z+z" by (simp add: nonneg add_increasing) 
+  thus ?thesis using  le_imp_0_less [OF le]
+    by (auto simp add: add_assoc) 
+next
+  case (neg n)
+  show ?thesis
+  proof
+    assume eq: "1 + z + z = 0"
+    have "0 < 1 + (int n + int n)"
+      by (simp add: le_imp_0_less add_increasing) 
+    also have "... = - (1 + z + z)" 
+      by (simp add: neg add_assoc [symmetric]) 
+    also have "... = 0" by (simp add: eq) 
+    finally have "0<0" ..
+    thus False by blast
+  qed
+qed
+
+
+text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
+lemma Ints_odd_nonzero: "a \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)"
+proof (unfold Ints_def) 
+  assume "a \<in> range of_int"
+  then obtain z where a: "a = of_int z" ..
+  show ?thesis
+  proof
+    assume eq: "1 + a + a = 0"
+    hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
+    hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
+    with odd_nonzero show False by blast
+  qed
+qed 
+
+lemma Ints_number_of: "(number_of w :: 'a::number_ring) \<in> Ints"
+by (simp add: number_of_eq Ints_def) 
+
+
+lemma iszero_number_of_BIT:
+     "iszero (number_of (w BIT x)::'a) = 
+      (~x & iszero (number_of w::'a::{ordered_idom,number_ring}))"
+by (simp add: iszero_def number_of_eq Bin_simps double_eq_0_iff 
+              Ints_odd_nonzero Ints_def)
+
+lemma iszero_number_of_0:
+     "iszero (number_of (w BIT False) :: 'a::{ordered_idom,number_ring}) = 
+      iszero (number_of w :: 'a)"
+by (simp only: iszero_number_of_BIT simp_thms)
+
+lemma iszero_number_of_1:
+     "~ iszero (number_of (w BIT True)::'a::{ordered_idom,number_ring})"
+by (simp only: iszero_number_of_BIT simp_thms)
+
+
+
+subsection{*The Less-Than Relation*}
+
+lemma less_number_of_eq_neg:
+    "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
+     = neg (number_of (bin_add x (bin_minus y)) :: 'a)"
+apply (subst less_iff_diff_less_0) 
+apply (simp add: neg_def diff_minus number_of_add number_of_minus)
+done
+
+text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
+  @{term Numeral0} IS @{term "number_of Numeral.Pls"} *}
+lemma not_neg_number_of_Pls:
+     "~ neg (number_of Numeral.Pls ::'a::{ordered_idom,number_ring})"
+by (simp add: neg_def numeral_0_eq_0)
+
+lemma neg_number_of_Min:
+     "neg (number_of Numeral.Min ::'a::{ordered_idom,number_ring})"
+by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
+
+lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
+proof -
+  have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
+  also have "... = (a < 0)"
+    by (simp add: mult_less_0_iff zero_less_two 
+                  order_less_not_sym [OF zero_less_two]) 
+  finally show ?thesis .
+qed
+
+lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))";
+proof (cases z rule: int_cases)
+  case (nonneg n)
+  thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
+                             le_imp_0_less [THEN order_less_imp_le])  
+next
+  case (neg n)
+  thus ?thesis by (simp del: int_Suc
+			add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
+qed
+
+text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
+lemma Ints_odd_less_0: 
+     "a \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
+proof (unfold Ints_def) 
+  assume "a \<in> range of_int"
+  then obtain z where a: "a = of_int z" ..
+  hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
+    by (simp add: a)
+  also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
+  also have "... = (a < 0)" by (simp add: a)
+  finally show ?thesis .
+qed
+
+lemma neg_number_of_BIT:
+     "neg (number_of (w BIT x)::'a) = 
+      neg (number_of w :: 'a::{ordered_idom,number_ring})"
+by (simp add: neg_def number_of_eq Bin_simps double_less_0_iff
+              Ints_odd_less_0 Ints_def)
+
+
+text{*Less-Than or Equals*}
+
+text{*Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals*}
+lemmas le_number_of_eq_not_less =
+       linorder_not_less [of "number_of w" "number_of v", symmetric, 
+                          standard]
+
+lemma le_number_of_eq:
+    "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
+     = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"
+by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
+
+
+text{*Absolute value (@{term abs})*}
+
+lemma abs_number_of:
+     "abs(number_of x::'a::{ordered_idom,number_ring}) =
+      (if number_of x < (0::'a) then -number_of x else number_of x)"
+by (simp add: abs_if)
+
+
+text{*Re-orientation of the equation nnn=x*}
+lemma number_of_reorient: "(number_of w = x) = (x = number_of w)"
+by auto
+
+
+
+
+subsection{*Simplification of arithmetic operations on integer constants.*}
+
+lemmas bin_arith_extra_simps = 
+       number_of_add [symmetric]
+       number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
+       number_of_mult [symmetric]
+       diff_number_of_eq abs_number_of 
+
+text{*For making a minimal simpset, one must include these default simprules.
+  Also include @{text simp_thms} or at least @{term "(~False)=True"} *}
+lemmas bin_arith_simps = 
+       Pls_0_eq Min_1_eq
+       bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
+       bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
+       bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
+       bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
+       bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0 
+       bin_add_Pls_right bin_add_Min_right
+       abs_zero abs_one bin_arith_extra_simps
+
+text{*Simplification of relational operations*}
+lemmas bin_rel_simps = 
+       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 not_neg_0 not_neg_1 not_iszero_1
+       neg_number_of_Min neg_number_of_BIT
+       le_number_of_eq
+
+declare bin_arith_extra_simps [simp]
+declare bin_rel_simps [simp]
+
+
+subsection{*Simplification of arithmetic when nested to the right*}
+
+lemma add_number_of_left [simp]:
+     "number_of v + (number_of w + z) =
+      (number_of(bin_add v w) + z::'a::number_ring)"
+by (simp add: add_assoc [symmetric])
+
+lemma mult_number_of_left [simp]:
+    "number_of v * (number_of w * z) =
+     (number_of(bin_mult v w) * z::'a::number_ring)"
+by (simp add: mult_assoc [symmetric])
+
+lemma add_number_of_diff1:
+    "number_of v + (number_of w - c) = 
+     number_of(bin_add v w) - (c::'a::number_ring)"
+by (simp add: diff_minus add_number_of_left)
+
+lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) =
+     number_of (bin_add v (bin_minus w)) + (c::'a::number_ring)"
+apply (subst diff_number_of_eq [symmetric])
+apply (simp only: compare_rls)
+done
+
+end
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Integ/Presburger.thy
--- a/src/HOL/Integ/Presburger.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Integ/Presburger.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -969,7 +969,7 @@
 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
   by simp
 
-theorem number_of2: "(0::int) <= number_of bin.Pls" by simp
+theorem number_of2: "(0::int) <= Numeral0" by simp
 
 theorem Suc_plus1: "Suc n = n + 1" by simp
 
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Integ/int_arith1.ML
--- a/src/HOL/Integ/int_arith1.ML	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Integ/int_arith1.ML	Thu Jul 01 12:29:53 2004 +0200
@@ -7,49 +7,37 @@
 
 (** Misc ML bindings **)
 
-val NCons_Pls = thm"NCons_Pls";
-val NCons_Min = thm"NCons_Min";
-val NCons_BIT = thm"NCons_BIT";
-val number_of_Pls = thm"number_of_Pls";
-val number_of_Min = thm"number_of_Min";
-val number_of_BIT = thm"number_of_BIT";
 val bin_succ_Pls = thm"bin_succ_Pls";
 val bin_succ_Min = thm"bin_succ_Min";
-val bin_succ_BIT = thm"bin_succ_BIT";
+val bin_succ_1 = thm"bin_succ_1";
+val bin_succ_0 = thm"bin_succ_0";
+
 val bin_pred_Pls = thm"bin_pred_Pls";
 val bin_pred_Min = thm"bin_pred_Min";
-val bin_pred_BIT = thm"bin_pred_BIT";
+val bin_pred_1 = thm"bin_pred_1";
+val bin_pred_0 = thm"bin_pred_0";
+
 val bin_minus_Pls = thm"bin_minus_Pls";
 val bin_minus_Min = thm"bin_minus_Min";
-val bin_minus_BIT = thm"bin_minus_BIT";
+val bin_minus_1 = thm"bin_minus_1";
+val bin_minus_0 = thm"bin_minus_0";
+
 val bin_add_Pls = thm"bin_add_Pls";
 val bin_add_Min = thm"bin_add_Min";
-val bin_mult_Pls = thm"bin_mult_Pls";
-val bin_mult_Min = thm"bin_mult_Min";
-val bin_mult_BIT = thm"bin_mult_BIT";
-
-val neg_def = thm "neg_def";
-val iszero_def = thm "iszero_def";
-
-val NCons_Pls_0 = thm"NCons_Pls_0";
-val NCons_Pls_1 = thm"NCons_Pls_1";
-val NCons_Min_0 = thm"NCons_Min_0";
-val NCons_Min_1 = thm"NCons_Min_1";
-val bin_succ_1 = thm"bin_succ_1";
-val bin_succ_0 = thm"bin_succ_0";
-val bin_pred_1 = thm"bin_pred_1";
-val bin_pred_0 = thm"bin_pred_0";
-val bin_minus_1 = thm"bin_minus_1";
-val bin_minus_0 = thm"bin_minus_0";
 val bin_add_BIT_11 = thm"bin_add_BIT_11";
 val bin_add_BIT_10 = thm"bin_add_BIT_10";
 val bin_add_BIT_0 = thm"bin_add_BIT_0";
 val bin_add_Pls_right = thm"bin_add_Pls_right";
 val bin_add_Min_right = thm"bin_add_Min_right";
-val bin_add_BIT_BIT = thm"bin_add_BIT_BIT";
+
+val bin_mult_Pls = thm"bin_mult_Pls";
+val bin_mult_Min = thm"bin_mult_Min";
 val bin_mult_1 = thm"bin_mult_1";
 val bin_mult_0 = thm"bin_mult_0";
-val number_of_NCons = thm"number_of_NCons";
+
+val neg_def = thm "neg_def";
+val iszero_def = thm "iszero_def";
+
 val number_of_succ = thm"number_of_succ";
 val number_of_pred = thm"number_of_pred";
 val number_of_minus = thm"number_of_minus";
@@ -86,7 +74,6 @@
 val eq_iff_diff_eq_0 = thm"eq_iff_diff_eq_0";
 val le_iff_diff_le_0 = thm"le_iff_diff_le_0";
 
-val NCons_simps = thms"NCons_simps";
 val bin_arith_extra_simps = thms"bin_arith_extra_simps";
 val bin_arith_simps = thms"bin_arith_simps";
 val bin_rel_simps = thms"bin_rel_simps";
@@ -298,10 +285,9 @@
     bin_simps \\ [add_number_of_left, number_of_add RS sym];
 
 (*To evaluate binary negations of coefficients*)
-val minus_simps = NCons_simps @
-                   [numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,
-                    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
-                    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
+val minus_simps = [numeral_m1_eq_minus_1 RS sym, number_of_minus RS sym,
+                   bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
+                   bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
 
 (*To let us treat subtraction as addition*)
 val diff_simps = [diff_minus, minus_add_distrib, minus_minus];
@@ -335,10 +321,10 @@
   val find_first_coeff  = find_first_coeff []
   val trans_tac         = trans_tac
   val norm_tac =
-     ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
+     ALLGOALS (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
                                          diff_simps@minus_simps@add_ac))
-     THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@mult_minus_simps))
-     THEN ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@
+     THEN ALLGOALS (simp_tac (num_ss addsimps non_add_bin_simps@mult_minus_simps))
+     THEN ALLGOALS (simp_tac (num_ss addsimps minus_from_mult_simps@
                                               add_ac@mult_ac))
   val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
@@ -411,10 +397,10 @@
   val prove_conv        = Bin_Simprocs.prove_conv_nohyps
   val trans_tac          = trans_tac
   val norm_tac =
-     ALLGOALS (simp_tac (HOL_ss addsimps numeral_syms@add_0s@mult_1s@
+     ALLGOALS (simp_tac (num_ss addsimps numeral_syms@add_0s@mult_1s@
                                          diff_simps@minus_simps@add_ac))
-     THEN ALLGOALS (simp_tac (HOL_ss addsimps non_add_bin_simps@mult_minus_simps))
-     THEN ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@
+     THEN ALLGOALS (simp_tac (num_ss addsimps non_add_bin_simps@mult_minus_simps))
+     THEN ALLGOALS (simp_tac (num_ss addsimps minus_from_mult_simps@
                                               add_ac@mult_ac))
   val numeral_simp_tac  = ALLGOALS
                     (simp_tac (HOL_ss addsimps add_0s@bin_simps))
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Integ/presburger.ML	Thu Jul 01 12:29:53 2004 +0200
@@ -120,9 +120,9 @@
    ("HOL.max", nT --> nT --> nT),
    ("HOL.min", nT --> nT --> nT),
 
-   ("Numeral.bin.Bit", binT --> bT --> binT),
-   ("Numeral.bin.Pls", binT),
-   ("Numeral.bin.Min", binT),
+   ("Numeral.Bit", binT --> bT --> binT),
+   ("Numeral.Pls", binT),
+   ("Numeral.Min", binT),
    ("Numeral.number_of", binT --> iT),
    ("Numeral.number_of", binT --> nT),
    ("0", nT),
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/IsaMakefile	Thu Jul 01 12:29:53 2004 +0200
@@ -84,14 +84,14 @@
   Datatype.thy Datatype_Universe.ML Datatype_Universe.thy \
   Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
   Fun.thy Gfp.ML Gfp.thy Hilbert_Choice.thy HOL.ML \
-  HOL.thy HOL_lemmas.ML Inductive.thy Infinite_Set.thy Integ/Bin.thy \
+  HOL.thy HOL_lemmas.ML Inductive.thy Infinite_Set.thy Integ/Numeral.thy \
   Integ/cooper_dec.ML Integ/cooper_proof.ML \
   Integ/Equiv.thy Integ/IntArith.thy Integ/IntDef.thy \
   Integ/IntDiv.thy Integ/NatBin.thy Integ/NatSimprocs.thy Integ/Parity.thy \
   Integ/int_arith1.ML Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
   Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
   Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
-  Nat.thy NatArith.ML NatArith.thy Numeral.thy \
+  Nat.thy NatArith.ML NatArith.thy \
   Power.thy PreList.thy Product_Type.ML Product_Type.thy \
   Refute.thy ROOT.ML \
   Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Library/Word.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -378,13 +378,14 @@
 
 constdefs
   bv_to_nat :: "bit list => int"
-  "bv_to_nat bv == number_of (foldl (%bn b. bn BIT (b = \<one>)) bin.Pls bv)"
+  "bv_to_nat bv == number_of (foldl (%bn b. bn BIT (b = \<one>)) Numeral.Pls bv)"
 
 lemma [simp]: "bv_to_nat [] = 0"
   by (simp add: bv_to_nat_def)
 
-lemma pos_number_of: "(0::int)\<le> number_of w ==> number_of (w BIT b) = (2::int) * number_of w + (if b then 1 else 0)"
-  by (induct w,auto,simp add: iszero_def)
+lemma pos_number_of:
+     "number_of (w BIT b) = (2::int) * number_of w + (if b then 1 else 0)"
+by (simp add: mult_2) 
 
 lemma bv_to_nat_helper [simp]: "bv_to_nat (b # bs) = bitval b * 2 ^ length bs + bv_to_nat bs"
 proof -
@@ -393,26 +394,24 @@
     by (simp add: bv_to_nat'_def)
   have [rule_format]: "\<forall> base bs. (0::int) \<le> number_of base --> (\<forall> b. bv_to_nat' base (b # bs) = bv_to_nat' (base BIT (b = \<one>)) bs)"
     by (simp add: bv_to_nat'_def)
-  have helper [rule_format]: "\<forall> base. (0::int) \<le> number_of base --> bv_to_nat' base bs = number_of base * 2 ^ length bs + bv_to_nat' bin.Pls bs"
+  have helper [rule_format]: "\<forall> base. (0::int) \<le> number_of base --> bv_to_nat' base bs = number_of base * 2 ^ length bs + bv_to_nat' Numeral.Pls bs"
   proof (induct bs,simp add: bv_to_nat'_def,clarify)
     fix x xs base
-    assume ind [rule_format]: "\<forall> base. (0::int) \<le> number_of base --> bv_to_nat' base xs = number_of base * 2 ^ length xs + bv_to_nat' bin.Pls xs"
+    assume ind [rule_format]: "\<forall> base. (0::int) \<le> number_of base --> bv_to_nat' base xs = number_of base * 2 ^ length xs + bv_to_nat' Numeral.Pls xs"
     assume base_pos: "(0::int) \<le> number_of base"
     def qq == "number_of base::int"
-    show "bv_to_nat' base (x # xs) = number_of base * 2 ^ (length (x # xs)) + bv_to_nat' bin.Pls (x # xs)"
+    show "bv_to_nat' base (x # xs) = number_of base * 2 ^ (length (x # xs)) + bv_to_nat' Numeral.Pls (x # xs)"
       apply (unfold bv_to_nat'_def)
       apply (simp only: foldl.simps)
       apply (fold bv_to_nat'_def)
       apply (subst ind [of "base BIT (x = \<one>)"])
       using base_pos
       apply simp
-      apply (subst ind [of "bin.Pls BIT (x = \<one>)"])
+      apply (subst ind [of "Numeral.Pls BIT (x = \<one>)"])
       apply simp
       apply (subst pos_number_of [of "base" "x = \<one>"])
       using base_pos
-      apply simp
-      apply (subst pos_number_of [of "bin.Pls" "x = \<one>"])
-      apply simp
+      apply (subst pos_number_of [of "Numeral.Pls" "x = \<one>"])
       apply (fold qq_def)
       apply (simp add: ring_distrib)
       done
@@ -2859,14 +2858,15 @@
 
 lemmas [simp] = length_nat_non0
 
-lemma "nat_to_bv (number_of bin.Pls) = []"
+lemma "nat_to_bv (number_of Numeral.Pls) = []"
   by simp
 
+(***NO LONGER WORKS
 consts
   fast_nat_to_bv_helper :: "bin => bit list => bit list"
 
 primrec
-  fast_nat_to_bv_Pls: "fast_nat_to_bv_helper bin.Pls res = res"
+  fast_nat_to_bv_Pls: "fast_nat_to_bv_helper Numeral.Pls res = res"
   fast_nat_to_bv_Bit: "fast_nat_to_bv_helper (w BIT b) res = fast_nat_to_bv_helper w ((if b then \<one> else \<zero>) # res)"
 
 lemma fast_nat_to_bv_def:
@@ -2889,7 +2889,7 @@
       by (simp add: qq_def)
     with posbb
     show "\<forall> l. norm_unsigned (nat_to_bv_helper (number_of (bin BIT b)) l) = norm_unsigned (fast_nat_to_bv_helper (bin BIT b) l)"
-      apply (subst pos_number_of,simp)
+      apply (subst pos_number_of)
       apply safe
       apply (fold qq_def)
       apply (cases "qq = 0")
@@ -2938,6 +2938,8 @@
 declare fast_nat_to_bv_Bit [simp del]
 declare fast_nat_to_bv_Bit0 [simp]
 declare fast_nat_to_bv_Bit1 [simp]
+****)
+
 
 consts
   fast_bv_to_nat_helper :: "[bit list, bin] => bin"
@@ -2952,13 +2954,13 @@
 lemma fast_bv_to_nat_Cons1: "fast_bv_to_nat_helper (\<one>#bs) bin = fast_bv_to_nat_helper bs (bin BIT True)"
   by simp
 
-lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs bin.Pls)"
+lemma fast_bv_to_nat_def: "bv_to_nat bs == number_of (fast_bv_to_nat_helper bs Numeral.Pls)"
 proof (simp add: bv_to_nat_def)
   have "\<forall> bin. (foldl (%bn b. bn BIT (b = \<one>)) bin bs) = (fast_bv_to_nat_helper bs bin)"
     apply (induct bs,simp)
     apply (case_tac a,simp_all)
     done
-  thus "number_of (foldl (%bn b. bn BIT (b = \<one>)) bin.Pls bs) == number_of (fast_bv_to_nat_helper bs bin.Pls)::int"
+  thus "number_of (foldl (%bn b. bn BIT (b = \<one>)) Numeral.Pls bs) == number_of (fast_bv_to_nat_helper bs Numeral.Pls)::int"
     by simp
 qed
 
@@ -2988,12 +2990,4 @@
 lemma [code]: "bv_to_nat bs = list_rec (0::int) (\<lambda>b bs n. bitval b * 2 ^ length bs + n) bs"
   by (induct bs,simp_all add: bv_to_nat_helper)
 
-text {* The following can be added for speedup, but depends on the
-exact definition of division and modulo of the ML compiler for soundness. *}
-
-(*
-consts_code "op div" ("'('(_') div '(_')')")
-consts_code "op mod" ("'('(_') mod '(_')')")
-*)
-
 end
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Library/word_setup.ML
--- a/src/HOL/Library/word_setup.ML	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Library/word_setup.ML	Thu Jul 01 12:29:53 2004 +0200
@@ -1,6 +1,8 @@
 (*  Title:      HOL/Library/word_setup.ML
     ID:         $Id$
     Author:     Sebastian Skalberg (TU Muenchen)
+
+comments containing lcp are the removal of fast_bv_of_nat.
 *)
 
 local
@@ -10,9 +12,9 @@
     fun is_const_bit (Const("Word.bit.Zero",_)) = true
       | is_const_bit (Const("Word.bit.One",_)) = true
       | is_const_bit _ = false
-    fun num_is_usable (Const("Numeral.bin.Pls",_)) = true
-      | num_is_usable (Const("Numeral.bin.Min",_)) = false
-      | num_is_usable (Const("Numeral.bin.Bit",_) $ w $ b) =
+    fun num_is_usable (Const("Numeral.Pls",_)) = true
+      | num_is_usable (Const("Numeral.Min",_)) = false
+      | num_is_usable (Const("Numeral.Bit",_) $ w $ b) =
 	num_is_usable w andalso is_const_bool b
       | num_is_usable _ = false
     fun vec_is_usable (Const("List.list.Nil",_)) = true
@@ -21,22 +23,22 @@
       | vec_is_usable _ = false
     fun add_word thy =
 	let
-	    val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"
+ (*lcp**	    val fast1_th = PureThy.get_thm thy "Word.fast_nat_to_bv_def"**)
 	    val fast2_th = PureThy.get_thm thy "Word.fast_bv_to_nat_def"
-	    fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
+ (*lcp**	    fun f sg thms (Const("Word.nat_to_bv",_) $ (Const("Numeral.number_of",_) $ t)) =
 		if num_is_usable t
 		then Some (Drule.cterm_instantiate [(cterm_of sg (Var(("w",0),Type("Numeral.bin",[]))),cterm_of sg t)] fast1_th)
 		else None
-	      | f _ _ _ = None
+	      | f _ _ _ = None **)
 	    fun g sg thms (Const("Word.bv_to_nat",_) $ (t as (Const("List.list.Cons",_) $ _ $ _))) =
 		if vec_is_usable t
 		then Some (Drule.cterm_instantiate [(cterm_of sg (Var(("bs",0),Type("List.list",[Type("Word.bit",[])]))),cterm_of sg t)] fast2_th)
 		else None
 	      | g _ _ _ = None
-	    val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of ?w)"] f
+  (*lcp**	    val simproc1 = Simplifier.simproc (sign_of thy) "nat_to_bv" ["Word.nat_to_bv (number_of ?w)"] f ***)
 	    val simproc2 = Simplifier.simproc (sign_of thy) "bv_to_nat" ["Word.bv_to_nat (?x # ?xs)"] g
 	in
-	    Simplifier.change_simpset_of (op addsimprocs) [simproc1,simproc2] thy
+	    Simplifier.change_simpset_of (op addsimprocs) [(*lcp*simproc1,**)simproc2] thy
 	end
 in
 val setup_word = [add_word]
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Wed Jun 30 14:04:58 2004 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,195 +0,0 @@
-(*  Title:      HOL/Numeral.thy
-    ID:         $Id$
-    Author:     Larry Paulson and Markus Wenzel
-
-Generic numerals represented as twos-complement bit strings.
-*)
-
-theory Numeral = Datatype
-files "Tools/numeral_syntax.ML":
-
-text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
-   Only qualified access bin.Pls and bin.Min is allowed.
-   We do not hide Bit because we need the BIT infix syntax.*}
-
-text{*A number can have multiple representations, namely leading Falses with
-sign @{term Pls} and leading Trues with sign @{term Min}.
-See @{text "ZF/Integ/twos-compl.ML"}, function @{text int_of_binary},
-for the numerical interpretation.
-
-The representation expects that @{text "(m mod 2)"} is 0 or 1,
-even if m is negative;
-For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
-@{text "-5 = (-3)*2 + 1"}.
-*}
-
-datatype
-  bin = Pls  --{*Plus: Stands for an infinite string of leading Falses*}
-      | Min --{*Minus: Stands for an infinite string of leading Trues*}
-      | Bit bin bool    (infixl "BIT" 90)
-
-axclass
-  number < type  -- {* for numeric types: nat, int, real, \dots *}
-
-consts
-  number_of :: "bin => 'a::number"
-
-syntax
-  "_Numeral" :: "num_const => 'a"    ("_")
-  Numeral0 :: 'a
-  Numeral1 :: 'a
-
-translations
-  "Numeral0" == "number_of bin.Pls"
-  "Numeral1" == "number_of (bin.Pls BIT True)"
-
-
-setup NumeralSyntax.setup
-
-syntax (xsymbols)
-  "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
-syntax (HTML output)
-  "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
-syntax (output)
-  "_square" :: "'a => 'a"  ("(_ ^/ 2)" [81] 80)
-translations
-  "x\<twosuperior>" == "x^2"
-  "x\<twosuperior>" <= "x^(2::nat)"
-
-
-lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
-  -- {* Unfold all @{text let}s involving constants *}
-  by (simp add: Let_def)
-
-lemma Let_0 [simp]: "Let 0 f == f 0"
-  by (simp add: Let_def)
-
-lemma Let_1 [simp]: "Let 1 f == f 1"
-  by (simp add: Let_def)
-
-
-consts
-  NCons     :: "[bin,bool]=>bin"
-  bin_succ  :: "bin=>bin"
-  bin_pred  :: "bin=>bin"
-  bin_minus :: "bin=>bin"
-  bin_add   :: "[bin,bin]=>bin"
-  bin_mult  :: "[bin,bin]=>bin"
-
-text{*@{term NCons} inserts a bit, suppressing leading 0s and 1s*}
-primrec
-  NCons_Pls:  "NCons bin.Pls b = (if b then (bin.Pls BIT b) else bin.Pls)"
-  NCons_Min:  "NCons bin.Min b = (if b then bin.Min else (bin.Min BIT b))"
-  NCons_BIT:  "NCons (w BIT x) b = (w BIT x) BIT b"
-
-
-primrec
-  bin_succ_Pls: "bin_succ bin.Pls = bin.Pls BIT True"
-  bin_succ_Min: "bin_succ bin.Min = bin.Pls"
-  bin_succ_BIT: "bin_succ(w BIT x) =
-  	            (if x then bin_succ w BIT False
-	                  else NCons w True)"
-
-primrec
-  bin_pred_Pls: "bin_pred bin.Pls = bin.Min"
-  bin_pred_Min: "bin_pred bin.Min = bin.Min BIT False"
-  bin_pred_BIT: "bin_pred(w BIT x) =
-	            (if x then NCons w False
-		          else (bin_pred w) BIT True)"
-
-primrec
-  bin_minus_Pls: "bin_minus bin.Pls = bin.Pls"
-  bin_minus_Min: "bin_minus bin.Min = bin.Pls BIT True"
-  bin_minus_BIT: "bin_minus(w BIT x) =
-	             (if x then bin_pred (NCons (bin_minus w) False)
-		           else bin_minus w BIT False)"
-
-primrec
-  bin_add_Pls: "bin_add bin.Pls w = w"
-  bin_add_Min: "bin_add bin.Min w = bin_pred w"
-  bin_add_BIT:
-    "bin_add (v BIT x) w =
-       (case w of bin.Pls => v BIT x
-                | bin.Min => bin_pred (v BIT x)
-                | (w BIT y) =>
-      	            NCons (bin_add v (if (x & y) then bin_succ w else w))
-	                  (x~=y))"
-
-primrec
-  bin_mult_Pls: "bin_mult bin.Pls w = bin.Pls"
-  bin_mult_Min: "bin_mult bin.Min w = bin_minus w"
-  bin_mult_BIT: "bin_mult (v BIT x) w =
-	            (if x then (bin_add (NCons (bin_mult v w) False) w)
-	                  else (NCons (bin_mult v w) False))"
-
-
-subsection{*Extra rules for @{term bin_succ}, @{term bin_pred}, 
-  @{term bin_add} and @{term bin_mult}*}
-
-lemma NCons_Pls_0: "NCons bin.Pls False = bin.Pls"
-by simp
-
-lemma NCons_Pls_1: "NCons bin.Pls True = bin.Pls BIT True"
-by simp
-
-lemma NCons_Min_0: "NCons bin.Min False = bin.Min BIT False"
-by simp
-
-lemma NCons_Min_1: "NCons bin.Min True = bin.Min"
-by simp
-
-lemma bin_succ_1: "bin_succ(w BIT True) = (bin_succ w) BIT False"
-by simp
-
-lemma bin_succ_0: "bin_succ(w BIT False) =  NCons w True"
-by simp
-
-lemma bin_pred_1: "bin_pred(w BIT True) = NCons w False"
-by simp
-
-lemma bin_pred_0: "bin_pred(w BIT False) = (bin_pred w) BIT True"
-by simp
-
-lemma bin_minus_1: "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)"
-by simp
-
-lemma bin_minus_0: "bin_minus(w BIT False) = (bin_minus w) BIT False"
-by simp
-
-
-subsection{*Binary Addition and Multiplication:
-         @{term bin_add} and @{term bin_mult}*}
-
-lemma bin_add_BIT_11:
-     "bin_add (v BIT True) (w BIT True) =
-     NCons (bin_add v (bin_succ w)) False"
-by simp
-
-lemma bin_add_BIT_10:
-     "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True"
-by simp
-
-lemma bin_add_BIT_0:
-     "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"
-by auto
-
-lemma bin_add_Pls_right: "bin_add w bin.Pls = w"
-by (induct_tac "w", auto)
-
-lemma bin_add_Min_right: "bin_add w bin.Min = bin_pred w"
-by (induct_tac "w", auto)
-
-lemma bin_add_BIT_BIT:
-     "bin_add (v BIT x) (w BIT y) =
-     NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
-by simp
-
-lemma bin_mult_1:
-     "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"
-by simp
-
-lemma bin_mult_0: "bin_mult (v BIT False) w = NCons (bin_mult v w) False"
-by simp
-
-
-end
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Presburger.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -969,7 +969,7 @@
 theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
   by simp
 
-theorem number_of2: "(0::int) <= number_of bin.Pls" by simp
+theorem number_of2: "(0::int) <= Numeral0" by simp
 
 theorem Suc_plus1: "Suc n = n + 1" by simp
 
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Real/PReal.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -705,7 +705,7 @@
       from preal_nonempty [OF A]
       show ?case  by force 
     case (Suc k)
-      from this obtain b where "b \<in> A" "b + of_int (int k) * u \<in> A" ..
+      from this obtain b where "b \<in> A" "b + of_nat k * u \<in> A" ..
       hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems)
       thus ?case by (force simp add: left_distrib add_ac prems) 
   qed
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Real/Rational.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -674,25 +674,12 @@
 
 instance rat :: number ..
 
-primrec  -- {* the type constraint is essential! *}
-  number_of_Pls: "number_of bin.Pls = 0"
-  number_of_Min: "number_of bin.Min = - (1::rat)"
-  number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
-                                       (number_of w) + (number_of w)"
-
-declare number_of_Pls [simp del]
-        number_of_Min [simp del]
-        number_of_BIT [simp del]
+defs (overloaded)
+  rat_number_of_def: "(number_of w :: rat) == of_int (Rep_Bin w)"
+    --{*the type constraint is essential!*}
 
 instance rat :: number_ring
-proof
-  show "Numeral0 = (0::rat)" by (rule number_of_Pls)
-  show "-1 = - (1::rat)" by (rule number_of_Min)
-  fix w :: bin and x :: bool
-  show "(number_of (w BIT x) :: rat) =
-        (if x then 1 else 0) + number_of w + number_of w"
-    by (rule number_of_BIT)
-qed
+by (intro_classes, simp add: rat_number_of_def) 
 
 declare diff_rat_def [symmetric]
 
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Real/RealDef.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -732,25 +732,12 @@
 
 instance real :: number ..
 
-primrec (*the type constraint is essential!*)
-  number_of_Pls: "number_of bin.Pls = 0"
-  number_of_Min: "number_of bin.Min = - (1::real)"
-  number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
-	                               (number_of w) + (number_of w)"
-
-declare number_of_Pls [simp del]
-        number_of_Min [simp del]
-        number_of_BIT [simp del]
+defs (overloaded)
+  real_number_of_def: "(number_of w :: real) == of_int (Rep_Bin w)"
+    --{*the type constraint is essential!*}
 
 instance real :: number_ring
-proof
-  show "Numeral0 = (0::real)" by (rule number_of_Pls)
-  show "-1 = - (1::real)" by (rule number_of_Min)
-  fix w :: bin and x :: bool
-  show "(number_of (w BIT x) :: real) =
-        (if x then 1 else 0) + number_of w + number_of w"
-    by (rule number_of_BIT)
-qed
+by (intro_classes, simp add: real_number_of_def) 
 
 
 text{*Collapse applications of @{term real} to @{term number_of}*}
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Thu Jul 01 12:29:53 2004 +0200
@@ -120,9 +120,9 @@
    ("HOL.max", nT --> nT --> nT),
    ("HOL.min", nT --> nT --> nT),
 
-   ("Numeral.bin.Bit", binT --> bT --> binT),
-   ("Numeral.bin.Pls", binT),
-   ("Numeral.bin.Min", binT),
+   ("Numeral.Bit", binT --> bT --> binT),
+   ("Numeral.Pls", binT),
+   ("Numeral.Min", binT),
    ("Numeral.number_of", binT --> iT),
    ("Numeral.number_of", binT --> nT),
    ("0", nT),
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Thu Jul 01 12:29:53 2004 +0200
@@ -28,8 +28,8 @@
   | prefix_len pred (x :: xs) =
       if pred x then 1 + prefix_len pred xs else 0;
 
-fun bin_of (Const ("bin.Pls", _)) = []
-  | bin_of (Const ("bin.Min", _)) = [~1]
+fun bin_of (Const ("Numeral.Pls", _)) = []
+  | bin_of (Const ("Numeral.Min", _)) = [~1]
   | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
   | bin_of _ = raise Match;
 
@@ -70,7 +70,7 @@
 (* theory setup *)
 
 val setup =
- [Theory.hide_consts false ["Numeral.bin.Pls", "Numeral.bin.Min"],
+ [Theory.hide_consts false ["Numeral.Pls", "Numeral.Min"],
   Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
   Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
 
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/ex/BinEx.thy
--- a/src/HOL/ex/BinEx.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/ex/BinEx.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -387,115 +387,7 @@
   by simp
 
 
-subsection {* Normal form of bit strings *}
-
-text {*
-  Definition of normal form for proving that binary arithmetic on
-  normalized operands yields normalized results.  Normal means no
-  leading 0s on positive numbers and no leading 1s on negatives.
-*}
-
-consts normal :: "bin set"
-inductive normal
-  intros
-    Pls [simp]: "bin.Pls: normal"
-    Min [simp]: "bin.Min: normal"
-    BIT_F [simp]: "w: normal ==> w \<noteq> bin.Pls ==> w BIT False : normal"
-    BIT_T [simp]: "w: normal ==> w \<noteq> bin.Min ==> w BIT True : normal"
-
-text {*
-  \medskip Binary arithmetic on normalized operands yields normalized
-  results.
-*}
-
-lemma normal_BIT_I [simp]: "w BIT b \<in> normal ==> w BIT b BIT c \<in> normal"
-  apply (case_tac c)
-   apply auto
-  done
-
-lemma normal_BIT_D: "w BIT b \<in> normal ==> w \<in> normal"
-  apply (erule normal.cases)
-     apply auto
-  done
-
-lemma NCons_normal [simp]: "w \<in> normal ==> NCons w b \<in> normal"
-  apply (induct w)
-    apply (auto simp add: NCons_Pls NCons_Min)
-  done
-
-lemma NCons_True: "NCons w True \<noteq> bin.Pls"
-  apply (induct w)
-    apply auto
-  done
-
-lemma NCons_False: "NCons w False \<noteq> bin.Min"
-  apply (induct w)
-    apply auto
-  done
-
-lemma bin_succ_normal [simp]: "w \<in> normal ==> bin_succ w \<in> normal"
-  apply (erule normal.induct)
-     apply (case_tac [4] w)
-  apply (auto simp add: NCons_True bin_succ_BIT)
-  done
-
-lemma bin_pred_normal [simp]: "w \<in> normal ==> bin_pred w \<in> normal"
-  apply (erule normal.induct)
-     apply (case_tac [3] w)
-  apply (auto simp add: NCons_False bin_pred_BIT)
-  done
-
-lemma bin_add_normal [rule_format]:
-  "w \<in> normal --> (\<forall>z. z \<in> normal --> bin_add w z \<in> normal)"
-  apply (induct w)
-    apply simp
-   apply simp
-  apply (rule impI)
-  apply (rule allI)
-  apply (induct_tac z)
-    apply (simp_all add: bin_add_BIT)
-  apply (safe dest!: normal_BIT_D)
-    apply simp_all
-  done
-
-lemma normal_Pls_eq_0: "w \<in> normal ==> (w = bin.Pls) = (number_of w = (0::int))"
-  apply (erule normal.induct)
-     apply auto
-  done
-
-lemma bin_minus_normal: "w \<in> normal ==> bin_minus w \<in> normal"
-  apply (erule normal.induct)
-     apply (simp_all add: bin_minus_BIT)
-  apply (rule normal.intros)
-   apply assumption
-  apply (simp add: normal_Pls_eq_0)
-  apply (simp only: number_of_minus zminus_0 iszero_def
-                    minus_equation_iff [of _ "0"])
-  done
-
-(*The previous command should have finished the proof but the lin-arith
-procedure at the end of simplificatioon fails.
-Problem: lin-arith correctly derives the contradictory thm
-"number_of w + 1 + - 0 \<le> 0 + number_of w"  [..]
-which its local simplification setup should turn into False.
-But on the way we get
-
-Procedure "int_add_eval_numerals" produced rewrite rule:
-number_of ?v3 + 1 \<equiv> number_of (bin_add ?v3 (bin.Pls BIT True))
-
-and eventually we arrive not at false but at
-
-"\<not> neg (number_of (bin_add w (bin_minus (bin_add w (bin.Pls BIT True)))))"
-
-The simplification with eq_commute should now be obsolete.
-*)
-
-lemma bin_mult_normal [rule_format]:
-    "w \<in> normal ==> z \<in> normal --> bin_mult w z \<in> normal"
-  apply (erule normal.induct)
-     apply (simp_all add: bin_minus_normal bin_mult_BIT)
-  apply (safe dest!: normal_BIT_D)
-  apply (simp add: bin_add_normal)
-  done
+text{*The proofs about arithmetic yielding normal forms have been deleted:
+ they are irrelevant with the new treatment of numerals.*}
 
 end
diff -r 28fa57b57209 -r 34264f5e4691 src/HOL/hologic.ML
--- a/src/HOL/hologic.ML	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/hologic.ML	Thu Jul 01 12:29:53 2004 +0200
@@ -282,9 +282,9 @@
 
 val binT = Type ("Numeral.bin", []);
 
-val pls_const = Const ("Numeral.bin.Pls", binT)
-and min_const = Const ("Numeral.bin.Min", binT)
-and bit_const = Const ("Numeral.bin.Bit", [binT, boolT] ---> binT);
+val pls_const = Const ("Numeral.Pls", binT)
+and min_const = Const ("Numeral.Min", binT)
+and bit_const = Const ("Numeral.Bit", [binT, boolT] ---> binT);
 
 fun number_of_const T = Const ("Numeral.number_of", binT --> T);
 
@@ -296,9 +296,9 @@
   | dest_bit (Const ("True", _)) = 1
   | dest_bit t = raise TERM("dest_bit", [t]);
 
-fun bin_of (Const ("Numeral.bin.Pls", _)) = []
-  | bin_of (Const ("Numeral.bin.Min", _)) = [~1]
-  | bin_of (Const ("Numeral.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
+fun bin_of (Const ("Numeral.Pls", _)) = []
+  | bin_of (Const ("Numeral.Min", _)) = [~1]
+  | bin_of (Const ("Numeral.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
   | bin_of t = raise TERM("bin_of", [t]);
 
 val dest_binum = int_of o bin_of;