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