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