author  wenzelm 
Sun, 18 Oct 2009 20:53:40 +0200  
changeset 32994  ccc07fbbfefd 
parent 32956  c39860141415 
child 33035  15eab423e573 
child 33037  b22e44496dc2 
permissions  rwrr 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

1 
(* Title: HOL/Tools/metis_tools.ML 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

3 
Copyright Cambridge University 2007 
23447  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 

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

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

9 
sig 
32955  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 

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

18 
structure MetisTools: METIS_TOOLS = 
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

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

20 

32956  21 
val trace = Unsynchronized.ref false; 
22 
fun trace_msg msg = if ! trace then tracing (msg ()) else (); 

32955  23 

32956  24 
structure Recon = ResReconstruct; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

25 

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

27 

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

29 

32956  30 
(*  *) 
31 
(* Useful Theorems *) 

32 
(*  *) 

33 
val EXCLUDED_MIDDLE = rotate_prems 1 (read_instantiate @{context} [(("R", 0), "False")] notE); 

34 
val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl); (*Rename from 0,1*) 

35 
val subst_em = zero_var_indexes (subst RS EXCLUDED_MIDDLE); 

36 
val ssubst_em = read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em); 

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

37 

32956  38 
(*  *) 
39 
(* Useful Functions *) 

40 
(*  *) 

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

41 

32956  42 
(* match untyped terms*) 
43 
fun untyped_aconv (Const(a,_)) (Const(b,_)) = (a=b) 

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

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

46 
 untyped_aconv (Bound i) (Bound j) = (i=j) 

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

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

49 
 untyped_aconv _ _ = false; 

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

50 

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

53 
let val lit = Envir.eta_contract lit 

54 
fun get n [] = raise Empty 

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

56 
then n else get (n+1) xs 

57 
in get 1 end; 

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

58 

32956  59 
(*  *) 
60 
(* HOL to FOL (Isabelle to Metis) *) 

61 
(*  *) 

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

62 

32956  63 
fun fn_isa_to_met "equal" = "=" 
64 
 fn_isa_to_met x = x; 

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

65 

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

67 

32956  68 
fun hol_type_to_fol (ResClause.AtomV x) = Metis.Term.Var x 
69 
 hol_type_to_fol (ResClause.AtomF x) = Metis.Term.Fn(x,[]) 

70 
 hol_type_to_fol (ResClause.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps); 

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

71 

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

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

74 

32956  75 
fun hol_term_to_fol_FO tm = 
76 
case ResHolClause.strip_comb tm of 

77 
(ResHolClause.CombConst(c,_,tys), tms) => 

78 
let val tyargs = map hol_type_to_fol tys 

79 
val args = map hol_term_to_fol_FO tms 

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

81 
 (ResHolClause.CombVar(v,_), []) => Metis.Term.Var v 

82 
 _ => error "hol_term_to_fol_FO"; 

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

83 

32994  84 
fun hol_term_to_fol_HO (ResHolClause.CombVar (a, _)) = Metis.Term.Var a 
85 
 hol_term_to_fol_HO (ResHolClause.CombConst (a, _, tylist)) = 

86 
Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist) 

87 
 hol_term_to_fol_HO (ResHolClause.CombApp (tm1, tm2)) = 

88 
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

89 

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

92 

93 
fun hol_term_to_fol_FT (ResHolClause.CombVar(a, ty)) = 

94 
wrap_type (Metis.Term.Var a, ty) 

95 
 hol_term_to_fol_FT (ResHolClause.CombConst(a, ty, _)) = 

96 
wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty) 

97 
 hol_term_to_fol_FT (tm as ResHolClause.CombApp(tm1,tm2)) = 

98 
wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]), 

99 
ResHolClause.type_of_combterm tm); 

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

100 

32956  101 
fun hol_literal_to_fol FO (ResHolClause.Literal (pol, tm)) = 
102 
let val (ResHolClause.CombConst(p,_,tys), tms) = ResHolClause.strip_comb tm 

103 
val tylits = if p = "equal" then [] else map hol_type_to_fol tys 

