axiomatization is now global-only;
authorwenzelm
Wed Sep 03 17:47:38 2008 +0200 (2008-09-03)
changeset 281142637fb838f74
parent 28113 f6e38928b77c
child 28115 cd0d170d4dc6
axiomatization is now global-only;
NEWS
doc-src/IsarRef/Thy/Spec.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/specification.ML
     1.1 --- a/NEWS	Wed Sep 03 17:47:37 2008 +0200
     1.2 +++ b/NEWS	Wed Sep 03 17:47:38 2008 +0200
     1.3 @@ -36,6 +36,9 @@
     1.4  
     1.5  * Keyword 'code_exception' now named 'code_abort'.  INCOMPATIBILITY.
     1.6  
     1.7 +* The 'axiomatization' command now only works within a global theory
     1.8 +context.  INCOMPATIBILITY.
     1.9 +
    1.10  
    1.11  *** Document preparation ***
    1.12  
     2.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Wed Sep 03 17:47:37 2008 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Sep 03 17:47:38 2008 +0200
     2.3 @@ -136,7 +136,7 @@
     2.4  
     2.5  text {*
     2.6    \begin{matharray}{rcll}
     2.7 -    @{command_def "axiomatization"} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
     2.8 +    @{command_def "axiomatization"} & : & \isarkeep{theory} & (axiomatic!)\\
     2.9      @{command_def "definition"} & : & \isarkeep{local{\dsh}theory} \\
    2.10      @{attribute_def "defn"} & : & \isaratt \\
    2.11      @{command_def "abbreviation"} & : & \isarkeep{local{\dsh}theory} \\
    2.12 @@ -178,8 +178,9 @@
    2.13    prevents additional specifications being issued later on.
    2.14    
    2.15    Note that axiomatic specifications are only appropriate when
    2.16 -  declaring a new logical system.  Normal applications should only use
    2.17 -  definitional mechanisms!
    2.18 +  declaring a new logical system; axiomatic specifications are
    2.19 +  restricted to global theory contexts.  Normal applications should
    2.20 +  only use definitional mechanisms!
    2.21  
    2.22    \item [@{command "definition"}~@{text "c \<WHERE> eq"}] produces an
    2.23    internal definition @{text "c \<equiv> t"} according to the specification
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Sep 03 17:47:37 2008 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Sep 03 17:47:38 2008 +0200
     3.3 @@ -252,10 +252,10 @@
     3.4  (* constant specifications *)
     3.5  
     3.6  val _ =
     3.7 -  OuterSyntax.local_theory "axiomatization" "axiomatic constant specification" K.thy_decl
     3.8 +  OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
     3.9      (Scan.optional P.fixes [] --
    3.10        Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) []
    3.11 -    >> (fn (x, y) => #2 o Specification.axiomatization_cmd x y));
    3.12 +    >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
    3.13  
    3.14  
    3.15  (* theorems *)
     4.1 --- a/src/Pure/Isar/specification.ML	Wed Sep 03 17:47:37 2008 +0200
     4.2 +++ b/src/Pure/Isar/specification.ML	Wed Sep 03 17:47:38 2008 +0200
     4.3 @@ -22,11 +22,11 @@
     4.4      (Attrib.binding * string list) list -> Proof.context ->
     4.5      (((Name.binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
     4.6    val axiomatization: (Name.binding * typ option * mixfix) list ->
     4.7 -    (Attrib.binding * term list) list -> local_theory ->
     4.8 -    (term list * (string * thm list) list) * local_theory
     4.9 +    (Attrib.binding * term list) list -> theory ->
    4.10 +    (term list * (string * thm list) list) * theory
    4.11    val axiomatization_cmd: (Name.binding * string option * mixfix) list ->
    4.12 -    (Attrib.binding * string list) list -> local_theory ->
    4.13 -    (term list * (string * thm list) list) * local_theory
    4.14 +    (Attrib.binding * string list) list -> theory ->
    4.15 +    (term list * (string * thm list) list) * theory
    4.16    val definition:
    4.17      (Name.binding * typ option * mixfix) option * (Attrib.binding * term) ->
    4.18      local_theory -> (term * (string * thm)) * local_theory
    4.19 @@ -137,18 +137,27 @@
    4.20  end;
    4.21  
    4.22  
    4.23 -(* axiomatization *)
    4.24 +(* axiomatization -- within global theory *)
    4.25  
    4.26 -fun gen_axioms do_print prep raw_vars raw_specs lthy =
    4.27 +fun gen_axioms do_print prep raw_vars raw_specs thy =
    4.28    let
    4.29 -    val ((vars, specs), _) = prep raw_vars [raw_specs] lthy;
    4.30 -    val ((consts, axioms), lthy') = LocalTheory.axioms Thm.axiomK (vars, specs) lthy;
    4.31 -    val consts' = map (Morphism.term (LocalTheory.target_morphism lthy')) consts;
    4.32 +    val ((vars, specs), _) = prep raw_vars [raw_specs] (ProofContext.init thy);
    4.33 +    val xs = map (fn ((b, T), _) => (Name.name_of b, T)) vars;
    4.34 +
    4.35 +    (*consts*)
    4.36 +    val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
    4.37 +    val subst = Term.subst_atomic (map Free xs ~~ consts);
    4.38 +
    4.39 +    (*axioms*)
    4.40 +    val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
    4.41 +        fold_map Thm.add_axiom (PureThy.name_multi (Name.name_of b) (map subst props))
    4.42 +        #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
    4.43 +    val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
    4.44 +      (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
    4.45      val _ =
    4.46        if not do_print then ()
    4.47 -      else print_consts lthy' (member (op =) (fold Term.add_frees consts' []))
    4.48 -        (map (fn ((b, T), _) => (Name.name_of b, T)) vars);
    4.49 -  in ((consts, axioms), lthy') end;
    4.50 +      else print_consts (ProofContext.init thy') (K false) xs;
    4.51 +  in ((consts, facts), thy') end;
    4.52  
    4.53  val axiomatization = gen_axioms false check_specification;
    4.54  val axiomatization_cmd = gen_axioms true read_specification;