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