author | wenzelm |
Thu, 16 Jan 1997 14:53:37 +0100 | |
changeset 2509 | 0a7169d89b7a |
parent 2503 | 7590fd5ce3c7 |
child 2521 | b7dd670cfe3a |
permissions | -rw-r--r-- |
1243 | 1 |
(* Title: Provers/simplifier.ML |
1 | 2 |
ID: $Id$ |
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1993 TU Munich |
|
5 |
||
6 |
Generic simplifier, suitable for most logics. |
|
2503 | 7 |
|
8 |
TODO: |
|
9 |
- stamps to identify funs / tacs |
|
10 |
- merge: fail if incompatible funs |
|
2509 | 11 |
- improve merge |
1 | 12 |
*) |
1260 | 13 |
|
2509 | 14 |
infix 4 addsimps addeqcongs addsimprocs delsimprocs addsolver delsimps |
15 |
setsolver setloop setmksimps settermless setsubgoaler; |
|
0 | 16 |
|
17 |
signature SIMPLIFIER = |
|
18 |
sig |
|
2509 | 19 |
type simproc |
20 |
val mk_simproc: string -> cterm list -> (Sign.sg -> term -> thm option) -> simproc |
|
21 |
val name_of_simproc: simproc -> string |
|
22 |
val conv_prover: (term * term -> term) -> thm -> (thm -> thm) |
|
23 |
-> tactic -> (int -> tactic) -> Sign.sg -> term -> term -> thm (* FIXME move?, rename? *) |
|
0 | 24 |
type simpset |
2503 | 25 |
val empty_ss: simpset |
2509 | 26 |
val rep_ss: simpset -> {simps: thm list, procs: string list, congs: thm list} |
2503 | 27 |
val prems_of_ss: simpset -> thm list |
28 |
val setloop: simpset * (int -> tactic) -> simpset |
|
29 |
val setsolver: simpset * (thm list -> int -> tactic) -> simpset |
|
30 |
val addsolver: simpset * (thm list -> int -> tactic) -> simpset |
|
31 |
val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset |
|
32 |
val setmksimps: simpset * (thm -> thm list) -> simpset |
|
2509 | 33 |
val settermless: simpset * (term * term -> bool) -> simpset |
0 | 34 |
val addsimps: simpset * thm list -> simpset |
88 | 35 |
val delsimps: simpset * thm list -> simpset |
2509 | 36 |
val addsimprocs: simpset * simproc list -> simpset |
37 |
val delsimprocs: simpset * simproc list -> simpset |
|
2503 | 38 |
val addeqcongs: simpset * thm list -> simpset |
0 | 39 |
val merge_ss: simpset * simpset -> simpset |
1243 | 40 |
val simpset: simpset ref |
41 |
val Addsimps: thm list -> unit |
|
42 |
val Delsimps: thm list -> unit |
|
2509 | 43 |
val Addsimprocs: simproc list -> unit |
44 |
val Delsimprocs: simproc list -> unit |
|
2503 | 45 |
val simp_tac: simpset -> int -> tactic |
46 |
val asm_simp_tac: simpset -> int -> tactic |
|
47 |
val full_simp_tac: simpset -> int -> tactic |
|
48 |
val asm_full_simp_tac: simpset -> int -> tactic |
|
49 |
val Simp_tac: int -> tactic |
|
1676 | 50 |
val Asm_simp_tac: int -> tactic |
51 |
val Full_simp_tac: int -> tactic |
|
1243 | 52 |
val Asm_full_simp_tac: int -> tactic |
0 | 53 |
end; |
54 |
||
2503 | 55 |
|
56 |
structure Simplifier: SIMPLIFIER = |
|
0 | 57 |
struct |
58 |
||
2509 | 59 |
|
60 |
(** simplification procedures **) |
|
61 |
||
62 |
(* datatype simproc *) |
|
63 |
||
64 |
datatype simproc = |
|
65 |
Simproc of { |
|
66 |
name: string, |
|
67 |
procs: (Sign.sg * term * (Sign.sg -> term -> thm option) * stamp) list} |
|
68 |
||
69 |
(* FIXME stamps!? *) |
|
70 |
fun eq_simproc (Simproc {name = name1, ...}, Simproc {name = name2, ...}) = |
|
71 |
(name1 = name2); |
|
72 |
||
73 |
fun mk_simproc name lhss proc = |
|
74 |
let |
|
75 |
fun mk_proc lhs = |
|
76 |
(#sign (Thm.rep_cterm lhs), Logic.varify (term_of lhs), proc, stamp ()); |
|
77 |
in |
|
78 |
Simproc {name = name, procs = map mk_proc lhss} |
|
79 |
end; |
|
80 |
||
81 |
fun name_of_simproc (Simproc {name, ...}) = name; |
|
82 |
||
83 |
||
84 |
(* generic conversion prover *) (* FIXME move?, rename? *) |
|
85 |
||
86 |
fun conv_prover mk_eqv eqv_refl mk_meta_eq expand_tac norm_tac sg t u = |
|
87 |
let |
|
88 |
val X = Free (gensym "X.", fastype_of t); |
|
89 |
val goal = Logic.mk_implies (mk_eqv (X, t), mk_eqv (X, u)); |
|
90 |
val pre_result = |
|
91 |
prove_goalw_cterm [] (cterm_of sg goal) (*goal: X=t ==> X=u*) |
|
92 |
(fn prems => [ |
|
93 |
expand_tac, (*expand u*) |
|
94 |
ALLGOALS (cut_facts_tac prems), |
|
95 |
ALLGOALS norm_tac]); (*normalize both t and u*) |
|
96 |
in |
|
97 |
mk_meta_eq (eqv_refl RS pre_result) (*final result: t==u*) |
|
98 |
end |
|
99 |
handle ERROR => error ("The error(s) above occurred while trying to prove " ^ |
|
100 |
(string_of_cterm (cterm_of sg (mk_eqv (t, u))))); |
|
101 |
||
102 |
||
103 |
||
2503 | 104 |
(** simplification sets **) |
105 |
||
106 |
(* type simpset *) |
|
107 |
||
0 | 108 |
datatype simpset = |
2503 | 109 |
Simpset of { |
110 |
mss: meta_simpset, |
|
111 |
simps: thm list, |
|
2509 | 112 |
procs: simproc list, |
2503 | 113 |
congs: thm list, |
114 |
subgoal_tac: simpset -> int -> tactic, |
|
115 |
finish_tac: thm list -> int -> tactic, |
|
116 |
loop_tac: int -> tactic}; |
|
117 |
||
2509 | 118 |
fun make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac) = |
119 |
Simpset {mss = mss, simps = simps, procs = procs, congs = congs, |
|
2503 | 120 |
subgoal_tac = subgoal_tac, finish_tac = finish_tac, |
121 |
loop_tac = loop_tac}; |
|
0 | 122 |
|
123 |
val empty_ss = |
|
2509 | 124 |
make_ss (Thm.empty_mss, [], [], [], K (K no_tac), K (K no_tac), K no_tac); |
2503 | 125 |
|
2509 | 126 |
fun rep_ss (Simpset {simps, procs, congs, ...}) = |
127 |
{simps = simps, procs = map name_of_simproc procs, congs = congs}; |
|
2503 | 128 |
|
129 |
fun prems_of_ss (Simpset {mss, ...}) = Thm.prems_of_mss mss; |
|
130 |
||
131 |
||
132 |
(* extend simpsets *) |
|
133 |
||
2509 | 134 |
fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac = _}) |
2503 | 135 |
setloop loop_tac = |
2509 | 136 |
make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, DETERM o loop_tac); |
2503 | 137 |
|
2509 | 138 |
fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac = _, loop_tac}) |
2503 | 139 |
setsolver finish_tac = |
2509 | 140 |
make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac); |
2503 | 141 |
|
2509 | 142 |
fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, finish_tac}) |
2503 | 143 |
addsolver tac = |
2509 | 144 |
make_ss (mss, simps, procs, congs, subgoal_tac, |
2503 | 145 |
fn hyps => finish_tac hyps ORELSE' tac hyps, loop_tac); |
146 |
||
2509 | 147 |
fun (Simpset {mss, simps, procs, congs, subgoal_tac = _, finish_tac, loop_tac}) |
2503 | 148 |
setsubgoaler subgoal_tac = |
2509 | 149 |
make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac); |
2503 | 150 |
|
2509 | 151 |
fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) |
2503 | 152 |
setmksimps mk_simps = |
2509 | 153 |
make_ss (Thm.set_mk_rews (mss, mk_simps), simps, procs, congs, |
2503 | 154 |
subgoal_tac, finish_tac, loop_tac); |
155 |
||
2509 | 156 |
fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) |
157 |
settermless termless = |
|
158 |
make_ss (Thm.set_termless (mss, termless), simps, procs, congs, |
|
159 |
subgoal_tac, finish_tac, loop_tac); |
|
160 |
||
161 |
fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) |
|
2503 | 162 |
addsimps rews = |
163 |
let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in |
|
164 |
make_ss (Thm.add_simps (mss, rews'), rews' @ simps, |
|
2509 | 165 |
procs, congs, subgoal_tac, finish_tac, loop_tac) |
2503 | 166 |
end; |
167 |
||
2509 | 168 |
fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) |
2503 | 169 |
delsimps rews = |
170 |
let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in |
|
171 |
make_ss (Thm.del_simps (mss, rews'), |
|
172 |
foldl (gen_rem eq_thm) (simps, rews'), |
|
2509 | 173 |
procs, congs, subgoal_tac, finish_tac, loop_tac) |
2503 | 174 |
end; |
175 |
||
2509 | 176 |
fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) |
2503 | 177 |
addeqcongs newcongs = |
178 |
make_ss (Thm.add_congs (mss, newcongs), |
|
2509 | 179 |
simps, procs, newcongs @ congs, subgoal_tac, finish_tac, loop_tac); |
180 |
||
181 |
fun addsimproc ((Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}), |
|
182 |
simproc as Simproc {name = _, procs = procs'}) = |
|
183 |
make_ss (Thm.add_simprocs (mss, procs'), |
|
184 |
simps, gen_ins eq_simproc (simproc, procs), |
|
185 |
congs, subgoal_tac, finish_tac, loop_tac); |
|
186 |
||
187 |
val op addsimprocs = foldl addsimproc; |
|
188 |
||
189 |
fun delsimproc ((Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}), |
|
190 |
simproc as Simproc {name = _, procs = procs'}) = |
|
191 |
make_ss (Thm.del_simprocs (mss, procs'), |
|
192 |
simps, gen_rem eq_simproc (procs, simproc), |
|
193 |
congs, subgoal_tac, finish_tac, loop_tac); |
|
194 |
||
195 |
val op delsimprocs = foldl delsimproc; |
|
2503 | 196 |
|
197 |
||
198 |
(* merge simpsets *) |
|
199 |
||
2509 | 200 |
(*prefers first simpset (FIXME improve?)*) |
201 |
fun merge_ss (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}, |
|
202 |
Simpset {simps = simps2, procs = procs2, congs = congs2, ...}) = |
|
2503 | 203 |
let |
204 |
val simps' = gen_union eq_thm (simps, simps2); |
|
2509 | 205 |
val procs' = gen_union eq_simproc (procs, procs2); |
2503 | 206 |
val congs' = gen_union eq_thm (congs, congs2); |
207 |
val mss' = Thm.set_mk_rews (empty_mss, Thm.mk_rews_of_mss mss); |
|
208 |
val mss' = Thm.add_simps (mss', simps'); |
|
209 |
val mss' = Thm.add_congs (mss', congs'); |
|
210 |
in |
|
2509 | 211 |
make_ss (mss', simps', procs', congs', subgoal_tac, finish_tac, loop_tac) |
2503 | 212 |
end; |
213 |
||
214 |
||
215 |
(* the current simpset *) |
|
0 | 216 |
|
1243 | 217 |
val simpset = ref empty_ss; |
0 | 218 |
|
2503 | 219 |
fun Addsimps rews = (simpset := ! simpset addsimps rews); |
220 |
fun Delsimps rews = (simpset := ! simpset delsimps rews); |
|
0 | 221 |
|
2509 | 222 |
fun Addsimprocs procs = (simpset := ! simpset addsimprocs procs); |
223 |
fun Delsimprocs procs = (simpset := ! simpset delsimprocs procs); |
|
224 |
||
0 | 225 |
|
1243 | 226 |
|
2503 | 227 |
(** simplification tactics **) |
0 | 228 |
|
1 | 229 |
fun NEWSUBGOALS tac tacf = |
2503 | 230 |
STATE (fn state0 => |
231 |
tac THEN STATE (fn state1 => tacf (nprems_of state1 - nprems_of state0))); |
|
1 | 232 |
|
217
c972c57e7762
got rid of METAHYPS due to the change of the basic simplification routines
nipkow
parents:
146
diff
changeset
|
233 |
fun gen_simp_tac mode = |
2509 | 234 |
fn (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) => |
0 | 235 |
let fun solve_all_tac mss = |
2509 | 236 |
let val ss = |
237 |
make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac); |
|
1 | 238 |
val solve1_tac = |
239 |
NEWSUBGOALS (subgoal_tac ss 1) |
|
240 |
(fn n => if n<0 then all_tac else no_tac) |
|
241 |
in DEPTH_SOLVE(solve1_tac) end |
|
0 | 242 |
|
1512 | 243 |
fun simp_loop_tac i thm = |
2503 | 244 |
(asm_rewrite_goal_tac mode solve_all_tac mss i THEN |
245 |
(finish_tac (prems_of_mss mss) i ORELSE looper i)) thm |
|
1 | 246 |
and allsimp i n = EVERY(map (fn j => simp_loop_tac (i+j)) (n downto 0)) |
247 |
and looper i = TRY(NEWSUBGOALS (loop_tac i) (allsimp i)) |
|
217
c972c57e7762
got rid of METAHYPS due to the change of the basic simplification routines
nipkow
parents:
146
diff
changeset
|
248 |
in simp_loop_tac end; |
0 | 249 |
|
2503 | 250 |
val simp_tac = gen_simp_tac (false, false); |
251 |
val asm_simp_tac = gen_simp_tac (false, true); |
|
252 |
val full_simp_tac = gen_simp_tac (true, false); |
|
253 |
val asm_full_simp_tac = gen_simp_tac (true, true); |
|
0 | 254 |
|
2503 | 255 |
fun Simp_tac i = simp_tac (! simpset) i; |
256 |
fun Asm_simp_tac i = asm_simp_tac (! simpset) i; |
|
257 |
fun Full_simp_tac i = full_simp_tac (! simpset) i; |
|
258 |
fun Asm_full_simp_tac i = asm_full_simp_tac (! simpset) i; |
|
406 | 259 |
|
1243 | 260 |
end; |