src/HOL/Tools/inductive_package.ML
 author wenzelm Wed Nov 21 00:34:06 2001 +0100 (2001-11-21 ago) changeset 12259 3949e7aba298 parent 12180 91c9f661b183 child 12311 ce5f9e61c037 permissions -rw-r--r--
Set.vimage;
```     1 (*  Title:      HOL/Tools/inductive_package.ML
```
```     2     ID:         \$Id\$
```
```     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Author:     Stefan Berghofer, TU Muenchen
```
```     5     Author:     Markus Wenzel, TU Muenchen
```
```     6     License:    GPL (GNU GENERAL PUBLIC LICENSE)
```
```     7
```
```     8 (Co)Inductive Definition module for HOL.
```
```     9
```
```    10 Features:
```
```    11   * least or greatest fixedpoints
```
```    12   * user-specified product and sum constructions
```
```    13   * mutually recursive definitions
```
```    14   * definitions involving arbitrary monotone operators
```
```    15   * automatically proves introduction and elimination rules
```
```    16
```
```    17 The recursive sets must *already* be declared as constants in the
```
```    18 current theory!
```
```    19
```
```    20   Introduction rules have the form
```
```    21   [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk
```
```    22   where M is some monotone operator (usually the identity)
```
```    23   P(x) is any side condition on the free variables
```
```    24   ti, t are any terms
```
```    25   Sj, Sk are two of the sets being defined in mutual recursion
```
```    26
```
```    27 Sums are used only for mutual recursion.  Products are used only to
```
```    28 derive "streamlined" induction rules for relations.
```
```    29 *)
```
```    30
```
```    31 signature INDUCTIVE_PACKAGE =
```
```    32 sig
```
```    33   val quiet_mode: bool ref
```
```    34   val unify_consts: Sign.sg -> term list -> term list -> term list * term list
```
```    35   val split_rule_vars: term list -> thm -> thm
```
```    36   val get_inductive: theory -> string -> ({names: string list, coind: bool} *
```
```    37     {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
```
```    38      intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
```
```    39   val print_inductives: theory -> unit
```
```    40   val mono_add_global: theory attribute
```
```    41   val mono_del_global: theory attribute
```
```    42   val get_monos: theory -> thm list
```
```    43   val inductive_forall_name: string
```
```    44   val inductive_forall_def: thm
```
```    45   val rulify: thm -> thm
```
```    46   val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
```
```    47     -> theory -> theory
```
```    48   val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
```
```    49     -> theory -> theory
```
```    50   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
```
```    51     ((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
```
```    52       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
```
```    53        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
```
```    54   val add_inductive: bool -> bool -> string list ->
```
```    55     ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
```
```    56     theory -> theory *
```
```    57       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
```
```    58        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
```
```    59   val setup: (theory -> theory) list
```
```    60 end;
```
```    61
```
```    62 structure InductivePackage: INDUCTIVE_PACKAGE =
```
```    63 struct
```
```    64
```
```    65
```
```    66 (** theory context references **)
```
```    67
```
```    68 val mono_name = "HOL.mono";
```
```    69 val gfp_name = "Gfp.gfp";
```
```    70 val lfp_name = "Lfp.lfp";
```
```    71 val vimage_name = "Set.vimage";
```
```    72 val Const _ \$ (vimage_f \$ _) \$ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
```
```    73
```
```    74 val inductive_forall_name = "HOL.induct_forall";
```
```    75 val inductive_forall_def = thm "induct_forall_def";
```
```    76 val inductive_conj_name = "HOL.induct_conj";
```
```    77 val inductive_conj_def = thm "induct_conj_def";
```
```    78 val inductive_conj = thms "induct_conj";
```
```    79 val inductive_atomize = thms "induct_atomize";
```
```    80 val inductive_rulify1 = thms "induct_rulify1";
```
```    81 val inductive_rulify2 = thms "induct_rulify2";
```
```    82
```
```    83
```
```    84
```
```    85 (** theory data **)
```
```    86
```
```    87 (* data kind 'HOL/inductive' *)
```
```    88
```
```    89 type inductive_info =
```
```    90   {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
```
```    91     induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
```
```    92
```
```    93 structure InductiveArgs =
```
```    94 struct
```
```    95   val name = "HOL/inductive";
```
```    96   type T = inductive_info Symtab.table * thm list;
```
```    97
```
```    98   val empty = (Symtab.empty, []);
```
```    99   val copy = I;
```
```   100   val finish = I;
```
```   101   val prep_ext = I;
```
```   102   fun merge ((tab1, monos1), (tab2, monos2)) =
```
```   103     (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
```
```   104
```
```   105   fun print sg (tab, monos) =
```
```   106     [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
```
```   107      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)]
```
```   108     |> Pretty.chunks |> Pretty.writeln;
```
```   109 end;
```
```   110
```
```   111 structure InductiveData = TheoryDataFun(InductiveArgs);
```
```   112 val print_inductives = InductiveData.print;
```
```   113
```
```   114
```
```   115 (* get and put data *)
```
```   116
```
```   117 fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name);
```
```   118
```
```   119 fun the_inductive thy name =
```
```   120   (case get_inductive thy name of
```
```   121     None => error ("Unknown (co)inductive set " ^ quote name)
```
```   122   | Some info => info);
```
```   123
```
```   124 fun put_inductives names info thy =
```
```   125   let
```
```   126     fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
```
```   127     val tab_monos = foldl upd (InductiveData.get thy, names)
```
```   128       handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
```
```   129   in InductiveData.put tab_monos thy end;
```
```   130
```
```   131
```
```   132
```
```   133 (** monotonicity rules **)
```
```   134
```
```   135 val get_monos = #2 o InductiveData.get;
```
```   136 fun map_monos f = InductiveData.map (Library.apsnd f);
```
```   137
```
```   138 fun mk_mono thm =
```
```   139   let
```
```   140     fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @
```
```   141       (case concl_of thm of
```
```   142           (_ \$ (_ \$ (Const ("Not", _) \$ _) \$ _)) => []
```
```   143         | _ => [standard (thm' RS (thm' RS eq_to_mono2))]);
```
```   144     val concl = concl_of thm
```
```   145   in
```
```   146     if Logic.is_equals concl then
```
```   147       eq2mono (thm RS meta_eq_to_obj_eq)
```
```   148     else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
```
```   149       eq2mono thm
```
```   150     else [thm]
```
```   151   end;
```
```   152
```
```   153
```
```   154 (* attributes *)
```
```   155
```
```   156 fun mono_add_global (thy, thm) = (map_monos (Drule.add_rules (mk_mono thm)) thy, thm);
```
```   157 fun mono_del_global (thy, thm) = (map_monos (Drule.del_rules (mk_mono thm)) thy, thm);
```
```   158
```
```   159 val mono_attr =
```
```   160  (Attrib.add_del_args mono_add_global mono_del_global,
```
```   161   Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute);
```
```   162
```
```   163
```
```   164
```
```   165 (** misc utilities **)
```
```   166
```
```   167 val quiet_mode = ref false;
```
```   168 fun message s = if ! quiet_mode then () else writeln s;
```
```   169 fun clean_message s = if ! quick_and_dirty then () else message s;
```
```   170
```
```   171 fun coind_prefix true = "co"
```
```   172   | coind_prefix false = "";
```
```   173
```
```   174
```
```   175 (*the following code ensures that each recursive set always has the
```
```   176   same type in all introduction rules*)
```
```   177 fun unify_consts sign cs intr_ts =
```
```   178   (let
```
```   179     val {tsig, ...} = Sign.rep_sg sign;
```
```   180     val add_term_consts_2 =
```
```   181       foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
```
```   182     fun varify (t, (i, ts)) =
```
```   183       let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
```
```   184       in (maxidx_of_term t', t'::ts) end;
```
```   185     val (i, cs') = foldr varify (cs, (~1, []));
```
```   186     val (i', intr_ts') = foldr varify (intr_ts, (i, []));
```
```   187     val rec_consts = foldl add_term_consts_2 ([], cs');
```
```   188     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
```
```   189     fun unify (env, (cname, cT)) =
```
```   190       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
```
```   191       in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
```
```   192           (env, (replicate (length consts) cT) ~~ consts)
```
```   193       end;
```
```   194     val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts);
```
```   195     fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T
```
```   196       in if T = T' then T else typ_subst_TVars_2 env T' end;
```
```   197     val subst = fst o Type.freeze_thaw o
```
```   198       (map_term_types (typ_subst_TVars_2 env))
```
```   199
```
```   200   in (map subst cs', map subst intr_ts')
```
```   201   end) handle Type.TUNIFY =>
```
```   202     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
```
```   203
```
```   204
```
```   205 (*make injections used in mutually recursive definitions*)
```
```   206 fun mk_inj cs sumT c x =
```
```   207   let
```
```   208     fun mk_inj' T n i =
```
```   209       if n = 1 then x else
```
```   210       let val n2 = n div 2;
```
```   211           val Type (_, [T1, T2]) = T
```
```   212       in
```
```   213         if i <= n2 then
```
```   214           Const ("Inl", T1 --> T) \$ (mk_inj' T1 n2 i)
```
```   215         else
```
```   216           Const ("Inr", T2 --> T) \$ (mk_inj' T2 (n - n2) (i - n2))
```
```   217       end
```
```   218   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
```
```   219   end;
```
```   220
```
```   221 (*make "vimage" terms for selecting out components of mutually rec.def*)
```
```   222 fun mk_vimage cs sumT t c = if length cs < 2 then t else
```
```   223   let
```
```   224     val cT = HOLogic.dest_setT (fastype_of c);
```
```   225     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
```
```   226   in
```
```   227     Const (vimage_name, vimageT) \$
```
```   228       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) \$ t
```
```   229   end;
```
```   230
```
```   231 (** proper splitting **)
```
```   232
```
```   233 fun prod_factors p (Const ("Pair", _) \$ t \$ u) =
```
```   234       p :: prod_factors (1::p) t @ prod_factors (2::p) u
```
```   235   | prod_factors p _ = [];
```
```   236
```
```   237 fun mg_prod_factors ts (fs, t \$ u) = if t mem ts then
```
```   238         let val f = prod_factors [] u
```
```   239         in overwrite (fs, (t, f inter if_none (assoc (fs, t)) f)) end
```
```   240       else mg_prod_factors ts (mg_prod_factors ts (fs, t), u)
```
```   241   | mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t)
```
```   242   | mg_prod_factors ts (fs, _) = fs;
```
```   243
```
```   244 fun prodT_factors p ps (T as Type ("*", [T1, T2])) =
```
```   245       if p mem ps then prodT_factors (1::p) ps T1 @ prodT_factors (2::p) ps T2
```
```   246       else [T]
```
```   247   | prodT_factors _ _ T = [T];
```
```   248
```
```   249 fun ap_split p ps (Type ("*", [T1, T2])) T3 u =
```
```   250       if p mem ps then HOLogic.split_const (T1, T2, T3) \$
```
```   251         Abs ("v", T1, ap_split (2::p) ps T2 T3 (ap_split (1::p) ps T1
```
```   252           (prodT_factors (2::p) ps T2 ---> T3) (incr_boundvars 1 u) \$ Bound 0))
```
```   253       else u
```
```   254   | ap_split _ _ _ _ u =  u;
```
```   255
```
```   256 fun mk_tuple p ps (Type ("*", [T1, T2])) (tms as t::_) =
```
```   257       if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms,
```
```   258         mk_tuple (2::p) ps T2 (drop (length (prodT_factors (1::p) ps T1), tms)))
```
```   259       else t
```
```   260   | mk_tuple _ _ _ (t::_) = t;
```
```   261
```
```   262 fun split_rule_var' ((t as Var (v, Type ("fun", [T1, T2])), ps), rl) =
```
```   263       let val T' = prodT_factors [] ps T1 ---> T2
```
```   264           val newt = ap_split [] ps T1 T2 (Var (v, T'))
```
```   265           val cterm = Thm.cterm_of (#sign (rep_thm rl))
```
```   266       in
```
```   267           instantiate ([], [(cterm t, cterm newt)]) rl
```
```   268       end
```
```   269   | split_rule_var' (_, rl) = rl;
```
```   270
```
```   271 val remove_split = rewrite_rule [split_conv RS eq_reflection];
```
```   272
```
```   273 fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
```
```   274   (mg_prod_factors vs ([], #prop (rep_thm rl)), rl)));
```
```   275
```
```   276 fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
```
```   277   (mapfilter (fn (t as Var ((a, _), _)) =>
```
```   278     apsome (pair t) (assoc (vs, a))) (term_vars (#prop (rep_thm rl))), rl)));
```
```   279
```
```   280
```
```   281 (** process rules **)
```
```   282
```
```   283 local
```
```   284
```
```   285 fun err_in_rule sg name t msg =
```
```   286   error (cat_lines ["Ill-formed introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
```
```   287
```
```   288 fun err_in_prem sg name t p msg =
```
```   289   error (cat_lines ["Ill-formed premise", Sign.string_of_term sg p,
```
```   290     "in introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
```
```   291
```
```   292 val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
```
```   293
```
```   294 val all_not_allowed =
```
```   295     "Introduction rule must not have a leading \"!!\" quantifier";
```
```   296
```
```   297 val atomize_cterm = Tactic.rewrite_cterm true inductive_atomize;
```
```   298
```
```   299 in
```
```   300
```
```   301 fun check_rule sg cs ((name, rule), att) =
```
```   302   let
```
```   303     val concl = Logic.strip_imp_concl rule;
```
```   304     val prems = Logic.strip_imp_prems rule;
```
```   305     val aprems = prems |> map (Thm.term_of o atomize_cterm o Thm.cterm_of sg);
```
```   306     val arule = Logic.list_implies (aprems, concl);
```
```   307
```
```   308     fun check_prem (prem, aprem) =
```
```   309       if can HOLogic.dest_Trueprop aprem then ()
```
```   310       else err_in_prem sg name rule prem "Non-atomic premise";
```
```   311   in
```
```   312     (case concl of
```
```   313       Const ("Trueprop", _) \$ (Const ("op :", _) \$ t \$ u) =>
```
```   314         if u mem cs then
```
```   315           if exists (Logic.occs o rpair t) cs then
```
```   316             err_in_rule sg name rule "Recursion term on left of member symbol"
```
```   317           else seq check_prem (prems ~~ aprems)
```
```   318         else err_in_rule sg name rule bad_concl
```
```   319       | Const ("all", _) \$ _ => err_in_rule sg name rule all_not_allowed
```
```   320       | _ => err_in_rule sg name rule bad_concl);
```
```   321     ((name, arule), att)
```
```   322   end;
```
```   323
```
```   324 val rulify =
```
```   325   standard o Tactic.norm_hhf o
```
```   326   hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o
```
```   327   hol_simplify inductive_conj;
```
```   328
```
```   329 end;
```
```   330
```
```   331
```
```   332
```
```   333 (** properties of (co)inductive sets **)
```
```   334
```
```   335 (* elimination rules *)
```
```   336
```
```   337 fun mk_elims cs cTs params intr_ts intr_names =
```
```   338   let
```
```   339     val used = foldr add_term_names (intr_ts, []);
```
```   340     val [aname, pname] = variantlist (["a", "P"], used);
```
```   341     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
```
```   342
```
```   343     fun dest_intr r =
```
```   344       let val Const ("op :", _) \$ t \$ u =
```
```   345         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
```
```   346       in (u, t, Logic.strip_imp_prems r) end;
```
```   347
```
```   348     val intrs = map dest_intr intr_ts ~~ intr_names;
```
```   349
```
```   350     fun mk_elim (c, T) =
```
```   351       let
```
```   352         val a = Free (aname, T);
```
```   353
```
```   354         fun mk_elim_prem (_, t, ts) =
```
```   355           list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
```
```   356             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
```
```   357         val c_intrs = (filter (equal c o #1 o #1) intrs);
```
```   358       in
```
```   359         (Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
```
```   360           map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs)
```
```   361       end
```
```   362   in
```
```   363     map mk_elim (cs ~~ cTs)
```
```   364   end;
```
```   365
```
```   366
```
```   367 (* premises and conclusions of induction rules *)
```
```   368
```
```   369 fun mk_indrule cs cTs params intr_ts =
```
```   370   let
```
```   371     val used = foldr add_term_names (intr_ts, []);
```
```   372
```
```   373     (* predicates for induction rule *)
```
```   374
```
```   375     val preds = map Free (variantlist (if length cs < 2 then ["P"] else
```
```   376       map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
```
```   377         map (fn T => T --> HOLogic.boolT) cTs);
```
```   378
```
```   379     (* transform an introduction rule into a premise for induction rule *)
```
```   380
```
```   381     fun mk_ind_prem r =
```
```   382       let
```
```   383         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
```
```   384
```
```   385         val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
```
```   386
```
```   387         fun subst (s as ((m as Const ("op :", T)) \$ t \$ u)) =
```
```   388               (case pred_of u of
```
```   389                   None => (m \$ fst (subst t) \$ fst (subst u), None)
```
```   390                 | Some P => (HOLogic.mk_binop inductive_conj_name (s, P \$ t), Some (s, P \$ t)))
```
```   391           | subst s =
```
```   392               (case pred_of s of
```
```   393                   Some P => (HOLogic.mk_binop "op Int"
```
```   394                     (s, HOLogic.Collect_const (HOLogic.dest_setT
```
```   395                       (fastype_of s)) \$ P), None)
```
```   396                 | None => (case s of
```
```   397                      (t \$ u) => (fst (subst t) \$ fst (subst u), None)
```
```   398                    | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None)
```
```   399                    | _ => (s, None)));
```
```   400
```
```   401         fun mk_prem (s, prems) = (case subst s of
```
```   402               (_, Some (t, u)) => t :: u :: prems
```
```   403             | (t, _) => t :: prems);
```
```   404
```
```   405         val Const ("op :", _) \$ t \$ u =
```
```   406           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
```
```   407
```
```   408       in list_all_free (frees,
```
```   409            Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
```
```   410              (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
```
```   411                HOLogic.mk_Trueprop (the (pred_of u) \$ t)))
```
```   412       end;
```
```   413
```
```   414     val ind_prems = map mk_ind_prem intr_ts;
```
```   415     val factors = foldl (mg_prod_factors preds) ([], ind_prems);
```
```   416
```
```   417     (* make conclusions for induction rules *)
```
```   418
```
```   419     fun mk_ind_concl ((c, P), (ts, x)) =
```
```   420       let val T = HOLogic.dest_setT (fastype_of c);
```
```   421           val ps = if_none (assoc (factors, P)) [];
```
```   422           val Ts = prodT_factors [] ps T;
```
```   423           val (frees, x') = foldr (fn (T', (fs, s)) =>
```
```   424             ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
```
```   425           val tuple = mk_tuple [] ps T frees;
```
```   426       in ((HOLogic.mk_binop "op -->"
```
```   427         (HOLogic.mk_mem (tuple, c), P \$ tuple))::ts, x')
```
```   428       end;
```
```   429
```
```   430     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
```
```   431         (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
```
```   432
```
```   433   in (preds, ind_prems, mutual_ind_concl,
```
```   434     map (apfst (fst o dest_Free)) factors)
```
```   435   end;
```
```   436
```
```   437
```
```   438 (* prepare cases and induct rules *)
```
```   439
```
```   440 (*
```
```   441   transform mutual rule:
```
```   442     HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
```
```   443   into i-th projection:
```
```   444     xi:Ai ==> HH ==> Pi xi
```
```   445 *)
```
```   446
```
```   447 fun project_rules [name] rule = [(name, rule)]
```
```   448   | project_rules names mutual_rule =
```
```   449       let
```
```   450         val n = length names;
```
```   451         fun proj i =
```
```   452           (if i < n then (fn th => th RS conjunct1) else I)
```
```   453             (Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule)
```
```   454             RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
```
```   455       in names ~~ map proj (1 upto n) end;
```
```   456
```
```   457 fun add_cases_induct no_elim no_induct names elims induct =
```
```   458   let
```
```   459     fun cases_spec (name, elim) thy =
```
```   460       thy
```
```   461       |> Theory.add_path (Sign.base_name name)
```
```   462       |> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
```
```   463       |> Theory.parent_path;
```
```   464     val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
```
```   465
```
```   466     fun induct_spec (name, th) = #1 o PureThy.add_thms
```
```   467       [(("", RuleCases.save induct th), [InductAttrib.induct_set_global name])];
```
```   468     val induct_specs = if no_induct then [] else map induct_spec (project_rules names induct);
```
```   469   in Library.apply (cases_specs @ induct_specs) end;
```
```   470
```
```   471
```
```   472
```
```   473 (** proofs for (co)inductive sets **)
```
```   474
```
```   475 (* prove monotonicity -- NOT subject to quick_and_dirty! *)
```
```   476
```
```   477 fun prove_mono setT fp_fun monos thy =
```
```   478  (message "  Proving monotonicity ...";
```
```   479   Goals.prove_goalw_cterm []      (*NO quick_and_dirty_prove_goalw_cterm here!*)
```
```   480     (Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
```
```   481       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) \$ fp_fun)))
```
```   482     (fn _ => [rtac monoI 1, REPEAT (ares_tac (flat (map mk_mono monos) @ get_monos thy) 1)]));
```
```   483
```
```   484
```
```   485 (* prove introduction rules *)
```
```   486
```
```   487 fun prove_intrs coind mono fp_def intr_ts rec_sets_defs thy =
```
```   488   let
```
```   489     val _ = clean_message "  Proving the introduction rules ...";
```
```   490
```
```   491     val unfold = standard (mono RS (fp_def RS
```
```   492       (if coind then def_gfp_unfold else def_lfp_unfold)));
```
```   493
```
```   494     fun select_disj 1 1 = []
```
```   495       | select_disj _ 1 = [rtac disjI1]
```
```   496       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
```
```   497
```
```   498     val intrs = map (fn (i, intr) => quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
```
```   499       (Thm.cterm_of (Theory.sign_of thy) intr) (fn prems =>
```
```   500        [(*insert prems and underlying sets*)
```
```   501        cut_facts_tac prems 1,
```
```   502        stac unfold 1,
```
```   503        REPEAT (resolve_tac [vimageI2, CollectI] 1),
```
```   504        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
```
```   505        EVERY1 (select_disj (length intr_ts) i),
```
```   506        (*Not ares_tac, since refl must be tried before any equality assumptions;
```
```   507          backtracking may occur if the premises have extra variables!*)
```
```   508        DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
```
```   509        (*Now solve the equations like Inl 0 = Inl ?b2*)
```
```   510        REPEAT (rtac refl 1)])
```
```   511       |> rulify) (1 upto (length intr_ts) ~~ intr_ts)
```
```   512
```
```   513   in (intrs, unfold) end;
```
```   514
```
```   515
```
```   516 (* prove elimination rules *)
```
```   517
```
```   518 fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy =
```
```   519   let
```
```   520     val _ = clean_message "  Proving the elimination rules ...";
```
```   521
```
```   522     val rules1 = [CollectE, disjE, make_elim vimageD, exE];
```
```   523     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
```
```   524   in
```
```   525     mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
```
```   526       quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
```
```   527         (Thm.cterm_of (Theory.sign_of thy) t) (fn prems =>
```
```   528           [cut_facts_tac [hd prems] 1,
```
```   529            dtac (unfold RS subst) 1,
```
```   530            REPEAT (FIRSTGOAL (eresolve_tac rules1)),
```
```   531            REPEAT (FIRSTGOAL (eresolve_tac rules2)),
```
```   532            EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
```
```   533         |> rulify
```
```   534         |> RuleCases.name cases)
```
```   535   end;
```
```   536
```
```   537
```
```   538 (* derivation of simplified elimination rules *)
```
```   539
```
```   540 local
```
```   541
```
```   542 (*cprop should have the form t:Si where Si is an inductive set*)
```
```   543 val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
```
```   544
```
```   545 (*delete needless equality assumptions*)
```
```   546 val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
```
```   547 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
```
```   548 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
```
```   549
```
```   550 fun simp_case_tac solved ss i =
```
```   551   EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i
```
```   552   THEN_MAYBE (if solved then no_tac else all_tac);
```
```   553
```
```   554 in
```
```   555
```
```   556 fun mk_cases_i elims ss cprop =
```
```   557   let
```
```   558     val prem = Thm.assume cprop;
```
```   559     val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac;
```
```   560     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
```
```   561   in
```
```   562     (case get_first (try mk_elim) elims of
```
```   563       Some r => r
```
```   564     | None => error (Pretty.string_of (Pretty.block
```
```   565         [Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop])))
```
```   566   end;
```
```   567
```
```   568 fun mk_cases elims s =
```
```   569   mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
```
```   570
```
```   571 fun smart_mk_cases thy ss cprop =
```
```   572   let
```
```   573     val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop
```
```   574       (Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err;
```
```   575     val (_, {elims, ...}) = the_inductive thy c;
```
```   576   in mk_cases_i elims ss cprop end;
```
```   577
```
```   578 end;
```
```   579
```
```   580
```
```   581 (* inductive_cases(_i) *)
```
```   582
```
```   583 fun gen_inductive_cases prep_att prep_prop (((name, raw_atts), raw_props), comment) thy =
```
```   584   let
```
```   585     val ss = Simplifier.simpset_of thy;
```
```   586     val sign = Theory.sign_of thy;
```
```   587     val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
```
```   588     val atts = map (prep_att thy) raw_atts;
```
```   589     val thms = map (smart_mk_cases thy ss) cprops;
```
```   590   in
```
```   591     thy |>
```
```   592     IsarThy.have_theorems_i Drule.lemmaK [(((name, atts), map Thm.no_attributes thms), comment)]
```
```   593   end;
```
```   594
```
```   595 val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
```
```   596 val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
```
```   597
```
```   598
```
```   599 (* mk_cases_meth *)
```
```   600
```
```   601 fun mk_cases_meth (ctxt, raw_props) =
```
```   602   let
```
```   603     val thy = ProofContext.theory_of ctxt;
```
```   604     val ss = Simplifier.get_local_simpset ctxt;
```
```   605     val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props;
```
```   606   in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
```
```   607
```
```   608 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
```
```   609
```
```   610
```
```   611 (* prove induction rule *)
```
```   612
```
```   613 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
```
```   614     fp_def rec_sets_defs thy =
```
```   615   let
```
```   616     val _ = clean_message "  Proving the induction rule ...";
```
```   617
```
```   618     val sign = Theory.sign_of thy;
```
```   619
```
```   620     val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
```
```   621         None => []
```
```   622       | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
```
```   623
```
```   624     val (preds, ind_prems, mutual_ind_concl, factors) =
```
```   625       mk_indrule cs cTs params intr_ts;
```
```   626
```
```   627     (* make predicate for instantiation of abstract induction rule *)
```
```   628
```
```   629     fun mk_ind_pred _ [P] = P
```
```   630       | mk_ind_pred T Ps =
```
```   631          let val n = (length Ps) div 2;
```
```   632              val Type (_, [T1, T2]) = T
```
```   633          in Const ("Datatype.sum.sum_case",
```
```   634            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) \$
```
```   635              mk_ind_pred T1 (take (n, Ps)) \$ mk_ind_pred T2 (drop (n, Ps))
```
```   636          end;
```
```   637
```
```   638     val ind_pred = mk_ind_pred sumT preds;
```
```   639
```
```   640     val ind_concl = HOLogic.mk_Trueprop
```
```   641       (HOLogic.all_const sumT \$ Abs ("x", sumT, HOLogic.mk_binop "op -->"
```
```   642         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred \$ Bound 0)));
```
```   643
```
```   644     (* simplification rules for vimage and Collect *)
```
```   645
```
```   646     val vimage_simps = if length cs < 2 then [] else
```
```   647       map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of sign
```
```   648         (HOLogic.mk_Trueprop (HOLogic.mk_eq
```
```   649           (mk_vimage cs sumT (HOLogic.Collect_const sumT \$ ind_pred) c,
```
```   650            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) \$
```
```   651              nth_elem (find_index_eq c cs, preds)))))
```
```   652         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
```
```   653
```
```   654     val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
```
```   655       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
```
```   656         [rtac (impI RS allI) 1,
```
```   657          DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
```
```   658          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
```
```   659          fold_goals_tac rec_sets_defs,
```
```   660          (*This CollectE and disjE separates out the introduction rules*)
```
```   661          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
```
```   662          (*Now break down the individual cases.  No disjE here in case
```
```   663            some premise involves disjunction.*)
```
```   664          REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
```
```   665          rewrite_goals_tac sum_case_rewrites,
```
```   666          EVERY (map (fn prem =>
```
```   667            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
```
```   668
```
```   669     val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
```
```   670       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
```
```   671         [cut_facts_tac prems 1,
```
```   672          REPEAT (EVERY
```
```   673            [REPEAT (resolve_tac [conjI, impI] 1),
```
```   674             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
```
```   675             rewrite_goals_tac sum_case_rewrites,
```
```   676             atac 1])])
```
```   677
```
```   678   in standard (split_rule factors (induct RS lemma)) end;
```
```   679
```
```   680
```
```   681
```
```   682 (** specification of (co)inductive sets **)
```
```   683
```
```   684 fun cond_declare_consts declare_consts cs paramTs cnames =
```
```   685   if declare_consts then
```
```   686     Theory.add_consts_i (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
```
```   687   else I;
```
```   688
```
```   689 fun mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
```
```   690       params paramTs cTs cnames =
```
```   691   let
```
```   692     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
```
```   693     val setT = HOLogic.mk_setT sumT;
```
```   694
```
```   695     val fp_name = if coind then gfp_name else lfp_name;
```
```   696
```
```   697     val used = foldr add_term_names (intr_ts, []);
```
```   698     val [sname, xname] = variantlist (["S", "x"], used);
```
```   699
```
```   700     (* transform an introduction rule into a conjunction  *)
```
```   701     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
```
```   702     (* is transformed into                                *)
```
```   703     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
```
```   704
```
```   705     fun transform_rule r =
```
```   706       let
```
```   707         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
```
```   708         val subst = subst_free
```
```   709           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
```
```   710         val Const ("op :", _) \$ t \$ u =
```
```   711           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
```
```   712
```
```   713       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
```
```   714         (frees, foldr1 HOLogic.mk_conj
```
```   715           (((HOLogic.eq_const sumT) \$ Free (xname, sumT) \$ (mk_inj cs sumT u t))::
```
```   716             (map (subst o HOLogic.dest_Trueprop)
```
```   717               (Logic.strip_imp_prems r))))
```
```   718       end
```
```   719
```
```   720     (* make a disjunction of all introduction rules *)
```
```   721
```
```   722     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) \$
```
```   723       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
```
```   724
```
```   725     (* add definiton of recursive sets to theory *)
```
```   726
```
```   727     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
```
```   728     val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
```
```   729
```
```   730     val rec_const = list_comb
```
```   731       (Const (full_rec_name, paramTs ---> setT), params);
```
```   732
```
```   733     val fp_def_term = Logic.mk_equals (rec_const,
```
```   734       Const (fp_name, (setT --> setT) --> setT) \$ fp_fun);
```
```   735
```
```   736     val def_terms = fp_def_term :: (if length cs < 2 then [] else
```
```   737       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
```
```   738
```
```   739     val (thy', [fp_def :: rec_sets_defs]) =
```
```   740       thy
```
```   741       |> cond_declare_consts declare_consts cs paramTs cnames
```
```   742       |> (if length cs < 2 then I
```
```   743           else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
```
```   744       |> Theory.add_path rec_name
```
```   745       |> PureThy.add_defss_i false [(("defs", def_terms), [])];
```
```   746
```
```   747     val mono = prove_mono setT fp_fun monos thy'
```
```   748
```
```   749   in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
```
```   750
```
```   751 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
```
```   752     intros monos thy params paramTs cTs cnames induct_cases =
```
```   753   let
```
```   754     val _ =
```
```   755       if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
```
```   756         commas_quote cnames) else ();
```
```   757
```
```   758     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
```
```   759
```
```   760     val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) =
```
```   761       mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
```
```   762         params paramTs cTs cnames;
```
```   763
```
```   764     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts rec_sets_defs thy1;
```
```   765     val elims = if no_elim then [] else
```
```   766       prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy1;
```
```   767     val raw_induct = if no_ind then Drule.asm_rl else
```
```   768       if coind then standard (rule_by_tactic
```
```   769         (rewrite_tac [mk_meta_eq vimage_Un] THEN
```
```   770           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
```
```   771       else
```
```   772         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
```
```   773           rec_sets_defs thy1;
```
```   774     val induct =
```
```   775       if coind orelse no_ind orelse length cs > 1 then (raw_induct, [RuleCases.consumes 0])
```
```   776       else (raw_induct RSN (2, rev_mp), [RuleCases.consumes 1]);
```
```   777
```
```   778     val (thy2, intrs') =
```
```   779       thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
```
```   780     val (thy3, ([intrs'', elims'], [induct'])) =
```
```   781       thy2
```
```   782       |> PureThy.add_thmss
```
```   783         [(("intros", intrs'), []),
```
```   784           (("elims", elims), [RuleCases.consumes 1])]
```
```   785       |>>> PureThy.add_thms
```
```   786         [((coind_prefix coind ^ "induct", rulify (#1 induct)),
```
```   787          (RuleCases.case_names induct_cases :: #2 induct))]
```
```   788       |>> Theory.parent_path;
```
```   789   in (thy3,
```
```   790     {defs = fp_def :: rec_sets_defs,
```
```   791      mono = mono,
```
```   792      unfold = unfold,
```
```   793      intrs = intrs'',
```
```   794      elims = elims',
```
```   795      mk_cases = mk_cases elims',
```
```   796      raw_induct = rulify raw_induct,
```
```   797      induct = induct'})
```
```   798   end;
```
```   799
```
```   800
```
```   801 (* external interfaces *)
```
```   802
```
```   803 fun try_term f msg sign t =
```
```   804   (case Library.try f t of
```
```   805     Some x => x
```
```   806   | None => error (msg ^ Sign.string_of_term sign t));
```
```   807
```
```   808 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy =
```
```   809   let
```
```   810     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
```
```   811     val sign = Theory.sign_of thy;
```
```   812
```
```   813     (*parameters should agree for all mutually recursive components*)
```
```   814     val (_, params) = strip_comb (hd cs);
```
```   815     val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\
```
```   816       \ component is not a free variable: " sign) params;
```
```   817
```
```   818     val cTs = map (try_term (HOLogic.dest_setT o fastype_of)
```
```   819       "Recursive component not of type set: " sign) cs;
```
```   820
```
```   821     val full_cnames = map (try_term (fst o dest_Const o head_of)
```
```   822       "Recursive set not previously declared as constant: " sign) cs;
```
```   823     val cnames = map Sign.base_name full_cnames;
```
```   824
```
```   825     val save_sign =
```
```   826       thy |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames |> Theory.sign_of;
```
```   827     val intros = map (check_rule save_sign cs) pre_intros;
```
```   828     val induct_cases = map (#1 o #1) intros;
```
```   829
```
```   830     val (thy1, result as {elims, induct, ...}) =
```
```   831       add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos
```
```   832         thy params paramTs cTs cnames induct_cases;
```
```   833     val thy2 = thy1
```
```   834       |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
```
```   835       |> add_cases_induct no_elim (no_ind orelse coind orelse length cs > 1)
```
```   836           full_cnames elims induct;
```
```   837   in (thy2, result) end;
```
```   838
```
```   839 fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =
```
```   840   let
```
```   841     val sign = Theory.sign_of thy;
```
```   842     val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
```
```   843
```
```   844     val intr_names = map (fst o fst) intro_srcs;
```
```   845     fun read_rule s = Thm.read_cterm sign (s, propT)
```
```   846       handle ERROR => error ("The error(s) above occurred for " ^ s);
```
```   847     val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
```
```   848     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
```
```   849     val (cs', intr_ts') = unify_consts sign cs intr_ts;
```
```   850
```
```   851     val (thy', monos) = thy |> IsarThy.apply_theorems raw_monos;
```
```   852   in
```
```   853     add_inductive_i verbose false "" coind false false cs'
```
```   854       ((intr_names ~~ intr_ts') ~~ intr_atts) monos thy'
```
```   855   end;
```
```   856
```
```   857
```
```   858
```
```   859 (** package setup **)
```
```   860
```
```   861 (* setup theory *)
```
```   862
```
```   863 val setup =
```
```   864  [InductiveData.init,
```
```   865   Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
```
```   866     "dynamic case analysis on sets")],
```
```   867   Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
```
```   868
```
```   869
```
```   870 (* outer syntax *)
```
```   871
```
```   872 local structure P = OuterParse and K = OuterSyntax.Keyword in
```
```   873
```
```   874 fun mk_ind coind ((sets, intrs), monos) =
```
```   875   #1 o add_inductive true coind sets (map P.triple_swap intrs) monos;
```
```   876
```
```   877 fun ind_decl coind =
```
```   878   (Scan.repeat1 P.term --| P.marg_comment) --
```
```   879   (P.\$\$\$ "intros" |--
```
```   880     P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
```
```   881   Scan.optional (P.\$\$\$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) []
```
```   882   >> (Toplevel.theory o mk_ind coind);
```
```   883
```
```   884 val inductiveP =
```
```   885   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
```
```   886
```
```   887 val coinductiveP =
```
```   888   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
```
```   889
```
```   890
```
```   891 val ind_cases =
```
```   892   P.opt_thm_name ":" -- Scan.repeat1 P.prop -- P.marg_comment
```
```   893   >> (Toplevel.theory o inductive_cases);
```
```   894
```
```   895 val inductive_casesP =
```
```   896   OuterSyntax.command "inductive_cases"
```
```   897     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
```
```   898
```
```   899 val _ = OuterSyntax.add_keywords ["intros", "monos"];
```
```   900 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
```
```   901
```
```   902 end;
```
```   903
```
```   904 end;
```