--- a/src/HOL/Tools/ATP/recon_order_clauses.ML Tue May 31 12:42:36 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Tue May 31 17:52:10 2005 +0200
@@ -41,7 +41,7 @@
else
takeUntil ch xs (res@[x]);
-fun contains_eq str = inlist "=" str
+fun contains_eq str = "=" mem str
fun eq_not_neq str = let val uptoeq = fst(takeUntil "=" str [])
in (last uptoeq) <> "~" end
--- a/src/HOL/Tools/ATP/recon_prelim.ML Tue May 31 12:42:36 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_prelim.ML Tue May 31 17:52:10 2005 +0200
@@ -131,31 +131,6 @@
Free (istr,tv)
end;
-fun inlist v [] = false
- | inlist v (first::rest) = if first = v then
- true
- else inlist v rest;
-
-(*fun in_vars v [] = false
- | in_vars v ((a,b)::rest) = if v = a then
- true
- else if v = b then
- true
- else in_vars v rest;*)
-
-fun in_vars v [] = false
- | in_vars v (a::rest) = if (fst v) = a then
- true
-
- else in_vars v rest;
-
-fun equalpair (a,b) (c,d) = if (a,b)= (c,d) then
- true
- else if (a,b) = (d,c) then
- true
- else false;
-
-
fun is_empty_seq thisseq = case Seq.chop (1, thisseq) of
([],_) => true
| _ => false
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue May 31 12:42:36 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue May 31 17:52:10 2005 +0200
@@ -53,13 +53,14 @@
(* Versions that include type information *)
-fun string_of_thm thm = let val _ = set show_sorts
- val str = Display.string_of_thm thm
- val no_returns =List.filter not_newline (explode str)
- val _ = reset show_sorts
- in
- implode no_returns
- end
+fun string_of_thm thm =
+ let val _ = set show_sorts
+ val str = Display.string_of_thm thm
+ val no_returns =List.filter not_newline (explode str)
+ val _ = reset show_sorts
+ in
+ implode no_returns
+ end
(* check separate args in the watcher program for separating strings with a * or ; or something *)
@@ -67,8 +68,6 @@
fun clause_strs_to_string [] str = str
| clause_strs_to_string (x::xs) str = clause_strs_to_string xs (str^x^"%")
-
-
fun thmvars_to_string [] str = str
| thmvars_to_string (x::xs) str = thmvars_to_string xs (str^x^"%")
@@ -174,11 +173,8 @@
fun get_assoc_snds [] xs assocs= assocs
| get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_out_of_order x ys))])
-
-
-
fun add_if_not_inlist [] xs newlist = newlist
-| add_if_not_inlist (y::ys) xs newlist = if (not (inlist y xs)) then
+| add_if_not_inlist (y::ys) xs newlist = if (not (y mem xs)) then
add_if_not_inlist ys xs (y::newlist)
else add_if_not_inlist ys xs (newlist)
@@ -205,57 +201,47 @@
(* retrieve the axioms that were obtained from the clasimpset *)
fun get_clasimp_cls clause_arr clasimp_num step_nums =
- let
- val realnums = map subone step_nums
-
-
- val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
- val axnums = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "axnums")))
- val _ = TextIO.output(axnums,(numstr clasimp_nums))
- val _ = TextIO.closeOut(axnums)
- in
- retrieve_axioms clause_arr clasimp_nums
- end
+ let val realnums = map subone step_nums
+ val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
+ val axnums = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "axnums")))
+ val _ = TextIO.output(axnums,(numstr clasimp_nums))
+ val _ = TextIO.closeOut(axnums)
+ in
+ retrieve_axioms clause_arr clasimp_nums
+ end
-fun get_cls [] = []
-| get_cls (x::xs) = ((#1 x)::(get_cls xs))
(* add array and table here, so can retrieve clasimp axioms *)
- fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * Thm.thm) Array.array) num_of_clauses =
- let
- (* not sure why this is necessary again, but seems to be *)
- val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
- val axioms = get_init_axioms proof_steps
- val step_nums = get_step_nums axioms []
-
- (***********************************************)
- (* here need to add the clauses from clause_arr*)
- (***********************************************)
-
- val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums
- val clauses=(get_cls clasimp_names_cls)
- val (names_clsnums) = map ResClause.clause_info clauses
- val clasimp_names = map fst names_clsnums
-
- val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "clasimp_names"))) val clasimp_namestr = concat clasimp_names
- val _ = TextIO.output (outfile,clasimp_namestr)
- val _ = TextIO.closeOut outfile
- val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
-
- in
- (clasimp_names)
- end
+ fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * thm) Array.array) num_of_clauses =
+ let
+ (* not sure why this is necessary again, but seems to be *)
+ val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
+ val axioms = get_init_axioms proof_steps
+ val step_nums = get_step_nums axioms []
+
+ (***********************************************)
+ (* here need to add the clauses from clause_arr*)
+ (***********************************************)
+
+ val (clasimp_names_cls) = get_clasimp_cls clause_arr num_of_clauses step_nums
+ val clasimp_names = map (#1 o ResClause.clause_info o #1) clasimp_names_cls
+
+ val _ = File.write (File.tmp_path (Path.basic "clasimp_names"))
+ (concat clasimp_names)
+ val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
+ in
+ clasimp_names
+ end
fun numclstr (vars, []) str = str
-| numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
-in
-numclstr (vars,rest) newstr
-end
+| numclstr ( vars, ((num, thm)::rest)) str =
+ let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
+ in
+ numclstr (vars,rest) newstr
+ end
-
-fun addvars c (a,b) = (a,b,c)
-
+fun addvars c (a,b) = (a,b,c)
fun get_axioms_used proof_steps thms clause_arr num_of_clauses =
let
--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Tue May 31 12:42:36 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Tue May 31 17:52:10 2005 +0200
@@ -10,10 +10,8 @@
else
(y::(add_in_order x ys))
fun add_once x [] = [x]
-| add_once x (y::ys) = if (inlist x (y::ys)) then
- (y::ys)
- else
- add_in_order x (y::ys)
+| 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);