(******************************************************************************)
(* 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 :   ( 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     *)
  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                          
  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 ; ; 

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 =
axiom = new_axiom ` !    ! fn1 . ( fn1 [ ] = x ) /\ ( !   fn1 ( CONS h t ) = f ( fn1 t ) h t ) ` 
 ( * |- !    ! fn1 . ( fn1 [ ] = x ) /\ ( !   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                      
        ! 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  ( 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 ,  ( 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 ? 
                  ( ` 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 ` ) ) 
                 ?  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 ` ) ) 
                 ?  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  = 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 (  , arg_types ) = 
           split ( map ( I # ( map type_of ) ) constrs_and_args ) 
    in   let acc_specs = 
           map ( \(c , args ) .  ( assoc c accessors ) ? [ ] ) , args ) 
                   ?  
                        ( ` 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 ,  , 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 :    ; ; 

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);;
*)

****************************************************************************
 FILE          : shells.ml                                                  
                                                                            
 READS FILES   : <none>                                                     
 WRITES FILES  : <none>                                                     
                                                                            
                                                                            
                                                                            
****************************************************************************
----------------------------------------------------------------------------
 ML datatype for holding information about a recursive logical type.        
----------------------------------------------------------------------------
 Constructor name   
 Argument types     
 Argument types for type constructor 
 Constructors for the type           
 Cases theorem                       
 Constructors distinct               
 Constructors one-one                
----------------------------------------------------------------------------
 Reference variable holding the currently defined system shells.            
----------------------------------------------------------------------------
----------------------------------------------------------------------------
 Function to find the details of a named shell from a list of shells.       
----------------------------------------------------------------------------
----------------------------------------------------------------------------
 Function to find the details of a named shell from the shells currently    
 defined in the system.                                                     
----------------------------------------------------------------------------
----------------------------------------------------------------------------
 Functions to extract the components of shell information.                  
----------------------------------------------------------------------------
----------------------------------------------------------------------------
 Function to extract details of a named constructor from shell information. 
----------------------------------------------------------------------------
----------------------------------------------------------------------------
 Functions to extract the argument types and the accessor functions for a   
 particular constructor. The source is a set of shell information.          
----------------------------------------------------------------------------
----------------------------------------------------------------------------
 shells : void -> string list                                               
                                                                            
 Function to compute the names of the currently defined system shells.      
----------------------------------------------------------------------------
----------------------------------------------------------------------------
 all_constructors : void -> string list                                     
                                                                            
 Returns a list of all the shell constructors (and bottom values) available 
 in the system.                                                             
----------------------------------------------------------------------------
----------------------------------------------------------------------------
 all_accessors : void -> string list                                        
                                                                            
 Returns a list of all the shell accessors available in the system.         
----------------------------------------------------------------------------
----------------------------------------------------------------------------
----------------------------------------------------------------------------
axiom = num_Axiom
         and
         and pre = PRE 
axiom = axiom;
----------------------------------------------------------------------------
----------------------------------------------------------------------------
 |- !x f. ?!fn1. (fn1 [] = x) /\ (!h t. fn1 (CONS h t) = f (fn1 t) h t) 
 axiom = axiom; 
----------------------------------------------------------------------------
----------------------------------------------------------------------------
----------------------------------------------------------------------------
 define_shell : string -> string -> (string # string list) list -> void     
                                                                            
 exists the function attempts to load the corresponding theorems from the   
 current theory hierarchy and use them to make the shell.                   
                                                                            
 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  
 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:      
                                                                            
                                                                            
 In certain cases the distinctness or injectivity theorems may not exist,   
 when nothing is saved for them.                                            
                                                                            
 theorems.                                                                  
----------------------------------------------------------------------------
  DESCRIPTION    : Vague approximation in ML to Boyer - Moore " shell " principle
  AUTHOR         : R.J.Boulton                                                
  DATE           : 8th May 1991                                               
  LAST MODIFIED : R.J.Boulton                                                
  DATE           : 12th October 1992                                          
  LAST MODIFIED :   ( University of Edinburgh )                
  DATE           : July 2009                                                  


type constructor_info =
  Accessor functions


type shell_info =
    constructors :
  axiom : thm ;                    ( * Type axiom                          
  Induction theorem                   
    struct_conv : conv -> conv};;

type shell = Shell of string * shell_info;;


let system_shells = ref ([]:shell list);;


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);;


let sys_shell_info name = shell_info !system_shells name;;

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 ; ; 

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;;
*)


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);;


let shell_constructor_arg_types name info =
   fst (shell_constructor name info)
and shell_constructor_accessors name info =
   snd (shell_constructor name info);;


let shells () =
   let rec shells' shl =
      if (shl = [])
      then []
      else match (hd shl) with (Shell (name,_)) -> (name::(shells' (tl shl)))
   in shells' !system_shells;;


let all_constructors () =
 flat (map (map fst3 o shell_constructors o sys_shell_info) (shells ()));;


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 =
         and cases = num_CASES
         and distinct = [NOT_SUC]
         and one_one = [SUC_INJ]
     in  Shell
            ("num",
             {arg_types = [];
              constructors =
                 [("0",[],[]);("SUC",[`:num`],[("PRE",CONJUNCT2 PRE)])];
              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 =
axiom = new_axiom ` !    ! fn1 . ( fn1 [ ] = x ) /\ ( !   fn1 ( CONS h t ) = f ( fn1 t ) h t ) ` 
 ( * |- !    ! fn1 . ( fn1 [ ] = x ) /\ ( !   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)])];
            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];;

  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
  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   
  other constructors there must be one accessor name for each argument and   
     Tok                 |- ! x. Tok(Atom x ) = x                               
     Car                 |- ! s1 s2 . Car(Cons s1 s2 ) = s1                      
        ! s1 s2 .    ) = s2                      
  Finally , a new Boyer - Moore shell is added based on the definitions and     

 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  ( 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 ,  ( 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 ? 
                  ( ` 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 ` ) ) 
                 ?  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 ` ) ) 
                 ?  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  = 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 (  , arg_types ) = 
           split ( map ( I # ( map type_of ) ) constrs_and_args ) 
    in   let acc_specs = 
           map ( \(c , args ) .  ( assoc c accessors ) ? [ ] ) , args ) 
                   ?  
                        ( ` 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 ,  , 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 :    ; ; 

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);;
*)
