equal
deleted
inserted
replaced
4 Boogie tactics and Boogie methods. |
4 Boogie tactics and Boogie methods. |
5 *) |
5 *) |
6 |
6 |
7 signature BOOGIE_TACTICS = |
7 signature BOOGIE_TACTICS = |
8 sig |
8 sig |
|
9 val unfold_labels_tac: Proof.context -> int -> tactic |
9 val boogie_tac: Proof.context -> thm list -> int -> tactic |
10 val boogie_tac: Proof.context -> thm list -> int -> tactic |
10 val boogie_all_tac: Proof.context -> thm list -> tactic |
11 val boogie_all_tac: Proof.context -> thm list -> tactic |
11 val setup: theory -> theory |
12 val setup: theory -> theory |
12 end |
13 end |
13 |
14 |
47 |
48 |
48 local |
49 local |
49 fun prep_tac facts = |
50 fun prep_tac facts = |
50 Method.insert_tac facts |
51 Method.insert_tac facts |
51 THEN' REPEAT_ALL_NEW |
52 THEN' REPEAT_ALL_NEW |
52 (Tactic.resolve_tac [@{thm impI}, @{thm conjI}, @{thm TrueI}] |
53 (Tactic.resolve_tac [@{thm impI}, @{thm conjI}, @{thm TrueI}] |
53 ORELSE' Tactic.eresolve_tac [@{thm conjE}, @{thm TrueE}]) |
54 ORELSE' Tactic.etac @{thm conjE}) |
54 |
55 |
55 val drop_assert_at = Conv.concl_conv ~1 (Conv.try_conv (Conv.arg_conv |
56 val drop_assert_at = Conv.concl_conv ~1 (Conv.try_conv (Conv.arg_conv |
56 (Conv.rewr_conv assert_at_def))) |
57 (Conv.rewr_conv assert_at_def))) |
57 |
58 |
58 fun case_name_of t = |
59 fun case_name_of t = |