# HG changeset patch
# User paulson
# Date 1078221997 -3600
# Node ID de890c247b38775a6cdfcb61d2cccc231ef69d00
# Parent  0a76d4633bb6f2443e6526faf194cae59c1847e4
fixed bugs in the setup of arithmetic procedures

diff -r 0a76d4633bb6 -r de890c247b38 src/HOL/Integ/int_factor_simprocs.ML
--- a/src/HOL/Integ/int_factor_simprocs.ML	Tue Mar 02 11:05:55 2004 +0100
+++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue Mar 02 11:06:37 2004 +0100
@@ -139,9 +139,9 @@
       "(l::'a::{field,number_ring}) = m * n"],
      FieldEqCancelNumeralFactor.proc),
     ("field_cancel_numeral_factor",
-     ["((l::'a::{field,number_ring}) * m) / n",
-      "(l::'a::{field,number_ring}) / (m * n)",
-      "((number_of v)::'a::{field,number_ring}) / (number_of w)"],
+     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
+      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
+      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
      FieldDivCancelNumeralFactor.proc)]
 
 end;
@@ -236,6 +236,8 @@
         [mult_1, mult_1_right]
         (([th, cancel_th]) MRS trans);
 
+(*At present, long_mk_prod creates Numeral1, so this requires the axclass
+  number_ring*)
 structure CancelFactorCommon =
   struct
   val mk_sum            = long_mk_prod
@@ -292,13 +294,17 @@
   val simplify_meta_eq  = cancel_simplify_meta_eq mult_divide_cancel_eq_if
 );
 
+(*The number_ring class is necessary because the simprocs refer to the 
+  binary number 1.  FIXME: probably they could use 1 instead.*)
 val field_cancel_factor =
   map Bin_Simprocs.prep_simproc
    [("field_eq_cancel_factor",
-     ["(l::'a::field) * m = n", "(l::'a::field) = m * n"], 
+     ["(l::'a::{field,number_ring}) * m = n",
+      "(l::'a::{field,number_ring}) = m * n"], 
      FieldEqCancelFactor.proc),
     ("field_divide_cancel_factor",
-     ["((l::'a::field) * m) / n", "(l::'a::field) / (m * n)"],
+     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
+      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)"],
      FieldDivideCancelFactor.proc)];
 
 end;
diff -r 0a76d4633bb6 -r de890c247b38 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Tue Mar 02 11:05:55 2004 +0100
+++ b/src/HOL/Real/RealDef.thy	Tue Mar 02 11:06:37 2004 +0100
@@ -805,17 +805,8 @@
 lemma real_of_int_real_of_nat: "real (int n) = real n"
 by (simp add: real_of_nat_def real_of_int_def int_eq_of_nat)
 
-
-text{*Still needed for binary arithmetic*}
-lemma real_of_nat_real_of_int: "~neg z ==> real (nat z) = real z"
-proof (simp add: not_neg_eq_ge_0 real_of_nat_def real_of_int_def)
-  assume "0 \<le> z"
-  hence eq: "of_nat (nat z) = z" 
-    by (simp add: nat_0_le int_eq_of_nat[symmetric]) 
-  have "of_nat (nat z) = of_int (of_nat (nat z))" by simp
-  also have "... = of_int z" by (simp add: eq)
-  finally show "of_nat (nat z) = of_int z" .
-qed
+lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n"
+by (simp add: real_of_int_def real_of_nat_def)
 
 
 
diff -r 0a76d4633bb6 -r de890c247b38 src/HOL/Real/real_arith.ML
--- a/src/HOL/Real/real_arith.ML	Tue Mar 02 11:05:55 2004 +0100
+++ b/src/HOL/Real/real_arith.ML	Tue Mar 02 11:06:37 2004 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Real/real_arith0.ML
+(*  Title:      HOL/Real/real_arith.ML
     ID:         $Id$
     Author:     Tobias Nipkow, TU Muenchen
     Copyright   1999 TU Muenchen
@@ -113,6 +113,7 @@
 val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff";
 val real_number_of = thm"real_number_of";
 val real_of_nat_number_of = thm"real_of_nat_number_of";
+val real_of_int_of_nat_eq = thm"real_of_int_of_nat_eq";
 
 
 (****Instantiation of the generic linear arithmetic package****)
@@ -130,7 +131,7 @@
 val simps = [real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, 
        real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add RS sym,
        real_of_int_minus RS sym, real_of_int_diff RS sym,
-       real_of_int_mult RS sym,
+       real_of_int_mult RS sym, real_of_int_of_nat_eq,
        real_of_nat_number_of, real_number_of];
 
 val int_inj_thms = [real_of_int_le_iff RS iffD2, real_of_int_less_iff RS iffD2,