diff -r 277addece9b7 -r 78faa9b31202 src/HOL/Tools/Sledgehammer/metis_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML Mon Oct 04 22:01:34 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,557 +0,0 @@ -(* Title: HOL/Tools/Sledgehammer/metis_reconstruct.ML - Author: Kong W. Susanto, Cambridge University Computer Laboratory - Author: Lawrence C. Paulson, Cambridge University Computer Laboratory - Author: Jasmin Blanchette, TU Muenchen - Copyright Cambridge University 2007 - -Proof reconstruction for Metis. -*) - -signature METIS_RECONSTRUCT = -sig - type mode = Metis_Translate.mode - - val trace : bool Unsynchronized.ref - val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a - val untyped_aconv : term -> term -> bool - val replay_one_inference : - Proof.context -> mode -> (string * term) list - -> Metis_Thm.thm * Metis_Proof.inference -> (Metis_Thm.thm * thm) list - -> (Metis_Thm.thm * thm) list -end; - -structure Metis_Reconstruct : METIS_RECONSTRUCT = -struct - -open Metis_Translate - -val trace = Unsynchronized.ref false -fun trace_msg msg = if !trace then tracing (msg ()) else () - -datatype term_or_type = SomeTerm of term | SomeType of typ - -fun terms_of [] = [] - | terms_of (SomeTerm t :: tts) = t :: terms_of tts - | terms_of (SomeType _ :: tts) = terms_of tts; - -fun types_of [] = [] - | types_of (SomeTerm (Var ((a,idx), _)) :: tts) = - if String.isPrefix "_" a then - (*Variable generated by Metis, which might have been a type variable.*) - TVar (("'" ^ a, idx), HOLogic.typeS) :: types_of tts - else types_of tts - | types_of (SomeTerm _ :: tts) = types_of tts - | types_of (SomeType T :: tts) = T :: types_of tts; - -fun apply_list rator nargs rands = - let val trands = terms_of rands - in if length trands = nargs then SomeTerm (list_comb(rator, trands)) - else raise Fail - ("apply_list: wrong number of arguments: " ^ Syntax.string_of_term_global Pure.thy rator ^ - " expected " ^ Int.toString nargs ^ - " received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands)) - end; - -fun infer_types ctxt = - Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt); - -(*We use 1 rather than 0 because variable references in clauses may otherwise conflict - with variable constraints in the goal...at least, type inference often fails otherwise. - SEE ALSO axiom_inf below.*) -fun mk_var (w, T) = Var ((w, 1), T) - -(*include the default sort, if available*) -fun mk_tfree ctxt w = - let val ww = "'" ^ w - in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end; - -(*Remove the "apply" operator from an HO term*) -fun strip_happ args (Metis_Term.Fn(".",[t,u])) = strip_happ (u::args) t - | strip_happ args x = (x, args); - -fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS) - -fun smart_invert_const "fequal" = @{const_name HOL.eq} - | smart_invert_const s = invert_const s - -fun hol_type_from_metis_term _ (Metis_Term.Var v) = - (case strip_prefix_and_unascii tvar_prefix v of - SOME w => make_tvar w - | NONE => make_tvar v) - | hol_type_from_metis_term ctxt (Metis_Term.Fn(x, tys)) = - (case strip_prefix_and_unascii type_const_prefix x of - SOME tc => Type (smart_invert_const tc, - map (hol_type_from_metis_term ctxt) tys) - | NONE => - case strip_prefix_and_unascii tfree_prefix x of - SOME tf => mk_tfree ctxt tf - | NONE => raise Fail ("hol_type_from_metis_term: " ^ x)); - -(*Maps metis terms to isabelle terms*) -fun hol_term_from_metis_PT ctxt fol_tm = - let val thy = ProofContext.theory_of ctxt - val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^ - Metis_Term.toString fol_tm) - fun tm_to_tt (Metis_Term.Var v) = - (case strip_prefix_and_unascii tvar_prefix v of - SOME w => SomeType (make_tvar w) - | NONE => - case strip_prefix_and_unascii schematic_var_prefix v of - SOME w => SomeTerm (mk_var (w, HOLogic.typeT)) - | NONE => SomeTerm (mk_var (v, HOLogic.typeT)) ) - (*Var from Metis with a name like _nnn; possibly a type variable*) - | tm_to_tt (Metis_Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*) - | tm_to_tt (t as Metis_Term.Fn (".",_)) = - let val (rator,rands) = strip_happ [] t - in case rator of - Metis_Term.Fn(fname,ts) => applic_to_tt (fname, ts @ rands) - | _ => case tm_to_tt rator of - SomeTerm t => SomeTerm (list_comb(t, terms_of (map tm_to_tt rands))) - | _ => raise Fail "tm_to_tt: HO application" - end - | tm_to_tt (Metis_Term.Fn (fname, args)) = applic_to_tt (fname,args) - and applic_to_tt ("=",ts) = - SomeTerm (list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), terms_of (map tm_to_tt ts))) - | applic_to_tt (a,ts) = - case strip_prefix_and_unascii const_prefix a of - SOME b => - let - val c = smart_invert_const b - val ntypes = num_type_args thy c - val nterms = length ts - ntypes - val tts = map tm_to_tt ts - val tys = types_of (List.take(tts,ntypes)) - val t = - if String.isPrefix new_skolem_const_prefix c then - Var (new_skolem_var_from_const c, - Type_Infer.paramify_vars (tl tys ---> hd tys)) - else - Const (c, dummyT) - in if length tys = ntypes then - apply_list t nterms (List.drop(tts,ntypes)) - else - raise Fail ("Constant " ^ c ^ " expects " ^ Int.toString ntypes ^ - " but gets " ^ Int.toString (length tys) ^ - " type arguments\n" ^ - cat_lines (map (Syntax.string_of_typ ctxt) tys) ^ - " the terms are \n" ^ - cat_lines (map (Syntax.string_of_term ctxt) (terms_of tts))) - end - | NONE => (*Not a constant. Is it a type constructor?*) - case strip_prefix_and_unascii type_const_prefix a of - SOME b => - SomeType (Type (smart_invert_const b, types_of (map tm_to_tt ts))) - | NONE => (*Maybe a TFree. Should then check that ts=[].*) - case strip_prefix_and_unascii tfree_prefix a of - SOME b => SomeType (mk_tfree ctxt b) - | NONE => (*a fixed variable? They are Skolem functions.*) - case strip_prefix_and_unascii fixed_var_prefix a of - SOME b => - let val opr = Free (b, HOLogic.typeT) - in apply_list opr (length ts) (map tm_to_tt ts) end - | NONE => raise Fail ("unexpected metis function: " ^ a) - in - case tm_to_tt fol_tm of - SomeTerm t => t - | SomeType T => raise TYPE ("fol_tm_to_tt: Term expected", [T], []) - end - -(*Maps fully-typed metis terms to isabelle terms*) -fun hol_term_from_metis_FT ctxt fol_tm = - let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^ - Metis_Term.toString fol_tm) - fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) = - (case strip_prefix_and_unascii schematic_var_prefix v of - SOME w => mk_var(w, dummyT) - | NONE => mk_var(v, dummyT)) - | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn ("=",[]), _])) = - Const (@{const_name HOL.eq}, HOLogic.typeT) - | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (x,[]), ty])) = - (case strip_prefix_and_unascii const_prefix x of - SOME c => Const (smart_invert_const c, dummyT) - | NONE => (*Not a constant. Is it a fixed variable??*) - case strip_prefix_and_unascii fixed_var_prefix x of - SOME v => Free (v, hol_type_from_metis_term ctxt ty) - | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x)) - | cvt (Metis_Term.Fn ("ti", [Metis_Term.Fn (".",[tm1,tm2]), _])) = - cvt tm1 $ cvt tm2 - | cvt (Metis_Term.Fn (".",[tm1,tm2])) = (*untyped application*) - cvt tm1 $ cvt tm2 - | cvt (Metis_Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*) - | cvt (Metis_Term.Fn ("=", [tm1,tm2])) = - list_comb(Const (@{const_name HOL.eq}, HOLogic.typeT), map cvt [tm1,tm2]) - | cvt (t as Metis_Term.Fn (x, [])) = - (case strip_prefix_and_unascii const_prefix x of - SOME c => Const (smart_invert_const c, dummyT) - | NONE => (*Not a constant. Is it a fixed variable??*) - case strip_prefix_and_unascii fixed_var_prefix x of - SOME v => Free (v, dummyT) - | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x); - hol_term_from_metis_PT ctxt t)) - | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t); - hol_term_from_metis_PT ctxt t) - in fol_tm |> cvt end - -fun hol_term_from_metis FT = hol_term_from_metis_FT - | hol_term_from_metis _ = hol_term_from_metis_PT - -fun hol_terms_from_fol ctxt mode old_skolems fol_tms = - let val ts = map (hol_term_from_metis mode ctxt) fol_tms - val _ = trace_msg (fn () => " calling type inference:") - val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts - val ts' = ts |> map (reveal_old_skolem_terms old_skolems) - |> infer_types ctxt - val _ = app (fn t => trace_msg - (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ - " of type " ^ Syntax.string_of_typ ctxt (type_of t))) - ts' - in ts' end; - -(* ------------------------------------------------------------------------- *) -(* FOL step Inference Rules *) -(* ------------------------------------------------------------------------- *) - -(*for debugging only*) -(* -fun print_thpair (fth,th) = - (trace_msg (fn () => "============================================="); - trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth); - trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th)); -*) - -fun lookth thpairs (fth : Metis_Thm.thm) = - the (AList.lookup (uncurry Metis_Thm.equal) thpairs fth) - handle Option.Option => - raise Fail ("Failed to find Metis theorem " ^ Metis_Thm.toString fth) - -fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx)); - -(* INFERENCE RULE: AXIOM *) - -fun axiom_inf thpairs th = Thm.incr_indexes 1 (lookth thpairs th); - (*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*) - -(* INFERENCE RULE: ASSUME *) - -val EXCLUDED_MIDDLE = @{lemma "P ==> ~ P ==> False" by (rule notE)} - -fun inst_excluded_middle thy i_atm = - let val th = EXCLUDED_MIDDLE - val [vx] = Term.add_vars (prop_of th) [] - val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)] - in cterm_instantiate substs th end; - -fun assume_inf ctxt mode old_skolems atm = - inst_excluded_middle - (ProofContext.theory_of ctxt) - (singleton (hol_terms_from_fol ctxt mode old_skolems) (Metis_Term.Fn atm)) - -(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying - to reconstruct them admits new possibilities of errors, e.g. concerning - sorts. Instead we try to arrange that new TVars are distinct and that types - can be inferred from terms. *) - -fun inst_inf ctxt mode old_skolems thpairs fsubst th = - let val thy = ProofContext.theory_of ctxt - val i_th = lookth thpairs th - val i_th_vars = Term.add_vars (prop_of i_th) [] - fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars) - fun subst_translation (x,y) = - let val v = find_var x - (* We call "reveal_old_skolem_terms" and "infer_types" below. *) - val t = hol_term_from_metis mode ctxt y - in SOME (cterm_of thy (Var v), t) end - handle Option.Option => - (trace_msg (fn () => "\"find_var\" failed for " ^ x ^ - " in " ^ Display.string_of_thm ctxt i_th); - NONE) - | TYPE _ => - (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^ - " in " ^ Display.string_of_thm ctxt i_th); - NONE) - fun remove_typeinst (a, t) = - case strip_prefix_and_unascii schematic_var_prefix a of - SOME b => SOME (b, t) - | NONE => case strip_prefix_and_unascii tvar_prefix a of - SOME _ => NONE (*type instantiations are forbidden!*) - | NONE => SOME (a,t) (*internal Metis var?*) - val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th) - val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst) - val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs) - val tms = rawtms |> map (reveal_old_skolem_terms old_skolems) - |> infer_types ctxt - val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th) - val substs' = ListPair.zip (vars, map ctm_of tms) - val _ = trace_msg (fn () => - cat_lines ("subst_translations:" :: - (substs' |> map (fn (x, y) => - Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^ - Syntax.string_of_term ctxt (term_of y))))); - in cterm_instantiate substs' i_th end - handle THM (msg, _, _) => - error ("Cannot replay Metis proof in Isabelle:\n" ^ msg) - -(* INFERENCE RULE: RESOLVE *) - -(* Like RSN, but we rename apart only the type variables. Vars here typically - have an index of 1, and the use of RSN would increase this typically to 3. - Instantiations of those Vars could then fail. See comment on "mk_var". *) -fun resolve_inc_tyvars thy tha i thb = - let - val tha = Drule.incr_type_indexes (1 + Thm.maxidx_of thb) tha - fun aux tha thb = - case Thm.bicompose false (false, tha, nprems_of tha) i thb - |> Seq.list_of |> distinct Thm.eq_thm of - [th] => th - | _ => raise THM ("resolve_inc_tyvars: unique result expected", i, - [tha, thb]) - in - aux tha thb - handle TERM z => - (* The unifier, which is invoked from "Thm.bicompose", will sometimes - refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a - "TERM" exception (with "add_ffpair" as first argument). We then - perform unification of the types of variables by hand and try - again. We could do this the first time around but this error - occurs seldom and we don't want to break existing proofs in subtle - ways or slow them down needlessly. *) - case [] |> fold (Term.add_vars o prop_of) [tha, thb] - |> AList.group (op =) - |> maps (fn ((s, _), T :: Ts) => - map (fn T' => (Free (s, T), Free (s, T'))) Ts) - |> rpair (Envir.empty ~1) - |-> fold (Pattern.unify thy) - |> Envir.type_env |> Vartab.dest - |> map (fn (x, (S, T)) => - pairself (ctyp_of thy) (TVar (x, S), T)) of - [] => raise TERM z - | ps => aux (instantiate (ps, []) tha) (instantiate (ps, []) thb) - end - -fun mk_not (Const (@{const_name Not}, _) $ b) = b - | mk_not b = HOLogic.mk_not b - -(* Match untyped terms. *) -fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b) - | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b) - | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) = - (a = b) (* The index is ignored, for some reason. *) - | untyped_aconv (Bound i) (Bound j) = (i = j) - | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u - | untyped_aconv (t1 $ t2) (u1 $ u2) = - untyped_aconv t1 u1 andalso untyped_aconv t2 u2 - | untyped_aconv _ _ = false - -(* Finding the relative location of an untyped term within a list of terms *) -fun literal_index lit = - let - val lit = Envir.eta_contract lit - fun get _ [] = raise Empty - | get n (x :: xs) = - if untyped_aconv lit (Envir.eta_contract (HOLogic.dest_Trueprop x)) then - n - else - get (n+1) xs - in get 1 end - -(* Permute a rule's premises to move the i-th premise to the last position. *) -fun make_last i th = - let val n = nprems_of th - in if 1 <= i andalso i <= n - then Thm.permute_prems (i-1) 1 th - else raise THM("select_literal", i, [th]) - end; - -(* Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing - double-negations. *) -val negate_head = rewrite_rule [@{thm atomize_not}, not_not RS eq_reflection] - -(* Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P *) -val select_literal = negate_head oo make_last - -fun resolve_inf ctxt mode old_skolems thpairs atm th1 th2 = - let - val thy = ProofContext.theory_of ctxt - val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2 - val _ = trace_msg (fn () => " isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1) - val _ = trace_msg (fn () => " isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2) - in - (* Trivial cases where one operand is type info *) - if Thm.eq_thm (TrueI, i_th1) then - i_th2 - else if Thm.eq_thm (TrueI, i_th2) then - i_th1 - else - let - val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems) - (Metis_Term.Fn atm) - val _ = trace_msg (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm) - val prems_th1 = prems_of i_th1 - val prems_th2 = prems_of i_th2 - val index_th1 = literal_index (mk_not i_atm) prems_th1 - handle Empty => raise Fail "Failed to find literal in th1" - val _ = trace_msg (fn () => " index_th1: " ^ Int.toString index_th1) - val index_th2 = literal_index i_atm prems_th2 - handle Empty => raise Fail "Failed to find literal in th2" - val _ = trace_msg (fn () => " index_th2: " ^ Int.toString index_th2) - in - resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2 - end - end; - -(* INFERENCE RULE: REFL *) - -val REFL_THM = Thm.incr_indexes 2 @{lemma "t ~= t ==> False" by simp} - -val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) []))); -val refl_idx = 1 + Thm.maxidx_of REFL_THM; - -fun refl_inf ctxt mode old_skolems t = - let val thy = ProofContext.theory_of ctxt - val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t - val _ = trace_msg (fn () => " term: " ^ Syntax.string_of_term ctxt i_t) - val c_t = cterm_incr_types thy refl_idx i_t - in cterm_instantiate [(refl_x, c_t)] REFL_THM end; - -(* INFERENCE RULE: EQUALITY *) - -val subst_em = @{lemma "s = t ==> P s ==> ~ P t ==> False" by simp} -val ssubst_em = @{lemma "s = t ==> P t ==> ~ P s ==> False" by simp} - -val metis_eq = Metis_Term.Fn ("=", []); - -fun get_ty_arg_size _ (Const (@{const_name HOL.eq}, _)) = 0 (*equality has no type arguments*) - | get_ty_arg_size thy (Const (c, _)) = (num_type_args thy c handle TYPE _ => 0) - | get_ty_arg_size _ _ = 0; - -fun equality_inf ctxt mode old_skolems (pos, atm) fp fr = - let val thy = ProofContext.theory_of ctxt - val m_tm = Metis_Term.Fn atm - val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr] - val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos) - fun replace_item_list lx 0 (_::ls) = lx::ls - | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls - fun path_finder_FO tm [] = (tm, Bound 0) - | path_finder_FO tm (p::ps) = - let val (tm1,args) = strip_comb tm - val adjustment = get_ty_arg_size thy tm1 - val p' = if adjustment > p then p else p-adjustment - val tm_p = List.nth(args,p') - handle Subscript => - error ("Cannot replay Metis proof in Isabelle:\n" ^ - "equality_inf: " ^ Int.toString p ^ " adj " ^ - Int.toString adjustment ^ " term " ^ - Syntax.string_of_term ctxt tm) - val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^ - " " ^ Syntax.string_of_term ctxt tm_p) - val (r,t) = path_finder_FO tm_p ps - in - (r, list_comb (tm1, replace_item_list t p' args)) - end - fun path_finder_HO tm [] = (tm, Bound 0) - | path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps) - | path_finder_HO (t$u) (_::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps) - | path_finder_HO tm ps = - raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ - "equality_inf, path_finder_HO: path = " ^ - space_implode " " (map Int.toString ps) ^ - " isa-term: " ^ Syntax.string_of_term ctxt tm) - fun path_finder_FT tm [] _ = (tm, Bound 0) - | path_finder_FT tm (0::ps) (Metis_Term.Fn ("ti", [t1, _])) = - path_finder_FT tm ps t1 - | path_finder_FT (t$u) (0::ps) (Metis_Term.Fn (".", [t1, _])) = - (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1) - | path_finder_FT (t$u) (1::ps) (Metis_Term.Fn (".", [_, t2])) = - (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2) - | path_finder_FT tm ps t = - raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ - "equality_inf, path_finder_FT: path = " ^ - space_implode " " (map Int.toString ps) ^ - " isa-term: " ^ Syntax.string_of_term ctxt tm ^ - " fol-term: " ^ Metis_Term.toString t) - fun path_finder FO tm ps _ = path_finder_FO tm ps - | path_finder HO (tm as Const(@{const_name HOL.eq},_) $ _ $ _) (p::ps) _ = - (*equality: not curried, as other predicates are*) - if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*) - else path_finder_HO tm (p::ps) (*1 selects second operand*) - | path_finder HO tm (_ :: ps) (Metis_Term.Fn ("{}", [_])) = - path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*) - | path_finder FT (tm as Const(@{const_name HOL.eq}, _) $ _ $ _) (p::ps) - (Metis_Term.Fn ("=", [t1,t2])) = - (*equality: not curried, as other predicates are*) - if p=0 then path_finder_FT tm (0::1::ps) - (Metis_Term.Fn (".", [Metis_Term.Fn (".", [metis_eq,t1]), t2])) - (*select first operand*) - else path_finder_FT tm (p::ps) - (Metis_Term.Fn (".", [metis_eq,t2])) - (*1 selects second operand*) - | path_finder FT tm (_ :: ps) (Metis_Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1 - (*if not equality, ignore head to skip the hBOOL predicate*) - | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*) - fun path_finder_lit ((nt as Const (@{const_name Not}, _)) $ tm_a) idx = - let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm - in (tm, nt $ tm_rslt) end - | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm - val (tm_subst, body) = path_finder_lit i_atm fp - val tm_abs = Abs ("x", type_of tm_subst, body) - val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs) - val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm) - val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst) - val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*) - val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em) - val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst') - val eq_terms = map (pairself (cterm_of thy)) - (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm])) - in cterm_instantiate eq_terms subst' end; - -val factor = Seq.hd o distinct_subgoals_tac; - -fun step ctxt mode old_skolems thpairs p = - case p of - (fol_th, Metis_Proof.Axiom _) => factor (axiom_inf thpairs fol_th) - | (_, Metis_Proof.Assume f_atm) => assume_inf ctxt mode old_skolems f_atm - | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => - factor (inst_inf ctxt mode old_skolems thpairs f_subst f_th1) - | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) => - factor (resolve_inf ctxt mode old_skolems thpairs f_atm f_th1 f_th2) - | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems f_tm - | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => - equality_inf ctxt mode old_skolems f_lit f_p f_r - -fun flexflex_first_order th = - case Thm.tpairs_of th of - [] => th - | pairs => - let val thy = theory_of_thm th - val (_, tenv) = - fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) - val t_pairs = map Meson.term_pair_of (Vartab.dest tenv) - val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th - in th' end - handle THM _ => th; - -fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s) -fun is_isabelle_literal_genuine t = - case t of _ $ (Const (@{const_name skolem}, _) $ _) => false | _ => true - -fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0 - -fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs = - let - val _ = trace_msg (fn () => "=============================================") - val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th) - val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf) - val th = step ctxt mode old_skolems thpairs (fol_th, inf) - |> flexflex_first_order - val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th) - val _ = trace_msg (fn () => "=============================================") - val num_metis_lits = - fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList - |> count is_metis_literal_genuine - val num_isabelle_lits = - th |> prems_of |> count is_isabelle_literal_genuine - val _ = if num_metis_lits = num_isabelle_lits then () - else error "Cannot replay Metis proof in Isabelle: Out of sync." - in (fol_th, th) :: thpairs end - -end;