src/HOL/Tools/Sledgehammer/metis_tactics.ML
author blanchet
Wed Sep 15 16:23:11 2010 +0200 (2010-09-15)
changeset 39419 c9accfd621a5
parent 39376 ca81b7ae543c
child 39450 7e9879fbb7c5
permissions -rw-r--r--
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet@35826
     1
(*  Title:      HOL/Tools/Sledgehammer/metis_tactics.ML
blanchet@38027
     2
    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
blanchet@38027
     3
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
blanchet@38027
     4
    Author:     Jasmin Blanchette, TU Muenchen
wenzelm@23442
     5
    Copyright   Cambridge University 2007
wenzelm@23447
     6
wenzelm@29266
     7
HOL setup for the Metis prover.
wenzelm@23442
     8
*)
wenzelm@23442
     9
blanchet@35826
    10
signature METIS_TACTICS =
wenzelm@23442
    11
sig
wenzelm@32955
    12
  val trace: bool Unsynchronized.ref
wenzelm@24309
    13
  val type_lits: bool Config.T
wenzelm@24319
    14
  val metis_tac: Proof.context -> thm list -> int -> tactic
wenzelm@24319
    15
  val metisF_tac: Proof.context -> thm list -> int -> tactic
paulson@32532
    16
  val metisFT_tac: Proof.context -> thm list -> int -> tactic
wenzelm@24319
    17
  val setup: theory -> theory
wenzelm@23442
    18
end
wenzelm@23442
    19
blanchet@35826
    20
structure Metis_Tactics : METIS_TACTICS =
wenzelm@23442
    21
struct
wenzelm@23442
    22
blanchet@37578
    23
open Metis_Clauses
blanchet@35826
    24
wenzelm@32956
    25
val trace = Unsynchronized.ref false;
blanchet@35826
    26
fun trace_msg msg = if !trace then tracing (msg ()) else ();
wenzelm@32955
    27
wenzelm@36001
    28
val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
wenzelm@23442
    29
blanchet@35826
    30
datatype mode = FO | HO | FT  (* first-order, higher-order, fully-typed *)
paulson@32532
    31
wenzelm@32956
    32
(* ------------------------------------------------------------------------- *)
wenzelm@32956
    33
(* Useful Theorems                                                           *)
wenzelm@32956
    34
(* ------------------------------------------------------------------------- *)
wenzelm@33689
    35
val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
wenzelm@36945
    36
val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
wenzelm@33689
    37
val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
wenzelm@33689
    38
val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
wenzelm@23442
    39
wenzelm@32956
    40
(* ------------------------------------------------------------------------- *)
wenzelm@32956
    41
(* Useful Functions                                                          *)
wenzelm@32956
    42
(* ------------------------------------------------------------------------- *)
wenzelm@23442
    43
blanchet@37417
    44
(* Match untyped terms. *)
blanchet@37417
    45
fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
blanchet@37417
    46
  | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
blanchet@37417
    47
  | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
blanchet@37417
    48
    (a = b) (* The index is ignored, for some reason. *)
blanchet@37417
    49
  | untyped_aconv (Bound i) (Bound j) = (i = j)
blanchet@37417
    50
  | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
blanchet@37417
    51
  | untyped_aconv (t1 $ t2) (u1 $ u2) =
blanchet@37417
    52
    untyped_aconv t1 u1 andalso untyped_aconv t2 u2
blanchet@37417
    53
  | untyped_aconv _ _ = false
wenzelm@23442
    54
wenzelm@32956
    55
(* Finding the relative location of an untyped term within a list of terms *)
wenzelm@32956
    56
fun get_index lit =
wenzelm@32956
    57
  let val lit = Envir.eta_contract lit
blanchet@37498
    58
      fun get _ [] = raise Empty
wenzelm@32956
    59
        | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x))
wenzelm@32956
    60
                          then n  else get (n+1) xs
wenzelm@32956
    61
  in get 1 end;
wenzelm@23442
    62
wenzelm@32956
    63
(* ------------------------------------------------------------------------- *)
wenzelm@32956
    64
(* HOL to FOL  (Isabelle to Metis)                                           *)
wenzelm@32956
    65
(* ------------------------------------------------------------------------- *)
wenzelm@23442
    66
blanchet@38614
    67
fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
blanchet@38606
    68
  | fn_isa_to_met_sublevel x = x
blanchet@38606
    69
fun fn_isa_to_met_toplevel "equal" = "="
blanchet@38606
    70
  | fn_isa_to_met_toplevel x = x
wenzelm@23442
    71
wenzelm@32956
    72
fun metis_lit b c args = (b, (c, args));
wenzelm@23442
    73
blanchet@39419
    74
fun metis_term_from_combtyp (CombTVar (s, _)) = Metis_Term.Var s
blanchet@39419
    75
  | metis_term_from_combtyp (CombTFree (s, _)) = Metis_Term.Fn (s, [])
blanchet@37926
    76
  | metis_term_from_combtyp (CombType ((s, _), tps)) =
blanchet@39419
    77
    Metis_Term.Fn (s, map metis_term_from_combtyp tps);
wenzelm@23442
    78
wenzelm@32956
    79
(*These two functions insert type literals before the real literals. That is the
wenzelm@32956
    80
  opposite order from TPTP linkup, but maybe OK.*)
wenzelm@23442
    81
wenzelm@32956
    82
fun hol_term_to_fol_FO tm =
blanchet@35865
    83
  case strip_combterm_comb tm of
blanchet@36170
    84
      (CombConst ((c, _), _, tys), tms) =>
blanchet@37926
    85
        let val tyargs = map metis_term_from_combtyp tys
wenzelm@32956
    86
            val args   = map hol_term_to_fol_FO tms
blanchet@39419
    87
        in Metis_Term.Fn (c, tyargs @ args) end
blanchet@39419
    88
    | (CombVar ((v, _), _), []) => Metis_Term.Var v
blanchet@38695
    89
    | _ => raise Fail "non-first-order combterm"
wenzelm@23442
    90
blanchet@38099
    91
fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
blanchet@39419
    92
      Metis_Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist)
blanchet@39419
    93
  | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis_Term.Var s
blanchet@35865
    94
  | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
blanchet@39419
    95
       Metis_Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
wenzelm@23442
    96
wenzelm@32956
    97
(*The fully-typed translation, to avoid type errors*)
blanchet@39419
    98
fun wrap_type (tm, ty) = Metis_Term.Fn("ti", [tm, metis_term_from_combtyp ty]);
wenzelm@32956
    99
blanchet@39419
   100
fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis_Term.Var s, ty)
blanchet@36170
   101
  | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
blanchet@39419
   102
      wrap_type (Metis_Term.Fn(fn_isa_to_met_sublevel a, []), ty)
blanchet@35865
   103
  | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
blanchet@39419
   104
       wrap_type (Metis_Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
blanchet@37994
   105
                  combtyp_of tm)
paulson@32532
   106
blanchet@37923
   107
fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
blanchet@36170
   108
      let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
