author  wenzelm 
Thu, 23 Jul 2015 14:25:05 +0200  
changeset 60770  240563fbf41d 
parent 59498  50b60f501b05 
child 61337  4645502c3c64 
permissions  rwrr 
17441  1 
(* Title: CTT/Arith.thy 
1474  2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  3 
Copyright 1991 University of Cambridge 
4 
*) 

5 

60770  6 
section \<open>Elementary arithmetic\<close> 
17441  7 

8 
theory Arith 

9 
imports Bool 

10 
begin 

0  11 

60770  12 
subsection \<open>Arithmetic operators and their definitions\<close> 
17441  13 

19762  14 
definition 
58977  15 
add :: "[i,i]\<Rightarrow>i" (infixr "#+" 65) where 
16 
"a#+b == rec(a, b, \<lambda>u v. succ(v))" 

0  17 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

18 
definition 
58977  19 
diff :: "[i,i]\<Rightarrow>i" (infixr "" 65) where 
20 
"ab == rec(b, a, \<lambda>u v. rec(v, 0, \<lambda>x y. x))" 

19762  21 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

22 
definition 
58977  23 
absdiff :: "[i,i]\<Rightarrow>i" (infixr "" 65) where 
19762  24 
"ab == (ab) #+ (ba)" 
25 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

26 
definition 
58977  27 
mult :: "[i,i]\<Rightarrow>i" (infixr "#*" 70) where 
28 
"a#*b == rec(a, 0, \<lambda>u v. b #+ v)" 

10467
e6e7205e9e91
xsymbol support for Pi, Sigma, >, : (membership)
paulson
parents:
3837
diff
changeset

29 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

30 
definition 
58977  31 
mod :: "[i,i]\<Rightarrow>i" (infixr "mod" 70) where 
19762  32 
"a mod b == rec(a, 0, %u v. rec(succ(v)  b, 0, %x y. succ(v)))" 
33 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

34 
definition 
58977  35 
div :: "[i,i]\<Rightarrow>i" (infixr "div" 70) where 
36 
"a div b == rec(a, 0, \<lambda>u v. rec(succ(u) mod b, succ(v), \<lambda>x y. v))" 

19762  37 

10467
e6e7205e9e91
xsymbol support for Pi, Sigma, >, : (membership)
paulson
parents:
3837
diff
changeset

38 

21210  39 
notation (xsymbols) 
19762  40 
mult (infixr "#\<times>" 70) 
41 

21210  42 
notation (HTML output) 
19762  43 
mult (infixr "#\<times>" 70) 
44 

17441  45 

19761  46 
lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def 
47 

48 

60770  49 
subsection \<open>Proofs about elementary arithmetic: addition, multiplication, etc.\<close> 
19761  50 

51 
(** Addition *) 

52 

53 
(*typing of add: short and long versions*) 

54 

58977  55 
lemma add_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #+ b : N" 
19761  56 
apply (unfold arith_defs) 
58972  57 
apply typechk 
19761  58 
done 
59 

58977  60 
lemma add_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #+ b = c #+ d : N" 
19761  61 
apply (unfold arith_defs) 
58972  62 
apply equal 
19761  63 
done 
64 

65 

66 
(*computation for add: 0 and successor cases*) 

67 

58977  68 
lemma addC0: "b:N \<Longrightarrow> 0 #+ b = b : N" 
19761  69 
apply (unfold arith_defs) 
58972  70 
apply rew 
19761  71 
done 
72 

58977  73 
lemma addC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #+ b = succ(a #+ b) : N" 
19761  74 
apply (unfold arith_defs) 
58972  75 
apply rew 
19761  76 
done 
77 

78 

79 
(** Multiplication *) 

80 

81 
(*typing of mult: short and long versions*) 

82 

58977  83 
lemma mult_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* b : N" 
19761  84 
apply (unfold arith_defs) 
58972  85 
apply (typechk add_typing) 
19761  86 
done 
87 

58977  88 
lemma mult_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #* b = c #* d : N" 
19761  89 
apply (unfold arith_defs) 
58972  90 
apply (equal add_typingL) 
19761  91 
done 
92 

93 
(*computation for mult: 0 and successor cases*) 

94 

