src/HOL/Integ/int_factor_simprocs.ML
 changeset 11701 3d51fbf81c17 parent 10713 69c9fc1d11f2 child 11704 3c50a2cd6f00
```     1.1 --- a/src/HOL/Integ/int_factor_simprocs.ML	Fri Oct 05 21:50:37 2001 +0200
1.2 +++ b/src/HOL/Integ/int_factor_simprocs.ML	Fri Oct 05 21:52:39 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) = ((#0 < k --> m<=n) & (k < #0 --> n<=m))";
1.8 +Goal "!!k::int. (k*m <= k*n) = ((Numeral0 < k --> m<=n) & (k < Numeral0 --> 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) = ((#0 < k & m<n) | (k < #0 & n<m))";
1.14 +Goal "!!k::int. (k*m < k*n) = ((Numeral0 < k & m<n) | (k < Numeral0 & 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 = #0 | m=n)";
1.20 +Goal "!!k::int. (k*m = k*n) = (k = Numeral0 | m=n)";
1.21  by Auto_tac;
1.22  qed "int_mult_eq_cancel1";
1.23
1.24 -Goal "!!k::int. k~=#0 ==> (k*m) div (k*n) = (m div n)";
1.25 +Goal "!!k::int. k~=Numeral0 ==> (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 = (#0::int) then #0 else m div n)";
1.32 +Goal "(k*m) div (k*n) = (if k = (Numeral0::int) then Numeral0 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 @@ -114,33 +114,33 @@
1.37  set trace_simp;
1.38  fun test s = (Goal s; by (Simp_tac 1));
1.39
1.40 -test "#9*x = #12 * (y::int)";
1.41 -test "(#9*x) div (#12 * (y::int)) = z";
1.42 -test "#9*x < #12 * (y::int)";
1.43 -test "#9*x <= #12 * (y::int)";
1.44 +test "# 9*x = # 12 * (y::int)";
1.45 +test "(# 9*x) div (# 12 * (y::int)) = z";
1.46 +test "# 9*x < # 12 * (y::int)";
1.47 +test "# 9*x <= # 12 * (y::int)";
1.48
1.49 -test "#-99*x = #132 * (y::int)";
1.50 -test "(#-99*x) div (#132 * (y::int)) = z";
1.51 -test "#-99*x < #132 * (y::int)";
1.52 -test "#-99*x <= #132 * (y::int)";
1.53 +test "# -99*x = # 132 * (y::int)";
1.54 +test "(# -99*x) div (# 132 * (y::int)) = z";
1.55 +test "# -99*x < # 132 * (y::int)";
1.56 +test "# -99*x <= # 132 * (y::int)";
1.57
1.58 -test "#999*x = #-396 * (y::int)";
1.59 -test "(#999*x) div (#-396 * (y::int)) = z";
1.60 -test "#999*x < #-396 * (y::int)";
1.61 -test "#999*x <= #-396 * (y::int)";
1.62 +test "# 999*x = # -396 * (y::int)";
1.63 +test "(# 999*x) div (# -396 * (y::int)) = z";
1.64 +test "# 999*x < # -396 * (y::int)";
1.65 +test "# 999*x <= # -396 * (y::int)";
1.66
1.67 -test "#-99*x = #-81 * (y::int)";
1.68 -test "(#-99*x) div (#-81 * (y::int)) = z";
1.69 -test "#-99*x <= #-81 * (y::int)";
1.70 -test "#-99*x < #-81 * (y::int)";
1.71 +test "# -99*x = # -81 * (y::int)";
1.72 +test "(# -99*x) div (# -81 * (y::int)) = z";
1.73 +test "# -99*x <= # -81 * (y::int)";
1.74 +test "# -99*x < # -81 * (y::int)";
1.75
1.76 -test "#-2 * x = #-1 * (y::int)";
1.77 -test "#-2 * x = -(y::int)";
1.78 -test "(#-2 * x) div (#-1 * (y::int)) = z";
1.79 -test "#-2 * x < -(y::int)";
1.80 -test "#-2 * x <= #-1 * (y::int)";
1.81 -test "-x < #-23 * (y::int)";
1.82 -test "-x <= #-23 * (y::int)";
1.83 +test "# -2 * x = # -1 * (y::int)";
1.84 +test "# -2 * x = -(y::int)";
1.85 +test "(# -2 * x) div (# -1 * (y::int)) = z";
1.86 +test "# -2 * x < -(y::int)";
1.87 +test "# -2 * x <= # -1 * (y::int)";
1.88 +test "-x < # -23 * (y::int)";
1.89 +test "-x <= # -23 * (y::int)";
1.90  *)
1.91
1.92
```