src/HOL/Tools/inductive_package.ML
author haftmann
Wed Jul 13 10:44:51 2005 +0200 (2005-07-13 ago)
changeset 16785 2eddcce4fd16
parent 16486 1a12cdb6ee6b
child 16786 54b5df610651
permissions -rw-r--r--
(intermediate commit)
     1 (*  Title:      HOL/Tools/inductive_package.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Author:     Stefan Berghofer, TU Muenchen
     5     Author:     Markus Wenzel, TU Muenchen
     6 
     7 (Co)Inductive Definition module for HOL.
     8 
     9 Features:
    10   * least or greatest fixedpoints
    11   * user-specified product and sum constructions
    12   * mutually recursive definitions
    13   * definitions involving arbitrary monotone operators
    14   * automatically proves introduction and elimination rules
    15 
    16 The recursive sets must *already* be declared as constants in the
    17 current theory!
    18 
    19   Introduction rules have the form
    20   [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk
    21   where M is some monotone operator (usually the identity)
    22   P(x) is any side condition on the free variables
    23   ti, t are any terms
    24   Sj, Sk are two of the sets being defined in mutual recursion
    25 
    26 Sums are used only for mutual recursion.  Products are used only to
    27 derive "streamlined" induction rules for relations.
    28 *)
    29 
    30 signature INDUCTIVE_PACKAGE =
    31 sig
    32   val quiet_mode: bool ref
    33   val trace: bool ref
    34   val unify_consts: theory -> term list -> term list -> term list * term list
    35   val split_rule_vars: term list -> thm -> thm
    36   val get_inductive: theory -> string -> ({names: string list, coind: bool} *
    37     {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    38      intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
    39   val the_mk_cases: theory -> string -> string -> thm
    40   val print_inductives: theory -> unit
    41   val mono_add_global: theory attribute
    42   val mono_del_global: theory attribute
    43   val get_monos: theory -> thm list
    44   val inductive_forall_name: string
    45   val inductive_forall_def: thm
    46   val rulify: thm -> thm
    47   val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
    48   val inductive_cases_i: ((bstring * theory attribute list) * term list) list -> theory -> theory
    49   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    50     ((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
    51       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    52        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    53   val add_inductive: bool -> bool -> string list ->
    54     ((bstring * string) * Attrib.src list) list -> (thmref * Attrib.src list) list ->
    55     theory -> theory *
    56       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    57        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    58   val setup: (theory -> theory) list
    59 end;
    60 
    61 structure InductivePackage: INDUCTIVE_PACKAGE =
    62 struct
    63 
    64 
    65 (** theory context references **)
    66 
    67 val mono_name = "Orderings.mono";
    68 val gfp_name = "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 InductiveData = TheoryDataFun
    93 (struct
    94   val name = "HOL/inductive";
    95   type T = inductive_info Symtab.table * thm list;
    96 
    97   val empty = (Symtab.empty, []);
    98   val copy = I;
    99   val extend = I;
   100   fun merge _ ((tab1, monos1), (tab2, monos2)) =
   101     (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
   102 
   103   fun print thy (tab, monos) =
   104     [Pretty.strs ("(co)inductives:" ::
   105       map #1 (NameSpace.extern_table (Sign.const_space thy, tab))),
   106      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg thy) monos)]
   107     |> Pretty.chunks |> Pretty.writeln;
   108 end);
   109 
   110 val print_inductives = InductiveData.print;
   111 
   112 
   113 (* get and put data *)
   114 
   115 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 thy cs intr_ts =
   179   (let
   180     val tsig = Sign.tsig_of thy;
   181     fun add_term_consts_2 (x, y) =
   182       fold_aterms (fn (Const c) => curry (op ins) c | _ => I) y x;
   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.theory_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 thy name t msg =
   284   error (cat_lines ["Ill-formed introduction rule " ^ quote name,
   285     Sign.string_of_term thy t, msg]);
   286 
   287 fun err_in_prem thy name t p msg =
   288   error (cat_lines ["Ill-formed premise", Sign.string_of_term thy p,
   289     "in introduction rule " ^ quote name, Sign.string_of_term thy 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 fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize [];
   297 
   298 in
   299 
   300 fun check_rule thy 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 = map (atomize_term thy) prems;
   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 thy 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 thy name rule "Recursion term on left of member symbol"
   316           else List.app check_prem (prems ~~ aprems)
   317         else err_in_rule thy name rule bad_concl
   318       | Const ("all", _) $ _ => err_in_rule thy name rule all_not_allowed
   319       | _ => err_in_rule thy name rule bad_concl);
   320     ((name, arule), att)
   321   end;
   322 
   323 val rulify =
   324   standard 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 = (List.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 (valOf (pred_of u) $ t)))
   411       end;
   412 
   413     val ind_prems = map mk_ind_prem intr_ts;
   414 
   415     val factors = Library.foldl (mg_prod_factors preds) ([], ind_prems);
   416 
   417     (* make conclusions for induction rules *)
   418 
   419     fun mk_ind_concl ((c, P), (ts, x)) =
   420       let val T = HOLogic.dest_setT (fastype_of c);
   421           val ps = getOpt (assoc (factors, P), []);
   422           val Ts = prodT_factors [] ps T;
   423           val (frees, x') = foldr (fn (T', (fs, s)) =>
   424             ((Free (s, T'))::fs, Symbol.bump_string s)) ([], x) Ts;
   425           val tuple = mk_tuple [] ps T frees;
   426       in ((HOLogic.mk_binop "op -->"
   427         (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
   428       end;
   429 
   430     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   431         (fst (foldr mk_ind_concl ([], "xa") (cs ~~ preds))))
   432 
   433   in (preds, ind_prems, mutual_ind_concl,
   434     map (apfst (fst o dest_Free)) factors)
   435   end;
   436 
   437 
   438 (* prepare cases and induct rules *)
   439 
   440 (*
   441   transform mutual rule:
   442     HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
   443   into i-th projection:
   444     xi:Ai ==> HH ==> Pi xi
   445 *)
   446 
   447 fun project_rules [name] rule = [(name, rule)]
   448   | project_rules names mutual_rule =
   449       let
   450         val n = length names;
   451         fun proj i =
   452           (if i < n then (fn th => th RS conjunct1) else I)
   453             (Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule)
   454             RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
   455       in names ~~ map proj (1 upto n) end;
   456 
   457 fun add_cases_induct no_elim no_induct names elims induct =
   458   let
   459     fun cases_spec (name, elim) thy =
   460       thy
   461       |> Theory.add_path (Sign.base_name name)
   462       |> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
   463       |> Theory.parent_path;
   464     val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
   465 
   466     fun induct_spec (name, th) = #1 o PureThy.add_thms
   467       [(("", RuleCases.save induct th), [InductAttrib.induct_set_global name])];
   468     val induct_specs = if no_induct then [] else map induct_spec (project_rules names induct);
   469   in Library.apply (cases_specs @ induct_specs) end;
   470 
   471 
   472 
   473 (** proofs for (co)inductive sets **)
   474 
   475 (* prove monotonicity -- NOT subject to quick_and_dirty! *)
   476 
   477 fun prove_mono setT fp_fun monos thy =
   478  (message "  Proving monotonicity ...";
   479   Goals.prove_goalw_cterm []      (*NO quick_and_dirty_prove_goalw_cterm here!*)
   480     (Thm.cterm_of thy (HOLogic.mk_Trueprop
   481       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
   482     (fn _ => [rtac monoI 1, REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)]));
   483 
   484 
   485 (* prove introduction rules *)
   486 
   487 fun prove_intrs coind mono fp_def intr_ts rec_sets_defs thy =
   488   let
   489     val _ = clean_message "  Proving the introduction rules ...";
   490 
   491     val unfold = standard' (mono RS (fp_def RS
   492       (if coind then def_gfp_unfold else def_lfp_unfold)));
   493 
   494     fun select_disj 1 1 = []
   495       | select_disj _ 1 = [rtac disjI1]
   496       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
   497 
   498     val intrs = map (fn (i, intr) => quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
   499       (Thm.cterm_of thy intr) (fn prems =>
   500        [(*insert prems and underlying sets*)
   501        cut_facts_tac prems 1,
   502        stac unfold 1,
   503        REPEAT (resolve_tac [vimageI2, CollectI] 1),
   504        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
   505        EVERY1 (select_disj (length intr_ts) i),
   506        (*Not ares_tac, since refl must be tried before any equality assumptions;
   507          backtracking may occur if the premises have extra variables!*)
   508        DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
   509        (*Now solve the equations like Inl 0 = Inl ?b2*)
   510        REPEAT (rtac refl 1)])
   511       |> rulify) (1 upto (length intr_ts) ~~ intr_ts)
   512 
   513   in (intrs, unfold) end;
   514 
   515 
   516 (* prove elimination rules *)
   517 
   518 fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy =
   519   let
   520     val _ = clean_message "  Proving the elimination rules ...";
   521 
   522     val rules1 = [CollectE, disjE, make_elim vimageD, exE];
   523     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
   524   in
   525     mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
   526       quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
   527         (Thm.cterm_of thy t) (fn prems =>
   528           [cut_facts_tac [hd prems] 1,
   529            dtac (unfold RS subst) 1,
   530            REPEAT (FIRSTGOAL (eresolve_tac rules1)),
   531            REPEAT (FIRSTGOAL (eresolve_tac rules2)),
   532            EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
   533         |> rulify
   534         |> RuleCases.name cases)
   535   end;
   536 
   537 
   538 (* derivation of simplified elimination rules *)
   539 
   540 local
   541 
   542 (*cprop should have the form t:Si where Si is an inductive set*)
   543 val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
   544 
   545 (*delete needless equality assumptions*)
   546 val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
   547 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
   548 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
   549 
   550 fun simp_case_tac solved ss i =
   551   EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i
   552   THEN_MAYBE (if solved then no_tac else all_tac);
   553 
   554 in
   555 
   556 fun mk_cases_i elims ss cprop =
   557   let
   558     val prem = Thm.assume cprop;
   559     val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac;
   560     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
   561   in
   562     (case get_first (try mk_elim) elims of
   563       SOME r => r
   564     | NONE => error (Pretty.string_of (Pretty.block
   565         [Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop])))
   566   end;
   567 
   568 fun mk_cases elims s =
   569   mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.theory_of_thm (hd elims)) (s, propT));
   570 
   571 fun smart_mk_cases thy ss cprop =
   572   let
   573     val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop
   574       (Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err;
   575     val (_, {elims, ...}) = the_inductive thy c;
   576   in mk_cases_i elims ss cprop end;
   577 
   578 end;
   579 
   580 
   581 (* inductive_cases(_i) *)
   582 
   583 fun gen_inductive_cases prep_att prep_prop args thy =
   584   let
   585     val cert_prop = Thm.cterm_of thy o prep_prop (ProofContext.init thy);
   586     val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop;
   587 
   588     val facts = args |> map (fn ((a, atts), props) =>
   589      ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
   590   in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
   591 
   592 val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
   593 val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
   594 
   595 
   596 (* mk_cases_meth *)
   597 
   598 fun mk_cases_meth (ctxt, raw_props) =
   599   let
   600     val thy = ProofContext.theory_of ctxt;
   601     val ss = local_simpset_of ctxt;
   602     val cprops = map (Thm.cterm_of thy o ProofContext.read_prop ctxt) raw_props;
   603   in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
   604 
   605 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
   606 
   607 
   608 (* prove induction rule *)
   609 
   610 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
   611     fp_def rec_sets_defs thy =
   612   let
   613     val _ = clean_message "  Proving the induction rule ...";
   614 
   615     val sum_case_rewrites =
   616       (if Context.theory_name thy = "Datatype" then
   617         PureThy.get_thms thy (Name "sum.cases")
   618       else
   619         (case ThyInfo.lookup_theory "Datatype" of
   620           NONE => []
   621         | SOME thy' => PureThy.get_thms thy' (Name "sum.cases")))
   622       |> map mk_meta_eq;
   623 
   624     val (preds, ind_prems, mutual_ind_concl, factors) =
   625       mk_indrule cs cTs params intr_ts;
   626 
   627     val dummy = if !trace then
   628 		(writeln "ind_prems = ";
   629 		 List.app (writeln o Sign.string_of_term thy) ind_prems)
   630 	    else ();
   631 
   632     (* make predicate for instantiation of abstract induction rule *)
   633 
   634     fun mk_ind_pred _ [P] = P
   635       | mk_ind_pred T Ps =
   636          let val n = (length Ps) div 2;
   637              val Type (_, [T1, T2]) = T
   638          in Const ("Datatype.sum.sum_case",
   639            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
   640              mk_ind_pred T1 (Library.take (n, Ps)) $ mk_ind_pred T2 (Library.drop (n, Ps))
   641          end;
   642 
   643     val ind_pred = mk_ind_pred sumT preds;
   644 
   645     val ind_concl = HOLogic.mk_Trueprop
   646       (HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->"
   647         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0)));
   648 
   649     (* simplification rules for vimage and Collect *)
   650 
   651     val vimage_simps = if length cs < 2 then [] else
   652       map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of thy
   653         (HOLogic.mk_Trueprop (HOLogic.mk_eq
   654           (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   655            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   656              List.nth (preds, find_index_eq c cs)))))
   657         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
   658 
   659     val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
   660 
   661     val dummy = if !trace then
   662 		(writeln "raw_fp_induct = "; print_thm raw_fp_induct)
   663 	    else ();
   664 
   665     val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of thy
   666       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   667         [rtac (impI RS allI) 1,
   668          DETERM (etac raw_fp_induct 1),
   669          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
   670          fold_goals_tac rec_sets_defs,
   671          (*This CollectE and disjE separates out the introduction rules*)
   672          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
   673          (*Now break down the individual cases.  No disjE here in case
   674            some premise involves disjunction.*)
   675          REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
   676          ALLGOALS (simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
   677          EVERY (map (fn prem =>
   678    	             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
   679 
   680     val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of thy
   681       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
   682         [cut_facts_tac prems 1,
   683          REPEAT (EVERY
   684            [REPEAT (resolve_tac [conjI, impI] 1),
   685             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
   686             rewrite_goals_tac sum_case_rewrites,
   687             atac 1])])
   688 
   689   in standard (split_rule factors (induct RS lemma)) end;
   690 
   691 
   692 
   693 (** specification of (co)inductive sets **)
   694 
   695 fun cond_declare_consts declare_consts cs paramTs cnames =
   696   if declare_consts then
   697     Theory.add_consts_i (map (fn (c, n) => (Sign.base_name n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   698   else I;
   699 
   700 fun mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
   701       params paramTs cTs cnames =
   702   let
   703     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
   704     val setT = HOLogic.mk_setT sumT;
   705 
   706     val fp_name = if coind then gfp_name else lfp_name;
   707 
   708     val used = foldr add_term_names [] intr_ts;
   709     val [sname, xname] = variantlist (["S", "x"], used);
   710 
   711     (* transform an introduction rule into a conjunction  *)
   712     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
   713     (* is transformed into                                *)
   714     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
   715 
   716     fun transform_rule r =
   717       let
   718         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   719         val subst = subst_free
   720           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
   721         val Const ("op :", _) $ t $ u =
   722           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   723 
   724       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
   725         (foldr1 HOLogic.mk_conj
   726           (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
   727             (map (subst o HOLogic.dest_Trueprop)
   728               (Logic.strip_imp_prems r)))) frees
   729       end
   730 
   731     (* make a disjunction of all introduction rules *)
   732 
   733     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
   734       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
   735 
   736     (* add definiton of recursive sets to theory *)
   737 
   738     val rec_name = if alt_name = "" then
   739       space_implode "_" (map Sign.base_name cnames) else alt_name;
   740     val full_rec_name = if length cs < 2 then hd cnames
   741       else Sign.full_name thy rec_name;
   742 
   743     val rec_const = list_comb
   744       (Const (full_rec_name, paramTs ---> setT), params);
   745 
   746     val fp_def_term = Logic.mk_equals (rec_const,
   747       Const (fp_name, (setT --> setT) --> setT) $ fp_fun);
   748 
   749     val def_terms = fp_def_term :: (if length cs < 2 then [] else
   750       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
   751 
   752     val (thy', [fp_def :: rec_sets_defs]) =
   753       thy
   754       |> cond_declare_consts declare_consts cs paramTs cnames
   755       |> (if length cs < 2 then I
   756           else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
   757       |> Theory.add_path rec_name
   758       |> PureThy.add_defss_i false [(("defs", def_terms), [])];
   759 
   760     val mono = prove_mono setT fp_fun monos thy'
   761 
   762   in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
   763 
   764 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   765     intros monos thy params paramTs cTs cnames induct_cases =
   766   let
   767     val _ =
   768       if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
   769         commas_quote (map Sign.base_name cnames)) else ();
   770 
   771     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   772 
   773     val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) =
   774       mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
   775         params paramTs cTs cnames;
   776 
   777     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts rec_sets_defs thy1;
   778     val elims = if no_elim then [] else
   779       prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy1;
   780     val raw_induct = if no_ind then Drule.asm_rl else
   781       if coind then standard (rule_by_tactic
   782         (rewrite_tac [mk_meta_eq vimage_Un] THEN
   783           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
   784       else
   785         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
   786           rec_sets_defs thy1;
   787     val induct =
   788       if coind orelse no_ind orelse length cs > 1 then (raw_induct, [RuleCases.consumes 0])
   789       else (raw_induct RSN (2, rev_mp), [RuleCases.consumes 1]);
   790 
   791     val (thy2, intrs') =
   792       thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
   793     val (thy3, ([intrs'', elims'], [induct'])) =
   794       thy2
   795       |> PureThy.add_thmss
   796         [(("intros", intrs'), []),
   797           (("elims", elims), [RuleCases.consumes 1])]
   798       |>>> PureThy.add_thms
   799         [((coind_prefix coind ^ "induct", rulify (#1 induct)),
   800          (RuleCases.case_names induct_cases :: #2 induct))]
   801       |>> Theory.parent_path;
   802   in (thy3,
   803     {defs = fp_def :: rec_sets_defs,
   804      mono = mono,
   805      unfold = unfold,
   806      intrs = intrs',
   807      elims = elims',
   808      mk_cases = mk_cases elims',
   809      raw_induct = rulify raw_induct,
   810      induct = induct'})
   811   end;
   812 
   813 
   814 (* external interfaces *)
   815 
   816 fun try_term f msg thy t =
   817   (case Library.try f t of
   818     SOME x => x
   819   | NONE => error (msg ^ Sign.string_of_term thy t));
   820 
   821 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy =
   822   let
   823     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
   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: " thy) params;
   829 
   830     val cTs = map (try_term (HOLogic.dest_setT o fastype_of)
   831       "Recursive component not of type set: " thy) cs;
   832 
   833     val cnames = map (try_term (fst o dest_Const o head_of)
   834       "Recursive set not previously declared as constant: " thy) cs;
   835 
   836     val save_thy = thy
   837       |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames;
   838     val intros = map (check_rule save_thy 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 cs = map (term_of o HOLogic.read_cterm thy) c_strings;
   853 
   854     val intr_names = map (fst o fst) intro_srcs;
   855     fun read_rule s = Thm.read_cterm thy (s, propT)
   856       handle ERROR => error ("The error(s) above occurred for " ^ s);
   857     val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
   858     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
   859     val (cs', intr_ts') = unify_consts thy cs intr_ts;
   860 
   861     val (thy', monos) = thy |> IsarThy.apply_theorems raw_monos;
   862   in
   863     add_inductive_i verbose false "" coind false false cs'
   864       ((intr_names ~~ intr_ts') ~~ intr_atts) monos 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) =
   885   #1 o add_inductive true coind sets (map P.triple_swap intrs) monos;
   886 
   887 fun ind_decl coind =
   888   Scan.repeat1 P.term --
   889   (P.$$$ "intros" |--
   890     P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) --
   891   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) []
   892   >> (Toplevel.theory o mk_ind coind);
   893 
   894 val inductiveP =
   895   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
   896 
   897 val coinductiveP =
   898   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
   899 
   900 
   901 val ind_cases =
   902   P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
   903   >> (Toplevel.theory o inductive_cases);
   904 
   905 val inductive_casesP =
   906   OuterSyntax.command "inductive_cases"
   907     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
   908 
   909 val _ = OuterSyntax.add_keywords ["intros", "monos"];
   910 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
   911 
   912 end;
   913 
   914 end;
   915