src/HOL/Integ/int_arith1.ML
changeset 11704 3c50a2cd6f00
parent 11701 3d51fbf81c17
child 11713 883d559b0b8c
     1.1 --- a/src/HOL/Integ/int_arith1.ML	Fri Oct 05 23:58:52 2001 +0200
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Sat Oct 06 00:02:46 2001 +0200
     1.3 @@ -279,7 +279,7 @@
     1.4  structure CombineNumeralsData =
     1.5    struct
     1.6    val add		= op + : int*int -> int 
     1.7 -  val mk_sum    	= long_mk_sum    (*to work for e.g. # 2*x + # 3*x *)
     1.8 +  val mk_sum    	= long_mk_sum    (*to work for e.g. 2*x + 3*x *)
     1.9    val dest_sum		= dest_sum
    1.10    val mk_coeff		= mk_coeff
    1.11    val dest_coeff	= dest_coeff 1
    1.12 @@ -318,35 +318,35 @@
    1.13  set trace_simp;
    1.14  fun test s = (Goal s; by (Simp_tac 1)); 
    1.15  
    1.16 -test "l + # 2 + # 2 + # 2 + (l + # 2) + (oo + # 2) = (uu::int)";
    1.17 +test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
    1.18  
    1.19 -test "# 2*u = (u::int)";
    1.20 -test "(i + j + # 12 + (k::int)) - # 15 = y";
    1.21 -test "(i + j + # 12 + (k::int)) - # 5 = y";
    1.22 +test "2*u = (u::int)";
    1.23 +test "(i + j + 12 + (k::int)) - 15 = y";
    1.24 +test "(i + j + 12 + (k::int)) - 5 = y";
    1.25  
    1.26  test "y - b < (b::int)";
    1.27 -test "y - (# 3*b + c) < (b::int) - # 2*c";
    1.28 +test "y - (3*b + c) < (b::int) - 2*c";
    1.29  
    1.30 -test "(# 2*x - (u*v) + y) - v*# 3*u = (w::int)";
    1.31 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u*# 4 = (w::int)";
    1.32 -test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::int)";
    1.33 -test "u*v - (x*u*v + (u*v)*# 4 + y) = (w::int)";
    1.34 +test "(2*x - (u*v) + y) - v*3*u = (w::int)";
    1.35 +test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)";
    1.36 +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)";
    1.37 +test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)";
    1.38  
    1.39 -test "(i + j + # 12 + (k::int)) = u + # 15 + y";
    1.40 -test "(i + j*# 2 + # 12 + (k::int)) = j + # 5 + y";
    1.41 +test "(i + j + 12 + (k::int)) = u + 15 + y";
    1.42 +test "(i + j*2 + 12 + (k::int)) = j + 5 + y";
    1.43  
    1.44 -test "# 2*y + # 3*z + # 6*w + # 2*y + # 3*z + # 2*u = # 2*y' + # 3*z' + # 6*w' + # 2*y' + # 3*z' + u + (vv::int)";
    1.45 +test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)";
    1.46  
    1.47  test "a + -(b+c) + b = (d::int)";
    1.48  test "a + -(b+c) - b = (d::int)";
    1.49  
    1.50  (*negative numerals*)
    1.51 -test "(i + j + # -2 + (k::int)) - (u + # 5 + y) = zz";
    1.52 -test "(i + j + # -3 + (k::int)) < u + # 5 + y";
    1.53 -test "(i + j + # 3 + (k::int)) < u + # -6 + y";
    1.54 -test "(i + j + # -12 + (k::int)) - # 15 = y";
    1.55 -test "(i + j + # 12 + (k::int)) - # -15 = y";
    1.56 -test "(i + j + # -12 + (k::int)) - # -15 = y";
    1.57 +test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz";
    1.58 +test "(i + j + -3 + (k::int)) < u + 5 + y";
    1.59 +test "(i + j + 3 + (k::int)) < u + -6 + y";
    1.60 +test "(i + j + -12 + (k::int)) - 15 = y";
    1.61 +test "(i + j + 12 + (k::int)) - -15 = y";
    1.62 +test "(i + j + -12 + (k::int)) - -15 = y";
    1.63  *)
    1.64  
    1.65  
    1.66 @@ -455,7 +455,7 @@
    1.67  (* Some test data
    1.68  Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
    1.69  by (fast_arith_tac 1);
    1.70 -Goal "!!a::int. [| a < b; c < d |] ==> a-d+ # 2 <= b+(-c)";
    1.71 +Goal "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)";
    1.72  by (fast_arith_tac 1);
    1.73  Goal "!!a::int. [| a < b; c < d |] ==> a+c+ Numeral1 < b+d";
    1.74  by (fast_arith_tac 1);
    1.75 @@ -465,7 +465,7 @@
    1.76  \     ==> a+a <= j+j";
    1.77  by (fast_arith_tac 1);
    1.78  Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
    1.79 -\     ==> a+a - - # -1 < j+j - # 3";
    1.80 +\     ==> a+a - - -1 < j+j - 3";
    1.81  by (fast_arith_tac 1);
    1.82  Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
    1.83  by (arith_tac 1);
    1.84 @@ -482,6 +482,6 @@
    1.85  \     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
    1.86  by (fast_arith_tac 1);
    1.87  Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
    1.88 -\     ==> # 6*a <= # 5*l+i";
    1.89 +\     ==> 6*a <= 5*l+i";
    1.90  by (fast_arith_tac 1);
    1.91  *)