# HG changeset patch
# User boehmes
# Date 1257288256 -3600
# Node ID a3b002e2cd55a3c91d7198763991cd9698207c57
# Parent  281a01e5f68b552912c386c093096a7424b07930
proper and unique case names for the split_vc method,
shortened label names,
added an example demonstrating the split_vc method

diff -r 281a01e5f68b -r a3b002e2cd55 src/HOL/Boogie/Examples/Boogie_Max.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy	Tue Nov 03 19:32:08 2009 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy	Tue Nov 03 23:44:16 2009 +0100
@@ -38,12 +38,35 @@
 
 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max"
 
+text {*
+Approach 1: Discharge the verification condition fully automatically by SMT:
+*}
 boogie_vc b_max
   unfolding labels
   using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/Boogie_b_max"]]
   using [[z3_proofs=true]]
   by (smt boogie)
 
+text {*
+Approach 2: Split the verification condition, try to solve the splinters by
+a selection of automated proof tools, and show the remaining subgoals by an
+explicit proof. This approach is most useful in an interactive debug-and-fix
+mode. 
+*}
+boogie_vc b_max
+proof (split_vc (verbose) try: fast simp)
+  print_cases
+  case L_14_5c
+  thus ?case by (metis abs_of_nonneg zabs_less_one_iff zle_linear)
+next
+  case L_14_5b
+  thus ?case by (metis less_le_not_le linorder_not_le xt1(10) zle_linear
+    zless_add1_eq)
+next
+  case L_14_5a
+  thus ?case by (metis less_le_not_le zle_add1_eq_le zless_linear)
+qed
+
 boogie_end
 
 end
diff -r 281a01e5f68b -r a3b002e2cd55 src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Tue Nov 03 19:32:08 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Tue Nov 03 23:44:16 2009 +0100
@@ -398,8 +398,8 @@
       scan_line "label" (label_kind -- num -- num) -- exp >>
         (fn (((l, line), col), t) =>
           if line = 0 orelse col = 0 then t
-          else l $ Free ("Line_" ^ string_of_int line ^ "_Column_" ^
-            string_of_int col, @{typ bool}) $ t) ||
+          else l $ Free ("L_" ^ string_of_int line ^ "_" ^ string_of_int col,
+            @{typ bool}) $ t) ||
       scan_line "int-num" num >> HOLogic.mk_number @{typ int} ||
       binexp "<" (binop @{term "op < :: int => _"}) ||
       binexp "<=" (binop @{term "op <= :: int => _"}) ||
diff -r 281a01e5f68b -r a3b002e2cd55 src/HOL/Boogie/Tools/boogie_split.ML
--- a/src/HOL/Boogie/Tools/boogie_split.ML	Tue Nov 03 19:32:08 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_split.ML	Tue Nov 03 23:44:16 2009 +0100
@@ -53,9 +53,11 @@
 
     infix IF_UNSOLVED
     fun (tac1 IF_UNSOLVED tac2) i st = st |> (tac1 i THEN (fn st' =>
-      if i > i + nprems_of st' - nprems_of st
-      then (solved (); Tactical.all_tac st')
-      else Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st'))
+      let val j = i + Thm.nprems_of st' - Thm.nprems_of st
+      in
+        if i > j then (solved (); Tactical.all_tac st')
+        else Seq.INTERVAL tac2 i j st'
+      end))
     
     fun TRY_ALL [] _ st = (failed (); Tactical.no_tac st)
       | TRY_ALL ((name, tac) :: tacs) i st = (trying name;
@@ -69,32 +71,66 @@
   end
 
 
+(* case names *)
+
+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]))
+
+local
+  fun make_case_name (i, t) =
+    the_default ("B_" ^ string_of_int (i + 1)) (try case_name_of t)
+
+  val assert_intro = Thm.symmetric (as_meta_eq @{thm assert_at_def})
+  val l = Thm.dest_arg1 (Thm.rhs_of assert_intro)
+  fun intro new =
+    Conv.rewr_conv (Thm.instantiate ([], [(l, new)]) assert_intro)
+
+  val assert_eq = @{lemma "assert_at x t == assert_at y t"
+    by (simp add: assert_at_def)}
+  val (x, y) = pairself Thm.dest_arg1 (Thm.dest_binop (Thm.cprop_of assert_eq))
+  fun rename old new =
+    Conv.rewr_conv (Thm.instantiate ([], [(x, old), (y, new)]) assert_eq)
+
+  fun at_concl cv = Conv.concl_conv ~1 (Conv.arg_conv cv)
+  fun make_label thy name = Thm.cterm_of thy (Free (name, @{typ bool}))
+
+  fun rename_case thy new ct =
+    (case try case_name_of (Thm.term_of ct) of
+      NONE => at_concl (intro (make_label thy new))
+    | SOME old => if new = old then Conv.all_conv
+        else at_concl (rename (make_label thy old) (make_label thy new))) ct
+in
+fun unique_case_names thy st =
+  let
+    val names = map_index make_case_name (Thm.prems_of st)
+      |> ` (duplicates (op =)) |-> Name.variant_list
+  in ALLGOALS (fn i => CONVERSION (rename_case thy (nth names (i-1))) i) st end
+end
+
+
 (* splitting method *)
 
 local
-  fun case_name_of _ i = "goal" ^ string_of_int i
-    (*FIXME: proper case names*)
-
   val split_rules = [@{thm impI}, @{thm conjI}, @{thm TrueI}]
 
   fun prep_tac ctxt args facts =
-    Method.insert_tac facts
-    THEN' REPEAT_ALL_NEW (Tactic.resolve_tac split_rules)
-    THEN_ALL_NEW SUBGOAL (fn (t, i) =>
-      TRY (sub_tactics_tac ctxt args (case_name_of t i) i))
-
-  fun case_names st =
-    map_index (fn (i, t) => (case_name_of t (i + 1), [])) (Thm.prems_of st)
+    HEADGOAL (Method.insert_tac facts)
+    THEN HEADGOAL (REPEAT_ALL_NEW (Tactic.resolve_tac split_rules))
+    THEN unique_case_names (ProofContext.theory_of ctxt)
+    THEN ALLGOALS (SUBGOAL (fn (t, i) =>
+      TRY (sub_tactics_tac ctxt args (case_name_of t) i)))
 
   val drop_assert_at = Conv.concl_conv ~1 (Conv.try_conv (Conv.arg_conv
     (Conv.rewr_conv (as_meta_eq @{thm assert_at_def}))))
 
   fun split_vc args ctxt = METHOD_CASES (fn facts =>
-    prep_tac ctxt args facts 1 #>
+    prep_tac ctxt args facts #>
     Seq.maps (fn st =>
       st
       |> ALLGOALS (CONVERSION drop_assert_at)
-      |> Seq.map (pair (case_names st))) #>
+      |> Seq.map (pair (map (rpair [] o case_name_of) (Thm.prems_of st)))) #>
     Seq.maps (fn (names, st) =>
       CASES
         (Rule_Cases.make_common false