author  berghofe 
Tue, 25 Jun 1996 13:11:29 +0200  
changeset 1824  44254696843a 
parent 1714  1a5e0101399d 
child 1875  54c0462f8fb2 
permissions  rwrr 
1465  1 
(* Title: HOL/Hoare/Arith2.ML 
1335  2 
ID: $Id$ 
1465  3 
Author: Norbert Galm 
1335  4 
Copyright 1995 TUM 
5 

6 
More arithmetic lemmas. 

7 
*) 

8 

9 
open Arith2; 

10 

11 

12 
(*** HOL lemmas ***) 

13 

14 

15 
val [prem1,prem2]=goal HOL.thy "[~P ==> ~Q; Q] ==> P"; 

16 
by (cut_facts_tac [prem1 COMP impI,prem2] 1); 

17 
by (fast_tac HOL_cs 1); 

18 
val not_imp_swap=result(); 

19 

20 

21 
(*** analogue of diff_induct, for simultaneous induction over 3 vars ***) 

22 

23 
val prems = goal Nat.thy 

24 
"[ !!x. P x 0 0; \ 

25 
\ !!y. P 0 (Suc y) 0; \ 

26 
\ !!z. P 0 0 (Suc z); \ 

27 
\ !!x y. [ P x y 0 ] ==> P (Suc x) (Suc y) 0; \ 

28 
\ !!x z. [ P x 0 z ] ==> P (Suc x) 0 (Suc z); \ 

29 
\ !!y z. [ P 0 y z ] ==> P 0 (Suc y) (Suc z); \ 

30 
\ !!x y z. [ P x y z ] ==> P (Suc x) (Suc y) (Suc z) \ 

31 
\ ] ==> P m n k"; 

32 
by (res_inst_tac [("x","m")] spec 1); 

1476  33 
br diff_induct 1; 
34 
br allI 1; 

35 
br allI 2; 

1335  36 
by (res_inst_tac [("m","xa"),("n","x")] diff_induct 1); 
37 
by (res_inst_tac [("m","x"),("n","Suc y")] diff_induct 4); 

1476  38 
br allI 7; 
1335  39 
by (nat_ind_tac "xa" 7); 
40 
by (ALLGOALS (resolve_tac prems)); 

1476  41 
ba 1; 
42 
ba 1; 

1335  43 
by (fast_tac HOL_cs 1); 
44 
by (fast_tac HOL_cs 1); 

45 
qed "diff_induct3"; 

46 

47 
(*** interaction of + and  ***) 

48 

49 
val prems=goal Arith.thy "~m<n+k ==> (m  n)  k = m  ((n + k)::nat)"; 

50 
by (cut_facts_tac prems 1); 

1476  51 
br mp 1; 
52 
ba 2; 

1335  53 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
54 
by (ALLGOALS Asm_simp_tac); 

55 
qed "diff_not_assoc"; 

56 

57 
val prems=goal Arith.thy "[~m<n; ~n<k] ==> (m  n) + k = m  ((n  k)::nat)"; 

58 
by (cut_facts_tac prems 1); 

1476  59 
bd conjI 1; 
60 
ba 1; 

1335  61 
by (res_inst_tac [("P","~m<n & ~n<k")] mp 1); 
1476  62 
ba 2; 
1335  63 
by (res_inst_tac [("m","m"),("n","n"),("k","k")] diff_induct3 1); 
64 
by (ALLGOALS Asm_simp_tac); 

1476  65 
br impI 1; 
1335  66 
by (dres_inst_tac [("P","~x<y")] conjE 1); 
1476  67 
ba 2; 
68 
br (Suc_diff_n RS sym) 1; 

69 
br le_less_trans 1; 

70 
be (not_less_eq RS subst) 2; 

71 
br (hd ([diff_less_Suc RS lessD] RL [Suc_le_mono RS subst])) 1; 

1335  72 
qed "diff_add_not_assoc"; 
73 

74 
val prems=goal Arith.thy "~n<k ==> (m + n)  k = m + ((n  k)::nat)"; 

75 
by (cut_facts_tac prems 1); 

1476  76 
br mp 1; 
77 
ba 2; 

