src/HOL/Library/Reflection.thy
author wenzelm
Fri Mar 13 19:58:26 2009 +0100 (2009-03-13)
changeset 30510 4120fc59dd85
parent 29650 cc3958d31b1d
child 30549 d2d7874648bd
permissions -rw-r--r--
unified type Proof.method and pervasive METHOD combinators;
     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 uses "reify_data.ML" ("reflection.ML")
    10 begin
    11 
    12 setup {* Reify_Data.setup *}
    13 
    14 lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
    15   by (blast intro: ext)
    16 
    17 use "reflection.ML"
    18 
    19 method_setup reify = {* fn src =>
    20   Method.syntax (Attrib.thms --
    21     Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
    22   (fn ((eqs, to), ctxt) => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
    23 *} "partial automatic reification"
    24 
    25 method_setup reflection = {* 
    26 let 
    27   fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
    28   val onlyN = "only";
    29   val rulesN = "rules";
    30   val any_keyword = keyword onlyN || keyword rulesN;
    31   val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    32   val terms = thms >> map (term_of o Drule.dest_term);
    33   fun optional scan = Scan.optional scan [];
    34 in fn src =>
    35   Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #> 
    36     (fn (((eqs,ths),to), ctxt) => 
    37       let 
    38         val (ceqs,cths) = Reify_Data.get ctxt 
    39         val corr_thms = ths@cths
    40         val raw_eqs = eqs@ceqs
    41       in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
    42      end) end
    43 *} "reflection method"
    44 
    45 end