author  blanchet 
Wed, 17 Mar 2010 19:26:05 +0100  
changeset 35826  1590abc3d42a 
parent 35825  a6aad5a70ed4 
child 35865  2f8fb5242799 
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 

35826  21 
structure SFC = Sledgehammer_FOL_Clause 
22 
structure SHC = Sledgehammer_HOL_Clause 

23 
structure SPR = Sledgehammer_Proof_Reconstruct 

24 

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

32956  28 
val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

29 

35826  30 
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

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)} 
d0a9ce721e0c
properly inlined @{lemma} antiqutations  might also reduce proof terms a bit;
wenzelm
parents:
33339
diff
changeset

36 
val REFL_THM = incr_indexes 2 @{lemma "t ~= t ==> False" by simp} 
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 

32956  44 
(* match untyped terms*) 
45 
fun untyped_aconv (Const(a,_)) (Const(b,_)) = (a=b) 

46 
 untyped_aconv (Free(a,_)) (Free(b,_)) = (a=b) 

47 
 untyped_aconv (Var((a,_),_)) (Var((b,_),_)) = (a=b) (*the index is ignored!*) 

48 
 untyped_aconv (Bound i) (Bound j) = (i=j) 

49 
 untyped_aconv (Abs(a,_,t)) (Abs(b,_,u)) = (a=b) andalso untyped_aconv t u 

50 
 untyped_aconv (t1$t2) (u1$u2) = untyped_aconv t1 u1 andalso untyped_aconv t2 u2 

51 
 untyped_aconv _ _ = false; 

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

52 

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

55 
let val lit = Envir.eta_contract lit 

56 
fun get n [] = raise Empty 

57 
 get n (x::xs) = if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) 

58 
then n else get (n+1) xs 

59 
in get 1 end; 

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

60 

32956  61 
(*  *) 
62 
(* HOL to FOL (Isabelle to Metis) *) 

63 
(*  *) 

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

64 

32956  65 
fun fn_isa_to_met "equal" = "=" 
66 
 fn_isa_to_met x = x; 

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

67 

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

69 

35826  70 
fun hol_type_to_fol (SFC.AtomV x) = Metis.Term.Var x 
71 
 hol_type_to_fol (SFC.AtomF x) = Metis.Term.Fn(x,[]) 

72 
 hol_type_to_fol (SFC.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps); 

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

73 

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

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

76 

32956  77 
fun hol_term_to_fol_FO tm = 
35826  78 
case SHC.strip_comb tm of 
79 
(SHC.CombConst(c,_,tys), tms) => 

32956  80 
let val tyargs = map hol_type_to_fol tys 
81 
val args = map hol_term_to_fol_FO tms 

82 
in Metis.Term.Fn (c, tyargs @ args) end 

35826  83 
 (SHC.CombVar(v,_), []) => Metis.Term.Var v 
32956  84 
 _ => error "hol_term_to_fol_FO"; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

85 

35826  86 
fun hol_term_to_fol_HO (SHC.CombVar (a, _)) = Metis.Term.Var a 
87 
 hol_term_to_fol_HO (SHC.CombConst (a, _, tylist)) = 

32994  88 
Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist) 
35826  89 
 hol_term_to_fol_HO (SHC.CombApp (tm1, tm2)) = 
32994  90 
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

91 

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

94 

35826  95 
fun hol_term_to_fol_FT (SHC.CombVar(a, ty)) = 
32956  96 
wrap_type (Metis.Term.Var a, ty) 
35826  97 
 hol_term_to_fol_FT (SHC.CombConst(a, ty, _)) = 
32956  98 
wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty) 
35826  99 
 hol_term_to_fol_FT (tm as SHC.CombApp(tm1,tm2)) = 
32956  100 
wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), 
35826  101 
SHC.type_of_combterm tm); 
32532
a0a54a51b15b
My umpteenth attempt to commit the method metisFT, a fullytyped version of metis
paulson
parents:
32530
diff
changeset

