author  wenzelm 
Fri, 01 Jan 2016 16:40:47 +0100  
changeset 62028  2ecee4679f99 
parent 61391  2332d9be352b 
child 63505  42e1dece537a 
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 
61391  16 
"a#+b \<equiv> 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 
61391  20 
"ab \<equiv> 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 
61391  24 
"ab \<equiv> (ab) #+ (ba)" 
19762  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 
61391  28 
"a#*b \<equiv> 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 
61391  32 
"a mod b \<equiv> rec(a, 0, \<lambda>u v. rec(succ(v)  b, 0, \<lambda>x y. succ(v)))" 
19762  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 
61391  36 
"a div b \<equiv> rec(a, 0, \<lambda>u v. rec(succ(u) mod b, succ(v), \<lambda>x y. v))" 
19762  37 

17441  38 

19761  39 
lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def 
40 

41 

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

44 
(** Addition *) 

45 

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

47 

58977  48 
lemma add_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #+ b : N" 
19761  49 
apply (unfold arith_defs) 
58972  50 
apply typechk 
19761  51 
done 
52 

58977  53 
lemma add_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #+ b = c #+ d : N" 
19761  54 
apply (unfold arith_defs) 
58972  55 
apply equal 
19761  56 
done 
57 

58 

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

60 

58977  61 
lemma addC0: "b:N \<Longrightarrow> 0 #+ b = b : N" 
19761  62 
apply (unfold arith_defs) 
58972  63 
apply rew 
19761  64 
done 
65 

58977  66 
lemma addC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #+ b = succ(a #+ b) : N" 
19761  67 
apply (unfold arith_defs) 
58972  68 
apply rew 
19761  69 
done 
70 

71 

72 
(** Multiplication *) 

73 

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

75 

58977  76 
lemma mult_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* b : N" 
19761  77 
apply (unfold arith_defs) 
58972  78 
apply (typechk add_typing) 
19761  79 
done 
80 

58977  81 
lemma mult_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #* b = c #* d : N" 
19761  82 
apply (unfold arith_defs) 
58972  83 
apply (equal add_typingL) 
19761  84 
done 
85 

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

87 

58977  88 
lemma multC0: "b:N \<Longrightarrow> 0 #* b = 0 : N" 
19761  89 
apply (unfold arith_defs) 
58972  90 
apply rew 
19761  91 
done 
92 

58977  93 
lemma multC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #* b = b #+ (a #* b) : N" 
19761  94 
apply (unfold arith_defs) 
58972  95 
apply rew 
19761  96 
done 
97 

98 

99 
(** Difference *) 

100 

101 
(*typing of difference*) 

102 

58977  103 
lemma diff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a  b : N" 
19761  104 
apply (unfold arith_defs) 
58972  105 
apply typechk 
19761  106 
done 
107 

58977  108 
lemma diff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a  b = c  d : N" 
19761  109 
apply (unfold arith_defs) 
58972  110 
apply equal 
19761  111 
done 
112 

113 

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

115 

58977  116 
lemma diffC0: "a:N \<Longrightarrow> a  0 = a : N" 
19761  117 
apply (unfold arith_defs) 
58972  118 
apply rew 
19761  119 
done 
120 

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

58977  123 
lemma diff_0_eq_0: "b:N \<Longrightarrow> 0  b = 0 : N" 
19761  124 
apply (unfold arith_defs) 
58972  125 
apply (NE b) 
126 
apply hyp_rew 

19761  127 
done 
128 

129 

130 
(*Essential to simplify FIRST!! (Else we get a critical pair) 

131 
succ(a)  succ(b) rewrites to pred(succ(a)  b) *) 

58977  132 
lemma diff_succ_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a)  succ(b) = a  b : N" 
19761  133 
apply (unfold arith_defs) 
58972  134 
apply hyp_rew 
135 
apply (NE b) 

136 
apply hyp_rew 

19761  137 
done 
138 

139 

60770  140 
subsection \<open>Simplification\<close> 
19761  141 

142 
lemmas arith_typing_rls = add_typing mult_typing diff_typing 

143 
and arith_congr_rls = add_typingL mult_typingL diff_typingL 

144 
lemmas congr_rls = arith_congr_rls intrL2_rls elimL_rls 

145 

146 
lemmas arithC_rls = 

147 
addC0 addC_succ 

148 
multC0 multC_succ 

149 
diffC0 diff_0_eq_0 diff_succ_succ 

150 

60770  151 
ML \<open> 
19761  152 

153 
structure Arith_simp_data: TSIMP_DATA = 

154 
struct 

39159  155 
val refl = @{thm refl_elem} 
156 
val sym = @{thm sym_elem} 

157 
val trans = @{thm trans_elem} 

158 
val refl_red = @{thm refl_red} 

159 
val trans_red = @{thm trans_red} 

160 
val red_if_equal = @{thm red_if_equal} 

