src/HOL/Tools/inductive_package.ML
author wenzelm
Sat Dec 01 18:52:32 2001 +0100 (2001-12-01 ago)
changeset 12338 de0f4a63baa5
parent 12311 ce5f9e61c037
child 12400 f12f95e216e0
permissions -rw-r--r--
renamed class "term" to "type" (actually "HOL.type");
     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     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     7 
     8 (Co)Inductive Definition module for HOL.
     9 
    10 Features:
    11   * least or greatest fixedpoints
    12   * user-specified product and sum constructions
    13   * mutually recursive definitions
    14   * definitions involving arbitrary monotone operators
    15   * automatically proves introduction and elimination rules
    16 
    17 The recursive sets must *already* be declared as constants in the
    18 current theory!
    19 
    20   Introduction rules have the form
    21   [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk
    22   where M is some monotone operator (usually the identity)
    23   P(x) is any side condition on the free variables
    24   ti, t are any terms
    25   Sj, Sk are two of the sets being defined in mutual recursion
    26 
    27 Sums are used only for mutual recursion.  Products are used only to
    28 derive "streamlined" induction rules for relations.
    29 *)
    30 
    31 signature INDUCTIVE_PACKAGE =
    32 sig
    33   val quiet_mode: bool ref
    34   val unify_consts: Sign.sg -> term list -> term list -> term list * term list
    35   val 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 print_inductives: theory -> unit
    40   val mono_add_global: theory attribute
    41   val mono_del_global: theory attribute
    42   val get_monos: theory -> thm list
    43   val inductive_forall_name: string
    44   val inductive_forall_def: thm
    45   val rulify: thm -> thm
    46   val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
    47     -> theory -> theory
    48   val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
    49     -> theory -> theory
    50   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    51     ((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
    52       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    53        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    54   val add_inductive: bool -> bool -> string list ->
    55     ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
    56     theory -> theory *
    57       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    58        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    59   val setup: (theory -> theory) list
    60 end;
    61 
    62 structure InductivePackage: INDUCTIVE_PACKAGE =
    63 struct
    64 
    65 
    66 (** theory context references **)
    67 
    68 val mono_name = "HOL.mono";
    69 val gfp_name = "Gfp.gfp";
    70 val lfp_name = "Lfp.lfp";
    71 val vimage_name = "Set.vimage";
    72 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
    73 
    74 val inductive_forall_name = "HOL.induct_forall";
    75 val inductive_forall_def = thm "induct_forall_def";
    76 val inductive_conj_name = "HOL.induct_conj";
    77 val inductive_conj_def = thm "induct_conj_def";
    78 val inductive_conj = thms "induct_conj";
    79 val inductive_atomize = thms "induct_atomize";
    80 val inductive_rulify1 = thms "induct_rulify1";
    81 val inductive_rulify2 = thms "induct_rulify2";
    82 
    83 
    84 
    85 (** theory data **)
    86 
    87 (* data kind 'HOL/inductive' *)
    88 
    89 type inductive_info =
    90   {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
    91     induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
    92 
    93 structure InductiveArgs =
    94 struct
    95   val name = "HOL/inductive";
    96   type T = inductive_info Symtab.table * thm list;
    97 
    98   val empty = (Symtab.empty, []);
    99   val copy = I;
   100   val prep_ext = I;
   101   fun merge ((tab1, monos1), (tab2, monos2)) =
   102     (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
   103 
   104   fun print sg (tab, monos) =
   105     [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
   106      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)]
   107     |> Pretty.chunks |> Pretty.writeln;
   108 end;
   109 
   110 structure InductiveData = TheoryDataFun(InductiveArgs);
   111 val print_inductives = InductiveData.print;
   112 
   113 
   114 (* get and put data *)
   115 
   116 fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name);
   117 
   118 fun the_inductive thy name =
   119   (case get_inductive thy name of
   120     None => error ("Unknown (co)inductive set " ^ quote name)
   121   | Some info => info);
   122 
   123 fun put_inductives names info thy =
   124   let
   125     fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
   126     val tab_monos = foldl upd (InductiveData.get thy, names)
   127       handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
   128   in InductiveData.put tab_monos thy end;
   129 
   130 
   131 
   132 (** monotonicity rules **)
   133 
   134 val get_monos = #2 o InductiveData.get;
   135 fun map_monos f = InductiveData.map (Library.apsnd f);
   136 
   137 fun mk_mono thm =
   138   let
   139     fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @
   140       (case concl_of thm of
   141           (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
   142         | _ => [standard (thm' RS (thm' RS eq_to_mono2))]);
   143     val concl = concl_of thm
   144   in
   145     if Logic.is_equals concl then
   146       eq2mono (thm RS meta_eq_to_obj_eq)
   147     else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
   148       eq2mono thm
   149     else [thm]
   150   end;
   151 
   152 
   153 (* attributes *)
   154 
   155 fun mono_add_global (thy, thm) = (map_monos (Drule.add_rules (mk_mono thm)) thy, thm);
   156 fun mono_del_global (thy, thm) = (map_monos (Drule.del_rules (mk_mono thm)) thy, thm);
   157 
   158 val mono_attr =
   159  (Attrib.add_del_args mono_add_global mono_del_global,
   160   Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute);
   161 
   162 
   163 
   164 (** misc utilities **)
   165 
   166 val quiet_mode = ref false;
   167 fun message s = if ! quiet_mode then () else writeln s;
   168 fun clean_message s = if ! quick_and_dirty then () else message s;
   169 
   170 fun coind_prefix true = "co"
   171   | coind_prefix false = "";
   172 
   173 
   174 (*the following code ensures that each recursive set always has the
   175   same type in all introduction rules*)
   176 fun unify_consts sign cs intr_ts =
   177   (let
   178     val {tsig, ...} = Sign.rep_sg sign;
   179     val add_term_consts_2 =
   180       foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
   181     fun varify (t, (i, ts)) =
   182       let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
   183       in (maxidx_of_term t', t'::ts) end;
   184     val (i, cs') = foldr varify (cs, (~1, []));
   185     val (i', intr_ts') = foldr varify (intr_ts, (i, []));
   186     val rec_consts = foldl add_term_consts_2 ([], cs');
   187     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
   188     fun unify (env, (cname, cT)) =
   189       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
   190       in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
   191           (env, (replicate (length consts) cT) ~~ consts)
   192       end;
   193     val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts);
   194     fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T
   195       in if T = T' then T else typ_subst_TVars_2 env T' end;
   196     val subst = fst o Type.freeze_thaw o
   197       (map_term_types (typ_subst_TVars_2 env))
   198 
   199   in (map subst cs', map subst intr_ts')
   200   end) handle Type.TUNIFY =>
   201     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
   202 
   203 
   204 (*make injections used in mutually recursive definitions*)
   205 fun mk_inj cs sumT c x =
   206   let
   207     fun mk_inj' T n i =
   208       if n = 1 then x else
   209       let val n2 = n div 2;
   210           val Type (_, [T1, T2]) = T
   211       in
   212         if i <= n2 then
   213           Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i)
   214         else
   215           Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
   216       end
   217   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
   218   end;
   219 
   220 (*make "vimage" terms for selecting out components of mutually rec.def*)
   221 fun mk_vimage cs sumT t c = if length cs < 2 then t else
   222   let
   223     val cT = HOLogic.dest_setT (fastype_of c);
   224     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
   225   in
   226     Const (vimage_name, vimageT) $
   227       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t
   228   end;
   229 
   230 (** proper splitting **)
   231 
   232 fun prod_factors p (Const ("Pair", _) $ t $ u) =
   233       p :: prod_factors (1::p) t @ prod_factors (2::p) u
   234   | prod_factors p _ = [];
   235 
   236 fun mg_prod_factors ts (fs, t $ u) = if t mem ts then
   237         let val f = prod_factors [] u
   238         in overwrite (fs, (t, f inter if_none (assoc (fs, t)) f)) end
   239       else mg_prod_factors ts (mg_prod_factors ts (fs, t), u)
   240   | mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t)
   241   | mg_prod_factors ts (fs, _) = fs;
   242 
   243 fun prodT_factors p ps (T as Type ("*", [T1, T2])) =
   244       if p mem ps then prodT_factors (1::p) ps T1 @ prodT_factors (2::p) ps T2
   245       else [T]
   246   | prodT_factors _ _ T = [T];
   247 
   248 fun ap_split p ps (Type ("*", [T1, T2])) T3 u =
   249       if p mem ps then HOLogic.split_const (T1, T2, T3) $
   250         Abs ("v", T1, ap_split (2::p) ps T2 T3 (ap_split (1::p) ps T1
   251           (prodT_factors (2::p) ps T2 ---> T3) (incr_boundvars 1 u) $ Bound 0))
   252       else u
   253   | ap_split _ _ _ _ u =  u;
   254 
   255 fun mk_tuple p ps (Type ("*", [T1, T2])) (tms as t::_) =
   256       if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms, 
   257         mk_tuple (2::p) ps T2 (drop (length (prodT_factors (1::p) ps T1), tms)))
   258       else t
   259   | mk_tuple _ _ _ (t::_) = t;
   260 
   261 fun split_rule_var' ((t as Var (v, Type ("fun", [T1, T2])), ps), rl) =
   262       let val T' = prodT_factors [] ps T1 ---> T2
   263           val newt = ap_split [] ps T1 T2 (Var (v, T'))
   264           val cterm = Thm.cterm_of (#sign (rep_thm rl))
   265       in
   266           instantiate ([], [(cterm t, cterm newt)]) rl
   267       end
   268   | split_rule_var' (_, rl) = rl;
   269 
   270 val remove_split = rewrite_rule [split_conv RS eq_reflection];
   271 
   272 fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
   273   (mg_prod_factors vs ([], #prop (rep_thm rl)), rl)));
   274 
   275 fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
   276   (mapfilter (fn (t as Var ((a, _), _)) =>
   277     apsome (pair t) (assoc (vs, a))) (term_vars (#prop (rep_thm rl))), rl)));
   278 
   279 
   280 (** process rules **)
   281 
   282 local
   283 
   284 fun err_in_rule sg name t msg =
   285   error (cat_lines ["Ill-formed introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
   286 
   287 fun err_in_prem sg name t p msg =
   288   error (cat_lines ["Ill-formed premise", Sign.string_of_term sg p,
   289     "in introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
   290 
   291 val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
   292 
   293 val all_not_allowed = 
   294     "Introduction rule must not have a leading \"!!\" quantifier";
   295 
   296 val atomize_cterm = Tactic.rewrite_cterm true inductive_atomize;
   297 
   298 in
   299 
   300 fun check_rule sg cs ((name, rule), att) =
   301   let
   302     val concl = Logic.strip_imp_concl rule;
   303     val prems = Logic.strip_imp_prems rule;
   304     val aprems = prems |> map (Thm.term_of o atomize_cterm o Thm.cterm_of sg);
   305     val arule = Logic.list_implies (aprems, concl);
   306 
   307     fun check_prem (prem, aprem) =
   308       if can HOLogic.dest_Trueprop aprem then ()
   309       else err_in_prem sg name rule prem "Non-atomic premise";
   310   in
   311     (case concl of
   312       Const ("Trueprop", _) $ (Const ("op :", _) $ t $ u) =>
   313         if u mem cs then
   314           if exists (Logic.occs o rpair t) cs then
   315             err_in_rule sg name rule "Recursion term on left of member symbol"
   316           else seq check_prem (prems ~~ aprems)
   317         else err_in_rule sg name rule bad_concl
   318       | Const ("all", _) $ _ => err_in_rule sg name rule all_not_allowed
   319       | _ => err_in_rule sg name rule bad_concl);
   320     ((name, arule), att)
   321   end;
   322 
   323 val rulify =
   324   standard o Tactic.norm_hhf o
   325   hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o
   326   hol_simplify inductive_conj;
   327 
   328 end;
   329 
   330 
   331 
   332 (** properties of (co)inductive sets **)
   333 
   334 (* elimination rules *)
   335 
   336 fun mk_elims cs cTs params intr_ts intr_names =
   337   let
   338     val used = foldr add_term_names (intr_ts, []);
   339     val [aname, pname] = variantlist (["a", "P"], used);
   340     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
   341 
   342     fun dest_intr r =
   343       let val Const ("op :", _) $ t $ u =
   344         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   345       in (u, t, Logic.strip_imp_prems r) end;
   346 
   347     val intrs = map dest_intr intr_ts ~~ intr_names;
   348 
   349     fun mk_elim (c, T) =
   350       let
   351         val a = Free (aname, T);
   352 
   353         fun mk_elim_prem (_, t, ts) =
   354           list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
   355             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
   356         val c_intrs = (filter (equal c o #1 o #1) intrs);
   357       in
   358         (Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
   359           map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs)
   360       end
   361   in
   362     map mk_elim (cs ~~ cTs)
   363   end;
   364 
   365 
   366 (* premises and conclusions of induction rules *)
   367 
   368 fun mk_indrule cs cTs params intr_ts =
   369   let
   370     val used = foldr add_term_names (intr_ts, []);
   371 
   372     (* predicates for induction rule *)
   373 
   374     val preds = map Free (variantlist (if length cs < 2 then ["P"] else
   375       map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
   376         map (fn T => T --> HOLogic.boolT) cTs);
   377 
   378     (* transform an introduction rule into a premise for induction rule *)
   379 
   380     fun mk_ind_prem r =
   381       let
   382         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   383 
   384         val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
   385 
   386         fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
   387               (case pred_of u of
   388                   None => (m $ fst (subst t) $ fst (subst u), None)
   389                 | Some P => (HOLogic.mk_binop inductive_conj_name (s, P $ t), Some (s, P $ t)))
   390           | subst s =
   391               (case pred_of s of
   392                   Some P => (HOLogic.mk_binop "op Int"
   393                     (s, HOLogic.Collect_const (HOLogic.dest_setT
   394                       (fastype_of s)) $ P), None)
   395                 | None => (case s of
   396                      (t $ u) => (fst (subst t) $ fst (subst u), None)
   397                    | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None)
   398                    | _ => (s, None)));
   399 
   400         fun mk_prem (s, prems) = (case subst s of
   401               (_, Some (t, u)) => t :: u :: prems
   402             | (t, _) => t :: prems);
   403 
   404         val Const ("op :", _) $ t $ u =
   405           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   406 
   407       in list_all_free (frees,
   408            Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
   409              (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
   410                HOLogic.mk_Trueprop (the (pred_of u) $ t)))
   411       end;
   412 
   413     val ind_prems = map mk_ind_prem intr_ts;
   414     val factors = 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 = if_none (assoc (factors, P)) [];
   421           val Ts = prodT_factors [] ps T;
   422           val (frees, x') = foldr (fn (T', (fs, s)) =>
   423             ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
   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 (cs ~~ preds, ([], "xa")))))
   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 (flat (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 (((name, raw_atts), raw_props), comment) thy =
   583   let
   584     val ss = Simplifier.simpset_of thy;
   585     val sign = Theory.sign_of thy;
   586     val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
   587     val atts = map (prep_att thy) raw_atts;
   588     val thms = map (smart_mk_cases thy ss) cprops;
   589   in
   590     thy |>
   591     IsarThy.have_theorems_i Drule.lemmaK [(((name, atts), map Thm.no_attributes thms), comment)]
   592   end;
   593 
   594 val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
   595 val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
   596 
   597 
   598 (* mk_cases_meth *)
   599 
   600 fun mk_cases_meth (ctxt, raw_props) =
   601   let
   602     val thy = ProofContext.theory_of ctxt;
   603     val ss = Simplifier.get_local_simpset ctxt;
   604     val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props;
   605   in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
   606 
   607 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
   608 
   609 
   610 (* prove induction rule *)
   611 
   612 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
   613     fp_def rec_sets_defs thy =
   614   let
   615     val _ = clean_message "  Proving the induction rule ...";
   616 
   617     val sign = Theory.sign_of thy;
   618 
   619     val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
   620         None => []
   621       | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
   622 
   623     val (preds, ind_prems, mutual_ind_concl, factors) =
   624       mk_indrule cs cTs params intr_ts;
   625 
   626     (* make predicate for instantiation of abstract induction rule *)
   627 
   628     fun mk_ind_pred _ [P] = P
   629       | mk_ind_pred T Ps =
   630          let val n = (length Ps) div 2;
   631              val Type (_, [T1, T2]) = T
   632          in Const ("Datatype.sum.sum_case",
   633            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
   634              mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
   635          end;
   636 
   637     val ind_pred = mk_ind_pred sumT preds;
   638 
   639     val ind_concl = HOLogic.mk_Trueprop
   640       (HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->"
   641         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0)));
   642 
   643     (* simplification rules for vimage and Collect *)
   644 
   645     val vimage_simps = if length cs < 2 then [] else
   646       map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of sign
   647         (HOLogic.mk_Trueprop (HOLogic.mk_eq
   648           (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   649            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   650              nth_elem (find_index_eq c cs, preds)))))
   651         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
   652 
   653     val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
   654       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   655         [rtac (impI RS allI) 1,
   656          DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
   657          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
   658          fold_goals_tac rec_sets_defs,
   659          (*This CollectE and disjE separates out the introduction rules*)
   660          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
   661          (*Now break down the individual cases.  No disjE here in case
   662            some premise involves disjunction.*)
   663          REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
   664          rewrite_goals_tac sum_case_rewrites,
   665          EVERY (map (fn prem =>
   666            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
   667 
   668     val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
   669       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
   670         [cut_facts_tac prems 1,
   671          REPEAT (EVERY
   672            [REPEAT (resolve_tac [conjI, impI] 1),
   673             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
   674             rewrite_goals_tac sum_case_rewrites,
   675             atac 1])])
   676 
   677   in standard (split_rule factors (induct RS lemma)) end;
   678 
   679 
   680 
   681 (** specification of (co)inductive sets **)
   682 
   683 fun cond_declare_consts declare_consts cs paramTs cnames =
   684   if declare_consts then
   685     Theory.add_consts_i (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   686   else I;
   687 
   688 fun mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
   689       params paramTs cTs cnames =
   690   let
   691     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
   692     val setT = HOLogic.mk_setT sumT;
   693 
   694     val fp_name = if coind then gfp_name else lfp_name;
   695 
   696     val used = foldr add_term_names (intr_ts, []);
   697     val [sname, xname] = variantlist (["S", "x"], used);
   698 
   699     (* transform an introduction rule into a conjunction  *)
   700     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
   701     (* is transformed into                                *)
   702     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
   703 
   704     fun transform_rule r =
   705       let
   706         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   707         val subst = subst_free
   708           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
   709         val Const ("op :", _) $ t $ u =
   710           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   711 
   712       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
   713         (frees, foldr1 HOLogic.mk_conj
   714           (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
   715             (map (subst o HOLogic.dest_Trueprop)
   716               (Logic.strip_imp_prems r))))
   717       end
   718 
   719     (* make a disjunction of all introduction rules *)
   720 
   721     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
   722       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
   723 
   724     (* add definiton of recursive sets to theory *)
   725 
   726     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
   727     val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
   728 
   729     val rec_const = list_comb
   730       (Const (full_rec_name, paramTs ---> setT), params);
   731 
   732     val fp_def_term = Logic.mk_equals (rec_const,
   733       Const (fp_name, (setT --> setT) --> setT) $ fp_fun);
   734 
   735     val def_terms = fp_def_term :: (if length cs < 2 then [] else
   736       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
   737 
   738     val (thy', [fp_def :: rec_sets_defs]) =
   739       thy
   740       |> cond_declare_consts declare_consts cs paramTs cnames
   741       |> (if length cs < 2 then I
   742           else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
   743       |> Theory.add_path rec_name
   744       |> PureThy.add_defss_i false [(("defs", def_terms), [])];
   745 
   746     val mono = prove_mono setT fp_fun monos thy'
   747 
   748   in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
   749 
   750 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   751     intros monos thy params paramTs cTs cnames induct_cases =
   752   let
   753     val _ =
   754       if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
   755         commas_quote cnames) else ();
   756 
   757     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   758 
   759     val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) =
   760       mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
   761         params paramTs cTs cnames;
   762 
   763     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts rec_sets_defs thy1;
   764     val elims = if no_elim then [] else
   765       prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy1;
   766     val raw_induct = if no_ind then Drule.asm_rl else
   767       if coind then standard (rule_by_tactic
   768         (rewrite_tac [mk_meta_eq vimage_Un] THEN
   769           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
   770       else
   771         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
   772           rec_sets_defs thy1;
   773     val induct =
   774       if coind orelse no_ind orelse length cs > 1 then (raw_induct, [RuleCases.consumes 0])
   775       else (raw_induct RSN (2, rev_mp), [RuleCases.consumes 1]);
   776 
   777     val (thy2, intrs') =
   778       thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
   779     val (thy3, ([intrs'', elims'], [induct'])) =
   780       thy2
   781       |> PureThy.add_thmss
   782         [(("intros", intrs'), []),
   783           (("elims", elims), [RuleCases.consumes 1])]
   784       |>>> PureThy.add_thms
   785         [((coind_prefix coind ^ "induct", rulify (#1 induct)),
   786          (RuleCases.case_names induct_cases :: #2 induct))]
   787       |>> Theory.parent_path;
   788   in (thy3,
   789     {defs = fp_def :: rec_sets_defs,
   790      mono = mono,
   791      unfold = unfold,
   792      intrs = intrs'',
   793      elims = elims',
   794      mk_cases = mk_cases elims',
   795      raw_induct = rulify raw_induct,
   796      induct = induct'})
   797   end;
   798 
   799 
   800 (* external interfaces *)
   801 
   802 fun try_term f msg sign t =
   803   (case Library.try f t of
   804     Some x => x
   805   | None => error (msg ^ Sign.string_of_term sign t));
   806 
   807 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy =
   808   let
   809     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
   810     val sign = Theory.sign_of thy;
   811 
   812     (*parameters should agree for all mutually recursive components*)
   813     val (_, params) = strip_comb (hd cs);
   814     val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\
   815       \ component is not a free variable: " sign) params;
   816 
   817     val cTs = map (try_term (HOLogic.dest_setT o fastype_of)
   818       "Recursive component not of type set: " sign) cs;
   819 
   820     val full_cnames = map (try_term (fst o dest_Const o head_of)
   821       "Recursive set not previously declared as constant: " sign) cs;
   822     val cnames = map Sign.base_name full_cnames;
   823 
   824     val save_sign =
   825       thy |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames |> Theory.sign_of;
   826     val intros = map (check_rule save_sign cs) pre_intros;
   827     val induct_cases = map (#1 o #1) intros;
   828 
   829     val (thy1, result as {elims, induct, ...}) =
   830       add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos
   831         thy params paramTs cTs cnames induct_cases;
   832     val thy2 = thy1
   833       |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
   834       |> add_cases_induct no_elim (no_ind orelse coind orelse length cs > 1)
   835           full_cnames elims induct;
   836   in (thy2, result) end;
   837 
   838 fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =
   839   let
   840     val sign = Theory.sign_of thy;
   841     val cs = map (term_of o HOLogic.read_cterm sign) c_strings;
   842 
   843     val intr_names = map (fst o fst) intro_srcs;
   844     fun read_rule s = Thm.read_cterm sign (s, propT)
   845       handle ERROR => error ("The error(s) above occurred for " ^ s);
   846     val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
   847     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
   848     val (cs', intr_ts') = unify_consts sign cs intr_ts;
   849 
   850     val (thy', monos) = thy |> IsarThy.apply_theorems raw_monos;
   851   in
   852     add_inductive_i verbose false "" coind false false cs'
   853       ((intr_names ~~ intr_ts') ~~ intr_atts) monos thy'
   854   end;
   855 
   856 
   857 
   858 (** package setup **)
   859 
   860 (* setup theory *)
   861 
   862 val setup =
   863  [InductiveData.init,
   864   Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
   865     "dynamic case analysis on sets")],
   866   Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
   867 
   868 
   869 (* outer syntax *)
   870 
   871 local structure P = OuterParse and K = OuterSyntax.Keyword in
   872 
   873 fun mk_ind coind ((sets, intrs), monos) =
   874   #1 o add_inductive true coind sets (map P.triple_swap intrs) monos;
   875 
   876 fun ind_decl coind =
   877   (Scan.repeat1 P.term --| P.marg_comment) --
   878   (P.$$$ "intros" |--
   879     P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
   880   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) []
   881   >> (Toplevel.theory o mk_ind coind);
   882 
   883 val inductiveP =
   884   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
   885 
   886 val coinductiveP =
   887   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
   888 
   889 
   890 val ind_cases =
   891   P.opt_thm_name ":" -- Scan.repeat1 P.prop -- P.marg_comment
   892   >> (Toplevel.theory o inductive_cases);
   893 
   894 val inductive_casesP =
   895   OuterSyntax.command "inductive_cases"
   896     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
   897 
   898 val _ = OuterSyntax.add_keywords ["intros", "monos"];
   899 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
   900 
   901 end;
   902 
   903 end;