src/HOL/Tools/SMT/z3_replay_methods.ML
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 58956 a816aa3ff391
child 59381 de4218223e00
permissions -rw-r--r--
proper context for match_tac etc.;
blanchet@58061
     1
(*  Title:      HOL/Tools/SMT/z3_replay_methods.ML
blanchet@56078
     2
    Author:     Sascha Boehme, TU Muenchen
blanchet@56078
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@56078
     4
blanchet@56078
     5
Proof methods for replaying Z3 proofs.
blanchet@56078
     6
*)
blanchet@56078
     7
blanchet@58061
     8
signature Z3_REPLAY_METHODS =
blanchet@56078
     9
sig
blanchet@56078
    10
  (*abstraction*)
blanchet@56078
    11
  type abs_context = int * term Termtab.table
blanchet@56078
    12
  type 'a abstracter = term -> abs_context -> 'a * abs_context
blanchet@56078
    13
  val add_arith_abstracter: (term abstracter -> term option abstracter) ->
blanchet@56078
    14
    Context.generic -> Context.generic
blanchet@56078
    15
blanchet@56078
    16
  (*theory lemma methods*)
blanchet@56078
    17
  type th_lemma_method = Proof.context -> thm list -> term -> thm
blanchet@56078
    18
  val add_th_lemma_method: string * th_lemma_method -> Context.generic ->
blanchet@56078
    19
    Context.generic
blanchet@56078
    20
blanchet@56078
    21
  (*methods for Z3 proof rules*)
blanchet@56078
    22
  type z3_method = Proof.context -> thm list -> term -> thm
blanchet@56078
    23
  val true_axiom: z3_method
blanchet@56078
    24
  val mp: z3_method
blanchet@56078
    25
  val refl: z3_method
blanchet@56078
    26
  val symm: z3_method
blanchet@56078
    27
  val trans: z3_method
blanchet@56078
    28
  val cong: z3_method
blanchet@56078
    29
  val quant_intro: z3_method
blanchet@56078
    30
  val distrib: z3_method
blanchet@56078
    31
  val and_elim: z3_method
blanchet@56078
    32
  val not_or_elim: z3_method
blanchet@56078
    33
  val rewrite: z3_method
blanchet@56078
    34
  val rewrite_star: z3_method
blanchet@56078
    35
  val pull_quant: z3_method
blanchet@56078
    36
  val push_quant: z3_method
blanchet@56078
    37
  val elim_unused: z3_method
blanchet@56078
    38
  val dest_eq_res: z3_method
blanchet@56078
    39
  val quant_inst: z3_method
blanchet@56078
    40
  val lemma: z3_method
blanchet@56078
    41
  val unit_res: z3_method
blanchet@56078
    42
  val iff_true: z3_method
blanchet@56078
    43
  val iff_false: z3_method
blanchet@56078
    44
  val comm: z3_method
blanchet@56078
    45
  val def_axiom: z3_method
blanchet@56078
    46
  val apply_def: z3_method
blanchet@56078
    47
  val iff_oeq: z3_method
blanchet@56078
    48
  val nnf_pos: z3_method
blanchet@56078
    49
  val nnf_neg: z3_method
blanchet@56078
    50
  val mp_oeq: z3_method
blanchet@56078
    51
  val th_lemma: string -> z3_method
blanchet@58061
    52
  val method_for: Z3_Proof.z3_rule -> z3_method
blanchet@57229
    53
end;
blanchet@56078
    54
blanchet@58061
    55
structure Z3_Replay_Methods: Z3_REPLAY_METHODS =
blanchet@56078
    56
struct
blanchet@56078
    57
blanchet@56078
    58
type z3_method = Proof.context -> thm list -> term -> thm
blanchet@56078
    59
blanchet@56078
    60
blanchet@56078
    61
(* utility functions *)
blanchet@56078
    62
blanchet@58061
    63
fun trace ctxt f = SMT_Config.trace_msg ctxt f ()
blanchet@56078
    64
blanchet@56078
    65
fun pretty_thm ctxt thm = Syntax.pretty_term ctxt (Thm.concl_of thm)
blanchet@56078
    66
blanchet@56078
    67
fun pretty_goal ctxt msg rule thms t =
blanchet@56078
    68
  let
blanchet@58061
    69
    val full_msg = msg ^ ": " ^ quote (Z3_Proof.string_of_rule rule)
blanchet@56078
    70
    val assms =
blanchet@56078
    71
      if null thms then []
blanchet@56078
    72
      else [Pretty.big_list "assumptions:" (map (pretty_thm ctxt) thms)]
blanchet@56078
    73
    val concl = Pretty.big_list "proposition:" [Syntax.pretty_term ctxt t]
blanchet@56078
    74
  in Pretty.big_list full_msg (assms @ [concl]) end
blanchet@56078
    75
blanchet@56078
    76
fun replay_error ctxt msg rule thms t = error (Pretty.string_of (pretty_goal ctxt msg rule thms t))
blanchet@56078
    77
blanchet@56078
    78
fun replay_rule_error ctxt = replay_error ctxt "Failed to replay Z3 proof step"
blanchet@56078
    79
blanchet@56078
    80
fun trace_goal ctxt rule thms t =
blanchet@56078
    81
  trace ctxt (fn () => Pretty.string_of (pretty_goal ctxt "Goal" rule thms t))
blanchet@56078
    82
blanchet@56078
    83
fun as_prop (t as Const (@{const_name Trueprop}, _) $ _) = t
blanchet@56078
    84
  | as_prop t = HOLogic.mk_Trueprop t
blanchet@56078
    85
blanchet@56078
    86
fun dest_prop (Const (@{const_name Trueprop}, _) $ t) = t
blanchet@56078
    87
  | dest_prop t = t
blanchet@56078
    88
blanchet@56078
    89
fun dest_thm thm = dest_prop (Thm.concl_of thm)
blanchet@56078
    90
blanchet@58061
    91