58977  95 
lemma multC0: "b:N \<Longrightarrow> 0 #* b = 0 : N" 
19761  96 
apply (unfold arith_defs) 
58972  97 
apply rew 
19761  98 
done 
99 

58977  100 
lemma multC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #* b = b #+ (a #* b) : N" 
19761  101 
apply (unfold arith_defs) 
58972  102 
apply rew 
19761  103 
done 
104 

105 

106 
(** Difference *) 

107 

108 
(*typing of difference*) 

109 

58977  110 
lemma diff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a  b : N" 
19761  111 
apply (unfold arith_defs) 
58972  112 
apply typechk 
19761  113 
done 
114 

58977  115 
lemma diff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a  b = c  d : N" 
19761  116 
apply (unfold arith_defs) 
58972  117 
apply equal 
19761  118 
done 
119 

120 

121 
(*computation for difference: 0 and successor cases*) 

122 

58977  123 
lemma diffC0: "a:N \<Longrightarrow> a  0 = a : N" 
19761  124 
apply (unfold arith_defs) 
58972  125 
apply rew 
19761  126 
done 
127 

58977  128 
(*Note: rec(a, 0, \<lambda>z w.z) is pred(a). *) 
19761  129 

58977  130 
lemma diff_0_eq_0: "b:N \<Longrightarrow> 0  b = 0 : N" 
19761  131 
apply (unfold arith_defs) 
58972  132 
apply (NE b) 
133 
apply hyp_rew 

19761  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) *) 

58977  139 
lemma diff_succ_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a)  succ(b) = a  b : N" 
19761  140 
apply (unfold arith_defs) 
58972  141 
apply hyp_rew 
142 
apply (NE b) 

143 
apply hyp_rew 

19761  144 
done 
145 

146 

60770  147 
subsection \<open>Simplification\<close> 
19761  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 

60770  158 
ML \<open> 
19761  159 

160 
structure Arith_simp_data: TSIMP_DATA = 

161 
struct 

39159  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}) 

19761  170 
end 
171 

172 
structure Arith_simp = TSimpFun (Arith_simp_data) 

173 

39159  174 
local val congr_rls = @{thms congr_rls} in 
19761  175 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

176 
fun arith_rew_tac ctxt prems = make_rew_tac ctxt 
58976  177 
(Arith_simp.norm_tac ctxt (congr_rls, prems)) 
19761  178 

58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

179 
fun hyp_arith_rew_tac ctxt prems = make_rew_tac ctxt 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58977
diff
changeset

180 
(Arith_simp.cond_norm_tac ctxt (prove_cond_tac ctxt, congr_rls, prems)) 
17441  181 

0  182 
end 
60770  183 
\<close> 
19761  184 

60770  185 
method_setup arith_rew = \<open> 
58972  186 
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (arith_rew_tac ctxt ths)) 
60770  187 
\<close> 
58972  188 

60770  189 
method_setup hyp_arith_rew = \<open> 
58972  190 
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_arith_rew_tac ctxt ths)) 
60770  191 
\<close> 
58972  192 

19761  193 

60770  194 
subsection \<open>Addition\<close> 
19761  195 

196 
(*Associative law for addition*) 

58977  197 
lemma add_assoc: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #+ b) #+ c = a #+ (b #+ c) : N" 
58972  198 
apply (NE a) 
199 
apply hyp_arith_rew 

19761  200 
done 
201 

202 

203 
(*Commutative law for addition. Can be proved using three inductions. 

204 
Must simplify after first induction! Orientation of rewrites is delicate*) 

58977  205 
lemma add_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #+ b = b #+ a : N" 
58972  206 
apply (NE a) 
207 
apply hyp_arith_rew 

19761  208 
apply (rule sym_elem) 
58972  209 
prefer 2 
210 
apply (NE b) 

211 
prefer 4 

212 
apply (NE b) 

213 
apply hyp_arith_rew 

19761  214 
done 
215 

216 

60770  217 
subsection \<open>Multiplication\<close> 
19761  218 

219 
(*right annihilation in product*) 

58977  220 
lemma mult_0_right: "a:N \<Longrightarrow> a #* 0 = 0 : N" 
58972  221 
apply (NE a) 
222 
apply hyp_arith_rew 

