| author | wenzelm |
| Fri, 06 Oct 2000 17:35:58 +0200 | |
| changeset 10168 | 50be659d4222 |
| parent 9633 | a71a83253997 |
| child 10228 | e653cb933293 |
| permissions | -rw-r--r-- |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9269
diff
changeset
|
1 |
(* Title: HOL/Integ/IntArith.ML |
| 7707 | 2 |
ID: $Id$ |
3 |
Authors: Larry Paulson and Tobias Nipkow |
|
4 |
*) |
|
5 |
||
| 9269 | 6 |
Goal "abs(abs(x::int)) = abs(x)"; |
7 |
by(arith_tac 1); |
|
| 9214 | 8 |
qed "abs_abs"; |
9 |
Addsimps [abs_abs]; |
|
10 |
||
| 9269 | 11 |
Goal "abs(-(x::int)) = abs(x)"; |
12 |
by(arith_tac 1); |
|
| 9214 | 13 |
qed "abs_minus"; |
14 |
Addsimps [abs_minus]; |
|
15 |
||
| 9269 | 16 |
Goal "abs(x+y) <= abs(x) + abs(y::int)"; |
17 |
by(arith_tac 1); |
|
18 |
qed "triangle_ineq"; |
|
19 |
||
| 9214 | 20 |
|
| 9063 | 21 |
(*** Some convenient biconditionals for products of signs ***) |
| 7707 | 22 |
|
| 9063 | 23 |
Goal "[| (#0::int) < i; #0 < j |] ==> #0 < i*j"; |
24 |
by (dtac zmult_zless_mono1 1); |
|
25 |
by Auto_tac; |
|
26 |
qed "zmult_pos"; |
|
| 7707 | 27 |
|
| 9063 | 28 |
Goal "[| i < (#0::int); j < #0 |] ==> #0 < i*j"; |
29 |
by (dtac zmult_zless_mono1_neg 1); |
|
30 |
by Auto_tac; |
|
31 |
qed "zmult_neg"; |
|
| 7707 | 32 |
|
| 9063 | 33 |
Goal "[| (#0::int) < i; j < #0 |] ==> i*j < #0"; |
34 |
by (dtac zmult_zless_mono1_neg 1); |
|
35 |
by Auto_tac; |
|
36 |
qed "zmult_pos_neg"; |
|
| 7707 | 37 |
|
| 9063 | 38 |
Goal "((#0::int) < x*y) = (#0 < x & #0 < y | x < #0 & y < #0)"; |
39 |
by (auto_tac (claset(), |
|
40 |
simpset() addsimps [order_le_less, linorder_not_less, |
|
41 |
zmult_pos, zmult_neg])); |
|
42 |
by (ALLGOALS (rtac ccontr)); |
|
43 |
by (auto_tac (claset(), |
|
44 |
simpset() addsimps [order_le_less, linorder_not_less])); |
|
45 |
by (ALLGOALS (etac rev_mp)); |
|
46 |
by (ALLGOALS (dtac zmult_pos_neg THEN' assume_tac)); |
|
47 |
by (auto_tac (claset() addDs [order_less_not_sym], |
|
48 |
simpset() addsimps [zmult_commute])); |
|
49 |
qed "int_0_less_mult_iff"; |
|
| 7707 | 50 |
|
| 9063 | 51 |
Goal "((#0::int) <= x*y) = (#0 <= x & #0 <= y | x <= #0 & y <= #0)"; |
52 |
by (auto_tac (claset(), |
|
53 |
simpset() addsimps [order_le_less, linorder_not_less, |
|
54 |
int_0_less_mult_iff])); |
|
55 |
qed "int_0_le_mult_iff"; |
|
| 7707 | 56 |
|
| 9063 | 57 |
Goal "(x*y < (#0::int)) = (#0 < x & y < #0 | x < #0 & #0 < y)"; |
58 |
by (auto_tac (claset(), |
|
59 |
simpset() addsimps [int_0_le_mult_iff, |
|
60 |
linorder_not_le RS sym])); |
|
61 |
by (auto_tac (claset() addDs [order_less_not_sym], |
|
62 |
simpset() addsimps [linorder_not_le])); |
|
63 |
qed "zmult_less_0_iff"; |
|
| 7707 | 64 |
|
| 9063 | 65 |
Goal "(x*y <= (#0::int)) = (#0 <= x & y <= #0 | x <= #0 & #0 <= y)"; |
66 |
by (auto_tac (claset() addDs [order_less_not_sym], |
|
67 |
simpset() addsimps [int_0_less_mult_iff, |
|
68 |
linorder_not_less RS sym])); |
|
69 |
qed "zmult_le_0_iff"; |
|
| 9509 | 70 |
|
71 |
||
72 |
(*** Products and 1, by T. M. Rasmussen ***) |
|
73 |
||
74 |
Goal "(m = m*(n::int)) = (n = #1 | m = #0)"; |
|
75 |
by Auto_tac; |
|
|
9633
a71a83253997
better rules for cancellation of common factors across comparisons
paulson
parents:
9509
diff
changeset
|
76 |
by (subgoal_tac "m*#1 = m*n" 1); |
|
a71a83253997
better rules for cancellation of common factors across comparisons
paulson
parents:
9509
diff
changeset
|
77 |
by (dtac (zmult_cancel1 RS iffD1) 1); |
| 9509 | 78 |
by Auto_tac; |
79 |
qed "zmult_eq_self_iff"; |
|
80 |
||
81 |
Goal "[| #1 < m; #1 < n |] ==> #1 < m*(n::int)"; |
|
82 |
by (res_inst_tac [("z2.0","#1*n")] zless_trans 1);
|
|
83 |
by (rtac zmult_zless_mono1 2); |
|
84 |
by (ALLGOALS Asm_simp_tac); |
|
85 |
qed "zless_1_zmult"; |
|
86 |
||
87 |
Goal "[| #0 < n; n ~= #1 |] ==> #1 < (n::int)"; |
|
88 |
by (arith_tac 1); |
|
89 |
val lemma = result(); |
|
90 |
||
91 |
Goal "#0 < (m::int) ==> (m * n = #1) = (m = #1 & n = #1)"; |
|
92 |
by Auto_tac; |
|
93 |
by (case_tac "m=#1" 1); |
|
94 |
by (case_tac "n=#1" 2); |
|
95 |
by (case_tac "m=#1" 4); |
|
96 |
by (case_tac "n=#1" 5); |
|
97 |
by Auto_tac; |
|
98 |
by distinct_subgoals_tac; |
|
99 |
by (subgoal_tac "#1<m*n" 1); |
|
100 |
by (Asm_full_simp_tac 1); |
|
101 |
by (rtac zless_1_zmult 1); |
|
102 |
by (ALLGOALS (rtac lemma)); |
|
103 |
by Auto_tac; |
|
104 |
by (subgoal_tac "#0<m*n" 1); |
|
105 |
by (Asm_simp_tac 2); |
|
106 |
by (dtac (int_0_less_mult_iff RS iffD1) 1); |
|
107 |
by Auto_tac; |
|
108 |
qed "pos_zmult_eq_1_iff"; |
|
109 |
||
110 |
Goal "(m*n = (#1::int)) = ((m = #1 & n = #1) | (m = #-1 & n = #-1))"; |
|
111 |
by (case_tac "#0<m" 1); |
|
112 |
by (asm_simp_tac (simpset() addsimps [pos_zmult_eq_1_iff]) 1); |
|
113 |
by (case_tac "m=#0" 1); |
|
114 |
by (Asm_simp_tac 1); |
|
115 |
by (subgoal_tac "#0 < -m" 1); |
|
116 |
by (arith_tac 2); |
|
117 |
by (dres_inst_tac [("n","-n")] pos_zmult_eq_1_iff 1);
|
|
118 |
by Auto_tac; |
|
119 |
qed "zmult_eq_1_iff"; |
|
120 |