author  obua 
Fri, 16 Sep 2005 21:02:15 +0200  
changeset 17440  df77edc4f5d0 
parent 9251  bd57acd44fc1 
child 17441  5b5feca0344a 
permissions  rwrr 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

1 
(* Title: CTT/Arith 
0  2 
ID: $Id$ 
1459  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1991 University of Cambridge 
5 

6 
Proofs about elementary arithmetic: addition, multiplication, etc. 

7 
Tests definitions and simplifier. 

8 
*) 

9 

10 
val arith_defs = [add_def, diff_def, absdiff_def, mult_def, mod_def, div_def]; 

11 

12 

13 
(** Addition *) 

14 

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

16 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

17 
Goalw arith_defs "[ a:N; b:N ] ==> a #+ b : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

18 
by (typechk_tac []) ; 
9249  19 
qed "add_typing"; 
0  20 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

21 
Goalw arith_defs "[ a=c:N; b=d:N ] ==> a #+ b = c #+ d : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

22 
by (equal_tac []) ; 
9249  23 
qed "add_typingL"; 
0  24 

25 

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

27 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

28 
Goalw arith_defs "b:N ==> 0 #+ b = b : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

29 
by (rew_tac []) ; 
9249  30 
qed "addC0"; 
0  31 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

32 
Goalw arith_defs "[ a:N; b:N ] ==> succ(a) #+ b = succ(a #+ b) : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

33 
by (rew_tac []) ; 
9249  34 
qed "addC_succ"; 
0  35 

36 

37 
(** Multiplication *) 

38 

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

40 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

41 
Goalw arith_defs "[ a:N; b:N ] ==> a #* b : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

42 
by (typechk_tac [add_typing]) ; 
9249  43 
qed "mult_typing"; 
0  44 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

45 
Goalw arith_defs "[ a=c:N; b=d:N ] ==> a #* b = c #* d : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

46 
by (equal_tac [add_typingL]) ; 
9249  47 
qed "mult_typingL"; 
0  48 

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

50 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

51 
Goalw arith_defs "b:N ==> 0 #* b = 0 : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

52 
by (rew_tac []) ; 
9249  53 
qed "multC0"; 
0  54 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

55 
Goalw arith_defs "[ a:N; b:N ] ==> succ(a) #* b = b #+ (a #* b) : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

56 
by (rew_tac []) ; 
9249  57 
qed "multC_succ"; 
0  58 

59 

60 
(** Difference *) 

61 

62 
(*typing of difference*) 

63 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

64 
Goalw arith_defs "[ a:N; b:N ] ==> a  b : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

65 
by (typechk_tac []) ; 
9249  66 
qed "diff_typing"; 
0  67 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

68 
Goalw arith_defs "[ a=c:N; b=d:N ] ==> a  b = c  d : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

69 
by (equal_tac []) ; 
9249  70 
qed "diff_typingL"; 
0  71 

72 

73 

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

75 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

76 
Goalw arith_defs "a:N ==> a  0 = a : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

77 
by (rew_tac []) ; 
9249  78 
qed "diffC0"; 
0  79 

80 
(*Note: rec(a, 0, %z w.z) is pred(a). *) 

81 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

