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