author  berghofe 
Tue, 30 May 2000 18:02:49 +0200  
changeset 9001  93af64f54bf2 
parent 8935  548901d05a0e 
child 9041  3730ae0f513a 
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 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

15 
Goal "0  n = (0::nat)"; 
7007  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 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

45 
Goal "m + 0 = (m::nat)"; 
7007  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 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

108 
Goal "!!m::nat. (m+n = 0) = (m=0 & n=0)"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

109 
by (case_tac "m" 1); 
5598  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 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

114 
Goal "!!m::nat. (0 = m+n) = (m=0 & n=0)"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

115 
by (case_tac "m" 1); 
5598  116 
by (Auto_tac); 
117 
qed "zero_is_add"; 

118 
AddIffs [zero_is_add]; 

119 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

120 
Goal "!!m::nat. (m+n=1) = (m=1 & n=0  m=0 & n=1)"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

121 
by (case_tac "m" 1); 
6301  122 
by (Auto_tac); 
5598  123 
qed "add_is_1"; 
124 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

125 
Goal "!!m::nat. (1=m+n) = (m=1 & n=0  m=0 & n=1)"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

126 
by (case_tac "m" 1); 
6301  127 
by (Auto_tac); 
5598  128 
qed "one_is_add"; 
129 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

130 
Goal "!!m::nat. (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)" *) 
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

136 
Goal "!!m::nat. 0<n ==> m + (n1) = (m+n)1"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

137 
by (case_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 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

143 
Goal "!!m::nat. 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*) 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

273 
Goal "!!m::nat. m * 0 = 0"; 
7007  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 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

327 
Goal "!!m::nat. (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 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

333 
Goal "!!m::nat. (0 = m*n) = (0=m  0=n)"; 
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

334 
by (stac eq_commute 1 THEN stac mult_is_0 1); 
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

335 
by Auto_tac; 
7622  336 
qed "zero_is_mult"; 
337 

338 
Addsimps [mult_is_0, zero_is_mult]; 

3293  339 

3234  340 

341 
(*** Difference ***) 

342 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

343 
Goal "!!m::nat. m  m = 0"; 
7007  344 
by (induct_tac "m" 1); 
345 
by (ALLGOALS Asm_simp_tac); 

346 
qed "diff_self_eq_0"; 

3234  347 

348 
Addsimps [diff_self_eq_0]; 

349 

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

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

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

355 

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

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

358 
qed "le_add_diff_inverse"; 
3234  359 

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

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

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

363 

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

364 
Addsimps [le_add_diff_inverse, le_add_diff_inverse2]; 
3234  365 

366 

367 
(*** More results about difference ***) 

368 

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

369 
Goal "n <= m ==> Suc(m)n = Suc(mn)"; 
5316  370 
by (etac rev_mp 1); 
3352  371 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
372 
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

373 
qed "Suc_diff_le"; 
3352  374 

5069  375 
Goal "m  n < Suc(m)"; 
3234  376 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
377 
by (etac less_SucE 3); 

4089  378 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq]))); 
3234  379 
qed "diff_less_Suc"; 
380 

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

385 
Addsimps [diff_le_self]; 
3234  386 

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

389 

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

393 
qed "diff_diff_left"; 

394 

5069  395 
Goal "(Suc m  n)  Suc k = m  n  k"; 
4423  396 
by (simp_tac (simpset() addsimps [diff_diff_left]) 1); 
4736  397 
qed "Suc_diff_diff"; 
398 
Addsimps [Suc_diff_diff]; 

4360  399 

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

400 
Goal "0<n ==> n  Suc i < n"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

401 
by (case_tac "n" 1); 
4732  402 
by Safe_tac; 
5497  403 
by (asm_simp_tac (simpset() addsimps le_simps) 1); 
4732  404 
qed "diff_Suc_less"; 
405 
Addsimps [diff_Suc_less]; 

406 

3396  407 
(*This and the next few suggested by Florian Kammueller*) 
5069  408 
Goal "!!i::nat. ijk = ikj"; 
4089  409 
by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1); 
3352  410 
qed "diff_commute"; 
411 

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

415 
qed_spec_mp "diff_add_assoc"; 

416 

8708
2f2d2b4215d6
added some new ifflemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset

