src/HOL/Tools/SMT/z3_proof_reconstruction.ML
author wenzelm
Wed Feb 15 23:19:30 2012 +0100 (2012-02-15)
changeset 46497 89ccf66aa73d
parent 46464 4cf5a84e2c05
child 49980 34b0464d7eef
permissions -rw-r--r--
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
boehmes@36898
     1
(*  Title:      HOL/Tools/SMT/z3_proof_reconstruction.ML
boehmes@36898
     2
    Author:     Sascha Boehme, TU Muenchen
boehmes@36898
     3
boehmes@36898
     4
Proof reconstruction for proofs found by Z3.
boehmes@36898
     5
*)
boehmes@36898
     6
boehmes@36898
     7
signature Z3_PROOF_RECONSTRUCTION =
boehmes@36898
     8
sig
boehmes@36899
     9
  val add_z3_rule: thm -> Context.generic -> Context.generic
boehmes@40162
    10
  val reconstruct: Proof.context -> SMT_Translate.recon -> string list ->
boehmes@41127
    11
    int list * thm
boehmes@36898
    12
  val setup: theory -> theory
boehmes@36898
    13
end
boehmes@36898
    14
boehmes@36898
    15
structure Z3_Proof_Reconstruction: Z3_PROOF_RECONSTRUCTION =
boehmes@36898
    16
struct
boehmes@36898
    17
boehmes@36898
    18
boehmes@40424
    19
fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
boehmes@40162
    20
  ("Z3 proof reconstruction: " ^ msg))
boehmes@36898
    21
boehmes@36898
    22
boehmes@36898
    23
boehmes@41130
    24
(* net of schematic rules *)
boehmes@36898
    25
boehmes@36898
    26
val z3_ruleN = "z3_rule"
boehmes@36898
    27
boehmes@36898
    28
local
boehmes@36898
    29
  val description = "declaration of Z3 proof rules"
boehmes@36898
    30
boehmes@36898
    31
  val eq = Thm.eq_thm
boehmes@36898
    32
boehmes@36898
    33
  structure Z3_Rules = Generic_Data
boehmes@36898
    34
  (
boehmes@36898
    35
    type T = thm Net.net
boehmes@36898
    36
    val empty = Net.empty
boehmes@36898
    37
    val extend = I
boehmes@36898
    38
    val merge = Net.merge eq
boehmes@36898
    39
  )
boehmes@36898
    40
boehmes@41328
    41
  val prep =
