author haftmann Wed Nov 25 11:16:57 2009 +0100 (2009-11-25) changeset 33959 2afc55e8ed27 parent 33958 a57f4c9d0a19 child 33960 53993394ac19
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
 src/HOL/Datatype.thy file | annotate | diff | revisions src/HOL/Inductive.thy file | annotate | diff | revisions src/HOL/Product_Type.thy file | annotate | diff | revisions src/HOL/Tools/Datatype/datatype.ML file | annotate | diff | revisions src/HOL/Tools/Datatype/datatype_rep_proofs.ML file | annotate | diff | revisions
```     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.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.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;
```