src/ZF/Tools/inductive_package.ML
author wenzelm
Sat Apr 16 15:25:25 2011 +0200 (2011-04-16)
changeset 42359 6ca5407863ed
parent 42290 b1f544c84040
child 42361 23f352990944
permissions -rw-r--r--
prefer local name spaces;
tuned signatures;
tuned;
     1 (*  Title:      ZF/Tools/inductive_package.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3 
     4 Fixedpoint definition module -- for Inductive/Coinductive Definitions
     5 
     6 The functor will be instantiated for normal sums/products (inductive defs)
     7                          and non-standard sums/products (coinductive defs)
     8 
     9 Sums are used only for mutual recursion;
    10 Products are used only to derive "streamlined" induction rules for relations
    11 *)
    12 
    13 type inductive_result =
    14    {defs       : thm list,             (*definitions made in thy*)
    15     bnd_mono   : thm,                  (*monotonicity for the lfp definition*)
    16     dom_subset : thm,                  (*inclusion of recursive set in dom*)
    17     intrs      : thm list,             (*introduction rules*)
    18     elim       : thm,                  (*case analysis theorem*)
    19     induct     : thm,                  (*main induction rule*)
    20     mutual_induct : thm};              (*mutual induction rule*)
    21 
    22 
    23 (*Functor's result signature*)
    24 signature INDUCTIVE_PACKAGE =
    25 sig
    26   (*Insert definitions for the recursive sets, which
    27      must *already* be declared as constants in parent theory!*)
    28   val add_inductive_i: bool -> term list * term ->
    29     ((binding * term) * attribute list) list ->
    30     thm list * thm list * thm list * thm list -> theory -> theory * inductive_result
    31   val add_inductive: string list * string ->
    32     ((binding * string) * Attrib.src list) list ->
    33     (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list *
    34     (Facts.ref * Attrib.src list) list * (Facts.ref * Attrib.src list) list ->
    35     theory -> theory * inductive_result
    36 end;
    37 
    38 
    39 (*Declares functions to add fixedpoint/constructor defs to a theory.
    40   Recursive sets must *already* be declared as constants.*)
    41 functor Add_inductive_def_Fun
    42     (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU val coind: bool)
    43  : INDUCTIVE_PACKAGE =
    44 struct
    45 
    46 val co_prefix = if coind then "co" else "";
    47 
    48 
    49 (* utils *)
    50 
    51 (*make distinct individual variables a1, a2, a3, ..., an. *)
    52 fun mk_frees a [] = []
    53   | mk_frees a (T::Ts) = Free(a,T) :: mk_frees (Symbol.bump_string a) Ts;
    54 
    55 
    56 (* add_inductive(_i) *)
    57 
    58 (*internal version, accepting terms*)
    59 fun add_inductive_i verbose (rec_tms, dom_sum)
    60   raw_intr_specs (monos, con_defs, type_intrs, type_elims) thy =
    61 let
    62   val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
    63   val ctxt = ProofContext.init_global thy;
    64 
    65   val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs;
    66   val (intr_names, intr_tms) = split_list (map fst intr_specs);
    67   val case_names = Rule_Cases.case_names intr_names;
    68 
    69   (*recT and rec_params should agree for all mutually recursive components*)
    70   val rec_hds = map head_of rec_tms;
    71 
    72   val dummy = assert_all is_Const rec_hds
    73           (fn t => "Recursive set not previously declared as constant: " ^
    74                    Syntax.string_of_term ctxt t);
    75 
    76   (*Now we know they are all Consts, so get their names, type and params*)
    77   val rec_names = map (#1 o dest_Const) rec_hds
    78   and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
    79 
    80   val rec_base_names = map Long_Name.base_name rec_names;
    81   val dummy = assert_all Lexicon.is_identifier rec_base_names
    82     (fn a => "Base name of recursive set not an identifier: " ^ a);
    83 
    84   local (*Checking the introduction rules*)
    85     val intr_sets = map (#2 o Ind_Syntax.rule_concl_msg thy) intr_tms;
    86     fun intr_ok set =
    87         case head_of set of Const(a,recT) => member (op =) rec_names a | _ => false;
    88   in
    89     val dummy =  assert_all intr_ok intr_sets
    90        (fn t => "Conclusion of rule does not name a recursive set: " ^
    91                 Syntax.string_of_term ctxt t);
    92   end;
    93 
    94   val dummy = assert_all is_Free rec_params
    95       (fn t => "Param in recursion term not a free variable: " ^
    96                Syntax.string_of_term ctxt t);
    97 
    98   (*** Construct the fixedpoint definition ***)
    99   val mk_variant = Name.variant (List.foldr OldTerm.add_term_names [] intr_tms);
   100 
   101   val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
   102 
   103   fun dest_tprop (Const(@{const_name Trueprop},_) $ P) = P
   104     | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
   105                             Syntax.string_of_term ctxt Q);
   106 
   107   (*Makes a disjunct from an introduction rule*)
   108   fun fp_part intr = (*quantify over rule's free vars except parameters*)
   109     let val prems = map dest_tprop (Logic.strip_imp_prems intr)
   110         val dummy = List.app (fn rec_hd => List.app (Ind_Syntax.chk_prem rec_hd) prems) rec_hds
   111         val exfrees = subtract (op =) rec_params (OldTerm.term_frees intr)
   112         val zeq = FOLogic.mk_eq (Free(z', Ind_Syntax.iT), #1 (Ind_Syntax.rule_concl intr))
   113     in List.foldr FOLogic.mk_exists
   114              (Balanced_Tree.make FOLogic.mk_conj (zeq::prems)) exfrees
   115     end;
   116 
   117   (*The Part(A,h) terms -- compose injections to make h*)
   118   fun mk_Part (Bound 0) = Free(X', Ind_Syntax.iT) (*no mutual rec, no Part needed*)
   119     | mk_Part h = @{const Part} $ Free(X', Ind_Syntax.iT) $ Abs (w', Ind_Syntax.iT, h);
   120 
   121   (*Access to balanced disjoint sums via injections*)
   122   val parts = map mk_Part
   123     (Balanced_Tree.accesses {left = fn t => Su.inl $ t, right = fn t => Su.inr $ t, init = Bound 0}
   124       (length rec_tms));
   125 
   126   (*replace each set by the corresponding Part(A,h)*)
   127   val part_intrs = map (subst_free (rec_tms ~~ parts) o fp_part) intr_tms;
   128 
   129   val fp_abs =
   130     absfree (X', Ind_Syntax.iT,
   131         Ind_Syntax.mk_Collect (z', dom_sum,
   132             Balanced_Tree.make FOLogic.mk_disj part_intrs));
   133 
   134   val fp_rhs = Fp.oper $ dom_sum $ fp_abs
   135 
   136   val dummy = List.app (fn rec_hd => (Logic.occs (rec_hd, fp_rhs) andalso
   137                              error "Illegal occurrence of recursion operator"; ()))
   138            rec_hds;
   139 
   140   (*** Make the new theory ***)
   141 
   142   (*A key definition:
   143     If no mutual recursion then it equals the one recursive set.
   144     If mutual recursion then it differs from all the recursive sets. *)
   145   val big_rec_base_name = space_implode "_" rec_base_names;
   146   val big_rec_name = ProofContext.intern_const ctxt big_rec_base_name;
   147 
   148 
   149   val _ =
   150     if verbose then
   151       writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name)
   152     else ();
   153 
   154   (*Big_rec... is the union of the mutually recursive sets*)
   155   val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
   156 
   157   (*The individual sets must already be declared*)
   158   val axpairs = map Misc_Legacy.mk_defpair
   159         ((big_rec_tm, fp_rhs) ::
   160          (case parts of
   161              [_] => []                        (*no mutual recursion*)
   162            | _ => rec_tms ~~          (*define the sets as Parts*)
   163                   map (subst_atomic [(Free (X', Ind_Syntax.iT), big_rec_tm)]) parts));
   164 
   165   (*tracing: print the fixedpoint definition*)
   166   val dummy = if !Ind_Syntax.trace then
   167               writeln (cat_lines (map (Syntax.string_of_term ctxt o #2) axpairs))
   168           else ()
   169 
   170   (*add definitions of the inductive sets*)
   171   val (_, thy1) =
   172     thy
   173     |> Sign.add_path big_rec_base_name
   174     |> Global_Theory.add_defs false (map (Thm.no_attributes o apfst Binding.name) axpairs);
   175 
   176   val ctxt1 = ProofContext.init_global thy1;
   177 
   178 
   179   (*fetch fp definitions from the theory*)
   180   val big_rec_def::part_rec_defs =
   181     map (Misc_Legacy.get_def thy1)
   182         (case rec_names of [_] => rec_names
   183                          | _   => big_rec_base_name::rec_names);
   184 
   185 
   186   (********)
   187   val dummy = writeln "  Proving monotonicity...";
   188 
   189   val bnd_mono =
   190     Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
   191       (fn _ => EVERY
   192         [rtac (@{thm Collect_subset} RS @{thm bnd_monoI}) 1,
   193          REPEAT (ares_tac (@{thms basic_monos} @ monos) 1)]);
   194 
   195   val dom_subset = Drule.export_without_context (big_rec_def RS Fp.subs);
   196 
   197   val unfold = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.Tarski);
   198 
   199   (********)
   200   val dummy = writeln "  Proving the introduction rules...";
   201 
   202   (*Mutual recursion?  Helps to derive subset rules for the
   203     individual sets.*)
   204   val Part_trans =
   205       case rec_names of
   206            [_] => asm_rl
   207          | _   => Drule.export_without_context (@{thm Part_subset} RS @{thm subset_trans});
   208 
   209   (*To type-check recursive occurrences of the inductive sets, possibly
   210     enclosed in some monotonic operator M.*)
   211   val rec_typechecks =
   212      [dom_subset] RL (asm_rl :: ([Part_trans] RL monos))
   213      RL [@{thm subsetD}];
   214 
   215   (*Type-checking is hardest aspect of proof;
   216     disjIn selects the correct disjunct after unfolding*)
   217   fun intro_tacsf disjIn =
   218     [DETERM (stac unfold 1),
   219      REPEAT (resolve_tac [@{thm Part_eqI}, @{thm CollectI}] 1),
   220      (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
   221      rtac disjIn 2,
   222      (*Not ares_tac, since refl must be tried before equality assumptions;
   223        backtracking may occur if the premises have extra variables!*)
   224      DEPTH_SOLVE_1 (resolve_tac [@{thm refl}, @{thm exI}, @{thm conjI}] 2 APPEND assume_tac 2),
   225      (*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
   226      rewrite_goals_tac con_defs,
   227      REPEAT (rtac @{thm refl} 2),
   228      (*Typechecking; this can fail*)
   229      if !Ind_Syntax.trace then print_tac "The type-checking subgoal:"
   230      else all_tac,
   231      REPEAT (FIRSTGOAL (        dresolve_tac rec_typechecks
   232                         ORELSE' eresolve_tac (asm_rl :: @{thm PartE} :: @{thm SigmaE2} ::
   233                                               type_elims)
   234                         ORELSE' hyp_subst_tac)),
   235      if !Ind_Syntax.trace then print_tac "The subgoal after monos, type_elims:"
   236      else all_tac,
   237      DEPTH_SOLVE (swap_res_tac (@{thm SigmaI} :: @{thm subsetI} :: type_intrs) 1)];
   238 
   239   (*combines disjI1 and disjI2 to get the corresponding nested disjunct...*)
   240   val mk_disj_rls = Balanced_Tree.accesses
   241     {left = fn rl => rl RS @{thm disjI1},
   242      right = fn rl => rl RS @{thm disjI2},
   243      init = @{thm asm_rl}};
   244 
   245   val intrs =
   246     (intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
   247     |> ListPair.map (fn (t, tacs) =>
   248       Goal.prove_global thy1 [] [] t
   249         (fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs)));
   250 
   251   (********)
   252   val dummy = writeln "  Proving the elimination rule...";
   253 
   254   (*Breaks down logical connectives in the monotonic function*)
   255   val basic_elim_tac =
   256       REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
   257                 ORELSE' bound_hyp_subst_tac))
   258       THEN prune_params_tac
   259           (*Mutual recursion: collapse references to Part(D,h)*)
   260       THEN (PRIMITIVE (fold_rule part_rec_defs));
   261 
   262   (*Elimination*)
   263   val elim = rule_by_tactic (ProofContext.init_global thy1) basic_elim_tac
   264                  (unfold RS Ind_Syntax.equals_CollectD)
   265 
   266   (*Applies freeness of the given constructors, which *must* be unfolded by
   267       the given defs.  Cannot simply use the local con_defs because
   268       con_defs=[] for inference systems.
   269     Proposition A should have the form t:Si where Si is an inductive set*)
   270   fun make_cases ctxt A =
   271     rule_by_tactic ctxt
   272       (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac (simpset_of ctxt)) THEN basic_elim_tac)
   273       (Thm.assume A RS elim)
   274       |> Drule.export_without_context_open;
   275 
   276   fun induction_rules raw_induct thy =
   277    let
   278      val dummy = writeln "  Proving the induction rule...";
   279 
   280      (*** Prove the main induction rule ***)
   281 
   282      val pred_name = "P";            (*name for predicate variables*)
   283 
   284      (*Used to make induction rules;
   285         ind_alist = [(rec_tm1,pred1),...] associates predicates with rec ops
   286         prem is a premise of an intr rule*)
   287      fun add_induct_prem ind_alist (prem as Const (@{const_name Trueprop}, _) $
   288                       (Const (@{const_name mem}, _) $ t $ X), iprems) =
   289           (case AList.lookup (op aconv) ind_alist X of
   290                SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
   291              | NONE => (*possibly membership in M(rec_tm), for M monotone*)
   292                  let fun mk_sb (rec_tm,pred) =
   293                              (rec_tm, @{const Collect} $ rec_tm $ pred)
   294                  in  subst_free (map mk_sb ind_alist) prem :: iprems  end)
   295        | add_induct_prem ind_alist (prem,iprems) = prem :: iprems;
   296 
   297      (*Make a premise of the induction rule.*)
   298      fun induct_prem ind_alist intr =
   299        let val quantfrees = map dest_Free (subtract (op =) rec_params (OldTerm.term_frees intr))
   300            val iprems = List.foldr (add_induct_prem ind_alist) []
   301                               (Logic.strip_imp_prems intr)
   302            val (t,X) = Ind_Syntax.rule_concl intr
   303            val (SOME pred) = AList.lookup (op aconv) ind_alist X
   304            val concl = FOLogic.mk_Trueprop (pred $ t)
   305        in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
   306        handle Bind => error"Recursion term not found in conclusion";
   307 
   308      (*Minimizes backtracking by delivering the correct premise to each goal.
   309        Intro rules with extra Vars in premises still cause some backtracking *)
   310      fun ind_tac [] 0 = all_tac
   311        | ind_tac(prem::prems) i =
   312              DEPTH_SOLVE_1 (ares_tac [prem, @{thm refl}] i) THEN ind_tac prems (i-1);
   313 
   314      val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT);
   315 
   316      val ind_prems = map (induct_prem (map (rpair pred) rec_tms))
   317                          intr_tms;
   318 
   319      val dummy =
   320       if ! Ind_Syntax.trace then
   321         writeln (cat_lines
   322           (["ind_prems:"] @ map (Syntax.string_of_term ctxt1) ind_prems @
   323            ["raw_induct:", Display.string_of_thm ctxt1 raw_induct]))
   324       else ();
   325 
   326 
   327      (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules.
   328        If the premises get simplified, then the proofs could fail.*)
   329      val min_ss = Simplifier.global_context thy empty_ss
   330            setmksimps (K (map mk_eq o ZF_atomize o gen_all))
   331            setSolver (mk_solver "minimal"
   332                       (fn prems => resolve_tac (triv_rls@prems)
   333                                    ORELSE' assume_tac
   334                                    ORELSE' etac @{thm FalseE}));
   335 
   336      val quant_induct =
   337        Goal.prove_global thy1 [] ind_prems
   338          (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
   339          (fn {prems, ...} => EVERY
   340            [rewrite_goals_tac part_rec_defs,
   341             rtac (@{thm impI} RS @{thm allI}) 1,
   342             DETERM (etac raw_induct 1),
   343             (*Push Part inside Collect*)
   344             full_simp_tac (min_ss addsimps [@{thm Part_Collect}]) 1,
   345             (*This CollectE and disjE separates out the introduction rules*)
   346             REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, @{thm disjE}])),
   347             (*Now break down the individual cases.  No disjE here in case
   348               some premise involves disjunction.*)
   349             REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, @{thm exE}, @{thm conjE}]
   350                                ORELSE' bound_hyp_subst_tac)),
   351             ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
   352 
   353      val dummy =
   354       if ! Ind_Syntax.trace then
   355         writeln ("quant_induct:\n" ^ Display.string_of_thm ctxt1 quant_induct)
   356       else ();
   357 
   358 
   359      (*** Prove the simultaneous induction rule ***)
   360 
   361      (*Make distinct predicates for each inductive set*)
   362 
   363      (*The components of the element type, several if it is a product*)
   364      val elem_type = CP.pseudo_type dom_sum;
   365      val elem_factors = CP.factors elem_type;
   366      val elem_frees = mk_frees "za" elem_factors;
   367      val elem_tuple = CP.mk_tuple Pr.pair elem_type elem_frees;
   368 
   369      (*Given a recursive set and its domain, return the "fsplit" predicate
   370        and a conclusion for the simultaneous induction rule.
   371        NOTE.  This will not work for mutually recursive predicates.  Previously
   372        a summand 'domt' was also an argument, but this required the domain of
   373        mutual recursion to invariably be a disjoint sum.*)
   374      fun mk_predpair rec_tm =
   375        let val rec_name = (#1 o dest_Const o head_of) rec_tm
   376            val pfree = Free(pred_name ^ "_" ^ Long_Name.base_name rec_name,
   377                             elem_factors ---> FOLogic.oT)
   378            val qconcl =
   379              List.foldr FOLogic.mk_all
   380                (FOLogic.imp $
   381                 (@{const mem} $ elem_tuple $ rec_tm)
   382                       $ (list_comb (pfree, elem_frees))) elem_frees
   383        in  (CP.ap_split elem_type FOLogic.oT pfree,
   384             qconcl)
   385        end;
   386 
   387      val (preds,qconcls) = split_list (map mk_predpair rec_tms);
   388 
   389      (*Used to form simultaneous induction lemma*)
   390      fun mk_rec_imp (rec_tm,pred) =
   391          FOLogic.imp $ (@{const mem} $ Bound 0 $ rec_tm) $
   392                           (pred $ Bound 0);
   393 
   394      (*To instantiate the main induction rule*)
   395      val induct_concl =
   396          FOLogic.mk_Trueprop
   397            (Ind_Syntax.mk_all_imp
   398             (big_rec_tm,
   399              Abs("z", Ind_Syntax.iT,
   400                  Balanced_Tree.make FOLogic.mk_conj
   401                  (ListPair.map mk_rec_imp (rec_tms, preds)))))
   402      and mutual_induct_concl =
   403       FOLogic.mk_Trueprop (Balanced_Tree.make FOLogic.mk_conj qconcls);
   404 
   405      val dummy = if !Ind_Syntax.trace then
   406                  (writeln ("induct_concl = " ^
   407                            Syntax.string_of_term ctxt1 induct_concl);
   408                   writeln ("mutual_induct_concl = " ^
   409                            Syntax.string_of_term ctxt1 mutual_induct_concl))
   410              else ();
   411 
   412 
   413      val lemma_tac = FIRST' [eresolve_tac [@{thm asm_rl}, @{thm conjE}, @{thm PartE}, @{thm mp}],
   414                              resolve_tac [@{thm allI}, @{thm impI}, @{thm conjI}, @{thm Part_eqI}],
   415                              dresolve_tac [@{thm spec}, @{thm mp}, Pr.fsplitD]];
   416 
   417      val need_mutual = length rec_names > 1;
   418 
   419      val lemma = (*makes the link between the two induction rules*)
   420        if need_mutual then
   421           (writeln "  Proving the mutual induction rule...";
   422            Goal.prove_global thy1 [] []
   423              (Logic.mk_implies (induct_concl, mutual_induct_concl))
   424              (fn _ => EVERY
   425                [rewrite_goals_tac part_rec_defs,
   426                 REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)]))
   427        else (writeln "  [ No mutual induction rule needed ]"; @{thm TrueI});
   428 
   429      val dummy =
   430       if ! Ind_Syntax.trace then
   431         writeln ("lemma: " ^ Display.string_of_thm ctxt1 lemma)
   432       else ();
   433 
   434 
   435      (*Mutual induction follows by freeness of Inl/Inr.*)
   436 
   437      (*Simplification largely reduces the mutual induction rule to the
   438        standard rule*)
   439      val mut_ss =
   440          min_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];
   441 
   442      val all_defs = con_defs @ part_rec_defs;
   443 
   444      (*Removes Collects caused by M-operators in the intro rules.  It is very
   445        hard to simplify
   446          list({v: tf. (v : t --> P_t(v)) & (v : f --> P_f(v))})
   447        where t==Part(tf,Inl) and f==Part(tf,Inr) to  list({v: tf. P_t(v)}).
   448        Instead the following rules extract the relevant conjunct.
   449      *)
   450      val cmonos = [@{thm subset_refl} RS @{thm Collect_mono}] RL monos
   451                    RLN (2,[@{thm rev_subsetD}]);
   452 
   453      (*Minimizes backtracking by delivering the correct premise to each goal*)
   454      fun mutual_ind_tac [] 0 = all_tac
   455        | mutual_ind_tac(prem::prems) i =
   456            DETERM
   457             (SELECT_GOAL
   458                (
   459                 (*Simplify the assumptions and goal by unfolding Part and
   460                   using freeness of the Sum constructors; proves all but one
   461                   conjunct by contradiction*)
   462                 rewrite_goals_tac all_defs  THEN
   463                 simp_tac (mut_ss addsimps [@{thm Part_iff}]) 1  THEN
   464                 IF_UNSOLVED (*simp_tac may have finished it off!*)
   465                   ((*simplify assumptions*)
   466                    (*some risk of excessive simplification here -- might have
   467                      to identify the bare minimum set of rewrites*)
   468                    full_simp_tac
   469                       (mut_ss addsimps @{thms conj_simps} @ @{thms imp_simps} @ @{thms quant_simps}) 1
   470                    THEN
   471                    (*unpackage and use "prem" in the corresponding place*)
   472                    REPEAT (rtac @{thm impI} 1)  THEN
   473                    rtac (rewrite_rule all_defs prem) 1  THEN
   474                    (*prem must not be REPEATed below: could loop!*)
   475                    DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE'
   476                                            eresolve_tac (@{thm conjE} :: @{thm mp} :: cmonos))))
   477                ) i)
   478             THEN mutual_ind_tac prems (i-1);
   479 
   480      val mutual_induct_fsplit =
   481        if need_mutual then
   482          Goal.prove_global thy1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
   483            mutual_induct_concl
   484            (fn {prems, ...} => EVERY
   485              [rtac (quant_induct RS lemma) 1,
   486               mutual_ind_tac (rev prems) (length prems)])
   487        else @{thm TrueI};
   488 
   489      (** Uncurrying the predicate in the ordinary induction rule **)
   490 
   491      (*instantiate the variable to a tuple, if it is non-trivial, in order to
   492        allow the predicate to be "opened up".
   493        The name "x.1" comes from the "RS spec" !*)
   494      val inst =
   495          case elem_frees of [_] => I
   496             | _ => instantiate ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)),
   497                                       cterm_of thy1 elem_tuple)]);
   498 
   499      (*strip quantifier and the implication*)
   500      val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp}));
   501 
   502      val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = concl_of induct0
   503 
   504      val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0)
   505                   |> Drule.export_without_context
   506      and mutual_induct = CP.remove_split mutual_induct_fsplit
   507 
   508      val ([induct', mutual_induct'], thy') =
   509        thy
   510        |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), induct),
   511              [case_names, Induct.induct_pred big_rec_name]),
   512            ((Binding.name "mutual_induct", mutual_induct), [case_names])];
   513     in ((thy', induct'), mutual_induct')
   514     end;  (*of induction_rules*)
   515 
   516   val raw_induct = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.induct)
   517 
   518   val ((thy2, induct), mutual_induct) =
   519     if not coind then induction_rules raw_induct thy1
   520     else
   521       (thy1
   522       |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])]
   523       |> apfst hd |> Library.swap, @{thm TrueI})
   524   and defs = big_rec_def :: part_rec_defs
   525 
   526 
   527   val (([bnd_mono', dom_subset', elim'], [defs', intrs']), thy3) =
   528     thy2
   529     |> IndCases.declare big_rec_name make_cases
   530     |> Global_Theory.add_thms
   531       [((Binding.name "bnd_mono", bnd_mono), []),
   532        ((Binding.name "dom_subset", dom_subset), []),
   533        ((Binding.name "cases", elim), [case_names, Induct.cases_pred big_rec_name])]
   534     ||>> (Global_Theory.add_thmss o map Thm.no_attributes)
   535         [(Binding.name "defs", defs),
   536          (Binding.name "intros", intrs)];
   537   val (intrs'', thy4) =
   538     thy3
   539     |> Global_Theory.add_thms ((map Binding.name intr_names ~~ intrs') ~~ map #2 intr_specs)
   540     ||> Sign.parent_path;
   541   in
   542     (thy4,
   543       {defs = defs',
   544        bnd_mono = bnd_mono',
   545        dom_subset = dom_subset',
   546        intrs = intrs'',
   547        elim = elim',
   548        induct = induct,
   549        mutual_induct = mutual_induct})
   550   end;
   551 
   552 (*source version*)
   553 fun add_inductive (srec_tms, sdom_sum) intr_srcs
   554     (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
   555   let
   556     val ctxt = ProofContext.init_global thy;
   557     val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT)
   558       #> Syntax.check_terms ctxt;
   559 
   560     val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs;
   561     val sintrs = map fst intr_srcs ~~ intr_atts;
   562     val rec_tms = read_terms srec_tms;
   563     val dom_sum = singleton read_terms sdom_sum;
   564     val intr_tms = Syntax.read_props ctxt (map (snd o fst) sintrs);
   565     val intr_specs = (map (fst o fst) sintrs ~~ intr_tms) ~~ map snd sintrs;
   566     val monos = Attrib.eval_thms ctxt raw_monos;
   567     val con_defs = Attrib.eval_thms ctxt raw_con_defs;
   568     val type_intrs = Attrib.eval_thms ctxt raw_type_intrs;
   569     val type_elims = Attrib.eval_thms ctxt raw_type_elims;
   570   in
   571     thy
   572     |> add_inductive_i true (rec_tms, dom_sum) intr_specs (monos, con_defs, type_intrs, type_elims)
   573   end;
   574 
   575 
   576 (* outer syntax *)
   577 
   578 val _ = List.app Keyword.keyword
   579   ["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"];
   580 
   581 fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) =
   582   #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims);
   583 
   584 val ind_decl =
   585   (Parse.$$$ "domains" |-- Parse.!!! (Parse.enum1 "+" Parse.term --
   586       ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.term))) --
   587   (Parse.$$$ "intros" |--
   588     Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) --
   589   Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
   590   Scan.optional (Parse.$$$ "con_defs" |-- Parse.!!! Parse_Spec.xthms1) [] --
   591   Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
   592   Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
   593   >> (Toplevel.theory o mk_ind);
   594 
   595 val _ =
   596   Outer_Syntax.command (co_prefix ^ "inductive")
   597     ("define " ^ co_prefix ^ "inductive sets") Keyword.thy_decl ind_decl;
   598 
   599 end;
   600