author  paulson 
Thu, 12 Sep 1996 10:32:43 +0200  
changeset 1979  91c74763c5a3 
parent 1909  f535276171d1 
child 2007  968f78b52540 
permissions  rwrr 
1465  1 
(* Title: HOL/Arith.ML 
923  2 
ID: $Id$ 
1465  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
923  4 
Copyright 1993 University of Cambridge 
5 

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

7 
Tests definitions and simplifier. 

8 
*) 

9 

10 
open Arith; 

11 

12 
(*** Basic rewrite rules for the arithmetic operators ***) 

13 

14 
val [pred_0, pred_Suc] = nat_recs pred_def; 

15 
val [add_0,add_Suc] = nat_recs add_def; 

1767
0c8f131eac40
Rules pred_0, pred_Suc etc. are now stored in theorem database.
berghofe
parents:
1760
diff
changeset

16 
val [mult_0,mult_Suc] = nat_recs mult_def; 
0c8f131eac40
Rules pred_0, pred_Suc etc. are now stored in theorem database.
berghofe
parents:
1760
diff
changeset

17 
store_thm("pred_0",pred_0); 
0c8f131eac40
Rules pred_0, pred_Suc etc. are now stored in theorem database.
berghofe
parents:
1760
diff
changeset

18 
store_thm("pred_Suc",pred_Suc); 
0c8f131eac40
Rules pred_0, pred_Suc etc. are now stored in theorem database.
berghofe
parents:
1760
diff
changeset

19 
store_thm("add_0",add_0); 
0c8f131eac40
Rules pred_0, pred_Suc etc. are now stored in theorem database.
berghofe
parents:
1760
diff
changeset

20 
store_thm("add_Suc",add_Suc); 
0c8f131eac40
Rules pred_0, pred_Suc etc. are now stored in theorem database.
berghofe
parents:
1760
diff
changeset

21 
store_thm("mult_0",mult_0); 
0c8f131eac40
Rules pred_0, pred_Suc etc. are now stored in theorem database.
berghofe
parents:
1760
diff
changeset

22 
store_thm("mult_Suc",mult_Suc); 
1301  23 
Addsimps [pred_0,pred_Suc,add_0,add_Suc,mult_0,mult_Suc]; 
24 

25 
(** pred **) 

26 

27 
val prems = goal Arith.thy "n ~= 0 ==> Suc(pred n) = n"; 

1552  28 
by (res_inst_tac [("n","n")] natE 1); 
29 
by (cut_facts_tac prems 1); 

30 
by (ALLGOALS Asm_full_simp_tac); 

1301  31 
qed "Suc_pred"; 
32 
Addsimps [Suc_pred]; 

923  33 

34 
(** Difference **) 

35 

1655  36 
bind_thm("diff_0", diff_def RS def_nat_rec_0); 
923  37 

38 
qed_goalw "diff_0_eq_0" Arith.thy [diff_def, pred_def] 

39 
"0  n = 0" 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

40 
(fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]); 
923  41 

42 
(*Must simplify BEFORE the induction!! (Else we get a critical pair) 

43 
Suc(m)  Suc(n) rewrites to pred(Suc(m)  n) *) 

44 
qed_goalw "diff_Suc_Suc" Arith.thy [diff_def, pred_def] 

45 
"Suc(m)  Suc(n) = m  n" 

46 
(fn _ => 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

47 
[Simp_tac 1, nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]); 
923  48 

1301  49 
Addsimps [diff_0, diff_0_eq_0, diff_Suc_Suc]; 
923  50 

51 

1713  52 
goal Arith.thy "!!k. 0<k ==> EX j. k = Suc(j)"; 
53 
by (etac rev_mp 1); 

54 
by (nat_ind_tac "k" 1); 

