src/HOL/ex/Reflection.thy
author wenzelm
Wed Nov 29 15:44:51 2006 +0100 (2006-11-29)
changeset 21588 cd0dc678a205
parent 20374 01b711328990
child 21879 a3efbae45735
permissions -rw-r--r--
simplified method setup;
     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.ML")
    11 begin
    12 
    13 lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
    14   by (blast intro: ext)
    15 use "reflection.ML"
    16 
    17 method_setup reify = {*
    18   fn src =>
    19     Method.syntax (Attrib.thms --
    20       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    21   (fn (ctxt, (eqs,to)) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt eqs to))
    22 *} "partial automatic reification"
    23 
    24 method_setup reflection = {*
    25   fn src =>
    26     Method.syntax (Attrib.thms --
    27       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    28   (fn (ctxt, (ths,to)) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt ths to))
    29 *} "reflection method"
    30 
    31 end