src/HOL/Tools/inductive_package.ML
author wenzelm
Sun Feb 27 15:32:10 2000 +0100 (2000-02-27)
changeset 8307 6600c6e53111
parent 8293 4a0e17cf8f70
child 8312 b470bc28b59d
permissions -rw-r--r--
add_cases_induct: induct_method setup;
removed cases_of, 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 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 (*Delete needless equality assumptions*)
   207 val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
   208      (fn _ => [assume_tac 1]);
   209 
   210 (*For simplifying the elimination rule*)
   211 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
   212 
   213 val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``";
   214 val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
   215 
   216 (* make injections needed in mutually recursive definitions *)
   217 
   218 fun mk_inj cs sumT c x =
   219   let
   220     fun mk_inj' T n i =
   221       if n = 1 then x else
   222       let val n2 = n div 2;
   223           val Type (_, [T1, T2]) = T
   224       in
   225         if i <= n2 then
   226           Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i)
   227         else
   228           Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
   229       end
   230   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
   231   end;
   232 
   233 (* make "vimage" terms for selecting out components of mutually rec.def. *)
   234 
   235 fun mk_vimage cs sumT t c = if length cs < 2 then t else
   236   let
   237     val cT = HOLogic.dest_setT (fastype_of c);
   238     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
   239   in
   240     Const (vimage_name, vimageT) $
   241       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t
   242   end;
   243 
   244 
   245 
   246 (** well-formedness checks **)
   247 
   248 fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^
   249   (Sign.string_of_term sign t) ^ "\n" ^ msg);
   250 
   251 fun err_in_prem sign t p msg = error ("Ill-formed premise\n" ^
   252   (Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^
   253   (Sign.string_of_term sign t) ^ "\n" ^ msg);
   254 
   255 val msg1 = "Conclusion of introduction rule must have form\
   256           \ ' t : S_i '";
   257 val msg2 = "Non-atomic premise";
   258 val msg3 = "Recursion term on left of member symbol";
   259 
   260 fun check_rule sign cs r =
   261   let
   262     fun check_prem prem = if can HOLogic.dest_Trueprop prem then ()
   263       else err_in_prem sign r prem msg2;
   264 
   265   in (case HOLogic.dest_Trueprop (Logic.strip_imp_concl r) of
   266         (Const ("op :", _) $ t $ u) =>
   267           if u mem cs then
   268             if exists (Logic.occs o (rpair t)) cs then
   269               err_in_rule sign r msg3
   270             else
   271               seq check_prem (Logic.strip_imp_prems r)
   272           else err_in_rule sign r msg1
   273       | _ => err_in_rule sign r msg1)
   274   end;
   275 
   276 fun try' f msg sign t = (case (try f t) of
   277       Some x => x
   278     | None => error (msg ^ Sign.string_of_term sign t));
   279 
   280 
   281 
   282 (*** properties of (co)inductive sets ***)
   283 
   284 (** elimination rules **)
   285 
   286 fun mk_elims cs cTs params intr_ts =
   287   let
   288     val used = foldr add_term_names (intr_ts, []);
   289     val [aname, pname] = variantlist (["a", "P"], used);
   290     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
   291 
   292     fun dest_intr r =
   293       let val Const ("op :", _) $ t $ u =
   294         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   295       in (u, t, Logic.strip_imp_prems r) end;
   296 
   297     val intrs = map dest_intr intr_ts;
   298 
   299     fun mk_elim (c, T) =
   300       let
   301         val a = Free (aname, T);
   302 
   303         fun mk_elim_prem (_, t, ts) =
   304           list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
   305             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
   306       in
   307         Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
   308           map mk_elim_prem (filter (equal c o #1) intrs), P)
   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 (*** proofs for (co)inductive sets ***)
   386 
   387 (** prove monotonicity **)
   388 
   389 fun prove_mono setT fp_fun monos thy =
   390   let
   391     val _ = message "  Proving monotonicity ...";
   392 
   393     val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
   394       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
   395         (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)])
   396 
   397   in mono end;
   398 
   399 
   400 
   401 (** prove introduction rules **)
   402 
   403 fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
   404   let
   405     val _ = message "  Proving the introduction rules ...";
   406 
   407     val unfold = standard (mono RS (fp_def RS
   408       (if coind then def_gfp_Tarski else def_lfp_Tarski)));
   409 
   410     fun select_disj 1 1 = []
   411       | select_disj _ 1 = [rtac disjI1]
   412       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
   413 
   414     val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
   415       (cterm_of (Theory.sign_of thy) intr) (fn prems =>
   416        [(*insert prems and underlying sets*)
   417        cut_facts_tac prems 1,
   418        stac unfold 1,
   419        REPEAT (resolve_tac [vimageI2, CollectI] 1),
   420        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
   421        EVERY1 (select_disj (length intr_ts) i),
   422        (*Not ares_tac, since refl must be tried before any equality assumptions;
   423          backtracking may occur if the premises have extra variables!*)
   424        DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
   425        (*Now solve the equations like Inl 0 = Inl ?b2*)
   426        rewrite_goals_tac con_defs,
   427        REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts)
   428 
   429   in (intrs, unfold) end;
   430 
   431 
   432 
   433 (** prove elimination rules **)
   434 
   435 fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =
   436   let
   437     val _ = message "  Proving the elimination rules ...";
   438 
   439     val rules1 = [CollectE, disjE, make_elim vimageD, exE];
   440     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @
   441       map make_elim [Inl_inject, Inr_inject];
   442 
   443     val elims = map (fn t => prove_goalw_cterm rec_sets_defs
   444       (cterm_of (Theory.sign_of thy) t) (fn prems =>
   445         [cut_facts_tac [hd prems] 1,
   446          dtac (unfold RS subst) 1,
   447          REPEAT (FIRSTGOAL (eresolve_tac rules1)),
   448          REPEAT (FIRSTGOAL (eresolve_tac rules2)),
   449          EVERY (map (fn prem =>
   450            DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]))
   451       (mk_elims cs cTs params intr_ts)
   452 
   453   in elims end;
   454 
   455 
   456 (** derivation of simplified elimination rules **)
   457 
   458 (*Applies freeness of the given constructors, which *must* be unfolded by
   459   the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   460   for inference systems.
   461  *)
   462 fun con_elim_tac ss =
   463   let val elim_tac = REPEAT o (eresolve_tac elim_rls)
   464   in ALLGOALS(EVERY'[elim_tac,
   465 		     asm_full_simp_tac ss,
   466 		     elim_tac,
   467 		     REPEAT o bound_hyp_subst_tac])
   468      THEN prune_params_tac
   469   end;
   470 
   471 (*cprop should have the form t:Si where Si is an inductive set*)
   472 fun mk_cases_i elims ss cprop =
   473   let
   474     val prem = Thm.assume cprop;
   475     fun mk_elim rl = standard (rule_by_tactic (con_elim_tac ss) (prem RS rl));
   476   in
   477     (case get_first (try mk_elim) elims of
   478       Some r => r
   479     | None => error (Pretty.string_of (Pretty.block
   480         [Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk,
   481           Display.pretty_cterm cprop])))
   482   end;
   483 
   484 fun mk_cases elims s =
   485   mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
   486 
   487 
   488 (* inductive_cases(_i) *)
   489 
   490 fun gen_inductive_cases prep_att prep_const prep_prop
   491     ((((name, raw_atts), raw_set), raw_props), comment) thy =
   492   let
   493     val sign = Theory.sign_of thy;
   494 
   495     val atts = map (prep_att thy) raw_atts;
   496     val (_, {elims, ...}) = get_inductive thy (prep_const sign raw_set);
   497     val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
   498     val thms = map (mk_cases_i elims (Simplifier.simpset_of thy)) cprops;
   499   in
   500     thy
   501     |> IsarThy.have_theorems_i (((name, atts), map Thm.no_attributes thms), comment)
   502   end;
   503 
   504 val inductive_cases =
   505   gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
   506 
   507 val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop;
   508 
   509 
   510 
   511 (** prove induction rule **)
   512 
   513 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
   514     fp_def rec_sets_defs thy =
   515   let
   516     val _ = message "  Proving the induction rule ...";
   517 
   518     val sign = Theory.sign_of thy;
   519 
   520     val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
   521         None => []
   522       | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
   523 
   524     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   525 
   526     (* make predicate for instantiation of abstract induction rule *)
   527 
   528     fun mk_ind_pred _ [P] = P
   529       | mk_ind_pred T Ps =
   530          let val n = (length Ps) div 2;
   531              val Type (_, [T1, T2]) = T
   532          in Const ("Datatype.sum.sum_case",
   533            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
   534              mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
   535          end;
   536 
   537     val ind_pred = mk_ind_pred sumT preds;
   538 
   539     val ind_concl = HOLogic.mk_Trueprop
   540       (HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->"
   541         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0)));
   542 
   543     (* simplification rules for vimage and Collect *)
   544 
   545     val vimage_simps = if length cs < 2 then [] else
   546       map (fn c => prove_goalw_cterm [] (cterm_of sign
   547         (HOLogic.mk_Trueprop (HOLogic.mk_eq
   548           (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   549            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   550              nth_elem (find_index_eq c cs, preds)))))
   551         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites,
   552           rtac refl 1])) cs;
   553 
   554     val induct = prove_goalw_cterm [] (cterm_of sign
   555       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   556         [rtac (impI RS allI) 1,
   557          DETERM (etac (mono RS (fp_def RS def_induct)) 1),
   558          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
   559          fold_goals_tac rec_sets_defs,
   560          (*This CollectE and disjE separates out the introduction rules*)
   561          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
   562          (*Now break down the individual cases.  No disjE here in case
   563            some premise involves disjunction.*)
   564          REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
   565          rewrite_goals_tac sum_case_rewrites,
   566          EVERY (map (fn prem =>
   567            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
   568 
   569     val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
   570       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
   571         [cut_facts_tac prems 1,
   572          REPEAT (EVERY
   573            [REPEAT (resolve_tac [conjI, impI] 1),
   574             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
   575             rewrite_goals_tac sum_case_rewrites,
   576             atac 1])])
   577 
   578   in standard (split_rule (induct RS lemma))
   579   end;
   580 
   581 
   582 
   583 (*** specification of (co)inductive sets ****)
   584 
   585 (** definitional introduction of (co)inductive sets **)
   586 
   587 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   588     atts intros monos con_defs thy params paramTs cTs cnames =
   589   let
   590     val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
   591       commas_quote cnames) else ();
   592 
   593     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
   594     val setT = HOLogic.mk_setT sumT;
   595 
   596     val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
   597       else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";
   598 
   599     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   600 
   601     val used = foldr add_term_names (intr_ts, []);
   602     val [sname, xname] = variantlist (["S", "x"], used);
   603 
   604     (* transform an introduction rule into a conjunction  *)
   605     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
   606     (* is transformed into                                *)
   607     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
   608 
   609     fun transform_rule r =
   610       let
   611         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   612         val subst = subst_free
   613           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
   614         val Const ("op :", _) $ t $ u =
   615           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   616 
   617       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
   618         (frees, foldr1 HOLogic.mk_conj
   619           (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
   620             (map (subst o HOLogic.dest_Trueprop)
   621               (Logic.strip_imp_prems r))))
   622       end
   623 
   624     (* make a disjunction of all introduction rules *)
   625 
   626     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
   627       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
   628 
   629     (* add definiton of recursive sets to theory *)
   630 
   631     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
   632     val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
   633 
   634     val rec_const = list_comb
   635       (Const (full_rec_name, paramTs ---> setT), params);
   636 
   637     val fp_def_term = Logic.mk_equals (rec_const,
   638       Const (fp_name, (setT --> setT) --> setT) $ fp_fun)
   639 
   640     val def_terms = fp_def_term :: (if length cs < 2 then [] else
   641       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
   642 
   643     val thy' = thy |>
   644       (if declare_consts then
   645         Theory.add_consts_i (map (fn (c, n) =>
   646           (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   647        else I) |>
   648       (if length cs < 2 then I else
   649        Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)]) |>
   650       Theory.add_path rec_name |>
   651       PureThy.add_defss_i [(("defs", def_terms), [])];
   652 
   653     (* get definitions from theory *)
   654 
   655     val fp_def::rec_sets_defs = PureThy.get_thms thy' "defs";
   656 
   657     (* prove and store theorems *)
   658 
   659     val mono = prove_mono setT fp_fun monos thy';
   660     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
   661       rec_sets_defs thy';
   662     val elims = if no_elim then [] else
   663       prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';
   664     val raw_induct = if no_ind then TrueI else
   665       if coind then standard (rule_by_tactic
   666         (rewrite_tac [mk_meta_eq vimage_Un] THEN
   667           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
   668       else
   669         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
   670           rec_sets_defs thy';
   671     val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
   672       else standard (raw_induct RSN (2, rev_mp));
   673 
   674     val thy'' = thy'
   675       |> PureThy.add_thmss [(("intrs", intrs), atts)]
   676       |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
   677       |> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])])
   678       |> (if no_ind then I else PureThy.add_thms
   679         [((coind_prefix coind ^ "induct", induct), [])])
   680       |> Theory.parent_path;
   681     val intrs' = PureThy.get_thms thy'' "intrs";
   682     val elims' = PureThy.get_thms thy'' "elims";
   683     val induct' = PureThy.get_thm thy'' (coind_prefix coind ^ "induct");
   684   in (thy'',
   685     {defs = fp_def::rec_sets_defs,
   686      mono = mono,
   687      unfold = unfold,
   688      intrs = intrs',
   689      elims = elims',
   690      mk_cases = mk_cases elims',
   691      raw_induct = raw_induct,
   692      induct = induct'})
   693   end;
   694 
   695 
   696 
   697 (** axiomatic introduction of (co)inductive sets **)
   698 
   699 fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
   700     atts intros monos con_defs thy params paramTs cTs cnames =
   701   let
   702     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
   703 
   704     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   705     val elim_ts = mk_elims cs cTs params intr_ts;
   706 
   707     val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   708     val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
   709     
   710     val thy' = thy
   711       |> (if declare_consts then
   712             Theory.add_consts_i
   713               (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   714          else I)
   715       |> Theory.add_path rec_name
   716       |> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("elims", elim_ts), [])]
   717       |> (if coind then I else
   718             PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
   719 
   720     val intrs = PureThy.get_thms thy' "intrs";
   721     val elims = PureThy.get_thms thy' "elims";
   722     val raw_induct = if coind then TrueI else PureThy.get_thm thy' "raw_induct";
   723     val induct = if coind orelse length cs > 1 then raw_induct
   724       else standard (raw_induct RSN (2, rev_mp));
   725 
   726     val thy'' =
   727       thy'
   728       |> (if coind then I else PureThy.add_thms [(("induct", induct), [])])
   729       |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
   730       |> Theory.parent_path;
   731     val induct' = if coind then raw_induct else PureThy.get_thm thy'' "induct";
   732   in (thy'',
   733     {defs = [],
   734      mono = TrueI,
   735      unfold = TrueI,
   736      intrs = intrs,
   737      elims = elims,
   738      mk_cases = mk_cases elims,
   739      raw_induct = raw_induct,
   740      induct = induct'})
   741   end;
   742 
   743 
   744 
   745 (** introduction of (co)inductive sets **)
   746 
   747 fun add_cases_induct names elims induct =
   748   PureThy.add_thms
   749     (map (fn name => (("", induct), [InductMethod.induct_set_global name])) names @
   750      map2 (fn (name, elim) => (("", elim), [InductMethod.cases_set_global name])) (names, elims));
   751 
   752 
   753 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
   754     atts intros monos con_defs thy =
   755   let
   756     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
   757     val sign = Theory.sign_of thy;
   758 
   759     (*parameters should agree for all mutually recursive components*)
   760     val (_, params) = strip_comb (hd cs);
   761     val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\
   762       \ component is not a free variable: " sign) params;
   763 
   764     val cTs = map (try' (HOLogic.dest_setT o fastype_of)
   765       "Recursive component not of type set: " sign) cs;
   766 
   767     val full_cnames = map (try' (fst o dest_Const o head_of)
   768       "Recursive set not previously declared as constant: " sign) cs;
   769     val cnames = map Sign.base_name full_cnames;
   770 
   771     val _ = seq (check_rule sign cs o snd o fst) intros;
   772 
   773     val (thy1, result) =
   774       (if ! quick_and_dirty then add_ind_axm else add_ind_def)
   775         verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
   776         con_defs thy params paramTs cTs cnames;
   777     val thy2 = thy1
   778       |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
   779       |> add_cases_induct full_cnames (#elims result) (#induct result);
   780   in (thy2, result) end;
   781 
   782 
   783 
   784 (** external interface **)
   785 
   786 fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
   787   let
   788     val sign = Theory.sign_of thy;
   789     val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
   790 
   791     val atts = map (Attrib.global_attribute thy) srcs;
   792     val intr_names = map (fst o fst) intro_srcs;
   793     val intr_ts = map (term_of o Thm.read_cterm sign o rpair propT o snd o fst) intro_srcs;
   794     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
   795     val (cs', intr_ts') = unify_consts sign cs intr_ts;
   796 
   797     val ((thy', con_defs), monos) = thy
   798       |> IsarThy.apply_theorems raw_monos
   799       |> apfst (IsarThy.apply_theorems raw_con_defs);
   800   in
   801     add_inductive_i verbose false "" coind false false cs'
   802       atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
   803   end;
   804 
   805 
   806 
   807 (** package setup **)
   808 
   809 (* setup theory *)
   810 
   811 val setup = [InductiveData.init,
   812              Attrib.add_attributes [(monoN, mono_attr, "monotonicity rule")]];
   813 
   814 
   815 (* outer syntax *)
   816 
   817 local structure P = OuterParse and K = OuterSyntax.Keyword in
   818 
   819 fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
   820   #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
   821 
   822 fun ind_decl coind =
   823   (Scan.repeat1 P.term --| P.marg_comment) --
   824   (P.$$$ "intrs" |--
   825     P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
   826   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
   827   Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
   828   >> (Toplevel.theory o mk_ind coind);
   829 
   830 val inductiveP =
   831   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
   832 
   833 val coinductiveP =
   834   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
   835 
   836 
   837 val ind_cases =
   838   P.opt_thm_name "=" -- P.xname --| P.$$$ ":" -- Scan.repeat1 P.prop -- P.marg_comment
   839   >> (Toplevel.theory o inductive_cases);
   840 
   841 val inductive_casesP =
   842   OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules"
   843     K.thy_decl ind_cases;
   844 
   845 val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"];
   846 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
   847 
   848 end;
   849 
   850 
   851 end;