src/HOL/Tools/inductive_package.ML
author wenzelm
Wed Aug 09 20:46:58 2000 +0200 (2000-08-09)
changeset 9562 6b07b56aa3a8
parent 9405 3235873fdd90
child 9598 65ee72db0236
permissions -rw-r--r--
fixed mk_cases_i: TRYALL InductMethod.simp_case_tac;
     1 (*  Title:      HOL/Tools/inductive_package.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4                 Stefan Berghofer,   TU Muenchen
     5     Copyright   1994  University of Cambridge
     6                 1998  TU Muenchen     
     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 unify_consts: Sign.sg -> term list -> term list -> term list * term list
    35   val get_inductive: theory -> string -> ({names: string list, coind: bool} *
    36     {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    37      intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
    38   val print_inductives: theory -> unit
    39   val mono_add_global: theory attribute
    40   val mono_del_global: theory attribute
    41   val get_monos: theory -> thm list
    42   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
    43     theory attribute list -> ((bstring * term) * theory attribute list) list ->
    44       thm list -> thm list -> theory -> theory *
    45       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    46        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    47   val add_inductive: bool -> bool -> string list -> Args.src list ->
    48     ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
    49       (xstring * Args.src list) list -> theory -> theory *
    50       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
    51        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
    52   val inductive_cases: (((bstring * Args.src list) * xstring) * string list) * Comment.text
    53     -> theory -> theory
    54   val inductive_cases_i: (((bstring * theory attribute list) * string) * term list) * Comment.text
    55     -> theory -> theory
    56   val setup: (theory -> theory) list
    57 end;
    58 
    59 structure InductivePackage: INDUCTIVE_PACKAGE =
    60 struct
    61 
    62 (*** theory data ***)
    63 
    64 (* data kind 'HOL/inductive' *)
    65 
    66 type inductive_info =
    67   {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
    68     induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
    69 
    70 structure InductiveArgs =
    71 struct
    72   val name = "HOL/inductive";
    73   type T = inductive_info Symtab.table * thm list;
    74 
    75   val empty = (Symtab.empty, []);
    76   val copy = I;
    77   val prep_ext = I;
    78   fun merge ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2),
    79     Library.generic_merge Thm.eq_thm I I monos1 monos2);
    80 
    81   fun print sg (tab, monos) =
    82     [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
    83      Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)]
    84     |> Pretty.chunks |> Pretty.writeln;
    85 end;
    86 
    87 structure InductiveData = TheoryDataFun(InductiveArgs);
    88 val print_inductives = InductiveData.print;
    89 
    90 
    91 (* get and put data *)
    92 
    93 fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name);
    94 
    95 fun put_inductives names info thy =
    96   let
    97     fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
    98     val tab_monos = foldl upd (InductiveData.get thy, names)
    99       handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
   100   in InductiveData.put tab_monos thy end;
   101 
   102 
   103 
   104 (** monotonicity rules **)
   105 
   106 val get_monos = snd o InductiveData.get;
   107 fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy;
   108 
   109 fun mk_mono thm =
   110   let
   111     fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @
   112       (case concl_of thm of
   113           (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
   114         | _ => [standard (thm' RS (thm' RS eq_to_mono2))]);
   115     val concl = concl_of thm
   116   in
   117     if Logic.is_equals concl then
   118       eq2mono (thm RS meta_eq_to_obj_eq)
   119     else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
   120       eq2mono thm
   121     else [thm]
   122   end;
   123 
   124 
   125 (* attributes *)
   126 
   127 local
   128 
   129 fun map_rules_global f thy = put_monos (f (get_monos thy)) thy;
   130 
   131 fun add_mono thm rules = Library.gen_union Thm.eq_thm (mk_mono thm, rules);
   132 fun del_mono thm rules = Library.gen_rems Thm.eq_thm (rules, mk_mono thm);
   133 
   134 fun mk_att f g (x, thm) = (f (g thm) x, thm);
   135 
   136 in
   137   val mono_add_global = mk_att map_rules_global add_mono;
   138   val mono_del_global = mk_att map_rules_global del_mono;
   139 end;
   140 
   141 val mono_attr =
   142  (Attrib.add_del_args mono_add_global mono_del_global,
   143   Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute);
   144 
   145 
   146 
   147 (** utilities **)
   148 
   149 (* messages *)
   150 
   151 val quiet_mode = ref false;
   152 fun message s = if !quiet_mode then () else writeln s;
   153 
   154 fun coind_prefix true = "co"
   155   | coind_prefix false = "";
   156 
   157 
   158 (* the following code ensures that each recursive set *)
   159 (* always has the same type in all introduction rules *)
   160 
   161 fun unify_consts sign cs intr_ts =
   162   (let
   163     val {tsig, ...} = Sign.rep_sg sign;
   164     val add_term_consts_2 =
   165       foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
   166     fun varify (t, (i, ts)) =
   167       let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
   168       in (maxidx_of_term t', t'::ts) end;
   169     val (i, cs') = foldr varify (cs, (~1, []));
   170     val (i', intr_ts') = foldr varify (intr_ts, (i, []));
   171     val rec_consts = foldl add_term_consts_2 ([], cs');
   172     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
   173     fun unify (env, (cname, cT)) =
   174       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
   175       in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
   176           (env, (replicate (length consts) cT) ~~ consts)
   177       end;
   178     val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts);
   179     fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T
   180       in if T = T' then T else typ_subst_TVars_2 env T' end;
   181     val subst = fst o Type.freeze_thaw o
   182       (map_term_types (typ_subst_TVars_2 env))
   183 
   184   in (map subst cs', map subst intr_ts')
   185   end) handle Type.TUNIFY =>
   186     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
   187 
   188 
   189 (* misc *)
   190 
   191 val Const _ $ (vimage_f $ _) $ _ = HOLogic.dest_Trueprop (concl_of vimageD);
   192 
   193 val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``";
   194 val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
   195 
   196 (* make injections needed in mutually recursive definitions *)
   197 
   198 fun mk_inj cs sumT c x =
   199   let
   200     fun mk_inj' T n i =
   201       if n = 1 then x else
   202       let val n2 = n div 2;
   203           val Type (_, [T1, T2]) = T
   204       in
   205         if i <= n2 then
   206           Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i)
   207         else
   208           Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
   209       end
   210   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
   211   end;
   212 
   213 (* make "vimage" terms for selecting out components of mutually rec.def. *)
   214 
   215 fun mk_vimage cs sumT t c = if length cs < 2 then t else
   216   let
   217     val cT = HOLogic.dest_setT (fastype_of c);
   218     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
   219   in
   220     Const (vimage_name, vimageT) $
   221       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t
   222   end;
   223 
   224 
   225 
   226 (** well-formedness checks **)
   227 
   228 fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^
   229   (Sign.string_of_term sign t) ^ "\n" ^ msg);
   230 
   231 fun err_in_prem sign t p msg = error ("Ill-formed premise\n" ^
   232   (Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^
   233   (Sign.string_of_term sign t) ^ "\n" ^ msg);
   234 
   235 val msg1 = "Conclusion of introduction rule must have form\
   236           \ ' t : S_i '";
   237 val msg2 = "Non-atomic premise";
   238 val msg3 = "Recursion term on left of member symbol";
   239 
   240 fun check_rule sign cs r =
   241   let
   242     fun check_prem prem = if can HOLogic.dest_Trueprop prem then ()
   243       else err_in_prem sign r prem msg2;
   244 
   245   in (case HOLogic.dest_Trueprop (Logic.strip_imp_concl r) of
   246         (Const ("op :", _) $ t $ u) =>
   247           if u mem cs then
   248             if exists (Logic.occs o (rpair t)) cs then
   249               err_in_rule sign r msg3
   250             else
   251               seq check_prem (Logic.strip_imp_prems r)
   252           else err_in_rule sign r msg1
   253       | _ => err_in_rule sign r msg1)
   254   end;
   255 
   256 fun try' f msg sign t = (case (try f t) of
   257       Some x => x
   258     | None => error (msg ^ Sign.string_of_term sign t));
   259 
   260 
   261 
   262 (*** properties of (co)inductive sets ***)
   263 
   264 (** elimination rules **)
   265 
   266 fun mk_elims cs cTs params intr_ts intr_names =
   267   let
   268     val used = foldr add_term_names (intr_ts, []);
   269     val [aname, pname] = variantlist (["a", "P"], used);
   270     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
   271 
   272     fun dest_intr r =
   273       let val Const ("op :", _) $ t $ u =
   274         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   275       in (u, t, Logic.strip_imp_prems r) end;
   276 
   277     val intrs = map dest_intr intr_ts ~~ intr_names;
   278 
   279     fun mk_elim (c, T) =
   280       let
   281         val a = Free (aname, T);
   282 
   283         fun mk_elim_prem (_, t, ts) =
   284           list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
   285             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
   286         val c_intrs = (filter (equal c o #1 o #1) intrs);
   287       in
   288         (Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
   289           map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs)
   290       end
   291   in
   292     map mk_elim (cs ~~ cTs)
   293   end;
   294         
   295 
   296 
   297 (** premises and conclusions of induction rules **)
   298 
   299 fun mk_indrule cs cTs params intr_ts =
   300   let
   301     val used = foldr add_term_names (intr_ts, []);
   302 
   303     (* predicates for induction rule *)
   304 
   305     val preds = map Free (variantlist (if length cs < 2 then ["P"] else
   306       map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
   307         map (fn T => T --> HOLogic.boolT) cTs);
   308 
   309     (* transform an introduction rule into a premise for induction rule *)
   310 
   311     fun mk_ind_prem r =
   312       let
   313         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   314 
   315         val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
   316 
   317         fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
   318               (case pred_of u of
   319                   None => (m $ fst (subst t) $ fst (subst u), None)
   320                 | Some P => (HOLogic.conj $ s $ (P $ t), Some (s, P $ t)))
   321           | subst s =
   322               (case pred_of s of
   323                   Some P => (HOLogic.mk_binop "op Int"
   324                     (s, HOLogic.Collect_const (HOLogic.dest_setT
   325                       (fastype_of s)) $ P), None)
   326                 | None => (case s of
   327                      (t $ u) => (fst (subst t) $ fst (subst u), None)
   328                    | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None)
   329                    | _ => (s, None)));
   330 
   331         fun mk_prem (s, prems) = (case subst s of
   332               (_, Some (t, u)) => t :: u :: prems
   333             | (t, _) => t :: prems);
   334           
   335         val Const ("op :", _) $ t $ u =
   336           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   337 
   338       in list_all_free (frees,
   339            Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
   340              (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
   341                HOLogic.mk_Trueprop (the (pred_of u) $ t)))
   342       end;
   343 
   344     val ind_prems = map mk_ind_prem intr_ts;
   345 
   346     (* make conclusions for induction rules *)
   347 
   348     fun mk_ind_concl ((c, P), (ts, x)) =
   349       let val T = HOLogic.dest_setT (fastype_of c);
   350           val Ts = HOLogic.prodT_factors T;
   351           val (frees, x') = foldr (fn (T', (fs, s)) =>
   352             ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
   353           val tuple = HOLogic.mk_tuple T frees;
   354       in ((HOLogic.mk_binop "op -->"
   355         (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
   356       end;
   357 
   358     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
   359         (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
   360 
   361   in (preds, ind_prems, mutual_ind_concl)
   362   end;
   363 
   364 
   365 
   366 (** prepare cases and induct rules **)
   367 
   368 (*
   369   transform mutual rule:
   370     HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
   371   into i-th projection:
   372     xi:Ai ==> HH ==> Pi xi
   373 *)
   374 
   375 fun project_rules [name] rule = [(name, rule)]
   376   | project_rules names mutual_rule =
   377       let
   378         val n = length names;
   379         fun proj i =
   380           (if i < n then (fn th => th RS conjunct1) else I)
   381             (Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule)
   382             RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
   383       in names ~~ map proj (1 upto n) end;
   384 
   385 fun add_cases_induct no_elim no_ind names elims induct induct_cases =
   386   let
   387     fun cases_spec (name, elim) thy =
   388       thy
   389       |> Theory.add_path (Sign.base_name name)
   390       |> (#1 o PureThy.add_thms [(("cases", elim), [InductMethod.cases_set_global name])])
   391       |> Theory.parent_path;
   392     val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
   393 
   394     fun induct_spec (name, th) = (#1 o PureThy.add_thms
   395       [(("", th), [RuleCases.case_names induct_cases, InductMethod.induct_set_global name])]);
   396     val induct_specs = if no_ind then [] else map induct_spec (project_rules names induct);
   397   in Library.apply (cases_specs @ induct_specs) end;
   398 
   399 
   400 
   401 (*** proofs for (co)inductive sets ***)
   402 
   403 (** prove monotonicity **)
   404 
   405 fun prove_mono setT fp_fun monos thy =
   406   let
   407     val _ = message "  Proving monotonicity ...";
   408 
   409     val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
   410       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
   411         (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)])
   412 
   413   in mono end;
   414 
   415 
   416 
   417 (** prove introduction rules **)
   418 
   419 fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
   420   let
   421     val _ = message "  Proving the introduction rules ...";
   422 
   423     val unfold = standard (mono RS (fp_def RS
   424       (if coind then def_gfp_Tarski else def_lfp_Tarski)));
   425 
   426     fun select_disj 1 1 = []
   427       | select_disj _ 1 = [rtac disjI1]
   428       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
   429 
   430     val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
   431       (cterm_of (Theory.sign_of thy) intr) (fn prems =>
   432        [(*insert prems and underlying sets*)
   433        cut_facts_tac prems 1,
   434        stac unfold 1,
   435        REPEAT (resolve_tac [vimageI2, CollectI] 1),
   436        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
   437        EVERY1 (select_disj (length intr_ts) i),
   438        (*Not ares_tac, since refl must be tried before any equality assumptions;
   439          backtracking may occur if the premises have extra variables!*)
   440        DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
   441        (*Now solve the equations like Inl 0 = Inl ?b2*)
   442        rewrite_goals_tac con_defs,
   443        REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts)
   444 
   445   in (intrs, unfold) end;
   446 
   447 
   448 
   449 (** prove elimination rules **)
   450 
   451 fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy =
   452   let
   453     val _ = message "  Proving the elimination rules ...";
   454 
   455     val rules1 = [CollectE, disjE, make_elim vimageD, exE];
   456     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @
   457       map make_elim [Inl_inject, Inr_inject];
   458   in
   459     map (fn (t, cases) => prove_goalw_cterm rec_sets_defs
   460       (cterm_of (Theory.sign_of thy) t) (fn prems =>
   461         [cut_facts_tac [hd prems] 1,
   462          dtac (unfold RS subst) 1,
   463          REPEAT (FIRSTGOAL (eresolve_tac rules1)),
   464          REPEAT (FIRSTGOAL (eresolve_tac rules2)),
   465          EVERY (map (fn prem =>
   466            DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
   467       |> RuleCases.name cases)
   468       (mk_elims cs cTs params intr_ts intr_names)
   469   end;
   470 
   471 
   472 (** derivation of simplified elimination rules **)
   473 
   474 (*Applies freeness of the given constructors, which *must* be unfolded by
   475   the given defs.  Cannot simply use the local con_defs because con_defs=[] 
   476   for inference systems.
   477  *)
   478 
   479 (*cprop should have the form t:Si where Si is an inductive set*)
   480 fun mk_cases_i solved elims ss cprop =
   481   let
   482     val prem = Thm.assume cprop;
   483     val tac = TRYALL (InductMethod.simp_case_tac solved ss) THEN prune_params_tac;
   484     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
   485   in
   486     (case get_first (try mk_elim) elims of
   487       Some r => r
   488     | None => error (Pretty.string_of (Pretty.block
   489         [Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk,
   490           Display.pretty_cterm cprop])))
   491   end;
   492 
   493 fun mk_cases elims s =
   494   mk_cases_i false elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
   495 
   496 
   497 (* inductive_cases(_i) *)
   498 
   499 fun gen_inductive_cases prep_att prep_const prep_prop
   500     ((((name, raw_atts), raw_set), raw_props), comment) thy =
   501   let val sign = Theory.sign_of thy;
   502   in (case get_inductive thy (prep_const sign raw_set) of
   503       None => error ("Unknown (co)inductive set " ^ quote name)
   504     | Some (_, {elims, ...}) =>
   505         let
   506           val atts = map (prep_att thy) raw_atts;
   507           val cprops = map
   508             (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
   509           val thms = map
   510             (mk_cases_i true elims (Simplifier.simpset_of thy)) cprops;
   511         in
   512           thy |> IsarThy.have_theorems_i
   513             [(((name, atts), map Thm.no_attributes thms), comment)]
   514         end)
   515   end;
   516 
   517 val inductive_cases =
   518   gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
   519 
   520 val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop;
   521 
   522 
   523 
   524 (** prove induction rule **)
   525 
   526 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
   527     fp_def rec_sets_defs thy =
   528   let
   529     val _ = message "  Proving the induction rule ...";
   530 
   531     val sign = Theory.sign_of thy;
   532 
   533     val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
   534         None => []
   535       | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
   536 
   537     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   538 
   539     (* make predicate for instantiation of abstract induction rule *)
   540 
   541     fun mk_ind_pred _ [P] = P
   542       | mk_ind_pred T Ps =
   543          let val n = (length Ps) div 2;
   544              val Type (_, [T1, T2]) = T
   545          in Const ("Datatype.sum.sum_case",
   546            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
   547              mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
   548          end;
   549 
   550     val ind_pred = mk_ind_pred sumT preds;
   551 
   552     val ind_concl = HOLogic.mk_Trueprop
   553       (HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->"
   554         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0)));
   555 
   556     (* simplification rules for vimage and Collect *)
   557 
   558     val vimage_simps = if length cs < 2 then [] else
   559       map (fn c => prove_goalw_cterm [] (cterm_of sign
   560         (HOLogic.mk_Trueprop (HOLogic.mk_eq
   561           (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
   562            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
   563              nth_elem (find_index_eq c cs, preds)))))
   564         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites,
   565           rtac refl 1])) cs;
   566 
   567     val induct = prove_goalw_cterm [] (cterm_of sign
   568       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
   569         [rtac (impI RS allI) 1,
   570          DETERM (etac (mono RS (fp_def RS def_induct)) 1),
   571          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
   572          fold_goals_tac rec_sets_defs,
   573          (*This CollectE and disjE separates out the introduction rules*)
   574          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
   575          (*Now break down the individual cases.  No disjE here in case
   576            some premise involves disjunction.*)
   577          REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
   578          rewrite_goals_tac sum_case_rewrites,
   579          EVERY (map (fn prem =>
   580            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
   581 
   582     val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
   583       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
   584         [cut_facts_tac prems 1,
   585          REPEAT (EVERY
   586            [REPEAT (resolve_tac [conjI, impI] 1),
   587             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
   588             rewrite_goals_tac sum_case_rewrites,
   589             atac 1])])
   590 
   591   in standard (split_rule (induct RS lemma))
   592   end;
   593 
   594 
   595 
   596 (*** specification of (co)inductive sets ****)
   597 
   598 (** definitional introduction of (co)inductive sets **)
   599 
   600 fun mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   601       params paramTs cTs cnames =
   602   let
   603     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
   604     val setT = HOLogic.mk_setT sumT;
   605 
   606     val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
   607       else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";
   608 
   609     val used = foldr add_term_names (intr_ts, []);
   610     val [sname, xname] = variantlist (["S", "x"], used);
   611 
   612     (* transform an introduction rule into a conjunction  *)
   613     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
   614     (* is transformed into                                *)
   615     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
   616 
   617     fun transform_rule r =
   618       let
   619         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
   620         val subst = subst_free
   621           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
   622         val Const ("op :", _) $ t $ u =
   623           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
   624 
   625       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
   626         (frees, foldr1 HOLogic.mk_conj
   627           (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
   628             (map (subst o HOLogic.dest_Trueprop)
   629               (Logic.strip_imp_prems r))))
   630       end
   631 
   632     (* make a disjunction of all introduction rules *)
   633 
   634     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
   635       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
   636 
   637     (* add definiton of recursive sets to theory *)
   638 
   639     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
   640     val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
   641 
   642     val rec_const = list_comb
   643       (Const (full_rec_name, paramTs ---> setT), params);
   644 
   645     val fp_def_term = Logic.mk_equals (rec_const,
   646       Const (fp_name, (setT --> setT) --> setT) $ fp_fun)
   647 
   648     val def_terms = fp_def_term :: (if length cs < 2 then [] else
   649       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
   650 
   651     val (thy', [fp_def :: rec_sets_defs]) =
   652       thy
   653       |> (if declare_consts then
   654           Theory.add_consts_i (map (fn (c, n) =>
   655             (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
   656           else I)
   657       |> (if length cs < 2 then I
   658           else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
   659       |> Theory.add_path rec_name
   660       |> PureThy.add_defss_i false [(("defs", def_terms), [])];
   661 
   662     val mono = prove_mono setT fp_fun monos thy'
   663 
   664   in
   665     (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) 
   666   end;
   667 
   668 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
   669     atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
   670   let
   671     val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
   672       commas_quote cnames) else ();
   673 
   674     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   675 
   676     val (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) =
   677       mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   678         params paramTs cTs cnames;
   679 
   680     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
   681       rec_sets_defs thy';
   682     val elims = if no_elim then [] else
   683       prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy';
   684     val raw_induct = if no_ind then Drule.asm_rl else
   685       if coind then standard (rule_by_tactic
   686         (rewrite_tac [mk_meta_eq vimage_Un] THEN
   687           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
   688       else
   689         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
   690           rec_sets_defs thy';
   691     val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
   692       else standard (raw_induct RSN (2, rev_mp));
   693 
   694     val (thy'', [intrs']) =
   695       thy'
   696       |> PureThy.add_thmss [(("intrs", intrs), atts)]
   697       |>> (#1 o PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts))
   698       |>> (if no_elim then I else #1 o PureThy.add_thmss [(("elims", elims), [])])
   699       |>> (if no_ind then I else #1 o PureThy.add_thms
   700         [((coind_prefix coind ^ "induct", induct), [RuleCases.case_names induct_cases])])
   701       |>> Theory.parent_path;
   702     val elims' = if no_elim then elims else PureThy.get_thms thy'' "elims";  (* FIXME improve *)
   703     val induct' = if no_ind then induct else PureThy.get_thm thy'' (coind_prefix coind ^ "induct");  (* FIXME improve *)
   704   in (thy'',
   705     {defs = fp_def::rec_sets_defs,
   706      mono = mono,
   707      unfold = unfold,
   708      intrs = intrs',
   709      elims = elims',
   710      mk_cases = mk_cases elims',
   711      raw_induct = raw_induct,
   712      induct = induct'})
   713   end;
   714 
   715 
   716 
   717 (** axiomatic introduction of (co)inductive sets **)
   718 
   719 fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
   720     atts intros monos con_defs thy params paramTs cTs cnames induct_cases =
   721   let
   722     val _ = message (coind_prefix coind ^ "inductive set(s) " ^ commas_quote cnames);
   723 
   724     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
   725     val (thy', _, fp_def, rec_sets_defs, _, _) =
   726       mk_ind_def declare_consts alt_name coind cs intr_ts monos con_defs thy
   727         params paramTs cTs cnames;
   728     val (elim_ts, elim_cases) = Library.split_list (mk_elims cs cTs params intr_ts intr_names);
   729     val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
   730     val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
   731     
   732     val thy'' =
   733       thy'
   734       |> (#1 o PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("raw_elims", elim_ts), [])])
   735       |> (if coind then I else
   736             #1 o PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
   737 
   738     val intrs = PureThy.get_thms thy'' "intrs";
   739     val elims = map2 (fn (th, cases) => RuleCases.name cases th)
   740       (PureThy.get_thms thy'' "raw_elims", elim_cases);
   741     val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy'' "raw_induct";
   742     val induct = if coind orelse length cs > 1 then raw_induct
   743       else standard (raw_induct RSN (2, rev_mp));
   744 
   745     val (thy''', ([elims'], intrs')) =
   746       thy''
   747       |> PureThy.add_thmss [(("elims", elims), [])]
   748       |>> (if coind then I
   749           else #1 o PureThy.add_thms [(("induct", induct), [RuleCases.case_names induct_cases])])
   750       |>>> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
   751       |>> Theory.parent_path;
   752     val induct' = if coind then raw_induct else PureThy.get_thm thy''' "induct";
   753   in (thy''',
   754     {defs = fp_def :: rec_sets_defs,
   755      mono = Drule.asm_rl,
   756      unfold = Drule.asm_rl,
   757      intrs = intrs',
   758      elims = elims',
   759      mk_cases = mk_cases elims',
   760      raw_induct = raw_induct,
   761      induct = induct'})
   762   end;
   763 
   764 
   765 
   766 (** introduction of (co)inductive sets **)
   767 
   768 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
   769     atts intros monos con_defs thy =
   770   let
   771     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
   772     val sign = Theory.sign_of thy;
   773 
   774     (*parameters should agree for all mutually recursive components*)
   775     val (_, params) = strip_comb (hd cs);
   776     val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\
   777       \ component is not a free variable: " sign) params;
   778 
   779     val cTs = map (try' (HOLogic.dest_setT o fastype_of)
   780       "Recursive component not of type set: " sign) cs;
   781 
   782     val full_cnames = map (try' (fst o dest_Const o head_of)
   783       "Recursive set not previously declared as constant: " sign) cs;
   784     val cnames = map Sign.base_name full_cnames;
   785 
   786     val _ = seq (check_rule sign cs o snd o fst) intros;
   787     val induct_cases = map (#1 o #1) intros;
   788 
   789     val (thy1, result as {elims, induct, ...}) =
   790       (if ! quick_and_dirty then add_ind_axm else add_ind_def)
   791         verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
   792         con_defs thy params paramTs cTs cnames induct_cases;
   793     val thy2 = thy1
   794       |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
   795       |> add_cases_induct no_elim (no_ind orelse coind) full_cnames elims induct induct_cases;
   796   in (thy2, result) end;
   797 
   798 
   799 
   800 (** external interface **)
   801 
   802 fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
   803   let
   804     val sign = Theory.sign_of thy;
   805     val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
   806 
   807     val atts = map (Attrib.global_attribute thy) srcs;
   808     val intr_names = map (fst o fst) intro_srcs;
   809     fun read_rule s = Thm.read_cterm sign (s, propT)
   810       handle ERROR => error ("The error(s) above occurred for " ^ s);
   811     val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
   812     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
   813     val (cs', intr_ts') = unify_consts sign cs intr_ts;
   814 
   815     val ((thy', con_defs), monos) = thy
   816       |> IsarThy.apply_theorems raw_monos
   817       |> apfst (IsarThy.apply_theorems raw_con_defs);
   818   in
   819     add_inductive_i verbose false "" coind false false cs'
   820       atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
   821   end;
   822 
   823 
   824 
   825 (** package setup **)
   826 
   827 (* setup theory *)
   828 
   829 val setup =
   830  [InductiveData.init,
   831   Attrib.add_attributes [("mono", mono_attr, "monotonicity rule")]];
   832 
   833 
   834 (* outer syntax *)
   835 
   836 local structure P = OuterParse and K = OuterSyntax.Keyword in
   837 
   838 fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
   839   #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
   840 
   841 fun ind_decl coind =
   842   (Scan.repeat1 P.term --| P.marg_comment) --
   843   (P.$$$ "intrs" |--
   844     P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
   845   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
   846   Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
   847   >> (Toplevel.theory o mk_ind coind);
   848 
   849 val inductiveP =
   850   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
   851 
   852 val coinductiveP =
   853   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
   854 
   855 
   856 val ind_cases =
   857   P.opt_thm_name "=" -- P.xname --| P.$$$ ":" -- Scan.repeat1 P.prop -- P.marg_comment
   858   >> (Toplevel.theory o inductive_cases);
   859 
   860 val inductive_casesP =
   861   OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules"
   862     K.thy_decl ind_cases;
   863 
   864 val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"];
   865 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
   866 
   867 end;
   868 
   869 
   870 end;