1 (* Title: HOL/Boogie/Tools/boogie_tactics.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Boogie tactics and Boogie methods. |
|
5 *) |
|
6 |
|
7 signature BOOGIE_TACTICS = |
|
8 sig |
|
9 val unfold_labels_tac: Proof.context -> int -> tactic |
|
10 val boogie_tac: Proof.context -> thm list -> int -> tactic |
|
11 val boogie_all_tac: Proof.context -> thm list -> tactic |
|
12 val split: term -> (term list * term) list |
|
13 val split_tac: int -> tactic |
|
14 val drop_assert_at_tac: int -> tactic |
|
15 val setup: theory -> theory |
|
16 end |
|
17 |
|
18 structure Boogie_Tactics: BOOGIE_TACTICS = |
|
19 struct |
|
20 |
|
21 fun as_meta_eq eq = eq RS @{thm eq_reflection} |
|
22 |
|
23 val assert_at_def = as_meta_eq @{thm assert_at_def} |
|
24 val block_at_def = as_meta_eq @{thm block_at_def} |
|
25 val label_eqs = [assert_at_def, block_at_def] |
|
26 |
|
27 fun unfold_labels_tac ctxt = |
|
28 let val unfold = Conv.rewrs_conv label_eqs |
|
29 in CONVERSION (Conv.top_sweep_conv (K unfold) ctxt) end |
|
30 |
|
31 val boogie_rules = |
|
32 [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] @ |
|
33 [@{thm fun_upd_same}, @{thm fun_upd_apply}] |
|
34 |
|
35 fun boogie_tac ctxt rules = |
|
36 unfold_labels_tac ctxt |
|
37 THEN' SMT_Solver.smt_tac ctxt (Boogie_Axioms.get ctxt @ boogie_rules @ rules) |
|
38 |
|
39 fun boogie_all_tac ctxt rules = |
|
40 PARALLEL_GOALS (ALLGOALS (boogie_tac ctxt rules)) |
|
41 |
|
42 fun boogie_method all = |
|
43 Scan.optional Attrib.thms [] >> (fn thms => fn ctxt => METHOD (fn facts => |
|
44 let val tac = if all then boogie_all_tac else HEADGOAL oo boogie_tac |
|
45 in tac ctxt (thms @ facts) end)) |
|
46 |
|
47 val setup_boogie = Method.setup @{binding boogie} (boogie_method false) |
|
48 "apply an SMT solver to the current goal \ |
|
49 \using the current set of Boogie background axioms" |
|
50 |
|
51 val setup_boogie_all = Method.setup @{binding boogie_all} (boogie_method true) |
|
52 "apply an SMT solver to all goals \ |
|
53 \using the current set of Boogie background axioms" |
|
54 |
|
55 |
|
56 local |
|
57 fun explode_conj (@{term HOL.conj} $ t $ u) = explode_conj t @ explode_conj u |
|
58 | explode_conj t = [t] |
|
59 |
|
60 fun splt (ts, @{term HOL.implies} $ t $ u) = splt (ts @ explode_conj t, u) |
|
61 | splt (ts, @{term HOL.conj} $ t $ u) = splt (ts, t) @ splt (ts, u) |
|
62 | splt (ts, @{term assert_at} $ _ $ t) = [(ts, t)] |
|
63 | splt (_, @{term True}) = [] |
|
64 | splt tp = [tp] |
|
65 in |
|
66 fun split t = |
|
67 splt ([], HOLogic.dest_Trueprop t) |
|
68 |> map (fn (us, u) => (map HOLogic.mk_Trueprop us, HOLogic.mk_Trueprop u)) |
|
69 end |
|
70 |
|
71 val split_tac = REPEAT_ALL_NEW ( |
|
72 Tactic.resolve_tac [@{thm impI}, @{thm conjI}, @{thm TrueI}] |
|
73 ORELSE' Tactic.etac @{thm conjE}) |
|
74 |
|
75 val drop_assert_at_tac = CONVERSION (Conv.concl_conv ~1 (Conv.try_conv ( |
|
76 Conv.arg_conv (Conv.rewr_conv assert_at_def)))) |
|
77 |
|
78 local |
|
79 fun case_name_of t = |
|
80 (case HOLogic.dest_Trueprop (Logic.strip_imp_concl t) of |
|
81 @{term assert_at} $ Free (n, _) $ _ => n |
|
82 | _ => raise TERM ("case_name_of", [t])) |
|
83 |
|
84 fun boogie_cases ctxt = METHOD_CASES (fn facts => |
|
85 ALLGOALS (Method.insert_tac facts THEN' split_tac) #> |
|
86 Seq.maps (fn st => |
|
87 st |
|
88 |> ALLGOALS drop_assert_at_tac |
|
89 |> Seq.map (pair (map (rpair [] o case_name_of) (Thm.prems_of st)))) #> |
|
90 Seq.maps (fn (names, st) => |
|
91 CASES |
|
92 (Rule_Cases.make_common |
|
93 (Proof_Context.theory_of ctxt, |
|
94 Thm.prop_of (Rule_Cases.internalize_params st)) (map (rpair []) names)) |
|
95 all_tac st)) |
|
96 in |
|
97 val setup_boogie_cases = Method.setup @{binding boogie_cases} |
|
98 (Scan.succeed boogie_cases) |
|
99 "prepare a set of Boogie assertions for case-based proofs" |
|
100 end |
|
101 |
|
102 |
|
103 val setup = |
|
104 setup_boogie #> |
|
105 setup_boogie_all #> |
|
106 setup_boogie_cases |
|
107 |
|
108 end |
|