author  paulson 
Fri, 18 Feb 2000 15:28:32 +0100  
changeset 8252  af44242c5e7a 
parent 8100  6186ee807f2e 
child 8352  0fda5ba36934 
permissions  rwrr 
1465  1 
(* Title: HOL/Arith.ML 
923  2 
ID: $Id$ 
1465  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
4736  4 
Copyright 1998 University of Cambridge 
923  5 

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

3234  7 
Some from the Hoare example from Norbert Galm 
923  8 
*) 
9 

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

11 

3896
ee8ebb74ec00
Various new lemmas. Improved conversion of equations to rewrite rules:
nipkow
parents:
3842
diff
changeset

12 

923  13 
(** Difference **) 
14 

7007  15 
Goal "0  n = 0"; 
16 
by (induct_tac "n" 1); 

17 
by (ALLGOALS Asm_simp_tac); 

18 
qed "diff_0_eq_0"; 

923  19 

5429  20 
(*Must simplify BEFORE the induction! (Else we get a critical pair) 
923  21 
Suc(m)  Suc(n) rewrites to pred(Suc(m)  n) *) 
7007  22 
Goal "Suc(m)  Suc(n) = m  n"; 
23 
by (Simp_tac 1); 

24 
by (induct_tac "n" 1); 

25 
by (ALLGOALS Asm_simp_tac); 

26 
qed "diff_Suc_Suc"; 

923  27 

2682
13cdbf95ed92
minor changes due to new primrec definitions for +,,*
pusch
parents:
2498
diff
changeset

28 
Addsimps [diff_0_eq_0, diff_Suc_Suc]; 
923  29 

4360  30 
(* Could be (and is, below) generalized in various ways; 
31 
However, none of the generalizations are currently in the simpset, 

32 
and I dread to think what happens if I put them in *) 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

33 
Goal "0 < n ==> Suc(n1) = n"; 
5183  34 
by (asm_simp_tac (simpset() addsplits [nat.split]) 1); 
4360  35 
qed "Suc_pred"; 
36 
Addsimps [Suc_pred]; 

37 

38 
Delsimps [diff_Suc]; 

39 

923  40 

41 
(**** Inductive properties of the operators ****) 

42 

43 
(*** Addition ***) 

44 

7007  45 
Goal "m + 0 = m"; 
46 
by (induct_tac "m" 1); 

47 
by (ALLGOALS Asm_simp_tac); 

48 
qed "add_0_right"; 

923  49 

7007  50 
Goal "m + Suc(n) = Suc(m+n)"; 
51 
by (induct_tac "m" 1); 

52 
by (ALLGOALS Asm_simp_tac); 

53 
qed "add_Suc_right"; 

923  54 

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

55 
Addsimps [add_0_right,add_Suc_right]; 
923  56 

7007  57 

923  58 
(*Associative law for addition*) 
7007  59 
Goal "(m + n) + k = m + ((n + k)::nat)"; 
60 
by (induct_tac "m" 1); 

61 
by (ALLGOALS Asm_simp_tac); 

62 
qed "add_assoc"; 

923  63 

64 
(*Commutative law for addition*) 

7007  65 
Goal "m + n = n + (m::nat)"; 
66 
by (induct_tac "m" 1); 

67 
by (ALLGOALS Asm_simp_tac); 

68 
qed "add_commute"; 

923  69 

7007  70 
Goal "x+(y+z)=y+((x+z)::nat)"; 
71 
by (rtac (add_commute RS trans) 1); 

72 
by (rtac (add_assoc RS trans) 1); 

73 
by (rtac (add_commute RS arg_cong) 1); 

74 
qed "add_left_commute"; 

923  75 

76 
(*Addition is an ACoperator*) 

7428  77 
bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]); 
923  78 

5429  79 
Goal "(k + m = k + n) = (m=(n::nat))"; 
3339  80 
by (induct_tac "k" 1); 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

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

82 
by (Asm_simp_tac 1); 
923  83 
qed "add_left_cancel"; 
84 

5429  85 
Goal "(m + k = n + k) = (m=(n::nat))"; 
3339  86 
by (induct_tac "k" 1); 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

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

88 
by (Asm_simp_tac 1); 
923  89 
qed "add_right_cancel"; 
90 

5429  91 
Goal "(k + m <= k + n) = (m<=(n::nat))"; 
3339  92 
by (induct_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_le"; 
96 

5429  97 
Goal "(k + m < k + n) = (m<(n::nat))"; 
3339  98 
by (induct_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_left_cancel_less"; 
102 

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

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

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

105 

3339  106 
(** Reasoning about m+0=0, etc. **) 
107 

5069  108 
Goal "(m+n = 0) = (m=0 & n=0)"; 
5598  109 
by (exhaust_tac "m" 1); 
110 
by (Auto_tac); 

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

111 
qed "add_is_0"; 
4360  112 
AddIffs [add_is_0]; 
1327
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

113 

5598  114 
Goal "(0 = m+n) = (m=0 & n=0)"; 
115 
by (exhaust_tac "m" 1); 

116 
by (Auto_tac); 

117 
qed "zero_is_add"; 

118 
AddIffs [zero_is_add]; 

119 

120 
Goal "(m+n=1) = (m=1 & n=0  m=0 & n=1)"; 

6301  121 
by (exhaust_tac "m" 1); 
122 
by (Auto_tac); 

5598  123 
qed "add_is_1"; 
124 

125 
Goal "(1=m+n) = (m=1 & n=0  m=0 & n=1)"; 

6301  126 
by (exhaust_tac "m" 1); 
127 
by (Auto_tac); 

5598  128 
qed "one_is_add"; 
129 

5069  130 
Goal "(0<m+n) = (0<m  0<n)"; 
4423  131 
by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1); 
4360  132 
qed "add_gr_0"; 
133 
AddIffs [add_gr_0]; 

134 

5429  135 
(* Could be generalized, eg to "k<n ==> m+(n(Suc k)) = (m+n)(Suc k)" *) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

136 
Goal "0<n ==> m + (n1) = (m+n)1"; 
4360  137 
by (exhaust_tac "m" 1); 
6075  138 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n] 
5183  139 
addsplits [nat.split]))); 
1327
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

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

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

142 

5429  143 
Goal "m + n = m ==> n = 0"; 
5078  144 
by (dtac (add_0_right RS ssubst) 1); 
145 
by (asm_full_simp_tac (simpset() addsimps [add_assoc] 

146 
delsimps [add_0_right]) 1); 

147 
qed "add_eq_self_zero"; 

148 

1626  149 

923  150 
(**** Additional theorems about "less than" ****) 
151 

5078  152 
(*Deleted less_natE; instead use less_eq_Suc_add RS exE*) 
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