104 
val lits = map hol_term_to_fol_FO tms 

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

106 
 hol_literal_to_fol HO (ResHolClause.Literal (pol, tm)) = 

107 
(case ResHolClause.strip_comb tm of 

108 
(ResHolClause.CombConst("equal",_,_), tms) => 

109 
metis_lit pol "=" (map hol_term_to_fol_HO tms) 

110 
 _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*) 

111 
 hol_literal_to_fol FT (ResHolClause.Literal (pol, tm)) = 

112 
(case ResHolClause.strip_comb tm of 

113 
(ResHolClause.CombConst("equal",_,_), tms) => 

114 
metis_lit pol "=" (map hol_term_to_fol_FT tms) 

115 
 _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*); 

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

116 

32956  117 
fun literals_of_hol_thm thy mode t = 
118 
let val (lits, types_sorts) = ResHolClause.literals_of_term thy t 

119 
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

120 

32956  121 
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) 
122 
fun metis_of_typeLit pos (ResClause.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x] 

123 
 metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])]; 

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

124 

32994  125 
fun default_sort _ (TVar _) = false 
126 
 default_sort ctxt (TFree (x, s)) = (s = Option.getOpt (Variable.def_sort ctxt (x, ~1), [])); 

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

127 

32956  128 
fun metis_of_tfree tf = 
129 
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

130 

32956  131 
fun hol_thm_to_fol is_conjecture ctxt mode th = 
132 
let val thy = ProofContext.theory_of ctxt 

133 
val (mlits, types_sorts) = 

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

135 
in 

136 
if is_conjecture then 

137 
(Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), ResClause.add_typs types_sorts) 

138 
else 

139 
let val tylits = ResClause.add_typs 

140 
(filter (not o default_sort ctxt) types_sorts) 

141 
val mtylits = if Config.get ctxt type_lits 

142 
then map (metis_of_typeLit false) tylits else [] 

143 
in 

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

145 
end 

146 
end; 

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

147 

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

149 

32956  150 
fun m_arity_cls (ResClause.TConsLit (c,t,args)) = 
151 
metis_lit true (ResClause.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)] 

152 
 m_arity_cls (ResClause.TVarLit (c,str)) = 

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

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

154 

32956  155 
(*TrueI is returned as the Isabelle counterpart because there isn't any.*) 
156 
fun arity_cls (ResClause.ArityClause{conclLit,premLits,...}) = 

157 
(TrueI, 

158 
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

159 

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

161 

32956  162 
fun m_classrel_cls subclass superclass = 
163 
[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

164 

32994  165 
fun classrel_cls (ResClause.ClassrelClause {subclass, superclass, ...}) = 
32956  166 
(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

167 

32956  168 
(*  *) 
169 
(* FOL to HOL (Metis to Isabelle) *) 

170 
(*  *) 

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

171 

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

173 

32956  174 
fun terms_of [] = [] 
175 
 terms_of (Term t :: tts) = t :: terms_of tts 

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

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

177 

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

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

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

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

186 

32956  187 
fun apply_list rator nargs rands = 
188 
let val trands = terms_of rands 

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

190 
else error 

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

192 
" expected " ^ Int.toString nargs ^ 

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

194 
end; 

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

195 

24500  196 
fun infer_types ctxt = 
197 
Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); 

25713  198 

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

201 
SEE ALSO axiom_inf below.*) 

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

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

203 

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

206 
let val ww = "'" ^ w 

207 
in TFree(ww, getOpt (Variable.def_sort ctxt (ww,~1), HOLogic.typeS)) end; 

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

208 

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

211 
 strip_happ args x = (x, args); 

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

212 

32994  213 
fun fol_type_to_isa _ (Metis.Term.Var v) = 
32956  214 
(case Recon.strip_prefix ResClause.tvar_prefix v of 
215 
SOME w => Recon.make_tvar w 

216 
 NONE => Recon.make_tvar v) 

217 
 fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) = 

218 
(case Recon.strip_prefix ResClause.tconst_prefix x of 

219 
SOME tc => Term.Type (Recon.invert_type_const tc, map (fol_type_to_isa ctxt) tys) 

220 
 NONE => 

221 
case Recon.strip_prefix ResClause.tfree_prefix x of 

222 
SOME tf => mk_tfree ctxt tf 

223 
 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

224 

32956  225 
(*Maps metis terms to isabelle terms*) 
226 
fun fol_term_to_hol_RAW ctxt fol_tm = 

227 
let val thy = ProofContext.theory_of ctxt 

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

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

230 
(case Recon.strip_prefix ResClause.tvar_prefix v of 

231 
SOME w => Type (Recon.make_tvar w) 

232 
 NONE => 

233 
case Recon.strip_prefix ResClause.schematic_var_prefix v of 

234 
SOME w => Term (mk_var (w, HOLogic.typeT)) 

235 
 NONE => Term (mk_var (v, HOLogic.typeT)) ) 

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

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

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

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

240 
in case rator of 

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

242 
 _ => case tm_to_tt rator of 

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

244 
 _ => error "tm_to_tt: HO application" 

245 
end 

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

247 
and applic_to_tt ("=",ts) = 

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

249 
 applic_to_tt (a,ts) = 

250 
case Recon.strip_prefix ResClause.const_prefix a of 

251 
SOME b => 

252 
let val c = Recon.invert_const b 

253 
val ntypes = Recon.num_typargs thy c 

254 
val nterms = length ts  ntypes 

255 
val tts = map tm_to_tt ts 

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

257 
val ntyargs = Recon.num_typargs thy c 

258 
in if length tys = ntyargs then 

259 
apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes)) 

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

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

