author nipkow Tue, 05 Nov 2019 21:07:15 +0100 changeset 71045 9858f391ed2d parent 71042 400e9512f1d3 (current diff) parent 71044 cb504351d058 (diff) child 71059 9b531e611d66
merged
```--- a/src/HOL/Analysis/Cartesian_Space.thy	Mon Nov 04 20:38:15 2019 +0000
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Tue Nov 05 21:07:15 2019 +0100
@@ -583,7 +583,7 @@
finally show ?thesis .
qed
then show ?thesis
-    by (simp add: dim_span)
+    by (simp)
qed

lemma column_rank_def:
@@ -1028,7 +1028,9 @@
qed

-subsection \<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
+subsection \<open>Finding an Orthogonal Matrix\<close>
+
+text \<open>We can find an orthogonal matrix taking any unit vector to any other.\<close>

lemma  orthogonal_matrix_transpose [simp]:
"orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
@@ -1123,9 +1125,9 @@
qed

-subsection  \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
+subsection  \<open>Scaling and isometry\<close>

-lemma  scaling_linear:
+proposition scaling_linear:
fixes f :: "'a::real_inner \<Rightarrow> 'a::real_inner"
assumes f0: "f 0 = 0"
and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y"
@@ -1158,7 +1160,7 @@
by (metis dist_0_norm)

-subsection  \<open>Can extend an isometry from unit sphere\<close>
+text \<open>Can extend an isometry from unit sphere:\<close>

lemma  isometry_sphere_extend:
fixes f:: "'a::real_inner \<Rightarrow> 'a"
@@ -1393,8 +1395,7 @@
fix A B
assume "P ((*v) A)" and "P ((*v) B)"
then show "P ((*v) (A ** B))"
-      by (auto simp add: matrix_vector_mult_matrix_matrix_mult_compose matrix_vector_mul_linear
-          intro!: comp)
+      by (auto simp add: matrix_vector_mult_matrix_matrix_mult_compose intro!: comp)
next
fix A :: "real^'n^'n" and i
assume "row i A = 0"```
```--- a/src/HOL/Analysis/Convex.thy	Mon Nov 04 20:38:15 2019 +0000
+++ b/src/HOL/Analysis/Convex.thy	Tue Nov 05 21:07:15 2019 +0100
@@ -14,7 +14,7 @@
"HOL-Library.Set_Algebras"
begin

-subsection \<open>Convexity\<close>
+subsection \<open>Convex Sets\<close>

definition\<^marker>\<open>tag important\<close> convex :: "'a::real_vector set \<Rightarrow> bool"
where "convex s \<longleftrightarrow> (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> u *\<^sub>R x + v *\<^sub>R y \<in> s)"
@@ -340,7 +340,7 @@
done

-subsection \<open>Functions that are convex on a set\<close>
+subsection \<open>Convex Functions on a Set\<close>

definition\<^marker>\<open>tag important\<close> convex_on :: "'a::real_vector set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
where "convex_on s f \<longleftrightarrow>
@@ -1865,7 +1865,7 @@
qed

-subsection \<open>Affine dependence and consequential theorems\<close>
+subsection \<open>Affine Dependence\<close>

text "Formalized by Lars Schewe."
```
```--- a/src/HOL/Analysis/Determinants.thy	Mon Nov 04 20:38:15 2019 +0000
+++ b/src/HOL/Analysis/Determinants.thy	Tue Nov 05 21:07:15 2019 +0100
@@ -2,7 +2,7 @@
Author:     Amine Chaieb, University of Cambridge; proofs reworked by LCP
*)

-section \<open>Traces, Determinant of square matrices and some properties\<close>
+section \<open>Traces and Determinants of Square Matrices\<close>

theory Determinants
imports```
```--- a/src/HOL/Analysis/Elementary_Topology.thy	Mon Nov 04 20:38:15 2019 +0000
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Tue Nov 05 21:07:15 2019 +0100
@@ -22,95 +22,6 @@
using openI by auto

-subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Archimedean properties and useful consequences\<close>
-
-text\<open>Bernoulli's inequality\<close>
-proposition Bernoulli_inequality:
-  fixes x :: real
-  assumes "-1 \<le> x"
-    shows "1 + n * x \<le> (1 + x) ^ n"
-proof (induct n)
-  case 0
-  then show ?case by simp
-next
-  case (Suc n)
-  have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
-    by (simp add: algebra_simps)
-  also have "... = (1 + x) * (1 + n*x)"
-    by (auto simp: power2_eq_square algebra_simps  of_nat_Suc)
-  also have "... \<le> (1 + x) ^ Suc n"
-    using Suc.hyps assms mult_left_mono by fastforce
-  finally show ?case .
-qed
-
-corollary Bernoulli_inequality_even:
-  fixes x :: real
-  assumes "even n"
-    shows "1 + n * x \<le> (1 + x) ^ n"
-proof (cases "-1 \<le> x \<or> n=0")
-  case True
-  then show ?thesis
-    by (auto simp: Bernoulli_inequality)
-next
-  case False
-  then have "real n \<ge> 1"
-    by simp
-  with False have "n * x \<le> -1"
-    by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
-  then have "1 + n * x \<le> 0"
-    by auto
-  also have "... \<le> (1 + x) ^ n"
-    using assms
-    using zero_le_even_power by blast
-  finally show ?thesis .
-qed
-
-corollary real_arch_pow:
-  fixes x :: real
-  assumes x: "1 < x"
-  shows "\<exists>n. y < x^n"
-proof -
-  from x have x0: "x - 1 > 0"
-    by arith
-  from reals_Archimedean3[OF x0, rule_format, of y]
-  obtain n :: nat where n: "y < real n * (x - 1)" by metis
-  from x0 have x00: "x- 1 \<ge> -1" by arith
-  from Bernoulli_inequality[OF x00, of n] n
-  have "y < x^n" by auto
-  then show ?thesis by metis
-qed
-
-corollary real_arch_pow_inv:
-  fixes x y :: real
-  assumes y: "y > 0"
-    and x1: "x < 1"
-  shows "\<exists>n. x^n < y"
-proof (cases "x > 0")
-  case True
-  with x1 have ix: "1 < 1/x" by (simp add: field_simps)
-  from real_arch_pow[OF ix, of "1/y"]
-  obtain n where n: "1/y < (1/x)^n" by blast
-  then show ?thesis using y \<open>x > 0\<close>
-    by (auto simp add: field_simps)
-next
-  case False
-  with y x1 show ?thesis
-    by (metis less_le_trans not_less power_one_right)
-qed
-
-lemma forall_pos_mono:
-  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
-    (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
-  by (metis real_arch_inverse)
-
-lemma forall_pos_mono_1:
-  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
-    (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
-  apply (rule forall_pos_mono)
-  apply auto
-  apply (metis Suc_pred of_nat_Suc)
-  done
-
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Affine transformations of intervals\<close>

lemma real_affinity_le: "0 < m \<Longrightarrow> m * x + c \<le> y \<longleftrightarrow> x \<le> inverse m * y + - (c / m)"```
```--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Mon Nov 04 20:38:15 2019 +0000
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Tue Nov 05 21:07:15 2019 +0100
@@ -135,8 +135,7 @@
by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff)
have "CARD('a) ^ CARD('b) = card (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))"
(is "_ = card ?A")
-      by (subst card_PiE) (auto simp: prod_constant)
-
+      by (subst card_PiE) (auto)
also have "?A = Pi UNIV (\<lambda>_. UNIV)"
by auto
finally show "card \<dots> = CARD('a) ^ CARD('b)" ..
@@ -1075,7 +1074,7 @@

lemma matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
apply (vector matrix_vector_mult_def mat_def)
-  apply (simp add: if_distrib if_distribR sum.delta' cong del: if_weak_cong)
+  apply (simp add: if_distrib if_distribR cong del: if_weak_cong)
done

lemma matrix_transpose_mul:```
```--- a/src/HOL/Analysis/Linear_Algebra.thy	Mon Nov 04 20:38:15 2019 +0000
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue Nov 05 21:07:15 2019 +0100
@@ -490,96 +490,6 @@
by (rule adjoint_unique, simp add: adjoint_clauses [OF lf])

-subsection \<open>Archimedean properties and useful consequences\<close>
-
-text\<open>Bernoulli's inequality\<close>
-proposition Bernoulli_inequality:
-  fixes x :: real
-  assumes "-1 \<le> x"
-    shows "1 + n * x \<le> (1 + x) ^ n"
-proof (induct n)
-  case 0
-  then show ?case by simp
-next
-  case (Suc n)
-  have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
-    by (simp add: algebra_simps)
-  also have "... = (1 + x) * (1 + n*x)"
-    by (auto simp: power2_eq_square algebra_simps  of_nat_Suc)
-  also have "... \<le> (1 + x) ^ Suc n"
-    using Suc.hyps assms mult_left_mono by fastforce
-  finally show ?case .
-qed
-
-corollary Bernoulli_inequality_even:
-  fixes x :: real
-  assumes "even n"
-    shows "1 + n * x \<le> (1 + x) ^ n"
-proof (cases "-1 \<le> x \<or> n=0")
-  case True
-  then show ?thesis
-    by (auto simp: Bernoulli_inequality)
-next
-  case False
-  then have "real n \<ge> 1"
-    by simp
-  with False have "n * x \<le> -1"
-    by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
-  then have "1 + n * x \<le> 0"
-    by auto
-  also have "... \<le> (1 + x) ^ n"
-    using assms
-    using zero_le_even_power by blast
-  finally show ?thesis .
-qed
-
-corollary real_arch_pow:
-  fixes x :: real
-  assumes x: "1 < x"
-  shows "\<exists>n. y < x^n"
-proof -
-  from x have x0: "x - 1 > 0"
-    by arith
-  from reals_Archimedean3[OF x0, rule_format, of y]
-  obtain n :: nat where n: "y < real n * (x - 1)" by metis
-  from x0 have x00: "x- 1 \<ge> -1" by arith
-  from Bernoulli_inequality[OF x00, of n] n
-  have "y < x^n" by auto
-  then show ?thesis by metis
-qed
-
-corollary real_arch_pow_inv:
-  fixes x y :: real
-  assumes y: "y > 0"
-    and x1: "x < 1"
-  shows "\<exists>n. x^n < y"
-proof (cases "x > 0")
-  case True
-  with x1 have ix: "1 < 1/x" by (simp add: field_simps)
-  from real_arch_pow[OF ix, of "1/y"]
-  obtain n where n: "1/y < (1/x)^n" by blast
-  then show ?thesis using y \<open>x > 0\<close>
-    by (auto simp add: field_simps)
-next
-  case False
-  with y x1 show ?thesis
-    by (metis less_le_trans not_less power_one_right)
-qed
-
-lemma forall_pos_mono:
-  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
-    (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
-  by (metis real_arch_inverse)
-
-lemma forall_pos_mono_1:
-  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
-    (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
-  apply (rule forall_pos_mono)
-  apply auto
-  apply (metis Suc_pred of_nat_Suc)
-  done
-
-
subsection\<^marker>\<open>tag unimportant\<close> \<open>Euclidean Spaces as Typeclass\<close>

lemma independent_Basis: "independent Basis"
@@ -896,7 +806,7 @@
by (simp add: span_span)
from card_le_dim_spanning[OF CSV SVC C(1)] C(2,3) fB
have iC: "independent C"
-    by (simp add: dim_span)
+    by (simp)
from C fB have "card C \<le> dim V"
by simp
moreover have "dim V \<le> card C"
@@ -1438,8 +1348,7 @@
show ?thesis
apply (rule that[OF b(1)])
apply (rule subspace_dim_equal)
-    by (auto simp: assms b dim_hyperplane dim_span subspace_hyperplane
-        subspace_span)
+    by (auto simp: assms b dim_hyperplane subspace_hyperplane)
qed

lemma dim_eq_hyperplane:
@@ -1448,7 +1357,7 @@
by (metis One_nat_def dim_hyperplane dim_span lowdim_eq_hyperplane)

-subsection\<open> Orthogonal bases, Gram-Schmidt process, and related theorems\<close>
+subsection\<open> Orthogonal bases and Gram-Schmidt process\<close>

lemma pairwise_orthogonal_independent:
assumes "pairwise orthogonal S" and "0 \<notin> S"
@@ -1509,7 +1418,7 @@
if "x \<in> S" for x
proof -
have "a \<bullet> x = (\<Sum>y\<in>S. if y = x then y \<bullet> a else 0)"
-      by (simp add: \<open>finite S\<close> inner_commute sum.delta that)
+      by (simp add: \<open>finite S\<close> inner_commute that)
also have "... =  (\<Sum>b\<in>S. b \<bullet> a * (b \<bullet> x) / (b \<bullet> b))"
apply (rule sum.cong [OF refl], simp)
by (meson S orthogonal_def pairwise_def that)
@@ -1662,8 +1571,7 @@
obtain B where "B \<subseteq> span S" and orthB: "pairwise orthogonal B"
and "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
and "independent B" "card B = dim S" "span B = span S"
-    by (rule orthonormal_basis_subspace [of "span S", OF subspace_span])
-      (auto simp: dim_span)
+    by (rule orthonormal_basis_subspace [of "span S", OF subspace_span]) (auto)
with assms obtain u where spanBT: "span B \<subseteq> span T" and "u \<notin> span B" "u \<in> span T"
by auto
obtain C where orthBC: "pairwise orthogonal (B \<union> C)" and spanBC: "span (B \<union> C) = span (B \<union> {u})"
@@ -1705,11 +1613,11 @@
assumes "dim S < DIM('a)"
obtains x where "x \<noteq> 0" "\<And>y. y \<in> span S \<Longrightarrow> orthogonal x y"
proof -
-have "span S \<subset> UNIV"
+  have "span S \<subset> UNIV"
by (metis (mono_tags) UNIV_I assms inner_eq_zero_iff less_le lowdim_subset_hyperplane
mem_Collect_eq top.extremum_strict top.not_eq_extremum)
with orthogonal_to_subspace_exists_gen [of S UNIV] that show ?thesis
-    by (auto simp: span_UNIV)
+    by (auto)
qed

corollary\<^marker>\<open>tag unimportant\<close> orthogonal_to_vector_exists:
@@ -1784,7 +1692,7 @@
using \<open>independent (S - {0})\<close> independent_imp_finite by blast
show "card (S - {0}) = DIM('a)"
using span_delete_0 [of S] S
-      by (simp add: \<open>independent (S - {0})\<close> indep_card_eq_dim_span dim_UNIV)
+      by (simp add: \<open>independent (S - {0})\<close> indep_card_eq_dim_span)
qed (use S \<open>a \<noteq> 0\<close> in auto)
qed

@@ -1835,7 +1743,7 @@
then have 0: "\<And>x y. \<lbrakk>x \<in> span A; y \<in> span B\<rbrakk> \<Longrightarrow> x \<bullet> y = 0"
by simp
have "dim(A \<union> B) = dim (span (A \<union> B))"
-    by (simp add: dim_span)
+    by (simp)
also have "span (A \<union> B) = ((\<lambda>(a, b). a + b) ` (span A \<times> span B))"
by (auto simp add: span_Un image_def)
also have "dim \<dots> = dim {x + y |x y. x \<in> span A \<and> y \<in> span B}"
@@ -1843,9 +1751,9 @@
also have "... = dim {x + y |x y. x \<in> span A \<and> y \<in> span B} + dim(span A \<inter> span B)"
by (auto simp: dest: 0)
also have "... = dim (span A) + dim (span B)"
-    by (rule dim_sums_Int) (auto simp: subspace_span)
+    by (rule dim_sums_Int) (auto)
also have "... = dim A + dim B"
-    by (simp add: dim_span)
+    by (simp)
finally show ?thesis .
qed

