src/ZF/Int_ZF.thy
 author wenzelm Fri Feb 18 16:22:27 2011 +0100 (2011-02-18) changeset 41777 1f7cbe39d425 parent 32960 69916a850301 child 45602 2a858377c3d2 permissions -rw-r--r--
1 (*  Title:      ZF/Int_ZF.thy
2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3     Copyright   1993  University of Cambridge
4 *)
6 header{*The Integers as Equivalence Classes Over Pairs of Natural Numbers*}
8 theory Int_ZF imports EquivClass ArithSimp begin
10 definition
11   intrel :: i  where
12     "intrel == {p : (nat*nat)*(nat*nat).
13                 \<exists>x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
15 definition
16   int :: i  where
17     "int == (nat*nat)//intrel"
19 definition
20   int_of :: "i=>i" --{*coercion from nat to int*}    ("\$# _" [80] 80)  where
21     "\$# m == intrel `` {<natify(m), 0>}"
23 definition
24   intify :: "i=>i" --{*coercion from ANYTHING to int*}  where
25     "intify(m) == if m : int then m else \$#0"
27 definition
28   raw_zminus :: "i=>i"  where
29     "raw_zminus(z) == \<Union><x,y>\<in>z. intrel``{<y,x>}"
31 definition
32   zminus :: "i=>i"                                 ("\$- _" [80] 80)  where
33     "\$- z == raw_zminus (intify(z))"
35 definition
36   znegative   ::      "i=>o"  where
37     "znegative(z) == \<exists>x y. x<y & y\<in>nat & <x,y>\<in>z"
39 definition
40   iszero      ::      "i=>o"  where
41     "iszero(z) == z = \$# 0"
43 definition
44   raw_nat_of  :: "i=>i"  where
45   "raw_nat_of(z) == natify (\<Union><x,y>\<in>z. x#-y)"
47 definition
48   nat_of  :: "i=>i"  where
49   "nat_of(z) == raw_nat_of (intify(z))"
51 definition
52   zmagnitude  ::      "i=>i"  where
53   --{*could be replaced by an absolute value function from int to int?*}
54     "zmagnitude(z) ==
55      THE m. m\<in>nat & ((~ znegative(z) & z = \$# m) |
56                        (znegative(z) & \$- z = \$# m))"
58 definition
59   raw_zmult   ::      "[i,i]=>i"  where
60     (*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2.
61       Perhaps a "curried" or even polymorphic congruent predicate would be
62       better.*)
63      "raw_zmult(z1,z2) ==
64        \<Union>p1\<in>z1. \<Union>p2\<in>z2.  split(%x1 y1. split(%x2 y2.
65                    intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
67 definition
68   zmult       ::      "[i,i]=>i"      (infixl "\$*" 70)  where
69      "z1 \$* z2 == raw_zmult (intify(z1),intify(z2))"
71 definition
74        \<Union>z1\<in>z1. \<Union>z2\<in>z2. let <x1,y1>=z1; <x2,y2>=z2
75                            in intrel``{<x1#+x2, y1#+y2>}"
77 definition
78   zadd        ::      "[i,i]=>i"      (infixl "\$+" 65)  where
79      "z1 \$+ z2 == raw_zadd (intify(z1),intify(z2))"
81 definition
82   zdiff        ::      "[i,i]=>i"      (infixl "\$-" 65)  where
83      "z1 \$- z2 == z1 \$+ zminus(z2)"
85 definition
86   zless        ::      "[i,i]=>o"      (infixl "\$<" 50)  where
87      "z1 \$< z2 == znegative(z1 \$- z2)"
89 definition
90   zle          ::      "[i,i]=>o"      (infixl "\$<=" 50)  where
91      "z1 \$<= z2 == z1 \$< z2 | intify(z1)=intify(z2)"
94 notation (xsymbols)
95   zmult  (infixl "\$\<times>" 70) and
96   zle  (infixl "\$\<le>" 50)  --{*less than or equals*}
98 notation (HTML output)
99   zmult  (infixl "\$\<times>" 70) and
100   zle  (infixl "\$\<le>" 50)
103 declare quotientE [elim!]
105 subsection{*Proving that @{term intrel} is an equivalence relation*}
107 (** Natural deduction for intrel **)
109 lemma intrel_iff [simp]:
110     "<<x1,y1>,<x2,y2>>: intrel <->
111      x1\<in>nat & y1\<in>nat & x2\<in>nat & y2\<in>nat & x1#+y2 = x2#+y1"
114 lemma intrelI [intro!]:
115     "[| x1#+y2 = x2#+y1; x1\<in>nat; y1\<in>nat; x2\<in>nat; y2\<in>nat |]
116      ==> <<x1,y1>,<x2,y2>>: intrel"
119 lemma intrelE [elim!]:
120   "[| p: intrel;
121       !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1;
122                         x1\<in>nat; y1\<in>nat; x2\<in>nat; y2\<in>nat |] ==> Q |]
123    ==> Q"
124 by (simp add: intrel_def, blast)
126 lemma int_trans_lemma:
127      "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1"
128 apply (rule sym)
130 apply (simp_all (no_asm_simp))
131 done
133 lemma equiv_intrel: "equiv(nat*nat, intrel)"
134 apply (simp add: equiv_def refl_def sym_def trans_def)
135 apply (fast elim!: sym int_trans_lemma)
136 done
138 lemma image_intrel_int: "[| m\<in>nat; n\<in>nat |] ==> intrel `` {<m,n>} : int"
141 declare equiv_intrel [THEN eq_equiv_class_iff, simp]
142 declare conj_cong [cong]
144 lemmas eq_intrelD = eq_equiv_class [OF _ equiv_intrel]
146 (** int_of: the injection from nat to int **)
148 lemma int_of_type [simp,TC]: "\$#m : int"
149 by (simp add: int_def quotient_def int_of_def, auto)
151 lemma int_of_eq [iff]: "(\$# m = \$# n) <-> natify(m)=natify(n)"
154 lemma int_of_inject: "[| \$#m = \$#n;  m\<in>nat;  n\<in>nat |] ==> m=n"
155 by (drule int_of_eq [THEN iffD1], auto)
158 (** intify: coercion from anything to int **)
160 lemma intify_in_int [iff,TC]: "intify(x) : int"
163 lemma intify_ident [simp]: "n : int ==> intify(n) = n"
167 subsection{*Collapsing rules: to remove @{term intify}
168             from arithmetic expressions*}
170 lemma intify_idem [simp]: "intify(intify(x)) = intify(x)"
171 by simp
173 lemma int_of_natify [simp]: "\$# (natify(m)) = \$# m"
176 lemma zminus_intify [simp]: "\$- (intify(m)) = \$- m"
181 lemma zadd_intify1 [simp]: "intify(x) \$+ y = x \$+ y"
184 lemma zadd_intify2 [simp]: "x \$+ intify(y) = x \$+ y"
187 (** Subtraction **)
189 lemma zdiff_intify1 [simp]:"intify(x) \$- y = x \$- y"
192 lemma zdiff_intify2 [simp]:"x \$- intify(y) = x \$- y"
195 (** Multiplication **)
197 lemma zmult_intify1 [simp]:"intify(x) \$* y = x \$* y"
200 lemma zmult_intify2 [simp]:"x \$* intify(y) = x \$* y"
203 (** Orderings **)
205 lemma zless_intify1 [simp]:"intify(x) \$< y <-> x \$< y"
208 lemma zless_intify2 [simp]:"x \$< intify(y) <-> x \$< y"
211 lemma zle_intify1 [simp]:"intify(x) \$<= y <-> x \$<= y"
214 lemma zle_intify2 [simp]:"x \$<= intify(y) <-> x \$<= y"
218 subsection{*@{term zminus}: unary negation on @{term int}*}
220 lemma zminus_congruent: "(%<x,y>. intrel``{<y,x>}) respects intrel"
223 lemma raw_zminus_type: "z : int ==> raw_zminus(z) : int"
224 apply (simp add: int_def raw_zminus_def)
225 apply (typecheck add: UN_equiv_class_type [OF equiv_intrel zminus_congruent])
226 done
228 lemma zminus_type [TC,iff]: "\$-z : int"
229 by (simp add: zminus_def raw_zminus_type)
231 lemma raw_zminus_inject:
232      "[| raw_zminus(z) = raw_zminus(w);  z: int;  w: int |] ==> z=w"
233 apply (simp add: int_def raw_zminus_def)
234 apply (erule UN_equiv_class_inject [OF equiv_intrel zminus_congruent], safe)
236 done
238 lemma zminus_inject_intify [dest!]: "\$-z = \$-w ==> intify(z) = intify(w)"
240 apply (blast dest!: raw_zminus_inject)
241 done
243 lemma zminus_inject: "[| \$-z = \$-w;  z: int;  w: int |] ==> z=w"
244 by auto
246 lemma raw_zminus:
247     "[| x\<in>nat;  y\<in>nat |] ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}"
248 apply (simp add: raw_zminus_def UN_equiv_class [OF equiv_intrel zminus_congruent])
249 done
251 lemma zminus:
252     "[| x\<in>nat;  y\<in>nat |]
253      ==> \$- (intrel``{<x,y>}) = intrel `` {<y,x>}"
254 by (simp add: zminus_def raw_zminus image_intrel_int)
256 lemma raw_zminus_zminus: "z : int ==> raw_zminus (raw_zminus(z)) = z"
257 by (auto simp add: int_def raw_zminus)
259 lemma zminus_zminus_intify [simp]: "\$- (\$- z) = intify(z)"
260 by (simp add: zminus_def raw_zminus_type raw_zminus_zminus)
262 lemma zminus_int0 [simp]: "\$- (\$#0) = \$#0"
263 by (simp add: int_of_def zminus)
265 lemma zminus_zminus: "z : int ==> \$- (\$- z) = z"
266 by simp
269 subsection{*@{term znegative}: the test for negative integers*}
271 lemma znegative: "[| x\<in>nat; y\<in>nat |] ==> znegative(intrel``{<x,y>}) <-> x<y"
272 apply (cases "x<y")
273 apply (auto simp add: znegative_def not_lt_iff_le)
274 apply (subgoal_tac "y #+ x2 < x #+ y2", force)
276 done
278 (*No natural number is negative!*)
279 lemma not_znegative_int_of [iff]: "~ znegative(\$# n)"
280 by (simp add: znegative int_of_def)
282 lemma znegative_zminus_int_of [simp]: "znegative(\$- \$# succ(n))"
283 by (simp add: znegative int_of_def zminus natify_succ)
285 lemma not_znegative_imp_zero: "~ znegative(\$- \$# n) ==> natify(n)=0"
286 by (simp add: znegative int_of_def zminus Ord_0_lt_iff [THEN iff_sym])
289 subsection{*@{term nat_of}: Coercion of an Integer to a Natural Number*}
291 lemma nat_of_intify [simp]: "nat_of(intify(z)) = nat_of(z)"
294 lemma nat_of_congruent: "(\<lambda>x. (\<lambda>\<langle>x,y\<rangle>. x #- y)(x)) respects intrel"
297 lemma raw_nat_of:
298     "[| x\<in>nat;  y\<in>nat |] ==> raw_nat_of(intrel``{<x,y>}) = x#-y"
299 by (simp add: raw_nat_of_def UN_equiv_class [OF equiv_intrel nat_of_congruent])
301 lemma raw_nat_of_int_of: "raw_nat_of(\$# n) = natify(n)"
302 by (simp add: int_of_def raw_nat_of)
304 lemma nat_of_int_of [simp]: "nat_of(\$# n) = natify(n)"
305 by (simp add: raw_nat_of_int_of nat_of_def)
307 lemma raw_nat_of_type: "raw_nat_of(z) \<in> nat"
310 lemma nat_of_type [iff,TC]: "nat_of(z) \<in> nat"
311 by (simp add: nat_of_def raw_nat_of_type)
313 subsection{*zmagnitude: magnitide of an integer, as a natural number*}
315 lemma zmagnitude_int_of [simp]: "zmagnitude(\$# n) = natify(n)"
316 by (auto simp add: zmagnitude_def int_of_eq)
318 lemma natify_int_of_eq: "natify(x)=n ==> \$#x = \$# n"
319 apply (drule sym)
320 apply (simp (no_asm_simp) add: int_of_eq)
321 done
323 lemma zmagnitude_zminus_int_of [simp]: "zmagnitude(\$- \$# n) = natify(n)"
325 apply (rule the_equality)
326 apply (auto dest!: not_znegative_imp_zero natify_int_of_eq
327             iff del: int_of_eq, auto)
328 done
330 lemma zmagnitude_type [iff,TC]: "zmagnitude(z)\<in>nat"
332 apply (rule theI2, auto)
333 done
335 lemma not_zneg_int_of:
336      "[| z: int; ~ znegative(z) |] ==> \<exists>n\<in>nat. z = \$# n"
337 apply (auto simp add: int_def znegative int_of_def not_lt_iff_le)
338 apply (rename_tac x y)
339 apply (rule_tac x="x#-y" in bexI)
341 done
343 lemma not_zneg_mag [simp]:
344      "[| z: int; ~ znegative(z) |] ==> \$# (zmagnitude(z)) = z"
345 by (drule not_zneg_int_of, auto)
347 lemma zneg_int_of:
348      "[| znegative(z); z: int |] ==> \<exists>n\<in>nat. z = \$- (\$# succ(n))"
351 lemma zneg_mag [simp]:
352      "[| znegative(z); z: int |] ==> \$# (zmagnitude(z)) = \$- z"
353 by (drule zneg_int_of, auto)
355 lemma int_cases: "z : int ==> \<exists>n\<in>nat. z = \$# n | z = \$- (\$# succ(n))"
356 apply (case_tac "znegative (z) ")
357 prefer 2 apply (blast dest: not_zneg_mag sym)
358 apply (blast dest: zneg_int_of)
359 done
361 lemma not_zneg_raw_nat_of:
362      "[| ~ znegative(z); z: int |] ==> \$# (raw_nat_of(z)) = z"
363 apply (drule not_zneg_int_of)
364 apply (auto simp add: raw_nat_of_type raw_nat_of_int_of)
365 done
367 lemma not_zneg_nat_of_intify:
368      "~ znegative(intify(z)) ==> \$# (nat_of(z)) = intify(z)"
369 by (simp (no_asm_simp) add: nat_of_def not_zneg_raw_nat_of)
371 lemma not_zneg_nat_of: "[| ~ znegative(z); z: int |] ==> \$# (nat_of(z)) = z"
372 apply (simp (no_asm_simp) add: not_zneg_nat_of_intify)
373 done
375 lemma zneg_nat_of [simp]: "znegative(intify(z)) ==> nat_of(z) = 0"
376 apply (subgoal_tac "intify(z) \<in> int")
378 apply (auto simp add: znegative nat_of_def raw_nat_of
380 done
387     "(%z1 z2. let <x1,y1>=z1; <x2,y2>=z2
388                             in intrel``{<x1#+x2, y1#+y2>})
389      respects2 intrel"
391 (*Proof via congruent2_commuteI seems longer*)
392 apply safe
394 (*The rest should be trivial, but rearranging terms is hard
395   add_ac does not help rewriting with the assumptions.*)
396 apply (rule_tac m1 = x1a in add_left_commute [THEN ssubst])
397 apply (rule_tac m1 = x2a in add_left_commute [THEN ssubst])
399 done
401 lemma raw_zadd_type: "[| z: int;  w: int |] ==> raw_zadd(z,w) : int"
403 apply (rule UN_equiv_class_type2 [OF equiv_intrel zadd_congruent2], assumption+)
405 done
407 lemma zadd_type [iff,TC]: "z \$+ w : int"
411   "[| x1\<in>nat; y1\<in>nat;  x2\<in>nat; y2\<in>nat |]
412    ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) =
413        intrel `` {<x1#+x2, y1#+y2>}"
415              UN_equiv_class2 [OF equiv_intrel equiv_intrel zadd_congruent2])
417 done
420   "[| x1\<in>nat; y1\<in>nat;  x2\<in>nat; y2\<in>nat |]
421    ==> (intrel``{<x1,y1>}) \$+ (intrel``{<x2,y2>}) =
422        intrel `` {<x1#+x2, y1#+y2>}"
428 lemma zadd_int0_intify [simp]: "\$#0 \$+ z = intify(z)"
431 lemma zadd_int0: "z: int ==> \$#0 \$+ z = z"
432 by simp
435      "[| z: int;  w: int |] ==> \$- raw_zadd(z,w) = raw_zadd(\$- z, \$- w)"
438 lemma zminus_zadd_distrib [simp]: "\$- (z \$+ w) = \$- z \$+ \$- w"
445 lemma zadd_commute: "z \$+ w = w \$+ z"
449     "[| z1: int;  z2: int;  z3: int |]
453 lemma zadd_assoc: "(z1 \$+ z2) \$+ z3 = z1 \$+ (z2 \$+ z3)"
456 (*For AC rewriting*)
457 lemma zadd_left_commute: "z1\$+(z2\$+z3) = z2\$+(z1\$+z3)"
460 done
462 (*Integer addition is an AC operator*)
465 lemma int_of_add: "\$# (m #+ n) = (\$#m) \$+ (\$#n)"
468 lemma int_succ_int_1: "\$# succ(m) = \$# 1 \$+ (\$# m)"
471 lemma int_of_diff:
472      "[| m\<in>nat;  n le m |] ==> \$# (m #- n) = (\$#m) \$- (\$#n)"
473 apply (simp add: int_of_def zdiff_def)
474 apply (frule lt_nat_in_nat)
476 done
478 lemma raw_zadd_zminus_inverse: "z : int ==> raw_zadd (z, \$- z) = \$#0"
481 lemma zadd_zminus_inverse [simp]: "z \$+ (\$- z) = \$#0"
483 apply (subst zminus_intify [symmetric])
484 apply (rule intify_in_int [THEN raw_zadd_zminus_inverse])
485 done
487 lemma zadd_zminus_inverse2 [simp]: "(\$- z) \$+ z = \$#0"
490 lemma zadd_int0_right_intify [simp]: "z \$+ \$#0 = intify(z)"
493 lemma zadd_int0_right: "z:int ==> z \$+ \$#0 = z"
494 by simp
497 subsection{*@{term zmult}: Integer Multiplication*}
499 text{*Congruence property for multiplication*}
500 lemma zmult_congruent2:
501     "(%p1 p2. split(%x1 y1. split(%x2 y2.
502                     intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))
503      respects2 intrel"
504 apply (rule equiv_intrel [THEN congruent2_commuteI], auto)
505 (*Proof that zmult is congruent in one argument*)
506 apply (rename_tac x y)
507 apply (frule_tac t = "%u. x#*u" in sym [THEN subst_context])
508 apply (drule_tac t = "%u. y#*u" in subst_context)
511 done
514 lemma raw_zmult_type: "[| z: int;  w: int |] ==> raw_zmult(z,w) : int"
515 apply (simp add: int_def raw_zmult_def)
516 apply (rule UN_equiv_class_type2 [OF equiv_intrel zmult_congruent2], assumption+)
518 done
520 lemma zmult_type [iff,TC]: "z \$* w : int"
521 by (simp add: zmult_def raw_zmult_type)
523 lemma raw_zmult:
524      "[| x1\<in>nat; y1\<in>nat;  x2\<in>nat; y2\<in>nat |]
525       ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) =
526           intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}"
528            UN_equiv_class2 [OF equiv_intrel equiv_intrel zmult_congruent2])
530 lemma zmult:
531      "[| x1\<in>nat; y1\<in>nat;  x2\<in>nat; y2\<in>nat |]
532       ==> (intrel``{<x1,y1>}) \$* (intrel``{<x2,y2>}) =
533           intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}"
534 by (simp add: zmult_def raw_zmult image_intrel_int)
536 lemma raw_zmult_int0: "z : int ==> raw_zmult (\$#0,z) = \$#0"
537 by (auto simp add: int_def int_of_def raw_zmult)
539 lemma zmult_int0 [simp]: "\$#0 \$* z = \$#0"
540 by (simp add: zmult_def raw_zmult_int0)
542 lemma raw_zmult_int1: "z : int ==> raw_zmult (\$#1,z) = z"
543 by (auto simp add: int_def int_of_def raw_zmult)
545 lemma zmult_int1_intify [simp]: "\$#1 \$* z = intify(z)"
546 by (simp add: zmult_def raw_zmult_int1)
548 lemma zmult_int1: "z : int ==> \$#1 \$* z = z"
549 by simp
551 lemma raw_zmult_commute:
552      "[| z: int;  w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)"
555 lemma zmult_commute: "z \$* w = w \$* z"
556 by (simp add: zmult_def raw_zmult_commute)
558 lemma raw_zmult_zminus:
559      "[| z: int;  w: int |] ==> raw_zmult(\$- z, w) = \$- raw_zmult(z, w)"
562 lemma zmult_zminus [simp]: "(\$- z) \$* w = \$- (z \$* w)"
563 apply (simp add: zmult_def raw_zmult_zminus)
564 apply (subst zminus_intify [symmetric], rule raw_zmult_zminus, auto)
565 done
567 lemma zmult_zminus_right [simp]: "w \$* (\$- z) = \$- (w \$* z)"
568 by (simp add: zmult_commute [of w])
570 lemma raw_zmult_assoc:
571     "[| z1: int;  z2: int;  z3: int |]
572      ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))"
575 lemma zmult_assoc: "(z1 \$* z2) \$* z3 = z1 \$* (z2 \$* z3)"
576 by (simp add: zmult_def raw_zmult_type raw_zmult_assoc)
578 (*For AC rewriting*)
579 lemma zmult_left_commute: "z1\$*(z2\$*z3) = z2\$*(z1\$*z3)"
580 apply (simp add: zmult_assoc [symmetric])
582 done
584 (*Integer multiplication is an AC operator*)
585 lemmas zmult_ac = zmult_assoc zmult_commute zmult_left_commute
588     "[| z1: int;  z2: int;  w: int |]
593 lemma zadd_zmult_distrib: "(z1 \$+ z2) \$* w = (z1 \$* w) \$+ (z2 \$* w)"
597 lemma zadd_zmult_distrib2: "w \$* (z1 \$+ z2) = (w \$* z1) \$+ (w \$* z2)"
600 lemmas int_typechecks =
601   int_of_type zminus_type zmagnitude_type zadd_type zmult_type
604 (*** Subtraction laws ***)
606 lemma zdiff_type [iff,TC]: "z \$- w : int"
609 lemma zminus_zdiff_eq [simp]: "\$- (z \$- y) = y \$- z"
612 lemma zdiff_zmult_distrib: "(z1 \$- z2) \$* w = (z1 \$* w) \$- (z2 \$* w)"
616 done
618 lemma zdiff_zmult_distrib2: "w \$* (z1 \$- z2) = (w \$* z1) \$- (w \$* z2)"
619 by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
621 lemma zadd_zdiff_eq: "x \$+ (y \$- z) = (x \$+ y) \$- z"
624 lemma zdiff_zadd_eq: "(x \$- y) \$+ z = (x \$+ z) \$- y"
628 subsection{*The "Less Than" Relation*}
630 (*"Less than" is a linear ordering*)
631 lemma zless_linear_lemma:
632      "[| z: int; w: int |] ==> z\$<w | z=w | w\$<z"
633 apply (simp add: int_def zless_def znegative_def zdiff_def, auto)
635 apply (rule_tac i = "xb#+ya" and j = "xc #+ y" in Ord_linear_lt)
637 done
639 lemma zless_linear: "z\$<w | intify(z)=intify(w) | w\$<z"
640 apply (cut_tac z = " intify (z) " and w = " intify (w) " in zless_linear_lemma)
641 apply auto
642 done
644 lemma zless_not_refl [iff]: "~ (z\$<z)"
645 by (auto simp add: zless_def znegative_def int_of_def zdiff_def)
647 lemma neq_iff_zless: "[| x: int; y: int |] ==> (x ~= y) <-> (x \$< y | y \$< x)"
648 by (cut_tac z = x and w = y in zless_linear, auto)
650 lemma zless_imp_intify_neq: "w \$< z ==> intify(w) ~= intify(z)"
651 apply auto
652 apply (subgoal_tac "~ (intify (w) \$< intify (z))")
653 apply (erule_tac [2] ssubst)
654 apply (simp (no_asm_use))
655 apply auto
656 done
658 (*This lemma allows direct proofs of other <-properties*)
660     "[| w \$< z; w: int; z: int |] ==> (\<exists>n\<in>nat. z = w \$+ \$#(succ(n)))"
661 apply (simp add: zless_def znegative_def zdiff_def int_def)
663 apply (rule_tac x = k in bexI)
665 done
668      "w \$< z ==> (\<exists>n\<in>nat. w \$+ \$#(succ(n)) = intify(z))"
669 apply (subgoal_tac "intify (w) \$< intify (z) ")
670 apply (drule_tac w = "intify (w) " in zless_imp_succ_zadd_lemma)
671 apply auto
672 done
675     "w : int ==> w \$< w \$+ \$# succ(n)"
676 apply (simp add: zless_def znegative_def zdiff_def int_def)
678 apply (rule_tac x = 0 in exI, auto)
679 done
681 lemma zless_succ_zadd: "w \$< w \$+ \$# succ(n)"
682 by (cut_tac intify_in_int [THEN zless_succ_zadd_lemma], auto)
685      "w \$< z <-> (\<exists>n\<in>nat. w \$+ \$#(succ(n)) = intify(z))"
686 apply (rule iffI)
688 apply (rename_tac "n")
689 apply (cut_tac w = w and n = n in zless_succ_zadd, auto)
690 done
692 lemma zless_int_of [simp]: "[| m\<in>nat; n\<in>nat |] ==> (\$#m \$< \$#n) <-> (m<n)"
694 apply (blast intro: sym)
695 done
697 lemma zless_trans_lemma:
698     "[| x \$< y; y \$< z; x: int; y : int; z: int |] ==> x \$< z"
699 apply (simp add: zless_def znegative_def zdiff_def int_def)
701 apply (rename_tac x1 x2 y1 y2)
702 apply (rule_tac x = "x1#+x2" in exI)
703 apply (rule_tac x = "y1#+y2" in exI)
705 apply (rule sym)
707 apply auto
708 done
710 lemma zless_trans: "[| x \$< y; y \$< z |] ==> x \$< z"
711 apply (subgoal_tac "intify (x) \$< intify (z) ")
712 apply (rule_tac [2] y = "intify (y) " in zless_trans_lemma)
713 apply auto
714 done
716 lemma zless_not_sym: "z \$< w ==> ~ (w \$< z)"
717 by (blast dest: zless_trans)
719 (* [| z \$< w; ~ P ==> w \$< z |] ==> P *)
720 lemmas zless_asym = zless_not_sym [THEN swap, standard]
722 lemma zless_imp_zle: "z \$< w ==> z \$<= w"
725 lemma zle_linear: "z \$<= w | w \$<= z"
727 apply (cut_tac zless_linear, blast)
728 done
731 subsection{*Less Than or Equals*}
733 lemma zle_refl: "z \$<= z"
736 lemma zle_eq_refl: "x=y ==> x \$<= y"
739 lemma zle_anti_sym_intify: "[| x \$<= y; y \$<= x |] ==> intify(x) = intify(y)"
740 apply (simp add: zle_def, auto)
741 apply (blast dest: zless_trans)
742 done
744 lemma zle_anti_sym: "[| x \$<= y; y \$<= x; x: int; y: int |] ==> x=y"
745 by (drule zle_anti_sym_intify, auto)
747 lemma zle_trans_lemma:
748      "[| x: int; y: int; z: int; x \$<= y; y \$<= z |] ==> x \$<= z"
749 apply (simp add: zle_def, auto)
750 apply (blast intro: zless_trans)
751 done
753 lemma zle_trans: "[| x \$<= y; y \$<= z |] ==> x \$<= z"
754 apply (subgoal_tac "intify (x) \$<= intify (z) ")
755 apply (rule_tac [2] y = "intify (y) " in zle_trans_lemma)
756 apply auto
757 done
759 lemma zle_zless_trans: "[| i \$<= j; j \$< k |] ==> i \$< k"
760 apply (auto simp add: zle_def)
761 apply (blast intro: zless_trans)
763 done
765 lemma zless_zle_trans: "[| i \$< j; j \$<= k |] ==> i \$< k"
766 apply (auto simp add: zle_def)
767 apply (blast intro: zless_trans)
768 apply (simp add: zless_def zdiff_def zminus_def)
769 done
771 lemma not_zless_iff_zle: "~ (z \$< w) <-> (w \$<= z)"
772 apply (cut_tac z = z and w = w in zless_linear)
773 apply (auto dest: zless_trans simp add: zle_def)
774 apply (auto dest!: zless_imp_intify_neq)
775 done
777 lemma not_zle_iff_zless: "~ (z \$<= w) <-> (w \$< z)"
778 by (simp add: not_zless_iff_zle [THEN iff_sym])
781 subsection{*More subtraction laws (for @{text zcompare_rls})*}
783 lemma zdiff_zdiff_eq: "(x \$- y) \$- z = x \$- (y \$+ z)"
786 lemma zdiff_zdiff_eq2: "x \$- (y \$- z) = (x \$+ z) \$- y"
789 lemma zdiff_zless_iff: "(x\$-y \$< z) <-> (x \$< z \$+ y)"
792 lemma zless_zdiff_iff: "(x \$< z\$-y) <-> (x \$+ y \$< z)"
795 lemma zdiff_eq_iff: "[| x: int; z: int |] ==> (x\$-y = z) <-> (x = z \$+ y)"
798 lemma eq_zdiff_iff: "[| x: int; z: int |] ==> (x = z\$-y) <-> (x \$+ y = z)"
801 lemma zdiff_zle_iff_lemma:
802      "[| x: int; z: int |] ==> (x\$-y \$<= z) <-> (x \$<= z \$+ y)"
803 by (auto simp add: zle_def zdiff_eq_iff zdiff_zless_iff)
805 lemma zdiff_zle_iff: "(x\$-y \$<= z) <-> (x \$<= z \$+ y)"
806 by (cut_tac zdiff_zle_iff_lemma [OF intify_in_int intify_in_int], simp)
808 lemma zle_zdiff_iff_lemma:
809      "[| x: int; z: int |] ==>(x \$<= z\$-y) <-> (x \$+ y \$<= z)"
810 apply (auto simp add: zle_def zdiff_eq_iff zless_zdiff_iff)
812 done
814 lemma zle_zdiff_iff: "(x \$<= z\$-y) <-> (x \$+ y \$<= z)"
815 by (cut_tac zle_zdiff_iff_lemma [ OF intify_in_int intify_in_int], simp)
817 text{*This list of rewrites simplifies (in)equalities by bringing subtractions
818   to the top and then moving negative terms to the other side.
820 lemmas zcompare_rls =
821      zdiff_def [symmetric]
823      zdiff_zless_iff zless_zdiff_iff zdiff_zle_iff zle_zdiff_iff
824      zdiff_eq_iff eq_zdiff_iff
827 subsection{*Monotonicity and Cancellation Results for Instantiation
828      of the CancelNumerals Simprocs*}
831      "[| w: int; w': int |] ==> (z \$+ w' = z \$+ w) <-> (w' = w)"
832 apply safe
833 apply (drule_tac t = "%x. x \$+ (\$-z) " in subst_context)
835 done
838      "(z \$+ w' = z \$+ w) <-> intify(w') = intify(w)"
839 apply (rule iff_trans)
840 apply (rule_tac [2] zadd_left_cancel, auto)
841 done
844      "[| w: int; w': int |] ==> (w' \$+ z = w \$+ z) <-> (w' = w)"
845 apply safe
846 apply (drule_tac t = "%x. x \$+ (\$-z) " in subst_context)
848 done
851      "(w' \$+ z = w \$+ z) <-> intify(w') = intify(w)"
852 apply (rule iff_trans)
853 apply (rule_tac [2] zadd_right_cancel, auto)
854 done
856 lemma zadd_right_cancel_zless [simp]: "(w' \$+ z \$< w \$+ z) <-> (w' \$< w)"
859 lemma zadd_left_cancel_zless [simp]: "(z \$+ w' \$< z \$+ w) <-> (w' \$< w)"
862 lemma zadd_right_cancel_zle [simp]: "(w' \$+ z \$<= w \$+ z) <-> w' \$<= w"
865 lemma zadd_left_cancel_zle [simp]: "(z \$+ w' \$<= z \$+ w) <->  w' \$<= w"
869 (*"v \$<= w ==> v\$+z \$<= w\$+z"*)
872 (*"v \$<= w ==> z\$+v \$<= z\$+w"*)
875 (*"v \$<= w ==> v\$+z \$<= w\$+z"*)
878 (*"v \$<= w ==> z\$+v \$<= z\$+w"*)
881 lemma zadd_zle_mono: "[| w' \$<= w; z' \$<= z |] ==> w' \$+ z' \$<= w \$+ z"
882 by (erule zadd_zle_mono1 [THEN zle_trans], simp)
884 lemma zadd_zless_mono: "[| w' \$< w; z' \$<= z |] ==> w' \$+ z' \$< w \$+ z"
885 by (erule zadd_zless_mono1 [THEN zless_zle_trans], simp)
888 subsection{*Comparison laws*}
890 lemma zminus_zless_zminus [simp]: "(\$- x \$< \$- y) <-> (y \$< x)"
893 lemma zminus_zle_zminus [simp]: "(\$- x \$<= \$- y) <-> (y \$<= x)"
894 by (simp add: not_zless_iff_zle [THEN iff_sym])
896 subsubsection{*More inequality lemmas*}
898 lemma equation_zminus: "[| x: int;  y: int |] ==> (x = \$- y) <-> (y = \$- x)"
899 by auto
901 lemma zminus_equation: "[| x: int;  y: int |] ==> (\$- x = y) <-> (\$- y = x)"
902 by auto
904 lemma equation_zminus_intify: "(intify(x) = \$- y) <-> (intify(y) = \$- x)"
905 apply (cut_tac x = "intify (x) " and y = "intify (y) " in equation_zminus)
906 apply auto
907 done
909 lemma zminus_equation_intify: "(\$- x = intify(y)) <-> (\$- y = intify(x))"
910 apply (cut_tac x = "intify (x) " and y = "intify (y) " in zminus_equation)
911 apply auto
912 done
915 subsubsection{*The next several equations are permutative: watch out!*}
917 lemma zless_zminus: "(x \$< \$- y) <-> (y \$< \$- x)"