author  blanchet 
Tue, 29 Jun 2010 09:26:56 +0200  
changeset 37625  35eeb95c5bee 
parent 37623  295f3a9b44b6 
child 37626  1146291fe718 
permissions  rwrr 
35826  1 
(* Title: HOL/Tools/Sledgehammer/metis_tactics.ML 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

2 
Author: Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

3 
Copyright Cambridge University 2007 
23447  4 

29266  5 
HOL setup for the Metis prover. 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

6 
*) 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

7 

35826  8 
signature METIS_TACTICS = 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

9 
sig 
32955  10 
val trace: bool Unsynchronized.ref 
24309
01f3e1a43c24
turned type_lits into configuration option (with attribute);
wenzelm
parents:
24300
diff
changeset

11 
val type_lits: bool Config.T 
24319  12 
val metis_tac: Proof.context > thm list > int > tactic 
13 
val metisF_tac: Proof.context > thm list > int > tactic 

32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

14 
val metisFT_tac: Proof.context > thm list > int > tactic 
24319  15 
val setup: theory > theory 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

16 
end 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

17 

35826  18 
structure Metis_Tactics : METIS_TACTICS = 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

19 
struct 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

20 

37574
b8c1f4c46983
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet
parents:
37573
diff
changeset

21 
open Clausifier 
37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37577
diff
changeset

22 
open Metis_Clauses 
35826  23 

37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

24 
exception METIS of string * string 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

25 

32956  26 
val trace = Unsynchronized.ref false; 
35826  27 
fun trace_msg msg = if !trace then tracing (msg ()) else (); 
32955  28 

36001  29 
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

30 

35826  31 
datatype mode = FO  HO  FT (* firstorder, higherorder, fullytyped *) 
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

32 

32956  33 
(*  *) 
34 
(* Useful Theorems *) 

35 
(*  *) 

33689
d0a9ce721e0c
properly inlined @{lemma} antiqutations  might also reduce proof terms a bit;
wenzelm
parents:
33339
diff
changeset

36 
val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} 
36945  37 
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

38 
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

39 
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

40 

32956  41 
(*  *) 
42 
(* Useful Functions *) 

43 
(*  *) 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

44 

37417
0714ece49081
A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents:
37410
diff
changeset

45 
(* Match untyped terms. *) 
0714ece49081
A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents:
37410
diff
changeset

46 
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

47 
 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

48 
 untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) = 
0714ece49081
A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents:
37410
diff
changeset

49 
(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

50 
 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

51 
 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

52 
 untyped_aconv (t1 $ t2) (u1 $ u2) = 
0714ece49081
A function called "untyped_aconv" shouldn't look at the bound names!
blanchet
parents:
37410
diff
changeset

53 
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

54 
 untyped_aconv _ _ = false 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

55 

32956  56 
(* Finding the relative location of an untyped term within a list of terms *) 
57 
fun get_index lit = 

58 
let val lit = Envir.eta_contract lit 

37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

59 
fun get _ [] = raise Empty 
32956  60 
 get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) 
61 
then n else get (n+1) xs 

62 
in get 1 end; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

63 

32956  64 
(*  *) 
65 
(* HOL to FOL (Isabelle to Metis) *) 

66 
(*  *) 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

67 

32956  68 
fun fn_isa_to_met "equal" = "=" 
69 
 fn_isa_to_met x = x; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

70 

32956  71 
fun metis_lit b c args = (b, (c, args)); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

72 

36169
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

73 
fun hol_type_to_fol (TyVar (x, _)) = Metis.Term.Var x 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

74 
 hol_type_to_fol (TyFree (s, _)) = Metis.Term.Fn (s, []) 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

75 
 hol_type_to_fol (TyConstr ((s, _), tps)) = 
27b1cc58715e
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet
parents:
36168
diff
changeset

76 
Metis.Term.Fn (s, map hol_type_to_fol tps); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

77 

32956  78 
(*These two functions insert type literals before the real literals. That is the 
79 
opposite order from TPTP linkup, but maybe OK.*) 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

80 

32956  81 
fun hol_term_to_fol_FO tm = 
35865  82 
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

83 
(CombConst ((c, _), _, tys), tms) => 
32956  84 
let val tyargs = map hol_type_to_fol tys 
85 
val args = map hol_term_to_fol_FO tms 

86 
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

87 
 (CombVar ((v, _), _), []) => Metis.Term.Var v 
37402
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

88 
 _ => raise Fail "hol_term_to_fol_FO"; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

89 

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

90 
fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s 
0cdb76723c88
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
blanchet
parents:
36169
diff
changeset

91 
 hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) = 
32994  92 
Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist) 
35865  93 
 hol_term_to_fol_HO (CombApp (tm1, tm2)) = 
32994  94 
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

95 