1335  78 
by (res_inst_tac [("m","n"),("n","k")] diff_induct 1); 
79 
by (ALLGOALS Asm_simp_tac); 

80 
qed "add_diff_assoc"; 

81 

82 
(*** more ***) 

83 

84 
val prems = goal Arith.thy "m~=(n::nat) = (m<n  n<m)"; 

1476  85 
br iffI 1; 
1335  86 
by (cut_inst_tac [("m","m"),("n","n")] less_linear 1); 
87 
by (Asm_full_simp_tac 1); 

1476  88 
be disjE 1; 
89 
be (less_not_refl2 RS not_sym) 1; 

90 
be less_not_refl2 1; 

1335  91 
qed "not_eq_eq_less_or_gr"; 
92 

93 
val [prem] = goal Arith.thy "m<n ==> nm~=0"; 

94 
by (rtac (prem RS rev_mp) 1); 

95 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 

96 
by (ALLGOALS Asm_simp_tac); 

97 
qed "less_imp_diff_not_0"; 

98 

99 
(*******************************************************************) 

100 

1714
1a5e0101399d
Deleted diff_mult_distrib_r as diff_mult_distrib is not proved in Arith.
paulson
parents:
1476
diff
changeset

101 
(** Some of these are now proved, with different names, in HOL/Arith.ML **) 
1a5e0101399d
Deleted diff_mult_distrib_r as diff_mult_distrib is not proved in Arith.
paulson
parents:
1476
diff
changeset

102 

1335  103 
val prems = goal Arith.thy "(i::nat)<j ==> k+i<k+j"; 
104 
by (cut_facts_tac prems 1); 

105 
by (nat_ind_tac "k" 1); 

106 
by (ALLGOALS Asm_simp_tac); 

107 
qed "add_less_mono_l"; 

108 

109 
val prems = goal Arith.thy "~(i::nat)<j ==> ~k+i<k+j"; 

110 
by (cut_facts_tac prems 1); 

111 
by (nat_ind_tac "k" 1); 

112 
by (ALLGOALS Asm_simp_tac); 

113 
qed "add_not_less_mono_l"; 

114 

115 
val prems = goal Arith.thy "[0<k; m<(n::nat)] ==> m*k<n*k"; 

116 
by (cut_facts_tac prems 1); 

117 
by (res_inst_tac [("n","k")] natE 1); 

118 
by (ALLGOALS Asm_full_simp_tac); 

119 
by (nat_ind_tac "x" 1); 

1476  120 
be add_less_mono 2; 
1335  121 
by (ALLGOALS Asm_full_simp_tac); 
122 
qed "mult_less_mono_r"; 

123 

124 
val prems = goal Arith.thy "~m<(n::nat) ==> ~m*k<n*k"; 

125 
by (cut_facts_tac prems 1); 

126 
by (nat_ind_tac "k" 1); 

127 
by (ALLGOALS Simp_tac); 

128 
by (fold_goals_tac [le_def]); 

1476  129 
be add_le_mono 1; 
130 
ba 1; 

1335  131 
qed "mult_not_less_mono_r"; 
132 

133 
val prems = goal Arith.thy "m=(n::nat) ==> m*k=n*k"; 

134 
by (cut_facts_tac prems 1); 

135 
by (nat_ind_tac "k" 1); 

136 
by (ALLGOALS Asm_simp_tac); 

137 
qed "mult_eq_mono_r"; 

138 

139 
val prems = goal Arith.thy "[0<k; m~=(n::nat)] ==> m*k~=n*k"; 

140 
by (cut_facts_tac prems 1); 

141 
by (res_inst_tac [("P","m<n"),("Q","n<m")] disjE 1); 

1476  142 
br (less_not_refl2 RS not_sym) 2; 
143 
be mult_less_mono_r 2; 

144 
br less_not_refl2 3; 

145 
be mult_less_mono_r 3; 

1335  146 
by (ALLGOALS (asm_full_simp_tac ((simpset_of "Arith") addsimps [not_eq_eq_less_or_gr]))); 
147 
qed "mult_not_eq_mono_r"; 

148 

