# HG changeset patch # User wenzelm # Date 1164560840 -3600 # Node ID 1e6bd5ed7abc74b85d556547d6c0257756199366 # Parent 1b18b5892dc48c70d8162bcb9462cfa8e30f744a added morh_result, the_inductive, add_inductive_global; removed get_inductive; more careful treatment of result naming/morphing; diff -r 1b18b5892dc4 -r 1e6bd5ed7abc src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Sun Nov 26 18:07:19 2006 +0100 +++ b/src/HOL/Tools/inductive_package.ML Sun Nov 26 18:07:20 2006 +0100 @@ -23,8 +23,9 @@ sig val quiet_mode: bool ref type inductive_result + val morph_result: morphism -> inductive_result -> inductive_result type inductive_info - val get_inductive: Proof.context -> string -> inductive_info option + val the_inductive: Proof.context -> string -> inductive_info val print_inductives: Proof.context -> unit val mono_add: attribute val mono_del: attribute @@ -45,6 +46,9 @@ (string * string option * mixfix) list -> ((bstring * Attrib.src list) * string) list -> (thmref * Attrib.src list) list -> local_theory -> inductive_result * local_theory + val add_inductive_global: bool -> bstring -> bool -> bool -> bool -> + (string * typ option * mixfix) list -> (string * typ option) list -> + ((bstring * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory val setup: theory -> theory end; @@ -83,12 +87,22 @@ {preds: term list, defs: thm list, elims: thm list, raw_induct: thm, induct: thm, intrs: thm list, mono: thm, unfold: thm}; +fun morph_result phi {preds, defs, elims, raw_induct: thm, induct, intrs, mono, unfold} = + let + val term = Morphism.term phi; + val thm = Morphism.thm phi; + val fact = Morphism.fact phi; + in + {preds = map term preds, defs = fact defs, elims = fact elims, raw_induct = thm raw_induct, + induct = thm induct, intrs = fact intrs, mono = thm mono, unfold = thm unfold} + end; + type inductive_info = {names: string list, coind: bool} * inductive_result; structure InductiveData = GenericDataFun (struct - val name = "HOL/inductive2"; + val name = "HOL/inductive"; type T = inductive_info Symtab.table * thm list; val empty = (Symtab.empty, []); @@ -96,36 +110,37 @@ fun merge _ ((tab1, monos1), (tab2, monos2)) = (Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2)); - fun print generic (tab, monos) = - [Pretty.strs ("(co)inductives:" :: - map #1 (NameSpace.extern_table - (Sign.const_space (Context.theory_of generic), tab))), (* FIXME? *) - Pretty.big_list "monotonicity rules:" - (map (ProofContext.pretty_thm (Context.proof_of generic)) monos)] - |> Pretty.chunks |> Pretty.writeln; + fun print context (tab, monos) = + let + val ctxt = Context.proof_of context; + val space = Consts.space_of (ProofContext.consts_of ctxt); + in + [Pretty.strs ("(co)inductives:" :: map #1 (NameSpace.extern_table (space, tab))), + Pretty.big_list "monotonicity rules:" (map (ProofContext.pretty_thm ctxt) monos)] + |> Pretty.chunks |> Pretty.writeln + end; end); +val get_inductives = InductiveData.get o Context.Proof; val print_inductives = InductiveData.print o Context.Proof; (* get and put data *) -val get_inductive = Symtab.lookup o #1 o InductiveData.get o Context.Proof; - fun the_inductive ctxt name = - (case get_inductive ctxt name of + (case Symtab.lookup (#1 (get_inductives ctxt)) name of NONE => error ("Unknown (co)inductive predicate " ^ quote name) | SOME info => info); fun put_inductives names info = InductiveData.map (apfst (fn tab => fold (fn name => Symtab.update_new (name, info)) names tab - handle Symtab.DUP dup => error ("Duplicate definition of (co)inductive predicate " ^ quote dup))); + handle Symtab.DUP d => error ("Duplicate definition of (co)inductive predicate " ^ quote d))); (** monotonicity rules **) -val get_monos = #2 o InductiveData.get o Context.Proof; +val get_monos = #2 o get_inductives; val map_monos = InductiveData.map o apsnd; fun mk_mono thm = @@ -143,9 +158,6 @@ else [thm] end; - -(* attributes *) - val mono_add = Thm.declaration_attribute (map_monos o fold Drule.add_rule o mk_mono); val mono_del = Thm.declaration_attribute (map_monos o fold Drule.del_rule o mk_mono); @@ -382,9 +394,6 @@ EVERY' [elim_tac, asm_full_simp_tac ss, elim_tac, REPEAT o bound_hyp_subst_tac] i THEN_MAYBE (if solved then no_tac else all_tac); (* FIXME !? *) -(*prop should have the form "P t" where P is an inductive predicate*) -val mk_cases_err = "mk_cases: proposition not an inductive predicate"; - in fun mk_cases ctxt prop = @@ -392,8 +401,13 @@ val thy = ProofContext.theory_of ctxt; val ss = Simplifier.local_simpset_of ctxt; - val c = #1 (Term.dest_Const (Term.head_of (HOLogic.dest_Trueprop - (Logic.strip_imp_concl prop)))) handle TERM _ => error mk_cases_err; + fun err msg = + error (Pretty.string_of (Pretty.block + [Pretty.str msg, Pretty.fbrk, ProofContext.pretty_term ctxt prop])); + + val P = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop) handle TERM _ => + err "Object-logic proposition expected"; + val c = Term.head_name_of P; val (_, {elims, ...}) = the_inductive ctxt c; val cprop = Thm.cterm_of thy prop; @@ -404,8 +418,7 @@ in (case get_first (try mk_elim) elims of SOME r => r - | NONE => error (Pretty.string_of (Pretty.block - [Pretty.str mk_cases_err, Pretty.fbrk, ProofContext.pretty_term ctxt prop]))) + | NONE => err "Proposition not an inductive predicate:") end; end; @@ -479,6 +492,7 @@ val ind_prems = map mk_ind_prem intr_ts; + (* make conclusions for induction rules *) val Tss = map (binder_types o fastype_of) preds; @@ -627,7 +641,7 @@ if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote (map fst cnames_syn)) else (); - val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn; + val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn; (* FIXME *) val ((intr_names, intr_atts), intr_ts) = apfst split_list (split_list intros); val (ctxt1, rec_name, mono, fp_def, rec_preds_defs, rec_const, preds, @@ -691,6 +705,7 @@ Attrib.internal (induct_att name)])))] |> snd end; + val names = map #1 cnames_syn; val result = {preds = preds, defs = fp_def :: rec_preds_defs, @@ -699,12 +714,17 @@ intrs = intrs', elims = elims', raw_induct = rulify raw_induct, - induct = induct'} + induct = induct'}; + val target_result = morph_result (LocalTheory.target_morphism ctxt4) result; - in - (result, LocalTheory.declaration (fn phi => (* FIXME *) - (put_inductives cnames ({names = cnames, coind = coind}, result))) ctxt4) - end; + val ctxt5 = ctxt4 + |> Context.proof_map (put_inductives names ({names = names, coind = coind}, result)) + |> LocalTheory.declaration (fn phi => + let + val names' = map (LocalTheory.target_name ctxt4 o Morphism.name phi) names; + val result' = morph_result phi target_result; + in put_inductives names' ({names = names', coind = coind}, result') end); + in (result, ctxt5) end; (* external interfaces *) @@ -750,6 +770,13 @@ add_inductive_i verbose "" coind false false cnames_syn' pnames intrs monos ctxt'' end; +fun add_inductive_global verbose alt_name coind no_elim no_ind cnames_syn pnames pre_intros monos = + TheoryTarget.init NONE #> + add_inductive_i verbose alt_name coind no_elim no_ind cnames_syn pnames pre_intros monos #> + (fn (_, lthy) => + (#2 (the_inductive (LocalTheory.target_of lthy) + (LocalTheory.target_name lthy (#1 (hd cnames_syn)))), + ProofContext.theory_of (LocalTheory.exit lthy))); (** package setup **)