src/HOL/Tools/Argo/argo_tactic.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (23 months ago)
changeset 66695 91500c024c7f
parent 66301 8a6a89d6cf2b
child 67091 1393c2340eec
permissions -rw-r--r--
tuned;
wenzelm@63992
     1
(*  Title:      HOL/Tools/Argo/argo_tactic.ML
boehmes@63960
     2
    Author:     Sascha Boehme
boehmes@63960
     3
boehmes@63960
     4
HOL method and tactic for the Argo solver.
boehmes@63960
     5
*)
boehmes@63960
     6
boehmes@63960
     7
signature ARGO_TACTIC =
boehmes@63960
     8
sig
boehmes@63960
     9
  val trace: string Config.T
boehmes@63960
    10
  val timeout: real Config.T
boehmes@63960
    11
boehmes@63960
    12
  (* extending the tactic *)
boehmes@63960
    13
  type trans_context =
boehmes@63960
    14
    Name.context * Argo_Expr.typ Typtab.table * (string * Argo_Expr.typ) Termtab.table
boehmes@63960
    15
  type ('a, 'b) trans = 'a -> trans_context -> 'b * trans_context
boehmes@63960
    16
  type ('a, 'b) trans' = 'a -> trans_context -> ('b * trans_context) option
boehmes@63960
    17
  type extension = {
boehmes@63960
    18
    trans_type: (typ, Argo_Expr.typ) trans -> (typ, Argo_Expr.typ) trans',
boehmes@63960
    19
    trans_term: (term, Argo_Expr.expr) trans -> (term, Argo_Expr.expr) trans',
boehmes@63960
    20
    term_of: (Argo_Expr.expr -> term) -> Argo_Expr.expr -> term option,
boehmes@63960
    21
    replay_rewr: Proof.context -> Argo_Proof.rewrite -> conv,
boehmes@63960
    22
    replay: (Argo_Expr.expr -> cterm) -> Proof.context -> Argo_Proof.rule -> thm list -> thm option}
boehmes@63960
    23
  val add_extension: extension -> theory -> theory
boehmes@63960
    24
boehmes@63960
    25
  (* proof utilities *)
boehmes@63960
    26
  val discharges: thm -> thm list -> thm list
boehmes@63960
    27
  val flatten_conv: conv -> thm -> conv
boehmes@63960
    28
boehmes@63960
    29
  (* interface to the tactic as well as the underlying checker and prover *)
boehmes@63960
    30
  datatype result = Satisfiable of term -> bool option | Unsatisfiable
boehmes@63960
    31
  val check: term list -> Proof.context -> result * Proof.context
boehmes@63960
    32
  val prove: thm list -> Proof.context -> thm option * Proof.context
boehmes@63960
    33
  val argo_tac: Proof.context -> thm list -> int -> tactic
boehmes@63960
    34
end
boehmes@63960
    35
boehmes@63960
    36
structure Argo_Tactic: ARGO_TACTIC =
boehmes@63960
    37
struct
boehmes@63960
    38
boehmes@63960
    39
(* readable fresh names for terms *)
boehmes@63960
    40
boehmes@63960
    41
fun fresh_name n = Name.variant (case Long_Name.base_name n of "" => "x" | n' => n')
boehmes@63960
    42
boehmes@63960
    43
fun fresh_type_name (Type (n, _)) = fresh_name n
boehmes@63960
    44
  | fresh_type_name (TFree (n, _)) = fresh_name n
boehmes@63960
    45
  | fresh_type_name (TVar ((n, i), _)) = fresh_name (n ^ "." ^ string_of_int i)
boehmes@63960
    46
boehmes@63960
    47
fun fresh_term_name (Const (n, _)) = fresh_name n
boehmes@63960
    48
  | fresh_term_name (Free (n, _)) = fresh_name n
boehmes@63960
    49
  | fresh_term_name (Var ((n, i), _)) = fresh_name (n ^ "." ^ string_of_int i)
boehmes@63960
    50
  | fresh_term_name _ = fresh_name ""
boehmes@63960
    51
boehmes@63960
    52
boehmes@63960
    53
(* tracing *)
boehmes@63960
    54
boehmes@63960
    55
datatype mode = None | Basic | Full
boehmes@63960
    56
boehmes@63960
    57
fun string_of_mode None = "none"
boehmes@63960
    58
  | string_of_mode Basic = "basic"
boehmes@63960
    59
  | string_of_mode Full = "full"
boehmes@63960
    60
boehmes@63960
    61
fun requires_mode None = []
boehmes@63960
    62
  | requires_mode Basic = [Basic, Full]
boehmes@63960
    63
  | requires_mode Full = [Full]
boehmes@63960
    64
boehmes@63960
    65
val trace = Attrib.setup_config_string @{binding argo_trace} (K (string_of_mode None))
boehmes@63960
    66
boehmes@63960
    67
fun allows_mode ctxt = exists (equal (Config.get ctxt trace) o string_of_mode) o requires_mode
boehmes@63960
    68
boehmes@63960
    69
fun output mode ctxt msg = if allows_mode ctxt mode then Output.tracing ("Argo: " ^ msg) else ()
boehmes@63960
    70
val tracing = output Basic
boehmes@63960
    71
val full_tracing = output Full
boehmes@63960
    72
boehmes@63960
    73
fun with_mode mode ctxt f = if allows_mode ctxt mode then f ctxt else ()
boehmes@63960
    74
val with_tracing = with_mode Basic
boehmes@63960
    75
val with_full_tracing = with_mode Full
boehmes@63960
    76
boehmes@63960
    77
boehmes@63960
    78
(* timeout *)
boehmes@63960
    79
boehmes@63960
    80
val timeout = Attrib.setup_config_real @{binding argo_timeout} (K 10.0)
boehmes@63960
    81
boehmes@63960
    82
fun time_of_timeout ctxt = Time.fromReal (Config.get ctxt timeout)
boehmes@63960
    83
boehmes@63960
    84
fun with_timeout ctxt f x = Timeout.apply (time_of_timeout ctxt) f x
boehmes@63960
    85
boehmes@63960
    86
boehmes@63960
    87
(* extending the tactic *)
boehmes@63960
    88
boehmes@63960
    89
type trans_context =
boehmes@63960
    90
  Name.context * Argo_Expr.typ Typtab.table * (string * Argo_Expr.typ) Termtab.table
boehmes@63960
    91
boehmes@63960
    92
type ('a, 'b) trans = 'a -> trans_context -> 'b * trans_context
boehmes@63960
    93
type ('a, 'b) trans' = 'a -> trans_context -> ('b * trans_context) option
boehmes@63960
    94
boehmes@63960
    95
type extension = {
boehmes@63960
    96
  trans_type: (typ, Argo_Expr.typ) trans -> (typ, Argo_Expr.typ) trans',
boehmes@63960
    97
  trans_term: (term, Argo_Expr.expr) trans -> (term, Argo_Expr.expr) trans',
boehmes@63960
    98
  term_of: (Argo_Expr.expr -> term) -> Argo_Expr.expr -> term option,
boehmes@63960
    99
  replay_rewr: Proof.context -> Argo_Proof.rewrite -> conv,
boehmes@63960
   100
  replay: (Argo_Expr.expr -> cterm) -> Proof.context -> Argo_Proof.rule -> thm list -> thm option}
boehmes@63960
   101
boehmes@63960
   102
fun eq_extension ((serial1, _), (serial2, _)) = (serial1 = serial2)
boehmes@63960
   103
boehmes@63960
   104
structure Extensions = Theory_Data
boehmes@63960
   105
(
boehmes@63960
   106
  type T = (serial * extension) list
boehmes@63960
   107
  val empty = []
boehmes@63960
   108
  val extend = I
boehmes@63960
   109
  val merge = merge eq_extension 
boehmes@63960
   110
)
boehmes@63960
   111
boehmes@63960
   112
fun add_extension ext = Extensions.map (insert eq_extension (serial (), ext))
boehmes@63960
   113
fun get_extensions ctxt = Extensions.get (Proof_Context.theory_of ctxt)
boehmes@63960
   114
fun apply_first ctxt f = get_first (fn (_, e) => f e) (get_extensions ctxt)
boehmes@63960
   115
boehmes@63960
   116
fun ext_trans sel ctxt f x tcx = apply_first ctxt (fn ext => sel ext f x tcx)
boehmes@63960
   117
boehmes@63960
   118
val ext_trans_type = ext_trans (fn {trans_type, ...}: extension => trans_type)
boehmes@63960
   119
val ext_trans_term = ext_trans (fn {trans_term, ...}: extension => trans_term)
boehmes@63960
   120
boehmes@63960
   121
fun ext_term_of ctxt f e = apply_first ctxt (fn {term_of, ...}: extension => term_of f e)
boehmes@63960
   122
boehmes@63960
   123
fun ext_replay_rewr ctxt r = 
boehmes@63960
   124
  get_extensions ctxt
boehmes@63960
   125
  |> map (fn (_, {replay_rewr, ...}: extension) => replay_rewr ctxt r)
boehmes@63960
   126
  |> Conv.first_conv
boehmes@63960
   127
boehmes@63960
   128
fun ext_replay cprop_of ctxt rule prems =
boehmes@63960
   129
  (case apply_first ctxt (fn {replay, ...}: extension => replay cprop_of ctxt rule prems) of
boehmes@63960
   130
    SOME thm => thm
boehmes@63960
   131
  | NONE => raise THM ("failed to replay " ^ quote (Argo_Proof.string_of_rule rule), 0, []))
boehmes@63960
   132
boehmes@63960
   133
boehmes@63960
   134
(* translating input terms *)
boehmes@63960
   135
boehmes@63960
   136
fun add_new_type T (names, types, terms) =
boehmes@63960
   137
  let
boehmes@63960
   138
    val (n, names') = fresh_type_name T names
boehmes@63960
   139
    val ty = Argo_Expr.Type n
boehmes@63960
   140
  in (ty, (names', Typtab.update (T, ty) types, terms)) end
boehmes@63960
   141
boehmes@63960
   142
fun add_type T (tcx as (_, types, _)) =
boehmes@63960
   143
  (case Typtab.lookup types T of
boehmes@63960
   144
    SOME ty => (ty, tcx)
boehmes@63960
   145
  | NONE => add_new_type T tcx)
boehmes@63960
   146
boehmes@63960
   147
fun trans_type _ @{typ HOL.bool} = pair Argo_Expr.Bool
boehmes@63960
   148
  | trans_type ctxt (Type (@{type_name "fun"}, [T1, T2])) =
boehmes@63960
   149
      trans_type ctxt T1 ##>> trans_type ctxt T2 #>> Argo_Expr.Func
boehmes@63960
   150
  | trans_type ctxt T = (fn tcx =>
boehmes@63960
   151
      (case ext_trans_type ctxt (trans_type ctxt) T tcx of
boehmes@63960
   152
        SOME result => result
boehmes@63960
   153
      | NONE => add_type T tcx))
boehmes@63960
   154
boehmes@63960
   155
fun add_new_term ctxt t T tcx =
boehmes@63960
   156
  let
boehmes@63960
   157
    val (ty, (names, types, terms)) = trans_type ctxt T tcx
boehmes@63960
   158
    val (n, names') = fresh_term_name t names
boehmes@63960
   159
    val c = (n, ty)
boehmes@63960
   160
  in (Argo_Expr.mk_con c, (names', types, Termtab.update (t, c) terms)) end
boehmes@63960
   161
boehmes@63960
   162
fun add_term ctxt t (tcx as (_, _, terms)) =
boehmes@63960
   163
  (case Termtab.lookup terms t of
boehmes@63960
   164
    SOME c => (Argo_Expr.mk_con c, tcx)
boehmes@63960
   165
  | NONE => add_new_term ctxt t (Term.fastype_of t) tcx)
boehmes@63960
   166
boehmes@63960
   167
fun mk_eq @{typ HOL.bool} = Argo_Expr.mk_iff
boehmes@63960
   168
  | mk_eq _ = Argo_Expr.mk_eq
boehmes@63960
   169
boehmes@63960
   170
fun trans_term _ @{const HOL.True} = pair Argo_Expr.true_expr
boehmes@63960
   171
  | trans_term _ @{const HOL.False} = pair Argo_Expr.false_expr
boehmes@63960
   172
  | trans_term ctxt (@{const HOL.Not} $ t) = trans_term ctxt t #>> Argo_Expr.mk_not
boehmes@63960
   173
  | trans_term ctxt (@{const HOL.conj} $ t1 $ t2) =
boehmes@63960
   174
      trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_and2
boehmes@63960
   175
  | trans_term ctxt (@{const HOL.disj} $ t1 $ t2) =
boehmes@63960
   176
      trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_or2
boehmes@63960
   177
  | trans_term ctxt (@{const HOL.implies} $ t1 $ t2) =
boehmes@63960
   178
      trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_imp
boehmes@63960
   179
  | trans_term ctxt (Const (@{const_name HOL.If}, _) $ t1 $ t2 $ t3) =
boehmes@63960
   180
      trans_term ctxt t1 ##>> trans_term ctxt t2 ##>> trans_term ctxt t3 #>>
boehmes@63960
   181
      (fn ((u1, u2), u3) => Argo_Expr.mk_ite u1 u2 u3)
boehmes@63960
   182
  | trans_term ctxt (Const (@{const_name HOL.eq}, T) $ t1 $ t2) =
boehmes@63960
   183
      trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry (mk_eq (Term.domain_type T))
boehmes@63960
   184
  | trans_term ctxt (t as (t1 $ t2)) = (fn tcx =>
boehmes@63960
   185
      (case ext_trans_term ctxt (trans_term ctxt) t tcx of
boehmes@63960
   186
        SOME result => result
boehmes@63960
   187
      | NONE => tcx |> trans_term ctxt t1 ||>> trans_term ctxt t2 |>> uncurry Argo_Expr.mk_app))
boehmes@63960
   188
  | trans_term ctxt t = (fn tcx =>
boehmes@63960
   189
      (case ext_trans_term ctxt (trans_term ctxt) t tcx of
boehmes@63960
   190
        SOME result => result
boehmes@63960
   191
      | NONE => add_term ctxt t tcx))
boehmes@63960
   192
boehmes@63960
   193
fun translate ctxt prop = trans_term ctxt (HOLogic.dest_Trueprop prop)
boehmes@63960
   194
boehmes@63960
   195
boehmes@63960
   196
(* invoking the solver *)
boehmes@63960
   197
boehmes@63960
   198
type data = {
boehmes@63960
   199
  names: Name.context,
boehmes@63960
   200
  types: Argo_Expr.typ Typtab.table,
boehmes@63960
   201
  terms: (string * Argo_Expr.typ) Termtab.table,
boehmes@63960
   202
  argo: Argo_Solver.context}
boehmes@63960
   203
boehmes@63960
   204
fun mk_data names types terms argo: data = {names=names, types=types, terms=terms, argo=argo}
boehmes@63960
   205
val empty_data = mk_data Name.context Typtab.empty Termtab.empty Argo_Solver.context
boehmes@63960
   206
boehmes@63960
   207
structure Solver_Data = Proof_Data
boehmes@63960
   208
(
boehmes@63960
   209
  type T = data option
boehmes@63960
   210
  fun init _ = SOME empty_data
boehmes@63960
   211
)
boehmes@63960
   212
boehmes@63960
   213
datatype ('m, 'p) solver_result = Model of 'm | Proof of 'p
boehmes@63960
   214
boehmes@63960
   215
fun raw_solve es argo = Model (Argo_Solver.assert es argo)
boehmes@63960
   216
  handle Argo_Proof.UNSAT proof => Proof proof
boehmes@63960
   217
boehmes@63960
   218
fun value_of terms model t =
boehmes@63960
   219
  (case Termtab.lookup terms t of
boehmes@63960
   220
    SOME c => model c
boehmes@63960
   221
  | _ => NONE)
boehmes@63960
   222
boehmes@63960
   223
fun trace_props props ctxt =
boehmes@63960
   224
  tracing ctxt (Pretty.string_of (Pretty.big_list "using these propositions:"
boehmes@63960
   225
    (map (Syntax.pretty_term ctxt) props)))
boehmes@63960
   226
boehmes@63960
   227
fun trace_result ctxt ({elapsed, ...}: Timing.timing) msg =
boehmes@63960
   228
  tracing ctxt ("found a " ^ msg ^ " in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")
boehmes@63960
   229
boehmes@63960
   230
fun solve props ctxt =
boehmes@63960
   231
  (case Solver_Data.get ctxt of
boehmes@63960
   232
    NONE => error "bad Argo solver context"
boehmes@63960
   233
  | SOME {names, types, terms, argo} =>
boehmes@63960
   234
      let
boehmes@63960
   235
        val _ = with_tracing ctxt (trace_props props)
boehmes@63960
   236
        val (es, (names', types', terms')) = fold_map (translate ctxt) props (names, types, terms)
boehmes@63960
   237
        val _ = tracing ctxt "starting the prover"
boehmes@63960
   238
      in
boehmes@63960
   239
        (case Timing.timing (raw_solve es) argo of
boehmes@63960
   240
          (time, Proof proof) =>
boehmes@63960
   241
            let val _ = trace_result ctxt time "proof"
boehmes@63960
   242
            in (Proof (terms', proof), Solver_Data.put NONE ctxt) end
boehmes@63960
   243
        | (time, Model argo') =>
boehmes@63960
   244
            let
boehmes@63960
   245
              val _ = trace_result ctxt time "model"
boehmes@63960
   246
              val model = value_of terms' (Argo_Solver.model_of argo')
boehmes@63960
   247
            in (Model model, Solver_Data.put (SOME (mk_data names' types' terms' argo')) ctxt) end)
boehmes@63960
   248
      end)
boehmes@63960
   249
boehmes@63960
   250
boehmes@63960
   251
(* reverse translation *)
boehmes@63960
   252
boehmes@63960
   253
structure Contab = Table(type key = string * Argo_Expr.typ val ord = Argo_Expr.con_ord)
boehmes@63960
   254
boehmes@63960
   255
fun mk_nary f ts = uncurry (fold_rev (curry f)) (split_last ts)
boehmes@63960
   256
boehmes@63960
   257
fun mk_nary' d _ [] = d
boehmes@63960
   258
  | mk_nary' _ f ts = mk_nary f ts
boehmes@63960
   259
boehmes@63960
   260
fun mk_ite t1 t2 t3 =
boehmes@63960
   261
  let
boehmes@63960
   262
    val T = Term.fastype_of t2
boehmes@63960
   263
    val ite = Const (@{const_name HOL.If}, [@{typ HOL.bool}, T, T] ---> T)
boehmes@63960
   264
  in ite $ t1 $ t2 $ t3 end
boehmes@63960
   265
boehmes@63960
   266
fun term_of _ (Argo_Expr.E (Argo_Expr.True, _)) = @{const HOL.True}
boehmes@63960
   267
  | term_of _ (Argo_Expr.E (Argo_Expr.False, _)) = @{const HOL.False}
boehmes@63960
   268
  | term_of cx (Argo_Expr.E (Argo_Expr.Not, [e])) = HOLogic.mk_not (term_of cx e)
boehmes@63960
   269
  | term_of cx (Argo_Expr.E (Argo_Expr.And, es)) =
boehmes@63960
   270
      mk_nary' @{const HOL.True} HOLogic.mk_conj (map (term_of cx) es)
boehmes@63960
   271
  | term_of cx (Argo_Expr.E (Argo_Expr.Or, es)) =
boehmes@63960
   272
      mk_nary' @{const HOL.False} HOLogic.mk_disj (map (term_of cx) es)
boehmes@63960
   273
  | term_of cx (Argo_Expr.E (Argo_Expr.Imp, [e1, e2])) =
boehmes@63960
   274
      HOLogic.mk_imp (term_of cx e1, term_of cx e2)
boehmes@63960
   275
  | term_of cx (Argo_Expr.E (Argo_Expr.Iff, [e1, e2])) =
boehmes@63960
   276
      HOLogic.mk_eq (term_of cx e1, term_of cx e2)
boehmes@63960
   277
  | term_of cx (Argo_Expr.E (Argo_Expr.Ite, [e1, e2, e3])) =
boehmes@63960
   278
      mk_ite (term_of cx e1) (term_of cx e2) (term_of cx e3)
boehmes@63960
   279
  | term_of cx (Argo_Expr.E (Argo_Expr.Eq, [e1, e2])) =
boehmes@63960
   280
      HOLogic.mk_eq (term_of cx e1, term_of cx e2)
boehmes@63960
   281
  | term_of cx (Argo_Expr.E (Argo_Expr.App, [e1, e2])) =
boehmes@63960
   282
      term_of cx e1 $ term_of cx e2
boehmes@63960
   283
  | term_of (_, cons) (Argo_Expr.E (Argo_Expr.Con (c as (n, _)), _)) =
boehmes@63960
   284
      (case Contab.lookup cons c of
boehmes@63960
   285
        SOME t => t
boehmes@63960
   286
      | NONE => error ("Unexpected expression named " ^ quote n))
boehmes@63960
   287
  | term_of (cx as (ctxt, _)) e =
boehmes@63960
   288
      (case ext_term_of ctxt (term_of cx) e of
boehmes@63960
   289
        SOME t => t
boehmes@63960
   290
      | NONE => raise Fail "bad expression")
boehmes@63960
   291
boehmes@63960
   292
fun as_prop ct = Thm.apply @{cterm HOL.Trueprop} ct
boehmes@63960
   293
boehmes@63960
   294
fun cterm_of ctxt cons e = Thm.cterm_of ctxt (term_of (ctxt, cons) e)
boehmes@63960
   295
fun cprop_of ctxt cons e = as_prop (cterm_of ctxt cons e)
boehmes@63960
   296
boehmes@63960
   297
boehmes@63960
   298
(* generic proof tools *)
boehmes@63960
   299
boehmes@63960
   300
fun discharge thm rule = thm INCR_COMP rule
boehmes@63960
   301
fun discharge2 thm1 thm2 rule = discharge thm2 (discharge thm1 rule)
boehmes@63960
   302
fun discharges thm rules = [thm] RL rules
boehmes@63960
   303
boehmes@63960
   304
fun under_assumption f ct =
boehmes@63960
   305
  let val cprop = as_prop ct
boehmes@63960
   306
  in Thm.implies_intr cprop (f (Thm.assume cprop)) end
boehmes@63960
   307
boehmes@63960
   308
fun instantiate cv ct = Thm.instantiate ([], [(Term.dest_Var (Thm.term_of cv), ct)])
boehmes@63960
   309
boehmes@63960
   310
boehmes@63960
   311
(* proof replay for tautologies *)
boehmes@63960
   312
boehmes@63960
   313
fun prove_taut ctxt ns t = Goal.prove ctxt ns [] (HOLogic.mk_Trueprop t)
boehmes@63960
   314
  (fn {context, ...} => HEADGOAL (Classical.fast_tac context))
boehmes@63960
   315
boehmes@63960
   316
fun with_frees ctxt n mk =
boehmes@63960
   317
  let
boehmes@63960
   318
    val ns = map (fn i => "P" ^ string_of_int i) (0 upto (n - 1))
boehmes@63960
   319
    val ts = map (Free o rpair @{typ bool}) ns
boehmes@63960
   320
    val t = mk_nary HOLogic.mk_disj (mk ts)
boehmes@63960
   321
  in prove_taut ctxt ns t end
boehmes@63960
   322
boehmes@63960
   323
fun taut_and1_term ts = mk_nary HOLogic.mk_conj ts :: map HOLogic.mk_not ts
boehmes@63960
   324
fun taut_and2_term i ts = [HOLogic.mk_not (mk_nary HOLogic.mk_conj ts), nth ts i]
boehmes@63960
   325
fun taut_or1_term i ts = [mk_nary HOLogic.mk_disj ts, HOLogic.mk_not (nth ts i)]
boehmes@63960
   326
fun taut_or2_term ts = HOLogic.mk_not (mk_nary HOLogic.mk_disj ts) :: ts
boehmes@63960
   327
boehmes@63960
   328
val iff_1_taut = @{lemma "P = Q | P | Q" by fast}
boehmes@63960
   329
val iff_2_taut = @{lemma "P = Q | (~P) | (~Q)" by fast}
boehmes@63960
   330
val iff_3_taut = @{lemma "~(P = Q) | (~P) | Q" by fast}
boehmes@63960
   331
val iff_4_taut = @{lemma "~(P = Q) | P | (~Q)" by fast}
boehmes@63960
   332
val ite_then_taut = @{lemma "~P | (if P then t else u) = t" by auto}
boehmes@63960
   333
val ite_else_taut = @{lemma "P | (if P then t else u) = u" by auto}
boehmes@63960
   334
boehmes@63960
   335
fun taut_rule_of ctxt (Argo_Proof.Taut_And_1 n) = with_frees ctxt n taut_and1_term
boehmes@63960
   336
  | taut_rule_of ctxt (Argo_Proof.Taut_And_2 (i, n)) = with_frees ctxt n (taut_and2_term i)
boehmes@63960
   337
  | taut_rule_of ctxt (Argo_Proof.Taut_Or_1 (i, n)) = with_frees ctxt n (taut_or1_term i)
boehmes@63960
   338
  | taut_rule_of ctxt (Argo_Proof.Taut_Or_2 n) = with_frees ctxt n taut_or2_term
boehmes@63960
   339
  | taut_rule_of _ Argo_Proof.Taut_Iff_1 = iff_1_taut
boehmes@63960
   340
  | taut_rule_of _ Argo_Proof.Taut_Iff_2 = iff_2_taut
boehmes@63960
   341
  | taut_rule_of _ Argo_Proof.Taut_Iff_3 = iff_3_taut
boehmes@63960
   342
  | taut_rule_of _ Argo_Proof.Taut_Iff_4 = iff_4_taut
boehmes@63960
   343
  | taut_rule_of _ Argo_Proof.Taut_Ite_Then = ite_then_taut
boehmes@63960
   344
  | taut_rule_of _ Argo_Proof.Taut_Ite_Else = ite_else_taut
boehmes@63960
   345
boehmes@63960
   346
fun replay_taut ctxt k ct =
boehmes@63960
   347
  let val rule = taut_rule_of ctxt k
boehmes@63960
   348
  in Thm.instantiate (Thm.match (Thm.cprop_of rule, ct)) rule end
boehmes@63960
   349
boehmes@63960
   350
boehmes@63960
   351
(* proof replay for conjunct extraction *)
boehmes@63960
   352
boehmes@63960
   353
fun replay_conjunct 0 1 thm = thm
boehmes@63960
   354
  | replay_conjunct 0 _ thm = discharge thm @{thm conjunct1}
boehmes@63960
   355
  | replay_conjunct 1 2 thm = discharge thm @{thm conjunct2}
boehmes@63960
   356
  | replay_conjunct i n thm = replay_conjunct (i - 1) (n - 1) (discharge thm @{thm conjunct2})
boehmes@63960
   357
boehmes@63960
   358
boehmes@63960
   359
(* proof replay for rewrite steps *)
boehmes@63960
   360
boehmes@63960
   361
fun mk_rewr thm = thm RS @{thm eq_reflection}
boehmes@63960
   362
boehmes@63960
   363
fun not_nary_conv rule i ct =
boehmes@63960
   364
  if i > 1 then (Conv.rewr_conv rule then_conv Conv.arg_conv (not_nary_conv rule (i - 1))) ct
boehmes@63960
   365
  else Conv.all_conv ct
boehmes@63960
   366
boehmes@63960
   367
val flatten_and_thm = @{lemma "(P1 & P2) & P3 == P1 & P2 & P3" by simp}
boehmes@63960
   368
val flatten_or_thm = @{lemma "(P1 | P2) | P3 == P1 | P2 | P3" by simp}
boehmes@63960
   369
boehmes@63960
   370
fun flatten_conv cv rule ct = (
boehmes@63960
   371
  Conv.try_conv (Conv.arg_conv cv) then_conv
boehmes@63960
   372
  Conv.try_conv (Conv.rewr_conv rule then_conv cv)) ct
boehmes@63960
   373
boehmes@63960
   374
fun flat_conj_conv ct =
boehmes@63960
   375
  (case Thm.term_of ct of
boehmes@63960
   376
    @{const HOL.conj} $ _ $ _ => flatten_conv flat_conj_conv flatten_and_thm ct
boehmes@63960
   377
  | _ => Conv.all_conv ct)
boehmes@63960
   378
boehmes@63960
   379
fun flat_disj_conv ct =
boehmes@63960
   380
  (case Thm.term_of ct of
boehmes@63960
   381
    @{const HOL.disj} $ _ $ _ => flatten_conv flat_disj_conv flatten_or_thm ct
boehmes@63960
   382
  | _ => Conv.all_conv ct)
boehmes@63960
   383
boehmes@63960
   384
fun explode rule1 rule2 thm =
boehmes@63960
   385
  explode rule1 rule2 (thm RS rule1) @ explode rule1 rule2 (thm RS rule2) handle THM _ => [thm]
boehmes@63960
   386
val explode_conj = explode @{thm conjunct1} @{thm conjunct2}
boehmes@63960
   387
val explode_ndis = explode @{lemma "~(P | Q) ==> ~P" by auto} @{lemma "~(P | Q) ==> ~Q" by auto}
boehmes@63960
   388
boehmes@63960
   389
fun pick_false i thms = nth thms i
boehmes@63960
   390
boehmes@63960
   391
fun pick_dual rule (i1, i2) thms =
boehmes@63960
   392
  rule OF [nth thms i1, nth thms i2] handle THM _ => rule OF [nth thms i2, nth thms i1]
boehmes@63960
   393
val pick_dual_conj = pick_dual @{lemma "~P ==> P ==> False" by auto}
boehmes@63960
   394
val pick_dual_ndis = pick_dual @{lemma "~P ==> P ==> ~True" by auto}
boehmes@63960
   395
boehmes@63960
   396
fun join thm0 rule is thms =
boehmes@63960
   397
  let
boehmes@63960
   398
    val l = length thms
boehmes@63960
   399
    val thms' = fold (fn i => cons (if 0 <= i andalso i < l then nth thms i else thm0)) is []
boehmes@63960
   400
  in fold (fn thm => fn thm' => discharge2 thm thm' rule) (tl thms') (hd thms') end
boehmes@63960
   401
boehmes@63960
   402
val join_conj = join @{lemma "True" by auto} @{lemma "P ==> Q ==> P & Q" by auto}
boehmes@63960
   403
val join_ndis = join @{lemma "~False" by auto} @{lemma "~P ==> ~Q ==> ~(P | Q)" by auto}
boehmes@63960
   404
boehmes@63960
   405
val false_thm = @{lemma "False ==> P" by auto}
boehmes@63960
   406
val ntrue_thm = @{lemma "~True ==> P" by auto}
boehmes@63960
   407
val iff_conj_thm = @{lemma "(P ==> Q) ==> (Q ==> P) ==> P = Q" by auto}
boehmes@63960
   408
val iff_ndis_thm = @{lemma "(~P ==> ~Q) ==> (~Q ==> ~P) ==> P = Q" by auto}
boehmes@63960
   409
boehmes@63960
   410
fun iff_intro rule lf rf ct =
boehmes@63960
   411
  let
boehmes@63960
   412
    val lhs = under_assumption lf ct
boehmes@63960
   413
    val rhs = rf (Thm.dest_arg (snd (Thm.dest_implies (Thm.cprop_of lhs))))
boehmes@63960
   414
  in mk_rewr (discharge2 lhs rhs rule) end
boehmes@63960
   415
boehmes@63960
   416
fun with_conj f g ct = iff_intro iff_conj_thm (f o explode_conj) g ct
boehmes@63960
   417
fun with_ndis f g ct = iff_intro iff_ndis_thm (f o explode_ndis) g (Thm.apply @{cterm HOL.Not} ct)
boehmes@63960
   418
boehmes@63960
   419
fun swap_indices n iss = map (fn i => find_index (fn is => member (op =) is i) iss) (0 upto (n - 1))
boehmes@63960
   420
fun sort_nary w f g (n, iss) = w (f (map hd iss)) (under_assumption (f (swap_indices n iss) o g))
boehmes@63960
   421
val sort_conj = sort_nary with_conj join_conj explode_conj
boehmes@63960
   422
val sort_ndis = sort_nary with_ndis join_ndis explode_ndis 
boehmes@63960
   423
boehmes@63960
   424
val not_true_thm = mk_rewr @{lemma "(~True) = False" by auto}
boehmes@63960
   425
val not_false_thm = mk_rewr @{lemma "(~False) = True" by auto}
boehmes@63960
   426
val not_not_thm = mk_rewr @{lemma "(~~P) = P" by auto}
boehmes@63960
   427
val not_and_thm = mk_rewr @{lemma "(~(P & Q)) = (~P | ~Q)" by auto}
boehmes@63960
   428
val not_or_thm = mk_rewr @{lemma "(~(P | Q)) = (~P & ~Q)" by auto}
boehmes@63960
   429
val not_iff_thms = map mk_rewr
boehmes@63960
   430
  @{lemma "(~((~P) = Q)) = (P = Q)" "(~(P = (~Q))) = (P = Q)" "(~(P = Q)) = ((~P) = Q)" by auto}
boehmes@63960
   431
val iff_true_thms = map mk_rewr @{lemma "(True = P) = P" "(P = True) = P" by auto}
boehmes@63960
   432
val iff_false_thms = map mk_rewr @{lemma "(False = P) = (~P)" "(P = False) = (~P)" by auto}
boehmes@63960
   433
val iff_not_not_thm = mk_rewr @{lemma "((~P) = (~Q)) = (P = Q)" by auto}
boehmes@63960
   434
val iff_refl_thm = mk_rewr @{lemma "(P = P) = True" by auto}
boehmes@63960
   435
val iff_symm_thm = mk_rewr @{lemma "(P = Q) = (Q = P)" by auto}
boehmes@63960
   436
val iff_dual_thms = map mk_rewr @{lemma "(P = (~P)) = False" "((~P) = P) = False" by auto}
boehmes@63960
   437
val imp_thm = mk_rewr @{lemma "(P --> Q) = (~P | Q)" by auto}
boehmes@63960
   438
val ite_prop_thm = mk_rewr @{lemma "(If P Q R) = ((~P | Q) & (P | R) & (Q | R))" by auto}
boehmes@63960
   439
val ite_true_thm = mk_rewr @{lemma "(If True t u) = t" by auto}
boehmes@63960
   440
val ite_false_thm = mk_rewr @{lemma "(If False t u) = u" by auto}
boehmes@63960
   441
val ite_eq_thm = mk_rewr @{lemma "(If P t t) = t" by auto}
boehmes@63960
   442
val eq_refl_thm = mk_rewr @{lemma "(t = t) = True" by auto}
boehmes@63960
   443
val eq_symm_thm = mk_rewr @{lemma "(t1 = t2) = (t2 = t1)" by auto}
boehmes@63960
   444
boehmes@63960
   445
fun replay_rewr _ Argo_Proof.Rewr_Not_True = Conv.rewr_conv not_true_thm
boehmes@63960
   446
  | replay_rewr _ Argo_Proof.Rewr_Not_False = Conv.rewr_conv not_false_thm
boehmes@63960
   447
  | replay_rewr _ Argo_Proof.Rewr_Not_Not = Conv.rewr_conv not_not_thm
boehmes@63960
   448
  | replay_rewr _ (Argo_Proof.Rewr_Not_And i) = not_nary_conv not_and_thm i
boehmes@63960
   449
  | replay_rewr _ (Argo_Proof.Rewr_Not_Or i) = not_nary_conv not_or_thm i
boehmes@63960
   450
  | replay_rewr _ Argo_Proof.Rewr_Not_Iff = Conv.rewrs_conv not_iff_thms
boehmes@63960
   451
  | replay_rewr _ (Argo_Proof.Rewr_And_False i) = with_conj (pick_false i) (K false_thm)
boehmes@63960
   452
  | replay_rewr _ (Argo_Proof.Rewr_And_Dual ip) = with_conj (pick_dual_conj ip) (K false_thm)
boehmes@63960
   453
  | replay_rewr _ (Argo_Proof.Rewr_And_Sort is) = flat_conj_conv then_conv sort_conj is
boehmes@63960
   454
  | replay_rewr _ (Argo_Proof.Rewr_Or_True i) = with_ndis (pick_false i) (K ntrue_thm)
boehmes@63960
   455
  | replay_rewr _ (Argo_Proof.Rewr_Or_Dual ip) = with_ndis (pick_dual_ndis ip) (K ntrue_thm)
boehmes@63960
   456
  | replay_rewr _ (Argo_Proof.Rewr_Or_Sort is) = flat_disj_conv then_conv sort_ndis is
boehmes@63960
   457
  | replay_rewr _ Argo_Proof.Rewr_Iff_True = Conv.rewrs_conv iff_true_thms
boehmes@63960
   458
  | replay_rewr _ Argo_Proof.Rewr_Iff_False = Conv.rewrs_conv iff_false_thms
boehmes@63960
   459
  | replay_rewr _ Argo_Proof.Rewr_Iff_Not_Not = Conv.rewr_conv iff_not_not_thm
boehmes@63960
   460
  | replay_rewr _ Argo_Proof.Rewr_Iff_Refl = Conv.rewr_conv iff_refl_thm
boehmes@63960
   461
  | replay_rewr _ Argo_Proof.Rewr_Iff_Symm = Conv.rewr_conv iff_symm_thm
boehmes@63960
   462
  | replay_rewr _ Argo_Proof.Rewr_Iff_Dual  = Conv.rewrs_conv iff_dual_thms
boehmes@63960
   463
  | replay_rewr _ Argo_Proof.Rewr_Imp = Conv.rewr_conv imp_thm
boehmes@63960
   464
  | replay_rewr _ Argo_Proof.Rewr_Ite_Prop = Conv.rewr_conv ite_prop_thm
boehmes@63960
   465
  | replay_rewr _ Argo_Proof.Rewr_Ite_True = Conv.rewr_conv ite_true_thm
boehmes@63960
   466
  | replay_rewr _ Argo_Proof.Rewr_Ite_False = Conv.rewr_conv ite_false_thm
boehmes@63960
   467
  | replay_rewr _ Argo_Proof.Rewr_Ite_Eq = Conv.rewr_conv ite_eq_thm
boehmes@63960
   468
  | replay_rewr _ Argo_Proof.Rewr_Eq_Refl = Conv.rewr_conv eq_refl_thm
boehmes@63960
   469
  | replay_rewr _ Argo_Proof.Rewr_Eq_Symm = Conv.rewr_conv eq_symm_thm
boehmes@63960
   470
  | replay_rewr ctxt r = ext_replay_rewr ctxt r
boehmes@63960
   471
boehmes@63960
   472
fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
boehmes@63960
   473
boehmes@63960
   474
fun replay_conv _ Argo_Proof.Keep_Conv ct = Conv.all_conv ct
boehmes@63960
   475
  | replay_conv ctxt (Argo_Proof.Then_Conv (c1, c2)) ct = 
boehmes@63960
   476
      (replay_conv ctxt c1 then_conv replay_conv ctxt c2) ct
boehmes@66301
   477
  | replay_conv ctxt (Argo_Proof.Args_Conv (Argo_Expr.App, [c1, c2])) ct =
boehmes@66301
   478
      Conv.combination_conv (replay_conv ctxt c1) (replay_conv ctxt c2) ct
boehmes@66301
   479
  | replay_conv ctxt (Argo_Proof.Args_Conv (_, cs)) ct = replay_args_conv ctxt cs ct
boehmes@63960
   480
  | replay_conv ctxt (Argo_Proof.Rewr_Conv r) ct = replay_rewr ctxt r ct
boehmes@63960
   481
boehmes@63960
   482
and replay_args_conv _ [] ct = Conv.all_conv ct
boehmes@63960
   483
  | replay_args_conv ctxt [c] ct = Conv.arg_conv (replay_conv ctxt c) ct
boehmes@63960
   484
  | replay_args_conv ctxt [c1, c2] ct = binop_conv (replay_conv ctxt c1) (replay_conv ctxt c2) ct
boehmes@63960
   485
  | replay_args_conv ctxt (c :: cs) ct =
boehmes@63960
   486
      (case Term.head_of (Thm.term_of ct) of
boehmes@63960
   487
        Const (@{const_name HOL.If}, _) =>
boehmes@63960
   488
          let val (cs', c') = split_last cs
boehmes@63960
   489
          in Conv.combination_conv (replay_args_conv ctxt (c :: cs')) (replay_conv ctxt c') ct end
boehmes@63960
   490
      | _ => binop_conv (replay_conv ctxt c) (replay_args_conv ctxt cs) ct)
boehmes@63960
   491
boehmes@63960
   492
fun replay_rewrite ctxt c thm = Conv.fconv_rule (HOLogic.Trueprop_conv (replay_conv ctxt c)) thm
boehmes@63960
   493
boehmes@63960
   494
boehmes@63960
   495
(* proof replay for clauses *)
boehmes@63960
   496
boehmes@63960
   497
val prep_clause_rule = @{lemma "P ==> ~P ==> False" by fast}
boehmes@63960
   498
val extract_lit_rule = @{lemma "(~(P | Q) ==> False) ==> ~P ==> ~Q ==> False" by fast}
boehmes@63960
   499
boehmes@63960
   500
fun add_lit i thm lits =
boehmes@63960
   501
  let val ct = Thm.cprem_of thm 1
boehmes@63960
   502
  in (Thm.implies_elim thm (Thm.assume ct), (i, ct) :: lits) end
boehmes@63960
   503
boehmes@63960
   504
fun extract_lits [] _ = error "Bad clause"
boehmes@63960
   505
  | extract_lits [i] (thm, lits) = add_lit i thm lits
boehmes@63960
   506
  | extract_lits (i :: is) (thm, lits) =
boehmes@63960
   507
      extract_lits is (add_lit i (discharge thm extract_lit_rule) lits)
boehmes@63960
   508
boehmes@63960
   509
fun lit_ord ((l1, _), (l2, _)) = int_ord (abs l1, abs l2)
boehmes@63960
   510
boehmes@63960
   511
fun replay_with_lits [] thm lits = (thm, lits)
boehmes@63960
   512
  | replay_with_lits is thm lits =
boehmes@63960
   513
      extract_lits is (discharge thm prep_clause_rule, lits)
boehmes@63960
   514
      ||> Ord_List.make lit_ord
boehmes@63960
   515
boehmes@63960
   516
fun replay_clause is thm = replay_with_lits is thm []
boehmes@63960
   517
boehmes@63960
   518
boehmes@63960
   519
(* proof replay for unit resolution *)
boehmes@63960
   520
boehmes@63960
   521
val unit_rule = @{lemma "(P ==> False) ==> (~P ==> False) ==> False" by fast}
boehmes@63960
   522
val unit_rule_var = Thm.dest_arg (Thm.dest_arg1 (Thm.cprem_of unit_rule 1))
boehmes@63960
   523
val bogus_ct = @{cterm HOL.True}
boehmes@63960
   524
boehmes@63960
   525
fun replay_unit_res lit (pthm, plits) (nthm, nlits) =
boehmes@63960
   526
  let
boehmes@63960
   527
    val plit = the (AList.lookup (op =) plits lit)
boehmes@63960
   528
    val nlit = the (AList.lookup (op =) nlits (~lit))
boehmes@63960
   529
    val prune = Ord_List.remove lit_ord (lit, bogus_ct)
boehmes@63960
   530
  in
boehmes@63960
   531
    unit_rule
boehmes@63960
   532
    |> instantiate unit_rule_var (Thm.dest_arg plit)
boehmes@63960
   533
    |> Thm.elim_implies (Thm.implies_intr plit pthm)
boehmes@63960
   534
    |> Thm.elim_implies (Thm.implies_intr nlit nthm)
boehmes@63960
   535
    |> rpair (Ord_List.union lit_ord (prune nlits) (prune plits))
boehmes@63960
   536
  end
boehmes@63960
   537
boehmes@63960
   538
boehmes@63960
   539
(* proof replay for hypothesis *)
boehmes@63960
   540
boehmes@63960
   541
val dneg_rule = @{lemma "~~P ==> P" by auto}
boehmes@63960
   542
boehmes@63960
   543
fun replay_hyp i ct =
boehmes@63960
   544
  if i < 0 then (Thm.assume ct, [(~i, ct)])
boehmes@63960
   545
  else
boehmes@63960
   546
    let val cu = as_prop (Thm.apply @{cterm HOL.Not} (Thm.apply @{cterm HOL.Not} (Thm.dest_arg ct)))
boehmes@63960
   547
    in (discharge (Thm.assume cu) dneg_rule, [(~i, cu)]) end
boehmes@63960
   548
boehmes@63960
   549
boehmes@63960
   550
(* proof replay for lemma *)
boehmes@63960
   551
boehmes@63960
   552
fun replay_lemma is (thm, lits) = replay_with_lits is thm lits
boehmes@63960
   553
boehmes@63960
   554
boehmes@63960
   555
(* proof replay for reflexivity *)
boehmes@63960
   556
boehmes@63960
   557
val refl_rule = @{thm refl}
boehmes@63960
   558
val refl_rule_var = Thm.dest_arg1 (Thm.dest_arg (Thm.cprop_of refl_rule))
boehmes@63960
   559
boehmes@63960
   560
fun replay_refl ct = Thm.instantiate (Thm.match (refl_rule_var, ct)) refl_rule
boehmes@63960
   561
boehmes@63960
   562
boehmes@63960
   563
(* proof replay for symmetry *)
boehmes@63960
   564
boehmes@63960
   565
val symm_rules = @{lemma "a = b ==> b = a" "~(a = b) ==> ~(b = a)" by simp_all}
boehmes@63960
   566
boehmes@63960
   567
fun replay_symm thm = hd (discharges thm symm_rules)
boehmes@63960
   568
boehmes@63960
   569
boehmes@63960
   570
(* proof replay for transitivity *)
boehmes@63960
   571
boehmes@63960
   572
val trans_rules = @{lemma
boehmes@63960
   573
  "~(a = b) ==> b = c ==> ~(a = c)"
boehmes@63960
   574
  "a = b ==> ~(b = c) ==> ~(a = c)"
boehmes@63960
   575
  "a = b ==> b = c ==> a = c"
boehmes@63960
   576
  by simp_all}
boehmes@63960
   577
boehmes@63960
   578
fun replay_trans thm1 thm2 = hd (discharges thm2 (discharges thm1 trans_rules))
boehmes@63960
   579
boehmes@63960
   580
boehmes@63960
   581
(* proof replay for congruence *)
boehmes@63960
   582
boehmes@63960
   583
fun replay_cong thm1 thm2 = discharge thm2 (discharge thm1 @{thm cong})
boehmes@63960
   584
boehmes@63960
   585
boehmes@63960
   586
(* proof replay for substitution *)
boehmes@63960
   587
boehmes@63960
   588
val subst_rule1 = @{lemma "~(p a) ==> p = q ==> a = b ==> ~(q b)" by simp}
boehmes@63960
   589
val subst_rule2 = @{lemma "p a ==> p = q ==> a = b ==> q b" by simp}
boehmes@63960
   590
boehmes@63960
   591
fun replay_subst thm1 thm2 thm3 =
boehmes@63960
   592
  subst_rule1 OF [thm1, thm2, thm3] handle THM _ => subst_rule2 OF [thm1, thm2, thm3]
boehmes@63960
   593
boehmes@63960
   594
boehmes@63960
   595
(* proof replay *)
boehmes@63960
   596
boehmes@63960
   597
structure Thm_Cache = Table(type key = Argo_Proof.proof_id val ord = Argo_Proof.proof_id_ord)
boehmes@63960
   598
boehmes@63960
   599
val unclausify_rule1 = @{lemma "(~P ==> False) ==> P" by auto}
boehmes@63960
   600
val unclausify_rule2 = @{lemma "(P ==> False) ==> ~P" by auto}
boehmes@63960
   601
boehmes@63960
   602
fun unclausify (thm, lits) ls =
boehmes@63960
   603
  (case (Thm.prop_of thm, lits) of
boehmes@63960
   604
    (@{const HOL.Trueprop} $ @{const HOL.False}, [(_, ct)]) =>
boehmes@63960
   605
      let val thm = Thm.implies_intr ct thm
boehmes@63960
   606
      in (discharge thm unclausify_rule1 handle THM _ => discharge thm unclausify_rule2, ls) end
boehmes@63960
   607
  | _ => (thm, Ord_List.union lit_ord lits ls))
boehmes@63960
   608
boehmes@63960
   609
fun with_thms f tps = fold_map unclausify tps [] |>> f
boehmes@63960
   610
boehmes@63960
   611
fun bad_premises () = raise Fail "bad number of premises"
boehmes@63960
   612
fun with_thms1 f = with_thms (fn [thm] => f thm | _ => bad_premises ())
boehmes@63960
   613
fun with_thms2 f = with_thms (fn [thm1, thm2] => f thm1 thm2 | _ => bad_premises ())
boehmes@63960
   614
fun with_thms3 f = with_thms (fn [thm1, thm2, thm3] => f thm1 thm2 thm3 | _ => bad_premises ())
boehmes@63960
   615
boehmes@63960
   616
fun replay_rule (ctxt, cons, facts) prems rule =
boehmes@63960
   617
  (case rule of
boehmes@63960
   618
    Argo_Proof.Axiom i => (nth facts i, [])
boehmes@63960
   619
  | Argo_Proof.Taut (k, concl) => (replay_taut ctxt k (cprop_of ctxt cons concl), [])
boehmes@63960
   620
  | Argo_Proof.Conjunct (i, n) => with_thms1 (replay_conjunct i n) prems
boehmes@63960
   621
  | Argo_Proof.Rewrite c => with_thms1 (replay_rewrite ctxt c) prems
boehmes@63960
   622
  | Argo_Proof.Clause is => replay_clause is (fst (hd prems))
boehmes@63960
   623
  | Argo_Proof.Unit_Res i => replay_unit_res i (hd prems) (hd (tl prems))
boehmes@63960
   624
  | Argo_Proof.Hyp (i, concl) => replay_hyp i (cprop_of ctxt cons concl)
boehmes@63960
   625
  | Argo_Proof.Lemma is => replay_lemma is (hd prems)
boehmes@63960
   626
  | Argo_Proof.Refl concl => (replay_refl (cterm_of ctxt cons concl), [])
boehmes@63960
   627
  | Argo_Proof.Symm => with_thms1 replay_symm prems
boehmes@63960
   628
  | Argo_Proof.Trans => with_thms2 replay_trans prems
boehmes@63960
   629
  | Argo_Proof.Cong => with_thms2 replay_cong prems
boehmes@63960
   630
  | Argo_Proof.Subst => with_thms3 replay_subst prems
boehmes@63960
   631
  | _ => with_thms (ext_replay (cprop_of ctxt cons) ctxt rule) prems)
boehmes@63960
   632
boehmes@63960
   633
fun with_cache f proof thm_cache =
boehmes@63960
   634
  (case Thm_Cache.lookup thm_cache (Argo_Proof.id_of proof) of
boehmes@63960
   635
    SOME thm => (thm, thm_cache)
boehmes@63960
   636
  | NONE =>
boehmes@63960
   637
      let val (thm, thm_cache') = f proof thm_cache
boehmes@63960
   638
      in (thm, Thm_Cache.update (Argo_Proof.id_of proof, thm) thm_cache') end)
boehmes@63960
   639
boehmes@63960
   640
fun trace_step ctxt proof_id rule proofs = with_full_tracing ctxt (fn ctxt' =>
boehmes@63960
   641
  let
boehmes@63960
   642
    val id = Argo_Proof.string_of_proof_id proof_id
boehmes@63960
   643
    val ids = map (Argo_Proof.string_of_proof_id o Argo_Proof.id_of) proofs
boehmes@63960
   644
    val rule_string = Argo_Proof.string_of_rule rule
boehmes@63960
   645
  in full_tracing ctxt' ("  " ^ id ^ " <- " ^ space_implode " " ids ^ " . " ^ rule_string) end)
boehmes@63960
   646
boehmes@63960
   647
fun replay_bottom_up (env as (ctxt, _, _)) proof thm_cache =
boehmes@63960
   648
  let
boehmes@63960
   649
    val (proof_id, rule, proofs) = Argo_Proof.dest proof
boehmes@63960
   650
    val (prems, thm_cache) = fold_map (with_cache (replay_bottom_up env)) proofs thm_cache
boehmes@63960
   651
    val _ = trace_step ctxt proof_id rule proofs
boehmes@63960
   652
  in (replay_rule env prems rule, thm_cache) end
boehmes@63960
   653
boehmes@63960
   654
fun replay_proof env proof = with_cache (replay_bottom_up env) proof Thm_Cache.empty
boehmes@63960
   655
boehmes@63960
   656
fun replay ctxt terms facts proof =
boehmes@63960
   657
  let
boehmes@63960
   658
    val env = (ctxt, Termtab.fold (Contab.update o swap) terms Contab.empty, facts)
boehmes@63960
   659
    val _ = tracing ctxt "replaying the proof"
boehmes@63960
   660
    val ({elapsed=t, ...}, ((thm, _), _)) = Timing.timing (replay_proof env) proof
boehmes@63960
   661
    val _ = tracing ctxt ("replayed the proof in " ^ string_of_int (Time.toMilliseconds t) ^ " ms")
boehmes@63960
   662
  in thm end
boehmes@63960
   663
boehmes@63960
   664
boehmes@63960
   665
(* normalizing goals *)
boehmes@63960
   666
boehmes@63960
   667
fun instantiate_elim_rule thm =
boehmes@63960
   668
  let val ct = Drule.strip_imp_concl (Thm.cprop_of thm)
boehmes@63960
   669
  in
boehmes@63960
   670
    (case Thm.term_of ct of
boehmes@63960
   671
      @{const HOL.Trueprop} $ Var (_, @{typ HOL.bool}) =>
boehmes@63960
   672
        instantiate (Thm.dest_arg ct) @{cterm HOL.False} thm
boehmes@63960
   673
    | Var _ => instantiate ct @{cprop HOL.False} thm
boehmes@63960
   674
    | _ => thm)
boehmes@63960
   675
  end
boehmes@63960
   676
boehmes@63960
   677
fun atomize_conv ctxt ct =
boehmes@63960
   678
  (case Thm.term_of ct of
boehmes@63960
   679
    @{const HOL.Trueprop} $ _ => Conv.all_conv
boehmes@63960
   680
  | @{const Pure.imp} $ _ $ _ =>
boehmes@63960
   681
      Conv.binop_conv (atomize_conv ctxt) then_conv
boehmes@63960
   682
      Conv.rewr_conv @{thm atomize_imp}
boehmes@63960
   683
  | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
boehmes@63960
   684
      Conv.binop_conv (atomize_conv ctxt) then_conv
boehmes@63960
   685
      Conv.rewr_conv @{thm atomize_eq}
boehmes@63960
   686
  | Const (@{const_name Pure.all}, _) $ Abs _ =>
boehmes@63960
   687
      Conv.binder_conv (atomize_conv o snd) ctxt then_conv
boehmes@63960
   688
      Conv.rewr_conv @{thm atomize_all}
boehmes@63960
   689
  | _ => Conv.all_conv) ct
boehmes@63960
   690
boehmes@63960
   691
fun normalize ctxt thm =
boehmes@63960
   692
  thm
boehmes@63960
   693
  |> instantiate_elim_rule
boehmes@63960
   694
  |> Conv.fconv_rule (Thm.beta_conversion true then_conv Thm.eta_conversion)
boehmes@63960
   695
  |> Drule.forall_intr_vars
boehmes@63960
   696
  |> Conv.fconv_rule (atomize_conv ctxt)
boehmes@63960
   697
boehmes@63960
   698
boehmes@63960
   699
(* prover, tactic and method *)
boehmes@63960
   700
boehmes@63960
   701
datatype result = Satisfiable of term -> bool option | Unsatisfiable
boehmes@63960
   702
boehmes@63960
   703
fun check props ctxt =
boehmes@63960
   704
  (case solve props ctxt of
boehmes@63960
   705
    (Proof _, ctxt') => (Unsatisfiable, ctxt')
boehmes@63960
   706
  | (Model model, ctxt') => (Satisfiable model, ctxt'))
boehmes@63960
   707
boehmes@63960
   708
fun prove thms ctxt =
boehmes@63960
   709
  let val thms' = map (normalize ctxt) thms
boehmes@63960
   710
  in
boehmes@63960
   711
    (case solve (map Thm.prop_of thms') ctxt of
boehmes@63960
   712
      (Model _, ctxt') => (NONE, ctxt')
boehmes@63960
   713
    | (Proof (terms, proof), ctxt') => (SOME (replay ctxt' terms thms' proof), ctxt'))
boehmes@63960
   714
  end
boehmes@63960
   715
boehmes@63960
   716
fun argo_tac ctxt thms =
boehmes@63960
   717
  CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
boehmes@63960
   718
    (Conv.try_conv (Conv.rewr_conv @{thm atomize_eq})))) ctxt)
boehmes@63960
   719
  THEN' Tactic.resolve_tac ctxt [@{thm ccontr}]
boehmes@63960
   720
  THEN' Subgoal.FOCUS (fn {context, prems, ...} =>
boehmes@63960
   721
    (case with_timeout context (prove (thms @ prems)) context of
boehmes@63960
   722
      (SOME thm, _) => Tactic.resolve_tac context [thm] 1
boehmes@63960
   723
    | (NONE, _) => Tactical.no_tac)) ctxt
boehmes@63960
   724
boehmes@63960
   725
val _ =
boehmes@63960
   726
  Theory.setup (Method.setup @{binding argo}
boehmes@63960
   727
    (Scan.optional Attrib.thms [] >>
boehmes@63960
   728
      (fn thms => fn ctxt => METHOD (fn facts =>
boehmes@63960
   729
        HEADGOAL (argo_tac ctxt (thms @ facts)))))
boehmes@63960
   730
    "Applies the Argo prover")
boehmes@63960
   731
boehmes@63960
   732
end