1 (* Title: HOL/arith_data.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel and Stefan Berghofer, TU Muenchen |
|
4 |
|
5 Setup various arithmetic proof procedures. |
|
6 *) |
|
7 |
|
8 signature ARITH_DATA = |
|
9 sig |
|
10 val nat_cancel_sums: simproc list |
|
11 val nat_cancel_factor: simproc list |
|
12 val nat_cancel: simproc list |
|
13 end; |
|
14 |
|
15 structure ArithData: ARITH_DATA = |
|
16 struct |
|
17 |
|
18 |
|
19 (** abstract syntax of structure nat: 0, Suc, + **) |
|
20 |
|
21 (* mk_sum, mk_norm_sum *) |
|
22 |
|
23 val one = HOLogic.mk_nat 1; |
|
24 val mk_plus = HOLogic.mk_binop "op +"; |
|
25 |
|
26 fun mk_sum [] = HOLogic.zero |
|
27 | mk_sum [t] = t |
|
28 | mk_sum (t :: ts) = mk_plus (t, mk_sum ts); |
|
29 |
|
30 (*normal form of sums: Suc (... (Suc (a + (b + ...))))*) |
|
31 fun mk_norm_sum ts = |
|
32 let val (ones, sums) = partition (equal one) ts in |
|
33 funpow (length ones) HOLogic.mk_Suc (mk_sum sums) |
|
34 end; |
|
35 |
|
36 |
|
37 (* dest_sum *) |
|
38 |
|
39 val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT; |
|
40 |
|
41 fun dest_sum tm = |
|
42 if HOLogic.is_zero tm then [] |
|
43 else |
|
44 (case try HOLogic.dest_Suc tm of |
|
45 Some t => one :: dest_sum t |
|
46 | None => |
|
47 (case try dest_plus tm of |
|
48 Some (t, u) => dest_sum t @ dest_sum u |
|
49 | None => [tm])); |
|
50 |
|
51 |
|
52 (** generic proof tools **) |
|
53 |
|
54 (* prove conversions *) |
|
55 |
|
56 val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq; |
|
57 |
|
58 fun prove_conv expand_tac norm_tac sg (t, u) = |
|
59 mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u))) |
|
60 (K [expand_tac, norm_tac])) |
|
61 handle ERROR => error ("The error(s) above occurred while trying to prove " ^ |
|
62 (string_of_cterm (cterm_of sg (mk_eqv (t, u))))); |
|
63 |
|
64 val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s" |
|
65 (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]); |
|
66 |
|
67 |
|
68 (* rewriting *) |
|
69 |
|
70 fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules)); |
|
71 |
|
72 val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right]; |
|
73 val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right]; |
|
74 |
|
75 |
|
76 |
|
77 (** cancel common summands **) |
|
78 |
|
79 structure Sum = |
|
80 struct |
|
81 val mk_sum = mk_norm_sum; |
|
82 val dest_sum = dest_sum; |
|
83 val prove_conv = prove_conv; |
|
84 val norm_tac = simp_all add_rules THEN simp_all add_ac; |
|
85 end; |
|
86 |
|
87 fun gen_uncancel_tac rule ct = |
|
88 rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1; |
|
89 |
|
90 |
|
91 (* nat eq *) |
|
92 |
|
93 structure EqCancelSums = CancelSumsFun |
|
94 (struct |
|
95 open Sum; |
|
96 val mk_bal = HOLogic.mk_eq; |
|
97 val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT; |
|
98 val uncancel_tac = gen_uncancel_tac add_left_cancel; |
|
99 end); |
|
100 |
|
101 |
|
102 (* nat less *) |
|
103 |
|
104 structure LessCancelSums = CancelSumsFun |
|
105 (struct |
|
106 open Sum; |
|
107 val mk_bal = HOLogic.mk_binrel "op <"; |
|
108 val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT; |
|
109 val uncancel_tac = gen_uncancel_tac add_left_cancel_less; |
|
110 end); |
|
111 |
|
112 |
|
113 (* nat le *) |
|
114 |
|
115 structure LeCancelSums = CancelSumsFun |
|
116 (struct |
|
117 open Sum; |
|
118 val mk_bal = HOLogic.mk_binrel "op <="; |
|
119 val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT; |
|
120 val uncancel_tac = gen_uncancel_tac add_left_cancel_le; |
|
121 end); |
|
122 |
|
123 |
|
124 (* nat diff *) |
|
125 |
|
126 structure DiffCancelSums = CancelSumsFun |
|
127 (struct |
|
128 open Sum; |
|
129 val mk_bal = HOLogic.mk_binop "op -"; |
|
130 val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT; |
|
131 val uncancel_tac = gen_uncancel_tac diff_cancel; |
|
132 end); |
|
133 |
|
134 |
|
135 |
|
136 (** cancel common factor **) |
|
137 |
|
138 structure Factor = |
|
139 struct |
|
140 val mk_sum = mk_norm_sum; |
|
141 val dest_sum = dest_sum; |
|
142 val prove_conv = prove_conv; |
|
143 val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac; |
|
144 end; |
|
145 |
|
146 fun mk_cnat n = cterm_of (sign_of Nat.thy) (HOLogic.mk_nat n); |
|
147 |
|
148 fun gen_multiply_tac rule k = |
|
149 if k > 0 then |
|
150 rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1 |
|
151 else no_tac; |
|
152 |
|
153 |
|
154 (* nat eq *) |
|
155 |
|
156 structure EqCancelFactor = CancelFactorFun |
|
157 (struct |
|
158 open Factor; |
|
159 val mk_bal = HOLogic.mk_eq; |
|
160 val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT; |
|
161 val multiply_tac = gen_multiply_tac Suc_mult_cancel1; |
|
162 end); |
|
163 |
|
164 |
|
165 (* nat less *) |
|
166 |
|
167 structure LessCancelFactor = CancelFactorFun |
|
168 (struct |
|
169 open Factor; |
|
170 val mk_bal = HOLogic.mk_binrel "op <"; |
|
171 val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT; |
|
172 val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1; |
|
173 end); |
|
174 |
|
175 |
|
176 (* nat le *) |
|
177 |
|
178 structure LeCancelFactor = CancelFactorFun |
|
179 (struct |
|
180 open Factor; |
|
181 val mk_bal = HOLogic.mk_binrel "op <="; |
|
182 val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT; |
|
183 val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1; |
|
184 end); |
|
185 |
|
186 |
|
187 |
|
188 (** prepare nat_cancel simprocs **) |
|
189 |
|
190 fun prep_pat s = Thm.read_cterm (sign_of Arith.thy) (s, HOLogic.termTVar); |
|
191 val prep_pats = map prep_pat; |
|
192 |
|
193 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; |
|
194 |
|
195 val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]; |
|
196 val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]; |
|
197 val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]; |
|
198 val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]; |
|
199 |
|
200 val nat_cancel_sums = map prep_simproc |
|
201 [("nateq_cancel_sums", eq_pats, EqCancelSums.proc), |
|
202 ("natless_cancel_sums", less_pats, LessCancelSums.proc), |
|
203 ("natle_cancel_sums", le_pats, LeCancelSums.proc), |
|
204 ("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)]; |
|
205 |
|
206 val nat_cancel_factor = map prep_simproc |
|
207 [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc), |
|
208 ("natless_cancel_factor", less_pats, LessCancelFactor.proc), |
|
209 ("natle_cancel_factor", le_pats, LeCancelFactor.proc)]; |
|
210 |
|
211 val nat_cancel = nat_cancel_factor @ nat_cancel_sums; |
|
212 |
|
213 |
|
214 end; |
|
215 |
|
216 |
|
217 open ArithData; |
|
218 |
|
219 |
|
220 context Arith.thy; |
|
221 Addsimprocs nat_cancel; |
|
222 |
|
223 |
|
224 (*This proof requires natdiff_cancel_sums*) |
|
225 Goal "m < (n::nat) --> m<l --> (l-n) < (l-m)"; |
|
226 by (induct_tac "l" 1); |
|
227 by (Simp_tac 1); |
|
228 by (Clarify_tac 1); |
|
229 by (etac less_SucE 1); |
|
230 by (Clarify_tac 2); |
|
231 by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 2); |
|
232 by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans, |
|
233 Suc_diff_le, less_imp_le]) 1); |
|
234 qed_spec_mp "diff_less_mono2"; |
|
235 |
|
236 (** Elimination of - on nat due to John Harrison **) |
|
237 (*This proof requires natle_cancel_sums*) |
|
238 |
|
239 Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))"; |
|
240 by(case_tac "a <= b" 1); |
|
241 by(Auto_tac); |
|
242 by(eres_inst_tac [("x","b-a")] allE 1); |
|
243 by(Auto_tac); |
|
244 qed "nat_diff_split"; |
|
245 |
|
246 (* |
|
247 This is an example of the power of nat_diff_split. Many of the `-' thms in |
|
248 Arith.ML could take advantage of this, but would need to be moved. |
|
249 *) |
|
250 Goal "m-n = 0 --> n-m = 0 --> m=n"; |
|
251 by(simp_tac (simpset() addsplits [nat_diff_split]) 1); |
|
252 qed_spec_mp "diffs0_imp_equal"; |
|
253 |
|
254 use"fast_nat_decider"; |
|
255 |
|
256 simpset_ref () := (simpset() addSolver |
|
257 (fn thms => cut_facts_tac thms THEN' Fast_Nat_Decider.nat_arith_tac)); |
|