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