55 
by (Simp_tac 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1713
diff
changeset

56 
by (Fast_tac 1); 
1713  57 
val lemma = result(); 
58 

59 
(* [ 0 < k; !!j. [ j: nat; k = succ(j) ] ==> Q ] ==> Q *) 

60 
bind_thm ("zero_less_natE", lemma RS exE); 

61 

62 

63 

923  64 
(**** Inductive properties of the operators ****) 
65 

66 
(*** Addition ***) 

67 

68 
qed_goal "add_0_right" Arith.thy "m + 0 = m" 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

69 
(fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); 
923  70 

71 
qed_goal "add_Suc_right" Arith.thy "m + Suc(n) = Suc(m+n)" 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

72 
(fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); 
923  73 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

74 
Addsimps [add_0_right,add_Suc_right]; 
923  75 

76 
(*Associative law for addition*) 

77 
qed_goal "add_assoc" Arith.thy "(m + n) + k = m + ((n + k)::nat)" 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

78 
(fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); 
923  79 

80 
(*Commutative law for addition*) 

81 
qed_goal "add_commute" Arith.thy "m + n = n + (m::nat)" 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

82 
(fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); 
923  83 

84 
qed_goal "add_left_commute" Arith.thy "x+(y+z)=y+((x+z)::nat)" 

85 
(fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1, 

86 
rtac (add_commute RS arg_cong) 1]); 

87 

88 
(*Addition is an ACoperator*) 

89 
val add_ac = [add_assoc, add_commute, add_left_commute]; 

90 

91 
goal Arith.thy "!!k::nat. (k + m = k + n) = (m=n)"; 

92 
by (nat_ind_tac "k" 1); 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

93 
by (Simp_tac 1); 
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

94 
by (Asm_simp_tac 1); 
923  95 
qed "add_left_cancel"; 
96 

97 
goal Arith.thy "!!k::nat. (m + k = n + k) = (m=n)"; 

98 
by (nat_ind_tac "k" 1); 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

99 
by (Simp_tac 1); 
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

100 
by (Asm_simp_tac 1); 
923  101 
qed "add_right_cancel"; 
102 

103 
goal Arith.thy "!!k::nat. (k + m <= k + n) = (m<=n)"; 

104 
by (nat_ind_tac "k" 1); 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

105 
by (Simp_tac 1); 
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

106 
by (Asm_simp_tac 1); 
923  107 
qed "add_left_cancel_le"; 
108 

109 
goal Arith.thy "!!k::nat. (k + m < k + n) = (m<n)"; 

110 
by (nat_ind_tac "k" 1); 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

111 
by (Simp_tac 1); 
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

112 
by (Asm_simp_tac 1); 
923  113 
qed "add_left_cancel_less"; 
114 

1327
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

115 
Addsimps [add_left_cancel, add_right_cancel, 
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

116 
add_left_cancel_le, add_left_cancel_less]; 
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

117 

6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

118 
goal Arith.thy "(m+n = 0) = (m=0 & n=0)"; 
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

119 
by (nat_ind_tac "m" 1); 
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

120 
by (ALLGOALS Asm_simp_tac); 
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

121 
qed "add_is_0"; 
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

122 
Addsimps [add_is_0]; 
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

123 

6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

124 
goal Arith.thy "!!n. n ~= 0 ==> m + pred n = pred(m+n)"; 
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

125 
by (nat_ind_tac "m" 1); 
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

126 
by (ALLGOALS Asm_simp_tac); 
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

127 
qed "add_pred"; 
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

128 
Addsimps [add_pred]; 
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

129 

923  130 
(*** Multiplication ***) 
131 

132 
(*right annihilation in product*) 

133 
qed_goal "mult_0_right" Arith.thy "m * 0 = 0" 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

134 
(fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); 
923  135 

136 
(*right Sucessor law for multiplication*) 

137 
qed_goal "mult_Suc_right" Arith.thy "m * Suc(n) = m + (m * n)" 

138 
(fn _ => [nat_ind_tac "m" 1, 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

139 
ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]); 
923  140 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

