equal
deleted
inserted
replaced
36 \end{verbatim} |
36 \end{verbatim} |
37 *} |
37 *} |
38 |
38 |
39 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max" |
39 boogie_open "~~/src/HOL/Boogie/Examples/Boogie_Max" |
40 |
40 |
|
41 text {* |
|
42 Approach 1: Discharge the verification condition fully automatically by SMT: |
|
43 *} |
41 boogie_vc b_max |
44 boogie_vc b_max |
42 unfolding labels |
45 unfolding labels |
43 using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/Boogie_b_max"]] |
46 using [[smt_cert="~~/src/HOL/Boogie/Examples/cert/Boogie_b_max"]] |
44 using [[z3_proofs=true]] |
47 using [[z3_proofs=true]] |
45 by (smt boogie) |
48 by (smt boogie) |
46 |
49 |
|
50 text {* |
|
51 Approach 2: Split the verification condition, try to solve the splinters by |
|
52 a selection of automated proof tools, and show the remaining subgoals by an |
|
53 explicit proof. This approach is most useful in an interactive debug-and-fix |
|
54 mode. |
|
55 *} |
|
56 boogie_vc b_max |
|
57 proof (split_vc (verbose) try: fast simp) |
|
58 print_cases |
|
59 case L_14_5c |
|
60 thus ?case by (metis abs_of_nonneg zabs_less_one_iff zle_linear) |
|
61 next |
|
62 case L_14_5b |
|
63 thus ?case by (metis less_le_not_le linorder_not_le xt1(10) zle_linear |
|
64 zless_add1_eq) |
|
65 next |
|
66 case L_14_5a |
|
67 thus ?case by (metis less_le_not_le zle_add1_eq_le zless_linear) |
|
68 qed |
|
69 |
47 boogie_end |
70 boogie_end |
48 |
71 |
49 end |
72 end |