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