src/HOL/Real/rat_arith.ML
changeset 14378 69c4d5997669
parent 14369 c50188fe6366
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Real/rat_arith.ML	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Real/rat_arith.ML	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -19,18 +19,6 @@
     1.4  val rat_number_of_def = thm "rat_number_of_def";
     1.5  val diff_rat_def = thm "diff_rat_def";
     1.6  
     1.7 -val rat_of_int_zero = thm "rat_of_int_zero";
     1.8 -val rat_of_int_one = thm "rat_of_int_one";
     1.9 -val rat_of_int_add_distrib = thm "rat_of_int_add_distrib";
    1.10 -val rat_of_int_minus_distrib = thm "rat_of_int_minus_distrib";
    1.11 -val rat_of_int_diff_distrib = thm "rat_of_int_diff_distrib";
    1.12 -val rat_of_int_mult_distrib = thm "rat_of_int_mult_distrib";
    1.13 -val rat_inject = thm "rat_inject";
    1.14 -val rat_of_int_zero_cancel = thm "rat_of_int_zero_cancel";
    1.15 -val rat_of_int_less_iff = thm "rat_of_int_less_iff";
    1.16 -val rat_of_int_le_iff = thm "rat_of_int_le_iff";
    1.17 -
    1.18 -val number_of_rat = thm "number_of_rat";
    1.19  val rat_numeral_0_eq_0 = thm "rat_numeral_0_eq_0";
    1.20  val rat_numeral_1_eq_1 = thm "rat_numeral_1_eq_1";
    1.21  val add_rat_number_of = thm "add_rat_number_of";
    1.22 @@ -615,9 +603,8 @@
    1.23  val simps = [True_implies_equals,
    1.24               inst "a" "(number_of ?v)" right_distrib,
    1.25               divide_1, times_divide_eq_right, times_divide_eq_left,
    1.26 -	     rat_of_int_zero, rat_of_int_one, rat_of_int_add_distrib,
    1.27 -	     rat_of_int_minus_distrib, rat_of_int_diff_distrib,
    1.28 -	     rat_of_int_mult_distrib, number_of_rat RS sym];
    1.29 +	     of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff,
    1.30 +	     of_int_mult, of_int_of_nat_eq, rat_number_of_def];
    1.31  
    1.32  in
    1.33  
    1.34 @@ -625,8 +612,11 @@
    1.35    "fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"]
    1.36    Fast_Arith.lin_arith_prover;
    1.37  
    1.38 -val int_inj_thms = [rat_of_int_le_iff RS iffD2, rat_of_int_less_iff RS iffD2,
    1.39 -                    rat_inject RS iffD2];
    1.40 +val nat_inj_thms = [of_nat_le_iff RS iffD2, of_nat_less_iff RS iffD2,
    1.41 +                    of_nat_eq_iff RS iffD2];
    1.42 +
    1.43 +val int_inj_thms = [of_int_le_iff RS iffD2, of_int_less_iff RS iffD2,
    1.44 +                    of_int_eq_iff RS iffD2];
    1.45  
    1.46  val rat_arith_setup =
    1.47   [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
    1.48 @@ -637,7 +627,8 @@
    1.49      simpset = simpset addsimps add_rules
    1.50                        addsimps simps
    1.51                        addsimprocs simprocs}),
    1.52 -  arith_inj_const ("Rational.rat", HOLogic.intT --> Rat_Numeral_Simprocs.ratT),
    1.53 +  arith_inj_const("IntDef.of_nat", HOLogic.natT --> Rat_Numeral_Simprocs.ratT),
    1.54 +  arith_inj_const("IntDef.of_int", HOLogic.intT --> Rat_Numeral_Simprocs.ratT),
    1.55    arith_discrete ("Rational.rat",false),
    1.56    Simplifier.change_simpset_of (op addsimprocs) [fast_rat_arith_simproc]];
    1.57