boehmes@41328
    42
    `Thm.prop_of o Simplifier.rewrite_rule [Z3_Proof_Literals.rewrite_true]
boehmes@36898
    43
boehmes@36898
    44
  fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
boehmes@36898
    45
  fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
boehmes@36898
    46
boehmes@36898
    47
  val add = Thm.declaration_attribute (Z3_Rules.map o ins)
boehmes@36898
    48
  val del = Thm.declaration_attribute (Z3_Rules.map o del)
boehmes@36898
    49
in
boehmes@36898
    50
boehmes@36899
    51
val add_z3_rule = Z3_Rules.map o ins
boehmes@36898
    52
boehmes@36898
    53
fun by_schematic_rule ctxt ct =
boehmes@41328
    54
  the (Z3_Proof_Tools.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)
boehmes@36898
    55
boehmes@36898
    56
val z3_rules_setup =
boehmes@36898
    57
  Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #>
wenzelm@39557
    58
  Global_Theory.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get)
boehmes@36898
    59
boehmes@36898
    60
end
boehmes@36898
    61
boehmes@36898
    62
boehmes@36898
    63
boehmes@41130
    64
(* proof tools *)
boehmes@36898
    65
boehmes@36898
    66
fun named ctxt name prover ct =
boehmes@40424
    67
  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
boehmes@36898
    68
  in prover ct end
boehmes@36898
    69
boehmes@36898
    70
fun NAMED ctxt name tac i st =
boehmes@40424
    71
  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
boehmes@36898
    72
  in tac i st end
boehmes@36898
    73
boehmes@36898
    74
fun pretty_goal ctxt thms t =
boehmes@36898
    75
  [Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]]
boehmes@36898
    76
  |> not (null thms) ? cons (Pretty.big_list "assumptions:"
boehmes@36898
    77
       (map (Display.pretty_thm ctxt) thms))
boehmes@36898
    78
boehmes@36898
    79
fun try_apply ctxt thms =
boehmes@36898
    80
  let
boehmes@36898
    81
    fun try_apply_err ct = Pretty.string_of (Pretty.chunks [
boehmes@36898
    82
      Pretty.big_list ("Z3 found a proof," ^
boehmes@36898
    83
        " but proof reconstruction failed at the following subgoal:")
boehmes@36898
    84
        (pretty_goal ctxt thms (Thm.term_of ct)),
boehmes@36898
    85
      Pretty.str ("Adding a rule to the lemma group " ^ quote z3_ruleN ^
boehmes@36898
    86
        " might solve this problem.")])
boehmes@36898
    87
boehmes@36898
    88
    fun apply [] ct = error (try_apply_err ct)
boehmes@36898
    89
      | apply (prover :: provers) ct =
boehmes@36898
    90
          (case try prover ct of
boehmes@40424
    91
            SOME thm => (SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm)
boehmes@36898
    92
          | NONE => apply provers ct)
boehmes@36898
    93
boehmes@43893
    94
    fun schematic_label full = "schematic rules" |> full ? suffix " (full)"
boehmes@43893
    95
    fun schematic ctxt full ct =
boehmes@43893
    96
      ct
boehmes@43893
    97
      |> full ? fold_rev (curry Drule.mk_implies o Thm.cprop_of) thms
boehmes@43893
    98
      |> named ctxt (schematic_label full) (by_schematic_rule ctxt)
boehmes@43893
    99
      |> fold Thm.elim_implies thms
boehmes@43893
   100
boehmes@43893
   101
  in apply o cons (schematic ctxt false) o cons (schematic ctxt true) end
boehmes@36898
   102
boehmes@36899
   103
local
boehmes@36899
   104
  val rewr_if =
boehmes@36899
   105
    @{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp}
boehmes@36899
   106
in
wenzelm@42793
   107
wenzelm@42793
   108
fun HOL_fast_tac ctxt =
wenzelm@42793
   109
  Classical.fast_tac (put_claset HOL_cs ctxt)
wenzelm@42793
   110
wenzelm@42793
   111
fun simp_fast_tac ctxt =
boehmes@36899
   112
  Simplifier.simp_tac (HOL_ss addsimps [rewr_if])
wenzelm@42793
   113
  THEN_ALL_NEW HOL_fast_tac ctxt
wenzelm@42793
   114
boehmes@36899
   115
end
boehmes@36899
   116
boehmes@36898
   117
boehmes@36898
   118
boehmes@41130
   119
(* theorems and proofs *)
boehmes@36898
   120
boehmes@41130
   121
(** theorem incarnations **)
boehmes@36898
   122
boehmes@36898
   123
datatype theorem =
boehmes@36898
   124
  Thm of thm | (* theorem without special features *)
boehmes@36898
   125
  MetaEq of thm | (* meta equality "t == s" *)
boehmes@41328
   126
  Literals of thm * Z3_Proof_Literals.littab
boehmes@36898
   127
    (* "P1 & ... & Pn" and table of all literals P1, ..., Pn *)
boehmes@36898
   128
boehmes@36898
   129
fun thm_of (Thm thm) = thm
boehmes@36898
   130
  | thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq}
boehmes@36898
   131
  | thm_of (Literals (thm, _)) = thm
boehmes@36898
   132
boehmes@36898
   133
fun meta_eq_of (MetaEq thm) = thm
boehmes@36898
   134
  | meta_eq_of p = mk_meta_eq (thm_of p)
boehmes@36898
   135
boehmes@36898
   136
fun literals_of (Literals (_, lits)) = lits
boehmes@41328
   137
  | literals_of p = Z3_Proof_Literals.make_littab [thm_of p]
boehmes@36898
   138
boehmes@36898
   139
boehmes@36898
   140
boehmes@36898
   141
(** core proof rules **)
boehmes@36898
   142
boehmes@36898
   143
(* assumption *)
boehmes@41131
   144
boehmes@36898
   145
local
boehmes@41131
   146
  val remove_trigger = mk_meta_eq @{thm SMT.trigger_def}
boehmes@41131
   147
  val remove_weight = mk_meta_eq @{thm SMT.weight_def}
boehmes@41131
   148
  val remove_fun_app = mk_meta_eq @{thm SMT.fun_app_def}
boehmes@36898
   149
boehmes@44488
   150
  fun rewrite_conv _ [] = Conv.all_conv
boehmes@44488
   151
    | rewrite_conv ctxt eqs = Simplifier.full_rewrite
boehmes@44488
   152
        (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
boehmes@36898
   153
boehmes@41131
   154
  val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
boehmes@41328
   155
    remove_fun_app, Z3_Proof_Literals.rewrite_true]
boehmes@41131
   156
boehmes@44488
   157
  fun rewrite _ [] = I
boehmes@44488
   158
    | rewrite ctxt eqs = Conv.fconv_rule (rewrite_conv ctxt eqs)
boehmes@36898
   159
boehmes@40164
   160
  fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm)
boehmes@41131
   161
boehmes@41131
   162
  fun lookup_assm assms_net ct =
boehmes@45393
   163
    Z3_Proof_Tools.net_instances assms_net ct
boehmes@45393
   164
    |> map (fn ithm as (_, thm) => (ithm, Thm.cprop_of thm aconvc ct))
boehmes@36898
   165
in
boehmes@41131
   166
boehmes@41131
   167
fun add_asserted outer_ctxt rewrite_rules assms asserted ctxt =
boehmes@36898
   168
  let
boehmes@41328
   169
    val eqs = map (rewrite ctxt [Z3_Proof_Literals.rewrite_true]) rewrite_rules
boehmes@41131
   170
    val eqs' = union Thm.eq_thm eqs prep_rules
boehmes@41131
   171
boehmes@41131
   172
    val assms_net =
boehmes@41127
   173
      assms
boehmes@41131
   174
      |> map (apsnd (rewrite ctxt eqs'))
boehmes@41127
   175
      |> map (apsnd (Conv.fconv_rule Thm.eta_conversion))
boehmes@41328
   176
      |> Z3_Proof_Tools.thm_net_of snd 
boehmes@41131
   177
boehmes@41131
   178
    fun revert_conv ctxt = rewrite_conv ctxt eqs' then_conv Thm.eta_conversion
boehmes@41131
   179
boehmes@41131
   180
    fun assume thm ctxt =
boehmes@41131
   181
      let
boehmes@41131
   182
        val ct = Thm.cprem_of thm 1
boehmes@41131
   183
        val (thm', ctxt') = yield_singleton Assumption.add_assumes ct ctxt
boehmes@41131
   184
      in (Thm.implies_elim thm thm', ctxt') end
boehmes@36898
   185
boehmes@45393
   186
    fun add1 idx thm1 ((i, th), exact) ((is, thms), (ctxt, ptab)) =
boehmes@45393
   187
      let
boehmes@45393
   188
        val (thm, ctxt') =
boehmes@45393
   189
          if exact then (Thm.implies_elim thm1 th, ctxt)
boehmes@45393
   190
          else assume thm1 ctxt
boehmes@45393
   191
        val thms' = if exact then thms else th :: thms
boehmes@45393
   192
      in 
boehmes@45393
   193
        ((insert (op =) i is, thms'),
boehmes@45393
   194
          (ctxt', Inttab.update (idx, Thm thm) ptab))
boehmes@45393
   195
      end
boehmes@45393
   196
boehmes@45393
   197
    fun add (idx, ct) (cx as ((is, thms), (ctxt, ptab))) =
boehmes@41131
   198
      let
boehmes@41131
   199
        val thm1 = 
boehmes@41131
   200
          Thm.trivial ct
boehmes@41131
   201
          |> Conv.fconv_rule (Conv.arg1_conv (revert_conv outer_ctxt))
boehmes@41131
   202
        val thm2 = singleton (Variable.export ctxt outer_ctxt) thm1
boehmes@41131
   203
      in
boehmes@41131
   204
        (case lookup_assm assms_net (Thm.cprem_of thm2 1) of
boehmes@45393
   205
          [] =>
boehmes@41131
   206
            let val (thm, ctxt') = assume thm1 ctxt
boehmes@41131
   207
            in ((is, thms), (ctxt', Inttab.update (idx, Thm thm) ptab)) end
boehmes@45393
   208
        | ithms => fold (add1 idx thm1) ithms cx)
boehmes@41131
   209
      end
boehmes@41131
   210
  in fold add asserted (([], []), (ctxt, Inttab.empty)) end
boehmes@40164
   211
boehmes@36898
   212
end
boehmes@36898
   213
boehmes@36898
   214
boehmes@36898
   215
(* P = Q ==> P ==> Q   or   P --> Q ==> P ==> Q *)
boehmes@36898
   216
local
boehmes@41328
   217
  val precomp = Z3_Proof_Tools.precompose2
boehmes@41328
   218
  val comp = Z3_Proof_Tools.compose
boehmes@36898
   219
boehmes@41328
   220
  val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
boehmes@41328
   221
  val meta_iffD1_c = precomp Thm.dest_binop meta_iffD1
boehmes@41328
   222
boehmes@41328
   223
  val iffD1_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
boehmes@41328
   224
  val mp_c = precomp (Thm.dest_binop o Thm.dest_arg) @{thm mp}
boehmes@36898
   225
in
boehmes@41328
   226
fun mp (MetaEq thm) p = Thm (Thm.implies_elim (comp meta_iffD1_c thm) p)
boehmes@36898
   227
  | mp p_q p = 
boehmes@36898
   228
      let
boehmes@36898
   229
        val pq = thm_of p_q
boehmes@41328
   230
        val thm = comp iffD1_c pq handle THM _ => comp mp_c pq
boehmes@36898
   231
      in Thm (Thm.implies_elim thm p) end
boehmes@36898
   232
end
boehmes@36898
   233
boehmes@36898
   234
boehmes@36898
   235
(* and_elim:     P1 & ... & Pn ==> Pi *)
boehmes@36898
   236
(* not_or_elim:  ~(P1 | ... | Pn) ==> ~Pi *)
boehmes@36898
   237
local
boehmes@41328
   238
  fun is_sublit conj t = Z3_Proof_Literals.exists_lit conj (fn u => u aconv t)
boehmes@36898
   239
boehmes@36898
   240
  fun derive conj t lits idx ptab =
boehmes@36898
   241
    let
boehmes@41328
   242
      val lit = the (Z3_Proof_Literals.get_first_lit (is_sublit conj t) lits)
boehmes@41328
   243
      val ls = Z3_Proof_Literals.explode conj false false [t] lit
boehmes@41328
   244
      val lits' = fold Z3_Proof_Literals.insert_lit ls
boehmes@41328
   245
        (Z3_Proof_Literals.delete_lit lit lits)
boehmes@36898
   246
boehmes@41130
   247
      fun upd thm = Literals (thm_of thm, lits')
boehmes@41328
   248
      val ptab' = Inttab.map_entry idx upd ptab
boehmes@41328
   249
    in (the (Z3_Proof_Literals.lookup_lit lits' t), ptab') end
boehmes@36898
   250
boehmes@36898
   251
  fun lit_elim conj (p, idx) ct ptab =
boehmes@36898
   252
    let val lits = literals_of p
boehmes@36898
   253
    in
boehmes@41328
   254
      (case Z3_Proof_Literals.lookup_lit lits (SMT_Utils.term_of ct) of
boehmes@36898
   255
        SOME lit => (Thm lit, ptab)
boehmes@41328
   256
      | NONE => apfst Thm (derive conj (SMT_Utils.term_of ct) lits idx ptab))
boehmes@36898
   257
    end
boehmes@36898
   258
in
boehmes@36898
   259
val and_elim = lit_elim true
boehmes@36898
   260
val not_or_elim = lit_elim false
boehmes@36898
   261
end
boehmes@36898
   262
boehmes@36898
   263
boehmes@36898
   264
(* P1, ..., Pn |- False ==> |- ~P1 | ... | ~Pn *)
boehmes@36898
   265
local
boehmes@36898
   266
  fun step lit thm =
boehmes@36898
   267
    Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit
boehmes@41328
   268
  val explode_disj = Z3_Proof_Literals.explode false false false
boehmes@36898
   269
  fun intro hyps thm th = fold step (explode_disj hyps th) thm
boehmes@36898
   270
boehmes@36898
   271
  fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))]
boehmes@41328
   272
  val ccontr = Z3_Proof_Tools.precompose dest_ccontr @{thm ccontr}
boehmes@36898
   273
in
boehmes@36898
   274
fun lemma thm ct =
boehmes@36898
   275
  let
boehmes@41328
   276
    val cu = Z3_Proof_Literals.negate (Thm.dest_arg ct)
wenzelm@44058
   277
    val hyps = map_filter (try HOLogic.dest_Trueprop) (Thm.hyps_of thm)
boehmes@41328
   278
    val th = Z3_Proof_Tools.under_assumption (intro hyps thm) cu
boehmes@41328
   279
  in Thm (Z3_Proof_Tools.compose ccontr th) end
boehmes@36898
   280
end
boehmes@36898
   281
boehmes@36898
   282
boehmes@36898
   283
(* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *)
boehmes@36898
   284
local
boehmes@41328
   285
  val explode_disj = Z3_Proof_Literals.explode false true false
boehmes@41328
   286
  val join_disj = Z3_Proof_Literals.join false
boehmes@36898
   287
  fun unit thm thms th =
boehmes@41328
   288
    let
boehmes@41328
   289
      val t = @{const Not} $ SMT_Utils.prop_of thm
boehmes@41328
   290
      val ts = map SMT_Utils.prop_of thms
boehmes@41328
   291
    in
boehmes@41328
   292
      join_disj (Z3_Proof_Literals.make_littab (thms @ explode_disj ts th)) t
boehmes@41328
   293
    end
boehmes@36898
   294
boehmes@36898
   295
  fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
boehmes@36898
   296
  fun dest ct = pairself dest_arg2 (Thm.dest_binop ct)
boehmes@41328
   297
  val contrapos =
boehmes@41328
   298
    Z3_Proof_Tools.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
boehmes@36898
   299
in
boehmes@36898
   300
fun unit_resolution thm thms ct =
boehmes@41328
   301
  Z3_Proof_Literals.negate (Thm.dest_arg ct)
boehmes@41328
   302
  |> Z3_Proof_Tools.under_assumption (unit thm thms)
boehmes@41328
   303
  |> Thm o Z3_Proof_Tools.discharge thm o Z3_Proof_Tools.compose contrapos
boehmes@36898
   304
end
boehmes@36898
   305
boehmes@36898
   306
boehmes@36898
   307
(* P ==> P == True   or   P ==> P == False *)
boehmes@36898
   308
local
boehmes@36898
   309
  val iff1 = @{lemma "P ==> P == (~ False)" by simp}
boehmes@36898
   310
  val iff2 = @{lemma "~P ==> P == False" by simp}
boehmes@36898
   311
in
boehmes@36898
   312
fun iff_true thm = MetaEq (thm COMP iff1)
boehmes@36898
   313
fun iff_false thm = MetaEq (thm COMP iff2)
boehmes@36898
   314
end
boehmes@36898
   315
boehmes@36898
   316
boehmes@36898
   317
(* distributivity of | over & *)
boehmes@36898
   318
fun distributivity ctxt = Thm o try_apply ctxt [] [
wenzelm@42793
   319
  named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
boehmes@36898
   320
    (* FIXME: not very well tested *)
boehmes@36898
   321
boehmes@36898
   322
boehmes@36898
   323
(* Tseitin-like axioms *)
boehmes@36898
   324
local
boehmes@36898
   325
  val disjI1 = @{lemma "(P ==> Q) ==> ~P | Q" by fast}
boehmes@36898
   326
  val disjI2 = @{lemma "(~P ==> Q) ==> P | Q" by fast}
boehmes@36898
   327
  val disjI3 = @{lemma "(~Q ==> P) ==> P | Q" by fast}
boehmes@36898
   328
  val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast}
boehmes@36898
   329
boehmes@36898
   330
  fun prove' conj1 conj2 ct2 thm =
boehmes@41328
   331
    let
boehmes@41328
   332
      val littab =
boehmes@41328
   333
        Z3_Proof_Literals.explode conj1 true (conj1 <> conj2) [] thm
boehmes@41328
   334
        |> cons Z3_Proof_Literals.true_thm
boehmes@41328
   335
        |> Z3_Proof_Literals.make_littab
boehmes@41328
   336
    in Z3_Proof_Literals.join conj2 littab (Thm.term_of ct2) end
boehmes@36898
   337
boehmes@36898
   338
  fun prove rule (ct1, conj1) (ct2, conj2) =
boehmes@41328
   339
    Z3_Proof_Tools.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule
boehmes@36898
   340
boehmes@36898
   341
  fun prove_def_axiom ct =
boehmes@36898
   342
    let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
boehmes@36898
   343
    in
boehmes@36898
   344
      (case Thm.term_of ct1 of
boehmes@40579
   345
        @{const Not} $ (@{const HOL.conj} $ _ $ _) =>
boehmes@36898
   346
          prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
boehmes@40579
   347
      | @{const HOL.conj} $ _ $ _ =>
boehmes@41328
   348
          prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, true)
boehmes@40579
   349
      | @{const Not} $ (@{const HOL.disj} $ _ $ _) =>
boehmes@41328
   350
          prove disjI3 (Z3_Proof_Literals.negate ct2, false) (ct1, false)
boehmes@40579
   351
      | @{const HOL.disj} $ _ $ _ =>
boehmes@41328
   352
          prove disjI2 (Z3_Proof_Literals.negate ct1, false) (ct2, true)
boehmes@40681
   353
      | Const (@{const_name distinct}, _) $ _ =>
boehmes@36898
   354
          let
boehmes@36898
   355
            fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
boehmes@41328
   356
            val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv
boehmes@36898
   357
            fun prv cu =
boehmes@36898
   358
              let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
boehmes@36898
   359
              in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
boehmes@41328
   360
          in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
boehmes@40681
   361
      | @{const Not} $ (Const (@{const_name distinct}, _) $ _) =>
boehmes@36898
   362
          let
boehmes@36898
   363
            fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
boehmes@41328
   364
            val unfold_dis_conv = dis_conv Z3_Proof_Tools.unfold_distinct_conv
boehmes@36898
   365
            fun prv cu =
boehmes@36898
   366
              let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
boehmes@36898
   367
              in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end
boehmes@41328
   368
          in Z3_Proof_Tools.with_conv unfold_dis_conv prv ct end
boehmes@36898
   369
      | _ => raise CTERM ("prove_def_axiom", [ct]))
boehmes@36898
   370
    end
boehmes@36898
   371
in
boehmes@36898
   372
fun def_axiom ctxt = Thm o try_apply ctxt [] [
boehmes@36898
   373
  named ctxt "conj/disj/distinct" prove_def_axiom,
boehmes@42992
   374
  Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
wenzelm@42793
   375
    named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
boehmes@36898
   376
end
boehmes@36898
   377
boehmes@36898
   378
boehmes@36898
   379
(* local definitions *)
boehmes@36898
   380
local
boehmes@36898
   381
  val intro_rules = [
boehmes@36898
   382
    @{lemma "n == P ==> (~n | P) & (n | ~P)" by simp},
boehmes@36898
   383
    @{lemma "n == (if P then s else t) ==> (~P | n = s) & (P | n = t)"
boehmes@36898
   384
      by simp},
boehmes@36898
   385
    @{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ]
boehmes@36898
   386
boehmes@36898
   387
  val apply_rules = [
boehmes@36898
   388
    @{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast},
boehmes@36898
   389
    @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n"
nipkow@44890
   390
      by (atomize(full)) fastforce} ]
boehmes@36898
   391
boehmes@41328
   392
  val inst_rule = Z3_Proof_Tools.match_instantiate Thm.dest_arg
boehmes@36898
   393
boehmes@36898
   394
  fun apply_rule ct =
boehmes@36898
   395
    (case get_first (try (inst_rule ct)) intro_rules of
boehmes@36898
   396
      SOME thm => thm
boehmes@36898
   397
    | NONE => raise CTERM ("intro_def", [ct]))
boehmes@36898
   398
in
boehmes@41328
   399
fun intro_def ct = Z3_Proof_Tools.make_hyp_def (apply_rule ct) #>> Thm
boehmes@36898
   400
boehmes@36898
   401
fun apply_def thm =
boehmes@36898
   402
  get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules
boehmes@36898
   403
  |> the_default (Thm thm)
boehmes@36898
   404
end
boehmes@36898
   405
boehmes@36898
   406
boehmes@36898
   407
(* negation normal form *)
boehmes@36898
   408
local
boehmes@36898
   409
  val quant_rules1 = ([
boehmes@36898
   410
    @{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp},
boehmes@36898
   411
    @{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [
boehmes@36898
   412
    @{lemma "(!!x. P x == Q x) ==> ALL x. P x == ALL x. Q x" by simp},
boehmes@36898
   413
    @{lemma "(!!x. P x == Q x) ==> EX x. P x == EX x. Q x" by simp}])
boehmes@36898
   414
boehmes@36898
   415
  val quant_rules2 = ([
boehmes@36898
   416
    @{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp},
boehmes@36898
   417
    @{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [
boehmes@36898
   418
    @{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp},
boehmes@36898
   419
    @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
boehmes@36898
   420
boehmes@36898
   421
  fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = (
boehmes@36898
   422
    Tactic.rtac thm ORELSE'
boehmes@36898
   423
    (Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
boehmes@36898
   424
    (Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
boehmes@36898
   425
boehmes@41328
   426
  fun nnf_quant_tac_varified vars eq =
boehmes@41328
   427
    nnf_quant_tac (Z3_Proof_Tools.varify vars eq)
boehmes@41328
   428
boehmes@36898
   429
  fun nnf_quant vars qs p ct =
boehmes@41328
   430
    Z3_Proof_Tools.as_meta_eq ct
boehmes@41328
   431
    |> Z3_Proof_Tools.by_tac (nnf_quant_tac_varified vars (meta_eq_of p) qs)
boehmes@36898
   432
boehmes@36898
   433
  fun prove_nnf ctxt = try_apply ctxt [] [
boehmes@41328
   434
    named ctxt "conj/disj" Z3_Proof_Literals.prove_conj_disj_eq,
boehmes@42992
   435
    Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
wenzelm@42793
   436
      named ctxt' "simp+fast" (Z3_Proof_Tools.by_tac (simp_fast_tac ctxt')))]
boehmes@36898
   437
in
boehmes@36898
   438
fun nnf ctxt vars ps ct =
boehmes@41328
   439
  (case SMT_Utils.term_of ct of
boehmes@36898
   440
    _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
boehmes@36898
   441
      if l aconv r
boehmes@36898
   442
      then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
boehmes@36898
   443
      else MetaEq (nnf_quant vars quant_rules1 (hd ps) ct)
boehmes@40579
   444
  | _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
boehmes@36898
   445
      MetaEq (nnf_quant vars quant_rules2 (hd ps) ct)
boehmes@36898
   446
  | _ =>
boehmes@36898
   447
      let
boehmes@36898
   448
        val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv
boehmes@41328
   449
          (Z3_Proof_Tools.unfold_eqs ctxt
boehmes@41328
   450
            (map (Thm.symmetric o meta_eq_of) ps)))
boehmes@41328
   451
      in Thm (Z3_Proof_Tools.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end)
boehmes@36898
   452
end
boehmes@36898
   453
boehmes@36898
   454
boehmes@36898
   455
boehmes@36898
   456
(** equality proof rules **)
boehmes@36898
   457
boehmes@36898
   458
(* |- t = t *)
boehmes@36898
   459
fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
boehmes@36898
   460
boehmes@36898
   461
boehmes@36898
   462
(* s = t ==> t = s *)
boehmes@36898
   463
local
boehmes@36898
   464
  val symm_rule = @{lemma "s = t ==> t == s" by simp}
boehmes@36898
   465
in
boehmes@36898
   466
fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm)
boehmes@36898
   467
  | symm p = MetaEq (thm_of p COMP symm_rule)
boehmes@36898
   468
end
boehmes@36898
   469
boehmes@36898
   470
boehmes@36898
   471
(* s = t ==> t = u ==> s = u *)
boehmes@36898
   472
local
boehmes@36898
   473
  val trans1 = @{lemma "s == t ==> t =  u ==> s == u" by simp}
boehmes@36898
   474
  val trans2 = @{lemma "s =  t ==> t == u ==> s == u" by simp}
boehmes@36898
   475
  val trans3 = @{lemma "s =  t ==> t =  u ==> s == u" by simp}
boehmes@36898
   476
in
boehmes@36898
   477
fun trans (MetaEq thm1) (MetaEq thm2) = MetaEq (Thm.transitive thm1 thm2)
boehmes@36898
   478
  | trans (MetaEq thm) q = MetaEq (thm_of q COMP (thm COMP trans1))
boehmes@36898
   479
  | trans p (MetaEq thm) = MetaEq (thm COMP (thm_of p COMP trans2))
boehmes@36898
   480
  | trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans3))
boehmes@36898
   481
end
boehmes@36898
   482
boehmes@36898
   483
boehmes@36898
   484
(* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn
boehmes@36898
   485
   (reflexive antecendents are droppped) *)
boehmes@36898
   486
local
boehmes@36898
   487
  exception MONO
boehmes@36898
   488
boehmes@36898
   489
  fun prove_refl (ct, _) = Thm.reflexive ct
boehmes@36898
   490
  fun prove_comb f g cp =
boehmes@36898
   491
    let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp
boehmes@36898
   492
    in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end
boehmes@36898
   493
  fun prove_arg f = prove_comb prove_refl f
boehmes@36898
   494
boehmes@36898
   495
  fun prove f cp = prove_comb (prove f) f cp handle CTERM _ => prove_refl cp
boehmes@36898
   496
boehmes@36898
   497
  fun prove_nary is_comb f =
boehmes@36898
   498
    let
boehmes@36898
   499
      fun prove (cp as (ct, _)) = f cp handle MONO =>
boehmes@36898
   500
        if is_comb (Thm.term_of ct)
boehmes@36898
   501
        then prove_comb (prove_arg prove) prove cp
boehmes@36898
   502
        else prove_refl cp
boehmes@36898
   503
    in prove end
boehmes@36898
   504
boehmes@36898
   505
  fun prove_list f n cp =
boehmes@36898
   506
    if n = 0 then prove_refl cp
boehmes@36898
   507
    else prove_comb (prove_arg f) (prove_list f (n-1)) cp
boehmes@36898
   508
boehmes@36898
   509
  fun with_length f (cp as (cl, _)) =
boehmes@36898
   510
    f (length (HOLogic.dest_list (Thm.term_of cl))) cp
boehmes@36898
   511
boehmes@36898
   512
  fun prove_distinct f = prove_arg (with_length (prove_list f))
boehmes@36898
   513
boehmes@36898
   514
  fun prove_eq exn lookup cp =
boehmes@36898
   515
    (case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of
boehmes@36898
   516
      SOME eq => eq
boehmes@36898
   517
    | NONE => if exn then raise MONO else prove_refl cp)
boehmes@36898
   518
  
boehmes@41328
   519
  val prove_exn = prove_eq true
boehmes@41328
   520
  and prove_safe = prove_eq false
boehmes@36898
   521
boehmes@36898
   522
  fun mono f (cp as (cl, _)) =
boehmes@36898
   523
    (case Term.head_of (Thm.term_of cl) of
boehmes@41328
   524
      @{const HOL.conj} => prove_nary Z3_Proof_Literals.is_conj (prove_exn f)
boehmes@41328
   525
    | @{const HOL.disj} => prove_nary Z3_Proof_Literals.is_disj (prove_exn f)
boehmes@41328
   526
    | Const (@{const_name distinct}, _) => prove_distinct (prove_safe f)
boehmes@41328
   527
    | _ => prove (prove_safe f)) cp
boehmes@36898
   528
in
boehmes@36898
   529
fun monotonicity eqs ct =
boehmes@36898
   530
  let
boehmes@40680
   531
    fun and_symmetric (t, thm) = [(t, thm), (t, Thm.symmetric thm)]
boehmes@40680
   532
    val teqs = maps (and_symmetric o `Thm.prop_of o meta_eq_of) eqs
