src/HOL/Tools/SMT/z3_replay_util.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (18 months ago)
changeset 67091 1393c2340eec
parent 62913 13252110a6fe
permissions -rw-r--r--
more symbols;
blanchet@58061
     1
(*  Title:      HOL/Tools/SMT/z3_replay_util.ML
blanchet@56078
     2
    Author:     Sascha Boehme, TU Muenchen
blanchet@56078
     3
blanchet@56078
     4
Helper functions required for Z3 proof replay.
blanchet@56078
     5
*)
blanchet@56078
     6
blanchet@58061
     7
signature Z3_REPLAY_UTIL =
blanchet@56078
     8
sig
blanchet@56078
     9
  (*theorem nets*)
blanchet@56078
    10
  val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
blanchet@56078
    11
  val net_instances: (int * thm) Net.net -> cterm -> (int * thm) list
blanchet@56078
    12
blanchet@56078
    13
  (*proof combinators*)
blanchet@56078
    14
  val under_assumption: (thm -> thm) -> cterm -> thm
blanchet@56078
    15
  val discharge: thm -> thm -> thm
blanchet@56078
    16
blanchet@56078
    17
  (*a faster COMP*)
wenzelm@60642
    18
  type compose_data = cterm list * (cterm -> cterm list) * thm
blanchet@56078
    19
  val precompose: (cterm -> cterm list) -> thm -> compose_data
blanchet@56078
    20
  val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
blanchet@56078
    21
  val compose: compose_data -> thm -> thm
blanchet@56078
    22
blanchet@56078
    23
  (*simpset*)
blanchet@56078
    24
  val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
blanchet@56078
    25
  val make_simpset: Proof.context -> thm list -> simpset
blanchet@57229
    26
end;
blanchet@56078
    27
blanchet@58061
    28
structure Z3_Replay_Util: Z3_REPLAY_UTIL =
blanchet@56078
    29
struct
blanchet@56078
    30
blanchet@56078
    31
(* theorem nets *)
blanchet@56078
    32
blanchet@56078
    33
fun thm_net_of f xthms =
blanchet@56078
    34
  let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm)
blanchet@56078
    35
  in fold insert xthms Net.empty end
blanchet@56078
    36
blanchet@56078
    37
fun maybe_instantiate ct thm =
blanchet@56078
    38
  try Thm.first_order_match (Thm.cprop_of thm, ct)
blanchet@56078
    39
  |> Option.map (fn inst => Thm.instantiate inst thm)
blanchet@56078
    40
blanchet@56078
    41
local
blanchet@56078
    42
  fun instances_from_net match f net ct =
blanchet@56078
    43
    let
blanchet@56078
    44
      val lookup = if match then Net.match_term else Net.unify_term
blanchet@56078
    45
      val xthms = lookup net (Thm.term_of ct)
blanchet@57230
    46
      fun select ct = map_filter (f (maybe_instantiate ct)) xthms
blanchet@56078
    47
      fun select' ct =
blanchet@56078
    48
        let val thm = Thm.trivial ct
blanchet@56078
    49
        in map_filter (f (try (fn rule => rule COMP thm))) xthms end
blanchet@56078
    50
    in (case select ct of [] => select' ct | xthms' => xthms') end
blanchet@56078
    51
in
blanchet@56078
    52
blanchet@56078
    53
fun net_instances net =
blanchet@56078
    54
  instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm))
blanchet@56078
    55
    net
blanchet@56078
    56
blanchet@56078
    57
end
blanchet@56078
    58
blanchet@56078
    59
blanchet@56078
    60
(* proof combinators *)
blanchet@56078
    61
blanchet@56078
    62
