--- 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
--- 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
--- 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)
--- 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
--- 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)"
--- 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:
--- 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
}
--- 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