--- 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\
--- 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)
--- 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
-
--- 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 *)
--- 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)
--- 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));