author  lcp 
Thu, 30 Sep 1993 10:10:21 +0100  
changeset 14  1c0926788772 
parent 6  8ce8c4d13d4d 
child 25  3ac1c0c0016e 
permissions  rwrr 
0  1 
(* Title: ZF/arith.ML 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

5 

6 
For arith.thy. Arithmetic operators and their definitions 

7 

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

9 

10 
Could prove def_rec_0, def_rec_succ... 

11 
*) 

12 

13 
open Arith; 

14 

15 
(*"Difference" is subtraction of natural numbers. 

16 
There are no negative numbers; we have 

17 
m # n = 0 iff m<=n and m # n = succ(k) iff m>n. 

18 
Also, rec(m, 0, %z w.z) is pred(m). 

19 
*) 

20 

21 
(** rec  better than nat_rec; the succ case has no type requirement! **) 

22 

23 
val rec_trans = rec_def RS def_transrec RS trans; 

24 

25 
goal Arith.thy "rec(0,a,b) = a"; 

26 
by (rtac rec_trans 1); 

27 
by (rtac nat_case_0 1); 

28 
val rec_0 = result(); 

29 

30 
goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))"; 

31 
by (rtac rec_trans 1); 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

32 
by (simp_tac (ZF_ss addsimps [nat_case_succ, nat_succI]) 1); 
0  33 
val rec_succ = result(); 
34 

35 
val major::prems = goal Arith.thy 

36 
"[ n: nat; \ 

37 
\ a: C(0); \ 

38 
\ !!m z. [ m: nat; z: C(m) ] ==> b(m,z): C(succ(m)) \ 

39 
\ ] ==> rec(n,a,b) : C(n)"; 

40 
by (rtac (major RS nat_induct) 1); 

41 
by (ALLGOALS 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

42 
(asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ])))); 
0  43 
val rec_type = result(); 
44 

45 
val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat]; 

46 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

47 
val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks); 
0  48 

49 

50 
(** Addition **) 

51 

52 
val add_type = prove_goalw Arith.thy [add_def] 

53 
"[ m:nat; n:nat ] ==> m #+ n : nat" 

54 
(fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]); 

55 

56 
val add_0 = prove_goalw Arith.thy [add_def] 

57 
"0 #+ n = n" 

58 
(fn _ => [ (rtac rec_0 1) ]); 

59 

60 
val add_succ = prove_goalw Arith.thy [add_def] 

61 
"succ(m) #+ n = succ(m #+ n)" 

62 
(fn _=> [ (rtac rec_succ 1) ]); 

63 

64 
(** Multiplication **) 

65 

66 
val mult_type = prove_goalw Arith.thy [mult_def] 

67 
"[ m:nat; n:nat ] ==> m #* n : nat" 

68 
(fn prems=> 

69 
[ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]); 

70 

71 
val mult_0 = prove_goalw Arith.thy [mult_def] 

72 
"0 #* n = 0" 

73 
(fn _ => [ (rtac rec_0 1) ]); 

74 

75 
val mult_succ = prove_goalw Arith.thy [mult_def] 

76 
"succ(m) #* n = n #+ (m #* n)" 

77 
(fn _ => [ (rtac rec_succ 1) ]); 

78 

79 
(** Difference **) 

80 

81 
val diff_type = prove_goalw Arith.thy [diff_def] 

82 
"[ m:nat; n:nat ] ==> m # n : nat" 

83 
(fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]); 

84 

85 
val diff_0 = prove_goalw Arith.thy [diff_def] 

86 
"m # 0 = m" 

87 
(fn _ => [ (rtac rec_0 1) ]); 

88 

89 
val diff_0_eq_0 = prove_goalw Arith.thy [diff_def] 

90 
"n:nat ==> 0 # n = 0" 

91 
(fn [prem]=> 

92 
[ (rtac (prem RS nat_induct) 1), 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

93 
(ALLGOALS (asm_simp_tac nat_ss)) ]); 
0  94 

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

96 
succ(m) # succ(n) rewrites to pred(succ(m) # n) *) 

97 
val diff_succ_succ = prove_goalw Arith.thy [diff_def] 

98 
"[ m:nat; n:nat ] ==> succ(m) # succ(n) = m # n" 

