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