src/HOL/ex/Reflection.thy
author chaieb
Tue Jul 03 17:49:55 2007 +0200 (2007-07-03)
changeset 23546 c8a1bd9585a0
parent 22199 b617ddd200eb
child 23607 6a8fb529b542
permissions -rw-r--r--
reflection and reification methods now manage Context data
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
chaieb@23546
    10
  uses "reflection_data.ML" ("reflection.ML")
wenzelm@20319
    11
begin
wenzelm@20319
    12
chaieb@23546
    13
setup {* Reify_Data.setup*}
chaieb@23546
    14
chaieb@23546
    15
chaieb@20374
    16
lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
chaieb@20374
    17
  by (blast intro: ext)
chaieb@22199
    18
chaieb@20374
    19
use "reflection.ML"
chaieb@23546
    20
ML{* Reify_Data.get @{context}*}
chaieb@20374
    21
wenzelm@20319
    22
method_setup reify = {*
wenzelm@20319
    23
  fn src =>
wenzelm@20319
    24
    Method.syntax (Attrib.thms --
wenzelm@20319
    25
      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
chaieb@23546
    26
  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ Reify_Data.get ctxt) to))
wenzelm@20319
    27
*} "partial automatic reification"
wenzelm@20319
    28
wenzelm@20319
    29
method_setup reflection = {*
wenzelm@20319
    30
  fn src =>
wenzelm@20319
    31
    Method.syntax (Attrib.thms --
wenzelm@20319
    32
      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
chaieb@23546
    33
  (fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt (ths @ Reify_Data.get ctxt) to))
wenzelm@20319
    34
*} "reflection method"
wenzelm@20319
    35
wenzelm@20319
    36
end