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