src/HOL/Tools/SMT/z3_proof_reconstruction.ML
author boehmes
Mon Nov 08 12:13:44 2010 +0100 (2010-11-08)
changeset 40424 7550b2cba1cb
parent 40274 6486c610a549
child 40516 516a367eb38c
permissions -rw-r--r--
better modularization: moved SMT configuration options and diagnostics as well as SMT failure and exception into separate structures (both of which are loaded first and consequently are available to other SMT structures)
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@40161
    11
    (int list * thm) * Proof.context
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
structure P = Z3_Proof_Parser
boehmes@36898
    19
structure T = Z3_Proof_Tools
boehmes@36898
    20
structure L = Z3_Proof_Literals
boehmes@36898
    21
boehmes@40424
    22
fun z3_exn msg = raise SMT_Failure.SMT (SMT_Failure.Other_Failure
boehmes@40162
    23
  ("Z3 proof reconstruction: " ^ msg))
boehmes@36898
    24
boehmes@36898
    25
boehmes@36898
    26
boehmes@36898
    27
(** net of schematic rules **)
boehmes@36898
    28
boehmes@36898
    29
val z3_ruleN = "z3_rule"
boehmes@36898
    30
boehmes@36898
    31
local
boehmes@36898
    32
  val description = "declaration of Z3 proof rules"
boehmes@36898
    33
boehmes@36898
    34
  val eq = Thm.eq_thm
boehmes@36898
    35
boehmes@36898
    36
  structure Z3_Rules = Generic_Data
boehmes@36898
    37
  (
boehmes@36898
    38
    type T = thm Net.net
boehmes@36898
    39
    val empty = Net.empty
boehmes@36898
    40
    val extend = I
boehmes@36898
    41
    val merge = Net.merge eq
boehmes@36898
    42
  )
boehmes@36898
    43
