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