--- a/doc-src/Locales/Locales/Examples3.thy Mon Jun 22 20:59:12 2009 +0200
+++ b/doc-src/Locales/Locales/Examples3.thy Mon Jun 22 20:59:33 2009 +0200
@@ -143,8 +143,8 @@
interpretation nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
- and nat_dvd_meet_eq: "lattice.meet op dvd = gcd"
- and nat_dvd_join_eq: "lattice.join op dvd = lcm"
+ and nat_dvd_meet_eq: "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
+ and nat_dvd_join_eq: "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
proof -
show "lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
apply unfold_locales
@@ -152,23 +152,24 @@
apply (rule_tac x = "gcd x y" in exI)
apply auto [1]
apply (rule_tac x = "lcm x y" in exI)
- apply (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
+ apply (auto intro: nat_lcm_least)
done
then interpret nat_dvd: lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool" .
show "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
by (rule nat_dvd_less_eq)
- show "lattice.meet op dvd = gcd"
+ show "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
apply (auto simp add: expand_fun_eq)
apply (unfold nat_dvd.meet_def)
apply (rule the_equality)
apply (unfold nat_dvd.is_inf_def)
by auto
- show "lattice.join op dvd = lcm"
+ show "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
apply (auto simp add: expand_fun_eq)
apply (unfold nat_dvd.join_def)
apply (rule the_equality)
apply (unfold nat_dvd.is_sup_def)
- by (auto intro: lcm_dvd1 lcm_dvd2 lcm_least)
+ apply (auto intro: nat_lcm_least iff: nat_lcm_unique)
+ done
qed
text {* Equations @{thm [source] nat_dvd_meet_eq} and @{thm [source]
@@ -198,8 +199,8 @@
interpretation %visible nat_dvd:
distrib_lattice "op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool"
where "partial_order.less op dvd (x::nat) y = (x dvd y \<and> x \<noteq> y)"
- and "lattice.meet op dvd = gcd"
- and "lattice.join op dvd = lcm"
+ and "lattice.meet (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = gcd"
+ and "lattice.join (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool) = lcm"
proof -
show "distrib_lattice (op dvd :: nat \<Rightarrow> nat \<Rightarrow> bool)"
apply unfold_locales
--- a/doc-src/Locales/Locales/document/Examples3.tex Mon Jun 22 20:59:12 2009 +0200
+++ b/doc-src/Locales/Locales/document/Examples3.tex Mon Jun 22 20:59:33 2009 +0200
@@ -307,8 +307,8 @@
\isacommand{interpretation}\isamarkupfalse%
\ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
%
\isadelimproof
%
@@ -330,7 +330,7 @@
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}lcm\ x\ y{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
-\ {\isacharparenleft}auto\ intro{\isacharcolon}\ lcm{\isacharunderscore}dvd{\isadigit{1}}\ lcm{\isacharunderscore}dvd{\isadigit{2}}\ lcm{\isacharunderscore}least{\isacharparenright}\isanewline
+\ {\isacharparenleft}auto\ intro{\isacharcolon}\ nat{\isacharunderscore}lcm{\isacharunderscore}least{\isacharparenright}\isanewline
\ \ \ \ \isacommand{done}\isamarkupfalse%
\isanewline
\ \ \isacommand{then}\isamarkupfalse%
@@ -342,7 +342,7 @@
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ {\isacharparenleft}rule\ nat{\isacharunderscore}dvd{\isacharunderscore}less{\isacharunderscore}eq{\isacharparenright}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
@@ -354,7 +354,7 @@
\ \ \ \ \isacommand{by}\isamarkupfalse%
\ auto\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
+\ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
@@ -363,8 +363,10 @@
\ {\isacharparenleft}rule\ the{\isacharunderscore}equality{\isacharparenright}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline
-\ \ \ \ \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}auto\ intro{\isacharcolon}\ lcm{\isacharunderscore}dvd{\isadigit{1}}\ lcm{\isacharunderscore}dvd{\isadigit{2}}\ lcm{\isacharunderscore}least{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{apply}\isamarkupfalse%
+\ {\isacharparenleft}auto\ intro{\isacharcolon}\ nat{\isacharunderscore}lcm{\isacharunderscore}least\ iff{\isacharcolon}\ nat{\isacharunderscore}lcm{\isacharunderscore}unique{\isacharparenright}\isanewline
+\ \ \ \ \isacommand{done}\isamarkupfalse%
+\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
@@ -407,8 +409,8 @@
\ nat{\isacharunderscore}dvd{\isacharcolon}\isanewline
\ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
\ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline
\isacommand{proof}\isamarkupfalse%
\ {\isacharminus}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
--- a/src/HOL/Tools/atp_manager.ML Mon Jun 22 20:59:12 2009 +0200
+++ b/src/HOL/Tools/atp_manager.ML Mon Jun 22 20:59:33 2009 +0200
@@ -20,9 +20,9 @@
val info: unit -> unit
val messages: int option -> unit
type prover = int -> (thm * (string * int)) list option ->
- (int Symtab.table * bool Symtab.table) option -> string -> int ->
+ (thm * (string * int)) list option -> string -> int ->
Proof.context * (thm list * thm) ->
- bool * string * string * string vector * (int Symtab.table * bool Symtab.table)
+ bool * string * string * string vector * (thm * (string * int)) list
val add_prover: string -> prover -> theory -> theory
val print_provers: theory -> unit
val get_prover: string -> theory -> prover option
@@ -292,9 +292,9 @@
(* named provers *)
type prover = int -> (thm * (string * int)) list option ->
- (int Symtab.table * bool Symtab.table) option -> string -> int ->
+ (thm * (string * int)) list option -> string -> int ->
Proof.context * (thm list * thm) ->
- bool * string * string * string vector * (int Symtab.table * bool Symtab.table)
+ bool * string * string * string vector * (thm * (string * int)) list
fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
--- a/src/HOL/Tools/atp_minimal.ML Mon Jun 22 20:59:12 2009 +0200
+++ b/src/HOL/Tools/atp_minimal.ML Mon Jun 22 20:59:33 2009 +0200
@@ -83,9 +83,9 @@
("# Cannot determine problem status within resource limit", Timeout),
("Error", Error)]
-fun produce_answer (success, message, result_string, thm_name_vec, const_counts) =
+fun produce_answer (success, message, result_string, thm_name_vec, filtered) =
if success then
- (Success (Vector.foldr op:: [] thm_name_vec, const_counts), result_string)
+ (Success (Vector.foldr op:: [] thm_name_vec, filtered), result_string)
else
let
val failure = failure_strings |> get_first (fn (s, t) =>
@@ -100,7 +100,7 @@
(* wrapper for calling external prover *)
-fun sh_test_thms prover prover_name time_limit subgoalno state counts name_thms_pairs =
+fun sh_test_thms prover prover_name time_limit subgoalno state filtered name_thms_pairs =
let
val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
val name_thm_pairs =
@@ -109,7 +109,7 @@
val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
val (result, proof) =
produce_answer
- (prover time_limit (SOME axclauses) counts prover_name subgoalno (Proof.get_goal state))
+ (prover time_limit (SOME axclauses) filtered prover_name subgoalno (Proof.get_goal state))
val _ = println (string_of_result result)
val _ = debug proof
in
@@ -127,11 +127,12 @@
val _ = debug_fn (fn () => app (fn (n, tl) =>
(debug n; app (fn t => debug (" " ^ Display.string_of_thm t)) tl)) name_thms_pairs)
val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
- fun test_thms counts thms = case test_thms_fun counts thms of (Success _, _) => true | _ => false
+ fun test_thms filtered thms =
+ case test_thms_fun filtered thms of (Success _, _) => true | _ => false
in
(* try prove first to check result and get used theorems *)
(case test_thms_fun NONE name_thms_pairs of
- (Success (used, const_counts), _) =>
+ (Success (used, filtered), _) =>
let
val ordered_used = order_unique used
val to_use =
@@ -139,7 +140,7 @@
filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
else
name_thms_pairs
- val min_thms = (minimal (test_thms (SOME const_counts)) to_use)
+ val min_thms = (minimal (test_thms (SOME filtered)) to_use)
val min_names = order_unique (map fst min_thms)
val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
val _ = debug_fn (fn () => print_names min_thms)
--- a/src/HOL/Tools/atp_wrapper.ML Mon Jun 22 20:59:12 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML Mon Jun 22 20:59:33 2009 +0200
@@ -41,7 +41,7 @@
(* basic template *)
fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer
- timeout axiom_clauses const_counts name subgoalno goal =
+ timeout axiom_clauses filtered_clauses name subgoalno goal =
let
(* path to unique problem file *)
val destdir' = ! destdir
@@ -54,37 +54,40 @@
else error ("No such directory: " ^ destdir')
end
- (* write out problem file and call prover *)
+ (* get clauses and prepare them for writing *)
val (ctxt, (chain_ths, th)) = goal
val thy = ProofContext.theory_of ctxt
val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
- val probfile = prob_pathname subgoalno
- val fname = File.platform_path probfile
val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th subgoalno)
handle THM ("assume: variables", _, _) =>
error "Sledgehammer: Goal contains type variables (TVars)"
val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls
+ val the_filtered_clauses =
+ case filtered_clauses of
+ NONE => relevance_filter goal goal_cls
+ | SOME fcls => fcls
val the_axiom_clauses =
case axiom_clauses of
- NONE => relevance_filter goal goal_cls
+ NONE => the_filtered_clauses
| SOME axcls => axcls
- val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses thy
- val the_const_counts = case const_counts of
- NONE =>
- ResHolClause.count_constants(
- case axiom_clauses of
- NONE => clauses
- | SOME axcls => #2(preparer goal_cls chain_ths (relevance_filter goal goal_cls) thy)
- )
- | SOME ccs => ccs
- val _ = writer fname the_const_counts clauses
+ val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
+
+ (* write out problem file and call prover *)
+ val probfile = prob_pathname subgoalno
+ val fname = File.platform_path probfile
+ val _ = writer fname clauses
val cmdline =
if File.exists cmd then "exec " ^ File.shell_path cmd ^ " " ^ args
else error ("Bad executable: " ^ Path.implode cmd)
val (proof, rc) = system_out (cmdline ^ " " ^ fname)
- (* remove *temporary* files *)
- val _ = if destdir' = "" then OS.FileSys.remove fname else ()
+ (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
+ val _ =
+ if destdir' = "" then OS.FileSys.remove fname
+ else
+ let val out = TextIO.openOut (fname ^ "_proof")
+ val _ = TextIO.output (out, proof)
+ in TextIO.closeOut out end
(* check for success and print out some information on failure *)
val failure = find_failure proof
@@ -94,7 +97,7 @@
else if rc <> 0 then "External prover failed: " ^ proof
else "Try this command: " ^ produce_answer name (proof, thm_names, ctxt, th, subgoalno)
val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
- in (success, message, proof, thm_names, the_const_counts) end;
+ in (success, message, proof, thm_names, the_filtered_clauses) end;
@@ -102,7 +105,7 @@
(* generic TPTP-based provers *)
-fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses ccs name n goal =
+fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses fcls name n goal =
external_prover
(ResAtp.get_relevant max_new theory_const)
(ResAtp.prepare_clauses false)
@@ -110,7 +113,7 @@
command
ResReconstruct.find_failure
(if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
- timeout ax_clauses ccs name n goal;
+ timeout ax_clauses fcls name n goal;
(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
fun tptp_prover_opts max_new theory_const =
@@ -167,7 +170,7 @@
(* SPASS *)
-fun spass_opts max_new theory_const timeout ax_clauses ccs name n goal = external_prover
+fun spass_opts max_new theory_const timeout ax_clauses fcls name n goal = external_prover
(ResAtp.get_relevant max_new theory_const)
(ResAtp.prepare_clauses true)
ResHolClause.dfg_write_file
@@ -175,7 +178,7 @@
"-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
ResReconstruct.find_failure
ResReconstruct.lemma_list_dfg
- timeout ax_clauses ccs name n goal;
+ timeout ax_clauses fcls name n goal;
val spass = spass_opts 40 true;
--- a/src/HOL/Tools/res_atp.ML Mon Jun 22 20:59:12 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Mon Jun 22 20:59:33 2009 +0200
@@ -9,6 +9,7 @@
val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
(thm * (string * int)) list
val prepare_clauses : bool -> thm list -> thm list ->
+ (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list ->
(thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
ResHolClause.axiom_name vector * (ResHolClause.clause list * ResHolClause.clause list *
ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
@@ -526,26 +527,30 @@
relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
end;
-(* prepare and count clauses before writing *)
-fun prepare_clauses dfg goal_cls chain_ths axcls thy =
+(* prepare for passing to writer,
+ create additional clauses based on the information from extra_cls *)
+fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
let
- val white_thms = filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths))
+ val white_thms =
+ filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths))
val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
- val axcls = white_cls @ axcls
- val ccls = subtract_cls goal_cls axcls
+ val extra_cls = white_cls @ extra_cls
+ val ccls = subtract_cls goal_cls extra_cls
val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
val ccltms = map prop_of ccls
- and axtms = map (prop_of o #1) axcls
+ and axtms = map (prop_of o #1) extra_cls
val subs = tfree_classes_of_terms ccltms
and supers = tvar_classes_of_terms axtms
and tycons = type_consts_of_terms thy (ccltms@axtms)
(*TFrees in conjecture clauses; TVars in axiom clauses*)
- val (clnames, (conjectures, axiom_clauses, helper_clauses)) =
- ResHolClause.prepare_clauses dfg thy (isFO thy goal_cls) ccls axcls []
+ val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls
+ val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls)
+ val helper_clauses = ResHolClause.get_helper_clauses dfg thy (isFO thy goal_cls) (conjectures, extra_cls, [])
val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
in
- (Vector.fromList clnames, (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses))
+ (Vector.fromList clnames,
+ (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses))
end
end;
--- a/src/HOL/Tools/res_hol_clause.ML Mon Jun 22 20:59:12 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Mon Jun 22 20:59:33 2009 +0200
@@ -28,13 +28,18 @@
val strip_comb: combterm -> combterm * combterm list
val literals_of_term: theory -> term -> literal list * typ list
exception TOO_TRIVIAL
- val count_constants: clause list * clause list * clause list * 'a * 'b ->
- int Symtab.table * bool Symtab.table
- val prepare_clauses: bool -> theory -> bool -> thm list -> (thm * (axiom_name * clause_id)) list ->
- string list -> axiom_name list * (clause list * clause list * clause list)
- val tptp_write_file: string -> int Symtab.table * bool Symtab.table ->
+ val make_conjecture_clauses: bool -> theory -> thm list -> clause list (* dfg thy ccls *)
+ val make_axiom_clauses: bool ->
+ theory ->
+ (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list (* dfg thy axcls *)
+ val get_helper_clauses: bool ->
+ theory ->
+ bool ->
+ clause list * (thm * (axiom_name * clause_id)) list * string list ->
+ clause list
+ val tptp_write_file: string ->
clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
- val dfg_write_file: string -> int Symtab.table * bool Symtab.table ->
+ val dfg_write_file: string ->
clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
end
@@ -403,10 +408,12 @@
fun cnf_helper_thms thy =
ResAxioms.cnf_rules_pairs thy o map ResAxioms.pairname
-fun get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas) =
+fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
if isFO then [] (*first-order*)
else
- let val ct0 = List.foldl count_clause init_counters conjectures
+ let
+ val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
+ val ct0 = List.foldl count_clause init_counters conjectures
val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
fun needed c = valOf (Symtab.lookup ct c) > 0
val IK = if needed "c_COMBI" orelse needed "c_COMBK"
@@ -464,18 +471,10 @@
(* tptp format *)
-fun prepare_clauses dfg thy isFO thms ax_tuples user_lemmas =
+fun tptp_write_file filename clauses =
let
- val conjectures = make_conjecture_clauses dfg thy thms
- val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses dfg thy ax_tuples)
- val helper_clauses = get_helper_clauses dfg thy isFO (conjectures, axclauses, user_lemmas)
- in
- (clnames, (conjectures, axclauses, helper_clauses))
- end
-
-(* write TPTP format to a single file *)
-fun tptp_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) =
- let
+ val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
+ val const_counts = count_constants clauses
val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_counts) conjectures)
val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
val out = TextIO.openOut filename
@@ -492,8 +491,10 @@
(* dfg format *)
-fun dfg_write_file filename const_counts (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) =
+fun dfg_write_file filename clauses =
let
+ val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
+ val const_counts = count_constants clauses
val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg const_counts) conjectures)
and probname = Path.implode (Path.base (Path.explode filename))
val axstrs = map (#1 o (clause2dfg const_counts)) axclauses
--- a/src/Pure/General/scan.scala Mon Jun 22 20:59:12 2009 +0200
+++ b/src/Pure/General/scan.scala Mon Jun 22 20:59:33 2009 +0200
@@ -19,11 +19,8 @@
private case class Tree(val branches: Map[Char, (String, Tree)])
private val empty_tree = Tree(Map())
- private def make(tree: Tree, max: Int): Lexicon =
- new Lexicon {
- override val main_tree = tree
- override val max_entry = max
- }
+ private def make(tree: Tree): Lexicon =
+ new Lexicon { override val main_tree = tree }
val empty: Lexicon = new Lexicon
def apply(strs: String*): Lexicon = (empty /: strs) ((lex, str) => lex + str)
@@ -35,7 +32,6 @@
import Lexicon.Tree
val main_tree: Tree = Lexicon.empty_tree
- val max_entry = -1
/* auxiliary operations */
@@ -74,7 +70,7 @@
override def stringPrefix = "Lexicon"
- override def isEmpty: Boolean = { max_entry < 0 }
+ override def isEmpty: Boolean = { main_tree.branches.isEmpty }
def size: Int = content(main_tree, Nil).length
def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements
@@ -102,7 +98,7 @@
} else tree
}
if (contains(str)) this
- else Lexicon.make(extend(main_tree, 0), max_entry max str.length)
+ else Lexicon.make(extend(main_tree, 0))
}
def empty[A]: Set[A] = error("Undefined")