# HG changeset patch
# User haftmann
# Date 1254126021 -7200
# Node ID 9072201cd69d7fce69477ae52b4837cf0ed80042
# Parent  866cebde3fcaf8ee5fe2f7ea8a48e721cd6142fa
avoid compound fields in datatype info record

diff -r 866cebde3fca -r 9072201cd69d src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 28 09:47:32 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 28 10:20:21 2009 +0200
@@ -245,7 +245,7 @@
     val (full_new_type_names',thy1) =
       Datatype.add_datatype config new_type_names' dts'' thy;
 
-    val {descr, inducts = (_, induct), ...} =
+    val {descr, induct, ...} =
       Datatype.the_info thy1 (hd full_new_type_names');
     fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
 
diff -r 866cebde3fca -r 9072201cd69d src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 28 09:47:32 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 28 10:20:21 2009 +0200
@@ -218,26 +218,28 @@
 
 (* arrange data entries *)
 
-fun make_dt_info alt_names descr sorts inducts reccomb_names rec_thms
-    ((((((((((i, (_, (tname, _, _))), case_name), case_thms),
-      exhaust_thm), distinct_thm), inject), splits), nchotomy), case_cong), weak_case_cong) =
+fun make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites
+    ((((((((((i, (_, (tname, _, _))), case_name), case_rewrites),
+      exhaust), distinct), inject), (split, split_asm)), nchotomy), case_cong), weak_case_cong) =
   (tname,
    {index = i,
     alt_names = alt_names,
     descr = descr,
     sorts = sorts,
     inject = inject,
-    distinct = distinct_thm,
+    distinct = distinct,
+    induct = induct,
     inducts = inducts,
-    exhaust = exhaust_thm,
+    exhaust = exhaust,
     nchotomy = nchotomy,
-    rec_names = reccomb_names,
-    rec_rewrites = rec_thms,
+    rec_names = rec_names,
+    rec_rewrites = rec_rewrites,
     case_name = case_name,
-    case_rewrites = case_thms,
+    case_rewrites = case_rewrites,
     case_cong = case_cong,
     weak_case_cong = weak_case_cong,
-    splits = splits});
+    split = split,
+    split_asm = split_asm});
 
 (* case names *)
 
@@ -320,12 +322,12 @@
   (type T = config * string list val eq: T * T -> bool = eq_snd op =);
 fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
 
-fun add_rules simps case_thms rec_thms inject distinct
+fun add_rules simps case_rewrites rec_rewrites inject distinct
                   weak_case_congs cong_att =
   PureThy.add_thmss [((Binding.name "simps", simps), []),
-    ((Binding.empty, flat case_thms @
-          flat distinct @ rec_thms), [Simplifier.simp_add]),
-    ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
+    ((Binding.empty, flat case_rewrites @
+          flat distinct @ rec_rewrites), [Simplifier.simp_add]),
+    ((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]),
     ((Binding.empty, flat inject), [iff_add]),
     ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
     ((Binding.empty, weak_case_congs), [cong_att])]
@@ -357,29 +359,29 @@
     val (casedist_thms, thy3) = thy2 |>
       DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
         case_names_exhausts;
-    val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
+    val ((rec_names, rec_rewrites), thy4) = DatatypeAbsProofs.prove_primrec_thms
       config new_type_names [descr] sorts (get_all thy3) inject distinct
       (Simplifier.theory_context thy3 dist_ss) induct thy3;
-    val ((case_thms, case_names), thy5) = DatatypeAbsProofs.prove_case_thms
-      config new_type_names [descr] sorts reccomb_names rec_thms thy4;
+    val ((case_rewrites, case_names), thy5) = DatatypeAbsProofs.prove_case_thms
+      config new_type_names [descr] sorts rec_names rec_rewrites thy4;
     val (split_thms, thy6) = DatatypeAbsProofs.prove_split_thms
-      config new_type_names [descr] sorts inject distinct casedist_thms case_thms thy5;
+      config new_type_names [descr] sorts inject distinct casedist_thms case_rewrites thy5;
     val (nchotomys, thy7) = DatatypeAbsProofs.prove_nchotomys config new_type_names
       [descr] sorts casedist_thms thy6;
     val (case_congs, thy8) = DatatypeAbsProofs.prove_case_congs new_type_names
-      [descr] sorts nchotomys case_thms thy7;
+      [descr] sorts nchotomys case_rewrites thy7;
     val (weak_case_congs, thy9) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
       [descr] sorts thy8;
 
-    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
-    val dt_infos = map (make_dt_info alt_names descr sorts (inducts, induct) reccomb_names rec_thms)
-      ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
+    val simps = flat (distinct @ inject @ case_rewrites) @ rec_rewrites;
+    val dt_infos = map (make_dt_info alt_names descr sorts induct inducts rec_names rec_rewrites)
+      ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_rewrites ~~ casedist_thms ~~
         map FewConstrs distinct ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
     val dt_names = map fst dt_infos;
   in
     thy9
     |> add_case_tr' case_names
-    |> add_rules simps case_thms rec_thms inject distinct weak_case_congs (Simplifier.attrib (op addcongs))
+    |> add_rules simps case_rewrites rec_rewrites inject distinct weak_case_congs (Simplifier.attrib (op addcongs))
     |> register dt_infos
     |> add_cases_induct dt_infos inducts
     |> Sign.parent_path
@@ -492,33 +494,33 @@
 
     val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
       sorts induct case_names_exhausts thy2;
