src/HOL/Tools/inductive_package.ML

Renamed sum_case to basic_sum_case.

(*  Title:      HOL/Tools/inductive_package.ML
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
                Stefan Berghofer,   TU Muenchen
    Copyright   1994  University of Cambridge
                1998  TU Muenchen     

(Co)Inductive Definition module for HOL.

Features:
  * least or greatest fixedpoints
  * user-specified product and sum constructions
  * mutually recursive definitions
  * definitions involving arbitrary monotone operators
  * automatically proves introduction and elimination rules

The recursive sets must *already* be declared as constants in the
current theory!

  Introduction rules have the form
  [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
  where M is some monotone operator (usually the identity)
  P(x) is any side condition on the free variables
  ti, t are any terms
  Sj, Sk are two of the sets being defined in mutual recursion

Sums are used only for mutual recursion.  Products are used only to
derive "streamlined" induction rules for relations.
*)

signature INDUCTIVE_PACKAGE =
sig
  val quiet_mode: bool ref
  val unify_consts: Sign.sg -> term list -> term list -> term list * term list
  val get_inductive: theory -> string ->
    {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
      induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
  val print_inductives: theory -> unit
  val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    theory attribute list -> ((bstring * term) * theory attribute list) list ->
      thm list -> thm list -> theory -> theory *
      {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
  val add_inductive: bool -> bool -> string list -> Args.src list ->
    ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
      (xstring * Args.src list) list -> theory -> theory *
      {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
       intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
  val inductive_cases: (((bstring * Args.src list) * xstring) * string list) * Comment.text
    -> theory -> theory
  val inductive_cases_i: (((bstring * theory attribute list) * string) * term list) * Comment.text
    -> theory -> theory
  val setup: (theory -> theory) list
end;

structure InductivePackage: INDUCTIVE_PACKAGE =
struct


(** utilities **)

(* messages *)

val quiet_mode = ref false;
fun message s = if !quiet_mode then () else writeln s;

fun coind_prefix true = "co"
  | coind_prefix false = "";


(* the following code ensures that each recursive set *)
(* always has the same type in all introduction rules *)

fun unify_consts sign cs intr_ts =
  (let
    val {tsig, ...} = Sign.rep_sg sign;
    val add_term_consts_2 =
      foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
    fun varify (t, (i, ts)) =
      let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
      in (maxidx_of_term t', t'::ts) end;
    val (i, cs') = foldr varify (cs, (~1, []));
    val (i', intr_ts') = foldr varify (intr_ts, (i, []));
    val rec_consts = foldl add_term_consts_2 ([], cs');
    val intr_consts = foldl add_term_consts_2 ([], intr_ts');
    fun unify (env, (cname, cT)) =
      let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
      in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
          (env, (replicate (length consts) cT) ~~ consts)
      end;
    val (env, _) = foldl unify (([], i'), rec_consts);
    fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T
      in if T = T' then T else typ_subst_TVars_2 env T' end;
    val subst = fst o Type.freeze_thaw o
      (map_term_types (typ_subst_TVars_2 env))

  in (map subst cs', map subst intr_ts')
  end) handle Type.TUNIFY =>
    (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));


(* misc *)

(*for proving monotonicity of recursion operator*)
val default_monos = basic_monos @ [vimage_mono];

val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD);

(*Delete needless equality assumptions*)
val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
     (fn _ => [assume_tac 1]);

(*For simplifying the elimination rule*)
val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];

val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``";
val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";

(* make injections needed in mutually recursive definitions *)

fun mk_inj cs sumT c x =
  let
    fun mk_inj' T n i =
      if n = 1 then x else
      let val n2 = n div 2;
          val Type (_, [T1, T2]) = T
      in
        if i <= n2 then
          Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i)
        else
          Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
      end
  in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
  end;

(* make "vimage" terms for selecting out components of mutually rec.def. *)

fun mk_vimage cs sumT t c = if length cs < 2 then t else
  let
    val cT = HOLogic.dest_setT (fastype_of c);
    val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
  in
    Const (vimage_name, vimageT) $
      Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t
  end;



(** well-formedness checks **)

fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^
  (Sign.string_of_term sign t) ^ "\n" ^ msg);

fun err_in_prem sign t p msg = error ("Ill-formed premise\n" ^
  (Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^
  (Sign.string_of_term sign t) ^ "\n" ^ msg);

val msg1 = "Conclusion of introduction rule must have form\
          \ ' t : S_i '";
val msg2 = "Premises mentioning recursive sets must have form\
          \ ' t : M S_i '";
val msg3 = "Recursion term on left of member symbol";

fun check_rule sign cs r =
  let
    fun check_prem prem = if exists (Logic.occs o (rpair prem)) cs then
         (case prem of
           (Const ("op :", _) $ t $ u) =>
             if exists (Logic.occs o (rpair t)) cs then
               err_in_prem sign r prem msg3 else ()
         | _ => err_in_prem sign r prem msg2)
        else ()

  in (case (HOLogic.dest_Trueprop o Logic.strip_imp_concl) r of
        (Const ("op :", _) $ _ $ u) =>
          if u mem cs then seq (check_prem o HOLogic.dest_Trueprop)
            (Logic.strip_imp_prems r)
          else err_in_rule sign r msg1
      | _ => err_in_rule sign r msg1)
  end;

fun try' f msg sign t = (case (try f t) of
      Some x => x
    | None => error (msg ^ Sign.string_of_term sign t));



(*** theory data ***)

(* data kind 'HOL/inductive' *)

type inductive_info =
  {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
    induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};

structure InductiveArgs =
struct
  val name = "HOL/inductive";
  type T = inductive_info Symtab.table;

  val empty = Symtab.empty;
  val copy = I;
  val prep_ext = I;
  val merge: T * T -> T = Symtab.merge (K true);

  fun print sg tab =
    Pretty.writeln (Pretty.strs ("(co)inductives:" ::
      map #1 (Sign.cond_extern_table sg Sign.constK tab)));
end;

structure InductiveData = TheoryDataFun(InductiveArgs);
val print_inductives = InductiveData.print;


(* get and put data *)

fun get_inductive thy name =
  (case Symtab.lookup (InductiveData.get thy, name) of
    Some info => info
  | None => error ("Unknown (co)inductive set " ^ quote name));

fun put_inductives names info thy =
  let
    fun upd (tab, name) = Symtab.update_new ((name, info), tab);
    val tab = foldl upd (InductiveData.get thy, names)
      handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
  in InductiveData.put tab thy end;



(*** properties of (co)inductive sets ***)

(** elimination rules **)

fun mk_elims cs cTs params intr_ts =
  let
    val used = foldr add_term_names (intr_ts, []);
    val [aname, pname] = variantlist (["a", "P"], used);
    val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));

    fun dest_intr r =
      let val Const ("op :", _) $ t $ u =
        HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
      in (u, t, Logic.strip_imp_prems r) end;

    val intrs = map dest_intr intr_ts;

    fun mk_elim (c, T) =
      let
        val a = Free (aname, T);

        fun mk_elim_prem (_, t, ts) =
          list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
            Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
      in
        Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
          map mk_elim_prem (filter (equal c o #1) intrs), P)
      end
  in
    map mk_elim (cs ~~ cTs)
  end;
        


(** premises and conclusions of induction rules **)

fun mk_indrule cs cTs params intr_ts =
  let
    val used = foldr add_term_names (intr_ts, []);

    (* predicates for induction rule *)

    val preds = map Free (variantlist (if length cs < 2 then ["P"] else
      map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
        map (fn T => T --> HOLogic.boolT) cTs);

    (* transform an introduction rule into a premise for induction rule *)

    fun mk_ind_prem r =
      let
        val frees = map dest_Free ((add_term_frees (r, [])) \\ params);

        fun subst (prem as (Const ("op :", T) $ t $ u), prems) =
              let val n = find_index_eq u cs in
                if n >= 0 then prem :: (nth_elem (n, preds)) $ t :: prems else
                  (subst_free (map (fn (c, P) => (c, HOLogic.mk_binop "op Int"
                    (c, HOLogic.Collect_const (HOLogic.dest_setT
                      (fastype_of c)) $ P))) (cs ~~ preds)) prem)::prems
              end
          | subst (prem, prems) = prem::prems;

        val Const ("op :", _) $ t $ u =
          HOLogic.dest_Trueprop (Logic.strip_imp_concl r)

      in list_all_free (frees,
           Logic.list_implies (map HOLogic.mk_Trueprop (foldr subst
             (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
               HOLogic.mk_Trueprop (nth_elem (find_index_eq u cs, preds) $ t)))
      end;

    val ind_prems = map mk_ind_prem intr_ts;

    (* make conclusions for induction rules *)

    fun mk_ind_concl ((c, P), (ts, x)) =
      let val T = HOLogic.dest_setT (fastype_of c);
          val Ts = HOLogic.prodT_factors T;
          val (frees, x') = foldr (fn (T', (fs, s)) =>
            ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
          val tuple = HOLogic.mk_tuple T frees;
      in ((HOLogic.mk_binop "op -->"
        (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
      end;

    val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 (app HOLogic.conj)
        (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))

  in (preds, ind_prems, mutual_ind_concl)
  end;



(*** proofs for (co)inductive sets ***)

(** prove monotonicity **)

fun prove_mono setT fp_fun monos thy =
  let
    val _ = message "  Proving monotonicity ...";

    val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
      (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
        (fn _ => [rtac monoI 1, REPEAT (ares_tac (default_monos @ monos) 1)])

  in mono end;



(** prove introduction rules **)

fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
  let
    val _ = message "  Proving the introduction rules ...";

    val unfold = standard (mono RS (fp_def RS
      (if coind then def_gfp_Tarski else def_lfp_Tarski)));

    fun select_disj 1 1 = []
      | select_disj _ 1 = [rtac disjI1]
      | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));

    val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
      (cterm_of (Theory.sign_of thy) intr) (fn prems =>
       [(*insert prems and underlying sets*)
       cut_facts_tac prems 1,
       stac unfold 1,
       REPEAT (resolve_tac [vimageI2, CollectI] 1),
       (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
       EVERY1 (select_disj (length intr_ts) i),
       (*Not ares_tac, since refl must be tried before any equality assumptions;
         backtracking may occur if the premises have extra variables!*)
       DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
       (*Now solve the equations like Inl 0 = Inl ?b2*)
       rewrite_goals_tac con_defs,
       REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts)

  in (intrs, unfold) end;



(** prove elimination rules **)

fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =
  let
    val _ = message "  Proving the elimination rules ...";

    val rules1 = [CollectE, disjE, make_elim vimageD];
    val rules2 = [exE, conjE, Inl_neq_Inr, Inr_neq_Inl] @
      map make_elim [Inl_inject, Inr_inject];

    val elims = map (fn t => prove_goalw_cterm rec_sets_defs
      (cterm_of (Theory.sign_of thy) t) (fn prems =>
        [cut_facts_tac [hd prems] 1,
         dtac (unfold RS subst) 1,
         REPEAT (FIRSTGOAL (eresolve_tac rules1)),
         REPEAT (FIRSTGOAL (eresolve_tac rules2)),
         EVERY (map (fn prem =>
           DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]))
      (mk_elims cs cTs params intr_ts)

  in elims end;


(** derivation of simplified elimination rules **)

(*Applies freeness of the given constructors, which *must* be unfolded by
  the given defs.  Cannot simply use the local con_defs because con_defs=[] 
  for inference systems.
 *)
fun con_elim_tac ss =
  let val elim_tac = REPEAT o (eresolve_tac elim_rls)
  in ALLGOALS(EVERY'[elim_tac,
		     asm_full_simp_tac ss,
		     elim_tac,
		     REPEAT o bound_hyp_subst_tac])
     THEN prune_params_tac
  end;

(*cprop should have the form t:Si where Si is an inductive set*)
fun mk_cases_i elims ss cprop =
  let
    val prem = Thm.assume cprop;
    fun mk_elim rl = standard (rule_by_tactic (con_elim_tac ss) (prem RS rl));
  in
    (case get_first (try mk_elim) elims of
      Some r => r
    | None => error (Pretty.string_of (Pretty.block
        [Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk,
          Display.pretty_cterm cprop])))
  end;

fun mk_cases elims s =
  mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));


(* inductive_cases(_i) *)

fun gen_inductive_cases prep_att prep_const prep_prop
    ((((name, raw_atts), raw_set), raw_props), comment) thy =
  let
    val sign = Theory.sign_of thy;

    val atts = map (prep_att thy) raw_atts;
    val (_, {elims, ...}) = get_inductive thy (prep_const sign raw_set);
    val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
    val thms = map (mk_cases_i elims (Simplifier.simpset_of thy)) cprops;
  in
    thy
    |> IsarThy.have_theorems_i (((name, atts), map Thm.no_attributes thms), comment)
  end;

val inductive_cases =
  gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;

val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop;



(** prove induction rule **)

fun prove_indrule cs cTs sumT rec_const params intr_ts mono
    fp_def rec_sets_defs thy =
  let
    val _ = message "  Proving the induction rule ...";

    val sign = Theory.sign_of thy;

    val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;

    (* make predicate for instantiation of abstract induction rule *)

    fun mk_ind_pred _ [P] = P
      | mk_ind_pred T Ps =
         let val n = (length Ps) div 2;
             val Type (_, [T1, T2]) = T
         in Const ("basic_sum_case",
           [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
             mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
         end;

    val ind_pred = mk_ind_pred sumT preds;

    val ind_concl = HOLogic.mk_Trueprop
      (HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->"
        (HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0)));

    (* simplification rules for vimage and Collect *)

    val vimage_simps = if length cs < 2 then [] else
      map (fn c => prove_goalw_cterm [] (cterm_of sign
        (HOLogic.mk_Trueprop (HOLogic.mk_eq
          (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
           HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
             nth_elem (find_index_eq c cs, preds)))))
        (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac
           (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
          rtac refl 1])) cs;

    val induct = prove_goalw_cterm [] (cterm_of sign
      (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
        [rtac (impI RS allI) 1,
         DETERM (etac (mono RS (fp_def RS def_induct)) 1),
         rewrite_goals_tac (map mk_meta_eq (vimage_Int::vimage_simps)),
         fold_goals_tac rec_sets_defs,
         (*This CollectE and disjE separates out the introduction rules*)
         REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
         (*Now break down the individual cases.  No disjE here in case
           some premise involves disjunction.*)
         REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE] 
                     ORELSE' hyp_subst_tac)),
         rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
         EVERY (map (fn prem =>
           DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);

    val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
      (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
        [cut_facts_tac prems 1,
         REPEAT (EVERY
           [REPEAT (resolve_tac [conjI, impI] 1),
            TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
            rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
            atac 1])])

  in standard (split_rule (induct RS lemma))
  end;



(*** specification of (co)inductive sets ****)

(** definitional introduction of (co)inductive sets **)

fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
    atts intros monos con_defs thy params paramTs cTs cnames =
  let
    val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
      commas_quote cnames) else ();

    val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
    val setT = HOLogic.mk_setT sumT;

    val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
      else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";

    val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);

    val used = foldr add_term_names (intr_ts, []);
    val [sname, xname] = variantlist (["S", "x"], used);

    (* transform an introduction rule into a conjunction  *)
    (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
    (* is transformed into                                *)
    (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)

    fun transform_rule r =
      let
        val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
        val subst = subst_free
          (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
        val Const ("op :", _) $ t $ u =
          HOLogic.dest_Trueprop (Logic.strip_imp_concl r)

      in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
        (frees, foldr1 (app HOLogic.conj)
          (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
            (map (subst o HOLogic.dest_Trueprop)
              (Logic.strip_imp_prems r))))
      end

    (* make a disjunction of all introduction rules *)

    val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
      absfree (xname, sumT, foldr1 (app HOLogic.disj) (map transform_rule intr_ts)));

    (* add definiton of recursive sets to theory *)

    val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
    val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;

    val rec_const = list_comb
      (Const (full_rec_name, paramTs ---> setT), params);

    val fp_def_term = Logic.mk_equals (rec_const,
      Const (fp_name, (setT --> setT) --> setT) $ fp_fun)

    val def_terms = fp_def_term :: (if length cs < 2 then [] else
      map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);

    val thy' = thy |>
      (if declare_consts then
        Theory.add_consts_i (map (fn (c, n) =>
          (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
       else I) |>
      (if length cs < 2 then I else
       Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)]) |>
      Theory.add_path rec_name |>
      PureThy.add_defss_i [(("defs", def_terms), [])];

    (* get definitions from theory *)

    val fp_def::rec_sets_defs = PureThy.get_thms thy' "defs";

    (* prove and store theorems *)

    val mono = prove_mono setT fp_fun monos thy';
    val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
      rec_sets_defs thy';
    val elims = if no_elim then [] else
      prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';
    val raw_induct = if no_ind then TrueI else
      if coind then standard (rule_by_tactic
        (rewrite_tac [mk_meta_eq vimage_Un] THEN
          fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
      else
        prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
          rec_sets_defs thy';
    val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
      else standard (raw_induct RSN (2, rev_mp));

    val thy'' = thy'
      |> PureThy.add_thmss [(("intrs", intrs), atts)]
      |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
      |> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])])
      |> (if no_ind then I else PureThy.add_thms
        [((coind_prefix coind ^ "induct", induct), [])])
      |> Theory.parent_path;

  in (thy'',
    {defs = fp_def::rec_sets_defs,
     mono = mono,
     unfold = unfold,
     intrs = intrs,
     elims = elims,
     mk_cases = mk_cases elims,
     raw_induct = raw_induct,
     induct = induct})
  end;



(** axiomatic introduction of (co)inductive sets **)

fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
    atts intros monos con_defs thy params paramTs cTs cnames =
  let
    val _ = if verbose then message ("Adding axioms for " ^ coind_prefix coind ^
      "inductive set(s) " ^ commas_quote cnames) else ();

    val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;

    val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
    val elim_ts = mk_elims cs cTs params intr_ts;

    val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
    val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
    
    val thy' = thy
      |> (if declare_consts then
            Theory.add_consts_i
              (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
         else I)
      |> Theory.add_path rec_name
      |> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("elims", elim_ts), [])]
      |> (if coind then I else PureThy.add_axioms_i [(("internal_induct", ind_t), [])]);

    val intrs = PureThy.get_thms thy' "intrs";
    val elims = PureThy.get_thms thy' "elims";
    val raw_induct = if coind then TrueI else
      standard (split_rule (PureThy.get_thm thy' "internal_induct"));
    val induct = if coind orelse length cs > 1 then raw_induct
      else standard (raw_induct RSN (2, rev_mp));

    val thy'' =
      thy'
      |> (if coind then I else PureThy.add_thms [(("induct", induct), [])])
      |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
      |> Theory.parent_path;
  in (thy'',
    {defs = [],
     mono = TrueI,
     unfold = TrueI,
     intrs = intrs,
     elims = elims,
     mk_cases = mk_cases elims,
     raw_induct = raw_induct,
     induct = induct})
  end;



(** introduction of (co)inductive sets **)

fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
    atts intros monos con_defs thy =
  let
    val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
    val sign = Theory.sign_of thy;

    (*parameters should agree for all mutually recursive components*)
    val (_, params) = strip_comb (hd cs);
    val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\
      \ component is not a free variable: " sign) params;

    val cTs = map (try' (HOLogic.dest_setT o fastype_of)
      "Recursive component not of type set: " sign) cs;

    val full_cnames = map (try' (fst o dest_Const o head_of)
      "Recursive set not previously declared as constant: " sign) cs;
    val cnames = map Sign.base_name full_cnames;

    val _ = assert_all Syntax.is_identifier cnames	(* FIXME why? *)
       (fn a => "Base name of recursive set not an identifier: " ^ a);
    val _ = seq (check_rule sign cs o snd o fst) intros;

    val (thy1, result) =
      (if ! quick_and_dirty then add_ind_axm else add_ind_def)
        verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
        con_defs thy params paramTs cTs cnames;
    val thy2 = thy1 |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result);
  in (thy2, result) end;



(** external interface **)

fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
  let
    val sign = Theory.sign_of thy;
    val cs = map (readtm (Theory.sign_of thy) HOLogic.termTVar) c_strings;

    val atts = map (Attrib.global_attribute thy) srcs;
    val intr_names = map (fst o fst) intro_srcs;
    val intr_ts = map (readtm (Theory.sign_of thy) propT o snd o fst) intro_srcs;
    val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
    val (cs', intr_ts') = unify_consts sign cs intr_ts;

    val ((thy', con_defs), monos) = thy
      |> IsarThy.apply_theorems raw_monos
      |> apfst (IsarThy.apply_theorems raw_con_defs);
  in
    add_inductive_i verbose false "" coind false false cs'
      atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
  end;



(** package setup **)

(* setup theory *)

val setup = [InductiveData.init];


(* outer syntax *)

local structure P = OuterParse and K = OuterSyntax.Keyword in

fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
  #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;

fun ind_decl coind =
  (Scan.repeat1 P.term --| P.marg_comment) --
  (P.$$$ "intrs" |--
    P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
  Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
  >> (Toplevel.theory o mk_ind coind);

val inductiveP =
  OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);

val coinductiveP =
  OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);


val ind_cases =
  P.opt_thm_name "=" -- P.xname --| P.$$$ ":" -- Scan.repeat1 P.prop -- P.marg_comment
  >> (Toplevel.theory o inductive_cases);

val inductive_casesP =
  OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules"
    K.thy_decl ind_cases;

val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"];
val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];

end;


end;