src/HOL/Library/Reflection.thy
author wenzelm
Mon Dec 28 01:28:28 2015 +0100 (2015-12-28)
changeset 61945 1135b8de26c3
parent 61476 1884c40f1539
child 69605 a96320074298
permissions -rw-r--r--
more symbols;
haftmann@29650
     1
(*  Title:      HOL/Library/Reflection.thy
wenzelm@20319
     2
    Author:     Amine Chaieb, TU Muenchen
wenzelm@20319
     3
*)
wenzelm@20319
     4
wenzelm@60500
     5
section \<open>Generic reflection and reification\<close>
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@60500
    13
method_setup reify = \<open>
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@60500
    17
\<close> "partial automatic reification"
wenzelm@20319
    18
wenzelm@60500
    19
method_setup reflection = \<open>
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;
wenzelm@61476
    25
  val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm);
wenzelm@59582
    26
  val terms = thms >> map (Thm.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
wenzelm@60500
    33
\<close> "partial automatic reflection"
haftmann@29650
    34
wenzelm@20319
    35
end
haftmann@46764
    36