author  paulson 
Wed, 23 Sep 1998 10:12:01 +0200  
changeset 5537  c2bd39a2c0ee 
parent 5497  497215d66441 
child 5598  6b8dee1a6ebb 
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 

4732  15 
qed_goal "diff_0_eq_0" thy 
923  16 
"0  n = 0" 
3339  17 
(fn _ => [induct_tac "n" 1, ALLGOALS Asm_simp_tac]); 
923  18 

5429  19 
(*Must simplify BEFORE the induction! (Else we get a critical pair) 
923  20 
Suc(m)  Suc(n) rewrites to pred(Suc(m)  n) *) 
4732  21 
qed_goal "diff_Suc_Suc" thy 
923  22 
"Suc(m)  Suc(n) = m  n" 
23 
(fn _ => 

3339  24 
[Simp_tac 1, induct_tac "n" 1, ALLGOALS Asm_simp_tac]); 
923  25 

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

26 
Addsimps [diff_0_eq_0, diff_Suc_Suc]; 
923  27 

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

30 
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

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

35 

36 
Delsimps [diff_Suc]; 

37 

923  38 

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

40 

41 
(*** Addition ***) 

42 

4732  43 
qed_goal "add_0_right" thy "m + 0 = m" 
3339  44 
(fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); 
923  45 

4732  46 
qed_goal "add_Suc_right" thy "m + Suc(n) = Suc(m+n)" 
3339  47 
(fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); 
923  48 

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

49 
Addsimps [add_0_right,add_Suc_right]; 
923  50 

51 
(*Associative law for addition*) 

4732  52 
qed_goal "add_assoc" thy "(m + n) + k = m + ((n + k)::nat)" 
3339  53 
(fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); 
923  54 

55 
(*Commutative law for addition*) 

4732  56 
qed_goal "add_commute" thy "m + n = n + (m::nat)" 
3339  57 
(fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); 
923  58 

4732  59 
qed_goal "add_left_commute" thy "x+(y+z)=y+((x+z)::nat)" 
923  60 
(fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1, 
61 
rtac (add_commute RS arg_cong) 1]); 

62 

63 
(*Addition is an ACoperator*) 

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

65 

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

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

69 
by (Asm_simp_tac 1); 
923  70 
qed "add_left_cancel"; 
71 

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

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

75 
by (Asm_simp_tac 1); 
923  76 
qed "add_right_cancel"; 
77 

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

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

81 
by (Asm_simp_tac 1); 
923  82 
qed "add_left_cancel_le"; 
83 

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

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

87 
by (Asm_simp_tac 1); 
923  88 
qed "add_left_cancel_less"; 
89 

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

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

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

92 

3339  93 
(** Reasoning about m+0=0, etc. **) 
94 

5069  95 
Goal "(m+n = 0) = (m=0 & n=0)"; 
3339  96 
by (induct_tac "m" 1); 
1327
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

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

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

100 

5069  101 
Goal "(0<m+n) = (0<m  0<n)"; 
4423  102 
by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1); 
4360  103 
qed "add_gr_0"; 
104 
AddIffs [add_gr_0]; 

105 

106 
(* FIXME: really needed?? *) 

5069  107 
Goal "((m+n)1 = 0) = (m=0 & n1 = 0  m1 = 0 & n=0)"; 
4360  108 
by (exhaust_tac "m" 1); 
4089  109 
by (ALLGOALS (fast_tac (claset() addss (simpset())))); 
3293  110 
qed "pred_add_is_0"; 
111 
Addsimps [pred_add_is_0]; 

112 

5429  113 
(* 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

114 
Goal "0<n ==> m + (n1) = (m+n)1"; 
4360  115 
by (exhaust_tac "m" 1); 
116 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc] 

5183  117 
addsplits [nat.split]))); 
1327
6c29cfab679c
added new arithmetic lemmas and the functions take and drop.
nipkow
parents:
1301
diff
changeset

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

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

120 

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

124 
delsimps [add_0_right]) 1); 

125 
qed "add_eq_self_zero"; 

126 

1626  127 

923  128 
(**** Additional theorems about "less than" ****) 
129 

