src/HOL/Integ/int_factor_simprocs.ML
changeset 14378 69c4d5997669
parent 14113 7b3513ba0f86
child 14387 e96d5c42c4b0
     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -5,25 +5,11 @@
     1.4  
     1.5  Factor cancellation simprocs for the integers.
     1.6  
     1.7 -This file can't be combined with int_arith1,2 because it requires IntDiv.thy.
     1.8 +This file can't be combined with int_arith1 because it requires IntDiv.thy.
     1.9  *)
    1.10  
    1.11  (** Factor cancellation theorems for "int" **)
    1.12  
    1.13 -Goal "!!k::int. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))";
    1.14 -by (stac zmult_zle_cancel1 1);
    1.15 -by Auto_tac;
    1.16 -qed "int_mult_le_cancel1";
    1.17 -
    1.18 -Goal "!!k::int. (k*m < k*n) = ((0 < k & m<n) | (k < 0 & n<m))";
    1.19 -by (stac zmult_zless_cancel1 1);
    1.20 -by Auto_tac;
    1.21 -qed "int_mult_less_cancel1";
    1.22 -
    1.23 -Goal "!!k::int. (k*m = k*n) = (k = 0 | m=n)";
    1.24 -by Auto_tac;
    1.25 -qed "int_mult_eq_cancel1";
    1.26 -
    1.27  Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";
    1.28  by (stac zdiv_zmult_zmult1 1);
    1.29  by Auto_tac;
    1.30 @@ -34,6 +20,7 @@
    1.31  by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1);
    1.32  qed "int_mult_div_cancel_disj";
    1.33  
    1.34 +
    1.35  local
    1.36    open Int_Numeral_Simprocs
    1.37  in
    1.38 @@ -65,7 +52,7 @@
    1.39    val prove_conv = Bin_Simprocs.prove_conv
    1.40    val mk_bal   = HOLogic.mk_eq
    1.41    val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    1.42 -  val cancel = int_mult_eq_cancel1 RS trans
    1.43 +  val cancel = mult_cancel_left RS trans
    1.44    val neg_exchanges = false
    1.45  )
    1.46  
    1.47 @@ -74,7 +61,7 @@
    1.48    val prove_conv = Bin_Simprocs.prove_conv
    1.49    val mk_bal   = HOLogic.mk_binrel "op <"
    1.50    val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
    1.51 -  val cancel = int_mult_less_cancel1 RS trans
    1.52 +  val cancel = mult_less_cancel_left RS trans
    1.53    val neg_exchanges = true
    1.54  )
    1.55  
    1.56 @@ -83,7 +70,7 @@
    1.57    val prove_conv = Bin_Simprocs.prove_conv
    1.58    val mk_bal   = HOLogic.mk_binrel "op <="
    1.59    val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
    1.60 -  val cancel = int_mult_le_cancel1 RS trans
    1.61 +  val cancel = mult_le_cancel_left RS trans
    1.62    val neg_exchanges = true
    1.63  )
    1.64  
    1.65 @@ -179,7 +166,7 @@
    1.66    val prove_conv = Bin_Simprocs.prove_conv
    1.67    val mk_bal   = HOLogic.mk_eq
    1.68    val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    1.69 -  val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_eq_cancel1
    1.70 +  val simplify_meta_eq  = cancel_simplify_meta_eq mult_cancel_left
    1.71  );
    1.72  
    1.73  structure DivideCancelFactor = ExtractCommonTermFun