# HG changeset patch
# User wenzelm
# Date 952647379 -3600
# Node ID 0255394a05dac3f1fd1a72a0a485bb9e15ebd1c7
# Parent  4b39358f9810fdbbea1a8f98e9afbb2b3b06d48b
add_cases_induct: produce proper case names;

diff -r 4b39358f9810 -r 0255394a05da src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Fri Mar 10 01:13:37 2000 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Fri Mar 10 01:16:19 2000 +0100
@@ -164,13 +164,13 @@
 
 (*Warn if the (induction) variable occurs Free among the premises, which
   usually signals a mistake.  But calls the tactic either way!*)
-fun occs_in_prems tacf vars = 
+fun occs_in_prems tacf vars =
   SUBGOAL (fn (Bi, i) =>
-	   (if  exists (fn Free (a, _) => a mem vars)
-	              (foldr add_term_frees (#2 (strip_context Bi), []))
-	     then warning "Induction variable occurs also among premises!"
-	     else ();
-	    tacf i));
+           (if  exists (fn Free (a, _) => a mem vars)
+                      (foldr add_term_frees (#2 (strip_context Bi), []))
+             then warning "Induction variable occurs also among premises!"
+             else ();
+            tacf i));
 
 (* generic induction tactic for datatypes *)
 
@@ -205,7 +205,7 @@
 val cases_tac = gen_exhaust_tac cases_of;
 
 
-(* add_cases_induct *)
+(* add_cases_induct -- interface to induct method *)
 
 fun add_cases_induct infos =
   let
@@ -214,12 +214,31 @@
           (if i + 1 < n then (fn th => th RS conjunct1) else I)
             (Library.funpow i (fn th => th RS conjunct2) thm)
           |> Drule.standard;
+
+    fun dt_recs (DtTFree _) = []
+      | dt_recs (DtType (_, dts)) = flat (map dt_recs dts)
+      | dt_recs (DtRec i) = [i];
+
+    fun dt_cases (descr: descr) (_, args, constrs) =
+      let
+        fun the_bname i = Sign.base_name (#1 (the (assoc (descr, i))));
+        val bnames = map the_bname (distinct (flat (map dt_recs args)));
+      in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
+
+    fun induct_cases descr =
+      Term.variantlist (flat (map (dt_cases descr) (map #2 descr)), []);
+
+    fun exhaust_cases descr i = dt_cases descr (the (assoc (descr, i)));
+
     fun add (ths, (name, {index, descr, induction, exhaustion, ...}: datatype_info)) =
-      (("", proj index (length descr) induction), [InductMethod.induct_type_global name]) ::
-       (("", exhaustion), [InductMethod.cases_type_global name]) :: ths;
+      (("", proj index (length descr) induction),
+        [RuleCases.case_names (induct_cases descr), InductMethod.induct_type_global name]) ::
+      (("", exhaustion), [RuleCases.case_names (exhaust_cases descr index),
+        InductMethod.cases_type_global name]) :: ths;
   in PureThy.add_thms (foldl add ([], infos)) end;
 
 
+
 (**** simplification procedure for showing distinctness of constructors ****)
 
 fun stripT (i, Type ("fun", [_, T])) = stripT (i + 1, T)
@@ -472,7 +491,7 @@
       (DatatypeProp.make_nchotomys descr sorts) thy8;
     val (thy10, case_congs) = add_and_get_axioms "case_cong" new_type_names
       (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
-    
+
     val dt_infos = map (make_dt_info descr' induct reccomb_names' rec_thms)
       ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
         exhaustion ~~ replicate (length (hd descr)) QuickAndDirty ~~ inject ~~
@@ -709,7 +728,7 @@
         val (constrs', constr_syntax', sorts') =
           foldl prep_constr (([], [], sorts), constrs)
 
-      in 
+      in
         case duplicates (map fst constrs') of
            [] =>
              (dts' @ [(i, (Sign.full_name sign (Syntax.type_name tname mx),