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