boehmes@40680
   533
    val lookup = AList.lookup (op aconv) teqs
boehmes@36898
   534
    val cp = Thm.dest_binop (Thm.dest_arg ct)
boehmes@41328
   535
  in MetaEq (prove_exn lookup cp handle MONO => mono lookup cp) end
boehmes@36898
   536
end
boehmes@36898
   537
boehmes@36898
   538
boehmes@36898
   539
(* |- f a b = f b a (where f is equality) *)
boehmes@36898
   540
local
boehmes@36898
   541
  val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)}
boehmes@36898
   542
in
boehmes@41328
   543
fun commutativity ct =
boehmes@41328
   544
  MetaEq (Z3_Proof_Tools.match_instantiate I
boehmes@41328
   545
    (Z3_Proof_Tools.as_meta_eq ct) rule)
boehmes@36898
   546
end
boehmes@36898
   547
boehmes@36898
   548
boehmes@36898
   549
boehmes@36898
   550
(** quantifier proof rules **)
boehmes@36898
   551
boehmes@36898
   552
(* P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x)
boehmes@36898
   553
   P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x)    *)
boehmes@36898
   554
local
boehmes@36898
   555
  val rules = [
boehmes@36898
   556
    @{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp},
boehmes@36898
   557
    @{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}]
boehmes@36898
   558
