src/CTT/Arith.ML
 author paulson Tue Apr 30 11:08:09 1996 +0200 (1996-04-30) changeset 1702 4aa538e82f76 parent 1459 d12da312eff4 child 3837 d7f033c74b38 permissions -rw-r--r--
Cosmetic re-ordering of declarations
```     1 (*  Title:      CTT/arith
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1991  University of Cambridge
```
```     5
```
```     6 Theorems for arith.thy (Arithmetic operators)
```
```     7
```
```     8 Proofs about elementary arithmetic: addition, multiplication, etc.
```
```     9 Tests definitions and simplifier.
```
```    10 *)
```
```    11
```
```    12 open Arith;
```
```    13 val arith_defs = [add_def, diff_def, absdiff_def, mult_def, mod_def, div_def];
```
```    14
```
```    15
```
```    16 (** Addition *)
```
```    17
```
```    18 (*typing of add: short and long versions*)
```
```    19
```
```    20 qed_goalw "add_typing" Arith.thy arith_defs
```
```    21     "[| a:N;  b:N |] ==> a #+ b : N"
```
```    22  (fn prems=> [ (typechk_tac prems) ]);
```
```    23
```
```    24 qed_goalw "add_typingL" Arith.thy arith_defs
```
```    25     "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N"
```
```    26  (fn prems=> [ (equal_tac prems) ]);
```
```    27
```
```    28
```
```    29 (*computation for add: 0 and successor cases*)
```
```    30
```
```    31 qed_goalw "addC0" Arith.thy arith_defs
```
```    32     "b:N ==> 0 #+ b = b : N"
```
```    33  (fn prems=> [ (rew_tac prems) ]);
```
```    34
```
```    35 qed_goalw "addC_succ" Arith.thy arith_defs
```
```    36     "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"
```
```    37  (fn prems=> [ (rew_tac prems) ]);
```
```    38
```
```    39
```
```    40 (** Multiplication *)
```
```    41
```
```    42 (*typing of mult: short and long versions*)
```
```    43
```
```    44 qed_goalw "mult_typing" Arith.thy arith_defs
```
```    45     "[| a:N;  b:N |] ==> a #* b : N"
```
```    46  (fn prems=>
```
```    47   [ (typechk_tac([add_typing]@prems)) ]);
```
```    48
```
```    49 qed_goalw "mult_typingL" Arith.thy arith_defs
```
```    50     "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N"
```
```    51  (fn prems=>
```
```    52   [ (equal_tac (prems@[add_typingL])) ]);
```
```    53
```
```    54 (*computation for mult: 0 and successor cases*)
```
```    55
```
```    56 qed_goalw "multC0" Arith.thy arith_defs
```
```    57     "b:N ==> 0 #* b = 0 : N"
```
```    58  (fn prems=> [ (rew_tac prems) ]);
```
```    59
```
```    60 qed_goalw "multC_succ" Arith.thy arith_defs
```
```    61     "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"
```
```    62  (fn prems=> [ (rew_tac prems) ]);
```
```    63
```
```    64
```
```    65 (** Difference *)
```
```    66
```
```    67 (*typing of difference*)
```
```    68
```
```    69 qed_goalw "diff_typing" Arith.thy arith_defs
```
```    70     "[| a:N;  b:N |] ==> a - b : N"
```
```    71  (fn prems=> [ (typechk_tac prems) ]);
```
```    72
```
```    73 qed_goalw "diff_typingL" Arith.thy arith_defs
```
```    74     "[| a=c:N;  b=d:N |] ==> a - b = c - d : N"
```
```    75  (fn prems=> [ (equal_tac prems) ]);
```
```    76
```
```    77
```
```    78
```
```    79 (*computation for difference: 0 and successor cases*)
```
```    80
```
```    81 qed_goalw "diffC0" Arith.thy arith_defs
```
```    82     "a:N ==> a - 0 = a : N"
```
```    83  (fn prems=> [ (rew_tac prems) ]);
```
```    84
```
```    85 (*Note: rec(a, 0, %z w.z) is pred(a). *)
```
```    86
```
```    87 qed_goalw "diff_0_eq_0" Arith.thy arith_defs
```
```    88     "b:N ==> 0 - b = 0 : N"
```
```    89  (fn prems=>
```
```    90   [ (NE_tac "b" 1),
```
```    91     (hyp_rew_tac prems) ]);
```
```    92
```
```    93
```
```    94 (*Essential to simplify FIRST!!  (Else we get a critical pair)
```
```    95   succ(a) - succ(b) rewrites to   pred(succ(a) - b)  *)
```
```    96 qed_goalw "diff_succ_succ" Arith.thy arith_defs
```
```    97     "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N"
```
```    98  (fn prems=>
```
```    99   [ (hyp_rew_tac prems),
```
```   100     (NE_tac "b" 1),
```
```   101     (hyp_rew_tac prems) ]);
```
```   102
```
```   103
```
```   104
```
```   105 (*** Simplification *)
```
```   106
```
```   107 val arith_typing_rls =
```
```   108   [add_typing, mult_typing, diff_typing];
```
```   109
```
```   110 val arith_congr_rls =
```
```   111   [add_typingL, mult_typingL, diff_typingL];
```
```   112
```
```   113 val congr_rls = arith_congr_rls@standard_congr_rls;
```
```   114
```
```   115 val arithC_rls =
```
```   116   [addC0, addC_succ,
```
```   117    multC0, multC_succ,
```
```   118    diffC0, diff_0_eq_0, diff_succ_succ];
```
```   119
```
```   120
```
```   121 structure Arith_simp_data: TSIMP_DATA =
```
```   122   struct
```
```   123   val refl              = refl_elem
```
```   124   val sym               = sym_elem
```
```   125   val trans             = trans_elem
```
```   126   val refl_red          = refl_red
```
```   127   val trans_red         = trans_red
```
```   128   val red_if_equal      = red_if_equal
```
```   129   val default_rls       = arithC_rls @ comp_rls
```
```   130   val routine_tac       = routine_tac (arith_typing_rls @ routine_rls)
```
```   131   end;
```
```   132
```
```   133 structure Arith_simp = TSimpFun (Arith_simp_data);
```
```   134
```
```   135 fun arith_rew_tac prems = make_rew_tac
```
```   136     (Arith_simp.norm_tac(congr_rls, prems));
```
```   137
```
```   138 fun hyp_arith_rew_tac prems = make_rew_tac
```
```   139     (Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems));
```
```   140
```
```   141
```
```   142 (**********
```
```   143   Addition
```
```   144  **********)
```
```   145
```
```   146 (*Associative law for addition*)
```
```   147 qed_goal "add_assoc" Arith.thy
```
```   148     "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"
```
```   149  (fn prems=>
```
```   150   [ (NE_tac "a" 1),
```
```   151     (hyp_arith_rew_tac prems) ]);
```
```   152
```
```   153
```
```   154 (*Commutative law for addition.  Can be proved using three inductions.
```
```   155   Must simplify after first induction!  Orientation of rewrites is delicate*)
```
```   156 qed_goal "add_commute" Arith.thy
```
```   157     "[| a:N;  b:N |] ==> a #+ b = b #+ a : N"
```
```   158  (fn prems=>
```
```   159   [ (NE_tac "a" 1),
```
```   160     (hyp_arith_rew_tac prems),
```
```   161     (NE_tac "b" 2),
```
```   162     (rtac sym_elem 1),
```
```   163     (NE_tac "b" 1),
```
```   164     (hyp_arith_rew_tac prems) ]);
```
```   165
```
```   166
```
```   167 (****************
```
```   168   Multiplication
```
```   169  ****************)
```
```   170
```
```   171 (*Commutative law for multiplication
```
```   172 qed_goal "mult_commute" Arith.thy
```
```   173     "[| a:N;  b:N |] ==> a #* b = b #* a : N"
```
```   174  (fn prems=>
```
```   175   [ (NE_tac "a" 1),
```
```   176     (hyp_arith_rew_tac prems),
```
```   177     (NE_tac "b" 2),
```
```   178     (rtac sym_elem 1),
```
```   179     (NE_tac "b" 1),
```
```   180     (hyp_arith_rew_tac prems) ]);   NEEDS COMMUTATIVE MATCHING
```
```   181 ***************)
```
```   182
```
```   183 (*right annihilation in product*)
```
```   184 qed_goal "mult_0_right" Arith.thy
```
```   185     "a:N ==> a #* 0 = 0 : N"
```
```   186  (fn prems=>
```
```   187   [ (NE_tac "a" 1),
```
```   188     (hyp_arith_rew_tac prems) ]);
```
```   189
```
```   190 (*right successor law for multiplication*)
```
```   191 qed_goal "mult_succ_right" Arith.thy
```
```   192     "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"
```
```   193  (fn prems=>
```
```   194   [ (NE_tac "a" 1),
```
```   195 (*swap round the associative law of addition*)
```
```   196     (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])),
```
```   197 (*leaves a goal involving a commutative law*)
```
```   198     (REPEAT (assume_tac 1  ORELSE
```
```   199             resolve_tac
```
```   200              (prems@[add_commute,mult_typingL,add_typingL]@
```
```   201                intrL_rls@[refl_elem])   1)) ]);
```
```   202
```
```   203 (*Commutative law for multiplication*)
```
```   204 qed_goal "mult_commute" Arith.thy
```
```   205     "[| a:N;  b:N |] ==> a #* b = b #* a : N"
```
```   206  (fn prems=>
```
```   207   [ (NE_tac "a" 1),
```
```   208     (hyp_arith_rew_tac (prems @ [mult_0_right, mult_succ_right])) ]);
```
```   209
```
```   210 (*addition distributes over multiplication*)
```
```   211 qed_goal "add_mult_distrib" Arith.thy
```
```   212     "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
```
```   213  (fn prems=>
```
```   214   [ (NE_tac "a" 1),
```
```   215 (*swap round the associative law of addition*)
```
```   216     (hyp_arith_rew_tac (prems @ [add_assoc RS sym_elem])) ]);
```
```   217
```
```   218
```
```   219 (*Associative law for multiplication*)
```
```   220 qed_goal "mult_assoc" Arith.thy
```
```   221     "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N"
```
```   222  (fn prems=>
```
```   223   [ (NE_tac "a" 1),
```
```   224     (hyp_arith_rew_tac (prems @ [add_mult_distrib])) ]);
```
```   225
```
```   226
```
```   227 (************
```
```   228   Difference
```
```   229  ************
```
```   230
```
```   231 Difference on natural numbers, without negative numbers
```
```   232   a - b = 0  iff  a<=b    a - b = succ(c) iff a>b   *)
```
```   233
```
```   234 qed_goal "diff_self_eq_0" Arith.thy
```
```   235     "a:N ==> a - a = 0 : N"
```
```   236  (fn prems=>
```
```   237   [ (NE_tac "a" 1),
```
```   238     (hyp_arith_rew_tac prems) ]);
```
```   239
```
```   240
```
```   241 (*  [| c : N; 0 : N; c : N |] ==> c #+ 0 = c : N  *)
```
```   242 val add_0_right = addC0 RSN (3, add_commute RS trans_elem);
```
```   243
```
```   244 (*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x.
```
```   245   An example of induction over a quantified formula (a product).
```
```   246   Uses rewriting with a quantified, implicative inductive hypothesis.*)
```
```   247 val prems =
```
```   248 goal Arith.thy
```
```   249     "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)";
```
```   250 by (NE_tac "b" 1);
```
```   251 (*strip one "universal quantifier" but not the "implication"*)
```
```   252 by (resolve_tac intr_rls 3);
```
```   253 (*case analysis on x in
```
```   254     (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
```
```   255 by (NE_tac "x" 4 THEN assume_tac 4);
```
```   256 (*Prepare for simplification of types -- the antecedent succ(u)<=x *)
```
```   257 by (rtac replace_type 5);
```
```   258 by (rtac replace_type 4);
```
```   259 by (arith_rew_tac prems);
```
```   260 (*Solves first 0 goal, simplifies others.  Two sugbgoals remain.
```
```   261   Both follow by rewriting, (2) using quantified induction hyp*)
```
```   262 by (intr_tac[]);  (*strips remaining PRODs*)
```
```   263 by (hyp_arith_rew_tac (prems@[add_0_right]));
```
```   264 by (assume_tac 1);
```
```   265 qed "add_diff_inverse_lemma";
```
```   266
```
```   267
```
```   268 (*Version of above with premise   b-a=0   i.e.    a >= b.
```
```   269   Using ProdE does not work -- for ?B(?a) is ambiguous.
```
```   270   Instead, add_diff_inverse_lemma states the desired induction scheme;
```
```   271     the use of RS below instantiates Vars in ProdE automatically. *)
```
```   272 val prems =
```
```   273 goal Arith.thy "[| a:N;  b:N;  b-a = 0 : N |] ==> b #+ (a-b) = a : N";
```
```   274 by (rtac EqE 1);
```
```   275 by (resolve_tac [ add_diff_inverse_lemma RS ProdE RS ProdE ] 1);
```
```   276 by (REPEAT (resolve_tac (prems@[EqI]) 1));
```
```   277 qed "add_diff_inverse";
```
```   278
```
```   279
```
```   280 (********************
```
```   281   Absolute difference
```
```   282  ********************)
```
```   283
```
```   284 (*typing of absolute difference: short and long versions*)
```
```   285
```
```   286 qed_goalw "absdiff_typing" Arith.thy arith_defs
```
```   287     "[| a:N;  b:N |] ==> a |-| b : N"
```
```   288  (fn prems=> [ (typechk_tac prems) ]);
```
```   289
```
```   290 qed_goalw "absdiff_typingL" Arith.thy arith_defs
```
```   291     "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N"
```
```   292  (fn prems=> [ (equal_tac prems) ]);
```
```   293
```
```   294 qed_goalw "absdiff_self_eq_0" Arith.thy [absdiff_def]
```
```   295     "a:N ==> a |-| a = 0 : N"
```
```   296  (fn prems=>
```
```   297   [ (arith_rew_tac (prems@[diff_self_eq_0])) ]);
```
```   298
```
```   299 qed_goalw "absdiffC0" Arith.thy [absdiff_def]
```
```   300     "a:N ==> 0 |-| a = a : N"
```
```   301  (fn prems=>
```
```   302   [ (hyp_arith_rew_tac prems) ]);
```
```   303
```
```   304
```
```   305 qed_goalw "absdiff_succ_succ" Arith.thy [absdiff_def]
```
```   306     "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N"
```
```   307  (fn prems=>
```
```   308   [ (hyp_arith_rew_tac prems) ]);
```
```   309
```
```   310 (*Note how easy using commutative laws can be?  ...not always... *)
```
```   311 val prems = goalw Arith.thy [absdiff_def]
```
```   312     "[| a:N;  b:N |] ==> a |-| b = b |-| a : N";
```
```   313 by (rtac add_commute 1);
```
```   314 by (typechk_tac ([diff_typing]@prems));
```
```   315 qed "absdiff_commute";
```
```   316
```
```   317 (*If a+b=0 then a=0.   Surprisingly tedious*)
```
```   318 val prems =
```
```   319 goal Arith.thy "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)";
```
```   320 by (NE_tac "a" 1);
```
```   321 by (rtac replace_type 3);
```
```   322 by (arith_rew_tac prems);
```
```   323 by (intr_tac[]);  (*strips remaining PRODs*)
```
```   324 by (resolve_tac [ zero_ne_succ RS FE ] 2);
```
```   325 by (etac (EqE RS sym_elem) 3);
```
```   326 by (typechk_tac ([add_typing] @prems));
```
```   327 qed "add_eq0_lemma";
```
```   328
```
```   329 (*Version of above with the premise  a+b=0.
```
```   330   Again, resolution instantiates variables in ProdE *)
```
```   331 val prems =
```
```   332 goal Arith.thy "[| a:N;  b:N;  a #+ b = 0 : N |] ==> a = 0 : N";
```
```   333 by (rtac EqE 1);
```
```   334 by (resolve_tac [add_eq0_lemma RS ProdE] 1);
```
```   335 by (rtac EqI 3);
```
```   336 by (ALLGOALS (resolve_tac prems));
```
```   337 qed "add_eq0";
```
```   338
```
```   339 (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
```
```   340 val prems = goalw Arith.thy [absdiff_def]
```
```   341     "[| a:N;  b:N;  a |-| b = 0 : N |] ==> \
```
```   342 \    ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)";
```
```   343 by (intr_tac[]);
```
```   344 by eqintr_tac;
```
```   345 by (rtac add_eq0 2);
```
```   346 by (rtac add_eq0 1);
```
```   347 by (resolve_tac [add_commute RS trans_elem] 6);
```
```   348 by (typechk_tac (diff_typing::prems));
```
```   349 qed "absdiff_eq0_lem";
```
```   350
```
```   351 (*if  a |-| b = 0  then  a = b
```
```   352   proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
```
```   353 val prems =
```
```   354 goal Arith.thy "[| a |-| b = 0 : N;  a:N;  b:N |] ==> a = b : N";
```
```   355 by (rtac EqE 1);
```
```   356 by (resolve_tac [absdiff_eq0_lem RS SumE] 1);
```
```   357 by (TRYALL (resolve_tac prems));
```
```   358 by eqintr_tac;
```
```   359 by (resolve_tac [add_diff_inverse RS sym_elem RS trans_elem] 1);
```
```   360 by (rtac EqE 3  THEN  assume_tac 3);
```
```   361 by (hyp_arith_rew_tac (prems@[add_0_right]));
```
```   362 qed "absdiff_eq0";
```
```   363
```
```   364 (***********************
```
```   365   Remainder and Quotient
```
```   366  ***********************)
```
```   367
```
```   368 (*typing of remainder: short and long versions*)
```
```   369
```
```   370 qed_goalw "mod_typing" Arith.thy [mod_def]
```
```   371     "[| a:N;  b:N |] ==> a mod b : N"
```
```   372  (fn prems=>
```
```   373   [ (typechk_tac (absdiff_typing::prems)) ]);
```
```   374
```
```   375 qed_goalw "mod_typingL" Arith.thy [mod_def]
```
```   376     "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N"
```
```   377  (fn prems=>
```
```   378   [ (equal_tac (prems@[absdiff_typingL])) ]);
```
```   379
```
```   380
```
```   381 (*computation for  mod : 0 and successor cases*)
```
```   382
```
```   383 qed_goalw "modC0" Arith.thy [mod_def] "b:N ==> 0 mod b = 0 : N"
```
```   384  (fn prems=>
```
```   385   [ (rew_tac(absdiff_typing::prems)) ]);
```
```   386
```
```   387 qed_goalw "modC_succ" Arith.thy [mod_def]
```
```   388 "[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y.succ(a mod b)) : N"
```
```   389  (fn prems=>
```
```   390   [ (rew_tac(absdiff_typing::prems)) ]);
```
```   391
```
```   392
```
```   393 (*typing of quotient: short and long versions*)
```
```   394
```
```   395 qed_goalw "div_typing" Arith.thy [div_def] "[| a:N;  b:N |] ==> a div b : N"
```
```   396  (fn prems=>
```
```   397   [ (typechk_tac ([absdiff_typing,mod_typing]@prems)) ]);
```
```   398
```
```   399 qed_goalw "div_typingL" Arith.thy [div_def]
```
```   400    "[| a=c:N;  b=d:N |] ==> a div b = c div d : N"
```
```   401  (fn prems=>
```
```   402   [ (equal_tac (prems @ [absdiff_typingL, mod_typingL])) ]);
```
```   403
```
```   404 val div_typing_rls = [mod_typing, div_typing, absdiff_typing];
```
```   405
```
```   406
```
```   407 (*computation for quotient: 0 and successor cases*)
```
```   408
```
```   409 qed_goalw "divC0" Arith.thy [div_def] "b:N ==> 0 div b = 0 : N"
```
```   410  (fn prems=>
```
```   411   [ (rew_tac([mod_typing, absdiff_typing] @ prems)) ]);
```
```   412
```
```   413 val divC_succ =
```
```   414 prove_goalw Arith.thy [div_def] "[| a:N;  b:N |] ==> succ(a) div b = \
```
```   415 \    rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"
```
```   416  (fn prems=>
```
```   417   [ (rew_tac([mod_typing]@prems)) ]);
```
```   418
```
```   419
```
```   420 (*Version of above with same condition as the  mod  one*)
```
```   421 qed_goal "divC_succ2" Arith.thy
```
```   422     "[| a:N;  b:N |] ==> \
```
```   423 \    succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
```
```   424  (fn prems=>
```
```   425   [ (resolve_tac [ divC_succ RS trans_elem ] 1),
```
```   426     (rew_tac(div_typing_rls @ prems @ [modC_succ])),
```
```   427     (NE_tac "succ(a mod b)|-|b" 1),
```
```   428     (rew_tac ([mod_typing, div_typing, absdiff_typing] @prems)) ]);
```
```   429
```
```   430 (*for case analysis on whether a number is 0 or a successor*)
```
```   431 qed_goal "iszero_decidable" Arith.thy
```
```   432     "a:N ==> rec(a, inl(eq), %ka kb.inr(<ka, eq>)) : \
```
```   433 \                     Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
```
```   434  (fn prems=>
```
```   435   [ (NE_tac "a" 1),
```
```   436     (rtac PlusI_inr 3),
```
```   437     (rtac PlusI_inl 2),
```
```   438     eqintr_tac,
```
```   439     (equal_tac prems) ]);
```
```   440
```
```   441 (*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
```
```   442 val prems =
```
```   443 goal Arith.thy "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N";
```
```   444 by (NE_tac "a" 1);
```
```   445 by (arith_rew_tac (div_typing_rls@prems@[modC0,modC_succ,divC0,divC_succ2]));
```
```   446 by (rtac EqE 1);
```
```   447 (*case analysis on   succ(u mod b)|-|b  *)
```
```   448 by (res_inst_tac [("a1", "succ(u mod b) |-| b")]
```
```   449                  (iszero_decidable RS PlusE) 1);
```
```   450 by (etac SumE 3);
```
```   451 by (hyp_arith_rew_tac (prems @ div_typing_rls @
```
```   452         [modC0,modC_succ, divC0, divC_succ2]));
```
```   453 (*Replace one occurence of  b  by succ(u mod b).  Clumsy!*)
```
```   454 by (resolve_tac [ add_typingL RS trans_elem ] 1);
```
```   455 by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1);
```
```   456 by (rtac refl_elem 3);
```
```   457 by (hyp_arith_rew_tac (prems @ div_typing_rls));
```
```   458 qed "mod_div_equality";
```
```   459
```
```   460 writeln"Reached end of file.";
```