src/HOL/Tools/inductive_package.ML
 author wenzelm Wed Jan 05 11:56:04 2000 +0100 (2000-01-05) changeset 8100 6186ee807f2e parent 7798 42e94b618f34 child 8277 493707fcd8a6 permissions -rw-r--r--
replaced HOLogic.termTVar by HOLogic.termT;
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;
105 val get_monos = snd o InductiveData.get;
107 fun put_monos thms thy = InductiveData.put (fst (InductiveData.get thy), thms) thy;
109 (** monotonicity rules **)
111 fun mk_mono thm =
112   let
113     fun eq2mono thm' = [standard (thm' RS (thm' RS eq_to_mono))] @
114       (case concl_of thm of
115           (_ \$ (_ \$ (Const ("Not", _) \$ _) \$ _)) => []
116         | _ => [standard (thm' RS (thm' RS eq_to_mono2))]);
117     val concl = concl_of thm
118   in
119     if Logic.is_equals concl then
120       eq2mono (thm RS meta_eq_to_obj_eq)
121     else if can (HOLogic.dest_eq o HOLogic.dest_Trueprop) concl then
122       eq2mono thm
123     else [thm]
124   end;
126 (* mono add/del *)
128 local
130 fun map_rules_global f thy = put_monos (f (get_monos thy)) thy;
132 fun add_mono thm rules = Library.gen_union Thm.eq_thm (mk_mono thm, rules);
133 fun del_mono thm rules = Library.gen_rems Thm.eq_thm (rules, mk_mono thm);
135 fun mk_att f g (x, thm) = (f (g thm) x, thm);
137 in
139 val mono_add_global = mk_att map_rules_global add_mono;
140 val mono_del_global = mk_att map_rules_global del_mono;
142 end;
145 (* concrete syntax *)
147 val monoN = "mono";
149 val delN = "del";
151 fun mono_att add del =
152   Attrib.syntax (Scan.lift (Args.\$\$\$ addN >> K add || Args.\$\$\$ delN >> K del || Scan.succeed add));
154 val mono_attr =
155   (mono_att mono_add_global mono_del_global, mono_att Attrib.undef_local_attribute Attrib.undef_local_attribute);
159 (** utilities **)
161 (* messages *)
163 val quiet_mode = ref false;
164 fun message s = if !quiet_mode then () else writeln s;
166 fun coind_prefix true = "co"
167   | coind_prefix false = "";
170 (* the following code ensures that each recursive set *)
171 (* always has the same type in all introduction rules *)
173 fun unify_consts sign cs intr_ts =
174   (let
175     val {tsig, ...} = Sign.rep_sg sign;
176     val add_term_consts_2 =
177       foldl_aterms (fn (cs, Const c) => c ins cs | (cs, _) => cs);
178     fun varify (t, (i, ts)) =
179       let val t' = map_term_types (incr_tvar (i + 1)) (Type.varify (t, []))
180       in (maxidx_of_term t', t'::ts) end;
181     val (i, cs') = foldr varify (cs, (~1, []));
182     val (i', intr_ts') = foldr varify (intr_ts, (i, []));
183     val rec_consts = foldl add_term_consts_2 ([], cs');
184     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
185     fun unify (env, (cname, cT)) =
186       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
187       in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
188           (env, (replicate (length consts) cT) ~~ consts)
189       end;
190     val (env, _) = foldl unify (([], i'), rec_consts);
191     fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T
192       in if T = T' then T else typ_subst_TVars_2 env T' end;
193     val subst = fst o Type.freeze_thaw o
194       (map_term_types (typ_subst_TVars_2 env))
196   in (map subst cs', map subst intr_ts')
197   end) handle Type.TUNIFY =>
198     (warning "Occurrences of recursive constant have non-unifiable types"; (cs, intr_ts));
201 (* misc *)
203 val Const _ \$ (vimage_f \$ _) \$ _ = HOLogic.dest_Trueprop (concl_of vimageD);
205 (*Delete needless equality assumptions*)
206 val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
207      (fn _ => [assume_tac 1]);
209 (*For simplifying the elimination rule*)
210 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
212 val vimage_name = Sign.intern_const (Theory.sign_of Vimage.thy) "op -``";
213 val mono_name = Sign.intern_const (Theory.sign_of Ord.thy) "mono";
215 (* make injections needed in mutually recursive definitions *)
217 fun mk_inj cs sumT c x =
218   let
219     fun mk_inj' T n i =
220       if n = 1 then x else
221       let val n2 = n div 2;
222           val Type (_, [T1, T2]) = T
223       in
224         if i <= n2 then
225           Const ("Inl", T1 --> T) \$ (mk_inj' T1 n2 i)
226         else
227           Const ("Inr", T2 --> T) \$ (mk_inj' T2 (n - n2) (i - n2))
228       end
229   in mk_inj' sumT (length cs) (1 + find_index_eq c cs)
230   end;
232 (* make "vimage" terms for selecting out components of mutually rec.def. *)
234 fun mk_vimage cs sumT t c = if length cs < 2 then t else
235   let
236     val cT = HOLogic.dest_setT (fastype_of c);
237     val vimageT = [cT --> sumT, HOLogic.mk_setT sumT] ---> HOLogic.mk_setT cT
238   in
239     Const (vimage_name, vimageT) \$
240       Abs ("y", cT, mk_inj cs sumT c (Bound 0)) \$ t
241   end;
245 (** well-formedness checks **)
247 fun err_in_rule sign t msg = error ("Ill-formed introduction rule\n" ^
248   (Sign.string_of_term sign t) ^ "\n" ^ msg);
250 fun err_in_prem sign t p msg = error ("Ill-formed premise\n" ^
251   (Sign.string_of_term sign p) ^ "\nin introduction rule\n" ^
252   (Sign.string_of_term sign t) ^ "\n" ^ msg);
254 val msg1 = "Conclusion of introduction rule must have form\
255           \ ' t : S_i '";
256 val msg2 = "Non-atomic premise";
257 val msg3 = "Recursion term on left of member symbol";
259 fun check_rule sign cs r =
260   let
261     fun check_prem prem = if can HOLogic.dest_Trueprop prem then ()
262       else err_in_prem sign r prem msg2;
264   in (case HOLogic.dest_Trueprop (Logic.strip_imp_concl r) of
265         (Const ("op :", _) \$ t \$ u) =>
266           if u mem cs then
267             if exists (Logic.occs o (rpair t)) cs then
268               err_in_rule sign r msg3
269             else
270               seq check_prem (Logic.strip_imp_prems r)
271           else err_in_rule sign r msg1
272       | _ => err_in_rule sign r msg1)
273   end;
275 fun try' f msg sign t = (case (try f t) of
276       Some x => x
277     | None => error (msg ^ Sign.string_of_term sign t));
281 (*** properties of (co)inductive sets ***)
283 (** elimination rules **)
285 fun mk_elims cs cTs params intr_ts =
286   let
287     val used = foldr add_term_names (intr_ts, []);
288     val [aname, pname] = variantlist (["a", "P"], used);
289     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
291     fun dest_intr r =
292       let val Const ("op :", _) \$ t \$ u =
293         HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
294       in (u, t, Logic.strip_imp_prems r) end;
296     val intrs = map dest_intr intr_ts;
298     fun mk_elim (c, T) =
299       let
300         val a = Free (aname, T);
302         fun mk_elim_prem (_, t, ts) =
303           list_all_free (map dest_Free ((foldr add_term_frees (t::ts, [])) \\ params),
304             Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (a, t)) :: ts, P));
305       in
306         Logic.list_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (a, c)) ::
307           map mk_elim_prem (filter (equal c o #1) intrs), P)
308       end
309   in
310     map mk_elim (cs ~~ cTs)
311   end;
315 (** premises and conclusions of induction rules **)
317 fun mk_indrule cs cTs params intr_ts =
318   let
319     val used = foldr add_term_names (intr_ts, []);
321     (* predicates for induction rule *)
323     val preds = map Free (variantlist (if length cs < 2 then ["P"] else
324       map (fn i => "P" ^ string_of_int i) (1 upto length cs), used) ~~
325         map (fn T => T --> HOLogic.boolT) cTs);
327     (* transform an introduction rule into a premise for induction rule *)
329     fun mk_ind_prem r =
330       let
331         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
333         val pred_of = curry (Library.gen_assoc (op aconv)) (cs ~~ preds);
335         fun subst (s as ((m as Const ("op :", T)) \$ t \$ u)) =
336               (case pred_of u of
337                   None => (m \$ fst (subst t) \$ fst (subst u), None)
338                 | Some P => (HOLogic.conj \$ s \$ (P \$ t), Some (s, P \$ t)))
339           | subst s =
340               (case pred_of s of
341                   Some P => (HOLogic.mk_binop "op Int"
342                     (s, HOLogic.Collect_const (HOLogic.dest_setT
343                       (fastype_of s)) \$ P), None)
344                 | None => (case s of
345                      (t \$ u) => (fst (subst t) \$ fst (subst u), None)
346                    | (Abs (a, T, t)) => (Abs (a, T, fst (subst t)), None)
347                    | _ => (s, None)));
349         fun mk_prem (s, prems) = (case subst s of
350               (_, Some (t, u)) => t :: u :: prems
351             | (t, _) => t :: prems);
353         val Const ("op :", _) \$ t \$ u =
354           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
356       in list_all_free (frees,
357            Logic.list_implies (map HOLogic.mk_Trueprop (foldr mk_prem
358              (map HOLogic.dest_Trueprop (Logic.strip_imp_prems r), [])),
359                HOLogic.mk_Trueprop (the (pred_of u) \$ t)))
360       end;
362     val ind_prems = map mk_ind_prem intr_ts;
364     (* make conclusions for induction rules *)
366     fun mk_ind_concl ((c, P), (ts, x)) =
367       let val T = HOLogic.dest_setT (fastype_of c);
368           val Ts = HOLogic.prodT_factors T;
369           val (frees, x') = foldr (fn (T', (fs, s)) =>
370             ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x));
371           val tuple = HOLogic.mk_tuple T frees;
372       in ((HOLogic.mk_binop "op -->"
373         (HOLogic.mk_mem (tuple, c), P \$ tuple))::ts, x')
374       end;
376     val mutual_ind_concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
377         (fst (foldr mk_ind_concl (cs ~~ preds, ([], "xa")))))
379   in (preds, ind_prems, mutual_ind_concl)
380   end;
384 (*** proofs for (co)inductive sets ***)
386 (** prove monotonicity **)
388 fun prove_mono setT fp_fun monos thy =
389   let
390     val _ = message "  Proving monotonicity ...";
392     val mono = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy) (HOLogic.mk_Trueprop
393       (Const (mono_name, (setT --> setT) --> HOLogic.boolT) \$ fp_fun)))
394         (fn _ => [rtac monoI 1, REPEAT (ares_tac (get_monos thy @ flat (map mk_mono monos)) 1)])
396   in mono end;
400 (** prove introduction rules **)
402 fun prove_intrs coind mono fp_def intr_ts con_defs rec_sets_defs thy =
403   let
404     val _ = message "  Proving the introduction rules ...";
406     val unfold = standard (mono RS (fp_def RS
407       (if coind then def_gfp_Tarski else def_lfp_Tarski)));
409     fun select_disj 1 1 = []
410       | select_disj _ 1 = [rtac disjI1]
411       | select_disj n i = (rtac disjI2)::(select_disj (n - 1) (i - 1));
413     val intrs = map (fn (i, intr) => prove_goalw_cterm rec_sets_defs
414       (cterm_of (Theory.sign_of thy) intr) (fn prems =>
415        [(*insert prems and underlying sets*)
416        cut_facts_tac prems 1,
417        stac unfold 1,
418        REPEAT (resolve_tac [vimageI2, CollectI] 1),
419        (*Now 1-2 subgoals: the disjunction, perhaps equality.*)
420        EVERY1 (select_disj (length intr_ts) i),
421        (*Not ares_tac, since refl must be tried before any equality assumptions;
422          backtracking may occur if the premises have extra variables!*)
423        DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 1 APPEND assume_tac 1),
424        (*Now solve the equations like Inl 0 = Inl ?b2*)
425        rewrite_goals_tac con_defs,
426        REPEAT (rtac refl 1)])) (1 upto (length intr_ts) ~~ intr_ts)
428   in (intrs, unfold) end;
432 (** prove elimination rules **)
434 fun prove_elims cs cTs params intr_ts unfold rec_sets_defs thy =
435   let
436     val _ = message "  Proving the elimination rules ...";
438     val rules1 = [CollectE, disjE, make_elim vimageD, exE];
439     val rules2 = [conjE, Inl_neq_Inr, Inr_neq_Inl] @
440       map make_elim [Inl_inject, Inr_inject];
442     val elims = map (fn t => prove_goalw_cterm rec_sets_defs
443       (cterm_of (Theory.sign_of thy) t) (fn prems =>
444         [cut_facts_tac [hd prems] 1,
445          dtac (unfold RS subst) 1,
446          REPEAT (FIRSTGOAL (eresolve_tac rules1)),
447          REPEAT (FIRSTGOAL (eresolve_tac rules2)),
448          EVERY (map (fn prem =>
449            DEPTH_SOLVE_1 (ares_tac [prem, conjI] 1)) (tl prems))]))
450       (mk_elims cs cTs params intr_ts)
452   in elims end;
455 (** derivation of simplified elimination rules **)
457 (*Applies freeness of the given constructors, which *must* be unfolded by
458   the given defs.  Cannot simply use the local con_defs because con_defs=[]
459   for inference systems.
460  *)
461 fun con_elim_tac ss =
462   let val elim_tac = REPEAT o (eresolve_tac elim_rls)
463   in ALLGOALS(EVERY'[elim_tac,
464 		     asm_full_simp_tac ss,
465 		     elim_tac,
466 		     REPEAT o bound_hyp_subst_tac])
467      THEN prune_params_tac
468   end;
470 (*cprop should have the form t:Si where Si is an inductive set*)
471 fun mk_cases_i elims ss cprop =
472   let
473     val prem = Thm.assume cprop;
474     fun mk_elim rl = standard (rule_by_tactic (con_elim_tac ss) (prem RS rl));
475   in
476     (case get_first (try mk_elim) elims of
477       Some r => r
478     | None => error (Pretty.string_of (Pretty.block
479         [Pretty.str "mk_cases: proposition not of form 't : S_i'", Pretty.fbrk,
480           Display.pretty_cterm cprop])))
481   end;
483 fun mk_cases elims s =
484   mk_cases_i elims (simpset()) (Thm.read_cterm (Thm.sign_of_thm (hd elims)) (s, propT));
487 (* inductive_cases(_i) *)
489 fun gen_inductive_cases prep_att prep_const prep_prop
490     ((((name, raw_atts), raw_set), raw_props), comment) thy =
491   let
492     val sign = Theory.sign_of thy;
494     val atts = map (prep_att thy) raw_atts;
495     val (_, {elims, ...}) = get_inductive thy (prep_const sign raw_set);
496     val cprops = map (Thm.cterm_of sign o prep_prop (ProofContext.init thy)) raw_props;
497     val thms = map (mk_cases_i elims (Simplifier.simpset_of thy)) cprops;
498   in
499     thy
500     |> IsarThy.have_theorems_i (((name, atts), map Thm.no_attributes thms), comment)
501   end;
503 val inductive_cases =
504   gen_inductive_cases Attrib.global_attribute Sign.intern_const ProofContext.read_prop;
506 val inductive_cases_i = gen_inductive_cases (K I) (K I) ProofContext.cert_prop;
510 (** prove induction rule **)
512 fun prove_indrule cs cTs sumT rec_const params intr_ts mono
513     fp_def rec_sets_defs thy =
514   let
515     val _ = message "  Proving the induction rule ...";
517     val sign = Theory.sign_of thy;
519     val sum_case_rewrites = (case ThyInfo.lookup_theory "Datatype" of
520         None => []
521       | Some thy' => map mk_meta_eq (PureThy.get_thms thy' "sum.cases"));
523     val (preds, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
525     (* make predicate for instantiation of abstract induction rule *)
527     fun mk_ind_pred _ [P] = P
528       | mk_ind_pred T Ps =
529          let val n = (length Ps) div 2;
530              val Type (_, [T1, T2]) = T
531          in Const ("Datatype.sum.sum_case",
532            [T1 --> HOLogic.boolT, T2 --> HOLogic.boolT, T] ---> HOLogic.boolT) \$
533              mk_ind_pred T1 (take (n, Ps)) \$ mk_ind_pred T2 (drop (n, Ps))
534          end;
536     val ind_pred = mk_ind_pred sumT preds;
538     val ind_concl = HOLogic.mk_Trueprop
539       (HOLogic.all_const sumT \$ Abs ("x", sumT, HOLogic.mk_binop "op -->"
540         (HOLogic.mk_mem (Bound 0, rec_const), ind_pred \$ Bound 0)));
542     (* simplification rules for vimage and Collect *)
544     val vimage_simps = if length cs < 2 then [] else
545       map (fn c => prove_goalw_cterm [] (cterm_of sign
546         (HOLogic.mk_Trueprop (HOLogic.mk_eq
547           (mk_vimage cs sumT (HOLogic.Collect_const sumT \$ ind_pred) c,
548            HOLogic.Collect_const (HOLogic.dest_setT (fastype_of c)) \$
549              nth_elem (find_index_eq c cs, preds)))))
550         (fn _ => [rtac vimage_Collect 1, rewrite_goals_tac sum_case_rewrites,
551           rtac refl 1])) cs;
553     val induct = prove_goalw_cterm [] (cterm_of sign
554       (Logic.list_implies (ind_prems, ind_concl))) (fn prems =>
555         [rtac (impI RS allI) 1,
556          DETERM (etac (mono RS (fp_def RS def_induct)) 1),
557          rewrite_goals_tac (map mk_meta_eq (vimage_Int::Int_Collect::vimage_simps)),
558          fold_goals_tac rec_sets_defs,
559          (*This CollectE and disjE separates out the introduction rules*)
560          REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE, exE])),
561          (*Now break down the individual cases.  No disjE here in case
562            some premise involves disjunction.*)
563          REPEAT (FIRSTGOAL (etac conjE ORELSE' hyp_subst_tac)),
564          rewrite_goals_tac sum_case_rewrites,
565          EVERY (map (fn prem =>
566            DEPTH_SOLVE_1 (ares_tac [prem, conjI, refl] 1)) prems)]);
568     val lemma = prove_goalw_cterm rec_sets_defs (cterm_of sign
569       (Logic.mk_implies (ind_concl, mutual_ind_concl))) (fn prems =>
570         [cut_facts_tac prems 1,
571          REPEAT (EVERY
572            [REPEAT (resolve_tac [conjI, impI] 1),
573             TRY (dtac vimageD 1), etac allE 1, dtac mp 1, atac 1,
574             rewrite_goals_tac sum_case_rewrites,
575             atac 1])])
577   in standard (split_rule (induct RS lemma))
578   end;
582 (*** specification of (co)inductive sets ****)
584 (** definitional introduction of (co)inductive sets **)
586 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs
587     atts intros monos con_defs thy params paramTs cTs cnames =
588   let
589     val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^
590       commas_quote cnames) else ();
592     val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs;
593     val setT = HOLogic.mk_setT sumT;
595     val fp_name = if coind then Sign.intern_const (Theory.sign_of Gfp.thy) "gfp"
596       else Sign.intern_const (Theory.sign_of Lfp.thy) "lfp";
598     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
600     val used = foldr add_term_names (intr_ts, []);
601     val [sname, xname] = variantlist (["S", "x"], used);
603     (* transform an introduction rule into a conjunction  *)
604     (*   [| t : ... S_i ... ; ... |] ==> u : S_j          *)
605     (* is transformed into                                *)
606     (*   x = Inj_j u & t : ... Inj_i -`` S ... & ...      *)
608     fun transform_rule r =
609       let
610         val frees = map dest_Free ((add_term_frees (r, [])) \\ params);
611         val subst = subst_free
612           (cs ~~ (map (mk_vimage cs sumT (Free (sname, setT))) cs));
613         val Const ("op :", _) \$ t \$ u =
614           HOLogic.dest_Trueprop (Logic.strip_imp_concl r)
616       in foldr (fn ((x, T), P) => HOLogic.mk_exists (x, T, P))
617         (frees, foldr1 HOLogic.mk_conj
618           (((HOLogic.eq_const sumT) \$ Free (xname, sumT) \$ (mk_inj cs sumT u t))::
619             (map (subst o HOLogic.dest_Trueprop)
620               (Logic.strip_imp_prems r))))
621       end
623     (* make a disjunction of all introduction rules *)
625     val fp_fun = absfree (sname, setT, (HOLogic.Collect_const sumT) \$
626       absfree (xname, sumT, foldr1 HOLogic.mk_disj (map transform_rule intr_ts)));
628     (* add definiton of recursive sets to theory *)
630     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
631     val full_rec_name = Sign.full_name (Theory.sign_of thy) rec_name;
633     val rec_const = list_comb
634       (Const (full_rec_name, paramTs ---> setT), params);
636     val fp_def_term = Logic.mk_equals (rec_const,
637       Const (fp_name, (setT --> setT) --> setT) \$ fp_fun)
639     val def_terms = fp_def_term :: (if length cs < 2 then [] else
640       map (fn c => Logic.mk_equals (c, mk_vimage cs sumT rec_const c)) cs);
642     val thy' = thy |>
643       (if declare_consts then
644         Theory.add_consts_i (map (fn (c, n) =>
645           (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
646        else I) |>
647       (if length cs < 2 then I else
648        Theory.add_consts_i [(rec_name, paramTs ---> setT, NoSyn)]) |>
649       Theory.add_path rec_name |>
650       PureThy.add_defss_i [(("defs", def_terms), [])];
652     (* get definitions from theory *)
654     val fp_def::rec_sets_defs = PureThy.get_thms thy' "defs";
656     (* prove and store theorems *)
658     val mono = prove_mono setT fp_fun monos thy';
659     val (intrs, unfold) = prove_intrs coind mono fp_def intr_ts con_defs
660       rec_sets_defs thy';
661     val elims = if no_elim then [] else
662       prove_elims cs cTs params intr_ts unfold rec_sets_defs thy';
663     val raw_induct = if no_ind then TrueI else
664       if coind then standard (rule_by_tactic
665         (rewrite_tac [mk_meta_eq vimage_Un] THEN
666           fold_tac rec_sets_defs) (mono RS (fp_def RS def_Collect_coinduct)))
667       else
668         prove_indrule cs cTs sumT rec_const params intr_ts mono fp_def
669           rec_sets_defs thy';
670     val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct
671       else standard (raw_induct RSN (2, rev_mp));
673     val thy'' = thy'
674       |> PureThy.add_thmss [(("intrs", intrs), atts)]
675       |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
676       |> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])])
677       |> (if no_ind then I else PureThy.add_thms
678         [((coind_prefix coind ^ "induct", induct), [])])
679       |> Theory.parent_path;
680     val intrs' = PureThy.get_thms thy'' "intrs";
681     val elims' = PureThy.get_thms thy'' "elims";
682     val induct' = PureThy.get_thm thy'' (coind_prefix coind ^ "induct");
683   in (thy'',
684     {defs = fp_def::rec_sets_defs,
685      mono = mono,
686      unfold = unfold,
687      intrs = intrs',
688      elims = elims',
689      mk_cases = mk_cases elims',
690      raw_induct = raw_induct,
691      induct = induct'})
692   end;
696 (** axiomatic introduction of (co)inductive sets **)
698 fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
699     atts intros monos con_defs thy params paramTs cTs cnames =
700   let
701     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
703     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);
704     val elim_ts = mk_elims cs cTs params intr_ts;
706     val (_, ind_prems, mutual_ind_concl) = mk_indrule cs cTs params intr_ts;
707     val ind_t = Logic.list_implies (ind_prems, mutual_ind_concl);
709     val thy' = thy
710       |> (if declare_consts then
712               (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames))
713          else I)
714       |> Theory.add_path rec_name
715       |> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("elims", elim_ts), [])]
716       |> (if coind then I else
717             PureThy.add_axioms_i [(("raw_induct", ind_t), [apsnd (standard o split_rule)])]);
719     val intrs = PureThy.get_thms thy' "intrs";
720     val elims = PureThy.get_thms thy' "elims";
721     val raw_induct = if coind then TrueI else PureThy.get_thm thy' "raw_induct";
722     val induct = if coind orelse length cs > 1 then raw_induct
723       else standard (raw_induct RSN (2, rev_mp));
725     val thy'' =
726       thy'
727       |> (if coind then I else PureThy.add_thms [(("induct", induct), [])])
728       |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts)
729       |> Theory.parent_path;
730     val induct' = if coind then raw_induct else PureThy.get_thm thy'' "induct";
731   in (thy'',
732     {defs = [],
733      mono = TrueI,
734      unfold = TrueI,
735      intrs = intrs,
736      elims = elims,
737      mk_cases = mk_cases elims,
738      raw_induct = raw_induct,
739      induct = induct'})
740   end;
744 (** introduction of (co)inductive sets **)
746 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs
747     atts intros monos con_defs thy =
748   let
749     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
750     val sign = Theory.sign_of thy;
752     (*parameters should agree for all mutually recursive components*)
753     val (_, params) = strip_comb (hd cs);
754     val paramTs = map (try' (snd o dest_Free) "Parameter in recursive\
755       \ component is not a free variable: " sign) params;
757     val cTs = map (try' (HOLogic.dest_setT o fastype_of)
758       "Recursive component not of type set: " sign) cs;
760     val full_cnames = map (try' (fst o dest_Const o head_of)
761       "Recursive set not previously declared as constant: " sign) cs;
762     val cnames = map Sign.base_name full_cnames;
764     val _ = seq (check_rule sign cs o snd o fst) intros;
766     val (thy1, result) =
767       (if ! quick_and_dirty then add_ind_axm else add_ind_def)
768         verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos
769         con_defs thy params paramTs cTs cnames;
770     val thy2 = thy1 |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result);
771   in (thy2, result) end;
775 (** external interface **)
777 fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy =
778   let
779     val sign = Theory.sign_of thy;
780     val cs = map (term_of o Thm.read_cterm sign o rpair HOLogic.termT) c_strings;
782     val atts = map (Attrib.global_attribute thy) srcs;
783     val intr_names = map (fst o fst) intro_srcs;
784     val intr_ts = map (term_of o Thm.read_cterm sign o rpair propT o snd o fst) intro_srcs;
785     val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs;
786     val (cs', intr_ts') = unify_consts sign cs intr_ts;
788     val ((thy', con_defs), monos) = thy
789       |> IsarThy.apply_theorems raw_monos
790       |> apfst (IsarThy.apply_theorems raw_con_defs);
791   in
792     add_inductive_i verbose false "" coind false false cs'
793       atts ((intr_names ~~ intr_ts') ~~ intr_atts) monos con_defs thy'
794   end;
798 (** package setup **)
800 (* setup theory *)
802 val setup = [InductiveData.init,
803              Attrib.add_attributes [(monoN, mono_attr, "monotonicity rule")]];
806 (* outer syntax *)
808 local structure P = OuterParse and K = OuterSyntax.Keyword in
810 fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) =
811   #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
813 fun ind_decl coind =
814   (Scan.repeat1 P.term --| P.marg_comment) --
815   (P.\$\$\$ "intrs" |--
816     P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
817   Scan.optional (P.\$\$\$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
818   Scan.optional (P.\$\$\$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
819   >> (Toplevel.theory o mk_ind coind);
821 val inductiveP =
822   OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false);
824 val coinductiveP =
825   OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true);
828 val ind_cases =
829   P.opt_thm_name "=" -- P.xname --| P.\$\$\$ ":" -- Scan.repeat1 P.prop -- P.marg_comment
830   >> (Toplevel.theory o inductive_cases);
832 val inductive_casesP =
833   OuterSyntax.command "inductive_cases" "create simplified instances of elimination rules"
834     K.thy_decl ind_cases;
836 val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"];
837 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
839 end;
842 end;