| author | wenzelm |
| Tue, 20 May 2025 17:02:10 +0200 | |
| changeset 82637 | c6c20afb29c2 |
| parent 69605 | a96320074298 |
| permissions | -rw-r--r-- |
| 29650 | 1 |
(* Title: HOL/Library/Reflection.thy |
| 20319 | 2 |
Author: Amine Chaieb, TU Muenchen |
3 |
*) |
|
4 |
||
| 60500 | 5 |
section \<open>Generic reflection and reification\<close> |
| 20319 | 6 |
|
7 |
theory Reflection |
|
8 |
imports Main |
|
9 |
begin |
|
10 |
||
| 69605 | 11 |
ML_file \<open>~~/src/HOL/Tools/reflection.ML\<close> |
| 48891 | 12 |
|
| 60500 | 13 |
method_setup reify = \<open> |
| 30549 | 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)) |
| 60500 | 17 |
\<close> "partial automatic reification" |
| 20319 | 18 |
|
| 60500 | 19 |
method_setup reflection = \<open> |
|
31412
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; |
|
| 61476 | 25 |
val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm); |
| 59582 | 26 |
val terms = thms >> map (Thm.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 |
| 60500 | 33 |
\<close> "partial automatic reflection" |
| 29650 | 34 |
|
| 20319 | 35 |
end |
| 46764 | 36 |