--- 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
*)
--- 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;
--- 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 |
--- 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)
--- 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
--- 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 **)
--- 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