src/HOL/ex/Reflection.thy
author chaieb
Tue Jul 03 17:49:55 2007 +0200 (2007-07-03)
changeset 23546 c8a1bd9585a0
parent 22199 b617ddd200eb
child 23607 6a8fb529b542
permissions -rw-r--r--
reflection and reification methods now manage Context data
     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 ML{* Reify_Data.get @{context}*}
    21 
    22 method_setup reify = {*
    23   fn src =>
    24     Method.syntax (Attrib.thms --
    25       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    26   (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ Reify_Data.get ctxt) to))
    27 *} "partial automatic reification"
    28 
    29 method_setup reflection = {*
    30   fn src =>
    31     Method.syntax (Attrib.thms --
    32       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    33   (fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt (ths @ Reify_Data.get ctxt) to))
    34 *} "reflection method"
    35 
    36 end