32956  96 
(*The fullytyped translation, to avoid type errors*) 
97 
fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]); 

98 

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

99 
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

100 
 hol_term_to_fol_FT (CombConst((a, _), ty, _)) = 
32956  101 
wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty) 
35865  102 
 hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) = 
32956  103 
wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), 
35865  104 
type_of_combterm tm); 
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

105 

35865  106 
fun hol_literal_to_fol FO (Literal (pol, 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

107 
let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm 
32956  108 
val tylits = if p = "equal" then [] else map hol_type_to_fol tys 
109 
val lits = map hol_term_to_fol_FO tms 

110 
in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end 

35865  111 
 hol_literal_to_fol HO (Literal (pol, tm)) = 
112 
(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

113 
(CombConst(("equal", _), _, _), tms) => 
32956  114 
metis_lit pol "=" (map hol_term_to_fol_HO tms) 
115 
 _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) 

35865  116 
 hol_literal_to_fol FT (Literal (pol, tm)) = 
117 
(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

118 
(CombConst(("equal", _), _, _), tms) => 
32956  119 
metis_lit pol "=" (map hol_term_to_fol_FT tms) 
120 
 _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

121 

37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

122 
fun literals_of_hol_term thy mode t = 
35865  123 
let val (lits, types_sorts) = literals_of_term thy t 
32956  124 
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

125 

32956  126 
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) 
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

127 
fun metis_of_type_literals pos (TyLitVar (s, (s', _))) = 
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

128 
metis_lit pos s [Metis.Term.Var s'] 
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_of_type_literals pos (TyLitFree (s, (s', _))) = 
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

130 
metis_lit pos s [Metis.Term.Fn (s',[])] 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

131 

32994  132 
fun default_sort _ (TVar _) = false 
33035  133 
 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

134 

32956  135 
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

136 
Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf)); 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

137 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

138 
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

139 
let 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

140 
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

141 
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

142 
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

143 
> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode) 
32956  144 
in 
145 
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

146 
(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

147 
type_literals_for_types types_sorts, skolems) 
32956  148 
else 
36966
adc11fb3f3aa
generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents:
36945
diff
changeset

149 
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

150 
> type_literals_for_types 
32956  151 
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

152 
then map (metis_of_type_literals false) tylits else [] 
32956  153 
in 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

154 
(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

155 
skolems) 
32956  156 
end 
157 
end; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

158 

32956  159 
(* ARITY CLAUSE *) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

160 

35865  161 
fun m_arity_cls (TConsLit (c,t,args)) = 
162 
metis_lit true (make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)] 

163 
 m_arity_cls (TVarLit (c,str)) = 

164 
metis_lit false (make_type_class c) [Metis.Term.Var str]; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

165 

32956  166 
(*TrueI is returned as the Isabelle counterpart because there isn't any.*) 
35865  167 
fun arity_cls (ArityClause {conclLit, premLits, ...}) = 
32956  168 
(TrueI, 
169 
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

170 

32956  171 
(* CLASSREL CLAUSE *) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

172 

32956  173 
fun m_classrel_cls subclass superclass = 
174 
[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

175 

35865  176 
fun classrel_cls (ClassrelClause {subclass, superclass, ...}) = 
32956  177 
(TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass))); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

178 

32956  179 
(*  *) 
180 
(* FOL to HOL (Metis to Isabelle) *) 

181 
(*  *) 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

182 

32956  183 
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

184 

32956  185 
fun terms_of [] = [] 
186 
 terms_of (Term t :: tts) = t :: terms_of tts 

187 
 terms_of (Type _ :: tts) = terms_of tts; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

188 

32956  189 
fun types_of [] = [] 
32994  190 
 types_of (Term (Term.Var ((a,idx), _)) :: tts) = 
32956  191 
if String.isPrefix "_" a then 
192 
(*Variable generated by Metis, which might have been a type variable.*) 

32994  193 
TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts 
32956  194 
else types_of tts 
195 
 types_of (Term _ :: tts) = types_of tts 

196 
 types_of (Type T :: tts) = T :: types_of tts; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

197 

32956  198 
fun apply_list rator nargs rands = 
199 
let val trands = terms_of rands 

200 
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

201 
else raise Fail 
32956  202 
("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ 
203 
" expected " ^ Int.toString nargs ^ 

204 
" received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) 

205 
end; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

206 

24500  207 
fun infer_types ctxt = 
208 
Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); 

25713  209 

32956  210 
(*We use 1 rather than 0 because variable references in clauses may otherwise conflict 
211 
with variable constraints in the goal...at least, type inference often fails otherwise. 

212 
SEE ALSO axiom_inf below.*) 

213 
fun mk_var (w,T) = Term.Var((w,1), T); 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

214 

32956  215 
(*include the default sort, if available*) 
216 
fun mk_tfree ctxt w = 

217 
let val ww = "'" ^ w 

33035  218 
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

219 

32956  220 
(*Remove the "apply" operator from an HO term*) 
221 
fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t 

222 
 strip_happ args x = (x, args); 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

223 

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

224 
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

225 

32994  226 
fun fol_type_to_isa _ (Metis.Term.Var v) = 
35865  227 
(case strip_prefix tvar_prefix v of 
228 
SOME w => make_tvar w 

229 
 NONE => make_tvar v) 

32956  230 
 fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) = 
35865  231 
(case strip_prefix tconst_prefix x of 
37572
a899f9506f39
more intramodule dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37566
diff
changeset

232 
SOME tc => Term.Type (invert_const tc, map (fol_type_to_isa ctxt) tys) 
32956  233 
 NONE => 
35865  234 
case strip_prefix tfree_prefix x of 
32956  235 
SOME tf => mk_tfree ctxt tf 
37402
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

236 
 NONE => raise Fail ("fol_type_to_isa: " ^ x)); 
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

237 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

238 
fun reveal_skolem_terms skolems = 
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

239 
map_aterms (fn t as Const (s, _) => 
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37402
diff
changeset

240 
if String.isPrefix skolem_theory_name s then 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

241 
AList.lookup (op =) skolems s > the 
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

242 
> map_types Type_Infer.paramify_vars 
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37402
diff
changeset

243 
else 
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37402
diff
changeset

244 
t 
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37402
diff
changeset

245 
 t => t) 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

246 

32956  247 
(*Maps metis terms to isabelle terms*) 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

248 
fun hol_term_from_fol_PT ctxt fol_tm = 
32956  249 
let val thy = ProofContext.theory_of ctxt 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

250 
val _ = trace_msg (fn () => "hol_term_from_fol_PT: " ^ 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

251 
Metis.Term.toString fol_tm) 
32956  252 
fun tm_to_tt (Metis.Term.Var v) = 
35865  253 
(case strip_prefix tvar_prefix v of 
254 
SOME w => Type (make_tvar w) 

32956  255 
 NONE => 
35865  256 
case strip_prefix schematic_var_prefix v of 
32956  257 
SOME w => Term (mk_var (w, HOLogic.typeT)) 
258 
 NONE => Term (mk_var (v, HOLogic.typeT)) ) 

259 
(*Var from Metis with a name like _nnn; possibly a type variable*) 

260 
 tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) 

261 
 tm_to_tt (t as Metis.Term.Fn (".",_)) = 

262 
let val (rator,rands) = strip_happ [] t 

263 
in case rator of 

264 
Metis.Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) 

265 
 _ => case tm_to_tt rator of 

266 
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

267 
 _ => raise Fail "tm_to_tt: HO application" 
32956  268 
end 
269 
 tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args) 

270 
and applic_to_tt ("=",ts) = 

35865  271 
Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts))) 
32956  272 
 applic_to_tt (a,ts) = 
35865  273 
case strip_prefix const_prefix a of 
32956  274 
SOME b => 
35865  275 
let val c = invert_const b 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36556
diff
changeset

276 
val ntypes = num_type_args thy c 
32956  277 
val nterms = length ts  ntypes 
278 
val tts = map tm_to_tt ts 

279 
val tys = types_of (List.take(tts,ntypes)) 

36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36556
diff
changeset

280 
in if length tys = ntypes then 
32956  281 
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

282 
else 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

283 
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

284 
" but gets " ^ Int.toString (length tys) ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

285 
" type arguments\n" ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

286 
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

287 
" the terms are \n" ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

288 
cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) 
32956  289 
end 
290 
 NONE => (*Not a constant. Is it a type constructor?*) 

