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