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