--- 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.
--- 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} &
--- 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 *)
--- 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 ********************************)
--- 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;
--- 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),