src/HOL/datatype.ML
author clasohm
Fri Apr 19 11:33:24 1996 +0200 (1996-04-19)
changeset 1668 8ead1fe65aad
parent 1574 5a63ab90ee8a
child 1690 e0ff33a33fa5
permissions -rw-r--r--
added Konrad's code for the datatype package
     1 (* Title:       HOL/datatype.ML
     2    ID:          $Id$
     3    Author:      Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker,
     4                 Konrad Slind
     5    Copyright 1995 TU Muenchen
     6 *)
     7 
     8 
     9 (*used for constructor parameters*)
    10 datatype dt_type = dtVar of string |
    11   dtTyp of dt_type list * string |
    12   dtRek of dt_type list * string;
    13 
    14 structure Datatype =
    15 struct
    16 local 
    17 
    18 val mysort = sort;
    19 open ThyParse HOLogic;
    20 exception Impossible;
    21 exception RecError of string;
    22 
    23 val is_dtRek = (fn dtRek _ => true  |  _  => false);
    24 fun opt_parens s = if s = "" then "" else enclose "(" ")" s; 
    25 
    26 (* ----------------------------------------------------------------------- *)
    27 (* Derivation of the primrec combinator application from the equations     *)
    28 
    29 (* substitute fname(ls,xk,rs) by yk(ls,rs) in t for (xk,yk) in pairs  *) 
    30 
    31 fun subst_apps (_,_) [] t = t
    32   | subst_apps (fname,rpos) pairs t =
    33     let 
    34     fun subst (Abs(a,T,t)) = Abs(a,T,subst t)
    35       | subst (funct $ body) = 
    36         let val (f,b) = strip_comb (funct$body)
    37         in 
    38           if is_Const f andalso fst(dest_Const f) = fname 
    39             then 
    40               let val (ls,rest) = (take(rpos,b), drop(rpos,b));
    41                 val (xk,rs) = (hd rest,tl rest)
    42                   handle LIST _ => raise RecError "not enough arguments \
    43                    \ in recursive application on rhs"
    44               in 
    45                 (case assoc (pairs,xk) of 
    46                    None   => list_comb(f, map subst b)
    47                  | Some U => list_comb(U, map subst (ls @ rs)))
    48               end
    49           else list_comb(f, map subst b)
    50         end
    51       | subst(t) = t
    52     in subst t end;
    53   
    54 (* abstract rhs *)
    55 
    56 fun abst_rec (fname,rpos,tc,ls,cargs,rs,rhs) =       
    57   let val rargs = (map fst o 
    58                    (filter (fn (a,T) => is_dtRek T))) (cargs ~~ tc);
    59       val subs = map (fn (s,T) => (s,dummyT))
    60                    (rev(rename_wrt_term rhs rargs));
    61       val subst_rhs = subst_apps (fname,rpos)
    62                         (map Free rargs ~~ map Free subs) rhs;
    63   in 
    64       list_abs_free (cargs @ subs @ ls @ rs, subst_rhs) 
    65   end;
    66 
    67 (* parsing the prim rec equations *)
    68 
    69 fun dest_eq ( Const("Trueprop",_) $ (Const ("op =",_) $ lhs $ rhs))
    70                  = (lhs, rhs)
    71    | dest_eq _ = raise RecError "not a proper equation"; 
    72 
    73 fun dest_rec eq = 
    74   let val (lhs,rhs) = dest_eq eq; 
    75     val (name,args) = strip_comb lhs; 
    76     val (ls',rest)  = take_prefix is_Free args; 
    77     val (middle,rs') = take_suffix is_Free rest;
    78     val rpos = length ls';
    79     val (c,cargs') = strip_comb (hd middle)
    80       handle LIST "hd" => raise RecError "constructor missing";
    81     val (ls,cargs,rs) = (map dest_Free ls', map dest_Free cargs'
    82                          , map dest_Free rs')
    83       handle TERM ("dest_Free",_) => 
    84           raise RecError "constructor has illegal argument in pattern";
    85   in 
    86     if length middle > 1 then 
    87       raise RecError "more than one non-variable in pattern"
    88     else if not(null(findrep (map fst (ls @ rs @ cargs)))) then 
    89       raise RecError "repeated variable name in pattern" 
    90          else (fst(dest_Const name) handle TERM _ => 
    91                raise RecError "function is not declared as constant in theory"
    92                  ,rpos,ls,fst( dest_Const c),cargs,rs,rhs)
    93   end; 
    94 
    95 (* check function specified for all constructors and sort function terms *)
    96 
    97 fun check_and_sort (n,its) = 
    98   if length its = n 
    99     then map snd (mysort (fn ((i : int,_),(j,_)) => i<j) its)
   100   else raise error "Primrec definition error:\n\
   101    \Please give an equation for every constructor";
   102 
   103 (* translate rec equations into function arguments suitable for rec comb *)
   104 (* theory parameter needed for printing error messages                   *) 
   105 
   106 fun trans_recs _ _ [] = error("No primrec equations.")
   107   | trans_recs thy cs' (eq1::eqs) = 
   108     let val (name1,rpos1,ls1,_,_,_,_) = dest_rec eq1
   109       handle RecError s =>
   110         error("Primrec definition error: " ^ s ^ ":\n" 
   111               ^ "   " ^ Sign.string_of_term (sign_of thy) eq1);
   112       val tcs = map (fn (_,c,T,_,_) => (c,T)) cs';  
   113       val cs = map fst tcs;
   114       fun trans_recs' _ [] = []
   115         | trans_recs' cis (eq::eqs) = 
   116           let val (name,rpos,ls,c,cargs,rs,rhs) = dest_rec eq; 
   117             val tc = assoc(tcs,c);
   118             val i = (1 + find (c,cs))  handle LIST "find" => 0; 
   119           in
   120           if name <> name1 then 
   121             raise RecError "function names inconsistent"
   122           else if rpos <> rpos1 then 
   123             raise RecError "position of rec. argument inconsistent"
   124           else if i = 0 then 
   125             raise RecError "illegal argument in pattern" 
   126           else if i mem cis then
   127             raise RecError "constructor already occured as pattern "
   128                else (i,abst_rec (name,rpos,the tc,ls,cargs,rs,rhs))
   129                      :: trans_recs' (i::cis) eqs 
   130           end
   131           handle RecError s =>
   132                 error("Primrec definition error\n" ^ s ^ "\n" 
   133                       ^ "   " ^ Sign.string_of_term (sign_of thy) eq);
   134     in (  name1, ls1
   135         , check_and_sort (length cs, trans_recs' [] (eq1::eqs)))
   136     end ;
   137 
   138 in
   139   fun add_datatype (typevars, tname, cons_list') thy = 
   140     let
   141       fun typid(dtRek(_,id)) = id
   142         | typid(dtVar s) = implode (tl (explode s))
   143         | typid(dtTyp(_,id)) = id;
   144 
   145       fun index_vnames(vn::vns,tab) =
   146             (case assoc(tab,vn) of
   147                None => if vn mem vns
   148                        then (vn^"1") :: index_vnames(vns,(vn,2)::tab)
   149                        else vn :: index_vnames(vns,tab)
   150              | Some(i) => (vn^(string_of_int i)) ::
   151                           index_vnames(vns,(vn,i+1)::tab))
   152         | index_vnames([],tab) = [];
   153 
   154       fun mk_var_names types = index_vnames(map typid types,[]);
   155 
   156       (*search for free type variables and convert recursive *)
   157       fun analyse_types (cons, types, syn) =
   158         let fun analyse(t as dtVar v) =
   159                   if t mem typevars then t
   160                   else error ("Free type variable " ^ v ^ " on rhs.")
   161               | analyse(dtTyp(typl,s)) =
   162                   if tname <> s then dtTyp(analyses typl, s)
   163                   else if typevars = typl then dtRek(typl, s)
   164                        else error (s ^ " used in different ways")
   165               | analyse(dtRek _) = raise Impossible
   166             and analyses ts = map analyse ts;
   167         in (cons, Syntax.const_name cons syn, analyses types,
   168             mk_var_names types, syn)
   169         end;
   170 
   171      (*test if all elements are recursive, i.e. if the type is empty*)
   172       
   173       fun non_empty (cs : ('a * 'b * dt_type list * 'c *'d) list) = 
   174         not(forall (exists is_dtRek o #3) cs) orelse
   175         error("Empty datatype not allowed!");
   176 
   177       val cons_list = map analyse_types cons_list';
   178       val dummy = non_empty cons_list;
   179       val num_of_cons = length cons_list;
   180 
   181      (* Auxiliary functions to construct argument and equation lists *)
   182 
   183      (*generate 'var_n, ..., var_m'*)
   184       fun Args(var, delim, n, m) = 
   185         space_implode delim (map (fn n => var^string_of_int(n)) (n upto m));
   186 
   187       fun C_exp name vns = name ^ opt_parens(space_implode ") (" vns);
   188 
   189      (*Arg_eqs([x1,...,xn],[y1,...,yn]) = "x1 = y1 & ... & xn = yn" *)
   190       fun arg_eqs vns vns' =
   191         let fun mkeq(x,x') = x ^ "=" ^ x'
   192         in space_implode " & " (map mkeq (vns~~vns')) end;
   193 
   194      (*Pretty printers for type lists;
   195        pp_typlist1: parentheses, pp_typlist2: brackets*)
   196       fun pp_typ (dtVar s) = "(" ^ s ^ "::term)"
   197         | pp_typ (dtTyp (typvars, id)) =
   198           if null typvars then id else (pp_typlist1 typvars) ^ id
   199         | pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id
   200       and
   201         pp_typlist' ts = commas (map pp_typ ts)
   202       and
   203         pp_typlist1 ts = if null ts then "" else parens (pp_typlist' ts);
   204 
   205       fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts);
   206 
   207      (* Generate syntax translation for case rules *)
   208       fun calc_xrules c_nr y_nr ((_, name, _, vns, _) :: cs) = 
   209         let val arity = length vns;
   210           val body  = "z" ^ string_of_int(c_nr);
   211           val args1 = if arity=0 then ""
   212                       else " " ^ Args ("y", " ", y_nr, y_nr+arity-1);
   213           val args2 = if arity=0 then ""
   214                       else "(% " ^ Args ("y", " ", y_nr, y_nr+arity-1) 
   215                         ^ ". ";
   216           val (rest1,rest2) = 
   217             if null cs then ("","")
   218             else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs
   219             in (" | " ^ h1, " " ^ h2) end;
   220         in (name ^ args1 ^ " => " ^ body ^ rest1,
   221             args2 ^ body ^ (if args2 = "" then "" else ")") ^ rest2)
   222         end
   223         | calc_xrules _ _ [] = raise Impossible;
   224       
   225       val xrules =
   226         let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
   227         in [("logic", "case x of " ^ first_part) <->
   228              ("logic", tname ^ "_case " ^ scnd_part ^ " x")]
   229         end;
   230 
   231      (*type declarations for constructors*)
   232       fun const_type (id, _, typlist, _, syn) =
   233         (id,  
   234          (if null typlist then "" else pp_typlist2 typlist ^ " => ") ^
   235             pp_typlist1 typevars ^ tname, syn);
   236 
   237 
   238       fun assumpt (dtRek _ :: ts, v :: vs ,found) =
   239         let val h = if found then ";P(" ^ v ^ ")" else "[| P(" ^ v ^ ")"
   240         in h ^ (assumpt (ts, vs, true)) end
   241         | assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found)
   242       | assumpt ([], [], found) = if found then "|] ==>" else ""
   243         | assumpt _ = raise Impossible;
   244 
   245       fun t_inducting ((_, name, types, vns, _) :: cs) =
   246         let
   247           val h = if null types then " P(" ^ name ^ ")"
   248                   else " !!" ^ (space_implode " " vns) ^ "." ^
   249                     (assumpt (types, vns, false)) ^
   250                     "P(" ^ C_exp name vns ^ ")";
   251           val rest = t_inducting cs;
   252         in if rest = "" then h else h ^ "; " ^ rest end
   253         | t_inducting [] = "";
   254 
   255       fun t_induct cl typ_name =
   256         "[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")";
   257 
   258       fun gen_typlist typevar f ((_, _, ts, _, _) :: cs) =
   259         let val h = if (length ts) > 0
   260                       then pp_typlist2(f ts) ^ "=>"
   261                     else ""
   262         in h ^ typevar ^  "," ^ (gen_typlist typevar f cs) end
   263         | gen_typlist _ _ [] = "";
   264 
   265 
   266 (* -------------------------------------------------------------------- *)
   267 (* The case constant and rules                                          *)
   268                 
   269       val t_case = tname ^ "_case";
   270 
   271       fun case_rule n (id, name, _, vns, _) =
   272         let val args = if vns = [] then "" else " " ^ space_implode " " vns
   273         in (t_case ^ "_" ^ id,
   274             t_case ^ " " ^ Args("f", " ", 1, num_of_cons)
   275             ^ " (" ^ name ^ args ^ ") = f"^string_of_int(n) ^ args)
   276         end
   277 
   278       fun case_rules n (c :: cs) = case_rule n c :: case_rules(n+1) cs
   279         | case_rules _ [] = [];
   280 
   281       val datatype_arity = length typevars;
   282 
   283       val types = [(tname, datatype_arity, NoSyn)];
   284 
   285       val arities = 
   286         let val term_list = replicate datatype_arity termS;
   287         in [(tname, term_list, termS)] 
   288         end;
   289 
   290       val datatype_name = pp_typlist1 typevars ^ tname;
   291 
   292       val new_tvar_name = variant (map (fn dtVar s => s) typevars) "'z";
   293 
   294       val case_const =
   295         (t_case,
   296          "[" ^ gen_typlist new_tvar_name I cons_list 
   297          ^  pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name^"::term",
   298          NoSyn);
   299 
   300       val rules_case = case_rules 1 cons_list;
   301 
   302 (* -------------------------------------------------------------------- *)
   303 (* The prim-rec combinator                                              *) 
   304 
   305       val t_rec = tname ^ "_rec"
   306 
   307 (* adding type variables for dtRek types to end of list of dt_types      *)   
   308 
   309       fun add_reks ts = 
   310         ts @ map (fn _ => dtVar new_tvar_name) (filter is_dtRek ts); 
   311 
   312 (* positions of the dtRek types in a list of dt_types, starting from 1  *)
   313       fun rek_vars ts vns = map snd (filter (is_dtRek o fst) (ts ~~ vns))
   314 
   315       fun rec_rule n (id,name,ts,vns,_) = 
   316         let val args = opt_parens(space_implode ") (" vns)
   317           val fargs = opt_parens(Args("f", ") (", 1, num_of_cons))
   318           fun rarg vn = t_rec ^ fargs ^ " (" ^ vn ^ ")"
   319           val rargs = opt_parens(space_implode ") ("
   320                                  (map rarg (rek_vars ts vns)))
   321         in
   322           (t_rec ^ "_" ^ id,
   323            t_rec ^ fargs ^ " (" ^ name ^ args ^ ") = f"
   324            ^ string_of_int(n) ^ args ^ rargs)
   325         end
   326 
   327       fun rec_rules n (c::cs) = rec_rule n c :: rec_rules (n+1) cs 
   328         | rec_rules _ [] = [];
   329 
   330       val rec_const =
   331         (t_rec,
   332          "[" ^ (gen_typlist new_tvar_name add_reks cons_list) 
   333          ^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name^"::term",
   334          NoSyn);
   335 
   336       val rules_rec = rec_rules 1 cons_list
   337 
   338 (* -------------------------------------------------------------------- *)
   339       val consts = 
   340         map const_type cons_list
   341         @ (if num_of_cons < dtK then []
   342            else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)])
   343         @ [case_const,rec_const];
   344 
   345 
   346       fun Ci_ing ((id, name, _, vns, _) :: cs) =
   347            if null vns then Ci_ing cs
   348            else let val vns' = variantlist(vns,vns)
   349                 in ("inject_" ^ id,
   350                     "(" ^ (C_exp name vns) ^ "=" ^ (C_exp name vns')
   351                     ^ ") = (" ^ (arg_eqs vns vns') ^ ")") :: (Ci_ing cs)
   352                 end
   353         | Ci_ing [] = [];
   354 
   355       fun Ci_negOne (id1,name1,_,vns1,_) (id2,name2,_,vns2,_) =
   356             let val vns2' = variantlist(vns2,vns1)
   357                 val ax = C_exp name1 vns1 ^ "~=" ^ C_exp name2 vns2'
   358         in (id1 ^ "_not_" ^ id2, ax) end;
   359 
   360       fun Ci_neg1 [] = []
   361         | Ci_neg1 (c1::cs) = (map (Ci_negOne c1) cs) @ Ci_neg1 cs;
   362 
   363       fun suc_expr n = 
   364         if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")";
   365 
   366       fun Ci_neg2() =
   367         let val ord_t = tname ^ "_ord";
   368           val cis = cons_list ~~ (0 upto (num_of_cons - 1))
   369           fun Ci_neg2equals ((id, name, _, vns, _), n) =
   370             let val ax = ord_t ^ "(" ^ (C_exp name vns) ^ ") = " ^ (suc_expr n)
   371             in (ord_t ^ "_" ^ id, ax) end
   372         in (ord_t ^ "_distinct", ord_t^"(x) ~= "^ord_t^"(y) ==> x ~= y") ::
   373           (map Ci_neg2equals cis)
   374         end;
   375 
   376       val rules_distinct = if num_of_cons < dtK then Ci_neg1 cons_list
   377                            else Ci_neg2();
   378 
   379       val rules_inject = Ci_ing cons_list;
   380 
   381       val rule_induct = (tname ^ "_induct", t_induct cons_list tname);
   382 
   383       val rules = rule_induct ::
   384         (rules_inject @ rules_distinct @ rules_case @ rules_rec);
   385 
   386       fun add_primrec eqns thy =
   387         let val rec_comb = Const(t_rec,dummyT)
   388           val teqns = map (fn neq => snd(read_axm (sign_of thy) neq)) eqns
   389           val (fname,ls,fns) = trans_recs thy cons_list teqns
   390           val rhs = 
   391             list_abs_free
   392             (ls @ [(tname,dummyT)]
   393              ,list_comb(rec_comb
   394                         , fns @ map Bound (0 ::(length ls downto 1))));
   395           val sg = sign_of thy;
   396           val defpair = (fname ^ "_" ^ tname ^ "_def",
   397                          Logic.mk_equals (Const(fname,dummyT), rhs))
   398           val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair;
   399           val varT = Type.varifyT T;
   400           val ftyp = the (Sign.const_type sg fname);
   401         in add_defs_i [defpairT] thy end;
   402 
   403     in
   404       (thy |> add_types types
   405            |> add_arities arities
   406            |> add_consts consts
   407            |> add_trrules xrules
   408            |> add_axioms rules, add_primrec)
   409     end
   410 end
   411 end
   412 
   413 (*
   414 Informal description of functions used in datatype.ML for the Isabelle/HOL
   415 implementation of prim. rec. function definitions. (N. Voelker, Feb. 1995) 
   416 
   417 * subst_apps (fname,rpos) pairs t:
   418    substitute the term 
   419        fname(ls,xk,rs) 
   420    by 
   421       yk(ls,rs) 
   422    in t for (xk,yk) in pairs, where rpos = length ls. 
   423    Applied with : 
   424      fname = function name 
   425      rpos = position of recursive argument 
   426      pairs = list of pairs (xk,yk), where 
   427           xk are the rec. arguments of the constructor in the pattern,
   428           yk is a variable with name derived from xk 
   429      t = rhs of equation 
   430 
   431 * abst_rec (fname,rpos,tc,ls,cargs,rs,rhs)
   432   - filter recursive arguments from constructor arguments cargs,
   433   - perform substitutions on rhs, 
   434   - derive list subs of new variable names yk for use in subst_apps, 
   435   - abstract rhs with respect to cargs, subs, ls and rs. 
   436 
   437 * dest_eq t 
   438   destruct a term denoting an equation into lhs and rhs. 
   439 
   440 * dest_req eq 
   441   destruct an equation of the form 
   442       name (vl1..vlrpos, Ci(vi1..vin), vr1..vrn) = rhs
   443   into 
   444   - function name  (name) 
   445   - position of the first non-variable parameter  (rpos)
   446   - the list of first rpos parameters (ls = [vl1..vlrpos]) 
   447   - the constructor (fst( dest_Const c) = Ci)
   448   - the arguments of the constructor (cargs = [vi1..vin])
   449   - the rest of the variables in the pattern (rs = [vr1..vrn])
   450   - the right hand side of the equation (rhs).  
   451  
   452 * check_and_sort (n,its)
   453   check that  n = length its holds, and sort elements of its by 
   454   first component. 
   455 
   456 * trans_recs thy cs' (eq1::eqs)
   457   destruct eq1 into name1, rpos1, ls1, etc.. 
   458   get constructor list with and without type (tcs resp. cs) from cs',  
   459   for every equation:  
   460     destruct it into (name,rpos,ls,c,cargs,rs,rhs)
   461     get typed constructor tc from c and tcs 
   462     determine the index i of the constructor 
   463     check function name and position of rec. argument by comparison
   464     with first equation 
   465     check for repeated variable names in pattern
   466     derive function term f_i which is used as argument of the rec. combinator
   467     sort the terms f_i according to i and return them together
   468       with the function name and the parameter of the definition (ls). 
   469 
   470 * Application:
   471 
   472   The rec. combinator is applied to the function terms resulting from
   473   trans_rec. This results in a function which takes the recursive arg. 
   474   as first parameter and then the arguments corresponding to ls. The
   475   order of parameters is corrected by setting the rhs equal to 
   476 
   477   list_abs_free
   478             (ls @ [(tname,dummyT)]
   479              ,list_comb(rec_comb
   480                         , fns @ map Bound (0 ::(length ls downto 1))));
   481 
   482   Note the de-Bruijn indices counting the number of lambdas between the
   483   variable and its binding. 
   484 *)
   485 
   486 
   487 
   488 (* ----------------------------------------------- *)
   489 (* The following has been written by Konrad Slind. *)
   490 
   491 
   492 type dtype_info = {case_const:term, case_rewrites:thm list,
   493                    constructors:term list, nchotomy:thm, case_cong:thm};
   494 
   495 signature Dtype_sig =
   496 sig
   497   val build_case_cong: Sign.sg -> thm list -> cterm
   498   val build_nchotomy: Sign.sg -> thm list -> cterm
   499 
   500   val prove_case_cong: thm -> thm list -> cterm -> thm
   501   val prove_nchotomy: (string -> int -> tactic) -> thm list -> cterm -> thm
   502 
   503   val case_thms : Sign.sg -> thm list -> (string -> int -> tactic)
   504                    -> {nchotomy:thm, case_cong:thm}
   505 
   506   val build_record : (theory * (string * string list)
   507                       * (string -> int -> tactic))
   508                      -> (string * dtype_info) 
   509 
   510 end;
   511 
   512 
   513 (*---------------------------------------------------------------------------
   514  * This structure is support for the Isabelle datatype package. It provides
   515  * entrypoints for 1) building and proving the case congruence theorem for
   516  * a datatype and 2) building and proving the "exhaustion" theorem for
   517  * a datatype (I have called this theorem "nchotomy" for no good reason).
   518  *
   519  * It also brings all these together in the function "build_record", which
   520  * is probably what will be used.
   521  *
   522  * Since these routines are required in order to support TFL, they have
   523  * been written so they will compile "stand-alone", i.e., in Isabelle-HOL
   524  * without any TFL code around.
   525  *---------------------------------------------------------------------------*)
   526 structure Dtype : Dtype_sig =
   527 struct
   528 
   529 exception DTYPE_ERR of {func:string, mesg:string};
   530 
   531 (*---------------------------------------------------------------------------
   532  * General support routines
   533  *---------------------------------------------------------------------------*)
   534 fun itlist f L base_value =
   535    let fun it [] = base_value
   536          | it (a::rst) = f a (it rst)
   537    in it L 
   538    end;
   539 
   540 fun end_itlist f =
   541 let fun endit [] = raise DTYPE_ERR{func="end_itlist", mesg="list too short"}
   542       | endit alist = 
   543          let val (base::ralist) = rev alist
   544          in itlist f (rev ralist) base  end
   545 in endit
   546 end;
   547 
   548 fun unzip L = itlist (fn (x,y) => fn (l1,l2) =>((x::l1),(y::l2))) L ([],[]);
   549 
   550 
   551 (*---------------------------------------------------------------------------
   552  * Miscellaneous Syntax manipulation
   553  *---------------------------------------------------------------------------*)
   554 val mk_var = Free;
   555 val mk_const = Const
   556 fun mk_comb(Rator,Rand) = Rator $ Rand;
   557 fun mk_abs(r as (Var((s,_),ty),_))  = Abs(s,ty,abstract_over r)
   558   | mk_abs(r as (Free(s,ty),_))     = Abs(s,ty,abstract_over r)
   559   | mk_abs _ = raise DTYPE_ERR{func="mk_abs", mesg="1st not a variable"};
   560 
   561 fun dest_var(Var((s,i),ty)) = (s,ty)
   562   | dest_var(Free(s,ty))    = (s,ty)
   563   | dest_var _ = raise DTYPE_ERR{func="dest_var", mesg="not a variable"};
   564 
   565 fun dest_const(Const p) = p
   566   | dest_const _ = raise DTYPE_ERR{func="dest_const", mesg="not a constant"};
   567 
   568 fun dest_comb(t1 $ t2) = (t1,t2)
   569   | dest_comb _ =  raise DTYPE_ERR{func = "dest_comb", mesg = "not a comb"};
   570 val rand = #2 o dest_comb;
   571 val rator = #1 o dest_comb;
   572 
   573 fun dest_abs(a as Abs(s,ty,M)) = 
   574      let val v = Free(s, ty)
   575       in (v, betapply (a,v)) end
   576   | dest_abs _ =  raise DTYPE_ERR{func="dest_abs", mesg="not an abstraction"};
   577 
   578 
   579 val bool = Type("bool",[])
   580 and prop = Type("prop",[]);
   581 
   582 fun mk_eq(lhs,rhs) = 
   583    let val ty = type_of lhs
   584        val c = mk_const("op =", ty --> ty --> bool)
   585    in list_comb(c,[lhs,rhs])
   586    end
   587 
   588 fun dest_eq(Const("op =",_) $ M $ N) = (M, N)
   589   | dest_eq _ = raise DTYPE_ERR{func="dest_eq", mesg="not an equality"};
   590 
   591 fun mk_disj(disj1,disj2) =
   592    let val c = Const("op |", bool --> bool --> bool)
   593    in list_comb(c,[disj1,disj2])
   594    end;
   595 
   596 fun mk_forall (r as (Bvar,_)) = 
   597   let val ty = type_of Bvar
   598       val c = Const("All", (ty --> bool) --> bool)
   599   in mk_comb(c, mk_abs r)
   600   end;
   601 
   602 fun mk_exists (r as (Bvar,_)) = 
   603   let val ty = type_of Bvar 
   604       val c = Const("Ex", (ty --> bool) --> bool)
   605   in mk_comb(c, mk_abs r)
   606   end;
   607 
   608 fun mk_prop (tm as Const("Trueprop",_) $ _) = tm
   609   | mk_prop tm = mk_comb(Const("Trueprop", bool --> prop),tm);
   610 
   611 fun drop_prop (Const("Trueprop",_) $ X) = X
   612   | drop_prop X = X;
   613 
   614 fun mk_all (r as (Bvar,_)) = mk_comb(all (type_of Bvar), mk_abs r);
   615 fun list_mk_all(V,t) = itlist(fn v => fn b => mk_all(v,b)) V t;
   616 fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v,b)) V t;
   617 val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1,tm))
   618 
   619 
   620 fun dest_thm thm = 
   621    let val {prop,hyps,...} = rep_thm thm
   622    in (map drop_prop hyps, drop_prop prop)
   623    end;
   624 
   625 val concl = #2 o dest_thm;
   626 
   627 
   628 (*---------------------------------------------------------------------------
   629  * Names of all variables occurring in a term, including bound ones. These
   630  * are added into the second argument.
   631  *---------------------------------------------------------------------------*)
   632 fun add_term_names tm =
   633 let fun insert (x:string) = 
   634      let fun canfind[] = [x] 
   635            | canfind(alist as (y::rst)) = 
   636               if (x<y) then x::alist
   637               else if (x=y) then y::rst
   638               else y::canfind rst 
   639      in canfind end
   640     fun add (Free(s,_)) V = insert s V
   641       | add (Var((s,_),_)) V = insert s V
   642       | add (Abs(s,_,body)) V = add body (insert s V)
   643       | add (f$t) V = add t (add f V)
   644       | add _ V = V
   645 in add tm
   646 end;
   647 
   648 
   649 (*---------------------------------------------------------------------------
   650  * We need to make everything free, so that we can put the term into a
   651  * goalstack, or submit it as an argument to prove_goalw_cterm.
   652  *---------------------------------------------------------------------------*)
   653 fun make_free_ty(Type(s,alist)) = Type(s,map make_free_ty alist)
   654   | make_free_ty(TVar((s,i),srt)) = TFree(s,srt)
   655   | make_free_ty x = x;
   656 
   657 fun make_free (Var((s,_),ty)) = Free(s,make_free_ty ty)
   658   | make_free (Abs(s,x,body)) = Abs(s,make_free_ty x, make_free body)
   659   | make_free (f$t) = (make_free f $ make_free t)
   660   | make_free (Const(s,ty)) = Const(s, make_free_ty ty)
   661   | make_free (Free(s,ty)) = Free(s, make_free_ty ty)
   662   | make_free b = b;
   663 
   664 
   665 (*---------------------------------------------------------------------------
   666  * Structure of case congruence theorem looks like this:
   667  *
   668  *    (M = M') 
   669  *    ==> (!!x1,...,xk. (M' = C1 x1..xk) ==> (f1 x1..xk = f1' x1..xk)) 
   670  *    ==> ... 
   671  *    ==> (!!x1,...,xj. (M' = Cn x1..xj) ==> (fn x1..xj = fn' x1..xj)) 
   672  *    ==>
   673  *      (ty_case f1..fn M = ty_case f1'..fn' m')
   674  *
   675  * The input is the list of rules for the case construct for the type, i.e.,
   676  * that found in the "ty.cases" field of a theory where datatype "ty" is
   677  * defined.
   678  *---------------------------------------------------------------------------*)
   679 
   680 fun build_case_cong sign case_rewrites =
   681  let val clauses = map concl case_rewrites
   682      val clause1 = hd clauses
   683      val left = (#1 o dest_eq) clause1
   684      val ty = type_of ((#2 o dest_comb) left)
   685      val varnames = itlist add_term_names clauses []
   686      val M = variant varnames "M"
   687      val Mvar = Free(M, ty)
   688      val M' = variant (M::varnames) M
   689      val M'var = Free(M', ty)
   690      fun mk_clause clause =
   691        let val (lhs,rhs) = dest_eq clause
   692            val func = (#1 o strip_comb) rhs
   693            val (constr,xbar) = strip_comb(rand lhs)
   694            val (Name,Ty) = dest_var func
   695            val func'name = variant (M::M'::varnames) (Name^"a")
   696            val func' = mk_var(func'name,Ty)
   697        in (func', list_mk_all
   698                   (xbar, Logic.mk_implies
   699                          (mk_prop(mk_eq(M'var, list_comb(constr,xbar))),
   700                           mk_prop(mk_eq(list_comb(func, xbar),
   701                                         list_comb(func',xbar))))))   end
   702      val (funcs',clauses') = unzip (map mk_clause clauses)
   703      val lhsM = mk_comb(rator left, Mvar)
   704      val c = #1(strip_comb left)
   705  in
   706  cterm_of sign
   707   (make_free
   708    (Logic.list_implies(mk_prop(mk_eq(Mvar, M'var))::clauses',
   709                        mk_prop(mk_eq(lhsM, list_comb(c,(funcs'@[M'var])))))))
   710  end
   711  handle _ => raise DTYPE_ERR{func="build_case_cong",mesg="failed"};
   712 
   713   
   714 (*---------------------------------------------------------------------------
   715  * Proves the result of "build_case_cong". 
   716  *---------------------------------------------------------------------------*)
   717 fun prove_case_cong nchotomy case_rewrites ctm =
   718  let val {sign,t,...} = rep_cterm ctm
   719      val (Const("==>",_) $ tm $ _) = t
   720      val (Const("Trueprop",_) $ (Const("op =",_) $ _ $ Ma)) = tm
   721      val (Free(str,_)) = Ma
   722      val thm = prove_goalw_cterm[] ctm
   723               (fn prems =>
   724                [simp_tac (HOL_ss addsimps [hd prems]) 1,
   725                 cut_inst_tac [("x",str)] (nchotomy RS spec) 1,
   726                 REPEAT (SOMEGOAL (etac disjE ORELSE' etac exE)),
   727                 ALLGOALS(asm_simp_tac(HOL_ss addsimps (prems@case_rewrites)))])
   728  in standard (thm RS eq_reflection)
   729  end
   730  handle _ => raise DTYPE_ERR{func="prove_case_cong",mesg="failed"};
   731 
   732 
   733 (*---------------------------------------------------------------------------
   734  * Structure of exhaustion theorem looks like this:
   735  *
   736  *    !v. (EX y1..yi. v = C1 y1..yi) | ... | (EX y1..yj. v = Cn y1..yj)
   737  *
   738  * As for "build_case_cong", the input is the list of rules for the case 
   739  * construct (the case "rewrites").
   740  *---------------------------------------------------------------------------*)
   741 fun build_nchotomy sign case_rewrites =
   742  let val clauses = map concl case_rewrites
   743      val C_ybars = map (rand o #1 o dest_eq) clauses
   744      val varnames = itlist add_term_names C_ybars []
   745      val vname = variant varnames "v"
   746      val ty = type_of (hd C_ybars)
   747      val v = mk_var(vname,ty)
   748      fun mk_disj C_ybar =
   749        let val ybar = #2(strip_comb C_ybar)
   750        in list_mk_exists(ybar, mk_eq(v,C_ybar))
   751        end
   752  in
   753  cterm_of sign
   754    (make_free(mk_prop (mk_forall(v, list_mk_disj (map mk_disj C_ybars)))))
   755  end
   756  handle _ => raise DTYPE_ERR{func="build_nchotomy",mesg="failed"};
   757 
   758 
   759 (*---------------------------------------------------------------------------
   760  * Takes the induction tactic for the datatype, and the result from 
   761  * "build_nchotomy" and proves the theorem.
   762  *---------------------------------------------------------------------------*)
   763 
   764 fun prove_nchotomy induct_tac case_rewrites ctm =
   765  let val {sign,t,...} = rep_cterm ctm
   766      val (Const ("Trueprop",_) $ g) = t
   767      val (Const ("All",_) $ Abs (v,_,_)) = g
   768  in 
   769  prove_goalw_cterm[] ctm
   770      (fn _ => [rtac allI 1,
   771                induct_tac v 1,
   772                ALLGOALS (simp_tac (HOL_ss addsimps case_rewrites)),
   773                ALLGOALS (fast_tac HOL_cs)])
   774  end
   775  handle _ => raise DTYPE_ERR {func="prove_nchotomy", mesg="failed"};
   776 
   777 
   778 (*---------------------------------------------------------------------------
   779  * Brings the preceeding functions together.
   780  *---------------------------------------------------------------------------*)
   781 fun case_thms sign case_rewrites induct_tac =
   782   let val nchotomy = prove_nchotomy induct_tac case_rewrites
   783                             (build_nchotomy sign case_rewrites)
   784       val cong = prove_case_cong nchotomy case_rewrites
   785                                  (build_case_cong sign case_rewrites)
   786   in {nchotomy=nchotomy, case_cong=cong}
   787   end;
   788 
   789 (*---------------------------------------------------------------------------
   790  * Tests
   791  *
   792  * 
   793      Dtype.case_thms (sign_of List.thy) List.list.cases List.list.induct_tac;
   794      Dtype.case_thms (sign_of Prod.thy) [split] 
   795                      (fn s => res_inst_tac [("p",s)] PairE_lemma);
   796      Dtype.case_thms (sign_of Nat.thy) [nat_case_0, nat_case_Suc] nat_ind_tac;
   797 
   798  *
   799  *---------------------------------------------------------------------------*)
   800 
   801 
   802 (*---------------------------------------------------------------------------
   803  * Given a theory and the name (and constructors) of a datatype declared in 
   804  * an ancestor of that theory and an induction tactic for that datatype, 
   805  * return the information that TFL needs. This should only be called once for
   806  * a datatype, because "build_record" proves various facts, and thus is slow. 
   807  * It fails on the datatype of pairs, which must be included for TFL to work. 
   808  * The test shows how to  build the record for pairs.
   809  *---------------------------------------------------------------------------*)
   810 
   811 local fun mk_rw th = (th RS eq_reflection) handle _ => th
   812       fun get_fact thy s = (get_axiom thy s handle _ => get_thm thy s)
   813 in
   814 fun build_record (thy,(ty,cl),itac) =
   815  let val sign = sign_of thy
   816      fun const s = Const(s, the(Sign.const_type sign s))
   817      val case_rewrites = map (fn c => get_fact thy (ty^"_case_"^c)) cl
   818      val {nchotomy,case_cong} = case_thms sign case_rewrites itac
   819  in
   820   (ty, {constructors = map(fn s => const s handle _ => const("op "^s)) cl,
   821         case_const = const (ty^"_case"),
   822         case_rewrites = map mk_rw case_rewrites,
   823         nchotomy = nchotomy,
   824         case_cong = case_cong})
   825  end
   826 end;
   827 
   828 
   829 (*---------------------------------------------------------------------------
   830  * Test
   831  *
   832  * 
   833     map Dtype.build_record 
   834           [(Nat.thy, ("nat",["0", "Suc"]), nat_ind_tac),
   835            (List.thy,("list",["[]", "#"]), List.list.induct_tac)]
   836     @
   837     [let val prod_case_thms = Dtype.case_thms (sign_of Prod.thy) [split] 
   838                                  (fn s => res_inst_tac [("p",s)] PairE_lemma)
   839          fun const s = Const(s, the(Sign.const_type (sign_of Prod.thy) s))
   840      in ("*", 
   841          {constructors = [const "Pair"],
   842             case_const = const "split",
   843          case_rewrites = [split RS eq_reflection],
   844              case_cong = #case_cong prod_case_thms,
   845               nchotomy = #nchotomy prod_case_thms}) end];
   846 
   847  *
   848  *---------------------------------------------------------------------------*)
   849 
   850 end;