src/HOL/ex/Reflection.thy
author chaieb
Sun Jan 28 11:52:52 2007 +0100 (2007-01-28)
changeset 22199 b617ddd200eb
parent 21879 a3efbae45735
child 23546 c8a1bd9585a0
permissions -rw-r--r--
Now deals with simples cases where the input equations contain type variables
See example in ReflectionEx.thy
     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 
    16 use "reflection.ML"
    17 
    18 method_setup reify = {*
    19   fn src =>
    20     Method.syntax (Attrib.thms --
    21       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    22   (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt eqs to))
    23 *} "partial automatic reification"
    24 
    25 method_setup reflection = {*
    26   fn src =>
    27     Method.syntax (Attrib.thms --
    28       Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    29   (fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt ths to))
    30 *} "reflection method"
    31 
    32 end