# HG changeset patch # User paulson # Date 1474989893 -3600 # Node ID 444eafb6e864121729d95628dcf8aac60eb5f653 # Parent 21eaff8c8fc9cbdaa67201f6d9414644b784f039 a few new theorems and a renaming diff -r 21eaff8c8fc9 -r 444eafb6e864 src/HOL/Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Mon Sep 26 16:57:05 2016 +0200 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Tue Sep 27 16:24:53 2016 +0100 @@ -1085,7 +1085,7 @@ lemma inter_interval_cart: fixes a :: "real^'n" shows "cbox a b \ cbox c d = {(\ i. max (a$i) (c$i)) .. (\ i. min (b$i) (d$i))}" - unfolding inter_interval + unfolding Int_interval by (auto simp: mem_box less_eq_vec_def) (auto simp: Basis_vec_def inner_axis) diff -r 21eaff8c8fc9 -r 444eafb6e864 src/HOL/Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Mon Sep 26 16:57:05 2016 +0200 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Tue Sep 27 16:24:53 2016 +0100 @@ -7748,6 +7748,22 @@ using rel_interior_empty by auto qed +lemma interior_simplex_nonempty: + fixes S :: "'N :: euclidean_space set" + assumes "independent S" "finite S" "card S = DIM('N)" + obtains a where "a \ interior (convex hull (insert 0 S))" +proof - + have "affine hull (insert 0 S) = UNIV" + apply (simp add: hull_inc affine_hull_span_0) + using assms dim_eq_full indep_card_eq_dim_span by fastforce + moreover have "rel_interior (convex hull insert 0 S) \ {}" + using rel_interior_eq_empty [of "convex hull (insert 0 S)"] by auto + ultimately have "interior (convex hull insert 0 S) \ {}" + by (simp add: rel_interior_interior) + with that show ?thesis + by auto +qed + lemma convex_rel_interior: fixes S :: "'n::euclidean_space set" assumes "convex S" diff -r 21eaff8c8fc9 -r 444eafb6e864 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Mon Sep 26 16:57:05 2016 +0200 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Tue Sep 27 16:24:53 2016 +0100 @@ -1108,7 +1108,7 @@ show "\a b. k = cbox a b" unfolding il using p'(4)[OF il(3)] d'(4)[OF il(2)] apply safe - unfolding inter_interval + unfolding Int_interval apply auto done next @@ -1288,7 +1288,7 @@ from d'(4)[OF k] snd_p(4)[OF prems(1)] guess u1 v1 u2 v2 by (elim exE) note uv=this show ?case using * - unfolding uv inter_interval content_eq_0_interior[symmetric] + unfolding uv Int_interval content_eq_0_interior[symmetric] by auto qed finally show ?case . @@ -1338,7 +1338,7 @@ ultimately have "interior(l1 \ k1) = {}" by auto then show "norm (integral (l1 \ k1) f) = 0" - unfolding uv inter_interval + unfolding uv Int_interval unfolding content_eq_0_interior[symmetric] by auto qed @@ -1429,7 +1429,7 @@ ultimately have "interior (l1 \ k1) = {}" by auto then show "\content (l1 \ k1)\ * norm (f x1) = 0" - unfolding uv inter_interval + unfolding uv Int_interval unfolding content_eq_0_interior[symmetric] by auto qed safe @@ -1453,7 +1453,7 @@ apply (drule d'(4)) apply safe apply (subst Int_commute) - unfolding inter_interval uv + unfolding Int_interval uv apply (subst abs_of_nonneg) apply auto done @@ -1475,7 +1475,7 @@ also have "\ = interior (k \ cbox u v)" unfolding prems(4) by auto finally show ?case - unfolding uv inter_interval content_eq_0_interior .. + unfolding uv Int_interval content_eq_0_interior .. qed also have "\ = setsum content {cbox u v \ k |k. k \ d \ cbox u v \ k \ {}}" apply (rule setsum.mono_neutral_right) @@ -1490,7 +1490,7 @@ from d'(4)[OF this(1)] guess a b by (elim exE) note ab=this have "interior (k \ cbox u v) \ {}" using prems(2) - unfolding ab inter_interval content_eq_0_interior + unfolding ab Int_interval content_eq_0_interior by auto then show ?case using prems(1) diff -r 21eaff8c8fc9 -r 444eafb6e864 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Mon Sep 26 16:57:05 2016 +0200 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Sep 27 16:24:53 2016 +0100 @@ -503,7 +503,7 @@ obtain a2 b2 where k2: "k2 = cbox a2 b2" using division_ofD(4)[OF assms(2) k(3)] by blast show "\a b. k = cbox a b" - unfolding k k1 k2 unfolding inter_interval by auto + unfolding k k1 k2 unfolding Int_interval by auto } fix k1 k2 assume "k1 \ ?A" @@ -826,7 +826,7 @@ next case False obtain u v where uv: "cbox a b \ cbox c d = cbox u v" - unfolding inter_interval by auto + unfolding Int_interval by auto have uv_sub: "cbox u v \ cbox c d" using uv by auto obtain p where "p division_of cbox c d" "cbox u v \ p" by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]]) @@ -4733,34 +4733,21 @@ subsection \Some other trivialities about negligible sets.\ -lemma negligible_subset[intro]: - assumes "negligible s" - and "t \ s" +lemma negligible_subset: + assumes "negligible s" "t \ s" shows "negligible t" unfolding negligible_def -proof (safe, goal_cases) - case (1 a b) - show ?case - using assms(1)[unfolded negligible_def,rule_format,of a b] - apply - - apply (rule has_integral_spike[OF assms(1)]) - defer - apply assumption - using assms(2) - unfolding indicator_def - apply auto - done -qed + by (metis (no_types) Diff_iff assms contra_subsetD has_integral_negligible indicator_simps(2)) lemma negligible_diff[intro?]: assumes "negligible s" shows "negligible (s - t)" - using assms by auto + using assms by (meson Diff_subset negligible_subset) lemma negligible_Int: assumes "negligible s \ negligible t" shows "negligible (s \ t)" - using assms by auto + using assms negligible_subset by force lemma negligible_Un: assumes "negligible s" @@ -4780,10 +4767,10 @@ qed lemma negligible_Un_eq[simp]: "negligible (s \ t) \ negligible s \ negligible t" - using negligible_Un by auto + using negligible_Un negligible_subset by blast lemma negligible_sing[intro]: "negligible {a::'a::euclidean_space}" - using negligible_standard_hyperplane[OF SOME_Basis, of "a \ (SOME i. i \ Basis)"] by auto + using negligible_standard_hyperplane[OF SOME_Basis, of "a \ (SOME i. i \ Basis)"] negligible_subset by blast lemma negligible_insert[simp]: "negligible (insert a s) \ negligible s" apply (subst insert_is_Un) @@ -4792,7 +4779,7 @@ done lemma negligible_empty[iff]: "negligible {}" - by auto + using negligible_insert by blast lemma negligible_finite[intro]: assumes "finite s" @@ -7652,7 +7639,7 @@ apply auto done qed -qed auto +qed (simp add: negligible_Int) lemma negligible_translation: assumes "negligible S" @@ -7689,32 +7676,24 @@ apply (rule has_integral_spike_eq[OF assms]) by (auto split: if_split_asm) -lemma has_integral_spike_set[dest]: +lemma has_integral_spike_set: fixes f :: "'n::euclidean_space \ 'a::banach" - assumes "negligible ((s - t) \ (t - s))" - and "(f has_integral y) s" + assumes "(f has_integral y) s" "negligible ((s - t) \ (t - s))" shows "(f has_integral y) t" using assms has_integral_spike_set_eq by auto -lemma integrable_spike_set[dest]: +lemma integrable_spike_set: fixes f :: "'n::euclidean_space \ 'a::banach" - assumes "negligible ((s - t) \ (t - s))" - and "f integrable_on s" - shows "f integrable_on t" - using assms(2) - unfolding integrable_on_def - unfolding has_integral_spike_set_eq[OF assms(1)] . + assumes "f integrable_on s" and "negligible ((s - t) \ (t - s))" + shows "f integrable_on t" + using assms by (simp add: integrable_on_def has_integral_spike_set_eq) lemma integrable_spike_set_eq: fixes f :: "'n::euclidean_space \ 'a::banach" assumes "negligible ((s - t) \ (t - s))" shows "f integrable_on s \ f integrable_on t" - apply rule - apply (rule_tac[!] integrable_spike_set) - using assms - apply auto - done +by (blast intro: integrable_spike_set assms negligible_subset) (*lemma integral_spike_set: "\f:real^M->real^N g s t. diff -r 21eaff8c8fc9 -r 444eafb6e864 src/HOL/Analysis/Homeomorphism.thy --- a/src/HOL/Analysis/Homeomorphism.thy Mon Sep 26 16:57:05 2016 +0200 +++ b/src/HOL/Analysis/Homeomorphism.thy Tue Sep 27 16:24:53 2016 +0100 @@ -973,6 +973,52 @@ by (metis closed_closure closed_imp_locally_compact inf_commute locally_compact_Int locally_compact_open_Int_closure open_imp_locally_compact) +lemma lowerdim_embeddings: + assumes "DIM('a) < DIM('b)" + obtains f :: "'a::euclidean_space*real \ 'b::euclidean_space" + and g :: "'b \ 'a*real" + and j :: 'b + where "linear f" "linear g" "\z. g (f z) = z" "j \ Basis" "\x. f(x,0) \ j = 0" +proof - + let ?B = "Basis :: ('a*real) set" + have b01: "(0,1) \ ?B" + by (simp add: Basis_prod_def) + have "DIM('a * real) \ DIM('b)" + by (simp add: Suc_leI assms) + then obtain basf :: "'a*real \ 'b" where sbf: "basf ` ?B \ Basis" and injbf: "inj_on basf Basis" + by (metis finite_Basis card_le_inj) + define basg:: "'b \ 'a * real" where + "basg \ \i. if i \ basf ` Basis then inv_into Basis basf i else (0,1)" + have bgf[simp]: "basg (basf i) = i" if "i \ Basis" for i + using inv_into_f_f injbf that by (force simp: basg_def) + have sbg: "basg ` Basis \ ?B" + by (force simp: basg_def injbf b01) + define f :: "'a*real \ 'b" where "f \ \u. \j\Basis. (u \ basg j) *\<^sub>R j" + define g :: "'b \ 'a*real" where "g \ \z. (\i\Basis. (z \ basf i) *\<^sub>R i)" + show ?thesis + proof + show "linear f" + unfolding f_def + by (intro linear_compose_setsum linearI ballI) (auto simp: algebra_simps) + show "linear g" + unfolding g_def + by (intro linear_compose_setsum linearI ballI) (auto simp: algebra_simps) + have *: "(\a \ Basis. a \ basf b * (x \ basg a)) = x \ b" if "b \ Basis" for x b + using sbf that by auto + show gf: "g (f x) = x" for x + apply (rule euclidean_eqI) + apply (simp add: f_def g_def inner_setsum_left scaleR_setsum_left algebra_simps) + apply (simp add: Groups_Big.setsum_distrib_left [symmetric] *) + done + show "basf(0,1) \ Basis" + using b01 sbf by auto + then show "f(x,0) \ basf(0,1) = 0" for x + apply (simp add: f_def inner_setsum_left) + apply (rule comm_monoid_add_class.setsum.neutral) + using b01 inner_not_same_Basis by fastforce + qed +qed + proposition locally_compact_homeomorphic_closed: fixes S :: "'a::euclidean_space set" assumes "locally compact S" and dimlt: "DIM('a) < DIM('b)" @@ -981,45 +1027,21 @@ obtain U:: "('a*real)set" and h where "closed U" and homU: "homeomorphism S U h fst" using locally_compact_homeomorphism_projection_closed assms by metis - let ?BP = "Basis :: ('a*real) set" - have "DIM('a * real) \ DIM('b)" - by (simp add: Suc_leI dimlt) - then obtain basf :: "'a*real \ 'b" where surbf: "basf ` ?BP \ Basis" and injbf: "inj_on basf Basis" - by (metis finite_Basis card_le_inj) - define basg:: "'b \ 'a * real" where - "basg \ \i. inv_into Basis basf i" - have bgf[simp]: "basg (basf i) = i" if "i \ Basis" for i - using inv_into_f_f injbf that by (force simp: basg_def) - define f :: "'a*real \ 'b" where "f \ \u. \j\Basis. (u \ basg j) *\<^sub>R j" - have "linear f" - unfolding f_def - apply (intro linear_compose_setsum linearI ballI) - apply (auto simp: algebra_simps) - done - define g :: "'b \ 'a*real" where "g \ \z. (\i\Basis. (z \ basf i) *\<^sub>R i)" - have "linear g" - unfolding g_def - apply (intro linear_compose_setsum linearI ballI) - apply (auto simp: algebra_simps) - done - have *: "(\a \ Basis. a \ basf b * (x \ basg a)) = x \ b" if "b \ Basis" for x b - using surbf that by auto - have gf[simp]: "g (f x) = x" for x - apply (rule euclidean_eqI) - apply (simp add: f_def g_def inner_setsum_left scaleR_setsum_left algebra_simps) - apply (simp add: Groups_Big.setsum_distrib_left [symmetric] *) - done - then have "inj f" by (metis injI) + obtain f :: "'a*real \ 'b" and g :: "'b \ 'a*real" + where "linear f" "linear g" and gf [simp]: "\z. g (f z) = z" + using lowerdim_embeddings [OF dimlt] by metis + then have "inj f" + by (metis injI) have gfU: "g ` f ` U = U" - by (rule set_eqI) (auto simp: image_def) + by (simp add: image_comp o_def) have "S homeomorphic U" using homU homeomorphic_def by blast also have "... homeomorphic f ` U" apply (rule homeomorphicI [OF refl gfU]) apply (meson \inj f\ \linear f\ homeomorphism_cont2 linear_homeomorphism_image) - using \linear g\ linear_continuous_on linear_conv_bounded_linear apply blast - apply auto - done + using \linear g\ linear_continuous_on linear_conv_bounded_linear apply blast + apply (auto simp: o_def) + done finally show ?thesis apply (rule_tac T = "f ` U" in that) apply (rule closed_injective_linear_image [OF \closed U\ \linear f\ \inj f\], assumption) diff -r 21eaff8c8fc9 -r 444eafb6e864 src/HOL/Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Sep 26 16:57:05 2016 +0200 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Sep 27 16:24:53 2016 +0100 @@ -1388,7 +1388,59 @@ done qed -lemma inter_interval: +lemma eq_cbox: "cbox a b = cbox c d \ cbox a b = {} \ cbox c d = {} \ a = c \ b = d" + (is "?lhs = ?rhs") +proof + assume ?lhs + then have "cbox a b \ cbox c d" "cbox c d \ cbox a b" + by auto + then show ?rhs + by (force simp add: subset_box box_eq_empty intro: antisym euclidean_eqI) +next + assume ?rhs + then show ?lhs + by force +qed + +lemma eq_cbox_box [simp]: "cbox a b = box c d \ cbox a b = {} \ box c d = {}" + (is "?lhs = ?rhs") +proof + assume ?lhs + then have "cbox a b \ box c d" "box c d \cbox a b" + by auto + then show ?rhs + apply (simp add: subset_box) + using \cbox a b = box c d\ box_ne_empty box_sing + apply (fastforce simp add:) + done +next + assume ?rhs + then show ?lhs + by force +qed + +lemma eq_box_cbox [simp]: "box a b = cbox c d \ box a b = {} \ cbox c d = {}" + by (metis eq_cbox_box) + +lemma eq_box: "box a b = box c d \ box a b = {} \ box c d = {} \ a = c \ b = d" + (is "?lhs = ?rhs") +proof + assume ?lhs + then have "box a b \ box c d" "box c d \ box a b" + by auto + then show ?rhs + apply (simp add: subset_box) + using box_ne_empty(2) \box a b = box c d\ + apply auto + apply (meson euclidean_eqI less_eq_real_def not_less)+ + done +next + assume ?rhs + then show ?lhs + by force +qed + +lemma Int_interval: fixes a :: "'a::euclidean_space" shows "cbox a b \ cbox c d = cbox (\i\Basis. max (a\i) (c\i) *\<^sub>R i) (\i\Basis. min (b\i) (d\i) *\<^sub>R i)" @@ -8077,6 +8129,11 @@ shows "cbox a b \ UNIV" "box a b \ UNIV" using bounded_box[of a b] bounded_cbox[of a b] by force+ +lemma not_interval_UNIV2 [simp]: + fixes a :: "'a::euclidean_space" + shows "UNIV \ cbox a b" "UNIV \ box a b" + using bounded_box[of a b] bounded_cbox[of a b] by force+ + lemma compact_cbox [simp]: fixes a :: "'a::euclidean_space" shows "compact (cbox a b)" @@ -9057,7 +9114,7 @@ shows "closed (span s)" by (simp add: closed_subspace subspace_span) -lemma dim_closure: +lemma dim_closure [simp]: fixes s :: "('a::euclidean_space) set" shows "dim(closure s) = dim s" (is "?dc = ?d") proof - diff -r 21eaff8c8fc9 -r 444eafb6e864 src/HOL/Archimedean_Field.thy --- a/src/HOL/Archimedean_Field.thy Mon Sep 26 16:57:05 2016 +0200 +++ b/src/HOL/Archimedean_Field.thy Tue Sep 27 16:24:53 2016 +0100 @@ -619,6 +619,15 @@ unfolding ceiling_def by simp +subsection \Natural numbers\ + +lemma of_nat_floor: "r\0 \ of_nat (nat \r\) \ r" + by simp + +lemma of_nat_ceiling: "of_nat (nat \r\) \ r" + by (cases "r\0") auto + + subsection \Frac Function\ definition frac :: "'a \ 'a::floor_ceiling"