153 
Goal "m<n > (? k. n=Suc(m+k))"; 
3339  154 
by (induct_tac "n" 1); 
5604  155 
by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less]))); 
4089  156 
by (blast_tac (claset() addSEs [less_SucE] 
5497  157 
addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1); 
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1475
diff
changeset

158 
qed_spec_mp "less_eq_Suc_add"; 
923  159 

5069  160 
Goal "n <= ((m + n)::nat)"; 
3339  161 
by (induct_tac "m" 1); 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

162 
by (ALLGOALS Simp_tac); 
5983  163 
by (etac le_SucI 1); 
923  164 
qed "le_add2"; 
165 

5069  166 
Goal "n <= ((n + m)::nat)"; 
4089  167 
by (simp_tac (simpset() addsimps add_ac) 1); 
923  168 
by (rtac le_add2 1); 
169 
qed "le_add1"; 

170 

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

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

173 

5429  174 
Goal "(m<n) = (? k. n=Suc(m+k))"; 
175 
by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1); 

176 
qed "less_iff_Suc_add"; 

177 

178 

923  179 
(*"i <= j ==> i <= j+m"*) 
180 
bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans)); 

181 

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

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

184 

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

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

187 

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

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

190 

5654  191 
Goal "i+j < (k::nat) > i<k"; 
3339  192 
by (induct_tac "j" 1); 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

193 
by (ALLGOALS Asm_simp_tac); 
6301  194 
by (blast_tac (claset() addDs [Suc_lessD]) 1); 
5654  195 
qed_spec_mp "add_lessD1"; 
1152  196 

5429  197 
Goal "~ (i+j < (i::nat))"; 
3457  198 
by (rtac notI 1); 
199 
by (etac (add_lessD1 RS less_irrefl) 1); 

3234  200 
qed "not_add_less1"; 
201 

5429  202 
Goal "~ (j+i < (i::nat))"; 
4089  203 
by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1); 
3234  204 
qed "not_add_less2"; 
205 
AddIffs [not_add_less1, not_add_less2]; 

206 

5069  207 
Goal "m+k<=n > m<=(n::nat)"; 
3339  208 
by (induct_tac "k" 1); 
5497  209 
by (ALLGOALS (asm_simp_tac (simpset() addsimps le_simps))); 
1485
240cc98b94a7
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
nipkow
parents:
1475
diff
changeset

210 
qed_spec_mp "add_leD1"; 
923  211 

5429  212 
Goal "m+k<=n ==> k<=(n::nat)"; 
4089  213 
by (full_simp_tac (simpset() addsimps [add_commute]) 1); 
2498  214 
by (etac add_leD1 1); 
215 
qed_spec_mp "add_leD2"; 

216 

5429  217 
Goal "m+k<=n ==> m<=n & k<=(n::nat)"; 
4089  218 
by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1); 
2498  219 
bind_thm ("add_leE", result() RS conjE); 
220 

5429  221 
(*needs !!k for add_ac to work*) 
222 
Goal "!!k:: nat. [ k<l; m+l = k+n ] ==> m<n"; 

5758
27a2b36efd95
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5654
diff
changeset

223 
by (force_tac (claset(), 
5497  224 
simpset() delsimps [add_Suc_right] 
5537  225 
addsimps [less_iff_Suc_add, 
5758
27a2b36efd95
corrected auto_tac (applications of unsafe wrappers)
oheimb
parents:
5654
diff
changeset

226 
add_Suc_right RS sym] @ add_ac) 1); 
923  227 
qed "less_add_eq_less"; 
228 

229 

1713  230 
(*** Monotonicity of Addition ***) 
923  231 

232 
(*strict, in 1st argument*) 

5429  233 
Goal "i < j ==> i + k < j + (k::nat)"; 
3339  234 
by (induct_tac "k" 1); 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

235 
by (ALLGOALS Asm_simp_tac); 
923  236 
qed "add_less_mono1"; 
237 

238 
(*strict, in both arguments*) 

5429  239 
Goal "[i < j; k < l] ==> i + k < j + (l::nat)"; 
923  240 
by (rtac (add_less_mono1 RS less_trans) 1); 
1198  241 
by (REPEAT (assume_tac 1)); 
3339  242 
by (induct_tac "j" 1); 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

243 
by (ALLGOALS Asm_simp_tac); 
923  244 
qed "add_less_mono"; 
245 

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

5316  247 
val [lt_mono,le] = Goal 
1465  248 
"[ !!i j::nat. i<j ==> f(i) < f(j); \ 
249 
\ i <= j \ 

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

5604  252 
by (asm_full_simp_tac (simpset() addsimps [order_le_less]) 1); 
4089  253 
by (blast_tac (claset() addSIs [lt_mono]) 1); 
923  254 
qed "less_mono_imp_le_mono"; 
255 

256 
(*nonstrict, in 1st argument*) 

5429  257 
Goal "i<=j ==> i + k <= j + (k::nat)"; 
3842  258 
by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1); 
1552  259 
by (etac add_less_mono1 1); 
923  260 
by (assume_tac 1); 
261 
qed "add_le_mono1"; 

262 

263 
(*nonstrict, in both arguments*) 

5429  264 
Goal "[i<=j; k<=l ] ==> i + k <= j + (l::nat)"; 
923  265 
by (etac (add_le_mono1 RS le_trans) 1); 
4089  266 
by (simp_tac (simpset() addsimps [add_commute]) 1); 
923  267 
qed "add_le_mono"; 
1713  268 

3234  269 

270 
(*** Multiplication ***) 

271 

272 
(*right annihilation in product*) 

7007  273 
Goal "m * 0 = 0"; 
274 
by (induct_tac "m" 1); 

275 
by (ALLGOALS Asm_simp_tac); 

276 
qed "mult_0_right"; 

3234  277 

3293  278 
(*right successor law for multiplication*) 
7007  279 
Goal "m * Suc(n) = m + (m * n)"; 
280 
by (induct_tac "m" 1); 

281 
by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))); 

282 
qed "mult_Suc_right"; 

3234  283 

3293  284 
Addsimps [mult_0_right, mult_Suc_right]; 
3234  285 

5069  286 
Goal "1 * n = n"; 
3234  287 
by (Asm_simp_tac 1); 
288 
qed "mult_1"; 

289 

5069  290 
Goal "n * 1 = n"; 
3234  291 
by (Asm_simp_tac 1); 
292 
qed "mult_1_right"; 

293 

294 
(*Commutative law for multiplication*) 

7007  295 
Goal "m * n = n * (m::nat)"; 
296 
by (induct_tac "m" 1); 

297 
by (ALLGOALS Asm_simp_tac); 

298 
qed "mult_commute"; 

3234  299 

300 
(*addition distributes over multiplication*) 

7007  301 
Goal "(m + n)*k = (m*k) + ((n*k)::nat)"; 
302 
by (induct_tac "m" 1); 

