tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
authorwenzelm
Mon May 12 17:17:32 2014 +0200 (2014-05-12)
changeset 56941952833323c99
parent 56940 35ce6dab3f5e
child 56942 5fff4dc31d34
tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
src/HOL/HOL.thy
src/HOL/HOLCF/Tools/Domain/domain.ML
src/HOL/HOLCF/Tools/Domain/domain_axioms.ML
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/Pure/Isar/typedecl.ML
src/Pure/axclass.ML
     1.1 --- a/src/HOL/HOL.thy	Mon May 12 00:13:38 2014 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon May 12 17:17:32 2014 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4  
     1.5  subsubsection {* Core syntax *}
     1.6  
     1.7 -setup {* Axclass.axiomatize_class (@{binding type}, []) *}
     1.8 +setup {* Axclass.class_axiomatization (@{binding type}, []) *}
     1.9  default_sort type
    1.10  setup {* Object_Logic.add_base_sort @{sort type} *}
    1.11  
     2.1 --- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Mon May 12 00:13:38 2014 +0200
     2.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Mon May 12 17:17:32 2014 +0200
     2.3 @@ -44,7 +44,7 @@
     2.4  fun add_arity ((b, sorts, mx), sort) thy : theory =
     2.5    thy
     2.6    |> Sign.add_types_global [(b, length sorts, mx)]
     2.7 -  |> Axclass.axiomatize_arity (Sign.full_name thy b, sorts, sort)
     2.8 +  |> Axclass.arity_axiomatization (Sign.full_name thy b, sorts, sort)
     2.9  
    2.10  fun gen_add_domain
    2.11      (prep_sort : theory -> 'a -> sort)
     3.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Mon May 12 00:13:38 2014 +0200
     3.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Mon May 12 17:17:32 2014 +0200
     3.3 @@ -104,7 +104,7 @@
     3.4      fun thy_arity (_, _, (lhsT, _)) =
     3.5          let val (dname, tvars) = dest_Type lhsT
     3.6          in (dname, map (snd o dest_TFree) tvars, @{sort pcpo}) end
     3.7 -    val thy = fold (Axclass.axiomatize_arity o thy_arity) dom_eqns thy
     3.8 +    val thy = fold (Axclass.arity_axiomatization o thy_arity) dom_eqns thy
     3.9  
    3.10      (* declare and axiomatize abs/rep *)
    3.11      val (iso_infos, thy) =
     4.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon May 12 00:13:38 2014 +0200
     4.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Mon May 12 17:17:32 2014 +0200
     4.3 @@ -428,7 +428,7 @@
     4.4          fun arity (vs, tbind, _, _, _) =
     4.5            (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"})
     4.6        in
     4.7 -        fold Axclass.axiomatize_arity (map arity doms) tmp_thy
     4.8 +        fold Axclass.arity_axiomatization (map arity doms) tmp_thy
     4.9        end
    4.10  
    4.11      (* check bifiniteness of right-hand sides *)
     5.1 --- a/src/Pure/Isar/typedecl.ML	Mon May 12 00:13:38 2014 +0200
     5.2 +++ b/src/Pure/Isar/typedecl.ML	Mon May 12 17:17:32 2014 +0200
     5.3 @@ -29,7 +29,7 @@
     5.4  fun object_logic_arity name thy =
     5.5    (case Object_Logic.get_base_sort thy of
     5.6      NONE => thy
     5.7 -  | SOME S => Axclass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy);
     5.8 +  | SOME S => Axclass.arity_axiomatization (name, replicate (Sign.arity_number thy name) S, S) thy);
     5.9  
    5.10  fun basic_decl decl (b, n, mx) lthy =
    5.11    let val name = Local_Theory.full_name lthy b in
     6.1 --- a/src/Pure/axclass.ML	Mon May 12 00:13:38 2014 +0200
     6.2 +++ b/src/Pure/axclass.ML	Mon May 12 17:17:32 2014 +0200
     6.3 @@ -30,9 +30,9 @@
     6.4    val prove_arity: string * sort list * sort -> (Proof.context -> tactic) -> theory -> theory
     6.5    val define_class: binding * class list -> string list ->
     6.6      (Thm.binding * term list) list -> theory -> class * theory
     6.7 -  val axiomatize_classrel: (class * class) list -> theory -> theory
     6.8 -  val axiomatize_arity: arity -> theory -> theory
     6.9 -  val axiomatize_class: binding * class list -> theory -> theory
    6.10 +  val classrel_axiomatization: (class * class) list -> theory -> theory
    6.11 +  val arity_axiomatization: arity -> theory -> theory
    6.12 +  val class_axiomatization: binding * class list -> theory -> theory
    6.13  end;
    6.14  
    6.15  structure Axclass: AXCLASS =
    6.16 @@ -582,7 +582,7 @@
    6.17  local
    6.18  
    6.19  (*old-style axioms*)
    6.20 -fun axiomatize prep mk name add raw_args thy =
    6.21 +fun add_axioms prep mk name add raw_args thy =
    6.22    let
    6.23      val args = prep thy raw_args;
    6.24      val specs = mk args;
    6.25 @@ -598,22 +598,22 @@
    6.26  
    6.27  in
    6.28  
    6.29 -val axiomatize_classrel =
    6.30 -  axiomatize (map o cert_classrel) (map Logic.mk_classrel)
    6.31 +val classrel_axiomatization =
    6.32 +  add_axioms (map o cert_classrel) (map Logic.mk_classrel)
    6.33      (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
    6.34  
    6.35 -val axiomatize_arity =
    6.36 -  axiomatize (Proof_Context.cert_arity o Proof_Context.init_global) Logic.mk_arities
    6.37 +val arity_axiomatization =
    6.38 +  add_axioms (Proof_Context.cert_arity o Proof_Context.init_global) Logic.mk_arities
    6.39      (map (prefix arity_prefix) o Logic.name_arities) add_arity;
    6.40  
    6.41 -fun axiomatize_class (bclass, raw_super) thy =
    6.42 +fun class_axiomatization (bclass, raw_super) thy =
    6.43    let
    6.44      val class = Sign.full_name thy bclass;
    6.45      val super = map (Sign.certify_class thy) raw_super |> Sign.minimize_sort thy;
    6.46    in
    6.47      thy
    6.48      |> Sign.primitive_class (bclass, super)
    6.49 -    |> axiomatize_classrel (map (fn c => (class, c)) super)
    6.50 +    |> classrel_axiomatization (map (fn c => (class, c)) super)
    6.51      |> Theory.add_deps_global "" (class_const class) (map class_const super)
    6.52    end;
    6.53