in
boehmes@36898
   559
fun quant_intro vars p ct =
boehmes@36898
   560
  let
boehmes@36898
   561
    val thm = meta_eq_of p
boehmes@41328
   562
    val rules' = Z3_Proof_Tools.varify vars thm :: rules
boehmes@41328
   563
    val cu = Z3_Proof_Tools.as_meta_eq ct
boehmes@41328
   564
    val tac = REPEAT_ALL_NEW (Tactic.match_tac rules')
boehmes@41328
   565
  in MetaEq (Z3_Proof_Tools.by_tac tac cu) end
boehmes@36898
   566
end
boehmes@36898
   567
boehmes@36898
   568
boehmes@36898
   569
(* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
boehmes@36898
   570
fun pull_quant ctxt = Thm o try_apply ctxt [] [
wenzelm@42793
   571
  named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
boehmes@36898
   572
    (* FIXME: not very well tested *)
boehmes@36898
   573
boehmes@36898
   574
boehmes@36898
   575
(* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
boehmes@36898
   576
fun push_quant ctxt = Thm o try_apply ctxt [] [
wenzelm@42793
   577
  named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
boehmes@36898
   578
    (* FIXME: not very well tested *)
boehmes@36898
   579
boehmes@36898
   580
boehmes@36898
   581
(* |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *)
boehmes@36898
   582
local
boehmes@42318
   583
  val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
boehmes@42318
   584
  val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
boehmes@36898
   585
boehmes@42318
   586
  fun elim_unused_tac i st = (
boehmes@42318
   587
    Tactic.match_tac [@{thm refl}]
boehmes@42318
   588
    ORELSE' (Tactic.match_tac [elim_all, elim_ex] THEN' elim_unused_tac)
boehmes@42318
   589
    ORELSE' (
boehmes@42318
   590
      Tactic.match_tac [@{thm iff_allI}, @{thm iff_exI}]
boehmes@42318
   591
      THEN' elim_unused_tac)) i st
boehmes@36898
   592
in
boehmes@42318
   593
boehmes@42318
   594
val elim_unused_vars = Thm o Z3_Proof_Tools.by_tac elim_unused_tac
boehmes@42318
   595
boehmes@36898
   596
end
boehmes@36898
   597
boehmes@36898
   598
boehmes@36898
   599
(* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
boehmes@36898
   600
fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
wenzelm@42793
   601
  named ctxt "fast" (Z3_Proof_Tools.by_tac (HOL_fast_tac ctxt))]
boehmes@36898
   602
    (* FIXME: not very well tested *)
boehmes@36898
   603
boehmes@36898
   604
boehmes@36898
   605
(* |- ~(ALL x1...xn. P x1...xn) | P a1...an *)
boehmes@36898
   606
local
boehmes@36898
   607
  val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
boehmes@36898
   608
in
boehmes@41328
   609
val quant_inst = Thm o Z3_Proof_Tools.by_tac (
boehmes@36898
   610
  REPEAT_ALL_NEW (Tactic.match_tac [rule])
boehmes@36898
   611
  THEN' Tactic.rtac @{thm excluded_middle})
boehmes@36898
   612
end
boehmes@36898
   613
boehmes@36898
   614
boehmes@42196
   615
(* |- (EX x. P x) = P c     |- ~(ALL x. P x) = ~ P c *)
boehmes@36898
   616
local
boehmes@42191
   617
  val forall =
boehmes@42191
   618
    SMT_Utils.mk_const_pat @{theory} @{const_name all}
boehmes@42191
   619
      (SMT_Utils.destT1 o SMT_Utils.destT1)
boehmes@42191
   620
  fun mk_forall cv ct =
wenzelm@46497
   621
    Thm.apply (SMT_Utils.instT' cv forall) (Thm.lambda cv ct)
boehmes@36898
   622
boehmes@42191
   623
  fun get_vars f mk pred ctxt t =
boehmes@42191
   624
    Term.fold_aterms f t []
boehmes@42191
   625
    |> map_filter (fn v =>
boehmes@42191
   626
         if pred v then SOME (SMT_Utils.certify ctxt (mk v)) else NONE)
boehmes@36898
   627
boehmes@42191
   628
  fun close vars f ct ctxt =
boehmes@42191
   629
    let
boehmes@42191
   630
      val frees_of = get_vars Term.add_frees Free (member (op =) vars o fst)
boehmes@42191
   631
      val vs = frees_of ctxt (Thm.term_of ct)
boehmes@42191
   632
      val (thm, ctxt') = f (fold_rev mk_forall vs ct) ctxt
boehmes@42191
   633
      val vars_of = get_vars Term.add_vars Var (K true) ctxt'
boehmes@42191
   634
    in (Thm.instantiate ([], vars_of (Thm.prop_of thm) ~~ vs) thm, ctxt') end
boehmes@36898
   635
boehmes@42191
   636
  val sk_rules = @{lemma
boehmes@44488
   637
    "c = (SOME x. P x) ==> (EX x. P x) = P c"
boehmes@44488
   638
    "c = (SOME x. ~P x) ==> (~(ALL x. P x)) = (~P c)"
boehmes@42191
   639
    by (metis someI_ex)+}
boehmes@36898
   640
in
boehmes@42191
   641
boehmes@42191
   642
fun skolemize vars =
boehmes@42191
   643
  apfst Thm oo close vars (yield_singleton Assumption.add_assumes)
boehmes@42191
   644
boehmes@42191
   645
fun discharge_sk_tac i st = (
boehmes@44488
   646
  Tactic.rtac @{thm trans} i
boehmes@44488
   647
  THEN Tactic.resolve_tac sk_rules i
boehmes@44488
   648
  THEN (Tactic.rtac @{thm refl} ORELSE' discharge_sk_tac) (i+1)
boehmes@44488
   649
  THEN Tactic.rtac @{thm refl} i) st
boehmes@42191
   650
boehmes@36898
   651
end
boehmes@36898
   652
boehmes@36898
   653
boehmes@42191
   654
boehmes@36898
   655
(** theory proof rules **)
boehmes@36898
   656
boehmes@36898
   657
(* theory lemmas: linear arithmetic, arrays *)
boehmes@36898
   658
fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [
boehmes@42992
   659
  Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt thms (fn ctxt' =>
boehmes@41328
   660
    Z3_Proof_Tools.by_tac (
boehmes@41328
   661
      NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
boehmes@41328
   662
      ORELSE' NAMED ctxt' "simp+arith" (
boehmes@44488
   663
        Simplifier.asm_full_simp_tac simpset
boehmes@41328
   664
        THEN_ALL_NEW Arith_Data.arith_tac ctxt')))]
boehmes@36898
   665
boehmes@36898
   666
boehmes@36898
   667
(* rewriting: prove equalities:
boehmes@36898
   668
     * ACI of conjunction/disjunction
boehmes@36898
   669
     * contradiction, excluded middle
boehmes@36898
   670
     * logical rewriting rules (for negation, implication, equivalence,
boehmes@36898
   671
         distinct)
boehmes@36898
   672
     * normal forms for polynoms (integer/real arithmetic)
boehmes@36898
   673
     * quantifier elimination over linear arithmetic
boehmes@36898
   674
     * ... ? **)
boehmes@36898
   675
structure Z3_Simps = Named_Thms
boehmes@36898
   676
(
wenzelm@45294
   677
  val name = @{binding z3_simp}
boehmes@36898
   678
  val description = "simplification rules for Z3 proof reconstruction"
boehmes@36898
   679
)
boehmes@36898
   680
boehmes@36898
   681
local
boehmes@36898
   682
  fun spec_meta_eq_of thm =
boehmes@36898
   683
    (case try (fn th => th RS @{thm spec}) thm of
boehmes@36898
   684
      SOME thm' => spec_meta_eq_of thm'
boehmes@36898
   685
    | NONE => mk_meta_eq thm)
boehmes@36898
   686
boehmes@36898
   687
  fun prep (Thm thm) = spec_meta_eq_of thm
boehmes@36898
   688
    | prep (MetaEq thm) = thm
boehmes@36898
   689
    | prep (Literals (thm, _)) = spec_meta_eq_of thm
boehmes@36898
   690
boehmes@36898
   691
  fun unfold_conv ctxt ths =
boehmes@41328
   692
    Conv.arg_conv (Conv.binop_conv (Z3_Proof_Tools.unfold_eqs ctxt
boehmes@41328
   693
      (map prep ths)))
boehmes@36898
   694
boehmes@36898
   695
  fun with_conv _ [] prv = prv
boehmes@41328
   696
    | with_conv ctxt ths prv =
boehmes@41328
   697
        Z3_Proof_Tools.with_conv (unfold_conv ctxt ths) prv
boehmes@36898
   698
boehmes@36898
   699
  val unfold_conv =
boehmes@41328
   700
    Conv.arg_conv (Conv.binop_conv
boehmes@41328
   701
      (Conv.try_conv Z3_Proof_Tools.unfold_distinct_conv))
boehmes@41328
   702
  val prove_conj_disj_eq =
boehmes@41328
   703
    Z3_Proof_Tools.with_conv unfold_conv Z3_Proof_Literals.prove_conj_disj_eq
boehmes@40663
   704
boehmes@41899
   705
  fun declare_hyps ctxt thm =
boehmes@41899
   706
    (thm, snd (Assumption.add_assumes (#hyps (Thm.crep_thm thm)) ctxt))
boehmes@36898
   707
in
boehmes@36898
   708
boehmes@42992
   709
val abstraction_depth = 3
boehmes@42992
   710
  (*
boehmes@42992
   711
    This value was chosen large enough to potentially catch exceptions,
boehmes@42992
   712
    yet small enough to not cause too much harm.  The value might be
boehmes@42992
   713
    increased in the future, if reconstructing 'rewrite' fails on problems
boehmes@42992
   714
    that get too much abstracted to be reconstructable.
boehmes@42992
   715
  *)
boehmes@42992
   716
boehmes@40663
   717
fun rewrite simpset ths ct ctxt =
boehmes@41899
   718
  apfst Thm (declare_hyps ctxt (with_conv ctxt ths (try_apply ctxt [] [
boehmes@40663
   719
    named ctxt "conj/disj/distinct" prove_conj_disj_eq,
boehmes@45392
   720
    named ctxt "pull-ite" Z3_Proof_Methods.prove_ite,
boehmes@42992
   721
    Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
boehmes@41328
   722
      Z3_Proof_Tools.by_tac (
boehmes@41328
   723
        NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
wenzelm@42793
   724
        THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
boehmes@42992
   725
    Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
boehmes@41328
   726
      Z3_Proof_Tools.by_tac (
wenzelm@46464
   727
        (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
boehmes@44488
   728
        THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
boehmes@41328
   729
        THEN_ALL_NEW (
wenzelm@42793
   730
          NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
boehmes@41328
   731
          ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
boehmes@42992
   732
    Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
boehmes@41328
   733
      Z3_Proof_Tools.by_tac (
wenzelm@46464
   734
        (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
boehmes@44488
   735
        THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
boehmes@41328
   736
        THEN_ALL_NEW (
wenzelm@42793
   737
          NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
boehmes@41328
   738
          ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
boehmes@42992
   739
    named ctxt "injectivity" (Z3_Proof_Methods.prove_injectivity ctxt),
boehmes@42992
   740
    Z3_Proof_Tools.by_abstraction abstraction_depth (true, true) ctxt []
boehmes@42992
   741
      (fn ctxt' =>
boehmes@42992
   742
        Z3_Proof_Tools.by_tac (
wenzelm@46464
   743
          (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
boehmes@44488
   744
          THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)
boehmes@42992
   745
          THEN_ALL_NEW (
boehmes@42992
   746
            NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
boehmes@42992
   747
            ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac
boehmes@42992
   748
              ctxt'))))]) ct))
boehmes@36898
   749
boehmes@36898
   750
end
boehmes@36898
   751
boehmes@36898
   752
boehmes@36898
   753
boehmes@41130
   754
(* proof reconstruction *)
boehmes@36898
   755
boehmes@41130
   756
(** tracing and checking **)
boehmes@36898
   757
boehmes@41130
   758
fun trace_before ctxt idx = SMT_Config.trace_msg ctxt (fn r =>
boehmes@41328
   759
  "Z3: #" ^ string_of_int idx ^ ": " ^ Z3_Proof_Parser.string_of_rule r)
boehmes@36898
   760
boehmes@41130
   761
fun check_after idx r ps ct (p, (ctxt, _)) =
boehmes@41130
   762
  if not (Config.get ctxt SMT_Config.trace) then ()
boehmes@41130
   763
  else
boehmes@36898
   764
    let val thm = thm_of p |> tap (Thm.join_proofs o single)
boehmes@36898
   765
    in
boehmes@36898
   766
      if (Thm.cprop_of thm) aconvc ct then ()
boehmes@41328
   767
      else
boehmes@41328
   768
        z3_exn (Pretty.string_of (Pretty.big_list
boehmes@41328
   769
          ("proof step failed: " ^ quote (Z3_Proof_Parser.string_of_rule r) ^
boehmes@41328
   770
            " (#" ^ string_of_int idx ^ ")")
boehmes@36898
   771
          (pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @
boehmes@41328
   772
            [Pretty.block [Pretty.str "expected: ",
boehmes@41328
   773
              Syntax.pretty_term ctxt (Thm.term_of ct)]])))
boehmes@36898
   774
    end
boehmes@36898
   775
boehmes@36898
   776
boehmes@41130
   777
(** overall reconstruction procedure **)
boehmes@36898
   778
boehmes@40164
   779
local
boehmes@40164
   780
  fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^
boehmes@41328
   781
    quote (Z3_Proof_Parser.string_of_rule r))
boehmes@36898
   782
boehmes@41131
   783
  fun prove_step simpset vars r ps ct (cxp as (cx, ptab)) =
boehmes@40164
   784
    (case (r, ps) of
boehmes@40164
   785
      (* core rules *)
boehmes@41328
   786
      (Z3_Proof_Parser.True_Axiom, _) => (Thm Z3_Proof_Literals.true_thm, cxp)
boehmes@41328
   787
    | (Z3_Proof_Parser.Asserted, _) => raise Fail "bad assertion"
boehmes@41328
   788
    | (Z3_Proof_Parser.Goal, _) => raise Fail "bad assertion"
boehmes@41328
   789
    | (Z3_Proof_Parser.Modus_Ponens, [(p, _), (q, _)]) =>
boehmes@41328
   790
        (mp q (thm_of p), cxp)
boehmes@41328
   791
    | (Z3_Proof_Parser.Modus_Ponens_Oeq, [(p, _), (q, _)]) =>
boehmes@41328
   792
        (mp q (thm_of p), cxp)
boehmes@41328
   793
    | (Z3_Proof_Parser.And_Elim, [(p, i)]) =>
boehmes@41328
   794
        and_elim (p, i) ct ptab ||> pair cx
boehmes@41328
   795
    | (Z3_Proof_Parser.Not_Or_Elim, [(p, i)]) =>
boehmes@41328
   796
        not_or_elim (p, i) ct ptab ||> pair cx
boehmes@41328
   797
    | (Z3_Proof_Parser.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
boehmes@41328
   798
    | (Z3_Proof_Parser.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
boehmes@41328
   799
    | (Z3_Proof_Parser.Unit_Resolution, (p, _) :: ps) =>
boehmes@40164
   800
        (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp)
boehmes@41328
   801
    | (Z3_Proof_Parser.Iff_True, [(p, _)]) => (iff_true (thm_of p), cxp)
boehmes@41328
   802
    | (Z3_Proof_Parser.Iff_False, [(p, _)]) => (iff_false (thm_of p), cxp)
boehmes@41328
   803
    | (Z3_Proof_Parser.Distributivity, _) => (distributivity cx ct, cxp)
boehmes@41328
   804
    | (Z3_Proof_Parser.Def_Axiom, _) => (def_axiom cx ct, cxp)
boehmes@41328
   805
    | (Z3_Proof_Parser.Intro_Def, _) => intro_def ct cx ||> rpair ptab
boehmes@41328
   806
    | (Z3_Proof_Parser.Apply_Def, [(p, _)]) => (apply_def (thm_of p), cxp)
boehmes@41328
   807
    | (Z3_Proof_Parser.Iff_Oeq, [(p, _)]) => (p, cxp)
boehmes@41328
   808
    | (Z3_Proof_Parser.Nnf_Pos, _) => (nnf cx vars (map fst ps) ct, cxp)
boehmes@41328
   809
    | (Z3_Proof_Parser.Nnf_Neg, _) => (nnf cx vars (map fst ps) ct, cxp)
boehmes@36898
   810
boehmes@40164
   811
      (* equality rules *)
boehmes@41328
   812
    | (Z3_Proof_Parser.Reflexivity, _) => (refl ct, cxp)
boehmes@41328
   813
    | (Z3_Proof_Parser.Symmetry, [(p, _)]) => (symm p, cxp)
boehmes@41328
   814
    | (Z3_Proof_Parser.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp)
boehmes@41328
   815
    | (Z3_Proof_Parser.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp)
boehmes@41328
   816
    | (Z3_Proof_Parser.Commutativity, _) => (commutativity ct, cxp)
boehmes@40164
   817
boehmes@40164
   818
      (* quantifier rules *)
boehmes@41328
   819
    | (Z3_Proof_Parser.Quant_Intro, [(p, _)]) => (quant_intro vars p ct, cxp)
boehmes@41328
   820
    | (Z3_Proof_Parser.Pull_Quant, _) => (pull_quant cx ct, cxp)
boehmes@41328
   821
    | (Z3_Proof_Parser.Push_Quant, _) => (push_quant cx ct, cxp)
boehmes@42318
   822
    | (Z3_Proof_Parser.Elim_Unused_Vars, _) => (elim_unused_vars ct, cxp)
boehmes@41328
   823
    | (Z3_Proof_Parser.Dest_Eq_Res, _) => (dest_eq_res cx ct, cxp)
boehmes@41328
   824
    | (Z3_Proof_Parser.Quant_Inst, _) => (quant_inst ct, cxp)
boehmes@42191
   825
    | (Z3_Proof_Parser.Skolemize, _) => skolemize vars ct cx ||> rpair ptab
boehmes@40164
   826
boehmes@40164
   827
      (* theory rules *)
boehmes@41328
   828
    | (Z3_Proof_Parser.Th_Lemma _, _) =>  (* FIXME: use arguments *)
boehmes@40164
   829
        (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
boehmes@41328
   830
    | (Z3_Proof_Parser.Rewrite, _) => rewrite simpset [] ct cx ||> rpair ptab
boehmes@41328
   831
    | (Z3_Proof_Parser.Rewrite_Star, ps) =>
boehmes@41328
   832
        rewrite simpset (map fst ps) ct cx ||> rpair ptab
boehmes@36898
   833
boehmes@41328
   834
    | (Z3_Proof_Parser.Nnf_Star, _) => not_supported r
boehmes@41328
   835
    | (Z3_Proof_Parser.Cnf_Star, _) => not_supported r
boehmes@41328
   836
    | (Z3_Proof_Parser.Transitivity_Star, _) => not_supported r
boehmes@41328
   837
    | (Z3_Proof_Parser.Pull_Quant_Star, _) => not_supported r
boehmes@36898
   838
boehmes@41328
   839
    | _ => raise Fail ("Z3: proof rule " ^
boehmes@41328
   840
        quote (Z3_Proof_Parser.string_of_rule r) ^
boehmes@41328
   841
        " has an unexpected number of arguments."))
boehmes@36898
   842
boehmes@41130
   843
  fun lookup_proof ptab idx =
boehmes@41130
   844
    (case Inttab.lookup ptab idx of
boehmes@41130
   845
      SOME p => (p, idx)
boehmes@41130
   846
    | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
boehmes@41130
   847
boehmes@41131
   848
  fun prove simpset vars (idx, step) (_, cxp as (ctxt, ptab)) =
boehmes@40164
   849
    let
boehmes@41328
   850
      val Z3_Proof_Parser.Proof_Step {rule=r, prems, prop, ...} = step
boehmes@41130
   851
      val ps = map (lookup_proof ptab) prems
boehmes@41130
   852
      val _ = trace_before ctxt idx r
boehmes@41130
   853
      val (thm, (ctxt', ptab')) =
boehmes@41130
   854
        cxp
boehmes@41131
   855
        |> prove_step simpset vars r ps prop
boehmes@41130
   856
        |> tap (check_after idx r ps prop)
boehmes@41130
   857
    in (thm, (ctxt', Inttab.update (idx, thm) ptab')) end
boehmes@36898
   858
boehmes@42191
   859
  fun make_discharge_rules rules = rules @ [@{thm allI}, @{thm refl},
boehmes@42191
   860
    @{thm reflexive}, Z3_Proof_Literals.true_thm]
boehmes@42191
   861
boehmes@45393
   862
  fun discharge_assms_tac rules =
boehmes@45393
   863
    REPEAT (HEADGOAL (
boehmes@45393
   864
      Tactic.resolve_tac rules ORELSE' SOLVED' discharge_sk_tac))
boehmes@45393
   865
    
boehmes@42191
   866
  fun discharge_assms rules thm =
boehmes@42191
   867
    if Thm.nprems_of thm = 0 then Goal.norm_result thm
boehmes@41127
   868
    else
boehmes@45393
   869
      (case Seq.pull (discharge_assms_tac rules thm) of
boehmes@45393
   870
        SOME (thm', _) => Goal.norm_result thm'
boehmes@41127
   871
      | NONE => raise THM ("failed to discharge premise", 1, [thm]))
boehmes@41127
   872
boehmes@41131
   873
  fun discharge rules outer_ctxt (p, (inner_ctxt, _)) =
boehmes@41130
   874
    thm_of p
wenzelm@42361
   875
    |> singleton (Proof_Context.export inner_ctxt outer_ctxt)
boehmes@42191
   876
    |> discharge_assms (make_discharge_rules rules)
boehmes@40164
   877
in
boehmes@40164
   878
boehmes@41127
   879
fun reconstruct outer_ctxt recon output =
boehmes@40164
   880
  let
boehmes@41127
   881
    val {context=ctxt, typs, terms, rewrite_rules, assms} = recon
boehmes@41328
   882
    val (asserted, steps, vars, ctxt1) =
boehmes@41328
   883
      Z3_Proof_Parser.parse ctxt typs terms output
boehmes@41131
   884
boehmes@41328
   885
    val simpset = Z3_Proof_Tools.make_simpset ctxt1 (Z3_Simps.get ctxt1)
boehmes@41131
   886
boehmes@41131
   887
    val ((is, rules), cxp as (ctxt2, _)) =
boehmes@41131
   888
      add_asserted outer_ctxt rewrite_rules assms asserted ctxt1
boehmes@36898
   889
  in
boehmes@41131
   890
    if Config.get ctxt2 SMT_Config.filter_only_facts then (is, @{thm TrueI})
boehmes@41127
   891
    else
boehmes@41131
   892
      (Thm @{thm TrueI}, cxp)
boehmes@41131
   893
      |> fold (prove simpset vars) steps 
boehmes@42191
   894
      |> discharge rules outer_ctxt
boehmes@41127
   895
      |> pair []
boehmes@36898
   896
  end
boehmes@36898
   897
boehmes@40164
   898
end
boehmes@36898
   899
boehmes@40164
   900
val setup = z3_rules_setup #> Z3_Simps.setup
boehmes@36898
   901
boehmes@36898
   902
end