141 
Addsimps [mult_0_right,mult_Suc_right]; 
923  142 

1795  143 
goal Arith.thy "1 * n = n"; 
144 
by (Asm_simp_tac 1); 

145 
qed "mult_1"; 

146 

147 
goal Arith.thy "n * 1 = n"; 

148 
by (Asm_simp_tac 1); 

149 
qed "mult_1_right"; 

150 

923  151 
(*Commutative law for multiplication*) 
152 
qed_goal "mult_commute" Arith.thy "m * n = n * (m::nat)" 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

153 
(fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); 
923  154 

155 
(*addition distributes over multiplication*) 

156 
qed_goal "add_mult_distrib" Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)" 

157 
(fn _ => [nat_ind_tac "m" 1, 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

158 
ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]); 
923  159 

160 
qed_goal "add_mult_distrib2" Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)" 

161 
(fn _ => [nat_ind_tac "m" 1, 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

162 
ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]); 
923  163 

164 
(*Associative law for multiplication*) 

165 
qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)" 

1795  166 
(fn _ => [nat_ind_tac "m" 1, 
167 
ALLGOALS (asm_simp_tac (!simpset addsimps [add_mult_distrib]))]); 

923  168 

169 
qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)" 

170 
(fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1, 

171 
rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]); 

172 

173 
val mult_ac = [mult_assoc,mult_commute,mult_left_commute]; 

174 

175 
(*** Difference ***) 

176 

177 
qed_goal "diff_self_eq_0" Arith.thy "m  m = 0" 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

178 
(fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]); 
1496  179 
Addsimps [diff_self_eq_0]; 
923  180 

181 
(*Addition is the inverse of subtraction: if n<=m then n+(mn) = m. *) 

182 
val [prem] = goal Arith.thy "[ ~ m<n ] ==> n+(mn) = (m::nat)"; 

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

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

1660  185 
by (ALLGOALS (Asm_simp_tac)); 
923  186 
qed "add_diff_inverse"; 
187 

188 

189 
(*** Remainder ***) 

190 

191 
goal Arith.thy "m  n < Suc(m)"; 

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

193 
by (etac less_SucE 3); 

1660  194 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq]))); 
923  195 
qed "diff_less_Suc"; 
196 

197 
goal Arith.thy "!!m::nat. m  n <= m"; 

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

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

199 
by (ALLGOALS Asm_simp_tac); 
923  200 
qed "diff_le_self"; 
201 

202 
goal Arith.thy "!!n::nat. (n+m)  n = m"; 

203 
by (nat_ind_tac "n" 1); 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

204 
by (ALLGOALS Asm_simp_tac); 
923  205 
qed "diff_add_inverse"; 
206 

1713  207 
goal Arith.thy "!!n::nat.(m+n)  n = m"; 
208 
by (res_inst_tac [("m1","m")] (add_commute RS ssubst) 1); 

209 
by (REPEAT (ares_tac [diff_add_inverse] 1)); 

210 
qed "diff_add_inverse2"; 

211 

212 
goal Arith.thy "!!k::nat. (k+m)  (k+n) = m  n"; 

213 
by (nat_ind_tac "k" 1); 

214 
by (ALLGOALS Asm_simp_tac); 

215 
qed "diff_cancel"; 

216 
Addsimps [diff_cancel]; 

217 

218 
goal Arith.thy "!!m::nat. (m+k)  (n+k) = m  n"; 

219 
val add_commute_k = read_instantiate [("n","k")] add_commute; 

220 
by (asm_simp_tac (!simpset addsimps ([add_commute_k])) 1); 

221 
qed "diff_cancel2"; 

222 
Addsimps [diff_cancel2]; 

223 

923  224 
goal Arith.thy "!!n::nat. n  (n+m) = 0"; 
225 
by (nat_ind_tac "n" 1); 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

226 
by (ALLGOALS Asm_simp_tac); 
923  227 
qed "diff_add_0"; 
1713  228 
Addsimps [diff_add_0]; 
229 

