src/HOL/ex/Reflection.thy
author haftmann
Mon Dec 18 08:21:35 2006 +0100 (2006-12-18)
changeset 21879 a3efbae45735
parent 21588 cd0dc678a205
child 22199 b617ddd200eb
permissions -rw-r--r--
switched argument order in *.syntax lifters
     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 ((eqs, to), ctxt) => 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 ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt ths to))
    29 *} "reflection method"
    30 
    31 end