author  wenzelm 
Mon, 10 Nov 2014 21:49:48 +0100  
changeset 58963  26bf09b95dda 
parent 58889  5b7a9633cfa8 
child 58972  5b026cfc5f04 
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 

58889  6 
section {* Elementary arithmetic *} 
17441  7 

8 
theory Arith 

9 
imports Bool 

10 
begin 

0  11 

19761  12 
subsection {* Arithmetic operators and their definitions *} 
17441  13 

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

15 
add :: "[i,i]=>i" (infixr "#+" 65) where 
19762  16 
"a#+b == rec(a, b, %u v. succ(v))" 
0  17 

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

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

19 
diff :: "[i,i]=>i" (infixr "" 65) where 
19762  20 
"ab == rec(b, a, %u v. rec(v, 0, %x y. x))" 
21 

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

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

23 
absdiff :: "[i,i]=>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 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

27 
mult :: "[i,i]=>i" (infixr "#*" 70) where 
19762  28 
"a#*b == rec(a, 0, %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 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

31 
mod :: "[i,i]=>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 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

35 
div :: "[i,i]=>i" (infixr "div" 70) where 
19762  36 
"a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))" 
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 

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) 

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

57 
apply (tactic "typechk_tac @{context} []") 
19761  58 
done 
59 

60 
lemma add_typingL: "[ a=c:N; b=d:N ] ==> a #+ b = c #+ d : N" 

61 
apply (unfold arith_defs) 

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

62 
apply (tactic "equal_tac @{context} []") 
19761  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) 

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

70 
apply (tactic "rew_tac @{context} []") 
19761  71 
done 
72 

73 
lemma addC_succ: "[ a:N; b:N ] ==> succ(a) #+ b = succ(a #+ b) : N" 

74 
apply (unfold arith_defs) 

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

75 
apply (tactic "rew_tac @{context} []") 
19761  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) 

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

85 
apply (tactic {* typechk_tac @{context} [@{thm add_typing}] *}) 
19761  86 
done 
87 

88 
lemma mult_typingL: "[ a=c:N; b=d:N ] ==> a #* b = c #* d : N" 

89 
apply (unfold arith_defs) 

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

90 
apply (tactic {* equal_tac @{context} [@{thm add_typingL}] *}) 
19761  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) 

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

97 
apply (tactic "rew_tac @{context} []") 
19761  98 
done 
99 

100 
lemma multC_succ: "[ a:N; b:N ] ==> succ(a) #* b = b #+ (a #* b) : N" 

101 
apply (unfold arith_defs) 

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

102 
apply (tactic "rew_tac @{context} []") 
19761  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) 

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

112 
apply (tactic "typechk_tac @{context} []") 
19761  113 
done 
114 

115 
lemma diff_typingL: "[ a=c:N; b=d:N ] ==> a  b = c  d : N" 

116 
apply (unfold arith_defs) 

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

117 
apply (tactic "equal_tac @{context} []") 
19761  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) 

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

125 
apply (tactic "rew_tac @{context} []") 
19761  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) 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

132 
apply (tactic {* NE_tac @{context} "b" 1 *}) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

133 
apply (tactic "hyp_rew_tac @{context} []") 
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) *) 

139 
lemma diff_succ_succ: "[ a:N; b:N ] ==> succ(a)  succ(b) = a  b : N" 

140 
apply (unfold arith_defs) 

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

141 
apply (tactic "hyp_rew_tac @{context} []") 
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

142 
apply (tactic {* NE_tac @{context} "b" 1 *}) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

143 
apply (tactic "hyp_rew_tac @{context} []") 
19761  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 

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 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

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 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

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

0  182 
end 
19761  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" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

190 
apply (tactic {* NE_tac @{context} "a" 1 *}) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

191 
apply (tactic "hyp_arith_rew_tac @{context} []") 
19761  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" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

198 
apply (tactic {* NE_tac @{context} "a" 1 *}) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

199 
apply (tactic "hyp_arith_rew_tac @{context} []") 
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