262 
" type arguments\n" ^ 

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

264 
" the terms are \n" ^ 

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

266 
end 

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

268 
case Recon.strip_prefix ResClause.tconst_prefix a of 

269 
SOME b => Type (Term.Type(Recon.invert_type_const b, types_of (map tm_to_tt ts))) 

270 
 NONE => (*Maybe a TFree. Should then check that ts=[].*) 

271 
case Recon.strip_prefix ResClause.tfree_prefix a of 

272 
SOME b => Type (mk_tfree ctxt b) 

273 
 NONE => (*a fixed variable? They are Skolem functions.*) 

274 
case Recon.strip_prefix ResClause.fixed_var_prefix a of 

275 
SOME b => 

276 
let val opr = Term.Free(b, HOLogic.typeT) 

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

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

279 
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

280 

32956  281 
(*Maps fullytyped metis terms to isabelle terms*) 
282 
fun fol_term_to_hol_FT ctxt fol_tm = 

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

32994  284 
fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) = 
32956  285 
(case Recon.strip_prefix ResClause.schematic_var_prefix v of 
286 
SOME w => mk_var(w, dummyT) 

287 
 NONE => mk_var(v, dummyT)) 

32994  288 
 cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) = 
32956  289 
Const ("op =", HOLogic.typeT) 
290 
 cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) = 

291 
(case Recon.strip_prefix ResClause.const_prefix x of 

292 
SOME c => Const (Recon.invert_const c, dummyT) 

293 
 NONE => (*Not a constant. Is it a fixed variable??*) 

294 
case Recon.strip_prefix ResClause.fixed_var_prefix x of 

295 
SOME v => Free (v, fol_type_to_isa ctxt ty) 

296 
 NONE => error ("fol_term_to_hol_FT bad constant: " ^ x)) 

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

298 
cvt tm1 $ cvt tm2 

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

300 
cvt tm1 $ cvt tm2 

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

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

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

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

305 
(case Recon.strip_prefix ResClause.const_prefix x of 

306 
SOME c => Const (Recon.invert_const c, dummyT) 

307 
 NONE => (*Not a constant. Is it a fixed variable??*) 

308 
case Recon.strip_prefix ResClause.fixed_var_prefix x of 

309 
SOME v => Free (v, dummyT) 

310 
 NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x); fol_term_to_hol_RAW ctxt t)) 

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