5078  130 
(*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

131 
Goal "m<n > (? k. n=Suc(m+k))"; 
3339  132 
by (induct_tac "n" 1); 
5497  133 
by (ALLGOALS (simp_tac (simpset() addsimps [le_eq_less_or_eq]))); 
4089  134 
by (blast_tac (claset() addSEs [less_SucE] 
5497  135 
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

136 
qed_spec_mp "less_eq_Suc_add"; 
923  137 

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

140 
by (ALLGOALS Simp_tac); 
923  141 
by (etac le_trans 1); 
142 
by (rtac (lessI RS less_imp_le) 1); 

143 
qed "le_add2"; 

144 

5069  145 
Goal "n <= ((n + m)::nat)"; 
4089  146 
by (simp_tac (simpset() addsimps add_ac) 1); 
923  147 
by (rtac le_add2 1); 
148 
qed "le_add1"; 

149 

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

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

152 

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

155 
qed "less_iff_Suc_add"; 

156 

157 

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

160 

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

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

163 

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

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

166 

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

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

169 

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

170 
Goal "i+j < (k::nat) ==> i<k"; 
1552  171 
by (etac rev_mp 1); 
3339  172 
by (induct_tac "j" 1); 
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1198
diff
changeset

173 
by (ALLGOALS Asm_simp_tac); 
4089  174 
by (blast_tac (claset() addDs [Suc_lessD]) 1); 
1152  175 
qed "add_lessD1"; 
176 

5429  177 
Goal "~ (i+j < (i::nat))"; 
3457  178 
by (rtac notI 1); 
179 
by (etac (add_lessD1 RS less_irrefl) 1); 

3234  180 
qed "not_add_less1"; 
181 

5429  182 
Goal "~ (j+i < (i::nat))"; 
4089  183 
by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1); 
3234  184 
qed "not_add_less2"; 
185 
AddIffs [not_add_less1, not_add_less2]; 

186 

5069  187 
Goal "m+k<=n > m<=(n::nat)"; 
3339  188 
by (induct_tac "k" 1); 
5497  189 
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

190 
qed_spec_mp "add_leD1"; 
923  191 

5429  192 
Goal "m+k<=n ==> k<=(n::nat)"; 
4089  193 
by (full_simp_tac (simpset() addsimps [add_commute]) 1); 
2498  194 
by (etac add_leD1 1); 
195 
qed_spec_mp "add_leD2"; 

196 

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

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

5497  203 
by (auto_tac (claset(), 
204 
simpset() delsimps [add_Suc_right] 

5537  205 
addsimps [less_iff_Suc_add, 
206 
add_Suc_right RS sym] @ add_ac)); 

923  207 
qed "less_add_eq_less"; 
208 

209 

1713  210 
(*** Monotonicity of Addition ***) 
923  211 

212 
(*strict, in 1st argument*) 

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

215 
by (ALLGOALS Asm_simp_tac); 
923  216 
qed "add_less_mono1"; 
217 

218 
(*strict, in both arguments*) 

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

223 
by (ALLGOALS Asm_simp_tac); 
923  224 
qed "add_less_mono"; 
225 

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

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

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

4089  232 
by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); 
233 
by (blast_tac (claset() addSIs [lt_mono]) 1); 

923  234 
qed "less_mono_imp_le_mono"; 
235 

236 
(*nonstrict, in 1st argument*) 

5429  237 
Goal "i<=j ==> i + k <= j + (k::nat)"; 
3842  238 
by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1); 
1552  239 
by (etac add_less_mono1 1); 
923  240 
by (assume_tac 1); 
241 
qed "add_le_mono1"; 

242 

243 
(*nonstrict, in both arguments*) 

5429  244 
Goal "[i<=j; k<=l ] ==> i + k <= j + (l::nat)"; 
923  245 
by (etac (add_le_mono1 RS le_trans) 1); 
4089  246 
by (simp_tac (simpset() addsimps [add_commute]) 1); 
923  247 
qed "add_le_mono"; 
1713  248 

3234  249 

250 
(*** Multiplication ***) 

251 

252 
(*right annihilation in product*) 

4732  253 
qed_goal "mult_0_right" thy "m * 0 = 0" 
3339  254 
(fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); 
3234  255 

3293  256 
(*right successor law for multiplication*) 
4732  257 
qed_goal "mult_Suc_right" thy "m * Suc(n) = m + (m * n)" 
3339  258 
(fn _ => [induct_tac "m" 1, 
4089  259 
ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]); 
3234  260 

3293  261 
Addsimps [mult_0_right, mult_Suc_right]; 
3234  262 

5069  263 
Goal "1 * n = n"; 
3234  264 
by (Asm_simp_tac 1); 
265 
qed "mult_1"; 