303 
by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))); 

304 
qed "add_mult_distrib"; 

3234  305 

7007  306 
Goal "k*(m + n) = (k*m) + ((k*n)::nat)"; 
307 
by (induct_tac "m" 1); 

308 
by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))); 

309 
qed "add_mult_distrib2"; 

3234  310 

311 
(*Associative law for multiplication*) 

7007  312 
Goal "(m * n) * k = m * ((n * k)::nat)"; 
313 
by (induct_tac "m" 1); 

314 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))); 

315 
qed "mult_assoc"; 

3234  316 

7007  317 
Goal "x*(y*z) = y*((x*z)::nat)"; 
318 
by (rtac trans 1); 

319 
by (rtac mult_commute 1); 

320 
by (rtac trans 1); 

321 
by (rtac mult_assoc 1); 

322 
by (rtac (mult_commute RS arg_cong) 1); 

323 
qed "mult_left_commute"; 

3234  324 

7428  325 
bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]); 
3234  326 

5069  327 
Goal "(m*n = 0) = (m=0  n=0)"; 
3339  328 
by (induct_tac "m" 1); 
329 
by (induct_tac "n" 2); 

3293  330 
by (ALLGOALS Asm_simp_tac); 
331 
qed "mult_is_0"; 

7622  332 

333 
Goal "(0 = m*n) = (0=m  0=n)"; 

334 
by (cut_facts_tac [mult_is_0] 1); 

335 
by (full_simp_tac (simpset() addsimps [eq_commute]) 1); 

336 
qed "zero_is_mult"; 

337 

338 
Addsimps [mult_is_0, zero_is_mult]; 

3293  339 

5429  340 
Goal "m <= m*(m::nat)"; 
4158  341 
by (induct_tac "m" 1); 
342 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym]))); 

343 
by (etac (le_add2 RSN (2,le_trans)) 1); 

344 
qed "le_square"; 

345 

3234  346 

347 
(*** Difference ***) 

348 

7007  349 
Goal "m  m = 0"; 
350 
by (induct_tac "m" 1); 

351 
by (ALLGOALS Asm_simp_tac); 

352 
qed "diff_self_eq_0"; 

3234  353 

354 
Addsimps [diff_self_eq_0]; 

355 

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

5069  357 
Goal "~ m<n > n+(mn) = (m::nat)"; 
3234  358 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
3352  359 
by (ALLGOALS Asm_simp_tac); 
3381
2bac33ec2b0d
New theorems le_add_diff_inverse, le_add_diff_inverse2
paulson
parents:
3366
diff
changeset

360 
qed_spec_mp "add_diff_inverse"; 
2bac33ec2b0d
New theorems le_add_diff_inverse, le_add_diff_inverse2
paulson
parents:
3366
diff
changeset

361 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

362 
Goal "n<=m ==> n+(mn) = (m::nat)"; 
4089  363 
by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1); 
3381
2bac33ec2b0d
New theorems le_add_diff_inverse, le_add_diff_inverse2
paulson
parents:
3366
diff
changeset

364 
qed "le_add_diff_inverse"; 
3234  365 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

366 
Goal "n<=m ==> (mn)+n = (m::nat)"; 
4089  367 
by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1); 
3381
2bac33ec2b0d
New theorems le_add_diff_inverse, le_add_diff_inverse2
paulson
parents:
3366
diff
changeset

368 
qed "le_add_diff_inverse2"; 
2bac33ec2b0d
New theorems le_add_diff_inverse, le_add_diff_inverse2
paulson
parents:
3366
diff
changeset

369 

2bac33ec2b0d
New theorems le_add_diff_inverse, le_add_diff_inverse2
paulson
parents:
3366
diff
changeset

370 
Addsimps [le_add_diff_inverse, le_add_diff_inverse2]; 
3234  371 

372 

373 
(*** More results about difference ***) 

374 

5414
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

375 
Goal "n <= m ==> Suc(m)n = Suc(mn)"; 
5316  376 
by (etac rev_mp 1); 
3352  377 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
378 
by (ALLGOALS Asm_simp_tac); 

5414
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

379 
qed "Suc_diff_le"; 
3352  380 

5069  381 
Goal "m  n < Suc(m)"; 
3234  382 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
383 
by (etac less_SucE 3); 

4089  384 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq]))); 
3234  385 
qed "diff_less_Suc"; 
386 

5429  387 
Goal "m  n <= (m::nat)"; 
3234  388 
by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1); 
6075  389 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI]))); 
3234  390 
qed "diff_le_self"; 
3903
1b29151a1009
New simprule diff_le_self, requiring a new proof of diff_diff_cancel
paulson
parents:
3896
diff
changeset

391 
Addsimps [diff_le_self]; 
3234  392 

4732  393 
(* j<k ==> jn < k *) 
394 
bind_thm ("less_imp_diff_less", diff_le_self RS le_less_trans); 

395 

5069  396 
Goal "!!i::nat. ijk = i  (j+k)"; 
3352  397 
by (res_inst_tac [("m","i"),("n","j")] diff_induct 1); 
398 
by (ALLGOALS Asm_simp_tac); 

399 
qed "diff_diff_left"; 

400 

5069  401 
Goal "(Suc m  n)  Suc k = m  n  k"; 
4423  402 
by (simp_tac (simpset() addsimps [diff_diff_left]) 1); 
4736  403 
qed "Suc_diff_diff"; 
404 
Addsimps [Suc_diff_diff]; 

4360  405 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

406 
Goal "0<n ==> n  Suc i < n"; 
5183  407 
by (exhaust_tac "n" 1); 
4732  408 
by Safe_tac; 
5497  409 
by (asm_simp_tac (simpset() addsimps le_simps) 1); 
4732  410 
qed "diff_Suc_less"; 
411 
Addsimps [diff_Suc_less]; 

412 

3396  413 
(*This and the next few suggested by Florian Kammueller*) 
5069  414 
Goal "!!i::nat. ijk = ikj"; 
4089  415 
by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1); 
3352  416 
qed "diff_commute"; 
417 

5429  418 
Goal "k<=j > j<=i > i  (j  k) = i  j + (k::nat)"; 
3352  419 
by (res_inst_tac [("m","i"),("n","j")] diff_induct 1); 
420 
by (ALLGOALS Asm_simp_tac); 

5414
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

421 
by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_Suc_eq]) 1); 
3352  422 
qed_spec_mp "diff_diff_right"; 
423 

5429  424 
Goal "k <= (j::nat) > (i + j)  k = i + (j  k)"; 
3352  425 
by (res_inst_tac [("m","j"),("n","k")] diff_induct 1); 
426 
by (ALLGOALS Asm_simp_tac); 

427 
qed_spec_mp "diff_add_assoc"; 

428 