417 
Goal "k <= (j::nat) > (j + i)  k = (j  k) + i"; 
4732  418 
by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1); 
419 
qed_spec_mp "diff_add_assoc2"; 

420 

5429  421 
Goal "(n+m)  n = (m::nat)"; 
3339  422 
by (induct_tac "n" 1); 
3234  423 
by (ALLGOALS Asm_simp_tac); 
424 
qed "diff_add_inverse"; 

425 

5429  426 
Goal "(m+n)  n = (m::nat)"; 
4089  427 
by (simp_tac (simpset() addsimps [diff_add_assoc]) 1); 
3234  428 
qed "diff_add_inverse2"; 
429 

5429  430 
Goal "i <= (j::nat) ==> (ji=k) = (j=k+i)"; 
3724  431 
by Safe_tac; 
8859  432 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_add_inverse2]))); 
3366  433 
qed "le_imp_diff_is_add"; 
434 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

435 
Goal "!!m::nat. (mn = 0) = (m <= n)"; 
3234  436 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
5497  437 
by (ALLGOALS Asm_simp_tac); 
5356  438 
qed "diff_is_0_eq"; 
7059  439 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

440 
Goal "!!m::nat. (0 = mn) = (m <= n)"; 
7059  441 
by (stac (diff_is_0_eq RS sym) 1); 
442 
by (rtac eq_sym_conv 1); 

443 
qed "zero_is_diff_eq"; 

444 
Addsimps [diff_is_0_eq, zero_is_diff_eq]; 

3234  445 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

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

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

450 
Addsimps [zero_less_diff]; 
3234  451 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

452 
Goal "i < j ==> ? k::nat. 0<k & i+k = j"; 
5078  453 
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

454 
by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1); 
5078  455 
qed "less_imp_add_positive"; 
456 

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

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

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

466 
qed "zero_induct"; 

467 

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

472 

5429  473 
Goal "(m+k)  (n+k) = m  (n::nat)"; 
8859  474 
by (asm_simp_tac 
475 
(simpset() addsimps [diff_cancel, inst "n" "k" add_commute]) 1); 

3234  476 
qed "diff_cancel2"; 
477 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

478 
Goal "n  (n+m) = (0::nat)"; 
3339  479 
by (induct_tac "n" 1); 
3234  480 
by (ALLGOALS Asm_simp_tac); 
481 
qed "diff_add_0"; 

482 

5409  483 

3234  484 
(** Difference distributes over multiplication **) 
485 

5069  486 
Goal "!!m::nat. (m  n) * k = (m * k)  (n * k)"; 
3234  487 
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); 
8859  488 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel]))); 
3234  489 
qed "diff_mult_distrib" ; 
490 

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

496 

497 

1713  498 
(*** Monotonicity of Multiplication ***) 
499 

5429  500 
Goal "i <= (j::nat) ==> i*k<=j*k"; 
3339  501 
by (induct_tac "k" 1); 
4089  502 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono]))); 
1713  503 
qed "mult_le_mono1"; 
504 

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

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

508 
qed "mult_le_mono2"; 

509 

510 
(* <= monotonicity, BOTH arguments*) 

5429  511 
Goal "[ i <= (j::nat); k <= l ] ==> i*k <= j*l"; 
2007  512 
by (etac (mult_le_mono1 RS le_trans) 1); 
6987  513 
by (etac mult_le_mono2 1); 
1713  514 
qed "mult_le_mono"; 
515 

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

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

517 
Goal "!!i::nat. [ i<j; 0<k ] ==> k*i < k*j"; 
5078  518 
by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1); 
1713  519 
by (Asm_simp_tac 1); 
3339  520 
by (induct_tac "x" 1); 
4089  521 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono]))); 
1713  522 
qed "mult_less_mono2"; 
523 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

524 
Goal "!!i::nat. [ i<j; 0<k ] ==> i*k < j*k"; 
3457  525 
by (dtac mult_less_mono2 1); 
4089  526 
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute]))); 
3234  527 
qed "mult_less_mono1"; 
528 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

529 
Goal "!!m::nat. (0 < m*n) = (0<m & 0<n)"; 
3339  530 
by (induct_tac "m" 1); 
8859  531 
by (case_tac "n" 2); 
1713  532 
by (ALLGOALS Asm_simp_tac); 
533 
qed "zero_less_mult_iff"; 

