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