# HG changeset patch
# User blanchet
# Date 1261059747 -3600
# Node ID 7aac4d74bb76664535cd951c4bfdd5cd199609ec
# Parent  c4628a1dcf75e4059b94c656d444c5d33118054c# Parent  87cbdecaa87958281c6f2a0b79a9c03449b509a7
merged

diff -r c4628a1dcf75 -r 7aac4d74bb76 Admin/user-aliases
--- a/Admin/user-aliases	Thu Dec 17 15:22:11 2009 +0100
+++ b/Admin/user-aliases	Thu Dec 17 15:22:27 2009 +0100
@@ -1,5 +1,6 @@
 lcp paulson
 norbert.schirmer@web.de schirmer
+schirmer@in.tum.de schirmer
 urbanc@in.tum.de urbanc
 nipkow@lapbroy100.local nipkow
 chaieb@chaieb-laptop chaieb
diff -r c4628a1dcf75 -r 7aac4d74bb76 src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Thu Dec 17 15:22:11 2009 +0100
+++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Thu Dec 17 15:22:27 2009 +0100
@@ -50,7 +50,7 @@
 text {* Let's find out which assertions of @{text max} are hard to prove: *}
 
 boogie_status (narrow timeout: 4) max
-  (try: (simp add: labels, (fast | blast)?))
+  (try: (simp add: labels, (fast | metis)?))
   -- {* The argument @{text timeout} is optional, restricting the runtime of
         each narrowing step by the given number of seconds. *}
   -- {* The tag @{text try} expects a method to be applied at each narrowing
diff -r c4628a1dcf75 -r 7aac4d74bb76 src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Thu Dec 17 15:22:11 2009 +0100
+++ b/src/HOL/Fun.thy	Thu Dec 17 15:22:27 2009 +0100
@@ -458,7 +458,7 @@
 where
   "swap a b f = f (a := f b, b:= f a)"
 
-lemma swap_self: "swap a a f = f"
+lemma swap_self [simp]: "swap a a f = f"
 by (simp add: swap_def)
 
 lemma swap_commute: "swap a b f = swap b a f"
@@ -467,6 +467,9 @@
 lemma swap_nilpotent [simp]: "swap a b (swap a b f) = f"
 by (rule ext, simp add: fun_upd_def swap_def)
 
+lemma comp_swap: "f \<circ> swap a b g = swap a b (f \<circ> g)"
+by (rule ext, simp add: fun_upd_def swap_def)
+
 lemma inj_on_imp_inj_on_swap:
   "[|inj_on f A; a \<in> A; b \<in> A|] ==> inj_on (swap a b f) A"
 by (simp add: inj_on_def swap_def, blast)
diff -r c4628a1dcf75 -r 7aac4d74bb76 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Thu Dec 17 15:22:11 2009 +0100
+++ b/src/HOL/Library/Permutations.thy	Thu Dec 17 15:22:27 2009 +0100
@@ -15,7 +15,6 @@
 (* Transpositions.                                                           *)
 (* ------------------------------------------------------------------------- *)
 
-declare swap_self[simp]
 lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id"
   by (auto simp add: expand_fun_eq swap_def fun_upd_def)
 lemma swap_id_refl: "Fun.swap a a id = id" by simp
diff -r c4628a1dcf75 -r 7aac4d74bb76 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Dec 17 15:22:11 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Dec 17 15:22:27 2009 +0100
@@ -208,13 +208,14 @@
     have *:"\<And>x. x - vec 0 = (x::real^'n)" by auto 
     have **:"\<And>d x. d * (c x $ k - (c (netlimit net) $ k + c' (x - netlimit net) $ k)) = (d *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net) ))) $k" by(auto simp add:field_simps)
     fix e assume "\<not> trivial_limit net" "0 < (e::real)"
-    then obtain A where A:"A\<in>Rep_net net" "\<forall>x\<in>A. dist ((1 / norm (x - netlimit net)) *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net)))) 0 < e"
-      using assms[unfolded has_derivative_def Lim] unfolding eventually_def by auto
-    show "eventually (\<lambda>x. dist (1 / norm (x - netlimit net) * (c x $ k - (c (netlimit net) $ k + c' (x - netlimit net) $ k))) 0 < e) net"
-      unfolding eventually_def apply(rule_tac x=A in bexI) apply rule proof-
-      case goal1 thus ?case apply -apply(drule A(2)[rule_format]) unfolding vector_dist_norm vec1_vec apply(rule le_less_trans) prefer 2 apply assumption unfolding * ** and norm_vec1[unfolded vec1_vec]
-	using component_le_norm[of "(1 / norm (x - netlimit net)) *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net))) - 0" k] by auto
-      qed(insert A, auto) qed(insert assms[unfolded has_derivative_def], auto simp add:linear_conv_bounded_linear) qed 
+    then have "eventually (\<lambda>x. dist ((1 / norm (x - netlimit net)) *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net)))) 0 < e) net"
+      using assms[unfolded has_derivative_def Lim] by auto
+    thus "eventually (\<lambda>x. dist (1 / norm (x - netlimit net) * (c x $ k - (c (netlimit net) $ k + c' (x - netlimit net) $ k))) 0 < e) net"
+      proof (rule eventually_elim1)
+      case goal1 thus ?case apply - unfolding vector_dist_norm vec1_vec apply(rule le_less_trans) prefer 2 apply assumption unfolding * ** and norm_vec1[unfolded vec1_vec]
+        using component_le_norm[of "(1 / norm (x - netlimit net)) *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net))) - 0" k] by auto
+      qed
+      qed(insert assms[unfolded has_derivative_def], auto simp add:linear_conv_bounded_linear) qed 
 
 lemma has_derivative_vmul_within: fixes c::"real \<Rightarrow> real" and v::"real^'a::finite"
   assumes "(c has_derivative c') (at x within s)"
diff -r c4628a1dcf75 -r 7aac4d74bb76 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Dec 17 15:22:11 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Dec 17 15:22:27 2009 +0100
@@ -383,14 +383,15 @@
                  ~(e2 = {}))"
 unfolding connected_def openin_open by (safe, blast+)
 
-lemma exists_diff: "(\<exists>S. P(UNIV - S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs")
+lemma exists_diff:
+  fixes P :: "'a set \<Rightarrow> bool"
+  shows "(\<exists>S. P(- S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
-
   {assume "?lhs" hence ?rhs by blast }
   moreover
   {fix S assume H: "P S"
-    have "S = UNIV - (UNIV - S)" by auto
-    with H have "P (UNIV - (UNIV - S))" by metis }
+    have "S = - (- S)" by auto
+    with H have "P (- (- S))" by metis }
   ultimately show ?thesis by metis
 qed
 
