1.1 --- a/src/HOL/Integ/nat_simprocs.ML Fri Oct 05 21:50:37 2001 +0200
1.2 +++ b/src/HOL/Integ/nat_simprocs.ML Fri Oct 05 21:52:39 2001 +0200
1.3 @@ -66,19 +66,19 @@
1.4
1.5 (** For cancel_numeral_factors **)
1.6
1.7 -Goal "(#0::nat) < k ==> (k*m <= k*n) = (m<=n)";
1.8 +Goal "(Numeral0::nat) < k ==> (k*m <= k*n) = (m<=n)";
1.9 by Auto_tac;
1.10 qed "nat_mult_le_cancel1";
1.11
1.12 -Goal "(#0::nat) < k ==> (k*m < k*n) = (m<n)";
1.13 +Goal "(Numeral0::nat) < k ==> (k*m < k*n) = (m<n)";
1.14 by Auto_tac;
1.15 qed "nat_mult_less_cancel1";
1.16
1.17 -Goal "(#0::nat) < k ==> (k*m = k*n) = (m=n)";
1.18 +Goal "(Numeral0::nat) < k ==> (k*m = k*n) = (m=n)";
1.19 by Auto_tac;
1.20 qed "nat_mult_eq_cancel1";
1.21
1.22 -Goal "(#0::nat) < k ==> (k*m) div (k*n) = (m div n)";
1.23 +Goal "(Numeral0::nat) < k ==> (k*m) div (k*n) = (m div n)";
1.24 by Auto_tac;
1.25 qed "nat_mult_div_cancel1";
1.26
1.27 @@ -125,7 +125,7 @@
1.28 val zero = mk_numeral 0;
1.29 val mk_plus = HOLogic.mk_binop "op +";
1.30
1.31 -(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
1.32 +(*Thus mk_sum[t] yields t+Numeral0; longer sums don't have a trailing zero*)
1.33 fun mk_sum [] = zero
1.34 | mk_sum [t,u] = mk_plus (t, u)
1.35 | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
1.36 @@ -158,7 +158,7 @@
1.37 val bin_simps = [add_nat_number_of, nat_number_of_add_left,
1.38 diff_nat_number_of, le_nat_number_of_eq_not_less,
1.39 less_nat_number_of, mult_nat_number_of,
1.40 - Let_number_of, nat_number_of] @
1.41 + thm "Let_number_of", nat_number_of] @
1.42 bin_arith_simps @ bin_rel_simps;
1.43
1.44 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
1.45 @@ -204,11 +204,11 @@
1.46 handle TERM _ => find_first_coeff (t::past) u terms;
1.47
1.48
1.49 -(*Simplify #1*n and n*#1 to n*)
1.50 +(*Simplify Numeral1*n and n*Numeral1 to n*)
1.51 val add_0s = map rename_numerals [add_0, add_0_right];
1.52 val mult_1s = map rename_numerals [mult_1, mult_1_right];
1.53
1.54 -(*Final simplification: cancel + and *; replace #0 by 0 and #1 by 1*)
1.55 +(*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
1.56 val simplify_meta_eq =
1.57 Int_Numeral_Simprocs.simplify_meta_eq
1.58 [numeral_0_eq_0, numeral_1_eq_1, add_0, add_0_right,
1.59 @@ -319,7 +319,7 @@
1.60 structure CombineNumeralsData =
1.61 struct
1.62 val add = op + : int*int -> int
1.63 - val mk_sum = long_mk_sum (*to work for e.g. #2*x + #3*x *)
1.64 + val mk_sum = long_mk_sum (*to work for e.g. # 2*x + # 3*x *)
1.65 val dest_sum = restricted_dest_Sucs_sum
1.66 val mk_coeff = mk_coeff
1.67 val dest_coeff = dest_coeff
1.68 @@ -504,62 +504,62 @@
1.69 fun test s = (Goal s; by (Simp_tac 1));
1.70
1.71 (*cancel_numerals*)
1.72 -test "l +( #2) + (#2) + #2 + (l + #2) + (oo + #2) = (uu::nat)";
1.73 -test "(#2*length xs < #2*length xs + j)";
1.74 -test "(#2*length xs < length xs * #2 + j)";
1.75 -test "#2*u = (u::nat)";
1.76 -test "#2*u = Suc (u)";
1.77 -test "(i + j + #12 + (k::nat)) - #15 = y";
1.78 -test "(i + j + #12 + (k::nat)) - #5 = y";
1.79 -test "Suc u - #2 = y";
1.80 -test "Suc (Suc (Suc u)) - #2 = y";
1.81 -test "(i + j + #2 + (k::nat)) - 1 = y";
1.82 -test "(i + j + #1 + (k::nat)) - 2 = y";
1.83 +test "l +( # 2) + (# 2) + # 2 + (l + # 2) + (oo + # 2) = (uu::nat)";
1.84 +test "(# 2*length xs < # 2*length xs + j)";
1.85 +test "(# 2*length xs < length xs * # 2 + j)";
1.86 +test "# 2*u = (u::nat)";
1.87 +test "# 2*u = Suc (u)";
1.88 +test "(i + j + # 12 + (k::nat)) - # 15 = y";
1.89 +test "(i + j + # 12 + (k::nat)) - # 5 = y";
1.90 +test "Suc u - # 2 = y";
1.91 +test "Suc (Suc (Suc u)) - # 2 = y";
1.92 +test "(i + j + # 2 + (k::nat)) - 1 = y";
1.93 +test "(i + j + Numeral1 + (k::nat)) - 2 = y";
1.94
1.95 -test "(#2*x + (u*v) + y) - v*#3*u = (w::nat)";
1.96 -test "(#2*x*u*v + #5 + (u*v)*#4 + y) - v*u*#4 = (w::nat)";
1.97 -test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::nat)";
1.98 -test "Suc (Suc (#2*x*u*v + u*#4 + y)) - u = w";
1.99 -test "Suc ((u*v)*#4) - v*#3*u = w";
1.100 -test "Suc (Suc ((u*v)*#3)) - v*#3*u = w";
1.101 +test "(# 2*x + (u*v) + y) - v*# 3*u = (w::nat)";
1.102 +test "(# 2*x*u*v + # 5 + (u*v)*# 4 + y) - v*u*# 4 = (w::nat)";
1.103 +test "(# 2*x*u*v + (u*v)*# 4 + y) - v*u = (w::nat)";
1.104 +test "Suc (Suc (# 2*x*u*v + u*# 4 + y)) - u = w";
1.105 +test "Suc ((u*v)*# 4) - v*# 3*u = w";
1.106 +test "Suc (Suc ((u*v)*# 3)) - v*# 3*u = w";
1.107
1.108 -test "(i + j + #12 + (k::nat)) = u + #15 + y";
1.109 -test "(i + j + #32 + (k::nat)) - (u + #15 + y) = zz";
1.110 -test "(i + j + #12 + (k::nat)) = u + #5 + y";
1.111 +test "(i + j + # 12 + (k::nat)) = u + # 15 + y";
1.112 +test "(i + j + # 32 + (k::nat)) - (u + # 15 + y) = zz";
1.113 +test "(i + j + # 12 + (k::nat)) = u + # 5 + y";
1.114 (*Suc*)
1.115 -test "(i + j + #12 + k) = Suc (u + y)";
1.116 -test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + #41 + k)";
1.117 -test "(i + j + #5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
1.118 -test "Suc (Suc (Suc (Suc (Suc (u + y))))) - #5 = v";
1.119 -test "(i + j + #5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
1.120 -test "#2*y + #3*z + #2*u = Suc (u)";
1.121 -test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = Suc (u)";
1.122 -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::nat)";
1.123 -test "#6 + #2*y + #3*z + #4*u = Suc (vv + #2*u + z)";
1.124 -test "(#2*n*m) < (#3*(m*n)) + (u::nat)";
1.125 +test "(i + j + # 12 + k) = Suc (u + y)";
1.126 +test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + # 41 + k)";
1.127 +test "(i + j + # 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
1.128 +test "Suc (Suc (Suc (Suc (Suc (u + y))))) - # 5 = v";
1.129 +test "(i + j + # 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
1.130 +test "# 2*y + # 3*z + # 2*u = Suc (u)";
1.131 +test "# 2*y + # 3*z + # 6*w + # 2*y + # 3*z + # 2*u = Suc (u)";
1.132 +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::nat)";
1.133 +test "# 6 + # 2*y + # 3*z + # 4*u = Suc (vv + # 2*u + z)";
1.134 +test "(# 2*n*m) < (# 3*(m*n)) + (u::nat)";
1.135
1.136 (*negative numerals: FAIL*)
1.137 -test "(i + j + #-23 + (k::nat)) < u + #15 + y";
1.138 -test "(i + j + #3 + (k::nat)) < u + #-15 + y";
1.139 -test "(i + j + #-12 + (k::nat)) - #15 = y";
1.140 -test "(i + j + #12 + (k::nat)) - #-15 = y";
1.141 -test "(i + j + #-12 + (k::nat)) - #-15 = y";
1.142 +test "(i + j + # -23 + (k::nat)) < u + # 15 + y";
1.143 +test "(i + j + # 3 + (k::nat)) < u + # -15 + y";
1.144 +test "(i + j + # -12 + (k::nat)) - # 15 = y";
1.145 +test "(i + j + # 12 + (k::nat)) - # -15 = y";
1.146 +test "(i + j + # -12 + (k::nat)) - # -15 = y";
1.147
1.148 (*combine_numerals*)
1.149 -test "k + #3*k = (u::nat)";
1.150 -test "Suc (i + #3) = u";
1.151 -test "Suc (i + j + #3 + k) = u";
1.152 -test "k + j + #3*k + j = (u::nat)";
1.153 -test "Suc (j*i + i + k + #5 + #3*k + i*j*#4) = (u::nat)";
1.154 -test "(#2*n*m) + (#3*(m*n)) = (u::nat)";
1.155 +test "k + # 3*k = (u::nat)";
1.156 +test "Suc (i + # 3) = u";
1.157 +test "Suc (i + j + # 3 + k) = u";
1.158 +test "k + j + # 3*k + j = (u::nat)";
1.159 +test "Suc (j*i + i + k + # 5 + # 3*k + i*j*# 4) = (u::nat)";
1.160 +test "(# 2*n*m) + (# 3*(m*n)) = (u::nat)";
1.161 (*negative numerals: FAIL*)
1.162 -test "Suc (i + j + #-3 + k) = u";
1.163 +test "Suc (i + j + # -3 + k) = u";
1.164
1.165 (*cancel_numeral_factors*)
1.166 -test "#9*x = #12 * (y::nat)";
1.167 -test "(#9*x) div (#12 * (y::nat)) = z";
1.168 -test "#9*x < #12 * (y::nat)";
1.169 -test "#9*x <= #12 * (y::nat)";
1.170 +test "# 9*x = # 12 * (y::nat)";
1.171 +test "(# 9*x) div (# 12 * (y::nat)) = z";
1.172 +test "# 9*x < # 12 * (y::nat)";
1.173 +test "# 9*x <= # 12 * (y::nat)";
1.174
1.175 (*cancel_factor*)
1.176 test "x*k = k*(y::nat)";
1.177 @@ -597,7 +597,7 @@
1.178 Suc_eq_number_of,eq_number_of_Suc,
1.179 mult_0, mult_0_right, mult_Suc, mult_Suc_right,
1.180 eq_number_of_0, eq_0_number_of, less_0_number_of,
1.181 - nat_number_of, Let_number_of, if_True, if_False];
1.182 + nat_number_of, thm "Let_number_of", if_True, if_False];
1.183
1.184 val simprocs = [Nat_Times_Assoc.conv,
1.185 Nat_Numeral_Simprocs.combine_numerals]@