src/ZF/Integ/Int.ML
author paulson
Fri Jul 14 13:39:03 2000 +0200 (2000-07-14)
changeset 9333 5cacc383157a
parent 8201 a81d18b0a9b1
child 9491 1a36151ee2fc
permissions -rw-r--r--
changed the quotient syntax from / to //
     1 (*  Title:      ZF/Integ/Int.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1993  University of Cambridge
     5 
     6 The integers as equivalence classes over nat*nat.
     7 
     8 Could also prove...
     9 "znegative(z) ==> $# zmagnitude(z) = $~ z"
    10 "~ znegative(z) ==> $# zmagnitude(z) = z"
    11 $< is a linear ordering
    12 $+ and $* are monotonic wrt $<
    13 *)
    14 
    15 AddSEs [quotientE];
    16 
    17 (*** Proving that intrel is an equivalence relation ***)
    18 
    19 (*By luck, requires no typing premises for y1, y2,y3*)
    20 val eqa::eqb::prems = goal Arith.thy 
    21     "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2;  \
    22 \       x1: nat; x2: nat; x3: nat |]    ==>    x1 #+ y3 = x3 #+ y1";
    23 by (cut_facts_tac prems 1);
    24 by (res_inst_tac [("k","x2")] add_left_cancel 1);
    25 by (rtac (add_left_commute RS trans) 1);
    26 by Auto_tac;
    27 by (stac eqb 1);
    28 by (rtac (add_left_commute RS trans) 1);
    29 by (stac eqa 3);
    30 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_left_commute])));
    31 qed "int_trans_lemma";
    32 
    33 (** Natural deduction for intrel **)
    34 
    35 Goalw [intrel_def]
    36     "<<x1,y1>,<x2,y2>>: intrel <-> \
    37 \    x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1";
    38 by (Fast_tac 1);
    39 qed "intrel_iff";
    40 
    41 Goalw [intrel_def]
    42     "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
    43 \             <<x1,y1>,<x2,y2>>: intrel";
    44 by (fast_tac (claset() addIs prems) 1);
    45 qed "intrelI";
    46 
    47 (*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
    48 Goalw [intrel_def]
    49   "p: intrel --> (EX x1 y1 x2 y2. \
    50 \                  p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \
    51 \                  x1: nat & y1: nat & x2: nat & y2: nat)";
    52 by (Fast_tac 1);
    53 qed "intrelE_lemma";
    54 
    55 val [major,minor] = goal thy
    56   "[| p: intrel;  \
    57 \     !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1; \
    58 \                       x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \
    59 \  ==> Q";
    60 by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
    61 by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
    62 qed "intrelE";
    63 
    64 AddSIs [intrelI];
    65 AddSEs [intrelE];
    66 
    67 Goalw [equiv_def, refl_def, sym_def, trans_def]
    68     "equiv(nat*nat, intrel)";
    69 by (fast_tac (claset() addSEs [sym, int_trans_lemma]) 1);
    70 qed "equiv_intrel";
    71 
    72 
    73 Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
    74 	  add_0_right, add_succ_right];
    75 Addcongs [conj_cong];
    76 
    77 val eq_intrelD = equiv_intrel RSN (2,eq_equiv_class);
    78 
    79 (** int_of: the injection from nat to int **)
    80 
    81 Goalw [int_def,quotient_def,int_of_def]
    82     "m : nat ==> $#m : int";
    83 by Auto_tac;
    84 qed "int_of_type";
    85 
    86 Addsimps [int_of_type];
    87 AddTCs   [int_of_type];
    88 
    89 Goalw [int_of_def] "[| $#m = $#n;  m: nat |] ==> m=n";
    90 by (dtac (sym RS eq_intrelD) 1);
    91 by Auto_tac;
    92 qed "int_of_inject";
    93 
    94 AddSDs [int_of_inject];
    95 
    96 Goal "m: nat ==> ($# m = $# n) <-> (m = n)"; 
    97 by (Blast_tac 1); 
    98 qed "int_of_eq"; 
    99 Addsimps [int_of_eq]; 
   100 
   101 (**** zminus: unary negation on int ****)
   102 
   103 Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})";
   104 by Safe_tac;
   105 by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
   106 qed "zminus_congruent";
   107 
   108 val RSLIST = curry (op MRS);
   109 
   110 (*Resolve th against the corresponding facts for zminus*)
   111 val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
   112 
   113 Goalw [int_def,zminus_def] "z : int ==> $~z : int";
   114 by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
   115 qed "zminus_type";
   116 AddTCs [zminus_type];
   117 
   118 Goalw [int_def,zminus_def] "[| $~z = $~w;  z: int;  w: int |] ==> z=w";
   119 by (etac (zminus_ize UN_equiv_class_inject) 1);
   120 by Safe_tac;
   121 (*The setloop is only needed because assumptions are in the wrong order!*)
   122 by (asm_full_simp_tac (simpset() addsimps add_ac
   123                        setloop dtac eq_intrelD) 1);
   124 qed "zminus_inject";
   125 
   126 Goalw [zminus_def]
   127     "[| x: nat;  y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
   128 by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
   129 qed "zminus";
   130 
   131 Goalw [int_def] "z : int ==> $~ ($~ z) = z";
   132 by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   133 by (asm_simp_tac (simpset() addsimps [zminus]) 1);
   134 qed "zminus_zminus";
   135 
   136 Goalw [int_def, int_of_def] "$~ ($#0) = $#0";
   137 by (simp_tac (simpset() addsimps [zminus]) 1);
   138 qed "zminus_0";
   139 
   140 Addsimps [zminus_zminus, zminus_0];
   141 
   142 
   143 (**** znegative: the test for negative integers ****)
   144 
   145 (*No natural number is negative!*)
   146 Goalw [znegative_def, int_of_def]  "~ znegative($# n)";
   147 by Safe_tac;
   148 by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
   149 by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
   150 by (force_tac (claset(),
   151 	       simpset() addsimps [add_le_self2 RS le_imp_not_lt]) 1);
   152 qed "not_znegative_int_of";
   153 
   154 Addsimps [not_znegative_int_of];
   155 AddSEs   [not_znegative_int_of RS notE];
   156 
   157 Goalw [znegative_def, int_of_def] "n: nat ==> znegative($~ $# succ(n))";
   158 by (asm_simp_tac (simpset() addsimps [zminus]) 1);
   159 by (blast_tac (claset() addIs [nat_0_le]) 1);
   160 qed "znegative_zminus_int_of";
   161 
   162 Addsimps [znegative_zminus_int_of];
   163 
   164 Goalw [znegative_def, int_of_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0";
   165 by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
   166 by (etac natE 1);
   167 by (dres_inst_tac [("x","0")] spec 2);
   168 by Auto_tac;
   169 qed "not_znegative_imp_zero";
   170 
   171 (**** zmagnitude: magnitide of an integer, as a natural number ****)
   172 
   173 Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n";
   174 by Auto_tac;
   175 qed "zmagnitude_int_of";
   176 
   177 Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n";
   178 by (force_tac(claset() addDs [not_znegative_imp_zero], simpset())1);
   179 qed "zmagnitude_zminus_int_of";
   180 
   181 Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
   182 
   183 Goalw [zmagnitude_def] "zmagnitude(z) : nat";
   184 by (rtac theI2 1);
   185 by Auto_tac;
   186 qed "zmagnitude_type";
   187 AddTCs [zmagnitude_type];
   188 
   189 Goalw [int_def, znegative_def, int_of_def]
   190      "[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n"; 
   191 by (auto_tac(claset() , simpset() addsimps [image_singleton_iff]));
   192 by (rename_tac "i j" 1);
   193 by (dres_inst_tac [("x", "i")] spec 1);
   194 by (dres_inst_tac [("x", "j")] spec 1);
   195 by (rtac bexI 1);
   196 by (rtac (add_diff_inverse2 RS sym) 1);
   197 by Auto_tac;
   198 by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le]) 1);
   199 qed "not_zneg_int_of";
   200 
   201 Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
   202 by (dtac not_zneg_int_of 1);
   203 by Auto_tac;
   204 qed "not_zneg_mag"; 
   205 
   206 Addsimps [not_zneg_mag];
   207 
   208 
   209 Goalw [int_def, znegative_def, int_of_def]
   210      "[| z: int; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))"; 
   211 by (auto_tac(claset() addSDs [less_imp_Suc_add], 
   212 	     simpset() addsimps [zminus, image_singleton_iff]));
   213 by (rename_tac "m n j k" 1);
   214 by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1);
   215 by (rotate_tac ~2 2);
   216 by (asm_full_simp_tac (simpset() addsimps add_ac) 2);
   217 by (blast_tac (claset() addSDs [add_left_cancel]) 1);
   218 qed "zneg_int_of";
   219 
   220 Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; 
   221 by (dtac zneg_int_of 1);
   222 by Auto_tac;
   223 qed "zneg_mag"; 
   224 
   225 Addsimps [zneg_mag];
   226 
   227 
   228 (**** zadd: addition on int ****)
   229 
   230 (** Congruence property for addition **)
   231 
   232 Goalw [congruent2_def]
   233     "congruent2(intrel, %z1 z2.                      \
   234 \         let <x1,y1>=z1; <x2,y2>=z2                 \
   235 \                           in intrel``{<x1#+x2, y1#+y2>})";
   236 (*Proof via congruent2_commuteI seems longer*)
   237 by Safe_tac;
   238 by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
   239 (*The rest should be trivial, but rearranging terms is hard;
   240   add_ac does not help rewriting with the assumptions.*)
   241 by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
   242 by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3);
   243 by Auto_tac;
   244 by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
   245 qed "zadd_congruent2";
   246 
   247 (*Resolve th against the corresponding facts for zadd*)
   248 val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
   249 
   250 Goalw [int_def,zadd_def] "[| z: int;  w: int |] ==> z $+ w : int";
   251 by (rtac (zadd_ize UN_equiv_class_type2) 1);
   252 by (simp_tac (simpset() addsimps [Let_def]) 3);
   253 by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
   254 qed "zadd_type";
   255 AddTCs [zadd_type];
   256 
   257 Goalw [zadd_def]
   258   "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>       \
   259 \           (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =        \
   260 \           intrel `` {<x1#+x2, y1#+y2>}";
   261 by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
   262 by (simp_tac (simpset() addsimps [Let_def]) 1);
   263 qed "zadd";
   264 
   265 Goalw [int_def,int_of_def] "z : int ==> $#0 $+ z = z";
   266 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   267 by (asm_simp_tac (simpset() addsimps [zadd]) 1);
   268 qed "zadd_0";
   269 
   270 Goalw [int_def] "[| z: int;  w: int |] ==> $~ (z $+ w) = $~ z $+ $~ w";
   271 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   272 by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
   273 qed "zminus_zadd_distrib";
   274 
   275 Goalw [int_def] "[| z: int;  w: int |] ==> z $+ w = w $+ z";
   276 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   277 by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
   278 qed "zadd_commute";
   279 
   280 Goalw [int_def]
   281     "[| z1: int;  z2: int;  z3: int |]   \
   282 \    ==> (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
   283 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   284 (*rewriting is much faster without intrel_iff, etc.*)
   285 by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
   286 qed "zadd_assoc";
   287 
   288 (*For AC rewriting*)
   289 Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)";
   290 by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
   291 by (asm_simp_tac (simpset() addsimps [zadd_commute]) 1);
   292 qed "zadd_left_commute";
   293 
   294 (*Integer addition is an AC operator*)
   295 val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
   296 
   297 Goalw [int_of_def]
   298     "[| m: nat;  n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
   299 by (asm_simp_tac (simpset() addsimps [zadd]) 1);
   300 qed "int_of_add";
   301 
   302 Goalw [int_def,int_of_def] "z : int ==> z $+ ($~ z) = $#0";
   303 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   304 by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
   305 qed "zadd_zminus_inverse";
   306 
   307 Goal "z : int ==> ($~ z) $+ z = $#0";
   308 by (asm_simp_tac
   309     (simpset() addsimps [zadd_commute, zminus_type, zadd_zminus_inverse]) 1);
   310 qed "zadd_zminus_inverse2";
   311 
   312 Goal "z:int ==> z $+ $#0 = z";
   313 by (rtac (zadd_commute RS trans) 1);
   314 by (REPEAT (ares_tac [int_of_type, nat_0I, zadd_0] 1));
   315 qed "zadd_0_right";
   316 
   317 Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
   318 
   319 
   320 (*Need properties of $- ???  Or use $- just as an abbreviation?
   321      [| m: nat;  n: nat;  m>=n |] ==> $# (m #- n) = ($#m) $- ($#n)
   322 *)
   323 
   324 (**** zmult: multiplication on int ****)
   325 
   326 (** Congruence property for multiplication **)
   327 
   328 Goal "congruent2(intrel, %p1 p2.                 \
   329 \               split(%x1 y1. split(%x2 y2.     \
   330 \                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
   331 by (rtac (equiv_intrel RS congruent2_commuteI) 1);
   332 by Safe_tac;
   333 by (ALLGOALS Asm_simp_tac);
   334 (*Proof that zmult is congruent in one argument*)
   335 by (asm_simp_tac 
   336     (simpset() addsimps add_ac @ [add_mult_distrib_left RS sym]) 2);
   337 by (asm_simp_tac
   338     (simpset() addsimps [add_assoc RS sym, add_mult_distrib_left RS sym]) 2);
   339 (*Proof that zmult is commutative on representatives*)
   340 by (asm_simp_tac (simpset() addsimps mult_ac@add_ac) 1);
   341 qed "zmult_congruent2";
   342 
   343 
   344 (*Resolve th against the corresponding facts for zmult*)
   345 val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
   346 
   347 Goalw [int_def,zmult_def] "[| z: int;  w: int |] ==> z $* w : int";
   348 by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
   349                       split_type, add_type, mult_type, 
   350                       quotientI, SigmaI] 1));
   351 qed "zmult_type";
   352 AddTCs [zmult_type];
   353 
   354 Goalw [zmult_def]
   355      "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>    \
   356 \              (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
   357 \              intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
   358 by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
   359 qed "zmult";
   360 
   361 Goalw [int_def,int_of_def] "z : int ==> $#0 $* z = $#0";
   362 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   363 by (asm_simp_tac (simpset() addsimps [zmult]) 1);
   364 qed "zmult_0";
   365 
   366 Goalw [int_def,int_of_def] "z : int ==> $#1 $* z = z";
   367 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   368 by (asm_simp_tac (simpset() addsimps [zmult, add_0_right]) 1);
   369 qed "zmult_1";
   370 
   371 Goalw [int_def] "[| z: int;  w: int |] ==> ($~ z) $* w = $~ (z $* w)";
   372 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   373 by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
   374 qed "zmult_zminus";
   375 
   376 Addsimps [zmult_0, zmult_1, zmult_zminus];
   377 
   378 Goalw [int_def] "[| z: int;  w: int |] ==> ($~ z) $* ($~ w) = (z $* w)";
   379 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   380 by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
   381 qed "zmult_zminus_zminus";
   382 
   383 Goalw [int_def] "[| z: int;  w: int |] ==> z $* w = w $* z";
   384 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   385 by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1);
   386 qed "zmult_commute";
   387 
   388 Goalw [int_def]
   389     "[| z1: int;  z2: int;  z3: int |]     \
   390 \    ==> (z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
   391 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   392 by (asm_simp_tac 
   393     (simpset() addsimps [zmult, add_mult_distrib_left, 
   394                          add_mult_distrib] @ add_ac @ mult_ac) 1);
   395 qed "zmult_assoc";
   396 
   397 (*For AC rewriting*)
   398 Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)";
   399 by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
   400 by (asm_simp_tac (simpset() addsimps [zmult_commute]) 1);
   401 qed "zmult_left_commute";
   402 
   403 (*Integer multiplication is an AC operator*)
   404 val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
   405 
   406 Goalw [int_def]
   407     "[| z1: int;  z2: int;  w: int |] ==> \
   408 \                (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
   409 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   410 by (asm_simp_tac (simpset() addsimps [zadd, zmult, add_mult_distrib]) 1);
   411 by (asm_simp_tac (simpset() addsimps add_ac @ mult_ac) 1);
   412 qed "zadd_zmult_distrib";
   413 
   414 val int_typechecks =
   415     [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
   416 
   417 Addsimps int_typechecks;
   418 
   419 
   420