src/HOL/Tools/Metis/metis_reconstruct.ML
author blanchet
Tue Nov 15 22:13:39 2011 +0100 (2011-11-15)
changeset 45511 9b0f8ca4388e
parent 45508 b216dc1b3630
child 45569 eb30a5490543
permissions -rw-r--r--
continued implementation of lambda-lifting in Metis
blanchet@39958
     1
(*  Title:      HOL/Tools/Metis/metis_reconstruct.ML
blanchet@39495
     2
    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
blanchet@39495
     3
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
blanchet@39495
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@39495
     5
    Copyright   Cambridge University 2007
blanchet@39495
     6
blanchet@39495
     7
Proof reconstruction for Metis.
blanchet@39495
     8
*)
blanchet@39495
     9
blanchet@39495
    10
signature METIS_RECONSTRUCT =
blanchet@39495
    11
sig
blanchet@44492
    12
  type type_enc = ATP_Translate.type_enc
blanchet@44492
    13
blanchet@42650
    14
  exception METIS of string * string
blanchet@42650
    15
blanchet@43159
    16
  val hol_clause_from_metis :
blanchet@45508
    17
    Proof.context -> type_enc -> int Symtab.table
blanchet@45508
    18
    -> (string * term) list * (string * term) list -> Metis_Thm.thm -> term
blanchet@39497
    19
  val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
blanchet@39497
    20
  val replay_one_inference :
blanchet@45508
    21
    Proof.context -> type_enc
blanchet@45508
    22
    -> (string * term) list * (string * term) list -> int Symtab.table
blanchet@39497
    23
    -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list
blanchet@39497
    24
    -> (Metis_Thm.thm * thm) list
blanchet@39964
    25
  val discharge_skolem_premises :
blanchet@39964
    26
    Proof.context -> (thm * term) option list -> thm -> thm
blanchet@39495
    27
end;
blanchet@39495
    28
blanchet@39495
    29
structure Metis_Reconstruct : METIS_RECONSTRUCT =
blanchet@39495
    30
struct
blanchet@39495
    31
blanchet@43094
    32
open ATP_Problem
blanchet@43085
    33
open ATP_Translate
blanchet@43094
    34
open ATP_Reconstruct
blanchet@39497
    35
open Metis_Translate
blanchet@39497
    36
blanchet@42650
    37
exception METIS of string * string
blanchet@42650
    38
blanchet@44492
    39
fun atp_name_from_metis type_enc s =
blanchet@44492
    40
  case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
blanchet@43104
    41
    SOME ((s, _), (_, swap)) => (s, swap)
blanchet@43104
    42
  | _ => (s, false)
blanchet@44492
    43
fun atp_term_from_metis type_enc (Metis_Term.Fn (s, tms)) =
blanchet@44492
    44
    let val (s, swap) = atp_name_from_metis type_enc (Metis_Name.toString s) in
blanchet@44492
    45
      ATerm (s, tms |> map (atp_term_from_metis type_enc) |> swap ? rev)
blanchet@43104
    46
    end
blanchet@44492
    47
  | atp_term_from_metis _ (Metis_Term.Var s) = ATerm (Metis_Name.toString s, [])
blanchet@39497
    48
blanchet@44492
    49
fun hol_term_from_metis ctxt type_enc sym_tab =
blanchet@44492
    50
  atp_term_from_metis type_enc #> term_from_atp ctxt false sym_tab NONE
blanchet@43094
    51
blanchet@44492
    52
fun atp_literal_from_metis type_enc (pos, atom) =
blanchet@44492
    53
  atom |> Metis_Term.Fn |> atp_term_from_metis type_enc
blanchet@44492
    54
       |> AAtom |> not pos ? mk_anot
blanchet@44492
    55
fun atp_clause_from_metis _ [] = AAtom (ATerm (tptp_false, []))
blanchet@44492
    56
  | atp_clause_from_metis type_enc lits =
blanchet@44492
    57
    lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
blanchet@43136
    58
blanchet@45508
    59
fun polish_hol_terms ctxt (lifted, old_skolems) =
blanchet@45511
    60
  map (reveal_lambda_lifted lifted #> reveal_old_skolem_terms old_skolems)
blanchet@43212
    61
  #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
blanchet@43184
    62
blanchet@45508
    63
fun hol_clause_from_metis ctxt type_enc sym_tab concealed =
blanchet@43159
    64
  Metis_Thm.clause
blanchet@43159
    65
  #> Metis_LiteralSet.toList
blanchet@44492
    66
  #> atp_clause_from_metis type_enc
blanchet@43159
    67
  #> prop_from_atp ctxt false sym_tab
blanchet@45508
    68
  #> singleton (polish_hol_terms ctxt concealed)
blanchet@43136
    69
blanchet@45508
    70
fun hol_terms_from_metis ctxt type_enc concealed sym_tab fol_tms =
blanchet@44492
    71
  let val ts = map (hol_term_from_metis ctxt type_enc sym_tab) fol_tms
blanchet@39978
    72
      val _ = trace_msg ctxt (fn () => "  calling type inference:")
blanchet@39978
    73
      val _ = app (fn t => trace_msg ctxt
blanchet@39978
    74
                                     (fn () => Syntax.string_of_term ctxt t)) ts
blanchet@45508
    75
      val ts' = ts |> polish_hol_terms ctxt concealed
blanchet@39978
    76
      val _ = app (fn t => trace_msg ctxt
blanchet@39497
    77
                    (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
blanchet@43128
    78
                              " of type " ^ Syntax.string_of_typ ctxt (type_of t)))
blanchet@39497
    79
                  ts'
blanchet@39497
    80
  in  ts'  end;
blanchet@39497
    81
blanchet@39497
    82
(* ------------------------------------------------------------------------- *)
blanchet@39497
    83
(* FOL step Inference Rules                                                  *)
blanchet@39497
    84
(* ------------------------------------------------------------------------- *)
blanchet@39497
    85
blanchet@39497
    86
(*for debugging only*)
blanchet@39497
    87
(*
blanchet@39978
    88
fun print_thpair ctxt (fth,th) =
blanchet@39978
    89
  (trace_msg ctxt (fn () => "=============================================");
blanchet@39978
    90
   trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth);
blanchet@39978
    91
   trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
blanchet@39497
    92
*)
blanchet@39497
    93
blanchet@43094
    94
fun lookth th_pairs fth =
blanchet@43094
    95
  the (AList.lookup (uncurry Metis_Thm.equal) th_pairs fth)
blanchet@39497
    96
  handle Option.Option =>
blanchet@39497
    97
         raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth)
