src/ZF/Integ/Int.ML
author paulson
Fri Aug 11 10:34:02 2000 +0200 (2000-08-11)
changeset 9576 3df14e0a3a51
parent 9570 e16e168984e1
child 9578 ab26d6c8ebfe
permissions -rw-r--r--
interim working version: more improvements to the integers
paulson@5561
     1
(*  Title:      ZF/Integ/Int.ML
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
The integers as equivalence classes over nat*nat.
paulson@5561
     7
paulson@5561
     8
Could also prove...
paulson@9548
     9
"znegative(z) ==> $# zmagnitude(z) = $- z"
paulson@5561
    10
"~ znegative(z) ==> $# zmagnitude(z) = z"
paulson@5561
    11
*)
paulson@5561
    12
paulson@5561
    13
AddSEs [quotientE];
paulson@5561
    14
paulson@5561
    15
(*** Proving that intrel is an equivalence relation ***)
paulson@5561
    16
paulson@5561
    17
(** Natural deduction for intrel **)
paulson@5561
    18
paulson@5561
    19
Goalw [intrel_def]
paulson@5561
    20
    "<<x1,y1>,<x2,y2>>: intrel <-> \
paulson@5561
    21
\    x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1";
paulson@5561
    22
by (Fast_tac 1);
paulson@5561
    23
qed "intrel_iff";
paulson@5561
    24
paulson@5561
    25
Goalw [intrel_def]
paulson@9496
    26
    "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |]  \
paulson@9496
    27
\    ==> <<x1,y1>,<x2,y2>>: intrel";
paulson@5561
    28
by (fast_tac (claset() addIs prems) 1);
paulson@5561
    29
qed "intrelI";
paulson@5561
    30
paulson@5561
    31
(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
paulson@5561
    32
Goalw [intrel_def]
paulson@5561
    33
  "p: intrel --> (EX x1 y1 x2 y2. \
paulson@5561
    34
\                  p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \
paulson@5561
    35
\                  x1: nat & y1: nat & x2: nat & y2: nat)";
paulson@5561
    36
by (Fast_tac 1);
paulson@5561
    37
qed "intrelE_lemma";
paulson@5561
    38
paulson@5561
    39
val [major,minor] = goal thy
paulson@5561
    40
  "[| p: intrel;  \
paulson@5561
    41
\     !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1; \
paulson@5561
    42
\                       x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \
paulson@5561
    43
\  ==> Q";
paulson@5561
    44
by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
paulson@5561
    45
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
paulson@5561
    46
qed "intrelE";
paulson@5561
    47
paulson@5561
    48
AddSIs [intrelI];
paulson@5561
    49
AddSEs [intrelE];
paulson@5561
    50
paulson@9548
    51
Goal "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1";
paulson@9548
    52
by (rtac sym 1);
paulson@9548
    53
by (REPEAT (etac add_left_cancel 1));
paulson@9548
    54
by (ALLGOALS Asm_simp_tac);
paulson@9491
    55
qed "int_trans_lemma";
paulson@9491
    56
paulson@5561
    57
Goalw [equiv_def, refl_def, sym_def, trans_def]
paulson@5561
    58
    "equiv(nat*nat, intrel)";
paulson@5561
    59
by (fast_tac (claset() addSEs [sym, int_trans_lemma]) 1);
paulson@5561
    60
qed "equiv_intrel";
paulson@5561
    61
paulson@5561
    62
paulson@9496
    63
Goalw [int_def] "[| m: nat; n: nat |] ==> intrel `` {<m,n>} : int";
paulson@9496
    64
by (blast_tac (claset() addIs [quotientI]) 1);
paulson@9496
    65
qed "image_intrel_int";
paulson@9496
    66
paulson@9496
    67
paulson@5561
    68
Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
paulson@5561
    69
	  add_0_right, add_succ_right];
paulson@5561
    70
Addcongs [conj_cong];
paulson@5561
    71
paulson@5561
    72
val eq_intrelD = equiv_intrel RSN (2,eq_equiv_class);
paulson@5561
    73
paulson@5561
    74
(** int_of: the injection from nat to int **)
paulson@5561
    75
paulson@9496
    76
Goalw [int_def,quotient_def,int_of_def]  "$#m : int";
paulson@6153
    77
by Auto_tac;
paulson@5561
    78
qed "int_of_type";
paulson@5561
    79
paulson@9496
    80
AddIffs [int_of_type];
paulson@9496
    81
AddTCs  [int_of_type];
paulson@9496
    82
paulson@5561
    83
paulson@9496
    84
Goalw [int_of_def] "($# m = $# n) <-> natify(m)=natify(n)"; 
paulson@9496
    85
by Auto_tac;  
paulson@9496
    86
qed "int_of_eq"; 
paulson@9496
    87
AddIffs [int_of_eq];
paulson@9496
    88
paulson@9496
    89
Goal "[| $#m = $#n;  m: nat;  n: nat |] ==> m=n";
paulson@9496
    90
by (dtac (int_of_eq RS iffD1) 1);
paulson@6153
    91
by Auto_tac;
paulson@5561
    92
qed "int_of_inject";
paulson@5561
    93
paulson@9496
    94
paulson@9496
    95
(** intify: coercion from anything to int **)
paulson@9496
    96
paulson@9496
    97
Goal "intify(x) : int";
paulson@9496
    98
by (simp_tac (simpset() addsimps [intify_def]) 1);
paulson@9496
    99
qed "intify_in_int";
paulson@9496
   100
AddIffs [intify_in_int];
paulson@9496
   101
AddTCs [intify_in_int];
paulson@9496
   102
paulson@9496
   103
Goal "n : int ==> intify(n) = n";
paulson@9496
   104
by (asm_simp_tac (simpset() addsimps [intify_def]) 1);
paulson@9496
   105
qed "intify_ident";
paulson@9496
   106
Addsimps [intify_ident];
paulson@9496
   107
paulson@9496
   108
paulson@9496
   109
(*** Collapsing rules: to remove intify from arithmetic expressions ***)
paulson@9496
   110
paulson@9496
   111
Goal "intify(intify(x)) = intify(x)";
paulson@9496
   112
by (Simp_tac 1);
paulson@9496
   113
qed "intify_idem";
paulson@9496
   114
Addsimps [intify_idem];
paulson@9496
   115
paulson@9496
   116
Goal "$# (natify(m)) = $# m";
paulson@9496
   117
by (simp_tac (simpset() addsimps [int_of_def]) 1);
paulson@9496
   118
qed "int_of_natify";
paulson@5561
   119
paulson@9548
   120
Goal "$- (intify(m)) = $- m";
paulson@9496
   121
by (simp_tac (simpset() addsimps [zminus_def]) 1);
paulson@9496
   122
qed "zminus_intify";
paulson@9496
   123
paulson@9496
   124
Addsimps [int_of_natify, zminus_intify];
paulson@9496
   125
paulson@9496
   126
(** Addition **)
paulson@9496
   127
paulson@9496
   128
Goal "intify(x) $+ y = x $+ y";
paulson@9496
   129
by (simp_tac (simpset() addsimps [zadd_def]) 1);
paulson@9496
   130
qed "zadd_intify1";
paulson@9496
   131
paulson@9496
   132
Goal "x $+ intify(y) = x $+ y";
paulson@9496
   133
by (simp_tac (simpset() addsimps [zadd_def]) 1);
paulson@9496
   134
qed "zadd_intify2";
paulson@9496
   135
Addsimps [zadd_intify1, zadd_intify2];
paulson@9496
   136
paulson@9548
   137