230 
(** Difference distributes over multiplication **) 

231 

232 
goal Arith.thy "!!m::nat. (m  n) * k = (m * k)  (n * k)"; 

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

234 
by (ALLGOALS Asm_simp_tac); 

235 
qed "diff_mult_distrib" ; 

236 

237 
goal Arith.thy "!!m::nat. k * (m  n) = (k * m)  (k * n)"; 

238 
val mult_commute_k = read_instantiate [("m","k")] mult_commute; 

239 
by (simp_tac (!simpset addsimps [diff_mult_distrib, mult_commute_k]) 1); 

240 
qed "diff_mult_distrib2" ; 

241 
(*NOT added as rewrites, since sometimes they are used from righttoleft*) 

242 

243 

244 
(** Lessthen properties **) 

923  245 

246 
(*In ordinary notation: if 0<n and n<=m then mn < m *) 

247 
goal Arith.thy "!!m. [ 0<n; ~ m<n ] ==> m  n < m"; 

248 
by (subgoal_tac "0<n > ~ m<n > m  n < m" 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1713
diff
changeset

249 
by (Fast_tac 1); 
923  250 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

251 
by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc]))); 
1398  252 
qed "diff_less"; 
923  253 

254 
val wf_less_trans = wf_pred_nat RS wf_trancl RSN (2, def_wfrec RS trans); 

255 

972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
965
diff
changeset

256 
goalw Nat.thy [less_def] "(m,n) : pred_nat^+ = (m<n)"; 
923  257 
by (rtac refl 1); 
258 
qed "less_eq"; 

259 

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

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

263 
val mod_def1 = result() RS eq_reflection; 

264 

923  265 
goal Arith.thy "!!m. m<n ==> m mod n = m"; 
1475  266 
by (rtac (mod_def1 RS wf_less_trans) 1); 
1552  267 
by (Asm_simp_tac 1); 
923  268 
qed "mod_less"; 
269 

270 
goal Arith.thy "!!m. [ 0<n; ~m<n ] ==> m mod n = (mn) mod n"; 

1475  271 
by (rtac (mod_def1 RS wf_less_trans) 1); 
1552  272 
by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1); 
923  273 
qed "mod_geq"; 
274 

275 

276 
(*** Quotient ***) 

277 

1475  278 
goal Arith.thy "(%m. m div n) = wfrec (trancl pred_nat) \ 
279 
\ (%f j. if j<n then 0 else Suc (f (jn)))"; 

280 
by (simp_tac (HOL_ss addsimps [div_def]) 1); 

281 
val div_def1 = result() RS eq_reflection; 

282 

923  283 
goal Arith.thy "!!m. m<n ==> m div n = 0"; 
1475  284 
by (rtac (div_def1 RS wf_less_trans) 1); 
1552  285 
by (Asm_simp_tac 1); 
923  286 
qed "div_less"; 
287 

288 
goal Arith.thy "!!M. [ 0<n; ~m<n ] ==> m div n = Suc((mn) div n)"; 

1475  289 
by (rtac (div_def1 RS wf_less_trans) 1); 
1552  290 
by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1); 
923  291 
qed "div_geq"; 
292 

293 
(*Main Result about quotient and remainder.*) 

294 
goal Arith.thy "!!m. 0<n ==> (m div n)*n + m mod n = m"; 

295 
by (res_inst_tac [("n","m")] less_induct 1); 

296 
by (rename_tac "k" 1); (*Variable name used in line below*) 

297 
by (case_tac "k<n" 1); 

1660  298 
by (ALLGOALS (asm_simp_tac(!simpset addsimps ([add_assoc] @ 
923  299 
[mod_less, mod_geq, div_less, div_geq, 
1465  300 
add_diff_inverse, diff_less])))); 
923  301 
qed "mod_div_equality"; 
302 

303 

304 
(*** More results about difference ***) 

305 

