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