bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
authorhaftmann
Wed Nov 25 11:16:57 2009 +0100 (2009-11-25)
changeset 339592afc55e8ed27
parent 33958 a57f4c9d0a19
child 33960 53993394ac19
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
src/HOL/Datatype.thy
src/HOL/Inductive.thy
src/HOL/Product_Type.thy
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Datatype.thy	Wed Nov 25 09:14:28 2009 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Wed Nov 25 11:16:57 2009 +0100
     1.3 @@ -8,9 +8,15 @@
     1.4  header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
     1.5  
     1.6  theory Datatype
     1.7 -imports Nat Product_Type
     1.8 +imports Product_Type Sum_Type Nat
     1.9 +uses
    1.10 +  ("Tools/Datatype/datatype_rep_proofs.ML")
    1.11 +  ("Tools/inductive_realizer.ML")
    1.12 +  ("Tools/Datatype/datatype_realizer.ML")
    1.13  begin
    1.14  
    1.15 +subsection {* The datatype universe *}
    1.16 +
    1.17  typedef (Node)
    1.18    ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}"
    1.19      --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*}
    1.20 @@ -513,75 +519,12 @@
    1.21  hide (open) type node item
    1.22  hide (open) const Push Node Atom Leaf Numb Lim Split Case
    1.23  
    1.24 -
    1.25 -section {* Datatypes *}
    1.26 -
    1.27 -subsection {* Representing sums *}
    1.28 -
    1.29 -rep_datatype (sum) Inl Inr
    1.30 -proof -
    1.31 -  fix P
    1.32 -  fix s :: "'a + 'b"
    1.33 -  assume x: "\<And>x\<Colon>'a. P (Inl x)" and y: "\<And>y\<Colon>'b. P (Inr y)"
    1.34 -  then show "P s" by (auto intro: sumE [of s])
    1.35 -qed simp_all
    1.36 -
    1.37 -lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)"
    1.38 -  by (rule ext) (simp split: sum.split)
    1.39 -
    1.40 -lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)"
    1.41 -  apply (rule_tac s = s in sumE)
    1.42 -   apply (erule ssubst)
    1.43 -   apply (rule sum.cases(1))
    1.44 -  apply (erule ssubst)
    1.45 -  apply (rule sum.cases(2))
    1.46 -  done
    1.47 -
    1.48 -lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t"
    1.49 -  -- {* Prevents simplification of @{text f} and @{text g}: much faster. *}
    1.50 -  by simp
    1.51 +use "Tools/Datatype/datatype_rep_proofs.ML"
    1.52  
    1.53 -lemma sum_case_inject:
    1.54 -  "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P"
    1.55 -proof -
    1.56 -  assume a: "sum_case f1 f2 = sum_case g1 g2"
    1.57 -  assume r: "f1 = g1 ==> f2 = g2 ==> P"
    1.58 -  show P
    1.59 -    apply (rule r)
    1.60 -     apply (rule ext)
    1.61 -     apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp)
    1.62 -    apply (rule ext)
    1.63 -    apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp)
    1.64 -    done
    1.65 -qed
    1.66 -
    1.67 -constdefs
    1.68 -  Suml :: "('a => 'c) => 'a + 'b => 'c"
    1.69 -  "Suml == (%f. sum_case f undefined)"
    1.70 -
    1.71 -  Sumr :: "('b => 'c) => 'a + 'b => 'c"
    1.72 -  "Sumr == sum_case undefined"
    1.73 +use "Tools/inductive_realizer.ML"
    1.74 +setup InductiveRealizer.setup
    1.75  
    1.76 -lemma [code]:
    1.77 -  "Suml f (Inl x) = f x"
    1.78 -  by (simp add: Suml_def)
    1.79 -
    1.80 -lemma [code]:
    1.81 -  "Sumr f (Inr x) = f x"
    1.82 -  by (simp add: Sumr_def)
    1.83 -
    1.84 -lemma Suml_inject: "Suml f = Suml g ==> f = g"
    1.85 -  by (unfold Suml_def) (erule sum_case_inject)
    1.86 -
    1.87 -lemma Sumr_inject: "Sumr f = Sumr g ==> f = g"
    1.88 -  by (unfold Sumr_def) (erule sum_case_inject)
    1.89 -
    1.90 -primrec Projl :: "'a + 'b => 'a"
    1.91 -where Projl_Inl: "Projl (Inl x) = x"
    1.92 -
    1.93 -primrec Projr :: "'a + 'b => 'b"
    1.94 -where Projr_Inr: "Projr (Inr x) = x"
    1.95 -
    1.96 -hide (open) const Suml Sumr Projl Projr
    1.97 +use "Tools/Datatype/datatype_realizer.ML"
    1.98 +setup DatatypeRealizer.setup
    1.99  
   1.100  end
     2.1 --- a/src/HOL/Inductive.thy	Wed Nov 25 09:14:28 2009 +0100
     2.2 +++ b/src/HOL/Inductive.thy	Wed Nov 25 11:16:57 2009 +0100
     2.3 @@ -5,16 +5,15 @@
     2.4  header {* Knaster-Tarski Fixpoint Theorem and inductive definitions *}
     2.5  
     2.6  theory Inductive 
     2.7 -imports Lattices Sum_Type
     2.8 +imports Complete_Lattice
     2.9  uses
    2.10    ("Tools/inductive.ML")
    2.11    "Tools/dseq.ML"
    2.12    ("Tools/inductive_codegen.ML")
    2.13 -  ("Tools/Datatype/datatype_aux.ML")
    2.14 -  ("Tools/Datatype/datatype_prop.ML")
    2.15 -  ("Tools/Datatype/datatype_rep_proofs.ML")
    2.16 +  "Tools/Datatype/datatype_aux.ML"
    2.17 +  "Tools/Datatype/datatype_prop.ML"
    2.18 +  "Tools/Datatype/datatype_case.ML"
    2.19    ("Tools/Datatype/datatype_abs_proofs.ML")
    2.20 -  ("Tools/Datatype/datatype_case.ML")
    2.21    ("Tools/Datatype/datatype.ML")
    2.22    ("Tools/old_primrec.ML")
    2.23    ("Tools/primrec.ML")
    2.24 @@ -282,11 +281,7 @@
    2.25  
    2.26  text {* Package setup. *}
    2.27  
    2.28 -use "Tools/Datatype/datatype_aux.ML"
    2.29 -use "Tools/Datatype/datatype_prop.ML"
    2.30 -use "Tools/Datatype/datatype_rep_proofs.ML"
    2.31  use "Tools/Datatype/datatype_abs_proofs.ML"
    2.32 -use "Tools/Datatype/datatype_case.ML"
    2.33  use "Tools/Datatype/datatype.ML"
    2.34  setup Datatype.setup
    2.35  
     3.1 --- a/src/HOL/Product_Type.thy	Wed Nov 25 09:14:28 2009 +0100
     3.2 +++ b/src/HOL/Product_Type.thy	Wed Nov 25 11:16:57 2009 +0100
     3.3 @@ -6,12 +6,10 @@
     3.4  header {* Cartesian products *}
     3.5  
     3.6  theory Product_Type
     3.7 -imports Inductive
     3.8 +imports Typedef Inductive Fun
     3.9  uses
    3.10    ("Tools/split_rule.ML")
    3.11    ("Tools/inductive_set.ML")
    3.12 -  ("Tools/inductive_realizer.ML")
    3.13 -  ("Tools/Datatype/datatype_realizer.ML")
    3.14  begin
    3.15  
    3.16  subsection {* @{typ bool} is a datatype *}
    3.17 @@ -1195,16 +1193,7 @@
    3.18  val unit_eq = thm "unit_eq";
    3.19  *}
    3.20  
    3.21 -
    3.22 -subsection {* Further inductive packages *}
    3.23 -
    3.24 -use "Tools/inductive_realizer.ML"
    3.25 -setup InductiveRealizer.setup
    3.26 -
    3.27  use "Tools/inductive_set.ML"
    3.28  setup Inductive_Set.setup
    3.29  
    3.30 -use "Tools/Datatype/datatype_realizer.ML"
    3.31 -setup DatatypeRealizer.setup
    3.32 -
    3.33  end
     4.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Wed Nov 25 09:14:28 2009 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Wed Nov 25 11:16:57 2009 +0100
     4.3 @@ -7,10 +7,9 @@
     4.4  signature DATATYPE =
     4.5  sig
     4.6    include DATATYPE_COMMON
     4.7 -  val add_datatype : config -> string list -> (string list * binding * mixfix *
     4.8 -    (binding * typ list * mixfix) list) list -> theory -> string list * theory
     4.9 -  val datatype_cmd : string list -> (string list * binding * mixfix *
    4.10 -    (binding * string list * mixfix) list) list -> theory -> theory
    4.11 +  val derive_datatype_props : config -> string list -> string list option
    4.12 +    -> descr list -> (string * sort) list -> thm -> thm list list -> thm list list
    4.13 +    -> theory -> string list * theory
    4.14    val rep_datatype : config -> (string list -> Proof.context -> Proof.context)
    4.15      -> string list option -> term list -> theory -> Proof.state
    4.16    val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
    4.17 @@ -30,6 +29,8 @@
    4.18      (term * term) list -> term * (term * (int * bool)) list
    4.19    val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
    4.20    val read_typ: theory -> string -> (string * sort) list -> typ * (string * sort) list
    4.21 +  val cert_typ: theory -> typ -> (string * sort) list -> typ * (string * sort) list
    4.22 +  val mk_case_names_induct: descr -> attribute
    4.23    val setup: theory -> theory
    4.24  end;
    4.25  
    4.26 @@ -442,89 +443,6 @@
    4.27  
    4.28  
    4.29  
    4.30 -(** definitional introduction of datatypes **)
    4.31 -
    4.32 -fun gen_add_datatype prep_typ config new_type_names dts thy =
    4.33 -  let
    4.34 -    val _ = Theory.requires thy "Datatype" "datatype definitions";
    4.35 -
    4.36 -    (* this theory is used just for parsing *)
    4.37 -    val tmp_thy = thy |>
    4.38 -      Theory.copy |>
    4.39 -      Sign.add_types (map (fn (tvs, tname, mx, _) =>
    4.40 -        (tname, length tvs, mx)) dts);
    4.41 -
    4.42 -    val (tyvars, _, _, _)::_ = dts;
    4.43 -    val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
    4.44 -      let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
    4.45 -      in
    4.46 -        (case duplicates (op =) tvs of
    4.47 -          [] =>
    4.48 -            if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
    4.49 -            else error ("Mutually recursive datatypes must have same type parameters")
    4.50 -        | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
    4.51 -            " : " ^ commas dups))
    4.52 -      end) dts);
    4.53 -    val dt_names = map fst new_dts;
    4.54 -
    4.55 -    val _ =
    4.56 -      (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
    4.57 -        [] => ()
    4.58 -      | dups => error ("Duplicate datatypes: " ^ commas dups));
    4.59 -
    4.60 -    fun prep_dt_spec ((tvs, tname, mx, constrs), tname') (dts', constr_syntax, sorts, i) =
    4.61 -      let
    4.62 -        fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
    4.63 -          let
    4.64 -            val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts';
    4.65 -            val _ =
    4.66 -              (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of
    4.67 -                [] => ()
    4.68 -              | vs => error ("Extra type variables on rhs: " ^ commas vs))
    4.69 -          in (constrs @ [(Sign.full_name_path tmp_thy tname'
    4.70 -                  (Binding.map_name (Syntax.const_name mx') cname),
    4.71 -                   map (dtyp_of_typ new_dts) cargs')],
    4.72 -              constr_syntax' @ [(cname, mx')], sorts'')
    4.73 -          end handle ERROR msg => cat_error msg
    4.74 -           ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
    4.75 -            " of datatype " ^ quote (Binding.str_of tname));
    4.76 -
    4.77 -        val (constrs', constr_syntax', sorts') =
    4.78 -          fold prep_constr constrs ([], [], sorts)
    4.79 -
    4.80 -      in
    4.81 -        case duplicates (op =) (map fst constrs') of
    4.82 -           [] =>
    4.83 -             (dts' @ [(i, (Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname),
    4.84 -                map DtTFree tvs, constrs'))],
    4.85 -              constr_syntax @ [constr_syntax'], sorts', i + 1)
    4.86 -         | dups => error ("Duplicate constructors " ^ commas dups ^
    4.87 -             " in datatype " ^ quote (Binding.str_of tname))
    4.88 -      end;
    4.89 -
    4.90 -    val (dts', constr_syntax, sorts', i) =
    4.91 -      fold prep_dt_spec (dts ~~ new_type_names) ([], [], [], 0);
    4.92 -    val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars));
    4.93 -    val dt_info = get_all thy;
    4.94 -    val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
    4.95 -    val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
    4.96 -      if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
    4.97 -      else raise exn;
    4.98 -
    4.99 -    val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
   4.100 -    val ((inject, distinct, induct), thy') = thy |>
   4.101 -      DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
   4.102 -        types_syntax constr_syntax (mk_case_names_induct (flat descr));
   4.103 -  in
   4.104 -    derive_datatype_props config dt_names (SOME new_type_names) descr sorts
   4.105 -      induct inject distinct thy'
   4.106 -  end;
   4.107 -
   4.108 -val add_datatype = gen_add_datatype cert_typ;
   4.109 -val datatype_cmd = snd ooo gen_add_datatype read_typ default_config;
   4.110 -
   4.111 -
   4.112 -
   4.113  (** package setup **)
   4.114  
   4.115  (* setup theory *)
   4.116 @@ -540,27 +458,9 @@
   4.117  
   4.118  structure P = OuterParse and K = OuterKeyword
   4.119  
   4.120 -fun prep_datatype_decls args =
   4.121 -  let
   4.122 -    val names = map
   4.123 -      (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
   4.124 -    val specs = map (fn ((((_, vs), t), mx), cons) =>
   4.125 -      (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
   4.126 -  in (names, specs) end;
   4.127 -
   4.128 -val parse_datatype_decl =
   4.129 -  (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
   4.130 -    (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
   4.131 -
   4.132 -val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;
   4.133 -
   4.134  in
   4.135  
   4.136  val _ =
   4.137 -  OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
   4.138 -    (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs)));
   4.139 -
   4.140 -val _ =
   4.141    OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal
   4.142      (Scan.option (P.$$$ "(" |-- Scan.repeat1 P.name --| P.$$$ ")") -- Scan.repeat1 P.term
   4.143        >> (fn (alt_names, ts) => Toplevel.print
     5.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Wed Nov 25 09:14:28 2009 +0100
     5.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Wed Nov 25 11:16:57 2009 +0100
     5.3 @@ -1,8 +1,7 @@
     5.4  (*  Title:      HOL/Tools/datatype_rep_proofs.ML
     5.5      Author:     Stefan Berghofer, TU Muenchen
     5.6  
     5.7 -Definitional introduction of datatypes
     5.8 -Proof of characteristic theorems:
     5.9 +Definitional introduction of datatypes with proof of characteristic theorems:
    5.10  
    5.11   - injectivity of constructors
    5.12   - distinctness of constructors
    5.13 @@ -12,52 +11,56 @@
    5.14  signature DATATYPE_REP_PROOFS =
    5.15  sig
    5.16    include DATATYPE_COMMON
    5.17 -  val representation_proofs : config -> info Symtab.table ->
    5.18 -    string list -> descr list -> (string * sort) list ->
    5.19 -      (binding * mixfix) list -> (binding * mixfix) list list -> attribute
    5.20 -        -> theory -> (thm list list * thm list list * thm) * theory
    5.21 +  val add_datatype : config -> string list -> (string list * binding * mixfix *
    5.22 +    (binding * typ list * mixfix) list) list -> theory -> string list * theory
    5.23 +  val datatype_cmd : string list -> (string list * binding * mixfix *
    5.24 +    (binding * string list * mixfix) list) list -> theory -> theory
    5.25  end;
    5.26  
    5.27  structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
    5.28  struct
    5.29  
    5.30 +(** auxiliary **)
    5.31 +
    5.32  open DatatypeAux;
    5.33  
    5.34  val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
    5.35  
    5.36  val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
    5.37  
    5.38 -
    5.39 -(** theory context references **)
    5.40 -
    5.41  fun exh_thm_of (dt_info : info Symtab.table) tname =
    5.42    #exhaust (the (Symtab.lookup dt_info tname));
    5.43  
    5.44 -(******************************************************************************)
    5.45 +val node_name = @{type_name "Datatype.node"};
    5.46 +val In0_name = @{const_name "Datatype.In0"};
    5.47 +val In1_name = @{const_name "Datatype.In1"};
    5.48 +val Scons_name = @{const_name "Datatype.Scons"};
    5.49 +val Leaf_name = @{const_name "Datatype.Leaf"};
    5.50 +val Numb_name = @{const_name "Datatype.Numb"};
    5.51 +val Lim_name = @{const_name "Datatype.Lim"};
    5.52 +val Suml_name = @{const_name "Sum_Type.Suml"};
    5.53 +val Sumr_name = @{const_name "Sum_Type.Sumr"};
    5.54 +
    5.55 +val In0_inject = @{thm In0_inject};
    5.56 +val In1_inject = @{thm In1_inject};
    5.57 +val Scons_inject = @{thm Scons_inject};
    5.58 +val Leaf_inject = @{thm Leaf_inject};
    5.59 +val In0_eq = @{thm In0_eq};
    5.60 +val In1_eq = @{thm In1_eq};
    5.61 +val In0_not_In1 = @{thm In0_not_In1};
    5.62 +val In1_not_In0 = @{thm In1_not_In0};
    5.63 +val Lim_inject = @{thm Lim_inject};
    5.64 +val Suml_inject = @{thm Suml_inject};
    5.65 +val Sumr_inject = @{thm Sumr_inject};
    5.66 +
    5.67 +
    5.68 +
    5.69 +(** proof of characteristic theorems **)
    5.70  
    5.71  fun representation_proofs (config : config) (dt_info : info Symtab.table)
    5.72        new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
    5.73    let
    5.74 -    val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
    5.75 -    val node_name = "Datatype.node";
    5.76 -    val In0_name = "Datatype.In0";
    5.77 -    val In1_name = "Datatype.In1";
    5.78 -    val Scons_name = "Datatype.Scons";
    5.79 -    val Leaf_name = "Datatype.Leaf";
    5.80 -    val Numb_name = "Datatype.Numb";
    5.81 -    val Lim_name = "Datatype.Lim";
    5.82 -    val Suml_name = "Datatype.Suml";
    5.83 -    val Sumr_name = "Datatype.Sumr";
    5.84 -
    5.85 -    val [In0_inject, In1_inject, Scons_inject, Leaf_inject,
    5.86 -         In0_eq, In1_eq, In0_not_In1, In1_not_In0,
    5.87 -         Lim_inject, Suml_inject, Sumr_inject] = map (PureThy.get_thm Datatype_thy)
    5.88 -          ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
    5.89 -           "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
    5.90 -           "Lim_inject", "Suml_inject", "Sumr_inject"];
    5.91 -
    5.92      val descr' = flat descr;
    5.93 -
    5.94      val big_name = space_implode "_" new_type_names;
    5.95      val thy1 = Sign.add_path big_name thy;
    5.96      val big_rec_name = big_name ^ "_rep_set";
    5.97 @@ -83,7 +86,7 @@
    5.98      val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
    5.99      val UnivT = HOLogic.mk_setT Univ_elT;
   5.100      val UnivT' = Univ_elT --> HOLogic.boolT;
   5.101 -    val Collect = Const ("Collect", UnivT' --> UnivT);
   5.102 +    val Collect = Const (@{const_name Collect}, UnivT' --> UnivT);
   5.103  
   5.104      val In0 = Const (In0_name, Univ_elT --> Univ_elT);
   5.105      val In1 = Const (In1_name, Univ_elT --> Univ_elT);
   5.106 @@ -100,9 +103,9 @@
   5.107                val Type (_, [T1, T2]) = T
   5.108            in
   5.109              if i <= n2 then
   5.110 -              Const ("Sum_Type.Inl", T1 --> T) $ (mk_inj' T1 n2 i)
   5.111 +              Const (@{const_name "Sum_Type.Inl"}, T1 --> T) $ (mk_inj' T1 n2 i)
   5.112              else
   5.113 -              Const ("Sum_Type.Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
   5.114 +              Const (@{const_name "Sum_Type.Inr"}, T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
   5.115            end
   5.116        in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs)
   5.117        end;
   5.118 @@ -629,4 +632,123 @@
   5.119      ((constr_inject', distinct_thms', dt_induct'), thy7)
   5.120    end;
   5.121  
   5.122 +
   5.123 +
   5.124 +(** definitional introduction of datatypes **)
   5.125 +
   5.126 +fun gen_add_datatype prep_typ config new_type_names dts thy =
   5.127 +  let
   5.128 +    val _ = Theory.requires thy "Datatype" "datatype definitions";
   5.129 +
   5.130 +    (* this theory is used just for parsing *)
   5.131 +    val tmp_thy = thy |>
   5.132 +      Theory.copy |>
   5.133 +      Sign.add_types (map (fn (tvs, tname, mx, _) =>
   5.134 +        (tname, length tvs, mx)) dts);
   5.135 +
   5.136 +    val (tyvars, _, _, _)::_ = dts;
   5.137 +    val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
   5.138 +      let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
   5.139 +      in
   5.140 +        (case duplicates (op =) tvs of
   5.141 +          [] =>
   5.142 +            if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
   5.143 +            else error ("Mutually recursive datatypes must have same type parameters")
   5.144 +        | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
   5.145 +            " : " ^ commas dups))
   5.146 +      end) dts);
   5.147 +    val dt_names = map fst new_dts;
   5.148 +
   5.149 +    val _ =
   5.150 +      (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
   5.151 +        [] => ()
   5.152 +      | dups => error ("Duplicate datatypes: " ^ commas dups));
   5.153 +
   5.154 +    fun prep_dt_spec (tvs, tname, mx, constrs) tname' (dts', constr_syntax, sorts, i) =
   5.155 +      let
   5.156 +        fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
   5.157 +          let
   5.158 +            val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts';
   5.159 +            val _ =
   5.160 +              (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of
   5.161 +                [] => ()
   5.162 +              | vs => error ("Extra type variables on rhs: " ^ commas vs))
   5.163 +          in (constrs @ [(Sign.full_name_path tmp_thy tname'
   5.164 +                  (Binding.map_name (Syntax.const_name mx') cname),
   5.165 +                   map (dtyp_of_typ new_dts) cargs')],
   5.166 +              constr_syntax' @ [(cname, mx')], sorts'')
   5.167 +          end handle ERROR msg => cat_error msg
   5.168 +           ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
   5.169 +            " of datatype " ^ quote (Binding.str_of tname));
   5.170 +
   5.171 +        val (constrs', constr_syntax', sorts') =
   5.172 +          fold prep_constr constrs ([], [], sorts)
   5.173 +
   5.174 +      in
   5.175 +        case duplicates (op =) (map fst constrs') of
   5.176 +           [] =>
   5.177 +             (dts' @ [(i, (Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname),
   5.178 +                map DtTFree tvs, constrs'))],
   5.179 +              constr_syntax @ [constr_syntax'], sorts', i + 1)
   5.180 +         | dups => error ("Duplicate constructors " ^ commas dups ^
   5.181 +             " in datatype " ^ quote (Binding.str_of tname))
   5.182 +      end;
   5.183 +
   5.184 +    val (dts', constr_syntax, sorts', i) =
   5.185 +      fold2 prep_dt_spec dts new_type_names ([], [], [], 0);
   5.186 +    val sorts = sorts' @ map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars);
   5.187 +    val dt_info = Datatype.get_all thy;
   5.188 +    val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
   5.189 +    val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
   5.190 +      if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
   5.191 +      else raise exn;
   5.192 +
   5.193 +    val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
   5.194 +
   5.195 +  in
   5.196 +    thy
   5.197 +    |> representation_proofs config dt_info new_type_names descr sorts
   5.198 +        types_syntax constr_syntax (Datatype.mk_case_names_induct (flat descr))
   5.199 +    |-> (fn (inject, distinct, induct) => Datatype.derive_datatype_props
   5.200 +        config dt_names (SOME new_type_names) descr sorts
   5.201 +        induct inject distinct)
   5.202 +  end;
   5.203 +
   5.204 +val add_datatype = gen_add_datatype Datatype.cert_typ;
   5.205 +val datatype_cmd = snd ooo gen_add_datatype Datatype.read_typ default_config;
   5.206 +
   5.207 +local
   5.208 +
   5.209 +structure P = OuterParse and K = OuterKeyword
   5.210 +
   5.211 +fun prep_datatype_decls args =
   5.212 +  let
   5.213 +    val names = map
   5.214 +      (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
   5.215 +    val specs = map (fn ((((_, vs), t), mx), cons) =>
   5.216 +      (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
   5.217 +  in (names, specs) end;
   5.218 +
   5.219 +val parse_datatype_decl =
   5.220 +  (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
   5.221 +    (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix)));
   5.222 +
   5.223 +val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls;
   5.224 +
   5.225 +in
   5.226 +
   5.227 +val _ =
   5.228 +  OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
   5.229 +    (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs)));
   5.230 +
   5.231  end;
   5.232 +
   5.233 +end;
   5.234 +
   5.235 +structure Datatype =
   5.236 +struct
   5.237 +
   5.238 +open Datatype;
   5.239 +open DatatypeRepProofs;
   5.240 +
   5.241 +end;