306 
val [prem] = goal Arith.thy "m < Suc(n) ==> mn = 0"; 

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

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

1660  309 
by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1); 
310 
by (ALLGOALS (Asm_simp_tac)); 

923  311 
qed "less_imp_diff_is_0"; 
312 

313 
val prems = goal Arith.thy "mn = 0 > nm = 0 > m=n"; 

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

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

315 
by (REPEAT(Simp_tac 1 THEN TRY(atac 1))); 
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1475
diff
changeset

316 
qed_spec_mp "diffs0_imp_equal"; 
923  317 

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

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

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

1660  321 
by (ALLGOALS (Asm_simp_tac)); 
923  322 
qed "less_imp_diff_positive"; 
323 

324 
val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)n = Suc(mn)"; 

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

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

1660  327 
by (ALLGOALS (Asm_simp_tac)); 
923  328 
qed "Suc_diff_n"; 
329 

1398  330 
goal Arith.thy "Suc(m)n = (if m<n then 0 else Suc(mn))"; 
1552  331 
by (simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n] 
923  332 
setloop (split_tac [expand_if])) 1); 
333 
qed "if_Suc_diff_n"; 

334 

335 
goal Arith.thy "P(k) > (!n. P(Suc(n))> P(n)) > P(ki)"; 

336 
by (res_inst_tac [("m","k"),("n","i")] diff_induct 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1713
diff
changeset

337 
by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o Fast_tac)); 
923  338 
qed "zero_induct_lemma"; 
339 

340 
val prems = goal Arith.thy "[ P(k); !!n. P(Suc(n)) ==> P(n) ] ==> P(0)"; 

341 
by (rtac (diff_self_eq_0 RS subst) 1); 

342 
by (rtac (zero_induct_lemma RS mp RS mp) 1); 

343 
by (REPEAT (ares_tac ([impI,allI]@prems) 1)); 

344 
qed "zero_induct"; 

345 

346 
(*13 July 1992: loaded in 105.7s*) 

347 

1618  348 

349 
(*** Further facts about mod (mainly for mutilated checkerboard ***) 

350 

351 
goal Arith.thy 

352 
"!!m n. 0<n ==> \ 

353 
\ Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))"; 

354 
by (res_inst_tac [("n","m")] less_induct 1); 

355 
by (excluded_middle_tac "Suc(na)<n" 1); 

356 
(* case Suc(na) < n *) 

357 
by (forward_tac [lessI RS less_trans] 2); 

358 
by (asm_simp_tac (!simpset addsimps [mod_less, less_not_refl2 RS not_sym]) 2); 

359 
(* case n <= Suc(na) *) 

360 
by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, mod_geq]) 1); 

361 
by (etac (le_imp_less_or_eq RS disjE) 1); 

362 
by (asm_simp_tac (!simpset addsimps [Suc_diff_n]) 1); 

363 
by (asm_full_simp_tac (!simpset addsimps [not_less_eq RS sym, 

364 
diff_less, mod_geq]) 1); 

365 
by (asm_simp_tac (!simpset addsimps [mod_less]) 1); 

366 
qed "mod_Suc"; 

367 

368 
goal Arith.thy "!!m n. 0<n ==> m mod n < n"; 

369 
by (res_inst_tac [("n","m")] less_induct 1); 

370 
by (excluded_middle_tac "na<n" 1); 

371 
(*case na<n*) 

372 
by (asm_simp_tac (!simpset addsimps [mod_less]) 2); 

373 
(*case n le na*) 

374 
by (asm_full_simp_tac (!simpset addsimps [mod_geq, diff_less]) 1); 

375 
qed "mod_less_divisor"; 

376 

377 

1626  378 
(** Evens and Odds **) 
379 

1909  380 
(*With less_zeroE, causes case analysis on b<2*) 
381 
AddSEs [less_SucE]; 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1713
diff
changeset

382 