266 

5069  267 
Goal "n * 1 = n"; 
3234  268 
by (Asm_simp_tac 1); 
269 
qed "mult_1_right"; 

270 

271 
(*Commutative law for multiplication*) 

4732  272 
qed_goal "mult_commute" thy "m * n = n * (m::nat)" 
3339  273 
(fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); 
3234  274 

275 
(*addition distributes over multiplication*) 

4732  276 
qed_goal "add_mult_distrib" thy "(m + n)*k = (m*k) + ((n*k)::nat)" 
3339  277 
(fn _ => [induct_tac "m" 1, 
4089  278 
ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]); 
3234  279 

4732  280 
qed_goal "add_mult_distrib2" thy "k*(m + n) = (k*m) + ((k*n)::nat)" 
3339  281 
(fn _ => [induct_tac "m" 1, 
4089  282 
ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]); 
3234  283 

284 
(*Associative law for multiplication*) 

4732  285 
qed_goal "mult_assoc" thy "(m * n) * k = m * ((n * k)::nat)" 
3339  286 
(fn _ => [induct_tac "m" 1, 
4089  287 
ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))]); 
3234  288 

4732  289 
qed_goal "mult_left_commute" thy "x*(y*z) = y*((x*z)::nat)" 
3234  290 
(fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1, 
291 
rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]); 

292 

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

294 

5069  295 
Goal "(m*n = 0) = (m=0  n=0)"; 
3339  296 
by (induct_tac "m" 1); 
297 
by (induct_tac "n" 2); 

3293  298 
by (ALLGOALS Asm_simp_tac); 
299 
qed "mult_is_0"; 

300 
Addsimps [mult_is_0]; 

301 

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

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

306 
qed "le_square"; 

307 

3234  308 

309 
(*** Difference ***) 

310 

311 

4732  312 
qed_goal "diff_self_eq_0" thy "m  m = 0" 
3339  313 
(fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]); 
3234  314 
Addsimps [diff_self_eq_0]; 
315 

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

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

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

321 

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

322 
Goal "n<=m ==> n+(mn) = (m::nat)"; 
4089  323 
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

324 
qed "le_add_diff_inverse"; 
3234  325 

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

326 
Goal "n<=m ==> (mn)+n = (m::nat)"; 
4089  327 
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

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

329 

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

330 
Addsimps [le_add_diff_inverse, le_add_diff_inverse2]; 
3234  331 

332 

333 
(*** More results about difference ***) 

334 

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

335 
Goal "n <= m ==> Suc(m)n = Suc(mn)"; 
5316  336 
by (etac rev_mp 1); 
3352  337 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
338 
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

339 
qed "Suc_diff_le"; 
3352  340 

5429  341 
Goal "n<=(l::nat) > Suc l  n + m = Suc (l  n + m)"; 
342 
by (res_inst_tac [("m","n"),("n","l")] diff_induct 1); 

343 
by (ALLGOALS Asm_simp_tac); 

344 
qed_spec_mp "Suc_diff_add_le"; 

345 

5069  346 
Goal "m  n < Suc(m)"; 
3234  347 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
348 
by (etac less_SucE 3); 

4089  349 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq]))); 
3234  350 
qed "diff_less_Suc"; 
351 

5429  352 
Goal "m  n <= (m::nat)"; 
3234  353 
by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1); 
354 
by (ALLGOALS Asm_simp_tac); 

355 
qed "diff_le_self"; 

3903
1b29151a1009
New simprule diff_le_self, requiring a new proof of diff_diff_cancel
paulson
parents:
3896
diff
changeset

356 
Addsimps [diff_le_self]; 
3234  357 

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

360 

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

364 
qed "diff_diff_left"; 

365 

5069  366 
Goal "(Suc m  n)  Suc k = m  n  k"; 
4423  367 
by (simp_tac (simpset() addsimps [diff_diff_left]) 1); 
4736  368 
qed "Suc_diff_diff"; 
369 
Addsimps [Suc_diff_diff]; 

4360  370 

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

371 
Goal "0<n ==> n  Suc i < n"; 
5183  372 
by (exhaust_tac "n" 1); 
4732  373 
by Safe_tac; 
5497  374 
by (asm_simp_tac (simpset() addsimps le_simps) 1); 
4732  375 
qed "diff_Suc_less"; 
376 
Addsimps [diff_Suc_less]; 