312 
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

313 

32956  314 
fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt 
315 
 fol_term_to_hol ctxt HO = fol_term_to_hol_RAW ctxt 

316 
 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

317 

32956  318 
fun fol_terms_to_hol ctxt mode fol_tms = 
319 
let val ts = map (fol_term_to_hol ctxt mode) fol_tms 

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

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

322 
val ts' = infer_types ctxt ts; 

323 
val _ = app (fn t => trace_msg 

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

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

326 
ts' 

327 
in ts' end; 

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

328 

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

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

331 

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

333 

32956  334 
(*  *) 
335 
(* FOL step Inference Rules *) 

336 
(*  *) 

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

337 

32956  338 
(*for debugging only*) 
339 
fun print_thpair (fth,th) = 

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

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

342 
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

343 

32956  344 
fun lookth thpairs (fth : Metis.Thm.thm) = 
345 
valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth) 

346 
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

347 

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

349 

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

32956  352 
fun inst_excluded_middle thy i_atm = 
353 
let val th = EXCLUDED_MIDDLE 

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

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

356 
in cterm_instantiate substs th end; 

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

357 

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

361 

32956  362 
(* INFERENCE RULE: ASSUME *) 
363 
fun assume_inf ctxt mode atm = 

364 
inst_excluded_middle 

365 
(ProofContext.theory_of ctxt) 

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

367 

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

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

371 
fun inst_inf ctxt mode thpairs fsubst th = 

372 
let val thy = ProofContext.theory_of ctxt 

373 
val i_th = lookth thpairs th 

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

375 
fun find_var x = valOf (List.find (fn ((a,_),_) => a=x) i_th_vars) 

376 
fun subst_translation (x,y) = 

377 
let val v = find_var x 

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

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

380 
handle Option => 

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

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

383 
NONE) 

384 
fun remove_typeinst (a, t) = 

385 
case Recon.strip_prefix ResClause.schematic_var_prefix a of 

386 
SOME b => SOME (b, t) 

387 
 NONE => case Recon.strip_prefix ResClause.tvar_prefix a of 

388 
SOME _ => NONE (*type instantiations are forbidden!*) 

389 
 NONE => SOME (a,t) (*internal Metis var?*) 

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

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

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

393 
val tms = infer_types ctxt rawtms; 

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

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

396 
val _ = trace_msg (fn () => 

397 
cat_lines ("subst_translations:" :: 

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

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

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

401 
in cterm_instantiate substs' i_th 

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

403 
end; 

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

404 

32956  405 
(* INFERENCE RULE: RESOLVE *) 
25713  406 

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

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

410 
fun resolve_inc_tyvars(tha,i,thb) = 

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

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

413 
in 

414 
case distinct Thm.eq_thm ths of 

415 
[th] => th 

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

417 
end; 

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

418 

32956  419 
fun resolve_inf ctxt mode thpairs atm th1 th2 = 
420 
let 

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

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

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

424 
in 

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

426 
else if is_TrueI i_th2 then i_th1 

427 
else 

428 
let 

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

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

431 
val prems_th1 = prems_of i_th1 

432 
val prems_th2 = prems_of i_th2 

433 
val index_th1 = get_index (mk_not i_atm) prems_th1 

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

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

436 
val index_th2 = get_index i_atm prems_th2 

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

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

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

440 
end; 

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

441 

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

444 
val refl_idx = 1 + Thm.maxidx_of REFL_THM; 

25713  445 

32956  446 
fun refl_inf ctxt mode t = 
447 
let val thy = ProofContext.theory_of ctxt 

448 
val i_t = singleton (fol_terms_to_hol ctxt mode) t 

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

450 
val c_t = cterm_incr_types thy refl_idx i_t 

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

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

452 

32994  453 
fun get_ty_arg_size _ (Const ("op =", _)) = 0 (*equality has no type arguments*) 
454 
 get_ty_arg_size thy (Const (c, _)) = (Recon.num_typargs thy c handle TYPE _ => 0) 

455 
 get_ty_arg_size _ _ = 0; 

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

456 

32956  457 
(* INFERENCE RULE: EQUALITY *) 
32994  458 
fun equality_inf ctxt mode (pos, atm) fp fr = 
32956  459 
let val thy = ProofContext.theory_of ctxt 
460 
val m_tm = Metis.Term.Fn atm 

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

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

32994  463 
fun replace_item_list lx 0 (_::ls) = lx::ls 
32956  464 
 replace_item_list lx i (l::ls) = l :: replace_item_list lx (i1) ls 
465 
fun path_finder_FO tm [] = (tm, Term.Bound 0) 

466 
 path_finder_FO tm (p::ps) = 

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

468 
val adjustment = get_ty_arg_size thy tm1 

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

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

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

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

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

474 
" " ^ Syntax.string_of_term ctxt tm_p) 

475 
val (r,t) = path_finder_FO tm_p ps 

476 
in 

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

478 
end 

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

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

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

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

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

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

493 
fun path_finder FO tm ps _ = path_finder_FO tm ps 

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

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

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

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

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

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

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

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

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

505 
(*select first operand*) 

506 
else path_finder_FT tm (p::ps) 

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

508 
(*1 selects second operand*) 

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

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

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

514 
in (tm, nt $ tm_rslt) end 

515 
 path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm 

516 
val (tm_subst, body) = path_finder_lit i_atm fp 

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

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

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

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

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

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

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

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

525 
(ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) 

526 
in cterm_instantiate eq_terms subst' end; 

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

527 

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

529 

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

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

32956  533 
factor (inst_inf ctxt mode thpairs f_subst f_th1) 
32994  534 
 step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) = 
