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