# HG changeset patch # User wenzelm # Date 1191356606 -7200 # Node ID f7093e90f36c0585c5a829cd641d06102f04ed51 # Parent 0384f48a806eef39df26f6466adc013445164f48 tuned internal interfaces: flags record, added kind for results; tuned; diff -r 0384f48a806e -r f7093e90f36c src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Tue Oct 02 22:23:24 2007 +0200 +++ b/src/HOL/Tools/inductive_package.ML Tue Oct 02 22:23:26 2007 +0200 @@ -38,7 +38,8 @@ Proof.context -> thm list list * local_theory val inductive_cases_i: ((bstring * Attrib.src list) * term list) list -> Proof.context -> thm list list * local_theory - val add_inductive_i: bool -> bstring -> bool -> bool -> bool -> + val add_inductive_i: + {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} -> ((string * typ) * mixfix) list -> (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list -> local_theory -> inductive_result * local_theory @@ -46,7 +47,8 @@ (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 -> + val add_inductive_global: + {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} -> ((string * typ) * mixfix) list -> (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list -> theory -> inductive_result * theory val arities_of: thm -> (string * int) list @@ -61,12 +63,12 @@ sig include BASIC_INDUCTIVE_PACKAGE type add_ind_def - val declare_rules: bstring -> bool -> bool -> string list -> + val declare_rules: string -> bstring -> bool -> bool -> string list -> thm list -> bstring list -> Attrib.src list list -> (thm * string list) list -> thm -> local_theory -> thm list * thm list * thm * local_theory val add_ind_def: add_ind_def val gen_add_inductive_i: add_ind_def -> - bool -> bstring -> bool -> bool -> bool -> + {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} -> ((string * typ) * mixfix) list -> (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list -> local_theory -> inductive_result * local_theory @@ -86,10 +88,6 @@ (** theory context references **) -val mono_name = "Orderings.mono"; -val gfp_name = "FixedPoint.gfp"; -val lfp_name = "FixedPoint.lfp"; - val inductive_forall_name = "HOL.induct_forall"; val inductive_forall_def = thm "induct_forall_def"; val inductive_conj_name = "HOL.induct_conj"; @@ -198,9 +196,6 @@ fun message s = if ! quiet_mode then () else writeln s; fun clean_message s = if ! quick_and_dirty then () else message s; -val note_theorems = LocalTheory.notes Thm.theoremK; -val note_theorem = LocalTheory.note Thm.theoremK; - fun coind_prefix true = "co" | coind_prefix false = ""; @@ -325,7 +320,7 @@ (message " Proving monotonicity ..."; Goal.prove ctxt [] [] (*NO quick_and_dirty here!*) (HOLogic.mk_Trueprop - (Const (mono_name, (predT --> predT) --> HOLogic.boolT) $ fp_fun)) + (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun)) (fn _ => EVERY [rtac monoI 1, REPEAT (resolve_tac [le_funI, le_boolI'] 1), REPEAT (FIRST @@ -462,7 +457,7 @@ val facts = args |> map (fn ((a, atts), props) => ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props)); - in lthy |> note_theorems facts |>> map snd end; + in lthy |> LocalTheory.notes Thm.theoremK facts |>> map snd end; val inductive_cases = gen_inductive_cases Attrib.intern_src Syntax.read_prop; val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop; @@ -594,7 +589,7 @@ fun mk_ind_def alt_name coind cs intr_ts monos params cnames_syn ctxt = let - val fp_name = if coind then gfp_name else lfp_name; + val fp_name = if coind then @{const_name FixedPoint.gfp} else @{const_name FixedPoint.lfp}; val argTs = fold (fn c => fn Ts => Ts @ (List.drop (binder_types (fastype_of c), length params) \\ Ts)) cs []; @@ -676,7 +671,7 @@ list_comb (rec_const, params), preds, argTs, bs, xs) end; -fun declare_rules rec_name coind no_ind cnames intrs intr_names intr_atts +fun declare_rules kind rec_name coind no_ind cnames intrs intr_names intr_atts elims raw_induct ctxt = let val ind_case_names = RuleCases.case_names intr_names; @@ -691,29 +686,29 @@ val (intrs', ctxt1) = ctxt |> - note_theorems + LocalTheory.notes kind (map (NameSpace.qualified rec_name) intr_names ~~ intr_atts ~~ map (fn th => [([th], [Attrib.internal (K (ContextRules.intro_query NONE))])]) intrs) |>> map (hd o snd); val (((_, elims'), (_, [induct'])), ctxt2) = ctxt1 |> - note_theorem ((NameSpace.qualified rec_name "intros", []), intrs') ||>> + LocalTheory.note kind ((NameSpace.qualified rec_name "intros", []), intrs') ||>> fold_map (fn (name, (elim, cases)) => - note_theorem ((NameSpace.qualified (Sign.base_name name) "cases", + LocalTheory.note kind ((NameSpace.qualified (Sign.base_name name) "cases", [Attrib.internal (K (RuleCases.case_names cases)), Attrib.internal (K (RuleCases.consumes 1)), Attrib.internal (K (InductAttrib.cases_set name)), Attrib.internal (K (ContextRules.elim_query NONE))]), [elim]) #> apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>> - note_theorem ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"), + LocalTheory.note kind ((NameSpace.qualified rec_name (coind_prefix coind ^ "induct"), map (Attrib.internal o K) (#2 induct)), [rulify (#1 induct)]); val ctxt3 = if no_ind orelse coind then ctxt2 else let val inducts = cnames ~~ ProjectRule.projects ctxt2 (1 upto length cnames) induct' in ctxt2 |> - note_theorems [((NameSpace.qualified rec_name "inducts", []), + LocalTheory.notes kind [((NameSpace.qualified rec_name "inducts", []), inducts |> map (fn (name, th) => ([th], [Attrib.internal (K ind_case_names), Attrib.internal (K (RuleCases.consumes 1)), @@ -721,13 +716,14 @@ end in (intrs', elims', induct', ctxt3) end; -type add_ind_def = bool -> bstring -> bool -> bool -> bool -> +type add_ind_def = + {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} -> term list -> ((string * Attrib.src list) * term) list -> thm list -> term list -> (string * mixfix) list -> local_theory -> inductive_result * local_theory -fun add_ind_def verbose alt_name coind no_elim no_ind cs - intros monos params cnames_syn ctxt = +fun add_ind_def {verbose, kind, alt_name, coind, no_elim, no_ind} + cs intros monos params cnames_syn ctxt = let val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ @@ -757,7 +753,7 @@ prove_indrule cs argTs bs xs rec_const params intr_ts mono fp_def rec_preds_defs ctxt1); - val (intrs', elims', induct, ctxt2) = declare_rules rec_name coind no_ind + val (intrs', elims', induct, ctxt2) = declare_rules kind rec_name coind no_ind cnames intrs intr_names intr_atts elims raw_induct ctxt1; val names = map #1 cnames_syn; @@ -780,7 +776,7 @@ (* external interfaces *) -fun gen_add_inductive_i mk_def verbose alt_name coind no_elim no_ind +fun gen_add_inductive_i mk_def (flags as {verbose, kind, alt_name, coind, no_elim, no_ind}) cnames_syn pnames pre_intros monos ctxt = let val thy = ProofContext.theory_of ctxt; @@ -831,10 +827,9 @@ val intros = map (close_rule ##> expand abbrevs') pre_intros'; in - ctxt |> - mk_def verbose alt_name coind no_elim no_ind cs intros monos - params cnames_syn'' ||> - fold (snd oo LocalTheory.abbrev Syntax.default_mode) abbrevs'' + ctxt + |> mk_def flags cs intros monos params cnames_syn'' + ||> fold (snd oo LocalTheory.abbrev Syntax.default_mode) abbrevs'' end; fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos lthy = @@ -844,14 +839,16 @@ val (cs, ps) = chop (length cnames_syn) vars; val intrs = map (apsnd the_single) specs; val monos = Attrib.eval_thms lthy raw_monos; - in gen_add_inductive_i mk_def verbose "" coind false false cs (map fst ps) intrs monos lthy end; + val flags = {verbose = verbose, kind = Thm.theoremK, alt_name = "", + coind = coind, no_elim = false, no_ind = false}; + in gen_add_inductive_i mk_def flags cs (map fst ps) intrs monos lthy end; val add_inductive_i = gen_add_inductive_i add_ind_def; val add_inductive = gen_add_inductive add_ind_def; -fun add_inductive_global verbose alt_name coind no_elim no_ind cnames_syn pnames pre_intros monos = +fun add_inductive_global flags 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 #> + add_inductive_i flags cnames_syn pnames pre_intros monos #> (fn (_, lthy) => (#2 (the_inductive (LocalTheory.target_of lthy) (LocalTheory.target_name lthy (fst (fst (hd cnames_syn))))), diff -r 0384f48a806e -r f7093e90f36c src/HOL/Tools/inductive_set_package.ML --- a/src/HOL/Tools/inductive_set_package.ML Tue Oct 02 22:23:24 2007 +0200 +++ b/src/HOL/Tools/inductive_set_package.ML Tue Oct 02 22:23:26 2007 +0200 @@ -11,7 +11,8 @@ val to_set_att: thm list -> attribute val to_pred_att: thm list -> attribute val pred_set_conv_att: attribute - val add_inductive_i: bool -> bstring -> bool -> bool -> bool -> + val add_inductive_i: + {verbose: bool, kind: string, alt_name: bstring, coind: bool, no_elim: bool, no_ind: bool} -> ((string * typ) * mixfix) list -> (string * typ) list -> ((bstring * Attrib.src list) * term) list -> thm list -> local_theory -> InductivePackage.inductive_result * local_theory @@ -25,13 +26,8 @@ structure InductiveSetPackage: INDUCTIVE_SET_PACKAGE = struct -val note_theorem = LocalTheory.note Thm.theoremK; - - (**** simplify {(x1, ..., xn). (x1, ..., xn) : S} to S ****) -val subset_antisym = thm "subset_antisym"; - val collect_mem_simproc = Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss => fn S as Const ("Collect", Type ("fun", [_, T])) $ t => @@ -50,7 +46,7 @@ SOME (Goal.prove (Simplifier.the_context ss) [] [] (Const ("==", T --> T --> propT) $ S $ S') (K (EVERY - [rtac eq_reflection 1, rtac subset_antisym 1, + [rtac eq_reflection 1, rtac @{thm subset_antisym} 1, rtac subsetI 1, dtac CollectD 1, simp, rtac subsetI 1, rtac CollectI 1, simp]))) end @@ -403,8 +399,8 @@ (**** definition of inductive sets ****) -fun add_ind_set_def verbose alt_name coind no_elim no_ind cs - intros monos params cnames_syn ctxt = +fun add_ind_set_def {verbose, kind, alt_name, coind, no_elim, no_ind} + cs intros monos params cnames_syn ctxt = let val thy = ProofContext.theory_of ctxt; val {set_arities, pred_arities, to_pred_simps, ...} = @@ -466,8 +462,10 @@ val cnames_syn' = map (fn (s, _) => (s ^ "p", NoSyn)) cnames_syn; val monos' = map (to_pred [] (Context.Proof ctxt)) monos; val ({preds, intrs, elims, raw_induct, ...}, ctxt1) = - InductivePackage.add_ind_def verbose "" coind - no_elim no_ind cs' intros' monos' params1 cnames_syn' ctxt; + InductivePackage.add_ind_def {verbose = verbose, kind = kind, + alt_name = "", (* FIXME pass alt_name (!?) *) + coind = coind, no_elim = no_elim, no_ind = no_ind} + cs' intros' monos' params1 cnames_syn' ctxt; (* define inductive sets using previously defined predicates *) val (defs, ctxt2) = LocalTheory.defs Thm.internalK @@ -489,7 +487,7 @@ (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps [def, mem_Collect_eq, split_conv]) 1)) in - ctxt |> note_theorem ((s ^ "p_" ^ s ^ "_eq", + ctxt |> LocalTheory.note kind ((s ^ "p_" ^ s ^ "_eq", [Attrib.internal (K pred_set_conv_att)]), [conv_thm]) |> snd end) (preds ~~ cs ~~ cs_info ~~ defs) ctxt2; @@ -501,7 +499,7 @@ val (intr_names, intr_atts) = split_list (map fst intros); val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct; val (intrs', elims', induct, ctxt4) = - InductivePackage.declare_rules rec_name coind no_ind cnames + InductivePackage.declare_rules kind rec_name coind no_ind cnames (map (to_set [] (Context.Proof ctxt3)) intrs) intr_names intr_atts (map (fn th => (to_set [] (Context.Proof ctxt3) th, map fst (fst (RuleCases.get th)))) elims)