src/ZF/Integ/Int.ML
author paulson
Wed Aug 02 16:07:32 2000 +0200 (2000-08-02)
changeset 9496 07e33cac5d9c
parent 9491 1a36151ee2fc
child 9548 15bee2731e43
permissions -rw-r--r--
coercion "intify" to remove type constraints from integer algebraic laws
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@5561
     9
"znegative(z) ==> $# zmagnitude(z) = $~ z"
paulson@5561
    10
"~ znegative(z) ==> $# zmagnitude(z) = z"
paulson@5561
    11
$< is a linear ordering
paulson@5561
    12
$+ and $* are monotonic wrt $<
paulson@5561
    13
*)
paulson@5561
    14
paulson@5561
    15
AddSEs [quotientE];
paulson@5561
    16
paulson@5561
    17
(*** Proving that intrel is an equivalence relation ***)
paulson@5561
    18
paulson@5561
    19
(** Natural deduction for intrel **)
paulson@5561
    20
paulson@5561
    21
Goalw [intrel_def]
paulson@5561
    22
    "<<x1,y1>,<x2,y2>>: intrel <-> \
paulson@5561
    23
\    x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1";
paulson@5561
    24
by (Fast_tac 1);
paulson@5561
    25
qed "intrel_iff";
paulson@5561
    26
paulson@5561
    27
Goalw [intrel_def]
paulson@9496
    28
    "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |]  \
paulson@9496
    29
\    ==> <<x1,y1>,<x2,y2>>: intrel";
paulson@5561
    30
by (fast_tac (claset() addIs prems) 1);
paulson@5561
    31
qed "intrelI";
paulson@5561
    32
paulson@5561
    33
(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
paulson@5561
    34
Goalw [intrel_def]
paulson@5561
    35
  "p: intrel --> (EX x1 y1 x2 y2. \
paulson@5561
    36
\                  p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \
paulson@5561
    37
\                  x1: nat & y1: nat & x2: nat & y2: nat)";
paulson@5561
    38
by (Fast_tac 1);
paulson@5561
    39
qed "intrelE_lemma";
paulson@5561
    40
paulson@5561
    41
val [major,minor] = goal thy
paulson@5561
    42
  "[| p: intrel;  \
paulson@5561
    43
\     !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1; \
paulson@5561
    44
\                       x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \
paulson@5561
    45
\  ==> Q";
paulson@5561
    46
by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
paulson@5561
    47
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
paulson@5561
    48
qed "intrelE";
paulson@5561
    49
paulson@5561
    50
AddSIs [intrelI];
paulson@5561
    51
AddSEs [intrelE];
paulson@5561
    52
paulson@9491
    53
val eqa::eqb::prems = goal Arith.thy 
paulson@9491
    54
    "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1";
paulson@9491
    55
by (res_inst_tac [("k","x2")] add_left_cancel 1);
paulson@9491
    56
by (rtac (add_left_commute RS trans) 1);
paulson@9491
    57
by Auto_tac;
paulson@9491
    58
by (stac eqb 1);
paulson@9491
    59
by (rtac (add_left_commute RS trans) 1);
paulson@9491
    60
by (ALLGOALS (asm_simp_tac (simpset() addsimps [eqa, add_left_commute])));
paulson@9491
    61
qed "int_trans_lemma";
paulson@9491
    62
paulson@5561
    63
Goalw [equiv_def, refl_def, sym_def, trans_def]
paulson@5561
    64
    "equiv(nat*nat, intrel)";
paulson@5561
    65
by (fast_tac (claset() addSEs [sym, int_trans_lemma]) 1);
paulson@5561
    66
qed "equiv_intrel";
paulson@5561
    67
paulson@5561
    68
paulson@9496
    69
Goalw [int_def] "[| m: nat; n: nat |] ==> intrel `` {<m,n>} : int";
paulson@9496
    70
by (blast_tac (claset() addIs [quotientI]) 1);
paulson@9496
    71
qed "image_intrel_int";
paulson@9496
    72
paulson@9496
    73
paulson@5561
    74
Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
paulson@5561
    75
	  add_0_right, add_succ_right];
paulson@5561
    76
Addcongs [conj_cong];
paulson@5561
    77
paulson@5561
    78
val eq_intrelD = equiv_intrel RSN (2,eq_equiv_class);
paulson@5561
    79
paulson@5561
    80
(** int_of: the injection from nat to int **)
paulson@5561
    81