(** Subtraction **)
paulson@9548
   138
paulson@9548
   139
Goal "intify(x) $- y = x $- y";
paulson@9548
   140
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
paulson@9548
   141
qed "zdiff_intify1";
paulson@9548
   142
paulson@9548
   143
Goal "x $- intify(y) = x $- y";
paulson@9548
   144
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
paulson@9548
   145
qed "zdiff_intify2";
paulson@9548
   146
Addsimps [zdiff_intify1, zdiff_intify2];
paulson@9548
   147
paulson@9496
   148
(** Multiplication **)
paulson@9496
   149
paulson@9496
   150
Goal "intify(x) $* y = x $* y";
paulson@9496
   151
by (simp_tac (simpset() addsimps [zmult_def]) 1);
paulson@9496
   152
qed "zmult_intify1";
paulson@9496
   153
paulson@9496
   154
Goal "x $* intify(y) = x $* y";
paulson@9496
   155
by (simp_tac (simpset() addsimps [zmult_def]) 1);
paulson@9496
   156
qed "zmult_intify2";
paulson@9496
   157
Addsimps [zmult_intify1, zmult_intify2];
paulson@9496
   158
paulson@9548
   159
(** Orderings **)
paulson@9548
   160
paulson@9548
   161
Goal "intify(x) $< y <-> x $< y";
paulson@9548
   162
by (simp_tac (simpset() addsimps [zless_def]) 1);
paulson@9548
   163
qed "zless_intify1";
paulson@9548
   164
paulson@9548
   165
Goal "x $< intify(y) <-> x $< y";
paulson@9548
   166
by (simp_tac (simpset() addsimps [zless_def]) 1);
paulson@9548
   167
qed "zless_intify2";
paulson@9548
   168
Addsimps [zless_intify1, zless_intify2];
paulson@9548
   169
paulson@9570
   170
Goal "intify(x) $<= y <-> x $<= y";
paulson@9570
   171
by (simp_tac (simpset() addsimps [zle_def]) 1);
paulson@9570
   172
qed "zle_intify1";
paulson@9570
   173
paulson@9570
   174
Goal "x $<= intify(y) <-> x $<= y";
paulson@9570
   175
by (simp_tac (simpset() addsimps [zle_def]) 1);
paulson@9570
   176
qed "zle_intify2";
paulson@9570
   177
Addsimps [zle_intify1, zle_intify2];
paulson@9570
   178
paulson@5561
   179
paulson@5561
   180
(**** zminus: unary negation on int ****)
paulson@5561
   181
paulson@5561
   182
Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})";
paulson@5561
   183
by Safe_tac;
paulson@5561
   184
by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
paulson@5561
   185
qed "zminus_congruent";
paulson@5561
   186
paulson@9333
   187
val RSLIST = curry (op MRS);
paulson@9333
   188
paulson@5561
   189
(*Resolve th against the corresponding facts for zminus*)
paulson@5561
   190
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
paulson@5561
   191
paulson@9496
   192
Goalw [int_def,raw_zminus_def] "z : int ==> raw_zminus(z) : int";
paulson@6153
   193
by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
paulson@9496
   194
qed "raw_zminus_type";
paulson@9496
   195
paulson@9548
   196
Goalw [zminus_def] "$-z : int";
paulson@9496
   197
by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type]) 1);
paulson@5561
   198
qed "zminus_type";
paulson@9496
   199
AddIffs [zminus_type];
paulson@6153
   200
AddTCs [zminus_type];
paulson@5561
   201
paulson@9496
   202
paulson@9496
   203
Goalw [int_def,raw_zminus_def]
paulson@9496
   204
     "[| raw_zminus(z) = raw_zminus(w);  z: int;  w: int |] ==> z=w";
paulson@5561
   205
by (etac (zminus_ize UN_equiv_class_inject) 1);
paulson@5561
   206
by Safe_tac;
paulson@9496
   207
by (auto_tac (claset() addDs [eq_intrelD], simpset() addsimps add_ac));  
paulson@9496
   208
qed "raw_zminus_inject";
paulson@9496
   209
paulson@9548
   210
Goalw [zminus_def] "$-z = $-w ==> intify(z) = intify(w)";
paulson@9496
   211
by (blast_tac (claset() addSDs [raw_zminus_inject]) 1);
paulson@9496
   212
qed "zminus_inject_intify";
paulson@9496
   213
paulson@9496
   214
AddSDs [zminus_inject_intify];
paulson@9496
   215
paulson@9548
   216
Goal "[| $-z = $-w;  z: int;  w: int |] ==> z=w";
paulson@9496
   217
by Auto_tac;  
paulson@5561
   218
qed "zminus_inject";
paulson@5561
   219
paulson@9496
   220
Goalw [raw_zminus_def]
paulson@9496
   221
    "[| x: nat;  y: nat |] \
paulson@9496
   222
\    ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}";
paulson@9496
   223
by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
paulson@9496
   224
qed "raw_zminus";
paulson@9496
   225
paulson@5561
   226
Goalw [zminus_def]
paulson@9496
   227
    "[| x: nat;  y: nat |] \
paulson@9548
   228
\    ==> $- (intrel``{<x,y>}) = intrel `` {<y,x>}";
paulson@9496
   229
by (asm_simp_tac (simpset() addsimps [raw_zminus, image_intrel_int]) 1);
paulson@5561
   230
qed "zminus";
paulson@5561
   231
paulson@9496
   232
Goalw [int_def] "z : int ==> raw_zminus (raw_zminus(z)) = z";
paulson@9496
   233
by (auto_tac (claset(), simpset() addsimps [raw_zminus]));  
paulson@9496
   234
qed "raw_zminus_zminus";
paulson@5561
   235
paulson@9548
   236
Goal "$- ($- z) = intify(z)";
paulson@9496
   237
by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type, 
paulson@9496
   238
	                          raw_zminus_zminus]) 1);
paulson@9496
   239
qed "zminus_zminus_intify"; 
paulson@9496
   240
paulson@9548
   241
Goalw [int_of_def] "$- ($#0) = $#0";
paulson@5561
   242
by (simp_tac (simpset() addsimps [zminus]) 1);
paulson@9576
   243
qed "zminus_int0";
paulson@5561
   244
paulson@9576
   245
Addsimps [zminus_zminus_intify, zminus_int0];
paulson@9496
   246
paulson@9548
   247
Goal "z : int ==> $- ($- z) = z";
paulson@9496
   248
by (Asm_simp_tac 1);
paulson@9496
   249
qed "zminus_zminus";
paulson@5561
   250
paulson@5561
   251
paulson@5561
   252
(**** znegative: the test for negative integers ****)
paulson@5561
   253
paulson@5561
   254
(*No natural number is negative!*)
paulson@5561
   255
Goalw [znegative_def, int_of_def]  "~ znegative($# n)";
paulson@5561
   256
by Safe_tac;
paulson@5561
   257
by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
paulson@5561
   258
by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
paulson@5561
   259
by (force_tac (claset(),
paulson@9548
   260
	       simpset() addsimps [add_le_self2 RS le_imp_not_lt,
paulson@9548
   261
				   natify_succ]) 1);
paulson@5561
   262
qed "not_znegative_int_of";
paulson@5561
   263
paulson@5561
   264
Addsimps [not_znegative_int_of];
paulson@5561
   265
AddSEs   [not_znegative_int_of RS notE];
paulson@5561
   266
paulson@9548
   267
Goalw [znegative_def, int_of_def] "znegative($- $# succ(n))";
paulson@9548
   268
