# HG changeset patch # User haftmann # Date 1259144217 -3600 # Node ID 2afc55e8ed27ce483cfe3813c8e6958df388a883 # Parent a57f4c9d0a193989907f9c631b52c657cef40c0a bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references) diff -r a57f4c9d0a19 -r 2afc55e8ed27 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Wed Nov 25 09:14:28 2009 +0100 +++ b/src/HOL/Datatype.thy Wed Nov 25 11:16:57 2009 +0100 @@ -8,9 +8,15 @@ header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *} theory Datatype -imports Nat Product_Type +imports Product_Type Sum_Type Nat +uses + ("Tools/Datatype/datatype_rep_proofs.ML") + ("Tools/inductive_realizer.ML") + ("Tools/Datatype/datatype_realizer.ML") begin +subsection {* The datatype universe *} + typedef (Node) ('a,'b) node = "{p. EX f x k. p = (f::nat=>'b+nat, x::'a+nat) & f k = Inr 0}" --{*it is a subtype of @{text "(nat=>'b+nat) * ('a+nat)"}*} @@ -513,75 +519,12 @@ hide (open) type node item hide (open) const Push Node Atom Leaf Numb Lim Split Case - -section {* Datatypes *} - -subsection {* Representing sums *} - -rep_datatype (sum) Inl Inr -proof - - fix P - fix s :: "'a + 'b" - assume x: "\x\'a. P (Inl x)" and y: "\y\'b. P (Inr y)" - then show "P s" by (auto intro: sumE [of s]) -qed simp_all - -lemma sum_case_KK[simp]: "sum_case (%x. a) (%x. a) = (%x. a)" - by (rule ext) (simp split: sum.split) - -lemma surjective_sum: "sum_case (%x::'a. f (Inl x)) (%y::'b. f (Inr y)) s = f(s)" - apply (rule_tac s = s in sumE) - apply (erule ssubst) - apply (rule sum.cases(1)) - apply (erule ssubst) - apply (rule sum.cases(2)) - done - -lemma sum_case_weak_cong: "s = t ==> sum_case f g s = sum_case f g t" - -- {* Prevents simplification of @{text f} and @{text g}: much faster. *} - by simp +use "Tools/Datatype/datatype_rep_proofs.ML" -lemma sum_case_inject: - "sum_case f1 f2 = sum_case g1 g2 ==> (f1 = g1 ==> f2 = g2 ==> P) ==> P" -proof - - assume a: "sum_case f1 f2 = sum_case g1 g2" - assume r: "f1 = g1 ==> f2 = g2 ==> P" - show P - apply (rule r) - apply (rule ext) - apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp) - apply (rule ext) - apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp) - done -qed - -constdefs - Suml :: "('a => 'c) => 'a + 'b => 'c" - "Suml == (%f. sum_case f undefined)" - - Sumr :: "('b => 'c) => 'a + 'b => 'c" - "Sumr == sum_case undefined" +use "Tools/inductive_realizer.ML" +setup InductiveRealizer.setup -lemma [code]: - "Suml f (Inl x) = f x" - by (simp add: Suml_def) - -lemma [code]: - "Sumr f (Inr x) = f x" - by (simp add: Sumr_def) - -lemma Suml_inject: "Suml f = Suml g ==> f = g" - by (unfold Suml_def) (erule sum_case_inject) - -lemma Sumr_inject: "Sumr f = Sumr g ==> f = g" - by (unfold Sumr_def) (erule sum_case_inject) - -primrec Projl :: "'a + 'b => 'a" -where Projl_Inl: "Projl (Inl x) = x" - -primrec Projr :: "'a + 'b => 'b" -where Projr_Inr: "Projr (Inr x) = x" - -hide (open) const Suml Sumr Projl Projr +use "Tools/Datatype/datatype_realizer.ML" +setup DatatypeRealizer.setup end diff -r a57f4c9d0a19 -r 2afc55e8ed27 src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Wed Nov 25 09:14:28 2009 +0100 +++ b/src/HOL/Inductive.thy Wed Nov 25 11:16:57 2009 +0100 @@ -5,16 +5,15 @@ header {* Knaster-Tarski Fixpoint Theorem and inductive definitions *} theory Inductive -imports Lattices Sum_Type +imports Complete_Lattice uses ("Tools/inductive.ML") "Tools/dseq.ML" ("Tools/inductive_codegen.ML") - ("Tools/Datatype/datatype_aux.ML") - ("Tools/Datatype/datatype_prop.ML") - ("Tools/Datatype/datatype_rep_proofs.ML") + "Tools/Datatype/datatype_aux.ML" + "Tools/Datatype/datatype_prop.ML" + "Tools/Datatype/datatype_case.ML" ("Tools/Datatype/datatype_abs_proofs.ML") - ("Tools/Datatype/datatype_case.ML") ("Tools/Datatype/datatype.ML") ("Tools/old_primrec.ML") ("Tools/primrec.ML") @@ -282,11 +281,7 @@ text {* Package setup. *} -use "Tools/Datatype/datatype_aux.ML" -use "Tools/Datatype/datatype_prop.ML" -use "Tools/Datatype/datatype_rep_proofs.ML" use "Tools/Datatype/datatype_abs_proofs.ML" -use "Tools/Datatype/datatype_case.ML" use "Tools/Datatype/datatype.ML" setup Datatype.setup diff -r a57f4c9d0a19 -r 2afc55e8ed27 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Wed Nov 25 09:14:28 2009 +0100 +++ b/src/HOL/Product_Type.thy Wed Nov 25 11:16:57 2009 +0100 @@ -6,12 +6,10 @@ header {* Cartesian products *} theory Product_Type -imports Inductive +imports Typedef Inductive Fun uses ("Tools/split_rule.ML") ("Tools/inductive_set.ML") - ("Tools/inductive_realizer.ML") - ("Tools/Datatype/datatype_realizer.ML") begin subsection {* @{typ bool} is a datatype *} @@ -1195,16 +1193,7 @@ val unit_eq = thm "unit_eq"; *} - -subsection {* Further inductive packages *} - -use "Tools/inductive_realizer.ML" -setup InductiveRealizer.setup - use "Tools/inductive_set.ML" setup Inductive_Set.setup -use "Tools/Datatype/datatype_realizer.ML" -setup DatatypeRealizer.setup - end diff -r a57f4c9d0a19 -r 2afc55e8ed27 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Wed Nov 25 09:14:28 2009 +0100 +++ b/src/HOL/Tools/Datatype/datatype.ML Wed Nov 25 11:16:57 2009 +0100 @@ -7,10 +7,9 @@ signature DATATYPE = sig include DATATYPE_COMMON - val add_datatype : config -> string list -> (string list * binding * mixfix * - (binding * typ list * mixfix) list) list -> theory -> string list * theory - val datatype_cmd : string list -> (string list * binding * mixfix * - (binding * string list * mixfix) list) list -> theory -> theory + val derive_datatype_props : config -> string list -> string list option + -> descr list -> (string * sort) list -> thm -> thm list list -> thm list list + -> theory -> string list * theory val rep_datatype : config -> (string list -> Proof.context -> Proof.context) -> string list option -> term list -> theory -> Proof.state val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state @@ -30,6 +29,8 @@ (term * term) list -> term * (term * (int * bool)) list val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option val read_typ: theory -> string -> (string * sort) list -> typ * (string * sort) list + val cert_typ: theory -> typ -> (string * sort) list -> typ * (string * sort) list + val mk_case_names_induct: descr -> attribute val setup: theory -> theory end; @@ -442,89 +443,6 @@ -(** definitional introduction of datatypes **) - -fun gen_add_datatype prep_typ config new_type_names dts thy = - let - val _ = Theory.requires thy "Datatype" "datatype definitions"; - - (* this theory is used just for parsing *) - val tmp_thy = thy |> - Theory.copy |> - Sign.add_types (map (fn (tvs, tname, mx, _) => - (tname, length tvs, mx)) dts); - - val (tyvars, _, _, _)::_ = dts; - val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) => - let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname) - in - (case duplicates (op =) tvs of - [] => - if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx)) - else error ("Mutually recursive datatypes must have same type parameters") - | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^ - " : " ^ commas dups)) - end) dts); - val dt_names = map fst new_dts; - - val _ = - (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of - [] => () - | dups => error ("Duplicate datatypes: " ^ commas dups)); - - fun prep_dt_spec ((tvs, tname, mx, constrs), tname') (dts', constr_syntax, sorts, i) = - let - fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') = - let - val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts'; - val _ = - (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of - [] => () - | vs => error ("Extra type variables on rhs: " ^ commas vs)) - in (constrs @ [(Sign.full_name_path tmp_thy tname' - (Binding.map_name (Syntax.const_name mx') cname), - map (dtyp_of_typ new_dts) cargs')], - constr_syntax' @ [(cname, mx')], sorts'') - end handle ERROR msg => cat_error msg - ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^ - " of datatype " ^ quote (Binding.str_of tname)); - - val (constrs', constr_syntax', sorts') = - fold prep_constr constrs ([], [], sorts) - - in - case duplicates (op =) (map fst constrs') of - [] => - (dts' @ [(i, (Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname), - map DtTFree tvs, constrs'))], - constr_syntax @ [constr_syntax'], sorts', i + 1) - | dups => error ("Duplicate constructors " ^ commas dups ^ - " in datatype " ^ quote (Binding.str_of tname)) - end; - - val (dts', constr_syntax, sorts', i) = - fold prep_dt_spec (dts ~~ new_type_names) ([], [], [], 0); - val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars)); - val dt_info = get_all thy; - val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i; - val _ = check_nonempty descr handle (exn as Datatype_Empty s) => - if #strict config then error ("Nonemptiness check failed for datatype " ^ s) - else raise exn; - - val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names); - val ((inject, distinct, induct), thy') = thy |> - DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts - types_syntax constr_syntax (mk_case_names_induct (flat descr)); - in - derive_datatype_props config dt_names (SOME new_type_names) descr sorts - induct inject distinct thy' - end; - -val add_datatype = gen_add_datatype cert_typ; -val datatype_cmd = snd ooo gen_add_datatype read_typ default_config; - - - (** package setup **) (* setup theory *) @@ -540,27 +458,9 @@ structure P = OuterParse and K = OuterKeyword -fun prep_datatype_decls args = - let - val names = map - (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args; - val specs = map (fn ((((_, vs), t), mx), cons) => - (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args; - in (names, specs) end; - -val parse_datatype_decl = - (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix -- - (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix))); - -val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls; - in val _ = - OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl - (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs))); - -val _ = OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_goal (Scan.option (P.$$$ "(" |-- Scan.repeat1 P.name --| P.$$$ ")") -- Scan.repeat1 P.term >> (fn (alt_names, ts) => Toplevel.print diff -r a57f4c9d0a19 -r 2afc55e8ed27 src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Wed Nov 25 09:14:28 2009 +0100 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Wed Nov 25 11:16:57 2009 +0100 @@ -1,8 +1,7 @@ (* Title: HOL/Tools/datatype_rep_proofs.ML Author: Stefan Berghofer, TU Muenchen -Definitional introduction of datatypes -Proof of characteristic theorems: +Definitional introduction of datatypes with proof of characteristic theorems: - injectivity of constructors - distinctness of constructors @@ -12,52 +11,56 @@ signature DATATYPE_REP_PROOFS = sig include DATATYPE_COMMON - val representation_proofs : config -> info Symtab.table -> - string list -> descr list -> (string * sort) list -> - (binding * mixfix) list -> (binding * mixfix) list list -> attribute - -> theory -> (thm list list * thm list list * thm) * theory + val add_datatype : config -> string list -> (string list * binding * mixfix * + (binding * typ list * mixfix) list) list -> theory -> string list * theory + val datatype_cmd : string list -> (string list * binding * mixfix * + (binding * string list * mixfix) list) list -> theory -> theory end; structure DatatypeRepProofs : DATATYPE_REP_PROOFS = struct +(** auxiliary **) + open DatatypeAux; val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma); val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq]; - -(** theory context references **) - fun exh_thm_of (dt_info : info Symtab.table) tname = #exhaust (the (Symtab.lookup dt_info tname)); -(******************************************************************************) +val node_name = @{type_name "Datatype.node"}; +val In0_name = @{const_name "Datatype.In0"}; +val In1_name = @{const_name "Datatype.In1"}; +val Scons_name = @{const_name "Datatype.Scons"}; +val Leaf_name = @{const_name "Datatype.Leaf"}; +val Numb_name = @{const_name "Datatype.Numb"}; +val Lim_name = @{const_name "Datatype.Lim"}; +val Suml_name = @{const_name "Sum_Type.Suml"}; +val Sumr_name = @{const_name "Sum_Type.Sumr"}; + +val In0_inject = @{thm In0_inject}; +val In1_inject = @{thm In1_inject}; +val Scons_inject = @{thm Scons_inject}; +val Leaf_inject = @{thm Leaf_inject}; +val In0_eq = @{thm In0_eq}; +val In1_eq = @{thm In1_eq}; +val In0_not_In1 = @{thm In0_not_In1}; +val In1_not_In0 = @{thm In1_not_In0}; +val Lim_inject = @{thm Lim_inject}; +val Suml_inject = @{thm Suml_inject}; +val Sumr_inject = @{thm Sumr_inject}; + + + +(** proof of characteristic theorems **) fun representation_proofs (config : config) (dt_info : info Symtab.table) new_type_names descr sorts types_syntax constr_syntax case_names_induct thy = let - val Datatype_thy = ThyInfo.the_theory "Datatype" thy; - val node_name = "Datatype.node"; - val In0_name = "Datatype.In0"; - val In1_name = "Datatype.In1"; - val Scons_name = "Datatype.Scons"; - val Leaf_name = "Datatype.Leaf"; - val Numb_name = "Datatype.Numb"; - val Lim_name = "Datatype.Lim"; - val Suml_name = "Datatype.Suml"; - val Sumr_name = "Datatype.Sumr"; - - val [In0_inject, In1_inject, Scons_inject, Leaf_inject, - In0_eq, In1_eq, In0_not_In1, In1_not_In0, - Lim_inject, Suml_inject, Sumr_inject] = map (PureThy.get_thm Datatype_thy) - ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", - "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", - "Lim_inject", "Suml_inject", "Sumr_inject"]; - val descr' = flat descr; - val big_name = space_implode "_" new_type_names; val thy1 = Sign.add_path big_name thy; val big_rec_name = big_name ^ "_rep_set"; @@ -83,7 +86,7 @@ val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT])); val UnivT = HOLogic.mk_setT Univ_elT; val UnivT' = Univ_elT --> HOLogic.boolT; - val Collect = Const ("Collect", UnivT' --> UnivT); + val Collect = Const (@{const_name Collect}, UnivT' --> UnivT); val In0 = Const (In0_name, Univ_elT --> Univ_elT); val In1 = Const (In1_name, Univ_elT --> Univ_elT); @@ -100,9 +103,9 @@ val Type (_, [T1, T2]) = T in if i <= n2 then - Const ("Sum_Type.Inl", T1 --> T) $ (mk_inj' T1 n2 i) + Const (@{const_name "Sum_Type.Inl"}, T1 --> T) $ (mk_inj' T1 n2 i) else - Const ("Sum_Type.Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2)) + Const (@{const_name "Sum_Type.Inr"}, T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2)) end in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs) end; @@ -629,4 +632,123 @@ ((constr_inject', distinct_thms', dt_induct'), thy7) end; + + +(** definitional introduction of datatypes **) + +fun gen_add_datatype prep_typ config new_type_names dts thy = + let + val _ = Theory.requires thy "Datatype" "datatype definitions"; + + (* this theory is used just for parsing *) + val tmp_thy = thy |> + Theory.copy |> + Sign.add_types (map (fn (tvs, tname, mx, _) => + (tname, length tvs, mx)) dts); + + val (tyvars, _, _, _)::_ = dts; + val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) => + let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname) + in + (case duplicates (op =) tvs of + [] => + if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx)) + else error ("Mutually recursive datatypes must have same type parameters") + | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^ + " : " ^ commas dups)) + end) dts); + val dt_names = map fst new_dts; + + val _ = + (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of + [] => () + | dups => error ("Duplicate datatypes: " ^ commas dups)); + + fun prep_dt_spec (tvs, tname, mx, constrs) tname' (dts', constr_syntax, sorts, i) = + let + fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') = + let + val (cargs', sorts'') = fold_map (prep_typ tmp_thy) cargs sorts'; + val _ = + (case subtract (op =) tvs (fold (curry OldTerm.add_typ_tfree_names) cargs' []) of + [] => () + | vs => error ("Extra type variables on rhs: " ^ commas vs)) + in (constrs @ [(Sign.full_name_path tmp_thy tname' + (Binding.map_name (Syntax.const_name mx') cname), + map (dtyp_of_typ new_dts) cargs')], + constr_syntax' @ [(cname, mx')], sorts'') + end handle ERROR msg => cat_error msg + ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^ + " of datatype " ^ quote (Binding.str_of tname)); + + val (constrs', constr_syntax', sorts') = + fold prep_constr constrs ([], [], sorts) + + in + case duplicates (op =) (map fst constrs') of + [] => + (dts' @ [(i, (Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname), + map DtTFree tvs, constrs'))], + constr_syntax @ [constr_syntax'], sorts', i + 1) + | dups => error ("Duplicate constructors " ^ commas dups ^ + " in datatype " ^ quote (Binding.str_of tname)) + end; + + val (dts', constr_syntax, sorts', i) = + fold2 prep_dt_spec dts new_type_names ([], [], [], 0); + val sorts = sorts' @ map (rpair (Sign.defaultS tmp_thy)) (subtract (op =) (map fst sorts') tyvars); + val dt_info = Datatype.get_all thy; + val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i; + val _ = check_nonempty descr handle (exn as Datatype_Empty s) => + if #strict config then error ("Nonemptiness check failed for datatype " ^ s) + else raise exn; + + val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names); + + in + thy + |> representation_proofs config dt_info new_type_names descr sorts + types_syntax constr_syntax (Datatype.mk_case_names_induct (flat descr)) + |-> (fn (inject, distinct, induct) => Datatype.derive_datatype_props + config dt_names (SOME new_type_names) descr sorts + induct inject distinct) + end; + +val add_datatype = gen_add_datatype Datatype.cert_typ; +val datatype_cmd = snd ooo gen_add_datatype Datatype.read_typ default_config; + +local + +structure P = OuterParse and K = OuterKeyword + +fun prep_datatype_decls args = + let + val names = map + (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args; + val specs = map (fn ((((_, vs), t), mx), cons) => + (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args; + in (names, specs) end; + +val parse_datatype_decl = + (Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix -- + (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix))); + +val parse_datatype_decls = P.and_list1 parse_datatype_decl >> prep_datatype_decls; + +in + +val _ = + OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl + (parse_datatype_decls >> (fn (names, specs) => Toplevel.theory (datatype_cmd names specs))); + end; + +end; + +structure Datatype = +struct + +open Datatype; +open DatatypeRepProofs; + +end;