src/HOL/Tools/Metis/metis_reconstruct.ML
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 58950 d07464875dd4
child 58963 26bf09b95dda
permissions -rw-r--r--
proper context for match_tac etc.;
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
blanchet@57408
    91
fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx))
blanchet@39497
    92
blanchet@39497
    93
(* INFERENCE RULE: AXIOM *)
blanchet@39497
    94
blanchet@43212
    95
(* This causes variables to have an index of 1 by default. See also
blanchet@52031
    96
   "term_of_atp" in "ATP_Proof_Reconstruct". *)
blanchet@43212
    97
val axiom_inference = Thm.incr_indexes 1 oo lookth
blanchet@39497
    98
blanchet@39497
    99
(* INFERENCE RULE: ASSUME *)
blanchet@39497
   100
blanchet@39497
   101
val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
blanchet@39497
   102
blanchet@43187
   103
fun inst_excluded_middle thy i_atom =
blanchet@57408
   104
  let
blanchet@57408
   105
    val th = EXCLUDED_MIDDLE
blanchet@57408
   106
    val [vx] = Term.add_vars (prop_of th) []
blanchet@57408
   107
    val substs = [(cterm_of thy (Var vx), cterm_of thy i_atom)]
blanchet@57408
   108
  in
blanchet@57408
   109
    cterm_instantiate substs th
blanchet@57408
   110
  end
blanchet@39497
   111
blanchet@45508
   112
fun assume_inference ctxt type_enc concealed sym_tab atom =
blanchet@57408
   113
  inst_excluded_middle (Proof_Context.theory_of ctxt)
blanchet@57408
   114
    (singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom))
blanchet@39497
   115
blanchet@39498
   116
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
blanchet@39497
   117
   to reconstruct them admits new possibilities of errors, e.g. concerning
blanchet@39497
   118
   sorts. Instead we try to arrange that new TVars are distinct and that types
blanchet@39498
   119
   can be inferred from terms. *)
blanchet@39497
   120
blanchet@45508
   121
fun inst_inference ctxt type_enc concealed sym_tab th_pairs fsubst th =
blanchet@57408
   122
  let
blanchet@57408
   123
    val thy = Proof_Context.theory_of ctxt
blanchet@57408
   124
    val i_th = lookth th_pairs th