35865  291 
case strip_prefix tconst_prefix a of 
33227  292 
SOME b => 
37572
a899f9506f39
more intramodule dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37566
diff
changeset

293 
Type (Term.Type (invert_const b, types_of (map tm_to_tt ts))) 
32956  294 
 NONE => (*Maybe a TFree. Should then check that ts=[].*) 
35865  295 
case strip_prefix tfree_prefix a of 
32956  296 
SOME b => Type (mk_tfree ctxt b) 
297 
 NONE => (*a fixed variable? They are Skolem functions.*) 

35865  298 
case strip_prefix fixed_var_prefix a of 
32956  299 
SOME b => 
300 
let val opr = Term.Free(b, HOLogic.typeT) 

301 
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

302 
 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

303 
in 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

304 
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

305 
Term t => t 
37402
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

306 
 _ => 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

307 
end 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

308 

32956  309 
(*Maps fullytyped metis terms to isabelle terms*) 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

310 
fun hol_term_from_fol_FT ctxt fol_tm = 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

311 
let val _ = trace_msg (fn () => "hol_term_from_fol_FT: " ^ 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

312 
Metis.Term.toString fol_tm) 
32994  313 
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = 
35865  314 
(case strip_prefix schematic_var_prefix v of 
32956  315 
SOME w => mk_var(w, dummyT) 
316 
 NONE => mk_var(v, dummyT)) 

