src/HOL/Integ/int_factor_simprocs.ML
changeset 16973 b2a894562b8f
parent 15271 3c32a26510c4
child 17877 67d5ab1cb0d8
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Mon Aug 01 19:20:25 2005 +0200
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Mon Aug 01 19:20:26 2005 +0200
     1.3 @@ -42,14 +42,16 @@
     1.4    struct
     1.5    val mk_coeff          = mk_coeff
     1.6    val dest_coeff        = dest_coeff 1
     1.7 -  val trans_tac         = trans_tac
     1.8 -  val norm_tac =
     1.9 -     ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps @ mult_1s))
    1.10 -     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_minus_simps))
    1.11 -     THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
    1.12 -  val numeral_simp_tac  =
    1.13 -         ALLGOALS (simp_tac (HOL_ss addsimps rel_number_of@bin_simps))
    1.14 -  val simplify_meta_eq  = 
    1.15 +  val trans_tac         = fn _ => trans_tac
    1.16 +  fun norm_tac ss =
    1.17 +    let val HOL_ss' = Simplifier.inherit_bounds ss HOL_ss in
    1.18 +      ALLGOALS (simp_tac (HOL_ss' addsimps minus_from_mult_simps @ mult_1s))
    1.19 +      THEN ALLGOALS (simp_tac (HOL_ss' addsimps bin_simps@mult_minus_simps))
    1.20 +      THEN ALLGOALS (simp_tac (HOL_ss' addsimps mult_ac))
    1.21 +    end
    1.22 +  fun numeral_simp_tac ss =
    1.23 +    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps rel_number_of @ bin_simps))
    1.24 +  val simplify_meta_eq = 
    1.25  	Int_Numeral_Simprocs.simplify_meta_eq
    1.26  	     [add_0, add_0_right,
    1.27  	      mult_zero_left, mult_zero_right, mult_1, mult_1_right];
    1.28 @@ -235,8 +237,8 @@
    1.29      Int_Numeral_Simprocs.simplify_meta_eq  
    1.30         [mult_1_left, mult_1_right, zdiv_1, numeral_1_eq_1];
    1.31  
    1.32 -fun cancel_simplify_meta_eq cancel_th th =
    1.33 -    simplify_one (([th, cancel_th]) MRS trans);
    1.34 +fun cancel_simplify_meta_eq cancel_th ss th =
    1.35 +    simplify_one ss (([th, cancel_th]) MRS trans);
    1.36  
    1.37  (*At present, long_mk_prod creates Numeral1, so this requires the axclass
    1.38    number_ring*)
    1.39 @@ -247,8 +249,9 @@
    1.40    val mk_coeff          = mk_coeff
    1.41    val dest_coeff        = dest_coeff
    1.42    val find_first        = find_first []
    1.43 -  val trans_tac         = trans_tac
    1.44 -  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
    1.45 +  val trans_tac         = fn _ => trans_tac
    1.46 +  fun norm_tac ss =
    1.47 +    ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps mult_1s @ mult_ac))
    1.48    end;
    1.49  
    1.50  (*mult_cancel_left requires an ordered comm_ring_1, such as int. The version in