src/HOL/Tools/inductive_package.ML
author berghofe
Wed Jul 01 19:03:54 1998 +0200 (1998-07-01)
changeset 5108 4074c7d86d44
parent 5094 ddcc3c114a0e
child 5120 f7f5442c934a
permissions -rw-r--r--
Fixed bug (improper handling of flag no_ind).
     1 (*  Title:      HOL/Tools/inductive_package.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4                 Stefan Berghofer,   TU Muenchen
     5     Copyright   1994  University of Cambridge
     6                 1998  TU Muenchen     
     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 parent theory!
    18 
    19   Introduction rules have the form
    20   [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
    21   where M is some monotone operator (usually the identity)
    22   P(x) is any side condition on the free variables
    23   ti, t are any terms
    24   Sj, Sk are two of the sets being defined in mutual recursion
    25 
    26 Sums are used only for mutual recursion;
    27 Products are used only to derive "streamlined" induction rules for relations
    28 *)
    29 
    30 signature INDUCTIVE_PACKAGE =
    31 sig
    32   val add_inductive_i : bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    33     term list -> thm list -> thm list -> theory -> theory *
    34       {defs:thm list, elims:thm list, raw_induct:thm, induct:thm,
    35        intrs:thm list,
    36        mk_cases:thm list -> string -> thm, mono:thm,
    37        unfold:thm}
    38   val add_inductive : bool -> bool -> string list -> string list
    39     -> thm list -> thm list -> theory -> theory *
    40       {defs:thm list, elims:thm list, raw_induct:thm, induct:thm,
    41        intrs:thm list,
    42        mk_cases:thm list -> string -> thm, mono:thm,
    43        unfold:thm}
    44 end;
    45 
    46 structure InductivePackage : INDUCTIVE_PACKAGE =
    47 struct
    48 
    49 (*For proving monotonicity of recursion operator*)
    50 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, 
    51                    ex_mono, Collect_mono, in_mono, vimage_mono];
    52 
    53 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD);
    54 
    55 (*Delete needless equality assumptions*)
    56 val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
    57      (fn _ => [assume_tac 1]);
    58 
    59 (*For simplifying the elimination rule*)
    60 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, disjE, Pair_inject];
    61 
    62 val vimage_name = Sign.intern_const (sign_of Vimage.thy) "op -``";
    63 val mono_name = Sign.intern_const (sign_of Ord.thy) "mono";
    64 
    65 (* make injections needed in mutually recursive definitions *)
    66 
    67 fun mk_inj cs sumT c x =
    68   let
    69     fun mk_inj' T n i =
    70       if n = 1 then x else
    71       let val n2 = n div 2;
    72           val Type (_, [T1, T2]) = T
    73       in
    74         if i <= n2 then
    75           Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i)
    76         else
    77           Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
    78       end
    79   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
    80   end;
    81 
    82 (* make "vimage" terms for selecting out components of mutually rec.def. *)
    83 
    84 fun mk_vimage cs sumT t c = if length cs < 2 then t else
    85   let
    86     val cT = HOLogic.dest_setT (fastype_of c);
    87     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
    88   in
    89     Const (vimage_name, vimageT) $
    90       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t
    91   end;
    92 
    93 (**************************** well-formedness checks **************************)
    94 
    95 fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^
    96   (Sign.string_of_term sign t) ^ "\n" ^ msg);
    97 
    98 fun err_in_prem sign t p msg = error ("Ill-formed premise\n" ^
    99   (Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^
   100   (Sign.string_of_term sign t) ^ "\n" ^ msg);
   101 
   102 val msg1 = "Conclusion of introduction rule must have form\
   103           \ ' t : S_i '";
   104 val msg2 = "Premises mentioning recursive sets must have form\
   105           \ ' t : M S_i '";
   106 val msg3 = "Recursion term on left of member symbol";
   107 
   108 fun check_rule sign cs r =
   109   let
   110     fun check_prem prem = if exists (Logic.occs o (rpair prem)) cs then
   111          (case prem of
   112            (Const ("op :", _) $ t $ u) =>
   113              if exists (Logic.occs o (rpair t)) cs then
   114                err_in_prem sign r prem msg3 else ()
   115          | _ => err_in_prem sign r prem msg2)
   116         else ()
   117 
   118   in (case (HOLogic.dest_Trueprop o Logic.strip_imp_concl) r of
   119         (Const ("op :", _) $ _ $ u) =>
   120           if u mem cs then map (check_prem o HOLogic.dest_Trueprop)
   121             (Logic.strip_imp_prems r)
   122           else err_in_rule sign r msg1
   123       | _ => err_in_rule sign r msg1)
   124   end;
   125 
   126 fun try' f msg sign t = (f t) handle _ => error (msg ^ Sign.string_of_term sign t);
   127 
   128 (*********************** properties of (co)inductive sets *********************)
   129 
   130 (***************************** elimination rules ******************************)
   131 
   132 fun mk_elims cs cTs params intr_ts =
   133   let
   134     val used = foldr add_term_names (intr_ts, []);
   135     val [aname, pname] = variantlist (["a", "P"], used);
   136     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
   137 
   138     fun dest_intr r =
   139       let val Const ("op :", _) $ t $ u =
   140         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   141       in (u, t, Logic.strip_imp_prems r) end;
   142 
   143     val intrs = map dest_intr intr_ts;
   144 
   145     fun mk_elim (c, T) =
   146       let
   147         val a = Free (aname, T);
   148 
   149         fun mk_elim_prem (_, t, ts) =
   150           list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
   151             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
   152       in
   153         Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
   154           map mk_elim_prem (filter (equal c o #1) intrs), P)
   155       end
   156   in
   157     map mk_elim (cs ~~ cTs)
   158   end;
   159         
   160 (***************** premises and conclusions of induction rules ****************)
   161 
   162 fun mk_indrule cs cTs params intr_ts =
   163   let
   164     val used = foldr add_term_names (intr_ts, []);
   165 
   166     (* predicates for induction rule *)
   167 
   168     val preds = map Free (variantlist (if length cs < 2 then ["P"] else
   169       map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
   170         map (fn T => T --> HOLogic.boolT) cTs);
   171 
   172     (* transform an introduction rule into a premise for induction rule *)
   173 
   174     fun mk_ind_prem r =
   175       let
   176         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   177 
   178         fun subst (prem as (Const ("op :", T) $ t $ u), prems) =
   179               let val n = find_index_eq u cs in
   180                 if n >= 0 then prem :: (nth_elem (n, preds)) $ t :: prems else
   181                   (subst_free (map (fn (c, P) => (c, HOLogic.mk_binop "op Int"
   182                     (c, HOLogic.Collect_const (HOLogic.dest_setT
   183                       (fastype_of c)) $ P))) (cs ~~ preds)) prem)::prems
   184               end
   185           | subst (prem, prems) = prem::prems;
   186 
   187         val Const ("op :", _) $ t $ u =
   188           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   189 
   190       in list_all_free (frees,
   191            Logic.list_implies (map HOLogic.mk_Trueprop (foldr subst
   192              (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
   193                HOLogic.mk_Trueprop (nth_elem (find_index_eq u cs, preds) $ t)))
   194       end;
   195 
   196     val ind_prems = map mk_ind_prem intr_ts;
   197 
   198     (* make conclusions for induction rules *)
   199 
   200     fun mk_ind_concl ((c, P), (ts, x)) =
   201       let val T = HOLogic.dest_setT (fastype_of c);
   202           val Ts = HOLogic.prodT_factors T;
   203           val (frees, x') = foldr (fn (T', (fs, s)) =>
   204             ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
   205           val tuple = HOLogic.mk_tuple T frees;
   206       in ((HOLogic.mk_binop "op -->"
   207         (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
   208       end;
   209 
   210     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 (app HOLogic.conj)
   211         (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
   212 
   213   in (preds, ind_prems, mutual_ind_concl)
   214   end;
   215 
   216 (********************** proofs for (co)inductive sets *************************)
   217 
   218 (**************************** prove monotonicity ******************************)
   219 
   220 fun prove_mono setT fp_fun monos thy =
   221   let
   222     val _ = writeln "  Proving monotonicity...";
   223 
   224     val mono = prove_goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop
   225       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
   226         (fn _ => [rtac monoI 1, REPEAT (ares_tac (basic_monos @ monos) 1)])
   227 
   228   in mono end;
   229 
   230 (************************* prove introduction rules ***************************)
   231 
   232 fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
   233   let
   234     val _ = writeln "  Proving the introduction rules...";
   235 
   236     val unfold = standard (mono RS (fp_def RS
   237       (if coind then def_gfp_Tarski else def_lfp_Tarski)));
   238 
   239     fun select_disj 1 1 = []
   240       | select_disj _ 1 = [rtac disjI1]
   241       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
   242 
   243     val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
   244       (cterm_of (sign_of thy) intr) (fn prems =>
   245        [(*insert prems and underlying sets*)
   246        cut_facts_tac prems 1,
   247        stac unfold 1,
   248        REPEAT (resolve_tac [vimageI2, CollectI] 1),
   249        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
   250        EVERY1 (select_disj (length intr_ts) i),
   251        (*Not ares_tac, since refl must be tried before any equality assumptions;
   252          backtracking may occur if the premises have extra variables!*)
   253        DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
   254        (*Now solve the equations like Inl 0 = Inl ?b2*)
   255        rewrite_goals_tac con_defs,
   256        REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts)
   257 
   258   in (intrs, unfold) end;
   259 
   260 (*************************** prove elimination rules **************************)
   261 
   262 fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =
   263   let
   264     val _ = writeln "  Proving the elimination rules...";
   265 
   266     val rules1 = [CollectE, disjE, make_elim vimageD];
   267     val rules2 = [exE, conjE, Inl_neq_Inr, Inr_neq_Inl] @
   268       map make_elim [Inl_inject, Inr_inject];
   269 
   270     val elims = map (fn t => prove_goalw_cterm rec_sets_defs
   271       (cterm_of (sign_of thy) t) (fn prems =>
   272         [cut_facts_tac [hd prems] 1,
   273          dtac (unfold RS subst) 1,
   274          REPEAT (FIRSTGOAL (eresolve_tac rules1)),
   275          REPEAT (FIRSTGOAL (eresolve_tac rules2)),
   276          EVERY (map (fn prem =>
   277            DEPTH_SOLVE_1 (ares_tac (prem::[conjI]) 1)) (tl prems))]))
   278       (mk_elims cs cTs params intr_ts)
   279 
   280   in elims end;
   281 
   282 (** derivation of simplified elimination rules **)
   283 
   284 (*Applies freeness of the given constructors, which *must* be unfolded by
   285   the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   286   for inference systems.
   287   FIXME: proper handling of conjunctive / disjunctive side conditions?!
   288  *)
   289 fun con_elim_tac simps =
   290   let val elim_tac = REPEAT o (eresolve_tac elim_rls)
   291   in ALLGOALS(EVERY'[elim_tac,
   292                  asm_full_simp_tac (simpset_of Nat.thy addsimps simps),
   293                  elim_tac,
   294                  REPEAT o bound_hyp_subst_tac])
   295      THEN prune_params_tac
   296   end;
   297 
   298 (*String s should have the form t:Si where Si is an inductive set*)
   299 fun mk_cases elims defs s =
   300   let val prem = assume (read_cterm (sign_of_thm (hd elims)) (s, propT));
   301       val elims' = map (try (fn r =>
   302         rule_by_tactic (con_elim_tac defs) (prem RS r) |> standard)) elims
   303   in case find_first is_some elims' of
   304        Some (Some r) => r
   305      | None => error ("mk_cases: string '" ^ s ^ "' not of form 't : S_i'")
   306   end;
   307 
   308 (**************************** prove induction rule ****************************)
   309 
   310 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
   311     fp_def rec_sets_defs thy =
   312   let
   313     val _ = writeln "  Proving the induction rule...";
   314 
   315     val sign = sign_of thy;
   316 
   317     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   318 
   319     (* make predicate for instantiation of abstract induction rule *)
   320 
   321     fun mk_ind_pred _ [P] = P
   322       | mk_ind_pred T Ps =
   323          let val n = (length Ps) div 2;
   324              val Type (_, [T1, T2]) = T
   325          in Const ("sum_case",
   326            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
   327              mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
   328          end;
   329 
   330     val ind_pred = mk_ind_pred sumT preds;
   331 
   332     val ind_concl = HOLogic.mk_Trueprop
   333       (HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->"
   334         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0)));
   335 
   336     (* simplification rules for vimage and Collect *)
   337 
   338     val vimage_simps = if length cs < 2 then [] else
   339       map (fn c => prove_goalw_cterm [] (cterm_of sign
   340         (HOLogic.mk_Trueprop (HOLogic.mk_eq
   341           (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   342            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   343              nth_elem (find_index_eq c cs, preds)))))
   344         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac
   345            (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
   346           rtac refl 1])) cs;
   347 
   348     val induct = prove_goalw_cterm [] (cterm_of sign
   349       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   350         [rtac (impI RS allI) 1,
   351          DETERM (etac (mono RS (fp_def RS def_induct)) 1),
   352          rewrite_goals_tac (map mk_meta_eq (vimage_Int::vimage_simps)),
   353          fold_goals_tac rec_sets_defs,
   354          (*This CollectE and disjE separates out the introduction rules*)
   355          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
   356          (*Now break down the individual cases.  No disjE here in case
   357            some premise involves disjunction.*)
   358          REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE] 
   359                      ORELSE' hyp_subst_tac)),
   360          rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
   361          EVERY (map (fn prem =>
   362            DEPTH_SOLVE_1 (ares_tac (prem::[conjI, refl]) 1)) prems)]);
   363 
   364     val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
   365       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
   366         [cut_facts_tac prems 1,
   367          REPEAT (EVERY
   368            [REPEAT (resolve_tac [conjI, impI] 1),
   369             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
   370             rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
   371             atac 1])])
   372 
   373   in standard (split_rule (induct RS lemma))
   374   end;
   375 
   376 (*************** definitional introduction of (co)inductive sets **************)
   377 
   378 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   379     intr_ts monos con_defs thy params paramTs cTs cnames =
   380   let
   381     val _ = if verbose then writeln ("Proofs for " ^
   382       (if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else ();
   383 
   384     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
   385     val setT = HOLogic.mk_setT sumT;
   386 
   387     val fp_name = if coind then Sign.intern_const (sign_of Gfp.thy) "gfp"
   388       else Sign.intern_const (sign_of Lfp.thy) "lfp";
   389 
   390     (* transform an introduction rule into a conjunction  *)
   391     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
   392     (* is transformed into                                *)
   393     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
   394 
   395     fun transform_rule r =
   396       let
   397         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   398         val idx = length frees;
   399         val subst = subst_free (cs ~~ (map (mk_vimage cs sumT (Bound (idx + 1))) cs));
   400         val Const ("op :", _) $ t $ u =
   401           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   402 
   403       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
   404         (frees, foldr1 (app HOLogic.conj)
   405           (((HOLogic.eq_const sumT) $ Bound idx $ (mk_inj cs sumT u t))::
   406             (map (subst o HOLogic.dest_Trueprop)
   407               (Logic.strip_imp_prems r))))
   408       end
   409 
   410     (* make a disjunction of all introduction rules *)
   411 
   412     val fp_fun = Abs ("S", setT, (HOLogic.Collect_const sumT) $
   413       Abs ("x", sumT, foldr1 (app HOLogic.disj) (map transform_rule intr_ts)));
   414 
   415     (* add definiton of recursive sets to theory *)
   416 
   417     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
   418     val full_rec_name = Sign.full_name (sign_of thy) rec_name;
   419 
   420     val rec_const = list_comb
   421       (Const (full_rec_name, paramTs ---> setT), params);
   422 
   423     val fp_def_term = Logic.mk_equals (rec_const,
   424       Const (fp_name, (setT --> setT) --> setT) $ fp_fun)
   425 
   426     val def_terms = fp_def_term :: (if length cs < 2 then [] else
   427       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
   428 
   429     val thy' = thy |>
   430       (if declare_consts then
   431         Theory.add_consts_i (map (fn (c, n) =>
   432           (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   433        else I) |>
   434       (if length cs < 2 then I else
   435        Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)]) |>
   436       Theory.add_path rec_name |>
   437       PureThy.add_defss_i [(("defs", def_terms), [])];
   438 
   439     (* get definitions from theory *)
   440 
   441     val fp_def::rec_sets_defs = get_thms thy' "defs";
   442 
   443     (* prove and store theorems *)
   444 
   445     val mono = prove_mono setT fp_fun monos thy';
   446     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
   447       rec_sets_defs thy';
   448     val elims = if no_elim then [] else
   449       prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';
   450     val raw_induct = if no_ind then TrueI else
   451       if coind then standard (rule_by_tactic
   452         (rewrite_tac [mk_meta_eq vimage_Un] THEN
   453           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
   454       else
   455         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
   456           rec_sets_defs thy';
   457     val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
   458       else standard (raw_induct RSN (2, rev_mp));
   459 
   460     val thy'' = thy' |>
   461       PureThy.add_tthmss [(("intrs", map Attribute.tthm_of intrs), [])] |>
   462       (if no_elim then I else PureThy.add_tthmss
   463         [(("elims", map Attribute.tthm_of elims), [])]) |>
   464       (if no_ind then I else PureThy.add_tthms
   465         [(((if coind then "co" else "") ^ "induct",
   466           Attribute.tthm_of induct), [])]) |>
   467       Theory.parent_path;
   468 
   469   in (thy'',
   470     {defs = fp_def::rec_sets_defs,
   471      mono = mono,
   472      unfold = unfold,
   473      intrs = intrs,
   474      elims = elims,
   475      mk_cases = mk_cases elims,
   476      raw_induct = raw_induct,
   477      induct = induct})
   478   end;
   479 
   480 (***************** axiomatic introduction of (co)inductive sets ***************)
   481 
   482 fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
   483     intr_ts monos con_defs thy params paramTs cTs cnames =
   484   let
   485     val _ = if verbose then writeln ("Adding axioms for " ^
   486       (if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else ();
   487 
   488     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
   489 
   490     val elim_ts = mk_elims cs cTs params intr_ts;
   491 
   492     val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   493     val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
   494     
   495     val thy' = thy |>
   496       (if declare_consts then
   497         Theory.add_consts_i (map (fn (c, n) =>
   498           (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   499        else I) |>
   500       Theory.add_path rec_name |>
   501       PureThy.add_axiomss_i [(("intrs", intr_ts), []), (("elims", elim_ts), [])] |>
   502       (if coind then I
   503        else PureThy.add_axioms_i [(("internal_induct", ind_t), [])]);
   504 
   505     val intrs = get_thms thy' "intrs";
   506     val elims = get_thms thy' "elims";
   507     val raw_induct = if coind then TrueI else
   508       standard (split_rule (get_thm thy' "internal_induct"));
   509     val induct = if coind orelse length cs > 1 then raw_induct
   510       else standard (raw_induct RSN (2, rev_mp));
   511 
   512     val thy'' = thy' |>
   513       (if coind then I
   514        else PureThy.add_tthms [(("induct", Attribute.tthm_of induct), [])]) |>
   515       Theory.parent_path
   516 
   517   in (thy'',
   518     {defs = [],
   519      mono = TrueI,
   520      unfold = TrueI,
   521      intrs = intrs,
   522      elims = elims,
   523      mk_cases = mk_cases elims,
   524      raw_induct = raw_induct,
   525      induct = induct})
   526   end;
   527 
   528 (********************** introduction of (co)inductive sets ********************)
   529 
   530 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
   531     intr_ts monos con_defs thy =
   532   let
   533     val _ = Theory.requires thy "Inductive"
   534       ((if coind then "co" else "") ^ "inductive definitions");
   535 
   536     val sign = sign_of thy;
   537 
   538     (*parameters should agree for all mutually recursive components*)
   539     val (_, params) = strip_comb (hd cs);
   540     val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\
   541       \ component is not a free variable: " sign) params;
   542 
   543     val cTs = map (try' (HOLogic.dest_setT o fastype_of)
   544       "Recursive component not of type set: " sign) cs;
   545 
   546     val cnames = map (try' (Sign.base_name o fst o dest_Const o head_of)
   547       "Recursive set not previously declared as constant: " sign) cs;
   548 
   549     val _ = assert_all Syntax.is_identifier cnames
   550        (fn a => "Base name of recursive set not an identifier: " ^ a);
   551 
   552     val _ = map (check_rule sign cs) intr_ts;
   553 
   554   in
   555     (if !quick_and_dirty then add_ind_axm else add_ind_def)
   556       verbose declare_consts alt_name coind no_elim no_ind cs intr_ts monos
   557         con_defs thy params paramTs cTs cnames
   558   end;
   559 
   560 (***************************** external interface *****************************)
   561 
   562 fun add_inductive verbose coind c_strings intr_strings monos con_defs thy =
   563   let
   564     val sign = sign_of thy;
   565     val cs = map (readtm (sign_of thy) HOLogic.termTVar) c_strings;
   566     val intr_ts = map (readtm (sign_of thy) propT) intr_strings;
   567 
   568     (* the following code ensures that each recursive set *)
   569     (* always has the same type in all introduction rules *)
   570 
   571     val {tsig, ...} = Sign.rep_sg sign;
   572     val add_term_consts_2 =
   573       foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
   574     fun varify (t, (i, ts)) =
   575       let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
   576       in (maxidx_of_term t', t'::ts) end;
   577     val (i, cs') = foldr varify (cs, (~1, []));
   578     val (i', intr_ts') = foldr varify (intr_ts, (i, []));
   579     val rec_consts = foldl add_term_consts_2 ([], cs');
   580     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
   581     fun unify (env, (cname, cT)) =
   582       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
   583       in (foldl (fn ((env', j'), Tp) => Type.unify tsig j' env' Tp)
   584         (env, (replicate (length consts) cT) ~~ consts)) handle _ =>
   585           error ("Occurrences of constant '" ^ cname ^
   586             "' have incompatible types")
   587       end;
   588     val (env, _) = foldl unify (([], i'), rec_consts);
   589     fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T
   590       in if T = T' then T else typ_subst_TVars_2 env T' end;
   591     val subst = fst o Type.freeze_thaw o
   592       (map_term_types (typ_subst_TVars_2 env));
   593     val cs'' = map subst cs';
   594     val intr_ts'' = map subst intr_ts';
   595 
   596   in add_inductive_i verbose false "" coind false false cs'' intr_ts''
   597     monos con_defs thy
   598   end;
   599 
   600 end;