src/HOL/Tools/inductive_package.ML
author wenzelm
Wed Oct 31 01:21:31 2001 +0100 (2001-10-31)
changeset 11991 da6ee05d9f3d
parent 11880 a625de9ad62a
child 12109 bd6eb9194a5d
permissions -rw-r--r--
use HOL.induct_XXX;
     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 prep_ext = I;
   102   fun merge ((tab1, monos1), (tab2, monos2)) =
   103     (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
   104 
   105   fun print sg (tab, monos) =
   106     [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
   107      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)]
   108     |> Pretty.chunks |> Pretty.writeln;
   109 end;
   110 
   111 structure InductiveData = TheoryDataFun(InductiveArgs);
   112 val print_inductives = InductiveData.print;
   113 
   114 
   115 (* get and put data *)
   116 
   117 fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name);
   118 
   119 fun the_inductive thy name =
   120   (case get_inductive thy name of
   121     None => error ("Unknown (co)inductive set " ^ quote name)
   122   | Some info => info);
   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 = 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 fun message s = if ! quiet_mode then () else writeln s;
   169 fun clean_message s = if ! quick_and_dirty then () else message s;
   170 
   171 fun coind_prefix true = "co"
   172   | coind_prefix false = "";
   173 
   174 
   175 (*the following code ensures that each recursive set always has the
   176   same type in all introduction rules*)
   177 fun unify_consts sign cs intr_ts =
   178   (let
   179     val {tsig, ...} = Sign.rep_sg sign;
   180     val add_term_consts_2 =
   181       foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
   182     fun varify (t, (i, ts)) =
   183       let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
   184       in (maxidx_of_term t', t'::ts) end;
   185     val (i, cs') = foldr varify (cs, (~1, []));
   186     val (i', intr_ts') = foldr varify (intr_ts, (i, []));
   187     val rec_consts = foldl add_term_consts_2 ([], cs');
   188     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
   189     fun unify (env, (cname, cT)) =
   190       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
   191       in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
   192           (env, (replicate (length consts) cT) ~~ consts)
   193       end;
   194     val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts);
   195     fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T
   196       in if T = T' then T else typ_subst_TVars_2 env T' end;
   197     val subst = fst o Type.freeze_thaw o
   198       (map_term_types (typ_subst_TVars_2 env))
   199 
   200   in (map subst cs', map subst intr_ts')
   201   end) handle Type.TUNIFY =>
   202     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
   203 
   204 
   205 (*make injections used in mutually recursive definitions*)
   206 fun mk_inj cs sumT c x =
   207   let
   208     fun mk_inj' T n i =
   209       if n = 1 then x else
   210       let val n2 = n div 2;
   211           val Type (_, [T1, T2]) = T
   212       in
   213         if i <= n2 then
   214           Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i)
   215         else
   216           Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
   217       end
   218   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
   219   end;
   220 
   221 (*make "vimage" terms for selecting out components of mutually rec.def*)
   222 fun mk_vimage cs sumT t c = if length cs < 2 then t else
   223   let
   224     val cT = HOLogic.dest_setT (fastype_of c);
   225     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
   226   in
   227     Const (vimage_name, vimageT) $
   228       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t
   229   end;
   230 
   231 (** proper splitting **)
   232 
   233 fun prod_factors p (Const ("Pair", _) $ t $ u) =
   234       p :: prod_factors (1::p) t @ prod_factors (2::p) u
   235   | prod_factors p _ = [];
   236 
   237 fun mg_prod_factors ts (fs, t $ u) = if t mem ts then
   238         let val f = prod_factors [] u
   239         in overwrite (fs, (t, f inter if_none (assoc (fs, t)) f)) end
   240       else mg_prod_factors ts (mg_prod_factors ts (fs, t), u)
   241   | mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t)
   242   | mg_prod_factors ts (fs, _) = fs;
   243 
   244 fun prodT_factors p ps (T as Type ("*", [T1, T2])) =
   245       if p mem ps then prodT_factors (1::p) ps T1 @ prodT_factors (2::p) ps T2
   246       else [T]
   247   | prodT_factors _ _ T = [T];
   248 
   249 fun ap_split p ps (Type ("*", [T1, T2])) T3 u =
   250       if p mem ps then HOLogic.split_const (T1, T2, T3) $
   251         Abs ("v", T1, ap_split (2::p) ps T2 T3 (ap_split (1::p) ps T1
   252           (prodT_factors (2::p) ps T2 ---> T3) (incr_boundvars 1 u) $ Bound 0))
   253       else u
   254   | ap_split _ _ _ _ u =  u;
   255 
   256 fun mk_tuple p ps (Type ("*", [T1, T2])) (tms as t::_) =
   257       if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms, 
   258         mk_tuple (2::p) ps T2 (drop (length (prodT_factors (1::p) ps T1), tms)))
   259       else t
   260   | mk_tuple _ _ _ (t::_) = t;
   261 
   262 fun split_rule_var' ((t as Var (v, Type ("fun", [T1, T2])), ps), rl) =
   263       let val T' = prodT_factors [] ps T1 ---> T2
   264           val newt = ap_split [] ps T1 T2 (Var (v, T'))
   265           val cterm = Thm.cterm_of (#sign (rep_thm rl))
   266       in
   267           instantiate ([], [(cterm t, cterm newt)]) rl
   268       end
   269   | split_rule_var' (_, rl) = rl;
   270 
   271 val remove_split = rewrite_rule [split_conv RS eq_reflection];
   272 
   273 fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
   274   (mg_prod_factors vs ([], #prop (rep_thm rl)), rl)));
   275 
   276 fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
   277   (mapfilter (fn (t as Var ((a, _), _)) =>
   278     apsome (pair t) (assoc (vs, a))) (term_vars (#prop (rep_thm rl))), rl)));
   279 
   280 
   281 (** process rules **)
   282 
   283 local
   284 
   285 fun err_in_rule sg name t msg =
   286   error (cat_lines ["Ill-formed introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
   287 
   288 fun err_in_prem sg name t p msg =
   289   error (cat_lines ["Ill-formed premise", Sign.string_of_term sg p,
   290     "in introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
   291 
   292 val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
   293 
   294 val all_not_allowed = 
   295     "Introduction rule must not have a leading \"!!\" quantifier";
   296 
   297 val atomize_cterm = Tactic.rewrite_cterm true inductive_atomize;
   298 
   299 in
   300 
   301 fun check_rule sg cs ((name, rule), att) =
   302   let
   303     val concl = Logic.strip_imp_concl rule;
   304     val prems = Logic.strip_imp_prems rule;
   305     val aprems = prems |> map (Thm.term_of o atomize_cterm o Thm.cterm_of sg);
   306     val arule = Logic.list_implies (aprems, concl);
   307 
   308     fun check_prem (prem, aprem) =
   309       if can HOLogic.dest_Trueprop aprem then ()
   310       else err_in_prem sg name rule prem "Non-atomic premise";
   311   in
   312     (case concl of
   313       Const ("Trueprop", _) $ (Const ("op :", _) $ t $ u) =>
   314         if u mem cs then
   315           if exists (Logic.occs o rpair t) cs then
   316             err_in_rule sg name rule "Recursion term on left of member symbol"
   317           else seq check_prem (prems ~~ aprems)
   318         else err_in_rule sg name rule bad_concl
   319       | Const ("all", _) $ _ => err_in_rule sg name rule all_not_allowed
   320       | _ => err_in_rule sg name rule bad_concl);
   321     ((name, arule), att)
   322   end;
   323 
   324 val rulify =
   325   standard o Tactic.norm_hhf o
   326   hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o
   327   hol_simplify inductive_conj;
   328 
   329 end;
   330 
   331 
   332 
   333 (** properties of (co)inductive sets **)
   334 
   335 (* elimination rules *)
   336 
   337 fun mk_elims cs cTs params intr_ts intr_names =
   338   let
   339     val used = foldr add_term_names (intr_ts, []);
   340     val [aname, pname] = variantlist (["a", "P"], used);
   341     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
   342 
   343     fun dest_intr r =
   344       let val Const ("op :", _) $ t $ u =
   345         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   346       in (u, t, Logic.strip_imp_prems r) end;
   347 
   348     val intrs = map dest_intr intr_ts ~~ intr_names;
   349 
   350     fun mk_elim (c, T) =
   351       let
   352         val a = Free (aname, T);
   353 
   354         fun mk_elim_prem (_, t, ts) =
   355           list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
   356             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
   357         val c_intrs = (filter (equal c o #1 o #1) intrs);
   358       in
   359         (Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
   360           map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs)
   361       end
   362   in
   363     map mk_elim (cs ~~ cTs)
   364   end;
   365 
   366 
   367 (* premises and conclusions of induction rules *)
   368 
   369 fun mk_indrule cs cTs params intr_ts =
   370   let
   371     val used = foldr add_term_names (intr_ts, []);
   372 
   373     (* predicates for induction rule *)
   374 
   375     val preds = map Free (variantlist (if length cs < 2 then ["P"] else
   376       map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
   377         map (fn T => T --> HOLogic.boolT) cTs);
   378 
   379     (* transform an introduction rule into a premise for induction rule *)
   380 
   381     fun mk_ind_prem r =
   382       let
   383         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   384 
   385         val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
   386 
   387         fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
   388               (case pred_of u of
   389                   None => (m $ fst (subst t) $ fst (subst u), None)
   390                 | Some P => (HOLogic.mk_binop inductive_conj_name (s, P $ t), Some (s, P $ t)))
   391           | subst s =
   392               (case pred_of s of
   393                   Some P => (HOLogic.mk_binop "op Int"
   394                     (s, HOLogic.Collect_const (HOLogic.dest_setT
   395                       (fastype_of s)) $ P), None)
   396                 | None => (case s of
   397                      (t $ u) => (fst (subst t) $ fst (subst u), None)
   398                    | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None)
   399                    | _ => (s, None)));
   400 
   401         fun mk_prem (s, prems) = (case subst s of
   402               (_, Some (t, u)) => t :: u :: prems
   403             | (t, _) => t :: prems);
   404 
   405         val Const ("op :", _) $ t $ u =
   406           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   407 
   408       in list_all_free (frees,
   409            Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
   410              (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
   411                HOLogic.mk_Trueprop (the (pred_of u) $ t)))
   412       end;
   413 
   414     val ind_prems = map mk_ind_prem intr_ts;
   415     val factors = 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 = if_none (assoc (factors, P)) [];
   422           val Ts = prodT_factors [] ps T;
   423           val (frees, x') = foldr (fn (T', (fs, s)) =>
   424             ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
   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 (cs ~~ preds, ([], "xa")))))
   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_ind 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_ind 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 (Theory.sign_of thy) (HOLogic.mk_Trueprop
   481       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
   482     (fn _ => [rtac monoI 1, REPEAT (ares_tac (flat (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 con_defs 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 (Theory.sign_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        rewrite_goals_tac con_defs,
   511        REPEAT (rtac refl 1)])
   512       |> rulify) (1 upto (length intr_ts) ~~ intr_ts)
   513 
   514   in (intrs, unfold) end;
   515 
   516 
   517 (* prove elimination rules *)
   518 
   519 fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy =
   520   let
   521     val _ = clean_message "  Proving the elimination rules ...";
   522 
   523     val rules1 = [CollectE, disjE, make_elim vimageD, exE];
   524     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
   525   in
   526     mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
   527       quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
   528         (Thm.cterm_of (Theory.sign_of thy) t) (fn prems =>
   529           [cut_facts_tac [hd prems] 1,
   530            dtac (unfold RS subst) 1,
   531            REPEAT (FIRSTGOAL (eresolve_tac rules1)),
   532            REPEAT (FIRSTGOAL (eresolve_tac rules2)),
   533            EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
   534         |> rulify
   535         |> RuleCases.name cases)
   536   end;
   537 
   538 
   539 (* derivation of simplified elimination rules *)
   540 
   541 (*Applies freeness of the given constructors, which *must* be unfolded by
   542   the given defs.  Cannot simply use the local con_defs because con_defs=[]
   543   for inference systems. (??) *)
   544 
   545 local
   546 
   547 (*cprop should have the form t:Si where Si is an inductive set*)
   548 val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
   549 
   550 (*delete needless equality assumptions*)
   551 val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
   552 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
   553 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
   554 
   555 fun simp_case_tac solved ss i =
   556   EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i
   557   THEN_MAYBE (if solved then no_tac else all_tac);
   558 
   559 in
   560 
   561 fun mk_cases_i elims ss cprop =
   562   let
   563     val prem = Thm.assume cprop;
   564     val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac;
   565     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
   566   in
   567     (case get_first (try mk_elim) elims of
   568       Some r => r
   569     | None => error (Pretty.string_of (Pretty.block
   570         [Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop])))
   571   end;
   572 
   573 fun mk_cases elims s =
   574   mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
   575 
   576 fun smart_mk_cases thy ss cprop =
   577   let
   578     val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop
   579       (Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err;
   580     val (_, {elims, ...}) = the_inductive thy c;
   581   in mk_cases_i elims ss cprop end;
   582 
   583 end;
   584 
   585 
   586 (* inductive_cases(_i) *)
   587 
   588 fun gen_inductive_cases prep_att prep_const prep_prop
   589     (((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 =
   602   gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
   603 
   604 val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop;
   605 
   606 
   607 (* mk_cases_meth *)
   608 
   609 fun mk_cases_meth (ctxt, raw_props) =
   610   let
   611     val thy = ProofContext.theory_of ctxt;
   612     val ss = Simplifier.get_local_simpset ctxt;
   613     val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props;
   614   in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
   615 
   616 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
   617 
   618 
   619 (* prove induction rule *)
   620 
   621 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
   622     fp_def rec_sets_defs thy =
   623   let
   624     val _ = clean_message "  Proving the induction rule ...";
   625 
   626     val sign = Theory.sign_of thy;
   627 
   628     val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
   629         None => []
   630       | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
   631 
   632     val (preds, ind_prems, mutual_ind_concl, factors) =
   633       mk_indrule cs cTs params intr_ts;
   634 
   635     (* make predicate for instantiation of abstract induction rule *)
   636 
   637     fun mk_ind_pred _ [P] = P
   638       | mk_ind_pred T Ps =
   639          let val n = (length Ps) div 2;
   640              val Type (_, [T1, T2]) = T
   641          in Const ("Datatype.sum.sum_case",
   642            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
   643              mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
   644          end;
   645 
   646     val ind_pred = mk_ind_pred sumT preds;
   647 
   648     val ind_concl = HOLogic.mk_Trueprop
   649       (HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->"
   650         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0)));
   651 
   652     (* simplification rules for vimage and Collect *)
   653 
   654     val vimage_simps = if length cs < 2 then [] else
   655       map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of sign
   656         (HOLogic.mk_Trueprop (HOLogic.mk_eq
   657           (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   658            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   659              nth_elem (find_index_eq c cs, preds)))))
   660         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
   661 
   662     val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
   663       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   664         [rtac (impI RS allI) 1,
   665          DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
   666          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
   667          fold_goals_tac rec_sets_defs,
   668          (*This CollectE and disjE separates out the introduction rules*)
   669          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
   670          (*Now break down the individual cases.  No disjE here in case
   671            some premise involves disjunction.*)
   672          REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
   673          rewrite_goals_tac sum_case_rewrites,
   674          EVERY (map (fn prem =>
   675            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
   676 
   677     val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
   678       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
   679         [cut_facts_tac prems 1,
   680          REPEAT (EVERY
   681            [REPEAT (resolve_tac [conjI, impI] 1),
   682             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
   683             rewrite_goals_tac sum_case_rewrites,
   684             atac 1])])
   685 
   686   in standard (split_rule factors (induct RS lemma)) end;
   687 
   688 
   689 
   690 (** specification of (co)inductive sets **)
   691 
   692 fun cond_declare_consts declare_consts cs paramTs cnames =
   693   if declare_consts then
   694     Theory.add_consts_i (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   695   else I;
   696 
   697 fun mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   698       params paramTs cTs cnames =
   699   let
   700     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
   701     val setT = HOLogic.mk_setT sumT;
   702 
   703     val fp_name = if coind then gfp_name else lfp_name;
   704 
   705     val used = foldr add_term_names (intr_ts, []);
   706     val [sname, xname] = variantlist (["S", "x"], used);
   707 
   708     (* transform an introduction rule into a conjunction  *)
   709     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
   710     (* is transformed into                                *)
   711     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
   712 
   713     fun transform_rule r =
   714       let
   715         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   716         val subst = subst_free
   717           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
   718         val Const ("op :", _) $ t $ u =
   719           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   720 
   721       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
   722         (frees, foldr1 HOLogic.mk_conj
   723           (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
   724             (map (subst o HOLogic.dest_Trueprop)
   725               (Logic.strip_imp_prems r))))
   726       end
   727 
   728     (* make a disjunction of all introduction rules *)
   729 
   730     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
   731       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
   732 
   733     (* add definiton of recursive sets to theory *)
   734 
   735     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
   736     val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
   737 
   738     val rec_const = list_comb
   739       (Const (full_rec_name, paramTs ---> setT), params);
   740 
   741     val fp_def_term = Logic.mk_equals (rec_const,
   742       Const (fp_name, (setT --> setT) --> setT) $ fp_fun);
   743 
   744     val def_terms = fp_def_term :: (if length cs < 2 then [] else
   745       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
   746 
   747     val (thy', [fp_def :: rec_sets_defs]) =
   748       thy
   749       |> cond_declare_consts declare_consts cs paramTs cnames
   750       |> (if length cs < 2 then I
   751           else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
   752       |> Theory.add_path rec_name
   753       |> PureThy.add_defss_i false [(("defs", def_terms), [])];
   754 
   755     val mono = prove_mono setT fp_fun monos thy'
   756 
   757   in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
   758 
   759 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   760     intros monos con_defs thy params paramTs cTs cnames induct_cases =
   761   let
   762     val _ =
   763       if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
   764         commas_quote cnames) else ();
   765 
   766     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   767 
   768     val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) =
   769       mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   770         params paramTs cTs cnames;
   771 
   772     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
   773       rec_sets_defs thy1;
   774     val elims = if no_elim then [] else
   775       prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy1;
   776     val raw_induct = if no_ind then Drule.asm_rl else
   777       if coind then standard (rule_by_tactic
   778         (rewrite_tac [mk_meta_eq vimage_Un] THEN
   779           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
   780       else
   781         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
   782           rec_sets_defs thy1;
   783     val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
   784       else standard (raw_induct RSN (2, rev_mp));
   785 
   786     val (thy2, intrs') =
   787       thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
   788     val (thy3, ([intrs'', elims'], [induct'])) =
   789       thy2
   790       |> PureThy.add_thmss
   791         [(("intros", intrs'), []),
   792           (("elims", elims), [RuleCases.consumes 1])]
   793       |>>> PureThy.add_thms
   794         [((coind_prefix coind ^ "induct", rulify induct),
   795          [RuleCases.case_names induct_cases,
   796           RuleCases.consumes 1])]
   797       |>> Theory.parent_path;
   798   in (thy3,
   799     {defs = fp_def :: rec_sets_defs,
   800      mono = mono,
   801      unfold = unfold,
   802      intrs = intrs'',
   803      elims = elims',
   804      mk_cases = mk_cases elims',
   805      raw_induct = rulify raw_induct,
   806      induct = induct'})
   807   end;
   808 
   809 
   810 (* external interfaces *)
   811 
   812 fun try_term f msg sign t =
   813   (case Library.try f t of
   814     Some x => x
   815   | None => error (msg ^ Sign.string_of_term sign t));
   816 
   817 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
   818     pre_intros monos con_defs thy =
   819   let
   820     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
   821     val sign = Theory.sign_of thy;
   822 
   823     (*parameters should agree for all mutually recursive components*)
   824     val (_, params) = strip_comb (hd cs);
   825     val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\
   826       \ component is not a free variable: " sign) params;
   827 
   828     val cTs = map (try_term (HOLogic.dest_setT o fastype_of)
   829       "Recursive component not of type set: " sign) cs;
   830 
   831     val full_cnames = map (try_term (fst o dest_Const o head_of)
   832       "Recursive set not previously declared as constant: " sign) cs;
   833     val cnames = map Sign.base_name full_cnames;
   834 
   835     val save_sign =
   836       thy |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames |> Theory.sign_of;
   837     val intros = map (check_rule save_sign cs) pre_intros;
   838     val induct_cases = map (#1 o #1) intros;
   839 
   840     val (thy1, result as {elims, induct, ...}) =
   841       add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos
   842         con_defs thy params paramTs cTs cnames induct_cases;
   843     val thy2 = thy1
   844       |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
   845       |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct;
   846   in (thy2, result) end;
   847 
   848 fun add_inductive verbose coind c_strings intro_srcs raw_monos raw_con_defs thy =
   849   let
   850     val sign = Theory.sign_of thy;
   851     val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
   852 
   853     val intr_names = map (fst o fst) intro_srcs;
   854     fun read_rule s = Thm.read_cterm sign (s, propT)
   855       handle ERROR => error ("The error(s) above occurred for " ^ s);
   856     val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
   857     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
   858     val (cs', intr_ts') = unify_consts sign cs intr_ts;
   859 
   860     val ((thy', con_defs), monos) = thy
   861       |> IsarThy.apply_theorems raw_monos
   862       |> apfst (IsarThy.apply_theorems raw_con_defs);
   863   in
   864     add_inductive_i verbose false "" coind false false cs'
   865       ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
   866   end;
   867 
   868 
   869 
   870 (** package setup **)
   871 
   872 (* setup theory *)
   873 
   874 val setup =
   875  [InductiveData.init,
   876   Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
   877     "dynamic case analysis on sets")],
   878   Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
   879 
   880 
   881 (* outer syntax *)
   882 
   883 local structure P = OuterParse and K = OuterSyntax.Keyword in
   884 
   885 fun mk_ind coind (((sets, intrs), monos), con_defs) =
   886   #1 o add_inductive true coind sets (map P.triple_swap intrs) monos con_defs;
   887 
   888 fun ind_decl coind =
   889   (Scan.repeat1 P.term --| P.marg_comment) --
   890   (P.$$$ "intros" |--
   891     P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
   892   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
   893   Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
   894   >> (Toplevel.theory o mk_ind coind);
   895 
   896 val inductiveP =
   897   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
   898 
   899 val coinductiveP =
   900   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
   901 
   902 
   903 val ind_cases =
   904   P.opt_thm_name ":" -- Scan.repeat1 P.prop -- P.marg_comment
   905   >> (Toplevel.theory o inductive_cases);
   906 
   907 val inductive_casesP =
   908   OuterSyntax.command "inductive_cases"
   909     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
   910 
   911 val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"];
   912 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
   913 
   914 end;
   915 
   916 end;