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