author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 127  eec6bb9c58ea 
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 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

45 
val nat_le_refl = naturals_are_ordinals RS le_refl; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

46 

3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

47 
val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat]; 
0  48 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

49 
val nat_simps = [rec_0, rec_succ, not_lt0, nat_0_le, le0_iff, succ_le_iff, 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

50 
nat_le_refl]; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

51 

3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

52 
val nat_ss = ZF_ss addsimps (nat_simps @ nat_typechecks); 
0  53 

54 

55 
(** Addition **) 

56 

57 
val add_type = prove_goalw Arith.thy [add_def] 

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

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

60 

61 
val add_0 = prove_goalw Arith.thy [add_def] 

62 
"0 #+ n = n" 

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

64 

65 
val add_succ = prove_goalw Arith.thy [add_def] 

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

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

68 

69 
(** Multiplication **) 

70 

71 
val mult_type = prove_goalw Arith.thy [mult_def] 

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

73 
(fn prems=> 

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

75 

76 
val mult_0 = prove_goalw Arith.thy [mult_def] 

77 
"0 #* n = 0" 

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

79 

80 
val mult_succ = prove_goalw Arith.thy [mult_def] 

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

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

83 

84 
(** Difference **) 

85 

86 
val diff_type = prove_goalw Arith.thy [diff_def] 

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

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

89 

90 
val diff_0 = prove_goalw Arith.thy [diff_def] 

91 
"m # 0 = m" 

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

93 

94 
val diff_0_eq_0 = prove_goalw Arith.thy [diff_def] 

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

96 
(fn [prem]=> 

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

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

98 
(ALLGOALS (asm_simp_tac nat_ss)) ]); 
0  99 

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

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

102 
val diff_succ_succ = prove_goalw Arith.thy [diff_def] 

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

104 
(fn prems=> 

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

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

107 
(ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]); 
0  108 

109 
val prems = goal Arith.thy 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

110 
"[ m:nat; n:nat ] ==> m # n le m"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

111 
by (rtac (prems MRS diff_induct) 1); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

112 
by (etac leE 3); 
0  113 
by (ALLGOALS 
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset

114 
(asm_simp_tac 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

115 
(nat_ss addsimps (prems @ [le_iff, diff_0, diff_0_eq_0, 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

116 
diff_succ_succ, naturals_are_ordinals])))); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

117 
val diff_le_self = result(); 
0  118 

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

120 

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

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

122 
val arith_simps = [add_0, add_succ, 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

123 
mult_0, mult_succ, 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

124 
diff_0, diff_0_eq_0, diff_succ_succ]; 
0  125 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

126 
val arith_ss = nat_ss addsimps (arith_simps@arith_typechecks); 
0  127 

128 
(*** Addition ***) 

129 

130 
(*Associative law for addition*) 

131 
val add_assoc = prove_goal Arith.thy 

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

133 
(fn prems=> 

134 
[ (nat_ind_tac "m" prems 1), 

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

135 
(ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
0  136 

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

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

139 
val add_0_right = prove_goal Arith.thy 

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

141 
(fn prems=> 

142 
[ (nat_ind_tac "m" prems 1), 

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

143 
(ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
0  144 

145 
val add_succ_right = prove_goal Arith.thy 

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

147 
(fn prems=> 

148 
[ (nat_ind_tac "m" prems 1), 

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

149 
(ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
0  150 

151 
(*Commutative law for addition*) 

152 
val add_commute = prove_goal Arith.thy 

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

154 
(fn prems=> 

155 
[ (nat_ind_tac "n" prems 1), 

156 
(ALLGOALS 

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

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

158 
(arith_ss addsimps (prems@[add_0_right, add_succ_right])))) ]); 
0  159 

160 
(*Cancellation law on the left*) 

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

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

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

164 
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

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

168 

169 
(*** Multiplication ***) 

170 

171 
(*right annihilation in product*) 

172 
val mult_0_right = prove_goal Arith.thy 

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

174 
(fn prems=> 

175 
[ (nat_ind_tac "m" prems 1), 

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

176 
(ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
0  177 

178 
(*right successor law for multiplication*) 

179 
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

180 
"!!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

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

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

183 
(ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))), 
0  184 
(*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

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

186 
(REPEAT (assume_tac 1)) ]); 
0  187 

188 
(*Commutative law for multiplication*) 

189 
val mult_commute = prove_goal Arith.thy 

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

191 
(fn prems=> 

192 
[ (nat_ind_tac "m" prems 1), 

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

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

194 
(arith_ss addsimps (prems@[mult_0_right, mult_succ_right])))) ]); 
0  195 

196 
(*addition distributes over multiplication*) 

197 
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

198 
"!!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

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

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

201 
(ALLGOALS (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]))) ]); 
0  202 

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

204 
val add_mult_distrib_left = prove_goal Arith.thy 

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

206 
(fn prems=> 

207 
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

208 
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

209 
in [ (simp_tac ss 1) ] 
0  210 
end); 
211 

212 
(*Associative law for multiplication*) 

213 
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

214 
"!!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

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

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

217 
(ALLGOALS (asm_simp_tac (arith_ss addsimps [add_mult_distrib]))) ]); 
0  218 

