| author | wenzelm |
| Sun, 25 Apr 2010 16:10:05 +0200 | |
| changeset 36324 | 7cd5057a5bb8 |
| parent 35356 | 5c937073e1d5 |
| child 36936 | c52d1c130898 |
| permissions | -rw-r--r-- |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
1 |
(* Title: HOL/Boogie/Tools/boogie_tactics.ML |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
3 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
4 |
Boogie tactics and Boogie methods. |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
5 |
*) |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
6 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
7 |
signature BOOGIE_TACTICS = |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
8 |
sig |
|
34181
003333ffa543
merged verification condition structure and term representation in one datatype,
boehmes
parents:
34068
diff
changeset
|
9 |
val unfold_labels_tac: Proof.context -> int -> tactic |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
10 |
val boogie_tac: Proof.context -> thm list -> int -> tactic |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
11 |
val boogie_all_tac: Proof.context -> thm list -> tactic |
|
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
12 |
val split: term -> (term list * term) list |
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
13 |
val split_tac: int -> tactic |
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
14 |
val drop_assert_at_tac: int -> tactic |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
15 |
val setup: theory -> theory |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
16 |
end |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
17 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
18 |
structure Boogie_Tactics: BOOGIE_TACTICS = |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
19 |
struct |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
20 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
21 |
fun as_meta_eq eq = eq RS @{thm eq_reflection}
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
22 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
23 |
val assert_at_def = as_meta_eq @{thm assert_at_def}
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
24 |
val block_at_def = as_meta_eq @{thm block_at_def}
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
25 |
val label_eqs = [assert_at_def, block_at_def] |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
26 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
27 |
fun unfold_labels_tac ctxt = |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
28 |
let val unfold = More_Conv.rewrs_conv label_eqs |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
29 |
in CONVERSION (More_Conv.top_sweep_conv (K unfold) ctxt) end |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
30 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
31 |
fun boogie_tac ctxt rules = |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
32 |
unfold_labels_tac ctxt |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
33 |
THEN' SMT_Solver.smt_tac ctxt (Boogie_Axioms.get ctxt @ rules) |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
34 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
35 |
fun boogie_all_tac ctxt rules = |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
36 |
PARALLEL_GOALS (HEADGOAL (boogie_tac ctxt rules)) |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
37 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
38 |
fun boogie_method all = |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
39 |
Scan.optional Attrib.thms [] >> (fn thms => fn ctxt => METHOD (fn facts => |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
40 |
let val tac = if all then boogie_all_tac else HEADGOAL oo boogie_tac |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
41 |
in tac ctxt (thms @ facts) end)) |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
42 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
43 |
val setup_boogie = Method.setup @{binding boogie} (boogie_method false)
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
44 |
("Applies an SMT solver to the current goal " ^
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
45 |
"using the current set of Boogie background axioms") |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
46 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
47 |
val setup_boogie_all = Method.setup @{binding boogie_all} (boogie_method true)
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
48 |
("Applies an SMT solver to all goals " ^
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
49 |
"using the current set of Boogie background axioms") |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
50 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
51 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
52 |
local |
|
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
53 |
fun explode_conj (@{term "op &"} $ t $ u) = explode_conj t @ explode_conj u
|
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
54 |
| explode_conj t = [t] |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
55 |
|
|
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
56 |
fun splt (ts, @{term "op -->"} $ t $ u) = splt (ts @ explode_conj t, u)
|
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
57 |
| splt (ts, @{term "op &"} $ t $ u) = splt (ts, t) @ splt (ts, u)
|
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
58 |
| splt (ts, @{term assert_at} $ _ $ t) = [(ts, t)]
|
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
59 |
| splt (_, @{term True}) = []
|
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
60 |
| splt tp = [tp] |
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
61 |
in |
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
62 |
fun split t = |
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
63 |
splt ([], HOLogic.dest_Trueprop t) |
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
64 |
|> map (fn (us, u) => (map HOLogic.mk_Trueprop us, HOLogic.mk_Trueprop u)) |
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
65 |
end |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
66 |
|
|
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
67 |
val split_tac = REPEAT_ALL_NEW ( |
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
68 |
Tactic.resolve_tac [@{thm impI}, @{thm conjI}, @{thm TrueI}]
|
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
69 |
ORELSE' Tactic.etac @{thm conjE})
|
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
70 |
|
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
71 |
val drop_assert_at_tac = CONVERSION (Conv.concl_conv ~1 (Conv.try_conv ( |
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
72 |
Conv.arg_conv (Conv.rewr_conv assert_at_def)))) |
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
73 |
|
|
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
74 |
local |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
75 |
fun case_name_of t = |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
76 |
(case HOLogic.dest_Trueprop (Logic.strip_imp_concl t) of |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
77 |
@{term assert_at} $ Free (n, _) $ _ => n
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
78 |
| _ => raise TERM ("case_name_of", [t]))
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
79 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
80 |
fun boogie_cases ctxt = METHOD_CASES (fn facts => |
|
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
81 |
ALLGOALS (Method.insert_tac facts THEN' split_tac) #> |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
82 |
Seq.maps (fn st => |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
83 |
st |
|
35356
5c937073e1d5
added variant of boogie_vc to prove a single assertion: keep premises (i.e. the trace up this assertion) as facts in the context (and not as part of the goal) to increase performance when dealing with large goals
boehmes
parents:
34916
diff
changeset
|
84 |
|> ALLGOALS drop_assert_at_tac |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
85 |
|> Seq.map (pair (map (rpair [] o case_name_of) (Thm.prems_of st)))) #> |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
86 |
Seq.maps (fn (names, st) => |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
87 |
CASES |
|
34916
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34181
diff
changeset
|
88 |
(Rule_Cases.make_common |
|
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34181
diff
changeset
|
89 |
(ProofContext.theory_of ctxt, |
|
f625d8d6fcf3
Eliminated is_open option of Rule_Cases.make_nested/make_common;
berghofe
parents:
34181
diff
changeset
|
90 |
Thm.prop_of (Rule_Cases.internalize_params st)) names) |
|
34068
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
91 |
Tactical.all_tac st)) |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
92 |
in |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
93 |
val setup_boogie_cases = Method.setup @{binding boogie_cases}
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
94 |
(Scan.succeed boogie_cases) |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
95 |
"Prepares a set of Boogie assertions for case-based proofs" |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
96 |
end |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
97 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
98 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
99 |
val setup = |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
100 |
setup_boogie #> |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
101 |
setup_boogie_all #> |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
102 |
setup_boogie_cases |
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
103 |
|
|
a78307d72e58
make assertion labels unique already when loading a verification condition,
boehmes
parents:
diff
changeset
|
104 |
end |