32994  317 
 cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) = 
32956  318 
Const ("op =", HOLogic.typeT) 
319 
 cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = 

35865  320 
(case strip_prefix const_prefix x of 
321 
SOME c => Const (invert_const c, dummyT) 

32956  322 
 NONE => (*Not a constant. Is it a fixed variable??*) 
35865  323 
case strip_prefix fixed_var_prefix x of 
32956  324 
SOME v => Free (v, fol_type_to_isa ctxt ty) 
37402
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

325 
 NONE => raise Fail ("hol_term_from_fol_FT bad constant: " ^ x)) 
32956  326 
 cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = 
327 
cvt tm1 $ cvt tm2 

328 
 cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*) 

329 
cvt tm1 $ cvt tm2 

330 
 cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) 

331 
 cvt (Metis.Term.Fn ("=", [tm1,tm2])) = 

35865  332 
list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2]) 
32956  333 
 cvt (t as Metis.Term.Fn (x, [])) = 
35865  334 
(case strip_prefix const_prefix x of 
335 
SOME c => Const (invert_const c, dummyT) 

32956  336 
 NONE => (*Not a constant. Is it a fixed variable??*) 
35865  337 
case strip_prefix fixed_var_prefix x of 
32956  338 
SOME v => Free (v, dummyT) 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

339 
 NONE => (trace_msg (fn () => "hol_term_from_fol_FT bad const: " ^ x); 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

340 
hol_term_from_fol_PT ctxt t)) 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

341 
 cvt t = (trace_msg (fn () => "hol_term_from_fol_FT bad term: " ^ Metis.Term.toString t); 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

342 
hol_term_from_fol_PT ctxt t) 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

343 
in fol_tm > cvt end 
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

344 

37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

345 
fun hol_term_from_fol FT = hol_term_from_fol_FT 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

346 
 hol_term_from_fol _ = hol_term_from_fol_PT 
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

347 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

348 
fun hol_terms_from_fol ctxt mode skolems fol_tms = 
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

349 
let val ts = map (hol_term_from_fol mode ctxt) fol_tms 
32956  350 
val _ = trace_msg (fn () => " calling type inference:") 
351 
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

352 
val ts' = ts > map (reveal_skolem_terms skolems) > infer_types ctxt 
32956  353 
val _ = app (fn t => trace_msg 
354 
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ 

355 
" of type " ^ Syntax.string_of_typ ctxt (type_of t))) 

356 
ts' 

357 
in ts' end; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

358 

35865  359 
fun mk_not (Const (@{const_name Not}, _) $ b) = b 
32956  360 
 mk_not b = HOLogic.mk_not b; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

361 

32956  362 
val metis_eq = Metis.Term.Fn ("=", []); 
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

363 

32956  364 
(*  *) 
365 
(* FOL step Inference Rules *) 

366 
(*  *) 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

367 

32956  368 
(*for debugging only*) 
369 
fun print_thpair (fth,th) = 

370 
(trace_msg (fn () => "============================================="); 

371 
trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth); 

372 
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

373 

32956  374 
fun lookth thpairs (fth : Metis.Thm.thm) = 
33035  375 
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

376 
handle Option => 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

377 
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

378 

32956  379 
fun is_TrueI th = Thm.eq_thm(TrueI,th); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

380 

32956  381 
fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); 
24974  382 

32956  383 
fun inst_excluded_middle thy i_atm = 
384 
let val th = EXCLUDED_MIDDLE 

385 
val [vx] = Term.add_vars (prop_of th) [] 

386 
val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)] 

387 
in cterm_instantiate substs th end; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

388 

32956  389 
(* INFERENCE RULE: AXIOM *) 
36945  390 
fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th); 
32956  391 
(*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

392 

32956  393 
(* INFERENCE RULE: ASSUME *) 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

394 
fun assume_inf ctxt mode skolems atm = 
32956  395 
inst_excluded_middle 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

396 
(ProofContext.theory_of ctxt) 
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

397 
(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

398 

32956  399 
(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct 
400 
them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange 

401 
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

402 
fun inst_inf ctxt mode skolems thpairs fsubst th = 
32956  403 
let val thy = ProofContext.theory_of ctxt 
404 
val i_th = lookth thpairs th 

405 
val i_th_vars = Term.add_vars (prop_of i_th) [] 

33035  406 
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) 
32956  407 
fun subst_translation (x,y) = 
408 
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

409 
(* We call "reveal_skolem_terms" and "infer_types" below. *) 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

410 
val t = hol_term_from_fol mode ctxt y 
32956  411 
in SOME (cterm_of thy (Var v), t) end 
412 
handle Option => 

413 
(trace_msg (fn() => "List.find failed for the variable " ^ x ^ 

414 
" in " ^ Display.string_of_thm ctxt i_th); 

415 
NONE) 

416 
fun remove_typeinst (a, t) = 

35865  417 
case strip_prefix schematic_var_prefix a of 
32956  418 
SOME b => SOME (b, t) 
35865  419 
 NONE => case strip_prefix tvar_prefix a of 
32956  420 
SOME _ => NONE (*type instantiations are forbidden!*) 
421 
 NONE => SOME (a,t) (*internal Metis var?*) 

422 
val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) 

423 
val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst) 