4356  534 
Addsimps [zero_less_mult_iff]; 
1713  535 

8859  536 
Goal "(1 <= m*n) = (1<=m & 1<=n)"; 
537 
by (induct_tac "m" 1); 

538 
by (case_tac "n" 2); 

539 
by (ALLGOALS Asm_simp_tac); 

540 
qed "one_le_mult_iff"; 

541 
Addsimps [one_le_mult_iff]; 

542 

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

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

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

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

558 
Goal "!!m::nat. 0<k ==> (k*m < k*n) = (m<n)"; 
3457  559 
by (dtac mult_less_cancel2 1); 
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

560 
by (etac subst 1); 
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

561 
by (simp_tac (simpset() addsimps [mult_commute]) 1); 
3234  562 
qed "mult_less_cancel1"; 
563 
Addsimps [mult_less_cancel1, mult_less_cancel2]; 

564 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

565 
Goal "!!m::nat. 0<k ==> (m*k <= n*k) = (m<=n)"; 
6864  566 
by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
567 
qed "mult_le_cancel2"; 

568 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

569 
Goal "!!m::nat. 0<k ==> (k*m <= k*n) = (m<=n)"; 
6864  570 
by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
571 
qed "mult_le_cancel1"; 

572 
Addsimps [mult_le_cancel1, mult_le_cancel2]; 

573 

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

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

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

578 

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

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

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

583 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

584 
Goal "0 < (k::nat) ==> (m*k = n*k) = (m=n)"; 
3234  585 
by (cut_facts_tac [less_linear] 1); 
3724  586 
by Safe_tac; 
3457  587 
by (assume_tac 2); 
3234  588 
by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac)); 
589 
by (ALLGOALS Asm_full_simp_tac); 

590 
qed "mult_cancel2"; 

591 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

592 
Goal "0 < (k::nat) ==> (k*m = k*n) = (m=n)"; 
3457  593 
by (dtac mult_cancel2 1); 
4089  594 
by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1); 
3234  595 
qed "mult_cancel1"; 
596 
Addsimps [mult_cancel1, mult_cancel2]; 

597 

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

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

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

602 

3234  603 

8352  604 
(*Lemma for gcd*) 
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

605 
Goal "!!m::nat. m = m*n ==> n=1  m=0"; 
1795  606 
by (dtac sym 1); 
607 
by (rtac disjCI 1); 

608 
by (rtac nat_less_cases 1 THEN assume_tac 2); 

4089  609 
by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1); 
4356  610 
by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1); 
1795  611 
qed "mult_eq_self_implies_10"; 
612 

613 

5983  614 

615 

616 
(**) 

617 
(* Various arithmetic proof procedures *) 

618 
(**) 

619 

620 
(**) 

621 
(* 1. Cancellation of common terms *) 

622 
(**) 

623 

624 
(* Title: HOL/arith_data.ML 

625 
ID: $Id$ 

626 
Author: Markus Wenzel and Stefan Berghofer, TU Muenchen 

627 

628 
Setup various arithmetic proof procedures. 

629 
*) 

630 

631 
signature ARITH_DATA = 

632 
sig 

6055  633 
val nat_cancel_sums_add: simproc list 
5983  634 
val nat_cancel_sums: simproc list 
635 
val nat_cancel_factor: simproc list 

636 
val nat_cancel: simproc list 

637 
end; 

638 

639 
structure ArithData: ARITH_DATA = 

640 
struct 

641 

642 

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

644 

645 
(* mk_sum, mk_norm_sum *) 

646 

647 
val one = HOLogic.mk_nat 1; 

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

649 

650 
fun mk_sum [] = HOLogic.zero 

651 
 mk_sum [t] = t 

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

653 

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

655 
fun mk_norm_sum ts = 

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

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

658 
end; 

659 

660 

661 
(* dest_sum *) 

662 

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

664 

665 
fun dest_sum tm = 

666 
if HOLogic.is_zero tm then [] 

667 
else 

668 
(case try HOLogic.dest_Suc tm of 

669 
Some t => one :: dest_sum t 

670 
 None => 

671 
(case try dest_plus tm of 

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

673 
 None => [tm])); 

674 

675 

676 
(** generic proof tools **) 

677 

678 
(* prove conversions *) 