102 

35826  103 
fun hol_literal_to_fol FO (SHC.Literal (pol, tm)) = 
104 
let val (SHC.CombConst(p,_,tys), tms) = SHC.strip_comb tm 

32956  105 
val tylits = if p = "equal" then [] else map hol_type_to_fol tys 
106 
val lits = map hol_term_to_fol_FO tms 

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

35826  108 
 hol_literal_to_fol HO (SHC.Literal (pol, tm)) = 
109 
(case SHC.strip_comb tm of 

110 
(SHC.CombConst("equal",_,_), tms) => 

32956  111 
metis_lit pol "=" (map hol_term_to_fol_HO tms) 
112 
 _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) 

35826  113 
 hol_literal_to_fol FT (SHC.Literal (pol, tm)) = 
114 
(case SHC.strip_comb tm of 

115 
(SHC.CombConst("equal",_,_), tms) => 

32956  116 
metis_lit pol "=" (map hol_term_to_fol_FT tms) 
117 
 _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); 

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

118 

32956  119 
fun literals_of_hol_thm thy mode t = 
35826  120 
let val (lits, types_sorts) = SHC.literals_of_term thy t 
32956  121 
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

122 

32956  123 
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) 
35826  124 
fun metis_of_typeLit pos (SFC.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x] 
125 
 metis_of_typeLit pos (SFC.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])]; 

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

126 

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

129 

32956  130 
fun metis_of_tfree tf = 
131 
Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf)); 

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

132 

32956  133 
fun hol_thm_to_fol is_conjecture ctxt mode th = 
134 
let val thy = ProofContext.theory_of ctxt 

135 
val (mlits, types_sorts) = 

136 
(literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th 

137 
in 

138 
if is_conjecture then 

35826  139 
(Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), SFC.add_typs types_sorts) 
32956  140 
else 
35826  141 
let val tylits = SFC.add_typs 
32956  142 
(filter (not o default_sort ctxt) types_sorts) 
143 
val mtylits = if Config.get ctxt type_lits 

144 
then map (metis_of_typeLit false) tylits else [] 

145 
in 

146 
(Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), []) 

147 
end 

148 
end; 

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

149 

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

151 

35826  152 
fun m_arity_cls (SFC.TConsLit (c,t,args)) = 
153 
metis_lit true (SFC.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)] 

154 
 m_arity_cls (SFC.TVarLit (c,str)) = 

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

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

156 

32956  157 
(*TrueI is returned as the Isabelle counterpart because there isn't any.*) 
35826  158 
fun arity_cls (SFC.ArityClause{conclLit,premLits,...}) = 
32956  159 
(TrueI, 
160 
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

161 

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

163 

32956  164 
fun m_classrel_cls subclass superclass = 
165 
[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

166 

35826  167 
fun classrel_cls (SFC.ClassrelClause {subclass, superclass, ...}) = 
32956  168 
(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

169 

32956  170 
(*  *) 
171 
(* FOL to HOL (Metis to Isabelle) *) 

172 
(*  *) 

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

173 

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

175 

32956  176 
fun terms_of [] = [] 
177 
 terms_of (Term t :: tts) = t :: terms_of tts 

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

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

179 

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

32994  184 
TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts 
32956  185 
else types_of tts 
186 
 types_of (Term _ :: tts) = types_of tts 

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

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

188 

32956  189 
fun apply_list rator nargs rands = 
190 
let val trands = terms_of rands 

191 
in if length trands = nargs then Term (list_comb(rator, trands)) 

192 
else error 

193 
("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ 

194 
" expected " ^ Int.toString nargs ^ 

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

196 
end; 

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

197 

24500  198 
fun infer_types ctxt = 
199 
Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); 

25713  200 

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

203 
SEE ALSO axiom_inf below.*) 

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

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

205 

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

208 
let val ww = "'" ^ w 

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

210 

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

213 
 strip_happ args x = (x, args); 

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

214 

32994  215 
fun fol_type_to_isa _ (Metis.Term.Var v) = 
35826  216 
(case SPR.strip_prefix SFC.tvar_prefix v of 
217 
SOME w => SPR.make_tvar w 

218 
 NONE => SPR.make_tvar v) 

32956  219 
 fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) = 
35826  220 
(case SPR.strip_prefix SFC.tconst_prefix x of 
221 
SOME tc => Term.Type (SPR.invert_type_const tc, map (fol_type_to_isa ctxt) tys) 

32956  222 
 NONE => 
35826  223 
case SPR.strip_prefix SFC.tfree_prefix x of 
32956  224 
SOME tf => mk_tfree ctxt tf 
225 
 NONE => error ("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

226 

32956  227 
(*Maps metis terms to isabelle terms*) 
228 
fun fol_term_to_hol_RAW ctxt fol_tm = 

229 
let val thy = ProofContext.theory_of ctxt 

230 
val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm) 

231 
fun tm_to_tt (Metis.Term.Var v) = 

35826  232 
(case SPR.strip_prefix SFC.tvar_prefix v of 
233 
SOME w => Type (SPR.make_tvar w) 

32956  234 
 NONE => 
35826  235 
case SPR.strip_prefix SFC.schematic_var_prefix v of 
32956  236 
SOME w => Term (mk_var (w, HOLogic.typeT)) 
237 
 NONE => Term (mk_var (v, HOLogic.typeT)) ) 

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

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

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

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

242 
in case rator of 

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

244 
 _ => case tm_to_tt rator of 

245 
Term t => Term (list_comb(t, terms_of (map tm_to_tt rands))) 

246 
 _ => error "tm_to_tt: HO application" 

247 
end 

248 
 tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args) 

249 
and applic_to_tt ("=",ts) = 

250 
Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts))) 

251 
 applic_to_tt (a,ts) = 

35826  252 
case SPR.strip_prefix SFC.const_prefix a of 
32956  253 
SOME b => 
35826  254 
let val c = SPR.invert_const b 
255 
val ntypes = SPR.num_typargs thy c 

32956  256 
val nterms = length ts  ntypes 
257 
val tts = map tm_to_tt ts 

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

35826  259 
val ntyargs = SPR.num_typargs thy c 
32956  260 
in if length tys = ntyargs then 
261 
apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) 

262 
else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^ 

263 
" but gets " ^ Int.toString (length tys) ^ 

264 
" type arguments\n" ^ 

265 
cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ 

266 
" the terms are \n" ^ 

267 
cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) 

268 
end 

269 
 NONE => (*Not a constant. Is it a type constructor?*) 

35826  270 
case SPR.strip_prefix SFC.tconst_prefix a of 
33227  271 
SOME b => 
35826  272 
Type (Term.Type (SPR.invert_type_const b, types_of (map tm_to_tt ts))) 
32956  273 
 NONE => (*Maybe a TFree. Should then check that ts=[].*) 
35826  274 
case SPR.strip_prefix SFC.tfree_prefix a of 
32956  275 
SOME b => Type (mk_tfree ctxt b) 
276 
 NONE => (*a fixed variable? They are Skolem functions.*) 

35826  277 
case SPR.strip_prefix SFC.fixed_var_prefix a of 
32956  278 
SOME b => 
279 
let val opr = Term.Free(b, HOLogic.typeT) 

280 
in apply_list opr (length ts) (map tm_to_tt ts) end 

281 
 NONE => error ("unexpected metis function: " ^ a) 

282 
in case tm_to_tt fol_tm of Term t => t  _ => error "fol_tm_to_tt: Term expected" end; 

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

283 

32956  284 
(*Maps fullytyped metis terms to isabelle terms*) 
285 
fun fol_term_to_hol_FT ctxt fol_tm = 

286 
let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm) 

