src/HOL/Tools/inductive_package.ML
author wenzelm
Sat Jan 06 21:26:27 2001 +0100 (2001-01-06 ago)
changeset 10804 306aee77eadd
parent 10743 8ea821d1e3a4
child 10910 058775a575db
permissions -rw-r--r--
Tactic.norm_hhf;
     1 (*  Title:      HOL/Tools/inductive_package.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Author:     Stefan Berghofer, TU Muenchen
     5     Author:     Markus Wenzel, TU Muenchen
     6     Copyright   1994  University of Cambridge
     7                 1998  TU Muenchen
     8 
     9 (Co)Inductive Definition module for HOL.
    10 
    11 Features:
    12   * least or greatest fixedpoints
    13   * user-specified product and sum constructions
    14   * mutually recursive definitions
    15   * definitions involving arbitrary monotone operators
    16   * automatically proves introduction and elimination rules
    17 
    18 The recursive sets must *already* be declared as constants in the
    19 current theory!
    20 
    21   Introduction rules have the form
    22   [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk
    23   where M is some monotone operator (usually the identity)
    24   P(x) is any side condition on the free variables
    25   ti, t are any terms
    26   Sj, Sk are two of the sets being defined in mutual recursion
    27 
    28 Sums are used only for mutual recursion.  Products are used only to
    29 derive "streamlined" induction rules for relations.
    30 *)
    31 
    32 signature INDUCTIVE_PACKAGE =
    33 sig
    34   val quiet_mode: bool ref
    35   val unify_consts: Sign.sg -> term list -> term list -> term list * term list
    36   val get_inductive: theory -> string -> ({names: string list, coind: bool} *
    37     {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    38      intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
    39   val print_inductives: theory -> unit
    40   val mono_add_global: theory attribute
    41   val mono_del_global: theory attribute
    42   val get_monos: theory -> thm list
    43   val inductive_cases: ((bstring * Args.src list) * string list) * Comment.text
    44     -> theory -> theory
    45   val inductive_cases_i: ((bstring * theory attribute list) * term list) * Comment.text
    46     -> theory -> theory
    47   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    48     theory attribute list -> ((bstring * term) * theory attribute list) list ->
    49       thm list -> thm 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 add_inductive: bool -> bool -> string list -> Args.src list ->
    53     ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
    54       (xstring * Args.src list) list -> theory -> theory *
    55       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    56        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    57   val setup: (theory -> theory) list
    58 end;
    59 
    60 structure InductivePackage: INDUCTIVE_PACKAGE =
    61 struct
    62 
    63 
    64 (** theory context references **)
    65 
    66 val mono_name = "Ord.mono";
    67 val gfp_name = "Gfp.gfp";
    68 val lfp_name = "Lfp.lfp";
    69 val vimage_name = "Inverse_Image.vimage";
    70 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
    71 
    72 val inductive_conj_name = "Inductive.conj";
    73 val inductive_conj_def = thm "conj_def";
    74 val inductive_conj = thms "inductive_conj";
    75 val inductive_atomize = thms "inductive_atomize";
    76 val inductive_rulify1 = thms "inductive_rulify1";
    77 val inductive_rulify2 = thms "inductive_rulify2";
    78 
    79 
    80 
    81 (** theory data **)
    82 
    83 (* data kind 'HOL/inductive' *)
    84 
    85 type inductive_info =
    86   {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
    87     induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
    88 
    89 structure InductiveArgs =
    90 struct
    91   val name = "HOL/inductive";
    92   type T = inductive_info Symtab.table * thm list;
    93 
    94   val empty = (Symtab.empty, []);
    95   val copy = I;
    96   val prep_ext = I;
    97   fun merge ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2),
    98     Library.generic_merge Thm.eq_thm I I monos1 monos2);
    99 
   100   fun print sg (tab, monos) =
   101     [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
   102      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)]
   103     |> Pretty.chunks |> Pretty.writeln;
   104 end;
   105 
   106 structure InductiveData = TheoryDataFun(InductiveArgs);
   107 val print_inductives = InductiveData.print;
   108 
   109 
   110 (* get and put data *)
   111 
   112 fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name);
   113 
   114 fun the_inductive thy name =
   115   (case get_inductive thy name of
   116     None => error ("Unknown (co)inductive set " ^ quote name)
   117   | Some info => info);
   118 
   119 fun put_inductives names info thy =
   120   let
   121     fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
   122     val tab_monos = foldl upd (InductiveData.get thy, names)
   123       handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
   124   in InductiveData.put tab_monos thy end;
   125 
   126 
   127 
   128 (** monotonicity rules **)
   129 
   130 val get_monos = #2 o InductiveData.get;
   131 fun map_monos f = InductiveData.map (Library.apsnd f);
   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 
   149 (* attributes *)
   150 
   151 fun mono_add_global (thy, thm) = (map_monos (Drule.add_rules (mk_mono thm)) thy, thm);
   152 fun mono_del_global (thy, thm) = (map_monos (Drule.del_rules (mk_mono thm)) thy, thm);
   153 
   154 val mono_attr =
   155  (Attrib.add_del_args mono_add_global mono_del_global,
   156   Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute);
   157 
   158 
   159 
   160 (** misc utilities **)
   161 
   162 val quiet_mode = ref false;
   163 fun message s = if ! quiet_mode then () else writeln s;
   164 fun clean_message s = if ! quick_and_dirty then () else message s;
   165 
   166 fun coind_prefix true = "co"
   167   | coind_prefix false = "";
   168 
   169 
   170 (*the following code ensures that each recursive set always has the
   171   same type in all introduction rules*)
   172 fun unify_consts sign cs intr_ts =
   173   (let
   174     val {tsig, ...} = Sign.rep_sg sign;
   175     val add_term_consts_2 =
   176       foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
   177     fun varify (t, (i, ts)) =
   178       let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
   179       in (maxidx_of_term t', t'::ts) end;
   180     val (i, cs') = foldr varify (cs, (~1, []));
   181     val (i', intr_ts') = foldr varify (intr_ts, (i, []));
   182     val rec_consts = foldl add_term_consts_2 ([], cs');
   183     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
   184     fun unify (env, (cname, cT)) =
   185       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
   186       in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
   187           (env, (replicate (length consts) cT) ~~ consts)
   188       end;
   189     val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts);
   190     fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T
   191       in if T = T' then T else typ_subst_TVars_2 env T' end;
   192     val subst = fst o Type.freeze_thaw o
   193       (map_term_types (typ_subst_TVars_2 env))
   194 
   195   in (map subst cs', map subst intr_ts')
   196   end) handle Type.TUNIFY =>
   197     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
   198 
   199 
   200 (*make injections used in mutually recursive definitions*)
   201 fun mk_inj cs sumT c x =
   202   let
   203     fun mk_inj' T n i =
   204       if n = 1 then x else
   205       let val n2 = n div 2;
   206           val Type (_, [T1, T2]) = T
   207       in
   208         if i <= n2 then
   209           Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i)
   210         else
   211           Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
   212       end
   213   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
   214   end;
   215 
   216 (*make "vimage" terms for selecting out components of mutually rec.def*)
   217 fun mk_vimage cs sumT t c = if length cs < 2 then t else
   218   let
   219     val cT = HOLogic.dest_setT (fastype_of c);
   220     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
   221   in
   222     Const (vimage_name, vimageT) $
   223       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t
   224   end;
   225 
   226 
   227 
   228 (** process rules **)
   229 
   230 local
   231 
   232 fun err_in_rule sg name t msg =
   233   error (cat_lines ["Ill-formed introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
   234 
   235 fun err_in_prem sg name t p msg =
   236   error (cat_lines ["Ill-formed premise", Sign.string_of_term sg p,
   237     "in introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
   238 
   239 val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
   240 
   241 val atomize_cterm = InductMethod.rewrite_cterm inductive_atomize;
   242 fun full_simplify rews = Simplifier.full_simplify (HOL_basic_ss addsimps rews);
   243 
   244 in
   245 
   246 fun check_rule sg cs ((name, rule), att) =
   247   let
   248     val concl = Logic.strip_imp_concl rule;
   249     val prems = Logic.strip_imp_prems rule;
   250     val aprems = prems |> map (Thm.term_of o atomize_cterm o Thm.cterm_of sg);
   251     val arule = Logic.list_implies (aprems, concl);
   252 
   253     fun check_prem (prem, aprem) =
   254       if can HOLogic.dest_Trueprop aprem then ()
   255       else err_in_prem sg name rule prem "Non-atomic premise";
   256   in
   257     (case HOLogic.dest_Trueprop concl of
   258       (Const ("op :", _) $ t $ u) =>
   259         if u mem cs then
   260           if exists (Logic.occs o rpair t) cs then
   261             err_in_rule sg name rule "Recursion term on left of member symbol"
   262           else seq check_prem (prems ~~ aprems)
   263         else err_in_rule sg name rule bad_concl
   264       | _ => err_in_rule sg name rule bad_concl);
   265     ((name, arule), att)
   266   end;
   267 
   268 val rulify =
   269   standard o Tactic.norm_hhf o
   270   full_simplify inductive_rulify2 o full_simplify inductive_rulify1 o
   271   full_simplify inductive_conj;
   272 
   273 end;
   274 
   275 
   276 
   277 (** properties of (co)inductive sets **)
   278 
   279 (* elimination rules *)
   280 
   281 fun mk_elims cs cTs params intr_ts intr_names =
   282   let
   283     val used = foldr add_term_names (intr_ts, []);
   284     val [aname, pname] = variantlist (["a", "P"], used);
   285     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
   286 
   287     fun dest_intr r =
   288       let val Const ("op :", _) $ t $ u =
   289         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   290       in (u, t, Logic.strip_imp_prems r) end;
   291 
   292     val intrs = map dest_intr intr_ts ~~ intr_names;
   293 
   294     fun mk_elim (c, T) =
   295       let
   296         val a = Free (aname, T);
   297 
   298         fun mk_elim_prem (_, t, ts) =
   299           list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
   300             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
   301         val c_intrs = (filter (equal c o #1 o #1) intrs);
   302       in
   303         (Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
   304           map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs)
   305       end
   306   in
   307     map mk_elim (cs ~~ cTs)
   308   end;
   309 
   310 
   311 (* premises and conclusions of induction rules *)
   312 
   313 fun mk_indrule cs cTs params intr_ts =
   314   let
   315     val used = foldr add_term_names (intr_ts, []);
   316 
   317     (* predicates for induction rule *)
   318 
   319     val preds = map Free (variantlist (if length cs < 2 then ["P"] else
   320       map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
   321         map (fn T => T --> HOLogic.boolT) cTs);
   322 
   323     (* transform an introduction rule into a premise for induction rule *)
   324 
   325     fun mk_ind_prem r =
   326       let
   327         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   328 
   329         val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
   330 
   331         fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
   332               (case pred_of u of
   333                   None => (m $ fst (subst t) $ fst (subst u), None)
   334                 | Some P => (HOLogic.mk_binop inductive_conj_name (s, P $ t), Some (s, P $ t)))
   335           | subst s =
   336               (case pred_of s of
   337                   Some P => (HOLogic.mk_binop "op Int"
   338                     (s, HOLogic.Collect_const (HOLogic.dest_setT
   339                       (fastype_of s)) $ P), None)
   340                 | None => (case s of
   341                      (t $ u) => (fst (subst t) $ fst (subst u), None)
   342                    | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None)
   343                    | _ => (s, None)));
   344 
   345         fun mk_prem (s, prems) = (case subst s of
   346               (_, Some (t, u)) => t :: u :: prems
   347             | (t, _) => t :: prems);
   348 
   349         val Const ("op :", _) $ t $ u =
   350           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   351 
   352       in list_all_free (frees,
   353            Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
   354              (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
   355                HOLogic.mk_Trueprop (the (pred_of u) $ t)))
   356       end;
   357 
   358     val ind_prems = map mk_ind_prem intr_ts;
   359 
   360     (* make conclusions for induction rules *)
   361 
   362     fun mk_ind_concl ((c, P), (ts, x)) =
   363       let val T = HOLogic.dest_setT (fastype_of c);
   364           val Ts = HOLogic.prodT_factors T;
   365           val (frees, x') = foldr (fn (T', (fs, s)) =>
   366             ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
   367           val tuple = HOLogic.mk_tuple T frees;
   368       in ((HOLogic.mk_binop "op -->"
   369         (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
   370       end;
   371 
   372     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   373         (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
   374 
   375   in (preds, ind_prems, mutual_ind_concl)
   376   end;
   377 
   378 
   379 (* prepare cases and induct rules *)
   380 
   381 (*
   382   transform mutual rule:
   383     HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
   384   into i-th projection:
   385     xi:Ai ==> HH ==> Pi xi
   386 *)
   387 
   388 fun project_rules [name] rule = [(name, rule)]
   389   | project_rules names mutual_rule =
   390       let
   391         val n = length names;
   392         fun proj i =
   393           (if i < n then (fn th => th RS conjunct1) else I)
   394             (Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule)
   395             RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
   396       in names ~~ map proj (1 upto n) end;
   397 
   398 fun add_cases_induct no_elim no_ind names elims induct induct_cases =
   399   let
   400     fun cases_spec (name, elim) thy =
   401       thy
   402       |> Theory.add_path (Sign.base_name name)
   403       |> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
   404       |> Theory.parent_path;
   405     val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
   406 
   407     fun induct_spec (name, th) = (#1 o PureThy.add_thms
   408       [(("", th), [RuleCases.case_names induct_cases, InductAttrib.induct_set_global name])]);
   409     val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct);
   410   in Library.apply (cases_specs @ induct_specs) end;
   411 
   412 
   413 
   414 (** proofs for (co)inductive sets **)
   415 
   416 (* prove monotonicity -- NOT subject to quick_and_dirty! *)
   417 
   418 fun prove_mono setT fp_fun monos thy =
   419  (message "  Proving monotonicity ...";
   420   Goals.prove_goalw_cterm []      (*NO SkipProof.prove_goalw_cterm here!*)
   421     (Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
   422       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
   423     (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)]));
   424 
   425 
   426 (* prove introduction rules *)
   427 
   428 fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
   429   let
   430     val _ = clean_message "  Proving the introduction rules ...";
   431 
   432     val unfold = standard (mono RS (fp_def RS
   433       (if coind then def_gfp_unfold else def_lfp_unfold)));
   434 
   435     fun select_disj 1 1 = []
   436       | select_disj _ 1 = [rtac disjI1]
   437       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
   438 
   439     val intrs = map (fn (i, intr) => SkipProof.prove_goalw_cterm thy rec_sets_defs
   440       (Thm.cterm_of (Theory.sign_of thy) intr) (fn prems =>
   441        [(*insert prems and underlying sets*)
   442        cut_facts_tac prems 1,
   443        stac unfold 1,
   444        REPEAT (resolve_tac [vimageI2, CollectI] 1),
   445        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
   446        EVERY1 (select_disj (length intr_ts) i),
   447        (*Not ares_tac, since refl must be tried before any equality assumptions;
   448          backtracking may occur if the premises have extra variables!*)
   449        DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
   450        (*Now solve the equations like Inl 0 = Inl ?b2*)
   451        rewrite_goals_tac con_defs,
   452        REPEAT (rtac refl 1)])
   453       |> rulify) (1 upto (length intr_ts) ~~ intr_ts)
   454 
   455   in (intrs, unfold) end;
   456 
   457 
   458 (* prove elimination rules *)
   459 
   460 fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy =
   461   let
   462     val _ = clean_message "  Proving the elimination rules ...";
   463 
   464     val rules1 = [CollectE, disjE, make_elim vimageD, exE];
   465     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
   466   in
   467     map (fn (t, cases) => SkipProof.prove_goalw_cterm thy rec_sets_defs
   468       (Thm.cterm_of (Theory.sign_of thy) t) (fn prems =>
   469         [cut_facts_tac [hd prems] 1,
   470          dtac (unfold RS subst) 1,
   471          REPEAT (FIRSTGOAL (eresolve_tac rules1)),
   472          REPEAT (FIRSTGOAL (eresolve_tac rules2)),
   473          EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
   474       |> rulify
   475       |> RuleCases.name cases)
   476       (mk_elims cs cTs params intr_ts intr_names)
   477   end;
   478 
   479 
   480 (* derivation of simplified elimination rules *)
   481 
   482 (*Applies freeness of the given constructors, which *must* be unfolded by
   483   the given defs.  Cannot simply use the local con_defs because con_defs=[]
   484   for inference systems. (??) *)
   485 
   486 (*cprop should have the form t:Si where Si is an inductive set*)
   487 
   488 val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
   489 
   490 fun mk_cases_i elims ss cprop =
   491   let
   492     val prem = Thm.assume cprop;
   493     val tac = ALLGOALS (InductMethod.simp_case_tac false ss) THEN prune_params_tac;
   494     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (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_err, Pretty.fbrk, Display.pretty_cterm cprop])))
   500   end;
   501 
   502 fun mk_cases elims s =
   503   mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
   504 
   505 fun smart_mk_cases thy ss cprop =
   506   let
   507     val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop
   508       (Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err;
   509     val (_, {elims, ...}) = the_inductive thy c;
   510   in mk_cases_i elims ss cprop end;
   511 
   512 
   513 (* inductive_cases(_i) *)
   514 
   515 fun gen_inductive_cases prep_att prep_const prep_prop
   516     (((name, raw_atts), raw_props), comment) thy =
   517   let
   518     val ss = Simplifier.simpset_of thy;
   519     val sign = Theory.sign_of thy;
   520     val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
   521     val atts = map (prep_att thy) raw_atts;
   522     val thms = map (smart_mk_cases thy ss) cprops;
   523   in thy |> IsarThy.have_theorems_i [(((name, atts), map Thm.no_attributes thms), comment)] 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 (* mk_cases_meth *)
   532 
   533 fun mk_cases_meth (ctxt, raw_props) =
   534   let
   535     val thy = ProofContext.theory_of ctxt;
   536     val ss = Simplifier.get_local_simpset ctxt;
   537     val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props;
   538   in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
   539 
   540 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
   541 
   542 
   543 (* prove induction rule *)
   544 
   545 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
   546     fp_def rec_sets_defs thy =
   547   let
   548     val _ = clean_message "  Proving the induction rule ...";
   549 
   550     val sign = Theory.sign_of thy;
   551 
   552     val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
   553         None => []
   554       | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
   555 
   556     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   557 
   558     (* make predicate for instantiation of abstract induction rule *)
   559 
   560     fun mk_ind_pred _ [P] = P
   561       | mk_ind_pred T Ps =
   562          let val n = (length Ps) div 2;
   563              val Type (_, [T1, T2]) = T
   564          in Const ("Datatype.sum.sum_case",
   565            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
   566              mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
   567          end;
   568 
   569     val ind_pred = mk_ind_pred sumT preds;
   570 
   571     val ind_concl = HOLogic.mk_Trueprop
   572       (HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->"
   573         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0)));
   574 
   575     (* simplification rules for vimage and Collect *)
   576 
   577     val vimage_simps = if length cs < 2 then [] else
   578       map (fn c => SkipProof.prove_goalw_cterm thy [] (Thm.cterm_of sign
   579         (HOLogic.mk_Trueprop (HOLogic.mk_eq
   580           (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   581            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   582              nth_elem (find_index_eq c cs, preds)))))
   583         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
   584 
   585     val induct = SkipProof.prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
   586       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   587         [rtac (impI RS allI) 1,
   588          DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
   589          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
   590          fold_goals_tac rec_sets_defs,
   591          (*This CollectE and disjE separates out the introduction rules*)
   592          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
   593          (*Now break down the individual cases.  No disjE here in case
   594            some premise involves disjunction.*)
   595          REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
   596          rewrite_goals_tac sum_case_rewrites,
   597          EVERY (map (fn prem =>
   598            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
   599 
   600     val lemma = SkipProof.prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
   601       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
   602         [cut_facts_tac prems 1,
   603          REPEAT (EVERY
   604            [REPEAT (resolve_tac [conjI, impI] 1),
   605             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
   606             rewrite_goals_tac sum_case_rewrites,
   607             atac 1])])
   608 
   609   in standard (split_rule (induct RS lemma)) end;
   610 
   611 
   612 
   613 (** specification of (co)inductive sets **)
   614 
   615 fun cond_declare_consts declare_consts cs paramTs cnames =
   616   if declare_consts then
   617     Theory.add_consts_i (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   618   else I;
   619 
   620 fun mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   621       params paramTs cTs cnames =
   622   let
   623     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
   624     val setT = HOLogic.mk_setT sumT;
   625 
   626     val fp_name = if coind then gfp_name else lfp_name;
   627 
   628     val used = foldr add_term_names (intr_ts, []);
   629     val [sname, xname] = variantlist (["S", "x"], used);
   630 
   631     (* transform an introduction rule into a conjunction  *)
   632     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
   633     (* is transformed into                                *)
   634     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
   635 
   636     fun transform_rule r =
   637       let
   638         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   639         val subst = subst_free
   640           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
   641         val Const ("op :", _) $ t $ u =
   642           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   643 
   644       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
   645         (frees, foldr1 HOLogic.mk_conj
   646           (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
   647             (map (subst o HOLogic.dest_Trueprop)
   648               (Logic.strip_imp_prems r))))
   649       end
   650 
   651     (* make a disjunction of all introduction rules *)
   652 
   653     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
   654       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
   655 
   656     (* add definiton of recursive sets to theory *)
   657 
   658     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
   659     val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
   660 
   661     val rec_const = list_comb
   662       (Const (full_rec_name, paramTs ---> setT), params);
   663 
   664     val fp_def_term = Logic.mk_equals (rec_const,
   665       Const (fp_name, (setT --> setT) --> setT) $ fp_fun);
   666 
   667     val def_terms = fp_def_term :: (if length cs < 2 then [] else
   668       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
   669 
   670     val (thy', [fp_def :: rec_sets_defs]) =
   671       thy
   672       |> cond_declare_consts declare_consts cs paramTs cnames
   673       |> (if length cs < 2 then I
   674           else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
   675       |> Theory.add_path rec_name
   676       |> PureThy.add_defss_i false [(("defs", def_terms), [])];
   677 
   678     val mono = prove_mono setT fp_fun monos thy'
   679 
   680   in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
   681 
   682 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   683     atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
   684   let
   685     val _ =
   686       if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
   687         commas_quote cnames) else ();
   688 
   689     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   690 
   691     val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) =
   692       mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   693         params paramTs cTs cnames;
   694 
   695     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
   696       rec_sets_defs thy1;
   697     val elims = if no_elim then [] else
   698       prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy1;
   699     val raw_induct = if no_ind then Drule.asm_rl else
   700       if coind then standard (rule_by_tactic
   701         (rewrite_tac [mk_meta_eq vimage_Un] THEN
   702           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
   703       else
   704         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
   705           rec_sets_defs thy1;
   706     val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
   707       else standard (raw_induct RSN (2, rev_mp));
   708 
   709     val (thy2, intrs') =
   710       thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
   711     val (thy3, ([intrs'', elims'], [induct'])) =
   712       thy2
   713       |> PureThy.add_thmss [(("intros", intrs'), atts), (("elims", elims), [])]
   714       |>>> PureThy.add_thms
   715         [((coind_prefix coind ^ "induct", rulify induct), [RuleCases.case_names induct_cases])]
   716       |>> Theory.parent_path;
   717   in (thy3,
   718     {defs = fp_def :: rec_sets_defs,
   719      mono = mono,
   720      unfold = unfold,
   721      intrs = intrs'',
   722      elims = elims',
   723      mk_cases = mk_cases elims',
   724      raw_induct = rulify raw_induct,
   725      induct = induct'})
   726   end;
   727 
   728 
   729 (* external interfaces *)
   730 
   731 fun try_term f msg sign t =
   732   (case Library.try f t of
   733     Some x => x
   734   | None => error (msg ^ Sign.string_of_term sign t));
   735 
   736 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
   737     atts pre_intros monos con_defs thy =
   738   let
   739     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
   740     val sign = Theory.sign_of thy;
   741 
   742     (*parameters should agree for all mutually recursive components*)
   743     val (_, params) = strip_comb (hd cs);
   744     val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\
   745       \ component is not a free variable: " sign) params;
   746 
   747     val cTs = map (try_term (HOLogic.dest_setT o fastype_of)
   748       "Recursive component not of type set: " sign) cs;
   749 
   750     val full_cnames = map (try_term (fst o dest_Const o head_of)
   751       "Recursive set not previously declared as constant: " sign) cs;
   752     val cnames = map Sign.base_name full_cnames;
   753 
   754     val save_sign =
   755       thy |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames |> Theory.sign_of;
   756     val intros = map (check_rule save_sign cs) pre_intros;
   757     val induct_cases = map (#1 o #1) intros;
   758 
   759     val (thy1, result as {elims, induct, ...}) =
   760       add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
   761         con_defs thy params paramTs cTs cnames induct_cases;
   762     val thy2 = thy1
   763       |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
   764       |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct induct_cases;
   765   in (thy2, result) end;
   766 
   767 fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
   768   let
   769     val sign = Theory.sign_of thy;
   770     val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
   771 
   772     val atts = map (Attrib.global_attribute thy) srcs;
   773     val intr_names = map (fst o fst) intro_srcs;
   774     fun read_rule s = Thm.read_cterm sign (s, propT)
   775       handle ERROR => error ("The error(s) above occurred for " ^ s);
   776     val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
   777     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
   778     val (cs', intr_ts') = unify_consts sign cs intr_ts;
   779 
   780     val ((thy', con_defs), monos) = thy
   781       |> IsarThy.apply_theorems raw_monos
   782       |> apfst (IsarThy.apply_theorems raw_con_defs);
   783   in
   784     add_inductive_i verbose false "" coind false false cs'
   785       atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
   786   end;
   787 
   788 
   789 
   790 (** package setup **)
   791 
   792 (* setup theory *)
   793 
   794 val setup =
   795  [InductiveData.init,
   796   Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
   797     "dynamic case analysis on sets")],
   798   Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
   799 
   800 
   801 (* outer syntax *)
   802 
   803 local structure P = OuterParse and K = OuterSyntax.Keyword in
   804 
   805 fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
   806   #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
   807 
   808 fun ind_decl coind =
   809   (Scan.repeat1 P.term --| P.marg_comment) --
   810   (P.$$$ "intros" |--
   811     P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
   812   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
   813   Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
   814   >> (Toplevel.theory o mk_ind coind);
   815 
   816 val inductiveP =
   817   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
   818 
   819 val coinductiveP =
   820   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
   821 
   822 
   823 val ind_cases =
   824   P.opt_thm_name ":" -- Scan.repeat1 P.prop -- P.marg_comment
   825   >> (Toplevel.theory o inductive_cases);
   826 
   827 val inductive_casesP =
   828   OuterSyntax.command "inductive_cases"
   829     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
   830 
   831 val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"];
   832 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
   833 
   834 end;
   835 
   836 end;