src/HOL/Tools/inductive_package.ML
 author wenzelm Thu Jul 28 15:19:49 2005 +0200 (2005-07-28) changeset 16934 9ef19e3c7fdd parent 16876 f57b38cced32 child 16975 34ed8d5d4f16 permissions -rw-r--r--
Sign.typ_unify;
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) list
59 end;
61 structure InductivePackage: INDUCTIVE_PACKAGE =
62 struct
65 (** theory context references **)
67 val mono_name = "Orderings.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";
84 (** theory data **)
86 (* data kind 'HOL/inductive' *)
88 type inductive_info =
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 InductiveData = TheoryDataFun
93 (struct
94   val name = "HOL/inductive";
95   type T = inductive_info Symtab.table * thm list;
97   val empty = (Symtab.empty, []);
98   val copy = I;
99   val extend = I;
100   fun merge _ ((tab1, monos1), (tab2, monos2)) =
101     (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
103   fun print thy (tab, monos) =
104     [Pretty.strs ("(co)inductives:" ::
105       map #1 (NameSpace.extern_table (Sign.const_space thy, tab))),
106      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg thy) monos)]
107     |> Pretty.chunks |> Pretty.writeln;
108 end);
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 =
125   let
126     fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
127     val tab_monos = Library.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);
138 fun mk_mono thm =
139   let
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
145   in
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
149       eq2mono thm
150     else [thm]
151   end;
154 (* attributes *)
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);
159 val mono_attr =
161   Attrib.add_del_args Attrib.undef_local_attribute Attrib.undef_local_attribute);
165 (** misc utilities **)
167 val quiet_mode = ref false;
168 val trace = ref false;  (*for debugging*)
169 fun message s = if ! quiet_mode then () else writeln s;
170 fun clean_message s = if ! quick_and_dirty then () else message s;
172 fun coind_prefix true = "co"
173   | coind_prefix false = "";
176 (*the following code ensures that each recursive set always has the
177   same type in all introduction rules*)
178 fun unify_consts thy cs intr_ts =
179   (let
180     val add_term_consts_2 = fold_aterms (fn Const c => insert (op =) c | _ => I);
181     fun varify (t, (i, ts)) =
182       let val t' = map_term_types (Logic.incr_tvar (i + 1)) (#1 (Type.varify (t, [])))
183       in (maxidx_of_term t', t'::ts) end;
184     val (i, cs') = foldr varify (~1, []) cs;
185     val (i', intr_ts') = foldr varify (i, []) intr_ts;
186     val rec_consts = fold add_term_consts_2 cs' [];
187     val intr_consts = fold add_term_consts_2 intr_ts' [];
188     fun unify (cname, cT) =
189       let val consts = map snd (List.filter (fn c => fst c = cname) intr_consts)
190       in fold (Sign.typ_unify thy) ((replicate (length consts) cT) ~~ consts) end;
191     val (env, _) = fold unify rec_consts (Vartab.empty, i');
192     val subst = Type.freeze o map_term_types (Envir.norm_type env)
194   in (map subst cs', map subst intr_ts')
195   end) handle Type.TUNIFY =>
196     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
199 (*make injections used in mutually recursive definitions*)
200 fun mk_inj cs sumT c x =
201   let
202     fun mk_inj' T n i =
203       if n = 1 then x else
204       let val n2 = n div 2;
205           val Type (_, [T1, T2]) = T
206       in
207         if i <= n2 then
208           Const ("Sum_Type.Inl", T1 --> T) \$ (mk_inj' T1 n2 i)
209         else
210           Const ("Sum_Type.Inr", T2 --> T) \$ (mk_inj' T2 (n - n2) (i - n2))
211       end
212   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
213   end;
215 (*make "vimage" terms for selecting out components of mutually rec.def*)
216 fun mk_vimage cs sumT t c = if length cs < 2 then t else
217   let
218     val cT = HOLogic.dest_setT (fastype_of c);
219     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
220   in
221     Const (vimage_name, vimageT) \$
222       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) \$ t
223   end;
225 (** proper splitting **)
227 fun prod_factors p (Const ("Pair", _) \$ t \$ u) =
228       p :: prod_factors (1::p) t @ prod_factors (2::p) u
229   | prod_factors p _ = [];
231 fun mg_prod_factors ts (fs, t \$ u) = if t mem ts then
232         let val f = prod_factors [] u
233         in overwrite (fs, (t, f inter (curry getOpt) (assoc (fs, t)) f)) end
234       else mg_prod_factors ts (mg_prod_factors ts (fs, t), u)
235   | mg_prod_factors ts (fs, Abs (_, _, t)) = mg_prod_factors ts (fs, t)
236   | mg_prod_factors ts (fs, _) = fs;
238 fun prodT_factors p ps (T as Type ("*", [T1, T2])) =
239       if p mem ps then prodT_factors (1::p) ps T1 @ prodT_factors (2::p) ps T2
240       else [T]
241   | prodT_factors _ _ T = [T];
243 fun ap_split p ps (Type ("*", [T1, T2])) T3 u =
244       if p mem ps then HOLogic.split_const (T1, T2, T3) \$
245         Abs ("v", T1, ap_split (2::p) ps T2 T3 (ap_split (1::p) ps T1
246           (prodT_factors (2::p) ps T2 ---> T3) (incr_boundvars 1 u) \$ Bound 0))
247       else u
248   | ap_split _ _ _ _ u =  u;
250 fun mk_tuple p ps (Type ("*", [T1, T2])) (tms as t::_) =
251       if p mem ps then HOLogic.mk_prod (mk_tuple (1::p) ps T1 tms,
252         mk_tuple (2::p) ps T2 (Library.drop (length (prodT_factors (1::p) ps T1), tms)))
253       else t
254   | mk_tuple _ _ _ (t::_) = t;
256 fun split_rule_var' ((t as Var (v, Type ("fun", [T1, T2])), ps), rl) =
257       let val T' = prodT_factors [] ps T1 ---> T2
258           val newt = ap_split [] ps T1 T2 (Var (v, T'))
259           val cterm = Thm.cterm_of (Thm.theory_of_thm rl)
260       in
261           instantiate ([], [(cterm t, cterm newt)]) rl
262       end
263   | split_rule_var' (_, rl) = rl;
265 val remove_split = rewrite_rule [split_conv RS eq_reflection];
267 fun split_rule_vars vs rl = standard (remove_split (foldr split_rule_var'
268   rl (mg_prod_factors vs ([], Thm.prop_of rl))));
270 fun split_rule vs rl = standard (remove_split (foldr split_rule_var'
271   rl (List.mapPartial (fn (t as Var ((a, _), _)) =>
272       Option.map (pair t) (assoc (vs, a))) (term_vars (Thm.prop_of rl)))));
275 (** process rules **)
277 local
279 fun err_in_rule thy name t msg =
280   error (cat_lines ["Ill-formed introduction rule " ^ quote name,
281     Sign.string_of_term thy t, msg]);
283 fun err_in_prem thy name t p msg =
284   error (cat_lines ["Ill-formed premise", Sign.string_of_term thy p,
285     "in introduction rule " ^ quote name, Sign.string_of_term thy t, msg]);
287 val bad_concl = "Conclusion of introduction rule must have form \"t : S_i\"";
289 val all_not_allowed =
290     "Introduction rule must not have a leading \"!!\" quantifier";
292 fun atomize_term thy = MetaSimplifier.rewrite_term thy inductive_atomize [];
294 in
296 fun check_rule thy cs ((name, rule), att) =
297   let
298     val concl = Logic.strip_imp_concl rule;
299     val prems = Logic.strip_imp_prems rule;
300     val aprems = map (atomize_term thy) prems;
301     val arule = Logic.list_implies (aprems, concl);
303     fun check_prem (prem, aprem) =
304       if can HOLogic.dest_Trueprop aprem then ()
305       else err_in_prem thy name rule prem "Non-atomic premise";
306   in
307     (case concl of
308       Const ("Trueprop", _) \$ (Const ("op :", _) \$ t \$ u) =>
309         if u mem cs then
310           if exists (Logic.occs o rpair t) cs then
311             err_in_rule thy name rule "Recursion term on left of member symbol"
312           else List.app check_prem (prems ~~ aprems)
313         else err_in_rule thy name rule bad_concl
314       | Const ("all", _) \$ _ => err_in_rule thy name rule all_not_allowed
315       | _ => err_in_rule thy name rule bad_concl);
316     ((name, arule), att)
317   end;
319 val rulify =
320   standard o
321   hol_simplify inductive_rulify2 o hol_simplify inductive_rulify1 o
322   hol_simplify inductive_conj;
324 end;
328 (** properties of (co)inductive sets **)
330 (* elimination rules *)
332 fun mk_elims cs cTs params intr_ts intr_names =
333   let
334     val used = foldr add_term_names [] intr_ts;
335     val [aname, pname] = variantlist (["a", "P"], used);
336     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
338     fun dest_intr r =
339       let val Const ("op :", _) \$ t \$ u =
340         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
341       in (u, t, Logic.strip_imp_prems r) end;
343     val intrs = map dest_intr intr_ts ~~ intr_names;
345     fun mk_elim (c, T) =
346       let
347         val a = Free (aname, T);
349         fun mk_elim_prem (_, t, ts) =
350           list_all_free (map dest_Free ((foldr add_term_frees [] (t::ts)) \\ params),
351             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
352         val c_intrs = (List.filter (equal c o #1 o #1) intrs);
353       in
354         (Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
355           map mk_elim_prem (map #1 c_intrs), P), map #2 c_intrs)
356       end
357   in
358     map mk_elim (cs ~~ cTs)
359   end;
362 (* premises and conclusions of induction rules *)
364 fun mk_indrule cs cTs params intr_ts =
365   let
366     val used = foldr add_term_names [] intr_ts;
368     (* predicates for induction rule *)
370     val preds = map Free (variantlist (if length cs < 2 then ["P"] else
371       map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
372         map (fn T => T --> HOLogic.boolT) cTs);
374     (* transform an introduction rule into a premise for induction rule *)
376     fun mk_ind_prem r =
377       let
378         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
380         val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
382         fun subst (s as ((m as Const ("op :", T)) \$ t \$ u)) =
383               (case pred_of u of
384                   NONE => (m \$ fst (subst t) \$ fst (subst u), NONE)
385                 | SOME P => (HOLogic.mk_binop inductive_conj_name (s, P \$ t), SOME (s, P \$ t)))
386           | subst s =
387               (case pred_of s of
388                   SOME P => (HOLogic.mk_binop "op Int"
389                     (s, HOLogic.Collect_const (HOLogic.dest_setT
390                       (fastype_of s)) \$ P), NONE)
391                 | NONE => (case s of
392                      (t \$ u) => (fst (subst t) \$ fst (subst u), NONE)
393                    | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), NONE)
394                    | _ => (s, NONE)));
396         fun mk_prem (s, prems) = (case subst s of
397               (_, SOME (t, u)) => t :: u :: prems
398             | (t, _) => t :: prems);
400         val Const ("op :", _) \$ t \$ u =
401           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
403       in list_all_free (frees,
404            Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
405              [] (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r))),
406                HOLogic.mk_Trueprop (valOf (pred_of u) \$ t)))
407       end;
409     val ind_prems = map mk_ind_prem intr_ts;
411     val factors = Library.foldl (mg_prod_factors preds) ([], ind_prems);
413     (* make conclusions for induction rules *)
415     fun mk_ind_concl ((c, P), (ts, x)) =
416       let val T = HOLogic.dest_setT (fastype_of c);
417           val ps = getOpt (assoc (factors, P), []);
418           val Ts = prodT_factors [] ps T;
419           val (frees, x') = foldr (fn (T', (fs, s)) =>
420             ((Free (s, T'))::fs, Symbol.bump_string s)) ([], x) Ts;
421           val tuple = mk_tuple [] ps T frees;
422       in ((HOLogic.mk_binop "op -->"
423         (HOLogic.mk_mem (tuple, c), P \$ tuple))::ts, x')
424       end;
426     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
427         (fst (foldr mk_ind_concl ([], "xa") (cs ~~ preds))))
429   in (preds, ind_prems, mutual_ind_concl,
430     map (apfst (fst o dest_Free)) factors)
431   end;
434 (* prepare cases and induct rules *)
436 (*
437   transform mutual rule:
438     HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
439   into i-th projection:
440     xi:Ai ==> HH ==> Pi xi
441 *)
443 fun project_rules [name] rule = [(name, rule)]
444   | project_rules names mutual_rule =
445       let
446         val n = length names;
447         fun proj i =
448           (if i < n then (fn th => th RS conjunct1) else I)
449             (Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule)
450             RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
451       in names ~~ map proj (1 upto n) end;
453 fun add_cases_induct no_elim no_induct names elims induct =
454   let
455     fun cases_spec (name, elim) thy =
456       thy
457       |> Theory.add_path (Sign.base_name name)
458       |> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
459       |> Theory.parent_path;
460     val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
462     fun induct_spec (name, th) = #1 o PureThy.add_thms
463       [(("", RuleCases.save induct th), [InductAttrib.induct_set_global name])];
464     val induct_specs = if no_induct then [] else map induct_spec (project_rules names induct);
465   in Library.apply (cases_specs @ induct_specs) end;
469 (** proofs for (co)inductive sets **)
471 (* prove monotonicity -- NOT subject to quick_and_dirty! *)
473 fun prove_mono setT fp_fun monos thy =
474  (message "  Proving monotonicity ...";
475   Goals.prove_goalw_cterm []      (*NO quick_and_dirty_prove_goalw_cterm here!*)
476     (Thm.cterm_of thy (HOLogic.mk_Trueprop
477       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) \$ fp_fun)))
478     (fn _ => [rtac monoI 1, REPEAT (ares_tac (List.concat (map mk_mono monos) @ get_monos thy) 1)]));
481 (* prove introduction rules *)
483 fun prove_intrs coind mono fp_def intr_ts rec_sets_defs thy =
484   let
485     val _ = clean_message "  Proving the introduction rules ...";
487     val unfold = standard' (mono RS (fp_def RS
488       (if coind then def_gfp_unfold else def_lfp_unfold)));
490     fun select_disj 1 1 = []
491       | select_disj _ 1 = [rtac disjI1]
492       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
494     val intrs = map (fn (i, intr) => quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
495       (Thm.cterm_of thy intr) (fn prems =>
496        [(*insert prems and underlying sets*)
497        cut_facts_tac prems 1,
498        stac unfold 1,
499        REPEAT (resolve_tac [vimageI2, CollectI] 1),
500        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
501        EVERY1 (select_disj (length intr_ts) i),
502        (*Not ares_tac, since refl must be tried before any equality assumptions;
503          backtracking may occur if the premises have extra variables!*)
504        DEPTH_SOLVE_1 (resolve_tac [refl, exI, conjI] 1 APPEND assume_tac 1),
505        (*Now solve the equations like Inl 0 = Inl ?b2*)
506        REPEAT (rtac refl 1)])
507       |> rulify) (1 upto (length intr_ts) ~~ intr_ts)
509   in (intrs, unfold) end;
512 (* prove elimination rules *)
514 fun prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy =
515   let
516     val _ = clean_message "  Proving the elimination rules ...";
518     val rules1 = [CollectE, disjE, make_elim vimageD, exE];
519     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @ map make_elim [Inl_inject, Inr_inject];
520   in
521     mk_elims cs cTs params intr_ts intr_names |> map (fn (t, cases) =>
522       quick_and_dirty_prove_goalw_cterm thy rec_sets_defs
523         (Thm.cterm_of thy t) (fn prems =>
524           [cut_facts_tac [hd prems] 1,
525            dtac (unfold RS subst) 1,
526            REPEAT (FIRSTGOAL (eresolve_tac rules1)),
527            REPEAT (FIRSTGOAL (eresolve_tac rules2)),
528            EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))])
529         |> rulify
530         |> RuleCases.name cases)
531   end;
534 (* derivation of simplified elimination rules *)
536 local
538 (*cprop should have the form t:Si where Si is an inductive set*)
539 val mk_cases_err = "mk_cases: proposition not of form \"t : S_i\"";
541 (*delete needless equality assumptions*)
542 val refl_thin = prove_goal HOL.thy "!!P. a = a ==> P ==> P" (fn _ => [assume_tac 1]);
543 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
544 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
546 fun simp_case_tac solved ss i =
547   EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i
548   THEN_MAYBE (if solved then no_tac else all_tac);
550 in
552 fun mk_cases_i elims ss cprop =
553   let
554     val prem = Thm.assume cprop;
555     val tac = ALLGOALS (simp_case_tac false ss) THEN prune_params_tac;
556     fun mk_elim rl = Drule.standard (Tactic.rule_by_tactic tac (prem RS rl));
557   in
558     (case get_first (try mk_elim) elims of
559       SOME r => r
560     | NONE => error (Pretty.string_of (Pretty.block
561         [Pretty.str mk_cases_err, Pretty.fbrk, Display.pretty_cterm cprop])))
562   end;
564 fun mk_cases elims s =
565   mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.theory_of_thm (hd elims)) (s, propT));
567 fun smart_mk_cases thy ss cprop =
568   let
569     val c = #1 (Term.dest_Const (Term.head_of (#2 (HOLogic.dest_mem (HOLogic.dest_Trueprop
570       (Logic.strip_imp_concl (Thm.term_of cprop))))))) handle TERM _ => error mk_cases_err;
571     val (_, {elims, ...}) = the_inductive thy c;
572   in mk_cases_i elims ss cprop end;
574 end;
577 (* inductive_cases(_i) *)
579 fun gen_inductive_cases prep_att prep_prop args thy =
580   let
581     val cert_prop = Thm.cterm_of thy o prep_prop (ProofContext.init thy);
582     val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop;
584     val facts = args |> map (fn ((a, atts), props) =>
585      ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
586   in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end;
588 val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop;
589 val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
592 (* mk_cases_meth *)
594 fun mk_cases_meth (ctxt, raw_props) =
595   let
596     val thy = ProofContext.theory_of ctxt;
597     val ss = local_simpset_of ctxt;
598     val cprops = map (Thm.cterm_of thy o ProofContext.read_prop ctxt) raw_props;
599   in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
601 val mk_cases_args = Method.syntax (Scan.lift (Scan.repeat1 Args.name));
604 (* prove induction rule *)
606 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
607     fp_def rec_sets_defs thy =
608   let
609     val _ = clean_message "  Proving the induction rule ...";
611     val sum_case_rewrites =
612       (if Context.theory_name thy = "Datatype" then
613         PureThy.get_thms thy (Name "sum.cases")
614       else
615         (case ThyInfo.lookup_theory "Datatype" of
616           NONE => []
617         | SOME thy' => PureThy.get_thms thy' (Name "sum.cases")))
618       |> map mk_meta_eq;
620     val (preds, ind_prems, mutual_ind_concl, factors) =
621       mk_indrule cs cTs params intr_ts;
623     val dummy = if !trace then
624 		(writeln "ind_prems = ";
625 		 List.app (writeln o Sign.string_of_term thy) ind_prems)
626 	    else ();
628     (* make predicate for instantiation of abstract induction rule *)
630     fun mk_ind_pred _ [P] = P
631       | mk_ind_pred T Ps =
632          let val n = (length Ps) div 2;
633              val Type (_, [T1, T2]) = T
634          in Const ("Datatype.sum.sum_case",
635            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) \$
636              mk_ind_pred T1 (Library.take (n, Ps)) \$ mk_ind_pred T2 (Library.drop (n, Ps))
637          end;
639     val ind_pred = mk_ind_pred sumT preds;
641     val ind_concl = HOLogic.mk_Trueprop
642       (HOLogic.all_const sumT \$ Abs ("x", sumT, HOLogic.mk_binop "op -->"
643         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred \$ Bound 0)));
645     (* simplification rules for vimage and Collect *)
647     val vimage_simps = if length cs < 2 then [] else
648       map (fn c => quick_and_dirty_prove_goalw_cterm thy [] (Thm.cterm_of thy
649         (HOLogic.mk_Trueprop (HOLogic.mk_eq
650           (mk_vimage cs sumT (HOLogic.Collect_const sumT \$ ind_pred) c,
651            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) \$
652              List.nth (preds, find_index_eq c cs)))))
653         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites, rtac refl 1])) cs;
655     val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
657     val dummy = if !trace then
658 		(writeln "raw_fp_induct = "; print_thm raw_fp_induct)
659 	    else ();
661     val induct = quick_and_dirty_prove_goalw_cterm thy [inductive_conj_def] (Thm.cterm_of thy
662       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
663         [rtac (impI RS allI) 1,
664          DETERM (etac raw_fp_induct 1),
665          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
666          fold_goals_tac rec_sets_defs,
667          (*This CollectE and disjE separates out the introduction rules*)
668          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
669          (*Now break down the individual cases.  No disjE here in case
670            some premise involves disjunction.*)
671          REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac)),
672          ALLGOALS (simp_tac (HOL_basic_ss addsimps sum_case_rewrites)),
673          EVERY (map (fn prem =>
674    	             DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
676     val lemma = quick_and_dirty_prove_goalw_cterm thy rec_sets_defs (Thm.cterm_of thy
677       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
678         [cut_facts_tac prems 1,
679          REPEAT (EVERY
680            [REPEAT (resolve_tac [conjI, impI] 1),
681             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
682             rewrite_goals_tac sum_case_rewrites,
683             atac 1])])
685   in standard (split_rule factors (induct RS lemma)) end;
689 (** specification of (co)inductive sets **)
691 fun cond_declare_consts declare_consts cs paramTs cnames =
692   if declare_consts then
693     Theory.add_consts_i (map (fn (c, n) => (Sign.base_name n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
694   else I;
696 fun mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
697       params paramTs cTs cnames =
698   let
699     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
700     val setT = HOLogic.mk_setT sumT;
702     val fp_name = if coind then gfp_name else lfp_name;
704     val used = foldr add_term_names [] intr_ts;
705     val [sname, xname] = variantlist (["S", "x"], used);
707     (* transform an introduction rule into a conjunction  *)
708     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
709     (* is transformed into                                *)
710     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
712     fun transform_rule r =
713       let
714         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
715         val subst = subst_free
716           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
717         val Const ("op :", _) \$ t \$ u =
718           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
720       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
721         (foldr1 HOLogic.mk_conj
722           (((HOLogic.eq_const sumT) \$ Free (xname, sumT) \$ (mk_inj cs sumT u t))::
723             (map (subst o HOLogic.dest_Trueprop)
724               (Logic.strip_imp_prems r)))) frees
725       end
727     (* make a disjunction of all introduction rules *)
729     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) \$
730       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
732     (* add definiton of recursive sets to theory *)
734     val rec_name = if alt_name = "" then
735       space_implode "_" (map Sign.base_name cnames) else alt_name;
736     val full_rec_name = if length cs < 2 then hd cnames
737       else Sign.full_name thy rec_name;
739     val rec_const = list_comb
740       (Const (full_rec_name, paramTs ---> setT), params);
742     val fp_def_term = Logic.mk_equals (rec_const,
743       Const (fp_name, (setT --> setT) --> setT) \$ fp_fun);
745     val def_terms = fp_def_term :: (if length cs < 2 then [] else
746       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
748     val (thy', [fp_def :: rec_sets_defs]) =
749       thy
750       |> cond_declare_consts declare_consts cs paramTs cnames
751       |> (if length cs < 2 then I
752           else Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)])
753       |> Theory.add_path rec_name
754       |> PureThy.add_defss_i false [(("defs", def_terms), [])];
756     val mono = prove_mono setT fp_fun monos thy'
758   in (thy', mono, fp_def, rec_sets_defs, rec_const, sumT) end;
760 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
761     intros monos thy params paramTs cTs cnames induct_cases =
762   let
763     val _ =
764       if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
765         commas_quote (map Sign.base_name cnames)) else ();
767     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
769     val (thy1, mono, fp_def, rec_sets_defs, rec_const, sumT) =
770       mk_ind_def declare_consts alt_name coind cs intr_ts monos thy
771         params paramTs cTs cnames;
773     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts rec_sets_defs thy1;
774     val elims = if no_elim then [] else
775       prove_elims cs cTs params intr_ts intr_names unfold rec_sets_defs thy1;
776     val raw_induct = if no_ind then Drule.asm_rl else
777       if coind then standard (rule_by_tactic
778         (rewrite_tac [mk_meta_eq vimage_Un] THEN
779           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
780       else
781         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
782           rec_sets_defs thy1;
783     val induct =
784       if coind orelse no_ind orelse length cs > 1 then (raw_induct, [RuleCases.consumes 0])
785       else (raw_induct RSN (2, rev_mp), [RuleCases.consumes 1]);
787     val (thy2, intrs') =
788       thy1 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts);
789     val (thy3, ([intrs'', elims'], [induct'])) =
790       thy2
792         [(("intros", intrs'), []),
793           (("elims", elims), [RuleCases.consumes 1])]
795         [((coind_prefix coind ^ "induct", rulify (#1 induct)),
796          (RuleCases.case_names induct_cases :: #2 induct))]
797       |>> Theory.parent_path;
798   in (thy3,
799     {defs = fp_def :: rec_sets_defs,
800      mono = mono,
801      unfold = unfold,
802      intrs = intrs',
803      elims = elims',
804      mk_cases = mk_cases elims',
805      raw_induct = rulify raw_induct,
806      induct = induct'})
807   end;
810 (* external interfaces *)
812 fun try_term f msg thy t =
813   (case Library.try f t of
814     SOME x => x
815   | NONE => error (msg ^ Sign.string_of_term thy t));
817 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs pre_intros monos thy =
818   let
819     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
821     (*parameters should agree for all mutually recursive components*)
822     val (_, params) = strip_comb (hd cs);
823     val paramTs = map (try_term (snd o dest_Free) "Parameter in recursive\
824       \ component is not a free variable: " thy) params;
826     val cTs = map (try_term (HOLogic.dest_setT o fastype_of)
827       "Recursive component not of type set: " thy) cs;
829     val cnames = map (try_term (fst o dest_Const o head_of)
830       "Recursive set not previously declared as constant: " thy) cs;
832     val save_thy = thy
833       |> Theory.copy |> cond_declare_consts declare_consts cs paramTs cnames;
834     val intros = map (check_rule save_thy cs) pre_intros;
835     val induct_cases = map (#1 o #1) intros;
837     val (thy1, result as {elims, induct, ...}) =
838       add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs intros monos
839         thy params paramTs cTs cnames induct_cases;
840     val thy2 = thy1
841       |> put_inductives cnames ({names = cnames, coind = coind}, result)
842       |> add_cases_induct no_elim (no_ind orelse coind orelse length cs > 1)
843           cnames elims induct;
844   in (thy2, result) end;
846 fun add_inductive verbose coind c_strings intro_srcs raw_monos thy =
847   let
848     val cs = map (term_of o HOLogic.read_cterm thy) c_strings;
850     val intr_names = map (fst o fst) intro_srcs;
851     fun read_rule s = Thm.read_cterm thy (s, propT)
852       handle ERROR => error ("The error(s) above occurred for " ^ s);
853     val intr_ts = map (Thm.term_of o read_rule o snd o fst) intro_srcs;
854     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
855     val (cs', intr_ts') = unify_consts thy cs intr_ts;
857     val (thy', monos) = thy |> IsarThy.apply_theorems raw_monos;
858   in
859     add_inductive_i verbose false "" coind false false cs'
860       ((intr_names ~~ intr_ts') ~~ intr_atts) monos thy'
861   end;
865 (** package setup **)
867 (* setup theory *)
869 val setup =
870  [InductiveData.init,
871   Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
872     "dynamic case analysis on sets")],
873   Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
876 (* outer syntax *)
878 local structure P = OuterParse and K = OuterSyntax.Keyword in
880 fun mk_ind coind ((sets, intrs), monos) =
881   #1 o add_inductive true coind sets (map P.triple_swap intrs) monos;
883 fun ind_decl coind =
884   Scan.repeat1 P.term --
885   (P.\$\$\$ "intros" |--
886     P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) --
887   Scan.optional (P.\$\$\$ "monos" |-- P.!!! P.xthms1) []
888   >> (Toplevel.theory o mk_ind coind);
890 val inductiveP =
891   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
893 val coinductiveP =
894   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
897 val ind_cases =
898   P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop)
899   >> (Toplevel.theory o inductive_cases);
901 val inductive_casesP =
902   OuterSyntax.command "inductive_cases"
903     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
905 val _ = OuterSyntax.add_keywords ["intros", "monos"];
906 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
908 end;
910 end;