src/HOL/Tools/inductive_package.ML
 changeset 5094 ddcc3c114a0e child 5108 4074c7d86d44
1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Jun 30 20:39:43 1998 +0200
1.3 @@ -0,0 +1,600 @@
1.4 +(*  Title:      HOL/Tools/inductive_package.ML
1.5 +    ID:         \$Id\$
1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 +                Stefan Berghofer,   TU Muenchen
1.8 +    Copyright   1994  University of Cambridge
1.9 +                1998  TU Muenchen
1.10 +
1.11 +(Co)Inductive Definition module for HOL
1.12 +
1.13 +Features:
1.14 +* least or greatest fixedpoints
1.15 +* user-specified product and sum constructions
1.16 +* mutually recursive definitions
1.17 +* definitions involving arbitrary monotone operators
1.18 +* automatically proves introduction and elimination rules
1.19 +
1.20 +The recursive sets must *already* be declared as constants in parent theory!
1.21 +
1.22 +  Introduction rules have the form
1.23 +  [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk |]
1.24 +  where M is some monotone operator (usually the identity)
1.25 +  P(x) is any side condition on the free variables
1.26 +  ti, t are any terms
1.27 +  Sj, Sk are two of the sets being defined in mutual recursion
1.28 +
1.29 +Sums are used only for mutual recursion;
1.30 +Products are used only to derive "streamlined" induction rules for relations
1.31 +*)
1.32 +
1.33 +signature INDUCTIVE_PACKAGE =
1.34 +sig
1.35 +  val add_inductive_i : bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
1.36 +    term list -> thm list -> thm list -> theory -> theory *
1.37 +      {defs:thm list, elims:thm list, raw_induct:thm, induct:thm,
1.38 +       intrs:thm list,
1.39 +       mk_cases:thm list -> string -> thm, mono:thm,
1.40 +       unfold:thm}
1.41 +  val add_inductive : bool -> bool -> string list -> string list
1.42 +    -> thm list -> thm list -> theory -> theory *
1.43 +      {defs:thm list, elims:thm list, raw_induct:thm, induct:thm,
1.44 +       intrs:thm list,
1.45 +       mk_cases:thm list -> string -> thm, mono:thm,
1.46 +       unfold:thm}
1.47 +end;
1.48 +
1.49 +structure InductivePackage : INDUCTIVE_PACKAGE =
1.50 +struct
1.51 +
1.52 +(*For proving monotonicity of recursion operator*)
1.53 +val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono,
1.54 +                   ex_mono, Collect_mono, in_mono, vimage_mono];
1.55 +
1.56 +val Const _ \$ (vimage_f \$ _) \$ _ = HOLogic.dest_Trueprop (concl_of vimageD);
1.57 +
1.58 +(*Delete needless equality assumptions*)
1.59 +val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
1.60 +     (fn _ => [assume_tac 1]);
1.61 +
1.62 +(*For simplifying the elimination rule*)
1.63 +val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, disjE, Pair_inject];
1.64 +
1.65 +val vimage_name = Sign.intern_const (sign_of Vimage.thy) "op -``";
1.66 +val mono_name = Sign.intern_const (sign_of Ord.thy) "mono";
1.67 +
1.68 +(* make injections needed in mutually recursive definitions *)
1.69 +
1.70 +fun mk_inj cs sumT c x =
1.71 +  let
1.72 +    fun mk_inj' T n i =
1.73 +      if n = 1 then x else
1.74 +      let val n2 = n div 2;
1.75 +          val Type (_, [T1, T2]) = T
1.76 +      in
1.77 +        if i <= n2 then
1.78 +          Const ("Inl", T1 --> T) \$ (mk_inj' T1 n2 i)
1.79 +        else
1.80 +          Const ("Inr", T2 --> T) \$ (mk_inj' T2 (n - n2) (i - n2))
1.81 +      end
1.82 +  in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
1.83 +  end;
1.84 +
1.85 +(* make "vimage" terms for selecting out components of mutually rec.def. *)
1.86 +
1.87 +fun mk_vimage cs sumT t c = if length cs < 2 then t else
1.88 +  let
1.89 +    val cT = HOLogic.dest_setT (fastype_of c);
1.90 +    val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
1.91 +  in
1.92 +    Const (vimage_name, vimageT) \$
1.93 +      Abs ("y", cT, mk_inj cs sumT c (Bound 0)) \$ t
1.94 +  end;
1.95 +
1.96 +(**************************** well-formedness checks **************************)
1.97 +
1.98 +fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^
1.99 +  (Sign.string_of_term sign t) ^ "\n" ^ msg);
1.101 +fun err_in_prem sign t p msg = error ("Ill-formed premise\n" ^
1.102 +  (Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^
1.103 +  (Sign.string_of_term sign t) ^ "\n" ^ msg);
1.105 +val msg1 = "Conclusion of introduction rule must have form\
1.106 +          \ ' t : S_i '";
1.107 +val msg2 = "Premises mentioning recursive sets must have form\
1.108 +          \ ' t : M S_i '";
1.109 +val msg3 = "Recursion term on left of member symbol";
1.111 +fun check_rule sign cs r =
1.112 +  let
1.113 +    fun check_prem prem = if exists (Logic.occs o (rpair prem)) cs then
1.114 +         (case prem of
1.115 +           (Const ("op :", _) \$ t \$ u) =>
1.116 +             if exists (Logic.occs o (rpair t)) cs then
1.117 +               err_in_prem sign r prem msg3 else ()
1.118 +         | _ => err_in_prem sign r prem msg2)
1.119 +        else ()
1.121 +  in (case (HOLogic.dest_Trueprop o Logic.strip_imp_concl) r of
1.122 +        (Const ("op :", _) \$ _ \$ u) =>
1.123 +          if u mem cs then map (check_prem o HOLogic.dest_Trueprop)
1.124 +            (Logic.strip_imp_prems r)
1.125 +          else err_in_rule sign r msg1
1.126 +      | _ => err_in_rule sign r msg1)
1.127 +  end;
1.129 +fun try' f msg sign t = (f t) handle _ => error (msg ^ Sign.string_of_term sign t);
1.131 +(*********************** properties of (co)inductive sets *********************)
1.133 +(***************************** elimination rules ******************************)
1.135 +fun mk_elims cs cTs params intr_ts =
1.136 +  let
1.137 +    val used = foldr add_term_names (intr_ts, []);
1.138 +    val [aname, pname] = variantlist (["a", "P"], used);
1.139 +    val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
1.141 +    fun dest_intr r =
1.142 +      let val Const ("op :", _) \$ t \$ u =
1.143 +        HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
1.144 +      in (u, t, Logic.strip_imp_prems r) end;
1.146 +    val intrs = map dest_intr intr_ts;
1.148 +    fun mk_elim (c, T) =
1.149 +      let
1.150 +        val a = Free (aname, T);
1.152 +        fun mk_elim_prem (_, t, ts) =
1.153 +          list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
1.154 +            Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
1.155 +      in
1.156 +        Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
1.157 +          map mk_elim_prem (filter (equal c o #1) intrs), P)
1.158 +      end
1.159 +  in
1.160 +    map mk_elim (cs ~~ cTs)
1.161 +  end;
1.163 +(***************** premises and conclusions of induction rules ****************)
1.165 +fun mk_indrule cs cTs params intr_ts =
1.166 +  let
1.167 +    val used = foldr add_term_names (intr_ts, []);
1.169 +    (* predicates for induction rule *)
1.171 +    val preds = map Free (variantlist (if length cs < 2 then ["P"] else
1.172 +      map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
1.173 +        map (fn T => T --> HOLogic.boolT) cTs);
1.175 +    (* transform an introduction rule into a premise for induction rule *)
1.177 +    fun mk_ind_prem r =
1.178 +      let
1.179 +        val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
1.181 +        fun subst (prem as (Const ("op :", T) \$ t \$ u), prems) =
1.182 +              let val n = find_index_eq u cs in
1.183 +                if n >= 0 then prem :: (nth_elem (n, preds)) \$ t :: prems else
1.184 +                  (subst_free (map (fn (c, P) => (c, HOLogic.mk_binop "op Int"
1.185 +                    (c, HOLogic.Collect_const (HOLogic.dest_setT
1.186 +                      (fastype_of c)) \$ P))) (cs ~~ preds)) prem)::prems
1.187 +              end
1.188 +          | subst (prem, prems) = prem::prems;
1.190 +        val Const ("op :", _) \$ t \$ u =
1.191 +          HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
1.193 +      in list_all_free (frees,
1.194 +           Logic.list_implies (map HOLogic.mk_Trueprop (foldr subst
1.195 +             (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
1.196 +               HOLogic.mk_Trueprop (nth_elem (find_index_eq u cs, preds) \$ t)))
1.197 +      end;
1.199 +    val ind_prems = map mk_ind_prem intr_ts;
1.201 +    (* make conclusions for induction rules *)
1.203 +    fun mk_ind_concl ((c, P), (ts, x)) =
1.204 +      let val T = HOLogic.dest_setT (fastype_of c);
1.205 +          val Ts = HOLogic.prodT_factors T;
1.206 +          val (frees, x') = foldr (fn (T', (fs, s)) =>
1.207 +            ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
1.208 +          val tuple = HOLogic.mk_tuple T frees;
1.209 +      in ((HOLogic.mk_binop "op -->"
1.210 +        (HOLogic.mk_mem (tuple, c), P \$ tuple))::ts, x')
1.211 +      end;
1.213 +    val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 (app HOLogic.conj)
1.214 +        (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
1.216 +  in (preds, ind_prems, mutual_ind_concl)
1.217 +  end;
1.219 +(********************** proofs for (co)inductive sets *************************)
1.221 +(**************************** prove monotonicity ******************************)
1.223 +fun prove_mono setT fp_fun monos thy =
1.224 +  let
1.225 +    val _ = writeln "  Proving monotonicity...";
1.227 +    val mono = prove_goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop
1.228 +      (Const (mono_name, (setT --> setT) --> HOLogic.boolT) \$ fp_fun)))
1.229 +        (fn _ => [rtac monoI 1, REPEAT (ares_tac (basic_monos @ monos) 1)])
1.231 +  in mono end;
1.233 +(************************* prove introduction rules ***************************)
1.235 +fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
1.236 +  let
1.237 +    val _ = writeln "  Proving the introduction rules...";
1.239 +    val unfold = standard (mono RS (fp_def RS
1.240 +      (if coind then def_gfp_Tarski else def_lfp_Tarski)));
1.242 +    fun select_disj 1 1 = []
1.243 +      | select_disj _ 1 = [rtac disjI1]
1.244 +      | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
1.246 +    val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
1.247 +      (cterm_of (sign_of thy) intr) (fn prems =>
1.248 +       [(*insert prems and underlying sets*)
1.249 +       cut_facts_tac prems 1,
1.250 +       stac unfold 1,
1.251 +       REPEAT (resolve_tac [vimageI2, CollectI] 1),
1.252 +       (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
1.253 +       EVERY1 (select_disj (length intr_ts) i),
1.254 +       (*Not ares_tac, since refl must be tried before any equality assumptions;
1.255 +         backtracking may occur if the premises have extra variables!*)
1.256 +       DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
1.257 +       (*Now solve the equations like Inl 0 = Inl ?b2*)
1.258 +       rewrite_goals_tac con_defs,
1.259 +       REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts)
1.261 +  in (intrs, unfold) end;
1.263 +(*************************** prove elimination rules **************************)
1.265 +fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =
1.266 +  let
1.267 +    val _ = writeln "  Proving the elimination rules...";
1.269 +    val rules1 = [CollectE, disjE, make_elim vimageD];
1.270 +    val rules2 = [exE, conjE, Inl_neq_Inr, Inr_neq_Inl] @
1.271 +      map make_elim [Inl_inject, Inr_inject];
1.273 +    val elims = map (fn t => prove_goalw_cterm rec_sets_defs
1.274 +      (cterm_of (sign_of thy) t) (fn prems =>
1.275 +        [cut_facts_tac [hd prems] 1,
1.276 +         dtac (unfold RS subst) 1,
1.277 +         REPEAT (FIRSTGOAL (eresolve_tac rules1)),
1.278 +         REPEAT (FIRSTGOAL (eresolve_tac rules2)),
1.279 +         EVERY (map (fn prem =>
1.280 +           DEPTH_SOLVE_1 (ares_tac (prem::[conjI]) 1)) (tl prems))]))
1.281 +      (mk_elims cs cTs params intr_ts)
1.283 +  in elims end;
1.285 +(** derivation of simplified elimination rules **)
1.287 +(*Applies freeness of the given constructors, which *must* be unfolded by
1.288 +  the given defs.  Cannot simply use the local con_defs because con_defs=[]
1.289 +  for inference systems.
1.290 +  FIXME: proper handling of conjunctive / disjunctive side conditions?!
1.291 + *)
1.292 +fun con_elim_tac simps =
1.293 +  let val elim_tac = REPEAT o (eresolve_tac elim_rls)
1.294 +  in ALLGOALS(EVERY'[elim_tac,
1.295 +                 asm_full_simp_tac (simpset_of Nat.thy addsimps simps),
1.296 +                 elim_tac,
1.297 +                 REPEAT o bound_hyp_subst_tac])
1.298 +     THEN prune_params_tac
1.299 +  end;
1.301 +(*String s should have the form t:Si where Si is an inductive set*)
1.302 +fun mk_cases elims defs s =
1.303 +  let val prem = assume (read_cterm (sign_of_thm (hd elims)) (s, propT));
1.304 +      val elims' = map (try (fn r =>
1.305 +        rule_by_tactic (con_elim_tac defs) (prem RS r) |> standard)) elims
1.306 +  in case find_first is_some elims' of
1.307 +       Some (Some r) => r
1.308 +     | None => error ("mk_cases: string '" ^ s ^ "' not of form 't : S_i'")
1.309 +  end;
1.311 +(**************************** prove induction rule ****************************)
1.313 +fun prove_indrule cs cTs sumT rec_const params intr_ts mono
1.314 +    fp_def rec_sets_defs thy =
1.315 +  let
1.316 +    val _ = writeln "  Proving the induction rule...";
1.318 +    val sign = sign_of thy;
1.320 +    val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
1.322 +    (* make predicate for instantiation of abstract induction rule *)
1.324 +    fun mk_ind_pred _ [P] = P
1.325 +      | mk_ind_pred T Ps =
1.326 +         let val n = (length Ps) div 2;
1.327 +             val Type (_, [T1, T2]) = T
1.328 +         in Const ("sum_case",
1.329 +           [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) \$
1.330 +             mk_ind_pred T1 (take (n, Ps)) \$ mk_ind_pred T2 (drop (n, Ps))
1.331 +         end;
1.333 +    val ind_pred = mk_ind_pred sumT preds;
1.335 +    val ind_concl = HOLogic.mk_Trueprop
1.336 +      (HOLogic.all_const sumT \$ Abs ("x", sumT, HOLogic.mk_binop "op -->"
1.337 +        (HOLogic.mk_mem (Bound 0, rec_const), ind_pred \$ Bound 0)));
1.339 +    (* simplification rules for vimage and Collect *)
1.341 +    val vimage_simps = if length cs < 2 then [] else
1.342 +      map (fn c => prove_goalw_cterm [] (cterm_of sign
1.343 +        (HOLogic.mk_Trueprop (HOLogic.mk_eq
1.344 +          (mk_vimage cs sumT (HOLogic.Collect_const sumT \$ ind_pred) c,
1.345 +           HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) \$
1.346 +             nth_elem (find_index_eq c cs, preds)))))
1.347 +        (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac
1.348 +           (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
1.349 +          rtac refl 1])) cs;
1.351 +    val induct = prove_goalw_cterm [] (cterm_of sign
1.352 +      (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
1.353 +        [rtac (impI RS allI) 1,
1.354 +         DETERM (etac (mono RS (fp_def RS def_induct)) 1),
1.355 +         rewrite_goals_tac (map mk_meta_eq (vimage_Int::vimage_simps)),
1.356 +         fold_goals_tac rec_sets_defs,
1.357 +         (*This CollectE and disjE separates out the introduction rules*)
1.358 +         REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])),
1.359 +         (*Now break down the individual cases.  No disjE here in case
1.360 +           some premise involves disjunction.*)
1.361 +         REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE]
1.362 +                     ORELSE' hyp_subst_tac)),
1.363 +         rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
1.364 +         EVERY (map (fn prem =>
1.365 +           DEPTH_SOLVE_1 (ares_tac (prem::[conjI, refl]) 1)) prems)]);
1.367 +    val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
1.368 +      (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
1.369 +        [cut_facts_tac prems 1,
1.370 +         REPEAT (EVERY
1.371 +           [REPEAT (resolve_tac [conjI, impI] 1),
1.372 +            TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
1.373 +            rewrite_goals_tac (map mk_meta_eq [sum_case_Inl, sum_case_Inr]),
1.374 +            atac 1])])
1.376 +  in standard (split_rule (induct RS lemma))
1.377 +  end;
1.379 +(*************** definitional introduction of (co)inductive sets **************)
1.381 +fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
1.382 +    intr_ts monos con_defs thy params paramTs cTs cnames =
1.383 +  let
1.384 +    val _ = if verbose then writeln ("Proofs for " ^
1.385 +      (if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else ();
1.387 +    val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
1.388 +    val setT = HOLogic.mk_setT sumT;
1.390 +    val fp_name = if coind then Sign.intern_const (sign_of Gfp.thy) "gfp"
1.391 +      else Sign.intern_const (sign_of Lfp.thy) "lfp";
1.393 +    (* transform an introduction rule into a conjunction  *)
1.394 +    (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
1.395 +    (* is transformed into                                *)
1.396 +    (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
1.398 +    fun transform_rule r =
1.399 +      let
1.400 +        val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
1.401 +        val idx = length frees;
1.402 +        val subst = subst_free (cs ~~ (map (mk_vimage cs sumT (Bound (idx + 1))) cs));
1.403 +        val Const ("op :", _) \$ t \$ u =
1.404 +          HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
1.406 +      in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
1.407 +        (frees, foldr1 (app HOLogic.conj)
1.408 +          (((HOLogic.eq_const sumT) \$ Bound idx \$ (mk_inj cs sumT u t))::
1.409 +            (map (subst o HOLogic.dest_Trueprop)
1.410 +              (Logic.strip_imp_prems r))))
1.411 +      end
1.413 +    (* make a disjunction of all introduction rules *)
1.415 +    val fp_fun = Abs ("S", setT, (HOLogic.Collect_const sumT) \$
1.416 +      Abs ("x", sumT, foldr1 (app HOLogic.disj) (map transform_rule intr_ts)));
1.418 +    (* add definiton of recursive sets to theory *)
1.420 +    val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
1.421 +    val full_rec_name = Sign.full_name (sign_of thy) rec_name;
1.423 +    val rec_const = list_comb
1.424 +      (Const (full_rec_name, paramTs ---> setT), params);
1.426 +    val fp_def_term = Logic.mk_equals (rec_const,
1.427 +      Const (fp_name, (setT --> setT) --> setT) \$ fp_fun)
1.429 +    val def_terms = fp_def_term :: (if length cs < 2 then [] else
1.430 +      map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
1.432 +    val thy' = thy |>
1.433 +      (if declare_consts then
1.434 +        Theory.add_consts_i (map (fn (c, n) =>
1.435 +          (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
1.436 +       else I) |>
1.437 +      (if length cs < 2 then I else
1.438 +       Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)]) |>
1.439 +      Theory.add_path rec_name |>
1.440 +      PureThy.add_defss_i [(("defs", def_terms), [])];
1.442 +    (* get definitions from theory *)
1.444 +    val fp_def::rec_sets_defs = get_thms thy' "defs";
1.446 +    (* prove and store theorems *)
1.448 +    val mono = prove_mono setT fp_fun monos thy';
1.449 +    val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
1.450 +      rec_sets_defs thy';
1.451 +    val elims = if no_elim then [] else
1.452 +      prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';
1.453 +    val raw_induct = if no_ind then TrueI else
1.454 +      if coind then standard (rule_by_tactic
1.455 +        (rewrite_tac [mk_meta_eq vimage_Un] THEN
1.456 +          fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
1.457 +      else
1.458 +        prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
1.459 +          rec_sets_defs thy';
1.460 +    val induct = if coind orelse length cs > 1 then raw_induct
1.461 +      else standard (raw_induct RSN (2, rev_mp));
1.463 +    val thy'' = thy' |>
1.464 +      PureThy.add_tthmss [(("intrs", map Attribute.tthm_of intrs), [])] |>
1.465 +      (if no_elim then I else PureThy.add_tthmss
1.466 +        [(("elims", map Attribute.tthm_of elims), [])]) |>
1.467 +      (if no_ind then I else PureThy.add_tthms
1.468 +        [(((if coind then "co" else "") ^ "induct",
1.469 +          Attribute.tthm_of induct), [])]) |>
1.470 +      Theory.parent_path;
1.472 +  in (thy'',
1.473 +    {defs = fp_def::rec_sets_defs,
1.474 +     mono = mono,
1.475 +     unfold = unfold,
1.476 +     intrs = intrs,
1.477 +     elims = elims,
1.478 +     mk_cases = mk_cases elims,
1.479 +     raw_induct = raw_induct,
1.480 +     induct = induct})
1.481 +  end;
1.483 +(***************** axiomatic introduction of (co)inductive sets ***************)
1.485 +fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
1.486 +    intr_ts monos con_defs thy params paramTs cTs cnames =
1.487 +  let
1.488 +    val _ = if verbose then writeln ("Adding axioms for " ^
1.489 +      (if coind then "co" else "") ^ "inductive set(s) " ^ commas cnames) else ();
1.491 +    val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
1.493 +    val elim_ts = mk_elims cs cTs params intr_ts;
1.495 +    val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
1.496 +    val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
1.498 +    val thy' = thy |>
1.499 +      (if declare_consts then
1.500 +        Theory.add_consts_i (map (fn (c, n) =>
1.501 +          (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
1.502 +       else I) |>
1.503 +      Theory.add_path rec_name |>
1.504 +      PureThy.add_axiomss_i [(("intrs", intr_ts), []), (("elims", elim_ts), [])] |>
1.505 +      (if coind then I
1.506 +       else PureThy.add_axioms_i [(("internal_induct", ind_t), [])]);
1.508 +    val intrs = get_thms thy' "intrs";
1.509 +    val elims = get_thms thy' "elims";
1.510 +    val raw_induct = if coind then TrueI else
1.511 +      standard (split_rule (get_thm thy' "internal_induct"));
1.512 +    val induct = if coind orelse length cs > 1 then raw_induct
1.513 +      else standard (raw_induct RSN (2, rev_mp));
1.515 +    val thy'' = thy' |>
1.516 +      (if coind then I
1.517 +       else PureThy.add_tthms [(("induct", Attribute.tthm_of induct), [])]) |>
1.518 +      Theory.parent_path
1.520 +  in (thy'',
1.521 +    {defs = [],
1.522 +     mono = TrueI,
1.523 +     unfold = TrueI,
1.524 +     intrs = intrs,
1.525 +     elims = elims,
1.526 +     mk_cases = mk_cases elims,
1.527 +     raw_induct = raw_induct,
1.528 +     induct = induct})
1.529 +  end;
1.531 +(********************** introduction of (co)inductive sets ********************)
1.533 +fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
1.534 +    intr_ts monos con_defs thy =
1.535 +  let
1.536 +    val _ = Theory.requires thy "Inductive"
1.537 +      ((if coind then "co" else "") ^ "inductive definitions");
1.539 +    val sign = sign_of thy;
1.541 +    (*parameters should agree for all mutually recursive components*)
1.542 +    val (_, params) = strip_comb (hd cs);
1.543 +    val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\
1.544 +      \ component is not a free variable: " sign) params;
1.546 +    val cTs = map (try' (HOLogic.dest_setT o fastype_of)
1.547 +      "Recursive component not of type set: " sign) cs;
1.549 +    val cnames = map (try' (Sign.base_name o fst o dest_Const o head_of)
1.550 +      "Recursive set not previously declared as constant: " sign) cs;
1.552 +    val _ = assert_all Syntax.is_identifier cnames
1.553 +       (fn a => "Base name of recursive set not an identifier: " ^ a);
1.555 +    val _ = map (check_rule sign cs) intr_ts;
1.557 +  in
1.558 +    (if !quick_and_dirty then add_ind_axm else add_ind_def)
1.559 +      verbose declare_consts alt_name coind no_elim no_ind cs intr_ts monos
1.560 +        con_defs thy params paramTs cTs cnames
1.561 +  end;
1.563 +(***************************** external interface *****************************)
1.565 +fun add_inductive verbose coind c_strings intr_strings monos con_defs thy =
1.566 +  let
1.567 +    val sign = sign_of thy;
1.568 +    val cs = map (readtm (sign_of thy) HOLogic.termTVar) c_strings;
1.569 +    val intr_ts = map (readtm (sign_of thy) propT) intr_strings;
1.571 +    (* the following code ensures that each recursive set *)
1.572 +    (* always has the same type in all introduction rules *)
1.574 +    val {tsig, ...} = Sign.rep_sg sign;
1.575 +    val add_term_consts_2 =
1.576 +      foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
1.577 +    fun varify (t, (i, ts)) =
1.578 +      let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
1.579 +      in (maxidx_of_term t', t'::ts) end;
1.580 +    val (i, cs') = foldr varify (cs, (~1, []));
1.581 +    val (i', intr_ts') = foldr varify (intr_ts, (i, []));
1.582 +    val rec_consts = foldl add_term_consts_2 ([], cs');
1.583 +    val intr_consts = foldl add_term_consts_2 ([], intr_ts');
1.584 +    fun unify (env, (cname, cT)) =
1.585 +      let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
1.586 +      in (foldl (fn ((env', j'), Tp) => Type.unify tsig j' env' Tp)
1.587 +        (env, (replicate (length consts) cT) ~~ consts)) handle _ =>
1.588 +          error ("Occurrences of constant '" ^ cname ^
1.589 +            "' have incompatible types")
1.590 +      end;
1.591 +    val (env, _) = foldl unify (([], i'), rec_consts);
1.592 +    fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T
1.593 +      in if T = T' then T else typ_subst_TVars_2 env T' end;
1.594 +    val subst = fst o Type.freeze_thaw o
1.595 +      (map_term_types (typ_subst_TVars_2 env));
1.596 +    val cs'' = map subst cs';
1.597 +    val intr_ts'' = map subst intr_ts';
1.599 +  in add_inductive_i verbose false "" coind false false cs'' intr_ts''
1.600 +    monos con_defs thy
1.601 +  end;
1.603 +end;