blanchet@39497
    98
blanchet@39497
    99
fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
blanchet@39497
   100
blanchet@39497
   101
(* INFERENCE RULE: AXIOM *)
blanchet@39497
   102
blanchet@43212
   103
(* This causes variables to have an index of 1 by default. See also
blanchet@43212
   104
   "term_from_atp" in "ATP_Reconstruct". *)
blanchet@43212
   105
val axiom_inference = Thm.incr_indexes 1 oo lookth
blanchet@39497
   106
blanchet@39497
   107
(* INFERENCE RULE: ASSUME *)
blanchet@39497
   108
blanchet@39497
   109
val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
blanchet@39497
   110
blanchet@43187
   111
fun inst_excluded_middle thy i_atom =
blanchet@39497
   112
  let val th = EXCLUDED_MIDDLE
blanchet@39497
   113
      val [vx] = Term.add_vars (prop_of th) []
blanchet@43187
   114
      val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
blanchet@39497
   115
  in  cterm_instantiate substs th  end;
blanchet@39497
   116
blanchet@45508
   117
fun assume_inference ctxt type_enc concealed sym_tab atom =
blanchet@39497
   118
  inst_excluded_middle
wenzelm@42361
   119
      (Proof_Context.theory_of ctxt)
blanchet@45508
   120
      (singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab)
blanchet@43187
   121
                 (Metis_Term.Fn atom))
blanchet@39497
   122
blanchet@39498
   123
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
blanchet@39497
   124
   to reconstruct them admits new possibilities of errors, e.g. concerning
blanchet@39497
   125
   sorts. Instead we try to arrange that new TVars are distinct and that types
blanchet@39498
   126
   can be inferred from terms. *)
blanchet@39497
   127
blanchet@45508
   128
fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th =
wenzelm@42361
   129
  let val thy = Proof_Context.theory_of ctxt
blanchet@43094
   130
      val i_th = lookth th_pairs th
blanchet@39497
   131
      val i_th_vars = Term.add_vars (prop_of i_th) []
blanchet@39497
   132
      fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
blanchet@39497
   133
      fun subst_translation (x,y) =
blanchet@39498
   134
        let val v = find_var x
blanchet@45508
   135
            (* We call "polish_hol_terms" below. *)
blanchet@44492
   136
            val t = hol_term_from_metis ctxt type_enc sym_tab y
blanchet@39498
   137
        in  SOME (cterm_of thy (Var v), t)  end
blanchet@39498
   138
        handle Option.Option =>
blanchet@39978
   139
               (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
blanchet@39978
   140
                                         " in " ^ Display.string_of_thm ctxt i_th);
blanchet@39498
   141
                NONE)
blanchet@39498
   142
             | TYPE _ =>
blanchet@39978
   143
               (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
blanchet@39978
   144
                                         " in " ^ Display.string_of_thm ctxt i_th);
blanchet@39498
   145
                NONE)
blanchet@39497
   146
      fun remove_typeinst (a, t) =
blanchet@43268
   147
        let val a = Metis_Name.toString a in
blanchet@45511
   148
          case unprefix_and_unascii schematic_var_prefix a of
blanchet@43268
   149
            SOME b => SOME (b, t)
blanchet@43268
   150
          | NONE =>
blanchet@45511
   151
            case unprefix_and_unascii tvar_prefix a of
blanchet@43268
   152
              SOME _ => NONE (* type instantiations are forbidden *)
blanchet@43268
   153
            | NONE => SOME (a, t) (* internal Metis var? *)
blanchet@43268
   154
        end
blanchet@39978
   155
      val _ = trace_msg ctxt (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
blanchet@39497
   156
      val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
blanchet@43184
   157
      val (vars, tms) =
blanchet@43184
   158
        ListPair.unzip (map_filter subst_translation substs)
blanchet@45508
   159
        ||> polish_hol_terms ctxt concealed
blanchet@39497
   160
      val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
blanchet@39497
   161
      val substs' = ListPair.zip (vars, map ctm_of tms)
blanchet@39978
   162
      val _ = trace_msg ctxt (fn () =>
blanchet@39497
   163
        cat_lines ("subst_translations:" ::
blanchet@39497
   164
          (substs' |> map (fn (x, y) =>
blanchet@39497
   165
            Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
blanchet@39497
   166
            Syntax.string_of_term ctxt (term_of y)))));
blanchet@39497
   167
  in cterm_instantiate substs' i_th end
blanchet@43186
   168
  handle THM (msg, _, _) => raise METIS ("inst_inference", msg)
blanchet@43186
   169
       | ERROR msg => raise METIS ("inst_inference", msg)
blanchet@39497
   170
blanchet@39497
   171
(* INFERENCE RULE: RESOLVE *)
blanchet@39497
   172
wenzelm@43330
   173
(*Increment the indexes of only the type variables*)
wenzelm@43330
   174
fun incr_type_indexes inc th =
wenzelm@43330
   175
  let val tvs = Term.add_tvars (Thm.full_prop_of th) []
wenzelm@43330
   176
      and thy = Thm.theory_of_thm th
wenzelm@43330
   177
      fun inc_tvar ((a,i),s) = pairself (ctyp_of thy) (TVar ((a,i),s), TVar ((a,i+inc),s))
wenzelm@43330
   178
  in Thm.instantiate (map inc_tvar tvs, []) th end;
wenzelm@43330
   179
blanchet@39497
   180
(* Like RSN, but we rename apart only the type variables. Vars here typically
blanchet@39497
   181
   have an index of 1, and the use of RSN would increase this typically to 3.
blanchet@43300
   182
   Instantiations of those Vars could then fail. *)
blanchet@39497
   183
fun resolve_inc_tyvars thy tha i thb =
blanchet@39497
   184
  let
