(* Title: HOL/Library/Reflection.thy
Author: Amine Chaieb, TU Muenchen
*)
header {* Generic reflection and reification *}
theory Reflection
imports Main
begin
ML_file "~~/src/HOL/Tools/reflection.ML"
method_setup reify = {*
Attrib.thms --
Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
(fn (user_eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.default_reify_tac ctxt user_eqs to))
*} "partial automatic reification"
method_setup reflection = {*
let
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
val onlyN = "only";
val rulesN = "rules";
val any_keyword = keyword onlyN || keyword rulesN;
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
val terms = thms >> map (term_of o Drule.dest_term);
in
thms -- Scan.optional (keyword rulesN |-- thms) [] --
Scan.option (keyword onlyN |-- Args.term) >>
(fn ((user_eqs, user_thms), to) => fn ctxt =>
SIMPLE_METHOD' (Reflection.default_reflection_tac ctxt user_thms user_eqs to))
end
*} "partial automatic reflection"
end