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