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