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