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