161 
val default_rls = @{thms arithC_rls} @ @{thms comp_rls} 

162 
val routine_tac = routine_tac (@{thms arith_typing_rls} @ @{thms routine_rls}) 

19761  163 
end 
164 

165 
structure Arith_simp = TSimpFun (Arith_simp_data) 

166 

39159  167 
local val congr_rls = @{thms congr_rls} in 
19761  168 

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

169 
fun arith_rew_tac ctxt prems = make_rew_tac ctxt 
58976  170 
(Arith_simp.norm_tac ctxt (congr_rls, prems)) 
19761  171 

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

172 
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

173 
(Arith_simp.cond_norm_tac ctxt (prove_cond_tac ctxt, congr_rls, prems)) 
17441  174 

0  175 
end 
60770  176 
\<close> 
19761  177 

60770  178 
method_setup arith_rew = \<open> 
58972  179 
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (arith_rew_tac ctxt ths)) 
60770  180 
\<close> 
58972  181 

60770  182 
method_setup hyp_arith_rew = \<open> 
58972  183 
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_arith_rew_tac ctxt ths)) 
60770  184 
\<close> 
58972  185 

19761  186 

60770  187 
subsection \<open>Addition\<close> 
19761  188 

189 
(*Associative law for addition*) 

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

19761  193 
done 
194 

195 

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

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

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

19761  201 
apply (rule sym_elem) 
58972  202 
prefer 2 
203 
apply (NE b) 

204 
prefer 4 

205 
apply (NE b) 

206 
apply hyp_arith_rew 

19761  207 
done 
208 

209 

60770  210 
subsection \<open>Multiplication\<close> 
19761  211 

212 
(*right annihilation in product*) 

58977  213 
lemma mult_0_right: "a:N \<Longrightarrow> a #* 0 = 0 : N" 
58972  214 
apply (NE a) 
215 
apply hyp_arith_rew 

19761  216 
done 
217 

218 
(*right successor law for multiplication*) 

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

19761  222 
apply (assumption  rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+ 
223 
done 

224 

225 
(*Commutative law for multiplication*) 

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

19761  229 
done 
230 

231 
(*addition distributes over multiplication*) 

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

19761  235 
done 
236 

237 
(*Associative law for multiplication*) 

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

19761  241 
done 
242 

243 

60770  244 
subsection \<open>Difference\<close> 
19761  245 

60770  246 
text \<open> 
19761  247 
Difference on natural numbers, without negative numbers 
60770  248 
a  b = 0 iff a<=b a  b = succ(c) iff a>b\<close> 
19761  249 

58977  250 
lemma diff_self_eq_0: "a:N \<Longrightarrow> a  a = 0 : N" 
58972  251 
apply (NE a) 
252 
apply hyp_arith_rew 

19761  253 
done 
254 

255 

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

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

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

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

61337  262 
schematic_goal add_diff_inverse_lemma: 
61391  263 
"b:N \<Longrightarrow> ?a : \<Prod>x:N. Eq(N, bx, 0) \<longrightarrow> Eq(N, b #+ (xb), x)" 
58972  264 
apply (NE b) 
19761  265 
(*strip one "universal quantifier" but not the "implication"*) 
266 
apply (rule_tac [3] intr_rls) 

267 
(*case analysis on x in 

61391  268 
(succ(u) <= x) \<longrightarrow> (succ(u)#+(xsucc(u)) = x) *) 
58972  269 
prefer 4 
270 
apply (NE x) 

271 
apply assumption 

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

275 
apply arith_rew 

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

58972  278 
apply intr (*strips remaining PRODs*) 
279 
apply (hyp_arith_rew add_0_right) 

19761  280 
apply assumption 
281 
done 

282 

283 

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

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

286 
Instead, add_diff_inverse_lemma states the desired induction scheme 

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

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

291 
apply (assumption  rule EqI)+ 

292 
done 

293 

294 

60770  295 
subsection \<open>Absolute difference\<close> 
19761  296 

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

298 

58977  299 
lemma absdiff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a  b : N" 
19761  300 
apply (unfold arith_defs) 
58972  301 
apply typechk 
19761  302 
done 
303 

58977  304 
lemma absdiff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a  b = c  d : N" 
19761  305 
apply (unfold arith_defs) 
58972  306 
apply equal 
19761  307 
done 
308 

58977  309 
lemma absdiff_self_eq_0: "a:N \<Longrightarrow> a  a = 0 : N" 
19761  310 
apply (unfold absdiff_def) 
58972  311 
apply (arith_rew diff_self_eq_0) 
19761  312 
done 
313 

58977  314 
lemma absdiffC0: "a:N \<Longrightarrow> 0  a = a : N" 
19761  315 
apply (unfold absdiff_def) 
58972  316 
apply hyp_arith_rew 
19761  317 
done 
318 

319 

58977  320 
lemma absdiff_succ_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a)  succ(b) = a  b : N" 
19761  321 
apply (unfold absdiff_def) 
58972  322 
apply hyp_arith_rew 
19761  323 
done 
324 

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

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

58972  329 
apply (typechk diff_typing) 
19761  330 
done 
331 

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

61391  333 
schematic_goal add_eq0_lemma: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?c : \<Prod>u: Eq(N,a#+b,0) . Eq(N,a,0)" 
58972  334 
apply (NE a) 
19761  335 
apply (rule_tac [3] replace_type) 
58972  336 
apply arith_rew 
337 
apply intr (*strips remaining PRODs*) 

19761  338 
apply (rule_tac [2] zero_ne_succ [THEN FE]) 
339 
apply (erule_tac [3] EqE [THEN sym_elem]) 

58972  340 
apply (typechk add_typing) 
19761  341 
done 
342 

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

344 
Again, resolution instantiates variables in ProdE *) 

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

348 
apply (rule_tac [3] EqI) 

58972  349 
apply typechk 
19761  350 
done 
351 

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

61337  353 
schematic_goal absdiff_eq0_lem: 
61391  354 
"\<lbrakk>a:N; b:N; a  b = 0 : N\<rbrakk> \<Longrightarrow> ?a : \<Sum>v: Eq(N, ab, 0) . Eq(N, ba, 0)" 
19761  355 
apply (unfold absdiff_def) 
58972  356 
apply intr 
357 
apply eqintr 

19761  358 
apply (rule_tac [2] add_eq0) 
359 
apply (rule add_eq0) 

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

58972  361 
apply (typechk diff_typing) 
19761  362 
done 
363 

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

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

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

58972  369 
apply eqintr 
19761  370 
apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem]) 
58972  371 
apply (erule_tac [3] EqE) 
372 
apply (hyp_arith_rew add_0_right) 

