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