boehmes@36898
    44
  val prep = `Thm.prop_of o Simplifier.rewrite_rule [L.rewrite_true]
boehmes@36898
    45
boehmes@36898
    46
  fun ins thm net = Net.insert_term eq (prep thm) net handle Net.INSERT => net
boehmes@36898
    47
  fun del thm net = Net.delete_term eq (prep thm) net handle Net.DELETE => net
boehmes@36898
    48
boehmes@36898
    49
  val add = Thm.declaration_attribute (Z3_Rules.map o ins)
boehmes@36898
    50
  val del = Thm.declaration_attribute (Z3_Rules.map o del)
boehmes@36898
    51
in
boehmes@36898
    52
boehmes@36899
    53
val add_z3_rule = Z3_Rules.map o ins
boehmes@36898
    54
boehmes@36898
    55
fun by_schematic_rule ctxt ct =
boehmes@36898
    56
  the (T.net_instance (Z3_Rules.get (Context.Proof ctxt)) ct)
boehmes@36898
    57
boehmes@36898
    58
val z3_rules_setup =
boehmes@36898
    59
  Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #>
wenzelm@39557
    60
  Global_Theory.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get)
boehmes@36898
    61
boehmes@36898
    62
end
boehmes@36898
    63
boehmes@36898
    64
boehmes@36898
    65
boehmes@36898
    66
(** proof tools **)
boehmes@36898
    67
boehmes@36898
    68
fun named ctxt name prover ct =
boehmes@40424
    69
  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
boehmes@36898
    70
  in prover ct end
boehmes@36898
    71
boehmes@36898
    72
fun NAMED ctxt name tac i st =
boehmes@40424
    73
  let val _ = SMT_Config.trace_msg ctxt I ("Z3: trying " ^ name ^ " ...")
boehmes@36898
    74
  in tac i st end
boehmes@36898
    75
boehmes@36898
    76
fun pretty_goal ctxt thms t =
boehmes@36898
    77
  [Pretty.block [Pretty.str "proposition: ", Syntax.pretty_term ctxt t]]
boehmes@36898
    78
  |> not (null thms) ? cons (Pretty.big_list "assumptions:"
boehmes@36898
    79
       (map (Display.pretty_thm ctxt) thms))
boehmes@36898
    80
boehmes@36898
    81
fun try_apply ctxt thms =
boehmes@36898
    82
  let
boehmes@36898
    83
    fun try_apply_err ct = Pretty.string_of (Pretty.chunks [
boehmes@36898
    84
      Pretty.big_list ("Z3 found a proof," ^
boehmes@36898
    85
        " but proof reconstruction failed at the following subgoal:")
boehmes@36898
    86
        (pretty_goal ctxt thms (Thm.term_of ct)),
boehmes@36898
    87
      Pretty.str ("Adding a rule to the lemma group " ^ quote z3_ruleN ^
boehmes@36898
    88
        " might solve this problem.")])
boehmes@36898
    89
boehmes@36898
    90
    fun apply [] ct = error (try_apply_err ct)
boehmes@36898
    91
      | apply (prover :: provers) ct =
boehmes@36898
    92
          (case try prover ct of
boehmes@40424
    93
            SOME thm => (SMT_Config.trace_msg ctxt I "Z3: succeeded"; thm)
boehmes@36898
    94
          | NONE => apply provers ct)
boehmes@36898
    95
boehmes@36898
    96
  in apply o cons (named ctxt "schematic rules" (by_schematic_rule ctxt)) end
boehmes@36898
    97
boehmes@36899
    98
local
boehmes@36899
    99
  val rewr_if =
boehmes@36899
   100
    @{lemma "(if P then Q1 else Q2) = ((P --> Q1) & (~P --> Q2))" by simp}
boehmes@36899
   101
in
boehmes@36899
   102
val simp_fast_tac =
boehmes@36899
   103
  Simplifier.simp_tac (HOL_ss addsimps [rewr_if])
boehmes@36899
   104
  THEN_ALL_NEW Classical.fast_tac HOL_cs
boehmes@36899
   105
end
boehmes@36899
   106
boehmes@36898
   107
boehmes@36898
   108
boehmes@36898
   109
(** theorems and proofs **)
boehmes@36898
   110
boehmes@36898
   111
(* theorem incarnations *)
boehmes@36898
   112
boehmes@36898
   113
datatype theorem =
boehmes@36898
   114
  Thm of thm | (* theorem without special features *)
boehmes@36898
   115
  MetaEq of thm | (* meta equality "t == s" *)
boehmes@36898
   116
  Literals of thm * L.littab
boehmes@36898
   117
    (* "P1 & ... & Pn" and table of all literals P1, ..., Pn *)
boehmes@36898
   118
boehmes@36898
   119
fun thm_of (Thm thm) = thm
boehmes@36898
   120
  | thm_of (MetaEq thm) = thm COMP @{thm meta_eq_to_obj_eq}
boehmes@36898
   121
  | thm_of (Literals (thm, _)) = thm
boehmes@36898
   122
boehmes@36898
   123
fun meta_eq_of (MetaEq thm) = thm
boehmes@36898
   124
  | meta_eq_of p = mk_meta_eq (thm_of p)
boehmes@36898
   125
boehmes@36898
   126
fun literals_of (Literals (_, lits)) = lits
boehmes@36898
   127
  | literals_of p = L.make_littab [thm_of p]
boehmes@36898
   128
boehmes@36898
   129
boehmes@36898
   130
(* proof representation *)
boehmes@36898
   131
boehmes@36898
   132
datatype proof = Unproved of P.proof_step | Proved of theorem
boehmes@36898
   133
boehmes@36898
   134
boehmes@36898
   135
boehmes@36898
   136
(** core proof rules **)
boehmes@36898
   137
boehmes@36898
   138
(* assumption *)
boehmes@36898
   139
boehmes@36898
   140
local
boehmes@36898
   141
  val remove_trigger = @{lemma "trigger t p == p"
boehmes@36898
   142
    by (rule eq_reflection, rule trigger_def)}
boehmes@36898
   143
boehmes@36898
   144
  val prep_rules = [@{thm Let_def}, remove_trigger, L.rewrite_true]
boehmes@36898
   145
boehmes@36898
   146
  fun rewrite_conv ctxt eqs = Simplifier.full_rewrite
boehmes@36898
   147
    (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
boehmes@36898
   148
boehmes@40164
   149
  fun rewrites f ctxt eqs = map (f (Conv.fconv_rule (rewrite_conv ctxt eqs)))
boehmes@36898
   150
boehmes@40164
   151
  fun burrow_snd_option f (i, thm) = Option.map (pair i) (f thm)
boehmes@36898
   152
  fun lookup_assm ctxt assms ct =
boehmes@40164
   153
    (case T.net_instance' burrow_snd_option assms ct of
boehmes@40164
   154
      SOME ithm => ithm
boehmes@36898
   155
    | _ => z3_exn ("not asserted: " ^
boehmes@36898
   156
        quote (Syntax.string_of_term ctxt (Thm.term_of ct))))
boehmes@36898
   157
in
boehmes@36898
   158
fun prepare_assms ctxt unfolds assms =
boehmes@36898
   159
  let
boehmes@40164
   160
    val unfolds' = rewrites I ctxt [L.rewrite_true] unfolds
boehmes@40164
   161
    val assms' =
boehmes@40164
   162
      rewrites apsnd ctxt (union Thm.eq_thm unfolds' prep_rules) assms
boehmes@40164
   163
  in (unfolds', T.thm_net_of snd assms') end
boehmes@36898
   164
boehmes@36899
   165
fun asserted ctxt (unfolds, assms) ct =
boehmes@36899
   166
  let val revert_conv = rewrite_conv ctxt unfolds
boehmes@40164
   167
  in Thm (T.with_conv revert_conv (snd o lookup_assm ctxt assms) ct) end
boehmes@40164
   168
boehmes@40164
   169
fun find_assm ctxt (unfolds, assms) ct =
boehmes@40164
   170
  fst (lookup_assm ctxt assms (Thm.rhs_of (rewrite_conv ctxt unfolds ct)))
boehmes@36898
   171
end
boehmes@36898
   172
boehmes@36898
   173
boehmes@36898
   174
boehmes@36898
   175
(* P = Q ==> P ==> Q   or   P --> Q ==> P ==> Q *)
boehmes@36898
   176
local
boehmes@36898
   177
  val meta_iffD1 = @{lemma "P == Q ==> P ==> (Q::bool)" by simp}
boehmes@36898
   178
  val meta_iffD1_c = T.precompose2 Thm.dest_binop meta_iffD1
boehmes@36898
   179
boehmes@36898
   180
  val iffD1_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm iffD1}
boehmes@36898
   181
  val mp_c = T.precompose2 (Thm.dest_binop o Thm.dest_arg) @{thm mp}
boehmes@36898
   182
in
boehmes@36898
   183
fun mp (MetaEq thm) p = Thm (Thm.implies_elim (T.compose meta_iffD1_c thm) p)
boehmes@36898
   184
  | mp p_q p = 
boehmes@36898
   185
      let
boehmes@36898
   186
        val pq = thm_of p_q
boehmes@36898
   187
        val thm = T.compose iffD1_c pq handle THM _ => T.compose mp_c pq
boehmes@36898
   188
      in Thm (Thm.implies_elim thm p) end
boehmes@36898
   189
end
boehmes@36898
   190
boehmes@36898
   191
boehmes@36898
   192
boehmes@36898
   193
(* and_elim:     P1 & ... & Pn ==> Pi *)
boehmes@36898
   194
(* not_or_elim:  ~(P1 | ... | Pn) ==> ~Pi *)
boehmes@36898
   195
local
boehmes@36898
   196
  fun is_sublit conj t = L.exists_lit conj (fn u => u aconv t)
boehmes@36898
   197
boehmes@36898
   198
  fun derive conj t lits idx ptab =
boehmes@36898
   199
    let
boehmes@36898
   200
      val lit = the (L.get_first_lit (is_sublit conj t) lits)
boehmes@36898
   201
      val ls = L.explode conj false false [t] lit
boehmes@36898
   202
      val lits' = fold L.insert_lit ls (L.delete_lit lit lits)
boehmes@36898
   203
boehmes@36898
   204
      fun upd (Proved thm) = Proved (Literals (thm_of thm, lits'))
boehmes@36898
   205
        | upd p = p
boehmes@36898
   206
    in (the (L.lookup_lit lits' t), Inttab.map_entry idx upd ptab) end
boehmes@36898
   207
boehmes@36898
   208
  fun lit_elim conj (p, idx) ct ptab =
boehmes@36898
   209
    let val lits = literals_of p
boehmes@36898
   210
    in
boehmes@36898
   211
      (case L.lookup_lit lits (T.term_of ct) of
boehmes@36898
   212
        SOME lit => (Thm lit, ptab)
boehmes@36898
   213
      | NONE => apfst Thm (derive conj (T.term_of ct) lits idx ptab))
boehmes@36898
   214
    end
boehmes@36898
   215
in
boehmes@36898
   216
val and_elim = lit_elim true
boehmes@36898
   217
val not_or_elim = lit_elim false
boehmes@36898
   218
end
boehmes@36898
   219
boehmes@36898
   220
boehmes@36898
   221
boehmes@36898
   222
(* P1, ..., Pn |- False ==> |- ~P1 | ... | ~Pn *)
boehmes@36898
   223
local
boehmes@36898
   224
  fun step lit thm =
boehmes@36898
   225
    Thm.implies_elim (Thm.implies_intr (Thm.cprop_of lit) thm) lit
boehmes@36898
   226
  val explode_disj = L.explode false false false
boehmes@36898
   227
  fun intro hyps thm th = fold step (explode_disj hyps th) thm
boehmes@36898
   228
boehmes@36898
   229
  fun dest_ccontr ct = [Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 ct))]
boehmes@36898
   230
  val ccontr = T.precompose dest_ccontr @{thm ccontr}
boehmes@36898
   231
in
boehmes@36898
   232
fun lemma thm ct =
boehmes@36898
   233
  let
boehmes@36898
   234
    val cu = Thm.capply @{cterm Not} (Thm.dest_arg ct)
boehmes@36898
   235
    val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
boehmes@36898
   236
  in Thm (T.compose ccontr (T.under_assumption (intro hyps thm) cu)) end
boehmes@36898
   237
end
boehmes@36898
   238
boehmes@36898
   239
boehmes@36898
   240
boehmes@36898
   241
(* \/{P1, ..., Pn, Q1, ..., Qn}, ~P1, ..., ~Pn ==> \/{Q1, ..., Qn} *)
boehmes@36898
   242
local
boehmes@36898
   243
  val explode_disj = L.explode false true false
boehmes@36898
   244
  val join_disj = L.join false
boehmes@36898
   245
  fun unit thm thms th =
boehmes@36898
   246
    let val t = @{term Not} $ T.prop_of thm and ts = map T.prop_of thms
boehmes@36898
   247
    in join_disj (L.make_littab (thms @ explode_disj ts th)) t end
boehmes@36898
   248
boehmes@36898
   249
  fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
boehmes@36898
   250
  fun dest ct = pairself dest_arg2 (Thm.dest_binop ct)
boehmes@36898
   251
  val contrapos = T.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
boehmes@36898
   252
in
boehmes@36898
   253
fun unit_resolution thm thms ct =
boehmes@36898
   254
  Thm.capply @{cterm Not} (Thm.dest_arg ct)
boehmes@36898
   255
  |> T.under_assumption (unit thm thms)
boehmes@36898
   256
  |> Thm o T.discharge thm o T.compose contrapos
boehmes@36898
   257
end
boehmes@36898
   258
boehmes@36898
   259
boehmes@36898
   260
boehmes@36898
   261
(* P ==> P == True   or   P ==> P == False *)
boehmes@36898
   262
local
boehmes@36898
   263
  val iff1 = @{lemma "P ==> P == (~ False)" by simp}
boehmes@36898
   264
  val iff2 = @{lemma "~P ==> P == False" by simp}
boehmes@36898
   265
in
boehmes@36898
   266
fun iff_true thm = MetaEq (thm COMP iff1)
boehmes@36898
   267
fun iff_false thm = MetaEq (thm COMP iff2)
boehmes@36898
   268
end
boehmes@36898
   269
boehmes@36898
   270
boehmes@36898
   271
boehmes@36898
   272
(* distributivity of | over & *)
boehmes@36898
   273
fun distributivity ctxt = Thm o try_apply ctxt [] [
boehmes@36899
   274
  named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
boehmes@36898
   275
    (* FIXME: not very well tested *)
boehmes@36898
   276
boehmes@36898
   277
boehmes@36898
   278
boehmes@36898
   279
(* Tseitin-like axioms *)
boehmes@36898
   280
boehmes@36898
   281
local
boehmes@36898
   282
  val disjI1 = @{lemma "(P ==> Q) ==> ~P | Q" by fast}
boehmes@36898
   283
  val disjI2 = @{lemma "(~P ==> Q) ==> P | Q" by fast}
boehmes@36898
   284
  val disjI3 = @{lemma "(~Q ==> P) ==> P | Q" by fast}
boehmes@36898
   285
  val disjI4 = @{lemma "(Q ==> P) ==> P | ~Q" by fast}
boehmes@36898
   286
boehmes@36898
   287
  fun prove' conj1 conj2 ct2 thm =
boehmes@36898
   288
    let val lits = L.true_thm :: L.explode conj1 true (conj1 <> conj2) [] thm
boehmes@36898
   289
    in L.join conj2 (L.make_littab lits) (Thm.term_of ct2) end
boehmes@36898
   290
boehmes@36898
   291
  fun prove rule (ct1, conj1) (ct2, conj2) =
boehmes@36898
   292
    T.under_assumption (prove' conj1 conj2 ct2) ct1 COMP rule
boehmes@36898
   293
boehmes@36898
   294
  fun prove_def_axiom ct =
boehmes@36898
   295
    let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
boehmes@36898
   296
    in
boehmes@36898
   297
      (case Thm.term_of ct1 of
haftmann@38795
   298
        @{term Not} $ (@{term HOL.conj} $ _ $ _) =>
boehmes@36898
   299
          prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
haftmann@38795
   300
      | @{term HOL.conj} $ _ $ _ =>
boehmes@36898
   301
          prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, true)
haftmann@38795
   302
      | @{term Not} $ (@{term HOL.disj} $ _ $ _) =>
boehmes@36898
   303
          prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false)
haftmann@38795
   304
      | @{term HOL.disj} $ _ $ _ =>
boehmes@36898
   305
          prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true)
boehmes@40274
   306
      | Const (@{const_name SMT.distinct}, _) $ _ =>
boehmes@36898
   307
          let
boehmes@36898
   308
            fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
boehmes@36898
   309
            fun prv cu =
boehmes@36898
   310
              let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
boehmes@36898
   311
              in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
boehmes@36898
   312
          in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
boehmes@40274
   313
      | @{term Not} $ (Const (@{const_name SMT.distinct}, _) $ _) =>
boehmes@36898
   314
          let
boehmes@36898
   315
            fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
boehmes@36898
   316
            fun prv cu =
boehmes@36898
   317
              let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
boehmes@36898
   318
              in prove disjI1 (Thm.dest_arg cu1, true) (cu2, true) end
boehmes@36898
   319
          in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
boehmes@36898
   320
      | _ => raise CTERM ("prove_def_axiom", [ct]))
boehmes@36898
   321
    end
boehmes@36898
   322
in
boehmes@36898
   323
fun def_axiom ctxt = Thm o try_apply ctxt [] [
boehmes@36898
   324
  named ctxt "conj/disj/distinct" prove_def_axiom,
boehmes@36899
   325
  T.by_abstraction (true, false) ctxt [] (fn ctxt' =>
boehmes@36899
   326
    named ctxt' "simp+fast" (T.by_tac simp_fast_tac))]
boehmes@36898
   327
end
boehmes@36898
   328
boehmes@36898
   329
boehmes@36898
   330
boehmes@36898
   331
(* local definitions *)
boehmes@36898
   332
local
boehmes@36898
   333
  val intro_rules = [
boehmes@36898
   334
    @{lemma "n == P ==> (~n | P) & (n | ~P)" by simp},
boehmes@36898
   335
    @{lemma "n == (if P then s else t) ==> (~P | n = s) & (P | n = t)"
boehmes@36898
   336
      by simp},
boehmes@36898
   337
    @{lemma "n == P ==> n = P" by (rule meta_eq_to_obj_eq)} ]
boehmes@36898
   338
boehmes@36898
   339
  val apply_rules = [
boehmes@36898
   340
    @{lemma "(~n | P) & (n | ~P) ==> P == n" by (atomize(full)) fast},
boehmes@36898
   341
    @{lemma "(~P | n = s) & (P | n = t) ==> (if P then s else t) == n"
boehmes@36898
   342
      by (atomize(full)) fastsimp} ]
boehmes@36898
   343
boehmes@36898
   344
  val inst_rule = T.match_instantiate Thm.dest_arg
boehmes@36898
   345
boehmes@36898
   346
  fun apply_rule ct =
boehmes@36898
   347
    (case get_first (try (inst_rule ct)) intro_rules of
boehmes@36898
   348
      SOME thm => thm
boehmes@36898
   349
    | NONE => raise CTERM ("intro_def", [ct]))
boehmes@36898
   350
in
boehmes@36898
   351
fun intro_def ct = T.make_hyp_def (apply_rule ct) #>> Thm
boehmes@36898
   352
boehmes@36898
   353
fun apply_def thm =
boehmes@36898
   354
  get_first (try (fn rule => MetaEq (thm COMP rule))) apply_rules
boehmes@36898
   355
  |> the_default (Thm thm)
boehmes@36898
   356
end
boehmes@36898
   357
boehmes@36898
   358
boehmes@36898
   359
boehmes@36898
   360
(* negation normal form *)
boehmes@36898
   361
boehmes@36898
   362
local
boehmes@36898
   363
  val quant_rules1 = ([
boehmes@36898
   364
    @{lemma "(!!x. P x == Q) ==> ALL x. P x == Q" by simp},
boehmes@36898
   365
    @{lemma "(!!x. P x == Q) ==> EX x. P x == Q" by simp}], [
boehmes@36898
   366
    @{lemma "(!!x. P x == Q x) ==> ALL x. P x == ALL x. Q x" by simp},
boehmes@36898
   367
    @{lemma "(!!x. P x == Q x) ==> EX x. P x == EX x. Q x" by simp}])
boehmes@36898
   368
boehmes@36898
   369
  val quant_rules2 = ([
boehmes@36898
   370
    @{lemma "(!!x. ~P x == Q) ==> ~(ALL x. P x) == Q" by simp},
boehmes@36898
   371
    @{lemma "(!!x. ~P x == Q) ==> ~(EX x. P x) == Q" by simp}], [
boehmes@36898
   372
    @{lemma "(!!x. ~P x == Q x) ==> ~(ALL x. P x) == EX x. Q x" by simp},
boehmes@36898
   373
    @{lemma "(!!x. ~P x == Q x) ==> ~(EX x. P x) == ALL x. Q x" by simp}])
boehmes@36898
   374
boehmes@36898
   375
  fun nnf_quant_tac thm (qs as (qs1, qs2)) i st = (
boehmes@36898
   376
    Tactic.rtac thm ORELSE'
boehmes@36898
   377
    (Tactic.match_tac qs1 THEN' nnf_quant_tac thm qs) ORELSE'
boehmes@36898
   378
    (Tactic.match_tac qs2 THEN' nnf_quant_tac thm qs)) i st
boehmes@36898
   379
boehmes@36898
   380
  fun nnf_quant vars qs p ct =
boehmes@36898
   381
    T.as_meta_eq ct
boehmes@36898
   382
    |> T.by_tac (nnf_quant_tac (T.varify vars (meta_eq_of p)) qs)
boehmes@36898
   383
boehmes@36898
   384
  fun prove_nnf ctxt = try_apply ctxt [] [
boehmes@36899
   385
    named ctxt "conj/disj" L.prove_conj_disj_eq,
boehmes@36899
   386
    T.by_abstraction (true, false) ctxt [] (fn ctxt' =>
boehmes@36899
   387
      named ctxt' "simp+fast" (T.by_tac simp_fast_tac))]
boehmes@36898
   388
in
boehmes@36898
   389
fun nnf ctxt vars ps ct =
boehmes@36898
   390
  (case T.term_of ct of
boehmes@36898
   391
    _ $ (l as Const _ $ Abs _) $ (r as Const _ $ Abs _) =>
boehmes@36898
   392
      if l aconv r
boehmes@36898
   393
      then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
boehmes@36898
   394
      else MetaEq (nnf_quant vars quant_rules1 (hd ps) ct)
boehmes@36898
   395
  | _ $ (@{term Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
boehmes@36898
   396
      MetaEq (nnf_quant vars quant_rules2 (hd ps) ct)
boehmes@36898
   397
  | _ =>
boehmes@36898
   398
      let
boehmes@36898
   399
        val nnf_rewr_conv = Conv.arg_conv (Conv.arg_conv
boehmes@36898
   400
          (T.unfold_eqs ctxt (map (Thm.symmetric o meta_eq_of) ps)))
boehmes@36898
   401
      in Thm (T.with_conv nnf_rewr_conv (prove_nnf ctxt) ct) end)
boehmes@36898
   402
end
boehmes@36898
   403
boehmes@36898
   404
boehmes@36898
   405
boehmes@36898
   406
(** equality proof rules **)
boehmes@36898
   407
boehmes@36898
   408
(* |- t = t *)
boehmes@36898
   409
fun refl ct = MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
boehmes@36898
   410
boehmes@36898
   411
boehmes@36898
   412
boehmes@36898
   413
(* s = t ==> t = s *)
boehmes@36898
   414
local
boehmes@36898
   415
  val symm_rule = @{lemma "s = t ==> t == s" by simp}
boehmes@36898
   416
in
boehmes@36898
   417
fun symm (MetaEq thm) = MetaEq (Thm.symmetric thm)
boehmes@36898
   418
  | symm p = MetaEq (thm_of p COMP symm_rule)
boehmes@36898
   419
end
boehmes@36898
   420
boehmes@36898
   421
boehmes@36898
   422
boehmes@36898
   423
(* s = t ==> t = u ==> s = u *)
boehmes@36898
   424
local
boehmes@36898
   425
  val trans1 = @{lemma "s == t ==> t =  u ==> s == u" by simp}
boehmes@36898
   426
  val trans2 = @{lemma "s =  t ==> t == u ==> s == u" by simp}
boehmes@36898
   427
  val trans3 = @{lemma "s =  t ==> t =  u ==> s == u" by simp}
boehmes@36898
   428
in
boehmes@36898
   429
fun trans (MetaEq thm1) (MetaEq thm2) = MetaEq (Thm.transitive thm1 thm2)
boehmes@36898
   430
  | trans (MetaEq thm) q = MetaEq (thm_of q COMP (thm COMP trans1))
boehmes@36898
   431
  | trans p (MetaEq thm) = MetaEq (thm COMP (thm_of p COMP trans2))
boehmes@36898
   432
  | trans p q = MetaEq (thm_of q COMP (thm_of p COMP trans3))
boehmes@36898
   433
end
boehmes@36898
   434
boehmes@36898
   435
boehmes@36898
   436
boehmes@36898
   437
(* t1 = s1 ==> ... ==> tn = sn ==> f t1 ... tn = f s1 .. sn
boehmes@36898
   438
   (reflexive antecendents are droppped) *)
boehmes@36898
   439
local
boehmes@36898
   440
  exception MONO
boehmes@36898
   441
boehmes@36898
   442
  fun prove_refl (ct, _) = Thm.reflexive ct
boehmes@36898
   443
  fun prove_comb f g cp =
boehmes@36898
   444
    let val ((ct1, ct2), (cu1, cu2)) = pairself Thm.dest_comb cp
boehmes@36898
   445
    in Thm.combination (f (ct1, cu1)) (g (ct2, cu2)) end
boehmes@36898
   446
  fun prove_arg f = prove_comb prove_refl f
boehmes@36898
   447
boehmes@36898
   448
  fun prove f cp = prove_comb (prove f) f cp handle CTERM _ => prove_refl cp
boehmes@36898
   449
boehmes@36898
   450
  fun prove_nary is_comb f =
boehmes@36898
   451
    let
boehmes@36898
   452
      fun prove (cp as (ct, _)) = f cp handle MONO =>
boehmes@36898
   453
        if is_comb (Thm.term_of ct)
boehmes@36898
   454
        then prove_comb (prove_arg prove) prove cp
boehmes@36898
   455
        else prove_refl cp
boehmes@36898
   456
    in prove end
boehmes@36898
   457
boehmes@36898
   458
  fun prove_list f n cp =
boehmes@36898
   459
    if n = 0 then prove_refl cp
boehmes@36898
   460
    else prove_comb (prove_arg f) (prove_list f (n-1)) cp
boehmes@36898
   461
boehmes@36898
   462
  fun with_length f (cp as (cl, _)) =
boehmes@36898
   463
    f (length (HOLogic.dest_list (Thm.term_of cl))) cp
boehmes@36898
   464
boehmes@36898
   465
  fun prove_distinct f = prove_arg (with_length (prove_list f))
boehmes@36898
   466
boehmes@36898
   467
  fun prove_eq exn lookup cp =
boehmes@36898
   468
    (case lookup (Logic.mk_equals (pairself Thm.term_of cp)) of
boehmes@36898
   469
      SOME eq => eq
boehmes@36898
   470
    | NONE => if exn then raise MONO else prove_refl cp)
boehmes@36898
   471
  
boehmes@36898
   472
  val prove_eq_exn = prove_eq true
boehmes@36898
   473
  and prove_eq_safe = prove_eq false
boehmes@36898
   474
boehmes@36898
   475
  fun mono f (cp as (cl, _)) =
boehmes@36898
   476
    (case Term.head_of (Thm.term_of cl) of
haftmann@38795
   477
      @{term HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
haftmann@38795
   478
    | @{term HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
boehmes@40274
   479
    | Const (@{const_name SMT.distinct}, _) => prove_distinct (prove_eq_safe f)
boehmes@36898
   480
    | _ => prove (prove_eq_safe f)) cp
boehmes@36898
   481
in
boehmes@36898
   482
fun monotonicity eqs ct =
boehmes@36898
   483
  let
boehmes@36898
   484
    val lookup = AList.lookup (op aconv) (map (`Thm.prop_of o meta_eq_of) eqs)
