fixed bugs in the setup of arithmetic procedures
authorpaulson
Tue Mar 02 11:06:37 2004 +0100 (2004-03-02)
changeset 14426de890c247b38
parent 14425 0a76d4633bb6
child 14427 cea7d2f76112
fixed bugs in the setup of arithmetic procedures
src/HOL/Integ/int_factor_simprocs.ML
src/HOL/Real/RealDef.thy
src/HOL/Real/real_arith.ML
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Tue Mar 02 11:05:55 2004 +0100
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue Mar 02 11:06:37 2004 +0100
     1.3 @@ -139,9 +139,9 @@
     1.4        "(l::'a::{field,number_ring}) = m * n"],
     1.5       FieldEqCancelNumeralFactor.proc),
     1.6      ("field_cancel_numeral_factor",
     1.7 -     ["((l::'a::{field,number_ring}) * m) / n",
     1.8 -      "(l::'a::{field,number_ring}) / (m * n)",
     1.9 -      "((number_of v)::'a::{field,number_ring}) / (number_of w)"],
    1.10 +     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
    1.11 +      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
    1.12 +      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
    1.13       FieldDivCancelNumeralFactor.proc)]
    1.14  
    1.15  end;
    1.16 @@ -236,6 +236,8 @@
    1.17          [mult_1, mult_1_right]
    1.18          (([th, cancel_th]) MRS trans);
    1.19  
    1.20 +(*At present, long_mk_prod creates Numeral1, so this requires the axclass
    1.21 +  number_ring*)
    1.22  structure CancelFactorCommon =
    1.23    struct
    1.24    val mk_sum            = long_mk_prod
    1.25 @@ -292,13 +294,17 @@
    1.26    val simplify_meta_eq  = cancel_simplify_meta_eq mult_divide_cancel_eq_if
    1.27  );
    1.28  
    1.29 +(*The number_ring class is necessary because the simprocs refer to the 
    1.30 +  binary number 1.  FIXME: probably they could use 1 instead.*)
    1.31  val field_cancel_factor =
    1.32    map Bin_Simprocs.prep_simproc
    1.33     [("field_eq_cancel_factor",
    1.34 -     ["(l::'a::field) * m = n", "(l::'a::field) = m * n"], 
    1.35 +     ["(l::'a::{field,number_ring}) * m = n",
    1.36 +      "(l::'a::{field,number_ring}) = m * n"], 
    1.37       FieldEqCancelFactor.proc),
    1.38      ("field_divide_cancel_factor",
    1.39 -     ["((l::'a::field) * m) / n", "(l::'a::field) / (m * n)"],
    1.40 +     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
    1.41 +      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)"],
    1.42       FieldDivideCancelFactor.proc)];
    1.43  
    1.44  end;
     2.1 --- a/src/HOL/Real/RealDef.thy	Tue Mar 02 11:05:55 2004 +0100
     2.2 +++ b/src/HOL/Real/RealDef.thy	Tue Mar 02 11:06:37 2004 +0100
     2.3 @@ -805,17 +805,8 @@
     2.4  lemma real_of_int_real_of_nat: "real (int n) = real n"
     2.5  by (simp add: real_of_nat_def real_of_int_def int_eq_of_nat)
     2.6  
     2.7 -
     2.8 -text{*Still needed for binary arithmetic*}
     2.9 -lemma real_of_nat_real_of_int: "~neg z ==> real (nat z) = real z"
    2.10 -proof (simp add: not_neg_eq_ge_0 real_of_nat_def real_of_int_def)
    2.11 -  assume "0 \<le> z"
    2.12 -  hence eq: "of_nat (nat z) = z" 
    2.13 -    by (simp add: nat_0_le int_eq_of_nat[symmetric]) 
    2.14 -  have "of_nat (nat z) = of_int (of_nat (nat z))" by simp
    2.15 -  also have "... = of_int z" by (simp add: eq)
    2.16 -  finally show "of_nat (nat z) = of_int z" .
    2.17 -qed
    2.18 +lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n"
    2.19 +by (simp add: real_of_int_def real_of_nat_def)
    2.20  
    2.21  
    2.22  
     3.1 --- a/src/HOL/Real/real_arith.ML	Tue Mar 02 11:05:55 2004 +0100
     3.2 +++ b/src/HOL/Real/real_arith.ML	Tue Mar 02 11:06:37 2004 +0100
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      HOL/Real/real_arith0.ML
     3.5 +(*  Title:      HOL/Real/real_arith.ML
     3.6      ID:         $Id$
     3.7      Author:     Tobias Nipkow, TU Muenchen
     3.8      Copyright   1999 TU Muenchen
     3.9 @@ -113,6 +113,7 @@
    3.10  val real_of_nat_ge_zero_cancel_iff = thm "real_of_nat_ge_zero_cancel_iff";
    3.11  val real_number_of = thm"real_number_of";
    3.12  val real_of_nat_number_of = thm"real_of_nat_number_of";
    3.13 +val real_of_int_of_nat_eq = thm"real_of_int_of_nat_eq";
    3.14  
    3.15  
    3.16  (****Instantiation of the generic linear arithmetic package****)
    3.17 @@ -130,7 +131,7 @@
    3.18  val simps = [real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, 
    3.19         real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add RS sym,
    3.20         real_of_int_minus RS sym, real_of_int_diff RS sym,
    3.21 -       real_of_int_mult RS sym,
    3.22 +       real_of_int_mult RS sym, real_of_int_of_nat_eq,
    3.23         real_of_nat_number_of, real_number_of];
    3.24  
    3.25  val int_inj_thms = [real_of_int_le_iff RS iffD2, real_of_int_less_iff RS iffD2,