proper and unique case names for the split_vc method,
shortened label names,
added an example demonstrating the split_vc method
--- 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
--- 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 => _"}) ||
--- 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