author | paulson |
Fri, 02 Nov 2001 17:55:24 +0100 | |
changeset 12018 | ec054019c910 |
parent 11868 | 56db9f3a6b3e |
child 12486 | 0ed8bdd883e0 |
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 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
6 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11868
diff
changeset
|
7 |
Goal "x - - y = x + (y::int)"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11868
diff
changeset
|
8 |
by (Simp_tac 1); |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11868
diff
changeset
|
9 |
qed "int_diff_minus_eq"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11868
diff
changeset
|
10 |
Addsimps [int_diff_minus_eq]; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11868
diff
changeset
|
11 |
|
9269 | 12 |
Goal "abs(abs(x::int)) = abs(x)"; |
13 |
by(arith_tac 1); |
|
9214 | 14 |
qed "abs_abs"; |
15 |
Addsimps [abs_abs]; |
|
16 |
||
9269 | 17 |
Goal "abs(-(x::int)) = abs(x)"; |
18 |
by(arith_tac 1); |
|
9214 | 19 |
qed "abs_minus"; |
20 |
Addsimps [abs_minus]; |
|
21 |
||
9269 | 22 |
Goal "abs(x+y) <= abs(x) + abs(y::int)"; |
23 |
by(arith_tac 1); |
|
24 |
qed "triangle_ineq"; |
|
25 |
||
9214 | 26 |
|
10228 | 27 |
(*** Intermediate value theorems ***) |
28 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
29 |
Goal "(ALL i<n::nat. abs(f(i+1) - f i) <= 1) --> \ |
10228 | 30 |
\ f 0 <= k --> k <= f n --> (EX i <= n. f i = (k::int))"; |
31 |
by(induct_tac "n" 1); |
|
32 |
by(Asm_simp_tac 1); |
|
33 |
by(strip_tac 1); |
|
34 |
by(etac impE 1); |
|
35 |
by(Asm_full_simp_tac 1); |
|
36 |
by(eres_inst_tac [("x","n")] allE 1); |
|
37 |
by(Asm_full_simp_tac 1); |
|
38 |
by(case_tac "k = f(n+1)" 1); |
|
39 |
by(Force_tac 1); |
|
40 |
by(etac impE 1); |
|
10702 | 41 |
by(asm_full_simp_tac (simpset() addsimps [zabs_def] |
42 |
addsplits [split_if_asm]) 1); |
|
10228 | 43 |
by(arith_tac 1); |
44 |
by(blast_tac (claset() addIs [le_SucI]) 1); |
|
45 |
val lemma = result(); |
|
46 |
||
11770 | 47 |
bind_thm("nat0_intermed_int_val", ObjectLogic.rulify_no_asm lemma); |
10228 | 48 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
49 |
Goal "[| !i. m <= i & i < n --> abs(f(i + 1::nat) - f i) <= 1; m < n; \ |
10228 | 50 |
\ f m <= k; k <= f n |] ==> ? i. m <= i & i <= n & f i = (k::int)"; |
51 |
by(cut_inst_tac [("n","n-m"),("f", "%i. f(i+m)"),("k","k")]lemma 1); |
|
52 |
by(Asm_full_simp_tac 1); |
|
53 |
by(etac impE 1); |
|
54 |
by(strip_tac 1); |
|
55 |
by(eres_inst_tac [("x","i+m")] allE 1); |
|
56 |
by(arith_tac 1); |
|
57 |
by(etac exE 1); |
|
58 |
by(res_inst_tac [("x","i+m")] exI 1); |
|
59 |
by(arith_tac 1); |
|
60 |
qed "nat_intermed_int_val"; |
|
61 |
||
62 |
||
9063 | 63 |
(*** Some convenient biconditionals for products of signs ***) |
7707 | 64 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
65 |
Goal "[| (0::int) < i; 0 < j |] ==> 0 < i*j"; |
9063 | 66 |
by (dtac zmult_zless_mono1 1); |
67 |
by Auto_tac; |
|
68 |
qed "zmult_pos"; |
|
7707 | 69 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
70 |
Goal "[| i < (0::int); j < 0 |] ==> 0 < i*j"; |
9063 | 71 |
by (dtac zmult_zless_mono1_neg 1); |
72 |
by Auto_tac; |
|
73 |
qed "zmult_neg"; |
|
7707 | 74 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
75 |
Goal "[| (0::int) < i; j < 0 |] ==> i*j < 0"; |
9063 | 76 |
by (dtac zmult_zless_mono1_neg 1); |
77 |
by Auto_tac; |
|
78 |
qed "zmult_pos_neg"; |
|
7707 | 79 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
80 |
Goal "((0::int) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"; |
9063 | 81 |
by (auto_tac (claset(), |
82 |
simpset() addsimps [order_le_less, linorder_not_less, |
|
83 |
zmult_pos, zmult_neg])); |
|
84 |
by (ALLGOALS (rtac ccontr)); |
|
85 |
by (auto_tac (claset(), |
|
86 |
simpset() addsimps [order_le_less, linorder_not_less])); |
|
87 |
by (ALLGOALS (etac rev_mp)); |
|
88 |
by (ALLGOALS (dtac zmult_pos_neg THEN' assume_tac)); |
|
89 |
by (auto_tac (claset() addDs [order_less_not_sym], |
|
90 |
simpset() addsimps [zmult_commute])); |
|
91 |
qed "int_0_less_mult_iff"; |
|
7707 | 92 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
93 |
Goal "((0::int) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)"; |
9063 | 94 |
by (auto_tac (claset(), |
95 |
simpset() addsimps [order_le_less, linorder_not_less, |
|
96 |
int_0_less_mult_iff])); |
|
97 |
qed "int_0_le_mult_iff"; |
|
7707 | 98 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
99 |
Goal "(x*y < (0::int)) = (0 < x & y < 0 | x < 0 & 0 < y)"; |
9063 | 100 |
by (auto_tac (claset(), |
101 |
simpset() addsimps [int_0_le_mult_iff, |
|
102 |
linorder_not_le RS sym])); |
|
103 |
by (auto_tac (claset() addDs [order_less_not_sym], |
|
104 |
simpset() addsimps [linorder_not_le])); |
|
105 |
qed "zmult_less_0_iff"; |
|
7707 | 106 |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
107 |
Goal "(x*y <= (0::int)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)"; |
9063 | 108 |
by (auto_tac (claset() addDs [order_less_not_sym], |
109 |
simpset() addsimps [int_0_less_mult_iff, |
|
110 |
linorder_not_less RS sym])); |
|
111 |
qed "zmult_le_0_iff"; |
|
9509 | 112 |
|
10476 | 113 |
Goal "abs (x * y) = abs x * abs (y::int)"; |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
114 |
by (simp_tac (simpset () delsimps [thm "number_of_reorient"] addsplits [zabs_split] |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
115 |
addsplits [zabs_split] |
10702 | 116 |
addsimps [zmult_less_0_iff, zle_def]) 1); |
10476 | 117 |
qed "abs_mult"; |
118 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
119 |
Goal "(abs x = 0) = (x = (0::int))"; |
10476 | 120 |
by (simp_tac (simpset () addsplits [zabs_split]) 1); |
121 |
qed "abs_eq_0"; |
|
122 |
AddIffs [abs_eq_0]; |
|
123 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
124 |
Goal "(0 < abs x) = (x ~= (0::int))"; |
10702 | 125 |
by (simp_tac (simpset () addsplits [zabs_split]) 1); |
126 |
by (arith_tac 1); |
|
127 |
qed "zero_less_abs_iff"; |
|
128 |
AddIffs [zero_less_abs_iff]; |
|
129 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
130 |
Goal "0 <= x * (x::int)"; |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
131 |
by (subgoal_tac "(- x) * x <= 0" 1); |
10476 | 132 |
by (Asm_full_simp_tac 1); |
133 |
by (simp_tac (HOL_basic_ss addsimps [zmult_le_0_iff]) 1); |
|
134 |
by Auto_tac; |
|
135 |
qed "square_nonzero"; |
|
136 |
Addsimps [square_nonzero]; |
|
137 |
AddIs [square_nonzero]; |
|
138 |
||
139 |
||
9509 | 140 |
(*** Products and 1, by T. M. Rasmussen ***) |
141 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
142 |
Goal "(m = m*(n::int)) = (n = 1 | m = 0)"; |
9509 | 143 |
by Auto_tac; |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
144 |
by (subgoal_tac "m*1 = m*n" 1); |
9633
a71a83253997
better rules for cancellation of common factors across comparisons
paulson
parents:
9509
diff
changeset
|
145 |
by (dtac (zmult_cancel1 RS iffD1) 1); |
9509 | 146 |
by Auto_tac; |
147 |
qed "zmult_eq_self_iff"; |
|
148 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
149 |
Goal "[| 1 < m; 1 < n |] ==> 1 < m*(n::int)"; |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
150 |
by (res_inst_tac [("y","1*n")] order_less_trans 1); |
9509 | 151 |
by (rtac zmult_zless_mono1 2); |
152 |
by (ALLGOALS Asm_simp_tac); |
|
153 |
qed "zless_1_zmult"; |
|
154 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
155 |
Goal "[| 0 < n; n ~= 1 |] ==> 1 < (n::int)"; |
9509 | 156 |
by (arith_tac 1); |
157 |
val lemma = result(); |
|
158 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
159 |
Goal "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"; |
9509 | 160 |
by Auto_tac; |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
161 |
by (case_tac "m=1" 1); |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
162 |
by (case_tac "n=1" 2); |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
163 |
by (case_tac "m=1" 4); |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
164 |
by (case_tac "n=1" 5); |
9509 | 165 |
by Auto_tac; |
166 |
by distinct_subgoals_tac; |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
167 |
by (subgoal_tac "1<m*n" 1); |
9509 | 168 |
by (Asm_full_simp_tac 1); |
169 |
by (rtac zless_1_zmult 1); |
|
170 |
by (ALLGOALS (rtac lemma)); |
|
171 |
by Auto_tac; |
|
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
172 |
by (subgoal_tac "0<m*n" 1); |
9509 | 173 |
by (Asm_simp_tac 2); |
174 |
by (dtac (int_0_less_mult_iff RS iffD1) 1); |
|
175 |
by Auto_tac; |
|
176 |
qed "pos_zmult_eq_1_iff"; |
|
177 |
||
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
178 |
Goal "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"; |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
179 |
by (case_tac "0<m" 1); |
9509 | 180 |
by (asm_simp_tac (simpset() addsimps [pos_zmult_eq_1_iff]) 1); |
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
181 |
by (case_tac "m=0" 1); |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
182 |
by (asm_simp_tac (simpset () delsimps [thm "number_of_reorient"]) 1); |
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11770
diff
changeset
|
183 |
by (subgoal_tac "0 < -m" 1); |
9509 | 184 |
by (arith_tac 2); |
185 |
by (dres_inst_tac [("n","-n")] pos_zmult_eq_1_iff 1); |
|
186 |
by Auto_tac; |
|
187 |
qed "zmult_eq_1_iff"; |
|
188 |