# HG changeset patch # User hoelzl # Date 1262886999 -3600 # Node ID 4e896680897eb62801ecd3bd13e7e88f8c1a7651 # Parent 1edf0f223c6ea5475ad02dddc2b4a84670547962 finite annotation on cartesian product is now implicit. diff -r 1edf0f223c6e -r 4e896680897e src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- 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" "\ (\x\s. (f x = (0::real^'n::finite)))" + assumes "compact s" "continuous_on s f" "\ (\x\s. (f x = (0::real^'n)))" obtains d where "0 < d" "\x\s. d \ norm(f x)" proof(cases "s={}") case False have "continuous_on s (norm \ f)" by(rule continuous_on_intros continuous_on_norm assms(2))+ then obtain x where x:"x\s" "\y\s. (norm \ f) x \ (norm \ f) y" @@ -1161,7 +1161,7 @@ apply(drule_tac assms(1)[rule_format]) by auto } hence "?R 0 \ ?R 1" by auto thus ?case by auto qed qed -lemma brouwer_cube: fixes f::"real^'n::finite \ real^'n::finite" +lemma brouwer_cube: fixes f::"real^'n \ real^'n" assumes "continuous_on {0..1} f" "f ` {0..1} \ {0..1}" shows "\x\{0..1}. f x = x" apply(rule ccontr) proof- def n \ "CARD('n)" have n:"1 \ n" "0 < n" "n \ 0" unfolding n_def by auto @@ -1291,7 +1291,7 @@ subsection {* Retractions. *} -definition "retraction s t (r::real^'n::finite\real^'n) \ +definition "retraction s t (r::real^'n\real^'n) \ t \ s \ continuous_on s r \ (r ` s \ t) \ (\x\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 \ s" "continuous_on s r" "r ` s \ t" "\y\t. r (i y) = y" "\f. continuous_on s f \ f ` s \ s \ (\x\s. f x = x)" "continuous_on t g" "g ` t \ t" obtains y where "y\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 "(\f. continuous_on s f \ f ` s \ s \ (\x\s. f x = x)) \ (\g. continuous_on t g \ g ` t \ t \ (\y\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 \ real^'n::finite" +lemma brouwer_weak: fixes f::"real^'n \ real^'n" assumes "compact s" "convex s" "interior s \ {}" "continuous_on s f" "f ` s \ s" obtains x where "x \ s" "f x = x" proof- have *:"interior {0..1::real^'n} \ {}" 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 \ real^'n::finite" +lemma brouwer_ball: fixes f::"real^'n \ real^'n" assumes "0 < e" "continuous_on (cball a e) f" "f ` (cball a e) \ (cball a e)" obtains x where "x \ 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 \ real^'n::finite" +lemma brouwer: fixes f::"real^'n \ real^'n" assumes "compact s" "convex s" "s \ {}" "continuous_on s f" "f ` s \ s" obtains x where "x \ s" "f x = x" proof- have "\e>0. s \ cball 0 e" using compact_imp_bounded[OF assms(1)] unfolding bounded_pos @@ -1389,7 +1389,7 @@ subsection {*Bijections between intervals. *} -definition "interval_bij = (\ (a,b) (u,v) (x::real^'n::finite). +definition "interval_bij = (\ (a,b) (u,v) (x::real^'n). (\ 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 \ {a..b}" "{u..v} \ {}" - shows "interval_bij (a,b) (u,v) x \ {u..v::real^'n::finite}" + shows "interval_bij (a,b) (u,v) x \ {u..v::real^'n}" unfolding interval_bij_def split_conv mem_interval Cart_lambda_beta proof(rule,rule) fix i::'n have "{a..b} \ {}" using assms by auto hence *:"a$i \ b$i" "u$i \ 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 diff -r 1edf0f223c6e -r 4e896680897e src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- 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\A \ A \ {}" by auto -lemma norm_not_0:"(x::real^'n::finite)\0 \ norm x \ 0" by auto +lemma norm_not_0:"(x::real^'n)\0 \ norm x \ 0" by auto lemma setsum_delta_notmem: assumes "x\s" shows "setsum (\y. if (y = x) then P x else Q y) s = setsum Q s" @@ -61,7 +61,7 @@ "(x \ {a<.. dest_vec1 a < dest_vec1 x \ 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:"(\x. m *\<^sub>R (x::real^'n::finite)) ` {a..b} = +lemma image_smult_interval:"(\x. m *\<^sub>R (x::real^'n)) ` {a..b} = (if {a..b} = {} then {} else if 0 \ 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 \ norm x = norm y" by auto -lemma norm_minus_eqI:"(x::real^'n::finite) = - y \ norm x = norm y" by auto +lemma norm_minus_eqI:"(x::real^'n) = - y \ norm x = norm y" by auto lemma Min_grI: assumes "finite A" "A \ {}" "\a\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. (\i. 0 \ x$i)}" +lemma convex_positive_orthant: "convex {x::real^'n. (\i. 0 \ 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 \ 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 \ dim s + 2" + assumes "finite (s::(real^'n) set)" "card s \ dim s + 2" shows "affine_dependent s" proof- from assms(2) have "s \ {}" 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. \s u. finite s \ s \ p \ card s \ CARD('n) + 1 \ (\x\s. 0 \ u x) \ setsum u s = 1 \ setsum (\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. \s. finite s \ s \ p \ + "convex hull p = {x::real^'n. \s. finite s \ s \ p \ card s \ CARD('n) + 1 \ x \ convex hull s}" unfolding expand_set_eq apply(rule, rule) unfolding mem_Collect_eq proof- fix x assume "x \ 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 \ real ^ 'n \ real ^ 'n" where + closest_point :: "(real ^ 'n) set \ real ^ 'n \ real ^ 'n" where "closest_point s a = (SOME x. x \ s \ (\y\s. dist a x \ dist a y))" lemma closest_point_exists: @@ -1580,7 +1580,7 @@ lemma norm_le: "norm x \ norm y \ inner x x \ 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 "\u>0. \v>0. v \ u \ 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 "\u>0. u \ 1 \ dist (x + u *\<^sub>R (z - x)) y < dist x y" proof- obtain u where "u>0" and u:"\v>0. v \ u \ 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 \ s" + assumes "convex (s::(real^'n) set)" "closed s" "0 \ s" shows "\a b. a \ 0 \ 0 < b \ (\x\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 \ {}" "s \ t = {}" + assumes "convex (s::(real^'n) set)" "closed s" "convex t" "compact t" "t \ {}" "s \ t = {}" shows "\a b. (\x\s. inner a x < b) \ (\x\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) \ s" + assumes "convex s" "(0::real^'n) \ s" shows "\a. a \ 0 \ (\x\s. 0 \ inner a x)" proof- let ?k = "\c. {x::real^'n. 0 \ inner c x}" have "frontier (cball 0 1) \ (\ (?k ` s)) \ {}" @@ -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 \ {}" "t \ {}" "s \ t = {}" + assumes "convex s" "convex (t::(real^'n) set)" "s \ {}" "t \ {}" "s \ t = {}" shows "\a b. a \ 0 \ (\x\s. inner a x \ b) \ (\x\t. inner a x \ b)" proof- from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]] obtain a where "a\0" "\x\{x - y |x y. x \ t \ y \ s}. 0 \ 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 \ CARD('n) + 1" "\s\f. convex s" "\t\f. card t = CARD('n) + 1 \ \ t \ {}" shows "\ f \ {}" @@ -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 \ CARD('n) + 1" "\s\f. convex s" "\t\f. card t = CARD('n) + 1 \ \ t \ {}" shows "\ f \{}" @@ -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 \ s " + assumes "compact s" "cball (0::real^'n) 1 \ s " "\x\s. \u. 0 \ u \ u < 1 \ (u *\<^sub>R x) \ (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 \ s" apply(rule frontier_subset_closed) using compact_imp_closed[OF assms(1)] by simp def pi \ "\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 \ 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 \ 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 \ {}" "0 < e" - shows "s homeomorphic (cball (b::real^'n::finite) e)" + shows "s homeomorphic (cball (b::real^'n) e)" proof- obtain a where "a\interior s" using assms(3) by auto then obtain d where "d>0" and d:"cball a d \ 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 \ {}" "convex t" "compact t" "interior t \ {}" shows "s homeomorphic t" @@ -2243,7 +2243,7 @@ subsection {* Epigraphs of convex functions. *} -definition "epigraph s (f::real^'n::finite \ real) = {xy. fstcart xy \ s \ f(fstcart xy) \ dest_vec1 (sndcart xy)}" +definition "epigraph s (f::real^'n \ real) = {xy. fstcart xy \ s \ f(fstcart xy) \ dest_vec1 (sndcart xy)}" lemma mem_epigraph: "(pastecart x (vec1 y)) \ epigraph s f \ x \ s \ f x \ y" unfolding epigraph_def by auto @@ -2317,7 +2317,7 @@ shows "is_interval s \ connected s" using is_interval_convex convex_connected by auto -lemma convex_interval: "convex {a .. b}" "convex {a<.. real^'n::finite" +lemma ivt_increasing_component_on_1: fixes f::"real^1 \ real^'n" assumes "dest_vec1 a \ dest_vec1 b" "continuous_on {a .. b} f" "(f a)$k \ y" "y \ (f b)$k" shows "\x\{a..b}. (f x)$k = y" proof- have "f a \ f ` {a..b}" "f b \ 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 \ real^'n::finite" +lemma ivt_increasing_component_1: fixes f::"real^1 \ real^'n" assumes "dest_vec1 a \ dest_vec1 b" "\x\{a .. b}. continuous (at x) f" "f a$k \ y" "y \ f b$k" shows "\x\{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 \ real^'n::finite" +lemma ivt_decreasing_component_on_1: fixes f::"real^1 \ real^'n" assumes "dest_vec1 a \ dest_vec1 b" "continuous_on {a .. b} f" "(f b)$k \ y" "y \ (f a)$k" shows "\x\{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 \ real^'n::finite" +lemma ivt_decreasing_component_1: fixes f::"real^1 \ real^'n" assumes "dest_vec1 a \ dest_vec1 b" "\x\{a .. b}. continuous (at x) f" "f b$k \ y" "y \ f a$k" shows "\x\{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. \i. (x$i = 0) \ (x$i = 1)}" (is "?int = convex hull ?points") + "{0::real^'n .. 1} = convex hull {x. \i. (x$i = 0) \ (x$i = 1)}" (is "?int = convex hull ?points") proof- have 01:"{0,1} \ convex hull ?points" apply rule apply(rule_tac hull_subset[unfolded subset_eq, rule_format]) by auto { fix n x assume "x\{0::real^'n .. 1}" "n \ CARD('n)" "card {i. x$i \ 0} \ n" hence "x\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 \ ?y j \ ?y j \ 1" by auto } moreover have "i\{j. x$j \ 0} - {j. ((\ j. ?y j)::real^'n) $ j \ 0}" using i01 by(auto simp add: Cart_lambda_beta) - hence "{j. x$j \ 0} \ {j. ((\ j. ?y j)::real^'n::finite) $ j \ 0}" by auto - hence **:"{j. ((\ j. ?y j)::real^'n::finite) $ j \ 0} \ {j. x$j \ 0}" apply - apply rule by(auto simp add: Cart_lambda_beta) + hence "{j. x$j \ 0} \ {j. ((\ j. ?y j)::real^'n) $ j \ 0}" by auto + hence **:"{j. ((\ j. ?y j)::real^'n) $ j \ 0} \ {j. x$j \ 0}" apply - apply rule by(auto simp add: Cart_lambda_beta) have "card {j. ((\ j. ?y j)::real^'n) $ j \ 0} \ 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. \i. x$i=0 \ x$i=1}"]) - apply(rule finite_subset[of _ "(\s. (\ i. if i\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. \i. x$i=0 \ x$i=1}"]) + apply(rule finite_subset[of _ "(\s. (\ i. if i\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:"\i. x $ i = 0 \ x $ i = 1" show "x \ (\s. \ i. if i \ 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 - (\ i. d) .. x + (\ i. d)} = convex hull s" proof- + assumes "0 < d" obtains s::"(real^'n) set" where "finite s" "{x - (\ i. d) .. x + (\ i. d)} = convex hull s" proof- let ?d = "(\ i. d)::real^'n" have *:"{x - ?d .. x + ?d} = (\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 \ real ^ 'n \ real ^ 'n" where + midpoint :: "real ^ 'n \ real ^ 'n \ real ^ 'n" where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)" definition - open_segment :: "real ^ 'n::finite \ real ^ 'n \ (real ^ 'n) set" where + open_segment :: "real ^ 'n \ real ^ 'n \ (real ^ 'n) set" where "open_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 < u \ u < 1}" definition - closed_segment :: "real ^ 'n::finite \ real ^ 'n \ (real ^ 'n) set" where + closed_segment :: "real ^ 'n \ real ^ 'n \ (real ^ 'n) set" where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \ u \ u \ 1}" definition "between = (\ (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 *: "\x y::real^'n::finite. 2 *\<^sub>R x = - y \ norm x = (norm y) / 2" unfolding equation_minus_iff by auto - have **:"\x y::real^'n::finite. 2 *\<^sub>R x = y \ norm x = (norm y) / 2" by auto + have *: "\x y::real^'n. 2 *\<^sub>R x = - y \ norm x = (norm y) / 2" unfolding equation_minus_iff by auto + have **:"\x y::real^'n. 2 *\<^sub>R x = y \ 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 \ a = (b::real^'n::finite)" + "midpoint a b = a \ a = (b::real^'n)" "midpoint a b = b \ 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 \ x \ closed_segment a b" unfolding between_def mem_def by auto -lemma between:"between (a,b) (x::real^'n::finite) \ dist a b = (dist a x) + (dist x b)" +lemma between:"between (a,b) (x::real^'n) \ 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 *:"\x y z. x = (1/2::real) *\<^sub>R z \ y = (1/2) *\<^sub>R z \ norm z = norm x + norm y" by auto @@ -2776,7 +2776,7 @@ lemma std_simplex: "convex hull (insert 0 { basis i | i. i\UNIV}) = - {x::real^'n::finite . (\i. 0 \ x$i) \ setsum (\i. x$i) UNIV \ 1 }" (is "convex hull (insert 0 ?p) = ?s") + {x::real^'n . (\i. 0 \ x$i) \ setsum (\i. x$i) UNIV \ 1 }" (is "convex hull (insert 0 ?p) = ?s") proof- let ?D = "UNIV::'n set" have "0\?p" by(auto simp add: basis_nonzero) have "{(basis i)::real^'n |i. i \ ?D} = basis ` ?D" by auto @@ -2796,7 +2796,7 @@ lemma interior_std_simplex: "interior (convex hull (insert 0 { basis i| i. i\UNIV})) = - {x::real^'n::finite. (\i. 0 < x$i) \ setsum (\i. x$i) UNIV < 1 }" + {x::real^'n. (\i. 0 < x$i) \ setsum (\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 "0xa. dist x xa < e \ (\x. 0 \ xa $ x) \ setsum (op $ xa) UNIV \ 1" @@ -2813,7 +2813,7 @@ also have "\ \ 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:"\i. 0 < x $ i" "setsum (op $ x) UNIV < 1" + fix x::"real^'n" assume as:"\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 \ 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 \ interior(convex hull (insert 0 {basis i | i . i \ UNIV}))" proof- let ?D = "UNIV::'n set" let ?a = "setsum (\b::real^'n. inverse (2 * real CARD('n)) *\<^sub>R b) {(basis i) | i. i \ ?D}" have *:"{basis i :: real ^ 'n | i. i \ ?D} = basis ` ?D" by auto @@ -2849,7 +2849,7 @@ subsection {* Paths. *} -definition "path (g::real^1 \ real^'n::finite) \ continuous_on {0 .. 1} g" +definition "path (g::real^1 \ real^'n) \ continuous_on {0 .. 1} g" definition "pathstart (g::real^1 \ real^'n) = g 0" @@ -3138,7 +3138,7 @@ subsection {* Special case of straight-line paths. *} definition - linepath :: "real ^ 'n::finite \ real ^ 'n \ real ^ 1 \ real ^ 'n" where + linepath :: "real ^ 'n \ real ^ 'n \ real ^ 1 \ real ^ 'n" where "linepath a b = (\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 \ CARD('n::finite)" shows "path_connected((UNIV::(real^'n::finite) set) - {a})" proof- + assumes "2 \ CARD('n::finite)" shows "path_connected((UNIV::(real^'n) set) - {a})" proof- obtain \ where \:"bij_betw \ {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 = "\k. basis (\ 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 \ CARD('n::finite)" shows "path_connected {x::real^'n::finite. norm(x - a) = r}" proof(cases "r\0") +lemma path_connected_sphere: assumes "2 \ CARD('n::finite)" shows "path_connected {x::real^'n. norm(x - a) = r}" proof(cases "r\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 \ CARD('n) \ connected {x::real^'n::finite. norm(x - a) = r}" +lemma connected_sphere: "2 \ CARD('n) \ connected {x::real^'n. norm(x - a) = r}" using path_connected_sphere path_connected_imp_connected by auto - + end diff -r 1edf0f223c6e -r 4e896680897e src/HOL/Multivariate_Analysis/Derivative.thy --- 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 \ dest_vec1) has_derivative (f' \ 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 \ real^'b::finite" shows +lemma derivative_is_linear: fixes f::"real^'a \ real^'b" shows "(f has_derivative f') net \ 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 \ real^'b::finite" and v::"real^'c::finite" +lemma has_derivative_vmul_component: fixes c::"real^'a \ real^'b" and v::"real^'c" assumes "(c has_derivative c') net" shows "((\x. c(x)$k *\<^sub>R v) has_derivative (\x. (c' x)$k *\<^sub>R v)) net" proof- have *:"\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 *:"\x. x - vec 0 = (x::real^'n::finite)" by auto + have *:"\x. x - vec 0 = (x::real^'n)" by auto have **:"\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 "\ trivial_limit net" "0 < (e::real)" then have "eventually (\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 \ real" and v::"real^'a::finite" +lemma has_derivative_vmul_within: fixes c::"real \ real" and v::"real^'a" assumes "(c has_derivative c') (at x within s)" shows "((\x. (c x) *\<^sub>R v) has_derivative (\x. (c' x) *\<^sub>R v)) (at x within s)" proof- have *:"\c. (\x. (vec1 \ c \ dest_vec1) x $ 1 *\<^sub>R v) = (\x. (c x) *\<^sub>R v) \ dest_vec1" unfolding o_def by auto show ?thesis using has_derivative_vmul_component[of "vec1 \ c \ dest_vec1" "vec1 \ c' \ 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 \ real" and v::"real^'a::finite" +lemma has_derivative_vmul_at: fixes c::"real \ real" and v::"real^'a" assumes "(c has_derivative c') (at x)" shows "((\x. (c x) *\<^sub>R v) has_derivative (\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) \ (f differentiable (at a))" unfolding differentiable_def has_derivative_within_open[OF assms] by auto -lemma differentiable_at_imp_differentiable_on: "(\x\(s::(real^'n::finite) set). f differentiable at x) \ f differentiable_on s" +lemma differentiable_at_imp_differentiable_on: "(\x\(s::(real^'n) set). f differentiable at x) \ f differentiable_on s" unfolding differentiable_on_def by(auto intro!: differentiable_at_withinI) lemma differentiable_on_eq_differentiable_at: "open s \ (f differentiable_on s \ (\x\s. f differentiable at x))" @@ -305,13 +305,13 @@ "f differentiable net \ (f has_derivative (frechet_derivative f net)) net" unfolding frechet_derivative_def differentiable_def and some_eq_ex[of "\ f' . (f has_derivative f') net"] .. -lemma linear_frechet_derivative: fixes f::"real^'a::finite \ real^'b::finite" +lemma linear_frechet_derivative: fixes f::"real^'a \ real^'b" shows "f differentiable net \ 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) \ (real^'b::finite)) differentiable net \ (f has_derivative (\h. (jacobian f net) *v h)) net" +lemma jacobian_works: "(f::(real^'a) \ (real^'b)) differentiable net \ (f has_derivative (\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)) \ bounded_linear f' \ + "(f has_derivative f') (at (x::real^'n)) \ bounded_linear f' \ (\e>0. \d>0. \y. norm(y - x) < d \ norm(f y - f x - f'(y - x)) \ 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="\z. f' z - f'a z" in exI) apply(rule has_derivative_sub) by auto -lemma differentiable_setsum: fixes f::"'a \ (real^'n::finite \real^'n)" +lemma differentiable_setsum: fixes f::"'a \ (real^'n \real^'n)" assumes "finite s" "\a\s. (f a) differentiable net" shows "(\x. setsum (\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::"_ \ (real^'n::finite \real^'n)" +lemma differentiable_setsum_numseg: fixes f::"_ \ (real^'n \real^'n)" shows "\i. m \ i \ i \ n \ (f i) differentiable net \ (\x. setsum (\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 \ real^'b::finite" +lemma frechet_derivative_unique_within: fixes f::"real^'a \ real^'b" assumes "(f has_derivative f') (at x within s)" "(f has_derivative f'') (at x within s)" "(\i::'a::finite. \e>0. \d. 0 < abs(d) \ abs(d) < e \ (x + d *\<^sub>R basis i) \ 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 \ real^'b::finite" +lemma frechet_derivative_unique_at: fixes f::"real^'a \ real^'b" shows "(f has_derivative f') (at x) \ (f has_derivative f'') (at x) \ 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 \ real^'b::finite" +lemma frechet_derivative_unique_within_closed_interval: fixes f::"real^'a \ real^'b" assumes "\i. a$i < b$i" "x \ {a..b}" (is "x\?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 \ real^'b::finite" +lemma frechet_derivative_unique_within_open_interval: fixes f::"real^'a \ real^'b" assumes "x \ {a<..0` and assms(1) unfolding mem_interval by(auto simp add:field_simps) qed -lemma frechet_derivative_at: fixes f::"real^'a::finite \ real^'b::finite" +lemma frechet_derivative_at: fixes f::"real^'a \ real^'b" shows "(f has_derivative f') (at x) \ (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 \ real^'b::finite" +lemma frechet_derivative_within_closed_interval: fixes f::"real^'a \ real^'b" assumes "\i. a$i < b$i" "x \ {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 \ real^'b::finite" +lemma differential_zero_maxmin_component: fixes f::"real^'a \ real^'b" assumes "0 < e" "((\y \ ball x e. (f y)$k \ (f x)$k) \ (\y\ball x e. (f x)$k \ (f y)$k))" "f differentiable (at x)" shows "jacobian f (at x) $ k = 0" proof(rule ccontr) def D \ "jacobian f (at x)" assume "jacobian f (at x) $ k \ 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 \ real" +lemma differential_zero_maxmin: fixes f::"real^'a \ real" assumes "x \ s" "open s" "(f has_derivative f') (at x)" "(\y\s. f y \ f x) \ (\y\s. f x \ f y)" shows "f' = (\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 \ b = inner a b" unfolding inner_vector_def dot_def by auto -lemma mvt_general: fixes f::"real\real^'n::finite" +lemma mvt_general: fixes f::"real\real^'n" assumes "ax\{a<..x\{a<.. norm(f'(x) (b - a))" proof- have "\x\{a<.. (f b - f a) \ f) b - (op \ (f b - f a) \ f) a = (f b - f a) \ f' x (b - a)" @@ -708,7 +708,7 @@ subsection {* Still more general bound theorem. *} -lemma differentiable_bound: fixes f::"real^'a::finite \ real^'b::finite" +lemma differentiable_bound: fixes f::"real^'a \ real^'b" assumes "convex s" "\x\s. (f has_derivative f'(x)) (at x within s)" "\x\s. onorm(f' x) \ B" and x:"x\s" and y:"y\s" shows "norm(f x - f y) \ B * norm(x - y)" proof- let ?p = "\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 \ real^'c::finite" +lemma has_derivative_inverse_basic: fixes f::"real^'b \ real^'c" assumes "(f has_derivative f') (at (g y))" "bounded_linear g'" "g' \ f' = id" "continuous (at y) g" "open t" "y \ t" "\z\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 \ real^'c::finite" +lemma has_derivative_inverse_basic_x: fixes f::"real^'b \ 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 \ t" "\y\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 \ real^'b::finite" +lemma has_derivative_inverse_dieudonne: fixes f::"real^'a \ real^'b" assumes "open s" "open (f ` s)" "continuous_on s f" "continuous_on (f ` s) g" "\x\s. g(f x) = x" (**) "x\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 \ real^'b::finite" +lemma has_derivative_inverse: fixes f::"real^'a \ real^'b" assumes "compact s" "x \ s" "f x \ interior(f ` s)" "continuous_on s f" "\y\s. g(f y) = y" "(f has_derivative f') (at x)" "bounded_linear g'" "g' \ 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 \ real^'n" +lemma brouwer_surjective: fixes f::"real^'n \ real^'n" assumes "compact t" "convex t" "t \ {}" "continuous_on t f" "\x\s. \y\t. x + (y - f y) \ t" "x\s" shows "\y\t. f y = x" proof- @@ -853,7 +853,7 @@ show ?thesis unfolding * apply(rule brouwer[OF assms(1-3), of "\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 \ real^'n" +lemma brouwer_surjective_cball: fixes f::"real^'n \ real^'n" assumes "0 < e" "continuous_on (cball a e) f" "\x\s. \y\cball a e. x + (y - f y) \ cball a e" "x\s" shows "\y\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 \ real^'b::finite" +lemma sussmann_open_mapping: fixes f::"real^'a \ real^'b" assumes "open s" "continuous_on s f" "x \ s" "(f has_derivative f') (at x)" "bounded_linear g'" "f' \ g' = id" (**) "t \ s" "x \ 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 \ real^'n" +lemma has_derivative_inverse_strong: fixes f::"real^'n \ real^'n" assumes "open s" "x \ s" "continuous_on s f" "\x\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 \ real^'n" +lemma has_derivative_inverse_strong_x: fixes f::"real^'n \ real^'n" assumes "open s" "g y \ s" "continuous_on s f" "\x\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 \ real^'n" +lemma has_derivative_inverse_on: fixes f::"real^'n \ real^'n" assumes "open s" "\x\s. (f has_derivative f'(x)) (at x)" "\x\s. g(f x) = x" "f'(x) o g'(x) = id" "x\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 \ bounded_linear g ==> bounded_linear (\x. f x - g x)" using bounded_linear_add[of f "\x. - g x"] bounded_linear_minus[of g] by(auto simp add:group_simps) -lemma has_derivative_locally_injective: fixes f::"real^'n::finite \ real^'m::finite" +lemma has_derivative_locally_injective: fixes f::"real^'n \ real^'m" assumes "a \ s" "open s" "bounded_linear g'" "g' o f'(a) = id" "\x\s. (f has_derivative f'(x)) (at x)" "\e>0. \d>0. \x. dist a x < d \ onorm(\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 \ real^'m::finite \ real^'n::finite" +lemma has_derivative_sequence_lipschitz_lemma: fixes f::"nat \ real^'m \ real^'n" assumes "convex s" "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" "\n\N. \x\s. \h. norm(f' n x h - g' x h) \ e * norm(h)" shows "\m\N. \n\N. \x\s. \y\s. norm((f m x - f n x) - (f m y - f n y)) \ 2 * e * norm(x - y)" proof(default)+ @@ -1033,7 +1033,7 @@ thus "onorm (\h. f' m x h - f' n x h) \ 2 * e" apply-apply(rule onorm(2)) apply(rule linear_compose_sub) unfolding linear_conv_bounded_linear using assms(2)[rule_format,OF `x\s`, THEN derivative_linear] by auto qed qed -lemma has_derivative_sequence_lipschitz: fixes f::"nat \ real^'m::finite \ real^'n::finite" +lemma has_derivative_sequence_lipschitz: fixes f::"nat \ real^'m \ real^'n" assumes "convex s" "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" "\e>0. \N. \n\N. \x\s. \h. norm(f' n x h - g' x h) \ e * norm(h)" "0 < e" shows "\e>0. \N. \m\N. \n\N. \x\s. \y\s. norm((f m x - f n x) - (f m y - f n y)) \ 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\real^'m::finite\real^'n::finite" +lemma has_derivative_sequence: fixes f::"nat\real^'m\real^'n" assumes "convex s" "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" "\e>0. \N. \n\N. \x\s. \h. norm(f' n x h - g' x h) \ e * norm(h)" "x0 \ s" "((\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\ real^'m::finite \ real^'n::finite" +lemma has_antiderivative_sequence: fixes f::"nat\ real^'m \ real^'n" assumes "convex s" "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" "\e>0. \N. \n\N. \x\s. \h. norm(f' n x h - g' x h) \ e * norm h" shows "\g. \x\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\s`) by(auto intro!: Lim_const) qed auto -lemma has_antiderivative_limit: fixes g'::"real^'m::finite \ real^'m::finite \ real^'n::finite" +lemma has_antiderivative_limit: fixes g'::"real^'m \ real^'m \ real^'n" assumes "convex s" "\e>0. \f f'. \x\s. (f has_derivative (f' x)) (at x within s) \ (\h. norm(f' x h - g' x h) \ e * norm(h))" shows "\g. \x\s. (g has_derivative g'(x)) (at x within s)" proof- have *:"\n. \f f'. \x\s. (f has_derivative (f' x)) (at x within s) \ (\h. norm(f' x h - g' x h) \ inverse (real (Suc n)) * norm(h))" @@ -1143,7 +1143,7 @@ definition sums_seq :: "(nat \ 'a::real_normed_vector) \ 'a \ (nat set) \ bool" (infixl "sums'_seq" 12) where "(f sums_seq l) s \ ((\n. setsum f (s \ {0..n})) ---> l) sequentially" -lemma has_derivative_series: fixes f::"nat \ real^'m::finite \ real^'n::finite" +lemma has_derivative_series: fixes f::"nat \ real^'m \ real^'n" assumes "convex s" "\n. \x\s. ((f n) has_derivative (f' n x)) (at x within s)" "\e>0. \N. \n\N. \x\s. \h. norm(setsum (\i. f' i x h) (k \ {0..n}) - g' x h) \ e * norm(h)" "x\s" "((\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 \ real^'n::finite \ real^'p::finite" and f::"real^'q::finite \ real^'m" +lemma has_derivative_bilinear_within: fixes h::"real^'m \ real^'n \ real^'p" and f::"real^'q \ real^'m" assumes "(f has_derivative f') (at x within s)" "(g has_derivative g') (at x within s)" "bounded_bilinear h" shows "((\x. h (f x) (g x)) has_derivative (\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 \ real^'n::finite \ real^'p::finite" and f::"real^'p::finite \ real^'m" +lemma has_derivative_bilinear_at: fixes h::"real^'m \ real^'n \ real^'p" and f::"real^'p \ real^'m" assumes "(f has_derivative f') (at x)" "(g has_derivative g') (at x)" "bounded_bilinear h" shows "((\x. h (f x) (g x)) has_derivative (\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\real^'n::finite" +lemma vector_derivative_unique_at: fixes f::"real\real^'n" assumes "(f has_vector_derivative f') (at x)" "(f has_vector_derivative f'') (at x)" shows "f' = f''" proof- have *:"(\x. x *\<^sub>R f') \ dest_vec1 = (\x. x *\<^sub>R f'') \ 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 "((\x. x *\<^sub>R f') \ dest_vec1) (vec1 1) = ((\x. x *\<^sub>R f'') \ 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 \ real^'n::finite" +lemma vector_derivative_unique_within_closed_interval: fixes f::"real \ real^'n" assumes "a < b" "x \ {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 "((\x. x *\<^sub>R f') \ dest_vec1) (vec1 1) = ((\x. x *\<^sub>R f'') \ 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 \ real^'a::finite" shows +lemma vector_derivative_at: fixes f::"real \ real^'a" shows "(f has_vector_derivative f') (at x) \ 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 \ real^'a::finite" +lemma vector_derivative_within_closed_interval: fixes f::"real \ real^'a" assumes "a < b" "x \ {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 \ real^'a::finite" shows +lemma has_vector_derivative_within_subset: fixes f::"real \ real^'a" shows "(f has_vector_derivative f') (at x within s) \ t \ s \ (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 "((\x. c) has_vector_derivative 0) net" unfolding has_vector_derivative_def using has_derivative_const by auto lemma has_vector_derivative_id: "((\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 \ real^'a::finite" +lemma has_vector_derivative_cmul: fixes f::"real \ real^'a" shows "(f has_vector_derivative f') net \ ((\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 \ real^'a::finite" assumes "c \ 0" +lemma has_vector_derivative_cmul_eq: fixes f::"real \ real^'a" assumes "c \ 0" shows "(((\x. c *\<^sub>R f x) has_vector_derivative (c *\<^sub>R f')) net \ (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 \ real^'n::finite \ real^'p::finite" +lemma has_vector_derivative_bilinear_within: fixes h::"real^'m \ real^'n \ 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 "((\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="\x. h (f x) (g x)" and f'="\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 \ real^'n::finite \ real^'p::finite" +lemma has_vector_derivative_bilinear_at: fixes h::"real^'m \ real^'n \ real^'p" assumes "(f has_vector_derivative f') (at x)" "(g has_vector_derivative g') (at x)" "bounded_bilinear h" shows "((\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 - diff -r 1edf0f223c6e -r 4e896680897e src/HOL/Multivariate_Analysis/Determinants.thy --- 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 \ 'a" where +definition trace :: "'a::semiring_1^'n^'n \ 'a" where "trace A = setsum (\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 \ 'a" where +definition det:: "'a::comm_ring_1^'n^'n \ 'a" where "det A = setsum (\p. of_int (sign p) * setprod (\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 = "\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: "\i j. i < j \ A$i$j = 0" shows "det A = setprod (\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: "\i j. i > j \ A$i$j = 0" shows "det A = setprod (\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: "\i j. i \ j \ A$i$j = 0" shows "det A = setprod (\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(\ 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(\ 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 \ 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 \ 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 \ j" shows "det (\ 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 \ span {row j A |j. j \ i}" shows "det (\ 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: "(\x. f x = g x) \ (Cart_lambda f::'a^'n) = (Cart_lambda g :: 'a^'n::finite)" +lemma Cart_lambda_cong: "(\x. f x = g x) \ (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 ((\ i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n::finite) = setsum (\j. det ((\ i. if i = k then a i j else c i)::'a^'n^'n)) S" + shows "det ((\ i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n) = setsum (\j. det ((\ 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((\ i. if i \ T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n::finite) = + shows "det((\ i. if i \ T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n) = setsum (\f. det((\ i. if i \ T then a i (f i) else c i)::'a^'n^'n)) {f. (\i \ T. f i \ S) \ (\i. i \ T \ f i = i)}" using fT @@ -580,7 +580,7 @@ lemma det_linear_rows_setsum: assumes fS: "finite (S::'n::finite set)" - shows "det (\ i. setsum (a i) S) = setsum (\f. det (\ i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n::finite)) {f. \i. f i \ S}" + shows "det (\ i. setsum (a i) S) = setsum (\f. det (\ i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. \i. f i \ S}" proof- have th0: "\x y. ((\ i. if i \ (UNIV:: 'n set) then x i else y i) :: 'a^'n^'n) = (\ 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 = (\ i. setsum (\k. A$i$k *s B $ k) (UNIV :: 'n set))" by (vector matrix_matrix_mult_def setsum_component) lemma det_rows_mul: - "det((\ i. c i *s a i)::'a::comm_ring_1^'n^'n::finite) = + "det((\ i. c i *s a i)::'a::comm_ring_1^'n^'n) = setprod (\i. c i) (UNIV:: 'n set) * det((\ 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 \ (\(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 \ (\(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 \ det A \ 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 ((\ i. if i = k then setsum (\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((\ 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 \ 0" shows "A *v x = b \ x = (\ k. det(\ 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) \ transp Q ** Q = mat 1 \ Q ** transp Q = mat 1" +definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \ transp Q ** Q = mat 1 \ Q ** transp Q = mat 1" -lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n::finite) \ transp Q ** Q = mat 1" +lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \ 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 \ real^'n::finite" + fixes f:: "real^'n \ real^'n" shows "orthogonal_transformation f \ linear f \ orthogonal_matrix(matrix f)" (is "?lhs \ ?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 \ det Q = - 1" proof- @@ -918,7 +918,7 @@ (* Linearity of scaling, and hence isometry, that preserves origin. *) (* ------------------------------------------------------------------------- *) lemma scaling_linear: - fixes f :: "real ^'n \ real ^'n::finite" + fixes f :: "real ^'n \ real ^'n" assumes f0: "f 0 = 0" and fd: "\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) \ \x y. dist(f x) (f y) = dist x y + "f (0:: real^'n) = (0:: real^'n) \ \x y. dist(f x) (f y) = dist x y \ linear f" by (rule scaling_linear[where c=1]) simp_all @@ -943,7 +943,7 @@ (* ------------------------------------------------------------------------- *) lemma orthogonal_transformation_isometry: - "orthogonal_transformation f \ f(0::real^'n) = (0::real^'n::finite) \ (\x y. dist(f x) (f y) = dist x y)" + "orthogonal_transformation f \ f(0::real^'n) = (0::real^'n) \ (\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 \ real ^'n::finite" + fixes f:: "real ^'n \ real ^'n" assumes f1: "\x. norm x = 1 \ norm (f x) = 1" and fd1: "\ x y. norm x = 1 \ norm y = 1 \ dist (f x) (f y) = dist x y" shows "\g. orthogonal_transformation g \ (\x. norm x = 1 \ g x = f x)" @@ -1034,7 +1034,7 @@ definition "rotoinversion_matrix Q \ orthogonal_matrix Q \ 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 \ rotation_matrix Q \ rotoinversion_matrix Q" by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix) (* ------------------------------------------------------------------------- *) diff -r 1edf0f223c6e -r 4e896680897e src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- 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 + \ (\ x y. (\ i. (x$i) + (y$i)))" instance .. end -instantiation "^" :: (times,finite) times +instantiation cart :: (times,finite) times begin definition vector_mult_def : "op * \ (\ x y. (\ i. (x$i) * (y$i)))" instance .. end -instantiation "^" :: (minus,finite) minus begin +instantiation cart :: (minus,finite) minus begin definition vector_minus_def : "op - \ (\ x y. (\ i. (x$i) - (y$i)))" instance .. end -instantiation "^" :: (uminus,finite) uminus begin +instantiation cart :: (uminus,finite) uminus begin definition vector_uminus_def : "uminus \ (\ x. (\ i. - (x$i)))" instance .. end -instantiation "^" :: (zero,finite) zero begin + +instantiation cart :: (zero,finite) zero begin definition vector_zero_def : "0 \ (\ i. 0)" instance .. end -instantiation "^" :: (one,finite) one begin +instantiation cart :: (one,finite) one begin definition vector_one_def : "1 \ (\ 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 = (\ r x. (\ i. scaleR r (x$i)))" instance .. @@ -109,7 +110,7 @@ text{* Also the scalar-vector multiplication. *} -definition vector_scalar_mult:: "'a::times \ 'a ^'n::finite \ 'a ^ 'n" (infixl "*s" 70) +definition vector_scalar_mult:: "'a::times \ 'a ^ 'n \ 'a ^ 'n" (infixl "*s" 70) where "c *s x = (\ i. c * (x$i))" text{* Constant Vectors *} @@ -118,7 +119,7 @@ text{* Dot products. *} -definition dot :: "'a::{comm_monoid_add, times} ^ 'n::finite \ 'a ^ 'n \ 'a" (infix "\" 70) where +definition dot :: "'a::{comm_monoid_add, times} ^ 'n \ 'a ^ 'n \ 'a" (infix "\" 70) where "x \ y = setsum (\i. x$i * y$i) UNIV" lemma dot_1[simp]: "(x::'a::{comm_monoid_add, times}^1) \ 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) \ nat \ '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 \ 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 \ 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 \ 'a::metric_space ^ 'n::finite" + fixes X :: "nat \ 'a::metric_space ^ 'n" assumes X: "\i. (\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 \ 'a::metric_space ^ 'n::finite" + fixes X :: "nat \ 'a::metric_space ^ 'n" assumes X: "\i. Cauchy (\n. X n $ i)" shows "Cauchy (\n. X n)" proof (rule metric_CauchyI) @@ -733,7 +723,7 @@ then show "\M. \m\M. \n\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 \ 'a ^ 'b" assume "Cauchy X" have "\i. (\n. X n $ i) ----> lim (\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) \ y = y \ x" +lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \ y = y \ x" by (vector mult_commute) -lemma dot_ladd: "((x::'a::ring ^ 'n::finite) + y) \ z = (x \ z) + (y \ z)" +lemma dot_ladd: "((x::'a::ring ^ 'n) + y) \ z = (x \ z) + (y \ z)" by (vector ring_simps) -lemma dot_radd: "x \ (y + (z::'a::ring ^ 'n::finite)) = (x \ y) + (x \ z)" +lemma dot_radd: "x \ (y + (z::'a::ring ^ 'n)) = (x \ y) + (x \ z)" by (vector ring_simps) -lemma dot_lsub: "((x::'a::ring ^ 'n::finite) - y) \ z = (x \ z) - (y \ z)" +lemma dot_lsub: "((x::'a::ring ^ 'n) - y) \ z = (x \ z) - (y \ z)" by (vector ring_simps) -lemma dot_rsub: "(x::'a::ring ^ 'n::finite) \ (y - z) = (x \ y) - (x \ z)" +lemma dot_rsub: "(x::'a::ring ^ 'n) \ (y - z) = (x \ y) - (x \ z)" by (vector ring_simps) lemma dot_lmult: "(c *s x) \ y = (c::'a::ring) * (x \ y)" by (vector ring_simps) lemma dot_rmult: "x \ (c *s y) = (c::'a::comm_ring) * (x \ y)" by (vector ring_simps) -lemma dot_lneg: "(-x) \ (y::'a::ring ^ 'n::finite) = -(x \ y)" by vector -lemma dot_rneg: "(x::'a::ring ^ 'n::finite) \ (-y) = -(x \ y)" by vector +lemma dot_lneg: "(-x) \ (y::'a::ring ^ 'n) = -(x \ y)" by vector +lemma dot_rneg: "(x::'a::ring ^ 'n) \ (-y) = -(x \ y)" by vector lemma dot_lzero[simp]: "0 \ x = (0::'a::{comm_monoid_add, mult_zero})" by vector lemma dot_rzero[simp]: "x \ 0 = (0::'a::{comm_monoid_add, mult_zero})" by vector lemma dot_pos_le[simp]: "(0::'a\ordered_ring_strict) <= x \ x" @@ -860,10 +850,10 @@ show ?case by (simp add: h) qed -lemma dot_eq_0: "x \ x = 0 \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n::finite) = 0" +lemma dot_eq_0: "x \ x = 0 \ (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 \ x) \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n::finite) \ 0" using dot_eq_0[of x] dot_pos_le[of x] +lemma dot_pos_lt[simp]: "(0 < x \ x) \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \ 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 \ 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) \ a = (0::'a::idom) \ x = 0" by vector lemma vector_mul_lcancel[simp]: "a *s x = a *s y \ a = (0::real) \ x = y" @@ -1017,7 +1007,7 @@ lemma vector_mul_rcancel_imp: "x \ 0 \ (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 \ 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 "\x \ y\ \ 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 \ 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: "\x$i\ <= norm (x::real ^ 'n::finite)" +lemma component_le_norm: "\x$i\ <= 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 - ==> \x$i\ <= e" +lemma norm_bound_component_le: "norm x <= e ==> \x$i\ <= e" by (metis component_le_norm order_trans) -lemma norm_bound_component_lt: "norm(x::real ^ 'n::finite) < e - ==> \x$i\ < e" +lemma norm_bound_component_lt: "norm x < e ==> \x$i\ < e" by (metis component_le_norm basic_trans_rules(21)) -lemma norm_le_l1: "norm (x:: real ^'n::finite) <= setsum(\i. \x$i\) UNIV" +lemma norm_le_l1: "norm x <= setsum(\i. \x$i\) UNIV" by (simp add: norm_vector_def setL2_le_setsum) -lemma real_abs_norm: "\norm x\ = norm (x :: real ^ _)" +lemma real_abs_norm: "\norm x\ = norm x" by (rule abs_norm_cancel) -lemma real_abs_sub_norm: "\norm(x::real ^'n::finite) - norm y\ <= norm(x - y)" +lemma real_abs_sub_norm: "\norm (x::real ^ 'n) - norm y\ <= norm(x - y)" by (rule norm_triangle_ineq3) -lemma norm_le: "norm(x::real ^ _) <= norm(y) \ x \ x <= y \ y" +lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \ x \ x <= y \ y" by (simp add: real_vector_norm_def) -lemma norm_lt: "norm(x::real ^ _) < norm(y) \ x \ x < y \ y" +lemma norm_lt: "norm(x::real ^ 'n) < norm(y) \ x \ x < y \ y" by (simp add: real_vector_norm_def) -lemma norm_eq: "norm (x::real ^ _) = norm y \ x \ x = y \ y" +lemma norm_eq: "norm(x::real ^ 'n) = norm y \ x \ x = y \ y" by (simp add: order_eq_iff norm_le) -lemma norm_eq_1: "norm(x::real ^ _) = 1 \ x \ x = 1" +lemma norm_eq_1: "norm(x::real ^ 'n) = 1 \ x \ 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 \"} products. *} -lemma vector_eq: "(x:: real ^ 'n::finite) = y \ x \ x = x \ y\ y \ y = x \ x" (is "?lhs \ ?rhs") +lemma vector_eq: "(x:: real ^ 'n) = y \ x \ x = x \ y\ y \ y = x \ x" (is "?lhs \ ?rhs") proof assume "?lhs" then show ?rhs by simp next @@ -1299,7 +1287,7 @@ by norm lemma setsum_component [simp]: - fixes f:: " 'a \ ('b::comm_monoid_add) ^'n::finite" + fixes f:: " 'a \ ('b::comm_monoid_add) ^'n" shows "(setsum f S)$i = setsum (\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 \ ('a::semiring_1)^'n::finite" + fixes f:: "'c \ ('a::semiring_1)^'n" shows "setsum (\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 \ real ^'n::finite" + fixes f :: "'a \ real ^'n" assumes fS: "finite S" shows "norm (setsum f S) <= setsum (\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 \ real ^ 'n::finite" + fixes f :: "'a \ real ^ 'n" assumes fS: "finite S" and fg: "\x \ S. norm (f x) \ g x" shows "norm (setsum f S) \ setsum g S" @@ -1378,7 +1366,7 @@ by simp lemma real_setsum_norm_bound: - fixes f :: "'a \ real ^ 'n::finite" + fixes f :: "'a \ real ^ 'n" assumes fS: "finite S" and K: "\x \ S. norm (f x) \ K" shows "norm (setsum f S) \ of_nat (card S) * K" @@ -1414,7 +1402,7 @@ by (auto intro: setsum_0') lemma vsum_norm_allsubsets_bound: - fixes f:: "'a \ real ^'n::finite" + fixes f:: "'a \ real ^'n" assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (setsum f Q) \ e" shows "setsum (\x. norm (f x)) P \ 2 * real CARD('n) * e" proof- @@ -1452,10 +1440,10 @@ finally show ?thesis . qed -lemma dot_lsum: "finite S \ setsum f S \ (y::'a::{comm_ring}^'n::finite) = setsum (\x. f x \ y) S " +lemma dot_lsum: "finite S \ setsum f S \ (y::'a::{comm_ring}^'n) = setsum (\x. f x \ y) S " by (induct rule: finite_induct, auto simp add: dot_lzero dot_ladd dot_radd) -lemma dot_rsum: "finite S \ (y::'a::{comm_ring}^'n::finite) \ setsum f S = setsum (\x. y \ f x) S " +lemma dot_rsum: "finite S \ (y::'a::{comm_ring}^'n) \ setsum f S = setsum (\x. y \ 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" "\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 ==> \(x::real^'n::finite). norm x = c" +lemma vector_choose_size: "0 <= c ==> \(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 "\(y::real^'n::finite). dist x y = e" + shows "\(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 \ real ^'n::finite)" +lemma basis_inj: "inj (basis :: 'n \ 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 (\i. (x$i) *s basis i) UNIV = (x::('a::ring_1) ^'n::finite)" (is "?lhs = ?rhs" is "setsum ?f ?S = _") + "setsum (\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 (\i. f i *s basis i) UNIV = (x::('a::comm_ring_1) ^'n::finite) \ (\i. f i = x$i)" + "setsum (\i. f i *s basis i) UNIV = (x::('a::comm_ring_1) ^'n) \ (\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 \ x = x$i" "x \ (basis i :: 'a^'n::finite) = (x$i :: 'a::semiring_1)" + shows "basis i \ x = x$i" "x \ (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) \ False" +lemma basis_eq_0: "basis i = (0::'a::semiring_1^'n) \ False" by (auto simp add: Cart_eq) lemma basis_nonzero: - shows "basis k \ (0:: 'a::semiring_1 ^'n::finite)" + shows "basis k \ (0:: 'a::semiring_1 ^'n)" by (simp add: basis_eq_0) -lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = (z::'a::semiring_1^'n::finite)" +lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ 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: "(\z. x \ z = y \ z) \ x = (y::'a::semiring_1^'n::finite)" +lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ 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 \ (x \ y = 0)" lemma orthogonal_basis: - shows "orthogonal (basis i :: 'a^'n::finite) x \ x$i = (0::'a::ring_1)" + shows "orthogonal (basis i :: 'a^'n) x \ 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) \ i \ j" + shows "orthogonal (basis i :: 'a::ring_1^'n) (basis j) \ i \ 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 \ 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 \ orthogonal y x" +lemma orthogonal_commute: "orthogonal (x::'a::{ab_semigroup_mult,comm_monoid_add} ^'n)y \ 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 (\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 \ 'a::comm_ring ^'m::finite) ==> linear (\x. -(f(x)))" by (vector linear_def Cart_eq) - -lemma linear_compose_add: "linear (f :: 'a ^'n::finite \ 'a::semiring_1 ^'m::finite) \ linear g ==> linear (\x. f(x) + g(x))" +lemma linear_compose_neg: "linear (f :: 'a ^'n \ 'a::comm_ring ^'m) ==> linear (\x. -(f(x)))" by (vector linear_def Cart_eq) + +lemma linear_compose_add: "linear (f :: 'a ^'n \ 'a::semiring_1 ^'m) \ linear g ==> linear (\x. f(x) + g(x))" by (vector linear_def Cart_eq ring_simps) -lemma linear_compose_sub: "linear (f :: 'a ^'n::finite \ 'a::ring_1 ^'m::finite) \ linear g ==> linear (\x. f x - g x)" +lemma linear_compose_sub: "linear (f :: 'a ^'n \ 'a::ring_1 ^'m) \ linear g ==> linear (\x. f x - g x)" by (vector linear_def Cart_eq ring_simps) lemma linear_compose: "linear f \ 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 (\x. 0::'a::semiring_1 ^ 'n::finite)" by (simp add: linear_def) +lemma linear_zero: "linear (\x. 0::'a::semiring_1 ^ 'n)" by (simp add: linear_def) lemma linear_compose_setsum: - assumes fS: "finite S" and lS: "\a \ S. linear (f a :: 'a::semiring_1 ^ 'n::finite \ 'a ^ 'm::finite)" - shows "linear(\x. setsum (\a. f a x :: 'a::semiring_1 ^'m::finite) S)" + assumes fS: "finite S" and lS: "\a \ S. linear (f a :: 'a::semiring_1 ^ 'n \ 'a ^'m)" + shows "linear(\x. setsum (\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 \ 'a^'n::finite" + fixes f:: "'a::semiring_1^'m \ 'a^'n" assumes lf: "linear f" shows "linear (\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 \ _) ==> f (-x) = - f x" +lemma linear_neg: "linear (f :: 'a::ring_1 ^'n \ _) ==> 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 \ _) ==> f(x - y) = f x - f y" +lemma linear_sub: "linear (f::'a::ring_1 ^'n \ _) ==> 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 \ _" + fixes f:: "'a::semiring_1^'n \ _" 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 \ 'a::semiring_1^'m::finite" + fixes f:: "'a ^'n \ 'a::semiring_1^'m" assumes lf: "linear f" and fS: "finite S" shows "f (setsum (\i. c i *s v i) S) = setsum (\i. c i *s f (v i)) S" using linear_setsum[OF lf fS, of "\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 \ _)" + assumes lf: "linear (f:: 'a::ring_1 ^ 'n \ _)" shows "inj f \ (\x. f x = 0 \ x = 0)" proof- have "inj f \ (\ x y. f x = f y \ x = y)" by (simp add: inj_on_def) @@ -1731,7 +1719,7 @@ qed lemma linear_bounded: - fixes f:: "real ^'m::finite \ real ^'n::finite" + fixes f:: "real ^'m \ real ^'n" assumes lf: "linear f" shows "\B. \x. norm (f x) \ B * norm x" proof- @@ -1760,7 +1748,7 @@ qed lemma linear_bounded_pos: - fixes f:: "real ^'n::finite \ real ^ 'm::finite" + fixes f:: "real ^'n \ real ^'m" assumes lf: "linear f" shows "\B > 0. \x. norm (f x) \ B * norm x" proof- @@ -1815,7 +1803,7 @@ by (simp add: f.add f.scaleR) qed -lemma bounded_linearI': fixes f::"real^'n::finite \ real^'m::finite" +lemma bounded_linearI': fixes f::"real^'n \ real^'m" assumes "\x y. f (x + y) = f x + f y" "\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 \ y = 0" using add_imp_eq[of x y 0] by auto lemma bilinear_lzero: - fixes h :: "'a::ring^'n::finite \ _" assumes bh: "bilinear h" shows "h 0 x = 0" + fixes h :: "'a::ring^'n \ _" 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 \ real^'n::finite \ real ^ 'k::finite" + fixes h:: "real ^'m \ real^'n \ real ^'k" assumes bh: "bilinear h" shows "\B. \x y. norm (h x y) \ B * norm x * norm y" proof- @@ -1903,7 +1891,7 @@ qed lemma bilinear_bounded_pos: - fixes h:: "real ^'m::finite \ real^'n::finite \ real ^ 'k::finite" + fixes h:: "real ^'m \ real^'n \ real ^'k" assumes bh: "bilinear h" shows "\B > 0. \x y. norm (h x y) \ B * norm x * norm y" proof- @@ -1965,7 +1953,7 @@ lemma choice_iff: "(\x. \y. P x y) \ (\f. \x. P x (f x))" by metis lemma adjoint_works_lemma: - fixes f:: "'a::ring_1 ^'n::finite \ 'a ^ 'm::finite" + fixes f:: "'a::ring_1 ^'n \ 'a ^'m" assumes lf: "linear f" shows "\x y. f x \ y = x \ adjoint f y" proof- @@ -1993,34 +1981,34 @@ qed lemma adjoint_works: - fixes f:: "'a::ring_1 ^'n::finite \ 'a ^ 'm::finite" + fixes f:: "'a::ring_1 ^'n \ 'a ^'m" assumes lf: "linear f" shows "x \ adjoint f y = f x \ y" using adjoint_works_lemma[OF lf] by metis lemma adjoint_linear: - fixes f :: "'a::comm_ring_1 ^'n::finite \ 'a ^ 'm::finite" + fixes f :: "'a::comm_ring_1 ^'n \ '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 \ 'a ^ 'm::finite" + fixes f:: "'a::comm_ring_1 ^'n \ 'a ^'m" assumes lf: "linear f" shows "x \ adjoint f y = f x \ y" and "adjoint f y \ x = y \ f x" by (simp_all add: adjoint_works[OF lf] dot_sym ) lemma adjoint_adjoint: - fixes f:: "'a::comm_ring_1 ^ 'n::finite \ 'a ^ 'm::finite" + fixes f:: "'a::comm_ring_1 ^ 'n \ '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 \ 'a ^ 'm::finite" + fixes f:: "'a::comm_ring_1 ^ 'n \ 'a ^'m" assumes lf: "linear f" and u: "\x y. f' x \ y = x \ f y" shows "f' = adjoint f" apply (rule ext) @@ -2032,14 +2020,14 @@ consts generic_mult :: "'a \ 'b \ 'c" (infixr "\" 75) defs (overloaded) -matrix_matrix_mult_def: "(m:: ('a::semiring_1) ^('n::finite)^'m::finite) \ (m' :: 'a ^('p::finite)^'n) \ (\ i j. setsum (\k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m" +matrix_matrix_mult_def: "(m:: ('a::semiring_1) ^'n^'m) \ (m' :: 'a ^'p^'n) \ (\ i j. setsum (\k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m" abbreviation - matrix_matrix_mult' :: "('a::semiring_1) ^('n::finite)^'m::finite \ 'a ^('p::finite)^'n \ 'a ^ 'p ^'m" (infixl "**" 70) + matrix_matrix_mult' :: "('a::semiring_1) ^'n^'m \ 'a ^'p^'n \ 'a ^ 'p ^'m" (infixl "**" 70) where "m ** m' == m\ m'" defs (overloaded) - matrix_vector_mult_def: "(m::('a::semiring_1) ^('n::finite)^('m::finite)) \ (x::'a ^'n) \ (\ i. setsum (\j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m" + matrix_vector_mult_def: "(m::('a::semiring_1) ^'n^'m) \ (x::'a ^'n) \ (\ i. setsum (\j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m" abbreviation matrix_vector_mult' :: "('a::semiring_1) ^'n^'m \ 'a ^'n \ 'a ^ 'm" (infixl "*v" 70) @@ -2047,26 +2035,26 @@ "m *v v == m \ v" defs (overloaded) - vector_matrix_mult_def: "(x::'a^('m::finite)) \ (m::('a::semiring_1) ^('n::finite)^'m) \ (\ j. setsum (\i. ((m$i)$j) * (x$i)) (UNIV :: 'm set)) :: 'a^'n" + vector_matrix_mult_def: "(x::'a^'m) \ (m::('a::semiring_1) ^'n^'m) \ (\ j. setsum (\i. ((m$i)$j) * (x$i)) (UNIV :: 'm set)) :: 'a^'n" abbreviation vactor_matrix_mult' :: "'a ^ 'm \ ('a::semiring_1) ^'n^'m \ 'a ^'n " (infixl "v*" 70) where "v v* m == v \ m" -definition "(mat::'a::zero => 'a ^('n::finite)^'n::finite) k = (\ i j. if i = j then k else 0)" -definition "(transp::'a^('n::finite)^('m::finite) \ 'a^'m^'n) A = (\ i j. ((A$j)$i))" -definition "(row::'m::finite => 'a ^'n^'m \ 'a ^'n::finite) i A = (\ j. ((A$i)$j))" -definition "(column::'n::finite =>'a^'n^'m =>'a^'m::finite) j A = (\ i. ((A$i)$j))" -definition "rows(A::'a^('n::finite)^'m::finite) = { row i A | i. i \ (UNIV :: 'm set)}" -definition "columns(A::'a^('n::finite)^'m::finite) = { column i A | i. i \ (UNIV :: 'n set)}" +definition "(mat::'a::zero => 'a ^'n^'n) k = (\ i j. if i = j then k else 0)" +definition "(transp::'a^'n^'m \ 'a^'m^'n) A = (\ i j. ((A$j)$i))" +definition "(row::'m => 'a ^'n^'m \ 'a ^'n) i A = (\ j. ((A$i)$j))" +definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\ i. ((A$i)$j))" +definition "rows(A::'a^'n^'m) = { row i A | i. i \ (UNIV :: 'm set)}" +definition "columns(A::'a^'n^'m) = { column i A | i. i \ (UNIV :: 'n set)}" lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def) lemma matrix_add_ldistrib: "(A ** (B + C)) = (A \ B) + (A \ 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 \ (\x. A *v x = B *v x)" (is "?lhs \ ?rhs") apply auto apply (subst Cart_eq) @@ -2146,16 +2134,16 @@ lemma matrix_mult_dot: "A *v x = (\ i. A$i \ 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 (\i. (x$i) *s column i A) (UNIV:: 'n set)" +lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\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) = (\ j. setsum (\i. (x$i) * (basis i :: 'a^'n)$j) (UNIV :: 'n set))" + "(x::'a::ring_1^'n) = (\ j. setsum (\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 \ 'a ^ _" + fixes f:: "'a::ring_1 ^'m \ 'a ^ _" assumes lf: "linear f" shows "(f x)$j = setsum (\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) \ (\A'::'a^'m^'n. A ** A' = mat 1 \ A' ** A = mat 1)" - -definition "matrix_inv(A:: 'a::semiring_1^('n::finite)^'m::finite) = +definition "invertible(A::'a::semiring_1^'n^'m) \ (\A'::'a^'m^'n. A ** A' = mat 1 \ A' ** A = mat 1)" + +definition "matrix_inv(A:: 'a::semiring_1^'n^'m) = (SOME A'::'a^'m^'n. A ** A' = mat 1 \ A' ** A = mat 1)" text{* Correspondence between matrices and linear operators. *} -definition matrix:: "('a::{plus,times, one, zero}^'m::finite \ 'a ^ 'n::finite) \ 'a^'m^'n" +definition matrix:: "('a::{plus,times, one, zero}^'m \ 'a ^ 'n) \ 'a^'m^'n" where "matrix f = (\ i j. (f(basis j))$i)" lemma matrix_vector_mul_linear: "linear(\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 = (\x. matrix f *v (x::'a::comm_ring_1 ^ 'n::finite))" by (simp add: ext matrix_works) - -lemma matrix_of_matrix_vector_mul: "matrix(\x. A *v (x :: 'a:: comm_ring_1 ^ 'n::finite)) = A" +lemma matrix_vector_mul: "linear f ==> f = (\x. matrix f *v (x::'a::comm_ring_1 ^ 'n))" by (simp add: ext matrix_works) + +lemma matrix_of_matrix_vector_mul: "matrix(\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 \ 'a^'m::finite)" - and lg: "linear (g::'a::comm_ring_1^'m::finite \ 'a^_)" + assumes lf: "linear (f::'a::comm_ring_1^'n \ 'a^'m)" + and lg: "linear (g::'a::comm_ring_1^'m \ '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 (\i. (x$i) *s ((transp A)$i)) (UNIV:: 'n set)" +lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\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(\x. (A::'a::comm_ring_1^'n::finite^'m::finite) *v x) = (\x. transp A *v x)" +lemma adjoint_matrix: "adjoint(\x. (A::'a::comm_ring_1^'n^'m) *v x) = (\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 \ 'a ^ 'm::finite)" +lemma matrix_adjoint: assumes lf: "linear (f :: 'a::comm_ring_1^'n \ '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: "(\i. \x. P i x) \ - (\x::'a ^ 'n::finite. \i. P i (x$i))" (is "?lhs \ ?rhs") + (\x::'a ^ 'n. \i. P i (x$i))" (is "?lhs \ ?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 \ real^'m::finite" + fixes f:: "real ^'n \ real^'m" assumes lf: "linear f" shows "(\x. norm x = 1 \ norm (f x) \ b) \ (\x. norm (f x) \ b * norm x)" (is "?lhs \ ?rhs") proof- @@ -2343,7 +2331,7 @@ qed lemma onorm: - fixes f:: "real ^'n::finite \ real ^'m::finite" + fixes f:: "real ^'n \ real ^'m" assumes lf: "linear f" shows "norm (f x) <= onorm f * norm x" and "\x. norm (f x) <= b * norm x \ onorm f <= b" @@ -2367,10 +2355,10 @@ } qed -lemma onorm_pos_le: assumes lf: "linear (f::real ^'n::finite \ real ^'m::finite)" shows "0 <= onorm f" +lemma onorm_pos_le: assumes lf: "linear (f::real ^'n \ 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 \ real ^'m::finite)" +lemma onorm_eq_0: assumes lf: "linear (f::real ^'n \ real ^'m)" shows "onorm f = 0 \ (\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(\x::real^'n::finite. (y::real ^ 'm::finite)) = norm y" +lemma onorm_const: "onorm(\x::real^'n. (y::real ^'m)) = norm y" proof- let ?f = "\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 \ real ^'m::finite)" +lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n \ real ^'m)" shows "0 < onorm f \ ~(\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 \ real ^'m::finite)" - and lg: "linear (g::real^'k::finite \ real^'n::finite)" + assumes lf: "linear (f::real ^'n \ real ^'m)" + and lg: "linear (g::real^'k \ 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 \ real^'m::finite)" +lemma onorm_neg_lemma: assumes lf: "linear (f::real ^'n \ real^'m)" shows "onorm (\x. - f x) \ 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 \ real^'m::finite)" +lemma onorm_neg: assumes lf: "linear (f::real ^'n \ real^'m)" shows "onorm (\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 \ real ^'m::finite)" and lg: "linear g" + assumes lf: "linear (f::real ^'n \ real ^'m)" and lg: "linear g" shows "onorm (\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 \ real ^'m::finite) \ linear g \ onorm(f) + onorm(g) <= e +lemma onorm_triangle_le: "linear (f::real ^'n \ real ^'m) \ linear g \ onorm(f) + onorm(g) <= e \ onorm(\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 \ real ^'m::finite) \ linear g \ onorm(f) + onorm(g) < e +lemma onorm_triangle_lt: "linear (f::real ^'n \ real ^'m) \ linear g \ onorm(f) + onorm(g) < e ==> onorm(\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 \ 'a^1)" +lemma linear_to_scalars: assumes lf: "linear (f::'a::comm_ring_1 ^'n \ 'a^1)" shows "f = (\x. vec1(row 1 (matrix f) \ 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)) \ (pastecart y1 y2) = x1 \ y1 + x2 \ y2" +lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n) (x2::'a::{times,comm_monoid_add}^'m)) \ (pastecart y1 y2) = x1 \ y1 + x2 \ 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 \ S \ span_induct_alt_help S z \ span_induct_alt_help S (c *s x + z)" lemma span_induct_alt': - assumes h0: "h (0::'a::semiring_1^'n::finite)" and hS: "\c x y. x \ S \ h y \ h (c*s x + y)" shows "\x \ span S. h x" + assumes h0: "h (0::'a::semiring_1^'n)" and hS: "\c x y. x \ S \ h y \ h (c*s x + y)" shows "\x \ 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: "\c x y. x \ S \ h y \ h (c*s x + y)" and x: "x \ span S" + assumes h0: "h (0::'a::semiring_1^'n)" and hS: "\c x y. x \ S \ h y \ h (c*s x + y)" and x: "x \ 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 \ (UNIV :: 'n set)} = UNIV" +lemma span_stdbasis:"span {basis i :: 'a::ring_1^'n | i. i \ (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\ (UNIV:: 'n set)}" (is "finite ?S") +lemma finite_stdbasis: "finite {basis i ::real^'n |i. i\ (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\ (UNIV :: 'n set)} = CARD('n)" (is "card ?S = _") +lemma card_stdbasis: "card {basis i ::real^'n |i. i\ (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\ (UNIV :: 'n set)}" +lemma independent_stdbasis: "independent {basis i ::real^'n |i. i\ (UNIV :: 'n set)}" proof- let ?I = "UNIV :: 'n set" let ?b = "basis :: _ \ 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 \ span t" shows "\t'. (card t' = card t) \ finite t' \ s \ t' \ t' \ s \ t \ s \ 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 \ finite S \ 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) \ V" and iS: "independent S" + assumes sv: "(S::(real^'n) set) \ V" and iS: "independent S" shows "\B. S \ B \ B \ V \ independent B \ V \ span B" using sv iS proof(induct d\ "CARD('n) - card S" arbitrary: S rule: nat_less_induct) @@ -3715,14 +3703,14 @@ qed lemma maximal_independent_subset: - "\(B:: (real ^'n::finite) set). B\ V \ independent B \ V \ span B" + "\(B:: (real ^'n) set). B\ V \ independent B \ V \ span B" by (metis maximal_independent_subset_extend[of "{}:: (real ^'n) set"] empty_subsetI independent_empty) (* Notion of dimension. *) definition "dim V = (SOME n. \B. B \ V \ independent B \ V \ span B \ (card B = n))" -lemma basis_exists: "\B. (B :: (real ^'n::finite) set) \ V \ independent B \ V \ span B \ (card B = dim V)" +lemma basis_exists: "\B. (B :: (real ^'n) set) \ V \ independent B \ V \ span B \ (card B = dim V)" unfolding dim_def some_eq_ex[of "\n. \B. B \ V \ independent B \ V \ span B \ (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) \ V" and "independent B" shows "card B \ dim V" + assumes "(B::(real ^'n) set) \ V" and "independent B" shows "card B \ dim V" proof - from basis_exists[of V] `B \ V` obtain B' where "independent B'" and "B \ 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) \ V \ V \ span B \ finite B \ dim V \ card B" +lemma span_card_ge_dim: "(B::(real ^'n) set) \ V \ V \ span B \ finite B \ dim V \ card B" by (metis basis_exists[of V] independent_span_bound subset_trans) lemma basis_card_eq_dim: - "B \ (V:: (real ^'n::finite) set) \ V \ span B \ independent B \ finite B \ card B = dim V" + "B \ (V:: (real ^'n) set) \ V \ span B \ independent B \ finite B \ 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) \ V \ V \ span B \ independent B \ card B = n \ dim V = n" +lemma dim_unique: "(B::(real ^'n) set) \ V \ V \ span B \ independent B \ card B = n \ 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\ (UNIV :: 'n set)}"]) by (auto simp only: span_stdbasis card_stdbasis finite_stdbasis independent_stdbasis) lemma dim_subset: - "(S:: (real ^'n::finite) set) \ T \ dim S \ dim T" + "(S:: (real ^'n) set) \ T \ dim S \ 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) \ CARD('n)" +lemma dim_subset_univ: "dim (S:: (real^'n) set) \ 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) \ V" and iB:"independent B" and dVB:"dim V \ card B" + assumes BV:"(B::(real ^'n) set) \ V" and iB:"independent B" and dVB:"dim V \ card B" shows "V \ span B" proof- {fix a assume aV: "a \ V" @@ -3779,7 +3767,7 @@ qed lemma card_le_dim_spanning: - assumes BV: "(B:: (real ^'n::finite) set) \ V" and VB: "V \ span B" + assumes BV: "(B:: (real ^'n) set) \ V" and VB: "V \ span B" and fB: "finite B" and dVB: "dim V \ 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) \ V \ card B = dim V \ finite B \ independent B \ V \ span B" +lemma card_eq_dim: "(B:: (real ^'n) set) \ V \ card B = dim V \ finite B \ independent B \ V \ 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) \ finite S \ card S \ dim S" + "independent (S:: (real^'n) set) \ finite S \ card S \ dim S" by (metis independent_card_le_dim independent_bound subset_refl) -lemma dependent_biggerset_general: "(finite (S:: (real^'n::finite) set) \ card S > dim S) \ dependent S" +lemma dependent_biggerset_general: "(finite (S:: (real^'n) set) \ card S > dim S) \ 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 \ 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) \ span T \ dim S \ dim T" +lemma subset_le_dim: "(S:: (real ^'n) set) \ span T \ dim S \ 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 \ real^'m::finite" - assumes lf: "linear f" shows "dim (f ` S) \ dim (S:: (real ^'n::finite) set)" + fixes f :: "real^'n \ real^'m" + assumes lf: "linear f" shows "dim (f ` S) \ dim (S:: (real ^'n) set)" proof- from basis_exists[of S] obtain B where B: "B \ S" "independent B" "S \ span B" "card B = dim S" by blast @@ -3886,14 +3874,14 @@ (* FIXME : Move to some general theory ?*) definition "pairwise R S \ (\x \ S. \y\ S. x\y \ R x y)" -lemma vector_sub_project_orthogonal: "(b::'a::ordered_field^'n::finite) \ (x - ((b \ x) / (b\b)) *s b) = 0" +lemma vector_sub_project_orthogonal: "(b::'a::ordered_field^'n) \ (x - ((b \ x) / (b\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 "\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C" (is " \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 "\B. independent B \ B \ span V \ V \ span B \ (card B = dim V) \ pairwise orthogonal B" proof- from basis_exists[of V] obtain B where B: "B \ V" "independent B" "V \ span B" "card B = dim V" by blast @@ -3997,7 +3985,7 @@ lemma span_not_univ_orthogonal: assumes sU: "span S \ UNIV" - shows "\(a:: real ^'n::finite). a \0 \ (\x \ span S. a \ x = 0)" + shows "\(a:: real ^'n). a \0 \ (\x \ span S. a \ x = 0)" proof- from sU obtain a where a: "a \ 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 \ (UNIV ::(real^'n::finite) set)" + assumes SU: "span S \ (UNIV ::(real^'n) set)" shows "\ a. a \0 \ span S \ {x. a \ x = 0}" using span_not_univ_orthogonal[OF SU] by auto lemma lowdim_subset_hyperplane: assumes d: "dim S < CARD('n::finite)" - shows "\(a::real ^'n::finite). a \ 0 \ span S \ {x. a \ x = 0}" + shows "\(a::real ^'n). a \ 0 \ span S \ {x. a \ 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 "\g. (\x\ span B. \y\ span B. g ((x::'a::field^'n::finite) + y) = g x + g y) + shows "\g. (\x\ span B. \y\ span B. g ((x::'a::field^'n) + y) = g x + g y) \ (\x\ span B. \c. g (c*s x) = c *s g x) \ (\x\ 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 "\g. linear g \ (\x\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 "\f. linear f \ f ` S = T \ inj_on f S" proof- @@ -4320,7 +4308,7 @@ qed lemma linear_eq_stdbasis: - assumes lf: "linear (f::'a::ring_1^'m::finite \ 'a^'n::finite)" and lg: "linear g" + assumes lf: "linear (f::'a::ring_1^'m \ 'a^'n)" and lg: "linear g" and fg: "\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 \ 'a^'n::finite \ 'a^_)" + assumes bf: "bilinear (f:: 'a::ring_1^'m \ 'a^'n \ 'a^_)" and bg: "bilinear g" and fg: "\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 \ real ^'m::finite)" and fi: "inj f" + assumes lf: "linear (f::real ^'n \ real ^'m)" and fi: "inj f" shows "\g. linear g \ 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 \ real ^'n::finite)" and sf: "surj f" + assumes lf: "linear (f:: real ^'m \ real ^'n)" and sf: "surj f" shows "\g. linear g \ f o g = id" proof- from linear_independent_extend[OF independent_stdbasis] @@ -4420,7 +4408,7 @@ qed lemma matrix_left_invertible_injective: -"(\B. (B::real^'m^'n) ** (A::real^'n::finite^'m::finite) = mat 1) \ (\x y. A *v x = A *v y \ x = y)" +"(\B. (B::real^'m^'n) ** (A::real^'n^'m) = mat 1) \ (\x y. A *v x = A *v y \ 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: - "(\B. (B::real ^'m::finite^'n::finite) ** (A::real^'n^'m) = mat 1) \ (\x. A *v x = 0 \ x = 0)" + "(\B. (B::real ^'m^'n) ** (A::real^'n^'m) = mat 1) \ (\x. A *v x = 0 \ 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: -"(\B. (A::real^'n::finite^'m::finite) ** (B::real^'m^'n) = mat 1) \ surj (\x. A *v x)" +"(\B. (A::real^'n^'m) ** (B::real^'m^'n) = mat 1) \ surj (\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 "(\(B::real ^'m^'n). B ** A = mat 1) \ (\c. setsum (\i. c i *s column i A) (UNIV :: 'n set) = 0 \ (\i. c i = 0))" (is "?lhs \ ?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 "(\(B::real^'m^'n). A ** B = mat 1) \ (\c. setsum (\i. c i *s row i A) (UNIV :: 'm set) = 0 \ (\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: - "(\(B::real ^'n::finite^'m::finite). (A::real ^'m^'n) ** B = mat 1) \ span (columns A) = UNIV" (is "?lhs = ?rhs") + "(\(B::real ^'n^'m). (A::real ^'m^'n) ** B = mat 1) \ 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: - "(\(B::real^'m::finite^'n::finite). B ** (A::real^'n^'m) = mat 1) \ span (rows A) = UNIV" + "(\(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \ 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 \ real ^'n)" and fi: "inj f" + assumes lf: "linear (f:: real ^'n \ 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 \ real ^'n)" and fi: "inj f" + assumes lf: "linear (f :: real^'n \ real ^'n)" and fi: "inj f" shows "\f'. linear f' \ (\x. f' (f x) = x) \ (\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 \ real ^'n)" and sf: "surj f" + assumes lf: "linear (f::real ^'n \ real ^'n)" and sf: "surj f" shows "\f'. linear f' \ (\x. f' (f x) = x) \ (\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 \ real ^'n)" and lf': "linear f'" + assumes lf: "linear (f::real ^'n \ real ^'n)" and lf': "linear f'" shows "f o f' = id \ f' o f = id" proof- {fix f f':: "real ^'n \ 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 \ real ^'n)" and gf: "g o f = id" + assumes lf: "linear (f::real ^'n \ 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 \ real ^'n)" and gf: "f o g = id" + assumes lf: "linear (f:: real ^'n \ 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 \ 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) \ y = (((rowvector x ::'a^'n^1) ** (columnvector y :: 'a^1^'n))$1)$1" +lemma dot_matrix_product: "(x::'a::semiring_1^'n) \ 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) \ (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\ (UNIV :: 'n set)}" +definition "infnorm (x::real^'n) = Sup {abs(x$i) |i. i\ (UNIV :: 'n set)}" lemma numseg_dimindex_nonempty: "\i. i \ (UNIV :: 'n set)" by auto @@ -4820,18 +4808,18 @@ (\i. abs(x$i)) ` (UNIV)" by blast lemma infnorm_set_lemma: - shows "finite {abs((x::'a::abs ^'n::finite)$i) |i. i\ (UNIV :: 'n set)}" + shows "finite {abs((x::'a::abs ^'n)$i) |i. i\ (UNIV :: 'n set)}" and "{abs(x$i) |i. i\ (UNIV :: 'n::finite set)} \ {}" unfolding infnorm_set_image by (auto intro: finite_imageI) -lemma infnorm_pos_le: "0 \ infnorm (x::real^'n::finite)" +lemma infnorm_pos_le: "0 \ 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) \ infnorm x + infnorm y" +lemma infnorm_triangle: "infnorm ((x::real^'n) + y) \ infnorm x + infnorm y" proof- have th: "\x y (z::real). x - y <= z \ x - z <= y" by arith have th1: "\S f. f ` S = { f i| i. i \ S}" by blast @@ -4852,7 +4840,7 @@ done qed -lemma infnorm_eq_0: "infnorm x = 0 \ (x::real ^'n::finite) = 0" +lemma infnorm_eq_0: "infnorm x = 0 \ (x::real ^'n) = 0" proof- have "infnorm x <= 0 \ x = 0" unfolding infnorm_def @@ -4894,7 +4882,7 @@ using infnorm_pos_le[of x] by arith lemma component_le_infnorm: - shows "\x$i\ \ infnorm (x::real^'n::finite)" + shows "\x$i\ \ infnorm (x::real^'n)" proof- let ?U = "UNIV :: 'n set" let ?S = "{\x$i\ |i. i\ ?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 \ 0" by simp @@ -4973,7 +4961,7 @@ (* Equality in Cauchy-Schwarz and triangle inequalities. *) -lemma norm_cauchy_schwarz_eq: "(x::real ^'n::finite) \ y = norm x * norm y \ norm x *s y = norm y *s x" (is "?lhs \ ?rhs") +lemma norm_cauchy_schwarz_eq: "(x::real ^'n) \ y = norm x * norm y \ norm x *s y = norm y *s x" (is "?lhs \ ?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 \ y) = norm x * norm y \ norm x *s y = norm y *s x \ norm(x) *s y = - norm y *s x" (is "?lhs \ ?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 \ norm x *s y = norm y *s x" proof- {assume x: "x =0 \ 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 \ y) = norm x * norm y \ collinear {(0::real^'n),x,y}" unfolding norm_cauchy_schwarz_abs_eq apply (cases "x=0", simp_all add: collinear_2) diff -r 1edf0f223c6e -r 4e896680897e src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- 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) \ 'a) set" + ('a, 'b) cart = "UNIV :: (('b::finite) \ 'a) set" morphisms Cart_nth Cart_lambda .. notation Cart_nth (infixl "$" 90) @@ -20,8 +19,8 @@ notation (xsymbols) Cart_lambda (binder "\" 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 \ type \ type" ("(_ ^/ _)" [15, 16] 15) @@ -45,15 +44,13 @@ apply auto done -lemma Cart_eq: "((x:: 'a ^ 'b::finite) = y) \ (\i. x$i = y$i)" +lemma Cart_eq: "(x = y) \ (\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 "(\i. f$i = g i) \ Cart_lambda g = f" +lemma Cart_lambda_unique: "(\i. f$i = g i) \ Cart_lambda g = f" by (auto simp add: Cart_eq) lemma Cart_lambda_eta: "(\ i. (g$i)) = g" @@ -61,14 +58,9 @@ text{* A non-standard sum to "paste" Cartesian products. *} -definition pastecart :: "'a ^ 'm::finite \ 'a ^ 'n::finite \ 'a ^ ('m + 'n)" where - "pastecart f g = (\ i. case i of Inl a \ f$a | Inr b \ g$b)" - -definition fstcart:: "'a ^('m::finite + 'n::finite) \ 'a ^ 'm" where - "fstcart f = (\ i. (f$(Inl i)))" - -definition sndcart:: "'a ^('m::finite + 'n::finite) \ 'a ^ 'n" where - "sndcart f = (\ i. (f$(Inr i)))" +definition "pastecart f g = (\ i. case i of Inl a \ f$a | Inr b \ g$b)" +definition "fstcart f = (\ i. (f$(Inl i)))" +definition "sndcart f = (\ 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 \ 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" diff -r 1edf0f223c6e -r 4e896680897e src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- 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]: "\ x islimpt {}" unfolding islimpt_def by auto -lemma closed_positive_orthant: "closed {x::real^'n::finite. \i. 0 \x$i}" +lemma closed_positive_orthant: "closed {x::real^'n. \i. 0 \x$i}" proof- let ?U = "UNIV :: 'n set" let ?O = "{x::real^'n. \i. x$i\0}" @@ -1296,7 +1296,7 @@ qed lemma Lim_component: - fixes f :: "'a \ 'b::metric_space ^ 'n::finite" + fixes f :: "'a \ 'b::metric_space ^ 'n" shows "(f ---> l) net \ ((\a. f a $i) ---> l$i) net" unfolding tendsto_iff apply (clarify) @@ -2284,7 +2284,7 @@ done lemma compact_lemma: - fixes f :: "nat \ 'a::heine_borel ^ 'n::finite" + fixes f :: "nat \ 'a::heine_borel ^ 'n" assumes "bounded s" and "\n. f n \ s" shows "\d. \l r. subseq r \ @@ -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 \ 'a ^ 'b" assume s: "bounded s" and f: "\n. f n \ 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 \ s \ y \ 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. \i. a$i < x$i \ x$i < b$i}" and "{a .. b} = {x::'a^'n. \i. a$i \ x$i \ x$i \ 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 \ {a<.. (\i. a$i < x$i \ x$i < b$i)" "x \ {a .. b} \ (\i. a$i \ x$i \ x$i \ 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} = {} \ (\i. b$i \ a$i))" (is ?th1) and "({a .. b} = {} \ (\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} \ {} \ (\i. a$i \ b$i)" and "{a <..< b} \ {} \ (\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 "(\i. a$i \ c$i \ d$i \ b$i) \ {c .. d} \ {a .. b}" and "(\i. a$i < c$i \ d$i < b$i) \ {c .. d} \ {a<..i. a$i \ c$i \ d$i \ b$i) \ {c<.. {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} \ {a<.. {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} \ {a .. b} \ (\i. c$i \ d$i) --> (\i. a$i \ c$i \ d$i \ b$i)" (is ?th1) and "{c .. d} \ {a<.. (\i. c$i \ d$i) --> (\i. a$i < c$i \ d$i < b$i)" (is ?th2) and "{c<.. {a .. b} \ (\i. c$i < d$i) --> (\i. a$i \ c$i \ d$i \ 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} \ {c .. d} = {} \ (\i. (b$i < a$i \ d$i < c$i \ b$i < c$i \ d$i < a$i))" (is ?th1) and "{a .. b} \ {c<.. (\i. (b$i < a$i \ d$i \ c$i \ b$i \ c$i \ d$i \ a$i))" (is ?th2) and "{a<.. {c .. d} = {} \ (\i. (b$i \ a$i \ d$i < c$i \ b$i \ c$i \ d$i \ 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} \ {c .. d} = {(\ i. max (a$i) (c$i)) .. (\ 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 \ x < b ==> (\d>0. \x'. abs(x' - x) < d --> a < x' \ 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<..{a<..e>0. \x'\{a..b}. x' \ x \ dist x' x < e"(* and xab:"a$i > x$i \ 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<.. ?L" using interior_maximal[OF interval_open_subset_closed open_interval] by auto @@ -4878,7 +4878,7 @@ thus "?L \ ?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 = "\i\UNIV. \a$i\ + \b$i\" @@ -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} \ bounded {a<.. UNIV) \ ({a<.. 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<.. {}" shows "((1/2) *\<^sub>R (a + b)) \ {a<.. {a<.. {a .. b}" and e:"0 < e" "e \ 1" shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \ {a<.. {}" shows "closure {a<..a. s \ {-a<..0" and b:"\x\s. norm x \ 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 ==> (\a b. s \ {a<..a. s \ {-a .. a}" proof- obtain a where "s \ {- a<.. (\a b. s \ {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<.. {}" shows "{a<.. {c .. d} = {} \ {a<.. {c<..i. x$i \ 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. \i. a$i \ x$i}" proof- { fix i @@ -5109,7 +5109,7 @@ definition "is_interval s \ (\a\s. \b\s. \x. (\i. ((a$i \ x$i \ x$i \ b$i) \ (b$i \ x$i \ x$i \ a$i))) \ x \ s)" -lemma is_interval_interval: "is_interval {a .. b::real^'n::finite}" (is ?th1) "is_interval {a<..x y z::real. x < y \ y < z \ 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 \ a}" + shows "closed {x::real^'n. x$i \ 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 \ a}" + shows "closed {x::real^'n. x$i \ 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 \ real^'n::finite" +lemma Lim_component_le: fixes f :: "'a \ real^'n" assumes "(f ---> l) net" "\ (trivial_limit net)" "eventually (\x. f(x)$i \ b) net" shows "l$i \ 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 \ real^'n::finite" +lemma Lim_component_ge: fixes f :: "'a \ real^'n" assumes "(f ---> l) net" "\ (trivial_limit net)" "eventually (\x. b \ (f x)$i) net" shows "b \ 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 \ real^'n::finite" +lemma Lim_component_eq: fixes f :: "'a \ real^'n" assumes net:"(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\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 \ x \ s \ y \ s \ x$k \ a \ a \ y$k \ (\z\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 \ real ^ 'n::finite" + fixes x :: "nat \ real ^ 'n" assumes e:"0 < e" and s:"subspace s" and f:"bounded_linear f" and normf:"\x\s. norm(f x) \ e * norm(x)" and xs:"\n::nat. x n \ 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 \ real^'n::finite" +lemma injective_imp_isometric: fixes f::"real^'m \ real^'n" assumes s:"closed s" "subspace s" and f:"bounded_linear f" "\x\s. (f x = 0) \ (x = 0)" shows "\e>0. \x\s. norm (f x) \ e * norm(x)" proof(cases "s \ {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. \i. P i --> x$i = 0}" (is "closed ?A") + "closed {x::real^'n. \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 \ ?D}" @@ -5587,7 +5587,7 @@ qed lemma dim_substandard: - shows "dim {x::real^'n::finite. \i. i \ d \ x$i = 0} = card d" (is "dim ?A = _") + shows "dim {x::real^'n. \i. i \ d \ x$i = 0} = card d" (is "dim ?A = _") proof- let ?D = "UNIV::'n set" let ?B = "(basis::'n\real^'n) ` d" @@ -5653,7 +5653,7 @@ apply (subgoal_tac "A \ 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 \ 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 "(\x. m *\<^sub>R x + c) ` {a .. b} = (if {a .. b} = {} then {} else (if 0 \ 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:"(\x. m *\<^sub>R (x::real^'n::finite)) ` {a..b} = +lemma image_smult_interval:"(\x. m *\<^sub>R (x::real^'n)) ` {a..b} = (if {a..b} = {} then {} else if 0 \ 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