# HG changeset patch # User huffman # Date 1316722634 25200 # Node ID f65593159ee816f761b489fe0b524d72d2b5dc07 # Parent 13efaee97111f8f98f15dec5a0a0df55d22fae05# Parent 59ca831deef485901823c139d372e81bf3e638de merged diff -r 13efaee97111 -r f65593159ee8 doc-src/Sledgehammer/sledgehammer.tex --- 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 diff -r 13efaee97111 -r f65593159ee8 src/HOL/IsaMakefile --- 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 \ diff -r 13efaee97111 -r f65593159ee8 src/HOL/Proofs/Extraction/Higman.thy --- 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 \ Random.seed \ letter list \ Random.seed" where - "mk_word_aux k = exec { - i \ Random.range 10; - (if i > 7 \ k > 2 \ k > 1000 then Pair [] - else exec { - let l = (if i mod 2 = 0 then A else B); - ls \ mk_word_aux (Suc k); - Pair (l # ls) - })}" -by pat_completeness auto -termination by (relation "measure ((op -) 1001)") auto - -definition mk_word :: "Random.seed \ letter list \ Random.seed" where - "mk_word = mk_word_aux 0" - -primrec mk_word_s :: "nat \ Random.seed \ letter list \ Random.seed" where - "mk_word_s 0 = mk_word" - | "mk_word_s (Suc n) = exec { - _ \ mk_word; - mk_word_s n - }" - -definition g1 :: "nat \ letter list" where - "g1 s = fst (mk_word_s s (20000, 1))" - -definition g2 :: "nat \ letter list" where - "g2 s = fst (mk_word_s s (50000, 1))" - -fun f1 :: "nat \ letter list" where - "f1 0 = [A, A]" - | "f1 (Suc 0) = [B]" - | "f1 (Suc (Suc 0)) = [A, B]" - | "f1 _ = []" - -fun f2 :: "nat \ 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 +(*>*) diff -r 13efaee97111 -r f65593159ee8 src/HOL/Proofs/Extraction/Higman_Extraction.thy --- /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 \ Random.seed \ letter list \ Random.seed" where + "mk_word_aux k = exec { + i \ Random.range 10; + (if i > 7 \ k > 2 \ k > 1000 then Pair [] + else exec { + let l = (if i mod 2 = 0 then A else B); + ls \ mk_word_aux (Suc k); + Pair (l # ls) + })}" +by pat_completeness auto +termination by (relation "measure ((op -) 1001)") auto + +definition mk_word :: "Random.seed \ letter list \ Random.seed" where + "mk_word = mk_word_aux 0" + +primrec mk_word_s :: "nat \ Random.seed \ letter list \ Random.seed" where + "mk_word_s 0 = mk_word" + | "mk_word_s (Suc n) = exec { + _ \ mk_word; + mk_word_s n + }" + +definition g1 :: "nat \ letter list" where + "g1 s = fst (mk_word_s s (20000, 1))" + +definition g2 :: "nat \ letter list" where + "g2 s = fst (mk_word_s s (50000, 1))" + +fun f1 :: "nat \ letter list" where + "f1 0 = [A, A]" + | "f1 (Suc 0) = [B]" + | "f1 (Suc (Suc 0)) = [A, B]" + | "f1 _ = []" + +fun f2 :: "nat \ 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 diff -r 13efaee97111 -r f65593159ee8 src/HOL/Proofs/Extraction/ROOT.ML --- 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"]; diff -r 13efaee97111 -r f65593159ee8 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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)