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