1626  383 
goal thy "!!k b. b<2 ==> k mod 2 = b  k mod 2 = (if b=1 then 0 else 1)"; 
384 
by (subgoal_tac "k mod 2 < 2" 1); 

385 
by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2); 

386 
by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1); 

1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1713
diff
changeset

387 
by (Fast_tac 1); 
1626  388 
qed "mod2_cases"; 
389 

390 
goal thy "Suc(Suc(m)) mod 2 = m mod 2"; 

391 
by (subgoal_tac "m mod 2 < 2" 1); 

392 
by (asm_simp_tac (!simpset addsimps [mod_less_divisor]) 2); 

1909  393 
by (Step_tac 1); 
1626  394 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [mod_Suc]))); 
395 
qed "mod2_Suc_Suc"; 

396 
Addsimps [mod2_Suc_Suc]; 

397 

398 
goal thy "(m+m) mod 2 = 0"; 

399 
by (nat_ind_tac "m" 1); 

400 
by (simp_tac (!simpset addsimps [mod_less]) 1); 

401 
by (asm_simp_tac (!simpset addsimps [mod2_Suc_Suc, add_Suc_right]) 1); 

402 
qed "mod2_add_self"; 

403 
Addsimps [mod2_add_self]; 

404 

1909  405 
Delrules [less_SucE]; 
406 

1626  407 

923  408 
(**** Additional theorems about "less than" ****) 
409 

1909  410 
goal Arith.thy "? k::nat. n = n+k"; 
411 
by (res_inst_tac [("x","0")] exI 1); 

412 
by (Simp_tac 1); 

413 
val lemma = result(); 

414 

923  415 
goal Arith.thy "!!m. m<n > (? k. n=Suc(m+k))"; 
416 
by (nat_ind_tac "n" 1); 

1909  417 
by (ALLGOALS (simp_tac (!simpset addsimps [less_Suc_eq]))); 
418 
by (step_tac (!claset addSIs [lemma]) 1); 

923  419 
by (res_inst_tac [("x","Suc(k)")] exI 1); 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

420 
by (Simp_tac 1); 
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1475
diff
changeset

421 
qed_spec_mp "less_eq_Suc_add"; 
923  422 

423 
goal Arith.thy "n <= ((m + n)::nat)"; 

424 
by (nat_ind_tac "m" 1); 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

425 
by (ALLGOALS Simp_tac); 
923  426 
by (etac le_trans 1); 
427 
by (rtac (lessI RS less_imp_le) 1); 

428 
qed "le_add2"; 

429 

430 
goal Arith.thy "n <= ((n + m)::nat)"; 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

431 
by (simp_tac (!simpset addsimps add_ac) 1); 
923  432 
by (rtac le_add2 1); 
433 
qed "le_add1"; 

434 

435 
bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans))); 

436 
bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans))); 

437 

438 
(*"i <= j ==> i <= j+m"*) 

439 
bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans)); 

440 

441 
(*"i <= j ==> i <= m+j"*) 

442 
bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans)); 

443 

444 
(*"i < j ==> i < j+m"*) 

445 
bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans)); 

446 

447 
(*"i < j ==> i < m+j"*) 

448 
bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans)); 

449 

1152  450 
goal Arith.thy "!!i. i+j < (k::nat) ==> i<k"; 
1552  451 
by (etac rev_mp 1); 
452 
by (nat_ind_tac "j" 1); 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

453 
by (ALLGOALS Asm_simp_tac); 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1713
diff
changeset

454 
by (fast_tac (!claset addDs [Suc_lessD]) 1); 
1152  455 
qed "add_lessD1"; 
456 

923  457 
goal Arith.thy "!!k::nat. m <= n ==> m <= n+k"; 
1552  458 
by (etac le_trans 1); 
459 
by (rtac le_add1 1); 

923  460 
qed "le_imp_add_le"; 
461 

462 
goal Arith.thy "!!k::nat. m < n ==> m < n+k"; 