boehmes@36898
   485
    val cp = Thm.dest_binop (Thm.dest_arg ct)
boehmes@36898
   486
  in MetaEq (prove_eq_exn lookup cp handle MONO => mono lookup cp) end
boehmes@36898
   487
end
boehmes@36898
   488
boehmes@36898
   489
boehmes@36898
   490
boehmes@36898
   491
(* |- f a b = f b a (where f is equality) *)
boehmes@36898
   492
local
boehmes@36898
   493
  val rule = @{lemma "a = b == b = a" by (atomize(full)) (rule eq_commute)}
boehmes@36898
   494
in
boehmes@36898
   495
fun commutativity ct = MetaEq (T.match_instantiate I (T.as_meta_eq ct) rule)
boehmes@36898
   496
end
boehmes@36898
   497
boehmes@36898
   498
boehmes@36898
   499
boehmes@36898
   500
(** quantifier proof rules **)
boehmes@36898
   501
boehmes@36898
   502
(* P ?x = Q ?x ==> (ALL x. P x) = (ALL x. Q x)
boehmes@36898
   503
   P ?x = Q ?x ==> (EX x. P x) = (EX x. Q x)    *)
boehmes@36898
   504
local
boehmes@36898
   505
  val rules = [
boehmes@36898
   506
    @{lemma "(!!x. P x == Q x) ==> (ALL x. P x) == (ALL x. Q x)" by simp},
boehmes@36898
   507
    @{lemma "(!!x. P x == Q x) ==> (EX x. P x) == (EX x. Q x)" by simp}]
