author | nipkow |
Wed, 28 Oct 1998 11:25:38 +0100 | |
changeset 5771 | 7c2c8cf20221 |
parent 5591 | fbb4e1ac234d |
child 5983 | 79e301a6a51b |
permissions | -rw-r--r-- |
4295 | 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 |
|
4309 | 10 |
val nat_cancel_sums: simproc list |
11 |
val nat_cancel_factor: simproc list |
|
4295 | 12 |
val nat_cancel: simproc list |
13 |
end; |
|
14 |
||
4309 | 15 |
structure ArithData: ARITH_DATA = |
4295 | 16 |
struct |
17 |
||
18 |
||
19 |
(** abstract syntax of structure nat: 0, Suc, + **) |
|
20 |
||
4310 | 21 |
(* mk_sum, mk_norm_sum *) |
4295 | 22 |
|
4310 | 23 |
val one = HOLogic.mk_nat 1; |
4295 | 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 |
||
4310 | 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 |
||
4295 | 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) = |
|
5553 | 59 |
mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u))) |
4295 | 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 |
|
4310 | 81 |
val mk_sum = mk_norm_sum; |
4295 | 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 |
||
4332 | 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); |
|
4295 | 133 |
|
134 |
||
135 |
||
136 |
(** cancel common factor **) |
|
137 |
||
138 |
structure Factor = |
|
139 |
struct |
|
4310 | 140 |
val mk_sum = mk_norm_sum; |
4295 | 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"]; |
|
4332 | 198 |
val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]; |
4295 | 199 |
|
4309 | 200 |
val nat_cancel_sums = map prep_simproc |
201 |
[("nateq_cancel_sums", eq_pats, EqCancelSums.proc), |
|
4295 | 202 |
("natless_cancel_sums", less_pats, LessCancelSums.proc), |
4332 | 203 |
("natle_cancel_sums", le_pats, LeCancelSums.proc), |
204 |
("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)]; |
|
4295 | 205 |
|
4309 | 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 |
||
4295 | 213 |
|
214 |
end; |
|
4336 | 215 |
|
216 |
||
217 |
open ArithData; |
|
4368
1f2dd130fe39
simplification procedures nat_cancel enabled by default;
wenzelm
parents:
4336
diff
changeset
|
218 |
|
1f2dd130fe39
simplification procedures nat_cancel enabled by default;
wenzelm
parents:
4336
diff
changeset
|
219 |
|
1f2dd130fe39
simplification procedures nat_cancel enabled by default;
wenzelm
parents:
4336
diff
changeset
|
220 |
context Arith.thy; |
1f2dd130fe39
simplification procedures nat_cancel enabled by default;
wenzelm
parents:
4336
diff
changeset
|
221 |
Addsimprocs nat_cancel; |
4675 | 222 |
|
223 |
||
224 |
(*This proof requires natdiff_cancel_sums*) |
|
5429 | 225 |
Goal "m < (n::nat) --> m<l --> (l-n) < (l-m)"; |
4675 | 226 |
by (induct_tac "l" 1); |
227 |
by (Simp_tac 1); |
|
228 |
by (Clarify_tac 1); |
|
5132 | 229 |
by (etac less_SucE 1); |
5429 | 230 |
by (Clarify_tac 2); |
231 |
by (asm_simp_tac (simpset() addsimps [Suc_le_eq]) 2); |
|
4675 | 232 |
by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans, |
5591 | 233 |
Suc_diff_le, less_imp_le]) 1); |
4675 | 234 |
qed_spec_mp "diff_less_mono2"; |
5771 | 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"; |