src/HOL/Library/Reflection.thy
author wenzelm
Wed Sep 12 13:42:28 2012 +0200 (2012-09-12)
changeset 49322 fbb320d02420
parent 48891 c0eafbd55de3
child 51542 738598beeb26
permissions -rw-r--r--
tuned headers;
     1 (*  Title:      HOL/Library/Reflection.thy
     2     Author:     Amine Chaieb, TU Muenchen
     3 *)
     4 
     5 header {* Generic reflection and reification *}
     6 
     7 theory Reflection
     8 imports Main
     9 begin
    10 
    11 ML_file "~~/src/HOL/Library/reify_data.ML"
    12 ML_file "~~/src/HOL/Library/reflection.ML"
    13 
    14 setup {* Reify_Data.setup *}
    15 
    16 method_setup reify = {*
    17   Attrib.thms --
    18     Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
    19   (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ fst (Reify_Data.get ctxt)) to))
    20 *} "partial automatic reification"
    21 
    22 method_setup reflection = {*
    23 let
    24   fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
    25   val onlyN = "only";
    26   val rulesN = "rules";
    27   val any_keyword = keyword onlyN || keyword rulesN;
    28   val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    29   val terms = thms >> map (term_of o Drule.dest_term);
    30 in
    31   thms --
    32   Scan.optional (keyword rulesN |-- thms) [] --
    33   Scan.option (keyword onlyN |-- Args.term) >>
    34   (fn ((eqs, ths), to) => fn ctxt =>
    35     let
    36       val (ceqs, cths) = Reify_Data.get ctxt
    37       val corr_thms = ths @ cths
    38       val raw_eqs = eqs @ ceqs
    39     in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
    40 end
    41 *}
    42 
    43 end
    44