377 

5329  378 
Goal "i<n ==> n  Suc i < n  i"; 
379 
by (exhaust_tac "n" 1); 

5497  380 
by (auto_tac (claset(), 
5537  381 
simpset() addsimps [Suc_diff_le]@le_simps)); 
5329  382 
qed "diff_Suc_less_diff"; 
383 

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

384 
Goal "m  n <= Suc m  n"; 
4732  385 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
386 
by (ALLGOALS Asm_simp_tac); 

387 
qed "diff_le_Suc_diff"; 

388 

3396  389 
(*This and the next few suggested by Florian Kammueller*) 
5069  390 
Goal "!!i::nat. ijk = ikj"; 
4089  391 
by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1); 
3352  392 
qed "diff_commute"; 
393 

5429  394 
Goal "k<=j > j<=i > i  (j  k) = i  j + (k::nat)"; 
3352  395 
by (res_inst_tac [("m","i"),("n","j")] diff_induct 1); 
396 
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

397 
by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_Suc_eq]) 1); 
3352  398 
qed_spec_mp "diff_diff_right"; 
399 

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

403 
qed_spec_mp "diff_add_assoc"; 

404 

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

408 

5429  409 
Goal "(n+m)  n = (m::nat)"; 
3339  410 
by (induct_tac "n" 1); 
3234  411 
by (ALLGOALS Asm_simp_tac); 
412 
qed "diff_add_inverse"; 

413 
Addsimps [diff_add_inverse]; 

414 

5429  415 
Goal "(m+n)  n = (m::nat)"; 
4089  416 
by (simp_tac (simpset() addsimps [diff_add_assoc]) 1); 
3234  417 
qed "diff_add_inverse2"; 
418 
Addsimps [diff_add_inverse2]; 

419 

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

422 
by (ALLGOALS Asm_simp_tac); 
3366  423 
qed "le_imp_diff_is_add"; 
424 

5356  425 
Goal "(mn = 0) = (m <= n)"; 
3234  426 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
5497  427 
by (ALLGOALS Asm_simp_tac); 
5356  428 
qed "diff_is_0_eq"; 
429 
Addsimps [diff_is_0_eq RS iffD2]; 

3234  430 

5316  431 
Goal "mn = 0 > nm = 0 > m=n"; 
3234  432 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
433 
by (REPEAT(Simp_tac 1 THEN TRY(atac 1))); 

434 
qed_spec_mp "diffs0_imp_equal"; 

435 

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

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

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

440 
Addsimps [zero_less_diff]; 
3234  441 

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

442 
Goal "i < j ==> ? k. 0<k & i+k = j"; 
5078  443 
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

444 
by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1); 
5078  445 
qed "less_imp_add_positive"; 
446 

5069  447 
Goal "Suc(m)n = (if m<n then 0 else Suc(mn))"; 
5414
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

448 
by (simp_tac (simpset() addsimps [leI, Suc_le_eq, Suc_diff_le]) 1); 
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

449 
qed "if_Suc_diff_le"; 
3234  450 

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

452 
by (simp_tac (simpset() addsimps [if_Suc_diff_le]) 1); 
4672
9d55bc687e1e
New theorem diff_Suc_le_Suc_diff; tidied another proof
paulson
parents:
4423
diff
changeset

453 
qed "diff_Suc_le_Suc_diff"; 
9d55bc687e1e
New theorem diff_Suc_le_Suc_diff; tidied another proof
paulson
parents:
4423
diff
changeset

454 

5069  455 
Goal "P(k) > (!n. P(Suc(n))> P(n)) > P(ki)"; 
3234  456 
by (res_inst_tac [("m","k"),("n","i")] diff_induct 1); 
3718  457 
by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac)); 
3234  458 
qed "zero_induct_lemma"; 
459 

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

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

464 
qed "zero_induct"; 

465 

5429  466 
Goal "(k+m)  (k+n) = m  (n::nat)"; 
3339  467 
by (induct_tac "k" 1); 
3234  468 
by (ALLGOALS Asm_simp_tac); 
469 
qed "diff_cancel"; 

470 
Addsimps [diff_cancel]; 

471 

5429  472 
Goal "(m+k)  (n+k) = m  (n::nat)"; 
3234  473 
val add_commute_k = read_instantiate [("n","k")] add_commute; 
5537  474 
by (asm_simp_tac (simpset() addsimps [add_commute_k]) 1); 
3234  475 
qed "diff_cancel2"; 
476 
Addsimps [diff_cancel2]; 