by (asm_simp_tac (simpset() addsimps [zminus, natify_succ]) 1);
paulson@5561
   269
by (blast_tac (claset() addIs [nat_0_le]) 1);
paulson@5561
   270
qed "znegative_zminus_int_of";
paulson@5561
   271
paulson@5561
   272
Addsimps [znegative_zminus_int_of];
paulson@5561
   273
paulson@9548
   274
Goalw [znegative_def, int_of_def] "~ znegative($- $# n) ==> natify(n)=0";
paulson@5561
   275
by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
paulson@9496
   276
by (dres_inst_tac [("x","0")] spec 1);
paulson@9496
   277
by (auto_tac(claset(), 
paulson@9496
   278
             simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff RS iff_sym]));
paulson@5561
   279
qed "not_znegative_imp_zero";
paulson@5561
   280
paulson@5561
   281
(**** zmagnitude: magnitide of an integer, as a natural number ****)
paulson@5561
   282
paulson@9496
   283
Goalw [zmagnitude_def] "zmagnitude($# n) = natify(n)";
paulson@9496
   284
by (auto_tac (claset(), simpset() addsimps [int_of_eq]));  
paulson@5561
   285
qed "zmagnitude_int_of";
paulson@5561
   286
paulson@9496
   287
Goal "natify(x)=n ==> $#x = $# n";
paulson@9496
   288
by (dtac sym 1);
paulson@9496
   289
by (asm_simp_tac (simpset() addsimps [int_of_eq]) 1);
paulson@9496
   290
qed "natify_int_of_eq";
paulson@9496
   291
paulson@9548
   292
Goalw [zmagnitude_def] "zmagnitude($- $# n) = natify(n)";
paulson@9496
   293
by (rtac the_equality 1);
paulson@9496
   294
by (auto_tac((claset() addSDs [not_znegative_imp_zero, natify_int_of_eq], 
paulson@9496
   295
              simpset())
paulson@9496
   296
             delIffs [int_of_eq]));
paulson@9496
   297
by Auto_tac;  
paulson@5561
   298
qed "zmagnitude_zminus_int_of";
paulson@5561
   299
paulson@5561
   300
Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
paulson@5561
   301
paulson@5561
   302
Goalw [zmagnitude_def] "zmagnitude(z) : nat";
paulson@6153
   303
by (rtac theI2 1);
paulson@5561
   304
by Auto_tac;
paulson@5561
   305
qed "zmagnitude_type";
paulson@9570
   306
AddIffs [zmagnitude_type];
paulson@6153
   307
AddTCs [zmagnitude_type];
paulson@5561
   308
paulson@5561
   309
Goalw [int_def, znegative_def, int_of_def]
paulson@5561
   310
     "[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n"; 
paulson@5561
   311
by (auto_tac(claset() , simpset() addsimps [image_singleton_iff]));
paulson@5561
   312
by (rename_tac "i j" 1);
paulson@5561
   313
by (dres_inst_tac [("x", "i")] spec 1);
paulson@5561
   314
by (dres_inst_tac [("x", "j")] spec 1);
paulson@6153
   315
by (rtac bexI 1);
paulson@6153
   316
by (rtac (add_diff_inverse2 RS sym) 1);
paulson@5561
   317
by Auto_tac;
paulson@8201
   318
by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le]) 1);
paulson@5561
   319
qed "not_zneg_int_of";
paulson@5561
   320
paulson@5561
   321
Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
paulson@6153
   322
by (dtac not_zneg_int_of 1);
paulson@5561
   323
by Auto_tac;
paulson@5561
   324
qed "not_zneg_mag"; 
paulson@5561
   325
paulson@5561
   326
Addsimps [not_zneg_mag];
paulson@5561
   327
paulson@5561
   328
Goalw [int_def, znegative_def, int_of_def]
paulson@9576
   329
     "[| znegative(z); z: int |] ==> EX n:nat. z = $- ($# succ(n))"; 
paulson@9548
   330
by (auto_tac(claset() addSDs [less_imp_succ_add], 
paulson@5561
   331
	     simpset() addsimps [zminus, image_singleton_iff]));
paulson@5561
   332
qed "zneg_int_of";
paulson@5561
   333
paulson@9576
   334
Goal "[| znegative(z); z: int |] ==> $# (zmagnitude(z)) = $- z"; 
paulson@6153
   335
by (dtac zneg_int_of 1);
paulson@5561
   336
by Auto_tac;
paulson@5561
   337
qed "zneg_mag"; 
paulson@5561
   338
paulson@5561
   339
Addsimps [zneg_mag];
paulson@5561
   340
paulson@9570
   341
Goal "z : int ==> EX n: nat. z = $# n | z = $- ($# succ(n))"; 
paulson@9570
   342
by (case_tac "znegative(z)" 1);
paulson@9570
   343
by (blast_tac (claset() addDs [not_zneg_mag, sym]) 2);
paulson@9570
   344
by (blast_tac (claset() addDs [zneg_int_of]) 1);
paulson@9570
   345
qed "int_cases"; 
paulson@9570
   346
paulson@5561
   347
paulson@5561
   348
(**** zadd: addition on int ****)
paulson@5561
   349
paulson@5561
   350
(** Congruence property for addition **)
paulson@5561
   351
paulson@5561
   352
Goalw [congruent2_def]
paulson@5561
   353
    "congruent2(intrel, %z1 z2.                      \
paulson@5561
   354
\         let <x1,y1>=z1; <x2,y2>=z2                 \
paulson@5561
   355
\                           in intrel``{<x1#+x2, y1#+y2>})";
paulson@5561
   356
(*Proof via congruent2_commuteI seems longer*)
paulson@5561
   357
by Safe_tac;
paulson@5561
   358
by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
paulson@5561
   359
(*The rest should be trivial, but rearranging terms is hard;
paulson@5561
   360
  add_ac does not help rewriting with the assumptions.*)
paulson@5561
   361
by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
paulson@9491
   362
by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 1);
paulson@5561
   363
by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
paulson@5561
   364
qed "zadd_congruent2";
paulson@5561
   365
paulson@5561
   366
(*Resolve th against the corresponding facts for zadd*)
paulson@5561
   367
val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
paulson@5561
   368
paulson@9496
   369
Goalw [int_def,raw_zadd_def] "[| z: int;  w: int |] ==> raw_zadd(z,w) : int";
paulson@5561
   370
by (rtac (zadd_ize UN_equiv_class_type2) 1);
paulson@5561
   371
by (simp_tac (simpset() addsimps [Let_def]) 3);
paulson@9496
   372
by (REPEAT (assume_tac 1));
paulson@9496
   373
qed "raw_zadd_type";
paulson@5561
   374
paulson@9496
   375
Goal "z $+ w : int";
paulson@9496
   376
by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type]) 1);
paulson@9496
   377
qed "zadd_type";
paulson@9496
   378
AddIffs [zadd_type];  AddTCs [zadd_type];
paulson@9496
   379
paulson@9496
   380
Goalw [raw_zadd_def]
paulson@9496
   381
  "[| x1: nat; y1: nat;  x2: nat; y2: nat |]              \
paulson@9496
   382
\  ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) =  \
paulson@9496
   383
