--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat Jun 12 15:48:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Jun 14 10:36:01 2010 +0200
@@ -10,11 +10,10 @@
val chained_prefix: string
val trace: bool Unsynchronized.ref
val trace_msg: (unit -> string) -> unit
- val skolem_Eps_pseudo_theory: string
+ val skolem_theory_name: string
val skolem_prefix: string
val skolem_infix: string
val is_skolem_const_name: string -> bool
- val skolem_type_and_args: typ -> term -> typ * term list
val cnf_axiom: theory -> thm -> thm list
val multi_base_blacklist: string list
val is_theorem_bad_for_atps: thm -> bool
@@ -42,7 +41,7 @@
val trace = Unsynchronized.ref false;
fun trace_msg msg = if !trace then tracing (msg ()) else ();
-val skolem_Eps_pseudo_theory = "Sledgehammer.Eps"
+val skolem_theory_name = "Sledgehammer.Sko"
val skolem_prefix = "sko_"
val skolem_infix = "$"
@@ -76,9 +75,6 @@
(**** SKOLEMIZATION BY INFERENCE (lcp) ****)
-fun skolem_Eps_const T =
- Const (@{const_name skolem_Eps}, (T --> HOLogic.boolT) --> T)
-
(*Keep the full complexity of the original name*)
fun flatten_name s = space_implode "_X" (Long_Name.explode s);
@@ -120,7 +116,7 @@
val id = skolem_name s (Unsynchronized.inc skolem_count) s'
val (cT, args) = skolem_type_and_args T body
val rhs = list_abs_free (map dest_Free args,
- skolem_Eps_const T $ body)
+ HOLogic.choice_const T $ body)
(*Forms a lambda-abstraction over the formal parameters*)
val (c, thy) =
Sign.declare_const ((Binding.conceal (Binding.name id), cT), NoSyn) thy
@@ -139,6 +135,9 @@
| dec_sko t thx = thx
in dec_sko (prop_of th) ([], thy) end
+fun mk_skolem_id t =
+ let val T = fastype_of t in Const (@{const_name skolem_id}, T --> T) $ t end
+
(*Traverse a theorem, accumulating Skolem function definitions.*)
fun assume_skolem_funs inline s th =
let
@@ -152,7 +151,9 @@
val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
val id = skolem_name s (Unsynchronized.inc skolem_count) s'
val c = Free (id, cT)
- val rhs = list_abs_free (map dest_Free args, skolem_Eps_const T $ body)
+ val rhs = list_abs_free (map dest_Free args,
+ HOLogic.choice_const T $ body)
+ |> inline ? mk_skolem_id
(*Forms a lambda-abstraction over the formal parameters*)
val def = Logic.mk_equals (c, rhs)
val comb = list_comb (if inline then rhs else c, args)
@@ -295,23 +296,26 @@
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
fun skolem_theorem_of_def inline def =
let
- val (c,rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
- val (ch, frees) = c_variant_abs_multi (rhs, [])
- val (chilbert,cabs) = Thm.dest_comb ch
+ val (c, rhs) = Thm.dest_equals (cprop_of (freeze_thm def))
+ val rhs' = rhs |> inline ? (snd o Thm.dest_comb)
+ val (ch, frees) = c_variant_abs_multi (rhs', [])
+ val (chilbert, cabs) = ch |> Thm.dest_comb
val thy = Thm.theory_of_cterm chilbert
val t = Thm.term_of chilbert
val T =
case t of
- Const (@{const_name skolem_Eps}, Type (@{type_name fun}, [_, T])) => T
- | _ => raise THM ("skolem_theorem_of_def: expected \"Eps\"", 0, [def])
+ Const (@{const_name Eps}, Type (@{type_name fun}, [_, T])) => T
+ | _ => raise TERM ("skolem_theorem_of_def: expected \"Eps\"", [t])
val cex = Thm.cterm_of thy (HOLogic.exists_const T)
val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
and conc =
Drule.list_comb (if inline then rhs else c, frees)
|> Drule.beta_conv cabs |> c_mkTrueprop
fun tacf [prem] =
- (if inline then all_tac else rewrite_goals_tac [def])
- THEN rtac (prem RS @{thm skolem_someI_ex}) 1
+ (if inline then rewrite_goals_tac @{thms skolem_id_def_raw}
+ else rewrite_goals_tac [def])
+ THEN rtac ((prem |> inline ? rewrite_rule @{thms 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.*)
@@ -398,12 +402,7 @@
let
val ctxt0 = Variable.global_thm_context th
val (nnfth, ctxt) = to_nnf th ctxt0
-
- val inline = false
-(*
-FIXME: Reintroduce code:
val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth)
-*)
val defs = skolem_theorems_of_assume inline s nnfth
val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
in
@@ -492,7 +491,8 @@
I
else
fold_index (fn (i, th) =>
- if is_theorem_bad_for_atps th orelse is_some (lookup_cache thy th) then
+ if is_theorem_bad_for_atps th orelse
+ is_some (lookup_cache thy th) then
I
else
cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths)