src/HOL/Tools/inductive_package.ML
author berghofe
Wed Jul 15 18:26:15 1998 +0200 (1998-07-15)
changeset 5149 10f0be29c0d1
parent 5120 f7f5442c934a
child 5179 819f90f278db
permissions -rw-r--r--
Fixed bug in transform_rule.
     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, 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  *)
   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 Nat.thy addsimps simps),
   292                  elim_tac,
   293                  REPEAT o bound_hyp_subst_tac])
   294      THEN prune_params_tac
   295   end;
   296 
   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;
   306 
   307 (**************************** prove induction rule ****************************)
   308 
   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...";
   313 
   314     val sign = sign_of thy;
   315 
   316     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   317 
   318     (* make predicate for instantiation of abstract induction rule *)
   319 
   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;
   328 
   329     val ind_pred = mk_ind_pred sumT preds;
   330 
   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)));
   334 
   335     (* simplification rules for vimage and Collect *)
   336 
   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 mk_meta_eq [sum_case_Inl, sum_case_Inr]),
   345           rtac refl 1])) cs;
   346 
   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 mk_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 mk_meta_eq [sum_case_Inl, sum_case_Inr]),
   360          EVERY (map (fn prem =>
   361            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
   362 
   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 mk_meta_eq [sum_case_Inl, sum_case_Inr]),
   370             atac 1])])
   371 
   372   in standard (split_rule (induct RS lemma))
   373   end;
   374 
   375 (*************** definitional introduction of (co)inductive sets **************)
   376 
   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 ();
   382 
   383     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
   384     val setT = HOLogic.mk_setT sumT;
   385 
   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";
   388 
   389     val used = foldr add_term_names (intr_ts, []);
   390     val [sname, xname] = variantlist (["S", "x"], used);
   391 
   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 ... & ...      *)
   396 
   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)
   404 
   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
   411 
   412     (* make a disjunction of all introduction rules *)
   413 
   414     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
   415       absfree (xname, sumT, foldr1 (app HOLogic.disj) (map transform_rule intr_ts)));
   416 
   417     (* add definiton of recursive sets to theory *)
   418 
   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;
   421 
   422     val rec_const = list_comb
   423       (Const (full_rec_name, paramTs ---> setT), params);
   424 
   425     val fp_def_term = Logic.mk_equals (rec_const,
   426       Const (fp_name, (setT --> setT) --> setT) $ fp_fun)
   427 
   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);
   430 
   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), [])];
   440 
   441     (* get definitions from theory *)
   442 
   443     val fp_def::rec_sets_defs = get_thms thy' "defs";
   444 
   445     (* prove and store theorems *)
   446 
   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 [mk_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));
   461 
   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;
   470 
   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;
   481 
   482 (***************** axiomatic introduction of (co)inductive sets ***************)
   483 
   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 ();
   489 
   490     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
   491 
   492     val elim_ts = mk_elims cs cTs params intr_ts;
   493 
   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);
   496     
   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), [])]);
   506 
   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));
   513 
   514     val thy'' = thy' |>
   515       (if coind then I
   516        else PureThy.add_tthms [(("induct", Attribute.tthm_of induct), [])]) |>
   517       Theory.parent_path
   518 
   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;
   529 
   530 (********************** introduction of (co)inductive sets ********************)
   531 
   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");
   537 
   538     val sign = sign_of thy;
   539 
   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;
   544 
   545     val cTs = map (try' (HOLogic.dest_setT o fastype_of)
   546       "Recursive component not of type set: " sign) cs;
   547 
   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;
   550 
   551     val _ = assert_all Syntax.is_identifier cnames
   552        (fn a => "Base name of recursive set not an identifier: " ^ a);
   553 
   554     val _ = map (check_rule sign cs) intr_ts;
   555 
   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;
   561 
   562 (***************************** external interface *****************************)
   563 
   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;
   569 
   570     (* the following code ensures that each recursive set *)
   571     (* always has the same type in all introduction rules *)
   572 
   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';
   597 
   598   in add_inductive_i verbose false "" coind false false cs'' intr_ts''
   599     monos con_defs thy
   600   end;
   601 
   602 end;