32994  287 
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = 
35826  288 
(case SPR.strip_prefix SFC.schematic_var_prefix v of 
32956  289 
SOME w => mk_var(w, dummyT) 
290 
 NONE => mk_var(v, dummyT)) 

32994  291 
 cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) = 
32956  292 
Const ("op =", HOLogic.typeT) 
293 
 cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = 

35826  294 
(case SPR.strip_prefix SFC.const_prefix x of 
295 
SOME c => Const (SPR.invert_const c, dummyT) 

32956  296 
 NONE => (*Not a constant. Is it a fixed variable??*) 
35826  297 
case SPR.strip_prefix SFC.fixed_var_prefix x of 
32956  298 
SOME v => Free (v, fol_type_to_isa ctxt ty) 
299 
 NONE => error ("fol_term_to_hol_FT bad constant: " ^ x)) 

300 
 cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) = 

301 
cvt tm1 $ cvt tm2 

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

303 
cvt tm1 $ cvt tm2 

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

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

306 
list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2]) 

307 
 cvt (t as Metis.Term.Fn (x, [])) = 

35826  308 
(case SPR.strip_prefix SFC.const_prefix x of 
309 
SOME c => Const (SPR.invert_const c, dummyT) 

32956  310 
 NONE => (*Not a constant. Is it a fixed variable??*) 
35826  311 
case SPR.strip_prefix SFC.fixed_var_prefix x of 
32956  312 
SOME v => Free (v, dummyT) 
33227  313 
 NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x); 
314 
fol_term_to_hol_RAW ctxt t)) 

315 
 cvt t = (trace_msg (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); 

316 
fol_term_to_hol_RAW ctxt t) 

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

318 

32956  319 
fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt 
320 
 fol_term_to_hol ctxt HO = fol_term_to_hol_RAW ctxt 

321 
 fol_term_to_hol ctxt FT = fol_term_to_hol_FT ctxt; 

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

322 

32956  323 
fun fol_terms_to_hol ctxt mode fol_tms = 
324 
let val ts = map (fol_term_to_hol ctxt mode) fol_tms 

325 
val _ = trace_msg (fn () => " calling type inference:") 

326 
val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts 

327 
val ts' = infer_types ctxt ts; 

328 
val _ = app (fn t => trace_msg 

329 
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ 

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

331 
ts' 

332 
in ts' end; 

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

333 

32956  334 
fun mk_not (Const ("Not", _) $ b) = b 
335 
 mk_not b = HOLogic.mk_not b; 

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

336 

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

338 

32956  339 
(*  *) 
340 
(* FOL step Inference Rules *) 

341 
(*  *) 

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

342 

32956  343 
(*for debugging only*) 
344 
fun print_thpair (fth,th) = 

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

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

347 
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

348 

32956  349 
fun lookth thpairs (fth : Metis.Thm.thm) = 
33035  350 
the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth) 
32956  351 
handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

352 

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

354 

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

32956  357 
fun inst_excluded_middle thy i_atm = 
358 
let val th = EXCLUDED_MIDDLE 

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

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

361 
in cterm_instantiate substs th end; 

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

362 

32956  363 
(* INFERENCE RULE: AXIOM *) 
32994  364 
fun axiom_inf thpairs th = incr_indexes 1 (lookth thpairs th); 
32956  365 
(*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

366 

32956  367 
(* INFERENCE RULE: ASSUME *) 
368 
fun assume_inf ctxt mode atm = 

369 
inst_excluded_middle 

370 
(ProofContext.theory_of ctxt) 

371 
(singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)); 

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

372 

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

375 
that new TVars are distinct and that types can be inferred from terms.*) 

376 
fun inst_inf ctxt mode thpairs fsubst th = 

377 
let val thy = ProofContext.theory_of ctxt 

378 
val i_th = lookth thpairs th 

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

33035  380 
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) 
32956  381 
fun subst_translation (x,y) = 
382 
let val v = find_var x 

383 
val t = fol_term_to_hol ctxt mode y (*we call infer_types below*) 

