Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Message-Id: <199305071826.AA16576@panther.cs.uidaho.edu>
To: Victor "A." Carreno <vac@air16.larc.nasa.gov>
Cc: info-hol@ted.cs.uidaho.edu
Subject: Re: concrete type definition
In-Reply-To: Your message of Fri, 07 May 93 14:19:36 -0400. <9305071819.AA21553@air52.larc.nasa.gov>
Date: Fri, 07 May 93 11:26:58 -0700
From: Phil Windley <windley@panther.cs.uidaho.edu>


On Fri, 07 May 93 14:19:36 EDT, vac@air16.larc.nasa.gov wrote:
+------------
| I don't know if this is trivial, but I am having a hard time with it:
| 
| #define_type `a_new_type` `the_thing = F_ITEM | S_ITEM | T_ITEM`;;
| 
| According to DESCRIPTION (11.8.1.4) F_ITEM, S_ITEM and T_ITEM have distinct
| values.
| 
| How can you show:
| 
| #g "~(F_ITEM = S_ITEM)";;
| 

Using the axiom that was returned from define_type, use the function
prove_constructors_distinct to prove that the constructors are distinct.
This only does it one way, however (i.e. ~(A = B) but not ~(B = A)), so you
have to break it apart and map GSYM onto iot and combine it with the others
to get a full set.

The easiest way to do all of this is to use my wrapper for the define_type
stuff which lets you say 

create_enum `a_new_type` `F_ITEM | S_ITEM | T_ITEM`;;

and returns a list of theorems, one of which is a complete distinct theorem.


I'll include the code below.  Most of it does more than enumerations, but
the enumeration stuff is there as well.

--phil--

Phillip J. Windley, Asst. Professor   |  windley@cs.uidaho.edu
Laboratory for Applied Logic	      |  windley@panther.cs.uidaho.edu
Department of Computer Science        |
University of Idaho                   |  Phone: 208.885.6501  
Moscow, ID    83843                   |  Fax:   208.885.6645

%----------------------------------------------------------------

   File:         datatypes.ml

   Description:  

   Defines a functions, create_datatype, that uses the abstract 
   type package to create a datatype and prove some useful theorems
   about the datatype.  Datatypes are simply an abstract type with 
   appropriate selector and mutator functions defined.

   Author:       (c) P. J. Windley 1992, 1993

   Modification History:

   09NOV92 [PJW] --- Original file taken from records.ml.

   11NOV92 [PJW] --- Modified to support single arm record declarations.
                     Both multi--arm data structures and single arm
		     records are now supported by the same code.

   08MAR93 [PJW] --- Added create_enum for creating enumerations.

----------------------------------------------------------------%

message `loading datatypes package`;;

begin_section datatypes;;

%----------------------------------------------------------------

 load the patch to concat if the following ml statement prints a 
 number less than 5000 and HOL version <= 2.00.

 lisp `(print call-arguments-limit)`;;


let test_string n = 
    letrec aux s i = 
        (i = 0) => s | aux (`x`^s) (i-1) in
    aux `` n;;

----------------------------------------------------------------%

% message `patching concat`;loadf `concat-patch`;; %

%----------------------------------------------------------------
 define some general list functions
----------------------------------------------------------------%

let int_to_term = (((C (curry mk_const)) ":num") o string_of_int) and
    term_to_int = (int_of_string o fst o dest_const);;

letrec for n lst = 
    (n=0) => []
           | (hd lst).(for (n-1) (tl lst));;


%----------------------------------------------------------------
 define auxilliary functions for new_abstract_representation
----------------------------------------------------------------%

let datatype_type_info = 
       (type_of o snd o dest_comb o 
	fst o dest_eq o snd o strip_forall o hd o conjuncts o snd o 
        strip_forall o snd o dest_abs o snd o dest_comb o 
        snd o strip_forall o concl) ;;

let dest_all_type ty = 
     is_vartype ty => (dest_vartype ty,[]:(type)list) | dest_type ty;;

