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) =
|
|
59 |
mk_meta_eq (prove_goalw_cterm [] (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
|
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;
|