--- 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 *)