let string_from_type ty =
    letrec string_aux ty = 
	let s,tl = dest_all_type ty in
	null tl => s |
	let sl = map string_aux tl in
	`(`^(itlist (\x y. x^`,`^y) (butlast sl) (last sl))^`)`^s in
    (string_aux ty)^` `;;


letrec replace (x,y) (lst:(*)list) =
         if (lst = []) then []
         else let (z.zs) = lst in
              if (x = z) then (y.zs)
              else (z.(replace (x,y) zs));;

letrec vector_map fl argl = 
    (null fl) => []
               | (hd fl) (hd argl) . (vector_map (tl fl) (tl argl));;

letrec mult_map fl argl =
    (null fl) => []
               | map (hd fl) argl . (mult_map (tl fl) argl);;

letrec map3 (f:(*#**#***)->****) lst = 
       (null (fst lst)) => [] | 
	   let head = (hd # (hd # hd)) lst and
	       rest = (tl # (tl # tl)) lst in
	   (f head) . (map3 f rest);;

%----------------------------------------------------------------
 function to create a multiarm (variant) record
----------------------------------------------------------------%

let create_datatype name recs =
    let cons_names, lsts = split recs in
    let nls,tls = split(map split lsts) in
    let ty_str_lsts = map (map string_from_type) tls in
    let cons_strs =
	map2  (\nl, sl . nl^` `^(itlist (\x y. x^`  `^y) sl ``)) 
	      (cons_names,ty_str_lsts) in
    let ty_str = 
	name^` = `^(itlist (\x y.x^` | `^y) 
			   (butlast cons_strs) 
			    (last cons_strs)) in
    let ty_axiom = 
        % print_string `.`; %
        define_type name ty_str in
    let cons_terms = 
       map (snd o dest_comb o fst o dest_eq o snd o strip_forall)
           ((conjuncts o snd o dest_abs o snd o dest_comb o snd o 
	     strip_forall o concl) ty_axiom) in
    let make_rec_def cons_term (x, y) =
        % print_string `.`; %
	new_recursive_definition false ty_axiom x 
	"^(mk_var (x,mk_type(`fun`,[type_of cons_term;
                                    type_of y]))) ^cons_term = ^y" in
    let rec_thml = 
	vector_map (map map2 (map make_rec_def cons_terms))
		   (combine(nls,map (snd o strip_comb) cons_terms)) in
    let selectors = 
	save_thm(name^`_selectors`,
		 LIST_CONJ(itlist (curry $@) rec_thml [])) in
    let make_update_def cons_term (x,y) = 
        % print_string `.`; %
        let (cons_term_rator,cons_term_vars) = strip_comb cons_term in
	let new_name = x^`_update` in 
	let new_y = variant cons_term_vars y in
	let new_cons_term = subst [new_y,y] cons_term in
	let update_type = 
	    mk_type(`fun`,[type_of y;
			   mk_type(`fun`,[type_of cons_term;
					  type_of cons_term])]) in
	new_recursive_definition false ty_axiom new_name 
	   "^(mk_var (new_name,update_type))
	    ^new_y
	    ^cons_term = ^new_cons_term" in
    let update_thml = 
	vector_map (map map2 (map make_update_def cons_terms))
		   (combine(nls,map (snd o strip_comb) cons_terms)) in
    let updates = 
	save_thm(name^`_updates`,
		 LIST_CONJ(itlist (curry $@) update_thml [])) in
    let make_pred_def name cons_term =
        let pred_name = `IS_`^name in
        let ((cons_rator,_),_) = ((dest_const # I) o strip_comb) cons_term in
        let boolval = if (cons_rator = name) then "T" else "F" in
        "^(mk_var (pred_name,
                   mk_type(`fun`,[type_of cons_term;":bool"]))) 
         ^cons_term = ^boolval" in
    let pred_terms = 
         map list_mk_conj 
             (mult_map (map make_pred_def cons_names) cons_terms) in
    let pred_thm = 
        map2 (\x,y.new_recursive_definition false ty_axiom (`IS_`^x) y)
             (cons_names, pred_terms) in
   letrec mk_func_vars n = 
       (n = 0) => []
		| (`f` ^ (string_of_int n)) . (mk_func_vars (n-1)) in
   let mk_func_comb (str, tm) = 
       mk_comb(mk_var(str,mk_type(`fun`,[type_of tm;type_of tm])),
	       tm) in
   let mk_func_tms (str,tm) =
       mk_var(str,mk_type(`fun`,[type_of tm;type_of tm])) in
   let func_combs cons_term = 
       let (cons_term_rator,cons_term_vars) = strip_comb cons_term in
       map2 mk_func_comb 
		 (rev(mk_func_vars(length(cons_term_vars))),
		 cons_term_vars) in
   let func_tms cons_term = 
       let (cons_term_rator,cons_term_vars) = strip_comb cons_term in
       map2 mk_func_tms 
	    (rev(mk_func_vars(length(cons_term_vars))),
             cons_term_vars) in
   let new_cons_term cons_term = 
       let (cons_term_rator,cons_term_vars) = strip_comb cons_term in
       subst (combine (func_combs cons_term,cons_term_vars)) cons_term in
   letrec mk_func_comb_type lst end =
	 (null lst) => mk_type(`fun`,[type_of end; type_of end]) |
	 let head.rest = lst in
	 mk_type(`fun`,[mk_type (`fun`,[type_of head;type_of head]);
		       mk_func_comb_type rest end]) in
   let update_lhs (name, cons_term) = 
       let update_rec_name = `Update_`^name in
       let (cons_term_rator,cons_term_vars) = strip_comb cons_term in
       list_mk_comb(mk_var (update_rec_name,
			    mk_func_comb_type cons_term_vars cons_term),
		    ((func_tms cons_term) @ [cons_term])) in
   let update_tm (name, cons_term) = 
       let tm = mk_eq(update_lhs (name, cons_term),
                      new_cons_term cons_term) in
       (`Update_`^name,tm) in
   let update_tms = map2 update_tm (cons_names,cons_terms) in
   let update_rec_thms = 
       map (uncurry (new_recursive_definition false ty_axiom))
           update_tms in
   let update_rec_thm = 
       save_thm(`Update_`^name^`_thm`, LIST_CONJ update_rec_thms) in
   let one_one_thm = 
       % print_string `.`; %
       save_thm(name^`_one_one`,prove_constructors_one_one ty_axiom) in
   let cases_thm = 
       % print_string `.`; %
       save_thm(name^`_cases`,
                     prove_cases_thm(prove_induction_thm ty_axiom)) in
   let distinct_thm = 
       (length recs) > 1 => 
          let thl = CONJUNCTS (prove_constructors_distinct ty_axiom) in
          save_thm(name^`_distinct`, LIST_CONJ(thl @ (map GSYM thl))) |
          BOOL_CASES_AX in
   let rec_type = datatype_type_info ty_axiom in
   let var_name = "x:^rec_type" in
   let selector_terms = 
       map(map (fst o strip_comb o fst o 
            dest_eq o snd o strip_forall o concl)) rec_thml in
   let selector_apps = map(map (\tm . mk_comb(tm,var_name))) selector_terms in
   let mk_pred name cons_term =
        let pred_name = `IS_`^name in
        let ((cons_rator,_),_) = ((dest_const # I) o strip_comb) cons_term in
        (mk_const (pred_name,
                   mk_type(`fun`,[type_of cons_term;":bool"]))) in
   let selector_goal_arm (name,cons_term, selector_app) = 
       let (cons_term_rator,_) = strip_comb cons_term in
       let pred = mk_comb(mk_pred name cons_term,var_name) in
       let eq_tm = mk_eq(var_name, 
			 list_mk_comb(cons_term_rator,selector_app)) in
       (length recs > 1) => mk_imp(pred,eq_tm)
	                  | eq_tm in
   let selector_goals = 
       map3 selector_goal_arm (cons_names,cons_terms,selector_apps) in
   let goal = 
       mk_forall(var_name,
                 itlist (curry mk_disj) 
	                (butlast selector_goals) 
	                (last selector_goals)) in
   let selector_tactic = 
       GEN_TAC
       THEN STRUCT_CASES_TAC 
	       (SPEC var_name cases_thm)
       THEN REWRITE_TAC ([selectors] @ pred_thm) in
   let selectors_work_thm = 
       % print_string `.`; %
       prove_thm(name^`_selectors_work`,
                 goal,
                 selector_tactic) in
    let mk_update_commutes_tm (name,cons_term) (x, y, z) = 
        let update_rec_name = `Update_`^name in
        let (_,cons_term_vars) = strip_comb cons_term in
 	let selector_tm =  
            (mk_const (x,mk_type(`fun`,[type_of cons_term; y]))) in
	let update_x = 
	    list_mk_comb(mk_const (update_rec_name,
				 mk_func_comb_type cons_term_vars cons_term),
			    ((func_tms cons_term) @ ["x:^rec_type"])) in
        let pred = mk_comb(mk_pred name cons_term,"x:^rec_type") in
        let eq_tm = "(^selector_tm ^update_x = ^z (^selector_tm x))" in
	let commute_tm = (length recs > 1) => mk_imp(pred,eq_tm) 
	                                    | eq_tm in
	list_mk_forall(frees commute_tm,commute_tm) in
    let commute_goals = 
	let goal_list_list =
            map2 (uncurry map3)
	     ((map2 mk_update_commutes_tm (cons_names, cons_terms)),
	      (combine(nls,combine(tls, (map func_tms cons_terms))))) in
        itlist (curry $@) goal_list_list [] in
    let commute_TAC =
        REPEAT GEN_TAC
        THEN STRUCT_CASES_TAC (SPEC "x:^rec_type" cases_thm)
	THEN REWRITE_TAC ([update_rec_thm;selectors] @ pred_thm) in
    let commute_thms = 
        save_thm(name^`_Update_commute_thms`,
                 LIST_CONJ(map (\goal . PROVE(goal,commute_TAC)) 
                               commute_goals)) in
   (length recs) > 1 => 
      ([ty_axiom;selectors;updates;one_one_thm;cases_thm;
	selectors_work_thm; update_rec_thm; commute_thms] @ 
       pred_thm @ [distinct_thm]) |
      ([ty_axiom;selectors;updates;one_one_thm;cases_thm;
	selectors_work_thm; update_rec_thm; commute_thms] @ pred_thm);;


let create_record name lst = 
    create_datatype name [name,lst];;

let create_enum name recs =
    let ty_str = 
	name^` = `^recs in
    let ty_axiom = 
        define_type name ty_str in
    let induct_thm = 
        save_thm(name^`_induct`,
                 prove_induction_thm ty_axiom) in
   let cases_thm = 
       save_thm(name^`_cases`,
                prove_cases_thm induct_thm) in
   let thl = CONJUNCTS (prove_constructors_distinct ty_axiom) in
   let distinct_thm = 
       save_thm(name^`_distinct`,LIST_CONJ(thl @ (map GSYM thl))) in
   ([ty_axiom;induct_thm;cases_thm;distinct_thm]);;


%----------------------------------------------------------------
create_enum `error` `ALREADY_EXISTS | NOT_FOUND | SUCCESS`;;
----------------------------------------------------------------%

%----------------------------------------------------------------
 Bind exportable functions to it
----------------------------------------------------------------%
(create_datatype,create_record,create_enum);;

end_section datatypes;;

%----------------------------------------------------------------
 Recover exportable functions from it.
----------------------------------------------------------------%
let (create_datatype, create_record, create_enum) = it;;