149 
(******************************************************************) 

150 

151 
(*** mod ***) 

152 

1476  153 
goal Arith.thy "(%m. m mod n) = wfrec (trancl pred_nat) \ 
154 
\ (%f j. if j<n then j else f (jn))"; 

155 
by (simp_tac (HOL_ss addsimps [mod_def]) 1); 

156 
val mod_def = result() RS eq_reflection; 

157 

1335  158 
(* AlternativBeweis zu mod_nn_is_0: Spezialfall zu mod_prod_nn_is_0 *) 
159 
(* 

160 
val prems = goal thy "0<n ==> n mod n = 0"; 

161 
by (cut_inst_tac [("m","Suc(0)")] (mod_prod_nn_is_0 COMP impI) 1); 

162 
by (cut_facts_tac prems 1); 

163 
by (Asm_full_simp_tac 1); 

164 
by (fast_tac HOL_cs 1); 

165 
*) 

166 

167 
val prems=goal thy "0<n ==> n mod n = 0"; 

168 
by (cut_facts_tac prems 1); 

1476  169 
br (mod_def RS wf_less_trans) 1; 
1335  170 
by (asm_full_simp_tac ((simpset_of "Arith") addsimps [diff_self_eq_0,cut_def,less_eq]) 1); 
1476  171 
be mod_less 1; 
1335  172 
qed "mod_nn_is_0"; 
173 

174 
val prems=goal thy "0<n ==> m mod n = (m+n) mod n"; 

175 
by (cut_facts_tac prems 1); 

176 
by (res_inst_tac [("s","n+m"),("t","m+n")] subst 1); 

1476  177 
br add_commute 1; 
1335  178 
by (res_inst_tac [("s","n+mn"),("P","%x.x mod n = (n + m) mod n")] subst 1); 
1476  179 
br diff_add_inverse 1; 
180 
br sym 1; 

181 
be mod_geq 1; 

1335  182 
by (res_inst_tac [("s","n<=n+m"),("t","~n+m<n")] subst 1); 
183 
by (simp_tac ((simpset_of "Arith") addsimps [le_def]) 1); 

1476  184 
br le_add1 1; 
1335  185 
qed "mod_eq_add"; 
186 

187 
val prems=goal thy "0<n ==> m*n mod n = 0"; 

188 
by (cut_facts_tac prems 1); 

189 
by (nat_ind_tac "m" 1); 

190 
by (Simp_tac 1); 

1476  191 
be mod_less 1; 
1335  192 
by (dres_inst_tac [("n","n"),("m","m1*n")] mod_eq_add 1); 
193 
by (asm_full_simp_tac ((simpset_of "Arith") addsimps [add_commute]) 1); 

194 
qed "mod_prod_nn_is_0"; 

195 

196 
val prems=goal thy "[0<x; m mod x = 0; n mod x = 0] ==> (m+n) mod x = 0"; 

197 
by (cut_facts_tac prems 1); 

198 
by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1); 

1476  199 
be mod_div_equality 1; 
1335  200 
by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1); 
1476  201 
be mod_div_equality 1; 
1335  202 
by (Asm_simp_tac 1); 
203 
by (res_inst_tac [("s","(m div x + n div x) * x"),("t","m div x * x + n div x * x")] subst 1); 

1476  204 
br add_mult_distrib 1; 
205 
be mod_prod_nn_is_0 1; 

1335  206 
qed "mod0_sum"; 
207 

208 
val prems=goal thy "[0<x; m mod x = 0; n mod x = 0; n<=m] ==> (mn) mod x = 0"; 

209 
by (cut_facts_tac prems 1); 

210 
by (res_inst_tac [("s","m div x * x + m mod x"),("t","m")] subst 1); 

1476  211 
be mod_div_equality 1; 
1335  212 
by (res_inst_tac [("s","n div x * x + n mod x"),("t","n")] subst 1); 
1476  213 
be mod_div_equality 1; 
1335  214 
by (Asm_simp_tac 1); 
215 
by (res_inst_tac [("s","(m div x  n div x) * x"),("t","m div x * x  n div x * x")] subst 1); 

