merged
authorwenzelm
Mon, 23 Aug 2010 17:46:13 +0200
changeset 38655 5001ed24e129
parent 38654 0b1a63d06805 (diff)
parent 38641 7ab0ae836f74 (current diff)
child 38656 d5d342611edb
merged
--- a/NEWS	Mon Aug 23 17:45:06 2010 +0200
+++ b/NEWS	Mon Aug 23 17:46:13 2010 +0200
@@ -35,6 +35,8 @@
 
 *** HOL ***
 
+* Dropped type classes mult_mono and mult_mono1.  INCOMPATIBILITY.
+
 * Theory SetsAndFunctions has been split into Function_Algebras and Set_Algebras;
 canonical names for instance definitions for functions; various improvements.
 INCOMPATIBILITY.
--- a/src/HOL/Library/Convex.thy	Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Library/Convex.thy	Mon Aug 23 17:46:13 2010 +0200
@@ -244,7 +244,7 @@
   shows "convex_on s (\<lambda>x. c * f x)"
 proof-
   have *:"\<And>u c fx v fy ::real. u * (c * fx) + v * (c * fy) = c * (u * fx + v * fy)" by (simp add: field_simps)
-  show ?thesis using assms(2) and mult_mono1[OF _ assms(1)] unfolding convex_on_def and * by auto
+  show ?thesis using assms(2) and mult_left_mono [OF _ assms(1)] unfolding convex_on_def and * by auto
 qed
 
 lemma convex_lower:
@@ -253,7 +253,7 @@
 proof-
   let ?m = "max (f x) (f y)"
   have "u * f x + v * f y \<le> u * max (f x) (f y) + v * max (f x) (f y)"
-    using assms(4,5) by(auto simp add: mult_mono1 add_mono)
+    using assms(4,5) by (auto simp add: mult_left_mono add_mono)
   also have "\<dots> = max (f x) (f y)" using assms(6) unfolding distrib[THEN sym] by auto
   finally show ?thesis
     using assms unfolding convex_on_def by fastsimp
@@ -481,8 +481,8 @@
   hence xpos: "?x \<in> C" using asm unfolding convex_alt by fastsimp
   have geq: "\<mu> * (f x - f ?x) + (1 - \<mu>) * (f y - f ?x)
             \<ge> \<mu> * f' ?x * (x - ?x) + (1 - \<mu>) * f' ?x * (y - ?x)"
