merged

--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Wed Feb 24 22:09:50 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Wed Feb 24 22:45:14 2010 +0100
@@ -30,7 +30,8 @@
   VC_Take of int list * (bool * string list) option |
   VC_Only of string list |
   VC_Without of string list |
-  VC_Examine of string list 
+  VC_Examine of string list |
+  VC_Single of string
 
 fun get_vc thy vc_name =
   (case Boogie_VCs.lookup thy vc_name of
@@ -42,11 +43,37 @@
       | _ => error ("There is no verification condition " ^
           quote vc_name ^ ".")))
 
+local
+  fun split_goal t =
+    (case Boogie_Tactics.split t of
+      [tp] => tp
+    | _ => error "Multiple goals.")
+
+  fun single_prep t =
+    let
+      val (us, u) = split_goal t
+      val assms = [((@{binding vc_trace}, []), map (rpair []) us)]
+    in
+      pair [u] o snd o ProofContext.add_assms_i Assumption.assume_export assms
+    end
+
+  fun single_prove goal ctxt thm =
+    Goal.prove ctxt [] [] goal (fn {context, ...} => HEADGOAL (
+      Boogie_Tactics.split_tac
+      THEN' Boogie_Tactics.drop_assert_at_tac
+      THEN' SUBPROOF (fn _ => Tactic.rtac thm 1) context))
+in
 fun boogie_vc (vc_name, vc_opts) lthy =
   let
     val thy = ProofContext.theory_of lthy
     val vc = get_vc thy vc_name
 
+    fun extract vc l =
+      (case Boogie_VCs.extract vc l of
+        SOME vc' => vc'
+      | NONE => error ("There is no assertion to be proved with label " ^
+          quote l ^ "."))
+
     val vcs =
       (case vc_opts of
         VC_Complete => [vc]
@@ -55,18 +82,29 @@
       | VC_Take (ps, SOME (false, ls)) => [Boogie_VCs.paths_without ps ls vc]
       | VC_Only ls => [Boogie_VCs.only ls vc]
       | VC_Without ls => [Boogie_VCs.without ls vc]
-      | VC_Examine ls => map_filter (Boogie_VCs.extract vc) ls)
+      | VC_Examine ls => map (extract vc) ls
+      | VC_Single l => [extract vc l])
     val ts = map Boogie_VCs.prop_of_vc vcs
 
+    val (prepare, finish) =
+      (case vc_opts of
+         VC_Single _ => (single_prep (hd ts), single_prove (hd ts))
+      | _ => (pair ts, K I))
+
     val discharge = fold (Boogie_VCs.discharge o pair vc_name)
     fun after_qed [thms] = Local_Theory.theory (discharge (vcs ~~ thms))
       | after_qed _ = I
   in
     lthy
     |> fold Variable.auto_fixes ts
-    |> Proof.theorem_i NONE after_qed [map (rpair []) ts]
+    |> (fn lthy1 => lthy1
+    |> prepare
+    |-> (fn us => fn lthy2 => lthy2
+    |> Proof.theorem_i NONE (fn thmss => fn ctxt =>
+         let val export = map (finish lthy1) o ProofContext.export ctxt lthy2
+         in after_qed (map export thmss) ctxt end) [map (rpair []) us]))
   end
-
+end
 
 fun write_list head =
   map Pretty.str o sort (dict_ord string_ord o pairself explode) #>
@@ -239,7 +277,8 @@
 
 val vc_name = OuterParse.name
 
-val vc_labels = Scan.repeat1 OuterParse.name
+val vc_label = OuterParse.name
+val vc_labels = Scan.repeat1 vc_label
 
 val vc_paths =
   OuterParse.nat -- (Args.$$$ "-" |-- OuterParse.nat) >> (op upto) ||
@@ -247,13 +286,14 @@
 
 val vc_opts =
   scan_arg
-   (scan_val "examine" vc_labels >> VC_Examine ||
+   (scan_val "assertion" vc_label >> VC_Single ||
+    scan_val "examine" vc_labels >> VC_Examine ||
     scan_val "take" ((OuterParse.list vc_paths >> flat) -- Scan.option (
       scan_val "without" vc_labels >> pair false ||
       scan_val "and_also" vc_labels >> pair true) >> VC_Take) ||
     scan_val "only" vc_labels >> VC_Only ||
     scan_val "without" vc_labels >> VC_Without) ||
-  Scan.succeed VC_Complete  
+  Scan.succeed VC_Complete
 
 val _ =
   OuterSyntax.command "boogie_vc"

--- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Wed Feb 24 22:09:50 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Wed Feb 24 22:45:14 2010 +0100
@@ -9,6 +9,9 @@
   val unfold_labels_tac: Proof.context -> int -> tactic
   val boogie_tac: Proof.context -> thm list -> int -> tactic
   val boogie_all_tac: Proof.context -> thm list -> tactic
+  val split: term -> (term list * term) list
+  val split_tac: int -> tactic
+  val drop_assert_at_tac: int -> tactic
   val setup: theory -> theory
 end
 
@@ -47,25 +50,38 @@
 
 
 local
-  fun prep_tac facts =
-    Method.insert_tac facts
-    THEN' REPEAT_ALL_NEW
-      (Tactic.resolve_tac [@{thm impI}, @{thm conjI}, @{thm TrueI}]
-       ORELSE' Tactic.etac @{thm conjE})
+  fun explode_conj (@{term "op &"} $ t $ u) = explode_conj t @ explode_conj u
+    | explode_conj t = [t] 
 
-  val drop_assert_at = Conv.concl_conv ~1 (Conv.try_conv (Conv.arg_conv
-    (Conv.rewr_conv assert_at_def)))
+  fun splt (ts, @{term "op -->"} $ t $ u) = splt (ts @ explode_conj t, u)
+    | splt (ts, @{term "op &"} $ t $ u) = splt (ts, t) @ splt (ts, u)
+    | splt (ts, @{term assert_at} $ _ $ t) = [(ts, t)]
+    | splt (_, @{term True}) = []
+    | splt tp = [tp]
+in
+fun split t =
+  splt ([], HOLogic.dest_Trueprop t)
+  |> map (fn (us, u) => (map HOLogic.mk_Trueprop us, HOLogic.mk_Trueprop u))
+end
 
+val split_tac = REPEAT_ALL_NEW (
+  Tactic.resolve_tac [@{thm impI}, @{thm conjI}, @{thm TrueI}]
+  ORELSE' Tactic.etac @{thm conjE})
+
+val drop_assert_at_tac = CONVERSION (Conv.concl_conv ~1 (Conv.try_conv (
+  Conv.arg_conv (Conv.rewr_conv assert_at_def))))
+
+local
   fun case_name_of t =
     (case HOLogic.dest_Trueprop (Logic.strip_imp_concl t) of
       @{term assert_at} $ Free (n, _) $ _ => n
     | _ => raise TERM ("case_name_of", [t]))
 
   fun boogie_cases ctxt = METHOD_CASES (fn facts =>
-    ALLGOALS (prep_tac facts) #>
+    ALLGOALS (Method.insert_tac facts THEN' split_tac) #>
     Seq.maps (fn st =>
       st
-      |> ALLGOALS (CONVERSION drop_assert_at)
+      |> ALLGOALS drop_assert_at_tac
       |> Seq.map (pair (map (rpair [] o case_name_of) (Thm.prems_of st)))) #>
     Seq.maps (fn (names, st) =>
       CASES