src/HOL/datatype.ML

adapted proof of drop_succ_Cons: problem with non-confluent simpset removed

(* Title:       HOL/datatype.ML
   ID:          $Id$
   Author:      Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker
   Copyright 1995 TU Muenchen
*)


(*used for constructor parameters*)
datatype dt_type = dtVar of string |
  dtTyp of dt_type list * string |
  dtRek of dt_type list * string;

structure Datatype =
struct
local 

val mysort = sort;
open ThyParse HOLogic;
exception Impossible;
exception RecError of string;

val is_dtRek = (fn dtRek _ => true  |  _  => false);
fun opt_parens s = if s = "" then "" else enclose "(" ")" s; 

(* ----------------------------------------------------------------------- *)
(* Derivation of the primrec combinator application from the equations     *)

(* substitute fname(ls,xk,rs) by yk(ls,rs) in t for (xk,yk) in pairs  *) 

fun subst_apps (_,_) [] t = t
  | subst_apps (fname,rpos) pairs t =
    let 
    fun subst (Abs(a,T,t)) = Abs(a,T,subst t)
      | subst (funct $ body) = 
        let val (f,b) = strip_comb (funct$body)
        in 
          if is_Const f andalso fst(dest_Const f) = fname 
            then 
              let val (ls,rest) = (take(rpos,b), drop(rpos,b));
                val (xk,rs) = (hd rest,tl rest)
                  handle LIST _ => raise RecError "not enough arguments \
                   \ in recursive application on rhs"
              in 
                (case assoc (pairs,xk) of 
                   None   => list_comb(f, map subst b)
                 | Some U => list_comb(U, map subst (ls @ rs)))
              end
          else list_comb(f, map subst b)
        end
      | subst(t) = t
    in subst t end;
  
(* abstract rhs *)

fun abst_rec (fname,rpos,tc,ls,cargs,rs,rhs) =       
  let val rargs = (map fst o 
                   (filter (fn (a,T) => is_dtRek T))) (cargs ~~ tc);
      val subs = map (fn (s,T) => (s,dummyT))
                   (rev(rename_wrt_term rhs rargs));
      val subst_rhs = subst_apps (fname,rpos)
                        (map Free rargs ~~ map Free subs) rhs;
  in 
      list_abs_free (cargs @ subs @ ls @ rs, subst_rhs) 
  end;

(* parsing the prim rec equations *)

fun dest_eq ( Const("Trueprop",_) $ (Const ("op =",_) $ lhs $ rhs))
                 = (lhs, rhs)
   | dest_eq _ = raise RecError "not a proper equation"; 