blanchet@37926
   109
          val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
wenzelm@32956
   110
          val lits = map hol_term_to_fol_FO tms
blanchet@38606
   111
      in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
blanchet@37923
   112
  | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
blanchet@35865
   113
     (case strip_combterm_comb tm of
blanchet@36170
   114
          (CombConst(("equal", _), _, _), tms) =>
blanchet@37923
   115
            metis_lit pos "=" (map hol_term_to_fol_HO tms)
blanchet@37923
   116
        | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
blanchet@37923
   117
  | hol_literal_to_fol FT (FOLLiteral (pos, tm)) =
blanchet@35865
   118
     (case strip_combterm_comb tm of
blanchet@36170
   119
          (CombConst(("equal", _), _, _), tms) =>
blanchet@37923
   120
            metis_lit pos "=" (map hol_term_to_fol_FT tms)
blanchet@37923
   121
        | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
wenzelm@23442
   122
blanchet@37399
   123
fun literals_of_hol_term thy mode t =
blanchet@35865
   124
      let val (lits, types_sorts) = literals_of_term thy t
wenzelm@32956
   125
      in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
wenzelm@23442
   126
wenzelm@32956
   127
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
blanchet@37643
   128
fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
blanchet@39419
   129
    metis_lit pos s [Metis_Term.Var s']
blanchet@37643
   130
  | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) =
blanchet@39419
   131
    metis_lit pos s [Metis_Term.Fn (s',[])]
wenzelm@23442
   132
wenzelm@32994
   133
fun default_sort _ (TVar _) = false
wenzelm@33035
   134
  | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
wenzelm@23442
   135
wenzelm@32956
   136
fun metis_of_tfree tf =
blanchet@39419
   137
  Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
paulson@24937
   138
blanchet@37625
   139
fun hol_thm_to_fol is_conjecture ctxt mode j skolems th =
blanchet@37399
   140
  let
blanchet@37399
   141
    val thy = ProofContext.theory_of ctxt
blanchet@37625
   142
    val (skolems, (mlits, types_sorts)) =
blanchet@37625
   143
     th |> prop_of |> conceal_skolem_terms j skolems
blanchet@37399
   144
        ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
wenzelm@32956
   145
  in
wenzelm@32956
   146
      if is_conjecture then
blanchet@39419
   147
          (Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
blanchet@37625
   148
           type_literals_for_types types_sorts, skolems)
wenzelm@32956
   149
      else
blanchet@36966
   150
        let val tylits = filter_out (default_sort ctxt) types_sorts
blanchet@36966
   151
                         |> type_literals_for_types
wenzelm@32956
   152
            val mtylits = if Config.get ctxt type_lits
blanchet@36556
   153
                          then map (metis_of_type_literals false) tylits else []
wenzelm@32956
   154
        in
blanchet@39419
   155
          (Metis_Thm.axiom (Metis_LiteralSet.fromList(mtylits @ mlits)), [],
blanchet@37625
   156
           skolems)
wenzelm@32956
   157
        end
wenzelm@32956
   158
  end;
wenzelm@23442
   159
wenzelm@32956
   160
(* ARITY CLAUSE *)
wenzelm@23442
   161
blanchet@37643
   162
fun m_arity_cls (TConsLit ((c, _), (t, _), args)) =
blanchet@39419
   163
    metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)]
blanchet@37643
   164
  | m_arity_cls (TVarLit ((c, _), (s, _))) =
blanchet@39419
   165
    metis_lit false c [Metis_Term.Var s]
wenzelm@23442
   166
wenzelm@32956
   167
(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
blanchet@35865
   168
fun arity_cls (ArityClause {conclLit, premLits, ...}) =
wenzelm@32956
   169
  (TrueI,
blanchet@39419
   170
   Metis_Thm.axiom (Metis_LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
wenzelm@23442
   171
wenzelm@32956
   172
(* CLASSREL CLAUSE *)
wenzelm@23442
   173
blanchet@37925
   174
fun m_class_rel_cls (subclass, _) (superclass, _) =
blanchet@39419
   175
  [metis_lit false subclass [Metis_Term.Var "T"], metis_lit true superclass [Metis_Term.Var "T"]];
wenzelm@23442
   176
blanchet@37925
   177
fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) =
blanchet@39419
   178
  (TrueI, Metis_Thm.axiom (Metis_LiteralSet.fromList (m_class_rel_cls subclass superclass)));
wenzelm@23442
   179
wenzelm@32956
   180
(* ------------------------------------------------------------------------- *)
wenzelm@32956
   181
(* FOL to HOL  (Metis to Isabelle)                                           *)
wenzelm@32956
   182
(* ------------------------------------------------------------------------- *)
wenzelm@23442
   183
wenzelm@32956
   184
datatype term_or_type = Term of Term.term | Type of Term.typ;
wenzelm@23442
   185
wenzelm@32956
   186
fun terms_of [] = []
wenzelm@32956
   187
  | terms_of (Term t :: tts) = t :: terms_of tts
wenzelm@32956
   188
  | terms_of (Type _ :: tts) = terms_of tts;
wenzelm@23442
   189
wenzelm@32956
   190
fun types_of [] = []
wenzelm@32994
   191
  | types_of (Term (Term.Var ((a,idx), _)) :: tts) =
wenzelm@32956
   192
      if String.isPrefix "_" a then
wenzelm@32956
   193
          (*Variable generated by Metis, which might have been a type variable.*)
wenzelm@32994
   194
          TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
wenzelm@32956
   195
      else types_of tts
wenzelm@32956
   196
  | types_of (Term _ :: tts) = types_of tts
wenzelm@32956
   197
  | types_of (Type T :: tts) = T :: types_of tts;
wenzelm@23442
   198
wenzelm@32956
   199
fun apply_list rator nargs rands =
wenzelm@32956
   200
  let val trands = terms_of rands
wenzelm@32956
   201
  in  if length trands = nargs then Term (list_comb(rator, trands))
blanchet@37402
   202
      else raise Fail
wenzelm@32956
   203
        ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
wenzelm@32956
   204
          " expected " ^ Int.toString nargs ^
wenzelm@32956
   205
          " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
wenzelm@32956
   206
  end;
wenzelm@23442
   207
wenzelm@24500
   208
fun infer_types ctxt =
wenzelm@24500
   209
  Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
wenzelm@25713
   210
wenzelm@32956
   211
(*We use 1 rather than 0 because variable references in clauses may otherwise conflict
wenzelm@32956
   212
  with variable constraints in the goal...at least, type inference often fails otherwise.
wenzelm@32956
   213
  SEE ALSO axiom_inf below.*)
wenzelm@32956
   214
fun mk_var (w,T) = Term.Var((w,1), T);
wenzelm@23442
   215
wenzelm@32956
   216
(*include the default sort, if available*)
wenzelm@32956
   217
fun mk_tfree ctxt w =
wenzelm@32956
   218
  let val ww = "'" ^ w
wenzelm@33035
   219
  in  TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))  end;
wenzelm@23442
   220
wenzelm@32956
   221
(*Remove the "apply" operator from an HO term*)
blanchet@39419
   222
fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t
wenzelm@32956
   223
  | strip_happ args x = (x, args);
wenzelm@23442
   224
blanchet@36967
   225
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
blanchet@36967
   226
haftmann@38864
   227
fun smart_invert_const "fequal" = @{const_name HOL.eq}
blanchet@38606
   228
  | smart_invert_const s = invert_const s
blanchet@38606
   229
blanchet@39419
   230
fun hol_type_from_metis_term _ (Metis_Term.Var v) =
blanchet@38748
   231
     (case strip_prefix_and_unascii tvar_prefix v of
blanchet@35865
   232
          SOME w => make_tvar w
blanchet@35865
   233
        | NONE   => make_tvar v)
blanchet@39419
   234
  | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) =
blanchet@38748
   235
     (case strip_prefix_and_unascii type_const_prefix x of
blanchet@38606
   236
          SOME tc => Term.Type (smart_invert_const tc,
blanchet@37926
   237
                                map (hol_type_from_metis_term ctxt) tys)
wenzelm@32956
   238
        | NONE    =>
blanchet@38748
   239
      case strip_prefix_and_unascii tfree_prefix x of
wenzelm@32956
   240
          SOME tf => mk_tfree ctxt tf
blanchet@37926
   241
        | NONE    => raise Fail ("hol_type_from_metis_term: " ^ x));
paulson@32532
   242
wenzelm@32956
   243
(*Maps metis terms to isabelle terms*)
blanchet@37926
   244
fun hol_term_from_metis_PT ctxt fol_tm =
wenzelm@32956
   245
  let val thy = ProofContext.theory_of ctxt
blanchet@37926
   246
      val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
blanchet@39419
   247
                                  Metis_Term.toString fol_tm)
