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