@@ -1877,8 +1785,7 @@
using \<open>y \<in> span A\<close> add.commute by blast
qed
show "span B \<subseteq> span ({y \<in> B. \<forall>x\<in>A. orthogonal x y} \<union> A)"
-      by (rule span_minimal)
-        (auto intro: * span_minimal simp: subspace_span)
+      by (rule span_minimal) (auto intro: * span_minimal)
qed
then show ?thesis
by (metis (no_types, lifting) dim_orthogonal_sum dim_span mem_Collect_eq
@@ -1935,7 +1842,7 @@
show "norm (h (f x) - h l) < e" if "norm (f x - l) < e / B" for x
using that B
apply (simp add: field_split_simps)
-          by (metis \<open>linear h\<close> le_less_trans linear_diff mult.commute)
+          by (metis \<open>linear h\<close> le_less_trans linear_diff)
qed
qed
qed```
```--- a/src/HOL/Real.thy	Mon Nov 04 20:38:15 2019 +0000
+++ b/src/HOL/Real.thy	Tue Nov 05 21:07:15 2019 +0100
@@ -1313,6 +1313,96 @@
by simp

+subsection \<open>Archimedean properties and useful consequences\<close>
+
+text\<open>Bernoulli's inequality\<close>
+proposition Bernoulli_inequality:
+  fixes x :: real
+  assumes "-1 \<le> x"
+    shows "1 + n * x \<le> (1 + x) ^ n"
+proof (induct n)
+  case 0
+  then show ?case by simp
+next
+  case (Suc n)
+  have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
+    by (simp add: algebra_simps)
+  also have "... = (1 + x) * (1 + n*x)"
+    by (auto simp: power2_eq_square algebra_simps)
+  also have "... \<le> (1 + x) ^ Suc n"
+    using Suc.hyps assms mult_left_mono by fastforce
+  finally show ?case .
+qed
+
+corollary Bernoulli_inequality_even:
+  fixes x :: real
+  assumes "even n"
+    shows "1 + n * x \<le> (1 + x) ^ n"
+proof (cases "-1 \<le> x \<or> n=0")
+  case True
+  then show ?thesis
+    by (auto simp: Bernoulli_inequality)
+next
+  case False
+  then have "real n \<ge> 1"
+    by simp
+  with False have "n * x \<le> -1"
+    by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
+  then have "1 + n * x \<le> 0"
+    by auto
+  also have "... \<le> (1 + x) ^ n"
+    using assms
+    using zero_le_even_power by blast
+  finally show ?thesis .
+qed
+
+corollary real_arch_pow:
+  fixes x :: real
+  assumes x: "1 < x"
+  shows "\<exists>n. y < x^n"
+proof -
+  from x have x0: "x - 1 > 0"
+    by arith
+  from reals_Archimedean3[OF x0, rule_format, of y]
+  obtain n :: nat where n: "y < real n * (x - 1)" by metis
+  from x0 have x00: "x- 1 \<ge> -1" by arith
+  from Bernoulli_inequality[OF x00, of n] n
+  have "y < x^n" by auto
+  then show ?thesis by metis
+qed
+
+corollary real_arch_pow_inv:
+  fixes x y :: real
+  assumes y: "y > 0"
+    and x1: "x < 1"
+  shows "\<exists>n. x^n < y"
+proof (cases "x > 0")
+  case True
+  with x1 have ix: "1 < 1/x" by (simp add: field_simps)
+  from real_arch_pow[OF ix, of "1/y"]
+  obtain n where n: "1/y < (1/x)^n" by blast
+  then show ?thesis using y \<open>x > 0\<close>
+    by (auto simp add: field_simps)
+next
+  case False
+  with y x1 show ?thesis
+    by (metis less_le_trans not_less power_one_right)
+qed
+
+lemma forall_pos_mono:
+  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
+    (\<And>n::nat. n \<noteq> 0 \<Longrightarrow> P (inverse (real n))) \<Longrightarrow> (\<And>e. 0 < e \<Longrightarrow> P e)"
+  by (metis real_arch_inverse)
+
+lemma forall_pos_mono_1:
+  "(\<And>d e::real. d < e \<Longrightarrow> P d \<Longrightarrow> P e) \<Longrightarrow>
+    (\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
+  apply (rule forall_pos_mono)
+  apply auto
+  apply (metis Suc_pred of_nat_Suc)
+  done
+
+
subsection \<open>Floor and Ceiling Functions from the Reals to the Integers\<close>

(* FIXME: theorems for negative numerals. Many duplicates, e.g. from Archimedean_Field.thy. *)```