src/HOL/Import/import_data.ML
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 59936 b8ffc3dc9e24
child 69597 ff784d5a5bfb
permissions -rw-r--r--
executable domain membership checks
cezarykaliszyk@47258
     1
(*  Title:      HOL/Import/import_data.ML
cezarykaliszyk@47258
     2
    Author:     Cezary Kaliszyk, University of Innsbruck
cezarykaliszyk@47258
     3
    Author:     Alexander Krauss, QAware GmbH
cezarykaliszyk@47258
     4
cezarykaliszyk@47258
     5
Importer data.
cezarykaliszyk@47258
     6
*)
cezarykaliszyk@47258
     7
cezarykaliszyk@47258
     8
signature IMPORT_DATA =
cezarykaliszyk@47258
     9
sig
cezarykaliszyk@47258
    10
  val get_const_map : string -> theory -> string option
cezarykaliszyk@47258
    11
  val get_typ_map : string -> theory -> string option
cezarykaliszyk@47258
    12
  val get_const_def : string -> theory -> thm option
cezarykaliszyk@47258
    13
  val get_typ_def : string -> theory -> thm option
cezarykaliszyk@47258
    14
cezarykaliszyk@47258
    15
  val add_const_map : string -> string -> theory -> theory
wenzelm@56266
    16
  val add_const_map_cmd : string -> string -> theory -> theory
cezarykaliszyk@47258
    17
  val add_typ_map : string -> string -> theory -> theory
wenzelm@56266
    18
  val add_typ_map_cmd : string -> string -> theory -> theory
cezarykaliszyk@47258
    19
  val add_const_def : string -> thm -> string option -> theory -> theory
cezarykaliszyk@47258
    20
  val add_typ_def : string -> string -> string -> thm -> theory -> theory
cezarykaliszyk@47258
    21
end
cezarykaliszyk@47258
    22
cezarykaliszyk@47258
    23
structure Import_Data: IMPORT_DATA =
cezarykaliszyk@47258
    24
struct
cezarykaliszyk@47258
    25
cezarykaliszyk@47258
    26
structure Data = Theory_Data
cezarykaliszyk@47258
    27
(
cezarykaliszyk@47258
    28
  type T = {const_map: string Symtab.table, ty_map: string Symtab.table,
cezarykaliszyk@47258
    29
            const_def: thm Symtab.table, ty_def: thm Symtab.table}
cezarykaliszyk@47258
    30
  val empty = {const_map = Symtab.empty, ty_map = Symtab.empty,
cezarykaliszyk@47258
    31
               const_def = Symtab.empty, ty_def = Symtab.empty}
cezarykaliszyk@47258
    32
  val extend = I
cezarykaliszyk@47258
    33
  fun merge
cezarykaliszyk@47258
    34
   ({const_map = cm1, ty_map = tm1, const_def = cd1, ty_def = td1},
cezarykaliszyk@47258
    35
    {const_map = cm2, ty_map = tm2, const_def = cd2, ty_def = td2}) : T =
cezarykaliszyk@47258
    36
    {const_map = Symtab.merge (K true) (cm1, cm2), ty_map = Symtab.merge (K true) (tm1, tm2),
cezarykaliszyk@47258
    37
     const_def = Symtab.merge (K true) (cd1, cd2), ty_def = Symtab.merge (K true) (td1, td2)
cezarykaliszyk@47258
    38
    }
cezarykaliszyk@47258
    39
)
cezarykaliszyk@47258
    40
cezarykaliszyk@47258
    41