1714
1a5e0101399d
Deleted diff_mult_distrib_r as diff_mult_distrib is not proved in Arith.
paulson
parents:
1476
diff
changeset

216 
br diff_mult_distrib 1; 
1476  217 
be mod_prod_nn_is_0 1; 
1335  218 
qed "mod0_diff"; 
219 

220 

221 
(*** div ***) 

222 

1476  223 

1335  224 
val prems = goal thy "0<n ==> m*n div n = m"; 
225 
by (cut_facts_tac prems 1); 

1476  226 
br (mult_not_eq_mono_r RS not_imp_swap) 1; 
227 
ba 1; 

228 
ba 1; 

1335  229 
by (res_inst_tac [("P","%x.m*n div n * n = x")] (mod_div_equality RS subst) 1); 
1476  230 
ba 1; 
1335  231 
by (dres_inst_tac [("m","m")] mod_prod_nn_is_0 1); 
232 
by (Asm_simp_tac 1); 

233 
qed "div_prod_nn_is_m"; 

234 

235 

236 
(*** divides ***) 

237 

238 
val prems=goalw thy [divides_def] "0<n ==> n divides n"; 

239 
by (cut_facts_tac prems 1); 

240 
by (forward_tac [mod_nn_is_0] 1); 

241 
by (Asm_simp_tac 1); 

242 
qed "divides_nn"; 

243 

244 
val prems=goalw thy [divides_def] "x divides n ==> x<=n"; 

245 
by (cut_facts_tac prems 1); 

1476  246 
br ((mod_less COMP rev_contrapos) RS (le_def RS meta_eq_to_obj_eq RS iffD2)) 1; 
1335  247 
by (Asm_simp_tac 1); 
1476  248 
br (less_not_refl2 RS not_sym) 1; 
1335  249 
by (Asm_simp_tac 1); 
250 
qed "divides_le"; 

251 

252 
val prems=goalw thy [divides_def] "[x divides m; x divides n] ==> x divides (m+n)"; 

253 
by (cut_facts_tac prems 1); 

254 
by (REPEAT ((dtac conjE 1) THEN (atac 2))); 

1476  255 
br conjI 1; 
1335  256 
by (dres_inst_tac [("m","0"),("n","m")] less_imp_add_less 1); 
1476  257 
ba 1; 
258 
be conjI 1; 

259 
br mod0_sum 1; 

1335  260 
by (ALLGOALS atac); 
261 
qed "divides_sum"; 

262 

263 
val prems=goalw thy [divides_def] "[x divides m; x divides n; n<m] ==> x divides (mn)"; 

264 
by (cut_facts_tac prems 1); 

265 
by (REPEAT ((dtac conjE 1) THEN (atac 2))); 

1476  266 
br conjI 1; 
267 
be less_imp_diff_positive 1; 

268 
be conjI 1; 

269 
br mod0_diff 1; 

1335  270 
by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [le_def]))); 
1476  271 
be less_not_sym 1; 
1335  272 
qed "divides_diff"; 
273 

274 

275 
(*** cd ***) 

276 

277 

278 
val prems=goalw thy [cd_def] "0<n ==> cd n n n"; 

279 
by (cut_facts_tac prems 1); 

1476  280 
bd divides_nn 1; 
1335  281 
by (Asm_simp_tac 1); 
282 
qed "cd_nnn"; 

283 

284 
val prems=goalw thy [cd_def] "cd x m n ==> x<=m & x<=n"; 

285 
by (cut_facts_tac prems 1); 

1476  286 
bd conjE 1; 
287 
ba 2; 

288 
bd divides_le 1; 

289 
bd divides_le 1; 

1335  290 
by (Asm_simp_tac 1); 
291 
qed "cd_le"; 

292 

293 
val prems=goalw thy [cd_def] "cd x m n = cd x n m"; 

294 
by (fast_tac HOL_cs 1); 

295 
qed "cd_swap"; 

296 

297 
val prems=goalw thy [cd_def] "n<m ==> cd x m n = cd x (mn) n"; 

298 
by (cut_facts_tac prems 1); 

1476  299 
br iffI 1; 
300 
bd conjE 1; 