paulson@9496
    82
Goalw [int_def,quotient_def,int_of_def]  "$#m : int";
paulson@6153
    83
by Auto_tac;
paulson@5561
    84
qed "int_of_type";
paulson@5561
    85
paulson@9496
    86
AddIffs [int_of_type];
paulson@9496
    87
AddTCs  [int_of_type];
paulson@9496
    88
paulson@5561
    89
paulson@9496
    90
Goalw [int_of_def] "($# m = $# n) <-> natify(m)=natify(n)"; 
paulson@9496
    91
by Auto_tac;  
paulson@9496
    92
qed "int_of_eq"; 
paulson@9496
    93
AddIffs [int_of_eq];
paulson@9496
    94
paulson@9496
    95
Goal "[| $#m = $#n;  m: nat;  n: nat |] ==> m=n";
paulson@9496
    96
by (dtac (int_of_eq RS iffD1) 1);
paulson@6153
    97
by Auto_tac;
paulson@5561
    98
qed "int_of_inject";
paulson@5561
    99
paulson@9496
   100
paulson@9496
   101
(** intify: coercion from anything to int **)
paulson@9496
   102
paulson@9496
   103
Goal "intify(x) : int";
paulson@9496
   104
by (simp_tac (simpset() addsimps [intify_def]) 1);
paulson@9496
   105
qed "intify_in_int";
paulson@9496
   106
AddIffs [intify_in_int];
paulson@9496
   107
AddTCs [intify_in_int];
paulson@9496
   108
paulson@9496
   109
Goal "n : int ==> intify(n) = n";
paulson@9496
   110
by (asm_simp_tac (simpset() addsimps [intify_def]) 1);
paulson@9496
   111
qed "intify_ident";
paulson@9496
   112
Addsimps [intify_ident];
paulson@9496
   113
paulson@9496
   114
paulson@9496
   115
(*** Collapsing rules: to remove intify from arithmetic expressions ***)
paulson@9496
   116
paulson@9496
   117
Goal "intify(intify(x)) = intify(x)";
paulson@9496
   118
by (Simp_tac 1);
paulson@9496
   119
qed "intify_idem";
paulson@9496
   120
Addsimps [intify_idem];
paulson@9496
   121
paulson@9496
   122
Goal "$# (natify(m)) = $# m";
paulson@9496
   123
by (simp_tac (simpset() addsimps [int_of_def]) 1);
paulson@9496
   124
qed "int_of_natify";
paulson@5561
   125
paulson@9496
   126
Goal "$~ (intify(m)) = $~ m";
paulson@9496
   127
by (simp_tac (simpset() addsimps [zminus_def]) 1);
paulson@9496
   128
qed "zminus_intify";
paulson@9496
   129
paulson@9496
   130
Addsimps [int_of_natify, zminus_intify];
paulson@9496
   131
paulson@9496
   132
(** Addition **)
paulson@9496
   133
paulson@9496
   134
Goal "intify(x) $+ y = x $+ y";
paulson@9496
   135
by (simp_tac (simpset() addsimps [zadd_def]) 1);
paulson@9496
   136
qed "zadd_intify1";
paulson@9496
   137
paulson@9496
   138
Goal "x $+ intify(y) = x $+ y";
paulson@9496
   139
by (simp_tac (simpset() addsimps [zadd_def]) 1);
paulson@9496
   140
qed "zadd_intify2";
paulson@9496
   141
Addsimps [zadd_intify1, zadd_intify2];
paulson@9496
   142
paulson@9496
   143
(** Multiplication **)
paulson@9496
   144
paulson@9496
   145
Goal "intify(x) $* y = x $* y";
paulson@9496
   146
by (simp_tac (simpset() addsimps [zmult_def]) 1);
paulson@9496
   147
qed "zmult_intify1";
paulson@9496
   148
paulson@9496
   149
Goal "x $* intify(y) = x $* y";
paulson@9496
   150
by (simp_tac (simpset() addsimps [zmult_def]) 1);
paulson@9496
   151
qed "zmult_intify2";
paulson@9496
   152
Addsimps [zmult_intify1, zmult_intify2];
paulson@9496
   153
paulson@5561
   154
paulson@5561
   155
(**** zminus: unary negation on int ****)
paulson@5561
   156
paulson@5561
   157
Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})";
paulson@5561
   158
by Safe_tac;
paulson@5561
   159
by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
paulson@5561
   160
