src/HOL/Tools/inductive_package.ML
author berghofe
Thu Jun 15 16:02:12 2000 +0200 (2000-06-15)
changeset 9072 a4896cf23638
parent 8720 840c75ab2a7f
child 9116 9df44b5c610b
permissions -rw-r--r--
Now also proves monotonicity when in quick_and_dirty mode.
     1 (*  Title:      HOL/Tools/inductive_package.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4                 Stefan Berghofer,   TU Muenchen
     5     Copyright   1994  University of Cambridge
     6                 1998  TU Muenchen     
     7 
     8 (Co)Inductive Definition module for HOL.
     9 
    10 Features:
    11   * least or greatest fixedpoints
    12   * user-specified product and sum constructions
    13   * mutually recursive definitions
    14   * definitions involving arbitrary monotone operators
    15   * automatically proves introduction and elimination rules
    16 
    17 The recursive sets must *already* be declared as constants in the
    18 current theory!
    19 
    20   Introduction rules have the form
    21   [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk
    22   where M is some monotone operator (usually the identity)
    23   P(x) is any side condition on the free variables
    24   ti, t are any terms
    25   Sj, Sk are two of the sets being defined in mutual recursion
    26 
    27 Sums are used only for mutual recursion.  Products are used only to
    28 derive "streamlined" induction rules for relations.
    29 *)
    30 
    31 signature INDUCTIVE_PACKAGE =
    32 sig
    33   val quiet_mode: bool ref
    34   val unify_consts: Sign.sg -> term list -> term list -> term list * term list
    35   val get_inductive: theory -> string ->
    36     {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
    37       induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    38   val print_inductives: theory -> unit
    39   val mono_add_global: theory attribute
    40   val mono_del_global: theory attribute
    41   val get_monos: theory -> thm list
    42   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    43     theory attribute list -> ((bstring * term) * theory attribute list) list ->
    44       thm list -> thm list -> theory -> theory *
    45       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    46        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    47   val add_inductive: bool -> bool -> string list -> Args.src list ->
    48     ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
    49       (xstring * Args.src list) list -> theory -> theory *
    50       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    51        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    52   val inductive_cases: (((bstring * Args.src list) * xstring) * string list) * Comment.text
    53     -> theory -> theory
    54   val inductive_cases_i: (((bstring * theory attribute list) * string) * term list) * Comment.text
    55     -> theory -> theory
    56   val setup: (theory -> theory) list
    57 end;
    58 
    59 structure InductivePackage: INDUCTIVE_PACKAGE =
    60 struct
    61 
    62 (*** theory data ***)
    63 
    64 (* data kind 'HOL/inductive' *)
    65 
    66 type inductive_info =
    67   {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
    68     induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
    69 
    70 structure InductiveArgs =
    71 struct
    72   val name = "HOL/inductive";
    73   type T = inductive_info Symtab.table * thm list;
    74 
    75   val empty = (Symtab.empty, []);
    76   val copy = I;
    77   val prep_ext = I;
    78   fun merge ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2),
    79     Library.generic_merge Thm.eq_thm I I monos1 monos2);
    80 
    81   fun print sg (tab, monos) =
    82     [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
    83      Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)]
    84     |> Pretty.chunks |> Pretty.writeln;
    85 end;
    86 
    87 structure InductiveData = TheoryDataFun(InductiveArgs);
    88 val print_inductives = InductiveData.print;
    89 
    90 
    91 (* get and put data *)
    92 
    93 fun get_inductive thy name =
    94   (case Symtab.lookup (fst (InductiveData.get thy), name) of
    95     Some info => info
    96   | None => error ("Unknown (co)inductive set " ^ quote name));
    97 
    98 fun put_inductives names info thy =
    99   let
   100     fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
   101     val tab_monos = foldl upd (InductiveData.get thy, names)
   102       handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
   103   in InductiveData.put tab_monos thy end;
   104 
   105 
   106 
   107 (** monotonicity rules **)
   108 
   109 val get_monos = snd o InductiveData.get;
   110 fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy;
   111 
   112 fun mk_mono thm =
   113   let
   114     fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @
   115       (case concl_of thm of
   116           (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
   117         | _ => [standard (thm' RS (thm' RS eq_to_mono2))]);
   118     val concl = concl_of thm
   119   in
   120     if Logic.is_equals concl then
   121       eq2mono (thm RS meta_eq_to_obj_eq)
   122     else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
   123       eq2mono thm
   124     else [thm]
   125   end;
   126 
   127 
   128 (* attributes *)
   129 
   130 local
   131 
   132 fun map_rules_global f thy = put_monos (f (get_monos thy)) thy;
   133 
   134 fun add_mono thm rules = Library.gen_union Thm.eq_thm (mk_mono thm, rules);
   135 fun del_mono thm rules = Library.gen_rems Thm.eq_thm (rules, mk_mono thm);
   136 
   137 fun mk_att f g (x, thm) = (f (g thm) x, thm);
   138 
   139 in
   140   val mono_add_global = mk_att map_rules_global add_mono;
   141   val mono_del_global = mk_att map_rules_global del_mono;
   142 end;
   143 
   144 val mono_attr =
   145  (Attrib.add_del_args mono_add_global mono_del_global,
   146   Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute);
   147 
   148 
   149 
   150 (** utilities **)
   151 
   152 (* messages *)
   153 
   154 val quiet_mode = ref false;
   155 fun message s = if !quiet_mode then () else writeln s;
   156 
   157 fun coind_prefix true = "co"
   158   | coind_prefix false = "";
   159 
   160 
   161 (* the following code ensures that each recursive set *)
   162 (* always has the same type in all introduction rules *)
   163 
   164 fun unify_consts sign cs intr_ts =
   165   (let
   166     val {tsig, ...} = Sign.rep_sg sign;
   167     val add_term_consts_2 =
   168       foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
   169     fun varify (t, (i, ts)) =
   170       let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
   171       in (maxidx_of_term t', t'::ts) end;
   172     val (i, cs') = foldr varify (cs, (~1, []));
   173     val (i', intr_ts') = foldr varify (intr_ts, (i, []));
   174     val rec_consts = foldl add_term_consts_2 ([], cs');
   175     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
   176     fun unify (env, (cname, cT)) =
   177       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
   178       in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
   179           (env, (replicate (length consts) cT) ~~ consts)
   180       end;
   181     val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts);
   182     fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T
   183       in if T = T' then T else typ_subst_TVars_2 env T' end;
   184     val subst = fst o Type.freeze_thaw o
   185       (map_term_types (typ_subst_TVars_2 env))
   186 
   187   in (map subst cs', map subst intr_ts')
   188   end) handle Type.TUNIFY =>
   189     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
   190 
   191 
   192 (* misc *)
   193 
   194 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD);
   195 
   196 val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``";
   197 val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
   198 
   199 (* make injections needed in mutually recursive definitions *)
   200 
   201 fun mk_inj cs sumT c x =
   202   let
   203     fun mk_inj' T n i =
   204       if n = 1 then x else
   205       let val n2 = n div 2;
   206           val Type (_, [T1, T2]) = T
   207       in
   208         if i <= n2 then
   209           Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i)
   210         else
   211           Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
   212       end
   213   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
   214   end;
   215 
   216 (* make "vimage" terms for selecting out components of mutually rec.def. *)
   217 
   218 fun mk_vimage cs sumT t c = if length cs < 2 then t else
   219   let
   220     val cT = HOLogic.dest_setT (fastype_of c);
   221     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
   222   in
   223     Const (vimage_name, vimageT) $
   224       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t
   225   end;
   226 
   227 
   228 
   229 (** well-formedness checks **)
   230 
   231 fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^
   232   (Sign.string_of_term sign t) ^ "\n" ^ msg);
   233 
   234 fun err_in_prem sign t p msg = error ("Ill-formed premise\n" ^
   235   (Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^
   236   (Sign.string_of_term sign t) ^ "\n" ^ msg);
   237 
   238 val msg1 = "Conclusion of introduction rule must have form\
   239           \ ' t : S_i '";
   240 val msg2 = "Non-atomic premise";
   241 val msg3 = "Recursion term on left of member symbol";
   242 
   243 fun check_rule sign cs r =
   244   let
   245     fun check_prem prem = if can HOLogic.dest_Trueprop prem then ()
   246       else err_in_prem sign r prem msg2;
   247 
   248   in (case HOLogic.dest_Trueprop (Logic.strip_imp_concl r) of
   249         (Const ("op :", _) $ t $ u) =>
   250           if u mem cs then
   251             if exists (Logic.occs o (rpair t)) cs then
   252               err_in_rule sign r msg3
   253             else
   254               seq check_prem (Logic.strip_imp_prems r)
   255           else err_in_rule sign r msg1
   256       | _ => err_in_rule sign r msg1)
   257   end;
   258 
   259 fun try' f msg sign t = (case (try f t) of
   260       Some x => x
   261     | None => error (msg ^ Sign.string_of_term sign t));
   262 
   263 
   264 
   265 (*** properties of (co)inductive sets ***)
   266 
   267 (** elimination rules **)
   268 
   269 fun mk_elims cs cTs params intr_ts intr_names =
   270   let
   271     val used = foldr add_term_names (intr_ts, []);
   272     val [aname, pname] = variantlist (["a", "P"], used);
   273     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
   274 
   275     fun dest_intr r =
   276       let val Const ("op :", _) $ t $ u =
   277         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   278       in (u, t, Logic.strip_imp_prems r) end;
   279 
   280     val intrs = map dest_intr intr_ts ~~ intr_names;
   281 
   282     fun mk_elim (c, T) =
   283       let
   284         val a = Free (aname, T);
   285 
   286         fun mk_elim_prem (_, t, ts) =
   287           list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
   288             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
   289         val c_intrs = (filter (equal c o #1 o #1) intrs);
   290       in
   291         (Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
   292           map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs)
   293       end
   294   in
   295     map mk_elim (cs ~~ cTs)
   296   end;
   297         
   298 
   299 
   300 (** premises and conclusions of induction rules **)
   301 
   302 fun mk_indrule cs cTs params intr_ts =
   303   let
   304     val used = foldr add_term_names (intr_ts, []);
   305 
   306     (* predicates for induction rule *)
   307 
   308     val preds = map Free (variantlist (if length cs < 2 then ["P"] else
   309       map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
   310         map (fn T => T --> HOLogic.boolT) cTs);
   311 
   312     (* transform an introduction rule into a premise for induction rule *)
   313 
   314     fun mk_ind_prem r =
   315       let
   316         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   317 
   318         val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
   319 
   320         fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
   321               (case pred_of u of
   322                   None => (m $ fst (subst t) $ fst (subst u), None)
   323                 | Some P => (HOLogic.conj $ s $ (P $ t), Some (s, P $ t)))
   324           | subst s =
   325               (case pred_of s of
   326                   Some P => (HOLogic.mk_binop "op Int"
   327                     (s, HOLogic.Collect_const (HOLogic.dest_setT
   328                       (fastype_of s)) $ P), None)
   329                 | None => (case s of
   330                      (t $ u) => (fst (subst t) $ fst (subst u), None)
   331                    | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None)
   332                    | _ => (s, None)));
   333 
   334         fun mk_prem (s, prems) = (case subst s of
   335               (_, Some (t, u)) => t :: u :: prems
   336             | (t, _) => t :: prems);
   337           
   338         val Const ("op :", _) $ t $ u =
   339           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   340 
   341       in list_all_free (frees,
   342            Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
   343              (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
   344                HOLogic.mk_Trueprop (the (pred_of u) $ t)))
   345       end;
   346 
   347     val ind_prems = map mk_ind_prem intr_ts;
   348 
   349     (* make conclusions for induction rules *)
   350 
   351     fun mk_ind_concl ((c, P), (ts, x)) =
   352       let val T = HOLogic.dest_setT (fastype_of c);
   353           val Ts = HOLogic.prodT_factors T;
   354           val (frees, x') = foldr (fn (T', (fs, s)) =>
   355             ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
   356           val tuple = HOLogic.mk_tuple T frees;
   357       in ((HOLogic.mk_binop "op -->"
   358         (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
   359       end;
   360 
   361     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   362         (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
   363 
   364   in (preds, ind_prems, mutual_ind_concl)
   365   end;
   366 
   367 
   368 
   369 (** prepare cases and induct rules **)
   370 
   371 (*
   372   transform mutual rule:
   373     HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
   374   into i-th projection:
   375     xi:Ai ==> HH ==> Pi xi
   376 *)
   377 
   378 fun project_rules [name] rule = [(name, rule)]
   379   | project_rules names mutual_rule =
   380       let
   381         val n = length names;
   382         fun proj i =
   383           (if i < n then (fn th => th RS conjunct1) else I)
   384             (Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule)
   385             RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
   386       in names ~~ map proj (1 upto n) end;
   387 
   388 fun add_cases_induct no_elim no_ind names elims induct induct_cases =
   389   let
   390     fun cases_spec (name, elim) = (("", elim), [InductMethod.cases_set_global name]);
   391     val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
   392 
   393     fun induct_spec (name, th) =
   394       (("", th), [RuleCases.case_names induct_cases, InductMethod.induct_set_global name]);
   395     val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct);
   396   in #1 o PureThy.add_thms (cases_specs @ induct_specs) end;
   397 
   398 
   399 
   400 (*** proofs for (co)inductive sets ***)
   401 
   402 (** prove monotonicity **)
   403 
   404 fun prove_mono setT fp_fun monos thy =
   405   let
   406     val _ = message "  Proving monotonicity ...";
   407 
   408     val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
   409       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
   410         (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)])
   411 
   412   in mono end;
   413 
   414 
   415 
   416 (** prove introduction rules **)
   417 
   418 fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
   419   let
   420     val _ = message "  Proving the introduction rules ...";
   421 
   422     val unfold = standard (mono RS (fp_def RS
   423       (if coind then def_gfp_Tarski else def_lfp_Tarski)));
   424 
   425     fun select_disj 1 1 = []
   426       | select_disj _ 1 = [rtac disjI1]
   427       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
   428 
   429     val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
   430       (cterm_of (Theory.sign_of thy) intr) (fn prems =>
   431        [(*insert prems and underlying sets*)
   432        cut_facts_tac prems 1,
   433        stac unfold 1,
   434        REPEAT (resolve_tac [vimageI2, CollectI] 1),
   435        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
   436        EVERY1 (select_disj (length intr_ts) i),
   437        (*Not ares_tac, since refl must be tried before any equality assumptions;
   438          backtracking may occur if the premises have extra variables!*)
   439        DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
   440        (*Now solve the equations like Inl 0 = Inl ?b2*)
   441        rewrite_goals_tac con_defs,
   442        REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts)
   443 
   444   in (intrs, unfold) end;
   445 
   446 
   447 
   448 (** prove elimination rules **)
   449 
   450 fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy =
   451   let
   452     val _ = message "  Proving the elimination rules ...";
   453 
   454     val rules1 = [CollectE, disjE, make_elim vimageD, exE];
   455     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @
   456       map make_elim [Inl_inject, Inr_inject];
   457   in
   458     map (fn (t, cases) => prove_goalw_cterm rec_sets_defs
   459       (cterm_of (Theory.sign_of thy) t) (fn prems =>
   460         [cut_facts_tac [hd prems] 1,
   461          dtac (unfold RS subst) 1,
   462          REPEAT (FIRSTGOAL (eresolve_tac rules1)),
   463          REPEAT (FIRSTGOAL (eresolve_tac rules2)),
   464          EVERY (map (fn prem =>
   465            DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
   466       |> RuleCases.name cases)
   467       (mk_elims cs cTs params intr_ts intr_names)
   468   end;
   469 
   470 
   471 (** derivation of simplified elimination rules **)
   472 
   473 (*Applies freeness of the given constructors, which *must* be unfolded by
   474   the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   475   for inference systems.
   476  *)
   477 
   478 (*cprop should have the form t:Si where Si is an inductive set*)
   479 fun mk_cases_i solved elims ss cprop =
   480   let
   481     val prem = Thm.assume cprop;
   482     val tac = if solved then InductMethod.con_elim_solved_tac else InductMethod.con_elim_tac;
   483     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic (tac ss) (prem RS rl));
   484   in
   485     (case get_first (try mk_elim) elims of
   486       Some r => r
   487     | None => error (Pretty.string_of (Pretty.block
   488         [Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk,
   489           Display.pretty_cterm cprop])))
   490   end;
   491 
   492 fun mk_cases elims s =
   493   mk_cases_i false elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
   494 
   495 
   496 (* inductive_cases(_i) *)
   497 
   498 fun gen_inductive_cases prep_att prep_const prep_prop
   499     ((((name, raw_atts), raw_set), raw_props), comment) thy =
   500   let
   501     val sign = Theory.sign_of thy;
   502 
   503     val atts = map (prep_att thy) raw_atts;
   504     val (_, {elims, ...}) = get_inductive thy (prep_const sign raw_set);
   505     val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
   506     val thms = map (mk_cases_i true elims (Simplifier.simpset_of thy)) cprops;
   507   in
   508     thy
   509     |> IsarThy.have_theorems_i (((name, atts), map Thm.no_attributes thms), comment)
   510   end;
   511 
   512 val inductive_cases =
   513   gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
   514 
   515 val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop;
   516 
   517 
   518 
   519 (** prove induction rule **)
   520 
   521 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
   522     fp_def rec_sets_defs thy =
   523   let
   524     val _ = message "  Proving the induction rule ...";
   525 
   526     val sign = Theory.sign_of thy;
   527 
   528     val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
   529         None => []
   530       | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
   531 
   532     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   533 
   534     (* make predicate for instantiation of abstract induction rule *)
   535 
   536     fun mk_ind_pred _ [P] = P
   537       | mk_ind_pred T Ps =
   538          let val n = (length Ps) div 2;
   539              val Type (_, [T1, T2]) = T
   540          in Const ("Datatype.sum.sum_case",
   541            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
   542              mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
   543          end;
   544 
   545     val ind_pred = mk_ind_pred sumT preds;
   546 
   547     val ind_concl = HOLogic.mk_Trueprop
   548       (HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->"
   549         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0)));
   550 
   551     (* simplification rules for vimage and Collect *)
   552 
   553     val vimage_simps = if length cs < 2 then [] else
   554       map (fn c => prove_goalw_cterm [] (cterm_of sign
   555         (HOLogic.mk_Trueprop (HOLogic.mk_eq
   556           (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   557            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   558              nth_elem (find_index_eq c cs, preds)))))
   559         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites,
   560           rtac refl 1])) cs;
   561 
   562     val induct = prove_goalw_cterm [] (cterm_of sign
   563       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   564         [rtac (impI RS allI) 1,
   565          DETERM (etac (mono RS (fp_def RS def_induct)) 1),
   566          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
   567          fold_goals_tac rec_sets_defs,
   568          (*This CollectE and disjE separates out the introduction rules*)
   569          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
   570          (*Now break down the individual cases.  No disjE here in case
   571            some premise involves disjunction.*)
   572          REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
   573          rewrite_goals_tac sum_case_rewrites,
   574          EVERY (map (fn prem =>
   575            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
   576 
   577     val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
   578       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
   579         [cut_facts_tac prems 1,
   580          REPEAT (EVERY
   581            [REPEAT (resolve_tac [conjI, impI] 1),
   582             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
   583             rewrite_goals_tac sum_case_rewrites,
   584             atac 1])])
   585 
   586   in standard (split_rule (induct RS lemma))
   587   end;
   588 
   589 
   590 
   591 (*** specification of (co)inductive sets ****)
   592 
   593 (** definitional introduction of (co)inductive sets **)
   594 
   595 fun mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   596       params paramTs cTs cnames =
   597   let
   598     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
   599     val setT = HOLogic.mk_setT sumT;
   600 
   601     val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
   602       else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";
   603 
   604     val used = foldr add_term_names (intr_ts, []);
   605     val [sname, xname] = variantlist (["S", "x"], used);
   606 
   607     (* transform an introduction rule into a conjunction  *)
   608     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
   609     (* is transformed into                                *)
   610     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
   611 
   612     fun transform_rule r =
   613       let
   614         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   615         val subst = subst_free
   616           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
   617         val Const ("op :", _) $ t $ u =
   618           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   619 
   620       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
   621         (frees, foldr1 HOLogic.mk_conj
   622           (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
   623             (map (subst o HOLogic.dest_Trueprop)
   624               (Logic.strip_imp_prems r))))
   625       end
   626 
   627     (* make a disjunction of all introduction rules *)
   628 
   629     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
   630       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
   631 
   632     (* add definiton of recursive sets to theory *)
   633 
   634     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
   635     val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
   636 
   637     val rec_const = list_comb
   638       (Const (full_rec_name, paramTs ---> setT), params);
   639 
   640     val fp_def_term = Logic.mk_equals (rec_const,
   641       Const (fp_name, (setT --> setT) --> setT) $ fp_fun)
   642 
   643     val def_terms = fp_def_term :: (if length cs < 2 then [] else
   644       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
   645 
   646     val (thy', [fp_def :: rec_sets_defs]) =
   647       thy
   648       |> (if declare_consts then
   649           Theory.add_consts_i (map (fn (c, n) =>
   650             (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   651           else I)
   652       |> (if length cs < 2 then I
   653           else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
   654       |> Theory.add_path rec_name
   655       |> PureThy.add_defss_i [(("defs", def_terms), [])];
   656 
   657     val mono = prove_mono setT fp_fun monos thy'
   658 
   659   in
   660     (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) 
   661   end;
   662 
   663 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   664     atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
   665   let
   666     val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
   667       commas_quote cnames) else ();
   668 
   669     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   670 
   671     val (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) =
   672       mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   673         params paramTs cTs cnames;
   674 
   675     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
   676       rec_sets_defs thy';
   677     val elims = if no_elim then [] else
   678       prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy';
   679     val raw_induct = if no_ind then Drule.asm_rl else
   680       if coind then standard (rule_by_tactic
   681         (rewrite_tac [mk_meta_eq vimage_Un] THEN
   682           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
   683       else
   684         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
   685           rec_sets_defs thy';
   686     val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
   687       else standard (raw_induct RSN (2, rev_mp));
   688 
   689     val (thy'', [intrs']) =
   690       thy'
   691       |> PureThy.add_thmss [(("intrs", intrs), atts)]
   692       |>> (#1 o PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts))
   693       |>> (if no_elim then I else #1 o PureThy.add_thmss [(("elims", elims), [])])
   694       |>> (if no_ind then I else #1 o PureThy.add_thms
   695         [((coind_prefix coind ^ "induct", induct), [RuleCases.case_names induct_cases])])
   696       |>> Theory.parent_path;
   697     val elims' = if no_elim then elims else PureThy.get_thms thy'' "elims";  (* FIXME improve *)
   698     val induct' = if no_ind then induct else PureThy.get_thm thy'' (coind_prefix coind ^ "induct");  (* FIXME improve *)
   699   in (thy'',
   700     {defs = fp_def::rec_sets_defs,
   701      mono = mono,
   702      unfold = unfold,
   703      intrs = intrs',
   704      elims = elims',
   705      mk_cases = mk_cases elims',
   706      raw_induct = raw_induct,
   707      induct = induct'})
   708   end;
   709 
   710 
   711 
   712 (** axiomatic introduction of (co)inductive sets **)
   713 
   714 fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
   715     atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
   716   let
   717     val _ = message (coind_prefix coind ^ "inductive set(s) " ^ commas_quote cnames);
   718 
   719     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   720     val (thy', _, _, _, _, _) =
   721       mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   722         params paramTs cTs cnames;
   723     val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names);
   724     val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   725     val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
   726     
   727     val thy'' =
   728       thy'
   729       |> (#1 o PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("raw_elims", elim_ts), [])])
   730       |> (if coind then I else
   731             #1 o PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
   732 
   733     val intrs = PureThy.get_thms thy'' "intrs";
   734     val elims = map2 (fn (th, cases) => RuleCases.name cases th)
   735       (PureThy.get_thms thy'' "raw_elims", elim_cases);
   736     val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy'' "raw_induct";
   737     val induct = if coind orelse length cs > 1 then raw_induct
   738       else standard (raw_induct RSN (2, rev_mp));
   739 
   740     val (thy''', ([elims'], intrs')) =
   741       thy''
   742       |> PureThy.add_thmss [(("elims", elims), [])]
   743       |>> (if coind then I
   744           else #1 o PureThy.add_thms [(("induct", induct), [RuleCases.case_names induct_cases])])
   745       |>>> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
   746       |>> Theory.parent_path;
   747     val induct' = if coind then raw_induct else PureThy.get_thm thy''' "induct";
   748   in (thy''',
   749     {defs = [],
   750      mono = Drule.asm_rl,
   751      unfold = Drule.asm_rl,
   752      intrs = intrs',
   753      elims = elims',
   754      mk_cases = mk_cases elims',
   755      raw_induct = raw_induct,
   756      induct = induct'})
   757   end;
   758 
   759 
   760 
   761 (** introduction of (co)inductive sets **)
   762 
   763 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
   764     atts intros monos con_defs thy =
   765   let
   766     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
   767     val sign = Theory.sign_of thy;
   768 
   769     (*parameters should agree for all mutually recursive components*)
   770     val (_, params) = strip_comb (hd cs);
   771     val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\
   772       \ component is not a free variable: " sign) params;
   773 
   774     val cTs = map (try' (HOLogic.dest_setT o fastype_of)
   775       "Recursive component not of type set: " sign) cs;
   776 
   777     val full_cnames = map (try' (fst o dest_Const o head_of)
   778       "Recursive set not previously declared as constant: " sign) cs;
   779     val cnames = map Sign.base_name full_cnames;
   780 
   781     val _ = seq (check_rule sign cs o snd o fst) intros;
   782     val induct_cases = map (#1 o #1) intros;
   783 
   784     val (thy1, result) =
   785       (if ! quick_and_dirty then add_ind_axm else add_ind_def)
   786         verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
   787         con_defs thy params paramTs cTs cnames induct_cases;
   788     val thy2 = thy1
   789       |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
   790       |> add_cases_induct no_elim (no_ind orelse coind) full_cnames
   791           (#elims result) (#induct result) induct_cases;
   792   in (thy2, result) end;
   793 
   794 
   795 
   796 (** external interface **)
   797 
   798 fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
   799   let
   800     val sign = Theory.sign_of thy;
   801     val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
   802 
   803     val atts = map (Attrib.global_attribute thy) srcs;
   804     val intr_names = map (fst o fst) intro_srcs;
   805     val intr_ts = map (term_of o Thm.read_cterm sign o rpair propT o snd o fst) intro_srcs;
   806     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
   807     val (cs', intr_ts') = unify_consts sign cs intr_ts;
   808 
   809     val ((thy', con_defs), monos) = thy
   810       |> IsarThy.apply_theorems raw_monos
   811       |> apfst (IsarThy.apply_theorems raw_con_defs);
   812   in
   813     add_inductive_i verbose false "" coind false false cs'
   814       atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
   815   end;
   816 
   817 
   818 
   819 (** package setup **)
   820 
   821 (* setup theory *)
   822 
   823 val setup =
   824  [InductiveData.init,
   825   Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]];
   826 
   827 
   828 (* outer syntax *)
   829 
   830 local structure P = OuterParse and K = OuterSyntax.Keyword in
   831 
   832 fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
   833   #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
   834 
   835 fun ind_decl coind =
   836   (Scan.repeat1 P.term --| P.marg_comment) --
   837   (P.$$$ "intrs" |--
   838     P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
   839   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
   840   Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
   841   >> (Toplevel.theory o mk_ind coind);
   842 
   843 val inductiveP =
   844   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
   845 
   846 val coinductiveP =
   847   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
   848 
   849 
   850 val ind_cases =
   851   P.opt_thm_name "=" -- P.xname --| P.$$$ ":" -- Scan.repeat1 P.prop -- P.marg_comment
   852   >> (Toplevel.theory o inductive_cases);
   853 
   854 val inductive_casesP =
   855   OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules"
   856     K.thy_decl ind_cases;
   857 
   858 val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"];
   859 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
   860 
   861 end;
   862 
   863 
   864 end;