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