src/ZF/Tools/inductive_package.ML
author wenzelm
Thu Oct 30 16:55:29 2014 +0100 (2014-10-30)
changeset 58838 59203adfc33f
parent 58028 e4250d370657
child 58936 7fbe4436952d
permissions -rw-r--r--
eliminated aliases;
     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) * Token.src list) list ->
    33     (Facts.ref * Token.src list) list * (Facts.ref * Token.src list) list *
    34     (Facts.ref * Token.src list) list * (Facts.ref * Token.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 (Context.theory_name @{theory}) "(co)inductive definitions";
    63   val ctxt = Proof_Context.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 = rec_hds |> forall (fn t => is_Const t orelse
    73       error ("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 = rec_base_names |> forall (fn a => Symbol_Pos.is_identifier a orelse
    82     error ("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 = intr_sets |> forall (fn t => intr_ok t orelse
    90       error ("Conclusion of rule does not name a recursive set: " ^
    91                 Syntax.string_of_term ctxt t));
    92   end;
    93 
    94   val dummy = rec_params |> forall (fn t => is_Free t orelse
    95       error ("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 = singleton (Name.variant_list (List.foldr Misc_Legacy.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 (Misc_Legacy.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 = Proof_Context.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 = Proof_Context.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         [resolve_tac [@{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 ctxt =
   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      resolve_tac [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 ctxt con_defs,
   227      REPEAT (resolve_tac @{thms refl} 2),
   228      (*Typechecking; this can fail*)
   229      if !Ind_Syntax.trace then print_tac ctxt "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 ctxt1)),
   235      if !Ind_Syntax.trace then print_tac ctxt "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 {context = ctxt, ...} => EVERY (rewrite_goals_tac ctxt part_rec_defs :: tacs ctxt)));
   250 
   251   (********)
   252   val dummy = writeln "  Proving the elimination rule...";
   253 
   254   (*Breaks down logical connectives in the monotonic function*)
   255   fun basic_elim_tac ctxt =
   256       REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs)
   257                 ORELSE' bound_hyp_subst_tac ctxt))
   258       THEN prune_params_tac ctxt
   259           (*Mutual recursion: collapse references to Part(D,h)*)
   260       THEN (PRIMITIVE (fold_rule ctxt part_rec_defs));
   261 
   262   (*Elimination*)
   263   val elim =
   264     rule_by_tactic ctxt1 (basic_elim_tac ctxt1) (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 ctxt THEN ALLGOALS (asm_full_simp_tac ctxt) THEN basic_elim_tac ctxt)
   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 xs = subtract (op =) rec_params (Misc_Legacy.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 fold_rev Logic.all xs (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 =
   330            (empty_simpset (Proof_Context.init_global thy)
   331              |> Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all)))
   332            setSolver (mk_solver "minimal"
   333                       (fn ctxt => resolve_tac (triv_rls @ Simplifier.prems_of ctxt)
   334                                    ORELSE' assume_tac
   335                                    ORELSE' eresolve_tac @{thms FalseE}));
   336 
   337      val quant_induct =
   338        Goal.prove_global thy1 [] ind_prems
   339          (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
   340          (fn {context = ctxt, prems} => EVERY
   341            [rewrite_goals_tac ctxt part_rec_defs,
   342             resolve_tac [@{thm impI} RS @{thm allI}] 1,
   343             DETERM (eresolve_tac [raw_induct] 1),
   344             (*Push Part inside Collect*)
   345             full_simp_tac (min_ss addsimps [@{thm Part_Collect}]) 1,
   346             (*This CollectE and disjE separates out the introduction rules*)
   347             REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, @{thm disjE}])),
   348             (*Now break down the individual cases.  No disjE here in case
   349               some premise involves disjunction.*)
   350             REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, @{thm exE}, @{thm conjE}]
   351                                ORELSE' (bound_hyp_subst_tac ctxt1))),
   352             ind_tac (rev (map (rewrite_rule ctxt part_rec_defs) prems)) (length prems)]);
   353 
   354      val dummy =
   355       if ! Ind_Syntax.trace then
   356         writeln ("quant_induct:\n" ^ Display.string_of_thm ctxt1 quant_induct)
   357       else ();
   358 
   359 
   360      (*** Prove the simultaneous induction rule ***)
   361 
   362      (*Make distinct predicates for each inductive set*)
   363 
   364      (*The components of the element type, several if it is a product*)
   365      val elem_type = CP.pseudo_type dom_sum;
   366      val elem_factors = CP.factors elem_type;
   367      val elem_frees = mk_frees "za" elem_factors;
   368      val elem_tuple = CP.mk_tuple Pr.pair elem_type elem_frees;
   369 
   370      (*Given a recursive set and its domain, return the "fsplit" predicate
   371        and a conclusion for the simultaneous induction rule.
   372        NOTE.  This will not work for mutually recursive predicates.  Previously
   373        a summand 'domt' was also an argument, but this required the domain of
   374        mutual recursion to invariably be a disjoint sum.*)
   375      fun mk_predpair rec_tm =
   376        let val rec_name = (#1 o dest_Const o head_of) rec_tm
   377            val pfree = Free(pred_name ^ "_" ^ Long_Name.base_name rec_name,
   378                             elem_factors ---> FOLogic.oT)
   379            val qconcl =
   380              List.foldr FOLogic.mk_all
   381                (FOLogic.imp $
   382                 (@{const mem} $ elem_tuple $ rec_tm)
   383                       $ (list_comb (pfree, elem_frees))) elem_frees
   384        in  (CP.ap_split elem_type FOLogic.oT pfree,
   385             qconcl)
   386        end;
   387 
   388      val (preds,qconcls) = split_list (map mk_predpair rec_tms);
   389 
   390      (*Used to form simultaneous induction lemma*)
   391      fun mk_rec_imp (rec_tm,pred) =
   392          FOLogic.imp $ (@{const mem} $ Bound 0 $ rec_tm) $
   393                           (pred $ Bound 0);
   394 
   395      (*To instantiate the main induction rule*)
   396      val induct_concl =
   397          FOLogic.mk_Trueprop
   398            (Ind_Syntax.mk_all_imp
   399             (big_rec_tm,
   400              Abs("z", Ind_Syntax.iT,
   401                  Balanced_Tree.make FOLogic.mk_conj
   402                  (ListPair.map mk_rec_imp (rec_tms, preds)))))
   403      and mutual_induct_concl =
   404       FOLogic.mk_Trueprop (Balanced_Tree.make FOLogic.mk_conj qconcls);
   405 
   406      val dummy = if !Ind_Syntax.trace then
   407                  (writeln ("induct_concl = " ^
   408                            Syntax.string_of_term ctxt1 induct_concl);
   409                   writeln ("mutual_induct_concl = " ^
   410                            Syntax.string_of_term ctxt1 mutual_induct_concl))
   411              else ();
   412 
   413 
   414      val lemma_tac = FIRST' [eresolve_tac [@{thm asm_rl}, @{thm conjE}, @{thm PartE}, @{thm mp}],
   415                              resolve_tac [@{thm allI}, @{thm impI}, @{thm conjI}, @{thm Part_eqI}],
   416                              dresolve_tac [@{thm spec}, @{thm mp}, Pr.fsplitD]];
   417 
   418      val need_mutual = length rec_names > 1;
   419 
   420      val lemma = (*makes the link between the two induction rules*)
   421        if need_mutual then
   422           (writeln "  Proving the mutual induction rule...";
   423            Goal.prove_global thy1 [] []
   424              (Logic.mk_implies (induct_concl, mutual_induct_concl))
   425              (fn {context = ctxt, ...} => EVERY
   426                [rewrite_goals_tac ctxt part_rec_defs,
   427                 REPEAT (rewrite_goals_tac ctxt [Pr.split_eq] THEN lemma_tac 1)]))
   428        else (writeln "  [ No mutual induction rule needed ]"; @{thm TrueI});
   429 
   430      val dummy =
   431       if ! Ind_Syntax.trace then
   432         writeln ("lemma: " ^ Display.string_of_thm ctxt1 lemma)
   433       else ();
   434 
   435 
   436      (*Mutual induction follows by freeness of Inl/Inr.*)
   437 
   438      (*Simplification largely reduces the mutual induction rule to the
   439        standard rule*)
   440      val mut_ss =
   441          min_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff];
   442 
   443      val all_defs = con_defs @ part_rec_defs;
   444 
   445      (*Removes Collects caused by M-operators in the intro rules.  It is very
   446        hard to simplify
   447          list({v: tf. (v : t --> P_t(v)) & (v : f --> P_f(v))})
   448        where t==Part(tf,Inl) and f==Part(tf,Inr) to  list({v: tf. P_t(v)}).
   449        Instead the following rules extract the relevant conjunct.
   450      *)
   451      val cmonos = [@{thm subset_refl} RS @{thm Collect_mono}] RL monos
   452                    RLN (2,[@{thm rev_subsetD}]);
   453 
   454      (*Minimizes backtracking by delivering the correct premise to each goal*)
   455      fun mutual_ind_tac _ [] 0 = all_tac
   456        | mutual_ind_tac ctxt (prem::prems) i =
   457            DETERM
   458             (SELECT_GOAL
   459                (
   460                 (*Simplify the assumptions and goal by unfolding Part and
   461                   using freeness of the Sum constructors; proves all but one
   462                   conjunct by contradiction*)
   463                 rewrite_goals_tac ctxt all_defs  THEN
   464                 simp_tac (mut_ss addsimps [@{thm Part_iff}]) 1  THEN
   465                 IF_UNSOLVED (*simp_tac may have finished it off!*)
   466                   ((*simplify assumptions*)
   467                    (*some risk of excessive simplification here -- might have
   468                      to identify the bare minimum set of rewrites*)
   469                    full_simp_tac
   470                       (mut_ss addsimps @{thms conj_simps} @ @{thms imp_simps} @ @{thms quant_simps}) 1
   471                    THEN
   472                    (*unpackage and use "prem" in the corresponding place*)
   473                    REPEAT (resolve_tac @{thms impI} 1)  THEN
   474                    resolve_tac [rewrite_rule ctxt all_defs prem] 1  THEN
   475                    (*prem must not be REPEATed below: could loop!*)
   476                    DEPTH_SOLVE (FIRSTGOAL (ares_tac [@{thm impI}] ORELSE'
   477                                            eresolve_tac (@{thm conjE} :: @{thm mp} :: cmonos))))
   478                ) i)
   479             THEN mutual_ind_tac ctxt prems (i-1);
   480 
   481      val mutual_induct_fsplit =
   482        if need_mutual then
   483          Goal.prove_global thy1 [] (map (induct_prem (rec_tms~~preds)) intr_tms)
   484            mutual_induct_concl
   485            (fn {context = ctxt, prems} => EVERY
   486              [resolve_tac [quant_induct RS lemma] 1,
   487               mutual_ind_tac ctxt (rev prems) (length prems)])
   488        else @{thm TrueI};
   489 
   490      (** Uncurrying the predicate in the ordinary induction rule **)
   491 
   492      (*instantiate the variable to a tuple, if it is non-trivial, in order to
   493        allow the predicate to be "opened up".
   494        The name "x.1" comes from the "RS spec" !*)
   495      val inst =
   496          case elem_frees of [_] => I
   497             | _ => Drule.instantiate_normalize ([], [(cterm_of thy1 (Var(("x",1), Ind_Syntax.iT)),
   498                                       cterm_of thy1 elem_tuple)]);
   499 
   500      (*strip quantifier and the implication*)
   501      val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp}));
   502 
   503      val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = concl_of induct0
   504 
   505      val induct =
   506        CP.split_rule_var (Proof_Context.init_global thy)
   507         (pred_var, elem_type-->FOLogic.oT, induct0)
   508        |> Drule.export_without_context
   509      and mutual_induct = CP.remove_split (Proof_Context.init_global thy) mutual_induct_fsplit
   510 
   511      val ([induct', mutual_induct'], thy') =
   512        thy
   513        |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), induct),
   514              [case_names, Induct.induct_pred big_rec_name]),
   515            ((Binding.name "mutual_induct", mutual_induct), [case_names])];
   516     in ((thy', induct'), mutual_induct')
   517     end;  (*of induction_rules*)
   518 
   519   val raw_induct = Drule.export_without_context ([big_rec_def, bnd_mono] MRS Fp.induct)
   520 
   521   val ((thy2, induct), mutual_induct) =
   522     if not coind then induction_rules raw_induct thy1
   523     else
   524       (thy1
   525       |> Global_Theory.add_thms [((Binding.name (co_prefix ^ "induct"), raw_induct), [])]
   526       |> apfst hd |> Library.swap, @{thm TrueI})
   527   and defs = big_rec_def :: part_rec_defs
   528 
   529 
   530   val (([bnd_mono', dom_subset', elim'], [defs', intrs']), thy3) =
   531     thy2
   532     |> IndCases.declare big_rec_name make_cases
   533     |> Global_Theory.add_thms
   534       [((Binding.name "bnd_mono", bnd_mono), []),
   535        ((Binding.name "dom_subset", dom_subset), []),
   536        ((Binding.name "cases", elim), [case_names, Induct.cases_pred big_rec_name])]
   537     ||>> (Global_Theory.add_thmss o map Thm.no_attributes)
   538         [(Binding.name "defs", defs),
   539          (Binding.name "intros", intrs)];
   540   val (intrs'', thy4) =
   541     thy3
   542     |> Global_Theory.add_thms ((map Binding.name intr_names ~~ intrs') ~~ map #2 intr_specs)
   543     ||> Sign.parent_path;
   544   in
   545     (thy4,
   546       {defs = defs',
   547        bnd_mono = bnd_mono',
   548        dom_subset = dom_subset',
   549        intrs = intrs'',
   550        elim = elim',
   551        induct = induct,
   552        mutual_induct = mutual_induct})
   553   end;
   554 
   555 (*source version*)
   556 fun add_inductive (srec_tms, sdom_sum) intr_srcs
   557     (raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy =
   558   let
   559     val ctxt = Proof_Context.init_global thy;
   560     val read_terms = map (Syntax.parse_term ctxt #> Type.constraint Ind_Syntax.iT)
   561       #> Syntax.check_terms ctxt;
   562 
   563     val intr_atts = map (map (Attrib.attribute_cmd ctxt) o snd) intr_srcs;
   564     val sintrs = map fst intr_srcs ~~ intr_atts;
   565     val rec_tms = read_terms srec_tms;
   566     val dom_sum = singleton read_terms sdom_sum;
   567     val intr_tms = Syntax.read_props ctxt (map (snd o fst) sintrs);
   568     val intr_specs = (map (fst o fst) sintrs ~~ intr_tms) ~~ map snd sintrs;
   569     val monos = Attrib.eval_thms ctxt raw_monos;
   570     val con_defs = Attrib.eval_thms ctxt raw_con_defs;
   571     val type_intrs = Attrib.eval_thms ctxt raw_type_intrs;
   572     val type_elims = Attrib.eval_thms ctxt raw_type_elims;
   573   in
   574     thy
   575     |> add_inductive_i true (rec_tms, dom_sum) intr_specs (monos, con_defs, type_intrs, type_elims)
   576   end;
   577 
   578 
   579 (* outer syntax *)
   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   (@{keyword "domains"} |-- Parse.!!! (Parse.enum1 "+" Parse.term --
   586       ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.term))) --
   587   (@{keyword "intros"} |--
   588     Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) --
   589   Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse.xthms1) [] --
   590   Scan.optional (@{keyword "con_defs"} |-- Parse.!!! Parse.xthms1) [] --
   591   Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse.xthms1) [] --
   592   Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse.xthms1) []
   593   >> (Toplevel.theory o mk_ind);
   594 
   595 val _ =
   596   Outer_Syntax.command
   597     (if coind then @{command_spec "coinductive"} else @{command_spec "inductive"})
   598     ("define " ^ co_prefix ^ "inductive sets") ind_decl;
   599 
   600 end;
   601