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