--- a/doc-src/Sledgehammer/sledgehammer.tex Thu Sep 22 12:55:19 2011 -0700
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Sep 22 13:17:14 2011 -0700
@@ -176,7 +176,7 @@
set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
\texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
-with E 1.0 to 1.3, SPASS 3.5 and 3.7, and Vampire 0.6, 1.0, and 1.8%
+with E 1.0 to 1.4, SPASS 3.5 and 3.7, and Vampire 0.6, 1.0, and 1.8%
\footnote{Following the rewrite of Vampire, the counter for version numbers was
reset to 0; hence the (new) Vampire versions 0.6, 1.0, and 1.8 are more recent
than, say, Vampire 9.0 or 11.5.}%
@@ -265,16 +265,12 @@
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this: \textbf{by} (\textit{metis hd.simps}) (15 ms). \\[3\smallskipamount]
%
-Sledgehammer: ``\textit{remote\_e\_sine}'' on goal \\
-$[a] = [b] \,\Longrightarrow\, a = b$ \\
-Try this: \textbf{by} (\textit{metis hd.simps}) (18 ms). \\[3\smallskipamount]
-%
Sledgehammer: ``\textit{remote\_z3}'' on goal \\
$[a] = [b] \,\Longrightarrow\, a = b$ \\
Try this: \textbf{by} (\textit{metis list.inject}) (20 ms).
\postw
-Sledgehammer ran E, E-SInE, SPASS, Vampire, Waldmeister, and Z3 in parallel.
+Sledgehammer ran E, SPASS, Vampire, Waldmeister, and Z3 in parallel.
Depending on which provers are installed and how many processor cores are
available, some of the provers might be missing or present with a
\textit{remote\_} prefix. Waldmeister is run only for unit equational problems,
@@ -505,7 +501,7 @@
Metis: Falling back on ``\textit{metis} (\textit{full\_types})''.
\postw
-in a successful Metis proof, you can advantageously pass the
+for a successful Metis proof, you can advantageously pass the
\textit{full\_types} option to \textit{metis} directly.
\point{Are generated proofs minimal?}
@@ -818,7 +814,7 @@
with TPTP syntax'' runs on Geoff Sutcliffe's Miami servers.
\end{enum}
-By default, Sledgehammer runs E, E-SInE, SPASS, Vampire, Z3 (or whatever
+By default, Sledgehammer runs E, SPASS, Vampire, Z3 (or whatever
the SMT module's \textit{smt\_solver} configuration option is set to), and (if
appropriate) Waldmeister in parallel---either locally or remotely, depending on
the number of processor cores available. For historical reasons, the default
--- a/src/HOL/IsaMakefile Thu Sep 22 12:55:19 2011 -0700
+++ b/src/HOL/IsaMakefile Thu Sep 22 13:17:14 2011 -0700
@@ -915,7 +915,8 @@
$(LOG)/HOL-Proofs-Extraction.gz: $(OUT)/HOL-Proofs \
Library/Efficient_Nat.thy Proofs/Extraction/Euclid.thy \
Proofs/Extraction/Greatest_Common_Divisor.thy \
- Proofs/Extraction/Higman.thy Proofs/Extraction/Pigeonhole.thy \
+ Proofs/Extraction/Higman.thy Proofs/Extraction/Higman_Extraction.thy \
+ Proofs/Extraction/Pigeonhole.thy \
Proofs/Extraction/QuotRem.thy Proofs/Extraction/ROOT.ML \
Proofs/Extraction/Util.thy Proofs/Extraction/Warshall.thy \
Proofs/Extraction/document/root.tex \
--- a/src/HOL/Proofs/Extraction/Higman.thy Thu Sep 22 12:55:19 2011 -0700
+++ b/src/HOL/Proofs/Extraction/Higman.thy Thu Sep 22 13:17:14 2011 -0700
@@ -6,7 +6,7 @@
header {* Higman's lemma *}
theory Higman
-imports Main "~~/src/HOL/Library/State_Monad" Random
+imports Main
begin
text {*
@@ -310,156 +310,6 @@
using higman
by (rule good_prefix_lemma) simp+
-subsection {* Extracting the program *}
-
-declare R.induct [ind_realizer]
-declare T.induct [ind_realizer]
-declare L.induct [ind_realizer]
-declare good.induct [ind_realizer]
-declare bar.induct [ind_realizer]
-
-extract higman_idx
-
-text {*
- Program extracted from the proof of @{text higman_idx}:
- @{thm [display] higman_idx_def [no_vars]}
- Corresponding correctness theorem:
- @{thm [display] higman_idx_correctness [no_vars]}
- Program extracted from the proof of @{text higman}:
- @{thm [display] higman_def [no_vars]}
- Program extracted from the proof of @{text prop1}:
- @{thm [display] prop1_def [no_vars]}
- Program extracted from the proof of @{text prop2}:
- @{thm [display] prop2_def [no_vars]}
- Program extracted from the proof of @{text prop3}:
- @{thm [display] prop3_def [no_vars]}
-*}
-
-
-subsection {* Some examples *}
-
-instantiation LT and TT :: default
-begin
-
-definition "default = L0 [] []"
-
-definition "default = T0 A [] [] [] R0"
-
-instance ..
-
+(*<*)
end
-
-function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
- "mk_word_aux k = exec {
- i \<leftarrow> Random.range 10;
- (if i > 7 \<and> k > 2 \<or> k > 1000 then Pair []
- else exec {
- let l = (if i mod 2 = 0 then A else B);
- ls \<leftarrow> mk_word_aux (Suc k);
- Pair (l # ls)
- })}"
-by pat_completeness auto
-termination by (relation "measure ((op -) 1001)") auto
-
-definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" where
- "mk_word = mk_word_aux 0"
-
-primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
- "mk_word_s 0 = mk_word"
- | "mk_word_s (Suc n) = exec {
- _ \<leftarrow> mk_word;
- mk_word_s n
- }"
-
-definition g1 :: "nat \<Rightarrow> letter list" where
- "g1 s = fst (mk_word_s s (20000, 1))"
-
-definition g2 :: "nat \<Rightarrow> letter list" where
- "g2 s = fst (mk_word_s s (50000, 1))"
-
-fun f1 :: "nat \<Rightarrow> letter list" where
- "f1 0 = [A, A]"
- | "f1 (Suc 0) = [B]"
- | "f1 (Suc (Suc 0)) = [A, B]"
- | "f1 _ = []"
-
-fun f2 :: "nat \<Rightarrow> letter list" where
- "f2 0 = [A, A]"
- | "f2 (Suc 0) = [B]"
- | "f2 (Suc (Suc 0)) = [B, A]"
- | "f2 _ = []"
-
-ML {*
-local
- val higman_idx = @{code higman_idx};
- val g1 = @{code g1};
- val g2 = @{code g2};
- val f1 = @{code f1};
- val f2 = @{code f2};
-in
- val (i1, j1) = higman_idx g1;
- val (v1, w1) = (g1 i1, g1 j1);
- val (i2, j2) = higman_idx g2;
- val (v2, w2) = (g2 i2, g2 j2);
- val (i3, j3) = higman_idx f1;
- val (v3, w3) = (f1 i3, f1 j3);
- val (i4, j4) = higman_idx f2;
- val (v4, w4) = (f2 i4, f2 j4);
-end;
-*}
-
-text {* The same story with the legacy SML code generator,
-this can be removed once the code generator is removed. *}
-
-code_module Higman
-contains
- higman = higman_idx
-
-ML {*
-local open Higman in
-
-val a = 16807.0;
-val m = 2147483647.0;
-
-fun nextRand seed =
- let val t = a*seed
- in t - m * real (Real.floor(t/m)) end;
-
-fun mk_word seed l =
- let
- val r = nextRand seed;
- val i = Real.round (r / m * 10.0);
- in if i > 7 andalso l > 2 then (r, []) else
- apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1))
- end;
-
-fun f s zero = mk_word s 0
- | f s (Suc n) = f (fst (mk_word s 0)) n;
-
-val g1 = snd o (f 20000.0);
-
-val g2 = snd o (f 50000.0);
-
-fun f1 zero = [A,A]
- | f1 (Suc zero) = [B]
- | f1 (Suc (Suc zero)) = [A,B]
- | f1 _ = [];
-
-fun f2 zero = [A,A]
- | f2 (Suc zero) = [B]
- | f2 (Suc (Suc zero)) = [B,A]
- | f2 _ = [];
-
-val (i1, j1) = higman g1;
-val (v1, w1) = (g1 i1, g1 j1);
-val (i2, j2) = higman g2;
-val (v2, w2) = (g2 i2, g2 j2);
-val (i3, j3) = higman f1;
-val (v3, w3) = (f1 i3, f1 j3);
-val (i4, j4) = higman f2;
-val (v4, w4) = (f2 i4, f2 j4);
-
-end;
-*}
-
-end
+(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy Thu Sep 22 13:17:14 2011 -0700
@@ -0,0 +1,164 @@
+(* Title: HOL/Proofs/Extraction/Higman_Extraction.thy
+ Author: Stefan Berghofer, TU Muenchen
+ Author: Monika Seisenberger, LMU Muenchen
+*)
+
+(*<*)
+theory Higman_Extraction
+imports Higman "~~/src/HOL/Library/State_Monad" Random
+begin
+(*>*)
+
+subsection {* Extracting the program *}
+
+declare R.induct [ind_realizer]
+declare T.induct [ind_realizer]
+declare L.induct [ind_realizer]
+declare good.induct [ind_realizer]
+declare bar.induct [ind_realizer]
+
+extract higman_idx
+
+text {*
+ Program extracted from the proof of @{text higman_idx}:
+ @{thm [display] higman_idx_def [no_vars]}
+ Corresponding correctness theorem:
+ @{thm [display] higman_idx_correctness [no_vars]}
+ Program extracted from the proof of @{text higman}:
+ @{thm [display] higman_def [no_vars]}
+ Program extracted from the proof of @{text prop1}:
+ @{thm [display] prop1_def [no_vars]}
+ Program extracted from the proof of @{text prop2}:
+ @{thm [display] prop2_def [no_vars]}
+ Program extracted from the proof of @{text prop3}:
+ @{thm [display] prop3_def [no_vars]}
+*}
+
+
+subsection {* Some examples *}
+
+instantiation LT and TT :: default
+begin
+
+definition "default = L0 [] []"
+
+definition "default = T0 A [] [] [] R0"
+
+instance ..
+
+end
+
+function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
+ "mk_word_aux k = exec {
+ i \<leftarrow> Random.range 10;
+ (if i > 7 \<and> k > 2 \<or> k > 1000 then Pair []
+ else exec {
+ let l = (if i mod 2 = 0 then A else B);
+ ls \<leftarrow> mk_word_aux (Suc k);
+ Pair (l # ls)
+ })}"
+by pat_completeness auto
+termination by (relation "measure ((op -) 1001)") auto
+
+definition mk_word :: "Random.seed \<Rightarrow> letter list \<times> Random.seed" where
+ "mk_word = mk_word_aux 0"
+
+primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
+ "mk_word_s 0 = mk_word"
+ | "mk_word_s (Suc n) = exec {
+ _ \<leftarrow> mk_word;
+ mk_word_s n
+ }"
+
+definition g1 :: "nat \<Rightarrow> letter list" where
+ "g1 s = fst (mk_word_s s (20000, 1))"
+
+definition g2 :: "nat \<Rightarrow> letter list" where
+ "g2 s = fst (mk_word_s s (50000, 1))"
+
+fun f1 :: "nat \<Rightarrow> letter list" where
+ "f1 0 = [A, A]"
+ | "f1 (Suc 0) = [B]"
+ | "f1 (Suc (Suc 0)) = [A, B]"
+ | "f1 _ = []"
+
+fun f2 :: "nat \<Rightarrow> letter list" where
+ "f2 0 = [A, A]"
+ | "f2 (Suc 0) = [B]"
+ | "f2 (Suc (Suc 0)) = [B, A]"
+ | "f2 _ = []"
+
+ML {*
+local
+ val higman_idx = @{code higman_idx};
+ val g1 = @{code g1};
+ val g2 = @{code g2};
+ val f1 = @{code f1};
+ val f2 = @{code f2};
+in
+ val (i1, j1) = higman_idx g1;
+ val (v1, w1) = (g1 i1, g1 j1);
+ val (i2, j2) = higman_idx g2;
+ val (v2, w2) = (g2 i2, g2 j2);
+ val (i3, j3) = higman_idx f1;
+ val (v3, w3) = (f1 i3, f1 j3);
+ val (i4, j4) = higman_idx f2;
+ val (v4, w4) = (f2 i4, f2 j4);
+end;
+*}
+
+text {* The same story with the legacy SML code generator,
+this can be removed once the code generator is removed. *}
+
+code_module Higman
+contains
+ higman = higman_idx
+
+ML {*
+local open Higman in
+
+val a = 16807.0;
+val m = 2147483647.0;
+
+fun nextRand seed =
+ let val t = a*seed
+ in t - m * real (Real.floor(t/m)) end;
+
+fun mk_word seed l =
+ let
+ val r = nextRand seed;
+ val i = Real.round (r / m * 10.0);
+ in if i > 7 andalso l > 2 then (r, []) else
+ apsnd (cons (if i mod 2 = 0 then A else B)) (mk_word r (l+1))
+ end;
+
+fun f s zero = mk_word s 0
+ | f s (Suc n) = f (fst (mk_word s 0)) n;
+
+val g1 = snd o (f 20000.0);
+
+val g2 = snd o (f 50000.0);
+
+fun f1 zero = [A,A]
+ | f1 (Suc zero) = [B]
+ | f1 (Suc (Suc zero)) = [A,B]
+ | f1 _ = [];
+
+fun f2 zero = [A,A]
+ | f2 (Suc zero) = [B]
+ | f2 (Suc (Suc zero)) = [B,A]
+ | f2 _ = [];
+
+val (i1, j1) = higman g1;
+val (v1, w1) = (g1 i1, g1 j1);
+val (i2, j2) = higman g2;
+val (v2, w2) = (g2 i2, g2 j2);
+val (i3, j3) = higman f1;
+val (v3, w3) = (f1 i3, f1 j3);
+val (i4, j4) = higman f2;
+val (v4, w4) = (f2 i4, f2 j4);
+
+end;
+*}
+
+end
--- a/src/HOL/Proofs/Extraction/ROOT.ML Thu Sep 22 12:55:19 2011 -0700
+++ b/src/HOL/Proofs/Extraction/ROOT.ML Thu Sep 22 13:17:14 2011 -0700
@@ -8,5 +8,5 @@
share_common_data ();
-no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization"];
-use_thys ["Greatest_Common_Divisor", "Warshall", "Higman", "Pigeonhole", "Euclid"];
+no_document use_thys ["~~/src/HOL/Number_Theory/UniqueFactorization", "~~/src/HOL/Library/State_Monad"];
+use_thys ["Greatest_Common_Divisor", "Warshall", "Higman_Extraction", "Pigeonhole", "Euclid"];
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Sep 22 12:55:19 2011 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Sep 22 13:17:14 2011 -0700
@@ -201,7 +201,7 @@
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
timeout, it makes sense to put SPASS first. *)
fun default_provers_param_value ctxt =
- [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, e_sineN, waldmeisterN]
+ [spassN, eN, vampireN, SMT_Solver.solver_name_of ctxt, waldmeisterN]
|> map_filter (remotify_prover_if_not_installed ctxt)
|> avoid_too_many_threads ctxt (Multithreading.max_threads_value (),
max_default_remote_threads)