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
8 (Co)Inductive Definition module for HOL.
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
17 The recursive sets must *already* be declared as constants in the
18 current theory!
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
27 Sums are used only for mutual recursion.  Products are used only to
28 derive "streamlined" induction rules for relations.
29 *)
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;
56 structure InductivePackage: INDUCTIVE_PACKAGE =
57 struct
60 (** utilities **)
62 (* messages *)
64 val quiet_mode = ref false;
65 fun message s = if !quiet_mode then () else writeln s;
67 fun coind_prefix true = "co"
68   | coind_prefix false = "";
71 (* the following code ensures that each recursive set *)
72 (* always has the same type in all introduction rules *)
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))
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));
102 (* misc *)
104 (*for proving monotonicity of recursion operator*)
105 val default_monos = basic_monos @ [vimage_mono];
107 val Const _ \$ (vimage_f \$ _) \$ _ = HOLogic.dest_Trueprop (concl_of vimageD);
109 (*Delete needless equality assumptions*)
110 val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
111      (fn _ => [assume_tac 1]);
113 (*For simplifying the elimination rule*)
114 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
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";
119 (* make injections needed in mutually recursive definitions *)
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;
136 (* make "vimage" terms for selecting out components of mutually rec.def. *)
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;
149 (** well-formedness checks **)
151 fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^
152   (Sign.string_of_term sign t) ^ "\n" ^ msg);
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);
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";
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 ()
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;
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));
188 (*** theory data ***)
190 (* data kind 'HOL/inductive' *)
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};
196 structure InductiveArgs =
197 struct
198   val name = "HOL/inductive";
199   type T = inductive_info Symtab.table;
201   val empty = Symtab.empty;
202   val copy = I;
203   val prep_ext = I;
204   val merge: T * T -> T = Symtab.merge (K true);
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;
211 structure InductiveData = TheoryDataFun(InductiveArgs);
212 val print_inductives = InductiveData.print;
215 (* get and put data *)
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));
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;
231 (*** properties of (co)inductive sets ***)
233 (** elimination rules **)
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));
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;
246     val intrs = map dest_intr intr_ts;
248     fun mk_elim (c, T) =
249       let
250         val a = Free (aname, T);
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;
265 (** premises and conclusions of induction rules **)
267 fun mk_indrule cs cTs params intr_ts =
268   let
269     val used = foldr add_term_names (intr_ts, []);
271     (* predicates for induction rule *)
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);
277     (* transform an introduction rule into a premise for induction rule *)
279     fun mk_ind_prem r =
280       let
281         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
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;
292         val Const ("op :", _) \$ t \$ u =
293           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
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;
301     val ind_prems = map mk_ind_prem intr_ts;
303     (* make conclusions for induction rules *)
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;
315     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 (app HOLogic.conj)
316         (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
318   in (preds, ind_prems, mutual_ind_concl)
319   end;
323 (*** proofs for (co)inductive sets ***)
325 (** prove monotonicity **)
327 fun prove_mono setT fp_fun monos thy =
328   let
329     val _ = message "  Proving monotonicity ...";
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)])
335   in mono end;
339 (** prove introduction rules **)
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 ...";
345     val unfold = standard (mono RS (fp_def RS
346       (if coind then def_gfp_Tarski else def_lfp_Tarski)));
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));
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)
367   in (intrs, unfold) end;
371 (** prove elimination rules **)
373 fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =
374   let
375     val _ = message "  Proving the elimination rules ...";
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];
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)
391   in elims end;
394 (** derivation of simplified elimination rules **)
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;
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;
422 fun mk_cases elims s =
423   mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
426 (* inductive_cases(_i) *)
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;
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;
442 val inductive_cases =
443   gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
445 val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop;
449 (** prove induction rule **)
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 ...";
456     val sign = Theory.sign_of thy;
458     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
460     (* make predicate for instantiation of abstract induction rule *)
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;
471     val ind_pred = mk_ind_pred sumT preds;
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)));
477     (* simplification rules for vimage and Collect *)
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;
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)]);
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])])
514   in standard (split_rule (induct RS lemma))
515   end;
519 (*** specification of (co)inductive sets ****)
521 (** definitional introduction of (co)inductive sets **)
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 ();
529     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
530     val setT = HOLogic.mk_setT sumT;
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";
535     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
537     val used = foldr add_term_names (intr_ts, []);
538     val [sname, xname] = variantlist (["S", "x"], used);
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 ... & ...      *)
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)
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
560     (* make a disjunction of all introduction rules *)
562     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) \$
563       absfree (xname, sumT, foldr1 (app HOLogic.disj) (map transform_rule intr_ts)));
565     (* add definiton of recursive sets to theory *)
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;
570     val rec_const = list_comb
571       (Const (full_rec_name, paramTs ---> setT), params);
573     val fp_def_term = Logic.mk_equals (rec_const,
574       Const (fp_name, (setT --> setT) --> setT) \$ fp_fun)
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);
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), [])];
589     (* get definitions from theory *)
591     val fp_def::rec_sets_defs = PureThy.get_thms thy' "defs";
593     (* prove and store theorems *)
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));
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;
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;
631 (** axiomatic introduction of (co)inductive sets **)
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 ();
639     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
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;
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);
647     val thy' = thy
648       |> (if declare_consts then
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), [])]);
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));
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;
681 (** introduction of (co)inductive sets **)
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;
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;
694     val cTs = map (try' (HOLogic.dest_setT o fastype_of)
695       "Recursive component not of type set: " sign) cs;
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;
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;
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;
714 (** external interface **)
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;
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;
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;
737 (** package setup **)
739 (* setup theory *)
741 val setup = [InductiveData.init];
744 (* outer syntax *)
746 local structure P = OuterParse and K = OuterSyntax.Keyword in
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;
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);
759 val inductiveP =
760   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
762 val coinductiveP =
763   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
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);
770 val inductive_casesP =
771   OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules"
772     K.thy_decl ind_cases;
774 val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"];
775 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
777 end;
780 end;