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