1(*  Title:      HOL/Tools/SMT/z3_replay_rules.ML
2    Author:     Sascha Boehme, TU Muenchen
3
4Custom rules for Z3 proof replay.
5*)
6
7signature Z3_REPLAY_RULES =
8sig
9  val apply: Proof.context -> cterm -> thm option
10end;
11
12structure Z3_Replay_Rules: Z3_REPLAY_RULES =
13struct
14
15structure 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
23fun 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
27fun 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
39val prep = `Thm.prop_of
40
41fun ins thm net = Net.insert_term Thm.eq_thm (prep thm) net handle Net.INSERT => net
42fun del thm net = Net.delete_term Thm.eq_thm (prep thm) net handle Net.DELETE => net
43
44val add = Thm.declaration_attribute (Data.map o ins)
45val del = Thm.declaration_attribute (Data.map o del)
46
47val name = Binding.name "z3_rule"
48
49val description = "declaration of Z3 proof rules"
50
51val _ = Theory.setup (Attrib.setup name (Attrib.add_del add del) description #>
52  Global_Theory.add_thms_dynamic (name, Net.content o Data.get))
53
54end;
55