# HG changeset patch
# User webertj
# Date 1257620150 0
# Node ID 5b31218a3a8cf9256aa34eeeac5235707c559803
# Parent  70026e20fa4c91616c1b14c92c9911220a47ffa4# Parent  e744ad2d03939fae1a5ffd105bf5a7f3a1f8f8b5
merged

diff -r 70026e20fa4c -r 5b31218a3a8c src/HOL/ex/HarmonicSeries.thy
--- 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)"
diff -r 70026e20fa4c -r 5b31218a3a8c src/HOL/ex/SAT_Examples.thy
--- 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