@@ -398,11 +399,11 @@
         (\<forall>T. openin (subtopology euclidean S) T \<and>
             closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
-  have " \<not> connected S \<longleftrightarrow> (\<exists>e1 e2. open e1 \<and> open (UNIV - e2) \<and> S \<subseteq> e1 \<union> (UNIV - e2) \<and> e1 \<inter> (UNIV - e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (UNIV - e2) \<inter> S \<noteq> {})"
+  have " \<not> connected S \<longleftrightarrow> (\<exists>e1 e2. open e1 \<and> open (- e2) \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
     unfolding connected_def openin_open closedin_closed
     apply (subst exists_diff) by blast
-  hence th0: "connected S \<longleftrightarrow> \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (UNIV - e2) \<and> e1 \<inter> (UNIV - e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (UNIV - e2) \<inter> S \<noteq> {})"
-    (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") apply (simp add: closed_def Compl_eq_Diff_UNIV) by metis
+  hence th0: "connected S \<longleftrightarrow> \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
+    (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") apply (simp add: closed_def) by metis
 
   have th1: "?rhs \<longleftrightarrow> \<not> (\<exists>t' t. closed t'\<and>t = S\<inter>t' \<and> t\<noteq>{} \<and> t\<noteq>S \<and> (\<exists>t'. open t' \<and> t = S \<inter> t'))"
     (is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)")
@@ -558,8 +559,8 @@
 lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)"
   unfolding closed_def
   apply (subst open_subopen)
-  apply (simp add: islimpt_def subset_eq Compl_eq_Diff_UNIV)
-  by (metis DiffE DiffI UNIV_I insertCI insert_absorb mem_def)
+  apply (simp add: islimpt_def subset_eq)
+  by (metis ComplE ComplI insertCI insert_absorb mem_def)
 
 lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
   unfolding islimpt_def by auto
@@ -719,12 +720,12 @@
 
 definition "closure S = S \<union> {x | x. x islimpt S}"
 
-lemma closure_interior: "closure S = UNIV - interior (UNIV - S)"
+lemma closure_interior: "closure S = - interior (- S)"
 proof-
   { fix x
-    have "x\<in>UNIV - interior (UNIV - S) \<longleftrightarrow> x \<in> closure S"  (is "?lhs = ?rhs")
+    have "x\<in>- interior (- S) \<longleftrightarrow> x \<in> closure S"  (is "?lhs = ?rhs")
     proof
-      let ?exT = "\<lambda> y. (\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> UNIV - S)"
+      let ?exT = "\<lambda> y. (\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> - S)"
       assume "?lhs"
       hence *:"\<not> ?exT x"
         unfolding interior_def
@@ -746,10 +747,10 @@
     by blast
 qed
 
-lemma interior_closure: "interior S = UNIV - (closure (UNIV - S))"
+lemma interior_closure: "interior S = - (closure (- S))"
 proof-
   { fix x
-    have "x \<in> interior S \<longleftrightarrow> x \<in> UNIV - (closure (UNIV - S))"
+    have "x \<in> interior S \<longleftrightarrow> x \<in> - (closure (- S))"
       unfolding interior_def closure_def islimpt_def
       by auto
   }
@@ -759,7 +760,7 @@
 
 lemma closed_closure[simp, intro]: "closed (closure S)"
 proof-
-  have "closed (UNIV - interior (UNIV -S))" by blast
+  have "closed (- interior (-S))" by blast
   thus ?thesis using closure_interior[of S] by simp
 qed
 
@@ -844,8 +845,8 @@
 
 lemma open_inter_closure_eq_empty:
   "open S \<Longrightarrow> (S \<inter> closure T) = {} \<longleftrightarrow> S \<inter> T = {}"
-  using open_subset_interior[of S "UNIV - T"]
-  using interior_subset[of "UNIV - T"]
+  using open_subset_interior[of S "- T"]
+  using interior_subset[of "- T"]
   unfolding closure_interior
   by auto
 
@@ -873,16 +874,16 @@
     by blast
 qed
 
-lemma closure_complement: "closure(UNIV - S) = UNIV - interior(S)"
+lemma closure_complement: "closure(- S) = - interior(S)"
 proof-
-  have "S = UNIV - (UNIV - S)"
+  have "S = - (- S)"
     by auto
   thus ?thesis
     unfolding closure_interior
     by auto
 qed
 
-lemma interior_complement: "interior(UNIV - S) = UNIV - closure(S)"
+lemma interior_complement: "interior(- S) = - closure(S)"
   unfolding closure_interior
   by blast
 
@@ -893,7 +894,7 @@
 lemma frontier_closed: "closed(frontier S)"
   by (simp add: frontier_def closed_Diff)
 
-lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(UNIV - S))"
+lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(- S))"
   by (auto simp add: frontier_def interior_closure)
 
 lemma frontier_straddle:
@@ -937,10 +938,10 @@
   { fix T assume "a \<in> T"  "open T" "a\<in>S"
     then obtain e where "e>0" and balle: "ball a e \<subseteq> T" unfolding open_contains_ball using `?rhs` by auto
     obtain x where "x \<notin> S" "dist a x < e" using `?rhs` using `e>0` by auto
-    hence "\<exists>y\<in>UNIV - S. y \<in> T \<and> y \<noteq> a" using balle `a\<in>S` unfolding ball_def by (rule_tac x=x in bexI)auto
+    hence "\<exists>y\<in>- S. y \<in> T \<and> y \<noteq> a" using balle `a\<in>S` unfolding ball_def by (rule_tac x=x in bexI)auto
   }
-  hence "a islimpt (UNIV - S) \<or> a\<notin>S" unfolding islimpt_def by auto
-  ultimately show ?lhs unfolding frontier_closures using closure_def[of "UNIV - S"] by auto
+  hence "a islimpt (- S) \<or> a\<notin>S" unfolding islimpt_def by auto
+  ultimately show ?lhs unfolding frontier_closures using closure_def[of "- S"] by auto
 qed
 
 lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S"
@@ -958,12 +959,12 @@
   thus ?thesis using frontier_subset_closed[of S] by auto
 qed
 
-lemma frontier_complement: "frontier(UNIV - S) = frontier S"
+lemma frontier_complement: "frontier(- S) = frontier S"
   by (auto simp add: frontier_def closure_complement interior_complement)
 
 lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
-  using frontier_complement frontier_subset_eq[of "UNIV - S"]
-  unfolding open_closed Compl_eq_Diff_UNIV by auto
+  using frontier_complement frontier_subset_eq[of "- S"]
+  unfolding open_closed by auto
 
 subsection{* Common nets and The "within" modifier for nets. *}
 
@@ -2437,7 +2438,7 @@
   thus "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < e"  using dist_triangle_half_l[of _ l e _] by (rule_tac x=N in exI) auto
 qed
 
-lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded {y. (\<exists>n::nat. y = s n)}"
+lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded (range s)"
 proof-
   from assms obtain N::nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1" unfolding cauchy_def apply(erule_tac x= 1 in allE) by auto
   hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
@@ -2448,7 +2449,7 @@
   ultimately show "?thesis"
     unfolding bounded_any_center [where a="s N"]
     apply(rule_tac x="max a 1" in exI) apply auto
-    apply(erule_tac x=n in allE) apply(erule_tac x=n in ballE) by auto
+    apply(erule_tac x=y in allE) apply(erule_tac x=y in ballE) by auto
 qed
 
 lemma compact_imp_complete: assumes "compact s" shows "complete s"
@@ -2474,12 +2475,12 @@
 instance heine_borel < complete_space
 proof
   fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
-  hence "bounded (range f)" unfolding image_def
-    using cauchy_imp_bounded [of f] by auto
+  hence "bounded (range f)"
+    by (rule cauchy_imp_bounded)
   hence "compact (closure (range f))"
     using bounded_closed_imp_compact [of "closure (range f)"] by auto
   hence "complete (closure (range f))"
-    using compact_imp_complete by auto
+    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"
@@ -2732,10 +2733,10 @@
 lemma sequence_infinite_lemma:
   fixes l :: "'a::metric_space" (* TODO: generalize *)
   assumes "\<forall>n::nat. (f n  \<noteq> l)"  "(f ---> l) sequentially"
-  shows "infinite {y. (\<exists> n. y = f n)}"
-proof(rule ccontr)
-  let ?A = "(\<lambda>x. dist x l) ` {y. \<exists>n. y = f n}"
-  assume "\<not> infinite {y. \<exists>n. y = f n}"
+  shows "infinite (range f)"
+proof
+  let ?A = "(\<lambda>x. dist x l) ` range f"
+  assume "finite (range f)"
   hence **:"finite ?A" "?A \<noteq> {}" by auto
   obtain k where k:"dist (f k) l = Min ?A" using Min_in[OF **] by auto
   have "0 < Min ?A" using assms(1) unfolding dist_nz unfolding Min_gr_iff[OF **] by auto
@@ -2746,7 +2747,7 @@
 
 lemma sequence_unique_limpt:
   fixes l :: "'a::metric_space" (* TODO: generalize *)
-  assumes "\<forall>n::nat. (f n \<noteq> l)"  "(f ---> l) sequentially"  "l' islimpt {y.  (\<exists>n. y = f n)}"
+  assumes "\<forall>n::nat. (f n \<noteq> l)"  "(f ---> l) sequentially"  "l' islimpt (range f)"
   shows "l' = l"
 proof(rule ccontr)
   def e \<equiv> "dist l' l"
@@ -2773,8 +2774,8 @@
       case False thus "l\<in>s" using as(1) by auto
     next
       case True note cas = this
-      with as(2) have "infinite {y. \<exists>n. y = x n}" using sequence_infinite_lemma[of x l] by auto
-      then obtain l' where "l'\<in>s" "l' islimpt {y. \<exists>n. y = x n}" using assms[THEN spec[where x="{y. \<exists>n. y = x n}"]] as(1) by auto
+      with as(2) have "infinite (range x)" using sequence_infinite_lemma[of x l] by auto
+      then obtain l' where "l'\<in>s" "l' islimpt (range x)" using assms[THEN spec[where x="range x"]] as(1) by auto
       thus "l\<in>s" using sequence_unique_limpt[of x l l'] using as cas by auto
     qed  }
   thus ?thesis unfolding closed_sequential_limits by fast
@@ -2957,11 +2958,11 @@
   shows "s \<inter> (\<Inter> f) \<noteq> {}"
 proof
   assume as:"s \<inter> (\<Inter> f) = {}"
-  hence "s \<subseteq> \<Union>op - UNIV ` f" by auto
-  moreover have "Ball (op - UNIV ` f) open" using open_Diff closed_Diff using assms(2) by auto
-  ultimately obtain f' where f':"f' \<subseteq> op - UNIV ` f"  "finite f'"  "s \<subseteq> \<Union>f'" using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="(\<lambda>t. UNIV - t) ` f"]] by auto
-  hence "finite (op - UNIV ` f') \<and> op - UNIV ` f' \<subseteq> f" by(auto simp add: Diff_Diff_Int)
-  hence "s \<inter> \<Inter>op - UNIV ` f' \<noteq> {}" using assms(3)[THEN spec[where x="op - UNIV ` f'"]] by auto
+  hence "s \<subseteq> \<Union> uminus ` f" by auto
+  moreover have "Ball (uminus ` f) open" using open_Diff closed_Diff using assms(2) by auto
+  ultimately obtain f' where f':"f' \<subseteq> uminus ` f"  "finite f'"  "s \<subseteq> \<Union>f'" using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="(\<lambda>t. - t) ` f"]] by auto
+  hence "finite (uminus ` f') \<and> uminus ` f' \<subseteq> f" by(auto simp add: Diff_Diff_Int)
+  hence "s \<inter> \<Inter>uminus ` f' \<noteq> {}" using assms(3)[THEN spec[where x="uminus ` f'"]] by auto
   thus False using f'(3) unfolding subset_eq and Union_iff by blast
 qed
 
