inductive: removed con_defs;
authorwenzelm
Wed Nov 14 18:44:27 2001 +0100 (2001-11-14)
changeset 1218091c9f661b183
parent 12179 5b427479cc14
child 12181 11a6c5620306
inductive: removed con_defs;
doc-src/HOL/HOL.tex
doc-src/TutorialI/appendix.tex
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_package.ML
src/HOL/thy_syntax.ML
     1.1 --- a/doc-src/HOL/HOL.tex	Wed Nov 14 18:42:34 2001 +0100
     1.2 +++ b/doc-src/HOL/HOL.tex	Wed Nov 14 18:44:27 2001 +0100
     1.3 @@ -2915,13 +2915,12 @@
     1.4  inductive    {\it inductive sets}
     1.5    intrs      {\it introduction rules}
     1.6    monos      {\it monotonicity theorems}
     1.7 -  con_defs   {\it constructor definitions}
     1.8  \end{ttbox}
     1.9  A coinductive definition is identical, except that it starts with the keyword
    1.10  \texttt{coinductive}.  
    1.11  
    1.12 -The \texttt{monos} and \texttt{con_defs} sections are optional.  If present,
    1.13 -each is specified by a list of identifiers.
    1.14 +The \texttt{monos} section is optional; if present it is specified by a list
    1.15 +of identifiers.
    1.16  
    1.17  \begin{itemize}
    1.18  \item The \textit{inductive sets} are specified by one or more strings.
     2.1 --- a/doc-src/TutorialI/appendix.tex	Wed Nov 14 18:42:34 2001 +0100
     2.2 +++ b/doc-src/TutorialI/appendix.tex	Wed Nov 14 18:44:27 2001 +0100
     2.3 @@ -164,7 +164,6 @@
     2.4  %\hline
     2.5  %\texttt{and} &
     2.6  %\texttt{binder} &
     2.7 -%\texttt{con_defs} &
     2.8  %\texttt{concl} &
     2.9  %\texttt{congs} \\
    2.10  %\texttt{distinct} &
     3.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Wed Nov 14 18:42:34 2001 +0100
     3.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Wed Nov 14 18:44:27 2001 +0100
     3.3 @@ -182,7 +182,7 @@
     3.4      val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
     3.5        setmp InductivePackage.quiet_mode (!quiet_mode)
     3.6          (InductivePackage.add_inductive_i false true big_rec_name' false false true
     3.7 -           rec_sets (map (fn x => (("", x), [])) rec_intr_ts) [fun_rel_comp_mono] []) thy0;
     3.8 +           rec_sets (map (fn x => (("", x), [])) rec_intr_ts) [fun_rel_comp_mono]) thy0;
     3.9  
    3.10      (* prove uniqueness and termination of primrec combinators *)
    3.11  
     4.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Wed Nov 14 18:42:34 2001 +0100
     4.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Wed Nov 14 18:44:27 2001 +0100
     4.3 @@ -180,7 +180,7 @@
     4.4      val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
     4.5        setmp InductivePackage.quiet_mode (!quiet_mode)
     4.6          (InductivePackage.add_inductive_i false true big_rec_name false true false
     4.7 -           consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono] []) thy1;
     4.8 +           consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono]) thy1;
     4.9  
    4.10      (********************************* typedef ********************************)
    4.11  
     5.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Nov 14 18:42:34 2001 +0100
     5.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Nov 14 18:44:27 2001 +0100
     5.3 @@ -48,13 +48,12 @@
     5.4    val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
     5.5      -> theory -> theory
     5.6    val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
     5.7 -    ((bstring * term) * theory attribute list) list ->
     5.8 -      thm list -> thm list -> theory -> theory *
     5.9 +    ((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
    5.10        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    5.11         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    5.12    val add_inductive: bool -> bool -> string list ->
    5.13      ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
    5.14 -      (xstring * Args.src list) list -> theory -> theory *
    5.15 +    theory -> theory *
    5.16        {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    5.17         intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    5.18    val setup: (theory -> theory) list
    5.19 @@ -485,7 +484,7 @@
    5.20  
    5.21  (* prove introduction rules *)
    5.22  
    5.23 -fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
    5.24 +fun prove_intrs coind mono fp_def intr_ts rec_sets_defs thy =
    5.25    let
    5.26      val _ = clean_message "  Proving the introduction rules ...";
    5.27  
    5.28 @@ -508,7 +507,6 @@
    5.29           backtracking may occur if the premises have extra variables!*)
    5.30         DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
    5.31         (*Now solve the equations like Inl 0 = Inl ?b2*)
    5.32 -       rewrite_goals_tac con_defs,
    5.33         REPEAT (rtac refl 1)])
    5.34        |> rulify) (1 upto (length intr_ts) ~~ intr_ts)
    5.35  
    5.36 @@ -539,10 +537,6 @@
    5.37  
    5.38  (* derivation of simplified elimination rules *)
    5.39  
    5.40 -(*Applies freeness of the given constructors, which *must* be unfolded by
    5.41 -  the given defs.  Cannot simply use the local con_defs because con_defs=[]
    5.42 -  for inference systems. (??) *)
    5.43 -
    5.44  local
    5.45  
    5.46  (*cprop should have the form t:Si where Si is an inductive set*)
    5.47 @@ -692,7 +686,7 @@
    5.48      Theory.add_consts_i (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
    5.49    else I;
    5.50  
    5.51 -fun mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
    5.52 +fun mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
    5.53        params paramTs cTs cnames =
    5.54    let
    5.55      val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
    5.56 @@ -755,7 +749,7 @@
    5.57    in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
    5.58  
    5.59  fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
    5.60 -    intros monos con_defs thy params paramTs cTs cnames induct_cases =
    5.61 +    intros monos thy params paramTs cTs cnames induct_cases =
    5.62    let
    5.63      val _ =
    5.64        if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
    5.65 @@ -764,11 +758,10 @@
    5.66      val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
    5.67  
    5.68      val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) =
    5.69 -      mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
    5.70 +      mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
    5.71          params paramTs cTs cnames;
    5.72  
    5.73 -    val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
    5.74 -      rec_sets_defs thy1;
    5.75 +    val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts rec_sets_defs thy1;
    5.76      val elims = if no_elim then [] else
    5.77        prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy1;
    5.78      val raw_induct = if no_ind then Drule.asm_rl else
    5.79 @@ -812,8 +805,7 @@
    5.80      Some x => x
    5.81    | None => error (msg ^ Sign.string_of_term sign t));
    5.82  
    5.83 -fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
    5.84 -    pre_intros monos con_defs thy =
    5.85 +fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy =
    5.86    let
    5.87      val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
    5.88      val sign = Theory.sign_of thy;
    5.89 @@ -837,14 +829,14 @@
    5.90  
    5.91      val (thy1, result as {elims, induct, ...}) =
    5.92        add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos
    5.93 -        con_defs thy params paramTs cTs cnames induct_cases;
    5.94 +        thy params paramTs cTs cnames induct_cases;
    5.95      val thy2 = thy1
    5.96        |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
    5.97        |> add_cases_induct no_elim (no_ind orelse coind orelse length cs > 1)
    5.98            full_cnames elims induct;
    5.99    in (thy2, result) end;
   5.100  
   5.101 -fun add_inductive verbose coind c_strings intro_srcs raw_monos raw_con_defs thy =
   5.102 +fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =
   5.103    let
   5.104      val sign = Theory.sign_of thy;
   5.105      val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
   5.106 @@ -856,12 +848,10 @@
   5.107      val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
   5.108      val (cs', intr_ts') = unify_consts sign cs intr_ts;
   5.109  
   5.110 -    val (thy', (monos, con_defs)) = thy
   5.111 -      |> IsarThy.apply_theorems raw_monos
   5.112 -      |>>> IsarThy.apply_theorems raw_con_defs;
   5.113 +    val (thy', monos) = thy |> IsarThy.apply_theorems raw_monos;
   5.114    in
   5.115      add_inductive_i verbose false "" coind false false cs'
   5.116 -      ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
   5.117 +      ((intr_names ~~ intr_ts') ~~ intr_atts) monos thy'
   5.118    end;
   5.119  
   5.120  
   5.121 @@ -881,15 +871,14 @@
   5.122  
   5.123  local structure P = OuterParse and K = OuterSyntax.Keyword in
   5.124  
   5.125 -fun mk_ind coind (((sets, intrs), monos), con_defs) =
   5.126 -  #1 o add_inductive true coind sets (map P.triple_swap intrs) monos con_defs;
   5.127 +fun mk_ind coind ((sets, intrs), monos) =
   5.128 +  #1 o add_inductive true coind sets (map P.triple_swap intrs) monos;
   5.129  
   5.130  fun ind_decl coind =
   5.131    (Scan.repeat1 P.term --| P.marg_comment) --
   5.132    (P.$$$ "intros" |--
   5.133      P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
   5.134 -  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
   5.135 -  Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
   5.136 +  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) []
   5.137    >> (Toplevel.theory o mk_ind coind);
   5.138  
   5.139  val inductiveP =
   5.140 @@ -907,7 +896,7 @@
   5.141    OuterSyntax.command "inductive_cases"
   5.142      "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
   5.143  
   5.144 -val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"];
   5.145 +val _ = OuterSyntax.add_keywords ["intros", "monos"];
   5.146  val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
   5.147  
   5.148  end;
     6.1 --- a/src/HOL/thy_syntax.ML	Wed Nov 14 18:42:34 2001 +0100
     6.2 +++ b/src/HOL/thy_syntax.ML	Wed Nov 14 18:44:27 2001 +0100
     6.3 @@ -54,7 +54,7 @@
     6.4      val no_atts = map (mk_pair o rpair "[]");
     6.5      fun mk_intr_name (s, _) =   (*the "op" cancels any infix status*)
     6.6        if Syntax.is_identifier s then "op " ^ s else "_";
     6.7 -    fun mk_params (((recs, ipairs), monos), con_defs) =
     6.8 +    fun mk_params ((recs, ipairs), monos) =
     6.9        let val big_rec_name = space_implode "_" (map (scan_to_id o unenclose) recs)
    6.10            and srec_tms = mk_list recs
    6.11            and sintrs   = mk_big_list (no_atts (map (mk_pair o apfst quote) ipairs))
    6.12 @@ -64,7 +64,7 @@
    6.13          \val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\
    6.14          \  InductivePackage.add_inductive true " ^
    6.15          (if coind then "true " else "false ") ^ srec_tms ^
    6.16 -         sintrs ^ " " ^ mk_list (no_atts monos) ^ " " ^ mk_list (no_atts con_defs) ^ " thy;\n\
    6.17 +         sintrs ^ " " ^ mk_list (no_atts monos) ^ " thy;\n\
    6.18          \in\n\
    6.19          \structure " ^ big_rec_name ^ " =\n\
    6.20          \struct\n\
    6.21 @@ -83,10 +83,7 @@
    6.22        end
    6.23      val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
    6.24      fun optlist s = optional (s $$-- list1 name) []
    6.25 -  in
    6.26 -    repeat1 name -- ipairs -- optlist "monos" -- optlist "con_defs"
    6.27 -      >> mk_params
    6.28 -  end;
    6.29 +  in repeat1 name -- ipairs -- optlist "monos" >> mk_params end;
    6.30  
    6.31  
    6.32  
    6.33 @@ -278,8 +275,7 @@
    6.34  in
    6.35  
    6.36  val _ = ThySyn.add_syntax
    6.37 - ["intrs", "monos", "con_defs", "congs", "simpset", "|",
    6.38 -  "and", "distinct", "inject", "induct"]
    6.39 + ["intrs", "monos", "congs", "simpset", "|", "and", "distinct", "inject", "induct"]
    6.40   [axm_section "typedef" "|> TypedefPackage.add_typedef_x" typedef_decl,
    6.41    section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl,
    6.42    section "inductive" 	"" (inductive_decl false),