# HG changeset patch # User wenzelm # Date 1571770513 -7200 # Node ID 98d9b78b7f47de61a7369e3fd6c5530ca971a4e7 # Parent 539dfd4c166b0b6f7e0ceb44982c6cb402d72379 clarified axiom_table: uniform space (e.g. like consts), e.g. relevant for export of HOL-ex.Join_Theory; diff -r 539dfd4c166b -r 98d9b78b7f47 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Tue Oct 22 20:08:25 2019 +0200 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Tue Oct 22 20:55:13 2019 +0200 @@ -322,15 +322,6 @@ \ ML \ -val axms_of_thy = - `Theory.axioms_of - #> apsnd cterm_of - #> swap - #> apsnd (map snd) - #> uncurry map -\ - -ML \ (*Show the skeleton-level inference which is done by each element of just_the_tacs. This is useful when debugging using the technique shown next*) if test_all @{context} orelse prob_names = [] then () else diff -r 539dfd4c166b -r 98d9b78b7f47 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Oct 22 20:08:25 2019 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Oct 22 20:55:13 2019 +0200 @@ -1338,8 +1338,7 @@ |> maps snd |> map_filter #def |> Ord_List.make fast_string_ord in - Theory.nodes_of thy - |> maps Thm.axioms_of + Thm.all_axioms_of thy |> map (apsnd (subst_atomic subst o Thm.prop_of)) |> sort (fast_string_ord o apply2 fst) |> Ord_List.inter (fast_string_ord o apsnd fst) def_names diff -r 539dfd4c166b -r 98d9b78b7f47 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Tue Oct 22 20:08:25 2019 +0200 +++ b/src/Pure/Thy/export_theory.ML Tue Oct 22 20:55:13 2019 +0200 @@ -242,8 +242,8 @@ encode_prop (#1 (standard_prop used [] prop NONE)); val _ = - export_entities "axioms" (fn _ => fn t => SOME (encode_axiom Name.context t)) - Theory.axiom_space (Theory.axioms_of thy); + export_entities "axioms" (K (SOME o encode_axiom Name.context)) + Theory.axiom_space (Theory.all_axioms_of thy); (* theorems and proof terms *) diff -r 539dfd4c166b -r 98d9b78b7f47 src/Pure/theory.ML --- a/src/Pure/theory.ML Tue Oct 22 20:08:25 2019 +0200 +++ b/src/Pure/theory.ML Tue Oct 22 20:55:13 2019 +0200 @@ -18,7 +18,6 @@ val check: {long: bool} -> Proof.context -> string * Position.T -> theory val axiom_table: theory -> term Name_Space.table val axiom_space: theory -> Name_Space.T - val axioms_of: theory -> (string * term) list val all_axioms_of: theory -> (string * term) list val defs_of: theory -> Defs.T val at_begin: (theory -> theory option) -> theory -> theory @@ -88,18 +87,17 @@ structure Thy = Theory_Data' ( type T = thy; - val empty_axioms = Name_Space.empty_table "axiom" : term Name_Space.table; - val empty = make_thy (Position.none, 0, empty_axioms, Defs.empty, ([], [])); + val empty = make_thy (Position.none, 0, Name_Space.empty_table "axiom", Defs.empty, ([], [])); - fun extend (Thy {pos = _, id = _, axioms = _, defs, wrappers}) = - make_thy (Position.none, 0, empty_axioms, defs, wrappers); + fun extend (Thy {pos = _, id = _, axioms, defs, wrappers}) = + make_thy (Position.none, 0, axioms, defs, wrappers); fun merge old_thys (thy1, thy2) = let - val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1; - val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2; + val Thy {pos = _, id = _, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1; + val Thy {pos = _, id = _, axioms = axioms2, defs = defs2, wrappers = (bgs2, ens2)} = thy2; - val axioms' = empty_axioms; + val axioms' = Name_Space.merge_tables (axioms1, axioms2); val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2); val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2); val ens' = Library.merge (eq_snd op =) (ens1, ens2); @@ -163,8 +161,7 @@ val axiom_table = #axioms o rep_theory; val axiom_space = Name_Space.space_of_table o axiom_table; -val axioms_of = Name_Space.dest_table o axiom_table; -fun all_axioms_of thy = maps axioms_of (nodes_of thy); +val all_axioms_of = Name_Space.dest_table o axiom_table; val defs_of = #defs o rep_theory; diff -r 539dfd4c166b -r 98d9b78b7f47 src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Oct 22 20:08:25 2019 +0200 +++ b/src/Pure/thm.ML Tue Oct 22 20:55:13 2019 +0200 @@ -113,7 +113,7 @@ val close_derivation: Position.T -> thm -> thm val trim_context: thm -> thm val axiom: theory -> string -> thm - val axioms_of: theory -> (string * thm) list + val all_axioms_of: theory -> (string * thm) list val get_tags: thm -> Properties.T val map_tags: (Properties.T -> Properties.T) -> thm -> thm val norm_proof: thm -> thm @@ -804,30 +804,23 @@ (** Axioms **) -fun axiom thy0 name = - let - fun get_ax thy = - Name_Space.lookup (Theory.axiom_table thy) name - |> Option.map (fn prop => - let - val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop); - val cert = Context.Certificate thy; - val maxidx = maxidx_of_term prop; - val shyps = Sorts.insert_term prop []; - in - Thm (der, - {cert = cert, tags = [], maxidx = maxidx, - constraints = [], shyps = shyps, hyps = [], tpairs = [], prop = prop}) - end); - in - (case get_first get_ax (Theory.nodes_of thy0) of - SOME thm => thm - | NONE => raise THEORY ("No axiom " ^ quote name, [thy0])) - end; +fun axiom thy name = + (case Name_Space.lookup (Theory.axiom_table thy) name of + SOME prop => + let + val der = deriv_rule0 (fn () => Proofterm.axm_proof name prop); + val cert = Context.Certificate thy; + val maxidx = maxidx_of_term prop; + val shyps = Sorts.insert_term prop []; + in + Thm (der, + {cert = cert, tags = [], maxidx = maxidx, + constraints = [], shyps = shyps, hyps = [], tpairs = [], prop = prop}) + end + | NONE => raise THEORY ("No axiom " ^ quote name, [thy])); -(*return additional axioms of this theory node*) -fun axioms_of thy = - map (fn (name, _) => (name, axiom thy name)) (Theory.axioms_of thy); +fun all_axioms_of thy = + map (fn (name, _) => (name, axiom thy name)) (Theory.all_axioms_of thy); (* tags *)