src/HOL/Tools/inductive_package.ML
author wenzelm
Mon Sep 04 21:19:07 2000 +0200 (2000-09-04)
changeset 9831 9b883c416aef
parent 9804 ee0c337327cf
child 9893 93d2fde0306c
permissions -rw-r--r--
tuned "mono" att setup;
     1 (*  Title:      HOL/Tools/inductive_package.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4                 Stefan Berghofer,   TU Muenchen
     5     Copyright   1994  University of Cambridge
     6                 1998  TU Muenchen
     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 get_inductive: theory -> string -> ({names: string list, coind: bool} *
    36     {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    37      intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
    38   val print_inductives: theory -> unit
    39   val mono_add_global: theory attribute
    40   val mono_del_global: theory attribute
    41   val get_monos: theory -> thm list
    42   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    43     theory attribute list -> ((bstring * term) * theory attribute list) list ->
    44       thm list -> thm list -> theory -> theory *
    45       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    46        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    47   val add_inductive: bool -> bool -> string list -> Args.src list ->
    48     ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
    49       (xstring * Args.src list) list -> theory -> theory *
    50       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    51        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    52   val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
    53     -> theory -> theory
    54   val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
    55     -> theory -> theory
    56   val setup: (theory -> theory) list
    57 end;
    58 
    59 structure InductivePackage: INDUCTIVE_PACKAGE =
    60 struct
    61 
    62 
    63 (*** theory data ***)
    64 
    65 (* data kind 'HOL/inductive' *)
    66 
    67 type inductive_info =
    68   {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
    69     induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
    70 
    71 structure InductiveArgs =
    72 struct
    73   val name = "HOL/inductive";
    74   type T = inductive_info Symtab.table * thm list;
    75 
    76   val empty = (Symtab.empty, []);
    77   val copy = I;
    78   val prep_ext = I;
    79   fun merge ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2),
    80     Library.generic_merge Thm.eq_thm I I monos1 monos2);
    81 
    82   fun print sg (tab, monos) =
    83     [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
    84      Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)]
    85     |> Pretty.chunks |> Pretty.writeln;
    86 end;
    87 
    88 structure InductiveData = TheoryDataFun(InductiveArgs);
    89 val print_inductives = InductiveData.print;
    90 
    91 
    92 (* get and put data *)
    93 
    94 fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name);
    95 
    96 fun the_inductive thy name =
    97   (case get_inductive thy name of
    98     None => error ("Unknown (co)inductive set " ^ quote name)
    99   | Some info => info);
   100 
   101 fun put_inductives names info thy =
   102   let
   103     fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
   104     val tab_monos = foldl upd (InductiveData.get thy, names)
   105       handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
   106   in InductiveData.put tab_monos thy end;
   107 
   108 
   109 
   110 (** monotonicity rules **)
   111 
   112 val get_monos = #2 o InductiveData.get;
   113 fun map_monos f = InductiveData.map (Library.apsnd f);
   114 
   115 fun mk_mono thm =
   116   let
   117     fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @
   118       (case concl_of thm of
   119           (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
   120         | _ => [standard (thm' RS (thm' RS eq_to_mono2))]);
   121     val concl = concl_of thm
   122   in
   123     if Logic.is_equals concl then
   124       eq2mono (thm RS meta_eq_to_obj_eq)
   125     else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
   126       eq2mono thm
   127     else [thm]
   128   end;
   129 
   130 
   131 (* attributes *)
   132 
   133 fun mono_add_global (thy, thm) = (map_monos (Drule.add_rules (mk_mono thm)) thy, thm);
   134 fun mono_del_global (thy, thm) = (map_monos (Drule.del_rules (mk_mono thm)) thy, thm);
   135 
   136 val mono_attr =
   137  (Attrib.add_del_args mono_add_global mono_del_global,
   138   Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute);
   139 
   140 
   141 
   142 (** utilities **)
   143 
   144 (* messages *)
   145 
   146 val quiet_mode = ref false;
   147 fun message s = if !quiet_mode then () else writeln s;
   148 
   149 fun coind_prefix true = "co"
   150   | coind_prefix false = "";
   151 
   152 
   153 (* the following code ensures that each recursive set *)
   154 (* always has the same type in all introduction rules *)
   155 
   156 fun unify_consts sign cs intr_ts =
   157   (let
   158     val {tsig, ...} = Sign.rep_sg sign;
   159     val add_term_consts_2 =
   160       foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
   161     fun varify (t, (i, ts)) =
   162       let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
   163       in (maxidx_of_term t', t'::ts) end;
   164     val (i, cs') = foldr varify (cs, (~1, []));
   165     val (i', intr_ts') = foldr varify (intr_ts, (i, []));
   166     val rec_consts = foldl add_term_consts_2 ([], cs');
   167     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
   168     fun unify (env, (cname, cT)) =
   169       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
   170       in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
   171           (env, (replicate (length consts) cT) ~~ consts)
   172       end;
   173     val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts);
   174     fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T
   175       in if T = T' then T else typ_subst_TVars_2 env T' end;
   176     val subst = fst o Type.freeze_thaw o
   177       (map_term_types (typ_subst_TVars_2 env))
   178 
   179   in (map subst cs', map subst intr_ts')
   180   end) handle Type.TUNIFY =>
   181     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
   182 
   183 
   184 (* misc *)
   185 
   186 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD);
   187 
   188 val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``";
   189 val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
   190 
   191 (* make injections needed in mutually recursive definitions *)
   192 
   193 fun mk_inj cs sumT c x =
   194   let
   195     fun mk_inj' T n i =
   196       if n = 1 then x else
   197       let val n2 = n div 2;
   198           val Type (_, [T1, T2]) = T
   199       in
   200         if i <= n2 then
   201           Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i)
   202         else
   203           Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
   204       end
   205   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
   206   end;
   207 
   208 (* make "vimage" terms for selecting out components of mutually rec.def. *)
   209 
   210 fun mk_vimage cs sumT t c = if length cs < 2 then t else
   211   let
   212     val cT = HOLogic.dest_setT (fastype_of c);
   213     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
   214   in
   215     Const (vimage_name, vimageT) $
   216       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t
   217   end;
   218 
   219 
   220 
   221 (** well-formedness checks **)
   222 
   223 fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^
   224   (Sign.string_of_term sign t) ^ "\n" ^ msg);
   225 
   226 fun err_in_prem sign t p msg = error ("Ill-formed premise\n" ^
   227   (Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^
   228   (Sign.string_of_term sign t) ^ "\n" ^ msg);
   229 
   230 val msg1 = "Conclusion of introduction rule must have form\
   231           \ ' t : S_i '";
   232 val msg2 = "Non-atomic premise";
   233 val msg3 = "Recursion term on left of member symbol";
   234 
   235 fun check_rule sign cs r =
   236   let
   237     fun check_prem prem = if can HOLogic.dest_Trueprop prem then ()
   238       else err_in_prem sign r prem msg2;
   239 
   240   in (case HOLogic.dest_Trueprop (Logic.strip_imp_concl r) of
   241         (Const ("op :", _) $ t $ u) =>
   242           if u mem cs then
   243             if exists (Logic.occs o (rpair t)) cs then
   244               err_in_rule sign r msg3
   245             else
   246               seq check_prem (Logic.strip_imp_prems r)
   247           else err_in_rule sign r msg1
   248       | _ => err_in_rule sign r msg1)
   249   end;
   250 
   251 fun try' f msg sign t = (case (try f t) of
   252       Some x => x
   253     | None => error (msg ^ Sign.string_of_term sign t));
   254 
   255 
   256 
   257 (*** properties of (co)inductive sets ***)
   258 
   259 (** elimination rules **)
   260 
   261 fun mk_elims cs cTs params intr_ts intr_names =
   262   let
   263     val used = foldr add_term_names (intr_ts, []);
   264     val [aname, pname] = variantlist (["a", "P"], used);
   265     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
   266 
   267     fun dest_intr r =
   268       let val Const ("op :", _) $ t $ u =
   269         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   270       in (u, t, Logic.strip_imp_prems r) end;
   271 
   272     val intrs = map dest_intr intr_ts ~~ intr_names;
   273 
   274     fun mk_elim (c, T) =
   275       let
   276         val a = Free (aname, T);
   277 
   278         fun mk_elim_prem (_, t, ts) =
   279           list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
   280             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
   281         val c_intrs = (filter (equal c o #1 o #1) intrs);
   282       in
   283         (Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
   284           map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs)
   285       end
   286   in
   287     map mk_elim (cs ~~ cTs)
   288   end;
   289 
   290 
   291 
   292 (** premises and conclusions of induction rules **)
   293 
   294 fun mk_indrule cs cTs params intr_ts =
   295   let
   296     val used = foldr add_term_names (intr_ts, []);
   297 
   298     (* predicates for induction rule *)
   299 
   300     val preds = map Free (variantlist (if length cs < 2 then ["P"] else
   301       map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
   302         map (fn T => T --> HOLogic.boolT) cTs);
   303 
   304     (* transform an introduction rule into a premise for induction rule *)
   305 
   306     fun mk_ind_prem r =
   307       let
   308         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   309 
   310         val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
   311 
   312         fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
   313               (case pred_of u of
   314                   None => (m $ fst (subst t) $ fst (subst u), None)
   315                 | Some P => (HOLogic.conj $ s $ (P $ t), Some (s, P $ t)))
   316           | subst s =
   317               (case pred_of s of
   318                   Some P => (HOLogic.mk_binop "op Int"
   319                     (s, HOLogic.Collect_const (HOLogic.dest_setT
   320                       (fastype_of s)) $ P), None)
   321                 | None => (case s of
   322                      (t $ u) => (fst (subst t) $ fst (subst u), None)
   323                    | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None)
   324                    | _ => (s, None)));
   325 
   326         fun mk_prem (s, prems) = (case subst s of
   327               (_, Some (t, u)) => t :: u :: prems
   328             | (t, _) => t :: prems);
   329 
   330         val Const ("op :", _) $ t $ u =
   331           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   332 
   333       in list_all_free (frees,
   334            Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
   335              (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
   336                HOLogic.mk_Trueprop (the (pred_of u) $ t)))
   337       end;
   338 
   339     val ind_prems = map mk_ind_prem intr_ts;
   340 
   341     (* make conclusions for induction rules *)
   342 
   343     fun mk_ind_concl ((c, P), (ts, x)) =
   344       let val T = HOLogic.dest_setT (fastype_of c);
   345           val Ts = HOLogic.prodT_factors T;
   346           val (frees, x') = foldr (fn (T', (fs, s)) =>
   347             ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
   348           val tuple = HOLogic.mk_tuple T frees;
   349       in ((HOLogic.mk_binop "op -->"
   350         (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
   351       end;
   352 
   353     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   354         (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
   355 
   356   in (preds, ind_prems, mutual_ind_concl)
   357   end;
   358 
   359 
   360 
   361 (** prepare cases and induct rules **)
   362 
   363 (*
   364   transform mutual rule:
   365     HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
   366   into i-th projection:
   367     xi:Ai ==> HH ==> Pi xi
   368 *)
   369 
   370 fun project_rules [name] rule = [(name, rule)]
   371   | project_rules names mutual_rule =
   372       let
   373         val n = length names;
   374         fun proj i =
   375           (if i < n then (fn th => th RS conjunct1) else I)
   376             (Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule)
   377             RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
   378       in names ~~ map proj (1 upto n) end;
   379 
   380 fun add_cases_induct no_elim no_ind names elims induct induct_cases =
   381   let
   382     fun cases_spec (name, elim) thy =
   383       thy
   384       |> Theory.add_path (Sign.base_name name)
   385       |> (#1 o PureThy.add_thms [(("cases", elim), [InductMethod.cases_set_global name])])
   386       |> Theory.parent_path;
   387     val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
   388 
   389     fun induct_spec (name, th) = (#1 o PureThy.add_thms
   390       [(("", th), [RuleCases.case_names induct_cases, InductMethod.induct_set_global name])]);
   391     val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct);
   392   in Library.apply (cases_specs @ induct_specs) end;
   393 
   394 
   395 
   396 (*** proofs for (co)inductive sets ***)
   397 
   398 (** prove monotonicity **)
   399 
   400 fun prove_mono setT fp_fun monos thy =
   401   let
   402     val _ = message "  Proving monotonicity ...";
   403 
   404     val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
   405       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
   406         (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)])
   407 
   408   in mono end;
   409 
   410 
   411 
   412 (** prove introduction rules **)
   413 
   414 fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
   415   let
   416     val _ = message "  Proving the introduction rules ...";
   417 
   418     val unfold = standard (mono RS (fp_def RS
   419       (if coind then def_gfp_Tarski else def_lfp_Tarski)));
   420 
   421     fun select_disj 1 1 = []
   422       | select_disj _ 1 = [rtac disjI1]
   423       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
   424 
   425     val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
   426       (cterm_of (Theory.sign_of thy) intr) (fn prems =>
   427        [(*insert prems and underlying sets*)
   428        cut_facts_tac prems 1,
   429        stac unfold 1,
   430        REPEAT (resolve_tac [vimageI2, CollectI] 1),
   431        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
   432        EVERY1 (select_disj (length intr_ts) i),
   433        (*Not ares_tac, since refl must be tried before any equality assumptions;
   434          backtracking may occur if the premises have extra variables!*)
   435        DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
   436        (*Now solve the equations like Inl 0 = Inl ?b2*)
   437        rewrite_goals_tac con_defs,
   438        REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts)
   439 
   440   in (intrs, unfold) end;
   441 
   442 
   443 
   444 (** prove elimination rules **)
   445 
   446 fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy =
   447   let
   448     val _ = message "  Proving the elimination rules ...";
   449 
   450     val rules1 = [CollectE, disjE, make_elim vimageD, exE];
   451     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @
   452       map make_elim [Inl_inject, Inr_inject];
   453   in
   454     map (fn (t, cases) => prove_goalw_cterm rec_sets_defs
   455       (cterm_of (Theory.sign_of thy) t) (fn prems =>
   456         [cut_facts_tac [hd prems] 1,
   457          dtac (unfold RS subst) 1,
   458          REPEAT (FIRSTGOAL (eresolve_tac rules1)),
   459          REPEAT (FIRSTGOAL (eresolve_tac rules2)),
   460          EVERY (map (fn prem =>
   461            DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
   462       |> RuleCases.name cases)
   463       (mk_elims cs cTs params intr_ts intr_names)
   464   end;
   465 
   466 
   467 (** derivation of simplified elimination rules **)
   468 
   469 (*Applies freeness of the given constructors, which *must* be unfolded by
   470   the given defs.  Cannot simply use the local con_defs because con_defs=[]
   471   for inference systems.
   472  *)
   473 
   474 (*cprop should have the form t:Si where Si is an inductive set*)
   475 
   476 val mk_cases_err = "mk_cases: proposition not of form 't : S_i'";
   477 
   478 fun mk_cases_i elims ss cprop =
   479   let
   480     val prem = Thm.assume cprop;
   481     val tac = ALLGOALS (InductMethod.simp_case_tac false ss) THEN prune_params_tac;
   482     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
   483   in
   484     (case get_first (try mk_elim) elims of
   485       Some r => r
   486     | None => error (Pretty.string_of (Pretty.block
   487         [Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop])))
   488   end;
   489 
   490 fun mk_cases elims s =
   491   mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
   492 
   493 fun smart_mk_cases thy ss cprop =
   494   let
   495     val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop
   496       (Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err;
   497     val (_, {elims, ...}) = the_inductive thy c;
   498   in mk_cases_i elims ss cprop end;
   499 
   500 
   501 (* inductive_cases(_i) *)
   502 
   503 fun gen_inductive_cases prep_att prep_const prep_prop
   504     (((name, raw_atts), raw_props), comment) thy =
   505   let
   506     val ss = Simplifier.simpset_of thy;
   507     val sign = Theory.sign_of thy;
   508     val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
   509     val atts = map (prep_att thy) raw_atts;
   510     val thms = map (smart_mk_cases thy ss) cprops;
   511   in thy |> IsarThy.have_theorems_i [(((name, atts), map Thm.no_attributes thms), comment)] end;
   512 
   513 val inductive_cases =
   514   gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
   515 
   516 val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop;
   517 
   518 
   519 (* mk_cases_meth *)
   520 
   521 fun mk_cases_meth (ctxt, raw_props) =
   522   let
   523     val thy = ProofContext.theory_of ctxt;
   524     val ss = Simplifier.get_local_simpset ctxt;
   525     val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props;
   526   in Method.erule (map (smart_mk_cases thy ss) cprops) end;
   527 
   528 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
   529 
   530 
   531 
   532 (** prove induction rule **)
   533 
   534 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
   535     fp_def rec_sets_defs thy =
   536   let
   537     val _ = message "  Proving the induction rule ...";
   538 
   539     val sign = Theory.sign_of thy;
   540 
   541     val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
   542         None => []
   543       | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
   544 
   545     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   546 
   547     (* make predicate for instantiation of abstract induction rule *)
   548 
   549     fun mk_ind_pred _ [P] = P
   550       | mk_ind_pred T Ps =
   551          let val n = (length Ps) div 2;
   552              val Type (_, [T1, T2]) = T
   553          in Const ("Datatype.sum.sum_case",
   554            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
   555              mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
   556          end;
   557 
   558     val ind_pred = mk_ind_pred sumT preds;
   559 
   560     val ind_concl = HOLogic.mk_Trueprop
   561       (HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->"
   562         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0)));
   563 
   564     (* simplification rules for vimage and Collect *)
   565 
   566     val vimage_simps = if length cs < 2 then [] else
   567       map (fn c => prove_goalw_cterm [] (cterm_of sign
   568         (HOLogic.mk_Trueprop (HOLogic.mk_eq
   569           (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   570            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   571              nth_elem (find_index_eq c cs, preds)))))
   572         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites,
   573           rtac refl 1])) cs;
   574 
   575     val induct = prove_goalw_cterm [] (cterm_of sign
   576       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   577         [rtac (impI RS allI) 1,
   578          DETERM (etac (mono RS (fp_def RS def_induct)) 1),
   579          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
   580          fold_goals_tac rec_sets_defs,
   581          (*This CollectE and disjE separates out the introduction rules*)
   582          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
   583          (*Now break down the individual cases.  No disjE here in case
   584            some premise involves disjunction.*)
   585          REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
   586          rewrite_goals_tac sum_case_rewrites,
   587          EVERY (map (fn prem =>
   588            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
   589 
   590     val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
   591       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
   592         [cut_facts_tac prems 1,
   593          REPEAT (EVERY
   594            [REPEAT (resolve_tac [conjI, impI] 1),
   595             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
   596             rewrite_goals_tac sum_case_rewrites,
   597             atac 1])])
   598 
   599   in standard (split_rule (induct RS lemma))
   600   end;
   601 
   602 
   603 
   604 (*** specification of (co)inductive sets ****)
   605 
   606 (** definitional introduction of (co)inductive sets **)
   607 
   608 fun mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   609       params paramTs cTs cnames =
   610   let
   611     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
   612     val setT = HOLogic.mk_setT sumT;
   613 
   614     val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
   615       else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";
   616 
   617     val used = foldr add_term_names (intr_ts, []);
   618     val [sname, xname] = variantlist (["S", "x"], used);
   619 
   620     (* transform an introduction rule into a conjunction  *)
   621     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
   622     (* is transformed into                                *)
   623     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
   624 
   625     fun transform_rule r =
   626       let
   627         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   628         val subst = subst_free
   629           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
   630         val Const ("op :", _) $ t $ u =
   631           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   632 
   633       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
   634         (frees, foldr1 HOLogic.mk_conj
   635           (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
   636             (map (subst o HOLogic.dest_Trueprop)
   637               (Logic.strip_imp_prems r))))
   638       end
   639 
   640     (* make a disjunction of all introduction rules *)
   641 
   642     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
   643       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
   644 
   645     (* add definiton of recursive sets to theory *)
   646 
   647     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
   648     val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
   649 
   650     val rec_const = list_comb
   651       (Const (full_rec_name, paramTs ---> setT), params);
   652 
   653     val fp_def_term = Logic.mk_equals (rec_const,
   654       Const (fp_name, (setT --> setT) --> setT) $ fp_fun)
   655 
   656     val def_terms = fp_def_term :: (if length cs < 2 then [] else
   657       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
   658 
   659     val (thy', [fp_def :: rec_sets_defs]) =
   660       thy
   661       |> (if declare_consts then
   662           Theory.add_consts_i (map (fn (c, n) =>
   663             (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   664           else I)
   665       |> (if length cs < 2 then I
   666           else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
   667       |> Theory.add_path rec_name
   668       |> PureThy.add_defss_i false [(("defs", def_terms), [])];
   669 
   670     val mono = prove_mono setT fp_fun monos thy'
   671 
   672   in
   673     (thy', mono, fp_def, rec_sets_defs, rec_const, sumT)
   674   end;
   675 
   676 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   677     atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
   678   let
   679     val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
   680       commas_quote cnames) else ();
   681 
   682     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   683 
   684     val (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) =
   685       mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   686         params paramTs cTs cnames;
   687 
   688     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
   689       rec_sets_defs thy';
   690     val elims = if no_elim then [] else
   691       prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy';
   692     val raw_induct = if no_ind then Drule.asm_rl else
   693       if coind then standard (rule_by_tactic
   694         (rewrite_tac [mk_meta_eq vimage_Un] THEN
   695           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
   696       else
   697         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
   698           rec_sets_defs thy';
   699     val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
   700       else standard (raw_induct RSN (2, rev_mp));
   701 
   702     val (thy'', [intrs']) =
   703       thy'
   704       |> PureThy.add_thmss [(("intros", intrs), atts)]
   705       |>> (#1 o PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts))
   706       |>> (if no_elim then I else #1 o PureThy.add_thmss [(("elims", elims), [])])
   707       |>> (if no_ind then I else #1 o PureThy.add_thms
   708         [((coind_prefix coind ^ "induct", induct), [RuleCases.case_names induct_cases])])
   709       |>> Theory.parent_path;
   710     val elims' = if no_elim then elims else PureThy.get_thms thy'' "elims";  (* FIXME improve *)
   711     val induct' = if no_ind then induct else PureThy.get_thm thy'' (coind_prefix coind ^ "induct");  (* FIXME improve *)
   712   in (thy'',
   713     {defs = fp_def::rec_sets_defs,
   714      mono = mono,
   715      unfold = unfold,
   716      intrs = intrs',
   717      elims = elims',
   718      mk_cases = mk_cases elims',
   719      raw_induct = raw_induct,
   720      induct = induct'})
   721   end;
   722 
   723 
   724 
   725 (** axiomatic introduction of (co)inductive sets **)
   726 
   727 fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
   728     atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
   729   let
   730     val _ = message (coind_prefix coind ^ "inductive set(s) " ^ commas_quote cnames);
   731 
   732     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   733     val (thy', _, fp_def, rec_sets_defs, _, _) =
   734       mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   735         params paramTs cTs cnames;
   736     val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names);
   737     val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   738     val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
   739 
   740     val (thy'', [intrs, raw_elims]) =
   741       thy'
   742       |> PureThy.add_axiomss_i [(("intros", intr_ts), atts), (("raw_elims", elim_ts), [])]
   743       |>> (if coind then I else
   744             #1 o PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
   745 
   746     val elims = map2 (fn (th, cases) => RuleCases.name cases th) (raw_elims, elim_cases);
   747     val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy'' "raw_induct";
   748     val induct = if coind orelse length cs > 1 then raw_induct
   749       else standard (raw_induct RSN (2, rev_mp));
   750 
   751     val (thy''', ([elims'], intrs')) =
   752       thy''
   753       |> PureThy.add_thmss [(("elims", elims), [])]
   754       |>> (if coind then I
   755           else #1 o PureThy.add_thms [(("induct", induct), [RuleCases.case_names induct_cases])])
   756       |>>> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
   757       |>> Theory.parent_path;
   758     val induct' = if coind then raw_induct else PureThy.get_thm thy''' "induct";
   759   in (thy''',
   760     {defs = fp_def :: rec_sets_defs,
   761      mono = Drule.asm_rl,
   762      unfold = Drule.asm_rl,
   763      intrs = intrs',
   764      elims = elims',
   765      mk_cases = mk_cases elims',
   766      raw_induct = raw_induct,
   767      induct = induct'})
   768   end;
   769 
   770 
   771 
   772 (** introduction of (co)inductive sets **)
   773 
   774 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
   775     atts intros monos con_defs thy =
   776   let
   777     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
   778     val sign = Theory.sign_of thy;
   779 
   780     (*parameters should agree for all mutually recursive components*)
   781     val (_, params) = strip_comb (hd cs);
   782     val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\
   783       \ component is not a free variable: " sign) params;
   784 
   785     val cTs = map (try' (HOLogic.dest_setT o fastype_of)
   786       "Recursive component not of type set: " sign) cs;
   787 
   788     val full_cnames = map (try' (fst o dest_Const o head_of)
   789       "Recursive set not previously declared as constant: " sign) cs;
   790     val cnames = map Sign.base_name full_cnames;
   791 
   792     val _ = seq (check_rule sign cs o snd o fst) intros;
   793     val induct_cases = map (#1 o #1) intros;
   794 
   795     val (thy1, result as {elims, induct, ...}) =
   796       (if ! quick_and_dirty then add_ind_axm else add_ind_def)
   797         verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
   798         con_defs thy params paramTs cTs cnames induct_cases;
   799     val thy2 = thy1
   800       |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
   801       |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct induct_cases;
   802   in (thy2, result) end;
   803 
   804 
   805 
   806 (** external interface **)
   807 
   808 fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
   809   let
   810     val sign = Theory.sign_of thy;
   811     val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
   812 
   813     val atts = map (Attrib.global_attribute thy) srcs;
   814     val intr_names = map (fst o fst) intro_srcs;
   815     fun read_rule s = Thm.read_cterm sign (s, propT)
   816       handle ERROR => error ("The error(s) above occurred for " ^ s);
   817     val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
   818     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
   819     val (cs', intr_ts') = unify_consts sign cs intr_ts;
   820 
   821     val ((thy', con_defs), monos) = thy
   822       |> IsarThy.apply_theorems raw_monos
   823       |> apfst (IsarThy.apply_theorems raw_con_defs);
   824   in
   825     add_inductive_i verbose false "" coind false false cs'
   826       atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
   827   end;
   828 
   829 
   830 
   831 (** package setup **)
   832 
   833 (* setup theory *)
   834 
   835 val setup =
   836  [InductiveData.init,
   837   Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
   838     "dynamic case analysis on sets")],
   839   Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]];
   840 
   841 
   842 (* outer syntax *)
   843 
   844 local structure P = OuterParse and K = OuterSyntax.Keyword in
   845 
   846 fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
   847   #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
   848 
   849 fun ind_decl coind =
   850   (Scan.repeat1 P.term --| P.marg_comment) --
   851   (P.$$$ "intros" |--
   852     P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
   853   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
   854   Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
   855   >> (Toplevel.theory o mk_ind coind);
   856 
   857 val inductiveP =
   858   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
   859 
   860 val coinductiveP =
   861   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
   862 
   863 
   864 val ind_cases =
   865   P.opt_thm_name ":" -- Scan.repeat1 P.prop -- P.marg_comment
   866   >> (Toplevel.theory o inductive_cases);
   867 
   868 val inductive_casesP =
   869   OuterSyntax.command "inductive_cases"
   870     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
   871 
   872 val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"];
   873 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
   874 
   875 end;
   876 
   877 
   878 end;