5429  429 
Goal "k <= (j::nat) > (j + i)  k = i + (j  k)"; 
4732  430 
by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1); 
431 
qed_spec_mp "diff_add_assoc2"; 

432 

5429  433 
Goal "(n+m)  n = (m::nat)"; 
3339  434 
by (induct_tac "n" 1); 
3234  435 
by (ALLGOALS Asm_simp_tac); 
436 
qed "diff_add_inverse"; 

437 
Addsimps [diff_add_inverse]; 

438 

5429  439 
Goal "(m+n)  n = (m::nat)"; 
4089  440 
by (simp_tac (simpset() addsimps [diff_add_assoc]) 1); 
3234  441 
qed "diff_add_inverse2"; 
442 
Addsimps [diff_add_inverse2]; 

443 

5429  444 
Goal "i <= (j::nat) ==> (ji=k) = (j=k+i)"; 
3724  445 
by Safe_tac; 
3381
2bac33ec2b0d
New theorems le_add_diff_inverse, le_add_diff_inverse2
paulson
parents:
3366
diff
changeset

446 
by (ALLGOALS Asm_simp_tac); 
3366  447 
qed "le_imp_diff_is_add"; 
448 

5356  449 
Goal "(mn = 0) = (m <= n)"; 
3234  450 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
5497  451 
by (ALLGOALS Asm_simp_tac); 
5356  452 
qed "diff_is_0_eq"; 
7059  453 

454 
Goal "(0 = mn) = (m <= n)"; 

455 
by (stac (diff_is_0_eq RS sym) 1); 

456 
by (rtac eq_sym_conv 1); 

457 
qed "zero_is_diff_eq"; 

458 
Addsimps [diff_is_0_eq, zero_is_diff_eq]; 

3234  459 

5333
ea33e66dcedd
Some new theorems. zero_less_diff replaces less_imp_diff_positive
paulson
parents:
5329
diff
changeset

460 
Goal "(0<nm) = (m<n)"; 
3234  461 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
3352  462 
by (ALLGOALS Asm_simp_tac); 
5333
ea33e66dcedd
Some new theorems. zero_less_diff replaces less_imp_diff_positive
paulson
parents:
5329
diff
changeset

463 
qed "zero_less_diff"; 
ea33e66dcedd
Some new theorems. zero_less_diff replaces less_imp_diff_positive
paulson
parents:
5329
diff
changeset

464 
Addsimps [zero_less_diff]; 
3234  465 

5333
ea33e66dcedd
Some new theorems. zero_less_diff replaces less_imp_diff_positive
paulson
parents:
5329
diff
changeset

466 
Goal "i < j ==> ? k. 0<k & i+k = j"; 
5078  467 
by (res_inst_tac [("x","j  i")] exI 1); 
5333
ea33e66dcedd
Some new theorems. zero_less_diff replaces less_imp_diff_positive
paulson
parents:
5329
diff
changeset

468 
by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1); 
5078  469 
qed "less_imp_add_positive"; 
470 

5069  471 
Goal "P(k) > (!n. P(Suc(n))> P(n)) > P(ki)"; 
3234  472 
by (res_inst_tac [("m","k"),("n","i")] diff_induct 1); 
3718  473 
by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac)); 
3234  474 
qed "zero_induct_lemma"; 
475 

5316  476 
val prems = Goal "[ P(k); !!n. P(Suc(n)) ==> P(n) ] ==> P(0)"; 
3234  477 
by (rtac (diff_self_eq_0 RS subst) 1); 
478 
by (rtac (zero_induct_lemma RS mp RS mp) 1); 

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

480 
qed "zero_induct"; 

481 

5429  482 
Goal "(k+m)  (k+n) = m  (n::nat)"; 
3339  483 
by (induct_tac "k" 1); 
3234  484 
by (ALLGOALS Asm_simp_tac); 
485 
qed "diff_cancel"; 

486 
Addsimps [diff_cancel]; 

487 

5429  488 
Goal "(m+k)  (n+k) = m  (n::nat)"; 
3234  489 
val add_commute_k = read_instantiate [("n","k")] add_commute; 
5537  490 
by (asm_simp_tac (simpset() addsimps [add_commute_k]) 1); 
3234  491 
qed "diff_cancel2"; 
492 
Addsimps [diff_cancel2]; 

493 

5429  494 
Goal "n  (n+m) = 0"; 
3339  495 
by (induct_tac "n" 1); 
3234  496 
by (ALLGOALS Asm_simp_tac); 
497 
qed "diff_add_0"; 

498 
Addsimps [diff_add_0]; 

499 

5409  500 

3234  501 
(** Difference distributes over multiplication **) 
502 

5069  503 
Goal "!!m::nat. (m  n) * k = (m * k)  (n * k)"; 
3234  504 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
505 
by (ALLGOALS Asm_simp_tac); 

506 
qed "diff_mult_distrib" ; 

507 

5069  508 
Goal "!!m::nat. k * (m  n) = (k * m)  (k * n)"; 
3234  509 
val mult_commute_k = read_instantiate [("m","k")] mult_commute; 
4089  510 
by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1); 
3234  511 
qed "diff_mult_distrib2" ; 
512 
(*NOT added as rewrites, since sometimes they are used from righttoleft*) 

513 

514 

1713  515 
(*** Monotonicity of Multiplication ***) 
516 

5429  517 
Goal "i <= (j::nat) ==> i*k<=j*k"; 
3339  518 
by (induct_tac "k" 1); 
4089  519 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono]))); 
1713  520 
qed "mult_le_mono1"; 
521 

6987  522 
Goal "i <= (j::nat) ==> k*i <= k*j"; 
523 
by (dtac mult_le_mono1 1); 

524 
by (asm_simp_tac (simpset() addsimps [mult_commute]) 1); 

525 
qed "mult_le_mono2"; 

526 

527 
(* <= monotonicity, BOTH arguments*) 

5429  528 
Goal "[ i <= (j::nat); k <= l ] ==> i*k <= j*l"; 
2007  529 
by (etac (mult_le_mono1 RS le_trans) 1); 
6987  530 
by (etac mult_le_mono2 1); 
1713  531 
qed "mult_le_mono"; 
532 

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

5429  534 
Goal "[ i<j; 0<k ] ==> k*i < k*j"; 
5078  535 
by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1); 
1713  536 
by (Asm_simp_tac 1); 
3339  537 
by (induct_tac "x" 1); 
4089  538 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono]))); 
1713  539 
qed "mult_less_mono2"; 
540 

5429  541 
Goal "[ i<j; 0<k ] ==> i*k < j*k"; 
3457  542 
by (dtac mult_less_mono2 1); 
4089  543 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute]))); 
3234  544 
qed "mult_less_mono1"; 
545 