blanchet@39419
   248
      fun tm_to_tt (Metis_Term.Var v) =
blanchet@38748
   249
             (case strip_prefix_and_unascii tvar_prefix v of
blanchet@35865
   250
                  SOME w => Type (make_tvar w)
wenzelm@32956
   251
                | NONE =>
blanchet@38748
   252
              case strip_prefix_and_unascii schematic_var_prefix v of
wenzelm@32956
   253
                  SOME w => Term (mk_var (w, HOLogic.typeT))
wenzelm@32956
   254
                | NONE   => Term (mk_var (v, HOLogic.typeT)) )
wenzelm@32956
   255
                    (*Var from Metis with a name like _nnn; possibly a type variable*)
blanchet@39419
   256
        | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
blanchet@39419
   257
        | tm_to_tt (t as Metis_Term.Fn (".",_)) =
wenzelm@32956
   258
            let val (rator,rands) = strip_happ [] t
wenzelm@32956
   259
            in  case rator of
blanchet@39419
   260
                    Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
wenzelm@32956
   261
                  | _ => case tm_to_tt rator of
wenzelm@32956
   262
                             Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
blanchet@37402
   263
                           | _ => raise Fail "tm_to_tt: HO application"
wenzelm@32956
   264
            end
blanchet@39419
   265
        | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args)
wenzelm@32956
   266
      and applic_to_tt ("=",ts) =
haftmann@38864
   267
            Term (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
wenzelm@32956
   268
        | applic_to_tt (a,ts) =
blanchet@38748
   269
            case strip_prefix_and_unascii const_prefix a of
wenzelm@32956
   270
                SOME b =>
blanchet@38606
   271
                  let val c = smart_invert_const b
blanchet@36909
   272
                      val ntypes = num_type_args thy c
wenzelm@32956
   273
                      val nterms = length ts - ntypes
wenzelm@32956
   274
                      val tts = map tm_to_tt ts
wenzelm@32956
   275
                      val tys = types_of (List.take(tts,ntypes))
blanchet@36909
   276
                  in if length tys = ntypes then
wenzelm@32956
   277
                         apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
blanchet@37402
   278
                     else
blanchet@37402
   279
                       raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
blanchet@37402
   280
                                   " but gets " ^ Int.toString (length tys) ^
blanchet@37402
   281
                                   " type arguments\n" ^
blanchet@37402
   282
                                   cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
blanchet@37402
   283
                                   " the terms are \n" ^
blanchet@37402
   284
                                   cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
wenzelm@32956
   285
                     end
wenzelm@32956
   286
              | NONE => (*Not a constant. Is it a type constructor?*)
blanchet@38748
   287
            case strip_prefix_and_unascii type_const_prefix a of
wenzelm@33227
   288
                SOME b =>
blanchet@38606
   289
                  Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
wenzelm@32956
   290
              | NONE => (*Maybe a TFree. Should then check that ts=[].*)
blanchet@38748
   291
            case strip_prefix_and_unascii tfree_prefix a of
wenzelm@32956
   292
                SOME b => Type (mk_tfree ctxt b)
wenzelm@32956
   293
              | NONE => (*a fixed variable? They are Skolem functions.*)
blanchet@38748
   294
            case strip_prefix_and_unascii fixed_var_prefix a of
wenzelm@32956
   295
                SOME b =>
wenzelm@32956
   296
                  let val opr = Term.Free(b, HOLogic.typeT)
wenzelm@32956
   297
                  in  apply_list opr (length ts) (map tm_to_tt ts)  end
blanchet@37402
   298
              | NONE => raise Fail ("unexpected metis function: " ^ a)
blanchet@37399
   299
  in
blanchet@37399
   300
    case tm_to_tt fol_tm of
blanchet@37399
   301
      Term t => t
blanchet@37402
   302
    | _ => raise Fail "fol_tm_to_tt: Term expected"
blanchet@37399
   303
  end
wenzelm@23442
   304
wenzelm@32956
   305
(*Maps fully-typed metis terms to isabelle terms*)
blanchet@37926
   306
fun hol_term_from_metis_FT ctxt fol_tm =
blanchet@37926
   307
  let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
blanchet@39419
   308
                                  Metis_Term.toString fol_tm)
blanchet@39419
   309
      fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
blanchet@38748
   310
             (case strip_prefix_and_unascii schematic_var_prefix v of
wenzelm@32956
   311
                  SOME w =>  mk_var(w, dummyT)
wenzelm@32956
   312
                | NONE   => mk_var(v, dummyT))
blanchet@39419
   313
        | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) =
haftmann@38864
   314
            Const (@{const_name HOL.eq}, HOLogic.typeT)
blanchet@39419
   315
        | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) =
blanchet@38748
   316
           (case strip_prefix_and_unascii const_prefix x of
blanchet@38606
   317
                SOME c => Const (smart_invert_const c, dummyT)
wenzelm@32956
   318
              | NONE => (*Not a constant. Is it a fixed variable??*)
blanchet@38748
   319
            case strip_prefix_and_unascii fixed_var_prefix x of
blanchet@37926
   320
                SOME v => Free (v, hol_type_from_metis_term ctxt ty)
blanchet@37926
   321
              | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
blanchet@39419
   322
        | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) =