-    val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
+    val ((rec_names, rec_rewrites), thy4) = DatatypeAbsProofs.prove_primrec_thms
       config new_type_names descr sorts dt_info inject dist_rewrites
       (Simplifier.theory_context thy3 dist_ss) induct thy3;
-    val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
-      config new_type_names descr sorts reccomb_names rec_thms thy4;
+    val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
+      config new_type_names descr sorts rec_names rec_rewrites thy4;
     val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms config new_type_names
-      descr sorts inject dist_rewrites casedist_thms case_thms thy6;
+      descr sorts inject dist_rewrites casedist_thms case_rewrites thy6;
     val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys config new_type_names
       descr sorts casedist_thms thy7;
     val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
-      descr sorts nchotomys case_thms thy8;
+      descr sorts nchotomys case_rewrites thy8;
     val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
       descr sorts thy9;
 
     val dt_infos = map
-      (make_dt_info (SOME new_type_names) (flat descr) sorts (inducts, induct) reccomb_names rec_thms)
-      ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_thms ~~
+      (make_dt_info (SOME new_type_names) (flat descr) sorts induct inducts rec_names rec_rewrites)
+      ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_rewrites ~~
         casedist_thms ~~ simproc_dists ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
 
-    val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
+    val simps = flat (distinct @ inject @ case_rewrites) @ rec_rewrites;
     val dt_names = map fst dt_infos;
 
     val thy12 =
       thy10
       |> add_case_tr' case_names
       |> Sign.add_path (space_implode "_" new_type_names)
-      |> add_rules simps case_thms rec_thms inject distinct
+      |> add_rules simps case_rewrites rec_rewrites inject distinct
           weak_case_congs (Simplifier.attrib (op addcongs))
       |> register dt_infos
       |> add_cases_induct dt_infos inducts
diff -r 866cebde3fca -r 9072201cd69d src/HOL/Tools/Datatype/datatype_aux.ML
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 28 09:47:32 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Mon Sep 28 10:20:21 2009 +0200
@@ -193,7 +193,8 @@
    sorts : (string * sort) list,
    inject : thm list,
    distinct : simproc_dist,
-   inducts : thm list * thm,
+   induct : thm,
+   inducts : thm list,
    exhaust : thm,
    nchotomy : thm,
    rec_names : string list,
@@ -202,7 +203,8 @@
    case_rewrites : thm list,
    case_cong : thm,
    weak_case_cong : thm,
-   splits : thm * thm};
+   split : thm,
+   split_asm: thm};
 
 fun mk_Free s T i = Free (s ^ (string_of_int i), T);
 
diff -r 866cebde3fca -r 9072201cd69d src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Sep 28 09:47:32 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Sep 28 10:20:21 2009 +0200
@@ -38,7 +38,7 @@
 
 fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
 
-fun make_ind sorts ({descr, rec_names, rec_rewrites, inducts = (_, induct), ...} : info) is thy =
+fun make_ind sorts ({descr, rec_names, rec_rewrites, induct, ...} : info) is thy =
   let
     val recTs = get_rec_types descr sorts;
     val pnames = if length descr = 1 then ["P"]
diff -r 866cebde3fca -r 9072201cd69d src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Mon Sep 28 09:47:32 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Mon Sep 28 10:20:21 2009 +0200
@@ -389,7 +389,7 @@
     fun prove_iso_thms (ds, (inj_thms, elem_thms)) =
       let
         val (_, (tname, _, _)) = hd ds;
-        val induct = (snd o #inducts o the o Symtab.lookup dt_info) tname;
+        val induct = (#induct o the o Symtab.lookup dt_info) tname;
 
         fun mk_ind_concl (i, _) =
           let
diff -r 866cebde3fca -r 9072201cd69d src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Mon Sep 28 09:47:32 2009 +0200
+++ b/src/HOL/Tools/Function/size.ML	Mon Sep 28 10:20:21 2009 +0200
@@ -59,7 +59,7 @@
 
 fun prove_size_thms (info : info) new_type_names thy =
   let
-    val {descr, alt_names, sorts, rec_names, rec_rewrites, inducts = (_, induct), ...} = info;
+    val {descr, alt_names, sorts, rec_names, rec_rewrites, induct, ...} = info;
     val l = length new_type_names;
     val alt_names' = (case alt_names of
       NONE => replicate l NONE | SOME names => map SOME names);
diff -r 866cebde3fca -r 9072201cd69d src/HOL/Tools/TFL/casesplit.ML
--- a/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 28 09:47:32 2009 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 28 10:20:21 2009 +0200
@@ -96,7 +96,7 @@
                    | TVar((s,i),_) => error ("Free variable: " ^ s)
       val dt = Datatype.the_info thy ty_str
     in
-      cases_thm_of_induct_thm (snd (#inducts dt))
+      cases_thm_of_induct_thm (#induct dt)
     end;
 
 (*
diff -r 866cebde3fca -r 9072201cd69d src/HOL/Tools/old_primrec.ML
--- a/src/HOL/Tools/old_primrec.ML	Mon Sep 28 09:47:32 2009 +0200
+++ b/src/HOL/Tools/old_primrec.ML	Mon Sep 28 10:20:21 2009 +0200
@@ -230,7 +230,7 @@
               (tname, dt)::(find_dts dt_info tnames' tnames)
             else find_dts dt_info tnames' tnames);
 
-fun prepare_induct ({descr, inducts = (_, induct), ...}: info) rec_eqns =
+fun prepare_induct ({descr, induct, ...}: info) rec_eqns =
   let
     fun constrs_of (_, (_, _, cs)) =
       map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs;