src/HOL/Library/Reflection.thy
author wenzelm
Wed, 17 Jun 2015 11:03:05 +0200
changeset 60500 903bb1495239
parent 59582 0fbed69ff081
child 61476 1884c40f1539
permissions -rw-r--r--
isabelle update_cartouches;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
     1
(*  Title:      HOL/Library/Reflection.thy
20319
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
     2
    Author:     Amine Chaieb, TU Muenchen
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
     3
*)
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
     4
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 59582
diff changeset
     5
section \<open>Generic reflection and reification\<close>
20319
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
     6
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
     7
theory Reflection
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
     8
imports Main
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
     9
begin
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
    10
51726
b3e599b5ecc8 reflection as official HOL tool
haftmann
parents: 51723
diff changeset
    11
ML_file "~~/src/HOL/Tools/reflection.ML"
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46765
diff changeset
    12
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 59582
diff changeset
    13
method_setup reify = \<open>
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    14
  Attrib.thms --
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    15
    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
51723
da12e44b2d65 combined reify_data.ML into reflection.ML;
haftmann
parents: 51542
diff changeset
    16
      (fn (user_eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.default_reify_tac ctxt user_eqs to))
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 59582
diff changeset
    17
\<close> "partial automatic reification"
20319
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
    18
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 59582
diff changeset
    19
method_setup reflection = \<open>
31412
f2e6b6526092 Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations.
hoelzl
parents: 30549
diff changeset
    20
let
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    21
  fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    22
  val onlyN = "only";
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    23
  val rulesN = "rules";
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    24
  val any_keyword = keyword onlyN || keyword rulesN;
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    25
  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 58881
diff changeset
    26
  val terms = thms >> map (Thm.term_of o Drule.dest_term);
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    27
in
51723
da12e44b2d65 combined reify_data.ML into reflection.ML;
haftmann
parents: 51542
diff changeset
    28
  thms -- Scan.optional (keyword rulesN |-- thms) [] --
da12e44b2d65 combined reify_data.ML into reflection.ML;
haftmann
parents: 51542
diff changeset
    29
    Scan.option (keyword onlyN |-- Args.term) >>
da12e44b2d65 combined reify_data.ML into reflection.ML;
haftmann
parents: 51542
diff changeset
    30
  (fn ((user_eqs, user_thms), to) => fn ctxt =>
da12e44b2d65 combined reify_data.ML into reflection.ML;
haftmann
parents: 51542
diff changeset
    31
        SIMPLE_METHOD' (Reflection.default_reflection_tac ctxt user_thms user_eqs to))
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    32
end
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 59582
diff changeset
    33
\<close> "partial automatic reflection"
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    34
20319
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
    35
end
46764
a65e18ceb1e3 tuned import
haftmann
parents: 46510
diff changeset
    36