200 
apply (tactic {* NE_tac @{context} "b" 2 *}) 
19761  201 
apply (rule sym_elem) 
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

202 
apply (tactic {* NE_tac @{context} "b" 1 *}) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

203 
apply (tactic "hyp_arith_rew_tac @{context} []") 
19761  204 
done 
205 

206 

207 
subsection {* Multiplication *} 

208 

209 
(*right annihilation in product*) 

210 
lemma mult_0_right: "a:N ==> a #* 0 = 0 : N" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

211 
apply (tactic {* NE_tac @{context} "a" 1 *}) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

212 
apply (tactic "hyp_arith_rew_tac @{context} []") 
19761  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" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

217 
apply (tactic {* NE_tac @{context} "a" 1 *}) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

218 
apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_assoc} RS @{thm sym_elem}] *}) 
19761  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" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

224 
apply (tactic {* NE_tac @{context} "a" 1 *}) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

225 
apply (tactic {* hyp_arith_rew_tac @{context} [@{thm mult_0_right}, @{thm mult_succ_right}] *}) 
19761  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" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

230 
apply (tactic {* NE_tac @{context} "a" 1 *}) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

231 
apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_assoc} RS @{thm sym_elem}] *}) 
19761  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" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

236 
apply (tactic {* NE_tac @{context} "a" 1 *}) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

237 
apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_mult_distrib}] *}) 
19761  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" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

248 
apply (tactic {* NE_tac @{context} "a" 1 *}) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

249 
apply (tactic "hyp_arith_rew_tac @{context} []") 
19761  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#+(xb) = x. 

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

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

36319  259 
schematic_lemma add_diff_inverse_lemma: 
260 
"b:N ==> ?a : PROD x:N. Eq(N, bx, 0) > Eq(N, b #+ (xb), x)" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

261 
apply (tactic {* NE_tac @{context} "b" 1 *}) 
19761  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)#+(xsucc(u)) = x) *) 

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

266 
apply (tactic {* NE_tac @{context} "x" 4 *}, tactic "assume_tac @{context} 4") 
19761  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) 

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

270 
apply (tactic "arith_rew_tac @{context} []") 
19761  271 
(*Solves first 0 goal, simplifies others. Two sugbgoals remain. 
272 
Both follow by rewriting, (2) using quantified induction hyp*) 

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

273 
apply (tactic "intr_tac @{context} []") (*strips remaining PRODs*) 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

274 
apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_0_right}] *}) 
19761  275 
apply assumption 
276 
done 

277 

278 

279 
(*Version of above with premise ba=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; ba = 0 : N ] ==> b #+ (ab) = 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) 

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

296 
apply (tactic "typechk_tac @{context} []") 
19761  297 
done 
298 

299 
lemma absdiff_typingL: "[ a=c:N; b=d:N ] ==> a  b = c  d : N" 

300 
apply (unfold arith_defs) 

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

301 
apply (tactic "equal_tac @{context} []") 
19761  302 
done 
303 

304 
lemma absdiff_self_eq_0: "a:N ==> a  a = 0 : N" 

305 
apply (unfold absdiff_def) 

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

306 
apply (tactic {* arith_rew_tac @{context} [@{thm diff_self_eq_0}] *}) 
19761  307 
done 
308 

309 
lemma absdiffC0: "a:N ==> 0  a = a : N" 

310 
apply (unfold absdiff_def) 

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

311 
apply (tactic "hyp_arith_rew_tac @{context} []") 
19761  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) 

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

317 
apply (tactic "hyp_arith_rew_tac @{context} []") 
19761  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) 

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

324 
apply (tactic {* typechk_tac @{context} [@{thm diff_typing}] *}) 
19761  325 
done 
326 

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

36319  328 
schematic_lemma add_eq0_lemma: "[ a:N; b:N ] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)" 
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

329 
apply (tactic {* NE_tac @{context} "a" 1 *}) 
19761  330 
apply (rule_tac [3] replace_type) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

331 
apply (tactic "arith_rew_tac @{context} []") 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