32956  535 
factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2) 
32994  536 
 step ctxt mode _ (_, Metis.Proof.Refl f_tm) = refl_inf ctxt mode f_tm 
537 
 step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) = 

538 
equality_inf ctxt mode f_lit f_p f_r; 

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

539 

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

541 

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

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

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

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

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

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

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

32956  552 
in 
553 
if nprems_of th = n_metis_lits then () 

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

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

556 
end; 

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

557 

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

32994  560 
 used_axioms _ _ = NONE; 
24855  561 

32956  562 
(*  *) 
563 
(* Translation of HO Clauses *) 

564 
(*  *) 

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

565 

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

567 

32956  568 
val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal}; 
569 
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

570 

32956  571 
val comb_I = cnf_th @{theory} ResHolClause.comb_I; 
572 
val comb_K = cnf_th @{theory} ResHolClause.comb_K; 

573 
val comb_B = cnf_th @{theory} ResHolClause.comb_B; 

574 
val comb_C = cnf_th @{theory} ResHolClause.comb_C; 

575 
val comb_S = cnf_th @{theory} ResHolClause.comb_S; 

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

576 

32956  577 
fun type_ext thy tms = 
578 
let val subs = ResAtp.tfree_classes_of_terms tms 

579 
val supers = ResAtp.tvar_classes_of_terms tms 

580 
and tycons = ResAtp.type_consts_of_terms thy tms 

32994  581 
val (supers', arity_clauses) = ResClause.make_arity_clauses thy tycons supers 
32956  582 
val classrel_clauses = ResClause.make_classrel_clauses thy subs supers' 
583 
in map classrel_cls classrel_clauses @ map arity_cls arity_clauses 

584 
end; 

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

585 

32956  586 
(*  *) 
587 
(* Logic maps manage the interface between HOL and firstorder logic. *) 

588 
(*  *) 

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

589 

32956  590 
type logic_map = 
591 
{axioms : (Metis.Thm.thm * Thm.thm) list, 

592 
tfrees : ResClause.type_literal list}; 

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

593 

32994  594 
fun const_in_metis c (pred, tm_list) = 
32956  595 
let 
32994  596 
fun in_mterm (Metis.Term.Var _) = false 
32956  597 
 in_mterm (Metis.Term.Fn (".", tm_list)) = exists in_mterm tm_list 
598 
 in_mterm (Metis.Term.Fn (nm, tm_list)) = c=nm orelse exists in_mterm tm_list 

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

600 

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

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

604 
in ResClause.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

605 

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

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

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

610 
tfrees = tfrees} 

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

