src/Pure/Isar/specification.ML

--- a/src/Pure/Isar/specification.ML	Thu Mar 12 21:33:06 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Mar 12 21:37:18 2009 +0100
@@ -8,16 +8,22 @@
 signature SPECIFICATION =
 sig
   val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
+  val check_spec:
+    (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
+    (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
+  val read_spec:
+    (binding * string option * mixfix) list -> (Attrib.binding * string) list -> Proof.context ->
+    (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
+  val check_free_spec:
+    (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
+    (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
+  val read_free_spec:
+    (binding * string option * mixfix) list -> (Attrib.binding * string) list -> Proof.context ->
+    (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
   val check_specification: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term list) list list -> Proof.context ->
+    (Attrib.binding * term list) list -> Proof.context ->
     (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   val read_specification: (binding * string option * mixfix) list ->
-    (Attrib.binding * string list) list list -> Proof.context ->
-    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
-  val check_free_specification: (binding * typ option * mixfix) list ->
-    (Attrib.binding * term list) list -> Proof.context ->
-    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
-  val read_free_specification: (binding * string option * mixfix) list ->
     (Attrib.binding * string list) list -> Proof.context ->
     (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   val axiomatization: (binding * typ option * mixfix) list ->
@@ -97,7 +103,7 @@
       in fold_rev close bounds A end;
   in map close_form As end;
 
-fun prep_spec prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt =
+fun prepare prep_vars parse_prop prep_att do_close raw_vars raw_specss ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
 
@@ -122,15 +128,30 @@
     val name_atts = map (fn ((name, atts), _) => (name, map (prep_att thy) atts)) (flat raw_specss);
   in ((params, name_atts ~~ specs), specs_ctxt) end;
 
-fun read_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src x;
-fun check_spec x = prep_spec ProofContext.cert_vars (K I) (K I) x;
+
+fun single_spec (a, prop) = [(a, [prop])];
+fun the_spec (a, [prop]) = (a, prop);
+
+fun prep_spec prep_vars parse_prop prep_att do_close vars specs =
+  prepare prep_vars parse_prop prep_att do_close
+    vars (map single_spec specs) #>> apsnd (map the_spec);
+
+fun prep_specification prep_vars parse_prop prep_att vars specs =
+  prepare prep_vars parse_prop prep_att true [specs];
 
 in
 
-fun read_specification x = read_spec true x;
-fun check_specification x = check_spec true x;
-fun read_free_specification vars specs = read_spec false vars [specs];
-fun check_free_specification vars specs = check_spec false vars [specs];
+fun check_spec x = prep_spec ProofContext.cert_vars (K I) (K I) true x;
+fun read_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src true x;
+
+fun check_free_spec x = prep_spec ProofContext.cert_vars (K I) (K I) false x;
+fun read_free_spec x = prep_spec ProofContext.read_vars Syntax.parse_prop Attrib.intern_src false x;
+
+fun check_specification vars specs =
+  prepare ProofContext.cert_vars (K I) (K I) true vars [specs];
+
+fun read_specification vars specs =
+  prepare ProofContext.read_vars Syntax.parse_prop Attrib.intern_src true vars [specs];
 
 end;
 
@@ -139,7 +160,7 @@
 
 fun gen_axioms do_print prep raw_vars raw_specs thy =
   let
-    val ((vars, specs), _) = prep raw_vars [raw_specs] (ProofContext.init thy);
+    val ((vars, specs), _) = prep raw_vars raw_specs (ProofContext.init thy);
     val xs = map (fn ((b, T), _) => (Binding.name_of b, T)) vars;
 
     (*consts*)
@@ -168,10 +189,9 @@
 
 (* definition *)
 
-fun gen_def do_print prep (raw_var, (raw_a, raw_prop)) lthy =
+fun gen_def do_print prep (raw_var, raw_spec) lthy =
   let
-    val (vars, [((raw_name, atts), [prop])]) =
-      fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
+    val (vars, [((raw_name, atts), prop)]) = fst (prep (the_list raw_var) [raw_spec] lthy);
     val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
     val var as (b, _) =
       (case vars of
@@ -197,16 +217,16 @@
       else print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
   in ((lhs, (def_name, th')), lthy3) end;
 
-val definition = gen_def false check_free_specification;
-val definition_cmd = gen_def true read_free_specification;
+val definition = gen_def false check_free_spec;
+val definition_cmd = gen_def true read_free_spec;
 
 
 (* abbreviation *)
 
 fun gen_abbrev do_print prep mode (raw_var, raw_prop) lthy =
   let
-    val ((vars, [(_, [prop])]), _) =
-      prep (the_list raw_var) [(("", []), [raw_prop])]
+    val ((vars, [(_, prop)]), _) =
+      prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
         (lthy |> ProofContext.set_mode ProofContext.mode_abbrev);
     val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
     val var =
@@ -227,8 +247,8 @@
     val _ = if not do_print then () else print_consts lthy' (K false) [(x, T)];
   in lthy' end;
 
-val abbreviation = gen_abbrev false check_free_specification;
-val abbreviation_cmd = gen_abbrev true read_free_specification;
+val abbreviation = gen_abbrev false check_free_spec;
+val abbreviation_cmd = gen_abbrev true read_free_spec;
 
 
 (* notation *)