wenzelm@43330
   185
    val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
blanchet@43359
   186
    fun aux (tha, thb) =
blanchet@39497
   187
      case Thm.bicompose false (false, tha, nprems_of tha) i thb
blanchet@39497
   188
           |> Seq.list_of |> distinct Thm.eq_thm of
blanchet@39497
   189
        [th] => th
blanchet@39497
   190
      | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
blanchet@39497
   191
                        [tha, thb])
blanchet@39497
   192
  in
blanchet@43359
   193
    aux (tha, thb)
blanchet@39497
   194
    handle TERM z =>
blanchet@39497
   195
           (* The unifier, which is invoked from "Thm.bicompose", will sometimes
blanchet@39497
   196
              refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
blanchet@39497
   197
              "TERM" exception (with "add_ffpair" as first argument). We then
blanchet@39497
   198
              perform unification of the types of variables by hand and try
blanchet@39497
   199
              again. We could do this the first time around but this error
blanchet@39497
   200
              occurs seldom and we don't want to break existing proofs in subtle
blanchet@39497
   201
              ways or slow them down needlessly. *)
blanchet@39497
   202
           case [] |> fold (Term.add_vars o prop_of) [tha, thb]
blanchet@39497
   203
                   |> AList.group (op =)
blanchet@39497
   204
                   |> maps (fn ((s, _), T :: Ts) =>
blanchet@39497
   205
                               map (fn T' => (Free (s, T), Free (s, T'))) Ts)
blanchet@39497
   206
                   |> rpair (Envir.empty ~1)
blanchet@39497
   207
                   |-> fold (Pattern.unify thy)
blanchet@39497
   208
                   |> Envir.type_env |> Vartab.dest
blanchet@39497
   209
                   |> map (fn (x, (S, T)) =>
blanchet@39497
   210
                              pairself (ctyp_of thy) (TVar (x, S), T)) of
blanchet@39497
   211
             [] => raise TERM z
blanchet@43359
   212
           | ps => (tha, thb) |> pairself (Drule.instantiate_normalize (ps, []))
blanchet@43359
   213
                              |> aux
blanchet@39497
   214
  end
blanchet@39497
   215
blanchet@40221
   216
fun s_not (@{const Not} $ t) = t
blanchet@40221
   217
  | s_not t = HOLogic.mk_not t
blanchet@43195
   218
fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t
blanchet@43195
   219
  | simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
blanchet@40221
   220
  | simp_not_not t = t
blanchet@39497
   221
blanchet@43195
   222
val normalize_literal = simp_not_not o Envir.eta_contract
blanchet@43195
   223
blanchet@43187
   224
(* Find the relative location of an untyped term within a list of terms as a
blanchet@43187
   225
   1-based index. Returns 0 in case of failure. *)
blanchet@40221
   226
fun index_of_literal lit haystack =
blanchet@39497
   227
  let
blanchet@43195
   228
    fun match_lit normalize =
blanchet@43134
   229
      HOLogic.dest_Trueprop #> normalize
blanchet@43301
   230
      #> curry Term.aconv_untyped (lit |> normalize)
blanchet@43195
   231
  in
blanchet@43195
   232
    (case find_index (match_lit I) haystack of
blanchet@43195
   233
       ~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack
blanchet@43195
   234
     | j => j) + 1
blanchet@43195
   235
  end
blanchet@39497
   236
blanchet@39893
   237