679 

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

681 

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

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

684 
(K [expand_tac, norm_tac])) 

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

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

687 

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

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

690 

691 

692 
(* rewriting *) 

693 

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

695 

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

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

698 

699 

700 

701 
(** cancel common summands **) 

702 

703 
structure Sum = 

704 
struct 

705 
val mk_sum = mk_norm_sum; 

706 
val dest_sum = dest_sum; 

707 
val prove_conv = prove_conv; 

708 
val norm_tac = simp_all add_rules THEN simp_all add_ac; 

709 
end; 

710 

711 
fun gen_uncancel_tac rule ct = 

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

713 

714 

715 
(* nat eq *) 

716 

717 
structure EqCancelSums = CancelSumsFun 

718 
(struct 

719 
open Sum; 

720 
val mk_bal = HOLogic.mk_eq; 

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

722 
val uncancel_tac = gen_uncancel_tac add_left_cancel; 

723 
end); 

724 

725 

726 
(* nat less *) 

727 

728 
structure LessCancelSums = CancelSumsFun 

729 
(struct 

730 
open Sum; 

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

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

733 
val uncancel_tac = gen_uncancel_tac add_left_cancel_less; 

734 
end); 

735 

736 

737 
(* nat le *) 

738 

739 
structure LeCancelSums = CancelSumsFun 

740 
(struct 

741 
open Sum; 

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

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

744 
val uncancel_tac = gen_uncancel_tac add_left_cancel_le; 

745 
end); 

746 

747 

748 
(* nat diff *) 

749 

750 
structure DiffCancelSums = CancelSumsFun 

751 
(struct 

752 
open Sum; 

753 
val mk_bal = HOLogic.mk_binop "op "; 

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

755 
val uncancel_tac = gen_uncancel_tac diff_cancel; 

756 
end); 

757 

758 

759 

760 
(** cancel common factor **) 

761 

762 
structure Factor = 

763 
struct 

764 
val mk_sum = mk_norm_sum; 

765 
val dest_sum = dest_sum; 

766 
val prove_conv = prove_conv; 

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

768 
end; 

769 

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

772 
fun gen_multiply_tac rule k = 

773 
if k > 0 then 

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

775 
else no_tac; 

776 

777 

778 
(* nat eq *) 

779 

780 
structure EqCancelFactor = CancelFactorFun 

781 
(struct 

782 
open Factor; 

783 
val mk_bal = HOLogic.mk_eq; 

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

785 
val multiply_tac = gen_multiply_tac Suc_mult_cancel1; 

786 
end); 

787 

788 

789 
(* nat less *) 

790 

791 
structure LessCancelFactor = CancelFactorFun 

792 
(struct 

793 
open Factor; 

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

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

796 
val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1; 

797 
end); 

798 

799 

800 
(* nat le *) 

801 

802 
structure LeCancelFactor = CancelFactorFun 

803 
(struct 

804 
open Factor; 

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

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

807 
val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1; 

808 
end); 

809 

810 

811 

812 
(** prepare nat_cancel simprocs **) 

813 

8100  814 
fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termT); 
5983  815 
val prep_pats = map prep_pat; 
816 

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

818 

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

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

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

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

823 

6055  824 
val nat_cancel_sums_add = map prep_simproc 
5983  825 
[("nateq_cancel_sums", eq_pats, EqCancelSums.proc), 
826 
("natless_cancel_sums", less_pats, LessCancelSums.proc), 

6055  827 
("natle_cancel_sums", le_pats, LeCancelSums.proc)]; 
828 

829 
val nat_cancel_sums = nat_cancel_sums_add @ 

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

5983  831 

832 
val nat_cancel_factor = map prep_simproc 

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

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

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

836 

837 
val nat_cancel = nat_cancel_factor @ nat_cancel_sums; 

838 

839 

840 
end; 

841 

842 
open ArithData; 

843 

844 
Addsimprocs nat_cancel; 

845 

846 
(**) 

847 
(* 2. Linear arithmetic *) 

848 
(**) 

849 

6101  850 
(* Parameters data for general linear arithmetic functor *) 
851 

852 
structure LA_Logic: LIN_ARITH_LOGIC = 

5983  853 
struct 
854 
val ccontr = ccontr; 

855 
val conjI = conjI; 