fun under_assumption f ct =
blanchet@58061
    63
  let val ct' = SMT_Util.mk_cprop ct in Thm.implies_intr ct' (f (Thm.assume ct')) end
blanchet@56078
    64
blanchet@56078
    65
fun discharge p pq = Thm.implies_elim pq p
blanchet@56078
    66
blanchet@56078
    67
blanchet@56078
    68
(* a faster COMP *)
blanchet@56078
    69
blanchet@56078
    70
type compose_data = cterm list * (cterm -> cterm list) * thm
blanchet@56078
    71
blanchet@56078
    72
fun list2 (x, y) = [x, y]
blanchet@56078
    73
wenzelm@60642
    74
fun precompose f rule : compose_data = (f (Thm.cprem_of rule 1), f, rule)
wenzelm@60642
    75
fun precompose2 f rule : compose_data = precompose (list2 o f) rule
blanchet@56078
    76
blanchet@56078
    77
fun compose (cvs, f, rule) thm =
wenzelm@60642
    78
  discharge thm
wenzelm@60642
    79
    (Thm.instantiate ([], map (dest_Var o Thm.term_of) cvs ~~ f (Thm.cprop_of thm)) rule)
blanchet@56078
    80
blanchet@56078
    81
blanchet@56078
    82
(* simpset *)
blanchet@56078
    83
blanchet@56078
    84
local
blanchet@56078
    85
  val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
blanchet@56078
    86
  val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
blanchet@56078
    87
  val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
blanchet@56078
    88
  val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
blanchet@56078
    89
blanchet@56078
    90
  fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
blanchet@56078
    91
  fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
blanchet@56078
    92
    | dest_binop t = raise TERM ("dest_binop", [t])
blanchet@56078
    93
wenzelm@61144
    94
  fun prove_antisym_le ctxt ct =
blanchet@56078
    95
    let
wenzelm@61144
    96
      val (le, r, s) = dest_binop (Thm.term_of ct)
blanchet@56078
    97
      val less = Const (@{const_name less}, Term.fastype_of le)
blanchet@56078
    98
      val prems = Simplifier.prems_of ctxt
blanchet@56078
    99
    in
blanchet@56078
   100
      (case find_first (eq_prop (le $ s $ r)) prems of
blanchet@56078
   101
        NONE =>
blanchet@56078
   102
          find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
blanchet@56078
   103
          |> Option.map (fn thm => thm RS antisym_less1)
blanchet@56078
   104
      | SOME thm => SOME (thm RS antisym_le1))
blanchet@56078
   105
    end
blanchet@56078
   106
    handle THM _ => NONE
blanchet@56078
   107
wenzelm@61144
   108
  fun prove_antisym_less ctxt ct =
blanchet@56078
   109
    let
wenzelm@61144
   110
      val (less, r, s) = dest_binop (HOLogic.dest_not (Thm.term_of ct))
blanchet@56078
   111
      val le = Const (@{const_name less_eq}, Term.fastype_of less)
blanchet@56078
   112
      val prems = Simplifier.prems_of ctxt
blanchet@56078
   113
    in
blanchet@56078
   114
      (case find_first (eq_prop (le $ r $ s)) prems of
blanchet@56078
   115
        NONE =>
blanchet@56078
   116
          find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
blanchet@56078
   117
          |> Option.map (fn thm => thm RS antisym_less2)
blanchet@56078
   118
      | SOME thm => SOME (thm RS antisym_le2))
blanchet@56078
   119
  end
blanchet@56078
   120
  handle THM _ => NONE
blanchet@56078
   121
blanchet@56078
   122
  val basic_simpset =
blanchet@56078
   123
    simpset_of (put_simpset HOL_ss @{context}
blanchet@56078
   124
      addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special
hoelzl@58776
   125
        arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def}
haftmann@60868
   126
      addsimprocs [@{simproc numeral_divmod},
wenzelm@61144
   127
        Simplifier.make_simproc @{context} "fast_int_arith"
wenzelm@61144
   128
         {lhss = [@{term "(m::int) < n"}, @{term "(m::int) \<le> n"}, @{term "(m::int) = n"}],
wenzelm@62913
   129
          proc = K Lin_Arith.simproc},
wenzelm@61144
   130
        Simplifier.make_simproc @{context} "antisym_le"
wenzelm@61144
   131
         {lhss = [@{term "(x::'a::order) \<le> y"}],
wenzelm@62913
   132
          proc = K prove_antisym_le},
wenzelm@61144
   133
        Simplifier.make_simproc @{context} "antisym_less"
wenzelm@61144
   134
         {lhss = [@{term "\<not> (x::'a::linorder) < y"}],
wenzelm@62913
   135
          proc = K prove_antisym_less}])
blanchet@56078
   136
blanchet@56078
   137
  structure Simpset = Generic_Data
blanchet@56078
   138
  (
blanchet@56078
   139
    type T = simpset
blanchet@56078
   140
    val empty = basic_simpset
blanchet@56078
   141
    val extend = I
blanchet@56078
   142
    val merge = Simplifier.merge_ss
blanchet@56078
   143
  )
blanchet@56078
   144
in
blanchet@56078
   145
blanchet@56078
   146
fun add_simproc simproc context =
blanchet@56078
   147
  Simpset.map (simpset_map (Context.proof_of context)
blanchet@56078
   148
    (fn ctxt => ctxt addsimprocs [simproc])) context
blanchet@56078
   149
blanchet@56078
   150
fun make_simpset ctxt rules =
blanchet@56078
   151
  simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt addsimps rules)
blanchet@56078
   152
blanchet@56078
   153
end
blanchet@56078
   154
blanchet@57229
   155
end;