qed "zminus_congruent";
paulson@5561
   161
paulson@9333
   162
val RSLIST = curry (op MRS);
paulson@9333
   163
paulson@5561
   164
(*Resolve th against the corresponding facts for zminus*)
paulson@5561
   165
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
paulson@5561
   166
paulson@9496
   167
Goalw [int_def,raw_zminus_def] "z : int ==> raw_zminus(z) : int";
paulson@6153
   168
by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
paulson@9496
   169
qed "raw_zminus_type";
paulson@9496
   170
paulson@9496
   171
Goalw [zminus_def] "$~z : int";
paulson@9496
   172
by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type]) 1);
paulson@5561
   173
qed "zminus_type";
paulson@9496
   174
AddIffs [zminus_type];
paulson@6153
   175
AddTCs [zminus_type];
paulson@5561
   176
paulson@9496
   177
paulson@9496
   178
Goalw [int_def,raw_zminus_def]
paulson@9496
   179
     "[| raw_zminus(z) = raw_zminus(w);  z: int;  w: int |] ==> z=w";
paulson@5561
   180
by (etac (zminus_ize UN_equiv_class_inject) 1);
paulson@5561
   181
by Safe_tac;
paulson@9496
   182
by (auto_tac (claset() addDs [eq_intrelD], simpset() addsimps add_ac));  
paulson@9496
   183
qed "raw_zminus_inject";
paulson@9496
   184
paulson@9496
   185
Goalw [zminus_def] "$~z = $~w ==> intify(z) = intify(w)";
paulson@9496
   186
by (blast_tac (claset() addSDs [raw_zminus_inject]) 1);
paulson@9496
   187
qed "zminus_inject_intify";
paulson@9496
   188
paulson@9496
   189
AddSDs [zminus_inject_intify];
paulson@9496
   190
paulson@9496
   191
Goal "[| $~z = $~w;  z: int;  w: int |] ==> z=w";
paulson@9496
   192
by Auto_tac;  
paulson@5561
   193
qed "zminus_inject";
paulson@5561
   194
paulson@9496
   195
Goalw [raw_zminus_def]
paulson@9496
   196
    "[| x: nat;  y: nat |] \
paulson@9496
   197
\    ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}";
paulson@9496
   198
by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
paulson@9496
   199
qed "raw_zminus";
paulson@9496
   200
paulson@5561
   201
Goalw [zminus_def]
paulson@9496
   202
    "[| x: nat;  y: nat |] \
paulson@9496
   203
\    ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
paulson@9496
   204
by (asm_simp_tac (simpset() addsimps [raw_zminus, image_intrel_int]) 1);
paulson@5561
   205
qed "zminus";
paulson@5561
   206
paulson@9496
   207
Goalw [int_def] "z : int ==> raw_zminus (raw_zminus(z)) = z";
paulson@9496
   208
by (auto_tac (claset(), simpset() addsimps [raw_zminus]));  
paulson@9496
   209
qed "raw_zminus_zminus";
paulson@5561
   210
paulson@9496
   211
Goal "$~ ($~ z) = intify(z)";
paulson@9496
   212
by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type, 
paulson@9496
   213
	                          raw_zminus_zminus]) 1);
paulson@9496
   214
qed "zminus_zminus_intify"; 
paulson@9496
   215
paulson@9496
   216
Goalw [int_of_def] "$~ ($#0) = $#0";
paulson@5561
   217
by (simp_tac (simpset() addsimps [zminus]) 1);
paulson@5561
   218
qed "zminus_0";
paulson@5561
   219
paulson@9496
   220
Addsimps [zminus_zminus_intify, zminus_0];
paulson@9496
   221
paulson@9496
   222
Goal "z : int ==> $~ ($~ z) = z";
paulson@9496
   223
by (Asm_simp_tac 1);
paulson@9496
   224
qed "zminus_zminus";
paulson@5561
   225
paulson@5561
   226
paulson@5561
   227
(**** znegative: the test for negative integers ****)
paulson@5561
   228
paulson@5561
   229
(*No natural number is negative!*)
paulson@5561
   230
Goalw [znegative_def, int_of_def]  "~ znegative($# n)";
paulson@5561
   231
by Safe_tac;
paulson@5561
   232
by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
paulson@5561
   233
by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
paulson@5561
   234
by (force_tac (claset(),
paulson@5561
   235
	       simpset() addsimps [add_le_self2 RS le_imp_not_lt]) 1);
paulson@5561
   236
