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