# HG changeset patch
# User haftmann
# Date 1254077905 -7200
# Node ID a5fcc7960681926aeb157ebaf5426231968dc483
# Parent  fc32e67717493da6e8d2e16c0aa66a89aacb41e3
emerging common infrastructure for datatype and rep_datatype

diff -r fc32e6771749 -r a5fcc7960681 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 20:43:47 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Sep 27 20:58:25 2009 +0200
@@ -268,37 +268,6 @@
 
 end;
 
-(* note rules and interpretations *)
-
-fun add_rules simps case_thms rec_thms 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 inject), [iff_add]),
-    ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
-    ((Binding.empty, weak_case_congs), [cong_att])]
-  #> snd;
-
-fun add_cases_induct infos inducts thy =
-  let
-    fun named_rules (name, {index, exhaust, ...}: info) =
-      [((Binding.empty, nth inducts index), [Induct.induct_type name]),
-       ((Binding.empty, exhaust), [Induct.cases_type name])];
-    fun unnamed_rule i =
-      ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
-  in
-    thy |> PureThy.add_thms
-      (maps named_rules infos @
-        map unnamed_rule (length infos upto length inducts - 1)) |> snd
-    |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
-  end;
-
-structure DatatypeInterpretation = InterpretationFun
-  (type T = config * string list val eq: T * T -> bool = eq_snd op =);
-fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
-
 (* translation rules for case *)
 
 fun make_case ctxt = DatatypeCase.make_case
@@ -345,23 +314,45 @@
     in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
 
 
-(** declare existing type as datatype **)
+(** abstract theory extensions relative to a datatype characterisation **)
+
+structure DatatypeInterpretation = InterpretationFun
+  (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
+                  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 inject), [iff_add]),
+    ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
+    ((Binding.empty, weak_case_congs), [cong_att])]
+  #> snd;
 
-fun prove_rep_datatype (config : config) dt_names alt_names descr sorts raw_induct raw_inject half_distinct thy1 =
+fun add_cases_induct infos inducts thy =
   let
-    val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
+    fun named_rules (name, {index, exhaust, ...}: info) =
+      [((Binding.empty, nth inducts index), [Induct.induct_type name]),
+       ((Binding.empty, exhaust), [Induct.cases_type name])];
+    fun unnamed_rule i =
+      ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
+  in
+    thy |> PureThy.add_thms
+      (maps named_rules infos @
+        map unnamed_rule (length infos upto length inducts - 1)) |> snd
+    |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
+  end;
+
+fun derive_datatype_props config dt_names alt_names descr sorts induct inject distinct thy2 =
+  let
     val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
+    val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
     val (case_names_induct, case_names_exhausts) =
       (mk_case_names_induct descr, mk_case_names_exhausts descr dt_names);
-    val (((inject, distinct), [induct]), thy2) =
-      thy1
-      |> store_thmss "inject" new_type_names raw_inject
-      ||>> store_thmss "distinct" new_type_names raw_distinct
-      ||> Sign.add_path (space_implode "_" new_type_names)
-      ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [case_names_induct])];
+    val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
 
-    val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
-    val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
     val (casedist_thms, thy3) = thy2 |>
       DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
         case_names_exhausts;
@@ -397,7 +388,24 @@
     |> pair dt_names
   end;
 
-fun gen_rep_datatype prep_term (config : config) after_qed alt_names raw_ts thy =
+
+(** declare existing type as datatype **)
+
+fun prove_rep_datatype config dt_names alt_names descr sorts raw_induct raw_inject half_distinct thy1 =
+  let
+    val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
+    val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
+    val (case_names_induct, case_names_exhausts) =
+      (mk_case_names_induct descr, mk_case_names_exhausts descr dt_names);
+    val (((inject, distinct), [induct]), thy2) =
+      thy1
+      |> store_thmss "inject" new_type_names raw_inject
+      ||>> store_thmss "distinct" new_type_names raw_distinct
+      ||> Sign.add_path (space_implode "_" new_type_names)
+      ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [case_names_induct])];
+  in derive_datatype_props config dt_names alt_names descr sorts induct inject distinct thy2 end;
+
+fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
   let
     fun constr_of_term (Const (c, T)) = (c, T)
       | constr_of_term t =
@@ -468,7 +476,7 @@
 
 (** definitional introduction of datatypes **)
 
-fun add_datatype_def (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
+fun add_datatype_def config new_type_names descr sorts types_syntax constr_syntax dt_info
     case_names_induct case_names_exhausts thy =
   let
     val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
@@ -515,7 +523,7 @@
       |> DatatypeInterpretation.data (config, map fst dt_infos);
   in (dt_names, thy12) end;
 
-fun gen_add_datatype prep_typ (config : config) new_type_names dts thy =
+fun gen_add_datatype prep_typ config new_type_names dts thy =
   let
     val _ = Theory.requires thy "Datatype" "datatype definitions";
 
@@ -582,7 +590,7 @@
     val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
   in
     add_datatype_def
-      (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
+      config new_type_names descr sorts types_syntax constr_syntax dt_info
       case_names_induct case_names_exhausts thy
   end;