\      intrel `` {<x1#+x2, y1#+y2>}";
paulson@5561
   384
by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
paulson@5561
   385
by (simp_tac (simpset() addsimps [Let_def]) 1);
paulson@9496
   386
qed "raw_zadd";
paulson@9496
   387
paulson@9496
   388
Goalw [zadd_def]
paulson@9496
   389
  "[| x1: nat; y1: nat;  x2: nat; y2: nat |]         \
paulson@9496
   390
\  ==> (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =  \
paulson@9496
   391
\      intrel `` {<x1#+x2, y1#+y2>}";
paulson@9496
   392
by (asm_simp_tac (simpset() addsimps [raw_zadd, image_intrel_int]) 1);
paulson@5561
   393
qed "zadd";
paulson@5561
   394
paulson@9496
   395
Goalw [int_def,int_of_def] "z : int ==> raw_zadd ($#0,z) = z";
paulson@9496
   396
by (auto_tac (claset(), simpset() addsimps [raw_zadd]));  
paulson@9548
   397
qed "raw_zadd_int0";
paulson@9496
   398
paulson@9496
   399
Goal "$#0 $+ z = intify(z)";
paulson@9548
   400
by (asm_simp_tac (simpset() addsimps [zadd_def, raw_zadd_int0]) 1);
paulson@9548
   401
qed "zadd_int0_intify";
paulson@9548
   402
Addsimps [zadd_int0_intify];
paulson@9496
   403
paulson@9496
   404
Goal "z: int ==> $#0 $+ z = z";
paulson@9496
   405
by (Asm_simp_tac 1);
paulson@9548
   406
qed "zadd_int0";
paulson@5561
   407
paulson@9496
   408
Goalw [int_def]
paulson@9548
   409
     "[| z: int;  w: int |] ==> $- raw_zadd(z,w) = raw_zadd($- z, $- w)";
paulson@9496
   410
by (auto_tac (claset(), simpset() addsimps [zminus,raw_zadd]));  
paulson@9496
   411
qed "raw_zminus_zadd_distrib";
paulson@9496
   412
paulson@9548
   413
Goal "$- (z $+ w) = $- z $+ $- w";
paulson@9496
   414
by (simp_tac (simpset() addsimps [zadd_def, raw_zminus_zadd_distrib]) 1);
paulson@5561
   415
qed "zminus_zadd_distrib";
paulson@5561
   416
paulson@9548
   417
Addsimps [zminus_zadd_distrib];
paulson@9548
   418
paulson@9496
   419
Goalw [int_def] "[| z: int;  w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)";
paulson@9496
   420
by (auto_tac (claset(), simpset() addsimps raw_zadd::add_ac));  
paulson@9496
   421
qed "raw_zadd_commute";
paulson@9496
   422
paulson@9496
   423
Goal "z $+ w = w $+ z";
paulson@9496
   424
by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_commute]) 1);
paulson@5561
   425
qed "zadd_commute";
paulson@5561
   426
paulson@5561
   427
Goalw [int_def]
paulson@5561
   428
    "[| z1: int;  z2: int;  z3: int |]   \
paulson@9496
   429
\    ==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))";
paulson@9496
   430
by (auto_tac (claset(), simpset() addsimps [raw_zadd, add_assoc]));  
paulson@9496
   431
qed "raw_zadd_assoc";
paulson@9496
   432
paulson@9496
   433
Goal "(z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
paulson@9496
   434
by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type, raw_zadd_assoc]) 1);
paulson@5561
   435
qed "zadd_assoc";
paulson@5561
   436
paulson@5561
   437
(*For AC rewriting*)
paulson@9496
   438
Goal "z1$+(z2$+z3) = z2$+(z1$+z3)";
paulson@6153
   439
by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
paulson@6153
   440
by (asm_simp_tac (simpset() addsimps [zadd_commute]) 1);
paulson@5561
   441
qed "zadd_left_commute";
paulson@5561
   442
paulson@5561
   443
(*Integer addition is an AC operator*)
paulson@5561
   444
val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
paulson@5561
   445
paulson@9496
   446
Goalw [int_of_def] "$# (m #+ n) = ($#m) $+ ($#n)";
paulson@5561
   447
by (asm_simp_tac (simpset() addsimps [zadd]) 1);
paulson@5561
   448
qed "int_of_add";
paulson@5561
   449
paulson@9570
   450
Goal "$# succ(m) = $# 1 $+ ($# m)";
paulson@9570
   451
by (simp_tac (simpset() addsimps [int_of_add RS sym, natify_succ]) 1);
paulson@9570
   452
qed "int_succ_int_1";
paulson@9570
   453
paulson@9570
   454
Goalw [int_of_def,zdiff_def]
paulson@9570
   455
     "[| m: nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)";
paulson@9570
   456
by (ftac lt_nat_in_nat 1);
paulson@9570
   457
by (asm_simp_tac (simpset() addsimps [zadd,zminus,add_diff_inverse2]) 2);
paulson@9570
   458
by Auto_tac;  
paulson@9570
   459
qed "int_of_diff";
paulson@9570
   460
paulson@9548
   461
Goalw [int_def,int_of_def] "z : int ==> raw_zadd (z, $- z) = $#0";
paulson@9496
   462
by (auto_tac (claset(), simpset() addsimps [zminus, raw_zadd, add_commute]));  
paulson@9496
   463
qed "raw_zadd_zminus_inverse";
paulson@9496
   464
paulson@9548
   465
Goal "z $+ ($- z) = $#0";
paulson@9496
   466
by (simp_tac (simpset() addsimps [zadd_def]) 1);
paulson@9496
   467
by (stac (zminus_intify RS sym) 1);
paulson@9496
   468
by (rtac (intify_in_int RS raw_zadd_zminus_inverse) 1); 
paulson@5561
   469
qed "zadd_zminus_inverse";
paulson@5561
   470
paulson@9548
   471
Goal "($- z) $+ z = $#0";
paulson@9496
   472
by (simp_tac (simpset() addsimps [zadd_commute, zadd_zminus_inverse]) 1);
paulson@5561
   473
qed "zadd_zminus_inverse2";
paulson@5561
   474
paulson@9496
   475
Goal "z $+ $#0 = intify(z)";
paulson@9548
   476
by (rtac ([zadd_commute, zadd_int0_intify] MRS trans) 1);
paulson@9548
   477
qed "zadd_int0_right_intify";
paulson@9548
   478
Addsimps [zadd_int0_right_intify];
paulson@9496
   479
paulson@5561
   480
Goal "z:int ==> z $+ $#0 = z";
paulson@9496
   481
by (Asm_simp_tac 1);
paulson@9548
   482
qed "zadd_int0_right";
paulson@5561
   483
paulson@9496
   484
Addsimps [zadd_zminus_inverse, zadd_zminus_inverse2];
paulson@5561
   485
paulson@5561
   486
paulson@5561
   487
paulson@5561
   488
(**** zmult: multiplication on int ****)
paulson@5561
   489
paulson@5561
   490
(** Congruence property for multiplication **)
paulson@5561
   491
paulson@5561
   492
Goal "congruent2(intrel, %p1 p2.                 \
paulson@5561
   493
\               split(%x1 y1. split(%x2 y2.     \
paulson@5561
   494
\                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
paulson@5561
   495
by (rtac (equiv_intrel RS congruent2_commuteI) 1);
paulson@9548
   496
by Auto_tac;
paulson@5561
   497
(*Proof that zmult is congruent in one argument*)
paulson@9548
   498
by (rename_tac "x y" 1);
paulson@9548
   499
by (forw_inst_tac [("t", "%u. x#*u")] (sym RS subst_context) 1);
paulson@9548
   500
by (dres_inst_tac [("t", "%u. y#*u")] subst_context 1);
paulson@9548
   501
by (REPEAT (etac add_left_cancel 1));
paulson@9548
   502
by (asm_simp_tac (simpset() addsimps [add_mult_distrib_left]) 1);
paulson@9548
   503
by Auto_tac;
paulson@5561
   504
qed "zmult_congruent2";
paulson@5561
   505
paulson@5561
   506
paulson@5561
   507
(*Resolve th against the corresponding facts for zmult*)
paulson@5561
   508
val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
paulson@5561
   509
paulson@9496
   510
Goalw [int_def,raw_zmult_def] "[| z: int;  w: int |] ==> raw_zmult(z,w) : int";
paulson@5561
   511
by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
paulson@5561
   512
                      split_type, add_type, mult_type, 
paulson@5561
   513
                      quotientI, SigmaI] 1));