-    using add_mono[OF mult_mono1[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
-      mult_mono1[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
+    using add_mono[OF mult_left_mono[OF leq[OF xpos asm(2)] `\<mu> \<ge> 0`]
+      mult_left_mono[OF leq[OF xpos asm(3)] `1 - \<mu> \<ge> 0`]] by auto
   hence "\<mu> * f x + (1 - \<mu>) * f y - f ?x \<ge> 0"
     by (auto simp add:field_simps)
   thus "f (\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y) \<le> \<mu> * f x + (1 - \<mu>) * f y"
--- a/src/HOL/Library/Function_Algebras.thy	Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Library/Function_Algebras.thy	Mon Aug 23 17:46:13 2010 +0200
@@ -105,12 +105,6 @@
 instance "fun" :: (type, mult_zero) mult_zero proof
 qed (simp_all add: zero_fun_def times_fun_def)
 
-instance "fun" :: (type, mult_mono) mult_mono proof
-qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
-
-instance "fun" :: (type, mult_mono1) mult_mono1 proof
-qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_mono1)
-
 instance "fun" :: (type, zero_neq_one) zero_neq_one proof
 qed (simp add: zero_fun_def one_fun_def expand_fun_eq)
 
@@ -186,9 +180,11 @@
 
 instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
 
-instance "fun" :: (type, ordered_semiring) ordered_semiring ..
+instance "fun" :: (type, ordered_semiring) ordered_semiring proof
+qed (auto simp add: zero_fun_def times_fun_def le_fun_def intro: mult_left_mono mult_right_mono)
 
-instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring ..
+instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring proof
+qed (fact mult_left_mono)
 
 instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
 
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Aug 23 17:46:13 2010 +0200
@@ -2507,7 +2507,7 @@
     fix i assume i:"i<DIM('a)" thus "0 < x $$ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0`
       unfolding dist_norm  by(auto simp add: inner_simps euclidean_component_def dot_basis elim!:allE[where x=i])
   next have **:"dist x (x + (e / 2) *\<^sub>R basis 0) < e" using  `e>0`
-      unfolding dist_norm by(auto intro!: mult_strict_left_mono_comm)
+      unfolding dist_norm by(auto intro!: mult_strict_left_mono)
     have "\<And>i. i<DIM('a) \<Longrightarrow> (x + (e / 2) *\<^sub>R basis 0) $$ i = x$$i + (if i = 0 then e/2 else 0)"
       unfolding euclidean_component_def by(auto simp add:inner_simps dot_basis)
     hence *:"setsum (op $$ (x + (e / 2) *\<^sub>R basis 0)) {..<DIM('a)} = setsum (\<lambda>i. x$$i + (if 0 = i then e/2 else 0)) {..<DIM('a)}"
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Aug 23 17:46:13 2010 +0200
@@ -220,7 +220,7 @@
   fixes x :: "'a::real_normed_vector"
   shows "b >= norm(x) ==> \<bar>c\<bar> * b >= norm(scaleR c x)"
   unfolding norm_scaleR
-  apply (erule mult_mono1)
+  apply (erule mult_left_mono)
   apply simp
   done
 
--- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Mon Aug 23 17:46:13 2010 +0200
@@ -107,7 +107,7 @@
   apply (subst mult_assoc)
   apply (rule order_trans)
   apply (rule onorm(1)[OF lf])
-  apply (rule mult_mono1)
+  apply (rule mult_left_mono)
   apply (rule onorm(1)[OF lg])
   apply (rule onorm_pos_le[OF lf])
   done
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Aug 23 17:46:13 2010 +0200
@@ -5678,7 +5678,7 @@
     next
       case (Suc m)
       hence "c * dist (z m) (z (Suc m)) \<le> c ^ Suc m * d"
-        using `0 \<le> c` using mult_mono1_class.mult_mono1[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by auto
+        using `0 \<le> c` using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by auto
       thus ?case using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s]
         unfolding fzn and mult_le_cancel_left by auto
     qed
--- a/src/HOL/NSA/StarDef.thy	Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/NSA/StarDef.thy	Mon Aug 23 17:46:13 2010 +0200
@@ -925,12 +925,12 @@
 done
 
 instance star :: (ordered_comm_semiring) ordered_comm_semiring
-by (intro_classes, transfer, rule mult_mono1_class.mult_mono1)
+by (intro_classes, transfer, rule mult_left_mono)
 
 instance star :: (ordered_cancel_comm_semiring) ordered_cancel_comm_semiring ..
 
 instance star :: (linordered_comm_semiring_strict) linordered_comm_semiring_strict
-by (intro_classes, transfer, rule mult_strict_left_mono_comm)
+by (intro_classes, transfer, rule mult_strict_left_mono)
 
 instance star :: (ordered_ring) ordered_ring ..
 instance star :: (ordered_ring_abs) ordered_ring_abs
--- a/src/HOL/Orderings.thy	Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Orderings.thy	Mon Aug 23 17:46:13 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 17:45:06 2010 +0200
+++ b/src/HOL/Predicate.thy	Mon Aug 23 17:46:13 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/Probability/Lebesgue.thy	Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Probability/Lebesgue.thy	Mon Aug 23 17:46:13 2010 +0200
@@ -700,7 +700,7 @@
     using `a \<in> nnfis f` unfolding nnfis_def by auto
   with `0 \<le> z`show ?thesis unfolding nnfis_def mono_convergent_def incseq_def
     by (auto intro!: exI[of _ "\<lambda>n w. z * u n w"] exI[of _ "\<lambda>n. z * x n"]
-      LIMSEQ_mult LIMSEQ_const psfis_mult mult_mono1)
+      LIMSEQ_mult LIMSEQ_const psfis_mult mult_left_mono)
 qed
 
 lemma nnfis_add:
--- a/src/HOL/Rings.thy	Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Rings.thy	Mon Aug 23 17:46:13 2010 +0200
@@ -628,10 +628,6 @@
 
 end
 
-class mult_mono = times + zero + ord +
-  assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
-  assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
-
 text {*
   The theory of partially ordered rings is taken from the books:
   \begin{itemize}
@@ -645,31 +641,29 @@
   \end{itemize}
 *}
 
-class ordered_semiring = mult_mono + semiring_0 + ordered_ab_semigroup_add 
+class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
+  assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
+  assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"
 begin
 
 lemma mult_mono:
-  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c
-     \<Longrightarrow> a * c \<le> b * d"
+  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
 apply (erule mult_right_mono [THEN order_trans], assumption)
 apply (erule mult_left_mono, assumption)
 done
 
 lemma mult_mono':
-  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c
-     \<Longrightarrow> a * c \<le> b * d"
+  "a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * d"
 apply (rule mult_mono)
 apply (fast intro: order_trans)+
 done
 
 end
 
-class ordered_cancel_semiring = mult_mono + ordered_ab_semigroup_add
-  + semiring + cancel_comm_monoid_add
+class ordered_cancel_semiring = ordered_semiring + cancel_comm_monoid_add
 begin
 
 subclass semiring_0_cancel ..
-subclass ordered_semiring ..
 
 lemma mult_nonneg_nonneg: "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a * b"
 using mult_left_mono [of 0 b a] by simp
@@ -689,7 +683,7 @@
 
 end
 
-class linordered_semiring = semiring + comm_monoid_add + linordered_cancel_ab_semigroup_add + mult_mono
+class linordered_semiring = ordered_semiring + linordered_cancel_ab_semigroup_add
 begin
 
 subclass ordered_cancel_semiring ..
@@ -854,41 +848,38 @@
 
 end
 
-class mult_mono1 = times + zero + ord +
-  assumes mult_mono1: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
-
-class ordered_comm_semiring = comm_semiring_0
-  + ordered_ab_semigroup_add + mult_mono1
+class ordered_comm_semiring = comm_semiring_0 + ordered_ab_semigroup_add + 
+  assumes comm_mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
 begin
 
 subclass ordered_semiring
 proof
   fix a b c :: 'a
   assume "a \<le> b" "0 \<le> c"
-  thus "c * a \<le> c * b" by (rule mult_mono1)
+  thus "c * a \<le> c * b" by (rule comm_mult_left_mono)
   thus "a * c \<le> b * c" by (simp only: mult_commute)
 qed
 
 end
 
-class ordered_cancel_comm_semiring = comm_semiring_0_cancel
-  + ordered_ab_semigroup_add + mult_mono1
+class ordered_cancel_comm_semiring = ordered_comm_semiring + cancel_comm_monoid_add
 begin
 
+subclass comm_semiring_0_cancel ..
 subclass ordered_comm_semiring ..
 subclass ordered_cancel_semiring ..
 
 end
 
 class linordered_comm_semiring_strict = comm_semiring_0 + linordered_cancel_ab_semigroup_add +
-  assumes mult_strict_left_mono_comm: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
+  assumes comm_mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
 begin
 
 subclass linordered_semiring_strict
 proof
   fix a b c :: 'a
   assume "a < b" "0 < c"
-  thus "c * a < c * b" by (rule mult_strict_left_mono_comm)
+  thus "c * a < c * b" by (rule comm_mult_strict_left_mono)
   thus "a * c < b * c" by (simp only: mult_commute)
 qed
 
--- a/src/HOL/Set.thy	Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Set.thy	Mon Aug 23 17:46:13 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 17:45:06 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 23 17:46:13 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 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 23 17:46:13 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 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Aug 23 17:46:13 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 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 23 17:46:13 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 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Mon Aug 23 17:46:13 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 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Aug 23 17:46:13 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 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Aug 23 17:46:13 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 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 17:46:13 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 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 23 17:46:13 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 17:45:06 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Aug 23 17:46:13 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')) =
--- a/src/HOL/Transcendental.thy	Mon Aug 23 17:45:06 2010 +0200
+++ b/src/HOL/Transcendental.thy	Mon Aug 23 17:46:13 2010 +0200
@@ -2790,7 +2790,7 @@
 
 lemma less_one_imp_sqr_less_one: fixes x :: real assumes "\<bar>x\<bar> < 1" shows "x^2 < 1"
 proof -
-  from mult_mono1[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
+  from mult_left_mono[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
   have "\<bar> x^2 \<bar> < 1" using `\<bar> x \<bar> < 1` unfolding numeral_2_eq_2 power_Suc2 by auto
   thus ?thesis using zero_le_power2 by auto
 qed