equal
deleted
inserted
replaced
6 |
6 |
7 signature MEASURABLE = |
7 signature MEASURABLE = |
8 sig |
8 sig |
9 datatype level = Concrete | Generic |
9 datatype level = Concrete | Generic |
10 |
10 |
|
11 val add_app : thm -> Context.generic -> Context.generic |
|
12 val add_dest : thm -> Context.generic -> Context.generic |
|
13 val add_thm : bool * level -> thm -> Context.generic -> Context.generic |
|
14 |
|
15 val measurable_tac : Proof.context -> thm list -> tactic |
|
16 |
11 val simproc : Proof.context -> cterm -> thm option |
17 val simproc : Proof.context -> cterm -> thm option |
12 val method : (Proof.context -> Method.method) context_parser |
|
13 val measurable_tac : Proof.context -> thm list -> tactic |
|
14 |
|
15 val attr : attribute context_parser |
|
16 val dest_attr : attribute context_parser |
|
17 val app_attr : attribute context_parser |
|
18 |
18 |
19 val get : level -> Proof.context -> thm list |
19 val get : level -> Proof.context -> thm list |
20 val get_all : Proof.context -> thm list |
20 val get_all : Proof.context -> thm list |
21 |
21 |
22 val update : (thm Item_Net.T -> thm Item_Net.T) -> level -> Context.generic -> Context.generic |
22 val update : (thm Item_Net.T -> thm Item_Net.T) -> level -> Context.generic -> Context.generic |
211 in debug_tac ctxt (debug_facts "start") depth_measurable_tac end; |
211 in debug_tac ctxt (debug_facts "start") depth_measurable_tac end; |
212 |
212 |
213 fun measurable_tac ctxt facts = |
213 fun measurable_tac ctxt facts = |
214 TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt facts); |
214 TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt facts); |
215 |
215 |
216 val attr_add = Thm.declaration_attribute o add_thm; |
|
217 |
|
218 val attr : attribute context_parser = |
|
219 Scan.lift (Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false -- |
|
220 Scan.optional (Args.$$$ "generic" >> K Generic) Concrete)) (false, Concrete) >> attr_add); |
|
221 |
|
222 val dest_attr : attribute context_parser = |
|
223 Scan.lift (Scan.succeed (Thm.declaration_attribute add_dest)); |
|
224 |
|
225 val app_attr : attribute context_parser = |
|
226 Scan.lift (Scan.succeed (Thm.declaration_attribute add_app)); |
|
227 |
|
228 val method : (Proof.context -> Method.method) context_parser = |
|
229 Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts))); |
|
230 |
|
231 fun simproc ctxt redex = |
216 fun simproc ctxt redex = |
232 let |
217 let |
233 val t = HOLogic.mk_Trueprop (term_of redex); |
218 val t = HOLogic.mk_Trueprop (term_of redex); |
234 fun tac {context = ctxt, prems = _ } = |
219 fun tac {context = ctxt, prems = _ } = |
235 SOLVE (measurable_tac' ctxt (Simplifier.prems_of ctxt)); |
220 SOLVE (measurable_tac' ctxt (Simplifier.prems_of ctxt)); |