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