src/HOL/Library/Reflection.thy
author wenzelm
Wed, 22 Aug 2012 22:55:41 +0200
changeset 48891 c0eafbd55de3
parent 46765 07f9eda810b3
child 51542 738598beeb26
permissions -rw-r--r--
prefer ML_file over old uses;
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
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
     5
header {* Generic reflection and reification *}
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
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46765
diff changeset
    11
ML_file "~~/src/HOL/Library/reify_data.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46765
diff changeset
    12
ML_file "~~/src/HOL/Library/reflection.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46765
diff changeset
    13
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    14
setup {* Reify_Data.setup *}
23546
c8a1bd9585a0 reflection and reification methods now manage Context data
chaieb
parents: 22199
diff changeset
    15
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    16
method_setup reify = {*
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    17
  Attrib.thms --
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    18
    Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")")) >>
46765
07f9eda810b3 tuned whitespace
haftmann
parents: 46764
diff changeset
    19
  (fn (eqs, to) => fn ctxt => SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ fst (Reify_Data.get ctxt)) to))
20319
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
    20
*} "partial automatic reification"
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
    21
31412
f2e6b6526092 Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations.
hoelzl
parents: 30549
diff changeset
    22
method_setup reflection = {*
f2e6b6526092 Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations.
hoelzl
parents: 30549
diff changeset
    23
let
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    24
  fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    25
  val onlyN = "only";
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    26
  val rulesN = "rules";
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    27
  val any_keyword = keyword onlyN || keyword rulesN;
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    28
  val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    29
  val terms = thms >> map (term_of o Drule.dest_term);
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    30
in
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    31
  thms --
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    32
  Scan.optional (keyword rulesN |-- thms) [] --
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    33
  Scan.option (keyword onlyN |-- Args.term) >>
46765
07f9eda810b3 tuned whitespace
haftmann
parents: 46764
diff changeset
    34
  (fn ((eqs, ths), to) => fn ctxt =>
31412
f2e6b6526092 Converted reification to use fold_map instead of Library.foldl_map. Use antiquotations.
hoelzl
parents: 30549
diff changeset
    35
    let
46765
07f9eda810b3 tuned whitespace
haftmann
parents: 46764
diff changeset
    36
      val (ceqs, cths) = Reify_Data.get ctxt
07f9eda810b3 tuned whitespace
haftmann
parents: 46764
diff changeset
    37
      val corr_thms = ths @ cths
07f9eda810b3 tuned whitespace
haftmann
parents: 46764
diff changeset
    38
      val raw_eqs = eqs @ ceqs
30549
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    39
    in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
d2d7874648bd simplified method setup;
wenzelm
parents: 30510
diff changeset
    40
end
42814
5af15f1e2ef6 simplified/unified method_setup/attribute_setup;
wenzelm
parents: 31412
diff changeset
    41
*}
29650
cc3958d31b1d Reflection.thy now in HOL/Library
haftmann
parents: 23649
diff changeset
    42
20319
a8761e8568de Generic reflection and reification (by Amine Chaieb).
wenzelm
parents:
diff changeset
    43
end
46764
a65e18ceb1e3 tuned import
haftmann
parents: 46510
diff changeset
    44