src/HOL/Tools/Sledgehammer/metis_tactics.ML
author blanchet
Wed Jun 02 17:19:44 2010 +0200 (2010-06-02)
changeset 37323 2f2f0d246d0f
parent 37318 32b3d16b04f6
child 37399 34f080a12063
permissions -rw-r--r--
handle Vampire's definitions smoothly
blanchet@35826
     1
(*  Title:      HOL/Tools/Sledgehammer/metis_tactics.ML
wenzelm@23442
     2
    Author:     Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory
wenzelm@23442
     3
    Copyright   Cambridge University 2007
wenzelm@23447
     4
wenzelm@29266
     5
HOL setup for the Metis prover.
wenzelm@23442
     6
*)
wenzelm@23442
     7
blanchet@35826
     8
signature METIS_TACTICS =
wenzelm@23442
     9
sig
wenzelm@32955
    10
  val trace: bool Unsynchronized.ref
wenzelm@24309
    11
  val type_lits: bool Config.T
wenzelm@24319
    12
  val metis_tac: Proof.context -> thm list -> int -> tactic
wenzelm@24319
    13
  val metisF_tac: Proof.context -> thm list -> int -> tactic
paulson@32532
    14
  val metisFT_tac: Proof.context -> thm list -> int -> tactic
wenzelm@24319
    15
  val setup: theory -> theory
wenzelm@23442
    16
end
wenzelm@23442
    17
blanchet@35826
    18
structure Metis_Tactics : METIS_TACTICS =
wenzelm@23442
    19
struct
wenzelm@23442
    20
blanchet@35865
    21
open Sledgehammer_FOL_Clause
blanchet@35865
    22
open Sledgehammer_Fact_Preprocessor
blanchet@35865
    23
open Sledgehammer_HOL_Clause
blanchet@35865
    24
open Sledgehammer_Proof_Reconstruct
blanchet@35865
    25
open Sledgehammer_Fact_Filter
blanchet@35826
    26
wenzelm@32956
    27
val trace = Unsynchronized.ref false;
blanchet@35826
    28
fun trace_msg msg = if !trace then tracing (msg ()) else ();
wenzelm@32955
    29
wenzelm@36001
    30
val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
wenzelm@23442
    31
blanchet@35826
    32
datatype mode = FO | HO | FT  (* first-order, higher-order, fully-typed *)
paulson@32532
    33
wenzelm@32956
    34
(* ------------------------------------------------------------------------- *)
wenzelm@32956
    35
(* Useful Theorems                                                           *)
wenzelm@32956
    36
(* ------------------------------------------------------------------------- *)
wenzelm@33689
    37
val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
wenzelm@36945
    38
val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
wenzelm@33689
    39
val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
wenzelm@33689
    40
val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
wenzelm@23442
    41
wenzelm@32956
    42
(* ------------------------------------------------------------------------- *)
wenzelm@32956
    43
(* Useful Functions                                                          *)
wenzelm@32956
    44
(* ------------------------------------------------------------------------- *)
wenzelm@23442
    45
wenzelm@32956
    46
(* match untyped terms*)
wenzelm@32956
    47
fun untyped_aconv (Const(a,_))   (Const(b,_))   = (a=b)
wenzelm@32956
    48
  | untyped_aconv (Free(a,_))    (Free(b,_))    = (a=b)
wenzelm@32956
    49
  | untyped_aconv (Var((a,_),_)) (Var((b,_),_)) = (a=b)   (*the index is ignored!*)
wenzelm@32956
    50
  | untyped_aconv (Bound i)      (Bound j)      = (i=j)
wenzelm@32956
    51
  | untyped_aconv (Abs(a,_,t))  (Abs(b,_,u))    = (a=b) andalso untyped_aconv t u
wenzelm@32956
    52
  | untyped_aconv (t1$t2) (u1$u2)  = untyped_aconv t1 u1 andalso untyped_aconv t2 u2
wenzelm@32956
    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
wenzelm@32956
    58
      fun get n [] = 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
wenzelm@32956
    67
fun fn_isa_to_met "equal" = "="
wenzelm@32956
    68
  | fn_isa_to_met x       = x;
wenzelm@23442
    69
wenzelm@32956
    70
fun metis_lit b c args = (b, (c, args));
wenzelm@23442
    71
blanchet@36169
    72
fun hol_type_to_fol (TyVar (x, _)) = Metis.Term.Var x
blanchet@36169
    73
  | hol_type_to_fol (TyFree (s, _)) = Metis.Term.Fn (s, [])
blanchet@36169
    74
  | hol_type_to_fol (TyConstr ((s, _), tps)) =
blanchet@36169
    75
    Metis.Term.Fn (s, map hol_type_to_fol tps);
wenzelm@23442
    76
wenzelm@32956
    77
(*These two functions insert type literals before the real literals. That is the
wenzelm@32956
    78
  opposite order from TPTP linkup, but maybe OK.*)
wenzelm@23442
    79
wenzelm@32956
    80
fun hol_term_to_fol_FO tm =
blanchet@35865
    81
  case strip_combterm_comb tm of
blanchet@36170
    82
      (CombConst ((c, _), _, tys), tms) =>
wenzelm@32956
    83
        let val tyargs = map hol_type_to_fol tys
wenzelm@32956
    84
            val args   = map hol_term_to_fol_FO tms
wenzelm@32956
    85
        in Metis.Term.Fn (c, tyargs @ args) end
blanchet@36170
    86
    | (CombVar ((v, _), _), []) => Metis.Term.Var v
wenzelm@32956
    87
    | _ => error "hol_term_to_fol_FO";
wenzelm@23442
    88
blanchet@36170
    89
fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
blanchet@36170
    90
  | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
wenzelm@32994
    91
      Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
blanchet@35865
    92
  | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
wenzelm@32994
    93
       Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
wenzelm@23442
    94
wenzelm@32956
    95
(*The fully-typed translation, to avoid type errors*)
wenzelm@32956
    96
fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
wenzelm@32956
    97
blanchet@36170
    98
fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty)
blanchet@36170
    99
  | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
wenzelm@32956
   100
      wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
blanchet@35865
   101
  | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
wenzelm@32956
   102
       wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
blanchet@35865
   103
                  type_of_combterm tm);
paulson@32532
   104
blanchet@35865
   105
fun hol_literal_to_fol FO (Literal (pol, tm)) =
blanchet@36170
   106
      let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
wenzelm@32956
   107
          val tylits = if p = "equal" then [] else map hol_type_to_fol tys
wenzelm@32956
   108
          val lits = map hol_term_to_fol_FO tms
wenzelm@32956
   109
      in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
blanchet@35865
   110
  | hol_literal_to_fol HO (Literal (pol, tm)) =
blanchet@35865
   111
     (case strip_combterm_comb tm of
blanchet@36170
   112
          (CombConst(("equal", _), _, _), tms) =>
wenzelm@32956
   113
            metis_lit pol "=" (map hol_term_to_fol_HO tms)
wenzelm@32956
   114
        | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
blanchet@35865
   115
  | hol_literal_to_fol FT (Literal (pol, tm)) =
blanchet@35865
   116
     (case strip_combterm_comb tm of
blanchet@36170
   117
          (CombConst(("equal", _), _, _), tms) =>
wenzelm@32956
   118
            metis_lit pol "=" (map hol_term_to_fol_FT tms)
wenzelm@32956
   119
        | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
wenzelm@23442
   120
wenzelm@32956
   121
fun literals_of_hol_thm thy mode t =
blanchet@35865
   122
      let val (lits, types_sorts) = literals_of_term thy t
wenzelm@32956
   123
      in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
wenzelm@23442
   124
wenzelm@32956
   125
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
blanchet@36556
   126
fun metis_of_type_literals pos (TyLitVar (s, (s', _))) =
blanchet@36556
   127
    metis_lit pos s [Metis.Term.Var s']
blanchet@36556
   128
  | metis_of_type_literals pos (TyLitFree (s, (s', _))) =
blanchet@36556
   129
    metis_lit pos s [Metis.Term.Fn (s',[])]
wenzelm@23442
   130
wenzelm@32994
   131
fun default_sort _ (TVar _) = false
wenzelm@33035
   132
  | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
wenzelm@23442
   133
wenzelm@32956
   134
fun metis_of_tfree tf =
blanchet@36556
   135
  Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf));
paulson@24937
   136
wenzelm@32956
   137
fun hol_thm_to_fol is_conjecture ctxt mode th =
wenzelm@32956
   138
  let val thy = ProofContext.theory_of ctxt
wenzelm@32956
   139
      val (mlits, types_sorts) =
wenzelm@32956
   140
             (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
wenzelm@32956
   141
  in
wenzelm@32956
   142
      if is_conjecture then
blanchet@36556
   143
          (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
blanchet@36966
   144
           type_literals_for_types types_sorts)
wenzelm@32956
   145
      else
blanchet@36966
   146
        let val tylits = filter_out (default_sort ctxt) types_sorts
blanchet@36966
   147
                         |> type_literals_for_types
wenzelm@32956
   148
            val mtylits = if Config.get ctxt type_lits
blanchet@36556
   149
                          then map (metis_of_type_literals false) tylits else []
wenzelm@32956
   150
        in
wenzelm@32956
   151
          (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
wenzelm@32956
   152
        end
wenzelm@32956
   153
  end;
wenzelm@23442
   154
wenzelm@32956
   155
(* ARITY CLAUSE *)
wenzelm@23442
   156
blanchet@35865
   157
fun m_arity_cls (TConsLit (c,t,args)) =
blanchet@35865
   158
      metis_lit true (make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
blanchet@35865
   159
  | m_arity_cls (TVarLit (c,str))     =
blanchet@35865
   160
      metis_lit false (make_type_class c) [Metis.Term.Var str];
wenzelm@23442
   161
wenzelm@32956
   162
(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
blanchet@35865
   163
fun arity_cls (ArityClause {conclLit, premLits, ...}) =
wenzelm@32956
   164
  (TrueI,
wenzelm@32956
   165
   Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
wenzelm@23442
   166
wenzelm@32956
   167
(* CLASSREL CLAUSE *)
wenzelm@23442
   168
wenzelm@32956
   169
fun m_classrel_cls subclass superclass =
wenzelm@32956
   170
  [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
wenzelm@23442
   171
blanchet@35865
   172
fun classrel_cls (ClassrelClause {subclass, superclass, ...}) =
wenzelm@32956
   173
  (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
wenzelm@23442
   174
wenzelm@32956
   175
(* ------------------------------------------------------------------------- *)
wenzelm@32956
   176
(* FOL to HOL  (Metis to Isabelle)                                           *)
wenzelm@32956
   177
(* ------------------------------------------------------------------------- *)
wenzelm@23442
   178
wenzelm@32956
   179
datatype term_or_type = Term of Term.term | Type of Term.typ;
wenzelm@23442
   180
wenzelm@32956
   181
fun terms_of [] = []
wenzelm@32956
   182
  | terms_of (Term t :: tts) = t :: terms_of tts
wenzelm@32956
   183
  | terms_of (Type _ :: tts) = terms_of tts;
wenzelm@23442
   184
wenzelm@32956
   185
fun types_of [] = []
wenzelm@32994
   186
  | types_of (Term (Term.Var ((a,idx), _)) :: tts) =
wenzelm@32956
   187
      if String.isPrefix "_" a then
wenzelm@32956
   188
          (*Variable generated by Metis, which might have been a type variable.*)
wenzelm@32994
   189
          TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
wenzelm@32956
   190
      else types_of tts
wenzelm@32956
   191
  | types_of (Term _ :: tts) = types_of tts
wenzelm@32956
   192
  | types_of (Type T :: tts) = T :: types_of tts;
wenzelm@23442
   193
wenzelm@32956
   194
fun apply_list rator nargs rands =
wenzelm@32956
   195
  let val trands = terms_of rands
wenzelm@32956
   196
  in  if length trands = nargs then Term (list_comb(rator, trands))
wenzelm@32956
   197
      else error
wenzelm@32956
   198
        ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
wenzelm@32956
   199
          " expected " ^ Int.toString nargs ^
wenzelm@32956
   200
          " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
wenzelm@32956
   201
  end;
wenzelm@23442
   202
wenzelm@24500
   203
fun infer_types ctxt =
wenzelm@24500
   204
  Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
wenzelm@25713
   205
wenzelm@32956
   206
(*We use 1 rather than 0 because variable references in clauses may otherwise conflict
wenzelm@32956
   207
  with variable constraints in the goal...at least, type inference often fails otherwise.
wenzelm@32956
   208
  SEE ALSO axiom_inf below.*)
wenzelm@32956
   209
fun mk_var (w,T) = Term.Var((w,1), T);
wenzelm@23442
   210
wenzelm@32956
   211
(*include the default sort, if available*)
wenzelm@32956
   212
fun mk_tfree ctxt w =
wenzelm@32956
   213
  let val ww = "'" ^ w
wenzelm@33035
   214
  in  TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))  end;
wenzelm@23442
   215
wenzelm@32956
   216
(*Remove the "apply" operator from an HO term*)
wenzelm@32956
   217
fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
wenzelm@32956
   218
  | strip_happ args x = (x, args);
wenzelm@23442
   219
blanchet@36967
   220
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
blanchet@36967
   221
wenzelm@32994
   222
fun fol_type_to_isa _ (Metis.Term.Var v) =
blanchet@35865
   223
     (case strip_prefix tvar_prefix v of
blanchet@35865
   224
          SOME w => make_tvar w
blanchet@35865
   225
        | NONE   => make_tvar v)
wenzelm@32956
   226
  | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
blanchet@35865
   227
     (case strip_prefix tconst_prefix x of
blanchet@35865
   228
          SOME tc => Term.Type (invert_type_const tc, map (fol_type_to_isa ctxt) tys)
wenzelm@32956
   229
        | NONE    =>
blanchet@35865
   230
      case strip_prefix tfree_prefix x of
wenzelm@32956
   231
          SOME tf => mk_tfree ctxt tf
wenzelm@32956
   232
        | NONE    => error ("fol_type_to_isa: " ^ x));
paulson@32532
   233
wenzelm@32956
   234
(*Maps metis terms to isabelle terms*)
wenzelm@32956
   235
fun fol_term_to_hol_RAW ctxt fol_tm =
wenzelm@32956
   236
  let val thy = ProofContext.theory_of ctxt
wenzelm@32956
   237
      val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
wenzelm@32956
   238
      fun tm_to_tt (Metis.Term.Var v) =
blanchet@35865
   239
             (case strip_prefix tvar_prefix v of
blanchet@35865
   240
                  SOME w => Type (make_tvar w)
wenzelm@32956
   241
                | NONE =>
blanchet@35865
   242
              case strip_prefix schematic_var_prefix v of
wenzelm@32956
   243
                  SOME w => Term (mk_var (w, HOLogic.typeT))
wenzelm@32956
   244
                | NONE   => Term (mk_var (v, HOLogic.typeT)) )
wenzelm@32956
   245
                    (*Var from Metis with a name like _nnn; possibly a type variable*)
wenzelm@32956
   246
        | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
wenzelm@32956
   247
        | tm_to_tt (t as Metis.Term.Fn (".",_)) =
wenzelm@32956
   248
            let val (rator,rands) = strip_happ [] t
wenzelm@32956
   249
            in  case rator of
wenzelm@32956
   250
                    Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
wenzelm@32956
   251
                  | _ => case tm_to_tt rator of
wenzelm@32956
   252
                             Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
wenzelm@32956
   253
                           | _ => error "tm_to_tt: HO application"
wenzelm@32956
   254
            end
wenzelm@32956
   255
        | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
wenzelm@32956
   256
      and applic_to_tt ("=",ts) =
blanchet@35865
   257
            Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
wenzelm@32956
   258
        | applic_to_tt (a,ts) =
blanchet@35865
   259
            case strip_prefix const_prefix a of
wenzelm@32956
   260
                SOME b =>
blanchet@35865
   261
                  let val c = invert_const b
blanchet@36909
   262
                      val ntypes = num_type_args thy c
wenzelm@32956
   263
                      val nterms = length ts - ntypes
wenzelm@32956
   264
                      val tts = map tm_to_tt ts
wenzelm@32956
   265
                      val tys = types_of (List.take(tts,ntypes))
blanchet@36909
   266
                  in if length tys = ntypes then
wenzelm@32956
   267
                         apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
blanchet@36909
   268
                     else error ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
wenzelm@32956
   269
                                 " but gets " ^ Int.toString (length tys) ^
wenzelm@32956
   270
                                 " type arguments\n" ^
wenzelm@32956
   271
                                 cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
wenzelm@32956
   272
                                 " the terms are \n" ^
wenzelm@32956
   273
                                 cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
wenzelm@32956
   274
                     end
wenzelm@32956
   275
              | NONE => (*Not a constant. Is it a type constructor?*)
blanchet@35865
   276
            case strip_prefix tconst_prefix a of
wenzelm@33227
   277
                SOME b =>
blanchet@35865
   278
                  Type (Term.Type (invert_type_const b, types_of (map tm_to_tt ts)))
wenzelm@32956
   279
              | NONE => (*Maybe a TFree. Should then check that ts=[].*)
blanchet@35865
   280
            case strip_prefix tfree_prefix a of
wenzelm@32956
   281
                SOME b => Type (mk_tfree ctxt b)
wenzelm@32956
   282
              | NONE => (*a fixed variable? They are Skolem functions.*)
blanchet@35865
   283
            case strip_prefix fixed_var_prefix a of
wenzelm@32956
   284
                SOME b =>
wenzelm@32956
   285
                  let val opr = Term.Free(b, HOLogic.typeT)
wenzelm@32956
   286
                  in  apply_list opr (length ts) (map tm_to_tt ts)  end
wenzelm@32956
   287
              | NONE => error ("unexpected metis function: " ^ a)
wenzelm@32956
   288
  in  case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected"  end;
wenzelm@23442
   289
wenzelm@32956
   290
(*Maps fully-typed metis terms to isabelle terms*)
wenzelm@32956
   291
fun fol_term_to_hol_FT ctxt fol_tm =
wenzelm@32956
   292
  let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
wenzelm@32994
   293
      fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
blanchet@35865
   294
             (case strip_prefix schematic_var_prefix v of
wenzelm@32956
   295
                  SOME w =>  mk_var(w, dummyT)
wenzelm@32956
   296
                | NONE   => mk_var(v, dummyT))
wenzelm@32994
   297
        | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
wenzelm@32956
   298
            Const ("op =", HOLogic.typeT)
wenzelm@32956
   299
        | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
blanchet@35865
   300
           (case strip_prefix const_prefix x of
blanchet@35865
   301
                SOME c => Const (invert_const c, dummyT)
wenzelm@32956
   302
              | NONE => (*Not a constant. Is it a fixed variable??*)
blanchet@35865
   303
            case strip_prefix fixed_var_prefix x of
wenzelm@32956
   304
                SOME v => Free (v, fol_type_to_isa ctxt ty)
wenzelm@32956
   305
              | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
wenzelm@32956
   306
        | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
wenzelm@32956
   307
            cvt tm1 $ cvt tm2
wenzelm@32956
   308
        | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
wenzelm@32956
   309
            cvt tm1 $ cvt tm2
wenzelm@32956
   310
        | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
wenzelm@32956
   311
        | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
blanchet@35865
   312
            list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
wenzelm@32956
   313
        | cvt (t as Metis.Term.Fn (x, [])) =
blanchet@35865
   314
           (case strip_prefix const_prefix x of
blanchet@35865
   315
                SOME c => Const (invert_const c, dummyT)
wenzelm@32956
   316
              | NONE => (*Not a constant. Is it a fixed variable??*)
blanchet@35865
   317
            case strip_prefix fixed_var_prefix x of
wenzelm@32956
   318
                SOME v => Free (v, dummyT)
wenzelm@33227
   319
              | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x);
wenzelm@33227
   320
                  fol_term_to_hol_RAW ctxt t))
wenzelm@33227
   321
        | cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t);
wenzelm@33227
   322
            fol_term_to_hol_RAW ctxt t)
wenzelm@32956
   323
  in  cvt fol_tm   end;
paulson@32532
   324
wenzelm@32956
   325
fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt
wenzelm@32956
   326
  | fol_term_to_hol ctxt HO = fol_term_to_hol_RAW ctxt
wenzelm@32956
   327
  | fol_term_to_hol ctxt FT = fol_term_to_hol_FT ctxt;
paulson@32532
   328
wenzelm@32956
   329
fun fol_terms_to_hol ctxt mode fol_tms =
wenzelm@32956
   330
  let val ts = map (fol_term_to_hol ctxt mode) fol_tms
wenzelm@32956
   331
      val _ = trace_msg (fn () => "  calling type inference:")
wenzelm@32956
   332
      val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
wenzelm@32956
   333
      val ts' = infer_types ctxt ts;
wenzelm@32956
   334
      val _ = app (fn t => trace_msg
wenzelm@32956
   335
                    (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
wenzelm@32956
   336
                              "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
wenzelm@32956
   337
                  ts'
wenzelm@32956
   338
  in  ts'  end;
wenzelm@23442
   339
blanchet@35865
   340
fun mk_not (Const (@{const_name Not}, _) $ b) = b
wenzelm@32956
   341
  | mk_not b = HOLogic.mk_not b;
wenzelm@23442
   342
wenzelm@32956
   343
val metis_eq = Metis.Term.Fn ("=", []);
paulson@32532
   344
wenzelm@32956
   345
(* ------------------------------------------------------------------------- *)
wenzelm@32956
   346
(* FOL step Inference Rules                                                  *)
wenzelm@32956
   347
(* ------------------------------------------------------------------------- *)
wenzelm@23442
   348
wenzelm@32956
   349
(*for debugging only*)
wenzelm@32956
   350
fun print_thpair (fth,th) =
wenzelm@32956
   351
  (trace_msg (fn () => "=============================================");
wenzelm@32956
   352
   trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth);
wenzelm@32956
   353
   trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
wenzelm@23442
   354
wenzelm@32956
   355
fun lookth thpairs (fth : Metis.Thm.thm) =
wenzelm@33035
   356
  the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
wenzelm@32956
   357
  handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
wenzelm@23442
   358
wenzelm@32956
   359
fun is_TrueI th = Thm.eq_thm(TrueI,th);
wenzelm@23442
   360
wenzelm@32956
   361
fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
paulson@24974
   362
wenzelm@32956
   363
fun inst_excluded_middle thy i_atm =
wenzelm@32956
   364
  let val th = EXCLUDED_MIDDLE
wenzelm@32956
   365
      val [vx] = Term.add_vars (prop_of th) []
wenzelm@32956
   366
      val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
wenzelm@32956
   367
  in  cterm_instantiate substs th  end;
wenzelm@23442
   368
wenzelm@32956
   369
(* INFERENCE RULE: AXIOM *)
wenzelm@36945
   370
fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
wenzelm@32956
   371
    (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
wenzelm@23442
   372
wenzelm@32956
   373
(* INFERENCE RULE: ASSUME *)
wenzelm@32956
   374
fun assume_inf ctxt mode atm =
wenzelm@32956
   375
  inst_excluded_middle
wenzelm@32956
   376
    (ProofContext.theory_of ctxt)
wenzelm@32956
   377
    (singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm));
wenzelm@23442
   378
wenzelm@32956
   379
(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
wenzelm@32956
   380
   them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
wenzelm@32956
   381
   that new TVars are distinct and that types can be inferred from terms.*)
wenzelm@32956
   382
fun inst_inf ctxt mode thpairs fsubst th =
wenzelm@32956
   383
  let val thy = ProofContext.theory_of ctxt
wenzelm@32956
   384
      val i_th   = lookth thpairs th
wenzelm@32956
   385
      val i_th_vars = Term.add_vars (prop_of i_th) []
wenzelm@33035
   386
      fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
wenzelm@32956
   387
      fun subst_translation (x,y) =
wenzelm@32956
   388
            let val v = find_var x
wenzelm@32956
   389
                val t = fol_term_to_hol ctxt mode y (*we call infer_types below*)
wenzelm@32956
   390
            in  SOME (cterm_of thy (Var v), t)  end
wenzelm@32956
   391
            handle Option =>
wenzelm@32956
   392
                (trace_msg (fn() => "List.find failed for the variable " ^ x ^
wenzelm@32956
   393
                                       " in " ^ Display.string_of_thm ctxt i_th);
wenzelm@32956
   394
                 NONE)
wenzelm@32956
   395
      fun remove_typeinst (a, t) =
blanchet@35865
   396
            case strip_prefix schematic_var_prefix a of
wenzelm@32956
   397
                SOME b => SOME (b, t)
blanchet@35865
   398
              | NONE   => case strip_prefix tvar_prefix a of
wenzelm@32956
   399
                SOME _ => NONE          (*type instantiations are forbidden!*)
wenzelm@32956
   400
              | NONE   => SOME (a,t)    (*internal Metis var?*)
wenzelm@32956
   401
      val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
wenzelm@32956
   402
      val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
wenzelm@32956
   403
      val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
wenzelm@32956
   404
      val tms = infer_types ctxt rawtms;
wenzelm@32956
   405
      val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
wenzelm@32956
   406
      val substs' = ListPair.zip (vars, map ctm_of tms)
wenzelm@32956
   407
      val _ = trace_msg (fn () =>
wenzelm@32956
   408
        cat_lines ("subst_translations:" ::
wenzelm@32956
   409
          (substs' |> map (fn (x, y) =>
wenzelm@32956
   410
            Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
wenzelm@32956
   411
            Syntax.string_of_term ctxt (term_of y)))));
blanchet@37318
   412
  in  cterm_instantiate substs' i_th end
blanchet@37318
   413
  handle THM (msg, _, _) => error ("metis error (inst_inf):\n" ^ msg)
blanchet@37318
   414
       | ERROR msg => error ("metis error (inst_inf):\n" ^ msg ^
blanchet@37318
   415
                             "\n(Perhaps you want to try \"metisFT\".)")
wenzelm@23442
   416
wenzelm@32956
   417
(* INFERENCE RULE: RESOLVE *)
wenzelm@25713
   418
wenzelm@32956
   419
(*Like RSN, but we rename apart only the type variables. Vars here typically have an index
wenzelm@32956
   420
  of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars
wenzelm@32956
   421
  could then fail. See comment on mk_var.*)
wenzelm@32956
   422
fun resolve_inc_tyvars(tha,i,thb) =
wenzelm@32956
   423
  let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
wenzelm@32956
   424
      val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
wenzelm@32956
   425
  in
wenzelm@32956
   426
      case distinct Thm.eq_thm ths of
wenzelm@32956
   427
        [th] => th
wenzelm@32956
   428
      | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
wenzelm@32956
   429
  end;
wenzelm@23442
   430
wenzelm@32956
   431
fun resolve_inf ctxt mode thpairs atm th1 th2 =
wenzelm@32956
   432
  let
wenzelm@32956
   433
    val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
wenzelm@32956
   434
    val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
wenzelm@32956
   435
    val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
wenzelm@32956
   436
  in
wenzelm@32956
   437
    if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*)
wenzelm@32956
   438
    else if is_TrueI i_th2 then i_th1
wenzelm@32956
   439
    else
wenzelm@32956
   440
      let
wenzelm@32956
   441
        val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)
wenzelm@32956
   442
        val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
wenzelm@32956
   443
        val prems_th1 = prems_of i_th1
wenzelm@32956
   444
        val prems_th2 = prems_of i_th2
wenzelm@32956
   445
        val index_th1 = get_index (mk_not i_atm) prems_th1
wenzelm@32956
   446
              handle Empty => error "Failed to find literal in th1"
wenzelm@32956
   447
        val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
wenzelm@32956
   448
        val index_th2 = get_index i_atm prems_th2
wenzelm@32956
   449
              handle Empty => error "Failed to find literal in th2"
wenzelm@32956
   450
        val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
wenzelm@32956
   451
    in  resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2)  end
wenzelm@32956
   452
  end;
wenzelm@23442
   453
wenzelm@32956
   454
(* INFERENCE RULE: REFL *)
wenzelm@32956
   455
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
wenzelm@32956
   456
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
wenzelm@25713
   457
wenzelm@32956
   458
fun refl_inf ctxt mode t =
wenzelm@32956
   459
  let val thy = ProofContext.theory_of ctxt
wenzelm@32956
   460
      val i_t = singleton (fol_terms_to_hol ctxt mode) t
wenzelm@32956
   461
      val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
wenzelm@32956
   462
      val c_t = cterm_incr_types thy refl_idx i_t
wenzelm@32956
   463
  in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
wenzelm@23442
   464
blanchet@35865
   465
fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0  (*equality has no type arguments*)
blanchet@36909
   466
  | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
wenzelm@32994
   467
  | get_ty_arg_size _ _ = 0;
wenzelm@23442
   468
wenzelm@32956
   469
(* INFERENCE RULE: EQUALITY *)
wenzelm@32994
   470
fun equality_inf ctxt mode (pos, atm) fp fr =
wenzelm@32956
   471
  let val thy = ProofContext.theory_of ctxt
wenzelm@32956
   472
      val m_tm = Metis.Term.Fn atm
wenzelm@32956
   473
      val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
wenzelm@32956
   474
      val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
wenzelm@32994
   475
      fun replace_item_list lx 0 (_::ls) = lx::ls
wenzelm@32956
   476
        | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
wenzelm@32956
   477
      fun path_finder_FO tm [] = (tm, Term.Bound 0)
wenzelm@32956
   478
        | path_finder_FO tm (p::ps) =
blanchet@35865
   479
            let val (tm1,args) = strip_comb tm
wenzelm@32956
   480
                val adjustment = get_ty_arg_size thy tm1
wenzelm@32956
   481
                val p' = if adjustment > p then p else p-adjustment
wenzelm@32956
   482
                val tm_p = List.nth(args,p')
wenzelm@32956
   483
                  handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
wenzelm@32956
   484
                    Int.toString adjustment  ^ " term " ^  Syntax.string_of_term ctxt tm)
wenzelm@32956
   485
                val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
wenzelm@32956
   486
                                      "  " ^ Syntax.string_of_term ctxt tm_p)
wenzelm@32956
   487
                val (r,t) = path_finder_FO tm_p ps
wenzelm@32956
   488
            in
wenzelm@32956
   489
                (r, list_comb (tm1, replace_item_list t p' args))
wenzelm@32956
   490
            end
wenzelm@32956
   491
      fun path_finder_HO tm [] = (tm, Term.Bound 0)
wenzelm@32956
   492
        | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
wenzelm@32994
   493
        | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
wenzelm@32956
   494
      fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
wenzelm@32994
   495
        | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) =
wenzelm@32956
   496
            path_finder_FT tm ps t1
wenzelm@32994
   497
        | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1, _])) =
wenzelm@32956
   498
            (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
wenzelm@32994
   499
        | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) =
wenzelm@32956
   500
            (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
wenzelm@32956
   501
        | path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^
wenzelm@32956
   502
                                        space_implode " " (map Int.toString ps) ^
wenzelm@32956
   503
                                        " isa-term: " ^  Syntax.string_of_term ctxt tm ^
wenzelm@32956
   504
                                        " fol-term: " ^ Metis.Term.toString t)
wenzelm@32956
   505
      fun path_finder FO tm ps _ = path_finder_FO tm ps
blanchet@35865
   506
        | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
wenzelm@32956
   507
             (*equality: not curried, as other predicates are*)
wenzelm@32956
   508
             if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
wenzelm@32956
   509
             else path_finder_HO tm (p::ps)        (*1 selects second operand*)
wenzelm@32994
   510
        | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
wenzelm@32956
   511
             path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
blanchet@35865
   512
        | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
wenzelm@32956
   513
                            (Metis.Term.Fn ("=", [t1,t2])) =
wenzelm@32956
   514
             (*equality: not curried, as other predicates are*)
wenzelm@32956
   515
             if p=0 then path_finder_FT tm (0::1::ps)
wenzelm@32956
   516
                          (Metis.Term.Fn (".", [Metis.Term.Fn (".", [metis_eq,t1]), t2]))
wenzelm@32956
   517
                          (*select first operand*)
wenzelm@32956
   518
             else path_finder_FT tm (p::ps)
wenzelm@32956
   519
                   (Metis.Term.Fn (".", [metis_eq,t2]))
wenzelm@32956
   520
                   (*1 selects second operand*)
wenzelm@32994
   521
        | path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
wenzelm@32956
   522
             (*if not equality, ignore head to skip the hBOOL predicate*)
wenzelm@32956
   523
        | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
blanchet@35865
   524
      fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
wenzelm@32956
   525
            let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
wenzelm@32956
   526
            in (tm, nt $ tm_rslt) end
wenzelm@32956
   527
        | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
wenzelm@32956
   528
      val (tm_subst, body) = path_finder_lit i_atm fp
wenzelm@32956
   529
      val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
wenzelm@32956
   530
      val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
wenzelm@32956
   531
      val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
wenzelm@32956
   532
      val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
wenzelm@32956
   533
      val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
wenzelm@36945
   534
      val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
wenzelm@32956
   535
      val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
wenzelm@32956
   536
      val eq_terms = map (pairself (cterm_of thy))
wenzelm@33227
   537
        (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
wenzelm@32956
   538
  in  cterm_instantiate eq_terms subst'  end;
wenzelm@23442
   539
wenzelm@32956
   540
val factor = Seq.hd o distinct_subgoals_tac;
paulson@28528
   541
wenzelm@32994
   542
fun step _ _ thpairs (fol_th, Metis.Proof.Axiom _) = factor (axiom_inf thpairs fol_th)
wenzelm@32994
   543
  | step ctxt mode _ (_, Metis.Proof.Assume f_atm) = assume_inf ctxt mode f_atm
wenzelm@32994
   544
  | step ctxt mode thpairs (_, Metis.Proof.Subst (f_subst, f_th1)) =
wenzelm@32956
   545
      factor (inst_inf ctxt mode thpairs f_subst f_th1)
wenzelm@32994
   546
  | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =
wenzelm@32956
   547
      factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2)
wenzelm@32994
   548
  | step ctxt mode _ (_, Metis.Proof.Refl f_tm) = refl_inf ctxt mode f_tm
wenzelm@32994
   549
  | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
wenzelm@32994
   550
      equality_inf ctxt mode f_lit f_p f_r;
wenzelm@23442
   551
blanchet@35865
   552
fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
wenzelm@23442
   553
wenzelm@32994
   554
fun translate _ _ thpairs [] = thpairs
wenzelm@32956
   555
  | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
wenzelm@32956
   556
      let val _ = trace_msg (fn () => "=============================================")
wenzelm@32956
   557
          val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
wenzelm@32956
   558
          val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
wenzelm@32956
   559
          val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
wenzelm@32956
   560
          val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
wenzelm@32956
   561
          val _ = trace_msg (fn () => "=============================================")
wenzelm@32994
   562
          val n_metis_lits =
wenzelm@32994
   563
            length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
wenzelm@32956
   564
      in
wenzelm@32956
   565
          if nprems_of th = n_metis_lits then ()
wenzelm@32956
   566
          else error "Metis: proof reconstruction has gone wrong";
wenzelm@32956
   567
          translate mode ctxt ((fol_th, th) :: thpairs) infpairs
wenzelm@32956
   568
      end;
wenzelm@23442
   569
wenzelm@32956
   570
(*Determining which axiom clauses are actually used*)
wenzelm@32956
   571
fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
wenzelm@32994
   572
  | used_axioms _ _ = NONE;
paulson@24855
   573
wenzelm@32956
   574
(* ------------------------------------------------------------------------- *)
wenzelm@32956
   575
(* Translation of HO Clauses                                                 *)
wenzelm@32956
   576
(* ------------------------------------------------------------------------- *)
wenzelm@23442
   577
blanchet@35865
   578
fun cnf_th thy th = hd (cnf_axiom thy th);
wenzelm@23442
   579
wenzelm@32956
   580
fun type_ext thy tms =
blanchet@35865
   581
  let val subs = tfree_classes_of_terms tms
blanchet@35865
   582
      val supers = tvar_classes_of_terms tms
blanchet@35865
   583
      and tycons = type_consts_of_terms thy tms
blanchet@35865
   584
      val (supers', arity_clauses) = make_arity_clauses thy tycons supers
blanchet@35865
   585
      val classrel_clauses = make_classrel_clauses thy subs supers'
wenzelm@32956
   586
  in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
wenzelm@32956
   587
  end;
wenzelm@23442
   588
wenzelm@32956
   589
(* ------------------------------------------------------------------------- *)
wenzelm@32956
   590
(* Logic maps manage the interface between HOL and first-order logic.        *)
wenzelm@32956
   591
(* ------------------------------------------------------------------------- *)
wenzelm@23442
   592
wenzelm@32956
   593
type logic_map =
blanchet@35865
   594
  {axioms: (Metis.Thm.thm * thm) list,
blanchet@35865
   595
   tfrees: type_literal list};
wenzelm@23442
   596
wenzelm@32994
   597
fun const_in_metis c (pred, tm_list) =
wenzelm@32956
   598
  let
wenzelm@32994
   599
    fun in_mterm (Metis.Term.Var _) = false
wenzelm@32956
   600
      | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list
wenzelm@32956
   601
      | in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list
wenzelm@32994
   602
  in  c = pred orelse exists in_mterm tm_list  end;
wenzelm@23442
   603
wenzelm@32956
   604
(*Extract TFree constraints from context to include as conjecture clauses*)
wenzelm@32956
   605
fun init_tfrees ctxt =
blanchet@36966
   606
  let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
blanchet@36966
   607
    Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
blanchet@36966
   608
    |> type_literals_for_types
blanchet@36556
   609
  end;
paulson@24937
   610
wenzelm@32956
   611
(*transform isabelle type / arity clause to metis clause *)
wenzelm@32956
   612
fun add_type_thm [] lmap = lmap
wenzelm@32956
   613
  | add_type_thm ((ith, mth) :: cls) {axioms, tfrees} =
wenzelm@32956
   614
      add_type_thm cls {axioms = (mth, ith) :: axioms,
wenzelm@32956
   615
                        tfrees = tfrees}
wenzelm@23442
   616
wenzelm@32956
   617
(*Insert non-logical axioms corresponding to all accumulated TFrees*)
wenzelm@32956
   618
fun add_tfrees {axioms, tfrees} : logic_map =
wenzelm@32956
   619
     {axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms,
wenzelm@32956
   620
      tfrees = tfrees};
wenzelm@25713
   621
wenzelm@32956
   622
fun string_of_mode FO = "FO"
wenzelm@32956
   623
  | string_of_mode HO = "HO"
wenzelm@32956
   624
  | string_of_mode FT = "FT"
paulson@32532
   625
wenzelm@32956
   626
(* Function to generate metis clauses, including comb and type clauses *)
wenzelm@32956
   627
fun build_map mode0 ctxt cls ths =
wenzelm@32956
   628
  let val thy = ProofContext.theory_of ctxt
wenzelm@32956
   629
      (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
wenzelm@32956
   630
      fun set_mode FO = FO
wenzelm@32956
   631
        | set_mode HO = if forall (Meson.is_fol_term thy o prop_of) (cls@ths) then FO else HO
wenzelm@32956
   632
        | set_mode FT = FT
wenzelm@32956
   633
      val mode = set_mode mode0
wenzelm@32956
   634
      (*transform isabelle clause to metis clause *)
wenzelm@33339
   635
      fun add_thm is_conjecture ith {axioms, tfrees} : logic_map =
wenzelm@32956
   636
        let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
wenzelm@32956
   637
        in
wenzelm@32956
   638
           {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
haftmann@33042
   639
            tfrees = union (op =) tfree_lits tfrees}
wenzelm@32956
   640
        end;
wenzelm@33339
   641
      val lmap0 = fold (add_thm true) cls {axioms = [], tfrees = init_tfrees ctxt}
wenzelm@33339
   642
      val lmap = fold (add_thm false) ths (add_tfrees lmap0)
wenzelm@32956
   643
      val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
wenzelm@32994
   644
      fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
wenzelm@32956
   645
      (*Now check for the existence of certain combinators*)
blanchet@35865
   646
      val thI  = if used "c_COMBI" then [cnf_th @{theory} @{thm COMBI_def}] else []
blanchet@35865
   647
      val thK  = if used "c_COMBK" then [cnf_th @{theory} @{thm COMBK_def}] else []
blanchet@35865
   648
      val thB   = if used "c_COMBB" then [cnf_th @{theory} @{thm COMBB_def}] else []
blanchet@35865
   649
      val thC   = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else []
blanchet@35865
   650
      val thS   = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else []
blanchet@35865
   651
      val thEQ  = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else []
wenzelm@32956
   652
      val lmap' = if mode=FO then lmap
wenzelm@33339
   653
                  else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap
wenzelm@32956
   654
  in
wenzelm@32956
   655
      (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap')
wenzelm@32956
   656
  end;
wenzelm@23442
   657
wenzelm@32956
   658
fun refute cls =
wenzelm@32956
   659
    Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
wenzelm@23442
   660
wenzelm@32956
   661
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const);
wenzelm@23442
   662
wenzelm@32956
   663
fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2);
paulson@24855
   664
wenzelm@32956
   665
exception METIS of string;
paulson@28233
   666
wenzelm@32956
   667
(* Main function to start metis prove and reconstruction *)
wenzelm@32956
   668
fun FOL_SOLVE mode ctxt cls ths0 =
wenzelm@32956
   669
  let val thy = ProofContext.theory_of ctxt
blanchet@35826
   670
      val th_cls_pairs =
blanchet@35865
   671
        map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0
wenzelm@32956
   672
      val ths = maps #2 th_cls_pairs
wenzelm@32956
   673
      val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
wenzelm@32956
   674
      val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
wenzelm@32956
   675
      val _ = trace_msg (fn () => "THEOREM CLAUSES")
wenzelm@32956
   676
      val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
wenzelm@32956
   677
      val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
wenzelm@32956
   678
      val _ = if null tfrees then ()
wenzelm@32956
   679
              else (trace_msg (fn () => "TFREE CLAUSES");
blanchet@36556
   680
                    app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees)
wenzelm@32956
   681
      val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
wenzelm@32956
   682
      val thms = map #1 axioms
wenzelm@32956
   683
      val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
wenzelm@32956
   684
      val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
wenzelm@32956
   685
      val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
wenzelm@32956
   686
  in
wenzelm@33317
   687
      case filter (is_false o prop_of) cls of
wenzelm@32956
   688
          false_th::_ => [false_th RS @{thm FalseE}]
wenzelm@32956
   689
        | [] =>
wenzelm@32956
   690
      case refute thms of
wenzelm@32956
   691
          Metis.Resolution.Contradiction mth =>
wenzelm@32956
   692
            let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
wenzelm@32956
   693
                          Metis.Thm.toString mth)
wenzelm@32956
   694
                val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
wenzelm@32956
   695
                             (*add constraints arising from converting goal to clause form*)
wenzelm@32956
   696
                val proof = Metis.Proof.proof mth
wenzelm@32956
   697
                val result = translate mode ctxt' axioms proof
wenzelm@32956
   698
                and used = map_filter (used_axioms axioms) proof
wenzelm@32956
   699
                val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
wenzelm@32956
   700
                val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
wenzelm@33305
   701
                val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
wenzelm@33305
   702
                  if common_thm used cls then NONE else SOME name)
wenzelm@32956
   703
            in
blanchet@36383
   704
                if not (null cls) andalso not (common_thm used cls) then
blanchet@36383
   705
                  warning "Metis: The assumptions are inconsistent."
blanchet@36383
   706
                else
blanchet@36383
   707
                  ();
blanchet@36383
   708
                if not (null unused) then
blanchet@36230
   709
                  warning ("Metis: Unused theorems: " ^ commas_quote unused
blanchet@36230
   710
                           ^ ".")
blanchet@36230
   711
                else
blanchet@36230
   712
                  ();
wenzelm@32956
   713
                case result of
wenzelm@32956
   714
                    (_,ith)::_ =>
blanchet@36230
   715
                        (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
wenzelm@32956
   716
                         [ith])
blanchet@36230
   717
                  | _ => (trace_msg (fn () => "Metis: No result");
wenzelm@32956
   718
                          [])
wenzelm@32956
   719
            end
wenzelm@32956
   720
        | Metis.Resolution.Satisfiable _ =>
wenzelm@32956
   721
            (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
wenzelm@32956
   722
             [])
wenzelm@32956
   723
  end;
wenzelm@23442
   724
wenzelm@32956
   725
fun metis_general_tac mode ctxt ths i st0 =
wenzelm@32956
   726
  let val _ = trace_msg (fn () =>
wenzelm@32956
   727
        "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
wenzelm@32956
   728
  in
blanchet@35865
   729
    if exists_type type_has_topsort (prop_of st0)
wenzelm@35568
   730
    then raise METIS "Metis: Proof state contains the universal sort {}"
wenzelm@35568
   731
    else
blanchet@36401
   732
      (Meson.MESON (maps neg_clausify)
wenzelm@35568
   733
        (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
blanchet@35865
   734
          THEN Meson_Tactic.expand_defs_tac st0) st0
wenzelm@32956
   735
  end
wenzelm@32956
   736
  handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
wenzelm@23442
   737
wenzelm@32956
   738
val metis_tac = metis_general_tac HO;
wenzelm@32956
   739
val metisF_tac = metis_general_tac FO;
wenzelm@32956
   740
val metisFT_tac = metis_general_tac FT;
wenzelm@23442
   741
wenzelm@32956
   742
fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
wenzelm@32956
   743
  SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment;
wenzelm@23442
   744
wenzelm@32956
   745
val setup =
wenzelm@32956
   746
  type_lits_setup #>
blanchet@35865
   747
  method @{binding metis} HO "METIS for FOL and HOL problems" #>
wenzelm@32956
   748
  method @{binding metisF} FO "METIS for FOL problems" #>
wenzelm@35568
   749
  method @{binding metisFT} FT "METIS with fully-typed translation" #>
wenzelm@32956
   750
  Method.setup @{binding finish_clausify}
blanchet@35865
   751
    (Scan.succeed (K (SIMPLE_METHOD (Meson_Tactic.expand_defs_tac refl))))
wenzelm@32956
   752
    "cleanup after conversion to clauses";
wenzelm@23442
   753
wenzelm@23442
   754
end;