5069  546 
Goal "(0 < m*n) = (0<m & 0<n)"; 
3339  547 
by (induct_tac "m" 1); 
548 
by (induct_tac "n" 2); 

1713  549 
by (ALLGOALS Asm_simp_tac); 
550 
qed "zero_less_mult_iff"; 

4356  551 
Addsimps [zero_less_mult_iff]; 
1713  552 

5069  553 
Goal "(m*n = 1) = (m=1 & n=1)"; 
3339  554 
by (induct_tac "m" 1); 
1795  555 
by (Simp_tac 1); 
3339  556 
by (induct_tac "n" 1); 
1795  557 
by (Simp_tac 1); 
4089  558 
by (fast_tac (claset() addss simpset()) 1); 
1795  559 
qed "mult_eq_1_iff"; 
4356  560 
Addsimps [mult_eq_1_iff]; 
1795  561 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

562 
Goal "0<k ==> (m*k < n*k) = (m<n)"; 
4089  563 
by (safe_tac (claset() addSIs [mult_less_mono1])); 
3234  564 
by (cut_facts_tac [less_linear] 1); 
4389  565 
by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1); 
3234  566 
qed "mult_less_cancel2"; 
567 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

568 
Goal "0<k ==> (k*m < k*n) = (m<n)"; 
3457  569 
by (dtac mult_less_cancel2 1); 
4089  570 
by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1); 
3234  571 
qed "mult_less_cancel1"; 
572 
Addsimps [mult_less_cancel1, mult_less_cancel2]; 

573 

6864  574 
Goal "0<k ==> (m*k <= n*k) = (m<=n)"; 
575 
by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 

576 
qed "mult_le_cancel2"; 

577 

578 
Goal "0<k ==> (k*m <= k*n) = (m<=n)"; 

579 
by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 

580 
qed "mult_le_cancel1"; 

581 
Addsimps [mult_le_cancel1, mult_le_cancel2]; 

582 

5069  583 
Goal "(Suc k * m < Suc k * n) = (m < n)"; 
4423  584 
by (rtac mult_less_cancel1 1); 
4297
5defc2105cc8
added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
wenzelm
parents:
4158
diff
changeset

585 
by (Simp_tac 1); 
5defc2105cc8
added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
wenzelm
parents:
4158
diff
changeset

586 
qed "Suc_mult_less_cancel1"; 
5defc2105cc8
added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
wenzelm
parents:
4158
diff
changeset

587 

5069  588 
Goalw [le_def] "(Suc k * m <= Suc k * n) = (m <= n)"; 
4297
5defc2105cc8
added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
wenzelm
parents:
4158
diff
changeset

589 
by (simp_tac (simpset_of HOL.thy) 1); 
4423  590 
by (rtac Suc_mult_less_cancel1 1); 
4297
5defc2105cc8
added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
wenzelm
parents:
4158
diff
changeset

591 
qed "Suc_mult_le_cancel1"; 
5defc2105cc8
added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
wenzelm
parents:
4158
diff
changeset

592 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

593 
Goal "0<k ==> (m*k = n*k) = (m=n)"; 
3234  594 
by (cut_facts_tac [less_linear] 1); 
3724  595 
by Safe_tac; 
3457  596 
by (assume_tac 2); 
3234  597 
by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac)); 
598 
by (ALLGOALS Asm_full_simp_tac); 

599 
qed "mult_cancel2"; 

600 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

601 
Goal "0<k ==> (k*m = k*n) = (m=n)"; 
3457  602 
by (dtac mult_cancel2 1); 
4089  603 
by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1); 
3234  604 
qed "mult_cancel1"; 
605 
Addsimps [mult_cancel1, mult_cancel2]; 

606 

5069  607 
Goal "(Suc k * m = Suc k * n) = (m = n)"; 
4423  608 
by (rtac mult_cancel1 1); 
4297
5defc2105cc8
added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
wenzelm
parents:
4158
diff
changeset

609 
by (Simp_tac 1); 
5defc2105cc8
added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
wenzelm
parents:
4158
diff
changeset

610 
qed "Suc_mult_cancel1"; 
5defc2105cc8
added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
wenzelm
parents:
4158
diff
changeset

611 

3234  612 

1795  613 
(** Lemma for gcd **) 
614 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

615 
Goal "m = m*n ==> n=1  m=0"; 
1795  616 
by (dtac sym 1); 
617 
by (rtac disjCI 1); 

618 
by (rtac nat_less_cases 1 THEN assume_tac 2); 

4089  619 
by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1); 
4356  620 
by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1); 
1795  621 
qed "mult_eq_self_implies_10"; 
622 

623 

5983  624 

625 

626 
(**) 

627 
(* Various arithmetic proof procedures *) 

628 
(**) 

629 

630 
(**) 

631 
(* 1. Cancellation of common terms *) 

632 
(**) 

633 

634 
(* Title: HOL/arith_data.ML 

635 
ID: $Id$ 

636 
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen 

637 

638 
Setup various arithmetic proof procedures. 

639 
*) 

640 

641 
signature ARITH_DATA = 

642 
sig 

6055  643 
val nat_cancel_sums_add: simproc list 
5983  644 
val nat_cancel_sums: simproc list 
645 
val nat_cancel_factor: simproc list 

646 
val nat_cancel: simproc list 

647 
end; 

648 

649 
structure ArithData: ARITH_DATA = 

650 
struct 

651 

652 

653 
(** abstract syntax of structure nat: 0, Suc, + **) 

654 

655 
(* mk_sum, mk_norm_sum *) 

656 

657 
val one = HOLogic.mk_nat 1; 

658 
val mk_plus = HOLogic.mk_binop "op +"; 

659 

660 
fun mk_sum [] = HOLogic.zero 

661 
 mk_sum [t] = t 

662 
 mk_sum (t :: ts) = mk_plus (t, mk_sum ts); 

663 

664 
(*normal form of sums: Suc (... (Suc (a + (b + ...))))*) 

665 
fun mk_norm_sum ts = 

666 
let val (ones, sums) = partition (equal one) ts in 

667 
funpow (length ones) HOLogic.mk_Suc (mk_sum sums) 

668 
end; 

669 

670 

671 
(* dest_sum *) 

672 

673 
val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT; 

674 

675 
fun dest_sum tm = 

676 
if HOLogic.is_zero tm then [] 

677 
else 

678 
(case try HOLogic.dest_Suc tm of 

679 
Some t => one :: dest_sum t 

680 
 None => 

681 
(case try dest_plus tm of 

682 
Some (t, u) => dest_sum t @ dest_sum u 

683 
 None => [tm])); 

684 

685 

686 
(** generic proof tools **) 

687 

688 
(* prove conversions *) 

689 

690 
val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq; 

691 

692 
fun prove_conv expand_tac norm_tac sg (t, u) = 

693 
mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u))) 

