new lemmas for signs of products
authorpaulson
Wed Jun 14 17:45:01 2000 +0200 (2000-06-14)
changeset 90630d7628966069
parent 9062 7b34ffecaaa8
child 9064 eacebbcafe57
new lemmas for signs of products
src/HOL/Integ/IntArith.ML
src/HOL/Integ/IntDiv.ML
     1.1 --- a/src/HOL/Integ/IntArith.ML	Wed Jun 14 17:44:43 2000 +0200
     1.2 +++ b/src/HOL/Integ/IntArith.ML	Wed Jun 14 17:45:01 2000 +0200
     1.3 @@ -31,14 +31,6 @@
     1.4  
     1.5  (** For cancel_numerals **)
     1.6  
     1.7 -Goal "!!i::int. ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)";
     1.8 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
     1.9 -qed "diff_add_eq1";
    1.10 -
    1.11 -Goal "!!i::int. ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))";
    1.12 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
    1.13 -qed "diff_add_eq2";
    1.14 -
    1.15  val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
    1.16                            [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
    1.17  			   zle_iff_zdiff_zle_0] @
    1.18 @@ -171,8 +163,7 @@
    1.19  val mult_1s = [zmult_1, zmult_1_right, zmult_minus1, zmult_minus1_right];
    1.20  
    1.21  (*To perform binary arithmetic*)
    1.22 -val bin_simps = [number_of_add RS sym, add_number_of_left] @ 
    1.23 -                bin_arith_simps @ bin_rel_simps;
    1.24 +val bin_simps = [add_number_of_left] @ bin_arith_simps @ bin_rel_simps;
    1.25  
    1.26  (*To evaluate binary negations of coefficients*)
    1.27  val zminus_simps = NCons_simps @
    1.28 @@ -478,33 +469,11 @@
    1.29  
    1.30  (** Simplification of inequalities involving numerical constants **)
    1.31  
    1.32 -Goal "(w <= z + (#1::int)) = (w<=z | w = z + (#1::int))";
    1.33 -by (arith_tac 1);
    1.34 -qed "zle_add1_eq";
    1.35 -
    1.36  Goal "(w <= z - (#1::int)) = (w<(z::int))";
    1.37  by (arith_tac 1);
    1.38  qed "zle_diff1_eq";
    1.39  Addsimps [zle_diff1_eq];
    1.40  
    1.41 -(*2nd premise can be proved automatically if v is a literal*)
    1.42 -Goal "[| w <= z; #0 <= v |] ==> w <= z + (v::int)";
    1.43 -by (fast_arith_tac 1);
    1.44 -qed "zle_imp_zle_zadd";
    1.45 -
    1.46 -Goal "w <= z ==> w <= z + (#1::int)";
    1.47 -by (fast_arith_tac 1);
    1.48 -qed "zle_imp_zle_zadd1";
    1.49 -
    1.50 -(*2nd premise can be proved automatically if v is a literal*)
    1.51 -Goal "[| w < z; #0 <= v |] ==> w < z + (v::int)";
    1.52 -by (fast_arith_tac 1);
    1.53 -qed "zless_imp_zless_zadd";
    1.54 -
    1.55 -Goal "w < z ==> w < z + (#1::int)";
    1.56 -by (fast_arith_tac 1);
    1.57 -qed "zless_imp_zless_zadd1";
    1.58 -
    1.59  Goal "(w < z + #1) = (w<=(z::int))";
    1.60  by (arith_tac 1);
    1.61  qed "zle_add1_eq_le";
    1.62 @@ -515,20 +484,6 @@
    1.63  qed "zadd_left_cancel0";
    1.64  Addsimps [zadd_left_cancel0];
    1.65  
    1.66 -(*LOOPS as a simprule!*)
    1.67 -Goal "[| w + v < z; #0 <= v |] ==> w < (z::int)";
    1.68 -by (fast_arith_tac 1);
    1.69 -qed "zless_zadd_imp_zless";
    1.70 -
    1.71 -(*LOOPS as a simprule!  Analogous to Suc_lessD*)
    1.72 -Goal "w + #1 < z ==> w < (z::int)";
    1.73 -by (fast_arith_tac 1);
    1.74 -qed "zless_zadd1_imp_zless";
    1.75 -
    1.76 -Goal "w + #-1 = w - (#1::int)";
    1.77 -by (Simp_tac 1);
    1.78 -qed "zplus_minus1_conv";
    1.79 -
    1.80  
    1.81  (* nat *)
    1.82  
    1.83 @@ -602,62 +557,53 @@
    1.84  qed_spec_mp "zdiff_int";
    1.85  
    1.86  
    1.87 -(** Products of signs **)
    1.88 +(*** Some convenient biconditionals for products of signs ***)
    1.89  
    1.90 -Goal "(m::int) < #0 ==> (#0 < m*n) = (n < #0)";
    1.91 -by Auto_tac;
    1.92 -by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2);
    1.93 -by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1);
    1.94 -by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
    1.95 -by (force_tac (claset() addDs [inst "k" "m" zmult_zless_mono1_neg], 
    1.96 -	       simpset()addsimps [order_le_less, zmult_commute]) 1);
    1.97 -qed "neg_imp_zmult_pos_iff";
    1.98 +Goal "[| (#0::int) < i; #0 < j |] ==> #0 < i*j";
    1.99 +by (dtac zmult_zless_mono1 1);
   1.100 +by Auto_tac; 
   1.101 +qed "zmult_pos";
   1.102  
   1.103 -Goal "(m::int) < #0 ==> (m*n < #0) = (#0 < n)";
   1.104 -by Auto_tac;
   1.105 -by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2);
   1.106 -by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1);
   1.107 -by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
   1.108 -by (force_tac (claset() addDs [zmult_zless_mono1_neg], 
   1.109 -	       simpset() addsimps [order_le_less]) 1);
   1.110 -qed "neg_imp_zmult_neg_iff";
   1.111 +Goal "[| i < (#0::int); j < #0 |] ==> #0 < i*j";
   1.112 +by (dtac zmult_zless_mono1_neg 1);
   1.113 +by Auto_tac; 
   1.114 +qed "zmult_neg";
   1.115  
   1.116 -Goal "#0 < (m::int) ==> (m*n < #0) = (n < #0)";
   1.117 -by Auto_tac;
   1.118 -by (force_tac (claset() addDs [zmult_zless_mono1_neg], simpset()) 2);
   1.119 -by (eres_inst_tac [("P", "m * n < #0")] rev_mp 1);
   1.120 -by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
   1.121 -by (force_tac (claset() addDs [zmult_zless_mono1], 
   1.122 -	       simpset() addsimps [order_le_less]) 1);
   1.123 -qed "pos_imp_zmult_neg_iff";
   1.124 +Goal "[| (#0::int) < i; j < #0 |] ==> i*j < #0";
   1.125 +by (dtac zmult_zless_mono1_neg 1);
   1.126 +by Auto_tac; 
   1.127 +qed "zmult_pos_neg";
   1.128  
   1.129 -Goal "#0 < (m::int) ==> (#0 < m*n) = (#0 < n)";
   1.130 -by Auto_tac;
   1.131 -by (force_tac (claset() addDs [zmult_zless_mono1], simpset()) 2);
   1.132 -by (eres_inst_tac [("P", "#0 < m * n")] rev_mp 1);
   1.133 -by (simp_tac (simpset() addsimps [linorder_not_le RS sym]) 1);
   1.134 -by (force_tac (claset() addDs [inst "k" "m" zmult_zless_mono1], 
   1.135 -	       simpset() addsimps [order_le_less, zmult_commute]) 1);
   1.136 -qed "pos_imp_zmult_pos_iff";
   1.137 -
   1.138 -(** <= versions of the theorems above **)
   1.139 +Goal "((#0::int) < x*y) = (#0 < x & #0 < y | x < #0 & y < #0)";
   1.140 +by (auto_tac (claset(), 
   1.141 +              simpset() addsimps [order_le_less, linorder_not_less,
   1.142 +	                          zmult_pos, zmult_neg]));
   1.143 +by (ALLGOALS (rtac ccontr)); 
   1.144 +by (auto_tac (claset(), 
   1.145 +	      simpset() addsimps [order_le_less, linorder_not_less]));
   1.146 +by (ALLGOALS (etac rev_mp)); 
   1.147 +by (ALLGOALS (dtac zmult_pos_neg THEN' assume_tac));
   1.148 +by (auto_tac (claset() addDs [order_less_not_sym], 
   1.149 +              simpset() addsimps [zmult_commute]));  
   1.150 +qed "int_0_less_mult_iff";
   1.151  
   1.152 -Goal "(m::int) < #0 ==> (m*n <= #0) = (#0 <= n)";
   1.153 -by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
   1.154 -				      neg_imp_zmult_pos_iff]) 1);
   1.155 -qed "neg_imp_zmult_nonpos_iff";
   1.156 -
   1.157 -Goal "(m::int) < #0 ==> (#0 <= m*n) = (n <= #0)";
   1.158 -by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
   1.159 -				      neg_imp_zmult_neg_iff]) 1);
   1.160 -qed "neg_imp_zmult_nonneg_iff";
   1.161 +Goal "((#0::int) <= x*y) = (#0 <= x & #0 <= y | x <= #0 & y <= #0)";
   1.162 +by (auto_tac (claset(), 
   1.163 +              simpset() addsimps [order_le_less, linorder_not_less,  
   1.164 +                                  int_0_less_mult_iff]));
   1.165 +qed "int_0_le_mult_iff";
   1.166  
   1.167 -Goal "#0 < (m::int) ==> (m*n <= #0) = (n <= #0)";
   1.168 -by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
   1.169 -				      pos_imp_zmult_pos_iff]) 1);
   1.170 -qed "pos_imp_zmult_nonpos_iff";
   1.171 +Goal "(x*y < (#0::int)) = (#0 < x & y < #0 | x < #0 & #0 < y)";
   1.172 +by (auto_tac (claset(), 
   1.173 +              simpset() addsimps [int_0_le_mult_iff, 
   1.174 +                                  linorder_not_le RS sym]));
   1.175 +by (auto_tac (claset() addDs [order_less_not_sym],  
   1.176 +              simpset() addsimps [linorder_not_le]));
   1.177 +qed "zmult_less_0_iff";
   1.178  
   1.179 -Goal "#0 < (m::int) ==> (#0 <= m*n) = (#0 <= n)";
   1.180 -by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym,
   1.181 -				      pos_imp_zmult_neg_iff]) 1);
   1.182 -qed "pos_imp_zmult_nonneg_iff";
   1.183 +Goal "(x*y <= (#0::int)) = (#0 <= x & y <= #0 | x <= #0 & #0 <= y)";
   1.184 +by (auto_tac (claset() addDs [order_less_not_sym], 
   1.185 +              simpset() addsimps [int_0_less_mult_iff, 
   1.186 +                                  linorder_not_less RS sym]));
   1.187 +qed "zmult_le_0_iff";
   1.188 +
     2.1 --- a/src/HOL/Integ/IntDiv.ML	Wed Jun 14 17:44:43 2000 +0200
     2.2 +++ b/src/HOL/Integ/IntDiv.ML	Wed Jun 14 17:45:01 2000 +0200
     2.3 @@ -115,9 +115,7 @@
     2.4  Goal "#0 <= a --> #0 < b --> quorem ((a, b), posDivAlg (a, b))";
     2.5  by (res_inst_tac [("u", "a"), ("v", "b")] posDivAlg_induct 1);
     2.6  by Auto_tac;
     2.7 -by (ALLGOALS 
     2.8 -    (asm_full_simp_tac (simpset() addsimps [quorem_def,
     2.9 -					    pos_imp_zmult_pos_iff])));
    2.10 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
    2.11  (*base case: a<b*)
    2.12  by (asm_full_simp_tac (simpset() addsimps [posDivAlg_eqn]) 1);
    2.13  (*main argument*)
    2.14 @@ -156,9 +154,7 @@
    2.15  Goal "a < #0 --> #0 < b --> quorem ((a, b), negDivAlg (a, b))";
    2.16  by (res_inst_tac [("u", "a"), ("v", "b")] negDivAlg_induct 1);
    2.17  by Auto_tac;
    2.18 -by (ALLGOALS 
    2.19 -    (asm_full_simp_tac (simpset() addsimps [quorem_def,
    2.20 -					    pos_imp_zmult_pos_iff])));
    2.21 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
    2.22  (*base case: 0<=a+b*)
    2.23  by (asm_full_simp_tac (simpset() addsimps [negDivAlg_eqn]) 1);
    2.24  (*main argument*)
    2.25 @@ -325,13 +321,13 @@
    2.26  Goal "[| (#0::int) < a; a = r + a*q; r < a |] ==> #1 <= q";
    2.27  by (subgoal_tac "#0 < a*q" 1);
    2.28  by (arith_tac 2);
    2.29 -by (asm_full_simp_tac (simpset() addsimps [pos_imp_zmult_pos_iff]) 1);
    2.30 +by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 1);
    2.31  val lemma1 = result();
    2.32  
    2.33  Goal "[| (#0::int) < a; a = r + a*q; #0 <= r |] ==> q <= #1";
    2.34  by (subgoal_tac "#0 <= a*(#1-q)" 1);
    2.35  by (asm_simp_tac (simpset() addsimps [zdiff_zmult_distrib2]) 2);
    2.36 -by (asm_full_simp_tac (simpset() addsimps [pos_imp_zmult_nonneg_iff]) 1);
    2.37 +by (asm_full_simp_tac (simpset() addsimps [int_0_le_mult_iff]) 1);
    2.38  val lemma2 = result();
    2.39  
    2.40  Goal "[| quorem((a,a),(q,r));  a ~= (#0::int) |] ==> q = #1";
    2.41 @@ -494,7 +490,7 @@
    2.42  by (subgoal_tac "#0 <= q'" 1);
    2.43   by (subgoal_tac "#0 < b'*(q' + #1)" 2);
    2.44    by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 3);
    2.45 - by (asm_full_simp_tac (simpset() addsimps [pos_imp_zmult_pos_iff]) 2);
    2.46 + by (asm_full_simp_tac (simpset() addsimps [int_0_less_mult_iff]) 2);
    2.47  by (subgoal_tac "b*q < b*(q' + #1)" 1);
    2.48   by (Asm_full_simp_tac 1);
    2.49  by (subgoal_tac "b*q = r' - r + b'*q'" 1);
    2.50 @@ -523,7 +519,7 @@
    2.51  by (subgoal_tac "q' < #0" 1);
    2.52   by (subgoal_tac "b'*q' < #0" 2);
    2.53    by (arith_tac 3);
    2.54 - by (asm_full_simp_tac (simpset() addsimps [pos_imp_zmult_neg_iff]) 2);
    2.55 + by (asm_full_simp_tac (simpset() addsimps [zmult_less_0_iff]) 2);
    2.56  by (subgoal_tac "b*q' < b*(q + #1)" 1);
    2.57   by (Asm_full_simp_tac 1);
    2.58  by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
    2.59 @@ -683,15 +679,13 @@
    2.60  Goal "[| (#0::int) < c;   b < r;  r <= #0 |] ==> b * (q mod c) + r <= #0";
    2.61  by (subgoal_tac "b * (q mod c) <= #0" 1);
    2.62  by (arith_tac 1);
    2.63 -by (asm_simp_tac (simpset() addsimps [neg_imp_zmult_nonpos_iff, 
    2.64 -				      pos_mod_sign]) 1);
    2.65 +by (asm_simp_tac (simpset() addsimps [zmult_le_0_iff, pos_mod_sign]) 1);
    2.66  val lemma2 = result();
    2.67  
    2.68  Goal "[| (#0::int) < c;  #0 <= r;  r < b |] ==> #0 <= b * (q mod c) + r";
    2.69  by (subgoal_tac "#0 <= b * (q mod c)" 1);
    2.70  by (arith_tac 1);
    2.71 -by (asm_simp_tac
    2.72 -    (simpset() addsimps [pos_imp_zmult_nonneg_iff, pos_mod_sign]) 1);
    2.73 +by (asm_simp_tac (simpset() addsimps [int_0_le_mult_iff, pos_mod_sign]) 1);
    2.74  val lemma3 = result();
    2.75  
    2.76  Goal "[| (#0::int) < c; #0 <= r; r < b |] ==> b * (q mod c) + r < b * c";
    2.77 @@ -712,8 +706,7 @@
    2.78      (claset(),
    2.79       simpset() addsimps zmult_ac@
    2.80                          [zmod_zdiv_equality, quorem_def, linorder_neq_iff,
    2.81 -			 pos_imp_zmult_pos_iff,
    2.82 -			 neg_imp_zmult_pos_iff,
    2.83 +			 int_0_less_mult_iff,
    2.84  			 zadd_zmult_distrib2 RS sym,
    2.85  			 lemma1, lemma2, lemma3, lemma4]));
    2.86  val lemma = result();
    2.87 @@ -816,12 +809,12 @@
    2.88  by (subgoal_tac "#0 <= b mod a" 1);
    2.89   by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2);
    2.90  by (arith_tac 1);
    2.91 -qed "pos_zdiv_times_2";
    2.92 +qed "pos_zdiv_mult_2";
    2.93  
    2.94  
    2.95  Goal "a <= (#0::int) ==> (#1 + #2*b) div (#2*a) = (b+#1) div a";
    2.96  by (subgoal_tac "(#1 + #2*(-b-#1)) div (#2 * (-a)) = (-b-#1) div (-a)" 1);
    2.97 -by (rtac pos_zdiv_times_2 2);
    2.98 +by (rtac pos_zdiv_mult_2 2);
    2.99  by (auto_tac (claset(),
   2.100  	      simpset() addsimps [zmult_zminus_right]));
   2.101  by (subgoal_tac "(#-1 - (#2 * b)) = - (#1 + (#2 * b))" 1);
   2.102 @@ -829,7 +822,7 @@
   2.103  by (asm_full_simp_tac (HOL_ss
   2.104  		       addsimps [zdiv_zminus_zminus, zdiff_def,
   2.105  				 zminus_zadd_distrib RS sym]) 1);
   2.106 -qed "neg_zdiv_times_2";
   2.107 +qed "neg_zdiv_mult_2";
   2.108  
   2.109  
   2.110  (*Not clear why this must be proved separately; probably number_of causes
   2.111 @@ -847,7 +840,7 @@
   2.112  by (asm_simp_tac (simpset()
   2.113                    delsimps bin_arith_extra_simps@bin_rel_simps
   2.114  		  addsimps [zdiv_zmult_zmult1,
   2.115 -			    pos_zdiv_times_2, lemma, neg_zdiv_times_2]) 1);
   2.116 +			    pos_zdiv_mult_2, lemma, neg_zdiv_mult_2]) 1);
   2.117  qed "zdiv_number_of_BIT";
   2.118  
   2.119  Addsimps [zdiv_number_of_BIT];
   2.120 @@ -878,13 +871,13 @@
   2.121  by (subgoal_tac "#0 <= b mod a" 1);
   2.122   by (asm_simp_tac (simpset() addsimps [pos_mod_sign]) 2);
   2.123  by (arith_tac 1);
   2.124 -qed "pos_zmod_times_2";
   2.125 +qed "pos_zmod_mult_2";
   2.126  
   2.127  
   2.128  Goal "a <= (#0::int) ==> (#1 + #2*b) mod (#2*a) = #2 * ((b+#1) mod a) - #1";
   2.129  by (subgoal_tac 
   2.130      "(#1 + #2*(-b-#1)) mod (#2*(-a)) = #1 + #2*((-b-#1) mod (-a))" 1);
   2.131 -by (rtac pos_zmod_times_2 2);
   2.132 +by (rtac pos_zmod_mult_2 2);
   2.133  by (auto_tac (claset(),
   2.134  	      simpset() addsimps [zmult_zminus_right]));
   2.135  by (subgoal_tac "(#-1 - (#2 * b)) = - (#1 + (#2 * b))" 1);
   2.136 @@ -894,7 +887,7 @@
   2.137  				 zminus_zadd_distrib RS sym]) 1);
   2.138  by (dtac (zminus_equation RS iffD1 RS sym) 1);
   2.139  by Auto_tac;
   2.140 -qed "neg_zmod_times_2";
   2.141 +qed "neg_zmod_mult_2";
   2.142  
   2.143  Goal "number_of (v BIT b) mod number_of (w BIT False) = \
   2.144  \         (if b then \
   2.145 @@ -907,7 +900,7 @@
   2.146  by (asm_simp_tac (simpset()
   2.147  		  delsimps bin_arith_extra_simps@bin_rel_simps
   2.148  		  addsimps [zmod_zmult_zmult1,
   2.149 -			    pos_zmod_times_2, lemma, neg_zmod_times_2]) 1);
   2.150 +			    pos_zmod_mult_2, lemma, neg_zmod_mult_2]) 1);
   2.151  qed "zmod_number_of_BIT";
   2.152  
   2.153  Addsimps [zmod_number_of_BIT];