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