1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Mon Oct 22 11:01:30 2001 +0200
     1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Mon Oct 22 11:54:22 2001 +0200
     1.3 @@ -10,27 +10,27 @@
     1.4  
     1.5  (** Factor cancellation theorems for "int" **)
     1.6  
     1.7 -Goal "!!k::int. (k*m <= k*n) = ((Numeral0 < k --> m<=n) & (k < Numeral0 --> n<=m))";
     1.8 +Goal "!!k::int. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))";
     1.9  by (stac zmult_zle_cancel1 1);
    1.10  by Auto_tac;  
    1.11  qed "int_mult_le_cancel1";
    1.12  
    1.13 -Goal "!!k::int. (k*m < k*n) = ((Numeral0 < k & m<n) | (k < Numeral0 & n<m))";
    1.14 +Goal "!!k::int. (k*m < k*n) = ((0 < k & m<n) | (k < 0 & n<m))";
    1.15  by (stac zmult_zless_cancel1 1);
    1.16  by Auto_tac;  
    1.17  qed "int_mult_less_cancel1";
    1.18  
    1.19 -Goal "!!k::int. (k*m = k*n) = (k = Numeral0 | m=n)";
    1.20 +Goal "!!k::int. (k*m = k*n) = (k = 0 | m=n)";
    1.21  by Auto_tac;  
    1.22  qed "int_mult_eq_cancel1";
    1.23  
    1.24 -Goal "!!k::int. k~=Numeral0 ==> (k*m) div (k*n) = (m div n)";
    1.25 +Goal "!!k::int. k~=0 ==> (k*m) div (k*n) = (m div n)";
    1.26  by (stac zdiv_zmult_zmult1 1); 
    1.27  by Auto_tac;  
    1.28  qed "int_mult_div_cancel1";
    1.29  
    1.30  (*For ExtractCommonTermFun, cancelling common factors*)
    1.31 -Goal "(k*m) div (k*n) = (if k = (Numeral0::int) then Numeral0 else m div n)";
    1.32 +Goal "(k*m) div (k*n) = (if k = (0::int) then 0 else m div n)";
    1.33  by (simp_tac (simpset() addsimps [int_mult_div_cancel1]) 1); 
    1.34  qed "int_mult_div_cancel_disj";
    1.35  
    1.36 @@ -54,7 +54,7 @@
    1.37  
    1.38  structure DivCancelNumeralFactor = CancelNumeralFactorFun
    1.39   (open CancelNumeralFactorCommon
    1.40 -  val prove_conv = prove_conv "intdiv_cancel_numeral_factor"
    1.41 +  val prove_conv = Bin_Simprocs.prove_conv "intdiv_cancel_numeral_factor"
    1.42    val mk_bal   = HOLogic.mk_binop "Divides.op div"
    1.43    val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
    1.44    val cancel = int_mult_div_cancel1 RS trans
    1.45 @@ -63,7 +63,7 @@
    1.46  
    1.47  structure EqCancelNumeralFactor = CancelNumeralFactorFun
    1.48   (open CancelNumeralFactorCommon
    1.49 -  val prove_conv = prove_conv "inteq_cancel_numeral_factor"
    1.50 +  val prove_conv = Bin_Simprocs.prove_conv "inteq_cancel_numeral_factor"
    1.51    val mk_bal   = HOLogic.mk_eq
    1.52    val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
    1.53    val cancel = int_mult_eq_cancel1 RS trans
    1.54 @@ -72,7 +72,7 @@
    1.55  
    1.56  structure LessCancelNumeralFactor = CancelNumeralFactorFun
    1.57   (open CancelNumeralFactorCommon
    1.58 -  val prove_conv = prove_conv "intless_cancel_numeral_factor"
    1.59 +  val prove_conv = Bin_Simprocs.prove_conv "intless_cancel_numeral_factor"
    1.60    val mk_bal   = HOLogic.mk_binrel "op <"
    1.61    val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
    1.62    val cancel = int_mult_less_cancel1 RS trans
    1.63 @@ -81,7 +81,7 @@
    1.64  
    1.65  structure LeCancelNumeralFactor = CancelNumeralFactorFun
    1.66   (open CancelNumeralFactorCommon
    1.67 -  val prove_conv = prove_conv "intle_cancel_numeral_factor"
    1.68 +  val prove_conv = Bin_Simprocs.prove_conv "intle_cancel_numeral_factor"
    1.69    val mk_bal   = HOLogic.mk_binrel "op <="
    1.70    val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
    1.71    val cancel = int_mult_le_cancel1 RS trans
    1.72 @@ -89,18 +89,18 @@
    1.73  )
    1.74  
    1.75  val int_cancel_numeral_factors = 
    1.76 -  map prep_simproc
    1.77 +  map Bin_Simprocs.prep_simproc
    1.78     [("inteq_cancel_numeral_factors",
    1.79 -     prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
    1.80 +     Bin_Simprocs.prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
    1.81       EqCancelNumeralFactor.proc),
    1.82      ("intless_cancel_numeral_factors", 
    1.83 -     prep_pats ["(l::int) * m < n", "(l::int) < m * n"], 
    1.84 +     Bin_Simprocs.prep_pats ["(l::int) * m < n", "(l::int) < m * n"], 
    1.85       LessCancelNumeralFactor.proc),
    1.86      ("intle_cancel_numeral_factors", 
    1.87 -     prep_pats ["(l::int) * m <= n", "(l::int) <= m * n"], 
    1.88 +     Bin_Simprocs.prep_pats ["(l::int) * m <= n", "(l::int) <= m * n"], 
    1.89       LeCancelNumeralFactor.proc),
    1.90      ("intdiv_cancel_numeral_factors", 
    1.91 -     prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
    1.92 +     Bin_Simprocs.prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
    1.93       DivCancelNumeralFactor.proc)];
    1.94  
    1.95  end;
    1.96 @@ -181,7 +181,7 @@
    1.97  
    1.98  structure EqCancelFactor = ExtractCommonTermFun
    1.99   (open CancelFactorCommon
   1.100 -  val prove_conv = prove_conv "int_eq_cancel_factor"
   1.101 +  val prove_conv = Bin_Simprocs.prove_conv "int_eq_cancel_factor"
   1.102    val mk_bal   = HOLogic.mk_eq
   1.103    val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
   1.104    val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_eq_cancel1
   1.105 @@ -189,19 +189,19 @@
   1.106  
   1.107  structure DivideCancelFactor = ExtractCommonTermFun
   1.108   (open CancelFactorCommon
   1.109 -  val prove_conv = prove_conv "int_divide_cancel_factor"
   1.110 +  val prove_conv = Bin_Simprocs.prove_conv "int_divide_cancel_factor"
   1.111    val mk_bal   = HOLogic.mk_binop "Divides.op div"
   1.112    val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.intT
   1.113    val simplify_meta_eq  = cancel_simplify_meta_eq int_mult_div_cancel_disj
   1.114  );
   1.115  
   1.116  val int_cancel_factor = 
   1.117 -  map prep_simproc
   1.118 +  map Bin_Simprocs.prep_simproc
   1.119     [("int_eq_cancel_factor",
   1.120 -     prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
   1.121 +     Bin_Simprocs.prep_pats ["(l::int) * m = n", "(l::int) = m * n"], 
   1.122       EqCancelFactor.proc),
   1.123      ("int_divide_cancel_factor", 
   1.124 -     prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
   1.125 +     Bin_Simprocs.prep_pats ["((l::int) * m) div n", "(l::int) div (m * n)"], 
   1.126       DivideCancelFactor.proc)];
   1.127  
   1.128  end;