src/HOL/Library/Reflection.thy
author haftmann
Fri Mar 02 15:18:05 2012 +0100 (2012-03-02)
changeset 46764 a65e18ceb1e3
parent 46510 696f3fec3f83
child 46765 07f9eda810b3
permissions -rw-r--r--
tuned import
haftmann@29650
     1
(*  Title:      HOL/Library/Reflection.thy
wenzelm@20319
     2
    Author:     Amine Chaieb, TU Muenchen
wenzelm@20319
     3
*)
wenzelm@20319
     4
wenzelm@20319
     5
header {* Generic reflection and reification *}
wenzelm@20319
     6
wenzelm@20319
     7
theory Reflection
wenzelm@20319
     8
imports Main
haftmann@46764
     9
uses
haftmann@46764
    10
  "~~/src/HOL/Library/reify_data.ML"
haftmann@46764
    11
  "~~/src/HOL/Library/reflection.ML"
wenzelm@20319
    12
begin
wenzelm@20319
    13
haftmann@29650
    14
setup {* Reify_Data.setup *}
chaieb@23546
    15
wenzelm@30549
    16
method_setup reify = {*
wenzelm@30549
    17
  Attrib.thms --
wenzelm@30549
    18
    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
wenzelm@30549
    19
  (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
wenzelm@20319
    20
*} "partial automatic reification"
wenzelm@20319
    21
hoelzl@31412
    22
method_setup reflection = {*
hoelzl@31412
    23
let
haftmann@29650
    24
  fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
haftmann@29650
    25
  val onlyN = "only";
haftmann@29650
    26
  val rulesN = "rules";
haftmann@29650
    27
  val any_keyword = keyword onlyN || keyword rulesN;
haftmann@29650
    28
  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
haftmann@29650
    29
  val terms = thms >> map (term_of o Drule.dest_term);
wenzelm@30549
    30
in
wenzelm@30549
    31
  thms --
wenzelm@30549
    32
  Scan.optional (keyword rulesN |-- thms) [] --
wenzelm@30549
    33
  Scan.option (keyword onlyN |-- Args.term) >>
wenzelm@30549
    34
  (fn ((eqs,ths),to) => fn ctxt =>
hoelzl@31412
    35
    let
hoelzl@31412
    36
      val (ceqs,cths) = Reify_Data.get ctxt
wenzelm@30549
    37
      val corr_thms = ths@cths
wenzelm@30549
    38
      val raw_eqs = eqs@ceqs
wenzelm@30549
    39
    in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
wenzelm@30549
    40
end
wenzelm@42814
    41
*}
haftmann@29650
    42
wenzelm@20319
    43
end
haftmann@46764
    44