paulson@9496
   514
qed "raw_zmult_type";
paulson@9496
   515
paulson@9496
   516
Goal "z $* w : int";
paulson@9496
   517
by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type]) 1);
paulson@5561
   518
qed "zmult_type";
paulson@9496
   519
AddIffs [zmult_type];  AddTCs [zmult_type];
paulson@9496
   520
paulson@9496
   521
Goalw [raw_zmult_def]
paulson@9496
   522
     "[| x1: nat; y1: nat;  x2: nat; y2: nat |]    \
paulson@9496
   523
\     ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) =     \
paulson@9496
   524
\         intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
paulson@9496
   525
by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
paulson@9496
   526
qed "raw_zmult";
paulson@5561
   527
paulson@5561
   528
Goalw [zmult_def]
paulson@9496
   529
     "[| x1: nat; y1: nat;  x2: nat; y2: nat |]    \
paulson@9496
   530
\     ==> (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
paulson@9496
   531
\         intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
paulson@9496
   532
by (asm_simp_tac (simpset() addsimps [raw_zmult, image_intrel_int]) 1);
paulson@5561
   533
qed "zmult";
paulson@5561
   534
paulson@9496
   535
Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#0,z) = $#0";
paulson@9496
   536
by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
paulson@9548
   537
qed "raw_zmult_int0";
paulson@9496
   538
paulson@9496
   539
Goal "$#0 $* z = $#0";
paulson@9548
   540
by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_int0]) 1);
paulson@9548
   541
qed "zmult_int0";
paulson@9548
   542
Addsimps [zmult_int0];
paulson@5561
   543
paulson@9496
   544
Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#1,z) = z";
paulson@9496
   545
by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
paulson@9548
   546
qed "raw_zmult_int1";
paulson@9496
   547
paulson@9496
   548
Goal "$#1 $* z = intify(z)";
paulson@9548
   549
by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_int1]) 1);
paulson@9548
   550
qed "zmult_int1_intify";
paulson@9548
   551
Addsimps [zmult_int1_intify];
paulson@9496
   552
paulson@9496
   553
Goal "z : int ==> $#1 $* z = z";
paulson@9496
   554
by (Asm_simp_tac 1);
paulson@9548
   555
qed "zmult_int1";
paulson@5561
   556
paulson@9496
   557
Goalw [int_def] "[| z: int;  w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)";
paulson@9496
   558
by (auto_tac (claset(), simpset() addsimps [raw_zmult] @ add_ac @ mult_ac));  
paulson@9496
   559
qed "raw_zmult_commute";
paulson@5561
   560
paulson@9496
   561
Goal "z $* w = w $* z";
paulson@9496
   562
by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_commute]) 1);
paulson@5561
   563
qed "zmult_commute";
paulson@5561
   564
paulson@5561
   565
Goalw [int_def]
paulson@9548
   566
     "[| z: int;  w: int |] ==> raw_zmult($- z, w) = $- raw_zmult(z, w)";
paulson@9496
   567
by (auto_tac (claset(), simpset() addsimps [zminus, raw_zmult] @ add_ac));  
paulson@9496
   568
qed "raw_zmult_zminus";
paulson@9496
   569
paulson@9548
   570
Goal "($- z) $* w = $- (z $* w)";
paulson@9496
   571
by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_zminus]) 1);
paulson@9496
   572
by (stac (zminus_intify RS sym) 1 THEN rtac raw_zmult_zminus 1); 
paulson@9496
   573
by Auto_tac;  
paulson@9496
   574
qed "zmult_zminus";
paulson@9496
   575
Addsimps [zmult_zminus];
paulson@9496
   576
paulson@9570
   577
Goal "w $* ($- z) = $- (w $* z)";
paulson@9570
   578
by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute]) 1);
paulson@9570
   579
qed "zmult_zminus_right";
paulson@9570
   580
Addsimps [zmult_zminus_right];
paulson@9496
   581
paulson@9496
   582
Goalw [int_def]
paulson@9496
   583
    "[| z1: int;  z2: int;  z3: int |]   \
paulson@9496
   584
\    ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))";
paulson@9496
   585
by (auto_tac (claset(), 
paulson@9496
   586
  simpset() addsimps [raw_zmult, add_mult_distrib_left] @ add_ac @ mult_ac));  
paulson@9496
   587
qed "raw_zmult_assoc";
paulson@9496
   588
paulson@9496
   589
Goal "(z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
paulson@9496
   590
by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type, 
paulson@9496
   591
                                  raw_zmult_assoc]) 1);
paulson@5561
   592
qed "zmult_assoc";
paulson@5561
   593
paulson@5561
   594
(*For AC rewriting*)
paulson@9496
   595
Goal "z1$*(z2$*z3) = z2$*(z1$*z3)";
paulson@6153
   596
by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
paulson@6153
   597
by (asm_simp_tac (simpset() addsimps [zmult_commute]) 1);
paulson@5561
   598
qed "zmult_left_commute";
paulson@5561
   599
paulson@5561
   600
(*Integer multiplication is an AC operator*)
paulson@5561
   601
val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
paulson@5561
   602
paulson@5561
   603
Goalw [int_def]
paulson@9496
   604
    "[| z1: int;  z2: int;  w: int |]  \
paulson@9496
   605
\    ==> raw_zmult(raw_zadd(z1,z2), w) = \
paulson@9496
   606
\        raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))";
paulson@9496
   607
by (auto_tac (claset(), 
paulson@9496
   608
              simpset() addsimps [raw_zadd, raw_zmult, add_mult_distrib_left] @ 
paulson@9496
   609
                                 add_ac @ mult_ac));  
paulson@9496
   610
qed "raw_zadd_zmult_distrib";
paulson@9496
   611
paulson@9496
   612
Goal "(z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
paulson@9496
   613
by (simp_tac (simpset() addsimps [zmult_def, zadd_def, raw_zadd_type, 
paulson@9496
   614
     	                          raw_zmult_type, raw_zadd_zmult_distrib]) 1);
paulson@5561
   615
qed "zadd_zmult_distrib";
paulson@5561
   616
paulson@9496
   617
Goal "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)";
paulson@9496
   618
by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute,
paulson@9496
   619
                                  zadd_zmult_distrib]) 1);
paulson@9576
   620
qed "zadd_zmult_distrib2";
paulson@9496
   621
paulson@5561
   622
