src/HOL/Tools/inductive_package.ML
 author oheimb Wed Aug 12 16:20:49 1998 +0200 (1998-08-12) changeset 5303 22029546d109 parent 5179 819f90f278db child 5553 ae42b36a50c2 permissions -rw-r--r--
renamed mk_meta_eq to meta_eq
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, 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  *)
288 fun con_elim_tac simps =
289   let val elim_tac = REPEAT o (eresolve_tac elim_rls)
290   in ALLGOALS(EVERY'[elim_tac,
291                  asm_full_simp_tac (simpset_of NatDef.thy addsimps simps),
292                  elim_tac,
293                  REPEAT o bound_hyp_subst_tac])
294      THEN prune_params_tac
295   end;
297 (*String s should have the form t:Si where Si is an inductive set*)
298 fun mk_cases elims simps s =
299   let val prem = assume (read_cterm (sign_of_thm (hd elims)) (s, propT));
300       val elims' = map (try (fn r =>
301         rule_by_tactic (con_elim_tac simps) (prem RS r) |> standard)) elims
302   in case find_first is_some elims' of
303        Some (Some r) => r
304      | None => error ("mk_cases: string '" ^ s ^ "' not of form 't : S_i'")
305   end;
307 (**************************** prove induction rule ****************************)
309 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
310     fp_def rec_sets_defs thy =
311   let
312     val _ = writeln "  Proving the induction rule...";
314     val sign = sign_of thy;
316     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
318     (* make predicate for instantiation of abstract induction rule *)
320     fun mk_ind_pred _ [P] = P
321       | mk_ind_pred T Ps =
322          let val n = (length Ps) div 2;
323              val Type (_, [T1, T2]) = T
324          in Const ("sum_case",
325            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) \$
326              mk_ind_pred T1 (take (n, Ps)) \$ mk_ind_pred T2 (drop (n, Ps))
327          end;
329     val ind_pred = mk_ind_pred sumT preds;
331     val ind_concl = HOLogic.mk_Trueprop
332       (HOLogic.all_const sumT \$ Abs ("x", sumT, HOLogic.mk_binop "op -->"
333         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred \$ Bound 0)));
335     (* simplification rules for vimage and Collect *)
337     val vimage_simps = if length cs < 2 then [] else
338       map (fn c => prove_goalw_cterm [] (cterm_of sign
339         (HOLogic.mk_Trueprop (HOLogic.mk_eq
340           (mk_vimage cs sumT (HOLogic.Collect_const sumT \$ ind_pred) c,
341            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) \$
342              nth_elem (find_index_eq c cs, preds)))))
343         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac
344            (map meta_eq [sum_case_Inl, sum_case_Inr]),
345           rtac refl 1])) cs;
347     val induct = prove_goalw_cterm [] (cterm_of sign
348       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
349         [rtac (impI RS allI) 1,
350          DETERM (etac (mono RS (fp_def RS def_induct)) 1),
351          rewrite_goals_tac (map meta_eq (vimage_Int::vimage_simps)),
352          fold_goals_tac rec_sets_defs,
353          (*This CollectE and disjE separates out the introduction rules*)
354          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
355          (*Now break down the individual cases.  No disjE here in case
356            some premise involves disjunction.*)
357          REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE]
358                      ORELSE' hyp_subst_tac)),
359          rewrite_goals_tac (map meta_eq [sum_case_Inl, sum_case_Inr]),
360          EVERY (map (fn prem =>
361            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
363     val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
364       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
365         [cut_facts_tac prems 1,
366          REPEAT (EVERY
367            [REPEAT (resolve_tac [conjI, impI] 1),
368             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
369             rewrite_goals_tac (map meta_eq [sum_case_Inl, sum_case_Inr]),
370             atac 1])])
372   in standard (split_rule (induct RS lemma))
373   end;
375 (*************** definitional introduction of (co)inductive sets **************)
377 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
378     intr_ts monos con_defs thy params paramTs cTs cnames =
379   let
380     val _ = if verbose then writeln ("Proofs for " ^
381       (if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else ();
383     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
384     val setT = HOLogic.mk_setT sumT;
386     val fp_name = if coind then Sign.intern_const (sign_of Gfp.thy) "gfp"
387       else Sign.intern_const (sign_of Lfp.thy) "lfp";
389     val used = foldr add_term_names (intr_ts, []);
390     val [sname, xname] = variantlist (["S", "x"], used);
392     (* transform an introduction rule into a conjunction  *)
393     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
394     (* is transformed into                                *)
395     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
397     fun transform_rule r =
398       let
399         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
400         val subst = subst_free
401           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
402         val Const ("op :", _) \$ t \$ u =
403           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
405       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
406         (frees, foldr1 (app HOLogic.conj)
407           (((HOLogic.eq_const sumT) \$ Free (xname, sumT) \$ (mk_inj cs sumT u t))::
408             (map (subst o HOLogic.dest_Trueprop)
409               (Logic.strip_imp_prems r))))
410       end
412     (* make a disjunction of all introduction rules *)
414     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) \$
415       absfree (xname, sumT, foldr1 (app HOLogic.disj) (map transform_rule intr_ts)));
417     (* add definiton of recursive sets to theory *)
419     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
420     val full_rec_name = Sign.full_name (sign_of thy) rec_name;
422     val rec_const = list_comb
423       (Const (full_rec_name, paramTs ---> setT), params);
425     val fp_def_term = Logic.mk_equals (rec_const,
426       Const (fp_name, (setT --> setT) --> setT) \$ fp_fun)
428     val def_terms = fp_def_term :: (if length cs < 2 then [] else
429       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
431     val thy' = thy |>
432       (if declare_consts then
433         Theory.add_consts_i (map (fn (c, n) =>
434           (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
435        else I) |>
436       (if length cs < 2 then I else
437        Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)]) |>
438       Theory.add_path rec_name |>
439       PureThy.add_defss_i [(("defs", def_terms), [])];
441     (* get definitions from theory *)
443     val fp_def::rec_sets_defs = get_thms thy' "defs";
445     (* prove and store theorems *)
447     val mono = prove_mono setT fp_fun monos thy';
448     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
449       rec_sets_defs thy';
450     val elims = if no_elim then [] else
451       prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';
452     val raw_induct = if no_ind then TrueI else
453       if coind then standard (rule_by_tactic
454         (rewrite_tac [meta_eq vimage_Un] THEN
455           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
456       else
457         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
458           rec_sets_defs thy';
459     val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
460       else standard (raw_induct RSN (2, rev_mp));
462     val thy'' = thy' |>
463       PureThy.add_tthmss [(("intrs", map Attribute.tthm_of intrs), [])] |>
464       (if no_elim then I else PureThy.add_tthmss
465         [(("elims", map Attribute.tthm_of elims), [])]) |>
466       (if no_ind then I else PureThy.add_tthms
467         [(((if coind then "co" else "") ^ "induct",
468           Attribute.tthm_of induct), [])]) |>
469       Theory.parent_path;
471   in (thy'',
472     {defs = fp_def::rec_sets_defs,
473      mono = mono,
474      unfold = unfold,
475      intrs = intrs,
476      elims = elims,
477      mk_cases = mk_cases elims,
478      raw_induct = raw_induct,
479      induct = induct})
480   end;
482 (***************** axiomatic introduction of (co)inductive sets ***************)
484 fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
485     intr_ts monos con_defs thy params paramTs cTs cnames =
486   let
487     val _ = if verbose then writeln ("Adding axioms for " ^
488       (if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else ();
490     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
492     val elim_ts = mk_elims cs cTs params intr_ts;
494     val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
495     val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
497     val thy' = thy |>
498       (if declare_consts then
499         Theory.add_consts_i (map (fn (c, n) =>
500           (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
501        else I) |>
502       Theory.add_path rec_name |>
503       PureThy.add_axiomss_i [(("intrs", intr_ts), []), (("elims", elim_ts), [])] |>
504       (if coind then I
505        else PureThy.add_axioms_i [(("internal_induct", ind_t), [])]);
507     val intrs = get_thms thy' "intrs";
508     val elims = get_thms thy' "elims";
509     val raw_induct = if coind then TrueI else
510       standard (split_rule (get_thm thy' "internal_induct"));
511     val induct = if coind orelse length cs > 1 then raw_induct
512       else standard (raw_induct RSN (2, rev_mp));
514     val thy'' = thy' |>
515       (if coind then I
516        else PureThy.add_tthms [(("induct", Attribute.tthm_of induct), [])]) |>
517       Theory.parent_path
519   in (thy'',
520     {defs = [],
521      mono = TrueI,
522      unfold = TrueI,
523      intrs = intrs,
524      elims = elims,
525      mk_cases = mk_cases elims,
526      raw_induct = raw_induct,
527      induct = induct})
528   end;
530 (********************** introduction of (co)inductive sets ********************)
532 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
533     intr_ts monos con_defs thy =
534   let
535     val _ = Theory.requires thy "Inductive"
536       ((if coind then "co" else "") ^ "inductive definitions");
538     val sign = sign_of thy;
540     (*parameters should agree for all mutually recursive components*)
541     val (_, params) = strip_comb (hd cs);
542     val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\
543       \ component is not a free variable: " sign) params;
545     val cTs = map (try' (HOLogic.dest_setT o fastype_of)
546       "Recursive component not of type set: " sign) cs;
548     val cnames = map (try' (Sign.base_name o fst o dest_Const o head_of)
549       "Recursive set not previously declared as constant: " sign) cs;
551     val _ = assert_all Syntax.is_identifier cnames
552        (fn a => "Base name of recursive set not an identifier: " ^ a);
554     val _ = map (check_rule sign cs) intr_ts;
556   in
557     (if !quick_and_dirty then add_ind_axm else add_ind_def)
558       verbose declare_consts alt_name coind no_elim no_ind cs intr_ts monos
559         con_defs thy params paramTs cTs cnames
560   end;
562 (***************************** external interface *****************************)
564 fun add_inductive verbose coind c_strings intr_strings monos con_defs thy =
565   let
566     val sign = sign_of thy;
567     val cs = map (readtm (sign_of thy) HOLogic.termTVar) c_strings;
568     val intr_ts = map (readtm (sign_of thy) propT) intr_strings;
570     (* the following code ensures that each recursive set *)
571     (* always has the same type in all introduction rules *)
573     val {tsig, ...} = Sign.rep_sg sign;
574     val add_term_consts_2 =
575       foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
576     fun varify (t, (i, ts)) =
577       let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
578       in (maxidx_of_term t', t'::ts) end;
579     val (i, cs') = foldr varify (cs, (~1, []));
580     val (i', intr_ts') = foldr varify (intr_ts, (i, []));
581     val rec_consts = foldl add_term_consts_2 ([], cs');
582     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
583     fun unify (env, (cname, cT)) =
584       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
585       in (foldl (fn ((env', j'), Tp) => Type.unify tsig j' env' Tp)
586         (env, (replicate (length consts) cT) ~~ consts)) handle _ =>
587           error ("Occurrences of constant '" ^ cname ^
588             "' have incompatible types")
589       end;
590     val (env, _) = foldl unify (([], i'), rec_consts);
591     fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T
592       in if T = T' then T else typ_subst_TVars_2 env T' end;
593     val subst = fst o Type.freeze_thaw o
594       (map_term_types (typ_subst_TVars_2 env));
595     val cs'' = map subst cs';
596     val intr_ts'' = map subst intr_ts';
598   in add_inductive_i verbose false "" coind false false cs'' intr_ts''
599     monos con_defs thy
600   end;
602 end;