# HG changeset patch
# User wenzelm
# Date 952950252 -3600
# Node ID 8a87fa482baf675bad6ac6df532bb8dd8fafd30d
# Parent  51a040fd2200f7b1695814ec53ff43161ab4bfd7
adapted to new PureThy.add_thms etc.;
proper handling of case names;

diff -r 51a040fd2200 -r 8a87fa482baf src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Mon Mar 13 13:22:31 2000 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Mar 13 13:24:12 2000 +0100
@@ -20,14 +20,14 @@
 sig
   val prove_casedist_thms : string list -> (int * (string * DatatypeAux.dtyp list *
     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-      thm -> theory -> theory * thm list
+      thm -> theory attribute list -> theory -> theory * thm list
   val prove_primrec_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
       DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
         simpset -> thm -> theory -> theory * string list * thm list
   val prove_case_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-      string list -> thm list -> theory -> theory * string list * thm list list
+      string list -> thm list -> theory -> theory * (thm list list * string list)
   val prove_split_thms : string list -> (int * (string * DatatypeAux.dtyp list *
     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
       thm list list -> thm list list -> thm list -> thm list list -> theory ->
@@ -43,7 +43,7 @@
       thm list -> thm list list -> theory -> theory * thm list
 end;
 
-structure DatatypeAbsProofs : DATATYPE_ABS_PROOFS =
+structure DatatypeAbsProofs: DATATYPE_ABS_PROOFS =
 struct
 
 open DatatypeAux;
@@ -54,7 +54,7 @@
 
 (************************ case distinction theorems ***************************)
 
-fun prove_casedist_thms new_type_names descr sorts induct thy =
+fun prove_casedist_thms new_type_names descr sorts induct case_names_exhausts thy =
   let
     val _ = message "Proving case distinction theorems ...";
 
@@ -85,10 +85,8 @@
 
     val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~
       (DatatypeProp.make_casedists descr sorts) ~~ newTs)
+  in thy |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms end;
 
-  in
-    (store_thms "exhaust" new_type_names casedist_thms thy, casedist_thms)
-  end;
 
 (*************************** primrec combinators ******************************)
 
@@ -256,7 +254,7 @@
       (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
         (reccomb_names ~~ recTs ~~ rec_result_Ts);
 
-    val thy2 = thy1 |>
+    val (thy2, reccomb_defs) = thy1 |>
       Theory.add_consts_i (map (fn ((name, T), T') =>
         (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
           (reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
@@ -264,10 +262,9 @@
         ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
            Const ("Eps", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
              HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set))))))
-               (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) |>
+               (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) |>>
       parent_path flat_names;
 
-    val reccomb_defs = map ((get_def thy2) o Sign.base_name) reccomb_names;
 
     (* prove characteristic equations for primrec combinators *)
 
@@ -284,7 +281,7 @@
 
   in
     (thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
-             PureThy.add_thmss [(("recs", rec_thms), [])] |>
+             (#1 o PureThy.add_thmss [(("recs", rec_thms), [])]) |>
              Theory.parent_path,
      reccomb_names, rec_thms)
   end;
@@ -342,10 +339,10 @@
             Logic.mk_equals (list_comb (Const (name, caseT), fns1),
               list_comb (reccomb, (flat (take (i, case_dummy_fns))) @
                 fns2 @ (flat (drop (i + 1, case_dummy_fns))) )));
-          val thy' = thy |>
+          val (thy', [def_thm]) = thy |>
             Theory.add_consts_i [decl] |> (PureThy.add_defs_i o map Thm.no_attributes) [def];
 
-        in (defs @ [get_def thy' (Sign.base_name name)], thy')
+        in (defs @ [def_thm], thy')
         end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
           (take (length newTs, reccomb_names)));
 
@@ -358,9 +355,7 @@
       (DatatypeProp.make_case_trrules new_type_names descr) |>
       parent_path flat_names;
 
-  in
-    (store_thmss "cases" new_type_names case_thms thy3, case_names, case_thms)
-  end;
+  in thy3 |> store_thmss "cases" new_type_names case_thms |> apsnd (rpair case_names) end;
 
 
 (******************************* case splitting *******************************)
@@ -395,9 +390,8 @@
     val (split_thms, split_asm_thms) = ListPair.unzip split_thm_pairs
 
   in
-    (thy |> store_thms "split" new_type_names split_thms |>
-            store_thms "split_asm" new_type_names split_asm_thms,
-     split_thm_pairs)
+    thy |> store_thms "split" new_type_names split_thms |>>>
+      store_thms "split_asm" new_type_names split_asm_thms |> apsnd ListPair.zip
   end;
 
 (******************************* size functions *******************************)
@@ -442,17 +436,16 @@
     val fs = flat (map (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr');
     val fTs = map fastype_of fs;
 
-    val thy' = thy1 |>
+    val (thy', size_def_thms) = thy1 |>
       Theory.add_consts_i (map (fn (s, T) =>
         (Sign.base_name s, T --> HOLogic.natT, NoSyn))
           (drop (length (hd descr), size_names ~~ recTs))) |>
       (PureThy.add_defs_i o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) =>
         (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
           list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs))))
-            (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |>
+            (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |>>
       parent_path flat_names;
 
-    val size_def_thms = map (get_thm thy') def_names;
     val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
 
     val size_thms = map (fn t => prove_goalw_cterm rewrites
@@ -461,7 +454,7 @@
 
   in
     (thy' |> Theory.add_path big_name |>
-             PureThy.add_thmss [(("size", size_thms), [])] |>
+             (#1 o PureThy.add_thmss [(("size", size_thms), [])]) |>
              Theory.parent_path,
      size_thms)
   end;
@@ -488,9 +481,7 @@
     val nchotomys =
       map prove_nchotomy (DatatypeProp.make_nchotomys descr sorts ~~ casedist_thms)
 
-  in
-    (store_thms "nchotomy" new_type_names nchotomys thy, nchotomys)
-  end;
+  in thy |> store_thms "nchotomy" new_type_names nchotomys end;
 
 fun prove_case_congs new_type_names descr sorts nchotomys case_thms thy =
   let
@@ -515,8 +506,6 @@
     val case_congs = map prove_case_cong (DatatypeProp.make_case_congs
       new_type_names descr sorts thy ~~ nchotomys ~~ case_thms)
 
-  in
-    (store_thms "case_cong" new_type_names case_congs thy, case_congs)
-  end;
+  in thy |> store_thms "case_cong" new_type_names case_congs end;
 
 end;
diff -r 51a040fd2200 -r 8a87fa482baf src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Mar 13 13:22:31 2000 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Mar 13 13:24:12 2000 +0100
@@ -17,8 +17,8 @@
   val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
     string list -> (int * (string * DatatypeAux.dtyp list *
       (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
-        (string * mixfix) list -> (string * mixfix) list list -> theory ->
-          theory * thm list list * thm list list * thm list list *
+        (string * mixfix) list -> (string * mixfix) list list -> theory attribute
+          -> theory -> theory * thm list list * thm list list * thm list list *
             DatatypeAux.simproc_dist list * thm
 end;
 
@@ -42,7 +42,7 @@
 (******************************************************************************)
 
 fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
-      new_type_names descr sorts types_syntax constr_syntax thy =
+      new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
   let
     val Datatype_thy = theory "Datatype";
     val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node";
@@ -231,12 +231,11 @@
         val def_name = (Sign.base_name cname) ^ "_def";
         val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
           (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
-        val thy' = thy |>
+        val (thy', [def_thm]) = thy |>
           Theory.add_consts_i [(cname', constrT, mx)] |>
           (PureThy.add_defs_i o map Thm.no_attributes) [(def_name, def)];
 
-      in (thy', defs @ [get_thm thy' def_name], eqns @ [eqn], i + 1)
-      end;
+      in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
 
     (* constructor definitions for datatype *)
 
@@ -382,8 +381,7 @@
         val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
           equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $
             list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos);
-        val thy' = (PureThy.add_defs_i o map Thm.no_attributes) defs thy;
-        val def_thms = map (get_thm thy') (map fst defs);
+        val (thy', def_thms) = (PureThy.add_defs_i o map Thm.no_attributes) defs thy;
 
         (* prove characteristic equations *)
 
@@ -580,8 +578,8 @@
       ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
 
     val thy6 = thy5 |> parent_path flat_names |>
-      store_thmss "inject" new_type_names constr_inject |>
-      store_thmss "distinct" new_type_names distinct_thms;
+      (#1 o store_thmss "inject" new_type_names constr_inject) |>
+      (#1 o store_thmss "distinct" new_type_names distinct_thms);
 
     (*************************** induction theorem ****************************)
 
@@ -638,12 +636,12 @@
               rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
                 (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
 
-    val thy7 = thy6 |>
+    val (thy7, [dt_induct']) = thy6 |>
       Theory.add_path big_name |>
-      PureThy.add_thms [(("induct", dt_induct), [])] |>
+      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
       Theory.parent_path;
 
-  in (thy7, constr_inject, distinct_thms, dist_rewrites, simproc_dists, dt_induct)
+  in (thy7, constr_inject, distinct_thms, dist_rewrites, simproc_dists, dt_induct')
   end;
 
 end;