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