adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
--- a/src/HOL/Sledgehammer.thy Sat Jun 12 15:48:17 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Mon Jun 14 10:36:01 2010 +0200
@@ -25,11 +25,8 @@
("Tools/Sledgehammer/metis_tactics.ML")
begin
-definition skolem_Eps :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
-[no_atp]: "skolem_Eps = Eps"
-
-lemma skolem_someI_ex [no_atp]: "\<exists>x. P x \<Longrightarrow> P (skolem_Eps (\<lambda>x. P x))"
-unfolding skolem_Eps_def by (rule someI_ex)
+definition skolem_id :: "'a \<Rightarrow> 'a" where
+[no_atp]: "skolem_id = (\<lambda>x. x)"
definition COMBI :: "'a \<Rightarrow> 'a" where
[no_atp]: "COMBI P \<equiv> P"
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Sat Jun 12 15:48:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Jun 14 10:36:01 2010 +0200
@@ -139,7 +139,7 @@
let
val thy = ProofContext.theory_of ctxt
val (skolem_somes, (mlits, types_sorts)) =
- th |> prop_of |> kill_skolem_Eps j skolem_somes
+ th |> prop_of |> conceal_skolem_somes j skolem_somes
||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
in
if is_conjecture then
@@ -235,24 +235,14 @@
SOME tf => mk_tfree ctxt tf
| NONE => raise Fail ("fol_type_to_isa: " ^ x));
-fun reintroduce_skolem_Eps thy skolem_somes =
- let
- fun aux Ts args t =
- case t of
- t1 $ t2 => aux Ts (aux Ts [] t2 :: args) t1
- | Abs (s, T, t') => list_comb (Abs (s, T, aux (T :: Ts) [] t'), args)
- | Const (s, T) =>
- if String.isPrefix skolem_Eps_pseudo_theory s then
- let
- val (T', args', def') = AList.lookup (op =) skolem_somes s |> the
- in
- def' |> subst_free (args' ~~ args)
- |> map_types Type_Infer.paramify_vars
- end
- else
- list_comb (t, args)
- | t => list_comb (t, args)
- in aux [] [] end
+fun reveal_skolem_somes skolem_somes =
+ map_aterms (fn t as Const (s, T) =>
+ if String.isPrefix skolem_theory_name s then
+ AList.lookup (op =) skolem_somes s
+ |> the |> map_types Type_Infer.paramify_vars
+ else
+ t
+ | t => t)
(*Maps metis terms to isabelle terms*)
fun hol_term_from_fol_PT ctxt fol_tm =
@@ -360,8 +350,7 @@
val ts = map (hol_term_from_fol mode ctxt) fol_tms
val _ = trace_msg (fn () => " calling type inference:")
val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
- val ts' =
- ts |> map (reintroduce_skolem_Eps thy skolem_somes) |> infer_types ctxt
+ val ts' = ts |> map (reveal_skolem_somes skolem_somes) |> infer_types ctxt
val _ = app (fn t => trace_msg
(fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
" of type " ^ Syntax.string_of_typ ctxt (type_of t)))
@@ -418,7 +407,7 @@
fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
fun subst_translation (x,y) =
let val v = find_var x
- (* We call "reintroduce_skolem_Eps" and "infer_types" below. *)
+ (* We call "reveal_skolem_somes" and "infer_types" below. *)
val t = hol_term_from_fol mode ctxt y
in SOME (cterm_of thy (Var v), t) end
handle Option =>
@@ -434,7 +423,7 @@
val _ = trace_msg (fn () => " isa th: " ^ Display.string_of_thm ctxt i_th)
val substs = map_filter remove_typeinst (Metis.Subst.toList fsubst)
val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
- val tms = rawtms |> map (reintroduce_skolem_Eps thy skolem_somes)
+ val tms = rawtms |> map (reveal_skolem_somes skolem_somes)
|> infer_types ctxt
val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
val substs' = ListPair.zip (vars, map ctm_of tms)
@@ -638,7 +627,7 @@
type logic_map =
{axioms: (Metis.Thm.thm * thm) list,
tfrees: type_literal list,
- skolem_somes: (string * (typ * term list * term)) list}
+ skolem_somes: (string * term) list}
fun const_in_metis c (pred, tm_list) =
let
@@ -708,12 +697,7 @@
val lmap =
lmap |> mode <> FO
? fold (add_thm false) (thEQ @ thS @ thC @ thB @ thK @ thI)
- in
- (mode, add_type_thm (type_ext thy
- (* FIXME: Call"kill_skolem_Eps" here? *)
- (map ((*snd o kill_skolem_Eps ~1 skolem_somes o*) prop_of)
- (cls @ ths))) lmap)
- end;
+ in (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap) end
fun refute cls =
Metis.Resolution.loop (Metis.Resolution.new Metis.Resolution.default cls);
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Sat Jun 12 15:48:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Jun 14 10:36:01 2010 +0200
@@ -117,7 +117,7 @@
add_const_typ_table (const_with_typ thy (c,typ), tab)
| add_term_consts_typs_rm thy (Free(c, typ), tab) =
add_const_typ_table (const_with_typ thy (c,typ), tab)
- | add_term_consts_typs_rm _ (Const (@{const_name skolem_Eps}, _) $ _, tab) =
+ | add_term_consts_typs_rm _ (Const (@{const_name skolem_id}, _) $ _, tab) =
tab
| add_term_consts_typs_rm thy (t $ u, tab) =
add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab))
@@ -471,7 +471,8 @@
(* ATP invocation methods setup *)
(***************************************************************)
-fun is_quasi_fol_term thy = Meson.is_fol_term thy o snd o kill_skolem_Eps ~1 []
+fun is_quasi_fol_term thy =
+ Meson.is_fol_term thy o snd o conceal_skolem_somes ~1 []
(*Ensures that no higher-order theorems "leak out"*)
fun restrict_to_logic thy true cls =
--- 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)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Sat Jun 12 15:48:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Mon Jun 14 10:36:01 2010 +0200
@@ -29,9 +29,8 @@
val type_of_combterm : combterm -> fol_type
val strip_combterm_comb : combterm -> combterm * combterm list
val literals_of_term : theory -> term -> literal list * typ list
- val kill_skolem_Eps :
- int -> (string * (typ * term list * term)) list -> term
- -> (string * (typ * term list * term)) list * term
+ val conceal_skolem_somes :
+ int -> (string * term) list -> term -> (string * term) list * term
exception TRIVIAL
val make_conjecture_clauses : bool -> theory -> thm list -> hol_clause list
val make_axiom_clauses : bool -> theory ->
@@ -123,7 +122,7 @@
let
val (tp, ts) = type_of dfg T
val tvar_list =
- (if String.isPrefix skolem_Eps_pseudo_theory c then
+ (if String.isPrefix skolem_theory_name c then
[] |> Term.add_tvarsT T |> map TVar
else
(c, T) |> Sign.const_typargs thy)
@@ -163,46 +162,24 @@
skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
skolem_infix ^ "g"
-val flip_type =
- map_atyps (fn TFree (s, S) => TVar ((s, 0), S)
- | TVar ((s, 0), S) => TFree (s, S)
- | T as TVar (_, S) => raise TYPE ("nonzero TVar", [T], [])
- | T => T)
-val flip_term =
- map_aterms (fn Free (s, T) => Var ((s, 0), T)
- | Var ((s, 0), T) => Free (s, T)
- | t as Var (_, S) => raise TERM ("nonzero Var", [t])
- | t => t)
- #> map_types flip_type
-
-fun flipped_skolem_type_and_args bound_T body =
- skolem_type_and_args (flip_type bound_T) (flip_term body)
- |>> flip_type ||> map flip_term
-
-fun triple_aconv ((T1, ts1, t1), (T2, ts2, t2)) =
- T1 = T2 andalso length ts1 = length ts2 andalso
- forall (op aconv) (ts1 ~~ ts2) andalso t1 aconv t2
-
-fun kill_skolem_Eps i skolem_somes t =
- if exists_Const (curry (op =) @{const_name skolem_Eps} o fst) t then
+fun conceal_skolem_somes i skolem_somes t =
+ if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
let
fun aux skolem_somes
- (t as (Const (@{const_name skolem_Eps}, eps_T) $ t2)) =
+ (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
let
- val bound_T = range_type eps_T
- val (T, args) = flipped_skolem_type_and_args bound_T t2
val (skolem_somes, s) =
if i = ~1 then
(skolem_somes, @{const_name undefined})
- else case AList.find triple_aconv skolem_somes (T, args, t) of
+ else case AList.find (op aconv) skolem_somes t of
s :: _ => (skolem_somes, s)
| _ =>
let
- val s = skolem_Eps_pseudo_theory ^ "." ^
+ val s = skolem_theory_name ^ "." ^
skolem_name i (length skolem_somes)
(length (Term.add_tvarsT T []))
- in ((s, (T, args, t)) :: skolem_somes, s) end
- in (skolem_somes, list_comb (Const (s, T), args)) end
+ in ((s, t) :: skolem_somes, s) end
+ in (skolem_somes, Const (s, T)) end
| aux skolem_somes (t1 $ t2) =
let
val (skolem_somes, t1) = aux skolem_somes t1
@@ -224,7 +201,7 @@
fun make_clause dfg thy (clause_id, axiom_name, kind, th) skolem_somes =
let
val (skolem_somes, t) =
- th |> prop_of |> kill_skolem_Eps clause_id skolem_somes
+ th |> prop_of |> conceal_skolem_somes clause_id skolem_somes
val (lits, ctypes_sorts) = literals_of_term_dfg dfg thy t
in
if forall isFalse lits then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sat Jun 12 15:48:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon Jun 14 10:36:01 2010 +0200
@@ -261,8 +261,8 @@
(instances of) Skolem pseudoconstants, this information is encoded in the
constant name. *)
fun num_type_args thy s =
- if String.isPrefix skolem_Eps_pseudo_theory s then
- s |> unprefix skolem_Eps_pseudo_theory
+ if String.isPrefix skolem_theory_name s then
+ s |> unprefix skolem_theory_name
|> space_explode skolem_infix |> hd
|> space_explode "_" |> List.last |> Int.fromString |> the
else
@@ -324,7 +324,7 @@
else
(* Extra args from "hAPP" come after any arguments
given directly to the constant. *)
- if String.isPrefix skolem_Eps_pseudo_theory c then
+ if String.isPrefix skolem_theory_name c then
map fastype_of ts ---> HOLogic.typeT
else
Sign.const_instance thy (c,
--- a/src/HOL/Tools/meson.ML Sat Jun 12 15:48:17 2010 +0200
+++ b/src/HOL/Tools/meson.ML Mon Jun 14 10:36:01 2010 +0200
@@ -98,9 +98,8 @@
val tmA = concl_of thA
val Const("==>",_) $ tmB $ _ = prop_of thB
val tenv =
- Pattern.first_order_match thy
- (pairself Envir.beta_eta_contract (tmB, tmA))
- (Vartab.empty, Vartab.empty) |> snd
+ Pattern.first_order_match thy (tmB, tmA)
+ (Vartab.empty, Vartab.empty) |> snd
val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
in thA RS (cterm_instantiate ct_pairs thB) end) () of
SOME th => th
@@ -317,17 +316,17 @@
val has_meta_conn =
exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
-fun apply_skolem_ths (th, rls) =
+fun apply_skolem_theorem (th, rls) =
let
- fun tryall [] = raise THM ("apply_skolem_ths", 0, th::rls)
+ fun tryall [] = raise THM ("apply_skolem_theorem", 0, th::rls)
| tryall (rl :: rls) =
first_order_resolve th rl handle THM _ => tryall rls
in tryall rls end
-(*Conjunctive normal form, adding clauses from th in front of ths (for foldr).
- Strips universal quantifiers and breaks up conjunctions.
- Eliminates existential quantifiers using skoths: Skolemization theorems.*)
-fun cnf skoths ctxt (th,ths) =
+(* Conjunctive normal form, adding clauses from th in front of ths (for foldr).
+ Strips universal quantifiers and breaks up conjunctions.
+ Eliminates existential quantifiers using Skolemization theorems. *)
+fun cnf skolem_ths ctxt (th, ths) =
let val ctxtr = Unsynchronized.ref ctxt (* FIXME ??? *)
fun cnf_aux (th,ths) =
if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
@@ -341,7 +340,7 @@
in ctxtr := ctxt'; cnf_aux (th', ths) end
| Const ("Ex", _) =>
(*existential quantifier: Insert Skolem functions*)
- cnf_aux (apply_skolem_ths (th,skoths), ths)
+ cnf_aux (apply_skolem_theorem (th, skolem_ths), ths)
| Const ("op |", _) =>
(*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
all combinations of converting P, Q to CNF.*)
@@ -357,7 +356,7 @@
else cnf_aux (th,ths)
in (cls, !ctxtr) end;
-fun make_cnf skoths th ctxt = cnf skoths ctxt (th, []);
+fun make_cnf skolem_ths th ctxt = cnf skolem_ths ctxt (th, []);
(*Generalization, removal of redundant equalities, removal of tautologies.*)
fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);