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