19761  223 
done 
224 

225 
(*right successor law for multiplication*) 

58977  226 
lemma mult_succ_right: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* succ(b) = a #+ (a #* b) : N" 
58972  227 
apply (NE a) 
228 
apply (hyp_arith_rew add_assoc [THEN sym_elem]) 

19761  229 
apply (assumption  rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+ 
230 
done 

231 

232 
(*Commutative law for multiplication*) 

58977  233 
lemma mult_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* b = b #* a : N" 
58972  234 
apply (NE a) 
235 
apply (hyp_arith_rew mult_0_right mult_succ_right) 

19761  236 
done 
237 

238 
(*addition distributes over multiplication*) 

58977  239 
lemma add_mult_distrib: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #+ b) #* c = (a #* c) #+ (b #* c) : N" 
58972  240 
apply (NE a) 
241 
apply (hyp_arith_rew add_assoc [THEN sym_elem]) 

19761  242 
done 
243 

244 
(*Associative law for multiplication*) 

58977  245 
lemma mult_assoc: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #* b) #* c = a #* (b #* c) : N" 
58972  246 
apply (NE a) 
247 
apply (hyp_arith_rew add_mult_distrib) 

19761  248 
done 
249 

250 

60770  251 
subsection \<open>Difference\<close> 
19761  252 

60770  253 
text \<open> 
19761  254 
Difference on natural numbers, without negative numbers 
60770  255 
a  b = 0 iff a<=b a  b = succ(c) iff a>b\<close> 
19761  256 

58977  257 
lemma diff_self_eq_0: "a:N \<Longrightarrow> a  a = 0 : N" 
58972  258 
apply (NE a) 
259 
apply hyp_arith_rew 

19761  260 
done 
261 

262 

58977  263 
lemma add_0_right: "\<lbrakk>c : N; 0 : N; c : N\<rbrakk> \<Longrightarrow> c #+ 0 = c : N" 
19761  264 
by (rule addC0 [THEN [3] add_commute [THEN trans_elem]]) 
265 

266 
(*Addition is the inverse of subtraction: if b<=x then b#+(xb) = x. 

267 
An example of induction over a quantified formula (a product). 

268 
Uses rewriting with a quantified, implicative inductive hypothesis.*) 

36319  269 
schematic_lemma add_diff_inverse_lemma: 
58977  270 
"b:N \<Longrightarrow> ?a : PROD x:N. Eq(N, bx, 0) > Eq(N, b #+ (xb), x)" 
58972  271 
apply (NE b) 
19761  272 
(*strip one "universal quantifier" but not the "implication"*) 
273 
apply (rule_tac [3] intr_rls) 

274 
(*case analysis on x in 

275 
(succ(u) <= x) > (succ(u)#+(xsucc(u)) = x) *) 

58972  276 
prefer 4 
277 
apply (NE x) 

278 
apply assumption 

19761  279 
(*Prepare for simplification of types  the antecedent succ(u)<=x *) 
58972  280 
apply (rule_tac [2] replace_type) 
281 
apply (rule_tac [1] replace_type) 

282 
apply arith_rew 

19761  283 
(*Solves first 0 goal, simplifies others. Two sugbgoals remain. 
284 
Both follow by rewriting, (2) using quantified induction hyp*) 

58972  285 
apply intr (*strips remaining PRODs*) 
286 
apply (hyp_arith_rew add_0_right) 

19761  287 
apply assumption 
288 
done 

289 

290 

291 
(*Version of above with premise ba=0 i.e. a >= b. 

292 
Using ProdE does not work  for ?B(?a) is ambiguous. 

293 
Instead, add_diff_inverse_lemma states the desired induction scheme 

294 
the use of RS below instantiates Vars in ProdE automatically. *) 

58977  295 
lemma add_diff_inverse: "\<lbrakk>a:N; b:N; b  a = 0 : N\<rbrakk> \<Longrightarrow> b #+ (ab) = a : N" 
19761  296 
apply (rule EqE) 
297 
apply (rule add_diff_inverse_lemma [THEN ProdE, THEN ProdE]) 

298 
apply (assumption  rule EqI)+ 

299 
done 

300 

301 

60770  302 
subsection \<open>Absolute difference\<close> 
19761  303 

304 
(*typing of absolute difference: short and long versions*) 

305 

58977  306 
lemma absdiff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a  b : N" 
19761  307 
apply (unfold arith_defs) 
58972  308 
apply typechk 
19761  309 
done 
310 

58977  311 
lemma absdiff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a  b = c  d : N" 
19761  312 
apply (unfold arith_defs) 
58972  313 
apply equal 
19761  314 
done 
315 

58977  316 
lemma absdiff_self_eq_0: "a:N \<Longrightarrow> a  a = 0 : N" 
19761  317 
apply (unfold absdiff_def) 
58972  318 
apply (arith_rew diff_self_eq_0) 
19761  319 
done 
320 

58977  321 
lemma absdiffC0: "a:N \<Longrightarrow> 0  a = a : N" 
19761  322 
apply (unfold absdiff_def) 
58972  323 
apply hyp_arith_rew 
19761  324 
done 
325 

326 

58977  327 
lemma absdiff_succ_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a)  succ(b) = a  b : N" 
19761  328 
apply (unfold absdiff_def) 
58972  329 
apply hyp_arith_rew 
19761  330 
done 
331 

332 
(*Note how easy using commutative laws can be? ...not always... *) 

58977  333 
lemma absdiff_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a  b = b  a : N" 
19761  334 
apply (unfold absdiff_def) 
335 
apply (rule add_commute) 

58972  336 
apply (typechk diff_typing) 
19761  337 
done 
338 

339 
(*If a+b=0 then a=0. Surprisingly tedious*) 

58977  340 
schematic_lemma add_eq0_lemma: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)" 
58972  341 
apply (NE a) 
19761  342 
apply (rule_tac [3] replace_type) 
58972  343 
apply arith_rew 
344 
apply intr (*strips remaining PRODs*) 

19761  345 
apply (rule_tac [2] zero_ne_succ [THEN FE]) 
346 
apply (erule_tac [3] EqE [THEN sym_elem]) 

58972  347 
apply (typechk add_typing) 
19761  348 
done 
349 

350 
(*Version of above with the premise a+b=0. 

351 
Again, resolution instantiates variables in ProdE *) 

58977  352 
lemma add_eq0: "\<lbrakk>a:N; b:N; a #+ b = 0 : N\<rbrakk> \<Longrightarrow> a = 0 : N" 
19761  353 
apply (rule EqE) 
354 
apply (rule add_eq0_lemma [THEN ProdE]) 

355 
apply (rule_tac [3] EqI) 

58972  356 
apply typechk 
19761  357 
done 
358 

359 
(*Here is a lemma to infer ab=0 and ba=0 from ab=0, below. *) 

36319  360 
schematic_lemma absdiff_eq0_lem: 
58977  361 
"\<lbrakk>a:N; b:N; a  b = 0 : N\<rbrakk> \<Longrightarrow> ?a : SUM v: Eq(N, ab, 0) . Eq(N, ba, 0)" 
19761  362 
apply (unfold absdiff_def) 
58972  363 
apply intr 
364 
apply eqintr 

19761  365 
apply (rule_tac [2] add_eq0) 
366 
apply (rule add_eq0) 

367 
apply (rule_tac [6] add_commute [THEN trans_elem]) 

58972  368 
apply (typechk diff_typing) 
19761  369 
done 
370 

371 
(*if a  b = 0 then a = b 

372 
proof: ab=0 and ba=0, so b = a+(ba) = a+0 = a*) 

58977  373 
lemma absdiff_eq0: "\<lbrakk>a  b = 0 : N; a:N; b:N\<rbrakk> \<Longrightarrow> a = b : N" 
19761  374 
apply (rule EqE) 
375 
apply (rule absdiff_eq0_lem [THEN SumE]) 

58972  376 
apply eqintr 
19761  377 
apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem]) 
58972  378 
apply (erule_tac [3] EqE) 
379 
apply (hyp_arith_rew add_0_right) 

