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