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