--- a/src/HOL/Complete_Lattice.thy Mon Apr 26 16:08:04 2010 +0200
+++ b/src/HOL/Complete_Lattice.thy Mon Apr 26 09:45:22 2010 -0700
@@ -98,9 +98,9 @@
syntax
"_SUP1" :: "pttrns => 'b => 'b" ("(3SUP _./ _)" [0, 10] 10)
- "_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" [0, 10] 10)
+ "_SUP" :: "pttrn => 'a set => 'b => 'b" ("(3SUP _:_./ _)" [0, 0, 10] 10)
"_INF1" :: "pttrns => 'b => 'b" ("(3INF _./ _)" [0, 10] 10)
- "_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" [0, 10] 10)
+ "_INF" :: "pttrn => 'a set => 'b => 'b" ("(3INF _:_./ _)" [0, 0, 10] 10)
translations
"SUP x y. B" == "SUP x. SUP y. B"
@@ -295,15 +295,15 @@
syntax
"_UNION1" :: "pttrns => 'b set => 'b set" ("(3UN _./ _)" [0, 10] 10)
- "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 10] 10)
+ "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3UN _:_./ _)" [0, 0, 10] 10)
syntax (xsymbols)
"_UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>_./ _)" [0, 10] 10)
- "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" [0, 10] 10)
+ "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>_\<in>_./ _)" [0, 0, 10] 10)
syntax (latex output)
"_UNION1" :: "pttrns => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
- "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
+ "_UNION" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
translations
"UN x y. B" == "UN x. UN y. B"
@@ -531,15 +531,15 @@
syntax
"_INTER1" :: "pttrns => 'b set => 'b set" ("(3INT _./ _)" [0, 10] 10)
- "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 10] 10)
+ "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3INT _:_./ _)" [0, 0, 10] 10)
syntax (xsymbols)
"_INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>_./ _)" [0, 10] 10)
- "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 10] 10)
+ "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10)
syntax (latex output)
"_INTER1" :: "pttrns => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
- "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 10] 10)
+ "_INTER" :: "pttrn => 'a set => 'b set => 'b set" ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
translations
"INT x y. B" == "INT x. INT y. B"
--- a/src/HOL/HOL.thy Mon Apr 26 16:08:04 2010 +0200
+++ b/src/HOL/HOL.thy Mon Apr 26 09:45:22 2010 -0700
@@ -73,7 +73,7 @@
local
consts
- If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)
+ If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" [0, 0, 10] 10)
subsubsection {* Additional concrete syntax *}
@@ -118,7 +118,7 @@
"_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10)
"" :: "letbind => letbinds" ("_")
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _")
- "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
+ "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" [0, 10] 10)
"_case_syntax":: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10)
"_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10)
--- a/src/HOL/Library/FrechetDeriv.thy Mon Apr 26 16:08:04 2010 +0200
+++ b/src/HOL/Library/FrechetDeriv.thy Mon Apr 26 09:45:22 2010 -0700
@@ -385,7 +385,7 @@
fixes x :: "'a::{real_normed_algebra,comm_ring_1}"
shows "FDERIV (\<lambda>x. x ^ Suc n) x :> (\<lambda>h. (1 + of_nat n) * x ^ n * h)"
apply (induct n)
- apply (simp add: power_Suc FDERIV_ident)
+ apply (simp add: FDERIV_ident)
apply (drule FDERIV_mult [OF FDERIV_ident])
apply (simp only: of_nat_Suc left_distrib mult_1_left)
apply (simp only: power_Suc right_distrib add_ac mult_ac)
--- a/src/HOL/Library/Permutations.thy Mon Apr 26 16:08:04 2010 +0200
+++ b/src/HOL/Library/Permutations.thy Mon Apr 26 09:45:22 2010 -0700
@@ -96,7 +96,7 @@
lemma permutes_superset:
"p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
-by (simp add: Ball_def permutes_def Diff_iff) metis
+by (simp add: Ball_def permutes_def) metis
(* ------------------------------------------------------------------------- *)
(* Group properties. *)
@@ -125,7 +125,7 @@
apply (rule permutes_compose[OF pS])
apply (rule permutes_swap_id, simp)
using permutes_in_image[OF pS, of a] apply simp
- apply (auto simp add: Ball_def Diff_iff swap_def)
+ apply (auto simp add: Ball_def swap_def)
done
lemma permutes_insert: "{p. p permutes (insert a S)} =
@@ -154,7 +154,7 @@
lemma card_permutations: assumes Sn: "card S = n" and fS: "finite S"
shows "card {p. p permutes S} = fact n"
using fS Sn proof (induct arbitrary: n)
- case empty thus ?case by (simp add: permutes_empty)
+ case empty thus ?case by simp
next
case (insert x F)
{ fix n assume H0: "card (insert x F) = n"
--- a/src/HOL/Limits.thy Mon Apr 26 16:08:04 2010 +0200
+++ b/src/HOL/Limits.thy Mon Apr 26 09:45:22 2010 -0700
@@ -11,62 +11,59 @@
subsection {* Nets *}
text {*
- A net is now defined as a filter base.
- The definition also allows non-proper filter bases.
+ A net is now defined simply as a filter.
+ The definition also allows non-proper filters.
*}
+locale is_filter =
+ fixes net :: "('a \<Rightarrow> bool) \<Rightarrow> bool"
+ assumes True: "net (\<lambda>x. True)"
+ assumes conj: "net (\<lambda>x. P x) \<Longrightarrow> net (\<lambda>x. Q x) \<Longrightarrow> net (\<lambda>x. P x \<and> Q x)"
+ assumes mono: "\<forall>x. P x \<longrightarrow> Q x \<Longrightarrow> net (\<lambda>x. P x) \<Longrightarrow> net (\<lambda>x. Q x)"
+
typedef (open) 'a net =
- "{net :: 'a set set. (\<exists>A. A \<in> net)
- \<and> (\<forall>A\<in>net. \<forall>B\<in>net. \<exists>C\<in>net. C \<subseteq> A \<and> C \<subseteq> B)}"
+ "{net :: ('a \<Rightarrow> bool) \<Rightarrow> bool. is_filter net}"
proof
- show "UNIV \<in> ?net" by auto
+ show "(\<lambda>x. True) \<in> ?net" by (auto intro: is_filter.intro)
qed
-lemma Rep_net_nonempty: "\<exists>A. A \<in> Rep_net net"
-using Rep_net [of net] by simp
-
-lemma Rep_net_directed:
- "A \<in> Rep_net net \<Longrightarrow> B \<in> Rep_net net \<Longrightarrow> \<exists>C\<in>Rep_net net. C \<subseteq> A \<and> C \<subseteq> B"
+lemma is_filter_Rep_net: "is_filter (Rep_net net)"
using Rep_net [of net] by simp
lemma Abs_net_inverse':
- assumes "\<exists>A. A \<in> net"
- assumes "\<And>A B. A \<in> net \<Longrightarrow> B \<in> net \<Longrightarrow> \<exists>C\<in>net. C \<subseteq> A \<and> C \<subseteq> B"
- shows "Rep_net (Abs_net net) = net"
+ assumes "is_filter net" shows "Rep_net (Abs_net net) = net"
using assms by (simp add: Abs_net_inverse)
-lemma image_nonempty: "\<exists>x. x \<in> A \<Longrightarrow> \<exists>x. x \<in> f ` A"
-by auto
-
subsection {* Eventually *}
definition
eventually :: "('a \<Rightarrow> bool) \<Rightarrow> 'a net \<Rightarrow> bool" where
- [code del]: "eventually P net \<longleftrightarrow> (\<exists>A\<in>Rep_net net. \<forall>x\<in>A. P x)"
+ [code del]: "eventually P net \<longleftrightarrow> Rep_net net P"
+
+lemma eventually_Abs_net:
+ assumes "is_filter net" shows "eventually P (Abs_net net) = net P"
+unfolding eventually_def using assms by (simp add: Abs_net_inverse)
+
+lemma expand_net_eq:
+ shows "net = net' \<longleftrightarrow> (\<forall>P. eventually P net = eventually P net')"
+unfolding Rep_net_inject [symmetric] expand_fun_eq eventually_def ..
lemma eventually_True [simp]: "eventually (\<lambda>x. True) net"
-unfolding eventually_def using Rep_net_nonempty [of net] by fast
+unfolding eventually_def
+by (rule is_filter.True [OF is_filter_Rep_net])
lemma eventually_mono:
"(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P net \<Longrightarrow> eventually Q net"
-unfolding eventually_def by blast
+unfolding eventually_def
+by (rule is_filter.mono [OF is_filter_Rep_net])
lemma eventually_conj:
assumes P: "eventually (\<lambda>x. P x) net"
assumes Q: "eventually (\<lambda>x. Q x) net"
shows "eventually (\<lambda>x. P x \<and> Q x) net"
-proof -
- obtain A where A: "A \<in> Rep_net net" "\<forall>x\<in>A. P x"
- using P unfolding eventually_def by fast
- obtain B where B: "B \<in> Rep_net net" "\<forall>x\<in>B. Q x"
- using Q unfolding eventually_def by fast
- obtain C where C: "C \<in> Rep_net net" "C \<subseteq> A" "C \<subseteq> B"
- using Rep_net_directed [OF A(1) B(1)] by fast
- then have "\<forall>x\<in>C. P x \<and> Q x" "C \<in> Rep_net net"
- using A(2) B(2) by auto
- then show ?thesis unfolding eventually_def ..
-qed
+using assms unfolding eventually_def
+by (rule is_filter.conj [OF is_filter_Rep_net])
lemma eventually_mp:
assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) net"
@@ -102,60 +99,116 @@
using assms by (auto elim!: eventually_rev_mp)
+subsection {* Finer-than relation *}
+
+text {* @{term "net \<le> net'"} means that @{term net'} is finer than
+@{term net}. *}
+
+instantiation net :: (type) "{order,top}"
+begin
+
+definition
+ le_net_def [code del]:
+ "net \<le> net' \<longleftrightarrow> (\<forall>P. eventually P net \<longrightarrow> eventually P net')"
+
+definition
+ less_net_def [code del]:
+ "(net :: 'a net) < net' \<longleftrightarrow> net \<le> net' \<and> \<not> net' \<le> net"
+
+definition
+ top_net_def [code del]:
+ "top = Abs_net (\<lambda>P. True)"
+
+lemma eventually_top [simp]: "eventually P top"
+unfolding top_net_def
+by (subst eventually_Abs_net, rule is_filter.intro, auto)
+
+instance proof
+ fix x y :: "'a net" show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
+ by (rule less_net_def)
+next
+ fix x :: "'a net" show "x \<le> x"
+ unfolding le_net_def by simp
+next
+ fix x y z :: "'a net" assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
+ unfolding le_net_def by simp
+next
+ fix x y :: "'a net" assume "x \<le> y" and "y \<le> x" thus "x = y"
+ unfolding le_net_def expand_net_eq by fast
+next
+ fix x :: "'a net" show "x \<le> top"
+ unfolding le_net_def by simp
+qed
+
+end
+
+lemma net_leD:
+ "net \<le> net' \<Longrightarrow> eventually P net \<Longrightarrow> eventually P net'"
+unfolding le_net_def by simp
+
+lemma net_leI:
+ "(\<And>P. eventually P net \<Longrightarrow> eventually P net') \<Longrightarrow> net \<le> net'"
+unfolding le_net_def by simp
+
+lemma eventually_False:
+ "eventually (\<lambda>x. False) net \<longleftrightarrow> net = top"
+unfolding expand_net_eq by (auto elim: eventually_rev_mp)
+
+
subsection {* Standard Nets *}
definition
- sequentially :: "nat net" where
- [code del]: "sequentially = Abs_net (range (\<lambda>n. {n..}))"
-
-definition
- within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70) where
- [code del]: "net within S = Abs_net ((\<lambda>A. A \<inter> S) ` Rep_net net)"
+ sequentially :: "nat net"
+where [code del]:
+ "sequentially = Abs_net (\<lambda>P. \<exists>k. \<forall>n\<ge>k. P n)"
definition
- at :: "'a::topological_space \<Rightarrow> 'a net" where
- [code del]: "at a = Abs_net ((\<lambda>S. S - {a}) ` {S. open S \<and> a \<in> S})"
-
-lemma Rep_net_sequentially:
- "Rep_net sequentially = range (\<lambda>n. {n..})"
-unfolding sequentially_def
-apply (rule Abs_net_inverse')
-apply (rule image_nonempty, simp)
-apply (clarsimp, rename_tac m n)
-apply (rule_tac x="max m n" in exI, auto)
-done
+ within :: "'a net \<Rightarrow> 'a set \<Rightarrow> 'a net" (infixr "within" 70)
+where [code del]:
+ "net within S = Abs_net (\<lambda>P. eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net)"
-lemma Rep_net_within:
- "Rep_net (net within S) = (\<lambda>A. A \<inter> S) ` Rep_net net"
-unfolding within_def
-apply (rule Abs_net_inverse')
-apply (rule image_nonempty, rule Rep_net_nonempty)
-apply (clarsimp, rename_tac A B)
-apply (drule (1) Rep_net_directed)
-apply (clarify, rule_tac x=C in bexI, auto)
-done
-
-lemma Rep_net_at:
- "Rep_net (at a) = ((\<lambda>S. S - {a}) ` {S. open S \<and> a \<in> S})"
-unfolding at_def
-apply (rule Abs_net_inverse')
-apply (rule image_nonempty)
-apply (rule_tac x="UNIV" in exI, simp)
-apply (clarsimp, rename_tac S T)
-apply (rule_tac x="S \<inter> T" in exI, auto simp add: open_Int)
-done
+definition
+ at :: "'a::topological_space \<Rightarrow> 'a net"
+where [code del]:
+ "at a = Abs_net (\<lambda>P. \<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
lemma eventually_sequentially:
"eventually P sequentially \<longleftrightarrow> (\<exists>N. \<forall>n\<ge>N. P n)"
-unfolding eventually_def Rep_net_sequentially by auto
+unfolding sequentially_def
+proof (rule eventually_Abs_net, rule is_filter.intro)
+ fix P Q :: "nat \<Rightarrow> bool"
+ assume "\<exists>i. \<forall>n\<ge>i. P n" and "\<exists>j. \<forall>n\<ge>j. Q n"
+ then obtain i j where "\<forall>n\<ge>i. P n" and "\<forall>n\<ge>j. Q n" by auto
+ then have "\<forall>n\<ge>max i j. P n \<and> Q n" by simp
+ then show "\<exists>k. \<forall>n\<ge>k. P n \<and> Q n" ..
+qed auto
lemma eventually_within:
"eventually P (net within S) = eventually (\<lambda>x. x \<in> S \<longrightarrow> P x) net"
-unfolding eventually_def Rep_net_within by auto
+unfolding within_def
+by (rule eventually_Abs_net, rule is_filter.intro)
+ (auto elim!: eventually_rev_mp)
+
+lemma within_UNIV: "net within UNIV = net"
+ unfolding expand_net_eq eventually_within by simp
lemma eventually_at_topological:
"eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
-unfolding eventually_def Rep_net_at by auto
+unfolding at_def
+proof (rule eventually_Abs_net, rule is_filter.intro)
+ have "open UNIV \<and> a \<in> UNIV \<and> (\<forall>x\<in>UNIV. x \<noteq> a \<longrightarrow> True)" by simp
+ thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> True)" by - rule
+next
+ fix P Q
+ assume "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x)"
+ and "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> Q x)"
+ then obtain S T where
+ "open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x)"
+ "open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> Q x)" by auto
+ hence "open (S \<inter> T) \<and> a \<in> S \<inter> T \<and> (\<forall>x\<in>(S \<inter> T). x \<noteq> a \<longrightarrow> P x \<and> Q x)"
+ by (simp add: open_Int)
+ thus "\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x \<and> Q x)" by - rule
+qed auto
lemma eventually_at:
fixes a :: "'a::metric_space"
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Apr 26 16:08:04 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon Apr 26 09:45:22 2010 -0700
@@ -22,8 +22,6 @@
imports Convex_Euclidean_Space
begin
-declare norm_scaleR[simp]
-
lemma brouwer_compactness_lemma:
assumes "compact s" "continuous_on s f" "\<not> (\<exists>x\<in>s. (f x = (0::real^'n)))"
obtains d where "0 < d" "\<forall>x\<in>s. d \<le> norm(f x)" proof(cases "s={}") case False
@@ -131,7 +129,7 @@
lemma image_lemma_2: assumes "finite s" "finite t" "card s = card t" "f ` s \<subseteq> t" "f ` s \<noteq> t" "b \<in> t"
shows "(card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 0) \<or>
(card {s'. \<exists>a\<in>s. (s' = s - {a}) \<and> f ` s' = t - {b}} = 2)" proof(cases "{a\<in>s. f ` (s - {a}) = t - {b}} = {}")
- case True thus ?thesis apply-apply(rule disjI1, rule image_lemma_0) using assms(1) by(auto simp add:card_0_eq)
+ case True thus ?thesis apply-apply(rule disjI1, rule image_lemma_0) using assms(1) by auto
next let ?M = "{a\<in>s. f ` (s - {a}) = t - {b}}"
case False then obtain a where "a\<in>?M" by auto hence a:"a\<in>s" "f ` (s - {a}) = t - {b}" by auto
have "f a \<in> t - {b}" using a and assms by auto
@@ -1691,11 +1689,11 @@
path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) \<union>
path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
- by(auto simp add: pathstart_join pathfinish_join path_image_join path_image_linepath path_join path_linepath)
+ by(auto simp add: path_image_join path_linepath)
have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:vector_le_def forall_2 vector_2)
guess z apply(rule fashoda[of ?P1 ?P2 ?a ?b])
unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 proof-
- show "path ?P1" "path ?P2" using assms by(auto simp add: pathstart_join pathfinish_join path_join)
+ show "path ?P1" "path ?P2" using assms by auto
have "path_image ?P1 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 3
apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
unfolding mem_interval forall_2 vector_2 using ab startfin abab assms(3)
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Apr 26 16:08:04 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon Apr 26 09:45:22 2010 -0700
@@ -24,7 +24,7 @@
lemma dest_vec1_simps[simp]: fixes a::"real^1"
shows "a$1 = 0 \<longleftrightarrow> a = 0" (*"a \<le> 1 \<longleftrightarrow> dest_vec1 a \<le> 1" "0 \<le> a \<longleftrightarrow> 0 \<le> dest_vec1 a"*)
"a \<le> b \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 b" "dest_vec1 (1::real^1) = 1"
- by(auto simp add:vector_component_simps forall_1 Cart_eq)
+ by(auto simp add: vector_le_def Cart_eq)
lemma norm_not_0:"(x::real^'n)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto
@@ -50,7 +50,7 @@
lemma mem_interval_1: fixes x :: "real^1" shows
"(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
"(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp_all add: Cart_eq vector_less_def vector_le_def forall_1)
+by(simp_all add: Cart_eq vector_less_def vector_le_def)
lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n)) ` {a..b} =
(if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})"
@@ -66,8 +66,7 @@
apply(rule_tac [!] allI)apply(rule_tac [!] impI)
apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI)
apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI)
- by (auto simp add: vector_less_def vector_le_def forall_1
- vec1_dest_vec1[unfolded One_nat_def])
+ by (auto simp add: vector_less_def vector_le_def)
lemma dest_vec1_setsum: assumes "finite S"
shows " dest_vec1 (setsum f S) = setsum (\<lambda>x. dest_vec1 (f x)) S"
@@ -90,7 +89,7 @@
using one_le_card_finite by auto
lemma real_dimindex_ge_1:"real (CARD('n::finite)) \<ge> 1"
- by(metis dimindex_ge_1 linorder_not_less real_eq_of_nat real_le_trans real_of_nat_1 real_of_nat_le_iff)
+ by(metis dimindex_ge_1 real_eq_of_nat real_of_nat_1 real_of_nat_le_iff)
lemma real_dimindex_gt_0:"real (CARD('n::finite)) > 0" apply(rule less_le_trans[OF _ real_dimindex_ge_1]) by auto
@@ -480,8 +479,8 @@
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::'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-
+ 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 t rule:finite_induct)
+ prefer 2 apply (rule,rule) apply(erule conjE)+ proof-
fix x f u assume ind:"\<forall>u. f \<subseteq> s \<and> (\<forall>x\<in>f. 0 \<le> u x) \<and> setsum u f = 1 \<longrightarrow> (\<Sum>x\<in>f. u x *\<^sub>R x) \<in> s"
assume as:"finite f" "x \<notin> f" "insert x f \<subseteq> s" "\<forall>x\<in>insert x f. 0 \<le> u x" "setsum u (insert x f) = (1::real)"
show "(\<Sum>x\<in>insert x f. u x *\<^sub>R x) \<in> s" proof(cases "u x = 1")
@@ -776,7 +775,7 @@
lemma convex_cball:
fixes x :: "'a::real_normed_vector"
shows "convex(cball x e)"
-proof(auto simp add: convex_def Ball_def mem_cball)
+proof(auto simp add: convex_def Ball_def)
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"
have "dist x (u *\<^sub>R y + v *\<^sub>R z) \<le> u * dist x y + v * dist x z" using uv yz
@@ -1144,7 +1143,7 @@
hence "x + y \<in> s" using `?lhs`[unfolded convex_def, THEN conjunct1]
apply(erule_tac x="2*\<^sub>R x" in ballE) apply(erule_tac x="2*\<^sub>R y" in ballE)
apply(erule_tac x="1/2" in allE) apply simp apply(erule_tac x="1/2" in allE) by auto }
- thus ?thesis unfolding convex_def cone_def by auto
+ thus ?thesis unfolding convex_def cone_def by blast
qed
lemma affine_dependent_biggerset: fixes s::"(real^'n) set"
@@ -1259,7 +1258,7 @@
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)
+ unfolding open_contains_cball convex_hull_explicit unfolding mem_Collect_eq ball_simps(10)
proof(rule, rule) fix a
assume "\<exists>sa u. finite sa \<and> sa \<subseteq> s \<and> (\<forall>x\<in>sa. 0 \<le> u x) \<and> setsum u sa = 1 \<and> (\<Sum>v\<in>sa. u v *\<^sub>R v) = a"
then obtain t u where obt:"finite t" "t\<subseteq>s" "\<forall>x\<in>t. 0 \<le> u x" "setsum u t = 1" "(\<Sum>v\<in>t. u v *\<^sub>R v) = a" by auto
@@ -1279,7 +1278,7 @@
hence "Min i \<le> b x" unfolding i_def apply(rule_tac Min_le) using obt(1) by auto
hence "x + (y - a) \<in> cball x (b x)" using y unfolding mem_cball dist_norm by auto
moreover from `x\<in>t` have "x\<in>s" using obt(2) by auto
- ultimately have "x + (y - a) \<in> s" using y and b[THEN bspec[where x=x]] unfolding subset_eq by auto }
+ ultimately have "x + (y - a) \<in> s" using y and b[THEN bspec[where x=x]] unfolding subset_eq by fast }
moreover
have *:"inj_on (\<lambda>v. v + (y - a)) t" unfolding inj_on_def by auto
have "(\<Sum>v\<in>(\<lambda>v. v + (y - a)) ` t. u (v - (y - a))) = 1"
@@ -1349,7 +1348,7 @@
show ?thesis unfolding caratheodory[of s]
proof(induct ("CARD('n) + 1"))
have *:"{x.\<exists>sa. finite sa \<and> sa \<subseteq> s \<and> card sa \<le> 0 \<and> x \<in> convex hull sa} = {}"
- using compact_empty by (auto simp add: convex_hull_empty)
+ using compact_empty by auto
case 0 thus ?case unfolding * by simp
next
case (Suc n)
@@ -1359,11 +1358,11 @@
fix x assume "\<exists>t. finite t \<and> t \<subseteq> s \<and> card t \<le> Suc n \<and> x \<in> convex hull t"
then obtain t where t:"finite t" "t \<subseteq> s" "card t \<le> Suc n" "x \<in> convex hull t" by auto
show "x\<in>s" proof(cases "card t = 0")
- case True thus ?thesis using t(4) unfolding card_0_eq[OF t(1)] by(simp add: convex_hull_empty)
+ case True thus ?thesis using t(4) unfolding card_0_eq[OF t(1)] by simp
next
case False hence "card t = Suc 0" using t(3) `n=0` by auto
then obtain a where "t = {a}" unfolding card_Suc_eq by auto
- thus ?thesis using t(2,4) by (simp add: convex_hull_singleton)
+ thus ?thesis using t(2,4) by simp
qed
next
fix x assume "x\<in>s"
@@ -1398,7 +1397,7 @@
show ?P proof(cases "u={}")
case True hence "x=a" using t(4)[unfolded au] by auto
show ?P unfolding `x=a` apply(rule_tac x=a in exI, rule_tac x=a in exI, rule_tac x=1 in exI)
- using t and `n\<noteq>0` unfolding au by(auto intro!: exI[where x="{a}"] simp add: convex_hull_singleton)
+ using t and `n\<noteq>0` unfolding au by(auto intro!: exI[where x="{a}"])
next
case False obtain ux vx b where obt:"ux\<ge>0" "vx\<ge>0" "ux + vx = 1" "b \<in> convex hull u" "x = ux *\<^sub>R a + vx *\<^sub>R b"
using t(4)[unfolded au convex_hull_insert[OF False]] by auto
@@ -1411,7 +1410,7 @@
qed
thus ?thesis using compact_convex_combinations[OF assms Suc] by simp
qed
- qed
+ qed
qed
lemma finite_imp_compact_convex_hull:
@@ -1851,7 +1850,7 @@
lemma convex_hull_scaling:
"convex hull ((\<lambda>x. c *\<^sub>R x) ` s) = (\<lambda>x. c *\<^sub>R x) ` (convex hull s)"
apply(cases "c=0") defer apply(rule convex_hull_bilemma[rule_format, of _ _ inverse]) apply(rule convex_hull_scaling_lemma)
- unfolding image_image scaleR_scaleR by(auto simp add:image_constant_conv convex_hull_eq_empty)
+ unfolding image_image scaleR_scaleR by(auto simp add:image_constant_conv)
lemma convex_hull_affinity:
"convex hull ((\<lambda>x. a + c *\<^sub>R x) ` s) = (\<lambda>x. a + c *\<^sub>R x) ` (convex hull s)"
@@ -2313,7 +2312,7 @@
hence "a < b" unfolding * using as(4) apply(rule_tac mult_left_less_imp_less) by(auto simp add: field_simps)
hence "u * a + v * b \<le> b" unfolding ** using **(2) as(3) by(auto simp add: field_simps intro!:mult_right_mono) }
ultimately show "u *\<^sub>R x + v *\<^sub>R y \<in> s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)])
- using as(3-) dimindex_ge_1 apply- by(auto simp add: vector_component) qed
+ using as(3-) dimindex_ge_1 by auto qed
lemma is_interval_connected:
fixes s :: "(real ^ _) set"
@@ -2336,7 +2335,7 @@
hence *:"dest_vec1 a < dest_vec1 x" "dest_vec1 x < dest_vec1 b" apply(rule_tac [!] ccontr) unfolding not_less by auto
let ?halfl = "{z. inner (basis 1) z < dest_vec1 x} " and ?halfr = "{z. inner (basis 1) z > dest_vec1 x} "
{ fix y assume "y \<in> s" have "y \<in> ?halfr \<union> ?halfl" apply(rule ccontr)
- using as(6) `y\<in>s` by (auto simp add: inner_vector_def dest_vec1_eq) }
+ using as(6) `y\<in>s` by (auto simp add: inner_vector_def) }
moreover have "a\<in>?halfl" "b\<in>?halfr" using * by (auto simp add: inner_vector_def)
hence "?halfl \<inter> s \<noteq> {}" "?halfr \<inter> s \<noteq> {}" using as(2-3) by auto
ultimately show False apply(rule_tac notE[OF as(1)[unfolded connected_def]])
@@ -2374,7 +2373,7 @@
shows "\<exists>x\<in>{a..b}. (f x)$k = y"
apply(subst neg_equal_iff_equal[THEN sym]) unfolding vector_uminus_component[THEN sym]
apply(rule ivt_increasing_component_on_1) using assms using continuous_on_neg
- by(auto simp add:vector_uminus_component)
+ by auto
lemma ivt_decreasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n"
shows "dest_vec1 a \<le> dest_vec1 b \<Longrightarrow> \<forall>x\<in>{a .. b}. continuous (at x) f
@@ -2415,7 +2414,7 @@
unfolding i'(1) xi_def apply(rule_tac Min_le) unfolding image_iff
defer apply(rule_tac x=j in bexI) using i' by auto
have i01:"x$i \<le> 1" "x$i > 0" using Suc(2)[unfolded mem_interval,rule_format,of i] using i'(2) `x$i \<noteq> 0`
- by(auto simp add: Cart_lambda_beta)
+ by auto
show ?thesis proof(cases "x$i=1")
case True have "\<forall>j\<in>{i. x$i \<noteq> 0}. x$j = 1" apply(rule, rule ccontr) unfolding mem_Collect_eq proof-
fix j assume "x $ j \<noteq> 0" "x $ j \<noteq> 1"
@@ -2424,21 +2423,21 @@
hence "x$j \<ge> x$i" unfolding i'(1) xi_def apply(rule_tac Min_le) by auto
thus False using True Suc(2) j by(auto simp add: vector_le_def elim!:ballE[where x=j]) qed
thus "x\<in>convex hull ?points" apply(rule_tac hull_subset[unfolded subset_eq, rule_format])
- by(auto simp add: Cart_lambda_beta)
+ by auto
next let ?y = "\<lambda>j. if x$j = 0 then 0 else (x$j - x$i) / (1 - x$i)"
case False hence *:"x = x$i *\<^sub>R (\<chi> j. if x$j = 0 then 0 else 1) + (1 - x$i) *\<^sub>R (\<chi> j. ?y j)" unfolding Cart_eq
- by(auto simp add: Cart_lambda_beta vector_add_component vector_smult_component vector_minus_component field_simps)
+ by(auto simp add: field_simps)
{ fix j have "x$j \<noteq> 0 \<Longrightarrow> 0 \<le> (x $ j - x $ i) / (1 - x $ i)" "(x $ j - x $ i) / (1 - x $ i) \<le> 1"
apply(rule_tac divide_nonneg_pos) using i(1)[of j] using False i01
- using Suc(2)[unfolded mem_interval, rule_format, of j] by(auto simp add:field_simps Cart_lambda_beta)
+ using Suc(2)[unfolded mem_interval, rule_format, of j] by(auto simp add:field_simps)
hence "0 \<le> ?y j \<and> ?y j \<le> 1" by auto }
- moreover have "i\<in>{j. x$j \<noteq> 0} - {j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0}" using i01 by(auto simp add: Cart_lambda_beta)
+ moreover have "i\<in>{j. x$j \<noteq> 0} - {j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0}" using i01 by auto
hence "{j. x$j \<noteq> 0} \<noteq> {j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0}" by auto
- hence **:"{j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0} \<subset> {j. x$j \<noteq> 0}" apply - apply rule by(auto simp add: Cart_lambda_beta)
+ hence **:"{j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0} \<subset> {j. x$j \<noteq> 0}" apply - apply rule by auto
have "card {j. ((\<chi> j. ?y j)::real^'n) $ j \<noteq> 0} \<le> n" using less_le_trans[OF psubset_card_mono[OF _ **] Suc(4)] by auto
ultimately show ?thesis apply(subst *) apply(rule convex_convex_hull[unfolded convex_def, rule_format])
apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) defer apply(rule Suc(1))
- unfolding mem_interval using i01 Suc(3) by (auto simp add: Cart_lambda_beta)
+ unfolding mem_interval using i01 Suc(3) by auto
qed qed qed } note * = this
show ?thesis apply rule defer apply(rule hull_minimal) unfolding subset_eq prefer 3 apply rule
apply(rule_tac n2="CARD('n)" in *) prefer 3 apply(rule card_mono) using 01 and convex_interval(1) prefer 5 apply - apply rule
@@ -2453,7 +2452,7 @@
prefer 3 apply(rule unit_interval_convex_hull) apply rule unfolding mem_Collect_eq proof-
fix x::"real^'n" assume as:"\<forall>i. x $ i = 0 \<or> x $ i = 1"
show "x \<in> (\<lambda>s. \<chi> i. if i \<in> s then 1 else 0) ` UNIV" apply(rule image_eqI[where x="{i. x$i = 1}"])
- unfolding Cart_eq using as by(auto simp add:Cart_lambda_beta) qed auto
+ unfolding Cart_eq using as by auto qed auto
subsection {* Hence any cube (could do any nonempty interval). *}
@@ -2464,23 +2463,23 @@
unfolding image_iff defer apply(erule bexE) proof-
fix y assume as:"y\<in>{x - ?d .. x + ?d}"
{ fix i::'n have "x $ i \<le> d + y $ i" "y $ i \<le> d + x $ i" using as[unfolded mem_interval, THEN spec[where x=i]]
- by(auto simp add: vector_component)
+ by auto
hence "1 \<ge> inverse d * (x $ i - y $ i)" "1 \<ge> inverse d * (y $ i - x $ i)"
apply(rule_tac[!] mult_left_le_imp_le[OF _ assms]) unfolding mult_assoc[THEN sym]
- using assms by(auto simp add: field_simps right_inverse)
+ using assms by(auto simp add: field_simps)
hence "inverse d * (x $ i * 2) \<le> 2 + inverse d * (y $ i * 2)"
"inverse d * (y $ i * 2) \<le> 2 + inverse d * (x $ i * 2)" by(auto simp add:field_simps) }
hence "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> {0..1}" unfolding mem_interval using assms
- by(auto simp add: Cart_eq vector_component_simps field_simps)
+ by(auto simp add: Cart_eq field_simps)
thus "\<exists>z\<in>{0..1}. y = x - ?d + (2 * d) *\<^sub>R z" apply- apply(rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
- using assms by(auto simp add: Cart_eq vector_le_def Cart_lambda_beta)
+ using assms by(auto simp add: Cart_eq vector_le_def)
next
fix y z assume as:"z\<in>{0..1}" "y = x - ?d + (2*d) *\<^sub>R z"
have "\<And>i. 0 \<le> d * z $ i \<and> d * z $ i \<le> d" using assms as(1)[unfolded mem_interval] apply(erule_tac x=i in allE)
apply rule apply(rule mult_nonneg_nonneg) prefer 3 apply(rule mult_right_le_one_le)
- using assms by(auto simp add: vector_component_simps Cart_eq)
+ using assms by(auto simp add: Cart_eq)
thus "y \<in> {x - ?d..x + ?d}" unfolding as(2) mem_interval apply- apply rule using as(1)[unfolded mem_interval]
- apply(erule_tac x=i in allE) using assms by(auto simp add: vector_component_simps Cart_eq) qed
+ apply(erule_tac x=i in allE) using assms by(auto simp add: Cart_eq) qed
obtain s where "finite s" "{0..1::real^'n} = convex hull s" using unit_cube_convex_hull by auto
thus ?thesis apply(rule_tac that[of "(\<lambda>y. x - ?d + (2 * d) *\<^sub>R y)` s"]) unfolding * and convex_hull_affinity by auto qed
@@ -2570,8 +2569,8 @@
have "0 < d" unfolding d_def using `e>0` dimge1 by(rule_tac divide_pos_pos, auto)
let ?d = "(\<chi> i. d)::real^'n"
obtain c where c:"finite c" "{x - ?d..x + ?d} = convex hull c" using cube_convex_hull[OF `d>0`, of x] by auto
- have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by(auto simp add:vector_component_simps)
- hence "c\<noteq>{}" using c by(auto simp add:convex_hull_empty)
+ have "x\<in>{x - ?d..x + ?d}" using `d>0` unfolding mem_interval by auto
+ hence "c\<noteq>{}" using c by auto
def k \<equiv> "Max (f ` c)"
have "convex_on {x - ?d..x + ?d} f" apply(rule convex_on_subset[OF assms(2)])
apply(rule subset_trans[OF _ e(1)]) unfolding subset_eq mem_cball proof
@@ -2579,7 +2578,7 @@
have e:"e = setsum (\<lambda>i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1
by (metis eq_divide_imp mult_frac_num real_dimindex_gt_0 real_eq_of_nat real_less_def real_mult_commute)
show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
- using z[unfolded mem_interval] apply(erule_tac x=i in allE) by(auto simp add:field_simps vector_component_simps) qed
+ using z[unfolded mem_interval] apply(erule_tac x=i in allE) by auto qed
hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption
unfolding k_def apply(rule, rule Max_ge) using c(1) by auto
have "d \<le> e" unfolding d_def apply(rule mult_imp_div_pos_le) using `e>0` dimge1 unfolding mult_le_cancel_left1 using real_dimindex_ge_1 by auto
@@ -2588,9 +2587,9 @@
hence "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)" apply(rule_tac convex_bounds_lemma) apply assumption proof
fix y assume y:"y\<in>cball x d"
{ fix i::'n have "x $ i - d \<le> y $ i" "y $ i \<le> x $ i + d"
- using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by(auto simp add: vector_component) }
+ using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by auto }
thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm
- by(auto simp add: vector_component_simps) qed
+ by auto qed
hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous)
apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball)
apply force
@@ -2716,17 +2715,17 @@
unfolding as(1) by(auto simp add:algebra_simps)
show "norm (a - x) *\<^sub>R (x - b) = norm (x - b) *\<^sub>R (a - x)"
unfolding norm_minus_commute[of x a] * Cart_eq using as(2,3)
- by(auto simp add: vector_component_simps field_simps)
+ by(auto simp add: field_simps)
next assume as:"dist a b = dist a x + dist x b"
have "norm (a - x) / norm (a - b) \<le> 1" unfolding divide_le_eq_1_pos[OF Fal2] unfolding as[unfolded dist_norm] norm_ge_zero by auto
thus "\<exists>u. x = (1 - u) *\<^sub>R a + u *\<^sub>R b \<and> 0 \<le> u \<and> u \<le> 1" apply(rule_tac x="dist a x / dist a b" in exI)
unfolding dist_norm Cart_eq apply- apply rule defer apply(rule, rule divide_nonneg_pos) prefer 4 proof rule
fix i::'n have "((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $ i =
((norm (a - b) - norm (a - x)) * (a $ i) + norm (a - x) * (b $ i)) / norm (a - b)"
- using Fal by(auto simp add:vector_component_simps field_simps)
+ using Fal by(auto simp add: field_simps)
also have "\<dots> = x$i" apply(rule divide_eq_imp[OF Fal])
unfolding as[unfolded dist_norm] using as[unfolded dist_triangle_eq Cart_eq,rule_format, of i]
- by(auto simp add:field_simps vector_component_simps)
+ by(auto simp add:field_simps)
finally show "x $ i = ((1 - norm (a - x) / norm (a - b)) *\<^sub>R a + (norm (a - x) / norm (a - b)) *\<^sub>R b) $ i" by auto
qed(insert Fal2, auto) qed qed
@@ -2735,7 +2734,7 @@
"between (b,a) (midpoint a b)" (is ?t2)
proof- have *:"\<And>x y z. x = (1/2::real) *\<^sub>R z \<Longrightarrow> y = (1/2) *\<^sub>R z \<Longrightarrow> norm z = norm x + norm y" by auto
show ?t1 ?t2 unfolding between midpoint_def dist_norm apply(rule_tac[!] *)
- by(auto simp add:field_simps Cart_eq vector_component_simps) qed
+ by(auto simp add:field_simps Cart_eq) qed
lemma between_mem_convex_hull:
"between (a,b) x \<longleftrightarrow> x \<in> convex hull {a,b}"
@@ -2754,7 +2753,7 @@
have *:"y = (1 - (1 - e)) *\<^sub>R ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) + (1 - e) *\<^sub>R x" using `e>0` by (auto simp add: scaleR_left_diff_distrib scaleR_right_diff_distrib)
have "dist c ((1 / e) *\<^sub>R y - ((1 - e) / e) *\<^sub>R x) = abs(1/e) * norm (e *\<^sub>R c - y + (1 - e) *\<^sub>R x)"
unfolding dist_norm unfolding norm_scaleR[THEN sym] apply(rule norm_eqI) using `e>0`
- by(auto simp add:vector_component_simps Cart_eq field_simps)
+ by(auto simp add: Cart_eq field_simps)
also have "\<dots> = abs(1/e) * norm (x - e *\<^sub>R (x - c) - y)" by(auto intro!:norm_eqI simp add: algebra_simps)
also have "\<dots> < d" using as[unfolded dist_norm] and `e>0`
by(auto simp add:pos_divide_less_eq[OF `e>0`] real_mult_commute)
@@ -2826,11 +2825,11 @@
fix x::"real^'n" and e assume "0<e" and as:"\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x. 0 \<le> xa $ x) \<and> setsum (op $ xa) UNIV \<le> 1"
show "(\<forall>xa. 0 < x $ xa) \<and> setsum (op $ x) UNIV < 1" apply(rule,rule) proof-
fix i::'n show "0 < x $ i" using as[THEN spec[where x="x - (e / 2) *\<^sub>R basis i"]] and `e>0`
- unfolding dist_norm by(auto simp add: norm_basis vector_component_simps basis_component elim:allE[where x=i])
+ unfolding dist_norm by(auto simp add: norm_basis elim:allE[where x=i])
next guess a using UNIV_witness[where 'a='n] ..
have **:"dist x (x + (e / 2) *\<^sub>R basis a) < e" using `e>0` and norm_basis[of a]
- unfolding dist_norm by(auto simp add: vector_component_simps basis_component intro!: mult_strict_left_mono_comm)
- have "\<And>i. (x + (e / 2) *\<^sub>R basis a) $ i = x$i + (if i = a then e/2 else 0)" by(auto simp add:vector_component_simps)
+ unfolding dist_norm by(auto intro!: mult_strict_left_mono_comm)
+ have "\<And>i. (x + (e / 2) *\<^sub>R basis a) $ i = x$i + (if i = a then e/2 else 0)" by auto
hence *:"setsum (op $ (x + (e / 2) *\<^sub>R basis a)) UNIV = setsum (\<lambda>i. x$i + (if a = i then e/2 else 0)) UNIV" by(rule_tac setsum_cong, auto)
have "setsum (op $ x) UNIV < setsum (op $ (x + (e / 2) *\<^sub>R basis a)) UNIV" unfolding * setsum_addf
using `0<e` dimindex_ge_1 by(auto simp add: setsum_delta')
@@ -2847,13 +2846,13 @@
fix y assume y:"dist x y < min (Min (op $ x ` UNIV)) ?d"
have "setsum (op $ y) UNIV \<le> setsum (\<lambda>i. x$i + ?d) UNIV" proof(rule setsum_mono)
fix i::'n have "abs (y$i - x$i) < ?d" apply(rule le_less_trans) using component_le_norm[of "y - x" i]
- using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add:vector_component_simps norm_minus_commute)
+ using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add: norm_minus_commute)
thus "y $ i \<le> x $ i + ?d" by auto qed
also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat using dimindex_ge_1 by(auto simp add: Suc_le_eq)
finally show "(\<forall>i. 0 \<le> y $ i) \<and> setsum (op $ y) UNIV \<le> 1" apply- proof(rule,rule)
fix i::'n have "norm (x - y) < x$i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
- using Min_gr_iff[of "op $ x ` dimset x"] dimindex_ge_1 by auto
- thus "0 \<le> y$i" using component_le_norm[of "x - y" i] and as(1)[rule_format, of i] by(auto simp add: vector_component_simps)
+ by auto
+ thus "0 \<le> y$i" using component_le_norm[of "x - y" i] and as(1)[rule_format, of i] by auto
qed auto qed auto qed
lemma interior_std_simplex_nonempty: obtains a::"real^'n" where
@@ -3040,9 +3039,6 @@
apply(erule_tac x="1-x" in ballE, erule_tac x="1-y" in ballE)
unfolding mem_interval_1 by auto
-(** move this **)
-declare vector_scaleR_component[simp]
-
lemma simple_path_join_loop:
assumes "injective_path g1" "injective_path g2" "pathfinish g2 = pathstart g1"
"(path_image g1 \<inter> path_image g2) \<subseteq> {pathstart g1,pathstart g2}"
@@ -3390,7 +3386,7 @@
hence "\<psi> k \<noteq> \<psi> (Suc k)" using \<psi>[unfolded bij_betw_def inj_on_def, THEN conjunct1, THEN bspec[where x=k]] by auto
hence **:"?basis k + ?basis (Suc k) \<in> {x. 0 < inner (?basis (Suc k)) x} \<inter> (?A k)"
"?basis k - ?basis (Suc k) \<in> {x. 0 > inner (?basis (Suc k)) x} \<inter> ({x. 0 < inner (?basis (Suc k)) x} \<union> (?A k))" using d
- by(auto simp add: inner_basis vector_component_simps intro!:bexI[where x=k])
+ by(auto simp add: inner_basis intro!:bexI[where x=k])
show ?thesis unfolding * Un_assoc apply(rule path_connected_Un) defer apply(rule path_connected_Un)
prefer 5 apply(rule_tac[1-2] convex_imp_path_connected, rule convex_halfspace_lt, rule convex_halfspace_gt)
apply(rule Suc(1)) using d ** False by auto
@@ -3404,7 +3400,7 @@
apply(rule_tac[5] x=" ?basis 1 + ?basis 2" in nequals0I)
apply(rule_tac[6] x="-?basis 1 + ?basis 2" in nequals0I)
apply(rule_tac[7] x="-?basis 1 - ?basis 2" in nequals0I)
- using d unfolding *** by(auto intro!: convex_halfspace_gt convex_halfspace_lt, auto simp add:vector_component_simps inner_basis)
+ using d unfolding *** by(auto intro!: convex_halfspace_gt convex_halfspace_lt, auto simp add: inner_basis)
qed qed auto qed note lem = this
have ***:"\<And>x::real^'n. (\<exists>i\<in>{1..CARD('n)}. inner (basis (\<psi> i)) x \<noteq> 0) \<longleftrightarrow> (\<exists>i. inner (basis i) x \<noteq> 0)"
@@ -3432,7 +3428,7 @@
apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
apply(rule continuous_at_norm[unfolded o_def]) by auto
thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms]
- by(auto intro!: path_connected_continuous_image continuous_on_intros continuous_on_mul) qed
+ by(auto intro!: path_connected_continuous_image continuous_on_intros) qed
lemma connected_sphere: "2 \<le> CARD('n) \<Longrightarrow> connected {x::real^'n. norm(x - a) = r}"
using path_connected_sphere path_connected_imp_connected by auto
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Mon Apr 26 16:08:04 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon Apr 26 09:45:22 2010 -0700
@@ -94,7 +94,7 @@
subsection {* Derivatives on real = Derivatives on @{typ "real^1"} *}
-lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding vector_dist_norm by(auto simp add:vec1_dest_vec1_simps)
+lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding vector_dist_norm by auto
lemma bounded_linear_vec1_dest_vec1: fixes f::"real \<Rightarrow> real"
shows "linear (vec1 \<circ> f \<circ> dest_vec1) = bounded_linear f" (is "?l = ?r") proof-
@@ -282,6 +282,8 @@
subsection {* differentiability. *}
+no_notation Deriv.differentiable (infixl "differentiable" 60)
+
definition differentiable :: "('a::real_normed_vector \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a net \<Rightarrow> bool" (infixr "differentiable" 30) where
"f differentiable net \<equiv> (\<exists>f'. (f has_derivative f') net)"
@@ -755,11 +757,11 @@
lemma onorm_vec1: fixes f::"real \<Rightarrow> real"
shows "onorm (\<lambda>x. vec1 (f (dest_vec1 x))) = onorm f" proof-
have "\<forall>x::real^1. norm x = 1 \<longleftrightarrow> x\<in>{vec1 -1, vec1 (1::real)}" unfolding forall_vec1 by(auto simp add:Cart_eq)
- hence 1:"{x. norm x = 1} = {vec1 -1, vec1 (1::real)}" by(auto simp add:norm_vec1)
+ hence 1:"{x. norm x = 1} = {vec1 -1, vec1 (1::real)}" by auto
have 2:"{norm (vec1 (f (dest_vec1 x))) |x. norm x = 1} = (\<lambda>x. norm (vec1 (f (dest_vec1 x)))) ` {x. norm x=1}" by auto
have "\<forall>x::real. norm x = 1 \<longleftrightarrow> x\<in>{-1, 1}" by auto hence 3:"{x. norm x = 1} = {-1, (1::real)}" by auto
have 4:"{norm (f x) |x. norm x = 1} = (\<lambda>x. norm (f x)) ` {x. norm x=1}" by auto
- show ?thesis unfolding onorm_def 1 2 3 4 by(simp add:Sup_finite_Max norm_vec1) qed
+ show ?thesis unfolding onorm_def 1 2 3 4 by(simp add:Sup_finite_Max) qed
lemma differentiable_bound_real: fixes f::"real \<Rightarrow> real"
assumes "convex s" "\<forall>x\<in>s. (f has_derivative f' x) (at x within s)" "\<forall>x\<in>s. onorm(f' x) \<le> B" and x:"x\<in>s" and y:"y\<in>s"
@@ -1014,7 +1016,7 @@
unfolding ph' * apply(rule diff_chain_within) defer apply(rule bounded_linear.has_derivative[OF assms(3)])
apply(rule has_derivative_intros) defer apply(rule has_derivative_sub[where g'="\<lambda>x.0",unfolded diff_0_right])
apply(rule has_derivative_at_within) using assms(5) and `u\<in>s` `a\<in>s`
- by(auto intro!: has_derivative_intros derivative_linear)
+ by(auto intro!: has_derivative_intros derivative_linear)
have **:"bounded_linear (\<lambda>x. f' u x - f' a x)" "bounded_linear (\<lambda>x. f' a x - f' u x)" apply(rule_tac[!] bounded_linear_sub)
apply(rule_tac[!] derivative_linear) using assms(5) `u\<in>s` `a\<in>s` by auto
have "onorm (\<lambda>v. v - g' (f' u v)) \<le> onorm g' * onorm (\<lambda>w. f' a w - f' u w)" unfolding * apply(rule onorm_compose)
--- a/src/HOL/Multivariate_Analysis/Determinants.thy Mon Apr 26 16:08:04 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Mon Apr 26 09:45:22 2010 -0700
@@ -813,7 +813,7 @@
lemma cramer:
fixes A ::"real^'n^'n"
assumes d0: "det A \<noteq> 0"
- shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j :: real^'n^'n) / det A)"
+ shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j) / det A)"
proof-
from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1"
unfolding invertible_det_nz[symmetric] invertible_def by blast
@@ -821,7 +821,7 @@
hence "A *v (B *v b) = b" by (simp add: matrix_vector_mul_assoc)
then have xe: "\<exists>x. A*v x = b" by blast
{fix x assume x: "A *v x = b"
- have "x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j :: real^'n^'n) / det A)"
+ have "x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j) / det A)"
unfolding x[symmetric]
using d0 by (simp add: Cart_eq cramer_lemma field_simps)}
with xe show ?thesis by auto
@@ -993,15 +993,15 @@
moreover
{assume "x = 0" "y \<noteq> 0"
then have "dist (?g x) (?g y) = dist x y"
- apply (simp add: dist_norm norm_mul)
+ apply (simp add: dist_norm)
apply (rule f1[rule_format])
- by(simp add: norm_mul field_simps)}
+ by(simp add: field_simps)}
moreover
{assume "x \<noteq> 0" "y = 0"
then have "dist (?g x) (?g y) = dist x y"
- apply (simp add: dist_norm norm_mul)
+ apply (simp add: dist_norm)
apply (rule f1[rule_format])
- by(simp add: norm_mul field_simps)}
+ by(simp add: field_simps)}
moreover
{assume z: "x \<noteq> 0" "y \<noteq> 0"
have th00: "x = norm x *s (inverse (norm x) *s x)" "y = norm y *s (inverse (norm y) *s y)" "norm x *s f ((inverse (norm x) *s x)) = norm x *s f (inverse (norm x) *s x)"
@@ -1013,7 +1013,7 @@
"norm (f (inverse (norm x) *s x) - f (inverse (norm y) *s y)) =
norm (inverse (norm x) *s x - inverse (norm y) *s y)"
using z
- by (auto simp add: vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
+ by (auto simp add: vector_smult_assoc field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
by (simp add: dist_norm)}
ultimately have "dist (?g x) (?g y) = dist x y" by blast}
@@ -1047,7 +1047,7 @@
by (simp add: nat_number setprod_numseg mult_commute)
lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
- by (simp add: det_def permutes_sing sign_id UNIV_1)
+ by (simp add: det_def sign_id UNIV_1)
lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1"
proof-
@@ -1057,7 +1057,7 @@
unfolding setsum_over_permutations_insert[OF f12]
unfolding permutes_sing
apply (simp add: sign_swap_id sign_id swap_id_eq)
- by (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31))
+ by (simp add: arith_simps(31)[symmetric] del: arith_simps(31))
qed
lemma det_3: "det (A::'a::comm_ring_1^3^3) =
@@ -1078,7 +1078,7 @@
unfolding permutes_sing
apply (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)
- apply (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31))
+ apply (simp add: arith_simps(31)[symmetric] del: arith_simps(31))
by (simp add: field_simps)
qed
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Apr 26 16:08:04 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Apr 26 09:45:22 2010 -0700
@@ -670,7 +670,7 @@
subsection{* The collapse of the general concepts to dimension one. *}
lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))"
- by (simp add: Cart_eq forall_1)
+ by (simp add: Cart_eq)
lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
apply auto
@@ -775,8 +775,7 @@
lemma sqrt_even_pow2: assumes n: "even n"
shows "sqrt(2 ^ n) = 2 ^ (n div 2)"
proof-
- from n obtain m where m: "n = 2*m" unfolding even_nat_equiv_def2
- by (auto simp add: nat_number)
+ from n obtain m where m: "n = 2*m" unfolding even_mult_two_ex ..
from m have "sqrt(2 ^ n) = sqrt ((2 ^ m) ^ 2)"
by (simp only: power_mult[symmetric] mult_commute)
then show ?thesis using m by simp
@@ -785,7 +784,7 @@
lemma real_div_sqrt: "0 <= x ==> x / sqrt(x) = sqrt(x)"
apply (cases "x = 0", simp_all)
using sqrt_divide_self_eq[of x]
- apply (simp add: inverse_eq_divide real_sqrt_ge_0_iff field_simps)
+ apply (simp add: inverse_eq_divide field_simps)
done
text{* Hence derive more interesting properties of the norm. *}
@@ -798,8 +797,8 @@
by (rule norm_zero)
lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x"
- by (simp add: norm_vector_def vector_component setL2_right_distrib
- abs_mult cong: strong_setL2_cong)
+ by (simp add: norm_vector_def setL2_right_distrib abs_mult)
+
lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (inner x x = (0::real))"
by (simp add: norm_vector_def setL2_def power2_eq_square)
lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
@@ -866,10 +865,14 @@
by (auto simp add: norm_eq_sqrt_inner)
lemma real_abs_le_square_iff: "\<bar>x\<bar> \<le> \<bar>y\<bar> \<longleftrightarrow> (x::real)^2 \<le> y^2"
-proof-
- have "x^2 \<le> y^2 \<longleftrightarrow> (x -y) * (y + x) \<le> 0" by (simp add: field_simps power2_eq_square)
- also have "\<dots> \<longleftrightarrow> \<bar>x\<bar> \<le> \<bar>y\<bar>" apply (simp add: zero_compare_simps real_abs_def not_less) by arith
-finally show ?thesis ..
+proof
+ assume "\<bar>x\<bar> \<le> \<bar>y\<bar>"
+ then have "\<bar>x\<bar>\<twosuperior> \<le> \<bar>y\<bar>\<twosuperior>" by (rule power_mono, simp)
+ then show "x\<twosuperior> \<le> y\<twosuperior>" by simp
+next
+ assume "x\<twosuperior> \<le> y\<twosuperior>"
+ then have "sqrt (x\<twosuperior>) \<le> sqrt (y\<twosuperior>)" by (rule real_sqrt_le_mono)
+ then show "\<bar>x\<bar> \<le> \<bar>y\<bar>" by simp
qed
lemma norm_le_square: "norm(x) <= a \<longleftrightarrow> 0 <= a \<and> x \<bullet> x <= a^2"
@@ -1179,7 +1182,7 @@
assumes fS: "finite S"
shows "setsum f S *s v = setsum (\<lambda>x. f x *s v) S"
proof(induct rule: finite_induct[OF fS])
- case 1 then show ?case by (simp add: vector_smult_lzero)
+ case 1 then show ?case by simp
next
case (2 x F)
from "2.hyps" have "setsum f (insert x F) *s v = (f x + setsum f F) *s v"
@@ -1398,7 +1401,7 @@
apply (subgoal_tac "vector [v$1] = v")
apply simp
apply (vector vector_def)
- apply (simp add: forall_1)
+ apply simp
done
lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
@@ -1536,7 +1539,7 @@
unfolding norm_mul
apply (simp only: mult_commute)
apply (rule mult_mono)
- by (auto simp add: field_simps norm_ge_zero) }
+ by (auto simp add: field_simps) }
then have th: "\<forall>i\<in> ?S. norm ((x$i) *s f (basis i :: real ^'m)) \<le> norm (f (basis i)) * norm x" by metis
from real_setsum_norm_le[OF fS, of "\<lambda>i. (x$i) *s (f (basis i))", OF th]
have "norm (f x) \<le> ?B * norm x" unfolding th0 setsum_left_distrib by metis}
@@ -1553,9 +1556,9 @@
let ?K = "\<bar>B\<bar> + 1"
have Kp: "?K > 0" by arith
{assume C: "B < 0"
- have "norm (1::real ^ 'n) > 0" by (simp add: zero_less_norm_iff)
+ have "norm (1::real ^ 'n) > 0" by simp
with C have "B * norm (1:: real ^ 'n) < 0"
- by (simp add: zero_compare_simps)
+ by (simp add: mult_less_0_iff)
with B[rule_format, of 1] norm_ge_zero[of "f 1"] have False by simp
}
then have Bp: "B \<ge> 0" by ferrack
@@ -1677,11 +1680,11 @@
apply (rule real_setsum_norm_le)
using fN fM
apply simp
- apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] norm_mul field_simps)
+ apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] field_simps)
apply (rule mult_mono)
- apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
+ apply (auto simp add: zero_le_mult_iff component_le_norm)
apply (rule mult_mono)
- apply (auto simp add: norm_ge_zero zero_le_mult_iff component_le_norm)
+ apply (auto simp add: zero_le_mult_iff component_le_norm)
done}
then show ?thesis by metis
qed
@@ -1701,7 +1704,7 @@
have "B * norm x * norm y \<le> ?K * norm x * norm y"
apply -
apply (rule mult_right_mono, rule mult_right_mono)
- by (auto simp add: norm_ge_zero)
+ by auto
then have "norm (h x y) \<le> ?K * norm x * norm y"
using B[rule_format, of x y] by simp}
with Kp show ?thesis by blast
@@ -2006,8 +2009,8 @@
have uv': "u = 0 \<longrightarrow> v \<noteq> 0" using u v uv by arith
have "a = a * (u + v)" unfolding uv by simp
hence th: "u * a + v * a = a" by (simp add: field_simps)
- from xa u have "u \<noteq> 0 \<Longrightarrow> u*x < u*a" by (simp add: mult_compare_simps)
- from ya v have "v \<noteq> 0 \<Longrightarrow> v * y < v * a" by (simp add: mult_compare_simps)
+ from xa u have "u \<noteq> 0 \<Longrightarrow> u*x < u*a" by (simp add: mult_strict_left_mono)
+ from ya v have "v \<noteq> 0 \<Longrightarrow> v * y < v * a" by (simp add: mult_strict_left_mono)
from xa ya u v have "u * x + v * y < u * a + v * a"
apply (cases "u = 0", simp_all add: uv')
apply(rule mult_strict_left_mono)
@@ -2048,7 +2051,7 @@
assumes x: "0 <= (x::real)" and y:"0 <= y" and z: "0 <= z" and xy: "x^2 <= y^2 + z^2"
shows "x <= y + z"
proof-
- have "y^2 + z^2 \<le> y^2 + 2*y*z + z^2" using z y by (simp add: zero_compare_simps)
+ have "y^2 + z^2 \<le> y^2 + 2*y*z + z^2" using z y by (simp add: mult_nonneg_nonneg)
with xy have th: "x ^2 \<le> (y+z)^2" by (simp add: power2_eq_square field_simps)
from y z have yz: "y + z \<ge> 0" by arith
from power2_le_imp_le[OF th yz] show ?thesis .
@@ -2100,10 +2103,10 @@
{assume x0: "x \<noteq> 0"
hence n0: "norm x \<noteq> 0" by (metis norm_eq_zero)
let ?c = "1/ norm x"
- have "norm (?c*s x) = 1" using x0 by (simp add: n0 norm_mul)
+ have "norm (?c*s x) = 1" using x0 by (simp add: n0)
with H have "norm (f(?c*s x)) \<le> b" by blast
hence "?c * norm (f x) \<le> b"
- by (simp add: linear_cmul[OF lf] norm_mul)
+ by (simp add: linear_cmul[OF lf])
hence "norm (f x) \<le> b * norm x"
using n0 norm_ge_zero[of x] by (auto simp add: field_simps)}
ultimately have "norm (f x) \<le> b * norm x" by blast}
@@ -2221,18 +2224,24 @@
where "dest_vec1 x \<equiv> (x$1)"
lemma vec1_component[simp]: "(vec1 x)$1 = x"
- by (simp add: )
-
-lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
- by (simp_all add: Cart_eq forall_1)
-
-lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))" by (metis vec1_dest_vec1)
-
-lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))" by (metis vec1_dest_vec1)
-
-lemma vec1_eq[simp]: "vec1 x = vec1 y \<longleftrightarrow> x = y" by (metis vec1_dest_vec1)
-
-lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y" by (metis vec1_dest_vec1)
+ by simp
+
+lemma vec1_dest_vec1: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
+ by (simp_all add: Cart_eq)
+
+declare vec1_dest_vec1(1) [simp]
+
+lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
+ by (metis vec1_dest_vec1(1))
+
+lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))"
+ by (metis vec1_dest_vec1(1))
+
+lemma vec1_eq[simp]: "vec1 x = vec1 y \<longleftrightarrow> x = y"
+ by (metis vec1_dest_vec1(2))
+
+lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y"
+ by (metis vec1_dest_vec1(1))
lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto
@@ -2260,8 +2269,8 @@
lemma dest_vec1_sum: assumes fS: "finite S"
shows "dest_vec1(setsum f S) = setsum (dest_vec1 o f) S"
apply (induct rule: finite_induct[OF fS])
- apply (simp add: dest_vec1_vec)
- apply (auto simp add:vector_minus_component)
+ apply simp
+ apply auto
done
lemma norm_vec1: "norm(vec1 x) = abs(x)"
@@ -2270,7 +2279,7 @@
lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
by (simp only: dist_real vec1_component)
lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
- by (metis vec1_dest_vec1 norm_vec1)
+ by (metis vec1_dest_vec1(1) norm_vec1)
lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component
vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def
@@ -2298,7 +2307,7 @@
shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
apply (rule ext)
apply (subst matrix_works[OF lf, symmetric])
- apply (simp add: Cart_eq matrix_vector_mult_def row_def inner_vector_def mult_commute forall_1)
+ apply (simp add: Cart_eq matrix_vector_mult_def row_def inner_vector_def mult_commute)
done
lemma dest_vec1_eq_0: "dest_vec1 x = 0 \<longleftrightarrow> x = 0"
@@ -2366,13 +2375,13 @@
by (induct rule: finite_induct[OF fS], simp_all add: vec_0[symmetric] del: vec_0)
lemma pastecart_vec[simp]: "pastecart (vec x) (vec x) = vec x"
- by (simp add: pastecart_eq fstcart_pastecart sndcart_pastecart)
+ by (simp add: pastecart_eq)
lemma pastecart_add[simp]:"pastecart (x1::'a::{plus,times}^_) y1 + pastecart x2 y2 = pastecart (x1 + x2) (y1 + y2)"
- by (simp add: pastecart_eq fstcart_pastecart sndcart_pastecart)
+ by (simp add: pastecart_eq)
lemma pastecart_cmul[simp]: "pastecart (c *s (x1::'a::{plus,times}^_)) (c *s y1) = c *s pastecart x1 y1"
- by (simp add: pastecart_eq fstcart_pastecart sndcart_pastecart)
+ by (simp add: pastecart_eq)
lemma pastecart_neg[simp]: "pastecart (- (x::'a::ring_1^_)) (- y) = - pastecart x y"
unfolding vector_sneg_minus1 pastecart_cmul ..
@@ -2384,7 +2393,7 @@
fixes f:: "'d \<Rightarrow> 'a::semiring_1^_"
assumes fS: "finite S"
shows "pastecart (setsum f S) (setsum g S) = setsum (\<lambda>i. pastecart (f i) (g i)) S"
- by (simp add: pastecart_eq fstcart_setsum[OF fS] sndcart_setsum[OF fS] fstcart_pastecart sndcart_pastecart)
+ by (simp add: pastecart_eq fstcart_setsum[OF fS] sndcart_setsum[OF fS])
lemma setsum_Plus:
"\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow>
@@ -2402,7 +2411,7 @@
lemma norm_fstcart: "norm(fstcart x) <= norm (x::real ^('n::finite + 'm::finite))"
proof-
have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))"
- by (simp add: pastecart_fst_snd)
+ by simp
have th1: "fstcart x \<bullet> fstcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)"
by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def setsum_nonneg)
then show ?thesis
@@ -2417,7 +2426,7 @@
lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n::finite + 'm::finite))"
proof-
have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))"
- by (simp add: pastecart_fst_snd)
+ by simp
have th1: "sndcart x \<bullet> sndcart x \<le> pastecart (fstcart x) (sndcart x) \<bullet> pastecart (fstcart x) (sndcart x)"
by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def setsum_nonneg)
then show ?thesis
@@ -2519,7 +2528,7 @@
lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
using reals_Archimedean
- apply (auto simp add: field_simps inverse_positive_iff_positive)
+ apply (auto simp add: field_simps)
apply (subgoal_tac "inverse (real n) > 0")
apply arith
apply simp
@@ -2732,7 +2741,8 @@
"0 \<in> span S"
"x\<in> span S \<Longrightarrow> y \<in> span S ==> x + y \<in> span S"
"x \<in> span S \<Longrightarrow> c *s x \<in> span S"
- by (metis span_def hull_subset subset_eq subspace_span subspace_def)+
+ by (metis span_def hull_subset subset_eq)
+ (metis subspace_span subspace_def)+
lemma span_induct: assumes SP: "\<And>x. x \<in> S ==> P x"
and P: "subspace P" and x: "x \<in> span S" shows "P x"
@@ -2830,7 +2840,7 @@
(* Individual closure properties. *)
-lemma span_superset: "x \<in> S ==> x \<in> span S" by (metis span_clauses)
+lemma span_superset: "x \<in> S ==> x \<in> span S" by (metis span_clauses(1))
lemma span_0: "0 \<in> span S" by (metis subspace_span subspace_0)
@@ -2847,8 +2857,7 @@
by (metis subspace_span subspace_sub)
lemma span_setsum: "finite A \<Longrightarrow> \<forall>x \<in> A. f x \<in> span S ==> setsum f A \<in> span S"
- apply (rule subspace_setsum)
- by (metis subspace_span subspace_setsum)+
+ by (rule subspace_setsum, rule subspace_span)
lemma span_add_eq: "(x::'a::ring_1^_) \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
apply (auto simp only: span_add span_sub)
@@ -3110,7 +3119,7 @@
from fS SP aP have th0: "finite ?S" "?S \<subseteq> P" "?v \<in> ?S" "?u ?v \<noteq> 0" by auto
have s0: "setsum (\<lambda>v. ?u v *s v) ?S = 0"
using fS aS
- apply (simp add: vector_smult_lneg vector_smult_lid setsum_clauses field_simps )
+ apply (simp add: vector_smult_lneg setsum_clauses field_simps)
apply (subst (2) ua[symmetric])
apply (rule setsum_cong2)
by auto
@@ -3479,7 +3488,7 @@
lemma basis_card_eq_dim:
"B \<subseteq> (V:: (real ^'n) set) \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> finite B \<and> card B = dim V"
- by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_mono independent_bound)
+ by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_bound)
lemma dim_unique: "(B::(real ^'n) set) \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> card B = n \<Longrightarrow> dim V = n"
by (metis basis_card_eq_dim)
@@ -3669,7 +3678,7 @@
apply (subst Cy)
using C(1) fth
apply (simp only: setsum_clauses) unfolding smult_conv_scaleR
- apply (auto simp add: inner_simps inner_eq_zero_iff inner_commute[of y a] dot_lsum[OF fth])
+ apply (auto simp add: inner_simps inner_commute[of y a] dot_lsum[OF fth])
apply (rule setsum_0')
apply clarsimp
apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
@@ -3686,7 +3695,7 @@
using C(1) fth
apply (simp only: setsum_clauses) unfolding smult_conv_scaleR
apply (subst inner_commute[of x])
- apply (auto simp add: inner_simps inner_eq_zero_iff inner_commute[of x a] dot_rsum[OF fth])
+ apply (auto simp add: inner_simps inner_commute[of x a] dot_rsum[OF fth])
apply (rule setsum_0')
apply clarsimp
apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
@@ -3759,10 +3768,10 @@
apply (subst B') using fB fth
unfolding setsum_clauses(2)[OF fth]
apply simp unfolding inner_simps smult_conv_scaleR
- apply (clarsimp simp add: inner_simps inner_eq_zero_iff smult_conv_scaleR dot_lsum)
+ apply (clarsimp simp add: inner_simps smult_conv_scaleR dot_lsum)
apply (rule setsum_0', rule ballI)
unfolding inner_commute
- by (auto simp add: x field_simps inner_eq_zero_iff intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])}
+ by (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])}
then show "\<forall>x \<in> B. ?a \<bullet> x = 0" by blast
qed
with a0 show ?thesis unfolding sSB by (auto intro: exI[where x="?a"])
@@ -3915,7 +3924,7 @@
{assume xb: "x \<in> b"
have h0: "0 = ?h x"
apply (rule conjunct2[OF h, rule_format])
- apply (metis span_superset insertI1 xb x)
+ apply (metis span_superset x)
apply simp
apply (metis span_superset xb)
done
@@ -4262,8 +4271,7 @@
{fix y have "?P y"
proof(rule span_induct_alt[of ?P "columns A"])
show "\<exists>x\<Colon>real ^ 'm. setsum (\<lambda>i. (x$i) *s column i A) ?U = 0"
- apply (rule exI[where x=0])
- by (simp add: zero_index vector_smult_lzero)
+ by (rule exI[where x=0], simp)
next
fix c y1 y2 assume y1: "y1 \<in> columns A" and y2: "?P y2"
from y1 obtain i where i: "i \<in> ?U" "y1 = column i A"
@@ -4687,7 +4695,7 @@
hence d2: "(sqrt (real ?d))^2 = real ?d"
by (auto intro: real_sqrt_pow2)
have th: "sqrt (real ?d) * infnorm x \<ge> 0"
- by (simp add: zero_le_mult_iff real_sqrt_ge_0_iff infnorm_pos_le)
+ by (simp add: zero_le_mult_iff infnorm_pos_le)
have th1: "x \<bullet> x \<le> (sqrt (real ?d) * infnorm x)^2"
unfolding power_mult_distrib d2
unfolding real_of_nat_def inner_vector_def
@@ -4861,4 +4869,3 @@
done
end
-
\ No newline at end of file
--- a/src/HOL/Multivariate_Analysis/Integration.thy Mon Apr 26 16:08:04 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon Apr 26 09:45:22 2010 -0700
@@ -933,7 +933,7 @@
lemma has_integral_vec1: assumes "(f has_integral k) {a..b}"
shows "((\<lambda>x. vec1 (f x)) has_integral (vec1 k)) {a..b}"
proof- have *:"\<And>p. (\<Sum>(x, k)\<in>p. content k *\<^sub>R vec1 (f x)) - vec1 k = vec1 ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k)"
- unfolding vec_sub Cart_eq by(auto simp add:vec1_dest_vec1_simps split_beta)
+ unfolding vec_sub Cart_eq by(auto simp add: split_beta)
show ?thesis using assms unfolding has_integral apply safe
apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
@@ -1356,7 +1356,7 @@
lemma has_integral_eq_eq:
shows "\<forall>x\<in>s. f x = g x \<Longrightarrow> ((f has_integral k) s \<longleftrightarrow> (g has_integral k) s)"
- using has_integral_eq[of s f g] has_integral_eq[of s g f] by auto
+ using has_integral_eq[of s f g] has_integral_eq[of s g f] by rule auto
lemma has_integral_null[dest]:
assumes "content({a..b}) = 0" shows "(f has_integral 0) ({a..b})"
@@ -1653,7 +1653,7 @@
proof- have *:"{a..b} = ({a..b} \<inter> {x. x$k \<le> c}) \<union> ({a..b} \<inter> {x. x$k \<ge> c})" by auto
show ?thesis apply(subst *) apply(rule tagged_division_union[OF assms])
unfolding interval_split interior_closed_interval
- by(auto simp add: vector_less_def Cart_lambda_beta elim!:allE[where x=k]) qed
+ by(auto simp add: vector_less_def elim!:allE[where x=k]) qed
lemma has_integral_separate_sides: fixes f::"real^'m \<Rightarrow> 'a::real_normed_vector"
assumes "(f has_integral i) ({a..b})" "e>0"
@@ -1743,11 +1743,11 @@
subsection {* Using additivity of lifted function to encode definedness. *}
lemma forall_option: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P(Some x))"
- by (metis map_of.simps option.nchotomy)
+ by (metis option.nchotomy)
lemma exists_option:
"(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P(Some x))"
- by (metis map_of.simps option.nchotomy)
+ by (metis option.nchotomy)
fun lifted where
"lifted (opp::'a\<Rightarrow>'a\<Rightarrow>'b) (Some x) (Some y) = Some(opp x y)" |
@@ -1842,9 +1842,8 @@
lemma operative_content[intro]: "operative (op +) content"
unfolding operative_def content_split[THEN sym] neutral_add by auto
-lemma neutral_monoid[simp]: "neutral ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a) = 0"
- unfolding neutral_def apply(rule some_equality) defer
- apply(erule_tac x=0 in allE) by auto
+lemma neutral_monoid: "neutral ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a) = 0"
+ by (rule neutral_add) (* FIXME: duplicate *)
lemma monoidal_monoid[intro]:
shows "monoidal ((op +)::('a::comm_monoid_add) \<Rightarrow> 'a \<Rightarrow> 'a)"
@@ -1941,7 +1940,7 @@
apply(rule_tac x="(k,(interval_lowerbound l)$k)" in exI) defer
apply(rule_tac x="(k,(interval_upperbound l)$k)" in exI)
unfolding division_points_def unfolding interval_bounds[OF ab]
- apply (auto simp add:interval_bounds) unfolding * by auto
+ apply auto unfolding * by auto
thus "?D1 \<subset> ?D" apply-apply(rule,rule division_points_subset[OF assms(1-4)]) by auto
have *:"interval_lowerbound ({a..b} \<inter> {x. x $ k \<ge> interval_lowerbound l $ k}) $ k = interval_lowerbound l $ k"
@@ -1952,7 +1951,7 @@
apply(rule_tac x="(k,(interval_lowerbound l)$k)" in exI) defer
apply(rule_tac x="(k,(interval_upperbound l)$k)" in exI)
unfolding division_points_def unfolding interval_bounds[OF ab]
- apply (auto simp add:interval_bounds) unfolding * by auto
+ apply auto unfolding * by auto
thus "?D2 \<subset> ?D" apply-apply(rule,rule division_points_subset[OF assms(1-4)]) by auto qed
subsection {* Preservation by divisions and tagged divisions. *}
@@ -2254,7 +2253,7 @@
assumes "p tagged_division_of {a..b}" "\<forall>x\<in>{a..b}. (f x)$i \<le> (g x)$i"
shows "(setsum (\<lambda>(x,k). content k *\<^sub>R f x) p)$i \<le> (setsum (\<lambda>(x,k). content k *\<^sub>R g x) p)$i"
unfolding setsum_component apply(rule setsum_mono)
- apply(rule mp) defer apply assumption apply(induct_tac x,rule) unfolding split_conv
+ apply(rule mp) defer apply assumption unfolding split_paired_all apply rule unfolding split_conv
proof- fix a b assume ab:"(a,b) \<in> p" note assm = tagged_division_ofD(2-4)[OF assms(1) ab]
from this(3) guess u v apply-by(erule exE)+ note b=this
show "(content b *\<^sub>R f a) $ i \<le> (content b *\<^sub>R g a) $ i" unfolding b
@@ -2903,7 +2902,7 @@
shows "setsum (\<lambda>(x,k). f(interval_upperbound k) - f(interval_lowerbound k)) p = f b - f a"
proof- let ?f = "(\<lambda>k::(real^1) set. if k = {} then 0 else f(interval_upperbound k) - f(interval_lowerbound k))"
have *:"operative op + ?f" unfolding operative_1_lt[OF monoidal_monoid] interval_eq_empty_1
- by(auto simp add:not_less interval_bound_1 vector_less_def)
+ by(auto simp add:not_less vector_less_def)
have **:"{a..b} \<noteq> {}" using assms(1) by auto note operative_tagged_division[OF monoidal_monoid * assms(2)]
note * = this[unfolded if_not_P[OF **] interval_bound_1[OF assms(1)],THEN sym ]
show ?thesis unfolding * apply(subst setsum_iterate[THEN sym]) defer
@@ -3340,7 +3339,7 @@
proof- { presume *:"a < b \<Longrightarrow> ?thesis"
show ?thesis proof(cases,rule *,assumption)
assume "\<not> a < b" hence "a = b" using assms(1) by auto
- hence *:"{vec a .. vec b} = {vec b}" "f b - f a = 0" apply(auto simp add: Cart_simps) by smt
+ hence *:"{vec a .. vec b} = {vec b}" "f b - f a = 0" by(auto simp add: Cart_eq vector_le_def order_antisym)
show ?thesis unfolding *(2) apply(rule has_integral_null) unfolding content_eq_0_1 using * `a=b` by auto
qed } assume ab:"a < b"
let ?P = "\<lambda>e. \<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of {vec1 a..vec1 b} \<and> d fine p \<longrightarrow>
@@ -3422,7 +3421,7 @@
hence "\<forall>i. u$i \<le> v$i" and uv:"{u,v}\<subseteq>{u..v}" using p(2)[OF as(1)] by auto note this(1) this(1)[unfolded forall_1]
note result = as(2)[unfolded k interval_bounds[OF this(1)] content_1[OF this(2)]]
- assume as':"x \<noteq> vec1 a" "x \<noteq> vec1 b" hence "x$1 \<in> {a<..<b}" using p(2-3)[OF as(1)] by(auto simp add:Cart_simps) note * = d(2)[OF this]
+ assume as':"x \<noteq> vec1 a" "x \<noteq> vec1 b" hence "x$1 \<in> {a<..<b}" using p(2-3)[OF as(1)] by(auto simp add: Cart_eq) note * = d(2)[OF this]
have "norm ((v$1 - u$1) *\<^sub>R f' (x$1) - (f (v$1) - f (u$1))) =
norm ((f (u$1) - f (x$1) - (u$1 - x$1) *\<^sub>R f' (x$1)) - (f (v$1) - f (x$1) - (v$1 - x$1) *\<^sub>R f' (x$1)))"
apply(rule arg_cong[of _ _ norm]) unfolding scaleR_left.diff by auto
@@ -3651,7 +3650,7 @@
lemma indefinite_integral_continuous: fixes f::"real^1 \<Rightarrow> 'a::banach"
assumes "f integrable_on {a..b}" shows "continuous_on {a..b} (\<lambda>x. integral {a..x} f)"
-proof(unfold continuous_on_def, safe) fix x e assume as:"x\<in>{a..b}" "0<(e::real)"
+proof(unfold continuous_on_iff, safe) fix x e assume as:"x\<in>{a..b}" "0<(e::real)"
let ?thesis = "\<exists>d>0. \<forall>x'\<in>{a..b}. dist x' x < d \<longrightarrow> dist (integral {a..x'} f) (integral {a..x} f) < e"
{ presume *:"a<b \<Longrightarrow> ?thesis"
show ?thesis apply(cases,rule *,assumption)
@@ -3669,7 +3668,7 @@
from indefinite_integral_continuous_left[OF assms(1) `a<b` this `e>0`] guess d . note d=this
show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute)
unfolding `x=b` vector_dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto
- next assume "a<x \<and> x<b" hence xl:"a<x" "x\<le>b" and xr:"a\<le>x" "x<b" by(auto simp add:Cart_simps)
+ next assume "a<x \<and> x<b" hence xl:"a<x" "x\<le>b" and xr:"a\<le>x" "x<b" by(auto simp add: vector_less_def)
from indefinite_integral_continuous_left [OF assms(1) xl `e>0`] guess d1 . note d1=this
from indefinite_integral_continuous_right[OF assms(1) xr `e>0`] guess d2 . note d2=this
show ?thesis apply(rule_tac x="min d1 d2" in exI)
@@ -3726,7 +3725,7 @@
unfolding o_def using assms(5) defer apply-apply(rule)
proof- fix t assume as:"t\<in>{0..1} - {t. (1 - t) *\<^sub>R c + t *\<^sub>R x \<in> k}"
have *:"c - t *\<^sub>R c + t *\<^sub>R x \<in> s - k" apply safe apply(rule conv[unfolded scaleR_simps])
- using `x\<in>s` `c\<in>s` as by(auto simp add:scaleR_simps)
+ using `x\<in>s` `c\<in>s` as by(auto simp add: algebra_simps)
have "(f \<circ> (\<lambda>t. (1 - t) *\<^sub>R c + t *\<^sub>R x) has_derivative (\<lambda>x. 0) \<circ> (\<lambda>z. (0 - z *\<^sub>R c) + z *\<^sub>R x)) (at t within {0..1})"
apply(rule diff_chain_within) apply(rule has_derivative_add)
unfolding scaleR_simps apply(rule has_derivative_sub) apply(rule has_derivative_const)
@@ -3949,7 +3948,7 @@
lemma has_integral_spike_set_eq: fixes f::"real^'n \<Rightarrow> 'a::banach"
assumes "negligible((s - t) \<union> (t - s))" shows "((f has_integral y) s \<longleftrightarrow> (f has_integral y) t)"
- unfolding has_integral_restrict_univ[THEN sym,of f] apply(rule has_integral_spike_eq[OF assms]) by auto
+ unfolding has_integral_restrict_univ[THEN sym,of f] apply(rule has_integral_spike_eq[OF assms]) by (safe, auto split: split_if_asm)
lemma has_integral_spike_set[dest]: fixes f::"real^'n \<Rightarrow> 'a::banach"
assumes "negligible((s - t) \<union> (t - s))" "(f has_integral y) s"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Apr 26 16:08:04 2010 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Apr 26 09:45:22 2010 -0700
@@ -48,16 +48,17 @@
"\<And>S T. openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S\<inter>T)"
"\<And>K. (\<forall>S \<in> K. openin U S) \<Longrightarrow> openin U (\<Union>K)"
using openin[of U] unfolding istopology_def Collect_def mem_def
- by (metis mem_def subset_eq)+
+ unfolding subset_eq Ball_def mem_def by auto
lemma openin_subset[intro]: "openin U S \<Longrightarrow> S \<subseteq> topspace U"
unfolding topspace_def by blast
lemma openin_empty[simp]: "openin U {}" by (simp add: openin_clauses)
lemma openin_Int[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<inter> T)"
- by (simp add: openin_clauses)
-
-lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union> K)" by (simp add: openin_clauses)
+ using openin_clauses by simp
+
+lemma openin_Union[intro]: "(\<forall>S \<in>K. openin U S) \<Longrightarrow> openin U (\<Union> K)"
+ using openin_clauses by simp
lemma openin_Un[intro]: "openin U S \<Longrightarrow> openin U T \<Longrightarrow> openin U (S \<union> T)"
using openin_Union[of "{S,T}" U] by auto
@@ -946,7 +947,7 @@
by (metis frontier_def closure_closed Diff_subset)
lemma frontier_empty[simp]: "frontier {} = {}"
- by (simp add: frontier_def closure_empty)
+ by (simp add: frontier_def)
lemma frontier_subset_eq: "frontier S \<subseteq> S \<longleftrightarrow> closed S"
proof-
@@ -954,7 +955,7 @@
hence "closure S \<subseteq> S" using interior_subset unfolding frontier_def by auto
hence "closed S" using closure_subset_eq by auto
}
- thus ?thesis using frontier_subset_closed[of S] by auto
+ thus ?thesis using frontier_subset_closed[of S] ..
qed
lemma frontier_complement: "frontier(- S) = frontier S"
@@ -968,7 +969,7 @@
definition
at_infinity :: "'a::real_normed_vector net" where
- "at_infinity = Abs_net (range (\<lambda>r. {x. r \<le> norm x}))"
+ "at_infinity = Abs_net (\<lambda>P. \<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x)"
definition
indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a net" (infixr "indirection" 70) where
@@ -976,23 +977,23 @@
text{* Prove That They are all nets. *}
-lemma Rep_net_at_infinity:
- "Rep_net at_infinity = range (\<lambda>r. {x. r \<le> norm x})"
+lemma eventually_at_infinity:
+ "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)"
unfolding at_infinity_def
-apply (rule Abs_net_inverse')
-apply (rule image_nonempty, simp)
-apply (clarsimp, rename_tac r s)
-apply (rule_tac x="max r s" in exI, auto)
-done
-
-lemma within_UNIV: "net within UNIV = net"
- by (simp add: Rep_net_inject [symmetric] Rep_net_within)
+proof (rule eventually_Abs_net, rule is_filter.intro)
+ fix P Q :: "'a \<Rightarrow> bool"
+ assume "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<exists>s. \<forall>x. s \<le> norm x \<longrightarrow> Q x"
+ then obtain r s where
+ "\<forall>x. r \<le> norm x \<longrightarrow> P x" and "\<forall>x. s \<le> norm x \<longrightarrow> Q x" by auto
+ then have "\<forall>x. max r s \<le> norm x \<longrightarrow> P x \<and> Q x" by simp
+ then show "\<exists>r. \<forall>x. r \<le> norm x \<longrightarrow> P x \<and> Q x" ..
+qed auto
subsection{* Identify Trivial limits, where we can't approach arbitrarily closely. *}
definition
trivial_limit :: "'a net \<Rightarrow> bool" where
- "trivial_limit net \<longleftrightarrow> {} \<in> Rep_net net"
+ "trivial_limit net \<longleftrightarrow> eventually (\<lambda>x. False) net"
lemma trivial_limit_within:
shows "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
@@ -1000,21 +1001,21 @@
assume "trivial_limit (at a within S)"
thus "\<not> a islimpt S"
unfolding trivial_limit_def
- unfolding Rep_net_within Rep_net_at
+ unfolding eventually_within eventually_at_topological
unfolding islimpt_def
apply (clarsimp simp add: expand_set_eq)
apply (rename_tac T, rule_tac x=T in exI)
- apply (clarsimp, drule_tac x=y in spec, simp)
+ apply (clarsimp, drule_tac x=y in bspec, simp_all)
done
next
assume "\<not> a islimpt S"
thus "trivial_limit (at a within S)"
unfolding trivial_limit_def
- unfolding Rep_net_within Rep_net_at
+ unfolding eventually_within eventually_at_topological
unfolding islimpt_def
- apply (clarsimp simp add: image_image)
- apply (rule_tac x=T in image_eqI)
- apply (auto simp add: expand_set_eq)
+ apply clarsimp
+ apply (rule_tac x=T in exI)
+ apply auto
done
qed
@@ -1030,14 +1031,14 @@
lemma trivial_limit_at_infinity:
"\<not> trivial_limit (at_infinity :: ('a::{real_normed_vector,zero_neq_one}) net)"
(* FIXME: find a more appropriate type class *)
- unfolding trivial_limit_def Rep_net_at_infinity
- apply (clarsimp simp add: expand_set_eq)
- apply (drule_tac x="scaleR r (sgn 1)" in spec)
+ unfolding trivial_limit_def eventually_at_infinity
+ apply clarsimp
+ apply (rule_tac x="scaleR b (sgn 1)" in exI)
apply (simp add: norm_sgn)
done
lemma trivial_limit_sequentially[intro]: "\<not> trivial_limit sequentially"
- by (auto simp add: trivial_limit_def Rep_net_sequentially)
+ by (auto simp add: trivial_limit_def eventually_sequentially)
subsection{* Some property holds "sufficiently close" to the limit point. *}
@@ -1045,10 +1046,6 @@
"eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
unfolding eventually_at dist_nz by auto
-lemma eventually_at_infinity:
- "eventually P at_infinity \<longleftrightarrow> (\<exists>b. \<forall>x. norm x >= b \<longrightarrow> P x)"
-unfolding eventually_def Rep_net_at_infinity by auto
-
lemma eventually_within: "eventually P (at a within S) \<longleftrightarrow>
(\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
unfolding eventually_within eventually_at dist_nz by auto
@@ -1059,18 +1056,20 @@
by auto (metis Rats_dense_in_nn_real order_le_less_trans order_refl)
lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
- unfolding eventually_def trivial_limit_def
- using Rep_net_nonempty [of net] by auto
+ unfolding trivial_limit_def
+ by (auto elim: eventually_rev_mp)
lemma always_eventually: "(\<forall>x. P x) ==> eventually P net"
- unfolding eventually_def trivial_limit_def
- using Rep_net_nonempty [of net] by auto
+proof -
+ assume "\<forall>x. P x" hence "P = (\<lambda>x. True)" by (simp add: ext)
+ thus "eventually P net" by simp
+qed
lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
- unfolding trivial_limit_def eventually_def by auto
+ unfolding trivial_limit_def by (auto elim: eventually_rev_mp)
lemma eventually_False: "eventually (\<lambda>x. False) net \<longleftrightarrow> trivial_limit net"
- unfolding trivial_limit_def eventually_def by auto
+ unfolding trivial_limit_def ..
lemma trivial_limit_eq: "trivial_limit net \<longleftrightarrow> (\<forall>P. eventually P net)"
apply (safe elim!: trivial_limit_eventually)
@@ -1590,7 +1589,7 @@
(* FIXME: Only one congruence rule for tendsto can be used at a time! *)
-lemma Lim_cong_within[cong add]:
+lemma Lim_cong_within(*[cong add]*):
fixes a :: "'a::metric_space"
fixes l :: "'b::metric_space" (* TODO: generalize *)
shows "(\<And>x. x \<noteq> a \<Longrightarrow> f x = g x) ==> ((\<lambda>x. f x) ---> l) (at a within S) \<longleftrightarrow> ((g ---> l) (at a within S))"
@@ -1669,7 +1668,7 @@
{ fix e::real assume "e>0"
hence "\<exists>N::nat. \<forall>n::nat\<ge>N. inverse (real n) < e"
using real_arch_inv[of e] apply auto apply(rule_tac x=n in exI)
- by (metis not_le le_imp_inverse_le not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7))
+ by (metis le_imp_inverse_le not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7))
}
thus ?thesis unfolding Lim_sequentially dist_norm by simp
qed
@@ -1704,7 +1703,7 @@
apply (simp add: interior_def, safe)
apply (force simp add: open_contains_cball)
apply (rule_tac x="ball x e" in exI)
- apply (simp add: open_ball centre_in_ball subset_trans [OF ball_subset_cball])
+ apply (simp add: subset_trans [OF ball_subset_cball])
done
lemma islimpt_ball:
@@ -1879,14 +1878,14 @@
lemma frontier_ball:
fixes a :: "'a::real_normed_vector"
shows "0 < e ==> frontier(ball a e) = {x. dist a x = e}"
- apply (simp add: frontier_def closure_ball interior_open open_ball order_less_imp_le)
+ apply (simp add: frontier_def closure_ball interior_open order_less_imp_le)
apply (simp add: expand_set_eq)
by arith
lemma frontier_cball:
fixes a :: "'a::{real_normed_vector, perfect_space}"
shows "frontier(cball a e) = {x. dist a x = e}"
- apply (simp add: frontier_def interior_cball closed_cball closure_closed order_less_imp_le)
+ apply (simp add: frontier_def interior_cball closed_cball order_less_imp_le)
apply (simp add: expand_set_eq)
by arith
@@ -2006,9 +2005,10 @@
lemma bounded_ball[simp,intro]: "bounded(ball x e)"
by (metis ball_subset_cball bounded_cball bounded_subset)
-lemma finite_imp_bounded[intro]: assumes "finite S" shows "bounded S"
+lemma finite_imp_bounded[intro]:
+ fixes S :: "'a::metric_space set" assumes "finite S" shows "bounded S"
proof-
- { fix a F assume as:"bounded F"
+ { fix a and F :: "'a set" assume as:"bounded F"
then obtain x e where "\<forall>y\<in>F. dist x y \<le> e" unfolding bounded_def by auto
hence "\<forall>y\<in>(insert a F). dist x y \<le> max e (dist x a)" by auto
hence "bounded (insert a F)" unfolding bounded_def by (intro exI)
@@ -2218,7 +2218,7 @@
apply (rule allI, rule impI, rule ext)
apply (erule conjE)
apply (induct_tac x)
-apply (simp add: nat_rec_0)
+apply simp
apply (erule_tac x="n" in allE)
apply (simp)
done
@@ -2650,7 +2650,8 @@
{ fix x y assume "x\<in>t" "y\<in>t" "f x = f y"
hence "x \<in> f x" "y \<in> f x \<longrightarrow> y = x" using f[THEN bspec[where x=x]] and `t\<subseteq>s` by auto
hence "x = y" using `f x = f y` and f[THEN bspec[where x=y]] and `y\<in>t` and `t\<subseteq>s` by auto }
- hence "infinite (f ` t)" using assms(2) using finite_imageD[unfolded inj_on_def, of f t] by auto
+ hence "inj_on f t" unfolding inj_on_def by simp
+ hence "infinite (f ` t)" using assms(2) using finite_imageD by auto
moreover
{ fix x assume "x\<in>t" "f x \<notin> g"
from g(3) assms(3) `x\<in>t` obtain h where "h\<in>g" and "x\<in>h" by auto
@@ -3145,7 +3146,7 @@
using `?lhs`[unfolded continuous_within Lim_within] by auto
{ fix y assume "y\<in>f ` (ball x d \<inter> s)"
hence "y \<in> ball (f x) e" using d(2) unfolding dist_nz[THEN sym]
- apply (auto simp add: dist_commute mem_ball) apply(erule_tac x=xa in ballE) apply auto using `e>0` by auto
+ apply (auto simp add: dist_commute) apply(erule_tac x=xa in ballE) apply auto using `e>0` by auto
}
hence "\<exists>d>0. f ` (ball x d \<inter> s) \<subseteq> ball (f x) e" using `d>0` unfolding subset_eq ball_def by (auto simp add: dist_commute) }
thus ?rhs by auto
@@ -3168,9 +3169,32 @@
text{* For setwise continuity, just start from the epsilon-delta definitions. *}
definition
- continuous_on :: "'a::metric_space set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> bool" where
- "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. \<forall>e>0. \<exists>d::real>0. \<forall>x' \<in> s. dist x' x < d --> dist (f x') (f x) < e)"
-
+ continuous_on ::
+ "'a set \<Rightarrow> ('a::topological_space \<Rightarrow> 'b::topological_space) \<Rightarrow> bool"
+where
+ "continuous_on s f \<longleftrightarrow>
+ (\<forall>x\<in>s. \<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow>
+ (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>x'\<in>s. x' \<in> A \<longrightarrow> f x' \<in> B)))"
+
+lemma continuous_on_iff:
+ "continuous_on s f \<longleftrightarrow>
+ (\<forall>x\<in>s. \<forall>e>0. \<exists>d>0. \<forall>x'\<in>s. dist x' x < d --> dist (f x') (f x) < e)"
+unfolding continuous_on_def
+apply safe
+apply (drule (1) bspec)
+apply (drule_tac x="ball (f x) e" in spec, simp, clarify)
+apply (drule (1) open_dist [THEN iffD1, THEN bspec])
+apply (clarify, rename_tac d)
+apply (rule_tac x=d in exI, clarify)
+apply (drule_tac x=x' in bspec, assumption)
+apply (drule_tac x=x' in spec, simp add: dist_commute)
+apply (drule_tac x=x in bspec, assumption)
+apply (drule (1) open_dist [THEN iffD1, THEN bspec], clarify)
+apply (drule_tac x=e in spec, simp, clarify)
+apply (rule_tac x="ball x d" in exI, simp, clarify)
+apply (drule_tac x=x' in bspec, assumption)
+apply (simp add: dist_commute)
+done
definition
uniformly_continuous_on ::
@@ -3184,14 +3208,14 @@
lemma continuous_on_o_dest_vec1: fixes f::"real \<Rightarrow> 'a::real_normed_vector"
assumes "continuous_on {a..b::real} f" shows "continuous_on {vec1 a..vec1 b} (f o dest_vec1)"
- using assms unfolding continuous_on_def apply safe
+ using assms unfolding continuous_on_iff apply safe
apply(erule_tac x="x$1" in ballE,erule_tac x=e in allE) apply safe
apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real
apply(erule_tac x="dest_vec1 x'" in ballE) by(auto simp add:vector_le_def)
lemma continuous_on_o_vec1: fixes f::"real^1 \<Rightarrow> 'a::real_normed_vector"
assumes "continuous_on {a..b} f" shows "continuous_on {dest_vec1 a..dest_vec1 b} (f o vec1)"
- using assms unfolding continuous_on_def apply safe
+ using assms unfolding continuous_on_iff apply safe
apply(erule_tac x="vec x" in ballE,erule_tac x=e in allE) apply safe
apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real
apply(erule_tac x="vec1 x'" in ballE) by(auto simp add:vector_le_def)
@@ -3200,15 +3224,17 @@
lemma uniformly_continuous_imp_continuous:
" uniformly_continuous_on s f ==> continuous_on s f"
- unfolding uniformly_continuous_on_def continuous_on_def by blast
+ unfolding uniformly_continuous_on_def continuous_on_iff by blast
lemma continuous_at_imp_continuous_within:
"continuous (at x) f ==> continuous (at x within s) f"
unfolding continuous_within continuous_at using Lim_at_within by auto
-lemma continuous_at_imp_continuous_on: assumes "(\<forall>x \<in> s. continuous (at x) f)"
+lemma continuous_at_imp_continuous_on:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ assumes "(\<forall>x \<in> s. continuous (at x) f)"
shows "continuous_on s f"
-proof(simp add: continuous_at continuous_on_def, rule, rule, rule)
+proof(simp add: continuous_at continuous_on_iff, rule, rule, rule)
fix x and e::real assume "x\<in>s" "e>0"
hence "eventually (\<lambda>xa. dist (f xa) (f x) < e) (at x)" using assms unfolding continuous_at tendsto_iff by auto
then obtain d where d:"d>0" "\<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" unfolding eventually_at by auto
@@ -3221,7 +3247,9 @@
qed
lemma continuous_on_eq_continuous_within:
- "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x within s) f)" (is "?lhs = ?rhs")
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x within s) f)"
+ (is "?lhs = ?rhs")
proof
assume ?rhs
{ fix x assume "x\<in>s"
@@ -3232,18 +3260,21 @@
hence "dist (f x') (f x) < e" using `e>0` d `x'\<in>s` dist_eq_0_iff[of x' x] zero_le_dist[of x' x] as(2) by (metis dist_eq_0_iff dist_nz) }
hence "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" using `d>0` by auto
}
- thus ?lhs using `?rhs` unfolding continuous_on_def continuous_within Lim_within by auto
+ thus ?lhs using `?rhs` unfolding continuous_on_iff continuous_within Lim_within by auto
next
assume ?lhs
- thus ?rhs unfolding continuous_on_def continuous_within Lim_within by blast
+ thus ?rhs unfolding continuous_on_iff continuous_within Lim_within by blast
qed
lemma continuous_on:
- "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. (f ---> f(x)) (at x within s))"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. (f ---> f(x)) (at x within s))"
by (auto simp add: continuous_on_eq_continuous_within continuous_within)
+ (* BH: maybe this should be the definition? *)
lemma continuous_on_eq_continuous_at:
- "open s ==> (continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x) f))"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ shows "open s ==> (continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x) f))"
by (auto simp add: continuous_on continuous_at Lim_within_open)
lemma continuous_within_subset:
@@ -3252,19 +3283,22 @@
unfolding continuous_within by(metis Lim_within_subset)
lemma continuous_on_subset:
- "continuous_on s f \<Longrightarrow> t \<subseteq> s ==> continuous_on t f"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ shows "continuous_on s f \<Longrightarrow> t \<subseteq> s ==> continuous_on t f"
unfolding continuous_on by (metis subset_eq Lim_within_subset)
lemma continuous_on_interior:
- "continuous_on s f \<Longrightarrow> x \<in> interior s ==> continuous (at x) f"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ shows "continuous_on s f \<Longrightarrow> x \<in> interior s ==> continuous (at x) f"
unfolding interior_def
apply simp
by (meson continuous_on_eq_continuous_at continuous_on_subset)
lemma continuous_on_eq:
- "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ shows "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f
==> continuous_on s g"
- by (simp add: continuous_on_def)
+ by (simp add: continuous_on_iff)
text{* Characterization of various kinds of continuity in terms of sequences. *}
@@ -3317,7 +3351,9 @@
using continuous_within_sequentially[of a UNIV f] unfolding within_UNIV by auto
lemma continuous_on_sequentially:
- "continuous_on s f \<longleftrightarrow> (\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x ---> a) sequentially
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ shows "continuous_on s f \<longleftrightarrow>
+ (\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x ---> a) sequentially
--> ((f o x) ---> f(a)) sequentially)" (is "?lhs = ?rhs")
proof
assume ?rhs thus ?lhs using continuous_within_sequentially[of _ s f] unfolding continuous_on_eq_continuous_within by auto
@@ -3436,7 +3472,7 @@
lemma continuous_on_const:
"continuous_on s (\<lambda>x. c)"
- unfolding continuous_on_eq_continuous_within using continuous_const by blast
+ unfolding continuous_on_def by auto
lemma continuous_on_cmul:
fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
@@ -3524,7 +3560,7 @@
lemma continuous_on_id:
"continuous_on s (\<lambda>x. x)"
- unfolding continuous_on Lim_within by auto
+ unfolding continuous_on_def by auto
lemma uniformly_continuous_on_id:
"uniformly_continuous_on s (\<lambda>x. x)"
@@ -3559,7 +3595,9 @@
qed
lemma continuous_on_compose:
- "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ fixes g :: "'b::metric_space \<Rightarrow> 'c::metric_space" (* TODO: generalize *)
+ shows "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
unfolding continuous_on_eq_continuous_within using continuous_within_compose[of _ s f g] by auto
lemma uniformly_continuous_on_compose:
@@ -3610,7 +3648,8 @@
qed
lemma continuous_on_open:
- "continuous_on s f \<longleftrightarrow>
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ shows "continuous_on s f \<longleftrightarrow>
(\<forall>t. openin (subtopology euclidean (f ` s)) t
--> openin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
proof
@@ -3643,7 +3682,8 @@
(* ------------------------------------------------------------------------- *)
lemma continuous_on_closed:
- "continuous_on s f \<longleftrightarrow> (\<forall>t. closedin (subtopology euclidean (f ` s)) t --> closedin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ shows "continuous_on s f \<longleftrightarrow> (\<forall>t. closedin (subtopology euclidean (f ` s)) t --> closedin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
proof
assume ?lhs
{ fix t
@@ -3667,6 +3707,7 @@
text{* Half-global and completely global cases. *}
lemma continuous_open_in_preimage:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "open t"
shows "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
proof-
@@ -3677,6 +3718,7 @@
qed
lemma continuous_closed_in_preimage:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "closed t"
shows "closedin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
proof-
@@ -3688,6 +3730,7 @@
qed
lemma continuous_open_preimage:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "open s" "open t"
shows "open {x \<in> s. f x \<in> t}"
proof-
@@ -3697,6 +3740,7 @@
qed
lemma continuous_closed_preimage:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "closed s" "closed t"
shows "closed {x \<in> s. f x \<in> t}"
proof-
@@ -3739,14 +3783,17 @@
text{* Equality of continuous functions on closure and related results. *}
lemma continuous_closed_in_preimage_constant:
- "continuous_on s f ==> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ shows "continuous_on s f ==> closedin (subtopology euclidean s) {x \<in> s. f x = a}"
using continuous_closed_in_preimage[of s f "{a}"] closed_sing by auto
lemma continuous_closed_preimage_constant:
- "continuous_on s f \<Longrightarrow> closed s ==> closed {x \<in> s. f x = a}"
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ shows "continuous_on s f \<Longrightarrow> closed s ==> closed {x \<in> s. f x = a}"
using continuous_closed_preimage[of s f "{a}"] closed_sing by auto
lemma continuous_constant_on_closure:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on (closure s) f"
"\<forall>x \<in> s. f x = a"
shows "\<forall>x \<in> (closure s). f x = a"
@@ -3754,6 +3801,7 @@
assms closure_minimal[of s "{x \<in> closure s. f x = a}"] closure_subset unfolding subset_eq by auto
lemma image_closure_subset:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on (closure s) f" "closed t" "(f ` s) \<subseteq> t"
shows "f ` (closure s) \<subseteq> t"
proof-
@@ -3798,11 +3846,13 @@
using assms using continuous_within_avoid[of x UNIV f a, unfolded within_UNIV] by auto
lemma continuous_on_avoid:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "x \<in> s" "f x \<noteq> a"
shows "\<exists>e>0. \<forall>y \<in> s. dist x y < e \<longrightarrow> f y \<noteq> a"
using assms(1)[unfolded continuous_on_eq_continuous_within, THEN bspec[where x=x], OF assms(2)] continuous_within_avoid[of x s f a] assms(2,3) by auto
lemma continuous_on_open_avoid:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "open s" "x \<in> s" "f x \<noteq> a"
shows "\<exists>e>0. \<forall>y. dist x y < e \<longrightarrow> f y \<noteq> a"
using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)] continuous_at_avoid[of x f a] assms(3,4) by auto
@@ -3810,22 +3860,25 @@
text{* Proving a function is constant by proving open-ness of level set. *}
lemma continuous_levelset_open_in_cases:
- "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
openin (subtopology euclidean s) {x \<in> s. f x = a}
==> (\<forall>x \<in> s. f x \<noteq> a) \<or> (\<forall>x \<in> s. f x = a)"
unfolding connected_clopen using continuous_closed_in_preimage_constant by auto
lemma continuous_levelset_open_in:
- "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
+ shows "connected s \<Longrightarrow> continuous_on s f \<Longrightarrow>
openin (subtopology euclidean s) {x \<in> s. f x = a} \<Longrightarrow>
(\<exists>x \<in> s. f x = a) ==> (\<forall>x \<in> s. f x = a)"
using continuous_levelset_open_in_cases[of s f ]
by meson
lemma continuous_levelset_open:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "connected s" "continuous_on s f" "open {x \<in> s. f x = a}" "\<exists>x \<in> s. f x = a"
shows "\<forall>x \<in> s. f x = a"
-using continuous_levelset_open_in[OF assms(1,2), of a, unfolded openin_open] using assms (3,4) by auto
+using continuous_levelset_open_in[OF assms(1,2), of a, unfolded openin_open] using assms (3,4) by fast
text{* Some arithmetical combinations (more to prove). *}
@@ -3906,7 +3959,7 @@
then obtain y where y:"\<forall>n. y n \<in> s \<and> x n = f (y n)" unfolding image_iff Bex_def using choice[of "\<lambda>n xa. xa \<in> s \<and> x n = f xa"] by auto
then obtain l r where "l\<in>s" and r:"subseq r" and lr:"((y \<circ> r) ---> l) sequentially" using assms(2)[unfolded compact_def, THEN spec[where x=y]] by auto
{ fix e::real assume "e>0"
- then obtain d where "d>0" and d:"\<forall>x'\<in>s. dist x' l < d \<longrightarrow> dist (f x') (f l) < e" using assms(1)[unfolded continuous_on_def, THEN bspec[where x=l], OF `l\<in>s`] by auto
+ then obtain d where "d>0" and d:"\<forall>x'\<in>s. dist x' l < d \<longrightarrow> dist (f x') (f l) < e" using assms(1)[unfolded continuous_on_iff, THEN bspec[where x=l], OF `l\<in>s`] by auto
then obtain N::nat where N:"\<forall>n\<ge>N. dist ((y \<circ> r) n) l < d" using lr[unfolded Lim_sequentially, THEN spec[where x=d]] by auto
{ fix n::nat assume "n\<ge>N" hence "dist ((x \<circ> r) n) (f l) < e" using N[THEN spec[where x=n]] d[THEN bspec[where x="y (r n)"]] y[THEN spec[where x="r n"]] by auto }
hence "\<exists>N. \<forall>n\<ge>N. dist ((x \<circ> r) n) (f l) < e" by auto }
@@ -3915,6 +3968,7 @@
qed
lemma connected_continuous_image:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "continuous_on s f" "connected s"
shows "connected(f ` s)"
proof-
@@ -3935,7 +3989,7 @@
shows "uniformly_continuous_on s f"
proof-
{ fix x assume x:"x\<in>s"
- hence "\<forall>xa. \<exists>y. 0 < xa \<longrightarrow> (y > 0 \<and> (\<forall>x'\<in>s. dist x' x < y \<longrightarrow> dist (f x') (f x) < xa))" using assms(1)[unfolded continuous_on_def, THEN bspec[where x=x]] by auto
+ hence "\<forall>xa. \<exists>y. 0 < xa \<longrightarrow> (y > 0 \<and> (\<forall>x'\<in>s. dist x' x < y \<longrightarrow> dist (f x') (f x) < xa))" using assms(1)[unfolded continuous_on_iff, THEN bspec[where x=x]] by auto
hence "\<exists>fa. \<forall>xa>0. \<forall>x'\<in>s. fa xa > 0 \<and> (dist x' x < fa xa \<longrightarrow> dist (f x') (f x) < xa)" using choice[of "\<lambda>e d. e>0 \<longrightarrow> d>0 \<and>(\<forall>x'\<in>s. (dist x' x < d \<longrightarrow> dist (f x') (f x) < e))"] by auto }
then have "\<forall>x\<in>s. \<exists>y. \<forall>xa. 0 < xa \<longrightarrow> (\<forall>x'\<in>s. y xa > 0 \<and> (dist x' x < y xa \<longrightarrow> dist (f x') (f x) < xa))" by auto
then obtain d where d:"\<forall>e>0. \<forall>x\<in>s. \<forall>x'\<in>s. d x e > 0 \<and> (dist x' x < d x e \<longrightarrow> dist (f x') (f x) < e)"
@@ -4007,7 +4061,7 @@
using eventually_and[of "(\<lambda>n. \<forall>x\<in>s. norm (f n x - g x) < e / 3)" "(\<lambda>n. continuous_on s (f n))" net] assms(1,2) eventually_happens by blast
have "e / 3 > 0" using `e>0` by auto
then obtain d where "d>0" and d:"\<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f n x') (f n x) < e / 3"
- using n(2)[unfolded continuous_on_def, THEN bspec[where x=x], OF `x\<in>s`, THEN spec[where x="e/3"]] by blast
+ using n(2)[unfolded continuous_on_iff, THEN bspec[where x=x], OF `x\<in>s`, THEN spec[where x="e/3"]] by blast
{ fix y assume "y\<in>s" "dist y x < d"
hence "dist (f n y) (f n x) < e / 3" using d[THEN bspec[where x=y]] by auto
hence "norm (f n y - g x) < 2 * e / 3" using norm_triangle_lt[of "f n y - f n x" "f n x - g x" "2*e/3"]
@@ -4015,7 +4069,7 @@
hence "dist (g y) (g x) < e" unfolding dist_norm using n(1)[THEN bspec[where x=y], OF `y\<in>s`]
unfolding norm_minus_cancel[of "f n y - g y", THEN sym] using norm_triangle_lt[of "f n y - g x" "g y - f n y" e] by (auto simp add: uminus_add_conv_diff) }
hence "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (g x') (g x) < e" using `d>0` by auto }
- thus ?thesis unfolding continuous_on_def by auto
+ thus ?thesis unfolding continuous_on_iff by auto
qed
subsection{* Topological properties of linear functions. *}
@@ -4060,6 +4114,7 @@
unfolding continuous_within using Lim_bilinear[of f "f x"] by auto
lemma bilinear_continuous_on_compose:
+ fixes s :: "'a::metric_space set" (* TODO: generalize *)
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
@@ -4098,7 +4153,7 @@
lemma continuous_on_real_range:
fixes f :: "'a::real_normed_vector \<Rightarrow> real"
shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d --> abs(f x' - f x) < e))"
- unfolding continuous_on_def dist_norm by simp
+ unfolding continuous_on_iff dist_norm by simp
lemma continuous_at_norm: "continuous (at x) norm"
unfolding continuous_at by (intro tendsto_intros)
@@ -4109,7 +4164,9 @@
lemma continuous_at_component: "continuous (at a) (\<lambda>x. x $ i)"
unfolding continuous_at by (intro tendsto_intros)
-lemma continuous_on_component: "continuous_on s (\<lambda>x. x $ i)"
+lemma continuous_on_component:
+ fixes s :: "('a::metric_space ^ 'n) set" (* TODO: generalize *)
+ shows "continuous_on s (\<lambda>x. x $ i)"
unfolding continuous_on by (intro ballI tendsto_intros)
lemma continuous_at_infnorm: "continuous (at x) infnorm"
@@ -4333,7 +4390,7 @@
using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\<lambda>n. sndcart (x n)"], THEN spec[where x="sndcart l"]]
unfolding Lim_sequentially by auto
hence "l \<in> {pastecart x y |x y. x \<in> s \<and> y \<in> t}" apply- unfolding mem_Collect_eq apply(rule_tac x="fstcart l" in exI,rule_tac x="sndcart l" in exI) by auto }
- thus ?thesis unfolding closed_sequential_limits by auto
+ thus ?thesis unfolding closed_sequential_limits by blast
qed
lemma compact_pastecart:
@@ -4424,7 +4481,7 @@
have "{x - y | x y . x\<in>s \<and> y\<in>s} \<noteq> {}" using `s \<noteq> {}` by auto
then obtain x where x:"x\<in>{x - y |x y. x \<in> s \<and> y \<in> s}" "\<forall>y\<in>{x - y |x y. x \<in> s \<and> y \<in> s}. norm y \<le> norm x"
using compact_differences[OF assms(1) assms(1)]
- using distance_attains_sup[where 'a="'a", unfolded dist_norm, of "{x - y | x y . x\<in>s \<and> y\<in>s}" 0] by(auto simp add: norm_minus_cancel)
+ using distance_attains_sup[where 'a="'a", unfolded dist_norm, of "{x - y | x y . x\<in>s \<and> y\<in>s}" 0] by auto
from x(1) obtain a b where "a\<in>s" "b\<in>s" "x = a - b" by auto
thus ?thesis using x(2)[unfolded `x = a - b`] by blast
qed
@@ -4445,7 +4502,7 @@
hence "norm (x - y) \<le> 2 * a" using norm_triangle_ineq[of x "-y", unfolded norm_minus_cancel] a[THEN bspec[where x=x]] a[THEN bspec[where x=y]] by (auto simp add: field_simps) }
note * = this
{ fix x y assume "x\<in>s" "y\<in>s" hence "s \<noteq> {}" by auto
- have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s`
+ have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s`
by simp (blast intro!: Sup_upper *) }
moreover
{ fix d::real assume "d>0" "d < diameter s"
@@ -4476,10 +4533,10 @@
proof-
have b:"bounded s" using assms(1) by (rule compact_imp_bounded)
then obtain x y where xys:"x\<in>s" "y\<in>s" and xy:"\<forall>u\<in>s. \<forall>v\<in>s. norm (u - v) \<le> norm (x - y)" using compact_sup_maxdistance[OF assms] by auto
- hence "diameter s \<le> norm (x - y)"
- by (force simp add: diameter_def intro!: Sup_least)
+ hence "diameter s \<le> norm (x - y)"
+ unfolding diameter_def by clarsimp (rule Sup_least, fast+)
thus ?thesis
- by (metis b diameter_bounded_bound order_antisym xys)
+ by (metis b diameter_bounded_bound order_antisym xys)
qed
text{* Related results with closure as the conclusion. *}
@@ -4668,7 +4725,7 @@
lemma mem_interval_1: fixes x :: "real^1" shows
"(x \<in> {a .. b} \<longleftrightarrow> dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b)"
"(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
-by(simp_all add: Cart_eq vector_less_def vector_le_def forall_1)
+by(simp_all add: Cart_eq vector_less_def vector_le_def)
lemma vec1_interval:fixes a::"real" shows
"vec1 ` {a .. b} = {vec1 a .. vec1 b}"
@@ -4694,7 +4751,7 @@
have "a$i < b$i" using as[THEN spec[where x=i]] by auto
hence "a$i < ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i < b$i"
unfolding vector_smult_component and vector_add_component
- by (auto simp add: less_divide_eq_number_of1) }
+ by auto }
hence "{a <..< b} \<noteq> {}" using mem_interval(1)[of "?x" a b] by auto }
ultimately show ?th1 by blast
@@ -4709,7 +4766,7 @@
have "a$i \<le> b$i" using as[THEN spec[where x=i]] by auto
hence "a$i \<le> ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i \<le> b$i"
unfolding vector_smult_component and vector_add_component
- by (auto simp add: less_divide_eq_number_of1) }
+ by auto }
hence "{a .. b} \<noteq> {}" using mem_interval(2)[of "?x" a b] by auto }
ultimately show ?th2 by blast
qed
@@ -4772,13 +4829,13 @@
{ fix j
have "c $ j < ?x $ j \<and> ?x $ j < d $ j" unfolding Cart_lambda_beta
apply(cases "j=i") using as(2)[THEN spec[where x=j]]
- by (auto simp add: less_divide_eq_number_of1 as2) }
+ by (auto simp add: as2) }
hence "?x\<in>{c<..<d}" unfolding mem_interval by auto
moreover
have "?x\<notin>{a .. b}"
unfolding mem_interval apply auto apply(rule_tac x=i in exI)
using as(2)[THEN spec[where x=i]] and as2
- by (auto simp add: less_divide_eq_number_of1)
+ by auto
ultimately have False using as by auto }
hence "a$i \<le> c$i" by(rule ccontr)auto
moreover
@@ -4787,13 +4844,13 @@
{ fix j
have "d $ j > ?x $ j \<and> ?x $ j > c $ j" unfolding Cart_lambda_beta
apply(cases "j=i") using as(2)[THEN spec[where x=j]]
- by (auto simp add: less_divide_eq_number_of1 as2) }
+ by (auto simp add: as2) }
hence "?x\<in>{c<..<d}" unfolding mem_interval by auto
moreover
have "?x\<notin>{a .. b}"
unfolding mem_interval apply auto apply(rule_tac x=i in exI)
using as(2)[THEN spec[where x=i]] and as2
- by (auto simp add: less_divide_eq_number_of1)
+ by auto
ultimately have False using as by auto }
hence "b$i \<ge> d$i" by(rule ccontr)auto
ultimately
@@ -4824,7 +4881,7 @@
lemma inter_interval: fixes a :: "'a::linorder^'n" shows
"{a .. b} \<inter> {c .. d} = {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
unfolding expand_set_eq and Int_iff and mem_interval
- by (auto simp add: less_divide_eq_number_of1 intro!: bexI)
+ by auto
(* Moved interval_open_subset_closed a bit upwards *)
@@ -4864,7 +4921,7 @@
using open_interval[of "vec1 a" "vec1 b"] unfolding open_contains_ball
apply-apply(rule,erule_tac x="vec1 x" in ballE) apply(erule exE,rule_tac x=e in exI)
unfolding subset_eq mem_ball apply(rule) defer apply(rule,erule conjE,erule_tac x="vec1 xa" in ballE)
- by(auto simp add: vec1_dest_vec1_simps vector_less_def forall_1)
+ by(auto simp add: dist_vec1 dist_real_def vector_less_def)
lemma closed_interval[intro]: fixes a :: "real^'n" shows "closed {a .. b}"
proof-
@@ -4945,7 +5002,7 @@
have "a $ i < ((1 / 2) *\<^sub>R (a + b)) $ i \<and> ((1 / 2) *\<^sub>R (a + b)) $ i < b $ i"
using assms[unfolded interval_ne_empty, THEN spec[where x=i]]
unfolding vector_smult_component and vector_add_component
- by(auto simp add: less_divide_eq_number_of1) }
+ by auto }
thus ?thesis unfolding mem_interval by auto
qed
@@ -4987,7 +5044,7 @@
x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)"
by (auto simp add: algebra_simps)
hence "f n < b" and "a < f n" using open_closed_interval_convex[OF open_interval_midpoint[OF assms] as *] unfolding f_def by auto
- hence False using fn unfolding f_def using xc by(auto simp add: vector_mul_lcancel vector_ssub_ldistrib) }
+ hence False using fn unfolding f_def using xc by(auto simp add: vector_ssub_ldistrib) }
moreover
{ assume "\<not> (f ---> x) sequentially"
{ fix e::real assume "e>0"
@@ -5261,12 +5318,14 @@
by (auto simp add: eventually_within_Un)
lemma continuous_on_union:
+ fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f"
shows "continuous_on (s \<union> t) f"
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 f :: "'a::metric_space \<Rightarrow> 'b::metric_space" (* TODO: generalize *)
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)"
@@ -5401,7 +5460,7 @@
then obtain y where y:"y\<in>t" "g y = x" by auto
then obtain x' where x':"x'\<in>s" "f x' = y" using assms(3) by auto
hence "x \<in> s" unfolding g_def using someI2[of "\<lambda>b. b\<in>s \<and> f b = y" x' "\<lambda>x. x\<in>s"] unfolding y(2)[THEN sym] and g_def by auto }
- ultimately have "x\<in>s \<longleftrightarrow> x \<in> g ` t" by auto }
+ ultimately have "x\<in>s \<longleftrightarrow> x \<in> g ` t" .. }
hence "g ` t = s" by auto
ultimately
show ?thesis unfolding homeomorphism_def homeomorphic_def
@@ -5543,7 +5602,7 @@
let ?S' = "{x::real^'m. x\<in>s \<and> norm x = norm a}"
let ?S'' = "{x::real^'m. norm x = norm a}"
- have "?S'' = frontier(cball 0 (norm a))" unfolding frontier_cball and dist_norm by (auto simp add: norm_minus_cancel)
+ have "?S'' = frontier(cball 0 (norm a))" unfolding frontier_cball and dist_norm by auto
hence "compact ?S''" using compact_frontier[OF compact_cball, of 0 "norm a"] by auto
moreover have "?S' = s \<inter> ?S''" by auto
ultimately have "compact ?S'" using closed_inter_compact[of s ?S''] using s(1) by auto
@@ -5590,7 +5649,7 @@
lemma subspace_substandard:
"subspace {x::real^_. (\<forall>i. P i \<longrightarrow> x$i = 0)}"
- unfolding subspace_def by(auto simp add: vector_add_component vector_smult_component elim!: ballE)
+ unfolding subspace_def by auto
lemma closed_substandard:
"closed {x::real^'n. \<forall>i. P i --> x$i = 0}" (is "closed ?A")
@@ -5607,7 +5666,7 @@
then obtain B where BB:"B \<in> ?Bs" and B:"B = {x::real^'n. inner (basis i) x = 0}" by auto
hence "x $ i = 0" unfolding B using x unfolding inner_basis by auto }
hence "x\<in>?A" by auto }
- ultimately have "x\<in>?A \<longleftrightarrow> x\<in> \<Inter>?Bs" by auto }
+ ultimately have "x\<in>?A \<longleftrightarrow> x\<in> \<Inter>?Bs" .. }
hence "?A = \<Inter> ?Bs" by auto
thus ?thesis by(auto simp add: closed_Inter closed_hyperplane)
qed
@@ -5783,23 +5842,23 @@
case False
{ fix y assume "a \<le> y" "y \<le> b" "m > 0"
hence "m *\<^sub>R a + c \<le> m *\<^sub>R y + c" "m *\<^sub>R y + c \<le> m *\<^sub>R b + c"
- unfolding vector_le_def by(auto simp add: vector_smult_component vector_add_component)
+ unfolding vector_le_def by auto
} moreover
{ fix y assume "a \<le> y" "y \<le> b" "m < 0"
hence "m *\<^sub>R b + c \<le> m *\<^sub>R y + c" "m *\<^sub>R y + c \<le> m *\<^sub>R a + c"
- unfolding vector_le_def by(auto simp add: vector_smult_component vector_add_component mult_left_mono_neg elim!:ballE)
+ unfolding vector_le_def by(auto simp add: mult_left_mono_neg)
} moreover
{ fix y assume "m > 0" "m *\<^sub>R a + c \<le> y" "y \<le> m *\<^sub>R b + c"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
unfolding image_iff Bex_def mem_interval vector_le_def
- apply(auto simp add: vector_smult_component vector_add_component vector_minus_component vector_smult_assoc pth_3[symmetric]
+ apply(auto simp add: vector_smult_assoc pth_3[symmetric]
intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
by(auto simp add: pos_le_divide_eq pos_divide_le_eq real_mult_commute diff_le_iff)
} moreover
{ fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
unfolding image_iff Bex_def mem_interval vector_le_def
- apply(auto simp add: vector_smult_component vector_add_component vector_minus_component vector_smult_assoc pth_3[symmetric]
+ apply(auto simp add: vector_smult_assoc pth_3[symmetric]
intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
by(auto simp add: neg_le_divide_eq neg_divide_le_eq real_mult_commute diff_le_iff)
}
@@ -6045,7 +6104,7 @@
{ fix x y assume "x\<in>s" "y\<in>s" moreover
fix e::real assume "e>0" ultimately
have "dist y x < e \<longrightarrow> dist (g y) (g x) < e" using dist by fastsimp }
- hence "continuous_on s g" unfolding continuous_on_def by auto
+ hence "continuous_on s g" unfolding continuous_on_iff by auto
hence "((snd \<circ> h \<circ> r) ---> g a) sequentially" unfolding continuous_on_sequentially
apply (rule allE[where x="\<lambda>n. (fst \<circ> h \<circ> r) n"]) apply (erule ballE[where x=a])
--- a/src/HOL/SetInterval.thy Mon Apr 26 16:08:04 2010 +0200
+++ b/src/HOL/SetInterval.thy Mon Apr 26 09:45:22 2010 -0700
@@ -54,22 +54,22 @@
@{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well. *}
syntax
- "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" 10)
- "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" 10)
- "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" 10)
- "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" 10)
+ "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" [0, 0, 10] 10)
+ "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" [0, 0, 10] 10)
+ "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" [0, 0, 10] 10)
+ "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" [0, 0, 10] 10)
syntax (xsymbols)
- "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _\<le>_./ _)" 10)
- "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _<_./ _)" 10)
- "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" 10)
- "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _<_./ _)" 10)
+ "_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _\<le>_./ _)" [0, 0, 10] 10)
+ "_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union> _<_./ _)" [0, 0, 10] 10)
+ "_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _\<le>_./ _)" [0, 0, 10] 10)
+ "_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _<_./ _)" [0, 0, 10] 10)
syntax (latex output)
- "_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" 10)
- "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ < _)/ _)" 10)
- "_INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ \<le> _)/ _)" 10)
- "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ < _)/ _)" 10)
+ "_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" [0, 0, 10] 10)
+ "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ < _)/ _)" [0, 0, 10] 10)
+ "_INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ \<le> _)/ _)" [0, 0, 10] 10)
+ "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ < _)/ _)" [0, 0, 10] 10)
translations
"UN i<=n. A" == "UN i:{..n}. A"