424 
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

425 
val tms = rawtms > map (reveal_skolem_terms skolems) > infer_types ctxt 
32956  426 
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) 
427 
val substs' = ListPair.zip (vars, map ctm_of tms) 

428 
val _ = trace_msg (fn () => 

429 
cat_lines ("subst_translations:" :: 

430 
(substs' > map (fn (x, y) => 

431 
Syntax.string_of_term ctxt (term_of x) ^ " > " ^ 

432 
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

433 
in cterm_instantiate substs' i_th end 
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

434 
handle THM (msg, _, _) => raise METIS ("inst_inf", msg) 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

435 
 ERROR msg => raise METIS ("inst_inf", msg) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

436 

32956  437 
(* INFERENCE RULE: RESOLVE *) 
25713  438 

32956  439 
(*Like RSN, but we rename apart only the type variables. Vars here typically have an index 
440 
of 1, and the use of RSN would increase this typically to 3. Instantiations of those Vars 

441 
could then fail. See comment on mk_var.*) 

442 
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

443 
let 
6a7a9261b9ad
make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"
blanchet
parents:
37538
diff
changeset

444 
val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha 
32956  445 
val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb) 
446 
in 

447 
case distinct Thm.eq_thm ths of 

448 
[th] => th 

449 
 _ => 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

450 
end 
6a7a9261b9ad
make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"
blanchet
parents:
37538
diff
changeset

451 
handle TERM (msg, _) => raise METIS ("resolve_inc_tyvars", msg) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

452 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

453 
fun resolve_inf ctxt mode skolems thpairs atm th1 th2 = 
32956  454 
let 
455 
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 

456 
val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) 

457 
val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) 

458 
in 

459 
if is_TrueI i_th1 then i_th2 (*Trivial cases where one operand is type info*) 

460 
else if is_TrueI i_th2 then i_th1 

461 
else 

462 
let 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

463 
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

464 
(Metis.Term.Fn atm) 
32956  465 
val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) 
466 
val prems_th1 = prems_of i_th1 

467 
val prems_th2 = prems_of i_th2 

468 
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

469 
handle Empty => raise Fail "Failed to find literal in th1" 
32956  470 
val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) 
471 
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

472 
handle Empty => raise Fail "Failed to find literal in th2" 
32956  473 
val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) 
474 
in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end 

475 
end; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

476 

32956  477 
(* INFERENCE RULE: REFL *) 
478 
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); 

479 
val refl_idx = 1 + Thm.maxidx_of REFL_THM; 

25713  480 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

481 
fun refl_inf ctxt mode skolems t = 
32956  482 
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

483 
val i_t = singleton (hol_terms_from_fol ctxt mode skolems) t 
32956  484 
val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) 
485 
val c_t = cterm_incr_types thy refl_idx i_t 

486 
in cterm_instantiate [(refl_x, c_t)] REFL_THM end; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

487 

35865  488 
fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0 (*equality has no type arguments*) 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36556
diff
changeset

489 
 get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0) 
32994  490 
 get_ty_arg_size _ _ = 0; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

491 

32956  492 
(* INFERENCE RULE: EQUALITY *) 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

493 
fun equality_inf ctxt mode skolems (pos, atm) fp fr = 
32956  494 
let val thy = ProofContext.theory_of ctxt 
495 
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

496 
val [i_atm,i_tm] = hol_terms_from_fol ctxt mode skolems [m_tm, fr] 
32956  497 
val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) 
32994  498 
fun replace_item_list lx 0 (_::ls) = lx::ls 
32956  499 
 replace_item_list lx i (l::ls) = l :: replace_item_list lx (i1) ls 
500 
fun path_finder_FO tm [] = (tm, Term.Bound 0) 

501 
 path_finder_FO tm (p::ps) = 

35865  502 
let val (tm1,args) = strip_comb tm 
32956  503 
val adjustment = get_ty_arg_size thy tm1 
504 
val p' = if adjustment > p then p else padjustment 

