src/HOL/Tools/SMT/z3_proof_tools.ML
author boehmes
Mon Nov 29 23:41:09 2010 +0100 (2010-11-29)
changeset 40806 59d96f777da3
parent 40681 872b08416fb4
child 41123 3bb9be510a9d
permissions -rw-r--r--
also support higher-order rules for Z3 proof reconstruction
     1 (*  Title:      HOL/Tools/SMT/z3_proof_tools.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Helper functions required for Z3 proof reconstruction.
     5 *)
     6 
     7 signature Z3_PROOF_TOOLS =
     8 sig
     9   (* accessing and modifying terms *)
    10   val term_of: cterm -> term
    11   val prop_of: thm -> term
    12   val as_meta_eq: cterm -> cterm
    13 
    14   (* theorem nets *)
    15   val thm_net_of: ('a -> thm) -> 'a list -> 'a Net.net
    16   val net_instance': ((thm -> thm option) -> 'a -> 'a option) -> 'a Net.net ->
    17     cterm -> 'a option
    18   val net_instance: thm Net.net -> cterm -> thm option
    19 
    20   (* proof combinators *)
    21   val under_assumption: (thm -> thm) -> cterm -> thm
    22   val with_conv: conv -> (cterm -> thm) -> cterm -> thm
    23   val discharge: thm -> thm -> thm
    24   val varify: string list -> thm -> thm
    25   val unfold_eqs: Proof.context -> thm list -> conv
    26   val match_instantiate: (cterm -> cterm) -> cterm -> thm -> thm
    27   val by_tac: (int -> tactic) -> cterm -> thm
    28   val make_hyp_def: thm -> Proof.context -> thm * Proof.context
    29   val by_abstraction: bool * bool -> Proof.context -> thm list ->
    30     (Proof.context -> cterm -> thm) -> cterm -> thm
    31 
    32   (* a faster COMP *)
    33   type compose_data
    34   val precompose: (cterm -> cterm list) -> thm -> compose_data
    35   val precompose2: (cterm -> cterm * cterm) -> thm -> compose_data
    36   val compose: compose_data -> thm -> thm
    37 
    38   (* unfolding of 'distinct' *)
    39   val unfold_distinct_conv: conv
    40 
    41   (* simpset *)
    42   val add_simproc: Simplifier.simproc -> Context.generic -> Context.generic
    43   val make_simpset: Proof.context -> thm list -> simpset
    44 end
    45 
    46 structure Z3_Proof_Tools: Z3_PROOF_TOOLS =
    47 struct
    48 
    49 structure U = SMT_Utils
    50 structure I = Z3_Interface
    51 
    52 
    53 
    54 (* accessing terms *)
    55 
    56 val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
    57 
    58 fun term_of ct = dest_prop (Thm.term_of ct)
    59 fun prop_of thm = dest_prop (Thm.prop_of thm)
    60 
    61 fun as_meta_eq ct = uncurry U.mk_cequals (Thm.dest_binop (U.dest_cprop ct))
    62 
    63 
    64 
    65 (* theorem nets *)
    66 
    67 fun thm_net_of f xthms =
    68   let fun insert xthm = Net.insert_term (K false) (Thm.prop_of (f xthm), xthm)
    69   in fold insert xthms Net.empty end
    70 
    71 fun maybe_instantiate ct thm =
    72   try Thm.first_order_match (Thm.cprop_of thm, ct)
    73   |> Option.map (fn inst => Thm.instantiate inst thm)
    74 
    75 fun net_instance' f net ct =
    76   let
    77     val xthms = Net.match_term net (Thm.term_of ct)
    78     fun first_of f ct = get_first (f (maybe_instantiate ct)) xthms 
    79     fun first_of' f ct =
    80       let val thm = Thm.trivial ct
    81       in get_first (f (try (fn rule => rule COMP thm))) xthms end
    82   in (case first_of f ct of NONE => first_of' f ct | some_thm => some_thm) end
    83 val net_instance = net_instance' I
    84 
    85 
    86 
    87 (* proof combinators *)
    88 
    89 fun under_assumption f ct =
    90   let val ct' = U.mk_cprop ct
    91   in Thm.implies_intr ct' (f (Thm.assume ct')) end
    92 
    93 fun with_conv conv prove ct =
    94   let val eq = Thm.symmetric (conv ct)
    95   in Thm.equal_elim eq (prove (Thm.lhs_of eq)) end
    96 
    97 fun discharge p pq = Thm.implies_elim pq p
    98 
    99 fun varify vars = Drule.generalize ([], vars)
   100 
   101 fun unfold_eqs _ [] = Conv.all_conv
   102   | unfold_eqs ctxt eqs =
   103       Conv.top_sweep_conv (K (Conv.rewrs_conv eqs)) ctxt
   104 
   105 fun match_instantiate f ct thm =
   106   Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
   107 
   108 fun by_tac tac ct = Goal.norm_result (Goal.prove_internal [] ct (K (tac 1)))
   109 
   110 (* |- c x == t x ==> P (c x)  ~~>  c == t |- P (c x) *) 
   111 fun make_hyp_def thm ctxt =
   112   let
   113     val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
   114     val (cf, cvs) = Drule.strip_comb lhs
   115     val eq = U.mk_cequals cf (fold_rev Thm.cabs cvs rhs)
   116     fun apply cv th =
   117       Thm.combination th (Thm.reflexive cv)
   118       |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
   119   in
   120     yield_singleton Assumption.add_assumes eq ctxt
   121     |>> Thm.implies_elim thm o fold apply cvs
   122   end
   123 
   124 
   125 
   126 (* abstraction *)
   127 
   128 local
   129 
   130 fun abs_context ctxt = (ctxt, Termtab.empty, 1, false)
   131 
   132 fun context_of (ctxt, _, _, _) = ctxt
   133 
   134 fun replace (_, (cv, ct)) = Thm.forall_elim ct o Thm.forall_intr cv
   135 
   136 fun abs_instantiate (_, tab, _, beta_norm) =
   137   fold replace (Termtab.dest tab) #>
   138   beta_norm ? Conv.fconv_rule (Thm.beta_conversion true)
   139 
   140 fun lambda_abstract cvs t =
   141   let
   142     val frees = map Free (Term.add_frees t [])
   143     val cvs' = filter (fn cv => member (op aconv) frees (Thm.term_of cv)) cvs
   144     val vs = map (Term.dest_Free o Thm.term_of) cvs'
   145   in (Term.list_abs_free (vs, t), cvs') end
   146 
   147 fun fresh_abstraction cvs ct (cx as (ctxt, tab, idx, beta_norm)) =
   148   let val (t, cvs') = lambda_abstract cvs (Thm.term_of ct)
   149   in
   150     (case Termtab.lookup tab t of
   151       SOME (cv, _) => (Drule.list_comb (cv, cvs'), cx)
   152     | NONE =>
   153         let
   154           val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt
   155           val cv = U.certify ctxt'
   156             (Free (n, map U.typ_of cvs' ---> U.typ_of ct))
   157           val cu = Drule.list_comb (cv, cvs')
   158           val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
   159           val beta_norm' = beta_norm orelse not (null cvs')
   160         in (cu, (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end)
   161   end
   162 
   163 fun abs_comb f g cvs ct =
   164   let val (cf, cu) = Thm.dest_comb ct
   165   in f cvs cf ##>> g cvs cu #>> uncurry Thm.capply end
   166 
   167 fun abs_arg f = abs_comb (K pair) f
   168 
   169 fun abs_args f cvs ct =
   170   (case Thm.term_of ct of
   171     _ $ _ => abs_comb (abs_args f) f cvs ct
   172   | _ => pair ct)
   173 
   174 fun abs_list f g cvs ct =
   175   (case Thm.term_of ct of
   176     Const (@{const_name Nil}, _) => pair ct
   177   | Const (@{const_name Cons}, _) $ _ $ _ =>
   178       abs_comb (abs_arg f) (abs_list f g) cvs ct
   179   | _ => g cvs ct)
   180 
   181 fun abs_abs f cvs ct =
   182   let val (cv, cu) = Thm.dest_abs NONE ct
   183   in f (cv :: cvs) cu #>> Thm.cabs cv end
   184 
   185 val is_atomic = (fn _ $ _ => false | Abs _ => false | _ => true)
   186 
   187 fun abstract (ext_logic, with_theories) =
   188   let
   189     fun abstr1 cvs ct = abs_arg abstr cvs ct
   190     and abstr2 cvs ct = abs_comb abstr1 abstr cvs ct
   191     and abstr3 cvs ct = abs_comb abstr2 abstr cvs ct
   192     and abstr_abs cvs ct = abs_arg (abs_abs abstr) cvs ct
   193 
   194     and abstr cvs ct =
   195       (case Thm.term_of ct of
   196         @{const Trueprop} $ _ => abstr1 cvs ct
   197       | @{const "==>"} $ _ $ _ => abstr2 cvs ct
   198       | @{const True} => pair ct
   199       | @{const False} => pair ct
   200       | @{const Not} $ _ => abstr1 cvs ct
   201       | @{const HOL.conj} $ _ $ _ => abstr2 cvs ct
   202       | @{const HOL.disj} $ _ $ _ => abstr2 cvs ct
   203       | @{const HOL.implies} $ _ $ _ => abstr2 cvs ct
   204       | Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
   205       | Const (@{const_name distinct}, _) $ _ =>
   206           if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
   207           else fresh_abstraction cvs ct
   208       | Const (@{const_name If}, _) $ _ $ _ $ _ =>
   209           if ext_logic then abstr3 cvs ct else fresh_abstraction cvs ct
   210       | Const (@{const_name All}, _) $ _ =>
   211           if ext_logic then abstr_abs cvs ct else fresh_abstraction cvs ct
   212       | Const (@{const_name Ex}, _) $ _ =>
   213           if ext_logic then abstr_abs cvs ct else fresh_abstraction cvs ct
   214       | t => (fn cx =>
   215           if is_atomic t orelse can HOLogic.dest_number t then (ct, cx)
   216           else if with_theories andalso
   217             I.is_builtin_theory_term (context_of cx) t
   218           then abs_args abstr cvs ct cx
   219           else fresh_abstraction cvs ct cx))
   220   in abstr [] end
   221 
   222 val cimp = Thm.cterm_of @{theory} @{const "==>"}
   223 
   224 fun with_prems thms f ct =
   225   fold_rev (Thm.mk_binop cimp o Thm.cprop_of) thms ct
   226   |> f
   227   |> fold (fn prem => fn th => Thm.implies_elim th prem) thms
   228 
   229 in
   230 
   231 fun by_abstraction mode ctxt thms prove = with_prems thms (fn ct =>
   232   let val (cu, cx) = abstract mode ct (abs_context ctxt)
   233   in abs_instantiate cx (prove (context_of cx) cu) end)
   234 
   235 end
   236 
   237 
   238 
   239 (* a faster COMP *)
   240 
   241 type compose_data = cterm list * (cterm -> cterm list) * thm
   242 
   243 fun list2 (x, y) = [x, y]
   244 
   245 fun precompose f rule = (f (Thm.cprem_of rule 1), f, rule)
   246 fun precompose2 f rule = precompose (list2 o f) rule
   247 
   248 fun compose (cvs, f, rule) thm =
   249   discharge thm (Thm.instantiate ([], cvs ~~ f (Thm.cprop_of thm)) rule)
   250 
   251 
   252 
   253 (* unfolding of 'distinct' *)
   254 
   255 local
   256   val set1 = @{lemma "x ~: set [] == ~False" by simp}
   257   val set2 = @{lemma "x ~: set [x] == False" by simp}
   258   val set3 = @{lemma "x ~: set [y] == x ~= y" by simp}
   259   val set4 = @{lemma "x ~: set (x # ys) == False" by simp}
   260   val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
   261 
   262   fun set_conv ct =
   263     (Conv.rewrs_conv [set1, set2, set3, set4] else_conv
   264     (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
   265 
   266   val dist1 = @{lemma "distinct [] == ~False" by (simp add: distinct_def)}
   267   val dist2 = @{lemma "distinct [x] == ~False" by (simp add: distinct_def)}
   268   val dist3 = @{lemma "distinct (x # xs) == x ~: set xs & distinct xs"
   269     by (simp add: distinct_def)}
   270 
   271   fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
   272 in
   273 fun unfold_distinct_conv ct =
   274   (Conv.rewrs_conv [dist1, dist2] else_conv
   275   (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
   276 end
   277 
   278 
   279 
   280 (* simpset *)
   281 
   282 local
   283   val antisym_le1 = mk_meta_eq @{thm order_class.antisym_conv}
   284   val antisym_le2 = mk_meta_eq @{thm linorder_class.antisym_conv2}
   285   val antisym_less1 = mk_meta_eq @{thm linorder_class.antisym_conv1}
   286   val antisym_less2 = mk_meta_eq @{thm linorder_class.antisym_conv3}
   287 
   288   fun eq_prop t thm = HOLogic.mk_Trueprop t aconv Thm.prop_of thm
   289   fun dest_binop ((c as Const _) $ t $ u) = (c, t, u)
   290     | dest_binop t = raise TERM ("dest_binop", [t])
   291 
   292   fun prove_antisym_le ss t =
   293     let
   294       val (le, r, s) = dest_binop t
   295       val less = Const (@{const_name less}, Term.fastype_of le)
   296       val prems = Simplifier.prems_of_ss ss
   297     in
   298       (case find_first (eq_prop (le $ s $ r)) prems of
   299         NONE =>
   300           find_first (eq_prop (HOLogic.mk_not (less $ r $ s))) prems
   301           |> Option.map (fn thm => thm RS antisym_less1)
   302       | SOME thm => SOME (thm RS antisym_le1))
   303     end
   304     handle THM _ => NONE
   305 
   306   fun prove_antisym_less ss t =
   307     let
   308       val (less, r, s) = dest_binop (HOLogic.dest_not t)
   309       val le = Const (@{const_name less_eq}, Term.fastype_of less)
   310       val prems = prems_of_ss ss
   311     in
   312       (case find_first (eq_prop (le $ r $ s)) prems of
   313         NONE =>
   314           find_first (eq_prop (HOLogic.mk_not (less $ s $ r))) prems
   315           |> Option.map (fn thm => thm RS antisym_less2)
   316       | SOME thm => SOME (thm RS antisym_le2))
   317   end
   318   handle THM _ => NONE
   319 
   320   val basic_simpset = HOL_ss addsimps @{thms field_simps}
   321     addsimps [@{thm times_divide_eq_right}, @{thm times_divide_eq_left}]
   322     addsimps @{thms arith_special} addsimps @{thms less_bin_simps}
   323     addsimps @{thms le_bin_simps} addsimps @{thms eq_bin_simps}
   324     addsimps @{thms add_bin_simps} addsimps @{thms succ_bin_simps}
   325     addsimps @{thms minus_bin_simps} addsimps @{thms pred_bin_simps}
   326     addsimps @{thms mult_bin_simps} addsimps @{thms iszero_simps}
   327     addsimps @{thms array_rules}
   328     addsimps @{thms z3div_def} addsimps @{thms z3mod_def}
   329     addsimprocs [
   330       Simplifier.simproc_global @{theory} "fast_int_arith" [
   331         "(m::int) < n", "(m::int) <= n", "(m::int) = n"] (K Lin_Arith.simproc),
   332       Simplifier.simproc_global @{theory} "antisym_le" ["(x::'a::order) <= y"]
   333         (K prove_antisym_le),
   334       Simplifier.simproc_global @{theory} "antisym_less" ["~ (x::'a::linorder) < y"]
   335         (K prove_antisym_less)]
   336 
   337   structure Simpset = Generic_Data
   338   (
   339     type T = simpset
   340     val empty = basic_simpset
   341     val extend = I
   342     val merge = Simplifier.merge_ss
   343   )
   344 in
   345 
   346 fun add_simproc simproc = Simpset.map (fn ss => ss addsimprocs [simproc])
   347 
   348 fun make_simpset ctxt rules =
   349   Simplifier.context ctxt (Simpset.get (Context.Proof ctxt)) addsimps rules
   350 
   351 end
   352 
   353 end