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