src/HOL/Tools/Sledgehammer/metis_tactics.ML
author blanchet
Thu, 26 Aug 2010 00:49:38 +0200
changeset 38748 69fea359d3f8
parent 38695 e85ce10cef1a
child 38864 4abe644fcea5
permissions -rw-r--r--
renaming
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
     1
(*  Title:      HOL/Tools/Sledgehammer/metis_tactics.ML
38027
505657ddb047 standardize "Author" tags
blanchet
parents: 38016
diff changeset
     2
    Author:     Kong W. Susanto, Cambridge University Computer Laboratory
505657ddb047 standardize "Author" tags
blanchet
parents: 38016
diff changeset
     3
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
505657ddb047 standardize "Author" tags
blanchet
parents: 38016
diff changeset
     4
    Author:     Jasmin Blanchette, TU Muenchen
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     5
    Copyright   Cambridge University 2007
23447
1f16190e3836 tuned comments;
wenzelm
parents: 23442
diff changeset
     6
29266
4a478f9d2847 use regular Term.add_vars, Term.add_frees etc.;
wenzelm
parents: 28700
diff changeset
     7
HOL setup for the Metis prover.
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     8
*)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     9
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
    10
signature METIS_TACTICS =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    11
sig
32955
4a78daeb012b local channels for tracing/debugging;
wenzelm
parents: 32952
diff changeset
    12
  val trace: bool Unsynchronized.ref
24309
01f3e1a43c24 turned type_lits into configuration option (with attribute);
wenzelm
parents: 24300
diff changeset
    13
  val type_lits: bool Config.T
24319
944705cc79d2 export more tactics;
wenzelm
parents: 24309
diff changeset
    14
  val metis_tac: Proof.context -> thm list -> int -> tactic
944705cc79d2 export more tactics;
wenzelm
parents: 24309
diff changeset
    15
  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
    16
  val metisFT_tac: Proof.context -> thm list -> int -> tactic
24319
944705cc79d2 export more tactics;
wenzelm
parents: 24309
diff changeset
    17
  val setup: theory -> theory
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    18
end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    19
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
    20
structure Metis_Tactics : METIS_TACTICS =
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    21
struct
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    22
37578
9367cb36b1c4 renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents: 37577
diff changeset
    23
open Metis_Clauses
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
    24
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    25
val trace = Unsynchronized.ref false;
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
    26
fun trace_msg msg = if !trace then tracing (msg ()) else ();
32955
4a78daeb012b local channels for tracing/debugging;
wenzelm
parents: 32952
diff changeset
    27
36001
992839c4be90 static defaults for configuration options;
wenzelm
parents: 35865
diff changeset
    28
val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    29
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
    30
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
    31
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    32
(* ------------------------------------------------------------------------- *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    33
(* Useful Theorems                                                           *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    34
(* ------------------------------------------------------------------------- *)
33689
d0a9ce721e0c properly inlined @{lemma} antiqutations -- might also reduce proof terms a bit;
wenzelm
parents: 33339
diff changeset
    35
val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)}
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36909
diff changeset
    36
val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp}
33689
d0a9ce721e0c properly inlined @{lemma} antiqutations -- might also reduce proof terms a bit;
wenzelm
parents: 33339
diff changeset
    37
val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp}
d0a9ce721e0c properly inlined @{lemma} antiqutations -- might also reduce proof terms a bit;
wenzelm
parents: 33339
diff changeset
    38