19761  380 
done 
381 

382 

60770  383 
subsection \<open>Remainder and Quotient\<close> 
19761  384 

385 
(*typing of remainder: short and long versions*) 

386 

58977  387 
lemma mod_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a mod b : N" 
19761  388 
apply (unfold mod_def) 
58972  389 
apply (typechk absdiff_typing) 
19761  390 
done 
391 

58977  392 
lemma mod_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a mod b = c mod d : N" 
19761  393 
apply (unfold mod_def) 
58972  394 
apply (equal absdiff_typingL) 
19761  395 
done 
396 

397 

398 
(*computation for mod : 0 and successor cases*) 

399 

58977  400 
lemma modC0: "b:N \<Longrightarrow> 0 mod b = 0 : N" 
19761  401 
apply (unfold mod_def) 
58972  402 
apply (rew absdiff_typing) 
19761  403 
done 
404 

58977  405 
lemma modC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> 
406 
succ(a) mod b = rec(succ(a mod b)  b, 0, \<lambda>x y. succ(a mod b)) : N" 

19761  407 
apply (unfold mod_def) 
58972  408 
apply (rew absdiff_typing) 
19761  409 
done 
410 

411 

412 
(*typing of quotient: short and long versions*) 

413 

58977  414 
lemma div_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a div b : N" 
19761  415 
apply (unfold div_def) 
58972  416 
apply (typechk absdiff_typing mod_typing) 
19761  417 
done 
418 

