src/HOL/Tools/inductive_package.ML
 author wenzelm Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago) changeset 18708 4b3dadb4fe33 parent 18678 dd0c569fa43d child 18728 6790126ab5f6 permissions -rw-r--r--
setup: theory -> theory;
1 (*  Title:      HOL/Tools/inductive_package.ML
2     ID:         \$Id\$
3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4     Author:     Stefan Berghofer, TU Muenchen
5     Author:     Markus Wenzel, TU Muenchen
7 (Co)Inductive Definition module for HOL.
9 Features:
10   * least or greatest fixedpoints
11   * user-specified product and sum constructions
12   * mutually recursive definitions
13   * definitions involving arbitrary monotone operators
14   * automatically proves introduction and elimination rules
16 The recursive sets must *already* be declared as constants in the
17 current theory!
19   Introduction rules have the form
20   [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk
21   where M is some monotone operator (usually the identity)
22   P(x) is any side condition on the free variables
23   ti, t are any terms
24   Sj, Sk are two of the sets being defined in mutual recursion
26 Sums are used only for mutual recursion.  Products are used only to
27 derive "streamlined" induction rules for relations.
28 *)
30 signature INDUCTIVE_PACKAGE =
31 sig
32   val quiet_mode: bool ref
33   val trace: bool ref
34   val unify_consts: theory -> term list -> term list -> term list * term list
35   val split_rule_vars: term list -> thm -> thm
36   val get_inductive: theory -> string -> ({names: string list, coind: bool} *
37     {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
38      intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}) option
39   val the_mk_cases: theory -> string -> string -> thm
40   val print_inductives: theory -> unit
41   val mono_add_global: theory attribute
42   val mono_del_global: theory attribute
43   val get_monos: theory -> thm list
44   val inductive_forall_name: string
45   val inductive_forall_def: thm
46   val rulify: thm -> thm
47   val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
48   val inductive_cases_i: ((bstring * theory attribute list) * term list) list -> theory -> theory
49   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
50     ((bstring * term) * theory attribute list) list -> thm list -> theory -> theory *
51       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
52        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
53   val add_inductive: bool -> bool -> string list ->
54     ((bstring * string) * Attrib.src list) list -> (thmref * Attrib.src list) list ->
55     theory -> theory *
56       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
57        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
58   val setup: theory -> theory
59 end;
61 structure InductivePackage: INDUCTIVE_PACKAGE =
62 struct
65 (** theory context references **)
67 val mono_name = "Orderings.mono";
68 val gfp_name = "FixedPoint.gfp";
69 val lfp_name = "FixedPoint.lfp";
70 val vimage_name = "Set.vimage";
71 val Const _ \$ (vimage_f \$ _) \$ _ = HOLogic.dest_Trueprop (Thm.concl_of vimageD);
73 val inductive_forall_name = "HOL.induct_forall";
74 val inductive_forall_def = thm "induct_forall_def";
75 val inductive_conj_name = "HOL.induct_conj";
76 val inductive_conj_def = thm "induct_conj_def";
77 val inductive_conj = thms "induct_conj";
78 val inductive_atomize = thms "induct_atomize";
79 val inductive_rulify = thms "induct_rulify";
80 val inductive_rulify_fallback = thms "induct_rulify_fallback";
84 (** theory data **)
86 type inductive_info =
87   {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
88     induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
90 structure InductiveData = TheoryDataFun
91 (struct
92   val name = "HOL/inductive";
93   type T = inductive_info Symtab.table * thm list;
95   val empty = (Symtab.empty, []);
96   val copy = I;
97   val extend = I;
98   fun merge _ ((tab1, monos1), (tab2, monos2)) =
99     (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
101   fun print thy (tab, monos) =
102     [Pretty.strs ("(co)inductives:" ::
103       map #1 (NameSpace.extern_table (Sign.const_space thy, tab))),
104      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg thy) monos)]
105     |> Pretty.chunks |> Pretty.writeln;
106 end);
108 val print_inductives = InductiveData.print;
111 (* get and put data *)
113 val get_inductive = Symtab.lookup o #1 o InductiveData.get;
115 fun the_inductive thy name =
116   (case get_inductive thy name of
117     NONE => error ("Unknown (co)inductive set " ^ quote name)
118   | SOME info => info);
120 val the_mk_cases = (#mk_cases o #2) oo the_inductive;
122 fun put_inductives names info = InductiveData.map (apfst (fn tab =>
123   fold (fn name => Symtab.update_new (name, info)) names tab
124     handle Symtab.DUP dup => error ("Duplicate definition of (co)inductive set " ^ quote dup)));
128 (** monotonicity rules **)
130 val get_monos = #2 o InductiveData.get;
131 fun map_monos f = InductiveData.map (Library.apsnd f);
133 fun mk_mono thm =
134   let
135     fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @
136       (case concl_of thm of
137           (_ \$ (_ \$ (Const ("Not", _) \$ _) \$ _)) => []
138         | _ => [standard (thm' RS (thm' RS eq_to_mono2))]);
139     val concl = concl_of thm
140   in
141     if Logic.is_equals concl then
142       eq2mono (thm RS meta_eq_to_obj_eq)
143     else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
144       eq2mono thm
145     else [thm]
146   end;
149 (* attributes *)
151 fun mono_add_global (thy, thm) = (map_monos (Drule.add_rules (mk_mono thm)) thy, thm);
152 fun mono_del_global (thy, thm) = (map_monos (Drule.del_rules (mk_mono thm)) thy, thm);
154 val mono_attr =
156   Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute);
160 (** misc utilities **)
162 val quiet_mode = ref false;
163 val trace = ref false;  (*for debugging*)
164 fun message s = if ! quiet_mode then () else writeln s;
165 fun clean_message s = if ! quick_and_dirty then () else message s;
167 fun coind_prefix true = "co"
168   | coind_prefix false = "";
171 (*the following code ensures that each recursive set always has the
172   same type in all introduction rules*)
173 fun unify_consts thy cs intr_ts =
174   (let
175     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
176     fun varify (t, (i, ts)) =
177       let val t' = map_term_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
178       in (maxidx_of_term t', t'::ts) end;
179     val (i, cs') = foldr varify (~1, []) cs;
180     val (i', intr_ts') = foldr varify (i, []) intr_ts;
181     val rec_consts = fold add_term_consts_2 cs' [];
182     val intr_consts = fold add_term_consts_2 intr_ts' [];
183     fun unify (cname, cT) =
184       let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
185       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
186     val (env, _) = fold unify rec_consts (Vartab.empty, i');
187     val subst = Type.freeze o map_term_types (Envir.norm_type env)
189   in (map subst cs', map subst intr_ts')
190   end) handle Type.TUNIFY =>
191     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
194 (*make injections used in mutually recursive definitions*)
195 fun mk_inj cs sumT c x =
196   let
197     fun mk_inj' T n i =
198       if n = 1 then x else
199       let val n2 = n div 2;
200           val Type (_, [T1, T2]) = T
201       in
202         if i <= n2 then
203           Const ("Sum_Type.Inl", T1 --> T) \$ (mk_inj' T1 n2 i)
204         else
205           Const ("Sum_Type.Inr", T2 --> T) \$ (mk_inj' T2 (n - n2) (i - n2))
206       end
207   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
208   end;
210 (*make "vimage" terms for selecting out components of mutually rec.def*)
211 fun mk_vimage cs sumT t c = if length cs < 2 then t else
212   let
213     val cT = HOLogic.dest_setT (fastype_of c);
214     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
215   in
216     Const (vimage_name, vimageT) \$
217       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) \$ t
218   end;
220 (** proper splitting **)
222 fun prod_factors p (Const ("Pair", _) \$ t \$ u) =
223       p :: prod_factors (1::p) t @ prod_factors (2::p) u
224   | prod_factors p _ = [];
226 fun mg_prod_factors ts (t \$ u) fs = if t mem ts then
227         let val f = prod_factors [] u
228         in AList.update (op =) (t, f inter (AList.lookup (op =) fs t) |> the_default f) fs end
229       else mg_prod_factors ts u (mg_prod_factors ts t fs)
230   | mg_prod_factors ts (Abs (_, _, t)) fs = mg_prod_factors ts t fs
231   | mg_prod_factors ts _ fs = fs;
233 fun prodT_factors p ps (T as Type ("*", [T1, T2])) =
234       if p mem ps then prodT_factors (1::p) ps T1 @ prodT_factors (2::p) ps T2
235       else [T]
236   | prodT_factors _ _ T = [T];
238 fun ap_split p ps (Type ("*", [T1, T2])) T3 u =
239       if p mem ps then HOLogic.split_const (T1, T2, T3) \$
240         Abs ("v", T1, ap_split (2::p) ps T2 T3 (ap_split (1::p) ps T1
241           (prodT_factors (2::p) ps T2 ---> T3) (incr_boundvars 1 u) \$ Bound 0))
242       else u
243   | ap_split _ _ _ _ u =  u;
245 fun mk_tuple p ps (Type ("*", [T1, T2])) (tms as t::_) =
246       if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms,
247         mk_tuple (2::p) ps T2 (Library.drop (length (prodT_factors (1::p) ps T1), tms)))
248       else t
249   | mk_tuple _ _ _ (t::_) = t;
251 fun split_rule_var' ((t as Var (v, Type ("fun", [T1, T2])), ps), rl) =
252       let val T' = prodT_factors [] ps T1 ---> T2
253           val newt = ap_split [] ps T1 T2 (Var (v, T'))
254           val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
255       in
256           instantiate ([], [(cterm t, cterm newt)]) rl
257       end
258   | split_rule_var' (_, rl) = rl;
260 val remove_split = rewrite_rule [split_conv RS eq_reflection];
262 fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
263   rl (mg_prod_factors vs (Thm.prop_of rl) [])));
265 fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
266   rl (List.mapPartial (fn (t as Var ((a, _), _)) =>
267       Option.map (pair t) (AList.lookup (op =) vs a)) (term_vars (Thm.prop_of rl)))));
270 (** process rules **)
272 local
274 fun err_in_rule thy name t msg =
275   error (cat_lines ["Ill-formed introduction rule " ^ quote name,
276     Sign.string_of_term thy t, msg]);
278 fun err_in_prem thy name t p msg =
279   error (cat_lines ["Ill-formed premise", Sign.string_of_term thy p,
280     "in introduction rule " ^ quote name, Sign.string_of_term thy t, msg]);
282 val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
284 val all_not_allowed =
285     "Introduction rule must not have a leading \"!!\" quantifier";
287 fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize [];
289 in
291 fun check_rule thy cs ((name, rule), att) =
292   let
293     val concl = Logic.strip_imp_concl rule;
294     val prems = Logic.strip_imp_prems rule;
295     val aprems = map (atomize_term thy) prems;
296     val arule = Logic.list_implies (aprems, concl);
298     fun check_prem (prem, aprem) =
299       if can HOLogic.dest_Trueprop aprem then ()
300       else err_in_prem thy name rule prem "Non-atomic premise";
301   in
302     (case concl of
303       Const ("Trueprop", _) \$ (Const ("op :", _) \$ t \$ u) =>
304         if u mem cs then
305           if exists (Logic.occs o rpair t) cs then
306             err_in_rule thy name rule "Recursion term on left of member symbol"
307           else List.app check_prem (prems ~~ aprems)
308         else err_in_rule thy name rule bad_concl
309       | Const ("all", _) \$ _ => err_in_rule thy name rule all_not_allowed
310       | _ => err_in_rule thy name rule bad_concl);
311     ((name, arule), att)
312   end;
314 val rulify =  (* FIXME norm_hhf *)
315   hol_simplify inductive_conj
316   #> hol_simplify inductive_rulify
317   #> hol_simplify inductive_rulify_fallback
318   #> standard;
320 end;
324 (** properties of (co)inductive sets **)
326 (* elimination rules *)
328 fun mk_elims cs cTs params intr_ts intr_names =
329   let
330     val used = foldr add_term_names [] intr_ts;
331     val [aname, pname] = variantlist (["a", "P"], used);
332     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
334     fun dest_intr r =
335       let val Const ("op :", _) \$ t \$ u =
336         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
337       in (u, t, Logic.strip_imp_prems r) end;
339     val intrs = map dest_intr intr_ts ~~ intr_names;
341     fun mk_elim (c, T) =
342       let
343         val a = Free (aname, T);
345         fun mk_elim_prem (_, t, ts) =
346           list_all_free (map dest_Free ((foldr add_term_frees [] (t::ts)) \\ params),
347             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
348         val c_intrs = (List.filter (equal c o #1 o #1) intrs);
349       in
350         (Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
351           map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs)
352       end
353   in
354     map mk_elim (cs ~~ cTs)
355   end;
358 (* premises and conclusions of induction rules *)
360 fun mk_indrule cs cTs params intr_ts =
361   let
362     val used = foldr add_term_names [] intr_ts;
364     (* predicates for induction rule *)
366     val preds = map Free (variantlist (if length cs < 2 then ["P"] else
367       map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
368         map (fn T => T --> HOLogic.boolT) cTs);
370     (* transform an introduction rule into a premise for induction rule *)
372     fun mk_ind_prem r =
373       let
374         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
376         val pred_of = AList.lookup (op aconv) (cs ~~ preds);
378         fun subst (s as ((m as Const ("op :", T)) \$ t \$ u)) =
379               (case pred_of u of
380                   NONE => (m \$ fst (subst t) \$ fst (subst u), NONE)
381                 | SOME P => (HOLogic.mk_binop inductive_conj_name (s, P \$ t), SOME (s, P \$ t)))
382           | subst s =
383               (case pred_of s of
384                   SOME P => (HOLogic.mk_binop "op Int"
385                     (s, HOLogic.Collect_const (HOLogic.dest_setT
386                       (fastype_of s)) \$ P), NONE)
387                 | NONE => (case s of
388                      (t \$ u) => (fst (subst t) \$ fst (subst u), NONE)
389                    | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
390                    | _ => (s, NONE)));
392         fun mk_prem (s, prems) = (case subst s of
393               (_, SOME (t, u)) => t :: u :: prems
394             | (t, _) => t :: prems);
396         val Const ("op :", _) \$ t \$ u =
397           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
399       in list_all_free (frees,
400            Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
401              [] (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r))),
402                HOLogic.mk_Trueprop (valOf (pred_of u) \$ t)))
403       end;
405     val ind_prems = map mk_ind_prem intr_ts;
407     val factors = Library.fold (mg_prod_factors preds) ind_prems [];
409     (* make conclusions for induction rules *)
411     fun mk_ind_concl ((c, P), (ts, x)) =
412       let val T = HOLogic.dest_setT (fastype_of c);
413           val ps = AList.lookup (op =) factors P |> the_default [];
414           val Ts = prodT_factors [] ps T;
415           val (frees, x') = foldr (fn (T', (fs, s)) =>
416             ((Free (s, T'))::fs, Symbol.bump_string s)) ([], x) Ts;
417           val tuple = mk_tuple [] ps T frees;
418       in ((HOLogic.mk_binop "op -->"
419         (HOLogic.mk_mem (tuple, c), P \$ tuple))::ts, x')
420       end;
422     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
423         (fst (foldr mk_ind_concl ([], "xa") (cs ~~ preds))))
425   in (preds, ind_prems, mutual_ind_concl,
426     map (apfst (fst o dest_Free)) factors)
427   end;
430 (* prepare cases and induct rules *)
432 fun add_cases_induct no_elim no_induct coind names elims induct =
433   let
434     fun cases_spec name elim thy =
435       thy
436       |> Theory.parent_path
437       |> Theory.add_path (Sign.base_name name)
438       |> PureThy.add_thms [(("cases", elim), [Attrib.theory (InductAttrib.cases_set name)])] |> snd
439       |> Theory.restore_naming thy;
440     val cases_specs = if no_elim then [] else map2 cases_spec names elims;
442     val induct_att =
443       Attrib.theory o (if coind then InductAttrib.coinduct_set else InductAttrib.induct_set);
444     val induct_specs =
445       if no_induct then I
446       else
447         let
448           val rules = names ~~ map (ProjectRule.project induct) (1 upto length names);
449           val inducts = map (RuleCases.save induct o standard o #2) rules;
450         in
451           PureThy.add_thms (rules |> map (fn (name, th) =>
452             (("", th), [RuleCases.consumes 1, induct_att name]))) #> snd #>
454             [((coind_prefix coind ^ "inducts", inducts), [RuleCases.consumes 1])] #> snd
455         end;
456   in Library.apply cases_specs #> induct_specs end;
460 (** proofs for (co)inductive sets **)
462 (* prove monotonicity -- NOT subject to quick_and_dirty! *)
464 fun prove_mono setT fp_fun monos thy =
465  (message "  Proving monotonicity ...";
466   standard (Goal.prove thy [] []   (*NO quick_and_dirty here!*)
467     (HOLogic.mk_Trueprop
468       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) \$ fp_fun))
469     (fn _ => EVERY [rtac monoI 1,
470       REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)])));
473 (* prove introduction rules *)
475 fun prove_intrs coind mono fp_def intr_ts rec_sets_defs thy =
476   let
477     val _ = clean_message "  Proving the introduction rules ...";
479     val unfold = standard' (mono RS (fp_def RS
480       (if coind then def_gfp_unfold else def_lfp_unfold)));
482     fun select_disj 1 1 = []
483       | select_disj _ 1 = [rtac disjI1]
484       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
486     val intrs = (1 upto (length intr_ts) ~~ intr_ts) |> map (fn (i, intr) =>
487       rulify (SkipProof.prove thy [] [] intr (fn _ => EVERY
488        [rewrite_goals_tac rec_sets_defs,
489         stac unfold 1,
490         REPEAT (resolve_tac [vimageI2, CollectI] 1),
491         (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
492         EVERY1 (select_disj (length intr_ts) i),
493         (*Not ares_tac, since refl must be tried before any equality assumptions;
494           backtracking may occur if the premises have extra variables!*)
495         DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
496         (*Now solve the equations like Inl 0 = Inl ?b2*)
497         REPEAT (rtac refl 1)])))
499   in (intrs, unfold) end;
502 (* prove elimination rules *)
504 fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy =
505   let
506     val _ = clean_message "  Proving the elimination rules ...";
508     val rules1 = [CollectE, disjE, make_elim vimageD, exE];
509     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
510   in
511     mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
512       SkipProof.prove thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
513         (fn prems => EVERY
514           [cut_facts_tac [hd prems] 1,
515            rewrite_goals_tac rec_sets_defs,
516            dtac (unfold RS subst) 1,
517            REPEAT (FIRSTGOAL (eresolve_tac rules1)),
518            REPEAT (FIRSTGOAL (eresolve_tac rules2)),
519            EVERY (map (fn prem =>
520              DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_sets_defs prem, conjI] 1)) (tl prems))])
521         |> rulify
522         |> RuleCases.name cases)
523   end;
526 (* derivation of simplified elimination rules *)
528 local
530 (*cprop should have the form t:Si where Si is an inductive set*)
531 val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
533 (*delete needless equality assumptions*)
534 val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
535 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
536 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
538 fun simp_case_tac solved ss i =
539   EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i
540   THEN_MAYBE (if solved then no_tac else all_tac);
542 in
544 fun mk_cases_i elims ss cprop =
545   let
546     val prem = Thm.assume cprop;
547     val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac;
548     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
549   in
550     (case get_first (try mk_elim) elims of
551       SOME r => r
552     | NONE => error (Pretty.string_of (Pretty.block
553         [Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop])))
554   end;
556 fun mk_cases elims s =
557   mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.theory_of_thm (hd elims)) (s, propT));
559 fun smart_mk_cases thy ss cprop =
560   let
561     val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop
562       (Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err;
563     val (_, {elims, ...}) = the_inductive thy c;
564   in mk_cases_i elims ss cprop end;
566 end;
569 (* inductive_cases(_i) *)
571 fun gen_inductive_cases prep_att prep_prop args thy =
572   let
573     val cert_prop = Thm.cterm_of thy o prep_prop (ProofContext.init thy);
574     val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop;
576     val facts = args |> map (fn ((a, atts), props) =>
577      ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
578   in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
580 val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
581 val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
584 (* mk_cases_meth *)
586 fun mk_cases_meth (ctxt, raw_props) =
587   let
588     val thy = ProofContext.theory_of ctxt;
589     val ss = local_simpset_of ctxt;
590     val cprops = map (Thm.cterm_of thy o ProofContext.read_prop ctxt) raw_props;
591   in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
593 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
596 (* prove induction rule *)
598 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
599     fp_def rec_sets_defs thy =
600   let
601     val _ = clean_message "  Proving the induction rule ...";
603     val sum_case_rewrites =
604       (if Context.theory_name thy = "Datatype" then
605         PureThy.get_thms thy (Name "sum.cases")
606       else
607         (case ThyInfo.lookup_theory "Datatype" of
608           NONE => []
609         | SOME thy' =>
610             if Theory.subthy (thy', thy) then
611               PureThy.get_thms thy' (Name "sum.cases")
612             else []))
613       |> map mk_meta_eq;
615     val (preds, ind_prems, mutual_ind_concl, factors) =
616       mk_indrule cs cTs params intr_ts;
618     val dummy = if !trace then
619                 (writeln "ind_prems = ";
620                  List.app (writeln o Sign.string_of_term thy) ind_prems)
621             else ();
623     (* make predicate for instantiation of abstract induction rule *)
625     fun mk_ind_pred _ [P] = P
626       | mk_ind_pred T Ps =
627          let val n = (length Ps) div 2;
628              val Type (_, [T1, T2]) = T
629          in Const ("Datatype.sum.sum_case",
630            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) \$
631              mk_ind_pred T1 (Library.take (n, Ps)) \$ mk_ind_pred T2 (Library.drop (n, Ps))
632          end;
634     val ind_pred = mk_ind_pred sumT preds;
636     val ind_concl = HOLogic.mk_Trueprop
637       (HOLogic.all_const sumT \$ Abs ("x", sumT, HOLogic.mk_binop "op -->"
638         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred \$ Bound 0)));
640     (* simplification rules for vimage and Collect *)
642     val vimage_simps = if length cs < 2 then [] else
643       map (fn c => standard (SkipProof.prove thy [] []
644         (HOLogic.mk_Trueprop (HOLogic.mk_eq
645           (mk_vimage cs sumT (HOLogic.Collect_const sumT \$ ind_pred) c,
646            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) \$
647              List.nth (preds, find_index_eq c cs))))
648         (fn _ => EVERY
649           [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1]))) cs;
651     val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
653     val dummy = if !trace then
654                 (writeln "raw_fp_induct = "; print_thm raw_fp_induct)
655             else ();
657     val induct = standard (SkipProof.prove thy [] ind_prems ind_concl
658       (fn prems => EVERY
659         [rewrite_goals_tac [inductive_conj_def],
660          rtac (impI RS allI) 1,
661          DETERM (etac raw_fp_induct 1),
662          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
663          fold_goals_tac rec_sets_defs,
664          (*This CollectE and disjE separates out the introduction rules*)
665          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
666          (*Now break down the individual cases.  No disjE here in case
667            some premise involves disjunction.*)
668          REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
669          ALLGOALS (simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
670          EVERY (map (fn prem =>
671            DEPTH_SOLVE_1 (ares_tac [rewrite_rule [inductive_conj_def] prem, conjI, refl] 1)) prems)]));
673     val lemma = standard (SkipProof.prove thy [] []
674       (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
675         [rewrite_goals_tac rec_sets_defs,
676          REPEAT (EVERY
677            [REPEAT (resolve_tac [conjI, impI] 1),
678             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
679             rewrite_goals_tac sum_case_rewrites,
680             atac 1])]))
682   in standard (split_rule factors (induct RS lemma)) end;
686 (** specification of (co)inductive sets **)
688 fun cond_declare_consts declare_consts cs paramTs cnames =
689   if declare_consts then
690     Theory.add_consts_i (map (fn (c, n) => (Sign.base_name n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
691   else I;
693 fun mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
694       params paramTs cTs cnames =
695   let
696     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
697     val setT = HOLogic.mk_setT sumT;
699     val fp_name = if coind then gfp_name else lfp_name;
701     val used = foldr add_term_names [] intr_ts;
702     val [sname, xname] = variantlist (["S", "x"], used);
704     (* transform an introduction rule into a conjunction  *)
705     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
706     (* is transformed into                                *)
707     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
709     fun transform_rule r =
710       let
711         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
712         val subst = subst_free
713           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
714         val Const ("op :", _) \$ t \$ u =
715           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
717       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
718         (foldr1 HOLogic.mk_conj
719           (((HOLogic.eq_const sumT) \$ Free (xname, sumT) \$ (mk_inj cs sumT u t))::
720             (map (subst o HOLogic.dest_Trueprop)
721               (Logic.strip_imp_prems r)))) frees
722       end
724     (* make a disjunction of all introduction rules *)
726     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) \$
727       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
729     (* add definiton of recursive sets to theory *)
731     val rec_name = if alt_name = "" then
732       space_implode "_" (map Sign.base_name cnames) else alt_name;
733     val full_rec_name = if length cs < 2 then hd cnames
734       else Sign.full_name thy rec_name;
736     val rec_const = list_comb
737       (Const (full_rec_name, paramTs ---> setT), params);
739     val fp_def_term = Logic.mk_equals (rec_const,
740       Const (fp_name, (setT --> setT) --> setT) \$ fp_fun);
742     val def_terms = fp_def_term :: (if length cs < 2 then [] else
743       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
745     val ([fp_def :: rec_sets_defs], thy') =
746       thy
747       |> cond_declare_consts declare_consts cs paramTs cnames
748       |> (if length cs < 2 then I
749           else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
750       |> Theory.add_path rec_name
751       |> PureThy.add_defss_i false [(("defs", def_terms), [])];
753     val mono = prove_mono setT fp_fun monos thy'
755   in (thy', rec_name, mono, fp_def, rec_sets_defs, rec_const, sumT) end;
757 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
758     intros monos thy params paramTs cTs cnames induct_cases =
759   let
760     val _ =
761       if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
762         commas_quote (map Sign.base_name cnames)) else ();
764     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
766     val (thy1, rec_name, mono, fp_def, rec_sets_defs, rec_const, sumT) =
767       mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
768         params paramTs cTs cnames;
770     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts rec_sets_defs thy1;
771     val elims = if no_elim then [] else
772       prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy1;
773     val raw_induct = if no_ind then Drule.asm_rl else
774       if coind then standard (rule_by_tactic
775         (rewrite_tac [mk_meta_eq vimage_Un] THEN
776           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
777       else
778         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
779           rec_sets_defs thy1;
780     val induct =
781       if coind then
782         (raw_induct, [RuleCases.case_names [rec_name],
783           RuleCases.case_conclusion (rec_name, induct_cases),
784           RuleCases.consumes 1])
785       else if no_ind orelse length cs > 1 then
786         (raw_induct, [RuleCases.case_names induct_cases, RuleCases.consumes 0])
787       else (raw_induct RSN (2, rev_mp), [RuleCases.case_names induct_cases, RuleCases.consumes 1]);
789     val (intrs', thy2) =
790       thy1
791       |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
792     val (([_, elims'], [induct']), thy3) =
793       thy2
795         [(("intros", intrs'), []),
796           (("elims", elims), [RuleCases.consumes 1])]
798         [((coind_prefix coind ^ "induct", rulify (#1 induct)), #2 induct)];
799   in (thy3,
800     {defs = fp_def :: rec_sets_defs,
801      mono = mono,
802      unfold = unfold,
803      intrs = intrs',
804      elims = elims',
805      mk_cases = mk_cases elims',
806      raw_induct = rulify raw_induct,
807      induct = induct'})
808   end;
811 (* external interfaces *)
813 fun try_term f msg thy t =
814   (case Library.try f t of
815     SOME x => x
816   | NONE => error (msg ^ Sign.string_of_term thy t));
818 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy =
819   let
820     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
822     (*parameters should agree for all mutually recursive components*)
823     val (_, params) = strip_comb (hd cs);
824     val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\
825       \ component is not a free variable: " thy) params;
827     val cTs = map (try_term (HOLogic.dest_setT o fastype_of)
828       "Recursive component not of type set: " thy) cs;
830     val cnames = map (try_term (fst o dest_Const o head_of)
831       "Recursive set not previously declared as constant: " thy) cs;
833     val save_thy = thy
834       |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames;
835     val intros = map (check_rule save_thy cs) pre_intros;
836     val induct_cases = map (#1 o #1) intros;
838     val (thy1, result as {elims, induct, ...}) =
839       add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos
840         thy params paramTs cTs cnames induct_cases;
841     val thy2 = thy1
842       |> put_inductives cnames ({names = cnames, coind = coind}, result)
843       |> add_cases_induct no_elim no_ind coind cnames elims induct
844       |> Theory.parent_path;
845   in (thy2, result) end;
847 fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =
848   let
849     val cs = map (Sign.read_term thy) c_strings;
851     val intr_names = map (fst o fst) intro_srcs;
852     fun read_rule s = Thm.read_cterm thy (s, propT)
853       handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s);
854     val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
855     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
856     val (cs', intr_ts') = unify_consts thy cs intr_ts;
858     val (monos, thy') = thy |> IsarThy.apply_theorems raw_monos;
859   in
860     add_inductive_i verbose false "" coind false false cs'
861       ((intr_names ~~ intr_ts') ~~ intr_atts) monos thy'
862   end;
866 (** package setup **)
868 (* setup theory *)
870 val setup =
871   InductiveData.init #>
872   Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
873     "dynamic case analysis on sets")] #>
874   Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")];
877 (* outer syntax *)
879 local structure P = OuterParse and K = OuterKeyword in
881 fun mk_ind coind ((sets, intrs), monos) =
882   #1 o add_inductive true coind sets (map P.triple_swap intrs) monos;
884 fun ind_decl coind =
885   Scan.repeat1 P.term --
886   (P.\$\$\$ "intros" |--
887     P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) --
888   Scan.optional (P.\$\$\$ "monos" |-- P.!!! P.xthms1) []
889   >> (Toplevel.theory o mk_ind coind);
891 val inductiveP =
892   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
894 val coinductiveP =
895   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
898 val ind_cases =
899   P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
900   >> (Toplevel.theory o inductive_cases);
902 val inductive_casesP =
903   OuterSyntax.command "inductive_cases"
904     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
906 val _ = OuterSyntax.add_keywords ["intros", "monos"];
907 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
909 end;
911 end;