wenzelm@32956
   323
            cvt tm1 $ cvt tm2
blanchet@39419
   324
        | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*)
wenzelm@32956
   325
            cvt tm1 $ cvt tm2
blanchet@39419
   326
        | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
blanchet@39419
   327
        | cvt (Metis_Term.Fn ("=", [tm1,tm2])) =
haftmann@38864
   328
            list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2])
blanchet@39419
   329
        | cvt (t as Metis_Term.Fn (x, [])) =
blanchet@38748
   330
           (case strip_prefix_and_unascii const_prefix x of
blanchet@38606
   331
                SOME c => Const (smart_invert_const c, dummyT)
wenzelm@32956
   332
              | NONE => (*Not a constant. Is it a fixed variable??*)
blanchet@38748
   333
            case strip_prefix_and_unascii fixed_var_prefix x of
wenzelm@32956
   334
                SOME v => Free (v, dummyT)
blanchet@37926
   335
              | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
blanchet@37926
   336
                  hol_term_from_metis_PT ctxt t))
blanchet@39419
   337
        | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
blanchet@37926
   338
            hol_term_from_metis_PT ctxt t)
blanchet@37399
   339
  in fol_tm |> cvt end
paulson@32532
   340
blanchet@37926
   341
fun hol_term_from_metis FT = hol_term_from_metis_FT
blanchet@37926
   342
  | hol_term_from_metis _ = hol_term_from_metis_PT
paulson@32532
   343
blanchet@37625
   344
fun hol_terms_from_fol ctxt mode skolems fol_tms =
blanchet@37926
   345
  let val ts = map (hol_term_from_metis mode ctxt) fol_tms
wenzelm@32956
   346
      val _ = trace_msg (fn () => "  calling type inference:")
wenzelm@32956
   347
      val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
blanchet@37625
   348
      val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt
wenzelm@32956
   349
      val _ = app (fn t => trace_msg
wenzelm@32956
   350
                    (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
wenzelm@32956
   351
                              "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
wenzelm@32956
   352
                  ts'
wenzelm@32956
   353
  in  ts'  end;
wenzelm@23442
   354
blanchet@35865
   355
fun mk_not (Const (@{const_name Not}, _) $ b) = b
wenzelm@32956
   356
  | mk_not b = HOLogic.mk_not b;
wenzelm@23442
   357
blanchet@39419
   358
val metis_eq = Metis_Term.Fn ("=", []);
paulson@32532
   359
wenzelm@32956
   360
(* ------------------------------------------------------------------------- *)
wenzelm@32956
   361
(* FOL step Inference Rules                                                  *)
wenzelm@32956
   362
(* ------------------------------------------------------------------------- *)
wenzelm@23442
   363
wenzelm@32956
   364
(*for debugging only*)
blanchet@39376
   365
(*
wenzelm@32956
   366
fun print_thpair (fth,th) =
wenzelm@32956
   367
  (trace_msg (fn () => "=============================================");
blanchet@39419
   368
   trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth);
wenzelm@32956
   369
   trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
blanchet@39376
   370
*)
wenzelm@23442
   371
blanchet@39419
   372
fun lookth thpairs (fth : Metis_Thm.thm) =
blanchet@39419
   373
  the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth)
blanchet@37402
   374
  handle Option =>
blanchet@39419
   375
         raise Fail ("Failed to find a Metis theorem " ^ Metis_Thm.toString fth);
wenzelm@23442
   376
wenzelm@32956
   377
fun is_TrueI th = Thm.eq_thm(TrueI,th);
wenzelm@23442
   378
wenzelm@32956
   379
fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
paulson@24974
   380
wenzelm@32956
   381
fun inst_excluded_middle thy i_atm =
wenzelm@32956
   382
  let val th = EXCLUDED_MIDDLE
wenzelm@32956
   383
      val [vx] = Term.add_vars (prop_of th) []
wenzelm@32956
   384
      val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
wenzelm@32956
   385
  in  cterm_instantiate substs th  end;
wenzelm@23442
   386
wenzelm@32956
   387
(* INFERENCE RULE: AXIOM *)
wenzelm@36945
   388
fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
wenzelm@32956
   389
    (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
wenzelm@23442
   390
wenzelm@32956
   391
(* INFERENCE RULE: ASSUME *)
blanchet@37625
   392
fun assume_inf ctxt mode skolems atm =
wenzelm@32956
   393
  inst_excluded_middle
blanchet@37625
   394
      (ProofContext.theory_of ctxt)
blanchet@39419
   395
      (singleton (hol_terms_from_fol ctxt mode skolems) (Metis_Term.Fn atm))
wenzelm@23442
   396
wenzelm@32956
   397
(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
wenzelm@32956
   398
   them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
wenzelm@32956
   399
   that new TVars are distinct and that types can be inferred from terms.*)
blanchet@37625
   400
fun inst_inf ctxt mode skolems thpairs fsubst th =
wenzelm@32956
   401
  let val thy = ProofContext.theory_of ctxt
wenzelm@32956
   402
      val i_th   = lookth thpairs th
wenzelm@32956
   403
      val i_th_vars = Term.add_vars (prop_of i_th) []
wenzelm@33035
   404
      fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
wenzelm@32956
   405
      fun subst_translation (x,y) =
wenzelm@32956
   406
            let val v = find_var x
blanchet@37625
   407
                (* We call "reveal_skolem_terms" and "infer_types" below. *)
blanchet@37926
   408
                val t = hol_term_from_metis mode ctxt y
wenzelm@32956
   409
            in  SOME (cterm_of thy (Var v), t)  end
wenzelm@32956
   410
            handle Option =>
blanchet@39356
   411
                (trace_msg (fn() => "\"find_var\" failed for the variable " ^ x ^
wenzelm@32956
   412
                                       " in " ^ Display.string_of_thm ctxt i_th);
wenzelm@32956
   413
                 NONE)
wenzelm@32956
   414
      fun remove_typeinst (a, t) =
blanchet@38748
   415
            case strip_prefix_and_unascii schematic_var_prefix a of
wenzelm@32956
   416
                SOME b => SOME (b, t)
blanchet@38748
   417
              | NONE => case strip_prefix_and_unascii tvar_prefix a of
wenzelm@32956
   418
                SOME _ => NONE          (*type instantiations are forbidden!*)
blanchet@38748
   419
              | NONE => SOME (a,t)    (*internal Metis var?*)
wenzelm@32956
   420
      val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
blanchet@39419
   421
      val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
wenzelm@32956
   422
      val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
blanchet@37625
   423
      val tms = rawtms |> map (reveal_skolem_terms skolems) |> infer_types ctxt
wenzelm@32956
   424
      val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
wenzelm@32956
   425
      val substs' = ListPair.zip (vars, map ctm_of tms)
wenzelm@32956
   426
      val _ = trace_msg (fn () =>
wenzelm@32956
   427
        cat_lines ("subst_translations:" ::
wenzelm@32956
   428
          (substs' |> map (fn (x, y) =>
wenzelm@32956
   429
            Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
wenzelm@32956
   430
            Syntax.string_of_term ctxt (term_of y)))));
blanchet@37399
   431
  in cterm_instantiate substs' i_th end
blanchet@38695
   432
  handle THM (msg, _, _) =>
blanchet@38695
   433
         error ("Cannot replay Metis proof in Isabelle:\n" ^ msg)
wenzelm@23442
   434
wenzelm@32956
   435
(* INFERENCE RULE: RESOLVE *)
wenzelm@25713
   436
blanchet@39267
   437
(* Like RSN, but we rename apart only the type variables. Vars here typically
blanchet@39267
   438
   have an index of 1, and the use of RSN would increase this typically to 3.
blanchet@39267
   439
   Instantiations of those Vars could then fail. See comment on "mk_var". *)
blanchet@39258
   440
fun resolve_inc_tyvars thy tha i thb =
blanchet@37548
   441
  let
blanchet@39266
   442
    val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
blanchet@39258
   443
    fun aux tha thb =
blanchet@39266
   444
      case Thm.bicompose false (false, tha, nprems_of tha) i thb
blanchet@39266
   445
           |> Seq.list_of |> distinct Thm.eq_thm of
blanchet@39266
   446
        [th] => th
blanchet@39266
   447
      | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
blanchet@39266
   448
                        [tha, thb])
