author paulson Thu, 01 Jul 1999 10:35:35 +0200 changeset 6866 f795b63139ec parent 6865 5577ffe4c2f1 child 6867 7cb9d3250db7
many new theorems concerning multiplication and (in)equations
 src/HOL/Integ/Int.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Integ/Int.ML	Thu Jul 01 10:33:50 1999 +0200
+++ b/src/HOL/Integ/Int.ML	Thu Jul 01 10:35:35 1999 +0200
@@ -4,6 +4,8 @@

Type "int" is a linear order
+
+And many further lemmas
*)

Goal "(w<z) = neg(w-z)";
@@ -214,7 +216,18 @@
by Auto_tac;
qed "neg_nat";

-(* a case theorem distinguishing positive and negative int *)
+(*An alternative condition is  int 0 <= w  *)
+Goal "int 0 < z ==> (nat w < nat z) = (w < z)";
+by (stac (zless_int RS sym) 1);
+by (asm_simp_tac (simpset() addsimps [not_neg_nat, not_neg_eq_ge_nat0,
+				      order_le_less]) 1);
+by (case_tac "neg w" 1);
+by (asm_simp_tac (simpset() addsimps [not_neg_nat]) 2);
+by (asm_full_simp_tac (simpset() addsimps [neg_eq_less_nat0, neg_nat]) 1);
+by (blast_tac (claset() addIs [order_less_trans]) 1);
+qed "zless_nat";
+
+(* a case theorem distinguishing non-negative and negative int *)

val prems = Goal "[|!! n. P (int n); !! n. P (- (int (Suc n))) |] ==> P z";
by (case_tac "neg z" 1);
@@ -225,3 +238,166 @@

fun int_case_tac x = res_inst_tac [("z",x)] int_cases;

