author | blanchet |
Wed, 25 Aug 2010 09:32:43 +0200 | |
changeset 38741 | 7635bf8918a1 |
parent 38695 | e85ce10cef1a |
child 38748 | 69fea359d3f8 |
permissions | -rw-r--r-- |
35826 | 1 |
(* Title: HOL/Tools/Sledgehammer/metis_tactics.ML |
38027 | 2 |
Author: Kong W. Susanto, Cambridge University Computer Laboratory |
3 |
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory |
|
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 | 6 |
|
29266 | 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 | 10 |
signature METIS_TACTICS = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
11 |
sig |
32955 | 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 | 14 |
val metis_tac: Proof.context -> thm list -> int -> tactic |
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 | 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 | 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 | 24 |
|
32956 | 25 |
val trace = Unsynchronized.ref false; |
35826 | 26 |
fun trace_msg msg = if !trace then tracing (msg ()) else (); |
32955 | 27 |
|
36001 | 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 | 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 | 32 |
(* ------------------------------------------------------------------------- *) |
33 |
(* Useful Theorems *) |
|
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 | 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 | 40 |
(* ------------------------------------------------------------------------- *) |
41 |
(* Useful Functions *) |
|
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 | 55 |
(* Finding the relative location of an untyped term within a list of terms *) |
56 |
fun get_index lit = |
|
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 | 59 |
| get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) |
60 |
then n else get (n+1) xs |
|
61 |
in get 1 end; |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
62 |
|
32956 | 63 |
(* ------------------------------------------------------------------------- *) |
64 |
(* HOL to FOL (Isabelle to Metis) *) |
|
65 |
(* ------------------------------------------------------------------------- *) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
66 |
|
38614 | 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 | 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 | 79 |
(*These two functions insert type literals before the real literals. That is the |
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 | 82 |
fun hol_term_to_fol_FO tm = |
35865 | 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 | 86 |
val args = map hol_term_to_fol_FO tms |
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 | 94 |
| hol_term_to_fol_HO (CombApp (tm1, tm2)) = |
32994 | 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 | 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 | 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 | 103 |
| hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) = |
32956 | 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 | 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 | 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 | 112 |
| hol_literal_to_fol HO (FOLLiteral (pos, tm)) = |
35865 | 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 | 115 |
metis_lit pos "=" (map hol_term_to_fol_HO tms) |
116 |
| _ => metis_lit pos "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) |
|
117 |
| hol_literal_to_fol FT (FOLLiteral (pos, tm)) = |
|
35865 | 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 | 120 |
metis_lit pos "=" (map hol_term_to_fol_FT tms) |
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 | 124 |
let val (lits, types_sorts) = literals_of_term thy t |
32956 | 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 | 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 | 133 |
fun default_sort _ (TVar _) = false |
33035 | 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 | 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 | 145 |
in |
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 | 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 | 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 | 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 | 157 |
end |
158 |
end; |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
159 |
|
32956 | 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 | 167 |
(*TrueI is returned as the Isabelle counterpart because there isn't any.*) |
35865 | 168 |
fun arity_cls (ArityClause {conclLit, premLits, ...}) = |
32956 | 169 |
(TrueI, |
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 | 172 |
(* CLASSREL CLAUSE *) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
173 |
|
37925 | 174 |
fun m_class_rel_cls (subclass, _) (superclass, _) = |
32956 | 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 | 177 |
fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) = |
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 | 180 |
(* ------------------------------------------------------------------------- *) |
181 |
(* FOL to HOL (Metis to Isabelle) *) |
|
182 |
(* ------------------------------------------------------------------------- *) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
183 |
|
32956 | 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 | 186 |
fun terms_of [] = [] |
187 |
| terms_of (Term t :: tts) = t :: terms_of tts |
|
188 |
| terms_of (Type _ :: tts) = terms_of tts; |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
189 |
|
32956 | 190 |
fun types_of [] = [] |
32994 | 191 |
| types_of (Term (Term.Var ((a,idx), _)) :: tts) = |
32956 | 192 |
if String.isPrefix "_" a then |
193 |
(*Variable generated by Metis, which might have been a type variable.*) |
|
32994 | 194 |
TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts |
32956 | 195 |
else types_of tts |
196 |
| types_of (Term _ :: tts) = types_of tts |
|
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 | 199 |
fun apply_list rator nargs rands = |
200 |
let val trands = terms_of rands |
|
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 | 203 |
("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ |
204 |
" expected " ^ Int.toString nargs ^ |
|
205 |
" received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) |
|
206 |
end; |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
207 |
|
24500 | 208 |
fun infer_types ctxt = |
209 |
Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); |
|
25713 | 210 |
|
32956 | 211 |
(*We use 1 rather than 0 because variable references in clauses may otherwise conflict |
212 |
with variable constraints in the goal...at least, type inference often fails otherwise. |
|
213 |
SEE ALSO axiom_inf below.*) |
|
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 | 216 |
(*include the default sort, if available*) |
217 |
fun mk_tfree ctxt w = |
|
218 |
let val ww = "'" ^ w |
|
33035 | 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 | 221 |
(*Remove the "apply" operator from an HO term*) |
222 |
fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t |
|
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) = |
37992 | 231 |
(case strip_prefix_and_undo_ascii tvar_prefix v of |
35865 | 232 |
SOME w => make_tvar w |
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)) = |
37992 | 235 |
(case strip_prefix_and_undo_ascii 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 | 238 |
| NONE => |
37992 | 239 |
case strip_prefix_and_undo_ascii tfree_prefix x of |
32956 | 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 | 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 | 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 | 248 |
fun tm_to_tt (Metis.Term.Var v) = |
37992 | 249 |
(case strip_prefix_and_undo_ascii tvar_prefix v of |
35865 | 250 |
SOME w => Type (make_tvar w) |
32956 | 251 |
| NONE => |
37992 | 252 |
case strip_prefix_and_undo_ascii schematic_var_prefix v of |
32956 | 253 |
SOME w => Term (mk_var (w, HOLogic.typeT)) |
254 |
| NONE => Term (mk_var (v, HOLogic.typeT)) ) |
|
255 |
(*Var from Metis with a name like _nnn; possibly a type variable*) |
|
256 |
| tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) |
|
257 |
| tm_to_tt (t as Metis.Term.Fn (".",_)) = |
|
258 |
let val (rator,rands) = strip_happ [] t |
|
259 |
in case rator of |
|
260 |
Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) |
|
261 |
| _ => case tm_to_tt rator of |
|
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 | 264 |
end |
265 |
| tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args) |
|
266 |
and applic_to_tt ("=",ts) = |
|
35865 | 267 |
Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts))) |
32956 | 268 |
| applic_to_tt (a,ts) = |
37992 | 269 |
case strip_prefix_and_undo_ascii const_prefix a of |
32956 | 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 | 273 |
val nterms = length ts - ntypes |
274 |
val tts = map tm_to_tt ts |
|
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 | 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 | 285 |
end |
286 |
| NONE => (*Not a constant. Is it a type constructor?*) |
|
37992 | 287 |
case strip_prefix_and_undo_ascii type_const_prefix a of |
33227 | 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 | 290 |
| NONE => (*Maybe a TFree. Should then check that ts=[].*) |
37992 | 291 |
case strip_prefix_and_undo_ascii tfree_prefix a of |
32956 | 292 |
SOME b => Type (mk_tfree ctxt b) |
293 |
| NONE => (*a fixed variable? They are Skolem functions.*) |
|
37992 | 294 |
case strip_prefix_and_undo_ascii fixed_var_prefix a of |
32956 | 295 |
SOME b => |
296 |
let val opr = Term.Free(b, HOLogic.typeT) |
|
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 | 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 | 309 |
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = |
37992 | 310 |
(case strip_prefix_and_undo_ascii schematic_var_prefix v of |
32956 | 311 |
SOME w => mk_var(w, dummyT) |
312 |
| NONE => mk_var(v, dummyT)) |
|
32994 | 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 | 315 |
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = |
37992 | 316 |
(case strip_prefix_and_undo_ascii 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 | 318 |
| NONE => (*Not a constant. Is it a fixed variable??*) |
37992 | 319 |
case strip_prefix_and_undo_ascii 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 | 322 |
| cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = |
323 |
cvt tm1 $ cvt tm2 |
|
324 |
| cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*) |
|
325 |
cvt tm1 $ cvt tm2 |
|
326 |
| cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) |
|
327 |
| cvt (Metis.Term.Fn ("=", [tm1,tm2])) = |
|
35865 | 328 |
list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2]) |
32956 | 329 |
| cvt (t as Metis.Term.Fn (x, [])) = |
37992 | 330 |
(case strip_prefix_and_undo_ascii 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 | 332 |
| NONE => (*Not a constant. Is it a fixed variable??*) |
37992 | 333 |
case strip_prefix_and_undo_ascii fixed_var_prefix x of |
32956 | 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 | 346 |
val _ = trace_msg (fn () => " calling type inference:") |
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 | 349 |
val _ = app (fn t => trace_msg |
350 |
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ |
|
351 |
" of type " ^ Syntax.string_of_typ ctxt (type_of t))) |
|
352 |
ts' |
|
353 |
in ts' end; |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
354 |
|
35865 | 355 |
fun mk_not (Const (@{const_name Not}, _) $ b) = b |
32956 | 356 |
| mk_not b = HOLogic.mk_not b; |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
357 |
|
32956 | 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 | 360 |
(* ------------------------------------------------------------------------- *) |
361 |
(* FOL step Inference Rules *) |
|
362 |
(* ------------------------------------------------------------------------- *) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
363 |
|
32956 | 364 |
(*for debugging only*) |
365 |
fun print_thpair (fth,th) = |
|
366 |
(trace_msg (fn () => "============================================="); |
|
367 |
trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth); |
|
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 | 370 |
fun lookth thpairs (fth : Metis.Thm.thm) = |
33035 | 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 | 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 | 377 |
fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); |
24974 | 378 |
|
32956 | 379 |
fun inst_excluded_middle thy i_atm = |
380 |
let val th = EXCLUDED_MIDDLE |
|
381 |
val [vx] = Term.add_vars (prop_of th) [] |
|
382 |
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)] |
|
383 |
in cterm_instantiate substs th end; |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
384 |
|
32956 | 385 |
(* INFERENCE RULE: AXIOM *) |
36945 | 386 |
fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th); |
32956 | 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 | 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 | 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 | 395 |
(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct |
396 |
them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange |
|
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 | 399 |
let val thy = ProofContext.theory_of ctxt |
400 |
val i_th = lookth thpairs th |
|
401 |
val i_th_vars = Term.add_vars (prop_of i_th) [] |
|
33035 | 402 |
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) |
32956 | 403 |
fun subst_translation (x,y) = |
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 | 407 |
in SOME (cterm_of thy (Var v), t) end |
408 |
handle Option => |
|
409 |
(trace_msg (fn() => "List.find failed for the variable " ^ x ^ |
|
410 |
" in " ^ Display.string_of_thm ctxt i_th); |
|
411 |
NONE) |
|
412 |
fun remove_typeinst (a, t) = |
|
37992 | 413 |
case strip_prefix_and_undo_ascii schematic_var_prefix a of |
32956 | 414 |
SOME b => SOME (b, t) |
37992 | 415 |
| NONE => case strip_prefix_and_undo_ascii tvar_prefix a of |
32956 | 416 |
SOME _ => NONE (*type instantiations are forbidden!*) |
417 |
| NONE => SOME (a,t) (*internal Metis var?*) |
|
418 |
val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) |
|
419 |
val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst) |
|
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 | 422 |
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) |
423 |
val substs' = ListPair.zip (vars, map ctm_of tms) |
|
424 |
val _ = trace_msg (fn () => |
|
425 |
cat_lines ("subst_translations:" :: |
|
426 |
(substs' |> map (fn (x, y) => |
|
427 |
Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ |
|
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 | 433 |
(* INFERENCE RULE: RESOLVE *) |
25713 | 434 |
|
32956 | 435 |
(*Like RSN, but we rename apart only the type variables. Vars here typically have an index |
436 |
of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars |
|
437 |
could then fail. See comment on mk_var.*) |
|
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 | 441 |
val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb) |
442 |
in |
|
443 |
case distinct Thm.eq_thm ths of |
|
444 |
[th] => th |
|
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 | 449 |
let |
450 |
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 |
|
451 |
val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) |
|
452 |
val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) |
|
453 |
in |
|
454 |
if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*) |
|
455 |
else if is_TrueI i_th2 then i_th1 |
|
456 |
else |
|
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 | 460 |
val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) |
461 |
val prems_th1 = prems_of i_th1 |
|
462 |
val prems_th2 = prems_of i_th2 |
|
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 | 465 |
val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) |
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 | 468 |
val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) |
469 |
in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end |
|
470 |
end; |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
471 |
|
32956 | 472 |
(* INFERENCE RULE: REFL *) |
473 |
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); |
|
474 |
val refl_idx = 1 + Thm.maxidx_of REFL_THM; |
|
25713 | 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 | 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 | 479 |
val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) |
480 |
val c_t = cterm_incr_types thy refl_idx i_t |
|
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 | 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 | 485 |
| get_ty_arg_size _ _ = 0; |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
486 |
|
32956 | 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 | 489 |
let val thy = ProofContext.theory_of ctxt |
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 | 492 |
val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) |
32994 | 493 |
fun replace_item_list lx 0 (_::ls) = lx::ls |
32956 | 494 |
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls |
495 |
fun path_finder_FO tm [] = (tm, Term.Bound 0) |
|
496 |
| path_finder_FO tm (p::ps) = |
|
35865 | 497 |
let val (tm1,args) = strip_comb tm |
32956 | 498 |
val adjustment = get_ty_arg_size thy tm1 |
499 |
val p' = if adjustment > p then p else p-adjustment |
|
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 | 506 |
val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ |
507 |
" " ^ Syntax.string_of_term ctxt tm_p) |
|
508 |
val (r,t) = path_finder_FO tm_p ps |
|
509 |
in |
|
510 |
(r, list_comb (tm1, replace_item_list t p' args)) |
|
511 |
end |
|
512 |
fun path_finder_HO tm [] = (tm, Term.Bound 0) |
|
513 |
| path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) |
|
32994 | 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 | 519 |
fun path_finder_FT tm [] _ = (tm, Term.Bound 0) |
32994 | 520 |
| path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) = |
32956 | 521 |
path_finder_FT tm ps t1 |
32994 | 522 |
| path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1, _])) = |
32956 | 523 |
(fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) |
32994 | 524 |
| path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) = |
32956 | 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 | 531 |
fun path_finder FO tm ps _ = path_finder_FO tm ps |
35865 | 532 |
| path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ = |
32956 | 533 |
(*equality: not curried, as other predicates are*) |
534 |
if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) |
|
535 |
else path_finder_HO tm (p::ps) (*1 selects second operand*) |
|
32994 | 536 |
| path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) = |
32956 | 537 |
path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) |
35865 | 538 |
| path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps) |
32956 | 539 |
(Metis.Term.Fn ("=", [t1,t2])) = |
540 |
(*equality: not curried, as other predicates are*) |
|
541 |
if p=0 then path_finder_FT tm (0::1::ps) |
|
542 |
(Metis.Term.Fn (".", [Metis.Term.Fn (".", [metis_eq,t1]), t2])) |
|
543 |
(*select first operand*) |
|
544 |
else path_finder_FT tm (p::ps) |
|
545 |
(Metis.Term.Fn (".", [metis_eq,t2])) |
|
546 |
(*1 selects second operand*) |
|
32994 | 547 |
| path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 |
32956 | 548 |
(*if not equality, ignore head to skip the hBOOL predicate*) |
549 |
| path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) |
|
35865 | 550 |
fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx = |
32956 | 551 |
let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm |
552 |
in (tm, nt $ tm_rslt) end |
|
553 |
| path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm |
|
554 |
val (tm_subst, body) = path_finder_lit i_atm fp |
|
555 |
val tm_abs = Term.Abs("x", Term.type_of tm_subst, body) |
|
556 |
val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) |
|
557 |
val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) |
|
558 |
val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) |
|
559 |
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) |
|
36945 | 560 |
val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) |
32956 | 561 |
val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') |
562 |
val eq_terms = map (pairself (cterm_of thy)) |
|
33227 | 563 |
(ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) |
32956 | 564 |
in cterm_instantiate eq_terms subst' end; |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
565 |
|
32956 | 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 | 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 | 582 |
fun translate_one ctxt mode skolems (fol_th, inf) thpairs = |
583 |
let |
|
584 |
val _ = trace_msg (fn () => "=============================================") |
|
585 |
val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th) |
|
586 |
val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf) |
|
587 |
val th = Meson.flexflex_first_order (step ctxt mode skolems |
|
588 |
thpairs (fol_th, inf)) |
|
589 |
val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) |
|
590 |
val _ = trace_msg (fn () => "=============================================") |
|
591 |
val n_metis_lits = |
|
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 | 595 |
in (fol_th, th) :: thpairs end |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
596 |
|
32956 | 597 |
(*Determining which axiom clauses are actually used*) |
598 |
fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th) |
|
32994 | 599 |
| used_axioms _ _ = NONE; |
24855 | 600 |
|
32956 | 601 |
(* ------------------------------------------------------------------------- *) |
602 |
(* Translation of HO Clauses *) |
|
603 |
(* ------------------------------------------------------------------------- *) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
604 |
|
32956 | 605 |
fun type_ext thy tms = |
35865 | 606 |
let val subs = tfree_classes_of_terms tms |
607 |
val supers = tvar_classes_of_terms tms |
|
608 |
and tycons = type_consts_of_terms thy tms |
|
609 |
val (supers', arity_clauses) = make_arity_clauses thy tycons supers |
|
37925 | 610 |
val class_rel_clauses = make_class_rel_clauses thy subs supers' |
611 |
in map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses |
|
32956 | 612 |
end; |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
613 |
|
32956 | 614 |
(* ------------------------------------------------------------------------- *) |
615 |
(* Logic maps manage the interface between HOL and first-order logic. *) |
|
616 |
(* ------------------------------------------------------------------------- *) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
617 |
|
32956 | 618 |
type logic_map = |
35865 | 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 | 623 |
fun const_in_metis c (pred, tm_list) = |
32956 | 624 |
let |
32994 | 625 |
fun in_mterm (Metis.Term.Var _) = false |
32956 | 626 |
| in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list |
627 |
| in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list |
|
32994 | 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 | 630 |
(*Extract TFree constraints from context to include as conjecture clauses*) |
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 | 637 |
(*transform isabelle type / arity clause to metis clause *) |
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 | 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 | 648 |
|
32956 | 649 |
fun string_of_mode FO = "FO" |
650 |
| string_of_mode HO = "HO" |
|
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 | 668 |
(* Function to generate metis clauses, including comb and type clauses *) |
669 |
fun build_map mode0 ctxt cls ths = |
|
670 |
let val thy = ProofContext.theory_of ctxt |
|
671 |
(*The modes FO and FT are sticky. HO can be downgraded to FO.*) |
|
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 | 675 |
| set_mode FT = FT |
676 |
val mode = set_mode mode0 |
|
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 | 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 | 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 | 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 | 711 |
fun refute cls = |
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 | 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 | 716 |
fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2); |
24855 | 717 |
|
37573 | 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 | 720 |
fun FOL_SOLVE mode ctxt cls ths0 = |
721 |
let val thy = ProofContext.theory_of ctxt |
|
35826 | 722 |
val th_cls_pairs = |
38016 | 723 |
map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy th)) ths0 |
32956 | 724 |
val ths = maps #2 th_cls_pairs |
725 |
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") |
|
726 |
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls |
|
727 |
val _ = trace_msg (fn () => "THEOREM CLAUSES") |
|
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 | 730 |
val _ = if null tfrees then () |
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 | 733 |
trace_msg (fn _ => s ^ "(" ^ s' ^ ")")) tfrees) |
32956 | 734 |
val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") |
735 |
val thms = map #1 axioms |
|
736 |
val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms |
|
737 |
val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode) |
|
738 |
val _ = trace_msg (fn () => "START METIS PROVE PROCESS") |
|
739 |
in |
|
33317 | 740 |
case filter (is_false o prop_of) cls of |
32956 | 741 |
false_th::_ => [false_th RS @{thm FalseE}] |
742 |
| [] => |
|
743 |
case refute thms of |
|
744 |
Metis.Resolution.Contradiction mth => |
|
745 |
let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^ |
|
746 |
Metis.Thm.toString mth) |
|
747 |
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt |
|
748 |
(*add constraints arising from converting goal to clause form*) |
|
749 |
val proof = Metis.Proof.proof mth |
|
38280 | 750 |
val result = fold (translate_one ctxt' mode skolems) proof axioms |
32956 | 751 |
and used = map_filter (used_axioms axioms) proof |
752 |
val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:") |
|
753 |
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used |
|
33305 | 754 |
val unused = th_cls_pairs |> map_filter (fn (name, cls) => |
755 |
if common_thm used cls then NONE else SOME name) |
|
32956 | 756 |
in |
36383 | 757 |
if not (null cls) andalso not (common_thm used cls) then |
758 |
warning "Metis: The assumptions are inconsistent." |
|
759 |
else |
|
760 |
(); |
|
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 | 766 |
case result of |
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 | 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 | 771 |
end |
772 |
| Metis.Resolution.Satisfiable _ => |
|
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 | 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 | 786 |
val neg_clausify = |
787 |
single |
|
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 | 790 |
#> map Clausifier.introduce_combinators_in_theorem |
791 |
#> Meson.finish_cnf |
|
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 | 799 |
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) |
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 | 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 | 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 | 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; |