384 
in SOME (cterm_of thy (Var v), t) end 

385 
handle Option => 

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

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

388 
NONE) 

389 
fun remove_typeinst (a, t) = 

35826  390 
case SPR.strip_prefix SFC.schematic_var_prefix a of 
32956  391 
SOME b => SOME (b, t) 
35826  392 
 NONE => case SPR.strip_prefix SFC.tvar_prefix a of 
32956  393 
SOME _ => NONE (*type instantiations are forbidden!*) 
394 
 NONE => SOME (a,t) (*internal Metis var?*) 

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

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

397 
val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) 

398 
val tms = infer_types ctxt rawtms; 

399 
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) 

400 
val substs' = ListPair.zip (vars, map ctm_of tms) 

401 
val _ = trace_msg (fn () => 

402 
cat_lines ("subst_translations:" :: 

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

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

405 
Syntax.string_of_term ctxt (term_of y))))); 

406 
in cterm_instantiate substs' i_th 

407 
handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg) 

408 
end; 

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

409 

32956  410 
(* INFERENCE RULE: RESOLVE *) 
25713  411 

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

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

415 
fun resolve_inc_tyvars(tha,i,thb) = 

416 
let val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha 

417 
val ths = Seq.list_of (Thm.bicompose false (false,tha,nprems_of tha) i thb) 

418 
in 

419 
case distinct Thm.eq_thm ths of 

420 
[th] => th 

421 
 _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb]) 

422 
end; 

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

423 

32956  424 
fun resolve_inf ctxt mode thpairs atm th1 th2 = 
425 
let 

426 
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 

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

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

429 
in 

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

431 
else if is_TrueI i_th2 then i_th1 

432 
else 

433 
let 

434 
val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm) 

435 
val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) 

436 
val prems_th1 = prems_of i_th1 

437 
val prems_th2 = prems_of i_th2 

438 
val index_th1 = get_index (mk_not i_atm) prems_th1 

439 
handle Empty => error "Failed to find literal in th1" 

440 
val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) 

441 
val index_th2 = get_index i_atm prems_th2 

442 
handle Empty => error "Failed to find literal in th2" 

443 
val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) 

444 
in resolve_inc_tyvars (Meson.select_literal index_th1 i_th1, index_th2, i_th2) end 

445 
end; 

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

446 

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

449 
val refl_idx = 1 + Thm.maxidx_of REFL_THM; 

25713  450 

32956  451 
fun refl_inf ctxt mode t = 
452 
let val thy = ProofContext.theory_of ctxt 

453 
val i_t = singleton (fol_terms_to_hol ctxt mode) t 

454 
val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) 

455 
val c_t = cterm_incr_types thy refl_idx i_t 

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

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

457 

32994  458 
fun get_ty_arg_size _ (Const ("op =", _)) = 0 (*equality has no type arguments*) 
35826  459 
 get_ty_arg_size thy (Const (c, _)) = (SPR.num_typargs thy c handle TYPE _ => 0) 
32994  460 
 get_ty_arg_size _ _ = 0; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

461 

32956  462 
(* INFERENCE RULE: EQUALITY *) 
32994  463 
fun equality_inf ctxt mode (pos, atm) fp fr = 
32956  464 
let val thy = ProofContext.theory_of ctxt 
465 
val m_tm = Metis.Term.Fn atm 

466 
val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr] 

467 
val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) 

32994  468 
fun replace_item_list lx 0 (_::ls) = lx::ls 
32956  469 
 replace_item_list lx i (l::ls) = l :: replace_item_list lx (i1) ls 
470 
fun path_finder_FO tm [] = (tm, Term.Bound 0) 

471 
 path_finder_FO tm (p::ps) = 

472 
let val (tm1,args) = Term.strip_comb tm 

473 
val adjustment = get_ty_arg_size thy tm1 

474 
val p' = if adjustment > p then p else padjustment 

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

