src/HOL/Tools/inductive_package.ML
 author wenzelm Fri Mar 03 21:01:57 2000 +0100 (2000-03-03) changeset 8336 fdf3ac335f77 parent 8316 74639e19eca0 child 8375 0544749a5e8f permissions -rw-r--r--
mk_cases / inductive_cases: use InductMethod.con_elim_(solved_)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 ->
36     {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
37       induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
38   val print_inductives: theory -> unit
39   val mono_add_global: theory attribute
40   val mono_del_global: theory attribute
41   val get_monos: theory -> thm list
42   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
43     theory attribute list -> ((bstring * term) * theory attribute list) list ->
44       thm list -> thm list -> theory -> theory *
45       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
46        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
47   val add_inductive: bool -> bool -> string list -> Args.src list ->
48     ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
49       (xstring * Args.src list) list -> theory -> theory *
50       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
51        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
52   val inductive_cases: (((bstring * Args.src list) * xstring) * string list) * Comment.text
53     -> theory -> theory
54   val inductive_cases_i: (((bstring * theory attribute list) * string) * term list) * Comment.text
55     -> theory -> theory
56   val setup: (theory -> theory) list
57 end;
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.writeln (Pretty.strs ("(co)inductives:" ::
83        map #1 (Sign.cond_extern_table sg Sign.constK tab)));
84      Pretty.writeln (Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)));
85 end;
87 structure InductiveData = TheoryDataFun(InductiveArgs);
88 val print_inductives = InductiveData.print;
91 (* get and put data *)
93 fun get_inductive thy name =
94   (case Symtab.lookup (fst (InductiveData.get thy), name) of
95     Some info => info
96   | None => error ("Unknown (co)inductive set " ^ quote name));
98 fun put_inductives names info thy =
99   let
100     fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
101     val tab_monos = foldl upd (InductiveData.get thy, names)
102       handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
103   in InductiveData.put tab_monos thy end;
107 (** monotonicity rules **)
109 val get_monos = snd o InductiveData.get;
110 fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy;
112 fun mk_mono thm =
113   let
114     fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @
115       (case concl_of thm of
116           (_ \$ (_ \$ (Const ("Not", _) \$ _) \$ _)) => []
117         | _ => [standard (thm' RS (thm' RS eq_to_mono2))]);
118     val concl = concl_of thm
119   in
120     if Logic.is_equals concl then
121       eq2mono (thm RS meta_eq_to_obj_eq)
122     else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
123       eq2mono thm
124     else [thm]
125   end;
127 (* mono add/del *)
129 local
131 fun map_rules_global f thy = put_monos (f (get_monos thy)) thy;
133 fun add_mono thm rules = Library.gen_union Thm.eq_thm (mk_mono thm, rules);
134 fun del_mono thm rules = Library.gen_rems Thm.eq_thm (rules, mk_mono thm);
136 fun mk_att f g (x, thm) = (f (g thm) x, thm);
138 in
140 val mono_add_global = mk_att map_rules_global add_mono;
141 val mono_del_global = mk_att map_rules_global del_mono;
143 end;
146 (* concrete syntax *)
148 val monoN = "mono";
150 val delN = "del";
152 fun mono_att add del =
153   Attrib.syntax (Scan.lift (Args.\$\$\$ addN >> K add || Args.\$\$\$ delN >> K del || Scan.succeed add));
155 val mono_attr =
156   (mono_att mono_add_global mono_del_global, mono_att Attrib.undef_local_attribute Attrib.undef_local_attribute);
160 (** utilities **)
162 (* messages *)
164 val quiet_mode = ref false;
165 fun message s = if !quiet_mode then () else writeln s;
167 fun coind_prefix true = "co"
168   | coind_prefix false = "";
171 (* the following code ensures that each recursive set *)
172 (* always has the same type in all introduction rules *)
174 fun unify_consts sign cs intr_ts =
175   (let
176     val {tsig, ...} = Sign.rep_sg sign;
177     val add_term_consts_2 =
178       foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
179     fun varify (t, (i, ts)) =
180       let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
181       in (maxidx_of_term t', t'::ts) end;
182     val (i, cs') = foldr varify (cs, (~1, []));
183     val (i', intr_ts') = foldr varify (intr_ts, (i, []));
184     val rec_consts = foldl add_term_consts_2 ([], cs');
185     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
186     fun unify (env, (cname, cT)) =
187       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
188       in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
189           (env, (replicate (length consts) cT) ~~ consts)
190       end;
191     val (env, _) = foldl unify (([], i'), rec_consts);
192     fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T
193       in if T = T' then T else typ_subst_TVars_2 env T' end;
194     val subst = fst o Type.freeze_thaw o
195       (map_term_types (typ_subst_TVars_2 env))
197   in (map subst cs', map subst intr_ts')
198   end) handle Type.TUNIFY =>
199     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
202 (* misc *)
204 val Const _ \$ (vimage_f \$ _) \$ _ = HOLogic.dest_Trueprop (concl_of vimageD);
206 val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``";
207 val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
209 (* make injections needed in mutually recursive definitions *)
211 fun mk_inj cs sumT c x =
212   let
213     fun mk_inj' T n i =
214       if n = 1 then x else
215       let val n2 = n div 2;
216           val Type (_, [T1, T2]) = T
217       in
218         if i <= n2 then
219           Const ("Inl", T1 --> T) \$ (mk_inj' T1 n2 i)
220         else
221           Const ("Inr", T2 --> T) \$ (mk_inj' T2 (n - n2) (i - n2))
222       end
223   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
224   end;
226 (* make "vimage" terms for selecting out components of mutually rec.def. *)
228 fun mk_vimage cs sumT t c = if length cs < 2 then t else
229   let
230     val cT = HOLogic.dest_setT (fastype_of c);
231     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
232   in
233     Const (vimage_name, vimageT) \$
234       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) \$ t
235   end;
239 (** well-formedness checks **)
241 fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^
242   (Sign.string_of_term sign t) ^ "\n" ^ msg);
244 fun err_in_prem sign t p msg = error ("Ill-formed premise\n" ^
245   (Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^
246   (Sign.string_of_term sign t) ^ "\n" ^ msg);
248 val msg1 = "Conclusion of introduction rule must have form\
249           \ ' t : S_i '";
250 val msg2 = "Non-atomic premise";
251 val msg3 = "Recursion term on left of member symbol";
253 fun check_rule sign cs r =
254   let
255     fun check_prem prem = if can HOLogic.dest_Trueprop prem then ()
256       else err_in_prem sign r prem msg2;
258   in (case HOLogic.dest_Trueprop (Logic.strip_imp_concl r) of
259         (Const ("op :", _) \$ t \$ u) =>
260           if u mem cs then
261             if exists (Logic.occs o (rpair t)) cs then
262               err_in_rule sign r msg3
263             else
264               seq check_prem (Logic.strip_imp_prems r)
265           else err_in_rule sign r msg1
266       | _ => err_in_rule sign r msg1)
267   end;
269 fun try' f msg sign t = (case (try f t) of
270       Some x => x
271     | None => error (msg ^ Sign.string_of_term sign t));
275 (*** properties of (co)inductive sets ***)
277 (** elimination rules **)
279 fun mk_elims cs cTs params intr_ts =
280   let
281     val used = foldr add_term_names (intr_ts, []);
282     val [aname, pname] = variantlist (["a", "P"], used);
283     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
285     fun dest_intr r =
286       let val Const ("op :", _) \$ t \$ u =
287         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
288       in (u, t, Logic.strip_imp_prems r) end;
290     val intrs = map dest_intr intr_ts;
292     fun mk_elim (c, T) =
293       let
294         val a = Free (aname, T);
296         fun mk_elim_prem (_, t, ts) =
297           list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
298             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
299       in
300         Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
301           map mk_elim_prem (filter (equal c o #1) intrs), P)
302       end
303   in
304     map mk_elim (cs ~~ cTs)
305   end;
309 (** premises and conclusions of induction rules **)
311 fun mk_indrule cs cTs params intr_ts =
312   let
313     val used = foldr add_term_names (intr_ts, []);
315     (* predicates for induction rule *)
317     val preds = map Free (variantlist (if length cs < 2 then ["P"] else
318       map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
319         map (fn T => T --> HOLogic.boolT) cTs);
321     (* transform an introduction rule into a premise for induction rule *)
323     fun mk_ind_prem r =
324       let
325         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
327         val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
329         fun subst (s as ((m as Const ("op :", T)) \$ t \$ u)) =
330               (case pred_of u of
331                   None => (m \$ fst (subst t) \$ fst (subst u), None)
332                 | Some P => (HOLogic.conj \$ s \$ (P \$ t), Some (s, P \$ t)))
333           | subst s =
334               (case pred_of s of
335                   Some P => (HOLogic.mk_binop "op Int"
336                     (s, HOLogic.Collect_const (HOLogic.dest_setT
337                       (fastype_of s)) \$ P), None)
338                 | None => (case s of
339                      (t \$ u) => (fst (subst t) \$ fst (subst u), None)
340                    | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None)
341                    | _ => (s, None)));
343         fun mk_prem (s, prems) = (case subst s of
344               (_, Some (t, u)) => t :: u :: prems
345             | (t, _) => t :: prems);
347         val Const ("op :", _) \$ t \$ u =
348           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
350       in list_all_free (frees,
351            Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
352              (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
353                HOLogic.mk_Trueprop (the (pred_of u) \$ t)))
354       end;
356     val ind_prems = map mk_ind_prem intr_ts;
358     (* make conclusions for induction rules *)
360     fun mk_ind_concl ((c, P), (ts, x)) =
361       let val T = HOLogic.dest_setT (fastype_of c);
362           val Ts = HOLogic.prodT_factors T;
363           val (frees, x') = foldr (fn (T', (fs, s)) =>
364             ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
365           val tuple = HOLogic.mk_tuple T frees;
366       in ((HOLogic.mk_binop "op -->"
367         (HOLogic.mk_mem (tuple, c), P \$ tuple))::ts, x')
368       end;
370     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
371         (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
373   in (preds, ind_prems, mutual_ind_concl)
374   end;
378 (** prepare cases and induct rules **)
380 (*
381   transform mutual rule:
382     HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
383   into i-th projection:
384     xi:Ai ==> HH ==> Pi xi
385 *)
387 fun project_rules [name] rule = [(name, rule)]
388   | project_rules names mutual_rule =
389       let
390         val n = length names;
391         fun proj i =
392           (if i < n then (fn th => th RS conjunct1) else I)
393             (Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule)
394             RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
395       in names ~~ map proj (1 upto n) end;
397 fun add_cases_induct no_elim no_ind names elims induct =
398   let
399     val cases_specs =
400       if no_elim then []
401       else map2 (fn (name, elim) => (("", elim), [InductMethod.cases_set_global name]))
402         (names, elims);
404     val induct_specs =
405       if no_ind then []
406       else map (fn (name, th) => (("", th), [InductMethod.induct_set_global name]))
407         (project_rules names induct);
408   in PureThy.add_thms (cases_specs @ induct_specs) end;
412 (*** proofs for (co)inductive sets ***)
414 (** prove monotonicity **)
416 fun prove_mono setT fp_fun monos thy =
417   let
418     val _ = message "  Proving monotonicity ...";
420     val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
421       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) \$ fp_fun)))
422         (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)])
424   in mono end;
428 (** prove introduction rules **)
430 fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
431   let
432     val _ = message "  Proving the introduction rules ...";
434     val unfold = standard (mono RS (fp_def RS
435       (if coind then def_gfp_Tarski else def_lfp_Tarski)));
437     fun select_disj 1 1 = []
438       | select_disj _ 1 = [rtac disjI1]
439       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
441     val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
442       (cterm_of (Theory.sign_of thy) intr) (fn prems =>
443        [(*insert prems and underlying sets*)
444        cut_facts_tac prems 1,
445        stac unfold 1,
446        REPEAT (resolve_tac [vimageI2, CollectI] 1),
447        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
448        EVERY1 (select_disj (length intr_ts) i),
449        (*Not ares_tac, since refl must be tried before any equality assumptions;
450          backtracking may occur if the premises have extra variables!*)
451        DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
452        (*Now solve the equations like Inl 0 = Inl ?b2*)
453        rewrite_goals_tac con_defs,
454        REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts)
456   in (intrs, unfold) end;
460 (** prove elimination rules **)
462 fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =
463   let
464     val _ = message "  Proving the elimination rules ...";
466     val rules1 = [CollectE, disjE, make_elim vimageD, exE];
467     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @
468       map make_elim [Inl_inject, Inr_inject];
470     val elims = map (fn t => prove_goalw_cterm rec_sets_defs
471       (cterm_of (Theory.sign_of thy) t) (fn prems =>
472         [cut_facts_tac [hd prems] 1,
473          dtac (unfold RS subst) 1,
474          REPEAT (FIRSTGOAL (eresolve_tac rules1)),
475          REPEAT (FIRSTGOAL (eresolve_tac rules2)),
476          EVERY (map (fn prem =>
477            DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]))
478       (mk_elims cs cTs params intr_ts)
480   in elims end;
483 (** derivation of simplified elimination rules **)
485 (*Applies freeness of the given constructors, which *must* be unfolded by
486   the given defs.  Cannot simply use the local con_defs because con_defs=[]
487   for inference systems.
488  *)
490 (*cprop should have the form t:Si where Si is an inductive set*)
491 fun mk_cases_i solved elims ss cprop =
492   let
493     val prem = Thm.assume cprop;
494     val tac = if solved then InductMethod.con_elim_solved_tac else InductMethod.con_elim_tac;
495     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic (tac ss) (prem RS rl));
496   in
497     (case get_first (try mk_elim) elims of
498       Some r => r
499     | None => error (Pretty.string_of (Pretty.block
500         [Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk,
501           Display.pretty_cterm cprop])))
502   end;
504 fun mk_cases elims s =
505   mk_cases_i false elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
508 (* inductive_cases(_i) *)
510 fun gen_inductive_cases prep_att prep_const prep_prop
511     ((((name, raw_atts), raw_set), raw_props), comment) thy =
512   let
513     val sign = Theory.sign_of thy;
515     val atts = map (prep_att thy) raw_atts;
516     val (_, {elims, ...}) = get_inductive thy (prep_const sign raw_set);
517     val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
518     val thms = map (mk_cases_i true elims (Simplifier.simpset_of thy)) cprops;
519   in
520     thy
521     |> IsarThy.have_theorems_i (((name, atts), map Thm.no_attributes thms), comment)
522   end;
524 val inductive_cases =
525   gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
527 val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop;
531 (** prove induction rule **)
533 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
534     fp_def rec_sets_defs thy =
535   let
536     val _ = message "  Proving the induction rule ...";
538     val sign = Theory.sign_of thy;
540     val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
541         None => []
542       | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
544     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
546     (* make predicate for instantiation of abstract induction rule *)
548     fun mk_ind_pred _ [P] = P
549       | mk_ind_pred T Ps =
550          let val n = (length Ps) div 2;
551              val Type (_, [T1, T2]) = T
552          in Const ("Datatype.sum.sum_case",
553            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) \$
554              mk_ind_pred T1 (take (n, Ps)) \$ mk_ind_pred T2 (drop (n, Ps))
555          end;
557     val ind_pred = mk_ind_pred sumT preds;
559     val ind_concl = HOLogic.mk_Trueprop
560       (HOLogic.all_const sumT \$ Abs ("x", sumT, HOLogic.mk_binop "op -->"
561         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred \$ Bound 0)));
563     (* simplification rules for vimage and Collect *)
565     val vimage_simps = if length cs < 2 then [] else
566       map (fn c => prove_goalw_cterm [] (cterm_of sign
567         (HOLogic.mk_Trueprop (HOLogic.mk_eq
568           (mk_vimage cs sumT (HOLogic.Collect_const sumT \$ ind_pred) c,
569            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) \$
570              nth_elem (find_index_eq c cs, preds)))))
571         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites,
572           rtac refl 1])) cs;
574     val induct = prove_goalw_cterm [] (cterm_of sign
575       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
576         [rtac (impI RS allI) 1,
577          DETERM (etac (mono RS (fp_def RS def_induct)) 1),
578          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
579          fold_goals_tac rec_sets_defs,
580          (*This CollectE and disjE separates out the introduction rules*)
581          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
582          (*Now break down the individual cases.  No disjE here in case
583            some premise involves disjunction.*)
584          REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
585          rewrite_goals_tac sum_case_rewrites,
586          EVERY (map (fn prem =>
587            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
589     val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
590       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
591         [cut_facts_tac prems 1,
592          REPEAT (EVERY
593            [REPEAT (resolve_tac [conjI, impI] 1),
594             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
595             rewrite_goals_tac sum_case_rewrites,
596             atac 1])])
598   in standard (split_rule (induct RS lemma))
599   end;
603 (*** specification of (co)inductive sets ****)
605 (** definitional introduction of (co)inductive sets **)
607 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
608     atts intros monos con_defs thy params paramTs cTs cnames =
609   let
610     val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
611       commas_quote cnames) else ();
613     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
614     val setT = HOLogic.mk_setT sumT;
616     val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
617       else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";
619     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
621     val used = foldr add_term_names (intr_ts, []);
622     val [sname, xname] = variantlist (["S", "x"], used);
624     (* transform an introduction rule into a conjunction  *)
625     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
626     (* is transformed into                                *)
627     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
629     fun transform_rule r =
630       let
631         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
632         val subst = subst_free
633           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
634         val Const ("op :", _) \$ t \$ u =
635           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
637       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
638         (frees, foldr1 HOLogic.mk_conj
639           (((HOLogic.eq_const sumT) \$ Free (xname, sumT) \$ (mk_inj cs sumT u t))::
640             (map (subst o HOLogic.dest_Trueprop)
641               (Logic.strip_imp_prems r))))
642       end
644     (* make a disjunction of all introduction rules *)
646     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) \$
647       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
649     (* add definiton of recursive sets to theory *)
651     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
652     val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
654     val rec_const = list_comb
655       (Const (full_rec_name, paramTs ---> setT), params);
657     val fp_def_term = Logic.mk_equals (rec_const,
658       Const (fp_name, (setT --> setT) --> setT) \$ fp_fun)
660     val def_terms = fp_def_term :: (if length cs < 2 then [] else
661       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
663     val thy' = thy |>
664       (if declare_consts then
665         Theory.add_consts_i (map (fn (c, n) =>
666           (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
667        else I) |>
668       (if length cs < 2 then I else
669        Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)]) |>
670       Theory.add_path rec_name |>
671       PureThy.add_defss_i [(("defs", def_terms), [])];
673     (* get definitions from theory *)
675     val fp_def::rec_sets_defs = PureThy.get_thms thy' "defs";
677     (* prove and store theorems *)
679     val mono = prove_mono setT fp_fun monos thy';
680     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
681       rec_sets_defs thy';
682     val elims = if no_elim then [] else
683       prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';
684     val raw_induct = if no_ind then Drule.asm_rl else
685       if coind then standard (rule_by_tactic
686         (rewrite_tac [mk_meta_eq vimage_Un] THEN
687           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
688       else
689         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
690           rec_sets_defs thy';
691     val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
692       else standard (raw_induct RSN (2, rev_mp));
694     val thy'' = thy'
695       |> PureThy.add_thmss [(("intrs", intrs), atts)]
696       |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
697       |> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])])
698       |> (if no_ind then I else PureThy.add_thms
699         [((coind_prefix coind ^ "induct", induct), [])])
700       |> Theory.parent_path;
701     val intrs' = PureThy.get_thms thy'' "intrs";
702     val elims' = if no_elim then elims else PureThy.get_thms thy'' "elims";  (* FIXME improve *)
703     val induct' = if no_ind then induct else PureThy.get_thm thy'' (coind_prefix coind ^ "induct");  (* FIXME improve *)
704   in (thy'',
705     {defs = fp_def::rec_sets_defs,
706      mono = mono,
707      unfold = unfold,
708      intrs = intrs',
709      elims = elims',
710      mk_cases = mk_cases elims',
711      raw_induct = raw_induct,
712      induct = induct'})
713   end;
717 (** axiomatic introduction of (co)inductive sets **)
719 fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
720     atts intros monos con_defs thy params paramTs cTs cnames =
721   let
722     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
724     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
725     val elim_ts = mk_elims cs cTs params intr_ts;
727     val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
728     val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
730     val thy' = thy
731       |> (if declare_consts then
733               (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
734          else I)
735       |> Theory.add_path rec_name
736       |> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("elims", elim_ts), [])]
737       |> (if coind then I else
738             PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
740     val intrs = PureThy.get_thms thy' "intrs";
741     val elims = PureThy.get_thms thy' "elims";
742     val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy' "raw_induct";
743     val induct = if coind orelse length cs > 1 then raw_induct
744       else standard (raw_induct RSN (2, rev_mp));
746     val thy'' =
747       thy'
748       |> (if coind then I else PureThy.add_thms [(("induct", induct), [])])
749       |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
750       |> Theory.parent_path;
751     val induct' = if coind then raw_induct else PureThy.get_thm thy'' "induct";
752   in (thy'',
753     {defs = [],
754      mono = Drule.asm_rl,
755      unfold = Drule.asm_rl,
756      intrs = intrs,
757      elims = elims,
758      mk_cases = mk_cases elims,
759      raw_induct = raw_induct,
760      induct = induct'})
761   end;
765 (** introduction of (co)inductive sets **)
767 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
768     atts intros monos con_defs thy =
769   let
770     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
771     val sign = Theory.sign_of thy;
773     (*parameters should agree for all mutually recursive components*)
774     val (_, params) = strip_comb (hd cs);
775     val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\
776       \ component is not a free variable: " sign) params;
778     val cTs = map (try' (HOLogic.dest_setT o fastype_of)
779       "Recursive component not of type set: " sign) cs;
781     val full_cnames = map (try' (fst o dest_Const o head_of)
782       "Recursive set not previously declared as constant: " sign) cs;
783     val cnames = map Sign.base_name full_cnames;
785     val _ = seq (check_rule sign cs o snd o fst) intros;
787     val (thy1, result) =
788       (if ! quick_and_dirty then add_ind_axm else add_ind_def)
789         verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
790         con_defs thy params paramTs cTs cnames;
791     val thy2 = thy1
792       |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
793       |> add_cases_induct no_elim no_ind full_cnames (#elims result) (#induct result);
794   in (thy2, result) end;
798 (** external interface **)
800 fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
801   let
802     val sign = Theory.sign_of thy;
803     val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
805     val atts = map (Attrib.global_attribute thy) srcs;
806     val intr_names = map (fst o fst) intro_srcs;
807     val intr_ts = map (term_of o Thm.read_cterm sign o rpair propT o snd o fst) intro_srcs;
808     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
809     val (cs', intr_ts') = unify_consts sign cs intr_ts;
811     val ((thy', con_defs), monos) = thy
812       |> IsarThy.apply_theorems raw_monos
813       |> apfst (IsarThy.apply_theorems raw_con_defs);
814   in
815     add_inductive_i verbose false "" coind false false cs'
816       atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
817   end;
821 (** package setup **)
823 (* setup theory *)
825 val setup = [InductiveData.init,
826              Attrib.add_attributes [(monoN, 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;