# HG changeset patch
# User berghofe
# Date 1299256770 -3600
# Node ID 582cccdda0ed4c4494dab3754cc8034efbce3d3b
# Parent  a2e9af953b901070c2eb7d66505bf877dfc01a17
spark_end now joins proofs of VCs before writing *.prv file.

diff -r a2e9af953b90 -r 582cccdda0ed src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri Mar 04 11:43:20 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Fri Mar 04 17:39:30 2011 +0100
@@ -45,7 +45,7 @@
 fun get_vc thy vc_name =
   (case SPARK_VCs.lookup_vc thy vc_name of
     SOME (ctxt, (_, proved, ctxt', stmt)) =>
-      if proved then
+      if is_some proved then
         error ("The verification condition " ^
           quote vc_name ^ " has already been proved.")
       else (ctxt @ [ctxt'], stmt)
@@ -58,12 +58,13 @@
     val (ctxt, stmt) = get_vc thy vc_name
   in
     Specification.theorem Thm.theoremK NONE
-      (K (Local_Theory.background_theory (SPARK_VCs.mark_proved vc_name)))
+      (fn thmss => (Local_Theory.background_theory
+         (SPARK_VCs.mark_proved vc_name (flat thmss))))
       (Binding.name vc_name, []) ctxt stmt true lthy
   end;
 
-fun string_of_status false = "(unproved)"
-  | string_of_status true = "(proved)";
+fun string_of_status NONE = "(unproved)"
+  | string_of_status (SOME _) = "(proved)";
 
 fun show_status (p, f) = Toplevel.no_timing o Toplevel.keep (fn state =>
   let
@@ -131,8 +132,8 @@
     Keyword.diag
     (Scan.optional
        (Args.parens
-          (   Args.$$$ "proved" >> K (I, K "")
-           || Args.$$$ "unproved" >> K (not, K "")))
+          (   Args.$$$ "proved" >> K (is_some, K "")
+           || Args.$$$ "unproved" >> K (is_none, K "")))
        (K true, string_of_status) >> show_status);
 
 val _ =
diff -r a2e9af953b90 -r 582cccdda0ed src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Mar 04 11:43:20 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Mar 04 17:39:30 2011 +0100
@@ -13,11 +13,11 @@
     string * ((string list * string) option * 'a) ->
     theory -> theory
   val lookup_vc: theory -> string -> (Element.context_i list *
-    (string * bool * Element.context_i * Element.statement_i)) option
+    (string * thm list option * Element.context_i * Element.statement_i)) option
   val get_vcs: theory ->
-    Element.context_i list * (binding * thm) list *
-    (string * (string * bool * Element.context_i * Element.statement_i)) list
-  val mark_proved: string -> theory -> theory
+    Element.context_i list * (binding * thm) list * (string *
+    (string * thm list option * Element.context_i * Element.statement_i)) list
+  val mark_proved: string -> thm list -> theory -> theory
   val close: theory -> theory
   val is_closed: theory -> bool
 end;
@@ -616,7 +616,7 @@
         funs: (string list * string) tab,
         ids: (term * string) Symtab.table * Name.context,
         proving: bool,
-        vcs: (string * bool *
+        vcs: (string * thm list option *
           (string * expr) list * (string * expr) list) VCtab.table,
         path: Path.T} option}
   val empty : T = {pfuns = Symtab.empty, env = NONE}
@@ -713,27 +713,28 @@
       end
   | _ => ([], [], []));
 
-fun mark_proved name = VCs.map (fn
+fun mark_proved name thms = VCs.map (fn
     {pfuns, env = SOME {ctxt, defs, types, funs, ids, vcs, path, ...}} =>
       {pfuns = pfuns,
        env = SOME {ctxt = ctxt, defs = defs,
          types = types, funs = funs, ids = ids,
          proving = true,
          vcs = VCtab.map_entry name (fn (trace, _, ps, cs) =>
-           (trace, true, ps, cs)) vcs,
+           (trace, SOME thms, ps, cs)) vcs,
          path = path}}
   | x => x);
 
 fun close thy = VCs.map (fn
     {pfuns, env = SOME {vcs, path, ...}} =>
-      (case VCtab.fold_rev (fn (s, (_, p, _, _)) =>
-           (if p then apfst else apsnd) (cons s)) vcs ([], []) of
+      (case VCtab.fold_rev (fn vc as (_, (_, p, _, _)) =>
+           (if is_some p then apfst else apsnd) (cons vc)) vcs ([], []) of
          (proved, []) =>
-           (File.write (Path.ext "prv" path)
-              (concat (map (fn s => snd (strip_number s) ^
+           (Thm.join_proofs (maps (the o #2 o snd) proved);
+            File.write (Path.ext "prv" path)
+              (concat (map (fn (s, _) => snd (strip_number s) ^
                  " -- proved by " ^ Distribution.version ^ "\n") proved));
             {pfuns = pfuns, env = NONE})
-       | (_, unproved) => err_vcs unproved)
+       | (_, unproved) => err_vcs (map fst unproved))
   | x => x) thy;
 
 
@@ -834,7 +835,7 @@
       else warning ("Ignoring rules: " ^ rulenames rules'');
 
     val vcs' = VCtab.make (maps (fn (tr, vcs) =>
-      map (fn (s, (ps, cs)) => (s, (tr, false, ps, cs)))
+      map (fn (s, (ps, cs)) => (s, (tr, NONE, ps, cs)))
         (filter_out (is_trivial_vc o snd) vcs)) vcs);
 
     val _ = (case filter_out (is_some o lookup funs)