# HG changeset patch
# User wenzelm
# Date 952950464 -3600
# Node ID 258281c43deae7e870d0ef6a462cacb68ec8cec6
# Parent  8a87fa482baf675bad6ac6df532bb8dd8fafd30d
removed cases_of;
renamed cases_tac to case_tac; tuned to work with basic HOL as well;
add_cases_induct: proper case names;
adapted to new PureThy.add_thms etc.;

diff -r 8a87fa482baf -r 258281c43dea src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Mar 13 13:24:12 2000 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Mon Mar 13 13:27:44 2000 +0100
@@ -9,8 +9,8 @@
 signature BASIC_DATATYPE_PACKAGE =
 sig
   val induct_tac : string -> int -> tactic
-  val exhaust_tac : string -> int -> tactic
-  val cases_tac : string -> int -> tactic
+  val exhaust_tac : string -> int -> tactic		(* FIXME remove !? *)
+  val case_tac : string -> int -> tactic
   val distinct_simproc : simproc
 end;
 
@@ -71,7 +71,6 @@
   val constrs_of : theory -> string -> term list option
   val constrs_of_sg : Sign.sg -> string -> term list option
   val case_const_of : theory -> string -> term option
-  val cases_of: Sign.sg -> string -> thm
   val setup: (theory -> theory) list
 end;
 
@@ -130,9 +129,6 @@
 
 val constrs_of = constrs_of_sg o Theory.sign_of;
 
-val exhaustion_of = #exhaustion oo datatype_info_sg_err
-fun cases_of sg name = if name = HOLogic.boolN then case_split_thm else exhaustion_of sg name;
-
 fun case_const_of thy tname = (case datatype_info thy tname of
    Some {case_name, ...} => Some (Const (case_name, the (Sign.const_type
      (Theory.sign_of thy) case_name)))
@@ -191,21 +187,58 @@
   end;
 
 
-(* generic exhaustion tactic for datatypes *)
+(* generic case tactic for datatypes *)
 
-fun gen_exhaust_tac get_rule aterm i state =
-  let
-    val rule = get_rule (Thm.sign_of_thm state) (infer_tname state i aterm);
-    val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
-      (hd (Logic.strip_assums_hyp (hd (Thm.prems_of rule))));
-    val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)))
-  in res_inst_tac [(exh_vname, aterm)] rule i state end;
+fun case_tac aterm i state =
+  let val name = infer_tname state i aterm in
+    if name = HOLogic.boolN then res_inst_tac [("P", aterm)] case_split_thm i state
+    else
+      let
+        val {exhaustion, ...} = datatype_info_sg_err (Thm.sign_of_thm state) name;
+        val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
+          (hd (Logic.strip_assums_hyp (hd (prems_of exhaustion))));
+        val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)))
+      in res_inst_tac [(exh_vname, aterm)] exhaustion i state end
+  end;
 
