src/HOL/Library/Reflection.thy
author wenzelm
Tue Mar 26 20:02:02 2013 +0100 (2013-03-26)
changeset 51542 738598beeb26
parent 48891 c0eafbd55de3
child 51723 da12e44b2d65
permissions -rw-r--r--
tuned imports;
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
wenzelm@20319
     9
begin
wenzelm@20319
    10
wenzelm@51542
    11
ML_file "reify_data.ML"
wenzelm@51542
    12
ML_file "reflection.ML"
wenzelm@48891
    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.$$$ ")")) >>
haftmann@46765
    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) >>
haftmann@46765
    34
  (fn ((eqs, ths), to) => fn ctxt =>
hoelzl@31412
    35
    let
haftmann@46765
    36
      val (ceqs, cths) = Reify_Data.get ctxt
haftmann@46765
    37
      val corr_thms = ths @ cths
haftmann@46765
    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