219 

220 
(*** Difference ***) 

221 

222 
val diff_self_eq_0 = prove_goal Arith.thy 

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

224 
(fn prems=> 

225 
[ (nat_ind_tac "m" prems 1), 

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

226 
(ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]); 
0  227 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

228 
(*Addition is the inverse of subtraction*) 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

229 
goal Arith.thy "!!m n. [ n le m; m:nat ] ==> n #+ (m#n) = m"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

230 
by (forward_tac [lt_nat_in_nat] 1); 
127  231 
by (etac nat_succI 1); 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

232 
by (etac rev_mp 1); 
0  233 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

234 
by (ALLGOALS (asm_simp_tac arith_ss)); 
0  235 
val add_diff_inverse = result(); 
236 

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

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

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

240 
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

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

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

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

246 
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

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

250 

251 
(*** Remainder ***) 

252 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

253 
goal Arith.thy "!!m n. [ 0<n; n le m; m:nat ] ==> m # n < m"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

254 
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); 
0  255 
by (etac rev_mp 1); 
256 
by (etac rev_mp 1); 

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

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

258 
by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_le_self,diff_succ_succ]))); 
0  259 
val div_termination = result(); 
260 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

261 
val div_rls = (*for mod and div*) 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

262 
nat_typechecks @ 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

263 
[Ord_transrec_type, apply_type, div_termination RS ltD, if_type, 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

264 
naturals_are_ordinals, not_lt_iff_le RS iffD1]; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

265 

3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

266 
val div_ss = ZF_ss addsimps [naturals_are_ordinals, div_termination RS ltD, 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

267 
not_lt_iff_le RS iffD2]; 
0  268 

269 
(*Type checking depends upon termination!*) 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

270 
goalw Arith.thy [mod_def] "!!m n. [ 0<n; m:nat; n:nat ] ==> m mod n : nat"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

271 
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1)); 
0  272 
val mod_type = result(); 
273 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

274 
goal Arith.thy "!!m n. [ 0<n; m<n ] ==> m mod n = m"; 
0  275 
by (rtac (mod_def RS def_transrec RS trans) 1); 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

276 
by (asm_simp_tac div_ss 1); 
0  277 
val mod_less = result(); 
278 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

279 
goal Arith.thy "!!m n. [ 0<n; n le m; m:nat ] ==> m mod n = (m#n) mod n"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

280 
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); 
0  281 
by (rtac (mod_def RS def_transrec RS trans) 1); 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

282 
by (asm_simp_tac div_ss 1); 
0  283 
val mod_geq = result(); 
284 

285 
(*** Quotient ***) 

286 

287 
(*Type checking depends upon termination!*) 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

288 
goalw Arith.thy [div_def] 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

289 
"!!m n. [ 0<n; m:nat; n:nat ] ==> m div n : nat"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

290 
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1)); 
0  291 
val div_type = result(); 
292 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

293 
goal Arith.thy "!!m n. [ 0<n; m<n ] ==> m div n = 0"; 
0  294 
by (rtac (div_def RS def_transrec RS trans) 1); 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

