author | berghofe |
Mon, 30 Sep 2002 16:48:15 +0200 | |
changeset 13612 | 55d32e76ef4e |
parent 13560 | d9651081578b |
child 14511 | 73493236e97f |
permissions | -rw-r--r-- |
5561
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
1 |
(* Title: ZF/Integ/Int.thy |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
4 |
Copyright 1993 University of Cambridge |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
5 |
|
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
6 |
*) |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
7 |
|
13560 | 8 |
header{*The Integers as Equivalence Classes Over Pairs of Natural Numbers*} |
9 |
||
10 |
theory Int = EquivClass + ArithSimp: |
|
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
11 |
|
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
12 |
constdefs |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
13 |
intrel :: i |
13560 | 14 |
"intrel == {p : (nat*nat)*(nat*nat). |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
15 |
EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}" |
5561
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
16 |
|
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
17 |
int :: i |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
18 |
"int == (nat*nat)//intrel" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
19 |
|
13560 | 20 |
int_of :: "i=>i" --{*coercion from nat to int*} ("$# _" [80] 80) |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
21 |
"$# m == intrel `` {<natify(m), 0>}" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
22 |
|
13560 | 23 |
intify :: "i=>i" --{*coercion from ANYTHING to int*} |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
24 |
"intify(m) == if m : int then m else $#0" |
5561
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
25 |
|
13560 | 26 |
raw_zminus :: "i=>i" |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
27 |
"raw_zminus(z) == UN <x,y>: z. intrel``{<y,x>}" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
28 |
|
13560 | 29 |
zminus :: "i=>i" ("$- _" [80] 80) |
9548 | 30 |
"$- z == raw_zminus (intify(z))" |
5561
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
31 |
|
13560 | 32 |
znegative :: "i=>o" |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
33 |
"znegative(z) == EX x y. x<y & y:nat & <x,y>:z" |
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
34 |
|
13560 | 35 |
iszero :: "i=>o" |
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
36 |
"iszero(z) == z = $# 0" |
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
37 |
|
13560 | 38 |
raw_nat_of :: "i=>i" |
9883 | 39 |
"raw_nat_of(z) == if znegative(z) then 0 |
40 |
else (THE m. m: nat & z = int_of(m))" |
|
41 |
||
13560 | 42 |
nat_of :: "i=>i" |
9883 | 43 |
"nat_of(z) == raw_nat_of (intify(z))" |
44 |
||
13560 | 45 |
zmagnitude :: "i=>i" |
46 |
--{*could be replaced by an absolute value function from int to int?*} |
|
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
47 |
"zmagnitude(z) == |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
48 |
THE m. m : nat & ((~ znegative(z) & z = $# m) | |
9548 | 49 |
(znegative(z) & $- z = $# m))" |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
50 |
|
13560 | 51 |
raw_zmult :: "[i,i]=>i" |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
52 |
(*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2. |
5561
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
53 |
Perhaps a "curried" or even polymorphic congruent predicate would be |
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
54 |
better.*) |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
55 |
"raw_zmult(z1,z2) == |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
56 |
UN p1:z1. UN p2:z2. split(%x1 y1. split(%x2 y2. |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
57 |
intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
58 |
|
13560 | 59 |
zmult :: "[i,i]=>i" (infixl "$*" 70) |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
60 |
"z1 $* z2 == raw_zmult (intify(z1),intify(z2))" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
61 |
|
13560 | 62 |
raw_zadd :: "[i,i]=>i" |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
63 |
"raw_zadd (z1, z2) == |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
64 |
UN z1:z1. UN z2:z2. let <x1,y1>=z1; <x2,y2>=z2 |
5561
426c1e330903
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents:
diff
changeset
|
65 |
in intrel``{<x1#+x2, y1#+y2>}" |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
66 |
|
13560 | 67 |
zadd :: "[i,i]=>i" (infixl "$+" 65) |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
68 |
"z1 $+ z2 == raw_zadd (intify(z1),intify(z2))" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
69 |
|
13560 | 70 |
zdiff :: "[i,i]=>i" (infixl "$-" 65) |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
71 |
"z1 $- z2 == z1 $+ zminus(z2)" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
72 |
|
13560 | 73 |
zless :: "[i,i]=>o" (infixl "$<" 50) |
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
74 |
"z1 $< z2 == znegative(z1 $- z2)" |
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
75 |
|
13560 | 76 |
zle :: "[i,i]=>o" (infixl "$<=" 50) |
9570
e16e168984e1
installation of cancellation simprocs for the integers
paulson
parents:
9548
diff
changeset
|
77 |
"z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)" |
9548 | 78 |
|
9654
9754ba005b64
X-symbols for ordinal, cardinal, integer arithmetic
paulson
parents:
9578
diff
changeset
|
79 |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
11321
diff
changeset
|
80 |
syntax (xsymbols) |
13560 | 81 |
zmult :: "[i,i]=>i" (infixl "$\<times>" 70) |
82 |
zle :: "[i,i]=>o" (infixl "$\<le>" 50) --{*less than or equals*} |
|
9654
9754ba005b64
X-symbols for ordinal, cardinal, integer arithmetic
paulson
parents:
9578
diff
changeset
|
83 |
|
9964 | 84 |
syntax (HTML output) |
13560 | 85 |
zmult :: "[i,i]=>i" (infixl "$\<times>" 70) |
86 |
||
87 |
||
88 |
declare quotientE [elim!] |
|
89 |
||
90 |
subsection{*Proving that @{term intrel} is an equivalence relation*} |
|
91 |
||
92 |
(** Natural deduction for intrel **) |
|
93 |
||
94 |
lemma intrel_iff [simp]: |
|
95 |
"<<x1,y1>,<x2,y2>>: intrel <-> |
|
96 |
x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1" |
|
97 |
by (unfold intrel_def, fast) |
|
98 |
||
99 |
lemma intrelI [intro!]: |
|
100 |
"[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] |
|
101 |
==> <<x1,y1>,<x2,y2>>: intrel" |
|
102 |
by (unfold intrel_def, fast) |
|
103 |
||
104 |
lemma intrelE [elim!]: |
|
105 |
"[| p: intrel; |
|
106 |
!!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>; x1#+y2 = x2#+y1; |
|
107 |
x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] |
|
108 |
==> Q" |
|
109 |
by (unfold intrel_def, blast) |
|
110 |
||
111 |
lemma int_trans_lemma: |
|
112 |
"[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1" |
|
113 |
apply (rule sym) |
|
114 |
apply (erule add_left_cancel)+ |
|
115 |
apply (simp_all (no_asm_simp)) |
|
116 |
done |
|
117 |
||
118 |
lemma equiv_intrel: "equiv(nat*nat, intrel)" |
|
119 |
apply (unfold equiv_def refl_def sym_def trans_def) |
|
120 |
apply (fast elim!: sym int_trans_lemma) |
|
121 |
done |
|
122 |
||
123 |
lemma image_intrel_int: "[| m: nat; n: nat |] ==> intrel `` {<m,n>} : int" |
|
124 |
apply (unfold int_def) |
|
125 |
apply (blast intro: quotientI) |
|
126 |
done |
|
127 |
||
128 |
declare equiv_intrel [THEN eq_equiv_class_iff, simp] |
|
129 |
declare conj_cong [cong] |
|
130 |
||
131 |
lemmas eq_intrelD = eq_equiv_class [OF _ equiv_intrel] |
|
132 |
||
133 |
(** int_of: the injection from nat to int **) |
|
134 |
||
135 |
lemma int_of_type [simp,TC]: "$#m : int" |
|
136 |
by (unfold int_def quotient_def int_of_def, auto) |
|
137 |
||
138 |
lemma int_of_eq [iff]: "($# m = $# n) <-> natify(m)=natify(n)" |
|
139 |
by (unfold int_of_def, auto) |
|
140 |
||
141 |
lemma int_of_inject: "[| $#m = $#n; m: nat; n: nat |] ==> m=n" |
|
142 |
by (drule int_of_eq [THEN iffD1], auto) |
|
143 |
||
144 |
||
145 |
(** intify: coercion from anything to int **) |
|
146 |
||
147 |
lemma intify_in_int [iff,TC]: "intify(x) : int" |
|
148 |
by (simp add: intify_def) |
|
149 |
||
150 |
lemma intify_ident [simp]: "n : int ==> intify(n) = n" |
|
151 |
by (simp add: intify_def) |
|
152 |
||
153 |
||
154 |
subsection{*Collapsing rules: to remove @{term intify} |
|
155 |
from arithmetic expressions*} |
|
156 |
||
157 |
lemma intify_idem [simp]: "intify(intify(x)) = intify(x)" |
|
158 |
by simp |
|
159 |
||
160 |
lemma int_of_natify [simp]: "$# (natify(m)) = $# m" |
|
161 |
by (simp add: int_of_def) |
|
162 |
||
163 |
lemma zminus_intify [simp]: "$- (intify(m)) = $- m" |
|
164 |
by (simp add: zminus_def) |
|
165 |
||
166 |
(** Addition **) |
|
167 |
||
168 |
lemma zadd_intify1 [simp]: "intify(x) $+ y = x $+ y" |
|
169 |
by (simp add: zadd_def) |
|
170 |
||
171 |
lemma zadd_intify2 [simp]: "x $+ intify(y) = x $+ y" |
|
172 |
by (simp add: zadd_def) |
|
173 |
||
174 |
(** Subtraction **) |
|
175 |
||
176 |
lemma zdiff_intify1 [simp]:"intify(x) $- y = x $- y" |
|
177 |
by (simp add: zdiff_def) |
|
178 |
||
179 |
lemma zdiff_intify2 [simp]:"x $- intify(y) = x $- y" |
|
180 |
by (simp add: zdiff_def) |
|
181 |
||
182 |
(** Multiplication **) |
|
183 |
||
184 |
lemma zmult_intify1 [simp]:"intify(x) $* y = x $* y" |
|
185 |
by (simp add: zmult_def) |
|
186 |
||
187 |
lemma zmult_intify2 [simp]:"x $* intify(y) = x $* y" |
|
188 |
by (simp add: zmult_def) |
|
189 |
||
190 |
(** Orderings **) |
|
191 |
||
192 |
lemma zless_intify1 [simp]:"intify(x) $< y <-> x $< y" |
|
193 |
by (simp add: zless_def) |
|
194 |
||
195 |
lemma zless_intify2 [simp]:"x $< intify(y) <-> x $< y" |
|
196 |
by (simp add: zless_def) |
|
197 |
||
198 |
lemma zle_intify1 [simp]:"intify(x) $<= y <-> x $<= y" |
|
199 |
by (simp add: zle_def) |
|
200 |
||
201 |
lemma zle_intify2 [simp]:"x $<= intify(y) <-> x $<= y" |
|
202 |
by (simp add: zle_def) |
|
203 |
||
204 |
||
205 |
subsection{*@{term zminus}: unary negation on @{term int}*} |
|
206 |
||
207 |
lemma zminus_congruent: "congruent(intrel, %<x,y>. intrel``{<y,x>})" |
|
208 |
apply (unfold congruent_def, safe) |
|
209 |
apply (simp add: add_ac) |
|
210 |
done |
|
211 |
||
212 |
lemma raw_zminus_type: "z : int ==> raw_zminus(z) : int" |
|
213 |
apply (unfold int_def raw_zminus_def) |
|
214 |
apply (typecheck add: UN_equiv_class_type [OF equiv_intrel zminus_congruent]) |
|
215 |
done |
|
216 |
||
217 |
lemma zminus_type [TC,iff]: "$-z : int" |
|
218 |
apply (unfold zminus_def) |
|
219 |
apply (simp add: zminus_def raw_zminus_type) |
|
220 |
done |
|
221 |
||
222 |
lemma raw_zminus_inject: |
|
223 |
"[| raw_zminus(z) = raw_zminus(w); z: int; w: int |] ==> z=w" |
|
224 |
apply (unfold int_def raw_zminus_def) |
|
225 |
apply (erule UN_equiv_class_inject [OF equiv_intrel zminus_congruent], safe) |
|
226 |
apply (auto dest: eq_intrelD simp add: add_ac) |
|
227 |
done |
|
228 |
||
229 |
lemma zminus_inject_intify [dest!]: "$-z = $-w ==> intify(z) = intify(w)" |
|
230 |
apply (unfold zminus_def) |
|
231 |
apply (blast dest!: raw_zminus_inject) |
|
232 |
done |
|
233 |
||
234 |
lemma zminus_inject: "[| $-z = $-w; z: int; w: int |] ==> z=w" |
|
235 |
by auto |
|
236 |
||
237 |
lemma raw_zminus: |
|
238 |
"[| x: nat; y: nat |] ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}" |
|
239 |
apply (unfold raw_zminus_def) |
|
240 |
apply (simp add: UN_equiv_class [OF equiv_intrel zminus_congruent]) |
|
241 |
done |
|
242 |
||
243 |
lemma zminus: |
|
244 |
"[| x: nat; y: nat |] |
|
245 |
==> $- (intrel``{<x,y>}) = intrel `` {<y,x>}" |
|
246 |
apply (unfold zminus_def) |
|
247 |
apply (simp (no_asm_simp) add: raw_zminus image_intrel_int) |
|
248 |
done |
|
249 |
||
250 |
lemma raw_zminus_zminus: "z : int ==> raw_zminus (raw_zminus(z)) = z" |
|
251 |
apply (unfold int_def) |
|
252 |
apply (auto simp add: raw_zminus) |
|
253 |
done |
|
254 |
||
255 |
lemma zminus_zminus_intify [simp]: "$- ($- z) = intify(z)" |
|
256 |
by (simp add: zminus_def raw_zminus_type raw_zminus_zminus) |
|
257 |
||
258 |
lemma zminus_int0 [simp]: "$- ($#0) = $#0" |
|
259 |
apply (unfold int_of_def) |
|
260 |
apply (simp add: zminus) |
|
261 |
done |
|
262 |
||
263 |
lemma zminus_zminus: "z : int ==> $- ($- z) = z" |
|
264 |
by simp |
|
265 |
||
266 |
||
267 |
subsection{*@{term znegative}: the test for negative integers*} |
|
268 |
||
269 |
(*No natural number is negative!*) |
|
270 |
lemma not_znegative_int_of [iff]: "~ znegative($# n)" |
|
271 |
apply (unfold znegative_def int_of_def, safe) |
|
272 |
apply (drule_tac psi = "?lhs=?rhs" in asm_rl) |
|
273 |
apply (drule_tac psi = "?lhs<?rhs" in asm_rl) |
|
274 |
apply (force simp add: add_le_self2 [THEN le_imp_not_lt] natify_succ) |
|
275 |
done |
|
276 |
||
277 |
lemma znegative_zminus_int_of [simp]: "znegative($- $# succ(n))" |
|
278 |
apply (unfold znegative_def int_of_def) |
|
279 |
apply (simp (no_asm_simp) add: zminus natify_succ) |
|
280 |
apply (blast intro: nat_0_le) |
|
281 |
done |
|
282 |
||
283 |
lemma not_znegative_imp_zero: "~ znegative($- $# n) ==> natify(n)=0" |
|
284 |
apply (unfold znegative_def int_of_def) |
|
285 |
apply (simp add: zminus image_singleton_iff) |
|
286 |
apply (drule_tac x = 0 in spec) |
|
287 |
apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff, THEN iff_sym]) |
|
288 |
done |
|
289 |
||
290 |
||
291 |
subsection{*@{term nat_of}: Coercion of an Integer to a Natural Number*} |
|
292 |
||
293 |
lemma nat_of_intify [simp]: "nat_of(intify(z)) = nat_of(z)" |
|
294 |
by (unfold nat_of_def, auto) |
|
295 |
||
296 |
lemma nat_of_int_of [simp]: "nat_of($# n) = natify(n)" |
|
297 |
apply (unfold nat_of_def raw_nat_of_def) |
|
298 |
apply (auto simp add: int_of_eq) |
|
299 |
done |
|
300 |
||
301 |
lemma raw_nat_of_type: "raw_nat_of(z) : nat" |
|
302 |
apply (unfold raw_nat_of_def, auto) |
|
303 |
apply (case_tac "EX! m. m: nat & z = int_of (m) ") |
|
304 |
apply (rule theI2) |
|
305 |
apply (simp_all add: the_0) |
|
306 |
done |
|
307 |
||
308 |
lemma nat_of_type [iff,TC]: "nat_of(z) : nat" |
|
309 |
apply (unfold nat_of_def) |
|
310 |
apply (simp add: raw_nat_of_type) |
|
311 |
done |
|
312 |
||
313 |
subsection{*zmagnitude: magnitide of an integer, as a natural number*} |
|
314 |
||
315 |
lemma zmagnitude_int_of [simp]: "zmagnitude($# n) = natify(n)" |
|
316 |
apply (unfold zmagnitude_def) |
|
317 |
apply (auto simp add: int_of_eq) |
|
318 |
done |
|
319 |
||
320 |
lemma natify_int_of_eq: "natify(x)=n ==> $#x = $# n" |
|
321 |
apply (drule sym) |
|
322 |
apply (simp (no_asm_simp) add: int_of_eq) |
|
323 |
done |
|
324 |
||
325 |
lemma zmagnitude_zminus_int_of [simp]: "zmagnitude($- $# n) = natify(n)" |
|
326 |
apply (unfold zmagnitude_def) |
|
327 |
apply (rule the_equality) |
|
328 |
apply (auto dest!: not_znegative_imp_zero natify_int_of_eq |
|
329 |
iff del: int_of_eq, auto) |
|
330 |
done |
|
331 |
||
332 |
lemma zmagnitude_type [iff,TC]: "zmagnitude(z) : nat" |
|
333 |
apply (unfold zmagnitude_def) |
|
334 |
apply (rule theI2, auto) |
|
335 |
done |
|
336 |
||
337 |
lemma not_zneg_int_of: |
|
338 |
"[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n" |
|
339 |
apply (unfold int_def znegative_def int_of_def) |
|
340 |
apply (auto simp add: image_singleton_iff) |
|
341 |
apply (rename_tac i j) |
|
342 |
apply (drule_tac x = i in spec) |
|
343 |
apply (drule_tac x = j in spec) |
|
344 |
apply (rule bexI) |
|
345 |
apply (rule add_diff_inverse2 [symmetric], auto) |
|
346 |
apply (simp add: not_lt_iff_le) |
|
347 |
done |
|
348 |
||
349 |
lemma not_zneg_mag [simp]: |
|
350 |
"[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z" |
|
351 |
by (drule not_zneg_int_of, auto) |
|
352 |
||
353 |
lemma zneg_int_of: |
|
354 |
"[| znegative(z); z: int |] ==> EX n:nat. z = $- ($# succ(n))" |
|
355 |
apply (unfold int_def znegative_def int_of_def) |
|
356 |
apply (auto dest!: less_imp_succ_add simp add: zminus image_singleton_iff) |
|
357 |
done |
|
358 |
||
359 |
lemma zneg_mag [simp]: |
|
360 |
"[| znegative(z); z: int |] ==> $# (zmagnitude(z)) = $- z" |
|
361 |
apply (drule zneg_int_of, auto) |
|
362 |
done |
|
363 |
||
364 |
lemma int_cases: "z : int ==> EX n: nat. z = $# n | z = $- ($# succ(n))" |
|
365 |
apply (case_tac "znegative (z) ") |
|
366 |
prefer 2 apply (blast dest: not_zneg_mag sym) |
|
367 |
apply (blast dest: zneg_int_of) |
|
368 |
done |
|
369 |
||
370 |
lemma not_zneg_raw_nat_of: |
|
371 |
"[| ~ znegative(z); z: int |] ==> $# (raw_nat_of(z)) = z" |
|
372 |
apply (drule not_zneg_int_of) |
|
373 |
apply (auto simp add: raw_nat_of_type) |
|
374 |
apply (auto simp add: raw_nat_of_def) |
|
375 |
done |
|
376 |
||
377 |
lemma not_zneg_nat_of_intify: |
|
378 |
"~ znegative(intify(z)) ==> $# (nat_of(z)) = intify(z)" |
|
379 |
by (simp (no_asm_simp) add: nat_of_def not_zneg_raw_nat_of) |
|
380 |
||
381 |
lemma not_zneg_nat_of: "[| ~ znegative(z); z: int |] ==> $# (nat_of(z)) = z" |
|
382 |
apply (simp (no_asm_simp) add: not_zneg_nat_of_intify) |
|
383 |
done |
|
384 |
||
385 |
lemma zneg_nat_of [simp]: "znegative(intify(z)) ==> nat_of(z) = 0" |
|
386 |
by (unfold nat_of_def raw_nat_of_def, auto) |
|
387 |
||
388 |
||
389 |
subsection{*@{term zadd}: addition on int*} |
|
390 |
||
391 |
text{*Congruence Property for Addition*} |
|
392 |
lemma zadd_congruent2: |
|
393 |
"congruent2(intrel, %z1 z2. |
|
394 |
let <x1,y1>=z1; <x2,y2>=z2 |
|
395 |
in intrel``{<x1#+x2, y1#+y2>})" |
|
396 |
apply (unfold congruent2_def) |
|
397 |
(*Proof via congruent2_commuteI seems longer*) |
|
398 |
apply safe |
|
399 |
apply (simp (no_asm_simp) add: add_assoc Let_def) |
|
400 |
(*The rest should be trivial, but rearranging terms is hard |
|
401 |
add_ac does not help rewriting with the assumptions.*) |
|
402 |
apply (rule_tac m1 = x1a in add_left_commute [THEN ssubst]) |
|
403 |
apply (rule_tac m1 = x2a in add_left_commute [THEN ssubst]) |
|
404 |
apply (simp (no_asm_simp) add: add_assoc [symmetric]) |
|
405 |
done |
|
406 |
||
407 |
lemma raw_zadd_type: "[| z: int; w: int |] ==> raw_zadd(z,w) : int" |
|
408 |
apply (unfold int_def raw_zadd_def) |
|
409 |
apply (rule UN_equiv_class_type2 [OF equiv_intrel zadd_congruent2], assumption+) |
|
410 |
apply (simp add: Let_def) |
|
411 |
done |
|
412 |
||
413 |
lemma zadd_type [iff,TC]: "z $+ w : int" |
|
414 |
by (simp add: zadd_def raw_zadd_type) |
|
415 |
||
416 |
lemma raw_zadd: |
|
417 |
"[| x1: nat; y1: nat; x2: nat; y2: nat |] |
|
418 |
==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) = |
|
419 |
intrel `` {<x1#+x2, y1#+y2>}" |
|
420 |
apply (unfold raw_zadd_def) |
|
421 |
apply (simp add: UN_equiv_class2 [OF equiv_intrel zadd_congruent2]) |
|
422 |
apply (simp add: Let_def) |
|
423 |
done |
|
424 |
||
425 |
lemma zadd: |
|
426 |
"[| x1: nat; y1: nat; x2: nat; y2: nat |] |
|
427 |
==> (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) = |
|
428 |
intrel `` {<x1#+x2, y1#+y2>}" |
|
429 |
apply (unfold zadd_def) |
|
430 |
apply (simp (no_asm_simp) add: raw_zadd image_intrel_int) |
|
431 |
done |
|
432 |
||
433 |
lemma raw_zadd_int0: "z : int ==> raw_zadd ($#0,z) = z" |
|
434 |
apply (unfold int_def int_of_def) |
|
435 |
apply (auto simp add: raw_zadd) |
|
436 |
done |
|
437 |
||
438 |
lemma zadd_int0_intify [simp]: "$#0 $+ z = intify(z)" |
|
439 |
by (simp add: zadd_def raw_zadd_int0) |
|
440 |
||
441 |
lemma zadd_int0: "z: int ==> $#0 $+ z = z" |
|
442 |
by simp |
|
443 |
||
444 |
lemma raw_zminus_zadd_distrib: |
|
445 |
"[| z: int; w: int |] ==> $- raw_zadd(z,w) = raw_zadd($- z, $- w)" |
|
446 |
apply (unfold int_def) |
|
447 |
apply (auto simp add: zminus raw_zadd) |
|
448 |
done |
|
449 |
||
450 |
lemma zminus_zadd_distrib [simp]: "$- (z $+ w) = $- z $+ $- w" |
|
451 |
by (simp add: zadd_def raw_zminus_zadd_distrib) |
|
452 |
||
453 |
lemma raw_zadd_commute: |
|
454 |
"[| z: int; w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)" |
|
455 |
apply (unfold int_def) |
|
456 |
apply (auto simp add: raw_zadd add_ac) |
|
457 |
done |
|
458 |
||
459 |
lemma zadd_commute: "z $+ w = w $+ z" |
|
460 |
by (simp add: zadd_def raw_zadd_commute) |
|
461 |
||
462 |
lemma raw_zadd_assoc: |
|
463 |
"[| z1: int; z2: int; z3: int |] |
|
464 |
==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))" |
|
465 |
apply (unfold int_def) |
|
466 |
apply (auto simp add: raw_zadd add_assoc) |
|
467 |
done |
|
468 |
||
469 |
lemma zadd_assoc: "(z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)" |
|
470 |
by (simp add: zadd_def raw_zadd_type raw_zadd_assoc) |
|
471 |
||
472 |
(*For AC rewriting*) |
|
473 |
lemma zadd_left_commute: "z1$+(z2$+z3) = z2$+(z1$+z3)" |
|
474 |
apply (simp add: zadd_assoc [symmetric]) |
|
475 |
apply (simp add: zadd_commute) |
|
476 |
done |
|
477 |
||
478 |
(*Integer addition is an AC operator*) |
|
479 |
lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute |
|
480 |
||
481 |
lemma int_of_add: "$# (m #+ n) = ($#m) $+ ($#n)" |
|
482 |
apply (unfold int_of_def) |
|
483 |
apply (simp add: zadd) |
|
484 |
done |
|
485 |
||
486 |
lemma int_succ_int_1: "$# succ(m) = $# 1 $+ ($# m)" |
|
487 |
by (simp add: int_of_add [symmetric] natify_succ) |
|
488 |
||
489 |
lemma int_of_diff: |
|
490 |
"[| m: nat; n le m |] ==> $# (m #- n) = ($#m) $- ($#n)" |
|
491 |
apply (unfold int_of_def zdiff_def) |
|
492 |
apply (frule lt_nat_in_nat) |
|
493 |
apply (simp_all add: zadd zminus add_diff_inverse2) |
|
494 |
done |
|
495 |
||
496 |
lemma raw_zadd_zminus_inverse: "z : int ==> raw_zadd (z, $- z) = $#0" |
|
497 |
apply (unfold int_def int_of_def) |
|
498 |
apply (auto simp add: zminus raw_zadd add_commute) |
|
499 |
done |
|
500 |
||
501 |
lemma zadd_zminus_inverse [simp]: "z $+ ($- z) = $#0" |
|
502 |
apply (simp add: zadd_def) |
|
503 |
apply (subst zminus_intify [symmetric]) |
|
504 |
apply (rule intify_in_int [THEN raw_zadd_zminus_inverse]) |
|
505 |
done |
|
506 |
||
507 |
lemma zadd_zminus_inverse2 [simp]: "($- z) $+ z = $#0" |
|
508 |
by (simp add: zadd_commute zadd_zminus_inverse) |
|
509 |
||
510 |
lemma zadd_int0_right_intify [simp]: "z $+ $#0 = intify(z)" |
|
511 |
by (rule trans [OF zadd_commute zadd_int0_intify]) |
|
512 |
||
513 |
lemma zadd_int0_right: "z:int ==> z $+ $#0 = z" |
|
514 |
by simp |
|
515 |
||
516 |
||
517 |
subsection{*@{term zmult}: Integer Multiplication*} |
|
518 |
||
519 |
text{*Congruence property for multiplication*} |
|
520 |
lemma zmult_congruent2: |
|
521 |
"congruent2(intrel, %p1 p2. |
|
522 |
split(%x1 y1. split(%x2 y2. |
|
523 |
intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))" |
|
524 |
apply (rule equiv_intrel [THEN congruent2_commuteI], auto) |
|
525 |
(*Proof that zmult is congruent in one argument*) |
|
526 |
apply (rename_tac x y) |
|
527 |
apply (frule_tac t = "%u. x#*u" in sym [THEN subst_context]) |
|
528 |
apply (drule_tac t = "%u. y#*u" in subst_context) |
|
529 |
apply (erule add_left_cancel)+ |
|
530 |
apply (simp_all add: add_mult_distrib_left) |
|
531 |
done |
|
532 |
||
533 |
||
534 |
lemma raw_zmult_type: "[| z: int; w: int |] ==> raw_zmult(z,w) : int" |
|
535 |
apply (unfold int_def raw_zmult_def) |
|
536 |
apply (rule UN_equiv_class_type2 [OF equiv_intrel zmult_congruent2], assumption+) |
|
537 |
apply (simp add: Let_def) |
|
538 |
done |
|
539 |
||
540 |
lemma zmult_type [iff,TC]: "z $* w : int" |
|
541 |
by (simp add: zmult_def raw_zmult_type) |
|
542 |
||
543 |
lemma raw_zmult: |
|
544 |
"[| x1: nat; y1: nat; x2: nat; y2: nat |] |
|
545 |
==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) = |
|
546 |
intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}" |
|
547 |
apply (unfold raw_zmult_def) |
|
548 |
apply (simp add: UN_equiv_class2 [OF equiv_intrel zmult_congruent2]) |
|
549 |
done |
|
550 |
||
551 |
lemma zmult: |
|
552 |
"[| x1: nat; y1: nat; x2: nat; y2: nat |] |
|
553 |
==> (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) = |
|
554 |
intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}" |
|
555 |
apply (unfold zmult_def) |
|
556 |
apply (simp add: raw_zmult image_intrel_int) |
|
557 |
done |
|
558 |
||
559 |
lemma raw_zmult_int0: "z : int ==> raw_zmult ($#0,z) = $#0" |
|
560 |
apply (unfold int_def int_of_def) |
|
561 |
apply (auto simp add: raw_zmult) |
|
562 |
done |
|
563 |
||
564 |
lemma zmult_int0 [simp]: "$#0 $* z = $#0" |
|
565 |
by (simp add: zmult_def raw_zmult_int0) |
|
566 |
||
567 |
lemma raw_zmult_int1: "z : int ==> raw_zmult ($#1,z) = z" |
|
568 |
apply (unfold int_def int_of_def) |
|
569 |
apply (auto simp add: raw_zmult) |
|
570 |
done |
|
571 |
||
572 |
lemma zmult_int1_intify [simp]: "$#1 $* z = intify(z)" |
|
573 |
by (simp add: zmult_def raw_zmult_int1) |
|
574 |
||
575 |
lemma zmult_int1: "z : int ==> $#1 $* z = z" |
|
576 |
by simp |
|
577 |
||
578 |
lemma raw_zmult_commute: |
|
579 |
"[| z: int; w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)" |
|
580 |
apply (unfold int_def) |
|
581 |
apply (auto simp add: raw_zmult add_ac mult_ac) |
|
582 |
done |
|
583 |
||
584 |
lemma zmult_commute: "z $* w = w $* z" |
|
585 |
by (simp add: zmult_def raw_zmult_commute) |
|
586 |
||
587 |
lemma raw_zmult_zminus: |
|
588 |
"[| z: int; w: int |] ==> raw_zmult($- z, w) = $- raw_zmult(z, w)" |
|
589 |
apply (unfold int_def) |
|
590 |
apply (auto simp add: zminus raw_zmult add_ac) |
|
591 |
done |
|
592 |
||
593 |
lemma zmult_zminus [simp]: "($- z) $* w = $- (z $* w)" |
|
594 |
apply (simp add: zmult_def raw_zmult_zminus) |
|
595 |
apply (subst zminus_intify [symmetric], rule raw_zmult_zminus, auto) |
|
596 |
done |
|
597 |
||
598 |
lemma zmult_zminus_right [simp]: "w $* ($- z) = $- (w $* z)" |
|
599 |
by (simp add: zmult_commute [of w]) |
|
600 |
||
601 |
lemma raw_zmult_assoc: |
|
602 |
"[| z1: int; z2: int; z3: int |] |
|
603 |
==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))" |
|
604 |
apply (unfold int_def) |
|
605 |
apply (auto simp add: raw_zmult add_mult_distrib_left add_ac mult_ac) |
|
606 |
done |
|
607 |
||
608 |
lemma zmult_assoc: "(z1 $* z2) $* z3 = z1 $* (z2 $* z3)" |
|
609 |
by (simp add: zmult_def raw_zmult_type raw_zmult_assoc) |
|
610 |
||
611 |
(*For AC rewriting*) |
|
612 |
lemma zmult_left_commute: "z1$*(z2$*z3) = z2$*(z1$*z3)" |
|
613 |
apply (simp add: zmult_assoc [symmetric]) |
|
614 |
apply (simp add: zmult_commute) |
|
615 |
done |
|
616 |
||
617 |
(*Integer multiplication is an AC operator*) |
|
618 |
lemmas zmult_ac = zmult_assoc zmult_commute zmult_left_commute |
|
619 |
||
620 |
lemma raw_zadd_zmult_distrib: |
|
621 |
"[| z1: int; z2: int; w: int |] |
|
622 |
==> raw_zmult(raw_zadd(z1,z2), w) = |
|
623 |
raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))" |
|
624 |
apply (unfold int_def) |
|
625 |
apply (auto simp add: raw_zadd raw_zmult add_mult_distrib_left add_ac mult_ac) |
|
626 |
done |
|
627 |
||
628 |
lemma zadd_zmult_distrib: "(z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)" |
|
629 |
by (simp add: zmult_def zadd_def raw_zadd_type raw_zmult_type |
|
630 |
raw_zadd_zmult_distrib) |
|
631 |
||
632 |
lemma zadd_zmult_distrib2: "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)" |
|
633 |
by (simp add: zmult_commute [of w] zadd_zmult_distrib) |
|
634 |
||
635 |
lemmas int_typechecks = |
|
636 |
int_of_type zminus_type zmagnitude_type zadd_type zmult_type |
|
637 |
||
638 |
||
639 |
(*** Subtraction laws ***) |
|
640 |
||
641 |
lemma zdiff_type [iff,TC]: "z $- w : int" |
|
642 |
by (simp add: zdiff_def) |
|
643 |
||
644 |
lemma zminus_zdiff_eq [simp]: "$- (z $- y) = y $- z" |
|
645 |
by (simp add: zdiff_def zadd_commute) |
|
646 |
||
647 |
lemma zdiff_zmult_distrib: "(z1 $- z2) $* w = (z1 $* w) $- (z2 $* w)" |
|
648 |
apply (unfold zdiff_def) |
|
649 |
apply (subst zadd_zmult_distrib) |
|
650 |
apply (simp add: zmult_zminus) |
|
651 |
done |
|
652 |
||
653 |
lemma zdiff_zmult_distrib2: "w $* (z1 $- z2) = (w $* z1) $- (w $* z2)" |
|
654 |
by (simp add: zmult_commute [of w] zdiff_zmult_distrib) |
|
655 |
||
656 |
lemma zadd_zdiff_eq: "x $+ (y $- z) = (x $+ y) $- z" |
|
657 |
by (simp add: zdiff_def zadd_ac) |
|
658 |
||
659 |
lemma zdiff_zadd_eq: "(x $- y) $+ z = (x $+ z) $- y" |
|
660 |
by (simp add: zdiff_def zadd_ac) |
|
661 |
||
662 |
||
663 |
subsection{*The "Less Than" Relation*} |
|
664 |
||
665 |
(*"Less than" is a linear ordering*) |
|
666 |
lemma zless_linear_lemma: |
|
667 |
"[| z: int; w: int |] ==> z$<w | z=w | w$<z" |
|
668 |
apply (unfold int_def zless_def znegative_def zdiff_def, auto) |
|
669 |
apply (simp add: zadd zminus image_iff Bex_def) |
|
670 |
apply (rule_tac i = "xb#+ya" and j = "xc #+ y" in Ord_linear_lt) |
|
671 |
apply (force dest!: spec simp add: add_ac)+ |
|
672 |
done |
|
673 |
||
674 |
lemma zless_linear: "z$<w | intify(z)=intify(w) | w$<z" |
|
675 |
apply (cut_tac z = " intify (z) " and w = " intify (w) " in zless_linear_lemma) |
|
676 |
apply auto |
|
677 |
done |
|
678 |
||
679 |
lemma zless_not_refl [iff]: "~ (z$<z)" |
|
680 |
apply (auto simp add: zless_def znegative_def int_of_def zdiff_def) |
|
681 |
done |
|
682 |
||
683 |
lemma neq_iff_zless: "[| x: int; y: int |] ==> (x ~= y) <-> (x $< y | y $< x)" |
|
684 |
by (cut_tac z = x and w = y in zless_linear, auto) |
|
685 |
||
686 |
lemma zless_imp_intify_neq: "w $< z ==> intify(w) ~= intify(z)" |
|
687 |
apply auto |
|
688 |
apply (subgoal_tac "~ (intify (w) $< intify (z))") |
|
689 |
apply (erule_tac [2] ssubst) |
|
690 |
apply (simp (no_asm_use)) |
|
691 |
apply auto |
|
692 |
done |
|
693 |
||
694 |
(*This lemma allows direct proofs of other <-properties*) |
|
695 |
lemma zless_imp_succ_zadd_lemma: |
|
696 |
"[| w $< z; w: int; z: int |] ==> (EX n: nat. z = w $+ $#(succ(n)))" |
|
697 |
apply (unfold zless_def znegative_def zdiff_def int_def) |
|
698 |
apply (auto dest!: less_imp_succ_add simp add: zadd zminus int_of_def) |
|
699 |
apply (rule_tac x = k in bexI) |
|
700 |
apply (erule add_left_cancel, auto) |
|
701 |
done |
|
702 |
||
703 |
lemma zless_imp_succ_zadd: |
|
704 |
"w $< z ==> (EX n: nat. w $+ $#(succ(n)) = intify(z))" |
|
705 |
apply (subgoal_tac "intify (w) $< intify (z) ") |
|
706 |
apply (drule_tac w = "intify (w) " in zless_imp_succ_zadd_lemma) |
|
707 |
apply auto |
|
708 |
done |
|
709 |
||
710 |
lemma zless_succ_zadd_lemma: |
|
711 |
"w : int ==> w $< w $+ $# succ(n)" |
|
712 |
apply (unfold zless_def znegative_def zdiff_def int_def) |
|
713 |
apply (auto simp add: zadd zminus int_of_def image_iff) |
|
714 |
apply (rule_tac x = 0 in exI, auto) |
|
715 |
done |
|
716 |
||
717 |
lemma zless_succ_zadd: "w $< w $+ $# succ(n)" |
|
718 |
by (cut_tac intify_in_int [THEN zless_succ_zadd_lemma], auto) |
|
719 |
||
720 |
lemma zless_iff_succ_zadd: |
|
721 |
"w $< z <-> (EX n: nat. w $+ $#(succ(n)) = intify(z))" |
|
722 |
apply (rule iffI) |
|
723 |
apply (erule zless_imp_succ_zadd, auto) |
|
724 |
apply (rename_tac "n") |
|
725 |
apply (cut_tac w = w and n = n in zless_succ_zadd, auto) |
|
726 |
done |
|
727 |
||
728 |
lemma zless_int_of [simp]: "[| m: nat; n: nat |] ==> ($#m $< $#n) <-> (m<n)" |
|
729 |
apply (simp add: less_iff_succ_add zless_iff_succ_zadd int_of_add [symmetric]) |
|
730 |
apply (blast intro: sym) |
|
731 |
done |
|
732 |
||
733 |
lemma zless_trans_lemma: |
|
734 |
"[| x $< y; y $< z; x: int; y : int; z: int |] ==> x $< z" |
|
735 |
apply (unfold zless_def znegative_def zdiff_def int_def) |
|
736 |
apply (auto simp add: zadd zminus image_iff) |
|
737 |
apply (rename_tac x1 x2 y1 y2) |
|
738 |
apply (rule_tac x = "x1#+x2" in exI) |
|
739 |
apply (rule_tac x = "y1#+y2" in exI) |
|
740 |
apply (auto simp add: add_lt_mono) |
|
741 |
apply (rule sym) |
|
742 |
apply (erule add_left_cancel)+ |
|
743 |
apply auto |
|
744 |
done |
|
745 |
||
746 |
lemma zless_trans: "[| x $< y; y $< z |] ==> x $< z" |
|
747 |
apply (subgoal_tac "intify (x) $< intify (z) ") |
|
748 |
apply (rule_tac [2] y = "intify (y) " in zless_trans_lemma) |
|
749 |
apply auto |
|
750 |
done |
|
751 |
||
752 |
lemma zless_not_sym: "z $< w ==> ~ (w $< z)" |
|
753 |
by (blast dest: zless_trans) |
|
754 |
||
755 |
(* [| z $< w; ~ P ==> w $< z |] ==> P *) |
|
756 |
lemmas zless_asym = zless_not_sym [THEN swap, standard] |
|
757 |
||
758 |
lemma zless_imp_zle: "z $< w ==> z $<= w" |
|
759 |
apply (unfold zle_def) |
|
760 |
apply (blast elim: zless_asym) |
|
761 |
done |
|
762 |
||
763 |
lemma zle_linear: "z $<= w | w $<= z" |
|
764 |
apply (simp add: zle_def) |
|
765 |
apply (cut_tac zless_linear, blast) |
|
766 |
done |
|
767 |
||
768 |
||
769 |
subsection{*Less Than or Equals*} |
|
770 |
||
771 |
lemma zle_refl: "z $<= z" |
|
772 |
by (unfold zle_def, auto) |
|
773 |
||
774 |
lemma zle_eq_refl: "x=y ==> x $<= y" |
|
775 |
by (simp add: zle_refl) |
|
776 |
||
777 |
lemma zle_anti_sym_intify: "[| x $<= y; y $<= x |] ==> intify(x) = intify(y)" |
|
778 |
apply (unfold zle_def, auto) |
|
779 |
apply (blast dest: zless_trans) |
|
780 |
done |
|
781 |
||
782 |
lemma zle_anti_sym: "[| x $<= y; y $<= x; x: int; y: int |] ==> x=y" |
|
783 |
by (drule zle_anti_sym_intify, auto) |
|
784 |
||
785 |
lemma zle_trans_lemma: |
|
786 |
"[| x: int; y: int; z: int; x $<= y; y $<= z |] ==> x $<= z" |
|
787 |
apply (unfold zle_def, auto) |
|
788 |
apply (blast intro: zless_trans) |
|
789 |
done |
|
790 |
||
791 |
lemma zle_trans: "[| x $<= y; y $<= z |] ==> x $<= z" |
|
792 |
apply (subgoal_tac "intify (x) $<= intify (z) ") |
|
793 |
apply (rule_tac [2] y = "intify (y) " in zle_trans_lemma) |
|
794 |
apply auto |
|
795 |
done |
|
796 |
||
797 |
lemma zle_zless_trans: "[| i $<= j; j $< k |] ==> i $< k" |
|
798 |
apply (auto simp add: zle_def) |
|
799 |
apply (blast intro: zless_trans) |
|
800 |
apply (simp add: zless_def zdiff_def zadd_def) |
|
801 |
done |
|
802 |
||
803 |
lemma zless_zle_trans: "[| i $< j; j $<= k |] ==> i $< k" |
|
804 |
apply (auto simp add: zle_def) |
|
805 |
apply (blast intro: zless_trans) |
|
806 |
apply (simp add: zless_def zdiff_def zminus_def) |
|
807 |
done |
|
808 |
||
809 |
lemma not_zless_iff_zle: "~ (z $< w) <-> (w $<= z)" |
|
810 |
apply (cut_tac z = z and w = w in zless_linear) |
|
811 |
apply (auto dest: zless_trans simp add: zle_def) |
|
812 |
apply (auto dest!: zless_imp_intify_neq) |
|
813 |
done |
|
814 |
||
815 |
lemma not_zle_iff_zless: "~ (z $<= w) <-> (w $< z)" |
|
816 |
by (simp add: not_zless_iff_zle [THEN iff_sym]) |
|
817 |
||
818 |
||
819 |
subsection{*More subtraction laws (for @{text zcompare_rls})*} |
|
820 |
||
821 |
lemma zdiff_zdiff_eq: "(x $- y) $- z = x $- (y $+ z)" |
|
822 |
by (simp add: zdiff_def zadd_ac) |
|
823 |
||
824 |
lemma zdiff_zdiff_eq2: "x $- (y $- z) = (x $+ z) $- y" |
|
825 |
by (simp add: zdiff_def zadd_ac) |
|
826 |
||
827 |
lemma zdiff_zless_iff: "(x$-y $< z) <-> (x $< z $+ y)" |
|
828 |
apply (unfold zless_def zdiff_def) |
|
829 |
apply (simp add: zadd_ac) |
|
830 |
done |
|
831 |
||
832 |
lemma zless_zdiff_iff: "(x $< z$-y) <-> (x $+ y $< z)" |
|
833 |
apply (unfold zless_def zdiff_def) |
|
834 |
apply (simp add: zadd_ac) |
|
835 |
done |
|
836 |
||
837 |
lemma zdiff_eq_iff: "[| x: int; z: int |] ==> (x$-y = z) <-> (x = z $+ y)" |
|
838 |
apply (unfold zdiff_def) |
|
839 |
apply (auto simp add: zadd_assoc) |
|
840 |
done |
|
841 |
||
842 |
lemma eq_zdiff_iff: "[| x: int; z: int |] ==> (x = z$-y) <-> (x $+ y = z)" |
|
843 |
apply (unfold zdiff_def) |
|
844 |
apply (auto simp add: zadd_assoc) |
|
845 |
done |
|
846 |
||
847 |
lemma zdiff_zle_iff_lemma: |
|
848 |
"[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)" |
|
849 |
apply (unfold zle_def) |
|
850 |
apply (auto simp add: zdiff_eq_iff zdiff_zless_iff) |
|
851 |
done |
|
852 |
||
853 |
lemma zdiff_zle_iff: "(x$-y $<= z) <-> (x $<= z $+ y)" |
|
854 |
by (cut_tac zdiff_zle_iff_lemma [OF intify_in_int intify_in_int], simp) |
|
855 |
||
856 |
lemma zle_zdiff_iff_lemma: |
|
857 |
"[| x: int; z: int |] ==>(x $<= z$-y) <-> (x $+ y $<= z)" |
|
858 |
apply (unfold zle_def) |
|
859 |
apply (auto simp add: zdiff_eq_iff zless_zdiff_iff) |
|
860 |
apply (auto simp add: zdiff_def zadd_assoc) |
|
861 |
done |
|
862 |
||
863 |
lemma zle_zdiff_iff: "(x $<= z$-y) <-> (x $+ y $<= z)" |
|
864 |
by (cut_tac zle_zdiff_iff_lemma [ OF intify_in_int intify_in_int], simp) |
|
865 |
||
866 |
text{*This list of rewrites simplifies (in)equalities by bringing subtractions |
|
867 |
to the top and then moving negative terms to the other side. |
|
868 |
Use with @{text zadd_ac}*} |
|
869 |
lemmas zcompare_rls = |
|
870 |
zdiff_def [symmetric] |
|
871 |
zadd_zdiff_eq zdiff_zadd_eq zdiff_zdiff_eq zdiff_zdiff_eq2 |
|
872 |
zdiff_zless_iff zless_zdiff_iff zdiff_zle_iff zle_zdiff_iff |
|
873 |
zdiff_eq_iff eq_zdiff_iff |
|
874 |
||
875 |
||
876 |
subsection{*Monotonicity and Cancellation Results for Instantiation |
|
877 |
of the CancelNumerals Simprocs*} |
|
878 |
||
879 |
lemma zadd_left_cancel: |
|
880 |
"[| w: int; w': int |] ==> (z $+ w' = z $+ w) <-> (w' = w)" |
|
881 |
apply safe |
|
882 |
apply (drule_tac t = "%x. x $+ ($-z) " in subst_context) |
|
883 |
apply (simp add: zadd_ac) |
|
884 |
done |
|
885 |
||
886 |
lemma zadd_left_cancel_intify [simp]: |
|
887 |
"(z $+ w' = z $+ w) <-> intify(w') = intify(w)" |
|
888 |
apply (rule iff_trans) |
|
889 |
apply (rule_tac [2] zadd_left_cancel, auto) |
|
890 |
done |
|
891 |
||
892 |
lemma zadd_right_cancel: |
|
893 |
"[| w: int; w': int |] ==> (w' $+ z = w $+ z) <-> (w' = w)" |
|
894 |
apply safe |
|
895 |
apply (drule_tac t = "%x. x $+ ($-z) " in subst_context) |
|
896 |
apply (simp add: zadd_ac) |
|
897 |
done |
|
898 |
||
899 |
lemma zadd_right_cancel_intify [simp]: |
|
900 |
"(w' $+ z = w $+ z) <-> intify(w') = intify(w)" |
|
901 |
apply (rule iff_trans) |
|
902 |
apply (rule_tac [2] zadd_right_cancel, auto) |
|
903 |
done |
|
904 |
||
905 |
lemma zadd_right_cancel_zless [simp]: "(w' $+ z $< w $+ z) <-> (w' $< w)" |
|
906 |
apply (simp add: zdiff_zless_iff [THEN iff_sym]) |
|
907 |
apply (simp add: zdiff_def zadd_assoc) |
|
908 |
done |
|
909 |
||
910 |
lemma zadd_left_cancel_zless [simp]: "(z $+ w' $< z $+ w) <-> (w' $< w)" |
|
911 |
by (simp add: zadd_commute [of z] zadd_right_cancel_zless) |
|
912 |
||
913 |
lemma zadd_right_cancel_zle [simp]: "(w' $+ z $<= w $+ z) <-> w' $<= w" |
|
914 |
by (simp add: zle_def) |
|
915 |
||
916 |
lemma zadd_left_cancel_zle [simp]: "(z $+ w' $<= z $+ w) <-> w' $<= w" |
|
917 |
by (simp add: zadd_commute [of z] zadd_right_cancel_zle) |
|
918 |
||
919 |
||
920 |
(*"v $<= w ==> v$+z $<= w$+z"*) |
|
921 |
lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard] |
|
922 |
||
923 |
(*"v $<= w ==> z$+v $<= z$+w"*) |
|
924 |
lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard] |
|
925 |
||
926 |
(*"v $<= w ==> v$+z $<= w$+z"*) |
|
927 |
lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard] |
|
928 |
||
929 |
(*"v $<= w ==> z$+v $<= z$+w"*) |
|
930 |
lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard] |
|
931 |
||
932 |
lemma zadd_zle_mono: "[| w' $<= w; z' $<= z |] ==> w' $+ z' $<= w $+ z" |
|
933 |
by (erule zadd_zle_mono1 [THEN zle_trans], simp) |
|
934 |
||
935 |
lemma zadd_zless_mono: "[| w' $< w; z' $<= z |] ==> w' $+ z' $< w $+ z" |
|
936 |
by (erule zadd_zless_mono1 [THEN zless_zle_trans], simp) |
|
937 |
||
938 |
||
939 |
subsection{*Comparison laws*} |
|
940 |
||
941 |
lemma zminus_zless_zminus [simp]: "($- x $< $- y) <-> (y $< x)" |
|
942 |
by (simp add: zless_def zdiff_def zadd_ac) |
|
943 |
||
944 |
lemma zminus_zle_zminus [simp]: "($- x $<= $- y) <-> (y $<= x)" |
|
945 |
by (simp add: not_zless_iff_zle [THEN iff_sym]) |
|
946 |
||
947 |
subsubsection{*More inequality lemmas*} |
|
948 |
||
949 |
lemma equation_zminus: "[| x: int; y: int |] ==> (x = $- y) <-> (y = $- x)" |
|
950 |
by auto |
|
951 |
||
952 |
lemma zminus_equation: "[| x: int; y: int |] ==> ($- x = y) <-> ($- y = x)" |
|
953 |
by auto |
|
954 |
||
955 |
lemma equation_zminus_intify: "(intify(x) = $- y) <-> (intify(y) = $- x)" |
|
956 |
apply (cut_tac x = "intify (x) " and y = "intify (y) " in equation_zminus) |
|
957 |
apply auto |
|
958 |
done |
|
959 |
||
960 |
lemma zminus_equation_intify: "($- x = intify(y)) <-> ($- y = intify(x))" |
|
961 |
apply (cut_tac x = "intify (x) " and y = "intify (y) " in zminus_equation) |
|
962 |
apply auto |
|
963 |
done |
|
964 |
||
965 |
||
966 |
subsubsection{*The next several equations are permutative: watch out!*} |
|
967 |
||
968 |
lemma zless_zminus: "(x $< $- y) <-> (y $< $- x)" |
|
969 |
by (simp add: zless_def zdiff_def zadd_ac) |
|
970 |
||
971 |
lemma zminus_zless: "($- x $< y) <-> ($- y $< x)" |
|
972 |
by (simp add: zless_def zdiff_def zadd_ac) |
|
973 |
||
974 |
lemma zle_zminus: "(x $<= $- y) <-> (y $<= $- x)" |
|
975 |
by (simp add: not_zless_iff_zle [THEN iff_sym] zminus_zless) |
|
976 |
||
977 |
lemma zminus_zle: "($- x $<= y) <-> ($- y $<= x)" |
|
978 |
by (simp add: not_zless_iff_zle [THEN iff_sym] zless_zminus) |
|
979 |
||
980 |
ML |
|
981 |
{* |
|
982 |
val zdiff_def = thm "zdiff_def"; |
|
983 |
val int_of_type = thm "int_of_type"; |
|
984 |
val int_of_eq = thm "int_of_eq"; |
|
985 |
val int_of_inject = thm "int_of_inject"; |
|
986 |
val intify_in_int = thm "intify_in_int"; |
|
987 |
val intify_ident = thm "intify_ident"; |
|
988 |
val intify_idem = thm "intify_idem"; |
|
989 |
val int_of_natify = thm "int_of_natify"; |
|
990 |
val zminus_intify = thm "zminus_intify"; |
|
991 |
val zadd_intify1 = thm "zadd_intify1"; |
|
992 |
val zadd_intify2 = thm "zadd_intify2"; |
|
993 |
val zdiff_intify1 = thm "zdiff_intify1"; |
|
994 |
val zdiff_intify2 = thm "zdiff_intify2"; |
|
995 |
val zmult_intify1 = thm "zmult_intify1"; |
|
996 |
val zmult_intify2 = thm "zmult_intify2"; |
|
997 |
val zless_intify1 = thm "zless_intify1"; |
|
998 |
val zless_intify2 = thm "zless_intify2"; |
|
999 |
val zle_intify1 = thm "zle_intify1"; |
|
1000 |
val zle_intify2 = thm "zle_intify2"; |
|
1001 |
val zminus_congruent = thm "zminus_congruent"; |
|
1002 |
val zminus_type = thm "zminus_type"; |
|
1003 |
val zminus_inject_intify = thm "zminus_inject_intify"; |
|
1004 |
val zminus_inject = thm "zminus_inject"; |
|
1005 |
val zminus = thm "zminus"; |
|
1006 |
val zminus_zminus_intify = thm "zminus_zminus_intify"; |
|
1007 |
val zminus_int0 = thm "zminus_int0"; |
|
1008 |
val zminus_zminus = thm "zminus_zminus"; |
|
1009 |
val not_znegative_int_of = thm "not_znegative_int_of"; |
|
1010 |
val znegative_zminus_int_of = thm "znegative_zminus_int_of"; |
|
1011 |
val not_znegative_imp_zero = thm "not_znegative_imp_zero"; |
|
1012 |
val nat_of_intify = thm "nat_of_intify"; |
|
1013 |
val nat_of_int_of = thm "nat_of_int_of"; |
|
1014 |
val nat_of_type = thm "nat_of_type"; |
|
1015 |
val zmagnitude_int_of = thm "zmagnitude_int_of"; |
|
1016 |
val natify_int_of_eq = thm "natify_int_of_eq"; |
|
1017 |
val zmagnitude_zminus_int_of = thm "zmagnitude_zminus_int_of"; |
|
1018 |
val zmagnitude_type = thm "zmagnitude_type"; |
|
1019 |
val not_zneg_int_of = thm "not_zneg_int_of"; |
|
1020 |
val not_zneg_mag = thm "not_zneg_mag"; |
|
1021 |
val zneg_int_of = thm "zneg_int_of"; |
|
1022 |
val zneg_mag = thm "zneg_mag"; |
|
1023 |
val int_cases = thm "int_cases"; |
|
1024 |
val not_zneg_nat_of_intify = thm "not_zneg_nat_of_intify"; |
|
1025 |
val not_zneg_nat_of = thm "not_zneg_nat_of"; |
|
1026 |
val zneg_nat_of = thm "zneg_nat_of"; |
|
1027 |
val zadd_congruent2 = thm "zadd_congruent2"; |
|
1028 |
val zadd_type = thm "zadd_type"; |
|
1029 |
val zadd = thm "zadd"; |
|
1030 |
val zadd_int0_intify = thm "zadd_int0_intify"; |
|
1031 |
val zadd_int0 = thm "zadd_int0"; |
|
1032 |
val zminus_zadd_distrib = thm "zminus_zadd_distrib"; |
|
1033 |
val zadd_commute = thm "zadd_commute"; |
|
1034 |
val zadd_assoc = thm "zadd_assoc"; |
|
1035 |
val zadd_left_commute = thm "zadd_left_commute"; |
|
1036 |
val zadd_ac = thms "zadd_ac"; |
|
1037 |
val int_of_add = thm "int_of_add"; |
|
1038 |
val int_succ_int_1 = thm "int_succ_int_1"; |
|
1039 |
val int_of_diff = thm "int_of_diff"; |
|
1040 |
val zadd_zminus_inverse = thm "zadd_zminus_inverse"; |
|
1041 |
val zadd_zminus_inverse2 = thm "zadd_zminus_inverse2"; |
|
1042 |
val zadd_int0_right_intify = thm "zadd_int0_right_intify"; |
|
1043 |
val zadd_int0_right = thm "zadd_int0_right"; |
|
1044 |
val zmult_congruent2 = thm "zmult_congruent2"; |
|
1045 |
val zmult_type = thm "zmult_type"; |
|
1046 |
val zmult = thm "zmult"; |
|
1047 |
val zmult_int0 = thm "zmult_int0"; |
|
1048 |
val zmult_int1_intify = thm "zmult_int1_intify"; |
|
1049 |
val zmult_int1 = thm "zmult_int1"; |
|
1050 |
val zmult_commute = thm "zmult_commute"; |
|
1051 |
val zmult_zminus = thm "zmult_zminus"; |
|
1052 |
val zmult_zminus_right = thm "zmult_zminus_right"; |
|
1053 |
val zmult_assoc = thm "zmult_assoc"; |
|
1054 |
val zmult_left_commute = thm "zmult_left_commute"; |
|
1055 |
val zmult_ac = thms "zmult_ac"; |
|
1056 |
val zadd_zmult_distrib = thm "zadd_zmult_distrib"; |
|
1057 |
val zadd_zmult_distrib2 = thm "zadd_zmult_distrib2"; |
|
1058 |
val int_typechecks = thms "int_typechecks"; |
|
1059 |
val zdiff_type = thm "zdiff_type"; |
|
1060 |
val zminus_zdiff_eq = thm "zminus_zdiff_eq"; |
|
1061 |
val zdiff_zmult_distrib = thm "zdiff_zmult_distrib"; |
|
1062 |
val zdiff_zmult_distrib2 = thm "zdiff_zmult_distrib2"; |
|
1063 |
val zadd_zdiff_eq = thm "zadd_zdiff_eq"; |
|
1064 |
val zdiff_zadd_eq = thm "zdiff_zadd_eq"; |
|
1065 |
val zless_linear = thm "zless_linear"; |
|
1066 |
val zless_not_refl = thm "zless_not_refl"; |
|
1067 |
val neq_iff_zless = thm "neq_iff_zless"; |
|
1068 |
val zless_imp_intify_neq = thm "zless_imp_intify_neq"; |
|
1069 |
val zless_imp_succ_zadd = thm "zless_imp_succ_zadd"; |
|
1070 |
val zless_succ_zadd = thm "zless_succ_zadd"; |
|
1071 |
val zless_iff_succ_zadd = thm "zless_iff_succ_zadd"; |
|
1072 |
val zless_int_of = thm "zless_int_of"; |
|
1073 |
val zless_trans = thm "zless_trans"; |
|
1074 |
val zless_not_sym = thm "zless_not_sym"; |
|
1075 |
val zless_asym = thm "zless_asym"; |
|
1076 |
val zless_imp_zle = thm "zless_imp_zle"; |
|
1077 |
val zle_linear = thm "zle_linear"; |
|
1078 |
val zle_refl = thm "zle_refl"; |
|
1079 |
val zle_eq_refl = thm "zle_eq_refl"; |
|
1080 |
val zle_anti_sym_intify = thm "zle_anti_sym_intify"; |
|
1081 |
val zle_anti_sym = thm "zle_anti_sym"; |
|
1082 |
val zle_trans = thm "zle_trans"; |
|
1083 |
val zle_zless_trans = thm "zle_zless_trans"; |
|
1084 |
val zless_zle_trans = thm "zless_zle_trans"; |
|
1085 |
val not_zless_iff_zle = thm "not_zless_iff_zle"; |
|
1086 |
val not_zle_iff_zless = thm "not_zle_iff_zless"; |
|
1087 |
val zdiff_zdiff_eq = thm "zdiff_zdiff_eq"; |
|
1088 |
val zdiff_zdiff_eq2 = thm "zdiff_zdiff_eq2"; |
|
1089 |
val zdiff_zless_iff = thm "zdiff_zless_iff"; |
|
1090 |
val zless_zdiff_iff = thm "zless_zdiff_iff"; |
|
1091 |
val zdiff_eq_iff = thm "zdiff_eq_iff"; |
|
1092 |
val eq_zdiff_iff = thm "eq_zdiff_iff"; |
|
1093 |
val zdiff_zle_iff = thm "zdiff_zle_iff"; |
|
1094 |
val zle_zdiff_iff = thm "zle_zdiff_iff"; |
|
1095 |
val zcompare_rls = thms "zcompare_rls"; |
|
1096 |
val zadd_left_cancel = thm "zadd_left_cancel"; |
|
1097 |
val zadd_left_cancel_intify = thm "zadd_left_cancel_intify"; |
|
1098 |
val zadd_right_cancel = thm "zadd_right_cancel"; |
|
1099 |
val zadd_right_cancel_intify = thm "zadd_right_cancel_intify"; |
|
1100 |
val zadd_right_cancel_zless = thm "zadd_right_cancel_zless"; |
|
1101 |
val zadd_left_cancel_zless = thm "zadd_left_cancel_zless"; |
|
1102 |
val zadd_right_cancel_zle = thm "zadd_right_cancel_zle"; |
|
1103 |
val zadd_left_cancel_zle = thm "zadd_left_cancel_zle"; |
|
1104 |
val zadd_zless_mono1 = thm "zadd_zless_mono1"; |
|
1105 |
val zadd_zless_mono2 = thm "zadd_zless_mono2"; |
|
1106 |
val zadd_zle_mono1 = thm "zadd_zle_mono1"; |
|
1107 |
val zadd_zle_mono2 = thm "zadd_zle_mono2"; |
|
1108 |
val zadd_zle_mono = thm "zadd_zle_mono"; |
|
1109 |
val zadd_zless_mono = thm "zadd_zless_mono"; |
|
1110 |
val zminus_zless_zminus = thm "zminus_zless_zminus"; |
|
1111 |
val zminus_zle_zminus = thm "zminus_zle_zminus"; |
|
1112 |
val equation_zminus = thm "equation_zminus"; |
|
1113 |
val zminus_equation = thm "zminus_equation"; |
|
1114 |
val equation_zminus_intify = thm "equation_zminus_intify"; |
|
1115 |
val zminus_equation_intify = thm "zminus_equation_intify"; |
|
1116 |
val zless_zminus = thm "zless_zminus"; |
|
1117 |
val zminus_zless = thm "zminus_zless"; |
|
1118 |
val zle_zminus = thm "zle_zminus"; |
|
1119 |
val zminus_zle = thm "zminus_zle"; |
|
1120 |
*} |
|
1121 |
||
1122 |
||
9496
07e33cac5d9c
coercion "intify" to remove type constraints from integer algebraic laws
paulson
parents:
9333
diff
changeset
|
1123 |
end |