src/HOL/Tools/inductive_package.ML
 author berghofe Tue Jun 30 20:39:43 1998 +0200 (1998-06-30) changeset 5094 ddcc3c114a0e child 5108 4074c7d86d44 permissions -rw-r--r--
New inductive definition package
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
8 (Co)Inductive Definition module for HOL
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
17 The recursive sets must *already* be declared as constants in parent theory!
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
26 Sums are used only for mutual recursion;
27 Products are used only to derive "streamlined" induction rules for relations
28 *)
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;
46 structure InductivePackage : INDUCTIVE_PACKAGE =
47 struct
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];
53 val Const _ \$ (vimage_f \$ _) \$ _ = HOLogic.dest_Trueprop (concl_of vimageD);
55 (*Delete needless equality assumptions*)
56 val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
57      (fn _ => [assume_tac 1]);
59 (*For simplifying the elimination rule*)
60 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, disjE, Pair_inject];
62 val vimage_name = Sign.intern_const (sign_of Vimage.thy) "op -``";
63 val mono_name = Sign.intern_const (sign_of Ord.thy) "mono";
65 (* make injections needed in mutually recursive definitions *)
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;
82 (* make "vimage" terms for selecting out components of mutually rec.def. *)
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;
93 (**************************** well-formedness checks **************************)
95 fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^
96   (Sign.string_of_term sign t) ^ "\n" ^ msg);
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);
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";
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 ()
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;
126 fun try' f msg sign t = (f t) handle _ => error (msg ^ Sign.string_of_term sign t);
128 (*********************** properties of (co)inductive sets *********************)
130 (***************************** elimination rules ******************************)
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));
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;
143     val intrs = map dest_intr intr_ts;
145     fun mk_elim (c, T) =
146       let
147         val a = Free (aname, T);
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;
160 (***************** premises and conclusions of induction rules ****************)
162 fun mk_indrule cs cTs params intr_ts =
163   let
164     val used = foldr add_term_names (intr_ts, []);
166     (* predicates for induction rule *)
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);
172     (* transform an introduction rule into a premise for induction rule *)
174     fun mk_ind_prem r =
175       let
176         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
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;
187         val Const ("op :", _) \$ t \$ u =
188           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
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;
196     val ind_prems = map mk_ind_prem intr_ts;
198     (* make conclusions for induction rules *)
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;
210     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 (app HOLogic.conj)
211         (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
213   in (preds, ind_prems, mutual_ind_concl)
214   end;
216 (********************** proofs for (co)inductive sets *************************)
218 (**************************** prove monotonicity ******************************)
220 fun prove_mono setT fp_fun monos thy =
221   let
222     val _ = writeln "  Proving monotonicity...";
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)])
228   in mono end;
230 (************************* prove introduction rules ***************************)
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...";
236     val unfold = standard (mono RS (fp_def RS
237       (if coind then def_gfp_Tarski else def_lfp_Tarski)));
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));
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)
258   in (intrs, unfold) end;
260 (*************************** prove elimination rules **************************)
262 fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =
263   let
264     val _ = writeln "  Proving the elimination rules...";
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];
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)
280   in elims end;
282 (** derivation of simplified elimination rules **)
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;
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;
308 (**************************** prove induction rule ****************************)
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...";
315     val sign = sign_of thy;
317     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
319     (* make predicate for instantiation of abstract induction rule *)
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;
330     val ind_pred = mk_ind_pred sumT preds;
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)));
336     (* simplification rules for vimage and Collect *)
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;
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)]);
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])])
373   in standard (split_rule (induct RS lemma))
374   end;
376 (*************** definitional introduction of (co)inductive sets **************)
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 ();
384     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
385     val setT = HOLogic.mk_setT sumT;
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";
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 ... & ...      *)
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)
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
410     (* make a disjunction of all introduction rules *)
412     val fp_fun = Abs ("S", setT, (HOLogic.Collect_const sumT) \$
413       Abs ("x", sumT, foldr1 (app HOLogic.disj) (map transform_rule intr_ts)));
415     (* add definiton of recursive sets to theory *)
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;
420     val rec_const = list_comb
421       (Const (full_rec_name, paramTs ---> setT), params);
423     val fp_def_term = Logic.mk_equals (rec_const,
424       Const (fp_name, (setT --> setT) --> setT) \$ fp_fun)
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);
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), [])];
439     (* get definitions from theory *)
441     val fp_def::rec_sets_defs = get_thms thy' "defs";
443     (* prove and store theorems *)
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 length cs > 1 then raw_induct
458       else standard (raw_induct RSN (2, rev_mp));
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;
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;
480 (***************** axiomatic introduction of (co)inductive sets ***************)
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 ();
488     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
490     val elim_ts = mk_elims cs cTs params intr_ts;
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);
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), [])]);
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));
512     val thy'' = thy' |>
513       (if coind then I
514        else PureThy.add_tthms [(("induct", Attribute.tthm_of induct), [])]) |>
515       Theory.parent_path
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;
528 (********************** introduction of (co)inductive sets ********************)
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");
536     val sign = sign_of thy;
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;
543     val cTs = map (try' (HOLogic.dest_setT o fastype_of)
544       "Recursive component not of type set: " sign) cs;
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;
549     val _ = assert_all Syntax.is_identifier cnames
550        (fn a => "Base name of recursive set not an identifier: " ^ a);
552     val _ = map (check_rule sign cs) intr_ts;
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;
560 (***************************** external interface *****************************)
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;
568     (* the following code ensures that each recursive set *)
569     (* always has the same type in all introduction rules *)
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';
596   in add_inductive_i verbose false "" coind false false cs'' intr_ts''
597     monos con_defs thy
598   end;
600 end;