val int_typechecks =
paulson@5561
   623
    [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
paulson@5561
   624
paulson@5561
   625
paulson@9548
   626
(*** Subtraction laws ***)
paulson@9548
   627
paulson@9570
   628
Goal "z $- w : int";
paulson@9570
   629
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
paulson@9570
   630
qed "zdiff_type";
paulson@9570
   631
AddIffs [zdiff_type];  AddTCs [zdiff_type];
paulson@9570
   632
paulson@9570
   633
Goal "$- (z $- y) = y $- z";
paulson@9570
   634
by (simp_tac (simpset() addsimps [zdiff_def, zadd_commute])1);
paulson@9570
   635
qed "zminus_zdiff_eq";
paulson@9570
   636
Addsimps [zminus_zdiff_eq];
paulson@9570
   637
paulson@9570
   638
Goal "$- (z $- y) = y $- z";
paulson@9570
   639
by (simp_tac (simpset() addsimps [zdiff_def, zadd_commute])1);
paulson@9570
   640
qed "zminus_zdiff_eq";
paulson@9570
   641
Addsimps [zminus_zdiff_eq];
paulson@9548
   642
paulson@9548
   643
Goalw [zdiff_def] "(z1 $- z2) $* w = (z1 $* w) $- (z2 $* w)";
paulson@9548
   644
by (stac zadd_zmult_distrib 1);
paulson@9548
   645
by (simp_tac (simpset() addsimps [zmult_zminus]) 1);
paulson@9548
   646
qed "zdiff_zmult_distrib";
paulson@9548
   647
paulson@9548
   648
val zmult_commute'= inst "z" "w" zmult_commute;
paulson@9548
   649
paulson@9548
   650
Goal "w $* (z1 $- z2) = (w $* z1) $- (w $* z2)";
paulson@9548
   651
by (simp_tac (simpset() addsimps [zmult_commute',zdiff_zmult_distrib]) 1);
paulson@9548
   652
qed "zdiff_zmult_distrib2";
paulson@9548
   653
paulson@9548
   654
Goal "x $+ (y $- z) = (x $+ y) $- z";
paulson@9548
   655
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
paulson@9548
   656
qed "zadd_zdiff_eq";
paulson@9548
   657
paulson@9548
   658
Goal "(x $- y) $+ z = (x $+ z) $- y";
paulson@9548
   659
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
paulson@9548
   660
qed "zdiff_zadd_eq";
paulson@9548
   661
paulson@9548
   662
paulson@9548
   663
(*** "Less Than" ***)
paulson@9548
   664
paulson@9548
   665
(*"Less than" is a linear ordering*)
paulson@9548
   666
Goalw [int_def, zless_def, znegative_def, zdiff_def] 
paulson@9548
   667
     "[| z: int; w: int |] ==> z$<w | z=w | w$<z"; 
paulson@9548
   668
by Auto_tac;  
paulson@9548
   669
by (asm_full_simp_tac
paulson@9548
   670
    (simpset() addsimps [zadd, zminus, image_iff, Bex_def]) 1);
paulson@9548
   671
by (res_inst_tac [("i", "xb#+ya"), ("j", "xc #+ y")] Ord_linear_lt 1);
paulson@9548
   672
by (ALLGOALS (force_tac (claset() addSDs [spec], 
paulson@9548
   673
                         simpset() addsimps add_ac)));
paulson@9548
   674
qed "zless_linear_lemma";
paulson@9548
   675
paulson@9548
   676
Goal "z$<w | intify(z)=intify(w) | w$<z"; 
paulson@9548
   677
by (cut_inst_tac [("z"," intify(z)"),("w"," intify(w)")] zless_linear_lemma 1);
paulson@9548
   678
by Auto_tac;  
paulson@9548
   679
qed "zless_linear";
paulson@9548
   680
paulson@9548
   681
Goal "~ (z$<z)";
paulson@9548
   682
by (auto_tac (claset(), 
paulson@9576
   683
              simpset() addsimps  [zless_def, znegative_def, int_of_def,
paulson@9576
   684
                                   zdiff_def]));  
paulson@9548
   685
by (rotate_tac 2 1);
paulson@9548
   686
by Auto_tac;  
paulson@9548
   687
qed "zless_not_refl";
paulson@9548
   688
AddIffs [zless_not_refl];
paulson@9548
   689
paulson@9576
   690
Goal "[| x: int; y: int |] ==> (x ~= y) <-> (x $< y | y $< x)";
paulson@9576
   691
by (cut_inst_tac [("z","x"),("w","y")] zless_linear 1);
paulson@9576
   692
by Auto_tac;  
paulson@9576
   693
qed "neq_iff_zless";
paulson@9576
   694
paulson@9576
   695
Goal "w $< z ==> intify(w) ~= intify(z)";
paulson@9576
   696
by Auto_tac;  
paulson@9576
   697
by (subgoal_tac "~ (intify(w) $< intify(z))" 1);
paulson@9576
   698
by (etac ssubst 2);
paulson@9576
   699
by (Full_simp_tac 1);
paulson@9576
   700
by Auto_tac;  
paulson@9576
   701
qed "zless_imp_intify_neq";
paulson@9576
   702
paulson@9548
   703
(*This lemma allows direct proofs of other <-properties*)
paulson@9548
   704
Goalw [zless_def, znegative_def, zdiff_def, int_def] 
paulson@9548
   705
    "[| w $< z; w: int; z: int |] ==> (EX n. z = w $+ $#(succ(n)))";
paulson@9548
   706
by (auto_tac (claset() addSDs [less_imp_succ_add], 
paulson@9548
   707
              simpset() addsimps [zadd, zminus, int_of_def]));  
paulson@9548
   708
by (res_inst_tac [("x","k")] exI 1);
paulson@9548
   709
by (etac add_left_cancel 1);
paulson@9548
   710
by Auto_tac;  
paulson@9576
   711
val lemma = result();
paulson@9548
   712
paulson@9548
   713
Goal "w $< z ==> (EX n. w $+ $#(succ(n)) = intify(z))";
paulson@9548
   714
by (subgoal_tac "intify(w) $< intify(z)" 1);
paulson@9576
   715
by (dres_inst_tac [("w","intify(w)")] lemma 1);
paulson@9548
   716
by Auto_tac;  
paulson@9548
   717
qed "zless_imp_succ_zadd";
paulson@9548
   718
paulson@9548
   719
Goalw [zless_def, znegative_def, zdiff_def, int_def] 
paulson@9548
   720
    "w : int ==> w $< w $+ $# succ(n)";
paulson@9548
   721
by (auto_tac (claset(), 
paulson@9548
   722
              simpset() addsimps [zadd, zminus, int_of_def, image_iff]));  
paulson@9548
   723
by (res_inst_tac [("x","0")] exI 1);
paulson@9548
   724
by Auto_tac;  
paulson@9576
   725
val lemma = result();
paulson@9548
   726
paulson@9548
   727
Goal "w $< w $+ $# succ(n)";
paulson@9576
   728
by (cut_facts_tac [intify_in_int RS lemma] 1);
paulson@9548
   729
by Auto_tac;  
paulson@9548
   730
qed "zless_succ_zadd";
paulson@9548
   731
paulson@9548
   732
Goal "w $< z <-> (EX n. w $+ $#(succ(n)) = intify(z))";
paulson@9548
   733
by (rtac iffI 1);
paulson@9548
   734
by (etac zless_imp_succ_zadd 1);
paulson@9548
   735
by Auto_tac;  
paulson@9548
   736
by (cut_inst_tac [("w","w"),("n","n")] zless_succ_zadd 1);
paulson@9548
   737
by Auto_tac;  
paulson@9548
   738
qed "zless_iff_succ_zadd";
paulson@9548
   739
paulson@9548
   740
Goalw [zless_def, znegative_def, zdiff_def, int_def] 
paulson@9548
   741
    "[| x $< y; y $< z; x: int; y : int; z: int |] ==> x $< z"; 
paulson@9548
   742
by (auto_tac (claset(), 
paulson@9548
   743
              simpset() addsimps [zadd, zminus, int_of_def, image_iff]));
paulson@9548
   744
by (rename_tac "x1 x2 y1 y2" 1);
paulson@9548
   745
by (res_inst_tac [("x","x1#+x2")] exI 1);  
paulson@9548
   746
by (res_inst_tac [("x","y1#+y2")] exI 1);  
paulson@9548
   747
by (auto_tac (claset(), simpset() addsimps [add_lt_mono]));  
paulson@9548
   748
by (rtac sym 1);
paulson@9548
   749
by (REPEAT (etac add_left_cancel 1));
paulson@9548
   750
by Auto_tac;  
paulson@9548
   751
qed "zless_trans_lemma";
paulson@9548
   752
paulson@9548
   753
Goal "[| x $< y; y $< z |] ==> x $< z"; 
paulson@9548
   754
by (subgoal_tac "intify(x) $< intify(z)" 1);
paulson@9548
   755
by (res_inst_tac [("y", "intify(y)")] zless_trans_lemma 2);
paulson@9548
   756
by Auto_tac;  
paulson@9548
   757
qed "zless_trans";
paulson@9548
   758
paulson@9576
   759
Goal "z $< w ==> ~ (w $< z)";
paulson@9576
   760
by (blast_tac (claset() addDs [zless_trans]) 1);
paulson@9576
   761
qed "zless_not_sym";
paulson@9576
   762
paulson@9576
   763
(* [| z $< w; ~ P ==> w $< z |] ==> P *)
paulson@9576
   764
bind_thm ("zless_asym", zless_not_sym RS swap);
paulson@9576
   765
paulson@9576
   766
paulson@9570
   767
(*** "Less Than or Equals", $<= ***)
paulson@9548
   768
paulson@9548
   769
Goalw [zle_def] "z $<= z";
paulson@9548
   770
by Auto_tac;  
paulson@9548
   771
qed "zle_refl";
paulson@9548
   772
paulson@9570
   773
Goalw [zle_def] "[| x $<= y; y $<= x |] ==> intify(x) = intify(y)";
paulson@9570
   774
by Auto_tac;  
paulson@9548
   775
by (blast_tac (claset() addDs [zless_trans]) 1);
paulson@9548
   776
qed "zle_anti_sym";
paulson@9548
   777
paulson@9570
   778
Goalw [zle_def] "[| x: int; y: int; z: int; x $<= y; y $<= z |] ==> x $<= z";
paulson@9570
   779
by Auto_tac;  
paulson@9548
   780
by (blast_tac (claset() addIs [zless_trans]) 1);
paulson@9570
   781
val lemma = result();
paulson@9570
   782
paulson@9570
   783
Goal "[| x $<= y; y $<= z |] ==> x $<= z";
paulson@9570
   784
by (subgoal_tac "intify(x) $<= intify(z)" 1);
paulson@9570
   785
by (res_inst_tac [("y", "intify(y)")] lemma 2);
paulson@9570
   786
by Auto_tac;  
paulson@9548
   787
qed "zle_trans";
paulson@9548
   788
paulson@9570
   789
Goal "[| i $<= j; j $< k |] ==> i $< k";
paulson@9570
   790
by (auto_tac (claset(), simpset() addsimps [zle_def]));  
paulson@9570
   791
by (blast_tac (claset() addIs [zless_trans]) 1);
paulson@9570
   792
by (asm_full_simp_tac (simpset() addsimps [zless_def, zdiff_def, zadd_def]) 1);
paulson@9570
   793
qed "zle_zless_trans";
paulson@9548
   794
paulson@9570
   795
Goal "[| i $< j; j $<= k |] ==> i $< k";
paulson@9570
   796
by (auto_tac (claset(), simpset() addsimps [zle_def]));  
paulson@9570
   797
by (blast_tac (claset() addIs [zless_trans]) 1);
paulson@9570
   798
by (asm_full_simp_tac
paulson@9570
   799
    (simpset() addsimps [zless_def, zdiff_def, zminus_def]) 1);
paulson@9570
   800
qed "zless_zle_trans";
paulson@9570
   801
paulson@9570
   802
Goal "~ (z $< w) <-> (w $<= z)";
paulson@9570
   803
by (cut_inst_tac [("z","z"),("w","w")] zless_linear 1);
paulson@9570
   804
by (auto_tac (claset() addDs [zless_trans], simpset() addsimps [zle_def]));  
paulson@9576
   805
by (auto_tac (claset() addSDs [zless_imp_intify_neq],  simpset()));
paulson@9570
   806
qed "not_zless_iff_zle";
paulson@9570
   807
paulson@9570
   808
Goal "~ (z $<= w) <-> (w $< z)";
paulson@9570
   809
by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
paulson@9570
   810
qed "not_zle_iff_zless";
paulson@9570
   811
paulson@9570
   812
paulson@9570
   813
(*** More subtraction laws (for zcompare_rls) ***)
paulson@9548
   814
paulson@9548
   815
Goal "(x $- y) $- z = x $- (y $+ z)";
paulson@9548
   816
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
paulson@9548
   817
qed "zdiff_zdiff_eq";
paulson@9548
   818
paulson@9548
   819
Goal "x $- (y $- z) = (x $+ z) $- y";
paulson@9548
   820
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
paulson@9548
   821
qed "zdiff_zdiff_eq2";
paulson@9548
   822
paulson@9548
   823
Goalw [zless_def, zdiff_def] "(x$-y $< z) <-> (x $< z $+ y)";
paulson@9548
   824
by (simp_tac (simpset() addsimps zadd_ac) 1);
paulson@9548
   825
qed "zdiff_zless_iff";
paulson@9548
   826
paulson@9548
   827
Goalw [zless_def, zdiff_def] "(x $< z$-y) <-> (x $+ y $< z)";
paulson@9548
   828
by (simp_tac (simpset() addsimps zadd_ac) 1);
paulson@9548
   829
qed "zless_zdiff_iff";
paulson@9548
   830
paulson@9548
   831
Goalw [zdiff_def] "[| x: int; z: int |] ==> (x$-y = z) <-> (x = z $+ y)";
paulson@9548
   832
by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
paulson@9548
   833
qed "zdiff_eq_iff";
paulson@9548
   834
paulson@9548
   835
Goalw [zdiff_def] "[| x: int; z: int |] ==> (x = z$-y) <-> (x $+ y = z)";
paulson@9548
   836
by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
paulson@9548
   837
qed "eq_zdiff_iff";
paulson@9548
   838
paulson@9548
   839
Goalw [zle_def] "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)";
paulson@9570
   840
by (auto_tac (claset(), simpset() addsimps [zdiff_eq_iff, zdiff_zless_iff]));  
paulson@9570
   841
val lemma = result();
paulson@9570
   842
paulson@9570
   843
Goal "(x$-y $<= z) <-> (x $<= z $+ y)";
paulson@9570
   844
by (cut_facts_tac [[intify_in_int, intify_in_int] MRS lemma] 1);
paulson@9570
   845
by (Asm_full_simp_tac 1);
paulson@9548
   846
qed "zdiff_zle_iff";
paulson@9548
   847
paulson@9570
   848
Goalw [zle_def] "[| x: int; z: int |] ==>(x $<= z$-y) <-> (x $+ y $<= z)";
paulson@9570
   849
by (auto_tac (claset(), simpset() addsimps [zdiff_eq_iff, zless_zdiff_iff]));  
paulson@9570
   850
by (auto_tac (claset(), simpset() addsimps [zdiff_def, zadd_assoc]));  
paulson@9570
   851
val lemma = result();
paulson@9570
   852
paulson@9570
   853
Goal "(x $<= z$-y) <-> (x $+ y $<= z)";
paulson@9570
   854
by (cut_facts_tac [[intify_in_int, intify_in_int] MRS lemma] 1);
paulson@9570
   855
by (Asm_full_simp_tac 1);
paulson@9548
   856
qed "zle_zdiff_iff";
paulson@9570
   857
paulson@9570
   858
(*This list of rewrites simplifies (in)equalities by bringing subtractions
paulson@9570
   859
  to the top and then moving negative terms to the other side.  
paulson@9570
   860
  Use with zadd_ac*)
paulson@9570
   861
bind_thms ("zcompare_rls",
paulson@9570
   862
    [symmetric zdiff_def,
paulson@9570
   863
     zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2, 
paulson@9570
   864
     zdiff_zless_iff, zless_zdiff_iff, zdiff_zle_iff, zle_zdiff_iff, 
paulson@9570
   865
     zdiff_eq_iff, eq_zdiff_iff]);
paulson@9548
   866
paulson@9548
   867
paulson@9548
   868
(*** Monotonicity/cancellation results that could allow instantiation
paulson@9548
   869
     of the CancelNumerals simprocs ***)
paulson@9548
   870
paulson@9548
   871
Goal "[| w: int; w': int |] ==> (z $+ w' = z $+ w) <-> (w' = w)";
paulson@9548
   872
by Safe_tac;
paulson@9548
   873
by (dres_inst_tac [("t", "%x. x $+ ($-z)")] subst_context 1);
paulson@9548
   874
by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
paulson@9548
   875
qed "zadd_left_cancel";
paulson@9548
   876
paulson@9548
   877
Goal "(z $+ w' = z $+ w) <-> intify(w') = intify(w)";
paulson@9548
   878
by (rtac iff_trans 1);
paulson@9548
   879
by (rtac zadd_left_cancel 2);
paulson@9548
   880
by Auto_tac;  
paulson@9548
   881
qed "zadd_left_cancel_intify";
paulson@9548
   882
paulson@9548
   883
Addsimps [zadd_left_cancel_intify];
paulson@9548
   884
paulson@9548
   885
Goal "[| w: int; w': int |] ==> (w' $+ z = w $+ z) <-> (w' = w)";
paulson@9548
   886
by Safe_tac;
paulson@9548
   887
by (dres_inst_tac [("t", "%x. x $+ ($-z)")] subst_context 1);
paulson@9548
   888
by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
paulson@9548
   889
qed "zadd_right_cancel";
paulson@9548
   890
paulson@9548
   891
Goal "(w' $+ z = w $+ z) <-> intify(w') = intify(w)";
paulson@9548
   892
by (rtac iff_trans 1);
paulson@9548
   893
by (rtac zadd_right_cancel 2);
paulson@9548
   894
by Auto_tac;  
paulson@9548
   895
qed "zadd_right_cancel_intify";
paulson@9548
   896
paulson@9548
   897
Addsimps [zadd_right_cancel_intify];
paulson@9548
   898
paulson@9548
   899
paulson@9548
   900
Goal "(w' $+ z $< w $+ z) <-> (w' $< w)";
paulson@9548
   901
by (simp_tac (simpset() addsimps [zdiff_zless_iff RS iff_sym]) 1);
paulson@9548
   902
by (simp_tac (simpset() addsimps [zdiff_def, zadd_assoc]) 1);
paulson@9548
   903
qed "zadd_right_cancel_zless";
paulson@9548
   904
paulson@9548
   905
Goal "(z $+ w' $< z $+ w) <-> (w' $< w)";
paulson@9548
   906
by (simp_tac (simpset() addsimps [inst "z" "z" zadd_commute,
paulson@9548
   907
                                  zadd_right_cancel_zless]) 1);
paulson@9548
   908
qed "zadd_left_cancel_zless";
paulson@9548
   909
paulson@9548
   910
Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
paulson@9548
   911
paulson@9548
   912
paulson@9570
   913
Goal "(w' $+ z $<= w $+ z) <-> w' $<= w";
paulson@9548
   914
by (simp_tac (simpset() addsimps [zle_def]) 1);
paulson@9548
   915
qed "zadd_right_cancel_zle";
paulson@9548
   916
paulson@9570
   917
Goal "(z $+ w' $<= z $+ w) <->  w' $<= w";
paulson@9548
   918
by (simp_tac (simpset() addsimps [inst "z" "z" zadd_commute,
paulson@9548
   919
                                  zadd_right_cancel_zle]) 1);
paulson@9548
   920
qed "zadd_left_cancel_zle";
paulson@9548
   921
paulson@9548
   922
Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
paulson@9548
   923
paulson@9570
   924
paulson@9576
   925
(*** Comparison laws ***)
paulson@9576
   926
paulson@9576
   927
Goal "($- x $< $- y) <-> (y $< x)";
paulson@9576
   928
by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
paulson@9576
   929
qed "zminus_zless_zminus"; 
paulson@9576
   930
Addsimps [zminus_zless_zminus];
paulson@9576
   931
paulson@9576
   932
Goal "($- x $<= $- y) <-> (y $<= x)";
paulson@9576
   933
by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
paulson@9576
   934
qed "zminus_zle_zminus"; 
paulson@9576
   935
Addsimps [zminus_zle_zminus];
paulson@9576
   936
paulson@9576
   937
paulson@9570
   938
(*** More inequality lemmas ***)
paulson@9570
   939
paulson@9570
   940
Goal "[| x: int;  y: int |] ==> (x = $- y) <-> (y = $- x)";
paulson@9570
   941
by Auto_tac;
paulson@9570
   942
qed "equation_zminus";
paulson@9570
   943
paulson@9570
   944
Goal "[| x: int;  y: int |] ==> ($- x = y) <-> ($- y = x)";
paulson@9570
   945
by Auto_tac;
paulson@9570
   946
qed "zminus_equation";
paulson@9576
   947
paulson@9576
   948
Goal "(intify(x) = $- y) <-> (intify(y) = $- x)";
paulson@9576
   949
by (cut_inst_tac [("x","intify(x)"), ("y","intify(y)")] equation_zminus 1);
paulson@9576
   950
by Auto_tac;
paulson@9576
   951
qed "equation_zminus_intify";
paulson@9576
   952
paulson@9576
   953
Goal "($- x = intify(y)) <-> ($- y = intify(x))";
paulson@9576
   954
by (cut_inst_tac [("x","intify(x)"), ("y","intify(y)")] zminus_equation 1);
paulson@9576
   955
by Auto_tac;
paulson@9576
   956
qed "zminus_equation_intify";
paulson@9576
   957
paulson@9576
   958
paulson@9576
   959
(** The next several equations are permutative: watch out! **)
paulson@9576
   960
paulson@9576
   961
Goal "(x $< $- y) <-> (y $< $- x)";
paulson@9576
   962
by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
paulson@9576
   963
qed "zless_zminus"; 
paulson@9576
   964
paulson@9576
   965
Goal "($- x $< y) <-> ($- y $< x)";
paulson@9576
   966
by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
paulson@9576
   967
qed "zminus_zless"; 
paulson@9576
   968
paulson@9576
   969
Goal "(x $<= $- y) <-> (y $<= $- x)";
paulson@9576
   970
by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym, 
paulson@9576
   971
                                  zminus_zless]) 1);
paulson@9576
   972
qed "zle_zminus"; 
paulson@9576
   973
paulson@9576
   974
Goal "($- x $<= y) <-> ($- y $<= x)";
paulson@9576
   975
by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym, 
paulson@9576
   976
                                  zless_zminus]) 1);
paulson@9576
   977
qed "zminus_zle";