--- 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 ***
--- 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 \<WHERE> eq"}] produces an
internal definition @{text "c \<equiv> t"} according to the specification
--- 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 *)
--- 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;