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