611 

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

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

615 
tfrees = tfrees}; 

25713  616 

32956  617 
fun string_of_mode FO = "FO" 
618 
 string_of_mode HO = "HO" 

619 
 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

620 

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

623 
let val thy = ProofContext.theory_of ctxt 

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

625 
fun set_mode FO = FO 

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

627 
 set_mode FT = FT 

628 
val mode = set_mode mode0 

629 
(*transform isabelle clause to metis clause *) 

630 
fun add_thm is_conjecture (ith, {axioms, tfrees}) : logic_map = 

631 
let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith 

632 
in 

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

634 
tfrees = tfree_lits union tfrees} 

635 
end; 

636 
val lmap0 = List.foldl (add_thm true) 

637 
{axioms = [], tfrees = init_tfrees ctxt} cls 

638 
val lmap = List.foldl (add_thm false) (add_tfrees lmap0) ths 

639 
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) 

32994  640 
fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists 
32956  641 
(*Now check for the existence of certain combinators*) 
642 
val thI = if used "c_COMBI" then [comb_I] else [] 

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

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

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

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

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

648 
val lmap' = if mode=FO then lmap 

649 
else List.foldl (add_thm false) lmap (thEQ @ thS @ thC @ thB @ thK @ thI) 

650 
in 

651 
(mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap') 

652 
end; 

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

653 

32956  654 
fun refute cls = 
655 
Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls); 

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

656 

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

658 

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

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

662 

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

665 
let val thy = ProofContext.theory_of ctxt 

666 
val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0 

667 
val ths = maps #2 th_cls_pairs 

668 
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") 

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

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

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

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

673 
val _ = if null tfrees then () 

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

675 
app (fn tf => trace_msg (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees) 

676 
val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") 

677 
val thms = map #1 axioms 

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

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

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

681 
in 

682 
case List.filter (is_false o prop_of) cls of 

683 
false_th::_ => [false_th RS @{thm FalseE}] 

684 
 [] => 

685 
case refute thms of 

686 
Metis.Resolution.Contradiction mth => 

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

688 
Metis.Thm.toString mth) 

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

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

691 
val proof = Metis.Proof.proof mth 

692 
val result = translate mode ctxt' axioms proof 

693 
and used = map_filter (used_axioms axioms) proof 

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

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

32994  696 
val unused = filter (fn (_, cls) => not (common_thm used cls)) th_cls_pairs 
32956  697 
in 
698 
if null unused then () 

699 
else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused)); 

700 
case result of 

701 
(_,ith)::_ => 

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

703 
[ith]) 

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

705 
[]) 

706 
end 

707 
 Metis.Resolution.Satisfiable _ => 

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

709 
[]) 

710 
end; 

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

711 

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

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

715 
in 

716 
if exists_type ResAxioms.type_has_empty_sort (prop_of st0) 

717 
then (warning "Proof state contains the empty sort"; Seq.empty) 

718 
else 

719 
(Meson.MESON ResAxioms.neg_clausify 

720 
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i 

721 
THEN ResAxioms.expand_defs_tac st0) st0 

722 
end 

723 
handle METIS s => (warning ("Metis: " ^ s); Seq.empty); 

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

724 

32956  725 
val metis_tac = metis_general_tac HO; 
726 
val metisF_tac = metis_general_tac FO; 

727 
val metisFT_tac = metis_general_tac FT; 

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

728 

32956  729 
fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt => 
730 
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

731 

32956  732 
val setup = 
733 
type_lits_setup #> 

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

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

736 
method @{binding metisFT} FT "METIS Withfully typed translation" #> 

737 
Method.setup @{binding finish_clausify} 

738 
(Scan.succeed (K (SIMPLE_METHOD (ResAxioms.expand_defs_tac refl)))) 

739 
"cleanup after conversion to clauses"; 

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

740 

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

741 
end; 