wenzelm@32956
   449
  in
blanchet@39258
   450
    aux tha thb
blanchet@39266
   451
    handle TERM z =>
blanchet@39267
   452
           (* The unifier, which is invoked from "Thm.bicompose", will sometimes
blanchet@39267
   453
              refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
blanchet@39267
   454
              "TERM" exception (with "add_ffpair" as first argument). We then
blanchet@39267
   455
              perform unification of the types of variables by hand and try
blanchet@39267
   456
              again. We could do this the first time around but this error
blanchet@39267
   457
              occurs seldom and we don't want to break existing proofs in subtle
blanchet@39267
   458
              ways or slow them down needlessly. *)
blanchet@39266
   459
           case [] |> fold (Term.add_vars o prop_of) [tha, thb]
blanchet@39266
   460
                   |> AList.group (op =)
blanchet@39266
   461
                   |> maps (fn ((s, _), T :: Ts) =>
blanchet@39266
   462
                               map (fn T' => (Free (s, T), Free (s, T'))) Ts)
blanchet@39266
   463
                   |> rpair (Envir.empty ~1)
blanchet@39266
   464
                   |-> fold (Pattern.unify thy)
blanchet@39266
   465
                   |> Envir.type_env |> Vartab.dest
blanchet@39266
   466
                   |> map (fn (x, (S, T)) =>
blanchet@39266
   467
                              pairself (ctyp_of thy) (TVar (x, S), T)) of
blanchet@39266
   468
             [] => raise TERM z
blanchet@39266
   469
           | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb)
blanchet@37548
   470
  end
wenzelm@23442
   471
blanchet@37625
   472
fun resolve_inf ctxt mode skolems thpairs atm th1 th2 =
wenzelm@32956
   473
  let
blanchet@39258
   474
    val thy = ProofContext.theory_of ctxt
wenzelm@32956
   475
    val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
wenzelm@32956
   476
    val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
wenzelm@32956
   477
    val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
wenzelm@32956
   478
  in
wenzelm@32956
   479
    if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
wenzelm@32956
   480
    else if is_TrueI i_th2 then i_th1
wenzelm@32956
   481
    else
wenzelm@32956
   482
      let
blanchet@37625
   483
        val i_atm = singleton (hol_terms_from_fol ctxt mode skolems)
blanchet@39419
   484
                              (Metis_Term.Fn atm)
wenzelm@32956
   485
        val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
wenzelm@32956
   486
        val prems_th1 = prems_of i_th1
wenzelm@32956
   487
        val prems_th2 = prems_of i_th2
wenzelm@32956
   488
        val index_th1 = get_index (mk_not i_atm) prems_th1
blanchet@37402
   489
              handle Empty => raise Fail "Failed to find literal in th1"
wenzelm@32956
   490
        val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
wenzelm@32956
   491
        val index_th2 = get_index i_atm prems_th2
blanchet@37402
   492
              handle Empty => raise Fail "Failed to find literal in th2"
wenzelm@32956
   493
        val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
blanchet@39258
   494
    in
blanchet@39258
   495
      resolve_inc_tyvars thy (Meson.select_literal index_th1 i_th1) index_th2
blanchet@39258
   496
                         i_th2
blanchet@39258
   497
    end
wenzelm@32956
   498
  end;
wenzelm@23442
   499
wenzelm@32956
   500
(* INFERENCE RULE: REFL *)
wenzelm@32956
   501
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
wenzelm@32956
   502
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
wenzelm@25713
   503
blanchet@37625
   504
fun refl_inf ctxt mode skolems t =
wenzelm@32956
   505
  let val thy = ProofContext.theory_of ctxt
blanchet@37625
   506
      val i_t = singleton (hol_terms_from_fol ctxt mode skolems) t
wenzelm@32956
   507
      val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
wenzelm@32956
   508
      val c_t = cterm_incr_types thy refl_idx i_t
wenzelm@32956
   509
  in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
wenzelm@23442
   510
haftmann@38864
   511
fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0  (*equality has no type arguments*)
blanchet@36909
   512
  | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
wenzelm@32994
   513
  | get_ty_arg_size _ _ = 0;
wenzelm@23442
   514
wenzelm@32956
   515
(* INFERENCE RULE: EQUALITY *)
blanchet@37625
   516
fun equality_inf ctxt mode skolems (pos, atm) fp fr =
wenzelm@32956
   517
  let val thy = ProofContext.theory_of ctxt
blanchet@39419
   518
      val m_tm = Metis_Term.Fn atm
blanchet@37625
   519
      val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolems [m_tm, fr]
wenzelm@32956
   520
      val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
wenzelm@32994
   521
      fun replace_item_list lx 0 (_::ls) = lx::ls
wenzelm@32956
   522
        | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
wenzelm@32956
   523
      fun path_finder_FO tm [] = (tm, Term.Bound 0)
wenzelm@32956
   524
        | path_finder_FO tm (p::ps) =
blanchet@35865
   525
            let val (tm1,args) = strip_comb tm
wenzelm@32956
   526
                val adjustment = get_ty_arg_size thy tm1
wenzelm@32956
   527
                val p' = if adjustment > p then p else p-adjustment
wenzelm@32956
   528
                val tm_p = List.nth(args,p')
blanchet@38695
   529
                  handle Subscript =>
blanchet@38695
   530
                         error ("Cannot replay Metis proof in Isabelle:\n" ^
blanchet@38695
   531
                                "equality_inf: " ^ Int.toString p ^ " adj " ^
blanchet@38695
   532
                                Int.toString adjustment ^ " term " ^
blanchet@38695
   533
                                Syntax.string_of_term ctxt tm)
wenzelm@32956
   534
                val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
wenzelm@32956
   535
                                      "  " ^ Syntax.string_of_term ctxt tm_p)
