author  blanchet 
Fri, 19 Mar 2010 13:02:18 +0100  
changeset 35865  2f8fb5242799 
parent 35826  1590abc3d42a 
child 36001  992839c4be90 
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 

35865  21 
open Sledgehammer_FOL_Clause 
22 
open Sledgehammer_Fact_Preprocessor 

23 
open Sledgehammer_HOL_Clause 

24 
open Sledgehammer_Proof_Reconstruct 

25 
open Sledgehammer_Fact_Filter 

35826  26 

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

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

31 

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

33 

32956  34 
(*  *) 
35 
(* Useful Theorems *) 

36 
(*  *) 

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

37 
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

38 
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

39 
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

40 
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

41 

32956  42 
(*  *) 
43 
(* Useful Functions *) 

44 
(*  *) 

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

45 

32956  46 
(* match untyped terms*) 
47 
fun untyped_aconv (Const(a,_)) (Const(b,_)) = (a=b) 

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

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

50 
 untyped_aconv (Bound i) (Bound j) = (i=j) 

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

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

53 
 untyped_aconv _ _ = false; 

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

54 

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

57 
let val lit = Envir.eta_contract lit 

58 
fun get n [] = raise Empty 

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

60 
then n else get (n+1) xs 

61 
in get 1 end; 

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

62 

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

65 
(*  *) 

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

66 

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

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

69 

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

71 

35865  72 
fun hol_type_to_fol (AtomV x) = Metis.Term.Var x 
73 
 hol_type_to_fol (AtomF x) = Metis.Term.Fn (x, []) 

74 
 hol_type_to_fol (Comp (tc, tps)) = 

75 
Metis.Term.Fn (tc, map hol_type_to_fol tps); 

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

76 

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

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

79 

32956  80 
fun hol_term_to_fol_FO tm = 
35865  81 
case strip_combterm_comb tm of 
82 
(CombConst(c,_,tys), tms) => 

32956  83 
let val tyargs = map hol_type_to_fol tys 
84 
val args = map hol_term_to_fol_FO tms 

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

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

88 

35865  89 
fun hol_term_to_fol_HO (CombVar (a, _)) = Metis.Term.Var a 
90 
 hol_term_to_fol_HO (CombConst (a, _, tylist)) = 

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

94 

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

97 

35865  98 
fun hol_term_to_fol_FT (CombVar(a, ty)) = wrap_type (Metis.Term.Var a, ty) 
99 
 hol_term_to_fol_FT (CombConst(a, ty, _)) = 

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

104 

35865  105 
fun hol_literal_to_fol FO (Literal (pol, tm)) = 
106 
let val (CombConst(p,_,tys), tms) = strip_combterm_comb tm 

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

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

35865  110 
 hol_literal_to_fol HO (Literal (pol, tm)) = 
111 
(case strip_combterm_comb tm of 

112 
(CombConst("equal",_,_), tms) => 

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

35865  115 
 hol_literal_to_fol FT (Literal (pol, tm)) = 
116 
(case strip_combterm_comb tm of 

117 
(CombConst("equal",_,_), tms) => 

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

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

120 

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

124 

32956  125 
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*) 
35865  126 
fun metis_of_typeLit pos (LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x] 
127 
 metis_of_typeLit pos (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

128 

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

131 

32956  132 
fun metis_of_tfree tf = 
133 
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

134 

32956  135 
fun hol_thm_to_fol is_conjecture ctxt mode th = 
136 
let val thy = ProofContext.theory_of ctxt 

137 
val (mlits, types_sorts) = 

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

139 
in 

140 
if is_conjecture then 

35865  141 
(Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), add_typs types_sorts) 
32956  142 
else 
35865  143 
let val tylits = add_typs (filter (not o default_sort ctxt) types_sorts) 
32956  144 
val mtylits = if Config.get ctxt type_lits 
145 
then map (metis_of_typeLit false) tylits else [] 

146 
in 

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

148 
end 

149 
end; 

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

150 

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

152 

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

155 
 m_arity_cls (TVarLit (c,str)) = 

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

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

157 

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

162 

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

164 

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

167 

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

170 

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

173 
(*  *) 

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

174 

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

176 

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

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

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

180 

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

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

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

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

189 

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

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

193 
else error 

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

195 
" expected " ^ Int.toString nargs ^ 

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

197 
end; 

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

198 

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

25713  201 

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

204 
SEE ALSO axiom_inf below.*) 

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

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

206 

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

209 
let val ww = "'" ^ w 

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

211 

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

214 
 strip_happ args x = (x, args); 

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

215 

32994  216 
fun fol_type_to_isa _ (Metis.Term.Var v) = 
35865  217 
(case strip_prefix tvar_prefix v of 
218 
SOME w => make_tvar w 

219 
 NONE => make_tvar v) 

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

32956  223 
 NONE => 
35865  224 
case strip_prefix tfree_prefix x of 
32956  225 
SOME tf => mk_tfree ctxt tf 
226 
 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