694 
(K [expand_tac, norm_tac])) 

695 
handle ERROR => error ("The error(s) above occurred while trying to prove " ^ 

696 
(string_of_cterm (cterm_of sg (mk_eqv (t, u))))); 

697 

698 
val subst_equals = prove_goal HOL.thy "[ t = s; u = t ] ==> u = s" 

699 
(fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]); 

700 

701 

702 
(* rewriting *) 

703 

704 
fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules)); 

705 

706 
val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right]; 

707 
val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right]; 

708 

709 

710 

711 
(** cancel common summands **) 

712 

713 
structure Sum = 

714 
struct 

715 
val mk_sum = mk_norm_sum; 

716 
val dest_sum = dest_sum; 

717 
val prove_conv = prove_conv; 

718 
val norm_tac = simp_all add_rules THEN simp_all add_ac; 

719 
end; 

720 

721 
fun gen_uncancel_tac rule ct = 

722 
rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1; 

723 

724 

725 
(* nat eq *) 

726 

727 
structure EqCancelSums = CancelSumsFun 

728 
(struct 

729 
open Sum; 

730 
val mk_bal = HOLogic.mk_eq; 

731 
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT; 

732 
val uncancel_tac = gen_uncancel_tac add_left_cancel; 

733 
end); 

734 

735 

736 
(* nat less *) 

737 

738 
structure LessCancelSums = CancelSumsFun 

739 
(struct 

740 
open Sum; 

741 
val mk_bal = HOLogic.mk_binrel "op <"; 

742 
val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT; 

743 
val uncancel_tac = gen_uncancel_tac add_left_cancel_less; 

744 
end); 

745 

746 

747 
(* nat le *) 

748 

749 
structure LeCancelSums = CancelSumsFun 

750 
(struct 

751 
open Sum; 

752 
val mk_bal = HOLogic.mk_binrel "op <="; 

753 
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT; 

754 
val uncancel_tac = gen_uncancel_tac add_left_cancel_le; 

755 
end); 

756 

757 

758 
(* nat diff *) 

759 

760 
structure DiffCancelSums = CancelSumsFun 

761 
(struct 

762 
open Sum; 

763 
val mk_bal = HOLogic.mk_binop "op "; 

764 
val dest_bal = HOLogic.dest_bin "op " HOLogic.natT; 

765 
val uncancel_tac = gen_uncancel_tac diff_cancel; 

766 
end); 

767 

768 

769 

770 
(** cancel common factor **) 

771 

772 
structure Factor = 

773 
struct 

774 
val mk_sum = mk_norm_sum; 

775 
val dest_sum = dest_sum; 

776 
val prove_conv = prove_conv; 

777 
val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac; 

778 
end; 

779 

6394  780 
fun mk_cnat n = cterm_of (Theory.sign_of Nat.thy) (HOLogic.mk_nat n); 
5983  781 

782 
fun gen_multiply_tac rule k = 

783 
if k > 0 then 

784 
rtac (instantiate' [] [None, Some (mk_cnat (k  1))] (rule RS subst_equals)) 1 

785 
else no_tac; 

786 

787 

788 
(* nat eq *) 

789 

790 
structure EqCancelFactor = CancelFactorFun 

791 
(struct 

792 
open Factor; 

793 
val mk_bal = HOLogic.mk_eq; 

794 
val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT; 

795 
val multiply_tac = gen_multiply_tac Suc_mult_cancel1; 

796 
end); 

797 

798 

799 
(* nat less *) 

800 

801 
structure LessCancelFactor = CancelFactorFun 

802 
(struct 

803 
open Factor; 

804 
val mk_bal = HOLogic.mk_binrel "op <"; 

805 
val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT; 

806 
val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1; 

807 
end); 

808 

809 

810 
(* nat le *) 

811 

812 
structure LeCancelFactor = CancelFactorFun 

813 
(struct 

814 
open Factor; 

815 
val mk_bal = HOLogic.mk_binrel "op <="; 

816 
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT; 

817 
val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1; 

818 
end); 

819 

820 

821 

822 
(** prepare nat_cancel simprocs **) 

823 

8100  824 
fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termT); 
5983  825 
val prep_pats = map prep_pat; 
826 

827 
fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; 

828 

829 
val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]; 

830 
val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]; 

831 
val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]; 

832 
val diff_pats = prep_pats ["((l::nat) + m)  n", "(l::nat)  (m + n)", "Suc m  n", "m  Suc n"]; 

833 

6055  834 
val nat_cancel_sums_add = map prep_simproc 
5983  835 
[("nateq_cancel_sums", eq_pats, EqCancelSums.proc), 
836 
("natless_cancel_sums", less_pats, LessCancelSums.proc), 

6055  837 
("natle_cancel_sums", le_pats, LeCancelSums.proc)]; 
838 

839 
val nat_cancel_sums = nat_cancel_sums_add @ 

840 
[prep_simproc("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)]; 

5983  841 

842 
val nat_cancel_factor = map prep_simproc 

843 
[("nateq_cancel_factor", eq_pats, EqCancelFactor.proc), 

844 
("natless_cancel_factor", less_pats, LessCancelFactor.proc), 

845 
("natle_cancel_factor", le_pats, LeCancelFactor.proc)]; 

846 

847 
val nat_cancel = nat_cancel_factor @ nat_cancel_sums; 

848 

849 

850 
end; 

851 

852 
open ArithData; 

853 

854 
Addsimprocs nat_cancel; 

855 

856 
(**) 

857 
(* 2. Linear arithmetic *) 

858 
(**) 

859 

6101  860 
(* Parameters data for general linear arithmetic functor *) 
861 

862 
structure LA_Logic: LIN_ARITH_LOGIC = 

5983  863 
struct 
864 
val ccontr = ccontr; 

865 
val conjI = conjI; 

6101  866 
val neqE = linorder_neqE; 
5983  867 
val notI = notI; 
868 
val sym = sym; 

6109  869 
val not_lessD = linorder_not_less RS iffD1; 
6128  870 
val not_leD = linorder_not_le RS iffD1; 
5983  871 

6128  872 

6968  873 
fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI); 
6128  874 

6073  875 
val mk_Trueprop = HOLogic.mk_Trueprop; 
876 

6079  877 
fun neg_prop(TP$(Const("Not",_)$t)) = TP$t 
878 
 neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT>HOLogic.boolT)$t); 

6073  879 

6101  880 
fun is_False thm = 
881 
let val _ $ t = #prop(rep_thm thm) 

882 
in t = Const("False",HOLogic.boolT) end; 

883 

6128  884 
fun is_nat(t) = fastype_of1 t = HOLogic.natT; 
885 

886 
fun mk_nat_thm sg t = 

887 
let val ct = cterm_of sg t and cn = cterm_of sg (Var(("n",0),HOLogic.natT)) 

