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