6101  856 
val neqE = linorder_neqE; 
5983  857 
val notI = notI; 
858 
val sym = sym; 

6109  859 
val not_lessD = linorder_not_less RS iffD1; 
6128  860 
val not_leD = linorder_not_le RS iffD1; 
5983  861 

6128  862 

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

6073  865 
val mk_Trueprop = HOLogic.mk_Trueprop; 
866 

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

6073  869 

6101  870 
fun is_False thm = 
871 
let val _ $ t = #prop(rep_thm thm) 

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

873 

6128  874 
fun is_nat(t) = fastype_of1 t = HOLogic.natT; 
875 

876 
fun mk_nat_thm sg t = 

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

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

879 

6101  880 
end; 
881 

7582  882 
signature LIN_ARITH_DATA2 = 
883 
sig 

884 
include LIN_ARITH_DATA 

885 
val discrete: (string * bool)list ref 

886 
end; 

5983  887 

7582  888 
structure LA_Data_Ref: LIN_ARITH_DATA2 = 
889 
struct 

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

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

892 
val ss_ref = ref HOL_basic_ss; 

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

5983  894 

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

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

896 

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

897 
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

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

899 

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

900 
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

901 
 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

902 

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

903 
(* 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

904 
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

905 
 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

906 
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

907 
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

908 
 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

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

910 
 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

911 
 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

912 
(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

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

914 
 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

915 
(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

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

917 
 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

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

919 
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

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

921 

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

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

923 
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

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

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

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

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

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

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

930 

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

931 
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

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

933 

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

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

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

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

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

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

941 
 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

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

943 

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

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

947 
 decomp _ = None 

6128  948 
end; 
6055  949 

7582  950 
let 
951 

952 
(* reduce contradictory <= to False. 

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

954 
*) 

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

956 

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

958 
(fn prems => [cut_facts_tac prems 1, 

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

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

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

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

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

964 
]; 

965 

966 
in 

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

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

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

970 
addsimprocs nat_cancel_sums_add; 

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

5983  972 
end; 
973 

6128  974 
structure Fast_Arith = 
975 
Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref); 

5983  976 

6128  977 
val fast_arith_tac = Fast_Arith.lin_arith_tac; 
6073  978 

7582  979 
let 
6128  980 
val nat_arith_simproc_pats = 
6394  981 
map (fn s => Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.boolT)) 
6128  982 
["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"]; 
5983  983 

7582  984 
val fast_nat_arith_simproc = mk_simproc 
985 
"fast_nat_arith" nat_arith_simproc_pats Fast_Arith.lin_arith_prover; 

986 
in 

987 
Addsimprocs [fast_nat_arith_simproc] 

988 
end; 

6073  989 

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

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

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

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

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

995 

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

6055  998 

8859  999 
(*Elimination of `' on nat*) 
1000 
Goal "P(a  b::nat) = (ALL d. (a<b > P 0) & (a = b + d > P d))"; 

1001 
by (case_tac "a < b" 1); 

1002 
by (auto_tac (claset(), simpset() addsimps [diff_is_0_eq RS iffD2])); 

6055  1003 
qed "nat_diff_split"; 
1004 

8859  1005 
val nat_diff_split = nat_diff_split; 
7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset

1006 

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

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

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

6055  1012 
*) 
7582  1013 
val arith_tac_split_thms = ref [nat_diff_split,split_min,split_max]; 
1014 
fun arith_tac i = 

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

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

6055  1017 

7131  1018 

1019 
(* proof method setup *) 

1020 

8502  1021 
fun arith_method prems = 
8571  1022 
Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac)); 
7131  1023 

1024 
val arith_setup = 

1025 
[Method.add_methods 

8502  1026 
[("arith", (arith_method o #2) oo Method.syntax Args.bang_facts , "decide linear arithmethic")]]; 
7131  1027 

5983  1028 
(**) 
1029 
(* End of proof procedures. Now go and USE them! *) 

1030 
(**) 

1031 

8833  1032 
Goal "m <= m*(m::nat)"; 
1033 
by (induct_tac "m" 1); 

1034 
by Auto_tac; 

1035 
qed "le_square"; 

1036 

1037 
Goal "(m::nat) <= m*(m*m)"; 

1038 
by (induct_tac "m" 1); 

1039 
by Auto_tac; 

1040 
qed "le_cube"; 

1041 

1042 

4736  1043 
(*** Subtraction laws  mostly from Clemens Ballarin ***) 
3234  1044 

5429  1045 
Goal "[ a < (b::nat); c <= a ] ==> ac < bc"; 
6301  1046 
by (arith_tac 1); 
3234  1047 
qed "diff_less_mono"; 
1048 

5427  1049 
Goal "(i < jk) = (i+k < (j::nat))"; 
6301  1050 
by (arith_tac 1); 
5427  1051 
qed "less_diff_conv"; 
1052 

5497  1053 
Goal "(jk <= (i::nat)) = (j <= i+k)"; 
6301  1054 
by (arith_tac 1); 
5485  1055 
qed "le_diff_conv"; 
1056 

5497  1057 
Goal "k <= j ==> (i <= jk) = (i+k <= (j::nat))"; 
6301  1058 
by (arith_tac 1); 
5497  1059 
qed "le_diff_conv2"; 
1060 

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

1061 
Goal "Suc i <= n ==> Suc (n  Suc i) = n  i"; 
6301  1062 
by (arith_tac 1); 
3234  1063 
qed "Suc_diff_Suc"; 
1064 

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

1068 
Addsimps [diff_diff_cancel]; 
3234  1069 

5429  1070 
Goal "k <= (n::nat) ==> m <= n + m  k"; 
6301  1071 
by (arith_tac 1); 
3234  1072 
qed "le_add_diff"; 
1073 

5356  1074 
Goal "m1 < n ==> m <= n"; 
6301  1075 
by (arith_tac 1); 
5356  1076 
qed "pred_less_imp_le"; 
1077 

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

6301  1079 
by (arith_tac 1); 
5356  1080 
qed "diff_less_Suc_diff"; 
1081 

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

6301  1083 
by (arith_tac 1); 
5356  1084 
qed "diff_le_Suc_diff"; 
1085 
AddIffs [diff_le_Suc_diff]; 

1086 

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

6301  1088 
by (arith_tac 1); 
5356  1089 
qed "diff_Suc_le_diff"; 
1090 
AddIffs [diff_Suc_le_diff]; 

1091 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

1092 
Goal "!!m::nat. 0 < n ==> (m <= n1) = (m<n)"; 
6301  1093 
by (arith_tac 1); 
5409  1094 
qed "le_pred_eq"; 
1095 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

1096 
Goal "!!m::nat. 0 < n ==> (m1 < n) = (m<=n)"; 
6301  1097 
by (arith_tac 1); 
5409  1098 
qed "less_pred_eq"; 
1099 

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

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

1102 
Goal "!!m::nat. [ 0<n; 0<m ] ==> m  n < m"; 
6301  1103 
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

1104 
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

1105 

8740
fa6c4e4182d9
replaced obsolete diff_right_cancel by diff_diff_eq
paulson
parents:
8708
diff
changeset

1106 
Goal "j <= (k::nat) ==> (j+i)k = i(kj)"; 
8859  1107 
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); 
8740
fa6c4e4182d9
replaced obsolete diff_right_cancel by diff_diff_eq
paulson
parents:
8708
diff
changeset

1108 
qed "diff_add_assoc_diff"; 
fa6c4e4182d9
replaced obsolete diff_right_cancel by diff_diff_eq
paulson
parents:
8708
diff
changeset

1109 

fa6c4e4182d9
replaced obsolete diff_right_cancel by diff_diff_eq
paulson
parents:
8708
diff
changeset

1110 

8708
2f2d2b4215d6
added some new ifflemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset

1111 
(*** Reducing subtraction to addition ***) 
7128  1112 

1113 
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

1114 
by (simp_tac (simpset() addsplits [nat_diff_split]) 1); 
7128  1115 
qed_spec_mp "Suc_diff_add_le"; 
1116 

1117 
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

1118 
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); 
7128  1119 
qed "diff_Suc_less_diff"; 
1120 

1121 
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

1122 
by (simp_tac (simpset() addsplits [nat_diff_split]) 1); 
7128  1123 
qed "if_Suc_diff_le"; 
1124 

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

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

1126 
by (simp_tac (simpset() addsplits [nat_diff_split]) 1); 
7128  1127 
qed "diff_Suc_le_Suc_diff"; 
1128 

8740
fa6c4e4182d9
replaced obsolete diff_right_cancel by diff_diff_eq
paulson
parents:
8708
diff
changeset

1129 
(** Simplification of relational expressions involving subtraction **) 
7128  1130 

8740
fa6c4e4182d9
replaced obsolete diff_right_cancel by diff_diff_eq
paulson
parents:
8708
diff
changeset

1131 
Goal "[ k <= m; k <= (n::nat) ] ==> ((mk)  (nk)) = (mn)"; 
8859  1132 
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); 
8740
fa6c4e4182d9
replaced obsolete diff_right_cancel by diff_diff_eq
paulson
parents:
8708
diff
changeset

1133 
qed "diff_diff_eq"; 
8708
2f2d2b4215d6
added some new ifflemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset

1134 

2f2d2b4215d6
added some new ifflemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset

1135 
Goal "[ k <= m; k <= (n::nat) ] ==> (mk = nk) = (m=n)"; 
8859  1136 
by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); 
8708
2f2d2b4215d6
added some new ifflemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset

1137 
qed "eq_diff_iff"; 
2f2d2b4215d6
added some new ifflemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset

1138 

2f2d2b4215d6
added some new ifflemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset

1139 
Goal "[ k <= m; k <= (n::nat) ] ==> (mk < nk) = (m<n)"; 
8859  1140 
by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); 
8708
2f2d2b4215d6
added some new ifflemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset

1141 
qed "less_diff_iff"; 
2f2d2b4215d6
added some new ifflemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset

1142 

2f2d2b4215d6
added some new ifflemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset

1143 
Goal "[ k <= m; k <= (n::nat) ] ==> (mk <= nk) = (m<=n)"; 
8859  1144 
by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); 
8708
2f2d2b4215d6
added some new ifflemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset

1145 
qed "le_diff_iff"; 
2f2d2b4215d6
added some new ifflemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset

1146 

7128  1147 

7108  1148 
(** (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

1149 

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

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

1152 
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); 
6055  1153 
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

1154 

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

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

6055  1159 
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

1160 
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); 
6055  1161 
qed "diff_less_mono2"; 
5983  1162 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

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

1164 
by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1); 
6055  1165 
qed "diffs0_imp_equal"; 
8352  1166 

1167 
(** Lemmas for ex/Factorization **) 

1168 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

1169 
Goal "!!m::nat. [ 1<n; 1<m ] ==> 1<m*n"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

1170 
by (case_tac "m" 1); 
8352  1171 
by Auto_tac; 
1172 
qed "one_less_mult"; 

1173 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

1174 
Goal "!!m::nat. [ 1<n; 1<m ] ==> n<m*n"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

1175 
by (case_tac "m" 1); 
8352  1176 
by Auto_tac; 
1177 
qed "n_less_m_mult_n"; 

1178 

8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset

1179 
Goal "!!m::nat. [ 1<n; 1<m ] ==> n<n*m"; 
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset

1180 
by (case_tac "m" 1); 
8352  1181 
by Auto_tac; 
1182 
qed "n_less_n_mult_m"; 

8859  1183 

1184 

1185 
(** Rewriting to pull differences out **) 

1186 

1187 
Goal "k<=j > i  (j  k) = i + (k::nat)  j"; 

1188 
by (arith_tac 1); 

1189 
qed "diff_diff_right"; 

1190 

1191 
Goal "k <= j ==> m  Suc (j  k) = m + k  Suc j"; 

1192 
by (arith_tac 1); 

1193 
qed "diff_Suc_diff_eq1"; 

1194 

1195 
Goal "k <= j ==> Suc (j  k)  m = Suc j  (k + m)"; 

1196 
by (arith_tac 1); 

1197 
qed "diff_Suc_diff_eq2"; 

1198 

1199 
(*The others are 

1200 
i  j  k = i  (j + k), 

1201 
k <= j ==> j  k + i = j + i  k, 

1202 
k <= j ==> i + (j  k) = i + j  k *) 

1203 
Addsimps [diff_diff_left, diff_diff_right, diff_add_assoc2 RS sym, 

1204 
diff_add_assoc RS sym, diff_Suc_diff_eq1, diff_Suc_diff_eq2]; 

1205 