--- a/src/HOL/Orderings.thy Mon Aug 23 11:56:12 2010 +0200
+++ b/src/HOL/Orderings.thy Mon Aug 23 15:30:42 2010 +0200
@@ -1264,7 +1264,8 @@
begin
definition
- top_fun_eq: "top = (\<lambda>x. top)"
+ top_fun_eq [no_atp]: "top = (\<lambda>x. top)"
+declare top_fun_eq_raw [no_atp]
instance proof
qed (simp add: top_fun_eq le_fun_def)
--- a/src/HOL/Predicate.thy Mon Aug 23 11:56:12 2010 +0200
+++ b/src/HOL/Predicate.thy Mon Aug 23 15:30:42 2010 +0200
@@ -92,7 +92,7 @@
lemma top2I [intro!]: "top x y"
by (simp add: top_fun_eq top_bool_eq)
-lemma bot1E [elim!]: "bot x \<Longrightarrow> P"
+lemma bot1E [no_atp, elim!]: "bot x \<Longrightarrow> P"
by (simp add: bot_fun_eq bot_bool_eq)
lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
--- a/src/HOL/Set.thy Mon Aug 23 11:56:12 2010 +0200
+++ b/src/HOL/Set.thy Mon Aug 23 15:30:42 2010 +0200
@@ -495,7 +495,7 @@
apply (rule Collect_mem_eq)
done
-lemma expand_set_eq: "(A = B) = (ALL x. (x:A) = (x:B))"
+lemma expand_set_eq [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
by(auto intro:set_ext)
lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"
@@ -852,7 +852,7 @@
lemma image_iff: "(z : f`A) = (EX x:A. z = f x)"
by blast
-lemma image_subset_iff: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
+lemma image_subset_iff [no_atp]: "(f`A \<subseteq> B) = (\<forall>x\<in>A. f x \<in> B)"
-- {* This rewrite rule would confuse users if made default. *}
by blast
@@ -1203,7 +1203,7 @@
lemma Int_UNIV [simp,no_atp]: "(A \<inter> B = UNIV) = (A = UNIV & B = UNIV)"
by (fact inf_eq_top_iff)
-lemma Int_subset_iff [simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
+lemma Int_subset_iff [no_atp, simp]: "(C \<subseteq> A \<inter> B) = (C \<subseteq> A & C \<subseteq> B)"
by (fact le_inf_iff)
lemma Int_Collect: "(x \<in> A \<inter> {x. P x}) = (x \<in> A & P x)"
@@ -1294,7 +1294,7 @@
lemma Un_empty [iff]: "(A \<union> B = {}) = (A = {} & B = {})"
by (fact sup_eq_bot_iff)
-lemma Un_subset_iff [simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
+lemma Un_subset_iff [no_atp, simp]: "(A \<union> B \<subseteq> C) = (A \<subseteq> C & B \<subseteq> C)"
by (fact le_sup_iff)
lemma Un_Diff_Int: "(A - B) \<union> (A \<inter> B) = A"
@@ -1490,7 +1490,7 @@
lemma set_eq_subset: "(A = B) = (A \<subseteq> B & B \<subseteq> A)"
by blast
-lemma subset_iff: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
+lemma subset_iff [no_atp]: "(A \<subseteq> B) = (\<forall>t. t \<in> A --> t \<in> B)"
by blast
lemma subset_iff_psubset_eq: "(A \<subseteq> B) = ((A \<subset> B) | (A = B))"
--- a/src/HOL/Tools/ATP/atp_systems.ML Mon Aug 23 11:56:12 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Mon Aug 23 15:30:42 2010 +0200
@@ -16,6 +16,7 @@
{exec: string * string,
required_execs: (string * string) list,
arguments: bool -> Time.time -> string,
+ has_incomplete_mode: bool,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
default_max_relevant_per_iter: int,
@@ -48,6 +49,7 @@
{exec: string * string,
required_execs: (string * string) list,
arguments: bool -> Time.time -> string,
+ has_incomplete_mode: bool,
proof_delims: (string * string) list,
known_failures: (failure * string) list,
default_max_relevant_per_iter: int,
@@ -136,6 +138,7 @@
arguments = fn _ => fn timeout =>
"--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^
string_of_int (to_generous_secs timeout),
+ has_incomplete_mode = false,
proof_delims = [tstp_proof_delims],
known_failures =
[(Unprovable, "SZS status: CounterSatisfiable"),
@@ -146,7 +149,7 @@
"# Cannot determine problem status within resource limit"),
(OutOfResources, "SZS status: ResourceOut"),
(OutOfResources, "SZS status ResourceOut")],
- default_max_relevant_per_iter = 50 (* FIXME *),
+ default_max_relevant_per_iter = 60 (* FUDGE *),
default_theory_relevant = false,
explicit_forall = false,
use_conjecture_for_hypotheses = true}
@@ -159,12 +162,11 @@
val spass_config : prover_config =
{exec = ("ISABELLE_ATP", "scripts/spass"),
required_execs = [("SPASS_HOME", "SPASS")],
- (* "div 2" accounts for the fact that SPASS is often run twice. *)
arguments = fn complete => fn timeout =>
("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
- \-VarWeight=3 -TimeLimit=" ^
- string_of_int ((to_generous_secs timeout + 1) div 2))
+ \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout))
|> not complete ? prefix "-SOS=1 ",
+ has_incomplete_mode = true,
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
known_perl_failures @
@@ -174,7 +176,7 @@
(MalformedInput, "Undefined symbol"),
(MalformedInput, "Free Variable"),
(SpassTooOld, "tptp2dfg")],
- default_max_relevant_per_iter = 35 (* FIXME *),
+ default_max_relevant_per_iter = 32 (* FUDGE *),
default_theory_relevant = true,
explicit_forall = true,
use_conjecture_for_hypotheses = true}
@@ -190,6 +192,7 @@
arguments = fn _ => fn timeout =>
"--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
" --thanks Andrei --input_file",
+ has_incomplete_mode = false,
proof_delims =
[("=========== Refutation ==========",
"======= End of refutation ======="),
@@ -200,8 +203,9 @@
(IncompleteUnprovable, "CANNOT PROVE"),
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
+ (Unprovable, "Termination reason: Satisfiable"),
(VampireTooOld, "not a valid option")],
- default_max_relevant_per_iter = 45 (* FIXME *),
+ default_max_relevant_per_iter = 45 (* FUDGE *),
default_theory_relevant = false,
explicit_forall = false,
use_conjecture_for_hypotheses = true}
@@ -242,6 +246,7 @@
arguments = fn _ => fn timeout =>
" -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
the_system system_prefix,
+ has_incomplete_mode = false,
proof_delims = insert (op =) tstp_proof_delims proof_delims,
known_failures =
known_failures @ known_perl_failures @
@@ -274,10 +279,10 @@
val remote_vampire = remotify_prover vampire "Vampire---9"
val remote_sine_e =
remote_prover "sine_e" "SInE---" []
- [(Unprovable, "says Unknown")] 150 (* FIXME *) false true
+ [(Unprovable, "says Unknown")] 150 (* FUDGE *) false true
val remote_snark =
remote_prover "snark" "SNARK---" [("refutation.", "end_refutation.")] []
- 50 (* FIXME *) false true
+ 50 (* FUDGE *) false true
(* Setup *)
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Aug 23 11:56:12 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Aug 23 15:30:42 2010 +0200
@@ -141,7 +141,6 @@
hol_context -> bool -> styp -> int -> styp
val sel_no_from_name : string -> int
val close_form : term -> term
- val eta_expand : typ list -> term -> int -> term
val distinctness_formula : typ -> term list -> term
val register_frac_type :
string -> (string * string) list -> morphism -> Context.generic
@@ -919,14 +918,6 @@
| aux zs t = close_up zs (Term.add_vars t zs) t
in aux [] end
-fun eta_expand _ t 0 = t
- | eta_expand Ts (Abs (s, T, t')) n =
- Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
- | eta_expand Ts t n =
- fold_rev (curry3 Abs ("x" ^ nat_subscript n))
- (List.take (binder_types (fastype_of1 (Ts, t)), n))
- (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
-
fun distinctness_formula T =
all_distinct_unordered_pairs_of
#> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Aug 23 11:56:12 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Aug 23 15:30:42 2010 +0200
@@ -52,6 +52,7 @@
val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
+ val nat_subscript : int -> string
val flip_polarity : polarity -> polarity
val prop_T : typ
val bool_T : typ
@@ -67,7 +68,7 @@
val monomorphic_term : Type.tyenv -> term -> term
val specialize_type : theory -> string * typ -> term -> term
val varify_type : Proof.context -> typ -> typ
- val nat_subscript : int -> string
+ val eta_expand : typ list -> term -> int -> term
val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
@@ -237,6 +238,18 @@
val parse_bool_option = Sledgehammer_Util.parse_bool_option
val parse_time_option = Sledgehammer_Util.parse_time_option
+val i_subscript = implode o map (prefix "\<^isub>") o explode
+fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
+fun nat_subscript n =
+ let val s = signed_string_of_int n in
+ if print_mode_active Symbol.xsymbolsN then
+ (* cheap trick to ensure proper alphanumeric ordering for one- and
+ two-digit numbers *)
+ (if n <= 9 then be_subscript else i_subscript) s
+ else
+ s
+ end
+
fun flip_polarity Pos = Neg
| flip_polarity Neg = Pos
| flip_polarity Neut = Neut
@@ -258,17 +271,7 @@
Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
|> snd |> the_single |> dest_Const |> snd
-val i_subscript = implode o map (prefix "\<^isub>") o explode
-fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
-fun nat_subscript n =
- let val s = signed_string_of_int n in
- if print_mode_active Symbol.xsymbolsN then
- (* cheap trick to ensure proper alphanumeric ordering for one- and
- two-digit numbers *)
- (if n <= 9 then be_subscript else i_subscript) s
- else
- s
- end
+val eta_expand = Sledgehammer_Util.eta_expand
fun time_limit NONE = I
| time_limit (SOME delay) = TimeLimit.timeLimit delay
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Aug 23 11:56:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Mon Aug 23 15:30:42 2010 +0200
@@ -7,7 +7,6 @@
signature CLAUSIFIER =
sig
- val transform_elim_theorem : thm -> thm
val extensionalize_theorem : thm -> thm
val introduce_combinators_in_cterm : cterm -> thm
val introduce_combinators_in_theorem : thm -> thm
@@ -25,7 +24,7 @@
(* Converts an elim-rule into an equivalent theorem that does not have the
predicate variable. Leaves other theorems unchanged. We simply instantiate
the conclusion variable to False. (Cf. "transform_elim_term" in
- "ATP_Systems".) *)
+ "Sledgehammer_Util".) *)
fun transform_elim_theorem th =
case concl_of th of (*conclusion variable*)
@{const Trueprop} $ (v as Var (_, @{typ bool})) =>
@@ -78,10 +77,6 @@
(**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
-(*Returns the vars of a theorem*)
-fun vars_of_thm th =
- map (cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
-
val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
(* Removes the lambdas from an equation of the form "t = (%x. u)".
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Aug 23 11:56:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Mon Aug 23 15:30:42 2010 +0200
@@ -99,7 +99,7 @@
(@{const_name "op &"}, "and"),
(@{const_name "op |"}, "or"),
(@{const_name "op -->"}, "implies"),
- (@{const_name Set.member}, "in"),
+ (@{const_name Set.member}, "member"),
(@{const_name fequal}, "fequal"),
(@{const_name COMBI}, "COMBI"),
(@{const_name COMBK}, "COMBK"),
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Aug 23 11:56:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Mon Aug 23 15:30:42 2010 +0200
@@ -775,9 +775,6 @@
[])
end;
-val type_has_top_sort =
- exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-
(* Extensionalize "th", because that makes sense and that's what Sledgehammer
does, but also keep an unextensionalized version of "th" for backward
compatibility. *)
@@ -794,6 +791,9 @@
#> map Clausifier.introduce_combinators_in_theorem
#> Meson.finish_cnf
+val type_has_top_sort =
+ exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
+
fun generic_metis_tac mode ctxt ths i st0 =
let
val _ = trace_msg (fn () =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 23 11:56:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 23 15:30:42 2010 +0200
@@ -207,8 +207,8 @@
(* generic TPTP-based provers *)
fun prover_fun atp_name
- {exec, required_execs, arguments, proof_delims, known_failures,
- default_max_relevant_per_iter, default_theory_relevant,
+ {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
+ known_failures, default_max_relevant_per_iter, default_theory_relevant,
explicit_forall, use_conjecture_for_hypotheses}
({debug, verbose, overlord, full_types, explicit_apply,
relevance_threshold, relevance_convergence,
@@ -260,7 +260,7 @@
val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
(* write out problem file and call prover *)
- fun command_line complete probfile =
+ fun command_line complete timeout probfile =
let
val core = File.shell_path command ^ " " ^ arguments complete timeout ^
" " ^ File.shell_path probfile
@@ -288,9 +288,9 @@
| [] =>
if File.exists command then
let
- fun do_run complete =
+ fun do_run complete timeout =
let
- val command = command_line complete probfile
+ val command = command_line complete timeout probfile
val ((output, msecs), res_code) =
bash_output command
|>> (if overlord then
@@ -316,13 +316,20 @@
conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
|> map single
val _ = print_d (fn () => "Running " ^ quote atp_name ^ "...")
+ val timer = Timer.startRealTimer ()
val result =
- do_run false
- |> (fn (_, msecs0, _, SOME _) =>
- do_run true
- |> (fn (output, msecs, proof, outcome) =>
- (output, msecs0 + msecs, proof, outcome))
- | result => result)
+ do_run false (if has_incomplete_mode then
+ Time.fromMilliseconds
+ (2 * Time.toMilliseconds timeout div 3)
+ else
+ timeout)
+ |> has_incomplete_mode
+ ? (fn (_, msecs0, _, SOME _) =>
+ do_run true
+ (Time.- (timeout, Timer.checkRealTimer timer))
+ |> (fn (output, msecs, proof, outcome) =>
+ (output, msecs0 + msecs, proof, outcome))
+ | result => result)
in ((pool, conjecture_shape, axiom_names), result) end
else
error ("Bad executable: " ^ Path.implode command ^ ".")
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 23 11:56:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Mon Aug 23 15:30:42 2010 +0200
@@ -23,6 +23,8 @@
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
struct
+open Sledgehammer_Util
+
val trace = Unsynchronized.ref false
fun trace_msg msg = if !trace then tracing (msg ()) else ()
@@ -43,7 +45,7 @@
val name = Facts.string_of_ref xref
|> forall (member Thm.eq_thm chained_ths) ths
? prefix chained_prefix
- in (name, ths |> map Clausifier.transform_elim_theorem) end
+ in (name, ths) end
(***************************************************************)
@@ -84,11 +86,10 @@
Symtab.map_default (c, [ctyps])
(fn [] => [] | ctypss => insert (op =) ctyps ctypss)
-val fresh_prefix = "Sledgehammer.Fresh."
+val fresh_prefix = "Sledgehammer.FRESH."
val flip = Option.map not
(* These are typically simplified away by "Meson.presimplify". *)
-val boring_consts =
- [@{const_name If}, @{const_name Let} (* TODO: , @{const_name Set.member}, @{const_name Collect} *)]
+val boring_consts = [@{const_name If}, @{const_name Let}]
fun get_consts_typs thy pos ts =
let
@@ -100,10 +101,7 @@
Const x => add_const_type_to_table (const_with_typ thy x)
| Free (s, _) => add_const_type_to_table (s, [])
| t1 $ t2 => do_term t1 #> do_term t2
- | Abs (_, _, t) =>
- (* Abstractions lead to combinators, so we add a penalty for them. *)
- add_const_type_to_table (gensym fresh_prefix, [])
- #> do_term t
+ | Abs (_, _, t') => do_term t'
| _ => I
fun do_quantifier will_surely_be_skolemized body_t =
do_formula pos body_t
@@ -424,7 +422,7 @@
val exists_sledgehammer_const =
exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
-fun is_strange_thm th =
+fun is_strange_theorem th =
case head_of (concl_of th) of
Const (a, _) => (a <> @{const_name Trueprop} andalso
a <> @{const_name "=="})
@@ -490,29 +488,37 @@
are omitted. *)
fun is_dangerous_term full_types t =
not full_types andalso
- (has_bound_or_var_of_type dangerous_types t orelse is_exhaustive_finite t)
+ ((has_bound_or_var_of_type dangerous_types t andalso
+ has_bound_or_var_of_type dangerous_types (transform_elim_term t))
+ orelse is_exhaustive_finite t)
fun is_theorem_bad_for_atps full_types thm =
let val t = prop_of thm in
is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse
- is_strange_thm thm
+ is_strange_theorem thm
end
fun all_name_thms_pairs ctxt full_types add_thms chained_ths =
let
val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
- val local_facts = ProofContext.facts_of ctxt;
+ val local_facts = ProofContext.facts_of ctxt
+ val named_locals = local_facts |> Facts.dest_static []
+ val unnamed_locals =
+ local_facts |> Facts.props
+ |> filter_out (fn th => exists (fn (_, ths) => member Thm.eq_thm ths th)
+ named_locals)
+ |> map (pair "" o single)
val full_space =
Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
-
- fun valid_facts facts =
- (facts, []) |-> Facts.fold_static (fn (name, ths0) =>
- if (Facts.is_concealed facts name orelse
+ fun valid_facts facts pairs =
+ (pairs, []) |-> fold (fn (name, ths0) =>
+ if name <> "" andalso
+ forall (not o member Thm.eq_thm add_thms) ths0 andalso
+ (Facts.is_concealed facts name orelse
(respect_no_atp andalso is_package_def name) orelse
member (op =) multi_base_blacklist (Long_Name.base_name name) orelse
- String.isSuffix "_def_raw" (* FIXME: crude hack *) name) andalso
- forall (not o member Thm.eq_thm add_thms) ths0 then
+ String.isSuffix "_def_raw" (* FIXME: crude hack *) name) then
I
else
let
@@ -523,17 +529,25 @@
val name1 = Facts.extern facts name;
val name2 = Name_Space.extern full_space name;
val ths =
- ths0 |> map Clausifier.transform_elim_theorem
- |> filter ((not o is_theorem_bad_for_atps full_types) orf
- member Thm.eq_thm add_thms)
+ ths0 |> filter ((not o is_theorem_bad_for_atps full_types) orf
+ member Thm.eq_thm add_thms)
+ val name' =
+ case find_first check_thms [name1, name2, name] of
+ SOME name' => name'
+ | NONE =>
+ ths |> map (fn th =>
+ "`" ^ Print_Mode.setmp [Print_Mode.input]
+ (Syntax.string_of_term ctxt)
+ (prop_of th) ^ "`")
+ |> space_implode " "
in
- case find_first check_thms [name1, name2, name] of
- NONE => I
- | SOME name' =>
- cons (name' |> forall (member Thm.eq_thm chained_ths) ths
- ? prefix chained_prefix, ths)
+ cons (name' |> forall (member Thm.eq_thm chained_ths) ths0
+ ? prefix chained_prefix, ths)
end)
- in valid_facts global_facts @ valid_facts local_facts end;
+ in
+ valid_facts local_facts (unnamed_locals @ named_locals) @
+ valid_facts global_facts (Facts.dest_static [] global_facts)
+ end
fun multi_name a th (n, pairs) =
(n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs);
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Aug 23 11:56:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Mon Aug 23 15:30:42 2010 +0200
@@ -119,8 +119,12 @@
@{const Not} $ t1 => @{const Not} $ aux Ts t1
| (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name All}, _)) $ t1 =>
+ aux Ts (t0 $ eta_expand Ts t1 1)
| (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
t0 $ Abs (s, T, aux (T :: Ts) t')
+ | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
+ aux Ts (t0 $ eta_expand Ts t1 1)
| (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
| (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
| (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
@@ -175,8 +179,10 @@
let
val thy = ProofContext.theory_of ctxt
val t = t |> Envir.beta_eta_contract
+ |> transform_elim_term
|> atomize_term
- val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
+ val need_trueprop = (fastype_of t = HOLogic.boolT)
+ val t = t |> need_trueprop ? HOLogic.mk_Trueprop
|> extensionalize_term
|> presimp ? presimplify_term thy
|> perhaps (try (HOLogic.dest_Trueprop))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Aug 23 11:56:12 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Mon Aug 23 15:30:42 2010 +0200
@@ -16,6 +16,8 @@
val unyxml : string -> string
val maybe_quote : string -> string
val monomorphic_term : Type.tyenv -> term -> term
+ val eta_expand : typ list -> term -> int -> term
+ val transform_elim_term : term -> term
val specialize_type : theory -> (string * typ) -> term -> term
val subgoal_count : Proof.state -> int
val strip_subgoal : thm -> int -> (string * typ) list * term list * term
@@ -107,6 +109,25 @@
| NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \
\variable", [t]))) t
+fun eta_expand _ t 0 = t
+ | eta_expand Ts (Abs (s, T, t')) n =
+ Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
+ | eta_expand Ts t n =
+ fold_rev (fn T => fn t' => Abs ("x" ^ nat_subscript n, T, t'))
+ (List.take (binder_types (fastype_of1 (Ts, t)), n))
+ (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
+
+(* Converts an elim-rule into an equivalent theorem that does not have the
+ predicate variable. Leaves other theorems unchanged. We simply instantiate
+ the conclusion variable to False. (Cf. "transform_elim_theorem" in
+ "Clausifier".) *)
+fun transform_elim_term t =
+ case Logic.strip_imp_concl t of
+ @{const Trueprop} $ Var (z, @{typ bool}) =>
+ subst_Vars [(z, @{const False})] t
+ | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
+ | _ => t
+
fun specialize_type thy (s, T) t =
let
fun subst_for (Const (s', T')) =