1signature OpenTheoryReader = sig
2type term = Term.term type hol_type = Type.hol_type type thm = Thm.thm
3type thy_tyop  = OpenTheoryMap.thy_tyop
4type thy_const = OpenTheoryMap.thy_const
5type otname    = OpenTheoryMap.otname
6
7(* record of data an article reader must provide: *)
8type reader = {
9  define_tyop  : {name:thy_tyop, ax:thm, args:hol_type list, rep:thy_const, abs:thy_const} ->
10                 {rep_abs:thm, abs_rep:thm},
11  define_const : thy_const -> term -> thm,
12  axiom        : thm Net.net -> (term list * term) -> thm,
13  const_name   : otname -> thy_const,
14  tyop_name    : otname -> thy_tyop}
15
16(*
17[define_tyop r] will be called when the article wants to define a type. [r]
18consists of the name of the type operator to be defined, the type axiom, a list
19of arguments (type variables) for the type operator in the desired order, and
20the names of the rep and abs constants. The call must return the type bijection
21theorems. The type axiom will be of the form |- P t. The bijection theorems
22should be:
23  abs_rep = |- (\a. abs (rep a)) = (\a. a)
24  rep_abs = |- (\r. rep(abs r) = r) = (\r. P r)
25
26[define_const name rhs] will be called when the article wants to define a new
27constant. The call must return a theorem |- const = rhs, where [const] is the
28constant with name [name].
29
30[axiom thms (h,c)] will be called when the article wants to retrieve an
31assumption or an axiom. [thms] is the collection of theorems the article has
32already proved, represented by a conclusion-indexed net. The call must return a
33theorem h |- c.
34
35[const_name n] and [tyop_name n] will be called to translate OpenTheory names
36to HOL4 names. The following functions can be used to simply look the names up in the global OpenTheory map.
37*)
38val const_name_in_map : otname -> thy_const
39val tyop_name_in_map  : otname -> thy_tyop
40
41val axiom_in_db : thm Net.net -> (term list * term) -> thm
42(*
43An axiom function for readers that tries to find the desired theorem in the
44following places (in order): an internal list of theorems that should be in
45the OpenTheory base package, the HOL4 database (via DB.match []), and the
46theorems already proved by the article.
47*)
48
49val define_tyop_in_thy :
50  {name:thy_tyop, ax:thm, args:hol_type list, rep:thy_const, abs:thy_const}
51    -> {rep_abs:thm, abs_rep:thm}
52val define_const_in_thy : (string -> string) -> thy_const -> term -> thm
53(*
54define_tyop and define_const functions for readers that try to produce the
55desired theorems by actually defining a new type or constant in the current
56theory. They fail if the theory of the type or constant desired is not the
57current theory. The first argument to [define_const_in_thy] is a function to
58produce the prefix of the ML name of the constant's definition from the
59constant's name (useful when a constant's name is not a valid ML identifier).
60*)
61
62val raw_read_article : TextIO.instream -> reader -> thm Net.net
63val read_article     : string -> reader -> thm Net.net
64
65val delete_unused_consts : thm list -> unit
66(*
67Given a list (usually by calling [Net.listItems] on the result of
68[read_article]), calls [Theory.delete_const] on any constants in the current
69theory that do not appear in some theorem in the list.
70*)
71
72val NUMERAL_conv : Conv.conv
73
74val uneta_type_bijection : thm -> thm
75
76end
77