|
(* Title: HOL/Tools/SMT/z3_replay_rules.ML
Author: Sascha Boehme, TU Muenchen
Custom rules for Z3 proof replay.
*)
signature Z3_REPLAY_RULES =
sig
val apply: Proof.context -> cterm -> thm option
end;
structure Z3_Replay_Rules: Z3_REPLAY_RULES =
struct
structure Data = Generic_Data
(
type T = thm Net.net
val empty = Net.empty
val extend = I
val merge = Net.merge Thm.eq_thm
)
fun maybe_instantiate ct thm =
try Thm.first_order_match (Thm.cprop_of thm, ct)
|> Option.map (fn inst => Thm.instantiate inst thm)
fun apply ctxt ct =
let
val net = Data.get (Context.Proof ctxt)
val xthms = Net.match_term net (Thm.term_of ct)
fun select ct = map_filter (maybe_instantiate ct) xthms
fun select' ct =
let val thm = Thm.trivial ct
in map_filter (try (fn rule => rule COMP thm)) xthms end
in try hd (case select ct of [] => select' ct | xthms' => xthms') end
val prep = `Thm.prop_of
fun ins thm net = Net.insert_term Thm.eq_thm (prep thm) net handle Net.INSERT => net
fun del thm net = Net.delete_term Thm.eq_thm (prep thm) net handle Net.DELETE => net
val add = Thm.declaration_attribute (Data.map o ins)
val del = Thm.declaration_attribute (Data.map o del)
val name = Binding.name "z3_rule"
val description = "declaration of Z3 proof rules"
val _ = Theory.setup (Attrib.setup name (Attrib.add_del add del) description #>
Global_Theory.add_thms_dynamic (name, Net.content o Data.get))
end;
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
