--- 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 \<inter> cbox c d = {(\<chi> i. max (a$i) (c$i)) .. (\<chi> 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)
--- 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 \<in> 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) \<noteq> {}"
+ using rel_interior_eq_empty [of "convex hull (insert 0 S)"] by auto
+ ultimately have "interior (convex hull insert 0 S) \<noteq> {}"
+ 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"
--- 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 "\<exists>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 \<inter> k1) = {}"
by auto
then show "norm (integral (l1 \<inter> 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 \<inter> k1) = {}"
by auto
then show "\<bar>content (l1 \<inter> k1)\<bar> * 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 "\<dots> = interior (k \<inter> 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 "\<dots> = setsum content {cbox u v \<inter> k |k. k \<in> d \<and> cbox u v \<inter> k \<noteq> {}}"
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 \<inter> cbox u v) \<noteq> {}"
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)
--- 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 "\<exists>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 \<in> ?A"
@@ -826,7 +826,7 @@
next
case False
obtain u v where uv: "cbox a b \<inter> cbox c d = cbox u v"
- unfolding inter_interval by auto
+ unfolding Int_interval by auto
have uv_sub: "cbox u v \<subseteq> cbox c d" using uv by auto
obtain p where "p division_of cbox c d" "cbox u v \<in> p"
by (rule partial_division_extend_1[OF uv_sub False[unfolded uv]])
@@ -4733,34 +4733,21 @@
subsection \<open>Some other trivialities about negligible sets.\<close>
-lemma negligible_subset[intro]:
- assumes "negligible s"
- and "t \<subseteq> s"
+lemma negligible_subset:
+ assumes "negligible s" "t \<subseteq> 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 \<or> negligible t"
shows "negligible (s \<inter> 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 \<union> t) \<longleftrightarrow> negligible s \<and> 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 \<bullet> (SOME i. i \<in> Basis)"] by auto
+ using negligible_standard_hyperplane[OF SOME_Basis, of "a \<bullet> (SOME i. i \<in> Basis)"] negligible_subset by blast
lemma negligible_insert[simp]: "negligible (insert a s) \<longleftrightarrow> 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 \<Rightarrow> 'a::banach"
- assumes "negligible ((s - t) \<union> (t - s))"
- and "(f has_integral y) s"
+ assumes "(f has_integral y) s" "negligible ((s - t) \<union> (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 \<Rightarrow> 'a::banach"
- assumes "negligible ((s - t) \<union> (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) \<union> (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 \<Rightarrow> 'a::banach"
assumes "negligible ((s - t) \<union> (t - s))"
shows "f integrable_on s \<longleftrightarrow> 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:
"\<forall>f:real^M->real^N g s t.
--- 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 \<Rightarrow> 'b::euclidean_space"
+ and g :: "'b \<Rightarrow> 'a*real"
+ and j :: 'b
+ where "linear f" "linear g" "\<And>z. g (f z) = z" "j \<in> Basis" "\<And>x. f(x,0) \<bullet> j = 0"
+proof -
+ let ?B = "Basis :: ('a*real) set"
+ have b01: "(0,1) \<in> ?B"
+ by (simp add: Basis_prod_def)
+ have "DIM('a * real) \<le> DIM('b)"
+ by (simp add: Suc_leI assms)
+ then obtain basf :: "'a*real \<Rightarrow> 'b" where sbf: "basf ` ?B \<subseteq> Basis" and injbf: "inj_on basf Basis"
+ by (metis finite_Basis card_le_inj)
+ define basg:: "'b \<Rightarrow> 'a * real" where
+ "basg \<equiv> \<lambda>i. if i \<in> basf ` Basis then inv_into Basis basf i else (0,1)"
+ have bgf[simp]: "basg (basf i) = i" if "i \<in> Basis" for i
+ using inv_into_f_f injbf that by (force simp: basg_def)
+ have sbg: "basg ` Basis \<subseteq> ?B"
+ by (force simp: basg_def injbf b01)
+ define f :: "'a*real \<Rightarrow> 'b" where "f \<equiv> \<lambda>u. \<Sum>j\<in>Basis. (u \<bullet> basg j) *\<^sub>R j"
+ define g :: "'b \<Rightarrow> 'a*real" where "g \<equiv> \<lambda>z. (\<Sum>i\<in>Basis. (z \<bullet> 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 *: "(\<Sum>a \<in> Basis. a \<bullet> basf b * (x \<bullet> basg a)) = x \<bullet> b" if "b \<in> 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) \<in> Basis"
+ using b01 sbf by auto
+ then show "f(x,0) \<bullet> 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) \<le> DIM('b)"
- by (simp add: Suc_leI dimlt)
- then obtain basf :: "'a*real \<Rightarrow> 'b" where surbf: "basf ` ?BP \<subseteq> Basis" and injbf: "inj_on basf Basis"
- by (metis finite_Basis card_le_inj)
- define basg:: "'b \<Rightarrow> 'a * real" where
- "basg \<equiv> \<lambda>i. inv_into Basis basf i"
- have bgf[simp]: "basg (basf i) = i" if "i \<in> Basis" for i
- using inv_into_f_f injbf that by (force simp: basg_def)
- define f :: "'a*real \<Rightarrow> 'b" where "f \<equiv> \<lambda>u. \<Sum>j\<in>Basis. (u \<bullet> 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 \<Rightarrow> 'a*real" where "g \<equiv> \<lambda>z. (\<Sum>i\<in>Basis. (z \<bullet> 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 *: "(\<Sum>a \<in> Basis. a \<bullet> basf b * (x \<bullet> basg a)) = x \<bullet> b" if "b \<in> 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 \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'a*real"
+ where "linear f" "linear g" and gf [simp]: "\<And>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 \<open>inj f\<close> \<open>linear f\<close> homeomorphism_cont2 linear_homeomorphism_image)
- using \<open>linear g\<close> linear_continuous_on linear_conv_bounded_linear apply blast
- apply auto
- done
+ using \<open>linear g\<close> 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 \<open>closed U\<close> \<open>linear f\<close> \<open>inj f\<close>], assumption)
--- 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 \<longleftrightarrow> cbox a b = {} \<and> cbox c d = {} \<or> a = c \<and> b = d"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then have "cbox a b \<subseteq> cbox c d" "cbox c d \<subseteq> 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 \<longleftrightarrow> cbox a b = {} \<and> box c d = {}"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then have "cbox a b \<subseteq> box c d" "box c d \<subseteq>cbox a b"
+ by auto
+ then show ?rhs
+ apply (simp add: subset_box)
+ using \<open>cbox a b = box c d\<close> 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 \<longleftrightarrow> box a b = {} \<and> cbox c d = {}"
+ by (metis eq_cbox_box)
+
+lemma eq_box: "box a b = box c d \<longleftrightarrow> box a b = {} \<and> box c d = {} \<or> a = c \<and> b = d"
+ (is "?lhs = ?rhs")
+proof
+ assume ?lhs
+ then have "box a b \<subseteq> box c d" "box c d \<subseteq> box a b"
+ by auto
+ then show ?rhs
+ apply (simp add: subset_box)
+ using box_ne_empty(2) \<open>box a b = box c d\<close>
+ 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 \<inter> cbox c d =
cbox (\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)"
@@ -8077,6 +8129,11 @@
shows "cbox a b \<noteq> UNIV" "box a b \<noteq> 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 \<noteq> cbox a b" "UNIV \<noteq> 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 -
--- 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 \<open>Natural numbers\<close>
+
+lemma of_nat_floor: "r\<ge>0 \<Longrightarrow> of_nat (nat \<lfloor>r\<rfloor>) \<le> r"
+ by simp
+
+lemma of_nat_ceiling: "of_nat (nat \<lceil>r\<rceil>) \<ge> r"
+ by (cases "r\<ge>0") auto
+
+
subsection \<open>Frac Function\<close>
definition frac :: "'a \<Rightarrow> 'a::floor_ceiling"