src/HOL/Tools/old_inductive_package.ML
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 21395 f34ac19659ae
child 21879 a3efbae45735
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
     1 (*  Title:      HOL/Tools/old_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 
     7 (Co)Inductive Definition module for HOL.
     8 
     9 Features:
    10   * least or greatest fixedpoints
    11   * user-specified product and sum constructions
    12   * mutually recursive definitions
    13   * definitions involving arbitrary monotone operators
    14   * automatically proves introduction and elimination rules
    15 
    16 The recursive sets must *already* be declared as constants in the
    17 current theory!
    18 
    19   Introduction rules have the form
    20   [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk
    21   where M is some monotone operator (usually the identity)
    22   P(x) is any side condition on the free variables
    23   ti, t are any terms
    24   Sj, Sk are two of the sets being defined in mutual recursion
    25 
    26 Sums are used only for mutual recursion.  Products are used only to
    27 derive "streamlined" induction rules for relations.
    28 *)
    29 
    30 signature OLD_INDUCTIVE_PACKAGE =
    31 sig
    32   val quiet_mode: bool ref
    33   val trace: bool ref
    34   val unify_consts: theory -> term list -> term list -> term list * term list
    35   val split_rule_vars: term list -> thm -> thm
    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 the_mk_cases: theory -> string -> string -> thm
    40   val print_inductives: theory -> unit
    41   val mono_add: attribute
    42   val mono_del: attribute
    43   val get_monos: theory -> thm list
    44   val inductive_forall_name: string
    45   val inductive_forall_def: thm
    46   val rulify: thm -> thm
    47   val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
    48   val inductive_cases_i: ((bstring * attribute list) * term list) list -> theory -> theory
    49   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    50     ((bstring * term) * attribute list) list -> thm list -> theory -> theory *
    51       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    52        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    53   val add_inductive: bool -> bool -> string list ->
    54     ((bstring * string) * Attrib.src list) list -> (thmref * Attrib.src list) list ->
    55     theory -> theory *
    56       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    57        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    58   val setup: theory -> theory
    59 end;
    60 
    61 structure OldInductivePackage: OLD_INDUCTIVE_PACKAGE =
    62 struct
    63 
    64 
    65 (** theory context references **)
    66 
    67 val mono_name = "Orderings.mono";
    68 val gfp_name = "FixedPoint.gfp";
    69 val lfp_name = "FixedPoint.lfp";
    70 val vimage_name = "Set.vimage";
    71 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
    72 
    73 val inductive_forall_name = "HOL.induct_forall";
    74 val inductive_forall_def = thm "induct_forall_def";
    75 val inductive_conj_name = "HOL.induct_conj";
    76 val inductive_conj_def = thm "induct_conj_def";
    77 val inductive_conj = thms "induct_conj";
    78 val inductive_atomize = thms "induct_atomize";
    79 val inductive_rulify = thms "induct_rulify";
    80 val inductive_rulify_fallback = thms "induct_rulify_fallback";
    81 
    82 
    83 
    84 (** theory data **)
    85 
    86 type inductive_info =
    87   {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
    88     induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
    89 
    90 structure InductiveData = TheoryDataFun
    91 (struct
    92   val name = "HOL/inductive";
    93   type T = inductive_info Symtab.table * thm list;
    94 
    95   val empty = (Symtab.empty, []);
    96   val copy = I;
    97   val extend = I;
    98   fun merge _ ((tab1, monos1), (tab2, monos2)) =
    99     (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
   100 
   101   fun print thy (tab, monos) =
   102     [Pretty.strs ("(co)inductives:" ::
   103       map #1 (NameSpace.extern_table (Sign.const_space thy, tab))),
   104      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg thy) monos)]
   105     |> Pretty.chunks |> Pretty.writeln;
   106 end);
   107 
   108 val print_inductives = InductiveData.print;
   109 
   110 
   111 (* get and put data *)
   112 
   113 val get_inductive = Symtab.lookup o #1 o InductiveData.get;
   114 
   115 fun the_inductive thy name =
   116   (case get_inductive thy name of
   117     NONE => error ("Unknown (co)inductive set " ^ quote name)
   118   | SOME info => info);
   119 
   120 val the_mk_cases = (#mk_cases o #2) oo the_inductive;
   121 
   122 fun put_inductives names info = InductiveData.map (apfst (fn tab =>
   123   fold (fn name => Symtab.update_new (name, info)) names tab
   124     handle Symtab.DUP dup => error ("Duplicate definition of (co)inductive set " ^ quote dup)));
   125 
   126 
   127 
   128 (** monotonicity rules **)
   129 
   130 val get_monos = #2 o InductiveData.get;
   131 val map_monos = InductiveData.map o Library.apsnd;
   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 can Logic.dest_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 val mono_add = Thm.declaration_attribute (fn th =>
   152   Context.mapping (map_monos (fold Drule.add_rule (mk_mono th))) I);
   153 
   154 val mono_del = Thm.declaration_attribute (fn th =>
   155   Context.mapping (map_monos (fold Drule.del_rule (mk_mono th))) I);
   156 
   157 
   158 
   159 (** misc utilities **)
   160 
   161 val quiet_mode = ref false;
   162 val trace = ref false;  (*for debugging*)
   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 thy cs intr_ts =
   173   (let
   174     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
   175     fun varify (t, (i, ts)) =
   176       let val t' = map_types (Logic.incr_tvar (i + 1)) (snd (Type.varify [] t))
   177       in (maxidx_of_term t', t'::ts) end;
   178     val (i, cs') = foldr varify (~1, []) cs;
   179     val (i', intr_ts') = foldr varify (i, []) intr_ts;
   180     val rec_consts = fold add_term_consts_2 cs' [];
   181     val intr_consts = fold add_term_consts_2 intr_ts' [];
   182     fun unify (cname, cT) =
   183       let val consts = map snd (filter (fn (c, _) => c = cname) intr_consts)
   184       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
   185     val (env, _) = fold unify rec_consts (Vartab.empty, i');
   186     val subst = Type.freeze o map_types (Envir.norm_type env)
   187 
   188   in (map subst cs', map subst intr_ts')
   189   end) handle Type.TUNIFY =>
   190     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
   191 
   192 
   193 (*make injections used in mutually recursive definitions*)
   194 fun mk_inj cs sumT c x =
   195   let
   196     fun mk_inj' T n i =
   197       if n = 1 then x else
   198       let val n2 = n div 2;
   199           val Type (_, [T1, T2]) = T
   200       in
   201         if i <= n2 then
   202           Const ("Sum_Type.Inl", T1 --> T) $ (mk_inj' T1 n2 i)
   203         else
   204           Const ("Sum_Type.Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
   205       end
   206   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
   207   end;
   208 
   209 (*make "vimage" terms for selecting out components of mutually rec.def*)
   210 fun mk_vimage cs sumT t c = if length cs < 2 then t else
   211   let
   212     val cT = HOLogic.dest_setT (fastype_of c);
   213     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
   214   in
   215     Const (vimage_name, vimageT) $
   216       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t
   217   end;
   218 
   219 (** proper splitting **)
   220 
   221 fun prod_factors p (Const ("Pair", _) $ t $ u) =
   222       p :: prod_factors (1::p) t @ prod_factors (2::p) u
   223   | prod_factors p _ = [];
   224 
   225 fun mg_prod_factors ts (t $ u) fs = if t mem ts then
   226         let val f = prod_factors [] u
   227         in AList.update (op =) (t, f inter (AList.lookup (op =) fs t) |> the_default f) fs end
   228       else mg_prod_factors ts u (mg_prod_factors ts t fs)
   229   | mg_prod_factors ts (Abs (_, _, t)) fs = mg_prod_factors ts t fs
   230   | mg_prod_factors ts _ fs = fs;
   231 
   232 fun prodT_factors p ps (T as Type ("*", [T1, T2])) =
   233       if p mem ps then prodT_factors (1::p) ps T1 @ prodT_factors (2::p) ps T2
   234       else [T]
   235   | prodT_factors _ _ T = [T];
   236 
   237 fun ap_split p ps (Type ("*", [T1, T2])) T3 u =
   238       if p mem ps then HOLogic.split_const (T1, T2, T3) $
   239         Abs ("v", T1, ap_split (2::p) ps T2 T3 (ap_split (1::p) ps T1
   240           (prodT_factors (2::p) ps T2 ---> T3) (incr_boundvars 1 u) $ Bound 0))
   241       else u
   242   | ap_split _ _ _ _ u =  u;
   243 
   244 fun mk_tuple p ps (Type ("*", [T1, T2])) (tms as t::_) =
   245       if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms,
   246         mk_tuple (2::p) ps T2 (Library.drop (length (prodT_factors (1::p) ps T1), tms)))
   247       else t
   248   | mk_tuple _ _ _ (t::_) = t;
   249 
   250 fun split_rule_var' ((t as Var (v, Type ("fun", [T1, T2])), ps), rl) =
   251       let val T' = prodT_factors [] ps T1 ---> T2
   252           val newt = ap_split [] ps T1 T2 (Var (v, T'))
   253           val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
   254       in
   255           instantiate ([], [(cterm t, cterm newt)]) rl
   256       end
   257   | split_rule_var' (_, rl) = rl;
   258 
   259 val remove_split = rewrite_rule [split_conv RS eq_reflection];
   260 
   261 fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
   262   rl (mg_prod_factors vs (Thm.prop_of rl) [])));
   263 
   264 fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
   265   rl (List.mapPartial (fn (t as Var ((a, _), _)) =>
   266       Option.map (pair t) (AList.lookup (op =) vs a)) (term_vars (Thm.prop_of rl)))));
   267 
   268 
   269 (** process rules **)
   270 
   271 local
   272 
   273 fun err_in_rule thy name t msg =
   274   error (cat_lines ["Ill-formed introduction rule " ^ quote name,
   275     Sign.string_of_term thy t, msg]);
   276 
   277 fun err_in_prem thy name t p msg =
   278   error (cat_lines ["Ill-formed premise", Sign.string_of_term thy p,
   279     "in introduction rule " ^ quote name, Sign.string_of_term thy t, msg]);
   280 
   281 val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
   282 
   283 val all_not_allowed =
   284     "Introduction rule must not have a leading \"!!\" quantifier";
   285 
   286 fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize [];
   287 
   288 in
   289 
   290 fun check_rule thy cs ((name, rule), att) =
   291   let
   292     val concl = Logic.strip_imp_concl rule;
   293     val prems = Logic.strip_imp_prems rule;
   294     val aprems = map (atomize_term thy) prems;
   295     val arule = Logic.list_implies (aprems, concl);
   296 
   297     fun check_prem (prem, aprem) =
   298       if can HOLogic.dest_Trueprop aprem then ()
   299       else err_in_prem thy name rule prem "Non-atomic premise";
   300   in
   301     (case concl of
   302       Const ("Trueprop", _) $ (Const ("op :", _) $ t $ u) =>
   303         if u mem cs then
   304           if exists (Logic.occs o rpair t) cs then
   305             err_in_rule thy name rule "Recursion term on left of member symbol"
   306           else List.app check_prem (prems ~~ aprems)
   307         else err_in_rule thy name rule bad_concl
   308       | Const ("all", _) $ _ => err_in_rule thy name rule all_not_allowed
   309       | _ => err_in_rule thy name rule bad_concl);
   310     ((name, arule), att)
   311   end;
   312 
   313 val rulify =  (* FIXME norm_hhf *)
   314   hol_simplify inductive_conj
   315   #> hol_simplify inductive_rulify
   316   #> hol_simplify inductive_rulify_fallback
   317   #> standard;
   318 
   319 end;
   320 
   321 
   322 
   323 (** properties of (co)inductive sets **)
   324 
   325 (* elimination rules *)
   326 
   327 fun mk_elims cs cTs params intr_ts intr_names =
   328   let
   329     val used = foldr add_term_names [] intr_ts;
   330     val [aname, pname] = Name.variant_list used ["a", "P"];
   331     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
   332 
   333     fun dest_intr r =
   334       let val Const ("op :", _) $ t $ u =
   335         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   336       in (u, t, Logic.strip_imp_prems r) end;
   337 
   338     val intrs = map dest_intr intr_ts ~~ intr_names;
   339 
   340     fun mk_elim (c, T) =
   341       let
   342         val a = Free (aname, T);
   343 
   344         fun mk_elim_prem (_, t, ts) =
   345           list_all_free (map dest_Free ((foldr add_term_frees [] (t::ts)) \\ params),
   346             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
   347         val c_intrs = (List.filter (equal c o #1 o #1) intrs);
   348       in
   349         (Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
   350           map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs)
   351       end
   352   in
   353     map mk_elim (cs ~~ cTs)
   354   end;
   355 
   356 
   357 (* premises and conclusions of induction rules *)
   358 
   359 fun mk_indrule cs cTs params intr_ts =
   360   let
   361     val used = foldr add_term_names [] intr_ts;
   362 
   363     (* predicates for induction rule *)
   364 
   365     val preds = map Free (Name.variant_list used (if length cs < 2 then ["P"] else
   366       map (fn i => "P" ^ string_of_int i) (1 upto length cs)) ~~
   367         map (fn T => T --> HOLogic.boolT) cTs);
   368 
   369     (* transform an introduction rule into a premise for induction rule *)
   370 
   371     fun mk_ind_prem r =
   372       let
   373         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   374 
   375         val pred_of = AList.lookup (op aconv) (cs ~~ preds);
   376 
   377         fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
   378               (case pred_of u of
   379                   NONE => (m $ fst (subst t) $ fst (subst u), NONE)
   380                 | SOME P => (HOLogic.mk_binop inductive_conj_name (s, P $ t), SOME (s, P $ t)))
   381           | subst s =
   382               (case pred_of s of
   383                   SOME P => (HOLogic.mk_binop "op Int"
   384                     (s, HOLogic.Collect_const (HOLogic.dest_setT
   385                       (fastype_of s)) $ P), NONE)
   386                 | NONE => (case s of
   387                      (t $ u) => (fst (subst t) $ fst (subst u), NONE)
   388                    | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
   389                    | _ => (s, NONE)));
   390 
   391         fun mk_prem (s, prems) = (case subst s of
   392               (_, SOME (t, u)) => t :: u :: prems
   393             | (t, _) => t :: prems);
   394 
   395         val Const ("op :", _) $ t $ u =
   396           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   397 
   398       in list_all_free (frees,
   399            Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
   400              [] (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r))),
   401                HOLogic.mk_Trueprop (valOf (pred_of u) $ t)))
   402       end;
   403 
   404     val ind_prems = map mk_ind_prem intr_ts;
   405 
   406     val factors = fold (mg_prod_factors preds) ind_prems [];
   407 
   408     (* make conclusions for induction rules *)
   409 
   410     fun mk_ind_concl ((c, P), (ts, x)) =
   411       let val T = HOLogic.dest_setT (fastype_of c);
   412           val ps = AList.lookup (op =) factors P |> the_default [];
   413           val Ts = prodT_factors [] ps T;
   414           val (frees, x') = foldr (fn (T', (fs, s)) =>
   415             ((Free (s, T'))::fs, Symbol.bump_string s)) ([], x) Ts;
   416           val tuple = mk_tuple [] ps T frees;
   417       in ((HOLogic.mk_binop "op -->"
   418         (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
   419       end;
   420 
   421     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   422         (fst (foldr mk_ind_concl ([], "xa") (cs ~~ preds))))
   423 
   424   in (preds, ind_prems, mutual_ind_concl,
   425     map (apfst (fst o dest_Free)) factors)
   426   end;
   427 
   428 
   429 (* prepare cases and induct rules *)
   430 
   431 fun add_cases_induct no_elim no_induct coind names elims induct =
   432   let
   433     fun cases_spec name elim thy =
   434       thy
   435       |> Theory.parent_path
   436       |> Theory.add_path (Sign.base_name name)
   437       |> PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set name])] |> snd
   438       |> Theory.restore_naming thy;
   439     val cases_specs = if no_elim then [] else map2 cases_spec names elims;
   440 
   441     val induct_att = if coind then InductAttrib.coinduct_set else InductAttrib.induct_set;
   442     fun induct_specs thy =
   443       if no_induct then thy
   444       else
   445         let
   446           val ctxt = ProofContext.init thy;
   447           val rules = names ~~ ProjectRule.projects ctxt (1 upto length names) induct;
   448           val inducts = map (RuleCases.save induct o standard o #2) rules;
   449         in
   450           thy
   451           |> PureThy.add_thms (rules |> map (fn (name, th) =>
   452             (("", th), [RuleCases.consumes 1, induct_att name]))) |> snd
   453           |> PureThy.add_thmss
   454             [((coind_prefix coind ^ "inducts", inducts), [RuleCases.consumes 1])] |> snd
   455         end;
   456   in Library.apply cases_specs #> induct_specs end;
   457 
   458 
   459 
   460 (** proofs for (co)inductive sets **)
   461 
   462 (* prove monotonicity -- NOT subject to quick_and_dirty! *)
   463 
   464 fun prove_mono setT fp_fun monos thy =
   465  (message "  Proving monotonicity ...";
   466   Goal.prove_global thy [] []   (*NO quick_and_dirty here!*)
   467     (HOLogic.mk_Trueprop
   468       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun))
   469     (fn _ => EVERY [rtac monoI 1,
   470       REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)]));
   471 
   472 
   473 (* prove introduction rules *)
   474 
   475 fun prove_intrs coind mono fp_def intr_ts rec_sets_defs ctxt =
   476   let
   477     val _ = clean_message "  Proving the introduction rules ...";
   478 
   479     val unfold = standard' (mono RS (fp_def RS
   480       (if coind then def_gfp_unfold else def_lfp_unfold)));
   481 
   482     fun select_disj 1 1 = []
   483       | select_disj _ 1 = [rtac disjI1]
   484       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
   485 
   486     val intrs = (1 upto (length intr_ts) ~~ intr_ts) |> map (fn (i, intr) =>
   487       rulify (SkipProof.prove ctxt [] [] intr (fn _ => EVERY
   488        [rewrite_goals_tac rec_sets_defs,
   489         stac unfold 1,
   490         REPEAT (resolve_tac [vimageI2, CollectI] 1),
   491         (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
   492         EVERY1 (select_disj (length intr_ts) i),
   493         (*Not ares_tac, since refl must be tried before any equality assumptions;
   494           backtracking may occur if the premises have extra variables!*)
   495         DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
   496         (*Now solve the equations like Inl 0 = Inl ?b2*)
   497         REPEAT (rtac refl 1)])))
   498 
   499   in (intrs, unfold) end;
   500 
   501 
   502 (* prove elimination rules *)
   503 
   504 fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs ctxt =
   505   let
   506     val _ = clean_message "  Proving the elimination rules ...";
   507 
   508     val rules1 = [CollectE, disjE, make_elim vimageD, exE, FalseE];
   509     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
   510   in
   511     mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
   512       SkipProof.prove ctxt [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
   513         (fn {prems, ...} => EVERY
   514           [cut_facts_tac [hd prems] 1,
   515            rewrite_goals_tac rec_sets_defs,
   516            dtac (unfold RS subst) 1,
   517            REPEAT (FIRSTGOAL (eresolve_tac rules1)),
   518            REPEAT (FIRSTGOAL (eresolve_tac rules2)),
   519            EVERY (map (fn prem =>
   520              DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_sets_defs prem, conjI] 1)) (tl prems))])
   521         |> rulify
   522         |> RuleCases.name cases)
   523   end;
   524 
   525 
   526 (* derivation of simplified elimination rules *)
   527 
   528 local
   529 
   530 (*cprop should have the form t:Si where Si is an inductive set*)
   531 val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
   532 
   533 (*delete needless equality assumptions*)
   534 val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
   535 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
   536 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
   537 
   538 fun simp_case_tac solved ss i =
   539   EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i
   540   THEN_MAYBE (if solved then no_tac else all_tac);
   541 
   542 in
   543 
   544 fun mk_cases_i elims ss cprop =
   545   let
   546     val prem = Thm.assume cprop;
   547     val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac;
   548     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
   549   in
   550     (case get_first (try mk_elim) elims of
   551       SOME r => r
   552     | NONE => error (Pretty.string_of (Pretty.block
   553         [Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop])))
   554   end;
   555 
   556 fun mk_cases elims s =
   557   mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.theory_of_thm (hd elims)) (s, propT));
   558 
   559 fun smart_mk_cases thy ss cprop =
   560   let
   561     val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop
   562       (Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err;
   563     val (_, {elims, ...}) = the_inductive thy c;
   564   in mk_cases_i elims ss cprop end;
   565 
   566 end;
   567 
   568 
   569 (* inductive_cases(_i) *)
   570 
   571 fun gen_inductive_cases prep_att prep_prop args thy =
   572   let
   573     val cert_prop = Thm.cterm_of thy o prep_prop (ProofContext.init thy);
   574     val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop;
   575 
   576     val facts = args |> map (fn ((a, atts), props) =>
   577      ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
   578   in thy |> PureThy.note_thmss_i "" facts |> snd end;
   579 
   580 val inductive_cases = gen_inductive_cases Attrib.attribute ProofContext.read_prop;
   581 val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
   582 
   583 
   584 (* mk_cases_meth *)
   585 
   586 fun mk_cases_meth (ctxt, raw_props) =
   587   let
   588     val thy = ProofContext.theory_of ctxt;
   589     val ss = local_simpset_of ctxt;
   590     val cprops = map (Thm.cterm_of thy o ProofContext.read_prop ctxt) raw_props;
   591   in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
   592 
   593 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
   594 
   595 
   596 (* prove induction rule *)
   597 
   598 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
   599     fp_def rec_sets_defs ctxt =
   600   let
   601     val _ = clean_message "  Proving the induction rule ...";
   602     val thy = ProofContext.theory_of ctxt;
   603 
   604     val sum_case_rewrites =
   605       (if Context.theory_name thy = "Datatype" then
   606         PureThy.get_thms thy (Name "sum.cases")
   607       else
   608         (case ThyInfo.lookup_theory "Datatype" of
   609           NONE => []
   610         | SOME thy' =>
   611             if Theory.subthy (thy', thy) then
   612               PureThy.get_thms thy' (Name "sum.cases")
   613             else []))
   614       |> map mk_meta_eq;
   615 
   616     val (preds, ind_prems, mutual_ind_concl, factors) =
   617       mk_indrule cs cTs params intr_ts;
   618 
   619     val dummy = if !trace then
   620                 (writeln "ind_prems = ";
   621                  List.app (writeln o Sign.string_of_term thy) ind_prems)
   622             else ();
   623 
   624     (* make predicate for instantiation of abstract induction rule *)
   625 
   626     fun mk_ind_pred _ [P] = P
   627       | mk_ind_pred T Ps =
   628          let val n = (length Ps) div 2;
   629              val Type (_, [T1, T2]) = T
   630          in Const ("Datatype.sum.sum_case",
   631            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
   632              mk_ind_pred T1 (Library.take (n, Ps)) $ mk_ind_pred T2 (Library.drop (n, Ps))
   633          end;
   634 
   635     val ind_pred = mk_ind_pred sumT preds;
   636 
   637     val ind_concl = HOLogic.mk_Trueprop
   638       (HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->"
   639         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0)));
   640 
   641     (* simplification rules for vimage and Collect *)
   642 
   643     val vimage_simps = if length cs < 2 then [] else
   644       map (fn c => standard (SkipProof.prove ctxt [] []
   645         (HOLogic.mk_Trueprop (HOLogic.mk_eq
   646           (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   647            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   648              List.nth (preds, find_index_eq c cs))))
   649         (fn _ => EVERY
   650           [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1]))) cs;
   651 
   652     val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct_set));
   653 
   654     val dummy = if !trace then
   655                 (writeln "raw_fp_induct = "; print_thm raw_fp_induct)
   656             else ();
   657 
   658     val induct = standard (SkipProof.prove ctxt [] ind_prems ind_concl
   659       (fn {prems, ...} => EVERY
   660         [rewrite_goals_tac [inductive_conj_def],
   661          rtac (impI RS allI) 1,
   662          DETERM (etac raw_fp_induct 1),
   663          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
   664          fold_goals_tac rec_sets_defs,
   665          (*This CollectE and disjE separates out the introduction rules*)
   666          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE, FalseE])),
   667          (*Now break down the individual cases.  No disjE here in case
   668            some premise involves disjunction.*)
   669          REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
   670          rewrite_goals_tac sum_case_rewrites,
   671          EVERY (map (fn prem =>
   672            DEPTH_SOLVE_1 (ares_tac [rewrite_rule [inductive_conj_def] prem, conjI, refl] 1)) prems)]));
   673 
   674     val lemma = standard (SkipProof.prove ctxt [] []
   675       (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
   676         [rewrite_goals_tac rec_sets_defs,
   677          REPEAT (EVERY
   678            [REPEAT (resolve_tac [conjI, impI] 1),
   679             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
   680             rewrite_goals_tac sum_case_rewrites,
   681             atac 1])]))
   682 
   683   in standard (split_rule factors (induct RS lemma)) end;
   684 
   685 
   686 
   687 (** specification of (co)inductive sets **)
   688 
   689 fun cond_declare_consts declare_consts cs paramTs cnames =
   690   if declare_consts then
   691     Theory.add_consts_i (map (fn (c, n) => (Sign.base_name n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   692   else I;
   693 
   694 fun mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
   695       params paramTs cTs cnames =
   696   let
   697     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
   698     val setT = HOLogic.mk_setT sumT;
   699 
   700     val fp_name = if coind then gfp_name else lfp_name;
   701 
   702     val used = foldr add_term_names [] intr_ts;
   703     val [sname, xname] = Name.variant_list used ["S", "x"];
   704 
   705     (* transform an introduction rule into a conjunction  *)
   706     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
   707     (* is transformed into                                *)
   708     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
   709 
   710     fun transform_rule r =
   711       let
   712         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   713         val subst = subst_free
   714           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
   715         val Const ("op :", _) $ t $ u =
   716           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   717 
   718       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
   719         (foldr1 HOLogic.mk_conj
   720           (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
   721             (map (subst o HOLogic.dest_Trueprop)
   722               (Logic.strip_imp_prems r)))) frees
   723       end
   724 
   725     (* make a disjunction of all introduction rules *)
   726 
   727     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
   728       absfree (xname, sumT, if null intr_ts then HOLogic.false_const
   729         else foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
   730 
   731     (* add definiton of recursive sets to theory *)
   732 
   733     val rec_name = if alt_name = "" then
   734       space_implode "_" (map Sign.base_name cnames) else alt_name;
   735     val full_rec_name = if length cs < 2 then hd cnames
   736       else Sign.full_name thy rec_name;
   737 
   738     val rec_const = list_comb
   739       (Const (full_rec_name, paramTs ---> setT), params);
   740 
   741     val fp_def_term = Logic.mk_equals (rec_const,
   742       Const (fp_name, (setT --> setT) --> setT) $ fp_fun);
   743 
   744     val def_terms = fp_def_term :: (if length cs < 2 then [] else
   745       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
   746 
   747     val ([fp_def :: rec_sets_defs], thy') =
   748       thy
   749       |> cond_declare_consts declare_consts cs paramTs cnames
   750       |> (if length cs < 2 then I
   751           else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
   752       |> Theory.add_path rec_name
   753       |> PureThy.add_defss_i false [(("defs", def_terms), [])];
   754 
   755     val mono = prove_mono setT fp_fun monos thy'
   756 
   757   in (thy', rec_name, mono, fp_def, rec_sets_defs, rec_const, sumT) end;
   758 
   759 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   760     intros monos thy params paramTs cTs cnames induct_cases =
   761   let
   762     val _ =
   763       if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
   764         commas_quote (map Sign.base_name cnames)) else ();
   765 
   766     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   767 
   768     val (thy1, rec_name, mono, fp_def, rec_sets_defs, rec_const, sumT) =
   769       mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
   770         params paramTs cTs cnames;
   771     val ctxt1 = ProofContext.init thy1;
   772 
   773     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts rec_sets_defs ctxt1;
   774     val elims = if no_elim then [] else
   775       prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs ctxt1;
   776     val raw_induct = if no_ind then Drule.asm_rl else
   777       if coind then standard (rule_by_tactic
   778         (rewrite_tac [mk_meta_eq vimage_Un] THEN
   779           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
   780       else
   781         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
   782           rec_sets_defs ctxt1;
   783     val induct =
   784       if coind then
   785         (raw_induct, [RuleCases.case_names [rec_name],
   786           RuleCases.case_conclusion (rec_name, induct_cases),
   787           RuleCases.consumes 1])
   788       else if no_ind orelse length cs > 1 then
   789         (raw_induct, [RuleCases.case_names induct_cases, RuleCases.consumes 0])
   790       else (raw_induct RSN (2, rev_mp), [RuleCases.case_names induct_cases, RuleCases.consumes 1]);
   791 
   792     val (intrs', thy2) =
   793       thy1
   794       |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
   795     val (([_, elims'], [induct']), thy3) =
   796       thy2
   797       |> PureThy.add_thmss
   798         [(("intros", intrs'), []),
   799           (("elims", elims), [RuleCases.consumes 1])]
   800       ||>> PureThy.add_thms
   801         [((coind_prefix coind ^ "induct", rulify (#1 induct)), #2 induct)];
   802   in (thy3,
   803     {defs = fp_def :: rec_sets_defs,
   804      mono = mono,
   805      unfold = unfold,
   806      intrs = intrs',
   807      elims = elims',
   808      mk_cases = mk_cases elims',
   809      raw_induct = rulify raw_induct,
   810      induct = induct'})
   811   end;
   812 
   813 
   814 (* external interfaces *)
   815 
   816 fun try_term f msg thy t =
   817   (case try f t of
   818     SOME x => x
   819   | NONE => error (msg ^ Sign.string_of_term thy t));
   820 
   821 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy =
   822   let
   823     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
   824 
   825     (*parameters should agree for all mutually recursive components*)
   826     val (_, params) = strip_comb (hd cs);
   827     val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\
   828       \ component is not a free variable: " thy) params;
   829 
   830     val cTs = map (try_term (HOLogic.dest_setT o fastype_of)
   831       "Recursive component not of type set: " thy) cs;
   832 
   833     val cnames = map (try_term (fst o dest_Const o head_of)
   834       "Recursive set not previously declared as constant: " thy) cs;
   835 
   836     val save_thy = thy
   837       |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames;
   838     val intros = map (check_rule save_thy cs) pre_intros;
   839     val induct_cases = map (#1 o #1) intros;
   840 
   841     val (thy1, result as {elims, induct, ...}) =
   842       add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos
   843         thy params paramTs cTs cnames induct_cases;
   844     val thy2 = thy1
   845       |> put_inductives cnames ({names = cnames, coind = coind}, result)
   846       |> add_cases_induct no_elim no_ind coind cnames elims induct
   847       |> Theory.parent_path;
   848   in (thy2, result) end;
   849 
   850 fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =
   851   let
   852     val cs = map (Sign.read_term thy) c_strings;
   853 
   854     val intr_names = map (fst o fst) intro_srcs;
   855     fun read_rule s = Thm.read_cterm thy (s, propT)
   856       handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s);
   857     val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
   858     val intr_atts = map (map (Attrib.attribute thy) o snd) intro_srcs;
   859     val (cs', intr_ts') = unify_consts thy cs intr_ts;
   860 
   861     val (monos, thy') = thy |> IsarCmd.apply_theorems raw_monos;
   862   in
   863     add_inductive_i verbose false "" coind false false cs'
   864       ((intr_names ~~ intr_ts') ~~ intr_atts) monos thy'
   865   end;
   866 
   867 
   868 
   869 (** package setup **)
   870 
   871 (* setup theory *)
   872 
   873 val setup =
   874   InductiveData.init #>
   875   Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
   876     "dynamic case analysis on sets")] #>
   877   Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del,
   878     "declaration of monotonicity rule")];
   879 
   880 
   881 (* outer syntax *)
   882 
   883 local structure P = OuterParse and K = OuterKeyword in
   884 
   885 fun mk_ind coind ((sets, intrs), monos) =
   886   #1 o add_inductive true coind sets (map P.triple_swap intrs) monos;
   887 
   888 fun ind_decl coind =
   889   Scan.repeat1 P.term --
   890   (P.$$$ "intros" |--
   891     P.!!! (Scan.repeat (P.opt_thm_name ":" -- P.prop))) --
   892   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) []
   893   >> (Toplevel.theory o mk_ind coind);
   894 
   895 val inductiveP =
   896   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
   897 
   898 val coinductiveP =
   899   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
   900 
   901 
   902 val ind_cases =
   903   P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
   904   >> (Toplevel.theory o inductive_cases);
   905 
   906 val inductive_casesP =
   907   OuterSyntax.command "inductive_cases"
   908     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
   909 
   910 val _ = OuterSyntax.add_keywords ["intros", "monos"];
   911 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
   912 
   913 end;
   914 
   915 end;
   916