477 

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

478 
(*From Clemens Ballarin, proof by lcp*) 
5429  479 
Goal "[ k<=n; n<=m ] ==> (mk)  (nk) = m(n::nat)"; 
5414
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

480 
by (REPEAT (etac rev_mp 1)); 
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

481 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

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

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

484 
by (asm_simp_tac (simpset() addsimps [Suc_diff_le, le_Suc_eq]) 1); 
3234  485 
qed "diff_right_cancel"; 
486 

5429  487 
Goal "n  (n+m) = 0"; 
3339  488 
by (induct_tac "n" 1); 
3234  489 
by (ALLGOALS Asm_simp_tac); 
490 
qed "diff_add_0"; 

491 
Addsimps [diff_add_0]; 

492 

5409  493 

3234  494 
(** Difference distributes over multiplication **) 
495 

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

499 
qed "diff_mult_distrib" ; 

500 

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

506 

507 

1713  508 
(*** Monotonicity of Multiplication ***) 
509 

5429  510 
Goal "i <= (j::nat) ==> i*k<=j*k"; 
3339  511 
by (induct_tac "k" 1); 
4089  512 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono]))); 
1713  513 
qed "mult_le_mono1"; 
514 

515 
(*<=monotonicity, BOTH arguments*) 

5429  516 
Goal "[ i <= (j::nat); k <= l ] ==> i*k <= j*l"; 
2007  517 
by (etac (mult_le_mono1 RS le_trans) 1); 
1713  518 
by (rtac le_trans 1); 
2007  519 
by (stac mult_commute 2); 
520 
by (etac mult_le_mono1 2); 

4089  521 
by (simp_tac (simpset() addsimps [mult_commute]) 1); 
1713  522 
qed "mult_le_mono"; 
523 

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

5429  525 
Goal "[ i<j; 0<k ] ==> k*i < k*j"; 
5078  526 
by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1); 
1713  527 
by (Asm_simp_tac 1); 
3339  528 
by (induct_tac "x" 1); 
4089  529 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono]))); 
1713  530 
qed "mult_less_mono2"; 
531 

5429  532 
Goal "[ i<j; 0<k ] ==> i*k < j*k"; 
3457  533 
by (dtac mult_less_mono2 1); 
4089  534 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute]))); 
3234  535 
qed "mult_less_mono1"; 
536 

5069  537 
Goal "(0 < m*n) = (0<m & 0<n)"; 
3339  538 
by (induct_tac "m" 1); 
539 
by (induct_tac "n" 2); 

1713  540 
by (ALLGOALS Asm_simp_tac); 
541 
qed "zero_less_mult_iff"; 

4356  542 
Addsimps [zero_less_mult_iff]; 
1713  543 

5069  544 
Goal "(m*n = 1) = (m=1 & n=1)"; 
3339  545 
by (induct_tac "m" 1); 
1795  546 
by (Simp_tac 1); 
3339  547 
by (induct_tac "n" 1); 
1795  548 
by (Simp_tac 1); 
4089  549 
by (fast_tac (claset() addss simpset()) 1); 
1795  550 
qed "mult_eq_1_iff"; 
4356  551 
Addsimps [mult_eq_1_iff]; 
1795  552 

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

553 
Goal "0<k ==> (m*k < n*k) = (m<n)"; 
4089  554 
by (safe_tac (claset() addSIs [mult_less_mono1])); 
3234  555 
by (cut_facts_tac [less_linear] 1); 
4389  556 
by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1); 
3234  557 
qed "mult_less_cancel2"; 
558 

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

559 
Goal "0<k ==> (k*m < k*n) = (m<n)"; 
3457  560 
by (dtac mult_less_cancel2 1); 
4089  561 
by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1); 
3234  562 
qed "mult_less_cancel1"; 
563 
Addsimps [mult_less_cancel1, mult_less_cancel2]; 

564 

5069  565 
Goal "(Suc k * m < Suc k * n) = (m < n)"; 
4423  566 
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

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

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

569 

5069  570 
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

571 
by (simp_tac (simpset_of HOL.thy) 1); 
4423  572 
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

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

574 

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

