author | wenzelm |
Thu, 19 Oct 2023 21:58:47 +0200 | |
changeset 78802 | 88593174aef5 |
parent 78800 | 0b3700d31758 |
child 78803 | 577835250124 |
permissions | -rw-r--r-- |
16014 | 1 |
(* Title: Pure/simplifier.ML |
2 |
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
|
3 |
||
4 |
Generic simplifier, suitable for most logics (see also |
|
41386 | 5 |
raw_simplifier.ML for the actual meta-level rewriting engine). |
16014 | 6 |
*) |
7 |
||
8 |
signature BASIC_SIMPLIFIER = |
|
9 |
sig |
|
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
10 |
include BASIC_RAW_SIMPLIFIER |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
11 |
val simp_tac: Proof.context -> int -> tactic |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
12 |
val asm_simp_tac: Proof.context -> int -> tactic |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
13 |
val full_simp_tac: Proof.context -> int -> tactic |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
14 |
val asm_lr_simp_tac: Proof.context -> int -> tactic |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
15 |
val asm_full_simp_tac: Proof.context -> int -> tactic |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
16 |
val safe_simp_tac: Proof.context -> int -> tactic |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
17 |
val safe_asm_simp_tac: Proof.context -> int -> tactic |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
18 |
val safe_full_simp_tac: Proof.context -> int -> tactic |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
19 |
val safe_asm_lr_simp_tac: Proof.context -> int -> tactic |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
20 |
val safe_asm_full_simp_tac: Proof.context -> int -> tactic |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
21 |
val simplify: Proof.context -> thm -> thm |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
22 |
val asm_simplify: Proof.context -> thm -> thm |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
23 |
val full_simplify: Proof.context -> thm -> thm |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
24 |
val asm_lr_simplify: Proof.context -> thm -> thm |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
25 |
val asm_full_simplify: Proof.context -> thm -> thm |
16014 | 26 |
end; |
27 |
||
28 |
signature SIMPLIFIER = |
|
29 |
sig |
|
30 |
include BASIC_SIMPLIFIER |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
31 |
val map_ss: (Proof.context -> Proof.context) -> Context.generic -> Context.generic |
56510
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
32 |
val attrib: (thm -> Proof.context -> Proof.context) -> attribute |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
33 |
val simp_add: attribute |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
34 |
val simp_del: attribute |
68403 | 35 |
val simp_flip: attribute |
56510
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
36 |
val cong_add: attribute |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
37 |
val cong_del: attribute |
78115 | 38 |
val check_simproc: Proof.context -> xstring * Position.T -> string * simproc |
56510
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
39 |
val the_simproc: Proof.context -> string -> simproc |
78792
103467dc5117
support for "simproc_setup ... (passive)": allow to define simprocs in Isar that are not added to the simpset (yet);
wenzelm
parents:
78115
diff
changeset
|
40 |
val make_simproc: Proof.context -> string -> |
78800 | 41 |
{lhss: term list, proc: morphism -> proc} -> simproc |
78802 | 42 |
val define_simproc: {passive: bool, name: binding, lhss: term list, proc: morphism -> proc} -> |
43 |
local_theory -> simproc * local_theory |
|
44 |
val define_simproc_cmd: {passive: bool, name: binding, lhss: string list, proc: morphism -> proc} -> |
|
45 |
local_theory -> simproc * local_theory |
|
78799 | 46 |
type 'a simproc_setup = {passive: bool, name: binding, lhss: string list, proc: 'a} |
78797 | 47 |
type simproc_setup_input = Input.source simproc_setup |
78800 | 48 |
type simproc_setup_internal = (morphism -> proc) simproc_setup |
78797 | 49 |
val simproc_setup_parser: Input.source simproc_setup parser |
78796
f34926a91fea
clarified signature: more concise simproc setup in ML;
wenzelm
parents:
78792
diff
changeset
|
50 |
val simproc_setup_ml: Input.source simproc_setup -> ML_Lex.token Antiquote.antiquote list |
78798
200daaab2578
clarified signature: Named_Target.setup works both for global and local theory;
wenzelm
parents:
78797
diff
changeset
|
51 |
val simproc_setup: simproc_setup_internal -> simproc |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59621
diff
changeset
|
52 |
val pretty_simpset: bool -> Proof.context -> Pretty.T |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
53 |
val default_mk_sym: Proof.context -> thm -> thm option |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
54 |
val prems_of: Proof.context -> thm list |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
55 |
val add_simp: thm -> Proof.context -> Proof.context |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
56 |
val del_simp: thm -> Proof.context -> Proof.context |
63221
7d43fbbaba28
avoid warnings on duplicate rules in the given list;
wenzelm
parents:
62913
diff
changeset
|
57 |
val init_simpset: thm list -> Proof.context -> Proof.context |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
58 |
val add_eqcong: thm -> Proof.context -> Proof.context |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
59 |
val del_eqcong: thm -> Proof.context -> Proof.context |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
60 |
val add_cong: thm -> Proof.context -> Proof.context |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
61 |
val del_cong: thm -> Proof.context -> Proof.context |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
62 |
val add_prems: thm list -> Proof.context -> Proof.context |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
63 |
val mksimps: Proof.context -> thm -> thm list |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
64 |
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:
51688
diff
changeset
|
65 |
val set_mkcong: (Proof.context -> thm -> thm) -> Proof.context -> Proof.context |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
66 |
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:
51688
diff
changeset
|
67 |
val set_mkeqTrue: (Proof.context -> thm -> thm option) -> Proof.context -> Proof.context |
70586 | 68 |
val set_term_ord: term ord -> Proof.context -> Proof.context |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
69 |
val set_subgoaler: (Proof.context -> int -> tactic) -> Proof.context -> Proof.context |
54729
c5cd7a58cf2d
generic trace operations for main steps of Simplifier;
wenzelm
parents:
54728
diff
changeset
|
70 |
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
|
71 |
val set_trace_ops: trace_ops -> theory -> theory |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
72 |
val rewrite: Proof.context -> conv |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
73 |
val asm_rewrite: Proof.context -> conv |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
74 |
val full_rewrite: Proof.context -> conv |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
75 |
val asm_lr_rewrite: Proof.context -> conv |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
76 |
val asm_full_rewrite: Proof.context -> conv |
30513 | 77 |
val cong_modifiers: Method.modifier parser list |
78 |
val simp_modifiers': Method.modifier parser list |
|
79 |
val simp_modifiers: Method.modifier parser list |
|
80 |
val method_setup: Method.modifier parser list -> theory -> theory |
|
63532
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
81 |
val unsafe_solver_tac: Proof.context -> int -> tactic |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
82 |
val unsafe_solver: solver |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
83 |
val safe_solver_tac: Proof.context -> int -> tactic |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
84 |
val safe_solver: solver |
16014 | 85 |
end; |
86 |
||
87 |
structure Simplifier: SIMPLIFIER = |
|
88 |
struct |
|
89 |
||
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
90 |
open Raw_Simplifier; |
21708 | 91 |
|
92 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
93 |
(** declarations **) |
16014 | 94 |
|
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset
|
95 |
(* attributes *) |
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset
|
96 |
|
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45375
diff
changeset
|
97 |
fun attrib f = Thm.declaration_attribute (map_ss o f); |
16014 | 98 |
|
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45375
diff
changeset
|
99 |
val simp_add = attrib add_simp; |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45375
diff
changeset
|
100 |
val simp_del = attrib del_simp; |
68403 | 101 |
val simp_flip = attrib flip_simp; |
45620
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45375
diff
changeset
|
102 |
val cong_add = attrib add_cong; |
f2a587696afb
modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents:
45375
diff
changeset
|
103 |
val cong_del = attrib del_cong; |
26497
1873915c64a9
purely functional setup of claset/simpset/clasimpset;
wenzelm
parents:
26463
diff
changeset
|
104 |
|
16014 | 105 |
|
22201 | 106 |
(** named simprocs **) |
107 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
108 |
structure Simprocs = Generic_Data |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
109 |
( |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
110 |
type T = simproc Name_Space.table; |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
111 |
val empty : T = Name_Space.empty_table "simproc"; |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
112 |
fun merge data : T = Name_Space.merge_tables data; |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
113 |
); |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
114 |
|
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
115 |
|
22204 | 116 |
(* get simprocs *) |
117 |
||
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
118 |
val get_simprocs = Simprocs.get o Context.Proof; |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
119 |
|
42466 | 120 |
val the_simproc = Name_Space.get o get_simprocs; |
78115 | 121 |
fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt); |
42465
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
122 |
|
53171 | 123 |
val _ = Theory.setup |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
124 |
(ML_Antiquotation.value_embedded \<^binding>\<open>simproc\<close> |
78115 | 125 |
(Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, name) => |
126 |
"Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (#1 (check_simproc ctxt name))))); |
|
22204 | 127 |
|
128 |
||
129 |
(* define simprocs *) |
|
22201 | 130 |
|
62913 | 131 |
fun make_simproc ctxt name {lhss, proc} = |
61144 | 132 |
let |
70308 | 133 |
val ctxt' = fold Proof_Context.augment lhss ctxt; |
61144 | 134 |
val lhss' = Variable.export_terms ctxt' ctxt lhss; |
135 |
in |
|
78072 | 136 |
cert_simproc (Proof_Context.theory_of ctxt) name |
137 |
{lhss = lhss', proc = Morphism.entity proc} |
|
61144 | 138 |
end; |
139 |
||
22201 | 140 |
local |
141 |
||
78802 | 142 |
fun def_simproc prep {passive, name, lhss, proc} lthy = |
22201 | 143 |
let |
78114 | 144 |
val simproc0 = |
78802 | 145 |
make_simproc lthy (Local_Theory.full_name lthy name) {lhss = prep lthy lhss, proc = proc}; |
22201 | 146 |
in |
78802 | 147 |
lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of name} |
78095 | 148 |
(fn phi => fn context => |
149 |
let |
|
78802 | 150 |
val name' = Morphism.binding phi name; |
78114 | 151 |
val simproc' = simproc0 |> transform_simproc phi |> trim_context_simproc; |
78095 | 152 |
in |
153 |
context |
|
78802 | 154 |
|> Simprocs.map (#2 o Name_Space.define context true (name', simproc')) |
78792
103467dc5117
support for "simproc_setup ... (passive)": allow to define simprocs in Isar that are not added to the simpset (yet);
wenzelm
parents:
78115
diff
changeset
|
155 |
|> not passive ? map_ss (fn ctxt => ctxt addsimprocs [simproc']) |
78095 | 156 |
end) |
78796
f34926a91fea
clarified signature: more concise simproc setup in ML;
wenzelm
parents:
78792
diff
changeset
|
157 |
|> pair simproc0 |
22201 | 158 |
end; |
159 |
||
160 |
in |
|
161 |
||
61144 | 162 |
val define_simproc = def_simproc Syntax.check_terms; |
163 |
val define_simproc_cmd = def_simproc Syntax.read_terms; |
|
22201 | 164 |
|
165 |
end; |
|
166 |
||
167 |
||
78796
f34926a91fea
clarified signature: more concise simproc setup in ML;
wenzelm
parents:
78792
diff
changeset
|
168 |
(* implicit simproc_setup *) |
f34926a91fea
clarified signature: more concise simproc setup in ML;
wenzelm
parents:
78792
diff
changeset
|
169 |
|
78799 | 170 |
type 'a simproc_setup = {passive: bool, name: binding, lhss: string list, proc: 'a}; |
78797 | 171 |
type simproc_setup_input = Input.source simproc_setup; |
78800 | 172 |
type simproc_setup_internal = (morphism -> proc) simproc_setup; |
78796
f34926a91fea
clarified signature: more concise simproc setup in ML;
wenzelm
parents:
78792
diff
changeset
|
173 |
|
78797 | 174 |
val simproc_setup_parser : simproc_setup_input parser = |
78799 | 175 |
Scan.optional (Parse.$$$ "passive" >> K true) false -- |
176 |
Parse.binding -- |
|
177 |
(Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")") -- |
|
178 |
(Parse.$$$ "=" |-- Parse.ML_source) |
|
179 |
>> (fn (((a, b), c), d) => {passive = a, name = b, lhss = c, proc = d}); |
|
78796
f34926a91fea
clarified signature: more concise simproc setup in ML;
wenzelm
parents:
78792
diff
changeset
|
180 |
|
78799 | 181 |
fun simproc_setup_ml ({name, passive, lhss, proc}: simproc_setup_input) = |
78796
f34926a91fea
clarified signature: more concise simproc setup in ML;
wenzelm
parents:
78792
diff
changeset
|
182 |
ML_Lex.read |
78799 | 183 |
("{passive = " ^ Bool.toString passive ^ |
184 |
", name = " ^ ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name) ^ |
|
78796
f34926a91fea
clarified signature: more concise simproc setup in ML;
wenzelm
parents:
78792
diff
changeset
|
185 |
", lhss = " ^ ML_Syntax.print_strings lhss ^ |
f34926a91fea
clarified signature: more concise simproc setup in ML;
wenzelm
parents:
78792
diff
changeset
|
186 |
", proc = (") @ ML_Lex.read_source proc @ ML_Lex.read ")}"; |
f34926a91fea
clarified signature: more concise simproc setup in ML;
wenzelm
parents:
78792
diff
changeset
|
187 |
|
78802 | 188 |
fun simproc_setup args = |
78798
200daaab2578
clarified signature: Named_Target.setup works both for global and local theory;
wenzelm
parents:
78797
diff
changeset
|
189 |
Named_Target.setup_result Raw_Simplifier.transform_simproc |
78802 | 190 |
(define_simproc_cmd args); |
78797 | 191 |
|
78796
f34926a91fea
clarified signature: more concise simproc setup in ML;
wenzelm
parents:
78792
diff
changeset
|
192 |
|
f34926a91fea
clarified signature: more concise simproc setup in ML;
wenzelm
parents:
78792
diff
changeset
|
193 |
|
71788
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71235
diff
changeset
|
194 |
(** congruence rule to protect foundational terms of local definitions **) |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71235
diff
changeset
|
195 |
|
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71235
diff
changeset
|
196 |
local |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71235
diff
changeset
|
197 |
|
78043 | 198 |
fun add_foundation_cong (binding, (const, target_params)) gthy = |
199 |
if null target_params then gthy |
|
71788
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71235
diff
changeset
|
200 |
else |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71235
diff
changeset
|
201 |
let |
78043 | 202 |
val thy = Context.theory_of gthy; |
203 |
val cong = |
|
204 |
list_comb (const, target_params) |
|
205 |
|> Logic.varify_global |
|
206 |
|> Thm.global_cterm_of thy |
|
207 |
|> Thm.reflexive |
|
208 |
|> Thm.close_derivation \<^here>; |
|
209 |
val cong_binding = Binding.qualify_name true binding "cong"; |
|
71788
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71235
diff
changeset
|
210 |
in |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71235
diff
changeset
|
211 |
gthy |
78043 | 212 |
|> Attrib.generic_notes Thm.theoremK [((cong_binding, []), [([cong], [])])] |
213 |
|> #2 |
|
71788
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71235
diff
changeset
|
214 |
end; |
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71235
diff
changeset
|
215 |
|
78043 | 216 |
val _ = Theory.setup (Generic_Target.add_foundation_interpretation add_foundation_cong); |
71788
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71235
diff
changeset
|
217 |
|
78043 | 218 |
in end; |
71788
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71235
diff
changeset
|
219 |
|
ca3ac5238c41
hooks for foundational terms: protection of foundational terms during simplification
haftmann
parents:
71235
diff
changeset
|
220 |
|
22201 | 221 |
|
56510
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
222 |
(** pretty_simpset **) |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
223 |
|
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59621
diff
changeset
|
224 |
fun pretty_simpset verbose ctxt = |
56510
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
225 |
let |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
226 |
val pretty_term = Syntax.pretty_term ctxt; |
61268 | 227 |
val pretty_thm = Thm.pretty_thm ctxt; |
228 |
val pretty_thm_item = Thm.pretty_thm_item ctxt; |
|
56510
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
229 |
|
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
230 |
fun pretty_simproc (name, lhss) = |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
231 |
Pretty.block |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
232 |
(Pretty.mark_str name :: Pretty.str ":" :: Pretty.fbrk :: |
61098 | 233 |
Pretty.fbreaks (map (Pretty.item o single o pretty_term) lhss)); |
56510
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
234 |
|
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
235 |
fun pretty_cong_name (const, name) = |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
236 |
pretty_term ((if const then Const else Free) (name, dummyT)); |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
237 |
fun pretty_cong (name, thm) = |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
238 |
Pretty.block [pretty_cong_name name, Pretty.str ":", Pretty.brk 1, pretty_thm thm]; |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
239 |
|
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
240 |
val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
241 |
dest_ss (simpset_of ctxt); |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
242 |
val simprocs = |
59917
9830c944670f
more uniform "verbose" option to print name space;
wenzelm
parents:
59621
diff
changeset
|
243 |
Name_Space.markup_entries verbose ctxt (Name_Space.space_of_table (get_simprocs ctxt)) procs; |
56510
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
244 |
in |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
245 |
[Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps), |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
246 |
Pretty.big_list "simplification procedures:" (map pretty_simproc simprocs), |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
247 |
Pretty.big_list "congruences:" (map pretty_cong congs), |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
248 |
Pretty.strs ("loopers:" :: map quote loopers), |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
249 |
Pretty.strs ("unsafe solvers:" :: map quote unsafe_solvers), |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
250 |
Pretty.strs ("safe solvers:" :: map quote safe_solvers)] |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
251 |
|> Pretty.chunks |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
252 |
end; |
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
253 |
|
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
254 |
|
aec722524c33
added simproc markup, which also indicates legacy simprocs outside the name space;
wenzelm
parents:
56204
diff
changeset
|
255 |
|
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
256 |
(** simplification tactics and rules **) |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
257 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
258 |
fun solve_all_tac solvers ctxt = |
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
259 |
let |
71235 | 260 |
val subgoal_tac = Raw_Simplifier.subgoal_tac (Raw_Simplifier.set_solvers solvers ctxt); |
261 |
val solve_tac = subgoal_tac THEN_ALL_NEW (K no_tac); |
|
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
262 |
in DEPTH_SOLVE (solve_tac 1) end; |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
263 |
|
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
264 |
(*NOTE: may instantiate unknowns that appear also in other subgoals*) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
265 |
fun generic_simp_tac safe mode ctxt = |
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
266 |
let |
71235 | 267 |
val loop_tac = Raw_Simplifier.loop_tac ctxt; |
268 |
val (unsafe_solvers, solvers) = Raw_Simplifier.solvers ctxt; |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
269 |
val solve_tac = FIRST' (map (Raw_Simplifier.solver ctxt) |
22717 | 270 |
(rev (if safe then solvers else unsafe_solvers))); |
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
271 |
|
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
272 |
fun simp_loop_tac i = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
273 |
Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ctxt i THEN |
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
274 |
(solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i)); |
52458
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
51717
diff
changeset
|
275 |
in PREFER_GOAL (simp_loop_tac 1) end; |
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
276 |
|
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
277 |
local |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
278 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
279 |
fun simp rew mode ctxt thm = |
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
280 |
let |
71235 | 281 |
val (unsafe_solvers, _) = Raw_Simplifier.solvers ctxt; |
22717 | 282 |
val tacf = solve_all_tac (rev unsafe_solvers); |
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
283 |
fun prover s th = Option.map #1 (Seq.pull (tacf s th)); |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
284 |
in rew mode prover ctxt thm end; |
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
285 |
|
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
286 |
in |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
287 |
|
41228
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
288 |
val simp_thm = simp Raw_Simplifier.rewrite_thm; |
e1fce873b814
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents:
41226
diff
changeset
|
289 |
val simp_cterm = simp Raw_Simplifier.rewrite_cterm; |
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
290 |
|
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
291 |
end; |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
292 |
|
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
293 |
|
16806 | 294 |
(* tactics *) |
295 |
||
16014 | 296 |
val simp_tac = generic_simp_tac false (false, false, false); |
297 |
val asm_simp_tac = generic_simp_tac false (false, true, false); |
|
298 |
val full_simp_tac = generic_simp_tac false (true, false, false); |
|
299 |
val asm_lr_simp_tac = generic_simp_tac false (true, true, false); |
|
300 |
val asm_full_simp_tac = generic_simp_tac false (true, true, true); |
|
50107 | 301 |
|
302 |
(*not totally safe: may instantiate unknowns that appear also in other subgoals*) |
|
303 |
val safe_simp_tac = generic_simp_tac true (false, false, false); |
|
304 |
val safe_asm_simp_tac = generic_simp_tac true (false, true, false); |
|
305 |
val safe_full_simp_tac = generic_simp_tac true (true, false, false); |
|
306 |
val safe_asm_lr_simp_tac = generic_simp_tac true (true, true, false); |
|
16014 | 307 |
val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true); |
308 |
||
16806 | 309 |
|
310 |
(* conversions *) |
|
311 |
||
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
312 |
val simplify = simp_thm (false, false, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
313 |
val asm_simplify = simp_thm (false, true, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
314 |
val full_simplify = simp_thm (true, false, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
315 |
val asm_lr_simplify = simp_thm (true, true, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
316 |
val asm_full_simplify = simp_thm (true, true, true); |
16014 | 317 |
|
17967
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
318 |
val rewrite = simp_cterm (false, false, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
319 |
val asm_rewrite = simp_cterm (false, true, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
320 |
val full_rewrite = simp_cterm (true, false, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
321 |
val asm_lr_rewrite = simp_cterm (true, true, false); |
7a733b7438e1
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm
parents:
17898
diff
changeset
|
322 |
val asm_full_rewrite = simp_cterm (true, true, true); |
16014 | 323 |
|
324 |
||
325 |
||
326 |
(** concrete syntax of attributes **) |
|
327 |
||
328 |
(* add / del *) |
|
329 |
||
330 |
val simpN = "simp"; |
|
68403 | 331 |
val flipN = "flip" |
16014 | 332 |
val congN = "cong"; |
333 |
val onlyN = "only"; |
|
334 |
val no_asmN = "no_asm"; |
|
335 |
val no_asm_useN = "no_asm_use"; |
|
336 |
val no_asm_simpN = "no_asm_simp"; |
|
337 |
val asm_lrN = "asm_lr"; |
|
338 |
||
339 |
||
24024 | 340 |
(* simprocs *) |
341 |
||
342 |
local |
|
343 |
||
344 |
val add_del = |
|
345 |
(Args.del -- Args.colon >> K (op delsimprocs) || |
|
346 |
Scan.option (Args.add -- Args.colon) >> K (op addsimprocs)) |
|
78072 | 347 |
>> (fn f => fn simproc => Morphism.entity (fn phi => Thm.declaration_attribute |
348 |
(K (Raw_Simplifier.map_ss (fn ctxt => f (ctxt, [transform_simproc phi simproc])))))); |
|
24024 | 349 |
|
350 |
in |
|
351 |
||
30528 | 352 |
val simproc_att = |
42465
1ba52683512a
clarified check_simproc (with report) vs. the_simproc;
wenzelm
parents:
42464
diff
changeset
|
353 |
(Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) => |
78115 | 354 |
Scan.repeat1 (Scan.lift (Args.named_attribute (decl o #2 o check_simproc ctxt)))) |
45375
7fe19930dfc9
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
wenzelm
parents:
45326
diff
changeset
|
355 |
>> (fn atts => Thm.declaration_attribute (fn th => |
46776 | 356 |
fold (fn att => Thm.attribute_declaration (Morphism.form att) th) atts)); |
24024 | 357 |
|
358 |
end; |
|
24124
4399175e3014
turned simp_depth_limit into configuration option;
wenzelm
parents:
24024
diff
changeset
|
359 |
|
24024 | 360 |
|
16014 | 361 |
(* conversions *) |
362 |
||
363 |
local |
|
364 |
||
365 |
fun conv_mode x = |
|
366 |
((Args.parens (Args.$$$ no_asmN) >> K simplify || |
|
367 |
Args.parens (Args.$$$ no_asm_simpN) >> K asm_simplify || |
|
368 |
Args.parens (Args.$$$ no_asm_useN) >> K full_simplify || |
|
369 |
Scan.succeed asm_full_simplify) |> Scan.lift) x; |
|
370 |
||
371 |
in |
|
372 |
||
30528 | 373 |
val simplified = conv_mode -- Attrib.thms >> |
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61841
diff
changeset
|
374 |
(fn (f, ths) => Thm.rule_attribute ths (fn context => |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
375 |
f ((if null ths then I else Raw_Simplifier.clear_simpset) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
376 |
(Context.proof_of context) addsimps ths))); |
16014 | 377 |
|
378 |
end; |
|
379 |
||
380 |
||
381 |
(* setup attributes *) |
|
382 |
||
53171 | 383 |
val _ = Theory.setup |
67147 | 384 |
(Attrib.setup \<^binding>\<open>simp\<close> (Attrib.add_del simp_add simp_del) |
30528 | 385 |
"declaration of Simplifier rewrite rule" #> |
67147 | 386 |
Attrib.setup \<^binding>\<open>cong\<close> (Attrib.add_del cong_add cong_del) |
30528 | 387 |
"declaration of Simplifier congruence rule" #> |
67147 | 388 |
Attrib.setup \<^binding>\<open>simproc\<close> simproc_att |
33671 | 389 |
"declaration of simplification procedures" #> |
67147 | 390 |
Attrib.setup \<^binding>\<open>simplified\<close> simplified "simplified rule"); |
16014 | 391 |
|
392 |
||
393 |
||
31300 | 394 |
(** method syntax **) |
16014 | 395 |
|
396 |
val cong_modifiers = |
|
64556 | 397 |
[Args.$$$ congN -- Args.colon >> K (Method.modifier cong_add \<^here>), |
398 |
Args.$$$ congN -- Args.add -- Args.colon >> K (Method.modifier cong_add \<^here>), |
|
399 |
Args.$$$ congN -- Args.del -- Args.colon >> K (Method.modifier cong_del \<^here>)]; |
|
16014 | 400 |
|
401 |
val simp_modifiers = |
|
64556 | 402 |
[Args.$$$ simpN -- Args.colon >> K (Method.modifier simp_add \<^here>), |
403 |
Args.$$$ simpN -- Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>), |
|
404 |
Args.$$$ simpN -- Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>), |
|
68403 | 405 |
Args.$$$ simpN -- Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>), |
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58008
diff
changeset
|
406 |
Args.$$$ simpN -- Args.$$$ onlyN -- Args.colon >> |
64556 | 407 |
K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}] |
16014 | 408 |
@ cong_modifiers; |
409 |
||
410 |
val simp_modifiers' = |
|
64556 | 411 |
[Args.add -- Args.colon >> K (Method.modifier simp_add \<^here>), |
412 |
Args.del -- Args.colon >> K (Method.modifier simp_del \<^here>), |
|
68403 | 413 |
Args.$$$ flipN -- Args.colon >> K (Method.modifier simp_flip \<^here>), |
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
58008
diff
changeset
|
414 |
Args.$$$ onlyN -- Args.colon >> |
64556 | 415 |
K {init = Raw_Simplifier.clear_simpset, attribute = simp_add, pos = \<^here>}] |
16014 | 416 |
@ cong_modifiers; |
417 |
||
31300 | 418 |
val simp_options = |
419 |
(Args.parens (Args.$$$ no_asmN) >> K simp_tac || |
|
420 |
Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac || |
|
421 |
Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac || |
|
422 |
Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac || |
|
423 |
Scan.succeed asm_full_simp_tac); |
|
16014 | 424 |
|
31300 | 425 |
fun simp_method more_mods meth = |
35613 | 426 |
Scan.lift simp_options --| |
31300 | 427 |
Method.sections (more_mods @ simp_modifiers') >> |
35613 | 428 |
(fn tac => fn ctxt => METHOD (fn facts => meth ctxt tac facts)); |
16014 | 429 |
|
430 |
||
431 |
||
18708 | 432 |
(** setup **) |
433 |
||
31300 | 434 |
fun method_setup more_mods = |
67147 | 435 |
Method.setup \<^binding>\<open>simp\<close> |
31300 | 436 |
(simp_method more_mods (fn ctxt => fn tac => fn facts => |
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61268
diff
changeset
|
437 |
HEADGOAL (Method.insert_tac ctxt facts THEN' |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51688
diff
changeset
|
438 |
(CHANGED_PROP oo tac) ctxt))) |
31300 | 439 |
"simplification" #> |
67147 | 440 |
Method.setup \<^binding>\<open>simp_all\<close> |
31300 | 441 |
(simp_method more_mods (fn ctxt => fn tac => fn facts => |
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61268
diff
changeset
|
442 |
ALLGOALS (Method.insert_tac ctxt facts) THEN |
58008 | 443 |
(CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt)) |
31300 | 444 |
"simplification (all goals)"; |
16014 | 445 |
|
63532
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
446 |
fun unsafe_solver_tac ctxt = |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
447 |
FIRST' [resolve_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), assume_tac ctxt]; |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
448 |
val unsafe_solver = mk_solver "Pure unsafe" unsafe_solver_tac; |
16014 | 449 |
|
63532
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
450 |
(*no premature instantiation of variables during simplification*) |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
451 |
fun safe_solver_tac ctxt = |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
452 |
FIRST' [match_tac ctxt (Drule.reflexive_thm :: Raw_Simplifier.prems_of ctxt), eq_assume_tac]; |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
453 |
val safe_solver = mk_solver "Pure safe" safe_solver_tac; |
16014 | 454 |
|
63532
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
455 |
val _ = |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
456 |
Theory.setup |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
457 |
(method_setup [] #> Context.theory_map (map_ss (fn ctxt => |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
458 |
empty_simpset ctxt |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
459 |
setSSolver safe_solver |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
460 |
setSolver unsafe_solver |
b01154b74314
provide Pure.simp/simp_all, which only know about meta-equality;
wenzelm
parents:
63221
diff
changeset
|
461 |
|> set_subgoaler asm_simp_tac))); |
16014 | 462 |
|
463 |
end; |
|
464 |
||
32738 | 465 |
structure Basic_Simplifier: BASIC_SIMPLIFIER = Simplifier; |
466 |
open Basic_Simplifier; |