(* ID: $Id: recon_translate_proof.ML,v 1.22 2005/09/19 16:30:23 paulson Exp $ Author: Claire Quigley Copyright 2004 University of Cambridge *) structure ReconTranslateProof = struct fun add_in_order (x:string) [] = [x] | add_in_order (x:string) ((y:string)::ys) = if (x < y) then (x::(y::ys)) else (y::(add_in_order x ys)) fun add_once x [] = [x] | add_once x (y::ys) = if x mem (y::ys) then (y::ys) else add_in_order x (y::ys) fun thm_vars thm = map (fn ((name,ix),_) => name) (Drule.vars_of thm); exception Reflex_equal; (********************************) (* Proofstep datatype *) (********************************) (* Assume rewrite steps have only two clauses in them just now, but lcl109-5 has Rew[5,3,5,3] *) datatype Side = Left |Right datatype Proofstep = ExtraAxiom | OrigAxiom | VampInput | Axiom | Binary of (int * int) * (int * int) (* (clause1,lit1), (clause2, lit2) *) | MRR of (int * int) * (int * int) | Factor of (int * int * int) (* (clause,lit1, lit2) *) | Para of (int * int) * (int * int) | Super_l of (int * int) * (int * int) | Super_r of (int * int) * (int * int) (*| Rewrite of (int * int) * (int * int) *) | Rewrite of (int * int) list | SortSimp of (int * int) * (int * int) | UnitConf of (int * int) * (int * int) | Obvious of (int * int) | AED of (int*int) | EqualRes of (int*int) | Condense of (int*int) (*| Hyper of int list*) | Unusedstep of unit datatype Clausesimp = Binary_s of int * int | Factor_s of unit | Demod_s of (int * int) list | Hyper_s of int list | Unusedstep_s of unit datatype Step_label = T_info |P_info fun is_alpha_space_digit_or_neg ch = (ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse (ReconOrderClauses.is_digit ch) orelse ( ch = " "); fun string_of_term (Const(s,_)) = s | string_of_term (Free(s,_)) = s | string_of_term (Var(ix,_)) = Term.string_of_vname ix | string_of_term (Bound i) = string_of_int i | string_of_term (Abs(x,_,t)) = "%" ^ x ^ ". " ^ string_of_term t | string_of_term (s $ t) = "(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")" fun lit_string_with_nums t = let val termstr = string_of_term t val exp_term = explode termstr in implode(List.filter is_alpha_space_digit_or_neg exp_term) end fun reconstruction_failed fname = error (fname ^ ": reconstruction failed") (************************************************) (* Reconstruct an axiom resolution step *) (* clauses is a list of (clausenum,clause) pairs*) (************************************************) fun follow_axiom clauses allvars (clausenum:int) thml clause_strs = let val this_axiom = (the o AList.lookup (op =) clauses) clausenum val (res, numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause this_axiom clause_strs allvars) val thmvars = thm_vars res in (res, (Axiom,clause_strs,thmvars ) ) end handle Option => reconstruction_failed "follow_axiom" (****************************************) (* Reconstruct a binary resolution step *) (****************************************) (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *) fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs = let val thm1 = select_literal (lit1 + 1) ((the o AList.lookup (op =) thml) clause1) val thm2 = (the o AList.lookup (op =) thml) clause2 val res = thm1 RSN ((lit2 +1), thm2) val (res', numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause res clause_strs allvars) val thmvars = thm_vars res in (res', ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) ) end handle Option => reconstruction_failed "follow_binary" (******************************************************) (* Reconstruct a matching replacement resolution step *) (******************************************************) fun follow_mrr ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs = let val thm1 = select_literal (lit1 + 1) ((the o AList.lookup (op =) thml) clause1) val thm2 = (the o AList.lookup (op =) thml) clause2 val res = thm1 RSN ((lit2 +1), thm2) val (res', numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause res clause_strs allvars) val thmvars = thm_vars res in (res', ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars)) end handle Option => reconstruction_failed "follow_mrr" (*******************************************) (* Reconstruct a factoring resolution step *) (*******************************************) fun mksubstlist [] sublist = sublist |mksubstlist ((a, (_, b)) :: rest) sublist = let val vartype = type_of b val avar = Var(a,vartype) val newlist = ((avar,b)::sublist) in mksubstlist rest newlist end; (* based on Tactic.distinct_subgoals_tac *) fun delete_assump_tac state lit = let val (frozth,thawfn) = freeze_thaw state val froz_prems = cprems_of frozth val assumed = implies_elim_list frozth (map assume froz_prems) val new_prems = ReconOrderClauses.remove_nth lit froz_prems val implied = implies_intr_list new_prems assumed in Seq.single (thawfn implied) end (*************************************) (* Reconstruct a factoring step *) (*************************************) fun getnewenv seq = fst (fst (the (Seq.pull seq))); (*FIXME: share code with that in Tools/reconstruction.ML*) fun follow_factor clause lit1 lit2 allvars thml clause_strs = let val th = (the o AList.lookup (op =) thml) clause val prems = prems_of th val sign = sign_of_thm th val fac1 = ReconOrderClauses.get_nth (lit1+1) prems val fac2 = ReconOrderClauses.get_nth (lit2+1) prems val unif_env = Unify.unifiers (sign,Envir.empty 0, [(fac1, fac2)]) val newenv = getnewenv unif_env val envlist = Envir.alist_of newenv val (t1,t2)::_ = mksubstlist envlist [] in if (is_Var t1) then let val str1 = lit_string_with_nums t1; val str2 = lit_string_with_nums t2; val facthm = read_instantiate [(str1,str2)] th; val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1))) val (res', numlist, symlist, nsymlist) = ReconOrderClauses.rearrange_clause res clause_strs allvars val thmvars = thm_vars res' in (res',((Factor (clause, lit1, lit2)),clause_strs,thmvars)) end else let val str2 = lit_string_with_nums t1; val str1 = lit_string_with_nums t2; val facthm = read_instantiate [(str1,str2)] th; val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1))) val (res', numlist, symlist, nsymlist) = ReconOrderClauses.rearrange_clause res clause_strs allvars val thmvars = thm_vars res' in (res', ((Factor (clause, lit1, lit2)),clause_strs, thmvars)) end end handle Option => reconstruction_failed "follow_factor" fun get_unif_comb t eqterm = if ((type_of t) = (type_of eqterm)) then t else let val _ $ rand = t in get_unif_comb rand eqterm end; fun get_unif_lit t eqterm = if (can HOLogic.dest_eq t) then let val (lhs,rhs) = HOLogic.dest_eq(HOLogic.dest_Trueprop eqterm) in lhs end else get_unif_comb t eqterm; (*************************************) (* Reconstruct a paramodulation step *) (*************************************) val rev_subst = rotate_prems 1 subst; val rev_ssubst = rotate_prems 1 ssubst; fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs = let val th1 = (the o AList.lookup (op =) thml) clause1 val th2 = (the o AList.lookup (op =) thml) clause2 val eq_lit_th = select_literal (lit1+1) th1 val mod_lit_th = select_literal (lit2+1) th2 val eqsubst = eq_lit_th RSN (2,rev_subst) val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) val newth' =negate_head newth val (res, numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause newth' clause_strs allvars handle Not_in_list => let val mod_lit_th' = mod_lit_th RS not_sym val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst) val newth' =negate_head newth in ReconOrderClauses.rearrange_clause newth' clause_strs allvars end) val thmvars = thm_vars res in (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars)) end handle Option => reconstruction_failed "follow_standard_para" (********************************) (* Reconstruct a rewriting step *) (********************************) (* val rev_subst = rotate_prems 1 subst; fun paramod_rule ((cl1, lit1), (cl2 , lit2)) = let val eq_lit_th = select_literal (lit1+1) cl1 val mod_lit_th = select_literal (lit2+1) cl2 val eqsubst = eq_lit_th RSN (2,rev_subst) val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) in Meson.negated_asm_of_head newth end; val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) val mod_lit_th' = mod_lit_th RS not_sym *) fun delete_assumps 0 th = th | delete_assumps n th = let val th_prems = length (prems_of th) val th' = hd (Seq.list_of(delete_assump_tac th (th_prems -1))) in delete_assumps (n-1) th' end (* extra conditions from the equality turn up as 2nd to last literals of result. Need to delete them *) (* changed negate_nead to negate_head here too*) (* clause1, lit1 is thing to rewrite with *) (*fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs = let val th1 = (the o AList.lookup (op =) thml) clause1 val th2 = (the o AList.lookup (op =) thml) clause2 val eq_lit_th = select_literal (lit1+1) th1 val mod_lit_th = select_literal (lit2+1) th2 val eqsubst = eq_lit_th RSN (2,rev_subst) val eq_lit_prem_num = length (prems_of eq_lit_th) val sign = Theory.merge (sign_of_thm th1, sign_of_thm th2) val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) val newthm = negate_head newth val newthm' = delete_assumps eq_lit_prem_num newthm val (res, numlist, symlist, nsymlist) = ReconOrderClauses.rearrange_clause newthm clause_strs allvars val thmvars = thm_vars res in (res, ((Rewrite ((clause1, lit1), (clause2, lit2))),clause_strs,thmvars)) end handle Option => reconstruction_failed "follow_rewrite" *) (*****************************************) (* Reconstruct an obvious reduction step *) (*****************************************) fun follow_obvious (clause1, lit1) allvars thml clause_strs = let val th1 = (the o AList.lookup (op =) thml) clause1 val prems1 = prems_of th1 val newthm = refl RSN ((lit1+ 1), th1) handle THM _ => hd (Seq.list_of(delete_assump_tac th1 (lit1 + 1))) val (res, numlist, symlist, nsymlist) = ReconOrderClauses.rearrange_clause newthm clause_strs allvars val thmvars = thm_vars res in (res, ((Obvious (clause1, lit1)),clause_strs,thmvars)) end handle Option => reconstruction_failed "follow_obvious" (**************************************************************************************) (* reconstruct a single line of the res. proof - depending on what sort of proof step it was*) (**************************************************************************************) fun follow_proof clauses allvars clausenum thml (Axiom ) clause_strs = follow_axiom clauses allvars clausenum thml clause_strs | follow_proof clauses allvars clausenum thml (Binary (a, b)) clause_strs = follow_binary (a, b) allvars thml clause_strs | follow_proof clauses allvars clausenum thml (MRR (a, b)) clause_strs = follow_mrr (a, b) allvars thml clause_strs | follow_proof clauses allvars clausenum thml (Factor (a, b, c)) clause_strs = follow_factor a b c allvars thml clause_strs | follow_proof clauses allvars clausenum thml (Para (a, b)) clause_strs = follow_standard_para (a, b) allvars thml clause_strs (* | follow_proof clauses allvars clausenum thml (Rewrite (a,b)) clause_strs = follow_rewrite (a,b) allvars thml clause_strs*) | follow_proof clauses allvars clausenum thml (Obvious (a,b)) clause_strs = follow_obvious (a,b) allvars thml clause_strs (*| follow_proof clauses clausenum thml (Hyper l) = follow_hyper l thml*) | follow_proof clauses allvars clausenum thml _ _ = error "proof step not implemented" (**************************************************************************************) (* reconstruct a single line of the res. proof - at the moment do only inference steps*) (**************************************************************************************) fun follow_line clauses allvars thml (clause_num, proof_step, clause_strs) recons = let val (thm, recon_fun) = follow_proof clauses allvars clause_num thml proof_step clause_strs in ((clause_num, thm)::thml, (clause_num,recon_fun)::recons) end (***************************************************************) (* follow through the res. proof, creating an Isabelle theorem *) (***************************************************************) fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126)) orelse (ch = " ") fun proofstring x = let val exp = explode x in List.filter (is_proof_char ) exp end fun replace_clause_strs [] recons newrecons = (newrecons) | replace_clause_strs ((thmnum, thm)::thml) ((clausenum,(step,clause_strs,thmvars))::recons) newrecons = let val new_clause_strs = ReconOrderClauses.get_meta_lits_bracket thm in replace_clause_strs thml recons ((clausenum,(step,new_clause_strs,thmvars))::newrecons) end fun follow clauses [] allvars thml recons = let val new_recons = replace_clause_strs thml recons [] in (#2(hd thml), new_recons) end | follow clauses (h::t) allvars thml recons = let val (thml', recons') = follow_line clauses allvars thml h recons val (thm, recons_list) = follow clauses t allvars thml' recons' in (thm,recons_list) end (* Assume we have the cnf clauses as a list of (clauseno, clause) *) (* and the proof as a list of the proper datatype *) (* take the cnf clauses of the goal and the proof from the res. prover *) (* as a list of type Proofstep and return the thm goal ==> False *) (* takes original axioms, proof_steps parsed from spass, variables *) fun translate_proof clauses proof allvars = let val (thm, recons) = follow clauses proof allvars [] [] in (thm, (recons)) end end;