# HG changeset patch # User paulson # Date 1113229531 -7200 # Node ID 681bcb7f03892d1f0a9f2053dcd50f0a3e282174 # Parent 1da4ce092c0be458e662f545d063bdc4f993913f removal of Main and other tidying up diff -r 1da4ce092c0b -r 681bcb7f0389 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Apr 11 12:34:34 2005 +0200 +++ b/src/HOL/IsaMakefile Mon Apr 11 16:25:31 2005 +0200 @@ -115,7 +115,7 @@ Tools/res_lib.ML Tools/res_clause.ML Tools/res_skolem_function.ML\ Tools/res_axioms.ML Tools/res_types_sorts.ML \ Tools/ATP/recon_prelim.ML Tools/ATP/recon_gandalf_base.ML Tools/ATP/recon_order_clauses.ML\ - Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML Tools/ATP/recon_reconstruct_proof.ML \ + Tools/ATP/recon_translate_proof.ML Tools/ATP/recon_parse.ML \ Tools/ATP/recon_transfer_proof.ML Tools/ATP/res_clasimpset.ML \ Tools/ATP/VampireCommunication.ML Tools/ATP/SpassCommunication.ML Tools/ATP/modUnix.ML \ Tools/ATP/watcher.sig Tools/ATP/watcher.ML Tools/res_atp.ML\ diff -r 1da4ce092c0b -r 681bcb7f0389 src/HOL/Tools/ATP/recon_order_clauses.ML --- a/src/HOL/Tools/ATP/recon_order_clauses.ML Mon Apr 11 12:34:34 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Mon Apr 11 16:25:31 2005 +0200 @@ -3,8 +3,6 @@ (*----------------------------------------------*) (* Reorder clauses for use in binary resolution *) (*----------------------------------------------*) -fun take n [] = [] -| take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs))) fun drop n [] = [] | drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs) @@ -13,7 +11,7 @@ | remove n (x::xs) = List.filter (not_equal n) (x::xs); fun remove_nth n [] = [] -| remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs)) +| remove_nth n xs = (List.take (xs, n-1)) @ (List.drop (xs, n)) fun get_nth n (x::xs) = hd (drop (n-1) (x::xs)) @@ -28,21 +26,6 @@ exception Not_in_list; - - - - (* get the literals from a disjunctive clause *) - -(*fun get_disj_literals t = if is_disj t then - let - val {disj1, disj2} = dest_disj t - in - disj1::(get_disj_literals disj2) - end - else - ([t]) - -*) (* (* gives horn clause with kth disj as concl (starting at 1) *) @@ -99,22 +82,6 @@ exception Not_in_list; -(*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("make_last", i, [th]) - end; - -(*Maps a rule that ends "... ==> P ==> False" to "... ==> ~P" while suppressing - double-negations.*) -val negate_head = rewrite_rule [atomize_not, not_not RS eq_reflection]; - -(*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*) -fun select_literal i cl = negate_head (make_last i cl); - - (* get a meta-clause for resolution with correct order of literals *) fun get_meta_cl (th,n) = let val lits = nliterals(prop_of th) val contra = if lits = 1 @@ -133,10 +100,6 @@ - - - - fun zip xs [] = [] | zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys)) @@ -381,14 +344,6 @@ *) - - - - - - - - (* checkorder Spass Isabelle [] *) fun checkorder [] strlist allvars (numlist, symlist, not_symlist)= (numlist,symlist, not_symlist) diff -r 1da4ce092c0b -r 681bcb7f0389 src/HOL/Tools/ATP/recon_reconstruct_proof.ML --- a/src/HOL/Tools/ATP/recon_reconstruct_proof.ML Mon Apr 11 12:34:34 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,308 +0,0 @@ - - -(****************************************) -(* Reconstruct an axiom resolution step *) -(****************************************) - - fun reconstruct_axiom clauses (clausenum:int) thml (numlist, symlist, nsymlist ) = - let val this_axiom =(assoc clausenum clauses) - val symmed = (apply_rule sym symlist this_axiom) - val nsymmed = (apply_rule not_sym nsymlist symmed ) - in - rearrange_prems numlist nsymmed - end - -(****************************************) -(* Reconstruct a binary resolution step *) -(****************************************) - -fun reconstruct_binary ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist ) - = let - val thm1 = select_literal (lit1 + 1) (assoc clause1 thml) - val thm2 = assoc clause2 thml - val res = thm1 RSN ((lit2 +1), thm2) - val symmed = (apply_rule sym symlist res) - val nsymmed = (apply_rule not_sym nsymlist symmed ) - in - rearrange_prems numlist nsymmed - end - - -(****************************************) -(* Reconstruct a binary resolution step *) -(****************************************) - -fun reconstruct_mrr ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist ) - = let - val thm1 = select_literal (lit1 + 1) (assoc clause1 thml) - val thm2 = assoc clause2 thml - val res = thm1 RSN ((lit2 +1), thm2) - val symmed = (apply_rule sym symlist res) - val nsymmed = (apply_rule not_sym nsymlist symmed ) - in - rearrange_prems numlist nsymmed - end - -(*******************************************) -(* Reconstruct a factoring resolution step *) -(*******************************************) - -fun reconstruct_factor (clause, lit1, lit2) thml (numlist, symlist, nsymlist )= - let - val th = assoc clause thml - val prems = prems_of th - val fac1 = get_nth (lit1+1) prems - val fac2 = get_nth (lit2+1) prems - val unif_env = unifiers (Mainsign,Envir.empty 0, [(fac1, fac2)]) - val newenv = getnewenv unif_env - val envlist = alist_of newenv - - val newsubsts = mksubstlist envlist [] - in - if (is_Var (fst(hd(newsubsts)))) - then - let - val str1 = lit_string_with_nums (fst (hd newsubsts)); - val str2 = lit_string_with_nums (snd (hd newsubsts)); - val facthm = read_instantiate [(str1,str2)] th; - val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1))) - val symmed = (apply_rule sym symlist res) - val nsymmed = (apply_rule not_sym nsymlist symmed ) - - in - rearrange_prems numlist nsymmed - end - else - let - val str2 = lit_string_with_nums (fst (hd newsubsts)); - val str1 = lit_string_with_nums (snd (hd newsubsts)); - val facthm = read_instantiate [(str1,str2)] th; - val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1))) - val symmed = (apply_rule sym symlist res) - val nsymmed = (apply_rule not_sym nsymlist symmed ) - in - rearrange_prems numlist nsymmed - end - end; - - -(****************************************) -(* Reconstruct a paramodulation step *) -(****************************************) - - (* clause1, lit1 is thing to rewrite with *) -fun reconstruct_standard_para_left ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist )= - - let - - val newthm = para_left ((clause1, lit1), (clause2 , lit2)) thml - val symmed = (apply_rule sym symlist newthm) - val nsymmed = (apply_rule not_sym nsymlist symmed ) - - in - rearrange_prems numlist nsymmed - end - - - - (* clause1, lit1 is thing to rewrite with *) -fun reconstruct_standard_para_right ((clause1, lit1), (clause2 , lit2)) thml (numlist, symlist, nsymlist )= - - let - - val newthm = para_right ((clause1, lit1), (clause2 , lit2)) thml - val symmed = (apply_rule sym symlist newthm) - val nsymmed = (apply_rule not_sym nsymlist symmed ) - - in - rearrange_prems numlist nsymmed - end - - - - - - - - - (* let - val th1 = assoc clause1 thml - val th2 = assoc clause2 thml - val prems1 = prems_of th1 - val prems2 = prems_of th2 - (* want to get first element of equality *) - - val fac1 = get_nth (lit1+1) prems1 - val {lhs, rhs} = dest_eq(dest_Trueprop fac1) - handle ERR _ => dest_eq(dest_neg (dest_Trueprop fac1)) - (* get other literal involved in the paramodulation *) - val fac2 = get_nth (lit2+1) prems2 - - (* get bit of th2 to unify with lhs of th1 *) - val unif_lit = get_unif_lit (dest_Trueprop fac2) lhs - val unif_env = unifiers (Mainsign,Envir.empty 0, [(unif_lit, lhs)]) - val newenv = getnewenv unif_env - val envlist = alist_of newenv - val newsubsts = mksubstlist envlist [] - (* instantiate th2 with unifiers *) - - val newth1 = - if (is_Var (fst(hd(newsubsts)))) - then - let - val str1 = lit_string_with_nums (fst (hd newsubsts)); - val str2 = lit_string_with_nums (snd (hd newsubsts)); - val facthm = read_instantiate [(str1,str2)] th1 - in - hd (Seq.list_of(distinct_subgoals_tac facthm)) - end - else - let - val str2 = lit_string_with_nums (fst (hd newsubsts)); - val str1 = lit_string_with_nums (snd (hd newsubsts)); - val facthm = read_instantiate [(str1,str2)] th1 - in - hd (Seq.list_of(distinct_subgoals_tac facthm)) - end - (*rewrite th2 with the equality bit of th2 i.e. lit2 *) - val facthm' = select_literal (lit1 + 1) newth1 - val equal_lit = concl_of facthm' - val cterm_eq = cterm_of Mainsign equal_lit - val eq_thm = assume cterm_eq - val meta_eq_thm = mk_meta_eq eq_thm - val newth2= rewrite_rule [meta_eq_thm] th2 - (*thin lit2 from th2 *) - (* get th1 with lit one as concl, then resolve with thin_rl *) - val thm' = facthm' RS thin_rl - (* now resolve th2 with last premise of thm' *) - val newthm = newth2 RSN ((length prems1), thm') - val symmed = (apply_rule sym symlist newthm) - val nsymmed = (apply_rule not_sym nsymlist symmed ) - - in - rearrange_prems numlist nsymmed - end - -*) - - -(********************************************) -(* Reconstruct a rewrite step *) -(********************************************) - - - - - - -(* does rewriting involve every literal in rewritten clause? *) - (* clause1, lit1 is thing to rewrite with *) - -fun reconstruct_rewrite (clause1, lit1, clause2) thml (numlist, symlist, nsymlist )= - - let val th1 = assoc clause1 thml - val th2 = assoc clause2 thml - val eq_lit_th = select_literal (lit1+1) th1 - val equal_lit = concl_of eq_lit_th - val cterm_eq = cterm_of Mainsign equal_lit - val eq_thm = assume cterm_eq - val meta_eq_thm = mk_meta_eq eq_thm - val newth2= rewrite_rule [meta_eq_thm] th2 - val symmed = (apply_rule sym symlist newth2) - val nsymmed = (apply_rule not_sym nsymlist symmed ) - - in - rearrange_prems numlist nsymmed - end - - - -(*****************************************) -(* Reconstruct an obvious reduction step *) -(*****************************************) - - -fun reconstruct_obvious (clause1, lit1) allvars thml clause_strs= - let val th1 = assoc clause1 thml - 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 symmed = (apply_rule sym symlist newthm) - val nsymmed = (apply_rule not_sym nsymlist symmed ) - in - rearrange_prems numlist nsymmed - end - - - -(********************************************************************************************) -(* reconstruct a single step of the res. proof - depending on what sort of proof step it was*) -(********************************************************************************************) - - - fun reconstruct_proof clauses clausenum thml Axiom (numlist, symlist, nsymlist) - = reconstruct_axiom clauses clausenum thml (numlist, symlist, nsymlist) - | reconstruct_proof clauses clausenum thml (Binary (a, b)) (numlist, symlist, nsymlist) - = reconstruct_binary (a, b) thml (numlist, symlist, nsymlist) - | reconstruct_proof clauses clausenum thml (MRR (a, b)) (numlist, symlist, nsymlist) - = reconstruct_mrr (a, b) thml (numlist, symlist, nsymlist) - | reconstruct_proof clauses clausenum thml (Factor (a, b, c)) (numlist, symlist, nsymlist) - = reconstruct_factor (a ,b ,c) thml (numlist, symlist, nsymlist) - | reconstruct_proof clauses clausenum thml (Para (a, b)) (numlist, symlist, nsymlist) - = reconstruct_standard_para (a, b) thml (numlist, symlist, nsymlist) - | reconstruct_proof clauses clausenum thml (Rewrite (a,b,c)) (numlist, symlist, nsymlist) - = reconstruct_rewrite (a,b,c) thml (numlist, symlist, nsymlist) - | reconstruct_proof clauses clausenum thml (Obvious (a,b)) (numlist, symlist, nsymlist) - = reconstruct_obvious (a,b) thml (numlist, symlist, nsymlist) - (*| reconstruct_proof clauses clausenum thml (Hyper l) - = reconstruct_hyper l thml*) - | reconstruct_proof clauses clausenum thml _ _ = - raise ASSERTION "proof step not implemented" - - -(********************************************************************************************) -(* reconstruct a single line of the res. proof - at the moment do only inference steps *) -(********************************************************************************************) - - fun reconstruct_line clauses thml (clause_num, (proof_step, numlist, symlist,nsymlist)) - = let - val thm = reconstruct_proof clauses clause_num thml proof_step (numlist, symlist,nsymlist) - - in - (clause_num, thm)::thml - end - -(********************************************************************) -(* reconstruct through the res. proof, creating an Isabelle theorem *) -(********************************************************************) - - -fun reconstruct clauses [] thml = ((snd( hd thml))) - | reconstruct clauses (h::t) thml - = let - val (thml') = reconstruct_line clauses thml h - val (thm) = reconstruct clauses t thml' - in - (thm) - 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); - -(*************************) -(* reconstruct res proof *) -(*************************) - -fun reconstruct_proof clauses proof - = let val thm = reconstruct clauses proof [] - in - thm - end - diff -r 1da4ce092c0b -r 681bcb7f0389 src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Mon Apr 11 12:34:34 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Mon Apr 11 16:25:31 2005 +0200 @@ -15,7 +15,7 @@ (* Versions that include type information *) fun string_of_thm thm = let val _ = set show_sorts - val str = Sign.string_of_term Mainsign (prop_of thm) + val str = string_of_thm thm val no_returns =List.filter not_newline (explode str) val _ = reset show_sorts in @@ -149,28 +149,6 @@ add_if_not_inlist ys xs (y::newlist) else add_if_not_inlist ys xs (newlist) -(* -fun is_alpha_space_neg_eq_colon ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = ";") orelse( ch = "=") - -(* replace | by ; here *) -fun change_or [] = [] -| change_or (x::xs) = if x = "|" - then - [";"]@(change_or xs) - else (x::(change_or xs)) - - -fun clause_lit_string t = let val termstr = (Sign.string_of_term Mainsign ) t - val exp_term = explode termstr - val colon_term = change_or exp_term - in - implode(List.filter is_alpha_space_neg_eq_colon colon_term) - end - -fun get_clause_lits thm = clause_lit_string (prop_of thm) -*) - - fun onestr [] str = str | onestr (x::xs) str = onestr xs (str^(concat x)) @@ -181,83 +159,10 @@ | onelist (x::xs) newlist = onelist xs (newlist@x) -(**** Code to support ordinary resolution, rather than Model Elimination ****) - -(*Convert a list of clauses (disjunctions) to meta-level clauses (==>), - with no contrapositives, for ordinary resolution.*) - -(*raises exception if no rules apply -- unlike RL*) -fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) - | tryres (th, []) = raise THM("tryres", 0, [th]); val prop_of = #prop o rep_thm; -(*For ordinary resolution. *) -val resolution_clause_rules = [disj_assoc, make_neg_rule', make_pos_rule']; -(*Use "theorem naming" to label the clauses*) -fun name_thms label = - let fun name1 (th, (k,ths)) = - (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths) - - in fn ths => #2 (foldr name1 (length ths, []) ths) end; - -(*Find an all-negative support clause*) -fun is_negative th = forall (not o #1) (literals (prop_of th)); - -val neg_clauses = List.filter is_negative; - - - -(*True if the given type contains bool anywhere*) -fun has_bool (Type("bool",_)) = true - | has_bool (Type(_, Ts)) = exists has_bool Ts - | has_bool _ = false; - - -(*Create a meta-level Horn clause*) -fun make_horn crules th = make_horn crules (tryres(th,crules)) - handle THM _ => th; - - -(*Raises an exception if any Vars in the theorem mention type bool. That would mean - they are higher-order, and in addition, they could cause make_horn to loop!*) -fun check_no_bool th = - if exists (has_bool o fastype_of) (term_vars (#prop (rep_thm th))) - then raise THM ("check_no_bool", 0, [th]) else th; - - -(*Rules to convert the head literal into a negated assumption. If the head - literal is already negated, then using notEfalse instead of notEfalse' - prevents a double negation.*) -val notEfalse = read_instantiate [("R","False")] notE; -val notEfalse' = rotate_prems 1 notEfalse; - -fun negated_asm_of_head th = - th RS notEfalse handle THM _ => th RS notEfalse'; - -(*Converting one clause*) -fun make_meta_clause th = - negated_asm_of_head (make_horn resolution_clause_rules (check_no_bool th)); - -fun make_meta_clauses ths = - name_thms "MClause#" - (gen_distinct Drule.eq_thm_prop (map make_meta_clause ths)); - -(*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 [atomize_not, not_not RS eq_reflection]; - -(*Maps the clause [P1,...Pn]==>False to [P1,...,P(i-1),P(i+1),...Pn] ==> ~P*) -fun select_literal i cl = negate_head (make_last i cl); fun get_axioms_used proof_steps thmstring = let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr"))) @@ -281,7 +186,7 @@ val distfrees = distinct frees - val metas = map make_meta_clause clauses + val metas = map Meson.make_meta_clause clauses val ax_strs = map #3 axioms (* literals of -all- axioms, not just those used by spass *) diff -r 1da4ce092c0b -r 681bcb7f0389 src/HOL/Tools/ATP/recon_translate_proof.ML --- a/src/HOL/Tools/ATP/recon_translate_proof.ML Mon Apr 11 12:34:34 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Mon Apr 11 16:25:31 2005 +0200 @@ -1,17 +1,4 @@ -fun take n [] = [] -| take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs))) - -fun drop n [] = [] -| drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs) - -fun remove n [] = [] -| remove n (x::xs) = List.filter (not_equal n) (x::xs); - -fun remove_nth n [] = [] -| remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs)) - -fun get_nth n (x::xs) = hd (drop (n-1) (x::xs)) fun add_in_order (x:string) [] = [x] | add_in_order (x:string) ((y:string)::ys) = if (x < y) @@ -69,7 +56,7 @@ -fun lit_string_with_nums t = let val termstr = (Sign.string_of_term Mainsign) t +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) @@ -158,19 +145,20 @@ let val th = Recon_Base.assoc clause thml val prems = prems_of th + val sign = sign_of_thm th val fac1 = get_nth (lit1+1) prems val fac2 = get_nth (lit2+1) prems val unif_env = Unify.unifiers (Mainsign,Envir.empty 0, [(fac1, fac2)]) val newenv = getnewenv unif_env val envlist = Envir.alist_of newenv - val newsubsts = mksubstlist envlist [] + val (t1,t2)::_ = mksubstlist envlist [] in - if (is_Var (fst(hd(newsubsts)))) + if (is_Var t1) then let - val str1 = lit_string_with_nums (fst (hd newsubsts)); - val str2 = lit_string_with_nums (snd (hd newsubsts)); + 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) = (rearrange_clause res clause_strs allvars) @@ -180,8 +168,8 @@ end else let - val str2 = lit_string_with_nums (fst (hd newsubsts)); - val str1 = lit_string_with_nums (snd (hd newsubsts)); + 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) = (rearrange_clause res clause_strs allvars) @@ -282,7 +270,7 @@ val eqsubst = eq_lit_th RSN (2,rev_subst) val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) - in negated_asm_of_head newth end; + in Meson.negated_asm_of_head newth end; val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) diff -r 1da4ce092c0b -r 681bcb7f0389 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Mon Apr 11 12:34:34 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Mon Apr 11 16:25:31 2005 +0200 @@ -146,13 +146,13 @@ (* should be modified to allow other provers to be called *) (*********************************************************************) -fun call_resolve_tac thms sg_term (childin, childout,pid) n = let +fun call_resolve_tac sign thms sg_term (childin, childout,pid) n = let val thmstring = concat_with_and (map string_of_thm thms) "" val thm_no = length thms val _ = warning ("number of thms is : "^(string_of_int thm_no)) val _ = warning ("thmstring in call_res is: "^thmstring) - val goalstr = Sign.string_of_term Mainsign sg_term + val goalstr = Sign.string_of_term sign sg_term val goalproofstring = proofstring goalstr val no_returns =List.filter not_newline ( goalproofstring) val goalstring = implode no_returns @@ -165,7 +165,7 @@ (*val _ = tptp_inputs clauses prob_file*) val thmstring = concat_with_and (map string_of_thm thms) "" - val goalstr = Sign.string_of_term Mainsign sg_term + val goalstr = Sign.string_of_term sign sg_term val goalproofstring = proofstring goalstr val no_returns =List.filter not_newline ( goalproofstring) val goalstring = implode no_returns @@ -226,36 +226,25 @@ (* dummy tac vs. Doesn't call resolve_tac *) -fun call_atp_tac_tfrees thms n tfrees sg_term (childin, childout,pid) = - ( (warning("ths for tptp: "^(concat_with_and (map string_of_thm thms) ""))); - (warning("in call_atp_tac_tfrees")); +fun call_atp_tac_tfrees sign thms n tfrees sg_term (childin, childout,pid) = + ( warning("ths for tptp: " ^ (concat_with_and (map string_of_thm thms) "")); + warning("in call_atp_tac_tfrees"); tptp_inputs_tfrees (make_clauses thms) n tfrees; - call_resolve_tac thms sg_term (childin, childout, pid) n; + call_resolve_tac sign thms sg_term (childin, childout, pid) n; dummy_tac); - -(* -fun atp_tac_tfrees tfrees sg_term (childin, childout,pid) n = -let val _ = (warning ("in atp_tac_tfrees ")) - in -SELECT_GOAL (EVERY1 [rtac ccontr,atomize_tac,(*skolemize_tac,*) METAHYPS(fn negs => ((warning("calling call_atp_tac_tfrees with negs"^(concat_with_and (map string_of_thm negs) "")));(*make_clauses negs;*)dummy_tac)) ])1 -end; - - - -METAHYPS(fn negs => ((warning("calling call_atp_tac_tfrees with negs"^(concat_with_and (map string_of_thm negs) ""))));make_clauses negs;dummy_tac)) 1; -*) - - -fun atp_tac_tfrees tfrees sg_term (childin, childout,pid) n = -let val _ = (warning ("in atp_tac_tfrees ")) - val _ = (warning ("sg_term :"^((Sign.string_of_term Mainsign) sg_term))) +fun atp_tac_tfrees tfrees sg_term (childin, childout,pid) n st = +let val sign = sign_of_thm st + val _ = warning ("in atp_tac_tfrees ") + val _ = warning ("sg_term :" ^ (Sign.string_of_term sign sg_term)) in SELECT_GOAL (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, - METAHYPS(fn negs => ((warning("calling call_atp_tac_tfrees with negs"^(concat_with_and (map string_of_thm negs) "")));call_atp_tac_tfrees (negs) n tfrees sg_term (childin, childout,pid) ))]) n + METAHYPS(fn negs => (warning("calling call_atp_tac_tfrees with negs" + ^ (concat_with_and (map string_of_thm negs) "")); + call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st end; @@ -315,9 +304,10 @@ let val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) val _= (warning ("in isar_atp'")) val prems = prems_of thm + val sign = sign_of_thm thm val thms_string =concat_with_and (map string_of_thm thms) "" val thmstring = string_of_thm thm - val prems_string = concat_with_and (map (Sign.string_of_term Mainsign) prems) "" + val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) "" (* set up variables for writing out the clasimps to a tptp file *) (* val _ = write_out_clasimp (File.sysify_path axiom_file)*) (* cq: add write out clasimps to file *) @@ -405,8 +395,9 @@ val d_ss_thms = Simplifier.get_delta_simpset ctxt val thmstring = string_of_thm thm val sg_prems = prems_of thm + val sign = sign_of_thm thm val prem_no = length sg_prems - val prems_string = concat_with_and (map (Sign.string_of_term Mainsign) sg_prems) "" + val prems_string = concat_with_and (map (Sign.string_of_term sign) sg_prems) "" in (warning ("initial thm in isar_atp: "^thmstring));