476 
handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^ 

477 
Int.toString adjustment ^ " term " ^ Syntax.string_of_term ctxt tm) 

478 
val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ 

479 
" " ^ Syntax.string_of_term ctxt tm_p) 

480 
val (r,t) = path_finder_FO tm_p ps 

481 
in 

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

483 
end 

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

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

32994  486 
 path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) 
32956  487 
fun path_finder_FT tm [] _ = (tm, Term.Bound 0) 
32994  488 
 path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1, _])) = 
32956  489 
path_finder_FT tm ps t1 
32994  490 
 path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1, _])) = 
32956  491 
(fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) 
32994  492 
 path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [_, t2])) = 
32956  493 
(fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) 
494 
 path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^ 

495 
space_implode " " (map Int.toString ps) ^ 

496 
" isaterm: " ^ Syntax.string_of_term ctxt tm ^ 

497 
" folterm: " ^ Metis.Term.toString t) 

498 
fun path_finder FO tm ps _ = path_finder_FO tm ps 

499 
 path_finder HO (tm as Const("op =",_) $ _ $ _) (p::ps) _ = 

500 
(*equality: not curried, as other predicates are*) 

501 
if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) 

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

32994  503 
 path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) = 
32956  504 
path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) 
505 
 path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps) 

506 
(Metis.Term.Fn ("=", [t1,t2])) = 

507 
(*equality: not curried, as other predicates are*) 

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

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

510 
(*select first operand*) 

511 
else path_finder_FT tm (p::ps) 

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

513 
(*1 selects second operand*) 

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

517 
fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx = 

518 
let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm 

519 
in (tm, nt $ tm_rslt) end 

520 
 path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm 

521 
val (tm_subst, body) = path_finder_lit i_atm fp 

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

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

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

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

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

527 
val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em) 

528 
val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') 

529 
val eq_terms = map (pairself (cterm_of thy)) 

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

532 

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

534 

32994  535 
fun step _ _ thpairs (fol_th, Metis.Proof.Axiom _) = factor (axiom_inf thpairs fol_th) 
536 
 step ctxt mode _ (_, Metis.Proof.Assume f_atm) = assume_inf ctxt mode f_atm 

537 
 step ctxt mode thpairs (_, Metis.Proof.Subst (f_subst, f_th1)) = 

32956  538 
factor (inst_inf ctxt mode thpairs f_subst f_th1) 
32994  539 
 step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) = 
32956  540 
factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2) 
32994  541 
 step ctxt mode _ (_, Metis.Proof.Refl f_tm) = refl_inf ctxt mode f_tm 
542 
 step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) = 

543 
equality_inf ctxt mode f_lit f_p f_r; 

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

544 

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

546 

32994  547 
fun translate _ _ thpairs [] = thpairs 
32956  548 
 translate mode ctxt thpairs ((fol_th, inf) :: infpairs) = 
549 
let val _ = trace_msg (fn () => "=============================================") 

550 
val _ = trace_msg (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th) 

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

552 
val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf)) 

553 
val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) 

554 
val _ = trace_msg (fn () => "=============================================") 

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

32956  557 
in 
558 
if nprems_of th = n_metis_lits then () 

559 
else error "Metis: proof reconstruction has gone wrong"; 

560 
translate mode ctxt ((fol_th, th) :: thpairs) infpairs 

561 
end; 

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

562 

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

32994  565 
 used_axioms _ _ = NONE; 
24855  566 

32956  567 
(*  *) 
568 
(* Translation of HO Clauses *) 

569 
(*  *) 

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

570 

35826  571 
fun cnf_th thy th = hd (Sledgehammer_Fact_Preprocessor.cnf_axiom thy th); 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

572 

32956  573 
val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal}; 
574 
val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal}; 

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

575 

35826  576 
val comb_I = cnf_th @{theory} SHC.comb_I; 
577 
val comb_K = cnf_th @{theory} SHC.comb_K; 

