--- a/Admin/isatest/isatest-makedist Wed Jun 17 08:21:27 2009 +0200
+++ b/Admin/isatest/isatest-makedist Wed Jun 17 08:31:13 2009 +0200
@@ -102,7 +102,7 @@
#sleep 15
$SSH macbroy22 "$MAKEALL $HOME/settings/at64-poly-5.1-para"
sleep 15
-$SSH macbroy23 "$MAKEALL $HOME/settings/at-sml-dev-e"
+$SSH macbroy23 -l HOL images "$MAKEALL $HOME/settings/at-sml-dev-e"
sleep 15
$SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly"
sleep 15
--- a/Admin/isatest/settings/mac-poly-M8 Wed Jun 17 08:21:27 2009 +0200
+++ b/Admin/isatest/settings/mac-poly-M8 Wed Jun 17 08:31:13 2009 +0200
@@ -4,7 +4,7 @@
ML_SYSTEM="polyml-experimental"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="--mutable 800 --immutable 2000"
+ ML_OPTIONS="--mutable 600 --immutable 1800"
ISABELLE_HOME_USER=~/isabelle-mac-poly-M8
--- a/src/HOL/Divides.thy Wed Jun 17 08:21:27 2009 +0200
+++ b/src/HOL/Divides.thy Wed Jun 17 08:31:13 2009 +0200
@@ -331,17 +331,22 @@
"(a * c) mod (b * c) = (a mod b) * c"
using mod_mult_mult1 [of c a b] by (simp add: mult_commute)
-end
+lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
+ unfolding dvd_def by (auto simp add: mod_mult_mult1)
+
+lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
+by (blast intro: dvd_mod_imp_dvd dvd_mod)
lemma div_power:
- "(y::'a::{semiring_div,no_zero_divisors,power}) dvd x \<Longrightarrow>
- (x div y) ^ n = x ^ n div y ^ n"
+ "y dvd x \<Longrightarrow> (x div y) ^ n = x ^ n div y ^ n"
apply (induct n)
apply simp
apply(simp add: div_mult_div_if_dvd dvd_power_same)
done
-class ring_div = semiring_div + comm_ring_1
+end
+
+class ring_div = semiring_div + idom
begin
text {* Negation respects modular equivalence. *}
@@ -905,15 +910,6 @@
apply (rule dvd_refl)
done
-lemma dvd_mod: "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n"
- unfolding dvd_def
- apply (case_tac "n = 0", auto)
- apply (blast intro: mod_mult_distrib2 [symmetric])
- done
-
-lemma dvd_mod_iff: "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)"
-by (blast intro: dvd_mod_imp_dvd dvd_mod)
-
lemma dvd_mult_cancel: "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n"
unfolding dvd_def
apply (erule exE)
--- a/src/HOL/IntDiv.thy Wed Jun 17 08:21:27 2009 +0200
+++ b/src/HOL/IntDiv.thy Wed Jun 17 08:31:13 2009 +0200
@@ -1059,13 +1059,10 @@
done
lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
- by (auto elim!: dvdE simp add: mod_mult_mult1)
+ by (rule dvd_mod) (* TODO: remove *)
lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)"
- apply (subgoal_tac "k dvd n * (m div n) + m mod n")
- apply (simp add: zmod_zdiv_equality [symmetric])
- apply (simp only: dvd_add dvd_mult2)
- done
+ by (rule dvd_mod_imp_dvd) (* TODO: remove *)
lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)"
apply (auto elim!: dvdE)
--- a/src/HOL/Library/Convex_Euclidean_Space.thy Wed Jun 17 08:21:27 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy Wed Jun 17 08:31:13 2009 +0200
@@ -46,7 +46,8 @@
"setsum (\<lambda>y. if (x = y) then P y else Q y) s = setsum Q s"
apply(rule_tac [!] setsum_cong2) using assms by auto
-lemma setsum_delta'': fixes s::"(real^'n) set" assumes "finite s"
+lemma setsum_delta'':
+ fixes s::"'a::real_vector set" assumes "finite s"
shows "(\<Sum>x\<in>s. (if y = x then f x else 0) *\<^sub>R x) = (if y\<in>s then (f y) *\<^sub>R y else 0)"
proof-
have *:"\<And>x y. (if y = x then f x else (0::real)) *\<^sub>R x = (if x=y then (f x) *\<^sub>R x else 0)" by auto
@@ -107,8 +108,8 @@
subsection {* Affine set and affine hull.*}
definition
- affine :: "(real ^ 'n::finite) set \<Rightarrow> bool" where
- "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v::real. u + v = 1 \<longrightarrow> (u *\<^sub>R x + v *\<^sub>R y) \<in> s)"
+ affine :: "'a::real_vector set \<Rightarrow> bool" where
+ "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
lemma affine_alt: "affine s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u::real. (1 - u) *\<^sub>R x + u *\<^sub>R y \<in> s)"
proof- have *:"\<And>u v ::real. u + v = 1 \<longleftrightarrow> v = 1 - u" by auto
@@ -149,7 +150,7 @@
subsection {* Some explicit formulations (from Lars Schewe). *}
-lemma affine: fixes V::"(real^'n::finite) set"
+lemma affine: fixes V::"'a::real_vector set"
shows "affine V \<longleftrightarrow> (\<forall>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> V \<and> setsum u s = 1 \<longrightarrow> (setsum (\<lambda>x. (u x) *\<^sub>R x)) s \<in> V)"
unfolding affine_def apply rule apply(rule, rule, rule) apply(erule conjE)+
defer apply(rule, rule, rule, rule, rule) proof-
@@ -169,7 +170,7 @@
thus ?thesis using as(1)[THEN bspec[where x=a], THEN bspec[where x=b]] using as(4,5)
by(auto simp add: setsum_clauses(2))
next assume "card s > 2" thus ?thesis using as and n_def proof(induct n arbitrary: u s)
- case (Suc n) fix s::"(real^'n) set" and u::"real^'n\<Rightarrow> real"
+ case (Suc n) fix s::"'a set" and u::"'a \<Rightarrow> real"
assume IA:"\<And>u s. \<lbrakk>2 < card s; \<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V; finite s;
s \<noteq> {}; s \<subseteq> V; setsum u s = 1; n \<equiv> card s \<rbrakk> \<Longrightarrow> (\<Sum>x\<in>s. u x *\<^sub>R x) \<in> V" and
as:"Suc n \<equiv> card s" "2 < card s" "\<forall>x\<in>V. \<forall>y\<in>V. \<forall>u v. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> V"
@@ -251,7 +252,8 @@
apply(rule hull_unique) unfolding mem_def by auto
lemma affine_hull_finite_step:
- shows "(\<exists>u::real^'n=>real. setsum u {} = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) {} = y) \<longleftrightarrow> w = 0 \<and> y = 0" (is ?th1)
+ fixes y :: "'a::real_vector"
+ shows "(\<exists>u. setsum u {} = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) {} = y) \<longleftrightarrow> w = 0 \<and> y = 0" (is ?th1)
"finite s \<Longrightarrow> (\<exists>u. setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y) \<longleftrightarrow>
(\<exists>v u. setsum u s = w - v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?as \<Longrightarrow> (?lhs = ?rhs)")
proof-
@@ -288,10 +290,12 @@
ultimately show "?lhs = ?rhs" by blast
qed
-lemma affine_hull_2:"affine hull {a,b::real^'n::finite} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs")
+lemma affine_hull_2:
+ fixes a b :: "'a::real_vector"
+ shows "affine hull {a,b} = {u *\<^sub>R a + v *\<^sub>R b| u v. (u + v = 1)}" (is "?lhs = ?rhs")
proof-
have *:"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)"
- "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real^'n)" by auto
+ "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
have "?lhs = {y. \<exists>u. setsum u {a, b} = 1 \<and> (\<Sum>v\<in>{a, b}. u v *\<^sub>R v) = y}"
using affine_hull_finite[of "{a,b}"] by auto
also have "\<dots> = {y. \<exists>v u. u b = 1 - v \<and> u b *\<^sub>R b = y - v *\<^sub>R a}"
@@ -300,10 +304,12 @@
finally show ?thesis by auto
qed
-lemma affine_hull_3: "affine hull {a,b,c::real^'n::finite} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" (is "?lhs = ?rhs")
+lemma affine_hull_3:
+ fixes a b c :: "'a::real_vector"
+ shows "affine hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c| u v w. u + v + w = 1}" (is "?lhs = ?rhs")
proof-
have *:"\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real)"
- "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::real^'n)" by auto
+ "\<And>x y z. z = x - y \<longleftrightarrow> y + z = (x::'a)" by auto
show ?thesis apply(simp add: affine_hull_finite affine_hull_finite_step)
unfolding * apply auto
apply(rule_tac x=v in exI) apply(rule_tac x=va in exI) apply auto
@@ -313,7 +319,8 @@
subsection {* Some relations between affine hull and subspaces. *}
lemma affine_hull_insert_subset_span:
- "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
+ fixes a :: "real ^ _"
+ shows "affine hull (insert a s) \<subseteq> {a + v| v . v \<in> span {x - a | x . x \<in> s}}"
unfolding subset_eq Ball_def unfolding affine_hull_explicit span_explicit mem_Collect_eq smult_conv_scaleR
apply(rule,rule) apply(erule exE)+ apply(erule conjE)+ proof-
fix x t u assume as:"finite t" "t \<noteq> {}" "t \<subseteq> insert a s" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = x"
@@ -330,6 +337,7 @@
unfolding as by simp qed
lemma affine_hull_insert_span:
+ fixes a :: "real ^ _"
assumes "a \<notin> s"
shows "affine hull (insert a s) =
{a + v | v . v \<in> span {x - a | x. x \<in> s}}"
@@ -349,14 +357,16 @@
by (auto simp add: setsum_subtractf scaleR_left.setsum algebra_simps) qed
lemma affine_hull_span:
+ fixes a :: "real ^ _"
assumes "a \<in> s"
shows "affine hull s = {a + v | v. v \<in> span {x - a | x. x \<in> s - {a}}}"
using affine_hull_insert_span[of a "s - {a}", unfolded insert_Diff[OF assms]] by auto
subsection {* Convexity. *}
-definition "convex (s::(real^'n::finite) set) \<longleftrightarrow>
- (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. (u + v = 1) \<longrightarrow> (u *\<^sub>R x + v *\<^sub>R y) \<in> s)"
+definition
+ convex :: "'a::real_vector set \<Rightarrow> bool" where
+ "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
lemma convex_alt: "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u. 0 \<le> u \<and> u \<le> 1 \<longrightarrow> ((1 - u) *\<^sub>R x + u *\<^sub>R y) \<in> s)"
proof- have *:"\<And>u v::real. u + v = 1 \<longleftrightarrow> u = 1 - v" by auto
@@ -445,7 +455,9 @@
thus ?thesis unfolding setsum_cl_ivl_Suc and *** and scaleR_right.setsum [symmetric] using nn by auto qed qed auto qed
-lemma convex_explicit: "convex (s::(real^'n::finite) set) \<longleftrightarrow>
+lemma convex_explicit:
+ fixes s :: "'a::real_vector set"
+ shows "convex s \<longleftrightarrow>
(\<forall>t u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> setsum (\<lambda>x. u x *\<^sub>R x) t \<in> s)"
unfolding convex_def apply(rule,rule,rule) apply(subst imp_conjL,rule) defer apply(rule,rule,rule,rule,rule,rule,rule) proof-
fix x y u v assume as:"\<forall>t u. finite t \<and> t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" "x \<in> s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = (1::real)"
@@ -453,7 +465,7 @@
case True show ?thesis unfolding True and scaleR_left_distrib[THEN sym] using as(3,6) by auto next
case False thus ?thesis using as(1)[THEN spec[where x="{x,y}"], THEN spec[where x="\<lambda>z. if z=x then u else v"]] and as(2-) by auto qed
next
- fix t u assume asm:"\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s" "finite (t::(real^'n) set)"
+ fix t u assume asm:"\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s" "finite (t::'a set)"
(*"finite t" "t \<subseteq> s" "\<forall>x\<in>t. (0::real) \<le> u x" "setsum u t = 1"*)
from this(2) have "\<forall>u. t \<subseteq> s \<and> (\<forall>x\<in>t. 0 \<le> u x) \<and> setsum u t = 1 \<longrightarrow> (\<Sum>x\<in>t. u x *\<^sub>R x) \<in> s" apply(induct_tac t rule:finite_induct)
prefer 3 apply (rule,rule) apply(erule conjE)+ proof-
@@ -493,7 +505,9 @@
subsection {* Cones. *}
-definition "cone (s::(real^'n) set) \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. (c *\<^sub>R x) \<in> s)"
+definition
+ cone :: "'a::real_vector set \<Rightarrow> bool" where
+ "cone s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>c\<ge>0. (c *\<^sub>R x) \<in> s)"
lemma cone_empty[intro, simp]: "cone {}"
unfolding cone_def by auto
@@ -517,7 +531,7 @@
subsection {* Affine dependence and consequential theorems (from Lars Schewe). *}
definition
- affine_dependent :: "(real ^ 'n::finite) set \<Rightarrow> bool" where
+ affine_dependent :: "'a::real_vector set \<Rightarrow> bool" where
"affine_dependent s \<longleftrightarrow> (\<exists>x\<in>s. x \<in> (affine hull (s - {x})))"
lemma affine_dependent_explicit:
@@ -537,21 +551,21 @@
have "s \<noteq> {v}" using as(3,6) by auto
thus "\<exists>x\<in>p. \<exists>s u. finite s \<and> s \<noteq> {} \<and> s \<subseteq> p - {x} \<and> setsum u s = 1 \<and> (\<Sum>v\<in>s. u v *\<^sub>R v) = x"
apply(rule_tac x=v in bexI, rule_tac x="s - {v}" in exI, rule_tac x="\<lambda>x. - (1 / u v) * u x" in exI)
- unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] unfolding setsum_right_distrib[THEN sym] and setsum_diff1_ring[OF as(1,5)] using as by auto
+ unfolding scaleR_scaleR[THEN sym] and scaleR_right.setsum [symmetric] unfolding setsum_right_distrib[THEN sym] and setsum_diff1[OF as(1)] using as by auto
qed
lemma affine_dependent_explicit_finite:
- assumes "finite (s::(real^'n::finite) set)"
+ fixes s :: "'a::real_vector set" assumes "finite s"
shows "affine_dependent s \<longleftrightarrow> (\<exists>u. setsum u s = 0 \<and> (\<exists>v\<in>s. u v \<noteq> 0) \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = 0)"
(is "?lhs = ?rhs")
proof
- have *:"\<And>vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else (0::real^'n))" by auto
+ have *:"\<And>vt u v. (if vt then u v else 0) *\<^sub>R v = (if vt then (u v) *\<^sub>R v else (0::'a))" by auto
assume ?lhs
then obtain t u v where "finite t" "t \<subseteq> s" "setsum u t = 0" "v\<in>t" "u v \<noteq> 0" "(\<Sum>v\<in>t. u v *\<^sub>R v) = 0"
unfolding affine_dependent_explicit by auto
thus ?rhs apply(rule_tac x="\<lambda>x. if x\<in>t then u x else 0" in exI)
apply auto unfolding * and setsum_restrict_set[OF assms, THEN sym]
- unfolding Int_absorb2[OF `t\<subseteq>s`, unfolded Int_commute] by auto
+ unfolding Int_absorb1[OF `t\<subseteq>s`] by auto
next
assume ?rhs
then obtain u v where "setsum u s = 0" "v\<in>s" "u v \<noteq> 0" "(\<Sum>v\<in>s. u v *\<^sub>R v) = 0" by auto
@@ -561,6 +575,7 @@
subsection {* A general lemma. *}
lemma convex_connected:
+ fixes s :: "'a::real_normed_vector set"
assumes "convex s" shows "connected s"
proof-
{ fix e1 e2 assume as:"open e1" "open e2" "e1 \<inter> e2 \<inter> s = {}" "s \<subseteq> e1 \<union> e2"
@@ -595,12 +610,14 @@
subsection {* One rather trivial consequence. *}
-lemma connected_UNIV: "connected (UNIV :: (real ^ _) set)"
+lemma connected_UNIV: "connected (UNIV :: 'a::real_normed_vector set)"
by(simp add: convex_connected convex_UNIV)
subsection {* Convex functions into the reals. *}
-definition "convex_on s (f::real^'n \<Rightarrow> real) =
+definition
+ convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool" where
+ "convex_on s f \<longleftrightarrow>
(\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y)"
lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f"
@@ -641,6 +658,7 @@
qed
lemma convex_local_global_minimum:
+ fixes s :: "'a::real_normed_vector set"
assumes "0<e" "convex_on s f" "ball x e \<subseteq> s" "\<forall>y\<in>ball x e. f x \<le> f y"
shows "\<forall>y\<in>s. f x \<le> f y"
proof(rule ccontr)
@@ -661,7 +679,9 @@
ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto
qed
-lemma convex_distance: "convex_on s (\<lambda>x. dist a x)"
+lemma convex_distance:
+ fixes s :: "'a::real_normed_vector set"
+ shows "convex_on s (\<lambda>x. dist a x)"
proof(auto simp add: convex_on_def dist_norm)
fix x y assume "x\<in>s" "y\<in>s"
fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1"
@@ -710,23 +730,28 @@
proof- have "{a + y |y. y \<in> s} = (\<lambda>x. a + x) ` s" by auto
thus ?thesis using convex_sums[OF convex_singleton[of a] assms] by auto qed
-lemma convex_affinity: assumes "convex (s::(real^'n::finite) set)" shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` s)"
+lemma convex_affinity: assumes "convex s" shows "convex ((\<lambda>x. a + c *\<^sub>R x) ` s)"
proof- have "(\<lambda>x. a + c *\<^sub>R x) ` s = op + a ` op *\<^sub>R c ` s" by auto
thus ?thesis using convex_translation[OF convex_scaling[OF assms], of a c] by auto qed
-lemma convex_linear_image: assumes c:"convex s" and l:"linear f" shows "convex(f ` s)"
+lemma convex_linear_image:
+ assumes c:"convex s" and l:"bounded_linear f"
+ shows "convex(f ` s)"
proof(auto simp add: convex_def)
+ interpret f: bounded_linear f by fact
fix x y assume xy:"x \<in> s" "y \<in> s"
fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
show "u *\<^sub>R f x + v *\<^sub>R f y \<in> f ` s" unfolding image_iff
apply(rule_tac x="u *\<^sub>R x + v *\<^sub>R y" in bexI)
- unfolding linear_add[OF l] linear_cmul[OF l, unfolded smult_conv_scaleR]
+ unfolding f.add f.scaleR
using c[unfolded convex_def] xy uv by auto
qed
subsection {* Balls, being convex, are connected. *}
-lemma convex_ball: "convex (ball x e)"
+lemma convex_ball:
+ fixes x :: "'a::real_normed_vector"
+ shows "convex (ball x e)"
proof(auto simp add: convex_def)
fix y z assume yz:"dist x y < e" "dist x z < e"
fix u v ::real assume uv:"0 \<le> u" "0 \<le> v" "u + v = 1"
@@ -735,7 +760,9 @@
thus "dist x (u *\<^sub>R y + v *\<^sub>R z) < e" using real_convex_bound_lt[OF yz uv] by auto
qed
-lemma convex_cball: "convex(cball x e)"
+lemma convex_cball:
+ fixes x :: "'a::real_normed_vector"
+ shows "convex(cball x e)"
proof(auto simp add: convex_def Ball_def mem_cball)
fix y z assume yz:"dist x y \<le> e" "dist x z \<le> e"
fix u v ::real assume uv:" 0 \<le> u" "0 \<le> v" "u + v = 1"
@@ -744,10 +771,14 @@
thus "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> e" using real_convex_bound_le[OF yz uv] by auto
qed
-lemma connected_ball: "connected(ball (x::real^_) e)" (* FIXME: generalize *)
+lemma connected_ball:
+ fixes x :: "'a::real_normed_vector"
+ shows "connected (ball x e)"
using convex_connected convex_ball by auto
-lemma connected_cball: "connected(cball (x::real^_) e)" (* FIXME: generalize *)
+lemma connected_cball:
+ fixes x :: "'a::real_normed_vector"
+ shows "connected(cball x e)"
using convex_connected convex_cball by auto
subsection {* Convex hull. *}
@@ -759,14 +790,17 @@
lemma convex_hull_eq: "(convex hull s = s) \<longleftrightarrow> convex s" apply(rule hull_eq[unfolded mem_def])
using convex_Inter[unfolded Ball_def mem_def] by auto
-lemma bounded_convex_hull: assumes "bounded s" shows "bounded(convex hull s)"
+lemma bounded_convex_hull:
+ fixes s :: "'a::real_normed_vector set"
+ assumes "bounded s" shows "bounded(convex hull s)"
proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_iff by auto
show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])
unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball]
unfolding subset_eq mem_cball dist_norm using B by auto qed
lemma finite_imp_bounded_convex_hull:
- "finite s \<Longrightarrow> bounded(convex hull s)"
+ fixes s :: "'a::real_normed_vector set"
+ shows "finite s \<Longrightarrow> bounded(convex hull s)"
using bounded_convex_hull finite_imp_bounded by auto
subsection {* Stepping theorems for convex hulls of finite sets. *}
@@ -778,6 +812,7 @@
apply(rule hull_unique) unfolding mem_def by auto
lemma convex_hull_insert:
+ fixes s :: "'a::real_vector set"
assumes "s \<noteq> {}"
shows "convex hull (insert a s) = {x. \<exists>u\<ge>0. \<exists>v\<ge>0. \<exists>b. (u + v = 1) \<and>
b \<in> (convex hull s) \<and> (x = u *\<^sub>R a + v *\<^sub>R b)}" (is "?xyz = ?hull")
@@ -797,10 +832,10 @@
fix x y u v assume as:"(0::real) \<le> u" "0 \<le> v" "u + v = 1" "x\<in>?hull" "y\<in>?hull"
from as(4) obtain u1 v1 b1 where obt1:"u1\<ge>0" "v1\<ge>0" "u1 + v1 = 1" "b1 \<in> convex hull s" "x = u1 *\<^sub>R a + v1 *\<^sub>R b1" by auto
from as(5) obtain u2 v2 b2 where obt2:"u2\<ge>0" "v2\<ge>0" "u2 + v2 = 1" "b2 \<in> convex hull s" "y = u2 *\<^sub>R a + v2 *\<^sub>R b2" by auto
- have *:"\<And>(x::real^_) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)
+ have *:"\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)
have "\<exists>b \<in> convex hull s. u *\<^sub>R x + v *\<^sub>R y = (u * u1) *\<^sub>R a + (v * u2) *\<^sub>R a + (b - (u * u1) *\<^sub>R b - (v * u2) *\<^sub>R b)"
proof(cases "u * v1 + v * v2 = 0")
- have *:"\<And>(x::real^_) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)
+ have *:"\<And>(x::'a) s1 s2. x - s1 *\<^sub>R x - s2 *\<^sub>R x = ((1::real) - (s1 + s2)) *\<^sub>R x" by (auto simp add: algebra_simps)
case True hence **:"u * v1 = 0" "v * v2 = 0" apply- apply(rule_tac [!] ccontr)
using mult_nonneg_nonneg[OF `u\<ge>0` `v1\<ge>0`] mult_nonneg_nonneg[OF `v\<ge>0` `v2\<ge>0`] by auto
hence "u * u1 + v * u2 = 1" using as(3) obt1(3) obt2(3) by auto
@@ -834,7 +869,8 @@
subsection {* Explicit expression for convex hull. *}
lemma convex_hull_indexed:
- "convex hull s = {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
+ fixes s :: "'a::real_vector set"
+ shows "convex hull s = {y. \<exists>k u x. (\<forall>i\<in>{1::nat .. k}. 0 \<le> u i \<and> x i \<in> s) \<and>
(setsum u {1..k} = 1) \<and>
(setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} = y)}" (is "?xyz = ?hull")
apply(rule hull_unique) unfolding mem_def[of _ convex] apply(rule) defer
@@ -852,7 +888,7 @@
fix x y u v assume uv:"0\<le>u" "0\<le>v" "u+v=(1::real)" and xy:"x\<in>?hull" "y\<in>?hull"
from xy obtain k1 u1 x1 where x:"\<forall>i\<in>{1::nat..k1}. 0\<le>u1 i \<and> x1 i \<in> s" "setsum u1 {Suc 0..k1} = 1" "(\<Sum>i = Suc 0..k1. u1 i *\<^sub>R x1 i) = x" by auto
from xy obtain k2 u2 x2 where y:"\<forall>i\<in>{1::nat..k2}. 0\<le>u2 i \<and> x2 i \<in> s" "setsum u2 {Suc 0..k2} = 1" "(\<Sum>i = Suc 0..k2. u2 i *\<^sub>R x2 i) = y" by auto
- have *:"\<And>P x1 x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)"
+ have *:"\<And>P (x1::'a) x2 s1 s2 i.(if P i then s1 else s2) *\<^sub>R (if P i then x1 else x2) = (if P i then s1 *\<^sub>R x1 else s2 *\<^sub>R x2)"
"{1..k1 + k2} \<inter> {1..k1} = {1..k1}" "{1..k1 + k2} \<inter> - {1..k1} = (\<lambda>i. i + k1) ` {1..k2}"
prefer 3 apply(rule,rule) unfolding image_iff apply(rule_tac x="x - k1" in bexI) by(auto simp add: not_le)
have inj:"inj_on (\<lambda>i. i + k1) {1..k2}" unfolding inj_on_def by auto
@@ -873,7 +909,8 @@
qed
lemma convex_hull_finite:
- assumes "finite (s::(real^'n::finite)set)"
+ fixes s :: "'a::real_vector set"
+ assumes "finite s"
shows "convex hull s = {y. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and>
setsum u s = 1 \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y}" (is "?HULL = ?set")
proof(rule hull_unique, auto simp add: mem_def[of _ convex] convex_def[of ?set])
@@ -902,8 +939,17 @@
subsection {* Another formulation from Lars Schewe. *}
+lemma setsum_constant_scaleR:
+ fixes y :: "'a::real_vector"
+ shows "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y"
+apply (cases "finite A")
+apply (induct set: finite)
+apply (simp_all add: algebra_simps)
+done
+
lemma convex_hull_explicit:
- "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and>
+ fixes p :: "'a::real_vector set"
+ shows "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and>
(\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}" (is "?lhs = ?rhs")
proof-
{ fix x assume "x\<in>?lhs"
@@ -940,7 +986,9 @@
then obtain i where "i\<in>{1..card s}" "f i = y" using f using image_iff[of y f "{1..card s}"] by auto
hence "{x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = {i}" apply auto using f(1)[unfolded inj_on_def] apply(erule_tac x=x in ballE) by auto
hence "card {x. Suc 0 \<le> x \<and> x \<le> card s \<and> f x = y} = 1" by auto
- hence "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y" "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y" by auto }
+ hence "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x)) = u y"
+ "(\<Sum>x\<in>{x \<in> {1..card s}. f x = y}. u (f x) *\<^sub>R f x) = u y *\<^sub>R y"
+ by (auto simp add: setsum_constant_scaleR) }
hence "(\<Sum>x = 1..card s. u (f x)) = 1" "(\<Sum>i = 1..card s. u (f i) *\<^sub>R f i) = y"
unfolding setsum_image_gen[OF *(1), of "\<lambda>x. u (f x) *\<^sub>R f x" f] and setsum_image_gen[OF *(1), of "\<lambda>x. u (f x)" f]
@@ -956,7 +1004,7 @@
subsection {* A stepping theorem for that expansion. *}
lemma convex_hull_finite_step:
- assumes "finite (s::(real^'n) set)"
+ fixes s :: "'a::real_vector set" assumes "finite s"
shows "(\<exists>u. (\<forall>x\<in>insert a s. 0 \<le> u x) \<and> setsum u (insert a s) = w \<and> setsum (\<lambda>x. u x *\<^sub>R x) (insert a s) = y)
\<longleftrightarrow> (\<exists>v\<ge>0. \<exists>u. (\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = w - v \<and> setsum (\<lambda>x. u x *\<^sub>R x) s = y - v *\<^sub>R a)" (is "?lhs = ?rhs")
proof(rule, case_tac[!] "a\<in>s")
@@ -995,7 +1043,7 @@
unfolding * apply auto apply(rule_tac[!] x=u in exI) by (auto simp add: algebra_simps) qed
lemma convex_hull_3:
- "convex hull {a::real^'n::finite,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c | u v w. 0 \<le> u \<and> 0 \<le> v \<and> 0 \<le> w \<and> u + v + w = 1}"
+ "convex hull {a,b,c} = { u *\<^sub>R a + v *\<^sub>R b + w *\<^sub>R c | u v w. 0 \<le> u \<and> 0 \<le> v \<and> 0 \<le> w \<and> u + v + w = 1}"
proof-
have fin:"finite {a,b,c}" "finite {b,c}" "finite {c}" by auto
have *:"\<And>x y z ::real. x + y + z = 1 \<longleftrightarrow> x = 1 - y - z"
@@ -1013,20 +1061,27 @@
subsection {* Relations among closure notions and corresponding hulls. *}
-lemma subspace_imp_affine: "subspace s \<Longrightarrow> affine s"
+text {* TODO: Generalize linear algebra concepts defined in @{text
+Euclidean_Space.thy} so that we can generalize these lemmas. *}
+
+lemma subspace_imp_affine:
+ fixes s :: "(real ^ _) set" shows "subspace s \<Longrightarrow> affine s"
unfolding subspace_def affine_def smult_conv_scaleR by auto
lemma affine_imp_convex: "affine s \<Longrightarrow> convex s"
unfolding affine_def convex_def by auto
-lemma subspace_imp_convex: "subspace s \<Longrightarrow> convex s"
+lemma subspace_imp_convex:
+ fixes s :: "(real ^ _) set" shows "subspace s \<Longrightarrow> convex s"
using subspace_imp_affine affine_imp_convex by auto
-lemma affine_hull_subset_span: "(affine hull s) \<subseteq> (span s)"
+lemma affine_hull_subset_span:
+ fixes s :: "(real ^ _) set" shows "(affine hull s) \<subseteq> (span s)"
unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def
using subspace_imp_affine by auto
-lemma convex_hull_subset_span: "(convex hull s) \<subseteq> (span s)"
+lemma convex_hull_subset_span:
+ fixes s :: "(real ^ _) set" shows "(convex hull s) \<subseteq> (span s)"
unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def
using subspace_imp_convex by auto
@@ -1034,11 +1089,13 @@
unfolding span_def apply(rule hull_antimono) unfolding subset_eq Ball_def mem_def
using affine_imp_convex by auto
-lemma affine_dependent_imp_dependent: "affine_dependent s \<Longrightarrow> dependent s"
+lemma affine_dependent_imp_dependent:
+ fixes s :: "(real ^ _) set" shows "affine_dependent s \<Longrightarrow> dependent s"
unfolding affine_dependent_def dependent_def
using affine_hull_subset_span by auto
lemma dependent_imp_affine_dependent:
+ fixes s :: "(real ^ _) set"
assumes "dependent {x - a| x . x \<in> s}" "a \<notin> s"
shows "affine_dependent (insert a s)"
proof-
@@ -1188,6 +1245,7 @@
subsection {* Openness and compactness are preserved by convex hull operation. *}
lemma open_convex_hull:
+ fixes s :: "'a::real_normed_vector set"
assumes "open s"
shows "open(convex hull s)"
unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(10)
@@ -1255,7 +1313,7 @@
qed
lemma compact_convex_combinations:
- fixes s t :: "(real ^ 'n::finite) set"
+ fixes s t :: "'a::real_normed_vector set"
assumes "compact s" "compact t"
shows "compact { (1 - u) *\<^sub>R x + u *\<^sub>R y | x y u. 0 \<le> u \<and> u \<le> 1 \<and> x \<in> s \<and> y \<in> t}"
proof-
@@ -1351,13 +1409,14 @@
qed
lemma finite_imp_compact_convex_hull:
- "finite s \<Longrightarrow> compact(convex hull s)"
+ fixes s :: "(real ^ _) set"
+ shows "finite s \<Longrightarrow> compact(convex hull s)"
apply(drule finite_imp_compact, drule compact_convex_hull) by assumption
subsection {* Extremal points of a simplex are some vertices. *}
lemma dist_increases_online:
- fixes a b d :: "real ^ 'n::finite"
+ fixes a b d :: "'a::real_inner"
assumes "d \<noteq> 0"
shows "dist a (b + d) > dist a b \<or> dist a (b - d) > dist a b"
proof(cases "inner a d - inner b d > 0")
@@ -1373,11 +1432,12 @@
qed
lemma norm_increases_online:
- "(d::real^'n::finite) \<noteq> 0 \<Longrightarrow> norm(a + d) > norm a \<or> norm(a - d) > norm a"
+ fixes d :: "'a::real_inner"
+ shows "d \<noteq> 0 \<Longrightarrow> norm(a + d) > norm a \<or> norm(a - d) > norm a"
using dist_increases_online[of d a 0] unfolding dist_norm by auto
lemma simplex_furthest_lt:
- fixes s::"(real^'n::finite) set" assumes "finite s"
+ fixes s::"'a::real_inner set" assumes "finite s"
shows "\<forall>x \<in> (convex hull s). x \<notin> s \<longrightarrow> (\<exists>y\<in>(convex hull s). norm(x - a) < norm(y - a))"
proof(induct_tac rule: finite_induct[of s])
fix x s assume as:"finite s" "x\<notin>s" "\<forall>x\<in>convex hull s. x \<notin> s \<longrightarrow> (\<exists>y\<in>convex hull s. norm (x - a) < norm (y - a))"
@@ -1432,6 +1492,7 @@
qed (auto simp add: assms)
lemma simplex_furthest_le:
+ fixes s :: "(real ^ _) set"
assumes "finite s" "s \<noteq> {}"
shows "\<exists>y\<in>s. \<forall>x\<in>(convex hull s). norm(x - a) \<le> norm(y - a)"
proof-
@@ -1447,10 +1508,12 @@
qed
lemma simplex_furthest_le_exists:
- "finite s \<Longrightarrow> (\<forall>x\<in>(convex hull s). \<exists>y\<in>s. norm(x - a) \<le> norm(y - a))"
+ fixes s :: "(real ^ _) set"
+ shows "finite s \<Longrightarrow> (\<forall>x\<in>(convex hull s). \<exists>y\<in>s. norm(x - a) \<le> norm(y - a))"
using simplex_furthest_le[of s] by (cases "s={}")auto
lemma simplex_extremal_le:
+ fixes s :: "(real ^ _) set"
assumes "finite s" "s \<noteq> {}"
shows "\<exists>u\<in>s. \<exists>v\<in>s. \<forall>x\<in>convex hull s. \<forall>y \<in> convex hull s. norm(x - y) \<le> norm(u - v)"
proof-
@@ -1471,7 +1534,8 @@
qed
lemma simplex_extremal_le_exists:
- "finite s \<Longrightarrow> x \<in> convex hull s \<Longrightarrow> y \<in> convex hull s
+ fixes s :: "(real ^ _) set"
+ shows "finite s \<Longrightarrow> x \<in> convex hull s \<Longrightarrow> y \<in> convex hull s
\<Longrightarrow> (\<exists>u\<in>s. \<exists>v\<in>s. norm(x - y) \<le> norm(u - v))"
using convex_hull_empty simplex_extremal_le[of s] by(cases "s={}")auto
@@ -1532,6 +1596,7 @@
unfolding dist_norm by(auto simp add: norm_minus_commute field_simps) qed
lemma any_closest_point_dot:
+ fixes s :: "(real ^ _) set"
assumes "convex s" "closed s" "x \<in> s" "y \<in> s" "\<forall>z\<in>s. dist a x \<le> dist a z"
shows "inner (a - x) (y - x) \<le> 0"
proof(rule ccontr) assume "\<not> inner (a - x) (y - x) \<le> 0"
@@ -1552,6 +1617,7 @@
qed
lemma any_closest_point_unique:
+ fixes s :: "(real ^ _) set"
assumes "convex s" "closed s" "x \<in> s" "y \<in> s"
"\<forall>z\<in>s. dist a x \<le> dist a z" "\<forall>z\<in>s. dist a y \<le> dist a z"
shows "x = y" using any_closest_point_dot[OF assms(1-4,5)] and any_closest_point_dot[OF assms(1-2,4,3,6)]
@@ -1603,6 +1669,7 @@
subsection {* Various point-to-set separating/supporting hyperplane theorems. *}
lemma supporting_hyperplane_closed_point:
+ fixes s :: "(real ^ _) set"
assumes "convex s" "closed s" "s \<noteq> {}" "z \<notin> s"
shows "\<exists>a b. \<exists>y\<in>s. inner a z < b \<and> (inner a y = b) \<and> (\<forall>x\<in>s. inner a x \<ge> b)"
proof-
@@ -1621,6 +1688,7 @@
qed
lemma separating_hyperplane_closed_point:
+ fixes s :: "(real ^ _) set"
assumes "convex s" "closed s" "z \<notin> s"
shows "\<exists>a b. inner a z < b \<and> (\<forall>x\<in>s. inner a x > b)"
proof(cases "s={}")
@@ -1691,6 +1759,7 @@
qed
lemma separating_hyperplane_compact_closed:
+ fixes s :: "(real ^ _) set"
assumes "convex s" "compact s" "s \<noteq> {}" "convex t" "closed t" "s \<inter> t = {}"
shows "\<exists>a b. (\<forall>x\<in>s. inner a x < b) \<and> (\<forall>x\<in>t. inner a x > b)"
proof- obtain a b where "(\<forall>x\<in>t. inner a x < b) \<and> (\<forall>x\<in>s. b < inner a x)"
@@ -1733,14 +1802,18 @@
subsection {* More convexity generalities. *}
-lemma convex_closure: assumes "convex s" shows "convex(closure s)"
+lemma convex_closure:
+ fixes s :: "'a::real_normed_vector set"
+ assumes "convex s" shows "convex(closure s)"
unfolding convex_def Ball_def closure_sequential
apply(rule,rule,rule,rule,rule,rule,rule,rule,rule) apply(erule_tac exE)+
apply(rule_tac x="\<lambda>n. u *\<^sub>R xb n + v *\<^sub>R xc n" in exI) apply(rule,rule)
apply(rule assms[unfolded convex_def, rule_format]) prefer 6
apply(rule Lim_add) apply(rule_tac [1-2] Lim_cmul) by auto
-lemma convex_interior: assumes "convex s" shows "convex(interior s)"
+lemma convex_interior:
+ fixes s :: "'a::real_normed_vector set"
+ assumes "convex s" shows "convex(interior s)"
unfolding convex_alt Ball_def mem_interior apply(rule,rule,rule,rule,rule,rule) apply(erule exE | erule conjE)+ proof-
fix x y u assume u:"0 \<le> u" "u \<le> (1::real)"
fix e d assume ed:"ball x e \<subseteq> s" "ball y d \<subseteq> s" "0<d" "0<e"
@@ -1789,6 +1862,7 @@
subsection {* Convex set as intersection of halfspaces. *}
lemma convex_halfspace_intersection:
+ fixes s :: "(real ^ _) set"
assumes "closed s" "convex s"
shows "s = \<Inter> {h. s \<subseteq> h \<and> (\<exists>a b. h = {x. inner a x \<le> b})}"
apply(rule set_ext, rule) unfolding Inter_iff Ball_def mem_Collect_eq apply(rule,rule,erule conjE) proof-
@@ -1915,20 +1989,23 @@
subsection {* Convex hull is "preserved" by a linear function. *}
lemma convex_hull_linear_image:
- assumes "linear f"
+ assumes "bounded_linear f"
shows "f ` (convex hull s) = convex hull (f ` s)"
apply rule unfolding subset_eq ball_simps apply(rule_tac[!] hull_induct, rule hull_inc) prefer 3
apply(erule imageE)apply(rule_tac x=xa in image_eqI) apply assumption
apply(rule hull_subset[unfolded subset_eq, rule_format]) apply assumption
-proof- show "convex {x. f x \<in> convex hull f ` s}"
- unfolding convex_def by(auto simp add: linear_cmul[OF assms, unfolded smult_conv_scaleR] linear_add[OF assms]
- convex_convex_hull[unfolded convex_def, rule_format]) next
+proof-
+ interpret f: bounded_linear f by fact
+ show "convex {x. f x \<in> convex hull f ` s}"
+ unfolding convex_def by(auto simp add: f.scaleR f.add convex_convex_hull[unfolded convex_def, rule_format]) next
+ interpret f: bounded_linear f by fact
show "convex {x. x \<in> f ` (convex hull s)}" using convex_convex_hull[unfolded convex_def, of s]
- unfolding convex_def by (auto simp add: linear_cmul[OF assms, THEN sym, unfolded smult_conv_scaleR] linear_add[OF assms, THEN sym])
+ unfolding convex_def by (auto simp add: f.scaleR [symmetric] f.add [symmetric])
qed auto
lemma in_convex_hull_linear_image:
- assumes "linear f" "x \<in> convex hull s" shows "(f x) \<in> convex hull (f ` s)"
+ assumes "bounded_linear f" "x \<in> convex hull s"
+ shows "(f x) \<in> convex hull (f ` s)"
using convex_hull_linear_image[OF assms(1)] assms(2) by auto
subsection {* Homeomorphism of all convex compact sets with nonempty interior. *}
@@ -2188,6 +2265,7 @@
apply(erule_tac x="dest_vec1 v" in allE) unfolding o_def vec1_dest_vec1 by auto
lemma convex_on:
+ fixes s :: "(real ^ _) set"
assumes "convex s"
shows "convex_on s f \<longleftrightarrow> (\<forall>k u x. (\<forall>i\<in>{1..k::nat}. 0 \<le> u i \<and> x i \<in> s) \<and> setsum u {1..k} = 1 \<longrightarrow>
f (setsum (\<lambda>i. u i *\<^sub>R x i) {1..k} ) \<le> setsum (\<lambda>i. u i * f(x i)) {1..k} ) "
@@ -2203,7 +2281,9 @@
subsection {* Convexity of general and special intervals. *}
-lemma is_interval_convex: assumes "is_interval s" shows "convex s"
+lemma is_interval_convex:
+ fixes s :: "(real ^ _) set"
+ assumes "is_interval s" shows "convex s"
unfolding convex_def apply(rule,rule,rule,rule,rule,rule,rule) proof-
fix x y u v assume as:"x \<in> s" "y \<in> s" "0 \<le> u" "0 \<le> v" "u + v = (1::real)"
hence *:"u = 1 - v" "1 - v \<ge> 0" and **:"v = 1 - u" "1 - u \<ge> 0" by auto
@@ -2288,6 +2368,7 @@
subsection {* A bound within a convex hull, and so an interval. *}
lemma convex_on_convex_hull_bound:
+ fixes s :: "(real ^ _) set"
assumes "convex_on (convex hull s) f" "\<forall>x\<in>s. f x \<le> b"
shows "\<forall>x\<in> convex hull s. f x \<le> b" proof
fix x assume "x\<in>convex hull s"
@@ -2390,6 +2471,7 @@
subsection {* Bounded convex function on open set is continuous. *}
lemma convex_on_bounded_continuous:
+ fixes s :: "(real ^ _) set"
assumes "open s" "convex_on s f" "\<forall>x\<in>s. abs(f x) \<le> b"
shows "continuous_on s f"
apply(rule continuous_at_imp_continuous_on) unfolding continuous_at_real_range proof(rule,rule,rule)
@@ -2440,6 +2522,7 @@
subsection {* Upper bound on a ball implies upper and lower bounds. *}
lemma convex_bounds_lemma:
+ fixes x :: "real ^ _"
assumes "convex_on (cball x e) f" "\<forall>y \<in> cball x e. f y \<le> b"
shows "\<forall>y \<in> cball x e. abs(f y) \<le> b + 2 * abs(f x)"
apply(rule) proof(cases "0 \<le> e") case True
@@ -2619,6 +2702,7 @@
subsection {* Shrinking towards the interior of a convex set. *}
lemma mem_interior_convex_shrink:
+ fixes s :: "(real ^ _) set"
assumes "convex s" "c \<in> interior s" "x \<in> s" "0 < e" "e \<le> 1"
shows "x - e *\<^sub>R (x - c) \<in> interior s"
proof- obtain d where "d>0" and d:"ball c d \<subseteq> s" using assms(2) unfolding mem_interior by auto
@@ -2637,6 +2721,7 @@
qed(rule mult_pos_pos, insert `e>0` `d>0`, auto) qed
lemma mem_interior_closure_convex_shrink:
+ fixes s :: "(real ^ _) set"
assumes "convex s" "c \<in> interior s" "x \<in> closure s" "0 < e" "e \<le> 1"
shows "x - e *\<^sub>R (x - c) \<in> interior s"
proof- obtain d where "d>0" and d:"ball c d \<subseteq> s" using assms(2) unfolding mem_interior by auto
--- a/src/HOL/Library/Euclidean_Space.thy Wed Jun 17 08:21:27 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy Wed Jun 17 08:31:13 2009 +0200
@@ -889,7 +889,7 @@
subsection {* A connectedness or intermediate value lemma with several applications. *}
lemma connected_real_lemma:
- fixes f :: "real \<Rightarrow> real ^ 'n::finite"
+ fixes f :: "real \<Rightarrow> 'a::metric_space"
assumes ab: "a \<le> b" and fa: "f a \<in> e1" and fb: "f b \<in> e2"
and dst: "\<And>e x. a <= x \<Longrightarrow> x <= b \<Longrightarrow> 0 < e ==> \<exists>d > 0. \<forall>y. abs(y - x) < d \<longrightarrow> dist(f y) (f x) < e"
and e1: "\<forall>y \<in> e1. \<exists>e > 0. \<forall>y'. dist y' y < e \<longrightarrow> y' \<in> e1"
--- a/src/HOL/Library/Polynomial.thy Wed Jun 17 08:21:27 2009 +0200
+++ b/src/HOL/Library/Polynomial.thy Wed Jun 17 08:31:13 2009 +0200
@@ -632,6 +632,25 @@
shows "a \<noteq> 0 \<Longrightarrow> p dvd smult a q \<longleftrightarrow> p dvd q"
by (safe elim!: dvd_smult dvd_smult_cancel)
+lemma smult_dvd_cancel:
+ "smult a p dvd q \<Longrightarrow> p dvd q"
+proof -
+ assume "smult a p dvd q"
+ then obtain k where "q = smult a p * k" ..
+ then have "q = p * smult a k" by simp
+ then show "p dvd q" ..
+qed
+
+lemma smult_dvd:
+ fixes a :: "'a::field"
+ shows "p dvd q \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> smult a p dvd q"
+ by (rule smult_dvd_cancel [where a="inverse a"]) simp
+
+lemma smult_dvd_iff:
+ fixes a :: "'a::field"
+ shows "smult a p dvd q \<longleftrightarrow> (if a = 0 then q = 0 else p dvd q)"
+ by (auto elim: smult_dvd smult_dvd_cancel)
+
lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
by (induct n, simp, auto intro: order_trans degree_mult_le)
@@ -1102,6 +1121,109 @@
done
+subsection {* GCD of polynomials *}
+
+function
+ poly_gcd :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
+ "poly_gcd x 0 = smult (inverse (coeff x (degree x))) x"
+| "y \<noteq> 0 \<Longrightarrow> poly_gcd x y = poly_gcd y (x mod y)"
+by auto
+
+termination poly_gcd
+by (relation "measure (\<lambda>(x, y). if y = 0 then 0 else Suc (degree y))")
+ (auto dest: degree_mod_less)
+
+declare poly_gcd.simps [simp del, code del]
+
+lemma poly_gcd_dvd1 [iff]: "poly_gcd x y dvd x"
+ and poly_gcd_dvd2 [iff]: "poly_gcd x y dvd y"
+ apply (induct x y rule: poly_gcd.induct)
+ apply (simp_all add: poly_gcd.simps)
+ apply (fastsimp simp add: smult_dvd_iff dest: inverse_zero_imp_zero)
+ apply (blast dest: dvd_mod_imp_dvd)
+ done
+
+lemma poly_gcd_greatest: "k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd poly_gcd x y"
+ by (induct x y rule: poly_gcd.induct)
+ (simp_all add: poly_gcd.simps dvd_mod dvd_smult)
+
+lemma dvd_poly_gcd_iff [iff]:
+ "k dvd poly_gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y"
+ by (blast intro!: poly_gcd_greatest intro: dvd_trans)
+
+lemma poly_gcd_monic:
+ "coeff (poly_gcd x y) (degree (poly_gcd x y)) =
+ (if x = 0 \<and> y = 0 then 0 else 1)"
+ by (induct x y rule: poly_gcd.induct)
+ (simp_all add: poly_gcd.simps nonzero_imp_inverse_nonzero)
+
+lemma poly_gcd_zero_iff [simp]:
+ "poly_gcd x y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
+ by (simp only: dvd_0_left_iff [symmetric] dvd_poly_gcd_iff)
+
+lemma poly_gcd_0_0 [simp]: "poly_gcd 0 0 = 0"
+ by simp
+
+lemma poly_dvd_antisym:
+ fixes p q :: "'a::idom poly"
+ assumes coeff: "coeff p (degree p) = coeff q (degree q)"
+ assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q"
+proof (cases "p = 0")
+ case True with coeff show "p = q" by simp
+next
+ case False with coeff have "q \<noteq> 0" by auto
+ have degree: "degree p = degree q"
+ using `p dvd q` `q dvd p` `p \<noteq> 0` `q \<noteq> 0`
+ by (intro order_antisym dvd_imp_degree_le)
+
+ from `p dvd q` obtain a where a: "q = p * a" ..
+ with `q \<noteq> 0` have "a \<noteq> 0" by auto
+ with degree a `p \<noteq> 0` have "degree a = 0"
+ by (simp add: degree_mult_eq)
+ with coeff a show "p = q"
+ by (cases a, auto split: if_splits)
+qed
+
+lemma poly_gcd_unique:
+ assumes dvd1: "d dvd x" and dvd2: "d dvd y"
+ and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d"
+ and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)"
+ shows "poly_gcd x y = d"
+proof -
+ have "coeff (poly_gcd x y) (degree (poly_gcd x y)) = coeff d (degree d)"
+ by (simp_all add: poly_gcd_monic monic)
+ moreover have "poly_gcd x y dvd d"
+ using poly_gcd_dvd1 poly_gcd_dvd2 by (rule greatest)
+ moreover have "d dvd poly_gcd x y"
+ using dvd1 dvd2 by (rule poly_gcd_greatest)
+ ultimately show ?thesis
+ by (rule poly_dvd_antisym)
+qed
+
+lemma poly_gcd_commute: "poly_gcd x y = poly_gcd y x"
+by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
+
+lemma poly_gcd_assoc: "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
+by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
+
+lemmas poly_gcd_left_commute =
+ mk_left_commute [where f=poly_gcd, OF poly_gcd_assoc poly_gcd_commute]
+
+lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute
+
+lemma poly_gcd_1_left [simp]: "poly_gcd 1 y = 1"
+by (rule poly_gcd_unique) simp_all
+
+lemma poly_gcd_1_right [simp]: "poly_gcd x 1 = 1"
+by (rule poly_gcd_unique) simp_all
+
+lemma poly_gcd_minus_left [simp]: "poly_gcd (- x) y = poly_gcd x y"
+by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
+
+lemma poly_gcd_minus_right [simp]: "poly_gcd x (- y) = poly_gcd x y"
+by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
+
+
subsection {* Evaluation of polynomials *}
definition
@@ -1472,4 +1594,10 @@
apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl])
done
+lemma poly_gcd_code [code]:
+ "poly_gcd x y =
+ (if y = 0 then smult (inverse (coeff x (degree x))) x
+ else poly_gcd y (x mod y))"
+ by (simp add: poly_gcd.simps)
+
end
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Wed Jun 17 08:21:27 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Wed Jun 17 08:31:13 2009 +0200
@@ -1102,7 +1102,7 @@
text{* Notation Lim to avoid collition with lim defined in analysis *}
definition
- Lim :: "'a net \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> 'b" where
+ Lim :: "'a net \<Rightarrow> ('a \<Rightarrow> 'b::t2_space) \<Rightarrow> 'b" where
"Lim net f = (THE l. (f ---> l) net)"
lemma Lim:
@@ -1238,11 +1238,10 @@
text{* Basic arithmetical combining theorems for limits. *}
-lemma Lim_linear: fixes f :: "('a \<Rightarrow> real^'n::finite)" and h :: "(real^'n \<Rightarrow> real^'m::finite)"
- assumes "(f ---> l) net" "linear h"
+lemma Lim_linear:
+ assumes "(f ---> l) net" "bounded_linear h"
shows "((\<lambda>x. h (f x)) ---> h l) net"
-using `linear h` `(f ---> l) net`
-unfolding linear_conv_bounded_linear
+using `bounded_linear h` `(f ---> l) net`
by (rule bounded_linear.tendsto)
lemma Lim_ident_at: "((\<lambda>x. x) ---> a) (at a)"
@@ -1252,7 +1251,7 @@
by (rule tendsto_const)
lemma Lim_cmul:
- fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
shows "(f ---> l) net ==> ((\<lambda>x. c *\<^sub>R f x) ---> c *\<^sub>R l) net"
by (intro tendsto_intros)
@@ -1402,47 +1401,41 @@
text{* Uniqueness of the limit, when nontrivial. *}
lemma Lim_unique:
- fixes f :: "'a \<Rightarrow> 'b::metric_space"
+ fixes f :: "'a \<Rightarrow> 'b::t2_space"
assumes "\<not> trivial_limit net" "(f ---> l) net" "(f ---> l') net"
shows "l = l'"
proof (rule ccontr)
- let ?d = "dist l l' / 2"
assume "l \<noteq> l'"
- then have "0 < ?d" by (simp add: dist_nz)
- have "eventually (\<lambda>x. dist (f x) l < ?d) net"
- using `(f ---> l) net` `0 < ?d` by (rule tendstoD)
+ obtain U V where "open U" "open V" "l \<in> U" "l' \<in> V" "U \<inter> V = {}"
+ using hausdorff [OF `l \<noteq> l'`] by fast
+ have "eventually (\<lambda>x. f x \<in> U) net"
+ using `(f ---> l) net` `open U` `l \<in> U` by (rule topological_tendstoD)
moreover
- have "eventually (\<lambda>x. dist (f x) l' < ?d) net"
- using `(f ---> l') net` `0 < ?d` by (rule tendstoD)
+ have "eventually (\<lambda>x. f x \<in> V) net"
+ using `(f ---> l') net` `open V` `l' \<in> V` by (rule topological_tendstoD)
ultimately
have "eventually (\<lambda>x. False) net"
proof (rule eventually_elim2)
fix x
- assume *: "dist (f x) l < ?d" "dist (f x) l' < ?d"
- have "dist l l' \<le> dist (f x) l + dist (f x) l'"
- by (rule dist_triangle_alt)
- also from * have "\<dots> < ?d + ?d"
- by (rule add_strict_mono)
- also have "\<dots> = dist l l'" by simp
- finally show "False" by simp
+ assume "f x \<in> U" "f x \<in> V"
+ hence "f x \<in> U \<inter> V" by simp
+ with `U \<inter> V = {}` show "False" by simp
qed
with `\<not> trivial_limit net` show "False"
by (simp add: eventually_False)
qed
lemma tendsto_Lim:
- fixes f :: "'a \<Rightarrow> 'b::metric_space"
+ fixes f :: "'a \<Rightarrow> 'b::t2_space"
shows "~(trivial_limit net) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
unfolding Lim_def using Lim_unique[of net f] by auto
text{* Limit under bilinear function *}
lemma Lim_bilinear:
- fixes net :: "'a net" and h:: "real ^'m::finite \<Rightarrow> real ^'n::finite \<Rightarrow> real ^'p::finite"
- assumes "(f ---> l) net" and "(g ---> m) net" and "bilinear h"
+ assumes "(f ---> l) net" and "(g ---> m) net" and "bounded_bilinear h"
shows "((\<lambda>x. h (f x) (g x)) ---> (h l m)) net"
-using `bilinear h` `(f ---> l) net` `(g ---> m) net`
-unfolding bilinear_conv_bounded_bilinear
+using `bounded_bilinear h` `(f ---> l) net` `(g ---> m) net`
by (rule bounded_bilinear.tendsto)
text{* These are special for limits out of the same vector space. *}
@@ -1496,29 +1489,19 @@
text{* It's also sometimes useful to extract the limit point from the net. *}
definition
- netlimit :: "'a::metric_space net \<Rightarrow> 'a" where
- "netlimit net = (SOME a. \<forall>r>0. eventually (\<lambda>x. dist x a < r) net)"
+ netlimit :: "'a::t2_space net \<Rightarrow> 'a" where
+ "netlimit net = (SOME a. ((\<lambda>x. x) ---> a) net)"
lemma netlimit_within:
assumes "\<not> trivial_limit (at a within S)"
shows "netlimit (at a within S) = a"
-using assms
-apply (simp add: trivial_limit_within)
-apply (simp add: netlimit_def eventually_within zero_less_dist_iff)
-apply (rule some_equality, fast)
-apply (rename_tac b)
-apply (rule ccontr)
-apply (drule_tac x="dist b a / 2" in spec, drule mp, simp add: dist_nz)
-apply (clarify, rename_tac r)
-apply (simp only: islimpt_approachable)
-apply (drule_tac x="min r (dist b a / 2)" in spec, drule mp, simp add: dist_nz)
-apply (clarify)
-apply (drule_tac x=x' in bspec, simp)
-apply (drule mp, simp)
-apply (subgoal_tac "dist b a < dist b a / 2 + dist b a / 2", simp)
-apply (rule le_less_trans [OF dist_triangle3])
-apply (erule add_strict_mono)
-apply simp
+unfolding netlimit_def
+apply (rule some_equality)
+apply (rule Lim_at_within)
+apply (rule Lim_ident_at)
+apply (erule Lim_unique [OF assms])
+apply (rule Lim_at_within)
+apply (rule Lim_ident_at)
done
lemma netlimit_at:
@@ -2078,12 +2061,11 @@
qed
lemma bounded_linear_image:
- fixes f :: "real^'m::finite \<Rightarrow> real^'n::finite"
- assumes "bounded S" "linear f"
+ assumes "bounded S" "bounded_linear f"
shows "bounded(f ` S)"
proof-
from assms(1) obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b" unfolding bounded_pos by auto
- from assms(2) obtain B where B:"B>0" "\<forall>x. norm (f x) \<le> B * norm x" using linear_bounded_pos by auto
+ from assms(2) obtain B where B:"B>0" "\<forall>x. norm (f x) \<le> B * norm x" using bounded_linear.pos_bounded by (auto simp add: mult_ac)
{ fix x assume "x\<in>S"
hence "norm x \<le> b" using b by auto
hence "norm (f x) \<le> B * b" using B(2) apply(erule_tac x=x in allE)
@@ -2094,10 +2076,9 @@
qed
lemma bounded_scaling:
- fixes S :: "(real ^ 'n::finite) set"
+ fixes S :: "'a::real_normed_vector set"
shows "bounded S \<Longrightarrow> bounded ((\<lambda>x. c *\<^sub>R x) ` S)"
apply (rule bounded_linear_image, assumption)
- apply (simp only: linear_conv_bounded_linear)
apply (rule scaleR.bounded_linear_right)
done
@@ -3148,17 +3129,16 @@
subsection{* Define continuity over a net to take in restrictions of the set. *}
definition
- continuous :: "'a::metric_space net \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> bool" where
+ continuous :: "'a::t2_space net \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
"continuous net f \<longleftrightarrow> (f ---> f(netlimit net)) net"
- (* FIXME: generalize 'b to topological_space *)
lemma continuous_trivial_limit:
"trivial_limit net ==> continuous net f"
- unfolding continuous_def tendsto_iff trivial_limit_eq by auto
+ unfolding continuous_def tendsto_def trivial_limit_eq by auto
lemma continuous_within: "continuous (at x within s) f \<longleftrightarrow> (f ---> f(x)) (at x within s)"
unfolding continuous_def
- unfolding tendsto_iff
+ unfolding tendsto_def
using netlimit_within[of x s]
by (cases "trivial_limit (at x within s)") (auto simp add: trivial_limit_eventually)
@@ -3166,17 +3146,9 @@
using continuous_within [of x UNIV f] by (simp add: within_UNIV)
lemma continuous_at_within:
- fixes x :: "'a::perfect_space"
assumes "continuous (at x) f" shows "continuous (at x within s) f"
- (* FIXME: generalize *)
-proof(cases "x islimpt s")
- case True show ?thesis using assms unfolding continuous_def and netlimit_at
- using Lim_at_within[of f "f x" "at x" s]
- unfolding netlimit_within[unfolded trivial_limit_within not_not, OF True] by blast
-next
- case False thus ?thesis unfolding continuous_def and netlimit_at
- unfolding Lim and trivial_limit_within by auto
-qed
+ using assms unfolding continuous_at continuous_within
+ by (rule Lim_at_within)
text{* Derive the epsilon-delta forms, which we often use as "definitions" *}
@@ -3308,8 +3280,10 @@
text{* Characterization of various kinds of continuity in terms of sequences. *}
+(* \<longrightarrow> could be generalized, but \<longleftarrow> requires metric space *)
lemma continuous_within_sequentially:
- "continuous (at a within s) f \<longleftrightarrow>
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ shows "continuous (at a within s) f \<longleftrightarrow>
(\<forall>x. (\<forall>n::nat. x n \<in> s) \<and> (x ---> a) sequentially
--> ((f o x) ---> f a) sequentially)" (is "?lhs = ?rhs")
proof
@@ -3349,7 +3323,8 @@
qed
lemma continuous_at_sequentially:
- "continuous (at a) f \<longleftrightarrow> (\<forall>x. (x ---> a) sequentially
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+ shows "continuous (at a) f \<longleftrightarrow> (\<forall>x. (x ---> a) sequentially
--> ((f o x) ---> f a) sequentially)"
using continuous_within_sequentially[of a UNIV f] unfolding within_UNIV by auto
@@ -3449,22 +3424,22 @@
by (auto simp add: continuous_def Lim_const)
lemma continuous_cmul:
- fixes f :: "'a::metric_space \<Rightarrow> real ^ 'n::finite"
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous net f ==> continuous net (\<lambda>x. c *\<^sub>R f x)"
by (auto simp add: continuous_def Lim_cmul)
lemma continuous_neg:
- fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous net f ==> continuous net (\<lambda>x. -(f x))"
by (auto simp add: continuous_def Lim_neg)
lemma continuous_add:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x + g x)"
by (auto simp add: continuous_def Lim_add)
lemma continuous_sub:
- fixes f g :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+ fixes f g :: "'a::t2_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous net f \<Longrightarrow> continuous net g \<Longrightarrow> continuous net (\<lambda>x. f x - g x)"
by (auto simp add: continuous_def Lim_sub)
@@ -3475,7 +3450,7 @@
unfolding continuous_on_eq_continuous_within using continuous_const by blast
lemma continuous_on_cmul:
- fixes f :: "'a::metric_space \<Rightarrow> real ^ _"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
shows "continuous_on s f ==> continuous_on s (\<lambda>x. c *\<^sub>R (f x))"
unfolding continuous_on_eq_continuous_within using continuous_cmul by blast
@@ -3503,7 +3478,8 @@
unfolding uniformly_continuous_on_def by simp
lemma uniformly_continuous_on_cmul:
- fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _"
+ fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+ (* FIXME: generalize 'a to metric_space *)
assumes "uniformly_continuous_on s f"
shows "uniformly_continuous_on s (\<lambda>x. c *\<^sub>R f(x))"
proof-
@@ -3551,11 +3527,11 @@
lemma continuous_within_id:
"continuous (at a within s) (\<lambda>x. x)"
- unfolding continuous_within Lim_within by auto
+ unfolding continuous_within by (rule Lim_at_within [OF Lim_ident_at])
lemma continuous_at_id:
"continuous (at a) (\<lambda>x. x)"
- unfolding continuous_at Lim_at by auto
+ unfolding continuous_at by (rule Lim_ident_at)
lemma continuous_on_id:
"continuous_on s (\<lambda>x. x)"
@@ -3568,6 +3544,8 @@
text{* Continuity of all kinds is preserved under composition. *}
lemma continuous_within_compose:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+ fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space"
assumes "continuous (at x within s) f" "continuous (at (f x) within f ` s) g"
shows "continuous (at x within s) (g o f)"
proof-
@@ -3582,6 +3560,8 @@
qed
lemma continuous_at_compose:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+ fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space"
assumes "continuous (at x) f" "continuous (at (f x)) g"
shows "continuous (at x) (g o f)"
proof-
@@ -3607,7 +3587,8 @@
text{* Continuity in terms of open preimages. *}
lemma continuous_at_open:
- "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))" (is "?lhs = ?rhs")
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+ shows "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))" (is "?lhs = ?rhs")
proof
assume ?lhs
{ fix t assume as: "open t" "f x \<in> t"
@@ -3736,13 +3717,25 @@
qed
lemma continuous_open_preimage_univ:
- "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+ shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto
lemma continuous_closed_preimage_univ:
- "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+ shows "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
+lemma continuous_open_vimage:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+ shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open (f -` s)"
+ unfolding vimage_def by (rule continuous_open_preimage_univ)
+
+lemma continuous_closed_vimage:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
+ shows "\<forall>x. continuous (at x) f \<Longrightarrow> closed s \<Longrightarrow> closed (f -` s)"
+ unfolding vimage_def by (rule continuous_closed_preimage_univ)
+
text{* Equality of continuous functions on closure and related results. *}
lemma continuous_closed_in_preimage_constant:
@@ -3786,6 +3779,7 @@
text{* Making a continuous function avoid some value in a neighbourhood. *}
lemma continuous_within_avoid:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
assumes "continuous (at x within s) f" "x \<in> s" "f x \<noteq> a"
shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e --> f y \<noteq> a"
proof-
@@ -3798,6 +3792,7 @@
qed
lemma continuous_at_avoid:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* FIXME: generalize *)
assumes "continuous (at x) f" "f x \<noteq> a"
shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
using assms using continuous_within_avoid[of x UNIV f a, unfolded within_UNIV] by auto
@@ -3873,7 +3868,7 @@
qed
lemma open_affinity:
- fixes s :: "(real ^ _) set"
+ fixes s :: "'a::real_normed_vector set"
assumes "open s" "c \<noteq> 0"
shows "open ((\<lambda>x. a + c *\<^sub>R x) ` s)"
proof-
@@ -4025,59 +4020,44 @@
subsection{* Topological properties of linear functions. *}
-lemma linear_lim_0: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
- assumes "linear f" shows "(f ---> 0) (at (0))"
+lemma linear_lim_0:
+ assumes "bounded_linear f" shows "(f ---> 0) (at (0))"
proof-
- obtain B where "B>0" and B:"\<forall>x. norm (f x) \<le> B * norm x" using linear_bounded_pos[OF assms] by auto
- { fix e::real assume "e>0"
- { fix x::"real^'a" assume "norm x < e / B"
- hence "B * norm x < e" using `B>0` using mult_strict_right_mono[of "norm x" " e / B" B] unfolding real_mult_commute by auto
- hence "norm (f x) < e" using B[THEN spec[where x=x]] `B>0` using order_le_less_trans[of "norm (f x)" "B * norm x" e] by auto }
- moreover have "e / B > 0" using `e>0` `B>0` divide_pos_pos by auto
- ultimately have "\<exists>d>0. \<forall>x. 0 < dist x 0 \<and> dist x 0 < d \<longrightarrow> dist (f x) 0 < e" unfolding dist_norm by auto }
- thus ?thesis unfolding Lim_at by auto
-qed
-
-lemma bounded_linear_continuous_at:
+ interpret f: bounded_linear f by fact
+ have "(f ---> f 0) (at 0)"
+ using tendsto_ident_at by (rule f.tendsto)
+ thus ?thesis unfolding f.zero .
+qed
+
+lemma linear_continuous_at:
assumes "bounded_linear f" shows "continuous (at a) f"
unfolding continuous_at using assms
apply (rule bounded_linear.tendsto)
- apply (rule Lim_at_id [unfolded id_def])
+ apply (rule tendsto_ident_at)
done
-lemma linear_continuous_at:
- fixes f :: "real ^ _ \<Rightarrow> real ^ _"
- assumes "linear f" shows "continuous (at a) f"
- using assms unfolding linear_conv_bounded_linear
- by (rule bounded_linear_continuous_at)
-
lemma linear_continuous_within:
- fixes f :: "real ^ _ \<Rightarrow> real ^ _"
- shows "linear f ==> continuous (at x within s) f"
+ shows "bounded_linear f ==> continuous (at x within s) f"
using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
lemma linear_continuous_on:
- fixes f :: "real ^ _ \<Rightarrow> real ^ _"
- shows "linear f ==> continuous_on s f"
+ shows "bounded_linear f ==> continuous_on s f"
using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
text{* Also bilinear functions, in composition form. *}
lemma bilinear_continuous_at_compose:
- fixes f :: "real ^ _ \<Rightarrow> real ^ _"
- shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bilinear h
+ shows "continuous (at x) f \<Longrightarrow> continuous (at x) g \<Longrightarrow> bounded_bilinear h
==> continuous (at x) (\<lambda>x. h (f x) (g x))"
unfolding continuous_at using Lim_bilinear[of f "f x" "(at x)" g "g x" h] by auto
lemma bilinear_continuous_within_compose:
- fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
- shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bilinear h
+ shows "continuous (at x within s) f \<Longrightarrow> continuous (at x within s) g \<Longrightarrow> bounded_bilinear h
==> continuous (at x within s) (\<lambda>x. h (f x) (g x))"
unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
lemma bilinear_continuous_on_compose:
- fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
- shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bilinear h
+ shows "continuous_on s f \<Longrightarrow> continuous_on s g \<Longrightarrow> bounded_bilinear h
==> continuous_on s (\<lambda>x. h (f x) (g x))"
unfolding continuous_on_eq_continuous_within apply auto apply(erule_tac x=x in ballE) apply auto apply(erule_tac x=x in ballE) apply auto
using bilinear_continuous_within_compose[of _ s f g h] by auto
@@ -4233,10 +4213,10 @@
subsection{* We can now extend limit compositions to consider the scalar multiplier. *}
lemma Lim_mul:
- fixes f :: "'a \<Rightarrow> real ^ _"
+ fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes "(c ---> d) net" "(f ---> l) net"
shows "((\<lambda>x. c(x) *\<^sub>R f x) ---> (d *\<^sub>R l)) net"
- unfolding smult_conv_scaleR using assms by (rule scaleR.tendsto)
+ using assms by (rule scaleR.tendsto)
lemma Lim_vmul:
fixes c :: "'a \<Rightarrow> real" and v :: "'b::real_normed_vector"
@@ -4367,25 +4347,20 @@
text{* Hence some useful properties follow quite easily. *}
-lemma compact_scaleR_image:
+lemma compact_scaling:
fixes s :: "'a::real_normed_vector set"
- assumes "compact s" shows "compact ((\<lambda>x. scaleR c x) ` s)"
+ assumes "compact s" shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)"
proof-
let ?f = "\<lambda>x. scaleR c x"
have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right)
show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
- using bounded_linear_continuous_at[OF *] assms by auto
-qed
-
-lemma compact_scaling:
- fixes s :: "(real ^ _) set"
- assumes "compact s" shows "compact ((\<lambda>x. c *\<^sub>R x) ` s)"
- using assms unfolding smult_conv_scaleR by (rule compact_scaleR_image)
+ using linear_continuous_at[OF *] assms by auto
+qed
lemma compact_negations:
fixes s :: "'a::real_normed_vector set"
assumes "compact s" shows "compact ((\<lambda>x. -x) ` s)"
- using compact_scaleR_image [OF assms, of "- 1"] by auto
+ using compact_scaling [OF assms, of "- 1"] by auto
lemma compact_sums:
fixes s t :: "'a::real_normed_vector set"
@@ -4416,7 +4391,7 @@
qed
lemma compact_affinity:
- fixes s :: "(real ^ _) set"
+ fixes s :: "'a::real_normed_vector set"
assumes "compact s" shows "compact ((\<lambda>x. a + c *\<^sub>R x) ` s)"
proof-
have "op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
@@ -4490,9 +4465,9 @@
text{* Related results with closure as the conclusion. *}
-lemma closed_scaleR_image:
+lemma closed_scaling:
fixes s :: "'a::real_normed_vector set"
- assumes "closed s" shows "closed ((\<lambda>x. scaleR c x) ` s)"
+ assumes "closed s" shows "closed ((\<lambda>x. c *\<^sub>R x) ` s)"
proof(cases "s={}")
case True thus ?thesis by auto
next
@@ -4524,15 +4499,10 @@
qed
qed
-lemma closed_scaling:
- fixes s :: "(real ^ _) set"
- assumes "closed s" shows "closed ((\<lambda>x. c *\<^sub>R x) ` s)"
- using assms unfolding smult_conv_scaleR by (rule closed_scaleR_image)
-
lemma closed_negations:
fixes s :: "'a::real_normed_vector set"
assumes "closed s" shows "closed ((\<lambda>x. -x) ` s)"
- using closed_scaleR_image[OF assms, of "- 1"] by simp
+ using closed_scaling[OF assms, of "- 1"] by simp
lemma compact_closed_sums:
fixes s :: "'a::real_normed_vector set"
@@ -5149,24 +5119,12 @@
subsection{* Closure of halfspaces and hyperplanes. *}
-lemma Lim_dot: fixes f :: "real^'m \<Rightarrow> real^'n::finite"
- assumes "(f ---> l) net" shows "((\<lambda>y. a \<bullet> (f y)) ---> a \<bullet> l) net"
- unfolding dot_def by (intro tendsto_intros assms)
-
-lemma continuous_at_dot:
- fixes x :: "real ^ _"
- shows "continuous (at x) (\<lambda>y. a \<bullet> y)"
-proof-
- have "((\<lambda>x. x) ---> x) (at x)" unfolding Lim_at by auto
- thus ?thesis unfolding continuous_at and o_def using Lim_dot[of "\<lambda>x. x" x "at x" a] by auto
-qed
-
-lemma continuous_on_dot:
- fixes s :: "(real ^ _) set"
- shows "continuous_on s (\<lambda>y. a \<bullet> y)"
- using continuous_at_imp_continuous_on[of s "\<lambda>y. a \<bullet> y"]
- using continuous_at_dot
- by auto
+lemma Lim_inner:
+ assumes "(f ---> l) net" shows "((\<lambda>y. inner a (f y)) ---> inner a l) net"
+ by (intro tendsto_intros assms)
+
+lemma continuous_at_inner: "continuous (at x) (inner a)"
+ unfolding continuous_at by (intro tendsto_intros)
lemma continuous_on_inner:
fixes s :: "'a::real_inner set"
@@ -5175,16 +5133,12 @@
lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
proof-
- have *:"{x \<in> UNIV. inner a x \<in> {r. \<exists>x. inner a x = r \<and> r \<le> b}} = {x. inner a x \<le> b}" by auto
- let ?T = "{..b}"
- have "closed ?T" by (rule closed_real_atMost)
- moreover have "{r. \<exists>x. inner a x = r \<and> r \<le> b} = range (inner a) \<inter> ?T"
- unfolding image_def by auto
- ultimately have "\<exists>T. closed T \<and> {r. \<exists>x. inner a x = r \<and> r \<le> b} = range (inner a) \<inter> T" by fast
- hence "closedin euclidean {x \<in> UNIV. inner a x \<in> {r. \<exists>x. inner a x = r \<and> r \<le> b}}"
- using continuous_on_inner[of UNIV a, unfolded continuous_on_closed subtopology_UNIV] unfolding closedin_closed
- by (fast elim!: allE[where x="{r. (\<exists>x. inner a x = r \<and> r \<le> b)}"])
- thus ?thesis unfolding closed_closedin[THEN sym] and * by auto
+ have "\<forall>x. continuous (at x) (inner a)"
+ unfolding continuous_at by (rule allI) (intro tendsto_intros)
+ hence "closed (inner a -` {..b})"
+ using closed_real_atMost by (rule continuous_closed_vimage)
+ moreover have "{x. inner a x \<le> b} = inner a -` {..b}" by auto
+ ultimately show ?thesis by simp
qed
lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
@@ -5279,7 +5233,7 @@
using assms unfolding continuous_on unfolding Lim_within_union
unfolding Lim unfolding trivial_limit_within unfolding closed_limpt by auto
-lemma continuous_on_cases: fixes g :: "real^'m::finite \<Rightarrow> real ^'n::finite"
+lemma continuous_on_cases:
assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g"
"\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x"
shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
@@ -5335,22 +5289,24 @@
(\<forall>x\<in>s. (g(f x) = x)) \<and> (f ` s = t) \<and> continuous_on s f \<and>
(\<forall>y\<in>t. (f(g y) = y)) \<and> (g ` t = s) \<and> continuous_on t g"
-definition homeomorphic :: "((real^'a::finite) set) \<Rightarrow> ((real^'b::finite) set) \<Rightarrow> bool" (infixr "homeomorphic" 60) where
+definition
+ homeomorphic :: "'a::metric_space set \<Rightarrow> 'b::metric_space set \<Rightarrow> bool"
+ (infixr "homeomorphic" 60) where
homeomorphic_def: "s homeomorphic t \<equiv> (\<exists>f g. homeomorphism s t f g)"
lemma homeomorphic_refl: "s homeomorphic s"
unfolding homeomorphic_def
unfolding homeomorphism_def
using continuous_on_id
- apply(rule_tac x = "(\<lambda>x::real^'a.x)" in exI)
- apply(rule_tac x = "(\<lambda>x::real^'b.x)" in exI)
+ apply(rule_tac x = "(\<lambda>x. x)" in exI)
+ apply(rule_tac x = "(\<lambda>x. x)" in exI)
by blast
lemma homeomorphic_sym:
"s homeomorphic t \<longleftrightarrow> t homeomorphic s"
unfolding homeomorphic_def
unfolding homeomorphism_def
-by blast
+by blast (* FIXME: slow *)
lemma homeomorphic_trans:
assumes "s homeomorphic t" "t homeomorphic u" shows "s homeomorphic u"
@@ -5392,7 +5348,8 @@
using assms unfolding inj_on_def inv_on_def by auto
lemma homeomorphism_compact:
- fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+ fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
+ (* class constraint due to continuous_on_inverse *)
assumes "compact s" "continuous_on s f" "f ` s = t" "inj_on f s"
shows "\<exists>g. homeomorphism s t f g"
proof-
@@ -5419,7 +5376,9 @@
qed
lemma homeomorphic_compact:
- "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
+ fixes f :: "'a::heine_borel \<Rightarrow> 'b::heine_borel"
+ (* class constraint due to continuous_on_inverse *)
+ shows "compact s \<Longrightarrow> continuous_on s f \<Longrightarrow> (f ` s = t) \<Longrightarrow> inj_on f s
\<Longrightarrow> s homeomorphic t"
unfolding homeomorphic_def by(metis homeomorphism_compact)
@@ -5433,6 +5392,7 @@
text{* Results on translation, scaling etc. *}
lemma homeomorphic_scaling:
+ fixes s :: "'a::real_normed_vector set"
assumes "c \<noteq> 0" shows "s homeomorphic ((\<lambda>x. c *\<^sub>R x) ` s)"
unfolding homeomorphic_minimal
apply(rule_tac x="\<lambda>x. c *\<^sub>R x" in exI)
@@ -5441,13 +5401,15 @@
using continuous_on_cmul[OF continuous_on_id] by auto
lemma homeomorphic_translation:
- "s homeomorphic ((\<lambda>x. a + x) ` s)"
+ fixes s :: "'a::real_normed_vector set"
+ shows "s homeomorphic ((\<lambda>x. a + x) ` s)"
unfolding homeomorphic_minimal
apply(rule_tac x="\<lambda>x. a + x" in exI)
apply(rule_tac x="\<lambda>x. -a + x" in exI)
using continuous_on_add[OF continuous_on_const continuous_on_id] by auto
lemma homeomorphic_affinity:
+ fixes s :: "'a::real_normed_vector set"
assumes "c \<noteq> 0" shows "s homeomorphic ((\<lambda>x. a + c *\<^sub>R x) ` s)"
proof-
have *:"op + a ` op *\<^sub>R c ` s = (\<lambda>x. a + c *\<^sub>R x) ` s" by auto
@@ -5457,7 +5419,8 @@
using homeomorphic_translation[of "(\<lambda>x. c *\<^sub>R x) ` s" a] unfolding * by auto
qed
-lemma homeomorphic_balls: fixes a b ::"real^'a::finite"
+lemma homeomorphic_balls:
+ fixes a b ::"'a::real_normed_vector" (* FIXME: generalize to metric_space *)
assumes "0 < d" "0 < e"
shows "(ball a d) homeomorphic (ball b e)" (is ?th)
"(cball a d) homeomorphic (cball b e)" (is ?cth)
@@ -5487,14 +5450,15 @@
lemma cauchy_isometric:
fixes x :: "nat \<Rightarrow> real ^ 'n::finite"
- assumes e:"0 < e" and s:"subspace s" and f:"linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and xs:"\<forall>n::nat. x n \<in> s" and cf:"Cauchy(f o x)"
+ assumes e:"0 < e" and s:"subspace s" and f:"bounded_linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and xs:"\<forall>n::nat. x n \<in> s" and cf:"Cauchy(f o x)"
shows "Cauchy x"
proof-
+ interpret f: bounded_linear f by fact
{ fix d::real assume "d>0"
then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] and e and mult_pos_pos[of e d] by auto
{ fix n assume "n\<ge>N"
- hence "norm (f (x n - x N)) < e * d" using N[THEN spec[where x=n]] unfolding linear_sub[OF f, THEN sym] by auto
+ hence "norm (f (x n - x N)) < e * d" using N[THEN spec[where x=n]] unfolding f.diff[THEN sym] by auto
moreover have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
using subspace_sub[OF s, of "x n" "x N"] using xs[THEN spec[where x=N]] and xs[THEN spec[where x=n]]
using normf[THEN bspec[where x="x n - x N"]] by auto
@@ -5506,7 +5470,7 @@
lemma complete_isometric_image:
fixes f :: "real ^ _ \<Rightarrow> real ^ _"
- assumes "0 < e" and s:"subspace s" and f:"linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and cs:"complete s"
+ assumes "0 < e" and s:"subspace s" and f:"bounded_linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and cs:"complete s"
shows "complete(f ` s)"
proof-
{ fix g assume as:"\<forall>n::nat. g n \<in> f ` s" and cfg:"Cauchy g"
@@ -5529,7 +5493,7 @@
unfolding dist_norm by simp
lemma injective_imp_isometric: fixes f::"real^'m::finite \<Rightarrow> real^'n::finite"
- assumes s:"closed s" "subspace s" and f:"linear f" "\<forall>x\<in>s. (f x = 0) \<longrightarrow> (x = 0)"
+ 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)"
proof(cases "s \<subseteq> {0::real^'m}")
case True
@@ -5538,6 +5502,7 @@
hence "norm x \<le> norm (f x)" by auto }
thus ?thesis by(auto intro!: exI[where x=1])
next
+ interpret f: bounded_linear f by fact
case False
then obtain a where a:"a\<noteq>0" "a\<in>s" by auto
from False have "s \<noteq> {}" by auto
@@ -5571,7 +5536,7 @@
have "\<forall>c. \<forall>x\<in>s. c *\<^sub>R x \<in> s" using s[unfolded subspace_def smult_conv_scaleR] by auto
hence "(norm a / norm x) *\<^sub>R x \<in> {x \<in> s. norm x = norm a}" using `x\<in>s` and `x\<noteq>0` by auto
thus "norm (f b) / norm b * norm x \<le> norm (f x)" using b[THEN bspec[where x="(norm a / norm x) *\<^sub>R x"]]
- unfolding linear_cmul[OF f(1), unfolded smult_conv_scaleR] and ba using `x\<noteq>0` `a\<noteq>0`
+ unfolding f.scaleR and ba using `x\<noteq>0` `a\<noteq>0`
by (auto simp add: real_mult_commute pos_le_divide_eq pos_divide_le_eq)
qed }
ultimately
@@ -5579,8 +5544,8 @@
qed
lemma closed_injective_image_subspace:
- fixes s :: "(real ^ _) set"
- assumes "subspace s" "linear f" "\<forall>x\<in>s. f x = 0 --> x = 0" "closed s"
+ fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+ assumes "subspace s" "bounded_linear f" "\<forall>x\<in>s. f x = 0 --> x = 0" "closed s"
shows "closed(f ` s)"
proof-
obtain e where "e>0" and e:"\<forall>x\<in>s. e * norm x \<le> norm (f x)" using injective_imp_isometric[OF assms(4,1,2,3)] by auto
@@ -5688,10 +5653,11 @@
then obtain d::"'n set" where t: "card d = dim s"
using closed_subspace_lemma by auto
let ?t = "{x::real^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0}"
- obtain f where f:"linear f" "f ` ?t = s" "inj_on f ?t"
- using subspace_isomorphism[OF subspace_substandard[of "\<lambda>i. i \<notin> d"] assms]
+ obtain f where f:"bounded_linear f" "f ` ?t = s" "inj_on f ?t"
+ using subspace_isomorphism[unfolded linear_conv_bounded_linear, OF subspace_substandard[of "\<lambda>i. i \<notin> d"] assms]
using dim_substandard[of d] and t by auto
- have "\<forall>x\<in>?t. f x = 0 \<longrightarrow> x = 0" using linear_0[OF f(1)] using f(3)[unfolded inj_on_def]
+ interpret f: bounded_linear f by fact
+ have "\<forall>x\<in>?t. f x = 0 \<longrightarrow> x = 0" using f.zero using f(3)[unfolded inj_on_def]
by(erule_tac x=0 in ballE) auto
moreover have "closed ?t" using closed_substandard .
moreover have "subspace ?t" using subspace_substandard .
--- a/src/HOL/Tools/quickcheck_generators.ML Wed Jun 17 08:21:27 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML Wed Jun 17 08:31:13 2009 +0200
@@ -212,7 +212,7 @@
fun prove_eqs aux_simp proj_defs lthy =
let
val proj_simps = map (snd o snd) proj_defs;
- fun tac { context = ctxt, ... } =
+ fun tac { context = ctxt, prems = _ } =
ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv]));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/scan.scala Wed Jun 17 08:31:13 2009 +0200
@@ -0,0 +1,140 @@
+/* Title: Pure/General/scan.scala
+ Author: Makarius
+
+Efficient scanning of keywords.
+*/
+
+package isabelle
+
+import scala.util.parsing.combinator.RegexParsers
+
+
+object Scan
+{
+
+ /** Lexicon -- position tree **/
+
+ object Lexicon
+ {
+ private case class Tree(val branches: Map[Char, (String, Tree)])
+ private val empty_tree = Tree(Map())
+
+ private def make(tree: Tree, max: Int): Lexicon =
+ new Lexicon {
+ override val main_tree = tree
+ override val max_entry = max
+ }
+
+ val empty: Lexicon = new Lexicon
+ def apply(strs: String*): Lexicon = (empty /: strs) ((lex, str) => lex + str)
+ }
+
+ class Lexicon extends scala.collection.immutable.Set[String] with RegexParsers
+ {
+ /* representation */
+
+ import Lexicon.Tree
+ val main_tree: Tree = Lexicon.empty_tree
+ val max_entry = -1
+
+
+ /* auxiliary operations */
+
+ private def content(tree: Tree, result: List[String]): List[String] =
+ (result /: tree.branches.toList) ((res, entry) =>
+ entry match { case (_, (s, tr)) =>
+ if (s.isEmpty) content(tr, res) else content(tr, s :: res) })
+
+ private def lookup(str: CharSequence): Option[(Boolean, Tree)] =
+ {
+ val len = str.length
+ def look(tree: Tree, tip: Boolean, i: Int): Option[(Boolean, Tree)] =
+ {
+ if (i < len) {
+ tree.branches.get(str.charAt(i)) match {
+ case Some((s, tr)) => look(tr, !s.isEmpty, i + 1)
+ case None => None
+ }
+ } else Some(tip, tree)
+ }
+ look(main_tree, false, 0)
+ }
+
+ def completions(str: CharSequence): List[String] =
+ {
+ (lookup(str) match {
+ case Some((true, tree)) => content(tree, List(str.toString))
+ case Some((false, tree)) => content(tree, Nil)
+ case None => Nil
+ }).sort((s1, s2) => s1.length < s2.length || s1.length == s2.length && s1 <= s2)
+ }
+
+
+ /* Set methods */
+
+ override def stringPrefix = "Lexicon"
+
+ override def isEmpty: Boolean = { max_entry < 0 }
+
+ def size: Int = content(main_tree, Nil).length
+ def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements
+
+ def contains(str: String): Boolean =
+ lookup(str) match {
+ case Some((tip, _)) => tip
+ case _ => false
+ }
+
+ def +(str: String): Lexicon =
+ {
+ val len = str.length
+ def extend(tree: Tree, i: Int): Tree =
+ {
+ if (i < len) {
+ val c = str.charAt(i)
+ val end = (i + 1 == len)
+ tree.branches.get(c) match {
+ case Some((s, tr)) =>
+ Tree(tree.branches + (c -> (if (end) str else s, extend(tr, i + 1))))
+ case None =>
+ Tree(tree.branches + (c -> (if (end) str else "", extend(Lexicon.empty_tree, i + 1))))
+ }
+ } else tree
+ }
+ if (contains(str)) this
+ else Lexicon.make(extend(main_tree, 0), max_entry max str.length)
+ }
+
+ def empty[A]: Set[A] = error("Undefined")
+ def -(str: String): Lexicon = error("Undefined")
+
+
+ /* RegexParsers methods */
+
+ override val whiteSpace = "".r
+
+ def keyword: Parser[String] = new Parser[String] {
+ def apply(in: Input) =
+ {
+ val source = in.source
+ val offset = in.offset
+ val len = source.length - offset
+
+ def scan(tree: Tree, text: String, i: Int): String =
+ {
+ if (i < len) {
+ tree.branches.get(source.charAt(offset + i)) match {
+ case Some((s, tr)) => scan(tr, if (s.isEmpty) text else s, i + 1)
+ case None => text
+ }
+ } else text
+ }
+ val text = scan(main_tree, "", 0)
+ if (text.isEmpty) Failure("keyword expected", in)
+ else Success(text, in.drop(text.length))
+ }
+ }.named("keyword")
+
+ }
+}
+
--- a/src/Pure/General/symbol.scala Wed Jun 17 08:21:27 2009 +0200
+++ b/src/Pure/General/symbol.scala Wed Jun 17 08:31:13 2009 +0200
@@ -118,6 +118,18 @@
yield read_decl(decl)
+ /* misc properties */
+
+ val names: Map[String, String] = {
+ val name = new Regex("""\\<([A-Za-z][A-Za-z0-9_']*)>""")
+ Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
+ }
+
+ val abbrevs: Map[String, String] = Map((
+ for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
+ yield (sym -> props("abbrev"))): _*)
+
+
/* main recoder methods */
private val (decoder, encoder) =
--- a/src/Pure/IsaMakefile Wed Jun 17 08:21:27 2009 +0200
+++ b/src/Pure/IsaMakefile Wed Jun 17 08:31:13 2009 +0200
@@ -115,9 +115,9 @@
## Scala material
SCALA_FILES = General/event_bus.scala General/markup.scala \
- General/position.scala General/swing.scala General/symbol.scala \
- General/xml.scala General/yxml.scala Isar/isar.scala \
- Isar/isar_document.scala Isar/outer_keyword.scala \
+ General/position.scala General/scan.scala General/swing.scala \
+ General/symbol.scala General/xml.scala General/yxml.scala \
+ Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala \
System/cygwin.scala System/isabelle_process.scala \
System/isabelle_system.scala Thy/thy_header.scala \
Tools/isabelle_syntax.scala
--- a/src/Pure/pure_setup.ML Wed Jun 17 08:21:27 2009 +0200
+++ b/src/Pure/pure_setup.ML Wed Jun 17 08:31:13 2009 +0200
@@ -4,15 +4,6 @@
Pure theory and ML toplevel setup.
*)
-(* ML toplevel use commands *)
-
-fun use name = Toplevel.program (fn () => ThyInfo.use name);
-fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name);
-fun use_thy name = Toplevel.program (fn () => ThyInfo.use_thy name);
-fun time_use name = Toplevel.program (fn () => ThyInfo.time_use name);
-fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
-
-
(* the Pure theories *)
val theory = ThyInfo.get_theory;
@@ -49,6 +40,15 @@
else ();
+(* ML toplevel use commands *)
+
+fun use name = Toplevel.program (fn () => ThyInfo.use name);
+fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name);
+fun use_thy name = Toplevel.program (fn () => ThyInfo.use_thy name);
+fun time_use name = Toplevel.program (fn () => ThyInfo.time_use name);
+fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
+
+
(* misc *)
val cd = File.cd o Path.explode;