src/HOL/Tools/inductive_package.ML
author berghofe
Mon Jan 29 13:26:04 2001 +0100 (2001-01-29 ago)
changeset 10988 e0016a009c17
parent 10910 058775a575db
child 11005 86f662ba3c3f
permissions -rw-r--r--
Splitting of arguments of product types in induction rules is now less
aggressive.
     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     Copyright   1994  University of Cambridge
     7                 1998  TU Muenchen
     8 
     9 (Co)Inductive Definition module for HOL.
    10 
    11 Features:
    12   * least or greatest fixedpoints
    13   * user-specified product and sum constructions
    14   * mutually recursive definitions
    15   * definitions involving arbitrary monotone operators
    16   * automatically proves introduction and elimination rules
    17 
    18 The recursive sets must *already* be declared as constants in the
    19 current theory!
    20 
    21   Introduction rules have the form
    22   [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk
    23   where M is some monotone operator (usually the identity)
    24   P(x) is any side condition on the free variables
    25   ti, t are any terms
    26   Sj, Sk are two of the sets being defined in mutual recursion
    27 
    28 Sums are used only for mutual recursion.  Products are used only to
    29 derive "streamlined" induction rules for relations.
    30 *)
    31 
    32 signature INDUCTIVE_PACKAGE =
    33 sig
    34   val quiet_mode: bool ref
    35   val unify_consts: Sign.sg -> term list -> term list -> term list * term list
    36   val split_rule_vars: term list -> thm -> thm
    37   val get_inductive: theory -> string -> ({names: string list, coind: bool} *
    38     {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    39      intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
    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 * Args.src list) * string list) * Comment.text
    48     -> theory -> theory
    49   val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
    50     -> theory -> theory
    51   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    52     theory attribute list -> ((bstring * term) * theory attribute list) list ->
    53       thm list -> thm list -> theory -> theory *
    54       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    55        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    56   val add_inductive: bool -> bool -> string list -> Args.src list ->
    57     ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
    58       (xstring * Args.src list) list -> theory -> theory *
    59       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    60        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    61   val setup: (theory -> theory) list
    62 end;
    63 
    64 structure InductivePackage: INDUCTIVE_PACKAGE =
    65 struct
    66 
    67 
    68 (** theory context references **)
    69 
    70 val mono_name = "Ord.mono";
    71 val gfp_name = "Gfp.gfp";
    72 val lfp_name = "Lfp.lfp";
    73 val vimage_name = "Inverse_Image.vimage";
    74 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
    75 
    76 val inductive_forall_name = "Inductive.forall";
    77 val inductive_forall_def = thm "forall_def";
    78 val inductive_conj_name = "Inductive.conj";
    79 val inductive_conj_def = thm "conj_def";
    80 val inductive_conj = thms "inductive_conj";
    81 val inductive_atomize = thms "inductive_atomize";
    82 val inductive_rulify1 = thms "inductive_rulify1";
    83 val inductive_rulify2 = thms "inductive_rulify2";
    84 
    85 
    86 
    87 (** theory data **)
    88 
    89 (* data kind 'HOL/inductive' *)
    90 
    91 type inductive_info =
    92   {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
    93     induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
    94 
    95 structure InductiveArgs =
    96 struct
    97   val name = "HOL/inductive";
    98   type T = inductive_info Symtab.table * thm list;
    99 
   100   val empty = (Symtab.empty, []);
   101   val copy = I;
   102   val prep_ext = I;
   103   fun merge ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2),
   104     Library.generic_merge Thm.eq_thm I I 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 atomize_cterm = InductMethod.rewrite_cterm inductive_atomize;
   296 fun full_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
   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 HOLogic.dest_Trueprop concl of
   312       (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       | _ => err_in_rule sg name rule bad_concl);
   319     ((name, arule), att)
   320   end;
   321 
   322 val rulify =
   323   standard o Tactic.norm_hhf o
   324   full_simplify inductive_rulify2 o full_simplify inductive_rulify1 o
   325   full_simplify inductive_conj;
   326 
   327 end;
   328 
   329 
   330 
   331 (** properties of (co)inductive sets **)
   332 
   333 (* elimination rules *)
   334 
   335 fun mk_elims cs cTs params intr_ts intr_names =
   336   let
   337     val used = foldr add_term_names (intr_ts, []);
   338     val [aname, pname] = variantlist (["a", "P"], used);
   339     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
   340 
   341     fun dest_intr r =
   342       let val Const ("op :", _) $ t $ u =
   343         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   344       in (u, t, Logic.strip_imp_prems r) end;
   345 
   346     val intrs = map dest_intr intr_ts ~~ intr_names;
   347 
   348     fun mk_elim (c, T) =
   349       let
   350         val a = Free (aname, T);
   351 
   352         fun mk_elim_prem (_, t, ts) =
   353           list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
   354             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
   355         val c_intrs = (filter (equal c o #1 o #1) intrs);
   356       in
   357         (Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
   358           map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs)
   359       end
   360   in
   361     map mk_elim (cs ~~ cTs)
   362   end;
   363 
   364 
   365 (* premises and conclusions of induction rules *)
   366 
   367 fun mk_indrule cs cTs params intr_ts =
   368   let
   369     val used = foldr add_term_names (intr_ts, []);
   370 
   371     (* predicates for induction rule *)
   372 
   373     val preds = map Free (variantlist (if length cs < 2 then ["P"] else
   374       map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
   375         map (fn T => T --> HOLogic.boolT) cTs);
   376 
   377     (* transform an introduction rule into a premise for induction rule *)
   378 
   379     fun mk_ind_prem r =
   380       let
   381         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   382 
   383         val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
   384 
   385         fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
   386               (case pred_of u of
   387                   None => (m $ fst (subst t) $ fst (subst u), None)
   388                 | Some P => (HOLogic.mk_binop inductive_conj_name (s, P $ t), Some (s, P $ t)))
   389           | subst s =
   390               (case pred_of s of
   391                   Some P => (HOLogic.mk_binop "op Int"
   392                     (s, HOLogic.Collect_const (HOLogic.dest_setT
   393                       (fastype_of s)) $ P), None)
   394                 | None => (case s of
   395                      (t $ u) => (fst (subst t) $ fst (subst u), None)
   396                    | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None)
   397                    | _ => (s, None)));
   398 
   399         fun mk_prem (s, prems) = (case subst s of
   400               (_, Some (t, u)) => t :: u :: prems
   401             | (t, _) => t :: prems);
   402 
   403         val Const ("op :", _) $ t $ u =
   404           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   405 
   406       in list_all_free (frees,
   407            Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
   408              (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
   409                HOLogic.mk_Trueprop (the (pred_of u) $ t)))
   410       end;
   411 
   412     val ind_prems = map mk_ind_prem intr_ts;
   413     val factors = foldl (mg_prod_factors preds) ([], ind_prems);
   414 
   415     (* make conclusions for induction rules *)
   416 
   417     fun mk_ind_concl ((c, P), (ts, x)) =
   418       let val T = HOLogic.dest_setT (fastype_of c);
   419           val ps = if_none (assoc (factors, P)) [];
   420           val Ts = prodT_factors [] ps T;
   421           val (frees, x') = foldr (fn (T', (fs, s)) =>
   422             ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
   423           val tuple = mk_tuple [] ps T frees;
   424       in ((HOLogic.mk_binop "op -->"
   425         (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
   426       end;
   427 
   428     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   429         (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
   430 
   431   in (preds, ind_prems, mutual_ind_concl,
   432     map (apfst (fst o dest_Free)) factors)
   433   end;
   434 
   435 
   436 (* prepare cases and induct rules *)
   437 
   438 (*
   439   transform mutual rule:
   440     HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
   441   into i-th projection:
   442     xi:Ai ==> HH ==> Pi xi
   443 *)
   444 
   445 fun project_rules [name] rule = [(name, rule)]
   446   | project_rules names mutual_rule =
   447       let
   448         val n = length names;
   449         fun proj i =
   450           (if i < n then (fn th => th RS conjunct1) else I)
   451             (Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule)
   452             RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
   453       in names ~~ map proj (1 upto n) end;
   454 
   455 fun add_cases_induct no_elim no_ind names elims induct induct_cases =
   456   let
   457     fun cases_spec (name, elim) thy =
   458       thy
   459       |> Theory.add_path (Sign.base_name name)
   460       |> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
   461       |> Theory.parent_path;
   462     val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
   463 
   464     fun induct_spec (name, th) = (#1 o PureThy.add_thms
   465       [(("", th), [RuleCases.case_names induct_cases, InductAttrib.induct_set_global name])]);
   466     val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct);
   467   in Library.apply (cases_specs @ induct_specs) end;
   468 
   469 
   470 
   471 (** proofs for (co)inductive sets **)
   472 
   473 (* prove monotonicity -- NOT subject to quick_and_dirty! *)
   474 
   475 fun prove_mono setT fp_fun monos thy =
   476  (message "  Proving monotonicity ...";
   477   Goals.prove_goalw_cterm []      (*NO SkipProof.prove_goalw_cterm here!*)
   478     (Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
   479       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
   480     (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)]));
   481 
   482 
   483 (* prove introduction rules *)
   484 
   485 fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
   486   let
   487     val _ = clean_message "  Proving the introduction rules ...";
   488 
   489     val unfold = standard (mono RS (fp_def RS
   490       (if coind then def_gfp_unfold else def_lfp_unfold)));
   491 
   492     fun select_disj 1 1 = []
   493       | select_disj _ 1 = [rtac disjI1]
   494       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
   495 
   496     val intrs = map (fn (i, intr) => SkipProof.prove_goalw_cterm thy rec_sets_defs
   497       (Thm.cterm_of (Theory.sign_of thy) intr) (fn prems =>
   498        [(*insert prems and underlying sets*)
   499        cut_facts_tac prems 1,
   500        stac unfold 1,
   501        REPEAT (resolve_tac [vimageI2, CollectI] 1),
   502        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
   503        EVERY1 (select_disj (length intr_ts) i),
   504        (*Not ares_tac, since refl must be tried before any equality assumptions;
   505          backtracking may occur if the premises have extra variables!*)
   506        DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
   507        (*Now solve the equations like Inl 0 = Inl ?b2*)
   508        rewrite_goals_tac con_defs,
   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     map (fn (t, cases) => SkipProof.prove_goalw_cterm thy rec_sets_defs
   525       (Thm.cterm_of (Theory.sign_of thy) t) (fn prems =>
   526         [cut_facts_tac [hd prems] 1,
   527          dtac (unfold RS subst) 1,
   528          REPEAT (FIRSTGOAL (eresolve_tac rules1)),
   529          REPEAT (FIRSTGOAL (eresolve_tac rules2)),
   530          EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
   531       |> rulify
   532       |> RuleCases.name cases)
   533       (mk_elims cs cTs params intr_ts intr_names)
   534   end;
   535 
   536 
   537 (* derivation of simplified elimination rules *)
   538 
   539 (*Applies freeness of the given constructors, which *must* be unfolded by
   540   the given defs.  Cannot simply use the local con_defs because con_defs=[]
   541   for inference systems. (??) *)
   542 
   543 (*cprop should have the form t:Si where Si is an inductive set*)
   544 
   545 val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
   546 
   547 fun mk_cases_i elims ss cprop =
   548   let
   549     val prem = Thm.assume cprop;
   550     val tac = ALLGOALS (InductMethod.simp_case_tac false ss) THEN prune_params_tac;
   551     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
   552   in
   553     (case get_first (try mk_elim) elims of
   554       Some r => r
   555     | None => error (Pretty.string_of (Pretty.block
   556         [Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop])))
   557   end;
   558 
   559 fun mk_cases elims s =
   560   mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
   561 
   562 fun smart_mk_cases thy ss cprop =
   563   let
   564     val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop
   565       (Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err;
   566     val (_, {elims, ...}) = the_inductive thy c;
   567   in mk_cases_i elims ss cprop end;
   568 
   569 
   570 (* inductive_cases(_i) *)
   571 
   572 fun gen_inductive_cases prep_att prep_const prep_prop
   573     (((name, raw_atts), raw_props), comment) thy =
   574   let
   575     val ss = Simplifier.simpset_of thy;
   576     val sign = Theory.sign_of thy;
   577     val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
   578     val atts = map (prep_att thy) raw_atts;
   579     val thms = map (smart_mk_cases thy ss) cprops;
   580   in thy |> IsarThy.have_theorems_i [(((name, atts), map Thm.no_attributes thms), comment)] end;
   581 
   582 val inductive_cases =
   583   gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
   584 
   585 val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop;
   586 
   587 
   588 (* mk_cases_meth *)
   589 
   590 fun mk_cases_meth (ctxt, raw_props) =
   591   let
   592     val thy = ProofContext.theory_of ctxt;
   593     val ss = Simplifier.get_local_simpset ctxt;
   594     val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props;
   595   in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
   596 
   597 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
   598 
   599 
   600 (* prove induction rule *)
   601 
   602 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
   603     fp_def rec_sets_defs thy =
   604   let
   605     val _ = clean_message "  Proving the induction rule ...";
   606 
   607     val sign = Theory.sign_of thy;
   608 
   609     val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
   610         None => []
   611       | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
   612 
   613     val (preds, ind_prems, mutual_ind_concl, factors) =
   614       mk_indrule cs cTs params intr_ts;
   615 
   616     (* make predicate for instantiation of abstract induction rule *)
   617 
   618     fun mk_ind_pred _ [P] = P
   619       | mk_ind_pred T Ps =
   620          let val n = (length Ps) div 2;
   621              val Type (_, [T1, T2]) = T
   622          in Const ("Datatype.sum.sum_case",
   623            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
   624              mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
   625          end;
   626 
   627     val ind_pred = mk_ind_pred sumT preds;
   628 
   629     val ind_concl = HOLogic.mk_Trueprop
   630       (HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->"
   631         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0)));
   632 
   633     (* simplification rules for vimage and Collect *)
   634 
   635     val vimage_simps = if length cs < 2 then [] else
   636       map (fn c => SkipProof.prove_goalw_cterm thy [] (Thm.cterm_of sign
   637         (HOLogic.mk_Trueprop (HOLogic.mk_eq
   638           (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   639            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   640              nth_elem (find_index_eq c cs, preds)))))
   641         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
   642 
   643     val induct = SkipProof.prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
   644       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   645         [rtac (impI RS allI) 1,
   646          DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
   647          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
   648          fold_goals_tac rec_sets_defs,
   649          (*This CollectE and disjE separates out the introduction rules*)
   650          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
   651          (*Now break down the individual cases.  No disjE here in case
   652            some premise involves disjunction.*)
   653          REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
   654          rewrite_goals_tac sum_case_rewrites,
   655          EVERY (map (fn prem =>
   656            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
   657 
   658     val lemma = SkipProof.prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
   659       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
   660         [cut_facts_tac prems 1,
   661          REPEAT (EVERY
   662            [REPEAT (resolve_tac [conjI, impI] 1),
   663             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
   664             rewrite_goals_tac sum_case_rewrites,
   665             atac 1])])
   666 
   667   in standard (split_rule factors (induct RS lemma)) end;
   668 
   669 
   670 
   671 (** specification of (co)inductive sets **)
   672 
   673 fun cond_declare_consts declare_consts cs paramTs cnames =
   674   if declare_consts then
   675     Theory.add_consts_i (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   676   else I;
   677 
   678 fun mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   679       params paramTs cTs cnames =
   680   let
   681     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
   682     val setT = HOLogic.mk_setT sumT;
   683 
   684     val fp_name = if coind then gfp_name else lfp_name;
   685 
   686     val used = foldr add_term_names (intr_ts, []);
   687     val [sname, xname] = variantlist (["S", "x"], used);
   688 
   689     (* transform an introduction rule into a conjunction  *)
   690     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
   691     (* is transformed into                                *)
   692     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
   693 
   694     fun transform_rule r =
   695       let
   696         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   697         val subst = subst_free
   698           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
   699         val Const ("op :", _) $ t $ u =
   700           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   701 
   702       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
   703         (frees, foldr1 HOLogic.mk_conj
   704           (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
   705             (map (subst o HOLogic.dest_Trueprop)
   706               (Logic.strip_imp_prems r))))
   707       end
   708 
   709     (* make a disjunction of all introduction rules *)
   710 
   711     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
   712       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
   713 
   714     (* add definiton of recursive sets to theory *)
   715 
   716     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
   717     val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
   718 
   719     val rec_const = list_comb
   720       (Const (full_rec_name, paramTs ---> setT), params);
   721 
   722     val fp_def_term = Logic.mk_equals (rec_const,
   723       Const (fp_name, (setT --> setT) --> setT) $ fp_fun);
   724 
   725     val def_terms = fp_def_term :: (if length cs < 2 then [] else
   726       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
   727 
   728     val (thy', [fp_def :: rec_sets_defs]) =
   729       thy
   730       |> cond_declare_consts declare_consts cs paramTs cnames
   731       |> (if length cs < 2 then I
   732           else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
   733       |> Theory.add_path rec_name
   734       |> PureThy.add_defss_i false [(("defs", def_terms), [])];
   735 
   736     val mono = prove_mono setT fp_fun monos thy'
   737 
   738   in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
   739 
   740 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   741     atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
   742   let
   743     val _ =
   744       if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
   745         commas_quote cnames) else ();
   746 
   747     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   748 
   749     val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) =
   750       mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   751         params paramTs cTs cnames;
   752 
   753     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
   754       rec_sets_defs thy1;
   755     val elims = if no_elim then [] else
   756       prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy1;
   757     val raw_induct = if no_ind then Drule.asm_rl else
   758       if coind then standard (rule_by_tactic
   759         (rewrite_tac [mk_meta_eq vimage_Un] THEN
   760           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
   761       else
   762         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
   763           rec_sets_defs thy1;
   764     val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
   765       else standard (raw_induct RSN (2, rev_mp));
   766 
   767     val (thy2, intrs') =
   768       thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
   769     val (thy3, ([intrs'', elims'], [induct'])) =
   770       thy2
   771       |> PureThy.add_thmss [(("intros", intrs'), atts), (("elims", elims), [])]
   772       |>>> PureThy.add_thms
   773         [((coind_prefix coind ^ "induct", rulify induct), [RuleCases.case_names induct_cases])]
   774       |>> Theory.parent_path;
   775   in (thy3,
   776     {defs = fp_def :: rec_sets_defs,
   777      mono = mono,
   778      unfold = unfold,
   779      intrs = intrs'',
   780      elims = elims',
   781      mk_cases = mk_cases elims',
   782      raw_induct = rulify raw_induct,
   783      induct = induct'})
   784   end;
   785 
   786 
   787 (* external interfaces *)
   788 
   789 fun try_term f msg sign t =
   790   (case Library.try f t of
   791     Some x => x
   792   | None => error (msg ^ Sign.string_of_term sign t));
   793 
   794 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
   795     atts pre_intros monos con_defs thy =
   796   let
   797     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
   798     val sign = Theory.sign_of thy;
   799 
   800     (*parameters should agree for all mutually recursive components*)
   801     val (_, params) = strip_comb (hd cs);
   802     val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\
   803       \ component is not a free variable: " sign) params;
   804 
   805     val cTs = map (try_term (HOLogic.dest_setT o fastype_of)
   806       "Recursive component not of type set: " sign) cs;
   807 
   808     val full_cnames = map (try_term (fst o dest_Const o head_of)
   809       "Recursive set not previously declared as constant: " sign) cs;
   810     val cnames = map Sign.base_name full_cnames;
   811 
   812     val save_sign =
   813       thy |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames |> Theory.sign_of;
   814     val intros = map (check_rule save_sign cs) pre_intros;
   815     val induct_cases = map (#1 o #1) intros;
   816 
   817     val (thy1, result as {elims, induct, ...}) =
   818       add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
   819         con_defs thy params paramTs cTs cnames induct_cases;
   820     val thy2 = thy1
   821       |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
   822       |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct induct_cases;
   823   in (thy2, result) end;
   824 
   825 fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
   826   let
   827     val sign = Theory.sign_of thy;
   828     val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
   829 
   830     val atts = map (Attrib.global_attribute thy) srcs;
   831     val intr_names = map (fst o fst) intro_srcs;
   832     fun read_rule s = Thm.read_cterm sign (s, propT)
   833       handle ERROR => error ("The error(s) above occurred for " ^ s);
   834     val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
   835     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
   836     val (cs', intr_ts') = unify_consts sign cs intr_ts;
   837 
   838     val ((thy', con_defs), monos) = thy
   839       |> IsarThy.apply_theorems raw_monos
   840       |> apfst (IsarThy.apply_theorems raw_con_defs);
   841   in
   842     add_inductive_i verbose false "" coind false false cs'
   843       atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
   844   end;
   845 
   846 
   847 
   848 (** package setup **)
   849 
   850 (* setup theory *)
   851 
   852 val setup =
   853  [InductiveData.init,
   854   Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
   855     "dynamic case analysis on sets")],
   856   Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
   857 
   858 
   859 (* outer syntax *)
   860 
   861 local structure P = OuterParse and K = OuterSyntax.Keyword in
   862 
   863 fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
   864   #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
   865 
   866 fun ind_decl coind =
   867   (Scan.repeat1 P.term --| P.marg_comment) --
   868   (P.$$$ "intros" |--
   869     P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
   870   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
   871   Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
   872   >> (Toplevel.theory o mk_ind coind);
   873 
   874 val inductiveP =
   875   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
   876 
   877 val coinductiveP =
   878   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
   879 
   880 
   881 val ind_cases =
   882   P.opt_thm_name ":" -- Scan.repeat1 P.prop -- P.marg_comment
   883   >> (Toplevel.theory o inductive_cases);
   884 
   885 val inductive_casesP =
   886   OuterSyntax.command "inductive_cases"
   887     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
   888 
   889 val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"];
   890 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
   891 
   892 end;
   893 
   894 end;