src/HOL/Tools/inductive_package.ML
 author wenzelm Tue Feb 29 23:06:20 2000 +0100 (2000-02-29) changeset 8316 74639e19eca0 parent 8312 b470bc28b59d child 8336 fdf3ac335f77 permissions -rw-r--r--
add_cases_induct: project_rules accomodates mutual induction;
1 (*  Title:      HOL/Tools/inductive_package.ML
2     ID:         \$Id\$
3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
4                 Stefan Berghofer,   TU Muenchen
5     Copyright   1994  University of Cambridge
6                 1998  TU Muenchen
8 (Co)Inductive Definition module for HOL.
10 Features:
11   * least or greatest fixedpoints
12   * user-specified product and sum constructions
13   * mutually recursive definitions
14   * definitions involving arbitrary monotone operators
15   * automatically proves introduction and elimination rules
17 The recursive sets must *already* be declared as constants in the
18 current theory!
20   Introduction rules have the form
21   [| ti:M(Sj), ..., P(x), ... |] ==> t: Sk
22   where M is some monotone operator (usually the identity)
23   P(x) is any side condition on the free variables
24   ti, t are any terms
25   Sj, Sk are two of the sets being defined in mutual recursion
27 Sums are used only for mutual recursion.  Products are used only to
28 derive "streamlined" induction rules for relations.
29 *)
31 signature INDUCTIVE_PACKAGE =
32 sig
33   val quiet_mode: bool ref
34   val unify_consts: Sign.sg -> term list -> term list -> term list * term list
35   val get_inductive: theory -> string ->
36     {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
37       induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
38   val print_inductives: theory -> unit
39   val mono_add_global: theory attribute
40   val mono_del_global: theory attribute
41   val get_monos: theory -> thm list
42   val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list ->
43     theory attribute list -> ((bstring * term) * theory attribute list) list ->
44       thm list -> thm list -> theory -> theory *
45       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
46        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
47   val add_inductive: bool -> bool -> string list -> Args.src list ->
48     ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list ->
49       (xstring * Args.src list) list -> theory -> theory *
50       {defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
51        intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
52   val inductive_cases: (((bstring * Args.src list) * xstring) * string list) * Comment.text
53     -> theory -> theory
54   val inductive_cases_i: (((bstring * theory attribute list) * string) * term list) * Comment.text
55     -> theory -> theory
56   val setup: (theory -> theory) list
57 end;
59 structure InductivePackage: INDUCTIVE_PACKAGE =
60 struct
62 (*** theory data ***)
64 (* data kind 'HOL/inductive' *)
66 type inductive_info =
67   {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm,
68     induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm};
70 structure InductiveArgs =
71 struct
72   val name = "HOL/inductive";
73   type T = inductive_info Symtab.table * thm list;
75   val empty = (Symtab.empty, []);
76   val copy = I;
77   val prep_ext = I;
78   fun merge ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2),
79     Library.generic_merge Thm.eq_thm I I monos1 monos2);
81   fun print sg (tab, monos) =
82     (Pretty.writeln (Pretty.strs ("(co)inductives:" ::
83        map #1 (Sign.cond_extern_table sg Sign.constK tab)));
84      Pretty.writeln (Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)));
85 end;
87 structure InductiveData = TheoryDataFun(InductiveArgs);
88 val print_inductives = InductiveData.print;
91 (* get and put data *)
93 fun get_inductive thy name =
94   (case Symtab.lookup (fst (InductiveData.get thy), name) of
95     Some info => info
96   | None => error ("Unknown (co)inductive set " ^ quote name));
98 fun put_inductives names info thy =
99   let
100     fun upd ((tab, monos), name) = (Symtab.update_new ((name, info), tab), monos);
101     val tab_monos = foldl upd (InductiveData.get thy, names)
102       handle Symtab.DUP name => error ("Duplicate definition of (co)inductive set " ^ quote name);
103   in InductiveData.put tab_monos thy end;
107 (** monotonicity rules **)
109 val get_monos = snd o InductiveData.get;
110 fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy;
112 fun mk_mono thm =
113   let
114     fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @
115       (case concl_of thm of
116           (_ \$ (_ \$ (Const ("Not", _) \$ _) \$ _)) => []
117         | _ => [standard (thm' RS (thm' RS eq_to_mono2))]);
118     val concl = concl_of thm
119   in
120     if Logic.is_equals concl then
121       eq2mono (thm RS meta_eq_to_obj_eq)
122     else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
123       eq2mono thm
124     else [thm]
125   end;
127 (* mono add/del *)
129 local
131 fun map_rules_global f thy = put_monos (f (get_monos thy)) thy;
133 fun add_mono thm rules = Library.gen_union Thm.eq_thm (mk_mono thm, rules);
134 fun del_mono thm rules = Library.gen_rems Thm.eq_thm (rules, mk_mono thm);
136 fun mk_att f g (x, thm) = (f (g thm) x, thm);
138 in
140 val mono_add_global = mk_att map_rules_global add_mono;
141 val mono_del_global = mk_att map_rules_global del_mono;
143 end;
146 (* concrete syntax *)
148 val monoN = "mono";
150 val delN = "del";
152 fun mono_att add del =
153   Attrib.syntax (Scan.lift (Args.\$\$\$ addN >> K add || Args.\$\$\$ delN >> K del || Scan.succeed add));
155 val mono_attr =
156   (mono_att mono_add_global mono_del_global, mono_att Attrib.undef_local_attribute Attrib.undef_local_attribute);
160 (** utilities **)
162 (* messages *)
164 val quiet_mode = ref false;
165 fun message s = if !quiet_mode then () else writeln s;
167 fun coind_prefix true = "co"
168   | coind_prefix false = "";
171 (* the following code ensures that each recursive set *)
172 (* always has the same type in all introduction rules *)
174 fun unify_consts sign cs intr_ts =
175   (let
176     val {tsig, ...} = Sign.rep_sg sign;
177     val add_term_consts_2 =
178       foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
179     fun varify (t, (i, ts)) =
180       let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
181       in (maxidx_of_term t', t'::ts) end;
182     val (i, cs') = foldr varify (cs, (~1, []));
183     val (i', intr_ts') = foldr varify (intr_ts, (i, []));
184     val rec_consts = foldl add_term_consts_2 ([], cs');
185     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
186     fun unify (env, (cname, cT)) =
187       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
188       in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
189           (env, (replicate (length consts) cT) ~~ consts)
190       end;
191     val (env, _) = foldl unify (([], i'), rec_consts);
192     fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T
193       in if T = T' then T else typ_subst_TVars_2 env T' end;
194     val subst = fst o Type.freeze_thaw o
195       (map_term_types (typ_subst_TVars_2 env))
197   in (map subst cs', map subst intr_ts')
198   end) handle Type.TUNIFY =>
199     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
202 (* misc *)
204 val Const _ \$ (vimage_f \$ _) \$ _ = HOLogic.dest_Trueprop (concl_of vimageD);
206 (*Delete needless equality assumptions*)
207 val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
208      (fn _ => [assume_tac 1]);
210 (*For simplifying the elimination rule*)
211 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
213 val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``";
214 val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
216 (* make injections needed in mutually recursive definitions *)
218 fun mk_inj cs sumT c x =
219   let
220     fun mk_inj' T n i =
221       if n = 1 then x else
222       let val n2 = n div 2;
223           val Type (_, [T1, T2]) = T
224       in
225         if i <= n2 then
226           Const ("Inl", T1 --> T) \$ (mk_inj' T1 n2 i)
227         else
228           Const ("Inr", T2 --> T) \$ (mk_inj' T2 (n - n2) (i - n2))
229       end
230   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
231   end;
233 (* make "vimage" terms for selecting out components of mutually rec.def. *)
235 fun mk_vimage cs sumT t c = if length cs < 2 then t else
236   let
237     val cT = HOLogic.dest_setT (fastype_of c);
238     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
239   in
240     Const (vimage_name, vimageT) \$
241       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) \$ t
242   end;
246 (** well-formedness checks **)
248 fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^
249   (Sign.string_of_term sign t) ^ "\n" ^ msg);
251 fun err_in_prem sign t p msg = error ("Ill-formed premise\n" ^
252   (Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^
253   (Sign.string_of_term sign t) ^ "\n" ^ msg);
255 val msg1 = "Conclusion of introduction rule must have form\
256           \ ' t : S_i '";
257 val msg2 = "Non-atomic premise";
258 val msg3 = "Recursion term on left of member symbol";
260 fun check_rule sign cs r =
261   let
262     fun check_prem prem = if can HOLogic.dest_Trueprop prem then ()
263       else err_in_prem sign r prem msg2;
265   in (case HOLogic.dest_Trueprop (Logic.strip_imp_concl r) of
266         (Const ("op :", _) \$ t \$ u) =>
267           if u mem cs then
268             if exists (Logic.occs o (rpair t)) cs then
269               err_in_rule sign r msg3
270             else
271               seq check_prem (Logic.strip_imp_prems r)
272           else err_in_rule sign r msg1
273       | _ => err_in_rule sign r msg1)
274   end;
276 fun try' f msg sign t = (case (try f t) of
277       Some x => x
278     | None => error (msg ^ Sign.string_of_term sign t));
282 (*** properties of (co)inductive sets ***)
284 (** elimination rules **)
286 fun mk_elims cs cTs params intr_ts =
287   let
288     val used = foldr add_term_names (intr_ts, []);
289     val [aname, pname] = variantlist (["a", "P"], used);
290     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
292     fun dest_intr r =
293       let val Const ("op :", _) \$ t \$ u =
294         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
295       in (u, t, Logic.strip_imp_prems r) end;
297     val intrs = map dest_intr intr_ts;
299     fun mk_elim (c, T) =
300       let
301         val a = Free (aname, T);
303         fun mk_elim_prem (_, t, ts) =
304           list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
305             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
306       in
307         Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
308           map mk_elim_prem (filter (equal c o #1) intrs), P)
309       end
310   in
311     map mk_elim (cs ~~ cTs)
312   end;
316 (** premises and conclusions of induction rules **)
318 fun mk_indrule cs cTs params intr_ts =
319   let
320     val used = foldr add_term_names (intr_ts, []);
322     (* predicates for induction rule *)
324     val preds = map Free (variantlist (if length cs < 2 then ["P"] else
325       map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
326         map (fn T => T --> HOLogic.boolT) cTs);
328     (* transform an introduction rule into a premise for induction rule *)
330     fun mk_ind_prem r =
331       let
332         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
334         val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
336         fun subst (s as ((m as Const ("op :", T)) \$ t \$ u)) =
337               (case pred_of u of
338                   None => (m \$ fst (subst t) \$ fst (subst u), None)
339                 | Some P => (HOLogic.conj \$ s \$ (P \$ t), Some (s, P \$ t)))
340           | subst s =
341               (case pred_of s of
342                   Some P => (HOLogic.mk_binop "op Int"
343                     (s, HOLogic.Collect_const (HOLogic.dest_setT
344                       (fastype_of s)) \$ P), None)
345                 | None => (case s of
346                      (t \$ u) => (fst (subst t) \$ fst (subst u), None)
347                    | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None)
348                    | _ => (s, None)));
350         fun mk_prem (s, prems) = (case subst s of
351               (_, Some (t, u)) => t :: u :: prems
352             | (t, _) => t :: prems);
354         val Const ("op :", _) \$ t \$ u =
355           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
357       in list_all_free (frees,
358            Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
359              (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
360                HOLogic.mk_Trueprop (the (pred_of u) \$ t)))
361       end;
363     val ind_prems = map mk_ind_prem intr_ts;
365     (* make conclusions for induction rules *)
367     fun mk_ind_concl ((c, P), (ts, x)) =
368       let val T = HOLogic.dest_setT (fastype_of c);
369           val Ts = HOLogic.prodT_factors T;
370           val (frees, x') = foldr (fn (T', (fs, s)) =>
371             ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
372           val tuple = HOLogic.mk_tuple T frees;
373       in ((HOLogic.mk_binop "op -->"
374         (HOLogic.mk_mem (tuple, c), P \$ tuple))::ts, x')
375       end;
377     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
378         (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
380   in (preds, ind_prems, mutual_ind_concl)
381   end;
385 (** prepare cases and induct rules **)
387 (*
388   transform mutual rule:
389     HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
390   into i-th projection:
391     xi:Ai ==> HH ==> Pi xi
392 *)
394 fun project_rules [name] rule = [(name, rule)]
395   | project_rules names mutual_rule =
396       let
397         val n = length names;
398         fun proj i =
399           (if i < n then (fn th => th RS conjunct1) else I)
400             (Library.funpow (i - 1) (fn th => th RS conjunct2) mutual_rule)
401             RS mp |> Thm.permute_prems 0 ~1 |> Drule.standard;
402       in names ~~ map proj (1 upto n) end;
404 fun add_cases_induct no_elim no_ind names elims induct =
405   let
406     val cases_specs =
407       if no_elim then []
408       else map2 (fn (name, elim) => (("", elim), [InductMethod.cases_set_global name]))
409         (names, elims);
411     val induct_specs =
412       if no_ind then []
413       else map (fn (name, th) => (("", th), [InductMethod.induct_set_global name]))
414         (project_rules names induct);
415   in PureThy.add_thms (cases_specs @ induct_specs) end;
419 (*** proofs for (co)inductive sets ***)
421 (** prove monotonicity **)
423 fun prove_mono setT fp_fun monos thy =
424   let
425     val _ = message "  Proving monotonicity ...";
427     val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
428       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) \$ fp_fun)))
429         (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)])
431   in mono end;
435 (** prove introduction rules **)
437 fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
438   let
439     val _ = message "  Proving the introduction rules ...";
441     val unfold = standard (mono RS (fp_def RS
442       (if coind then def_gfp_Tarski else def_lfp_Tarski)));
444     fun select_disj 1 1 = []
445       | select_disj _ 1 = [rtac disjI1]
446       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
448     val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
449       (cterm_of (Theory.sign_of thy) intr) (fn prems =>
450        [(*insert prems and underlying sets*)
451        cut_facts_tac prems 1,
452        stac unfold 1,
453        REPEAT (resolve_tac [vimageI2, CollectI] 1),
454        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
455        EVERY1 (select_disj (length intr_ts) i),
456        (*Not ares_tac, since refl must be tried before any equality assumptions;
457          backtracking may occur if the premises have extra variables!*)
458        DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
459        (*Now solve the equations like Inl 0 = Inl ?b2*)
460        rewrite_goals_tac con_defs,
461        REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts)
463   in (intrs, unfold) end;
467 (** prove elimination rules **)
469 fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =
470   let
471     val _ = message "  Proving the elimination rules ...";
473     val rules1 = [CollectE, disjE, make_elim vimageD, exE];
474     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @
475       map make_elim [Inl_inject, Inr_inject];
477     val elims = map (fn t => prove_goalw_cterm rec_sets_defs
478       (cterm_of (Theory.sign_of thy) t) (fn prems =>
479         [cut_facts_tac [hd prems] 1,
480          dtac (unfold RS subst) 1,
481          REPEAT (FIRSTGOAL (eresolve_tac rules1)),
482          REPEAT (FIRSTGOAL (eresolve_tac rules2)),
483          EVERY (map (fn prem =>
484            DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]))
485       (mk_elims cs cTs params intr_ts)
487   in elims end;
490 (** derivation of simplified elimination rules **)
492 (*Applies freeness of the given constructors, which *must* be unfolded by
493   the given defs.  Cannot simply use the local con_defs because con_defs=[]
494   for inference systems.
495  *)
496 fun con_elim_tac ss =
497   let val elim_tac = REPEAT o (eresolve_tac elim_rls)
498   in ALLGOALS(EVERY'[elim_tac,
499 		     asm_full_simp_tac ss,
500 		     elim_tac,
501 		     REPEAT o bound_hyp_subst_tac])
502      THEN prune_params_tac
503   end;
505 (*cprop should have the form t:Si where Si is an inductive set*)
506 fun mk_cases_i elims ss cprop =
507   let
508     val prem = Thm.assume cprop;
509     fun mk_elim rl = standard (rule_by_tactic (con_elim_tac ss) (prem RS rl));
510   in
511     (case get_first (try mk_elim) elims of
512       Some r => r
513     | None => error (Pretty.string_of (Pretty.block
514         [Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk,
515           Display.pretty_cterm cprop])))
516   end;
518 fun mk_cases elims s =
519   mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
522 (* inductive_cases(_i) *)
524 fun gen_inductive_cases prep_att prep_const prep_prop
525     ((((name, raw_atts), raw_set), raw_props), comment) thy =
526   let
527     val sign = Theory.sign_of thy;
529     val atts = map (prep_att thy) raw_atts;
530     val (_, {elims, ...}) = get_inductive thy (prep_const sign raw_set);
531     val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
532     val thms = map (mk_cases_i elims (Simplifier.simpset_of thy)) cprops;
533   in
534     thy
535     |> IsarThy.have_theorems_i (((name, atts), map Thm.no_attributes thms), comment)
536   end;
538 val inductive_cases =
539   gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
541 val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop;
545 (** prove induction rule **)
547 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
548     fp_def rec_sets_defs thy =
549   let
550     val _ = message "  Proving the induction rule ...";
552     val sign = Theory.sign_of thy;
554     val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
555         None => []
556       | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
558     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
560     (* make predicate for instantiation of abstract induction rule *)
562     fun mk_ind_pred _ [P] = P
563       | mk_ind_pred T Ps =
564          let val n = (length Ps) div 2;
565              val Type (_, [T1, T2]) = T
566          in Const ("Datatype.sum.sum_case",
567            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) \$
568              mk_ind_pred T1 (take (n, Ps)) \$ mk_ind_pred T2 (drop (n, Ps))
569          end;
571     val ind_pred = mk_ind_pred sumT preds;
573     val ind_concl = HOLogic.mk_Trueprop
574       (HOLogic.all_const sumT \$ Abs ("x", sumT, HOLogic.mk_binop "op -->"
575         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred \$ Bound 0)));
577     (* simplification rules for vimage and Collect *)
579     val vimage_simps = if length cs < 2 then [] else
580       map (fn c => prove_goalw_cterm [] (cterm_of sign
581         (HOLogic.mk_Trueprop (HOLogic.mk_eq
582           (mk_vimage cs sumT (HOLogic.Collect_const sumT \$ ind_pred) c,
583            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) \$
584              nth_elem (find_index_eq c cs, preds)))))
585         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites,
586           rtac refl 1])) cs;
588     val induct = prove_goalw_cterm [] (cterm_of sign
589       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
590         [rtac (impI RS allI) 1,
591          DETERM (etac (mono RS (fp_def RS def_induct)) 1),
592          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
593          fold_goals_tac rec_sets_defs,
594          (*This CollectE and disjE separates out the introduction rules*)
595          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
596          (*Now break down the individual cases.  No disjE here in case
597            some premise involves disjunction.*)
598          REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
599          rewrite_goals_tac sum_case_rewrites,
600          EVERY (map (fn prem =>
601            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
603     val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
604       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
605         [cut_facts_tac prems 1,
606          REPEAT (EVERY
607            [REPEAT (resolve_tac [conjI, impI] 1),
608             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
609             rewrite_goals_tac sum_case_rewrites,
610             atac 1])])
612   in standard (split_rule (induct RS lemma))
613   end;
617 (*** specification of (co)inductive sets ****)
619 (** definitional introduction of (co)inductive sets **)
621 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
622     atts intros monos con_defs thy params paramTs cTs cnames =
623   let
624     val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
625       commas_quote cnames) else ();
627     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
628     val setT = HOLogic.mk_setT sumT;
630     val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
631       else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";
633     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
635     val used = foldr add_term_names (intr_ts, []);
636     val [sname, xname] = variantlist (["S", "x"], used);
638     (* transform an introduction rule into a conjunction  *)
639     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
640     (* is transformed into                                *)
641     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
643     fun transform_rule r =
644       let
645         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
646         val subst = subst_free
647           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
648         val Const ("op :", _) \$ t \$ u =
649           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
651       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
652         (frees, foldr1 HOLogic.mk_conj
653           (((HOLogic.eq_const sumT) \$ Free (xname, sumT) \$ (mk_inj cs sumT u t))::
654             (map (subst o HOLogic.dest_Trueprop)
655               (Logic.strip_imp_prems r))))
656       end
658     (* make a disjunction of all introduction rules *)
660     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) \$
661       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
663     (* add definiton of recursive sets to theory *)
665     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
666     val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
668     val rec_const = list_comb
669       (Const (full_rec_name, paramTs ---> setT), params);
671     val fp_def_term = Logic.mk_equals (rec_const,
672       Const (fp_name, (setT --> setT) --> setT) \$ fp_fun)
674     val def_terms = fp_def_term :: (if length cs < 2 then [] else
675       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
677     val thy' = thy |>
678       (if declare_consts then
679         Theory.add_consts_i (map (fn (c, n) =>
680           (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
681        else I) |>
682       (if length cs < 2 then I else
683        Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)]) |>
684       Theory.add_path rec_name |>
685       PureThy.add_defss_i [(("defs", def_terms), [])];
687     (* get definitions from theory *)
689     val fp_def::rec_sets_defs = PureThy.get_thms thy' "defs";
691     (* prove and store theorems *)
693     val mono = prove_mono setT fp_fun monos thy';
694     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
695       rec_sets_defs thy';
696     val elims = if no_elim then [] else
697       prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';
698     val raw_induct = if no_ind then Drule.asm_rl else
699       if coind then standard (rule_by_tactic
700         (rewrite_tac [mk_meta_eq vimage_Un] THEN
701           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
702       else
703         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
704           rec_sets_defs thy';
705     val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
706       else standard (raw_induct RSN (2, rev_mp));
708     val thy'' = thy'
709       |> PureThy.add_thmss [(("intrs", intrs), atts)]
710       |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
711       |> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])])
712       |> (if no_ind then I else PureThy.add_thms
713         [((coind_prefix coind ^ "induct", induct), [])])
714       |> Theory.parent_path;
715     val intrs' = PureThy.get_thms thy'' "intrs";
716     val elims' = if no_elim then elims else PureThy.get_thms thy'' "elims";  (* FIXME improve *)
717     val induct' = if no_ind then induct else PureThy.get_thm thy'' (coind_prefix coind ^ "induct");  (* FIXME improve *)
718   in (thy'',
719     {defs = fp_def::rec_sets_defs,
720      mono = mono,
721      unfold = unfold,
722      intrs = intrs',
723      elims = elims',
724      mk_cases = mk_cases elims',
725      raw_induct = raw_induct,
726      induct = induct'})
727   end;
731 (** axiomatic introduction of (co)inductive sets **)
733 fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
734     atts intros monos con_defs thy params paramTs cTs cnames =
735   let
736     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
738     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
739     val elim_ts = mk_elims cs cTs params intr_ts;
741     val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
742     val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
744     val thy' = thy
745       |> (if declare_consts then
747               (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
748          else I)
749       |> Theory.add_path rec_name
750       |> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("elims", elim_ts), [])]
751       |> (if coind then I else
752             PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
754     val intrs = PureThy.get_thms thy' "intrs";
755     val elims = PureThy.get_thms thy' "elims";
756     val raw_induct = if coind then Drule.asm_rl else PureThy.get_thm thy' "raw_induct";
757     val induct = if coind orelse length cs > 1 then raw_induct
758       else standard (raw_induct RSN (2, rev_mp));
760     val thy'' =
761       thy'
762       |> (if coind then I else PureThy.add_thms [(("induct", induct), [])])
763       |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
764       |> Theory.parent_path;
765     val induct' = if coind then raw_induct else PureThy.get_thm thy'' "induct";
766   in (thy'',
767     {defs = [],
768      mono = Drule.asm_rl,
769      unfold = Drule.asm_rl,
770      intrs = intrs,
771      elims = elims,
772      mk_cases = mk_cases elims,
773      raw_induct = raw_induct,
774      induct = induct'})
775   end;
779 (** introduction of (co)inductive sets **)
781 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
782     atts intros monos con_defs thy =
783   let
784     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
785     val sign = Theory.sign_of thy;
787     (*parameters should agree for all mutually recursive components*)
788     val (_, params) = strip_comb (hd cs);
789     val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\
790       \ component is not a free variable: " sign) params;
792     val cTs = map (try' (HOLogic.dest_setT o fastype_of)
793       "Recursive component not of type set: " sign) cs;
795     val full_cnames = map (try' (fst o dest_Const o head_of)
796       "Recursive set not previously declared as constant: " sign) cs;
797     val cnames = map Sign.base_name full_cnames;
799     val _ = seq (check_rule sign cs o snd o fst) intros;
801     val (thy1, result) =
802       (if ! quick_and_dirty then add_ind_axm else add_ind_def)
803         verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
804         con_defs thy params paramTs cTs cnames;
805     val thy2 = thy1
806       |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result)
807       |> add_cases_induct no_elim no_ind full_cnames (#elims result) (#induct result);
808   in (thy2, result) end;
812 (** external interface **)
814 fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
815   let
816     val sign = Theory.sign_of thy;
817     val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
819     val atts = map (Attrib.global_attribute thy) srcs;
820     val intr_names = map (fst o fst) intro_srcs;
821     val intr_ts = map (term_of o Thm.read_cterm sign o rpair propT o snd o fst) intro_srcs;
822     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
823     val (cs', intr_ts') = unify_consts sign cs intr_ts;
825     val ((thy', con_defs), monos) = thy
826       |> IsarThy.apply_theorems raw_monos
827       |> apfst (IsarThy.apply_theorems raw_con_defs);
828   in
829     add_inductive_i verbose false "" coind false false cs'
830       atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
831   end;
835 (** package setup **)
837 (* setup theory *)
839 val setup = [InductiveData.init,
840              Attrib.add_attributes [(monoN, mono_attr, "monotonicity rule")]];
843 (* outer syntax *)
845 local structure P = OuterParse and K = OuterSyntax.Keyword in
847 fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
848   #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
850 fun ind_decl coind =
851   (Scan.repeat1 P.term --| P.marg_comment) --
852   (P.\$\$\$ "intrs" |--
853     P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
854   Scan.optional (P.\$\$\$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
855   Scan.optional (P.\$\$\$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
856   >> (Toplevel.theory o mk_ind coind);
858 val inductiveP =
859   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
861 val coinductiveP =
862   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
865 val ind_cases =
866   P.opt_thm_name "=" -- P.xname --| P.\$\$\$ ":" -- Scan.repeat1 P.prop -- P.marg_comment
867   >> (Toplevel.theory o inductive_cases);
869 val inductive_casesP =
870   OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules"
871     K.thy_decl ind_cases;
873 val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"];
874 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
876 end;
879 end;