qed "not_znegative_int_of";
paulson@5561
   237
paulson@5561
   238
Addsimps [not_znegative_int_of];
paulson@5561
   239
AddSEs   [not_znegative_int_of RS notE];
paulson@5561
   240
paulson@9496
   241
Goalw [znegative_def, int_of_def] "znegative($~ $# succ(n))";
paulson@5561
   242
by (asm_simp_tac (simpset() addsimps [zminus]) 1);
paulson@5561
   243
by (blast_tac (claset() addIs [nat_0_le]) 1);
paulson@5561
   244
qed "znegative_zminus_int_of";
paulson@5561
   245
paulson@5561
   246
Addsimps [znegative_zminus_int_of];
paulson@5561
   247
paulson@9496
   248
Goalw [znegative_def, int_of_def] "~ znegative($~ $# n) ==> natify(n)=0";
paulson@5561
   249
by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
paulson@9496
   250
by (dres_inst_tac [("x","0")] spec 1);
paulson@9496
   251
by (auto_tac(claset(), 
paulson@9496
   252
             simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff RS iff_sym]));
paulson@5561
   253
qed "not_znegative_imp_zero";
paulson@5561
   254
paulson@5561
   255
(**** zmagnitude: magnitide of an integer, as a natural number ****)
paulson@5561
   256
paulson@9496
   257
Goalw [zmagnitude_def] "zmagnitude($# n) = natify(n)";
paulson@9496
   258
by (auto_tac (claset(), simpset() addsimps [int_of_eq]));  
paulson@5561
   259
qed "zmagnitude_int_of";
paulson@5561
   260
paulson@9496
   261
Goal "natify(x)=n ==> $#x = $# n";
paulson@9496
   262
by (dtac sym 1);
paulson@9496
   263
by (asm_simp_tac (simpset() addsimps [int_of_eq]) 1);
paulson@9496
   264
qed "natify_int_of_eq";
paulson@9496
   265
paulson@9496
   266
Goalw [zmagnitude_def] "zmagnitude($~ $# n) = natify(n)";
paulson@9496
   267
by (rtac the_equality 1);
paulson@9496
   268
by (auto_tac((claset() addSDs [not_znegative_imp_zero, natify_int_of_eq], 
paulson@9496
   269
              simpset())
paulson@9496
   270
             delIffs [int_of_eq]));
paulson@9496
   271
by Auto_tac;  
paulson@5561
   272
qed "zmagnitude_zminus_int_of";
paulson@5561
   273
paulson@5561
   274
Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
paulson@5561
   275
paulson@5561
   276
Goalw [zmagnitude_def] "zmagnitude(z) : nat";
paulson@6153
   277
by (rtac theI2 1);
paulson@5561
   278
by Auto_tac;
paulson@5561
   279
qed "zmagnitude_type";
paulson@6153
   280
AddTCs [zmagnitude_type];
paulson@5561
   281
paulson@5561
   282
Goalw [int_def, znegative_def, int_of_def]
paulson@5561
   283
     "[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n"; 
paulson@5561
   284
by (auto_tac(claset() , simpset() addsimps [image_singleton_iff]));
paulson@5561
   285
by (rename_tac "i j" 1);
paulson@5561
   286
by (dres_inst_tac [("x", "i")] spec 1);
paulson@5561
   287
by (dres_inst_tac [("x", "j")] spec 1);
paulson@6153
   288
by (rtac bexI 1);
paulson@6153
   289
by (rtac (add_diff_inverse2 RS sym) 1);
paulson@5561
   290
by Auto_tac;
paulson@8201
   291
by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le]) 1);
paulson@5561
   292
qed "not_zneg_int_of";
paulson@5561
   293
paulson@5561
   294
Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
paulson@6153
   295
by (dtac not_zneg_int_of 1);
paulson@5561
   296
by Auto_tac;
paulson@5561
   297
qed "not_zneg_mag"; 
paulson@5561
   298
paulson@5561
   299
Addsimps [not_zneg_mag];
paulson@5561
   300
paulson@5561
   301
paulson@5561
   302
Goalw [int_def, znegative_def, int_of_def]
paulson@5561
   303
     "[| z: int; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))"; 
paulson@5561
   304
by (auto_tac(claset() addSDs [less_imp_Suc_add], 
paulson@5561
   305
	     simpset() addsimps [zminus, image_singleton_iff]));
paulson@5561
   306
