src/HOL/ex/Reflection.thy
author chaieb
Sun Jul 08 19:01:30 2007 +0200 (2007-07-08)
changeset 23649 4d865f3e4405
parent 23607 6a8fb529b542
permissions -rw-r--r--
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
     1 (*
     2     ID:         $Id$
     3     Author:     Amine Chaieb, TU Muenchen
     4 *)
     5 
     6 header {* Generic reflection and reification *}
     7 
     8 theory Reflection
     9 imports Main
    10   uses "reflection_data.ML" ("reflection.ML")
    11 begin
    12 
    13 setup {* Reify_Data.setup*}
    14 
    15 
    16 lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
    17   by (blast intro: ext)
    18 
    19 use "reflection.ML"
    20 
    21 method_setup reify = {*
    22   fn src =>
    23     Method.syntax (Attrib.thms --
    24       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
    25   (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
    26 *} "partial automatic reification"
    27 
    28 method_setup reflection = {* 
    29 let 
    30 fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
    31 val onlyN = "only";
    32 val rulesN = "rules";
    33 val any_keyword = keyword onlyN || keyword rulesN;
    34 val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    35 val terms = thms >> map (term_of o Drule.dest_term);
    36 fun optional scan = Scan.optional scan [];
    37 in
    38 fn src =>
    39     Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #> 
    40   (fn (((eqs,ths),to), ctxt) => 
    41       let 
    42         val (ceqs,cths) = Reify_Data.get ctxt 
    43         val corr_thms = ths@cths
    44         val raw_eqs = eqs@ceqs
    45       in Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
    46      end) end
    47 *} "reflection method"
    48 end