src/HOL/Tools/inductive_package.ML

   val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
     -> theory -> theory
   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
 end;
 

     (fn _ => [rtac monoI 1, REPEAT (ares_tac (flat (map mk_mono monos) @ get_monos thy) 1)]));
 
 
 (* 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 ...";
 
     val unfold = standard (mono RS (fp_def RS
       (if coind then def_gfp_unfold else def_lfp_unfold)));

        EVERY1 (select_disj (length intr_ts) i),
        (*Not ares_tac, since refl must be tried before any equality assumptions;
          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)
 
   in (intrs, unfold) end;
 

         |> RuleCases.name cases)
   end;
 
 
 (* 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*)
 val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";

 fun cond_declare_consts declare_consts cs paramTs cnames =
   if declare_consts then
     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;
     val setT = HOLogic.mk_setT sumT;
 

     val mono = prove_mono setT fp_fun monos thy'
 
   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) " ^
         commas_quote cnames) else ();
 
     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
       if coind then standard (rule_by_tactic
         (rewrite_tac [mk_meta_eq vimage_Un] THEN

 fun try_term f msg sign t =
   (case Library.try f t of
     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;
 
     (*parameters should agree for all mutually recursive components*)

     val intros = map (check_rule save_sign cs) pre_intros;
     val induct_cases = map (#1 o #1) intros;
 
     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;
 
     val intr_names = map (fst o fst) intro_srcs;

       handle ERROR => error ("The error(s) above occurred for " ^ s);
     val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
     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;
 
 
 
 (** package setup **)

 
 (* outer syntax *)
 
 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 =
   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
 

 
 val inductive_casesP =
   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;
 
 end;