--- a/src/HOL/Integ/IntArith.ML Wed Jun 14 17:44:43 2000 +0200
+++ b/src/HOL/Integ/IntArith.ML Wed Jun 14 17:45:01 2000 +0200
@@ -31,14 +31,6 @@
(** For cancel_numerals **)
-Goal "!!i::int. ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)";
-by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
-qed "diff_add_eq1";
-
-Goal "!!i::int. ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))";
-by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
-qed "diff_add_eq2";
-
val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
[zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
zle_iff_zdiff_zle_0] @
@@ -171,8 +163,7 @@
val mult_1s = [zmult_1, zmult_1_right, zmult_minus1, zmult_minus1_right];
(*To perform binary arithmetic*)
-val bin_simps = [number_of_add RS sym, add_number_of_left] @
- bin_arith_simps @ bin_rel_simps;
+val bin_simps = [add_number_of_left] @ bin_arith_simps @ bin_rel_simps;
(*To evaluate binary negations of coefficients*)
val zminus_simps = NCons_simps @
@@ -478,33 +469,11 @@
(** Simplification of inequalities involving numerical constants **)
-Goal "(w <= z + (#1::int)) = (w<=z | w = z + (#1::int))";
-by (arith_tac 1);
-qed "zle_add1_eq";
-
Goal "(w <= z - (#1::int)) = (w<(z::int))";
by (arith_tac 1);
qed "zle_diff1_eq";
Addsimps [zle_diff1_eq];
-(*2nd premise can be proved automatically if v is a literal*)
-Goal "[| w <= z; #0 <= v |] ==> w <= z + (v::int)";
-by (fast_arith_tac 1);
-qed "zle_imp_zle_zadd";
-
-Goal "w <= z ==> w <= z + (#1::int)";
-by (fast_arith_tac 1);
-qed "zle_imp_zle_zadd1";
-
-(*2nd premise can be proved automatically if v is a literal*)
-Goal "[| w < z; #0 <= v |] ==> w < z + (v::int)";
-by (fast_arith_tac 1);
-qed "zless_imp_zless_zadd";
-
-Goal "w < z ==> w < z + (#1::int)";
-by (fast_arith_tac 1);
-qed "zless_imp_zless_zadd1";
-
Goal "(w < z + #1) = (w<=(z::int))";
by (arith_tac 1);
qed "zle_add1_eq_le";
@@ -515,20 +484,6 @@
qed "zadd_left_cancel0";
Addsimps [zadd_left_cancel0];
-(*LOOPS as a simprule!*)
-Goal "[| w + v < z; #0 <= v |] ==> w < (z::int)";
-by (fast_arith_tac 1);
-qed "zless_zadd_imp_zless";
-
-(*LOOPS as a simprule! Analogous to Suc_lessD*)
-Goal "w + #1 < z ==> w < (z::int)";
-by (fast_arith_tac 1);
-qed "zless_zadd1_imp_zless";
-
-Goal "w + #-1 = w - (#1::int)";
-by (Simp_tac 1);
-qed "zplus_minus1_conv";
-
(* nat *)
@@ -602,62 +557,53 @@
qed_spec_mp "zdiff_int";
-(** Products of signs **)
+(*** Some convenient biconditionals for products of signs ***)
-Goal "(m::int) < #0 ==> (#0 < m*n) = (n < #0)";
-by Auto_tac;
-by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2);
-by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1);
-by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
-by (force_tac (claset() addDs [inst "k" "m" zmult_zless_mono1_neg],
- simpset()addsimps [order_le_less, zmult_commute]) 1);
-qed "neg_imp_zmult_pos_iff";
+Goal "[| (#0::int) < i; #0 < j |] ==> #0 < i*j";
+by (dtac zmult_zless_mono1 1);
+by Auto_tac;
+qed "zmult_pos";
-Goal "(m::int) < #0 ==> (m*n < #0) = (#0 < n)";
-by Auto_tac;
-by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2);
-by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1);
-by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
-by (force_tac (claset() addDs [zmult_zless_mono1_neg],
- simpset() addsimps [order_le_less]) 1);
-qed "neg_imp_zmult_neg_iff";
+Goal "[| i < (#0::int); j < #0 |] ==> #0 < i*j";
+by (dtac zmult_zless_mono1_neg 1);
+by Auto_tac;
+qed "zmult_neg";
-Goal "#0 < (m::int) ==> (m*n < #0) = (n < #0)";
-by Auto_tac;
-by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2);
-by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1);
-by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
-by (force_tac (claset() addDs [zmult_zless_mono1],
- simpset() addsimps [order_le_less]) 1);
-qed "pos_imp_zmult_neg_iff";
+Goal "[| (#0::int) < i; j < #0 |] ==> i*j < #0";
+by (dtac zmult_zless_mono1_neg 1);
+by Auto_tac;
+qed "zmult_pos_neg";
-Goal "#0 < (m::int) ==> (#0 < m*n) = (#0 < n)";
-by Auto_tac;
-by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2);
-by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1);
-by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
-by (force_tac (claset() addDs [inst "k" "m" zmult_zless_mono1],
- simpset() addsimps [order_le_less, zmult_commute]) 1);
-qed "pos_imp_zmult_pos_iff";
-
-(** <= versions of the theorems above **)
+Goal "((#0::int) < x*y) = (#0 < x & #0 < y | x < #0 & y < #0)";
+by (auto_tac (claset(),
+ simpset() addsimps [order_le_less, linorder_not_less,
+ zmult_pos, zmult_neg]));
+by (ALLGOALS (rtac ccontr));
+by (auto_tac (claset(),
+ simpset() addsimps [order_le_less, linorder_not_less]));
+by (ALLGOALS (etac rev_mp));
+by (ALLGOALS (dtac zmult_pos_neg THEN' assume_tac));
+by (auto_tac (claset() addDs [order_less_not_sym],
+ simpset() addsimps [zmult_commute]));
+qed "int_0_less_mult_iff";
-Goal "(m::int) < #0 ==> (m*n <= #0) = (#0 <= n)";
-by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
- neg_imp_zmult_pos_iff]) 1);
-qed "neg_imp_zmult_nonpos_iff";
-
-Goal "(m::int) < #0 ==> (#0 <= m*n) = (n <= #0)";
-by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
- neg_imp_zmult_neg_iff]) 1);
-qed "neg_imp_zmult_nonneg_iff";
+Goal "((#0::int) <= x*y) = (#0 <= x & #0 <= y | x <= #0 & y <= #0)";
+by (auto_tac (claset(),
+ simpset() addsimps [order_le_less, linorder_not_less,
+ int_0_less_mult_iff]));
+qed "int_0_le_mult_iff";
-Goal "#0 < (m::int) ==> (m*n <= #0) = (n <= #0)";
-by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
- pos_imp_zmult_pos_iff]) 1);
-qed "pos_imp_zmult_nonpos_iff";
+Goal "(x*y < (#0::int)) = (#0 < x & y < #0 | x < #0 & #0 < y)";
+by (auto_tac (claset(),
+ simpset() addsimps [int_0_le_mult_iff,
+ linorder_not_le RS sym]));
+by (auto_tac (claset() addDs [order_less_not_sym],
+ simpset() addsimps [linorder_not_le]));
+qed "zmult_less_0_iff";
-Goal "#0 < (m::int) ==> (#0 <= m*n) = (#0 <= n)";
-by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
- pos_imp_zmult_neg_iff]) 1);
-qed "pos_imp_zmult_nonneg_iff";
+Goal "(x*y <= (#0::int)) = (#0 <= x & y <= #0 | x <= #0 & #0 <= y)";
+by (auto_tac (claset() addDs [order_less_not_sym],
+ simpset() addsimps [int_0_less_mult_iff,
+ linorder_not_less RS sym]));
+qed "zmult_le_0_iff";
+
--- a/src/HOL/Integ/IntDiv.ML Wed Jun 14 17:44:43 2000 +0200
+++ b/src/HOL/Integ/IntDiv.ML Wed Jun 14 17:45:01 2000 +0200
@@ -115,9 +115,7 @@
Goal "#0 <= a --> #0 < b --> quorem ((a, b), posDivAlg (a, b))";
by (res_inst_tac [("u", "a"), ("v", "b")] posDivAlg_induct 1);
by Auto_tac;
-by (ALLGOALS
- (asm_full_simp_tac (simpset() addsimps [quorem_def,
- pos_imp_zmult_pos_iff])));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
(*base case: a<b*)
by (asm_full_simp_tac (simpset() addsimps [posDivAlg_eqn]) 1);
(*main argument*)
@@ -156,9 +154,7 @@
Goal "a < #0 --> #0 < b --> quorem ((a, b), negDivAlg (a, b))";
by (res_inst_tac [("u", "a"), ("v", "b")] negDivAlg_induct 1);
by Auto_tac;
-by (ALLGOALS
- (asm_full_simp_tac (simpset() addsimps [quorem_def,
- pos_imp_zmult_pos_iff])));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
(*base case: 0<=a+b*)
by (asm_full_simp_tac (simpset() addsimps [negDivAlg_eqn]) 1);
(*main argument*)
@@ -325,13 +321,13 @@
Goal "[| (#0::int) < a; a = r + a*q; r < a |] ==> #1 <= q";
by (subgoal_tac "#0 < a*q" 1);
by (arith_tac 2);
-by (asm_full_simp_tac (simpset() addsimps [pos_imp_zmult_pos_iff]) 1);
+by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1);
val lemma1 = result();
Goal "[| (#0::int) < a; a = r + a*q; #0 <= r |] ==> q <= #1";
by (subgoal_tac "#0 <= a*(#1-q)" 1);
by (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2);
-by (asm_full_simp_tac (simpset() addsimps [pos_imp_zmult_nonneg_iff]) 1);
+by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1);
val lemma2 = result();
Goal "[| quorem((a,a),(q,r)); a ~= (#0::int) |] ==> q = #1";
@@ -494,7 +490,7 @@
by (subgoal_tac "#0 <= q'" 1);
by (subgoal_tac "#0 < b'*(q' + #1)" 2);
by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 3);
- by (asm_full_simp_tac (simpset() addsimps [pos_imp_zmult_pos_iff]) 2);
+ by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 2);
by (subgoal_tac "b*q < b*(q' + #1)" 1);
by (Asm_full_simp_tac 1);
by (subgoal_tac "b*q = r' - r + b'*q'" 1);
@@ -523,7 +519,7 @@
by (subgoal_tac "q' < #0" 1);
by (subgoal_tac "b'*q' < #0" 2);
by (arith_tac 3);
- by (asm_full_simp_tac (simpset() addsimps [pos_imp_zmult_neg_iff]) 2);
+ by (asm_full_simp_tac (simpset() addsimps [zmult_less_0_iff]) 2);
by (subgoal_tac "b*q' < b*(q + #1)" 1);
by (Asm_full_simp_tac 1);
by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
@@ -683,15 +679,13 @@
Goal "[| (#0::int) < c; b < r; r <= #0 |] ==> b * (q mod c) + r <= #0";
by (subgoal_tac "b * (q mod c) <= #0" 1);
by (arith_tac 1);
-by (asm_simp_tac (simpset() addsimps [neg_imp_zmult_nonpos_iff,
- pos_mod_sign]) 1);
+by (asm_simp_tac (simpset() addsimps [zmult_le_0_iff, pos_mod_sign]) 1);
val lemma2 = result();
Goal "[| (#0::int) < c; #0 <= r; r < b |] ==> #0 <= b * (q mod c) + r";
by (subgoal_tac "#0 <= b * (q mod c)" 1);
by (arith_tac 1);
-by (asm_simp_tac
- (simpset() addsimps [pos_imp_zmult_nonneg_iff, pos_mod_sign]) 1);
+by (asm_simp_tac (simpset() addsimps [int_0_le_mult_iff, pos_mod_sign]) 1);
val lemma3 = result();
Goal "[| (#0::int) < c; #0 <= r; r < b |] ==> b * (q mod c) + r < b * c";
@@ -712,8 +706,7 @@
(claset(),
simpset() addsimps zmult_ac@
[zmod_zdiv_equality, quorem_def, linorder_neq_iff,
- pos_imp_zmult_pos_iff,
- neg_imp_zmult_pos_iff,
+ int_0_less_mult_iff,
zadd_zmult_distrib2 RS sym,
lemma1, lemma2, lemma3, lemma4]));
val lemma = result();
@@ -816,12 +809,12 @@
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";
+qed "pos_zdiv_mult_2";
Goal "a <= (#0::int) ==> (#1 + #2*b) div (#2*a) = (b+#1) div a";
by (subgoal_tac "(#1 + #2*(-b-#1)) div (#2 * (-a)) = (-b-#1) div (-a)" 1);
-by (rtac pos_zdiv_times_2 2);
+by (rtac pos_zdiv_mult_2 2);
by (auto_tac (claset(),
simpset() addsimps [zmult_zminus_right]));
by (subgoal_tac "(#-1 - (#2 * b)) = - (#1 + (#2 * b))" 1);
@@ -829,7 +822,7 @@
by (asm_full_simp_tac (HOL_ss
addsimps [zdiv_zminus_zminus, zdiff_def,
zminus_zadd_distrib RS sym]) 1);
-qed "neg_zdiv_times_2";
+qed "neg_zdiv_mult_2";
(*Not clear why this must be proved separately; probably number_of causes
@@ -847,7 +840,7 @@
by (asm_simp_tac (simpset()
delsimps bin_arith_extra_simps@bin_rel_simps
addsimps [zdiv_zmult_zmult1,
- pos_zdiv_times_2, lemma, neg_zdiv_times_2]) 1);
+ pos_zdiv_mult_2, lemma, neg_zdiv_mult_2]) 1);
qed "zdiv_number_of_BIT";
Addsimps [zdiv_number_of_BIT];
@@ -878,13 +871,13 @@
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";
+qed "pos_zmod_mult_2";
Goal "a <= (#0::int) ==> (#1 + #2*b) mod (#2*a) = #2 * ((b+#1) mod a) - #1";
by (subgoal_tac
"(#1 + #2*(-b-#1)) mod (#2*(-a)) = #1 + #2*((-b-#1) mod (-a))" 1);
-by (rtac pos_zmod_times_2 2);
+by (rtac pos_zmod_mult_2 2);
by (auto_tac (claset(),
simpset() addsimps [zmult_zminus_right]));
by (subgoal_tac "(#-1 - (#2 * b)) = - (#1 + (#2 * b))" 1);
@@ -894,7 +887,7 @@
zminus_zadd_distrib RS sym]) 1);
by (dtac (zminus_equation RS iffD1 RS sym) 1);
by Auto_tac;
-qed "neg_zmod_times_2";
+qed "neg_zmod_mult_2";
Goal "number_of (v BIT b) mod number_of (w BIT False) = \
\ (if b then \
@@ -907,7 +900,7 @@
by (asm_simp_tac (simpset()
delsimps bin_arith_extra_simps@bin_rel_simps
addsimps [zmod_zmult_zmult1,
- pos_zmod_times_2, lemma, neg_zmod_times_2]) 1);
+ pos_zmod_mult_2, lemma, neg_zmod_mult_2]) 1);
qed "zmod_number_of_BIT";
Addsimps [zmod_number_of_BIT];