author | nipkow |
Fri, 10 Sep 2004 00:19:15 +0200 | |
changeset 15195 | 197e00ce3f20 |
parent 15088 | b8a95eadbc14 |
child 15199 | 29ca1fe63e7b |
permissions | -rw-r--r-- |
10413 | 1 |
(* Title: Pure/meta_simplifier.ML |
2 |
ID: $Id$ |
|
11672 | 3 |
Author: Tobias Nipkow and Stefan Berghofer |
10413 | 4 |
|
11672 | 5 |
Meta-level Simplification. |
10413 | 6 |
*) |
7 |
||
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
8 |
infix 4 |
15023 | 9 |
addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs |
15195 | 10 |
setmksimps setmksimps2 setmkcong setmksym setmkeqTrue settermless setsubgoaler |
15023 | 11 |
setloop addloop delloop setSSolver addSSolver setSolver addSolver; |
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
12 |
|
11672 | 13 |
signature BASIC_META_SIMPLIFIER = |
14 |
sig |
|
15023 | 15 |
val debug_simp: bool ref |
11672 | 16 |
val trace_simp: bool ref |
13828 | 17 |
val simp_depth_limit: int ref |
15023 | 18 |
type rrule |
19 |
type cong |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
20 |
type solver |
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
21 |
val mk_solver: string -> (thm list -> int -> tactic) -> solver |
15023 | 22 |
type simpset |
23 |
type proc |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
24 |
val rep_ss: simpset -> |
15023 | 25 |
{rules: rrule Net.net, |
26 |
prems: thm list, |
|
27 |
bounds: string list, |
|
28 |
depth: int} * |
|
29 |
{congs: (string * cong) list * string list, |
|
30 |
procs: proc Net.net, |
|
31 |
mk_rews: |
|
32 |
{mk: thm -> thm list, |
|
15195 | 33 |
mk2: thm list -> thm -> thm list, |
15023 | 34 |
mk_cong: thm -> thm, |
35 |
mk_sym: thm -> thm option, |
|
36 |
mk_eq_True: thm -> thm option}, |
|
37 |
termless: term * term -> bool, |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
38 |
subgoal_tac: simpset -> int -> tactic, |
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
39 |
loop_tacs: (string * (int -> tactic)) list, |
15023 | 40 |
solvers: solver list * solver list} |
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
41 |
val print_ss: simpset -> unit |
15023 | 42 |
val empty_ss: simpset |
43 |
val merge_ss: simpset * simpset -> simpset |
|
44 |
type simproc |
|
45 |
val mk_simproc: string -> cterm list -> |
|
46 |
(Sign.sg -> simpset -> term -> thm option) -> simproc |
|
47 |
val add_prems: thm list -> simpset -> simpset |
|
48 |
val prems_of_ss: simpset -> thm list |
|
49 |
val addsimps: simpset * thm list -> simpset |
|
50 |
val delsimps: simpset * thm list -> simpset |
|
51 |
val addeqcongs: simpset * thm list -> simpset |
|
52 |
val deleqcongs: simpset * thm list -> simpset |
|
53 |
val addcongs: simpset * thm list -> simpset |
|
54 |
val delcongs: simpset * thm list -> simpset |
|
55 |
val addsimprocs: simpset * simproc list -> simpset |
|
56 |
val delsimprocs: simpset * simproc list -> simpset |
|
57 |
val setmksimps: simpset * (thm -> thm list) -> simpset |
|
15195 | 58 |
val setmksimps2: simpset * (thm list -> thm -> thm list) -> simpset |
15023 | 59 |
val setmkcong: simpset * (thm -> thm) -> simpset |
60 |
val setmksym: simpset * (thm -> thm option) -> simpset |
|
61 |
val setmkeqTrue: simpset * (thm -> thm option) -> simpset |
|
62 |
val settermless: simpset * (term * term -> bool) -> simpset |
|
63 |
val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset |
|
64 |
val setloop: simpset * (int -> tactic) -> simpset |
|
65 |
val addloop: simpset * (string * (int -> tactic)) -> simpset |
|
66 |
val delloop: simpset * string -> simpset |
|
67 |
val setSSolver: simpset * solver -> simpset |
|
68 |
val addSSolver: simpset * solver -> simpset |
|
69 |
val setSolver: simpset * solver -> simpset |
|
70 |
val addSolver: simpset * solver -> simpset |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
71 |
val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic |
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
72 |
end; |
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
73 |
|
10413 | 74 |
signature META_SIMPLIFIER = |
75 |
sig |
|
11672 | 76 |
include BASIC_META_SIMPLIFIER |
10413 | 77 |
exception SIMPLIFIER of string * thm |
15023 | 78 |
val clear_ss: simpset -> simpset |
79 |
exception SIMPROC_FAIL of string * exn |
|
80 |
val simproc_i: Sign.sg -> string -> term list |
|
81 |
-> (Sign.sg -> simpset -> term -> thm option) -> simproc |
|
82 |
val simproc: Sign.sg -> string -> string list |
|
83 |
-> (Sign.sg -> simpset -> term -> thm option) -> simproc |
|
11672 | 84 |
val rewrite_cterm: bool * bool * bool -> |
15023 | 85 |
(simpset -> thm -> thm option) -> simpset -> cterm -> thm |
86 |
val rewrite_aux: (simpset -> thm -> thm option) -> bool -> thm list -> cterm -> thm |
|
87 |
val simplify_aux: (simpset -> thm -> thm option) -> bool -> thm list -> thm -> thm |
|
13196 | 88 |
val rewrite_term: Sign.sg -> thm list -> (term -> term option) list -> term -> term |
15023 | 89 |
val rewrite_thm: bool * bool * bool -> |
90 |
(simpset -> thm -> thm option) -> simpset -> thm -> thm |
|
91 |
val rewrite_goals_rule_aux: (simpset -> thm -> thm option) -> thm list -> thm -> thm |
|
92 |
val rewrite_goal_rule: bool * bool * bool -> |
|
93 |
(simpset -> thm -> thm option) -> simpset -> int -> thm -> thm |
|
94 |
val asm_rewrite_goal_tac: bool * bool * bool -> |
|
95 |
(simpset -> tactic) -> simpset -> int -> tactic |
|
96 |
val simp_thm: bool * bool * bool -> simpset -> thm -> thm |
|
97 |
val simp_cterm: bool * bool * bool -> simpset -> cterm -> thm |
|
10413 | 98 |
end; |
99 |
||
15023 | 100 |
structure MetaSimplifier: META_SIMPLIFIER = |
10413 | 101 |
struct |
102 |
||
15023 | 103 |
|
10413 | 104 |
(** diagnostics **) |
105 |
||
106 |
exception SIMPLIFIER of string * thm; |
|
107 |
||
15023 | 108 |
val debug_simp = ref false; |
109 |
val trace_simp = ref false; |
|
11505
a410fa8acfca
Implemented indentation schema for conditional rewrite trace.
nipkow
parents:
11504
diff
changeset
|
110 |
val simp_depth = ref 0; |
13828 | 111 |
val simp_depth_limit = ref 1000; |
11505
a410fa8acfca
Implemented indentation schema for conditional rewrite trace.
nipkow
parents:
11504
diff
changeset
|
112 |
|
12603 | 113 |
local |
114 |
||
115 |
fun println a = |
|
15023 | 116 |
tracing (case ! simp_depth of 0 => a | n => enclose "[" "]" (string_of_int n) ^ a); |
11505
a410fa8acfca
Implemented indentation schema for conditional rewrite trace.
nipkow
parents:
11504
diff
changeset
|
117 |
|
a410fa8acfca
Implemented indentation schema for conditional rewrite trace.
nipkow
parents:
11504
diff
changeset
|
118 |
fun prnt warn a = if warn then warning a else println a; |
15023 | 119 |
fun prtm warn a sg t = prnt warn (a ^ "\n" ^ Sign.string_of_term sg t); |
12603 | 120 |
fun prctm warn a t = prnt warn (a ^ "\n" ^ Display.string_of_cterm t); |
10413 | 121 |
|
12603 | 122 |
in |
10413 | 123 |
|
15023 | 124 |
fun debug warn a = if ! debug_simp then prnt warn a else (); |
125 |
fun trace warn a = if ! trace_simp then prnt warn a else (); |
|
10413 | 126 |
|
15023 | 127 |
fun debug_term warn a sign t = if ! debug_simp then prtm warn a sign t else (); |
128 |
fun trace_term warn a sign t = if ! trace_simp then prtm warn a sign t else (); |
|
129 |
fun trace_cterm warn a ct = if ! trace_simp then prctm warn a ct else (); |
|
130 |
fun trace_thm a th = if ! trace_simp then prctm false a (Thm.cprop_of th) else (); |
|
13569 | 131 |
|
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
132 |
fun trace_named_thm a (thm, name) = |
15023 | 133 |
if ! trace_simp then |
134 |
prctm false (if name = "" then a else a ^ " " ^ quote name ^ ":") (Thm.cprop_of thm) |
|
135 |
else (); |
|
136 |
||
137 |
fun warn_thm a = prctm true a o Thm.cprop_of; |
|
10413 | 138 |
|
12603 | 139 |
end; |
10413 | 140 |
|
141 |
||
142 |
||
15023 | 143 |
(** datatype simpset **) |
144 |
||
145 |
(* rewrite rules *) |
|
10413 | 146 |
|
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
147 |
type rrule = {thm: thm, name: string, lhs: term, elhs: cterm, fo: bool, perm: bool}; |
15023 | 148 |
|
149 |
(*thm: the rewrite rule; |
|
150 |
name: name of theorem from which rewrite rule was extracted; |
|
151 |
lhs: the left-hand side; |
|
152 |
elhs: the etac-contracted lhs; |
|
153 |
fo: use first-order matching; |
|
154 |
perm: the rewrite rule is permutative; |
|
155 |
||
12603 | 156 |
Remarks: |
10413 | 157 |
- elhs is used for matching, |
15023 | 158 |
lhs only for preservation of bound variable names; |
10413 | 159 |
- fo is set iff |
160 |
either elhs is first-order (no Var is applied), |
|
15023 | 161 |
in which case fo-matching is complete, |
10413 | 162 |
or elhs is not a pattern, |
15023 | 163 |
in which case there is nothing better to do;*) |
10413 | 164 |
|
165 |
fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) = |
|
15023 | 166 |
Drule.eq_thm_prop (thm1, thm2); |
167 |
||
168 |
||
169 |
(* congruences *) |
|
170 |
||
171 |
type cong = {thm: thm, lhs: cterm}; |
|
10413 | 172 |
|
12603 | 173 |
fun eq_cong ({thm = thm1, ...}: cong, {thm = thm2, ...}: cong) = |
15023 | 174 |
Drule.eq_thm_prop (thm1, thm2); |
10413 | 175 |
|
176 |
||
15023 | 177 |
(* solvers *) |
178 |
||
179 |
datatype solver = |
|
180 |
Solver of |
|
181 |
{name: string, |
|
182 |
solver: thm list -> int -> tactic, |
|
183 |
id: stamp}; |
|
184 |
||
185 |
fun mk_solver name solver = Solver {name = name, solver = solver, id = stamp ()}; |
|
186 |
||
15034 | 187 |
fun solver_name (Solver {name, ...}) = name; |
15023 | 188 |
fun solver ths (Solver {solver = tacf, ...}) = tacf ths; |
189 |
fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2); |
|
190 |
val merge_solvers = gen_merge_lists eq_solver; |
|
191 |
||
192 |
||
193 |
(* simplification sets and procedures *) |
|
194 |
||
195 |
(*A simpset contains data required during conversion: |
|
10413 | 196 |
rules: discrimination net of rewrite rules; |
15023 | 197 |
prems: current premises; |
198 |
bounds: names of bound variables already used |
|
199 |
(for generating new names when rewriting under lambda abstractions); |
|
200 |
depth: depth of conditional rewriting; |
|
10413 | 201 |
congs: association list of congruence rules and |
202 |
a list of `weak' congruence constants. |
|
203 |
A congruence is `weak' if it avoids normalization of some argument. |
|
204 |
procs: discrimination net of simplification procedures |
|
205 |
(functions that prove rewrite rules on the fly); |
|
15023 | 206 |
mk_rews: |
207 |
mk: turn simplification thms into rewrite rules; |
|
15195 | 208 |
mk2: like mk but may also depend on the other premises |
15023 | 209 |
mk_cong: prepare congruence rules; |
210 |
mk_sym: turn == around; |
|
211 |
mk_eq_True: turn P into P == True; |
|
212 |
termless: relation for ordered rewriting;*) |
|
15011 | 213 |
|
15023 | 214 |
type mk_rews = |
215 |
{mk: thm -> thm list, |
|
15195 | 216 |
mk2: thm list -> thm -> thm list, |
15023 | 217 |
mk_cong: thm -> thm, |
218 |
mk_sym: thm -> thm option, |
|
219 |
mk_eq_True: thm -> thm option}; |
|
220 |
||
221 |
datatype simpset = |
|
222 |
Simpset of |
|
223 |
{rules: rrule Net.net, |
|
10413 | 224 |
prems: thm list, |
15023 | 225 |
bounds: string list, |
226 |
depth: int} * |
|
227 |
{congs: (string * cong) list * string list, |
|
228 |
procs: proc Net.net, |
|
229 |
mk_rews: mk_rews, |
|
11504 | 230 |
termless: term * term -> bool, |
15011 | 231 |
subgoal_tac: simpset -> int -> tactic, |
232 |
loop_tacs: (string * (int -> tactic)) list, |
|
15023 | 233 |
solvers: solver list * solver list} |
234 |
and proc = |
|
235 |
Proc of |
|
236 |
{name: string, |
|
237 |
lhs: cterm, |
|
238 |
proc: Sign.sg -> simpset -> term -> thm option, |
|
239 |
id: stamp}; |
|
240 |
||
241 |
fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = (id1 = id2); |
|
242 |
||
243 |
fun rep_ss (Simpset args) = args; |
|
10413 | 244 |
|
15023 | 245 |
fun make_ss1 (rules, prems, bounds, depth) = |
246 |
{rules = rules, prems = prems, bounds = bounds, depth = depth}; |
|
247 |
||
248 |
fun map_ss1 f {rules, prems, bounds, depth} = |
|
249 |
make_ss1 (f (rules, prems, bounds, depth)); |
|
10413 | 250 |
|
15023 | 251 |
fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) = |
252 |
{congs = congs, procs = procs, mk_rews = mk_rews, termless = termless, |
|
253 |
subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers}; |
|
254 |
||
255 |
fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} = |
|
256 |
make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); |
|
257 |
||
258 |
fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2); |
|
10413 | 259 |
|
15023 | 260 |
fun map_simpset f (Simpset ({rules, prems, bounds, depth}, |
261 |
{congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers})) = |
|
262 |
make_simpset (f ((rules, prems, bounds, depth), |
|
263 |
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers))); |
|
10413 | 264 |
|
15023 | 265 |
fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2); |
266 |
fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2); |
|
267 |
||
268 |
||
269 |
(* print simpsets *) |
|
10413 | 270 |
|
15023 | 271 |
fun print_ss ss = |
272 |
let |
|
15034 | 273 |
val pretty_thms = map Display.pretty_thm; |
15023 | 274 |
|
15034 | 275 |
fun pretty_cong (name, th) = |
276 |
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, Display.pretty_thm th]; |
|
15023 | 277 |
fun pretty_proc (name, lhss) = |
278 |
Pretty.big_list (name ^ ":") (map Display.pretty_cterm lhss); |
|
15034 | 279 |
|
280 |
val Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...}) = ss; |
|
281 |
val smps = map (#thm o #2) (Net.dest rules); |
|
282 |
val cngs = map (fn (name, {thm, ...}) => (name, thm)) (#1 congs); |
|
283 |
val prcs = Net.dest procs |> |
|
284 |
map (fn (_, Proc {name, lhs, id, ...}) => ((name, lhs), id)) |
|
285 |
|> partition_eq eq_snd |
|
286 |
|> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps)) |
|
287 |
|> Library.sort_wrt #1; |
|
15023 | 288 |
in |
15034 | 289 |
[Pretty.big_list "simplification rules:" (pretty_thms smps), |
290 |
Pretty.big_list "simplification procedures:" (map pretty_proc prcs), |
|
291 |
Pretty.big_list "congruences:" (map pretty_cong cngs), |
|
15088 | 292 |
Pretty.strs ("loopers:" :: map (quote o #1) loop_tacs), |
293 |
Pretty.strs ("unsafe solvers:" :: map (quote o solver_name) (#1 solvers)), |
|
294 |
Pretty.strs ("safe solvers:" :: map (quote o solver_name) (#2 solvers))] |
|
15023 | 295 |
|> Pretty.chunks |> Pretty.writeln |
13828 | 296 |
end; |
10413 | 297 |
|
15023 | 298 |
|
299 |
(* empty simpsets *) |
|
300 |
||
301 |
local |
|
302 |
||
303 |
fun init_ss mk_rews termless subgoal_tac solvers = |
|
304 |
make_simpset ((Net.empty, [], [], 0), |
|
305 |
(([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers)); |
|
306 |
||
307 |
val basic_mk_rews: mk_rews = |
|
308 |
{mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [], |
|
15195 | 309 |
mk2 = fn thms => fn thm => [], |
15023 | 310 |
mk_cong = I, |
311 |
mk_sym = Some o Drule.symmetric_fun, |
|
312 |
mk_eq_True = K None}; |
|
313 |
||
314 |
in |
|
315 |
||
316 |
val empty_ss = init_ss basic_mk_rews Term.termless (K (K no_tac)) ([], []); |
|
317 |
||
318 |
fun clear_ss (Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) = |
|
319 |
init_ss mk_rews termless subgoal_tac solvers; |
|
320 |
||
321 |
end; |
|
322 |
||
323 |
||
324 |
(* merge simpsets *) (*NOTE: ignores some fields of 2nd simpset*) |
|
15011 | 325 |
|
15023 | 326 |
fun merge_ss (ss1, ss2) = |
327 |
let |
|
328 |
val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth}, |
|
329 |
{congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac, |
|
330 |
loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1; |
|
331 |
val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = _}, |
|
332 |
{congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _, |
|
333 |
loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2; |
|
15011 | 334 |
|
15023 | 335 |
val rules' = Net.merge (rules1, rules2, eq_rrule); |
336 |
val prems' = gen_merge_lists Drule.eq_thm_prop prems1 prems2; |
|
337 |
val bounds' = merge_lists bounds1 bounds2; |
|
338 |
val congs' = gen_merge_lists (eq_cong o pairself #2) congs1 congs2; |
|
339 |
val weak' = merge_lists weak1 weak2; |
|
340 |
val procs' = Net.merge (procs1, procs2, eq_proc); |
|
341 |
val loop_tacs' = merge_alists loop_tacs1 loop_tacs2; |
|
342 |
val unsafe_solvers' = merge_solvers unsafe_solvers1 unsafe_solvers2; |
|
343 |
val solvers' = merge_solvers solvers1 solvers2; |
|
344 |
in |
|
345 |
make_simpset ((rules', prems', bounds', depth), ((congs', weak'), procs', |
|
346 |
mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers'))) |
|
347 |
end; |
|
348 |
||
349 |
||
350 |
(* simprocs *) |
|
351 |
||
352 |
exception SIMPROC_FAIL of string * exn; |
|
353 |
||
354 |
datatype simproc = Simproc of proc list; |
|
355 |
||
356 |
fun mk_simproc name lhss proc = |
|
357 |
let val id = stamp () in |
|
358 |
Simproc (lhss |> map (fn lhs => |
|
359 |
Proc {name = name, lhs = lhs, proc = proc, id = id})) |
|
360 |
end; |
|
361 |
||
362 |
fun simproc_i sg name = mk_simproc name o map (Thm.cterm_of sg o Logic.varify); |
|
363 |
fun simproc sg name = simproc_i sg name o map (Sign.simple_read_term sg TypeInfer.logicT); |
|
364 |
||
15011 | 365 |
|
10413 | 366 |
|
367 |
(** simpset operations **) |
|
368 |
||
15023 | 369 |
(* bounds and prems *) |
10413 | 370 |
|
15023 | 371 |
fun add_bound b = map_simpset1 (fn (rules, prems, bounds, depth) => |
372 |
(rules, prems, b :: bounds, depth)); |
|
10413 | 373 |
|
15023 | 374 |
fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth) => |
375 |
(rules, ths @ prems, bounds, depth)); |
|
376 |
||
377 |
fun prems_of_ss (Simpset ({prems, ...}, _)) = prems; |
|
10413 | 378 |
|
379 |
||
15023 | 380 |
(* addsimps *) |
10413 | 381 |
|
15023 | 382 |
fun mk_rrule2 {thm, name, lhs, elhs, perm} = |
383 |
let |
|
384 |
val fo = Pattern.first_order (term_of elhs) orelse not (Pattern.pattern (term_of elhs)) |
|
385 |
in {thm = thm, name = name, lhs = lhs, elhs = elhs, fo = fo, perm = perm} end; |
|
10413 | 386 |
|
15023 | 387 |
fun insert_rrule quiet (ss, rrule as {thm, name, lhs, elhs, perm}) = |
388 |
(trace_named_thm "Adding rewrite rule" (thm, name); |
|
389 |
ss |> map_simpset1 (fn (rules, prems, bounds, depth) => |
|
390 |
let |
|
391 |
val rrule2 as {elhs, ...} = mk_rrule2 rrule; |
|
392 |
val rules' = Net.insert_term ((term_of elhs, rrule2), rules, eq_rrule); |
|
393 |
in (rules', prems, bounds, depth) end) |
|
394 |
handle Net.INSERT => |
|
395 |
(if quiet then () else warn_thm "Ignoring duplicate rewrite rule:" thm; ss)); |
|
10413 | 396 |
|
397 |
fun vperm (Var _, Var _) = true |
|
398 |
| vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t) |
|
399 |
| vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2) |
|
400 |
| vperm (t, u) = (t = u); |
|
401 |
||
402 |
fun var_perm (t, u) = |
|
403 |
vperm (t, u) andalso eq_set (term_varnames t, term_varnames u); |
|
404 |
||
405 |
(* FIXME: it seems that the conditions on extra variables are too liberal if |
|
406 |
prems are nonempty: does solving the prems really guarantee instantiation of |
|
407 |
all its Vars? Better: a dynamic check each time a rule is applied. |
|
408 |
*) |
|
409 |
fun rewrite_rule_extra_vars prems elhs erhs = |
|
410 |
not (term_varnames erhs subset foldl add_term_varnames (term_varnames elhs, prems)) |
|
411 |
orelse |
|
15023 | 412 |
not (term_tvars erhs subset (term_tvars elhs union List.concat (map term_tvars prems))); |
10413 | 413 |
|
15023 | 414 |
(*simple test for looping rewrite rules and stupid orientations*) |
10413 | 415 |
fun reorient sign prems lhs rhs = |
15023 | 416 |
rewrite_rule_extra_vars prems lhs rhs |
417 |
orelse |
|
418 |
is_Var (head_of lhs) |
|
419 |
orelse |
|
420 |
exists (apl (lhs, Logic.occs)) (rhs :: prems) |
|
421 |
orelse |
|
422 |
null prems andalso Pattern.matches (Sign.tsig_of sign) (lhs, rhs) |
|
10413 | 423 |
(*the condition "null prems" is necessary because conditional rewrites |
424 |
with extra variables in the conditions may terminate although |
|
15023 | 425 |
the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*) |
426 |
orelse |
|
427 |
is_Const lhs andalso not (is_Const rhs); |
|
10413 | 428 |
|
429 |
fun decomp_simp thm = |
|
15023 | 430 |
let |
431 |
val {sign, prop, ...} = Thm.rep_thm thm; |
|
432 |
val prems = Logic.strip_imp_prems prop; |
|
433 |
val concl = Drule.strip_imp_concl (Thm.cprop_of thm); |
|
434 |
val (lhs, rhs) = Drule.dest_equals concl handle TERM _ => |
|
435 |
raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm); |
|
436 |
val (_, elhs) = Drule.dest_equals (Thm.cprop_of (Thm.eta_conversion lhs)); |
|
437 |
val elhs = if elhs = lhs then lhs else elhs; (*share identical copies*) |
|
438 |
val erhs = Pattern.eta_contract (term_of rhs); |
|
439 |
val perm = |
|
440 |
var_perm (term_of elhs, erhs) andalso |
|
441 |
not (term_of elhs aconv erhs) andalso |
|
442 |
not (is_Var (term_of elhs)); |
|
10413 | 443 |
in (sign, prems, term_of lhs, elhs, term_of rhs, perm) end; |
444 |
||
12783 | 445 |
fun decomp_simp' thm = |
12979
4c76bce4ce39
decomp_simp': use lhs instead of elhs (preserves more bound variable names);
wenzelm
parents:
12783
diff
changeset
|
446 |
let val (_, _, lhs, _, rhs, _) = decomp_simp thm in |
12783 | 447 |
if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm) |
12979
4c76bce4ce39
decomp_simp': use lhs instead of elhs (preserves more bound variable names);
wenzelm
parents:
12783
diff
changeset
|
448 |
else (lhs, rhs) |
12783 | 449 |
end; |
450 |
||
15023 | 451 |
fun mk_eq_True (Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) = |
452 |
(case mk_eq_True thm of |
|
10413 | 453 |
None => [] |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
454 |
| Some eq_True => |
15023 | 455 |
let val (_, _, lhs, elhs, _, _) = decomp_simp eq_True |
456 |
in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end); |
|
10413 | 457 |
|
15023 | 458 |
(*create the rewrite rule and possibly also the eq_True variant, |
459 |
in case there are extra vars on the rhs*) |
|
460 |
fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) = |
|
461 |
let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in |
|
462 |
if term_varnames rhs subset term_varnames lhs andalso |
|
463 |
term_tvars rhs subset term_tvars lhs then [rrule] |
|
464 |
else mk_eq_True ss (thm2, name) @ [rrule] |
|
10413 | 465 |
end; |
466 |
||
15023 | 467 |
fun mk_rrule ss (thm, name) = |
468 |
let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in |
|
469 |
if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}] |
|
470 |
else |
|
471 |
(*weak test for loops*) |
|
472 |
if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs) |
|
473 |
then mk_eq_True ss (thm, name) |
|
474 |
else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm) |
|
10413 | 475 |
end; |
476 |
||
15023 | 477 |
fun orient_rrule ss (thm, name) = |
478 |
let val (sign, prems, lhs, elhs, rhs, perm) = decomp_simp thm in |
|
479 |
if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}] |
|
480 |
else if reorient sign prems lhs rhs then |
|
481 |
if reorient sign prems rhs lhs |
|
482 |
then mk_eq_True ss (thm, name) |
|
483 |
else |
|
484 |
let val Simpset (_, {mk_rews = {mk_sym, ...}, ...}) = ss in |
|
485 |
(case mk_sym thm of |
|
486 |
None => [] |
|
487 |
| Some thm' => |
|
488 |
let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm' |
|
489 |
in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end) |
|
490 |
end |
|
491 |
else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm) |
|
10413 | 492 |
end; |
493 |
||
15195 | 494 |
fun extract_rews (Simpset ({prems, ...}, {mk_rews = {mk, ...}, ...}), thms) |
495 |
= flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms); |
|
496 |
||
497 |
fun extract_rews2 (Simpset ({prems, ...}, {mk_rews = {mk2, ...}, ...}), thms) |
|
498 |
= flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk2 prems thm)) thms); |
|
10413 | 499 |
|
15023 | 500 |
fun orient_comb_simps comb mk_rrule (ss, thms) = |
501 |
let |
|
502 |
val rews = extract_rews (ss, thms); |
|
503 |
val rrules = flat (map mk_rrule rews); |
|
504 |
in foldl comb (ss, rrules) end; |
|
10413 | 505 |
|
15023 | 506 |
fun extract_safe_rrules (ss, thm) = |
507 |
flat (map (orient_rrule ss) (extract_rews (ss, [thm]))); |
|
10413 | 508 |
|
15195 | 509 |
fun extract_safe_rrules2 (ss, thm) = |
510 |
flat (map (orient_rrule ss) (extract_rews2 (ss, [thm]))); |
|
511 |
||
15023 | 512 |
(*add rewrite rules explicitly; do not reorient!*) |
513 |
fun ss addsimps thms = |
|
514 |
orient_comb_simps (insert_rrule false) (mk_rrule ss) (ss, thms); |
|
10413 | 515 |
|
516 |
||
15195 | 517 |
fun add_prem2(ss,thm) = |
518 |
foldl (insert_rrule true) (ss,extract_safe_rrules2(ss,thm)) |
|
519 |
|> add_prems [thm]; |
|
520 |
||
521 |
fun add_prems2 thms ss = foldl add_prem2 (ss,thms); |
|
522 |
||
15023 | 523 |
(* delsimps *) |
10413 | 524 |
|
15023 | 525 |
fun del_rrule (ss, rrule as {thm, elhs, ...}) = |
526 |
ss |> map_simpset1 (fn (rules, prems, bounds, depth) => |
|
527 |
(Net.delete_term ((term_of elhs, rrule), rules, eq_rrule), prems, bounds, depth)) |
|
528 |
handle Net.DELETE => (warn_thm "Rewrite rule not in simpset:" thm; ss); |
|
10413 | 529 |
|
15023 | 530 |
fun ss delsimps thms = |
531 |
orient_comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms); |
|
532 |
||
533 |
||
534 |
(* congs *) |
|
10413 | 535 |
|
13835
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
13828
diff
changeset
|
536 |
fun cong_name (Const (a, _)) = Some a |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
13828
diff
changeset
|
537 |
| cong_name (Free (a, _)) = Some ("Free: " ^ a) |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
13828
diff
changeset
|
538 |
| cong_name _ = None; |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
13828
diff
changeset
|
539 |
|
15023 | 540 |
local |
541 |
||
542 |
fun is_full_cong_prems [] [] = true |
|
543 |
| is_full_cong_prems [] _ = false |
|
544 |
| is_full_cong_prems (p :: prems) varpairs = |
|
545 |
(case Logic.strip_assums_concl p of |
|
546 |
Const ("==", _) $ lhs $ rhs => |
|
547 |
let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in |
|
548 |
is_Var x andalso forall is_Bound xs andalso |
|
549 |
null (findrep xs) andalso xs = ys andalso |
|
550 |
(x, y) mem varpairs andalso |
|
551 |
is_full_cong_prems prems (varpairs \ (x, y)) |
|
552 |
end |
|
553 |
| _ => false); |
|
554 |
||
555 |
fun is_full_cong thm = |
|
10413 | 556 |
let |
15023 | 557 |
val prems = prems_of thm and concl = concl_of thm; |
558 |
val (lhs, rhs) = Logic.dest_equals concl; |
|
559 |
val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs; |
|
10413 | 560 |
in |
15023 | 561 |
f = g andalso null (findrep (xs @ ys)) andalso length xs = length ys andalso |
562 |
is_full_cong_prems prems (xs ~~ ys) |
|
10413 | 563 |
end; |
564 |
||
15023 | 565 |
fun add_cong (ss, thm) = ss |> |
566 |
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
|
567 |
let |
|
568 |
val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm)) |
|
569 |
handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm); |
|
570 |
(*val lhs = Pattern.eta_contract lhs;*) |
|
571 |
val a = the (cong_name (head_of (term_of lhs))) handle Library.OPTION => |
|
572 |
raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm); |
|
573 |
val (alist, weak) = congs; |
|
574 |
val alist2 = overwrite_warn (alist, (a, {lhs = lhs, thm = thm})) |
|
575 |
("Overwriting congruence rule for " ^ quote a); |
|
576 |
val weak2 = if is_full_cong thm then weak else a :: weak; |
|
577 |
in ((alist2, weak2), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); |
|
10413 | 578 |
|
15023 | 579 |
fun del_cong (ss, thm) = ss |> |
580 |
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
|
581 |
let |
|
582 |
val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ => |
|
583 |
raise SIMPLIFIER ("Congruence not a meta-equality", thm); |
|
584 |
(*val lhs = Pattern.eta_contract lhs;*) |
|
585 |
val a = the (cong_name (head_of lhs)) handle Library.OPTION => |
|
586 |
raise SIMPLIFIER ("Congruence must start with a constant", thm); |
|
587 |
val (alist, _) = congs; |
|
588 |
val alist2 = filter (fn (x, _) => x <> a) alist; |
|
589 |
val weak2 = alist2 |> mapfilter (fn (a, {thm, ...}) => |
|
590 |
if is_full_cong thm then None else Some a); |
|
591 |
in ((alist2, weak2), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); |
|
10413 | 592 |
|
15023 | 593 |
fun mk_cong (Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f; |
594 |
||
595 |
in |
|
596 |
||
597 |
val (op addeqcongs) = foldl add_cong; |
|
598 |
val (op deleqcongs) = foldl del_cong; |
|
599 |
||
600 |
fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs; |
|
601 |
fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs; |
|
602 |
||
603 |
end; |
|
10413 | 604 |
|
605 |
||
15023 | 606 |
(* simprocs *) |
607 |
||
608 |
local |
|
10413 | 609 |
|
15023 | 610 |
fun add_proc (ss, proc as Proc {name, lhs, ...}) = |
611 |
(trace_cterm false ("Adding simplification procedure " ^ quote name ^ " for") lhs; |
|
612 |
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
|
613 |
(congs, Net.insert_term ((term_of lhs, proc), procs, eq_proc), |
|
614 |
mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss |
|
615 |
handle Net.INSERT => |
|
616 |
(warning ("Ignoring duplicate simplification procedure " ^ quote name); ss)); |
|
10413 | 617 |
|
15023 | 618 |
fun del_proc (ss, proc as Proc {name, lhs, ...}) = |
619 |
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
|
620 |
(congs, Net.delete_term ((term_of lhs, proc), procs, eq_proc), |
|
621 |
mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss |
|
622 |
handle Net.DELETE => |
|
623 |
(warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ss); |
|
10413 | 624 |
|
15023 | 625 |
in |
10413 | 626 |
|
15023 | 627 |
val (op addsimprocs) = foldl (fn (ss, Simproc procs) => foldl add_proc (ss, procs)); |
628 |
val (op delsimprocs) = foldl (fn (ss, Simproc procs) => foldl del_proc (ss, procs)); |
|
10413 | 629 |
|
15023 | 630 |
end; |
10413 | 631 |
|
632 |
||
633 |
(* mk_rews *) |
|
634 |
||
15023 | 635 |
local |
636 |
||
15195 | 637 |
fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk2, mk_cong, mk_sym, mk_eq_True}, |
15023 | 638 |
termless, subgoal_tac, loop_tacs, solvers) => |
15195 | 639 |
let val (mk', mk2', mk_cong', mk_sym', mk_eq_True') = f (mk, mk2, mk_cong, mk_sym, mk_eq_True) in |
640 |
(congs, procs, {mk = mk', mk2 = mk2', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True'}, |
|
15023 | 641 |
termless, subgoal_tac, loop_tacs, solvers) |
642 |
end); |
|
643 |
||
644 |
in |
|
10413 | 645 |
|
15195 | 646 |
fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk2, mk_cong, mk_sym, mk_eq_True) => |
647 |
(mk, mk2, mk_cong, mk_sym, mk_eq_True)); |
|
15023 | 648 |
|
15195 | 649 |
fun ss setmksimps2 mk2 = ss |> map_mk_rews (fn (mk, _, mk_cong, mk_sym, mk_eq_True) => |
650 |
(mk, mk2, mk_cong, mk_sym, mk_eq_True)); |
|
10413 | 651 |
|
15195 | 652 |
fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, mk2, _, mk_sym, mk_eq_True) => |
653 |
(mk, mk2, mk_cong, mk_sym, mk_eq_True)); |
|
10413 | 654 |
|
15195 | 655 |
fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk2, mk_cong, _, mk_eq_True) => |
656 |
(mk, mk2, mk_cong, mk_sym, mk_eq_True)); |
|
657 |
||
658 |
fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk2, mk_cong, mk_sym, _) => |
|
659 |
(mk, mk2, mk_cong, mk_sym, mk_eq_True)); |
|
15023 | 660 |
|
661 |
end; |
|
662 |
||
14242
ec70653a02bf
Added access to the mk_rews field (and friends).
skalberg
parents:
14040
diff
changeset
|
663 |
|
10413 | 664 |
(* termless *) |
665 |
||
15023 | 666 |
fun ss settermless termless = ss |> |
667 |
map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) => |
|
668 |
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
669 |
|
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
670 |
|
15023 | 671 |
(* tactics *) |
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
672 |
|
15023 | 673 |
fun ss setsubgoaler subgoal_tac = ss |> |
674 |
map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) => |
|
675 |
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers)); |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
676 |
|
15023 | 677 |
fun ss setloop tac = ss |> |
678 |
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) => |
|
679 |
(congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers)); |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
680 |
|
15023 | 681 |
fun ss addloop (name, tac) = ss |> |
682 |
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
|
683 |
(congs, procs, mk_rews, termless, subgoal_tac, |
|
684 |
overwrite_warn (loop_tacs, (name, tac)) ("Overwriting looper " ^ quote name), |
|
685 |
solvers)); |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
686 |
|
15023 | 687 |
fun ss delloop name = ss |> |
688 |
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) => |
|
15034 | 689 |
let val loop_tacs' = filter_out (equal name o #1) loop_tacs in |
690 |
if length loop_tacs <> length loop_tacs' then () |
|
691 |
else warning ("No such looper in simpset: " ^ quote name); |
|
692 |
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs', solvers) |
|
15023 | 693 |
end); |
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
694 |
|
15023 | 695 |
fun ss setSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, |
696 |
subgoal_tac, loop_tacs, (unsafe_solvers, _)) => |
|
697 |
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver]))); |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
698 |
|
15023 | 699 |
fun ss addSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, |
700 |
subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless, |
|
701 |
subgoal_tac, loop_tacs, (unsafe_solvers, merge_solvers solvers [solver]))); |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
702 |
|
15023 | 703 |
fun ss setSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, |
704 |
subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless, |
|
705 |
subgoal_tac, loop_tacs, ([solver], solvers))); |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
706 |
|
15023 | 707 |
fun ss addSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless, |
708 |
subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless, |
|
709 |
subgoal_tac, loop_tacs, (merge_solvers unsafe_solvers [solver], solvers))); |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
710 |
|
15023 | 711 |
fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless, |
712 |
subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless, |
|
713 |
subgoal_tac, loop_tacs, (solvers, solvers))); |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
714 |
|
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
715 |
|
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
716 |
|
10413 | 717 |
(** rewriting **) |
718 |
||
719 |
(* |
|
720 |
Uses conversions, see: |
|
721 |
L C Paulson, A higher-order implementation of rewriting, |
|
722 |
Science of Computer Programming 3 (1983), pages 119-149. |
|
723 |
*) |
|
724 |
||
15023 | 725 |
val dest_eq = Drule.dest_equals o Thm.cprop_of; |
726 |
val lhs_of = #1 o dest_eq; |
|
727 |
val rhs_of = #2 o dest_eq; |
|
10413 | 728 |
|
729 |
fun check_conv msg thm thm' = |
|
730 |
let |
|
731 |
val thm'' = transitive thm (transitive |
|
15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14981
diff
changeset
|
732 |
(symmetric (Drule.beta_eta_conversion (lhs_of thm'))) thm') |
15023 | 733 |
in if msg then trace_thm "SUCCEEDED" thm' else (); Some thm'' end |
10413 | 734 |
handle THM _ => |
15023 | 735 |
let val {sign, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in |
736 |
trace_thm "Proved wrong thm (Check subgoaler?)" thm'; |
|
737 |
trace_term false "Should have proved:" sign prop0; |
|
738 |
None |
|
10413 | 739 |
end; |
740 |
||
741 |
||
742 |
(* mk_procrule *) |
|
743 |
||
744 |
fun mk_procrule thm = |
|
15023 | 745 |
let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in |
746 |
if rewrite_rule_extra_vars prems lhs rhs |
|
747 |
then (warn_thm "Extra vars on rhs:" thm; []) |
|
748 |
else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}] |
|
10413 | 749 |
end; |
750 |
||
751 |
||
15023 | 752 |
(* rewritec: conversion to apply the meta simpset to a term *) |
10413 | 753 |
|
15023 | 754 |
(*Since the rewriting strategy is bottom-up, we avoid re-normalizing already |
755 |
normalized terms by carrying around the rhs of the rewrite rule just |
|
756 |
applied. This is called the `skeleton'. It is decomposed in parallel |
|
757 |
with the term. Once a Var is encountered, the corresponding term is |
|
758 |
already in normal form. |
|
759 |
skel0 is a dummy skeleton that is to enforce complete normalization.*) |
|
760 |
||
10413 | 761 |
val skel0 = Bound 0; |
762 |
||
15023 | 763 |
(*Use rhs as skeleton only if the lhs does not contain unnormalized bits. |
764 |
The latter may happen iff there are weak congruence rules for constants |
|
765 |
in the lhs.*) |
|
10413 | 766 |
|
15023 | 767 |
fun uncond_skel ((_, weak), (lhs, rhs)) = |
768 |
if null weak then rhs (*optimization*) |
|
769 |
else if exists_Const (fn (c, _) => c mem weak) lhs then skel0 |
|
770 |
else rhs; |
|
771 |
||
772 |
(*Behaves like unconditional rule if rhs does not contain vars not in the lhs. |
|
773 |
Otherwise those vars may become instantiated with unnormalized terms |
|
774 |
while the premises are solved.*) |
|
775 |
||
776 |
fun cond_skel (args as (congs, (lhs, rhs))) = |
|
777 |
if term_varnames rhs subset term_varnames lhs then uncond_skel args |
|
10413 | 778 |
else skel0; |
779 |
||
15023 | 780 |
fun incr_depth ss = |
781 |
let |
|
782 |
val ss' = ss |> map_simpset1 (fn (rules, prems, bounds, depth) => |
|
783 |
(rules, prems, bounds, depth + 1)); |
|
784 |
val Simpset ({depth = depth', ...}, _) = ss'; |
|
785 |
in |
|
786 |
if depth' > ! simp_depth_limit |
|
787 |
then (warning "simp_depth_limit exceeded - giving up"; None) |
|
788 |
else |
|
789 |
(if depth' mod 10 = 0 |
|
790 |
then warning ("Simplification depth " ^ string_of_int depth') |
|
791 |
else (); |
|
792 |
Some ss') |
|
793 |
end; |
|
794 |
||
10413 | 795 |
(* |
15023 | 796 |
Rewriting -- we try in order: |
10413 | 797 |
(1) beta reduction |
798 |
(2) unconditional rewrite rules |
|
799 |
(3) conditional rewrite rules |
|
800 |
(4) simplification procedures |
|
801 |
||
802 |
IMPORTANT: rewrite rules must not introduce new Vars or TVars! |
|
803 |
*) |
|
804 |
||
15023 | 805 |
fun rewritec (prover, signt, maxt) ss t = |
10413 | 806 |
let |
15023 | 807 |
val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss; |
10413 | 808 |
val eta_thm = Thm.eta_conversion t; |
809 |
val eta_t' = rhs_of eta_thm; |
|
810 |
val eta_t = term_of eta_t'; |
|
811 |
val tsigt = Sign.tsig_of signt; |
|
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
812 |
fun rew {thm, name, lhs, elhs, fo, perm} = |
10413 | 813 |
let |
814 |
val {sign, prop, maxidx, ...} = rep_thm thm; |
|
815 |
val _ = if Sign.subsig (sign, signt) then () |
|
15023 | 816 |
else (warn_thm "Ignoring rewrite rule from different theory:" thm; |
10413 | 817 |
raise Pattern.MATCH); |
818 |
val (rthm, elhs') = if maxt = ~1 then (thm, elhs) |
|
819 |
else (Thm.incr_indexes (maxt+1) thm, Thm.cterm_incr_indexes (maxt+1) elhs); |
|
820 |
val insts = if fo then Thm.cterm_first_order_match (elhs', eta_t') |
|
821 |
else Thm.cterm_match (elhs', eta_t'); |
|
822 |
val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm); |
|
14643 | 823 |
val prop' = Thm.prop_of thm'; |
10413 | 824 |
val unconditional = (Logic.count_prems (prop',0) = 0); |
825 |
val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop') |
|
826 |
in |
|
11295 | 827 |
if perm andalso not (termless (rhs', lhs')) |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
828 |
then (trace_named_thm "Cannot apply permutative rewrite rule" (thm, name); |
13569 | 829 |
trace_thm "Term does not become smaller:" thm'; None) |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
830 |
else (trace_named_thm "Applying instance of rewrite rule" (thm, name); |
10413 | 831 |
if unconditional |
832 |
then |
|
13569 | 833 |
(trace_thm "Rewriting:" thm'; |
10413 | 834 |
let val lr = Logic.dest_equals prop; |
835 |
val Some thm'' = check_conv false eta_thm thm' |
|
836 |
in Some (thm'', uncond_skel (congs, lr)) end) |
|
837 |
else |
|
13569 | 838 |
(trace_thm "Trying to rewrite:" thm'; |
15023 | 839 |
case incr_depth ss of |
13828 | 840 |
None => (trace_thm "FAILED - reached depth limit" thm'; None) |
15023 | 841 |
| Some ss' => |
842 |
(case prover ss' thm' of |
|
843 |
None => (trace_thm "FAILED" thm'; None) |
|
10413 | 844 |
| Some thm2 => |
845 |
(case check_conv true eta_thm thm2 of |
|
846 |
None => None | |
|
847 |
Some thm2' => |
|
848 |
let val concl = Logic.strip_imp_concl prop |
|
849 |
val lr = Logic.dest_equals concl |
|
13828 | 850 |
in Some (thm2', cond_skel (congs, lr)) end)))) |
10413 | 851 |
end |
852 |
||
853 |
fun rews [] = None |
|
854 |
| rews (rrule :: rrules) = |
|
855 |
let val opt = rew rrule handle Pattern.MATCH => None |
|
856 |
in case opt of None => rews rrules | some => some end; |
|
857 |
||
858 |
fun sort_rrules rrs = let |
|
14643 | 859 |
fun is_simple({thm, ...}:rrule) = case Thm.prop_of thm of |
10413 | 860 |
Const("==",_) $ _ $ _ => true |
12603 | 861 |
| _ => false |
10413 | 862 |
fun sort [] (re1,re2) = re1 @ re2 |
12603 | 863 |
| sort (rr::rrs) (re1,re2) = if is_simple rr |
10413 | 864 |
then sort rrs (rr::re1,re2) |
865 |
else sort rrs (re1,rr::re2) |
|
866 |
in sort rrs ([],[]) end |
|
867 |
||
15023 | 868 |
fun proc_rews [] = None |
869 |
| proc_rews (Proc {name, proc, lhs, ...} :: ps) = |
|
870 |
if Pattern.matches tsigt (Thm.term_of lhs, Thm.term_of t) then |
|
10413 | 871 |
(debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t; |
13486
54464ea94d6f
exception SIMPROC_FAIL: solid error reporting of simprocs;
wenzelm
parents:
13458
diff
changeset
|
872 |
case transform_failure (curry SIMPROC_FAIL name) |
15023 | 873 |
(fn () => proc signt ss eta_t) () of |
13486
54464ea94d6f
exception SIMPROC_FAIL: solid error reporting of simprocs;
wenzelm
parents:
13458
diff
changeset
|
874 |
None => (debug false "FAILED"; proc_rews ps) |
54464ea94d6f
exception SIMPROC_FAIL: solid error reporting of simprocs;
wenzelm
parents:
13458
diff
changeset
|
875 |
| Some raw_thm => |
13569 | 876 |
(trace_thm ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm; |
10413 | 877 |
(case rews (mk_procrule raw_thm) of |
13486
54464ea94d6f
exception SIMPROC_FAIL: solid error reporting of simprocs;
wenzelm
parents:
13458
diff
changeset
|
878 |
None => (trace_cterm true ("IGNORED result of simproc " ^ quote name ^ |
54464ea94d6f
exception SIMPROC_FAIL: solid error reporting of simprocs;
wenzelm
parents:
13458
diff
changeset
|
879 |
" -- does not match") t; proc_rews ps) |
10413 | 880 |
| some => some))) |
881 |
else proc_rews ps; |
|
882 |
in case eta_t of |
|
883 |
Abs _ $ _ => Some (transitive eta_thm |
|
12155
13c5469b4bb3
congc now returns None if congruence rule has no effect.
berghofe
parents:
11886
diff
changeset
|
884 |
(beta_conversion false eta_t'), skel0) |
10413 | 885 |
| _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of |
886 |
None => proc_rews (Net.match_term procs eta_t) |
|
887 |
| some => some) |
|
888 |
end; |
|
889 |
||
890 |
||
891 |
(* conversion to apply a congruence rule to a term *) |
|
892 |
||
893 |
fun congc (prover,signt,maxt) {thm=cong,lhs=lhs} t = |
|
14643 | 894 |
let val sign = Thm.sign_of_thm cong |
10413 | 895 |
val _ = if Sign.subsig (sign, signt) then () |
896 |
else error("Congruence rule from different theory") |
|
897 |
val rthm = if maxt = ~1 then cong else Thm.incr_indexes (maxt+1) cong; |
|
898 |
val rlhs = fst (Drule.dest_equals (Drule.strip_imp_concl (cprop_of rthm))); |
|
899 |
val insts = Thm.cterm_match (rlhs, t) |
|
900 |
(* Pattern.match can raise Pattern.MATCH; |
|
901 |
is handled when congc is called *) |
|
902 |
val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm); |
|
13569 | 903 |
val unit = trace_thm "Applying congruence rule:" thm'; |
13932
0eb3d91b519a
Simplifier no longer aborts on failed congruence proof.
ballarin
parents:
13835
diff
changeset
|
904 |
fun err (msg, thm) = (trace_thm msg thm; None) |
10413 | 905 |
in case prover thm' of |
13932
0eb3d91b519a
Simplifier no longer aborts on failed congruence proof.
ballarin
parents:
13835
diff
changeset
|
906 |
None => err ("Congruence proof failed. Could not prove", thm') |
15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14981
diff
changeset
|
907 |
| Some thm2 => (case check_conv true (Drule.beta_eta_conversion t) thm2 of |
13932
0eb3d91b519a
Simplifier no longer aborts on failed congruence proof.
ballarin
parents:
13835
diff
changeset
|
908 |
None => err ("Congruence proof failed. Should not have proved", thm2) |
12155
13c5469b4bb3
congc now returns None if congruence rule has no effect.
berghofe
parents:
11886
diff
changeset
|
909 |
| Some thm2' => |
13c5469b4bb3
congc now returns None if congruence rule has no effect.
berghofe
parents:
11886
diff
changeset
|
910 |
if op aconv (pairself term_of (dest_equals (cprop_of thm2'))) |
13c5469b4bb3
congc now returns None if congruence rule has no effect.
berghofe
parents:
11886
diff
changeset
|
911 |
then None else Some thm2') |
10413 | 912 |
end; |
913 |
||
914 |
val (cA, (cB, cC)) = |
|
915 |
apsnd dest_equals (dest_implies (hd (cprems_of Drule.imp_cong))); |
|
916 |
||
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
917 |
fun transitive1 None None = None |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
918 |
| transitive1 (Some thm1) None = Some thm1 |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
919 |
| transitive1 None (Some thm2) = Some thm2 |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
920 |
| transitive1 (Some thm1) (Some thm2) = Some (transitive thm1 thm2) |
10413 | 921 |
|
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
922 |
fun transitive2 thm = transitive1 (Some thm); |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
923 |
fun transitive3 thm = transitive1 thm o Some; |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
924 |
|
15023 | 925 |
fun bottomc ((simprem, useprem, mutsimp), prover, sign, maxidx) = |
10413 | 926 |
let |
15023 | 927 |
fun botc skel ss t = |
10413 | 928 |
if is_Var skel then None |
929 |
else |
|
15023 | 930 |
(case subc skel ss t of |
10413 | 931 |
some as Some thm1 => |
15023 | 932 |
(case rewritec (prover, sign, maxidx) ss (rhs_of thm1) of |
10413 | 933 |
Some (thm2, skel2) => |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
934 |
transitive2 (transitive thm1 thm2) |
15023 | 935 |
(botc skel2 ss (rhs_of thm2)) |
10413 | 936 |
| None => some) |
937 |
| None => |
|
15023 | 938 |
(case rewritec (prover, sign, maxidx) ss t of |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
939 |
Some (thm2, skel2) => transitive2 thm2 |
15023 | 940 |
(botc skel2 ss (rhs_of thm2)) |
10413 | 941 |
| None => None)) |
942 |
||
15023 | 943 |
and try_botc ss t = |
944 |
(case botc skel0 ss t of |
|
10413 | 945 |
Some trec1 => trec1 | None => (reflexive t)) |
946 |
||
15023 | 947 |
and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 = |
10413 | 948 |
(case term_of t0 of |
949 |
Abs (a, T, t) => |
|
15023 | 950 |
let |
951 |
val b = variant bounds a; |
|
952 |
val (v, t') = Thm.dest_abs (Some ("." ^ b)) t0; |
|
953 |
val ss' = add_bound b ss; |
|
954 |
val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0; |
|
955 |
in case botc skel' ss' t' of |
|
10413 | 956 |
Some thm => Some (abstract_rule a v thm) |
957 |
| None => None |
|
958 |
end |
|
959 |
| t $ _ => (case t of |
|
15023 | 960 |
Const ("==>", _) $ _ => impc t0 ss |
10413 | 961 |
| Abs _ => |
962 |
let val thm = beta_conversion false t0 |
|
15023 | 963 |
in case subc skel0 ss (rhs_of thm) of |
10413 | 964 |
None => Some thm |
965 |
| Some thm' => Some (transitive thm thm') |
|
966 |
end |
|
967 |
| _ => |
|
968 |
let fun appc () = |
|
969 |
let |
|
970 |
val (tskel, uskel) = case skel of |
|
971 |
tskel $ uskel => (tskel, uskel) |
|
972 |
| _ => (skel0, skel0); |
|
10767
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10413
diff
changeset
|
973 |
val (ct, cu) = Thm.dest_comb t0 |
10413 | 974 |
in |
15023 | 975 |
(case botc tskel ss ct of |
10413 | 976 |
Some thm1 => |
15023 | 977 |
(case botc uskel ss cu of |
10413 | 978 |
Some thm2 => Some (combination thm1 thm2) |
979 |
| None => Some (combination thm1 (reflexive cu))) |
|
980 |
| None => |
|
15023 | 981 |
(case botc uskel ss cu of |
10413 | 982 |
Some thm1 => Some (combination (reflexive ct) thm1) |
983 |
| None => None)) |
|
984 |
end |
|
985 |
val (h, ts) = strip_comb t |
|
13835
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
13828
diff
changeset
|
986 |
in case cong_name h of |
12b2ffbe543a
Change to meta simplifier: congruence rules may now have frees as head of term.
ballarin
parents:
13828
diff
changeset
|
987 |
Some a => |
10413 | 988 |
(case assoc_string (fst congs, a) of |
989 |
None => appc () |
|
990 |
| Some cong => |
|
15023 | 991 |
(*post processing: some partial applications h t1 ... tj, j <= length ts, |
992 |
may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*) |
|
10413 | 993 |
(let |
15023 | 994 |
val thm = congc (prover ss, sign, maxidx) cong t0; |
12155
13c5469b4bb3
congc now returns None if congruence rule has no effect.
berghofe
parents:
11886
diff
changeset
|
995 |
val t = if_none (apsome rhs_of thm) t0; |
10767
8fa4aafa7314
Thm: dest_comb, dest_abs, capply, cabs no longer global;
wenzelm
parents:
10413
diff
changeset
|
996 |
val (cl, cr) = Thm.dest_comb t |
10413 | 997 |
val dVar = Var(("", 0), dummyT) |
998 |
val skel = |
|
999 |
list_comb (h, replicate (length ts) dVar) |
|
15023 | 1000 |
in case botc skel ss cl of |
12155
13c5469b4bb3
congc now returns None if congruence rule has no effect.
berghofe
parents:
11886
diff
changeset
|
1001 |
None => thm |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1002 |
| Some thm' => transitive3 thm |
12155
13c5469b4bb3
congc now returns None if congruence rule has no effect.
berghofe
parents:
11886
diff
changeset
|
1003 |
(combination thm' (reflexive cr)) |
10413 | 1004 |
end handle TERM _ => error "congc result" |
1005 |
| Pattern.MATCH => appc ())) |
|
1006 |
| _ => appc () |
|
1007 |
end) |
|
1008 |
| _ => None) |
|
1009 |
||
15023 | 1010 |
and impc ct ss = |
1011 |
if mutsimp then mut_impc0 [] ct [] [] ss else nonmut_impc ct ss |
|
10413 | 1012 |
|
15023 | 1013 |
and rules_of_prem ss prem = |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1014 |
if maxidx_of_term (term_of prem) <> ~1 |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1015 |
then (trace_cterm true |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1016 |
"Cannot add premise as rewrite rule because it contains (type) unknowns:" prem; ([], None)) |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1017 |
else |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1018 |
let val asm = assume prem |
15023 | 1019 |
in (extract_safe_rrules (ss, asm), Some asm) end |
10413 | 1020 |
|
15023 | 1021 |
and add_rrules (rrss, asms) ss = |
15195 | 1022 |
let val Asms = mapfilter I asms |
1023 |
in foldl (insert_rrule true) (ss, flat rrss) |> add_prems2 Asms end |
|
10413 | 1024 |
|
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1025 |
and disch r (prem, eq) = |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1026 |
let |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1027 |
val (lhs, rhs) = dest_eq eq; |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1028 |
val eq' = implies_elim (Thm.instantiate |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1029 |
([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong) |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1030 |
(implies_intr prem eq) |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1031 |
in if not r then eq' else |
10413 | 1032 |
let |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1033 |
val (prem', concl) = dest_implies lhs; |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1034 |
val (prem'', _) = dest_implies rhs |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1035 |
in transitive (transitive |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1036 |
(Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)]) |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1037 |
Drule.swap_prems_eq) eq') |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1038 |
(Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)]) |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1039 |
Drule.swap_prems_eq) |
10413 | 1040 |
end |
1041 |
end |
|
1042 |
||
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1043 |
and rebuild [] _ _ _ _ eq = eq |
15023 | 1044 |
| rebuild (prem :: prems) concl (rrs :: rrss) (asm :: asms) ss eq = |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1045 |
let |
15023 | 1046 |
val ss' = add_rrules (rev rrss, rev asms) ss; |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1047 |
val concl' = |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1048 |
Drule.mk_implies (prem, if_none (apsome rhs_of eq) concl); |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1049 |
val dprem = apsome (curry (disch false) prem) |
15023 | 1050 |
in case rewritec (prover, sign, maxidx) ss' concl' of |
1051 |
None => rebuild prems concl' rrss asms ss (dprem eq) |
|
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1052 |
| Some (eq', _) => transitive2 (foldl (disch false o swap) |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1053 |
(the (transitive3 (dprem eq) eq'), prems)) |
15023 | 1054 |
(mut_impc0 (rev prems) (rhs_of eq') (rev rrss) (rev asms) ss) |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1055 |
end |
15023 | 1056 |
|
1057 |
and mut_impc0 prems concl rrss asms ss = |
|
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1058 |
let |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1059 |
val prems' = strip_imp_prems concl; |
15023 | 1060 |
val (rrss', asms') = split_list (map (rules_of_prem ss) prems') |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1061 |
in mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss') |
15023 | 1062 |
(asms @ asms') [] [] [] [] ss ~1 ~1 |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1063 |
end |
15023 | 1064 |
|
1065 |
and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k = |
|
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1066 |
transitive1 (foldl (fn (eq2, (eq1, prem)) => transitive1 eq1 |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1067 |
(apsome (curry (disch false) prem) eq2)) (None, eqns ~~ prems')) |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1068 |
(if changed > 0 then |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1069 |
mut_impc (rev prems') concl (rev rrss') (rev asms') |
15023 | 1070 |
[] [] [] [] ss ~1 changed |
1071 |
else rebuild prems' concl rrss' asms' ss |
|
1072 |
(botc skel0 (add_rrules (rev rrss', rev asms') ss) concl)) |
|
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1073 |
|
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1074 |
| mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms) |
15023 | 1075 |
prems' rrss' asms' eqns ss changed k = |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1076 |
case (if k = 0 then None else botc skel0 (add_rrules |
15023 | 1077 |
(rev rrss' @ rrss, rev asms' @ asms) ss) prem) of |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1078 |
None => mut_impc prems concl rrss asms (prem :: prems') |
15023 | 1079 |
(rrs :: rrss') (asm :: asms') (None :: eqns) ss changed |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1080 |
(if k = 0 then 0 else k - 1) |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1081 |
| Some eqn => |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1082 |
let |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1083 |
val prem' = rhs_of eqn; |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1084 |
val tprems = map term_of prems; |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1085 |
val i = 1 + foldl Int.max (~1, map (fn p => |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1086 |
find_index_eq p tprems) (#hyps (rep_thm eqn))); |
15023 | 1087 |
val (rrs', asm') = rules_of_prem ss prem' |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1088 |
in mut_impc prems concl rrss asms (prem' :: prems') |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1089 |
(rrs' :: rrss') (asm' :: asms') (Some (foldr (disch true) |
15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14981
diff
changeset
|
1090 |
(take (i, prems), Drule.imp_cong' eqn (reflexive (Drule.list_implies |
15023 | 1091 |
(drop (i, prems), concl))))) :: eqns) ss (length prems') ~1 |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1092 |
end |
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1093 |
|
15023 | 1094 |
(*legacy code - only for backwards compatibility*) |
1095 |
and nonmut_impc ct ss = |
|
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1096 |
let val (prem, conc) = dest_implies ct; |
15023 | 1097 |
val thm1 = if simprem then botc skel0 ss prem else None; |
10413 | 1098 |
val prem1 = if_none (apsome rhs_of thm1) prem; |
15023 | 1099 |
val ss1 = if not useprem then ss else add_rrules |
1100 |
(apsnd single (apfst single (rules_of_prem ss prem1))) ss |
|
1101 |
in (case botc skel0 ss1 conc of |
|
10413 | 1102 |
None => (case thm1 of |
1103 |
None => None |
|
15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14981
diff
changeset
|
1104 |
| Some thm1' => Some (Drule.imp_cong' thm1' (reflexive conc))) |
10413 | 1105 |
| Some thm2 => |
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1106 |
let val thm2' = disch false (prem1, thm2) |
10413 | 1107 |
in (case thm1 of |
1108 |
None => Some thm2' |
|
13607
6908230623a3
Completely reimplemented mutual simplification of premises.
berghofe
parents:
13569
diff
changeset
|
1109 |
| Some thm1' => |
15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14981
diff
changeset
|
1110 |
Some (transitive (Drule.imp_cong' thm1' (reflexive conc)) thm2')) |
10413 | 1111 |
end) |
1112 |
end |
|
1113 |
||
15023 | 1114 |
in try_botc end; |
10413 | 1115 |
|
1116 |
||
15023 | 1117 |
(* Meta-rewriting: rewrites t to u and returns the theorem t==u *) |
10413 | 1118 |
|
1119 |
(* |
|
1120 |
Parameters: |
|
1121 |
mode = (simplify A, |
|
1122 |
use A in simplifying B, |
|
1123 |
use prems of B (if B is again a meta-impl.) to simplify A) |
|
1124 |
when simplifying A ==> B |
|
1125 |
prover: how to solve premises in conditional rewrites and congruences |
|
1126 |
*) |
|
1127 |
||
15023 | 1128 |
fun rewrite_cterm mode prover ss ct = |
1129 |
let |
|
1130 |
val Simpset ({depth, ...}, _) = ss; |
|
1131 |
val {sign, t, maxidx, ...} = Thm.rep_cterm ct; |
|
1132 |
in |
|
1133 |
trace_cterm false "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" ct; |
|
1134 |
simp_depth := depth; |
|
1135 |
bottomc (mode, prover, sign, maxidx) ss ct |
|
1136 |
end handle THM (s, _, thms) => |
|
10413 | 1137 |
error ("Exception THM was raised in simplifier:\n" ^ s ^ "\n" ^ |
11886 | 1138 |
Pretty.string_of (Display.pretty_thms thms)); |
10413 | 1139 |
|
11760 | 1140 |
(*Rewrite a cterm*) |
11767 | 1141 |
fun rewrite_aux _ _ [] = (fn ct => Thm.reflexive ct) |
15023 | 1142 |
| rewrite_aux prover full thms = |
1143 |
rewrite_cterm (full, false, false) prover (empty_ss addsimps thms); |
|
11672 | 1144 |
|
10413 | 1145 |
(*Rewrite a theorem*) |
11767 | 1146 |
fun simplify_aux _ _ [] = (fn th => th) |
1147 |
| simplify_aux prover full thms = |
|
15023 | 1148 |
Drule.fconv_rule (rewrite_cterm (full, false, false) prover (empty_ss addsimps thms)); |
10413 | 1149 |
|
15023 | 1150 |
(*simple term rewriting -- no proof*) |
1151 |
fun rewrite_term sg rules procs = |
|
1152 |
Pattern.rewrite_term (Sign.tsig_of sg) (map decomp_simp' rules) procs; |
|
1153 |
||
1154 |
fun rewrite_thm mode prover ss = Drule.fconv_rule (rewrite_cterm mode prover ss); |
|
10413 | 1155 |
|
1156 |
(*Rewrite the subgoals of a proof state (represented by a theorem) *) |
|
1157 |
fun rewrite_goals_rule_aux _ [] th = th |
|
1158 |
| rewrite_goals_rule_aux prover thms th = |
|
15001
fb2141a9f8c0
Moved conversion rules from MetaSimplifier to Drule. refl_implies removed
skalberg
parents:
14981
diff
changeset
|
1159 |
Drule.fconv_rule (Drule.goals_conv (K true) (rewrite_cterm (true, true, false) prover |
15023 | 1160 |
(empty_ss addsimps thms))) th; |
10413 | 1161 |
|
15023 | 1162 |
(*Rewrite the subgoal of a proof state (represented by a theorem)*) |
15011 | 1163 |
fun rewrite_goal_rule mode prover ss i thm = |
10413 | 1164 |
if 0 < i andalso i <= nprems_of thm |
15011 | 1165 |
then Drule.fconv_rule (Drule.goals_conv (fn j => j=i) (rewrite_cterm mode prover ss)) thm |
10413 | 1166 |
else raise THM("rewrite_goal_rule",i,[thm]); |
1167 |
||
15023 | 1168 |
(*Rewrite subgoal i only. SELECT_GOAL avoids inefficiencies in goals_conv.*) |
1169 |
fun asm_rewrite_goal_tac mode prover_tac ss = |
|
1170 |
SELECT_GOAL |
|
1171 |
(PRIMITIVE (rewrite_goal_rule mode (SINGLE o prover_tac) ss 1)); |
|
12783 | 1172 |
|
15023 | 1173 |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
1174 |
|
15023 | 1175 |
(** simplification tactics and rules **) |
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
1176 |
|
15023 | 1177 |
fun solve_all_tac solvers ss = |
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
1178 |
let |
15023 | 1179 |
val Simpset (_, {subgoal_tac, ...}) = ss; |
1180 |
val solve_tac = subgoal_tac (set_solvers solvers ss) THEN_ALL_NEW (K no_tac); |
|
1181 |
in DEPTH_SOLVE (solve_tac 1) end; |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
1182 |
|
15023 | 1183 |
(*NOTE: may instantiate unknowns that appear also in other subgoals*) |
1184 |
fun generic_simp_tac safe mode ss = |
|
1185 |
let |
|
1186 |
val Simpset ({prems, ...}, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = ss; |
|
1187 |
val loop_tac = FIRST' (map #2 loop_tacs); |
|
1188 |
val solve_tac = FIRST' (map (solver prems) (if safe then solvers else unsafe_solvers)); |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
1189 |
|
15023 | 1190 |
fun simp_loop_tac i = |
1191 |
asm_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ss i THEN |
|
1192 |
(solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i)); |
|
1193 |
in simp_loop_tac end; |
|
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
1194 |
|
15023 | 1195 |
fun simp rew mode ss thm = |
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
1196 |
let |
15023 | 1197 |
val Simpset (_, {solvers = (unsafe_solvers, _), ...}) = ss; |
1198 |
val tacf = solve_all_tac unsafe_solvers; |
|
1199 |
fun prover s th = apsome #1 (Seq.pull (tacf s th)); |
|
15011 | 1200 |
in rew mode prover ss thm end; |
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
1201 |
|
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
1202 |
val simp_thm = simp rewrite_thm; |
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
1203 |
val simp_cterm = simp rewrite_cterm; |
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
15001
diff
changeset
|
1204 |
|
10413 | 1205 |
end; |
1206 |
||
11672 | 1207 |
structure BasicMetaSimplifier: BASIC_META_SIMPLIFIER = MetaSimplifier; |
1208 |
open BasicMetaSimplifier; |