# HG changeset patch # User wenzelm # Date 1005759867 -3600 # Node ID 91c9f661b183d2abffd5f1db762db111d94488d2 # Parent 5b427479cc14c266bd3c4c1af5160c8ce80138c3 inductive: removed con_defs; diff -r 5b427479cc14 -r 91c9f661b183 doc-src/HOL/HOL.tex --- a/doc-src/HOL/HOL.tex Wed Nov 14 18:42:34 2001 +0100 +++ b/doc-src/HOL/HOL.tex Wed Nov 14 18:44:27 2001 +0100 @@ -2915,13 +2915,12 @@ inductive {\it inductive sets} intrs {\it introduction rules} monos {\it monotonicity theorems} - con_defs {\it constructor definitions} \end{ttbox} A coinductive definition is identical, except that it starts with the keyword \texttt{coinductive}. -The \texttt{monos} and \texttt{con_defs} sections are optional. If present, -each is specified by a list of identifiers. +The \texttt{monos} section is optional; if present it is specified by a list +of identifiers. \begin{itemize} \item The \textit{inductive sets} are specified by one or more strings. diff -r 5b427479cc14 -r 91c9f661b183 doc-src/TutorialI/appendix.tex --- a/doc-src/TutorialI/appendix.tex Wed Nov 14 18:42:34 2001 +0100 +++ b/doc-src/TutorialI/appendix.tex Wed Nov 14 18:44:27 2001 +0100 @@ -164,7 +164,6 @@ %\hline %\texttt{and} & %\texttt{binder} & -%\texttt{con_defs} & %\texttt{concl} & %\texttt{congs} \\ %\texttt{distinct} & diff -r 5b427479cc14 -r 91c9f661b183 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Wed Nov 14 18:42:34 2001 +0100 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Wed Nov 14 18:44:27 2001 +0100 @@ -182,7 +182,7 @@ val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) = setmp InductivePackage.quiet_mode (!quiet_mode) (InductivePackage.add_inductive_i false true big_rec_name' false false true - rec_sets (map (fn x => (("", x), [])) rec_intr_ts) [fun_rel_comp_mono] []) thy0; + rec_sets (map (fn x => (("", x), [])) rec_intr_ts) [fun_rel_comp_mono]) thy0; (* prove uniqueness and termination of primrec combinators *) diff -r 5b427479cc14 -r 91c9f661b183 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Wed Nov 14 18:42:34 2001 +0100 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed Nov 14 18:44:27 2001 +0100 @@ -180,7 +180,7 @@ val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) = setmp InductivePackage.quiet_mode (!quiet_mode) (InductivePackage.add_inductive_i false true big_rec_name false true false - consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono] []) thy1; + consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono]) thy1; (********************************* typedef ********************************) diff -r 5b427479cc14 -r 91c9f661b183 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Wed Nov 14 18:42:34 2001 +0100 +++ b/src/HOL/Tools/inductive_package.ML Wed Nov 14 18:44:27 2001 +0100 @@ -48,13 +48,12 @@ val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text -> theory -> theory val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list -> - ((bstring * term) * theory attribute list) list -> - thm list -> thm list -> theory -> theory * + ((bstring * term) * theory attribute list) list -> thm list -> theory -> theory * {defs: thm list, elims: thm list, raw_induct: thm, induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} val add_inductive: bool -> bool -> string list -> ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list -> - (xstring * Args.src list) list -> theory -> theory * + theory -> theory * {defs: thm list, elims: thm list, raw_induct: thm, induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} val setup: (theory -> theory) list @@ -485,7 +484,7 @@ (* prove introduction rules *) -fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy = +fun prove_intrs coind mono fp_def intr_ts rec_sets_defs thy = let val _ = clean_message " Proving the introduction rules ..."; @@ -508,7 +507,6 @@ backtracking may occur if the premises have extra variables!*) DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1), (*Now solve the equations like Inl 0 = Inl ?b2*) - rewrite_goals_tac con_defs, REPEAT (rtac refl 1)]) |> rulify) (1 upto (length intr_ts) ~~ intr_ts) @@ -539,10 +537,6 @@ (* derivation of simplified elimination rules *) -(*Applies freeness of the given constructors, which *must* be unfolded by - the given defs. Cannot simply use the local con_defs because con_defs=[] - for inference systems. (??) *) - local (*cprop should have the form t:Si where Si is an inductive set*) @@ -692,7 +686,7 @@ Theory.add_consts_i (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames)) else I; -fun mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy +fun mk_ind_def declare_consts alt_name coind cs intr_ts monos thy params paramTs cTs cnames = let val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; @@ -755,7 +749,7 @@ in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end; fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs - intros monos con_defs thy params paramTs cTs cnames induct_cases = + intros monos thy params paramTs cTs cnames induct_cases = let val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ @@ -764,11 +758,10 @@ val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros); val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) = - mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy + mk_ind_def declare_consts alt_name coind cs intr_ts monos thy params paramTs cTs cnames; - val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs - rec_sets_defs thy1; + val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts rec_sets_defs thy1; val elims = if no_elim then [] else prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy1; val raw_induct = if no_ind then Drule.asm_rl else @@ -812,8 +805,7 @@ Some x => x | None => error (msg ^ Sign.string_of_term sign t)); -fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs - pre_intros monos con_defs thy = +fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy = let val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); val sign = Theory.sign_of thy; @@ -837,14 +829,14 @@ val (thy1, result as {elims, induct, ...}) = add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos - con_defs thy params paramTs cTs cnames induct_cases; + thy params paramTs cTs cnames induct_cases; val thy2 = thy1 |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result) |> add_cases_induct no_elim (no_ind orelse coind orelse length cs > 1) full_cnames elims induct; in (thy2, result) end; -fun add_inductive verbose coind c_strings intro_srcs raw_monos raw_con_defs thy = +fun add_inductive verbose coind c_strings intro_srcs raw_monos thy = let val sign = Theory.sign_of thy; val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings; @@ -856,12 +848,10 @@ val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs; val (cs', intr_ts') = unify_consts sign cs intr_ts; - val (thy', (monos, con_defs)) = thy - |> IsarThy.apply_theorems raw_monos - |>>> IsarThy.apply_theorems raw_con_defs; + val (thy', monos) = thy |> IsarThy.apply_theorems raw_monos; in add_inductive_i verbose false "" coind false false cs' - ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy' + ((intr_names ~~ intr_ts') ~~ intr_atts) monos thy' end; @@ -881,15 +871,14 @@ local structure P = OuterParse and K = OuterSyntax.Keyword in -fun mk_ind coind (((sets, intrs), monos), con_defs) = - #1 o add_inductive true coind sets (map P.triple_swap intrs) monos con_defs; +fun mk_ind coind ((sets, intrs), monos) = + #1 o add_inductive true coind sets (map P.triple_swap intrs) monos; fun ind_decl coind = (Scan.repeat1 P.term --| P.marg_comment) -- (P.$$$ "intros" |-- P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) -- - Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] -- - Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) [] + Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] >> (Toplevel.theory o mk_ind coind); val inductiveP = @@ -907,7 +896,7 @@ OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules (improper)" K.thy_script ind_cases; -val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"]; +val _ = OuterSyntax.add_keywords ["intros", "monos"]; val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP]; end; diff -r 5b427479cc14 -r 91c9f661b183 src/HOL/thy_syntax.ML --- a/src/HOL/thy_syntax.ML Wed Nov 14 18:42:34 2001 +0100 +++ b/src/HOL/thy_syntax.ML Wed Nov 14 18:44:27 2001 +0100 @@ -54,7 +54,7 @@ val no_atts = map (mk_pair o rpair "[]"); fun mk_intr_name (s, _) = (*the "op" cancels any infix status*) if Syntax.is_identifier s then "op " ^ s else "_"; - fun mk_params (((recs, ipairs), monos), con_defs) = + fun mk_params ((recs, ipairs), monos) = let val big_rec_name = space_implode "_" (map (scan_to_id o unenclose) recs) and srec_tms = mk_list recs and sintrs = mk_big_list (no_atts (map (mk_pair o apfst quote) ipairs)) @@ -64,7 +64,7 @@ \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\ \ InductivePackage.add_inductive true " ^ (if coind then "true " else "false ") ^ srec_tms ^ - sintrs ^ " " ^ mk_list (no_atts monos) ^ " " ^ mk_list (no_atts con_defs) ^ " thy;\n\ + sintrs ^ " " ^ mk_list (no_atts monos) ^ " thy;\n\ \in\n\ \structure " ^ big_rec_name ^ " =\n\ \struct\n\ @@ -83,10 +83,7 @@ end val ipairs = "intrs" $$-- repeat1 (ident -- !! string) fun optlist s = optional (s $$-- list1 name) [] - in - repeat1 name -- ipairs -- optlist "monos" -- optlist "con_defs" - >> mk_params - end; + in repeat1 name -- ipairs -- optlist "monos" >> mk_params end; @@ -278,8 +275,7 @@ in val _ = ThySyn.add_syntax - ["intrs", "monos", "con_defs", "congs", "simpset", "|", - "and", "distinct", "inject", "induct"] + ["intrs", "monos", "congs", "simpset", "|", "and", "distinct", "inject", "induct"] [axm_section "typedef" "|> TypedefPackage.add_typedef_x" typedef_decl, section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl, section "inductive" "" (inductive_decl false),