1552  463 
by (etac less_le_trans 1); 
464 
by (rtac le_add1 1); 

923  465 
qed "less_imp_add_less"; 
466 

467 
goal Arith.thy "m+k<=n > m<=(n::nat)"; 

468 
by (nat_ind_tac "k" 1); 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

469 
by (ALLGOALS Asm_simp_tac); 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1713
diff
changeset

470 
by (fast_tac (!claset addDs [Suc_leD]) 1); 
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1475
diff
changeset

471 
qed_spec_mp "add_leD1"; 
923  472 

473 
goal Arith.thy "!!k l::nat. [ k<l; m+l = k+n ] ==> m<n"; 

1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1767
diff
changeset

474 
by (safe_tac (!claset addSDs [less_eq_Suc_add])); 
923  475 
by (asm_full_simp_tac 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

476 
(!simpset delsimps [add_Suc_right] 
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

477 
addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1); 
1552  478 
by (etac subst 1); 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

479 
by (simp_tac (!simpset addsimps [less_add_Suc1]) 1); 
923  480 
qed "less_add_eq_less"; 
481 

482 

1713  483 
(*** Monotonicity of Addition ***) 
923  484 

485 
(*strict, in 1st argument*) 

486 
goal Arith.thy "!!i j k::nat. i < j ==> i + k < j + k"; 

487 
by (nat_ind_tac "k" 1); 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

488 
by (ALLGOALS Asm_simp_tac); 
923  489 
qed "add_less_mono1"; 
490 

491 
(*strict, in both arguments*) 

492 
goal Arith.thy "!!i j k::nat. [i < j; k < l] ==> i + k < j + l"; 

493 
by (rtac (add_less_mono1 RS less_trans) 1); 

1198  494 
by (REPEAT (assume_tac 1)); 
923  495 
by (nat_ind_tac "j" 1); 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

496 
by (ALLGOALS Asm_simp_tac); 
923  497 
qed "add_less_mono"; 
498 

499 
(*A [clumsy] way of lifting < monotonicity to <= monotonicity *) 

500 
val [lt_mono,le] = goal Arith.thy 

1465  501 
"[ !!i j::nat. i<j ==> f(i) < f(j); \ 
502 
\ i <= j \ 

923  503 
\ ] ==> f(i) <= (f(j)::nat)"; 
504 
by (cut_facts_tac [le] 1); 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

505 
by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1); 
1760
6f41a494f3b1
Replaced fast_tac by Fast_tac (which uses default claset)
berghofe
parents:
1713
diff
changeset

506 
by (fast_tac (!claset addSIs [lt_mono]) 1); 
923  507 
qed "less_mono_imp_le_mono"; 
508 

509 
(*nonstrict, in 1st argument*) 

510 
goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k"; 

511 
by (res_inst_tac [("f", "%j.j+k")] less_mono_imp_le_mono 1); 

1552  512 
by (etac add_less_mono1 1); 
923  513 
by (assume_tac 1); 
514 
qed "add_le_mono1"; 

515 

516 
(*nonstrict, in both arguments*) 

517 
goal Arith.thy "!!k l::nat. [i<=j; k<=l ] ==> i + k <= j + l"; 

518 
by (etac (add_le_mono1 RS le_trans) 1); 

1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

519 
by (simp_tac (!simpset addsimps [add_commute]) 1); 
923  520 
(*j moves to the end because it is free while k, l are bound*) 
1552  521 
by (etac add_le_mono1 1); 
923  522 
qed "add_le_mono"; 
1713  523 

524 
(*** Monotonicity of Multiplication ***) 

525 

526 
goal Arith.thy "!!i::nat. i<=j ==> i*k<=j*k"; 

527 
by (nat_ind_tac "k" 1); 

528 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_le_mono]))); 

529 
qed "mult_le_mono1"; 

530 

531 
(*<=monotonicity, BOTH arguments*) 

