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