finite annotation on cartesian product is now implicit.
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Jan 07 17:43:35 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Jan 07 18:56:39 2010 +0100
@@ -25,7 +25,7 @@
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::finite)))"
+ 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
have "continuous_on s (norm \<circ> f)" by(rule continuous_on_intros continuous_on_norm assms(2))+
then obtain x where x:"x\<in>s" "\<forall>y\<in>s. (norm \<circ> f) x \<le> (norm \<circ> f) y"
@@ -1161,7 +1161,7 @@
apply(drule_tac assms(1)[rule_format]) by auto }
hence "?R 0 \<or> ?R 1" by auto thus ?case by auto qed qed
-lemma brouwer_cube: fixes f::"real^'n::finite \<Rightarrow> real^'n::finite"
+lemma brouwer_cube: fixes f::"real^'n \<Rightarrow> real^'n"
assumes "continuous_on {0..1} f" "f ` {0..1} \<subseteq> {0..1}"
shows "\<exists>x\<in>{0..1}. f x = x" apply(rule ccontr) proof-
def n \<equiv> "CARD('n)" have n:"1 \<le> n" "0 < n" "n \<noteq> 0" unfolding n_def by auto
@@ -1291,7 +1291,7 @@
subsection {* Retractions. *}
-definition "retraction s t (r::real^'n::finite\<Rightarrow>real^'n) \<longleftrightarrow>
+definition "retraction s t (r::real^'n\<Rightarrow>real^'n) \<longleftrightarrow>
t \<subseteq> s \<and> continuous_on s r \<and> (r ` s \<subseteq> t) \<and> (\<forall>x\<in>t. r x = x)"
definition retract_of (infixl "retract'_of" 12) where
@@ -1302,7 +1302,7 @@
subsection {*preservation of fixpoints under (more general notion of) retraction. *}
-lemma invertible_fixpoint_property: fixes s::"(real^'n::finite) set" and t::"(real^'m::finite) set"
+lemma invertible_fixpoint_property: fixes s::"(real^'n) set" and t::"(real^'m) set"
assumes "continuous_on t i" "i ` t \<subseteq> s" "continuous_on s r" "r ` s \<subseteq> t" "\<forall>y\<in>t. r (i y) = y"
"\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)" "continuous_on t g" "g ` t \<subseteq> t"
obtains y where "y\<in>t" "g y = y" proof-
@@ -1315,7 +1315,7 @@
unfolding assms(5)[rule_format,OF *] using assms(4) by auto qed
lemma homeomorphic_fixpoint_property:
- fixes s::"(real^'n::finite) set" and t::"(real^'m::finite) set" assumes "s homeomorphic t"
+ fixes s::"(real^'n) set" and t::"(real^'m) set" assumes "s homeomorphic t"
shows "(\<forall>f. continuous_on s f \<and> f ` s \<subseteq> s \<longrightarrow> (\<exists>x\<in>s. f x = x)) \<longleftrightarrow>
(\<forall>g. continuous_on t g \<and> g ` t \<subseteq> t \<longrightarrow> (\<exists>y\<in>t. g y = y))" proof-
guess r using assms[unfolded homeomorphic_def homeomorphism_def] .. then guess i ..
@@ -1332,7 +1332,7 @@
subsection {*So the Brouwer theorem for any set with nonempty interior. *}
-lemma brouwer_weak: fixes f::"real^'n::finite \<Rightarrow> real^'n::finite"
+lemma brouwer_weak: fixes f::"real^'n \<Rightarrow> real^'n"
assumes "compact s" "convex s" "interior s \<noteq> {}" "continuous_on s f" "f ` s \<subseteq> s"
obtains x where "x \<in> s" "f x = x" proof-
have *:"interior {0..1::real^'n} \<noteq> {}" unfolding interior_closed_interval interval_eq_empty by auto
@@ -1343,7 +1343,7 @@
subsection {* And in particular for a closed ball. *}
-lemma brouwer_ball: fixes f::"real^'n::finite \<Rightarrow> real^'n::finite"
+lemma brouwer_ball: fixes f::"real^'n \<Rightarrow> real^'n"
assumes "0 < e" "continuous_on (cball a e) f" "f ` (cball a e) \<subseteq> (cball a e)"
obtains x where "x \<in> cball a e" "f x = x"
using brouwer_weak[OF compact_cball convex_cball,of a e f] unfolding interior_cball ball_eq_empty
@@ -1353,7 +1353,7 @@
rather involved HOMEOMORPHIC_CONVEX_COMPACT theorem, just using
a scaling and translation to put the set inside the unit cube. *}
-lemma brouwer: fixes f::"real^'n::finite \<Rightarrow> real^'n::finite"
+lemma brouwer: fixes f::"real^'n \<Rightarrow> real^'n"
assumes "compact s" "convex s" "s \<noteq> {}" "continuous_on s f" "f ` s \<subseteq> s"
obtains x where "x \<in> s" "f x = x" proof-
have "\<exists>e>0. s \<subseteq> cball 0 e" using compact_imp_bounded[OF assms(1)] unfolding bounded_pos
@@ -1389,7 +1389,7 @@
subsection {*Bijections between intervals. *}
-definition "interval_bij = (\<lambda> (a,b) (u,v) (x::real^'n::finite).
+definition "interval_bij = (\<lambda> (a,b) (u,v) (x::real^'n).
(\<chi> i. u$i + (x$i - a$i) / (b$i - a$i) * (v$i - u$i))::real^'n)"
lemma interval_bij_affine:
@@ -1399,7 +1399,7 @@
by(auto simp add:group_simps field_simps add_divide_distrib[THEN sym])
lemma continuous_interval_bij:
- "continuous (at x) (interval_bij (a,b::real^'n::finite) (u,v))"
+ "continuous (at x) (interval_bij (a,b::real^'n) (u,v))"
unfolding interval_bij_affine apply(rule continuous_intros)
apply(rule linear_continuous_at) unfolding linear_conv_bounded_linear[THEN sym]
unfolding linear_def unfolding Cart_eq unfolding Cart_lambda_beta defer
@@ -1413,7 +1413,7 @@
apply(cases "b=0") defer apply(rule divide_nonneg_pos) using assms by auto
lemma in_interval_interval_bij: assumes "x \<in> {a..b}" "{u..v} \<noteq> {}"
- shows "interval_bij (a,b) (u,v) x \<in> {u..v::real^'n::finite}"
+ shows "interval_bij (a,b) (u,v) x \<in> {u..v::real^'n}"
unfolding interval_bij_def split_conv mem_interval Cart_lambda_beta proof(rule,rule)
fix i::'n have "{a..b} \<noteq> {}" using assms by auto
hence *:"a$i \<le> b$i" "u$i \<le> v$i" using assms(2) unfolding interval_eq_empty not_ex apply-
@@ -1979,5 +1979,4 @@
==> connected((:real^N) DIFF path_image p)`,
SIMP_TAC[PATH_CONNECTED_ARC_COMPLEMENT; PATH_CONNECTED_IMP_CONNECTED]);; *)
-end
-
+end
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jan 07 17:43:35 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Thu Jan 07 18:56:39 2010 +0100
@@ -35,7 +35,7 @@
lemma nequals0I:"x\<in>A \<Longrightarrow> A \<noteq> {}" by auto
-lemma norm_not_0:"(x::real^'n::finite)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto
+lemma norm_not_0:"(x::real^'n)\<noteq>0 \<Longrightarrow> norm x \<noteq> 0" by auto
lemma setsum_delta_notmem: assumes "x\<notin>s"
shows "setsum (\<lambda>y. if (y = x) then P x else Q y) s = setsum Q s"
@@ -61,7 +61,7 @@
"(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 dest_vec1_def all_1)
-lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n::finite)) ` {a..b} =
+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})"
using image_affinity_interval[of m 0 a b] by auto
@@ -90,7 +90,7 @@
by(auto simp add:norm_minus_commute) qed
lemma norm_eqI:"x = y \<Longrightarrow> norm x = norm y" by auto
-lemma norm_minus_eqI:"(x::real^'n::finite) = - y \<Longrightarrow> norm x = norm y" by auto
+lemma norm_minus_eqI:"(x::real^'n) = - y \<Longrightarrow> norm x = norm y" by auto
lemma Min_grI: assumes "finite A" "A \<noteq> {}" "\<forall>a\<in>A. x < a" shows "x < Min A"
unfolding Min_gr_iff[OF assms(1,2)] using assms(3) by auto
@@ -418,7 +418,7 @@
lemma convex_halfspace_gt: "convex {x. inner a x > b}"
using convex_halfspace_lt[of "-a" "-b"] by auto
-lemma convex_positive_orthant: "convex {x::real^'n::finite. (\<forall>i. 0 \<le> x$i)}"
+lemma convex_positive_orthant: "convex {x::real^'n. (\<forall>i. 0 \<le> x$i)}"
unfolding convex_def apply auto apply(erule_tac x=i in allE)+
apply(rule add_nonneg_nonneg) by(auto simp add: mult_nonneg_nonneg)
@@ -1140,7 +1140,7 @@
thus ?thesis unfolding convex_def cone_def by auto
qed
-lemma affine_dependent_biggerset: fixes s::"(real^'n::finite) set"
+lemma affine_dependent_biggerset: fixes s::"(real^'n) set"
assumes "finite s" "card s \<ge> CARD('n) + 2"
shows "affine_dependent s"
proof-
@@ -1155,7 +1155,7 @@
apply(rule dependent_biggerset) by auto qed
lemma affine_dependent_biggerset_general:
- assumes "finite (s::(real^'n::finite) set)" "card s \<ge> dim s + 2"
+ assumes "finite (s::(real^'n) set)" "card s \<ge> dim s + 2"
shows "affine_dependent s"
proof-
from assms(2) have "s \<noteq> {}" by auto
@@ -1174,7 +1174,7 @@
subsection {* Caratheodory's theorem. *}
-lemma convex_hull_caratheodory: fixes p::"(real^'n::finite) set"
+lemma convex_hull_caratheodory: fixes p::"(real^'n) set"
shows "convex hull p = {y. \<exists>s u. finite s \<and> s \<subseteq> p \<and> card s \<le> CARD('n) + 1 \<and>
(\<forall>x\<in>s. 0 \<le> u x) \<and> setsum u s = 1 \<and> setsum (\<lambda>v. u v *\<^sub>R v) s = y}"
unfolding convex_hull_explicit expand_set_eq mem_Collect_eq
@@ -1231,7 +1231,7 @@
qed auto
lemma caratheodory:
- "convex hull p = {x::real^'n::finite. \<exists>s. finite s \<and> s \<subseteq> p \<and>
+ "convex hull p = {x::real^'n. \<exists>s. finite s \<and> s \<subseteq> p \<and>
card s \<le> CARD('n) + 1 \<and> x \<in> convex hull s}"
unfolding expand_set_eq apply(rule, rule) unfolding mem_Collect_eq proof-
fix x assume "x \<in> convex hull p"
@@ -1338,7 +1338,7 @@
done
qed
-lemma compact_convex_hull: fixes s::"(real^'n::finite) set"
+lemma compact_convex_hull: fixes s::"(real^'n) set"
assumes "compact s" shows "compact(convex hull s)"
proof(cases "s={}")
case True thus ?thesis using compact_empty by simp
@@ -1546,7 +1546,7 @@
subsection {* Closest point of a convex set is unique, with a continuous projection. *}
definition
- closest_point :: "(real ^ 'n::finite) set \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
+ closest_point :: "(real ^ 'n) set \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
"closest_point s a = (SOME x. x \<in> s \<and> (\<forall>y\<in>s. dist a x \<le> dist a y))"
lemma closest_point_exists:
@@ -1580,7 +1580,7 @@
lemma norm_le: "norm x \<le> norm y \<longleftrightarrow> inner x x \<le> inner y y"
unfolding norm_eq_sqrt_inner by simp
-lemma closer_points_lemma: fixes y::"real^'n::finite"
+lemma closer_points_lemma: fixes y::"real^'n"
assumes "inner y z > 0"
shows "\<exists>u>0. \<forall>v>0. v \<le> u \<longrightarrow> norm(v *\<^sub>R z - y) < norm y"
proof- have z:"inner z z > 0" unfolding inner_gt_zero_iff using assms by auto
@@ -1591,7 +1591,7 @@
qed(rule divide_pos_pos, auto) qed
lemma closer_point_lemma:
- fixes x y z :: "real ^ 'n::finite"
+ fixes x y z :: "real ^ 'n"
assumes "inner (y - x) (z - x) > 0"
shows "\<exists>u>0. u \<le> 1 \<and> dist (x + u *\<^sub>R (z - x)) y < dist x y"
proof- obtain u where "u>0" and u:"\<forall>v>0. v \<le> u \<longrightarrow> norm (v *\<^sub>R (z - x) - (y - x)) < norm (y - x)"
@@ -1718,10 +1718,10 @@
qed
lemma separating_hyperplane_closed_0:
- assumes "convex (s::(real^'n::finite) set)" "closed s" "0 \<notin> s"
+ assumes "convex (s::(real^'n) set)" "closed s" "0 \<notin> s"
shows "\<exists>a b. a \<noteq> 0 \<and> 0 < b \<and> (\<forall>x\<in>s. inner a x > b)"
proof(cases "s={}") guess a using UNIV_witness[where 'a='n] ..
- case True have "norm ((basis a)::real^'n::finite) = 1"
+ case True have "norm ((basis a)::real^'n) = 1"
using norm_basis and dimindex_ge_1 by auto
thus ?thesis apply(rule_tac x="basis a" in exI, rule_tac x=1 in exI) using True by auto
next case False thus ?thesis using False using separating_hyperplane_closed_point[OF assms]
@@ -1730,7 +1730,7 @@
subsection {* Now set-to-set for closed/compact sets. *}
lemma separating_hyperplane_closed_compact:
- assumes "convex (s::(real^'n::finite) set)" "closed s" "convex t" "compact t" "t \<noteq> {}" "s \<inter> t = {}"
+ assumes "convex (s::(real^'n) set)" "closed s" "convex t" "compact t" "t \<noteq> {}" "s \<inter> t = {}"
shows "\<exists>a b. (\<forall>x\<in>s. inner a x < b) \<and> (\<forall>x\<in>t. inner a x > b)"
proof(cases "s={}")
case True
@@ -1772,7 +1772,7 @@
subsection {* General case without assuming closure and getting non-strict separation. *}
lemma separating_hyperplane_set_0:
- assumes "convex s" "(0::real^'n::finite) \<notin> s"
+ assumes "convex s" "(0::real^'n) \<notin> s"
shows "\<exists>a. a \<noteq> 0 \<and> (\<forall>x\<in>s. 0 \<le> inner a x)"
proof- let ?k = "\<lambda>c. {x::real^'n. 0 \<le> inner c x}"
have "frontier (cball 0 1) \<inter> (\<Inter> (?k ` s)) \<noteq> {}"
@@ -1794,7 +1794,7 @@
thus ?thesis apply(rule_tac x=x in exI) by(auto simp add: inner_commute) qed
lemma separating_hyperplane_sets:
- assumes "convex s" "convex (t::(real^'n::finite) set)" "s \<noteq> {}" "t \<noteq> {}" "s \<inter> t = {}"
+ assumes "convex s" "convex (t::(real^'n) set)" "s \<noteq> {}" "t \<noteq> {}" "s \<inter> t = {}"
shows "\<exists>a b. a \<noteq> 0 \<and> (\<forall>x\<in>s. inner a x \<le> b) \<and> (\<forall>x\<in>t. inner a x \<ge> b)"
proof- from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
obtain a where "a\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x"
@@ -1955,7 +1955,7 @@
subsection {* Helly's theorem. *}
-lemma helly_induct: fixes f::"(real^'n::finite) set set"
+lemma helly_induct: fixes f::"(real^'n) set set"
assumes "card f = n" "n \<ge> CARD('n) + 1"
"\<forall>s\<in>f. convex s" "\<forall>t\<subseteq>f. card t = CARD('n) + 1 \<longrightarrow> \<Inter> t \<noteq> {}"
shows "\<Inter> f \<noteq> {}"
@@ -1993,7 +1993,7 @@
thus ?thesis unfolding f using mp(3)[unfolded gh] by blast qed
qed(insert dimindex_ge_1, auto) qed(auto)
-lemma helly: fixes f::"(real^'n::finite) set set"
+lemma helly: fixes f::"(real^'n) set set"
assumes "card f \<ge> CARD('n) + 1" "\<forall>s\<in>f. convex s"
"\<forall>t\<subseteq>f. card t = CARD('n) + 1 \<longrightarrow> \<Inter> t \<noteq> {}"
shows "\<Inter> f \<noteq>{}"
@@ -2062,9 +2062,9 @@
apply(rule,rule,rule ccontr) apply(rule u_max) by auto qed
lemma starlike_compact_projective:
- assumes "compact s" "cball (0::real^'n::finite) 1 \<subseteq> s "
+ assumes "compact s" "cball (0::real^'n) 1 \<subseteq> s "
"\<forall>x\<in>s. \<forall>u. 0 \<le> u \<and> u < 1 \<longrightarrow> (u *\<^sub>R x) \<in> (s - frontier s )"
- shows "s homeomorphic (cball (0::real^'n::finite) 1)"
+ shows "s homeomorphic (cball (0::real^'n) 1)"
proof-
have fs:"frontier s \<subseteq> s" apply(rule frontier_subset_closed) using compact_imp_closed[OF assms(1)] by simp
def pi \<equiv> "\<lambda>x::real^'n. inverse (norm x) *\<^sub>R x"
@@ -2200,7 +2200,7 @@
ultimately show ?thesis using injpi by auto qed qed
qed auto qed
-lemma homeomorphic_convex_compact_lemma: fixes s::"(real^'n::finite) set"
+lemma homeomorphic_convex_compact_lemma: fixes s::"(real^'n) set"
assumes "convex s" "compact s" "cball 0 1 \<subseteq> s"
shows "s homeomorphic (cball (0::real^'n) 1)"
apply(rule starlike_compact_projective[OF assms(2-3)]) proof(rule,rule,rule,erule conjE)
@@ -2218,9 +2218,9 @@
using as unfolding scaleR_scaleR by auto qed auto
thus "u *\<^sub>R x \<in> s - frontier s" using frontier_def and interior_subset by auto qed
-lemma homeomorphic_convex_compact_cball: fixes e::real and s::"(real^'n::finite) set"
+lemma homeomorphic_convex_compact_cball: fixes e::real and s::"(real^'n) set"
assumes "convex s" "compact s" "interior s \<noteq> {}" "0 < e"
- shows "s homeomorphic (cball (b::real^'n::finite) e)"
+ shows "s homeomorphic (cball (b::real^'n) e)"
proof- obtain a where "a\<in>interior s" using assms(3) by auto
then obtain d where "d>0" and d:"cball a d \<subseteq> s" unfolding mem_interior_cball by auto
let ?d = "inverse d" and ?n = "0::real^'n"
@@ -2235,7 +2235,7 @@
apply(rule homeomorphic_trans[OF homeomorphic_affinity[of "?d" s "?d *\<^sub>R -a"]])
using `d>0` `e>0` by(auto simp add: uminus_add_conv_diff scaleR_right_diff_distrib) qed
-lemma homeomorphic_convex_compact: fixes s::"(real^'n::finite) set" and t::"(real^'n) set"
+lemma homeomorphic_convex_compact: fixes s::"(real^'n) set" and t::"(real^'n) set"
assumes "convex s" "compact s" "interior s \<noteq> {}"
"convex t" "compact t" "interior t \<noteq> {}"
shows "s homeomorphic t"
@@ -2243,7 +2243,7 @@
subsection {* Epigraphs of convex functions. *}
-definition "epigraph s (f::real^'n::finite \<Rightarrow> real) = {xy. fstcart xy \<in> s \<and> f(fstcart xy) \<le> dest_vec1 (sndcart xy)}"
+definition "epigraph s (f::real^'n \<Rightarrow> real) = {xy. fstcart xy \<in> s \<and> f(fstcart xy) \<le> dest_vec1 (sndcart xy)}"
lemma mem_epigraph: "(pastecart x (vec1 y)) \<in> epigraph s f \<longleftrightarrow> x \<in> s \<and> f x \<le> y" unfolding epigraph_def by auto
@@ -2317,7 +2317,7 @@
shows "is_interval s \<Longrightarrow> connected s"
using is_interval_convex convex_connected by auto
-lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n::finite}"
+lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n}"
apply(rule_tac[!] is_interval_convex) using is_interval_interval by auto
subsection {* On @{text "real^1"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}
@@ -2351,7 +2351,7 @@
subsection {* Another intermediate value theorem formulation. *}
-lemma ivt_increasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n::finite"
+lemma ivt_increasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n"
assumes "dest_vec1 a \<le> dest_vec1 b" "continuous_on {a .. b} f" "(f a)$k \<le> y" "y \<le> (f b)$k"
shows "\<exists>x\<in>{a..b}. (f x)$k = y"
proof- have "f a \<in> f ` {a..b}" "f b \<in> f ` {a..b}" apply(rule_tac[!] imageI)
@@ -2360,20 +2360,20 @@
using connected_continuous_image[OF assms(2) convex_connected[OF convex_interval(1)]]
using assms by(auto intro!: imageI) qed
-lemma ivt_increasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n::finite"
+lemma ivt_increasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n"
assumes "dest_vec1 a \<le> dest_vec1 b"
"\<forall>x\<in>{a .. b}. continuous (at x) f" "f a$k \<le> y" "y \<le> f b$k"
shows "\<exists>x\<in>{a..b}. (f x)$k = y"
apply(rule ivt_increasing_component_on_1) using assms using continuous_at_imp_continuous_on by auto
-lemma ivt_decreasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n::finite"
+lemma ivt_decreasing_component_on_1: fixes f::"real^1 \<Rightarrow> real^'n"
assumes "dest_vec1 a \<le> dest_vec1 b" "continuous_on {a .. b} f" "(f b)$k \<le> y" "y \<le> (f a)$k"
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)
-lemma ivt_decreasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n::finite"
+lemma ivt_decreasing_component_1: fixes f::"real^1 \<Rightarrow> real^'n"
assumes "dest_vec1 a \<le> dest_vec1 b" "\<forall>x\<in>{a .. b}. continuous (at x) f" "f b$k \<le> y" "y \<le> f a$k"
shows "\<exists>x\<in>{a..b}. (f x)$k = y"
apply(rule ivt_decreasing_component_on_1) using assms using continuous_at_imp_continuous_on by auto
@@ -2394,7 +2394,7 @@
unfolding obt(2-3) using obt(1) and hull_subset[unfolded subset_eq, rule_format, of _ s] by auto qed
lemma unit_interval_convex_hull:
- "{0::real^'n::finite .. 1} = convex hull {x. \<forall>i. (x$i = 0) \<or> (x$i = 1)}" (is "?int = convex hull ?points")
+ "{0::real^'n .. 1} = convex hull {x. \<forall>i. (x$i = 0) \<or> (x$i = 1)}" (is "?int = convex hull ?points")
proof- have 01:"{0,1} \<subseteq> convex hull ?points" apply rule apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) by auto
{ fix n x assume "x\<in>{0::real^'n .. 1}" "n \<le> CARD('n)" "card {i. x$i \<noteq> 0} \<le> n"
hence "x\<in>convex hull ?points" proof(induct n arbitrary: x)
@@ -2430,8 +2430,8 @@
using Suc(2)[unfolded mem_interval, rule_format, of j] by(auto simp add:field_simps Cart_lambda_beta)
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)
- hence "{j. x$j \<noteq> 0} \<noteq> {j. ((\<chi> j. ?y j)::real^'n::finite) $ j \<noteq> 0}" by auto
- hence **:"{j. ((\<chi> j. ?y j)::real^'n::finite) $ j \<noteq> 0} \<subset> {j. x$j \<noteq> 0}" apply - apply rule by(auto simp add: Cart_lambda_beta)
+ 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)
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))
@@ -2444,9 +2444,9 @@
subsection {* And this is a finite set of vertices. *}
-lemma unit_cube_convex_hull: obtains s where "finite s" "{0 .. 1::real^'n::finite} = convex hull s"
- apply(rule that[of "{x::real^'n::finite. \<forall>i. x$i=0 \<or> x$i=1}"])
- apply(rule finite_subset[of _ "(\<lambda>s. (\<chi> i. if i\<in>s then 1::real else 0)::real^'n::finite) ` UNIV"])
+lemma unit_cube_convex_hull: obtains s where "finite s" "{0 .. 1::real^'n} = convex hull s"
+ apply(rule that[of "{x::real^'n. \<forall>i. x$i=0 \<or> x$i=1}"])
+ apply(rule finite_subset[of _ "(\<lambda>s. (\<chi> i. if i\<in>s then 1::real else 0)::real^'n) ` UNIV"])
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}"])
@@ -2455,7 +2455,7 @@
subsection {* Hence any cube (could do any nonempty interval). *}
lemma cube_convex_hull:
- assumes "0 < d" obtains s::"(real^'n::finite) set" where "finite s" "{x - (\<chi> i. d) .. x + (\<chi> i. d)} = convex hull s" proof-
+ assumes "0 < d" obtains s::"(real^'n) set" where "finite s" "{x - (\<chi> i. d) .. x + (\<chi> i. d)} = convex hull s" proof-
let ?d = "(\<chi> i. d)::real^'n"
have *:"{x - ?d .. x + ?d} = (\<lambda>y. x - ?d + (2 * d) *\<^sub>R y) ` {0 .. 1}" apply(rule set_ext, rule)
unfolding image_iff defer apply(erule bexE) proof-
@@ -2552,7 +2552,7 @@
subsection {* Hence a convex function on an open set is continuous. *}
lemma convex_on_continuous:
- assumes "open (s::(real^'n::finite) set)" "convex_on s f"
+ assumes "open (s::(real^'n) set)" "convex_on s f"
shows "continuous_on s f"
unfolding continuous_on_eq_continuous_at[OF assms(1)] proof
note dimge1 = dimindex_ge_1[where 'a='n]
@@ -2597,15 +2597,15 @@
segment[a,b] is closed and segment(a,b) is open relative to affine hull. *)
definition
- midpoint :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
+ midpoint :: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
"midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
definition
- open_segment :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> (real ^ 'n) set" where
+ open_segment :: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> (real ^ 'n) set" where
"open_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 < u \<and> u < 1}"
definition
- closed_segment :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> (real ^ 'n) set" where
+ closed_segment :: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> (real ^ 'n) set" where
"closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
definition "between = (\<lambda> (a,b). closed_segment a b)"
@@ -2625,8 +2625,8 @@
"dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
"dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
proof-
- have *: "\<And>x y::real^'n::finite. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2" unfolding equation_minus_iff by auto
- have **:"\<And>x y::real^'n::finite. 2 *\<^sub>R x = y \<Longrightarrow> norm x = (norm y) / 2" by auto
+ have *: "\<And>x y::real^'n. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2" unfolding equation_minus_iff by auto
+ have **:"\<And>x y::real^'n. 2 *\<^sub>R x = y \<Longrightarrow> norm x = (norm y) / 2" by auto
note scaleR_right_distrib [simp]
show ?t1 unfolding midpoint_def dist_norm apply (rule **) by(auto,vector)
show ?t2 unfolding midpoint_def dist_norm apply (rule *) by(auto,vector)
@@ -2634,7 +2634,7 @@
show ?t4 unfolding midpoint_def dist_norm apply (rule **) by(auto,vector) qed
lemma midpoint_eq_endpoint:
- "midpoint a b = a \<longleftrightarrow> a = (b::real^'n::finite)"
+ "midpoint a b = a \<longleftrightarrow> a = (b::real^'n)"
"midpoint a b = b \<longleftrightarrow> a = b"
unfolding dist_eq_0_iff[where 'a="real^'n", THEN sym] dist_midpoint by auto
@@ -2679,7 +2679,7 @@
lemma between_mem_segment: "between (a,b) x \<longleftrightarrow> x \<in> closed_segment a b"
unfolding between_def mem_def by auto
-lemma between:"between (a,b) (x::real^'n::finite) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)"
+lemma between:"between (a,b) (x::real^'n) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)"
proof(cases "a = b")
case True thus ?thesis unfolding between_def split_conv mem_def[of x, symmetric]
by(auto simp add:segment_refl dist_commute) next
@@ -2706,7 +2706,7 @@
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
-lemma between_midpoint: fixes a::"real^'n::finite" shows
+lemma between_midpoint: fixes a::"real^'n" shows
"between (a,b) (midpoint a b)" (is ?t1)
"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
@@ -2776,7 +2776,7 @@
lemma std_simplex:
"convex hull (insert 0 { basis i | i. i\<in>UNIV}) =
- {x::real^'n::finite . (\<forall>i. 0 \<le> x$i) \<and> setsum (\<lambda>i. x$i) UNIV \<le> 1 }" (is "convex hull (insert 0 ?p) = ?s")
+ {x::real^'n . (\<forall>i. 0 \<le> x$i) \<and> setsum (\<lambda>i. x$i) UNIV \<le> 1 }" (is "convex hull (insert 0 ?p) = ?s")
proof- let ?D = "UNIV::'n set"
have "0\<notin>?p" by(auto simp add: basis_nonzero)
have "{(basis i)::real^'n |i. i \<in> ?D} = basis ` ?D" by auto
@@ -2796,7 +2796,7 @@
lemma interior_std_simplex:
"interior (convex hull (insert 0 { basis i| i. i\<in>UNIV})) =
- {x::real^'n::finite. (\<forall>i. 0 < x$i) \<and> setsum (\<lambda>i. x$i) UNIV < 1 }"
+ {x::real^'n. (\<forall>i. 0 < x$i) \<and> setsum (\<lambda>i. x$i) UNIV < 1 }"
apply(rule set_ext) unfolding mem_interior std_simplex unfolding subset_eq mem_Collect_eq Ball_def mem_ball
unfolding Ball_def[symmetric] apply rule apply(erule exE, (erule conjE)+) defer apply(erule conjE) proof-
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"
@@ -2813,7 +2813,7 @@
also have "\<dots> \<le> 1" using ** apply(drule_tac as[rule_format]) by auto
finally show "setsum (op $ x) UNIV < 1" by auto qed
next
- fix x::"real^'n::finite" assume as:"\<forall>i. 0 < x $ i" "setsum (op $ x) UNIV < 1"
+ fix x::"real^'n" assume as:"\<forall>i. 0 < x $ i" "setsum (op $ x) UNIV < 1"
guess a using UNIV_witness[where 'a='b] ..
let ?d = "(1 - setsum (op $ x) UNIV) / real (CARD('n))"
have "Min ((op $ x) ` UNIV) > 0" apply(rule Min_grI) using as(1) dimindex_ge_1 by auto
@@ -2832,7 +2832,7 @@
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)
qed auto qed auto qed
-lemma interior_std_simplex_nonempty: obtains a::"real^'n::finite" where
+lemma interior_std_simplex_nonempty: obtains a::"real^'n" where
"a \<in> interior(convex hull (insert 0 {basis i | i . i \<in> UNIV}))" proof-
let ?D = "UNIV::'n set" let ?a = "setsum (\<lambda>b::real^'n. inverse (2 * real CARD('n)) *\<^sub>R b) {(basis i) | i. i \<in> ?D}"
have *:"{basis i :: real ^ 'n | i. i \<in> ?D} = basis ` ?D" by auto
@@ -2849,7 +2849,7 @@
subsection {* Paths. *}
-definition "path (g::real^1 \<Rightarrow> real^'n::finite) \<longleftrightarrow> continuous_on {0 .. 1} g"
+definition "path (g::real^1 \<Rightarrow> real^'n) \<longleftrightarrow> continuous_on {0 .. 1} g"
definition "pathstart (g::real^1 \<Rightarrow> real^'n) = g 0"
@@ -3138,7 +3138,7 @@
subsection {* Special case of straight-line paths. *}
definition
- linepath :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 1 \<Rightarrow> real ^ 'n" where
+ linepath :: "real ^ 'n \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 1 \<Rightarrow> real ^ 'n" where
"linepath a b = (\<lambda>x. (1 - dest_vec1 x) *\<^sub>R a + dest_vec1 x *\<^sub>R b)"
lemma pathstart_linepath[simp]: "pathstart(linepath a b) = a"
@@ -3323,7 +3323,7 @@
subsection {* sphere is path-connected. *}
lemma path_connected_punctured_universe:
- assumes "2 \<le> CARD('n::finite)" shows "path_connected((UNIV::(real^'n::finite) set) - {a})" proof-
+ assumes "2 \<le> CARD('n::finite)" shows "path_connected((UNIV::(real^'n) set) - {a})" proof-
obtain \<psi> where \<psi>:"bij_betw \<psi> {1..CARD('n)} (UNIV::'n set)" using ex_bij_betw_nat_finite_1[OF finite_UNIV] by auto
let ?U = "UNIV::(real^'n) set" let ?u = "?U - {0}"
let ?basis = "\<lambda>k. basis (\<psi> k)"
@@ -3366,7 +3366,7 @@
show ?thesis unfolding * apply(rule path_connected_continuous_image) apply(rule continuous_on_intros)+
unfolding ** apply(rule lem[THEN bspec[where x="CARD('n)"], unfolded ***]) using assms by auto qed
-lemma path_connected_sphere: assumes "2 \<le> CARD('n::finite)" shows "path_connected {x::real^'n::finite. norm(x - a) = r}" proof(cases "r\<le>0")
+lemma path_connected_sphere: assumes "2 \<le> CARD('n::finite)" shows "path_connected {x::real^'n. norm(x - a) = r}" proof(cases "r\<le>0")
case True thus ?thesis proof(cases "r=0")
case False hence "{x::real^'n. norm(x - a) = r} = {}" using True by auto
thus ?thesis using path_connected_empty by auto
@@ -3381,7 +3381,7 @@
thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms]
by(auto intro!: path_connected_continuous_image continuous_on_intros continuous_on_mul) qed
-lemma connected_sphere: "2 \<le> CARD('n) \<Longrightarrow> connected {x::real^'n::finite. norm(x - a) = r}"
+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
-
+
end
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Jan 07 17:43:35 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Thu Jan 07 18:56:39 2010 +0100
@@ -122,7 +122,7 @@
"((f \<circ> dest_vec1) has_derivative (f' \<circ> dest_vec1)) (at (vec1 x)) = (f has_derivative f') (at x)"
using has_derivative_within_dest_vec1[where s=UNIV] by(auto simp add:within_UNIV)
-lemma derivative_is_linear: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite" shows
+lemma derivative_is_linear: fixes f::"real^'a \<Rightarrow> real^'b" shows
"(f has_derivative f') net \<Longrightarrow> linear f'"
unfolding has_derivative_def and linear_conv_bounded_linear by auto
@@ -194,7 +194,7 @@
subsection {* somewhat different results for derivative of scalar multiplier. *}
-lemma has_derivative_vmul_component: fixes c::"real^'a::finite \<Rightarrow> real^'b::finite" and v::"real^'c::finite"
+lemma has_derivative_vmul_component: fixes c::"real^'a \<Rightarrow> real^'b" and v::"real^'c"
assumes "(c has_derivative c') net"
shows "((\<lambda>x. c(x)$k *\<^sub>R v) has_derivative (\<lambda>x. (c' x)$k *\<^sub>R v)) net" proof-
have *:"\<And>y. (c y $ k *\<^sub>R v - (c (netlimit net) $ k *\<^sub>R v + c' (y - netlimit net) $ k *\<^sub>R v)) =
@@ -205,7 +205,7 @@
apply(subst vector_smult_lzero[THEN sym, of v]) unfolding scaleR_scaleR smult_conv_scaleR apply(rule Lim_vmul)
using assms[unfolded has_derivative_def] unfolding Lim o_def apply- apply(cases "trivial_limit net")
apply(rule,assumption,rule disjI2,rule,rule) proof-
- have *:"\<And>x. x - vec 0 = (x::real^'n::finite)" by auto
+ have *:"\<And>x. x - vec 0 = (x::real^'n)" by auto
have **:"\<And>d x. d * (c x $ k - (c (netlimit net) $ k + c' (x - netlimit net) $ k)) = (d *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net) ))) $k" by(auto simp add:field_simps)
fix e assume "\<not> trivial_limit net" "0 < (e::real)"
then have "eventually (\<lambda>x. dist ((1 / norm (x - netlimit net)) *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net)))) 0 < e) net"
@@ -217,14 +217,14 @@
qed
qed(insert assms[unfolded has_derivative_def], auto simp add:linear_conv_bounded_linear) qed
-lemma has_derivative_vmul_within: fixes c::"real \<Rightarrow> real" and v::"real^'a::finite"
+lemma has_derivative_vmul_within: fixes c::"real \<Rightarrow> real" and v::"real^'a"
assumes "(c has_derivative c') (at x within s)"
shows "((\<lambda>x. (c x) *\<^sub>R v) has_derivative (\<lambda>x. (c' x) *\<^sub>R v)) (at x within s)" proof-
have *:"\<And>c. (\<lambda>x. (vec1 \<circ> c \<circ> dest_vec1) x $ 1 *\<^sub>R v) = (\<lambda>x. (c x) *\<^sub>R v) \<circ> dest_vec1" unfolding o_def by auto
show ?thesis using has_derivative_vmul_component[of "vec1 \<circ> c \<circ> dest_vec1" "vec1 \<circ> c' \<circ> dest_vec1" "at (vec1 x) within vec1 ` s" 1 v]
unfolding * and has_derivative_within_vec1_dest_vec1 unfolding has_derivative_within_dest_vec1 using assms by auto qed
-lemma has_derivative_vmul_at: fixes c::"real \<Rightarrow> real" and v::"real^'a::finite"
+lemma has_derivative_vmul_at: fixes c::"real \<Rightarrow> real" and v::"real^'a"
assumes "(c has_derivative c') (at x)"
shows "((\<lambda>x. (c x) *\<^sub>R v) has_derivative (\<lambda>x. (c' x) *\<^sub>R v)) (at x)"
using has_derivative_vmul_within[where s=UNIV] and assms by(auto simp add: within_UNIV)
@@ -281,7 +281,7 @@
"f differentiable (at a within s) \<longleftrightarrow> (f differentiable (at a))"
unfolding differentiable_def has_derivative_within_open[OF assms] by auto
-lemma differentiable_at_imp_differentiable_on: "(\<forall>x\<in>(s::(real^'n::finite) set). f differentiable at x) \<Longrightarrow> f differentiable_on s"
+lemma differentiable_at_imp_differentiable_on: "(\<forall>x\<in>(s::(real^'n) set). f differentiable at x) \<Longrightarrow> f differentiable_on s"
unfolding differentiable_on_def by(auto intro!: differentiable_at_withinI)
lemma differentiable_on_eq_differentiable_at: "open s \<Longrightarrow> (f differentiable_on s \<longleftrightarrow> (\<forall>x\<in>s. f differentiable at x))"
@@ -305,13 +305,13 @@
"f differentiable net \<longleftrightarrow> (f has_derivative (frechet_derivative f net)) net"
unfolding frechet_derivative_def differentiable_def and some_eq_ex[of "\<lambda> f' . (f has_derivative f') net"] ..
-lemma linear_frechet_derivative: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
+lemma linear_frechet_derivative: fixes f::"real^'a \<Rightarrow> real^'b"
shows "f differentiable net \<Longrightarrow> linear(frechet_derivative f net)"
unfolding frechet_derivative_works has_derivative_def unfolding linear_conv_bounded_linear by auto
definition "jacobian f net = matrix(frechet_derivative f net)"
-lemma jacobian_works: "(f::(real^'a::finite) \<Rightarrow> (real^'b::finite)) differentiable net \<longleftrightarrow> (f has_derivative (\<lambda>h. (jacobian f net) *v h)) net"
+lemma jacobian_works: "(f::(real^'a) \<Rightarrow> (real^'b)) differentiable net \<longleftrightarrow> (f has_derivative (\<lambda>h. (jacobian f net) *v h)) net"
apply rule unfolding jacobian_def apply(simp only: matrix_works[OF linear_frechet_derivative]) defer
apply(rule differentiableI) apply assumption unfolding frechet_derivative_works by assumption
@@ -387,7 +387,7 @@
apply(rule_tac le_less_trans[of _ "e/2"]) by(auto intro!:mult_imp_div_pos_le simp add:group_simps) qed auto qed
lemma has_derivative_at_alt:
- "(f has_derivative f') (at (x::real^'n::finite)) \<longleftrightarrow> bounded_linear f' \<and>
+ "(f has_derivative f') (at (x::real^'n)) \<longleftrightarrow> bounded_linear f' \<and>
(\<forall>e>0. \<exists>d>0. \<forall>y. norm(y - x) < d \<longrightarrow> norm(f y - f x - f'(y - x)) \<le> e * norm(y - x))"
using has_derivative_within_alt[where s=UNIV] unfolding within_UNIV by auto
@@ -474,13 +474,13 @@
unfolding differentiable_def apply(erule exE)+ apply(rule_tac x="\<lambda>z. f' z - f'a z" in exI)
apply(rule has_derivative_sub) by auto
-lemma differentiable_setsum: fixes f::"'a \<Rightarrow> (real^'n::finite \<Rightarrow>real^'n)"
+lemma differentiable_setsum: fixes f::"'a \<Rightarrow> (real^'n \<Rightarrow>real^'n)"
assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net"
shows "(\<lambda>x. setsum (\<lambda>a. f a x) s) differentiable net" proof-
guess f' using bchoice[OF assms(2)[unfolded differentiable_def]] ..
thus ?thesis unfolding differentiable_def apply- apply(rule,rule has_derivative_setsum[where f'=f'],rule assms(1)) by auto qed
-lemma differentiable_setsum_numseg: fixes f::"_ \<Rightarrow> (real^'n::finite \<Rightarrow>real^'n)"
+lemma differentiable_setsum_numseg: fixes f::"_ \<Rightarrow> (real^'n \<Rightarrow>real^'n)"
shows "\<forall>i. m \<le> i \<and> i \<le> n \<longrightarrow> (f i) differentiable net \<Longrightarrow> (\<lambda>x. setsum (\<lambda>a. f a x) {m::nat..n}) differentiable net"
apply(rule differentiable_setsum) using finite_atLeastAtMost[of n m] by auto
@@ -498,7 +498,7 @@
(* The general result is a bit messy because we need approachability of the *)
(* limit point from any direction. But OK for nontrivial intervals etc. *}
-lemma frechet_derivative_unique_within: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
+lemma frechet_derivative_unique_within: fixes f::"real^'a \<Rightarrow> real^'b"
assumes "(f has_derivative f') (at x within s)" "(f has_derivative f'') (at x within s)"
"(\<forall>i::'a::finite. \<forall>e>0. \<exists>d. 0 < abs(d) \<and> abs(d) < e \<and> (x + d *\<^sub>R basis i) \<in> s)" shows "f' = f''" proof-
note as = assms(1,2)[unfolded has_derivative_def]
@@ -523,7 +523,7 @@
finally show False using c using d[THEN conjunct2,rule_format,of "x + c *\<^sub>R basis i"] using norm_basis[of i] unfolding vector_dist_norm
unfolding f'.scaleR f''.scaleR f'.add f''.add f'.diff f''.diff scaleR_scaleR scaleR_right_diff_distrib scaleR_right_distrib by auto qed qed
-lemma frechet_derivative_unique_at: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
+lemma frechet_derivative_unique_at: fixes f::"real^'a \<Rightarrow> real^'b"
shows "(f has_derivative f') (at x) \<Longrightarrow> (f has_derivative f'') (at x) \<Longrightarrow> f' = f''"
apply(rule frechet_derivative_unique_within[of f f' x UNIV f'']) unfolding within_UNIV apply(assumption)+
apply(rule,rule,rule) apply(rule_tac x="e/2" in exI) by auto
@@ -531,7 +531,7 @@
lemma "isCont f x = continuous (at x) f" unfolding isCont_def LIM_def
unfolding continuous_at Lim_at unfolding dist_nz by auto
-lemma frechet_derivative_unique_within_closed_interval: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
+lemma frechet_derivative_unique_within_closed_interval: fixes f::"real^'a \<Rightarrow> real^'b"
assumes "\<forall>i. a$i < b$i" "x \<in> {a..b}" (is "x\<in>?I") and
"(f has_derivative f' ) (at x within {a..b})" and
"(f has_derivative f'') (at x within {a..b})"
@@ -552,7 +552,7 @@
using assms(1)[THEN spec[where x=i]] and `e>0` and assms(2)
unfolding mem_interval by(auto simp add:field_simps) qed qed
-lemma frechet_derivative_unique_within_open_interval: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
+lemma frechet_derivative_unique_within_open_interval: fixes f::"real^'a \<Rightarrow> real^'b"
assumes "x \<in> {a<..<b}" "(f has_derivative f' ) (at x within {a<..<b})"
"(f has_derivative f'') (at x within {a<..<b})"
shows "f' = f''" apply(rule frechet_derivative_unique_within) apply(rule assms(2-3))+ proof(rule,rule,rule)
@@ -568,12 +568,12 @@
apply(rule_tac x="- (min (x$i - a$i) e) / 2" in exI)
using `e>0` and assms(1) unfolding mem_interval by(auto simp add:field_simps) qed
-lemma frechet_derivative_at: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
+lemma frechet_derivative_at: fixes f::"real^'a \<Rightarrow> real^'b"
shows "(f has_derivative f') (at x) \<Longrightarrow> (f' = frechet_derivative f (at x))"
apply(rule frechet_derivative_unique_at[of f],assumption)
unfolding frechet_derivative_works[THEN sym] using differentiable_def by auto
-lemma frechet_derivative_within_closed_interval: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
+lemma frechet_derivative_within_closed_interval: fixes f::"real^'a \<Rightarrow> real^'b"
assumes "\<forall>i. a$i < b$i" "x \<in> {a..b}" "(f has_derivative f') (at x within {a.. b})"
shows "frechet_derivative f (at x within {a.. b}) = f'"
apply(rule frechet_derivative_unique_within_closed_interval[where f=f])
@@ -583,7 +583,7 @@
subsection {* Component of the differential must be zero if it exists at a local *)
(* maximum or minimum for that corresponding component. *}
-lemma differential_zero_maxmin_component: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
+lemma differential_zero_maxmin_component: fixes f::"real^'a \<Rightarrow> real^'b"
assumes "0 < e" "((\<forall>y \<in> ball x e. (f y)$k \<le> (f x)$k) \<or> (\<forall>y\<in>ball x e. (f x)$k \<le> (f y)$k))"
"f differentiable (at x)" shows "jacobian f (at x) $ k = 0" proof(rule ccontr)
def D \<equiv> "jacobian f (at x)" assume "jacobian f (at x) $ k \<noteq> 0"
@@ -611,7 +611,7 @@
subsection {* In particular if we have a mapping into R^1. *}
-lemma differential_zero_maxmin: fixes f::"real^'a::finite \<Rightarrow> real"
+lemma differential_zero_maxmin: fixes f::"real^'a \<Rightarrow> real"
assumes "x \<in> s" "open s" "(f has_derivative f') (at x)"
"(\<forall>y\<in>s. f y \<le> f x) \<or> (\<forall>y\<in>s. f x \<le> f y)"
shows "f' = (\<lambda>v. 0)" proof-
@@ -688,10 +688,10 @@
subsection {* A nice generalization (see Havin's proof of 5.19 from Rudin's book). *}
-lemma inner_eq_dot: fixes a::"real^'n::finite"
+lemma inner_eq_dot: fixes a::"real^'n"
shows "a \<bullet> b = inner a b" unfolding inner_vector_def dot_def by auto
-lemma mvt_general: fixes f::"real\<Rightarrow>real^'n::finite"
+lemma mvt_general: fixes f::"real\<Rightarrow>real^'n"
assumes "a<b" "continuous_on {a..b} f" "\<forall>x\<in>{a<..<b}. (f has_derivative f'(x)) (at x)"
shows "\<exists>x\<in>{a<..<b}. norm(f b - f a) \<le> norm(f'(x) (b - a))" proof-
have "\<exists>x\<in>{a<..<b}. (op \<bullet> (f b - f a) \<circ> f) b - (op \<bullet> (f b - f a) \<circ> f) a = (f b - f a) \<bullet> f' x (b - a)"
@@ -708,7 +708,7 @@
subsection {* Still more general bound theorem. *}
-lemma differentiable_bound: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
+lemma differentiable_bound: fixes f::"real^'a \<Rightarrow> real^'b"
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"
shows "norm(f x - f y) \<le> B * norm(x - y)" proof-
let ?p = "\<lambda>u. x + u *\<^sub>R (y - x)"
@@ -771,7 +771,7 @@
subsection {* Differentiability of inverse function (most basic form). *}
-lemma has_derivative_inverse_basic: fixes f::"real^'b::finite \<Rightarrow> real^'c::finite"
+lemma has_derivative_inverse_basic: fixes f::"real^'b \<Rightarrow> real^'c"
assumes "(f has_derivative f') (at (g y))" "bounded_linear g'" "g' \<circ> f' = id" "continuous (at y) g"
"open t" "y \<in> t" "\<forall>z\<in>t. f(g z) = z"
shows "(g has_derivative g') (at y)" proof-
@@ -815,7 +815,7 @@
subsection {* Simply rewrite that based on the domain point x. *}
-lemma has_derivative_inverse_basic_x: fixes f::"real^'b::finite \<Rightarrow> real^'c::finite"
+lemma has_derivative_inverse_basic_x: fixes f::"real^'b \<Rightarrow> real^'c"
assumes "(f has_derivative f') (at x)" "bounded_linear g'" "g' o f' = id"
"continuous (at (f x)) g" "g(f x) = x" "open t" "f x \<in> t" "\<forall>y\<in>t. f(g y) = y"
shows "(g has_derivative g') (at (f(x)))"
@@ -823,7 +823,7 @@
subsection {* This is the version in Dieudonne', assuming continuity of f and g. *}
-lemma has_derivative_inverse_dieudonne: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
+lemma has_derivative_inverse_dieudonne: fixes f::"real^'a \<Rightarrow> real^'b"
assumes "open s" "open (f ` s)" "continuous_on s f" "continuous_on (f ` s) g" "\<forall>x\<in>s. g(f x) = x"
(**) "x\<in>s" "(f has_derivative f') (at x)" "bounded_linear g'" "g' o f' = id"
shows "(g has_derivative g') (at (f x))"
@@ -832,7 +832,7 @@
subsection {* Here's the simplest way of not assuming much about g. *}
-lemma has_derivative_inverse: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
+lemma has_derivative_inverse: fixes f::"real^'a \<Rightarrow> real^'b"
assumes "compact s" "x \<in> s" "f x \<in> interior(f ` s)" "continuous_on s f"
"\<forall>y\<in>s. g(f y) = y" "(f has_derivative f') (at x)" "bounded_linear g'" "g' \<circ> f' = id"
shows "(g has_derivative g') (at (f x))" proof-
@@ -845,7 +845,7 @@
subsection {* Proving surjectivity via Brouwer fixpoint theorem. *}
-lemma brouwer_surjective: fixes f::"real^'n::finite \<Rightarrow> real^'n"
+lemma brouwer_surjective: fixes f::"real^'n \<Rightarrow> real^'n"
assumes "compact t" "convex t" "t \<noteq> {}" "continuous_on t f"
"\<forall>x\<in>s. \<forall>y\<in>t. x + (y - f y) \<in> t" "x\<in>s"
shows "\<exists>y\<in>t. f y = x" proof-
@@ -853,7 +853,7 @@
show ?thesis unfolding * apply(rule brouwer[OF assms(1-3), of "\<lambda>y. x + (y - f y)"])
apply(rule continuous_on_intros assms)+ using assms(4-6) by auto qed
-lemma brouwer_surjective_cball: fixes f::"real^'n::finite \<Rightarrow> real^'n"
+lemma brouwer_surjective_cball: fixes f::"real^'n \<Rightarrow> real^'n"
assumes "0 < e" "continuous_on (cball a e) f"
"\<forall>x\<in>s. \<forall>y\<in>cball a e. x + (y - f y) \<in> cball a e" "x\<in>s"
shows "\<exists>y\<in>cball a e. f y = x" apply(rule brouwer_surjective) apply(rule compact_cball convex_cball)+
@@ -861,7 +861,7 @@
text {* See Sussmann: "Multidifferential calculus", Theorem 2.1.1 *}
-lemma sussmann_open_mapping: fixes f::"real^'a::finite \<Rightarrow> real^'b::finite"
+lemma sussmann_open_mapping: fixes f::"real^'a \<Rightarrow> real^'b"
assumes "open s" "continuous_on s f" "x \<in> s"
"(f has_derivative f') (at x)" "bounded_linear g'" "f' \<circ> g' = id"
(**) "t \<subseteq> s" "x \<in> interior t"
@@ -918,7 +918,7 @@
(* We could put f' o g = I but this happens to fit with the minimal linear *)
(* algebra theory I've set up so far. *}
-lemma has_derivative_inverse_strong: fixes f::"real^'n::finite \<Rightarrow> real^'n"
+lemma has_derivative_inverse_strong: fixes f::"real^'n \<Rightarrow> real^'n"
assumes "open s" "x \<in> s" "continuous_on s f"
"\<forall>x\<in>s. g(f x) = x" "(f has_derivative f') (at x)" "f' o g' = id"
shows "(g has_derivative g') (at (f x))" proof-
@@ -949,7 +949,7 @@
subsection {* A rewrite based on the other domain. *}
-lemma has_derivative_inverse_strong_x: fixes f::"real^'n::finite \<Rightarrow> real^'n"
+lemma has_derivative_inverse_strong_x: fixes f::"real^'n \<Rightarrow> real^'n"
assumes "open s" "g y \<in> s" "continuous_on s f"
"\<forall>x\<in>s. g(f x) = x" "(f has_derivative f') (at (g y))" "f' o g' = id" "f(g y) = y"
shows "(g has_derivative g') (at y)"
@@ -957,7 +957,7 @@
subsection {* On a region. *}
-lemma has_derivative_inverse_on: fixes f::"real^'n::finite \<Rightarrow> real^'n"
+lemma has_derivative_inverse_on: fixes f::"real^'n \<Rightarrow> real^'n"
assumes "open s" "\<forall>x\<in>s. (f has_derivative f'(x)) (at x)" "\<forall>x\<in>s. g(f x) = x" "f'(x) o g'(x) = id" "x\<in>s"
shows "(g has_derivative g'(x)) (at (f x))"
apply(rule has_derivative_inverse_strong[where g'="g' x" and f=f]) apply(rule assms)+
@@ -972,7 +972,7 @@
lemma bounded_linear_sub: "bounded_linear f \<Longrightarrow> bounded_linear g ==> bounded_linear (\<lambda>x. f x - g x)"
using bounded_linear_add[of f "\<lambda>x. - g x"] bounded_linear_minus[of g] by(auto simp add:group_simps)
-lemma has_derivative_locally_injective: fixes f::"real^'n::finite \<Rightarrow> real^'m::finite"
+lemma has_derivative_locally_injective: fixes f::"real^'n \<Rightarrow> real^'m"
assumes "a \<in> s" "open s" "bounded_linear g'" "g' o f'(a) = id"
"\<forall>x\<in>s. (f has_derivative f'(x)) (at x)"
"\<forall>e>0. \<exists>d>0. \<forall>x. dist a x < d \<longrightarrow> onorm(\<lambda>v. f' x v - f' a v) < e"
@@ -1016,7 +1016,7 @@
subsection {* Uniformly convergent sequence of derivatives. *}
-lemma has_derivative_sequence_lipschitz_lemma: fixes f::"nat \<Rightarrow> real^'m::finite \<Rightarrow> real^'n::finite"
+lemma has_derivative_sequence_lipschitz_lemma: fixes f::"nat \<Rightarrow> real^'m \<Rightarrow> real^'n"
assumes "convex s" "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
"\<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm(f' n x h - g' x h) \<le> e * norm(h)"
shows "\<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm((f m x - f n x) - (f m y - f n y)) \<le> 2 * e * norm(x - y)" proof(default)+
@@ -1033,7 +1033,7 @@
thus "onorm (\<lambda>h. f' m x h - f' n x h) \<le> 2 * e" apply-apply(rule onorm(2)) apply(rule linear_compose_sub)
unfolding linear_conv_bounded_linear using assms(2)[rule_format,OF `x\<in>s`, THEN derivative_linear] by auto qed qed
-lemma has_derivative_sequence_lipschitz: fixes f::"nat \<Rightarrow> real^'m::finite \<Rightarrow> real^'n::finite"
+lemma has_derivative_sequence_lipschitz: fixes f::"nat \<Rightarrow> real^'m \<Rightarrow> real^'n"
assumes "convex s" "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
"\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm(f' n x h - g' x h) \<le> e * norm(h)" "0 < e"
shows "\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>y\<in>s. norm((f m x - f n x) - (f m y - f n y)) \<le> e * norm(x - y)" proof(rule,rule)
@@ -1041,7 +1041,7 @@
guess N using assms(3)[rule_format,OF *(2)] ..
thus ?case apply(rule_tac x=N in exI) apply(rule has_derivative_sequence_lipschitz_lemma[where e="1/2 *e", unfolded *]) using assms by auto qed
-lemma has_derivative_sequence: fixes f::"nat\<Rightarrow>real^'m::finite\<Rightarrow>real^'n::finite"
+lemma has_derivative_sequence: fixes f::"nat\<Rightarrow>real^'m\<Rightarrow>real^'n"
assumes "convex s" "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
"\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm(f' n x h - g' x h) \<le> e * norm(h)"
"x0 \<in> s" "((\<lambda>n. f n x0) ---> l) sequentially"
@@ -1115,7 +1115,7 @@
subsection {* Can choose to line up antiderivatives if we want. *}
-lemma has_antiderivative_sequence: fixes f::"nat\<Rightarrow> real^'m::finite \<Rightarrow> real^'n::finite"
+lemma has_antiderivative_sequence: fixes f::"nat\<Rightarrow> real^'m \<Rightarrow> real^'n"
assumes "convex s" "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
"\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm(f' n x h - g' x h) \<le> e * norm h"
shows "\<exists>g. \<forall>x\<in>s. (g has_derivative g'(x)) (at x within s)" proof(cases "s={}")
@@ -1124,7 +1124,7 @@
apply(rule,rule) apply(rule has_derivative_add_const, rule assms(2)[rule_format], assumption)
apply(rule `a\<in>s`) by(auto intro!: Lim_const) qed auto
-lemma has_antiderivative_limit: fixes g'::"real^'m::finite \<Rightarrow> real^'m::finite \<Rightarrow> real^'n::finite"
+lemma has_antiderivative_limit: fixes g'::"real^'m \<Rightarrow> real^'m \<Rightarrow> real^'n"
assumes "convex s" "\<forall>e>0. \<exists>f f'. \<forall>x\<in>s. (f has_derivative (f' x)) (at x within s) \<and> (\<forall>h. norm(f' x h - g' x h) \<le> e * norm(h))"
shows "\<exists>g. \<forall>x\<in>s. (g has_derivative g'(x)) (at x within s)" proof-
have *:"\<forall>n. \<exists>f f'. \<forall>x\<in>s. (f has_derivative (f' x)) (at x within s) \<and> (\<forall>h. norm(f' x h - g' x h) \<le> inverse (real (Suc n)) * norm(h))"
@@ -1143,7 +1143,7 @@
definition sums_seq :: "(nat \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> (nat set) \<Rightarrow> bool"
(infixl "sums'_seq" 12) where "(f sums_seq l) s \<equiv> ((\<lambda>n. setsum f (s \<inter> {0..n})) ---> l) sequentially"
-lemma has_derivative_series: fixes f::"nat \<Rightarrow> real^'m::finite \<Rightarrow> real^'n::finite"
+lemma has_derivative_series: fixes f::"nat \<Rightarrow> real^'m \<Rightarrow> real^'n"
assumes "convex s" "\<forall>n. \<forall>x\<in>s. ((f n) has_derivative (f' n x)) (at x within s)"
"\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm(setsum (\<lambda>i. f' i x h) (k \<inter> {0..n}) - g' x h) \<le> e * norm(h)"
"x\<in>s" "((\<lambda>n. f n x) sums_seq l) k"
@@ -1154,7 +1154,7 @@
subsection {* Derivative with composed bilinear function. *}
-lemma has_derivative_bilinear_within: fixes h::"real^'m::finite \<Rightarrow> real^'n::finite \<Rightarrow> real^'p::finite" and f::"real^'q::finite \<Rightarrow> real^'m"
+lemma has_derivative_bilinear_within: fixes h::"real^'m \<Rightarrow> real^'n \<Rightarrow> real^'p" and f::"real^'q \<Rightarrow> real^'m"
assumes "(f has_derivative f') (at x within s)" "(g has_derivative g') (at x within s)" "bounded_bilinear h"
shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x within s)" proof-
have "(g ---> g x) (at x within s)" apply(rule differentiable_imp_continuous_within[unfolded continuous_within])
@@ -1194,7 +1194,7 @@
h.add_right h.add_left scaleR_right_distrib h.scaleR_left h.scaleR_right h.diff_right h.diff_left
scaleR_right_diff_distrib h.zero_right h.zero_left by(auto simp add:field_simps) qed
-lemma has_derivative_bilinear_at: fixes h::"real^'m::finite \<Rightarrow> real^'n::finite \<Rightarrow> real^'p::finite" and f::"real^'p::finite \<Rightarrow> real^'m"
+lemma has_derivative_bilinear_at: fixes h::"real^'m \<Rightarrow> real^'n \<Rightarrow> real^'p" and f::"real^'p \<Rightarrow> real^'m"
assumes "(f has_derivative f') (at x)" "(g has_derivative g') (at x)" "bounded_bilinear h"
shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
using has_derivative_bilinear_within[of f f' x UNIV g g' h] unfolding within_UNIV using assms by auto
@@ -1216,7 +1216,7 @@
using f' unfolding scaleR[THEN sym] by auto
next assume ?r thus ?l unfolding vector_derivative_def has_vector_derivative_def differentiable_def by auto qed
-lemma vector_derivative_unique_at: fixes f::"real\<Rightarrow>real^'n::finite"
+lemma vector_derivative_unique_at: fixes f::"real\<Rightarrow>real^'n"
assumes "(f has_vector_derivative f') (at x)" "(f has_vector_derivative f'') (at x)" shows "f' = f''" proof-
have *:"(\<lambda>x. x *\<^sub>R f') \<circ> dest_vec1 = (\<lambda>x. x *\<^sub>R f'') \<circ> dest_vec1" apply(rule frechet_derivative_unique_at)
using assms[unfolded has_vector_derivative_def] unfolding has_derivative_at_dest_vec1[THEN sym] by auto
@@ -1224,7 +1224,7 @@
hence "((\<lambda>x. x *\<^sub>R f') \<circ> dest_vec1) (vec1 1) = ((\<lambda>x. x *\<^sub>R f'') \<circ> dest_vec1) (vec1 1)" using * by auto
ultimately show False unfolding o_def vec1_dest_vec1 by auto qed qed
-lemma vector_derivative_unique_within_closed_interval: fixes f::"real \<Rightarrow> real^'n::finite"
+lemma vector_derivative_unique_within_closed_interval: fixes f::"real \<Rightarrow> real^'n"
assumes "a < b" "x \<in> {a..b}"
"(f has_vector_derivative f') (at x within {a..b})"
"(f has_vector_derivative f'') (at x within {a..b})" shows "f' = f''" proof-
@@ -1236,35 +1236,35 @@
hence "((\<lambda>x. x *\<^sub>R f') \<circ> dest_vec1) (vec1 1) = ((\<lambda>x. x *\<^sub>R f'') \<circ> dest_vec1) (vec1 1)" using * by auto
ultimately show False unfolding o_def vec1_dest_vec1 by auto qed qed
-lemma vector_derivative_at: fixes f::"real \<Rightarrow> real^'a::finite" shows
+lemma vector_derivative_at: fixes f::"real \<Rightarrow> real^'a" shows
"(f has_vector_derivative f') (at x) \<Longrightarrow> vector_derivative f (at x) = f'"
apply(rule vector_derivative_unique_at) defer apply assumption
unfolding vector_derivative_works[THEN sym] differentiable_def
unfolding has_vector_derivative_def by auto
-lemma vector_derivative_within_closed_interval: fixes f::"real \<Rightarrow> real^'a::finite"
+lemma vector_derivative_within_closed_interval: fixes f::"real \<Rightarrow> real^'a"
assumes "a < b" "x \<in> {a..b}" "(f has_vector_derivative f') (at x within {a..b})"
shows "vector_derivative f (at x within {a..b}) = f'"
apply(rule vector_derivative_unique_within_closed_interval)
using vector_derivative_works[unfolded differentiable_def]
using assms by(auto simp add:has_vector_derivative_def)
-lemma has_vector_derivative_within_subset: fixes f::"real \<Rightarrow> real^'a::finite" shows
+lemma has_vector_derivative_within_subset: fixes f::"real \<Rightarrow> real^'a" shows
"(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
unfolding has_vector_derivative_def apply(rule has_derivative_within_subset) by auto
-lemma has_vector_derivative_const: fixes c::"real^'n::finite" shows
+lemma has_vector_derivative_const: fixes c::"real^'n" shows
"((\<lambda>x. c) has_vector_derivative 0) net"
unfolding has_vector_derivative_def using has_derivative_const by auto
lemma has_vector_derivative_id: "((\<lambda>x::real. x) has_vector_derivative 1) net"
unfolding has_vector_derivative_def using has_derivative_id by auto
-lemma has_vector_derivative_cmul: fixes f::"real \<Rightarrow> real^'a::finite"
+lemma has_vector_derivative_cmul: fixes f::"real \<Rightarrow> real^'a"
shows "(f has_vector_derivative f') net \<Longrightarrow> ((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net"
unfolding has_vector_derivative_def apply(drule has_derivative_cmul) by(auto simp add:group_simps)
-lemma has_vector_derivative_cmul_eq: fixes f::"real \<Rightarrow> real^'a::finite" assumes "c \<noteq> 0"
+lemma has_vector_derivative_cmul_eq: fixes f::"real \<Rightarrow> real^'a" assumes "c \<noteq> 0"
shows "(((\<lambda>x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net \<longleftrightarrow> (f has_vector_derivative f') net)"
apply rule apply(drule has_vector_derivative_cmul[where c="1/c"]) defer
apply(rule has_vector_derivative_cmul) using assms by auto
@@ -1285,7 +1285,7 @@
using has_derivative_sub[OF assms[unfolded has_vector_derivative_def]]
unfolding has_vector_derivative_def scaleR_right_diff_distrib by auto
-lemma has_vector_derivative_bilinear_within: fixes h::"real^'m::finite \<Rightarrow> real^'n::finite \<Rightarrow> real^'p::finite"
+lemma has_vector_derivative_bilinear_within: fixes h::"real^'m \<Rightarrow> real^'n \<Rightarrow> real^'p"
assumes "(f has_vector_derivative f') (at x within s)" "(g has_vector_derivative g') (at x within s)" "bounded_bilinear h"
shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x within s)" proof-
interpret bounded_bilinear h using assms by auto
@@ -1294,7 +1294,7 @@
unfolding has_derivative_within_dest_vec1[unfolded o_def, where f="\<lambda>x. h (f x) (g x)" and f'="\<lambda>d. h (f x) (d *\<^sub>R g') + h (d *\<^sub>R f') (g x)"]
using assms(3) unfolding scaleR_right scaleR_left scaleR_right_distrib by auto qed
-lemma has_vector_derivative_bilinear_at: fixes h::"real^'m::finite \<Rightarrow> real^'n::finite \<Rightarrow> real^'p::finite"
+lemma has_vector_derivative_bilinear_at: fixes h::"real^'m \<Rightarrow> real^'n \<Rightarrow> real^'p"
assumes "(f has_vector_derivative f') (at x)" "(g has_vector_derivative g') (at x)" "bounded_bilinear h"
shows "((\<lambda>x. h (f x) (g x)) has_vector_derivative (h (f x) g' + h f' (g x))) (at x)"
apply(rule has_vector_derivative_bilinear_within[where s=UNIV, unfolded within_UNIV]) using assms by auto
@@ -1330,4 +1330,3 @@
unfolding o_def scaleR.scaleR_left by auto
end
-
--- a/src/HOL/Multivariate_Analysis/Determinants.thy Thu Jan 07 17:43:35 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Thu Jan 07 18:56:39 2010 +0100
@@ -67,22 +67,22 @@
subsection{* Trace *}
-definition trace :: "'a::semiring_1^'n^'n::finite \<Rightarrow> 'a" where
+definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a" where
"trace A = setsum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)"
lemma trace_0: "trace(mat 0) = 0"
by (simp add: trace_def mat_def)
-lemma trace_I: "trace(mat 1 :: 'a::semiring_1^'n^'n::finite) = of_nat(CARD('n))"
+lemma trace_I: "trace(mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))"
by (simp add: trace_def mat_def)
-lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n::finite) + B) = trace A + trace B"
+lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B"
by (simp add: trace_def setsum_addf)
-lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n::finite) - B) = trace A - trace B"
+lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B"
by (simp add: trace_def setsum_subtractf)
-lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'n::finite) ** B) = trace (B**A)"
+lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'n) ** B) = trace (B**A)"
apply (simp add: trace_def matrix_matrix_mult_def)
apply (subst setsum_commute)
by (simp add: mult_commute)
@@ -91,7 +91,7 @@
(* Definition of determinant. *)
(* ------------------------------------------------------------------------- *)
-definition det:: "'a::comm_ring_1^'n^'n::finite \<Rightarrow> 'a" where
+definition det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where
"det A = setsum (\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)) {p. p permutes (UNIV :: 'n set)}"
(* ------------------------------------------------------------------------- *)
@@ -121,7 +121,7 @@
(* Basic determinant properties. *)
(* ------------------------------------------------------------------------- *)
-lemma det_transp: "det (transp A) = det (A::'a::comm_ring_1 ^'n^'n::finite)"
+lemma det_transp: "det (transp A) = det (A::'a::comm_ring_1 ^'n^'n)"
proof-
let ?di = "\<lambda>A i j. A$i$j"
let ?U = "(UNIV :: 'n set)"
@@ -151,7 +151,7 @@
qed
lemma det_lowerdiagonal:
- fixes A :: "'a::comm_ring_1^'n^'n::{finite,wellorder}"
+ fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})"
assumes ld: "\<And>i j. i < j \<Longrightarrow> A$i$j = 0"
shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
proof-
@@ -173,7 +173,7 @@
qed
lemma det_upperdiagonal:
- fixes A :: "'a::comm_ring_1^'n^'n::{finite,wellorder}"
+ fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}"
assumes ld: "\<And>i j. i > j \<Longrightarrow> A$i$j = 0"
shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
proof-
@@ -195,7 +195,7 @@
qed
lemma det_diagonal:
- fixes A :: "'a::comm_ring_1^'n^'n::finite"
+ fixes A :: "'a::comm_ring_1^'n^'n"
assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0"
shows "det A = setprod (\<lambda>i. A$i$i) (UNIV::'n set)"
proof-
@@ -215,7 +215,7 @@
unfolding det_def by (simp add: sign_id)
qed
-lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n::finite) = 1"
+lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1"
proof-
let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n"
let ?U = "UNIV :: 'n set"
@@ -232,11 +232,11 @@
finally show ?thesis .
qed
-lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n::finite) = 0"
+lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
by (simp add: det_def setprod_zero)
lemma det_permute_rows:
- fixes A :: "'a::comm_ring_1^'n^'n::finite"
+ fixes A :: "'a::comm_ring_1^'n^'n"
assumes p: "p permutes (UNIV :: 'n::finite set)"
shows "det(\<chi> i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A"
apply (simp add: det_def setsum_right_distrib mult_assoc[symmetric])
@@ -262,7 +262,7 @@
qed
lemma det_permute_columns:
- fixes A :: "'a::comm_ring_1^'n^'n::finite"
+ fixes A :: "'a::comm_ring_1^'n^'n"
assumes p: "p permutes (UNIV :: 'n set)"
shows "det(\<chi> i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A"
proof-
@@ -277,7 +277,7 @@
qed
lemma det_identical_rows:
- fixes A :: "'a::ordered_idom^'n^'n::finite"
+ fixes A :: "'a::ordered_idom^'n^'n"
assumes ij: "i \<noteq> j"
and r: "row i A = row j A"
shows "det A = 0"
@@ -295,7 +295,7 @@
qed
lemma det_identical_columns:
- fixes A :: "'a::ordered_idom^'n^'n::finite"
+ fixes A :: "'a::ordered_idom^'n^'n"
assumes ij: "i \<noteq> j"
and r: "column i A = column j A"
shows "det A = 0"
@@ -304,7 +304,7 @@
by (metis row_transp r)
lemma det_zero_row:
- fixes A :: "'a::{idom, ring_char_0}^'n^'n::finite"
+ fixes A :: "'a::{idom, ring_char_0}^'n^'n"
assumes r: "row i A = 0"
shows "det A = 0"
using r
@@ -314,7 +314,7 @@
done
lemma det_zero_column:
- fixes A :: "'a::{idom,ring_char_0}^'n^'n::finite"
+ fixes A :: "'a::{idom,ring_char_0}^'n^'n"
assumes r: "column i A = 0"
shows "det A = 0"
apply (subst det_transp[symmetric])
@@ -407,7 +407,7 @@
unfolding vector_smult_lzero .
lemma det_row_operation:
- fixes A :: "'a::ordered_idom^'n^'n::finite"
+ fixes A :: "'a::ordered_idom^'n^'n"
assumes ij: "i \<noteq> j"
shows "det (\<chi> k. if k = i then row i A + c *s row j A else row k A) = det A"
proof-
@@ -421,7 +421,7 @@
qed
lemma det_row_span:
- fixes A :: "'a:: ordered_idom^'n^'n::finite"
+ fixes A :: "'a:: ordered_idom^'n^'n"
assumes x: "x \<in> span {row j A |j. j \<noteq> i}"
shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A"
proof-
@@ -462,7 +462,7 @@
(* ------------------------------------------------------------------------- *)
lemma det_dependent_rows:
- fixes A:: "'a::ordered_idom^'n^'n::finite"
+ fixes A:: "'a::ordered_idom^'n^'n"
assumes d: "dependent (rows A)"
shows "det A = 0"
proof-
@@ -488,19 +488,19 @@
ultimately show ?thesis by blast
qed
-lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::ordered_idom^'n^'n::finite))" shows "det A = 0"
+lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::ordered_idom^'n^'n))" shows "det A = 0"
by (metis d det_dependent_rows rows_transp det_transp)
(* ------------------------------------------------------------------------- *)
(* Multilinearity and the multiplication formula. *)
(* ------------------------------------------------------------------------- *)
-lemma Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (Cart_lambda f::'a^'n) = (Cart_lambda g :: 'a^'n::finite)"
+lemma Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (Cart_lambda f::'a^'n) = (Cart_lambda g :: 'a^'n)"
apply (rule iffD1[OF Cart_lambda_unique]) by vector
lemma det_linear_row_setsum:
assumes fS: "finite S"
- shows "det ((\<chi> i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n::finite) = setsum (\<lambda>j. det ((\<chi> i. if i = k then a i j else c i)::'a^'n^'n)) S"
+ shows "det ((\<chi> i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n) = setsum (\<lambda>j. det ((\<chi> i. if i = k then a i j else c i)::'a^'n^'n)) S"
proof(induct rule: finite_induct[OF fS])
case 1 thus ?case apply simp unfolding setsum_empty det_row_0[of k] ..
next
@@ -534,7 +534,7 @@
lemma det_linear_rows_setsum_lemma:
assumes fS: "finite S" and fT: "finite T"
- shows "det((\<chi> i. if i \<in> T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n::finite) =
+ shows "det((\<chi> i. if i \<in> T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n) =
setsum (\<lambda>f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n))
{f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}"
using fT
@@ -580,7 +580,7 @@
lemma det_linear_rows_setsum:
assumes fS: "finite (S::'n::finite set)"
- shows "det (\<chi> i. setsum (a i) S) = setsum (\<lambda>f. det (\<chi> i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n::finite)) {f. \<forall>i. f i \<in> S}"
+ shows "det (\<chi> i. setsum (a i) S) = setsum (\<lambda>f. det (\<chi> i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. \<forall>i. f i \<in> S}"
proof-
have th0: "\<And>x y. ((\<chi> i. if i \<in> (UNIV:: 'n set) then x i else y i) :: 'a^'n^'n) = (\<chi> i. x i)" by vector
@@ -588,12 +588,12 @@
qed
lemma matrix_mul_setsum_alt:
- fixes A B :: "'a::comm_ring_1^'n^'n::finite"
+ fixes A B :: "'a::comm_ring_1^'n^'n"
shows "A ** B = (\<chi> i. setsum (\<lambda>k. A$i$k *s B $ k) (UNIV :: 'n set))"
by (vector matrix_matrix_mult_def setsum_component)
lemma det_rows_mul:
- "det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n::finite) =
+ "det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n) =
setprod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)"
proof (simp add: det_def setsum_right_distrib cong add: setprod_cong, rule setsum_cong2)
let ?U = "UNIV :: 'n set"
@@ -608,7 +608,7 @@
qed
lemma det_mul:
- fixes A B :: "'a::ordered_idom^'n^'n::finite"
+ fixes A B :: "'a::ordered_idom^'n^'n"
shows "det (A ** B) = det A * det B"
proof-
let ?U = "UNIV :: 'n set"
@@ -700,17 +700,17 @@
(* ------------------------------------------------------------------------- *)
lemma invertible_left_inverse:
- fixes A :: "real^'n^'n::finite"
+ fixes A :: "real^'n^'n"
shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). B** A = mat 1)"
by (metis invertible_def matrix_left_right_inverse)
lemma invertible_righ_inverse:
- fixes A :: "real^'n^'n::finite"
+ fixes A :: "real^'n^'n"
shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). A** B = mat 1)"
by (metis invertible_def matrix_left_right_inverse)
lemma invertible_det_nz:
- fixes A::"real ^'n^'n::finite"
+ fixes A::"real ^'n^'n"
shows "invertible A \<longleftrightarrow> det A \<noteq> 0"
proof-
{assume "invertible A"
@@ -761,7 +761,7 @@
(* ------------------------------------------------------------------------- *)
lemma cramer_lemma_transp:
- fixes A:: "'a::ordered_idom^'n^'n::finite" and x :: "'a ^'n::finite"
+ fixes A:: "'a::ordered_idom^'n^'n" and x :: "'a ^'n"
shows "det ((\<chi> i. if i = k then setsum (\<lambda>i. x$i *s row i A) (UNIV::'n set)
else row i A)::'a^'n^'n) = x$k * det A"
(is "?lhs = ?rhs")
@@ -797,7 +797,7 @@
qed
lemma cramer_lemma:
- fixes A :: "'a::ordered_idom ^'n^'n::finite"
+ fixes A :: "'a::ordered_idom ^'n^'n"
shows "det((\<chi> i j. if j = k then (A *v x)$i else A$i$j):: 'a^'n^'n) = x$k * det A"
proof-
let ?U = "UNIV :: 'n set"
@@ -811,7 +811,7 @@
qed
lemma cramer:
- fixes A ::"real^'n^'n::finite"
+ 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)"
proof-
@@ -840,16 +840,16 @@
apply (simp add: real_vector_norm_def)
by (simp add: dot_norm linear_add[symmetric])
-definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n::finite) \<longleftrightarrow> transp Q ** Q = mat 1 \<and> Q ** transp Q = mat 1"
+definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> transp Q ** Q = mat 1 \<and> Q ** transp Q = mat 1"
-lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n::finite) \<longleftrightarrow> transp Q ** Q = mat 1"
+lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transp Q ** Q = mat 1"
by (metis matrix_left_right_inverse orthogonal_matrix_def)
-lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n::finite)"
+lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)"
by (simp add: orthogonal_matrix_def transp_mat matrix_mul_lid)
lemma orthogonal_matrix_mul:
- fixes A :: "real ^'n^'n::finite"
+ fixes A :: "real ^'n^'n"
assumes oA : "orthogonal_matrix A"
and oB: "orthogonal_matrix B"
shows "orthogonal_matrix(A ** B)"
@@ -860,7 +860,7 @@
by (simp add: matrix_mul_rid)
lemma orthogonal_transformation_matrix:
- fixes f:: "real^'n \<Rightarrow> real^'n::finite"
+ fixes f:: "real^'n \<Rightarrow> real^'n"
shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)"
(is "?lhs \<longleftrightarrow> ?rhs")
proof-
@@ -893,7 +893,7 @@
qed
lemma det_orthogonal_matrix:
- fixes Q:: "'a::ordered_idom^'n^'n::finite"
+ fixes Q:: "'a::ordered_idom^'n^'n"
assumes oQ: "orthogonal_matrix Q"
shows "det Q = 1 \<or> det Q = - 1"
proof-
@@ -918,7 +918,7 @@
(* Linearity of scaling, and hence isometry, that preserves origin. *)
(* ------------------------------------------------------------------------- *)
lemma scaling_linear:
- fixes f :: "real ^'n \<Rightarrow> real ^'n::finite"
+ fixes f :: "real ^'n \<Rightarrow> real ^'n"
assumes f0: "f 0 = 0" and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y"
shows "linear f"
proof-
@@ -934,7 +934,7 @@
qed
lemma isometry_linear:
- "f (0:: real^'n) = (0:: real^'n::finite) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y
+ "f (0:: real^'n) = (0:: real^'n) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y
\<Longrightarrow> linear f"
by (rule scaling_linear[where c=1]) simp_all
@@ -943,7 +943,7 @@
(* ------------------------------------------------------------------------- *)
lemma orthogonal_transformation_isometry:
- "orthogonal_transformation f \<longleftrightarrow> f(0::real^'n) = (0::real^'n::finite) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
+ "orthogonal_transformation f \<longleftrightarrow> f(0::real^'n) = (0::real^'n) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
unfolding orthogonal_transformation
apply (rule iffI)
apply clarify
@@ -962,7 +962,7 @@
(* ------------------------------------------------------------------------- *)
lemma isometry_sphere_extend:
- fixes f:: "real ^'n \<Rightarrow> real ^'n::finite"
+ fixes f:: "real ^'n \<Rightarrow> real ^'n"
assumes f1: "\<forall>x. norm x = 1 \<longrightarrow> norm (f x) = 1"
and fd1: "\<forall> x y. norm x = 1 \<longrightarrow> norm y = 1 \<longrightarrow> dist (f x) (f y) = dist x y"
shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)"
@@ -1034,7 +1034,7 @@
definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
lemma orthogonal_rotation_or_rotoinversion:
- fixes Q :: "'a::ordered_idom^'n^'n::finite"
+ fixes Q :: "'a::ordered_idom^'n^'n"
shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q"
by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix)
(* ------------------------------------------------------------------------- *)
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Jan 07 17:43:35 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Jan 07 18:56:39 2010 +0100
@@ -61,38 +61,39 @@
subsection{* Basic componentwise operations on vectors. *}
-instantiation "^" :: (plus,finite) plus
+instantiation cart :: (plus,finite) plus
begin
definition vector_add_def : "op + \<equiv> (\<lambda> x y. (\<chi> i. (x$i) + (y$i)))"
instance ..
end
-instantiation "^" :: (times,finite) times
+instantiation cart :: (times,finite) times
begin
definition vector_mult_def : "op * \<equiv> (\<lambda> x y. (\<chi> i. (x$i) * (y$i)))"
instance ..
end
-instantiation "^" :: (minus,finite) minus begin
+instantiation cart :: (minus,finite) minus begin
definition vector_minus_def : "op - \<equiv> (\<lambda> x y. (\<chi> i. (x$i) - (y$i)))"
instance ..
end
-instantiation "^" :: (uminus,finite) uminus begin
+instantiation cart :: (uminus,finite) uminus begin
definition vector_uminus_def : "uminus \<equiv> (\<lambda> x. (\<chi> i. - (x$i)))"
instance ..
end
-instantiation "^" :: (zero,finite) zero begin
+
+instantiation cart :: (zero,finite) zero begin
definition vector_zero_def : "0 \<equiv> (\<chi> i. 0)"
instance ..
end
-instantiation "^" :: (one,finite) one begin
+instantiation cart :: (one,finite) one begin
definition vector_one_def : "1 \<equiv> (\<chi> i. 1)"
instance ..
end
-instantiation "^" :: (ord,finite) ord
+instantiation cart :: (ord,finite) ord
begin
definition vector_le_def:
"less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)"
@@ -101,7 +102,7 @@
instance by (intro_classes)
end
-instantiation "^" :: (scaleR, finite) scaleR
+instantiation cart :: (scaleR, finite) scaleR
begin
definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
instance ..
@@ -109,7 +110,7 @@
text{* Also the scalar-vector multiplication. *}
-definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n::finite \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
+definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
where "c *s x = (\<chi> i. c * (x$i))"
text{* Constant Vectors *}
@@ -118,7 +119,7 @@
text{* Dot products. *}
-definition dot :: "'a::{comm_monoid_add, times} ^ 'n::finite \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" (infix "\<bullet>" 70) where
+definition dot :: "'a::{comm_monoid_add, times} ^ 'n \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a" (infix "\<bullet>" 70) where
"x \<bullet> y = setsum (\<lambda>i. x$i * y$i) UNIV"
lemma dot_1[simp]: "(x::'a::{comm_monoid_add, times}^1) \<bullet> y = (x$1) * (y$1)"
@@ -162,37 +163,25 @@
text{* Obvious "component-pushing". *}
-lemma vec_component [simp]: "(vec x :: 'a ^ 'n::finite)$i = x"
+lemma vec_component [simp]: "vec x $ i = x"
by (vector vec_def)
-lemma vector_add_component [simp]:
- fixes x y :: "'a::{plus} ^ 'n::finite"
- shows "(x + y)$i = x$i + y$i"
+lemma vector_add_component [simp]: "(x + y)$i = x$i + y$i"
by vector
-lemma vector_minus_component [simp]:
- fixes x y :: "'a::{minus} ^ 'n::finite"
- shows "(x - y)$i = x$i - y$i"
+lemma vector_minus_component [simp]: "(x - y)$i = x$i - y$i"
by vector
-lemma vector_mult_component [simp]:
- fixes x y :: "'a::{times} ^ 'n::finite"
- shows "(x * y)$i = x$i * y$i"
+lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i"
by vector
-lemma vector_smult_component [simp]:
- fixes y :: "'a::{times} ^ 'n::finite"
- shows "(c *s y)$i = c * (y$i)"
+lemma vector_smult_component [simp]: "(c *s y)$i = c * (y$i)"
by vector
-lemma vector_uminus_component [simp]:
- fixes x :: "'a::{uminus} ^ 'n::finite"
- shows "(- x)$i = - (x$i)"
+lemma vector_uminus_component [simp]: "(- x)$i = - (x$i)"
by vector
-lemma vector_scaleR_component [simp]:
- fixes x :: "'a::scaleR ^ 'n::finite"
- shows "(scaleR r x)$i = scaleR r (x$i)"
+lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)"
by vector
lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector
@@ -204,95 +193,96 @@
subsection {* Some frequently useful arithmetic lemmas over vectors. *}
-instance "^" :: (semigroup_add,finite) semigroup_add
+instance cart :: (semigroup_add,finite) semigroup_add
apply (intro_classes) by (vector add_assoc)
-instance "^" :: (monoid_add,finite) monoid_add
+instance cart :: (monoid_add,finite) monoid_add
apply (intro_classes) by vector+
-instance "^" :: (group_add,finite) group_add
+instance cart :: (group_add,finite) group_add
apply (intro_classes) by (vector algebra_simps)+
-instance "^" :: (ab_semigroup_add,finite) ab_semigroup_add
+instance cart :: (ab_semigroup_add,finite) ab_semigroup_add
apply (intro_classes) by (vector add_commute)
-instance "^" :: (comm_monoid_add,finite) comm_monoid_add
+instance cart :: (comm_monoid_add,finite) comm_monoid_add
apply (intro_classes) by vector
-instance "^" :: (ab_group_add,finite) ab_group_add
+instance cart :: (ab_group_add,finite) ab_group_add
apply (intro_classes) by vector+
-instance "^" :: (cancel_semigroup_add,finite) cancel_semigroup_add
+instance cart :: (cancel_semigroup_add,finite) cancel_semigroup_add
apply (intro_classes)
by (vector Cart_eq)+
-instance "^" :: (cancel_ab_semigroup_add,finite) cancel_ab_semigroup_add
+instance cart :: (cancel_ab_semigroup_add,finite) cancel_ab_semigroup_add
apply (intro_classes)
by (vector Cart_eq)
-instance "^" :: (real_vector, finite) real_vector
+instance cart :: (real_vector, finite) real_vector
by default (vector scaleR_left_distrib scaleR_right_distrib)+
-instance "^" :: (semigroup_mult,finite) semigroup_mult
+instance cart :: (semigroup_mult,finite) semigroup_mult
apply (intro_classes) by (vector mult_assoc)
-instance "^" :: (monoid_mult,finite) monoid_mult
+instance cart :: (monoid_mult,finite) monoid_mult
apply (intro_classes) by vector+
-instance "^" :: (ab_semigroup_mult,finite) ab_semigroup_mult
+instance cart :: (ab_semigroup_mult,finite) ab_semigroup_mult
apply (intro_classes) by (vector mult_commute)
-instance "^" :: (ab_semigroup_idem_mult,finite) ab_semigroup_idem_mult
+instance cart :: (ab_semigroup_idem_mult,finite) ab_semigroup_idem_mult
apply (intro_classes) by (vector mult_idem)
-instance "^" :: (comm_monoid_mult,finite) comm_monoid_mult
+instance cart :: (comm_monoid_mult,finite) comm_monoid_mult
apply (intro_classes) by vector
-fun vector_power :: "('a::{one,times} ^'n::finite) \<Rightarrow> nat \<Rightarrow> 'a^'n" where
+fun vector_power where
"vector_power x 0 = 1"
| "vector_power x (Suc n) = x * vector_power x n"
-instance "^" :: (semiring,finite) semiring
+instance cart :: (semiring,finite) semiring
apply (intro_classes) by (vector ring_simps)+
-instance "^" :: (semiring_0,finite) semiring_0
+instance cart :: (semiring_0,finite) semiring_0
apply (intro_classes) by (vector ring_simps)+
-instance "^" :: (semiring_1,finite) semiring_1
+instance cart :: (semiring_1,finite) semiring_1
apply (intro_classes) by vector
-instance "^" :: (comm_semiring,finite) comm_semiring
+instance cart :: (comm_semiring,finite) comm_semiring
apply (intro_classes) by (vector ring_simps)+
-instance "^" :: (comm_semiring_0,finite) comm_semiring_0 by (intro_classes)
-instance "^" :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
-instance "^" :: (semiring_0_cancel,finite) semiring_0_cancel by (intro_classes)
-instance "^" :: (comm_semiring_0_cancel,finite) comm_semiring_0_cancel by (intro_classes)
-instance "^" :: (ring,finite) ring by (intro_classes)
-instance "^" :: (semiring_1_cancel,finite) semiring_1_cancel by (intro_classes)
-instance "^" :: (comm_semiring_1,finite) comm_semiring_1 by (intro_classes)
-
-instance "^" :: (ring_1,finite) ring_1 ..
-
-instance "^" :: (real_algebra,finite) real_algebra
+instance cart :: (comm_semiring_0,finite) comm_semiring_0 by (intro_classes)
+instance cart :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add ..
+instance cart :: (semiring_0_cancel,finite) semiring_0_cancel by (intro_classes)
+instance cart :: (comm_semiring_0_cancel,finite) comm_semiring_0_cancel by (intro_classes)
+instance cart :: (ring,finite) ring by (intro_classes)
+instance cart :: (semiring_1_cancel,finite) semiring_1_cancel by (intro_classes)
+instance cart :: (comm_semiring_1,finite) comm_semiring_1 by (intro_classes)
+
+instance cart :: (ring_1,finite) ring_1 ..
+
+instance cart :: (real_algebra,finite) real_algebra
apply intro_classes
apply (simp_all add: vector_scaleR_def ring_simps)
apply vector
apply vector
done
-instance "^" :: (real_algebra_1,finite) real_algebra_1 ..
+instance cart :: (real_algebra_1,finite) real_algebra_1 ..
lemma of_nat_index:
- "(of_nat n :: 'a::semiring_1 ^'n::finite)$i = of_nat n"
+ "(of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n"
apply (induct n)
apply vector
apply vector
done
+
lemma zero_index[simp]:
- "(0 :: 'a::zero ^'n::finite)$i = 0" by vector
+ "(0 :: 'a::zero ^'n)$i = 0" by vector
lemma one_index[simp]:
- "(1 :: 'a::one ^'n::finite)$i = 1" by vector
+ "(1 :: 'a::one ^'n)$i = 1" by vector
lemma one_plus_of_nat_neq_0: "(1::'a::semiring_char_0) + of_nat n \<noteq> 0"
proof-
@@ -301,15 +291,15 @@
finally show ?thesis by simp
qed
-instance "^" :: (semiring_char_0,finite) semiring_char_0
+instance cart :: (semiring_char_0,finite) semiring_char_0
proof (intro_classes)
fix m n ::nat
show "(of_nat m :: 'a^'b) = of_nat n \<longleftrightarrow> m = n"
by (simp add: Cart_eq of_nat_index)
qed
-instance "^" :: (comm_ring_1,finite) comm_ring_1 by intro_classes
-instance "^" :: (ring_char_0,finite) ring_char_0 by intro_classes
+instance cart :: (comm_ring_1,finite) comm_ring_1 by intro_classes
+instance cart :: (ring_char_0,finite) ring_char_0 by intro_classes
lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x"
by (vector mult_assoc)
@@ -324,7 +314,7 @@
lemma vector_smult_rneg: "(c::'a::ring) *s -x = -(c *s x)" by vector
lemma vector_smult_lneg: "- (c::'a::ring) *s x = -(c *s x)" by vector
lemma vector_sneg_minus1: "-x = (- (1::'a::ring_1)) *s x" by vector
-lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n::finite)" by vector
+lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector
lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x"
by (vector ring_simps)
@@ -333,7 +323,7 @@
subsection {* Topological space *}
-instantiation "^" :: (topological_space, finite) topological_space
+instantiation cart :: (topological_space, finite) topological_space
begin
definition open_vector_def:
@@ -589,7 +579,7 @@
apply (rule_tac x="f(x:=y)" in exI, simp)
done
-instantiation "^" :: (metric_space, finite) metric_space
+instantiation cart :: (metric_space, finite) metric_space
begin
definition dist_vector_def:
@@ -667,7 +657,7 @@
unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_nth_le])
lemma LIMSEQ_vector:
- fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n::finite"
+ fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n"
assumes X: "\<And>i. (\<lambda>n. X n $ i) ----> (a $ i)"
shows "X ----> a"
proof (rule metric_LIMSEQ_I)
@@ -700,7 +690,7 @@
qed
lemma Cauchy_vector:
- fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n::finite"
+ fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n"
assumes X: "\<And>i. Cauchy (\<lambda>n. X n $ i)"
shows "Cauchy (\<lambda>n. X n)"
proof (rule metric_CauchyI)
@@ -733,7 +723,7 @@
then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" ..
qed
-instance "^" :: (complete_space, finite) complete_space
+instance cart :: (complete_space, finite) complete_space
proof
fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X"
have "\<And>i. (\<lambda>n. X n $ i) ----> lim (\<lambda>n. X n $ i)"
@@ -747,7 +737,7 @@
subsection {* Norms *}
-instantiation "^" :: (real_normed_vector, finite) real_normed_vector
+instantiation cart :: (real_normed_vector, finite) real_normed_vector
begin
definition norm_vector_def:
@@ -792,11 +782,11 @@
apply (rule_tac x="1" in exI, simp add: norm_nth_le)
done
-instance "^" :: (banach, finite) banach ..
+instance cart :: (banach, finite) banach ..
subsection {* Inner products *}
-instantiation "^" :: (real_inner, finite) real_inner
+instantiation cart :: (real_inner, finite) real_inner
begin
definition inner_vector_def:
@@ -828,20 +818,20 @@
subsection{* Properties of the dot product. *}
-lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n::finite) \<bullet> y = y \<bullet> x"
+lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x"
by (vector mult_commute)
-lemma dot_ladd: "((x::'a::ring ^ 'n::finite) + y) \<bullet> z = (x \<bullet> z) + (y \<bullet> z)"
+lemma dot_ladd: "((x::'a::ring ^ 'n) + y) \<bullet> z = (x \<bullet> z) + (y \<bullet> z)"
by (vector ring_simps)
-lemma dot_radd: "x \<bullet> (y + (z::'a::ring ^ 'n::finite)) = (x \<bullet> y) + (x \<bullet> z)"
+lemma dot_radd: "x \<bullet> (y + (z::'a::ring ^ 'n)) = (x \<bullet> y) + (x \<bullet> z)"
by (vector ring_simps)
-lemma dot_lsub: "((x::'a::ring ^ 'n::finite) - y) \<bullet> z = (x \<bullet> z) - (y \<bullet> z)"
+lemma dot_lsub: "((x::'a::ring ^ 'n) - y) \<bullet> z = (x \<bullet> z) - (y \<bullet> z)"
by (vector ring_simps)
-lemma dot_rsub: "(x::'a::ring ^ 'n::finite) \<bullet> (y - z) = (x \<bullet> y) - (x \<bullet> z)"
+lemma dot_rsub: "(x::'a::ring ^ 'n) \<bullet> (y - z) = (x \<bullet> y) - (x \<bullet> z)"
by (vector ring_simps)
lemma dot_lmult: "(c *s x) \<bullet> y = (c::'a::ring) * (x \<bullet> y)" by (vector ring_simps)
lemma dot_rmult: "x \<bullet> (c *s y) = (c::'a::comm_ring) * (x \<bullet> y)" by (vector ring_simps)
-lemma dot_lneg: "(-x) \<bullet> (y::'a::ring ^ 'n::finite) = -(x \<bullet> y)" by vector
-lemma dot_rneg: "(x::'a::ring ^ 'n::finite) \<bullet> (-y) = -(x \<bullet> y)" by vector
+lemma dot_lneg: "(-x) \<bullet> (y::'a::ring ^ 'n) = -(x \<bullet> y)" by vector
+lemma dot_rneg: "(x::'a::ring ^ 'n) \<bullet> (-y) = -(x \<bullet> y)" by vector
lemma dot_lzero[simp]: "0 \<bullet> x = (0::'a::{comm_monoid_add, mult_zero})" by vector
lemma dot_rzero[simp]: "x \<bullet> 0 = (0::'a::{comm_monoid_add, mult_zero})" by vector
lemma dot_pos_le[simp]: "(0::'a\<Colon>ordered_ring_strict) <= x \<bullet> x"
@@ -860,10 +850,10 @@
show ?case by (simp add: h)
qed
-lemma dot_eq_0: "x \<bullet> x = 0 \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n::finite) = 0"
+lemma dot_eq_0: "x \<bullet> x = 0 \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) = 0"
by (simp add: dot_def setsum_squares_eq_0_iff Cart_eq)
-lemma dot_pos_lt[simp]: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n::finite) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x]
+lemma dot_pos_lt[simp]: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x]
by (auto simp add: le_less)
subsection{* The collapse of the general concepts to dimension one. *}
@@ -1005,7 +995,7 @@
by (simp add: norm_vector_def setL2_def dot_def power2_eq_square)
lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
by (simp add: real_vector_norm_def)
-lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n::finite)" by (metis norm_eq_zero)
+lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
by vector
lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
@@ -1017,7 +1007,7 @@
lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
by (metis vector_mul_rcancel)
lemma norm_cauchy_schwarz:
- fixes x y :: "real ^ 'n::finite"
+ fixes x y :: "real ^ 'n"
shows "x \<bullet> y <= norm x * norm y"
proof-
{assume "norm x = 0"
@@ -1040,7 +1030,7 @@
qed
lemma norm_cauchy_schwarz_abs:
- fixes x y :: "real ^ 'n::finite"
+ fixes x y :: "real ^ 'n"
shows "\<bar>x \<bullet> y\<bar> \<le> norm x * norm y"
using norm_cauchy_schwarz[of x y] norm_cauchy_schwarz[of x "-y"]
by (simp add: real_abs_def dot_rneg)
@@ -1050,38 +1040,36 @@
shows "norm x \<le> norm y + norm (x - y)"
using norm_triangle_ineq[of "y" "x - y"] by (simp add: ring_simps)
-lemma norm_triangle_le: "norm(x::real ^'n::finite) + norm y <= e ==> norm(x + y) <= e"
+lemma norm_triangle_le: "norm(x::real ^ 'n) + norm y <= e ==> norm(x + y) <= e"
by (metis order_trans norm_triangle_ineq)
-lemma norm_triangle_lt: "norm(x::real ^'n::finite) + norm(y) < e ==> norm(x + y) < e"
+lemma norm_triangle_lt: "norm(x::real ^ 'n) + norm(y) < e ==> norm(x + y) < e"
by (metis basic_trans_rules(21) norm_triangle_ineq)
-lemma component_le_norm: "\<bar>x$i\<bar> <= norm (x::real ^ 'n::finite)"
+lemma component_le_norm: "\<bar>x$i\<bar> <= norm x"
apply (simp add: norm_vector_def)
apply (rule member_le_setL2, simp_all)
done
-lemma norm_bound_component_le: "norm(x::real ^ 'n::finite) <= e
- ==> \<bar>x$i\<bar> <= e"
+lemma norm_bound_component_le: "norm x <= e ==> \<bar>x$i\<bar> <= e"
by (metis component_le_norm order_trans)
-lemma norm_bound_component_lt: "norm(x::real ^ 'n::finite) < e
- ==> \<bar>x$i\<bar> < e"
+lemma norm_bound_component_lt: "norm x < e ==> \<bar>x$i\<bar> < e"
by (metis component_le_norm basic_trans_rules(21))
-lemma norm_le_l1: "norm (x:: real ^'n::finite) <= setsum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
+lemma norm_le_l1: "norm x <= setsum(\<lambda>i. \<bar>x$i\<bar>) UNIV"
by (simp add: norm_vector_def setL2_le_setsum)
-lemma real_abs_norm: "\<bar>norm x\<bar> = norm (x :: real ^ _)"
+lemma real_abs_norm: "\<bar>norm x\<bar> = norm x"
by (rule abs_norm_cancel)
-lemma real_abs_sub_norm: "\<bar>norm(x::real ^'n::finite) - norm y\<bar> <= norm(x - y)"
+lemma real_abs_sub_norm: "\<bar>norm (x::real ^ 'n) - norm y\<bar> <= norm(x - y)"
by (rule norm_triangle_ineq3)
-lemma norm_le: "norm(x::real ^ _) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"
+lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \<longleftrightarrow> x \<bullet> x <= y \<bullet> y"
by (simp add: real_vector_norm_def)
-lemma norm_lt: "norm(x::real ^ _) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
+lemma norm_lt: "norm(x::real ^ 'n) < norm(y) \<longleftrightarrow> x \<bullet> x < y \<bullet> y"
by (simp add: real_vector_norm_def)
-lemma norm_eq: "norm (x::real ^ _) = norm y \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
+lemma norm_eq: "norm(x::real ^ 'n) = norm y \<longleftrightarrow> x \<bullet> x = y \<bullet> y"
by (simp add: order_eq_iff norm_le)
-lemma norm_eq_1: "norm(x::real ^ _) = 1 \<longleftrightarrow> x \<bullet> x = 1"
+lemma norm_eq_1: "norm(x::real ^ 'n) = 1 \<longleftrightarrow> x \<bullet> x = 1"
by (simp add: real_vector_norm_def)
text{* Squaring equations and inequalities involving norms. *}
@@ -1127,7 +1115,7 @@
text{* Equality of vectors in terms of @{term "op \<bullet>"} products. *}
-lemma vector_eq: "(x:: real ^ 'n::finite) = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y\<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs")
+lemma vector_eq: "(x:: real ^ 'n) = y \<longleftrightarrow> x \<bullet> x = x \<bullet> y\<and> y \<bullet> y = x \<bullet> x" (is "?lhs \<longleftrightarrow> ?rhs")
proof
assume "?lhs" then show ?rhs by simp
next
@@ -1299,7 +1287,7 @@
by norm
lemma setsum_component [simp]:
- fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n::finite"
+ fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n"
shows "(setsum f S)$i = setsum (\<lambda>x. (f x)$i) S"
by (cases "finite S", induct S set: finite, simp_all)
@@ -1313,7 +1301,7 @@
by (auto simp add: insert_absorb)
lemma setsum_cmul:
- fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n::finite"
+ fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n"
shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S"
by (simp add: Cart_eq setsum_right_distrib)
@@ -1332,7 +1320,7 @@
qed
lemma real_setsum_norm:
- fixes f :: "'a \<Rightarrow> real ^'n::finite"
+ fixes f :: "'a \<Rightarrow> real ^'n"
assumes fS: "finite S"
shows "norm (setsum f S) <= setsum (\<lambda>x. norm(f x)) S"
proof(induct rule: finite_induct[OF fS])
@@ -1358,7 +1346,7 @@
qed
lemma real_setsum_norm_le:
- fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
+ fixes f :: "'a \<Rightarrow> real ^ 'n"
assumes fS: "finite S"
and fg: "\<forall>x \<in> S. norm (f x) \<le> g x"
shows "norm (setsum f S) \<le> setsum g S"
@@ -1378,7 +1366,7 @@
by simp
lemma real_setsum_norm_bound:
- fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
+ fixes f :: "'a \<Rightarrow> real ^ 'n"
assumes fS: "finite S"
and K: "\<forall>x \<in> S. norm (f x) \<le> K"
shows "norm (setsum f S) \<le> of_nat (card S) * K"
@@ -1414,7 +1402,7 @@
by (auto intro: setsum_0')
lemma vsum_norm_allsubsets_bound:
- fixes f:: "'a \<Rightarrow> real ^'n::finite"
+ fixes f:: "'a \<Rightarrow> real ^'n"
assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) * e"
proof-
@@ -1452,10 +1440,10 @@
finally show ?thesis .
qed
-lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> (y::'a::{comm_ring}^'n::finite) = setsum (\<lambda>x. f x \<bullet> y) S "
+lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> (y::'a::{comm_ring}^'n) = setsum (\<lambda>x. f x \<bullet> y) S "
by (induct rule: finite_induct, auto simp add: dot_lzero dot_ladd dot_radd)
-lemma dot_rsum: "finite S \<Longrightarrow> (y::'a::{comm_ring}^'n::finite) \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
+lemma dot_rsum: "finite S \<Longrightarrow> (y::'a::{comm_ring}^'n) \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
by (induct rule: finite_induct, auto simp add: dot_rzero dot_radd)
subsection{* Basis vectors in coordinate directions. *}
@@ -1470,7 +1458,7 @@
"(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" by (cases "k=a", auto)
lemma norm_basis:
- shows "norm (basis k :: real ^'n::finite) = 1"
+ shows "norm (basis k :: real ^'n) = 1"
apply (simp add: basis_def real_vector_norm_def dot_def)
apply (vector delta_mult_idempotent)
using setsum_delta[of "UNIV :: 'n set" "k" "\<lambda>k. 1::real"]
@@ -1480,12 +1468,12 @@
lemma norm_basis_1: "norm(basis 1 :: real ^'n::{finite,one}) = 1"
by (rule norm_basis)
-lemma vector_choose_size: "0 <= c ==> \<exists>(x::real^'n::finite). norm x = c"
+lemma vector_choose_size: "0 <= c ==> \<exists>(x::real^'n). norm x = c"
apply (rule exI[where x="c *s basis arbitrary"])
by (simp only: norm_mul norm_basis)
lemma vector_choose_dist: assumes e: "0 <= e"
- shows "\<exists>(y::real^'n::finite). dist x y = e"
+ shows "\<exists>(y::real^'n). dist x y = e"
proof-
from vector_choose_size[OF e] obtain c:: "real ^'n" where "norm c = e"
by blast
@@ -1493,42 +1481,42 @@
then show ?thesis by blast
qed
-lemma basis_inj: "inj (basis :: 'n \<Rightarrow> real ^'n::finite)"
+lemma basis_inj: "inj (basis :: 'n \<Rightarrow> real ^'n)"
by (simp add: inj_on_def Cart_eq)
lemma cond_value_iff: "f (if b then x else y) = (if b then f x else f y)"
by auto
lemma basis_expansion:
- "setsum (\<lambda>i. (x$i) *s basis i) UNIV = (x::('a::ring_1) ^'n::finite)" (is "?lhs = ?rhs" is "setsum ?f ?S = _")
+ "setsum (\<lambda>i. (x$i) *s basis i) UNIV = (x::('a::ring_1) ^'n)" (is "?lhs = ?rhs" is "setsum ?f ?S = _")
by (auto simp add: Cart_eq cond_value_iff setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong)
lemma basis_expansion_unique:
- "setsum (\<lambda>i. f i *s basis i) UNIV = (x::('a::comm_ring_1) ^'n::finite) \<longleftrightarrow> (\<forall>i. f i = x$i)"
+ "setsum (\<lambda>i. f i *s basis i) UNIV = (x::('a::comm_ring_1) ^'n) \<longleftrightarrow> (\<forall>i. f i = x$i)"
by (simp add: Cart_eq setsum_delta cond_value_iff cong del: if_weak_cong)
lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)"
by auto
lemma dot_basis:
- shows "basis i \<bullet> x = x$i" "x \<bullet> (basis i :: 'a^'n::finite) = (x$i :: 'a::semiring_1)"
+ shows "basis i \<bullet> x = x$i" "x \<bullet> (basis i :: 'a^'n) = (x$i :: 'a::semiring_1)"
by (auto simp add: dot_def basis_def cond_application_beta cond_value_iff setsum_delta cong del: if_weak_cong)
lemma inner_basis:
- fixes x :: "'a::{real_inner, real_algebra_1} ^ 'n::finite"
+ fixes x :: "'a::{real_inner, real_algebra_1} ^ 'n"
shows "inner (basis i) x = inner 1 (x $ i)"
and "inner x (basis i) = inner (x $ i) 1"
unfolding inner_vector_def basis_def
by (auto simp add: cond_application_beta cond_value_iff setsum_delta cong del: if_weak_cong)
-lemma basis_eq_0: "basis i = (0::'a::semiring_1^'n::finite) \<longleftrightarrow> False"
+lemma basis_eq_0: "basis i = (0::'a::semiring_1^'n) \<longleftrightarrow> False"
by (auto simp add: Cart_eq)
lemma basis_nonzero:
- shows "basis k \<noteq> (0:: 'a::semiring_1 ^'n::finite)"
+ shows "basis k \<noteq> (0:: 'a::semiring_1 ^'n)"
by (simp add: basis_eq_0)
-lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = (z::'a::semiring_1^'n::finite)"
+lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = (z::'a::semiring_1^'n)"
apply (auto simp add: Cart_eq dot_basis)
apply (erule_tac x="basis i" in allE)
apply (simp add: dot_basis)
@@ -1537,7 +1525,7 @@
apply (simp add: Cart_eq)
done
-lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = (y::'a::semiring_1^'n::finite)"
+lemma vector_eq_rdot: "(\<forall>z. x \<bullet> z = y \<bullet> z) \<longleftrightarrow> x = (y::'a::semiring_1^'n)"
apply (auto simp add: Cart_eq dot_basis)
apply (erule_tac x="basis i" in allE)
apply (simp add: dot_basis)
@@ -1551,16 +1539,16 @@
definition "orthogonal x y \<longleftrightarrow> (x \<bullet> y = 0)"
lemma orthogonal_basis:
- shows "orthogonal (basis i :: 'a^'n::finite) x \<longleftrightarrow> x$i = (0::'a::ring_1)"
+ shows "orthogonal (basis i :: 'a^'n) x \<longleftrightarrow> x$i = (0::'a::ring_1)"
by (auto simp add: orthogonal_def dot_def basis_def cond_value_iff cond_application_beta setsum_delta cong del: if_weak_cong)
lemma orthogonal_basis_basis:
- shows "orthogonal (basis i :: 'a::ring_1^'n::finite) (basis j) \<longleftrightarrow> i \<noteq> j"
+ shows "orthogonal (basis i :: 'a::ring_1^'n) (basis j) \<longleftrightarrow> i \<noteq> j"
unfolding orthogonal_basis[of i] basis_component[of j] by simp
(* FIXME : Maybe some of these require less than comm_ring, but not all*)
lemma orthogonal_clauses:
- "orthogonal a (0::'a::comm_ring ^'n::finite)"
+ "orthogonal a (0::'a::comm_ring ^'n)"
"orthogonal a x ==> orthogonal a (c *s x)"
"orthogonal a x ==> orthogonal a (-x)"
"orthogonal a x \<Longrightarrow> orthogonal a y ==> orthogonal a (x + y)"
@@ -1574,7 +1562,7 @@
dot_lzero dot_rzero dot_lneg dot_lmult dot_ladd dot_lsub
by simp_all
-lemma orthogonal_commute: "orthogonal (x::'a::{ab_semigroup_mult,comm_monoid_add} ^'n::finite)y \<longleftrightarrow> orthogonal y x"
+lemma orthogonal_commute: "orthogonal (x::'a::{ab_semigroup_mult,comm_monoid_add} ^'n)y \<longleftrightarrow> orthogonal y x"
by (simp add: orthogonal_def dot_sym)
subsection{* Explicit vector construction from lists. *}
@@ -1648,12 +1636,12 @@
lemma linear_compose_cmul: "linear f ==> linear (\<lambda>x. (c::'a::comm_semiring) *s f x)"
by (vector linear_def Cart_eq ring_simps)
-lemma linear_compose_neg: "linear (f :: 'a ^'n::finite \<Rightarrow> 'a::comm_ring ^'m::finite) ==> linear (\<lambda>x. -(f(x)))" by (vector linear_def Cart_eq)
-
-lemma linear_compose_add: "linear (f :: 'a ^'n::finite \<Rightarrow> 'a::semiring_1 ^'m::finite) \<Longrightarrow> linear g ==> linear (\<lambda>x. f(x) + g(x))"
+lemma linear_compose_neg: "linear (f :: 'a ^'n \<Rightarrow> 'a::comm_ring ^'m) ==> linear (\<lambda>x. -(f(x)))" by (vector linear_def Cart_eq)
+
+lemma linear_compose_add: "linear (f :: 'a ^'n \<Rightarrow> 'a::semiring_1 ^'m) \<Longrightarrow> linear g ==> linear (\<lambda>x. f(x) + g(x))"
by (vector linear_def Cart_eq ring_simps)
-lemma linear_compose_sub: "linear (f :: 'a ^'n::finite \<Rightarrow> 'a::ring_1 ^'m::finite) \<Longrightarrow> linear g ==> linear (\<lambda>x. f x - g x)"
+lemma linear_compose_sub: "linear (f :: 'a ^'n \<Rightarrow> 'a::ring_1 ^'m) \<Longrightarrow> linear g ==> linear (\<lambda>x. f x - g x)"
by (vector linear_def Cart_eq ring_simps)
lemma linear_compose: "linear f \<Longrightarrow> linear g ==> linear (g o f)"
@@ -1661,24 +1649,24 @@
lemma linear_id: "linear id" by (simp add: linear_def id_def)
-lemma linear_zero: "linear (\<lambda>x. 0::'a::semiring_1 ^ 'n::finite)" by (simp add: linear_def)
+lemma linear_zero: "linear (\<lambda>x. 0::'a::semiring_1 ^ 'n)" by (simp add: linear_def)
lemma linear_compose_setsum:
- assumes fS: "finite S" and lS: "\<forall>a \<in> S. linear (f a :: 'a::semiring_1 ^ 'n::finite \<Rightarrow> 'a ^ 'm::finite)"
- shows "linear(\<lambda>x. setsum (\<lambda>a. f a x :: 'a::semiring_1 ^'m::finite) S)"
+ assumes fS: "finite S" and lS: "\<forall>a \<in> S. linear (f a :: 'a::semiring_1 ^ 'n \<Rightarrow> 'a ^'m)"
+ shows "linear(\<lambda>x. setsum (\<lambda>a. f a x :: 'a::semiring_1 ^'m) S)"
using lS
apply (induct rule: finite_induct[OF fS])
by (auto simp add: linear_zero intro: linear_compose_add)
lemma linear_vmul_component:
- fixes f:: "'a::semiring_1^'m::finite \<Rightarrow> 'a^'n::finite"
+ fixes f:: "'a::semiring_1^'m \<Rightarrow> 'a^'n"
assumes lf: "linear f"
shows "linear (\<lambda>x. f x $ k *s v)"
using lf
apply (auto simp add: linear_def )
by (vector ring_simps)+
-lemma linear_0: "linear f ==> f 0 = (0::'a::semiring_1 ^'n::finite)"
+lemma linear_0: "linear f ==> f 0 = (0::'a::semiring_1 ^'n)"
unfolding linear_def
apply clarsimp
apply (erule allE[where x="0::'a"])
@@ -1687,17 +1675,17 @@
lemma linear_cmul: "linear f ==> f(c*s x) = c *s f x" by (simp add: linear_def)
-lemma linear_neg: "linear (f :: 'a::ring_1 ^'n::finite \<Rightarrow> _) ==> f (-x) = - f x"
+lemma linear_neg: "linear (f :: 'a::ring_1 ^'n \<Rightarrow> _) ==> f (-x) = - f x"
unfolding vector_sneg_minus1
using linear_cmul[of f] by auto
lemma linear_add: "linear f ==> f(x + y) = f x + f y" by (metis linear_def)
-lemma linear_sub: "linear (f::'a::ring_1 ^'n::finite \<Rightarrow> _) ==> f(x - y) = f x - f y"
+lemma linear_sub: "linear (f::'a::ring_1 ^'n \<Rightarrow> _) ==> f(x - y) = f x - f y"
by (simp add: diff_def linear_add linear_neg)
lemma linear_setsum:
- fixes f:: "'a::semiring_1^'n::finite \<Rightarrow> _"
+ fixes f:: "'a::semiring_1^'n \<Rightarrow> _"
assumes lf: "linear f" and fS: "finite S"
shows "f (setsum g S) = setsum (f o g) S"
proof (induct rule: finite_induct[OF fS])
@@ -1712,14 +1700,14 @@
qed
lemma linear_setsum_mul:
- fixes f:: "'a ^'n::finite \<Rightarrow> 'a::semiring_1^'m::finite"
+ fixes f:: "'a ^'n \<Rightarrow> 'a::semiring_1^'m"
assumes lf: "linear f" and fS: "finite S"
shows "f (setsum (\<lambda>i. c i *s v i) S) = setsum (\<lambda>i. c i *s f (v i)) S"
using linear_setsum[OF lf fS, of "\<lambda>i. c i *s v i" , unfolded o_def]
linear_cmul[OF lf] by simp
lemma linear_injective_0:
- assumes lf: "linear (f:: 'a::ring_1 ^ 'n::finite \<Rightarrow> _)"
+ assumes lf: "linear (f:: 'a::ring_1 ^ 'n \<Rightarrow> _)"
shows "inj f \<longleftrightarrow> (\<forall>x. f x = 0 \<longrightarrow> x = 0)"
proof-
have "inj f \<longleftrightarrow> (\<forall> x y. f x = f y \<longrightarrow> x = y)" by (simp add: inj_on_def)
@@ -1731,7 +1719,7 @@
qed
lemma linear_bounded:
- fixes f:: "real ^'m::finite \<Rightarrow> real ^'n::finite"
+ fixes f:: "real ^'m \<Rightarrow> real ^'n"
assumes lf: "linear f"
shows "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
proof-
@@ -1760,7 +1748,7 @@
qed
lemma linear_bounded_pos:
- fixes f:: "real ^'n::finite \<Rightarrow> real ^ 'm::finite"
+ fixes f:: "real ^'n \<Rightarrow> real ^'m"
assumes lf: "linear f"
shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"
proof-
@@ -1815,7 +1803,7 @@
by (simp add: f.add f.scaleR)
qed
-lemma bounded_linearI': fixes f::"real^'n::finite \<Rightarrow> real^'m::finite"
+lemma bounded_linearI': fixes f::"real^'n \<Rightarrow> real^'m"
assumes "\<And>x y. f (x + y) = f x + f y" "\<And>c x. f (c *s x) = c *s f x"
shows "bounded_linear f" unfolding linear_conv_bounded_linear[THEN sym]
by(rule linearI[OF assms])
@@ -1835,17 +1823,17 @@
lemma bilinear_rmul: "bilinear h ==> h x (c *s y) = c *s (h x y)"
by (simp add: bilinear_def linear_def)
-lemma bilinear_lneg: "bilinear h ==> h (- (x:: 'a::ring_1 ^ 'n::finite)) y = -(h x y)"
+lemma bilinear_lneg: "bilinear h ==> h (- (x:: 'a::ring_1 ^ 'n)) y = -(h x y)"
by (simp only: vector_sneg_minus1 bilinear_lmul)
-lemma bilinear_rneg: "bilinear h ==> h x (- (y:: 'a::ring_1 ^ 'n::finite)) = - h x y"
+lemma bilinear_rneg: "bilinear h ==> h x (- (y:: 'a::ring_1 ^ 'n)) = - h x y"
by (simp only: vector_sneg_minus1 bilinear_rmul)
lemma (in ab_group_add) eq_add_iff: "x = x + y \<longleftrightarrow> y = 0"
using add_imp_eq[of x y 0] by auto
lemma bilinear_lzero:
- fixes h :: "'a::ring^'n::finite \<Rightarrow> _" assumes bh: "bilinear h" shows "h 0 x = 0"
+ fixes h :: "'a::ring^'n \<Rightarrow> _" assumes bh: "bilinear h" shows "h 0 x = 0"
using bilinear_ladd[OF bh, of 0 0 x]
by (simp add: eq_add_iff ring_simps)
@@ -1876,7 +1864,7 @@
qed
lemma bilinear_bounded:
- fixes h:: "real ^'m::finite \<Rightarrow> real^'n::finite \<Rightarrow> real ^ 'k::finite"
+ fixes h:: "real ^'m \<Rightarrow> real^'n \<Rightarrow> real ^'k"
assumes bh: "bilinear h"
shows "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
proof-
@@ -1903,7 +1891,7 @@
qed
lemma bilinear_bounded_pos:
- fixes h:: "real ^'m::finite \<Rightarrow> real^'n::finite \<Rightarrow> real ^ 'k::finite"
+ fixes h:: "real ^'m \<Rightarrow> real^'n \<Rightarrow> real ^'k"
assumes bh: "bilinear h"
shows "\<exists>B > 0. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
proof-
@@ -1965,7 +1953,7 @@
lemma choice_iff: "(\<forall>x. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x. P x (f x))" by metis
lemma adjoint_works_lemma:
- fixes f:: "'a::ring_1 ^'n::finite \<Rightarrow> 'a ^ 'm::finite"
+ fixes f:: "'a::ring_1 ^'n \<Rightarrow> 'a ^'m"
assumes lf: "linear f"
shows "\<forall>x y. f x \<bullet> y = x \<bullet> adjoint f y"
proof-
@@ -1993,34 +1981,34 @@
qed
lemma adjoint_works:
- fixes f:: "'a::ring_1 ^'n::finite \<Rightarrow> 'a ^ 'm::finite"
+ fixes f:: "'a::ring_1 ^'n \<Rightarrow> 'a ^'m"
assumes lf: "linear f"
shows "x \<bullet> adjoint f y = f x \<bullet> y"
using adjoint_works_lemma[OF lf] by metis
lemma adjoint_linear:
- fixes f :: "'a::comm_ring_1 ^'n::finite \<Rightarrow> 'a ^ 'm::finite"
+ fixes f :: "'a::comm_ring_1 ^'n \<Rightarrow> 'a ^'m"
assumes lf: "linear f"
shows "linear (adjoint f)"
by (simp add: linear_def vector_eq_ldot[symmetric] dot_radd dot_rmult adjoint_works[OF lf])
lemma adjoint_clauses:
- fixes f:: "'a::comm_ring_1 ^'n::finite \<Rightarrow> 'a ^ 'm::finite"
+ fixes f:: "'a::comm_ring_1 ^'n \<Rightarrow> 'a ^'m"
assumes lf: "linear f"
shows "x \<bullet> adjoint f y = f x \<bullet> y"
and "adjoint f y \<bullet> x = y \<bullet> f x"
by (simp_all add: adjoint_works[OF lf] dot_sym )
lemma adjoint_adjoint:
- fixes f:: "'a::comm_ring_1 ^ 'n::finite \<Rightarrow> 'a ^ 'm::finite"
+ fixes f:: "'a::comm_ring_1 ^ 'n \<Rightarrow> 'a ^'m"
assumes lf: "linear f"
shows "adjoint (adjoint f) = f"
apply (rule ext)
by (simp add: vector_eq_ldot[symmetric] adjoint_clauses[OF adjoint_linear[OF lf]] adjoint_clauses[OF lf])
lemma adjoint_unique:
- fixes f:: "'a::comm_ring_1 ^ 'n::finite \<Rightarrow> 'a ^ 'm::finite"
+ fixes f:: "'a::comm_ring_1 ^ 'n \<Rightarrow> 'a ^'m"
assumes lf: "linear f" and u: "\<forall>x y. f' x \<bullet> y = x \<bullet> f y"
shows "f' = adjoint f"
apply (rule ext)
@@ -2032,14 +2020,14 @@
consts generic_mult :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" (infixr "\<star>" 75)
defs (overloaded)
-matrix_matrix_mult_def: "(m:: ('a::semiring_1) ^('n::finite)^'m::finite) \<star> (m' :: 'a ^('p::finite)^'n) \<equiv> (\<chi> i j. setsum (\<lambda>k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"
+matrix_matrix_mult_def: "(m:: ('a::semiring_1) ^'n^'m) \<star> (m' :: 'a ^'p^'n) \<equiv> (\<chi> i j. setsum (\<lambda>k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m"
abbreviation
- matrix_matrix_mult' :: "('a::semiring_1) ^('n::finite)^'m::finite \<Rightarrow> 'a ^('p::finite)^'n \<Rightarrow> 'a ^ 'p ^'m" (infixl "**" 70)
+ matrix_matrix_mult' :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m" (infixl "**" 70)
where "m ** m' == m\<star> m'"
defs (overloaded)
- matrix_vector_mult_def: "(m::('a::semiring_1) ^('n::finite)^('m::finite)) \<star> (x::'a ^'n) \<equiv> (\<chi> i. setsum (\<lambda>j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m"
+ matrix_vector_mult_def: "(m::('a::semiring_1) ^'n^'m) \<star> (x::'a ^'n) \<equiv> (\<chi> i. setsum (\<lambda>j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m"
abbreviation
matrix_vector_mult' :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'm" (infixl "*v" 70)
@@ -2047,26 +2035,26 @@
"m *v v == m \<star> v"
defs (overloaded)
- vector_matrix_mult_def: "(x::'a^('m::finite)) \<star> (m::('a::semiring_1) ^('n::finite)^'m) \<equiv> (\<chi> j. setsum (\<lambda>i. ((m$i)$j) * (x$i)) (UNIV :: 'm set)) :: 'a^'n"
+ vector_matrix_mult_def: "(x::'a^'m) \<star> (m::('a::semiring_1) ^'n^'m) \<equiv> (\<chi> j. setsum (\<lambda>i. ((m$i)$j) * (x$i)) (UNIV :: 'm set)) :: 'a^'n"
abbreviation
vactor_matrix_mult' :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n " (infixl "v*" 70)
where
"v v* m == v \<star> m"
-definition "(mat::'a::zero => 'a ^('n::finite)^'n::finite) k = (\<chi> i j. if i = j then k else 0)"
-definition "(transp::'a^('n::finite)^('m::finite) \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A$j)$i))"
-definition "(row::'m::finite => 'a ^'n^'m \<Rightarrow> 'a ^'n::finite) i A = (\<chi> j. ((A$i)$j))"
-definition "(column::'n::finite =>'a^'n^'m =>'a^'m::finite) j A = (\<chi> i. ((A$i)$j))"
-definition "rows(A::'a^('n::finite)^'m::finite) = { row i A | i. i \<in> (UNIV :: 'm set)}"
-definition "columns(A::'a^('n::finite)^'m::finite) = { column i A | i. i \<in> (UNIV :: 'n set)}"
+definition "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
+definition "(transp::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A$j)$i))"
+definition "(row::'m => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A$i)$j))"
+definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A$i)$j))"
+definition "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}"
+definition "columns(A::'a^'n^'m) = { column i A | i. i \<in> (UNIV :: 'n set)}"
lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def)
lemma matrix_add_ldistrib: "(A ** (B + C)) = (A \<star> B) + (A \<star> C)"
by (vector matrix_matrix_mult_def setsum_addf[symmetric] ring_simps)
lemma matrix_mul_lid:
- fixes A :: "'a::semiring_1 ^ ('m::finite) ^ _"
+ fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
shows "mat 1 ** A = A"
apply (simp add: matrix_matrix_mult_def mat_def)
apply vector
@@ -2074,7 +2062,7 @@
lemma matrix_mul_rid:
- fixes A :: "'a::semiring_1 ^ 'm::finite ^ _::finite"
+ fixes A :: "'a::semiring_1 ^ 'm ^ 'n"
shows "A ** mat 1 = A"
apply (simp add: matrix_matrix_mult_def mat_def)
apply vector
@@ -2092,7 +2080,7 @@
apply simp
done
-lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n::finite)"
+lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
apply (vector matrix_vector_mult_def mat_def)
by (simp add: cond_value_iff cond_application_beta
setsum_delta' cong del: if_weak_cong)
@@ -2101,7 +2089,7 @@
by (simp add: matrix_matrix_mult_def transp_def Cart_eq mult_commute)
lemma matrix_eq:
- fixes A B :: "'a::semiring_1 ^ 'n::finite ^ _::finite"
+ fixes A B :: "'a::semiring_1 ^ 'n ^ 'm"
shows "A = B \<longleftrightarrow> (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs")
apply auto
apply (subst Cart_eq)
@@ -2146,16 +2134,16 @@
lemma matrix_mult_dot: "A *v x = (\<chi> i. A$i \<bullet> x)"
by (simp add: matrix_vector_mult_def dot_def)
-lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^('n::finite)^'m::finite) *v x = setsum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)"
+lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)"
by (simp add: matrix_vector_mult_def Cart_eq column_def mult_commute)
lemma vector_componentwise:
- "(x::'a::ring_1^'n::finite) = (\<chi> j. setsum (\<lambda>i. (x$i) * (basis i :: 'a^'n)$j) (UNIV :: 'n set))"
+ "(x::'a::ring_1^'n) = (\<chi> j. setsum (\<lambda>i. (x$i) * (basis i :: 'a^'n)$j) (UNIV :: 'n set))"
apply (subst basis_expansion[symmetric])
by (vector Cart_eq setsum_component)
lemma linear_componentwise:
- fixes f:: "'a::ring_1 ^ 'm::finite \<Rightarrow> 'a ^ _"
+ fixes f:: "'a::ring_1 ^'m \<Rightarrow> 'a ^ _"
assumes lf: "linear f"
shows "(f x)$j = setsum (\<lambda>i. (x$i) * (f (basis i)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")
proof-
@@ -2171,41 +2159,41 @@
text{* Inverse matrices (not necessarily square) *}
-definition "invertible(A::'a::semiring_1^('n::finite)^'m::finite) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
-
-definition "matrix_inv(A:: 'a::semiring_1^('n::finite)^'m::finite) =
+definition "invertible(A::'a::semiring_1^'n^'m) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
+
+definition "matrix_inv(A:: 'a::semiring_1^'n^'m) =
(SOME A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)"
text{* Correspondence between matrices and linear operators. *}
-definition matrix:: "('a::{plus,times, one, zero}^'m::finite \<Rightarrow> 'a ^ 'n::finite) \<Rightarrow> 'a^'m^'n"
+definition matrix:: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n"
where "matrix f = (\<chi> i j. (f(basis j))$i)"
lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::'a::comm_semiring_1 ^ _))"
by (simp add: linear_def matrix_vector_mult_def Cart_eq ring_simps setsum_right_distrib setsum_addf)
-lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::'a::comm_ring_1 ^ 'n::finite)"
+lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::'a::comm_ring_1 ^ 'n)"
apply (simp add: matrix_def matrix_vector_mult_def Cart_eq mult_commute)
apply clarify
apply (rule linear_componentwise[OF lf, symmetric])
done
-lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::'a::comm_ring_1 ^ 'n::finite))" by (simp add: ext matrix_works)
-
-lemma matrix_of_matrix_vector_mul: "matrix(\<lambda>x. A *v (x :: 'a:: comm_ring_1 ^ 'n::finite)) = A"
+lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::'a::comm_ring_1 ^ 'n))" by (simp add: ext matrix_works)
+
+lemma matrix_of_matrix_vector_mul: "matrix(\<lambda>x. A *v (x :: 'a:: comm_ring_1 ^ 'n)) = A"
by (simp add: matrix_eq matrix_vector_mul_linear matrix_works)
lemma matrix_compose:
- assumes lf: "linear (f::'a::comm_ring_1^'n::finite \<Rightarrow> 'a^'m::finite)"
- and lg: "linear (g::'a::comm_ring_1^'m::finite \<Rightarrow> 'a^_)"
+ assumes lf: "linear (f::'a::comm_ring_1^'n \<Rightarrow> 'a^'m)"
+ and lg: "linear (g::'a::comm_ring_1^'m \<Rightarrow> 'a^_)"
shows "matrix (g o f) = matrix g ** matrix f"
using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]]
by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)
-lemma matrix_vector_column:"(A::'a::comm_semiring_1^('n::finite)^_) *v x = setsum (\<lambda>i. (x$i) *s ((transp A)$i)) (UNIV:: 'n set)"
+lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\<lambda>i. (x$i) *s ((transp A)$i)) (UNIV:: 'n set)"
by (simp add: matrix_vector_mult_def transp_def Cart_eq mult_commute)
-lemma adjoint_matrix: "adjoint(\<lambda>x. (A::'a::comm_ring_1^'n::finite^'m::finite) *v x) = (\<lambda>x. transp A *v x)"
+lemma adjoint_matrix: "adjoint(\<lambda>x. (A::'a::comm_ring_1^'n^'m) *v x) = (\<lambda>x. transp A *v x)"
apply (rule adjoint_unique[symmetric])
apply (rule matrix_vector_mul_linear)
apply (simp add: transp_def dot_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib)
@@ -2213,7 +2201,7 @@
apply (auto simp add: mult_ac)
done
-lemma matrix_adjoint: assumes lf: "linear (f :: 'a::comm_ring_1^'n::finite \<Rightarrow> 'a ^ 'm::finite)"
+lemma matrix_adjoint: assumes lf: "linear (f :: 'a::comm_ring_1^'n \<Rightarrow> 'a ^'m)"
shows "matrix(adjoint f) = transp(matrix f)"
apply (subst matrix_vector_mul[OF lf])
unfolding adjoint_matrix matrix_of_matrix_vector_mul ..
@@ -2287,7 +2275,7 @@
lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
- (\<exists>x::'a ^ 'n::finite. \<forall>i. P i (x$i))" (is "?lhs \<longleftrightarrow> ?rhs")
+ (\<exists>x::'a ^ 'n. \<forall>i. P i (x$i))" (is "?lhs \<longleftrightarrow> ?rhs")
proof-
let ?S = "(UNIV :: 'n set)"
{assume H: "?rhs"
@@ -2310,7 +2298,7 @@
definition "onorm f = Sup {norm (f x)| x. norm x = 1}"
lemma norm_bound_generalize:
- fixes f:: "real ^'n::finite \<Rightarrow> real^'m::finite"
+ fixes f:: "real ^'n \<Rightarrow> real^'m"
assumes lf: "linear f"
shows "(\<forall>x. norm x = 1 \<longrightarrow> norm (f x) \<le> b) \<longleftrightarrow> (\<forall>x. norm (f x) \<le> b * norm x)" (is "?lhs \<longleftrightarrow> ?rhs")
proof-
@@ -2343,7 +2331,7 @@
qed
lemma onorm:
- fixes f:: "real ^'n::finite \<Rightarrow> real ^'m::finite"
+ fixes f:: "real ^'n \<Rightarrow> real ^'m"
assumes lf: "linear f"
shows "norm (f x) <= onorm f * norm x"
and "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
@@ -2367,10 +2355,10 @@
}
qed
-lemma onorm_pos_le: assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'m::finite)" shows "0 <= onorm f"
+lemma onorm_pos_le: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" shows "0 <= onorm f"
using order_trans[OF norm_ge_zero onorm(1)[OF lf, of "basis arbitrary"], unfolded norm_basis] by simp
-lemma onorm_eq_0: assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'m::finite)"
+lemma onorm_eq_0: assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)"
shows "onorm f = 0 \<longleftrightarrow> (\<forall>x. f x = 0)"
using onorm[OF lf]
apply (auto simp add: onorm_pos_le)
@@ -2380,7 +2368,7 @@
apply arith
done
-lemma onorm_const: "onorm(\<lambda>x::real^'n::finite. (y::real ^ 'm::finite)) = norm y"
+lemma onorm_const: "onorm(\<lambda>x::real^'n. (y::real ^'m)) = norm y"
proof-
let ?f = "\<lambda>x::real^'n. (y::real ^ 'm)"
have th: "{norm (?f x)| x. norm x = 1} = {norm y}"
@@ -2390,14 +2378,14 @@
apply (rule Sup_unique) by (simp_all add: setle_def)
qed
-lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n::finite \<Rightarrow> real ^'m::finite)"
+lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n \<Rightarrow> real ^'m)"
shows "0 < onorm f \<longleftrightarrow> ~(\<forall>x. f x = 0)"
unfolding onorm_eq_0[OF lf, symmetric]
using onorm_pos_le[OF lf] by arith
lemma onorm_compose:
- assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'m::finite)"
- and lg: "linear (g::real^'k::finite \<Rightarrow> real^'n::finite)"
+ assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)"
+ and lg: "linear (g::real^'k \<Rightarrow> real^'n)"
shows "onorm (f o g) <= onorm f * onorm g"
apply (rule onorm(2)[OF linear_compose[OF lg lf], rule_format])
unfolding o_def
@@ -2409,18 +2397,18 @@
apply (rule onorm_pos_le[OF lf])
done
-lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real^'m::finite)"
+lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
shows "onorm (\<lambda>x. - f x) \<le> onorm f"
using onorm[OF linear_compose_neg[OF lf]] onorm[OF lf]
unfolding norm_minus_cancel by metis
-lemma onorm_neg: assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real^'m::finite)"
+lemma onorm_neg: assumes lf: "linear (f::real ^'n \<Rightarrow> real^'m)"
shows "onorm (\<lambda>x. - f x) = onorm f"
using onorm_neg_lemma[OF lf] onorm_neg_lemma[OF linear_compose_neg[OF lf]]
by simp
lemma onorm_triangle:
- assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'m::finite)" and lg: "linear g"
+ assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" and lg: "linear g"
shows "onorm (\<lambda>x. f x + g x) <= onorm f + onorm g"
apply(rule onorm(2)[OF linear_compose_add[OF lf lg], rule_format])
apply (rule order_trans)
@@ -2431,14 +2419,14 @@
apply (rule onorm(1)[OF lg])
done
-lemma onorm_triangle_le: "linear (f::real ^'n::finite \<Rightarrow> real ^'m::finite) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) <= e
+lemma onorm_triangle_le: "linear (f::real ^'n \<Rightarrow> real ^'m) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) <= e
\<Longrightarrow> onorm(\<lambda>x. f x + g x) <= e"
apply (rule order_trans)
apply (rule onorm_triangle)
apply assumption+
done
-lemma onorm_triangle_lt: "linear (f::real ^'n::finite \<Rightarrow> real ^'m::finite) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) < e
+lemma onorm_triangle_lt: "linear (f::real ^'n \<Rightarrow> real ^'m) \<Longrightarrow> linear g \<Longrightarrow> onorm(f) + onorm(g) < e
==> onorm(\<lambda>x. f x + g x) < e"
apply (rule order_le_less_trans)
apply (rule onorm_triangle)
@@ -2548,7 +2536,7 @@
apply (auto simp add: Cart_eq matrix_vector_mult_def dest_vec1_def column_def mult_commute UNIV_1)
done
-lemma linear_to_scalars: assumes lf: "linear (f::'a::comm_ring_1 ^'n::finite \<Rightarrow> 'a^1)"
+lemma linear_to_scalars: assumes lf: "linear (f::'a::comm_ring_1 ^'n \<Rightarrow> 'a^1)"
shows "f = (\<lambda>x. vec1(row 1 (matrix f) \<bullet> x))"
apply (rule ext)
apply (subst matrix_works[OF lf, symmetric])
@@ -2683,7 +2671,7 @@
lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y"
unfolding dist_norm by (metis sndcart_sub[symmetric] norm_sndcart)
-lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n::finite) (x2::'a::{times,comm_monoid_add}^'m::finite)) \<bullet> (pastecart y1 y2) = x1 \<bullet> y1 + x2 \<bullet> y2"
+lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n) (x2::'a::{times,comm_monoid_add}^'m)) \<bullet> (pastecart y1 y2) = x1 \<bullet> y1 + x2 \<bullet> y2"
by (simp add: dot_def setsum_UNIV_sum pastecart_def)
text {* TODO: move to NthRoot *}
@@ -3029,7 +3017,7 @@
| span_induct_alt_help_S: "x \<in> S \<Longrightarrow> span_induct_alt_help S z \<Longrightarrow> span_induct_alt_help S (c *s x + z)"
lemma span_induct_alt':
- assumes h0: "h (0::'a::semiring_1^'n::finite)" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c*s x + y)" shows "\<forall>x \<in> span S. h x"
+ assumes h0: "h (0::'a::semiring_1^'n)" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c*s x + y)" shows "\<forall>x \<in> span S. h x"
proof-
{fix x:: "'a^'n" assume x: "span_induct_alt_help S x"
have "h x"
@@ -3078,7 +3066,7 @@
qed
lemma span_induct_alt:
- assumes h0: "h (0::'a::semiring_1^'n::finite)" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c*s x + y)" and x: "x \<in> span S"
+ assumes h0: "h (0::'a::semiring_1^'n)" and hS: "\<And>c x y. x \<in> S \<Longrightarrow> h y \<Longrightarrow> h (c*s x + y)" and x: "x \<in> span S"
shows "h x"
using span_induct_alt'[of h S] h0 hS x by blast
@@ -3424,7 +3412,7 @@
(* Standard bases are a spanning set, and obviously finite. *)
-lemma span_stdbasis:"span {basis i :: 'a::ring_1^'n::finite | i. i \<in> (UNIV :: 'n set)} = UNIV"
+lemma span_stdbasis:"span {basis i :: 'a::ring_1^'n | i. i \<in> (UNIV :: 'n set)} = UNIV"
apply (rule set_ext)
apply auto
apply (subst basis_expansion[symmetric])
@@ -3436,13 +3424,13 @@
apply (auto simp add: Collect_def mem_def)
done
-lemma finite_stdbasis: "finite {basis i ::real^'n::finite |i. i\<in> (UNIV:: 'n set)}" (is "finite ?S")
+lemma finite_stdbasis: "finite {basis i ::real^'n |i. i\<in> (UNIV:: 'n set)}" (is "finite ?S")
proof-
have eq: "?S = basis ` UNIV" by blast
show ?thesis unfolding eq by auto
qed
-lemma card_stdbasis: "card {basis i ::real^'n::finite |i. i\<in> (UNIV :: 'n set)} = CARD('n)" (is "card ?S = _")
+lemma card_stdbasis: "card {basis i ::real^'n |i. i\<in> (UNIV :: 'n set)} = CARD('n)" (is "card ?S = _")
proof-
have eq: "?S = basis ` UNIV" by blast
show ?thesis unfolding eq using card_image[OF basis_inj] by simp
@@ -3466,7 +3454,7 @@
using x span_induct[of ?B ?P x] iS by blast
qed
-lemma independent_stdbasis: "independent {basis i ::real^'n::finite |i. i\<in> (UNIV :: 'n set)}"
+lemma independent_stdbasis: "independent {basis i ::real^'n |i. i\<in> (UNIV :: 'n set)}"
proof-
let ?I = "UNIV :: 'n set"
let ?b = "basis :: _ \<Rightarrow> real ^'n"
@@ -3566,7 +3554,7 @@
(* The general case of the Exchange Lemma, the key to what follows. *)
lemma exchange_lemma:
- assumes f:"finite (t:: ('a::field^'n::finite) set)" and i: "independent s"
+ assumes f:"finite (t:: ('a::field^'n) set)" and i: "independent s"
and sp:"s \<subseteq> span t"
shows "\<exists>t'. (card t' = card t) \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
using f i sp
@@ -3666,7 +3654,7 @@
lemma independent_bound:
- fixes S:: "(real^'n::finite) set"
+ fixes S:: "(real^'n) set"
shows "independent S \<Longrightarrow> finite S \<and> card S <= CARD('n)"
apply (subst card_stdbasis[symmetric])
apply (rule independent_span_bound)
@@ -3676,13 +3664,13 @@
apply (rule subset_UNIV)
done
-lemma dependent_biggerset: "(finite (S::(real ^'n::finite) set) ==> card S > CARD('n)) ==> dependent S"
+lemma dependent_biggerset: "(finite (S::(real ^'n) set) ==> card S > CARD('n)) ==> dependent S"
by (metis independent_bound not_less)
(* Hence we can create a maximal independent subset. *)
lemma maximal_independent_subset_extend:
- assumes sv: "(S::(real^'n::finite) set) \<subseteq> V" and iS: "independent S"
+ assumes sv: "(S::(real^'n) set) \<subseteq> V" and iS: "independent S"
shows "\<exists>B. S \<subseteq> B \<and> B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
using sv iS
proof(induct d\<equiv> "CARD('n) - card S" arbitrary: S rule: nat_less_induct)
@@ -3715,14 +3703,14 @@
qed
lemma maximal_independent_subset:
- "\<exists>(B:: (real ^'n::finite) set). B\<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
+ "\<exists>(B:: (real ^'n) set). B\<subseteq> V \<and> independent B \<and> V \<subseteq> span B"
by (metis maximal_independent_subset_extend[of "{}:: (real ^'n) set"] empty_subsetI independent_empty)
(* Notion of dimension. *)
definition "dim V = (SOME n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = n))"
-lemma basis_exists: "\<exists>B. (B :: (real ^'n::finite) set) \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = dim V)"
+lemma basis_exists: "\<exists>B. (B :: (real ^'n) set) \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = dim V)"
unfolding dim_def some_eq_ex[of "\<lambda>n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = n)"]
using maximal_independent_subset[of V] independent_bound
by auto
@@ -3730,7 +3718,7 @@
(* Consequences of independence or spanning for cardinality. *)
lemma independent_card_le_dim:
- assumes "(B::(real ^'n::finite) set) \<subseteq> V" and "independent B" shows "card B \<le> dim V"
+ assumes "(B::(real ^'n) set) \<subseteq> V" and "independent B" shows "card B \<le> dim V"
proof -
from basis_exists[of V] `B \<subseteq> V`
obtain B' where "independent B'" and "B \<subseteq> span B'" and "card B' = dim V" by blast
@@ -3738,34 +3726,34 @@
show ?thesis by auto
qed
-lemma span_card_ge_dim: "(B::(real ^'n::finite) set) \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> finite B \<Longrightarrow> dim V \<le> card B"
+lemma span_card_ge_dim: "(B::(real ^'n) set) \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> finite B \<Longrightarrow> dim V \<le> card B"
by (metis basis_exists[of V] independent_span_bound subset_trans)
lemma basis_card_eq_dim:
- "B \<subseteq> (V:: (real ^'n::finite) set) \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> finite B \<and> card B = dim V"
+ "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)
-lemma dim_unique: "(B::(real ^'n::finite) set) \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> card B = n \<Longrightarrow> dim V = n"
+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)
(* More lemmas about dimension. *)
-lemma dim_univ: "dim (UNIV :: (real^'n::finite) set) = CARD('n)"
+lemma dim_univ: "dim (UNIV :: (real^'n) set) = CARD('n)"
apply (rule dim_unique[of "{basis i |i. i\<in> (UNIV :: 'n set)}"])
by (auto simp only: span_stdbasis card_stdbasis finite_stdbasis independent_stdbasis)
lemma dim_subset:
- "(S:: (real ^'n::finite) set) \<subseteq> T \<Longrightarrow> dim S \<le> dim T"
+ "(S:: (real ^'n) set) \<subseteq> T \<Longrightarrow> dim S \<le> dim T"
using basis_exists[of T] basis_exists[of S]
by (metis independent_card_le_dim subset_trans)
-lemma dim_subset_univ: "dim (S:: (real^'n::finite) set) \<le> CARD('n)"
+lemma dim_subset_univ: "dim (S:: (real^'n) set) \<le> CARD('n)"
by (metis dim_subset subset_UNIV dim_univ)
(* Converses to those. *)
lemma card_ge_dim_independent:
- assumes BV:"(B::(real ^'n::finite) set) \<subseteq> V" and iB:"independent B" and dVB:"dim V \<le> card B"
+ assumes BV:"(B::(real ^'n) set) \<subseteq> V" and iB:"independent B" and dVB:"dim V \<le> card B"
shows "V \<subseteq> span B"
proof-
{fix a assume aV: "a \<in> V"
@@ -3779,7 +3767,7 @@
qed
lemma card_le_dim_spanning:
- assumes BV: "(B:: (real ^'n::finite) set) \<subseteq> V" and VB: "V \<subseteq> span B"
+ assumes BV: "(B:: (real ^'n) set) \<subseteq> V" and VB: "V \<subseteq> span B"
and fB: "finite B" and dVB: "dim V \<ge> card B"
shows "independent B"
proof-
@@ -3800,7 +3788,7 @@
then show ?thesis unfolding dependent_def by blast
qed
-lemma card_eq_dim: "(B:: (real ^'n::finite) set) \<subseteq> V \<Longrightarrow> card B = dim V \<Longrightarrow> finite B \<Longrightarrow> independent B \<longleftrightarrow> V \<subseteq> span B"
+lemma card_eq_dim: "(B:: (real ^'n) set) \<subseteq> V \<Longrightarrow> card B = dim V \<Longrightarrow> finite B \<Longrightarrow> independent B \<longleftrightarrow> V \<subseteq> span B"
by (metis order_eq_iff card_le_dim_spanning
card_ge_dim_independent)
@@ -3809,13 +3797,13 @@
(* ------------------------------------------------------------------------- *)
lemma independent_bound_general:
- "independent (S:: (real^'n::finite) set) \<Longrightarrow> finite S \<and> card S \<le> dim S"
+ "independent (S:: (real^'n) set) \<Longrightarrow> finite S \<and> card S \<le> dim S"
by (metis independent_card_le_dim independent_bound subset_refl)
-lemma dependent_biggerset_general: "(finite (S:: (real^'n::finite) set) \<Longrightarrow> card S > dim S) \<Longrightarrow> dependent S"
+lemma dependent_biggerset_general: "(finite (S:: (real^'n) set) \<Longrightarrow> card S > dim S) \<Longrightarrow> dependent S"
using independent_bound_general[of S] by (metis linorder_not_le)
-lemma dim_span: "dim (span (S:: (real ^'n::finite) set)) = dim S"
+lemma dim_span: "dim (span (S:: (real ^'n) set)) = dim S"
proof-
have th0: "dim S \<le> dim (span S)"
by (auto simp add: subset_eq intro: dim_subset span_superset)
@@ -3828,10 +3816,10 @@
using fB(2) by arith
qed
-lemma subset_le_dim: "(S:: (real ^'n::finite) set) \<subseteq> span T \<Longrightarrow> dim S \<le> dim T"
+lemma subset_le_dim: "(S:: (real ^'n) set) \<subseteq> span T \<Longrightarrow> dim S \<le> dim T"
by (metis dim_span dim_subset)
-lemma span_eq_dim: "span (S:: (real ^'n::finite) set) = span T ==> dim S = dim T"
+lemma span_eq_dim: "span (S:: (real ^'n) set) = span T ==> dim S = dim T"
by (metis dim_span)
lemma spans_image:
@@ -3841,8 +3829,8 @@
by (metis VB image_mono)
lemma dim_image_le:
- fixes f :: "real^'n::finite \<Rightarrow> real^'m::finite"
- assumes lf: "linear f" shows "dim (f ` S) \<le> dim (S:: (real ^'n::finite) set)"
+ fixes f :: "real^'n \<Rightarrow> real^'m"
+ assumes lf: "linear f" shows "dim (f ` S) \<le> dim (S:: (real ^'n) set)"
proof-
from basis_exists[of S] obtain B where
B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S" by blast
@@ -3886,14 +3874,14 @@
(* FIXME : Move to some general theory ?*)
definition "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x\<noteq>y \<longrightarrow> R x y)"
-lemma vector_sub_project_orthogonal: "(b::'a::ordered_field^'n::finite) \<bullet> (x - ((b \<bullet> x) / (b\<bullet>b)) *s b) = 0"
+lemma vector_sub_project_orthogonal: "(b::'a::ordered_field^'n) \<bullet> (x - ((b \<bullet> x) / (b\<bullet>b)) *s b) = 0"
apply (cases "b = 0", simp)
apply (simp add: dot_rsub dot_rmult)
unfolding times_divide_eq_right[symmetric]
by (simp add: field_simps dot_eq_0)
lemma basis_orthogonal:
- fixes B :: "(real ^'n::finite) set"
+ fixes B :: "(real ^'n) set"
assumes fB: "finite B"
shows "\<exists>C. finite C \<and> card C \<le> card B \<and> span C = span B \<and> pairwise orthogonal C"
(is " \<exists>C. ?P B C")
@@ -3969,7 +3957,7 @@
qed
lemma orthogonal_basis_exists:
- fixes V :: "(real ^'n::finite) set"
+ fixes V :: "(real ^'n) set"
shows "\<exists>B. independent B \<and> B \<subseteq> span V \<and> V \<subseteq> span B \<and> (card B = dim V) \<and> pairwise orthogonal B"
proof-
from basis_exists[of V] obtain B where B: "B \<subseteq> V" "independent B" "V \<subseteq> span B" "card B = dim V" by blast
@@ -3997,7 +3985,7 @@
lemma span_not_univ_orthogonal:
assumes sU: "span S \<noteq> UNIV"
- shows "\<exists>(a:: real ^'n::finite). a \<noteq>0 \<and> (\<forall>x \<in> span S. a \<bullet> x = 0)"
+ shows "\<exists>(a:: real ^'n). a \<noteq>0 \<and> (\<forall>x \<in> span S. a \<bullet> x = 0)"
proof-
from sU obtain a where a: "a \<notin> span S" by blast
from orthogonal_basis_exists obtain B where
@@ -4036,13 +4024,13 @@
qed
lemma span_not_univ_subset_hyperplane:
- assumes SU: "span S \<noteq> (UNIV ::(real^'n::finite) set)"
+ assumes SU: "span S \<noteq> (UNIV ::(real^'n) set)"
shows "\<exists> a. a \<noteq>0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"
using span_not_univ_orthogonal[OF SU] by auto
lemma lowdim_subset_hyperplane:
assumes d: "dim S < CARD('n::finite)"
- shows "\<exists>(a::real ^'n::finite). a \<noteq> 0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"
+ shows "\<exists>(a::real ^'n). a \<noteq> 0 \<and> span S \<subseteq> {x. a \<bullet> x = 0}"
proof-
{assume "span S = UNIV"
hence "dim (span S) = dim (UNIV :: (real ^'n) set)" by simp
@@ -4109,7 +4097,7 @@
lemma linear_independent_extend_lemma:
assumes fi: "finite B" and ib: "independent B"
- shows "\<exists>g. (\<forall>x\<in> span B. \<forall>y\<in> span B. g ((x::'a::field^'n::finite) + y) = g x + g y)
+ shows "\<exists>g. (\<forall>x\<in> span B. \<forall>y\<in> span B. g ((x::'a::field^'n) + y) = g x + g y)
\<and> (\<forall>x\<in> span B. \<forall>c. g (c*s x) = c *s g x)
\<and> (\<forall>x\<in> B. g x = f x)"
using ib fi
@@ -4193,7 +4181,7 @@
qed
lemma linear_independent_extend:
- assumes iB: "independent (B:: (real ^'n::finite) set)"
+ assumes iB: "independent (B:: (real ^'n) set)"
shows "\<exists>g. linear g \<and> (\<forall>x\<in>B. g x = f x)"
proof-
from maximal_independent_subset_extend[of B UNIV] iB
@@ -4246,8 +4234,8 @@
qed
lemma subspace_isomorphism:
- assumes s: "subspace (S:: (real ^'n::finite) set)"
- and t: "subspace (T :: (real ^ 'm::finite) set)"
+ assumes s: "subspace (S:: (real ^'n) set)"
+ and t: "subspace (T :: (real ^'m) set)"
and d: "dim S = dim T"
shows "\<exists>f. linear f \<and> f ` S = T \<and> inj_on f S"
proof-
@@ -4320,7 +4308,7 @@
qed
lemma linear_eq_stdbasis:
- assumes lf: "linear (f::'a::ring_1^'m::finite \<Rightarrow> 'a^'n::finite)" and lg: "linear g"
+ assumes lf: "linear (f::'a::ring_1^'m \<Rightarrow> 'a^'n)" and lg: "linear g"
and fg: "\<forall>i. f (basis i) = g(basis i)"
shows "f = g"
proof-
@@ -4365,7 +4353,7 @@
qed
lemma bilinear_eq_stdbasis:
- assumes bf: "bilinear (f:: 'a::ring_1^'m::finite \<Rightarrow> 'a^'n::finite \<Rightarrow> 'a^_)"
+ assumes bf: "bilinear (f:: 'a::ring_1^'m \<Rightarrow> 'a^'n \<Rightarrow> 'a^_)"
and bg: "bilinear g"
and fg: "\<forall>i j. f (basis i) (basis j) = g (basis i) (basis j)"
shows "f = g"
@@ -4385,7 +4373,7 @@
by (metis matrix_transp_mul transp_mat transp_transp)
lemma linear_injective_left_inverse:
- assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'m::finite)" and fi: "inj f"
+ assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'m)" and fi: "inj f"
shows "\<exists>g. linear g \<and> g o f = id"
proof-
from linear_independent_extend[OF independent_injective_image, OF independent_stdbasis, OF lf fi]
@@ -4401,7 +4389,7 @@
qed
lemma linear_surjective_right_inverse:
- assumes lf: "linear (f:: real ^'m::finite \<Rightarrow> real ^'n::finite)" and sf: "surj f"
+ assumes lf: "linear (f:: real ^'m \<Rightarrow> real ^'n)" and sf: "surj f"
shows "\<exists>g. linear g \<and> f o g = id"
proof-
from linear_independent_extend[OF independent_stdbasis]
@@ -4420,7 +4408,7 @@
qed
lemma matrix_left_invertible_injective:
-"(\<exists>B. (B::real^'m^'n) ** (A::real^'n::finite^'m::finite) = mat 1) \<longleftrightarrow> (\<forall>x y. A *v x = A *v y \<longrightarrow> x = y)"
+"(\<exists>B. (B::real^'m^'n) ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x y. A *v x = A *v y \<longrightarrow> x = y)"
proof-
{fix B:: "real^'m^'n" and x y assume B: "B ** A = mat 1" and xy: "A *v x = A*v y"
from xy have "B*v (A *v x) = B *v (A*v y)" by simp
@@ -4439,13 +4427,13 @@
qed
lemma matrix_left_invertible_ker:
- "(\<exists>B. (B::real ^'m::finite^'n::finite) ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x. A *v x = 0 \<longrightarrow> x = 0)"
+ "(\<exists>B. (B::real ^'m^'n) ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x. A *v x = 0 \<longrightarrow> x = 0)"
unfolding matrix_left_invertible_injective
using linear_injective_0[OF matrix_vector_mul_linear, of A]
by (simp add: inj_on_def)
lemma matrix_right_invertible_surjective:
-"(\<exists>B. (A::real^'n::finite^'m::finite) ** (B::real^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"
+"(\<exists>B. (A::real^'n^'m) ** (B::real^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"
proof-
{fix B :: "real ^'m^'n" assume AB: "A ** B = mat 1"
{fix x :: "real ^ 'm"
@@ -4469,7 +4457,7 @@
qed
lemma matrix_left_invertible_independent_columns:
- fixes A :: "real^'n::finite^'m::finite"
+ fixes A :: "real^'n^'m"
shows "(\<exists>(B::real ^'m^'n). B ** A = mat 1) \<longleftrightarrow> (\<forall>c. setsum (\<lambda>i. c i *s column i A) (UNIV :: 'n set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
(is "?lhs \<longleftrightarrow> ?rhs")
proof-
@@ -4495,14 +4483,14 @@
qed
lemma matrix_right_invertible_independent_rows:
- fixes A :: "real^'n::finite^'m::finite"
+ fixes A :: "real^'n^'m"
shows "(\<exists>(B::real^'m^'n). A ** B = mat 1) \<longleftrightarrow> (\<forall>c. setsum (\<lambda>i. c i *s row i A) (UNIV :: 'm set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
unfolding left_invertible_transp[symmetric]
matrix_left_invertible_independent_columns
by (simp add: column_transp)
lemma matrix_right_invertible_span_columns:
- "(\<exists>(B::real ^'n::finite^'m::finite). (A::real ^'m^'n) ** B = mat 1) \<longleftrightarrow> span (columns A) = UNIV" (is "?lhs = ?rhs")
+ "(\<exists>(B::real ^'n^'m). (A::real ^'m^'n) ** B = mat 1) \<longleftrightarrow> span (columns A) = UNIV" (is "?lhs = ?rhs")
proof-
let ?U = "UNIV :: 'm set"
have fU: "finite ?U" by simp
@@ -4564,7 +4552,7 @@
qed
lemma matrix_left_invertible_span_rows:
- "(\<exists>(B::real^'m::finite^'n::finite). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"
+ "(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"
unfolding right_invertible_transp[symmetric]
unfolding columns_transp[symmetric]
unfolding matrix_right_invertible_span_columns
@@ -4573,7 +4561,7 @@
(* An injective map real^'n->real^'n is also surjective. *)
lemma linear_injective_imp_surjective:
- assumes lf: "linear (f:: real ^'n::finite \<Rightarrow> real ^'n)" and fi: "inj f"
+ assumes lf: "linear (f:: real ^'n \<Rightarrow> real ^'n)" and fi: "inj f"
shows "surj f"
proof-
let ?U = "UNIV :: (real ^'n) set"
@@ -4635,7 +4623,7 @@
qed
lemma linear_surjective_imp_injective:
- assumes lf: "linear (f::real ^'n::finite => real ^'n)" and sf: "surj f"
+ assumes lf: "linear (f::real ^'n => real ^'n)" and sf: "surj f"
shows "inj f"
proof-
let ?U = "UNIV :: (real ^'n) set"
@@ -4694,14 +4682,14 @@
by (simp add: expand_fun_eq o_def id_def)
lemma linear_injective_isomorphism:
- assumes lf: "linear (f :: real^'n::finite \<Rightarrow> real ^'n)" and fi: "inj f"
+ assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'n)" and fi: "inj f"
shows "\<exists>f'. linear f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"
unfolding isomorphism_expand[symmetric]
using linear_surjective_right_inverse[OF lf linear_injective_imp_surjective[OF lf fi]] linear_injective_left_inverse[OF lf fi]
by (metis left_right_inverse_eq)
lemma linear_surjective_isomorphism:
- assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'n)" and sf: "surj f"
+ assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'n)" and sf: "surj f"
shows "\<exists>f'. linear f' \<and> (\<forall>x. f' (f x) = x) \<and> (\<forall>x. f (f' x) = x)"
unfolding isomorphism_expand[symmetric]
using linear_surjective_right_inverse[OF lf sf] linear_injective_left_inverse[OF lf linear_surjective_imp_injective[OF lf sf]]
@@ -4710,7 +4698,7 @@
(* Left and right inverses are the same for R^N->R^N. *)
lemma linear_inverse_left:
- assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'n)" and lf': "linear f'"
+ assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'n)" and lf': "linear f'"
shows "f o f' = id \<longleftrightarrow> f' o f = id"
proof-
{fix f f':: "real ^'n \<Rightarrow> real ^'n"
@@ -4728,7 +4716,7 @@
(* Moreover, a one-sided inverse is automatically linear. *)
lemma left_inverse_linear:
- assumes lf: "linear (f::real ^'n::finite \<Rightarrow> real ^'n)" and gf: "g o f = id"
+ assumes lf: "linear (f::real ^'n \<Rightarrow> real ^'n)" and gf: "g o f = id"
shows "linear g"
proof-
from gf have fi: "inj f" apply (auto simp add: inj_on_def o_def id_def stupid_ext[symmetric])
@@ -4743,7 +4731,7 @@
qed
lemma right_inverse_linear:
- assumes lf: "linear (f:: real ^'n::finite \<Rightarrow> real ^'n)" and gf: "f o g = id"
+ assumes lf: "linear (f:: real ^'n \<Rightarrow> real ^'n)" and gf: "f o g = id"
shows "linear g"
proof-
from gf have fi: "surj f" apply (auto simp add: surj_def o_def id_def stupid_ext[symmetric])
@@ -4760,7 +4748,7 @@
(* The same result in terms of square matrices. *)
lemma matrix_left_right_inverse:
- fixes A A' :: "real ^'n::finite^'n"
+ fixes A A' :: "real ^'n^'n"
shows "A ** A' = mat 1 \<longleftrightarrow> A' ** A = mat 1"
proof-
{fix A A' :: "real ^'n^'n" assume AA': "A ** A' = mat 1"
@@ -4798,11 +4786,11 @@
"columnvector (A *v v) = A ** columnvector v"
by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def)
-lemma dot_matrix_product: "(x::'a::semiring_1^'n::finite) \<bullet> y = (((rowvector x ::'a^'n^1) ** (columnvector y :: 'a^1^'n))$1)$1"
+lemma dot_matrix_product: "(x::'a::semiring_1^'n) \<bullet> y = (((rowvector x ::'a^'n^1) ** (columnvector y :: 'a^1^'n))$1)$1"
by (vector matrix_matrix_mult_def rowvector_def columnvector_def dot_def)
lemma dot_matrix_vector_mul:
- fixes A B :: "real ^'n::finite ^'n" and x y :: "real ^'n"
+ fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"
shows "(A *v x) \<bullet> (B *v y) =
(((rowvector x :: real^'n^1) ** ((transp A ** B) ** (columnvector y :: real ^1^'n)))$1)$1"
unfolding dot_matrix_product transp_columnvector[symmetric]
@@ -4810,7 +4798,7 @@
(* Infinity norm. *)
-definition "infnorm (x::real^'n::finite) = Sup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
+definition "infnorm (x::real^'n) = Sup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
lemma numseg_dimindex_nonempty: "\<exists>i. i \<in> (UNIV :: 'n set)"
by auto
@@ -4820,18 +4808,18 @@
(\<lambda>i. abs(x$i)) ` (UNIV)" by blast
lemma infnorm_set_lemma:
- shows "finite {abs((x::'a::abs ^'n::finite)$i) |i. i\<in> (UNIV :: 'n set)}"
+ shows "finite {abs((x::'a::abs ^'n)$i) |i. i\<in> (UNIV :: 'n set)}"
and "{abs(x$i) |i. i\<in> (UNIV :: 'n::finite set)} \<noteq> {}"
unfolding infnorm_set_image
by (auto intro: finite_imageI)
-lemma infnorm_pos_le: "0 \<le> infnorm (x::real^'n::finite)"
+lemma infnorm_pos_le: "0 \<le> infnorm (x::real^'n)"
unfolding infnorm_def
unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
unfolding infnorm_set_image
by auto
-lemma infnorm_triangle: "infnorm ((x::real^'n::finite) + y) \<le> infnorm x + infnorm y"
+lemma infnorm_triangle: "infnorm ((x::real^'n) + y) \<le> infnorm x + infnorm y"
proof-
have th: "\<And>x y (z::real). x - y <= z \<longleftrightarrow> x - z <= y" by arith
have th1: "\<And>S f. f ` S = { f i| i. i \<in> S}" by blast
@@ -4852,7 +4840,7 @@
done
qed
-lemma infnorm_eq_0: "infnorm x = 0 \<longleftrightarrow> (x::real ^'n::finite) = 0"
+lemma infnorm_eq_0: "infnorm x = 0 \<longleftrightarrow> (x::real ^'n) = 0"
proof-
have "infnorm x <= 0 \<longleftrightarrow> x = 0"
unfolding infnorm_def
@@ -4894,7 +4882,7 @@
using infnorm_pos_le[of x] by arith
lemma component_le_infnorm:
- shows "\<bar>x$i\<bar> \<le> infnorm (x::real^'n::finite)"
+ shows "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)"
proof-
let ?U = "UNIV :: 'n set"
let ?S = "{\<bar>x$i\<bar> |i. i\<in> ?U}"
@@ -4947,7 +4935,7 @@
unfolding infnorm_set_image ball_simps
by (metis component_le_norm)
lemma card_enum: "card {1 .. n} = n" by auto
-lemma norm_le_infnorm: "norm(x) <= sqrt(real CARD('n)) * infnorm(x::real ^'n::finite)"
+lemma norm_le_infnorm: "norm(x) <= sqrt(real CARD('n)) * infnorm(x::real ^'n)"
proof-
let ?d = "CARD('n)"
have "real ?d \<ge> 0" by simp
@@ -4973,7 +4961,7 @@
(* Equality in Cauchy-Schwarz and triangle inequalities. *)
-lemma norm_cauchy_schwarz_eq: "(x::real ^'n::finite) \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *s y = norm y *s x" (is "?lhs \<longleftrightarrow> ?rhs")
+lemma norm_cauchy_schwarz_eq: "(x::real ^'n) \<bullet> y = norm x * norm y \<longleftrightarrow> norm x *s y = norm y *s x" (is "?lhs \<longleftrightarrow> ?rhs")
proof-
{assume h: "x = 0"
hence ?thesis by simp}
@@ -5000,7 +4988,7 @@
qed
lemma norm_cauchy_schwarz_abs_eq:
- fixes x y :: "real ^ 'n::finite"
+ fixes x y :: "real ^ 'n"
shows "abs(x \<bullet> y) = norm x * norm y \<longleftrightarrow>
norm x *s y = norm y *s x \<or> norm(x) *s y = - norm y *s x" (is "?lhs \<longleftrightarrow> ?rhs")
proof-
@@ -5019,7 +5007,7 @@
qed
lemma norm_triangle_eq:
- fixes x y :: "real ^ 'n::finite"
+ fixes x y :: "real ^ 'n"
shows "norm(x + y) = norm x + norm y \<longleftrightarrow> norm x *s y = norm y *s x"
proof-
{assume x: "x =0 \<or> y =0"
@@ -5099,7 +5087,7 @@
qed
lemma norm_cauchy_schwarz_equal:
- fixes x y :: "real ^ 'n::finite"
+ fixes x y :: "real ^ 'n"
shows "abs(x \<bullet> y) = norm x * norm y \<longleftrightarrow> collinear {(0::real^'n),x,y}"
unfolding norm_cauchy_schwarz_abs_eq
apply (cases "x=0", simp_all add: collinear_2)
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Jan 07 17:43:35 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Jan 07 18:56:39 2010 +0100
@@ -11,8 +11,7 @@
subsection {* Finite Cartesian products, with indexing and lambdas. *}
typedef (open Cart)
- ('a, 'b) "^" (infixl "^" 15)
- = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
+ ('a, 'b) cart = "UNIV :: (('b::finite) \<Rightarrow> 'a) set"
morphisms Cart_nth Cart_lambda ..
notation Cart_nth (infixl "$" 90)
@@ -20,8 +19,8 @@
notation (xsymbols) Cart_lambda (binder "\<chi>" 10)
(*
- Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n needs more than one
- type class write "cart 'b ('n::{finite, ...})"
+ Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than
+ the finite type class write "cart 'b 'n"
*)
syntax "_finite_cart" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15)
@@ -45,15 +44,13 @@
apply auto
done
-lemma Cart_eq: "((x:: 'a ^ 'b::finite) = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
+lemma Cart_eq: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
by (simp add: Cart_nth_inject [symmetric] expand_fun_eq)
lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i"
by (simp add: Cart_lambda_inverse)
-lemma Cart_lambda_unique:
- fixes f :: "'a ^ 'b::finite"
- shows "(\<forall>i. f$i = g i) \<longleftrightarrow> Cart_lambda g = f"
+lemma Cart_lambda_unique: "(\<forall>i. f$i = g i) \<longleftrightarrow> Cart_lambda g = f"
by (auto simp add: Cart_eq)
lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g"
@@ -61,14 +58,9 @@
text{* A non-standard sum to "paste" Cartesian products. *}
-definition pastecart :: "'a ^ 'm::finite \<Rightarrow> 'a ^ 'n::finite \<Rightarrow> 'a ^ ('m + 'n)" where
- "pastecart f g = (\<chi> i. case i of Inl a \<Rightarrow> f$a | Inr b \<Rightarrow> g$b)"
-
-definition fstcart:: "'a ^('m::finite + 'n::finite) \<Rightarrow> 'a ^ 'm" where
- "fstcart f = (\<chi> i. (f$(Inl i)))"
-
-definition sndcart:: "'a ^('m::finite + 'n::finite) \<Rightarrow> 'a ^ 'n" where
- "sndcart f = (\<chi> i. (f$(Inr i)))"
+definition "pastecart f g = (\<chi> i. case i of Inl a \<Rightarrow> f$a | Inr b \<Rightarrow> g$b)"
+definition "fstcart f = (\<chi> i. (f$(Inl i)))"
+definition "sndcart f = (\<chi> i. (f$(Inr i)))"
lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a"
unfolding pastecart_def by simp
@@ -85,10 +77,10 @@
lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr"
by (auto, case_tac x, auto)
-lemma fstcart_pastecart: "fstcart (pastecart (x::'a ^'m::finite ) (y:: 'a ^ 'n::finite)) = x"
+lemma fstcart_pastecart: "fstcart (pastecart x y) = x"
by (simp add: Cart_eq)
-lemma sndcart_pastecart: "sndcart (pastecart (x::'a ^'m::finite ) (y:: 'a ^ 'n::finite)) = y"
+lemma sndcart_pastecart: "sndcart (pastecart x y) = y"
by (simp add: Cart_eq)
lemma pastecart_fst_snd: "pastecart (fstcart z) (sndcart z) = z"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jan 07 17:43:35 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Jan 07 18:56:39 2010 +0100
@@ -532,7 +532,7 @@
apply (auto simp add: dist_norm)
done
-instance "^" :: (perfect_space, finite) perfect_space
+instance cart :: (perfect_space, finite) perfect_space
proof
fix x :: "'a ^ 'b"
{
@@ -565,7 +565,7 @@
lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
unfolding islimpt_def by auto
-lemma closed_positive_orthant: "closed {x::real^'n::finite. \<forall>i. 0 \<le>x$i}"
+lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
proof-
let ?U = "UNIV :: 'n set"
let ?O = "{x::real^'n. \<forall>i. x$i\<ge>0}"
@@ -1296,7 +1296,7 @@
qed
lemma Lim_component:
- fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n::finite"
+ fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n"
shows "(f ---> l) net \<Longrightarrow> ((\<lambda>a. f a $i) ---> l$i) net"
unfolding tendsto_iff
apply (clarify)
@@ -2284,7 +2284,7 @@
done
lemma compact_lemma:
- fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n::finite"
+ fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n"
assumes "bounded s" and "\<forall>n. f n \<in> s"
shows "\<forall>d.
\<exists>l r. subseq r \<and>
@@ -2317,7 +2317,7 @@
qed
qed
-instance "^" :: (heine_borel, finite) heine_borel
+instance cart :: (heine_borel, finite) heine_borel
proof
fix s :: "('a ^ 'b) set" and f :: "nat \<Rightarrow> 'a ^ 'b"
assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
@@ -4283,7 +4283,7 @@
qed
lemma closed_pastecart:
- fixes s :: "(real ^ 'a::finite) set" (* FIXME: generalize *)
+ fixes s :: "(real ^ 'a) set" (* FIXME: generalize *)
assumes "closed s" "closed t"
shows "closed {pastecart x y | x y . x \<in> s \<and> y \<in> t}"
proof-
@@ -4623,12 +4623,12 @@
(* A cute way of denoting open and closed intervals using overloading. *)
-lemma interval: fixes a :: "'a::ord^'n::finite" shows
+lemma interval: fixes a :: "'a::ord^'n" shows
"{a <..< b} = {x::'a^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" and
"{a .. b} = {x::'a^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}"
by (auto simp add: expand_set_eq vector_less_def vector_le_def)
-lemma mem_interval: fixes a :: "'a::ord^'n::finite" shows
+lemma mem_interval: fixes a :: "'a::ord^'n" shows
"x \<in> {a<..<b} \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)"
"x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)"
using interval[of a b] by(auto simp add: expand_set_eq vector_less_def vector_le_def)
@@ -4647,7 +4647,7 @@
apply(rule_tac x="dest_vec1 x" in bexI) by auto
-lemma interval_eq_empty: fixes a :: "real^'n::finite" shows
+lemma interval_eq_empty: fixes a :: "real^'n" shows
"({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1) and
"({a .. b} = {} \<longleftrightarrow> (\<exists>i. b$i < a$i))" (is ?th2)
proof-
@@ -4682,12 +4682,12 @@
ultimately show ?th2 by blast
qed
-lemma interval_ne_empty: fixes a :: "real^'n::finite" shows
+lemma interval_ne_empty: fixes a :: "real^'n" shows
"{a .. b} \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i \<le> b$i)" and
"{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i < b$i)"
unfolding interval_eq_empty[of a b] by (auto simp add: not_less not_le) (* BH: Why doesn't just "auto" work here? *)
-lemma subset_interval_imp: fixes a :: "real^'n::finite" shows
+lemma subset_interval_imp: fixes a :: "real^'n" shows
"(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}" and
"(\<forall>i. a$i < c$i \<and> d$i < b$i) \<Longrightarrow> {c .. d} \<subseteq> {a<..<b}" and
"(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> {c<..<d} \<subseteq> {a .. b}" and
@@ -4695,14 +4695,14 @@
unfolding subset_eq[unfolded Ball_def] unfolding mem_interval
by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *)
-lemma interval_sing: fixes a :: "'a::linorder^'n::finite" shows
+lemma interval_sing: fixes a :: "'a::linorder^'n" shows
"{a .. a} = {a} \<and> {a<..<a} = {}"
apply(auto simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
apply (simp add: order_eq_iff)
apply (auto simp add: not_less less_imp_le)
done
-lemma interval_open_subset_closed: fixes a :: "'a::preorder^'n::finite" shows
+lemma interval_open_subset_closed: fixes a :: "'a::preorder^'n" shows
"{a<..<b} \<subseteq> {a .. b}"
proof(simp add: subset_eq, rule)
fix x
@@ -4723,7 +4723,7 @@
by(simp add: expand_set_eq vector_less_def vector_le_def Cart_eq)
qed
-lemma subset_interval: fixes a :: "real^'n::finite" shows
+lemma subset_interval: fixes a :: "real^'n" shows
"{c .. d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i. c$i \<le> d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th1) and
"{c .. d} \<subseteq> {a<..<b} \<longleftrightarrow> (\<forall>i. c$i \<le> d$i) --> (\<forall>i. a$i < c$i \<and> d$i < b$i)" (is ?th2) and
"{c<..<d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i. c$i < d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th3) and
@@ -4775,7 +4775,7 @@
thus ?th4 unfolding subset_eq and Ball_def and mem_interval apply auto apply (erule_tac x=ia in allE, simp)+ by (erule_tac x=i in allE, erule_tac x=i in allE, simp)+
qed
-lemma disjoint_interval: fixes a::"real^'n::finite" shows
+lemma disjoint_interval: fixes a::"real^'n" shows
"{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i. (b$i < a$i \<or> d$i < c$i \<or> b$i < c$i \<or> d$i < a$i))" (is ?th1) and
"{a .. b} \<inter> {c<..<d} = {} \<longleftrightarrow> (\<exists>i. (b$i < a$i \<or> d$i \<le> c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th2) and
"{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i. (b$i \<le> a$i \<or> d$i < c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th3) and
@@ -4789,7 +4789,7 @@
done
qed
-lemma inter_interval: fixes a :: "'a::linorder^'n::finite" shows
+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)
@@ -4800,7 +4800,7 @@
"a < x \<Longrightarrow> x < b ==> (\<exists>d>0. \<forall>x'. abs(x' - x) < d --> a < x' \<and> x' < b)"
by(rule_tac x="min (x - a) (b - x)" in exI, auto)
-lemma open_interval: fixes a :: "real^'n::finite" shows "open {a<..<b}"
+lemma open_interval: fixes a :: "real^'n" shows "open {a<..<b}"
proof-
{ fix x assume x:"x\<in>{a<..<b}"
{ fix i
@@ -4834,7 +4834,7 @@
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)
-lemma closed_interval: fixes a :: "real^'n::finite" shows "closed {a .. b}"
+lemma closed_interval: fixes a :: "real^'n" shows "closed {a .. b}"
proof-
{ fix x i assume as:"\<forall>e>0. \<exists>x'\<in>{a..b}. x' \<noteq> x \<and> dist x' x < e"(* and xab:"a$i > x$i \<or> b$i < x$i"*)
{ assume xa:"a$i > x$i"
@@ -4853,7 +4853,7 @@
thus ?thesis unfolding closed_limpt islimpt_approachable mem_interval by auto
qed
-lemma interior_closed_interval: fixes a :: "real^'n::finite" shows
+lemma interior_closed_interval: fixes a :: "real^'n" shows
"interior {a .. b} = {a<..<b}" (is "?L = ?R")
proof(rule subset_antisym)
show "?R \<subseteq> ?L" using interior_maximal[OF interval_open_subset_closed open_interval] by auto
@@ -4878,7 +4878,7 @@
thus "?L \<subseteq> ?R" unfolding interior_def and subset_eq by auto
qed
-lemma bounded_closed_interval: fixes a :: "real^'n::finite" shows
+lemma bounded_closed_interval: fixes a :: "real^'n" shows
"bounded {a .. b}"
proof-
let ?b = "\<Sum>i\<in>UNIV. \<bar>a$i\<bar> + \<bar>b$i\<bar>"
@@ -4890,23 +4890,23 @@
thus ?thesis unfolding interval and bounded_iff by auto
qed
-lemma bounded_interval: fixes a :: "real^'n::finite" shows
+lemma bounded_interval: fixes a :: "real^'n" shows
"bounded {a .. b} \<and> bounded {a<..<b}"
using bounded_closed_interval[of a b]
using interval_open_subset_closed[of a b]
using bounded_subset[of "{a..b}" "{a<..<b}"]
by simp
-lemma not_interval_univ: fixes a :: "real^'n::finite" shows
+lemma not_interval_univ: fixes a :: "real^'n" shows
"({a .. b} \<noteq> UNIV) \<and> ({a<..<b} \<noteq> UNIV)"
using bounded_interval[of a b]
by auto
-lemma compact_interval: fixes a :: "real^'n::finite" shows
+lemma compact_interval: fixes a :: "real^'n" shows
"compact {a .. b}"
using bounded_closed_imp_compact using bounded_interval[of a b] using closed_interval[of a b] by auto
-lemma open_interval_midpoint: fixes a :: "real^'n::finite"
+lemma open_interval_midpoint: fixes a :: "real^'n"
assumes "{a<..<b} \<noteq> {}" shows "((1/2) *\<^sub>R (a + b)) \<in> {a<..<b}"
proof-
{ fix i
@@ -4917,7 +4917,7 @@
thus ?thesis unfolding mem_interval by auto
qed
-lemma open_closed_interval_convex: fixes x :: "real^'n::finite"
+lemma open_closed_interval_convex: fixes x :: "real^'n"
assumes x:"x \<in> {a<..<b}" and y:"y \<in> {a .. b}" and e:"0 < e" "e \<le> 1"
shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> {a<..<b}"
proof-
@@ -4941,7 +4941,7 @@
thus ?thesis unfolding mem_interval by auto
qed
-lemma closure_open_interval: fixes a :: "real^'n::finite"
+lemma closure_open_interval: fixes a :: "real^'n"
assumes "{a<..<b} \<noteq> {}"
shows "closure {a<..<b} = {a .. b}"
proof-
@@ -4973,7 +4973,7 @@
thus ?thesis using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast
qed
-lemma bounded_subset_open_interval_symmetric: fixes s::"(real^'n::finite) set"
+lemma bounded_subset_open_interval_symmetric: fixes s::"(real^'n) set"
assumes "bounded s" shows "\<exists>a. s \<subseteq> {-a<..<a}"
proof-
obtain b where "b>0" and b:"\<forall>x\<in>s. norm x \<le> b" using assms[unfolded bounded_pos] by auto
@@ -4987,12 +4987,12 @@
qed
lemma bounded_subset_open_interval:
- fixes s :: "(real ^ 'n::finite) set"
+ fixes s :: "(real ^ 'n) set"
shows "bounded s ==> (\<exists>a b. s \<subseteq> {a<..<b})"
by (auto dest!: bounded_subset_open_interval_symmetric)
lemma bounded_subset_closed_interval_symmetric:
- fixes s :: "(real ^ 'n::finite) set"
+ fixes s :: "(real ^ 'n) set"
assumes "bounded s" shows "\<exists>a. s \<subseteq> {-a .. a}"
proof-
obtain a where "s \<subseteq> {- a<..<a}" using bounded_subset_open_interval_symmetric[OF assms] by auto
@@ -5000,7 +5000,7 @@
qed
lemma bounded_subset_closed_interval:
- fixes s :: "(real ^ 'n::finite) set"
+ fixes s :: "(real ^ 'n) set"
shows "bounded s ==> (\<exists>a b. s \<subseteq> {a .. b})"
using bounded_subset_closed_interval_symmetric[of s] by auto
@@ -5018,7 +5018,7 @@
case False thus ?thesis unfolding frontier_def and closure_open_interval[OF False] and interior_open[OF open_interval] by auto
qed
-lemma inter_interval_mixed_eq_empty: fixes a :: "real^'n::finite"
+lemma inter_interval_mixed_eq_empty: fixes a :: "real^'n"
assumes "{c<..<d} \<noteq> {}" shows "{a<..<b} \<inter> {c .. d} = {} \<longleftrightarrow> {a<..<b} \<inter> {c<..<d} = {}"
unfolding closure_open_interval[OF assms, THEN sym] unfolding open_inter_closure_eq_empty[OF open_interval] ..
@@ -5081,7 +5081,7 @@
(* Some stuff for half-infinite intervals too; FIXME: notation? *)
-lemma closed_interval_left: fixes b::"real^'n::finite"
+lemma closed_interval_left: fixes b::"real^'n"
shows "closed {x::real^'n. \<forall>i. x$i \<le> b$i}"
proof-
{ fix i
@@ -5093,7 +5093,7 @@
thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
qed
-lemma closed_interval_right: fixes a::"real^'n::finite"
+lemma closed_interval_right: fixes a::"real^'n"
shows "closed {x::real^'n. \<forall>i. a$i \<le> x$i}"
proof-
{ fix i
@@ -5109,7 +5109,7 @@
definition "is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a$i \<le> x$i \<and> x$i \<le> b$i) \<or> (b$i \<le> x$i \<and> x$i \<le> a$i))) \<longrightarrow> x \<in> s)"
-lemma is_interval_interval: "is_interval {a .. b::real^'n::finite}" (is ?th1) "is_interval {a<..<b}" (is ?th2) proof -
+lemma is_interval_interval: "is_interval {a .. b::real^'n}" (is ?th1) "is_interval {a<..<b}" (is ?th2) proof -
have *:"\<And>x y z::real. x < y \<Longrightarrow> y < z \<Longrightarrow> x < z" by auto
show ?th1 ?th2 unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff
by(meson real_le_trans le_less_trans less_le_trans *)+ qed
@@ -5158,11 +5158,11 @@
qed
lemma closed_halfspace_component_le:
- shows "closed {x::real^'n::finite. x$i \<le> a}"
+ shows "closed {x::real^'n. x$i \<le> a}"
using closed_halfspace_le[of "(basis i)::real^'n" a] unfolding inner_basis[OF assms] by auto
lemma closed_halfspace_component_ge:
- shows "closed {x::real^'n::finite. x$i \<ge> a}"
+ shows "closed {x::real^'n. x$i \<ge> a}"
using closed_halfspace_ge[of a "(basis i)::real^'n"] unfolding inner_basis[OF assms] by auto
text{* Openness of halfspaces. *}
@@ -5180,16 +5180,16 @@
qed
lemma open_halfspace_component_lt:
- shows "open {x::real^'n::finite. x$i < a}"
+ shows "open {x::real^'n. x$i < a}"
using open_halfspace_lt[of "(basis i)::real^'n" a] unfolding inner_basis[OF assms] by auto
lemma open_halfspace_component_gt:
- shows "open {x::real^'n::finite. x$i > a}"
+ shows "open {x::real^'n. x$i > a}"
using open_halfspace_gt[of a "(basis i)::real^'n"] unfolding inner_basis[OF assms] by auto
text{* This gives a simple derivation of limit component bounds. *}
-lemma Lim_component_le: fixes f :: "'a \<Rightarrow> real^'n::finite"
+lemma Lim_component_le: fixes f :: "'a \<Rightarrow> real^'n"
assumes "(f ---> l) net" "\<not> (trivial_limit net)" "eventually (\<lambda>x. f(x)$i \<le> b) net"
shows "l$i \<le> b"
proof-
@@ -5198,7 +5198,7 @@
using closed_halfspace_le[of "(basis i)::real^'n" b] and assms(1,2,3) by auto
qed
-lemma Lim_component_ge: fixes f :: "'a \<Rightarrow> real^'n::finite"
+lemma Lim_component_ge: fixes f :: "'a \<Rightarrow> real^'n"
assumes "(f ---> l) net" "\<not> (trivial_limit net)" "eventually (\<lambda>x. b \<le> (f x)$i) net"
shows "b \<le> l$i"
proof-
@@ -5207,7 +5207,7 @@
using closed_halfspace_ge[of b "(basis i)::real^'n"] and assms(1,2,3) by auto
qed
-lemma Lim_component_eq: fixes f :: "'a \<Rightarrow> real^'n::finite"
+lemma Lim_component_eq: fixes f :: "'a \<Rightarrow> real^'n"
assumes net:"(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\<lambda>x. f(x)$i = b) net"
shows "l$i = b"
using ev[unfolded order_eq_iff eventually_and] using Lim_component_ge[OF net, of b i] and Lim_component_le[OF net, of i b] by auto
@@ -5270,7 +5270,7 @@
ultimately show False using assms(1)[unfolded connected_def not_ex, THEN spec[where x="?A"], THEN spec[where x="?B"]] and assms(2-5) by auto
qed
-lemma connected_ivt_component: fixes x::"real^'n::finite" shows
+lemma connected_ivt_component: fixes x::"real^'n" shows
"connected s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x$k \<le> a \<Longrightarrow> a \<le> y$k \<Longrightarrow> (\<exists>z\<in>s. z$k = a)"
using connected_ivt_hyperplane[of s x y "(basis k)::real^'n" a] by (auto simp add: inner_basis)
@@ -5456,7 +5456,7 @@
text{* "Isometry" (up to constant bounds) of injective linear map etc. *}
lemma cauchy_isometric:
- fixes x :: "nat \<Rightarrow> real ^ 'n::finite"
+ fixes x :: "nat \<Rightarrow> real ^ 'n"
assumes e:"0 < e" and s:"subspace s" and f:"bounded_linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and xs:"\<forall>n::nat. x n \<in> s" and cf:"Cauchy(f o x)"
shows "Cauchy x"
proof-
@@ -5499,7 +5499,7 @@
shows "dist 0 x = norm x"
unfolding dist_norm by simp
-lemma injective_imp_isometric: fixes f::"real^'m::finite \<Rightarrow> real^'n::finite"
+lemma injective_imp_isometric: fixes f::"real^'m \<Rightarrow> real^'n"
assumes s:"closed s" "subspace s" and f:"bounded_linear f" "\<forall>x\<in>s. (f x = 0) \<longrightarrow> (x = 0)"
shows "\<exists>e>0. \<forall>x\<in>s. norm (f x) \<ge> e * norm(x)"
proof(cases "s \<subseteq> {0::real^'m}")
@@ -5567,7 +5567,7 @@
unfolding subspace_def by(auto simp add: vector_add_component vector_smult_component elim!: ballE)
lemma closed_substandard:
- "closed {x::real^'n::finite. \<forall>i. P i --> x$i = 0}" (is "closed ?A")
+ "closed {x::real^'n. \<forall>i. P i --> x$i = 0}" (is "closed ?A")
proof-
let ?D = "{i. P i}"
let ?Bs = "{{x::real^'n. inner (basis i) x = 0}| i. i \<in> ?D}"
@@ -5587,7 +5587,7 @@
qed
lemma dim_substandard:
- shows "dim {x::real^'n::finite. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0} = card d" (is "dim ?A = _")
+ shows "dim {x::real^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0} = card d" (is "dim ?A = _")
proof-
let ?D = "UNIV::'n set"
let ?B = "(basis::'n\<Rightarrow>real^'n) ` d"
@@ -5653,7 +5653,7 @@
apply (subgoal_tac "A \<noteq> UNIV", auto)
done
-lemma closed_subspace: fixes s::"(real^'n::finite) set"
+lemma closed_subspace: fixes s::"(real^'n) set"
assumes "subspace s" shows "closed s"
proof-
have "dim s \<le> card (UNIV :: 'n set)" using dim_subset_univ by auto
@@ -5742,7 +5742,7 @@
by metis
lemma image_affinity_interval: fixes m::real
- fixes a b c :: "real^'n::finite"
+ fixes a b c :: "real^'n"
shows "(\<lambda>x. m *\<^sub>R x + c) ` {a .. b} =
(if {a .. b} = {} then {}
else (if 0 \<le> m then {m *\<^sub>R a + c .. m *\<^sub>R b + c}
@@ -5780,7 +5780,7 @@
ultimately show ?thesis using False by auto
qed
-lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::real^'n::finite)) ` {a..b} =
+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})"
using image_affinity_interval[of m 0 a b] by auto