332 
apply (tactic "intr_tac @{context} []") (*strips remaining PRODs*) 
19761  333 
apply (rule_tac [2] zero_ne_succ [THEN FE]) 
334 
apply (erule_tac [3] EqE [THEN sym_elem]) 

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

335 
apply (tactic {* typechk_tac @{context} [@{thm add_typing}] *}) 
19761  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) 

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

344 
apply (tactic "typechk_tac @{context} []") 
19761  345 
done 
346 

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

36319  348 
schematic_lemma absdiff_eq0_lem: 
19761  349 
"[ a:N; b:N; a  b = 0 : N ] ==> 
350 
?a : SUM v: Eq(N, ab, 0) . Eq(N, ba, 0)" 

351 
apply (unfold absdiff_def) 

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

352 
apply (tactic "intr_tac @{context} []") 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

353 
apply (tactic "eqintr_tac @{context}") 
19761  354 
apply (rule_tac [2] add_eq0) 
355 
apply (rule add_eq0) 

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

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

357 
apply (tactic {* typechk_tac @{context} [@{thm diff_typing}] *}) 
19761  358 
done 
359 

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

361 
proof: ab=0 and ba=0, so b = a+(ba) = 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]) 

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

365 
apply (tactic "TRYALL (assume_tac @{context})") 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

366 
apply (tactic "eqintr_tac @{context}") 
19761  367 
apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem]) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

368 
apply (rule_tac [3] EqE, tactic "assume_tac @{context} 3") 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

369 
apply (tactic {* hyp_arith_rew_tac @{context} [@{thm add_0_right}] *}) 
19761  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) 

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

379 
apply (tactic {* typechk_tac @{context} [@{thm absdiff_typing}] *}) 
19761  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) 

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

384 
apply (tactic {* equal_tac @{context} [@{thm absdiff_typingL}] *}) 
19761  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) 

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

392 
apply (tactic {* rew_tac @{context} [@{thm absdiff_typing}] *}) 
19761  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) 

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

398 
apply (tactic {* rew_tac @{context} [@{thm absdiff_typing}] *}) 
19761  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) 

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

406 
apply (tactic {* typechk_tac @{context} [@{thm absdiff_typing}, @{thm mod_typing}] *}) 
19761  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) 

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

411 
apply (tactic {* equal_tac @{context} [@{thm absdiff_typingL}, @{thm mod_typingL}] *}) 
19761  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) 

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

421 
apply (tactic {* rew_tac @{context} [@{thm mod_typing}, @{thm absdiff_typing}] *}) 
19761  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) 

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

428 
apply (tactic {* rew_tac @{context} [@{thm mod_typing}] *}) 
19761  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]) 

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

436 
apply (tactic {* rew_tac @{context} (@{thms div_typing_rls} @ [@{thm modC_succ}]) *}) 
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

437 
apply (tactic {* NE_tac @{context} "succ (a mod b) b" 1 *}) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

438 
apply (tactic {* rew_tac @{context} [@{thm mod_typing}, @{thm div_typing}, @{thm absdiff_typing}] *}) 
19761  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)))" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

444 
apply (tactic {* NE_tac @{context} "a" 1 *}) 
19761  445 
apply (rule_tac [3] PlusI_inr) 
446 
apply (rule_tac [2] PlusI_inl) 

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

447 
apply (tactic "eqintr_tac @{context}") 
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

448 
apply (tactic "equal_tac @{context} []") 
19761  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" 

27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
21404
diff
changeset

453 
apply (tactic {* NE_tac @{context} "a" 1 *}) 
58963
26bf09b95dda
proper context for assume_tac (atac remains as fallback without context);
wenzelm
parents:
58889
diff
changeset

454 
apply (tactic {* arith_rew_tac @{context} (@{thms div_typing_rls} @ 
39159  455 
[@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *}) 
19761  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) 

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

460 
apply (tactic {* hyp_arith_rew_tac @{context} (@{thms div_typing_rls} @ 
39159  461 
[@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm 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) 

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

466 
apply (tactic {* hyp_arith_rew_tac @{context} @{thms div_typing_rls} *}) 
19761  467 
done 
468 

469 
end 