src/HOL/Library/Reflection.thy
author haftmann
Sun Apr 21 10:41:18 2013 +0200 (2013-04-21)
changeset 51726 b3e599b5ecc8
parent 51723 da12e44b2d65
child 58881 b9556a055632
permissions -rw-r--r--
reflection as official HOL tool
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
haftmann@51726
    11
ML_file "~~/src/HOL/Tools/reflection.ML"
wenzelm@48891
    12
wenzelm@30549
    13
method_setup reify = {*
wenzelm@30549
    14
  Attrib.thms --
wenzelm@30549
    15
    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
haftmann@51723
    16
      (fn (user_eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.default_reify_tac ctxt user_eqs to))
wenzelm@20319
    17
*} "partial automatic reification"
wenzelm@20319
    18
hoelzl@31412
    19
method_setup reflection = {*
hoelzl@31412
    20
let
haftmann@29650
    21
  fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
haftmann@29650
    22
  val onlyN = "only";
haftmann@29650
    23
  val rulesN = "rules";
haftmann@29650
    24
  val any_keyword = keyword onlyN || keyword rulesN;
haftmann@29650
    25
  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
haftmann@29650
    26
  val terms = thms >> map (term_of o Drule.dest_term);
wenzelm@30549
    27
in
haftmann@51723
    28
  thms -- Scan.optional (keyword rulesN |-- thms) [] --
haftmann@51723
    29
    Scan.option (keyword onlyN |-- Args.term) >>
haftmann@51723
    30
  (fn ((user_eqs, user_thms), to) => fn ctxt =>
haftmann@51723
    31
        SIMPLE_METHOD' (Reflection.default_reflection_tac ctxt user_thms user_eqs to))
wenzelm@30549
    32
end
haftmann@51723
    33
*} "partial automatic reflection"
haftmann@29650
    34
wenzelm@20319
    35
end
haftmann@46764
    36