src/HOL/ex/Reflection.thy
author wenzelm
Thu Aug 03 15:03:05 2006 +0200 (2006-08-03)
changeset 20319 a8761e8568de
child 20374 01b711328990
permissions -rw-r--r--
Generic reflection and reification (by Amine Chaieb).
wenzelm@20319
     1
(*
wenzelm@20319
     2
    ID:         $Id$
wenzelm@20319
     3
    Author:     Amine Chaieb, TU Muenchen
wenzelm@20319
     4
*)
wenzelm@20319
     5
wenzelm@20319
     6
header {* Generic reflection and reification *}
wenzelm@20319
     7
wenzelm@20319
     8
theory Reflection
wenzelm@20319
     9
imports Main
wenzelm@20319
    10
uses "reflection.ML"
wenzelm@20319
    11
begin
wenzelm@20319
    12
wenzelm@20319
    13
method_setup reify = {*
wenzelm@20319
    14
  fn src =>
wenzelm@20319
    15
    Method.syntax (Attrib.thms --
wenzelm@20319
    16
      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
wenzelm@20319
    17
  (fn (ctxt, (eqs,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.genreify_tac ctxt eqs to))
wenzelm@20319
    18
*} "partial automatic reification"
wenzelm@20319
    19
wenzelm@20319
    20
method_setup reflection = {*
wenzelm@20319
    21
  fn src =>
wenzelm@20319
    22
    Method.syntax (Attrib.thms --
wenzelm@20319
    23
      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
wenzelm@20319
    24
  (fn (ctxt, (ths,to)) => Method.SIMPLE_METHOD' HEADGOAL (Reflection.reflection_tac ctxt ths to))
wenzelm@20319
    25
*} "reflection method"
wenzelm@20319
    26
wenzelm@20319
    27
end