|
1 (* Title: HOL/Tools/SMT/z3_replay_rules.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Custom rules for Z3 proof replay. |
|
5 *) |
|
6 |
|
7 signature Z3_REPLAY_RULES = |
|
8 sig |
|
9 val apply: Proof.context -> cterm -> thm option |
|
10 end; |
|
11 |
|
12 structure Z3_Replay_Rules: Z3_REPLAY_RULES = |
|
13 struct |
|
14 |
|
15 structure Data = Generic_Data |
|
16 ( |
|
17 type T = thm Net.net |
|
18 val empty = Net.empty |
|
19 val extend = I |
|
20 val merge = Net.merge Thm.eq_thm |
|
21 ) |
|
22 |
|
23 fun maybe_instantiate ct thm = |
|
24 try Thm.first_order_match (Thm.cprop_of thm, ct) |
|
25 |> Option.map (fn inst => Thm.instantiate inst thm) |
|
26 |
|
27 fun apply ctxt ct = |
|
28 let |
|
29 val net = Data.get (Context.Proof ctxt) |
|
30 val xthms = Net.match_term net (Thm.term_of ct) |
|
31 |
|
32 fun select ct = map_filter (maybe_instantiate ct) xthms |
|
33 fun select' ct = |
|
34 let val thm = Thm.trivial ct |
|
35 in map_filter (try (fn rule => rule COMP thm)) xthms end |
|
36 |
|
37 in try hd (case select ct of [] => select' ct | xthms' => xthms') end |
|
38 |
|
39 val prep = `Thm.prop_of |
|
40 |
|
41 fun ins thm net = Net.insert_term Thm.eq_thm (prep thm) net handle Net.INSERT => net |
|
42 fun del thm net = Net.delete_term Thm.eq_thm (prep thm) net handle Net.DELETE => net |
|
43 |
|
44 val add = Thm.declaration_attribute (Data.map o ins) |
|
45 val del = Thm.declaration_attribute (Data.map o del) |
|
46 |
|
47 val name = Binding.name "z3_rule" |
|
48 |
|
49 val description = "declaration of Z3 proof rules" |
|
50 |
|
51 val _ = Theory.setup (Attrib.setup name (Attrib.add_del add del) description #> |
|
52 Global_Theory.add_thms_dynamic (name, Net.content o Data.get)) |
|
53 |
|
54 end; |