--- a/src/HOL/ex/HarmonicSeries.thy Sat Nov 07 08:31:56 2009 -0800
+++ b/src/HOL/ex/HarmonicSeries.thy Sat Nov 07 18:55:50 2009 +0000
@@ -8,7 +8,7 @@
imports Complex_Main
begin
-section {* Abstract *}
+subsection {* Abstract *}
text {* The following document presents a proof of the Divergence of
Harmonic Series theorem formalised in the Isabelle/Isar theorem
@@ -35,7 +35,7 @@
QED.
*}
-section {* Formal Proof *}
+subsection {* Formal Proof *}
lemma two_pow_sub:
"0 < m \<Longrightarrow> (2::nat)^m - 2^(m - 1) = 2^(m - 1)"
--- a/src/HOL/ex/SAT_Examples.thy Sat Nov 07 08:31:56 2009 -0800
+++ b/src/HOL/ex/SAT_Examples.thy Sat Nov 07 18:55:50 2009 +0000
@@ -1,7 +1,6 @@
(* Title: HOL/ex/SAT_Examples.thy
- ID: $Id$
Author: Alwen Tiu, Tjark Weber
- Copyright 2005-2006
+ Copyright 2005-2009
*)
header {* Examples for the 'sat' and 'satx' tactic *}
@@ -534,4 +533,38 @@
(* ML {* Toplevel.profiling := 0; *} *)
+text {*
+Function {\tt benchmark} takes the name of an existing DIMACS CNF
+file, parses this file, passes the problem to a SAT solver, and checks
+the proof of unsatisfiability found by the solver. The function
+measures the time spent on proof reconstruction (at least real time
+also includes time spent in the SAT solver), and additionally returns
+the number of resolution steps in the proof.
+*}
+
+(* ML {*
+sat.solver := "zchaff_with_proofs";
+Unsynchronized.reset sat.trace_sat;
+Unsynchronized.reset quick_and_dirty;
+*} *)
+
+ML {*
+fun benchmark dimacsfile =
+let
+ val prop_fm = SatSolver.read_dimacs_cnf_file (Path.explode dimacsfile)
+ fun and_to_list (PropLogic.And (fm1, fm2)) acc =
+ and_to_list fm2 (fm1 :: acc)
+ | and_to_list fm acc =
+ rev (fm :: acc)
+ val clauses = and_to_list prop_fm []
+ val terms = map (HOLogic.mk_Trueprop o PropLogic.term_of_prop_formula)
+ clauses
+ val cterms = map (Thm.cterm_of @{theory}) terms
+ val timer = start_timing ()
+ val thm = sat.rawsat_thm @{context} cterms
+in
+ (end_timing timer, !sat.counter)
+end;
+*}
+
end