575 
Goal "0<k ==> (m*k = n*k) = (m=n)"; 
3234  576 
by (cut_facts_tac [less_linear] 1); 
3724  577 
by Safe_tac; 
3457  578 
by (assume_tac 2); 
3234  579 
by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac)); 
580 
by (ALLGOALS Asm_full_simp_tac); 

581 
qed "mult_cancel2"; 

582 

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

583 
Goal "0<k ==> (k*m = k*n) = (m=n)"; 
3457  584 
by (dtac mult_cancel2 1); 
4089  585 
by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1); 
3234  586 
qed "mult_cancel1"; 
587 
Addsimps [mult_cancel1, mult_cancel2]; 

588 

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

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

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

593 

3234  594 

1795  595 
(** Lemma for gcd **) 
596 

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

597 
Goal "m = m*n ==> n=1  m=0"; 
1795  598 
by (dtac sym 1); 
599 
by (rtac disjCI 1); 

600 
by (rtac nat_less_cases 1 THEN assume_tac 2); 

4089  601 
by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1); 
4356  602 
by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1); 
1795  603 
qed "mult_eq_self_implies_10"; 
604 

605 

4736  606 
(*** Subtraction laws  mostly from Clemens Ballarin ***) 
3234  607 

5429  608 
Goal "[ a < (b::nat); c <= a ] ==> ac < bc"; 
3234  609 
by (subgoal_tac "c+(ac) < c+(bc)" 1); 
3381
2bac33ec2b0d
New theorems le_add_diff_inverse, le_add_diff_inverse2
paulson
parents:
3366
diff
changeset

610 
by (Full_simp_tac 1); 
3234  611 
by (subgoal_tac "c <= b" 1); 
4089  612 
by (blast_tac (claset() addIs [less_imp_le, le_trans]) 2); 
3381
2bac33ec2b0d
New theorems le_add_diff_inverse, le_add_diff_inverse2
paulson
parents:
3366
diff
changeset

613 
by (Asm_simp_tac 1); 
3234  614 
qed "diff_less_mono"; 
615 

5429  616 
Goal "a+b < (c::nat) ==> a < cb"; 
3457  617 
by (dtac diff_less_mono 1); 
618 
by (rtac le_add2 1); 

3234  619 
by (Asm_full_simp_tac 1); 
620 
qed "add_less_imp_less_diff"; 

621 

5427  622 
Goal "(i < jk) = (i+k < (j::nat))"; 
5497  623 
by (rtac iffI 1); 
624 
by (case_tac "k <= j" 1); 

625 
by (dtac le_add_diff_inverse2 1); 

626 
by (dres_inst_tac [("k","k")] add_less_mono1 1); 

627 
by (Asm_full_simp_tac 1); 

628 
by (rotate_tac 1 1); 

629 
by (asm_full_simp_tac (simpset() addSolver cut_trans_tac) 1); 

630 
by (etac add_less_imp_less_diff 1); 

5427  631 
qed "less_diff_conv"; 
632 

5497  633 
Goal "(jk <= (i::nat)) = (j <= i+k)"; 
634 
by (simp_tac (simpset() addsimps [less_diff_conv, le_def]) 1); 

5485  635 
qed "le_diff_conv"; 
636 

5497  637 
Goal "k <= j ==> (i <= jk) = (i+k <= (j::nat))"; 
638 
by (asm_full_simp_tac 

639 
(simpset() delsimps [less_Suc_eq_le] 

640 
addsimps [less_Suc_eq_le RS sym, less_diff_conv, 

641 
Suc_diff_le RS sym]) 1); 

642 
qed "le_diff_conv2"; 

643 

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

644 
Goal "Suc i <= n ==> Suc (n  Suc i) = n  i"; 
5497  645 
by (asm_full_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1); 
3234  646 
qed "Suc_diff_Suc"; 
647 

5429  648 
Goal "i <= (n::nat) ==> n  (n  i) = i"; 
3903
1b29151a1009
New simprule diff_le_self, requiring a new proof of diff_diff_cancel
paulson
parents:
3896
diff
changeset

649 
by (etac rev_mp 1); 
1b29151a1009
New simprule diff_le_self, requiring a new proof of diff_diff_cancel
paulson
parents:
3896
diff
changeset

650 
by (res_inst_tac [("m","n"),("n","i")] diff_induct 1); 
4089  651 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Suc_diff_le]))); 
3234  652 
qed "diff_diff_cancel"; 
3381
2bac33ec2b0d
New theorems le_add_diff_inverse, le_add_diff_inverse2
paulson
parents:
3366
diff
changeset

