--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Jun 29 10:36:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Jun 29 10:56:45 2010 +0200
@@ -7,9 +7,9 @@
signature CLAUSIFIER =
sig
- val cnf_axiom: theory -> thm -> thm list
+ val cnf_axiom: theory -> bool -> thm -> thm list
val cnf_rules_pairs :
- theory -> (string * thm) list -> ((string * int) * thm) list
+ theory -> bool -> (string * thm) list -> ((string * int) * thm) list
val neg_clausify: thm -> thm list
val neg_conjecture_clauses:
Proof.context -> thm -> int -> thm list list * (string * typ) list
@@ -193,7 +193,7 @@
(* Given the definition of a Skolem function, return a theorem to replace
an existential formula by a use of that function.
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
-fun skolem_theorem_of_def thy rhs0 =
+fun skolem_theorem_of_def thy cheat rhs0 =
let
val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of thy
val rhs' = rhs |> Thm.dest_comb |> snd
@@ -213,10 +213,13 @@
THEN rtac ((prem |> rewrite_rule skolem_id_def_raw)
RS @{thm someI_ex}) 1
in
- Goal.prove_internal [ex_tm] conc tacf
- |> forall_intr_list frees
- |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
- |> Thm.varifyT_global
+ (if cheat then
+ Skip_Proof.make_thm thy (Logic.mk_implies (pairself term_of (ex_tm, conc)))
+ else
+ Goal.prove_internal [ex_tm] conc tacf
+ |> forall_intr_list frees
+ |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
+ |> Thm.varifyT_global)
end
(*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
@@ -229,11 +232,12 @@
in (th3, ctxt) end;
(*Skolemize a named theorem, with Skolem functions as additional premises.*)
-fun skolemize_theorem thy th =
+fun skolemize_theorem thy cheat th =
let
val ctxt0 = Variable.global_thm_context th
val (nnfth, ctxt) = to_nnf th ctxt0
- val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs nnfth)
+ val sko_ths = map (skolem_theorem_of_def thy cheat)
+ (assume_skolem_funs nnfth)
val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
in
cnfs |> map introduce_combinators
@@ -245,13 +249,13 @@
(* Convert Isabelle theorems into axiom clauses. *)
(* FIXME: is transfer necessary? *)
-fun cnf_axiom thy = skolemize_theorem thy o Thm.transfer thy
+fun cnf_axiom thy cheat = skolemize_theorem thy cheat o Thm.transfer thy
(**** Translate a set of theorems into CNF ****)
(*The combination of rev and tail recursion preserves the original order*)
-fun cnf_rules_pairs thy =
+fun cnf_rules_pairs thy cheat =
let
fun do_one _ [] = []
| do_one ((name, k), th) (cls :: clss) =
@@ -259,7 +263,7 @@
fun do_all pairs [] = pairs
| do_all pairs ((name, th) :: ths) =
let
- val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th)
+ val new_pairs = do_one ((name, 0), th) (cnf_axiom thy cheat th)
handle THM _ => []
in do_all (new_pairs @ pairs) ths end
in do_all [] o rev end