--- a/NEWS Tue Jun 15 07:41:37 2010 +0200
+++ b/NEWS Tue Jun 15 07:42:48 2010 +0200
@@ -25,6 +25,9 @@
INCOMPATIBILITY.
+* Removed simplifier congruence rule of "prod_case", as has for long
+been the case with "split".
+
* Datatype package: theorems generated for executable equality
(class eq) carry proper names and are treated as default code
equations.
@@ -33,6 +36,7 @@
generating Haskell code.
+
New in Isabelle2009-2 (June 2010)
---------------------------------
--- a/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 15 07:41:37 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Tue Jun 15 07:42:48 2010 +0200
@@ -338,11 +338,13 @@
Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the
environment variable \texttt{SPASS\_HOME} to the directory that contains the
\texttt{SPASS} executable, or install the prebuilt SPASS package from Isabelle's
-download page. See \S\ref{installation} for details.
+download page. Sledgehammer requires version 3.5 or above. See
+\S\ref{installation} for details.
-\item[$\bullet$] \textbf{\textit{spass\_tptp}:} Same as the above, except that
-Sledgehammer communicates with SPASS using the TPTP syntax rather than the
-native DFG syntax. This ATP is provided for experimental purposes.
+\item[$\bullet$] \textbf{\textit{spass\_dfg}:} Same as the above, except that
+Sledgehammer communicates with SPASS using the native DFG syntax rather than the
+TPTP syntax. Sledgehammer requires version 3.0 or above. This ATP is provided
+for compatibility reasons.
\item[$\bullet$] \textbf{\textit{vampire}:} Vampire is an ATP developed by
Andrei Voronkov and his colleagues \cite{riazanov-voronkov-2002}. To use
--- a/src/HOL/Decision_Procs/Approximation.thy Tue Jun 15 07:41:37 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Tue Jun 15 07:42:48 2010 +0200
@@ -2552,9 +2552,7 @@
where l_eq: "Some (l, u') = approx prec a vs"
and u_eq: "Some (l', u) = approx prec b vs"
and approx_form': "approx_form' prec f (ss ! n) n l u vs ss"
- by (cases "approx prec a vs", simp,
- cases "approx prec b vs", auto) blast
-
+ by (cases "approx prec a vs", simp) (cases "approx prec b vs", auto)
{ assume "xs ! n \<in> { interpret_floatarith a xs .. interpret_floatarith b xs }"
with approx[OF Bound.prems(2) l_eq] and approx[OF Bound.prems(2) u_eq]
have "xs ! n \<in> { real l .. real u}" by auto
--- a/src/HOL/Product_Type.thy Tue Jun 15 07:41:37 2010 +0200
+++ b/src/HOL/Product_Type.thy Tue Jun 15 07:42:48 2010 +0200
@@ -158,6 +158,8 @@
by (simp add: Pair_def Abs_prod_inject)
qed
+declare weak_case_cong [cong del]
+
subsubsection {* Tuple syntax *}
--- a/src/HOL/Sledgehammer.thy Tue Jun 15 07:41:37 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Tue Jun 15 07:42:48 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/ATP_Manager/atp_manager.ML Tue Jun 15 07:41:37 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Tue Jun 15 07:42:48 2010 +0200
@@ -34,8 +34,8 @@
axiom_clauses: (thm * (string * int)) list option,
filtered_clauses: (thm * (string * int)) list option}
datatype failure =
- Unprovable | TimedOut | OutOfResources | OldSpass | MalformedInput |
- MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
+ MalformedInput | MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,
message: string,
@@ -95,8 +95,8 @@
filtered_clauses: (thm * (string * int)) list option};
datatype failure =
- Unprovable | TimedOut | OutOfResources | OldSpass | MalformedInput |
- MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
+ MalformedInput | MalformedOutput | UnknownError
type prover_result =
{outcome: failure option,
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 15 07:41:37 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Tue Jun 15 07:42:48 2010 +0200
@@ -87,6 +87,8 @@
| (failure :: _) => ("", SOME failure)
fun string_for_failure Unprovable = "The ATP problem is unprovable."
+ | string_for_failure IncompleteUnprovable =
+ "The ATP cannot prove the problem."
| string_for_failure TimedOut = "Timed out."
| string_for_failure OutOfResources = "The ATP ran out of resources."
| string_for_failure OldSpass =
@@ -274,9 +276,9 @@
"======= End of refutation ======="),
("% SZS output start Refutation", "% SZS output end Refutation")],
known_failures =
- [(Unprovable, "Satisfiability detected"),
- (Unprovable, "UNPROVABLE"),
- (Unprovable, "CANNOT PROVE"),
+ [(Unprovable, "UNPROVABLE"),
+ (IncompleteUnprovable, "CANNOT PROVE"),
+ (Unprovable, "Satisfiability detected"),
(OutOfResources, "Refutation not found")],
max_axiom_clauses = 60,
prefers_theory_relevant = false}
@@ -329,39 +331,29 @@
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
-val spass_config : prover_config =
+fun generic_spass_config dfg : prover_config =
{home_var = "SPASS_HOME",
executable = "SPASS",
arguments = fn timeout =>
"-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
- \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout),
+ \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout)
+ |> not dfg ? prefix "-TPTP ",
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
- [(Unprovable, "SPASS beiseite: Completion found"),
+ [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
(TimedOut, "SPASS beiseite: Ran out of time"),
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
- (MalformedInput, "Undefined symbol")],
+ (MalformedInput, "Undefined symbol"),
+ (MalformedInput, "Free Variable"),
+ (OldSpass, "unrecognized option `-TPTP'"),
+ (OldSpass, "Unrecognized option TPTP")],
max_axiom_clauses = 40,
prefers_theory_relevant = true}
-val spass = dfg_prover "spass" spass_config
-
-(* SPASS 3.7 supports both the DFG and the TPTP syntax, whereas SPASS 3.0
- supports only the DFG syntax. As soon as all Isabelle repository/snapshot
- users have upgraded to 3.7, we can kill "spass" (and all DFG support in
- Sledgehammer) and rename "spass_tptp" "spass". *)
+val spass_dfg_config = generic_spass_config true
+val spass_dfg = dfg_prover "spass_dfg" spass_dfg_config
-val spass_tptp_config =
- {home_var = #home_var spass_config,
- executable = #executable spass_config,
- arguments = prefix "-TPTP " o #arguments spass_config,
- proof_delims = #proof_delims spass_config,
- known_failures =
- #known_failures spass_config @
- [(OldSpass, "unrecognized option `-TPTP'"),
- (OldSpass, "Unrecognized option TPTP")],
- max_axiom_clauses = #max_axiom_clauses spass_config,
- prefers_theory_relevant = #prefers_theory_relevant spass_config}
-val spass_tptp = tptp_prover "spass_tptp" spass_tptp_config
+val spass_config = generic_spass_config false
+val spass = tptp_prover "spass" spass_config
(* remote prover invocation via SystemOnTPTP *)
@@ -423,7 +415,7 @@
remotify (fst vampire)]
val provers =
- [spass, spass_tptp, vampire, e, remote_vampire, remote_spass, remote_e]
+ [spass, spass_dfg, vampire, e, remote_vampire, remote_spass, remote_e]
val prover_setup = fold add_prover provers
val setup =
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 15 07:41:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Jun 15 07:42:48 2010 +0200
@@ -44,14 +44,16 @@
(* Useful Functions *)
(* ------------------------------------------------------------------------- *)
-(* match untyped terms*)
-fun untyped_aconv (Const(a,_)) (Const(b,_)) = (a=b)
- | untyped_aconv (Free(a,_)) (Free(b,_)) = (a=b)
- | untyped_aconv (Var((a,_),_)) (Var((b,_),_)) = (a=b) (*the index is ignored!*)
- | untyped_aconv (Bound i) (Bound j) = (i=j)
- | untyped_aconv (Abs(a,_,t)) (Abs(b,_,u)) = (a=b) andalso untyped_aconv t u
- | untyped_aconv (t1$t2) (u1$u2) = untyped_aconv t1 u1 andalso untyped_aconv t2 u2
- | untyped_aconv _ _ = false;
+(* Match untyped terms. *)
+fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
+ | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
+ | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) =
+ (a = b) (* The index is ignored, for some reason. *)
+ | untyped_aconv (Bound i) (Bound j) = (i = j)
+ | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
+ | untyped_aconv (t1 $ t2) (u1 $ u2) =
+ untyped_aconv t1 u1 andalso untyped_aconv t2 u2
+ | untyped_aconv _ _ = false
(* Finding the relative location of an untyped term within a list of terms *)
fun get_index lit =
@@ -139,7 +141,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 +237,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 +352,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 +409,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 +425,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 +629,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 +699,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 Tue Jun 15 07:41:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Jun 15 07:42:48 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_minimizer.ML Tue Jun 15 07:41:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jun 15 07:42:48 2010 +0200
@@ -38,6 +38,7 @@
(* wrapper for calling external prover *)
fun string_for_failure Unprovable = "Unprovable."
+ | string_for_failure IncompleteUnprovable = "Failed."
| string_for_failure TimedOut = "Timed out."
| string_for_failure OutOfResources = "Failed."
| string_for_failure OldSpass = "Error."
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Jun 15 07:41:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Jun 15 07:42:48 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)
@@ -194,7 +195,11 @@
strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
| _ => th;
-val lambda_free = not o Term.has_abs;
+fun is_quasi_lambda_free (Const (@{const_name skolem_id}, _) $ _) = true
+ | is_quasi_lambda_free (t1 $ t2) =
+ is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
+ | is_quasi_lambda_free (Abs _) = false
+ | is_quasi_lambda_free _ = true
val [f_B,g_B] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_B}));
val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
@@ -245,7 +250,7 @@
(* Traverse a theorem, remplacing lambda-abstractions with combinators. *)
fun do_introduce_combinators ct =
- if lambda_free (term_of ct) then
+ if is_quasi_lambda_free (term_of ct) then
Thm.reflexive ct
else case term_of ct of
Abs _ =>
@@ -263,7 +268,7 @@
end
fun introduce_combinators th =
- if lambda_free (prop_of th) then
+ if is_quasi_lambda_free (prop_of th) then
th
else
let
@@ -295,23 +300,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 +406,8 @@
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 inline = false (* FIXME: temporary *)
val defs = skolem_theorems_of_assume inline s nnfth
val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt
in
@@ -434,8 +438,8 @@
fun cnf_axiom thy th0 =
let val th = Thm.transfer thy th0 in
case lookup_cache thy th of
- NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th)
- | SOME cls => cls
+ SOME cls => cls
+ | NONE => map Thm.close_derivation (skolemize_theorem (fake_name th) th)
end;
@@ -444,15 +448,17 @@
fun pair_name_cls k (n, []) = []
| pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
-fun cnf_rules_pairs_aux _ pairs [] = pairs
- | cnf_rules_pairs_aux thy pairs ((name,th)::ths) =
- let val pairs' = (pair_name_cls 0 (name, cnf_axiom thy th)) @ pairs
- handle THM _ => pairs |
- CLAUSE _ => pairs
- in cnf_rules_pairs_aux thy pairs' ths end;
-
(*The combination of rev and tail recursion preserves the original order*)
-fun cnf_rules_pairs thy l = cnf_rules_pairs_aux thy [] (rev l);
+fun cnf_rules_pairs thy =
+ let
+ fun aux pairs [] = pairs
+ | aux pairs ((name, th) :: ths) =
+ let
+ val new_pairs = pair_name_cls 0 (name, cnf_axiom thy th)
+ handle THM _ => [] |
+ CLAUSE _ => []
+ in aux (new_pairs @ pairs) ths end
+ in aux [] o rev end
(**** Convert all facts of the theory into FOL or HOL clauses ****)
@@ -492,7 +498,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)
@@ -517,9 +524,9 @@
if !use_skolem_cache then saturate_skolem_cache thy else NONE
-(*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are
- lambda_free, but then the individual theory caches become much bigger.*)
-
+(* The cache can be kept smaller by inspecting the prop of each thm. Can ignore
+ all that are quasi-lambda-free, but then the individual theory caches become
+ much bigger. *)
fun strip_subgoal goal i =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Tue Jun 15 07:41:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Tue Jun 15 07:42:48 2010 +0200
@@ -193,8 +193,7 @@
tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
-val max_dfg_symbol_length =
- if is_new_spass_version then 1000000 (* arbitrary large number *) else 63
+val max_dfg_symbol_length = 63
(* HACK because SPASS 3.0 truncates identifiers to 63 characters. *)
fun controlled_length dfg s =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Jun 15 07:41:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Tue Jun 15 07:42:48 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
@@ -446,10 +423,13 @@
fold (add_literal_decls params) literals decls
handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
-fun decls_of_clauses params clauses arity_clauses =
- let val functab =
- init_functab |> fold Symtab.update [(type_wrapper_name, 2), ("hAPP", 2),
- ("tc_bool", 0)]
+fun decls_of_clauses (params as (full_types, explicit_apply, _, _)) clauses
+ arity_clauses =
+ let
+ val functab =
+ init_functab
+ |> fold Symtab.update [(type_wrapper_name, 2), ("hAPP", 2),
+ ("tc_bool", 0)]
val predtab = Symtab.empty |> Symtab.update ("hBOOL", 1)
val (functab, predtab) =
(functab, predtab) |> fold (add_clause_decls params) clauses
@@ -618,7 +598,8 @@
val tfree_preds = map dfg_tfree_predicate tfree_lits
val (helper_clauses_strs, pool) =
pool_map (apfst fst oo dfg_clause params) helper_clauses pool
- val (funcs, cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
+ val (funcs, cl_preds) =
+ decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
val ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
val preds = tfree_preds @ cl_preds @ ty_preds
val conjecture_offset =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jun 15 07:41:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Jun 15 07:42:48 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/Sledgehammer/sledgehammer_util.ML Tue Jun 15 07:41:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Jun 15 07:42:48 2010 +0200
@@ -6,7 +6,6 @@
signature SLEDGEHAMMER_UTIL =
sig
- val is_new_spass_version : bool
val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
val plural_s : int -> string
val serial_commas : string -> string list -> string list
@@ -25,18 +24,6 @@
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
struct
-val is_new_spass_version =
- case getenv "SPASS_VERSION" of
- "" => (case getenv "SPASS_HOME" of
- "" => false
- | s =>
- (* Hack: Preliminary versions of the SPASS 3.7 package don't set
- "SPASS_VERSION". *)
- String.isSubstring "/spass-3.7/" s)
- | s => (case s |> space_explode "." |> map Int.fromString of
- SOME m :: SOME n :: _ => m > 3 orelse (m = 3 andalso n >= 5)
- | _ => false)
-
fun pairf f g x = (f x, g x)
fun plural_s n = if n = 1 then "" else "s"
--- a/src/HOL/Tools/meson.ML Tue Jun 15 07:41:37 2010 +0200
+++ b/src/HOL/Tools/meson.ML Tue Jun 15 07:42:48 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);