227 

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

230 
let val thy = ProofContext.theory_of ctxt 

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

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

35865  233 
(case strip_prefix tvar_prefix v of 
234 
SOME w => Type (make_tvar w) 

32956  235 
 NONE => 
35865  236 
case strip_prefix schematic_var_prefix v of 
32956  237 
SOME w => Term (mk_var (w, HOLogic.typeT)) 
238 
 NONE => Term (mk_var (v, HOLogic.typeT)) ) 

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

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

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

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

243 
in case rator of 

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

245 
 _ => case tm_to_tt rator of 

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

247 
 _ => error "tm_to_tt: HO application" 

248 
end 

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

250 
and applic_to_tt ("=",ts) = 

35865  251 
Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts))) 
32956  252 
 applic_to_tt (a,ts) = 
35865  253 
case strip_prefix const_prefix a of 
32956  254 
SOME b => 
35865  255 
let val c = invert_const b 
256 
val ntypes = num_typargs thy c 

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

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

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

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

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

265 
" type arguments\n" ^ 

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

267 
" the terms are \n" ^ 

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

269 
end 

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

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

35865  278 
case strip_prefix fixed_var_prefix a of 
32956  279 
SOME b => 
280 
let val opr = Term.Free(b, HOLogic.typeT) 

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

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

283 
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

284 

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

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

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

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

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

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

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

302 
cvt tm1 $ cvt tm2 

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

304 
cvt tm1 $ cvt tm2 

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

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

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

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

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

317 
fol_term_to_hol_RAW ctxt t) 

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

319 

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

322 
 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

323 

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

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

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

328 
val ts' = infer_types ctxt ts; 

329 
val _ = app (fn t => trace_msg 

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

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

332 
ts' 

333 
in ts' end; 

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

334 

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

337 

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

339 

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

342 
(*  *) 

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

343 

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

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

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

348 
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

349 

32956  350 
fun lookth thpairs (fth : Metis.Thm.thm) = 
33035  351 
the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth) 
32956  352 
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

353 

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

355 

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

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

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

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

362 
in cterm_instantiate substs th end; 

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

363 

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

367 

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

370 
inst_excluded_middle 

371 
(ProofContext.theory_of ctxt) 

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

373 

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

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

377 
fun inst_inf ctxt mode thpairs fsubst th = 

378 
let val thy = ProofContext.theory_of ctxt 

379 
val i_th = lookth thpairs th 

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

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

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

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

386 
handle Option => 

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

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

389 
NONE) 

390 
fun remove_typeinst (a, t) = 

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

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

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

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

399 
val tms = infer_types ctxt rawtms; 

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

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

402 
val _ = trace_msg (fn () => 

403 
cat_lines ("subst_translations:" :: 

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

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

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

407 
in cterm_instantiate substs' i_th 

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

409 
end; 

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

410 

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

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

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

416 
fun resolve_inc_tyvars(tha,i,thb) = 

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

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

419 
in 

420 
case distinct Thm.eq_thm ths of 

421 
[th] => th 

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

423 
end; 

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

424 

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

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

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

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

430 
in 

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

432 
else if is_TrueI i_th2 then i_th1 

433 
else 

434 
let 

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

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

437 
val prems_th1 = prems_of i_th1 

438 
val prems_th2 = prems_of i_th2 

439 
val index_th1 = get_index (mk_not i_atm) prems_th1 

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

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

442 
val index_th2 = get_index i_atm prems_th2 

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

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

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

446 
end; 

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

447 

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

450 
val refl_idx = 1 + Thm.maxidx_of REFL_THM; 

25713  451 

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

454 
val i_t = singleton (fol_terms_to_hol ctxt mode) t 

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

456 
val c_t = cterm_incr_types thy refl_idx i_t 

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

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

458 

35865  459 
fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0 (*equality has no type arguments*) 
460 
 get_ty_arg_size thy (Const (c, _)) = (num_typargs thy c handle TYPE _ => 0) 

32994  461 
 get_ty_arg_size _ _ = 0; 
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset

462 

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

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

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

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

472 
 path_finder_FO tm (p::ps) = 

35865  473 
let val (tm1,args) = strip_comb tm 
32956  474 
val adjustment = get_ty_arg_size thy tm1 
475 
val p' = if adjustment > p then p else padjustment 

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

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

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

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

480 
" " ^ Syntax.string_of_term ctxt tm_p) 

481 
val (r,t) = path_finder_FO tm_p ps 

482 
in 

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

484 
end 

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

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

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

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

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

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

499 
fun path_finder FO tm ps _ = path_finder_FO tm ps 

35865  500 
 path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ = 
32956  501 
(*equality: not curried, as other predicates are*) 
502 
if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) 

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

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

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

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

511 
(*select first operand*) 

512 
else path_finder_FT tm (p::ps) 

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

514 
(*1 selects second operand*) 

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

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

521 
 path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm 

522 
val (tm_subst, body) = path_finder_lit i_atm fp 

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

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

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

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

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

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

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

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

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

