src/HOL/ex/Reflection.thy
author wenzelm
Wed Nov 29 15:44:51 2006 +0100 (2006-11-29)
changeset 21588 cd0dc678a205
parent 20374 01b711328990
child 21879 a3efbae45735
permissions -rw-r--r--
simplified method setup;
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@20374
    10
uses ("reflection.ML")
wenzelm@20319
    11
begin
wenzelm@20319
    12
chaieb@20374
    13
lemma ext2: "(\<forall>x. f x = g x) \<Longrightarrow> f = g"
chaieb@20374
    14
  by (blast intro: ext)
chaieb@20374
    15
use "reflection.ML"
chaieb@20374
    16
wenzelm@20319
    17
method_setup reify = {*
wenzelm@20319
    18
  fn src =>
wenzelm@20319
    19
    Method.syntax (Attrib.thms --
wenzelm@20319
    20
      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
wenzelm@21588
    21
  (fn (ctxt, (eqs,to)) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt eqs to))
wenzelm@20319
    22
*} "partial automatic reification"
wenzelm@20319
    23
wenzelm@20319
    24
method_setup reflection = {*
wenzelm@20319
    25
  fn src =>
wenzelm@20319
    26
    Method.syntax (Attrib.thms --
wenzelm@20319
    27
      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
wenzelm@21588
    28
  (fn (ctxt, (ths,to)) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt ths to))
wenzelm@20319
    29
*} "reflection method"
wenzelm@20319
    30
wenzelm@20319
    31
end