Installation of CombineNumerals for the integers
Many bug fixes
Removal of AssocFold for addition (nat and int)
--- a/src/HOL/Integ/Bin.ML Wed May 03 18:30:29 2000 +0200
+++ b/src/HOL/Integ/Bin.ML Wed May 03 18:33:28 2000 +0200
@@ -265,6 +265,13 @@
by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
qed "zmult_2_right";
+(*Negation of a coefficient*)
+Goal "- (number_of w) * z = number_of(bin_minus w) * (z::int)";
+by (simp_tac (simpset_of Int.thy addsimps [number_of_minus, zmult_zminus]) 1);
+qed "zminus_number_of_zmult";
+
+Addsimps [zminus_number_of_zmult];
+
(** Inequality reasoning **)
--- a/src/HOL/Integ/Int.ML Wed May 03 18:30:29 2000 +0200
+++ b/src/HOL/Integ/Int.ML Wed May 03 18:33:28 2000 +0200
@@ -69,6 +69,11 @@
(*** misc ***)
+Goal "- (z - y) = y - (z::int)";
+by (Simp_tac 1);
+qed "zminus_zdiff_eq";
+Addsimps [zminus_zdiff_eq];
+
Goal "(w<z) = neg(w-z)";
by (simp_tac (simpset() addsimps [zless_def]) 1);
qed "zless_eq_neg";
--- a/src/HOL/Integ/IntArith.ML Wed May 03 18:30:29 2000 +0200
+++ b/src/HOL/Integ/IntArith.ML Wed May 03 18:33:28 2000 +0200
@@ -22,6 +22,13 @@
qed "zle_iff_zdiff_zle_0";
+(** For combine_numerals **)
+
+Goal "i*u + (j*u + k) = (i+j)*u + (k::int)";
+by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
+qed "left_zadd_zmult_distrib";
+
+
(** For cancel_numerals **)
Goal "!!i::int. ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)";
@@ -79,8 +86,10 @@
NumeralSyntax.mk_bin n;
(*Decodes a binary INTEGER*)
-fun dest_numeral (Const("Numeral.number_of", _) $ w) = NumeralSyntax.dest_bin w
- | dest_numeral t = raise TERM("dest_numeral", [t]);
+fun dest_numeral (Const("Numeral.number_of", _) $ w) =
+ (NumeralSyntax.dest_bin w
+ handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
+ | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
fun find_first_numeral past (t::terms) =
((dest_numeral t, rev past @ terms)
@@ -97,6 +106,10 @@
| mk_sum [t,u] = mk_plus (t, u)
| mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+(*this version ALWAYS includes a trailing zero*)
+fun long_mk_sum [] = zero
+ | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+
val dest_plus = HOLogic.dest_bin "op +" HOLogic.intT;
(*decompose additions AND subtractions as a sum*)
@@ -259,10 +272,42 @@
"(l::int) * m - n", "(l::int) - m * n"],
DiffCancelNumerals.proc)];
+
+structure CombineNumeralsData =
+ struct
+ val mk_sum = long_mk_sum (*to work for e.g. #2*x + #3*x *)
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val left_distrib = left_zadd_zmult_distrib RS trans
+ val prove_conv = prove_conv "int_combine_numerals"
+ val subst_tac = subst_tac
+ val norm_tac = ALLGOALS
+ (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
+ zadd_ac))
+ THEN ALLGOALS
+ (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
+ bin_simps@zadd_ac@zmult_ac))
+ val numeral_simp_tac = ALLGOALS
+ (simp_tac (HOL_ss addsimps add_0s@bin_simps))
+ end;
+
+structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
+
+val combine_numerals =
+ prep_simproc ("int_combine_numerals",
+ prep_pats ["(i::int) + (j+k)", "(i::int) + (j*k)",
+ "(j+k) + (i::int)", "(j*k) + (i::int)"],
+ CombineNumerals.proc);
+
end;
Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
+Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
+
+(*The Abel_Cancel simprocs are now obsolete*)
+Delsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
(*examples:
print_depth 22;
@@ -270,6 +315,8 @@
set trace_simp;
fun test s = (Goal s; by (Simp_tac 1));
+test "l + #2 + #2 + #2 + (l + #2) + (oo + #2) = (uu::int)";
+
test "#2*u = (u::int)";
test "(i + j + #12 + (k::int)) - #15 = y";
test "(i + j + #12 + (k::int)) - #5 = y";
@@ -277,15 +324,19 @@
test "y - b < (b::int)";
test "y - (#3*b + c) < (b::int) - #2*c";
-test "(#2*x + (u*v) + y) - v*#3*u = (w::int)";
+test "(#2*x - (u*v) + y) - v*#3*u = (w::int)";
test "(#2*x*u*v + (u*v)*#4 + y) - v*u*#4 = (w::int)";
test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::int)";
+test "u*v - (x*u*v + (u*v)*#4 + y) = (w::int)";
test "(i + j + #12 + (k::int)) = u + #15 + y";
test "(i + j*#2 + #12 + (k::int)) = j + #5 + y";
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)";
+test "a + -(b+c) + b = (d::int)";
+test "a + -(b+c) - b = (d::int)";
+
(*negative numerals*)
test "(i + j + #-2 + (k::int)) - (u + #5 + y) = zz";
test "(i + j + #-3 + (k::int)) < u + #5 + y";
@@ -299,8 +350,9 @@
(** Constant folding for integer plus and times **)
(*We do not need
+ structure Nat_Plus_Assoc = Assoc_Fold (Nat_Plus_Assoc_Data);
structure Int_Plus_Assoc = Assoc_Fold (Int_Plus_Assoc_Data);
- because cancel_coeffs does the same thing*)
+ because combine_numerals does the same thing*)
structure Int_Times_Assoc_Data : ASSOC_FOLD_DATA =
struct
@@ -319,18 +371,6 @@
(** The same for the naturals **)
-structure Nat_Plus_Assoc_Data : ASSOC_FOLD_DATA =
-struct
- val ss = HOL_ss
- val eq_reflection = eq_reflection
- val thy = Bin.thy
- val T = HOLogic.natT
- val plus = Const ("op +", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT);
- val add_ac = add_ac
-end;
-
-structure Nat_Plus_Assoc = Assoc_Fold (Nat_Plus_Assoc_Data);
-
structure Nat_Times_Assoc_Data : ASSOC_FOLD_DATA =
struct
val ss = HOL_ss
@@ -343,7 +383,7 @@
structure Nat_Times_Assoc = Assoc_Fold (Nat_Times_Assoc_Data);
-Addsimprocs [Nat_Plus_Assoc.conv, Nat_Times_Assoc.conv];
+Addsimprocs [Nat_Times_Assoc.conv];
@@ -362,11 +402,14 @@
(* reduce contradictory <= to False *)
val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @
- [int_0,zmult_0,zmult_0_right];
+ [int_0, zadd_0, zadd_0_right, zdiff_def,
+ zadd_zminus_inverse, zadd_zminus_inverse2,
+ zmult_0, zmult_0_right,
+ zmult_1, zmult_1_right,
+ zmult_minus1, zmult_minus1_right];
-val simprocs = Int_Numeral_Simprocs.cancel_numerals@
- [Int_Cancel.sum_conv, Int_Cancel.rel_conv (*****,
- Int_CC.sum_conv, Int_CC.rel_conv***)];
+val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
+ Int_Numeral_Simprocs.cancel_numerals;
val add_mono_thms =
map (fn s => prove_goal Int.thy s
--- a/src/HOL/Integ/IntDiv.ML Wed May 03 18:30:29 2000 +0200
+++ b/src/HOL/Integ/IntDiv.ML Wed May 03 18:33:28 2000 +0200
@@ -198,8 +198,7 @@
Addsimps [negateSnd_eq];
Goal "quorem ((-a,-b), qr) ==> quorem ((a,b), negateSnd qr)";
-by (auto_tac (claset(),
- simpset() addsimps split_ifs@[zmult_zminus, quorem_def]));
+by (auto_tac (claset(), simpset() addsimps split_ifs@[quorem_def]));
qed "quorem_neg";
Goal "b ~= #0 ==> quorem ((a,b), divAlg(a,b))";
@@ -804,7 +803,7 @@
by (subgoal_tac "#1 <= a" 1);
by (arith_tac 2);
by (subgoal_tac "#1 < a * #2" 1);
- by (dres_inst_tac [("i","#1"), ("k", "#2")] zmult_zle_mono1 2);
+ by (arith_tac 2);
by (subgoal_tac "#2*(#1 + b mod a) <= #2*a" 1);
by (rtac zmult_zle_mono2 2);
by (auto_tac (claset(),
@@ -819,6 +818,9 @@
pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
by (auto_tac (claset(),
simpset() addsimps [mod_pos_pos_trivial]));
+by (subgoal_tac "#0 <= b mod a" 1);
+ by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2);
+by (arith_tac 1);
qed "pos_zdiv_times_2";
@@ -863,7 +865,7 @@
by (subgoal_tac "#1 <= a" 1);
by (arith_tac 2);
by (subgoal_tac "#1 < a * #2" 1);
- by (dres_inst_tac [("i","#1"), ("k", "#2")] zmult_zle_mono1 2);
+ by (arith_tac 2);
by (subgoal_tac "#2*(#1 + b mod a) <= #2*a" 1);
by (rtac zmult_zle_mono2 2);
by (auto_tac (claset(),
@@ -878,6 +880,9 @@
pos_mod_sign RS zadd_zle_mono1 RSN (2,order_trans)]) 1);
by (auto_tac (claset(),
simpset() addsimps [mod_pos_pos_trivial]));
+by (subgoal_tac "#0 <= b mod a" 1);
+ by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2);
+by (arith_tac 1);
qed "pos_zmod_times_2";
--- a/src/HOL/Integ/NatSimprocs.ML Wed May 03 18:30:29 2000 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML Wed May 03 18:33:28 2000 +0200
@@ -76,9 +76,9 @@
fun dest_numeral (Const ("0", _)) = 0
| dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
| dest_numeral (Const("Numeral.number_of", _) $ w) =
- (BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w)
- handle Match => raise TERM("dest_numeral:1", [w]))
- | dest_numeral t = raise TERM("dest_numeral:2", [t]);
+ (BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w)
+ handle Match => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
+ | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
fun find_first_numeral past (t::terms) =
((dest_numeral t, t, rev past @ terms)
@@ -175,9 +175,10 @@
val find_first_coeff = find_first_coeff []
val subst_tac = subst_tac
val norm_tac = ALLGOALS
- (simp_tac (HOL_ss addsimps add_0s@mult_1s@bin_simps@
+ (simp_tac (HOL_ss addsimps add_0s@mult_1s@
[add_0, Suc_eq_add_numeral_1]@add_ac))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac@add_ac))
+ THEN ALLGOALS (simp_tac
+ (HOL_ss addsimps bin_simps@add_ac@mult_ac))
val numeral_simp_tac = ALLGOALS
(simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
end;
@@ -254,9 +255,10 @@
val prove_conv = prove_conv "nat_combine_numerals"
val subst_tac = subst_tac
val norm_tac = ALLGOALS
- (simp_tac (HOL_ss addsimps add_0s@mult_1s@bin_simps@
+ (simp_tac (HOL_ss addsimps add_0s@mult_1s@
[add_0, Suc_eq_add_numeral_1]@add_ac))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac@add_ac))
+ THEN ALLGOALS (simp_tac
+ (HOL_ss addsimps bin_simps@add_ac@mult_ac))
val numeral_simp_tac = ALLGOALS
(simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
end;
@@ -360,8 +362,6 @@
addsimprocs simprocs
end;
-Delsimprocs [Nat_Plus_Assoc.conv]; (*combine_numerals makes it redundant*)
-
(** For simplifying Suc m - #n **)