wenzelm@32956
   536
                val (r,t) = path_finder_FO tm_p ps
wenzelm@32956
   537
            in
wenzelm@32956
   538
                (r, list_comb (tm1, replace_item_list t p' args))
wenzelm@32956
   539
            end
wenzelm@32956
   540
      fun path_finder_HO tm [] = (tm, Term.Bound 0)
wenzelm@32956
   541
        | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
wenzelm@32994
   542
        | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
blanchet@37402
   543
        | path_finder_HO tm ps =
blanchet@37402
   544
          raise Fail ("equality_inf, path_finder_HO: path = " ^
blanchet@37402
   545
                      space_implode " " (map Int.toString ps) ^
blanchet@37402
   546
                      " isa-term: " ^  Syntax.string_of_term ctxt tm)
wenzelm@32956
   547
      fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
blanchet@39419
   548
        | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) =
wenzelm@32956
   549
            path_finder_FT tm ps t1
blanchet@39419
   550
        | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) =
wenzelm@32956
   551
            (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
blanchet@39419
   552
        | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) =
wenzelm@32956
   553
            (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
blanchet@37402
   554
        | path_finder_FT tm ps t =
blanchet@37402
   555
          raise Fail ("equality_inf, path_finder_FT: path = " ^
blanchet@37402
   556
                      space_implode " " (map Int.toString ps) ^
blanchet@37402
   557
                      " isa-term: " ^  Syntax.string_of_term ctxt tm ^
blanchet@39419
   558
                      " fol-term: " ^ Metis_Term.toString t)
wenzelm@32956
   559
      fun path_finder FO tm ps _ = path_finder_FO tm ps
haftmann@38864
   560
        | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ =
wenzelm@32956
   561
             (*equality: not curried, as other predicates are*)
wenzelm@32956
   562
             if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
wenzelm@32956
   563
             else path_finder_HO tm (p::ps)        (*1 selects second operand*)
blanchet@39419
   564
        | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) =
wenzelm@32956
   565
             path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
haftmann@38864
   566
        | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps)
blanchet@39419
   567
                            (Metis_Term.Fn ("=", [t1,t2])) =
wenzelm@32956
   568
             (*equality: not curried, as other predicates are*)
wenzelm@32956
   569
             if p=0 then path_finder_FT tm (0::1::ps)
blanchet@39419
   570
                          (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2]))
wenzelm@32956
   571
                          (*select first operand*)
wenzelm@32956
   572
             else path_finder_FT tm (p::ps)
blanchet@39419
   573
                   (Metis_Term.Fn (".", [metis_eq,t2]))
wenzelm@32956
   574
                   (*1 selects second operand*)
blanchet@39419
   575
        | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
wenzelm@32956
   576
             (*if not equality, ignore head to skip the hBOOL predicate*)
wenzelm@32956
   577
        | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
blanchet@35865
   578
      fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
wenzelm@32956
   579
            let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
wenzelm@32956
   580
            in (tm, nt $ tm_rslt) end
wenzelm@32956
   581
        | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
wenzelm@32956
   582
      val (tm_subst, body) = path_finder_lit i_atm fp
wenzelm@32956
   583
      val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
wenzelm@32956
   584
      val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
wenzelm@32956
   585
      val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
wenzelm@32956
   586
      val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
wenzelm@32956
   587
      val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
wenzelm@36945
   588
      val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
wenzelm@32956
   589
      val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
wenzelm@32956
   590
      val eq_terms = map (pairself (cterm_of thy))
wenzelm@33227
   591
        (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
wenzelm@32956
   592
  in  cterm_instantiate eq_terms subst'  end;
wenzelm@23442
   593
wenzelm@32956
   594
val factor = Seq.hd o distinct_subgoals_tac;
paulson@28528
   595
blanchet@37625
   596
fun step ctxt mode skolems thpairs p =
blanchet@37399
   597
  case p of
blanchet@39419
   598
    (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
blanchet@39419
   599
  | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode skolems f_atm
blanchet@39419
   600
  | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) =>
blanchet@37625
   601
    factor (inst_inf ctxt mode skolems thpairs f_subst f_th1)
blanchet@39419
   602
  | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) =>
blanchet@37625
   603
    factor (resolve_inf ctxt mode skolems thpairs f_atm f_th1 f_th2)
blanchet@39419
   604
  | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode skolems f_tm
blanchet@39419
   605
  | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) =>
blanchet@37625
   606
    equality_inf ctxt mode skolems f_lit f_p f_r
wenzelm@23442
   607
blanchet@35865
   608
fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
wenzelm@23442
   609
blanchet@38280
   610
fun translate_one ctxt mode skolems (fol_th, inf) thpairs =
blanchet@38280
   611
  let
blanchet@38280
   612
    val _ = trace_msg (fn () => "=============================================")
blanchet@39419
   613
    val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
blanchet@39419
   614
    val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
blanchet@38280
   615
    val th = Meson.flexflex_first_order (step ctxt mode skolems
blanchet@38280
   616
                                              thpairs (fol_th, inf))
blanchet@38280
   617
    val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
blanchet@38280
   618
    val _ = trace_msg (fn () => "=============================================")
blanchet@38280
   619
    val n_metis_lits =
blanchet@39419
   620
      length (filter real_literal (Metis_LiteralSet.toList (Metis_Thm.clause fol_th)))
blanchet@38695
   621
    val _ = if nprems_of th = n_metis_lits then ()
blanchet@38695
   622
            else error "Cannot replay Metis proof in Isabelle."
blanchet@38280
   623
  in (fol_th, th) :: thpairs end
wenzelm@23442
   624
wenzelm@32956
   625
(*Determining which axiom clauses are actually used*)
blanchet@39419
   626
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
wenzelm@32994
   627
  | used_axioms _ _ = NONE;
paulson@24855
   628
wenzelm@32956
   629
(* ------------------------------------------------------------------------- *)
wenzelm@32956
   630
(* Translation of HO Clauses                                                 *)
wenzelm@32956
   631
(* ------------------------------------------------------------------------- *)
wenzelm@23442
   632
wenzelm@32956
   633
fun type_ext thy tms =
blanchet@35865
   634
  let val subs = tfree_classes_of_terms tms
blanchet@35865
   635
      val supers = tvar_classes_of_terms tms
blanchet@35865
   636
      and tycons = type_consts_of_terms thy tms
