src/HOL/Tools/SMT/z3_replay_rules.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (18 months ago)
changeset 67091 1393c2340eec
parent 58061 3d060f43accb
permissions -rw-r--r--
more symbols;
     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;