# HG changeset patch
# User blanchet
# Date 1280252479 -7200
# Node ID 22dcaec5fa77eb224623d4601dc54be135cb3317
# Parent  505657ddb0479feb1a143d5638b023e5c1002da9
minor refactoring

diff -r 505657ddb047 -r 22dcaec5fa77 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Tue Jul 27 19:17:15 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Tue Jul 27 19:41:19 2010 +0200
@@ -1,6 +1,6 @@
 (*  Title:      HOL/Sledgehammer.thy
     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
-    Author:     Jia Meng, NICTA
+    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     Author:     Fabian Immler, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
 *)
diff -r 505657ddb047 -r 22dcaec5fa77 src/HOL/Tools/Sledgehammer/clausifier.ML
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Jul 27 19:17:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Tue Jul 27 19:41:19 2010 +0200
@@ -8,8 +8,8 @@
 signature CLAUSIFIER =
 sig
   val introduce_combinators_in_cterm : cterm -> thm
+  val introduce_combinators_in_theorem : thm -> thm
   val cnf_axiom: theory -> thm -> thm list
-  val neg_clausify: thm -> thm list
 end;
 
 structure Clausifier : CLAUSIFIER =
@@ -251,16 +251,4 @@
 (* FIXME: is transfer necessary? *)
 fun cnf_axiom thy = skolemize_theorem thy o Thm.transfer thy
 
-
-(*** Converting a subgoal into negated conjecture clauses. ***)
-
-fun neg_skolemize_tac ctxt =
-  EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt]
-
-val neg_clausify =
-  single
-  #> Meson.make_clauses_unsorted
-  #> map introduce_combinators_in_theorem
-  #> Meson.finish_cnf
-
 end;
diff -r 505657ddb047 -r 22dcaec5fa77 src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Jul 27 19:17:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Tue Jul 27 19:41:19 2010 +0200
@@ -15,10 +15,10 @@
   datatype arLit =
     TConsLit of name * name * name list |
     TVarLit of name * name
-  datatype arity_clause = ArityClause of
-   {axiom_name: string, conclLit: arLit, premLits: arLit list}
-  datatype class_rel_clause = ClassRelClause of
-   {axiom_name: string, subclass: name, superclass: name}
+  datatype arity_clause =
+    ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
+  datatype class_rel_clause =
+    ClassRelClause of {axiom_name: string, subclass: name, superclass: name}
   datatype combtyp =
     CombTVar of name |
     CombTFree of name |
diff -r 505657ddb047 -r 22dcaec5fa77 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jul 27 19:17:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Jul 27 19:41:19 2010 +0200
@@ -775,6 +775,12 @@
 val type_has_top_sort =
   exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
 
+val neg_clausify =
+  single
+  #> Meson.make_clauses_unsorted
+  #> map Clausifier.introduce_combinators_in_theorem
+  #> Meson.finish_cnf
+
 fun generic_metis_tac mode ctxt ths i st0 =
   let
     val _ = trace_msg (fn () =>
@@ -783,7 +789,7 @@
     if exists_type type_has_top_sort (prop_of st0) then
       (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
     else
-      Meson.MESON (maps Clausifier.neg_clausify)
+      Meson.MESON (maps neg_clausify)
                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
                   ctxt i st0
      handle ERROR msg => raise METIS ("generic_metis_tac", msg)
diff -r 505657ddb047 -r 22dcaec5fa77 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 27 19:17:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Jul 27 19:41:19 2010 +0200
@@ -62,11 +62,11 @@
 structure Sledgehammer : SLEDGEHAMMER =
 struct
 
+open ATP_Problem
+open ATP_Systems
 open Metis_Clauses
 open Sledgehammer_Util
 open Sledgehammer_Fact_Filter
-open ATP_Problem
-open ATP_Systems
 open Sledgehammer_Proof_Reconstruct
 
 
diff -r 505657ddb047 -r 22dcaec5fa77 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jul 27 19:17:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jul 27 19:41:19 2010 +0200
@@ -17,10 +17,10 @@
 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
 struct
 
+open ATP_Systems
 open Sledgehammer_Util
 open Sledgehammer_Fact_Filter
 open Sledgehammer
-open ATP_Systems
 open Sledgehammer_Fact_Minimizer
 
 (** Sledgehammer commands **)
diff -r 505657ddb047 -r 22dcaec5fa77 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Jul 27 19:17:15 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Jul 27 19:41:19 2010 +0200
@@ -27,10 +27,10 @@
 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
 struct
 
+open ATP_Problem
 open Metis_Clauses
 open Sledgehammer_Util
 open Sledgehammer_Fact_Filter
-open ATP_Problem
 
 type minimize_command = string list -> string