src/HOL/Tools/SMT2/z3_new_proof_rules.ML
author blanchet
Thu Mar 13 13:18:13 2014 +0100 (2014-03-13)
changeset 56078 624faeda77b5
permissions -rw-r--r--
moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle
blanchet@56078
     1
(*  Title:      HOL/Tools/SMT2/z3_new_proof_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@56078
     7
signature Z3_NEW_PROOF_RULES =
blanchet@56078
     8
sig
blanchet@56078
     9
  val apply: Proof.context -> cterm -> thm option
blanchet@56078
    10
end
blanchet@56078
    11
blanchet@56078
    12
structure Z3_New_Proof_Rules: Z3_NEW_PROOF_RULES =
blanchet@56078
    13
struct
blanchet@56078
    14
blanchet@56078
    15
val eq = Thm.eq_thm
blanchet@56078
    16
blanchet@56078
    17
structure Data = Generic_Data
blanchet@56078
    18
(
blanchet@56078
    19
  type T = thm Net.net
blanchet@56078
    20
  val empty = Net.empty
blanchet@56078
    21
  val extend = I
blanchet@56078
    22
  val merge = Net.merge eq
blanchet@56078
    23
)
blanchet@56078
    24
blanchet@56078
    25
fun maybe_instantiate ct thm =
blanchet@56078
    26
  try Thm.first_order_match (Thm.cprop_of thm, ct)
blanchet@56078
    27
  |> Option.map (fn inst => Thm.instantiate inst thm)
blanchet@56078
    28
blanchet@56078
    29
fun apply ctxt ct =
blanchet@56078
    30
  let
blanchet@56078
    31
    val net = Data.get (Context.Proof ctxt)
blanchet@56078
    32
    val xthms = Net.match_term net (Thm.term_of ct)
blanchet@56078
    33
blanchet@56078
    34
    fun select ct = map_filter (maybe_instantiate ct) xthms 
blanchet@56078
    35
    fun select' ct =
blanchet@56078
    36
      let val thm = Thm.trivial ct
blanchet@56078
    37
      in map_filter (try (fn rule => rule COMP thm)) xthms end
blanchet@56078
    38
blanchet@56078
    39
  in try hd (case select ct of [] => select' ct | xthms' => xthms') end
blanchet@56078
    40
blanchet@56078
    41
val prep = `Thm.prop_of
blanchet@56078
    42
blanchet@56078
    43
fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
blanchet@56078
    44
fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
blanchet@56078
    45
blanchet@56078
    46
val add = Thm.declaration_attribute (Data.map o ins)
blanchet@56078
    47
val del = Thm.declaration_attribute (Data.map o del)
blanchet@56078
    48
blanchet@56078
    49
val name = Binding.name "z3_new_rule"
blanchet@56078
    50
blanchet@56078
    51
val description = "declaration of Z3 proof rules"
blanchet@56078
    52
blanchet@56078
    53
val _ = Theory.setup (Attrib.setup name (Attrib.add_del add del) description #>
blanchet@56078
    54
  Global_Theory.add_thms_dynamic (name, Net.content o Data.get))
blanchet@56078
    55
blanchet@56078
    56
end