wenzelm@41494
|
1 |
(* Title: Pure/raw_simplifier.ML
|
wenzelm@29269
|
2 |
Author: Tobias Nipkow and Stefan Berghofer, TU Muenchen
|
berghofe@10413
|
3 |
|
wenzelm@41494
|
4 |
Higher-order Simplification.
|
berghofe@10413
|
5 |
*)
|
berghofe@10413
|
6 |
|
skalberg@15006
|
7 |
infix 4
|
wenzelm@15023
|
8 |
addsimps delsimps addeqcongs deleqcongs addcongs delcongs addsimprocs delsimprocs
|
nipkow@15199
|
9 |
setmksimps setmkcong setmksym setmkeqTrue settermless setsubgoaler
|
wenzelm@17882
|
10 |
setloop' setloop addloop addloop' delloop setSSolver addSSolver setSolver addSolver;
|
skalberg@15006
|
11 |
|
wenzelm@41494
|
12 |
signature BASIC_RAW_SIMPLIFIER =
|
wenzelm@11672
|
13 |
sig
|
wenzelm@41493
|
14 |
val simp_depth_limit: int Config.T
|
wenzelm@41493
|
15 |
val simp_trace_depth_limit: int Config.T
|
wenzelm@41136
|
16 |
val simp_debug: bool Config.T
|
wenzelm@41136
|
17 |
val simp_trace: bool Config.T
|
wenzelm@15023
|
18 |
type rrule
|
wenzelm@16807
|
19 |
val eq_rrule: rrule * rrule -> bool
|
wenzelm@15023
|
20 |
type simpset
|
wenzelm@15023
|
21 |
type proc
|
wenzelm@17614
|
22 |
type solver
|
wenzelm@44469
|
23 |
val mk_solver: string -> (simpset -> int -> tactic) -> solver
|
wenzelm@15023
|
24 |
val empty_ss: simpset
|
wenzelm@15023
|
25 |
val merge_ss: simpset * simpset -> simpset
|
wenzelm@30356
|
26 |
val dest_ss: simpset ->
|
wenzelm@30356
|
27 |
{simps: (string * thm) list,
|
wenzelm@30356
|
28 |
procs: (string * cterm list) list,
|
wenzelm@30356
|
29 |
congs: (string * thm) list,
|
wenzelm@30356
|
30 |
weak_congs: string list,
|
wenzelm@30356
|
31 |
loopers: string list,
|
wenzelm@30356
|
32 |
unsafe_solvers: string list,
|
wenzelm@30356
|
33 |
safe_solvers: string list}
|
wenzelm@15023
|
34 |
type simproc
|
wenzelm@22234
|
35 |
val eq_simproc: simproc * simproc -> bool
|
wenzelm@22234
|
36 |
val morph_simproc: morphism -> simproc -> simproc
|
wenzelm@22234
|
37 |
val make_simproc: {name: string, lhss: cterm list,
|
wenzelm@22234
|
38 |
proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc
|
wenzelm@22008
|
39 |
val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
|
wenzelm@15023
|
40 |
val prems_of_ss: simpset -> thm list
|
wenzelm@15023
|
41 |
val addsimps: simpset * thm list -> simpset
|
wenzelm@15023
|
42 |
val delsimps: simpset * thm list -> simpset
|
wenzelm@15023
|
43 |
val addeqcongs: simpset * thm list -> simpset
|
wenzelm@15023
|
44 |
val deleqcongs: simpset * thm list -> simpset
|
wenzelm@15023
|
45 |
val addcongs: simpset * thm list -> simpset
|
wenzelm@15023
|
46 |
val delcongs: simpset * thm list -> simpset
|
wenzelm@15023
|
47 |
val addsimprocs: simpset * simproc list -> simpset
|
wenzelm@15023
|
48 |
val delsimprocs: simpset * simproc list -> simpset
|
wenzelm@30321
|
49 |
val mksimps: simpset -> thm -> thm list
|
wenzelm@36543
|
50 |
val setmksimps: simpset * (simpset -> thm -> thm list) -> simpset
|
wenzelm@36543
|
51 |
val setmkcong: simpset * (simpset -> thm -> thm) -> simpset
|
wenzelm@36543
|
52 |
val setmksym: simpset * (simpset -> thm -> thm option) -> simpset
|
wenzelm@36543
|
53 |
val setmkeqTrue: simpset * (simpset -> thm -> thm option) -> simpset
|
wenzelm@15023
|
54 |
val settermless: simpset * (term * term -> bool) -> simpset
|
wenzelm@15023
|
55 |
val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset
|
wenzelm@17882
|
56 |
val setloop': simpset * (simpset -> int -> tactic) -> simpset
|
wenzelm@15023
|
57 |
val setloop: simpset * (int -> tactic) -> simpset
|
wenzelm@17882
|
58 |
val addloop': simpset * (string * (simpset -> int -> tactic)) -> simpset
|
wenzelm@15023
|
59 |
val addloop: simpset * (string * (int -> tactic)) -> simpset
|
wenzelm@15023
|
60 |
val delloop: simpset * string -> simpset
|
wenzelm@15023
|
61 |
val setSSolver: simpset * solver -> simpset
|
wenzelm@15023
|
62 |
val addSSolver: simpset * solver -> simpset
|
wenzelm@15023
|
63 |
val setSolver: simpset * solver -> simpset
|
wenzelm@15023
|
64 |
val addSolver: simpset * solver -> simpset
|
wenzelm@21708
|
65 |
|
wenzelm@21708
|
66 |
val rewrite_rule: thm list -> thm -> thm
|
wenzelm@21708
|
67 |
val rewrite_goals_rule: thm list -> thm -> thm
|
wenzelm@21708
|
68 |
val rewrite_goals_tac: thm list -> tactic
|
wenzelm@23536
|
69 |
val rewrite_goal_tac: thm list -> int -> tactic
|
wenzelm@21708
|
70 |
val rewtac: thm -> tactic
|
wenzelm@21708
|
71 |
val prune_params_tac: tactic
|
wenzelm@21708
|
72 |
val fold_rule: thm list -> thm -> thm
|
wenzelm@21708
|
73 |
val fold_goals_tac: thm list -> tactic
|
wenzelm@30554
|
74 |
val norm_hhf: thm -> thm
|
wenzelm@30554
|
75 |
val norm_hhf_protect: thm -> thm
|
skalberg@15006
|
76 |
end;
|
skalberg@15006
|
77 |
|
wenzelm@41494
|
78 |
signature RAW_SIMPLIFIER =
|
berghofe@10413
|
79 |
sig
|
wenzelm@41494
|
80 |
include BASIC_RAW_SIMPLIFIER
|
berghofe@10413
|
81 |
exception SIMPLIFIER of string * thm
|
wenzelm@30342
|
82 |
val internal_ss: simpset ->
|
wenzelm@30342
|
83 |
{rules: rrule Net.net,
|
wenzelm@30342
|
84 |
prems: thm list,
|
wenzelm@30342
|
85 |
bounds: int * ((string * typ) * string) list,
|
wenzelm@32738
|
86 |
depth: int * bool Unsynchronized.ref,
|
wenzelm@30342
|
87 |
context: Proof.context option} *
|
krauss@30908
|
88 |
{congs: (string * thm) list * string list,
|
wenzelm@30342
|
89 |
procs: proc Net.net,
|
wenzelm@30342
|
90 |
mk_rews:
|
wenzelm@36543
|
91 |
{mk: simpset -> thm -> thm list,
|
wenzelm@36543
|
92 |
mk_cong: simpset -> thm -> thm,
|
wenzelm@36543
|
93 |
mk_sym: simpset -> thm -> thm option,
|
wenzelm@36543
|
94 |
mk_eq_True: simpset -> thm -> thm option,
|
wenzelm@30342
|
95 |
reorient: theory -> term list -> term -> term -> bool},
|
wenzelm@30342
|
96 |
termless: term * term -> bool,
|
wenzelm@30342
|
97 |
subgoal_tac: simpset -> int -> tactic,
|
wenzelm@30342
|
98 |
loop_tacs: (string * (simpset -> int -> tactic)) list,
|
wenzelm@30342
|
99 |
solvers: solver list * solver list}
|
haftmann@27558
|
100 |
val add_simp: thm -> simpset -> simpset
|
haftmann@27558
|
101 |
val del_simp: thm -> simpset -> simpset
|
wenzelm@17966
|
102 |
val solver: simpset -> solver -> int -> tactic
|
wenzelm@39409
|
103 |
val simp_depth_limit_raw: Config.raw
|
wenzelm@15023
|
104 |
val clear_ss: simpset -> simpset
|
wenzelm@38963
|
105 |
val simproc_global_i: theory -> string -> term list
|
wenzelm@16458
|
106 |
-> (theory -> simpset -> term -> thm option) -> simproc
|
wenzelm@38963
|
107 |
val simproc_global: theory -> string -> string list
|
wenzelm@16458
|
108 |
-> (theory -> simpset -> term -> thm option) -> simproc
|
wenzelm@41493
|
109 |
val simp_trace_depth_limit_raw: Config.raw
|
wenzelm@41493
|
110 |
val simp_trace_depth_limit_default: int Unsynchronized.ref
|
wenzelm@41493
|
111 |
val simp_trace_default: bool Unsynchronized.ref
|
wenzelm@41493
|
112 |
val simp_trace_raw: Config.raw
|
wenzelm@41493
|
113 |
val simp_debug_raw: Config.raw
|
wenzelm@41492
|
114 |
val add_prems: thm list -> simpset -> simpset
|
wenzelm@17882
|
115 |
val inherit_context: simpset -> simpset -> simpset
|
wenzelm@20289
|
116 |
val the_context: simpset -> Proof.context
|
wenzelm@20289
|
117 |
val context: Proof.context -> simpset -> simpset
|
wenzelm@43325
|
118 |
val global_context: theory -> simpset -> simpset
|
wenzelm@36577
|
119 |
val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset
|
wenzelm@32738
|
120 |
val debug_bounds: bool Unsynchronized.ref
|
wenzelm@18208
|
121 |
val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset
|
wenzelm@17966
|
122 |
val set_solvers: solver list -> simpset -> simpset
|
wenzelm@23598
|
123 |
val rewrite_cterm: bool * bool * bool -> (simpset -> thm -> thm option) -> simpset -> conv
|
wenzelm@16458
|
124 |
val rewrite_term: theory -> thm list -> (term -> term option) list -> term -> term
|
wenzelm@15023
|
125 |
val rewrite_thm: bool * bool * bool ->
|
wenzelm@15023
|
126 |
(simpset -> thm -> thm option) -> simpset -> thm -> thm
|
wenzelm@15023
|
127 |
val rewrite_goal_rule: bool * bool * bool ->
|
wenzelm@15023
|
128 |
(simpset -> thm -> thm option) -> simpset -> int -> thm -> thm
|
wenzelm@23536
|
129 |
val asm_rewrite_goal_tac: bool * bool * bool ->
|
wenzelm@23536
|
130 |
(simpset -> tactic) -> simpset -> int -> tactic
|
wenzelm@23598
|
131 |
val rewrite: bool -> thm list -> conv
|
wenzelm@21708
|
132 |
val simplify: bool -> thm list -> thm -> thm
|
berghofe@10413
|
133 |
end;
|
berghofe@10413
|
134 |
|
wenzelm@41494
|
135 |
structure Raw_Simplifier: RAW_SIMPLIFIER =
|
berghofe@10413
|
136 |
struct
|
berghofe@10413
|
137 |
|
wenzelm@15023
|
138 |
(** datatype simpset **)
|
wenzelm@15023
|
139 |
|
wenzelm@15023
|
140 |
(* rewrite rules *)
|
berghofe@10413
|
141 |
|
wenzelm@20546
|
142 |
type rrule =
|
wenzelm@20546
|
143 |
{thm: thm, (*the rewrite rule*)
|
wenzelm@20546
|
144 |
name: string, (*name of theorem from which rewrite rule was extracted*)
|
wenzelm@20546
|
145 |
lhs: term, (*the left-hand side*)
|
wenzelm@20546
|
146 |
elhs: cterm, (*the etac-contracted lhs*)
|
wenzelm@20546
|
147 |
extra: bool, (*extra variables outside of elhs*)
|
wenzelm@20546
|
148 |
fo: bool, (*use first-order matching*)
|
wenzelm@20546
|
149 |
perm: bool}; (*the rewrite rule is permutative*)
|
wenzelm@15023
|
150 |
|
wenzelm@20546
|
151 |
(*
|
wenzelm@12603
|
152 |
Remarks:
|
berghofe@10413
|
153 |
- elhs is used for matching,
|
wenzelm@15023
|
154 |
lhs only for preservation of bound variable names;
|
berghofe@10413
|
155 |
- fo is set iff
|
berghofe@10413
|
156 |
either elhs is first-order (no Var is applied),
|
wenzelm@15023
|
157 |
in which case fo-matching is complete,
|
berghofe@10413
|
158 |
or elhs is not a pattern,
|
wenzelm@20546
|
159 |
in which case there is nothing better to do;
|
wenzelm@20546
|
160 |
*)
|
wenzelm@15023
|
161 |
|
wenzelm@15023
|
162 |
fun eq_rrule ({thm = thm1, ...}: rrule, {thm = thm2, ...}: rrule) =
|
wenzelm@22360
|
163 |
Thm.eq_thm_prop (thm1, thm2);
|
wenzelm@15023
|
164 |
|
wenzelm@15023
|
165 |
|
wenzelm@17614
|
166 |
(* simplification sets, procedures, and solvers *)
|
wenzelm@15023
|
167 |
|
wenzelm@15023
|
168 |
(*A simpset contains data required during conversion:
|
berghofe@10413
|
169 |
rules: discrimination net of rewrite rules;
|
wenzelm@15023
|
170 |
prems: current premises;
|
berghofe@15249
|
171 |
bounds: maximal index of bound variables already used
|
wenzelm@15023
|
172 |
(for generating new names when rewriting under lambda abstractions);
|
wenzelm@22892
|
173 |
depth: simp_depth and exceeded flag;
|
berghofe@10413
|
174 |
congs: association list of congruence rules and
|
berghofe@10413
|
175 |
a list of `weak' congruence constants.
|
berghofe@10413
|
176 |
A congruence is `weak' if it avoids normalization of some argument.
|
berghofe@10413
|
177 |
procs: discrimination net of simplification procedures
|
berghofe@10413
|
178 |
(functions that prove rewrite rules on the fly);
|
wenzelm@15023
|
179 |
mk_rews:
|
wenzelm@15023
|
180 |
mk: turn simplification thms into rewrite rules;
|
wenzelm@15023
|
181 |
mk_cong: prepare congruence rules;
|
wenzelm@15023
|
182 |
mk_sym: turn == around;
|
wenzelm@15023
|
183 |
mk_eq_True: turn P into P == True;
|
wenzelm@15023
|
184 |
termless: relation for ordered rewriting;*)
|
berghofe@10413
|
185 |
|
wenzelm@15023
|
186 |
datatype simpset =
|
wenzelm@15023
|
187 |
Simpset of
|
wenzelm@15023
|
188 |
{rules: rrule Net.net,
|
wenzelm@15023
|
189 |
prems: thm list,
|
wenzelm@17882
|
190 |
bounds: int * ((string * typ) * string) list,
|
wenzelm@32738
|
191 |
depth: int * bool Unsynchronized.ref,
|
wenzelm@20289
|
192 |
context: Proof.context option} *
|
krauss@30908
|
193 |
{congs: (string * thm) list * string list,
|
wenzelm@15023
|
194 |
procs: proc Net.net,
|
wenzelm@36543
|
195 |
mk_rews:
|
wenzelm@36543
|
196 |
{mk: simpset -> thm -> thm list,
|
wenzelm@36543
|
197 |
mk_cong: simpset -> thm -> thm,
|
wenzelm@36543
|
198 |
mk_sym: simpset -> thm -> thm option,
|
wenzelm@36543
|
199 |
mk_eq_True: simpset -> thm -> thm option,
|
wenzelm@36543
|
200 |
reorient: theory -> term list -> term -> term -> bool},
|
nipkow@11504
|
201 |
termless: term * term -> bool,
|
skalberg@15011
|
202 |
subgoal_tac: simpset -> int -> tactic,
|
wenzelm@17882
|
203 |
loop_tacs: (string * (simpset -> int -> tactic)) list,
|
wenzelm@15023
|
204 |
solvers: solver list * solver list}
|
wenzelm@15023
|
205 |
and proc =
|
wenzelm@15023
|
206 |
Proc of
|
wenzelm@15023
|
207 |
{name: string,
|
wenzelm@15023
|
208 |
lhs: cterm,
|
wenzelm@22008
|
209 |
proc: simpset -> cterm -> thm option,
|
wenzelm@22234
|
210 |
id: stamp * thm list}
|
wenzelm@17614
|
211 |
and solver =
|
wenzelm@17614
|
212 |
Solver of
|
wenzelm@17614
|
213 |
{name: string,
|
wenzelm@17614
|
214 |
solver: simpset -> int -> tactic,
|
wenzelm@15023
|
215 |
id: stamp};
|
berghofe@10413
|
216 |
|
berghofe@10413
|
217 |
|
wenzelm@30342
|
218 |
fun internal_ss (Simpset args) = args;
|
berghofe@10413
|
219 |
|
wenzelm@22892
|
220 |
fun make_ss1 (rules, prems, bounds, depth, context) =
|
wenzelm@22892
|
221 |
{rules = rules, prems = prems, bounds = bounds, depth = depth, context = context};
|
berghofe@10413
|
222 |
|
wenzelm@22892
|
223 |
fun map_ss1 f {rules, prems, bounds, depth, context} =
|
wenzelm@22892
|
224 |
make_ss1 (f (rules, prems, bounds, depth, context));
|
berghofe@10413
|
225 |
|
wenzelm@15023
|
226 |
fun make_ss2 (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =
|
wenzelm@15023
|
227 |
{congs = congs, procs = procs, mk_rews = mk_rews, termless = termless,
|
wenzelm@15023
|
228 |
subgoal_tac = subgoal_tac, loop_tacs = loop_tacs, solvers = solvers};
|
berghofe@10413
|
229 |
|
wenzelm@15023
|
230 |
fun map_ss2 f {congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers} =
|
wenzelm@15023
|
231 |
make_ss2 (f (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
|
skalberg@15011
|
232 |
|
wenzelm@15023
|
233 |
fun make_simpset (args1, args2) = Simpset (make_ss1 args1, make_ss2 args2);
|
skalberg@15011
|
234 |
|
wenzelm@15023
|
235 |
fun map_simpset1 f (Simpset (r1, r2)) = Simpset (map_ss1 f r1, r2);
|
wenzelm@15023
|
236 |
fun map_simpset2 f (Simpset (r1, r2)) = Simpset (r1, map_ss2 f r2);
|
berghofe@10413
|
237 |
|
wenzelm@17614
|
238 |
fun prems_of_ss (Simpset ({prems, ...}, _)) = prems;
|
wenzelm@17614
|
239 |
|
wenzelm@22234
|
240 |
fun eq_procid ((s1: stamp, ths1: thm list), (s2, ths2)) =
|
wenzelm@22360
|
241 |
s1 = s2 andalso eq_list Thm.eq_thm (ths1, ths2);
|
wenzelm@22234
|
242 |
fun eq_proc (Proc {id = id1, ...}, Proc {id = id2, ...}) = eq_procid (id1, id2);
|
wenzelm@17614
|
243 |
|
wenzelm@44469
|
244 |
fun mk_solver name solver = Solver {name = name, solver = solver, id = stamp ()};
|
wenzelm@17614
|
245 |
|
wenzelm@17614
|
246 |
fun solver_name (Solver {name, ...}) = name;
|
wenzelm@17966
|
247 |
fun solver ss (Solver {solver = tac, ...}) = tac ss;
|
wenzelm@17614
|
248 |
fun eq_solver (Solver {id = id1, ...}, Solver {id = id2, ...}) = (id1 = id2);
|
wenzelm@17614
|
249 |
|
berghofe@10413
|
250 |
|
wenzelm@22892
|
251 |
(* simp depth *)
|
wenzelm@22892
|
252 |
|
wenzelm@39409
|
253 |
val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
|
wenzelm@39409
|
254 |
val simp_depth_limit = Config.int simp_depth_limit_raw;
|
wenzelm@24124
|
255 |
|
boehmes@41431
|
256 |
val simp_trace_depth_limit_default = Unsynchronized.ref 1;
|
boehmes@41431
|
257 |
val simp_trace_depth_limit_raw = Config.declare "simp_trace_depth_limit"
|
boehmes@41431
|
258 |
(fn _ => Config.Int (! simp_trace_depth_limit_default));
|
boehmes@41431
|
259 |
val simp_trace_depth_limit = Config.int simp_trace_depth_limit_raw;
|
wenzelm@22892
|
260 |
|
boehmes@41431
|
261 |
fun simp_trace_depth_limit_of NONE = ! simp_trace_depth_limit_default
|
boehmes@41431
|
262 |
| simp_trace_depth_limit_of (SOME ctxt) = Config.get ctxt simp_trace_depth_limit;
|
boehmes@41431
|
263 |
|
boehmes@41431
|
264 |
fun trace_depth (Simpset ({depth = (depth, exceeded), context, ...}, _)) msg =
|
boehmes@41431
|
265 |
if depth > simp_trace_depth_limit_of context then
|
wenzelm@41136
|
266 |
if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true)
|
wenzelm@22892
|
267 |
else
|
wenzelm@23938
|
268 |
(tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false);
|
wenzelm@22892
|
269 |
|
wenzelm@22892
|
270 |
val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
|
wenzelm@22892
|
271 |
(rules, prems, bounds,
|
wenzelm@32738
|
272 |
(depth + 1,
|
boehmes@41431
|
273 |
if depth = simp_trace_depth_limit_of context then Unsynchronized.ref false else exceeded), context));
|
wenzelm@22892
|
274 |
|
wenzelm@22892
|
275 |
fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
|
wenzelm@22892
|
276 |
|
wenzelm@22892
|
277 |
|
wenzelm@16985
|
278 |
(* diagnostics *)
|
wenzelm@16985
|
279 |
|
wenzelm@16985
|
280 |
exception SIMPLIFIER of string * thm;
|
wenzelm@16985
|
281 |
|
wenzelm@41136
|
282 |
val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
|
wenzelm@41136
|
283 |
val simp_debug = Config.bool simp_debug_raw;
|
boehmes@35979
|
284 |
|
wenzelm@41136
|
285 |
val simp_trace_default = Unsynchronized.ref false;
|
wenzelm@41136
|
286 |
val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default));
|
wenzelm@41136
|
287 |
val simp_trace = Config.bool simp_trace_raw;
|
wenzelm@22892
|
288 |
|
wenzelm@39080
|
289 |
fun if_enabled (Simpset ({context, ...}, _)) flag f =
|
wenzelm@39080
|
290 |
(case context of
|
wenzelm@39080
|
291 |
SOME ctxt => if Config.get ctxt flag then f ctxt else ()
|
wenzelm@39080
|
292 |
| NONE => ())
|
wenzelm@39080
|
293 |
|
wenzelm@39080
|
294 |
fun if_visible (Simpset ({context, ...}, _)) f x =
|
wenzelm@39080
|
295 |
(case context of
|
wenzelm@41717
|
296 |
SOME ctxt => Context_Position.if_visible ctxt f x
|
wenzelm@39080
|
297 |
| NONE => ());
|
wenzelm@39080
|
298 |
|
wenzelm@16985
|
299 |
local
|
wenzelm@16985
|
300 |
|
wenzelm@22892
|
301 |
fun prnt ss warn a = if warn then warning a else trace_depth ss a;
|
wenzelm@16985
|
302 |
|
wenzelm@16985
|
303 |
fun show_bounds (Simpset ({bounds = (_, bs), ...}, _)) t =
|
wenzelm@16985
|
304 |
let
|
wenzelm@20146
|
305 |
val names = Term.declare_term_names t Name.context;
|
wenzelm@44208
|
306 |
val xs = rev (#1 (fold_map Name.variant (rev (map #2 bs)) names));
|
wenzelm@43156
|
307 |
fun subst (((b, T), _), x') = (Free (b, T), Syntax_Trans.mark_boundT (x', T));
|
wenzelm@16985
|
308 |
in Term.subst_atomic (ListPair.map subst (bs, xs)) t end;
|
wenzelm@16985
|
309 |
|
boehmes@35979
|
310 |
fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
|
boehmes@35979
|
311 |
Syntax.string_of_term ctxt
|
wenzelm@41136
|
312 |
(if Config.get ctxt simp_debug then t else show_bounds ss t));
|
boehmes@35979
|
313 |
|
wenzelm@17705
|
314 |
in
|
wenzelm@17705
|
315 |
|
boehmes@35979
|
316 |
fun print_term_global ss warn a thy t =
|
wenzelm@43231
|
317 |
print_term ss warn (K a) t (Proof_Context.init_global thy);
|
wenzelm@16985
|
318 |
|
wenzelm@41136
|
319 |
fun debug warn a ss = if_enabled ss simp_debug (fn _ => prnt ss warn (a ()));
|
wenzelm@41136
|
320 |
fun trace warn a ss = if_enabled ss simp_trace (fn _ => prnt ss warn (a ()));
|
boehmes@35979
|
321 |
|
wenzelm@41136
|
322 |
fun debug_term warn a ss t = if_enabled ss simp_debug (print_term ss warn a t);
|
wenzelm@41136
|
323 |
fun trace_term warn a ss t = if_enabled ss simp_trace (print_term ss warn a t);
|
wenzelm@16985
|
324 |
|
wenzelm@16985
|
325 |
fun trace_cterm warn a ss ct =
|
wenzelm@41136
|
326 |
if_enabled ss simp_trace (print_term ss warn a (Thm.term_of ct));
|
wenzelm@16985
|
327 |
|
wenzelm@16985
|
328 |
fun trace_thm a ss th =
|
wenzelm@41136
|
329 |
if_enabled ss simp_trace (print_term ss false a (Thm.full_prop_of th));
|
wenzelm@16985
|
330 |
|
wenzelm@16985
|
331 |
fun trace_named_thm a ss (th, name) =
|
wenzelm@41136
|
332 |
if_enabled ss simp_trace (print_term ss false
|
boehmes@35979
|
333 |
(fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
|
boehmes@35979
|
334 |
(Thm.full_prop_of th));
|
wenzelm@16985
|
335 |
|
wenzelm@22892
|
336 |
fun warn_thm a ss th =
|
boehmes@35979
|
337 |
print_term_global ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th);
|
wenzelm@16985
|
338 |
|
wenzelm@39080
|
339 |
fun cond_warn_thm a ss th = if_visible ss (fn () => warn_thm a ss th) ();
|
wenzelm@20028
|
340 |
|
wenzelm@16985
|
341 |
end;
|
wenzelm@16985
|
342 |
|
wenzelm@16985
|
343 |
|
wenzelm@15023
|
344 |
|
wenzelm@15023
|
345 |
(** simpset operations **)
|
wenzelm@15023
|
346 |
|
wenzelm@17882
|
347 |
(* context *)
|
wenzelm@15023
|
348 |
|
wenzelm@17614
|
349 |
fun eq_bound (x: string, (y, _)) = x = y;
|
wenzelm@17614
|
350 |
|
wenzelm@22892
|
351 |
fun add_bound bound = map_simpset1 (fn (rules, prems, (count, bounds), depth, context) =>
|
wenzelm@22892
|
352 |
(rules, prems, (count + 1, bound :: bounds), depth, context));
|
wenzelm@16985
|
353 |
|
wenzelm@22892
|
354 |
fun add_prems ths = map_simpset1 (fn (rules, prems, bounds, depth, context) =>
|
wenzelm@22892
|
355 |
(rules, ths @ prems, bounds, depth, context));
|
wenzelm@15023
|
356 |
|
wenzelm@22892
|
357 |
fun inherit_context (Simpset ({bounds, depth, context, ...}, _)) =
|
wenzelm@22892
|
358 |
map_simpset1 (fn (rules, prems, _, _, _) => (rules, prems, bounds, depth, context));
|
wenzelm@17882
|
359 |
|
wenzelm@17882
|
360 |
fun the_context (Simpset ({context = SOME ctxt, ...}, _)) = ctxt
|
wenzelm@17882
|
361 |
| the_context _ = raise Fail "Simplifier: no proof context in simpset";
|
wenzelm@17882
|
362 |
|
wenzelm@17897
|
363 |
fun context ctxt =
|
wenzelm@22892
|
364 |
map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt));
|
wenzelm@17882
|
365 |
|
wenzelm@43231
|
366 |
val global_context = context o Proof_Context.init_global;
|
wenzelm@17897
|
367 |
|
wenzelm@27312
|
368 |
fun activate_context thy ss =
|
wenzelm@27312
|
369 |
let
|
wenzelm@27312
|
370 |
val ctxt = the_context ss;
|
wenzelm@36577
|
371 |
val ctxt' = ctxt
|
wenzelm@43231
|
372 |
|> Context.raw_transfer (Theory.merge (thy, Proof_Context.theory_of ctxt))
|
wenzelm@36577
|
373 |
|> Context_Position.set_visible false;
|
wenzelm@27312
|
374 |
in context ctxt' ss end;
|
wenzelm@17897
|
375 |
|
wenzelm@36577
|
376 |
fun with_context ctxt f ss = inherit_context ss (f (context ctxt ss));
|
wenzelm@36577
|
377 |
|
wenzelm@17897
|
378 |
|
wenzelm@20028
|
379 |
(* maintain simp rules *)
|
wenzelm@15023
|
380 |
|
wenzelm@20546
|
381 |
(* FIXME: it seems that the conditions on extra variables are too liberal if
|
wenzelm@20546
|
382 |
prems are nonempty: does solving the prems really guarantee instantiation of
|
wenzelm@20546
|
383 |
all its Vars? Better: a dynamic check each time a rule is applied.
|
wenzelm@20546
|
384 |
*)
|
wenzelm@20546
|
385 |
fun rewrite_rule_extra_vars prems elhs erhs =
|
wenzelm@20546
|
386 |
let
|
wenzelm@20546
|
387 |
val elhss = elhs :: prems;
|
wenzelm@20546
|
388 |
val tvars = fold Term.add_tvars elhss [];
|
wenzelm@20546
|
389 |
val vars = fold Term.add_vars elhss [];
|
wenzelm@20546
|
390 |
in
|
wenzelm@20546
|
391 |
erhs |> Term.exists_type (Term.exists_subtype
|
wenzelm@20546
|
392 |
(fn TVar v => not (member (op =) tvars v) | _ => false)) orelse
|
wenzelm@20546
|
393 |
erhs |> Term.exists_subterm
|
wenzelm@20546
|
394 |
(fn Var v => not (member (op =) vars v) | _ => false)
|
wenzelm@20546
|
395 |
end;
|
wenzelm@20546
|
396 |
|
wenzelm@20546
|
397 |
fun rrule_extra_vars elhs thm =
|
wenzelm@20546
|
398 |
rewrite_rule_extra_vars [] (term_of elhs) (Thm.full_prop_of thm);
|
wenzelm@20546
|
399 |
|
wenzelm@15023
|
400 |
fun mk_rrule2 {thm, name, lhs, elhs, perm} =
|
wenzelm@15023
|
401 |
let
|
wenzelm@20546
|
402 |
val t = term_of elhs;
|
wenzelm@20546
|
403 |
val fo = Pattern.first_order t orelse not (Pattern.pattern t);
|
wenzelm@20546
|
404 |
val extra = rrule_extra_vars elhs thm;
|
wenzelm@20546
|
405 |
in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end;
|
wenzelm@15023
|
406 |
|
wenzelm@20028
|
407 |
fun del_rrule (rrule as {thm, elhs, ...}) ss =
|
wenzelm@22892
|
408 |
ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
|
wenzelm@22892
|
409 |
(Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, bounds, depth, context))
|
wenzelm@20028
|
410 |
handle Net.DELETE => (cond_warn_thm "Rewrite rule not in simpset:" ss thm; ss);
|
wenzelm@20028
|
411 |
|
wenzelm@32804
|
412 |
fun insert_rrule (rrule as {thm, name, ...}) ss =
|
wenzelm@22254
|
413 |
(trace_named_thm (fn () => "Adding rewrite rule") ss (thm, name);
|
wenzelm@22892
|
414 |
ss |> map_simpset1 (fn (rules, prems, bounds, depth, context) =>
|
wenzelm@15023
|
415 |
let
|
wenzelm@15023
|
416 |
val rrule2 as {elhs, ...} = mk_rrule2 rrule;
|
wenzelm@16807
|
417 |
val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules;
|
wenzelm@22892
|
418 |
in (rules', prems, bounds, depth, context) end)
|
wenzelm@20028
|
419 |
handle Net.INSERT => (cond_warn_thm "Ignoring duplicate rewrite rule:" ss thm; ss));
|
berghofe@10413
|
420 |
|
berghofe@10413
|
421 |
fun vperm (Var _, Var _) = true
|
berghofe@10413
|
422 |
| vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t)
|
berghofe@10413
|
423 |
| vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2)
|
berghofe@10413
|
424 |
| vperm (t, u) = (t = u);
|
berghofe@10413
|
425 |
|
berghofe@10413
|
426 |
fun var_perm (t, u) =
|
haftmann@33038
|
427 |
vperm (t, u) andalso eq_set (op =) (Term.add_vars t [], Term.add_vars u []);
|
berghofe@10413
|
428 |
|
wenzelm@15023
|
429 |
(*simple test for looping rewrite rules and stupid orientations*)
|
wenzelm@18208
|
430 |
fun default_reorient thy prems lhs rhs =
|
wenzelm@15023
|
431 |
rewrite_rule_extra_vars prems lhs rhs
|
wenzelm@15023
|
432 |
orelse
|
wenzelm@15023
|
433 |
is_Var (head_of lhs)
|
wenzelm@15023
|
434 |
orelse
|
nipkow@16305
|
435 |
(* turns t = x around, which causes a headache if x is a local variable -
|
nipkow@16305
|
436 |
usually it is very useful :-(
|
nipkow@16305
|
437 |
is_Free rhs andalso not(is_Free lhs) andalso not(Logic.occs(rhs,lhs))
|
nipkow@16305
|
438 |
andalso not(exists_subterm is_Var lhs)
|
nipkow@16305
|
439 |
orelse
|
nipkow@16305
|
440 |
*)
|
wenzelm@16842
|
441 |
exists (fn t => Logic.occs (lhs, t)) (rhs :: prems)
|
wenzelm@15023
|
442 |
orelse
|
wenzelm@17203
|
443 |
null prems andalso Pattern.matches thy (lhs, rhs)
|
berghofe@10413
|
444 |
(*the condition "null prems" is necessary because conditional rewrites
|
berghofe@10413
|
445 |
with extra variables in the conditions may terminate although
|
wenzelm@15023
|
446 |
the rhs is an instance of the lhs; example: ?m < ?n ==> f(?n) == f(?m)*)
|
wenzelm@15023
|
447 |
orelse
|
wenzelm@15023
|
448 |
is_Const lhs andalso not (is_Const rhs);
|
berghofe@10413
|
449 |
|
berghofe@10413
|
450 |
fun decomp_simp thm =
|
wenzelm@15023
|
451 |
let
|
wenzelm@26626
|
452 |
val thy = Thm.theory_of_thm thm;
|
wenzelm@26626
|
453 |
val prop = Thm.prop_of thm;
|
wenzelm@15023
|
454 |
val prems = Logic.strip_imp_prems prop;
|
wenzelm@15023
|
455 |
val concl = Drule.strip_imp_concl (Thm.cprop_of thm);
|
wenzelm@22902
|
456 |
val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
|
wenzelm@15023
|
457 |
raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm);
|
wenzelm@20579
|
458 |
val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
|
wenzelm@16665
|
459 |
val elhs = if term_of elhs aconv term_of lhs then lhs else elhs; (*share identical copies*)
|
wenzelm@18929
|
460 |
val erhs = Envir.eta_contract (term_of rhs);
|
wenzelm@15023
|
461 |
val perm =
|
wenzelm@15023
|
462 |
var_perm (term_of elhs, erhs) andalso
|
wenzelm@15023
|
463 |
not (term_of elhs aconv erhs) andalso
|
wenzelm@15023
|
464 |
not (is_Var (term_of elhs));
|
wenzelm@16458
|
465 |
in (thy, prems, term_of lhs, elhs, term_of rhs, perm) end;
|
berghofe@10413
|
466 |
|
wenzelm@12783
|
467 |
fun decomp_simp' thm =
|
wenzelm@12979
|
468 |
let val (_, _, lhs, _, rhs, _) = decomp_simp thm in
|
wenzelm@12783
|
469 |
if Thm.nprems_of thm > 0 then raise SIMPLIFIER ("Bad conditional rewrite rule", thm)
|
wenzelm@12979
|
470 |
else (lhs, rhs)
|
wenzelm@12783
|
471 |
end;
|
wenzelm@12783
|
472 |
|
wenzelm@36543
|
473 |
fun mk_eq_True (ss as Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) =
|
wenzelm@36543
|
474 |
(case mk_eq_True ss thm of
|
skalberg@15531
|
475 |
NONE => []
|
skalberg@15531
|
476 |
| SOME eq_True =>
|
wenzelm@20546
|
477 |
let
|
wenzelm@20546
|
478 |
val (_, _, lhs, elhs, _, _) = decomp_simp eq_True;
|
wenzelm@15023
|
479 |
in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end);
|
berghofe@10413
|
480 |
|
wenzelm@15023
|
481 |
(*create the rewrite rule and possibly also the eq_True variant,
|
wenzelm@15023
|
482 |
in case there are extra vars on the rhs*)
|
wenzelm@15023
|
483 |
fun rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm2) =
|
wenzelm@15023
|
484 |
let val rrule = {thm = thm, name = name, lhs = lhs, elhs = elhs, perm = false} in
|
wenzelm@20546
|
485 |
if rewrite_rule_extra_vars [] lhs rhs then
|
wenzelm@20546
|
486 |
mk_eq_True ss (thm2, name) @ [rrule]
|
wenzelm@20546
|
487 |
else [rrule]
|
berghofe@10413
|
488 |
end;
|
berghofe@10413
|
489 |
|
wenzelm@15023
|
490 |
fun mk_rrule ss (thm, name) =
|
wenzelm@15023
|
491 |
let val (_, prems, lhs, elhs, rhs, perm) = decomp_simp thm in
|
wenzelm@15023
|
492 |
if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
|
wenzelm@15023
|
493 |
else
|
wenzelm@15023
|
494 |
(*weak test for loops*)
|
wenzelm@15023
|
495 |
if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs)
|
wenzelm@15023
|
496 |
then mk_eq_True ss (thm, name)
|
wenzelm@15023
|
497 |
else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
|
berghofe@10413
|
498 |
end;
|
berghofe@10413
|
499 |
|
wenzelm@15023
|
500 |
fun orient_rrule ss (thm, name) =
|
wenzelm@18208
|
501 |
let
|
wenzelm@18208
|
502 |
val (thy, prems, lhs, elhs, rhs, perm) = decomp_simp thm;
|
wenzelm@18208
|
503 |
val Simpset (_, {mk_rews = {reorient, mk_sym, ...}, ...}) = ss;
|
wenzelm@18208
|
504 |
in
|
wenzelm@15023
|
505 |
if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
|
wenzelm@16458
|
506 |
else if reorient thy prems lhs rhs then
|
wenzelm@16458
|
507 |
if reorient thy prems rhs lhs
|
wenzelm@15023
|
508 |
then mk_eq_True ss (thm, name)
|
wenzelm@15023
|
509 |
else
|
wenzelm@36543
|
510 |
(case mk_sym ss thm of
|
wenzelm@18208
|
511 |
NONE => []
|
wenzelm@18208
|
512 |
| SOME thm' =>
|
wenzelm@18208
|
513 |
let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm'
|
wenzelm@18208
|
514 |
in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end)
|
wenzelm@15023
|
515 |
else rrule_eq_True (thm, name, lhs, elhs, rhs, ss, thm)
|
berghofe@10413
|
516 |
end;
|
berghofe@10413
|
517 |
|
wenzelm@36543
|
518 |
fun extract_rews (ss as Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
|
wenzelm@36543
|
519 |
maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk ss thm)) thms;
|
berghofe@10413
|
520 |
|
wenzelm@15023
|
521 |
fun extract_safe_rrules (ss, thm) =
|
wenzelm@19482
|
522 |
maps (orient_rrule ss) (extract_rews (ss, [thm]));
|
berghofe@10413
|
523 |
|
wenzelm@20028
|
524 |
|
wenzelm@20028
|
525 |
(* add/del rules explicitly *)
|
wenzelm@20028
|
526 |
|
wenzelm@20028
|
527 |
fun comb_simps comb mk_rrule (ss, thms) =
|
wenzelm@20028
|
528 |
let
|
wenzelm@20028
|
529 |
val rews = extract_rews (ss, thms);
|
wenzelm@20028
|
530 |
in fold (fold comb o mk_rrule) rews ss end;
|
wenzelm@20028
|
531 |
|
wenzelm@15023
|
532 |
fun ss addsimps thms =
|
wenzelm@20028
|
533 |
comb_simps insert_rrule (mk_rrule ss) (ss, thms);
|
berghofe@10413
|
534 |
|
wenzelm@15023
|
535 |
fun ss delsimps thms =
|
wenzelm@20028
|
536 |
comb_simps del_rrule (map mk_rrule2 o mk_rrule ss) (ss, thms);
|
berghofe@10413
|
537 |
|
haftmann@27558
|
538 |
fun add_simp thm ss = ss addsimps [thm];
|
haftmann@27558
|
539 |
fun del_simp thm ss = ss delsimps [thm];
|
berghofe@10413
|
540 |
|
wenzelm@30321
|
541 |
|
wenzelm@15023
|
542 |
(* congs *)
|
berghofe@10413
|
543 |
|
skalberg@15531
|
544 |
fun cong_name (Const (a, _)) = SOME a
|
skalberg@15531
|
545 |
| cong_name (Free (a, _)) = SOME ("Free: " ^ a)
|
skalberg@15531
|
546 |
| cong_name _ = NONE;
|
ballarin@13835
|
547 |
|
wenzelm@15023
|
548 |
local
|
wenzelm@15023
|
549 |
|
wenzelm@15023
|
550 |
fun is_full_cong_prems [] [] = true
|
wenzelm@15023
|
551 |
| is_full_cong_prems [] _ = false
|
wenzelm@15023
|
552 |
| is_full_cong_prems (p :: prems) varpairs =
|
wenzelm@15023
|
553 |
(case Logic.strip_assums_concl p of
|
wenzelm@15023
|
554 |
Const ("==", _) $ lhs $ rhs =>
|
wenzelm@15023
|
555 |
let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
|
wenzelm@15023
|
556 |
is_Var x andalso forall is_Bound xs andalso
|
haftmann@20972
|
557 |
not (has_duplicates (op =) xs) andalso xs = ys andalso
|
wenzelm@20671
|
558 |
member (op =) varpairs (x, y) andalso
|
wenzelm@19303
|
559 |
is_full_cong_prems prems (remove (op =) (x, y) varpairs)
|
wenzelm@15023
|
560 |
end
|
wenzelm@15023
|
561 |
| _ => false);
|
wenzelm@15023
|
562 |
|
wenzelm@15023
|
563 |
fun is_full_cong thm =
|
berghofe@10413
|
564 |
let
|
wenzelm@15023
|
565 |
val prems = prems_of thm and concl = concl_of thm;
|
wenzelm@15023
|
566 |
val (lhs, rhs) = Logic.dest_equals concl;
|
wenzelm@15023
|
567 |
val (f, xs) = strip_comb lhs and (g, ys) = strip_comb rhs;
|
berghofe@10413
|
568 |
in
|
haftmann@20972
|
569 |
f = g andalso not (has_duplicates (op =) (xs @ ys)) andalso length xs = length ys andalso
|
wenzelm@15023
|
570 |
is_full_cong_prems prems (xs ~~ ys)
|
berghofe@10413
|
571 |
end;
|
berghofe@10413
|
572 |
|
wenzelm@15023
|
573 |
fun add_cong (ss, thm) = ss |>
|
wenzelm@15023
|
574 |
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
|
wenzelm@15023
|
575 |
let
|
wenzelm@22902
|
576 |
val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
|
wenzelm@15023
|
577 |
handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
|
wenzelm@18929
|
578 |
(*val lhs = Envir.eta_contract lhs;*)
|
wenzelm@20057
|
579 |
val a = the (cong_name (head_of (term_of lhs))) handle Option.Option =>
|
wenzelm@15023
|
580 |
raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
|
haftmann@22221
|
581 |
val (xs, weak) = congs;
|
wenzelm@39080
|
582 |
val _ =
|
wenzelm@39080
|
583 |
if AList.defined (op =) xs a
|
wenzelm@39080
|
584 |
then if_visible ss warning ("Overwriting congruence rule for " ^ quote a)
|
haftmann@22221
|
585 |
else ();
|
krauss@30908
|
586 |
val xs' = AList.update (op =) (a, thm) xs;
|
haftmann@22221
|
587 |
val weak' = if is_full_cong thm then weak else a :: weak;
|
haftmann@22221
|
588 |
in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
|
berghofe@10413
|
589 |
|
wenzelm@15023
|
590 |
fun del_cong (ss, thm) = ss |>
|
wenzelm@15023
|
591 |
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
|
wenzelm@15023
|
592 |
let
|
wenzelm@15023
|
593 |
val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
|
wenzelm@15023
|
594 |
raise SIMPLIFIER ("Congruence not a meta-equality", thm);
|
wenzelm@18929
|
595 |
(*val lhs = Envir.eta_contract lhs;*)
|
wenzelm@20057
|
596 |
val a = the (cong_name (head_of lhs)) handle Option.Option =>
|
wenzelm@15023
|
597 |
raise SIMPLIFIER ("Congruence must start with a constant", thm);
|
haftmann@22221
|
598 |
val (xs, _) = congs;
|
haftmann@22221
|
599 |
val xs' = filter_out (fn (x : string, _) => x = a) xs;
|
krauss@30908
|
600 |
val weak' = xs' |> map_filter (fn (a, thm) =>
|
skalberg@15531
|
601 |
if is_full_cong thm then NONE else SOME a);
|
haftmann@22221
|
602 |
in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
|
berghofe@10413
|
603 |
|
wenzelm@36543
|
604 |
fun mk_cong (ss as Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f ss;
|
berghofe@10413
|
605 |
|
wenzelm@15023
|
606 |
in
|
berghofe@10413
|
607 |
|
skalberg@15570
|
608 |
val (op addeqcongs) = Library.foldl add_cong;
|
skalberg@15570
|
609 |
val (op deleqcongs) = Library.foldl del_cong;
|
berghofe@10413
|
610 |
|
wenzelm@15023
|
611 |
fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs;
|
wenzelm@15023
|
612 |
fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs;
|
berghofe@10413
|
613 |
|
wenzelm@15023
|
614 |
end;
|
berghofe@10413
|
615 |
|
berghofe@10413
|
616 |
|
wenzelm@15023
|
617 |
(* simprocs *)
|
berghofe@10413
|
618 |
|
wenzelm@22234
|
619 |
datatype simproc =
|
wenzelm@22234
|
620 |
Simproc of
|
wenzelm@22234
|
621 |
{name: string,
|
wenzelm@22234
|
622 |
lhss: cterm list,
|
wenzelm@22234
|
623 |
proc: morphism -> simpset -> cterm -> thm option,
|
wenzelm@22234
|
624 |
id: stamp * thm list};
|
wenzelm@22008
|
625 |
|
wenzelm@22234
|
626 |
fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
|
wenzelm@22234
|
627 |
|
wenzelm@22234
|
628 |
fun morph_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
|
wenzelm@22234
|
629 |
Simproc
|
wenzelm@22234
|
630 |
{name = name,
|
wenzelm@22234
|
631 |
lhss = map (Morphism.cterm phi) lhss,
|
wenzelm@22669
|
632 |
proc = Morphism.transform phi proc,
|
wenzelm@22234
|
633 |
id = (s, Morphism.fact phi ths)};
|
wenzelm@22234
|
634 |
|
wenzelm@22234
|
635 |
fun make_simproc {name, lhss, proc, identifier} =
|
wenzelm@22234
|
636 |
Simproc {name = name, lhss = lhss, proc = proc, id = (stamp (), identifier)};
|
wenzelm@22008
|
637 |
|
wenzelm@22008
|
638 |
fun mk_simproc name lhss proc =
|
wenzelm@22234
|
639 |
make_simproc {name = name, lhss = lhss, proc = fn _ => fn ss => fn ct =>
|
wenzelm@43231
|
640 |
proc (Proof_Context.theory_of (the_context ss)) ss (Thm.term_of ct), identifier = []};
|
wenzelm@22008
|
641 |
|
wenzelm@35845
|
642 |
(* FIXME avoid global thy and Logic.varify_global *)
|
wenzelm@38963
|
643 |
fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
|
wenzelm@38963
|
644 |
fun simproc_global thy name = simproc_global_i thy name o map (Syntax.read_term_global thy);
|
wenzelm@22008
|
645 |
|
wenzelm@22008
|
646 |
|
wenzelm@15023
|
647 |
local
|
berghofe@10413
|
648 |
|
wenzelm@16985
|
649 |
fun add_proc (proc as Proc {name, lhs, ...}) ss =
|
wenzelm@22254
|
650 |
(trace_cterm false (fn () => "Adding simplification procedure " ^ quote name ^ " for") ss lhs;
|
wenzelm@15023
|
651 |
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
|
wenzelm@16807
|
652 |
(congs, Net.insert_term eq_proc (term_of lhs, proc) procs,
|
wenzelm@15023
|
653 |
mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
|
wenzelm@15023
|
654 |
handle Net.INSERT =>
|
wenzelm@39080
|
655 |
(if_visible ss warning ("Ignoring duplicate simplification procedure " ^ quote name); ss));
|
berghofe@10413
|
656 |
|
wenzelm@16985
|
657 |
fun del_proc (proc as Proc {name, lhs, ...}) ss =
|
wenzelm@15023
|
658 |
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
|
wenzelm@16807
|
659 |
(congs, Net.delete_term eq_proc (term_of lhs, proc) procs,
|
wenzelm@15023
|
660 |
mk_rews, termless, subgoal_tac, loop_tacs, solvers)) ss
|
wenzelm@15023
|
661 |
handle Net.DELETE =>
|
wenzelm@39080
|
662 |
(if_visible ss warning ("Simplification procedure " ^ quote name ^ " not in simpset"); ss);
|
berghofe@10413
|
663 |
|
wenzelm@22234
|
664 |
fun prep_procs (Simproc {name, lhss, proc, id}) =
|
wenzelm@22669
|
665 |
lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, id = id});
|
wenzelm@22234
|
666 |
|
wenzelm@15023
|
667 |
in
|
berghofe@10413
|
668 |
|
wenzelm@22234
|
669 |
fun ss addsimprocs ps = fold (fold add_proc o prep_procs) ps ss;
|
wenzelm@22234
|
670 |
fun ss delsimprocs ps = fold (fold del_proc o prep_procs) ps ss;
|
berghofe@10413
|
671 |
|
wenzelm@15023
|
672 |
end;
|
berghofe@10413
|
673 |
|
berghofe@10413
|
674 |
|
berghofe@10413
|
675 |
(* mk_rews *)
|
berghofe@10413
|
676 |
|
wenzelm@15023
|
677 |
local
|
berghofe@10413
|
678 |
|
wenzelm@18208
|
679 |
fun map_mk_rews f = map_simpset2 (fn (congs, procs, {mk, mk_cong, mk_sym, mk_eq_True, reorient},
|
wenzelm@15023
|
680 |
termless, subgoal_tac, loop_tacs, solvers) =>
|
wenzelm@18208
|
681 |
let
|
wenzelm@18208
|
682 |
val (mk', mk_cong', mk_sym', mk_eq_True', reorient') =
|
wenzelm@18208
|
683 |
f (mk, mk_cong, mk_sym, mk_eq_True, reorient);
|
wenzelm@18208
|
684 |
val mk_rews' = {mk = mk', mk_cong = mk_cong', mk_sym = mk_sym', mk_eq_True = mk_eq_True',
|
wenzelm@18208
|
685 |
reorient = reorient'};
|
wenzelm@18208
|
686 |
in (congs, procs, mk_rews', termless, subgoal_tac, loop_tacs, solvers) end);
|
berghofe@10413
|
687 |
|
wenzelm@15023
|
688 |
in
|
berghofe@10413
|
689 |
|
wenzelm@36543
|
690 |
fun mksimps (ss as Simpset (_, {mk_rews = {mk, ...}, ...})) = mk ss;
|
wenzelm@30321
|
691 |
|
wenzelm@18208
|
692 |
fun ss setmksimps mk = ss |> map_mk_rews (fn (_, mk_cong, mk_sym, mk_eq_True, reorient) =>
|
wenzelm@18208
|
693 |
(mk, mk_cong, mk_sym, mk_eq_True, reorient));
|
wenzelm@15023
|
694 |
|
wenzelm@18208
|
695 |
fun ss setmkcong mk_cong = ss |> map_mk_rews (fn (mk, _, mk_sym, mk_eq_True, reorient) =>
|
wenzelm@18208
|
696 |
(mk, mk_cong, mk_sym, mk_eq_True, reorient));
|
wenzelm@15023
|
697 |
|
wenzelm@18208
|
698 |
fun ss setmksym mk_sym = ss |> map_mk_rews (fn (mk, mk_cong, _, mk_eq_True, reorient) =>
|
wenzelm@18208
|
699 |
(mk, mk_cong, mk_sym, mk_eq_True, reorient));
|
wenzelm@15023
|
700 |
|
wenzelm@18208
|
701 |
fun ss setmkeqTrue mk_eq_True = ss |> map_mk_rews (fn (mk, mk_cong, mk_sym, _, reorient) =>
|
wenzelm@18208
|
702 |
(mk, mk_cong, mk_sym, mk_eq_True, reorient));
|
wenzelm@18208
|
703 |
|
wenzelm@18208
|
704 |
fun set_reorient reorient = map_mk_rews (fn (mk, mk_cong, mk_sym, mk_eq_True, _) =>
|
wenzelm@18208
|
705 |
(mk, mk_cong, mk_sym, mk_eq_True, reorient));
|
wenzelm@15023
|
706 |
|
wenzelm@15023
|
707 |
end;
|
wenzelm@15023
|
708 |
|
skalberg@14242
|
709 |
|
berghofe@10413
|
710 |
(* termless *)
|
berghofe@10413
|
711 |
|
wenzelm@15023
|
712 |
fun ss settermless termless = ss |>
|
wenzelm@15023
|
713 |
map_simpset2 (fn (congs, procs, mk_rews, _, subgoal_tac, loop_tacs, solvers) =>
|
wenzelm@15023
|
714 |
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
|
berghofe@10413
|
715 |
|
berghofe@10413
|
716 |
|
wenzelm@15023
|
717 |
(* tactics *)
|
berghofe@10413
|
718 |
|
wenzelm@15023
|
719 |
fun ss setsubgoaler subgoal_tac = ss |>
|
wenzelm@15023
|
720 |
map_simpset2 (fn (congs, procs, mk_rews, termless, _, loop_tacs, solvers) =>
|
wenzelm@15023
|
721 |
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers));
|
skalberg@15006
|
722 |
|
wenzelm@17882
|
723 |
fun ss setloop' tac = ss |>
|
wenzelm@15023
|
724 |
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, _, solvers) =>
|
wenzelm@15023
|
725 |
(congs, procs, mk_rews, termless, subgoal_tac, [("", tac)], solvers));
|
skalberg@15006
|
726 |
|
wenzelm@17882
|
727 |
fun ss setloop tac = ss setloop' (K tac);
|
wenzelm@17882
|
728 |
|
wenzelm@17882
|
729 |
fun ss addloop' (name, tac) = ss |>
|
wenzelm@15023
|
730 |
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
|
wenzelm@15023
|
731 |
(congs, procs, mk_rews, termless, subgoal_tac,
|
wenzelm@39080
|
732 |
(if AList.defined (op =) loop_tacs name
|
wenzelm@39080
|
733 |
then if_visible ss warning ("Overwriting looper " ^ quote name)
|
wenzelm@39080
|
734 |
else (); AList.update (op =) (name, tac) loop_tacs), solvers));
|
skalberg@15011
|
735 |
|
wenzelm@17882
|
736 |
fun ss addloop (name, tac) = ss addloop' (name, K tac);
|
wenzelm@17882
|
737 |
|
wenzelm@15023
|
738 |
fun ss delloop name = ss |>
|
wenzelm@15023
|
739 |
map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
|
haftmann@21286
|
740 |
(congs, procs, mk_rews, termless, subgoal_tac,
|
wenzelm@39080
|
741 |
(if AList.defined (op =) loop_tacs name then ()
|
wenzelm@39080
|
742 |
else if_visible ss warning ("No such looper in simpset: " ^ quote name);
|
wenzelm@39080
|
743 |
AList.delete (op =) name loop_tacs), solvers));
|
skalberg@15006
|
744 |
|
wenzelm@15023
|
745 |
fun ss setSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
|
wenzelm@15023
|
746 |
subgoal_tac, loop_tacs, (unsafe_solvers, _)) =>
|
wenzelm@15023
|
747 |
(congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, (unsafe_solvers, [solver])));
|
skalberg@15006
|
748 |
|
wenzelm@15023
|
749 |
fun ss addSSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
|
wenzelm@15023
|
750 |
subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
|
haftmann@22717
|
751 |
subgoal_tac, loop_tacs, (unsafe_solvers, insert eq_solver solver solvers)));
|
skalberg@15006
|
752 |
|
wenzelm@15023
|
753 |
fun ss setSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
|
wenzelm@15023
|
754 |
subgoal_tac, loop_tacs, (_, solvers)) => (congs, procs, mk_rews, termless,
|
wenzelm@15023
|
755 |
subgoal_tac, loop_tacs, ([solver], solvers)));
|
skalberg@15006
|
756 |
|
wenzelm@15023
|
757 |
fun ss addSolver solver = ss |> map_simpset2 (fn (congs, procs, mk_rews, termless,
|
wenzelm@15023
|
758 |
subgoal_tac, loop_tacs, (unsafe_solvers, solvers)) => (congs, procs, mk_rews, termless,
|
haftmann@22717
|
759 |
subgoal_tac, loop_tacs, (insert eq_solver solver unsafe_solvers, solvers)));
|
skalberg@15006
|
760 |
|
wenzelm@15023
|
761 |
fun set_solvers solvers = map_simpset2 (fn (congs, procs, mk_rews, termless,
|
wenzelm@15023
|
762 |
subgoal_tac, loop_tacs, _) => (congs, procs, mk_rews, termless,
|
wenzelm@15023
|
763 |
subgoal_tac, loop_tacs, (solvers, solvers)));
|
skalberg@15006
|
764 |
|
skalberg@15006
|
765 |
|
wenzelm@18208
|
766 |
(* empty *)
|
wenzelm@18208
|
767 |
|
wenzelm@18208
|
768 |
fun init_ss mk_rews termless subgoal_tac solvers =
|
wenzelm@32738
|
769 |
make_simpset ((Net.empty, [], (0, []), (0, Unsynchronized.ref false), NONE),
|
wenzelm@18208
|
770 |
(([], []), Net.empty, mk_rews, termless, subgoal_tac, [], solvers));
|
wenzelm@18208
|
771 |
|
wenzelm@18208
|
772 |
fun clear_ss (ss as Simpset (_, {mk_rews, termless, subgoal_tac, solvers, ...})) =
|
wenzelm@18208
|
773 |
init_ss mk_rews termless subgoal_tac solvers
|
wenzelm@18208
|
774 |
|> inherit_context ss;
|
wenzelm@18208
|
775 |
|
wenzelm@36543
|
776 |
val empty_ss =
|
wenzelm@36543
|
777 |
init_ss
|
wenzelm@36543
|
778 |
{mk = fn _ => fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [],
|
wenzelm@36543
|
779 |
mk_cong = K I,
|
wenzelm@36543
|
780 |
mk_sym = K (SOME o Drule.symmetric_fun),
|
wenzelm@36543
|
781 |
mk_eq_True = K (K NONE),
|
wenzelm@36543
|
782 |
reorient = default_reorient}
|
wenzelm@36543
|
783 |
Term_Ord.termless (K (K no_tac)) ([], []);
|
wenzelm@18208
|
784 |
|
wenzelm@18208
|
785 |
|
wenzelm@18208
|
786 |
(* merge *) (*NOTE: ignores some fields of 2nd simpset*)
|
wenzelm@18208
|
787 |
|
wenzelm@18208
|
788 |
fun merge_ss (ss1, ss2) =
|
wenzelm@24358
|
789 |
if pointer_eq (ss1, ss2) then ss1
|
wenzelm@24358
|
790 |
else
|
wenzelm@24358
|
791 |
let
|
wenzelm@24358
|
792 |
val Simpset ({rules = rules1, prems = prems1, bounds = bounds1, depth = depth1, context = _},
|
wenzelm@24358
|
793 |
{congs = (congs1, weak1), procs = procs1, mk_rews, termless, subgoal_tac,
|
wenzelm@24358
|
794 |
loop_tacs = loop_tacs1, solvers = (unsafe_solvers1, solvers1)}) = ss1;
|
wenzelm@24358
|
795 |
val Simpset ({rules = rules2, prems = prems2, bounds = bounds2, depth = depth2, context = _},
|
wenzelm@24358
|
796 |
{congs = (congs2, weak2), procs = procs2, mk_rews = _, termless = _, subgoal_tac = _,
|
wenzelm@24358
|
797 |
loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
|
wenzelm@30356
|
798 |
|
wenzelm@24358
|
799 |
val rules' = Net.merge eq_rrule (rules1, rules2);
|
wenzelm@33520
|
800 |
val prems' = Thm.merge_thms (prems1, prems2);
|
wenzelm@24358
|
801 |
val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
|
wenzelm@24358
|
802 |
val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
|
wenzelm@31298
|
803 |
val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2);
|
wenzelm@24358
|
804 |
val weak' = merge (op =) (weak1, weak2);
|
wenzelm@24358
|
805 |
val procs' = Net.merge eq_proc (procs1, procs2);
|
wenzelm@24358
|
806 |
val loop_tacs' = AList.merge (op =) (K true) (loop_tacs1, loop_tacs2);
|
wenzelm@24358
|
807 |
val unsafe_solvers' = merge eq_solver (unsafe_solvers1, unsafe_solvers2);
|
wenzelm@24358
|
808 |
val solvers' = merge eq_solver (solvers1, solvers2);
|
wenzelm@24358
|
809 |
in
|
wenzelm@24358
|
810 |
make_simpset ((rules', prems', bounds', depth', NONE), ((congs', weak'), procs',
|
wenzelm@24358
|
811 |
mk_rews, termless, subgoal_tac, loop_tacs', (unsafe_solvers', solvers')))
|
wenzelm@24358
|
812 |
end;
|
wenzelm@18208
|
813 |
|
wenzelm@18208
|
814 |
|
wenzelm@30356
|
815 |
(* dest_ss *)
|
wenzelm@30356
|
816 |
|
wenzelm@30356
|
817 |
fun dest_ss (Simpset ({rules, ...}, {congs, procs, loop_tacs, solvers, ...})) =
|
wenzelm@30356
|
818 |
{simps = Net.entries rules
|
wenzelm@30356
|
819 |
|> map (fn {name, thm, ...} => (name, thm)),
|
wenzelm@30356
|
820 |
procs = Net.entries procs
|
wenzelm@30356
|
821 |
|> map (fn Proc {name, lhs, id, ...} => ((name, lhs), id))
|
wenzelm@30356
|
822 |
|> partition_eq (eq_snd eq_procid)
|
wenzelm@30356
|
823 |
|> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)),
|
krauss@30908
|
824 |
congs = #1 congs,
|
wenzelm@30356
|
825 |
weak_congs = #2 congs,
|
wenzelm@30356
|
826 |
loopers = map fst loop_tacs,
|
wenzelm@30356
|
827 |
unsafe_solvers = map solver_name (#1 solvers),
|
wenzelm@30356
|
828 |
safe_solvers = map solver_name (#2 solvers)};
|
wenzelm@30356
|
829 |
|
wenzelm@30356
|
830 |
|
skalberg@15006
|
831 |
|
berghofe@10413
|
832 |
(** rewriting **)
|
berghofe@10413
|
833 |
|
berghofe@10413
|
834 |
(*
|
berghofe@10413
|
835 |
Uses conversions, see:
|
berghofe@10413
|
836 |
L C Paulson, A higher-order implementation of rewriting,
|
berghofe@10413
|
837 |
Science of Computer Programming 3 (1983), pages 119-149.
|
berghofe@10413
|
838 |
*)
|
berghofe@10413
|
839 |
|
wenzelm@16985
|
840 |
fun check_conv msg ss thm thm' =
|
berghofe@10413
|
841 |
let
|
wenzelm@36944
|
842 |
val thm'' = Thm.transitive thm thm' handle THM _ =>
|
wenzelm@36944
|
843 |
Thm.transitive thm (Thm.transitive
|
wenzelm@36944
|
844 |
(Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
|
wenzelm@22254
|
845 |
in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
|
berghofe@10413
|
846 |
handle THM _ =>
|
wenzelm@26626
|
847 |
let
|
wenzelm@26626
|
848 |
val _ $ _ $ prop0 = Thm.prop_of thm;
|
wenzelm@26626
|
849 |
in
|
wenzelm@22254
|
850 |
trace_thm (fn () => "Proved wrong thm (Check subgoaler?)") ss thm';
|
boehmes@35979
|
851 |
trace_term false (fn () => "Should have proved:") ss prop0;
|
skalberg@15531
|
852 |
NONE
|
berghofe@10413
|
853 |
end;
|
berghofe@10413
|
854 |
|
berghofe@10413
|
855 |
|
berghofe@10413
|
856 |
(* mk_procrule *)
|
berghofe@10413
|
857 |
|
wenzelm@16985
|
858 |
fun mk_procrule ss thm =
|
wenzelm@15023
|
859 |
let val (_, prems, lhs, elhs, rhs, _) = decomp_simp thm in
|
wenzelm@15023
|
860 |
if rewrite_rule_extra_vars prems lhs rhs
|
wenzelm@39080
|
861 |
then (cond_warn_thm "Extra vars on rhs:" ss thm; [])
|
wenzelm@15023
|
862 |
else [mk_rrule2 {thm = thm, name = "", lhs = lhs, elhs = elhs, perm = false}]
|
berghofe@10413
|
863 |
end;
|
berghofe@10413
|
864 |
|
berghofe@10413
|
865 |
|
wenzelm@15023
|
866 |
(* rewritec: conversion to apply the meta simpset to a term *)
|
berghofe@10413
|
867 |
|
wenzelm@15023
|
868 |
(*Since the rewriting strategy is bottom-up, we avoid re-normalizing already
|
wenzelm@15023
|
869 |
normalized terms by carrying around the rhs of the rewrite rule just
|
wenzelm@15023
|
870 |
applied. This is called the `skeleton'. It is decomposed in parallel
|
wenzelm@15023
|
871 |
with the term. Once a Var is encountered, the corresponding term is
|
wenzelm@15023
|
872 |
already in normal form.
|
wenzelm@15023
|
873 |
skel0 is a dummy skeleton that is to enforce complete normalization.*)
|
wenzelm@15023
|
874 |
|
berghofe@10413
|
875 |
val skel0 = Bound 0;
|
berghofe@10413
|
876 |
|
wenzelm@15023
|
877 |
(*Use rhs as skeleton only if the lhs does not contain unnormalized bits.
|
wenzelm@15023
|
878 |
The latter may happen iff there are weak congruence rules for constants
|
wenzelm@15023
|
879 |
in the lhs.*)
|
berghofe@10413
|
880 |
|
wenzelm@15023
|
881 |
fun uncond_skel ((_, weak), (lhs, rhs)) =
|
wenzelm@15023
|
882 |
if null weak then rhs (*optimization*)
|
wenzelm@20671
|
883 |
else if exists_Const (member (op =) weak o #1) lhs then skel0
|
wenzelm@15023
|
884 |
else rhs;
|
wenzelm@15023
|
885 |
|
wenzelm@15023
|
886 |
(*Behaves like unconditional rule if rhs does not contain vars not in the lhs.
|
wenzelm@15023
|
887 |
Otherwise those vars may become instantiated with unnormalized terms
|
wenzelm@15023
|
888 |
while the premises are solved.*)
|
wenzelm@15023
|
889 |
|
wenzelm@32804
|
890 |
fun cond_skel (args as (_, (lhs, rhs))) =
|
haftmann@33038
|
891 |
if subset (op =) (Term.add_vars rhs [], Term.add_vars lhs []) then uncond_skel args
|
berghofe@10413
|
892 |
else skel0;
|
berghofe@10413
|
893 |
|
berghofe@10413
|
894 |
(*
|
wenzelm@15023
|
895 |
Rewriting -- we try in order:
|
berghofe@10413
|
896 |
(1) beta reduction
|
berghofe@10413
|
897 |
(2) unconditional rewrite rules
|
berghofe@10413
|
898 |
(3) conditional rewrite rules
|
berghofe@10413
|
899 |
(4) simplification procedures
|
berghofe@10413
|
900 |
|
berghofe@10413
|
901 |
IMPORTANT: rewrite rules must not introduce new Vars or TVars!
|
berghofe@10413
|
902 |
*)
|
berghofe@10413
|
903 |
|
wenzelm@16458
|
904 |
fun rewritec (prover, thyt, maxt) ss t =
|
berghofe@10413
|
905 |
let
|
wenzelm@24124
|
906 |
val ctxt = the_context ss;
|
wenzelm@15023
|
907 |
val Simpset ({rules, ...}, {congs, procs, termless, ...}) = ss;
|
berghofe@10413
|
908 |
val eta_thm = Thm.eta_conversion t;
|
wenzelm@22902
|
909 |
val eta_t' = Thm.rhs_of eta_thm;
|
berghofe@10413
|
910 |
val eta_t = term_of eta_t';
|
wenzelm@20546
|
911 |
fun rew {thm, name, lhs, elhs, extra, fo, perm} =
|
berghofe@10413
|
912 |
let
|
wenzelm@32804
|
913 |
val prop = Thm.prop_of thm;
|
wenzelm@20546
|
914 |
val (rthm, elhs') =
|
wenzelm@20546
|
915 |
if maxt = ~1 orelse not extra then (thm, elhs)
|
wenzelm@22902
|
916 |
else (Thm.incr_indexes (maxt + 1) thm, Thm.incr_indexes_cterm (maxt + 1) elhs);
|
wenzelm@22902
|
917 |
val insts =
|
wenzelm@22902
|
918 |
if fo then Thm.first_order_match (elhs', eta_t')
|
wenzelm@22902
|
919 |
else Thm.match (elhs', eta_t');
|
berghofe@10413
|
920 |
val thm' = Thm.instantiate insts (Thm.rename_boundvars lhs eta_t rthm);
|
wenzelm@14643
|
921 |
val prop' = Thm.prop_of thm';
|
wenzelm@21576
|
922 |
val unconditional = (Logic.count_prems prop' = 0);
|
berghofe@10413
|
923 |
val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop')
|
berghofe@10413
|
924 |
in
|
nipkow@11295
|
925 |
if perm andalso not (termless (rhs', lhs'))
|
wenzelm@22254
|
926 |
then (trace_named_thm (fn () => "Cannot apply permutative rewrite rule") ss (thm, name);
|
wenzelm@22254
|
927 |
trace_thm (fn () => "Term does not become smaller:") ss thm'; NONE)
|
wenzelm@22254
|
928 |
else (trace_named_thm (fn () => "Applying instance of rewrite rule") ss (thm, name);
|
berghofe@10413
|
929 |
if unconditional
|
berghofe@10413
|
930 |
then
|
wenzelm@22254
|
931 |
(trace_thm (fn () => "Rewriting:") ss thm';
|
wenzelm@39080
|
932 |
let
|
wenzelm@39080
|
933 |
val lr = Logic.dest_equals prop;
|
wenzelm@39080
|
934 |
val SOME thm'' = check_conv false ss eta_thm thm';
|
skalberg@15531
|
935 |
in SOME (thm'', uncond_skel (congs, lr)) end)
|
berghofe@10413
|
936 |
else
|
wenzelm@22254
|
937 |
(trace_thm (fn () => "Trying to rewrite:") ss thm';
|
wenzelm@24124
|
938 |
if simp_depth ss > Config.get ctxt simp_depth_limit
|
wenzelm@39080
|
939 |
then
|
wenzelm@39080
|
940 |
let
|
wenzelm@39080
|
941 |
val s = "simp_depth_limit exceeded - giving up";
|
wenzelm@39080
|
942 |
val _ = trace false (fn () => s) ss;
|
wenzelm@39080
|
943 |
val _ = if_visible ss warning s;
|
wenzelm@39080
|
944 |
in NONE end
|
nipkow@16042
|
945 |
else
|
nipkow@16042
|
946 |
case prover ss thm' of
|
wenzelm@22254
|
947 |
NONE => (trace_thm (fn () => "FAILED") ss thm'; NONE)
|
skalberg@15531
|
948 |
| SOME thm2 =>
|
wenzelm@16985
|
949 |
(case check_conv true ss eta_thm thm2 of
|
skalberg@15531
|
950 |
NONE => NONE |
|
skalberg@15531
|
951 |
SOME thm2' =>
|
berghofe@10413
|
952 |
let val concl = Logic.strip_imp_concl prop
|
berghofe@10413
|
953 |
val lr = Logic.dest_equals concl
|
nipkow@16042
|
954 |
in SOME (thm2', cond_skel (congs, lr)) end)))
|
berghofe@10413
|
955 |
end
|
berghofe@10413
|
956 |
|
skalberg@15531
|
957 |
fun rews [] = NONE
|
berghofe@10413
|
958 |
| rews (rrule :: rrules) =
|
skalberg@15531
|
959 |
let val opt = rew rrule handle Pattern.MATCH => NONE
|
skalberg@15531
|
960 |
in case opt of NONE => rews rrules | some => some end;
|
berghofe@10413
|
961 |
|
wenzelm@39080
|
962 |
fun sort_rrules rrs =
|
wenzelm@39080
|
963 |
let
|
wenzelm@39080
|
964 |
fun is_simple ({thm, ...}: rrule) =
|
wenzelm@39080
|
965 |
(case Thm.prop_of thm of
|
wenzelm@39080
|
966 |
Const ("==", _) $ _ $ _ => true
|
wenzelm@39080
|
967 |
| _ => false);
|
wenzelm@39080
|
968 |
fun sort [] (re1, re2) = re1 @ re2
|
wenzelm@39080
|
969 |
| sort (rr :: rrs) (re1, re2) =
|
wenzelm@39080
|
970 |
if is_simple rr
|
wenzelm@39080
|
971 |
then sort rrs (rr :: re1, re2)
|
wenzelm@39080
|
972 |
else sort rrs (re1, rr :: re2);
|
wenzelm@39080
|
973 |
in sort rrs ([], []) end;
|
berghofe@10413
|
974 |
|
skalberg@15531
|
975 |
fun proc_rews [] = NONE
|
wenzelm@15023
|
976 |
| proc_rews (Proc {name, proc, lhs, ...} :: ps) =
|
wenzelm@17203
|
977 |
if Pattern.matches thyt (Thm.term_of lhs, Thm.term_of t) then
|
boehmes@35979
|
978 |
(debug_term false (fn () => "Trying procedure " ^ quote name ^ " on:") ss eta_t;
|
wenzelm@23938
|
979 |
case proc ss eta_t' of
|
wenzelm@22892
|
980 |
NONE => (debug false (fn () => "FAILED") ss; proc_rews ps)
|
skalberg@15531
|
981 |
| SOME raw_thm =>
|
wenzelm@22254
|
982 |
(trace_thm (fn () => "Procedure " ^ quote name ^ " produced rewrite rule:")
|
wenzelm@22254
|
983 |
ss raw_thm;
|
wenzelm@16985
|
984 |
(case rews (mk_procrule ss raw_thm) of
|
wenzelm@22254
|
985 |
NONE => (trace_cterm true (fn () => "IGNORED result of simproc " ^ quote name ^
|
wenzelm@16985
|
986 |
" -- does not match") ss t; proc_rews ps)
|
berghofe@10413
|
987 |
| some => some)))
|
berghofe@10413
|
988 |
else proc_rews ps;
|
wenzelm@39080
|
989 |
in
|
wenzelm@39080
|
990 |
(case eta_t of
|
wenzelm@39080
|
991 |
Abs _ $ _ => SOME (Thm.transitive eta_thm (Thm.beta_conversion false eta_t'), skel0)
|
wenzelm@39080
|
992 |
| _ =>
|
wenzelm@39080
|
993 |
(case rews (sort_rrules (Net.match_term rules eta_t)) of
|
wenzelm@39080
|
994 |
NONE => proc_rews (Net.match_term procs eta_t)
|
wenzelm@39080
|
995 |
| some => some))
|
berghofe@10413
|
996 |
end;
|
berghofe@10413
|
997 |
|
berghofe@10413
|
998 |
|
berghofe@10413
|
999 |
(* conversion to apply a congruence rule to a term *)
|
berghofe@10413
|
1000 |
|
krauss@30908
|
1001 |
fun congc prover ss maxt cong t =
|
wenzelm@22902
|
1002 |
let val rthm = Thm.incr_indexes (maxt + 1) cong;
|
wenzelm@22902
|
1003 |
val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
|
wenzelm@22902
|
1004 |
val insts = Thm.match (rlhs, t)
|
wenzelm@22902
|
1005 |
(* Thm.match can raise Pattern.MATCH;
|
berghofe@10413
|
1006 |
is handled when congc is called *)
|
berghofe@10413
|
1007 |
val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
|
wenzelm@32804
|
1008 |
val _ = trace_thm (fn () => "Applying congruence rule:") ss thm';
|
wenzelm@22254
|
1009 |
fun err (msg, thm) = (trace_thm (fn () => msg) ss thm; NONE)
|
wenzelm@39080
|
1010 |
in
|
wenzelm@39080
|
1011 |
(case prover thm' of
|
wenzelm@39080
|
1012 |
NONE => err ("Congruence proof failed. Could not prove", thm')
|
wenzelm@39080
|
1013 |
| SOME thm2 =>
|
wenzelm@39080
|
1014 |
(case check_conv true ss (Drule.beta_eta_conversion t) thm2 of
|
skalberg@15531
|
1015 |
NONE => err ("Congruence proof failed. Should not have proved", thm2)
|
skalberg@15531
|
1016 |
| SOME thm2' =>
|
wenzelm@22902
|
1017 |
if op aconv (pairself term_of (Thm.dest_equals (cprop_of thm2')))
|
wenzelm@39080
|
1018 |
then NONE else SOME thm2'))
|
berghofe@10413
|
1019 |
end;
|
berghofe@10413
|
1020 |
|
berghofe@10413
|
1021 |
val (cA, (cB, cC)) =
|
wenzelm@22902
|
1022 |
apsnd Thm.dest_equals (Thm.dest_implies (hd (cprems_of Drule.imp_cong)));
|
berghofe@10413
|
1023 |
|
skalberg@15531
|
1024 |
fun transitive1 NONE NONE = NONE
|
skalberg@15531
|
1025 |
| transitive1 (SOME thm1) NONE = SOME thm1
|
skalberg@15531
|
1026 |
| transitive1 NONE (SOME thm2) = SOME thm2
|
wenzelm@36944
|
1027 |
| transitive1 (SOME thm1) (SOME thm2) = SOME (Thm.transitive thm1 thm2)
|
berghofe@10413
|
1028 |
|
skalberg@15531
|
1029 |
fun transitive2 thm = transitive1 (SOME thm);
|
skalberg@15531
|
1030 |
fun transitive3 thm = transitive1 thm o SOME;
|
berghofe@13607
|
1031 |
|
wenzelm@16458
|
1032 |
fun bottomc ((simprem, useprem, mutsimp), prover, thy, maxidx) =
|
berghofe@10413
|
1033 |
let
|
wenzelm@15023
|
1034 |
fun botc skel ss t =
|
skalberg@15531
|
1035 |
if is_Var skel then NONE
|
berghofe@10413
|
1036 |
else
|
wenzelm@15023
|
1037 |
(case subc skel ss t of
|
skalberg@15531
|
1038 |
some as SOME thm1 =>
|
wenzelm@22902
|
1039 |
(case rewritec (prover, thy, maxidx) ss (Thm.rhs_of thm1) of
|
skalberg@15531
|
1040 |
SOME (thm2, skel2) =>
|
wenzelm@36944
|
1041 |
transitive2 (Thm.transitive thm1 thm2)
|
wenzelm@22902
|
1042 |
(botc skel2 ss (Thm.rhs_of thm2))
|
skalberg@15531
|
1043 |
| NONE => some)
|
skalberg@15531
|
1044 |
| NONE =>
|
wenzelm@16458
|
1045 |
(case rewritec (prover, thy, maxidx) ss t of
|
skalberg@15531
|
1046 |
SOME (thm2, skel2) => transitive2 thm2
|
wenzelm@22902
|
1047 |
(botc skel2 ss (Thm.rhs_of thm2))
|
skalberg@15531
|
1048 |
| NONE => NONE))
|
berghofe@10413
|
1049 |
|
wenzelm@15023
|
1050 |
and try_botc ss t =
|
wenzelm@15023
|
1051 |
(case botc skel0 ss t of
|
wenzelm@36944
|
1052 |
SOME trec1 => trec1 | NONE => (Thm.reflexive t))
|
berghofe@10413
|
1053 |
|
wenzelm@15023
|
1054 |
and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 =
|
berghofe@10413
|
1055 |
(case term_of t0 of
|
wenzelm@32804
|
1056 |
Abs (a, T, _) =>
|
wenzelm@15023
|
1057 |
let
|
wenzelm@20079
|
1058 |
val b = Name.bound (#1 bounds);
|
wenzelm@16985
|
1059 |
val (v, t') = Thm.dest_abs (SOME b) t0;
|
wenzelm@16985
|
1060 |
val b' = #1 (Term.dest_Free (Thm.term_of v));
|
wenzelm@21962
|
1061 |
val _ =
|
wenzelm@21962
|
1062 |
if b <> b' then
|
wenzelm@35231
|
1063 |
warning ("Simplifier: renamed bound variable " ^
|
wenzelm@35231
|
1064 |
quote b ^ " to " ^ quote b' ^ Position.str_of (Position.thread_data ()))
|
wenzelm@21962
|
1065 |
else ();
|
wenzelm@17614
|
1066 |
val ss' = add_bound ((b', T), a) ss;
|
wenzelm@15023
|
1067 |
val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0;
|
wenzelm@15023
|
1068 |
in case botc skel' ss' t' of
|
wenzelm@36944
|
1069 |
SOME thm => SOME (Thm.abstract_rule a v thm)
|
skalberg@15531
|
1070 |
| NONE => NONE
|
berghofe@10413
|
1071 |
end
|
berghofe@10413
|
1072 |
| t $ _ => (case t of
|
wenzelm@15023
|
1073 |
Const ("==>", _) $ _ => impc t0 ss
|
berghofe@10413
|
1074 |
| Abs _ =>
|
wenzelm@36944
|
1075 |
let val thm = Thm.beta_conversion false t0
|
wenzelm@22902
|
1076 |
in case subc skel0 ss (Thm.rhs_of thm) of
|
skalberg@15531
|
1077 |
NONE => SOME thm
|
wenzelm@36944
|
1078 |
| SOME thm' => SOME (Thm.transitive thm thm')
|
berghofe@10413
|
1079 |
end
|
berghofe@10413
|
1080 |
| _ =>
|
berghofe@10413
|
1081 |
let fun appc () =
|
berghofe@10413
|
1082 |
let
|
berghofe@10413
|
1083 |
val (tskel, uskel) = case skel of
|
berghofe@10413
|
1084 |
tskel $ uskel => (tskel, uskel)
|
berghofe@10413
|
1085 |
| _ => (skel0, skel0);
|
wenzelm@10767
|
1086 |
val (ct, cu) = Thm.dest_comb t0
|
berghofe@10413
|
1087 |
in
|
wenzelm@15023
|
1088 |
(case botc tskel ss ct of
|
skalberg@15531
|
1089 |
SOME thm1 =>
|
wenzelm@15023
|
1090 |
(case botc uskel ss cu of
|
wenzelm@36944
|
1091 |
SOME thm2 => SOME (Thm.combination thm1 thm2)
|
wenzelm@36944
|
1092 |
| NONE => SOME (Thm.combination thm1 (Thm.reflexive cu)))
|
skalberg@15531
|
1093 |
| NONE =>
|
wenzelm@15023
|
1094 |
(case botc uskel ss cu of
|
wenzelm@36944
|
1095 |
SOME thm1 => SOME (Thm.combination (Thm.reflexive ct) thm1)
|
skalberg@15531
|
1096 |
| NONE => NONE))
|
berghofe@10413
|
1097 |
end
|
berghofe@10413
|
1098 |
val (h, ts) = strip_comb t
|
ballarin@13835
|
1099 |
in case cong_name h of
|
skalberg@15531
|
1100 |
SOME a =>
|
haftmann@17232
|
1101 |
(case AList.lookup (op =) (fst congs) a of
|
skalberg@15531
|
1102 |
NONE => appc ()
|
skalberg@15531
|
1103 |
| SOME cong =>
|
wenzelm@15023
|
1104 |
(*post processing: some partial applications h t1 ... tj, j <= length ts,
|
wenzelm@15023
|
1105 |
may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
|
berghofe@10413
|
1106 |
(let
|
wenzelm@16985
|
1107 |
val thm = congc (prover ss) ss maxidx cong t0;
|
wenzelm@22902
|
1108 |
val t = the_default t0 (Option.map Thm.rhs_of thm);
|
wenzelm@10767
|
1109 |
val (cl, cr) = Thm.dest_comb t
|
berghofe@10413
|
1110 |
val dVar = Var(("", 0), dummyT)
|
berghofe@10413
|
1111 |
val skel =
|
berghofe@10413
|
1112 |
list_comb (h, replicate (length ts) dVar)
|
wenzelm@15023
|
1113 |
in case botc skel ss cl of
|
skalberg@15531
|
1114 |
NONE => thm
|
skalberg@15531
|
1115 |
| SOME thm' => transitive3 thm
|
wenzelm@36944
|
1116 |
(Thm.combination thm' (Thm.reflexive cr))
|
wenzelm@20057
|
1117 |
end handle Pattern.MATCH => appc ()))
|
berghofe@10413
|
1118 |
| _ => appc ()
|
berghofe@10413
|
1119 |
end)
|
skalberg@15531
|
1120 |
| _ => NONE)
|
berghofe@10413
|
1121 |
|
wenzelm@15023
|
1122 |
and impc ct ss =
|
wenzelm@15023
|
1123 |
if mutsimp then mut_impc0 [] ct [] [] ss else nonmut_impc ct ss
|
berghofe@10413
|
1124 |
|
wenzelm@15023
|
1125 |
and rules_of_prem ss prem =
|
berghofe@13607
|
1126 |
if maxidx_of_term (term_of prem) <> ~1
|
berghofe@13607
|
1127 |
then (trace_cterm true
|
wenzelm@22254
|
1128 |
(fn () => "Cannot add premise as rewrite rule because it contains (type) unknowns:")
|
wenzelm@22254
|
1129 |
ss prem; ([], NONE))
|
berghofe@13607
|
1130 |
else
|
wenzelm@36944
|
1131 |
let val asm = Thm.assume prem
|
skalberg@15531
|
1132 |
in (extract_safe_rrules (ss, asm), SOME asm) end
|
berghofe@10413
|
1133 |
|
wenzelm@15023
|
1134 |
and add_rrules (rrss, asms) ss =
|
wenzelm@20028
|
1135 |
(fold o fold) insert_rrule rrss ss |> add_prems (map_filter I asms)
|
berghofe@13607
|
1136 |
|
wenzelm@23178
|
1137 |
and disch r prem eq =
|
berghofe@10413
|
1138 |
let
|
wenzelm@22902
|
1139 |
val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
|
wenzelm@36944
|
1140 |
val eq' = Thm.implies_elim (Thm.instantiate
|
berghofe@13607
|
1141 |
([], [(cA, prem), (cB, lhs), (cC, rhs)]) Drule.imp_cong)
|
wenzelm@36944
|
1142 |
(Thm.implies_intr prem eq)
|
berghofe@13607
|
1143 |
in if not r then eq' else
|
berghofe@10413
|
1144 |
let
|
wenzelm@22902
|
1145 |
val (prem', concl) = Thm.dest_implies lhs;
|
wenzelm@22902
|
1146 |
val (prem'', _) = Thm.dest_implies rhs
|
wenzelm@36944
|
1147 |
in Thm.transitive (Thm.transitive
|
berghofe@13607
|
1148 |
(Thm.instantiate ([], [(cA, prem'), (cB, prem), (cC, concl)])
|
berghofe@13607
|
1149 |
Drule.swap_prems_eq) eq')
|
berghofe@13607
|
1150 |
(Thm.instantiate ([], [(cA, prem), (cB, prem''), (cC, concl)])
|
berghofe@13607
|
1151 |
Drule.swap_prems_eq)
|
berghofe@10413
|
1152 |
end
|
berghofe@10413
|
1153 |
end
|
berghofe@10413
|
1154 |
|
berghofe@13607
|
1155 |
and rebuild [] _ _ _ _ eq = eq
|
wenzelm@32804
|
1156 |
| rebuild (prem :: prems) concl (_ :: rrss) (_ :: asms) ss eq =
|
berghofe@13607
|
1157 |
let
|
wenzelm@15023
|
1158 |
val ss' = add_rrules (rev rrss, rev asms) ss;
|
berghofe@13607
|
1159 |
val concl' =
|
wenzelm@22902
|
1160 |
Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
|
wenzelm@23178
|
1161 |
val dprem = Option.map (disch false prem)
|
wenzelm@39080
|
1162 |
in
|
wenzelm@39080
|
1163 |
(case rewritec (prover, thy, maxidx) ss' concl' of
|
skalberg@15531
|
1164 |
NONE => rebuild prems concl' rrss asms ss (dprem eq)
|
wenzelm@23178
|
1165 |
| SOME (eq', _) => transitive2 (fold (disch false)
|
wenzelm@23178
|
1166 |
prems (the (transitive3 (dprem eq) eq')))
|
wenzelm@39080
|
1167 |
(mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ss))
|
berghofe@13607
|
1168 |
end
|
wenzelm@15023
|
1169 |
|
wenzelm@15023
|
1170 |
and mut_impc0 prems concl rrss asms ss =
|
berghofe@13607
|
1171 |
let
|
berghofe@13607
|
1172 |
val prems' = strip_imp_prems concl;
|
wenzelm@15023
|
1173 |
val (rrss', asms') = split_list (map (rules_of_prem ss) prems')
|
wenzelm@39080
|
1174 |
in
|
wenzelm@39080
|
1175 |
mut_impc (prems @ prems') (strip_imp_concl concl) (rrss @ rrss')
|
wenzelm@39080
|
1176 |
(asms @ asms') [] [] [] [] ss ~1 ~1
|
berghofe@13607
|
1177 |
end
|
wenzelm@15023
|
1178 |
|
wenzelm@15023
|
1179 |
and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k =
|
wenzelm@33261
|
1180 |
transitive1 (fold (fn (eq1, prem) => fn eq2 => transitive1 eq1
|
wenzelm@33261
|
1181 |
(Option.map (disch false prem) eq2)) (eqns ~~ prems') NONE)
|
berghofe@13607
|
1182 |
(if changed > 0 then
|
berghofe@13607
|
1183 |
mut_impc (rev prems') concl (rev rrss') (rev asms')
|
wenzelm@15023
|
1184 |
[] [] [] [] ss ~1 changed
|
wenzelm@15023
|
1185 |
else rebuild prems' concl rrss' asms' ss
|
wenzelm@15023
|
1186 |
(botc skel0 (add_rrules (rev rrss', rev asms') ss) concl))
|
berghofe@13607
|
1187 |
|
berghofe@13607
|
1188 |
| mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms)
|
wenzelm@15023
|
1189 |
prems' rrss' asms' eqns ss changed k =
|
skalberg@15531
|
1190 |
case (if k = 0 then NONE else botc skel0 (add_rrules
|
wenzelm@15023
|
1191 |
(rev rrss' @ rrss, rev asms' @ asms) ss) prem) of
|
skalberg@15531
|
1192 |
NONE => mut_impc prems concl rrss asms (prem :: prems')
|
skalberg@15531
|
1193 |
(rrs :: rrss') (asm :: asms') (NONE :: eqns) ss changed
|
berghofe@13607
|
1194 |
(if k = 0 then 0 else k - 1)
|
skalberg@15531
|
1195 |
| SOME eqn =>
|
berghofe@13607
|
1196 |
let
|
wenzelm@22902
|
1197 |
val prem' = Thm.rhs_of eqn;
|
berghofe@13607
|
1198 |
val tprems = map term_of prems;
|
wenzelm@33029
|
1199 |
val i = 1 + fold Integer.max (map (fn p =>
|
wenzelm@33029
|
1200 |
find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn))) ~1;
|
wenzelm@15023
|
1201 |
val (rrs', asm') = rules_of_prem ss prem'
|
berghofe@13607
|
1202 |
in mut_impc prems concl rrss asms (prem' :: prems')
|
wenzelm@23178
|
1203 |
(rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
|
haftmann@33956
|
1204 |
(take i prems)
|
wenzelm@36944
|
1205 |
(Drule.imp_cong_rule eqn (Thm.reflexive (Drule.list_implies
|
haftmann@33956
|
1206 |
(drop i prems, concl))))) :: eqns)
|
wenzelm@20671
|
1207 |
ss (length prems') ~1
|
berghofe@13607
|
1208 |
end
|
berghofe@13607
|
1209 |
|
wenzelm@15023
|
1210 |
(*legacy code - only for backwards compatibility*)
|
wenzelm@39080
|
1211 |
and nonmut_impc ct ss =
|
wenzelm@39080
|
1212 |
let
|
wenzelm@39080
|
1213 |
val (prem, conc) = Thm.dest_implies ct;
|
wenzelm@39080
|
1214 |
val thm1 = if simprem then botc skel0 ss prem else NONE;
|
wenzelm@39080
|
1215 |
val prem1 = the_default prem (Option.map Thm.rhs_of thm1);
|
wenzelm@39080
|
1216 |
val ss1 =
|
wenzelm@39080
|
1217 |
if not useprem then ss
|
wenzelm@39080
|
1218 |
else add_rrules (apsnd single (apfst single (rules_of_prem ss prem1))) ss
|
wenzelm@39080
|
1219 |
in
|
wenzelm@39080
|
1220 |
(case botc skel0 ss1 conc of
|
wenzelm@39080
|
1221 |
NONE =>
|
wenzelm@39080
|
1222 |
(case thm1 of
|
wenzelm@39080
|
1223 |
NONE => NONE
|
wenzelm@39080
|
1224 |
| SOME thm1' => SOME (Drule.imp_cong_rule thm1' (Thm.reflexive conc)))
|
wenzelm@39080
|
1225 |
| SOME thm2 =>
|
wenzelm@39080
|
1226 |
let val thm2' = disch false prem1 thm2 in
|
wenzelm@39080
|
1227 |
(case thm1 of
|
wenzelm@39080
|
1228 |
NONE => SOME thm2'
|
wenzelm@39080
|
1229 |
| SOME thm1' =>
|
wenzelm@36944
|
1230 |
SOME (Thm.transitive (Drule.imp_cong_rule thm1' (Thm.reflexive conc)) thm2'))
|
wenzelm@39080
|
1231 |
end)
|
wenzelm@39080
|
1232 |
end
|
berghofe@10413
|
1233 |
|
wenzelm@15023
|
1234 |
in try_botc end;
|
berghofe@10413
|
1235 |
|
berghofe@10413
|
1236 |
|
wenzelm@15023
|
1237 |
(* Meta-rewriting: rewrites t to u and returns the theorem t==u *)
|
berghofe@10413
|
1238 |
|
berghofe@10413
|
1239 |
(*
|
berghofe@10413
|
1240 |
Parameters:
|
berghofe@10413
|
1241 |
mode = (simplify A,
|
berghofe@10413
|
1242 |
use A in simplifying B,
|
berghofe@10413
|
1243 |
use prems of B (if B is again a meta-impl.) to simplify A)
|
berghofe@10413
|
1244 |
when simplifying A ==> B
|
berghofe@10413
|
1245 |
prover: how to solve premises in conditional rewrites and congruences
|
berghofe@10413
|
1246 |
*)
|
berghofe@10413
|
1247 |
|
wenzelm@32738
|
1248 |
val debug_bounds = Unsynchronized.ref false;
|
wenzelm@17705
|
1249 |
|
wenzelm@21962
|
1250 |
fun check_bounds ss ct =
|
wenzelm@21962
|
1251 |
if ! debug_bounds then
|
wenzelm@21962
|
1252 |
let
|
wenzelm@21962
|
1253 |
val Simpset ({bounds = (_, bounds), ...}, _) = ss;
|
wenzelm@21962
|
1254 |
val bs = fold_aterms (fn Free (x, _) =>
|
wenzelm@21962
|
1255 |
if Name.is_bound x andalso not (AList.defined eq_bound bounds x)
|
wenzelm@21962
|
1256 |
then insert (op =) x else I
|
wenzelm@21962
|
1257 |
| _ => I) (term_of ct) [];
|
wenzelm@21962
|
1258 |
in
|
wenzelm@21962
|
1259 |
if null bs then ()
|
boehmes@35979
|
1260 |
else print_term_global ss true ("Simplifier: term contains loose bounds: " ^ commas_quote bs)
|
wenzelm@21962
|
1261 |
(Thm.theory_of_cterm ct) (Thm.term_of ct)
|
wenzelm@21962
|
1262 |
end
|
wenzelm@21962
|
1263 |
else ();
|
wenzelm@17614
|
1264 |
|
wenzelm@19052
|
1265 |
fun rewrite_cterm mode prover raw_ss raw_ct =
|
wenzelm@17882
|
1266 |
let
|
wenzelm@26626
|
1267 |
val thy = Thm.theory_of_cterm raw_ct;
|
wenzelm@20260
|
1268 |
val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
|
wenzelm@32804
|
1269 |
val {maxidx, ...} = Thm.rep_cterm ct;
|
wenzelm@22892
|
1270 |
val ss = inc_simp_depth (activate_context thy raw_ss);
|
wenzelm@22892
|
1271 |
val depth = simp_depth ss;
|
wenzelm@21962
|
1272 |
val _ =
|
wenzelm@22892
|
1273 |
if depth mod 20 = 0 then
|
wenzelm@39080
|
1274 |
if_visible ss warning ("Simplification depth " ^ string_of_int depth)
|
wenzelm@21962
|
1275 |
else ();
|
wenzelm@22254
|
1276 |
val _ = trace_cterm false (fn () => "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:") ss ct;
|
wenzelm@17882
|
1277 |
val _ = check_bounds ss ct;
|
wenzelm@22892
|
1278 |
in bottomc (mode, Option.map Drule.flexflex_unique oo prover, thy, maxidx) ss ct end;
|
berghofe@10413
|
1279 |
|
wenzelm@21708
|
1280 |
val simple_prover =
|
wenzelm@21708
|
1281 |
SINGLE o (fn ss => ALLGOALS (resolve_tac (prems_of_ss ss)));
|
wenzelm@21708
|
1282 |
|
wenzelm@21708
|
1283 |
fun rewrite _ [] ct = Thm.reflexive ct
|
haftmann@27582
|
1284 |
| rewrite full thms ct = rewrite_cterm (full, false, false) simple_prover
|
wenzelm@35232
|
1285 |
(global_context (Thm.theory_of_cterm ct) empty_ss addsimps thms) ct;
|
wenzelm@11672
|
1286 |
|
wenzelm@23598
|
1287 |
fun simplify full thms = Conv.fconv_rule (rewrite full thms);
|
wenzelm@21708
|
1288 |
val rewrite_rule = simplify true;
|
wenzelm@21708
|
1289 |
|
wenzelm@15023
|
1290 |
(*simple term rewriting -- no proof*)
|
wenzelm@16458
|
1291 |
fun rewrite_term thy rules procs =
|
wenzelm@17203
|
1292 |
Pattern.rewrite_term thy (map decomp_simp' rules) procs;
|
wenzelm@15023
|
1293 |
|
wenzelm@22902
|
1294 |
fun rewrite_thm mode prover ss = Conv.fconv_rule (rewrite_cterm mode prover ss);
|
berghofe@10413
|
1295 |
|
wenzelm@23536
|
1296 |
(*Rewrite the subgoals of a proof state (represented by a theorem)*)
|
wenzelm@21708
|
1297 |
fun rewrite_goals_rule thms th =
|
wenzelm@23584
|
1298 |
Conv.fconv_rule (Conv.prems_conv ~1 (rewrite_cterm (true, true, true) simple_prover
|
wenzelm@35232
|
1299 |
(global_context (Thm.theory_of_thm th) empty_ss addsimps thms))) th;
|
berghofe@10413
|
1300 |
|
wenzelm@15023
|
1301 |
(*Rewrite the subgoal of a proof state (represented by a theorem)*)
|
skalberg@15011
|
1302 |
fun rewrite_goal_rule mode prover ss i thm =
|
wenzelm@23536
|
1303 |
if 0 < i andalso i <= Thm.nprems_of thm
|
wenzelm@23584
|
1304 |
then Conv.gconv_rule (rewrite_cterm mode prover ss) i thm
|
wenzelm@23536
|
1305 |
else raise THM ("rewrite_goal_rule", i, [thm]);
|
berghofe@10413
|
1306 |
|
wenzelm@20228
|
1307 |
|
wenzelm@21708
|
1308 |
(** meta-rewriting tactics **)
|
wenzelm@21708
|
1309 |
|
wenzelm@28839
|
1310 |
(*Rewrite all subgoals*)
|
wenzelm@21708
|
1311 |
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs);
|
wenzelm@21708
|
1312 |
fun rewtac def = rewrite_goals_tac [def];
|
wenzelm@21708
|
1313 |
|
wenzelm@28839
|
1314 |
(*Rewrite one subgoal*)
|
wenzelm@25203
|
1315 |
fun asm_rewrite_goal_tac mode prover_tac ss i thm =
|
wenzelm@25203
|
1316 |
if 0 < i andalso i <= Thm.nprems_of thm then
|
wenzelm@25203
|
1317 |
Seq.single (Conv.gconv_rule (rewrite_cterm mode (SINGLE o prover_tac) ss) i thm)
|
wenzelm@25203
|
1318 |
else Seq.empty;
|
wenzelm@23536
|
1319 |
|
wenzelm@23536
|
1320 |
fun rewrite_goal_tac rews =
|
wenzelm@23536
|
1321 |
let val ss = empty_ss addsimps rews in
|
wenzelm@23536
|
1322 |
fn i => fn st => asm_rewrite_goal_tac (true, false, false) (K no_tac)
|
wenzelm@35232
|
1323 |
(global_context (Thm.theory_of_thm st) ss) i st
|
wenzelm@23536
|
1324 |
end;
|
wenzelm@23536
|
1325 |
|
wenzelm@21708
|
1326 |
(*Prunes all redundant parameters from the proof state by rewriting.
|
wenzelm@21708
|
1327 |
DOES NOT rewrite main goal, where quantification over an unused bound
|
wenzelm@21708
|
1328 |
variable is sometimes done to avoid the need for cut_facts_tac.*)
|
wenzelm@21708
|
1329 |
val prune_params_tac = rewrite_goals_tac [triv_forall_equality];
|
wenzelm@21708
|
1330 |
|
wenzelm@21708
|
1331 |
|
wenzelm@21708
|
1332 |
(* for folding definitions, handling critical pairs *)
|
wenzelm@21708
|
1333 |
|
wenzelm@21708
|
1334 |
(*The depth of nesting in a term*)
|
wenzelm@32804
|
1335 |
fun term_depth (Abs (_, _, t)) = 1 + term_depth t
|
wenzelm@32804
|
1336 |
| term_depth (f $ t) = 1 + Int.max (term_depth f, term_depth t)
|
wenzelm@21708
|
1337 |
| term_depth _ = 0;
|
wenzelm@21708
|
1338 |
|
wenzelm@21708
|
1339 |
val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
|
wenzelm@21708
|
1340 |
|
wenzelm@21708
|
1341 |
(*folding should handle critical pairs! E.g. K == Inl(0), S == Inr(Inl(0))
|
wenzelm@21708
|
1342 |
Returns longest lhs first to avoid folding its subexpressions.*)
|
wenzelm@21708
|
1343 |
fun sort_lhs_depths defs =
|
wenzelm@21708
|
1344 |
let val keylist = AList.make (term_depth o lhs_of_thm) defs
|
wenzelm@21708
|
1345 |
val keys = sort_distinct (rev_order o int_ord) (map #2 keylist)
|
wenzelm@21708
|
1346 |
in map (AList.find (op =) keylist) keys end;
|
wenzelm@21708
|
1347 |
|
wenzelm@36944
|
1348 |
val rev_defs = sort_lhs_depths o map Thm.symmetric;
|
wenzelm@21708
|
1349 |
|
wenzelm@21708
|
1350 |
fun fold_rule defs = fold rewrite_rule (rev_defs defs);
|
wenzelm@21708
|
1351 |
fun fold_goals_tac defs = EVERY (map rewrite_goals_tac (rev_defs defs));
|
wenzelm@21708
|
1352 |
|
wenzelm@21708
|
1353 |
|
wenzelm@20228
|
1354 |
(* HHF normal form: !! before ==>, outermost !! generalized *)
|
wenzelm@20228
|
1355 |
|
wenzelm@20228
|
1356 |
local
|
wenzelm@20228
|
1357 |
|
wenzelm@21565
|
1358 |
fun gen_norm_hhf ss th =
|
wenzelm@21565
|
1359 |
(if Drule.is_norm_hhf (Thm.prop_of th) then th
|
wenzelm@26424
|
1360 |
else Conv.fconv_rule
|
wenzelm@35232
|
1361 |
(rewrite_cterm (true, false, false) (K (K NONE)) (global_context (Thm.theory_of_thm th) ss)) th)
|
wenzelm@21565
|
1362 |
|> Thm.adjust_maxidx_thm ~1
|
wenzelm@21565
|
1363 |
|> Drule.gen_all;
|
wenzelm@20228
|
1364 |
|
wenzelm@28620
|
1365 |
val hhf_ss = empty_ss addsimps Drule.norm_hhf_eqs;
|
wenzelm@20228
|
1366 |
|
wenzelm@20228
|
1367 |
in
|
wenzelm@20228
|
1368 |
|
wenzelm@26424
|
1369 |
val norm_hhf = gen_norm_hhf hhf_ss;
|
wenzelm@26424
|
1370 |
val norm_hhf_protect = gen_norm_hhf (hhf_ss addeqcongs [Drule.protect_cong]);
|
wenzelm@20228
|
1371 |
|
wenzelm@20228
|
1372 |
end;
|
wenzelm@20228
|
1373 |
|
berghofe@10413
|
1374 |
end;
|
berghofe@10413
|
1375 |
|
wenzelm@41494
|
1376 |
structure Basic_Meta_Simplifier: BASIC_RAW_SIMPLIFIER = Raw_Simplifier;
|
wenzelm@32738
|
1377 |
open Basic_Meta_Simplifier;
|