533 

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

535 

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

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

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

544 
equality_inf ctxt mode f_lit f_p f_r; 

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

545 

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

547 

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

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

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

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

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

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

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

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

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

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

562 
end; 

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

563 

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

32994  566 
 used_axioms _ _ = NONE; 
24855  567 

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

570 
(*  *) 

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

571 

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

573 

32956  574 
fun type_ext thy tms = 
35865  575 
let val subs = tfree_classes_of_terms tms 
576 
val supers = tvar_classes_of_terms tms 

577 
and tycons = type_consts_of_terms thy tms 

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

579 
val classrel_clauses = make_classrel_clauses thy subs supers' 

32956  580 
in map classrel_cls classrel_clauses @ map arity_cls arity_clauses 
581 
end; 

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

582 

32956  583 
(*  *) 
584 
(* Logic maps manage the interface between HOL and firstorder logic. *) 

585 
(*  *) 

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

586 

32956  587 
type logic_map = 
35865  588 
{axioms: (Metis.Thm.thm * thm) list, 
589 
tfrees: type_literal list}; 

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

590 

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

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

597 

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

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

35865  601 
in 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

602 

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

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

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

607 
tfrees = tfrees} 

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

608 

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

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

612 
tfrees = tfrees}; 

25713  613 

32956  614 
fun string_of_mode FO = "FO" 
615 
 string_of_mode HO = "HO" 

616 
 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

617 

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

620 
let val thy = ProofContext.theory_of ctxt 

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

622 
fun set_mode FO = FO 

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

624 
 set_mode FT = FT 

625 
val mode = set_mode mode0 

626 
(*transform isabelle clause to metis clause *) 

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

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

33042  631 
tfrees = union (op =) tfree_lits tfrees} 
32956  632 
end; 
33339  633 
val lmap0 = fold (add_thm true) cls {axioms = [], tfrees = init_tfrees ctxt} 
634 
val lmap = fold (add_thm false) ths (add_tfrees lmap0) 

32956  635 
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap) 
32994  636 
fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists 
32956  637 
(*Now check for the existence of certain combinators*) 
35865  638 
val thI = if used "c_COMBI" then [cnf_th @{theory} @{thm COMBI_def}] else [] 
639 
val thK = if used "c_COMBK" then [cnf_th @{theory} @{thm COMBK_def}] else [] 

640 
val thB = if used "c_COMBB" then [cnf_th @{theory} @{thm COMBB_def}] else [] 

641 
val thC = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else [] 

642 
val thS = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else [] 

643 
val thEQ = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else [] 

32956  644 
val lmap' = if mode=FO then lmap 
33339  645 
else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap 
32956  646 
in 
647 
(mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap') 

648 
end; 

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

649 

32956  650 
fun refute cls = 
651 
Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls); 

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

652 

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

654 

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

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

658 

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

661 
let val thy = ProofContext.theory_of ctxt 

35826  662 
val th_cls_pairs = 
35865  663 
map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0 
32956  664 
val ths = maps #2 th_cls_pairs 
665 
val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") 

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

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

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

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

670 
val _ = if null tfrees then () 

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

35865  672 
app (fn tf => trace_msg (fn _ => tptp_of_typeLit true tf)) tfrees) 
32956  673 
val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS") 
674 
val thms = map #1 axioms 

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

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

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

678 
in 

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

682 
case refute thms of 

683 
Metis.Resolution.Contradiction mth => 

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

685 
Metis.Thm.toString mth) 

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

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

688 
val proof = Metis.Proof.proof mth 

689 
val result = translate mode ctxt' axioms proof 

690 
and used = map_filter (used_axioms axioms) proof 

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

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

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

32956  695 
in 
696 
if null unused then () 

33305  697 
else warning ("Metis: unused theorems " ^ commas_quote unused); 
32956  698 
case result of 
699 
(_,ith)::_ => 

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

701 
[ith]) 

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

703 
[]) 

704 
end 

705 
 Metis.Resolution.Satisfiable _ => 

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

707 
[]) 

708 
end; 

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

709 

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

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

713 
in 

35865  714 
if exists_type 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

715 
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

716 
else 
35865  717 
(Meson.MESON neg_clausify 
35568
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort  {} is the full universal sort;
wenzelm
parents:
34087
diff
changeset

718 
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i 
35865  719 
THEN Meson_Tactic.expand_defs_tac st0) st0 
32956  720 
end 
721 
handle METIS s => (warning ("Metis: " ^ s); Seq.empty); 

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

722 

32956  723 
val metis_tac = metis_general_tac HO; 
724 
val metisF_tac = metis_general_tac FO; 

725 
val metisFT_tac = metis_general_tac FT; 

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

726 

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

729 

32956  730 
val setup = 
731 
type_lits_setup #> 

35865  732 
method @{binding metis} HO "METIS for FOL and HOL problems" #> 
32956  733 
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

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

738 

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

739 
end; 