1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
|
(******************************************************************************)
(* FILE : shells.ml *)
(* DESCRIPTION : Vague approximation in ML to Boyer-Moore "shell" principle *)
(* *)
(* READS FILES : <none> *)
(* WRITES FILES : <none> *)
(* *)
(* AUTHOR : R.J.Boulton *)
(* DATE : 8th May 1991 *)
(* *)
(* LAST MODIFIED : R.J.Boulton *)
(* DATE : 12th October 1992 *)
(* *)
(* LAST MODIFIED : P. Papapanagiotou (University of Edinburgh) *)
(* DATE : July 2009 *)
(******************************************************************************)
(*----------------------------------------------------------------------------*)
(* ML datatype for holding information about a recursive logical type. *)
(*----------------------------------------------------------------------------*)
type constructor_info =
string * (* Constructor name *)
hol_type list * (* Argument types *)
(string * thm) list;; (* Accessor functions *)
type shell_info =
{arg_types : hol_type list; (* Argument types for type constructor *)
constructors :
constructor_info list; (* Constructors for the type *)
axiom : thm; (* Type axiom *)
induct : thm; (* Induction theorem *)
cases : thm; (* Cases theorem *)
distinct : thm list; (* Constructors distinct *)
one_one : thm list; (* Constructors one-one *)
struct_conv : conv -> conv};;
type shell = Shell of string * shell_info;;
(*----------------------------------------------------------------------------*)
(* Reference variable holding the currently defined system shells. *)
(*----------------------------------------------------------------------------*)
let system_shells = ref ([]:shell list);;
(*----------------------------------------------------------------------------*)
(* Function to find the details of a named shell from a list of shells. *)
(*----------------------------------------------------------------------------*)
let rec shell_info (shl:shell list) name =
if (shl = [])
then failwith "shell_info"
else match (hd shl) with Shell (sh_name,info) ->
(if (sh_name = name)
then info
else shell_info (tl shl) name);;
(*----------------------------------------------------------------------------*)
(* Function to find the details of a named shell from the shells currently *)
(* defined in the system. *)
(*----------------------------------------------------------------------------*)
let sys_shell_info name = shell_info !system_shells name;;
(*----------------------------------------------------------------------------*)
(* Functions to extract the components of shell information. *)
(*----------------------------------------------------------------------------*)
let shell_constructors info = info.constructors;;
let shell_accessor_thms info =
((map snd) o flat o (map thd3) o shell_constructors) info;;
let shell_arg_types info = info.arg_types;;
(*
let shell_arg_types info = fst info
and shell_constructors info = (fst o snd) info
and shell_axiom info = (fst o snd o snd) info
and shell_induct info = (fst o snd o snd o snd) info
and shell_cases info = (fst o snd o snd o snd o snd) info
and shell_distinct info = (fst o snd o snd o snd o snd o snd) info
and shell_one_one info = (fst o snd o snd o snd o snd o snd o snd) info
and shell_struct_conv info = (snd o snd o snd o snd o snd o snd o snd) info;;
*)
(*----------------------------------------------------------------------------*)
(* Function to extract details of a named constructor from shell information. *)
(*----------------------------------------------------------------------------*)
let shell_constructor name (info:shell_info) =
let rec shell_constructor' name triples =
if (triples = [])
then failwith "shell_constructor"
else let (con_name,arg_types,accessors) = (hd triples)
in if (con_name = name)
then (arg_types,accessors)
else shell_constructor' name (tl triples)
in shell_constructor' name (info.constructors);;
(*----------------------------------------------------------------------------*)
(* Functions to extract the argument types and the accessor functions for a *)
(* particular constructor. The source is a set of shell information. *)
(*----------------------------------------------------------------------------*)
let shell_constructor_arg_types name info =
fst (shell_constructor name info)
and shell_constructor_accessors name info =
snd (shell_constructor name info);;
(*----------------------------------------------------------------------------*)
(* shells : void -> string list *)
(* *)
(* Function to compute the names of the currently defined system shells. *)
(*----------------------------------------------------------------------------*)
let shells () =
let rec shells' shl =
if (shl = [])
then []
else match (hd shl) with (Shell (name,_)) -> (name::(shells' (tl shl)))
in shells' !system_shells;;
(*----------------------------------------------------------------------------*)
(* all_constructors : void -> string list *)
(* *)
(* Returns a list of all the shell constructors (and bottom values) available *)
(* in the system. *)
(*----------------------------------------------------------------------------*)
let all_constructors () =
flat (map (map fst3 o shell_constructors o sys_shell_info) (shells ()));;
(*----------------------------------------------------------------------------*)
(* all_accessors : void -> string list *)
(* *)
(* Returns a list of all the shell accessors available in the system. *)
(*----------------------------------------------------------------------------*)
let all_accessors () =
flat (map (flat o map (map fst o thd3) o shell_constructors o
sys_shell_info) (shells ()));;
let all_accessor_thms () =
flat (map (shell_accessor_thms o sys_shell_info) (shells ()));;
(*----------------------------------------------------------------------------*)
(* `Shell' for natural numbers. *)
(*----------------------------------------------------------------------------*)
let num_shell =
let axiom = num_Axiom
and induct = num_INDUCTION
and cases = num_CASES
and distinct = [NOT_SUC]
and one_one = [SUC_INJ]
(* and pre = PRE *)
in Shell
("num",
{arg_types = [];
constructors =
[("0",[],[]);("SUC",[`:num`],[("PRE",CONJUNCT2 PRE)])];
axiom = axiom;
induct = induct;
cases = cases;
distinct = distinct;
one_one = one_one;
struct_conv = ONE_STEP_RECTY_EQ_CONV
(induct,distinct,one_one)});;
(*----------------------------------------------------------------------------*)
(* `Shell' for lists. *)
(*----------------------------------------------------------------------------*)
let list_shell =
let axiom = new_axiom `!x f. ?!fn1. (fn1 [] = x) /\ (!h t. fn1 (CONS h t) = f (fn1 t) h t)`
(* |- !x f. ?!fn1. (fn1 [] = x) /\ (!h t. fn1 (CONS h t) = f (fn1 t) h t) *)
and induct = list_INDUCT
and cases = list_CASES
and distinct = [NOT_CONS_NIL]
and one_one = [CONS_11]
in Shell
("list",
{arg_types = [`:'a`];
constructors =
[("NIL",[],[]);
("CONS",
[`:'a`;`:('a)list`],[("HD",HD);("TL",TL)])];
axiom = axiom;
induct = induct;
cases = cases;
distinct = distinct;
one_one = one_one;
struct_conv = ONE_STEP_RECTY_EQ_CONV
(induct,distinct,one_one)});;
(*----------------------------------------------------------------------------*)
(* Set-up the system shell to reflect the basic HOL system. *)
(*----------------------------------------------------------------------------*)
system_shells := [list_shell;num_shell];;
(*----------------------------------------------------------------------------*)
(* define_shell : string -> string -> (string # string list) list -> void *)
(* *)
(* Function for defining a new HOL type together with accessor functions, and *)
(* making a new Boyer-Moore shell from these definitions. If the type already *)
(* exists the function attempts to load the corresponding theorems from the *)
(* current theory hierarchy and use them to make the shell. *)
(* *)
(* The first two arguments correspond to the arguments taken by `define_type' *)
(* and the third argument defines the accessor functions. This is a list of *)
(* constructor names each with names of accessors. The function assumes that *)
(* there are no accessors for a constructor that doesn't appear in the list, *)
(* so it is not necessary to include an entry for a nullary constructor. For *)
(* other constructors there must be one accessor name for each argument and *)
(* they should be given in the correct order. The function ignores any item *)
(* in the list with a constructor name that does not belong to the type. *)
(* *)
(* The constructor and accessor names must all be distinct and must not be *)
(* the names of existing constants. *)
(* *)
(* Example: *)
(* *)
(* define_shell `sexp` `sexp = Nil | Atom * | Cons sexp sexp` *)
(* [(`Atom`,[`Tok`]);(`Cons`,[`Car`;`Cdr`])];; *)
(* *)
(* This results in the following theorems being stored in the current theory *)
(* (or these are the theorems the function would expect to find in the theory *)
(* hierarchy if the type already exists): *)
(* *)
(* sexp (type axiom) *)
(* sexp_Induct (induction theorem) *)
(* sexp_one_one (injectivity of constructors) *)
(* sexp_distinct (distinctness of constructors) *)
(* sexp_cases (cases theorem) *)
(* *)
(* The following definitions for the accessor functions are also stored: *)
(* *)
(* Tok |- !x. Tok(Atom x) = x *)
(* Car |- !s1 s2. Car(Cons s1 s2) = s1 *)
(* Cdr |- !s1 s2. Cdr(Cons s1 s2) = s2 *)
(* *)
(* In certain cases the distinctness or injectivity theorems may not exist, *)
(* when nothing is saved for them. *)
(* *)
(* Finally, a new Boyer-Moore shell is added based on the definitions and *)
(* theorems. *)
(*----------------------------------------------------------------------------*)
(*
let define_shell name syntax accessors =
let find_theory s =
letrec f s l =
if (null l)
then failwith `find_theory`
else if can (theorem (hd l)) s
then hd l
else f s (tl l)
in f s (ancestry ())
in
let mk_def_eq (name,comb,arg) =
let ty = mk_type(`fun`,[type_of comb;type_of arg])
in mk_eq(mk_comb(mk_var(name,ty),comb),arg)
in
let define_accessor axiom (name,tm) =
(name,new_recursive_definition false axiom name tm)
in
let define_accessors axiom (comb,specs) =
map (\(name,arg). define_accessor axiom (name,mk_def_eq (name,comb,arg)))
specs
in
if (mem name (shells ()))
then failwith `define_shell -- shell already exists`
else
let defined = is_type name
in let theory =
if defined
then (find_theory name ?
failwith (`define_shell -- no axiom found for type ` ^ name))
else current_theory ()
in let name_Axiom =
if defined
then theorem theory name
else define_type name syntax
in let name_Induct =
if defined
then theorem theory (name ^ `_Induct`)
else save_thm((name ^ `_Induct`),prove_induction_thm name_Axiom)
and name_one_ones =
if defined
then (CONJUNCTS (theorem theory (name ^ `_one_one`))
?\s if (can prove_constructors_one_one name_Axiom)
then failwith s
else [])
else ((CONJUNCTS o save_thm)
((name ^ `_one_one`),prove_constructors_one_one name_Axiom)
? [])
and name_distincts =
if defined
then (CONJUNCTS (theorem theory (name ^ `_distinct`))
?\s if (can prove_constructors_distinct name_Axiom)
then failwith s
else [])
else ((CONJUNCTS o save_thm)
((name ^ `_distinct`),prove_constructors_distinct name_Axiom)
? [])
in let name_cases =
if defined
then theorem theory (name ^ `_cases`)
else save_thm((name ^ `_cases`),prove_cases_thm name_Induct)
in let ty = (type_of o fst o dest_forall o concl) name_cases
in let ty_args = snd (dest_type ty)
in let cases = (disjuncts o snd o dest_forall o concl) name_cases
in let combs = map (rhs o snd o strip_exists) cases
in let constrs_and_args = map (((fst o dest_const) # I) o strip_comb) combs
in let (constrs,arg_types) =
split (map (I # (map type_of)) constrs_and_args)
in let acc_specs =
map (\(c,args). combine((snd (assoc c accessors) ? []),args)
? failwith
(`define_shell -- ` ^
`incorrect number of accessors for constructor ` ^ c))
constrs_and_args
in let acc_defs =
if defined
then map (map ((\acc. (acc,definition theory acc)) o fst)) acc_specs
else map (define_accessors name_Axiom) (combine (combs,acc_specs))
in let name_shell =
Shell (name,ty_args,combine(constrs,combine(arg_types,acc_defs)),
name_Axiom,name_Induct,name_cases,
name_distincts,name_one_ones,
ONE_STEP_RECTY_EQ_CONV
(name_Induct,name_distincts,name_one_ones))
in do (system_shells := name_shell.system_shells);;
*)
|