82 
Goalw arith_defs "b:N ==> 0  b = 0 : N"; 
9249  83 
by (NE_tac "b" 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

84 
by (hyp_rew_tac []) ; 
9249  85 
qed "diff_0_eq_0"; 
0  86 

87 

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

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

90 
Goalw arith_defs "[ a:N; b:N ] ==> succ(a)  succ(b) = a  b : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

91 
by (hyp_rew_tac []); 
9249  92 
by (NE_tac "b" 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

93 
by (hyp_rew_tac []) ; 
9249  94 
qed "diff_succ_succ"; 
0  95 

96 

97 

98 
(*** Simplification *) 

99 

100 
val arith_typing_rls = 

101 
[add_typing, mult_typing, diff_typing]; 

102 

103 
val arith_congr_rls = 

104 
[add_typingL, mult_typingL, diff_typingL]; 

105 

106 
val congr_rls = arith_congr_rls@standard_congr_rls; 

107 

108 
val arithC_rls = 

109 
[addC0, addC_succ, 

110 
multC0, multC_succ, 

111 
diffC0, diff_0_eq_0, diff_succ_succ]; 

112 

113 

114 
structure Arith_simp_data: TSIMP_DATA = 

115 
struct 

1459  116 
val refl = refl_elem 
117 
val sym = sym_elem 

118 
val trans = trans_elem 

119 
val refl_red = refl_red 

120 
val trans_red = trans_red 

121 
val red_if_equal = red_if_equal 

122 
val default_rls = arithC_rls @ comp_rls 

123 
val routine_tac = routine_tac (arith_typing_rls @ routine_rls) 

0  124 
end; 
125 

126 
structure Arith_simp = TSimpFun (Arith_simp_data); 

127 

128 
fun arith_rew_tac prems = make_rew_tac 

129 
(Arith_simp.norm_tac(congr_rls, prems)); 

130 

131 
fun hyp_arith_rew_tac prems = make_rew_tac 

132 
(Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems)); 

133 

134 

135 
(********** 

136 
Addition 

137 
**********) 

138 

139 
(*Associative law for addition*) 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

140 
Goal "[ a:N; b:N; c:N ] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"; 
9249  141 
by (NE_tac "a" 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

142 
by (hyp_arith_rew_tac []) ; 
9249  143 
qed "add_assoc"; 
0  144 

145 

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

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

148 
Goal "[ a:N; b:N ] ==> a #+ b = b #+ a : N"; 
9249  149 
by (NE_tac "a" 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

150 
by (hyp_arith_rew_tac []); 
9249  151 
by (NE_tac "b" 2); 
152 
by (rtac sym_elem 1); 

153 
by (NE_tac "b" 1); 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

154 
by (hyp_arith_rew_tac []) ; 
9249  155 
qed "add_commute"; 
0  156 

157 

158 
(**************** 

159 
Multiplication 

160 
****************) 

161 

162 
(*Commutative law for multiplication 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

163 
Goal "[ a:N; b:N ] ==> a #* b = b #* a : N"; 
9249  164 
by (NE_tac "a" 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

165 
by (hyp_arith_rew_tac []); 
9249  166 
by (NE_tac "b" 2); 
167 
by (rtac sym_elem 1); 

168 
by (NE_tac "b" 1); 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

169 
by (hyp_arith_rew_tac []) ; 
9249  170 
qed "mult_commute"; NEEDS COMMUTATIVE MATCHING 
0  171 
***************) 
172 

173 
(*right annihilation in product*) 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

174 
Goal "a:N ==> a #* 0 = 0 : N"; 
9249  175 
by (NE_tac "a" 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

176 
by (hyp_arith_rew_tac []) ; 
9249  177 
qed "mult_0_right"; 
0  178 

179 
(*right successor law for multiplication*) 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

180 
Goal "[ a:N; b:N ] ==> a #* succ(b) = a #+ (a #* b) : N"; 
9249  181 
by (NE_tac "a" 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

182 
by (hyp_arith_rew_tac [add_assoc RS sym_elem]); 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

183 
by (REPEAT (assume_tac 1 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

184 
ORELSE resolve_tac ([add_commute,mult_typingL,add_typingL]@ intrL_rls@ 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

185 
[refl_elem]) 1)) ; 
9249  186 
qed "mult_succ_right"; 
0  187 

188 
(*Commutative law for multiplication*) 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

189 
Goal "[ a:N; b:N ] ==> a #* b = b #* a : N"; 
9249  190 
by (NE_tac "a" 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

191 
by (hyp_arith_rew_tac [mult_0_right, mult_succ_right]) ; 
9249  192 
qed "mult_commute"; 
0  193 

194 
(*addition distributes over multiplication*) 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

195 
Goal "[ a:N; b:N; c:N ] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"; 
9249  196 
by (NE_tac "a" 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

197 
by (hyp_arith_rew_tac [add_assoc RS sym_elem]) ; 
9249  198 
qed "add_mult_distrib"; 
0  199 

200 

201 
(*Associative law for multiplication*) 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

202 
Goal "[ a:N; b:N; c:N ] ==> (a #* b) #* c = a #* (b #* c) : N"; 
9249  203 
by (NE_tac "a" 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

204 
by (hyp_arith_rew_tac [add_mult_distrib]) ; 
9249  205 
qed "mult_assoc"; 
0  206 

207 

208 
(************ 

209 
Difference 

210 
************ 

211 

212 
Difference on natural numbers, without negative numbers 

213 
a  b = 0 iff a<=b a  b = succ(c) iff a>b *) 

214 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

215 
Goal "a:N ==> a  a = 0 : N"; 
9249  216 
by (NE_tac "a" 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

217 
by (hyp_arith_rew_tac []) ; 
9249  218 
qed "diff_self_eq_0"; 
0  219 

220 

221 
(* [ c : N; 0 : N; c : N ] ==> c #+ 0 = c : N *) 

222 
val add_0_right = addC0 RSN (3, add_commute RS trans_elem); 

223 

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

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

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

227 
Goal "b:N ==> ?a : PROD x:N. Eq(N, bx, 0) > Eq(N, b #+ (xb), x)"; 
0  228 
by (NE_tac "b" 1); 
229 
(*strip one "universal quantifier" but not the "implication"*) 

230 
by (resolve_tac intr_rls 3); 

231 
(*case analysis on x in 

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

233 
by (NE_tac "x" 4 THEN assume_tac 4); 

234 
(*Prepare for simplification of types  the antecedent succ(u)<=x *) 

1459  235 
by (rtac replace_type 5); 
236 
by (rtac replace_type 4); 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

237 
by (arith_rew_tac []); 
0  238 
(*Solves first 0 goal, simplifies others. Two sugbgoals remain. 
239 
Both follow by rewriting, (2) using quantified induction hyp*) 

240 
by (intr_tac[]); (*strips remaining PRODs*) 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

241 
by (hyp_arith_rew_tac [add_0_right]); 
0  242 
by (assume_tac 1); 
1294  243 
qed "add_diff_inverse_lemma"; 
0  244 

245 

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

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

248 
Instead, add_diff_inverse_lemma states the desired induction scheme; 

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

250 
Goal "[ a:N; b:N; ba = 0 : N ] ==> b #+ (ab) = a : N"; 
1459  251 
by (rtac EqE 1); 
0  252 
by (resolve_tac [ add_diff_inverse_lemma RS ProdE RS ProdE ] 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

253 
by (REPEAT (ares_tac [EqI] 1)); 
1294  254 
qed "add_diff_inverse"; 
0  255 

256 

257 
(******************** 

258 
Absolute difference 

259 
********************) 

260 

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

262 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

263 
Goalw arith_defs "[ a:N; b:N ] ==> a  b : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

264 
by (typechk_tac []) ; 
9249  265 
qed "absdiff_typing"; 
0  266 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

267 
Goalw arith_defs "[ a=c:N; b=d:N ] ==> a  b = c  d : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

268 
by (equal_tac []) ; 
9249  269 
qed "absdiff_typingL"; 
0  270 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

271 
Goalw [absdiff_def] "a:N ==> a  a = 0 : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

272 
by (arith_rew_tac [diff_self_eq_0]) ; 
9249  273 
qed "absdiff_self_eq_0"; 
0  274 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

275 
Goalw [absdiff_def] "a:N ==> 0  a = a : N"; 
9249  276 
by (hyp_arith_rew_tac []); 
277 
qed "absdiffC0"; 

0  278 

279 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

280 
Goalw [absdiff_def] "[ a:N; b:N ] ==> succ(a)  succ(b) = a  b : N"; 
9249  281 
by (hyp_arith_rew_tac []) ; 
282 
qed "absdiff_succ_succ"; 

0  283 

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

285 
Goalw [absdiff_def] "[ a:N; b:N ] ==> a  b = b  a : N"; 
1459  286 
by (rtac add_commute 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

287 
by (typechk_tac [diff_typing]); 
1294  288 
qed "absdiff_commute"; 
0  289 

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

291 
Goal "[ a:N; b:N ] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)"; 
0  292 
by (NE_tac "a" 1); 
1459  293 
by (rtac replace_type 3); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

294 
by (arith_rew_tac []); 
0  295 
by (intr_tac[]); (*strips remaining PRODs*) 
296 
by (resolve_tac [ zero_ne_succ RS FE ] 2); 

297 
by (etac (EqE RS sym_elem) 3); 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

298 
by (typechk_tac [add_typing]); 
1294  299 
qed "add_eq0_lemma"; 
0  300 

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

302 
Again, resolution instantiates variables in ProdE *) 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

303 
Goal "[ a:N; b:N; a #+ b = 0 : N ] ==> a = 0 : N"; 
1459  304 
by (rtac EqE 1); 
0  305 
by (resolve_tac [add_eq0_lemma RS ProdE] 1); 
1459  306 
by (rtac EqI 3); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

307 
by (typechk_tac []) ; 
1294  308 
qed "add_eq0"; 
0  309 

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

311 
Goalw [absdiff_def] 
0  312 
"[ a:N; b:N; a  b = 0 : N ] ==> \ 
313 
\ ?a : SUM v: Eq(N, ab, 0) . Eq(N, ba, 0)"; 

314 
by (intr_tac[]); 

315 
by eqintr_tac; 

1459  316 
by (rtac add_eq0 2); 
317 
by (rtac add_eq0 1); 

0  318 
by (resolve_tac [add_commute RS trans_elem] 6); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

319 
by (typechk_tac [diff_typing]); 
1294  320 
qed "absdiff_eq0_lem"; 
0  321 

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

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

324 
Goal "[ a  b = 0 : N; a:N; b:N ] ==> a = b : N"; 
1459  325 
by (rtac EqE 1); 
0  326 
by (resolve_tac [absdiff_eq0_lem RS SumE] 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

327 
by (TRYALL assume_tac); 
0  328 
by eqintr_tac; 
329 
by (resolve_tac [add_diff_inverse RS sym_elem RS trans_elem] 1); 

1459  330 
by (rtac EqE 3 THEN assume_tac 3); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

331 
by (hyp_arith_rew_tac [add_0_right]); 
1294  332 
qed "absdiff_eq0"; 
0  333 

334 
(*********************** 

335 
Remainder and Quotient 

336 
***********************) 

337 

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

339 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

340 
Goalw [mod_def] "[ a:N; b:N ] ==> a mod b : N"; 
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

341 
by (typechk_tac [absdiff_typing]) ; 
9249  342 
qed "mod_typing"; 
0  343 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

344 
Goalw [mod_def] "[ a=c:N; b=d:N ] ==> a mod b = c mod d : N"; 
9249  345 
by (equal_tac [absdiff_typingL]) ; 
346 
qed "mod_typingL"; 

0  347 

348 

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

350 

9249  351 
Goalw [mod_def] "b:N ==> 0 mod b = 0 : N"; 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

352 
by (rew_tac [absdiff_typing]) ; 
9249  353 
qed "modC0"; 
0  354 

9249  355 
Goalw [mod_def] 
356 
"[ a:N; b:N ] ==> succ(a) mod b = rec(succ(a mod b)  b, 0, %x y. succ(a mod b)) : N"; 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

357 
by (rew_tac [absdiff_typing]) ; 
9249  358 
qed "modC_succ"; 
0  359 

360 

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

362 

9249  363 
Goalw [div_def] "[ a:N; b:N ] ==> a div b : N"; 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

364 
by (typechk_tac [absdiff_typing,mod_typing]) ; 
9249  365 
qed "div_typing"; 
0  366 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

367 
Goalw [div_def] "[ a=c:N; b=d:N ] ==> a div b = c div d : N"; 
9249  368 
by (equal_tac [absdiff_typingL, mod_typingL]); 
369 
qed "div_typingL"; 

0  370 

371 
val div_typing_rls = [mod_typing, div_typing, absdiff_typing]; 

372 

373 

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

375 

9249  376 
Goalw [div_def] "b:N ==> 0 div b = 0 : N"; 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

377 
by (rew_tac [mod_typing, absdiff_typing]) ; 
9249  378 
qed "divC0"; 
0  379 

9249  380 
Goalw [div_def] 
381 
"[ a:N; b:N ] ==> succ(a) div b = \ 

382 
\ rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"; 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

383 
by (rew_tac [mod_typing]) ; 
9249  384 
qed "divC_succ"; 
0  385 

386 

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

388 
Goal "[ a:N; b:N ] ==> \ 
9249  389 
\ succ(a) div b =rec(succ(a mod b)  b, succ(a div b), %x y. a div b) : N"; 
390 
by (resolve_tac [ divC_succ RS trans_elem ] 1); 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

391 
by (rew_tac(div_typing_rls @ [modC_succ])); 
9249  392 
by (NE_tac "succ(a mod b)b" 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

393 
by (rew_tac [mod_typing, div_typing, absdiff_typing]); 
9249  394 
qed "divC_succ2"; 
0  395 

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

397 
Goal "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) : \ 
9249  398 
\ Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"; 
399 
by (NE_tac "a" 1); 

400 
by (rtac PlusI_inr 3); 

401 
by (rtac PlusI_inl 2); 

402 
by eqintr_tac; 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

403 
by (equal_tac []) ; 
9249  404 
qed "iszero_decidable"; 
0  405 

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

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

407 
Goal "[ a:N; b:N ] ==> a mod b #+ (a div b) #* b = a : N"; 
0  408 
by (NE_tac "a" 1); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

409 
by (arith_rew_tac (div_typing_rls@[modC0,modC_succ,divC0,divC_succ2])); 
1459  410 
by (rtac EqE 1); 
0  411 
(*case analysis on succ(u mod b)b *) 
412 
by (res_inst_tac [("a1", "succ(u mod b)  b")] 

413 
(iszero_decidable RS PlusE) 1); 

414 
by (etac SumE 3); 

9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

415 
by (hyp_arith_rew_tac (div_typing_rls @ 
1459  416 
[modC0,modC_succ, divC0, divC_succ2])); 
0  417 
(*Replace one occurence of b by succ(u mod b). Clumsy!*) 
418 
by (resolve_tac [ add_typingL RS trans_elem ] 1); 

419 
by (eresolve_tac [EqE RS absdiff_eq0 RS sym_elem] 1); 

1459  420 
by (rtac refl_elem 3); 
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
9249
diff
changeset

421 
by (hyp_arith_rew_tac (div_typing_rls)); 
1294  422 
qed "mod_div_equality"; 
0  423 

424 
writeln"Reached end of file."; 