888 
in instantiate ([],[(cn,ct)]) le0 end; 

889 

6101  890 
end; 
891 

7582  892 
signature LIN_ARITH_DATA2 = 
893 
sig 

894 
include LIN_ARITH_DATA 

895 
val discrete: (string * bool)list ref 

896 
end; 

5983  897 

7582  898 
structure LA_Data_Ref: LIN_ARITH_DATA2 = 
899 
struct 

900 
val add_mono_thms = ref ([]:thm list); 

901 
val lessD = ref ([]:thm list); 

902 
val ss_ref = ref HOL_basic_ss; 

903 
val discrete = ref ([]:(string*bool)list); 

5983  904 

7548
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

905 
(* Decomposition of terms *) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

906 

9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

907 
fun nT (Type("fun",[N,_])) = N = HOLogic.natT 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

908 
 nT _ = false; 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

909 

9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

910 
fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

911 
 Some n => (overwrite(p,(t,n+m:int)), i)); 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

912 

9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

913 
(* Turn term into list of summand * multiplicity plus a constant *) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

914 
fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi)) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

915 
 poly(all as Const("op ",T) $ s $ t, m, pi) = 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

916 
if nT T then add_atom(all,m,pi) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

917 
else poly(s,m,poly(t,~1*m,pi)) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

918 
 poly(Const("uminus",_) $ t, m, pi) = poly(t,~1*m,pi) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

919 
 poly(Const("0",_), _, pi) = pi 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

920 
 poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,i+m)) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

921 
 poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi)= 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

922 
(poly(t,m*HOLogic.dest_binum c,pi) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

923 
handle TERM _ => add_atom(all,m,pi)) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

924 
 poly(all as Const("op *",_) $ t $ (Const("Numeral.number_of",_)$c), m, pi)= 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

925 
(poly(t,m*HOLogic.dest_binum c,pi) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

926 
handle TERM _ => add_atom(all,m,pi)) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

927 
 poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) = 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

928 
((p,i + m*HOLogic.dest_binum t) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

929 
handle TERM _ => add_atom(all,m,(p,i))) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

930 
 poly x = add_atom x; 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

931 

9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

932 
fun decomp2(rel,lhs,rhs) = 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

933 
let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0)) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

934 
in case rel of 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

935 
"op <" => Some(p,i,"<",q,j) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

936 
 "op <=" => Some(p,i,"<=",q,j) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

937 
 "op =" => Some(p,i,"=",q,j) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

938 
 _ => None 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

939 
end; 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

940 

9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

941 
fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

942 
 negate None = None; 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

943 

7582  944 
fun decomp1 (T,xxx) = 
7548
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

945 
(case T of 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

946 
Type("fun",[Type(D,[]),_]) => 
7582  947 
(case assoc(!discrete,D) of 
7548
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

948 
None => None 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

949 
 Some d => (case decomp2 xxx of 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

950 
None => None 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

951 
 Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d))) 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

952 
 _ => None); 
9e29a3af64ab
ROOT: Integ/bin_simprocs.ML now loaded in Integ/Bin.ML
nipkow
parents:
7428
diff
changeset

953 

7582  954 
fun decomp (_$(Const(rel,T)$lhs$rhs)) = decomp1 (T,(rel,lhs,rhs)) 
955 
 decomp (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) = 

956 
negate(decomp1 (T,(rel,lhs,rhs))) 

957 
 decomp _ = None 

6128  958 
end; 
6055  959 

7582  960 
let 
961 

962 
(* reduce contradictory <= to False. 

963 
Most of the work is done by the cancel tactics. 

964 
*) 

965 
val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq]; 

966 

967 
val add_mono_thms = map (fn s => prove_goal Arith.thy s 

968 
(fn prems => [cut_facts_tac prems 1, 

969 
blast_tac (claset() addIs [add_le_mono]) 1])) 

970 
["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)", 

971 
"(i = j) & (k <= l) ==> i + k <= j + (l::nat)", 

972 
"(i <= j) & (k = l) ==> i + k <= j + (l::nat)", 

973 
"(i = j) & (k = l) ==> i + k = j + (l::nat)" 

974 
]; 

975 

976 
in 

977 
LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms; 

978 
LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [Suc_leI]; 

979 
LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules 

980 
addsimprocs nat_cancel_sums_add; 

981 
LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("nat",true)] 

5983  982 
end; 
983 

6128  984 
structure Fast_Arith = 
985 
Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref); 

5983  986 

6128  987 
val fast_arith_tac = Fast_Arith.lin_arith_tac; 
6073  988 

7582  989 
let 
6128  990 
val nat_arith_simproc_pats = 
6394  991 
map (fn s => Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.boolT)) 
6128  992 
["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"]; 
5983  993 

7582  994 
val fast_nat_arith_simproc = mk_simproc 
995 
"fast_nat_arith" nat_arith_simproc_pats Fast_Arith.lin_arith_prover; 

996 
in 

997 
Addsimprocs [fast_nat_arith_simproc] 

998 
end; 

6073  999 

1000 
(* Because of fast_nat_arith_simproc, the arithmetic solver is really only 

1001 
useful to detect inconsistencies among the premises for subgoals which are 

1002 
*not* themselves (in)equalities, because the latter activate 

1003 
fast_nat_arith_simproc anyway. However, it seems cheaper to activate the 

1004 
solver all the time rather than add the additional check. *) 

1005 

7570  1006 
simpset_ref () := (simpset() addSolver 
1007 
(mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac)); 

6055  1008 

