src/HOL/Integ/int_factor_simprocs.ML
changeset 14387 e96d5c42c4b0
parent 14378 69c4d5997669
child 14390 55fe71faadda
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Sat Feb 14 02:06:12 2004 +0100
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Sun Feb 15 10:46:37 2004 +0100
     1.3 @@ -31,9 +31,9 @@
     1.4    val dest_coeff        = dest_coeff 1
     1.5    val trans_tac         = trans_tac
     1.6    val norm_tac =
     1.7 -     ALLGOALS (simp_tac (HOL_ss addsimps int_minus_from_mult_simps@mult_1s))
     1.8 -     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@int_mult_minus_simps))
     1.9 -     THEN ALLGOALS (simp_tac (HOL_ss addsimps zmult_ac))
    1.10 +     ALLGOALS (simp_tac (HOL_ss addsimps minus_from_mult_simps@mult_1s))
    1.11 +     THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_minus_simps))
    1.12 +     THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
    1.13    val numeral_simp_tac  = ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
    1.14    val simplify_meta_eq  = simplify_meta_eq mult_1s
    1.15    end
    1.16 @@ -132,11 +132,6 @@
    1.17    open Int_Numeral_Simprocs
    1.18  in
    1.19  
    1.20 -
    1.21 -(*this version ALWAYS includes a trailing one*)
    1.22 -fun long_mk_prod []        = one
    1.23 -  | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
    1.24 -
    1.25  (*Find first term that matches u*)
    1.26  fun find_first past u []         = raise TERM("find_first", [])
    1.27    | find_first past u (t::terms) =
    1.28 @@ -147,7 +142,7 @@
    1.29  (*Final simplification: cancel + and *  *)
    1.30  fun cancel_simplify_meta_eq cancel_th th =
    1.31      Int_Numeral_Simprocs.simplify_meta_eq
    1.32 -        [zmult_1, zmult_1_right]
    1.33 +        [mult_1, mult_1_right]
    1.34          (([th, cancel_th]) MRS trans);
    1.35  
    1.36  structure CancelFactorCommon =
    1.37 @@ -158,9 +153,11 @@
    1.38    val dest_coeff        = dest_coeff
    1.39    val find_first        = find_first []
    1.40    val trans_tac         = trans_tac
    1.41 -  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@zmult_ac))
    1.42 +  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@mult_ac))
    1.43    end;
    1.44  
    1.45 +(*mult_cancel_left requires an ordered ring, such as int. The version in
    1.46 +  rat_arith.ML works for all fields.*)
    1.47  structure EqCancelFactor = ExtractCommonTermFun
    1.48   (open CancelFactorCommon
    1.49    val prove_conv = Bin_Simprocs.prove_conv
    1.50 @@ -169,6 +166,8 @@
    1.51    val simplify_meta_eq  = cancel_simplify_meta_eq mult_cancel_left
    1.52  );
    1.53  
    1.54 +(*int_mult_div_cancel_disj is for integer division (div). The version in
    1.55 +  rat_arith.ML works for all fields, using real division (/).*)
    1.56  structure DivideCancelFactor = ExtractCommonTermFun
    1.57   (open CancelFactorCommon
    1.58    val prove_conv = Bin_Simprocs.prove_conv