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