src/HOL/Tools/SMT/z3_replay_util.ML
changeset 58061 3d060f43accb
parent 57230 ec5ff6bb2a92
child 58776 95e58e04e534
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/SMT/z3_replay_util.ML	Thu Aug 28 00:40:38 2014 +0200
     1.3 @@ -0,0 +1,150 @@
     1.4 +(*  Title:      HOL/Tools/SMT/z3_replay_util.ML
     1.5 +    Author:     Sascha Boehme, TU Muenchen
     1.6 +
     1.7 +Helper functions required for Z3 proof replay.
     1.8 +*)
     1.9 +
    1.10 +signature Z3_REPLAY_UTIL =
    1.11 +sig
    1.12 +  (*theorem nets*)
    1.13 +  val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
    1.14 +  val net_instances: (int * thm) Net.net -> cterm -> (int * thm) list
    1.15 +
    1.16 +  (*proof combinators*)
    1.17 +  val under_assumption: (thm -> thm) -> cterm -> thm
    1.18 +  val discharge: thm -> thm -> thm
    1.19 +
    1.20 +  (*a faster COMP*)
    1.21 +  type compose_data
    1.22 +  val precompose: (cterm -> cterm list) -> thm -> compose_data
    1.23 +  val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
    1.24 +  val compose: compose_data -> thm -> thm
    1.25 +
    1.26 +  (*simpset*)
    1.27 +  val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
    1.28 +  val make_simpset: Proof.context -> thm list -> simpset
    1.29 +end;
    1.30 +
    1.31 +structure Z3_Replay_Util: Z3_REPLAY_UTIL =
    1.32 +struct
    1.33 +
    1.34 +(* theorem nets *)
    1.35 +
    1.36 +fun thm_net_of f xthms =
    1.37 +  let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm)
    1.38 +  in fold insert xthms Net.empty end
    1.39 +
    1.40 +fun maybe_instantiate ct thm =
    1.41 +  try Thm.first_order_match (Thm.cprop_of thm, ct)
    1.42 +  |> Option.map (fn inst => Thm.instantiate inst thm)
    1.43 +
    1.44 +local
    1.45 +  fun instances_from_net match f net ct =
    1.46 +    let
    1.47 +      val lookup = if match then Net.match_term else Net.unify_term
    1.48 +      val xthms = lookup net (Thm.term_of ct)
    1.49 +      fun select ct = map_filter (f (maybe_instantiate ct)) xthms
    1.50 +      fun select' ct =
    1.51 +        let val thm = Thm.trivial ct
    1.52 +        in map_filter (f (try (fn rule => rule COMP thm))) xthms end
    1.53 +    in (case select ct of [] => select' ct | xthms' => xthms') end
    1.54 +in
    1.55 +
    1.56 +fun net_instances net =
    1.57 +  instances_from_net false (fn f => fn (i, thm) => Option.map (pair i) (f thm))
    1.58 +    net
    1.59 +
    1.60 +end
    1.61 +
    1.62 +
    1.63 +(* proof combinators *)
    1.64 +
    1.65 +fun under_assumption f ct =
    1.66 +  let val ct' = SMT_Util.mk_cprop ct in Thm.implies_intr ct' (f (Thm.assume ct')) end
    1.67 +
    1.68 +fun discharge p pq = Thm.implies_elim pq p
    1.69 +
    1.70 +
    1.71 +(* a faster COMP *)
    1.72 +
    1.73 +type compose_data = cterm list * (cterm -> cterm list) * thm
    1.74 +
    1.75 +fun list2 (x, y) = [x, y]
    1.76 +
    1.77 +fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
    1.78 +fun precompose2 f rule = precompose (list2 o f) rule
    1.79 +
    1.80 +fun compose (cvs, f, rule) thm =
    1.81 +  discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
    1.82 +
    1.83 +
    1.84 +(* simpset *)
    1.85 +
    1.86 +local
    1.87 +  val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
    1.88 +  val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
    1.89 +  val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
    1.90 +  val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
    1.91 +
    1.92 +  fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
    1.93 +  fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
    1.94 +    | dest_binop t = raise TERM ("dest_binop", [t])
    1.95 +
    1.96 +  fun prove_antisym_le ctxt t =
    1.97 +    let
    1.98 +      val (le, r, s) = dest_binop t
    1.99 +      val less = Const (@{const_name less}, Term.fastype_of le)
   1.100 +      val prems = Simplifier.prems_of ctxt
   1.101 +    in
   1.102 +      (case find_first (eq_prop (le $ s $ r)) prems of
   1.103 +        NONE =>
   1.104 +          find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
   1.105 +          |> Option.map (fn thm => thm RS antisym_less1)
   1.106 +      | SOME thm => SOME (thm RS antisym_le1))
   1.107 +    end
   1.108 +    handle THM _ => NONE
   1.109 +
   1.110 +  fun prove_antisym_less ctxt t =
   1.111 +    let
   1.112 +      val (less, r, s) = dest_binop (HOLogic.dest_not t)
   1.113 +      val le = Const (@{const_name less_eq}, Term.fastype_of less)
   1.114 +      val prems = Simplifier.prems_of ctxt
   1.115 +    in
   1.116 +      (case find_first (eq_prop (le $ r $ s)) prems of
   1.117 +        NONE =>
   1.118 +          find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
   1.119 +          |> Option.map (fn thm => thm RS antisym_less2)
   1.120 +      | SOME thm => SOME (thm RS antisym_le2))
   1.121 +  end
   1.122 +  handle THM _ => NONE
   1.123 +
   1.124 +  val basic_simpset =
   1.125 +    simpset_of (put_simpset HOL_ss @{context}
   1.126 +      addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special
   1.127 +        arith_simps rel_simps array_rules z3div_def z3mod_def}
   1.128 +      addsimprocs [@{simproc binary_int_div}, @{simproc binary_int_mod},
   1.129 +        Simplifier.simproc_global @{theory} "fast_int_arith" [
   1.130 +          "(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc,
   1.131 +        Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"] prove_antisym_le,
   1.132 +        Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
   1.133 +          prove_antisym_less])
   1.134 +
   1.135 +  structure Simpset = Generic_Data
   1.136 +  (
   1.137 +    type T = simpset
   1.138 +    val empty = basic_simpset
   1.139 +    val extend = I
   1.140 +    val merge = Simplifier.merge_ss
   1.141 +  )
   1.142 +in
   1.143 +
   1.144 +fun add_simproc simproc context =
   1.145 +  Simpset.map (simpset_map (Context.proof_of context)
   1.146 +    (fn ctxt => ctxt addsimprocs [simproc])) context
   1.147 +
   1.148 +fun make_simpset ctxt rules =
   1.149 +  simpset_of (put_simpset (Simpset.get (Context.Proof ctxt)) ctxt addsimps rules)
   1.150 +
   1.151 +end
   1.152 +
   1.153 +end;