1 (* Title: HOL/Tools/inductive_package.ML
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4 Author: Stefan Berghofer, TU Muenchen
5 Author: Markus Wenzel, TU Muenchen
6 License: GPL (GNU GENERAL PUBLIC LICENSE)
8 (Co)Inductive Definition module for HOL.
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
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
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.
31 signature INDUCTIVE_PACKAGE =
33 val quiet_mode: bool ref
34 val unify_consts: Sign.sg -> 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 * Args.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) * Args.src list) list -> (xstring * Args.src list) list ->
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) list
61 structure InductivePackage: INDUCTIVE_PACKAGE =
65 (** theory context references **)
67 val mono_name = "HOL.mono";
68 val gfp_name = "Gfp.gfp";
69 val lfp_name = "Lfp.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_rulify1 = thms "induct_rulify1";
80 val inductive_rulify2 = thms "induct_rulify2";
86 (* data kind 'HOL/inductive' *)
89 {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
90 induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
92 structure InductiveArgs =
94 val name = "HOL/inductive";
95 type T = inductive_info Symtab.table * thm list;
97 val empty = (Symtab.empty, []);
100 fun merge ((tab1, monos1), (tab2, monos2)) =
101 (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
103 fun print sg (tab, monos) =
104 [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
105 Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)]
106 |> Pretty.chunks |> Pretty.writeln;
109 structure InductiveData = TheoryDataFun(InductiveArgs);
110 val print_inductives = InductiveData.print;
113 (* get and put data *)
115 fun get_inductive thy name = Symtab.lookup (fst (InductiveData.get thy), name);
117 fun the_inductive thy name =
118 (case get_inductive thy name of
119 None => error ("Unknown (co)inductive set " ^ quote name)
120 | Some info => info);
122 val the_mk_cases = (#mk_cases o #2) oo the_inductive;
124 fun put_inductives names info thy =
126 fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
127 val tab_monos = foldl upd (InductiveData.get thy, names)
128 handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
129 in InductiveData.put tab_monos thy end;
133 (** monotonicity rules **)
135 val get_monos = #2 o InductiveData.get;
136 fun map_monos f = InductiveData.map (Library.apsnd f);
140 fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @
141 (case concl_of thm of
142 (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
143 | _ => [standard (thm' RS (thm' RS eq_to_mono2))]);
144 val concl = concl_of thm
146 if Logic.is_equals concl then
147 eq2mono (thm RS meta_eq_to_obj_eq)
148 else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
156 fun mono_add_global (thy, thm) = (map_monos (Drule.add_rules (mk_mono thm)) thy, thm);
157 fun mono_del_global (thy, thm) = (map_monos (Drule.del_rules (mk_mono thm)) thy, thm);
160 (Attrib.add_del_args mono_add_global mono_del_global,
161 Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute);
165 (** misc utilities **)
167 val quiet_mode = ref false;
168 fun message s = if ! quiet_mode then () else writeln s;
169 fun clean_message s = if ! quick_and_dirty then () else message s;
171 fun coind_prefix true = "co"
172 | coind_prefix false = "";
175 (*the following code ensures that each recursive set always has the
176 same type in all introduction rules*)
177 fun unify_consts sign cs intr_ts =
179 val {tsig, ...} = Sign.rep_sg sign;
180 val add_term_consts_2 =
181 foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
182 fun varify (t, (i, ts)) =
183 let val t' = map_term_types (incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
184 in (maxidx_of_term t', t'::ts) end;
185 val (i, cs') = foldr varify (cs, (~1, []));
186 val (i', intr_ts') = foldr varify (intr_ts, (i, []));
187 val rec_consts = foldl add_term_consts_2 ([], cs');
188 val intr_consts = foldl add_term_consts_2 ([], intr_ts');
189 fun unify (env, (cname, cT)) =
190 let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
191 in foldl (fn ((env', j'), Tp) => (Type.unify tsig (env', j') Tp))
192 (env, (replicate (length consts) cT) ~~ consts)
194 val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts);
195 fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T
196 in if T = T' then T else typ_subst_TVars_2 env T' end;
197 val subst = fst o Type.freeze_thaw o
198 (map_term_types (typ_subst_TVars_2 env))
200 in (map subst cs', map subst intr_ts')
201 end) handle Type.TUNIFY =>
202 (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
205 (*make injections used in mutually recursive definitions*)
206 fun mk_inj cs sumT c x =
210 let val n2 = n div 2;
211 val Type (_, [T1, T2]) = T
214 Const ("Inl", T1 --> T) $ (mk_inj' T1 n2 i)
216 Const ("Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
218 in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
221 (*make "vimage" terms for selecting out components of mutually rec.def*)
222 fun mk_vimage cs sumT t c = if length cs < 2 then t else
224 val cT = HOLogic.dest_setT (fastype_of c);
225 val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
227 Const (vimage_name, vimageT) $
228 Abs ("y", cT, mk_inj cs sumT c (Bound 0)) $ t
231 (** proper splitting **)
233 fun prod_factors p (Const ("Pair", _) $ t $ u) =
234 p :: prod_factors (1::p) t @ prod_factors (2::p) u
235 | prod_factors p _ = [];
237 fun mg_prod_factors ts (fs, t $ u) = if t mem ts then
238 let val f = prod_factors [] u
239 in overwrite (fs, (t, f inter if_none (assoc (fs, t)) f)) end
240 else mg_prod_factors ts (mg_prod_factors ts (fs, t), u)
241 | mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t)
242 | mg_prod_factors ts (fs, _) = fs;
244 fun prodT_factors p ps (T as Type ("*", [T1, T2])) =
245 if p mem ps then prodT_factors (1::p) ps T1 @ prodT_factors (2::p) ps T2
247 | prodT_factors _ _ T = [T];
249 fun ap_split p ps (Type ("*", [T1, T2])) T3 u =
250 if p mem ps then HOLogic.split_const (T1, T2, T3) $
251 Abs ("v", T1, ap_split (2::p) ps T2 T3 (ap_split (1::p) ps T1
252 (prodT_factors (2::p) ps T2 ---> T3) (incr_boundvars 1 u) $ Bound 0))
254 | ap_split _ _ _ _ u = u;
256 fun mk_tuple p ps (Type ("*", [T1, T2])) (tms as t::_) =
257 if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms,
258 mk_tuple (2::p) ps T2 (drop (length (prodT_factors (1::p) ps T1), tms)))
260 | mk_tuple _ _ _ (t::_) = t;
262 fun split_rule_var' ((t as Var (v, Type ("fun", [T1, T2])), ps), rl) =
263 let val T' = prodT_factors [] ps T1 ---> T2
264 val newt = ap_split [] ps T1 T2 (Var (v, T'))
265 val cterm = Thm.cterm_of (#sign (rep_thm rl))
267 instantiate ([], [(cterm t, cterm newt)]) rl
269 | split_rule_var' (_, rl) = rl;
271 val remove_split = rewrite_rule [split_conv RS eq_reflection];
273 fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
274 (mg_prod_factors vs ([], #prop (rep_thm rl)), rl)));
276 fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
277 (mapfilter (fn (t as Var ((a, _), _)) =>
278 apsome (pair t) (assoc (vs, a))) (term_vars (#prop (rep_thm rl))), rl)));
281 (** process rules **)
285 fun err_in_rule sg name t msg =
286 error (cat_lines ["Ill-formed introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
288 fun err_in_prem sg name t p msg =
289 error (cat_lines ["Ill-formed premise", Sign.string_of_term sg p,
290 "in introduction rule " ^ quote name, Sign.string_of_term sg t, msg]);
292 val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
294 val all_not_allowed =
295 "Introduction rule must not have a leading \"!!\" quantifier";
297 fun atomize_term sg = MetaSimplifier.rewrite_term sg inductive_atomize;
301 fun check_rule sg cs ((name, rule), att) =
303 val concl = Logic.strip_imp_concl rule;
304 val prems = Logic.strip_imp_prems rule;
305 val aprems = map (atomize_term sg) prems;
306 val arule = Logic.list_implies (aprems, concl);
308 fun check_prem (prem, aprem) =
309 if can HOLogic.dest_Trueprop aprem then ()
310 else err_in_prem sg name rule prem "Non-atomic premise";
313 Const ("Trueprop", _) $ (Const ("op :", _) $ t $ u) =>
315 if exists (Logic.occs o rpair t) cs then
316 err_in_rule sg name rule "Recursion term on left of member symbol"
317 else seq check_prem (prems ~~ aprems)
318 else err_in_rule sg name rule bad_concl
319 | Const ("all", _) $ _ => err_in_rule sg name rule all_not_allowed
320 | _ => err_in_rule sg name rule bad_concl);
325 standard o Tactic.norm_hhf_rule o
326 hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o
327 hol_simplify inductive_conj;
333 (** properties of (co)inductive sets **)
335 (* elimination rules *)
337 fun mk_elims cs cTs params intr_ts intr_names =
339 val used = foldr add_term_names (intr_ts, []);
340 val [aname, pname] = variantlist (["a", "P"], used);
341 val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
344 let val Const ("op :", _) $ t $ u =
345 HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
346 in (u, t, Logic.strip_imp_prems r) end;
348 val intrs = map dest_intr intr_ts ~~ intr_names;
352 val a = Free (aname, T);
354 fun mk_elim_prem (_, t, ts) =
355 list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
356 Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
357 val c_intrs = (filter (equal c o #1 o #1) intrs);
359 (Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
360 map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs)
363 map mk_elim (cs ~~ cTs)
367 (* premises and conclusions of induction rules *)
369 fun mk_indrule cs cTs params intr_ts =
371 val used = foldr add_term_names (intr_ts, []);
373 (* predicates for induction rule *)
375 val preds = map Free (variantlist (if length cs < 2 then ["P"] else
376 map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
377 map (fn T => T --> HOLogic.boolT) cTs);
379 (* transform an introduction rule into a premise for induction rule *)
383 val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
385 val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
387 fun subst (s as ((m as Const ("op :", T)) $ t $ u)) =
389 None => (m $ fst (subst t) $ fst (subst u), None)
390 | Some P => (HOLogic.mk_binop inductive_conj_name (s, P $ t), Some (s, P $ t)))
393 Some P => (HOLogic.mk_binop "op Int"
394 (s, HOLogic.Collect_const (HOLogic.dest_setT
395 (fastype_of s)) $ P), None)
397 (t $ u) => (fst (subst t) $ fst (subst u), None)
398 | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None)
401 fun mk_prem (s, prems) = (case subst s of
402 (_, Some (t, u)) => t :: u :: prems
403 | (t, _) => t :: prems);
405 val Const ("op :", _) $ t $ u =
406 HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
408 in list_all_free (frees,
409 Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
410 (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
411 HOLogic.mk_Trueprop (the (pred_of u) $ t)))
414 val ind_prems = map mk_ind_prem intr_ts;
415 val factors = foldl (mg_prod_factors preds) ([], ind_prems);
417 (* make conclusions for induction rules *)
419 fun mk_ind_concl ((c, P), (ts, x)) =
420 let val T = HOLogic.dest_setT (fastype_of c);
421 val ps = if_none (assoc (factors, P)) [];
422 val Ts = prodT_factors [] ps T;
423 val (frees, x') = foldr (fn (T', (fs, s)) =>
424 ((Free (s, T'))::fs, Symbol.bump_string s)) (Ts, ([], x));
425 val tuple = mk_tuple [] ps T frees;
426 in ((HOLogic.mk_binop "op -->"
427 (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x')
430 val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
431 (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
433 in (preds, ind_prems, mutual_ind_concl,
434 map (apfst (fst o dest_Free)) factors)
438 (* prepare cases and induct rules *)
441 transform mutual rule:
442 HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
443 into i-th projection:
444 xi:Ai ==> HH ==> Pi xi
447 fun project_rules [name] rule = [(name, rule)]
448 | project_rules names mutual_rule =
450 val n = length names;
452 (if i < n then (fn th => th RS conjunct1) else I)
453 (Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule)
454 RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
455 in names ~~ map proj (1 upto n) end;
457 fun add_cases_induct no_elim no_induct names elims induct =
459 fun cases_spec (name, elim) thy =
461 |> Theory.add_path (Sign.base_name name)
462 |> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
463 |> Theory.parent_path;
464 val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
466 fun induct_spec (name, th) = #1 o PureThy.add_thms
467 [(("", RuleCases.save induct th), [InductAttrib.induct_set_global name])];
468 val induct_specs = if no_induct then [] else map induct_spec (project_rules names induct);
469 in Library.apply (cases_specs @ induct_specs) end;
473 (** proofs for (co)inductive sets **)
475 (* prove monotonicity -- NOT subject to quick_and_dirty! *)
477 fun prove_mono setT fp_fun monos thy =
478 (message " Proving monotonicity ...";
479 Goals.prove_goalw_cterm [] (*NO quick_and_dirty_prove_goalw_cterm here!*)
480 (Thm.cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
481 (Const (mono_name, (setT --> setT) --> HOLogic.boolT) $ fp_fun)))
482 (fn _ => [rtac monoI 1, REPEAT (ares_tac (flat (map mk_mono monos) @ get_monos thy) 1)]));
485 (* prove introduction rules *)
487 fun prove_intrs coind mono fp_def intr_ts rec_sets_defs thy =
489 val _ = clean_message " Proving the introduction rules ...";
491 val unfold = standard (mono RS (fp_def RS
492 (if coind then def_gfp_unfold else def_lfp_unfold)));
494 fun select_disj 1 1 = []
495 | select_disj _ 1 = [rtac disjI1]
496 | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
498 val intrs = map (fn (i, intr) => quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
499 (Thm.cterm_of (Theory.sign_of thy) intr) (fn prems =>
500 [(*insert prems and underlying sets*)
501 cut_facts_tac prems 1,
503 REPEAT (resolve_tac [vimageI2, CollectI] 1),
504 (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
505 EVERY1 (select_disj (length intr_ts) i),
506 (*Not ares_tac, since refl must be tried before any equality assumptions;
507 backtracking may occur if the premises have extra variables!*)
508 DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
509 (*Now solve the equations like Inl 0 = Inl ?b2*)
510 REPEAT (rtac refl 1)])
511 |> rulify) (1 upto (length intr_ts) ~~ intr_ts)
513 in (intrs, unfold) end;
516 (* prove elimination rules *)
518 fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy =
520 val _ = clean_message " Proving the elimination rules ...";
522 val rules1 = [CollectE, disjE, make_elim vimageD, exE];
523 val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
525 mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
526 quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
527 (Thm.cterm_of (Theory.sign_of thy) t) (fn prems =>
528 [cut_facts_tac [hd prems] 1,
529 dtac (unfold RS subst) 1,
530 REPEAT (FIRSTGOAL (eresolve_tac rules1)),
531 REPEAT (FIRSTGOAL (eresolve_tac rules2)),
532 EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
534 |> RuleCases.name cases)
538 (* derivation of simplified elimination rules *)
542 (*cprop should have the form t:Si where Si is an inductive set*)
543 val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
545 (*delete needless equality assumptions*)
546 val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
547 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
548 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
550 fun simp_case_tac solved ss i =
551 EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i
552 THEN_MAYBE (if solved then no_tac else all_tac);
556 fun mk_cases_i elims ss cprop =
558 val prem = Thm.assume cprop;
559 val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac;
560 fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
562 (case get_first (try mk_elim) elims of
564 | None => error (Pretty.string_of (Pretty.block
565 [Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop])))
568 fun mk_cases elims s =
569 mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
571 fun smart_mk_cases thy ss cprop =
573 val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop
574 (Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err;
575 val (_, {elims, ...}) = the_inductive thy c;
576 in mk_cases_i elims ss cprop end;
581 (* inductive_cases(_i) *)
583 fun gen_inductive_cases prep_att prep_prop args thy =
585 val cert_prop = Thm.cterm_of (Theory.sign_of thy) o prep_prop (ProofContext.init thy);
586 val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop;
588 val facts = args |> map (fn ((a, atts), props) =>
589 ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
590 in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
592 val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
593 val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
598 fun mk_cases_meth (ctxt, raw_props) =
600 val thy = ProofContext.theory_of ctxt;
601 val ss = Simplifier.get_local_simpset ctxt;
602 val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props;
603 in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
605 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
608 (* prove induction rule *)
610 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
611 fp_def rec_sets_defs thy =
613 val _ = clean_message " Proving the induction rule ...";
615 val sign = Theory.sign_of thy;
617 val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
619 | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
621 val (preds, ind_prems, mutual_ind_concl, factors) =
622 mk_indrule cs cTs params intr_ts;
624 (* make predicate for instantiation of abstract induction rule *)
626 fun mk_ind_pred _ [P] = P
628 let val n = (length Ps) div 2;
629 val Type (_, [T1, T2]) = T
630 in Const ("Datatype.sum.sum_case",
631 [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) $
632 mk_ind_pred T1 (take (n, Ps)) $ mk_ind_pred T2 (drop (n, Ps))
635 val ind_pred = mk_ind_pred sumT preds;
637 val ind_concl = HOLogic.mk_Trueprop
638 (HOLogic.all_const sumT $ Abs ("x", sumT, HOLogic.mk_binop "op -->"
639 (HOLogic.mk_mem (Bound 0, rec_const), ind_pred $ Bound 0)));
641 (* simplification rules for vimage and Collect *)
643 val vimage_simps = if length cs < 2 then [] else
644 map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of sign
645 (HOLogic.mk_Trueprop (HOLogic.mk_eq
646 (mk_vimage cs sumT (HOLogic.Collect_const sumT $ ind_pred) c,
647 HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) $
648 nth_elem (find_index_eq c cs, preds)))))
649 (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
651 val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of sign
652 (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
653 [rtac (impI RS allI) 1,
654 DETERM (etac (mono RS (fp_def RS def_lfp_induct)) 1),
655 rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
656 fold_goals_tac rec_sets_defs,
657 (*This CollectE and disjE separates out the introduction rules*)
658 REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
659 (*Now break down the individual cases. No disjE here in case
660 some premise involves disjunction.*)
661 REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
662 rewrite_goals_tac sum_case_rewrites,
663 EVERY (map (fn prem =>
664 DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
666 val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of sign
667 (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
668 [cut_facts_tac prems 1,
670 [REPEAT (resolve_tac [conjI, impI] 1),
671 TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
672 rewrite_goals_tac sum_case_rewrites,
675 in standard (split_rule factors (induct RS lemma)) end;
679 (** specification of (co)inductive sets **)
681 fun cond_declare_consts declare_consts cs paramTs cnames =
682 if declare_consts then
683 Theory.add_consts_i (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
686 fun mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
687 params paramTs cTs cnames =
689 val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
690 val setT = HOLogic.mk_setT sumT;
692 val fp_name = if coind then gfp_name else lfp_name;
694 val used = foldr add_term_names (intr_ts, []);
695 val [sname, xname] = variantlist (["S", "x"], used);
697 (* transform an introduction rule into a conjunction *)
698 (* [| t : ... S_i ... ; ... |] ==> u : S_j *)
699 (* is transformed into *)
700 (* x = Inj_j u & t : ... Inj_i -`` S ... & ... *)
702 fun transform_rule r =
704 val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
705 val subst = subst_free
706 (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
707 val Const ("op :", _) $ t $ u =
708 HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
710 in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
711 (frees, foldr1 HOLogic.mk_conj
712 (((HOLogic.eq_const sumT) $ Free (xname, sumT) $ (mk_inj cs sumT u t))::
713 (map (subst o HOLogic.dest_Trueprop)
714 (Logic.strip_imp_prems r))))
717 (* make a disjunction of all introduction rules *)
719 val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) $
720 absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
722 (* add definiton of recursive sets to theory *)
724 val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
725 val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
727 val rec_const = list_comb
728 (Const (full_rec_name, paramTs ---> setT), params);
730 val fp_def_term = Logic.mk_equals (rec_const,
731 Const (fp_name, (setT --> setT) --> setT) $ fp_fun);
733 val def_terms = fp_def_term :: (if length cs < 2 then [] else
734 map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
736 val (thy', [fp_def :: rec_sets_defs]) =
738 |> cond_declare_consts declare_consts cs paramTs cnames
739 |> (if length cs < 2 then I
740 else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
741 |> Theory.add_path rec_name
742 |> PureThy.add_defss_i false [(("defs", def_terms), [])];
744 val mono = prove_mono setT fp_fun monos thy'
746 in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
748 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
749 intros monos thy params paramTs cTs cnames induct_cases =
752 if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
753 commas_quote cnames) else ();
755 val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
757 val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) =
758 mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
759 params paramTs cTs cnames;
761 val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts rec_sets_defs thy1;
762 val elims = if no_elim then [] else
763 prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy1;
764 val raw_induct = if no_ind then Drule.asm_rl else
765 if coind then standard (rule_by_tactic
766 (rewrite_tac [mk_meta_eq vimage_Un] THEN
767 fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
769 prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
772 if coind orelse no_ind orelse length cs > 1 then (raw_induct, [RuleCases.consumes 0])
773 else (raw_induct RSN (2, rev_mp), [RuleCases.consumes 1]);
776 thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
777 val (thy3, ([intrs'', elims'], [induct'])) =
780 [(("intros", intrs'), []),
781 (("elims", elims), [RuleCases.consumes 1])]
782 |>>> PureThy.add_thms
783 [((coind_prefix coind ^ "induct", rulify (#1 induct)),
784 (RuleCases.case_names induct_cases :: #2 induct))]
785 |>> Theory.parent_path;
787 {defs = fp_def :: rec_sets_defs,
792 mk_cases = mk_cases elims',
793 raw_induct = rulify raw_induct,
798 (* external interfaces *)
800 fun try_term f msg sign t =
801 (case Library.try f t of
803 | None => error (msg ^ Sign.string_of_term sign t));
805 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy =
807 val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
808 val sign = Theory.sign_of thy;
810 (*parameters should agree for all mutually recursive components*)
811 val (_, params) = strip_comb (hd cs);
812 val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\
813 \ component is not a free variable: " sign) params;
815 val cTs = map (try_term (HOLogic.dest_setT o fastype_of)
816 "Recursive component not of type set: " sign) cs;
818 val full_cnames = map (try_term (fst o dest_Const o head_of)
819 "Recursive set not previously declared as constant: " sign) cs;
820 val cnames = map Sign.base_name full_cnames;
823 thy |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames |> Theory.sign_of;
824 val intros = map (check_rule save_sign cs) pre_intros;
825 val induct_cases = map (#1 o #1) intros;
827 val (thy1, result as {elims, induct, ...}) =
828 add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos
829 thy params paramTs cTs cnames induct_cases;
831 |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
832 |> add_cases_induct no_elim (no_ind orelse coind orelse length cs > 1)
833 full_cnames elims induct;
834 in (thy2, result) end;
836 fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =
838 val sign = Theory.sign_of thy;
839 val cs = map (term_of o HOLogic.read_cterm sign) c_strings;
841 val intr_names = map (fst o fst) intro_srcs;
842 fun read_rule s = Thm.read_cterm sign (s, propT)
843 handle ERROR => error ("The error(s) above occurred for " ^ s);
844 val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
845 val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
846 val (cs', intr_ts') = unify_consts sign cs intr_ts;
848 val (thy', monos) = thy |> IsarThy.apply_theorems raw_monos;
850 add_inductive_i verbose false "" coind false false cs'
851 ((intr_names ~~ intr_ts') ~~ intr_atts) monos thy'
856 (** package setup **)
862 Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
863 "dynamic case analysis on sets")],
864 Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
869 local structure P = OuterParse and K = OuterSyntax.Keyword in
871 fun mk_ind coind ((sets, intrs), monos) =
872 #1 o add_inductive true coind sets (map P.triple_swap intrs) monos;
875 Scan.repeat1 P.term --
877 P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) --
878 Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) []
879 >> (Toplevel.theory o mk_ind coind);
882 OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
885 OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
889 P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
890 >> (Toplevel.theory o inductive_cases);
892 val inductive_casesP =
893 OuterSyntax.command "inductive_cases"
894 "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
896 val _ = OuterSyntax.add_keywords ["intros", "monos"];
897 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];