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