# HG changeset patch
# User wenzelm
# Date 1358537482 -3600
# Node ID 21da2a03b9d2cfd9e1ce902008643645b5c6eae4
# Parent  4a2c82644889b94b9c9b53133e45837c6571ba00# Parent  20edcc6a8def03819d4fc67b113a579f6a08e9da
merged

diff -r 20edcc6a8def -r 21da2a03b9d2 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jan 18 20:24:51 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Fri Jan 18 20:31:22 2013 +0100
@@ -3284,7 +3284,7 @@
   have "convex hull s \<noteq> {}" using hull_subset[of s convex] and assms(2) by auto
   then obtain u v where obt:"u\<in>convex hull s" "v\<in>convex hull s"
     "\<forall>x\<in>convex hull s. \<forall>y\<in>convex hull s. norm (x - y) \<le> norm (u - v)"
-    using compact_sup_maxdistance[OF finite_imp_compact_convex_hull[OF assms(1)]] by auto
+    using compact_sup_maxdistance[OF finite_imp_compact_convex_hull[OF assms(1)]] by (auto simp: dist_norm)
   thus ?thesis proof(cases "u\<notin>s \<or> v\<notin>s", erule_tac disjE)
     assume "u\<notin>s" then obtain y where "y\<in>convex hull s" "norm (u - v) < norm (y - v)"
       using simplex_furthest_lt[OF assms(1), THEN bspec[where x=u]] and obt(1) by auto
diff -r 20edcc6a8def -r 21da2a03b9d2 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jan 18 20:24:51 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jan 18 20:31:22 2013 +0100
@@ -9,7 +9,6 @@
 theory Topology_Euclidean_Space
 imports
   Complex_Main
-  "~~/src/HOL/Library/Diagonal_Subsequence"
   "~~/src/HOL/Library/Countable_Set"
   "~~/src/HOL/Library/Glbs"
   "~~/src/HOL/Library/FuncSet"
@@ -17,9 +16,18 @@
   Norm_Arith
 begin
 
+lemma dist_0_norm:
+  fixes x :: "'a::real_normed_vector"
+  shows "dist 0 x = norm x"
+unfolding dist_norm by simp
+
 lemma dist_double: "dist x y < d / 2 \<Longrightarrow> dist x z < d / 2 \<Longrightarrow> dist y z < d"
   using dist_triangle[of y z x] by (simp add: dist_commute)
 
+(* LEGACY *)
+lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s o r) ----> l"
+  by (rule LIMSEQ_subseq_LIMSEQ)
+
 (* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
 lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
   apply (frule isGlb_isLb)
@@ -2223,6 +2231,9 @@
   apply (subgoal_tac "\<And>x (y::real). 0 < 1 + abs y \<and> (x <= y \<longrightarrow> x <= 1 + abs y)")
   by metis arith
 
+lemma Bseq_eq_bounded: "Bseq f \<longleftrightarrow> bounded (range f)"
+  unfolding Bseq_def bounded_pos by auto
+
 lemma bounded_Int[intro]: "bounded S \<or> bounded T \<Longrightarrow> bounded (S \<inter> T)"
   by (metis Int_lower1 Int_lower2 bounded_subset)
 
@@ -3219,88 +3230,24 @@
     using bounded_closed_imp_seq_compact[of s] unfolding compact_eq_seq_compact_metric by auto
 qed
 
-lemma lim_subseq:
-  "subseq r \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
-unfolding tendsto_def eventually_sequentially o_def
-by (metis seq_suble le_trans)
-
-lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
-  unfolding Ex1_def
-  apply (rule_tac x="nat_rec e f" in exI)
-  apply (rule conjI)+
-apply (rule def_nat_rec_0, simp)
-apply (rule allI, rule def_nat_rec_Suc, simp)
-apply (rule allI, rule impI, rule ext)
-apply (erule conjE)
-apply (induct_tac x)
-apply simp
-apply (erule_tac x="n" in allE)
-apply (simp)
-done
-
-lemma convergent_bounded_increasing: fixes s ::"nat\<Rightarrow>real"
-  assumes "incseq s" and "\<forall>n. abs(s n) \<le> b"
-  shows "\<exists> l. \<forall>e::real>0. \<exists> N. \<forall>n \<ge> N.  abs(s n - l) < e"
-proof-
-  have "isUb UNIV (range s) b" using assms(2) and abs_le_D1 unfolding isUb_def and setle_def by auto
-  then obtain t where t:"isLub UNIV (range s) t" using reals_complete[of "range s" ] by auto
-  { fix e::real assume "e>0" and as:"\<forall>N. \<exists>n\<ge>N. \<not> \<bar>s n - t\<bar> < e"
-    { fix n::nat
-      obtain N where "N\<ge>n" and n:"\<bar>s N - t\<bar> \<ge> e" using as[THEN spec[where x=n]] by auto
-      have "t \<ge> s N" using isLub_isUb[OF t, unfolded isUb_def setle_def] by auto
-      with n have "s N \<le> t - e" using `e>0` by auto
-      hence "s n \<le> t - e" using assms(1)[unfolded incseq_def, THEN spec[where x=n], THEN spec[where x=N]] using `n\<le>N` by auto  }
-    hence "isUb UNIV (range s) (t - e)" unfolding isUb_def and setle_def by auto
-    hence False using isLub_le_isUb[OF t, of "t - e"] and `e>0` by auto  }
-  thus ?thesis by blast
-qed
-
-lemma convergent_bounded_monotone: fixes s::"nat \<Rightarrow> real"
-  assumes "\<forall>n. abs(s n) \<le> b" and "monoseq s"
-  shows "\<exists>l. \<forall>e::real>0. \<exists>N. \<forall>n\<ge>N. abs(s n - l) < e"
-  using convergent_bounded_increasing[of s b] assms using convergent_bounded_increasing[of "\<lambda>n. - s n" b]
-  unfolding monoseq_def incseq_def
-  apply auto unfolding minus_add_distrib[THEN sym, unfolded diff_minus[THEN sym]]
-  unfolding abs_minus_cancel by(rule_tac x="-l" in exI)auto
-
-(* TODO: merge this lemma with the ones above *)
-lemma bounded_increasing_convergent: fixes s::"nat \<Rightarrow> real"
-  assumes "bounded {s n| n::nat. True}"  "\<forall>n. (s n) \<le>(s(Suc n))"
-  shows "\<exists>l. (s ---> l) sequentially"
-proof-
-  obtain a where a:"\<forall>n. \<bar> (s n)\<bar> \<le>  a" using assms(1)[unfolded bounded_iff] by auto
-  { fix m::nat
-    have "\<And> n. n\<ge>m \<longrightarrow>  (s m) \<le> (s n)"
-      apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE)
-      apply(case_tac "m \<le> na") unfolding not_less_eq_eq by(auto simp add: not_less_eq_eq)  }
-  hence "\<forall>m n. m \<le> n \<longrightarrow> (s m) \<le> (s n)" by auto
-  then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar> (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a]
-    unfolding monoseq_def by auto
-  thus ?thesis unfolding LIMSEQ_def apply(rule_tac x="l" in exI)
-    unfolding dist_norm  by auto
-qed
-
-lemma compact_real_lemma:
-  assumes "\<forall>n::nat. abs(s n) \<le> b"
-  shows "\<exists>(l::real) r. subseq r \<and> ((s \<circ> r) ---> l) sequentially"
-proof-
-  obtain r where r:"subseq r" "monoseq (\<lambda>n. s (r n))"
-    using seq_monosub[of s] by auto
-  thus ?thesis using convergent_bounded_monotone[of "\<lambda>n. s (r n)" b] and assms
-    unfolding tendsto_iff dist_norm eventually_sequentially by auto
-qed
+(* TODO: is this lemma necessary? *)
+lemma bounded_increasing_convergent:
+  fixes s :: "nat \<Rightarrow> real"
+  shows "bounded {s n| n. True} \<Longrightarrow> \<forall>n. s n \<le> s (Suc n) \<Longrightarrow> \<exists>l. s ----> l"
+  using Bseq_mono_convergent[of s] incseq_Suc_iff[of s]
+  by (auto simp: image_def Bseq_eq_bounded convergent_def incseq_def)
 
 instance real :: heine_borel
 proof
   fix s :: "real set" and f :: "nat \<Rightarrow> real"
   assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