by (rename_tac "m n j k" 1);
paulson@5561
   307
by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1);
paulson@5561
   308
by (rotate_tac ~2 2);
paulson@5561
   309
by (asm_full_simp_tac (simpset() addsimps add_ac) 2);
paulson@5561
   310
by (blast_tac (claset() addSDs [add_left_cancel]) 1);
paulson@5561
   311
qed "zneg_int_of";
paulson@5561
   312
paulson@5561
   313
Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; 
paulson@6153
   314
by (dtac zneg_int_of 1);
paulson@5561
   315
by Auto_tac;
paulson@5561
   316
qed "zneg_mag"; 
paulson@5561
   317
paulson@5561
   318
Addsimps [zneg_mag];
paulson@5561
   319
paulson@5561
   320
paulson@5561
   321
(**** zadd: addition on int ****)
paulson@5561
   322
paulson@5561
   323
(** Congruence property for addition **)
paulson@5561
   324
paulson@5561
   325
Goalw [congruent2_def]
paulson@5561
   326
    "congruent2(intrel, %z1 z2.                      \
paulson@5561
   327
\         let <x1,y1>=z1; <x2,y2>=z2                 \
paulson@5561
   328
\                           in intrel``{<x1#+x2, y1#+y2>})";
paulson@5561
   329
(*Proof via congruent2_commuteI seems longer*)
paulson@5561
   330
by Safe_tac;
paulson@5561
   331
by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
paulson@5561
   332
(*The rest should be trivial, but rearranging terms is hard;
paulson@5561
   333
  add_ac does not help rewriting with the assumptions.*)
paulson@5561
   334
by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
paulson@9491
   335
by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 1);
paulson@5561
   336
by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
paulson@5561
   337
qed "zadd_congruent2";
paulson@5561
   338
paulson@5561
   339
(*Resolve th against the corresponding facts for zadd*)
paulson@5561
   340
val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
paulson@5561
   341
paulson@9496
   342
Goalw [int_def,raw_zadd_def] "[| z: int;  w: int |] ==> raw_zadd(z,w) : int";
paulson@5561
   343
by (rtac (zadd_ize UN_equiv_class_type2) 1);
paulson@5561
   344
by (simp_tac (simpset() addsimps [Let_def]) 3);
paulson@9496
   345
by (REPEAT (assume_tac 1));
paulson@9496
   346
qed "raw_zadd_type";
paulson@5561
   347
paulson@9496
   348
Goal "z $+ w : int";
paulson@9496
   349
by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type]) 1);
paulson@9496
   350
qed "zadd_type";
paulson@9496
   351
AddIffs [zadd_type];  AddTCs [zadd_type];
paulson@9496
   352
paulson@9496
   353
Goalw [raw_zadd_def]
paulson@9496
   354
  "[| x1: nat; y1: nat;  x2: nat; y2: nat |]              \
paulson@9496
   355
\  ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) =  \
paulson@9496
   356
\      intrel `` {<x1#+x2, y1#+y2>}";
paulson@5561
   357
by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
paulson@5561
   358
by (simp_tac (simpset() addsimps [Let_def]) 1);
paulson@9496
   359
qed "raw_zadd";
paulson@9496
   360
paulson@9496
   361
Goalw [zadd_def]
paulson@9496
   362
  "[| x1: nat; y1: nat;  x2: nat; y2: nat |]         \
paulson@9496
   363
\  ==> (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =  \
paulson@9496
   364
\      intrel `` {<x1#+x2, y1#+y2>}";
paulson@9496
   365
by (asm_simp_tac (simpset() addsimps [raw_zadd, image_intrel_int]) 1);
paulson@5561
   366
qed "zadd";
paulson@5561
   367
paulson@9496
   368
Goalw [int_def,int_of_def] "z : int ==> raw_zadd ($#0,z) = z";
paulson@9496
   369
by (auto_tac (claset(), simpset() addsimps [raw_zadd]));  
paulson@9496
   370
qed "raw_zadd_0";
paulson@9496
   371
paulson@9496
   372
Goal "$#0 $+ z = intify(z)";
paulson@9496
   373
by (asm_simp_tac (simpset() addsimps [zadd_def, raw_zadd_0]) 1);
paulson@9496
   374
qed "zadd_0_intify";
paulson@9496
   375
Addsimps [zadd_0_intify];
paulson@9496
   376
paulson@9496
   377
Goal "z: int ==> $#0 $+ z = z";
paulson@9496
   378
by (Asm_simp_tac 1);
paulson@5561
   379
qed "zadd_0";
paulson@5561
   380
paulson@9496
   381
Goalw [int_def]
paulson@9496
   382
     "[| z: int;  w: int |] ==> $~ raw_zadd(z,w) = raw_zadd($~ z, $~ w)";
paulson@9496
   383
by (auto_tac (claset(), simpset() addsimps [zminus,raw_zadd]));  
paulson@9496
   384
qed "raw_zminus_zadd_distrib";
paulson@9496
   385
paulson@9496
   386
Goal "$~ (z $+ w) = $~ z $+ $~ w";
paulson@9496
   387
by (simp_tac (simpset() addsimps [zadd_def, raw_zminus_zadd_distrib]) 1);
paulson@5561
   388
qed "zminus_zadd_distrib";
paulson@5561
   389
paulson@9496
   390
Goalw [int_def] "[| z: int;  w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)";
paulson@9496
   391
by (auto_tac (claset(), simpset() addsimps raw_zadd::add_ac));  
paulson@9496
   392
qed "raw_zadd_commute";
paulson@9496
   393
paulson@9496
   394
Goal "z $+ w = w $+ z";
paulson@9496
   395
by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_commute]) 1);
paulson@5561
   396
