start experimental implementation of revised new_specification

Based on Rob Arthan's "HOL Constant Definition Done Right". The tricky
part is deciding how and where to implement the existing definitional
rules that are theoretically subsumed by the new one.

src/0/Thm.sml

@@ -1143,6 +1143,14 @@ fun check_free_vars tm f =
             ("Free variables in rhs of definition: "
              :: commafy (map (Lib.quote o fst o dest_var) V)));
 
+fun check_vars tm vars f =
+ case Lib.set_diff (free_vars tm) vars
+  of [] => ()
+   | extras =>
+      raise f (String.concat
+         ("Unbound variable(s) in definition: "
+           :: commafy (map (Lib.quote o fst o dest_var) extras)));
+
 fun check_tyvars body_tyvars ty f =
  case Lib.set_diff body_tyvars (Type.type_vars ty)
   of [] => ()
@@ -1174,6 +1182,7 @@ in
   mk_defn_thm(tag thm, mk_exists(rep, list_mk_comb(TYDEF,[P,rep])))
 end
 
+(* subsumed by prim_specification
 fun prim_constant_definition Thy M = let
   val (lhs, rhs) = with_exn dest_eq M DEF_FORM_ERR
   val {Name, Thy, Ty} =
@@ -1196,25 +1205,38 @@ fun prim_constant_definition Thy M = let
 in
   mk_defn_thm(empty_tag, mk_eq(new_lhs, rhs))
 end
+*)
 
 fun bind thy s ty =
     Term.prim_new_const {Name = s, Thy = thy} ty
 
-fun prim_specification thyname cnames th = let
-  val con       = concl th
-  val checked   = check_null_hyp th SPEC_ERR
-  val checked   = check_free_vars con SPEC_ERR
-  val checked   =
+fun prim_specification thyname th = let
+  val hyps        = hypset th
+  val stys        =
+    let
+      fun foldthis (tm,stys) =
+        let
+          val (l,r)   =
+              with_exn dest_eq tm (SPEC_ERR "non-equational hypothesis")
+          val (s,ty)  =
+              with_exn dest_var l (SPEC_ERR "lhs of hyp not a variable")
+          val checked = check_free_vars r SPEC_ERR
+          val checked = check_tyvars (type_vars_in_term r) ty SPEC_ERR
+        in
+          (s,ty)::stys
+        end
+    in
+      HOLset.foldl foldthis [] hyps
+    end
+  val cnames      = List.map fst stys
+  val checked     =
       assert_exn (op=) (length(mk_set cnames),length cnames)
                  (SPEC_ERR "duplicate constant names in specification")
-  val (V,body)  =
-      with_exn (nstrip_exists (length cnames)) con
-               (SPEC_ERR "too few existentially quantified variables")
-  fun vOK V v   = check_tyvars V (type_of v) SPEC_ERR
-  val checked   = List.app (vOK (type_vars_in_term body)) V
-  fun addc v s  = v |-> bind thyname s (snd(dest_var v))
+  val body        = concl th
+  val checked     = check_vars body (List.map mk_var stys) SPEC_ERR
+  fun addc (s,ty) = (mk_var (s,ty)) |-> bind thyname s ty
 in
-  mk_defn_thm (tag th, subst (map2 addc V cnames) body)
+  (cnames, mk_defn_thm (tag th, subst (List.map addc stys) body))
 end
 
 

src/postkernel/Theory.sig

@@ -75,6 +75,7 @@ sig
 (* Extensions by definition *)
   structure Definition : sig
     val new_type_definition    : string * thm -> thm
+    val loose_specification    : string * thm -> thm
     val new_definition         : string * term -> thm
     val new_specification      : string * string list * thm -> thm
 

src/postkernel/Theory.sml

@@ -1071,6 +1071,17 @@ fun new_type_definition (name,thm) = let
  end
  handle e => raise (wrap_exn "Theory.Definition" "new_type_definition" e);
 
+fun loose_specification(name, th) = let
+  val thy = current_theory()
+  val (cnames,def) = Thm.prim_specification thy th
+ in
+  store_definition (name, def) before
+  List.app (fn s => call_hooks (TheoryDelta.NewConstant{Name=s, Thy=thy}))
+           cnames
+ end
+ handle e => raise (wrap_exn "Definition" "loose_specification" e);
+
+(* TODO: implement these two in terms of the above
 
 fun new_definition(name,M) =
  let val (dest,post) = !new_definition_hook
@@ -1094,6 +1105,8 @@ fun new_specification (name, cnames, th) = let
  end
  handle e => raise (wrap_exn "Definition" "new_specification" e);
 
+*)
+
 end (* Definition struct *)
 
 end (* Theory *)

src/prekernel/FinalThm-sig.sml

@@ -110,8 +110,7 @@ sig
 
   (* definitional rules of inference *)
   val prim_type_definition : {Thy : string, Tyop : string} * thm -> thm
-  val prim_constant_definition : string -> term -> thm
-  val prim_specification : string -> string list -> thm -> thm
+  val prim_specification : string -> thm -> string list * thm
 
   (* Fetching theorems from disk *)