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