# HG changeset patch
# User blanchet
# Date 1409581066 -7200
# Node ID 82db9ad610b935f608fa73b4bf62d1f8db081d88
# Parent  019c0211ed1f413211633e7c8385c223786b0c38
tuned structure inclusion

diff -r 019c0211ed1f -r 82db9ad610b9 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Fun.thy	Mon Sep 01 16:17:46 2014 +0200
@@ -585,7 +585,7 @@
   "f(x:=y)" == "CONST fun_upd f x y"
 
 (* Hint: to define the sum of two functions (or maps), use case_sum.
-         A nice infix syntax could be defined (in Datatype.thy or below) by
+         A nice infix syntax could be defined by
 notation
   case_sum  (infixr "'(+')"80)
 *)
diff -r 019c0211ed1f -r 82db9ad610b9 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -233,8 +233,7 @@
  ["finite_intvl_succ_class",
   "nibble"]
 
-val forbidden_consts =
- [@{const_name Pure.type}, @{const_name Datatype.dsum}, @{const_name Datatype.usum}]
+val forbidden_consts = [@{const_name Pure.type}]
 
 fun is_forbidden_theorem (s, th) =
   let val consts = Term.add_const_names (prop_of th) [] in
diff -r 019c0211ed1f -r 82db9ad610b9 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -100,9 +100,9 @@
     val (_,thy1) = 
     fold_map (fn ak => fn thy => 
           let val dt = ((Binding.name ak, [], NoSyn), [(Binding.name ak, [@{typ nat}], NoSyn)])
-              val (dt_names, thy1) = Datatype.add_datatype Datatype.default_config [dt] thy;
+              val (dt_names, thy1) = Datatype.add_datatype Datatype_Aux.default_config [dt] thy;
             
-              val injects = maps (#inject o Datatype.the_info thy1) dt_names;
+              val injects = maps (#inject o Datatype_Data.the_info thy1) dt_names;
               val ak_type = Type (Sign.intern_type thy1 ak,[])
               val ak_sign = Sign.intern_const thy1 ak 
               
diff -r 019c0211ed1f -r 82db9ad610b9 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -6,8 +6,8 @@
 
 signature NOMINAL_DATATYPE =
 sig
-  val nominal_datatype : Datatype.config -> Datatype.spec list -> theory -> theory
-  val nominal_datatype_cmd : Datatype.config -> Datatype.spec_cmd list -> theory -> theory
+  val nominal_datatype : Datatype_Aux.config -> Datatype.spec list -> theory -> theory
+  val nominal_datatype_cmd : Datatype_Aux.config -> Datatype.spec_cmd list -> theory -> theory
   type descr
   type nominal_datatype_info
   val get_nominal_datatypes : theory -> nominal_datatype_info Symtab.table
@@ -42,8 +42,8 @@
 (* theory data *)
 
 type descr =
-  (int * (string * Datatype.dtyp list *
-      (string * (Datatype.dtyp list * Datatype.dtyp) list) list)) list;
+  (int * (string * Datatype_Aux.dtyp list *
+      (string * (Datatype_Aux.dtyp list * Datatype_Aux.dtyp) list) list)) list;
 
 type nominal_datatype_info =
   {index : int,
@@ -201,8 +201,8 @@
 
     val (full_new_type_names',thy1) = Datatype.add_datatype config dts'' thy;
 
-    val {descr, induct, ...} = Datatype.the_info thy1 (hd full_new_type_names');
-    fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr (Datatype.DtRec i);
+    val {descr, induct, ...} = Datatype_Data.the_info thy1 (hd full_new_type_names');
+    fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr (Datatype_Aux.DtRec i);
 
     val big_name = space_implode "_" new_type_names;
 
@@ -467,13 +467,13 @@
           | (i, _) => SOME (Datatype_Aux.name_of_typ (nth_dtyp i))) descr)) ^ "_set";
     val _ = warning ("big_rep_name: " ^ big_rep_name);
 
-    fun strip_option (dtf as Datatype.DtType ("fun", [dt, Datatype.DtRec i])) =
+    fun strip_option (dtf as Datatype_Aux.DtType ("fun", [dt, Datatype_Aux.DtRec i])) =
           (case AList.lookup op = descr i of
              SOME (@{type_name noption}, _, [(_, [dt']), _]) =>
                apfst (cons dt) (strip_option dt')
            | _ => ([], dtf))
-      | strip_option (Datatype.DtType ("fun",
-            [dt, Datatype.DtType (@{type_name noption}, [dt'])])) =
+      | strip_option (Datatype_Aux.DtType ("fun",
+            [dt, Datatype_Aux.DtType (@{type_name noption}, [dt'])])) =
           apfst (cons dt) (strip_option dt')
       | strip_option dt = ([], dt);
 
@@ -499,7 +499,7 @@
               end
           in (j + 1, j' + length Ts,
             case dt'' of
-                Datatype.DtRec k => Logic.list_all (map (pair "x") Us,
+                Datatype_Aux.DtRec k => Logic.list_all (map (pair "x") Us,
                   HOLogic.mk_Trueprop (Free (nth rep_set_names k,
                     T --> HOLogic.boolT) $ free')) :: prems
               | _ => prems,
@@ -680,8 +680,8 @@
       (fn ((i, (@{type_name noption}, _, _)), p) => p
         | ((i, _), (ty_idxs, j)) => (ty_idxs @ [(i, j)], j + 1)) ([], 0) descr;
 
-    fun reindex (Datatype.DtType (s, dts)) = Datatype.DtType (s, map reindex dts)
-      | reindex (Datatype.DtRec i) = Datatype.DtRec (the (AList.lookup op = ty_idxs i))
+    fun reindex (Datatype_Aux.DtType (s, dts)) = Datatype_Aux.DtType (s, map reindex dts)
+      | reindex (Datatype_Aux.DtRec i) = Datatype_Aux.DtRec (the (AList.lookup op = ty_idxs i))
       | reindex dt = dt;
 
     fun strip_suffix i s = implode (List.take (raw_explode s, size s - i));  (* FIXME Symbol.explode (?) *)
@@ -717,7 +717,7 @@
       map (fn ((cname, cargs), idxs) => (cname, partition_cargs idxs cargs))
         (constrs ~~ idxss)))) (descr'' ~~ ndescr);
 
-    fun nth_dtyp' i = Datatype_Aux.typ_of_dtyp descr'' (Datatype.DtRec i);
+    fun nth_dtyp' i = Datatype_Aux.typ_of_dtyp descr'' (Datatype_Aux.DtRec i);
 
     val rep_names = map (fn s =>
       Sign.intern_const thy7 ("Rep_" ^ s)) new_type_names;
@@ -744,7 +744,7 @@
              xs @ x :: l_args,
              fold_rev mk_abs_fun xs
                (case dt of
-                  Datatype.DtRec k => if k < length new_type_names then
+                  Datatype_Aux.DtRec k => if k < length new_type_names then
                       Const (nth rep_names k, Datatype_Aux.typ_of_dtyp descr'' dt -->
                         Datatype_Aux.typ_of_dtyp descr dt) $ x
                     else error "nested recursion not (yet) supported"
@@ -1053,7 +1053,7 @@
             DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
                 (prems ~~ constr_defs))]);
 
-    val case_names_induct = Datatype.mk_case_names_induct descr'';
+    val case_names_induct = Datatype_Data.mk_case_names_induct descr'';
 
     (**** prove that new datatypes have finite support ****)
 
@@ -1446,7 +1446,7 @@
         val binders = maps fst frees';
         val atomTs = distinct op = (maps (map snd o fst) frees');
         val recs = map_filter
-          (fn ((_, Datatype.DtRec i), p) => SOME (i, p) | _ => NONE)
+          (fn ((_, Datatype_Aux.DtRec i), p) => SOME (i, p) | _ => NONE)
           (partition_cargs idxs cargs ~~ frees');
         val frees'' = map (fn i => "y" ^ string_of_int i) (1 upto length recs) ~~
           map (fn (i, _) => nth rec_result_Ts i) recs;
@@ -2053,6 +2053,6 @@
 val _ =
   Outer_Syntax.command @{command_spec "nominal_datatype"} "define nominal datatypes"
     (Parse.and_list1 Datatype.spec_cmd >>
-      (Toplevel.theory o nominal_datatype_cmd Datatype.default_config));
+      (Toplevel.theory o nominal_datatype_cmd Datatype_Aux.default_config));
 
 end
diff -r 019c0211ed1f -r 82db9ad610b9 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -173,8 +173,8 @@
 
 fun add_enum_type tyname tyname' thy =
   let
-    val {case_name, ...} = the (Datatype.get_info thy tyname');
-    val cs = map Const (the (Datatype.get_constrs thy tyname'));
+    val {case_name, ...} = the (Datatype_Data.get_info thy tyname');
+    val cs = map Const (the (Datatype_Data.get_constrs thy tyname'));
     val k = length cs;
     val T = Type (tyname', []);
     val p = Const (@{const_name pos}, T --> HOLogic.intT);
@@ -209,7 +209,7 @@
       (fn _ =>
          rtac @{thm subset_antisym} 1 THEN
          rtac @{thm subsetI} 1 THEN
-         Datatype_Aux.exh_tac (K (#exhaust (Datatype.the_info
+         Datatype_Aux.exh_tac (K (#exhaust (Datatype_Data.the_info
            (Proof_Context.theory_of lthy) tyname'))) 1 THEN
          ALLGOALS (asm_full_simp_tac lthy));
 
@@ -327,7 +327,7 @@
                  tyname)
               end
           | SOME (T as Type (tyname, []), cmap) =>
-              (case Datatype.get_constrs thy tyname of
+              (case Datatype_Data.get_constrs thy tyname of
                  NONE => assoc_ty_err thy T s "is not a datatype"
                | SOME cs =>
                    let val (prfx', _) = strip_prfx s
@@ -338,7 +338,7 @@
                      | SOME msg => assoc_ty_err thy T s msg
                    end)
           | SOME (T, _) => assoc_ty_err thy T s "is not a datatype");
-        val cs = map Const (the (Datatype.get_constrs thy' tyname));
+        val cs = map Const (the (Datatype_Data.get_constrs thy' tyname));
       in
         ((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
           fold Name.declare els ctxt),
@@ -888,7 +888,7 @@
                 handle Symtab.DUP _ => error ("SPARK type " ^ s ^
                   " already associated with type")) |>
         (fn thy' =>
-           case Datatype.get_constrs thy' tyname of
+           case Datatype_Data.get_constrs thy' tyname of
              NONE => (case get_record_info thy' T of
                NONE => thy'
              | SOME {fields, ...} =>
diff -r 019c0211ed1f -r 82db9ad610b9 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Statespace/state_fun.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -339,7 +339,7 @@
   | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
   | mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x);
 
-fun is_datatype thy = is_some o Datatype.get_info thy;
+fun is_datatype thy = is_some o Datatype_Data.get_info thy;
 
 fun mk_map @{type_name List.list} = Syntax.const @{const_name List.map}
   | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);
diff -r 019c0211ed1f -r 82db9ad610b9 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -9,7 +9,6 @@
 
 signature DATATYPE =
 sig
-  include DATATYPE_DATA
   val distinct_lemma: thm
   type spec =
     (binding * (string * sort) list * mixfix) *
@@ -19,8 +18,8 @@
     (binding * string list * mixfix) list
   val read_specs: spec_cmd list -> theory -> spec list * Proof.context
   val check_specs: spec list -> theory -> spec list * Proof.context
-  val add_datatype: config -> spec list -> theory -> string list * theory
-  val add_datatype_cmd: config -> spec_cmd list -> theory -> string list * theory
+  val add_datatype: Datatype_Aux.config -> spec list -> theory -> string list * theory
+  val add_datatype_cmd: Datatype_Aux.config -> spec_cmd list -> theory -> string list * theory
   val spec_cmd: spec_cmd parser
 end;
 
diff -r 019c0211ed1f -r 82db9ad610b9 src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -7,6 +7,7 @@
 signature DATATYPE_DATA =
 sig
   include DATATYPE_COMMON
+
   val get_all : theory -> info Symtab.table
   val get_info : theory -> string -> info option
   val the_info : theory -> string -> info
diff -r 019c0211ed1f -r 82db9ad610b9 src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -7,7 +7,7 @@
 
 signature DATATYPE_REALIZER =
 sig
-  val add_dt_realizers: Datatype.config -> string list -> theory -> theory
+  val add_dt_realizers: Datatype_Aux.config -> string list -> theory -> theory
   val setup: theory -> theory
 end;
 
@@ -25,7 +25,7 @@
 fun tname_of (Type (s, _)) = s
   | tname_of _ = "";
 
-fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Datatype.info) is thy =
+fun make_ind ({descr, rec_names, rec_rewrites, induct, ...} : Datatype_Aux.info) is thy =
   let
     val ctxt = Proof_Context.init_global thy;
     val cert = cterm_of thy;
@@ -84,7 +84,7 @@
         in (apfst (fold_rev (Logic.all o Free) frees) (mk_prems (map Free frees) recs), j + 1) end)
           constrs) (descr ~~ recTs) 1)));
 
-    fun mk_proj j [] t = t
+    fun mk_proj _ [] t = t
       | mk_proj j (i :: is) t =
           if null is then t
           else if (j: int) = i then HOLogic.mk_fst t
@@ -159,7 +159,8 @@
   in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
 
 
-fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype.info) thy =
+fun make_casedists ({index, descr, case_name, case_rewrites, exhaust, ...} : Datatype_Aux.info)
+    thy =
   let
     val ctxt = Proof_Context.init_global thy;
     val cert = cterm_of thy;
@@ -232,7 +233,7 @@
   else
     let
       val _ = Datatype_Aux.message config "Adding realizers for induction and case analysis ...";
-      val infos = map (Datatype.the_info thy) names;
+      val infos = map (Datatype_Data.the_info thy) names;
       val info :: _ = infos;
     in
       thy
@@ -240,6 +241,6 @@
       |> fold_rev make_casedists infos
     end;
 
-val setup = Datatype.interpretation add_dt_realizers;
+val setup = Datatype_Data.interpretation add_dt_realizers;
 
 end;
diff -r 019c0211ed1f -r 82db9ad610b9 src/HOL/Tools/TFL/casesplit.ML
--- a/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -24,7 +24,7 @@
                      Type(ty_str, _) => ty_str
                    | TFree(s,_)  => error ("Free type: " ^ s)
                    | TVar((s,i),_) => error ("Free variable: " ^ s)
-      val {induct, ...} = Datatype.the_info thy ty_str
+      val {induct, ...} = Datatype_Data.the_info thy ty_str
     in
       cases_thm_of_induct_thm induct
     end;
diff -r 019c0211ed1f -r 82db9ad610b9 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -435,7 +435,7 @@
        put_simpset HOL_basic_ss ctxt
           addsimps case_rewrites
           |> fold (Simplifier.add_cong o #case_cong_weak o snd)
-              (Symtab.dest (Datatype.get_all theory))
+              (Symtab.dest (Datatype_Data.get_all theory))
      val corollaries' = map (Simplifier.simplify case_simpset) corollaries
      val extract = Rules.CONTEXT_REWRITE_RULE
                      (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
diff -r 019c0211ed1f -r 82db9ad610b9 src/HOL/Tools/TFL/thry.ML
--- a/src/HOL/Tools/TFL/thry.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/TFL/thry.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -58,20 +58,20 @@
  *---------------------------------------------------------------------------*)
 
 fun match_info thy dtco =
-  case (Datatype.get_info thy dtco,
-         Datatype.get_constrs thy dtco) of
+  case (Datatype_Data.get_info thy dtco,
+         Datatype_Data.get_constrs thy dtco) of
       (SOME { case_name, ... }, SOME constructors) =>
         SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
     | _ => NONE;
 
-fun induct_info thy dtco = case Datatype.get_info thy dtco of
+fun induct_info thy dtco = case Datatype_Data.get_info thy dtco of
         NONE => NONE
       | SOME {nchotomy, ...} =>
           SOME {nchotomy = nchotomy,
-                constructors = (map Const o the o Datatype.get_constrs thy) dtco};
+                constructors = (map Const o the o Datatype_Data.get_constrs thy) dtco};
 
 fun extract_info thy =
- let val infos = map snd (Symtab.dest (Datatype.get_all thy))
+ let val infos = map snd (Symtab.dest (Datatype_Data.get_all thy))
  in {case_congs = map (mk_meta_eq o #case_cong) infos,
      case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos}
  end;
diff -r 019c0211ed1f -r 82db9ad610b9 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Mon Sep 01 16:17:46 2014 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon Sep 01 16:17:46 2014 +0200
@@ -313,10 +313,10 @@
       ||> Extraction.add_typeof_eqns_i ty_eqs
       ||> Extraction.add_realizes_eqns_i rlz_eqs;
     val dt_names = these some_dt_names;
-    val case_thms = map (#case_rewrites o Datatype.the_info thy2) dt_names;
+    val case_thms = map (#case_rewrites o Datatype_Data.the_info thy2) dt_names;
     val rec_thms =
       if null dt_names then []
-      else #rec_rewrites (Datatype.the_info thy2 (hd dt_names));
+      else #rec_rewrites (Datatype_Data.the_info thy2 (hd dt_names));
     val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
       HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms);
     val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>