99 
(fn prems=> 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

100 
[ (asm_simp_tac (nat_ss addsimps prems) 1), 
0  101 
(nat_ind_tac "n" prems 1), 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

102 
(ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]); 
0  103 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

104 
(*The conclusion is equivalent to m#n <= m *) 
0  105 
val prems = goal Arith.thy 
106 
"[ m:nat; n:nat ] ==> m # n : succ(m)"; 

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

108 
by (resolve_tac prems 1); 

109 
by (resolve_tac prems 1); 

110 
by (etac succE 3); 

111 
by (ALLGOALS 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

112 
(asm_simp_tac 
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

113 
(nat_ss addsimps (prems @ [succ_iff, diff_0, diff_0_eq_0, 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

114 
diff_succ_succ])))); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

115 
val diff_less_succ = result(); 
0  116 

117 
(*** Simplification over add, mult, diff ***) 

118 

119 
val arith_typechecks = [add_type, mult_type, diff_type]; 

120 
val arith_rews = [add_0, add_succ, 

121 
mult_0, mult_succ, 

122 
diff_0, diff_0_eq_0, diff_succ_succ]; 

123 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

124 
val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks); 
0  125 

126 
(*** Addition ***) 

127 

128 
(*Associative law for addition*) 

129 
val add_assoc = prove_goal Arith.thy 

130 
"m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)" 

131 
(fn prems=> 

132 
[ (nat_ind_tac "m" prems 1), 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

133 
(ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
0  134 

135 
(*The following two lemmas are used for add_commute and sometimes 

136 
elsewhere, since they are safe for rewriting.*) 

137 
val add_0_right = prove_goal Arith.thy 

138 
"m:nat ==> m #+ 0 = m" 

139 
(fn prems=> 

140 
[ (nat_ind_tac "m" prems 1), 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

141 
(ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
0  142 

143 
val add_succ_right = prove_goal Arith.thy 

144 
"m:nat ==> m #+ succ(n) = succ(m #+ n)" 

145 
(fn prems=> 

146 
[ (nat_ind_tac "m" prems 1), 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

147 
(ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
0  148 

149 
(*Commutative law for addition*) 

150 
val add_commute = prove_goal Arith.thy 

151 
"[ m:nat; n:nat ] ==> m #+ n = n #+ m" 

152 
(fn prems=> 

153 
[ (nat_ind_tac "n" prems 1), 

154 
(ALLGOALS 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

155 
(asm_simp_tac 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

156 
(arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]); 
0  157 

158 
(*Cancellation law on the left*) 

159 
val [knat,eqn] = goal Arith.thy 

160 
"[ k:nat; k #+ m = k #+ n ] ==> m=n"; 

161 
by (rtac (eqn RS rev_mp) 1); 

162 
by (nat_ind_tac "k" [knat] 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

163 
by (ALLGOALS (simp_tac arith_ss)); 
0  164 
by (fast_tac ZF_cs 1); 
165 
val add_left_cancel = result(); 

166 

167 
(*** Multiplication ***) 

168 

169 
(*right annihilation in product*) 

170 
val mult_0_right = prove_goal Arith.thy 

171 
"m:nat ==> m #* 0 = 0" 

172 
(fn prems=> 

173 
[ (nat_ind_tac "m" prems 1), 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

174 
(ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
0  175 

176 
(*right successor law for multiplication*) 

177 
val mult_succ_right = prove_goal Arith.thy 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

178 
"!!m n. [ m:nat; n:nat ] ==> m #* succ(n) = m #+ (m #* n)" 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

179 
(fn _=> 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

180 
[ (nat_ind_tac "m" [] 1), 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

181 
(ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))), 
0  182 
(*The final goal requires the commutative law for addition*) 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

183 
(rtac (add_commute RS subst_context) 1), 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

184 
(REPEAT (assume_tac 1)) ]); 
0  185 

186 
(*Commutative law for multiplication*) 

187 
val mult_commute = prove_goal Arith.thy 

188 
"[ m:nat; n:nat ] ==> m #* n = n #* m" 

189 
(fn prems=> 

190 
[ (nat_ind_tac "m" prems 1), 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

191 
(ALLGOALS (asm_simp_tac 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

192 
(arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]); 
0  193 

194 
(*addition distributes over multiplication*) 

195 
val add_mult_distrib = prove_goal Arith.thy 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

196 
"!!m n. [ m:nat; k:nat ] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)" 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

197 
(fn _=> 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

198 
[ (etac nat_induct 1), 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

199 
(ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))) ]); 
0  200 

201 
(*Distributive law on the left; requires an extra typing premise*) 

202 
val add_mult_distrib_left = prove_goal Arith.thy 

203 
"[ m:nat; n:nat; k:nat ] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)" 

204 
(fn prems=> 

205 
let val mult_commute' = read_instantiate [("m","k")] mult_commute 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

206 
val ss = arith_ss addsimps ([mult_commute',add_mult_distrib]@prems) 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

207 
in [ (simp_tac ss 1) ] 
0  208 
end); 
209 

210 
(*Associative law for multiplication*) 

211 
val mult_assoc = prove_goal Arith.thy 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

212 
"!!m n k. [ m:nat; n:nat; k:nat ] ==> (m #* n) #* k = m #* (n #* k)" 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

213 
(fn _=> 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

214 
[ (etac nat_induct 1), 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

215 
(ALLGOALS (asm_simp_tac (arith_ss addsimps [add_mult_distrib]))) ]); 
0  216 

217 

218 
(*** Difference ***) 

219 

220 
val diff_self_eq_0 = prove_goal Arith.thy 

221 
"m:nat ==> m # m = 0" 

222 
(fn prems=> 

223 
[ (nat_ind_tac "m" prems 1), 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

224 
(ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
0  225 

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

227 
val notless::prems = goal Arith.thy 

228 
"[ ~m:n; m:nat; n:nat ] ==> n #+ (m#n) = m"; 

229 
by (rtac (notless RS rev_mp) 1); 

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

231 
by (resolve_tac prems 1); 

232 
by (resolve_tac prems 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

233 
by (ALLGOALS (asm_simp_tac 
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

234 
(arith_ss addsimps (prems@[succ_mem_succ_iff, nat_0_in_succ, 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

235 
naturals_are_ordinals])))); 
0  236 
val add_diff_inverse = result(); 
237 

238 

239 
(*Subtraction is the inverse of addition. *) 

240 
val [mnat,nnat] = goal Arith.thy 

241 
"[ m:nat; n:nat ] ==> (n#+m) #n = m"; 

242 
by (rtac (nnat RS nat_induct) 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

243 
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat]))); 
0  244 
val diff_add_inverse = result(); 
245 

246 
val [mnat,nnat] = goal Arith.thy 

247 
"[ m:nat; n:nat ] ==> n # (n#+m) = 0"; 

248 
by (rtac (nnat RS nat_induct) 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

249 
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mnat]))); 
0  250 
val diff_add_0 = result(); 
251 

252 

253 
(*** Remainder ***) 

254 

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

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

256 
goal Arith.thy "!!m n. [ 0:n; ~ m:n; m:nat; n:nat ] ==> m # n : m"; 
0  257 
by (etac rev_mp 1); 
258 
by (etac rev_mp 1); 

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

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

260 
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_less_succ,diff_succ_succ]))); 
0  261 
val div_termination = result(); 
262 

263 
val div_rls = 

264 
[Ord_transrec_type, apply_type, div_termination, if_type] @ 

265 
nat_typechecks; 

266 

267 
(*Type checking depends upon termination!*) 

268 
val prems = goalw Arith.thy [mod_def] 

269 
"[ 0:n; m:nat; n:nat ] ==> m mod n : nat"; 

270 
by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1)); 

271 
val mod_type = result(); 

272 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

273 
val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination]; 
0  274 

275 
val prems = goal Arith.thy "[ 0:n; m:n; m:nat; n:nat ] ==> m mod n = m"; 

276 
by (rtac (mod_def RS def_transrec RS trans) 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

277 
by (simp_tac (div_ss addsimps prems) 1); 
0  278 
val mod_less = result(); 
279 

280 
val prems = goal Arith.thy 

281 
"[ 0:n; ~m:n; m:nat; n:nat ] ==> m mod n = (m#n) mod n"; 

282 
by (rtac (mod_def RS def_transrec RS trans) 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

283 
by (simp_tac (div_ss addsimps prems) 1); 
0  284 
val mod_geq = result(); 
285 

286 
(*** Quotient ***) 

287 

288 
(*Type checking depends upon termination!*) 

289 
val prems = goalw Arith.thy [div_def] 

290 
"[ 0:n; m:nat; n:nat ] ==> m div n : nat"; 

291 
by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1)); 

292 
val div_type = result(); 

293 

294 
val prems = goal Arith.thy 

295 
"[ 0:n; m:n; m:nat; n:nat ] ==> m div n = 0"; 

296 
by (rtac (div_def RS def_transrec RS trans) 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

297 
by (simp_tac (div_ss addsimps prems) 1); 
0  298 
val div_less = result(); 
299 

300 
val prems = goal Arith.thy 

301 
"[ 0:n; ~m:n; m:nat; n:nat ] ==> m div n = succ((m#n) div n)"; 

302 
by (rtac (div_def RS def_transrec RS trans) 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

303 
by (simp_tac (div_ss addsimps prems) 1); 
0  304 
val div_geq = result(); 
305 

306 
(*Main Result.*) 

307 
val prems = goal Arith.thy 

308 
"[ 0:n; m:nat; n:nat ] ==> (m div n)#*n #+ m mod n = m"; 

309 
by (res_inst_tac [("i","m")] complete_induct 1); 

310 
by (resolve_tac prems 1); 

311 
by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1); 

312 
by (ALLGOALS 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

313 
(asm_simp_tac 
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

314 
(arith_ss addsimps ([mod_type,div_type] @ prems @ 
0  315 
[mod_less,mod_geq, div_less, div_geq, 
316 
add_assoc, add_diff_inverse, div_termination])))); 

317 
val mod_div_equality = result(); 

318 

319 

320 
(**** Additional theorems about "less than" ****) 

321 

322 
val [mnat,nnat] = goal Arith.thy 

323 
"[ m:nat; n:nat ] ==> ~ (m #+ n) : n"; 

324 
by (rtac (mnat RS nat_induct) 1); 

6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

325 
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl]))); 
0  326 
by (rtac notI 1); 
327 
by (etac notE 1); 

328 
by (etac (succI1 RS Ord_trans) 1); 

329 
by (rtac (nnat RS naturals_are_ordinals) 1); 

330 
val add_not_less_self = result(); 

331 

332 
val [mnat,nnat] = goal Arith.thy 

333 
"[ m:nat; n:nat ] ==> m : succ(m #+ n)"; 

334 
by (rtac (mnat RS nat_induct) 1); 

335 
(*May not simplify even with ZF_ss because it would expand m:succ(...) *) 

336 
by (rtac (add_0 RS ssubst) 1); 

337 
by (rtac (add_succ RS ssubst) 2); 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

338 
by (REPEAT (ares_tac [nnat, nat_0_in_succ, succ_mem_succI, 
0  339 
naturals_are_ordinals, nat_succI, add_type] 1)); 
340 
val add_less_succ_self = result(); 

14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

341 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

342 
goal Arith.thy "!!m n. [ m:nat; n:nat ] ==> m <= m #+ n"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

343 
by (rtac (add_less_succ_self RS member_succD) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

344 
by (REPEAT (ares_tac [naturals_are_ordinals, add_type] 1)); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

345 
val add_leq_self = result(); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

346 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

347 
goal Arith.thy "!!m n. [ m:nat; n:nat ] ==> m <= n #+ m"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

348 
by (rtac (add_commute RS ssubst) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

349 
by (REPEAT (ares_tac [add_leq_self] 1)); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

350 
val add_leq_self2 = result(); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

351 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

352 
(** Monotonicity of addition **) 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

353 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

354 
(*strict, in 1st argument*) 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

355 
goal Arith.thy "!!i j k. [ i:j; j:nat ] ==> i#+k : j#+k"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

356 
by (etac succ_less_induct 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

357 
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [succ_iff]))); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

358 
val add_less_mono1 = result(); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

359 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

360 
(*strict, in both arguments*) 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

361 
goal Arith.thy "!!i j k l. [ i:j; k:l; j:nat; l:nat ] ==> i#+k : j#+l"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

362 
by (rtac (add_less_mono1 RS Ord_trans) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

363 
by (REPEAT_FIRST (ares_tac [add_type, naturals_are_ordinals])); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

364 
by (EVERY [rtac (add_commute RS ssubst) 1, 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

365 
rtac (add_commute RS ssubst) 3, 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

366 
rtac add_less_mono1 5]); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

367 
by (REPEAT (ares_tac [Ord_nat RSN (3,Ord_trans)] 1)); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

368 
val add_less_mono = result(); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

369 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

370 
(*A [clumsy] way of lifting < monotonictity to <= monotonicity *) 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

371 
val less_mono::ford::prems = goal Ord.thy 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

372 
"[ !!i j. [ i:j; j:k ] ==> f(i) : f(j); \ 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

373 
\ !!i. i:k ==> f(i):k; \ 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

374 
\ i<=j; i:k; j:k; Ord(k) \ 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

375 
\ ] ==> f(i) <= f(j)"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

376 
by (cut_facts_tac prems 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

377 
by (rtac member_succD 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

378 
by (dtac member_succI 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

379 
by (fast_tac (ZF_cs addSIs [less_mono]) 3); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

380 
by (REPEAT (ares_tac [ford,Ord_in_Ord] 1)); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

381 
val Ord_less_mono_imp_mono = result(); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

382 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

383 
(*<=, in 1st argument*) 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

384 
goal Arith.thy 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

385 
"!!i j k. [ i<=j; i:nat; j:nat; k:nat ] ==> i#+k <= j#+k"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

386 
by (res_inst_tac [("f", "%j.j#+k")] Ord_less_mono_imp_mono 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

387 
by (REPEAT (ares_tac [add_less_mono1, add_type, Ord_nat] 1)); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

388 
val add_mono1 = result(); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

389 

1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

390 
(*<=, in both arguments*) 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

391 
goal Arith.thy 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

392 
"!!i j k. [ i<=j; k<=l; i:nat; j:nat; k:nat; l:nat ] ==> i#+k <= j#+l"; 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

393 
by (rtac (add_mono1 RS subset_trans) 1); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

394 
by (REPEAT (assume_tac 1)); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

395 
by (EVERY [rtac (add_commute RS ssubst) 1, 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

396 
rtac (add_commute RS ssubst) 3, 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

397 
rtac add_mono1 5]); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

398 
by (REPEAT (assume_tac 1)); 
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

399 
val add_mono = result(); 