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