19761  373 
done 
374 

375 

60770  376 
subsection \<open>Remainder and Quotient\<close> 
19761  377 

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

379 

58977  380 
lemma mod_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a mod b : N" 
19761  381 
apply (unfold mod_def) 
58972  382 
apply (typechk absdiff_typing) 
19761  383 
done 
384 

58977  385 
lemma mod_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a mod b = c mod d : N" 
19761  386 
apply (unfold mod_def) 
58972  387 
apply (equal absdiff_typingL) 
19761  388 
done 
389 

390 

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

392 

58977  393 
lemma modC0: "b:N \<Longrightarrow> 0 mod b = 0 : N" 
19761  394 
apply (unfold mod_def) 
58972  395 
apply (rew absdiff_typing) 
19761  396 
done 
397 

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

19761  400 
apply (unfold mod_def) 
58972  401 
apply (rew absdiff_typing) 
19761  402 
done 
403 

404 

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

406 

58977  407 
lemma div_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a div b : N" 
19761  408 
apply (unfold div_def) 
58972  409 
apply (typechk absdiff_typing mod_typing) 
19761  410 
done 
411 

58977  412 
lemma div_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a div b = c div d : N" 
19761  413 
apply (unfold div_def) 
58972  414 
apply (equal absdiff_typingL mod_typingL) 
19761  415 
done 
416 

417 
lemmas div_typing_rls = mod_typing div_typing absdiff_typing 

418 

419 

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

421 

58977  422 
lemma divC0: "b:N \<Longrightarrow> 0 div b = 0 : N" 
19761  423 
apply (unfold div_def) 
58972  424 
apply (rew mod_typing absdiff_typing) 
19761  425 
done 
426 

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

19761  429 
apply (unfold div_def) 
58972  430 
apply (rew mod_typing) 
19761  431 
done 
432 

433 

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

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

19761  437 
apply (rule divC_succ [THEN trans_elem]) 
58972  438 
apply (rew div_typing_rls modC_succ) 
439 
apply (NE "succ (a mod b) b") 

440 
apply (rew mod_typing div_typing absdiff_typing) 

19761  441 
done 
442 

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

58977  444 
lemma iszero_decidable: "a:N \<Longrightarrow> rec(a, inl(eq), \<lambda>ka kb. inr(<ka, eq>)) : 
61391  445 
Eq(N,a,0) + (\<Sum>x:N. Eq(N,a, succ(x)))" 
58972  446 
apply (NE a) 
19761  447 
apply (rule_tac [3] PlusI_inr) 
448 
apply (rule_tac [2] PlusI_inl) 

58972  449 
apply eqintr 
450 
apply equal 

19761  451 
done 
452 

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

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

19761  457 
apply (rule EqE) 
458 
(*case analysis on succ(u mod b)b *) 

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

460 
apply (erule_tac [3] SumE) 

58972  461 
apply (hyp_arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2) 
58318  462 
(*Replace one occurrence of b by succ(u mod b). Clumsy!*) 
19761  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) 

58972  466 
apply (hyp_arith_rew div_typing_rls) 
19761  467 
done 
468 

469 
end 