58977  419 
lemma div_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a div b = c div d : N" 
19761  420 
apply (unfold div_def) 
58972  421 
apply (equal absdiff_typingL mod_typingL) 
19761  422 
done 
423 

424 
lemmas div_typing_rls = mod_typing div_typing absdiff_typing 

425 

426 

427 
(*computation for quotient: 0 and successor cases*) 

428 

58977  429 
lemma divC0: "b:N \<Longrightarrow> 0 div b = 0 : N" 
19761  430 
apply (unfold div_def) 
58972  431 
apply (rew mod_typing absdiff_typing) 
19761  432 
done 
433 

58977  434 
lemma divC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> 
435 
succ(a) div b = rec(succ(a) mod b, succ(a div b), \<lambda>x y. a div b) : N" 

19761  436 
apply (unfold div_def) 
58972  437 
apply (rew mod_typing) 
19761  438 
done 
439 

440 

441 
(*Version of above with same condition as the mod one*) 

58977  442 
lemma divC_succ2: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> 
443 
succ(a) div b =rec(succ(a mod b)  b, succ(a div b), \<lambda>x y. a div b) : N" 

19761  444 
apply (rule divC_succ [THEN trans_elem]) 
58972  445 
apply (rew div_typing_rls modC_succ) 
446 
apply (NE "succ (a mod b) b") 

447 
apply (rew mod_typing div_typing absdiff_typing) 

19761  448 
done 
449 

450 
(*for case analysis on whether a number is 0 or a successor*) 

58977  451 
lemma iszero_decidable: "a:N \<Longrightarrow> rec(a, inl(eq), \<lambda>ka kb. inr(<ka, eq>)) : 
19761  452 
Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))" 
58972  453 
apply (NE a) 
19761  454 
apply (rule_tac [3] PlusI_inr) 
455 
apply (rule_tac [2] PlusI_inl) 

58972  456 
apply eqintr 
457 
apply equal 

19761  458 
done 
459 

460 
(*Main Result. Holds when b is 0 since a mod 0 = a and a div 0 = 0 *) 

58977  461 
lemma mod_div_equality: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a mod b #+ (a div b) #* b = a : N" 
58972  462 
apply (NE a) 
463 
apply (arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2) 

19761  464 
apply (rule EqE) 
465 
(*case analysis on succ(u mod b)b *) 

466 
apply (rule_tac a1 = "succ (u mod b)  b" in iszero_decidable [THEN PlusE]) 

467 
apply (erule_tac [3] SumE) 

58972  468 
apply (hyp_arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2) 
58318  469 
(*Replace one occurrence of b by succ(u mod b). Clumsy!*) 
19761  470 
apply (rule add_typingL [THEN trans_elem]) 
471 
apply (erule EqE [THEN absdiff_eq0, THEN sym_elem]) 

472 
apply (rule_tac [3] refl_elem) 

58972  473 
apply (hyp_arith_rew div_typing_rls) 
19761  474 
done 
475 

476 
end 