1signature polytypicLib =
2sig
3        include Abbrev
4
5(* The types required *)
6type ('a,'b) dict = ('a,'b) Binarymap.dict
7type proof = proofManagerLib.proof;
8
9(* The types defined *)
10        type translation_scheme =
11                {target : hol_type, induction : thm, recursion : thm,
12                left : term, right : term, predicate : term,
13                bottom : term, bottom_thm : thm};
14        type function =
15                {const : term, definition : thm,
16                induction : (thm * (term * (term * hol_type)) list) option}
17        datatype exception_level = Standard | Fatal | Debug;
18
19(* The exception constructor *)
20        val polyExn : exception_level * string list * string -> exn
21
22        val cstores : (string, hol_type list ref) dict ref;
23
24(* Exception handling functions *)
25        val exn_to_string : exn -> string
26        val Raise : exn -> 'a
27        val isFatal : exn -> bool
28        val wrapException : string -> exn -> 'a
29        val wrapExceptionHOL : string -> exn -> 'a
30        val mkStandardExn : string -> string -> exn
31        val mkFatalExn : string -> string -> exn
32        val mkDebugExn : string -> string -> exn
33        val tryfind_e : exn -> ('a -> 'b) -> 'a list -> 'b
34        val first_e : exn -> ('a -> bool) -> 'a list -> 'a
35        val can : ('a -> 'b) -> 'a -> bool
36        val total : ('a -> 'b) -> 'a -> 'b option
37        val repeat : ('a -> 'a) -> 'a -> 'a
38        val debug  : bool ref
39        val assert : string -> (string * ('a -> bool)) list -> 'a -> 'a
40        val guarenteed : ('a -> 'b) -> 'a -> 'b
41
42(* Tracing functions *)
43        val type_trace : int -> string -> unit
44        val xlist_to_string : ('a -> string) -> 'a list -> string
45        val xpair_to_string : ('a -> string) -> ('b -> string) -> 'a * 'b -> string
46
47(* Input testing *)
48        val both : bool * bool -> bool
49        val is_conjunction_of : (term -> bool) -> term -> bool
50        val is_disjunction_of : (term -> bool) -> term -> bool
51        val is_implication_of : (term -> bool) -> (term -> bool) -> term -> bool
52        val is_anything : term -> bool
53        val is_source_function : term -> bool
54        val is_target_function : term -> bool
55        val is_expanded_function : term -> bool
56        val is_single_constructor : translation_scheme -> term -> bool
57        val is_double_term_target : translation_scheme -> term list -> term -> term -> bool
58        val is_double_term_source : term list -> term -> term -> bool
59
60(* List manipulation tools *)
61        val pick_e : exn -> ('a -> 'b) -> 'a list -> 'b * 'a list
62        val bucket_alist : (''a * 'b) list -> (''a * 'b list) list
63        val mappartition : ('a -> 'b) -> 'a list -> 'b list * 'a list
64        val reachable_graph : (''a -> ''a list) -> ''a -> (''a * ''a) list
65        val TC : (''a * ''a) list -> (''a * ''a) list
66        val RTC : (''a * ''a) list -> (''a * ''a) list
67
68(* Term manipulation tools *)
69        val list_mk_cond : (term * term) list -> term -> term
70        val imk_comb : (term * term) -> term
71        val rimk_comb : (term * term) -> term
72        val list_imk_comb : (term * term list) -> term
73        val full_beta_conv : term -> term
74        val full_beta      : term -> term
75
76(* Theorem manipulation tools *)
77        val UNDISCH_ONLY : thm -> thm
78        val UNDISCH_ALL_ONLY : thm -> thm
79        val CONJUNCTS_HYP : term -> thm -> thm
80        val CONV_HYP : (term -> thm) -> thm -> thm
81        val CHOOSE_L : term list * thm -> thm -> thm
82        val GEN_THM : term list -> thm -> thm
83        val PROVE_HYP_CHECK : thm -> thm -> thm
84        val ADDR_AND_CONV : term -> term -> thm
85        val ADDL_AND_CONV : term -> term -> thm
86        val MATCH_CONV : thm -> term -> thm
87        val ORDER_FORALL_CONV : term list -> term -> thm
88        val ORDER_EXISTS_CONV : term list -> term -> thm
89        val FUN_EQ_CONV : term -> thm
90        val UNFUN_EQ_CONV : term -> thm
91        val UNBETA_LIST_CONV : term list -> term -> thm
92        val NTH_CONJ_CONV : int -> (term -> thm) -> term -> thm
93        val PUSH_COND_CONV : term -> thm
94        val CASE_SPLIT_CONV : term -> thm
95        val MK_CONJ : thm -> thm -> thm
96        val LIST_MK_CONJ : thm list -> thm
97        val TC_THMS : thm list -> thm list
98        val prove_rec_fn_exists : thm -> term -> thm
99        val UNDISCH_EQ : thm -> thm
100        val UNDISCH_ALL_EQ : thm -> thm
101        val UNDISCH_CONJ : thm -> thm
102        val DISCH_LIST_CONJ : term list -> thm -> thm
103        val DISCH_ALL_CONJ : thm -> thm
104        val MATCH_CONC : thm -> term -> thm
105
106(* Type manipulation tools *)
107        val constructors_of : hol_type -> term list
108        val base26 : int -> char list
109        val base_type : hol_type -> hol_type
110        val cannon_type : hol_type -> hol_type
111        val sub_types : hol_type -> hol_type list
112        val uncurried_subtypes : hol_type -> hol_type list
113        val split_nested_recursive_set : hol_type -> (hol_type * (hol_type list * hol_type list)) list
114        val zip_on_types : ('a -> hol_type) -> ('b -> hol_type) -> 'a list -> 'b list -> ('a * 'b) list
115        val get_type_string : hol_type -> string
116        val SAFE_INST_TYPE : {redex : hol_type, residue : hol_type} list -> thm -> thm
117        val safe_inst : {redex : hol_type, residue : hol_type} list -> term -> term
118        val safe_type_subst : {redex : hol_type, residue : hol_type} list -> hol_type -> hol_type
119        val delete_matching_types : hol_type list -> hol_type -> hol_type
120        val all_types : hol_type -> hol_type list
121        val relevant_types : hol_type -> hol_type list
122
123(* Function splitting *)
124        val RFUN_CONV : thm list -> term -> thm
125        val SPLIT_HFUN_CONV : thm -> term list -> term -> thm list * term list * thm
126        val SPLIT_PAIR_CONV : (term list -> term -> term -> bool) -> term list -> thm -> term -> thm list * term list * thm
127        val SPLIT_FUNCTION_CONV : (term list -> term -> term -> bool) * thm -> thm list -> term -> thm
128
129(* Split function definition *)
130        val build_call_graph : term * term -> term list -> (int * (int list * int list)) list
131        val create_mutual_theorem : (int * (int list * int list)) list -> thm -> thm
132        val instantiate_mutual_theorem : thm -> term list -> thm
133        val create_ind_theorem : (int * (int list * int list)) list -> translation_scheme -> thm
134        val prove_recind_thms_mutual : translation_scheme -> term -> thm * thm
135        val LEQ_REWRITES : term -> term -> thm list -> thm
136        val prove_induction_recursion_thms : translation_scheme -> term -> thm * (term * term) list * thm
137
138(* The function and theorem database *)
139        val get_translation_scheme : hol_type -> translation_scheme
140        val exists_translation_precise : hol_type -> hol_type -> bool
141        val exists_translation : hol_type -> hol_type -> bool
142        val add_translation : hol_type -> hol_type -> unit
143        val add_translation_precise : hol_type -> hol_type -> unit
144        val get_translation_precise : hol_type -> hol_type -> (string,function) dict ref
145        val get_translation : hol_type -> hol_type -> (string,function) dict ref
146        val get_theorems_precise : hol_type -> hol_type -> (string, thm) dict ref
147        val get_theorems : hol_type -> hol_type -> (string, thm) dict ref
148        val get_translation_types : hol_type -> hol_type list
149        val add_translation_scheme : hol_type -> thm -> thm -> unit
150        val clearCoding : unit -> unit
151        val clearSource : unit -> unit
152        val most_precise_type : (hol_type -> bool) -> hol_type -> hol_type
153
154(* Function retrieval *)
155        val exists_coding_function_precise : hol_type -> hol_type -> string -> bool
156        val exists_coding_function : hol_type -> hol_type -> string -> bool
157        val get_coding_function_precise : hol_type -> hol_type -> string -> function
158        val get_coding_function : hol_type -> hol_type -> string -> function
159        val get_coding_function_def : hol_type -> hol_type -> string -> thm
160        val get_coding_function_const : hol_type -> hol_type -> string -> term
161        val get_coding_function_induction : hol_type -> hol_type -> string -> thm * (term * (term * hol_type)) list
162        val get_coding_function_precise_def : hol_type -> hol_type -> string -> thm
163        val get_coding_function_precise_const : hol_type -> hol_type -> string -> term
164        val get_coding_function_precise_induction : hol_type -> hol_type -> string -> thm * (term * (term * hol_type)) list
165        val add_coding_function_precise : hol_type -> hol_type -> string -> function -> unit
166        val add_coding_function : hol_type -> hol_type -> string -> function -> unit
167        val exists_source_function_precise : hol_type -> string -> bool
168        val exists_source_function : hol_type -> string -> bool
169        val get_source_function_precise : hol_type -> string -> function
170        val get_source_function : hol_type -> string -> function
171        val get_source_function_def : hol_type -> string -> thm
172        val get_source_function_const : hol_type -> string -> term
173        val get_source_function_induction : hol_type -> string -> thm * (term * (term * hol_type)) list
174        val get_source_function_precise_def : hol_type -> string -> thm
175        val get_source_function_precise_const : hol_type -> string -> term
176        val get_source_function_precise_induction : hol_type -> string -> thm * (term * (term * hol_type)) list
177        val add_source_function_precise : hol_type -> string -> function -> unit
178        val add_source_function : hol_type -> string -> function -> unit
179
180(* Theorem retrieval *)
181        val exists_coding_theorem_precise : hol_type -> hol_type -> string -> bool
182        val exists_coding_theorem : hol_type -> hol_type -> string -> bool
183        val add_coding_theorem_precise : hol_type -> hol_type -> string -> thm -> unit
184        val add_coding_theorem : hol_type -> hol_type -> string -> thm -> unit
185        val get_coding_theorem_precise : hol_type -> hol_type -> string -> thm
186        val get_coding_theorem : hol_type -> hol_type -> string -> thm
187        val exists_source_theorem_precise : hol_type -> string -> bool
188        val exists_source_theorem : hol_type -> string -> bool
189        val get_source_theorem_precise : hol_type -> string -> thm
190        val get_source_theorem : hol_type -> string -> thm
191        val add_source_theorem_precise : hol_type -> string -> thm -> unit
192        val add_source_theorem : hol_type -> string -> thm -> unit
193        val remove_source_theorem_precise : hol_type -> string -> unit
194        val remove_coding_theorem_precise : hol_type -> hol_type -> string -> unit
195
196(* Function creation tools *)
197        val inst_function_def : (hol_type -> thm) -> (hol_type -> term) -> hol_type -> thm
198        val expanded_function_def : (term -> thm) -> (term -> thm) -> (hol_type -> thm) -> hol_type -> term list -> thm
199        val mk_split_source_function : (hol_type -> term) -> (hol_type -> thm) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) -> hol_type -> thm * thm
200        val mk_split_target_function : (hol_type -> term) -> (hol_type -> thm) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) ->
201                                        translation_scheme -> hol_type -> (thm * (term * term) list * thm) * thm
202
203(* Removal of function splits *)
204        val MATCH_IND_TERM : term -> thm -> thm
205        val strengthen_proof_term : thm list -> term -> thm
206        val prove_split_term : (term * (term * hol_type)) list -> thm -> thm -> thm * term -> term -> thm
207        val prove_all_split_terms : (hol_type -> thm * (term * (term * hol_type)) list) * (hol_type -> thm) * (term -> thm) * (term -> thm) * thm * term ->
208                                                (term * hol_type) list -> thm -> thm list * thm
209        val remove_hyp_terms : thm -> thm list -> thm list * thm -> thm
210        val match_mapping : thm -> (term * term) list -> (hol_type -> term) -> thm -> hol_type -> (term * (term * hol_type)) list
211        val unsplit_function : (hol_type -> thm * (term * (term * hol_type)) list) -> (hol_type -> thm) -> (hol_type -> term) ->
212                                                (term -> thm) -> (term -> thm) -> thm * term -> hol_type -> thm * thm -> thm
213
214(* Full function creation *)
215        val mk_source_functions : string -> (hol_type -> term) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) -> hol_type -> unit
216        val mk_coding_functions : string -> (hol_type -> term) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) -> hol_type -> hol_type -> unit
217        val mk_target_functions : string -> (hol_type -> term) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) -> hol_type -> hol_type -> unit
218
219(* Automatic generation of functions *)
220        val add_coding_function_generator : hol_type -> string -> (hol_type -> bool) -> (hol_type -> function) -> unit
221        val add_source_function_generator : string -> (hol_type -> bool) -> (hol_type -> function) -> unit
222        val generate_coding_function : hol_type -> string -> hol_type -> unit
223        val generate_source_function : string -> hol_type -> unit
224        val add_compound_coding_function_generator : string -> (hol_type -> term) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) -> hol_type -> unit
225        val add_compound_target_function_generator : string -> (hol_type -> term) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) -> hol_type -> unit
226        val add_compound_source_function_generator : string -> (hol_type -> term) -> (hol_type -> term) -> (term -> thm) -> (term -> thm) -> unit
227
228(* Automatic generation of theorems *)
229        val generate_coding_theorem : hol_type -> string -> hol_type -> thm
230        val generate_source_theorem : string -> hol_type -> thm
231        val set_coding_theorem_conclusion : hol_type -> string -> (hol_type -> term) -> unit
232        val set_source_theorem_conclusion : string -> (hol_type -> term) -> unit
233        val get_coding_theorem_conclusion : hol_type -> string -> (hol_type -> term)
234        val get_source_theorem_conclusion : string -> (hol_type -> term)
235        val exists_coding_theorem_conclusion : hol_type -> string -> bool
236        val exists_source_theorem_conclusion : string -> bool
237        val make_predicate_map : thm -> (term * term list) list
238        val inductive_coding_goal : string -> (hol_type -> term) -> hol_type -> hol_type -> (term -> thm) -> proof
239        val inductive_source_goal : string -> (hol_type -> term) -> hol_type -> (term -> thm) -> proof
240        val add_inductive_coding_theorem_generator : string -> string -> hol_type -> (term -> thm) -> (hol_type -> tactic) -> unit
241        val add_inductive_source_theorem_generator : string -> string -> (term -> thm) -> (hol_type -> tactic) -> unit
242        val add_tactic_coding_theorem_generator : string -> (hol_type -> bool) -> (hol_type -> tactic) -> hol_type -> unit
243        val add_tactic_source_theorem_generator : string -> (hol_type -> bool) -> (hol_type -> tactic) -> unit
244        val add_rule_coding_theorem_generator : string -> (hol_type -> bool) -> (hol_type -> thm) -> hol_type -> unit
245        val add_rule_source_theorem_generator : string -> (hol_type -> bool) -> (hol_type -> thm) -> unit
246
247end
248