@@ -3031,21 +3032,22 @@
 text{* Strengthen it to the intersection actually being a singleton.             *}
 
 lemma decreasing_closed_nest_sing:
+  fixes s :: "nat \<Rightarrow> 'a::heine_borel set"
   assumes "\<forall>n. closed(s n)"
           "\<forall>n. s n \<noteq> {}"
           "\<forall>m n. m \<le> n --> s n \<subseteq> s m"
           "\<forall>e>0. \<exists>n. \<forall>x \<in> (s n). \<forall> y\<in>(s n). dist x y < e"
-  shows "\<exists>a::'a::heine_borel. \<Inter> {t. (\<exists>n::nat. t = s n)} = {a}"
+  shows "\<exists>a. \<Inter>(range s) = {a}"
 proof-
   obtain a where a:"\<forall>n. a \<in> s n" using decreasing_closed_nest[of s] using assms by auto
-  { fix b assume b:"b \<in> \<Inter>{t. \<exists>n. t = s n}"
+  { fix b assume b:"b \<in> \<Inter>(range s)"
     { fix e::real assume "e>0"
       hence "dist a b < e" using assms(4 )using b using a by blast
     }
     hence "dist a b = 0" by (metis dist_eq_0_iff dist_nz real_less_def)
   }
-  with a have "\<Inter>{t. \<exists>n. t = s n} = {a}"  by auto
-  thus ?thesis by auto
+  with a have "\<Inter>(range s) = {a}" unfolding image_def by auto
+  thus ?thesis ..
 qed
 
 text{* Cauchy-type criteria for uniform convergence. *}
@@ -4547,6 +4549,11 @@
   thus ?thesis using compact_closed_sums[OF compact_sing[of a] assms] by auto
 qed
 
+lemma translation_Compl:
+  fixes a :: "'a::ab_group_add"
+  shows "(\<lambda>x. a + x) ` (- t) = - ((\<lambda>x. a + x) ` t)"
+  apply (auto simp add: image_iff) apply(rule_tac x="x - a" in bexI) by auto
+
 lemma translation_UNIV:
   fixes a :: "'a::ab_group_add" shows "range (\<lambda>x. a + x) = UNIV"
   apply (auto simp add: image_iff) apply(rule_tac x="x - a" in exI) by auto
@@ -4560,10 +4567,10 @@
   fixes a :: "'a::real_normed_vector"
   shows "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)"
 proof-
-  have *:"op + a ` (UNIV - s) = UNIV - op + a ` s"
+  have *:"op + a ` (- s) = - op + a ` s"
     apply auto unfolding image_iff apply(rule_tac x="x - a" in bexI) by auto
-  show ?thesis unfolding closure_interior translation_diff translation_UNIV
-    using interior_translation[of a "UNIV - s"] unfolding * by auto
+  show ?thesis unfolding closure_interior translation_Compl
+    using interior_translation[of a "- s"] unfolding * by auto
 qed
 
 lemma frontier_translation:
@@ -5162,14 +5169,14 @@
 
 lemma open_halfspace_lt: "open {x. inner a x < b}"
 proof-
-  have "UNIV - {x. b \<le> inner a x} = {x. inner a x < b}" by auto
-  thus ?thesis using closed_halfspace_ge[unfolded closed_def Compl_eq_Diff_UNIV, of b a] by auto
+  have "- {x. b \<le> inner a x} = {x. inner a x < b}" by auto
+  thus ?thesis using closed_halfspace_ge[unfolded closed_def, of b a] by auto
 qed
 
 lemma open_halfspace_gt: "open {x. inner a x > b}"
 proof-
-  have "UNIV - {x. b \<ge> inner a x} = {x. inner a x > b}" by auto
-  thus ?thesis using closed_halfspace_le[unfolded closed_def Compl_eq_Diff_UNIV, of a b] by auto
+  have "- {x. b \<ge> inner a x} = {x. inner a x > b}" by auto
+  thus ?thesis using closed_halfspace_le[unfolded closed_def, of a b] by auto
 qed
 
 lemma open_halfspace_component_lt:
diff -r c4628a1dcf75 -r 7aac4d74bb76 src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Thu Dec 17 15:22:11 2009 +0100
+++ b/src/Pure/Thy/completion.scala	Thu Dec 17 15:22:27 2009 +0100
@@ -116,13 +116,14 @@
     abbrevs_lex.parse(abbrevs_lex.keyword, new Completion.Reverse(line)) match {
       case abbrevs_lex.Success(rev_a, _) =>
         val (word, c) = abbrevs_map(rev_a)
-        Some(word, List(c))
+        if (word == c) None
+        else Some(word, List(c))
       case _ =>
         Completion.Parse.read(line) match {
           case Some(word) =>
-            words_lex.completions(word) match {
+            words_lex.completions(word).map(words_map(_)).filter(_ != word) match {
               case Nil => None
-              case cs => Some(word, cs.map(words_map(_)).sort(Completion.length_ord _))
+              case cs => Some (word, cs.sort(Completion.length_ord _))
             }
           case None => None
         }
diff -r c4628a1dcf75 -r 7aac4d74bb76 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Thu Dec 17 15:22:11 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Thu Dec 17 15:22:27 2009 +0100
@@ -409,7 +409,7 @@
 
         val len = length matches;
         val lim = the_default (! limit) opt_limit;
-      in (SOME len, drop (len - lim) matches) end;
+      in (SOME len, drop (Int.max (len - lim, 0)) matches) end;
 
     val find =
       if rem_dups orelse is_none opt_limit