# HG changeset patch # User wenzelm # Date 1218725566 -7200 # Node ID 27a8ad9612a31ef88cc403eb63ecdb6d0ecaf4ce # Parent 827730aea9e863022a0019f21c733daa974f0c8b moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML); diff -r 827730aea9e8 -r 27a8ad9612a3 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/HOL/Import/shuffler.ML Thu Aug 14 16:52:46 2008 +0200 @@ -627,7 +627,7 @@ val shuffles = ShuffleData.get thy val ignored = collect_ignored shuffles [] val all_thms = - map (`PureThy.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy))) + map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy))) in List.filter (match_consts ignored t) all_thms end diff -r 827730aea9e8 -r 27a8ad9612a3 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/HOL/Tools/datatype_package.ML Thu Aug 14 16:52:46 2008 +0200 @@ -217,7 +217,7 @@ [(("", nth inducts index), [Induct.induct_type name]), (("", exhaustion), [Induct.cases_type name])]; fun unnamed_rule i = - (("", nth inducts i), [PureThy.kind_internal, Induct.induct_type ""]); + (("", nth inducts i), [Thm.kind_internal, Induct.induct_type ""]); in thy |> PureThy.add_thms (maps named_rules infos @ diff -r 827730aea9e8 -r 27a8ad9612a3 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/HOL/Tools/meson.ML Thu Aug 14 16:52:46 2008 +0200 @@ -431,7 +431,7 @@ (*Use "theorem naming" to label the clauses*) fun name_thms label = let fun name1 (th, (k,ths)) = - (k-1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths) + (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths) in fn ths => #2 (foldr name1 (length ths, []) ths) end; (*Is the given disjunction an all-negative support clause?*) diff -r 827730aea9e8 -r 27a8ad9612a3 src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/HOL/Tools/metis_tools.ML Thu Aug 14 16:52:46 2008 +0200 @@ -568,7 +568,7 @@ (* Main function to start metis prove and reconstruction *) fun FOL_SOLVE mode ctxt cls ths0 = let val thy = ProofContext.theory_of ctxt - val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0 + val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0 val ths = List.concat (map #2 th_cls_pairs) val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause" else (); diff -r 827730aea9e8 -r 27a8ad9612a3 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/HOL/Tools/res_atp.ML Thu Aug 14 16:52:46 2008 +0200 @@ -817,7 +817,7 @@ fun sledgehammer state = let val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state) - val chain_ths = map (PureThy.put_name_hint Recon.chained_hint) chain_ths + val chain_ths = map (Thm.put_name_hint Recon.chained_hint) chain_ths (*Mark the chained theorems to keep them out of metis calls; their original "name hints" may be bad anyway.*) val thy = ProofContext.theory_of ctxt diff -r 827730aea9e8 -r 27a8ad9612a3 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/HOL/Tools/res_axioms.ML Thu Aug 14 16:52:46 2008 +0200 @@ -327,7 +327,7 @@ | _ => false; fun bad_for_atp th = - PureThy.is_internal th + Thm.is_internal th orelse too_complex (prop_of th) orelse exists_type type_has_empty_sort (prop_of th) orelse is_strange_thm th; @@ -340,11 +340,11 @@ fun flatten_name s = space_implode "_X" (NameSpace.explode s); fun fake_name th = - if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th) + if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th) else gensym "unknown_thm_"; fun name_or_string th = - if PureThy.has_name_hint th then PureThy.get_name_hint th + if Thm.has_name_hint th then Thm.get_name_hint th else Display.string_of_thm th; (*Skolemize a named theorem, with Skolem functions as additional premises.*) @@ -404,7 +404,7 @@ (**** Extract and Clausify theorems from a theory's claset and simpset ****) -fun pairname th = (PureThy.get_name_hint th, th); +fun pairname th = (Thm.get_name_hint th, th); fun rules_of_claset cs = let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs diff -r 827730aea9e8 -r 27a8ad9612a3 src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/HOL/Tools/res_reconstruct.ML Thu Aug 14 16:52:46 2008 +0200 @@ -488,7 +488,7 @@ (**** retrieve the axioms that were used in the proof ****) -(*PureThy.get_name_hint returns "??.unknown" if no name is available.*) +(*Thm.get_name_hint returns "??.unknown" if no name is available.*) fun goodhint x = (x <> "??.unknown"); (*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*) diff -r 827730aea9e8 -r 27a8ad9612a3 src/HOL/ex/Quickcheck.thy --- a/src/HOL/ex/Quickcheck.thy Thu Aug 14 11:55:05 2008 +0200 +++ b/src/HOL/ex/Quickcheck.thy Thu Aug 14 16:52:46 2008 +0200 @@ -121,7 +121,7 @@ |> singleton (ProofContext.export lthy (ProofContext.init thy)) in lthy - |> LocalTheory.theory (PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [PureThy.kind_internal]) + |> LocalTheory.theory (PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal]) #-> Code.add_func) end; in diff -r 827730aea9e8 -r 27a8ad9612a3 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/Pure/Isar/attrib.ML Thu Aug 14 16:52:46 2008 +0200 @@ -215,10 +215,10 @@ (* tags *) -val tagged = syntax (Scan.lift (Args.name -- Args.name) >> PureThy.tag); -val untagged = syntax (Scan.lift Args.name >> PureThy.untag); +val tagged = syntax (Scan.lift (Args.name -- Args.name) >> Thm.tag); +val untagged = syntax (Scan.lift Args.name >> Thm.untag); -val kind = syntax (Scan.lift Args.name >> PureThy.kind); +val kind = syntax (Scan.lift Args.name >> Thm.kind); (* rule composition *) diff -r 827730aea9e8 -r 27a8ad9612a3 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/Pure/Isar/element.ML Thu Aug 14 16:52:46 2008 +0200 @@ -228,9 +228,9 @@ fun thm_name kind th prts = let val head = - if PureThy.has_name_hint th then + if Thm.has_name_hint th then Pretty.block [Pretty.command kind, - Pretty.brk 1, Pretty.str (Sign.base_name (PureThy.get_name_hint th) ^ ":")] + Pretty.brk 1, Pretty.str (Sign.base_name (Thm.get_name_hint th) ^ ":")] else Pretty.command kind in Pretty.block (Pretty.fbreaks (head :: prts)) end; diff -r 827730aea9e8 -r 27a8ad9612a3 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/Pure/Isar/locale.ML Thu Aug 14 16:52:46 2008 +0200 @@ -1775,7 +1775,7 @@ |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], []) |> Sign.declare_const [] (bname, predT, NoSyn) |> snd |> PureThy.add_defs false - [((Thm.def_name bname, Logic.mk_equals (head, body)), [PureThy.kind_internal])]; + [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])]; val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head; val cert = Thm.cterm_of defs_thy; diff -r 827730aea9e8 -r 27a8ad9612a3 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/Pure/Isar/rule_cases.ML Thu Aug 14 16:52:46 2008 +0200 @@ -223,8 +223,8 @@ fun put_consumes NONE th = th | put_consumes (SOME n) th = th - |> PureThy.untag_rule consumes_tagN - |> PureThy.tag_rule + |> Thm.untag_rule consumes_tagN + |> Thm.tag_rule (consumes_tagN, Library.string_of_int (if n < 0 then Thm.nprems_of th + n else n)); fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th; @@ -247,8 +247,8 @@ fun add_case_names NONE = I | add_case_names (SOME names) = - PureThy.untag_rule case_names_tagN - #> PureThy.tag_rule (case_names_tagN, implode_args names); + Thm.untag_rule case_names_tagN + #> Thm.tag_rule (case_names_tagN, implode_args names); fun lookup_case_names th = AList.lookup (op =) (Thm.get_tags th) case_names_tagN diff -r 827730aea9e8 -r 27a8ad9612a3 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/Pure/Proof/extraction.ML Thu Aug 14 16:52:46 2008 +0200 @@ -356,7 +356,7 @@ val is_def = (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of (Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts) - andalso (PureThy.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name) + andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name) | _ => false) handle TERM _ => false; in (ExtractionData.put (if is_def then diff -r 827730aea9e8 -r 27a8ad9612a3 src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Aug 14 16:52:46 2008 +0200 @@ -176,7 +176,7 @@ fun tell_thm_deps ths = if print_mode_active thm_depsN then let - val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths); + val names = map Thm.get_name_hint (filter Thm.has_name_hint ths); val deps = Symtab.keys (fold Proofterm.thms_of_proof' (map Thm.proof_of ths) Symtab.empty); in diff -r 827730aea9e8 -r 27a8ad9612a3 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Aug 14 16:52:46 2008 +0200 @@ -341,7 +341,7 @@ fun tell_thm_deps ths = if !show_theorem_dependencies then let - val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths); + val names = map Thm.get_name_hint (filter Thm.has_name_hint ths); val deps = (Symtab.keys (fold Proofterm.thms_of_proof' (map Thm.proof_of ths) Symtab.empty)) in diff -r 827730aea9e8 -r 27a8ad9612a3 src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/Pure/Thy/thm_deps.ML Thu Aug 14 16:52:46 2008 +0200 @@ -93,13 +93,13 @@ | SOME ps => not (member (op aconv) (map fst ps) (Thm.prop_of th)); (* groups containing at least one used theorem *) val grps = fold (fn p as (_, thm) => if is_unused p then I else - case PureThy.get_group thm of + case Thm.get_group thm of NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty; val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') => - if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (PureThy.get_kind thm) + if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm) andalso is_unused p then - (case PureThy.get_group thm of + (case Thm.get_group thm of NONE => (p :: thms, grps') | SOME grp => (* do not output theorem if another theorem in group has been used *) diff -r 827730aea9e8 -r 27a8ad9612a3 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/Pure/axclass.ML Thu Aug 14 16:52:46 2008 +0200 @@ -374,7 +374,7 @@ (Thm.def_name c', Logic.mk_equals (Const (c, T'), const')) #>> Thm.varifyT #-> (fn thm => add_inst_param (c, tyco) (c'', thm) - #> PureThy.add_thm ((c', thm), [PureThy.kind_internal]) + #> PureThy.add_thm ((c', thm), [Thm.kind_internal]) #> snd #> Sign.restore_naming thy #> pair (Const (c, T)))) diff -r 827730aea9e8 -r 27a8ad9612a3 src/Pure/drule.ML --- a/src/Pure/drule.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/Pure/drule.ML Thu Aug 14 16:52:46 2008 +0200 @@ -791,13 +791,13 @@ val term_def = get_axiom "term_def"; in val protect = Thm.capply (certify Logic.protectC); - val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard + val protectI = store_thm "protectI" (Thm.kind_rule Thm.internalK (standard (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)))); - val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard + val protectD = store_thm "protectD" (Thm.kind_rule Thm.internalK (standard (Thm.equal_elim prop_def (Thm.assume (protect A))))); val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A)); - val termI = store_thm "termI" (PureThy.kind_rule Thm.internalK (standard + val termI = store_thm "termI" (Thm.kind_rule Thm.internalK (standard (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))))); end; diff -r 827730aea9e8 -r 27a8ad9612a3 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/Pure/meta_simplifier.ML Thu Aug 14 16:52:46 2008 +0200 @@ -528,7 +528,7 @@ end; fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) = - maps (fn thm => map (rpair (PureThy.get_name_hint thm)) (mk thm)) thms; + maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk thm)) thms; fun extract_safe_rrules (ss, thm) = maps (orient_rrule ss) (extract_rews (ss, [thm])); diff -r 827730aea9e8 -r 27a8ad9612a3 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/Pure/pure_thy.ML Thu Aug 14 16:52:46 2008 +0200 @@ -7,23 +7,6 @@ signature PURE_THY = sig - val tag_rule: Markup.property -> thm -> thm - val untag_rule: string -> thm -> thm - val tag: Markup.property -> attribute - val untag: string -> attribute - val has_name_hint: thm -> bool - val get_name_hint: thm -> string - val put_name_hint: string -> thm -> thm - val get_group: thm -> string option - val put_group: string -> thm -> thm - val group: string -> attribute - val has_kind: thm -> bool - val get_kind: thm -> string - val kind_rule: string -> thm -> thm - val kind: string -> attribute - val kind_internal: attribute - val has_internal: Markup.property list -> bool - val is_internal: thm -> bool val facts_of: theory -> Facts.T val intern_fact: theory -> xstring -> string val defined_fact: theory -> string -> bool @@ -69,52 +52,6 @@ struct -(*** theorem tags ***) - -(* add / delete tags *) - -fun tag_rule tg = Thm.map_tags (insert (op =) tg); -fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s')); - -fun tag tg x = Thm.rule_attribute (K (tag_rule tg)) x; -fun untag s x = Thm.rule_attribute (K (untag_rule s)) x; - - -(* unofficial theorem names *) - -fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); - -val has_name_hint = can the_name_hint; -val get_name_hint = the_default "??.unknown" o try the_name_hint; - -fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); - - -(* theorem groups *) - -fun get_group thm = AList.lookup (op =) (Thm.get_tags thm) Markup.groupN; - -fun put_group name = - if name = "" then I else Thm.map_tags (AList.update (op =) (Markup.groupN, name)); - -fun group name = Thm.rule_attribute (K (put_group name)); - - -(* theorem kinds *) - -fun the_kind thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.kindN); - -val has_kind = can the_kind; -val get_kind = the_default "" o try the_kind; - -fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; -fun kind k x = if k = "" then x else Thm.rule_attribute (K (kind_rule k)) x; -fun kind_internal x = kind Thm.internalK x; -fun has_internal tags = exists (fn tg => tg = (Markup.kindN, Thm.internalK)) tags; -val is_internal = has_internal o Thm.get_tags; - - - (*** stored facts ***) (** theory data **) @@ -159,7 +96,7 @@ fun get_thm thy name = Facts.the_single name (get_thms thy name); fun all_thms_of thy = - Facts.fold_static (fn (_, ths) => append (map (`(get_name_hint)) ths)) (facts_of thy) []; + Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) []; @@ -180,8 +117,8 @@ fun name_thm pre official name thm = thm |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name) - |> (if has_name_hint thm andalso pre orelse name = "" then I else put_name_hint name) - |> Thm.map_tags (Position.default_properties (Position.thread_data ())); + |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name) + |> Thm.default_position (Position.thread_data ()); fun name_thms pre official name xs = map (uncurry (name_thm pre official)) (name_multi name xs); @@ -250,8 +187,8 @@ in -fun note_thmss k = gen_note_thmss (kind k); -fun note_thmss_grouped k g = gen_note_thmss (kind k #> group g); +fun note_thmss k = gen_note_thmss (Thm.kind k); +fun note_thmss_grouped k g = gen_note_thmss (Thm.kind k #> Thm.group g); end; @@ -414,4 +351,3 @@ #> Theory.add_axioms_i Proofterm.equality_axms)); end; - diff -r 827730aea9e8 -r 27a8ad9612a3 src/Tools/induct.ML --- a/src/Tools/induct.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/Tools/induct.ML Thu Aug 14 16:52:46 2008 +0200 @@ -573,7 +573,7 @@ ((fn [] => NONE | ts => List.last ts) #> (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #> find_inductT ctxt)) [[]] - |> filter_out (forall PureThy.is_internal); + |> filter_out (forall Thm.is_internal); fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact)) | get_inductP _ _ = [];