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