fun certify_prop ctxt t = SMT_Util.certify ctxt (as_prop t)
blanchet@56078
    92
blanchet@56078
    93
fun try_provers ctxt rule [] thms t = replay_rule_error ctxt rule thms t
blanchet@56078
    94
  | try_provers ctxt rule ((name, prover) :: named_provers) thms t =
blanchet@56078
    95
      (case (trace ctxt (K ("Trying prover " ^ quote name)); try prover t) of
blanchet@56078
    96
        SOME thm => thm
blanchet@56078
    97
      | NONE => try_provers ctxt rule named_provers thms t)
blanchet@56078
    98
blanchet@56078
    99
fun match ctxt pat t =
blanchet@56078
   100
  (Vartab.empty, Vartab.empty)
blanchet@56078
   101
  |> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, t)
blanchet@56078
   102
blanchet@56078
   103
fun gen_certify_inst sel mk cert ctxt thm t =
blanchet@56078
   104
  let
blanchet@56078
   105
    val inst = match ctxt (dest_thm thm) (dest_prop t)
blanchet@56078
   106
    fun cert_inst (ix, (a, b)) = (cert (mk (ix, a)), cert b)
blanchet@56078
   107
  in Vartab.fold (cons o cert_inst) (sel inst) [] end
blanchet@56078
   108
blanchet@56078
   109
fun match_instantiateT ctxt t thm =
blanchet@56078
   110
  if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
blanchet@56078
   111
    let val certT = Thm.ctyp_of (Proof_Context.theory_of ctxt)
blanchet@56078
   112
    in Thm.instantiate (gen_certify_inst fst TVar certT ctxt thm t, []) thm end
blanchet@56078
   113
  else thm
blanchet@56078
   114
blanchet@56078
   115
fun match_instantiate ctxt t thm =
blanchet@56078
   116
  let
blanchet@58061
   117
    val cert = SMT_Util.certify ctxt
blanchet@56078
   118
    val thm' = match_instantiateT ctxt t thm
blanchet@56078
   119
  in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end
blanchet@56078
   120
blanchet@56078
   121
fun apply_rule ctxt t =
blanchet@58061
   122
  (case Z3_Replay_Rules.apply ctxt (certify_prop ctxt t) of
blanchet@56078
   123
    SOME thm => thm
blanchet@56078
   124
  | NONE => raise Fail "apply_rule")
blanchet@56078
   125
blanchet@56078
   126
fun discharge _ [] thm = thm
blanchet@56078
   127
  | discharge i (rule :: rules) thm = discharge (i + Thm.nprems_of rule) rules (rule RSN (i, thm))
blanchet@56078
   128
blanchet@56078
   129
fun by_tac ctxt thms ns ts t tac =
blanchet@56078
   130
  Goal.prove ctxt [] (map as_prop ts) (as_prop t)
blanchet@56078
   131
    (fn {context, prems} => HEADGOAL (tac context prems))
blanchet@56078
   132
  |> Drule.generalize ([], ns)
blanchet@56078
   133
  |> discharge 1 thms
blanchet@56078
   134
blanchet@56078
   135
fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac)
blanchet@56078
   136
blanchet@56078
   137
fun prop_tac ctxt prems =
boehmes@56816
   138
  Method.insert_tac prems
boehmes@56816
   139
  THEN' SUBGOAL (fn (prop, i) =>
boehmes@56816
   140
    if Term.size_of_term prop > 100 then SAT.satx_tac ctxt i
boehmes@56816
   141
    else (Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt) i)
blanchet@56078
   142
blanchet@56078
   143
fun quant_tac ctxt = Blast.blast_tac ctxt
blanchet@56078
   144
blanchet@56078
   145
blanchet@56078
   146
(* plug-ins *)
blanchet@56078
   147
blanchet@56078
   148
type abs_context = int * term Termtab.table
blanchet@56078
   149
blanchet@56078
   150
type 'a abstracter = term -> abs_context -> 'a * abs_context
blanchet@56078
   151
blanchet@56078
   152
type th_lemma_method = Proof.context -> thm list -> term -> thm
blanchet@56078
   153
blanchet@56078
   154
fun id_ord ((id1, _), (id2, _)) = int_ord (id1, id2)
blanchet@56078
   155
blanchet@56078
   156
structure Plugins = Generic_Data
blanchet@56078
   157
(
blanchet@56078
   158
  type T =
blanchet@56078
   159
    (int * (term abstracter -> term option abstracter)) list *
blanchet@56078
   160
    th_lemma_method Symtab.table
blanchet@56078
   161
  val empty = ([], Symtab.empty)
blanchet@56078
   162
  val extend = I
blanchet@56078
   163
  fun merge ((abss1, ths1), (abss2, ths2)) = (
blanchet@56078
   164
    Ord_List.merge id_ord (abss1, abss2),
blanchet@56078
   165
    Symtab.merge (K true) (ths1, ths2))
blanchet@56078
   166
)
blanchet@56078
   167
blanchet@56078
   168
fun add_arith_abstracter abs = Plugins.map (apfst (Ord_List.insert id_ord (serial (), abs)))
blanchet@56078
   169
fun get_arith_abstracters ctxt = map snd (fst (Plugins.get (Context.Proof ctxt)))
blanchet@56078
   170
blanchet@56078
   171
fun add_th_lemma_method method = Plugins.map (apsnd (Symtab.update_new method))
blanchet@56078
   172
fun get_th_lemma_method ctxt = snd (Plugins.get (Context.Proof ctxt))
blanchet@56078
   173
blanchet@56078
   174
blanchet@56078
   175
(* abstraction *)
blanchet@56078
   176
blanchet@56078
   177
fun prove_abstract ctxt thms t tac f =
blanchet@56078
   178
  let
blanchet@56078
   179
    val ((prems, concl), (_, ts)) = f (1, Termtab.empty)
