(******************************************************************************) (* FILE : shells.ml *) (* DESCRIPTION : Vague approximation in ML to Boyer-Moore "shell" principle *) (* *) (* READS FILES : *) (* WRITES FILES : *) (* *) (* 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);; *)