-val exhaust_tac = gen_exhaust_tac exhaustion_of;
-val cases_tac = gen_exhaust_tac cases_of;
+val exhaust_tac = case_tac;
+
 
 
-(* add_cases_induct -- interface to induct method *)
+(** induct method setup **)
+
+(* case names *)
+
+local
+
+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 =
+  DatatypeProp.indexify_names (flat (map (dt_cases descr) (map #2 descr)));
+
+fun exhaust_cases descr i = dt_cases descr (the (assoc (descr, i)));
+
+in
+
+fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
+
+fun mk_case_names_exhausts descr new =
+  map (RuleCases.case_names o exhaust_cases descr o #1)
+    (filter (fn ((_, (name, _, _))) => name mem_string new) descr);
+
+end;
+
+
+(* add_cases_induct *)
 
 fun add_cases_induct infos =
   let
@@ -215,27 +248,10 @@
             (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),
-        [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;
+      (("", proj index (length descr) induction), [InductMethod.induct_type_global name]) ::
+      (("", exhaustion), [InductMethod.cases_type_global name]) :: ths;
+  in #1 o PureThy.add_thms (foldl add ([], infos)) end;
 
 
 
@@ -341,27 +357,29 @@
 
 (********************* axiomatic introduction of datatypes ********************)
 
-fun add_and_get_axioms label tnames ts thy =
-  foldr (fn ((tname, t), (thy', axs)) =>
+fun add_and_get_axioms_atts label tnames attss ts thy =
+  foldr (fn (((tname, atts), t), (thy', axs)) =>
     let
-      val thy'' = thy' |>
+      val (thy'', [ax]) = thy' |>
         Theory.add_path tname |>
-        PureThy.add_axioms_i [((label, t), [])];
-      val ax = PureThy.get_thm thy'' label
+        PureThy.add_axioms_i [((label, t), atts)];
     in (Theory.parent_path thy'', ax::axs)
-    end) (tnames ~~ ts, (thy, []));
+    end) (tnames ~~ attss ~~ ts, (thy, []));
+
+fun add_and_get_axioms label tnames =
+  add_and_get_axioms_atts label tnames (replicate (length tnames) []);
 
 fun add_and_get_axiomss label tnames tss thy =
   foldr (fn ((tname, ts), (thy', axss)) =>
     let
-      val thy'' = thy' |>
+      val (thy'', [axs]) = thy' |>
         Theory.add_path tname |>
         PureThy.add_axiomss_i [((label, ts), [])];
-      val axs = PureThy.get_thms thy'' label
     in (Theory.parent_path thy'', axs::axss)
     end) (tnames ~~ tss, (thy, []));
 
-fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy =
+fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
+    case_names_induct case_names_exhausts thy =
   let
     val descr' = flat descr;
     val recTs = get_rec_types descr' sorts;
@@ -465,21 +483,22 @@
     val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
     val size_axs = if no_size then [] else DatatypeProp.make_size new_type_names descr sorts thy2;
 
-    val (thy3, inject) = thy2 |>
+    val (thy3, (([induct], [rec_thms]), inject)) =
+      thy2 |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [])] |>
-      PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>
-      (if no_size then I else PureThy.add_axiomss_i [(("size", size_axs), [])]) |>
-      Theory.parent_path |>
+      PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [case_names_induct])] |>>>
+      PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>>
+      (if no_size then I else #1 o PureThy.add_axiomss_i [(("size", size_axs), [])]) |>>
+      Theory.parent_path |>>>
       add_and_get_axiomss "inject" new_type_names
         (DatatypeProp.make_injs descr sorts);
-    val induct = get_thm thy3 "induct";
-    val rec_thms = get_thms thy3 "recs";
     val size_thms = if no_size then [] else get_thms thy3 "size";
     val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
       (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
-    val (thy5, exhaustion) = add_and_get_axioms "exhaust" new_type_names
-      (DatatypeProp.make_casedists descr sorts) thy4;
+
+    val exhaust_ts = DatatypeProp.make_casedists descr sorts;
+    val (thy5, exhaustion) = add_and_get_axioms_atts "exhaust" new_type_names
+      (map Library.single case_names_exhausts) exhaust_ts thy4;
     val (thy6, case_thms) = add_and_get_axiomss "cases" new_type_names
       (DatatypeProp.make_cases new_type_names descr sorts thy5) thy5;
     val (split_ts, split_asm_ts) = ListPair.unzip
@@ -501,7 +520,7 @@
 
     val thy11 = thy10 |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      PureThy.add_thmss [(("simps", simps), [])] |>
+      (#1 o PureThy.add_thmss [(("simps", simps), [])]) |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       add_cases_induct dt_infos |>
       Theory.parent_path;
@@ -526,19 +545,20 @@
 
 (******************* definitional introduction of datatypes *******************)
 
-fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy =
+fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
+    case_names_induct case_names_exhausts thy =
   let
     val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
 
     val (thy2, inject, distinct, dist_rewrites, simproc_dists, induct) = thy |>
       DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
-        types_syntax constr_syntax;
+        types_syntax constr_syntax case_names_induct;
 
-    val (thy3, casedist_thms) =
-      DatatypeAbsProofs.prove_casedist_thms new_type_names descr sorts induct thy2;
+    val (thy3, casedist_thms) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
+      sorts induct case_names_exhausts thy2;
     val (thy4, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
       flat_names new_type_names descr sorts dt_info inject dist_rewrites dist_ss induct thy3;
-    val (thy6, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
+    val (thy6, (case_thms, case_names)) = DatatypeAbsProofs.prove_case_thms
       flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
     val (thy7, split_thms) = DatatypeAbsProofs.prove_split_thms new_type_names
       descr sorts inject dist_rewrites casedist_thms case_thms thy6;
@@ -557,7 +577,7 @@
 
     val thy11 = thy10 |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      PureThy.add_thmss [(("simps", simps), [])] |>
+      (#1 o PureThy.add_thmss [(("simps", simps), [])]) |>
       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
       add_cases_induct dt_infos |>
       Theory.parent_path;
@@ -602,7 +622,7 @@
           ((tname, map dest_TFree Ts) handle TERM _ => err t)
       | get_typ t = err t;
 
-    val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induction')));
+    val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induction')));
     val new_type_names = if_none alt_names (map fst dtnames);
 
     fun get_constr t = (case Logic.strip_assums_concl t of
@@ -624,13 +644,18 @@
     val sorts = add_term_tfrees (concl_of induction', []);
     val dt_info = get_datatypes thy1;
 
+    val case_names_induct = mk_case_names_induct descr;
+    val case_names_exhausts = mk_case_names_exhausts descr (map #1 dtnames);
+    
+
     val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
 
     val (thy2, casedist_thms) = thy1 |>
-      DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction;
+      DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction
+        case_names_exhausts;
     val (thy3, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
       false new_type_names [descr] sorts dt_info inject distinct dist_ss induction thy2;
-    val (thy4, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms false
+    val (thy4, (case_thms, case_names)) = DatatypeAbsProofs.prove_case_thms false
       new_type_names [descr] sorts reccomb_names rec_thms thy3;
     val (thy5, split_thms) = DatatypeAbsProofs.prove_split_thms
       new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
@@ -650,20 +675,20 @@
 
     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
 
-    val thy9 = thy8 |>
-      store_thmss "inject" new_type_names inject |>
-      store_thmss "distinct" new_type_names distinct |>
+    val (thy9, [induction']) = thy8 |>
+      (#1 o store_thmss "inject" new_type_names inject) |>
+      (#1 o store_thmss "distinct" new_type_names distinct) |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      PureThy.add_thms [(("induct", induction), [])] |>
-      PureThy.add_thmss [(("simps", simps), [])] |>
-      put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
-      add_cases_induct dt_infos |>
+      PureThy.add_thms [(("induct", induction), [case_names_induct])] |>>
+      (#1 o PureThy.add_thmss [(("simps", simps), [])]) |>>
+      put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>>
+      add_cases_induct dt_infos |>>
       Theory.parent_path;
 
+    (* FIXME use attributes *)
     val _ = store_clasimp thy9 ((claset_of thy9, simpset_of thy9)
       addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
       addIffs flat (inject @ distinct));
-
   in
     (thy9,
      {distinct = distinct,
@@ -672,7 +697,7 @@
       rec_thms = rec_thms,
       case_thms = case_thms,
       split_thms = split_thms,
-      induction = induction,
+      induction = induction',
       size = size_thms,
       simps = simps})
   end;
@@ -744,9 +769,13 @@
     val (descr, _) = unfold_datatypes sign dts' sorts dt_info dts' i;
     val _ = check_nonempty descr;
 
+    val descr' = flat descr;
+    val case_names_induct = mk_case_names_induct descr';
+    val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
   in
     (if (!quick_and_dirty) then add_datatype_axm else add_datatype_def)
-      flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy
+      flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
+      case_names_induct case_names_exhausts thy
   end;
 
 val add_datatype_i = gen_add_datatype cert_typ;