# HG changeset patch # User blanchet # Date 1307385395 -7200 # Node ID 38ef5a2b000c6253ebb3807e99f2eb336ce52d86 # Parent 697d32fa183da1bddc1c974fc246cb50b06aad09 tuning diff -r 697d32fa183d -r 38ef5a2b000c src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Mon Jun 06 20:36:35 2011 +0200 @@ -79,7 +79,7 @@ (* 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. *) + often fails otherwise. See also "axiom_inference" below. *) fun make_var (w, T) = Var ((w, 1), T) (*Remove the "apply" operator from an HO term*) @@ -285,7 +285,7 @@ (* This causes variables to have an index of 1 by default. See also "make_var" above. *) -fun axiom_inf th_pairs th = Thm.incr_indexes 1 (lookth th_pairs th) +fun axiom_inference th_pairs th = Thm.incr_indexes 1 (lookth th_pairs th) (* INFERENCE RULE: ASSUME *) @@ -297,7 +297,7 @@ 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 sym_tab atm = +fun assume_inference ctxt mode old_skolems sym_tab atm = inst_excluded_middle (Proof_Context.theory_of ctxt) (singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab) @@ -308,7 +308,7 @@ 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 sym_tab th_pairs fsubst th = +fun inst_inference ctxt mode old_skolems sym_tab th_pairs fsubst th = let val thy = Proof_Context.theory_of ctxt val i_th = lookth th_pairs th val i_th_vars = Term.add_vars (prop_of i_th) [] @@ -345,8 +345,8 @@ 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, _, _) => raise METIS ("inst_inf", msg) - | ERROR msg => raise METIS ("inst_inf", msg) + handle THM (msg, _, _) => raise METIS ("inst_inference", msg) + | ERROR msg => raise METIS ("inst_inference", msg) (* INFERENCE RULE: RESOLVE *) @@ -433,7 +433,7 @@ (* 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 sym_tab th_pairs atm th1 th2 = +fun resolve_inference ctxt mode old_skolems sym_tab th_pairs atm th1 th2 = let val thy = Proof_Context.theory_of ctxt val (i_th1, i_th2) = pairself (lookth th_pairs) (th1, th2) @@ -463,7 +463,7 @@ val _ = trace_msg ctxt (fn () => " index_th2: " ^ string_of_int index_th2) in resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2 - handle TERM (s, _) => raise METIS ("resolve_inf", s) + handle TERM (s, _) => raise METIS ("resolve_inference", s) end end; @@ -474,7 +474,7 @@ 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 sym_tab t = +fun refl_inference ctxt mode old_skolems sym_tab t = let val thy = Proof_Context.theory_of ctxt val i_t = singleton (hol_terms_from_metis ctxt mode old_skolems sym_tab) t @@ -495,7 +495,7 @@ (num_type_args thy s handle TYPE _ => 0) | get_ty_arg_size _ _ = 0 -fun equality_inf ctxt mode old_skolems sym_tab (pos, atm) fp fr = +fun equality_inference ctxt mode old_skolems sym_tab (pos, atm) fp fr = let val thy = Proof_Context.theory_of ctxt val m_tm = Metis_Term.Fn atm val [i_atm, i_tm] = @@ -505,7 +505,7 @@ | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls fun path_finder_fail mode tm ps t = raise Fail ("Cannot replay Metis proof in Isabelle:\n" ^ - "equality_inf, path_finder_" ^ string_of_mode mode ^ + "equality_inference, path_finder_" ^ string_of_mode mode ^ ": path = " ^ space_implode " " (map string_of_int ps) ^ " isa-term: " ^ Syntax.string_of_term ctxt tm ^ (case t of @@ -518,7 +518,7 @@ val p' = if adjustment > p then p else p - adjustment val tm_p = nth args p' handle Subscript => - raise METIS ("equality_inf", + raise METIS ("equality_inference", string_of_int p ^ " adj " ^ string_of_int adjustment ^ " term " ^ Syntax.string_of_term ctxt tm) @@ -614,17 +614,19 @@ fun one_step ctxt mode old_skolems sym_tab th_pairs p = case p of - (fol_th, Metis_Proof.Axiom _) => axiom_inf th_pairs fol_th |> factor + (fol_th, Metis_Proof.Axiom _) => axiom_inference th_pairs fol_th |> factor | (_, Metis_Proof.Assume f_atm) => - assume_inf ctxt mode old_skolems sym_tab f_atm + assume_inference ctxt mode old_skolems sym_tab f_atm | (_, Metis_Proof.Metis_Subst (f_subst, f_th1)) => - inst_inf ctxt mode old_skolems sym_tab th_pairs f_subst f_th1 |> factor + inst_inference ctxt mode old_skolems sym_tab th_pairs f_subst f_th1 + |> factor | (_, Metis_Proof.Resolve(f_atm, f_th1, f_th2)) => - resolve_inf ctxt mode old_skolems sym_tab th_pairs f_atm f_th1 f_th2 + resolve_inference ctxt mode old_skolems sym_tab th_pairs f_atm f_th1 f_th2 |> factor - | (_, Metis_Proof.Refl f_tm) => refl_inf ctxt mode old_skolems sym_tab f_tm + | (_, Metis_Proof.Refl f_tm) => + refl_inference ctxt mode old_skolems sym_tab f_tm | (_, Metis_Proof.Equality (f_lit, f_p, f_r)) => - equality_inf ctxt mode old_skolems sym_tab f_lit f_p f_r + equality_inference ctxt mode old_skolems sym_tab f_lit f_p f_r fun flexflex_first_order th = case Thm.tpairs_of th of