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