val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp}
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
(* ------------------------------------------------------------------------- *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    41
(* Useful Functions                                                          *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    42
(* ------------------------------------------------------------------------- *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    43
37417
0714ece49081 A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents: 37410
diff changeset
    44
(* Match untyped terms. *)
0714ece49081 A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents: 37410
diff changeset
    45
fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
0714ece49081 A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents: 37410
diff changeset
    46
  | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
0714ece49081 A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents: 37410
diff changeset
    47
  | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
0714ece49081 A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents: 37410
diff changeset
    48
    (a = b) (* The index is ignored, for some reason. *)
0714ece49081 A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents: 37410
diff changeset
    49
  | untyped_aconv (Bound i) (Bound j) = (i = j)
0714ece49081 A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents: 37410
diff changeset
    50
  | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
0714ece49081 A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents: 37410
diff changeset
    51
  | untyped_aconv (t1 $ t2) (u1 $ u2) =
0714ece49081 A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents: 37410
diff changeset
    52
    untyped_aconv t1 u1 andalso untyped_aconv t2 u2
0714ece49081 A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents: 37410
diff changeset
    53
  | untyped_aconv _ _ = false
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    54
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    55
(* Finding the relative location of an untyped term within a list of terms *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    56
fun get_index lit =
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    57
  let val lit = Envir.eta_contract lit
37498
b426cbdb5a23 removed Sledgehammer's support for the DFG syntax;
blanchet
parents: 37479
diff changeset
    58
      fun get _ [] = raise Empty
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    59
        | get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x))
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    60
                          then n  else get (n+1) xs
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    61
  in get 1 end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    62
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    63
(* ------------------------------------------------------------------------- *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    64
(* HOL to FOL  (Isabelle to Metis)                                           *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    65
(* ------------------------------------------------------------------------- *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    66
38614
61672fa2983a temporarily disable "fequal" handling in Metis;
blanchet
parents: 38612
diff changeset
    67
fun fn_isa_to_met_sublevel "equal" = "=" (* FIXME: "c_fequal" *)
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
    68
  | fn_isa_to_met_sublevel x = x
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
    69
fun fn_isa_to_met_toplevel "equal" = "="
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
    70
  | fn_isa_to_met_toplevel x = x
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    71
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    72
fun metis_lit b c args = (b, (c, args));
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    73
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
    74
fun metis_term_from_combtyp (CombTVar (s, _)) = Metis.Term.Var s
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
    75
  | metis_term_from_combtyp (CombTFree (s, _)) = Metis.Term.Fn (s, [])
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
    76
  | metis_term_from_combtyp (CombType ((s, _), tps)) =
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
    77
    Metis.Term.Fn (s, map metis_term_from_combtyp tps);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    78
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    79
(*These two functions insert type literals before the real literals. That is the
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    80
  opposite order from TPTP linkup, but maybe OK.*)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    81
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    82
fun hol_term_to_fol_FO tm =
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
    83
  case strip_combterm_comb tm of
36170
0cdb76723c88 added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents: 36169
diff changeset
    84
      (CombConst ((c, _), _, tys), tms) =>
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
    85
        let val tyargs = map metis_term_from_combtyp tys
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    86
            val args   = map hol_term_to_fol_FO tms
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    87
        in Metis.Term.Fn (c, tyargs @ args) end
36170
0cdb76723c88 added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents: 36169
diff changeset
    88
    | (CombVar ((v, _), _), []) => Metis.Term.Var v
38695
e85ce10cef1a revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents: 38652
diff changeset
    89
    | _ => raise Fail "non-first-order combterm"
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    90
38099
e3bb96b83807 fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents: 38097
diff changeset
    91
fun hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
    92
      Metis.Term.Fn (fn_isa_to_met_sublevel a, map metis_term_from_combtyp tylist)
38099
e3bb96b83807 fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
blanchet
parents: 38097
diff changeset
    93
  | hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
    94
  | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
    95
       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
    96
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    97
(*The fully-typed translation, to avoid type errors*)
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
    98
fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, metis_term_from_combtyp ty]);
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
    99
36170
0cdb76723c88 added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents: 36169
diff changeset
   100
fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty)
0cdb76723c88 added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents: 36169
diff changeset
   101
  | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   102
      wrap_type (Metis.Term.Fn(fn_isa_to_met_sublevel a, []), ty)
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   103
  | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   104
       wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
37994
b04307085a09 make TPTP generator accept full first-order formulas
blanchet
parents: 37992
diff changeset
   105
                  combtyp_of tm)
32532
a0a54a51b15b My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents: 32530
diff changeset
   106
37923
8edbaf6ba405 renamed "Literal" to "FOLLiteral"
blanchet
parents: 37643
diff changeset
   107
fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
36170
0cdb76723c88 added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents: 36169
diff changeset
   108
      let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   109
          val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   110
          val lits = map hol_term_to_fol_FO tms
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   111
      in metis_lit pos (fn_isa_to_met_toplevel p) (tylits @ lits) end
37923
8edbaf6ba405 renamed "Literal" to "FOLLiteral"
blanchet
parents: 37643
diff changeset
   112
  | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   113
     (case strip_combterm_comb tm of
36170
0cdb76723c88 added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents: 36169
diff changeset
   114
          (CombConst(("equal", _), _, _), tms) =>
37923
8edbaf6ba405 renamed "Literal" to "FOLLiteral"
blanchet
parents: 37643
diff changeset
   115
            metis_lit pos "=" (map hol_term_to_fol_HO tms)
8edbaf6ba405 renamed "Literal" to "FOLLiteral"
blanchet
parents: 37643
diff changeset
   116
        | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
8edbaf6ba405 renamed "Literal" to "FOLLiteral"
blanchet
parents: 37643
diff changeset
   117
  | hol_literal_to_fol FT (FOLLiteral (pos, tm)) =
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   118
     (case strip_combterm_comb tm of
36170
0cdb76723c88 added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents: 36169
diff changeset
   119
          (CombConst(("equal", _), _, _), tms) =>
37923
8edbaf6ba405 renamed "Literal" to "FOLLiteral"
blanchet
parents: 37643
diff changeset
   120
            metis_lit pos "=" (map hol_term_to_fol_FT tms)
8edbaf6ba405 renamed "Literal" to "FOLLiteral"
blanchet
parents: 37643
diff changeset
   121
        | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   122
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   123
fun literals_of_hol_term thy mode t =
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   124
      let val (lits, types_sorts) = literals_of_term thy t
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   125
      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
   126
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   127
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37632
diff changeset
   128
fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
36556
81dc2c20f052 use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents: 36401
diff changeset
   129
    metis_lit pos s [Metis.Term.Var s']
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37632
diff changeset
   130
  | metis_of_type_literals pos (TyLitFree ((s, _), (s', _))) =
36556
81dc2c20f052 use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents: 36401
diff changeset
   131
    metis_lit pos s [Metis.Term.Fn (s',[])]
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   132
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
   133
fun default_sort _ (TVar _) = false
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 32994
diff changeset
   134
  | 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
   135
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   136
fun metis_of_tfree tf =
36556
81dc2c20f052 use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents: 36401
diff changeset
   137
  Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf));
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   138
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   139
fun hol_thm_to_fol is_conjecture ctxt mode j skolems th =
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   140
  let
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   141
    val thy = ProofContext.theory_of ctxt
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   142
    val (skolems, (mlits, types_sorts)) =
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   143
     th |> prop_of |> conceal_skolem_terms j skolems
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   144
        ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   145
  in
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   146
      if is_conjecture then
36556
81dc2c20f052 use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents: 36401
diff changeset
   147
          (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   148
           type_literals_for_types types_sorts, skolems)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   149
      else
36966
adc11fb3f3aa generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents: 36945
diff changeset
   150
        let val tylits = filter_out (default_sort ctxt) types_sorts
adc11fb3f3aa generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents: 36945
diff changeset
   151
                         |> type_literals_for_types
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   152
            val mtylits = if Config.get ctxt type_lits
36556
81dc2c20f052 use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents: 36401
diff changeset
   153
                          then map (metis_of_type_literals false) tylits else []
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   154
        in
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   155
          (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [],
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   156
           skolems)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   157
        end
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   158
  end;
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
(* ARITY CLAUSE *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   161
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37632
diff changeset
   162
fun m_arity_cls (TConsLit ((c, _), (t, _), args)) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37632
diff changeset
   163
    metis_lit true c [Metis.Term.Fn(t, map (Metis.Term.Var o fst) args)]
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37632
diff changeset
   164
  | m_arity_cls (TVarLit ((c, _), (s, _))) =
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37632
diff changeset
   165
    metis_lit false c [Metis.Term.Var s]
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   166
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   167
(*TrueI is returned as the Isabelle counterpart because there isn't any.*)
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   168
fun arity_cls (ArityClause {conclLit, premLits, ...}) =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   169
  (TrueI,
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   170
   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
   171
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   172
(* CLASSREL CLAUSE *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   173
37925
1188e6bff48d rename "classrel" to "class_rel"
blanchet
parents: 37924
diff changeset
   174
fun m_class_rel_cls (subclass, _) (superclass, _) =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   175
  [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
   176
37925
1188e6bff48d rename "classrel" to "class_rel"
blanchet
parents: 37924
diff changeset
   177
fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) =
1188e6bff48d rename "classrel" to "class_rel"
blanchet
parents: 37924
diff changeset
   178
  (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_class_rel_cls subclass superclass)));
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   179
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   180
(* ------------------------------------------------------------------------- *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   181
(* FOL to HOL  (Metis to Isabelle)                                           *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   182
(* ------------------------------------------------------------------------- *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   183
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   184
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
   185
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   186
fun terms_of [] = []
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   187
  | terms_of (Term t :: tts) = t :: terms_of tts
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   188
  | terms_of (Type _ :: tts) = terms_of tts;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   189
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   190
fun types_of [] = []
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
   191
  | types_of (Term (Term.Var ((a,idx), _)) :: tts) =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   192
      if String.isPrefix "_" a then
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   193
          (*Variable generated by Metis, which might have been a type variable.*)
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
   194
          TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   195
      else types_of tts
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   196
  | types_of (Term _ :: tts) = types_of tts
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   197
  | types_of (Type T :: tts) = T :: types_of tts;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   198
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   199
fun apply_list rator nargs rands =
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   200
  let val trands = terms_of rands
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   201
  in  if length trands = nargs then Term (list_comb(rator, trands))
37402
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   202
      else raise Fail
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   203
        ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   204
          " expected " ^ Int.toString nargs ^
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   205
          " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   206
  end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   207
24500
5e135602f660 type_infer: mode_pattern;
wenzelm
parents: 24494
diff changeset
   208
fun infer_types ctxt =
5e135602f660 type_infer: mode_pattern;
wenzelm
parents: 24494
diff changeset
   209
  Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   210
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   211
(*We use 1 rather than 0 because variable references in clauses may otherwise conflict
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   212
  with variable constraints in the goal...at least, type inference often fails otherwise.
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   213
  SEE ALSO axiom_inf below.*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   214
fun mk_var (w,T) = Term.Var((w,1), T);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   215
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   216
(*include the default sort, if available*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   217
fun mk_tfree ctxt w =
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   218
  let val ww = "'" ^ w
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 32994
diff changeset
   219
  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
   220
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   221
(*Remove the "apply" operator from an HO term*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   222
fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   223
  | strip_happ args x = (x, args);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   224
36967
3c804030474b fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents: 36966
diff changeset
   225
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
3c804030474b fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents: 36966
diff changeset
   226
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   227
fun smart_invert_const "fequal" = @{const_name "op ="}
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   228
  | smart_invert_const s = invert_const s
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   229
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   230
fun hol_type_from_metis_term _ (Metis.Term.Var v) =
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   231
     (case strip_prefix_and_unascii tvar_prefix v of
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   232
          SOME w => make_tvar w
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   233
        | NONE   => make_tvar v)
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   234
  | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   235
     (case strip_prefix_and_unascii type_const_prefix x of
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   236
          SOME tc => Term.Type (smart_invert_const tc,
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   237
                                map (hol_type_from_metis_term ctxt) tys)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   238
        | NONE    =>
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   239
      case strip_prefix_and_unascii tfree_prefix x of
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   240
          SOME tf => mk_tfree ctxt tf
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   241
        | NONE    => raise Fail ("hol_type_from_metis_term: " ^ x));
32532
a0a54a51b15b My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents: 32530
diff changeset
   242
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   243
(*Maps metis terms to isabelle terms*)
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   244
fun hol_term_from_metis_PT ctxt fol_tm =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   245
  let val thy = ProofContext.theory_of ctxt
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   246
      val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   247
                                  Metis.Term.toString fol_tm)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   248
      fun tm_to_tt (Metis.Term.Var v) =
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   249
             (case strip_prefix_and_unascii tvar_prefix v of
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   250
                  SOME w => Type (make_tvar w)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   251
                | NONE =>
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   252
              case strip_prefix_and_unascii schematic_var_prefix v of
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   253
                  SOME w => Term (mk_var (w, HOLogic.typeT))
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   254
                | NONE   => Term (mk_var (v, HOLogic.typeT)) )
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   255
                    (*Var from Metis with a name like _nnn; possibly a type variable*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   256
        | tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg   (*hBOOL*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   257
        | tm_to_tt (t as Metis.Term.Fn (".",_)) =
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   258
            let val (rator,rands) = strip_happ [] t
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   259
            in  case rator of
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   260
                    Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   261
                  | _ => case tm_to_tt rator of
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   262
                             Term t => Term (list_comb(t, terms_of (map tm_to_tt rands)))
37402
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   263
                           | _ => raise Fail "tm_to_tt: HO application"
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   264
            end
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   265
        | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   266
      and applic_to_tt ("=",ts) =
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   267
            Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   268
        | applic_to_tt (a,ts) =
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   269
            case strip_prefix_and_unascii const_prefix a of
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   270
                SOME b =>
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   271
                  let val c = smart_invert_const b
36909
7d5587f6d5f7 made Sledgehammer's full-typed proof reconstruction work for the first time;
blanchet
parents: 36556
diff changeset
   272
                      val ntypes = num_type_args thy c
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   273
                      val nterms = length ts - ntypes
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   274
                      val tts = map tm_to_tt ts
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   275
                      val tys = types_of (List.take(tts,ntypes))
36909
7d5587f6d5f7 made Sledgehammer's full-typed proof reconstruction work for the first time;
blanchet
parents: 36556
diff changeset
   276
                  in if length tys = ntypes then
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   277
                         apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
37402
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   278
                     else
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   279
                       raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   280
                                   " but gets " ^ Int.toString (length tys) ^
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   281
                                   " type arguments\n" ^
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   282
                                   cat_lines (map (Syntax.string_of_typ ctxt) tys) ^
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   283
                                   " the terms are \n" ^
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   284
                                   cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   285
                     end
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   286
              | NONE => (*Not a constant. Is it a type constructor?*)
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   287
            case strip_prefix_and_unascii type_const_prefix a of
33227
83322d668601 avoid structure alias;
wenzelm
parents: 33042
diff changeset
   288
                SOME b =>
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   289
                  Type (Term.Type (smart_invert_const b, types_of (map tm_to_tt ts)))
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   290
              | NONE => (*Maybe a TFree. Should then check that ts=[].*)
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   291
            case strip_prefix_and_unascii tfree_prefix a of
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   292
                SOME b => Type (mk_tfree ctxt b)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   293
              | NONE => (*a fixed variable? They are Skolem functions.*)
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   294
            case strip_prefix_and_unascii fixed_var_prefix a of
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   295
                SOME b =>
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   296
                  let val opr = Term.Free(b, HOLogic.typeT)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   297
                  in  apply_list opr (length ts) (map tm_to_tt ts)  end
37402
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   298
              | NONE => raise Fail ("unexpected metis function: " ^ a)
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   299
  in
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   300
    case tm_to_tt fol_tm of
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   301
      Term t => t
37402
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   302
    | _ => raise Fail "fol_tm_to_tt: Term expected"
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   303
  end
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   304
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   305
(*Maps fully-typed metis terms to isabelle terms*)
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   306
fun hol_term_from_metis_FT ctxt fol_tm =
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   307
  let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   308
                                  Metis.Term.toString fol_tm)
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
   309
      fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   310
             (case strip_prefix_and_unascii schematic_var_prefix v of
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   311
                  SOME w =>  mk_var(w, dummyT)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   312
                | NONE   => mk_var(v, dummyT))
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
   313
        | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
38549
d0385f2764d8 use antiquotations for remaining unqualified constants in HOL
haftmann
parents: 38433
diff changeset
   314
            Const (@{const_name "op ="}, HOLogic.typeT)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   315
        | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   316
           (case strip_prefix_and_unascii const_prefix x of
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   317
                SOME c => Const (smart_invert_const c, dummyT)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   318
              | NONE => (*Not a constant. Is it a fixed variable??*)
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   319
            case strip_prefix_and_unascii fixed_var_prefix x of
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   320
                SOME v => Free (v, hol_type_from_metis_term ctxt ty)
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   321
              | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   322
        | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   323
            cvt tm1 $ cvt tm2
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   324
        | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   325
            cvt tm1 $ cvt tm2
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   326
        | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg   (*hBOOL*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   327
        | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   328
            list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   329
        | cvt (t as Metis.Term.Fn (x, [])) =
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   330
           (case strip_prefix_and_unascii const_prefix x of
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   331
                SOME c => Const (smart_invert_const c, dummyT)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   332
              | NONE => (*Not a constant. Is it a fixed variable??*)
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   333
            case strip_prefix_and_unascii fixed_var_prefix x of
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   334
                SOME v => Free (v, dummyT)
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   335
              | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   336
                  hol_term_from_metis_PT ctxt t))
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   337
        | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis.Term.toString t);
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   338
            hol_term_from_metis_PT ctxt t)
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   339
  in fol_tm |> cvt end
32532
a0a54a51b15b My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents: 32530
diff changeset
   340
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   341
fun hol_term_from_metis FT = hol_term_from_metis_FT
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   342
  | hol_term_from_metis _ = hol_term_from_metis_PT
32532
a0a54a51b15b My umpteenth attempt to commit the method metisFT, a fully-typed version of metis
paulson
parents: 32530
diff changeset
   343
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   344
fun hol_terms_from_fol ctxt mode skolems fol_tms =
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   345
  let val ts = map (hol_term_from_metis mode ctxt) fol_tms
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   346
      val _ = trace_msg (fn () => "  calling type inference:")
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   347
      val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   348
      val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   349
      val _ = app (fn t => trace_msg
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   350
                    (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   351
                              "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   352
                  ts'
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   353
  in  ts'  end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   354
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   355
fun mk_not (Const (@{const_name Not}, _) $ b) = b
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   356
  | mk_not b = HOLogic.mk_not b;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   357
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   358
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
   359
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   360
(* ------------------------------------------------------------------------- *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   361
(* FOL step Inference Rules                                                  *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   362
(* ------------------------------------------------------------------------- *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   363
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   364
(*for debugging only*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   365
fun print_thpair (fth,th) =
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   366
  (trace_msg (fn () => "=============================================");
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   367
   trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth);
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   368
   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
   369
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   370
fun lookth thpairs (fth : Metis.Thm.thm) =
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 32994
diff changeset
   371
  the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
37402
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   372
  handle Option =>
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   373
         raise Fail ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   374
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   375
fun is_TrueI th = Thm.eq_thm(TrueI,th);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   376
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   377
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
   378
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   379
fun inst_excluded_middle thy i_atm =
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   380
  let val th = EXCLUDED_MIDDLE
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   381
      val [vx] = Term.add_vars (prop_of th) []
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   382
      val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   383
  in  cterm_instantiate substs th  end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   384
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   385
(* INFERENCE RULE: AXIOM *)
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36909
diff changeset
   386
fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th);
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   387
    (*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
   388
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   389
(* INFERENCE RULE: ASSUME *)
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   390
fun assume_inf ctxt mode skolems atm =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   391
  inst_excluded_middle
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   392
      (ProofContext.theory_of ctxt)
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   393
      (singleton (hol_terms_from_fol ctxt mode skolems) (Metis.Term.Fn atm))
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   394
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   395
(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   396
   them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   397
   that new TVars are distinct and that types can be inferred from terms.*)
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   398
fun inst_inf ctxt mode skolems thpairs fsubst th =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   399
  let val thy = ProofContext.theory_of ctxt
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   400
      val i_th   = lookth thpairs th
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   401
      val i_th_vars = Term.add_vars (prop_of i_th) []
33035
15eab423e573 standardized basic operations on type option;
wenzelm
parents: 32994
diff changeset
   402
      fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   403
      fun subst_translation (x,y) =
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   404
            let val v = find_var x
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   405
                (* We call "reveal_skolem_terms" and "infer_types" below. *)
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   406
                val t = hol_term_from_metis mode ctxt y
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   407
            in  SOME (cterm_of thy (Var v), t)  end
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   408
            handle Option =>
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   409
                (trace_msg (fn() => "List.find failed for the variable " ^ x ^
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   410
                                       " in " ^ Display.string_of_thm ctxt i_th);
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   411
                 NONE)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   412
      fun remove_typeinst (a, t) =
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   413
            case strip_prefix_and_unascii schematic_var_prefix a of
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   414
                SOME b => SOME (b, t)
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   415
              | NONE => case strip_prefix_and_unascii tvar_prefix a of
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   416
                SOME _ => NONE          (*type instantiations are forbidden!*)
38748
69fea359d3f8 renaming
blanchet
parents: 38695
diff changeset
   417
              | NONE => SOME (a,t)    (*internal Metis var?*)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   418
      val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   419
      val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   420
      val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   421
      val tms = rawtms |> map (reveal_skolem_terms skolems) |> infer_types ctxt
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   422
      val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   423
      val substs' = ListPair.zip (vars, map ctm_of tms)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   424
      val _ = trace_msg (fn () =>
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   425
        cat_lines ("subst_translations:" ::
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   426
          (substs' |> map (fn (x, y) =>
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   427
            Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   428
            Syntax.string_of_term ctxt (term_of y)))));
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   429
  in cterm_instantiate substs' i_th end
38695
e85ce10cef1a revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents: 38652
diff changeset
   430
  handle THM (msg, _, _) =>
e85ce10cef1a revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents: 38652
diff changeset
   431
         error ("Cannot replay Metis proof in Isabelle:\n" ^ msg)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   432
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   433
(* INFERENCE RULE: RESOLVE *)
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   434
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   435
(*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
   436
  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
   437
  could then fail. See comment on mk_var.*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   438
fun resolve_inc_tyvars(tha,i,thb) =
37548
6a7a9261b9ad make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"
blanchet
parents: 37538
diff changeset
   439
  let
6a7a9261b9ad make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"
blanchet
parents: 37538
diff changeset
   440
      val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   441
      val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   442
  in
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   443
      case distinct Thm.eq_thm ths of
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   444
        [th] => th
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   445
      | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
37548
6a7a9261b9ad make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"
blanchet
parents: 37538
diff changeset
   446
  end
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   447
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   448
fun resolve_inf ctxt mode skolems thpairs atm th1 th2 =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   449
  let
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   450
    val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   451
    val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   452
    val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   453
  in
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   454
    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
   455
    else if is_TrueI i_th2 then i_th1
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   456
    else
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   457
      let
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   458
        val i_atm = singleton (hol_terms_from_fol ctxt mode skolems)
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   459
                              (Metis.Term.Fn atm)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   460
        val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   461
        val prems_th1 = prems_of i_th1
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   462
        val prems_th2 = prems_of i_th2
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   463
        val index_th1 = get_index (mk_not i_atm) prems_th1
37402
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   464
              handle Empty => raise Fail "Failed to find literal in th1"
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   465
        val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   466
        val index_th2 = get_index i_atm prems_th2
37402
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   467
              handle Empty => raise Fail "Failed to find literal in th2"
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   468
        val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   469
    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
   470
  end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   471
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   472
(* INFERENCE RULE: REFL *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   473
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   474
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   475
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   476
fun refl_inf ctxt mode skolems t =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   477
  let val thy = ProofContext.theory_of ctxt
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   478
      val i_t = singleton (hol_terms_from_fol ctxt mode skolems) t
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   479
      val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   480
      val c_t = cterm_incr_types thy refl_idx i_t
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   481
  in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   482
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   483
fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0  (*equality has no type arguments*)
36909
7d5587f6d5f7 made Sledgehammer's full-typed proof reconstruction work for the first time;
blanchet
parents: 36556
diff changeset
   484
  | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0)
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
   485
  | get_ty_arg_size _ _ = 0;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   486
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   487
(* INFERENCE RULE: EQUALITY *)
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   488
fun equality_inf ctxt mode skolems (pos, atm) fp fr =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   489
  let val thy = ProofContext.theory_of ctxt
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   490
      val m_tm = Metis.Term.Fn atm
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   491
      val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolems [m_tm, fr]
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   492
      val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
   493
      fun replace_item_list lx 0 (_::ls) = lx::ls
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   494
        | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   495
      fun path_finder_FO tm [] = (tm, Term.Bound 0)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   496
        | path_finder_FO tm (p::ps) =
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   497
            let val (tm1,args) = strip_comb tm
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   498
                val adjustment = get_ty_arg_size thy tm1
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   499
                val p' = if adjustment > p then p else p-adjustment
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   500
                val tm_p = List.nth(args,p')
38695
e85ce10cef1a revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents: 38652
diff changeset
   501
                  handle Subscript =>
e85ce10cef1a revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents: 38652
diff changeset
   502
                         error ("Cannot replay Metis proof in Isabelle:\n" ^
e85ce10cef1a revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents: 38652
diff changeset
   503
                                "equality_inf: " ^ Int.toString p ^ " adj " ^
e85ce10cef1a revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents: 38652
diff changeset
   504
                                Int.toString adjustment ^ " term " ^
e85ce10cef1a revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents: 38652
diff changeset
   505
                                Syntax.string_of_term ctxt tm)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   506
                val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   507
                                      "  " ^ Syntax.string_of_term ctxt tm_p)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   508
                val (r,t) = path_finder_FO tm_p ps
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   509
            in
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   510
                (r, list_comb (tm1, replace_item_list t p' args))
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   511
            end
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   512
      fun path_finder_HO tm [] = (tm, Term.Bound 0)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   513
        | 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
   514
        | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
37402
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   515
        | path_finder_HO tm ps =
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   516
          raise Fail ("equality_inf, path_finder_HO: path = " ^
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   517
                      space_implode " " (map Int.toString ps) ^
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   518
                      " isa-term: " ^  Syntax.string_of_term ctxt tm)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   519
      fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
   520
        | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   521
            path_finder_FT tm ps t1
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
   522
        | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1, _])) =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   523
            (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
   524
        | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   525
            (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
37402
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   526
        | path_finder_FT tm ps t =
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   527
          raise Fail ("equality_inf, path_finder_FT: path = " ^
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   528
                      space_implode " " (map Int.toString ps) ^
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   529
                      " isa-term: " ^  Syntax.string_of_term ctxt tm ^
12cb33916e37 "raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents: 37399
diff changeset
   530
                      " fol-term: " ^ Metis.Term.toString t)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   531
      fun path_finder FO tm ps _ = path_finder_FO tm ps
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   532
        | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   533
             (*equality: not curried, as other predicates are*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   534
             if p=0 then path_finder_HO tm (0::1::ps)  (*select first operand*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   535
             else path_finder_HO tm (p::ps)        (*1 selects second operand*)
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
   536
        | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   537
             path_finder_HO tm ps      (*if not equality, ignore head to skip hBOOL*)
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   538
        | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   539
                            (Metis.Term.Fn ("=", [t1,t2])) =
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   540
             (*equality: not curried, as other predicates are*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   541
             if p=0 then path_finder_FT tm (0::1::ps)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   542
                          (Metis.Term.Fn (".", [Metis.Term.Fn (".", [metis_eq,t1]), t2]))
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   543
                          (*select first operand*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   544
             else path_finder_FT tm (p::ps)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   545
                   (Metis.Term.Fn (".", [metis_eq,t2]))
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   546
                   (*1 selects second operand*)
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
   547
        | 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
   548
             (*if not equality, ignore head to skip the hBOOL predicate*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   549
        | path_finder FT tm ps t = path_finder_FT tm ps t  (*really an error case!*)
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   550
      fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   551
            let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   552
            in (tm, nt $ tm_rslt) end
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   553
        | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   554
      val (tm_subst, body) = path_finder_lit i_atm fp
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   555
      val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   556
      val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   557
      val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   558
      val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   559
      val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36909
diff changeset
   560
      val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   561
      val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   562
      val eq_terms = map (pairself (cterm_of thy))
33227
83322d668601 avoid structure alias;
wenzelm
parents: 33042
diff changeset
   563
        (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   564
  in  cterm_instantiate eq_terms subst'  end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   565
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   566
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
   567
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   568
fun step ctxt mode skolems thpairs p =
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   569
  case p of
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   570
    (fol_th, Metis.Proof.Axiom _) => factor (axiom_inf thpairs fol_th)
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   571
  | (_, Metis.Proof.Assume f_atm) => assume_inf ctxt mode skolems f_atm
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   572
  | (_, Metis.Proof.Subst (f_subst, f_th1)) =>
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   573
    factor (inst_inf ctxt mode skolems thpairs f_subst f_th1)
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   574
  | (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =>
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   575
    factor (resolve_inf ctxt mode skolems thpairs f_atm f_th1 f_th2)
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   576
  | (_, Metis.Proof.Refl f_tm) => refl_inf ctxt mode skolems f_tm
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   577
  | (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =>
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   578
    equality_inf ctxt mode skolems f_lit f_p f_r
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   579
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   580
fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   581
38280
577f138af235 replace recursion with "fold"
blanchet
parents: 38100
diff changeset
   582
fun translate_one ctxt mode skolems (fol_th, inf) thpairs =
577f138af235 replace recursion with "fold"
blanchet
parents: 38100
diff changeset
   583
  let
577f138af235 replace recursion with "fold"
blanchet
parents: 38100
diff changeset
   584
    val _ = trace_msg (fn () => "=============================================")
577f138af235 replace recursion with "fold"
blanchet
parents: 38100
diff changeset
   585
    val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
577f138af235 replace recursion with "fold"
blanchet
parents: 38100
diff changeset
   586
    val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
577f138af235 replace recursion with "fold"
blanchet
parents: 38100
diff changeset
   587
    val th = Meson.flexflex_first_order (step ctxt mode skolems
577f138af235 replace recursion with "fold"
blanchet
parents: 38100
diff changeset
   588
                                              thpairs (fol_th, inf))
577f138af235 replace recursion with "fold"
blanchet
parents: 38100
diff changeset
   589
    val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
577f138af235 replace recursion with "fold"
blanchet
parents: 38100
diff changeset
   590
    val _ = trace_msg (fn () => "=============================================")
577f138af235 replace recursion with "fold"
blanchet
parents: 38100
diff changeset
   591
    val n_metis_lits =
577f138af235 replace recursion with "fold"
blanchet
parents: 38100
diff changeset
   592
      length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
38695
e85ce10cef1a revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents: 38652
diff changeset
   593
    val _ = if nprems_of th = n_metis_lits then ()
e85ce10cef1a revert this idea of automatically invoking "metisFT" when "metis" fails;
blanchet
parents: 38652
diff changeset
   594
            else error "Cannot replay Metis proof in Isabelle."
38280
577f138af235 replace recursion with "fold"
blanchet
parents: 38100
diff changeset
   595
  in (fol_th, th) :: thpairs end
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   596
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   597
(*Determining which axiom clauses are actually used*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   598
fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th)
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
   599
  | used_axioms _ _ = NONE;
24855
161eb8381b49 metis method: used theorems
paulson
parents: 24827
diff changeset
   600
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   601
(* ------------------------------------------------------------------------- *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   602
(* Translation of HO Clauses                                                 *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   603
(* ------------------------------------------------------------------------- *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   604
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   605
fun type_ext thy tms =
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   606
  let val subs = tfree_classes_of_terms tms
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   607
      val supers = tvar_classes_of_terms tms
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   608
      and tycons = type_consts_of_terms thy tms
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   609
      val (supers', arity_clauses) = make_arity_clauses thy tycons supers
37925
1188e6bff48d rename "classrel" to "class_rel"
blanchet
parents: 37924
diff changeset
   610
      val class_rel_clauses = make_class_rel_clauses thy subs supers'
1188e6bff48d rename "classrel" to "class_rel"
blanchet
parents: 37924
diff changeset
   611
  in  map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   612
  end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   613
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   614
(* ------------------------------------------------------------------------- *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   615
(* Logic maps manage the interface between HOL and first-order logic.        *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   616
(* ------------------------------------------------------------------------- *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   617
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   618
type logic_map =
35865
2f8fb5242799 more Sledgehammer refactoring
blanchet
parents: 35826
diff changeset
   619
  {axioms: (Metis.Thm.thm * thm) list,
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   620
   tfrees: type_literal list,
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   621
   skolems: (string * term) list}
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   622
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
   623
fun const_in_metis c (pred, tm_list) =
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   624
  let
32994
ccc07fbbfefd removed some unreferenced material;
wenzelm
parents: 32956
diff changeset
   625
    fun in_mterm (Metis.Term.Var _) = false
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   626
      | in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   627
      | 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
   628
  in  c = pred orelse exists in_mterm tm_list  end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   629
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   630
(*Extract TFree constraints from context to include as conjecture clauses*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   631
fun init_tfrees ctxt =
36966
adc11fb3f3aa generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents: 36945
diff changeset
   632
  let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts in
adc11fb3f3aa generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents: 36945
diff changeset
   633
    Vartab.fold add (#2 (Variable.constraints_of ctxt)) []
adc11fb3f3aa generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents: 36945
diff changeset
   634
    |> type_literals_for_types
36556
81dc2c20f052 use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents: 36401
diff changeset
   635
  end;
24937
340523598914 context-based treatment of generalization; also handling TFrees in axiom clauses
paulson
parents: 24920
diff changeset
   636
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   637
(*transform isabelle type / arity clause to metis clause *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   638
fun add_type_thm [] lmap = lmap
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   639
  | add_type_thm ((ith, mth) :: cls) {axioms, tfrees, skolems} =
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   640
      add_type_thm cls {axioms = (mth, ith) :: axioms, tfrees = tfrees,
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   641
                        skolems = skolems}
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   642
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   643
(*Insert non-logical axioms corresponding to all accumulated TFrees*)
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   644
fun add_tfrees {axioms, tfrees, skolems} : logic_map =
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   645
     {axioms = map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   646
               axioms,
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   647
      tfrees = tfrees, skolems = skolems}
25713
1c45623e0edf removed duplicate CRITICAL markup;
wenzelm
parents: 25710
diff changeset
   648
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   649
fun string_of_mode FO = "FO"
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   650
  | string_of_mode HO = "HO"
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   651
  | 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
   652
37479
f6b1ee5b420b try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents: 37417
diff changeset
   653
val helpers =
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   654
  [("c_COMBI", (false, map (`I) @{thms COMBI_def})),
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   655
   ("c_COMBK", (false, map (`I) @{thms COMBK_def})),
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   656
   ("c_COMBB", (false, map (`I) @{thms COMBB_def})),
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   657
   ("c_COMBC", (false, map (`I) @{thms COMBC_def})),
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   658
   ("c_COMBS", (false, map (`I) @{thms COMBS_def})),
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   659
   ("c_fequal", (false, map (rpair @{thm equal_imp_equal})
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   660
                            @{thms fequal_imp_equal equal_imp_fequal})),
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   661
   ("c_True", (true, map (`I) @{thms True_or_False})),
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   662
   ("c_False", (true, map (`I) @{thms True_or_False})),
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   663
   ("c_If", (true, map (`I) @{thms if_True if_False True_or_False}))]
37479
f6b1ee5b420b try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents: 37417
diff changeset
   664
38100
e458a0dd3dc1 use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
blanchet
parents: 38099
diff changeset
   665
fun is_quasi_fol_clause thy =
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   666
  Meson.is_fol_term thy o snd o conceal_skolem_terms ~1 [] o prop_of
37623
295f3a9b44b6 move functions not needed by Metis out of "Metis_Clauses"
blanchet
parents: 37619
diff changeset
   667
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   668
(* Function to generate metis clauses, including comb and type clauses *)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   669
fun build_map mode0 ctxt cls ths =
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   670
  let val thy = ProofContext.theory_of ctxt
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   671
      (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   672
      fun set_mode FO = FO
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   673
        | set_mode HO =
37623
295f3a9b44b6 move functions not needed by Metis out of "Metis_Clauses"
blanchet
parents: 37619
diff changeset
   674
          if forall (is_quasi_fol_clause thy) (cls @ ths) then FO else HO
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   675
        | set_mode FT = FT
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   676
      val mode = set_mode mode0
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   677
      (*transform isabelle clause to metis clause *)
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   678
      fun add_thm is_conjecture (metis_ith, isa_ith) {axioms, tfrees, skolems}
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   679
                  : logic_map =
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   680
        let
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   681
          val (mth, tfree_lits, skolems) =
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   682
            hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   683
                           metis_ith
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   684
        in
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   685
           {axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   686
            tfrees = union (op =) tfree_lits tfrees, skolems = skolems}
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   687
        end;
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   688
      val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []}
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   689
                 |> fold (add_thm true o `I) cls
37498
b426cbdb5a23 removed Sledgehammer's support for the DFG syntax;
blanchet
parents: 37479
diff changeset
   690
                 |> add_tfrees
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   691
                 |> fold (add_thm false o `I) ths
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   692
      val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
37479
f6b1ee5b420b try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents: 37417
diff changeset
   693
      fun is_used c =
f6b1ee5b420b try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents: 37417
diff changeset
   694
        exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
37399
34f080a12063 proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents: 37318
diff changeset
   695
      val lmap =
37479
f6b1ee5b420b try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents: 37417
diff changeset
   696
        if mode = FO then
f6b1ee5b420b try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents: 37417
diff changeset
   697
          lmap
f6b1ee5b420b try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents: 37417
diff changeset
   698
        else
f6b1ee5b420b try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents: 37417
diff changeset
   699
          let
f6b1ee5b420b try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents: 37417
diff changeset
   700
            val helper_ths =
f6b1ee5b420b try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents: 37417
diff changeset
   701
              helpers |> filter (is_used o fst)
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   702
                      |> maps (fn (c, (needs_full_types, thms)) =>
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   703
                                  if not (is_used c) orelse
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   704
                                     needs_full_types andalso mode <> FT then
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   705
                                    []
37479
f6b1ee5b420b try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents: 37417
diff changeset
   706
                                  else
38606
3003ddbd46d9 encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
blanchet
parents: 38433
diff changeset
   707
                                    thms)
37479
f6b1ee5b420b try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents: 37417
diff changeset
   708
          in lmap |> fold (add_thm false) helper_ths end
37410
2bf7e6136047 adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents: 37402
diff changeset
   709
  in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   710
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   711
fun refute cls =
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   712
    Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   713
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   714
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
   715
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   716
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
   717
37573
7f987e8582a7 fewer dependencies
blanchet
parents: 37572
diff changeset
   718
37516
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   719
(* Main function to start Metis proof and reconstruction *)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   720
fun FOL_SOLVE mode ctxt cls ths0 =
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   721
  let val thy = ProofContext.theory_of ctxt
35826
1590abc3d42a renamed Sledgehammer structures
blanchet
parents: 35825
diff changeset
   722
      val th_cls_pairs =
38016
135f7d489492 get rid of more dead wood
blanchet
parents: 37994
diff changeset
   723
        map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy th)) ths0
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   724
      val ths = maps #2 th_cls_pairs
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   725
      val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   726
      val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   727
      val _ = trace_msg (fn () => "THEOREM CLAUSES")
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   728
      val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths
37625
35eeb95c5bee rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents: 37623
diff changeset
   729
      val (mode, {axioms, tfrees, skolems}) = build_map mode ctxt cls ths
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   730
      val _ = if null tfrees then ()
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   731
              else (trace_msg (fn () => "TFREE CLAUSES");
37643
f576af716aa6 rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents: 37632
diff changeset
   732
                    app (fn TyLitFree ((s, _), (s', _)) =>
37573
7f987e8582a7 fewer dependencies
blanchet
parents: 37572
diff changeset
   733
                            trace_msg (fn _ => s ^ "(" ^ s' ^ ")")) tfrees)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   734
      val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   735
      val thms = map #1 axioms
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   736
      val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   737
      val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   738
      val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   739
  in
33317
b4534348b8fd standardized filter/filter_out;
wenzelm
parents: 33316
diff changeset
   740
      case filter (is_false o prop_of) cls of
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   741
          false_th::_ => [false_th RS @{thm FalseE}]
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   742
        | [] =>
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   743
      case refute thms of
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   744
          Metis.Resolution.Contradiction mth =>
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   745
            let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   746
                          Metis.Thm.toString mth)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   747
                val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   748
                             (*add constraints arising from converting goal to clause form*)
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   749
                val proof = Metis.Proof.proof mth
38280
577f138af235 replace recursion with "fold"
blanchet
parents: 38100
diff changeset
   750
                val result = fold (translate_one ctxt' mode skolems) proof axioms
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   751
                and used = map_filter (used_axioms axioms) proof
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   752
                val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   753
                val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
33305
wenzelm
parents: 33243
diff changeset
   754
                val unused = th_cls_pairs |> map_filter (fn (name, cls) =>
wenzelm
parents: 33243
diff changeset
   755
                  if common_thm used cls then NONE else SOME name)
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   756
            in
36383
6adf1068ac0f better error reporting;
blanchet
parents: 36230
diff changeset
   757
                if not (null cls) andalso not (common_thm used cls) then
6adf1068ac0f better error reporting;
blanchet
parents: 36230
diff changeset
   758
                  warning "Metis: The assumptions are inconsistent."
6adf1068ac0f better error reporting;
blanchet
parents: 36230
diff changeset
   759
                else
6adf1068ac0f better error reporting;
blanchet
parents: 36230
diff changeset
   760
                  ();
6adf1068ac0f better error reporting;
blanchet
parents: 36230
diff changeset
   761
                if not (null unused) then
36230
43d10a494c91 added warning about inconsistent context to Metis;
blanchet
parents: 36170
diff changeset
   762
                  warning ("Metis: Unused theorems: " ^ commas_quote unused
43d10a494c91 added warning about inconsistent context to Metis;
blanchet
parents: 36170
diff changeset
   763
                           ^ ".")
43d10a494c91 added warning about inconsistent context to Metis;
blanchet
parents: 36170
diff changeset
   764
                else
43d10a494c91 added warning about inconsistent context to Metis;
blanchet
parents: 36170
diff changeset
   765
                  ();
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   766
                case result of
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   767
                    (_,ith)::_ =>
36230
43d10a494c91 added warning about inconsistent context to Metis;
blanchet
parents: 36170
diff changeset
   768
                        (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   769
                         [ith])
38097
5e4ad2df09f3 revert exception throwing in FOL_SOLVE, since they're not caught anyway
blanchet
parents: 38028
diff changeset
   770
                  | _ => (trace_msg (fn () => "Metis: No result"); [])
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   771
            end
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   772
        | Metis.Resolution.Satisfiable _ =>
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   773
            (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
38097
5e4ad2df09f3 revert exception throwing in FOL_SOLVE, since they're not caught anyway
blanchet
parents: 38028
diff changeset
   774
             [])
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   775
  end;
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   776
38632
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   777
(* Extensionalize "th", because that makes sense and that's what Sledgehammer
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   778
   does, but also keep an unextensionalized version of "th" for backward
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   779
   compatibility. *)
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   780
fun also_extensionalize_theorem th =
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   781
  let val th' = Clausifier.extensionalize_theorem th in
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   782
    if Thm.eq_thm (th, th') then [th]
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   783
    else th :: Meson.make_clauses_unsorted [th']
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   784
  end
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   785
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   786
val neg_clausify =
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   787
  single
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   788
  #> Meson.make_clauses_unsorted
38632
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   789
  #> maps also_extensionalize_theorem
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   790
  #> map Clausifier.introduce_combinators_in_theorem
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   791
  #> Meson.finish_cnf
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   792
38652
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38632
diff changeset
   793
val type_has_top_sort =
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38632
diff changeset
   794
  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
e063be321438 perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents: 38632
diff changeset
   795
37516
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   796
fun generic_metis_tac mode ctxt ths i st0 =
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   797
  let
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   798
    val _ = trace_msg (fn () =>
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   799
        "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   800
  in
37626
1146291fe718 move blacklisting completely out of the clausifier;
blanchet
parents: 37625
diff changeset
   801
    if exists_type type_has_top_sort (prop_of st0) then
37516
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   802
      (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
35568
8fbbfc39508f renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
wenzelm
parents: 34087
diff changeset
   803
    else
38028
22dcaec5fa77 minor refactoring
blanchet
parents: 38027
diff changeset
   804
      Meson.MESON (maps neg_clausify)
37926
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   805
                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
e6ff246c0cdb renamings + only need second component of name pool to reconstruct proofs
blanchet
parents: 37925
diff changeset
   806
                  ctxt i st0
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   807
  end
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   808
37516
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   809
val metis_tac = generic_metis_tac HO
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   810
val metisF_tac = generic_metis_tac FO
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   811
val metisFT_tac = generic_metis_tac FT
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   812
38632
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   813
(* Whenever "X" has schematic type variables, we treat "using X by metis" as
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   814
   "by (metis X)", to prevent "Subgoal.FOCUS" from freezing the type variables.
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   815
   We don't do it for nonschematic facts "X" because this breaks a few proofs
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   816
   (in the rare and subtle case where a proof relied on extensionality not being
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   817
   applied) and brings no benefits. *)
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   818
val has_tvar =
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   819
  exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of
37516
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   820
fun method name mode =
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   821
  Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
38632
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   822
    METHOD (fn facts =>
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   823
               let
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   824
                 val (schem_facts, nonschem_facts) =
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   825
                   List.partition has_tvar facts
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   826
               in
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   827
                 HEADGOAL (Method.insert_tac nonschem_facts THEN'
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   828
                           CHANGED_PROP
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   829
                           o generic_metis_tac mode ctxt (schem_facts @ ths))
9cde57cdd0e3 treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents: 38614
diff changeset
   830
               end)))
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   831
32956
c39860141415 tuned white space;
wenzelm
parents: 32955
diff changeset
   832
val setup =
37516
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   833
  type_lits_setup
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   834
  #> method @{binding metis} HO "Metis for FOL/HOL problems"
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   835
  #> method @{binding metisF} FO "Metis for FOL problems"
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   836
  #> method @{binding metisFT} FT
c81c86bfc18a have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents: 37509
diff changeset
   837
            "Metis for FOL/HOL problems with fully-typed translation"
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   838
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   839
end;