# HG changeset patch
# User wenzelm
# Date 1258313962 -3600
# Node ID 9dd1079cec3a94fd6eabcf2ca8ff963131887891
# Parent  768d14a67256a901df3657b7f9075bb8ea68acac
primitive defs: clarified def (axiom name) vs. description;

diff -r 768d14a67256 -r 9dd1079cec3a src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 15 19:45:05 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Nov 15 20:39:22 2009 +0100
@@ -1044,7 +1044,7 @@
     (* theory list -> term list *)
     val axioms_of_thys = maps Thm.axioms_of #> map (apsnd prop_of)
     val specs = Defs.all_specifications_of (Theory.defs_of thy)
-    val def_names = specs |> maps snd |> filter #is_def |> map #name
+    val def_names = specs |> maps snd |> map_filter #def
                     |> OrdList.make fast_string_ord
     val thys = thy :: Theory.ancestors_of thy
     val (built_in_thys, user_thys) = List.partition is_built_in_theory thys
diff -r 768d14a67256 -r 9dd1079cec3a src/Pure/defs.ML
--- a/src/Pure/defs.ML	Sun Nov 15 19:45:05 2009 +0100
+++ b/src/Pure/defs.ML	Sun Nov 15 20:39:22 2009 +0100
@@ -10,16 +10,16 @@
   val pretty_const: Pretty.pp -> string * typ list -> Pretty.T
   val plain_args: typ list -> bool
   type T
-  val all_specifications_of: T -> (string * {is_def: bool, name: string,
+  val all_specifications_of: T -> (string * {def: string option, description: string,
     lhs: typ list, rhs: (string * typ list) list} list) list
-  val specifications_of: T -> string -> {is_def: bool, name: string,
+  val specifications_of: T -> string -> {def: string option, description: string,
     lhs: typ list, rhs: (string * typ list) list} list
   val dest: T ->
    {restricts: ((string * typ list) * string) list,
     reducts: ((string * typ list) * (string * typ list) list) list}
   val empty: T
   val merge: Pretty.pp -> T * T -> T
-  val define: Pretty.pp -> bool -> bool -> string ->
+  val define: Pretty.pp -> bool -> string option -> string ->
     string * typ list -> (string * typ list) list -> T -> T
 end
 
@@ -52,7 +52,8 @@
 
 (* datatype defs *)
 
-type spec = {is_def: bool, name: string, lhs: args, rhs: (string * args) list};
+type spec =
+  {def: string option, description: string, lhs: args, rhs: (string * args) list};
 
 type def =
  {specs: spec Inttab.table,                 (*source specifications*)
@@ -86,7 +87,7 @@
 fun dest (Defs defs) =
   let
     val restricts = Symtab.fold (fn (c, {restricts, ...}) =>
-      fold (fn (args, name) => cons ((c, args), name)) restricts) defs [];
+      fold (fn (args, description) => cons ((c, args), description)) restricts) defs [];
     val reducts = Symtab.fold (fn (c, {reducts, ...}) =>
       fold (fn (args, deps) => cons ((c, args), deps)) reducts) defs [];
   in {restricts = restricts, reducts = reducts} end;
@@ -96,8 +97,8 @@
 
 (* specifications *)
 
-fun disjoint_specs c (i, {lhs = Ts, name = a, ...}: spec) =
-  Inttab.forall (fn (j, {lhs = Us, name = b, ...}: spec) =>
+fun disjoint_specs c (i, {lhs = Ts, description = a, ...}: spec) =
+  Inttab.forall (fn (j, {lhs = Us, description = b, ...}: spec) =>
     i = j orelse disjoint_args (Ts, Us) orelse
       error ("Clash of specifications " ^ quote a ^ " and " ^ quote b ^
         " for constant " ^ quote c));
@@ -132,9 +133,9 @@
 fun wellformed pp defs (c, args) (d, Us) =
   forall is_TVar Us orelse
   (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
-    SOME (Ts, name) =>
+    SOME (Ts, description) =>
       err pp (c, args) (d, Us) "Malformed"
-        ("\n(restriction " ^ prt pp (d, Ts) ^ " from " ^ quote name ^ ")")
+        ("\n(restriction " ^ prt pp (d, Ts) ^ " from " ^ quote description ^ ")")
   | NONE => true);
 
 fun reduction pp defs const deps =
@@ -201,14 +202,14 @@
 
 (* define *)
 
-fun define pp unchecked is_def name (c, args) deps (Defs defs) =
+fun define pp unchecked def description (c, args) deps (Defs defs) =
   let
     val restr =
       if plain_args args orelse
         (case args of [Type (_, rec_args)] => plain_args rec_args | _ => false)
-      then [] else [(args, name)];
+      then [] else [(args, description)];
     val spec =
-      (serial (), {is_def = is_def, name = name, lhs = args, rhs = deps});
+      (serial (), {def = def, description = description, lhs = args, rhs = deps});
     val defs' = defs |> update_specs c spec;
   in Defs (defs' |> (if unchecked then I else dependencies pp (c, args) restr deps)) end;
 
diff -r 768d14a67256 -r 9dd1079cec3a src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Nov 15 19:45:05 2009 +0100
+++ b/src/Pure/theory.ML	Sun Nov 15 20:39:22 2009 +0100
@@ -195,7 +195,7 @@
 
 (* dependencies *)
 
-fun dependencies thy unchecked is_def name lhs rhs =
+fun dependencies thy unchecked def description lhs rhs =
   let
     val pp = Syntax.pp_global thy;
     val consts = Sign.consts_of thy;
@@ -210,14 +210,14 @@
       if null rhs_extras then ()
       else error ("Specification depends on extra type variables: " ^
         commas_quote (map (Pretty.string_of_typ pp o TFree) rhs_extras) ^
-        "\nThe error(s) above occurred in " ^ quote name);
-  in Defs.define pp unchecked is_def name (prep lhs) (map prep rhs) end;
+        "\nThe error(s) above occurred in " ^ quote description);
+  in Defs.define pp unchecked def description (prep lhs) (map prep rhs) end;
 
 fun add_deps a raw_lhs raw_rhs thy =
   let
     val lhs :: rhs = map (dest_Const o Sign.cert_term thy o Const) (raw_lhs :: raw_rhs);
-    val name = if a = "" then (#1 lhs ^ " axiom") else a;
-  in thy |> map_defs (dependencies thy false false name lhs rhs) end;
+    val description = if a = "" then #1 lhs ^ " axiom" else a;
+  in thy |> map_defs (dependencies thy false NONE description lhs rhs) end;
 
 fun specify_const decl thy =
   let val (t as Const const, thy') = Sign.declare_const decl thy
@@ -256,7 +256,7 @@
     val (lhs_const, rhs) = Sign.cert_def ctxt tm;
     val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
     val _ = check_overloading thy overloaded lhs_const;
-  in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
+  in defs |> dependencies thy unchecked (SOME name) name lhs_const rhs_consts end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"),
     Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
@@ -290,7 +290,7 @@
     fun const_of (Const const) = const
       | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
       | const_of _ = error "Attempt to finalize non-constant term";
-    fun specify (c, T) = dependencies thy false false (c ^ " axiom") (c, T) [];
+    fun specify (c, T) = dependencies thy false NONE (c ^ " axiom") (c, T) [];
     val finalize = specify o check_overloading thy overloaded o const_of o
       Sign.cert_term thy o prep_term thy;
   in thy |> map_defs (fold finalize args) end;