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