blanchet@35865
   637
      val (supers', arity_clauses) = make_arity_clauses thy tycons supers
blanchet@37925
   638
      val class_rel_clauses = make_class_rel_clauses thy subs supers'
blanchet@37925
   639
  in  map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses
wenzelm@32956
   640
  end;
wenzelm@23442
   641
wenzelm@32956
   642
(* ------------------------------------------------------------------------- *)
wenzelm@32956
   643
(* Logic maps manage the interface between HOL and first-order logic.        *)
wenzelm@32956
   644
(* ------------------------------------------------------------------------- *)
wenzelm@23442
   645
wenzelm@32956
   646
type logic_map =
blanchet@39419
   647
  {axioms: (Metis_Thm.thm * thm) list,
blanchet@37399
   648
   tfrees: type_literal list,
blanchet@37625
   649
   skolems: (string * term) list}
wenzelm@23442
   650
wenzelm@32994
   651
fun const_in_metis c (pred, tm_list) =
wenzelm@32956
   652
  let
blanchet@39419
   653
    fun in_mterm (Metis_Term.Var _) = false
blanchet@39419
   654
      | in_mterm (Metis_Term.Fn (".", tm_list)) = exists in_mterm tm_list
blanchet@39419
   655
      | in_mterm (Metis_Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
wenzelm@32994
   656
  in  c = pred orelse exists in_mterm tm_list  end;
wenzelm@23442
   657
wenzelm@32956
   658
(*Extract TFree constraints from context to include as conjecture clauses*)
wenzelm@32956
   659
fun init_tfrees ctxt =
blanchet@36966
   660
  let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
blanchet@36966
   661
    Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
blanchet@36966
   662
    |> type_literals_for_types
blanchet@36556
   663
  end;
paulson@24937
   664
wenzelm@32956
   665
(*transform isabelle type / arity clause to metis clause *)
wenzelm@32956
   666
fun add_type_thm [] lmap = lmap
blanchet@37625
   667
  | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolems} =
blanchet@37399
   668
      add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
blanchet@37625
   669
                        skolems = skolems}
wenzelm@23442
   670
wenzelm@32956
   671
(*Insert non-logical axioms corresponding to all accumulated TFrees*)
blanchet@37625
   672
fun add_tfrees {axioms, tfrees, skolems} : logic_map =
blanchet@37399
   673
     {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
blanchet@37399
   674
               axioms,
blanchet@37625
   675
      tfrees = tfrees, skolems = skolems}
wenzelm@25713
   676
wenzelm@32956
   677
fun string_of_mode FO = "FO"
wenzelm@32956
   678
  | string_of_mode HO = "HO"
wenzelm@32956
   679
  | string_of_mode FT = "FT"
paulson@32532
   680
blanchet@37479
   681
