src/HOL/Integ/int_factor_simprocs.ML
 changeset 11868 56db9f3a6b3e parent 11704 3c50a2cd6f00 child 12018 ec054019c910
```     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;
```