# HG changeset patch
# User webertj
# Date 1146590628 -7200
# Node ID 1724ec4032c5a1b4c2b9d031644f0cd5c99f2221
# Parent  fc4c6458d5698eb016c5bbcdd4e0016e9aec6b64
beta_eta_conversion added to pre_cnf_tac

diff -r fc4c6458d569 -r 1724ec4032c5 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Tue May 02 16:19:53 2006 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Tue May 02 19:23:48 2006 +0200
@@ -242,6 +242,9 @@
 	(* trivial clauses during preprocessing, and otherwise our clause     *)
 	(* numbering would be off                                             *)
 	val non_triv_clauses  = filter (not o cnf.clause_is_trivial o HOLogic.dest_Trueprop o prop_of) clauses
+	val _                 = if !trace_sat then
+			tracing ("Non-trivial clauses:\n" ^ space_implode "\n" (map (string_of_cterm o cprop_of) non_triv_clauses))
+		else ()
 	(* translate clauses from HOL terms to PropLogic.prop_formula *)
 	val (fms, atom_table) = fold_map (PropLogic.prop_formula_of_term o HOLogic.dest_Trueprop o prop_of) non_triv_clauses Termtab.empty
 	val _                 = if !trace_sat then
@@ -333,12 +336,13 @@
 (*      (handling meta-logical connectives in B properly before negating),   *)
 (*      then replaces meta-logical connectives in the premises (i.e. "==>",  *)
 (*      "!!" and "==") by connectives of the HOL object-logic (i.e. by       *)
-(*      "-->", "!", and "=")                                                 *)
+(*      "-->", "!", and "="), then performs beta-eta-normalization           *)
 (* ------------------------------------------------------------------------- *)
 
 (* int -> Tactical.tactic *)
 
-fun pre_cnf_tac i = rtac ccontr i THEN ObjectLogic.atomize_tac i;
+fun pre_cnf_tac i = rtac ccontr i THEN ObjectLogic.atomize_tac i THEN
+  (fn st => Seq.single (Thm.equal_elim (Drule.beta_eta_conversion (cprop_of st)) st));
 
 (* ------------------------------------------------------------------------- *)
 (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
diff -r fc4c6458d569 -r 1724ec4032c5 src/HOL/ex/SAT_Examples.thy
--- a/src/HOL/ex/SAT_Examples.thy	Tue May 02 16:19:53 2006 +0200
+++ b/src/HOL/ex/SAT_Examples.thy	Tue May 02 19:23:48 2006 +0200
@@ -64,6 +64,11 @@
 ~(c | (~p & (p | (q & ~q)))) |] ==> False"
 by satx
 
+text {* eta-Equivalence *}
+
+lemma "(ALL x. P x) | ~ All P"
+by sat
+
 ML {* reset sat.trace_sat; *}
 ML {* reset quick_and_dirty; *}