653 
Addsimps [diff_diff_cancel]; 
3234  654 

5429  655 
Goal "k <= (n::nat) ==> m <= n + m  k"; 
3457  656 
by (etac rev_mp 1); 
3234  657 
by (res_inst_tac [("m", "k"), ("n", "n")] diff_induct 1); 
658 
by (Simp_tac 1); 

5497  659 
by (simp_tac (simpset() addsimps [le_add2, less_imp_le]) 1); 
3234  660 
by (Simp_tac 1); 
661 
qed "le_add_diff"; 

662 

5429  663 
Goal "0<k ==> j<i > j+ki < k"; 
4736  664 
by (res_inst_tac [("m","j"),("n","i")] diff_induct 1); 
665 
by (ALLGOALS Asm_simp_tac); 

666 
qed_spec_mp "add_diff_less"; 

667 

3234  668 

5356  669 
Goal "m1 < n ==> m <= n"; 
670 
by (exhaust_tac "m" 1); 

671 
by (auto_tac (claset(), simpset() addsimps [Suc_le_eq])); 

672 
qed "pred_less_imp_le"; 

673 

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

675 
by (REPEAT (etac rev_mp 1)); 

676 
by (res_inst_tac [("m","i"),("n","j")] diff_induct 1); 

677 
by Auto_tac; 

678 
qed "diff_less_Suc_diff"; 

679 

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

681 
by (res_inst_tac [("m","i"),("n","j")] diff_induct 1); 

682 
by Auto_tac; 

683 
qed "diff_le_Suc_diff"; 

684 
AddIffs [diff_le_Suc_diff]; 

685 

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

687 
by (case_tac "i<n" 1); 

5497  688 
by (dtac diff_Suc_less_diff 1); 
689 
by (auto_tac (claset(), simpset() addsimps [leI])); 

5356  690 
qed "diff_Suc_le_diff"; 
691 
AddIffs [diff_Suc_le_diff]; 

692 

5409  693 
Goal "0 < n ==> (m <= n1) = (m<n)"; 
694 
by (exhaust_tac "n" 1); 

5497  695 
by (auto_tac (claset(), simpset() addsimps le_simps)); 
5409  696 
qed "le_pred_eq"; 
697 

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

699 
by (exhaust_tac "m" 1); 

700 
by (auto_tac (claset(), simpset() addsimps [Suc_le_eq])); 

701 
qed "less_pred_eq"; 

702 

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

703 
(*In ordinary notation: if 0<n and n<=m then mn < m *) 
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

704 
Goal "[ 0<n; ~ m<n ] ==> m  n < m"; 
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

705 
by (subgoal_tac "0<n > ~ m<n > m  n < m" 1); 
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

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

707 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

708 
by (ALLGOALS(asm_simp_tac(simpset() addsimps [diff_less_Suc]))); 
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

709 
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

710 

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

711 
Goal "[ 0<n; n<=m ] ==> m  n < m"; 
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

712 
by (asm_simp_tac (simpset() addsimps [diff_less, not_less_iff_le]) 1); 
8a458866637c
changed Suc_diff_n to Suc_diff_le, with premise n <= m instead of n < Suc(m)
paulson
parents:
5409
diff
changeset

713 
qed "le_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

714 

5356  715 

4732  716 

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

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

718 

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

719 
(* Monotonicity of subtraction in first argument *) 
5429  720 
Goal "m <= (n::nat) > (ml) <= (nl)"; 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

721 
by (induct_tac "n" 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

722 
by (Simp_tac 1); 
4089  723 
by (simp_tac (simpset() addsimps [le_Suc_eq]) 1); 
4732  724 
by (blast_tac (claset() addIs [diff_le_Suc_diff, le_trans]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

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

726 

5429  727 
Goal "m <= (n::nat) ==> (ln) <= (lm)"; 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

728 
by (induct_tac "l" 1); 
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

729 
by (Simp_tac 1); 
5183  730 
by (case_tac "n <= na" 1); 
731 
by (subgoal_tac "m <= na" 1); 

4089  732 
by (asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1); 
733 
by (fast_tac (claset() addEs [le_trans]) 1); 

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

734 
by (dtac not_leE 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

735 
by (asm_simp_tac (simpset() addsimps [if_Suc_diff_le]) 1); 
3484
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset

736 
qed_spec_mp "diff_le_mono2"; 