val helpers =
blanchet@38606
   682
  [("c_COMBI", (false, map (`I) @{thms COMBI_def})),
blanchet@38606
   683
   ("c_COMBK", (false, map (`I) @{thms COMBK_def})),
blanchet@38606
   684
   ("c_COMBB", (false, map (`I) @{thms COMBB_def})),
blanchet@38606
   685
   ("c_COMBC", (false, map (`I) @{thms COMBC_def})),
blanchet@38606
   686
   ("c_COMBS", (false, map (`I) @{thms COMBS_def})),
blanchet@38606
   687
   ("c_fequal", (false, map (rpair @{thm equal_imp_equal})
blanchet@38606
   688
                            @{thms fequal_imp_equal equal_imp_fequal})),
blanchet@38606
   689
   ("c_True", (true, map (`I) @{thms True_or_False})),
blanchet@38606
   690
   ("c_False", (true, map (`I) @{thms True_or_False})),
blanchet@38606
   691
   ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))]
blanchet@37479
   692
blanchet@38100
   693
fun is_quasi_fol_clause thy =
blanchet@37625
   694
  Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
blanchet@37623
   695
wenzelm@32956
   696
(* Function to generate metis clauses, including comb and type clauses *)
wenzelm@32956
   697
fun build_map mode0 ctxt cls ths =
wenzelm@32956
   698
  let val thy = ProofContext.theory_of ctxt
wenzelm@32956
   699
      (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
wenzelm@32956
   700
      fun set_mode FO = FO
blanchet@37399
   701
        | set_mode HO =
blanchet@37623
   702
          if forall (is_quasi_fol_clause thy) (cls @ ths) then FO else HO
wenzelm@32956
   703
        | set_mode FT = FT
wenzelm@32956
   704
      val mode = set_mode mode0
wenzelm@32956
   705
      (*transform isabelle clause to metis clause *)
blanchet@38606
   706
      fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems}
blanchet@38606
   707
                  : logic_map =
blanchet@37399
   708
        let
blanchet@37625
   709
          val (mth, tfree_lits, skolems) =
blanchet@38606
   710
            hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems
blanchet@38606
   711
                           metis_ith
wenzelm@32956
   712
        in
blanchet@38606
   713
           {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
blanchet@37625
   714
            tfrees = union (op =) tfree_lits tfrees, skolems = skolems}
wenzelm@32956
   715
        end;
blanchet@37625
   716
      val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []}
blanchet@38606
   717
                 |> fold (add_thm true o `I) cls
blanchet@37498
   718
                 |> add_tfrees
blanchet@38606
   719
                 |> fold (add_thm false o `I) ths
blanchet@39419
   720
      val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap)
blanchet@37479
   721
      fun is_used c =
blanchet@39419
   722
        exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
blanchet@37399
   723
      val lmap =
blanchet@37479
   724
        if mode = FO then
blanchet@37479
   725
          lmap
blanchet@37479
   726
        else
blanchet@37479
   727
          let
blanchet@37479
   728
            val helper_ths =
blanchet@37479
   729
              helpers |> filter (is_used o fst)
blanchet@38606
   730
                      |> maps (fn (c, (needs_full_types, thms)) =>
blanchet@38606
   731
                                  if not (is_used c) orelse
blanchet@38606
   732
                                     needs_full_types andalso mode <> FT then
blanchet@38606
   733
                                    []
blanchet@37479
   734
                                  else
blanchet@38606
   735
                                    thms)
blanchet@37479
   736
          in lmap |> fold (add_thm false) helper_ths end
blanchet@37410
   737
  in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
wenzelm@23442
   738
wenzelm@32956
   739
fun refute cls =
blanchet@39419
   740
    Metis_Resolution.loop (Metis_Resolution.new Metis_Resolution.default {axioms = cls, conjecture = []});
wenzelm@23442
   741
wenzelm@32956
   742
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
wenzelm@23442
   743
wenzelm@32956
   744
fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);
paulson@24855
   745
blanchet@37573
   746
blanchet@37516
   747
(* Main function to start Metis proof and reconstruction *)
wenzelm@32956
   748
fun FOL_SOLVE mode ctxt cls ths0 =
wenzelm@32956
   749
  let val thy = ProofContext.theory_of ctxt
blanchet@35826
   750
      val th_cls_pairs =
blanchet@38016
   751
        map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy th)) ths0
wenzelm@32956
   752
      val ths = maps #2 th_cls_pairs
wenzelm@32956
   753
      val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
wenzelm@32956
   754
      val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
wenzelm@32956
   755
      val _ = trace_msg (fn () => "THEOREM CLAUSES")
wenzelm@32956
   756
      val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
blanchet@37625
   757
      val (mode, {axioms, tfrees, skolems}) = build_map mode ctxt cls ths
wenzelm@32956
   758
      val _ = if null tfrees then ()
wenzelm@32956
   759
              else (trace_msg (fn () => "TFREE CLAUSES");
blanchet@37643
   760
                    app (fn TyLitFree ((s, _), (s', _)) =>
blanchet@37573
   761
                            trace_msg (fn _ => s ^ "(" ^ s' ^ ")")) tfrees)
wenzelm@32956
   762
      val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
wenzelm@32956
   763
      val thms = map #1 axioms
blanchet@39419
   764
      val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms
wenzelm@32956
   765
      val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
wenzelm@32956
   766
      val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
wenzelm@32956
   767
  in
wenzelm@33317
   768
      case filter (is_false o prop_of) cls of
wenzelm@32956
   769
          false_th::_ => [false_th RS @{thm FalseE}]
wenzelm@32956
   770
        | [] =>
wenzelm@32956
   771
      case refute thms of
blanchet@39419
   772
          Metis_Resolution.Contradiction mth =>
wenzelm@32956
   773
            let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
blanchet@39419
   774
                          Metis_Thm.toString mth)
wenzelm@32956
   775
                val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
wenzelm@32956
   776
                             (*add constraints arising from converting goal to clause form*)
blanchet@39419
   777
                val proof = Metis_Proof.proof mth
blanchet@38280
   778
                val result = fold (translate_one ctxt' mode skolems) proof axioms
wenzelm@32956
   779
                and used = map_filter (used_axioms axioms) proof
wenzelm@32956
   780
                val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
wenzelm@32956
   781
                val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
wenzelm@33305
   782
                val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
wenzelm@33305
   783
                  if common_thm used cls then NONE else SOME name)
wenzelm@32956
   784
            in
blanchet@36383
   785
                if not (null cls) andalso not (common_thm used cls) then
blanchet@36383
   786
                  warning "Metis: The assumptions are inconsistent."
blanchet@36383
   787
                else
blanchet@36383
   788
                  ();
blanchet@36383
   789
                if not (null unused) then
blanchet@36230
   790
                  warning ("Metis: Unused theorems: " ^ commas_quote unused
blanchet@36230
   791
                           ^ ".")
blanchet@36230
   792
                else
blanchet@36230
   793
                  ();
wenzelm@32956
   794
                case result of
wenzelm@32956
   795
                    (_,ith)::_ =>
blanchet@36230
   796
                        (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
wenzelm@32956
   797
                         [ith])
blanchet@38097
   798
                  | _ => (trace_msg (fn () => "Metis: No result"); [])
wenzelm@32956
   799
            end
blanchet@39419
   800
        | Metis_Resolution.Satisfiable _ =>
wenzelm@32956
   801
            (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
blanchet@38097
   802
             [])
wenzelm@32956
   803
  end;
wenzelm@23442
   804
blanchet@38632
   805
(* Extensionalize "th", because that makes sense and that's what Sledgehammer
blanchet@38632
   806
   does, but also keep an unextensionalized version of "th" for backward
blanchet@38632
   807
   compatibility. *)
blanchet@38632
   808
fun also_extensionalize_theorem th =
blanchet@38632
   809
  let val th' = Clausifier.extensionalize_theorem th in
blanchet@38632
   810
    if Thm.eq_thm (th, th') then [th]
blanchet@38632
   811
    else th :: Meson.make_clauses_unsorted [th']
blanchet@38632
   812
  end
blanchet@38632
   813
blanchet@38028
   814
val neg_clausify =
blanchet@38028
   815
  single
blanchet@38028
   816
  #> Meson.make_clauses_unsorted
blanchet@38632
   817
  #> maps also_extensionalize_theorem
blanchet@38028
   818
  #> map Clausifier.introduce_combinators_in_theorem
blanchet@38028
   819
  #> Meson.finish_cnf
blanchet@38028
   820
blanchet@39269
   821
fun preskolem_tac ctxt st0 =
blanchet@39269
   822
  (if exists (Meson.has_too_many_clauses ctxt)
blanchet@39269
   823
             (Logic.prems_of_goal (prop_of st0) 1) then
blanchet@39269
   824
     cnf.cnfx_rewrite_tac ctxt 1
blanchet@39269
   825
   else
blanchet@39269
   826
     all_tac) st0
blanchet@39269
   827
blanchet@38652
   828
val type_has_top_sort =
blanchet@38652
   829
  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
blanchet@38652
   830
blanchet@37516
   831
fun generic_metis_tac mode ctxt ths i st0 =
blanchet@37926
   832
  let
blanchet@37926
   833
    val _ = trace_msg (fn () =>
wenzelm@32956
   834
        "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
wenzelm@32956
   835
  in
blanchet@37626
   836
    if exists_type type_has_top_sort (prop_of st0) then
blanchet@37516
   837
      (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
wenzelm@35568
   838
    else
blanchet@39269
   839
      Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
blanchet@37926
   840
                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
blanchet@37926
   841
                  ctxt i st0
wenzelm@32956
   842
  end
wenzelm@23442
   843
blanchet@37516
   844
val metis_tac = generic_metis_tac HO
blanchet@37516
   845
val metisF_tac = generic_metis_tac FO
blanchet@37516
   846
val metisFT_tac = generic_metis_tac FT
wenzelm@23442
   847
blanchet@38632
   848
(* Whenever "X" has schematic type variables, we treat "using X by metis" as
blanchet@38632
   849
   "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables.
blanchet@38632
   850
   We don't do it for nonschematic facts "X" because this breaks a few proofs
blanchet@38632
   851
   (in the rare and subtle case where a proof relied on extensionality not being
blanchet@38994
   852
   applied) and brings few benefits. *)
blanchet@38632
   853
val has_tvar =
blanchet@38632
   854
  exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
blanchet@37516
   855
fun method name mode =
blanchet@37516
   856
  Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
blanchet@38632
   857
    METHOD (fn facts =>
blanchet@38632
   858
               let
blanchet@38632
   859
                 val (schem_facts, nonschem_facts) =
blanchet@38632
   860
                   List.partition has_tvar facts
blanchet@38632
   861
               in
blanchet@38632
   862
                 HEADGOAL (Method.insert_tac nonschem_facts THEN'
blanchet@38632
   863
                           CHANGED_PROP
blanchet@38632
   864
                           o generic_metis_tac mode ctxt (schem_facts @ ths))
blanchet@38632
   865
               end)))
wenzelm@23442
   866
wenzelm@32956
   867
val setup =
blanchet@37516
   868
  type_lits_setup
blanchet@37516
   869
  #> method @{binding metis} HO "Metis for FOL/HOL problems"
blanchet@37516
   870
  #> method @{binding metisF} FO "Metis for FOL problems"
blanchet@37516
   871
  #> method @{binding metisFT} FT
blanchet@37516
   872
            "Metis for FOL/HOL problems with fully-typed translation"
wenzelm@23442
   873
wenzelm@23442
   874
end;