fun get_const_map s thy = Symtab.lookup (#const_map (Data.get thy)) s
cezarykaliszyk@47258
    42
cezarykaliszyk@47258
    43
fun get_typ_map s thy = Symtab.lookup (#ty_map (Data.get thy)) s
cezarykaliszyk@47258
    44
cezarykaliszyk@47258
    45
fun get_const_def s thy = Symtab.lookup (#const_def (Data.get thy)) s
cezarykaliszyk@47258
    46
cezarykaliszyk@47258
    47
fun get_typ_def s thy = Symtab.lookup (#ty_def (Data.get thy)) s
cezarykaliszyk@47258
    48
cezarykaliszyk@47258
    49
fun add_const_map s1 s2 thy =
cezarykaliszyk@47258
    50
  Data.map (fn {const_map, ty_map, const_def, ty_def} =>
cezarykaliszyk@47258
    51
    {const_map = (Symtab.update (s1, s2) const_map), ty_map = ty_map,
cezarykaliszyk@47258
    52
     const_def = const_def, ty_def = ty_def}) thy
cezarykaliszyk@47258
    53
wenzelm@56266
    54
fun add_const_map_cmd s1 raw_s2 thy =
wenzelm@56266
    55
  let
wenzelm@56266
    56
    val ctxt = Proof_Context.init_global thy
wenzelm@56266
    57
    val Const (s2, _) = Proof_Context.read_const {proper = true, strict = false} ctxt raw_s2
wenzelm@56266
    58
  in add_const_map s1 s2 thy end
wenzelm@56266
    59
cezarykaliszyk@47258
    60
fun add_typ_map s1 s2 thy =
cezarykaliszyk@47258
    61
  Data.map (fn {const_map, ty_map, const_def, ty_def} =>
cezarykaliszyk@47258
    62
    {const_map = const_map, ty_map = (Symtab.update (s1, s2) ty_map),
cezarykaliszyk@47258
    63
     const_def = const_def, ty_def = ty_def}) thy
cezarykaliszyk@47258
    64
wenzelm@56266
    65
fun add_typ_map_cmd s1 raw_s2 thy =
wenzelm@56266
    66
  let
wenzelm@56266
    67
    val ctxt = Proof_Context.init_global thy
wenzelm@56266
    68
    val Type (s2, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt raw_s2
wenzelm@56266
    69
  in add_typ_map s1 s2 thy end
wenzelm@56266
    70
cezarykaliszyk@47258
    71
fun add_const_def s th name_opt thy =
cezarykaliszyk@47258
    72
  let
cezarykaliszyk@47258
    73
    val th = Thm.legacy_freezeT th
cezarykaliszyk@47258
    74
    val name = case name_opt of
cezarykaliszyk@47258
    75
         NONE => (fst o dest_Const o fst o HOLogic.dest_eq o
wenzelm@59582
    76
           HOLogic.dest_Trueprop o Thm.prop_of) th
cezarykaliszyk@47258
    77
       | SOME n => n
cezarykaliszyk@47258
    78
    val thy' = add_const_map s name thy
cezarykaliszyk@47258
    79
  in
cezarykaliszyk@47258
    80
    Data.map (fn {const_map, ty_map, const_def, ty_def} =>
cezarykaliszyk@47258
    81
      {const_map = const_map, ty_map = ty_map,
cezarykaliszyk@47258
    82
       const_def = (Symtab.update (s, th) const_def), ty_def = ty_def}) thy'
cezarykaliszyk@47258
    83
  end
cezarykaliszyk@47258
    84
cezarykaliszyk@47258
    85
fun add_typ_def tyname absname repname th thy =
cezarykaliszyk@47258
    86
  let
cezarykaliszyk@47258
    87
    val th = Thm.legacy_freezeT th
wenzelm@59582
    88
    val (l, _) = dest_comb (HOLogic.dest_Trueprop (Thm.prop_of th))
cezarykaliszyk@47258
    89
    val (l, abst) = dest_comb l
cezarykaliszyk@47258
    90
    val (_, rept) = dest_comb l
cezarykaliszyk@47258
    91
    val (absn, _) = dest_Const abst
cezarykaliszyk@47258
    92
    val (repn, _) = dest_Const rept
cezarykaliszyk@47258
    93
    val nty = domain_type (fastype_of rept)
cezarykaliszyk@47258
    94
    val ntyn = fst (dest_Type nty)
cezarykaliszyk@47258
    95
    val thy2 = add_typ_map tyname ntyn thy
cezarykaliszyk@47258
    96
    val thy3 = add_const_map absname absn thy2
cezarykaliszyk@47258
    97
    val thy4 = add_const_map repname repn thy3
cezarykaliszyk@47258
    98
  in
cezarykaliszyk@47258
    99
    Data.map (fn {const_map, ty_map, const_def, ty_def} =>
cezarykaliszyk@47258
   100
      {const_map = const_map, ty_map = ty_map,
cezarykaliszyk@47258
   101
       const_def = const_def, ty_def = (Symtab.update (tyname, th) ty_def)}) thy4
cezarykaliszyk@47258
   102
  end
cezarykaliszyk@47258
   103
wenzelm@53171
   104
val _ = Theory.setup
wenzelm@53172
   105
  (Attrib.setup @{binding import_const}
wenzelm@56266
   106
    (Scan.lift Parse.name --
wenzelm@56266
   107
      Scan.option (Scan.lift @{keyword ":"} |-- Args.const {proper = true, strict = false}) >>
wenzelm@53172
   108
      (fn (s1, s2) => Thm.declaration_attribute
wenzelm@53172
   109
        (fn th => Context.mapping (add_const_def s1 th s2) I)))
wenzelm@53172
   110
  "declare a theorem as an equality that maps the given constant")
cezarykaliszyk@47258
   111
wenzelm@53171
   112
val _ = Theory.setup
wenzelm@53172
   113
  (Attrib.setup @{binding import_type}
wenzelm@53172
   114
    (Scan.lift (Parse.name -- Parse.name -- Parse.name) >>
wenzelm@53172
   115
      (fn ((tyname, absname), repname) => Thm.declaration_attribute
wenzelm@53172
   116
        (fn th => Context.mapping (add_typ_def tyname absname repname th) I)))
haftmann@58772
   117
  "declare a type_definition theorem as a map for an imported type with abs and rep")
cezarykaliszyk@47258
   118
wenzelm@53172
   119
val _ =
wenzelm@59936
   120
  Outer_Syntax.command @{command_keyword import_type_map}
wenzelm@53172
   121
    "map external type name to existing Isabelle/HOL type name"
wenzelm@56266
   122
    ((Parse.name --| @{keyword ":"}) -- Parse.type_const >>
wenzelm@56266
   123
      (fn (ty_name1, ty_name2) => Toplevel.theory (add_typ_map_cmd ty_name1 ty_name2)))
cezarykaliszyk@47258
   124
wenzelm@53172
   125
val _ =
wenzelm@59936
   126
  Outer_Syntax.command @{command_keyword import_const_map}
wenzelm@53172
   127
    "map external const name to existing Isabelle/HOL const name"
wenzelm@56266
   128
    ((Parse.name --| @{keyword ":"}) -- Parse.const >>
wenzelm@56266
   129
      (fn (cname1, cname2) => Toplevel.theory (add_const_map_cmd cname1 cname2)))
cezarykaliszyk@47258
   130
cezarykaliszyk@47258
   131
(* Initial type and constant maps, for types and constants that are not
cezarykaliszyk@47258
   132
   defined, which means their definitions do not appear in the proof dump *)
wenzelm@53171
   133
val _ = Theory.setup
wenzelm@53172
   134
  (add_typ_map "bool" @{type_name bool} #>
wenzelm@53172
   135
  add_typ_map "fun" @{type_name fun} #>
wenzelm@53172
   136
  add_typ_map "ind" @{type_name ind} #>
wenzelm@53172
   137
  add_const_map "=" @{const_name HOL.eq} #>
wenzelm@53171
   138
  add_const_map "@" @{const_name "Eps"})
cezarykaliszyk@47258
   139
cezarykaliszyk@47258
   140
end