blanchet@56078
   180
    val ns = Termtab.fold (fn (_, v) => cons (fst (Term.dest_Free v))) ts []
blanchet@56078
   181
  in
blanchet@56078
   182
    by_tac ctxt [] ns prems concl tac
blanchet@56078
   183
    |> match_instantiate ctxt t
blanchet@56078
   184
    |> discharge 1 thms
blanchet@56078
   185
  end
blanchet@56078
   186
blanchet@56078
   187
fun prove_abstract' ctxt t tac f =
blanchet@56078
   188
  prove_abstract ctxt [] t tac (f #>> pair [])
blanchet@56078
   189
blanchet@56078
   190
fun lookup_term (_, terms) t = Termtab.lookup terms t
blanchet@56078
   191
blanchet@56078
   192
fun abstract_sub t f cx =
blanchet@56078
   193
  (case lookup_term cx t of
blanchet@56078
   194
    SOME v => (v, cx)
blanchet@56078
   195
  | NONE => f cx)
blanchet@56078
   196
blanchet@56078
   197
fun mk_fresh_free t (i, terms) =
blanchet@56078
   198
  let val v = Free ("t" ^ string_of_int i, fastype_of t)
blanchet@56078
   199
  in (v, (i + 1, Termtab.update (t, v) terms)) end
blanchet@56078
   200
blanchet@56078
   201
fun apply_abstracters _ [] _ cx = (NONE, cx)
blanchet@56078
   202
  | apply_abstracters abs (abstracter :: abstracters) t cx =
blanchet@56078
   203
      (case abstracter abs t cx of
blanchet@56078
   204
        (NONE, _) => apply_abstracters abs abstracters t cx
blanchet@56078
   205
      | x as (SOME _, _) => x)
blanchet@56078
   206
blanchet@56078
   207
fun abstract_term (t as _ $ _) = abstract_sub t (mk_fresh_free t)
blanchet@56078
   208
  | abstract_term (t as Abs _) = abstract_sub t (mk_fresh_free t)
blanchet@56078
   209
  | abstract_term t = pair t
blanchet@56078
   210
blanchet@56078
   211
fun abstract_bin abs f t t1 t2 = abstract_sub t (abs t1 ##>> abs t2 #>> f)
blanchet@56078
   212
blanchet@56078
   213
fun abstract_ter abs f t t1 t2 t3 =
blanchet@56078
   214
  abstract_sub t (abs t1 ##>> abs t2 ##>> abs t3 #>> (Parse.triple1 #> f))
blanchet@56078
   215
blanchet@56078
   216
fun abstract_lit (@{const HOL.Not} $ t) = abstract_term t #>> HOLogic.mk_not
blanchet@56078
   217
  | abstract_lit t = abstract_term t
blanchet@56078
   218
blanchet@56078
   219
fun abstract_not abs (t as @{const HOL.Not} $ t1) =
blanchet@56078
   220
      abstract_sub t (abs t1 #>> HOLogic.mk_not)
blanchet@56078
   221
  | abstract_not _ t = abstract_lit t
blanchet@56078
   222
blanchet@56078
   223
fun abstract_conj (t as @{const HOL.conj} $ t1 $ t2) =
blanchet@56078
   224
      abstract_bin abstract_conj HOLogic.mk_conj t t1 t2
blanchet@56078
   225
  | abstract_conj t = abstract_lit t
blanchet@56078
   226
blanchet@56078
   227
fun abstract_disj (t as @{const HOL.disj} $ t1 $ t2) =
blanchet@56078
   228
      abstract_bin abstract_disj HOLogic.mk_disj t t1 t2
blanchet@56078
   229
  | abstract_disj t = abstract_lit t
blanchet@56078
   230
blanchet@56078
   231
fun abstract_prop (t as (c as @{const If (bool)}) $ t1 $ t2 $ t3) =
blanchet@56078
   232
      abstract_ter abstract_prop (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
blanchet@56078
   233
  | abstract_prop (t as @{const HOL.disj} $ t1 $ t2) =
blanchet@56078
   234
      abstract_bin abstract_prop HOLogic.mk_disj t t1 t2
blanchet@56078
   235
  | abstract_prop (t as @{const HOL.conj} $ t1 $ t2) =
blanchet@56078
   236
      abstract_bin abstract_prop HOLogic.mk_conj t t1 t2
blanchet@56078
   237
  | abstract_prop (t as @{const HOL.implies} $ t1 $ t2) =
blanchet@56078
   238
      abstract_bin abstract_prop HOLogic.mk_imp t t1 t2
blanchet@56078
   239
  | abstract_prop (t as @{term "HOL.eq :: bool => _"} $ t1 $ t2) =
blanchet@56078
   240
      abstract_bin abstract_prop HOLogic.mk_eq t t1 t2
blanchet@56078
   241
  | abstract_prop t = abstract_not abstract_prop t
blanchet@56078
   242
blanchet@56078
   243
fun abstract_arith ctxt u =
blanchet@56078
   244
  let
blanchet@56078
   245
    fun abs (t as (c as Const _) $ Abs (s, T, t')) =
blanchet@56078
   246
          abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u')))
blanchet@56078
   247
      | abs (t as (c as Const (@{const_name If}, _)) $ t1 $ t2 $ t3) =
blanchet@56078
   248
          abstract_ter abs (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3
blanchet@56078
   249
      | abs (t as @{const HOL.Not} $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not)
blanchet@56078
   250
      | abs (t as @{const HOL.disj} $ t1 $ t2) =
blanchet@56078
   251
          abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj)
blanchet@56078
   252
      | abs (t as (c as Const (@{const_name uminus_class.uminus}, _)) $ t1) =
blanchet@56078
   253
          abstract_sub t (abs t1 #>> (fn u => c $ u))
blanchet@56078
   254
      | abs (t as (c as Const (@{const_name plus_class.plus}, _)) $ t1 $ t2) =
blanchet@56078
   255
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
blanchet@56078
   256
      | abs (t as (c as Const (@{const_name minus_class.minus}, _)) $ t1 $ t2) =
blanchet@56078
   257
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
blanchet@56078
   258
      | abs (t as (c as Const (@{const_name times_class.times}, _)) $ t1 $ t2) =
blanchet@56078
   259
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
blanchet@56078
   260
      | abs (t as (c as Const (@{const_name z3div}, _)) $ t1 $ t2) =
blanchet@56078
   261
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
blanchet@56078
   262
      | abs (t as (c as Const (@{const_name z3mod}, _)) $ t1 $ t2) =
blanchet@56078
   263
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
blanchet@56078
   264
      | abs (t as (c as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
blanchet@56078
   265
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
blanchet@56078
   266
      | abs (t as (c as Const (@{const_name ord_class.less}, _)) $ t1 $ t2) =
blanchet@56078
   267
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
blanchet@56078
   268
      | abs (t as (c as Const (@{const_name ord_class.less_eq}, _)) $ t1 $ t2) =
blanchet@56078
   269
          abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2))
blanchet@56078
   270
      | abs t = abstract_sub t (fn cx =>
blanchet@56078
   271
          if can HOLogic.dest_number t then (t, cx)
blanchet@56078
   272
          else
blanchet@56078
   273
            (case apply_abstracters abs (get_arith_abstracters ctxt) t cx of
blanchet@56078
   274
              (SOME u, cx') => (u, cx')
blanchet@56078
   275
            | (NONE, _) => abstract_term t cx))
blanchet@56078
   276
  in abs u end
blanchet@56078
   277
blanchet@56078
   278
blanchet@56078
   279
(* truth axiom *)
blanchet@56078
   280
blanchet@56078
   281
fun true_axiom _ _ _ = @{thm TrueI}
blanchet@56078
   282
blanchet@56078
   283
blanchet@56078
   284
(* modus ponens *)
blanchet@56078
   285
blanchet@56078
   286
fun mp _ [p, p_eq_q] _ = discharge 1 [p_eq_q, p] iffD1
blanchet@58061
   287
  | mp ctxt thms t = replay_rule_error ctxt Z3_Proof.Modus_Ponens thms t
blanchet@56078
   288
blanchet@56078
   289
val mp_oeq = mp
blanchet@56078
   290
blanchet@56078
   291
blanchet@56078
   292
(* reflexivity *)
blanchet@56078
   293
blanchet@56078
   294
fun refl ctxt _ t = match_instantiate ctxt t @{thm refl}
blanchet@56078
   295
blanchet@56078
   296
blanchet@56078
   297
(* symmetry *)
blanchet@56078
   298
blanchet@56078
   299
fun symm _ [thm] _ = thm RS @{thm sym}
blanchet@58061
   300
  | symm ctxt thms t = replay_rule_error ctxt Z3_Proof.Reflexivity thms t
blanchet@56078
   301
blanchet@56078
   302
blanchet@56078
   303
(* transitivity *)
blanchet@56078
   304
blanchet@56078
   305
fun trans _ [thm1, thm2] _ = thm1 RSN (1, thm2 RSN (2, @{thm trans}))
blanchet@58061
   306
  | trans ctxt thms t = replay_rule_error ctxt Z3_Proof.Transitivity thms t
blanchet@56078
   307
blanchet@56078
   308
blanchet@56078
   309
(* congruence *)
blanchet@56078
   310
wenzelm@58956
   311
fun ctac ctxt prems i st = st |> (
blanchet@56078
   312
  resolve_tac (@{thm refl} :: prems) i
wenzelm@58956
   313
  ORELSE (cong_tac ctxt i THEN ctac ctxt prems (i + 1) THEN ctac ctxt prems i))
blanchet@56078
   314
blanchet@56078
   315
fun cong_basic ctxt thms t =
blanchet@56078
   316
  let val st = Thm.trivial (certify_prop ctxt t)
blanchet@56078
   317
  in
wenzelm@58956
   318
    (case Seq.pull (ctac ctxt thms 1 st) of
blanchet@56078
   319
      SOME (thm, _) => thm
blanchet@56078
   320
    | NONE => raise THM ("cong", 0, thms @ [st]))
blanchet@56078
   321
  end
blanchet@56078
   322
blanchet@56078
   323
val cong_dest_rules = @{lemma
blanchet@56078
   324
  "(~ P | Q) & (P | ~ Q) ==> P = Q"
blanchet@56078
   325
  "(P | ~ Q) & (~ P | Q) ==> P = Q"
blanchet@56078
   326
  by fast+}
blanchet@56078
   327
blanchet@56078
   328
fun cong_full ctxt thms t = prove ctxt t (fn ctxt' =>
blanchet@56078
   329
  Method.insert_tac thms
blanchet@56078
   330
  THEN' (Classical.fast_tac ctxt'
blanchet@56078
   331
    ORELSE' dresolve_tac cong_dest_rules
blanchet@56078
   332
    THEN' Classical.fast_tac ctxt'))
blanchet@56078
   333
blanchet@58061
   334
fun cong ctxt thms = try_provers ctxt Z3_Proof.Monotonicity [
blanchet@56078
   335
  ("basic", cong_basic ctxt thms),
blanchet@56078
   336
  ("full", cong_full ctxt thms)] thms
blanchet@56078
   337
blanchet@56078
   338
blanchet@56078
   339
(* quantifier introduction *)
blanchet@56078
   340
blanchet@56078
   341
val quant_intro_rules = @{lemma
blanchet@56078
   342
  "(!!x. P x = Q x) ==> (ALL x. P x) = (ALL x. Q x)"
blanchet@56078
   343
  "(!!x. P x = Q x) ==> (EX x. P x) = (EX x. Q x)"
blanchet@56078
   344
  "(!!x. (~ P x) = Q x) ==> (~ (EX x. P x)) = (ALL x. Q x)"
blanchet@56078
   345
  "(!!x. (~ P x) = Q x) ==> (~ (ALL x. P x)) = (EX x. Q x)"
blanchet@56078
   346
  by fast+}
blanchet@56078
   347
blanchet@56078
   348
fun quant_intro ctxt [thm] t =
blanchet@56078
   349
    prove ctxt t (K (REPEAT_ALL_NEW (resolve_tac (thm :: quant_intro_rules))))
blanchet@58061
   350
  | quant_intro ctxt thms t = replay_rule_error ctxt Z3_Proof.Quant_Intro thms t
blanchet@56078
   351
blanchet@56078
   352
blanchet@56078
   353
(* distributivity of conjunctions and disjunctions *)
blanchet@56078
   354
blanchet@56078
   355
(* TODO: there are no tests with this proof rule *)
blanchet@56078
   356
fun distrib ctxt _ t =
blanchet@56078
   357
  prove_abstract' ctxt t prop_tac (abstract_prop (dest_prop t))
blanchet@56078
   358
blanchet@56078
   359
blanchet@56078
   360
(* elimination of conjunctions *)
blanchet@56078
   361
blanchet@56078
   362
fun and_elim ctxt [thm] t =
blanchet@56078
   363
      prove_abstract ctxt [thm] t prop_tac (
blanchet@56078
   364
        abstract_lit (dest_prop t) ##>>
blanchet@56078
   365
        abstract_conj (dest_thm thm) #>>
blanchet@56078
   366
        apfst single o swap)
blanchet@58061
   367
  | and_elim ctxt thms t = replay_rule_error ctxt Z3_Proof.And_Elim thms t
blanchet@56078
   368
blanchet@56078
   369
blanchet@56078
   370
(* elimination of negated disjunctions *)
blanchet@56078
   371
blanchet@56078
   372
fun not_or_elim ctxt [thm] t =
blanchet@56078
   373
      prove_abstract ctxt [thm] t prop_tac (
blanchet@56078
   374
        abstract_lit (dest_prop t) ##>>
blanchet@56078
   375
        abstract_not abstract_disj (dest_thm thm) #>>
blanchet@56078
   376
        apfst single o swap)
blanchet@56078
   377
  | not_or_elim ctxt thms t =
blanchet@58061
   378
      replay_rule_error ctxt Z3_Proof.Not_Or_Elim thms t
blanchet@56078
   379
blanchet@56078
   380
blanchet@56078
   381
(* rewriting *)
blanchet@56078
   382
boehmes@57144
   383
local
boehmes@57144
   384
boehmes@57144
   385
fun dest_all (Const (@{const_name HOL.All}, _) $ Abs (_, T, t)) nctxt =
boehmes@57144
   386
      let
boehmes@57144
   387
        val (n, nctxt') = Name.variant "" nctxt
boehmes@57144
   388
        val f = Free (n, T)
boehmes@57144
   389
        val t' = Term.subst_bound (f, t)
boehmes@57144
   390
      in dest_all t' nctxt' |>> cons f end
boehmes@57144
   391
  | dest_all t _ = ([], t)
boehmes@57144
   392
boehmes@57144
   393
fun dest_alls t =
boehmes@57144
   394
  let
boehmes@57144
   395
    val nctxt = Name.make_context (Term.add_free_names t [])
boehmes@57144
   396
    val (lhs, rhs) = HOLogic.dest_eq (dest_prop t)
boehmes@57144
   397
    val (ls, lhs') = dest_all lhs nctxt
boehmes@57144
   398
    val (rs, rhs') = dest_all rhs nctxt
boehmes@57144
   399
  in
boehmes@57144
   400
    if eq_list (op aconv) (ls, rs) then SOME (ls, (HOLogic.mk_eq (lhs', rhs')))
boehmes@57144
   401
    else NONE
boehmes@57144
   402
  end
boehmes@57144
   403
boehmes@57144
   404
fun forall_intr ctxt t thm =
boehmes@57144
   405
  let val ct = Thm.cterm_of (Proof_Context.theory_of ctxt) t
boehmes@57144
   406
  in Thm.forall_intr ct thm COMP_INCR @{thm iff_allI} end
boehmes@57144
   407
boehmes@57144
   408
in
boehmes@57144
   409
boehmes@57144
   410
fun focus_eq f ctxt t =
boehmes@57144
   411
  (case dest_alls t of
boehmes@57144
   412
    NONE => f ctxt t
boehmes@57144
   413
  | SOME (vs, t') => fold (forall_intr ctxt) vs (f ctxt t'))
boehmes@57144
   414
boehmes@57144
   415
end
boehmes@57144
   416
boehmes@57144
   417
fun abstract_eq f (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
boehmes@57144
   418
      f t1 ##>> f t2 #>> HOLogic.mk_eq
boehmes@57144
   419
  | abstract_eq _ t = abstract_term t
blanchet@56078
   420
blanchet@56078
   421
fun prove_prop_rewrite ctxt t =
blanchet@56078
   422
  prove_abstract' ctxt t prop_tac (
boehmes@57145
   423
    abstract_eq abstract_prop (dest_prop t))
blanchet@56078
   424
blanchet@56078
   425
fun arith_rewrite_tac ctxt _ =
blanchet@56078
   426
  TRY o Simplifier.simp_tac ctxt
blanchet@56078
   427
  THEN_ALL_NEW (Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt)
blanchet@56078
   428
blanchet@56078
   429
fun prove_arith_rewrite ctxt t =
blanchet@56078
   430
  prove_abstract' ctxt t arith_rewrite_tac (
boehmes@57144
   431
    abstract_eq (abstract_arith ctxt) (dest_prop t))
blanchet@56078
   432
boehmes@58140
   433
val lift_ite_thm = @{thm HOL.if_distrib} RS @{thm eq_reflection}
boehmes@58140
   434
boehmes@58140
   435
fun ternary_conv cv = Conv.combination_conv (Conv.binop_conv cv) cv
boehmes@58140
   436
boehmes@58140
   437
fun if_context_conv ctxt ct =
boehmes@58140
   438
  (case Thm.term_of ct of
boehmes@58140
   439
    Const (@{const_name HOL.If}, _) $ _ $ _ $ _ =>
boehmes@58140
   440
      ternary_conv (if_context_conv ctxt)
boehmes@58140
   441
  | _ $ (Const (@{const_name HOL.If}, _) $ _ $ _ $ _) =>
boehmes@58140
   442
      Conv.rewr_conv lift_ite_thm then_conv ternary_conv (if_context_conv ctxt)
boehmes@58140
   443
  | _ => Conv.sub_conv (Conv.top_sweep_conv if_context_conv) ctxt) ct
boehmes@58140
   444
boehmes@58140
   445
fun lift_ite_rewrite ctxt t =
boehmes@58140
   446
  prove ctxt t (fn ctxt => 
boehmes@58140
   447
    CONVERSION (HOLogic.Trueprop_conv (Conv.binop_conv (if_context_conv ctxt)))
boehmes@58140
   448
    THEN' rtac @{thm refl})
boehmes@58140
   449
blanchet@58061
   450
fun rewrite ctxt _ = try_provers ctxt Z3_Proof.Rewrite [
blanchet@56078
   451
  ("rules", apply_rule ctxt),
blanchet@56078
   452
  ("prop_rewrite", prove_prop_rewrite ctxt),
boehmes@58140
   453
  ("arith_rewrite", focus_eq prove_arith_rewrite ctxt),
boehmes@58140
   454
  ("if_rewrite", lift_ite_rewrite ctxt)] []
blanchet@56078
   455
blanchet@56078
   456
fun rewrite_star ctxt = rewrite ctxt
blanchet@56078
   457
blanchet@56078
   458
blanchet@56078
   459
(* pulling quantifiers *)
blanchet@56078
   460
blanchet@56078
   461
fun pull_quant ctxt _ t = prove ctxt t quant_tac
blanchet@56078
   462
blanchet@56078
   463
blanchet@56078
   464
(* pushing quantifiers *)
blanchet@56078
   465
blanchet@56078
   466
fun push_quant _ _ _ = raise Fail "unsupported" (* FIXME *)
blanchet@56078
   467
blanchet@56078
   468
blanchet@56078
   469
(* elimination of unused bound variables *)
blanchet@56078
   470
blanchet@56078
   471
val elim_all = @{lemma "P = Q ==> (ALL x. P) = Q" by fast}
blanchet@56078
   472
val elim_ex = @{lemma "P = Q ==> (EX x. P) = Q" by fast}
blanchet@56078
   473
wenzelm@58957
   474
fun elim_unused_tac ctxt i st = (
wenzelm@58957
   475
  match_tac ctxt [@{thm refl}]
wenzelm@58957
   476
  ORELSE' (match_tac ctxt [elim_all, elim_ex] THEN' elim_unused_tac ctxt)
blanchet@56078
   477
  ORELSE' (
wenzelm@58957
   478
    match_tac ctxt [@{thm iff_allI}, @{thm iff_exI}]
wenzelm@58957
   479
    THEN' elim_unused_tac ctxt)) i st
blanchet@56078
   480
wenzelm@58957
   481
fun elim_unused ctxt _ t = prove ctxt t elim_unused_tac
blanchet@56078
   482
blanchet@56078
   483
blanchet@56078
   484
(* destructive equality resolution *)
blanchet@56078
   485
blanchet@56078
   486
fun dest_eq_res _ _ _ = raise Fail "dest_eq_res" (* FIXME *)
blanchet@56078
   487
blanchet@56078
   488
blanchet@56078
   489
(* quantifier instantiation *)
blanchet@56078
   490
blanchet@56078
   491
val quant_inst_rule = @{lemma "~P x | Q ==> ~(ALL x. P x) | Q" by fast}
blanchet@56078
   492
blanchet@57230
   493
fun quant_inst ctxt _ t = prove ctxt t (fn _ =>
blanchet@56078
   494
  REPEAT_ALL_NEW (rtac quant_inst_rule)
blanchet@56078
   495
  THEN' rtac @{thm excluded_middle})
blanchet@56078
   496
blanchet@56078
   497
blanchet@56078
   498
(* propositional lemma *)
blanchet@56078
   499
blanchet@56078
   500
exception LEMMA of unit
blanchet@56078
   501
blanchet@56078
   502
val intro_hyp_rule1 = @{lemma "(~P ==> Q) ==> P | Q" by fast}
blanchet@56078
   503
val intro_hyp_rule2 = @{lemma "(P ==> Q) ==> ~P | Q" by fast}
blanchet@56078
   504
blanchet@56078
   505
fun norm_lemma thm =
blanchet@56078
   506
  (thm COMP_INCR intro_hyp_rule1)
blanchet@56078
   507
  handle THM _ => thm COMP_INCR intro_hyp_rule2
blanchet@56078
   508
blanchet@56078
   509
fun negated_prop (@{const HOL.Not} $ t) = HOLogic.mk_Trueprop t
blanchet@56078
   510
  | negated_prop t = HOLogic.mk_Trueprop (HOLogic.mk_not t)
blanchet@56078
   511
blanchet@56078
   512
fun intro_hyps tab (t as @{const HOL.disj} $ t1 $ t2) cx =
blanchet@56078
   513
      lookup_intro_hyps tab t (fold (intro_hyps tab) [t1, t2]) cx
blanchet@56078
   514
  | intro_hyps tab t cx =
blanchet@56078
   515
      lookup_intro_hyps tab t (fn _ => raise LEMMA ()) cx
blanchet@56078
   516
blanchet@56078
   517
and lookup_intro_hyps tab t f (cx as (thm, terms)) =
blanchet@56078
   518
  (case Termtab.lookup tab (negated_prop t) of
blanchet@56078
   519
    NONE => f cx
blanchet@56078
   520
  | SOME hyp => (norm_lemma (Thm.implies_intr hyp thm), t :: terms))
blanchet@56078
   521
blanchet@56078
   522
fun lemma ctxt (thms as [thm]) t =
blanchet@56078
   523
    (let
blanchet@56078
   524
       val tab = Termtab.make (map (`Thm.term_of) (#hyps (Thm.crep_thm thm)))
blanchet@56078
   525
       val (thm', terms) = intro_hyps tab (dest_prop t) (thm, [])
blanchet@56078
   526
     in
blanchet@56078
   527
       prove_abstract ctxt [thm'] t prop_tac (
blanchet@56078
   528
         fold (snd oo abstract_lit) terms #>
blanchet@56078
   529
         abstract_disj (dest_thm thm') #>> single ##>>
blanchet@56078
   530
         abstract_disj (dest_prop t))
blanchet@56078
   531
     end
blanchet@58061
   532
     handle LEMMA () => replay_error ctxt "Bad proof state" Z3_Proof.Lemma thms t)
blanchet@58061
   533
  | lemma ctxt thms t = replay_rule_error ctxt Z3_Proof.Lemma thms t
blanchet@56078
   534
blanchet@56078
   535
blanchet@56078
   536
(* unit resolution *)
blanchet@56078
   537
blanchet@56078
   538
fun abstract_unit (t as (@{const HOL.Not} $ (@{const HOL.disj} $ t1 $ t2))) =
blanchet@56078
   539
      abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
blanchet@56078
   540
        HOLogic.mk_not o HOLogic.mk_disj)
blanchet@56078
   541
  | abstract_unit (t as (@{const HOL.disj} $ t1 $ t2)) =
blanchet@56078
   542
      abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>>
blanchet@56078
   543
        HOLogic.mk_disj)
blanchet@56078
   544
  | abstract_unit t = abstract_lit t
blanchet@56078
   545
blanchet@56078
   546
fun unit_res ctxt thms t =
blanchet@56078
   547
  prove_abstract ctxt thms t prop_tac (
blanchet@56078
   548
    fold_map (abstract_unit o dest_thm) thms ##>>
blanchet@56078
   549
    abstract_unit (dest_prop t) #>>
blanchet@56078
   550
    (fn (prems, concl) => (prems, concl)))
blanchet@56078
   551
blanchet@56078
   552
blanchet@56078
   553
(* iff-true *)
blanchet@56078
   554
blanchet@56078
   555
val iff_true_rule = @{lemma "P ==> P = True" by fast}
blanchet@56078
   556
blanchet@56078
   557
fun iff_true _ [thm] _ = thm RS iff_true_rule
blanchet@58061
   558
  | iff_true ctxt thms t = replay_rule_error ctxt Z3_Proof.Iff_True thms t
blanchet@56078
   559
blanchet@56078
   560
blanchet@56078
   561
(* iff-false *)
blanchet@56078
   562
blanchet@56078
   563
val iff_false_rule = @{lemma "~P ==> P = False" by fast}
blanchet@56078
   564
blanchet@56078
   565
fun iff_false _ [thm] _ = thm RS iff_false_rule
blanchet@58061
   566
  | iff_false ctxt thms t = replay_rule_error ctxt Z3_Proof.Iff_False thms t
blanchet@56078
   567
blanchet@56078
   568
blanchet@56078
   569
(* commutativity *)
blanchet@56078
   570
blanchet@56078
   571
fun comm ctxt _ t = match_instantiate ctxt t @{thm eq_commute}
blanchet@56078
   572
blanchet@56078
   573
blanchet@56078
   574
(* definitional axioms *)
blanchet@56078
   575
blanchet@56078
   576
fun def_axiom_disj ctxt t =
blanchet@56078
   577
  (case dest_prop t of
blanchet@56078
   578
    @{const HOL.disj} $ u1 $ u2 =>
blanchet@56078
   579
      prove_abstract' ctxt t prop_tac (
blanchet@56078
   580
        abstract_prop u2 ##>> abstract_prop u1 #>> HOLogic.mk_disj o swap)
blanchet@56078
   581
  | u => prove_abstract' ctxt t prop_tac (abstract_prop u))
blanchet@56078
   582
blanchet@58061
   583
fun def_axiom ctxt _ = try_provers ctxt Z3_Proof.Def_Axiom [
blanchet@56078
   584
  ("rules", apply_rule ctxt),
blanchet@56078
   585
  ("disj", def_axiom_disj ctxt)] []
blanchet@56078
   586
blanchet@56078
   587
blanchet@56078
   588
(* application of definitions *)
blanchet@56078
   589
blanchet@56078
   590
fun apply_def _ [thm] _ = thm (* TODO: cover also the missing cases *)
blanchet@58061
   591
  | apply_def ctxt thms t = replay_rule_error ctxt Z3_Proof.Apply_Def thms t
blanchet@56078
   592
blanchet@56078
   593
blanchet@56078
   594
(* iff-oeq *)
blanchet@56078
   595
blanchet@56078
   596
fun iff_oeq _ _ _ = raise Fail "iff_oeq" (* FIXME *)
blanchet@56078
   597
blanchet@56078
   598
blanchet@56078
   599
(* negation normal form *)
blanchet@56078
   600
blanchet@56078
   601
fun nnf_prop ctxt thms t =
blanchet@56078
   602
  prove_abstract ctxt thms t prop_tac (
blanchet@56078
   603
    fold_map (abstract_prop o dest_thm) thms ##>>
blanchet@56078
   604
    abstract_prop (dest_prop t))
blanchet@56078
   605
blanchet@56078
   606
fun nnf ctxt rule thms = try_provers ctxt rule [
blanchet@56078
   607
  ("prop", nnf_prop ctxt thms),
blanchet@56078
   608
  ("quant", quant_intro ctxt [hd thms])] thms
blanchet@56078
   609
blanchet@58061
   610
fun nnf_pos ctxt = nnf ctxt Z3_Proof.Nnf_Pos
blanchet@58061
   611
fun nnf_neg ctxt = nnf ctxt Z3_Proof.Nnf_Neg
blanchet@56078
   612
blanchet@56078
   613
blanchet@56078
   614
(* theory lemmas *)
blanchet@56078
   615
blanchet@56078
   616
fun arith_th_lemma_tac ctxt prems =
blanchet@56078
   617
  Method.insert_tac prems
blanchet@56078
   618
  THEN' SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms z3div_def z3mod_def})
blanchet@56078
   619
  THEN' Arith_Data.arith_tac ctxt
blanchet@56078
   620
blanchet@56078
   621
fun arith_th_lemma ctxt thms t =
blanchet@56078
   622
  prove_abstract ctxt thms t arith_th_lemma_tac (
blanchet@56078
   623
    fold_map (abstract_arith ctxt o dest_thm) thms ##>>
blanchet@56078
   624
    abstract_arith ctxt (dest_prop t))
blanchet@56078
   625
blanchet@56078
   626
val _ = Theory.setup (Context.theory_map (add_th_lemma_method ("arith", arith_th_lemma)))
blanchet@56078
   627
blanchet@56078
   628
fun th_lemma name ctxt thms =
blanchet@56078
   629
  (case Symtab.lookup (get_th_lemma_method ctxt) name of
blanchet@56078
   630
    SOME method => method ctxt thms
blanchet@58061
   631
  | NONE => replay_error ctxt "Bad theory" (Z3_Proof.Th_Lemma name) thms)
blanchet@56078
   632
blanchet@56078
   633
blanchet@56078
   634
(* mapping of rules to methods *)
blanchet@56078
   635
blanchet@56078
   636
fun unsupported rule ctxt = replay_error ctxt "Unsupported" rule
blanchet@56078
   637
fun assumed rule ctxt = replay_error ctxt "Assumed" rule
blanchet@56078
   638
blanchet@58061
   639
fun choose Z3_Proof.True_Axiom = true_axiom
blanchet@58061
   640
  | choose (r as Z3_Proof.Asserted) = assumed r
blanchet@58061
   641
  | choose (r as Z3_Proof.Goal) = assumed r
blanchet@58061
   642
  | choose Z3_Proof.Modus_Ponens = mp
blanchet@58061
   643
  | choose Z3_Proof.Reflexivity = refl
blanchet@58061
   644
  | choose Z3_Proof.Symmetry = symm
blanchet@58061
   645
  | choose Z3_Proof.Transitivity = trans
blanchet@58061
   646
  | choose (r as Z3_Proof.Transitivity_Star) = unsupported r
blanchet@58061
   647
  | choose Z3_Proof.Monotonicity = cong
blanchet@58061
   648
  | choose Z3_Proof.Quant_Intro = quant_intro
blanchet@58061
   649
  | choose Z3_Proof.Distributivity = distrib
blanchet@58061
   650
  | choose Z3_Proof.And_Elim = and_elim
blanchet@58061
   651
  | choose Z3_Proof.Not_Or_Elim = not_or_elim
blanchet@58061
   652
  | choose Z3_Proof.Rewrite = rewrite
blanchet@58061
   653
  | choose Z3_Proof.Rewrite_Star = rewrite_star
blanchet@58061
   654
  | choose Z3_Proof.Pull_Quant = pull_quant
blanchet@58061
   655
  | choose (r as Z3_Proof.Pull_Quant_Star) = unsupported r
blanchet@58061
   656
  | choose Z3_Proof.Push_Quant = push_quant
blanchet@58061
   657
  | choose Z3_Proof.Elim_Unused_Vars = elim_unused
blanchet@58061
   658
  | choose Z3_Proof.Dest_Eq_Res = dest_eq_res
blanchet@58061
   659
  | choose Z3_Proof.Quant_Inst = quant_inst
blanchet@58061
   660
  | choose (r as Z3_Proof.Hypothesis) = assumed r
blanchet@58061
   661
  | choose Z3_Proof.Lemma = lemma
blanchet@58061
   662
  | choose Z3_Proof.Unit_Resolution = unit_res
blanchet@58061
   663
  | choose Z3_Proof.Iff_True = iff_true
blanchet@58061
   664
  | choose Z3_Proof.Iff_False = iff_false
blanchet@58061
   665
  | choose Z3_Proof.Commutativity = comm
blanchet@58061
   666
  | choose Z3_Proof.Def_Axiom = def_axiom
blanchet@58061
   667
  | choose (r as Z3_Proof.Intro_Def) = assumed r
blanchet@58061
   668
  | choose Z3_Proof.Apply_Def = apply_def
blanchet@58061
   669
  | choose Z3_Proof.Iff_Oeq = iff_oeq
blanchet@58061
   670
  | choose Z3_Proof.Nnf_Pos = nnf_pos
blanchet@58061
   671
  | choose Z3_Proof.Nnf_Neg = nnf_neg
blanchet@58061
   672
  | choose (r as Z3_Proof.Nnf_Star) = unsupported r
blanchet@58061
   673
  | choose (r as Z3_Proof.Cnf_Star) = unsupported r
blanchet@58061
   674
  | choose (r as Z3_Proof.Skolemize) = assumed r
blanchet@58061
   675
  | choose Z3_Proof.Modus_Ponens_Oeq = mp_oeq
blanchet@58061
   676
  | choose (Z3_Proof.Th_Lemma name) = th_lemma name
blanchet@56078
   677
blanchet@56078
   678
fun with_tracing rule method ctxt thms t =
blanchet@56078
   679
  let val _ = trace_goal ctxt rule thms t
blanchet@56078
   680
  in method ctxt thms t end
blanchet@56078
   681
blanchet@56078
   682
fun method_for rule = with_tracing rule (choose rule)
blanchet@56078
   683
blanchet@57229
   684
end;