1.1 --- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Mar 19 06:14:37 2010 +0100
1.2 +++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Fri Mar 19 13:02:18 2010 +0100
1.3 @@ -18,9 +18,11 @@
1.4 structure Metis_Tactics : METIS_TACTICS =
1.5 struct
1.6
1.7 -structure SFC = Sledgehammer_FOL_Clause
1.8 -structure SHC = Sledgehammer_HOL_Clause
1.9 -structure SPR = Sledgehammer_Proof_Reconstruct
1.10 +open Sledgehammer_FOL_Clause
1.11 +open Sledgehammer_Fact_Preprocessor
1.12 +open Sledgehammer_HOL_Clause
1.13 +open Sledgehammer_Proof_Reconstruct
1.14 +open Sledgehammer_Fact_Filter
1.15
1.16 val trace = Unsynchronized.ref false;
1.17 fun trace_msg msg = if !trace then tracing (msg ()) else ();
1.18 @@ -67,62 +69,62 @@
1.19
1.20 fun metis_lit b c args = (b, (c, args));
1.21
1.22 -fun hol_type_to_fol (SFC.AtomV x) = Metis.Term.Var x
1.23 - | hol_type_to_fol (SFC.AtomF x) = Metis.Term.Fn(x,[])
1.24 - | hol_type_to_fol (SFC.Comp(tc,tps)) = Metis.Term.Fn(tc, map hol_type_to_fol tps);
1.25 +fun hol_type_to_fol (AtomV x) = Metis.Term.Var x
1.26 + | hol_type_to_fol (AtomF x) = Metis.Term.Fn (x, [])
1.27 + | hol_type_to_fol (Comp (tc, tps)) =
1.28 + Metis.Term.Fn (tc, map hol_type_to_fol tps);
1.29
1.30 (*These two functions insert type literals before the real literals. That is the
1.31 opposite order from TPTP linkup, but maybe OK.*)
1.32
1.33 fun hol_term_to_fol_FO tm =
1.34 - case SHC.strip_comb tm of
1.35 - (SHC.CombConst(c,_,tys), tms) =>
1.36 + case strip_combterm_comb tm of
1.37 + (CombConst(c,_,tys), tms) =>
1.38 let val tyargs = map hol_type_to_fol tys
1.39 val args = map hol_term_to_fol_FO tms
1.40 in Metis.Term.Fn (c, tyargs @ args) end
1.41 - | (SHC.CombVar(v,_), []) => Metis.Term.Var v
1.42 + | (CombVar(v,_), []) => Metis.Term.Var v
1.43 | _ => error "hol_term_to_fol_FO";
1.44
1.45 -fun hol_term_to_fol_HO (SHC.CombVar (a, _)) = Metis.Term.Var a
1.46 - | hol_term_to_fol_HO (SHC.CombConst (a, _, tylist)) =
1.47 +fun hol_term_to_fol_HO (CombVar (a, _)) = Metis.Term.Var a
1.48 + | hol_term_to_fol_HO (CombConst (a, _, tylist)) =
1.49 Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
1.50 - | hol_term_to_fol_HO (SHC.CombApp (tm1, tm2)) =
1.51 + | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
1.52 Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
1.53
1.54 (*The fully-typed translation, to avoid type errors*)
1.55 fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
1.56
1.57 -fun hol_term_to_fol_FT (SHC.CombVar(a, ty)) =
1.58 - wrap_type (Metis.Term.Var a, ty)
1.59 - | hol_term_to_fol_FT (SHC.CombConst(a, ty, _)) =
1.60 +fun hol_term_to_fol_FT (CombVar(a, ty)) = wrap_type (Metis.Term.Var a, ty)
1.61 + | hol_term_to_fol_FT (CombConst(a, ty, _)) =
1.62 wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
1.63 - | hol_term_to_fol_FT (tm as SHC.CombApp(tm1,tm2)) =
1.64 + | hol_term_to_fol_FT (tm as CombApp(tm1,tm2)) =
1.65 wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
1.66 - SHC.type_of_combterm tm);
1.67 + type_of_combterm tm);
1.68
1.69 -fun hol_literal_to_fol FO (SHC.Literal (pol, tm)) =
1.70 - let val (SHC.CombConst(p,_,tys), tms) = SHC.strip_comb tm
1.71 +fun hol_literal_to_fol FO (Literal (pol, tm)) =
1.72 + let val (CombConst(p,_,tys), tms) = strip_combterm_comb tm
1.73 val tylits = if p = "equal" then [] else map hol_type_to_fol tys
1.74 val lits = map hol_term_to_fol_FO tms
1.75 in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
1.76 - | hol_literal_to_fol HO (SHC.Literal (pol, tm)) =
1.77 - (case SHC.strip_comb tm of
1.78 - (SHC.CombConst("equal",_,_), tms) =>
1.79 + | hol_literal_to_fol HO (Literal (pol, tm)) =
1.80 + (case strip_combterm_comb tm of
1.81 + (CombConst("equal",_,_), tms) =>
1.82 metis_lit pol "=" (map hol_term_to_fol_HO tms)
1.83 | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*)
1.84 - | hol_literal_to_fol FT (SHC.Literal (pol, tm)) =
1.85 - (case SHC.strip_comb tm of
1.86 - (SHC.CombConst("equal",_,_), tms) =>
1.87 + | hol_literal_to_fol FT (Literal (pol, tm)) =
1.88 + (case strip_combterm_comb tm of
1.89 + (CombConst("equal",_,_), tms) =>
1.90 metis_lit pol "=" (map hol_term_to_fol_FT tms)
1.91 | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
1.92
1.93 fun literals_of_hol_thm thy mode t =
1.94 - let val (lits, types_sorts) = SHC.literals_of_term thy t
1.95 + let val (lits, types_sorts) = literals_of_term thy t
1.96 in (map (hol_literal_to_fol mode) lits, types_sorts) end;
1.97
1.98 (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
1.99 -fun metis_of_typeLit pos (SFC.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
1.100 - | metis_of_typeLit pos (SFC.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
1.101 +fun metis_of_typeLit pos (LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
1.102 + | metis_of_typeLit pos (LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
1.103
1.104 fun default_sort _ (TVar _) = false
1.105 | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
1.106 @@ -136,10 +138,9 @@
1.107 (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
1.108 in
1.109 if is_conjecture then
1.110 - (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), SFC.add_typs types_sorts)
1.111 + (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), add_typs types_sorts)
1.112 else
1.113 - let val tylits = SFC.add_typs
1.114 - (filter (not o default_sort ctxt) types_sorts)
1.115 + let val tylits = add_typs (filter (not o default_sort ctxt) types_sorts)
1.116 val mtylits = if Config.get ctxt type_lits
1.117 then map (metis_of_typeLit false) tylits else []
1.118 in
1.119 @@ -149,13 +150,13 @@
1.120
1.121 (* ARITY CLAUSE *)
1.122
1.123 -fun m_arity_cls (SFC.TConsLit (c,t,args)) =
1.124 - metis_lit true (SFC.make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
1.125 - | m_arity_cls (SFC.TVarLit (c,str)) =
1.126 - metis_lit false (SFC.make_type_class c) [Metis.Term.Var str];
1.127 +fun m_arity_cls (TConsLit (c,t,args)) =
1.128 + metis_lit true (make_type_class c) [Metis.Term.Fn(t, map Metis.Term.Var args)]
1.129 + | m_arity_cls (TVarLit (c,str)) =
1.130 + metis_lit false (make_type_class c) [Metis.Term.Var str];
1.131
1.132 (*TrueI is returned as the Isabelle counterpart because there isn't any.*)
1.133 -fun arity_cls (SFC.ArityClause{conclLit,premLits,...}) =
1.134 +fun arity_cls (ArityClause {conclLit, premLits, ...}) =
1.135 (TrueI,
1.136 Metis.Thm.axiom (Metis.LiteralSet.fromList (map m_arity_cls (conclLit :: premLits))));
1.137
1.138 @@ -164,7 +165,7 @@
1.139 fun m_classrel_cls subclass superclass =
1.140 [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
1.141
1.142 -fun classrel_cls (SFC.ClassrelClause {subclass, superclass, ...}) =
1.143 +fun classrel_cls (ClassrelClause {subclass, superclass, ...}) =
1.144 (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
1.145
1.146 (* ------------------------------------------------------------------------- *)
1.147 @@ -213,14 +214,14 @@
1.148 | strip_happ args x = (x, args);
1.149
1.150 fun fol_type_to_isa _ (Metis.Term.Var v) =
1.151 - (case SPR.strip_prefix SFC.tvar_prefix v of
1.152 - SOME w => SPR.make_tvar w
1.153 - | NONE => SPR.make_tvar v)
1.154 + (case strip_prefix tvar_prefix v of
1.155 + SOME w => make_tvar w
1.156 + | NONE => make_tvar v)
1.157 | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
1.158 - (case SPR.strip_prefix SFC.tconst_prefix x of
1.159 - SOME tc => Term.Type (SPR.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
1.160 + (case strip_prefix tconst_prefix x of
1.161 + SOME tc => Term.Type (invert_type_const tc, map (fol_type_to_isa ctxt) tys)
1.162 | NONE =>
1.163 - case SPR.strip_prefix SFC.tfree_prefix x of
1.164 + case strip_prefix tfree_prefix x of
1.165 SOME tf => mk_tfree ctxt tf
1.166 | NONE => error ("fol_type_to_isa: " ^ x));
1.167
1.168 @@ -229,10 +230,10 @@
1.169 let val thy = ProofContext.theory_of ctxt
1.170 val _ = trace_msg (fn () => "fol_term_to_hol: " ^ Metis.Term.toString fol_tm)
1.171 fun tm_to_tt (Metis.Term.Var v) =
1.172 - (case SPR.strip_prefix SFC.tvar_prefix v of
1.173 - SOME w => Type (SPR.make_tvar w)
1.174 + (case strip_prefix tvar_prefix v of
1.175 + SOME w => Type (make_tvar w)
1.176 | NONE =>
1.177 - case SPR.strip_prefix SFC.schematic_var_prefix v of
1.178 + case strip_prefix schematic_var_prefix v of
1.179 SOME w => Term (mk_var (w, HOLogic.typeT))
1.180 | NONE => Term (mk_var (v, HOLogic.typeT)) )
1.181 (*Var from Metis with a name like _nnn; possibly a type variable*)
1.182 @@ -247,16 +248,16 @@
1.183 end
1.184 | tm_to_tt (Metis.Term.Fn (fname, args)) = applic_to_tt (fname,args)
1.185 and applic_to_tt ("=",ts) =
1.186 - Term (list_comb(Const ("op =", HOLogic.typeT), terms_of (map tm_to_tt ts)))
1.187 + Term (list_comb(Const (@{const_name "op ="}, HOLogic.typeT), terms_of (map tm_to_tt ts)))
1.188 | applic_to_tt (a,ts) =
1.189 - case SPR.strip_prefix SFC.const_prefix a of
1.190 + case strip_prefix const_prefix a of
1.191 SOME b =>
1.192 - let val c = SPR.invert_const b
1.193 - val ntypes = SPR.num_typargs thy c
1.194 + let val c = invert_const b
1.195 + val ntypes = num_typargs thy c
1.196 val nterms = length ts - ntypes
1.197 val tts = map tm_to_tt ts
1.198 val tys = types_of (List.take(tts,ntypes))
1.199 - val ntyargs = SPR.num_typargs thy c
1.200 + val ntyargs = num_typargs thy c
1.201 in if length tys = ntyargs then
1.202 apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
1.203 else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
1.204 @@ -267,14 +268,14 @@
1.205 cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts)))
1.206 end
1.207 | NONE => (*Not a constant. Is it a type constructor?*)
1.208 - case SPR.strip_prefix SFC.tconst_prefix a of
1.209 + case strip_prefix tconst_prefix a of
1.210 SOME b =>
1.211 - Type (Term.Type (SPR.invert_type_const b, types_of (map tm_to_tt ts)))
1.212 + Type (Term.Type (invert_type_const b, types_of (map tm_to_tt ts)))
1.213 | NONE => (*Maybe a TFree. Should then check that ts=[].*)
1.214 - case SPR.strip_prefix SFC.tfree_prefix a of
1.215 + case strip_prefix tfree_prefix a of
1.216 SOME b => Type (mk_tfree ctxt b)
1.217 | NONE => (*a fixed variable? They are Skolem functions.*)
1.218 - case SPR.strip_prefix SFC.fixed_var_prefix a of
1.219 + case strip_prefix fixed_var_prefix a of
1.220 SOME b =>
1.221 let val opr = Term.Free(b, HOLogic.typeT)
1.222 in apply_list opr (length ts) (map tm_to_tt ts) end
1.223 @@ -285,16 +286,16 @@
1.224 fun fol_term_to_hol_FT ctxt fol_tm =
1.225 let val _ = trace_msg (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
1.226 fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
1.227 - (case SPR.strip_prefix SFC.schematic_var_prefix v of
1.228 + (case strip_prefix schematic_var_prefix v of
1.229 SOME w => mk_var(w, dummyT)
1.230 | NONE => mk_var(v, dummyT))
1.231 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), _])) =
1.232 Const ("op =", HOLogic.typeT)
1.233 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
1.234 - (case SPR.strip_prefix SFC.const_prefix x of
1.235 - SOME c => Const (SPR.invert_const c, dummyT)
1.236 + (case strip_prefix const_prefix x of
1.237 + SOME c => Const (invert_const c, dummyT)
1.238 | NONE => (*Not a constant. Is it a fixed variable??*)
1.239 - case SPR.strip_prefix SFC.fixed_var_prefix x of
1.240 + case strip_prefix fixed_var_prefix x of
1.241 SOME v => Free (v, fol_type_to_isa ctxt ty)
1.242 | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
1.243 | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
1.244 @@ -303,12 +304,12 @@
1.245 cvt tm1 $ cvt tm2
1.246 | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*)
1.247 | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
1.248 - list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2])
1.249 + list_comb(Const (@{const_name "op ="}, HOLogic.typeT), map cvt [tm1,tm2])
1.250 | cvt (t as Metis.Term.Fn (x, [])) =
1.251 - (case SPR.strip_prefix SFC.const_prefix x of
1.252 - SOME c => Const (SPR.invert_const c, dummyT)
1.253 + (case strip_prefix const_prefix x of
1.254 + SOME c => Const (invert_const c, dummyT)
1.255 | NONE => (*Not a constant. Is it a fixed variable??*)
1.256 - case SPR.strip_prefix SFC.fixed_var_prefix x of
1.257 + case strip_prefix fixed_var_prefix x of
1.258 SOME v => Free (v, dummyT)
1.259 | NONE => (trace_msg (fn () => "fol_term_to_hol_FT bad const: " ^ x);
1.260 fol_term_to_hol_RAW ctxt t))
1.261 @@ -331,7 +332,7 @@
1.262 ts'
1.263 in ts' end;
1.264
1.265 -fun mk_not (Const ("Not", _) $ b) = b
1.266 +fun mk_not (Const (@{const_name Not}, _) $ b) = b
1.267 | mk_not b = HOLogic.mk_not b;
1.268
1.269 val metis_eq = Metis.Term.Fn ("=", []);
1.270 @@ -387,9 +388,9 @@
1.271 " in " ^ Display.string_of_thm ctxt i_th);
1.272 NONE)
1.273 fun remove_typeinst (a, t) =
1.274 - case SPR.strip_prefix SFC.schematic_var_prefix a of
1.275 + case strip_prefix schematic_var_prefix a of
1.276 SOME b => SOME (b, t)
1.277 - | NONE => case SPR.strip_prefix SFC.tvar_prefix a of
1.278 + | NONE => case strip_prefix tvar_prefix a of
1.279 SOME _ => NONE (*type instantiations are forbidden!*)
1.280 | NONE => SOME (a,t) (*internal Metis var?*)
1.281 val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
1.282 @@ -455,8 +456,8 @@
1.283 val c_t = cterm_incr_types thy refl_idx i_t
1.284 in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
1.285
1.286 -fun get_ty_arg_size _ (Const ("op =", _)) = 0 (*equality has no type arguments*)
1.287 - | get_ty_arg_size thy (Const (c, _)) = (SPR.num_typargs thy c handle TYPE _ => 0)
1.288 +fun get_ty_arg_size _ (Const (@{const_name "op ="}, _)) = 0 (*equality has no type arguments*)
1.289 + | get_ty_arg_size thy (Const (c, _)) = (num_typargs thy c handle TYPE _ => 0)
1.290 | get_ty_arg_size _ _ = 0;
1.291
1.292 (* INFERENCE RULE: EQUALITY *)
1.293 @@ -469,7 +470,7 @@
1.294 | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
1.295 fun path_finder_FO tm [] = (tm, Term.Bound 0)
1.296 | path_finder_FO tm (p::ps) =
1.297 - let val (tm1,args) = Term.strip_comb tm
1.298 + let val (tm1,args) = strip_comb tm
1.299 val adjustment = get_ty_arg_size thy tm1
1.300 val p' = if adjustment > p then p else p-adjustment
1.301 val tm_p = List.nth(args,p')
1.302 @@ -496,13 +497,13 @@
1.303 " isa-term: " ^ Syntax.string_of_term ctxt tm ^
1.304 " fol-term: " ^ Metis.Term.toString t)
1.305 fun path_finder FO tm ps _ = path_finder_FO tm ps
1.306 - | path_finder HO (tm as Const("op =",_) $ _ $ _) (p::ps) _ =
1.307 + | path_finder HO (tm as Const(@{const_name "op ="},_) $ _ $ _) (p::ps) _ =
1.308 (*equality: not curried, as other predicates are*)
1.309 if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
1.310 else path_finder_HO tm (p::ps) (*1 selects second operand*)
1.311 | path_finder HO tm (_ :: ps) (Metis.Term.Fn ("{}", [_])) =
1.312 path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
1.313 - | path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps)
1.314 + | path_finder FT (tm as Const(@{const_name "op ="}, _) $ _ $ _) (p::ps)
1.315 (Metis.Term.Fn ("=", [t1,t2])) =
1.316 (*equality: not curried, as other predicates are*)
1.317 if p=0 then path_finder_FT tm (0::1::ps)
1.318 @@ -514,7 +515,7 @@
1.319 | path_finder FT tm (_ :: ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
1.320 (*if not equality, ignore head to skip the hBOOL predicate*)
1.321 | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*)
1.322 - fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx =
1.323 + fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx =
1.324 let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
1.325 in (tm, nt $ tm_rslt) end
1.326 | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
1.327 @@ -542,7 +543,7 @@
1.328 | step ctxt mode _ (_, Metis.Proof.Equality (f_lit, f_p, f_r)) =
1.329 equality_inf ctxt mode f_lit f_p f_r;
1.330
1.331 -fun real_literal (_, (c, _)) = not (String.isPrefix SFC.class_prefix c);
1.332 +fun real_literal (_, (c, _)) = not (String.isPrefix class_prefix c);
1.333
1.334 fun translate _ _ thpairs [] = thpairs
1.335 | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
1.336 @@ -568,23 +569,14 @@
1.337 (* Translation of HO Clauses *)
1.338 (* ------------------------------------------------------------------------- *)
1.339
1.340 -fun cnf_th thy th = hd (Sledgehammer_Fact_Preprocessor.cnf_axiom thy th);
1.341 -
1.342 -val equal_imp_fequal' = cnf_th @{theory} @{thm equal_imp_fequal};
1.343 -val fequal_imp_equal' = cnf_th @{theory} @{thm fequal_imp_equal};
1.344 -
1.345 -val comb_I = cnf_th @{theory} SHC.comb_I;
1.346 -val comb_K = cnf_th @{theory} SHC.comb_K;
1.347 -val comb_B = cnf_th @{theory} SHC.comb_B;
1.348 -val comb_C = cnf_th @{theory} SHC.comb_C;
1.349 -val comb_S = cnf_th @{theory} SHC.comb_S;
1.350 +fun cnf_th thy th = hd (cnf_axiom thy th);
1.351
1.352 fun type_ext thy tms =
1.353 - let val subs = Sledgehammer_Fact_Filter.tfree_classes_of_terms tms
1.354 - val supers = Sledgehammer_Fact_Filter.tvar_classes_of_terms tms
1.355 - and tycons = Sledgehammer_Fact_Filter.type_consts_of_terms thy tms
1.356 - val (supers', arity_clauses) = SFC.make_arity_clauses thy tycons supers
1.357 - val classrel_clauses = SFC.make_classrel_clauses thy subs supers'
1.358 + let val subs = tfree_classes_of_terms tms
1.359 + val supers = tvar_classes_of_terms tms
1.360 + and tycons = type_consts_of_terms thy tms
1.361 + val (supers', arity_clauses) = make_arity_clauses thy tycons supers
1.362 + val classrel_clauses = make_classrel_clauses thy subs supers'
1.363 in map classrel_cls classrel_clauses @ map arity_cls arity_clauses
1.364 end;
1.365
1.366 @@ -593,8 +585,8 @@
1.367 (* ------------------------------------------------------------------------- *)
1.368
1.369 type logic_map =
1.370 - {axioms : (Metis.Thm.thm * thm) list,
1.371 - tfrees : SFC.type_literal list};
1.372 + {axioms: (Metis.Thm.thm * thm) list,
1.373 + tfrees: type_literal list};
1.374
1.375 fun const_in_metis c (pred, tm_list) =
1.376 let
1.377 @@ -606,7 +598,7 @@
1.378 (*Extract TFree constraints from context to include as conjecture clauses*)
1.379 fun init_tfrees ctxt =
1.380 let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
1.381 - in SFC.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
1.382 + in add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
1.383
1.384 (*transform isabelle type / arity clause to metis clause *)
1.385 fun add_type_thm [] lmap = lmap
1.386 @@ -643,12 +635,12 @@
1.387 val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
1.388 fun used c = exists (Metis.LiteralSet.exists (const_in_metis c o #2)) clause_lists
1.389 (*Now check for the existence of certain combinators*)
1.390 - val thI = if used "c_COMBI" then [comb_I] else []
1.391 - val thK = if used "c_COMBK" then [comb_K] else []
1.392 - val thB = if used "c_COMBB" then [comb_B] else []
1.393 - val thC = if used "c_COMBC" then [comb_C] else []
1.394 - val thS = if used "c_COMBS" then [comb_S] else []
1.395 - val thEQ = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
1.396 + val thI = if used "c_COMBI" then [cnf_th @{theory} @{thm COMBI_def}] else []
1.397 + val thK = if used "c_COMBK" then [cnf_th @{theory} @{thm COMBK_def}] else []
1.398 + val thB = if used "c_COMBB" then [cnf_th @{theory} @{thm COMBB_def}] else []
1.399 + val thC = if used "c_COMBC" then [cnf_th @{theory} @{thm COMBC_def}] else []
1.400 + val thS = if used "c_COMBS" then [cnf_th @{theory} @{thm COMBS_def}] else []
1.401 + val thEQ = if used "c_fequal" then [cnf_th @{theory} @{thm fequal_imp_equal}, cnf_th @{theory} @{thm equal_imp_fequal}] else []
1.402 val lmap' = if mode=FO then lmap
1.403 else fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI) lmap
1.404 in
1.405 @@ -668,7 +660,7 @@
1.406 fun FOL_SOLVE mode ctxt cls ths0 =
1.407 let val thy = ProofContext.theory_of ctxt
1.408 val th_cls_pairs =
1.409 - map (fn th => (Thm.get_name_hint th, Sledgehammer_Fact_Preprocessor.cnf_axiom thy th)) ths0
1.410 + map (fn th => (Thm.get_name_hint th, cnf_axiom thy th)) ths0
1.411 val ths = maps #2 th_cls_pairs
1.412 val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
1.413 val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
1.414 @@ -677,7 +669,7 @@
1.415 val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
1.416 val _ = if null tfrees then ()
1.417 else (trace_msg (fn () => "TFREE CLAUSES");
1.418 - app (fn tf => trace_msg (fn _ => SFC.tptp_of_typeLit true tf)) tfrees)
1.419 + app (fn tf => trace_msg (fn _ => tptp_of_typeLit true tf)) tfrees)
1.420 val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
1.421 val thms = map #1 axioms
1.422 val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
1.423 @@ -719,12 +711,12 @@
1.424 let val _ = trace_msg (fn () =>
1.425 "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
1.426 in
1.427 - if exists_type Sledgehammer_Fact_Preprocessor.type_has_topsort (prop_of st0)
1.428 + if exists_type type_has_topsort (prop_of st0)
1.429 then raise METIS "Metis: Proof state contains the universal sort {}"
1.430 else
1.431 - (Meson.MESON Sledgehammer_Fact_Preprocessor.neg_clausify
1.432 + (Meson.MESON neg_clausify
1.433 (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
1.434 - THEN Sledgehammer_Fact_Preprocessor.expand_defs_tac st0) st0
1.435 + THEN Meson_Tactic.expand_defs_tac st0) st0
1.436 end
1.437 handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
1.438
1.439 @@ -737,11 +729,11 @@
1.440
1.441 val setup =
1.442 type_lits_setup #>
1.443 - method @{binding metis} HO "METIS for FOL & HOL problems" #>
1.444 + method @{binding metis} HO "METIS for FOL and HOL problems" #>
1.445 method @{binding metisF} FO "METIS for FOL problems" #>
1.446 method @{binding metisFT} FT "METIS with fully-typed translation" #>
1.447 Method.setup @{binding finish_clausify}
1.448 - (Scan.succeed (K (SIMPLE_METHOD (Sledgehammer_Fact_Preprocessor.expand_defs_tac refl))))
1.449 + (Scan.succeed (K (SIMPLE_METHOD (Meson_Tactic.expand_defs_tac refl))))
1.450 "cleanup after conversion to clauses";
1.451
1.452 end;