boehmes@36898
   508
in
boehmes@36898
   509
fun quant_intro vars p ct =
boehmes@36898
   510
  let
boehmes@36898
   511
    val thm = meta_eq_of p
boehmes@36898
   512
    val rules' = T.varify vars thm :: rules
boehmes@36898
   513
    val cu = T.as_meta_eq ct
boehmes@36898
   514
  in MetaEq (T.by_tac (REPEAT_ALL_NEW (Tactic.match_tac rules')) cu) end
boehmes@36898
   515
end
boehmes@36898
   516
boehmes@36898
   517
boehmes@36898
   518
boehmes@36898
   519
(* |- ((ALL x. P x) | Q) = (ALL x. P x | Q) *)
boehmes@36898
   520
fun pull_quant ctxt = Thm o try_apply ctxt [] [
boehmes@36898
   521
  named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
boehmes@36898
   522
    (* FIXME: not very well tested *)
boehmes@36898
   523
boehmes@36898
   524
boehmes@36898
   525
boehmes@36898
   526
(* |- (ALL x. P x & Q x) = ((ALL x. P x) & (ALL x. Q x)) *)
boehmes@36898
   527
fun push_quant ctxt = Thm o try_apply ctxt [] [
boehmes@36898
   528
  named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
boehmes@36898
   529
    (* FIXME: not very well tested *)
boehmes@36898
   530
boehmes@36898
   531
boehmes@36898
   532
boehmes@36898
   533
(* |- (ALL x1 ... xn y1 ... yn. P x1 ... xn) = (ALL x1 ... xn. P x1 ... xn) *)
boehmes@36898
   534
local
boehmes@36898
   535
  val elim_all = @{lemma "(ALL x. P) == P" by simp}
boehmes@36898
   536
  val elim_ex = @{lemma "(EX x. P) == P" by simp}
boehmes@36898
   537
boehmes@36898
   538
  fun elim_unused_conv ctxt =
boehmes@36898
   539
    Conv.params_conv ~1 (K (Conv.arg_conv (Conv.arg1_conv
wenzelm@36936
   540
      (Conv.rewrs_conv [elim_all, elim_ex])))) ctxt
boehmes@36898
   541
boehmes@36898
   542
  fun elim_unused_tac ctxt =
boehmes@36898
   543
    REPEAT_ALL_NEW (
boehmes@36898
   544
      Tactic.match_tac [@{thm refl}, @{thm iff_allI}, @{thm iff_exI}]
boehmes@36898
   545
      ORELSE' CONVERSION (elim_unused_conv ctxt))
boehmes@36898
   546
in
boehmes@36898
   547
fun elim_unused_vars ctxt = Thm o T.by_tac (elim_unused_tac ctxt)
boehmes@36898
   548
end
boehmes@36898
   549
boehmes@36898
   550
boehmes@36898
   551
boehmes@36898
   552
(* |- (ALL x1 ... xn. ~(x1 = t1 & ... xn = tn) | P x1 ... xn) = P t1 ... tn *)
boehmes@36898
   553
fun dest_eq_res ctxt = Thm o try_apply ctxt [] [
boehmes@36898
   554
  named ctxt "fast" (T.by_tac (Classical.fast_tac HOL_cs))]
boehmes@36898
   555
    (* FIXME: not very well tested *)
boehmes@36898
   556
boehmes@36898
   557
boehmes@36898
   558
boehmes@36898
   559
(* |- ~(ALL x1...xn. P x1...xn) | P a1...an *)
boehmes@36898
   560
local
boehmes@36898
   561
  val rule = @{lemma "~ P x | Q ==> ~(ALL x. P x) | Q" by fast}
boehmes@36898
   562
in
boehmes@36898
   563
val quant_inst = Thm o T.by_tac (
boehmes@36898
   564
  REPEAT_ALL_NEW (Tactic.match_tac [rule])
boehmes@36898
   565
  THEN' Tactic.rtac @{thm excluded_middle})
boehmes@36898
   566
end
boehmes@36898
   567
boehmes@36898
   568
boehmes@36898
   569
boehmes@36898
   570
(* c = SOME x. P x |- (EX x. P x) = P c
boehmes@36898
   571
   c = SOME x. ~ P x |- ~(ALL x. P x) = ~ P c *)
boehmes@36898
   572
local
boehmes@36898
   573
  val elim_ex = @{lemma "EX x. P == P" by simp}
boehmes@36898
   574
  val elim_all = @{lemma "~ (ALL x. P) == ~P" by simp}
boehmes@36898
   575
  val sk_ex = @{lemma "c == SOME x. P x ==> EX x. P x == P c"
boehmes@36898
   576
    by simp (intro eq_reflection some_eq_ex[symmetric])}
boehmes@36898
   577
  val sk_all = @{lemma "c == SOME x. ~ P x ==> ~(ALL x. P x) == ~ P c"
boehmes@36898
   578
    by (simp only: not_all) (intro eq_reflection some_eq_ex[symmetric])}
boehmes@36898
   579
  val sk_ex_rule = ((sk_ex, I), elim_ex)
boehmes@36898
   580
  and sk_all_rule = ((sk_all, Thm.dest_arg), elim_all)
boehmes@36898
   581
boehmes@36898
   582
  fun dest f sk_rule = 
boehmes@36898
   583
    Thm.dest_comb (f (Thm.dest_arg (Thm.dest_arg (Thm.cprop_of sk_rule))))
boehmes@36898
   584
  fun type_of f sk_rule = Thm.ctyp_of_term (snd (dest f sk_rule))
boehmes@36898
   585
  fun pair2 (a, b) (c, d) = [(a, c), (b, d)]
boehmes@36898
   586
  fun inst_sk (sk_rule, f) p c =
boehmes@36898
   587
    Thm.instantiate ([(type_of f sk_rule, Thm.ctyp_of_term c)], []) sk_rule
boehmes@36898
   588
    |> (fn sk' => Thm.instantiate ([], (pair2 (dest f sk') (p, c))) sk')
boehmes@36898
   589
    |> Conv.fconv_rule (Thm.beta_conversion true)
boehmes@36898
   590
boehmes@36898
   591
  fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I)
boehmes@36898
   592
    | kind (@{term Not} $ (Const (@{const_name All}, _) $ _)) =
boehmes@36898
   593
        (sk_all_rule, Thm.dest_arg, Thm.capply @{cterm Not})
boehmes@36898
   594
    | kind t = raise TERM ("skolemize", [t])
boehmes@36898
   595
boehmes@36898
   596
  fun dest_abs_type (Abs (_, T, _)) = T
boehmes@36898
   597
    | dest_abs_type t = raise TERM ("dest_abs_type", [t])
boehmes@36898
   598
boehmes@36898
   599
  fun bodies_of thy lhs rhs =
boehmes@36898
   600
    let
boehmes@36898
   601
      val (rule, dest, make) = kind (Thm.term_of lhs)
boehmes@36898
   602
boehmes@36898
   603
      fun dest_body idx cbs ct =
boehmes@36898
   604
        let
boehmes@36898
   605
          val cb = Thm.dest_arg (dest ct)
boehmes@36898
   606
          val T = dest_abs_type (Thm.term_of cb)
boehmes@36898
   607
          val cv = Thm.cterm_of thy (Var (("x", idx), T))
boehmes@36898
   608
          val cu = make (Drule.beta_conv cb cv)
boehmes@36898
   609
          val cbs' = (cv, cb) :: cbs
boehmes@36898
   610
        in
boehmes@36898
   611
          (snd (Thm.first_order_match (cu, rhs)), rev cbs')
boehmes@36898
   612
          handle Pattern.MATCH => dest_body (idx+1) cbs' cu
boehmes@36898
   613
        end
boehmes@36898
   614
    in (rule, dest_body 1 [] lhs) end
boehmes@36898
   615
boehmes@36898
   616
  fun transitive f thm = Thm.transitive thm (f (Thm.rhs_of thm))
boehmes@36898
   617
boehmes@36898
   618
  fun sk_step (rule, elim) (cv, mct, cb) ((is, thm), ctxt) =
boehmes@36898
   619
    (case mct of
boehmes@36898
   620
      SOME ct =>
boehmes@36898
   621
        ctxt
boehmes@36898
   622
        |> T.make_hyp_def (inst_sk rule (Thm.instantiate_cterm ([], is) cb) ct)
boehmes@36898
   623
        |>> pair ((cv, ct) :: is) o Thm.transitive thm
boehmes@36898
   624
    | NONE => ((is, transitive (Conv.rewr_conv elim) thm), ctxt))
boehmes@36898
   625
in
boehmes@36898
   626
fun skolemize ct ctxt =
boehmes@36898
   627
  let
boehmes@36898
   628
    val (lhs, rhs) = Thm.dest_binop (Thm.dest_arg ct)
boehmes@36898
   629
    val (rule, (ctab, cbs)) = bodies_of (ProofContext.theory_of ctxt) lhs rhs
boehmes@36898
   630
    fun lookup_var (cv, cb) = (cv, AList.lookup (op aconvc) ctab cv, cb)
boehmes@36898
   631
  in
boehmes@36898
   632
    (([], Thm.reflexive lhs), ctxt)
boehmes@36898
   633
    |> fold (sk_step rule) (map lookup_var cbs)
boehmes@36898
   634
    |>> MetaEq o snd
boehmes@36898
   635
  end
boehmes@36898
   636
end
boehmes@36898
   637
boehmes@36898
   638
boehmes@36898
   639
boehmes@36898
   640
(** theory proof rules **)
boehmes@36898
   641
boehmes@36898
   642
(* theory lemmas: linear arithmetic, arrays *)
boehmes@36898
   643
boehmes@36898
   644
fun th_lemma ctxt simpset thms = Thm o try_apply ctxt thms [
boehmes@36899
   645
  T.by_abstraction (false, true) ctxt thms (fn ctxt' => T.by_tac (
boehmes@36898
   646
    NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
boehmes@36898
   647
    ORELSE' NAMED ctxt' "simp+arith" (Simplifier.simp_tac simpset THEN_ALL_NEW
boehmes@36898
   648
      Arith_Data.arith_tac ctxt')))]
boehmes@36898
   649
boehmes@36898
   650
boehmes@36898
   651
boehmes@36898
   652
(* rewriting: prove equalities:
boehmes@36898
   653
     * ACI of conjunction/disjunction
boehmes@36898
   654
     * contradiction, excluded middle
boehmes@36898
   655
     * logical rewriting rules (for negation, implication, equivalence,
boehmes@36898
   656
         distinct)
boehmes@36898
   657
     * normal forms for polynoms (integer/real arithmetic)
boehmes@36898
   658
     * quantifier elimination over linear arithmetic
boehmes@36898
   659
     * ... ? **)
boehmes@36898
   660
structure Z3_Simps = Named_Thms
boehmes@36898
   661
(
boehmes@36898
   662
  val name = "z3_simp"
boehmes@36898
   663
  val description = "simplification rules for Z3 proof reconstruction"
boehmes@36898
   664
)
boehmes@36898
   665
boehmes@36898
   666
local
boehmes@36898
   667
  fun spec_meta_eq_of thm =
boehmes@36898
   668
    (case try (fn th => th RS @{thm spec}) thm of
boehmes@36898
   669
      SOME thm' => spec_meta_eq_of thm'
boehmes@36898
   670
    | NONE => mk_meta_eq thm)
boehmes@36898
   671
boehmes@36898
   672
  fun prep (Thm thm) = spec_meta_eq_of thm
boehmes@36898
   673
    | prep (MetaEq thm) = thm
boehmes@36898
   674
    | prep (Literals (thm, _)) = spec_meta_eq_of thm
boehmes@36898
   675
boehmes@36898
   676
  fun unfold_conv ctxt ths =
boehmes@36898
   677
    Conv.arg_conv (Conv.binop_conv (T.unfold_eqs ctxt (map prep ths)))
boehmes@36898
   678
boehmes@36898
   679
  fun with_conv _ [] prv = prv
boehmes@36898
   680
    | with_conv ctxt ths prv = T.with_conv (unfold_conv ctxt ths) prv
boehmes@36898
   681
boehmes@36898
   682
  val unfold_conv =
boehmes@36898
   683
    Conv.arg_conv (Conv.binop_conv (Conv.try_conv T.unfold_distinct_conv))
boehmes@36898
   684
  val prove_conj_disj_eq = T.with_conv unfold_conv L.prove_conj_disj_eq
boehmes@36898
   685
in
boehmes@36898
   686
boehmes@36898
   687
fun rewrite ctxt simpset ths = Thm o with_conv ctxt ths (try_apply ctxt [] [
boehmes@36898
   688
  named ctxt "conj/disj/distinct" prove_conj_disj_eq,
boehmes@37126
   689
  T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac (
boehmes@37126
   690
    NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
boehmes@37126
   691
    THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
boehmes@37126
   692
  T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac (
boehmes@37126
   693
    NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
boehmes@36898
   694
    THEN_ALL_NEW (
boehmes@37126
   695
      NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
boehmes@37126
   696
      ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
boehmes@37126
   697
  T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
boehmes@37126
   698
    NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
boehmes@37126
   699
    THEN_ALL_NEW (
boehmes@37126
   700
      NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
boehmes@37126
   701
      ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt'))))])
boehmes@36898
   702
boehmes@36898
   703
end
boehmes@36898
   704
boehmes@36898
   705
boehmes@36898
   706
boehmes@36898
   707
(** proof reconstruction **)
boehmes@36898
   708
boehmes@36898
   709
(* tracing and checking *)
boehmes@36898
   710
boehmes@36898
   711
local
boehmes@36898
   712
  fun count_rules ptab =
boehmes@36898
   713
    let
boehmes@36898
   714
      fun count (_, Unproved _) (solved, total) = (solved, total + 1)
boehmes@36898
   715
        | count (_, Proved _) (solved, total) = (solved + 1, total + 1)
boehmes@36898
   716
    in Inttab.fold count ptab (0, 0) end
boehmes@36898
   717
boehmes@36898
   718
  fun header idx r (solved, total) = 
boehmes@36898
   719
    "Z3: #" ^ string_of_int idx ^ ": " ^ P.string_of_rule r ^ " (goal " ^
boehmes@36898
   720
    string_of_int (solved + 1) ^ " of " ^ string_of_int total ^ ")"
boehmes@36898
   721
boehmes@36898
   722
  fun check ctxt idx r ps ct p =
boehmes@36898
   723
    let val thm = thm_of p |> tap (Thm.join_proofs o single)
boehmes@36898
   724
    in
boehmes@36898
   725
      if (Thm.cprop_of thm) aconvc ct then ()
boehmes@36898
   726
      else z3_exn (Pretty.string_of (Pretty.big_list ("proof step failed: " ^
boehmes@36898
   727
        quote (P.string_of_rule r) ^ " (#" ^ string_of_int idx ^ ")")
boehmes@36898
   728
          (pretty_goal ctxt (map (thm_of o fst) ps) (Thm.prop_of thm) @
boehmes@36898
   729
           [Pretty.block [Pretty.str "expected: ",
boehmes@36898
   730
            Syntax.pretty_term ctxt (Thm.term_of ct)]])))
boehmes@36898
   731
    end
boehmes@36898
   732
in
boehmes@36898
   733
fun trace_rule idx prove r ps ct (cxp as (ctxt, ptab)) =
boehmes@36898
   734
  let
boehmes@40424
   735
    val _ = SMT_Config.trace_msg ctxt (header idx r o count_rules) ptab
boehmes@36899
   736
    val result as (p, (ctxt', _)) = prove r ps ct cxp
boehmes@40424
   737
    val _ = if not (Config.get ctxt' SMT_Config.trace) then ()
boehmes@36898
   738
      else check ctxt' idx r ps ct p
boehmes@36898
   739
  in result end
boehmes@36898
   740
end
boehmes@36898
   741
boehmes@36898
   742
boehmes@36898
   743
(* overall reconstruction procedure *)
boehmes@36898
   744
boehmes@40164
   745
local
boehmes@40164
   746
  fun not_supported r = raise Fail ("Z3: proof rule not implemented: " ^
boehmes@40164
   747
    quote (P.string_of_rule r))
boehmes@36898
   748
boehmes@40164
   749
  fun step assms simpset vars r ps ct (cxp as (cx, ptab)) =
boehmes@40164
   750
    (case (r, ps) of
boehmes@40164
   751
      (* core rules *)
boehmes@40164
   752
      (P.TrueAxiom, _) => (Thm L.true_thm, cxp)
boehmes@40164
   753
    | (P.Asserted, _) => (asserted cx assms ct, cxp)
boehmes@40164
   754
    | (P.Goal, _) => (asserted cx assms ct, cxp)
boehmes@40164
   755
    | (P.ModusPonens, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
boehmes@40164
   756
    | (P.ModusPonensOeq, [(p, _), (q, _)]) => (mp q (thm_of p), cxp)
boehmes@40164
   757
    | (P.AndElim, [(p, i)]) => and_elim (p, i) ct ptab ||> pair cx
boehmes@40164
   758
    | (P.NotOrElim, [(p, i)]) => not_or_elim (p, i) ct ptab ||> pair cx
boehmes@40164
   759
    | (P.Hypothesis, _) => (Thm (Thm.assume ct), cxp)
boehmes@40164
   760
    | (P.Lemma, [(p, _)]) => (lemma (thm_of p) ct, cxp)
boehmes@40164
   761
    | (P.UnitResolution, (p, _) :: ps) =>
boehmes@40164
   762
        (unit_resolution (thm_of p) (map (thm_of o fst) ps) ct, cxp)
boehmes@40164
   763
    | (P.IffTrue, [(p, _)]) => (iff_true (thm_of p), cxp)
boehmes@40164
   764
    | (P.IffFalse, [(p, _)]) => (iff_false (thm_of p), cxp)
boehmes@40164
   765
    | (P.Distributivity, _) => (distributivity cx ct, cxp)
boehmes@40164
   766
    | (P.DefAxiom, _) => (def_axiom cx ct, cxp)
boehmes@40164
   767
    | (P.IntroDef, _) => intro_def ct cx ||> rpair ptab
boehmes@40164
   768
    | (P.ApplyDef, [(p, _)]) => (apply_def (thm_of p), cxp)
boehmes@40164
   769
    | (P.IffOeq, [(p, _)]) => (p, cxp)
boehmes@40164
   770
    | (P.NnfPos, _) => (nnf cx vars (map fst ps) ct, cxp)
boehmes@40164
   771
    | (P.NnfNeg, _) => (nnf cx vars (map fst ps) ct, cxp)
boehmes@36898
   772
boehmes@40164
   773
      (* equality rules *)
boehmes@40164
   774
    | (P.Reflexivity, _) => (refl ct, cxp)
boehmes@40164
   775
    | (P.Symmetry, [(p, _)]) => (symm p, cxp)
boehmes@40164
   776
    | (P.Transitivity, [(p, _), (q, _)]) => (trans p q, cxp)
boehmes@40164
   777
    | (P.Monotonicity, _) => (monotonicity (map fst ps) ct, cxp)
boehmes@40164
   778
    | (P.Commutativity, _) => (commutativity ct, cxp)
boehmes@40164
   779
boehmes@40164
   780
      (* quantifier rules *)
boehmes@40164
   781
    | (P.QuantIntro, [(p, _)]) => (quant_intro vars p ct, cxp)
boehmes@40164
   782
    | (P.PullQuant, _) => (pull_quant cx ct, cxp)
boehmes@40164
   783
    | (P.PushQuant, _) => (push_quant cx ct, cxp)
boehmes@40164
   784
    | (P.ElimUnusedVars, _) => (elim_unused_vars cx ct, cxp)
boehmes@40164
   785
    | (P.DestEqRes, _) => (dest_eq_res cx ct, cxp)
boehmes@40164
   786
    | (P.QuantInst, _) => (quant_inst ct, cxp)
boehmes@40164
   787
    | (P.Skolemize, _) => skolemize ct cx ||> rpair ptab
boehmes@40164
   788
boehmes@40164
   789
      (* theory rules *)
boehmes@40164
   790
    | (P.ThLemma, _) =>
boehmes@40164
   791
        (th_lemma cx simpset (map (thm_of o fst) ps) ct, cxp)
boehmes@40164
   792
    | (P.Rewrite, _) => (rewrite cx simpset [] ct, cxp)
boehmes@40164
   793
    | (P.RewriteStar, ps) =>
boehmes@40164
   794
        (rewrite cx simpset (map fst ps) ct, cxp)
boehmes@36898
   795
boehmes@40164
   796
    | (P.NnfStar, _) => not_supported r
boehmes@40164
   797
    | (P.CnfStar, _) => not_supported r
boehmes@40164
   798
    | (P.TransitivityStar, _) => not_supported r
boehmes@40164
   799
    | (P.PullQuantStar, _) => not_supported r
boehmes@36898
   800
boehmes@40164
   801
    | _ => raise Fail ("Z3: proof rule " ^ quote (P.string_of_rule r) ^
boehmes@40164
   802
       " has an unexpected number of arguments."))
boehmes@36898
   803
boehmes@40164
   804
  fun prove ctxt assms vars =
boehmes@40164
   805
    let
boehmes@40164
   806
      val simpset = T.make_simpset ctxt (Z3_Simps.get ctxt)
boehmes@40164
   807
 
boehmes@40164
   808
      fun conclude idx rule prop (ps, cxp) =
boehmes@40164
   809
        trace_rule idx (step assms simpset vars) rule ps prop cxp
boehmes@40164
   810
        |-> (fn p => apsnd (Inttab.update (idx, Proved p)) #> pair p)
boehmes@40164
   811
 
boehmes@40164
   812
      fun lookup idx (cxp as (_, ptab)) =
boehmes@40164
   813
        (case Inttab.lookup ptab idx of
boehmes@40164
   814
          SOME (Unproved (P.Proof_Step {rule, prems, prop})) =>
boehmes@40164
   815
            fold_map lookup prems cxp
boehmes@40164
   816
            |>> map2 rpair prems
boehmes@40164
   817
            |> conclude idx rule prop
boehmes@40164
   818
        | SOME (Proved p) => (p, cxp)
boehmes@40164
   819
        | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
boehmes@40164
   820
 
boehmes@40164
   821
      fun result (p, (cx, _)) = (thm_of p, cx)
boehmes@40164
   822
    in
boehmes@40164
   823
      (fn idx => result o lookup idx o pair ctxt o Inttab.map (K Unproved))
boehmes@40164
   824
    end
boehmes@36898
   825
boehmes@40164
   826
  fun filter_assms ctxt assms ptab =
boehmes@40164
   827
    let
boehmes@40164
   828
      fun step r ct =
boehmes@40164
   829
        (case r of
boehmes@40164
   830
          P.Asserted => insert (op =) (find_assm ctxt assms ct)
boehmes@40164
   831
        | P.Goal => insert (op =) (find_assm ctxt assms ct)
boehmes@40164
   832
        | _ => I)
boehmes@36898
   833
boehmes@40164
   834
      fun lookup idx =
boehmes@40164
   835
        (case Inttab.lookup ptab idx of
boehmes@40164
   836
          SOME (P.Proof_Step {rule, prems, prop}) =>
boehmes@40164
   837
            fold lookup prems #> step rule prop
boehmes@40164
   838
        | NONE => z3_exn ("unknown proof id: " ^ quote (string_of_int idx)))
boehmes@40164
   839
    in lookup end
boehmes@40164
   840
in
boehmes@40164
   841
boehmes@40164
   842
fun reconstruct ctxt {typs, terms, unfolds, assms} output =
boehmes@40164
   843
  let
boehmes@40164
   844
    val (idx, (ptab, vars, cx)) = P.parse ctxt typs terms output
boehmes@40164
   845
    val assms' = prepare_assms cx unfolds assms
boehmes@36898
   846
  in
boehmes@40424
   847
    if Config.get cx SMT_Config.filter_only_facts
boehmes@40164
   848
    then ((filter_assms cx assms' ptab idx [], @{thm TrueI}), cx)
boehmes@40164
   849
    else apfst (pair []) (prove cx assms' vars idx ptab)
boehmes@36898
   850
  end
boehmes@36898
   851
boehmes@40164
   852
end
boehmes@36898
   853
boehmes@40164
   854
val setup = z3_rules_setup #> Z3_Simps.setup
boehmes@36898
   855
boehmes@36898
   856
end