blanchet@57408
   125
    val i_th_vars = Term.add_vars (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
blanchet@57408
   134
        SOME (cterm_of thy (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
blanchet@57408
   158
    val ctm_of = cterm_incr_types thy (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) =>
blanchet@57408
   163
          Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
blanchet@57408
   164
          Syntax.string_of_term ctxt (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@43330
   174
fun incr_type_indexes inc th =
blanchet@57408
   175
  let
blanchet@57408
   176
    val tvs = Term.add_tvars (Thm.full_prop_of th) []
blanchet@57408
   177
    val thy = Thm.theory_of_thm th
blanchet@57408
   178
    fun inc_tvar ((a, i), s) = pairself (ctyp_of thy) (TVar ((a, i), s), TVar ((a, i + inc), s))
blanchet@57408
   179
  in
blanchet@57408
   180
    Thm.instantiate (map inc_tvar tvs, []) th
blanchet@57408
   181
  end
wenzelm@43330
   182
blanchet@39497
   183
(* Like RSN, but we rename apart only the type variables. Vars here typically
blanchet@39497
   184
   have an index of 1, and the use of RSN would increase this typically to 3.
blanchet@43300
   185
   Instantiations of those Vars could then fail. *)
blanchet@57400
   186
fun resolve_inc_tyvars ctxt tha i thb =
blanchet@39497
   187
  let
wenzelm@43330
   188
    val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
blanchet@57400
   189
    fun res (tha, thb) =
wenzelm@58950
   190
      (case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
wenzelm@52223
   191
            (false, tha, nprems_of tha) i thb
blanchet@39497
   192
           |> Seq.list_of |> distinct Thm.eq_thm of
blanchet@39497
   193
        [th] => th
blanchet@57400
   194
      | _ =>
blanchet@57400
   195
        let
blanchet@57400
   196
          val thaa'bb' as [(tha', _), (thb', _)] =
blanchet@57400
   197
            map (`(Local_Defs.unfold ctxt meta_not_not)) [tha, thb]
blanchet@57400
   198
        in
blanchet@57400
   199
          if forall Thm.eq_thm_prop thaa'bb' then
blanchet@57400
   200
            raise THM ("resolve_inc_tyvars: unique result expected", i, [tha, thb])
blanchet@57400
   201
          else
blanchet@57400
   202
            res (tha', thb')
blanchet@57408
   203
        end)
blanchet@39497
   204
  in
blanchet@57400
   205
    res (tha, thb)
wenzelm@52225
   206
    handle TERM z =>
blanchet@57400
   207
      let
blanchet@57400
   208
        val thy = Proof_Context.theory_of ctxt
blanchet@57400
   209
        val ps = []
blanchet@57400
   210
          |> fold (Term.add_vars o prop_of) [tha, thb]
blanchet@57400
   211
          |> AList.group (op =)
blanchet@57400
   212
          |> maps (fn ((s, _), T :: Ts) => map (fn T' => (Free (s, T), Free (s, T'))) Ts)
blanchet@57400
   213
          |> rpair (Envir.empty ~1)
wenzelm@58950
   214
          |-> fold (Pattern.unify (Context.Proof ctxt))
blanchet@57400
   215
          |> Envir.type_env |> Vartab.dest
blanchet@57400
   216
          |> map (fn (x, (S, T)) => pairself (ctyp_of thy) (TVar (x, S), T))
blanchet@57400
   217
      in
blanchet@57400
   218
        (* The unifier, which is invoked from "Thm.bicompose", will sometimes refuse to unify
blanchet@57400
   219
           "?a::?'a" with "?a::?'b" or "?a::nat" and throw a "TERM" exception (with "add_ffpair" as
blanchet@57400
   220
           first argument). We then perform unification of the types of variables by hand and try
blanchet@57400
   221
           again. We could do this the first time around but this error occurs seldom and we don't
blanchet@57400
   222
           want to break existing proofs in subtle ways or slow them down. *)
blanchet@57400
   223
        if null ps then raise TERM z
blanchet@57400
   224
        else res (pairself (Drule.instantiate_normalize (ps, [])) (tha, thb))
blanchet@57400
   225
      end
blanchet@39497
   226
  end
blanchet@39497
   227
blanchet@40221
   228
fun s_not (@{const Not} $ t) = t
blanchet@40221
   229
  | s_not t = HOLogic.mk_not t
blanchet@43195
   230
fun simp_not_not (@{const Trueprop} $ t) = @{const Trueprop} $ simp_not_not t
blanchet@43195
   231
  | simp_not_not (@{const Not} $ t) = s_not (simp_not_not t)
blanchet@40221
   232
  | simp_not_not t = t
blanchet@39497
   233
blanchet@43195
   234
val normalize_literal = simp_not_not o Envir.eta_contract
blanchet@43195
   235
blanchet@43187
   236
(* Find the relative location of an untyped term within a list of terms as a
blanchet@43187
   237
   1-based index. Returns 0 in case of failure. *)
blanchet@40221
   238
fun index_of_literal lit haystack =
blanchet@39497
   239
  let
blanchet@43195
   240
    fun match_lit normalize =
blanchet@43134
   241
      HOLogic.dest_Trueprop #> normalize
blanchet@43301
   242
      #> curry Term.aconv_untyped (lit |> normalize)
blanchet@43195
   243
  in
blanchet@43195
   244
    (case find_index (match_lit I) haystack of
blanchet@43195
   245
       ~1 => find_index (match_lit (simp_not_not o Envir.eta_contract)) haystack
blanchet@43195
   246
     | j => j) + 1
blanchet@43195
   247
  end
blanchet@39497
   248
blanchet@39893
   249
(* Permute a rule's premises to move the i-th premise to the last position. *)
blanchet@39893
   250
fun make_last i th =
blanchet@54756
   251
  let val n = nprems_of th in
blanchet@54756
   252
    if i >= 1 andalso i <= n then Thm.permute_prems (i - 1) 1 th
blanchet@54756
   253
    else raise THM ("select_literal", i, [th])
blanchet@57408
   254
  end
blanchet@39893
   255
blanchet@42348
   256
(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~ P" while avoiding
blanchet@42349
   257
   to create double negations. The "select" wrapper is a trick to ensure that
blanchet@42349
   258
   "P ==> ~ False ==> False" is rewritten to "P ==> False", not to "~ P". We
blanchet@42349
   259
   don't use this trick in general because it makes the proof object uglier than
blanchet@42349
   260
   necessary. FIXME. *)
wenzelm@54742
   261
fun negate_head ctxt th =
blanchet@42349
   262
  if exists (fn t => t aconv @{prop "~ False"}) (prems_of th) then
blanchet@42349
   263
    (th RS @{thm select_FalseI})
blanchet@54756
   264
    |> fold (rewrite_rule ctxt o single) @{thms not_atomize_select atomize_not_select}
blanchet@42349
   265
  else
wenzelm@54742
   266
    th |> fold (rewrite_rule ctxt o single) @{thms not_atomize atomize_not}
blanchet@39893
   267
blanchet@39893
   268
(* Maps the clause  [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *)
wenzelm@54742
   269
fun select_literal ctxt = negate_head ctxt oo make_last
blanchet@39893
   270
blanchet@45508
   271
fun resolve_inference ctxt type_enc concealed sym_tab th_pairs atom th1 th2 =
blanchet@39497
   272
  let
blanchet@43094
   273
    val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2)
blanchet@43187
   274
    val _ = trace_msg ctxt (fn () =>
blanchet@43187
   275
        "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1 ^ "\n\
blanchet@43187
   276
        \  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
blanchet@39497
   277
  in
blanchet@39497
   278
    (* Trivial cases where one operand is type info *)
blanchet@39497
   279
    if Thm.eq_thm (TrueI, i_th1) then
blanchet@39497
   280
      i_th2
blanchet@39497
   281
    else if Thm.eq_thm (TrueI, i_th2) then
blanchet@39497
   282
      i_th1
blanchet@39497
   283
    else
blanchet@39497
   284
      let
blanchet@43187
   285
        val i_atom =
blanchet@54756
   286
          singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom)
blanchet@54756
   287
        val _ = trace_msg ctxt (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atom)
blanchet@43187
   288
      in
blanchet@54756
   289
        (case index_of_literal (s_not i_atom) (prems_of i_th1) of
blanchet@54756
   290
          0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th1\""); i_th1)
blanchet@43187
   291
        | j1 =>
blanchet@43187
   292
          (trace_msg ctxt (fn () => "  index th1: " ^ string_of_int j1);
blanchet@57408
   293
           (case index_of_literal i_atom (prems_of i_th2) of
blanchet@54756
   294
             0 => (trace_msg ctxt (fn () => "Failed to find literal in \"th2\""); i_th2)
blanchet@43187
   295
           | j2 =>
blanchet@43187
   296
             (trace_msg ctxt (fn () => "  index th2: " ^ string_of_int j2);
blanchet@57400
   297
              resolve_inc_tyvars ctxt (select_literal ctxt j1 i_th1) j2 i_th2
blanchet@57408
   298
              handle TERM (s, _) => raise METIS_RECONSTRUCT ("resolve_inference", s)))))
blanchet@43187
   299
      end
blanchet@43187
   300
  end
blanchet@39497
   301
blanchet@39497
   302
(* INFERENCE RULE: REFL *)
blanchet@39497
   303
blanchet@39497
   304
val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
blanchet@39497
   305
blanchet@39497
   306
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
blanchet@39497
   307
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
blanchet@39497
   308
blanchet@45508
   309
fun refl_inference ctxt type_enc concealed sym_tab t =
blanchet@43094
   310
  let
blanchet@43094
   311
    val thy = Proof_Context.theory_of ctxt
blanchet@54756
   312
    val i_t = singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t
blanchet@43094
   313
    val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
blanchet@43094
   314
    val c_t = cterm_incr_types thy refl_idx i_t
blanchet@43094
   315
  in cterm_instantiate [(refl_x, c_t)] REFL_THM end
blanchet@39497
   316
blanchet@39497
   317
(* INFERENCE RULE: EQUALITY *)
blanchet@39497
   318
blanchet@39497
   319
val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
blanchet@39497
   320
val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
blanchet@39497
   321
blanchet@45508
   322
fun equality_inference ctxt type_enc concealed sym_tab (pos, atom) fp fr =
wenzelm@42361
   323
  let val thy = Proof_Context.theory_of ctxt
blanchet@43187
   324
      val m_tm = Metis_Term.Fn atom
blanchet@54756
   325
      val [i_atom, i_tm] = hol_terms_of_metis ctxt type_enc concealed sym_tab [m_tm, fr]
wenzelm@58070
   326
      val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
blanchet@39497
   327
      fun replace_item_list lx 0 (_::ls) = lx::ls
blanchet@39497
   328
        | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
blanchet@43205
   329
      fun path_finder_fail tm ps t =
blanchet@50875
   330
        raise METIS_RECONSTRUCT ("equality_inference (path_finder)",
blanchet@50875
   331
                  "path = " ^ space_implode " " (map string_of_int ps) ^
blanchet@50875
   332
                  " isa-term: " ^ Syntax.string_of_term ctxt tm ^
blanchet@50875
   333
                  (case t of
blanchet@54756
   334
                    SOME t => " fol-term: " ^ Metis_Term.toString t
blanchet@54756
   335
                  | NONE => ""))
blanchet@43212
   336
      fun path_finder tm [] _ = (tm, Bound 0)
blanchet@43212
   337
        | path_finder tm (p :: ps) (t as Metis_Term.Fn (s, ts)) =
blanchet@43177
   338
          let
blanchet@43268
   339
            val s = s |> Metis_Name.toString
blanchet@45511
   340
                      |> perhaps (try (unprefix_and_unascii const_prefix
blanchet@46392
   341
                                       #> the #> unmangled_const_name #> hd))
blanchet@43177
   342
          in
blanchet@43177
   343
            if s = metis_predicator orelse s = predicator_name orelse
blanchet@44492
   344
               s = metis_systematic_type_tag orelse s = metis_ad_hoc_type_tag
blanchet@44492
   345
               orelse s = type_tag_name then
blanchet@43212
   346
              path_finder tm ps (nth ts p)
blanchet@43177
   347
            else if s = metis_app_op orelse s = app_op_name then
blanchet@43130
   348
              let
blanchet@43130
   349
                val (tm1, tm2) = dest_comb tm
blanchet@43130
   350
                val p' = p - (length ts - 2)
blanchet@43130
   351
              in
blanchet@54756
   352
                if p' = 0 then path_finder tm1 ps (nth ts p) ||> (fn y => y $ tm2)
blanchet@54756
   353
                else path_finder tm2 ps (nth ts p) ||> (fn y => tm1 $ y)
blanchet@43130
   354
              end
blanchet@43130
   355
            else
blanchet@43130
   356
              let
blanchet@43130
   357
                val (tm1, args) = strip_comb tm
blanchet@43130
   358
                val adjustment = length ts - length args
blanchet@43130
   359
                val p' = if adjustment > p then p else p - adjustment
blanchet@54756
   360
                val tm_p = nth args p'
wenzelm@43278
   361
                  handle General.Subscript => path_finder_fail tm (p :: ps) (SOME t)
blanchet@43130
   362
                val _ = trace_msg ctxt (fn () =>
blanchet@43130
   363
                    "path_finder: " ^ string_of_int p ^ "  " ^
blanchet@43130
   364
                    Syntax.string_of_term ctxt tm_p)
blanchet@43212
   365
                val (r, t) = path_finder tm_p ps (nth ts p)
blanchet@43130
   366
              in (r, list_comb (tm1, replace_item_list t p' args)) end
blanchet@43130
   367
          end
blanchet@43212
   368
        | path_finder tm ps t = path_finder_fail tm ps (SOME t)
blanchet@43212
   369
      val (tm_subst, body) = path_finder i_atom fp m_tm
blanchet@39498
   370
      val tm_abs = Abs ("x", type_of tm_subst, body)
blanchet@39978
   371
      val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
blanchet@39978
   372
      val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
blanchet@39978
   373
      val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
blanchet@54501
   374
      val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill-typed but gives right max*)
blanchet@39497
   375
      val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
blanchet@39978
   376
      val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
blanchet@39497
   377
      val eq_terms = map (pairself (cterm_of thy))
wenzelm@44121
   378
        (ListPair.zip (Misc_Legacy.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
blanchet@57408
   379
  in
blanchet@57408
   380
    cterm_instantiate eq_terms subst'
blanchet@57408
   381
  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@57408
   386
  (case p of
blanchet@43186
   387
    (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor
blanchet@54756
   388
  | (_, Metis_Proof.Assume f_atom) => assume_inference ctxt type_enc concealed sym_tab f_atom
blanchet@39497
   389
  | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
blanchet@54756
   390
    inst_inference ctxt type_enc concealed sym_tab th_pairs f_subst f_th1 |> factor
blanchet@43187
   391
  | (_, Metis_Proof.Resolve(f_atom, f_th1, f_th2)) =>
blanchet@54756
   392
    resolve_inference ctxt type_enc concealed sym_tab th_pairs f_atom f_th1 f_th2 |> factor
blanchet@54756
   393
  | (_, Metis_Proof.Refl f_tm) => refl_inference ctxt type_enc concealed sym_tab f_tm
blanchet@39497
   394
  | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
blanchet@57408
   395
    equality_inference ctxt type_enc concealed sym_tab f_lit f_p f_r)
blanchet@39497
   396
blanchet@39893
   397
fun flexflex_first_order th =
blanchet@54756
   398
  (case Thm.tpairs_of th of
blanchet@54756
   399
    [] => th
blanchet@54756
   400
  | pairs =>
blanchet@54756
   401
    let
blanchet@54756
   402
      val thy = theory_of_thm th
blanchet@54756
   403
      val cert = cterm_of thy
blanchet@54756
   404
      val certT = ctyp_of thy
blanchet@54756
   405
      val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty)
blanchet@54756
   406
blanchet@54756
   407
      fun mkT (v, (S, T)) = (certT (TVar (v, S)), certT T)
blanchet@54756
   408
      fun mk (v, (T, t)) = (cert (Var (v, Envir.subst_type tyenv T)), cert t)
blanchet@54756
   409
blanchet@54756
   410
      val instsT = Vartab.fold (cons o mkT) tyenv []
blanchet@54756
   411
      val insts = Vartab.fold (cons o mk) tenv []
blanchet@54756
   412
    in
blanchet@54756
   413
      Thm.instantiate (instsT, insts) th
blanchet@54756
   414
    end
blanchet@54756
   415
    handle THM _ => th)
blanchet@39497
   416
blanchet@43268
   417
fun is_metis_literal_genuine (_, (s, _)) =
blanchet@43268
   418
  not (String.isPrefix class_prefix (Metis_Name.toString s))
blanchet@39895
   419
fun is_isabelle_literal_genuine t =
blanchet@54756
   420
  (case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true)
blanchet@39895
   421
blanchet@39895
   422
fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
blanchet@39895
   423
blanchet@42333
   424
(* Seldomly needed hack. A Metis clause is represented as a set, so duplicate
blanchet@42333
   425
   disjuncts are impossible. In the Isabelle proof, in spite of efforts to
blanchet@42333
   426
   eliminate them, duplicates sometimes appear with slightly different (but
blanchet@42333
   427
   unifiable) types. *)
blanchet@42333
   428
fun resynchronize ctxt fol_th th =
blanchet@42333
   429
  let
blanchet@42333
   430
    val num_metis_lits =
blanchet@54756
   431
      count is_metis_literal_genuine (Metis_LiteralSet.toList (Metis_Thm.clause fol_th))
blanchet@42333
   432
    val num_isabelle_lits = count is_isabelle_literal_genuine (prems_of th)
blanchet@42333
   433
  in
blanchet@42333
   434
    if num_metis_lits >= num_isabelle_lits then
blanchet@42333
   435
      th
blanchet@42333
   436
    else
blanchet@42333
   437
      let
blanchet@42333
   438
        val (prems0, concl) = th |> prop_of |> Logic.strip_horn
blanchet@54756
   439
        val prems = prems0 |> map normalize_literal |> distinct Term.aconv_untyped
blanchet@42333
   440
        val goal = Logic.list_implies (prems, concl)
wenzelm@54984
   441
        val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm th)) ctxt
blanchet@57400
   442
        val tac = cut_tac th 1 THEN rewrite_goals_tac ctxt' meta_not_not THEN ALLGOALS assume_tac
blanchet@42333
   443
      in
blanchet@42333
   444
        if length prems = length prems0 then
blanchet@50875
   445
          raise METIS_RECONSTRUCT ("resynchronize", "Out of sync")
blanchet@42333
   446
        else
wenzelm@54984
   447
          Goal.prove ctxt' [] [] goal (K tac)
wenzelm@54984
   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@54756
   454
  if not (null th_pairs) andalso prop_of (snd (hd th_pairs)) aconv @{prop False} then
blanchet@40868
   455
    (* Isabelle sometimes identifies literals (premises) that are distinct in
blanchet@40868
   456
       Metis (e.g., because of type variables). We give the Isabelle proof the
blanchet@40868
   457
       benefice of the doubt. *)
blanchet@43094
   458
    th_pairs
blanchet@40868
   459
  else
blanchet@40868
   460
    let
blanchet@54756
   461
      val _ = trace_msg ctxt (fn () => "=============================================")
blanchet@54756
   462
      val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
blanchet@54756
   463
      val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
blanchet@45508
   464
      val th = one_step ctxt type_enc concealed sym_tab th_pairs (fol_th, inf)
blanchet@54756
   465
        |> flexflex_first_order
blanchet@54756
   466
        |> resynchronize ctxt fol_th
blanchet@54756
   467
      val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
blanchet@54756
   468
      val _ = trace_msg ctxt (fn () => "=============================================")
blanchet@54756
   469
    in
blanchet@54756
   470
      (fol_th, th) :: th_pairs
blanchet@54756
   471
    end
blanchet@39497
   472
blanchet@42342
   473
(* It is normally sufficient to apply "assume_tac" to unify the conclusion with
blanchet@42342
   474
   one of the premises. Unfortunately, this sometimes yields "Variable
wenzelm@51701
   475
   has two distinct types" errors. To avoid this, we instantiate the
blanchet@42342
   476
   variables before applying "assume_tac". Typical constraints are of the form
blanchet@42342
   477
     ?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
   478
   where the nonvariables are goal parameters. *)
blanchet@42342
   479
fun unify_first_prem_with_concl thy i th =
blanchet@42342
   480
  let
blanchet@42342
   481
    val goal = Logic.get_goal (prop_of th) i |> Envir.beta_eta_contract
blanchet@42342
   482
    val prem = goal |> Logic.strip_assums_hyp |> hd
blanchet@42342
   483
    val concl = goal |> Logic.strip_assums_concl
blanchet@54756
   484
blanchet@42342
   485
    fun pair_untyped_aconv (t1, t2) (u1, u2) =
blanchet@43301
   486
      Term.aconv_untyped (t1, u1) andalso Term.aconv_untyped (t2, u2)
blanchet@54756
   487
blanchet@42342
   488
    fun add_terms tp inst =
blanchet@42342
   489
      if exists (pair_untyped_aconv tp) inst then inst
blanchet@42342
   490
      else tp :: map (apsnd (subst_atomic [tp])) inst
blanchet@54756
   491
blanchet@42342
   492
    fun is_flex t =
blanchet@54756
   493
      (case strip_comb t of
blanchet@42342
   494
        (Var _, args) => forall is_Bound args
blanchet@54756
   495
      | _ => false)
blanchet@54756
   496
blanchet@42342
   497
    fun unify_flex flex rigid =
blanchet@54756
   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@54756
   502
      | _ => I)
blanchet@54756
   503
blanchet@42342
   504
    fun unify_potential_flex comb atom =
blanchet@42342
   505
      if is_flex comb then unify_flex comb atom
blanchet@42342
   506
      else if is_Var atom then add_terms (atom, comb)
blanchet@42342
   507
      else I
blanchet@54756
   508
blanchet@42342
   509
    fun unify_terms (t, u) =
blanchet@54756
   510
      (case (t, u) of
blanchet@42342
   511
        (t1 $ t2, u1 $ u2) =>
blanchet@42342
   512
        if is_flex t then unify_flex t u
blanchet@42342
   513
        else if is_flex u then unify_flex u t
blanchet@42342
   514
        else fold unify_terms [(t1, u1), (t2, u2)]
blanchet@42342
   515
      | (_ $ _, _) => unify_potential_flex t u
blanchet@42342
   516
      | (_, _ $ _) => unify_potential_flex u t
blanchet@42342
   517
      | (Var _, _) => add_terms (t, u)
blanchet@42342
   518
      | (_, Var _) => add_terms (u, t)
blanchet@54756
   519
      | _ => I)
blanchet@54756
   520
blanchet@42344
   521
    val t_inst =
blanchet@42344
   522
      [] |> try (unify_terms (prem, concl) #> map (pairself (cterm_of thy)))
blanchet@42344
   523
         |> the_default [] (* FIXME *)
blanchet@54756
   524
  in
blanchet@54756
   525
    cterm_instantiate t_inst th
blanchet@54756
   526
  end
blanchet@39964
   527
blanchet@39964
   528
val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
blanchet@39964
   529
blanchet@39964
   530
fun copy_prems_tac [] ns i =
blanchet@39964
   531
    if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
blanchet@54756
   532
  | copy_prems_tac (1 :: ms) ns i = rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
blanchet@39964
   533
  | copy_prems_tac (m :: ms) ns i =
wenzelm@58839
   534
    eresolve_tac [copy_prem] i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
blanchet@39964
   535
blanchet@42271
   536
(* Metis generates variables of the form _nnn. *)
blanchet@42271
   537
val is_metis_fresh_variable = String.isPrefix "_"
blanchet@42271
   538
blanchet@40258
   539
fun instantiate_forall_tac thy t i st =
blanchet@39964
   540
  let
blanchet@40258
   541
    val params = Logic.strip_params (Logic.get_goal (prop_of st) i) |> rev
blanchet@54756
   542
blanchet@39964
   543
    fun repair (t as (Var ((s, _), _))) =
blanchet@40258
   544
        (case find_index (fn (s', _) => s' = s) params of
blanchet@54756
   545
          ~1 => t
blanchet@54756
   546
        | j => Bound j)
blanchet@40261
   547
      | repair (t $ u) =
blanchet@40261
   548
        (case (repair t, repair u) of
blanchet@54756
   549
          (t as Bound j, u as Bound k) =>
blanchet@54756
   550
          (* This is a trick to repair the discrepancy between the fully skolemized term that MESON
blanchet@54756
   551
             gives us (where existentials were pulled out) and the reality. *)
blanchet@54756
   552
          if k > j then t else t $ u
blanchet@54756
   553
        | (t, u) => t $ u)
blanchet@39964
   554
      | repair t = t
blanchet@54756
   555
wenzelm@44241
   556
    val t' = t |> repair |> fold (absdummy o snd) params
blanchet@54756
   557
blanchet@39964
   558
    fun do_instantiate th =
blanchet@54756
   559
      (case Term.add_vars (prop_of th) []
blanchet@54756
   560
            |> filter_out ((Meson_Clausify.is_zapped_var_name orf is_metis_fresh_variable) o fst
blanchet@54756
   561
              o fst) of
blanchet@42270
   562
        [] => th
blanchet@42271
   563
      | [var as (_, T)] =>
blanchet@42271
   564
        let
blanchet@42271
   565
          val var_binder_Ts = T |> binder_types |> take (length params) |> rev
blanchet@42271
   566
          val var_body_T = T |> funpow (length params) range_type
blanchet@42271
   567
          val tyenv =
blanchet@42271
   568
            Vartab.empty |> Type.raw_unifys (fastype_of t :: map snd params,
blanchet@42271
   569
                                             var_body_T :: var_binder_Ts)
blanchet@42271
   570
          val env =
blanchet@42271
   571
            Envir.Envir {maxidx = Vartab.fold (Integer.max o snd o fst) tyenv 0,
blanchet@54756
   572
              tenv = Vartab.empty, tyenv = tyenv}
blanchet@42271
   573
          val ty_inst =
blanchet@54756
   574
            Vartab.fold (fn (x, (S, T)) => cons (pairself (ctyp_of thy) (TVar (x, S), T))) tyenv []
blanchet@54756
   575
          val t_inst = [pairself (cterm_of thy o Envir.norm_term env) (Var var, t')]
blanchet@54756
   576
        in
blanchet@54756
   577
          Drule.instantiate_normalize (ty_inst, 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@58839
   581
    (DETERM (eresolve_tac @{thms allE} i THEN rotate_tac ~1 i) THEN PRIMITIVE do_instantiate) st
blanchet@39964
   582
  end
blanchet@39964
   583
wenzelm@58839
   584
fun fix_exists_tac t = eresolve_tac [exE] THEN' rename_tac [t |> dest_Var |> fst |> fst]
blanchet@40261
   585
blanchet@40261
   586
fun release_quantifier_tac thy (skolem, t) =
blanchet@41135
   587
  (if skolem then fix_exists_tac else instantiate_forall_tac thy) t
blanchet@40261
   588
blanchet@40258
   589
fun release_clusters_tac _ _ _ [] = K all_tac
blanchet@54756
   590
  | release_clusters_tac thy 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 =
blanchet@40261
   605
        map (release_quantifier_tac thy) 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)
blanchet@40258
   611
      THEN' release_clusters_tac thy 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 =
blanchet@54756
   617
  prod_ord int_ord (prod_ord int_ord (prod_ord bool_ord int_ord)) (pairself 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)
blanchet@40258
   630
fun shuffle_ord p = prod_ord int_ord int_ord (pairself 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 =
blanchet@39964
   637
  if 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
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@57408
   657
blanchet@51998
   658
      fun subst_info_of_prem subgoal_no prem =
blanchet@57408
   659
        (case prem of
blanchet@39964
   660
          _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
blanchet@39964
   661
          let val ax_no = HOLogic.dest_nat num in
blanchet@39964
   662
            (ax_no, (subgoal_no,
blanchet@39964
   663
                     match_term (nth axioms ax_no |> the |> snd, t)))
blanchet@39964
   664
          end
blanchet@57408
   665
        | _ => raise TERM ("discharge_skolem_premises: Malformed premise", [prem]))
blanchet@57408
   666
blanchet@39964
   667
      fun cluster_of_var_name skolem s =
blanchet@57408
   668
        (case try Meson_Clausify.cluster_of_zapped_var_name s of
blanchet@42098
   669
          NONE => NONE
blanchet@42098
   670
        | SOME ((ax_no, (cluster_no, _)), skolem') =>
blanchet@57408
   671
          if skolem' = skolem andalso cluster_no > 0 then SOME (ax_no, cluster_no) else NONE)
blanchet@57408
   672
blanchet@39964
   673
      fun clusters_in_term skolem t =
blanchet@39964
   674
        Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
blanchet@57408
   675
blanchet@51998
   676
      fun deps_of_term_subst (var, t) =
blanchet@57408
   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@57408
   681
            clusters_in_term true t |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
blanchet@57408
   682
        | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var]))
blanchet@57408
   683
blanchet@39964
   684
      val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
blanchet@51998
   685
      val substs = prems |> map2 subst_info_of_prem (1 upto length prems)
blanchet@39964
   686
                         |> sort (int_ord o pairself fst)
blanchet@51998
   687
      val depss = maps (map_filter deps_of_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@55523
   695
               error "Cannot replay Metis proof in Isabelle without \"Hilbert_Choice\""
blanchet@39964
   696
      val ax_counts =
blanchet@39964
   697
        Int_Tysubst_Table.empty
blanchet@39964
   698
        |> fold (fn (ax_no, (_, (tysubst, _))) =>
blanchet@43262
   699
                    Int_Tysubst_Table.map_default ((ax_no, tysubst), 0)
blanchet@39964
   700
                                                  (Integer.add 1)) substs
blanchet@39964
   701
        |> Int_Tysubst_Table.dest
blanchet@42339
   702
      val needed_axiom_props =
blanchet@42339
   703
        0 upto length axioms - 1 ~~ axioms
blanchet@42339
   704
        |> map_filter (fn (_, NONE) => NONE
blanchet@42339
   705
                        | (ax_no, SOME (_, t)) =>
blanchet@42339
   706
                          if exists (fn ((ax_no', _), n) =>
blanchet@42339
   707
                                        ax_no' = ax_no andalso n > 0)
blanchet@42339
   708
                                    ax_counts then
blanchet@42339
   709
                            SOME t
blanchet@42339
   710
                          else
blanchet@42339
   711
                            NONE)
blanchet@42339
   712
      val outer_param_names =
blanchet@42339
   713
        [] |> fold Term.add_var_names needed_axiom_props
blanchet@42339
   714
           |> filter (Meson_Clausify.is_zapped_var_name o fst)
blanchet@42339
   715
           |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst))
blanchet@42339
   716
           |> filter (fn (((_, (cluster_no, _)), skolem), _) =>
blanchet@42339
   717
                         cluster_no = 0 andalso skolem)
blanchet@42339
   718
           |> sort shuffle_ord |> map (fst o snd)
blanchet@57408
   719
blanchet@42270
   720
(* for debugging only:
blanchet@51998
   721
      fun string_of_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
blanchet@39964
   722
        "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
wenzelm@51929
   723
        "; tysubst: " ^ @{make_string} tysubst ^ "; tsubst: {" ^
blanchet@39964
   724
        commas (map ((fn (s, t) => s ^ " |-> " ^ t)
blanchet@39964
   725
                     o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
wenzelm@51929
   726
      val _ = tracing ("ORDERED CLUSTERS: " ^ @{make_string} ordered_clusters)
wenzelm@51929
   727
      val _ = tracing ("AXIOM COUNTS: " ^ @{make_string} ax_counts)
wenzelm@51929
   728
      val _ = tracing ("OUTER PARAMS: " ^ @{make_string} outer_param_names)
blanchet@39964
   729
      val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
blanchet@51998
   730
                       cat_lines (map string_of_subst_info substs))
blanchet@39964
   731
*)
blanchet@57408
   732
wenzelm@58839
   733
      fun cut_and_ex_tac axiom =
wenzelm@58839
   734
        cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (eresolve_tac @{thms exE}) 1)
blanchet@51998
   735
      fun rotation_of_subgoal i =
blanchet@39964
   736
        find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
blanchet@57408
   737
wenzelm@54984
   738
      val ctxt' = fold Thm.declare_hyps (#hyps (Thm.crep_thm prems_imp_false)) ctxt
blanchet@39964
   739
    in
wenzelm@54984
   740
      Goal.prove ctxt' [] [] @{prop False}
blanchet@57408
   741
        (K (DETERM (EVERY (map (cut_and_ex_tac o fst o the o nth axioms o fst o fst) ax_counts)
blanchet@57408
   742
              THEN rename_tac outer_param_names 1
blanchet@57408
   743
              THEN copy_prems_tac (map snd ax_counts) [] 1)
blanchet@57408
   744
            THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
wenzelm@58957
   745
            THEN match_tac ctxt' [prems_imp_false] 1
wenzelm@58839
   746
            THEN ALLGOALS (fn i => resolve_tac @{thms Meson.skolem_COMBK_I} i
blanchet@57408
   747
              THEN rotate_tac (rotation_of_subgoal i) i
blanchet@57408
   748
              THEN PRIMITIVE (unify_first_prem_with_concl thy i)
blanchet@57408
   749
              THEN assume_tac i
wenzelm@58950
   750
              THEN flexflex_tac ctxt')))
wenzelm@54984
   751
      handle ERROR msg =>
wenzelm@54984
   752
        cat_error msg
blanchet@55523
   753
          "Cannot replay Metis proof in Isabelle: error when discharging Skolem assumptions"
blanchet@39964
   754
    end
blanchet@39964
   755
blanchet@39495
   756
end;