| author | blanchet |
| Wed, 07 Aug 2013 17:23:40 +0200 | |
| changeset 52899 | 3ff23987f316 |
| parent 51726 | b3e599b5ecc8 |
| child 58881 | b9556a055632 |
| permissions | -rw-r--r-- |
| 29650 | 1 |
(* Title: HOL/Library/Reflection.thy |
| 20319 | 2 |
Author: Amine Chaieb, TU Muenchen |
3 |
*) |
|
4 |
||
5 |
header {* Generic reflection and reification *}
|
|
6 |
||
7 |
theory Reflection |
|
8 |
imports Main |
|
9 |
begin |
|
10 |
||
| 51726 | 11 |
ML_file "~~/src/HOL/Tools/reflection.ML" |
| 48891 | 12 |
|
| 30549 | 13 |
method_setup reify = {*
|
14 |
Attrib.thms -- |
|
15 |
Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
|
|
| 51723 | 16 |
(fn (user_eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.default_reify_tac ctxt user_eqs to)) |
| 20319 | 17 |
*} "partial automatic reification" |
18 |
||
|
31412
f2e6b6526092
Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations.
hoelzl
parents:
30549
diff
changeset
|
19 |
method_setup reflection = {*
|
|
f2e6b6526092
Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations.
hoelzl
parents:
30549
diff
changeset
|
20 |
let |
| 29650 | 21 |
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K (); |
22 |
val onlyN = "only"; |
|
23 |
val rulesN = "rules"; |
|
24 |
val any_keyword = keyword onlyN || keyword rulesN; |
|
25 |
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; |
|
26 |
val terms = thms >> map (term_of o Drule.dest_term); |
|
| 30549 | 27 |
in |
| 51723 | 28 |
thms -- Scan.optional (keyword rulesN |-- thms) [] -- |
29 |
Scan.option (keyword onlyN |-- Args.term) >> |
|
30 |
(fn ((user_eqs, user_thms), to) => fn ctxt => |
|
31 |
SIMPLE_METHOD' (Reflection.default_reflection_tac ctxt user_thms user_eqs to)) |
|
| 30549 | 32 |
end |
| 51723 | 33 |
*} "partial automatic reflection" |
| 29650 | 34 |
|
| 20319 | 35 |
end |
| 46764 | 36 |