src/HOL/Tools/Datatype/datatype.ML
changeset 31781 861e675f01e6
parent 31775 2b04504fcb69
child 31783 cfbe9609ceb1
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 12:09:30 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 23 14:50:34 2009 +0200
     1.3 @@ -7,19 +7,15 @@
     1.4  signature DATATYPE =
     1.5  sig
     1.6    include DATATYPE_COMMON
     1.7 -  type rules = {distinct : thm list list,
     1.8 -    inject : thm list list,
     1.9 -    exhaustion : thm list,
    1.10 -    rec_thms : thm list,
    1.11 -    case_thms : thm list list,
    1.12 -    split_thms : (thm * thm) list,
    1.13 -    induction : thm,
    1.14 -    simps : thm list}
    1.15    val add_datatype : config -> string list -> (string list * binding * mixfix *
    1.16 -    (binding * typ list * mixfix) list) list -> theory -> rules * theory
    1.17 +    (binding * typ list * mixfix) list) list -> theory ->
    1.18 +     (string list * {inject : thm list list,
    1.19 +      rec_thms : thm list,
    1.20 +      case_thms : thm list list,
    1.21 +      induction : thm}) * theory
    1.22    val datatype_cmd : string list -> (string list * binding * mixfix *
    1.23      (binding * string list * mixfix) list) list -> theory -> theory
    1.24 -  val rep_datatype : config -> (rules -> Proof.context -> Proof.context)
    1.25 +  val rep_datatype : config -> (string list -> Proof.context -> Proof.context)
    1.26      -> string list option -> term list -> theory -> Proof.state
    1.27    val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
    1.28    val get_datatypes : theory -> info Symtab.table
    1.29 @@ -334,15 +330,6 @@
    1.30      case_cong = case_cong,
    1.31      weak_case_cong = weak_case_cong});
    1.32  
    1.33 -type rules = {distinct : thm list list,
    1.34 -  inject : thm list list,
    1.35 -  exhaustion : thm list,
    1.36 -  rec_thms : thm list,
    1.37 -  case_thms : thm list list,
    1.38 -  split_thms : (thm * thm) list,
    1.39 -  induction : thm,
    1.40 -  simps : thm list}
    1.41 -
    1.42  structure DatatypeInterpretation = InterpretationFun
    1.43    (type T = config * string list val eq: T * T -> bool = eq_snd op =);
    1.44  fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
    1.45 @@ -377,10 +364,11 @@
    1.46  
    1.47      val dt_infos = map
    1.48        (make_dt_info (SOME new_type_names) (flat descr) sorts induct reccomb_names rec_thms)
    1.49 -      ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
    1.50 +      ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_thms ~~
    1.51          casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    1.52  
    1.53      val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
    1.54 +    val dt_names = map fst dt_infos;
    1.55  
    1.56      val thy12 =
    1.57        thy10
    1.58 @@ -394,14 +382,10 @@
    1.59        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    1.60        |> DatatypeInterpretation.data (config, map fst dt_infos);
    1.61    in
    1.62 -    ({distinct = distinct,
    1.63 -      inject = inject,
    1.64 -      exhaustion = casedist_thms,
    1.65 +    ((dt_names, {inject = inject,
    1.66        rec_thms = rec_thms,
    1.67        case_thms = case_thms,
    1.68 -      split_thms = split_thms,
    1.69 -      induction = induct,
    1.70 -      simps = simps}, thy12)
    1.71 +      induction = induct}), thy12)
    1.72    end;
    1.73  
    1.74  
    1.75 @@ -457,6 +441,7 @@
    1.76          map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
    1.77  
    1.78      val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
    1.79 +    val dt_names = map fst dt_infos;
    1.80  
    1.81      val thy11 =
    1.82        thy10
    1.83 @@ -468,17 +453,8 @@
    1.84        |> Sign.parent_path
    1.85        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    1.86        |> snd
    1.87 -      |> DatatypeInterpretation.data (config, map fst dt_infos);
    1.88 -  in
    1.89 -    ({distinct = distinct,
    1.90 -      inject = inject,
    1.91 -      exhaustion = casedist_thms,
    1.92 -      rec_thms = rec_thms,
    1.93 -      case_thms = case_thms,
    1.94 -      split_thms = split_thms,
    1.95 -      induction = induct',
    1.96 -      simps = simps}, thy11)
    1.97 -  end;
    1.98 +      |> DatatypeInterpretation.data (config, dt_names);
    1.99 +  in (dt_names, thy11) end;
   1.100  
   1.101  fun gen_rep_datatype prep_term (config : config) after_qed alt_names raw_ts thy =
   1.102    let