# HG changeset patch # User haftmann # Date 1272866391 -7200 # Node ID 6ed6112f0a954a79db70f72c5d4bb4a03ca82fa2 # Parent e5f7235f39c5b4b38b8fadf552360eb21a78c728# Parent 16736dde54c0edfd5ec1ac8079d6e1190bc02094 merged diff -r 16736dde54c0 -r 6ed6112f0a95 Admin/isatest/isatest-stats --- a/Admin/isatest/isatest-stats Fri Apr 30 18:34:51 2010 +0200 +++ b/Admin/isatest/isatest-stats Mon May 03 07:59:51 2010 +0200 @@ -6,7 +6,7 @@ THIS=$(cd "$(dirname "$0")"; pwd -P) -PLATFORMS="at-poly at-poly-test at64-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev sun-poly" +PLATFORMS="at-poly at-poly-test at64-poly cygwin-poly mac-poly-M4 mac-poly64-M4 mac-poly-M8 mac-poly64-M8 at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev sun-poly" ISABELLE_SESSIONS="\ HOL-Plain \ diff -r 16736dde54c0 -r 6ed6112f0a95 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/FOL/simpdata.ML Mon May 03 07:59:51 2010 +0200 @@ -21,13 +21,13 @@ | _ => th RS @{thm iff_reflection_T}; (*Replace premises x=y, X<->Y by X==Y*) -val mk_meta_prems = - rule_by_tactic +fun mk_meta_prems ctxt = + rule_by_tactic ctxt (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}])); (*Congruence rules for = or <-> (instead of ==)*) -fun mk_meta_cong (_: simpset) rl = - Drule.export_without_context (mk_meta_eq (mk_meta_prems rl)) +fun mk_meta_cong ss rl = + Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl)) handle THM _ => error("Premises and conclusion of congruence rules must use =-equality or <->"); @@ -35,10 +35,6 @@ [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]), ("All", [@{thm spec}]), ("True", []), ("False", [])]; -(* ###FIXME: move to simplifier.ML -val mk_atomize: (string * thm list) list -> thm -> thm list -*) -(* ###FIXME: move to simplifier.ML *) fun mk_atomize pairs = let fun atoms th = (case concl_of th of diff -r 16736dde54c0 -r 6ed6112f0a95 src/FOLP/simp.ML --- a/src/FOLP/simp.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/FOLP/simp.ML Mon May 03 07:59:51 2010 +0200 @@ -222,7 +222,7 @@ fun normed_rews congs = let val add_norms = add_norm_tags congs in fn thm => Variable.tradeT - (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.thm_context thm) [thm] + (K (map (add_norms o mk_trans) o maps mk_rew_rules)) (Variable.global_thm_context thm) [thm] end; fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac]; diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/IsaMakefile Mon May 03 07:59:51 2010 +0200 @@ -1080,18 +1080,22 @@ $(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL-SMT \ Multivariate_Analysis/ROOT.ML \ Multivariate_Analysis/document/root.tex \ + Multivariate_Analysis/Brouwer_Fixpoint.thy \ + Multivariate_Analysis/Convex_Euclidean_Space.thy \ + Multivariate_Analysis/Derivative.thy \ + Multivariate_Analysis/Determinants.thy \ + Multivariate_Analysis/Euclidean_Space.thy \ + Multivariate_Analysis/Fashoda.thy \ + Multivariate_Analysis/Finite_Cartesian_Product.thy \ + Multivariate_Analysis/Integration.thy \ + Multivariate_Analysis/Integration.cert \ Multivariate_Analysis/L2_Norm.thy \ Multivariate_Analysis/Multivariate_Analysis.thy \ - Multivariate_Analysis/Determinants.thy \ - Multivariate_Analysis/Finite_Cartesian_Product.thy \ - Multivariate_Analysis/Euclidean_Space.thy \ + Multivariate_Analysis/Operator_Norm.thy \ + Multivariate_Analysis/Path_Connected.thy \ + Multivariate_Analysis/Real_Integration.thy \ Multivariate_Analysis/Topology_Euclidean_Space.thy \ - Multivariate_Analysis/Convex_Euclidean_Space.thy \ - Multivariate_Analysis/Brouwer_Fixpoint.thy \ - Multivariate_Analysis/Derivative.thy \ - Multivariate_Analysis/Integration.thy \ - Multivariate_Analysis/Integration.cert \ - Multivariate_Analysis/Real_Integration.thy + Multivariate_Analysis/Vec1.thy @cd Multivariate_Analysis; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-SMT HOL-Multivariate_Analysis diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Mon May 03 07:59:51 2010 +0200 @@ -152,7 +152,8 @@ in case map_filter (fn th'' => SOME (th'', singleton - (Variable.trade (K (fn [th'''] => [th''' RS th'])) (Variable.thm_context th'')) th'') + (Variable.trade (K (fn [th'''] => [th''' RS th'])) + (Variable.global_thm_context th'')) th'') handle THM _ => NONE) thms of [] => NONE | thps => diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Library/normarith.ML --- a/src/HOL/Library/normarith.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Library/normarith.ML Mon May 03 07:59:51 2010 +0200 @@ -395,7 +395,7 @@ fun init_conv ctxt = Simplifier.rewrite (Simplifier.context ctxt - (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm vector_dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) + (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) then_conv field_comp_conv then_conv nnf_conv diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Metis_Examples/Message.thy --- a/src/HOL/Metis_Examples/Message.thy Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Metis_Examples/Message.thy Mon May 03 07:59:51 2010 +0200 @@ -711,7 +711,7 @@ lemma Fake_parts_insert: "X \ synth (analz H) ==> parts (insert X H) \ synth (analz H) \ parts H" -sledgehammer +(*sledgehammer*) proof - assume A1: "X \ synth (analz H)" have F1: "\x\<^isub>1. analz x\<^isub>1 \ synth (analz x\<^isub>1) = analz (synth (analz x\<^isub>1))" diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Mon May 03 07:59:51 2010 +0200 @@ -1190,7 +1190,7 @@ have d':"d / real n / 8 > 0" apply(rule divide_pos_pos)+ using d(1) unfolding n_def by auto have *:"uniformly_continuous_on {0..1} f" by(rule compact_uniformly_continuous[OF assms(1) compact_interval]) guess e using *[unfolded uniformly_continuous_on_def,rule_format,OF d'] apply-apply(erule exE,(erule conjE)+) . - note e=this[rule_format,unfolded vector_dist_norm] + note e=this[rule_format,unfolded dist_norm] show ?thesis apply(rule_tac x="min (e/2) (d/real n/8)" in exI) apply(rule) defer apply(rule,rule,rule,rule,rule) apply(erule conjE)+ proof- show "0 < min (e / 2) (d / real n / 8)" using d' e by auto @@ -1202,7 +1202,7 @@ show "\f x $ i - x $ i\ \ norm (f y -f x) + norm (y - x)" apply(rule lem1[rule_format]) using as by auto show "\f x $ i - f z $ i\ \ norm (f x - f z)" "\x $ i - z $ i\ \ norm (x - z)" unfolding vector_minus_component[THEN sym] by(rule component_le_norm)+ - have tria:"norm (y - x) \ norm (y - z) + norm (x - z)" using dist_triangle[of y x z,unfolded vector_dist_norm] + have tria:"norm (y - x) \ norm (y - z) + norm (x - z)" using dist_triangle[of y x z,unfolded dist_norm] unfolding norm_minus_commute by auto also have "\ < e / 2 + e / 2" apply(rule add_strict_mono) using as(4,5) by auto finally show "norm (f y - f x) < d / real n / 8" apply- apply(rule e(2)) using as by auto @@ -1355,14 +1355,14 @@ 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 - apply(erule_tac exE,rule_tac x=b in exI) by(auto simp add: vector_dist_norm) + apply(erule_tac exE,rule_tac x=b in exI) by(auto simp add: dist_norm) then guess e apply-apply(erule exE,(erule conjE)+) . note e=this have "\x\ cball 0 e. (f \ closest_point s) x = x" apply(rule_tac brouwer_ball[OF e(1), of 0 "f \ closest_point s"]) apply(rule continuous_on_compose ) apply(rule continuous_on_closest_point[OF assms(2) compact_imp_closed[OF assms(1)] assms(3)]) apply(rule continuous_on_subset[OF assms(4)]) using closest_point_in_set[OF compact_imp_closed[OF assms(1)] assms(3)] apply - defer - using assms(5)[unfolded subset_eq] using e(2)[unfolded subset_eq mem_cball] by(auto simp add:vector_dist_norm) + using assms(5)[unfolded subset_eq] using e(2)[unfolded subset_eq mem_cball] by(auto simp add: dist_norm) then guess x .. note x=this have *:"closest_point s x = x" apply(rule closest_point_self) apply(rule assms(5)[unfolded subset_eq,THEN bspec[where x="x"],unfolded image_iff]) @@ -1380,7 +1380,7 @@ apply(rule,rule,erule conjE) apply(rule brouwer_ball[OF assms]) apply assumption+ apply(rule_tac x=x in bexI) apply assumption+ apply(rule continuous_on_intros)+ unfolding frontier_cball subset_eq Ball_def image_iff apply(rule,rule,erule bexE) - unfolding vector_dist_norm apply(simp add: * norm_minus_commute) . note x = this + unfolding dist_norm apply(simp add: * norm_minus_commute) . note x = this hence "scaleR 2 a = scaleR 1 x + scaleR 1 x" by(auto simp add:algebra_simps) hence "a = x" unfolding scaleR_left_distrib[THEN sym] by auto thus False using x using assms by auto qed diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Mon May 03 07:59:51 2010 +0200 @@ -2110,7 +2110,7 @@ unfolding Ball_def mem_cball dist_norm by (auto simp add: norm_basis[unfolded One_nat_def]) case True show ?thesis unfolding True continuous_at Lim_at apply(rule,rule) apply(rule_tac x="e / B" in exI) apply(rule) apply(rule divide_pos_pos) prefer 3 apply(rule,rule,erule conjE) - unfolding norm_0 scaleR_zero_left dist_norm diff_0_right norm_scaleR abs_norm_cancel proof- + unfolding norm_zero scaleR_zero_left dist_norm diff_0_right norm_scaleR abs_norm_cancel proof- fix e and x::"real^'n" assume as:"norm x < e / B" "0 < norm x" "0 frontier s" using pi(1)[of x] unfolding surf(5)[THEN sym] by auto hence "norm (surf (pi x)) \ B" using B fs by auto @@ -2205,14 +2205,6 @@ subsection {* Use this to derive general bound property of convex function. *} -lemma forall_of_pastecart: - "(\p. P (\x. fstcart (p x)) (\x. sndcart (p x))) \ (\x y. P x y)" apply meson - apply(erule_tac x="\a. pastecart (x a) (y a)" in allE) unfolding o_def by auto - -lemma forall_of_pastecart': - "(\p. P (fstcart p) (sndcart p)) \ (\x y. P x y)" apply meson - apply(erule_tac x="pastecart x y" in allE) unfolding o_def by auto - (* TODO: move *) lemma fst_setsum: "fst (\x\A. f x) = (\x\A. fst (f x))" by (cases "finite A", induct set: finite, simp_all) @@ -2815,563 +2807,4 @@ also have "\ < 1" unfolding setsum_constant card_enum real_eq_of_nat real_divide_def[THEN sym] by (auto simp add:field_simps) finally show "setsum (op $ ?a) ?D < 1" by auto qed qed -subsection {* Paths. *} - -definition - path :: "(real \ 'a::topological_space) \ bool" - where "path g \ continuous_on {0 .. 1} g" - -definition - pathstart :: "(real \ 'a::topological_space) \ 'a" - where "pathstart g = g 0" - -definition - pathfinish :: "(real \ 'a::topological_space) \ 'a" - where "pathfinish g = g 1" - -definition - path_image :: "(real \ 'a::topological_space) \ 'a set" - where "path_image g = g ` {0 .. 1}" - -definition - reversepath :: "(real \ 'a::topological_space) \ (real \ 'a)" - where "reversepath g = (\x. g(1 - x))" - -definition - joinpaths :: "(real \ 'a::topological_space) \ (real \ 'a) \ (real \ 'a)" - (infixr "+++" 75) - where "g1 +++ g2 = (\x. if x \ 1/2 then g1 (2 * x) else g2 (2 * x - 1))" - -definition - simple_path :: "(real \ 'a::topological_space) \ bool" - where "simple_path g \ - (\x\{0..1}. \y\{0..1}. g x = g y \ x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0)" - -definition - injective_path :: "(real \ 'a::topological_space) \ bool" - where "injective_path g \ (\x\{0..1}. \y\{0..1}. g x = g y \ x = y)" - -subsection {* Some lemmas about these concepts. *} - -lemma injective_imp_simple_path: - "injective_path g \ simple_path g" - unfolding injective_path_def simple_path_def by auto - -lemma path_image_nonempty: "path_image g \ {}" - unfolding path_image_def image_is_empty interval_eq_empty by auto - -lemma pathstart_in_path_image[intro]: "(pathstart g) \ path_image g" - unfolding pathstart_def path_image_def by auto - -lemma pathfinish_in_path_image[intro]: "(pathfinish g) \ path_image g" - unfolding pathfinish_def path_image_def by auto - -lemma connected_path_image[intro]: "path g \ connected(path_image g)" - unfolding path_def path_image_def - apply (erule connected_continuous_image) - by(rule convex_connected, rule convex_real_interval) - -lemma compact_path_image[intro]: "path g \ compact(path_image g)" - unfolding path_def path_image_def - by (erule compact_continuous_image, rule compact_real_interval) - -lemma reversepath_reversepath[simp]: "reversepath(reversepath g) = g" - unfolding reversepath_def by auto - -lemma pathstart_reversepath[simp]: "pathstart(reversepath g) = pathfinish g" - unfolding pathstart_def reversepath_def pathfinish_def by auto - -lemma pathfinish_reversepath[simp]: "pathfinish(reversepath g) = pathstart g" - unfolding pathstart_def reversepath_def pathfinish_def by auto - -lemma pathstart_join[simp]: "pathstart(g1 +++ g2) = pathstart g1" - unfolding pathstart_def joinpaths_def pathfinish_def by auto - -lemma pathfinish_join[simp]:"pathfinish(g1 +++ g2) = pathfinish g2" - unfolding pathstart_def joinpaths_def pathfinish_def by auto - -lemma path_image_reversepath[simp]: "path_image(reversepath g) = path_image g" proof- - have *:"\g. path_image(reversepath g) \ path_image g" - unfolding path_image_def subset_eq reversepath_def Ball_def image_iff apply(rule,rule,erule bexE) - apply(rule_tac x="1 - xa" in bexI) by auto - show ?thesis using *[of g] *[of "reversepath g"] unfolding reversepath_reversepath by auto qed - -lemma path_reversepath[simp]: "path(reversepath g) \ path g" proof- - have *:"\g. path g \ path(reversepath g)" unfolding path_def reversepath_def - apply(rule continuous_on_compose[unfolded o_def, of _ "\x. 1 - x"]) - apply(rule continuous_on_sub, rule continuous_on_const, rule continuous_on_id) - apply(rule continuous_on_subset[of "{0..1}"], assumption) by auto - show ?thesis using *[of "reversepath g"] *[of g] unfolding reversepath_reversepath by (rule iffI) qed - -lemmas reversepath_simps = path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath - -lemma path_join[simp]: assumes "pathfinish g1 = pathstart g2" shows "path (g1 +++ g2) \ path g1 \ path g2" - unfolding path_def pathfinish_def pathstart_def apply rule defer apply(erule conjE) proof- - assume as:"continuous_on {0..1} (g1 +++ g2)" - have *:"g1 = (\x. g1 (2 *\<^sub>R x)) \ (\x. (1/2) *\<^sub>R x)" - "g2 = (\x. g2 (2 *\<^sub>R x - 1)) \ (\x. (1/2) *\<^sub>R (x + 1))" - unfolding o_def by (auto simp add: add_divide_distrib) - have "op *\<^sub>R (1 / 2) ` {0::real..1} \ {0..1}" "(\x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real)..1} \ {0..1}" - by auto - thus "continuous_on {0..1} g1 \ continuous_on {0..1} g2" apply -apply rule - apply(subst *) defer apply(subst *) apply (rule_tac[!] continuous_on_compose) - apply (rule continuous_on_cmul, rule continuous_on_add, rule continuous_on_id, rule continuous_on_const) defer - apply (rule continuous_on_cmul, rule continuous_on_id) apply(rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3 - apply(rule_tac[1-2] continuous_on_subset[of "{0 .. 1}"]) apply(rule as, assumption, rule as, assumption) - apply(rule) defer apply rule proof- - fix x assume "x \ op *\<^sub>R (1 / 2) ` {0::real..1}" - hence "x \ 1 / 2" unfolding image_iff by auto - thus "(g1 +++ g2) x = g1 (2 *\<^sub>R x)" unfolding joinpaths_def by auto next - fix x assume "x \ (\x. (1 / 2) *\<^sub>R (x + 1)) ` {0::real..1}" - hence "x \ 1 / 2" unfolding image_iff by auto - thus "(g1 +++ g2) x = g2 (2 *\<^sub>R x - 1)" proof(cases "x = 1 / 2") - case True hence "x = (1/2) *\<^sub>R 1" unfolding Cart_eq by auto - thus ?thesis unfolding joinpaths_def using assms[unfolded pathstart_def pathfinish_def] by (auto simp add: mult_ac) - qed (auto simp add:le_less joinpaths_def) qed -next assume as:"continuous_on {0..1} g1" "continuous_on {0..1} g2" - have *:"{0 .. 1::real} = {0.. (1/2)*\<^sub>R 1} \ {(1/2) *\<^sub>R 1 .. 1}" by auto - have **:"op *\<^sub>R 2 ` {0..(1 / 2) *\<^sub>R 1} = {0..1::real}" apply(rule set_ext, rule) unfolding image_iff - defer apply(rule_tac x="(1/2)*\<^sub>R x" in bexI) by auto - have ***:"(\x. 2 *\<^sub>R x - 1) ` {(1 / 2) *\<^sub>R 1..1} = {0..1::real}" - apply (auto simp add: image_def) - apply (rule_tac x="(x + 1) / 2" in bexI) - apply (auto simp add: add_divide_distrib) - done - show "continuous_on {0..1} (g1 +++ g2)" unfolding * apply(rule continuous_on_union) apply (rule closed_real_atLeastAtMost)+ proof- - show "continuous_on {0..(1 / 2) *\<^sub>R 1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "\x. g1 (2 *\<^sub>R x)"]) defer - unfolding o_def[THEN sym] apply(rule continuous_on_compose) apply(rule continuous_on_cmul, rule continuous_on_id) - unfolding ** apply(rule as(1)) unfolding joinpaths_def by auto next - show "continuous_on {(1/2)*\<^sub>R1..1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "g2 \ (\x. 2 *\<^sub>R x - 1)"]) defer - apply(rule continuous_on_compose) apply(rule continuous_on_sub, rule continuous_on_cmul, rule continuous_on_id, rule continuous_on_const) - unfolding *** o_def joinpaths_def apply(rule as(2)) using assms[unfolded pathstart_def pathfinish_def] - by (auto simp add: mult_ac) qed qed - -lemma path_image_join_subset: "path_image(g1 +++ g2) \ (path_image g1 \ path_image g2)" proof - fix x assume "x \ path_image (g1 +++ g2)" - then obtain y where y:"y\{0..1}" "x = (if y \ 1 / 2 then g1 (2 *\<^sub>R y) else g2 (2 *\<^sub>R y - 1))" - unfolding path_image_def image_iff joinpaths_def by auto - thus "x \ path_image g1 \ path_image g2" apply(cases "y \ 1/2") - apply(rule_tac UnI1) defer apply(rule_tac UnI2) unfolding y(2) path_image_def using y(1) - by(auto intro!: imageI) qed - -lemma subset_path_image_join: - assumes "path_image g1 \ s" "path_image g2 \ s" shows "path_image(g1 +++ g2) \ s" - using path_image_join_subset[of g1 g2] and assms by auto - -lemma path_image_join: - assumes "path g1" "path g2" "pathfinish g1 = pathstart g2" - shows "path_image(g1 +++ g2) = (path_image g1) \ (path_image g2)" -apply(rule, rule path_image_join_subset, rule) unfolding Un_iff proof(erule disjE) - fix x assume "x \ path_image g1" - then obtain y where y:"y\{0..1}" "x = g1 y" unfolding path_image_def image_iff by auto - thus "x \ path_image (g1 +++ g2)" unfolding joinpaths_def path_image_def image_iff - apply(rule_tac x="(1/2) *\<^sub>R y" in bexI) by auto next - fix x assume "x \ path_image g2" - then obtain y where y:"y\{0..1}" "x = g2 y" unfolding path_image_def image_iff by auto - then show "x \ path_image (g1 +++ g2)" unfolding joinpaths_def path_image_def image_iff - apply(rule_tac x="(1/2) *\<^sub>R (y + 1)" in bexI) using assms(3)[unfolded pathfinish_def pathstart_def] - by (auto simp add: add_divide_distrib) qed - -lemma not_in_path_image_join: - assumes "x \ path_image g1" "x \ path_image g2" shows "x \ path_image(g1 +++ g2)" - using assms and path_image_join_subset[of g1 g2] by auto - -lemma simple_path_reversepath: assumes "simple_path g" shows "simple_path (reversepath g)" - using assms unfolding simple_path_def reversepath_def apply- apply(rule ballI)+ - apply(erule_tac x="1-x" in ballE, erule_tac x="1-y" in ballE) - by auto - -lemma simple_path_join_loop: - assumes "injective_path g1" "injective_path g2" "pathfinish g2 = pathstart g1" - "(path_image g1 \ path_image g2) \ {pathstart g1,pathstart g2}" - shows "simple_path(g1 +++ g2)" -unfolding simple_path_def proof((rule ballI)+, rule impI) let ?g = "g1 +++ g2" - note inj = assms(1,2)[unfolded injective_path_def, rule_format] - fix x y::"real" assume xy:"x \ {0..1}" "y \ {0..1}" "?g x = ?g y" - show "x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0" proof(case_tac "x \ 1/2",case_tac[!] "y \ 1/2", unfold not_le) - assume as:"x \ 1 / 2" "y \ 1 / 2" - hence "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" using xy(3) unfolding joinpaths_def by auto - moreover have "2 *\<^sub>R x \ {0..1}" "2 *\<^sub>R y \ {0..1}" using xy(1,2) as - by auto - ultimately show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by auto - next assume as:"x > 1 / 2" "y > 1 / 2" - hence "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)" using xy(3) unfolding joinpaths_def by auto - moreover have "2 *\<^sub>R x - 1 \ {0..1}" "2 *\<^sub>R y - 1 \ {0..1}" using xy(1,2) as by auto - ultimately show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto - next assume as:"x \ 1 / 2" "y > 1 / 2" - hence "?g x \ path_image g1" "?g y \ path_image g2" unfolding path_image_def joinpaths_def - using xy(1,2) by auto - moreover have "?g y \ pathstart g2" using as(2) unfolding pathstart_def joinpaths_def - using inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(2) - by (auto simp add: field_simps) - ultimately have *:"?g x = pathstart g1" using assms(4) unfolding xy(3) by auto - hence "x = 0" unfolding pathstart_def joinpaths_def using as(1) and xy(1) - using inj(1)[of "2 *\<^sub>R x" 0] by auto - moreover have "y = 1" using * unfolding xy(3) assms(3)[THEN sym] - unfolding joinpaths_def pathfinish_def using as(2) and xy(2) - using inj(2)[of "2 *\<^sub>R y - 1" 1] by auto - ultimately show ?thesis by auto - next assume as:"x > 1 / 2" "y \ 1 / 2" - hence "?g x \ path_image g2" "?g y \ path_image g1" unfolding path_image_def joinpaths_def - using xy(1,2) by auto - moreover have "?g x \ pathstart g2" using as(1) unfolding pathstart_def joinpaths_def - using inj(2)[of "2 *\<^sub>R x - 1" 0] and xy(1) - by (auto simp add: field_simps) - ultimately have *:"?g y = pathstart g1" using assms(4) unfolding xy(3) by auto - hence "y = 0" unfolding pathstart_def joinpaths_def using as(2) and xy(2) - using inj(1)[of "2 *\<^sub>R y" 0] by auto - moreover have "x = 1" using * unfolding xy(3)[THEN sym] assms(3)[THEN sym] - unfolding joinpaths_def pathfinish_def using as(1) and xy(1) - using inj(2)[of "2 *\<^sub>R x - 1" 1] by auto - ultimately show ?thesis by auto qed qed - -lemma injective_path_join: - assumes "injective_path g1" "injective_path g2" "pathfinish g1 = pathstart g2" - "(path_image g1 \ path_image g2) \ {pathstart g2}" - shows "injective_path(g1 +++ g2)" - unfolding injective_path_def proof(rule,rule,rule) let ?g = "g1 +++ g2" - note inj = assms(1,2)[unfolded injective_path_def, rule_format] - fix x y assume xy:"x \ {0..1}" "y \ {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y" - show "x = y" proof(cases "x \ 1/2", case_tac[!] "y \ 1/2", unfold not_le) - assume "x \ 1 / 2" "y \ 1 / 2" thus ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy - unfolding joinpaths_def by auto - next assume "x > 1 / 2" "y > 1 / 2" thus ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] and xy - unfolding joinpaths_def by auto - next assume as:"x \ 1 / 2" "y > 1 / 2" - hence "?g x \ path_image g1" "?g y \ path_image g2" unfolding path_image_def joinpaths_def - using xy(1,2) by auto - hence "?g x = pathfinish g1" "?g y = pathstart g2" using assms(4) unfolding assms(3) xy(3) by auto - thus ?thesis using as and inj(1)[of "2 *\<^sub>R x" 1] inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(1,2) - unfolding pathstart_def pathfinish_def joinpaths_def - by auto - next assume as:"x > 1 / 2" "y \ 1 / 2" - hence "?g x \ path_image g2" "?g y \ path_image g1" unfolding path_image_def joinpaths_def - using xy(1,2) by auto - hence "?g x = pathstart g2" "?g y = pathfinish g1" using assms(4) unfolding assms(3) xy(3) by auto - thus ?thesis using as and inj(2)[of "2 *\<^sub>R x - 1" 0] inj(1)[of "2 *\<^sub>R y" 1] and xy(1,2) - unfolding pathstart_def pathfinish_def joinpaths_def - by auto qed qed - -lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join - -subsection {* Reparametrizing a closed curve to start at some chosen point. *} - -definition "shiftpath a (f::real \ 'a::topological_space) = - (\x. if (a + x) \ 1 then f(a + x) else f(a + x - 1))" - -lemma pathstart_shiftpath: "a \ 1 \ pathstart(shiftpath a g) = g a" - unfolding pathstart_def shiftpath_def by auto - -lemma pathfinish_shiftpath: assumes "0 \ a" "pathfinish g = pathstart g" - shows "pathfinish(shiftpath a g) = g a" - using assms unfolding pathstart_def pathfinish_def shiftpath_def - by auto - -lemma endpoints_shiftpath: - assumes "pathfinish g = pathstart g" "a \ {0 .. 1}" - shows "pathfinish(shiftpath a g) = g a" "pathstart(shiftpath a g) = g a" - using assms by(auto intro!:pathfinish_shiftpath pathstart_shiftpath) - -lemma closed_shiftpath: - assumes "pathfinish g = pathstart g" "a \ {0..1}" - shows "pathfinish(shiftpath a g) = pathstart(shiftpath a g)" - using endpoints_shiftpath[OF assms] by auto - -lemma path_shiftpath: - assumes "path g" "pathfinish g = pathstart g" "a \ {0..1}" - shows "path(shiftpath a g)" proof- - have *:"{0 .. 1} = {0 .. 1-a} \ {1-a .. 1}" using assms(3) by auto - have **:"\x. x + a = 1 \ g (x + a - 1) = g (x + a)" - using assms(2)[unfolded pathfinish_def pathstart_def] by auto - show ?thesis unfolding path_def shiftpath_def * apply(rule continuous_on_union) - apply(rule closed_real_atLeastAtMost)+ apply(rule continuous_on_eq[of _ "g \ (\x. a + x)"]) prefer 3 - apply(rule continuous_on_eq[of _ "g \ (\x. a - 1 + x)"]) defer prefer 3 - apply(rule continuous_on_intros)+ prefer 2 apply(rule continuous_on_intros)+ - apply(rule_tac[1-2] continuous_on_subset[OF assms(1)[unfolded path_def]]) - using assms(3) and ** by(auto, auto simp add: field_simps) qed - -lemma shiftpath_shiftpath: assumes "pathfinish g = pathstart g" "a \ {0..1}" "x \ {0..1}" - shows "shiftpath (1 - a) (shiftpath a g) x = g x" - using assms unfolding pathfinish_def pathstart_def shiftpath_def by auto - -lemma path_image_shiftpath: - assumes "a \ {0..1}" "pathfinish g = pathstart g" - shows "path_image(shiftpath a g) = path_image g" proof- - { fix x assume as:"g 1 = g 0" "x \ {0..1::real}" " \y\{0..1} \ {x. \ a + x \ 1}. g x \ g (a + y - 1)" - hence "\y\{0..1} \ {x. a + x \ 1}. g x = g (a + y)" proof(cases "a \ x") - case False thus ?thesis apply(rule_tac x="1 + x - a" in bexI) - using as(1,2) and as(3)[THEN bspec[where x="1 + x - a"]] and assms(1) - by(auto simp add: field_simps atomize_not) next - case True thus ?thesis using as(1-2) and assms(1) apply(rule_tac x="x - a" in bexI) - by(auto simp add: field_simps) qed } - thus ?thesis using assms unfolding shiftpath_def path_image_def pathfinish_def pathstart_def - by(auto simp add: image_iff) qed - -subsection {* Special case of straight-line paths. *} - -definition - linepath :: "'a::real_normed_vector \ 'a \ real \ 'a" where - "linepath a b = (\x. (1 - x) *\<^sub>R a + x *\<^sub>R b)" - -lemma pathstart_linepath[simp]: "pathstart(linepath a b) = a" - unfolding pathstart_def linepath_def by auto - -lemma pathfinish_linepath[simp]: "pathfinish(linepath a b) = b" - unfolding pathfinish_def linepath_def by auto - -lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)" - unfolding linepath_def by (intro continuous_intros) - -lemma continuous_on_linepath[intro]: "continuous_on s (linepath a b)" - using continuous_linepath_at by(auto intro!: continuous_at_imp_continuous_on) - -lemma path_linepath[intro]: "path(linepath a b)" - unfolding path_def by(rule continuous_on_linepath) - -lemma path_image_linepath[simp]: "path_image(linepath a b) = (closed_segment a b)" - unfolding path_image_def segment linepath_def apply (rule set_ext, rule) defer - unfolding mem_Collect_eq image_iff apply(erule exE) apply(rule_tac x="u *\<^sub>R 1" in bexI) - by auto - -lemma reversepath_linepath[simp]: "reversepath(linepath a b) = linepath b a" - unfolding reversepath_def linepath_def by(rule ext, auto) - -lemma injective_path_linepath: - assumes "a \ b" shows "injective_path(linepath a b)" -proof - - { fix x y :: "real" - assume "x *\<^sub>R b + y *\<^sub>R a = x *\<^sub>R a + y *\<^sub>R b" - hence "(x - y) *\<^sub>R a = (x - y) *\<^sub>R b" by (simp add: algebra_simps) - with assms have "x = y" by simp } - thus ?thesis unfolding injective_path_def linepath_def by(auto simp add: algebra_simps) qed - -lemma simple_path_linepath[intro]: "a \ b \ simple_path(linepath a b)" by(auto intro!: injective_imp_simple_path injective_path_linepath) - -subsection {* Bounding a point away from a path. *} - -lemma not_on_path_ball: - fixes g :: "real \ 'a::heine_borel" - assumes "path g" "z \ path_image g" - shows "\e>0. ball z e \ (path_image g) = {}" proof- - obtain a where "a\path_image g" "\y\path_image g. dist z a \ dist z y" - using distance_attains_inf[OF _ path_image_nonempty, of g z] - using compact_path_image[THEN compact_imp_closed, OF assms(1)] by auto - thus ?thesis apply(rule_tac x="dist z a" in exI) using assms(2) by(auto intro!: dist_pos_lt) qed - -lemma not_on_path_cball: - fixes g :: "real \ 'a::heine_borel" - assumes "path g" "z \ path_image g" - shows "\e>0. cball z e \ (path_image g) = {}" proof- - obtain e where "ball z e \ path_image g = {}" "e>0" using not_on_path_ball[OF assms] by auto - moreover have "cball z (e/2) \ ball z e" using `e>0` by auto - ultimately show ?thesis apply(rule_tac x="e/2" in exI) by auto qed - -subsection {* Path component, considered as a "joinability" relation (from Tom Hales). *} - -definition "path_component s x y \ (\g. path g \ path_image g \ s \ pathstart g = x \ pathfinish g = y)" - -lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def - -lemma path_component_mem: assumes "path_component s x y" shows "x \ s" "y \ s" - using assms unfolding path_defs by auto - -lemma path_component_refl: assumes "x \ s" shows "path_component s x x" - unfolding path_defs apply(rule_tac x="\u. x" in exI) using assms - by(auto intro!:continuous_on_intros) - -lemma path_component_refl_eq: "path_component s x x \ x \ s" - by(auto intro!: path_component_mem path_component_refl) - -lemma path_component_sym: "path_component s x y \ path_component s y x" - using assms unfolding path_component_def apply(erule exE) apply(rule_tac x="reversepath g" in exI) - by auto - -lemma path_component_trans: assumes "path_component s x y" "path_component s y z" shows "path_component s x z" - using assms unfolding path_component_def apply- apply(erule exE)+ apply(rule_tac x="g +++ ga" in exI) by(auto simp add: path_image_join) - -lemma path_component_of_subset: "s \ t \ path_component s x y \ path_component t x y" - unfolding path_component_def by auto - -subsection {* Can also consider it as a set, as the name suggests. *} - -lemma path_component_set: "path_component s x = { y. (\g. path g \ path_image g \ s \ pathstart g = x \ pathfinish g = y )}" - apply(rule set_ext) unfolding mem_Collect_eq unfolding mem_def path_component_def by auto - -lemma mem_path_component_set:"x \ path_component s y \ path_component s y x" unfolding mem_def by auto - -lemma path_component_subset: "(path_component s x) \ s" - apply(rule, rule path_component_mem(2)) by(auto simp add:mem_def) - -lemma path_component_eq_empty: "path_component s x = {} \ x \ s" - apply rule apply(drule equals0D[of _ x]) defer apply(rule equals0I) unfolding mem_path_component_set - apply(drule path_component_mem(1)) using path_component_refl by auto - -subsection {* Path connectedness of a space. *} - -definition "path_connected s \ (\x\s. \y\s. \g. path g \ (path_image g) \ s \ pathstart g = x \ pathfinish g = y)" - -lemma path_connected_component: "path_connected s \ (\x\s. \y\s. path_component s x y)" - unfolding path_connected_def path_component_def by auto - -lemma path_connected_component_set: "path_connected s \ (\x\s. path_component s x = s)" - unfolding path_connected_component apply(rule, rule, rule, rule path_component_subset) - unfolding subset_eq mem_path_component_set Ball_def mem_def by auto - -subsection {* Some useful lemmas about path-connectedness. *} - -lemma convex_imp_path_connected: - fixes s :: "'a::real_normed_vector set" - assumes "convex s" shows "path_connected s" - unfolding path_connected_def apply(rule,rule,rule_tac x="linepath x y" in exI) - unfolding path_image_linepath using assms[unfolded convex_contains_segment] by auto - -lemma path_connected_imp_connected: assumes "path_connected s" shows "connected s" - unfolding connected_def not_ex apply(rule,rule,rule ccontr) unfolding not_not apply(erule conjE)+ proof- - fix e1 e2 assume as:"open e1" "open e2" "s \ e1 \ e2" "e1 \ e2 \ s = {}" "e1 \ s \ {}" "e2 \ s \ {}" - then obtain x1 x2 where obt:"x1\e1\s" "x2\e2\s" by auto - then obtain g where g:"path g" "path_image g \ s" "pathstart g = x1" "pathfinish g = x2" - using assms[unfolded path_connected_def,rule_format,of x1 x2] by auto - have *:"connected {0..1::real}" by(auto intro!: convex_connected convex_real_interval) - have "{0..1} \ {x \ {0..1}. g x \ e1} \ {x \ {0..1}. g x \ e2}" using as(3) g(2)[unfolded path_defs] by blast - moreover have "{x \ {0..1}. g x \ e1} \ {x \ {0..1}. g x \ e2} = {}" using as(4) g(2)[unfolded path_defs] unfolding subset_eq by auto - moreover have "{x \ {0..1}. g x \ e1} \ {} \ {x \ {0..1}. g x \ e2} \ {}" using g(3,4)[unfolded path_defs] using obt - by (simp add: ex_in_conv [symmetric], metis zero_le_one order_refl) - ultimately show False using *[unfolded connected_local not_ex,rule_format, of "{x\{0..1}. g x \ e1}" "{x\{0..1}. g x \ e2}"] - using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(1)] - using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)] by auto qed - -lemma open_path_component: - fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*) - assumes "open s" shows "open(path_component s x)" - unfolding open_contains_ball proof - fix y assume as:"y \ path_component s x" - hence "y\s" apply- apply(rule path_component_mem(2)) unfolding mem_def by auto - then obtain e where e:"e>0" "ball y e \ s" using assms[unfolded open_contains_ball] by auto - show "\e>0. ball y e \ path_component s x" apply(rule_tac x=e in exI) apply(rule,rule `e>0`,rule) unfolding mem_ball mem_path_component_set proof- - fix z assume "dist y z < e" thus "path_component s x z" apply(rule_tac path_component_trans[of _ _ y]) defer - apply(rule path_component_of_subset[OF e(2)]) apply(rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) using `e>0` - using as[unfolded mem_def] by auto qed qed - -lemma open_non_path_component: - fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*) - assumes "open s" shows "open(s - path_component s x)" - unfolding open_contains_ball proof - fix y assume as:"y\s - path_component s x" - then obtain e where e:"e>0" "ball y e \ s" using assms[unfolded open_contains_ball] by auto - show "\e>0. ball y e \ s - path_component s x" apply(rule_tac x=e in exI) apply(rule,rule `e>0`,rule,rule) defer proof(rule ccontr) - fix z assume "z\ball y e" "\ z \ path_component s x" - hence "y \ path_component s x" unfolding not_not mem_path_component_set using `e>0` - apply- apply(rule path_component_trans,assumption) apply(rule path_component_of_subset[OF e(2)]) - apply(rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) by auto - thus False using as by auto qed(insert e(2), auto) qed - -lemma connected_open_path_connected: - fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*) - assumes "open s" "connected s" shows "path_connected s" - unfolding path_connected_component_set proof(rule,rule,rule path_component_subset, rule) - fix x y assume "x \ s" "y \ s" show "y \ path_component s x" proof(rule ccontr) - assume "y \ path_component s x" moreover - have "path_component s x \ s \ {}" using `x\s` path_component_eq_empty path_component_subset[of s x] by auto - ultimately show False using `y\s` open_non_path_component[OF assms(1)] open_path_component[OF assms(1)] - using assms(2)[unfolded connected_def not_ex, rule_format, of"path_component s x" "s - path_component s x"] by auto -qed qed - -lemma path_connected_continuous_image: - assumes "continuous_on s f" "path_connected s" shows "path_connected (f ` s)" - unfolding path_connected_def proof(rule,rule) - fix x' y' assume "x' \ f ` s" "y' \ f ` s" - then obtain x y where xy:"x\s" "y\s" "x' = f x" "y' = f y" by auto - guess g using assms(2)[unfolded path_connected_def,rule_format,OF xy(1,2)] .. - thus "\g. path g \ path_image g \ f ` s \ pathstart g = x' \ pathfinish g = y'" - unfolding xy apply(rule_tac x="f \ g" in exI) unfolding path_defs - using assms(1) by(auto intro!: continuous_on_compose continuous_on_subset[of _ _ "g ` {0..1}"]) qed - -lemma homeomorphic_path_connectedness: - "s homeomorphic t \ (path_connected s \ path_connected t)" - unfolding homeomorphic_def homeomorphism_def apply(erule exE|erule conjE)+ apply rule - apply(drule_tac f=f in path_connected_continuous_image) prefer 3 - apply(drule_tac f=g in path_connected_continuous_image) by auto - -lemma path_connected_empty: "path_connected {}" - unfolding path_connected_def by auto - -lemma path_connected_singleton: "path_connected {a}" - unfolding path_connected_def pathstart_def pathfinish_def path_image_def - apply (clarify, rule_tac x="\x. a" in exI, simp add: image_constant_conv) - apply (simp add: path_def continuous_on_const) - done - -lemma path_connected_Un: assumes "path_connected s" "path_connected t" "s \ t \ {}" - shows "path_connected (s \ t)" unfolding path_connected_component proof(rule,rule) - fix x y assume as:"x \ s \ t" "y \ s \ t" - from assms(3) obtain z where "z \ s \ t" by auto - thus "path_component (s \ t) x y" using as using assms(1-2)[unfolded path_connected_component] apply- - apply(erule_tac[!] UnE)+ apply(rule_tac[2-3] path_component_trans[of _ _ z]) - by(auto simp add:path_component_of_subset [OF Un_upper1] path_component_of_subset[OF Un_upper2]) qed - -subsection {* sphere is path-connected. *} - -lemma path_connected_punctured_universe: - 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)" - let ?A = "\k. {x::real^'n. \i\{1..k}. inner (basis (\ i)) x \ 0}" - have "\k\{2..CARD('n)}. path_connected (?A k)" proof - have *:"\k. ?A (Suc k) = {x. inner (?basis (Suc k)) x < 0} \ {x. inner (?basis (Suc k)) x > 0} \ ?A k" apply(rule set_ext,rule) defer - apply(erule UnE)+ unfolding mem_Collect_eq apply(rule_tac[1-2] x="Suc k" in bexI) - by(auto elim!: ballE simp add: not_less le_Suc_eq) - fix k assume "k \ {2..CARD('n)}" thus "path_connected (?A k)" proof(induct k) - case (Suc k) show ?case proof(cases "k = 1") - case False from Suc have d:"k \ {1..CARD('n)}" "Suc k \ {1..CARD('n)}" by auto - hence "\ k \ \ (Suc k)" using \[unfolded bij_betw_def inj_on_def, THEN conjunct1, THEN bspec[where x=k]] by auto - hence **:"?basis k + ?basis (Suc k) \ {x. 0 < inner (?basis (Suc k)) x} \ (?A k)" - "?basis k - ?basis (Suc k) \ {x. 0 > inner (?basis (Suc k)) x} \ ({x. 0 < inner (?basis (Suc k)) x} \ (?A k))" using d - by(auto simp add: inner_basis intro!:bexI[where x=k]) - show ?thesis unfolding * Un_assoc apply(rule path_connected_Un) defer apply(rule path_connected_Un) - prefer 5 apply(rule_tac[1-2] convex_imp_path_connected, rule convex_halfspace_lt, rule convex_halfspace_gt) - apply(rule Suc(1)) using d ** False by auto - next case True hence d:"1\{1..CARD('n)}" "2\{1..CARD('n)}" using Suc(2) by auto - have ***:"Suc 1 = 2" by auto - have **:"\s t P Q. s \ t \ {x. P x \ Q x} = (s \ {x. P x}) \ (t \ {x. Q x})" by auto - have nequals0I:"\x A. x\A \ A \ {}" by auto - have "\ 2 \ \ (Suc 0)" using \[unfolded bij_betw_def inj_on_def, THEN conjunct1, THEN bspec[where x=2]] using assms by auto - thus ?thesis unfolding * True unfolding ** neq_iff bex_disj_distrib apply - - apply(rule path_connected_Un, rule_tac[1-2] path_connected_Un) defer 3 apply(rule_tac[1-4] convex_imp_path_connected) - apply(rule_tac[5] x=" ?basis 1 + ?basis 2" in nequals0I) - apply(rule_tac[6] x="-?basis 1 + ?basis 2" in nequals0I) - apply(rule_tac[7] x="-?basis 1 - ?basis 2" in nequals0I) - using d unfolding *** by(auto intro!: convex_halfspace_gt convex_halfspace_lt, auto simp add: inner_basis) - qed qed auto qed note lem = this - - have ***:"\x::real^'n. (\i\{1..CARD('n)}. inner (basis (\ i)) x \ 0) \ (\i. inner (basis i) x \ 0)" - apply rule apply(erule bexE) apply(rule_tac x="\ i" in exI) defer apply(erule exE) proof- - fix x::"real^'n" and i assume as:"inner (basis i) x \ 0" - have "i\\ ` {1..CARD('n)}" using \[unfolded bij_betw_def, THEN conjunct2] by auto - then obtain j where "j\{1..CARD('n)}" "\ j = i" by auto - thus "\i\{1..CARD('n)}. inner (basis (\ i)) x \ 0" apply(rule_tac x=j in bexI) using as by auto qed auto - have *:"?U - {a} = (\x. x + a) ` {x. x \ 0}" apply(rule set_ext) unfolding image_iff - apply rule apply(rule_tac x="x - a" in bexI) by auto - have **:"\x::real^'n. x\0 \ (\i. inner (basis i) x \ 0)" unfolding Cart_eq by(auto simp add: inner_basis) - 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. 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 - qed(auto intro!:path_connected_singleton) next - case False hence *:"{x::real^'n. norm(x - a) = r} = (\x. a + r *\<^sub>R x) ` {x. norm x = 1}" unfolding not_le apply -apply(rule set_ext,rule) - unfolding image_iff apply(rule_tac x="(1/r) *\<^sub>R (x - a)" in bexI) unfolding mem_Collect_eq norm_scaleR by (auto simp add: scaleR_right_diff_distrib) - have **:"{x::real^'n. norm x = 1} = (\x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" apply(rule set_ext,rule) - unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto split:split_if_asm) - have "continuous_on (UNIV - {0}) (\x::real^'n. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within - apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within) - apply(rule continuous_at_norm[unfolded o_def]) by auto - thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms] - by(auto intro!: path_connected_continuous_image continuous_on_intros) qed - -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 16736dde54c0 -r 6ed6112f0a95 src/HOL/Multivariate_Analysis/Derivative.thy --- a/src/HOL/Multivariate_Analysis/Derivative.thy Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy Mon May 03 07:59:51 2010 +0200 @@ -6,7 +6,7 @@ header {* Multivariate calculus in Euclidean space. *} theory Derivative -imports Brouwer_Fixpoint Vec1 RealVector +imports Brouwer_Fixpoint Vec1 RealVector Operator_Norm begin @@ -31,14 +31,14 @@ assume ?l note as = this[unfolded deriv_def LIM_def,rule_format] show ?r unfolding has_derivative_def Lim_at apply- apply(rule,rule mult.bounded_linear_right) apply safe apply(drule as,safe) apply(rule_tac x=s in exI) apply safe - apply(erule_tac x="xa - x" in allE) unfolding vector_dist_norm netlimit_at[of x] unfolding diff_0_right norm_scaleR + apply(erule_tac x="xa - x" in allE) unfolding dist_norm netlimit_at[of x] unfolding diff_0_right norm_scaleR by(auto simp add:field_simps) next assume ?r note this[unfolded has_derivative_def Lim_at] note as=conjunct2[OF this,rule_format] have *:"\x xa f'. xa \ 0 \ \(f (xa + x) - f x) / xa - f'\ = \(f (xa + x) - f x) - xa * f'\ / \xa\" by(auto simp add:field_simps) show ?l unfolding deriv_def LIM_def apply safe apply(drule as,safe) apply(rule_tac x=d in exI,safe) apply(erule_tac x="xa + x" in allE) - unfolding vector_dist_norm diff_0_right norm_scaleR - unfolding vector_dist_norm netlimit_at[of x] by(auto simp add:algebra_simps *) qed + unfolding dist_norm diff_0_right norm_scaleR + unfolding dist_norm netlimit_at[of x] by(auto simp add:algebra_simps *) qed lemma FDERIV_conv_has_derivative:"FDERIV f (x::'a::{real_normed_vector,perfect_space}) :> f' = (f has_derivative f') (at x)" (is "?l = ?r") proof assume ?l note as = this[unfolded fderiv_def] @@ -48,14 +48,14 @@ thus "\d>0. \xa. 0 < dist xa x \ dist xa x < d \ dist ((1 / norm (xa - netlimit (at x))) *\<^sub>R (f xa - (f (netlimit (at x)) + f' (xa - netlimit (at x))))) (0) < e" apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa - x" in allE) - unfolding vector_dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq) qed next + unfolding dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq) qed next assume ?r note as = this[unfolded has_derivative_def] show ?l unfolding fderiv_def LIM_def apply-apply(rule,rule as[THEN conjunct1]) proof(rule,rule) fix e::real assume "e>0" guess d using as[THEN conjunct2,unfolded Lim_at,rule_format,OF`e>0`] .. thus "\s>0. \xa. xa \ 0 \ dist xa 0 < s \ dist (norm (f (x + xa) - f x - f' xa) / norm xa) 0 < e" apply- apply(rule_tac x=d in exI) apply(erule conjE,rule,assumption) apply rule apply(erule_tac x="xa + x" in allE) - unfolding vector_dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq add.commute) qed qed + unfolding dist_norm netlimit_at[of x] by (auto simp add: diff_diff_eq add.commute) qed qed subsection {* These are the only cases we'll care about, probably. *} @@ -73,7 +73,7 @@ "(f has_derivative f')(at x within s) \ bounded_linear f' \ (\e>0. \d>0. \x'\s. 0 < norm(x' - x) \ norm(x' - x) < d \ norm(f x' - f x - f'(x' - x)) / norm(x' - x) < e)" - unfolding has_derivative_within Lim_within vector_dist_norm + unfolding has_derivative_within Lim_within dist_norm unfolding diff_0_right norm_mul by (simp add: diff_diff_eq) lemma has_derivative_at': @@ -216,7 +216,7 @@ using assms[unfolded has_derivative_def Lim] by auto thus "eventually (\x. dist (1 / norm (x - netlimit net) * (c x $ k - (c (netlimit net) $ k + c' (x - netlimit net) $ k))) 0 < e) net" proof (rule eventually_elim1) - case goal1 thus ?case apply - unfolding vector_dist_norm apply(rule le_less_trans) prefer 2 apply assumption unfolding * ** and norm_vec1 + case goal1 thus ?case apply - unfolding dist_norm apply(rule le_less_trans) prefer 2 apply assumption unfolding * ** and norm_vec1 using component_le_norm[of "(1 / norm (x - netlimit net)) *\<^sub>R (c x - (c (netlimit net) + c' (x - netlimit net))) - 0" k] by auto qed qed(insert assms[unfolded has_derivative_def], auto simp add:linear_conv_bounded_linear) qed @@ -326,7 +326,7 @@ lemma Lim_mul_norm_within: fixes f::"'a::real_normed_vector \ 'b::real_normed_vector" shows "(f ---> 0) (at a within s) \ ((\x. norm(x - a) *\<^sub>R f(x)) ---> 0) (at a within s)" unfolding Lim_within apply(rule,rule) apply(erule_tac x=e in allE,erule impE,assumption,erule exE,erule conjE) - apply(rule_tac x="min d 1" in exI) apply rule defer apply(rule,erule_tac x=x in ballE) unfolding vector_dist_norm diff_0_right norm_mul + apply(rule_tac x="min d 1" in exI) apply rule defer apply(rule,erule_tac x=x in ballE) unfolding dist_norm diff_0_right norm_mul by(auto intro!: mult_strict_mono[of _ "1::real", unfolded mult_1_left]) lemma differentiable_imp_continuous_within: assumes "f differentiable (at x within s)" @@ -339,7 +339,7 @@ apply(rule continuous_within_compose) apply(rule continuous_intros)+ by(rule linear_continuous_within[OF f'[THEN conjunct1]]) show ?thesis unfolding continuous_within using f'[THEN conjunct2, THEN Lim_mul_norm_within] - apply-apply(drule Lim_add) apply(rule **[unfolded continuous_within]) unfolding Lim_within and vector_dist_norm + apply-apply(drule Lim_add) apply(rule **[unfolded continuous_within]) unfolding Lim_within and dist_norm apply(rule,rule) apply(erule_tac x=e in allE) apply(erule impE|assumption)+ apply(erule exE,rule_tac x=d in exI) by(auto simp add:zero * elim!:allE) qed @@ -379,13 +379,13 @@ show "norm (f y - f x - f' (y - x)) \ e * norm (y - x)" proof(cases "y=x") case True thus ?thesis using `bounded_linear f'` by(auto simp add: zero) next case False hence "norm (f y - (f x + f' (y - x))) < e * norm (y - x)" using as(4)[rule_format, OF `y\s`] - unfolding vector_dist_norm diff_0_right norm_mul using as(3) - using pos_divide_less_eq[OF False[unfolded dist_nz], unfolded vector_dist_norm] + unfolding dist_norm diff_0_right norm_mul using as(3) + using pos_divide_less_eq[OF False[unfolded dist_nz], unfolded dist_norm] by (auto simp add: linear_0 linear_sub) thus ?thesis by(auto simp add:algebra_simps) qed qed next assume ?rhs thus ?lhs unfolding has_derivative_within Lim_within apply-apply(erule conjE,rule,assumption) apply(rule,erule_tac x="e/2" in allE,rule,erule impE) defer apply(erule exE,rule_tac x=d in exI) - apply(erule conjE,rule,assumption,rule,rule) unfolding vector_dist_norm diff_0_right norm_scaleR + apply(erule conjE,rule,assumption,rule,rule) unfolding dist_norm diff_0_right norm_scaleR apply(erule_tac x=xa in ballE,erule impE) proof- fix e d y assume "bounded_linear f'" "0 < e" "0 < d" "y \ s" "0 < norm (y - x) \ norm (y - x) < d" "norm (f y - f x - f' (y - x)) \ e / 2 * norm (y - x)" @@ -513,7 +513,7 @@ guess a using UNIV_witness[where 'a='a] .. fix e::real assume "00`,of a] .. thus "\x'\s. x' \ x \ dist x' x < e" apply(rule_tac x="x + d*\<^sub>R basis a" in bexI) - using basis_nonzero[of a] norm_basis[of a] unfolding vector_dist_norm by auto qed + using basis_nonzero[of a] norm_basis[of a] unfolding dist_norm by auto qed hence *:"netlimit (at x within s) = x" apply-apply(rule netlimit_within) unfolding trivial_limit_within by simp show ?thesis apply(rule linear_eq_stdbasis) unfolding linear_conv_bounded_linear apply(rule as(1,2)[THEN conjunct1])+ proof(rule,rule ccontr) @@ -526,7 +526,7 @@ also have "\ = norm ((1 / abs c) *\<^sub>R (c *\<^sub>R (- (f' (basis i)) + f'' (basis i))))" unfolding f'.scaleR f''.scaleR unfolding scaleR_right_distrib scaleR_minus_right by auto also have "\ = e" unfolding e_def norm_mul using c[THEN conjunct1] using norm_minus_cancel[of "f' (basis i) - f'' (basis i)"] by (auto simp add: add.commute ab_diff_minus) - 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 + finally show False using c using d[THEN conjunct2,rule_format,of "x + c *\<^sub>R basis i"] using norm_basis[of i] unfolding 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 \ real^'b" @@ -607,7 +607,7 @@ unfolding vector_component_simps matrix_vector_mul_component unfolding smult_conv_scaleR[symmetric] unfolding inner_simps dot_basis smult_conv_scaleR by simp } note * = this have "x + d *\<^sub>R basis j \ ball x e" "x - d *\<^sub>R basis j \ ball x e" - unfolding mem_ball vector_dist_norm using norm_basis[of j] d by auto + unfolding mem_ball dist_norm using norm_basis[of j] d by auto hence **:"((f (x - d *\<^sub>R basis j))$k \ (f x)$k \ (f (x + d *\<^sub>R basis j))$k \ (f x)$k) \ ((f (x - d *\<^sub>R basis j))$k \ (f x)$k \ (f (x + d *\<^sub>R basis j))$k \ (f x)$k)" using assms(2) by auto have ***:"\y y1 y2 d dx::real. (y1\y\y2\y) \ (y\y1\y\y2) \ d < abs dx \ abs(y1 - y - - dx) \ d \ (abs (y2 - y - dx) \ d) \ False" by arith @@ -787,14 +787,14 @@ guess d2 using assms(5)[unfolded open_dist,rule_format,OF assms(6)] .. note d2=this guess d using real_lbound_gt_zero[OF d1[THEN conjunct1] d2[THEN conjunct1]] .. note d=this thus ?case apply(rule_tac x=d in exI) apply rule defer proof(rule,rule) - fix z assume as:"norm (z - y) < d" hence "z\t" using d2 d unfolding vector_dist_norm by auto + fix z assume as:"norm (z - y) < d" hence "z\t" using d2 d unfolding dist_norm by auto have "norm (g z - g y - g' (z - y)) \ norm (g' (f (g z) - y - f' (g z - g y)))" unfolding g'.diff f'.diff unfolding assms(3)[unfolded o_def id_def, THEN fun_cong] unfolding assms(7)[rule_format,OF `z\t`] apply(subst norm_minus_cancel[THEN sym]) by auto also have "\ \ norm(f (g z) - y - f' (g z - g y)) * C" by(rule C[THEN conjunct2,rule_format]) also have "\ \ (e / C) * norm (g z - g y) * C" apply(rule mult_right_mono) apply(rule d0[THEN conjunct2,rule_format,unfolded assms(7)[rule_format,OF `y\t`]]) apply(cases "z=y") defer - apply(rule d1[THEN conjunct2, unfolded vector_dist_norm,rule_format]) using as d C d0 by auto + apply(rule d1[THEN conjunct2, unfolded dist_norm,rule_format]) using as d C d0 by auto also have "\ \ e * norm (g z - g y)" using C by(auto simp add:field_simps) finally show "norm (g z - g y - g' (z - y)) \ e * norm (g z - g y)" by simp qed auto qed have *:"(0::real) < 1 / 2" by auto guess d using lem1[rule_format,OF *] .. note d=this def B\"C*2" @@ -882,36 +882,36 @@ apply(rule continuous_on_intros linear_continuous_on[OF assms(5)])+ apply(rule continuous_on_subset[OF assms(2)]) apply(rule,unfold image_iff,erule bexE) proof- fix y z assume as:"y \cball (f x) e" "z = x + (g' y - g' (f x))" - have "dist x z = norm (g' (f x) - g' y)" unfolding as(2) and vector_dist_norm by auto + have "dist x z = norm (g' (f x) - g' y)" unfolding as(2) and dist_norm by auto also have "\ \ norm (f x - y) * B" unfolding g'.diff[THEN sym] using B by auto - also have "\ \ e * B" using as(1)[unfolded mem_cball vector_dist_norm] using B by auto + also have "\ \ e * B" using as(1)[unfolded mem_cball dist_norm] using B by auto also have "\ \ e1" using e unfolding less_divide_eq using B by auto finally have "z\cball x e1" unfolding mem_cball by force thus "z \ s" using e1 assms(7) by auto qed next fix y z assume as:"y \ cball (f x) (e / 2)" "z \ cball (f x) e" have "norm (g' (z - f x)) \ norm (z - f x) * B" using B by auto - also have "\ \ e * B" apply(rule mult_right_mono) using as(2)[unfolded mem_cball vector_dist_norm] and B unfolding norm_minus_commute by auto + also have "\ \ e * B" apply(rule mult_right_mono) using as(2)[unfolded mem_cball dist_norm] and B unfolding norm_minus_commute by auto also have "\ < e0" using e and B unfolding less_divide_eq by auto finally have *:"norm (x + g' (z - f x) - x) < e0" by auto have **:"f x + f' (x + g' (z - f x) - x) = z" using assms(6)[unfolded o_def id_def,THEN cong] by auto have "norm (f x - (y + (z - f (x + g' (z - f x))))) \ norm (f (x + g' (z - f x)) - z) + norm (f x - y)" using norm_triangle_ineq[of "f (x + g'(z - f x)) - z" "f x - y"] by(auto simp add:algebra_simps) also have "\ \ 1 / (B * 2) * norm (g' (z - f x)) + norm (f x - y)" using e0[THEN conjunct2,rule_format,OF *] unfolding algebra_simps ** by auto - also have "\ \ 1 / (B * 2) * norm (g' (z - f x)) + e/2" using as(1)[unfolded mem_cball vector_dist_norm] by auto + also have "\ \ 1 / (B * 2) * norm (g' (z - f x)) + e/2" using as(1)[unfolded mem_cball dist_norm] by auto also have "\ \ 1 / (B * 2) * B * norm (z - f x) + e/2" using * and B by(auto simp add:field_simps) also have "\ \ 1 / 2 * norm (z - f x) + e/2" by auto - also have "\ \ e/2 + e/2" apply(rule add_right_mono) using as(2)[unfolded mem_cball vector_dist_norm] unfolding norm_minus_commute by auto - finally show "y + (z - f (x + g' (z - f x))) \ cball (f x) e" unfolding mem_cball vector_dist_norm by auto + also have "\ \ e/2 + e/2" apply(rule add_right_mono) using as(2)[unfolded mem_cball dist_norm] unfolding norm_minus_commute by auto + finally show "y + (z - f (x + g' (z - f x))) \ cball (f x) e" unfolding mem_cball dist_norm by auto qed(insert e, auto) note lem = this show ?thesis unfolding mem_interior apply(rule_tac x="e/2" in exI) apply(rule,rule divide_pos_pos) prefer 3 proof fix y assume "y \ ball (f x) (e/2)" hence *:"y\cball (f x) (e/2)" by auto guess z using lem[rule_format,OF *] .. note z=this hence "norm (g' (z - f x)) \ norm (z - f x) * B" using B by(auto simp add:field_simps) - also have "\ \ e * B" apply(rule mult_right_mono) using z(1) unfolding mem_cball vector_dist_norm norm_minus_commute using B by auto + also have "\ \ e * B" apply(rule mult_right_mono) using z(1) unfolding mem_cball dist_norm norm_minus_commute using B by auto also have "\ \ e1" using e B unfolding less_divide_eq by auto finally have "x + g'(z - f x) \ t" apply- apply(rule e1[THEN conjunct2,unfolded subset_eq,rule_format]) - unfolding mem_cball vector_dist_norm by auto + unfolding mem_cball dist_norm by auto thus "y \ f ` t" using z by auto qed(insert e, auto) qed text {* Hence the following eccentric variant of the inverse function theorem. *) @@ -1059,9 +1059,9 @@ show " \M. \m\M. \n\M. dist (f m x) (f n x) < e" apply(rule_tac x="max M N" in exI) proof(default+) fix m n assume as:"max M N \m" "max M N\n" have "dist (f m x) (f n x) \ norm (f m x0 - f n x0) + norm (f m x - f n x - (f m x0 - f n x0))" - unfolding vector_dist_norm by(rule norm_triangle_sub) + unfolding dist_norm by(rule norm_triangle_sub) also have "\ \ norm (f m x0 - f n x0) + e / 2" using N[rule_format,OF _ _ `x\s` `x0\s`, of m n] and as and False by auto - also have "\ < e / 2 + e / 2" apply(rule add_strict_right_mono) using as and M[rule_format] unfolding vector_dist_norm by auto + also have "\ < e / 2 + e / 2" apply(rule add_strict_right_mono) using as and M[rule_format] unfolding dist_norm by auto finally show "dist (f m x) (f n x) < e" by auto qed qed qed qed then guess g .. note g = this have lem2:"\e>0. \N. \n\N. \x\s. \y\s. norm((f n x - f n y) - (g x - g y)) \ e * norm(x - y)" proof(rule,rule) @@ -1085,12 +1085,12 @@ case False hence *:"e / 2 / norm u > 0" using `e>0` by(auto intro!: divide_pos_pos) guess N using assms(3)[rule_format,OF *] .. note N=this show ?thesis apply(rule_tac x=N in exI) proof(rule,rule) case goal1 - show ?case unfolding vector_dist_norm using N[rule_format,OF goal1 `x\s`, of u] False `e>0` + show ?case unfolding dist_norm using N[rule_format,OF goal1 `x\s`, of u] False `e>0` by (auto simp add:field_simps) qed qed qed show "bounded_linear (g' x)" unfolding linear_linear linear_def apply(rule,rule,rule) defer proof(rule,rule) fix x' y z::"real^'m" and c::real note lin = assms(2)[rule_format,OF `x\s`,THEN derivative_linear] - show "g' x (c *s x') = c *s g' x x'" apply(rule Lim_unique[OF trivial_limit_sequentially]) + show "g' x (c *\<^sub>R x') = c *\<^sub>R g' x x'" apply(rule Lim_unique[OF trivial_limit_sequentially]) apply(rule lem3[rule_format]) unfolding smult_conv_scaleR unfolding lin[unfolded bounded_linear_def bounded_linear_axioms_def,THEN conjunct2,THEN conjunct1,rule_format] apply(rule Lim_cmul) by(rule lem3[rule_format]) @@ -1184,9 +1184,9 @@ apply(rule mult_mono) using B C D by (auto simp add: field_simps intro!:mult_nonneg_nonneg) also have "\ = (B * C * D * norm (y - x)) * norm (y - x)" by(auto simp add:field_simps) also have "\ < e * norm (y - x)" apply(rule mult_strict_right_mono) - using as(3)[unfolded vector_dist_norm] and as(2) unfolding pos_less_divide_eq[OF bcd] by (auto simp add:field_simps) + using as(3)[unfolded dist_norm] and as(2) unfolding pos_less_divide_eq[OF bcd] by (auto simp add:field_simps) finally show "dist ((1 / norm (y - x)) *\<^sub>R h (f' (y - x)) (g' (y - x))) 0 < e" - unfolding vector_dist_norm apply-apply(cases "y = x") by(auto simp add:field_simps) qed qed + unfolding dist_norm apply-apply(cases "y = x") by(auto simp add:field_simps) qed qed have "bounded_linear (\d. h (f x) (g' d) + h (f' d) (g x))" unfolding linear_linear linear_def unfolding smult_conv_scaleR unfolding g'.add f'.scaleR f'.add g'.scaleR unfolding h.add_right h.add_left scaleR_right_distrib h.scaleR_left h.scaleR_right by auto diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Mon May 03 07:59:51 2010 +0200 @@ -421,7 +421,7 @@ qed lemma det_row_span: - fixes A :: "'a:: linordered_idom^'n^'n" + fixes A :: "real^'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- @@ -450,7 +450,7 @@ ultimately show ?thesis apply - - apply (rule span_induct_alt[of ?P ?S, OF P0]) + apply (rule span_induct_alt[of ?P ?S, OF P0, folded smult_conv_scaleR]) apply blast apply (rule x) done @@ -462,7 +462,7 @@ (* ------------------------------------------------------------------------- *) lemma det_dependent_rows: - fixes A:: "'a::linordered_idom^'n^'n" + fixes A:: "real^'n^'n" assumes d: "dependent (rows A)" shows "det A = 0" proof- @@ -483,12 +483,12 @@ from det_row_span[OF th0] have "det A = det (\ k. if k = i then 0 *s 1 else row k A)" unfolding right_minus vector_smult_lzero .. - with det_row_mul[of i "0::'a" "\i. 1"] + with det_row_mul[of i "0::real" "\i. 1"] have "det A = 0" by simp} ultimately show ?thesis by blast qed -lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::linordered_idom^'n^'n))" shows "det A = 0" +lemma det_dependent_columns: assumes d: "dependent(columns (A::real^'n^'n))" shows "det A = 0" by (metis d det_dependent_rows rows_transpose det_transpose) (* ------------------------------------------------------------------------- *) @@ -744,7 +744,7 @@ apply (rule span_setsum) apply simp apply (rule ballI) - apply (rule span_mul)+ + apply (rule span_mul [where 'a="real^'n", folded smult_conv_scaleR])+ apply (rule span_superset) apply auto done @@ -761,9 +761,9 @@ (* ------------------------------------------------------------------------- *) lemma cramer_lemma_transpose: - fixes A:: "'a::linordered_idom^'n^'n" and x :: "'a ^'n" + fixes A:: "real^'n^'n" and x :: "real^'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" + else row i A)::real^'n^'n) = x$k * det A" (is "?lhs = ?rhs") proof- let ?U = "UNIV :: 'n set" @@ -780,7 +780,7 @@ apply (rule det_row_span) apply (rule span_setsum[OF fUk]) apply (rule ballI) - apply (rule span_mul) + apply (rule span_mul [where 'a="real^'n", folded smult_conv_scaleR])+ apply (rule span_superset) apply auto done @@ -797,8 +797,8 @@ qed lemma cramer_lemma: - fixes A :: "'a::linordered_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" + fixes A :: "real^'n^'n" + shows "det((\ i j. if j = k then (A *v x)$i else A$i$j):: real^'n^'n) = x$k * det A" proof- let ?U = "UNIV :: 'n set" have stupid: "\c. setsum (\i. c i *s row i (transpose A)) ?U = setsum (\i. c i *s column i A) ?U" @@ -929,7 +929,7 @@ unfolding dot_norm_neg dist_norm[symmetric] unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)} note fc = this - show ?thesis unfolding linear_def vector_eq smult_conv_scaleR by (simp add: inner_simps fc field_simps) + show ?thesis unfolding linear_def vector_eq[where 'a="real^'n"] smult_conv_scaleR by (simp add: inner_simps fc field_simps) qed lemma isometry_linear: diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon May 03 07:59:51 2010 +0200 @@ -14,48 +14,18 @@ subsection{* Basic componentwise operations on vectors. *} -instantiation cart :: (plus,finite) plus -begin - definition vector_add_def : "op + \ (\ x y. (\ i. (x$i) + (y$i)))" - instance .. -end - instantiation cart :: (times,finite) times begin definition vector_mult_def : "op * \ (\ x y. (\ i. (x$i) * (y$i)))" instance .. end -instantiation cart :: (minus,finite) minus -begin - definition vector_minus_def : "op - \ (\ x y. (\ i. (x$i) - (y$i)))" - instance .. -end - -instantiation cart :: (uminus,finite) uminus -begin - definition vector_uminus_def : "uminus \ (\ x. (\ i. - (x$i)))" - instance .. -end - -instantiation cart :: (zero,finite) zero -begin - definition vector_zero_def : "0 \ (\ i. 0)" - instance .. -end - instantiation cart :: (one,finite) one begin definition vector_one_def : "1 \ (\ i. 1)" instance .. end -instantiation cart :: (scaleR, finite) scaleR -begin - definition vector_scaleR_def: "scaleR = (\ r x. (\ i. scaleR r (x$i)))" - instance .. -end - instantiation cart :: (ord,finite) ord begin definition vector_le_def: @@ -126,24 +96,12 @@ lemma vec_component [simp]: "vec x $ i = x" by (vector vec_def) -lemma vector_add_component [simp]: "(x + y)$i = x$i + y$i" - by vector - -lemma vector_minus_component [simp]: "(x - y)$i = x$i - y$i" - by vector - lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i" by vector lemma vector_smult_component [simp]: "(c *s y)$i = c * (y$i)" by vector -lemma vector_uminus_component [simp]: "(- x)$i = - (x$i)" - by vector - -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 lemmas vector_component = @@ -153,35 +111,6 @@ subsection {* Some frequently useful arithmetic lemmas over vectors. *} -instance cart :: (semigroup_add,finite) semigroup_add - apply (intro_classes) by (vector add_assoc) - -instance cart :: (monoid_add,finite) monoid_add - apply (intro_classes) by vector+ - -instance cart :: (group_add,finite) group_add - apply (intro_classes) by (vector algebra_simps)+ - -instance cart :: (ab_semigroup_add,finite) ab_semigroup_add - apply (intro_classes) by (vector add_commute) - -instance cart :: (comm_monoid_add,finite) comm_monoid_add - apply (intro_classes) by vector - -instance cart :: (ab_group_add,finite) ab_group_add - apply (intro_classes) by vector+ - -instance cart :: (cancel_semigroup_add,finite) cancel_semigroup_add - apply (intro_classes) - by (vector Cart_eq)+ - -instance cart :: (cancel_ab_semigroup_add,finite) cancel_ab_semigroup_add - apply (intro_classes) - by (vector Cart_eq) - -instance cart :: (real_vector, finite) real_vector - by default (vector scaleR_left_distrib scaleR_right_distrib)+ - instance cart :: (semigroup_mult,finite) semigroup_mult apply (intro_classes) by (vector mult_assoc) @@ -197,10 +126,6 @@ instance cart :: (comm_monoid_mult,finite) comm_monoid_mult apply (intro_classes) by vector -fun vector_power where - "vector_power x 0 = 1" - | "vector_power x (Suc n) = x * vector_power x n" - instance cart :: (semiring,finite) semiring apply (intro_classes) by (vector field_simps)+ @@ -237,19 +162,9 @@ apply vector done -lemma zero_index[simp]: - "(0 :: 'a::zero ^'n)$i = 0" by vector - lemma one_index[simp]: "(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- - have "(1::'a) + of_nat n = 0 \ of_nat 1 + of_nat n = (of_nat 0 :: 'a)" by simp - also have "\ \ 1 + n = 0" by (simp only: of_nat_add[symmetric] of_nat_eq_iff) - finally show ?thesis by simp -qed - instance cart :: (semiring_char_0,finite) semiring_char_0 proof (intro_classes) fix m n ::nat @@ -280,325 +195,8 @@ lemma vec_eq[simp]: "(vec m = vec n) \ (m = n)" by (simp add: Cart_eq) -subsection {* Topological space *} - -instantiation cart :: (topological_space, finite) topological_space -begin - -definition open_vector_def: - "open (S :: ('a ^ 'b) set) \ - (\x\S. \A. (\i. open (A i) \ x$i \ A i) \ - (\y. (\i. y$i \ A i) \ y \ S))" - -instance proof - show "open (UNIV :: ('a ^ 'b) set)" - unfolding open_vector_def by auto -next - fix S T :: "('a ^ 'b) set" - assume "open S" "open T" thus "open (S \ T)" - unfolding open_vector_def - apply clarify - apply (drule (1) bspec)+ - apply (clarify, rename_tac Sa Ta) - apply (rule_tac x="\i. Sa i \ Ta i" in exI) - apply (simp add: open_Int) - done -next - fix K :: "('a ^ 'b) set set" - assume "\S\K. open S" thus "open (\K)" - unfolding open_vector_def - apply clarify - apply (drule (1) bspec) - apply (drule (1) bspec) - apply clarify - apply (rule_tac x=A in exI) - apply fast - done -qed - -end - -lemma open_vector_box: "\i. open (S i) \ open {x. \i. x $ i \ S i}" -unfolding open_vector_def by auto - -lemma open_vimage_Cart_nth: "open S \ open ((\x. x $ i) -` S)" -unfolding open_vector_def -apply clarify -apply (rule_tac x="\k. if k = i then S else UNIV" in exI, simp) -done - -lemma closed_vimage_Cart_nth: "closed S \ closed ((\x. x $ i) -` S)" -unfolding closed_open vimage_Compl [symmetric] -by (rule open_vimage_Cart_nth) - -lemma closed_vector_box: "\i. closed (S i) \ closed {x. \i. x $ i \ S i}" -proof - - have "{x. \i. x $ i \ S i} = (\i. (\x. x $ i) -` S i)" by auto - thus "\i. closed (S i) \ closed {x. \i. x $ i \ S i}" - by (simp add: closed_INT closed_vimage_Cart_nth) -qed - -lemma tendsto_Cart_nth [tendsto_intros]: - assumes "((\x. f x) ---> a) net" - shows "((\x. f x $ i) ---> a $ i) net" -proof (rule topological_tendstoI) - fix S assume "open S" "a $ i \ S" - then have "open ((\y. y $ i) -` S)" "a \ ((\y. y $ i) -` S)" - by (simp_all add: open_vimage_Cart_nth) - with assms have "eventually (\x. f x \ (\y. y $ i) -` S) net" - by (rule topological_tendstoD) - then show "eventually (\x. f x $ i \ S) net" - by simp -qed - -subsection {* Metric *} - -(* TODO: move somewhere else *) -lemma finite_choice: "finite A \ \x\A. \y. P x y \ \f. \x\A. P x (f x)" -apply (induct set: finite, simp_all) -apply (clarify, rename_tac y) -apply (rule_tac x="f(x:=y)" in exI, simp) -done - -instantiation cart :: (metric_space, finite) metric_space -begin - -definition dist_vector_def: - "dist (x::'a^'b) (y::'a^'b) = setL2 (\i. dist (x$i) (y$i)) UNIV" - -lemma dist_nth_le: "dist (x $ i) (y $ i) \ dist x y" -unfolding dist_vector_def -by (rule member_le_setL2) simp_all - -instance proof - fix x y :: "'a ^ 'b" - show "dist x y = 0 \ x = y" - unfolding dist_vector_def - by (simp add: setL2_eq_0_iff Cart_eq) -next - fix x y z :: "'a ^ 'b" - show "dist x y \ dist x z + dist y z" - unfolding dist_vector_def - apply (rule order_trans [OF _ setL2_triangle_ineq]) - apply (simp add: setL2_mono dist_triangle2) - done -next - (* FIXME: long proof! *) - fix S :: "('a ^ 'b) set" - show "open S \ (\x\S. \e>0. \y. dist y x < e \ y \ S)" - unfolding open_vector_def open_dist - apply safe - apply (drule (1) bspec) - apply clarify - apply (subgoal_tac "\e>0. \i y. dist y (x$i) < e \ y \ A i") - apply clarify - apply (rule_tac x=e in exI, clarify) - apply (drule spec, erule mp, clarify) - apply (drule spec, drule spec, erule mp) - apply (erule le_less_trans [OF dist_nth_le]) - apply (subgoal_tac "\i\UNIV. \e>0. \y. dist y (x$i) < e \ y \ A i") - apply (drule finite_choice [OF finite], clarify) - apply (rule_tac x="Min (range f)" in exI, simp) - apply clarify - apply (drule_tac x=i in spec, clarify) - apply (erule (1) bspec) - apply (drule (1) bspec, clarify) - apply (subgoal_tac "\r. (\i::'b. 0 < r i) \ e = setL2 r UNIV") - apply clarify - apply (rule_tac x="\i. {y. dist y (x$i) < r i}" in exI) - apply (rule conjI) - apply clarify - apply (rule conjI) - apply (clarify, rename_tac y) - apply (rule_tac x="r i - dist y (x$i)" in exI, rule conjI, simp) - apply clarify - apply (simp only: less_diff_eq) - apply (erule le_less_trans [OF dist_triangle]) - apply simp - apply clarify - apply (drule spec, erule mp) - apply (simp add: dist_vector_def setL2_strict_mono) - apply (rule_tac x="\i. e / sqrt (of_nat CARD('b))" in exI) - apply (simp add: divide_pos_pos setL2_constant) - done -qed - -end - -lemma LIMSEQ_Cart_nth: - "(X ----> a) \ (\n. X n $ i) ----> a $ i" -unfolding LIMSEQ_conv_tendsto by (rule tendsto_Cart_nth) - -lemma LIM_Cart_nth: - "(f -- x --> y) \ (\x. f x $ i) -- x --> y $ i" -unfolding LIM_conv_tendsto by (rule tendsto_Cart_nth) - -lemma Cauchy_Cart_nth: - "Cauchy (\n. X n) \ Cauchy (\n. X n $ i)" -unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_nth_le]) - -lemma LIMSEQ_vector: - fixes X :: "nat \ 'a::metric_space ^ 'n" - assumes X: "\i. (\n. X n $ i) ----> (a $ i)" - shows "X ----> a" -proof (rule metric_LIMSEQ_I) - fix r :: real assume "0 < r" - then have "0 < r / of_nat CARD('n)" (is "0 < ?s") - by (simp add: divide_pos_pos) - def N \ "\i. LEAST N. \n\N. dist (X n $ i) (a $ i) < ?s" - def M \ "Max (range N)" - have "\i. \N. \n\N. dist (X n $ i) (a $ i) < ?s" - using X `0 < ?s` by (rule metric_LIMSEQ_D) - hence "\i. \n\N i. dist (X n $ i) (a $ i) < ?s" - unfolding N_def by (rule LeastI_ex) - hence M: "\i. \n\M. dist (X n $ i) (a $ i) < ?s" - unfolding M_def by simp - { - fix n :: nat assume "M \ n" - have "dist (X n) a = setL2 (\i. dist (X n $ i) (a $ i)) UNIV" - unfolding dist_vector_def .. - also have "\ \ setsum (\i. dist (X n $ i) (a $ i)) UNIV" - by (rule setL2_le_setsum [OF zero_le_dist]) - also have "\ < setsum (\i::'n. ?s) UNIV" - by (rule setsum_strict_mono, simp_all add: M `M \ n`) - also have "\ = r" - by simp - finally have "dist (X n) a < r" . - } - hence "\n\M. dist (X n) a < r" - by simp - then show "\M. \n\M. dist (X n) a < r" .. -qed - -lemma Cauchy_vector: - fixes X :: "nat \ 'a::metric_space ^ 'n" - assumes X: "\i. Cauchy (\n. X n $ i)" - shows "Cauchy (\n. X n)" -proof (rule metric_CauchyI) - fix r :: real assume "0 < r" - then have "0 < r / of_nat CARD('n)" (is "0 < ?s") - by (simp add: divide_pos_pos) - def N \ "\i. LEAST N. \m\N. \n\N. dist (X m $ i) (X n $ i) < ?s" - def M \ "Max (range N)" - have "\i. \N. \m\N. \n\N. dist (X m $ i) (X n $ i) < ?s" - using X `0 < ?s` by (rule metric_CauchyD) - hence "\i. \m\N i. \n\N i. dist (X m $ i) (X n $ i) < ?s" - unfolding N_def by (rule LeastI_ex) - hence M: "\i. \m\M. \n\M. dist (X m $ i) (X n $ i) < ?s" - unfolding M_def by simp - { - fix m n :: nat - assume "M \ m" "M \ n" - have "dist (X m) (X n) = setL2 (\i. dist (X m $ i) (X n $ i)) UNIV" - unfolding dist_vector_def .. - also have "\ \ setsum (\i. dist (X m $ i) (X n $ i)) UNIV" - by (rule setL2_le_setsum [OF zero_le_dist]) - also have "\ < setsum (\i::'n. ?s) UNIV" - by (rule setsum_strict_mono, simp_all add: M `M \ m` `M \ n`) - also have "\ = r" - by simp - finally have "dist (X m) (X n) < r" . - } - hence "\m\M. \n\M. dist (X m) (X n) < r" - by simp - then show "\M. \m\M. \n\M. dist (X m) (X n) < r" .. -qed - -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)" - using Cauchy_Cart_nth [OF `Cauchy X`] - by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) - hence "X ----> Cart_lambda (\i. lim (\n. X n $ i))" - by (simp add: LIMSEQ_vector) - then show "convergent X" - by (rule convergentI) -qed - -subsection {* Norms *} - -instantiation cart :: (real_normed_vector, finite) real_normed_vector -begin - -definition norm_vector_def: - "norm (x::'a^'b) = setL2 (\i. norm (x$i)) UNIV" - -definition vector_sgn_def: - "sgn (x::'a^'b) = scaleR (inverse (norm x)) x" - -instance proof - fix a :: real and x y :: "'a ^ 'b" - show "0 \ norm x" - unfolding norm_vector_def - by (rule setL2_nonneg) - show "norm x = 0 \ x = 0" - unfolding norm_vector_def - by (simp add: setL2_eq_0_iff Cart_eq) - show "norm (x + y) \ norm x + norm y" - unfolding norm_vector_def - apply (rule order_trans [OF _ setL2_triangle_ineq]) - apply (simp add: setL2_mono norm_triangle_ineq) - done - show "norm (scaleR a x) = \a\ * norm x" - unfolding norm_vector_def - by (simp add: setL2_right_distrib) - show "sgn x = scaleR (inverse (norm x)) x" - by (rule vector_sgn_def) - show "dist x y = norm (x - y)" - unfolding dist_vector_def norm_vector_def - by (simp add: dist_norm) -qed - -end - -lemma norm_nth_le: "norm (x $ i) \ norm x" -unfolding norm_vector_def -by (rule member_le_setL2) simp_all - -interpretation Cart_nth: bounded_linear "\x. x $ i" -apply default -apply (rule vector_add_component) -apply (rule vector_scaleR_component) -apply (rule_tac x="1" in exI, simp add: norm_nth_le) -done - -instance cart :: (banach, finite) banach .. - -subsection {* Inner products *} - abbreviation inner_bullet (infix "\" 70) where "x \ y \ inner x y" -instantiation cart :: (real_inner, finite) real_inner -begin - -definition inner_vector_def: - "inner x y = setsum (\i. inner (x$i) (y$i)) UNIV" - -instance proof - fix r :: real and x y z :: "'a ^ 'b" - show "inner x y = inner y x" - unfolding inner_vector_def - by (simp add: inner_commute) - show "inner (x + y) z = inner x z + inner y z" - unfolding inner_vector_def - by (simp add: inner_add_left setsum_addf) - show "inner (scaleR r x) y = r * inner x y" - unfolding inner_vector_def - by (simp add: setsum_right_distrib) - show "0 \ inner x x" - unfolding inner_vector_def - by (simp add: setsum_nonneg) - show "inner x x = 0 \ x = 0" - unfolding inner_vector_def - by (simp add: Cart_eq setsum_nonneg_eq_0_iff) - show "norm x = sqrt (inner x x)" - unfolding inner_vector_def norm_vector_def setL2_def - by (simp add: power2_norm_eq_inner) -qed - -end - subsection {* A connectedness or intermediate value lemma with several applications. *} lemma connected_real_lemma: @@ -701,13 +299,6 @@ text{* Hence derive more interesting properties of the norm. *} -text {* - This type-specific version is only here - to make @{text normarith.ML} happy. -*} -lemma norm_0: "norm (0::real ^ _) = 0" - by (rule norm_zero) - lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x" by (simp add: norm_vector_def setL2_right_distrib abs_mult) @@ -726,15 +317,12 @@ by (metis vector_mul_rcancel) lemma norm_cauchy_schwarz: - fixes x y :: "real ^ 'n" shows "inner x y <= norm x * norm y" using Cauchy_Schwarz_ineq2[of x y] by auto lemma norm_cauchy_schwarz_abs: - fixes x y :: "real ^ 'n" shows "\inner 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) + by (rule Cauchy_Schwarz_ineq2) lemma norm_triangle_sub: fixes x y :: "'a::real_normed_vector" @@ -757,15 +345,15 @@ lemma real_abs_norm: "\norm x\ = norm x" by (rule abs_norm_cancel) -lemma real_abs_sub_norm: "\norm (x::real ^ 'n) - norm y\ <= norm(x - y)" +lemma real_abs_sub_norm: "\norm x - norm y\ <= norm(x - y)" by (rule norm_triangle_ineq3) -lemma norm_le: "norm(x::real ^ 'n) <= norm(y) \ x \ x <= y \ y" +lemma norm_le: "norm(x) <= norm(y) \ x \ x <= y \ y" by (simp add: norm_eq_sqrt_inner) -lemma norm_lt: "norm(x::real ^ 'n) < norm(y) \ x \ x < y \ y" +lemma norm_lt: "norm(x) < norm(y) \ x \ x < y \ y" by (simp add: norm_eq_sqrt_inner) -lemma norm_eq: "norm(x::real ^ 'n) = norm (y::real ^ 'n) \ x \ x = y \ y" +lemma norm_eq: "norm(x) = norm (y) \ x \ x = y \ y" apply(subst order_eq_iff) unfolding norm_le by auto -lemma norm_eq_1: "norm(x::real ^ 'n) = 1 \ x \ x = 1" +lemma norm_eq_1: "norm(x) = 1 \ x \ x = 1" unfolding norm_eq_sqrt_inner by auto text{* Squaring equations and inequalities involving norms. *} @@ -817,9 +405,9 @@ text{* Equality of vectors in terms of @{term "op \"} products. *} -lemma vector_eq: "(x:: real ^ 'n) = y \ x \ x = x \ y\ y \ y = x \ x" (is "?lhs \ ?rhs") +lemma vector_eq: "x = y \ x \ x = x \ y \ y \ y = x \ x" (is "?lhs \ ?rhs") proof - assume "?lhs" then show ?rhs by simp + assume ?lhs then show ?rhs by simp next assume ?rhs then have "x \ x - x \ y = 0 \ x \ y - y \ y = 0" by simp @@ -925,11 +513,6 @@ "x \ y \ \ (norm (x - y) \ 0)" using norm_ge_zero[of "x - y"] by auto -lemma vector_dist_norm: - fixes x :: "'a::real_normed_vector" - shows "dist x y = norm (x - y)" - by (rule dist_norm) - use "normarith.ML" method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac) @@ -941,7 +524,7 @@ lemma dist_triangle_alt: fixes x y z :: "'a::metric_space" shows "dist y z <= dist x y + dist x z" -using dist_triangle [of y z x] by (simp add: dist_commute) +by (rule dist_triangle3) lemma dist_pos_lt: fixes x y :: "'a::metric_space" @@ -976,12 +559,12 @@ lemma norm_triangle_half_r: shows "norm (y - x1) < e / 2 \ norm (y - x2) < e / 2 \ norm (x1 - x2) < e" - using dist_triangle_half_r unfolding vector_dist_norm[THEN sym] by auto + using dist_triangle_half_r unfolding dist_norm[THEN sym] by auto lemma norm_triangle_half_l: assumes "norm (x - y) < e / 2" "norm (x' - (y)) < e / 2" shows "norm (x - x') < e" - using dist_triangle_half_l[OF assms[unfolded vector_dist_norm[THEN sym]]] - unfolding vector_dist_norm[THEN sym] . + using dist_triangle_half_l[OF assms[unfolded dist_norm[THEN sym]]] + unfolding dist_norm[THEN sym] . lemma norm_triangle_le: "norm(x) + norm y <= e ==> norm(x + y) <= e" by (metis order_trans norm_triangle_ineq) @@ -1035,20 +618,6 @@ finally show ?case using "2.hyps" by simp qed -lemma real_setsum_norm: - 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]) - case 1 thus ?case by simp -next - case (2 x S) - from "2.hyps" have "norm (setsum f (insert x S)) \ norm (f x) + norm (setsum f S)" by (simp add: norm_triangle_ineq) - also have "\ \ norm (f x) + setsum (\x. norm(f x)) S" - using "2.hyps" by simp - finally show ?case using "2.hyps" by simp -qed - lemma setsum_norm_le: fixes f :: "'a \ 'b::real_normed_vector" assumes fS: "finite S" @@ -1061,18 +630,6 @@ by arith qed -lemma real_setsum_norm_le: - 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" -proof- - from fg have "setsum (\x. norm(f x)) S <= setsum g S" - by - (rule setsum_mono, simp) - then show ?thesis using real_setsum_norm[OF fS, of f] fg - by arith -qed - lemma setsum_norm_bound: fixes f :: "'a \ 'b::real_normed_vector" assumes fS: "finite S" @@ -1081,16 +638,8 @@ using setsum_norm_le[OF fS K] setsum_constant[symmetric] by simp -lemma real_setsum_norm_bound: - 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" - using real_setsum_norm_le[OF fS K] setsum_constant[symmetric] - by simp - lemma setsum_vmul: - fixes f :: "'a \ 'b::{real_normed_vector,semiring, mult_zero}" + fixes f :: "'a \ 'b::semiring_0" assumes fS: "finite S" shows "setsum f S *s v = setsum (\x. f x *s v) S" proof(induct rule: finite_induct[OF fS]) @@ -1156,10 +705,10 @@ finally show ?thesis . qed -lemma dot_lsum: "finite S \ setsum f S \ (y::'a::{real_inner}^'n) = setsum (\x. f x \ y) S " +lemma dot_lsum: "finite S \ setsum f S \ y = setsum (\x. f x \ y) S " apply(induct rule: finite_induct) by(auto simp add: inner_simps) -lemma dot_rsum: "finite S \ (y::'a::{real_inner}^'n) \ setsum f S = setsum (\x. y \ f x) S " +lemma dot_rsum: "finite S \ y \ setsum f S = setsum (\x. y \ f x) S " apply(induct rule: finite_induct) by(auto simp add: inner_simps) subsection{* Basis vectors in coordinate directions. *} @@ -1204,6 +753,13 @@ "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 smult_conv_scaleR: "c *s x = scaleR c x" + unfolding vector_scalar_mult_def vector_scaleR_def by simp + +lemma basis_expansion': + "setsum (\i. (x$i) *\<^sub>R basis i) UNIV = x" + by (rule basis_expansion [where 'a=real, unfolded smult_conv_scaleR]) + lemma basis_expansion_unique: "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) @@ -1229,23 +785,21 @@ 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::real^'n)" - apply (auto simp add: Cart_eq dot_basis) - apply (erule_tac x="basis i" in allE) - apply (simp add: dot_basis) - apply (subgoal_tac "y = z") - apply simp - apply (simp add: Cart_eq) - done - -lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ x = (y::real^'n)" - apply (auto simp add: Cart_eq dot_basis) - apply (erule_tac x="basis i" in allE) - apply (simp add: dot_basis) - apply (subgoal_tac "x = y") - apply simp - apply (simp add: Cart_eq) - done +lemma vector_eq_ldot: "(\x. x \ y = x \ z) \ y = z" +proof + assume "\x. x \ y = x \ z" + hence "\x. x \ (y - z) = 0" by (simp add: inner_simps) + hence "(y - z) \ (y - z) = 0" .. + thus "y = z" by simp +qed simp + +lemma vector_eq_rdot: "(\z. x \ z = y \ z) \ x = y" +proof + assume "\z. x \ z = y \ z" + hence "\z. (x - y) \ z = 0" by (simp add: inner_simps) + hence "(x - y) \ (x - y) = 0" .. + thus "x = y" by simp +qed simp subsection{* Orthogonality. *} @@ -1259,9 +813,8 @@ shows "orthogonal (basis i :: real^'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::real ^'n)" + "orthogonal a 0" "orthogonal a x ==> orthogonal a (c *\<^sub>R x)" "orthogonal a x ==> orthogonal a (-x)" "orthogonal a x \ orthogonal a y ==> orthogonal a (x + y)" @@ -1273,69 +826,68 @@ "orthogonal x a \ orthogonal y a ==> orthogonal (x - y) a" unfolding orthogonal_def inner_simps by auto -lemma orthogonal_commute: "orthogonal (x::real ^'n)y \ orthogonal y x" +lemma orthogonal_commute: "orthogonal x y \ orthogonal y x" by (simp add: orthogonal_def inner_commute) subsection{* Linear functions. *} -definition "linear f \ (\x y. f(x + y) = f x + f y) \ (\c x. f(c *s x) = c *s f x)" - -lemma linearI: assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *s x) = c *s f x" +definition + linear :: "('a::real_vector \ 'b::real_vector) \ bool" where + "linear f \ (\x y. f(x + y) = f x + f y) \ (\c x. f(c *\<^sub>R x) = c *\<^sub>R f x)" + +lemma linearI: assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" shows "linear f" using assms unfolding linear_def by auto -lemma linear_compose_cmul: "linear f ==> linear (\x. (c::'a::comm_semiring) *s f x)" - by (vector linear_def Cart_eq field_simps) - -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 field_simps) - -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 field_simps) +lemma linear_compose_cmul: "linear f ==> linear (\x. c *\<^sub>R f x)" + by (simp add: linear_def algebra_simps) + +lemma linear_compose_neg: "linear f ==> linear (\x. -(f(x)))" + by (simp add: linear_def) + +lemma linear_compose_add: "linear f \ linear g ==> linear (\x. f(x) + g(x))" + by (simp add: linear_def algebra_simps) + +lemma linear_compose_sub: "linear f \ linear g ==> linear (\x. f x - g x)" + by (simp add: linear_def algebra_simps) lemma linear_compose: "linear f \ linear g ==> linear (g o f)" by (simp add: linear_def) lemma linear_id: "linear id" by (simp add: linear_def id_def) -lemma linear_zero: "linear (\x. 0::'a::semiring_1 ^ 'n)" by (simp add: linear_def) +lemma linear_zero: "linear (\x. 0)" by (simp add: linear_def) lemma linear_compose_setsum: - 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)" + assumes fS: "finite S" and lS: "\a \ S. linear (f a)" + shows "linear(\x. setsum (\a. f a x) 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 \ 'a^'n" assumes lf: "linear f" - shows "linear (\x. f x $ k *s v)" + shows "linear (\x. f x $ k *\<^sub>R v)" using lf - apply (auto simp add: linear_def ) - by (vector field_simps)+ - -lemma linear_0: "linear f ==> f 0 = (0::'a::semiring_1 ^'n)" + by (auto simp add: linear_def algebra_simps) + +lemma linear_0: "linear f ==> f 0 = 0" unfolding linear_def apply clarsimp apply (erule allE[where x="0::'a"]) apply simp done -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 \ _) ==> f (-x) = - f x" - unfolding vector_sneg_minus1 - using linear_cmul[of f] by auto +lemma linear_cmul: "linear f ==> f(c *\<^sub>R x) = c *\<^sub>R f x" by (simp add: linear_def) + +lemma linear_neg: "linear f ==> f (-x) = - f x" + using linear_cmul [where c="-1"] by simp 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 \ _) ==> f(x - y) = f x - f y" +lemma linear_sub: "linear f ==> 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 \ _" 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]) @@ -1350,14 +902,13 @@ qed lemma linear_setsum_mul: - 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] + shows "f (setsum (\i. c i *\<^sub>R v i) S) = setsum (\i. c i *\<^sub>R f (v i)) S" + using linear_setsum[OF lf fS, of "\i. c i *\<^sub>R v i" , unfolded o_def] linear_cmul[OF lf] by simp lemma linear_injective_0: - assumes lf: "linear (f:: 'a::ring_1 ^ 'n \ _)" + assumes lf: "linear f" 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) @@ -1377,22 +928,22 @@ let ?B = "setsum (\i. norm(f(basis i))) ?S" have fS: "finite ?S" by simp {fix x:: "real ^ 'm" - let ?g = "(\i. (x$i) *s (basis i) :: real ^ 'm)" - have "norm (f x) = norm (f (setsum (\i. (x$i) *s (basis i)) ?S))" - by (simp only: basis_expansion) - also have "\ = norm (setsum (\i. (x$i) *s f (basis i))?S)" + let ?g = "(\i. (x$i) *\<^sub>R (basis i) :: real ^ 'm)" + have "norm (f x) = norm (f (setsum (\i. (x$i) *\<^sub>R (basis i)) ?S))" + by (simp add: basis_expansion') + also have "\ = norm (setsum (\i. (x$i) *\<^sub>R f (basis i))?S)" using linear_setsum[OF lf fS, of ?g, unfolded o_def] linear_cmul[OF lf] by auto - finally have th0: "norm (f x) = norm (setsum (\i. (x$i) *s f (basis i))?S)" . + finally have th0: "norm (f x) = norm (setsum (\i. (x$i) *\<^sub>R f (basis i))?S)" . {fix i assume i: "i \ ?S" from component_le_norm[of x i] - have "norm ((x$i) *s f (basis i :: real ^'m)) \ norm (f (basis i)) * norm x" - unfolding norm_mul + have "norm ((x$i) *\<^sub>R f (basis i :: real ^'m)) \ norm (f (basis i)) * norm x" + unfolding norm_scaleR apply (simp only: mult_commute) apply (rule mult_mono) by (auto simp add: field_simps) } - then have th: "\i\ ?S. norm ((x$i) *s f (basis i :: real ^'m)) \ norm (f (basis i)) * norm x" by metis - from real_setsum_norm_le[OF fS, of "\i. (x$i) *s (f (basis i))", OF th] + then have th: "\i\ ?S. norm ((x$i) *\<^sub>R f (basis i :: real ^'m)) \ norm (f (basis i)) * norm x" by metis + from setsum_norm_le[OF fS, of "\i. (x$i) *\<^sub>R (f (basis i))", OF th] have "norm (f x) \ ?B * norm x" unfolding th0 setsum_left_distrib by metis} then show ?thesis by blast qed @@ -1423,9 +974,6 @@ then show ?thesis using Kp by blast qed -lemma smult_conv_scaleR: "c *s x = scaleR c x" - unfolding vector_scalar_mult_def vector_scaleR_def by simp - lemma linear_conv_bounded_linear: fixes f :: "real ^ _ \ real ^ _" shows "linear f \ bounded_linear f" @@ -1454,7 +1002,7 @@ qed 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" + assumes "\x y. f (x + y) = f x + f y" "\c x. f (c *\<^sub>R x) = c *\<^sub>R f x" shows "bounded_linear f" unfolding linear_conv_bounded_linear[THEN sym] by(rule linearI[OF assms]) @@ -1467,39 +1015,38 @@ lemma bilinear_radd: "bilinear h ==> h x (y + z) = (h x y) + (h x z)" by (simp add: bilinear_def linear_def) -lemma bilinear_lmul: "bilinear h ==> h (c *s x) y = c *s (h x y)" +lemma bilinear_lmul: "bilinear h ==> h (c *\<^sub>R x) y = c *\<^sub>R (h x y)" by (simp add: bilinear_def linear_def) -lemma bilinear_rmul: "bilinear h ==> h x (c *s y) = c *s (h x y)" +lemma bilinear_rmul: "bilinear h ==> h x (c *\<^sub>R y) = c *\<^sub>R (h x y)" by (simp add: bilinear_def linear_def) -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)) = - h x y" - by (simp only: vector_sneg_minus1 bilinear_rmul) +lemma bilinear_lneg: "bilinear h ==> h (- x) y = -(h x y)" + by (simp only: scaleR_minus1_left [symmetric] bilinear_lmul) + +lemma bilinear_rneg: "bilinear h ==> h x (- y) = - h x y" + by (simp only: scaleR_minus1_left [symmetric] 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 \ _" assumes bh: "bilinear h" shows "h 0 x = 0" + assumes bh: "bilinear h" shows "h 0 x = 0" using bilinear_ladd[OF bh, of 0 0 x] by (simp add: eq_add_iff field_simps) lemma bilinear_rzero: - fixes h :: "'a::ring^_ \ _" assumes bh: "bilinear h" shows "h x 0 = 0" + assumes bh: "bilinear h" shows "h x 0 = 0" using bilinear_radd[OF bh, of x 0 0 ] by (simp add: eq_add_iff field_simps) -lemma bilinear_lsub: "bilinear h ==> h (x - (y:: 'a::ring_1 ^ _)) z = h x z - h y z" +lemma bilinear_lsub: "bilinear h ==> h (x - y) z = h x z - h y z" by (simp add: diff_def bilinear_ladd bilinear_lneg) -lemma bilinear_rsub: "bilinear h ==> h z (x - (y:: 'a::ring_1 ^ _)) = h z x - h z y" +lemma bilinear_rsub: "bilinear h ==> h z (x - y) = h z x - h z y" by (simp add: diff_def bilinear_radd bilinear_rneg) lemma bilinear_setsum: - fixes h:: "'a ^_ \ 'a::semiring_1^_\ 'a ^ _" assumes bh: "bilinear h" and fS: "finite S" and fT: "finite T" shows "h (setsum f S) (setsum g T) = setsum (\(i,j). h (f i) (g j)) (S \ T) " proof- @@ -1523,15 +1070,15 @@ let ?B = "setsum (\(i,j). norm (h (basis i) (basis j))) (?M \ ?N)" have fM: "finite ?M" and fN: "finite ?N" by simp_all {fix x:: "real ^ 'm" and y :: "real^'n" - have "norm (h x y) = norm (h (setsum (\i. (x$i) *s basis i) ?M) (setsum (\i. (y$i) *s basis i) ?N))" unfolding basis_expansion .. - also have "\ = norm (setsum (\ (i,j). h ((x$i) *s basis i) ((y$j) *s basis j)) (?M \ ?N))" unfolding bilinear_setsum[OF bh fM fN] .. + have "norm (h x y) = norm (h (setsum (\i. (x$i) *\<^sub>R basis i) ?M) (setsum (\i. (y$i) *\<^sub>R basis i) ?N))" unfolding basis_expansion' .. + also have "\ = norm (setsum (\ (i,j). h ((x$i) *\<^sub>R basis i) ((y$j) *\<^sub>R basis j)) (?M \ ?N))" unfolding bilinear_setsum[OF bh fM fN] .. finally have th: "norm (h x y) = \" . have "norm (h x y) \ ?B * norm x * norm y" apply (simp add: setsum_left_distrib th) - apply (rule real_setsum_norm_le) + apply (rule setsum_norm_le) using fN fM apply simp - apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] field_simps) + apply (auto simp add: bilinear_rmul[OF bh] bilinear_lmul[OF bh] field_simps simp del: scaleR_scaleR) apply (rule mult_mono) apply (auto simp add: zero_le_mult_iff component_le_norm) apply (rule mult_mono) @@ -1600,8 +1147,28 @@ definition "adjoint f = (SOME f'. \x y. f x \ y = x \ f' y)" +lemma adjoint_unique: + assumes "\x y. inner (f x) y = inner x (g y)" + shows "adjoint f = g" +unfolding adjoint_def +proof (rule some_equality) + show "\x y. inner (f x) y = inner x (g y)" using assms . +next + fix h assume "\x y. inner (f x) y = inner x (h y)" + hence "\x y. inner x (g y) = inner x (h y)" using assms by simp + hence "\x y. inner x (g y - h y) = 0" by (simp add: inner_diff_right) + hence "\y. inner (g y - h y) (g y - h y) = 0" by simp + hence "\y. h y = g y" by simp + thus "h = g" by (simp add: ext) +qed + lemma choice_iff: "(\x. \y. P x y) \ (\f. \x. P x (f x))" by metis +text {* TODO: The following lemmas about adjoints should hold for any +Hilbert space (i.e. complete inner product space). +(see \url{http://en.wikipedia.org/wiki/Hermitian_adjoint}) +*} + lemma adjoint_works_lemma: fixes f:: "real ^'n \ real ^'m" assumes lf: "linear f" @@ -1614,9 +1181,9 @@ {fix y:: "real ^ 'm" let ?w = "(\ i. (f (basis i) \ y)) :: real ^ 'n" {fix x - have "f x \ y = f (setsum (\i. (x$i) *s basis i) ?N) \ y" - by (simp only: basis_expansion) - also have "\ = (setsum (\i. (x$i) *s f (basis i)) ?N) \ y" + have "f x \ y = f (setsum (\i. (x$i) *\<^sub>R basis i) ?N) \ y" + by (simp only: basis_expansion') + also have "\ = (setsum (\i. (x$i) *\<^sub>R f (basis i)) ?N) \ y" unfolding linear_setsum[OF lf fN] by (simp add: linear_cmul[OF lf]) finally have "f x \ y = x \ ?w" @@ -1640,7 +1207,7 @@ fixes f:: "real ^'n \ real ^'m" assumes lf: "linear f" shows "linear (adjoint f)" - unfolding linear_def vector_eq_ldot[symmetric] apply safe + unfolding linear_def vector_eq_ldot[where 'a="real^'n", symmetric] apply safe unfolding inner_simps smult_conv_scaleR adjoint_works[OF lf] by auto lemma adjoint_clauses: @@ -1654,16 +1221,9 @@ fixes f:: "real ^'n \ real ^'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:: "real ^'n \ real ^'m" - assumes lf: "linear f" and u: "\x y. f' x \ y = x \ f y" - shows "f' = adjoint f" - apply (rule ext) - using u - by (simp add: vector_eq_rdot[symmetric] adjoint_clauses[OF lf]) + by (rule adjoint_unique, simp add: adjoint_clauses [OF lf]) + +subsection {* Matrix operations *} text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *} @@ -1778,18 +1338,18 @@ by (vector Cart_eq setsum_component) lemma linear_componentwise: - fixes f:: "'a::ring_1 ^'m \ 'a ^ _" + fixes f:: "real ^'m \ real ^ _" assumes lf: "linear f" shows "(f x)$j = setsum (\i. (x$i) * (f (basis i)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs") proof- let ?M = "(UNIV :: 'm set)" let ?N = "(UNIV :: 'n set)" have fM: "finite ?M" by simp - have "?rhs = (setsum (\i.(x$i) *s f (basis i) ) ?M)$j" - unfolding vector_smult_component[symmetric] - unfolding setsum_component[of "(\i.(x$i) *s f (basis i :: 'a^'m))" ?M] + have "?rhs = (setsum (\i.(x$i) *\<^sub>R f (basis i) ) ?M)$j" + unfolding vector_smult_component[symmetric] smult_conv_scaleR + unfolding setsum_component[of "(\i.(x$i) *\<^sub>R f (basis i :: real^'m))" ?M] .. - then show ?thesis unfolding linear_setsum_mul[OF lf fM, symmetric] basis_expansion .. + then show ?thesis unfolding linear_setsum_mul[OF lf fM, symmetric] basis_expansion' .. qed text{* Inverse matrices (not necessarily square) *} @@ -1804,23 +1364,23 @@ 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 ^ _))" +lemma matrix_vector_mul_linear: "linear(\x. A *v (x::real ^ _))" by (simp add: linear_def matrix_vector_mult_def Cart_eq field_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)" +lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::real ^ '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))" by (simp add: ext matrix_works) - -lemma matrix_of_matrix_vector_mul: "matrix(\x. A *v (x :: 'a:: comm_ring_1 ^ 'n)) = A" +lemma matrix_vector_mul: "linear f ==> f = (\x. matrix f *v (x::real ^ 'n))" by (simp add: ext matrix_works) + +lemma matrix_of_matrix_vector_mul: "matrix(\x. A *v (x :: real ^ '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 \ 'a^'m)" - and lg: "linear (g::'a::comm_ring_1^'m \ 'a^_)" + assumes lf: "linear (f::real^'n \ real^'m)" + and lg: "linear (g::real^'m \ real^_)" 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) @@ -1829,8 +1389,7 @@ by (simp add: matrix_vector_mult_def transpose_def Cart_eq mult_commute) lemma adjoint_matrix: "adjoint(\x. (A::real^'n^'m) *v x) = (\x. transpose A *v x)" - apply (rule adjoint_unique[symmetric]) - apply (rule matrix_vector_mul_linear) + apply (rule adjoint_unique) apply (simp add: transpose_def inner_vector_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib) apply (subst setsum_commute) apply (auto simp add: mult_ac) @@ -1928,145 +1487,6 @@ ultimately show ?thesis by metis qed -subsection{* Operator norm. *} - -definition "onorm f = Sup {norm (f x)| x. norm x = 1}" - -lemma norm_bound_generalize: - 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- - {assume H: ?rhs - {fix x :: "real^'n" assume x: "norm x = 1" - from H[rule_format, of x] x have "norm (f x) \ b" by simp} - then have ?lhs by blast } - - moreover - {assume H: ?lhs - from H[rule_format, of "basis arbitrary"] - have bp: "b \ 0" using norm_ge_zero[of "f (basis arbitrary)"] - by (auto simp add: norm_basis elim: order_trans [OF norm_ge_zero]) - {fix x :: "real ^'n" - {assume "x = 0" - then have "norm (f x) \ b * norm x" by (simp add: linear_0[OF lf] bp)} - moreover - {assume x0: "x \ 0" - hence n0: "norm x \ 0" by (metis norm_eq_zero) - let ?c = "1/ norm x" - have "norm (?c*s x) = 1" using x0 by (simp add: n0) - with H have "norm (f(?c*s x)) \ b" by blast - hence "?c * norm (f x) \ b" - by (simp add: linear_cmul[OF lf]) - hence "norm (f x) \ b * norm x" - using n0 norm_ge_zero[of x] by (auto simp add: field_simps)} - ultimately have "norm (f x) \ b * norm x" by blast} - then have ?rhs by blast} - ultimately show ?thesis by blast -qed - -lemma onorm: - 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" -proof- - { - let ?S = "{norm (f x) |x. norm x = 1}" - have Se: "?S \ {}" using norm_basis by auto - from linear_bounded[OF lf] have b: "\ b. ?S *<= b" - unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def) - {from Sup[OF Se b, unfolded onorm_def[symmetric]] - show "norm (f x) <= onorm f * norm x" - apply - - apply (rule spec[where x = x]) - unfolding norm_bound_generalize[OF lf, symmetric] - by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)} - { - show "\x. norm (f x) <= b * norm x \ onorm f <= b" - using Sup[OF Se b, unfolded onorm_def[symmetric]] - unfolding norm_bound_generalize[OF lf, symmetric] - by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)} - } -qed - -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 \ real ^'m)" - shows "onorm f = 0 \ (\x. f x = 0)" - using onorm[OF lf] - apply (auto simp add: onorm_pos_le) - apply atomize - apply (erule allE[where x="0::real"]) - using onorm_pos_le[OF lf] - apply arith - done - -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}" - by(auto intro: vector_choose_size set_ext) - show ?thesis - unfolding onorm_def th - apply (rule Sup_unique) by (simp_all add: setle_def) -qed - -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 \ 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 - apply (subst mult_assoc) - apply (rule order_trans) - apply (rule onorm(1)[OF lf]) - apply (rule mult_mono1) - apply (rule onorm(1)[OF lg]) - apply (rule onorm_pos_le[OF lf]) - done - -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 \ 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 \ 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) - apply (rule norm_triangle_ineq) - apply (simp add: distrib) - apply (rule add_mono) - apply (rule onorm(1)[OF lf]) - apply (rule onorm(1)[OF lg]) - done - -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 \ 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) - by assumption+ - lemma vec_in_image_vec: "vec x \ (vec ` S) \ x \ S" by auto lemma vec_add: "vec(x + y) = vec x + vec y" by (vector vec_def) @@ -2081,77 +1501,6 @@ apply (auto simp add: vec_add) done -text{* Pasting vectors. *} - -lemma linear_fstcart[intro]: "linear fstcart" - by (auto simp add: linear_def Cart_eq) - -lemma linear_sndcart[intro]: "linear sndcart" - by (auto simp add: linear_def Cart_eq) - -lemma fstcart_vec[simp]: "fstcart(vec x) = vec x" - by (simp add: Cart_eq) - -lemma fstcart_add[simp]:"fstcart(x + y) = fstcart (x::'a::{plus,times}^('b::finite + 'c::finite)) + fstcart y" - by (simp add: Cart_eq) - -lemma fstcart_cmul[simp]:"fstcart(c*s x) = c*s fstcart (x::'a::{plus,times}^('b::finite + 'c::finite))" - by (simp add: Cart_eq) - -lemma fstcart_neg[simp]:"fstcart(- x) = - fstcart (x::'a::ring_1^(_ + _))" - by (simp add: Cart_eq) - -lemma fstcart_sub[simp]:"fstcart(x - y) = fstcart (x::'a::ring_1^(_ + _)) - fstcart y" - by (simp add: Cart_eq) - -lemma fstcart_setsum: - fixes f:: "'d \ 'a::semiring_1^_" - assumes fS: "finite S" - shows "fstcart (setsum f S) = setsum (\i. fstcart (f i)) S" - by (induct rule: finite_induct[OF fS], simp_all add: vec_0[symmetric] del: vec_0) - -lemma sndcart_vec[simp]: "sndcart(vec x) = vec x" - by (simp add: Cart_eq) - -lemma sndcart_add[simp]:"sndcart(x + y) = sndcart (x::'a::{plus,times}^(_ + _)) + sndcart y" - by (simp add: Cart_eq) - -lemma sndcart_cmul[simp]:"sndcart(c*s x) = c*s sndcart (x::'a::{plus,times}^(_ + _))" - by (simp add: Cart_eq) - -lemma sndcart_neg[simp]:"sndcart(- x) = - sndcart (x::'a::ring_1^(_ + _))" - by (simp add: Cart_eq) - -lemma sndcart_sub[simp]:"sndcart(x - y) = sndcart (x::'a::ring_1^(_ + _)) - sndcart y" - by (simp add: Cart_eq) - -lemma sndcart_setsum: - fixes f:: "'d \ 'a::semiring_1^_" - assumes fS: "finite S" - shows "sndcart (setsum f S) = setsum (\i. sndcart (f i)) S" - by (induct rule: finite_induct[OF fS], simp_all add: vec_0[symmetric] del: vec_0) - -lemma pastecart_vec[simp]: "pastecart (vec x) (vec x) = vec x" - by (simp add: pastecart_eq) - -lemma pastecart_add[simp]:"pastecart (x1::'a::{plus,times}^_) y1 + pastecart x2 y2 = pastecart (x1 + x2) (y1 + y2)" - by (simp add: pastecart_eq) - -lemma pastecart_cmul[simp]: "pastecart (c *s (x1::'a::{plus,times}^_)) (c *s y1) = c *s pastecart x1 y1" - by (simp add: pastecart_eq) - -lemma pastecart_neg[simp]: "pastecart (- (x::'a::ring_1^_)) (- y) = - pastecart x y" - unfolding vector_sneg_minus1 pastecart_cmul .. - -lemma pastecart_sub: "pastecart (x1::'a::ring_1^_) y1 - pastecart x2 y2 = pastecart (x1 - x2) (y1 - y2)" - by (simp add: diff_def pastecart_neg[symmetric] del: pastecart_neg) - -lemma pastecart_setsum: - fixes f:: "'d \ 'a::semiring_1^_" - assumes fS: "finite S" - shows "pastecart (setsum f S) (setsum g S) = setsum (\i. pastecart (f i) (g i)) S" - by (simp add: pastecart_eq fstcart_setsum[OF fS] sndcart_setsum[OF fS]) - lemma setsum_Plus: "\finite A; finite B\ \ (\x\A <+> B. g x) = (\x\A. g (Inl x)) + (\x\B. g (Inr x))" @@ -2165,39 +1514,6 @@ apply (rule setsum_Plus [OF finite finite]) done -lemma norm_fstcart: "norm(fstcart x) <= norm (x::real ^('n::finite + 'm::finite))" -proof- - have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))" - by simp - have th1: "fstcart x \ fstcart x \ pastecart (fstcart x) (sndcart x) \ pastecart (fstcart x) (sndcart x)" - by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def setsum_nonneg) - then show ?thesis - unfolding th0 - unfolding norm_eq_sqrt_inner real_sqrt_le_iff id_def - by (simp add: inner_vector_def) -qed - -lemma dist_fstcart: "dist(fstcart (x::real^_)) (fstcart y) <= dist x y" - unfolding dist_norm by (metis fstcart_sub[symmetric] norm_fstcart) - -lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n::finite + 'm::finite))" -proof- - have th0: "norm x = norm (pastecart (fstcart x) (sndcart x))" - by simp - have th1: "sndcart x \ sndcart x \ pastecart (fstcart x) (sndcart x) \ pastecart (fstcart x) (sndcart x)" - by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def setsum_nonneg) - then show ?thesis - unfolding th0 - unfolding norm_eq_sqrt_inner real_sqrt_le_iff id_def - by (simp add: inner_vector_def) -qed - -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::real^'n) (x2::real^'m)) \ (pastecart y1 y2) = x1 \ y1 + x2 \ y2" - by (simp add: inner_vector_def setsum_UNIV_sum pastecart_def) - text {* TODO: move to NthRoot *} lemma sqrt_add_le_add_sqrt: assumes x: "0 \ x" and y: "0 \ y" @@ -2208,10 +1524,6 @@ apply (simp add: add_nonneg_nonneg x y) done -lemma norm_pastecart: "norm (pastecart x y) <= norm x + norm y" - unfolding norm_vector_def setL2_def setsum_UNIV_sum - by (simp add: sqrt_add_le_add_sqrt setsum_nonneg) - subsection {* A generic notion of "hull" (convex, affine, conic hull and closure). *} definition hull :: "'a set set \ 'a set \ 'a set" (infixl "hull" 75) where @@ -2417,7 +1729,10 @@ subsection{* A bit of linear algebra. *} -definition "subspace S \ 0 \ S \ (\x\ S. \y \S. x + y \ S) \ (\c. \x \S. c *s x \S )" +definition + subspace :: "'a::real_vector set \ bool" where + "subspace S \ 0 \ S \ (\x\ S. \y \S. x + y \ S) \ (\c. \x \S. c *\<^sub>R x \S )" + definition "span S = (subspace hull S)" definition "dependent S \ (\a \ S. a \ span(S - {a}))" abbreviation "independent s == ~(dependent s)" @@ -2431,13 +1746,13 @@ lemma subspace_add: "subspace S \ x \ S \ y \ S ==> x + y \ S" by (metis subspace_def) -lemma subspace_mul: "subspace S \ x \ S \ c *s x \ S" +lemma subspace_mul: "subspace S \ x \ S \ c *\<^sub>R x \ S" by (metis subspace_def) -lemma subspace_neg: "subspace S \ (x::'a::ring_1^_) \ S \ - x \ S" - by (metis vector_sneg_minus1 subspace_mul) - -lemma subspace_sub: "subspace S \ (x::'a::ring_1^_) \ S \ y \ S \ x - y \ S" +lemma subspace_neg: "subspace S \ x \ S \ - x \ S" + by (metis scaleR_minus1_left subspace_mul) + +lemma subspace_sub: "subspace S \ x \ S \ y \ S \ x - y \ S" by (metis diff_def subspace_add subspace_neg) lemma subspace_setsum: @@ -2449,19 +1764,19 @@ by (simp add: subspace_def sA, auto simp add: sA subspace_add) lemma subspace_linear_image: - assumes lf: "linear (f::'a::semiring_1^_ \ _)" and sS: "subspace S" + assumes lf: "linear f" and sS: "subspace S" shows "subspace(f ` S)" using lf sS linear_0[OF lf] unfolding linear_def subspace_def apply (auto simp add: image_iff) apply (rule_tac x="x + y" in bexI, auto) - apply (rule_tac x="c*s x" in bexI, auto) + apply (rule_tac x="c *\<^sub>R x" in bexI, auto) done -lemma subspace_linear_preimage: "linear (f::'a::semiring_1^_ \ _) ==> subspace S ==> subspace {x. f x \ S}" +lemma subspace_linear_preimage: "linear f ==> subspace S ==> subspace {x. f x \ S}" by (auto simp add: subspace_def linear_def linear_0[of f]) -lemma subspace_trivial: "subspace {0::'a::semiring_1 ^_}" +lemma subspace_trivial: "subspace {0}" by (simp add: subspace_def) lemma subspace_inter: "subspace A \ subspace B ==> subspace (A \ B)" @@ -2497,7 +1812,7 @@ "a \ S ==> a \ span S" "0 \ span S" "x\ span S \ y \ span S ==> x + y \ span S" - "x \ span S \ c *s x \ span S" + "x \ span S \ c *\<^sub>R x \ span S" by (metis span_def hull_subset subset_eq) (metis subspace_span subspace_def)+ @@ -2510,11 +1825,11 @@ show "P x" by (metis mem_def subset_eq) qed -lemma span_empty: "span {} = {(0::'a::semiring_0 ^ _)}" +lemma span_empty: "span {} = {0}" apply (simp add: span_def) apply (rule hull_unique) apply (auto simp add: mem_def subspace_def) - unfolding mem_def[of "0::'a^_", symmetric] + unfolding mem_def[of "0::'a", symmetric] apply simp done @@ -2536,15 +1851,15 @@ and P: "subspace P" shows "\x \ span S. P x" using span_induct SP P by blast -inductive span_induct_alt_help for S:: "'a::semiring_1^_ \ bool" +inductive span_induct_alt_help for S:: "'a::real_vector \ bool" where span_induct_alt_help_0: "span_induct_alt_help S 0" - | span_induct_alt_help_S: "x \ S \ span_induct_alt_help S z \ span_induct_alt_help S (c *s x + z)" + | span_induct_alt_help_S: "x \ S \ span_induct_alt_help S z \ span_induct_alt_help S (c *\<^sub>R x + z)" lemma span_induct_alt': - 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" + assumes h0: "h 0" and hS: "\c x y. x \ S \ h y \ h (c *\<^sub>R x + y)" shows "\x \ span S. h x" proof- - {fix x:: "'a^'n" assume x: "span_induct_alt_help S x" + {fix x:: "'a" assume x: "span_induct_alt_help S x" have "h x" apply (rule span_induct_alt_help.induct[OF x]) apply (rule h0) @@ -2575,10 +1890,10 @@ done} moreover {fix c x assume xt: "span_induct_alt_help S x" - then have "span_induct_alt_help S (c*s x)" + then have "span_induct_alt_help S (c *\<^sub>R x)" apply (induct rule: span_induct_alt_help.induct) apply (simp add: span_induct_alt_help_0) - apply (simp add: vector_smult_assoc vector_add_ldistrib) + apply (simp add: scaleR_right_distrib) apply (rule span_induct_alt_help_S) apply assumption apply simp @@ -2591,7 +1906,7 @@ qed lemma span_induct_alt: - 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" + assumes h0: "h 0" and hS: "\c x y. x \ S \ h y \ h (c *\<^sub>R x + y)" and x: "x \ span S" shows "h x" using span_induct_alt'[of h S] h0 hS x by blast @@ -2604,26 +1919,26 @@ lemma span_add: "x \ span S \ y \ span S ==> x + y \ span S" by (metis subspace_add subspace_span) -lemma span_mul: "x \ span S ==> (c *s x) \ span S" +lemma span_mul: "x \ span S ==> (c *\<^sub>R x) \ span S" by (metis subspace_span subspace_mul) -lemma span_neg: "x \ span S ==> - (x::'a::ring_1^_) \ span S" +lemma span_neg: "x \ span S ==> - x \ span S" by (metis subspace_neg subspace_span) -lemma span_sub: "(x::'a::ring_1^_) \ span S \ y \ span S ==> x - y \ span S" +lemma span_sub: "x \ span S \ y \ span S ==> x - y \ span S" by (metis subspace_span subspace_sub) lemma span_setsum: "finite A \ \x \ A. f x \ span S ==> setsum f A \ span S" by (rule subspace_setsum, rule subspace_span) -lemma span_add_eq: "(x::'a::ring_1^_) \ span S \ x + y \ span S \ y \ span S" +lemma span_add_eq: "x \ span S \ x + y \ span S \ y \ span S" apply (auto simp only: span_add span_sub) apply (subgoal_tac "(x + y) - x \ span S", simp) by (simp only: span_add span_sub) (* Mapping under linear image. *) -lemma span_linear_image: assumes lf: "linear (f::'a::semiring_1 ^ _ => _)" +lemma span_linear_image: assumes lf: "linear f" shows "span (f ` S) = f ` (span S)" proof- {fix x @@ -2656,8 +1971,8 @@ (* The key breakdown property. *) lemma span_breakdown: - assumes bS: "(b::'a::ring_1 ^ _) \ S" and aS: "a \ span S" - shows "\k. a - k*s b \ span (S - {b})" (is "?P a") + assumes bS: "b \ S" and aS: "a \ span S" + shows "\k. a - k *\<^sub>R b \ span (S - {b})" (is "?P a") proof- {fix x assume xS: "x \ S" {assume ab: "x = b" @@ -2682,23 +1997,23 @@ apply (simp add: mem_def) apply (clarsimp simp add: mem_def) apply (rule_tac x="k + ka" in exI) - apply (subgoal_tac "x + y - (k + ka) *s b = (x - k*s b) + (y - ka *s b)") + apply (subgoal_tac "x + y - (k + ka) *\<^sub>R b = (x - k*\<^sub>R b) + (y - ka *\<^sub>R b)") apply (simp only: ) apply (rule span_add[unfolded mem_def]) apply assumption+ - apply (vector field_simps) + apply (simp add: algebra_simps) apply (clarsimp simp add: mem_def) apply (rule_tac x= "c*k" in exI) - apply (subgoal_tac "c *s x - (c * k) *s b = c*s (x - k*s b)") + apply (subgoal_tac "c *\<^sub>R x - (c * k) *\<^sub>R b = c*\<^sub>R (x - k*\<^sub>R b)") apply (simp only: ) apply (rule span_mul[unfolded mem_def]) apply assumption - by (vector field_simps) + by (simp add: algebra_simps) ultimately show "?P a" using aS span_induct[where S=S and P= "?P"] by metis qed lemma span_breakdown_eq: - "(x::'a::ring_1^_) \ span (insert a S) \ (\k. (x - k *s a) \ span S)" (is "?lhs \ ?rhs") + "x \ span (insert a S) \ (\k. (x - k *\<^sub>R a) \ span S)" (is "?lhs \ ?rhs") proof- {assume x: "x \ span (insert a S)" from x span_breakdown[of "a" "insert a S" "x"] @@ -2710,9 +2025,9 @@ apply blast done} moreover - { fix k assume k: "x - k *s a \ span S" - have eq: "x = (x - k *s a) + k *s a" by vector - have "(x - k *s a) + k *s a \ span (insert a S)" + { fix k assume k: "x - k *\<^sub>R a \ span S" + have eq: "x = (x - k *\<^sub>R a) + k *\<^sub>R a" by vector + have "(x - k *\<^sub>R a) + k *\<^sub>R a \ span (insert a S)" apply (rule span_add) apply (rule set_rev_mp[of _ "span S" _]) apply (rule k) @@ -2729,11 +2044,11 @@ (* Hence some "reversal" results.*) lemma in_span_insert: - assumes a: "(a::'a::field^_) \ span (insert b S)" and na: "a \ span S" + assumes a: "a \ span (insert b S)" and na: "a \ span S" shows "b \ span (insert a S)" proof- from span_breakdown[of b "insert b S" a, OF insertI1 a] - obtain k where k: "a - k*s b \ span (S - {b})" by auto + obtain k where k: "a - k*\<^sub>R b \ span (S - {b})" by auto {assume k0: "k = 0" with k have "a \ span S" apply (simp) @@ -2745,12 +2060,12 @@ with na have ?thesis by blast} moreover {assume k0: "k \ 0" - have eq: "b = (1/k) *s a - ((1/k) *s a - b)" by vector - from k0 have eq': "(1/k) *s (a - k*s b) = (1/k) *s a - b" - by (vector field_simps) - from k have "(1/k) *s (a - k*s b) \ span (S - {b})" + have eq: "b = (1/k) *\<^sub>R a - ((1/k) *\<^sub>R a - b)" by vector + from k0 have eq': "(1/k) *\<^sub>R (a - k*\<^sub>R b) = (1/k) *\<^sub>R a - b" + by (simp add: algebra_simps) + from k have "(1/k) *\<^sub>R (a - k*\<^sub>R b) \ span (S - {b})" by (rule span_mul) - hence th: "(1/k) *s a - b \ span (S - {b})" + hence th: "(1/k) *\<^sub>R a - b \ span (S - {b})" unfolding eq' . from k @@ -2768,7 +2083,7 @@ qed lemma in_span_delete: - assumes a: "(a::'a::field^_) \ span S" + assumes a: "a \ span S" and na: "a \ span (S-{b})" shows "b \ span (insert a (S - {b}))" apply (rule in_span_insert) @@ -2782,12 +2097,12 @@ (* Transitivity property. *) lemma span_trans: - assumes x: "(x::'a::ring_1^_) \ span S" and y: "y \ span (insert x S)" + assumes x: "x \ span S" and y: "y \ span (insert x S)" shows "y \ span S" proof- from span_breakdown[of x "insert x S" y, OF insertI1 y] - obtain k where k: "y -k*s x \ span (S - {x})" by auto - have eq: "y = (y - k *s x) + k *s x" by vector + obtain k where k: "y -k*\<^sub>R x \ span (S - {x})" by auto + have eq: "y = (y - k *\<^sub>R x) + k *\<^sub>R x" by vector show ?thesis apply (subst eq) apply (rule span_add) @@ -2804,11 +2119,11 @@ (* ------------------------------------------------------------------------- *) lemma span_explicit: - "span P = {y::'a::semiring_1^_. \S u. finite S \ S \ P \ setsum (\v. u v *s v) S = y}" + "span P = {y. \S u. finite S \ S \ P \ setsum (\v. u v *\<^sub>R v) S = y}" (is "_ = ?E" is "_ = {y. ?h y}" is "_ = {y. \S u. ?Q S u y}") proof- {fix x assume x: "x \ ?E" - then obtain S u where fS: "finite S" and SP: "S\P" and u: "setsum (\v. u v *s v) S = x" + then obtain S u where fS: "finite S" and SP: "S\P" and u: "setsum (\v. u v *\<^sub>R v) S = x" by blast have "x \ span P" unfolding u[symmetric] @@ -2825,7 +2140,7 @@ fix c x y assume x: "x \ P" and hy: "?h y" from hy obtain S u where fS: "finite S" and SP: "S\P" - and u: "setsum (\v. u v *s v) S = y" by blast + and u: "setsum (\v. u v *\<^sub>R v) S = y" by blast let ?S = "insert x S" let ?u = "\y. if y = x then (if x \ S then u y + c else c) else u y" @@ -2833,28 +2148,28 @@ {assume xS: "x \ S" have S1: "S = (S - {x}) \ {x}" and Sss:"finite (S - {x})" "finite {x}" "(S -{x}) \ {x} = {}" using xS fS by auto - have "setsum (\v. ?u v *s v) ?S =(\v\S - {x}. u v *s v) + (u x + c) *s x" + have "setsum (\v. ?u v *\<^sub>R v) ?S =(\v\S - {x}. u v *\<^sub>R v) + (u x + c) *\<^sub>R x" using xS by (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]] setsum_clauses(2)[OF fS] cong del: if_weak_cong) - also have "\ = (\v\S. u v *s v) + c *s x" + also have "\ = (\v\S. u v *\<^sub>R v) + c *\<^sub>R x" apply (simp add: setsum_Un_disjoint[OF Sss, unfolded S1[symmetric]]) - by (vector field_simps) - also have "\ = c*s x + y" + by (simp add: algebra_simps) + also have "\ = c*\<^sub>R x + y" by (simp add: add_commute u) - finally have "setsum (\v. ?u v *s v) ?S = c*s x + y" . - then have "?Q ?S ?u (c*s x + y)" using th0 by blast} + finally have "setsum (\v. ?u v *\<^sub>R v) ?S = c*\<^sub>R x + y" . + then have "?Q ?S ?u (c*\<^sub>R x + y)" using th0 by blast} moreover {assume xS: "x \ S" - have th00: "(\v\S. (if v = x then c else u v) *s v) = y" + have th00: "(\v\S. (if v = x then c else u v) *\<^sub>R v) = y" unfolding u[symmetric] apply (rule setsum_cong2) using xS by auto - have "?Q ?S ?u (c*s x + y)" using fS xS th0 + have "?Q ?S ?u (c*\<^sub>R x + y)" using fS xS th0 by (simp add: th00 setsum_clauses add_commute cong del: if_weak_cong)} - ultimately have "?Q ?S ?u (c*s x + y)" + ultimately have "?Q ?S ?u (c*\<^sub>R x + y)" by (cases "x \ S", simp, simp) - then show "?h (c*s x + y)" + then show "?h (c*\<^sub>R x + y)" apply - apply (rule exI[where x="?S"]) apply (rule exI[where x="?u"]) by metis @@ -2863,18 +2178,18 @@ qed lemma dependent_explicit: - "dependent P \ (\S u. finite S \ S \ P \ (\(v::'a::{idom,field}^_) \S. u v \ 0 \ setsum (\v. u v *s v) S = 0))" (is "?lhs = ?rhs") + "dependent P \ (\S u. finite S \ S \ P \ (\v\S. u v \ 0 \ setsum (\v. u v *\<^sub>R v) S = 0))" (is "?lhs = ?rhs") proof- {assume dP: "dependent P" then obtain a S u where aP: "a \ P" and fS: "finite S" - and SP: "S \ P - {a}" and ua: "setsum (\v. u v *s v) S = a" + and SP: "S \ P - {a}" and ua: "setsum (\v. u v *\<^sub>R v) S = a" unfolding dependent_def span_explicit by blast let ?S = "insert a S" let ?u = "\y. if y = a then - 1 else u y" let ?v = a from aP SP have aS: "a \ S" by blast from fS SP aP have th0: "finite ?S" "?S \ P" "?v \ ?S" "?u ?v \ 0" by auto - have s0: "setsum (\v. ?u v *s v) ?S = 0" + have s0: "setsum (\v. ?u v *\<^sub>R v) ?S = 0" using fS aS apply (simp add: vector_smult_lneg setsum_clauses field_simps) apply (subst (2) ua[symmetric]) @@ -2888,47 +2203,47 @@ moreover {fix S u v assume fS: "finite S" and SP: "S \ P" and vS: "v \ S" and uv: "u v \ 0" - and u: "setsum (\v. u v *s v) S = 0" + and u: "setsum (\v. u v *\<^sub>R v) S = 0" let ?a = v let ?S = "S - {v}" let ?u = "\i. (- u i) / u v" have th0: "?a \ P" "finite ?S" "?S \ P" using fS SP vS by auto - have "setsum (\v. ?u v *s v) ?S = setsum (\v. (- (inverse (u ?a))) *s (u v *s v)) S - ?u v *s v" + have "setsum (\v. ?u v *\<^sub>R v) ?S = setsum (\v. (- (inverse (u ?a))) *\<^sub>R (u v *\<^sub>R v)) S - ?u v *\<^sub>R v" using fS vS uv by (simp add: setsum_diff1 vector_smult_lneg divide_inverse vector_smult_assoc field_simps) also have "\ = ?a" - unfolding setsum_cmul u - using uv by (simp add: vector_smult_lneg) - finally have "setsum (\v. ?u v *s v) ?S = ?a" . + unfolding scaleR_right.setsum [symmetric] u + using uv by simp + finally have "setsum (\v. ?u v *\<^sub>R v) ?S = ?a" . with th0 have ?lhs unfolding dependent_def span_explicit apply - apply (rule bexI[where x= "?a"]) - apply simp_all + apply (simp_all del: scaleR_minus_left) apply (rule exI[where x= "?S"]) - by auto} + by (auto simp del: scaleR_minus_left)} ultimately show ?thesis by blast qed lemma span_finite: assumes fS: "finite S" - shows "span S = {(y::'a::semiring_1^_). \u. setsum (\v. u v *s v) S = y}" + shows "span S = {y. \u. setsum (\v. u v *\<^sub>R v) S = y}" (is "_ = ?rhs") proof- {fix y assume y: "y \ span S" from y obtain S' u where fS': "finite S'" and SS': "S' \ S" and - u: "setsum (\v. u v *s v) S' = y" unfolding span_explicit by blast + u: "setsum (\v. u v *\<^sub>R v) S' = y" unfolding span_explicit by blast let ?u = "\x. if x \ S' then u x else 0" - from setsum_restrict_set[OF fS, of "\v. u v *s v" S', symmetric] SS' - have "setsum (\v. ?u v *s v) S = setsum (\v. u v *s v) S'" + from setsum_restrict_set[OF fS, of "\v. u v *\<^sub>R v" S', symmetric] SS' + have "setsum (\v. ?u v *\<^sub>R v) S = setsum (\v. u v *\<^sub>R v) S'" unfolding cond_value_iff cond_application_beta by (simp add: cond_value_iff inf_absorb2 cong del: if_weak_cong) - hence "setsum (\v. ?u v *s v) S = y" by (metis u) + hence "setsum (\v. ?u v *\<^sub>R v) S = y" by (metis u) hence "y \ ?rhs" by auto} moreover - {fix y u assume u: "setsum (\v. u v *s v) S = y" + {fix y u assume u: "setsum (\v. u v *\<^sub>R v) S = y" then have "y \ span S" using fS unfolding span_explicit by auto} ultimately show ?thesis by blast qed @@ -2936,10 +2251,10 @@ (* Standard bases are a spanning set, and obviously finite. *) -lemma span_stdbasis:"span {basis i :: 'a::ring_1^'n | i. i \ (UNIV :: 'n set)} = UNIV" +lemma span_stdbasis:"span {basis i :: real^'n | i. i \ (UNIV :: 'n set)} = UNIV" apply (rule set_ext) apply auto -apply (subst basis_expansion[symmetric]) +apply (subst basis_expansion'[symmetric]) apply (rule span_setsum) apply simp apply auto @@ -2962,14 +2277,14 @@ lemma independent_stdbasis_lemma: - assumes x: "(x::'a::semiring_1 ^ _) \ span (basis ` S)" + assumes x: "(x::real ^ 'n) \ span (basis ` S)" and iS: "i \ S" shows "(x$i) = 0" proof- let ?U = "UNIV :: 'n set" let ?B = "basis ` S" - let ?P = "\(x::'a^_). \i\ ?U. i \ S \ x$i =0" - {fix x::"'a^_" assume xS: "x\ ?B" + let ?P = "\(x::real^_). \i\ ?U. i \ S \ x$i =0" + {fix x::"real^_" assume xS: "x\ ?B" from xS have "?P x" by auto} moreover have "subspace ?P" @@ -3002,7 +2317,7 @@ (* This is useful for building a basis step-by-step. *) lemma independent_insert: - "independent(insert (a::'a::field ^_) S) \ + "independent(insert a S) \ (if a \ S then independent S else independent S \ a \ span S)" (is "?lhs \ ?rhs") proof- @@ -3051,7 +2366,7 @@ by (metis subset_eq span_superset) lemma spanning_subset_independent: - assumes BA: "B \ A" and iA: "independent (A::('a::field ^_) set)" + assumes BA: "B \ A" and iA: "independent A" and AsB: "A \ span B" shows "A = B" proof @@ -3078,7 +2393,7 @@ (* The general case of the Exchange Lemma, the key to what follows. *) lemma exchange_lemma: - assumes f:"finite (t:: ('a::field^'n) set)" and i: "independent s" + assumes f:"finite t" 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 @@ -3154,7 +2469,7 @@ (* This implies corresponding size bounds. *) lemma independent_span_bound: - assumes f: "finite t" and i: "independent (s::('a::field^_) set)" and sp:"s \ span t" + assumes f: "finite t" and i: "independent s" and sp:"s \ span t" shows "finite s \ card s \ card t" by (metis exchange_lemma[OF f i sp] finite_subset card_mono) @@ -3337,7 +2652,7 @@ by (metis dim_span) lemma spans_image: - assumes lf: "linear (f::'a::semiring_1^_ \ _)" and VB: "V \ span B" + assumes lf: "linear f" and VB: "V \ span B" shows "f ` V \ span (f ` B)" unfolding span_linear_image[OF lf] by (metis VB image_mono) @@ -3359,7 +2674,7 @@ (* Relation between bases and injectivity/surjectivity of map. *) lemma spanning_surjective_image: - assumes us: "UNIV \ span (S:: ('a::semiring_1 ^_) set)" + assumes us: "UNIV \ span S" and lf: "linear f" and sf: "surj f" shows "UNIV \ span (f ` S)" proof- @@ -3369,7 +2684,7 @@ qed lemma independent_injective_image: - assumes iS: "independent (S::('a::semiring_1^_) set)" and lf: "linear f" and fi: "inj f" + assumes iS: "independent S" and lf: "linear f" and fi: "inj f" shows "independent (f ` S)" proof- {fix a assume a: "a \ S" "f a \ span (f ` S - {f a})" @@ -3404,14 +2719,14 @@ from `\C. finite C \ card C \ card B \ span C = span B \ pairwise orthogonal C` obtain C where C: "finite C" "card C \ card B" "span C = span B" "pairwise orthogonal C" by blast - let ?a = "a - setsum (\x. (x \ a / (x \ x)) *s x) C" + let ?a = "a - setsum (\x. (x \ a / (x \ x)) *\<^sub>R x) C" let ?C = "insert ?a C" from C(1) have fC: "finite ?C" by simp from fB aB C(1,2) have cC: "card ?C \ card (insert a B)" by (simp add: card_insert_if) {fix x k have th0: "\(a::'b::comm_ring) b c. a - (b - c) = c + (a - b)" by (simp add: field_simps) - have "x - k *s (a - (\x\C. (x \ a / (x \ x)) *s x)) \ span C \ x - k *s a \ span C" - apply (simp only: vector_ssub_ldistrib th0) + have "x - k *\<^sub>R (a - (\x\C. (x \ a / (x \ x)) *\<^sub>R x)) \ span C \ x - k *\<^sub>R a \ span C" + apply (simp only: scaleR_right_diff_distrib th0) apply (rule span_add_eq) apply (rule span_mul) apply (rule span_setsum[OF C(1)]) @@ -3505,8 +2820,8 @@ from B have fB: "finite B" "card B = dim S" using independent_bound by auto from span_mono[OF B(2)] span_mono[OF B(3)] have sSB: "span S = span B" by (simp add: span_span) - let ?a = "a - setsum (\b. (a \ b / (b \ b)) *s b) B" - have "setsum (\b. (a \ b / (b \ b)) *s b) B \ span S" + let ?a = "a - setsum (\b. (a \ b / (b \ b)) *\<^sub>R b) B" + have "setsum (\b. (a \ b / (b \ b)) *\<^sub>R b) B \ span S" unfolding sSB apply (rule span_setsum[OF fB(1)]) apply clarsimp @@ -3557,7 +2872,7 @@ assumes lf: "linear f" and fB: "finite B" and ifB: "independent (f ` B)" and fi: "inj_on f B" and xsB: "x \ span B" - and fx: "f (x::'a::field^_) = 0" + and fx: "f x = 0" shows "x = 0" using fB ifB fi xsB fx proof(induct arbitrary: x rule: finite_induct[OF fB]) @@ -3573,14 +2888,14 @@ apply (rule subset_inj_on [OF "2.prems"(3)]) by blast from span_breakdown[of a "insert a b", simplified, OF "2.prems"(4)] - obtain k where k: "x - k*s a \ span (b -{a})" by blast - have "f (x - k*s a) \ span (f ` b)" + obtain k where k: "x - k*\<^sub>R a \ span (b -{a})" by blast + have "f (x - k*\<^sub>R a) \ span (f ` b)" unfolding span_linear_image[OF lf] apply (rule imageI) using k span_mono[of "b-{a}" b] by blast - hence "f x - k*s f a \ span (f ` b)" + hence "f x - k*\<^sub>R f a \ span (f ` b)" by (simp add: linear_sub[OF lf] linear_cmul[OF lf]) - hence th: "-k *s f a \ span (f ` b)" + hence th: "-k *\<^sub>R f a \ span (f ` b)" using "2.prems"(5) by (simp add: vector_smult_lneg) {assume k0: "k = 0" from k0 k have "x \ span (b -{a})" by simp @@ -3607,9 +2922,10 @@ (* We can extend a linear mapping from basis. *) lemma linear_independent_extend_lemma: + fixes f :: "'a::real_vector \ 'b::real_vector" assumes fi: "finite B" and ib: "independent B" - 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) + shows "\g. (\x\ span B. \y\ span B. g (x + y) = g x + g y) + \ (\x\ span B. \c. g (c*\<^sub>R x) = c *\<^sub>R g x) \ (\x\ B. g x = f x)" using ib fi proof(induct rule: finite_induct[OF fi]) @@ -3620,30 +2936,30 @@ by (simp_all add: independent_insert) from "2.hyps"(3)[OF ibf] obtain g where g: "\x\span b. \y\span b. g (x + y) = g x + g y" - "\x\span b. \c. g (c *s x) = c *s g x" "\x\b. g x = f x" by blast - let ?h = "\z. SOME k. (z - k *s a) \ span b" + "\x\span b. \c. g (c *\<^sub>R x) = c *\<^sub>R g x" "\x\b. g x = f x" by blast + let ?h = "\z. SOME k. (z - k *\<^sub>R a) \ span b" {fix z assume z: "z \ span (insert a b)" - have th0: "z - ?h z *s a \ span b" + have th0: "z - ?h z *\<^sub>R a \ span b" apply (rule someI_ex) unfolding span_breakdown_eq[symmetric] using z . - {fix k assume k: "z - k *s a \ span b" - have eq: "z - ?h z *s a - (z - k*s a) = (k - ?h z) *s a" - by (simp add: field_simps vector_sadd_rdistrib[symmetric]) + {fix k assume k: "z - k *\<^sub>R a \ span b" + have eq: "z - ?h z *\<^sub>R a - (z - k*\<^sub>R a) = (k - ?h z) *\<^sub>R a" + by (simp add: field_simps scaleR_left_distrib [symmetric]) from span_sub[OF th0 k] - have khz: "(k - ?h z) *s a \ span b" by (simp add: eq) + have khz: "(k - ?h z) *\<^sub>R a \ span b" by (simp add: eq) {assume "k \ ?h z" hence k0: "k - ?h z \ 0" by simp from k0 span_mul[OF khz, of "1 /(k - ?h z)"] have "a \ span b" by (simp add: vector_smult_assoc) with "2.prems"(1) "2.hyps"(2) have False by (auto simp add: dependent_def)} then have "k = ?h z" by blast} - with th0 have "z - ?h z *s a \ span b \ (\k. z - k *s a \ span b \ k = ?h z)" by blast} + with th0 have "z - ?h z *\<^sub>R a \ span b \ (\k. z - k *\<^sub>R a \ span b \ k = ?h z)" by blast} note h = this - let ?g = "\z. ?h z *s f a + g (z - ?h z *s a)" + let ?g = "\z. ?h z *\<^sub>R f a + g (z - ?h z *\<^sub>R a)" {fix x y assume x: "x \ span (insert a b)" and y: "y \ span (insert a b)" - have tha: "\(x::'a^'n) y a k l. (x + y) - (k + l) *s a = (x - k *s a) + (y - l *s a)" - by (vector field_simps) + have tha: "\(x::'a) y a k l. (x + y) - (k + l) *\<^sub>R a = (x - k *\<^sub>R a) + (y - l *\<^sub>R a)" + by (simp add: algebra_simps) have addh: "?h (x + y) = ?h x + ?h y" apply (rule conjunct2[OF h, rule_format, symmetric]) apply (rule span_add[OF x y]) @@ -3652,18 +2968,18 @@ have "?g (x + y) = ?g x + ?g y" unfolding addh tha g(1)[rule_format,OF conjunct1[OF h, OF x] conjunct1[OF h, OF y]] - by (simp add: vector_sadd_rdistrib)} + by (simp add: scaleR_left_distrib)} moreover - {fix x:: "'a^'n" and c:: 'a assume x: "x \ span (insert a b)" - have tha: "\(x::'a^'n) c k a. c *s x - (c * k) *s a = c *s (x - k *s a)" - by (vector field_simps) - have hc: "?h (c *s x) = c * ?h x" + {fix x:: "'a" and c:: real assume x: "x \ span (insert a b)" + have tha: "\(x::'a) c k a. c *\<^sub>R x - (c * k) *\<^sub>R a = c *\<^sub>R (x - k *\<^sub>R a)" + by (simp add: algebra_simps) + have hc: "?h (c *\<^sub>R x) = c * ?h x" apply (rule conjunct2[OF h, rule_format, symmetric]) apply (metis span_mul x) by (metis tha span_mul x conjunct1[OF h]) - have "?g (c *s x) = c*s ?g x" + have "?g (c *\<^sub>R x) = c*\<^sub>R ?g x" unfolding hc tha g(2)[rule_format, OF conjunct1[OF h, OF x]] - by (vector field_simps)} + by (simp add: algebra_simps)} moreover {fix x assume x: "x \ (insert a b)" {assume xa: "x = a" @@ -3700,7 +3016,7 @@ from C(2) independent_bound[of C] linear_independent_extend_lemma[of C f] obtain g where g: "(\x\ span C. \y\ span C. g (x + y) = g x + g y) - \ (\x\ span C. \c. g (c*s x) = c *s g x) + \ (\x\ span C. \c. g (c*\<^sub>R x) = c *\<^sub>R g x) \ (\x\ C. g x = f x)" by blast from g show ?thesis unfolding linear_def using C apply clarsimp by blast @@ -3787,14 +3103,14 @@ (* linear functions are equal on a subspace if they are on a spanning set. *) lemma subspace_kernel: - assumes lf: "linear (f::'a::semiring_1 ^_ \ _)" + assumes lf: "linear f" shows "subspace {x. f x = 0}" apply (simp add: subspace_def) by (simp add: linear_add[OF lf] linear_cmul[OF lf] linear_0[OF lf]) lemma linear_eq_0_span: assumes lf: "linear f" and f0: "\x\B. f x = 0" - shows "\x \ span B. f x = (0::'a::semiring_1 ^_)" + shows "\x \ span B. f x = 0" proof fix x assume x: "x \ span B" let ?P = "\x. f x = 0" @@ -3804,11 +3120,11 @@ lemma linear_eq_0: assumes lf: "linear f" and SB: "S \ span B" and f0: "\x\B. f x = 0" - shows "\x \ S. f x = (0::'a::semiring_1^_)" + shows "\x \ S. f x = 0" by (metis linear_eq_0_span[OF lf] subset_eq SB f0) lemma linear_eq: - assumes lf: "linear (f::'a::ring_1^_ \ _)" and lg: "linear g" and S: "S \ span B" + assumes lf: "linear f" and lg: "linear g" and S: "S \ span B" and fg: "\ x\ B. f x = g x" shows "\x\ S. f x = g x" proof- @@ -3819,15 +3135,15 @@ qed lemma linear_eq_stdbasis: - assumes lf: "linear (f::'a::ring_1^'m \ 'a^'n)" and lg: "linear g" + assumes lf: "linear (f::real^'m \ _)" and lg: "linear g" and fg: "\i. f (basis i) = g(basis i)" shows "f = g" proof- let ?U = "UNIV :: 'm set" - let ?I = "{basis i:: 'a^'m|i. i \ ?U}" - {fix x assume x: "x \ (UNIV :: ('a^'m) set)" + let ?I = "{basis i:: real^'m|i. i \ ?U}" + {fix x assume x: "x \ (UNIV :: (real^'m) set)" from equalityD2[OF span_stdbasis] - have IU: " (UNIV :: ('a^'m) set) \ span ?I" by blast + have IU: " (UNIV :: (real^'m) set) \ span ?I" by blast from linear_eq[OF lf lg IU] fg x have "f x = g x" unfolding Collect_def Ball_def mem_def by metis} then show ?thesis by (auto intro: ext) @@ -3836,7 +3152,7 @@ (* Similar results for bilinear functions. *) lemma bilinear_eq: - assumes bf: "bilinear (f:: 'a::ring^_ \ 'a^_ \ 'a^_)" + assumes bf: "bilinear f" and bg: "bilinear g" and SB: "S \ span B" and TC: "T \ span C" and fg: "\x\ B. \y\ C. f x y = g x y" @@ -3864,7 +3180,7 @@ qed lemma bilinear_eq_stdbasis: - assumes bf: "bilinear (f:: 'a::ring_1^'m \ 'a^'n \ 'a^_)" + assumes bf: "bilinear (f:: real^'m \ real^'n \ _)" and bg: "bilinear g" and fg: "\i j. f (basis i) (basis j) = g (basis i) (basis j)" shows "f = g" @@ -4017,6 +3333,7 @@ unfolding y[symmetric] apply (rule span_setsum[OF fU]) apply clarify + unfolding smult_conv_scaleR apply (rule span_mul) apply (rule span_superset) unfolding columns_def @@ -4026,7 +3343,7 @@ {assume h:?rhs let ?P = "\(y::real ^'n). \(x::real^'m). setsum (\i. (x$i) *s column i A) ?U = y" {fix y have "?P y" - proof(rule span_induct_alt[of ?P "columns A"]) + proof(rule span_induct_alt[of ?P "columns A", folded smult_conv_scaleR]) show "\x\real ^ 'm. setsum (\i. (x$i) *s column i A) ?U = 0" by (rule exI[where x=0], simp) next @@ -4469,7 +3786,7 @@ (* Equality in Cauchy-Schwarz and triangle inequalities. *) -lemma norm_cauchy_schwarz_eq: "(x::real ^'n) \ y = norm x * norm y \ norm x *s y = norm y *s x" (is "?lhs \ ?rhs") +lemma norm_cauchy_schwarz_eq: "x \ y = norm x * norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x" (is "?lhs \ ?rhs") proof- {assume h: "x = 0" hence ?thesis by simp} @@ -4478,7 +3795,7 @@ hence ?thesis by simp} moreover {assume x: "x \ 0" and y: "y \ 0" - from inner_eq_zero_iff[of "norm y *s x - norm x *s y"] + from inner_eq_zero_iff[of "norm y *\<^sub>R x - norm x *\<^sub>R y"] have "?rhs \ (norm y * (norm y * norm x * norm x - norm x * (x \ y)) - norm x * (norm y * (y \ x) - norm x * norm y * norm y) = 0)" using x y unfolding inner_simps smult_conv_scaleR @@ -4494,26 +3811,24 @@ qed lemma norm_cauchy_schwarz_abs_eq: - 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") + norm x *\<^sub>R y = norm y *\<^sub>R x \ norm(x) *\<^sub>R y = - norm y *\<^sub>R x" (is "?lhs \ ?rhs") proof- have th: "\(x::real) a. a \ 0 \ abs x = a \ x = a \ x = - a" by arith - have "?rhs \ norm x *s y = norm y *s x \ norm (- x) *s y = norm y *s (- x)" - apply simp by vector + have "?rhs \ norm x *\<^sub>R y = norm y *\<^sub>R x \ norm (- x) *\<^sub>R y = norm y *\<^sub>R (- x)" + by simp also have "\ \(x \ y = norm x * norm y \ (-x) \ y = norm x * norm y)" unfolding norm_cauchy_schwarz_eq[symmetric] - unfolding norm_minus_cancel - norm_mul by blast + unfolding norm_minus_cancel norm_scaleR .. also have "\ \ ?lhs" unfolding th[OF mult_nonneg_nonneg, OF norm_ge_zero[of x] norm_ge_zero[of y]] inner_simps by auto finally show ?thesis .. qed lemma norm_triangle_eq: - fixes x y :: "real ^ 'n" - shows "norm(x + y) = norm x + norm y \ norm x *s y = norm y *s x" + fixes x y :: "'a::real_inner" + shows "norm(x + y) = norm x + norm y \ norm x *\<^sub>R y = norm y *\<^sub>R x" proof- {assume x: "x =0 \ y =0" hence ?thesis by (cases "x=0", simp_all)} @@ -4528,7 +3843,7 @@ have "norm(x + y) = norm x + norm y \ norm(x + y)^ 2 = (norm x + norm y) ^2" apply (rule th) using n norm_ge_zero[of "x + y"] by arith - also have "\ \ norm x *s y = norm y *s x" + also have "\ \ norm x *\<^sub>R y = norm y *\<^sub>R x" unfolding norm_cauchy_schwarz_eq[symmetric] unfolding power2_norm_eq_inner inner_simps by (simp add: power2_norm_eq_inner[symmetric] power2_eq_square inner_commute field_simps) @@ -4538,62 +3853,59 @@ (* Collinearity.*) -definition "collinear S \ (\u. \x \ S. \ y \ S. \c. x - y = c *s u)" +definition + collinear :: "'a::real_vector set \ bool" where + "collinear S \ (\u. \x \ S. \ y \ S. \c. x - y = c *\<^sub>R u)" lemma collinear_empty: "collinear {}" by (simp add: collinear_def) -lemma collinear_sing: "collinear {(x::'a::ring_1^_)}" - apply (simp add: collinear_def) - apply (rule exI[where x=0]) - by simp - -lemma collinear_2: "collinear {(x::'a::ring_1^_),y}" +lemma collinear_sing: "collinear {x}" + by (simp add: collinear_def) + +lemma collinear_2: "collinear {x, y}" apply (simp add: collinear_def) apply (rule exI[where x="x - y"]) apply auto - apply (rule exI[where x=0], simp) apply (rule exI[where x=1], simp) - apply (rule exI[where x="- 1"], simp add: vector_sneg_minus1[symmetric]) - apply (rule exI[where x=0], simp) + apply (rule exI[where x="- 1"], simp) done -lemma collinear_lemma: "collinear {(0::real^_),x,y} \ x = 0 \ y = 0 \ (\c. y = c *s x)" (is "?lhs \ ?rhs") +lemma collinear_lemma: "collinear {0,x,y} \ x = 0 \ y = 0 \ (\c. y = c *\<^sub>R x)" (is "?lhs \ ?rhs") proof- {assume "x=0 \ y = 0" hence ?thesis by (cases "x = 0", simp_all add: collinear_2 insert_commute)} moreover {assume x: "x \ 0" and y: "y \ 0" {assume h: "?lhs" - then obtain u where u: "\ x\ {0,x,y}. \y\ {0,x,y}. \c. x - y = c *s u" unfolding collinear_def by blast + then obtain u where u: "\ x\ {0,x,y}. \y\ {0,x,y}. \c. x - y = c *\<^sub>R u" unfolding collinear_def by blast from u[rule_format, of x 0] u[rule_format, of y 0] obtain cx and cy where - cx: "x = cx*s u" and cy: "y = cy*s u" + cx: "x = cx *\<^sub>R u" and cy: "y = cy *\<^sub>R u" by auto from cx x have cx0: "cx \ 0" by auto from cy y have cy0: "cy \ 0" by auto let ?d = "cy / cx" - from cx cy cx0 have "y = ?d *s x" + from cx cy cx0 have "y = ?d *\<^sub>R x" by (simp add: vector_smult_assoc) hence ?rhs using x y by blast} moreover {assume h: "?rhs" - then obtain c where c: "y = c*s x" using x y by blast + then obtain c where c: "y = c *\<^sub>R x" using x y by blast have ?lhs unfolding collinear_def c apply (rule exI[where x=x]) apply auto - apply (rule exI[where x="- 1"], simp only: vector_smult_lneg vector_smult_lid) - apply (rule exI[where x= "-c"], simp only: vector_smult_lneg) + apply (rule exI[where x="- 1"], simp) + apply (rule exI[where x= "-c"], simp) apply (rule exI[where x=1], simp) - apply (rule exI[where x="1 - c"], simp add: vector_smult_lneg vector_sub_rdistrib) - apply (rule exI[where x="c - 1"], simp add: vector_smult_lneg vector_sub_rdistrib) + apply (rule exI[where x="1 - c"], simp add: scaleR_left_diff_distrib) + apply (rule exI[where x="c - 1"], simp add: scaleR_left_diff_distrib) done} ultimately have ?thesis by blast} ultimately show ?thesis by blast qed lemma norm_cauchy_schwarz_equal: - fixes x y :: "real ^ 'n" - shows "abs(x \ y) = norm x * norm y \ collinear {(0::real^'n),x,y}" + shows "abs(x \ y) = norm x * norm y \ collinear {0,x,y}" unfolding norm_cauchy_schwarz_abs_eq apply (cases "x=0", simp_all add: collinear_2) apply (cases "y=0", simp_all add: collinear_2 insert_commute) @@ -4602,20 +3914,20 @@ apply (subgoal_tac "norm x \ 0") apply (subgoal_tac "norm y \ 0") apply (rule iffI) -apply (cases "norm x *s y = norm y *s x") +apply (cases "norm x *\<^sub>R y = norm y *\<^sub>R x") apply (rule exI[where x="(1/norm x) * norm y"]) apply (drule sym) -unfolding vector_smult_assoc[symmetric] +unfolding scaleR_scaleR[symmetric] apply (simp add: vector_smult_assoc field_simps) apply (rule exI[where x="(1/norm x) * - norm y"]) apply clarify apply (drule sym) -unfolding vector_smult_assoc[symmetric] +unfolding scaleR_scaleR[symmetric] apply (simp add: vector_smult_assoc field_simps) apply (erule exE) apply (erule ssubst) -unfolding vector_smult_assoc -unfolding norm_mul +unfolding scaleR_scaleR +unfolding norm_scaleR apply (subgoal_tac "norm x * c = \c\ * norm x \ norm x * c = - \c\ * norm x") apply (case_tac "c <= 0", simp add: field_simps) apply (simp add: field_simps) diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Multivariate_Analysis/Fashoda.thy --- a/src/HOL/Multivariate_Analysis/Fashoda.thy Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Mon May 03 07:59:51 2010 +0200 @@ -4,7 +4,7 @@ header {* Fashoda meet theorem. *} theory Fashoda -imports Brouwer_Fixpoint Vec1 +imports Brouwer_Fixpoint Vec1 Path_Connected begin subsection {*Fashoda meet theorem. *} @@ -47,7 +47,7 @@ apply(rule continuous_on_mul ) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def]) apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof- show "bounded_linear negatex" apply(rule bounded_linearI') unfolding Cart_eq proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real - show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *s x) $ i = (c *s negatex x) $ i" + show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i" apply-apply(case_tac[!] "i\1") prefer 3 apply(drule_tac[1-2] 21) unfolding negatex_def by(auto simp add:vector_2 ) qed qed(insert x0, auto) have 3:"(negatex \ sqprojection \ ?F) ` {- 1..1} \ {- 1..1}" unfolding subset_eq apply rule proof- diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Mon May 03 07:59:51 2010 +0200 @@ -5,7 +5,7 @@ header {* Definition of finite Cartesian product types. *} theory Finite_Cartesian_Product -imports Main +imports Inner_Product L2_Norm Numeral_Type begin subsection {* Finite Cartesian products, with indexing and lambdas. *} @@ -53,46 +53,410 @@ lemma Cart_lambda_eta: "(\ i. (g$i)) = g" by (simp add: Cart_eq) -text{* A non-standard sum to "paste" Cartesian products. *} + +subsection {* Group operations and class instances *} + +instantiation cart :: (zero,finite) zero +begin + definition vector_zero_def : "0 \ (\ i. 0)" + instance .. +end -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)))" +instantiation cart :: (plus,finite) plus +begin + definition vector_add_def : "op + \ (\ x y. (\ i. (x$i) + (y$i)))" + instance .. +end -lemma nth_pastecart_Inl [simp]: "pastecart f g $ Inl a = f$a" - unfolding pastecart_def by simp +instantiation cart :: (minus,finite) minus +begin + definition vector_minus_def : "op - \ (\ x y. (\ i. (x$i) - (y$i)))" + instance .. +end + +instantiation cart :: (uminus,finite) uminus +begin + definition vector_uminus_def : "uminus \ (\ x. (\ i. - (x$i)))" + instance .. +end -lemma nth_pastecart_Inr [simp]: "pastecart f g $ Inr b = g$b" - unfolding pastecart_def by simp +lemma zero_index [simp]: "0 $ i = 0" + unfolding vector_zero_def by simp + +lemma vector_add_component [simp]: "(x + y)$i = x$i + y$i" + unfolding vector_add_def by simp + +lemma vector_minus_component [simp]: "(x - y)$i = x$i - y$i" + unfolding vector_minus_def by simp + +lemma vector_uminus_component [simp]: "(- x)$i = - (x$i)" + unfolding vector_uminus_def by simp + +instance cart :: (semigroup_add, finite) semigroup_add + by default (simp add: Cart_eq add_assoc) -lemma nth_fstcart [simp]: "fstcart f $ i = f $ Inl i" - unfolding fstcart_def by simp +instance cart :: (ab_semigroup_add, finite) ab_semigroup_add + by default (simp add: Cart_eq add_commute) + +instance cart :: (monoid_add, finite) monoid_add + by default (simp_all add: Cart_eq) -lemma nth_sndtcart [simp]: "sndcart f $ i = f $ Inr i" - unfolding sndcart_def by simp +instance cart :: (comm_monoid_add, finite) comm_monoid_add + by default (simp add: Cart_eq) + +instance cart :: (cancel_semigroup_add, finite) cancel_semigroup_add + by default (simp_all add: Cart_eq) + +instance cart :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add + by default (simp add: Cart_eq) + +instance cart :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. -lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \ range Inr" - apply auto - apply (case_tac x) - apply auto - done +instance cart :: (group_add, finite) group_add + by default (simp_all add: Cart_eq diff_minus) + +instance cart :: (ab_group_add, finite) ab_group_add + by default (simp_all add: Cart_eq) + + +subsection {* Real vector space *} + +instantiation cart :: (real_vector, finite) real_vector +begin + +definition vector_scaleR_def: "scaleR = (\ r x. (\ i. scaleR r (x$i)))" -lemma fstcart_pastecart[simp]: "fstcart (pastecart x y) = x" - by (simp add: Cart_eq) +lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)" + unfolding vector_scaleR_def by simp + +instance + by default (simp_all add: Cart_eq scaleR_left_distrib scaleR_right_distrib) -lemma sndcart_pastecart[simp]: "sndcart (pastecart x y) = y" - by (simp add: Cart_eq) +end + + +subsection {* Topological space *} + +instantiation cart :: (topological_space, finite) topological_space +begin -lemma pastecart_fst_snd[simp]: "pastecart (fstcart z) (sndcart z) = z" - by (simp add: Cart_eq pastecart_def fstcart_def sndcart_def split: sum.split) - -lemma pastecart_eq: "(x = y) \ (fstcart x = fstcart y) \ (sndcart x = sndcart y)" - using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis +definition open_vector_def: + "open (S :: ('a ^ 'b) set) \ + (\x\S. \A. (\i. open (A i) \ x$i \ A i) \ + (\y. (\i. y$i \ A i) \ y \ S))" -lemma forall_pastecart: "(\p. P p) \ (\x y. P (pastecart x y))" - by (metis pastecart_fst_snd) - -lemma exists_pastecart: "(\p. P p) \ (\x y. P (pastecart x y))" - by (metis pastecart_fst_snd) +instance proof + show "open (UNIV :: ('a ^ 'b) set)" + unfolding open_vector_def by auto +next + fix S T :: "('a ^ 'b) set" + assume "open S" "open T" thus "open (S \ T)" + unfolding open_vector_def + apply clarify + apply (drule (1) bspec)+ + apply (clarify, rename_tac Sa Ta) + apply (rule_tac x="\i. Sa i \ Ta i" in exI) + apply (simp add: open_Int) + done +next + fix K :: "('a ^ 'b) set set" + assume "\S\K. open S" thus "open (\K)" + unfolding open_vector_def + apply clarify + apply (drule (1) bspec) + apply (drule (1) bspec) + apply clarify + apply (rule_tac x=A in exI) + apply fast + done +qed end + +lemma open_vector_box: "\i. open (S i) \ open {x. \i. x $ i \ S i}" +unfolding open_vector_def by auto + +lemma open_vimage_Cart_nth: "open S \ open ((\x. x $ i) -` S)" +unfolding open_vector_def +apply clarify +apply (rule_tac x="\k. if k = i then S else UNIV" in exI, simp) +done + +lemma closed_vimage_Cart_nth: "closed S \ closed ((\x. x $ i) -` S)" +unfolding closed_open vimage_Compl [symmetric] +by (rule open_vimage_Cart_nth) + +lemma closed_vector_box: "\i. closed (S i) \ closed {x. \i. x $ i \ S i}" +proof - + have "{x. \i. x $ i \ S i} = (\i. (\x. x $ i) -` S i)" by auto + thus "\i. closed (S i) \ closed {x. \i. x $ i \ S i}" + by (simp add: closed_INT closed_vimage_Cart_nth) +qed + +lemma tendsto_Cart_nth [tendsto_intros]: + assumes "((\x. f x) ---> a) net" + shows "((\x. f x $ i) ---> a $ i) net" +proof (rule topological_tendstoI) + fix S assume "open S" "a $ i \ S" + then have "open ((\y. y $ i) -` S)" "a \ ((\y. y $ i) -` S)" + by (simp_all add: open_vimage_Cart_nth) + with assms have "eventually (\x. f x \ (\y. y $ i) -` S) net" + by (rule topological_tendstoD) + then show "eventually (\x. f x $ i \ S) net" + by simp +qed + +lemma eventually_Ball_finite: (* TODO: move *) + assumes "finite A" and "\y\A. eventually (\x. P x y) net" + shows "eventually (\x. \y\A. P x y) net" +using assms by (induct set: finite, simp, simp add: eventually_conj) + +lemma eventually_all_finite: (* TODO: move *) + fixes P :: "'a \ 'b::finite \ bool" + assumes "\y. eventually (\x. P x y) net" + shows "eventually (\x. \y. P x y) net" +using eventually_Ball_finite [of UNIV P] assms by simp + +lemma tendsto_vector: + assumes "\i. ((\x. f x $ i) ---> a $ i) net" + shows "((\x. f x) ---> a) net" +proof (rule topological_tendstoI) + fix S assume "open S" and "a \ S" + then obtain A where A: "\i. open (A i)" "\i. a $ i \ A i" + and S: "\y. \i. y $ i \ A i \ y \ S" + unfolding open_vector_def by metis + have "\i. eventually (\x. f x $ i \ A i) net" + using assms A by (rule topological_tendstoD) + hence "eventually (\x. \i. f x $ i \ A i) net" + by (rule eventually_all_finite) + thus "eventually (\x. f x \ S) net" + by (rule eventually_elim1, simp add: S) +qed + +lemma tendsto_Cart_lambda [tendsto_intros]: + assumes "\i. ((\x. f x i) ---> a i) net" + shows "((\x. \ i. f x i) ---> (\ i. a i)) net" +using assms by (simp add: tendsto_vector) + + +subsection {* Metric *} + +(* TODO: move somewhere else *) +lemma finite_choice: "finite A \ \x\A. \y. P x y \ \f. \x\A. P x (f x)" +apply (induct set: finite, simp_all) +apply (clarify, rename_tac y) +apply (rule_tac x="f(x:=y)" in exI, simp) +done + +instantiation cart :: (metric_space, finite) metric_space +begin + +definition dist_vector_def: + "dist x y = setL2 (\i. dist (x$i) (y$i)) UNIV" + +lemma dist_nth_le: "dist (x $ i) (y $ i) \ dist x y" +unfolding dist_vector_def +by (rule member_le_setL2) simp_all + +instance proof + fix x y :: "'a ^ 'b" + show "dist x y = 0 \ x = y" + unfolding dist_vector_def + by (simp add: setL2_eq_0_iff Cart_eq) +next + fix x y z :: "'a ^ 'b" + show "dist x y \ dist x z + dist y z" + unfolding dist_vector_def + apply (rule order_trans [OF _ setL2_triangle_ineq]) + apply (simp add: setL2_mono dist_triangle2) + done +next + (* FIXME: long proof! *) + fix S :: "('a ^ 'b) set" + show "open S \ (\x\S. \e>0. \y. dist y x < e \ y \ S)" + unfolding open_vector_def open_dist + apply safe + apply (drule (1) bspec) + apply clarify + apply (subgoal_tac "\e>0. \i y. dist y (x$i) < e \ y \ A i") + apply clarify + apply (rule_tac x=e in exI, clarify) + apply (drule spec, erule mp, clarify) + apply (drule spec, drule spec, erule mp) + apply (erule le_less_trans [OF dist_nth_le]) + apply (subgoal_tac "\i\UNIV. \e>0. \y. dist y (x$i) < e \ y \ A i") + apply (drule finite_choice [OF finite], clarify) + apply (rule_tac x="Min (range f)" in exI, simp) + apply clarify + apply (drule_tac x=i in spec, clarify) + apply (erule (1) bspec) + apply (drule (1) bspec, clarify) + apply (subgoal_tac "\r. (\i::'b. 0 < r i) \ e = setL2 r UNIV") + apply clarify + apply (rule_tac x="\i. {y. dist y (x$i) < r i}" in exI) + apply (rule conjI) + apply clarify + apply (rule conjI) + apply (clarify, rename_tac y) + apply (rule_tac x="r i - dist y (x$i)" in exI, rule conjI, simp) + apply clarify + apply (simp only: less_diff_eq) + apply (erule le_less_trans [OF dist_triangle]) + apply simp + apply clarify + apply (drule spec, erule mp) + apply (simp add: dist_vector_def setL2_strict_mono) + apply (rule_tac x="\i. e / sqrt (of_nat CARD('b))" in exI) + apply (simp add: divide_pos_pos setL2_constant) + done +qed + +end + +lemma LIMSEQ_Cart_nth: + "(X ----> a) \ (\n. X n $ i) ----> a $ i" +unfolding LIMSEQ_conv_tendsto by (rule tendsto_Cart_nth) + +lemma LIM_Cart_nth: + "(f -- x --> y) \ (\x. f x $ i) -- x --> y $ i" +unfolding LIM_conv_tendsto by (rule tendsto_Cart_nth) + +lemma Cauchy_Cart_nth: + "Cauchy (\n. X n) \ Cauchy (\n. X n $ i)" +unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_nth_le]) + +lemma LIMSEQ_vector: + assumes "\i. (\n. X n $ i) ----> (a $ i)" + shows "X ----> a" +using assms unfolding LIMSEQ_conv_tendsto by (rule tendsto_vector) + +lemma Cauchy_vector: + fixes X :: "nat \ 'a::metric_space ^ 'n" + assumes X: "\i. Cauchy (\n. X n $ i)" + shows "Cauchy (\n. X n)" +proof (rule metric_CauchyI) + fix r :: real assume "0 < r" + then have "0 < r / of_nat CARD('n)" (is "0 < ?s") + by (simp add: divide_pos_pos) + def N \ "\i. LEAST N. \m\N. \n\N. dist (X m $ i) (X n $ i) < ?s" + def M \ "Max (range N)" + have "\i. \N. \m\N. \n\N. dist (X m $ i) (X n $ i) < ?s" + using X `0 < ?s` by (rule metric_CauchyD) + hence "\i. \m\N i. \n\N i. dist (X m $ i) (X n $ i) < ?s" + unfolding N_def by (rule LeastI_ex) + hence M: "\i. \m\M. \n\M. dist (X m $ i) (X n $ i) < ?s" + unfolding M_def by simp + { + fix m n :: nat + assume "M \ m" "M \ n" + have "dist (X m) (X n) = setL2 (\i. dist (X m $ i) (X n $ i)) UNIV" + unfolding dist_vector_def .. + also have "\ \ setsum (\i. dist (X m $ i) (X n $ i)) UNIV" + by (rule setL2_le_setsum [OF zero_le_dist]) + also have "\ < setsum (\i::'n. ?s) UNIV" + by (rule setsum_strict_mono, simp_all add: M `M \ m` `M \ n`) + also have "\ = r" + by simp + finally have "dist (X m) (X n) < r" . + } + hence "\m\M. \n\M. dist (X m) (X n) < r" + by simp + then show "\M. \m\M. \n\M. dist (X m) (X n) < r" .. +qed + +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)" + using Cauchy_Cart_nth [OF `Cauchy X`] + by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) + hence "X ----> Cart_lambda (\i. lim (\n. X n $ i))" + by (simp add: LIMSEQ_vector) + then show "convergent X" + by (rule convergentI) +qed + + +subsection {* Normed vector space *} + +instantiation cart :: (real_normed_vector, finite) real_normed_vector +begin + +definition norm_vector_def: + "norm x = setL2 (\i. norm (x$i)) UNIV" + +definition vector_sgn_def: + "sgn (x::'a^'b) = scaleR (inverse (norm x)) x" + +instance proof + fix a :: real and x y :: "'a ^ 'b" + show "0 \ norm x" + unfolding norm_vector_def + by (rule setL2_nonneg) + show "norm x = 0 \ x = 0" + unfolding norm_vector_def + by (simp add: setL2_eq_0_iff Cart_eq) + show "norm (x + y) \ norm x + norm y" + unfolding norm_vector_def + apply (rule order_trans [OF _ setL2_triangle_ineq]) + apply (simp add: setL2_mono norm_triangle_ineq) + done + show "norm (scaleR a x) = \a\ * norm x" + unfolding norm_vector_def + by (simp add: setL2_right_distrib) + show "sgn x = scaleR (inverse (norm x)) x" + by (rule vector_sgn_def) + show "dist x y = norm (x - y)" + unfolding dist_vector_def norm_vector_def + by (simp add: dist_norm) +qed + +end + +lemma norm_nth_le: "norm (x $ i) \ norm x" +unfolding norm_vector_def +by (rule member_le_setL2) simp_all + +interpretation Cart_nth: bounded_linear "\x. x $ i" +apply default +apply (rule vector_add_component) +apply (rule vector_scaleR_component) +apply (rule_tac x="1" in exI, simp add: norm_nth_le) +done + +instance cart :: (banach, finite) banach .. + + +subsection {* Inner product space *} + +instantiation cart :: (real_inner, finite) real_inner +begin + +definition inner_vector_def: + "inner x y = setsum (\i. inner (x$i) (y$i)) UNIV" + +instance proof + fix r :: real and x y z :: "'a ^ 'b" + show "inner x y = inner y x" + unfolding inner_vector_def + by (simp add: inner_commute) + show "inner (x + y) z = inner x z + inner y z" + unfolding inner_vector_def + by (simp add: inner_add_left setsum_addf) + show "inner (scaleR r x) y = r * inner x y" + unfolding inner_vector_def + by (simp add: setsum_right_distrib) + show "0 \ inner x x" + unfolding inner_vector_def + by (simp add: setsum_nonneg) + show "inner x x = 0 \ x = 0" + unfolding inner_vector_def + by (simp add: Cart_eq setsum_nonneg_eq_0_iff) + show "norm x = sqrt (inner x x)" + unfolding inner_vector_def norm_vector_def setL2_def + by (simp add: power2_norm_eq_inner) +qed + +end + +end diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Multivariate_Analysis/Integration.thy --- a/src/HOL/Multivariate_Analysis/Integration.thy Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Integration.thy Mon May 03 07:59:51 2010 +0200 @@ -137,27 +137,27 @@ hence "\x. ball x (e/2) \ s \ (\f)" proof(erule_tac disjE) let ?z = "x - (e/2) *\<^sub>R basis k" assume as:"x$k = a$k" have "ball ?z (e / 2) \ i = {}" apply(rule ccontr) unfolding ex_in_conv[THEN sym] proof(erule exE) fix y assume "y \ ball ?z (e / 2) \ i" hence "dist ?z y < e/2" and yi:"y\i" by auto - hence "\(?z - y) $ k\ < e/2" using component_le_norm[of "?z - y" k] unfolding vector_dist_norm by auto + hence "\(?z - y) $ k\ < e/2" using component_le_norm[of "?z - y" k] unfolding dist_norm by auto hence "y$k < a$k" unfolding vector_component_simps vector_scaleR_component as using e[THEN conjunct1] by(auto simp add:field_simps) hence "y \ i" unfolding ab mem_interval not_all by(rule_tac x=k in exI,auto) thus False using yi by auto qed moreover have "ball ?z (e/2) \ s \ (\insert i f)" apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) proof fix y assume as:"y\ ball ?z (e/2)" have "norm (x - y) \ \e\ / 2 + norm (x - y - (e / 2) *\<^sub>R basis k)" apply-apply(rule order_trans,rule norm_triangle_sub[of "x - y" "(e/2) *\<^sub>R basis k"]) unfolding norm_scaleR norm_basis by auto - also have "\ < \e\ / 2 + \e\ / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball vector_dist_norm using e by(auto simp add:field_simps) - finally show "y\ball x e" unfolding mem_ball vector_dist_norm using e by(auto simp add:field_simps) qed + also have "\ < \e\ / 2 + \e\ / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball dist_norm using e by(auto simp add:field_simps) + finally show "y\ball x e" unfolding mem_ball dist_norm using e by(auto simp add:field_simps) qed ultimately show ?thesis apply(rule_tac x="?z" in exI) unfolding Union_insert by auto next let ?z = "x + (e/2) *\<^sub>R basis k" assume as:"x$k = b$k" have "ball ?z (e / 2) \ i = {}" apply(rule ccontr) unfolding ex_in_conv[THEN sym] proof(erule exE) fix y assume "y \ ball ?z (e / 2) \ i" hence "dist ?z y < e/2" and yi:"y\i" by auto - hence "\(?z - y) $ k\ < e/2" using component_le_norm[of "?z - y" k] unfolding vector_dist_norm by auto + hence "\(?z - y) $ k\ < e/2" using component_le_norm[of "?z - y" k] unfolding dist_norm by auto hence "y$k > b$k" unfolding vector_component_simps vector_scaleR_component as using e[THEN conjunct1] by(auto simp add:field_simps) hence "y \ i" unfolding ab mem_interval not_all by(rule_tac x=k in exI,auto) thus False using yi by auto qed moreover have "ball ?z (e/2) \ s \ (\insert i f)" apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) proof fix y assume as:"y\ ball ?z (e/2)" have "norm (x - y) \ \e\ / 2 + norm (x - y + (e / 2) *\<^sub>R basis k)" apply-apply(rule order_trans,rule norm_triangle_sub[of "x - y" "- (e/2) *\<^sub>R basis k"]) unfolding norm_scaleR norm_basis by auto - also have "\ < \e\ / 2 + \e\ / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball vector_dist_norm using e by(auto simp add:field_simps) - finally show "y\ball x e" unfolding mem_ball vector_dist_norm using e by(auto simp add:field_simps) qed + also have "\ < \e\ / 2 + \e\ / 2" apply(rule add_strict_left_mono) using as unfolding mem_ball dist_norm using e by(auto simp add:field_simps) + finally show "y\ball x e" unfolding mem_ball dist_norm using e by(auto simp add:field_simps) qed ultimately show ?thesis apply(rule_tac x="?z" in exI) unfolding Union_insert by auto qed then guess x .. hence "x \ s \ interior (\f)" unfolding lem1[where U="\f",THEN sym] using centre_in_ball e[THEN conjunct1] by auto thus ?thesis apply-apply(rule lem2,rule insert(3)) using insert(4) by auto qed qed qed qed note * = this @@ -1067,7 +1067,7 @@ proof- case goal1 guess n using real_arch_pow2[of "(setsum (\i. b$i - a$i) UNIV) / e"] .. note n=this show ?case apply(rule_tac x=n in exI) proof(rule,rule) fix x y assume xy:"x\{A n..B n}" "y\{A n..B n}" - have "dist x y \ setsum (\i. abs((x - y)$i)) UNIV" unfolding vector_dist_norm by(rule norm_le_l1) + have "dist x y \ setsum (\i. abs((x - y)$i)) UNIV" unfolding dist_norm by(rule norm_le_l1) also have "\ \ setsum (\i. B n$i - A n$i) UNIV" proof(rule setsum_mono) fix i show "\(x - y) $ i\ \ B n $ i - A n $ i" using xy[unfolded mem_interval,THEN spec[where x=i]] @@ -1417,7 +1417,7 @@ show ?case apply(rule_tac x=d in exI,rule,rule d) apply(rule,rule,rule,(erule conjE)+) proof- fix p1 p2 assume as:"p1 tagged_division_of {a..b}" "d fine p1" "p2 tagged_division_of {a..b}" "d fine p2" show "norm ((\(x, k)\p1. content k *\<^sub>R f x) - (\(x, k)\p2. content k *\<^sub>R f x)) < e" - apply(rule dist_triangle_half_l[where y=y,unfolded vector_dist_norm]) + apply(rule dist_triangle_half_l[where y=y,unfolded dist_norm]) using d(2)[OF conjI[OF as(1-2)]] d(2)[OF conjI[OF as(3-4)]] . qed qed next assume "\e>0. \d. ?P e d" hence "\n::nat. \d. ?P (inverse(real (n + 1))) d" by auto @@ -1447,7 +1447,7 @@ have *:"inverse (real (N1 + N2 + 1)) < e / 2" apply(rule less_trans) using N1 by auto show "norm ((\(x, k)\q. content k *\<^sub>R f x) - y) < e" apply(rule norm_triangle_half_r) apply(rule less_trans[OF _ *]) apply(subst N1', rule d(2)[of "p (N1+N2)"]) defer - using N2[rule_format,unfolded vector_dist_norm,of "N1+N2"] + using N2[rule_format,unfolded dist_norm,of "N1+N2"] using as dp[of "N1 - 1 + 1 + N2" "N1 + N2"] using p(1)[of "N1 + N2"] using N1 by auto qed qed qed subsection {* Additivity of integral on abutting intervals. *} @@ -1554,7 +1554,7 @@ using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto hence "\y. y \ ball x \x $ k - c\ \ {x. x $ k \ c}" using goal1(1) by blast then guess y .. hence "\x $ k - y $ k\ < \x $ k - c\" "y$k \ c" apply-apply(rule le_less_trans) - using component_le_norm[of "x - y" k,unfolded vector_minus_component] by(auto simp add:vector_dist_norm) + using component_le_norm[of "x - y" k,unfolded vector_minus_component] by(auto simp add:dist_norm) thus False using goal1(2)[unfolded not_le] by(auto simp add:field_simps) qed show "~(kk \ {x. x$k \ c} = {}) \ x$k \ c" @@ -1563,7 +1563,7 @@ using p(2)[unfolded fine_def,rule_format,OF as,unfolded split_conv] by auto hence "\y. y \ ball x \x $ k - c\ \ {x. x $ k \ c}" using goal1(1) by blast then guess y .. hence "\x $ k - y $ k\ < \x $ k - c\" "y$k \ c" apply-apply(rule le_less_trans) - using component_le_norm[of "x - y" k,unfolded vector_minus_component] by(auto simp add:vector_dist_norm) + using component_le_norm[of "x - y" k,unfolded vector_minus_component] by(auto simp add:dist_norm) thus False using goal1(2)[unfolded not_le] by(auto simp add:field_simps) qed qed @@ -1676,7 +1676,7 @@ then guess e unfolding mem_interior .. note e=this have x:"x$k = c" using x interior_subset by fastsimp have *:"\i. \(x - (x + (\ i. if i = k then e / 2 else 0))) $ i\ = (if i = k then e/2 else 0)" using e by auto - have "x + (\ i. if i = k then e/2 else 0) \ ball x e" unfolding mem_ball vector_dist_norm + have "x + (\ i. if i = k then e/2 else 0) \ ball x e" unfolding mem_ball dist_norm apply(rule le_less_trans[OF norm_le_l1]) unfolding * unfolding setsum_delta[OF finite_UNIV] using e by auto hence "x + (\ i. if i = k then e/2 else 0) \ {x. x$k = c}" using e by auto @@ -2384,7 +2384,7 @@ also have "\ < e" using goal1 unfolding norm_minus_commute by(auto simp add:algebra_simps) finally show ?case . qed - show ?case unfolding vector_dist_norm apply(rule lem2) defer + show ?case unfolding dist_norm apply(rule lem2) defer apply(rule gm(2)[OF conjI[OF p(1)]],rule_tac[2] gn(2)[OF conjI[OF p(1)]]) using conjunctD2[OF p(2)[unfolded fine_inter]] apply- apply assumption+ apply(rule order_trans) apply(rule rsum_diff_bound[OF p(1), where e="2 / real M"]) @@ -2426,7 +2426,7 @@ apply-apply(rule less_le_trans,assumption) using `e>0` by auto thus "inverse (real (N1 + N2) + 1) * content {a..b} \ e / 3" unfolding inverse_eq_divide by(auto simp add:field_simps) - show "norm (i (N1 + N2) - s) < e / 3" by(rule N1[rule_format,unfolded vector_dist_norm],auto) + show "norm (i (N1 + N2) - s) < e / 3" by(rule N1[rule_format,unfolded dist_norm],auto) qed qed qed qed subsection {* Negligible sets. *} @@ -2510,7 +2510,7 @@ show "content l = content (l \ {x. \x $ k - c\ \ d})" apply(rule arg_cong[where f=content]) apply(rule set_ext,rule,rule) unfolding mem_Collect_eq proof- fix y assume y:"y\l" note p[THEN conjunct2,unfolded fine_def,rule_format,OF as(1),unfolded split_conv] - note this[unfolded subset_eq mem_ball vector_dist_norm,rule_format,OF y] note le_less_trans[OF component_le_norm[of _ k] this] + note this[unfolded subset_eq mem_ball dist_norm,rule_format,OF y] note le_less_trans[OF component_le_norm[of _ k] this] thus "\y $ k - c\ \ d" unfolding Cart_nth.diff xk by auto qed auto qed note p'= tagged_division_ofD[OF p[THEN conjunct1]] and p''=division_of_tagged_division[OF p[THEN conjunct1]] @@ -2837,7 +2837,7 @@ proof safe show "(\y. f x) integrable_on l" unfolding integrable_on_def l by(rule,rule has_integral_const) fix y assume y:"y\l" note fineD[OF p(2) as,unfolded subset_eq,rule_format,OF this] note d(2)[OF _ _ this[unfolded mem_ball]] - thus "norm (f y - f x) \ e" using y p'(2-3)[OF as] unfolding vector_dist_norm l norm_minus_commute by fastsimp qed qed + thus "norm (f y - f x) \ e" using y p'(2-3)[OF as] unfolding dist_norm l norm_minus_commute by fastsimp qed qed from e have "0 \ e" by auto from approximable_on_division[OF this division_of_tagged_division[OF p(1)] *] guess g . thus "\g. (\x\{a..b}. norm (f x - g x) \ e) \ g integrable_on {a..b}" by auto qed @@ -2960,9 +2960,9 @@ apply(rule add_mono) apply(rule d(2)[of "x$1" "u$1",unfolded o_def vec1_dest_vec1]) prefer 4 apply(rule d(2)[of "x$1" "v$1",unfolded o_def vec1_dest_vec1]) using ball[rule_format,of u] ball[rule_format,of v] - using xk(1-2) unfolding k subset_eq by(auto simp add:vector_dist_norm norm_real) + using xk(1-2) unfolding k subset_eq by(auto simp add:dist_norm norm_real) also have "... \ e * dest_vec1 (interval_upperbound k - interval_lowerbound k)" - unfolding k interval_bound_1[OF *] using xk(1) unfolding k by(auto simp add:vector_dist_norm norm_real field_simps) + unfolding k interval_bound_1[OF *] using xk(1) unfolding k by(auto simp add:dist_norm norm_real field_simps) finally show "norm (content k *\<^sub>R f' x - (f (interval_upperbound k) - f (interval_lowerbound k))) \ e * dest_vec1 (interval_upperbound k - interval_lowerbound k)" unfolding k interval_bound_1[OF *] content_1[OF *] . qed(insert as, auto) qed qed @@ -3011,7 +3011,7 @@ proof- show "\(y - x) $ i\ < e" unfolding y_def Cart_lambda_beta vector_minus_component if_P[OF refl] apply(cases) apply(subst if_P,assumption) unfolding if_not_P unfolding i xi using di as(2) by auto show "(\i\UNIV - {i}. \(y - x) $ i\) \ (\i\UNIV. 0)" unfolding y_def by auto - qed auto thus "dist y x < e" unfolding vector_dist_norm by auto + qed auto thus "dist y x < e" unfolding dist_norm by auto have "y\k" unfolding k mem_interval apply rule apply(erule_tac x=i in allE) using xyi unfolding k i xi by auto moreover have "y \ \s" unfolding s mem_interval proof note simps = y_def Cart_lambda_beta if_not_P @@ -3107,7 +3107,7 @@ have *:"y - x = norm(y - x)" using False by auto show "((\xa. f x) has_integral (y - x) *\<^sub>R f x) {vec1 x..vec1 y}" apply(subst *) unfolding ** by auto show "\xa\{vec1 x..vec1 y}. norm (f (dest_vec1 xa) - f x) \ e" apply safe apply(rule less_imp_le) - apply(rule d(2)[unfolded vector_dist_norm]) using assms(2) using goal1 by auto + apply(rule d(2)[unfolded dist_norm]) using assms(2) using goal1 by auto qed(insert e,auto) next case True have "f \ dest_vec1 integrable_on {vec1 a..vec1 x}" apply(rule integrable_subinterval,rule integrable_continuous) apply(rule continuous_on_o_dest_vec1 assms)+ unfolding not_less using assms(2) goal1 by auto @@ -3124,7 +3124,7 @@ have *:"x - y = norm(y - x)" using True by auto show "((\xa. f x) has_integral (x - y) *\<^sub>R f x) {vec1 y..vec1 x}" apply(subst *) unfolding ** by auto show "\xa\{vec1 y..vec1 x}. norm (f (dest_vec1 xa) - f x) \ e" apply safe apply(rule less_imp_le) - apply(rule d(2)[unfolded vector_dist_norm]) using assms(2) using goal1 by auto + apply(rule d(2)[unfolded dist_norm]) using assms(2) using goal1 by auto qed(insert e,auto) qed qed qed lemma integral_has_vector_derivative': fixes f::"real^1 \ 'a::banach" @@ -3375,7 +3375,7 @@ proof(rule add_mono) case goal1 have "\c - a\ \ \l\" using as' by auto thus ?case apply-apply(rule order_trans[OF _ l(2)]) unfolding norm_scaleR apply(rule mult_right_mono) by auto next case goal2 show ?case apply(rule less_imp_le) apply(cases "a = c") defer - apply(rule k(2)[unfolded vector_dist_norm]) using as' e ab by(auto simp add:field_simps) + apply(rule k(2)[unfolded dist_norm]) using as' e ab by(auto simp add:field_simps) qed finally show "norm (content {vec1 a..vec1 c} *\<^sub>R f' a - (f c - f a)) \ e * (b - a) / 4" unfolding content_1'[OF as(1)] by auto qed qed then guess da .. note da=conjunctD2[OF this,rule_format] @@ -3399,7 +3399,7 @@ proof(rule add_mono) case goal1 have "\c - b\ \ \l\" using as' by auto thus ?case apply-apply(rule order_trans[OF _ l(2)]) unfolding norm_scaleR apply(rule mult_right_mono) by auto next case goal2 show ?case apply(rule less_imp_le) apply(cases "b = c") defer apply(subst norm_minus_commute) - apply(rule k(2)[unfolded vector_dist_norm]) using as' e ab by(auto simp add:field_simps) + apply(rule k(2)[unfolded dist_norm]) using as' e ab by(auto simp add:field_simps) qed finally show "norm (content {vec1 c..vec1 b} *\<^sub>R f' b - (f b - f c)) \ e * (b - a) / 4" unfolding content_1'[OF as(1)] by auto qed qed then guess db .. note db=conjunctD2[OF this,rule_format] @@ -3663,11 +3663,11 @@ proof- assume "x=a" have "a \ a" by auto from indefinite_integral_continuous_right[OF assms(1) this `a0`] guess d . note d=this show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute) - unfolding `x=a` vector_dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto + unfolding `x=a` dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto next assume "x=b" have "b \ b" by auto from indefinite_integral_continuous_left[OF assms(1) `a0`] guess d . note d=this show ?thesis apply(rule,rule,rule d,safe) apply(subst dist_commute) - unfolding `x=b` vector_dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto + unfolding `x=b` dist_norm apply(rule d(2)[rule_format]) unfolding norm_real by auto next assume "a xb" and xr:"a\x" "x0`] guess d1 . note d1=this from indefinite_integral_continuous_right[OF assms(1) xr `e>0`] guess d2 . note d2=this @@ -3675,7 +3675,7 @@ proof safe show "0 < min d1 d2" using d1 d2 by auto fix y assume "y\{a..b}" "dist y x < min d1 d2" thus "dist (integral {a..y} f) (integral {a..x} f) < e" apply-apply(subst dist_commute) - apply(cases "y < x") unfolding vector_dist_norm apply(rule d1(2)[rule_format]) defer + apply(cases "y < x") unfolding dist_norm apply(rule d1(2)[rule_format]) defer apply(rule d2(2)[rule_format]) unfolding Cart_simps not_less norm_real by(auto simp add:field_simps) qed qed qed @@ -3831,7 +3831,7 @@ thus "((\x. if x \ s then f x else 0) has_integral i) {c..d}" unfolding s apply-apply(rule has_integral_restrict_closed_subinterval) apply(rule `?l`[unfolded s]) apply safe apply(drule B(2)[rule_format]) unfolding subset_eq apply(erule_tac x=x in ballE) - by(auto simp add:vector_dist_norm) + by(auto simp add:dist_norm) qed(insert B `e>0`, auto) next assume as:"\e>0. ?r e" from this[rule_format,OF zero_less_one] guess C .. note C=conjunctD2[OF this,rule_format] @@ -3839,7 +3839,7 @@ have c_d:"{a..b} \ {c..d}" apply safe apply(drule B(2)) unfolding mem_interval proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by(auto simp add:field_simps) qed - have "ball 0 C \ {c..d}" apply safe unfolding mem_interval mem_ball vector_dist_norm + have "ball 0 C \ {c..d}" apply safe unfolding mem_interval mem_ball dist_norm proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed from C(2)[OF this] have "\y. (f has_integral y) {a..b}" unfolding has_integral_restrict_closed_subintervals_eq[OF c_d,THEN sym] unfolding s by auto @@ -3851,7 +3851,7 @@ have c_d:"{a..b} \ {c..d}" apply safe apply(drule B(2)) unfolding mem_interval proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by(auto simp add:field_simps) qed - have "ball 0 C \ {c..d}" apply safe unfolding mem_interval mem_ball vector_dist_norm + have "ball 0 C \ {c..d}" apply safe unfolding mem_interval mem_ball dist_norm proof case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed note C(2)[OF this] then guess z .. note z = conjunctD2[OF this, unfolded s] note this[unfolded has_integral_restrict_closed_subintervals_eq[OF c_d]] @@ -4037,7 +4037,7 @@ from as[OF zero_less_one] guess B .. note B=conjunctD2[OF this,rule_format] let ?a = "(\ i. min (a$i) (-B))::real^'n" and ?b = "(\ i. max (b$i) B)::real^'n" show "?f integrable_on {a..b}" apply(rule integrable_subinterval[of _ ?a ?b]) - proof- have "ball 0 B \ {?a..?b}" apply safe unfolding mem_ball mem_interval vector_dist_norm + proof- have "ball 0 B \ {?a..?b}" apply safe unfolding mem_ball mem_interval dist_norm proof case goal1 thus ?case using component_le_norm[of x i] by(auto simp add:field_simps) qed from B(2)[OF this] guess z .. note conjunct1[OF this] thus "?f integrable_on {?a..?b}" unfolding integrable_on_def by auto @@ -4071,10 +4071,10 @@ from as(2)[OF this] guess B .. note B = conjunctD2[OF this,rule_format] from real_arch_simple[of B] guess N .. note N = this { fix n assume n:"n \ N" have "ball 0 B \ {\ i. - real n..\ i. real n}" apply safe - unfolding mem_ball mem_interval vector_dist_norm + unfolding mem_ball mem_interval dist_norm proof case goal1 thus ?case using component_le_norm[of x i] using n N by(auto simp add:field_simps) qed } - thus ?case apply-apply(rule_tac x=N in exI) apply safe unfolding vector_dist_norm apply(rule B(2)) by auto + thus ?case apply-apply(rule_tac x=N in exI) apply safe unfolding dist_norm apply(rule B(2)) by auto qed from this[unfolded convergent_eq_cauchy[THEN sym]] guess i .. note i = this[unfolded Lim_sequentially, rule_format] @@ -4089,11 +4089,11 @@ from real_arch_simple[of ?B] guess n .. note n=this show "norm (integral {a..b} (\x. if x \ s then f x else 0) - i) < e" apply(rule norm_triangle_half_l) apply(rule B(2)) defer apply(subst norm_minus_commute) - apply(rule N[unfolded vector_dist_norm, of n]) + apply(rule N[unfolded dist_norm, of n]) proof safe show "N \ n" using n by auto fix x::"real^'n" assume x:"x \ ball 0 B" hence "x\ ball 0 ?B" by auto thus "x\{a..b}" using ab by blast - show "x\{\ i. - real n..\ i. real n}" using x unfolding mem_interval mem_ball vector_dist_norm apply- + show "x\{\ i. - real n..\ i. real n}" using x unfolding mem_interval mem_ball dist_norm apply- proof case goal1 thus ?case using component_le_norm[of x i] using n by(auto simp add:field_simps) qed qed qed qed qed @@ -4159,7 +4159,7 @@ note obt(2)[unfolded has_integral_alt'[of h]] note conjunctD2[OF this, rule_format] note h = this(1) and this(2)[OF *] from this(2) guess B2 .. note B2 = conjunctD2[OF this,rule_format] def c \ "\ i. min (a$i) (- (max B1 B2))" and d \ "\ i. max (b$i) (max B1 B2)" - have *:"ball 0 B1 \ {c..d}" "ball 0 B2 \ {c..d}" apply safe unfolding mem_ball mem_interval vector_dist_norm + have *:"ball 0 B1 \ {c..d}" "ball 0 B2 \ {c..d}" apply safe unfolding mem_ball mem_interval dist_norm proof(rule_tac[!] allI) case goal1 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto next case goal2 thus ?case using component_le_norm[of x i] unfolding c_def d_def by auto qed @@ -4622,7 +4622,7 @@ from g(2)[unfolded Lim_sequentially,of a b,rule_format,OF this] guess M .. note M=this have **:"norm (integral {a..b} (\x. if x \ s then f N x else 0) - i) < e/2" apply(rule norm_triangle_half_l) using B(2)[rule_format,OF ab] N[rule_format,of N] - unfolding vector_dist_norm apply-defer apply(subst norm_minus_commute) by auto + unfolding dist_norm apply-defer apply(subst norm_minus_commute) by auto have *:"\f1 f2 g. abs(f1 - i$1) < e / 2 \ abs(f2 - g) < e / 2 \ f1 \ f2 \ f2 \ i$1 \ abs(g - i$1) < e" by arith show "norm (integral {a..b} (\x. if x \ s then g x else 0) - i) < e" diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Multivariate_Analysis/Operator_Norm.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy Mon May 03 07:59:51 2010 +0200 @@ -0,0 +1,148 @@ +(* Title: Library/Operator_Norm.thy + Author: Amine Chaieb, University of Cambridge +*) + +header {* Operator Norm *} + +theory Operator_Norm +imports Euclidean_Space +begin + +definition "onorm f = Sup {norm (f x)| x. norm x = 1}" + +lemma norm_bound_generalize: + 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- + {assume H: ?rhs + {fix x :: "real^'n" assume x: "norm x = 1" + from H[rule_format, of x] x have "norm (f x) \ b" by simp} + then have ?lhs by blast } + + moreover + {assume H: ?lhs + from H[rule_format, of "basis arbitrary"] + have bp: "b \ 0" using norm_ge_zero[of "f (basis arbitrary)"] + by (auto simp add: norm_basis elim: order_trans [OF norm_ge_zero]) + {fix x :: "real ^'n" + {assume "x = 0" + then have "norm (f x) \ b * norm x" by (simp add: linear_0[OF lf] bp)} + moreover + {assume x0: "x \ 0" + hence n0: "norm x \ 0" by (metis norm_eq_zero) + let ?c = "1/ norm x" + have "norm (?c *\<^sub>R x) = 1" using x0 by (simp add: n0) + with H have "norm (f (?c *\<^sub>R x)) \ b" by blast + hence "?c * norm (f x) \ b" + by (simp add: linear_cmul[OF lf]) + hence "norm (f x) \ b * norm x" + using n0 norm_ge_zero[of x] by (auto simp add: field_simps)} + ultimately have "norm (f x) \ b * norm x" by blast} + then have ?rhs by blast} + ultimately show ?thesis by blast +qed + +lemma onorm: + 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" +proof- + { + let ?S = "{norm (f x) |x. norm x = 1}" + have Se: "?S \ {}" using norm_basis by auto + from linear_bounded[OF lf] have b: "\ b. ?S *<= b" + unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def) + {from Sup[OF Se b, unfolded onorm_def[symmetric]] + show "norm (f x) <= onorm f * norm x" + apply - + apply (rule spec[where x = x]) + unfolding norm_bound_generalize[OF lf, symmetric] + by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)} + { + show "\x. norm (f x) <= b * norm x \ onorm f <= b" + using Sup[OF Se b, unfolded onorm_def[symmetric]] + unfolding norm_bound_generalize[OF lf, symmetric] + by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)} + } +qed + +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 \ real ^'m)" + shows "onorm f = 0 \ (\x. f x = 0)" + using onorm[OF lf] + apply (auto simp add: onorm_pos_le) + apply atomize + apply (erule allE[where x="0::real"]) + using onorm_pos_le[OF lf] + apply arith + done + +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}" + by(auto intro: vector_choose_size set_ext) + show ?thesis + unfolding onorm_def th + apply (rule Sup_unique) by (simp_all add: setle_def) +qed + +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 \ 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 + apply (subst mult_assoc) + apply (rule order_trans) + apply (rule onorm(1)[OF lf]) + apply (rule mult_mono1) + apply (rule onorm(1)[OF lg]) + apply (rule onorm_pos_le[OF lf]) + done + +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 \ 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 \ 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) + apply (rule norm_triangle_ineq) + apply (simp add: distrib) + apply (rule add_mono) + apply (rule onorm(1)[OF lf]) + apply (rule onorm(1)[OF lg]) + done + +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 \ 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) + by assumption+ + +end diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Multivariate_Analysis/Path_Connected.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon May 03 07:59:51 2010 +0200 @@ -0,0 +1,570 @@ +(* Title: Multivariate_Analysis/Path_Connected.thy + Author: Robert Himmelmann, TU Muenchen +*) + +header {* Continuous paths and path-connected sets *} + +theory Path_Connected +imports Convex_Euclidean_Space +begin + +subsection {* Paths. *} + +definition + path :: "(real \ 'a::topological_space) \ bool" + where "path g \ continuous_on {0 .. 1} g" + +definition + pathstart :: "(real \ 'a::topological_space) \ 'a" + where "pathstart g = g 0" + +definition + pathfinish :: "(real \ 'a::topological_space) \ 'a" + where "pathfinish g = g 1" + +definition + path_image :: "(real \ 'a::topological_space) \ 'a set" + where "path_image g = g ` {0 .. 1}" + +definition + reversepath :: "(real \ 'a::topological_space) \ (real \ 'a)" + where "reversepath g = (\x. g(1 - x))" + +definition + joinpaths :: "(real \ 'a::topological_space) \ (real \ 'a) \ (real \ 'a)" + (infixr "+++" 75) + where "g1 +++ g2 = (\x. if x \ 1/2 then g1 (2 * x) else g2 (2 * x - 1))" + +definition + simple_path :: "(real \ 'a::topological_space) \ bool" + where "simple_path g \ + (\x\{0..1}. \y\{0..1}. g x = g y \ x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0)" + +definition + injective_path :: "(real \ 'a::topological_space) \ bool" + where "injective_path g \ (\x\{0..1}. \y\{0..1}. g x = g y \ x = y)" + +subsection {* Some lemmas about these concepts. *} + +lemma injective_imp_simple_path: + "injective_path g \ simple_path g" + unfolding injective_path_def simple_path_def by auto + +lemma path_image_nonempty: "path_image g \ {}" + unfolding path_image_def image_is_empty interval_eq_empty by auto + +lemma pathstart_in_path_image[intro]: "(pathstart g) \ path_image g" + unfolding pathstart_def path_image_def by auto + +lemma pathfinish_in_path_image[intro]: "(pathfinish g) \ path_image g" + unfolding pathfinish_def path_image_def by auto + +lemma connected_path_image[intro]: "path g \ connected(path_image g)" + unfolding path_def path_image_def + apply (erule connected_continuous_image) + by(rule convex_connected, rule convex_real_interval) + +lemma compact_path_image[intro]: "path g \ compact(path_image g)" + unfolding path_def path_image_def + by (erule compact_continuous_image, rule compact_real_interval) + +lemma reversepath_reversepath[simp]: "reversepath(reversepath g) = g" + unfolding reversepath_def by auto + +lemma pathstart_reversepath[simp]: "pathstart(reversepath g) = pathfinish g" + unfolding pathstart_def reversepath_def pathfinish_def by auto + +lemma pathfinish_reversepath[simp]: "pathfinish(reversepath g) = pathstart g" + unfolding pathstart_def reversepath_def pathfinish_def by auto + +lemma pathstart_join[simp]: "pathstart(g1 +++ g2) = pathstart g1" + unfolding pathstart_def joinpaths_def pathfinish_def by auto + +lemma pathfinish_join[simp]:"pathfinish(g1 +++ g2) = pathfinish g2" + unfolding pathstart_def joinpaths_def pathfinish_def by auto + +lemma path_image_reversepath[simp]: "path_image(reversepath g) = path_image g" proof- + have *:"\g. path_image(reversepath g) \ path_image g" + unfolding path_image_def subset_eq reversepath_def Ball_def image_iff apply(rule,rule,erule bexE) + apply(rule_tac x="1 - xa" in bexI) by auto + show ?thesis using *[of g] *[of "reversepath g"] unfolding reversepath_reversepath by auto qed + +lemma path_reversepath[simp]: "path(reversepath g) \ path g" proof- + have *:"\g. path g \ path(reversepath g)" unfolding path_def reversepath_def + apply(rule continuous_on_compose[unfolded o_def, of _ "\x. 1 - x"]) + apply(rule continuous_on_sub, rule continuous_on_const, rule continuous_on_id) + apply(rule continuous_on_subset[of "{0..1}"], assumption) by auto + show ?thesis using *[of "reversepath g"] *[of g] unfolding reversepath_reversepath by (rule iffI) qed + +lemmas reversepath_simps = path_reversepath path_image_reversepath pathstart_reversepath pathfinish_reversepath + +lemma path_join[simp]: assumes "pathfinish g1 = pathstart g2" shows "path (g1 +++ g2) \ path g1 \ path g2" + unfolding path_def pathfinish_def pathstart_def apply rule defer apply(erule conjE) proof- + assume as:"continuous_on {0..1} (g1 +++ g2)" + have *:"g1 = (\x. g1 (2 *\<^sub>R x)) \ (\x. (1/2) *\<^sub>R x)" + "g2 = (\x. g2 (2 *\<^sub>R x - 1)) \ (\x. (1/2) *\<^sub>R (x + 1))" + unfolding o_def by (auto simp add: add_divide_distrib) + have "op *\<^sub>R (1 / 2) ` {0::real..1} \ {0..1}" "(\x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real)..1} \ {0..1}" + by auto + thus "continuous_on {0..1} g1 \ continuous_on {0..1} g2" apply -apply rule + apply(subst *) defer apply(subst *) apply (rule_tac[!] continuous_on_compose) + apply (rule continuous_on_cmul, rule continuous_on_add, rule continuous_on_id, rule continuous_on_const) defer + apply (rule continuous_on_cmul, rule continuous_on_id) apply(rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3 + apply(rule_tac[1-2] continuous_on_subset[of "{0 .. 1}"]) apply(rule as, assumption, rule as, assumption) + apply(rule) defer apply rule proof- + fix x assume "x \ op *\<^sub>R (1 / 2) ` {0::real..1}" + hence "x \ 1 / 2" unfolding image_iff by auto + thus "(g1 +++ g2) x = g1 (2 *\<^sub>R x)" unfolding joinpaths_def by auto next + fix x assume "x \ (\x. (1 / 2) *\<^sub>R (x + 1)) ` {0::real..1}" + hence "x \ 1 / 2" unfolding image_iff by auto + thus "(g1 +++ g2) x = g2 (2 *\<^sub>R x - 1)" proof(cases "x = 1 / 2") + case True hence "x = (1/2) *\<^sub>R 1" unfolding Cart_eq by auto + thus ?thesis unfolding joinpaths_def using assms[unfolded pathstart_def pathfinish_def] by (auto simp add: mult_ac) + qed (auto simp add:le_less joinpaths_def) qed +next assume as:"continuous_on {0..1} g1" "continuous_on {0..1} g2" + have *:"{0 .. 1::real} = {0.. (1/2)*\<^sub>R 1} \ {(1/2) *\<^sub>R 1 .. 1}" by auto + have **:"op *\<^sub>R 2 ` {0..(1 / 2) *\<^sub>R 1} = {0..1::real}" apply(rule set_ext, rule) unfolding image_iff + defer apply(rule_tac x="(1/2)*\<^sub>R x" in bexI) by auto + have ***:"(\x. 2 *\<^sub>R x - 1) ` {(1 / 2) *\<^sub>R 1..1} = {0..1::real}" + apply (auto simp add: image_def) + apply (rule_tac x="(x + 1) / 2" in bexI) + apply (auto simp add: add_divide_distrib) + done + show "continuous_on {0..1} (g1 +++ g2)" unfolding * apply(rule continuous_on_union) apply (rule closed_real_atLeastAtMost)+ proof- + show "continuous_on {0..(1 / 2) *\<^sub>R 1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "\x. g1 (2 *\<^sub>R x)"]) defer + unfolding o_def[THEN sym] apply(rule continuous_on_compose) apply(rule continuous_on_cmul, rule continuous_on_id) + unfolding ** apply(rule as(1)) unfolding joinpaths_def by auto next + show "continuous_on {(1/2)*\<^sub>R1..1} (g1 +++ g2)" apply(rule continuous_on_eq[of _ "g2 \ (\x. 2 *\<^sub>R x - 1)"]) defer + apply(rule continuous_on_compose) apply(rule continuous_on_sub, rule continuous_on_cmul, rule continuous_on_id, rule continuous_on_const) + unfolding *** o_def joinpaths_def apply(rule as(2)) using assms[unfolded pathstart_def pathfinish_def] + by (auto simp add: mult_ac) qed qed + +lemma path_image_join_subset: "path_image(g1 +++ g2) \ (path_image g1 \ path_image g2)" proof + fix x assume "x \ path_image (g1 +++ g2)" + then obtain y where y:"y\{0..1}" "x = (if y \ 1 / 2 then g1 (2 *\<^sub>R y) else g2 (2 *\<^sub>R y - 1))" + unfolding path_image_def image_iff joinpaths_def by auto + thus "x \ path_image g1 \ path_image g2" apply(cases "y \ 1/2") + apply(rule_tac UnI1) defer apply(rule_tac UnI2) unfolding y(2) path_image_def using y(1) + by(auto intro!: imageI) qed + +lemma subset_path_image_join: + assumes "path_image g1 \ s" "path_image g2 \ s" shows "path_image(g1 +++ g2) \ s" + using path_image_join_subset[of g1 g2] and assms by auto + +lemma path_image_join: + assumes "path g1" "path g2" "pathfinish g1 = pathstart g2" + shows "path_image(g1 +++ g2) = (path_image g1) \ (path_image g2)" +apply(rule, rule path_image_join_subset, rule) unfolding Un_iff proof(erule disjE) + fix x assume "x \ path_image g1" + then obtain y where y:"y\{0..1}" "x = g1 y" unfolding path_image_def image_iff by auto + thus "x \ path_image (g1 +++ g2)" unfolding joinpaths_def path_image_def image_iff + apply(rule_tac x="(1/2) *\<^sub>R y" in bexI) by auto next + fix x assume "x \ path_image g2" + then obtain y where y:"y\{0..1}" "x = g2 y" unfolding path_image_def image_iff by auto + then show "x \ path_image (g1 +++ g2)" unfolding joinpaths_def path_image_def image_iff + apply(rule_tac x="(1/2) *\<^sub>R (y + 1)" in bexI) using assms(3)[unfolded pathfinish_def pathstart_def] + by (auto simp add: add_divide_distrib) qed + +lemma not_in_path_image_join: + assumes "x \ path_image g1" "x \ path_image g2" shows "x \ path_image(g1 +++ g2)" + using assms and path_image_join_subset[of g1 g2] by auto + +lemma simple_path_reversepath: assumes "simple_path g" shows "simple_path (reversepath g)" + using assms unfolding simple_path_def reversepath_def apply- apply(rule ballI)+ + apply(erule_tac x="1-x" in ballE, erule_tac x="1-y" in ballE) + by auto + +lemma simple_path_join_loop: + assumes "injective_path g1" "injective_path g2" "pathfinish g2 = pathstart g1" + "(path_image g1 \ path_image g2) \ {pathstart g1,pathstart g2}" + shows "simple_path(g1 +++ g2)" +unfolding simple_path_def proof((rule ballI)+, rule impI) let ?g = "g1 +++ g2" + note inj = assms(1,2)[unfolded injective_path_def, rule_format] + fix x y::"real" assume xy:"x \ {0..1}" "y \ {0..1}" "?g x = ?g y" + show "x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0" proof(case_tac "x \ 1/2",case_tac[!] "y \ 1/2", unfold not_le) + assume as:"x \ 1 / 2" "y \ 1 / 2" + hence "g1 (2 *\<^sub>R x) = g1 (2 *\<^sub>R y)" using xy(3) unfolding joinpaths_def by auto + moreover have "2 *\<^sub>R x \ {0..1}" "2 *\<^sub>R y \ {0..1}" using xy(1,2) as + by auto + ultimately show ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] by auto + next assume as:"x > 1 / 2" "y > 1 / 2" + hence "g2 (2 *\<^sub>R x - 1) = g2 (2 *\<^sub>R y - 1)" using xy(3) unfolding joinpaths_def by auto + moreover have "2 *\<^sub>R x - 1 \ {0..1}" "2 *\<^sub>R y - 1 \ {0..1}" using xy(1,2) as by auto + ultimately show ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] by auto + next assume as:"x \ 1 / 2" "y > 1 / 2" + hence "?g x \ path_image g1" "?g y \ path_image g2" unfolding path_image_def joinpaths_def + using xy(1,2) by auto + moreover have "?g y \ pathstart g2" using as(2) unfolding pathstart_def joinpaths_def + using inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(2) + by (auto simp add: field_simps) + ultimately have *:"?g x = pathstart g1" using assms(4) unfolding xy(3) by auto + hence "x = 0" unfolding pathstart_def joinpaths_def using as(1) and xy(1) + using inj(1)[of "2 *\<^sub>R x" 0] by auto + moreover have "y = 1" using * unfolding xy(3) assms(3)[THEN sym] + unfolding joinpaths_def pathfinish_def using as(2) and xy(2) + using inj(2)[of "2 *\<^sub>R y - 1" 1] by auto + ultimately show ?thesis by auto + next assume as:"x > 1 / 2" "y \ 1 / 2" + hence "?g x \ path_image g2" "?g y \ path_image g1" unfolding path_image_def joinpaths_def + using xy(1,2) by auto + moreover have "?g x \ pathstart g2" using as(1) unfolding pathstart_def joinpaths_def + using inj(2)[of "2 *\<^sub>R x - 1" 0] and xy(1) + by (auto simp add: field_simps) + ultimately have *:"?g y = pathstart g1" using assms(4) unfolding xy(3) by auto + hence "y = 0" unfolding pathstart_def joinpaths_def using as(2) and xy(2) + using inj(1)[of "2 *\<^sub>R y" 0] by auto + moreover have "x = 1" using * unfolding xy(3)[THEN sym] assms(3)[THEN sym] + unfolding joinpaths_def pathfinish_def using as(1) and xy(1) + using inj(2)[of "2 *\<^sub>R x - 1" 1] by auto + ultimately show ?thesis by auto qed qed + +lemma injective_path_join: + assumes "injective_path g1" "injective_path g2" "pathfinish g1 = pathstart g2" + "(path_image g1 \ path_image g2) \ {pathstart g2}" + shows "injective_path(g1 +++ g2)" + unfolding injective_path_def proof(rule,rule,rule) let ?g = "g1 +++ g2" + note inj = assms(1,2)[unfolded injective_path_def, rule_format] + fix x y assume xy:"x \ {0..1}" "y \ {0..1}" "(g1 +++ g2) x = (g1 +++ g2) y" + show "x = y" proof(cases "x \ 1/2", case_tac[!] "y \ 1/2", unfold not_le) + assume "x \ 1 / 2" "y \ 1 / 2" thus ?thesis using inj(1)[of "2*\<^sub>R x" "2*\<^sub>R y"] and xy + unfolding joinpaths_def by auto + next assume "x > 1 / 2" "y > 1 / 2" thus ?thesis using inj(2)[of "2*\<^sub>R x - 1" "2*\<^sub>R y - 1"] and xy + unfolding joinpaths_def by auto + next assume as:"x \ 1 / 2" "y > 1 / 2" + hence "?g x \ path_image g1" "?g y \ path_image g2" unfolding path_image_def joinpaths_def + using xy(1,2) by auto + hence "?g x = pathfinish g1" "?g y = pathstart g2" using assms(4) unfolding assms(3) xy(3) by auto + thus ?thesis using as and inj(1)[of "2 *\<^sub>R x" 1] inj(2)[of "2 *\<^sub>R y - 1" 0] and xy(1,2) + unfolding pathstart_def pathfinish_def joinpaths_def + by auto + next assume as:"x > 1 / 2" "y \ 1 / 2" + hence "?g x \ path_image g2" "?g y \ path_image g1" unfolding path_image_def joinpaths_def + using xy(1,2) by auto + hence "?g x = pathstart g2" "?g y = pathfinish g1" using assms(4) unfolding assms(3) xy(3) by auto + thus ?thesis using as and inj(2)[of "2 *\<^sub>R x - 1" 0] inj(1)[of "2 *\<^sub>R y" 1] and xy(1,2) + unfolding pathstart_def pathfinish_def joinpaths_def + by auto qed qed + +lemmas join_paths_simps = path_join path_image_join pathstart_join pathfinish_join + +subsection {* Reparametrizing a closed curve to start at some chosen point. *} + +definition "shiftpath a (f::real \ 'a::topological_space) = + (\x. if (a + x) \ 1 then f(a + x) else f(a + x - 1))" + +lemma pathstart_shiftpath: "a \ 1 \ pathstart(shiftpath a g) = g a" + unfolding pathstart_def shiftpath_def by auto + +lemma pathfinish_shiftpath: assumes "0 \ a" "pathfinish g = pathstart g" + shows "pathfinish(shiftpath a g) = g a" + using assms unfolding pathstart_def pathfinish_def shiftpath_def + by auto + +lemma endpoints_shiftpath: + assumes "pathfinish g = pathstart g" "a \ {0 .. 1}" + shows "pathfinish(shiftpath a g) = g a" "pathstart(shiftpath a g) = g a" + using assms by(auto intro!:pathfinish_shiftpath pathstart_shiftpath) + +lemma closed_shiftpath: + assumes "pathfinish g = pathstart g" "a \ {0..1}" + shows "pathfinish(shiftpath a g) = pathstart(shiftpath a g)" + using endpoints_shiftpath[OF assms] by auto + +lemma path_shiftpath: + assumes "path g" "pathfinish g = pathstart g" "a \ {0..1}" + shows "path(shiftpath a g)" proof- + have *:"{0 .. 1} = {0 .. 1-a} \ {1-a .. 1}" using assms(3) by auto + have **:"\x. x + a = 1 \ g (x + a - 1) = g (x + a)" + using assms(2)[unfolded pathfinish_def pathstart_def] by auto + show ?thesis unfolding path_def shiftpath_def * apply(rule continuous_on_union) + apply(rule closed_real_atLeastAtMost)+ apply(rule continuous_on_eq[of _ "g \ (\x. a + x)"]) prefer 3 + apply(rule continuous_on_eq[of _ "g \ (\x. a - 1 + x)"]) defer prefer 3 + apply(rule continuous_on_intros)+ prefer 2 apply(rule continuous_on_intros)+ + apply(rule_tac[1-2] continuous_on_subset[OF assms(1)[unfolded path_def]]) + using assms(3) and ** by(auto, auto simp add: field_simps) qed + +lemma shiftpath_shiftpath: assumes "pathfinish g = pathstart g" "a \ {0..1}" "x \ {0..1}" + shows "shiftpath (1 - a) (shiftpath a g) x = g x" + using assms unfolding pathfinish_def pathstart_def shiftpath_def by auto + +lemma path_image_shiftpath: + assumes "a \ {0..1}" "pathfinish g = pathstart g" + shows "path_image(shiftpath a g) = path_image g" proof- + { fix x assume as:"g 1 = g 0" "x \ {0..1::real}" " \y\{0..1} \ {x. \ a + x \ 1}. g x \ g (a + y - 1)" + hence "\y\{0..1} \ {x. a + x \ 1}. g x = g (a + y)" proof(cases "a \ x") + case False thus ?thesis apply(rule_tac x="1 + x - a" in bexI) + using as(1,2) and as(3)[THEN bspec[where x="1 + x - a"]] and assms(1) + by(auto simp add: field_simps atomize_not) next + case True thus ?thesis using as(1-2) and assms(1) apply(rule_tac x="x - a" in bexI) + by(auto simp add: field_simps) qed } + thus ?thesis using assms unfolding shiftpath_def path_image_def pathfinish_def pathstart_def + by(auto simp add: image_iff) qed + +subsection {* Special case of straight-line paths. *} + +definition + linepath :: "'a::real_normed_vector \ 'a \ real \ 'a" where + "linepath a b = (\x. (1 - x) *\<^sub>R a + x *\<^sub>R b)" + +lemma pathstart_linepath[simp]: "pathstart(linepath a b) = a" + unfolding pathstart_def linepath_def by auto + +lemma pathfinish_linepath[simp]: "pathfinish(linepath a b) = b" + unfolding pathfinish_def linepath_def by auto + +lemma continuous_linepath_at[intro]: "continuous (at x) (linepath a b)" + unfolding linepath_def by (intro continuous_intros) + +lemma continuous_on_linepath[intro]: "continuous_on s (linepath a b)" + using continuous_linepath_at by(auto intro!: continuous_at_imp_continuous_on) + +lemma path_linepath[intro]: "path(linepath a b)" + unfolding path_def by(rule continuous_on_linepath) + +lemma path_image_linepath[simp]: "path_image(linepath a b) = (closed_segment a b)" + unfolding path_image_def segment linepath_def apply (rule set_ext, rule) defer + unfolding mem_Collect_eq image_iff apply(erule exE) apply(rule_tac x="u *\<^sub>R 1" in bexI) + by auto + +lemma reversepath_linepath[simp]: "reversepath(linepath a b) = linepath b a" + unfolding reversepath_def linepath_def by(rule ext, auto) + +lemma injective_path_linepath: + assumes "a \ b" shows "injective_path(linepath a b)" +proof - + { fix x y :: "real" + assume "x *\<^sub>R b + y *\<^sub>R a = x *\<^sub>R a + y *\<^sub>R b" + hence "(x - y) *\<^sub>R a = (x - y) *\<^sub>R b" by (simp add: algebra_simps) + with assms have "x = y" by simp } + thus ?thesis unfolding injective_path_def linepath_def by(auto simp add: algebra_simps) qed + +lemma simple_path_linepath[intro]: "a \ b \ simple_path(linepath a b)" by(auto intro!: injective_imp_simple_path injective_path_linepath) + +subsection {* Bounding a point away from a path. *} + +lemma not_on_path_ball: + fixes g :: "real \ 'a::heine_borel" + assumes "path g" "z \ path_image g" + shows "\e>0. ball z e \ (path_image g) = {}" proof- + obtain a where "a\path_image g" "\y\path_image g. dist z a \ dist z y" + using distance_attains_inf[OF _ path_image_nonempty, of g z] + using compact_path_image[THEN compact_imp_closed, OF assms(1)] by auto + thus ?thesis apply(rule_tac x="dist z a" in exI) using assms(2) by(auto intro!: dist_pos_lt) qed + +lemma not_on_path_cball: + fixes g :: "real \ 'a::heine_borel" + assumes "path g" "z \ path_image g" + shows "\e>0. cball z e \ (path_image g) = {}" proof- + obtain e where "ball z e \ path_image g = {}" "e>0" using not_on_path_ball[OF assms] by auto + moreover have "cball z (e/2) \ ball z e" using `e>0` by auto + ultimately show ?thesis apply(rule_tac x="e/2" in exI) by auto qed + +subsection {* Path component, considered as a "joinability" relation (from Tom Hales). *} + +definition "path_component s x y \ (\g. path g \ path_image g \ s \ pathstart g = x \ pathfinish g = y)" + +lemmas path_defs = path_def pathstart_def pathfinish_def path_image_def path_component_def + +lemma path_component_mem: assumes "path_component s x y" shows "x \ s" "y \ s" + using assms unfolding path_defs by auto + +lemma path_component_refl: assumes "x \ s" shows "path_component s x x" + unfolding path_defs apply(rule_tac x="\u. x" in exI) using assms + by(auto intro!:continuous_on_intros) + +lemma path_component_refl_eq: "path_component s x x \ x \ s" + by(auto intro!: path_component_mem path_component_refl) + +lemma path_component_sym: "path_component s x y \ path_component s y x" + using assms unfolding path_component_def apply(erule exE) apply(rule_tac x="reversepath g" in exI) + by auto + +lemma path_component_trans: assumes "path_component s x y" "path_component s y z" shows "path_component s x z" + using assms unfolding path_component_def apply- apply(erule exE)+ apply(rule_tac x="g +++ ga" in exI) by(auto simp add: path_image_join) + +lemma path_component_of_subset: "s \ t \ path_component s x y \ path_component t x y" + unfolding path_component_def by auto + +subsection {* Can also consider it as a set, as the name suggests. *} + +lemma path_component_set: "path_component s x = { y. (\g. path g \ path_image g \ s \ pathstart g = x \ pathfinish g = y )}" + apply(rule set_ext) unfolding mem_Collect_eq unfolding mem_def path_component_def by auto + +lemma mem_path_component_set:"x \ path_component s y \ path_component s y x" unfolding mem_def by auto + +lemma path_component_subset: "(path_component s x) \ s" + apply(rule, rule path_component_mem(2)) by(auto simp add:mem_def) + +lemma path_component_eq_empty: "path_component s x = {} \ x \ s" + apply rule apply(drule equals0D[of _ x]) defer apply(rule equals0I) unfolding mem_path_component_set + apply(drule path_component_mem(1)) using path_component_refl by auto + +subsection {* Path connectedness of a space. *} + +definition "path_connected s \ (\x\s. \y\s. \g. path g \ (path_image g) \ s \ pathstart g = x \ pathfinish g = y)" + +lemma path_connected_component: "path_connected s \ (\x\s. \y\s. path_component s x y)" + unfolding path_connected_def path_component_def by auto + +lemma path_connected_component_set: "path_connected s \ (\x\s. path_component s x = s)" + unfolding path_connected_component apply(rule, rule, rule, rule path_component_subset) + unfolding subset_eq mem_path_component_set Ball_def mem_def by auto + +subsection {* Some useful lemmas about path-connectedness. *} + +lemma convex_imp_path_connected: + fixes s :: "'a::real_normed_vector set" + assumes "convex s" shows "path_connected s" + unfolding path_connected_def apply(rule,rule,rule_tac x="linepath x y" in exI) + unfolding path_image_linepath using assms[unfolded convex_contains_segment] by auto + +lemma path_connected_imp_connected: assumes "path_connected s" shows "connected s" + unfolding connected_def not_ex apply(rule,rule,rule ccontr) unfolding not_not apply(erule conjE)+ proof- + fix e1 e2 assume as:"open e1" "open e2" "s \ e1 \ e2" "e1 \ e2 \ s = {}" "e1 \ s \ {}" "e2 \ s \ {}" + then obtain x1 x2 where obt:"x1\e1\s" "x2\e2\s" by auto + then obtain g where g:"path g" "path_image g \ s" "pathstart g = x1" "pathfinish g = x2" + using assms[unfolded path_connected_def,rule_format,of x1 x2] by auto + have *:"connected {0..1::real}" by(auto intro!: convex_connected convex_real_interval) + have "{0..1} \ {x \ {0..1}. g x \ e1} \ {x \ {0..1}. g x \ e2}" using as(3) g(2)[unfolded path_defs] by blast + moreover have "{x \ {0..1}. g x \ e1} \ {x \ {0..1}. g x \ e2} = {}" using as(4) g(2)[unfolded path_defs] unfolding subset_eq by auto + moreover have "{x \ {0..1}. g x \ e1} \ {} \ {x \ {0..1}. g x \ e2} \ {}" using g(3,4)[unfolded path_defs] using obt + by (simp add: ex_in_conv [symmetric], metis zero_le_one order_refl) + ultimately show False using *[unfolded connected_local not_ex,rule_format, of "{x\{0..1}. g x \ e1}" "{x\{0..1}. g x \ e2}"] + using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(1)] + using continuous_open_in_preimage[OF g(1)[unfolded path_def] as(2)] by auto qed + +lemma open_path_component: + fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*) + assumes "open s" shows "open(path_component s x)" + unfolding open_contains_ball proof + fix y assume as:"y \ path_component s x" + hence "y\s" apply- apply(rule path_component_mem(2)) unfolding mem_def by auto + then obtain e where e:"e>0" "ball y e \ s" using assms[unfolded open_contains_ball] by auto + show "\e>0. ball y e \ path_component s x" apply(rule_tac x=e in exI) apply(rule,rule `e>0`,rule) unfolding mem_ball mem_path_component_set proof- + fix z assume "dist y z < e" thus "path_component s x z" apply(rule_tac path_component_trans[of _ _ y]) defer + apply(rule path_component_of_subset[OF e(2)]) apply(rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) using `e>0` + using as[unfolded mem_def] by auto qed qed + +lemma open_non_path_component: + fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*) + assumes "open s" shows "open(s - path_component s x)" + unfolding open_contains_ball proof + fix y assume as:"y\s - path_component s x" + then obtain e where e:"e>0" "ball y e \ s" using assms[unfolded open_contains_ball] by auto + show "\e>0. ball y e \ s - path_component s x" apply(rule_tac x=e in exI) apply(rule,rule `e>0`,rule,rule) defer proof(rule ccontr) + fix z assume "z\ball y e" "\ z \ path_component s x" + hence "y \ path_component s x" unfolding not_not mem_path_component_set using `e>0` + apply- apply(rule path_component_trans,assumption) apply(rule path_component_of_subset[OF e(2)]) + apply(rule convex_imp_path_connected[OF convex_ball, unfolded path_connected_component, rule_format]) by auto + thus False using as by auto qed(insert e(2), auto) qed + +lemma connected_open_path_connected: + fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*) + assumes "open s" "connected s" shows "path_connected s" + unfolding path_connected_component_set proof(rule,rule,rule path_component_subset, rule) + fix x y assume "x \ s" "y \ s" show "y \ path_component s x" proof(rule ccontr) + assume "y \ path_component s x" moreover + have "path_component s x \ s \ {}" using `x\s` path_component_eq_empty path_component_subset[of s x] by auto + ultimately show False using `y\s` open_non_path_component[OF assms(1)] open_path_component[OF assms(1)] + using assms(2)[unfolded connected_def not_ex, rule_format, of"path_component s x" "s - path_component s x"] by auto +qed qed + +lemma path_connected_continuous_image: + assumes "continuous_on s f" "path_connected s" shows "path_connected (f ` s)" + unfolding path_connected_def proof(rule,rule) + fix x' y' assume "x' \ f ` s" "y' \ f ` s" + then obtain x y where xy:"x\s" "y\s" "x' = f x" "y' = f y" by auto + guess g using assms(2)[unfolded path_connected_def,rule_format,OF xy(1,2)] .. + thus "\g. path g \ path_image g \ f ` s \ pathstart g = x' \ pathfinish g = y'" + unfolding xy apply(rule_tac x="f \ g" in exI) unfolding path_defs + using assms(1) by(auto intro!: continuous_on_compose continuous_on_subset[of _ _ "g ` {0..1}"]) qed + +lemma homeomorphic_path_connectedness: + "s homeomorphic t \ (path_connected s \ path_connected t)" + unfolding homeomorphic_def homeomorphism_def apply(erule exE|erule conjE)+ apply rule + apply(drule_tac f=f in path_connected_continuous_image) prefer 3 + apply(drule_tac f=g in path_connected_continuous_image) by auto + +lemma path_connected_empty: "path_connected {}" + unfolding path_connected_def by auto + +lemma path_connected_singleton: "path_connected {a}" + unfolding path_connected_def pathstart_def pathfinish_def path_image_def + apply (clarify, rule_tac x="\x. a" in exI, simp add: image_constant_conv) + apply (simp add: path_def continuous_on_const) + done + +lemma path_connected_Un: assumes "path_connected s" "path_connected t" "s \ t \ {}" + shows "path_connected (s \ t)" unfolding path_connected_component proof(rule,rule) + fix x y assume as:"x \ s \ t" "y \ s \ t" + from assms(3) obtain z where "z \ s \ t" by auto + thus "path_component (s \ t) x y" using as using assms(1-2)[unfolded path_connected_component] apply- + apply(erule_tac[!] UnE)+ apply(rule_tac[2-3] path_component_trans[of _ _ z]) + by(auto simp add:path_component_of_subset [OF Un_upper1] path_component_of_subset[OF Un_upper2]) qed + +subsection {* sphere is path-connected. *} + +lemma path_connected_punctured_universe: + 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)" + let ?A = "\k. {x::real^'n. \i\{1..k}. inner (basis (\ i)) x \ 0}" + have "\k\{2..CARD('n)}. path_connected (?A k)" proof + have *:"\k. ?A (Suc k) = {x. inner (?basis (Suc k)) x < 0} \ {x. inner (?basis (Suc k)) x > 0} \ ?A k" apply(rule set_ext,rule) defer + apply(erule UnE)+ unfolding mem_Collect_eq apply(rule_tac[1-2] x="Suc k" in bexI) + by(auto elim!: ballE simp add: not_less le_Suc_eq) + fix k assume "k \ {2..CARD('n)}" thus "path_connected (?A k)" proof(induct k) + case (Suc k) show ?case proof(cases "k = 1") + case False from Suc have d:"k \ {1..CARD('n)}" "Suc k \ {1..CARD('n)}" by auto + hence "\ k \ \ (Suc k)" using \[unfolded bij_betw_def inj_on_def, THEN conjunct1, THEN bspec[where x=k]] by auto + hence **:"?basis k + ?basis (Suc k) \ {x. 0 < inner (?basis (Suc k)) x} \ (?A k)" + "?basis k - ?basis (Suc k) \ {x. 0 > inner (?basis (Suc k)) x} \ ({x. 0 < inner (?basis (Suc k)) x} \ (?A k))" using d + by(auto simp add: inner_basis intro!:bexI[where x=k]) + show ?thesis unfolding * Un_assoc apply(rule path_connected_Un) defer apply(rule path_connected_Un) + prefer 5 apply(rule_tac[1-2] convex_imp_path_connected, rule convex_halfspace_lt, rule convex_halfspace_gt) + apply(rule Suc(1)) using d ** False by auto + next case True hence d:"1\{1..CARD('n)}" "2\{1..CARD('n)}" using Suc(2) by auto + have ***:"Suc 1 = 2" by auto + have **:"\s t P Q. s \ t \ {x. P x \ Q x} = (s \ {x. P x}) \ (t \ {x. Q x})" by auto + have nequals0I:"\x A. x\A \ A \ {}" by auto + have "\ 2 \ \ (Suc 0)" using \[unfolded bij_betw_def inj_on_def, THEN conjunct1, THEN bspec[where x=2]] using assms by auto + thus ?thesis unfolding * True unfolding ** neq_iff bex_disj_distrib apply - + apply(rule path_connected_Un, rule_tac[1-2] path_connected_Un) defer 3 apply(rule_tac[1-4] convex_imp_path_connected) + apply(rule_tac[5] x=" ?basis 1 + ?basis 2" in nequals0I) + apply(rule_tac[6] x="-?basis 1 + ?basis 2" in nequals0I) + apply(rule_tac[7] x="-?basis 1 - ?basis 2" in nequals0I) + using d unfolding *** by(auto intro!: convex_halfspace_gt convex_halfspace_lt, auto simp add: inner_basis) + qed qed auto qed note lem = this + + have ***:"\x::real^'n. (\i\{1..CARD('n)}. inner (basis (\ i)) x \ 0) \ (\i. inner (basis i) x \ 0)" + apply rule apply(erule bexE) apply(rule_tac x="\ i" in exI) defer apply(erule exE) proof- + fix x::"real^'n" and i assume as:"inner (basis i) x \ 0" + have "i\\ ` {1..CARD('n)}" using \[unfolded bij_betw_def, THEN conjunct2] by auto + then obtain j where "j\{1..CARD('n)}" "\ j = i" by auto + thus "\i\{1..CARD('n)}. inner (basis (\ i)) x \ 0" apply(rule_tac x=j in bexI) using as by auto qed auto + have *:"?U - {a} = (\x. x + a) ` {x. x \ 0}" apply(rule set_ext) unfolding image_iff + apply rule apply(rule_tac x="x - a" in bexI) by auto + have **:"\x::real^'n. x\0 \ (\i. inner (basis i) x \ 0)" unfolding Cart_eq by(auto simp add: inner_basis) + 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. 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 + qed(auto intro!:path_connected_singleton) next + case False hence *:"{x::real^'n. norm(x - a) = r} = (\x. a + r *\<^sub>R x) ` {x. norm x = 1}" unfolding not_le apply -apply(rule set_ext,rule) + unfolding image_iff apply(rule_tac x="(1/r) *\<^sub>R (x - a)" in bexI) unfolding mem_Collect_eq norm_scaleR by (auto simp add: scaleR_right_diff_distrib) + have **:"{x::real^'n. norm x = 1} = (\x. (1/norm x) *\<^sub>R x) ` (UNIV - {0})" apply(rule set_ext,rule) + unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq by(auto split:split_if_asm) + have "continuous_on (UNIV - {0}) (\x::real^'n. 1 / norm x)" unfolding o_def continuous_on_eq_continuous_within + apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within) + apply(rule continuous_at_norm[unfolded o_def]) by auto + thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms] + by(auto intro!: path_connected_continuous_image continuous_on_intros) qed + +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 16736dde54c0 -r 6ed6112f0a95 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon May 03 07:59:51 2010 +0200 @@ -66,16 +66,14 @@ lemma openin_topspace[intro, simp]: "openin U (topspace U)" by (simp add: openin_Union topspace_def) lemma openin_subopen: "openin U S \ (\x \ S. \T. openin U T \ x \ T \ T \ S)" (is "?lhs \ ?rhs") -proof- - {assume ?lhs then have ?rhs by auto } - moreover - {assume H: ?rhs - then obtain t where t: "\x\S. openin U (t x) \ x \ t x \ t x \ S" - unfolding Ball_def ex_simps(6)[symmetric] choice_iff by blast - from t have th0: "\x\ t`S. openin U x" by auto - have "\ t`S = S" using t by auto - with openin_Union[OF th0] have "openin U S" by simp } - ultimately show ?thesis by blast +proof + assume ?lhs then show ?rhs by auto +next + assume H: ?rhs + let ?t = "\{T. openin U T \ T \ S}" + have "openin U ?t" by (simp add: openin_Union) + also have "?t = S" using H by auto + finally show "openin U S" . qed subsection{* Closed sets *} @@ -4294,18 +4292,6 @@ subsection {* Pasted sets *} -lemma bounded_pastecart: - fixes s :: "('a::real_normed_vector ^ _) set" (* FIXME: generalize to metric_space *) - assumes "bounded s" "bounded t" - shows "bounded { pastecart x y | x y . (x \ s \ y \ t)}" -proof- - obtain a b where ab:"\x\s. norm x \ a" "\x\t. norm x \ b" using assms[unfolded bounded_iff] by auto - { fix x y assume "x\s" "y\t" - hence "norm x \ a" "norm y \ b" using ab by auto - hence "norm (pastecart x y) \ a + b" using norm_pastecart[of x y] by auto } - thus ?thesis unfolding bounded_iff by auto -qed - lemma bounded_Times: assumes "bounded s" "bounded t" shows "bounded (s \ t)" proof- @@ -4316,33 +4302,6 @@ thus ?thesis unfolding bounded_any_center [where a="(x, y)"] by auto qed -lemma closed_pastecart: - fixes s :: "(real ^ 'a) set" (* FIXME: generalize *) - assumes "closed s" "closed t" - shows "closed {pastecart x y | x y . x \ s \ y \ t}" -proof- - { fix x l assume as:"\n::nat. x n \ {pastecart x y |x y. x \ s \ y \ t}" "(x ---> l) sequentially" - { fix n::nat have "fstcart (x n) \ s" "sndcart (x n) \ t" using as(1)[THEN spec[where x=n]] by auto } note * = this - moreover - { fix e::real assume "e>0" - then obtain N::nat where N:"\n\N. dist (x n) l < e" using as(2)[unfolded Lim_sequentially, THEN spec[where x=e]] by auto - { fix n::nat assume "n\N" - hence "dist (fstcart (x n)) (fstcart l) < e" "dist (sndcart (x n)) (sndcart l) < e" - using N[THEN spec[where x=n]] dist_fstcart[of "x n" l] dist_sndcart[of "x n" l] by auto } - hence "\N. \n\N. dist (fstcart (x n)) (fstcart l) < e" "\N. \n\N. dist (sndcart (x n)) (sndcart l) < e" by auto } - ultimately have "fstcart l \ s" "sndcart l \ t" - using assms(1)[unfolded closed_sequential_limits, THEN spec[where x="\n. fstcart (x n)"], THEN spec[where x="fstcart l"]] - using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="\n. sndcart (x n)"], THEN spec[where x="sndcart l"]] - unfolding Lim_sequentially by auto - hence "l \ {pastecart x y |x y. x \ s \ y \ t}" apply- unfolding mem_Collect_eq apply(rule_tac x="fstcart l" in exI,rule_tac x="sndcart l" in exI) by auto } - thus ?thesis unfolding closed_sequential_limits by blast -qed - -lemma compact_pastecart: - fixes s t :: "(real ^ _) set" - shows "compact s \ compact t ==> compact {pastecart x y | x y . x \ s \ y \ t}" - unfolding compact_eq_bounded_closed using bounded_pastecart[of s t] closed_pastecart[of s t] by auto - lemma mem_Times_iff: "x \ A \ B \ fst x \ A \ snd x \ B" by (induct x) simp @@ -5556,7 +5515,7 @@ moreover have "basis k \ span (?bas ` (insert k F))" by(rule span_superset, auto) hence "x$k *\<^sub>R basis k \ span (?bas ` (insert k F))" - using span_mul [where 'a=real, unfolded smult_conv_scaleR] by auto + using span_mul by auto ultimately have "y + x$k *\<^sub>R basis k \ span (?bas ` (insert k F))" using span_add by auto diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Multivariate_Analysis/Vec1.thy --- a/src/HOL/Multivariate_Analysis/Vec1.thy Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Vec1.thy Mon May 03 07:59:51 2010 +0200 @@ -205,14 +205,15 @@ apply(rule conjI) defer apply(rule conjI) defer apply(rule_tac x=1 in exI) by auto lemma linear_vmul_dest_vec1: - fixes f:: "'a::semiring_1^_ \ 'a^1" + fixes f:: "real^_ \ real^1" shows "linear f \ linear (\x. dest_vec1(f x) *s v)" - apply (rule linear_vmul_component) - by auto + unfolding smult_conv_scaleR + by (rule linear_vmul_component) lemma linear_from_scalars: - assumes lf: "linear (f::'a::comm_ring_1 ^1 \ 'a^_)" + assumes lf: "linear (f::real^1 \ real^_)" shows "f = (\x. dest_vec1 x *s column 1 (matrix f))" + unfolding smult_conv_scaleR apply (rule ext) apply (subst matrix_works[OF lf, symmetric]) apply (auto simp add: Cart_eq matrix_vector_mult_def column_def mult_commute) @@ -386,7 +387,7 @@ apply rule apply rule apply(erule_tac x="(vec1 x)" in allE) defer apply rule apply(erule_tac x="dest_vec1 v" in allE) unfolding o_def vec1_dest_vec1 by auto -lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding vector_dist_norm by auto +lemma dist_vec1_0[simp]: "dist(vec1 (x::real)) 0 = norm x" unfolding dist_norm by auto lemma bounded_linear_vec1_dest_vec1: fixes f::"real \ real" shows "linear (vec1 \ f \ dest_vec1) = bounded_linear f" (is "?l = ?r") proof- diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Mon May 03 07:59:51 2010 +0200 @@ -342,8 +342,8 @@ ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]), ((Binding.empty, weak_case_congs), [Simplifier.attrib (op addcongs)]), - ((Binding.empty, flat (distinct @ inject)), [Induct.add_simp_rule])] - @ named_rules @ unnamed_rules) + ((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @ + named_rules @ unnamed_rules) |> snd |> add_case_tr' case_names |> register dt_infos diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Tools/Nitpick/nitpick_isar.ML --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon May 03 07:59:51 2010 +0200 @@ -130,7 +130,7 @@ type T = raw_param list val empty = map (apsnd single) default_default_params val extend = I - val merge = AList.merge (op =) (K true)) + fun merge (x, y) = AList.merge (op =) (K true) (x, y)) val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param val default_raw_params = Data.get diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon May 03 07:59:51 2010 +0200 @@ -62,7 +62,7 @@ type T = (typ * term_postprocessor) list val empty = [] val extend = I - val merge = AList.merge (op =) (K true)) + fun merge (x, y) = AList.merge (op =) (K true) (x, y)) val irrelevant = "_" val unknown = "?" diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Mon May 03 07:59:51 2010 +0200 @@ -62,7 +62,8 @@ filtered_clauses = SOME (the_default axclauses filtered_clauses)} in prover params (K "") timeout problem - |> tap (priority o string_for_outcome o #outcome) + |> tap (fn result : prover_result => + priority (string_for_outcome (#outcome result))) end (* minimalization of thms *) diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon May 03 07:59:51 2010 +0200 @@ -355,7 +355,7 @@ if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse bad_for_atp th then [] else let - val ctxt0 = Variable.thm_context th + val ctxt0 = Variable.global_thm_context th val (nnfth, ctxt1) = to_nnf th ctxt0 val (cnfs, ctxt2) = Meson.make_cnf (assume_skolem_of_def s nnfth) nnfth ctxt1 in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end @@ -408,7 +408,7 @@ local fun skolem_def (name, th) thy = - let val ctxt0 = Variable.thm_context th in + let val ctxt0 = Variable.global_thm_context th in (case try (to_nnf th) ctxt0 of NONE => (NONE, thy) | SOME (nnfth, ctxt1) => diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon May 03 07:59:51 2010 +0200 @@ -35,7 +35,7 @@ (** Attribute for converting a theorem into clauses **) -val parse_clausify_attribute = +val parse_clausify_attribute : attribute context_parser = Scan.lift OuterParse.nat >> (fn i => Thm.rule_attribute (fn context => fn th => let val thy = Context.theory_of context in diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Mon May 03 07:59:51 2010 +0200 @@ -48,7 +48,8 @@ Long_Name.base_name #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix -val index_in_shape = find_index o exists o curry (op =) +val index_in_shape : int -> int list list -> int = + find_index o exists o curry (op =) fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names fun is_conjecture_clause_number conjecture_shape num = index_in_shape num conjecture_shape >= 0 diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Tools/TFL/post.ML Mon May 03 07:59:51 2010 +0200 @@ -128,9 +128,9 @@ Split_Rule.split_rule_var (Term.head_of (HOLogic.dest_Trueprop (concl_of rl))) rl; (*lcp: put a theorem into Isabelle form, using meta-level connectives*) -val meta_outer = +fun meta_outer ctxt = curry_rule o Drule.export_without_context o - rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE))); + rule_by_tactic ctxt (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE))); (*Strip off the outer !P*) val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec; @@ -139,7 +139,9 @@ | tracing false msg = writeln msg; fun simplify_defn strict thy cs ss congs wfs id pats def0 = - let val def = Thm.freezeT def0 RS meta_eq_to_obj_eq + let + val ctxt = ProofContext.init thy + val def = Thm.freezeT def0 RS meta_eq_to_obj_eq val {rules,rows,TCs,full_pats_TCs} = Prim.post_definition congs (thy, (def,pats)) val {lhs=f,rhs} = S.dest_eq (concl def) @@ -153,7 +155,7 @@ TCs = TCs} val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm) (R.CONJUNCTS rules) - in {induct = meta_outer (Object_Logic.rulify_no_asm (induction RS spec')), + in {induct = meta_outer ctxt (Object_Logic.rulify_no_asm (induction RS spec')), rules = ListPair.zip(rules', rows), tcs = (termination_goals rules') @ tcs} end diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Tools/inductive.ML Mon May 03 07:59:51 2010 +0200 @@ -446,7 +446,7 @@ val cprop = Thm.cterm_of thy prop; val tac = ALLGOALS (simp_case_tac ss) THEN prune_params_tac; fun mk_elim rl = - Thm.implies_intr cprop (Tactic.rule_by_tactic tac (Thm.assume cprop RS rl)) + Thm.implies_intr cprop (Tactic.rule_by_tactic ctxt tac (Thm.assume cprop RS rl)) |> singleton (Variable.export (Variable.auto_fixes prop ctxt) ctxt); in (case get_first (try mk_elim) elims of diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Tools/meson.ML Mon May 03 07:59:51 2010 +0200 @@ -555,7 +555,7 @@ skolemize_nnf_list ctxt ths); fun add_clauses th cls = - let val ctxt0 = Variable.thm_context th + let val ctxt0 = Variable.global_thm_context th val (cnfs, ctxt) = make_cnf [] th ctxt0 in Variable.export ctxt ctxt0 cnfs @ cls end; diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Tools/simpdata.ML Mon May 03 07:59:51 2010 +0200 @@ -95,7 +95,7 @@ fun res th = map (fn rl => th RS rl); (*exception THM*) fun res_fixed rls = if Thm.maxidx_of (Thm.adjust_maxidx_thm ~1 thm) = ~1 then res thm rls - else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.thm_context thm) [thm]; + else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.global_thm_context thm) [thm]; in case concl_of thm of Const (@{const_name Trueprop}, _) $ p => (case head_of p diff -r 16736dde54c0 -r 6ed6112f0a95 src/HOL/Tools/split_rule.ML --- a/src/HOL/Tools/split_rule.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/HOL/Tools/split_rule.ML Mon May 03 07:59:51 2010 +0200 @@ -116,7 +116,7 @@ fun split_rule_goal ctxt xss rl = let - fun one_split i s = Tactic.rule_by_tactic (pair_tac ctxt s i); + fun one_split i s = Tactic.rule_by_tactic ctxt (pair_tac ctxt s i); fun one_goal (i, xs) = fold (one_split (i + 1)) xs; in rl diff -r 16736dde54c0 -r 6ed6112f0a95 src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/Provers/clasimp.ML Mon May 03 07:59:51 2010 +0200 @@ -70,8 +70,14 @@ fun get_css context = (Classical.get_cs context, Simplifier.get_ss context); fun map_css f context = - let val (cs', ss') = f (get_css context) - in context |> Classical.map_cs (K cs') |> Simplifier.map_ss (K ss') end; + let + val (cs, ss) = get_css context; + val (cs', ss') = f (cs, Simplifier.context (Context.proof_of context) ss); + in + context + |> Classical.map_cs (K cs') + |> Simplifier.map_ss (K (Simplifier.inherit_context ss ss')) + end; fun clasimpset_of ctxt = (Classical.claset_of ctxt, Simplifier.simpset_of ctxt); diff -r 16736dde54c0 -r 6ed6112f0a95 src/Provers/classical.ML --- a/src/Provers/classical.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/Provers/classical.ML Mon May 03 07:59:51 2010 +0200 @@ -208,8 +208,11 @@ fun dup_intr th = zero_var_indexes (th RS classical); fun dup_elim th = - rule_by_tactic (TRYALL (etac revcut_rl)) - ((th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd); + let + val rl = (th RSN (2, revcut_rl)) |> Thm.assumption 2 |> Seq.hd; + val ctxt = ProofContext.init (Thm.theory_of_thm rl); + in rule_by_tactic ctxt (TRYALL (etac revcut_rl)) rl end; + (**** Classical rule sets ****) diff -r 16736dde54c0 -r 6ed6112f0a95 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/Pure/meta_simplifier.ML Mon May 03 07:59:51 2010 +0200 @@ -115,6 +115,7 @@ val the_context: simpset -> Proof.context val context: Proof.context -> simpset -> simpset val global_context: theory -> simpset -> simpset + val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset val debug_bounds: bool Unsynchronized.ref val set_reorient: (theory -> term list -> term -> term -> bool) -> simpset -> simpset val set_solvers: solver list -> simpset -> simpset @@ -326,7 +327,8 @@ print_term_global ss true a (Thm.theory_of_thm th) (Thm.full_prop_of th); fun cond_warn_thm a (ss as Simpset ({context, ...}, _)) th = - if is_some context then () else warn_thm a ss th; + if (case context of NONE => true | SOME ctxt => Context_Position.is_visible ctxt) + then warn_thm a ss th else (); end; @@ -358,9 +360,13 @@ fun activate_context thy ss = let val ctxt = the_context ss; - val ctxt' = Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt)) ctxt; + val ctxt' = ctxt + |> Context.raw_transfer (Theory.merge (thy, ProofContext.theory_of ctxt)) + |> Context_Position.set_visible false; in context ctxt' ss end; +fun with_context ctxt f ss = inherit_context ss (f (context ctxt ss)); + (* maintain simp rules *) diff -r 16736dde54c0 -r 6ed6112f0a95 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/Pure/simplifier.ML Mon May 03 07:59:51 2010 +0200 @@ -37,6 +37,7 @@ val the_context: simpset -> Proof.context val context: Proof.context -> simpset -> simpset val global_context: theory -> simpset -> simpset + val with_context: Proof.context -> (simpset -> simpset) -> simpset -> simpset val simproc_i: theory -> string -> term list -> (theory -> simpset -> term -> thm option) -> simproc val simproc: theory -> string -> string list @@ -108,7 +109,7 @@ ); val get_ss = SimpsetData.get; -val map_ss = SimpsetData.map; +fun map_ss f context = SimpsetData.map (with_context (Context.proof_of context) f) context; (* attributes *) diff -r 16736dde54c0 -r 6ed6112f0a95 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/Pure/tactic.ML Mon May 03 07:59:51 2010 +0200 @@ -7,7 +7,7 @@ signature BASIC_TACTIC = sig val trace_goalno_tac: (int -> tactic) -> int -> tactic - val rule_by_tactic: tactic -> thm -> thm + val rule_by_tactic: Proof.context -> tactic -> thm -> thm val assume_tac: int -> tactic val eq_assume_tac: int -> tactic val compose_tac: (bool * thm * int) -> int -> tactic @@ -86,14 +86,14 @@ Seq.make(fn()=> seqcell)); (*Makes a rule by applying a tactic to an existing rule*) -fun rule_by_tactic tac rl = +fun rule_by_tactic ctxt tac rl = let - val ctxt = Variable.thm_context rl; - val ((_, [st]), ctxt') = Variable.import true [rl] ctxt; + val ctxt' = Variable.declare_thm rl ctxt; + val ((_, [st]), ctxt'') = Variable.import true [rl] ctxt'; in (case Seq.pull (tac st) of NONE => raise THM ("rule_by_tactic", 0, [rl]) - | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt' ctxt) st')) + | SOME (st', _) => zero_var_indexes (singleton (Variable.export ctxt'' ctxt') st')) end; diff -r 16736dde54c0 -r 6ed6112f0a95 src/Pure/variable.ML --- a/src/Pure/variable.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/Pure/variable.ML Mon May 03 07:59:51 2010 +0200 @@ -28,7 +28,7 @@ val declare_typ: typ -> Proof.context -> Proof.context val declare_prf: Proofterm.proof -> Proof.context -> Proof.context val declare_thm: thm -> Proof.context -> Proof.context - val thm_context: thm -> Proof.context + val global_thm_context: thm -> Proof.context val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list val bind_term: indexname * term option -> Proof.context -> Proof.context val expand_binds: Proof.context -> term -> term @@ -235,7 +235,7 @@ val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type); val declare_thm = Thm.fold_terms declare_internal; -fun thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th)); +fun global_thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th)); (* renaming term/type frees *) diff -r 16736dde54c0 -r 6ed6112f0a95 src/Sequents/simpdata.ML --- a/src/Sequents/simpdata.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/Sequents/simpdata.ML Mon May 03 07:59:51 2010 +0200 @@ -42,13 +42,13 @@ Display.string_of_thm_without_context th)); (*Replace premises x=y, X<->Y by X==Y*) -val mk_meta_prems = - rule_by_tactic +fun mk_meta_prems ctxt = + rule_by_tactic ctxt (REPEAT_FIRST (resolve_tac [@{thm meta_eq_to_obj_eq}, @{thm def_imp_iff}])); (*Congruence rules for = or <-> (instead of ==)*) -fun mk_meta_cong (_: simpset) rl = - Drule.export_without_context(mk_meta_eq (mk_meta_prems rl)) +fun mk_meta_cong ss rl = + Drule.export_without_context (mk_meta_eq (mk_meta_prems (Simplifier.the_context ss) rl)) handle THM _ => error("Premises and conclusion of congruence rules must use =-equality or <->"); diff -r 16736dde54c0 -r 6ed6112f0a95 src/Tools/induct.ML --- a/src/Tools/induct.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/Tools/induct.ML Mon May 03 07:59:51 2010 +0200 @@ -46,7 +46,8 @@ val coinduct_pred: string -> attribute val coinduct_del: attribute val map_simpset: (simpset -> simpset) -> Context.generic -> Context.generic - val add_simp_rule: attribute + val induct_simp_add: attribute + val induct_simp_del: attribute val no_simpN: string val casesN: string val inductN: string @@ -320,8 +321,14 @@ val coinduct_del = del_att map3; fun map_simpset f = InductData.map (map4 f); -fun add_simp_rule (ctxt, thm) = - (map_simpset (fn ss => ss addsimps [thm]) ctxt, thm); + +fun induct_simp f = + Thm.declaration_attribute (fn thm => fn context => + (map_simpset + (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context)); + +val induct_simp_add = induct_simp (op addsimps); +val induct_simp_del = induct_simp (op delsimps); end; @@ -359,7 +366,7 @@ "declaration of induction rule" #> Attrib.setup @{binding coinduct} (attrib coinduct_type coinduct_pred coinduct_del) "declaration of coinduction rule" #> - Attrib.setup @{binding induct_simp} (Scan.succeed add_simp_rule) + Attrib.setup @{binding induct_simp} (Attrib.add_del induct_simp_add induct_simp_del) "declaration of rules for simplifying induction or cases rules"; end; diff -r 16736dde54c0 -r 6ed6112f0a95 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Fri Apr 30 18:34:51 2010 +0200 +++ b/src/ZF/Tools/inductive_package.ML Mon May 03 07:59:51 2010 +0200 @@ -261,7 +261,7 @@ THEN (PRIMITIVE (fold_rule part_rec_defs)); (*Elimination*) - val elim = rule_by_tactic basic_elim_tac + val elim = rule_by_tactic (ProofContext.init thy1) basic_elim_tac (unfold RS Ind_Syntax.equals_CollectD) (*Applies freeness of the given constructors, which *must* be unfolded by @@ -269,7 +269,7 @@ con_defs=[] for inference systems. Proposition A should have the form t:Si where Si is an inductive set*) fun make_cases ctxt A = - rule_by_tactic + rule_by_tactic ctxt (basic_elim_tac THEN ALLGOALS (asm_full_simp_tac (simpset_of ctxt)) THEN basic_elim_tac) (Thm.assume A RS elim) |> Drule.export_without_context_open;