8252  1009 
(*Elimination of `' on nat due to John Harrison. *) 
7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset

1010 
Goal "P(a  b::nat) = (ALL d. (b = a + d > P 0) & (a = b + d > P d))"; 
6301  1011 
by (case_tac "a <= b" 1); 
7059  1012 
by Auto_tac; 
6301  1013 
by (eres_inst_tac [("x","ba")] allE 1); 
7059  1014 
by (asm_simp_tac (simpset() addsimps [diff_is_0_eq RS iffD2]) 1); 
6055  1015 
qed "nat_diff_split"; 
1016 

8252  1017 
(*LCP's version, replacing b=a+d by a<b, which sometimes works better*) 
1018 
Goal "P(a  b::nat) = (ALL d. (a<b > P 0) & (a = b + d > P d))"; 

1019 
by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); 

1020 
qed "nat_diff_split'"; 

1021 

7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset

1022 

6055  1023 
(* FIXME: K true should be replaced by a sensible test to speed things up 
6157  1024 
in case there are lots of irrelevant terms involved; 
1025 
elimination of min/max can be optimized: 

1026 
(max m n + k <= r) = (m+k <= r & n+k <= r) 

1027 
(l <= min m n + k) = (l <= m+k & l <= n+k) 

6055  1028 
*) 
7582  1029 
val arith_tac_split_thms = ref [nat_diff_split,split_min,split_max]; 
1030 
fun arith_tac i = 

1031 
refute_tac (K true) (REPEAT o split_tac (!arith_tac_split_thms)) 

1032 
((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i; 

6055  1033 

7131  1034 

1035 
(* proof method setup *) 

1036 

7428  1037 
val arith_method = 
1038 
Method.METHOD (fn facts => FIRSTGOAL (Method.insert_tac facts THEN' arith_tac)); 

7131  1039 

1040 
val arith_setup = 

1041 
[Method.add_methods 

1042 
[("arith", Method.no_args arith_method, "decide linear arithmethic")]]; 

1043 

5983  1044 
(**) 
1045 
(* End of proof procedures. Now go and USE them! *) 

1046 
(**) 

1047 

4736  1048 
(*** Subtraction laws  mostly from Clemens Ballarin ***) 
3234  1049 

5429  1050 
Goal "[ a < (b::nat); c <= a ] ==> ac < bc"; 
6301  1051 
by (arith_tac 1); 
3234  1052 
qed "diff_less_mono"; 
1053 

5429  1054 
Goal "a+b < (c::nat) ==> a < cb"; 
6301  1055 
by (arith_tac 1); 
3234  1056 
qed "add_less_imp_less_diff"; 
1057 

5427  1058 
Goal "(i < jk) = (i+k < (j::nat))"; 
6301  1059 
by (arith_tac 1); 
5427  1060 
qed "less_diff_conv"; 
1061 

5497  1062 
Goal "(jk <= (i::nat)) = (j <= i+k)"; 
6301  1063 
by (arith_tac 1); 
5485  1064 
qed "le_diff_conv"; 
1065 

5497  1066 
Goal "k <= j ==> (i <= jk) = (i+k <= (j::nat))"; 
6301  1067 
by (arith_tac 1); 
5497  1068 
qed "le_diff_conv2"; 
1069 

5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset

1070 
Goal "Suc i <= n ==> Suc (n  Suc i) = n  i"; 
6301  1071 
by (arith_tac 1); 
3234  1072 
qed "Suc_diff_Suc"; 
1073 

5429  1074 
Goal "i <= (n::nat) ==> n  (n  i) = i"; 
6301  1075 
by (arith_tac 1); 
3234  1076 
qed "diff_diff_cancel"; 
3381
2bac33ec2b0d
New theorems le_add_diff_inverse, le_add_diff_inverse2
paulson
parents:
3366
diff
changeset

1077 
Addsimps [diff_diff_cancel]; 
3234  1078 

5429  1079 
Goal "k <= (n::nat) ==> m <= n + m  k"; 
6301  1080 
by (arith_tac 1); 
3234  1081 
qed "le_add_diff"; 
1082 

6055  1083 
Goal "[ 0<k; j<i ] ==> j+ki < k"; 
6301  1084 
by (arith_tac 1); 
6055  1085 
qed "add_diff_less"; 
3234  1086 

5356  1087 
Goal "m1 < n ==> m <= n"; 
6301  1088 
by (arith_tac 1); 
5356  1089 
qed "pred_less_imp_le"; 
1090 

1091 
Goal "j<=i ==> i  j < Suc i  j"; 

6301  1092 
by (arith_tac 1); 
5356  1093 
qed "diff_less_Suc_diff"; 
1094 

1095 
Goal "i  j <= Suc i  j"; 

6301  1096 
by (arith_tac 1); 
5356  1097 
qed "diff_le_Suc_diff"; 
1098 
AddIffs [diff_le_Suc_diff]; 

1099 

1100 
Goal "n  Suc i <= n  i"; 

6301  1101 
by (arith_tac 1); 
5356  1102 
qed "diff_Suc_le_diff"; 
1103 
AddIffs [diff_Suc_le_diff]; 

1104 

5409  1105 
Goal "0 < n ==> (m <= n1) = (m<n)"; 
6301  1106 
by (arith_tac 1); 
5409  1107 
qed "le_pred_eq"; 
1108 

1109 
Goal "0 < n ==> (m1 < n) = (m<=n)"; 

6301  1110 
by (arith_tac 1); 
5409  1111 
qed "less_pred_eq"; 
1112 

7059  1113 
(*Replaces the previous diff_less and le_diff_less, which had the stronger 
1114 
second premise n<=m*) 

1115 
Goal "[ 0<n; 0<m ] ==> m  n < m"; 

6301  1116 
by (arith_tac 1); 
5414
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

1117 
qed "diff_less"; 
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

1118 

4732  1119 

7128  1120 
(*** Reducting subtraction to addition ***) 
1121 

1122 
Goal "n<=(l::nat) > Suc l  n + m = Suc (l  n + m)"; 

7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset

1123 
by (simp_tac (simpset() addsplits [nat_diff_split]) 1); 
7128  1124 
qed_spec_mp "Suc_diff_add_le"; 
1125 

1126 
Goal "i<n ==> n  Suc i < n  i"; 

7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset

1127 
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); 
7128  1128 
qed "diff_Suc_less_diff"; 
1129 

1130 
Goal "Suc(m)n = (if m<n then 0 else Suc(mn))"; 

7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset

1131 
by (simp_tac (simpset() addsplits [nat_diff_split]) 1); 
7128  1132 
qed "if_Suc_diff_le"; 
1133 

1134 
Goal "Suc(m)n <= Suc(mn)"; 

7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset

1135 
by (simp_tac (simpset() addsplits [nat_diff_split]) 1); 
7128  1136 
qed "diff_Suc_le_Suc_diff"; 
1137 

1138 
Goal "[ k<=n; n<=m ] ==> (mk)  (nk) = m(n::nat)"; 

7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset

1139 
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); 
7128  1140 
qed "diff_right_cancel"; 
1141 

1142 

7108  1143 
(** (Anti)Monotonicity of subtraction  by Stephan Merz **) 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

1144 

1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

1145 
(* Monotonicity of subtraction in first argument *) 
6055  1146 
Goal "m <= (n::nat) ==> (ml) <= (nl)"; 
7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset

1147 
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); 
6055  1148 
qed "diff_le_mono"; 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

1149 

5429  1150 
Goal "m <= (n::nat) ==> (ln) <= (lm)"; 
7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset

1151 
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); 
6055  1152 
qed "diff_le_mono2"; 
5983  1153 

6055  1154 
Goal "[ m < (n::nat); m<l ] ==> (ln) < (lm)"; 
7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset

1155 
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); 
6055  1156 
qed "diff_less_mono2"; 
5983  1157 

6055  1158 
Goal "[ mn = 0; nm = 0 ] ==> m=n"; 
7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset

1159 
by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1); 
6055  1160 
qed "diffs0_imp_equal"; 