qed "zadd_commute";
paulson@5561
   397
paulson@5561
   398
Goalw [int_def]
paulson@5561
   399
    "[| z1: int;  z2: int;  z3: int |]   \
paulson@9496
   400
\    ==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))";
paulson@9496
   401
by (auto_tac (claset(), simpset() addsimps [raw_zadd, add_assoc]));  
paulson@9496
   402
qed "raw_zadd_assoc";
paulson@9496
   403
paulson@9496
   404
Goal "(z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
paulson@9496
   405
by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type, raw_zadd_assoc]) 1);
paulson@5561
   406
qed "zadd_assoc";
paulson@5561
   407
paulson@5561
   408
(*For AC rewriting*)
paulson@9496
   409
Goal "z1$+(z2$+z3) = z2$+(z1$+z3)";
paulson@6153
   410
by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
paulson@6153
   411
by (asm_simp_tac (simpset() addsimps [zadd_commute]) 1);
paulson@5561
   412
qed "zadd_left_commute";
paulson@5561
   413
paulson@5561
   414
(*Integer addition is an AC operator*)
paulson@5561
   415
val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
paulson@5561
   416
paulson@9496
   417
Goalw [int_of_def] "$# (m #+ n) = ($#m) $+ ($#n)";
paulson@5561
   418
by (asm_simp_tac (simpset() addsimps [zadd]) 1);
paulson@5561
   419
qed "int_of_add";
paulson@5561
   420
paulson@9496
   421
Goalw [int_def,int_of_def] "z : int ==> raw_zadd (z, $~ z) = $#0";
paulson@9496
   422
by (auto_tac (claset(), simpset() addsimps [zminus, raw_zadd, add_commute]));  
paulson@9496
   423
qed "raw_zadd_zminus_inverse";
paulson@9496
   424
paulson@9496
   425
Goal "z $+ ($~ z) = $#0";
paulson@9496
   426
by (simp_tac (simpset() addsimps [zadd_def]) 1);
paulson@9496
   427
by (stac (zminus_intify RS sym) 1);
paulson@9496
   428
by (rtac (intify_in_int RS raw_zadd_zminus_inverse) 1); 
paulson@5561
   429
qed "zadd_zminus_inverse";
paulson@5561
   430
paulson@9496
   431
Goal "($~ z) $+ z = $#0";
paulson@9496
   432
by (simp_tac (simpset() addsimps [zadd_commute, zadd_zminus_inverse]) 1);
paulson@5561
   433
qed "zadd_zminus_inverse2";
paulson@5561
   434
paulson@9496
   435
Goal "z $+ $#0 = intify(z)";
paulson@9496
   436
by (rtac ([zadd_commute, zadd_0_intify] MRS trans) 1);
paulson@9496
   437
qed "zadd_0_right_intify";
paulson@9496
   438
Addsimps [zadd_0_right_intify];
paulson@9496
   439
paulson@5561
   440
Goal "z:int ==> z $+ $#0 = z";
paulson@9496
   441
by (Asm_simp_tac 1);
paulson@5561
   442
qed "zadd_0_right";
paulson@5561
   443
paulson@9496
   444