-  then obtain b where b: "\<forall>n. abs (f n) \<le> b"
-    unfolding bounded_iff by auto
-  obtain l :: real and r :: "nat \<Rightarrow> nat" where
-    r: "subseq r" and l: "((f \<circ> r) ---> l) sequentially"
-    using compact_real_lemma [OF b] by auto
-  thus "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
-    by auto
+  obtain r where r: "subseq r" "monoseq (f \<circ> r)"
+    unfolding comp_def by (metis seq_monosub)
+  moreover
+  then have "Bseq (f \<circ> r)"
+    unfolding Bseq_eq_bounded using s f by (auto intro: bounded_subset)
+  ultimately show "\<exists>l r. subseq r \<and> (f \<circ> r) ----> l"
+    using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
 qed
 
 lemma compact_lemma:
@@ -3406,7 +3353,7 @@
     using bounded_imp_convergent_subsequence [OF s2 f2]
     unfolding o_def by fast
   have l1': "((\<lambda>n. fst (f (r1 (r2 n)))) ---> l1) sequentially"
-    using lim_subseq [OF r2 l1] unfolding o_def .
+    using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def .
   have l: "((f \<circ> (r1 \<circ> r2)) ---> (l1, l2)) sequentially"
     using tendsto_Pair [OF l1' l2] unfolding o_def by simp
   have r: "subseq (r1 \<circ> r2)"
@@ -3417,10 +3364,120 @@
 
 subsubsection{* Completeness *}
 
-definition
-  complete :: "'a::metric_space set \<Rightarrow> bool" where
-  "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f
-                      --> (\<exists>l \<in> s. (f ---> l) sequentially))"
+definition complete :: "'a::metric_space set \<Rightarrow> bool" where
+  "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>s. f ----> l))"
+
+lemma compact_imp_complete: assumes "compact s" shows "complete s"
+proof-
+  { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
+    from as(1) obtain l r where lr: "l\<in>s" "subseq r" "(f \<circ> r) ----> l"
+      using assms unfolding compact_def by blast
+
+    note lr' = seq_suble [OF lr(2)]
+
+    { fix e::real assume "e>0"
+      from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2" unfolding cauchy_def using `e>0` apply (erule_tac x="e/2" in allE) by auto
+      from lr(3)[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2" using `e>0` by auto
+      { fix n::nat assume n:"n \<ge> max N M"
+        have "dist ((f \<circ> r) n) l < e/2" using n M by auto
+        moreover have "r n \<ge> N" using lr'[of n] n by auto
+        hence "dist (f n) ((f \<circ> r) n) < e / 2" using N using n by auto
+        ultimately have "dist (f n) l < e" using dist_triangle_half_r[of "f (r n)" "f n" e l] by (auto simp add: dist_commute)  }
+      hence "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast  }
+    hence "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>s` unfolding LIMSEQ_def by auto  }
+  thus ?thesis unfolding complete_def by auto
+qed
+
+lemma nat_approx_posE:
+  fixes e::real
+  assumes "0 < e"
+  obtains n::nat where "1 / (Suc n) < e"
+proof atomize_elim
+  have " 1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
+    by (rule divide_strict_left_mono) (auto intro!: mult_pos_pos simp: `0 < e`)
+  also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
+    by (rule divide_left_mono) (auto intro!: divide_pos_pos simp: `0 < e`)
+  also have "\<dots> = e" by simp
+  finally show  "\<exists>n. 1 / real (Suc n) < e" ..
+qed
+
+lemma compact_eq_totally_bounded:
+  "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
+    (is "_ \<longleftrightarrow> ?rhs")
+proof
+  assume assms: "?rhs"
+  then obtain k where k: "\<And>e. 0 < e \<Longrightarrow> finite (k e)" "\<And>e. 0 < e \<Longrightarrow> s \<subseteq> (\<Union>x\<in>k e. ball x e)"
+    by (auto simp: choice_iff')
+
+  show "compact s"
+  proof cases
+    assume "s = {}" thus "compact s" by (simp add: compact_def)
+  next
+    assume "s \<noteq> {}"
+    show ?thesis
+      unfolding compact_def
+    proof safe
+      fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> s"
+      
+      def e \<equiv> "\<lambda>n. 1 / (2 * Suc n)"
+      then have [simp]: "\<And>n. 0 < e n" by auto
+      def B \<equiv> "\<lambda>n U. SOME b. infinite {n. f n \<in> b} \<and> (\<exists>x. b \<subseteq> ball x (e n) \<inter> U)"
+      { fix n U assume "infinite {n. f n \<in> U}"
+        then have "\<exists>b\<in>k (e n). infinite {i\<in>{n. f n \<in> U}. f i \<in> ball b (e n)}"
+          using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq)
+        then guess a ..
+        then have "\<exists>b. infinite {i. f i \<in> b} \<and> (\<exists>x. b \<subseteq> ball x (e n) \<inter> U)"
+          by (intro exI[of _ "ball a (e n) \<inter> U"] exI[of _ a]) (auto simp: ac_simps)
+        from someI_ex[OF this]
+        have "infinite {i. f i \<in> B n U}" "\<exists>x. B n U \<subseteq> ball x (e n) \<inter> U"
+          unfolding B_def by auto }
+      note B = this
+
+      def F \<equiv> "nat_rec (B 0 UNIV) B"
+      { fix n have "infinite {i. f i \<in> F n}"
+          by (induct n) (auto simp: F_def B) }
+      then have F: "\<And>n. \<exists>x. F (Suc n) \<subseteq> ball x (e n) \<inter> F n"
+        using B by (simp add: F_def)
+      then have F_dec: "\<And>m n. m \<le> n \<Longrightarrow> F n \<subseteq> F m"
+        using decseq_SucI[of F] by (auto simp: decseq_def)
+
+      obtain sel where sel: "\<And>k i. i < sel k i" "\<And>k i. f (sel k i) \<in> F k"
+      proof (atomize_elim, unfold all_conj_distrib[symmetric], intro choice allI)
+        fix k i
+        have "infinite ({n. f n \<in> F k} - {.. i})"
+          using `infinite {n. f n \<in> F k}` by auto
+        from infinite_imp_nonempty[OF this]
+        show "\<exists>x>i. f x \<in> F k"
+          by (simp add: set_eq_iff not_le conj_commute)
+      qed
+
+      def t \<equiv> "nat_rec (sel 0 0) (\<lambda>n i. sel (Suc n) i)"
+      have "subseq t"
+        unfolding subseq_Suc_iff by (simp add: t_def sel)
+      moreover have "\<forall>i. (f \<circ> t) i \<in> s"
+        using f by auto
+      moreover
+      { fix n have "(f \<circ> t) n \<in> F n"
+          by (cases n) (simp_all add: t_def sel) }
+      note t = this
+
+      have "Cauchy (f \<circ> t)"
+      proof (safe intro!: metric_CauchyI exI elim!: nat_approx_posE)
+        fix r :: real and N n m assume "1 / Suc N < r" "Suc N \<le> n" "Suc N \<le> m"
+        then have "(f \<circ> t) n \<in> F (Suc N)" "(f \<circ> t) m \<in> F (Suc N)" "2 * e N < r"
+          using F_dec t by (auto simp: e_def field_simps real_of_nat_Suc)
+        with F[of N] obtain x where "dist x ((f \<circ> t) n) < e N" "dist x ((f \<circ> t) m) < e N"
+          by (auto simp: subset_eq)
+        with dist_triangle[of "(f \<circ> t) m" "(f \<circ> t) n" x] `2 * e N < r`
+        show "dist ((f \<circ> t) m) ((f \<circ> t) n) < r"
+          by (simp add: dist_commute)
+      qed
+
+      ultimately show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l"
+        using assms unfolding complete_def by blast
+    qed
+  qed
+qed (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded)
 
 lemma cauchy: "Cauchy s \<longleftrightarrow> (\<forall>e>0.\<exists> N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
 proof-
@@ -3462,35 +3519,15 @@
     apply(erule_tac x=y in allE) apply(erule_tac x=y in ballE) by auto
 qed
 
-lemma seq_compact_imp_complete: assumes "seq_compact s" shows "complete s"
-proof-
-  { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
-    from as(1) obtain l r where lr: "l\<in>s" "subseq r" "((f \<circ> r) ---> l) sequentially" using assms unfolding seq_compact_def by blast
-
-    note lr' = seq_suble [OF lr(2)]
-
-    { fix e::real assume "e>0"
-      from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (f m) (f n) < e/2" unfolding cauchy_def using `e>0` apply (erule_tac x="e/2" in allE) by auto
-      from lr(3)[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2" using `e>0` by auto
-      { fix n::nat assume n:"n \<ge> max N M"
-        have "dist ((f \<circ> r) n) l < e/2" using n M by auto
-        moreover have "r n \<ge> N" using lr'[of n] n by auto
-        hence "dist (f n) ((f \<circ> r) n) < e / 2" using N using n by auto
-        ultimately have "dist (f n) l < e" using dist_triangle_half_r[of "f (r n)" "f n" e l] by (auto simp add: dist_commute)  }
-      hence "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast  }
-    hence "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>s` unfolding LIMSEQ_def by auto  }
-  thus ?thesis unfolding complete_def by auto
-qed
-
 instance heine_borel < complete_space
 proof
   fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
   hence "bounded (range f)"
     by (rule cauchy_imp_bounded)
-  hence "seq_compact (closure (range f))"
-    using bounded_closed_imp_seq_compact [of "closure (range f)"] by auto
+  hence "compact (closure (range f))"
+    unfolding compact_eq_bounded_closed by auto
   hence "complete (closure (range f))"
-    by (rule seq_compact_imp_complete)
+    by (rule compact_imp_complete)
   moreover have "\<forall>n. f n \<in> closure (range f)"
     using closure_subset [of "range f"] by auto
   ultimately have "\<exists>l\<in>closure (range f). (f ---> l) sequentially"
@@ -3543,154 +3580,6 @@
   shows "(s ---> l) sequentially \<Longrightarrow> bounded (range s)"
   by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy)
 
-lemma nat_approx_posE:
-  fixes e::real
-  assumes "0 < e"
-  obtains n::nat where "1 / (Suc n) < e"
-proof atomize_elim
-  have " 1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
-    by (rule divide_strict_left_mono) (auto intro!: mult_pos_pos simp: `0 < e`)
-  also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
-    by (rule divide_left_mono) (auto intro!: divide_pos_pos simp: `0 < e`)
-  also have "\<dots> = e" by simp
-  finally show  "\<exists>n. 1 / real (Suc n) < e" ..
-qed
-
-lemma compact_eq_totally_bounded:
-  "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
-proof (safe intro!: seq_compact_imp_complete[unfolded  compact_eq_seq_compact_metric[symmetric]])
-  fix e::real
-  def f \<equiv> "(\<lambda>x::'a. ball x e) ` UNIV"
-  assume "0 < e" "compact s"
-  hence "(\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f \<longrightarrow> (\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')"
-    by (simp add: compact_eq_heine_borel)
-  moreover
-  have d0: "\<And>x::'a. dist x x < e" using `0 < e` by simp
-  hence "(\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f" by (auto simp: f_def intro!: d0)
-  ultimately have "(\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')" ..
-  then guess K .. note K = this
-  have "\<forall>K'\<in>K. \<exists>k. K' = ball k e" using K by (auto simp: f_def)
-  then obtain k where "\<And>K'. K' \<in> K \<Longrightarrow> K' = ball (k K') e" unfolding bchoice_iff by blast
-  thus "\<exists>k. finite k \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k" using K
-    by (intro exI[where x="k ` K"]) (auto simp: f_def)
-next
-  assume assms: "complete s" "\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k"
-  show "compact s"
-  proof cases
-    assume "s = {}" thus "compact s" by (simp add: compact_def)
-  next
-    assume "s \<noteq> {}"
-    show ?thesis
-      unfolding compact_def
-    proof safe
-      fix f::"nat \<Rightarrow> _" assume "\<forall>n. f n \<in> s" hence f: "\<And>n. f n \<in> s" by simp
-      from assms have "\<forall>e. \<exists>k. e>0 \<longrightarrow> finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))" by simp
-      then obtain K where
-        K: "\<And>e. e > 0 \<Longrightarrow> finite (K e) \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
-        unfolding choice_iff by blast
-      {
-        fix e::real and f' have f': "\<And>n::nat. (f o f') n \<in> s" using f by auto
-        assume "e > 0"
-        from K[OF this] have K: "finite (K e)" "s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
-          by simp_all
-        have "\<exists>k\<in>(K e). \<exists>r. subseq r \<and> (\<forall>i. (f o f' o r) i \<in> ball k e)"
-        proof (rule ccontr)
-          from K have "finite (K e)" "K e \<noteq> {}" "s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
-            using `s \<noteq> {}`
-            by auto
-          moreover
-          assume "\<not> (\<exists>k\<in>K e. \<exists>r. subseq r \<and> (\<forall>i. (f \<circ> f' o r) i \<in> ball k e))"
-          hence "\<And>r k. k \<in> K e \<Longrightarrow> subseq r \<Longrightarrow> (\<exists>i. (f o f' o r) i \<notin> ball k e)" by simp
-          ultimately
-          show False using f'
-          proof (induct arbitrary: s f f' rule: finite_ne_induct)
-            case (singleton x)
-            have "\<exists>i. (f \<circ> f' o id) i \<notin> ball x e" by (rule singleton) (auto simp: subseq_def)
-            thus ?case using singleton by (auto simp: ball_def)
-          next
-            case (insert x A)
-            show ?case
-            proof cases
-              have inf_ms: "infinite ((f o f') -` s)" using insert by (simp add: vimage_def)
-              have "infinite ((f o f') -` \<Union>((\<lambda>x. ball x e) ` (insert x A)))"
-                using insert by (intro infinite_super[OF _ inf_ms]) auto
-              also have "((f o f') -` \<Union>((\<lambda>x. ball x e) ` (insert x A))) =
-                {m. (f o f') m \<in> ball x e} \<union> {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}" by auto
-              finally have "infinite \<dots>" .
-              moreover assume "finite {m. (f o f') m \<in> ball x e}"
-              ultimately have inf: "infinite {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}" by blast
-              hence "A \<noteq> {}" by auto then obtain k where "k \<in> A" by auto
-              def r \<equiv> "enumerate {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}"
-              have r_mono: "\<And>n m. n < m \<Longrightarrow> r n < r m"
-                using enumerate_mono[OF _ inf] by (simp add: r_def)
-              hence "subseq r" by (simp add: subseq_def)
-              have r_in_set: "\<And>n. r n \<in> {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}"
-                using enumerate_in_set[OF inf] by (simp add: r_def)
-              show False
-              proof (rule insert)
-                show "\<Union>(\<lambda>x. ball x e) ` A \<subseteq> \<Union>(\<lambda>x. ball x e) ` A" by simp
-                fix k s assume "k \<in> A" "subseq s"
-                thus "\<exists>i. (f o f' o r o s) i \<notin> ball k e" using `subseq r`
-                  by (subst (2) o_assoc[symmetric]) (intro insert(6) subseq_o, simp_all)
-              next
-                fix n show "(f \<circ> f' o r) n \<in> \<Union>(\<lambda>x. ball x e) ` A" using r_in_set by auto
-              qed
-            next
-              assume inf: "infinite {m. (f o f') m \<in> ball x e}"
-              def r \<equiv> "enumerate {m. (f o f') m \<in> ball x e}"
-              have r_mono: "\<And>n m. n < m \<Longrightarrow> r n < r m"
-                using enumerate_mono[OF _ inf] by (simp add: r_def)
-              hence "subseq r" by (simp add: subseq_def)
-              from insert(6)[OF insertI1 this] obtain i where "(f o f') (r i) \<notin> ball x e" by auto
-              moreover
-              have r_in_set: "\<And>n. r n \<in> {m. (f o f') m \<in> ball x e}"
-                using enumerate_in_set[OF inf] by (simp add: r_def)
-              hence "(f o f') (r i) \<in> ball x e" by simp
-              ultimately show False by simp
-            qed
-          qed
-        qed
-      }
-      hence ex: "\<forall>f'. \<forall>e > 0. (\<exists>k\<in>K e. \<exists>r. subseq r \<and> (\<forall>i. (f o f' \<circ> r) i \<in> ball k e))" by simp
-      let ?e = "\<lambda>n. 1 / real (Suc n)"
-      let ?P = "\<lambda>n s. \<exists>k\<in>K (?e n). (\<forall>i. (f o s) i \<in> ball k (?e n))"
-      interpret subseqs ?P using ex by unfold_locales force
-      from `complete s` have limI: "\<And>f. (\<And>n. f n \<in> s) \<Longrightarrow> Cauchy f \<Longrightarrow> (\<exists>l\<in>s. f ----> l)"
-        by (simp add: complete_def)
-      have "\<exists>l\<in>s. (f o diagseq) ----> l"
-      proof (intro limI metric_CauchyI)
-        fix e::real assume "0 < e" hence "0 < e / 2" by auto
-        from nat_approx_posE[OF this] guess n . note n = this
-        show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) n) < e"
-        proof (rule exI[where x="Suc n"], safe)
-          fix m mm assume "Suc n \<le> m" "Suc n \<le> mm"
-          let ?e = "1 / real (Suc n)"
-          from reducer_reduces[of n] obtain k where
-            "k\<in>K ?e"  "\<And>i. (f o seqseq (Suc n)) i \<in> ball k ?e"
-            unfolding seqseq_reducer by auto
-          moreover
-          note diagseq_sub[OF `Suc n \<le> m`] diagseq_sub[OF `Suc n \<le> mm`]
-          ultimately have "{(f o diagseq) m, (f o diagseq) mm} \<subseteq> ball k ?e" by auto
-          also have "\<dots> \<subseteq> ball k (e / 2)" using n by (intro subset_ball) simp
-          finally
-          have "dist k ((f \<circ> diagseq) m) + dist k ((f \<circ> diagseq) mm) < e / 2 + e /2"
-            by (intro add_strict_mono) auto
-          hence "dist ((f \<circ> diagseq) m) k + dist ((f \<circ> diagseq) mm) k < e"
-            by (simp add: dist_commute)
-          moreover have "dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) mm) \<le>
-            dist ((f \<circ> diagseq) m) k + dist ((f \<circ> diagseq) mm) k"
-            by (rule dist_triangle2)
-          ultimately show "dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) mm) < e"
-            by simp
-        qed
-      next
-        fix n show "(f o diagseq) n \<in> s" using f by simp
-      qed
-      thus "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l" using subseq_diagseq by auto
-    qed
-  qed
-qed
-
 lemma compact_cball[simp]:
   fixes x :: "'a::heine_borel"
   shows "compact(cball x e)"
@@ -3872,6 +3761,10 @@
 lemma continuous_at: "continuous (at x) f \<longleftrightarrow> (f ---> f(x)) (at x)"
   using continuous_within [of x UNIV f] by simp
 
+lemma continuous_isCont: "isCont f x = continuous (at x) f"
+  unfolding isCont_def LIM_def
+  unfolding continuous_at Lim_at unfolding dist_nz by auto
+
 lemma continuous_at_within:
   assumes "continuous (at x) f"  shows "continuous (at x within s) f"
   using assms unfolding continuous_at continuous_within
@@ -5142,7 +5035,7 @@
 apply (rule_tac x="(l1, l2)" in rev_bexI, simp)
 apply (rule_tac x="r1 \<circ> r2" in exI)
 apply (rule conjI, simp add: subseq_def)
-apply (drule_tac r=r2 in lim_subseq [rotated], assumption)
+apply (drule_tac f=r2 in LIMSEQ_subseq_LIMSEQ, assumption)
 apply (drule (1) tendsto_Pair) back
 apply (simp add: o_def)
 done
@@ -5209,66 +5102,74 @@
 text {* Hence we get the following. *}
 
 lemma compact_sup_maxdistance:
-  fixes s :: "'a::real_normed_vector set"
+  fixes s :: "'a::metric_space set"
   assumes "compact s"  "s \<noteq> {}"
-  shows "\<exists>x\<in>s. \<exists>y\<in>s. \<forall>u\<in>s. \<forall>v\<in>s. norm(u - v) \<le> norm(x - y)"
+  shows "\<exists>x\<in>s. \<exists>y\<in>s. \<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
 proof-
-  have "{x - y | x y . x\<in>s \<and> y\<in>s} \<noteq> {}" using `s \<noteq> {}` by auto
-  then obtain x where x:"x\<in>{x - y |x y. x \<in> s \<and> y \<in> s}"  "\<forall>y\<in>{x - y |x y. x \<in> s \<and> y \<in> s}. norm y \<le> norm x"
-    using compact_differences[OF assms(1) assms(1)]
-    using distance_attains_sup[where 'a="'a", unfolded dist_norm, of "{x - y | x y . x\<in>s \<and> y\<in>s}" 0] by auto
-  from x(1) obtain a b where "a\<in>s" "b\<in>s" "x = a - b" by auto
-  thus ?thesis using x(2)[unfolded `x = a - b`] by blast
+  have "compact (s \<times> s)" using `compact s` by (intro compact_Times)
+  moreover have "s \<times> s \<noteq> {}" using `s \<noteq> {}` by auto
+  moreover have "continuous_on (s \<times> s) (\<lambda>x. dist (fst x) (snd x))"
+    by (intro continuous_at_imp_continuous_on ballI continuous_dist
+      continuous_isCont[THEN iffD1] isCont_fst isCont_snd isCont_ident)
+  ultimately show ?thesis
+    using continuous_attains_sup[of "s \<times> s" "\<lambda>x. dist (fst x) (snd x)"] by auto
 qed
 
 text {* We can state this in terms of diameter of a set. *}
 
-definition "diameter s = (if s = {} then 0::real else Sup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
-  (* TODO: generalize to class metric_space *)
+definition "diameter s = (if s = {} then 0::real else Sup {dist x y | x y. x \<in> s \<and> y \<in> s})"
+
+lemma diameter_bounded_bound:
+  fixes s :: "'a :: metric_space set"
+  assumes s: "bounded s" "x \<in> s" "y \<in> s"
+  shows "dist x y \<le> diameter s"
+proof -
+  let ?D = "{dist x y |x y. x \<in> s \<and> y \<in> s}"
+  from s obtain z d where z: "\<And>x. x \<in> s \<Longrightarrow> dist z x \<le> d"
+    unfolding bounded_def by auto
+  have "dist x y \<le> Sup ?D"
+  proof (rule Sup_upper, safe)
+    fix a b assume "a \<in> s" "b \<in> s"
+    with z[of a] z[of b] dist_triangle[of a b z]
+    show "dist a b \<le> 2 * d"
+      by (simp add: dist_commute)
+  qed (insert s, auto)
+  with `x \<in> s` show ?thesis
+    by (auto simp add: diameter_def)
+qed
+
+lemma diameter_lower_bounded:
+  fixes s :: "'a :: metric_space set"
+  assumes s: "bounded s" and d: "0 < d" "d < diameter s"
+  shows "\<exists>x\<in>s. \<exists>y\<in>s. d < dist x y"
+proof (rule ccontr)
+  let ?D = "{dist x y |x y. x \<in> s \<and> y \<in> s}"
+  assume contr: "\<not> ?thesis"
+  moreover
+  from d have "s \<noteq> {}"
+    by (auto simp: diameter_def)
+  then have "?D \<noteq> {}" by auto
+  ultimately have "Sup ?D \<le> d"
+    by (intro Sup_least) (auto simp: not_less)
+  with `d < diameter s` `s \<noteq> {}` show False
+    by (auto simp: diameter_def)
+qed
 
 lemma diameter_bounded:
   assumes "bounded s"
-  shows "\<forall>x\<in>s. \<forall>y\<in>s. norm(x - y) \<le> diameter s"
-        "\<forall>d>0. d < diameter s --> (\<exists>x\<in>s. \<exists>y\<in>s. norm(x - y) > d)"
-proof-
-  let ?D = "{norm (x - y) |x y. x \<in> s \<and> y \<in> s}"
-  obtain a where a:"\<forall>x\<in>s. norm x \<le> a" using assms[unfolded bounded_iff] by auto
-  { fix x y assume "x \<in> s" "y \<in> s"
-    hence "norm (x - y) \<le> 2 * a" using norm_triangle_ineq[of x "-y", unfolded norm_minus_cancel] a[THEN bspec[where x=x]] a[THEN bspec[where x=y]] by (auto simp add: field_simps)  }
-  note * = this
-  { fix x y assume "x\<in>s" "y\<in>s"  hence "s \<noteq> {}" by auto
-    have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s`
-      by simp (blast del: Sup_upper intro!: * Sup_upper) }
-  moreover
-  { fix d::real assume "d>0" "d < diameter s"
-    hence "s\<noteq>{}" unfolding diameter_def by auto
-    have "\<exists>d' \<in> ?D. d' > d"
-    proof(rule ccontr)
-      assume "\<not> (\<exists>d'\<in>{norm (x - y) |x y. x \<in> s \<and> y \<in> s}. d < d')"
-      hence "\<forall>d'\<in>?D. d' \<le> d" by auto (metis not_leE) 
-      thus False using `d < diameter s` `s\<noteq>{}` 
-        apply (auto simp add: diameter_def) 
-        apply (drule Sup_real_iff [THEN [2] rev_iffD2])
-        apply (auto, force) 
-        done
-    qed
-    hence "\<exists>x\<in>s. \<exists>y\<in>s. norm(x - y) > d" by auto  }
-  ultimately show "\<forall>x\<in>s. \<forall>y\<in>s. norm(x - y) \<le> diameter s"
-        "\<forall>d>0. d < diameter s --> (\<exists>x\<in>s. \<exists>y\<in>s. norm(x - y) > d)" by auto
-qed
-
-lemma diameter_bounded_bound:
- "bounded s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s ==> norm(x - y) \<le> diameter s"
-  using diameter_bounded by blast
+  shows "\<forall>x\<in>s. \<forall>y\<in>s. dist x y \<le> diameter s"
+        "\<forall>d>0. d < diameter s \<longrightarrow> (\<exists>x\<in>s. \<exists>y\<in>s. dist x y > d)"
+  using diameter_bounded_bound[of s] diameter_lower_bounded[of s] assms
+  by auto
 
 lemma diameter_compact_attained:
-  fixes s :: "'a::real_normed_vector set"
   assumes "compact s"  "s \<noteq> {}"
-  shows "\<exists>x\<in>s. \<exists>y\<in>s. (norm(x - y) = diameter s)"
-proof-
+  shows "\<exists>x\<in>s. \<exists>y\<in>s. dist x y = diameter s"
+proof -
   have b:"bounded s" using assms(1) by (rule compact_imp_bounded)
-  then obtain x y where xys:"x\<in>s" "y\<in>s" and xy:"\<forall>u\<in>s. \<forall>v\<in>s. norm (u - v) \<le> norm (x - y)" using compact_sup_maxdistance[OF assms] by auto
-  hence "diameter s \<le> norm (x - y)"
+  then obtain x y where xys:"x\<in>s" "y\<in>s" and xy:"\<forall>u\<in>s. \<forall>v\<in>s. dist u v \<le> dist x y"
+    using compact_sup_maxdistance[OF assms] by auto
+  hence "diameter s \<le> dist x y"
     unfolding diameter_def by clarsimp (rule Sup_least, fast+)
   thus ?thesis
     by (metis b diameter_bounded_bound order_antisym xys)
@@ -5326,7 +5227,7 @@
     obtain l' r where "l'\<in>s" and r:"subseq r" and lr:"(((\<lambda>n. fst (f n)) \<circ> r) ---> l') sequentially"
       using assms(1)[unfolded compact_def, THEN spec[where x="\<lambda> n. fst (f n)"]] using f(2) by auto
     have "((\<lambda>n. snd (f (r n))) ---> l - l') sequentially"
-      using tendsto_diff[OF lim_subseq[OF r as(2)] lr] and f(1) unfolding o_def by auto
+      using tendsto_diff[OF LIMSEQ_subseq_LIMSEQ[OF as(2) r] lr] and f(1) unfolding o_def by auto
     hence "l - l' \<in> t"
       using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\<lambda> n. snd (f (r n))"], THEN spec[where x="l - l'"]]
       using f(3) by auto
@@ -6320,11 +6221,6 @@
   thus ?thesis unfolding complete_def by auto
 qed
 
-lemma dist_0_norm:
-  fixes x :: "'a::real_normed_vector"
-  shows "dist 0 x = norm x"
-unfolding dist_norm by simp
-
 lemma injective_imp_isometric: fixes f::"'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes s:"closed s"  "subspace s"  and f:"bounded_linear f" "\<forall>x\<in>s. (f x = 0) \<longrightarrow> (x = 0)"
   shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm(x)"
@@ -6699,7 +6595,7 @@
 subsection {* Edelstein fixed point theorem *}
 
 lemma edelstein_fix:
-  fixes s :: "'a::real_normed_vector set"
+  fixes s :: "'a::metric_space set"
   assumes s:"compact s" "s \<noteq> {}" and gs:"(g ` s) \<subseteq> s"
       and dist:"\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
   shows "\<exists>! x\<in>s. g x = x"
@@ -6760,23 +6656,29 @@
     unfolding o_def a_def b_def by (rule tendsto_intros)+
 
   { fix n::nat
-    have *:"\<And>fx fy (x::'a) y. dist fx fy \<le> dist x y \<Longrightarrow> \<not> (dist (fx - fy) (a - b) < dist a b - dist x y)" unfolding dist_norm by norm
-    { fix x y :: 'a
-      have "dist (-x) (-y) = dist x y" unfolding dist_norm
-        using norm_minus_cancel[of "x - y"] by (auto simp add: uminus_add_conv_diff) } note ** = this
+    have *:"\<And>fx fy (x::'a) y. dist fx fy \<le> dist x y \<Longrightarrow> \<not> (\<bar>dist fx fy - dist a b\<bar> < dist a b - dist x y)" by auto
 
     { assume as:"dist a b > dist (f n x) (f n y)"
       then obtain Na Nb where "\<forall>m\<ge>Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2"
         and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2"
         using lima limb unfolding h_def LIMSEQ_def by (fastforce simp del: less_divide_eq_numeral1)
-      hence "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) < dist a b - dist (f n x) (f n y)"
-        apply(erule_tac x="Na+Nb+n" in allE)
-        apply(erule_tac x="Na+Nb+n" in allE) apply simp
-        using dist_triangle_add_half[of a "f (r (Na + Nb + n)) x" "dist a b - dist (f n x) (f n y)"
-          "-b"  "- f (r (Na + Nb + n)) y"]
-        unfolding ** by (auto simp add: algebra_simps dist_commute)
+      hence "\<bar>dist (f (r (Na + Nb + n)) x) (f (r (Na + Nb + n)) y) - dist a b\<bar> < dist a b - dist (f n x) (f n y)"
+        apply -
+        apply (drule_tac x="Na+Nb+n" in spec, drule mp, simp)
+        apply (drule_tac x="Na+Nb+n" in spec, drule mp, simp)
+        apply (drule (1) add_strict_mono, simp only: real_sum_of_halves)
+        apply (erule le_less_trans [rotated])
+        apply (erule thin_rl)
+        apply (rule abs_leI)
+        apply (simp add: diff_le_iff add_assoc)
+        apply (rule order_trans [OF dist_triangle add_left_mono])
+        apply (subst add_commute, rule dist_triangle2)
+        apply (simp add: diff_le_iff add_assoc)
+        apply (rule order_trans [OF dist_triangle3 add_left_mono])
+        apply (subst add_commute, rule dist_triangle)
+        done
       moreover
-      have "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) \<ge> dist a b - dist (f n x) (f n y)"
+      have "\<bar>dist (f (r (Na + Nb + n)) x) (f (r (Na + Nb + n)) y) - dist a b\<bar> \<ge> dist a b - dist (f n x) (f n y)"
         using distf[of n "r (Na+Nb+n)", OF _ `x\<in>s` `y\<in>s`]
         using seq_suble[OF r, of "Na+Nb+n"]
         using *[of "f (r (Na + Nb + n)) x" "f (r (Na + Nb + n)) y" "f n x" "f n y"] by auto
@@ -6797,7 +6699,10 @@
     moreover have "dist (f (Suc n) y) (g b) \<le> dist (f n y) b"
       using dist[THEN bspec[where x="f n y"], THEN bspec[where x="b"]] and fs by auto
     ultimately have "dist (f (Suc n) x) (g a) + dist (f (Suc n) y) (g b) < e" using n by auto
-    thus False unfolding e_def using ab_fn[of "Suc n"] by norm
+    thus False unfolding e_def using ab_fn[of "Suc n"]
+      using dist_triangle2 [of "f (Suc n) y" "g a" "g b"]
+      using dist_triangle2 [of "f (Suc n) x" "f (Suc n) y" "g a"]
+      by auto
   qed
 
   have [simp]:"\<And>n. f (Suc n) x = f n y" unfolding f_def y_def by(induct_tac n)auto
diff -r 20edcc6a8def -r 21da2a03b9d2 src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Fri Jan 18 20:24:51 2013 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy	Fri Jan 18 20:31:22 2013 +0100
@@ -11,7 +11,7 @@
     Regularity
     Projective_Family
     Infinite_Product_Measure
-    "~~/src/HOL/Library/Countable_Set"
+    "~~/src/HOL/Library/Diagonal_Subsequence"
 begin
 
 subsection {* Sequences of Finite Maps in Compact Sets *}
diff -r 20edcc6a8def -r 21da2a03b9d2 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jan 18 20:24:51 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Jan 18 20:31:22 2013 +0100
@@ -849,7 +849,7 @@
 
 fun filter_type_args thy constrs type_enc s ary T_args =
   let val poly = polymorphism_of_type_enc type_enc in
-    if s = type_tag_name then (* ### FIXME: why not "type_guard_name" as well? *)
+    if s = type_tag_name then (* FIXME: why not "type_guard_name" as well? *)
       T_args
     else case type_enc of
       Native (_, Raw_Polymorphic _, _) => T_args
@@ -1383,7 +1383,7 @@
 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
    dangerous because their "exhaust" properties can easily lead to unsound ATP
    proofs. On the other hand, all HOL infinite types can be given the same
-   models in first-order logic (via Löwenheim-Skolem). *)
+   models in first-order logic (via Loewenheim-Skolem). *)
 
 fun should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
                              maybe_nonmono_Ts}
@@ -1580,7 +1580,7 @@
     fun add_iterm_syms conj_fact =
       add_iterm_syms_to_sym_table ctxt app_op_level conj_fact true
     fun add_fact_syms conj_fact =
-      K (add_iterm_syms conj_fact) |> formula_fold NONE |> ifact_lift
+      ifact_lift (formula_fold NONE (K (add_iterm_syms conj_fact)))
   in
     ((false, []), Symtab.empty)
     |> fold (add_fact_syms true) conjs
@@ -2243,7 +2243,7 @@
          | _ => I)
         #> fold add_iterm_syms args
       end
-    val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> ifact_lift
+    val add_fact_syms = ifact_lift (formula_fold NONE (K add_iterm_syms))
     fun add_formula_var_types (ATyQuant (_, _, phi)) = add_formula_var_types phi
       | add_formula_var_types (AQuant (_, xs, phi)) =
         fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs
@@ -2291,8 +2291,8 @@
      | _ => known_infinite_types,
    maybe_nonmono_Ts = [if completish then tvar_a else @{typ bool}]}
 
-(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
-   out with monotonicity" paper presented at CADE 2011. *)
+(* This inference is described in section 4 of Blanchette et al., "Encoding
+   monomorphic and polymorphic types", TACAS 2013. *)
 fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
   | add_iterm_mononotonicity_info ctxt level _
         (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
@@ -2338,8 +2338,10 @@
       | add_args _ = I
     and add_term tm = add_type (ityp_of tm) #> add_args tm
   in formula_fold NONE (K add_term) end
+
 fun add_fact_monotonic_types ctxt mono type_enc =
-  add_iformula_monotonic_types ctxt mono type_enc |> ifact_lift
+  ifact_lift (add_iformula_monotonic_types ctxt mono type_enc)
+
 fun monotonic_types_for_facts ctxt mono type_enc facts =
   let val level = level_of_type_enc type_enc in
     [] |> (is_type_enc_polymorphic type_enc andalso
@@ -2396,8 +2398,7 @@
                    ? curry APi (map (tvar_name o dest_TVar) T_args))
   end
 
-fun honor_conj_sym_role in_conj =
-  if in_conj then (Hypothesis, I) else (Axiom, I)
+fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I)
 
 fun line_for_guards_sym_decl ctxt mono type_enc n s j
                              (s', T_args, T, _, ary, in_conj) =
diff -r 20edcc6a8def -r 21da2a03b9d2 src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Fri Jan 18 20:24:51 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_util.ML	Fri Jan 18 20:31:22 2013 +0100
@@ -156,12 +156,11 @@
     let
       val tvars = Term.add_tvar_namesT T []
       val tvars' = Term.add_tvar_namesT T' []
+      val maxidx' = maxidx_of_typ T'
       val T =
-        if exists (member (op =) tvars') tvars then
-          T |> Logic.incr_tvar (maxidx_of_typ T' + 1)
-        else
-          T
-    in can (Sign.typ_unify thy (T, T')) (Vartab.empty, 0) end
+        T |> exists (member (op =) tvars') tvars ? Logic.incr_tvar (maxidx' + 1)
+      val maxidx = Integer.max (maxidx_of_typ T) maxidx'
+    in can (Sign.typ_unify thy (T, T')) (Vartab.empty, maxidx) end
 
 val type_equiv = Sign.typ_equiv
 
diff -r 20edcc6a8def -r 21da2a03b9d2 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 18 20:24:51 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 18 20:31:22 2013 +0100
@@ -39,7 +39,7 @@
       -> (string * string list * (string * real) list * string list) list -> unit
     val relearn :
       Proof.context -> bool -> (string * string list) list -> unit
-    val suggest :
+    val query :
       Proof.context -> bool -> bool -> int
       -> string list * (string * real) list * string list -> string list
   end
@@ -256,8 +256,8 @@
          elide_string 1000 (space_implode " " (map #1 relearns)));
      run_mash_tool ctxt overlord true 0 (relearns, str_of_relearn) (K ()))
 
-fun suggest ctxt overlord learn_hints max_suggs (query as (_, feats, hints)) =
-  (trace_msg ctxt (fn () => "MaSh suggest " ^ encode_features feats);
+fun query ctxt overlord learn_hints max_suggs (query as (_, feats, hints)) =
+  (trace_msg ctxt (fn () => "MaSh query " ^ encode_features feats);
    run_mash_tool ctxt overlord (learn_hints andalso not (null hints))
        max_suggs ([query], str_of_query learn_hints)
        (fn suggs =>
@@ -808,8 +808,8 @@
                 chained |> filter (is_fact_in_graph access_G snd)
                         |> map (nickname_of_thm o snd)
             in
-              (access_G, MaSh.suggest ctxt overlord learn max_facts
-                                      (parents, feats, hints))
+              (access_G, MaSh.query ctxt overlord learn max_facts
+                                    (parents, feats, hints))
             end)
     val unknown = facts |> filter_out (is_fact_in_graph access_G snd)
   in find_mash_suggestions max_facts suggs facts chained unknown end