author | wenzelm |
Sun, 30 Jul 2000 13:02:14 +0200 | |
changeset 9473 | 7d13a5ace928 |
parent 9436 | 62bb04ab4b01 |
permissions | -rw-r--r-- |
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 |
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9073
diff
changeset
|
6 |
Further proofs about elementary arithmetic, using the arithmetic proof |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9073
diff
changeset
|
7 |
procedures. |
923 | 8 |
*) |
9 |
||
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9073
diff
changeset
|
10 |
(*legacy ...*) |
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9073
diff
changeset
|
11 |
structure Arith = struct val thy = the_context () end; |
1713 | 12 |
|
5983 | 13 |
|
8833 | 14 |
Goal "m <= m*(m::nat)"; |
15 |
by (induct_tac "m" 1); |
|
16 |
by Auto_tac; |
|
17 |
qed "le_square"; |
|
18 |
||
19 |
Goal "(m::nat) <= m*(m*m)"; |
|
20 |
by (induct_tac "m" 1); |
|
21 |
by Auto_tac; |
|
22 |
qed "le_cube"; |
|
23 |
||
24 |
||
4736 | 25 |
(*** Subtraction laws -- mostly from Clemens Ballarin ***) |
3234 | 26 |
|
5429 | 27 |
Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c"; |
6301 | 28 |
by (arith_tac 1); |
3234 | 29 |
qed "diff_less_mono"; |
30 |
||
5427 | 31 |
Goal "(i < j-k) = (i+k < (j::nat))"; |
6301 | 32 |
by (arith_tac 1); |
5427 | 33 |
qed "less_diff_conv"; |
34 |
||
5497 | 35 |
Goal "(j-k <= (i::nat)) = (j <= i+k)"; |
6301 | 36 |
by (arith_tac 1); |
5485 | 37 |
qed "le_diff_conv"; |
38 |
||
5497 | 39 |
Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))"; |
6301 | 40 |
by (arith_tac 1); |
5497 | 41 |
qed "le_diff_conv2"; |
42 |
||
5143
b94cd208f073
Removal of leading "\!\!..." from most Goal commands
paulson
parents:
5078
diff
changeset
|
43 |
Goal "Suc i <= n ==> Suc (n - Suc i) = n - i"; |
6301 | 44 |
by (arith_tac 1); |
3234 | 45 |
qed "Suc_diff_Suc"; |
46 |
||
5429 | 47 |
Goal "i <= (n::nat) ==> n - (n - i) = i"; |
6301 | 48 |
by (arith_tac 1); |
3234 | 49 |
qed "diff_diff_cancel"; |
3381
2bac33ec2b0d
New theorems le_add_diff_inverse, le_add_diff_inverse2
paulson
parents:
3366
diff
changeset
|
50 |
Addsimps [diff_diff_cancel]; |
3234 | 51 |
|
5429 | 52 |
Goal "k <= (n::nat) ==> m <= n + m - k"; |
6301 | 53 |
by (arith_tac 1); |
3234 | 54 |
qed "le_add_diff"; |
55 |
||
5356 | 56 |
Goal "m-1 < n ==> m <= n"; |
6301 | 57 |
by (arith_tac 1); |
5356 | 58 |
qed "pred_less_imp_le"; |
59 |
||
60 |
Goal "j<=i ==> i - j < Suc i - j"; |
|
6301 | 61 |
by (arith_tac 1); |
5356 | 62 |
qed "diff_less_Suc_diff"; |
63 |
||
64 |
Goal "i - j <= Suc i - j"; |
|
6301 | 65 |
by (arith_tac 1); |
5356 | 66 |
qed "diff_le_Suc_diff"; |
67 |
AddIffs [diff_le_Suc_diff]; |
|
68 |
||
69 |
Goal "n - Suc i <= n - i"; |
|
6301 | 70 |
by (arith_tac 1); |
5356 | 71 |
qed "diff_Suc_le_diff"; |
72 |
AddIffs [diff_Suc_le_diff]; |
|
73 |
||
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset
|
74 |
Goal "!!m::nat. 0 < n ==> (m <= n-1) = (m<n)"; |
6301 | 75 |
by (arith_tac 1); |
5409 | 76 |
qed "le_pred_eq"; |
77 |
||
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset
|
78 |
Goal "!!m::nat. 0 < n ==> (m-1 < n) = (m<=n)"; |
6301 | 79 |
by (arith_tac 1); |
5409 | 80 |
qed "less_pred_eq"; |
81 |
||
7059 | 82 |
(*Replaces the previous diff_less and le_diff_less, which had the stronger |
83 |
second premise n<=m*) |
|
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset
|
84 |
Goal "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"; |
6301 | 85 |
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
|
86 |
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
|
87 |
|
8740
fa6c4e4182d9
replaced obsolete diff_right_cancel by diff_diff_eq
paulson
parents:
8708
diff
changeset
|
88 |
Goal "j <= (k::nat) ==> (j+i)-k = i-(k-j)"; |
8859 | 89 |
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
|
90 |
qed "diff_add_assoc_diff"; |
fa6c4e4182d9
replaced obsolete diff_right_cancel by diff_diff_eq
paulson
parents:
8708
diff
changeset
|
91 |
|
fa6c4e4182d9
replaced obsolete diff_right_cancel by diff_diff_eq
paulson
parents:
8708
diff
changeset
|
92 |
|
8708
2f2d2b4215d6
added some new iff-lemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset
|
93 |
(*** Reducing subtraction to addition ***) |
7128 | 94 |
|
95 |
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
|
96 |
by (simp_tac (simpset() addsplits [nat_diff_split]) 1); |
7128 | 97 |
qed_spec_mp "Suc_diff_add_le"; |
98 |
||
99 |
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
|
100 |
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); |
7128 | 101 |
qed "diff_Suc_less_diff"; |
102 |
||
103 |
Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))"; |
|
7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset
|
104 |
by (simp_tac (simpset() addsplits [nat_diff_split]) 1); |
7128 | 105 |
qed "if_Suc_diff_le"; |
106 |
||
107 |
Goal "Suc(m)-n <= Suc(m-n)"; |
|
7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset
|
108 |
by (simp_tac (simpset() addsplits [nat_diff_split]) 1); |
7128 | 109 |
qed "diff_Suc_le_Suc_diff"; |
110 |
||
8740
fa6c4e4182d9
replaced obsolete diff_right_cancel by diff_diff_eq
paulson
parents:
8708
diff
changeset
|
111 |
(** Simplification of relational expressions involving subtraction **) |
7128 | 112 |
|
8740
fa6c4e4182d9
replaced obsolete diff_right_cancel by diff_diff_eq
paulson
parents:
8708
diff
changeset
|
113 |
Goal "[| k <= m; k <= (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"; |
8859 | 114 |
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
|
115 |
qed "diff_diff_eq"; |
8708
2f2d2b4215d6
added some new iff-lemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset
|
116 |
|
2f2d2b4215d6
added some new iff-lemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset
|
117 |
Goal "[| k <= m; k <= (n::nat) |] ==> (m-k = n-k) = (m=n)"; |
8859 | 118 |
by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); |
8708
2f2d2b4215d6
added some new iff-lemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset
|
119 |
qed "eq_diff_iff"; |
2f2d2b4215d6
added some new iff-lemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset
|
120 |
|
2f2d2b4215d6
added some new iff-lemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset
|
121 |
Goal "[| k <= m; k <= (n::nat) |] ==> (m-k < n-k) = (m<n)"; |
8859 | 122 |
by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); |
8708
2f2d2b4215d6
added some new iff-lemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset
|
123 |
qed "less_diff_iff"; |
2f2d2b4215d6
added some new iff-lemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset
|
124 |
|
2f2d2b4215d6
added some new iff-lemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset
|
125 |
Goal "[| k <= m; k <= (n::nat) |] ==> (m-k <= n-k) = (m<=n)"; |
8859 | 126 |
by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); |
8708
2f2d2b4215d6
added some new iff-lemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset
|
127 |
qed "le_diff_iff"; |
2f2d2b4215d6
added some new iff-lemmas; removed some obsolete thms
paulson
parents:
8571
diff
changeset
|
128 |
|
7128 | 129 |
|
7108 | 130 |
(** (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
|
131 |
|
1e93eb09ebb9
Added the following lemmas tp Divides and a few others to Arith and NatDef:
nipkow
parents:
3457
diff
changeset
|
132 |
(* Monotonicity of subtraction in first argument *) |
6055 | 133 |
Goal "m <= (n::nat) ==> (m-l) <= (n-l)"; |
7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset
|
134 |
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); |
6055 | 135 |
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
|
136 |
|
5429 | 137 |
Goal "m <= (n::nat) ==> (l-n) <= (l-m)"; |
7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset
|
138 |
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); |
6055 | 139 |
qed "diff_le_mono2"; |
5983 | 140 |
|
6055 | 141 |
Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"; |
7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset
|
142 |
by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); |
6055 | 143 |
qed "diff_less_mono2"; |
5983 | 144 |
|
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset
|
145 |
Goal "!!m::nat. [| m-n = 0; n-m = 0 |] ==> m=n"; |
7945
3aca6352f063
got rid of split_diff, which duplicated nat_diff_split, and
paulson
parents:
7622
diff
changeset
|
146 |
by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1); |
6055 | 147 |
qed "diffs0_imp_equal"; |
8352 | 148 |
|
149 |
(** Lemmas for ex/Factorization **) |
|
150 |
||
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset
|
151 |
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
|
152 |
by (case_tac "m" 1); |
8352 | 153 |
by Auto_tac; |
154 |
qed "one_less_mult"; |
|
155 |
||
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset
|
156 |
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
|
157 |
by (case_tac "m" 1); |
8352 | 158 |
by Auto_tac; |
159 |
qed "n_less_m_mult_n"; |
|
160 |
||
8935
548901d05a0e
added type constraint ::nat because 0 is now overloaded
paulson
parents:
8859
diff
changeset
|
161 |
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
|
162 |
by (case_tac "m" 1); |
8352 | 163 |
by Auto_tac; |
164 |
qed "n_less_n_mult_m"; |
|
8859 | 165 |
|
166 |
||
167 |
(** Rewriting to pull differences out **) |
|
168 |
||
169 |
Goal "k<=j --> i - (j - k) = i + (k::nat) - j"; |
|
170 |
by (arith_tac 1); |
|
171 |
qed "diff_diff_right"; |
|
172 |
||
173 |
Goal "k <= j ==> m - Suc (j - k) = m + k - Suc j"; |
|
174 |
by (arith_tac 1); |
|
175 |
qed "diff_Suc_diff_eq1"; |
|
176 |
||
177 |
Goal "k <= j ==> Suc (j - k) - m = Suc j - (k + m)"; |
|
178 |
by (arith_tac 1); |
|
179 |
qed "diff_Suc_diff_eq2"; |
|
180 |
||
181 |
(*The others are |
|
182 |
i - j - k = i - (j + k), |
|
183 |
k <= j ==> j - k + i = j + i - k, |
|
184 |
k <= j ==> i + (j - k) = i + j - k *) |
|
185 |
Addsimps [diff_diff_left, diff_diff_right, diff_add_assoc2 RS sym, |
|
186 |
diff_add_assoc RS sym, diff_Suc_diff_eq1, diff_Suc_diff_eq2]; |
|
187 |