--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Fri Apr 15 12:00:00 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Fri Apr 15 13:35:53 2005 +0200
@@ -214,7 +214,6 @@
val rev_ssubst = rotate_prems 1 ssubst;
-(* have changed from negate_nead to negate_head. God knows if this will actually work *)
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs=
let
val th1 = Recon_Base.assoc clause1 thml
@@ -403,14 +402,11 @@
fun not_newline ch = not (ch = "\n");
-fun concat_with_and [] str = str
-| concat_with_and (x::[]) str = str^"("^x^")"
-| concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
(*
fun follow clauses [] allvars thml recons =
let (* val _ = reset show_sorts*)
- val thmstring = concat_with_and (map string_of_thm (map snd thml)) ""
+ 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
--- a/src/HOL/Tools/ATP/res_clasimpset.ML Fri Apr 15 12:00:00 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Fri Apr 15 13:35:53 2005 +0200
@@ -62,20 +62,6 @@
|SOME cls => cls ;
-fun retr_thms ([]:MetaSimplifier.rrule list) = []
- | retr_thms (r::rs) = (#name r, #thm r)::(retr_thms rs);
-
-fun snds [] = []
- | snds ((x,y)::l) = y::(snds l);
-
-fun simpset_rules_of_thy thy =
- let val simpset = simpset_of thy
- val rules = #rules(fst (rep_ss simpset))
- val thms = retr_thms (snds(Net.dest rules))
- in thms end;
-
-
-
fun not_second c (a,b) = not_equal b c;
@@ -124,7 +110,7 @@
val names_rules = zip good_names name_fol_cs;
- val new_clasrls = (fst(ResAxioms.clausify_classical_rules name_fol_cs[]));
+ val new_clasrls = #1(ResAxioms.clausify_classical_rules name_fol_cs[])
val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;
@@ -161,25 +147,25 @@
(*********************)
(* Get simpset rules *)
(*********************)
- val (simpset_name_rules) =simpset_rules_of_thy (the_context());
+ val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context());
val named_simps = List.filter has_name_pair simpset_name_rules;
- val simp_names = map fst named_simps;
- val simp_rules = map snd named_simps;
+ val simp_names = map #1 named_simps;
+ val simp_rules = map #2 named_simps;
val (simpset_cls,badthms) = ResAxioms.clausify_simpset_rules simp_rules [];
(* 1137 clausif simps *)
val clausifiable_simps = remove_all_simps badthms named_simps;
val name_fol_simps = List.filter thm_is_fol clausifiable_simps ;
- val simp_names = map fst name_fol_simps;
- val simp_rules = map snd name_fol_simps;
+ val simp_names = map #1 name_fol_simps;
+ val simp_rules = map #2 name_fol_simps;
(* 995 of these *)
(* need to get names of claset_cluases so we can make sure we've*)
(* got the same ones (ie. the named ones ) as the claset rules *)
(* length 1374*)
- val new_simps = fst(ResAxioms.clausify_simpset_rules simp_rules []);
+ val new_simps = #1(ResAxioms.clausify_simpset_rules simp_rules []);
val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
val stick_strs = map stick simpset_tptp_strs;
--- a/src/HOL/Tools/meson.ML Fri Apr 15 12:00:00 2005 +0200
+++ b/src/HOL/Tools/meson.ML Fri Apr 15 13:35:53 2005 +0200
@@ -84,12 +84,10 @@
| has _ = false
in has end;
-(* for tracing statements *)
-
-fun concat_with_and [] str = str
-| concat_with_and (x::[]) str = str^" ("^x^")"
-| concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
-
+(* for tracing: encloses each string element in brackets. *)
+fun concat_with_and [] = ""
+ | concat_with_and [x] = "(" ^ x ^ ")"
+ | concat_with_and (x::xs) = "(" ^ x ^ ")" ^ " & " ^ concat_with_and xs;
(**** Clause handling ****)
@@ -326,7 +324,8 @@
(*Make clauses from a list of theorems, previously Skolemized and put into nnf.
The resulting clauses are HOL disjunctions.*)
fun make_clauses ths =
- ( (warning("in make_clauses ths are:"^(concat_with_and (map string_of_thm ths) ""))); sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
+ (warning("in make_clauses ths = " ^ concat_with_and (map string_of_thm ths));
+ sort_clauses (map (generalize o nodups) (foldr cnf [] ths)));
(*Convert a list of clauses to (contrapositive) Horn clauses*)
fun make_horns ths =
--- a/src/HOL/Tools/res_atp.ML Fri Apr 15 12:00:00 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Fri Apr 15 13:35:53 2005 +0200
@@ -64,12 +64,6 @@
val dummy_tac = PRIMITIVE(fn thm => thm );
-fun concat_with_and [] str = str
-| concat_with_and (x::[]) str = str^" ("^x^")"
-| concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & "))
-
-
-
(**** for Isabelle/ML interface ****)
fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ")
@@ -147,7 +141,7 @@
(*********************************************************************)
fun call_resolve_tac sign thms sg_term (childin, childout,pid) n = let
- val thmstring = concat_with_and (map string_of_thm thms) ""
+ val thmstring = Meson.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)
@@ -163,7 +157,7 @@
val clauses = make_clauses thms
val _ =( warning ("called make_clauses "))*)
(*val _ = tptp_inputs clauses prob_file*)
- val thmstring = concat_with_and (map string_of_thm thms) ""
+ val thmstring = Meson.concat_with_and (map string_of_thm thms)
val goalstr = Sign.string_of_term sign sg_term
val goalproofstring = proofstring goalstr
@@ -227,7 +221,8 @@
(* dummy tac vs. Doesn't call resolve_tac *)
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("ths for tptp: " ^
+ Meson.concat_with_and (map string_of_thm thms));
warning("in call_atp_tac_tfrees");
tptp_inputs_tfrees (make_clauses thms) n tfrees;
@@ -243,7 +238,7 @@
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) ""));
+ ^ Meson.concat_with_and (map string_of_thm negs));
call_atp_tac_tfrees sign negs n tfrees sg_term (childin, childout,pid) ))]) n st
end;
@@ -305,9 +300,9 @@
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 thms_string = Meson.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 sign) prems) ""
+ val prems_string = Meson.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 *)
@@ -397,9 +392,8 @@
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 sign) sg_prems) ""
+ val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems)
in
-
(warning ("initial thm in isar_atp: "^thmstring));
(warning ("subgoals in isar_atp: "^prems_string));
(warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
--- a/src/HOL/Tools/res_axioms.ML Fri Apr 15 12:00:00 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML Fri Apr 15 13:35:53 2005 +0200
@@ -229,7 +229,7 @@
val rm_Eps
: (Term.term * Term.term) list -> Thm.thm list -> Term.term list
val claset_rules_of_thy : Theory.theory -> Thm.thm list
-val simpset_rules_of_thy : Theory.theory -> Thm.thm list
+val simpset_rules_of_thy : Theory.theory -> (string * Thm.thm) list
val clausify_simpset_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list
val clausify_classical_rules : Thm.thm list -> Thm.thm list -> ResClause.clause list list * Thm.thm list
@@ -391,17 +391,8 @@
(******** Extracting and CNF/Clausify theorems from a classical reasoner and simpset of a given theory ******)
-local
-
fun retr_thms ([]:MetaSimplifier.rrule list) = []
- | retr_thms (r::rs) = (#thm r)::(retr_thms rs);
-
-
-fun snds [] = []
- | snds ((x,y)::l) = y::(snds l);
-
-in
-
+ | retr_thms (r::rs) = (#name r, #thm r)::(retr_thms rs);
fun claset_rules_of_thy thy =
let val clsset = rep_cs (claset_of thy)
@@ -416,13 +407,11 @@
fun simpset_rules_of_thy thy =
let val simpset = simpset_of thy
val rules = #rules(fst (rep_ss simpset))
- val thms = retr_thms (snds(Net.dest rules))
+ val thms = retr_thms (map #2 (Net.dest rules))
in
thms
end;
-end;
-
(**** Translate a set of classical rules or simplifier rules into CNF (still as type "thm") from a given theory ****)
@@ -455,7 +444,7 @@
(* CNF all simplifier rules from a given theory's simpset *)
fun cnf_simpset_rules_thy thy =
- let val thms = simpset_rules_of_thy thy
+ let val thms = map #2 (simpset_rules_of_thy thy)
in
cnf_simpset_rules thms []
end;
@@ -474,7 +463,7 @@
-(* convert all classical rules from a given theory's classical reasoner into Clause.clause format. *)
+(* convert all classical rules from a given theory into Clause.clause format. *)
fun clausify_classical_rules_thy thy =
let val rules = claset_rules_of_thy thy
in
@@ -491,9 +480,9 @@
end;
-(* convert all simplifier rules from a given theory's simplifier into Clause.clause format. *)
+(* convert all simplifier rules from a given theory into Clause.clause format. *)
fun clausify_simpset_rules_thy thy =
- let val thms = simpset_rules_of_thy thy
+ let val thms = map #2 (simpset_rules_of_thy thy)
in
clausify_simpset_rules thms []
end;