295 
by (asm_simp_tac div_ss 1); 
0  296 
val div_less = result(); 
297 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

298 
goal Arith.thy 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

299 
"!!m n. [ 0<n; n le m; m:nat ] ==> m div n = succ((m#n) div n)"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

300 
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); 
0  301 
by (rtac (div_def RS def_transrec RS trans) 1); 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

302 
by (asm_simp_tac div_ss 1); 
0  303 
val div_geq = result(); 
304 

305 
(*Main Result.*) 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

306 
goal Arith.thy 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

307 
"!!m n. [ 0<n; m:nat; n:nat ] ==> (m div n)#*n #+ m mod n = m"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

308 
by (etac complete_induct 1); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

309 
by (res_inst_tac [("Q","x<n")] (excluded_middle RS disjE) 1); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

310 
(*case x<n*) 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

311 
by (asm_simp_tac (arith_ss addsimps [mod_less, div_less]) 2); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

312 
(*case n le x*) 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

313 
by (asm_full_simp_tac 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

314 
(arith_ss addsimps [not_lt_iff_le, naturals_are_ordinals, 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

315 
mod_geq, div_geq, add_assoc, 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

316 
div_termination RS ltD, add_diff_inverse]) 1); 
0  317 
val mod_div_equality = result(); 
318 

319 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

320 
(**** Additional theorems about "le" ****) 
0  321 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

322 
goal Arith.thy "!!m n. [ m:nat; n:nat ] ==> m le m #+ n"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

323 
by (etac nat_induct 1); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

324 
by (ALLGOALS (asm_simp_tac arith_ss)); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

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

326 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

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

328 
by (rtac (add_commute RS ssubst) 1); 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

329 
by (REPEAT (ares_tac [add_le_self] 1)); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

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

331 

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

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

333 

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

334 
(*strict, in 1st argument*) 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

335 
goal Arith.thy "!!i j k. [ i<j; j:nat; k:nat ] ==> i#+k < j#+k"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

336 
by (forward_tac [lt_nat_in_nat] 1); 
127  337 
by (assume_tac 1); 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

338 
by (etac succ_lt_induct 1); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

339 
by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI]))); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

340 
val add_lt_mono1 = 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 
(*strict, in both arguments*) 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

343 
goal Arith.thy "!!i j k l. [ i<j; k<l; j:nat; l:nat ] ==> i#+k < j#+l"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

344 
by (rtac (add_lt_mono1 RS lt_trans) 1); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

345 
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1)); 
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

346 
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

347 
rtac (add_commute RS ssubst) 3, 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

348 
rtac add_lt_mono1 5]); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

349 
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1)); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

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

351 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

352 
(*A [clumsy] way of lifting < monotonicity to le monotonicity *) 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

353 
val lt_mono::ford::prems = goal Ord.thy 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

354 
"[ !!i j. [ i<j; j:k ] ==> f(i) < f(j); \ 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

355 
\ !!i. i:k ==> Ord(f(i)); \ 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

356 
\ i le j; j:k \ 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

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

358 
by (cut_facts_tac prems 1); 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

359 
by (fast_tac (lt_cs addSIs [lt_mono,ford] addSEs [leE]) 1); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

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

361 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

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

363 
goal Arith.thy 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

364 
"!!i j k. [ i le j; j:nat; k:nat ] ==> i#+k le j#+k"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

365 
by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

366 
by (REPEAT (ares_tac [add_lt_mono1, add_type RS naturals_are_ordinals] 1)); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

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

368 

25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

369 
(* le monotonicity, BOTH arguments*) 
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

370 
goal Arith.thy 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

371 
"!!i j k. [ i le j; k le l; j:nat; l:nat ] ==> i#+k le j#+l"; 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

372 
by (rtac (add_le_mono1 RS le_trans) 1); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

373 
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); 
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
6
diff
changeset

374 
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

375 
rtac (add_commute RS ssubst) 3, 
25
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

376 
rtac add_le_mono1 5]); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

377 
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1)); 
3ac1c0c0016e
ordinal: DEFINITION of < and le to replace : and <= on ordinals! Many
lcp
parents:
14
diff
changeset

378 
val add_le_mono = result(); 