(* ID: $Id$
Author: Claire Quigley
Copyright 2004 University of Cambridge
*)
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);
Goal "False ==> False";
by Auto_tac;
qed "False_imp";
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
| 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)
| Rewrite of (int * int) * (int * int)
| Obvious 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 lit_string_with_nums t = let val termstr = Term.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 = valOf (assoc (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) (valOf (assoc (thml,clause1)))
val thm2 = valOf (assoc (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) (valOf (assoc (thml,clause1)))
val thm2 = valOf (assoc (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 *)
(*************************************)
(*FIXME: share code with that in Tools/reconstruction.ML*)
fun follow_factor clause lit1 lit2 allvars thml clause_strs =
let
val th = valOf (assoc (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 = valOf (assoc (thml,clause1))
val th2 = valOf (assoc (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"
(*
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs=
let
val th1 = valOf (assoc (thml,clause1))
val th2 = valOf (assoc (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_nead newth
val (res, numlist, symlist, nsymlist) = (rearrange_clause newth' clause_strs allvars)
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 = valOf (assoc (thml,clause1))
val th2 = valOf (assoc (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 = Sign.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 = valOf (assoc (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 _ _ =
raise ASSERTION "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
val recon_step = (recon_fun)
in
(((clause_num, thm)::thml), ((clause_num,recon_step)::recons))
end
(***************************************************************)
(* follow through the res. proof, creating an Isabelle theorem *)
(***************************************************************)
(*fun is_proof_char ch = (case ch of
"(" => true
| ")" => true
| ":" => true
| "'" => true
| "&" => true
| "|" => true
| "~" => true
| "." => true
|(is_alpha ) => true
|(is_digit) => true
| _ => false)*)
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 not_newline ch = not (ch = "\n");
(*
fun follow clauses [] allvars thml recons =
let (* val _ = reset show_sorts*)
val thmstring = Meson.concat_with_and (map string_of_thm (map snd thml))
val thmproofstring = proofstring ( thmstring)
val no_returns =List.filter not_newline ( thmproofstring)
val thmstr = implode no_returns
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thml_file")))
val _ = TextIO.output(outfile, "thmstr is "^thmstr)
val _ = TextIO.flushOut outfile;
val _ = TextIO.closeOut outfile
(*val _ = set show_sorts*)
in
((snd( hd thml)), 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
*)
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 *)
fun first_pair (a,b,c) = (a,b);
fun second_pair (a,b,c) = (b,c);
(* 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
fun remove_tinfo [] = []
| remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) =
(clausenum, step , newstrs)::(remove_tinfo xs)