--- a/src/HOL/Analysis/Cartesian_Space.thy Tue Nov 05 19:55:42 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Space.thy Tue Nov 05 21:07:03 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 Tue Nov 05 19:55:42 2019 +0100
+++ b/src/HOL/Analysis/Convex.thy Tue Nov 05 21:07:03 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 Tue Nov 05 19:55:42 2019 +0100
+++ b/src/HOL/Analysis/Determinants.thy Tue Nov 05 21:07:03 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/Finite_Cartesian_Product.thy Tue Nov 05 19:55:42 2019 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Tue Nov 05 21:07:03 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 Tue Nov 05 19:55:42 2019 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy Tue Nov 05 21:07:03 2019 +0100
@@ -806,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"
@@ -1348,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:
@@ -1358,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"
@@ -1419,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)
@@ -1572,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})"
@@ -1615,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:
@@ -1694,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
@@ -1745,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}"
@@ -1753,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
@@ -1787,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
@@ -1845,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