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