505 
val tm_p = List.nth(args,p') 

37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

506 
handle Subscript => raise METIS ("equality_inf", Int.toString p ^ " adj " ^ 
32956  507 
Int.toString adjustment ^ " term " ^ Syntax.string_of_term ctxt tm) 
508 
val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ 

509 
" " ^ Syntax.string_of_term ctxt tm_p) 

510 
val (r,t) = path_finder_FO tm_p ps 

511 
in 

512 
(r, list_comb (tm1, replace_item_list t p' args)) 

513 
end 

514 
fun path_finder_HO tm [] = (tm, Term.Bound 0) 

515 
 path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) 

32994  516 
 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

517 
 path_finder_HO tm ps = 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

518 
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

519 
space_implode " " (map Int.toString ps) ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

520 
" isaterm: " ^ Syntax.string_of_term ctxt tm) 
32956  521 
fun path_finder_FT tm [] _ = (tm, Term.Bound 0) 
32994  522 
 path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) = 
32956  523 
path_finder_FT tm ps t1 
32994  524 
 path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1, _])) = 
32956  525 
(fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) 
32994  526 
 path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) = 
32956  527 
(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

528 
 path_finder_FT tm ps t = 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

529 
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

530 
space_implode " " (map Int.toString ps) ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

531 
" isaterm: " ^ Syntax.string_of_term ctxt tm ^ 
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

532 
" folterm: " ^ Metis.Term.toString t) 
32956  533 
fun path_finder FO tm ps _ = path_finder_FO tm ps 
35865  534 
 path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ = 
32956  535 
(*equality: not curried, as other predicates are*) 
536 
if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) 

537 
else path_finder_HO tm (p::ps) (*1 selects second operand*) 

32994  538 
 path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) = 
32956  539 
path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) 
35865  540 
 path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps) 
32956  541 
(Metis.Term.Fn ("=", [t1,t2])) = 
542 
(*equality: not curried, as other predicates are*) 

543 
if p=0 then path_finder_FT tm (0::1::ps) 

544 
(Metis.Term.Fn (".", [Metis.Term.Fn (".", [metis_eq,t1]), t2])) 

545 
(*select first operand*) 

546 
else path_finder_FT tm (p::ps) 

547 
(Metis.Term.Fn (".", [metis_eq,t2])) 

548 
(*1 selects second operand*) 

32994  549 
 path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 
32956  550 
(*if not equality, ignore head to skip the hBOOL predicate*) 
551 
 path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) 

35865  552 
fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx = 
32956  553 
let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm 
554 
in (tm, nt $ tm_rslt) end 

555 
 path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm 

556 
val (tm_subst, body) = path_finder_lit i_atm fp 

557 
val tm_abs = Term.Abs("x", Term.type_of tm_subst, body) 

558 
val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) 

559 
val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) 

560 
val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) 

561 
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) 

36945  562 
val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) 
32956  563 
val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') 
564 
val eq_terms = map (pairself (cterm_of thy)) 

33227  565 
(ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) 
32956  566 
in cterm_instantiate eq_terms subst' end; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

567 

32956  568 
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

569 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

570 
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

571 
case p of 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