578 
val comb_B = cnf_th @{theory} SHC.comb_B; 

579 
val comb_C = cnf_th @{theory} SHC.comb_C; 

580 
val comb_S = cnf_th @{theory} SHC.comb_S; 

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

581 

32956  582 
fun type_ext thy tms = 
35826  583 
let val subs = Sledgehammer_Fact_Filter.tfree_classes_of_terms tms 
584 
val supers = Sledgehammer_Fact_Filter.tvar_classes_of_terms tms 

585 
and tycons = Sledgehammer_Fact_Filter.type_consts_of_terms thy tms 

586 
val (supers', arity_clauses) = SFC.make_arity_clauses thy tycons supers 

587 
val classrel_clauses = SFC.make_classrel_clauses thy subs supers' 

32956  588 
in map classrel_cls classrel_clauses @ map arity_cls arity_clauses 
589 
end; 

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

590 

32956  591 
(*  *) 
592 
(* Logic maps manage the interface between HOL and firstorder logic. *) 

593 
(*  *) 

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

594 

32956  595 
type logic_map = 
33243  596 
{axioms : (Metis.Thm.thm * thm) list, 
35826  597 
tfrees : SFC.type_literal list}; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

598 

32994  599 
fun const_in_metis c (pred, tm_list) = 
32956  600 
let 
32994  601 
fun in_mterm (Metis.Term.Var _) = false 
32956  602 
 in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list 
603 
 in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list 

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

605 

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

608 
let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts 

35826  609 
in SFC.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end; 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

610 

32956  611 
(*transform isabelle type / arity clause to metis clause *) 
612 
fun add_type_thm [] lmap = lmap 

613 
 add_type_thm ((ith, mth) :: cls) {axioms, tfrees} = 

614 
add_type_thm cls {axioms = (mth, ith) :: axioms, 

615 
tfrees = tfrees} 

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

616 

32956  617 
(*Insert nonlogical axioms corresponding to all accumulated TFrees*) 
618 
fun add_tfrees {axioms, tfrees} : logic_map = 

619 
{axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms, 

620 
tfrees = tfrees}; 

25713  621 

32956  622 
fun string_of_mode FO = "FO" 
623 
 string_of_mode HO = "HO" 

624 
 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

625 

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

628 
let val thy = ProofContext.theory_of ctxt 

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

630 
fun set_mode FO = FO 

631 
 set_mode HO = if forall (Meson.is_fol_term thy o prop_of) (cls@ths) then FO else HO 

632 
 set_mode FT = FT 

633 
val mode = set_mode mode0 

634 
(*transform isabelle clause to metis clause *) 

33339  635 
fun add_thm is_conjecture ith {axioms, tfrees} : logic_map = 
32956  636 
let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith 
637 
in 

638 
{axioms = (mth, Meson.make_meta_clause ith) :: axioms, 

33042  639 
tfrees = union (op =) tfree_lits tfrees} 
32956  640 
end; 
33339  641 
val lmap0 = fold (add_thm true) cls {axioms = [], tfrees = init_tfrees ctxt} 
642 
val lmap = fold (add_thm false) ths (add_tfrees lmap0) 

32956  643 
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) 
32994  644 
fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists 
32956  645 
(*Now check for the existence of certain combinators*) 
646 
val thI = if used "c_COMBI" then [comb_I] else [] 

647 
val thK = if used "c_COMBK" then [comb_K] else [] 

648 
val thB = if used "c_COMBB" then [comb_B] else [] 

649 
val thC = if used "c_COMBC" then [comb_C] else [] 

650 
val thS = if used "c_COMBS" then [comb_S] else [] 

651 
val thEQ = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else [] 

652 
val lmap' = if mode=FO then lmap 

33339  653 
else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap 
32956  654 
in 
655 
(mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap') 

656 
end; 

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

657 

32956  658 
fun refute cls = 
659 
Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls); 

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

660 

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

662 

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

