--- a/src/HOL/ATP_Linkup.thy Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/ATP_Linkup.thy Wed Dec 19 17:40:48 2007 +0100
@@ -109,6 +109,7 @@
use "Tools/res_atp_methods.ML"
setup ResAtpMethods.setup --{*Oracle ATP methods: still useful?*}
+setup ResReconstruct.setup --{*Config parameters*}
setup ResAxioms.setup --{*Sledgehammer*}
subsection {* The Metis prover *}
--- a/src/HOL/MetisExamples/BigO.thy Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/MetisExamples/BigO.thy Wed Dec 19 17:40:48 2007 +0100
@@ -31,7 +31,7 @@
(*** Now various verions with an increasing modulus ***)
-ML{*ResReconstruct.modulus := 1*}
+declare [[reconstruction_modulus = 1]]
lemma bigo_pos_const: "(EX (c::'a::ordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -100,6 +100,8 @@
by (metis abs_le_iff 5 18 14)
qed
+declare [[reconstruction_modulus = 2]]
+
lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
= (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
@@ -107,7 +109,6 @@
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
apply (rule_tac x = "abs c" in exI, auto);
-ML{*ResReconstruct.modulus:=2*}
proof (neg_clausify)
fix c x
have 0: "\<And>(X1\<Colon>'a\<Colon>ordered_idom) X2\<Colon>'a\<Colon>ordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
@@ -140,6 +141,8 @@
by (metis 8 abs_ge_zero abs_mult_pos abs_mult 1 9 3 abs_le_iff)
qed
+declare [[reconstruction_modulus = 3]]
+
lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
= (EX c. 0 < c & (ALL x. (abs(h x)) <= (c * (abs (f x)))))"
@@ -147,7 +150,6 @@
apply (case_tac "c = 0", simp)
apply (rule_tac x = "1" in exI, simp)
apply (rule_tac x = "abs c" in exI, auto);
-ML{*ResReconstruct.modulus:=3*}
proof (neg_clausify)
fix c x
assume 0: "\<And>x\<Colon>'b\<Colon>type.
@@ -171,7 +173,7 @@
qed
-ML{*ResReconstruct.modulus:=1*}
+declare [[reconstruction_modulus = 1]]
lemma (*bigo_pos_const:*) "(EX (c::'a::ordered_idom).
ALL x. (abs (h x)) <= (c * (abs (f x))))
@@ -207,8 +209,7 @@
qed
-ML{*ResReconstruct.recon_sorts:=true*}
-
+declare [[reconstruction_sorts = true]]
lemma bigo_alt_def: "O(f) =
{h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
@@ -361,8 +362,8 @@
apply (rule add_mono)
ML{*ResAtp.problem_name := "BigO__bigo_plus_eq_simpler"*}
(*Found by SPASS; SLOW*)
-apply (metis le_maxI2 linorder_linear linorder_not_le min_max.less_eq_less_sup.sup_absorb1 mult_le_cancel_right xt1(6))
-apply (metis le_maxI2 linorder_not_le mult_le_cancel_right xt1(6))
+apply (metis le_maxI2 linorder_linear linorder_not_le min_max.less_eq_less_sup.sup_absorb1 mult_le_cancel_right order_trans)
+apply (metis le_maxI2 linorder_not_le mult_le_cancel_right order_trans)
done
ML{*ResAtp.problem_name := "BigO__bigo_bounded_alt"*}
@@ -429,7 +430,7 @@
lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)"
apply (auto simp add: bigo_def)
(*Version 1: one-shot proof*)
-apply (metis Orderings.leD Orderings.leI abs_ge_self abs_le_D1 abs_mult abs_of_nonneg order_le_less xt1(12));
+ apply (metis Orderings.leD Orderings.leI abs_ge_self abs_le_D1 abs_mult abs_of_nonneg order_le_less)
done
text{*So here is the easier (and more natural) problem using transitivity*}
--- a/src/HOL/MetisExamples/Message.thy Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/MetisExamples/Message.thy Wed Dec 19 17:40:48 2007 +0100
@@ -206,7 +206,7 @@
ML{*ResAtp.problem_name := "Message__parts_insert_two"*}
lemma parts_insert2:
"parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
-by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right insert_commute parts_Un)
+by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right parts_Un)
lemma parts_UN_subset1: "(\<Union>x\<in>A. parts(H x)) \<subseteq> parts(\<Union>x\<in>A. H x)"
@@ -244,7 +244,7 @@
lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
apply (rule iffI)
apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing)
-apply (metis parts_Un parts_idem parts_increasing parts_mono)
+apply (metis parts_idem parts_mono)
done
lemma parts_trans: "[| X\<in> parts G; G \<subseteq> parts H |] ==> X\<in> parts H"
--- a/src/HOL/MetisExamples/Tarski.thy Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/MetisExamples/Tarski.thy Wed Dec 19 17:40:48 2007 +0100
@@ -574,7 +574,7 @@
qed
qed
-lemma (in CLF) lubH_is_fixp:
+lemma (in CLF) (*lubH_is_fixp:*)
"H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
apply (simp add: fix_def)
apply (rule conjI)
--- a/src/HOL/MetisExamples/set.thy Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/MetisExamples/set.thy Wed Dec 19 17:40:48 2007 +0100
@@ -20,7 +20,7 @@
lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
by metis
-ML{*ResReconstruct.modulus := 1*}
+declare [[reconstruction_modulus = 1]]
(*multiple versions of this example*)
lemma (*equal_union: *)
@@ -90,8 +90,7 @@
by (metis 31 29)
qed
-
-ML{*ResReconstruct.modulus := 2*}
+declare [[reconstruction_modulus = 2]]
lemma (*equal_union: *)
"(X = Y \<union> Z) =
@@ -134,7 +133,7 @@
by (metis 18 17)
qed
-ML{*ResReconstruct.modulus := 3*}
+declare [[reconstruction_modulus = 3]]
lemma (*equal_union: *)
"(X = Y \<union> Z) =
@@ -169,7 +168,7 @@
(*Example included in TPHOLs paper*)
-ML{*ResReconstruct.modulus := 4*}
+declare [[reconstruction_modulus = 4]]
lemma (*equal_union: *)
"(X = Y \<union> Z) =
--- a/src/HOL/Tools/meson.ML Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/Tools/meson.ML Wed Dec 19 17:40:48 2007 +0100
@@ -528,7 +528,7 @@
fun skolemize_nnf_list [] = []
| skolemize_nnf_list (th::ths) =
skolemize (make_nnf th) :: skolemize_nnf_list ths
- handle THM _ =>
+ handle THM _ => (*RS can fail if Unify.search_bound is too small*)
(warning ("Failed to Skolemize " ^ string_of_thm th);
skolemize_nnf_list ths);
--- a/src/HOL/Tools/metis_tools.ML Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/Tools/metis_tools.ML Wed Dec 19 17:40:48 2007 +0100
@@ -586,7 +586,7 @@
else Output.debug (fn () => "goal is higher-order")
val _ = Output.debug (fn () => "START METIS PROVE PROCESS")
in
- case refute thms of
+ case NAMED_CRITICAL "refute" (fn () => refute thms) of
Metis.Resolution.Contradiction mth =>
let val _ = Output.debug (fn () => "METIS RECONSTRUCTION START: " ^
Metis.Thm.toString mth)
--- a/src/HOL/Tools/res_reconstruct.ML Wed Dec 19 16:52:26 2007 +0100
+++ b/src/HOL/Tools/res_reconstruct.ML Wed Dec 19 17:40:48 2007 +0100
@@ -9,8 +9,6 @@
signature RES_RECONSTRUCT =
sig
datatype atp = E | SPASS | Vampire
- val modulus: int ref
- val recon_sorts: bool ref
val chained_hint: string
val checkEProofFound:
TextIO.instream * TextIO.outstream * Posix.Process.pid *
@@ -29,6 +27,7 @@
val num_typargs: Context.theory -> string -> int
val make_tvar: string -> typ
val strip_prefix: string -> string -> string option
+ val setup: Context.theory -> Context.theory
end;
structure ResReconstruct : RES_RECONSTRUCT =
@@ -39,11 +38,15 @@
fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
else ();
-datatype atp = E | SPASS | Vampire;
+(*For generating structured proofs: keep every nth proof line*)
+val (modulus, modulus_setup) = Attrib.config_int "reconstruction_modulus" 1;
-val recon_sorts = ref true;
+(*Indicates whether to include sort information in generated proofs*)
+val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "reconstruction_sorts" true;
-val modulus = ref 1; (*keep every nth proof line*)
+val setup = modulus_setup #> recon_sorts_setup;
+
+datatype atp = E | SPASS | Vampire;
(**** PARSING OF TSTP FORMAT ****)
@@ -358,7 +361,7 @@
"\"\n by (metis " ^ space_implode " " deps ^ ")\n"
fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
| dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
- in setmp show_sorts (!recon_sorts) dolines end;
+ in setmp show_sorts (Config.get ctxt recon_sorts) dolines end;
fun notequal t (_,t',_) = not (t aconv t');
@@ -408,13 +411,13 @@
counts the number of proof lines processed so far.
Deleted lines are replaced by their own dependencies. Note that the "add_nonnull_prfline"
phase may delete some dependencies, hence this phase comes later.*)
-fun add_wanted_prfline ((lno, t, []), (nlines, lines)) =
+fun add_wanted_prfline ctxt ((lno, t, []), (nlines, lines)) =
(nlines, (lno, t, []) :: lines) (*conjecture clauses must be kept*)
- | add_wanted_prfline ((lno, t, deps), (nlines, lines)) =
+ | add_wanted_prfline ctxt ((lno, t, deps), (nlines, lines)) =
if eq_types t orelse not (null (term_tvars t)) orelse
exists bad_free (term_frees t) orelse
(not (null lines) andalso (*final line can't be deleted for these reasons*)
- (length deps < 2 orelse nlines mod !modulus <> 0))
+ (length deps < 2 orelse nlines mod (Config.get ctxt modulus) <> 0))
then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*)
else (nlines+1, (lno, t, deps) :: lines);
@@ -442,7 +445,7 @@
val nonnull_lines =
foldr add_nonnull_prfline []
(foldr add_prfline [] (decode_tstp_list ctxt tuples))
- val (_,lines) = foldr add_wanted_prfline (0,[]) nonnull_lines
+ val (_,lines) = foldr (add_wanted_prfline ctxt) (0,[]) nonnull_lines
val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno
val ccls = map forall_intr_vars ccls
in