src/ZF/Tools/datatype_package.ML
author paulson
Mon, 28 Dec 1998 16:58:11 +0100
changeset 6052 4f093e55beeb
child 6065 3b4a29166f26
permissions -rw-r--r--
revised datatype definition package
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6052
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     1
(*  Title:      ZF/datatype_package.ML
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     2
    ID:         $Id$
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     5
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     6
Fixedpoint definition module -- for Inductive/Codatatype Definitions
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     7
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     8
The functor will be instantiated for normal sums/products (datatype defs)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
     9
                         and non-standard sums/products (codatatype defs)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    10
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    11
Sums are used only for mutual recursion;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    12
Products are used only to derive "streamlined" induction rules for relations
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    13
*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    14
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    15
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    16
(** Datatype information, e.g. associated theorems **)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    17
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    18
type datatype_info =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    19
  {inductive: bool,		(*true if inductive, not coinductive*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    20
   constructors : term list,    (*the constructors, as Consts*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    21
   rec_rewrites : thm list,     (*recursor equations*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    22
   case_rewrites : thm list,    (*case equations*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    23
   induct : thm,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    24
   mutual_induct : thm,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    25
   exhaustion : thm};
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    26
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    27
structure DatatypesArgs =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    28
  struct
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    29
  val name = "ZF/datatypes";
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    30
  type T = datatype_info Symtab.table;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    31
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    32
  val empty = Symtab.empty;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    33
  val prep_ext = I;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    34
  val merge: T * T -> T = Symtab.merge (K true);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    35
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    36
  fun print sg tab =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    37
    Pretty.writeln (Pretty.strs ("datatypes:" ::
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    38
      map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    39
  end;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    40
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    41
structure DatatypesData = TheoryDataFun(DatatypesArgs);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    42
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    43
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    44
(** Constructor information: needed to map constructors to datatypes **)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    45
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    46
type constructor_info =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    47
  {big_rec_name : string,     (*name of the mutually recursive set*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    48
   constructors : term list,  (*the constructors, as Consts*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    49
   rec_rewrites : thm list};  (*recursor equations*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    50
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    51
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    52
structure ConstructorsArgs =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    53
struct
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    54
  val name = "ZF/constructors"
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    55
  type T = constructor_info Symtab.table
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    56
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    57
  val empty = Symtab.empty
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    58
  val prep_ext = I
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    59
  val merge: T * T -> T = Symtab.merge (K true)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    60
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    61
  fun print sg tab = ()   (*nothing extra to print*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    62
end;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    63
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    64
structure ConstructorsData = TheoryDataFun(ConstructorsArgs);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    65
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    66
val setup_datatypes = [DatatypesData.init, ConstructorsData.init];
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    67
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    68
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    69
type datatype_result =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    70
   {con_defs   : thm list,             (*definitions made in thy*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    71
    case_eqns  : thm list,             (*equations for case operator*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    72
    recursor_eqns : thm list,          (*equations for the recursor*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    73
    free_iffs  : thm list,             (*freeness rewrite rules*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    74
    free_SEs   : thm list,             (*freeness destruct rules*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    75
    mk_free    : string -> thm};      (*makes freeness theorems*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    76
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    77
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    78
signature DATATYPE_ARG =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    79
  sig 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    80
  val intrs : thm list
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    81
  val elims : thm list
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    82
  end;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    83
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    84
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    85
(*Functor's result signature*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    86
signature DATATYPE_PACKAGE =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    87
  sig 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    88
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    89
  (*Insert definitions for the recursive sets, which
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    90
     must *already* be declared as constants in parent theory!*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    91
  val add_datatype_i : 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    92
      term * term list * Ind_Syntax.constructor_spec list list * 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    93
      thm list * thm list * thm list
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    94
      -> theory -> theory * inductive_result * datatype_result
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    95
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    96
  val add_datatype : 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    97
      string * string list * 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    98
      (string * string list * mixfix) list list *
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
    99
      thm list * thm list * thm list
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   100
      -> theory -> theory * inductive_result * datatype_result
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   101
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   102
  end;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   103
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   104
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   105
(*Declares functions to add fixedpoint/constructor defs to a theory.
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   106
  Recursive sets must *already* be declared as constants.*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   107
functor Add_datatype_def_Fun 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   108
    (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   109
 	   and Ind_Package : INDUCTIVE_PACKAGE
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   110
           and Datatype_Arg : DATATYPE_ARG)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   111
 : DATATYPE_PACKAGE =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   112
struct
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   113
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   114
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   115
(*con_ty_lists specifies the constructors in the form (name,prems,mixfix) *)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   116
fun add_datatype_i (dom_sum, rec_tms, con_ty_lists, 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   117
		    monos, type_intrs, type_elims) thy =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   118
 let
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   119
  open BasisLibrary
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   120
  val dummy = (*has essential ancestors?*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   121
    Theory.requires thy "Datatype" "(co)datatype definitions";
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   122
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   123
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   124
  val rec_names = map (#1 o dest_Const o head_of) rec_tms
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   125
  val rec_base_names = map Sign.base_name rec_names
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   126
  val big_rec_base_name = space_implode "_" rec_base_names
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   127
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   128
  val thy_path = thy |> Theory.add_path big_rec_base_name
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   129
  val sign = sign_of thy_path
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   130
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   131
  val big_rec_name = Sign.intern_const sign big_rec_base_name;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   132
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   133
  val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   134
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   135
  val dummy =	
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   136
	writeln ((if (#1 (dest_Const Fp.oper) = "lfp") then "Datatype" 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   137
		  else "Codatatype")
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   138
		 ^ " definition " ^ big_rec_name)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   139
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   140
  val case_varname = "f";                (*name for case variables*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   141
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   142
  (** Define the constructors **)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   143
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   144
  (*The empty tuple is 0*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   145
  fun mk_tuple [] = Const("0",iT)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   146
    | mk_tuple args = foldr1 (app Pr.pair) args;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   147
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   148
  fun mk_inject n k u = access_bal (ap Su.inl, ap Su.inr, u) n k;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   149
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   150
  val npart = length rec_names;  (*number of mutually recursive parts*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   151
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   152
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   153
  val full_name = Sign.full_name sign;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   154
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   155
  (*Make constructor definition; 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   156
    kpart is the number of this mutually recursive part*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   157
  fun mk_con_defs (kpart, con_ty_list) = 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   158
    let val ncon = length con_ty_list    (*number of constructors*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   159
	fun mk_def (((id,T,syn), name, args, prems), kcon) =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   160
	      (*kcon is index of constructor*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   161
	    Logic.mk_defpair (list_comb (Const (full_name name, T), args),
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   162
			mk_inject npart kpart
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   163
			(mk_inject ncon kcon (mk_tuple args)))
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   164
    in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   165
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   166
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   167
  (*** Define the case operator ***)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   168
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   169
  (*Combine split terms using case; yields the case operator for one part*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   170
  fun call_case case_list = 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   171
    let fun call_f (free,[]) = Abs("null", iT, free)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   172
	  | call_f (free,args) =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   173
		CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   174
			    Ind_Syntax.iT 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   175
			    free 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   176
    in  fold_bal (app Su.elim) (map call_f case_list)  end;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   177
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   178
  (** Generating function variables for the case definition
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   179
      Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   180
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   181
  (*The function variable for a single constructor*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   182
  fun add_case (((_, T, _), name, args, _), (opno, cases)) =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   183
    if Syntax.is_identifier name then
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   184
      (opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   185
    else
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   186
      (opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args) 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   187
       :: cases);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   188
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   189
  (*Treatment of a list of constructors, for one part
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   190
    Result adds a list of terms, each a function variable with arguments*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   191
  fun add_case_list (con_ty_list, (opno, case_lists)) =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   192
    let val (opno', case_list) = foldr add_case (con_ty_list, (opno, []))
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   193
    in (opno', case_list :: case_lists) end;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   194
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   195
  (*Treatment of all parts*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   196
  val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   197
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   198
  (*extract the types of all the variables*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   199
  val case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   200
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   201
  val case_base_name = big_rec_base_name ^ "_case";
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   202
  val case_name = full_name case_base_name;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   203
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   204
  (*The list of all the function variables*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   205
  val case_args = flat (map (map #1) case_lists);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   206
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   207
  val case_const = Const (case_name, case_typ); 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   208
  val case_tm = list_comb (case_const, case_args);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   209
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   210
  val case_def = Logic.mk_defpair
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   211
           (case_tm, fold_bal (app Su.elim) (map call_case case_lists));
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   212
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   213
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   214
  (** Generating function variables for the recursor definition
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   215
      Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   216
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   217
  (*a recursive call for x is the application rec`x  *)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   218
  val rec_call = Ind_Syntax.apply_const $ Free ("rec", iT);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   219
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   220
  (*look back down the "case args" (which have been reversed) to 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   221
    determine the de Bruijn index*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   222
  fun make_rec_call ([], _) arg = error
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   223
	  "Internal error in datatype (variable name mismatch)" 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   224
    | make_rec_call (a::args, i) arg = 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   225
	   if a = arg then rec_call $ Bound i
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   226
	   else make_rec_call (args, i+1) arg;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   227
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   228
  (*creates one case of the "X_case" definition of the recursor*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   229
  fun call_recursor ((case_var, case_args), (recursor_var, recursor_args)) = 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   230
      let fun add_abs (Free(a,T), u) = Abs(a,T,u)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   231
	  val ncase_args = length case_args
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   232
	  val bound_args = map Bound ((ncase_args - 1) downto 0)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   233
	  val rec_args = map (make_rec_call (rev case_args,0))
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   234
			 (List.drop(recursor_args, ncase_args))
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   235
      in
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   236
	  foldr add_abs
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   237
	    (case_args, list_comb (recursor_var,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   238
				   bound_args @ rec_args))
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   239
      end
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   240
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   241
  (*Find each recursive argument and add a recursive call for it*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   242
  fun rec_args [] = []
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   243
    | rec_args ((Const("op :",_)$arg$X)::prems) =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   244
       (case head_of X of
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   245
	    Const(a,_) => (*recursive occurrence?*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   246
			  if Sign.base_name a mem_string rec_base_names
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   247
			      then arg :: rec_args prems 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   248
			  else rec_args prems
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   249
	  | _ => rec_args prems)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   250
    | rec_args (_::prems) = rec_args prems;	  
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   251
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   252
  (*Add an argument position for each occurrence of a recursive set.
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   253
    Strictly speaking, the recursive arguments are the LAST of the function
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   254
    variable, but they all have type "i" anyway*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   255
  fun add_rec_args args' T = (map (fn _ => iT) args') ---> T
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   256
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   257
  (*Plug in the function variable type needed for the recursor
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   258
    as well as the new arguments (recursive calls)*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   259
  fun rec_ty_elem ((id, T, syn), name, args, prems) =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   260
      let val args' = rec_args prems 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   261
      in ((id, add_rec_args args' T, syn), 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   262
	  name, args @ args', prems)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   263
      end;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   264
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   265
  val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists); 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   266
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   267
  (*Treatment of all parts*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   268
  val (_, recursor_lists) = foldr add_case_list (rec_ty_lists, (1,[]));
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   269
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   270
  (*extract the types of all the variables*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   271
  val recursor_typ = flat (map (map (#2 o #1)) rec_ty_lists)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   272
			 ---> (iT-->iT);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   273
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   274
  val recursor_base_name = big_rec_base_name ^ "_rec";
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   275
  val recursor_name = full_name recursor_base_name;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   276
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   277
  (*The list of all the function variables*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   278
  val recursor_args = flat (map (map #1) recursor_lists);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   279
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   280
  val recursor_tm =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   281
    list_comb (Const (recursor_name, recursor_typ), recursor_args); 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   282
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   283
  val recursor_cases = map call_recursor 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   284
			 (flat case_lists ~~ flat recursor_lists)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   285
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   286
  val recursor_def = 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   287
      Logic.mk_defpair
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   288
        (recursor_tm, 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   289
	 Ind_Syntax.Vrecursor_const $ 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   290
  	   absfree ("rec", iT, list_comb (case_const, recursor_cases)));
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   291
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   292
  (* Build the new theory *)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   293
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   294
  val need_recursor = 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   295
      (#1 (dest_Const Fp.oper) = "lfp" andalso recursor_typ <> case_typ);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   296
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   297
  fun add_recursor thy = 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   298
      if need_recursor then
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   299
	   thy |> Theory.add_consts_i 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   300
	            [(recursor_base_name, recursor_typ, NoSyn)]
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   301
	       |> PureThy.add_defs_i [Attribute.none recursor_def]
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   302
      else thy;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   303
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   304
  val thy0 = thy_path
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   305
	     |> Theory.add_consts_i 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   306
		 ((case_base_name, case_typ, NoSyn) ::
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   307
		  map #1 (flat con_ty_lists))
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   308
	     |> PureThy.add_defs_i
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   309
		 (map Attribute.none 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   310
		  (case_def :: 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   311
		   flat (ListPair.map mk_con_defs
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   312
			 (1 upto npart, con_ty_lists))))
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   313
	     |> add_recursor
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   314
	     |> Theory.parent_path
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   315
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   316
  val con_defs = get_def thy0 case_name :: 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   317
		 map (get_def thy0 o #2) (flat con_ty_lists);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   318
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   319
  val (thy1, ind_result) = 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   320
         thy0  |> Ind_Package.add_inductive_i
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   321
	            false (rec_tms, dom_sum, intr_tms, 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   322
			   monos, con_defs, 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   323
			   type_intrs @ Datatype_Arg.intrs, 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   324
			   type_elims @ Datatype_Arg.elims)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   325
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   326
  (**** Now prove the datatype theorems in this theory ****)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   327
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   328
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   329
  (*** Prove the case theorems ***)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   330
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   331
  (*Each equation has the form 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   332
    case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   333
  fun mk_case_eqn (((_,T,_), name, args, _), case_free) = 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   334
    FOLogic.mk_Trueprop
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   335
      (FOLogic.mk_eq
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   336
       (case_tm $
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   337
	 (list_comb (Const (Sign.intern_const (sign_of thy1) name,T), 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   338
		     args)),
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   339
	list_comb (case_free, args)));
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   340
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   341
  val case_trans = hd con_defs RS Ind_Syntax.def_trans
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   342
  and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   343
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   344
  (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   345
  fun case_tacsf con_def _ = 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   346
    [rewtac con_def,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   347
     rtac case_trans 1,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   348
     REPEAT (resolve_tac [refl, split_trans, 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   349
			  Su.case_inl RS trans, 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   350
			  Su.case_inr RS trans] 1)];
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   351
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   352
  fun prove_case_eqn (arg,con_def) =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   353
      prove_goalw_cterm [] 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   354
	(Ind_Syntax.traceIt "next case equation = "
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   355
	   (cterm_of (sign_of thy1) (mk_case_eqn arg)))
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   356
	(case_tacsf con_def);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   357
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   358
  val con_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   359
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   360
  val case_eqns = 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   361
      map prove_case_eqn 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   362
	 (flat con_ty_lists ~~ case_args ~~ tl con_defs);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   363
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   364
  (*** Prove the recursor theorems ***)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   365
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   366
  val recursor_eqns = case try (get_def thy1) recursor_base_name of
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   367
     None => (writeln "  [ No recursion operator ]";
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   368
	      [])
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   369
   | Some recursor_def => 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   370
      let
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   371
	(*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   372
	fun subst_rec (Const("op `",_) $ Free _ $ arg) = recursor_tm $ arg
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   373
	  | subst_rec tm = 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   374
	      let val (head, args) = strip_comb tm 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   375
	      in  list_comb (head, map subst_rec args)  end;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   376
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   377
	(*Each equation has the form 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   378
	  REC(coni(args)) = f_coni(args, REC(rec_arg), ...) 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   379
	  where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   380
	  constructor argument.*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   381
	fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) = 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   382
	  FOLogic.mk_Trueprop
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   383
	   (FOLogic.mk_eq
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   384
	    (recursor_tm $
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   385
	     (list_comb (Const (Sign.intern_const (sign_of thy1) name,T), 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   386
			 args)),
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   387
	     subst_rec (foldl betapply (recursor_case, args))));
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   388
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   389
	val recursor_trans = recursor_def RS def_Vrecursor RS trans;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   390
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   391
	(*Proves a single recursor equation.*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   392
	fun recursor_tacsf _ = 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   393
	  [rtac recursor_trans 1,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   394
	   simp_tac (rank_ss addsimps case_eqns) 1,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   395
	   IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)];
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   396
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   397
	fun prove_recursor_eqn arg =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   398
	    prove_goalw_cterm [] 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   399
	      (Ind_Syntax.traceIt "next recursor equation = "
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   400
		(cterm_of (sign_of thy1) (mk_recursor_eqn arg)))
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   401
	      recursor_tacsf
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   402
      in
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   403
	 map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   404
      end
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   405
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   406
  val constructors =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   407
      map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   408
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   409
  val free_iffs = con_iffs @ 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   410
    [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   411
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   412
  val free_SEs = Ind_Syntax.mk_free_SEs con_iffs @ Su.free_SEs;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   413
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   414
  val {elim, induct, mutual_induct, ...} = ind_result
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   415
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   416
  (*Typical theorems have the form ~con1=con2, con1=con2==>False,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   417
    con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   418
  fun mk_free s =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   419
      prove_goalw (theory_of_thm elim)   (*Don't use thy1: it will be stale*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   420
                  con_defs s
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   421
	(fn prems => [cut_facts_tac prems 1, 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   422
		      fast_tac (ZF_cs addSEs free_SEs) 1]);
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   423
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   424
  val simps = case_eqns @ recursor_eqns;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   425
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   426
  val dt_info =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   427
	{inductive = true,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   428
	 constructors = constructors,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   429
	 rec_rewrites = recursor_eqns,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   430
	 case_rewrites = case_eqns,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   431
	 induct = induct,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   432
	 mutual_induct = mutual_induct,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   433
	 exhaustion = elim};
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   434
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   435
  val con_info =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   436
        {big_rec_name = big_rec_name,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   437
	 constructors = constructors,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   438
            (*let primrec handle definition by cases*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   439
	 rec_rewrites = (case recursor_eqns of
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   440
			     [] => case_eqns | _ => recursor_eqns)};
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   441
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   442
  (*associate with each constructor the datatype name and rewrites*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   443
  val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   444
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   445
 in
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   446
  (*Updating theory components: simprules and datatype info*)
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   447
  (thy1 |> Theory.add_path big_rec_base_name
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   448
        |> PureThy.add_tthmss [(("simps", Attribute.tthms_of simps), 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   449
				[Simplifier.simp_add_global])] 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   450
        |> DatatypesData.put 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   451
	    (Symtab.update
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   452
	     ((big_rec_name, dt_info), DatatypesData.get thy1)) 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   453
        |> ConstructorsData.put
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   454
	     (foldr Symtab.update (con_pairs, ConstructorsData.get thy1))
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   455
	|> Theory.parent_path,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   456
   ind_result,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   457
   {con_defs = con_defs,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   458
    case_eqns = case_eqns,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   459
    recursor_eqns = recursor_eqns,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   460
    free_iffs = free_iffs,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   461
    free_SEs = free_SEs,
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   462
    mk_free = mk_free})
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   463
  end;
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   464
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   465
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   466
fun add_datatype (sdom, srec_tms, scon_ty_lists, 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   467
		  monos, type_intrs, type_elims) thy =
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   468
  let val sign = sign_of thy
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   469
      val rec_tms = map (readtm sign Ind_Syntax.iT) srec_tms
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   470
      val dom_sum = 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   471
          if sdom = "" then
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   472
	      Ind_Syntax.data_domain (#1 (dest_Const Fp.oper) <> "lfp") rec_tms
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   473
          else readtm sign Ind_Syntax.iT sdom
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   474
      and con_ty_lists	= Ind_Syntax.read_constructs sign scon_ty_lists
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   475
  in 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   476
      add_datatype_i (dom_sum, rec_tms, con_ty_lists, 
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   477
		      monos, type_intrs, type_elims) thy
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   478
  end		    
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   479
4f093e55beeb revised datatype definition package
paulson
parents:
diff changeset
   480
end;