src/HOL/ex/reflection_data.ML
author wenzelm
Sun Jul 29 14:30:01 2007 +0200 (2007-07-29)
changeset 24045 bead02a55952
parent 23647 89286c4e7928
child 25979 3297781f8141
permissions -rw-r--r--
renamed Drule.add/del/merge_rules to Thm.add/del/merge_thms;
tuned;
chaieb@23545
     1
(*  Title:      HOL/ex/reflection_data.ML
chaieb@23545
     2
    ID:         $Id$
chaieb@23545
     3
    Author:     Amine Chaieb, TU Muenchen
chaieb@23545
     4
wenzelm@24045
     5
Data for the reification and reflection methods.
chaieb@23545
     6
*)
chaieb@23545
     7
chaieb@23545
     8
signature REIFY_DATA =
chaieb@23545
     9
sig
wenzelm@24045
    10
  type entry = thm list * thm list
chaieb@23545
    11
  val get: Proof.context -> entry
chaieb@23606
    12
  val del: attribute
wenzelm@24045
    13
  val add: attribute
chaieb@23545
    14
  val setup: theory -> theory
chaieb@23545
    15
end;
chaieb@23545
    16
chaieb@23545
    17
structure Reify_Data : REIFY_DATA =
chaieb@23545
    18
struct
chaieb@23545
    19
wenzelm@24045
    20
type entry = thm list * thm list;
chaieb@23545
    21
chaieb@23545
    22
structure Data = GenericDataFun
wenzelm@24045
    23
(
chaieb@23647
    24
  type T = entry
wenzelm@24045
    25
  val empty = ([], [])
chaieb@23545
    26
  val extend = I
wenzelm@24045
    27
  fun merge _ = pairself Thm.merge_thms
wenzelm@24045
    28
);
chaieb@23545
    29
chaieb@23545
    30
val get = Data.get o Context.Proof;
chaieb@23545
    31
wenzelm@24045
    32
val add = Thm.declaration_attribute (fn th => fn context =>
wenzelm@24045
    33
  context |> Data.map (apfst (Thm.add_thm th)))
chaieb@23545
    34
wenzelm@24045
    35
val del = Thm.declaration_attribute (fn th => fn context =>
wenzelm@24045
    36
  context |> Data.map (apfst (Thm.del_thm th)))
chaieb@23647
    37
wenzelm@24045
    38
val radd = Thm.declaration_attribute (fn th => fn context =>
wenzelm@24045
    39
  context |> Data.map (apsnd (Thm.add_thm th)))
chaieb@23647
    40
wenzelm@24045
    41
val rdel = Thm.declaration_attribute (fn th => fn context =>
wenzelm@24045
    42
  context |> Data.map (apsnd (Thm.del_thm th)))
chaieb@23545
    43
chaieb@23545
    44
(* concrete syntax *)
chaieb@23606
    45
(*
chaieb@23545
    46
local
chaieb@23545
    47
fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
chaieb@23545
    48
chaieb@23545
    49
val constsN = "consts";
chaieb@23545
    50
val addN = "add";
chaieb@23545
    51
val delN = "del";
chaieb@23545
    52
val any_keyword = keyword constsN || keyword addN || keyword delN;
chaieb@23545
    53
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
chaieb@23545
    54
val terms = thms >> map (term_of o Drule.dest_term);
chaieb@23545
    55
chaieb@23545
    56
fun optional scan = Scan.optional scan [];
chaieb@23545
    57
chaieb@23545
    58
in
chaieb@23545
    59
fun att_syntax src = src |> Attrib.syntax
chaieb@23545
    60
 ((Scan.lift (Args.$$$ "del") |-- thms) >> del ||
chaieb@23545
    61
  optional (keyword addN |-- thms) >> add)
chaieb@23545
    62
end;
chaieb@23606
    63
*)
chaieb@23545
    64
chaieb@23545
    65
(* theory setup *)
chaieb@23545
    66
 val setup =
chaieb@23647
    67
  Attrib.add_attributes [("reify", Attrib.add_del_args add del, "Reify data"),
chaieb@23647
    68
                         ("reflection", Attrib.add_del_args radd rdel, "Reflection data")];
chaieb@23545
    69
end;