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