572 
(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

573 
 (_, 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

574 
 (_, 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

575 
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

576 
 (_, 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

577 
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

578 
 (_, 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

579 
 (_, 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

580 
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

581 

35865  582 
fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

583 

37402
12cb33916e37
"raise Fail" for internal errors + one new internal error (instead of "Match")
blanchet
parents:
37399
diff
changeset

584 
(* FIXME: use "fold" instead *) 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

585 
fun translate _ _ _ thpairs [] = thpairs 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

586 
 translate ctxt mode skolems thpairs ((fol_th, inf) :: infpairs) = 
32956  587 
let val _ = trace_msg (fn () => "=============================================") 
588 
val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th) 

589 
val _ = trace_msg (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf) 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

590 
val th = Meson.flexflex_first_order (step ctxt mode skolems 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

591 
thpairs (fol_th, inf)) 
32956  592 
val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) 
593 
val _ = trace_msg (fn () => "=============================================") 

32994  594 
val n_metis_lits = 
595 
length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th))) 

32956  596 
in 
597 
if nprems_of th = n_metis_lits 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

598 
else raise METIS ("translate", "Proof reconstruction has gone wrong."); 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

599 
translate ctxt mode skolems ((fol_th, th) :: thpairs) infpairs 
32956  600 
end; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

601 

32956  602 
(*Determining which axiom clauses are actually used*) 
603 
fun used_axioms axioms (th, Metis.Proof.Axiom _) = SOME (lookth axioms th) 

32994  604 
 used_axioms _ _ = NONE; 
24855  605 

32956  606 
(*  *) 
607 
(* Translation of HO Clauses *) 

608 
(*  *) 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

609 

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

610 
fun cnf_helper_theorem thy raw th = 
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

611 
if raw then th else the_single (cnf_axiom thy th) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

612 

32956  613 
fun type_ext thy tms = 
35865  614 
let val subs = tfree_classes_of_terms tms 
615 
val supers = tvar_classes_of_terms tms 

616 
and tycons = type_consts_of_terms thy tms 

617 
val (supers', arity_clauses) = make_arity_clauses thy tycons supers 

618 
val classrel_clauses = make_classrel_clauses thy subs supers' 

32956  619 
in map classrel_cls classrel_clauses @ map arity_cls arity_clauses 
620 
end; 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

621 

32956  622 
(*  *) 
623 
(* Logic maps manage the interface between HOL and firstorder logic. *) 

624 
(*  *) 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

625 

32956  626 
type logic_map = 
35865  627 
{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

628 
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

629 
skolems: (string * term) list} 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

630 

32994  631 
fun const_in_metis c (pred, tm_list) = 
32956  632 
let 
32994  633 
fun in_mterm (Metis.Term.Var _) = false 
32956  634 
 in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list 
635 
 in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list 

32994  636 
in c = pred orelse exists in_mterm tm_list end; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

637 

32956  638 
(*Extract TFree constraints from context to include as conjecture clauses*) 
639 
fun init_tfrees ctxt = 

36966
adc11fb3f3aa
generate proper arity declarations for TFrees for SPASS's DFG format;
blanchet
parents:
36945
diff
changeset

640 
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

641 
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

642 
> 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

643 
end; 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

644 

32956  645 
(*transform isabelle type / arity clause to metis clause *) 
646 
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

647 
 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

648 
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

649 
skolems = skolems} 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

650 

32956  651 
(*Insert nonlogical 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

652 
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

653 
{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

654 
axioms, 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

655 
tfrees = tfrees, skolems = skolems} 
25713  656 

32956  657 
fun string_of_mode FO = "FO" 
658 
 string_of_mode HO = "HO" 

659 
 string_of_mode FT = "FT" 

32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

660 

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

661 
val helpers = 
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

662 
[("c_COMBI", (false, @{thms COMBI_def})), 
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

663 
("c_COMBK", (false, @{thms COMBK_def})), 
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 
("c_COMBB", (false, @{thms COMBB_def})), 
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

665 
("c_COMBC", (false, @{thms COMBC_def})), 
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

666 
("c_COMBS", (false, @{thms COMBS_def})), 
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

667 
("c_fequal", (false, @{thms fequal_imp_equal equal_imp_fequal})), 
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

668 
("c_True", (true, @{thms True_or_False})), 
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

669 
("c_False", (true, @{thms True_or_False})), 
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

670 
("c_If", (true, @{thms if_True if_False True_or_False}))] 
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

671 

37623
295f3a9b44b6
move functions not needed by Metis out of "Metis_Clauses"
blanchet
parents:
37619
diff
changeset

672 
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

673 
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

674 

32956  675 
(* Function to generate metis clauses, including comb and type clauses *) 
676 
fun build_map mode0 ctxt cls ths = 

677 
let val thy = ProofContext.theory_of ctxt 

678 
(*The modes FO and FT are sticky. HO can be downgraded to FO.*) 

679 
fun set_mode FO = FO 

37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

680 
 set_mode HO = 
37623
295f3a9b44b6
move functions not needed by Metis out of "Metis_Clauses"
blanchet
parents:
37619
diff
changeset

681 
if forall (is_quasi_fol_clause thy) (cls @ ths) then FO else HO 
32956  682 
 set_mode FT = FT 
683 
val mode = set_mode mode0 

684 
(*transform isabelle clause to metis clause *) 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

685 
fun add_thm is_conjecture ith {axioms, tfrees, skolems} : logic_map = 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37318
diff
changeset

686 
let 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

687 
val (mth, tfree_lits, skolems) = 
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

688 
hol_thm_to_fol is_conjecture ctxt mode (length axioms) skolems ith 
32956  689 
in 
690 
{axioms = (mth, Meson.make_meta_clause ith) :: axioms, 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

691 
tfrees = union (op =) tfree_lits tfrees, skolems = skolems} 
32956  692 
end; 
37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

693 
val lmap = {axioms = [], tfrees = init_tfrees ctxt, skolems = []} 
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

694 
> fold (add_thm true) cls 
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

695 
> add_tfrees 
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

696 
> fold (add_thm false) ths 
32956  697 
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

698 
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

699 
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

700 
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

701 
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

702 
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

703 
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

704 
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

705 
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

706 
helpers > filter (is_used o fst) 
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

707 
> maps (fn (_, (raw, thms)) => 
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 
if mode = FT orelse not raw 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

709 
map (cnf_helper_theorem @{theory} raw) thms 
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

710 
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

711 
[]) 
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

712 
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

713 
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

714 

32956  715 
fun refute cls = 
716 
Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls); 

23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

717 

32956  718 
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

719 

32956  720 
fun common_thm ths1 ths2 = exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2); 
24855  721 

