|
1 (* Title: HOL/NatArith.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Further proofs about elementary arithmetic, using the arithmetic proof |
|
7 procedures. |
|
8 *) |
|
9 |
|
10 (*legacy ...*) |
|
11 structure NatArith = struct val thy = the_context () end; |
|
12 |
|
13 |
|
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 |
|
25 (*** Subtraction laws -- mostly from Clemens Ballarin ***) |
|
26 |
|
27 Goal "[| a < (b::nat); c <= a |] ==> a-c < b-c"; |
|
28 by (arith_tac 1); |
|
29 qed "diff_less_mono"; |
|
30 |
|
31 Goal "(i < j-k) = (i+k < (j::nat))"; |
|
32 by (arith_tac 1); |
|
33 qed "less_diff_conv"; |
|
34 |
|
35 Goal "(j-k <= (i::nat)) = (j <= i+k)"; |
|
36 by (arith_tac 1); |
|
37 qed "le_diff_conv"; |
|
38 |
|
39 Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))"; |
|
40 by (arith_tac 1); |
|
41 qed "le_diff_conv2"; |
|
42 |
|
43 Goal "Suc i <= n ==> Suc (n - Suc i) = n - i"; |
|
44 by (arith_tac 1); |
|
45 qed "Suc_diff_Suc"; |
|
46 |
|
47 Goal "i <= (n::nat) ==> n - (n - i) = i"; |
|
48 by (arith_tac 1); |
|
49 qed "diff_diff_cancel"; |
|
50 Addsimps [diff_diff_cancel]; |
|
51 |
|
52 Goal "k <= (n::nat) ==> m <= n + m - k"; |
|
53 by (arith_tac 1); |
|
54 qed "le_add_diff"; |
|
55 |
|
56 Goal "m-1 < n ==> m <= n"; |
|
57 by (arith_tac 1); |
|
58 qed "pred_less_imp_le"; |
|
59 |
|
60 Goal "j<=i ==> i - j < Suc i - j"; |
|
61 by (arith_tac 1); |
|
62 qed "diff_less_Suc_diff"; |
|
63 |
|
64 Goal "i - j <= Suc i - j"; |
|
65 by (arith_tac 1); |
|
66 qed "diff_le_Suc_diff"; |
|
67 AddIffs [diff_le_Suc_diff]; |
|
68 |
|
69 Goal "n - Suc i <= n - i"; |
|
70 by (arith_tac 1); |
|
71 qed "diff_Suc_le_diff"; |
|
72 AddIffs [diff_Suc_le_diff]; |
|
73 |
|
74 Goal "!!m::nat. 0 < n ==> (m <= n-1) = (m<n)"; |
|
75 by (arith_tac 1); |
|
76 qed "le_pred_eq"; |
|
77 |
|
78 Goal "!!m::nat. 0 < n ==> (m-1 < n) = (m<=n)"; |
|
79 by (arith_tac 1); |
|
80 qed "less_pred_eq"; |
|
81 |
|
82 (*Replaces the previous diff_less and le_diff_less, which had the stronger |
|
83 second premise n<=m*) |
|
84 Goal "!!m::nat. [| 0<n; 0<m |] ==> m - n < m"; |
|
85 by (arith_tac 1); |
|
86 qed "diff_less"; |
|
87 |
|
88 Goal "j <= (k::nat) ==> (j+i)-k = i-(k-j)"; |
|
89 by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); |
|
90 qed "diff_add_assoc_diff"; |
|
91 |
|
92 |
|
93 (*** Reducing subtraction to addition ***) |
|
94 |
|
95 Goal "n<=(l::nat) --> Suc l - n + m = Suc (l - n + m)"; |
|
96 by (simp_tac (simpset() addsplits [nat_diff_split]) 1); |
|
97 qed_spec_mp "Suc_diff_add_le"; |
|
98 |
|
99 Goal "i<n ==> n - Suc i < n - i"; |
|
100 by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); |
|
101 qed "diff_Suc_less_diff"; |
|
102 |
|
103 Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))"; |
|
104 by (simp_tac (simpset() addsplits [nat_diff_split]) 1); |
|
105 qed "if_Suc_diff_le"; |
|
106 |
|
107 Goal "Suc(m)-n <= Suc(m-n)"; |
|
108 by (simp_tac (simpset() addsplits [nat_diff_split]) 1); |
|
109 qed "diff_Suc_le_Suc_diff"; |
|
110 |
|
111 (** Simplification of relational expressions involving subtraction **) |
|
112 |
|
113 Goal "[| k <= m; k <= (n::nat) |] ==> ((m-k) - (n-k)) = (m-n)"; |
|
114 by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); |
|
115 qed "diff_diff_eq"; |
|
116 |
|
117 Goal "[| k <= m; k <= (n::nat) |] ==> (m-k = n-k) = (m=n)"; |
|
118 by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); |
|
119 qed "eq_diff_iff"; |
|
120 |
|
121 Goal "[| k <= m; k <= (n::nat) |] ==> (m-k < n-k) = (m<n)"; |
|
122 by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); |
|
123 qed "less_diff_iff"; |
|
124 |
|
125 Goal "[| k <= m; k <= (n::nat) |] ==> (m-k <= n-k) = (m<=n)"; |
|
126 by (auto_tac (claset(), simpset() addsplits [nat_diff_split])); |
|
127 qed "le_diff_iff"; |
|
128 |
|
129 |
|
130 (** (Anti)Monotonicity of subtraction -- by Stephan Merz **) |
|
131 |
|
132 (* Monotonicity of subtraction in first argument *) |
|
133 Goal "m <= (n::nat) ==> (m-l) <= (n-l)"; |
|
134 by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); |
|
135 qed "diff_le_mono"; |
|
136 |
|
137 Goal "m <= (n::nat) ==> (l-n) <= (l-m)"; |
|
138 by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); |
|
139 qed "diff_le_mono2"; |
|
140 |
|
141 Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)"; |
|
142 by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1); |
|
143 qed "diff_less_mono2"; |
|
144 |
|
145 Goal "!!m::nat. [| m-n = 0; n-m = 0 |] ==> m=n"; |
|
146 by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1); |
|
147 qed "diffs0_imp_equal"; |
|
148 |
|
149 (** Lemmas for ex/Factorization **) |
|
150 |
|
151 Goal "!!m::nat. [| 1<n; 1<m |] ==> 1<m*n"; |
|
152 by (case_tac "m" 1); |
|
153 by Auto_tac; |
|
154 qed "one_less_mult"; |
|
155 |
|
156 Goal "!!m::nat. [| 1<n; 1<m |] ==> n<m*n"; |
|
157 by (case_tac "m" 1); |
|
158 by Auto_tac; |
|
159 qed "n_less_m_mult_n"; |
|
160 |
|
161 Goal "!!m::nat. [| 1<n; 1<m |] ==> n<n*m"; |
|
162 by (case_tac "m" 1); |
|
163 by Auto_tac; |
|
164 qed "n_less_n_mult_m"; |
|
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 |