Addsimps [zadd_zminus_inverse, zadd_zminus_inverse2];
paulson@5561
   445
paulson@5561
   446
paulson@5561
   447
(*Need properties of $- ???  Or use $- just as an abbreviation?
paulson@9496
   448
     [| m: nat;  n: nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)
paulson@5561
   449
*)
paulson@5561
   450
paulson@5561
   451
(**** zmult: multiplication on int ****)
paulson@5561
   452
paulson@5561
   453
(** Congruence property for multiplication **)
paulson@5561
   454
paulson@5561
   455
Goal "congruent2(intrel, %p1 p2.                 \
paulson@5561
   456
\               split(%x1 y1. split(%x2 y2.     \
paulson@5561
   457
\                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
paulson@5561
   458
by (rtac (equiv_intrel RS congruent2_commuteI) 1);
paulson@5561
   459
by Safe_tac;
paulson@5561
   460
by (ALLGOALS Asm_simp_tac);
paulson@5561
   461
(*Proof that zmult is congruent in one argument*)
paulson@5561
   462
by (asm_simp_tac 
paulson@5561
   463
    (simpset() addsimps add_ac @ [add_mult_distrib_left RS sym]) 2);
paulson@5561
   464
by (asm_simp_tac
paulson@5561
   465
    (simpset() addsimps [add_assoc RS sym, add_mult_distrib_left RS sym]) 2);
paulson@5561
   466
(*Proof that zmult is commutative on representatives*)
paulson@5561
   467
by (asm_simp_tac (simpset() addsimps mult_ac@add_ac) 1);
paulson@5561
   468
qed "zmult_congruent2";
paulson@5561
   469
paulson@5561
   470
paulson@5561
   471
(*Resolve th against the corresponding facts for zmult*)
paulson@5561
   472
val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
paulson@5561
   473
paulson@9496
   474
Goalw [int_def,raw_zmult_def] "[| z: int;  w: int |] ==> raw_zmult(z,w) : int";
paulson@5561
   475
by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
paulson@5561
   476
                      split_type, add_type, mult_type, 
paulson@5561
   477
                      quotientI, SigmaI] 1));
paulson@9496
   478
qed "raw_zmult_type";
paulson@9496
   479
paulson@9496
   480
Goal "z $* w : int";
paulson@9496
   481
by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type]) 1);
paulson@5561
   482
qed "zmult_type";
paulson@9496
   483
AddIffs [zmult_type];  AddTCs [zmult_type];
paulson@9496
   484
paulson@9496
   485
Goalw [raw_zmult_def]
paulson@9496
   486
     "[| x1: nat; y1: nat;  x2: nat; y2: nat |]    \
paulson@9496
   487
\     ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) =     \
paulson@9496
   488
\         intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
paulson@9496
   489
by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
paulson@9496
   490
qed "raw_zmult";
paulson@5561
   491
paulson@5561
   492
Goalw [zmult_def]
paulson@9496
   493
     "[| x1: nat; y1: nat;  x2: nat; y2: nat |]    \
paulson@9496
   494
\     ==> (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
paulson@9496
   495
\         intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
paulson@9496
   496
by (asm_simp_tac (simpset() addsimps [raw_zmult, image_intrel_int]) 1);
paulson@5561
   497
qed "zmult";
paulson@5561
   498
paulson@9496
   499
Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#0,z) = $#0";
paulson@9496
   500
by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
paulson@9496
   501
qed "raw_zmult_0";
paulson@9496
   502
paulson@9496
   503
Goal "$#0 $* z = $#0";
paulson@9496
   504
by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_0]) 1);
paulson@5561
   505
qed "zmult_0";
paulson@9496
   506
Addsimps [zmult_0];
paulson@5561
   507
paulson@9496
   508
Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#1,z) = z";
paulson@9496
   509
by (auto_tac (claset(), simpset() addsimps [raw_zmult]));  
paulson@9496
   510
qed "raw_zmult_1";
paulson@9496
   511
paulson@9496
   512
Goal "$#1 $* z = intify(z)";
paulson@9496
   513
by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_1]) 1);
paulson@9496
   514
qed "zmult_1_intify";
paulson@9496
   515
Addsimps [zmult_1_intify];
paulson@9496
   516
paulson@9496
   517
Goal "z : int ==> $#1 $* z = z";
paulson@9496
   518
by (Asm_simp_tac 1);
paulson@5561
   519
qed "zmult_1";
paulson@5561
   520