37573  722 

37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

723 
(* Main function to start Metis proof and reconstruction *) 
32956  724 
fun FOL_SOLVE mode ctxt cls ths0 = 
725 
let val thy = ProofContext.theory_of ctxt 

35826  726 
val th_cls_pairs = 
35865  727 
map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0 
32956  728 
val ths = maps #2 th_cls_pairs 
729 
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") 

730 
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls 

731 
val _ = trace_msg (fn () => "THEOREM CLAUSES") 

732 
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

733 
val (mode, {axioms, tfrees, skolems}) = build_map mode ctxt cls ths 
32956  734 
val _ = if null tfrees then () 
735 
else (trace_msg (fn () => "TFREE CLAUSES"); 

37573  736 
app (fn TyLitFree (s, (s', _)) => 
737 
trace_msg (fn _ => s ^ "(" ^ s' ^ ")")) tfrees) 

32956  738 
val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") 
739 
val thms = map #1 axioms 

740 
val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms 

741 
val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode) 

742 
val _ = trace_msg (fn () => "START METIS PROVE PROCESS") 

743 
in 

33317  744 
case filter (is_false o prop_of) cls of 
32956  745 
false_th::_ => [false_th RS @{thm FalseE}] 
746 
 [] => 

747 
case refute thms of 

748 
Metis.Resolution.Contradiction mth => 

749 
let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^ 

750 
Metis.Thm.toString mth) 

751 
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt 

752 
(*add constraints arising from converting goal to clause form*) 

753 
val proof = Metis.Proof.proof mth 

37625
35eeb95c5bee
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
blanchet
parents:
37623
diff
changeset

754 
val result = translate ctxt' mode skolems axioms proof 
32956  755 
and used = map_filter (used_axioms axioms) proof 
756 
val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:") 

757 
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used 

33305  758 
val unused = th_cls_pairs > map_filter (fn (name, cls) => 
759 
if common_thm used cls then NONE else SOME name) 

32956  760 
in 
36383  761 
if not (null cls) andalso not (common_thm used cls) then 
762 
warning "Metis: The assumptions are inconsistent." 

763 
else 

764 
(); 

765 
if not (null unused) then 

36230
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

766 
warning ("Metis: Unused theorems: " ^ commas_quote unused 
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

767 
^ ".") 
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

768 
else 
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

769 
(); 
32956  770 
case result of 
771 
(_,ith)::_ => 

36230
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

772 
(trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith); 
32956  773 
[ith]) 
36230
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset

774 
 _ => (trace_msg (fn () => "Metis: No result"); 
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

775 
raise METIS ("FOL_SOLVE", "")) 
32956  776 
end 
777 
 Metis.Resolution.Satisfiable _ => 

778 
(trace_msg (fn () => "Metis: No firstorder proof with the lemmas supplied"); 

37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

779 
raise METIS ("FOL_SOLVE", "")) 
32956  780 
end; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

781 

37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

782 
fun generic_metis_tac mode ctxt ths i st0 = 
32956  783 
let val _ = trace_msg (fn () => 
784 
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) 

785 
in 

37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

786 
if exists_type type_has_topsort (prop_of st0) then 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

787 
(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

788 
else 
36401
31252c4d4923
adapt code to reflect new signature of "neg_clausify"
blanchet
parents:
36383
diff
changeset

789 
(Meson.MESON (maps neg_clausify) 
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

790 
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) 
37619  791 
ctxt i) st0 
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

792 
handle ERROR msg => raise METIS ("generic_metis_tac", msg) 
32956  793 
end 
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

794 
handle METIS (loc, msg) => 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

795 
if mode = HO then 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

796 
(warning ("Metis: Falling back on \"metisFT\"."); 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

797 
generic_metis_tac FT ctxt ths i st0) 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

798 
else if msg = "" then 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

799 
Seq.empty 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

800 
else 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

801 
raise error ("Metis (" ^ loc ^ "): " ^ msg) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

802 

37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

803 
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

804 
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

805 
val metisFT_tac = generic_metis_tac FT 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

806 

37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

807 
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

808 
Method.setup name (Attrib.thms >> (fn ths => fn ctxt => 
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset

809 
SIMPLE_METHOD' (CHANGED_PROP o generic_metis_tac mode ctxt ths))) 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

810 

32956  811 
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

812 
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

813 
#> 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

814 
#> 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

815 
#> 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

816 
"Metis for FOL/HOL problems with fullytyped translation" 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

817 

028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

818 
end; 