# HG changeset patch # User wenzelm # Date 1220456858 -7200 # Node ID 2637fb838f743857c362cc66e9687ca1cfa3231a # Parent f6e38928b77cd7ba879db65f86713db696124fd6 axiomatization is now global-only; diff -r f6e38928b77c -r 2637fb838f74 NEWS --- a/NEWS Wed Sep 03 17:47:37 2008 +0200 +++ b/NEWS Wed Sep 03 17:47:38 2008 +0200 @@ -36,6 +36,9 @@ * Keyword 'code_exception' now named 'code_abort'. INCOMPATIBILITY. +* The 'axiomatization' command now only works within a global theory +context. INCOMPATIBILITY. + *** Document preparation *** diff -r f6e38928b77c -r 2637fb838f74 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Wed Sep 03 17:47:37 2008 +0200 +++ b/doc-src/IsarRef/Thy/Spec.thy Wed Sep 03 17:47:38 2008 +0200 @@ -136,7 +136,7 @@ text {* \begin{matharray}{rcll} - @{command_def "axiomatization"} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\ + @{command_def "axiomatization"} & : & \isarkeep{theory} & (axiomatic!)\\ @{command_def "definition"} & : & \isarkeep{local{\dsh}theory} \\ @{attribute_def "defn"} & : & \isaratt \\ @{command_def "abbreviation"} & : & \isarkeep{local{\dsh}theory} \\ @@ -178,8 +178,9 @@ prevents additional specifications being issued later on. Note that axiomatic specifications are only appropriate when - declaring a new logical system. Normal applications should only use - definitional mechanisms! + declaring a new logical system; axiomatic specifications are + restricted to global theory contexts. Normal applications should + only use definitional mechanisms! \item [@{command "definition"}~@{text "c \ eq"}] produces an internal definition @{text "c \ t"} according to the specification diff -r f6e38928b77c -r 2637fb838f74 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Sep 03 17:47:37 2008 +0200 +++ b/src/Pure/Isar/isar_syn.ML Wed Sep 03 17:47:38 2008 +0200 @@ -252,10 +252,10 @@ (* constant specifications *) val _ = - OuterSyntax.local_theory "axiomatization" "axiomatic constant specification" K.thy_decl + OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl (Scan.optional P.fixes [] -- Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) [] - >> (fn (x, y) => #2 o Specification.axiomatization_cmd x y)); + >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y))); (* theorems *) diff -r f6e38928b77c -r 2637fb838f74 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Wed Sep 03 17:47:37 2008 +0200 +++ b/src/Pure/Isar/specification.ML Wed Sep 03 17:47:38 2008 +0200 @@ -22,11 +22,11 @@ (Attrib.binding * string list) list -> Proof.context -> (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context val axiomatization: (Name.binding * typ option * mixfix) list -> - (Attrib.binding * term list) list -> local_theory -> - (term list * (string * thm list) list) * local_theory + (Attrib.binding * term list) list -> theory -> + (term list * (string * thm list) list) * theory val axiomatization_cmd: (Name.binding * string option * mixfix) list -> - (Attrib.binding * string list) list -> local_theory -> - (term list * (string * thm list) list) * local_theory + (Attrib.binding * string list) list -> theory -> + (term list * (string * thm list) list) * theory val definition: (Name.binding * typ option * mixfix) option * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory @@ -137,18 +137,27 @@ end; -(* axiomatization *) +(* axiomatization -- within global theory *) -fun gen_axioms do_print prep raw_vars raw_specs lthy = +fun gen_axioms do_print prep raw_vars raw_specs thy = let - val ((vars, specs), _) = prep raw_vars [raw_specs] lthy; - val ((consts, axioms), lthy') = LocalTheory.axioms Thm.axiomK (vars, specs) lthy; - val consts' = map (Morphism.term (LocalTheory.target_morphism lthy')) consts; + val ((vars, specs), _) = prep raw_vars [raw_specs] (ProofContext.init thy); + val xs = map (fn ((b, T), _) => (Name.name_of b, T)) vars; + + (*consts*) + val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars; + val subst = Term.subst_atomic (map Free xs ~~ consts); + + (*axioms*) + val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) => + fold_map Thm.add_axiom (PureThy.name_multi (Name.name_of b) (map subst props)) + #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs; + val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK + (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms); val _ = if not do_print then () - else print_consts lthy' (member (op =) (fold Term.add_frees consts' [])) - (map (fn ((b, T), _) => (Name.name_of b, T)) vars); - in ((consts, axioms), lthy') end; + else print_consts (ProofContext.init thy') (K false) xs; + in ((consts, facts), thy') end; val axiomatization = gen_axioms false check_specification; val axiomatization_cmd = gen_axioms true read_specification;