src/HOL/Library/Reflection.thy
author Manuel Eberl <eberlm@in.tum.de>
Mon Mar 26 16:14:16 2018 +0200 (18 months ago)
changeset 67951 655aa11359dc
parent 61476 1884c40f1539
child 69605 a96320074298
permissions -rw-r--r--
Removed some uses of deprecated _tac methods. (Patch from Viorel Preoteasa)
     1 (*  Title:      HOL/Library/Reflection.thy
     2     Author:     Amine Chaieb, TU Muenchen
     3 *)
     4 
     5 section \<open>Generic reflection and reification\<close>
     6 
     7 theory Reflection
     8 imports Main
     9 begin
    10 
    11 ML_file "~~/src/HOL/Tools/reflection.ML"
    12 
    13 method_setup reify = \<open>
    14   Attrib.thms --
    15     Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
    16       (fn (user_eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.default_reify_tac ctxt user_eqs to))
    17 \<close> "partial automatic reification"
    18 
    19 method_setup reflection = \<open>
    20 let
    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.repeats (Scan.unless any_keyword Attrib.multi_thm);
    26   val terms = thms >> map (Thm.term_of o Drule.dest_term);
    27 in
    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))
    32 end
    33 \<close> "partial automatic reflection"
    34 
    35 end
    36