532 
goal Arith.thy "!!i::nat. [ i<=j; k<=l ] ==> i*k<=j*l"; 

533 
by (rtac le_trans 1); 

534 
by (ALLGOALS 

1786
8a31d85d27b8
best_tac, deepen_tac and safe_tac now also use default claset.
berghofe
parents:
1767
diff
changeset

535 
(deepen_tac (!claset addIs [mult_commute RS ssubst, mult_le_mono1]) 0)); 
1713  536 
qed "mult_le_mono"; 
537 

538 
(*strict, in 1st argument; proof is by induction on k>0*) 

539 
goal Arith.thy "!!i::nat. [ i<j; 0<k ] ==> k*i < k*j"; 

540 
be zero_less_natE 1; 

541 
by (Asm_simp_tac 1); 

542 
by (nat_ind_tac "x" 1); 

543 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_less_mono]))); 

544 
qed "mult_less_mono2"; 

545 

546 
goal Arith.thy "(0 < m*n) = (0<m & 0<n)"; 

547 
by (nat_ind_tac "m" 1); 

548 
by (nat_ind_tac "n" 2); 

549 
by (ALLGOALS Asm_simp_tac); 

550 
qed "zero_less_mult_iff"; 

551 

1795  552 
goal Arith.thy "(m*n = 1) = (m=1 & n=1)"; 
553 
by (nat_ind_tac "m" 1); 

554 
by (Simp_tac 1); 

555 
by (nat_ind_tac "n" 1); 

556 
by (Simp_tac 1); 

557 
by (fast_tac (!claset addss !simpset) 1); 

558 
qed "mult_eq_1_iff"; 

559 

1713  560 
(*Cancellation law for division*) 
561 
goal Arith.thy "!!k. [ 0<n; 0<k ] ==> (k*m) div (k*n) = m div n"; 

562 
by (res_inst_tac [("n","m")] less_induct 1); 

563 
by (case_tac "na<n" 1); 

564 
by (asm_simp_tac (!simpset addsimps [div_less, zero_less_mult_iff, 

565 
mult_less_mono2]) 1); 

566 
by (subgoal_tac "~ k*na < k*n" 1); 

567 
by (asm_simp_tac 

568 
(!simpset addsimps [zero_less_mult_iff, div_geq, 

569 
diff_mult_distrib2 RS sym, diff_less]) 1); 

570 
by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, 

571 
le_refl RS mult_le_mono]) 1); 

572 
qed "div_cancel"; 

573 

574 
goal Arith.thy "!!k. [ 0<n; 0<k ] ==> (k*m) mod (k*n) = k * (m mod n)"; 

575 
by (res_inst_tac [("n","m")] less_induct 1); 

576 
by (case_tac "na<n" 1); 

577 
by (asm_simp_tac (!simpset addsimps [mod_less, zero_less_mult_iff, 

578 
mult_less_mono2]) 1); 

579 
by (subgoal_tac "~ k*na < k*n" 1); 

580 
by (asm_simp_tac 

581 
(!simpset addsimps [zero_less_mult_iff, mod_geq, 

582 
diff_mult_distrib2 RS sym, diff_less]) 1); 

583 
by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le, 

584 
le_refl RS mult_le_mono]) 1); 

585 
qed "mult_mod_distrib"; 

586 

587 

1795  588 
(** Lemma for gcd **) 
589 

590 
goal Arith.thy "!!m n. m = m*n ==> n=1  m=0"; 

591 
by (dtac sym 1); 

592 
by (rtac disjCI 1); 

593 
by (rtac nat_less_cases 1 THEN assume_tac 2); 

1909  594 
by (fast_tac (!claset addSEs [less_SucE] addss !simpset) 1); 
1979  595 
by (best_tac (!claset addDs [mult_less_mono2] 
1795  596 
addss (!simpset addsimps [zero_less_eq RS sym])) 1); 
597 
qed "mult_eq_self_implies_10"; 

598 

599 