author | paulson |
Tue, 27 Jan 2004 15:39:51 +0100 | |
changeset 14365 | 3d4df8c166ae |
parent 14353 | 79f9fbef9106 |
permissions | -rw-r--r-- |
13577 | 1 |
(* Title: Integ/Int.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
*) |
|
6 |
||
14271 | 7 |
header {*Type "int" is an Ordered Ring and Other Lemmas*} |
14264 | 8 |
|
9 |
theory Int = IntDef: |
|
13577 | 10 |
|
11 |
constdefs |
|
14264 | 12 |
nat :: "int => nat" |
13 |
"nat(Z) == if neg Z then 0 else (THE m. Z = int m)" |
|
13577 | 14 |
|
15 |
defs (overloaded) |
|
14264 | 16 |
zabs_def: "abs(i::int) == if i < 0 then -i else i" |
17 |
||
18 |
||
19 |
lemma int_0 [simp]: "int 0 = (0::int)" |
|
20 |
by (simp add: Zero_int_def) |
|
21 |
||
22 |
lemma int_1 [simp]: "int 1 = 1" |
|
23 |
by (simp add: One_int_def) |
|
24 |
||
25 |
lemma int_Suc0_eq_1: "int (Suc 0) = 1" |
|
26 |
by (simp add: One_int_def One_nat_def) |
|
27 |
||
28 |
lemma neg_eq_less_0: "neg x = (x < 0)" |
|
29 |
by (unfold zdiff_def zless_def, auto) |
|
30 |
||
14266 | 31 |
lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)" |
14264 | 32 |
apply (unfold zle_def) |
33 |
apply (simp add: neg_eq_less_0) |
|
34 |
done |
|
35 |
||
36 |
subsection{*To simplify inequalities when Numeral1 can get simplified to 1*} |
|
37 |
||
38 |
lemma not_neg_0: "~ neg 0" |
|
39 |
by (simp add: One_int_def neg_eq_less_0) |
|
40 |
||
41 |
lemma not_neg_1: "~ neg 1" |
|
42 |
by (simp add: One_int_def neg_eq_less_0) |
|
43 |
||
44 |
lemma iszero_0: "iszero 0" |
|
45 |
by (simp add: iszero_def) |
|
46 |
||
47 |
lemma not_iszero_1: "~ iszero 1" |
|
48 |
by (simp only: Zero_int_def One_int_def One_nat_def iszero_def int_int_eq) |
|
49 |
||
50 |
||
14271 | 51 |
subsection{*nat: magnitide of an integer, as a natural number*} |
52 |
||
53 |
lemma nat_int [simp]: "nat(int n) = n" |
|
54 |
by (unfold nat_def, auto) |
|
55 |
||
56 |
lemma nat_zero [simp]: "nat 0 = 0" |
|
57 |
apply (unfold Zero_int_def) |
|
58 |
apply (rule nat_int) |
|
59 |
done |
|
60 |
||
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
61 |
lemma neg_nat: "neg z ==> nat z = 0" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
62 |
by (unfold nat_def, auto) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
63 |
|
14271 | 64 |
lemma not_neg_nat: "~ neg z ==> int (nat z) = z" |
65 |
apply (drule not_neg_eq_ge_0 [THEN iffD1]) |
|
66 |
apply (drule zle_imp_zless_or_eq) |
|
67 |
apply (auto simp add: zless_iff_Suc_zadd) |
|
68 |
done |
|
69 |
||
70 |
lemma nat_0_le [simp]: "0 \<le> z ==> int (nat z) = z" |
|
71 |
by (simp add: neg_eq_less_0 zle_def not_neg_nat) |
|
72 |
||
73 |
lemma nat_le_0 [simp]: "z \<le> 0 ==> nat z = 0" |
|
74 |
by (auto simp add: order_le_less neg_eq_less_0 zle_def neg_nat) |
|
75 |
||
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
76 |
text{*An alternative condition is @{term "0 \<le> w"} *} |
14271 | 77 |
lemma nat_mono_iff: "0 < z ==> (nat w < nat z) = (w < z)" |
78 |
apply (subst zless_int [symmetric]) |
|
79 |
apply (simp (no_asm_simp) add: not_neg_nat not_neg_eq_ge_0 order_le_less) |
|
80 |
apply (case_tac "neg w") |
|
81 |
apply (simp add: neg_eq_less_0 neg_nat) |
|
82 |
apply (blast intro: order_less_trans) |
|
83 |
apply (simp add: not_neg_nat) |
|
84 |
done |
|
85 |
||
86 |
lemma zless_nat_conj: "(nat w < nat z) = (0 < z & w < z)" |
|
87 |
apply (case_tac "0 < z") |
|
88 |
apply (auto simp add: nat_mono_iff linorder_not_less) |
|
89 |
done |
|
90 |
||
91 |
subsection{*Monotonicity results*} |
|
92 |
||
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
93 |
text{*Most are available in theory @{text Ring_and_Field}, but they are |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
94 |
not yet available: we must prove @{text zadd_zless_mono} before we |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
95 |
can prove that the integers are a ring.*} |
14271 | 96 |
|
97 |
lemma zadd_right_cancel_zless [simp]: "(v+z < w+z) = (v < (w::int))" |
|
98 |
by (simp add: zless_def zdiff_def zadd_ac) |
|
99 |
||
100 |
lemma zadd_left_cancel_zless [simp]: "(z+v < z+w) = (v < (w::int))" |
|
101 |
by (simp add: zless_def zdiff_def zadd_ac) |
|
102 |
||
103 |
lemma zadd_right_cancel_zle [simp] : "(v+z \<le> w+z) = (v \<le> (w::int))" |
|
104 |
by (simp add: linorder_not_less [symmetric]) |
|
105 |
||
106 |
lemma zadd_left_cancel_zle [simp] : "(z+v \<le> z+w) = (v \<le> (w::int))" |
|
107 |
by (simp add: linorder_not_less [symmetric]) |
|
108 |
||
109 |
(*"v\<le>w ==> v+z \<le> w+z"*) |
|
110 |
lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard] |
|
111 |
||
112 |
(*"v\<le>w ==> z+v \<le> z+w"*) |
|
113 |
lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard] |
|
114 |
||
115 |
(*"v\<le>w ==> v+z \<le> w+z"*) |
|
116 |
lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard] |
|
117 |
||
118 |
(*"v\<le>w ==> z+v \<le> z+w"*) |
|
119 |
lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard] |
|
120 |
||
121 |
lemma zadd_zle_mono: "[| w'\<le>w; z'\<le>z |] ==> w' + z' \<le> w + (z::int)" |
|
122 |
by (erule zadd_zle_mono1 [THEN zle_trans], simp) |
|
123 |
||
124 |
lemma zadd_zless_mono: "[| w'<w; z'\<le>z |] ==> w' + z' < w + (z::int)" |
|
125 |
by (erule zadd_zless_mono1 [THEN order_less_le_trans], simp) |
|
126 |
||
127 |
||
128 |
subsection{*Strict Monotonicity of Multiplication*} |
|
129 |
||
130 |
text{*strict, in 1st argument; proof is by induction on k>0*} |
|
131 |
lemma zmult_zless_mono2_lemma: "i<j ==> 0<k --> int k * i < int k * j" |
|
132 |
apply (induct_tac "k", simp) |
|
133 |
apply (simp add: int_Suc) |
|
134 |
apply (case_tac "n=0") |
|
135 |
apply (simp_all add: zadd_zmult_distrib int_Suc0_eq_1 order_le_less) |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
136 |
apply (simp_all add: zadd_zless_mono int_Suc0_eq_1 order_le_less) |
14271 | 137 |
done |
138 |
||
139 |
lemma zmult_zless_mono2: "[| i<j; (0::int) < k |] ==> k*i < k*j" |
|
140 |
apply (rule_tac t = k in not_neg_nat [THEN subst]) |
|
141 |
apply (erule_tac [2] zmult_zless_mono2_lemma [THEN mp]) |
|
142 |
apply (simp add: not_neg_eq_ge_0 order_le_less) |
|
143 |
apply (frule conjI [THEN zless_nat_conj [THEN iffD2]], auto) |
|
144 |
done |
|
145 |
||
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
146 |
|
14271 | 147 |
text{*The Integers Form an Ordered Ring*} |
148 |
instance int :: ordered_ring |
|
149 |
proof |
|
150 |
fix i j k :: int |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
151 |
show "0 < (1::int)" by (rule int_0_less_1) |
14271 | 152 |
show "i \<le> j ==> k + i \<le> k + j" by simp |
153 |
show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: zmult_zless_mono2) |
|
154 |
show "\<bar>i\<bar> = (if i < 0 then -i else i)" by (simp only: zabs_def) |
|
155 |
qed |
|
156 |
||
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
157 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
158 |
subsection{*Comparison laws*} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
159 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
160 |
text{*Legacy bindings: all are in theory @{text Ring_and_Field}.*} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
161 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
162 |
lemma zminus_zless_zminus: "(- x < - y) = (y < (x::int))" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
163 |
by (rule Ring_and_Field.neg_less_iff_less) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
164 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
165 |
lemma zminus_zle_zminus: "(- x \<le> - y) = (y \<le> (x::int))" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
166 |
by (rule Ring_and_Field.neg_le_iff_le) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
167 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
168 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
169 |
text{*The next several equations can make the simplifier loop!*} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
170 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
171 |
lemma zless_zminus: "(x < - y) = (y < - (x::int))" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
172 |
by (rule Ring_and_Field.less_minus_iff) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
173 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
174 |
lemma zminus_zless: "(- x < y) = (- y < (x::int))" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
175 |
by (rule Ring_and_Field.minus_less_iff) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
176 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
177 |
lemma zle_zminus: "(x \<le> - y) = (y \<le> - (x::int))" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
178 |
by (rule Ring_and_Field.le_minus_iff) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
179 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
180 |
lemma zminus_zle: "(- x \<le> y) = (- y \<le> (x::int))" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
181 |
by (rule Ring_and_Field.minus_le_iff) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
182 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
183 |
lemma equation_zminus: "(x = - y) = (y = - (x::int))" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
184 |
by (rule Ring_and_Field.equation_minus_iff) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
185 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
186 |
lemma zminus_equation: "(- x = y) = (- (y::int) = x)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
187 |
by (rule Ring_and_Field.minus_equation_iff) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
188 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
189 |
|
14271 | 190 |
subsection{*Lemmas about the Function @{term int} and Orderings*} |
14264 | 191 |
|
192 |
lemma negative_zless_0: "- (int (Suc n)) < 0" |
|
193 |
by (simp add: zless_def) |
|
194 |
||
195 |
lemma negative_zless [iff]: "- (int (Suc n)) < int m" |
|
196 |
by (rule negative_zless_0 [THEN order_less_le_trans], simp) |
|
197 |
||
14266 | 198 |
lemma negative_zle_0: "- int n \<le> 0" |
14264 | 199 |
by (simp add: zminus_zle) |
200 |
||
14266 | 201 |
lemma negative_zle [iff]: "- int n \<le> int m" |
14264 | 202 |
by (simp add: zless_def zle_def zdiff_def zadd_int) |
203 |
||
14266 | 204 |
lemma not_zle_0_negative [simp]: "~(0 \<le> - (int (Suc n)))" |
14264 | 205 |
by (subst zle_zminus, simp) |
206 |
||
14266 | 207 |
lemma int_zle_neg: "(int n \<le> - int m) = (n = 0 & m = 0)" |
14264 | 208 |
apply safe |
209 |
apply (drule_tac [2] zle_zminus [THEN iffD1]) |
|
210 |
apply (auto dest: zle_trans [OF _ negative_zle_0]) |
|
211 |
done |
|
212 |
||
213 |
lemma not_int_zless_negative [simp]: "~(int n < - int m)" |
|
214 |
by (simp add: zle_def [symmetric]) |
|
215 |
||
216 |
lemma negative_eq_positive [simp]: "(- int n = int m) = (n = 0 & m = 0)" |
|
217 |
apply (rule iffI) |
|
218 |
apply (rule int_zle_neg [THEN iffD1]) |
|
219 |
apply (drule sym) |
|
220 |
apply (simp_all (no_asm_simp)) |
|
221 |
done |
|
13577 | 222 |
|
14290 | 223 |
lemma zle_iff_zadd: "(w \<le> z) = (\<exists>n. z = w + int n)" |
14264 | 224 |
by (force intro: exI [of _ "0::nat"] |
225 |
intro!: not_sym [THEN not0_implies_Suc] |
|
226 |
simp add: zless_iff_Suc_zadd int_le_less) |
|
227 |
||
228 |
lemma abs_int_eq [simp]: "abs (int m) = int m" |
|
229 |
by (simp add: zabs_def) |
|
230 |
||
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14290
diff
changeset
|
231 |
text{*This version is proved for all ordered rings, not just integers! |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
232 |
It is proved here because attribute @{text arith_split} is not available |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
233 |
in theory @{text Ring_and_Field}. |
14294
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14290
diff
changeset
|
234 |
But is it really better than just rewriting with @{text abs_if}?*} |
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14290
diff
changeset
|
235 |
lemma abs_split [arith_split]: |
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14290
diff
changeset
|
236 |
"P(abs(a::'a::ordered_ring)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))" |
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14290
diff
changeset
|
237 |
by (force dest: order_less_le_trans simp add: abs_if linorder_not_less) |
f4d806fd72ce
absolute value theorems moved to HOL/Ring_and_Field
paulson
parents:
14290
diff
changeset
|
238 |
|
14264 | 239 |
|
14271 | 240 |
subsection{*Misc Results*} |
14264 | 241 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
242 |
lemma nat_zminus_int [simp]: "nat(- (int n)) = 0" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
243 |
apply (unfold nat_def) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
244 |
apply (auto simp add: neg_eq_less_0 zero_reorient zminus_zless) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
245 |
done |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
246 |
|
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
247 |
lemma zless_nat_eq_int_zless: "(m < nat z) = (int m < z)" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
248 |
apply (case_tac "neg z") |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
249 |
apply (erule_tac [2] not_neg_nat [THEN subst]) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
250 |
apply (auto simp add: neg_nat) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
251 |
apply (auto dest: order_less_trans simp add: neg_eq_less_0) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
252 |
done |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
253 |
|
14271 | 254 |
lemma zless_eq_neg: "(w<z) = neg(w-z)" |
255 |
by (simp add: zless_def) |
|
14264 | 256 |
|
14271 | 257 |
lemma eq_eq_iszero: "(w=z) = iszero(w-z)" |
258 |
by (simp add: iszero_def diff_eq_eq) |
|
14264 | 259 |
|
14271 | 260 |
lemma zle_eq_not_neg: "(w\<le>z) = (~ neg(z-w))" |
261 |
by (simp add: zle_def zless_def) |
|
14264 | 262 |
|
14266 | 263 |
|
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
264 |
subsection{*Monotonicity of Multiplication*} |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
265 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
266 |
lemma zmult_zle_mono1: "[| i \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*k" |
14271 | 267 |
by (rule Ring_and_Field.mult_right_mono) |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
268 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
269 |
lemma zmult_zle_mono1_neg: "[| i \<le> j; k \<le> (0::int) |] ==> j*k \<le> i*k" |
14271 | 270 |
by (rule Ring_and_Field.mult_right_mono_neg) |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
271 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
272 |
lemma zmult_zle_mono2: "[| i \<le> j; (0::int) \<le> k |] ==> k*i \<le> k*j" |
14271 | 273 |
by (rule Ring_and_Field.mult_left_mono) |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
274 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
275 |
lemma zmult_zle_mono2_neg: "[| i \<le> j; k \<le> (0::int) |] ==> k*j \<le> k*i" |
14271 | 276 |
by (rule Ring_and_Field.mult_left_mono_neg) |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
277 |
|
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
278 |
(* \<le> monotonicity, BOTH arguments*) |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
279 |
lemma zmult_zle_mono: |
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
280 |
"[| i \<le> j; k \<le> l; (0::int) \<le> j; (0::int) \<le> k |] ==> i*k \<le> j*l" |
14271 | 281 |
by (rule Ring_and_Field.mult_mono) |
14267
b963e9cee2a0
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
paulson
parents:
14266
diff
changeset
|
282 |
|
14264 | 283 |
lemma zmult_zless_mono1: "[| i<j; (0::int) < k |] ==> i*k < j*k" |
14266 | 284 |
by (rule Ring_and_Field.mult_strict_right_mono) |
14264 | 285 |
|
286 |
lemma zmult_zless_mono1_neg: "[| i<j; k < (0::int) |] ==> j*k < i*k" |
|
14266 | 287 |
by (rule Ring_and_Field.mult_strict_right_mono_neg) |
14264 | 288 |
|
289 |
lemma zmult_zless_mono2_neg: "[| i<j; k < (0::int) |] ==> k*j < k*i" |
|
14266 | 290 |
by (rule Ring_and_Field.mult_strict_left_mono_neg) |
14264 | 291 |
|
292 |
lemma zmult_eq_0_iff [iff]: "(m*n = (0::int)) = (m = 0 | n = 0)" |
|
14266 | 293 |
by simp |
294 |
||
295 |
lemma zmult_zless_cancel2: "(m*k < n*k) = (((0::int) < k & m<n) | (k<0 & n<m))" |
|
296 |
by (rule Ring_and_Field.mult_less_cancel_right) |
|
297 |
||
298 |
lemma zmult_zless_cancel1: |
|
299 |
"(k*m < k*n) = (((0::int) < k & m<n) | (k < 0 & n<m))" |
|
300 |
by (rule Ring_and_Field.mult_less_cancel_left) |
|
301 |
||
302 |
lemma zmult_zle_cancel2: |
|
303 |
"(m*k \<le> n*k) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))" |
|
304 |
by (rule Ring_and_Field.mult_le_cancel_right) |
|
305 |
||
306 |
lemma zmult_zle_cancel1: |
|
307 |
"(k*m \<le> k*n) = (((0::int) < k --> m\<le>n) & (k < 0 --> n\<le>m))" |
|
308 |
by (rule Ring_and_Field.mult_le_cancel_left) |
|
309 |
||
310 |
lemma zmult_cancel2: "(m*k = n*k) = (k = (0::int) | m=n)" |
|
311 |
by (rule Ring_and_Field.mult_cancel_right) |
|
312 |
||
313 |
lemma zmult_cancel1 [simp]: "(k*m = k*n) = (k = (0::int) | m=n)" |
|
314 |
by (rule Ring_and_Field.mult_cancel_left) |
|
315 |
||
14271 | 316 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
317 |
text{*A case theorem distinguishing non-negative and negative int*} |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
318 |
|
14290 | 319 |
lemma negD: "neg x ==> \<exists>n. x = - (int (Suc n))" |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
320 |
by (auto simp add: neg_eq_less_0 zless_iff_Suc_zadd |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
321 |
diff_eq_eq [symmetric] zdiff_def) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
322 |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
323 |
lemma int_cases [cases type: int, case_names nonneg neg]: |
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
324 |
"[|!! n. z = int n ==> P; !! n. z = - (int (Suc n)) ==> P |] ==> P" |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
325 |
apply (case_tac "neg z") |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
326 |
apply (fast dest!: negD) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
327 |
apply (drule not_neg_nat [symmetric], auto) |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
328 |
done |
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
329 |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
330 |
lemma int_induct [induct type: int, case_names nonneg neg]: |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
331 |
"[|!! n. P (int n); !!n. P (- (int (Suc n))) |] ==> P z" |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
332 |
by (cases z) auto |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
14353
diff
changeset
|
333 |
|
14273
e33ffff0123c
further simplifications of the integer development; converting more .ML files
paulson
parents:
14272
diff
changeset
|
334 |
|
14271 | 335 |
(*Legacy ML bindings, but no longer the structure Int.*) |
336 |
ML |
|
337 |
{* |
|
338 |
val zabs_def = thm "zabs_def" |
|
339 |
val nat_def = thm "nat_def" |
|
340 |
||
341 |
val int_0 = thm "int_0"; |
|
342 |
val int_1 = thm "int_1"; |
|
343 |
val int_Suc0_eq_1 = thm "int_Suc0_eq_1"; |
|
344 |
val neg_eq_less_0 = thm "neg_eq_less_0"; |
|
345 |
val not_neg_eq_ge_0 = thm "not_neg_eq_ge_0"; |
|
346 |
val not_neg_0 = thm "not_neg_0"; |
|
347 |
val not_neg_1 = thm "not_neg_1"; |
|
348 |
val iszero_0 = thm "iszero_0"; |
|
349 |
val not_iszero_1 = thm "not_iszero_1"; |
|
350 |
val int_0_less_1 = thm "int_0_less_1"; |
|
351 |
val int_0_neq_1 = thm "int_0_neq_1"; |
|
14264 | 352 |
val zless_eq_neg = thm "zless_eq_neg"; |
353 |
val eq_eq_iszero = thm "eq_eq_iszero"; |
|
354 |
val zle_eq_not_neg = thm "zle_eq_not_neg"; |
|
355 |
val zadd_right_cancel_zless = thm "zadd_right_cancel_zless"; |
|
356 |
val zadd_left_cancel_zless = thm "zadd_left_cancel_zless"; |
|
357 |
val zadd_right_cancel_zle = thm "zadd_right_cancel_zle"; |
|
358 |
val zadd_left_cancel_zle = thm "zadd_left_cancel_zle"; |
|
359 |
val zadd_zless_mono1 = thm "zadd_zless_mono1"; |
|
360 |
val zadd_zless_mono2 = thm "zadd_zless_mono2"; |
|
361 |
val zadd_zle_mono1 = thm "zadd_zle_mono1"; |
|
362 |
val zadd_zle_mono2 = thm "zadd_zle_mono2"; |
|
363 |
val zadd_zle_mono = thm "zadd_zle_mono"; |
|
364 |
val zadd_zless_mono = thm "zadd_zless_mono"; |
|
365 |
val zminus_zless_zminus = thm "zminus_zless_zminus"; |
|
366 |
val zminus_zle_zminus = thm "zminus_zle_zminus"; |
|
367 |
val zless_zminus = thm "zless_zminus"; |
|
368 |
val zminus_zless = thm "zminus_zless"; |
|
369 |
val zle_zminus = thm "zle_zminus"; |
|
370 |
val zminus_zle = thm "zminus_zle"; |
|
371 |
val equation_zminus = thm "equation_zminus"; |
|
372 |
val zminus_equation = thm "zminus_equation"; |
|
373 |
val negative_zless = thm "negative_zless"; |
|
374 |
val negative_zle = thm "negative_zle"; |
|
375 |
val not_zle_0_negative = thm "not_zle_0_negative"; |
|
376 |
val not_int_zless_negative = thm "not_int_zless_negative"; |
|
377 |
val negative_eq_positive = thm "negative_eq_positive"; |
|
378 |
val zle_iff_zadd = thm "zle_iff_zadd"; |
|
379 |
val abs_int_eq = thm "abs_int_eq"; |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
380 |
val abs_split = thm"abs_split"; |
14264 | 381 |
val nat_int = thm "nat_int"; |
382 |
val nat_zminus_int = thm "nat_zminus_int"; |
|
383 |
val nat_zero = thm "nat_zero"; |
|
384 |
val not_neg_nat = thm "not_neg_nat"; |
|
385 |
val neg_nat = thm "neg_nat"; |
|
386 |
val zless_nat_eq_int_zless = thm "zless_nat_eq_int_zless"; |
|
387 |
val nat_0_le = thm "nat_0_le"; |
|
388 |
val nat_le_0 = thm "nat_le_0"; |
|
389 |
val zless_nat_conj = thm "zless_nat_conj"; |
|
390 |
val int_cases = thm "int_cases"; |
|
391 |
val zmult_zle_mono1 = thm "zmult_zle_mono1"; |
|
392 |
val zmult_zle_mono1_neg = thm "zmult_zle_mono1_neg"; |
|
393 |
val zmult_zle_mono2 = thm "zmult_zle_mono2"; |
|
394 |
val zmult_zle_mono2_neg = thm "zmult_zle_mono2_neg"; |
|
395 |
val zmult_zle_mono = thm "zmult_zle_mono"; |
|
396 |
val zmult_zless_mono2 = thm "zmult_zless_mono2"; |
|
397 |
val zmult_zless_mono1 = thm "zmult_zless_mono1"; |
|
398 |
val zmult_zless_mono1_neg = thm "zmult_zless_mono1_neg"; |
|
399 |
val zmult_zless_mono2_neg = thm "zmult_zless_mono2_neg"; |
|
400 |
val zmult_eq_0_iff = thm "zmult_eq_0_iff"; |
|
401 |
val zmult_zless_cancel2 = thm "zmult_zless_cancel2"; |
|
402 |
val zmult_zless_cancel1 = thm "zmult_zless_cancel1"; |
|
403 |
val zmult_zle_cancel2 = thm "zmult_zle_cancel2"; |
|
404 |
val zmult_zle_cancel1 = thm "zmult_zle_cancel1"; |
|
405 |
val zmult_cancel2 = thm "zmult_cancel2"; |
|
406 |
val zmult_cancel1 = thm "zmult_cancel1"; |
|
407 |
*} |
|
13577 | 408 |
|
409 |
end |