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