(* Permute a rule's premises to move the i-th premise to the last position. *)
blanchet@39893
   238
fun make_last i th =
blanchet@39893
   239
  let val n = nprems_of th
blanchet@39893
   240
  in  if 1 <= i andalso i <= n
blanchet@39893
   241
      then Thm.permute_prems (i-1) 1 th
blanchet@39893
   242
      else raise THM("select_literal", i, [th])
blanchet@39893
   243
  end;
blanchet@39893
   244
blanchet@42348
   245
(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
blanchet@42349
   246
   to create double negations. The "select" wrapper is a trick to ensure that
blanchet@42349
   247
   "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
blanchet@42349
   248
   don't use this trick in general because it makes the proof object uglier than
blanchet@42349
   249
   necessary. FIXME. *)
blanchet@42349
   250
fun negate_head th =
blanchet@42349
   251
  if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then
blanchet@42349
   252
    (th RS @{thm select_FalseI})
blanchet@42349
   253
    |> fold (rewrite_rule o single)
blanchet@42349
   254
            @{thms not_atomize_select atomize_not_select}
blanchet@42349
   255
  else
blanchet@42349
   256
    th |> fold (rewrite_rule o single) @{thms not_atomize atomize_not}
blanchet@39893
   257
blanchet@39893
   258
(* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
blanchet@42348
   259
val select_literal = negate_head oo make_last
blanchet@39893
   260
blanchet@45508
   261
fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 =
blanchet@39497
   262
  let
blanchet@43094
   263
    val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
blanchet@43187
   264
    val _ = trace_msg ctxt (fn () =>
blanchet@43187
   265
        "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\
blanchet@43187
   266
        \  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
blanchet@39497
   267
  in
blanchet@39497
   268
    (* Trivial cases where one operand is type info *)
blanchet@39497
   269
    if Thm.eq_thm (TrueI, i_th1) then
blanchet@39497
   270
      i_th2
blanchet@39497
   271
    else if Thm.eq_thm (TrueI, i_th2) then
blanchet@39497
   272
      i_th1
blanchet@39497
   273
    else
blanchet@39497
   274
      let
blanchet@43187
   275
        val thy = Proof_Context.theory_of ctxt
blanchet@43187
   276
        val i_atom =
blanchet@45508
   277
          singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab)
blanchet@43187
   278
                    (Metis_Term.Fn atom)
blanchet@43187
   279
        val _ = trace_msg ctxt (fn () =>
blanchet@43187
   280
                    "  atom: " ^ Syntax.string_of_term ctxt i_atom)
blanchet@43187
   281
      in
blanchet@43187
   282
        case index_of_literal (s_not i_atom) (prems_of i_th1) of
blanchet@43187
   283
          0 =>
blanchet@43187
   284
          (trace_msg ctxt (fn () => "Failed to find literal in \"th1\"");
blanchet@43187
   285
           i_th1)
blanchet@43187
   286
        | j1 =>
blanchet@43187
   287
          (trace_msg ctxt (fn () => "  index th1: " ^ string_of_int j1);
blanchet@43187
   288
           case index_of_literal i_atom (prems_of i_th2) of
blanchet@43187
   289
             0 =>
blanchet@43187
   290
             (trace_msg ctxt (fn () => "Failed to find literal in \"th2\"");
blanchet@43187
   291
              i_th2)
blanchet@43187
   292
           | j2 =>
blanchet@43187
   293
             (trace_msg ctxt (fn () => "  index th2: " ^ string_of_int j2);
blanchet@43187
   294
              resolve_inc_tyvars thy (select_literal j1 i_th1) j2 i_th2
blanchet@43187
   295
              handle TERM (s, _) => raise METIS ("resolve_inference", s)))
blanchet@43187
   296
      end
blanchet@43187
   297
  end
blanchet@39497
   298
blanchet@39497
   299
(* INFERENCE RULE: REFL *)
blanchet@39497
   300
blanchet@39497
   301
val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
blanchet@39497
   302
blanchet@39497
   303
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
blanchet@39497
   304
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
blanchet@39497
   305
blanchet@45508
   306
fun refl_inference ctxt type_enc concealed sym_tab t =
blanchet@43094
   307
  let
blanchet@43094
   308
    val thy = Proof_Context.theory_of ctxt
blanchet@44492
   309
    val i_t =
blanchet@45508
   310
      singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab) t
blanchet@43094
   311
    val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
blanchet@43094
   312
    val c_t = cterm_incr_types thy refl_idx i_t
blanchet@43094
   313
  in cterm_instantiate [(refl_x, c_t)] REFL_THM end
blanchet@39497
   314
blanchet@39497
   315
(* INFERENCE RULE: EQUALITY *)
blanchet@39497
   316
blanchet@39497
   317
val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
blanchet@39497
   318
val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
blanchet@39497
   319
blanchet@45508
   320
fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr =
wenzelm@42361
   321
  let val thy = Proof_Context.theory_of ctxt
blanchet@43187
   322
      val m_tm = Metis_Term.Fn atom
blanchet@43187
   323
      val [i_atom, i_tm] =
blanchet@45508
   324
        hol_terms_from_metis ctxt type_enc concealed sym_tab [m_tm, fr]
blanchet@39978
   325
      val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
blanchet@39497
   326
      fun replace_item_list lx 0 (_::ls) = lx::ls
blanchet@39497
   327
        | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
blanchet@43205
   328
      fun path_finder_fail tm ps t =
blanchet@43209
   329
        raise METIS ("equality_inference (path_finder)",
blanchet@43209
   330
                     "path = " ^ space_implode " " (map string_of_int ps) ^
blanchet@43209
   331
                     " isa-term: " ^ Syntax.string_of_term ctxt tm ^
blanchet@43209
   332
                     (case t of
blanchet@43209
   333
                        SOME t => " fol-term: " ^ Metis_Term.toString t
blanchet@43209
   334
                      | NONE => ""))
blanchet@43212
   335
      fun path_finder tm [] _ = (tm, Bound 0)
blanchet@43212
   336
        | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
blanchet@43177
   337
          let
blanchet@43268
   338
            val s = s |> Metis_Name.toString
blanchet@45511
   339
                      |> perhaps (try (unprefix_and_unascii const_prefix
blanchet@43177
   340
                                       #> the #> unmangled_const_name))
blanchet@43177
   341
          in
blanchet@43177
   342
            if s = metis_predicator orelse s = predicator_name orelse
blanchet@44492
   343
               s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag
blanchet@44492
   344
               orelse s = type_tag_name then
blanchet@43212
   345
              path_finder tm ps (nth ts p)
blanchet@43177
   346
            else if s = metis_app_op orelse s = app_op_name then
blanchet@43130
   347
              let
blanchet@43130
   348
                val (tm1, tm2) = dest_comb tm
blanchet@43130
   349
                val p' = p - (length ts - 2)
blanchet@43130
   350
              in
blanchet@43130
   351
                if p' = 0 then
blanchet@43212
   352
                  path_finder tm1 ps (nth ts p) ||> (fn y => y $ tm2)
blanchet@43130
   353
                else
blanchet@43212
   354
                  path_finder tm2 ps (nth ts p) ||> (fn y => tm1 $ y)
blanchet@43130
   355
              end
blanchet@43130
   356
            else
blanchet@43130
   357
              let
blanchet@43130
   358
                val (tm1, args) = strip_comb tm
blanchet@43130
   359
                val adjustment = length ts - length args
blanchet@43130
   360
                val p' = if adjustment > p then p else p - adjustment
blanchet@43205
   361
                val tm_p =
blanchet@43205
   362
                  nth args p'
wenzelm@43278
   363
                  handle General.Subscript => path_finder_fail tm (p :: ps) (SOME t)
blanchet@43130
   364
                val _ = trace_msg ctxt (fn () =>
blanchet@43130
   365
                    "path_finder: " ^ string_of_int p ^ "  " ^
blanchet@43130
   366
                    Syntax.string_of_term ctxt tm_p)
blanchet@43212
   367
                val (r, t) = path_finder tm_p ps (nth ts p)
blanchet@43130
   368
              in (r, list_comb (tm1, replace_item_list t p' args)) end
blanchet@43130
   369
          end
blanchet@43212
   370
        | path_finder tm ps t = path_finder_fail tm ps (SOME t)
blanchet@43212
   371
      val (tm_subst, body) = path_finder i_atom fp m_tm
blanchet@39498
   372
      val tm_abs = Abs ("x", type_of tm_subst, body)
blanchet@39978
   373
      val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
blanchet@39978
   374
      val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
blanchet@39978
   375
      val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
blanchet@39497
   376
      val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
blanchet@39497
   377
      val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
blanchet@39978
   378
      val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
blanchet@39497
   379
      val eq_terms = map (pairself (cterm_of thy))
wenzelm@44121
   380
        (ListPair.zip (Misc_Legacy.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
blanchet@39497
   381
  in  cterm_instantiate eq_terms subst'  end;
blanchet@39497
   382
blanchet@43094
   383
val factor = Seq.hd o distinct_subgoals_tac
blanchet@39497
   384
blanchet@45508
   385
fun one_step ctxt type_enc concealed sym_tab th_pairs p =
blanchet@39497
   386
  case p of
blanchet@43186
   387
    (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
blanchet@43187
   388
  | (_, Metis_Proof.Assume f_atom) =>
blanchet@45508
   389
    assume_inference ctxt type_enc concealed sym_tab f_atom
blanchet@39497
   390
  | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
blanchet@45508
   391
    inst_inference ctxt type_enc concealed sym_tab th_pairs f_subst f_th1
blanchet@43186
   392
    |> factor
blanchet@43187
   393
  | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
blanchet@45508
   394
    resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1
blanchet@44492
   395
                      f_th2
blanchet@43094
   396
    |> factor
blanchet@43186
   397
  | (_, Metis_Proof.Refl f_tm) =>
blanchet@45508
   398
    refl_inference ctxt type_enc concealed sym_tab f_tm
blanchet@39497
   399
  | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
blanchet@45508
   400
    equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r
blanchet@39497
   401
blanchet@39893
   402
fun flexflex_first_order th =
blanchet@39893
   403
  case Thm.tpairs_of th of
blanchet@39893
   404
      [] => th
blanchet@39893
   405
    | pairs =>
blanchet@39893
   406
        let val thy = theory_of_thm th
blanchet@39893
   407
            val (_, tenv) =
blanchet@39893
   408
              fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
blanchet@39893
   409
            val t_pairs = map Meson.term_pair_of (Vartab.dest tenv)
blanchet@39893
   410
            val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
blanchet@39893
   411
        in  th'  end
blanchet@39893
   412
        handle THM _ => th;
blanchet@39497
   413
blanchet@43268
   414
fun is_metis_literal_genuine (_, (s, _)) =
blanchet@43268
   415
  not (String.isPrefix class_prefix (Metis_Name.toString s))
blanchet@39895
   416
fun is_isabelle_literal_genuine t =
blanchet@39953
   417
  case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
blanchet@39895
   418
blanchet@39895
   419
fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
blanchet@39895
   420
blanchet@42333
   421
(* Seldomly needed hack. A Metis clause is represented as a set, so duplicate
blanchet@42333
   422
   disjuncts are impossible. In the Isabelle proof, in spite of efforts to
blanchet@42333
   423
   eliminate them, duplicates sometimes appear with slightly different (but
blanchet@42333
   424
   unifiable) types. *)
blanchet@42333
   425
fun resynchronize ctxt fol_th th =
blanchet@42333
   426
  let
blanchet@42333
   427
    val num_metis_lits =
blanchet@42333
   428
      count is_metis_literal_genuine
blanchet@42333
   429
            (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))
blanchet@42333
   430
    val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th)
blanchet@42333
   431
  in
blanchet@42333
   432
    if num_metis_lits >= num_isabelle_lits then
blanchet@42333
   433
      th
blanchet@42333
   434
    else
blanchet@42333
   435
      let
blanchet@42333
   436
        val (prems0, concl) = th |> prop_of |> Logic.strip_horn
blanchet@43195
   437
        val prems = prems0 |> map normalize_literal
blanchet@43301
   438
                           |> distinct Term.aconv_untyped
blanchet@42333
   439
        val goal = Logic.list_implies (prems, concl)
blanchet@43195
   440
        val tac = cut_rules_tac [th] 1
blanchet@43195
   441
                  THEN rewrite_goals_tac @{thms not_not [THEN eq_reflection]}
blanchet@43195
   442
                  THEN ALLGOALS assume_tac
blanchet@42333
   443
      in
blanchet@42333
   444
        if length prems = length prems0 then
blanchet@42650
   445
          raise METIS ("resynchronize", "Out of sync")
blanchet@42333
   446
        else
blanchet@43195
   447
          Goal.prove ctxt [] [] goal (K tac)
blanchet@42333
   448
          |> resynchronize ctxt fol_th
blanchet@42333
   449
      end
blanchet@42333
   450
  end
blanchet@42333
   451
blanchet@45508
   452
fun replay_one_inference ctxt type_enc concealed sym_tab (fol_th, inf)
blanchet@44492
   453
                         th_pairs =
blanchet@43094
   454
  if not (null th_pairs) andalso
blanchet@43094
   455
     prop_of (snd (hd th_pairs)) aconv @{prop False} then
blanchet@40868
   456
    (* Isabelle sometimes identifies literals (premises) that are distinct in
blanchet@40868
   457
       Metis (e.g., because of type variables). We give the Isabelle proof the
blanchet@40868
   458
       benefice of the doubt. *)
blanchet@43094
   459
    th_pairs
blanchet@40868
   460
  else
blanchet@40868
   461
    let
blanchet@40868
   462
      val _ = trace_msg ctxt
blanchet@40868
   463
                  (fn () => "=============================================")
blanchet@40868
   464
      val _ = trace_msg ctxt
blanchet@40868
   465
                  (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
blanchet@40868
   466
      val _ = trace_msg ctxt
blanchet@40868
   467
                  (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
blanchet@45508
   468
      val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf)
blanchet@40868
   469
               |> flexflex_first_order
blanchet@42333
   470
               |> resynchronize ctxt fol_th
blanchet@40868
   471
      val _ = trace_msg ctxt
blanchet@40868
   472
                  (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
blanchet@40868
   473
      val _ = trace_msg ctxt
blanchet@40868
   474
                  (fn () => "=============================================")
blanchet@43094
   475
    in (fol_th, th) :: th_pairs end
blanchet@39497
   476
blanchet@42342
   477
(* It is normally sufficient to apply "assume_tac" to unify the conclusion with
blanchet@42342
   478
   one of the premises. Unfortunately, this sometimes yields "Variable
blanchet@42342
   479
   ?SK_a_b_c_x has two distinct types" errors. To avoid this, we instantiate the
blanchet@42342
   480
   variables before applying "assume_tac". Typical constraints are of the form
blanchet@42342
   481
     ?SK_a_b_c_x SK_d_e_f_y ... SK_a_b_c_x ... SK_g_h_i_z =?= SK_a_b_c_x,
blanchet@42342
   482
   where the nonvariables are goal parameters. *)
blanchet@42342
   483
fun unify_first_prem_with_concl thy i th =
blanchet@42342
   484
  let
blanchet@42342
   485
    val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
blanchet@42342
   486
    val prem = goal |> Logic.strip_assums_hyp |> hd
blanchet@42342
   487
    val concl = goal |> Logic.strip_assums_concl
blanchet@42342
   488
    fun pair_untyped_aconv (t1, t2) (u1, u2) =
blanchet@43301
   489
      Term.aconv_untyped (t1, u1) andalso Term.aconv_untyped (t2, u2)
blanchet@42342
   490
    fun add_terms tp inst =
blanchet@42342
   491
      if exists (pair_untyped_aconv tp) inst then inst
blanchet@42342
   492
      else tp :: map (apsnd (subst_atomic [tp])) inst
blanchet@42342
   493
    fun is_flex t =
blanchet@42342
   494
      case strip_comb t of
blanchet@42342
   495
        (Var _, args) => forall is_Bound args
blanchet@42342
   496
      | _ => false
blanchet@42342
   497
    fun unify_flex flex rigid =
blanchet@42342
   498
      case strip_comb flex of
blanchet@42342
   499
        (Var (z as (_, T)), args) =>
blanchet@42342
   500
        add_terms (Var z,
wenzelm@44241
   501
          fold_rev absdummy (take (length args) (binder_types T)) rigid)
blanchet@42342
   502
      | _ => I
blanchet@42342
   503
    fun unify_potential_flex comb atom =
blanchet@42342
   504
      if is_flex comb then unify_flex comb atom
blanchet@42342
   505
      else if is_Var atom then add_terms (atom, comb)
blanchet@42342
   506
      else I
blanchet@42342
   507
    fun unify_terms (t, u) =
blanchet@42342
   508
      case (t, u) of
blanchet@42342
   509
        (t1 $ t2, u1 $ u2) =>
blanchet@42342
   510
        if is_flex t then unify_flex t u
blanchet@42342
   511
        else if is_flex u then unify_flex u t
blanchet@42342
   512
        else fold unify_terms [(t1, u1), (t2, u2)]
blanchet@42342
   513
      | (_ $ _, _) => unify_potential_flex t u
blanchet@42342
   514
      | (_, _ $ _) => unify_potential_flex u t
blanchet@42342
   515
      | (Var _, _) => add_terms (t, u)
blanchet@42342
   516
      | (_, Var _) => add_terms (u, t)
blanchet@42342
   517
      | _ => I
blanchet@42344
   518
    val t_inst =
blanchet@42344
   519
      [] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy)))
blanchet@42344
   520
         |> the_default [] (* FIXME *)
blanchet@42342
   521
  in th |> cterm_instantiate t_inst end
blanchet@39964
   522
blanchet@39964
   523
val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
blanchet@39964
   524
blanchet@39964
   525
fun copy_prems_tac [] ns i =
blanchet@39964
   526
    if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
blanchet@39964
   527
  | copy_prems_tac (1 :: ms) ns i =
blanchet@39964
   528
    rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
blanchet@39964
   529
  | copy_prems_tac (m :: ms) ns i =
blanchet@39964
   530
    etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
blanchet@39964
   531
blanchet@42271
   532
(* Metis generates variables of the form _nnn. *)
blanchet@42271
   533
val is_metis_fresh_variable = String.isPrefix "_"
blanchet@42271
   534
blanchet@40258
   535
fun instantiate_forall_tac thy t i st =
blanchet@39964
   536
  let
blanchet@40258
   537
    val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
blanchet@39964
   538
    fun repair (t as (Var ((s, _), _))) =
blanchet@40258
   539
        (case find_index (fn (s', _) => s' = s) params of
blanchet@39964
   540
           ~1 => t
blanchet@39964
   541
         | j => Bound j)
blanchet@40261
   542
      | repair (t $ u) =
blanchet@40261
   543
        (case (repair t, repair u) of
blanchet@40261
   544
           (t as Bound j, u as Bound k) =>
blanchet@40261
   545
           (* This is a rather subtle trick to repair the discrepancy between
blanchet@40261
   546
              the fully skolemized term that MESON gives us (where existentials
blanchet@40261
   547
              were pulled out) and the reality. *)
blanchet@40261
   548
           if k > j then t else t $ u
blanchet@40261
   549
         | (t, u) => t $ u)
blanchet@39964
   550
      | repair t = t
wenzelm@44241
   551
    val t' = t |> repair |> fold (absdummy o snd) params
blanchet@39964
   552
    fun do_instantiate th =
blanchet@42270
   553
      case Term.add_vars (prop_of th) []
blanchet@42271
   554
           |> filter_out ((Meson_Clausify.is_zapped_var_name orf
blanchet@42271
   555
                           is_metis_fresh_variable) o fst o fst) of
blanchet@42270
   556
        [] => th
blanchet@42271
   557
      | [var as (_, T)] =>
blanchet@42271
   558
        let
blanchet@42271
   559
          val var_binder_Ts = T |> binder_types |> take (length params) |> rev
blanchet@42271
   560
          val var_body_T = T |> funpow (length params) range_type
blanchet@42271
   561
          val tyenv =
blanchet@42271
   562
            Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params,
blanchet@42271
   563
                                             var_body_T :: var_binder_Ts)
blanchet@42271
   564
          val env =
blanchet@42271
   565
            Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
blanchet@42271
   566
                         tenv = Vartab.empty, tyenv = tyenv}
blanchet@42271
   567
          val ty_inst =
blanchet@42271
   568
            Vartab.fold (fn (x, (S, T)) =>
blanchet@42271
   569
                            cons (pairself (ctyp_of thy) (TVar (x, S), T)))
blanchet@42271
   570
                        tyenv []
blanchet@42271
   571
          val t_inst =
blanchet@42271
   572
            [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
wenzelm@43333
   573
        in th |> Drule.instantiate_normalize (ty_inst, t_inst) end
blanchet@42271
   574
      | _ => raise Fail "expected a single non-zapped, non-Metis Var"
blanchet@39964
   575
  in
blanchet@42271
   576
    (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i)
blanchet@40258
   577
     THEN PRIMITIVE do_instantiate) st
blanchet@39964
   578
  end
blanchet@39964
   579
blanchet@41135
   580
fun fix_exists_tac t =
blanchet@43162
   581
  etac @{thm exE} THEN' rename_tac [t |> dest_Var |> fst |> fst]
blanchet@40261
   582
blanchet@40261
   583
fun release_quantifier_tac thy (skolem, t) =
blanchet@41135
   584
  (if skolem then fix_exists_tac else instantiate_forall_tac thy) t
blanchet@40261
   585
blanchet@40258
   586
fun release_clusters_tac _ _ _ [] = K all_tac
blanchet@40258
   587
  | release_clusters_tac thy ax_counts substs
blanchet@39964
   588
                         ((ax_no, cluster_no) :: clusters) =
blanchet@39964
   589
    let
blanchet@40261
   590
      val cluster_of_var =
blanchet@40261
   591
        Meson_Clausify.cluster_of_zapped_var_name o fst o fst o dest_Var
blanchet@40261
   592
      fun in_right_cluster ((_, (cluster_no', _)), _) = cluster_no' = cluster_no
blanchet@39964
   593
      val cluster_substs =
blanchet@39964
   594
        substs
blanchet@39964
   595
        |> map_filter (fn (ax_no', (_, (_, tsubst))) =>
blanchet@39964
   596
                          if ax_no' = ax_no then
blanchet@40261
   597
                            tsubst |> map (apfst cluster_of_var)
blanchet@40261
   598
                                   |> filter (in_right_cluster o fst)
blanchet@40261
   599
                                   |> map (apfst snd)
blanchet@40261
   600
                                   |> SOME
blanchet@40261
   601
                          else
blanchet@40261
   602
                            NONE)
blanchet@39964
   603
      fun do_cluster_subst cluster_subst =
blanchet@40261
   604
        map (release_quantifier_tac thy) cluster_subst @ [rotate_tac 1]
blanchet@39964
   605
      val first_prem = find_index (fn (ax_no', _) => ax_no' = ax_no) substs
blanchet@39964
   606
    in
blanchet@39964
   607
      rotate_tac first_prem
blanchet@39964
   608
      THEN' (EVERY' (maps do_cluster_subst cluster_substs))
blanchet@39964
   609
      THEN' rotate_tac (~ first_prem - length cluster_substs)
blanchet@40258
   610
      THEN' release_clusters_tac thy ax_counts substs clusters
blanchet@39964
   611
    end
blanchet@39964
   612
blanchet@40264
   613
fun cluster_key ((ax_no, (cluster_no, index_no)), skolem) =
blanchet@40264
   614
  (ax_no, (cluster_no, (skolem, index_no)))
blanchet@40264
   615
fun cluster_ord p =
blanchet@40264
   616
  prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord))
blanchet@40264
   617
           (pairself cluster_key p)
blanchet@39964
   618
blanchet@39964
   619
val tysubst_ord =
blanchet@39964
   620
  list_ord (prod_ord Term_Ord.fast_indexname_ord
blanchet@39964
   621
                     (prod_ord Term_Ord.sort_ord Term_Ord.typ_ord))
blanchet@39964
   622
blanchet@39964
   623
structure Int_Tysubst_Table =
blanchet@39964
   624
  Table(type key = int * (indexname * (sort * typ)) list
blanchet@39964
   625
        val ord = prod_ord int_ord tysubst_ord)
blanchet@39964
   626
blanchet@39964
   627
structure Int_Pair_Graph =
blanchet@39964
   628
  Graph(type key = int * int val ord = prod_ord int_ord int_ord)
blanchet@39964
   629
blanchet@42271
   630
fun shuffle_key (((axiom_no, (_, index_no)), _), _) = (axiom_no, index_no)
blanchet@40258
   631
fun shuffle_ord p = prod_ord int_ord int_ord (pairself shuffle_key p)
blanchet@40258
   632
blanchet@39964
   633
(* Attempts to derive the theorem "False" from a theorem of the form
blanchet@39964
   634
   "P1 ==> ... ==> Pn ==> False", where the "Pi"s are to be discharged using the
blanchet@39964
   635
   specified axioms. The axioms have leading "All" and "Ex" quantifiers, which
blanchet@39964
   636
   must be eliminated first. *)
blanchet@39964
   637
fun discharge_skolem_premises ctxt axioms prems_imp_false =
blanchet@39964
   638
  if prop_of prems_imp_false aconv @{prop False} then
blanchet@39964
   639
    prems_imp_false
blanchet@39964
   640
  else
blanchet@39964
   641
    let
wenzelm@42361
   642
      val thy = Proof_Context.theory_of ctxt
blanchet@39964
   643
      fun match_term p =
blanchet@39964
   644
        let
blanchet@39964
   645
          val (tyenv, tenv) =
blanchet@39964
   646
            Pattern.first_order_match thy p (Vartab.empty, Vartab.empty)
blanchet@39964
   647
          val tsubst =
blanchet@39964
   648
            tenv |> Vartab.dest
blanchet@42099
   649
                 |> filter (Meson_Clausify.is_zapped_var_name o fst o fst)
blanchet@39964
   650
                 |> sort (cluster_ord
blanchet@39964
   651
                          o pairself (Meson_Clausify.cluster_of_zapped_var_name
blanchet@39964
   652
                                      o fst o fst))
blanchet@39964
   653
                 |> map (Meson.term_pair_of
blanchet@39964
   654
                         #> pairself (Envir.subst_term_types tyenv))
blanchet@39964
   655
          val tysubst = tyenv |> Vartab.dest
blanchet@39964
   656
        in (tysubst, tsubst) end
blanchet@39964
   657
      fun subst_info_for_prem subgoal_no prem =
blanchet@39964
   658
        case prem of
blanchet@39964
   659
          _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
blanchet@39964
   660
          let val ax_no = HOLogic.dest_nat num in
blanchet@39964
   661
            (ax_no, (subgoal_no,
blanchet@39964
   662
                     match_term (nth axioms ax_no |> the |> snd, t)))
blanchet@39964
   663
          end
blanchet@39964
   664
        | _ => raise TERM ("discharge_skolem_premises: Malformed premise",
blanchet@39964
   665
                           [prem])
blanchet@39964
   666
      fun cluster_of_var_name skolem s =
blanchet@42098
   667
        case try Meson_Clausify.cluster_of_zapped_var_name s of
blanchet@42098
   668
          NONE => NONE
blanchet@42098
   669
        | SOME ((ax_no, (cluster_no, _)), skolem') =>
blanchet@39964
   670
          if skolem' = skolem andalso cluster_no > 0 then
blanchet@39964
   671
            SOME (ax_no, cluster_no)
blanchet@39964
   672
          else
blanchet@39964
   673
            NONE
blanchet@39964
   674
      fun clusters_in_term skolem t =
blanchet@39964
   675
        Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
blanchet@39964
   676
      fun deps_for_term_subst (var, t) =
blanchet@39964
   677
        case clusters_in_term false var of
blanchet@39964
   678
          [] => NONE
blanchet@39964
   679
        | [(ax_no, cluster_no)] =>
blanchet@39964
   680
          SOME ((ax_no, cluster_no),
blanchet@39964
   681
                clusters_in_term true t
blanchet@39964
   682
                |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
blanchet@39964
   683
        | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
blanchet@39964
   684
      val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
blanchet@39964
   685
      val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
blanchet@39964
   686
                         |> sort (int_ord o pairself fst)
blanchet@39964
   687
      val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
blanchet@39964
   688
      val clusters = maps (op ::) depss
blanchet@39964
   689
      val ordered_clusters =
blanchet@39964
   690
        Int_Pair_Graph.empty
blanchet@39964
   691
        |> fold Int_Pair_Graph.default_node (map (rpair ()) clusters)
blanchet@39964
   692
        |> fold Int_Pair_Graph.add_deps_acyclic depss
blanchet@39964
   693
        |> Int_Pair_Graph.topological_order
blanchet@39964
   694
        handle Int_Pair_Graph.CYCLES _ =>
blanchet@40158
   695
               error "Cannot replay Metis proof in Isabelle without \
blanchet@40158
   696
                     \\"Hilbert_Choice\"."
blanchet@39964
   697
      val ax_counts =
blanchet@39964
   698
        Int_Tysubst_Table.empty
blanchet@39964
   699
        |> fold (fn (ax_no, (_, (tysubst, _))) =>
blanchet@43262
   700
                    Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
blanchet@39964
   701
                                                  (Integer.add 1)) substs
blanchet@39964
   702
        |> Int_Tysubst_Table.dest
blanchet@42339
   703
      val needed_axiom_props =
blanchet@42339
   704
        0 upto length axioms - 1 ~~ axioms
blanchet@42339
   705
        |> map_filter (fn (_, NONE) => NONE
blanchet@42339
   706
                        | (ax_no, SOME (_, t)) =>
blanchet@42339
   707
                          if exists (fn ((ax_no', _), n) =>
blanchet@42339
   708
                                        ax_no' = ax_no andalso n > 0)
blanchet@42339
   709
                                    ax_counts then
blanchet@42339
   710
                            SOME t
blanchet@42339
   711
                          else
blanchet@42339
   712
                            NONE)
blanchet@42339
   713
      val outer_param_names =
blanchet@42339
   714
        [] |> fold Term.add_var_names needed_axiom_props
blanchet@42339
   715
           |> filter (Meson_Clausify.is_zapped_var_name o fst)
blanchet@42339
   716
           |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
blanchet@42339
   717
           |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
blanchet@42339
   718
                         cluster_no = 0 andalso skolem)
blanchet@42339
   719
           |> sort shuffle_ord |> map (fst o snd)
blanchet@42270
   720
(* for debugging only:
blanchet@39964
   721
      fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
blanchet@39964
   722
        "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
blanchet@39964
   723
        "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
blanchet@39964
   724
        commas (map ((fn (s, t) => s ^ " |-> " ^ t)
blanchet@39964
   725
                     o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
blanchet@40264
   726
      val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
blanchet@40264
   727
      val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)
blanchet@42339
   728
      val _ = tracing ("OUTER PARAMS: " ^ PolyML.makestring outer_param_names)
blanchet@39964
   729
      val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
blanchet@39964
   730
                       cat_lines (map string_for_subst_info substs))
blanchet@39964
   731
*)
blanchet@42271
   732
      fun cut_and_ex_tac axiom =
blanchet@42271
   733
        cut_rules_tac [axiom] 1
blanchet@42271
   734
        THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
blanchet@39964
   735
      fun rotation_for_subgoal i =
blanchet@39964
   736
        find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
blanchet@39964
   737
    in
blanchet@39964
   738
      Goal.prove ctxt [] [] @{prop False}
blanchet@42271
   739
          (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst
blanchet@42271
   740
                                  o fst) ax_counts)
blanchet@42271
   741
                      THEN rename_tac outer_param_names 1
blanchet@42271
   742
                      THEN copy_prems_tac (map snd ax_counts) [] 1)
blanchet@40258
   743
              THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
blanchet@39964
   744
              THEN match_tac [prems_imp_false] 1
blanchet@39964
   745
              THEN ALLGOALS (fn i =>
blanchet@39964
   746
                       rtac @{thm Meson.skolem_COMBK_I} i
blanchet@39964
   747
                       THEN rotate_tac (rotation_for_subgoal i) i
blanchet@42342
   748
                       THEN PRIMITIVE (unify_first_prem_with_concl thy i)
blanchet@42271
   749
                       THEN assume_tac i
blanchet@42270
   750
                       THEN flexflex_tac)))
blanchet@40158
   751
      handle ERROR _ =>
blanchet@40158
   752
             error ("Cannot replay Metis proof in Isabelle:\n\
blanchet@40158
   753
                    \Error when discharging Skolem assumptions.")
blanchet@39964
   754
    end
blanchet@39964
   755
blanchet@39495
   756
end;