32956  665 
exception METIS of string; 
28233
f14f34194f63
The metis method now fails in the usual manner, rather than raising an exception,
paulson
parents:
28175
diff
changeset

666 

32956  667 
(* Main function to start metis prove and reconstruction *) 
668 
fun FOL_SOLVE mode ctxt cls ths0 = 

669 
let val thy = ProofContext.theory_of ctxt 

35826  670 
val th_cls_pairs = 
671 
map (fn th => (Thm.get_name_hint th, Sledgehammer_Fact_Preprocessor.cnf_axiom thy th)) ths0 

32956  672 
val ths = maps #2 th_cls_pairs 
673 
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") 

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

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

676 
val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) ths 

677 
val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths 

678 
val _ = if null tfrees then () 

679 
else (trace_msg (fn () => "TFREE CLAUSES"); 

35826  680 
app (fn tf => trace_msg (fn _ => SFC.tptp_of_typeLit true tf)) tfrees) 
32956  681 
val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") 
682 
val thms = map #1 axioms 

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

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

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

686 
in 

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

690 
case refute thms of 

691 
Metis.Resolution.Contradiction mth => 

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

693 
Metis.Thm.toString mth) 

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

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

696 
val proof = Metis.Proof.proof mth 

697 
val result = translate mode ctxt' axioms proof 

698 
and used = map_filter (used_axioms axioms) proof 

699 
val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:") 

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

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

32956  703 
in 
704 
if null unused then () 

33305  705 
else warning ("Metis: unused theorems " ^ commas_quote unused); 
32956  706 
case result of 
707 
(_,ith)::_ => 

708 
(trace_msg (fn () => "success: " ^ Display.string_of_thm ctxt ith); 

709 
[ith]) 

710 
 _ => (trace_msg (fn () => "Metis: no result"); 

711 
[]) 

712 
end 

713 
 Metis.Resolution.Satisfiable _ => 

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

715 
[]) 

716 
end; 

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

717 

32956  718 
fun metis_general_tac mode ctxt ths i st0 = 
719 
let val _ = trace_msg (fn () => 

720 
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths)) 

721 
in 

35826  722 
if exists_type Sledgehammer_Fact_Preprocessor.type_has_topsort (prop_of st0) 
35568
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort  {} is the full universal sort;
wenzelm
parents:
34087
diff
changeset

723 
then raise METIS "Metis: Proof state contains the universal sort {}" 
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort  {} is the full universal sort;
wenzelm
parents:
34087
diff
changeset

724 
else 
35826  725 
(Meson.MESON Sledgehammer_Fact_Preprocessor.neg_clausify 
35568
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort  {} is the full universal sort;
wenzelm
parents:
34087
diff
changeset

726 
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i 
35826  727 
THEN Sledgehammer_Fact_Preprocessor.expand_defs_tac st0) st0 
32956  728 
end 
729 
handle METIS s => (warning ("Metis: " ^ s); Seq.empty); 

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

730 

32956  731 
val metis_tac = metis_general_tac HO; 
732 
val metisF_tac = metis_general_tac FO; 

733 
val metisFT_tac = metis_general_tac FT; 

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

734 

32956  735 
fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt => 
736 
SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment; 

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

737 

32956  738 
val setup = 
739 
type_lits_setup #> 

740 
method @{binding metis} HO "METIS for FOL & HOL problems" #> 

741 
method @{binding metisF} FO "METIS for FOL problems" #> 

35568
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort  {} is the full universal sort;
wenzelm
parents:
34087
diff
changeset

742 
method @{binding metisFT} FT "METIS with fullytyped translation" #> 
32956  743 
Method.setup @{binding finish_clausify} 
35826  744 
(Scan.succeed (K (SIMPLE_METHOD (Sledgehammer_Fact_Preprocessor.expand_defs_tac refl)))) 
32956  745 
"cleanup after conversion to clauses"; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

746 

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

747 
end; 