+
+(*** Monotonicity of Multiplication ***)
+
+Goal "i <= (j::int) ==> i * int k <= j * int k";
+by (induct_tac "k" 1);
+by (stac int_Suc_int_1 2);
+by (ALLGOALS
+val lemma = result();
+
+Goal "[| i <= j;  int 0 <= k |] ==> i*k <= j*k";
+by (res_inst_tac [("t", "k")] (not_neg_nat RS subst) 1);
+by (etac lemma 2);
+by (full_simp_tac (simpset() addsimps [not_neg_eq_ge_nat0]) 1);
+qed "zmult_zle_mono1";
+
+Goal "[| i <= j;  k <= int 0 |] ==> j*k <= i*k";
+by (rtac (zminus_zle_zminus RS iffD1) 1);
+by (asm_simp_tac (simpset() addsimps [zmult_zminus_right RS sym,
+				      zmult_zle_mono1, zle_zminus]) 1);
+qed "zmult_zle_mono1_neg";
+
+(*<=monotonicity, BOTH arguments*)
+Goal "[| i <= j;  k <= l;  int 0 <= j;  int 0 <= k |] ==> i*k <= j*l";
+by (etac (zmult_zle_mono1 RS order_trans) 1);
+by (assume_tac 1);
+by (rtac order_trans 1);
+by (stac zmult_commute 2);
+by (etac zmult_zle_mono1 2);
+by (assume_tac 2);
+by (simp_tac (simpset() addsimps [zmult_commute]) 1);
+qed "zmult_zle_mono";
+
+
+(** strict, in 1st argument; proof is by induction on k>0 **)
+
+Goal "i<j ==> 0<k --> int k * i < int k * j";
+by (induct_tac "k" 1);
+by (stac int_Suc_int_1 2);
+by (case_tac "n=0" 2);
+by (ALLGOALS (asm_full_simp_tac
+				   order_le_less])));
+val lemma = result() RS mp;
+
+Goal "[| i<j;  int 0 < k |] ==> k*i < k*j";
+by (res_inst_tac [("t", "k")] (not_neg_nat RS subst) 1);
+by (etac lemma 2);
+				      order_le_less]) 1);
+by (forward_tac [zless_nat RS iffD2] 1);
+by Auto_tac;
+qed "zmult_zless_mono2";
+
+Goal "[| i<j;  int 0 < k |] ==> i*k < j*k";
+by (dtac zmult_zless_mono2 1);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [zmult_commute])));
+qed "zmult_zless_mono1";
+
+Goal "[| i<j;  k < int 0 |] ==> j*k < i*k";
+by (rtac (zminus_zless_zminus RS iffD1) 1);
+by (asm_simp_tac (simpset() addsimps [zmult_zminus_right RS sym,
+				      zmult_zless_mono1, zless_zminus]) 1);
+qed "zmult_zless_mono1_neg";
+
+Goal "[| i<j;  k < int 0 |] ==> k*j < k*i";
+by (rtac (zminus_zless_zminus RS iffD1) 1);
+by (asm_simp_tac (simpset() addsimps [zmult_zminus RS sym,
+				      zmult_zless_mono2, zless_zminus]) 1);
+qed "zmult_zless_mono2_neg";
+
+
+(** Products of signs.  Useful?  **)
+
+Goal "[| m < int 0;  n < int 0 |] ==> int 0 < m*n";
+by (dtac zmult_zless_mono1_neg 1);
+by Auto_tac;
+qed "neg_times_neg_is_pos";
+
+Goal "[| m < int 0;  int 0 < n |] ==> m*n < int 0";
+by (dtac zmult_zless_mono1 1);
+by Auto_tac;
+qed "neg_times_pos_is_neg";
+
+Goal "[| int 0 < m;  n < int 0 |] ==> m*n < int 0";
+by (dtac zmult_zless_mono1_neg 1);
+by Auto_tac;
+qed "pos_times_neg_is_neg";
+
+Goal "[| int 0 < m;  int 0 < n |] ==> int 0 < m*n";
+by (dtac zmult_zless_mono1 1);
+by Auto_tac;
+qed "pos_times_pos_is_pos";
+
+Goal "(m*n = int 0) = (m = int 0 | n = int 0)";
+by (case_tac "m < int 0" 1);
+by (auto_tac (claset(),
+				  linorder_neq_iff]));
+by (REPEAT
+    (force_tac (claset() addDs [zmult_zless_mono1_neg, zmult_zless_mono1],
+		simpset()) 1));
+qed "zmult_eq_iff";
+
+
+Goal "int 0 < k ==> (m*k < n*k) = (m<n)";
+by (cut_facts_tac [linorder_less_linear] 1);
+qed "zmult_zless_cancel2";
+
+Goal "int 0 < k ==> (k*m < k*n) = (m<n)";
+by (dtac zmult_zless_cancel2 1);
+by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 1);
+qed "zmult_zless_cancel1";
+
+Goal "k < int 0 ==> (m*k < n*k) = (n<m)";
+by (cut_facts_tac [linorder_less_linear] 1);
+qed "zmult_zless_cancel2_neg";
+
+Goal "k < int 0 ==> (k*m < k*n) = (n<m)";
+by (dtac zmult_zless_cancel2_neg 1);
+by (asm_full_simp_tac (simpset() addsimps [zmult_commute]) 1);
+qed "zmult_zless_cancel1_neg";
+
+Goal "int 0 < k ==> (m*k <= n*k) = (m<=n)";
+by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+qed "zmult_zle_cancel2";
+
+Goal "int 0 < k ==> (k*m <= k*n) = (m<=n)";
+by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+qed "zmult_zle_cancel1";
+
+Goal "k < int 0 ==> (m*k <= n*k) = (n<=m)";
+by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+qed "zmult_zle_cancel2_neg";
+
+Goal "k < int 0 ==> (k*m <= k*n) = (n<=m)";
+by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
+qed "zmult_zle_cancel1_neg";
+
+Goal "k ~= int 0 ==> (m*k = n*k) = (m=n)";
+by (cut_facts_tac [linorder_less_linear] 1);
+by Safe_tac;
+by (assume_tac 2);
+by (REPEAT
+    (force_tac (claset() addD2 ("mono_neg", zmult_zless_mono1_neg)