301 
ba 2; 

302 
br conjI 1; 

303 
br divides_diff 1; 

304 
bd conjE 5; 

305 
ba 6; 

306 
br conjI 5; 

307 
bd less_not_sym 5; 

308 
bd add_diff_inverse 5; 

1335  309 
by (dres_inst_tac [("m","n"),("n","mn")] divides_sum 5); 
310 
by (ALLGOALS Asm_full_simp_tac); 

311 
qed "cd_diff_l"; 

312 

313 
val prems=goalw thy [cd_def] "m<n ==> cd x m n = cd x m (nm)"; 

314 
by (cut_facts_tac prems 1); 

1476  315 
br iffI 1; 
316 
bd conjE 1; 

317 
ba 2; 

318 
br conjI 1; 

319 
br divides_diff 2; 

320 
bd conjE 5; 

321 
ba 6; 

322 
br conjI 5; 

323 
bd less_not_sym 6; 

324 
bd add_diff_inverse 6; 

1335  325 
by (dres_inst_tac [("n","nm")] divides_sum 6); 
326 
by (ALLGOALS Asm_full_simp_tac); 

327 
qed "cd_diff_r"; 

328 

329 

330 
(*** gcd ***) 

331 

332 
val prems = goalw thy [gcd_def] "0<n ==> n = gcd n n"; 

333 
by (cut_facts_tac prems 1); 

1476  334 
bd cd_nnn 1; 
335 
br (select_equality RS sym) 1; 

336 
be conjI 1; 

337 
br allI 1; 

338 
br impI 1; 

339 
bd cd_le 1; 

340 
bd conjE 2; 

341 
ba 3; 

342 
br le_anti_sym 2; 

1335  343 
by (dres_inst_tac [("x","x")] cd_le 2); 
344 
by (dres_inst_tac [("x","n")] spec 3); 

345 
by (ALLGOALS Asm_full_simp_tac); 

346 
qed "gcd_nnn"; 

347 

348 
val prems = goalw thy [gcd_def] "gcd m n = gcd n m"; 

349 
by (simp_tac ((simpset_of "Arith") addsimps [cd_swap]) 1); 

350 
qed "gcd_swap"; 

351 

352 
val prems=goalw thy [gcd_def] "n<m ==> gcd m n = gcd (mn) n"; 

353 
by (cut_facts_tac prems 1); 

354 
by (subgoal_tac "n<m ==> !x.cd x m n = cd x (mn) n" 1); 

355 
by (Asm_simp_tac 1); 

1476  356 
br allI 1; 
357 
be cd_diff_l 1; 

1335  358 
qed "gcd_diff_l"; 
359 

360 
val prems=goalw thy [gcd_def] "m<n ==> gcd m n = gcd m (nm)"; 

361 
by (cut_facts_tac prems 1); 

362 
by (subgoal_tac "m<n ==> !x.cd x m n = cd x m (nm)" 1); 

363 
by (Asm_simp_tac 1); 

1476  364 
br allI 1; 
365 
be cd_diff_r 1; 

1335  366 
qed "gcd_diff_r"; 
367 

368 

369 
(*** pow ***) 

370 

371 
val [pow_0,pow_Suc] = nat_recs pow_def; 

372 
store_thm("pow_0",pow_0); 

373 
store_thm("pow_Suc",pow_Suc); 

374 

375 
goalw thy [pow_def] "m pow (n+k) = m pow n * m pow k"; 

376 
by (nat_ind_tac "k" 1); 

377 
by (ALLGOALS (asm_simp_tac ((simpset_of "Arith") addsimps [mult_left_commute]))); 

378 
qed "pow_add_reduce"; 

379 

380 
goalw thy [pow_def] "m pow n pow k = m pow (n*k)"; 

381 
by (nat_ind_tac "k" 1); 

382 
by (ALLGOALS Asm_simp_tac); 

383 
by (fold_goals_tac [pow_def]); 

1476  384 
br (pow_add_reduce RS sym) 1; 
1335  385 
qed "pow_pow_reduce"; 
386 

387 
(*** fac ***) 

388 

389 
Addsimps(nat_recs fac_def); 