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.100 +
   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.104 +
   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.110 +
   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.120 +
   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.128 +
   1.129 +fun try' f msg sign t = (f t) handle _ => error (msg ^ Sign.string_of_term sign t);
   1.130 +
   1.131 +(*********************** properties of (co)inductive sets *********************)
   1.132 +
   1.133 +(***************************** elimination rules ******************************)
   1.134 +
   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.140 +
   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.145 +
   1.146 +    val intrs = map dest_intr intr_ts;
   1.147 +
   1.148 +    fun mk_elim (c, T) =
   1.149 +      let
   1.150 +        val a = Free (aname, T);
   1.151 +
   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.162 +        
   1.163 +(***************** premises and conclusions of induction rules ****************)
   1.164 +
   1.165 +fun mk_indrule cs cTs params intr_ts =
   1.166 +  let
   1.167 +    val used = foldr add_term_names (intr_ts, []);
   1.168 +
   1.169 +    (* predicates for induction rule *)
   1.170 +
   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.174 +
   1.175 +    (* transform an introduction rule into a premise for induction rule *)
   1.176 +
   1.177 +    fun mk_ind_prem r =
   1.178 +      let
   1.179 +        val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   1.180 +
   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.189 +
   1.190 +        val Const ("op :", _) $ t $ u =
   1.191 +          HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   1.192 +
   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.198 +
   1.199 +    val ind_prems = map mk_ind_prem intr_ts;
   1.200 +
   1.201 +    (* make conclusions for induction rules *)
   1.202 +
   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.212 +
   1.213 +    val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 (app HOLogic.conj)
   1.214 +        (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
   1.215 +
   1.216 +  in (preds, ind_prems, mutual_ind_concl)
   1.217 +  end;
   1.218 +
   1.219 +(********************** proofs for (co)inductive sets *************************)
   1.220 +
   1.221 +(**************************** prove monotonicity ******************************)
   1.222 +
   1.223 +fun prove_mono setT fp_fun monos thy =
   1.224 +  let
   1.225 +    val _ = writeln "  Proving monotonicity...";
   1.226 +
   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.230 +
   1.231 +  in mono end;
   1.232 +
   1.233 +(************************* prove introduction rules ***************************)
   1.234 +
   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.238 +
   1.239 +    val unfold = standard (mono RS (fp_def RS
   1.240 +      (if coind then def_gfp_Tarski else def_lfp_Tarski)));
   1.241 +
   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.245 +
   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.260 +
   1.261 +  in (intrs, unfold) end;
   1.262 +
   1.263 +(*************************** prove elimination rules **************************)
   1.264 +
   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.268 +
   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.272 +
   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.282 +
   1.283 +  in elims end;
   1.284 +
   1.285 +(** derivation of simplified elimination rules **)
   1.286 +
   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.300 +
   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.310 +
   1.311 +(**************************** prove induction rule ****************************)
   1.312 +
   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.317 +
   1.318 +    val sign = sign_of thy;
   1.319 +
   1.320 +    val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   1.321 +
   1.322 +    (* make predicate for instantiation of abstract induction rule *)
   1.323 +
   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.332 +
   1.333 +    val ind_pred = mk_ind_pred sumT preds;
   1.334 +
   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.338 +
   1.339 +    (* simplification rules for vimage and Collect *)
   1.340 +
   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.350 +
   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.366 +
   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.375 +
   1.376 +  in standard (split_rule (induct RS lemma))
   1.377 +  end;
   1.378 +
   1.379 +(*************** definitional introduction of (co)inductive sets **************)
   1.380 +
   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.386 +
   1.387 +    val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
   1.388 +    val setT = HOLogic.mk_setT sumT;
   1.389 +
   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.392 +
   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.397 +
   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.405 +
   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.412 +
   1.413 +    (* make a disjunction of all introduction rules *)
   1.414 +
   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.417 +
   1.418 +    (* add definiton of recursive sets to theory *)
   1.419 +
   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.422 +
   1.423 +    val rec_const = list_comb
   1.424 +      (Const (full_rec_name, paramTs ---> setT), params);
   1.425 +
   1.426 +    val fp_def_term = Logic.mk_equals (rec_const,
   1.427 +      Const (fp_name, (setT --> setT) --> setT) $ fp_fun)
   1.428 +
   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.431 +
   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.441 +
   1.442 +    (* get definitions from theory *)
   1.443 +
   1.444 +    val fp_def::rec_sets_defs = get_thms thy' "defs";
   1.445 +
   1.446 +    (* prove and store theorems *)
   1.447 +
   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.462 +
   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.471 +
   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.482 +
   1.483 +(***************** axiomatic introduction of (co)inductive sets ***************)
   1.484 +
   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.490 +
   1.491 +    val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
   1.492 +
   1.493 +    val elim_ts = mk_elims cs cTs params intr_ts;
   1.494 +
   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.497 +    
   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.507 +
   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.514 +
   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.519 +
   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.530 +
   1.531 +(********************** introduction of (co)inductive sets ********************)
   1.532 +
   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.538 +
   1.539 +    val sign = sign_of thy;
   1.540 +
   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.545 +
   1.546 +    val cTs = map (try' (HOLogic.dest_setT o fastype_of)
   1.547 +      "Recursive component not of type set: " sign) cs;
   1.548 +
   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.551 +
   1.552 +    val _ = assert_all Syntax.is_identifier cnames
   1.553 +       (fn a => "Base name of recursive set not an identifier: " ^ a);
   1.554 +
   1.555 +    val _ = map (check_rule sign cs) intr_ts;
   1.556 +
   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.562 +
   1.563 +(***************************** external interface *****************************)
   1.564 +
   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.570 +
   1.571 +    (* the following code ensures that each recursive set *)
   1.572 +    (* always has the same type in all introduction rules *)
   1.573 +
   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.598 +
   1.599 +  in add_inductive_i verbose false "" coind false false cs'' intr_ts''
   1.600 +    monos con_defs thy
   1.601 +  end;
   1.602 +
   1.603 +end;