paulson@9496
   521
Goalw [int_def] "[| z: int;  w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)";
paulson@9496
   522
by (auto_tac (claset(), simpset() addsimps [raw_zmult] @ add_ac @ mult_ac));  
paulson@9496
   523
qed "raw_zmult_commute";
paulson@5561
   524
paulson@9496
   525
Goal "z $* w = w $* z";
paulson@9496
   526
by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_commute]) 1);
paulson@5561
   527
qed "zmult_commute";
paulson@5561
   528
paulson@5561
   529
Goalw [int_def]
paulson@9496
   530
     "[| z: int;  w: int |] ==> raw_zmult($~ z, w) = $~ raw_zmult(z, w)";
paulson@9496
   531
by (auto_tac (claset(), simpset() addsimps [zminus, raw_zmult] @ add_ac));  
paulson@9496
   532
qed "raw_zmult_zminus";
paulson@9496
   533
paulson@9496
   534
Goal "($~ z) $* w = $~ (z $* w)";
paulson@9496
   535
by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_zminus]) 1);
paulson@9496
   536
by (stac (zminus_intify RS sym) 1 THEN rtac raw_zmult_zminus 1); 
paulson@9496
   537
by Auto_tac;  
paulson@9496
   538
qed "zmult_zminus";
paulson@9496
   539
Addsimps [zmult_zminus];
paulson@9496
   540
paulson@9496
   541
Goal "($~ z) $* ($~ w) = (z $* w)";
paulson@9496
   542
by (stac zmult_zminus 1);
paulson@9496
   543
by (stac zmult_commute 1 THEN stac zmult_zminus 1);
paulson@9496
   544
by (simp_tac (simpset() addsimps [zmult_commute])1);
paulson@9496
   545
qed "zmult_zminus_zminus";
paulson@9496
   546
paulson@9496
   547
Goalw [int_def]
paulson@9496
   548
    "[| z1: int;  z2: int;  z3: int |]   \
paulson@9496
   549
\    ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))";
paulson@9496
   550
by (auto_tac (claset(), 
paulson@9496
   551
  simpset() addsimps [raw_zmult, add_mult_distrib_left] @ add_ac @ mult_ac));  
paulson@9496
   552
qed "raw_zmult_assoc";
paulson@9496
   553
paulson@9496
   554
Goal "(z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
paulson@9496
   555
by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type, 
paulson@9496
   556
                                  raw_zmult_assoc]) 1);
paulson@5561
   557
qed "zmult_assoc";
paulson@5561
   558
paulson@5561
   559
(*For AC rewriting*)
paulson@9496
   560
Goal "z1$*(z2$*z3) = z2$*(z1$*z3)";
paulson@6153
   561
by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
paulson@6153
   562
by (asm_simp_tac (simpset() addsimps [zmult_commute]) 1);
paulson@5561
   563
qed "zmult_left_commute";
paulson@5561
   564
paulson@5561
   565
(*Integer multiplication is an AC operator*)
paulson@5561
   566
val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
paulson@5561
   567
paulson@5561
   568
Goalw [int_def]
paulson@9496
   569
    "[| z1: int;  z2: int;  w: int |]  \
paulson@9496
   570
\    ==> raw_zmult(raw_zadd(z1,z2), w) = \
paulson@9496
   571
\        raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))";
paulson@9496
   572
by (auto_tac (claset(), 
paulson@9496
   573
              simpset() addsimps [raw_zadd, raw_zmult, add_mult_distrib_left] @ 
paulson@9496
   574
                                 add_ac @ mult_ac));  
paulson@9496
   575
qed "raw_zadd_zmult_distrib";
paulson@9496
   576
paulson@9496
   577
Goal "(z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
paulson@9496
   578
by (simp_tac (simpset() addsimps [zmult_def, zadd_def, raw_zadd_type, 
paulson@9496
   579
     	                          raw_zmult_type, raw_zadd_zmult_distrib]) 1);
paulson@5561
   580
qed "zadd_zmult_distrib";
paulson@5561
   581
paulson@9496
   582
Goal "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)";
paulson@9496
   583
by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute,
paulson@9496
   584
                                  zadd_zmult_distrib]) 1);
paulson@9496
   585
qed "zadd_zmult_distrib_left";
paulson@9496
   586
paulson@5561
   587
val int_typechecks =
paulson@5561
   588
    [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
paulson@5561
   589
paulson@5561
   590