fun dest_rec eq = 
  let val (lhs,rhs) = dest_eq eq; 
    val (name,args) = strip_comb lhs; 
    val (ls',rest)  = take_prefix is_Free args; 
    val (middle,rs') = take_suffix is_Free rest;
    val rpos = length ls';
    val (c,cargs') = strip_comb (hd middle)
      handle LIST "hd" => raise RecError "constructor missing";
    val (ls,cargs,rs) = (map dest_Free ls', map dest_Free cargs'
                         , map dest_Free rs')
      handle TERM ("dest_Free",_) => 
          raise RecError "constructor has illegal argument in pattern";
  in 
    if length middle > 1 then 
      raise RecError "more than one non-variable in pattern"
    else if not(null(findrep (map fst (ls @ rs @ cargs)))) then 
      raise RecError "repeated variable name in pattern" 
         else (fst(dest_Const name) handle TERM _ => 
               raise RecError "function is not declared as constant in theory"
                 ,rpos,ls,fst( dest_Const c),cargs,rs,rhs)
  end; 

(* check function specified for all constructors and sort function terms *)

fun check_and_sort (n,its) = 
  if length its = n 
    then map snd (mysort (fn ((i : int,_),(j,_)) => i<j) its)
  else raise error "Primrec definition error:\n\
   \Please give an equation for every constructor";

(* translate rec equations into function arguments suitable for rec comb *)
(* theory parameter needed for printing error messages                   *) 

fun trans_recs _ _ [] = error("No primrec equations.")
  | trans_recs thy cs' (eq1::eqs) = 
    let val (name1,rpos1,ls1,_,_,_,_) = dest_rec eq1
      handle RecError s =>
        error("Primrec definition error: " ^ s ^ ":\n" 
              ^ "   " ^ Sign.string_of_term (sign_of thy) eq1);
      val tcs = map (fn (_,c,T,_,_) => (c,T)) cs';  
      val cs = map fst tcs;
      fun trans_recs' _ [] = []
        | trans_recs' cis (eq::eqs) = 
          let val (name,rpos,ls,c,cargs,rs,rhs) = dest_rec eq; 
            val tc = assoc(tcs,c);
            val i = (1 + find (c,cs))  handle LIST "find" => 0; 
          in
          if name <> name1 then 
            raise RecError "function names inconsistent"
          else if rpos <> rpos1 then 
            raise RecError "position of rec. argument inconsistent"
          else if i = 0 then 
            raise RecError "illegal argument in pattern" 
          else if i mem cis then
            raise RecError "constructor already occured as pattern "
               else (i,abst_rec (name,rpos,the tc,ls,cargs,rs,rhs))
                     :: trans_recs' (i::cis) eqs 
          end
          handle RecError s =>
                error("Primrec definition error\n" ^ s ^ "\n" 
                      ^ "   " ^ Sign.string_of_term (sign_of thy) eq);
    in (  name1, ls1
        , check_and_sort (length cs, trans_recs' [] (eq1::eqs)))
    end ;

in
  fun add_datatype (typevars, tname, cons_list') thy = 
    let
      fun typid(dtRek(_,id)) = id
        | typid(dtVar s) = implode (tl (explode s))
        | typid(dtTyp(_,id)) = id;

      fun index_vnames(vn::vns,tab) =
            (case assoc(tab,vn) of
               None => if vn mem vns
                       then (vn^"1") :: index_vnames(vns,(vn,2)::tab)
                       else vn :: index_vnames(vns,tab)
             | Some(i) => (vn^(string_of_int i)) ::
                          index_vnames(vns,(vn,i+1)::tab))
        | index_vnames([],tab) = [];

      fun mk_var_names types = index_vnames(map typid types,[]);

      (*search for free type variables and convert recursive *)
      fun analyse_types (cons, types, syn) =
        let fun analyse(t as dtVar v) =
                  if t mem typevars then t
                  else error ("Free type variable " ^ v ^ " on rhs.")
              | analyse(dtTyp(typl,s)) =
                  if tname <> s then dtTyp(analyses typl, s)
                  else if typevars = typl then dtRek(typl, s)
                       else error (s ^ " used in different ways")
              | analyse(dtRek _) = raise Impossible
            and analyses ts = map analyse ts;
        in (cons, Syntax.const_name cons syn, analyses types,
            mk_var_names types, syn)
        end;

     (*test if all elements are recursive, i.e. if the type is empty*)
      
      fun non_empty (cs : ('a * 'b * dt_type list * 'c *'d) list) = 
        not(forall (exists is_dtRek o #3) cs) orelse
        error("Empty datatype not allowed!");

      val cons_list = map analyse_types cons_list';
      val dummy = non_empty cons_list;
      val num_of_cons = length cons_list;

     (* Auxiliary functions to construct argument and equation lists *)

     (*generate 'var_n, ..., var_m'*)
      fun Args(var, delim, n, m) = 
        space_implode delim (map (fn n => var^string_of_int(n)) (n upto m));

      fun C_exp name vns = name ^ opt_parens(space_implode ") (" vns);

     (*Arg_eqs([x1,...,xn],[y1,...,yn]) = "x1 = y1 & ... & xn = yn" *)
      fun arg_eqs vns vns' =
        let fun mkeq(x,x') = x ^ "=" ^ x'
        in space_implode " & " (map mkeq (vns~~vns')) end;

     (*Pretty printers for type lists;
       pp_typlist1: parentheses, pp_typlist2: brackets*)
      fun pp_typ (dtVar s) = "(" ^ s ^ "::term)"
        | pp_typ (dtTyp (typvars, id)) =
          if null typvars then id else (pp_typlist1 typvars) ^ id
        | pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id
      and
        pp_typlist' ts = commas (map pp_typ ts)
      and
        pp_typlist1 ts = if null ts then "" else parens (pp_typlist' ts);

      fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts);

     (* Generate syntax translation for case rules *)
      fun calc_xrules c_nr y_nr ((_, name, _, vns, _) :: cs) = 
        let val arity = length vns;
          val body  = "z" ^ string_of_int(c_nr);
          val args1 = if arity=0 then ""
                      else " " ^ Args ("y", " ", y_nr, y_nr+arity-1);
          val args2 = if arity=0 then ""
                      else "(% " ^ Args ("y", " ", y_nr, y_nr+arity-1) 
                        ^ ". ";
          val (rest1,rest2) = 
            if null cs then ("","")
            else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs
            in (" | " ^ h1, " " ^ h2) end;
        in (name ^ args1 ^ " => " ^ body ^ rest1,
            args2 ^ body ^ (if args2 = "" then "" else ")") ^ rest2)
        end
        | calc_xrules _ _ [] = raise Impossible;
      
      val xrules =
        let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
        in [("logic", "case x of " ^ first_part) <->
             ("logic", tname ^ "_case " ^ scnd_part ^ " x")]
        end;

     (*type declarations for constructors*)
      fun const_type (id, _, typlist, _, syn) =
        (id,  
         (if null typlist then "" else pp_typlist2 typlist ^ " => ") ^
            pp_typlist1 typevars ^ tname, syn);


      fun assumpt (dtRek _ :: ts, v :: vs ,found) =
        let val h = if found then ";P(" ^ v ^ ")" else "[| P(" ^ v ^ ")"
        in h ^ (assumpt (ts, vs, true)) end
        | assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found)
      | assumpt ([], [], found) = if found then "|] ==>" else ""
        | assumpt _ = raise Impossible;

      fun t_inducting ((_, name, types, vns, _) :: cs) =
        let
          val h = if null types then " P(" ^ name ^ ")"
                  else " !!" ^ (space_implode " " vns) ^ "." ^
                    (assumpt (types, vns, false)) ^
                    "P(" ^ C_exp name vns ^ ")";
          val rest = t_inducting cs;
        in if rest = "" then h else h ^ "; " ^ rest end
        | t_inducting [] = "";

      fun t_induct cl typ_name =
        "[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")";

      fun gen_typlist typevar f ((_, _, ts, _, _) :: cs) =
        let val h = if (length ts) > 0
                      then pp_typlist2(f ts) ^ "=>"
                    else ""
        in h ^ typevar ^  "," ^ (gen_typlist typevar f cs) end
        | gen_typlist _ _ [] = "";


(* -------------------------------------------------------------------- *)
(* The case constant and rules                                          *)
                
      val t_case = tname ^ "_case";

      fun case_rule n (id, name, _, vns, _) =
        let val args = if vns = [] then "" else " " ^ space_implode " " vns
        in (t_case ^ "_" ^ id,
            t_case ^ " " ^ Args("f", " ", 1, num_of_cons)
            ^ " (" ^ name ^ args ^ ") = f"^string_of_int(n) ^ args)
        end

      fun case_rules n (c :: cs) = case_rule n c :: case_rules(n+1) cs
        | case_rules _ [] = [];

      val datatype_arity = length typevars;

      val types = [(tname, datatype_arity, NoSyn)];

      val arities = 
        let val term_list = replicate datatype_arity termS;
        in [(tname, term_list, termS)] 
        end;

      val datatype_name = pp_typlist1 typevars ^ tname;

      val new_tvar_name = variant (map (fn dtVar s => s) typevars) "'z";

      val case_const =
        (t_case,
         "[" ^ gen_typlist new_tvar_name I cons_list 
         ^  pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name^"::term",
         NoSyn);

      val rules_case = case_rules 1 cons_list;

(* -------------------------------------------------------------------- *)
(* The prim-rec combinator                                              *) 

      val t_rec = tname ^ "_rec"

(* adding type variables for dtRek types to end of list of dt_types      *)   

      fun add_reks ts = 
        ts @ map (fn _ => dtVar new_tvar_name) (filter is_dtRek ts); 

(* positions of the dtRek types in a list of dt_types, starting from 1  *)
      fun rek_vars ts vns = map snd (filter (is_dtRek o fst) (ts ~~ vns))

      fun rec_rule n (id,name,ts,vns,_) = 
        let val args = opt_parens(space_implode ") (" vns)
          val fargs = opt_parens(Args("f", ") (", 1, num_of_cons))
          fun rarg vn = t_rec ^ fargs ^ " (" ^ vn ^ ")"
          val rargs = opt_parens(space_implode ") ("
                                 (map rarg (rek_vars ts vns)))
        in
          (t_rec ^ "_" ^ id,
           t_rec ^ fargs ^ " (" ^ name ^ args ^ ") = f"
           ^ string_of_int(n) ^ args ^ rargs)
        end

      fun rec_rules n (c::cs) = rec_rule n c :: rec_rules (n+1) cs 
        | rec_rules _ [] = [];

      val rec_const =
        (t_rec,
         "[" ^ (gen_typlist new_tvar_name add_reks cons_list) 
         ^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name^"::term",
         NoSyn);

      val rules_rec = rec_rules 1 cons_list

(* -------------------------------------------------------------------- *)
      val consts = 
        map const_type cons_list
        @ (if num_of_cons < dtK then []
           else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)])
        @ [case_const,rec_const];


      fun Ci_ing ((id, name, _, vns, _) :: cs) =
           if null vns then Ci_ing cs
           else let val vns' = variantlist(vns,vns)
                in ("inject_" ^ id,
                    "(" ^ (C_exp name vns) ^ "=" ^ (C_exp name vns')
                    ^ ") = (" ^ (arg_eqs vns vns') ^ ")") :: (Ci_ing cs)
                end
        | Ci_ing [] = [];

      fun Ci_negOne (id1,name1,_,vns1,_) (id2,name2,_,vns2,_) =
            let val vns2' = variantlist(vns2,vns1)
                val ax = C_exp name1 vns1 ^ "~=" ^ C_exp name2 vns2'
        in (id1 ^ "_not_" ^ id2, ax) end;

      fun Ci_neg1 [] = []
        | Ci_neg1 (c1::cs) = (map (Ci_negOne c1) cs) @ Ci_neg1 cs;

      fun suc_expr n = 
        if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")";

      fun Ci_neg2() =
        let val ord_t = tname ^ "_ord";
          val cis = cons_list ~~ (0 upto (num_of_cons - 1))
          fun Ci_neg2equals ((id, name, _, vns, _), n) =
            let val ax = ord_t ^ "(" ^ (C_exp name vns) ^ ") = " ^ (suc_expr n)
            in (ord_t ^ "_" ^ id, ax) end
        in (ord_t ^ "_distinct", ord_t^"(x) ~= "^ord_t^"(y) ==> x ~= y") ::
          (map Ci_neg2equals cis)
        end;

      val rules_distinct = if num_of_cons < dtK then Ci_neg1 cons_list
                           else Ci_neg2();

      val rules_inject = Ci_ing cons_list;

      val rule_induct = (tname ^ "_induct", t_induct cons_list tname);

      val rules = rule_induct ::
        (rules_inject @ rules_distinct @ rules_case @ rules_rec);

      fun add_primrec eqns thy =
        let val rec_comb = Const(t_rec,dummyT)
          val teqns = map (fn neq => snd(read_axm (sign_of thy) neq)) eqns
          val (fname,ls,fns) = trans_recs thy cons_list teqns
          val rhs = 
            list_abs_free
            (ls @ [(tname,dummyT)]
             ,list_comb(rec_comb
                        , fns @ map Bound (0 ::(length ls downto 1))));
          val sg = sign_of thy;
          val defpair = (fname ^ "_" ^ tname ^ "_def",
                         Logic.mk_equals (Const(fname,dummyT), rhs))
          val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair;
          val varT = Type.varifyT T;
          val ftyp = the (Sign.const_type sg fname);
        in add_defs_i [defpairT] thy end;

    in
      datatypes := map (fn (x,_,_) => x) cons_list' @ (!datatypes);
      (thy |> add_types types
           |> add_arities arities
           |> add_consts consts
           |> add_trrules xrules
           |> add_axioms rules, add_primrec)
    end
end
end

(*
Informal description of functions used in datatype.ML for the Isabelle/HOL
implementation of prim. rec. function definitions. (N. Voelker, Feb. 1995) 

* subst_apps (fname,rpos) pairs t:
   substitute the term 
       fname(ls,xk,rs) 
   by 
      yk(ls,rs) 
   in t for (xk,yk) in pairs, where rpos = length ls. 
   Applied with : 
     fname = function name 
     rpos = position of recursive argument 
     pairs = list of pairs (xk,yk), where 
          xk are the rec. arguments of the constructor in the pattern,
          yk is a variable with name derived from xk 
     t = rhs of equation 

* abst_rec (fname,rpos,tc,ls,cargs,rs,rhs)
  - filter recursive arguments from constructor arguments cargs,
  - perform substitutions on rhs, 
  - derive list subs of new variable names yk for use in subst_apps, 
  - abstract rhs with respect to cargs, subs, ls and rs. 

* dest_eq t 
  destruct a term denoting an equation into lhs and rhs. 

* dest_req eq 
  destruct an equation of the form 
      name (vl1..vlrpos, Ci(vi1..vin), vr1..vrn) = rhs
  into 
  - function name  (name) 
  - position of the first non-variable parameter  (rpos)
  - the list of first rpos parameters (ls = [vl1..vlrpos]) 
  - the constructor (fst( dest_Const c) = Ci)
  - the arguments of the constructor (cargs = [vi1..vin])
  - the rest of the variables in the pattern (rs = [vr1..vrn])
  - the right hand side of the equation (rhs).  
 
* check_and_sort (n,its)
  check that  n = length its holds, and sort elements of its by 
  first component. 

* trans_recs thy cs' (eq1::eqs)
  destruct eq1 into name1, rpos1, ls1, etc.. 
  get constructor list with and without type (tcs resp. cs) from cs',  
  for every equation:  
    destruct it into (name,rpos,ls,c,cargs,rs,rhs)
    get typed constructor tc from c and tcs 
    determine the index i of the constructor 
    check function name and position of rec. argument by comparison
    with first equation 
    check for repeated variable names in pattern
    derive function term f_i which is used as argument of the rec. combinator
    sort the terms f_i according to i and return them together
      with the function name and the parameter of the definition (ls). 

* Application:

  The rec. combinator is applied to the function terms resulting from
  trans_rec. This results in a function which takes the recursive arg. 
  as first parameter and then the arguments corresponding to ls. The
  order of parameters is corrected by setting the rhs equal to 

  list_abs_free
            (ls @ [(tname,dummyT)]
             ,list_comb(rec_comb
                        , fns @ map Bound (0 ::(length ls downto 1))));

  Note the de-Bruijn indices counting the number of lambdas between the
  variable and its binding. 
*)